-
Notifications
You must be signed in to change notification settings - Fork 10
State Transitions
Each Obsidian contract is in one of several states. For simplicity, assume that every contract has a specially-named Start state. To use an artificial but simple example:
resource contract money {…}
contract C {
state Start {
transaction t(money m) {
// Suppose we want to transition to S1 and then S2, each time using "m" as the stored money.
// How does that look?
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}
// external code
C c = new C();
money m = …;
c.t(m);
The question is posed in the comment: //Suppose we want to transition to S1 and then S2, each time using "m" as the stored money. How does that look?
contract C {
state Start {
transaction t(money m) {
->S1({m1 = m})
// Now m1 is in scope even though this code is lexically in the Start state.
// But if the above code could result in more than one possible state, static checking would be impossible.
->S2({m2 = m1})
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}
This option does not seem to be much better because it still requires permitting invoking code from S1 while lexically inside Start.
contract C {
state Start {
transaction t(money m) {
->S1({m1 = m})
toS2(); // allowed because we are in S1 now, but still awkward.
}
}
state S1 {
money m1;
transaction toS2() {
->S2({m2 = m1});
}
}
state S2 {
money m2;
}
}
This option seems more appealing than option 2, but the special syntax here can lead to a lot of nesting. Essentially all code after a state transition requires an extra indent.
contract C {
state Start {
transaction t(money m) {
->S1({m1 = m}) {
->S2({m2 = m1}) // allowed because we are in S1 now, but still awkward.
}
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}
This option addresses the problem at the risk of hard-to-understand code.
contract C {
state Start {
transaction t(money m) {
->S1(m)
// This is confusing; it looks like we should be in S1 after calling t(), but we are actually in S2!
}
}
state S1 {
money m1;
S1(money m) { // State constructor that builds in the behavior we wanted to implement in Start.t().
m1 = m;
->S2();
}
}
state S2 {
money m2;
S2(money m) { // State constructor that builds in the behavior we wanted to implement in S1.S1().
m2 = m;
}
}
}
This addresses the problems above but now it's hard to tell what one can do with a contract in a particular state. Although IDE tools could help with that, it still seems like we lose an important organizational tool.
contract C {
state Start {
}
state S1 {
money m1;
}
state S2 {
money m2;
}
transaction t(money m) available in Start {
->S1({m1 = m})
->S2({m2 = m1})
}
}
Repeated use of "this" seems onerous but this approach at least makes typestate change explicit. But this might get unpleasant when the state is statically unknown (see 5.1).
contract C {
state Start {
transaction t(money m) {
C.S1 this = this->S1({m1 = m})
C.S2 this = this->S2({m2 = m1})
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}
Now, what if someone neglects to assign the result of the state transition to "this"? Perhaps that is a compile error if and only if the typestate of "this" must change as a result. The typestate must change exactly when the result typestate of the transition or invocation is not a subtype of the current typestate of "this".
What if invoking a transaction can result in a set (of size > 1) of possible states? See u().
contract C {
state Start {
transaction t(money m) : (S1 | S2) { // resulting state is either S1 or S2
if (m > 10) {
C.S1 this = this->S1({m1 = m})
}
else {
C.S2 this = this->S2({m2 = m})
}
}
transaction u(money m) : S1 {
(S1 | S2) this = t(m)
switch (this) {
case (S1) { // In this block, the type of this is known to be S1. }
case (S2) { // In this block, the type of this is known to be S2.
S1 this = this->S1({m1 = m2})
}
}
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}