-
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;
}
}
contract C {
state Start {
transaction t(money m) {
this <- S1{m1 = m}
then toS2();
}
}
state S1 {
money m1;
transaction toS2() {
this <- S2{m2 = 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;
}
}
Jonathan objected that option 5 mixes up assignment with mutation. This approach uses new syntax to clarify the situation and merges in the ideas from option 2. We support blocks identified by two new syntaxes:
-
in <S> {…}means "Assert that the current state is S, and then run the code in the block with "this" having type S. -
if in <S> {…}means "Dynamically check the state. If the state is S, run the code in the block with "this" having type S.
Code not in either of those constructs would have the same "this" type as before.
In both cases, the compiler would give an error if it could prove that the current state could NOT be S (unreachable code).
We might also want:
-
verify in <S> {…}, which means "Statically check the state and either prove it is S or give a compile error. Run the code in the block with "this" having type S.
contract C {
state Start {
transaction t(money m) {
->S1({m1 = m})
in S1 {
// The runtime asserts that the state is S1 and either proceeds or throws an exception.
// In this case, we can actually eliminate the runtime check because we can prove statically the type is always C.S1.
->S2({m2 = m1})
}
in S2 {
// Actually, we don't need to do anything in this case, but this is here as an example.
}
m = … // This code runs only if the current state is Start. This code happens to be unreachable (for which the compiler can give an error).
}
}
state S1 {
money m1;
}
state S2 {
money m2;
}
}
This approach has the potential to replace the existing match syntax, except that there are two things missing. One is the ability to do case analysis on objects other than this, but we can fix that with a small extension:
Bond.Proposed b = new Bond();
b.buy();
b.in Purchased {
// in here, b has type "Bond.Purchased"
…
}
// Code here assumes type of b is Bond.Proposed, which is not the case!
// The code here is typechecked as if b: Bond.Purchased
// EXCEPT THAT any code that requires b: Bond.Purchased instead of b: Bond.Proposed will result in an error.
// Examples:
b.buy(); // error: can't buy a purchased bond
println("hello, world"); // OK, has nothing to do with b
b.makePayment(); // error: this code must be in an "in" block
In the above, we enforce that all typestate is expressed explicitly either in variable declarations or in "in" blocks. This provides the documentation-oriented advantages of types. We can also provide IDE-based tooling to do this automatically when necessary (in the example above, moving b.makePayment() into a block rather than giving an error).
The second thing that is missing is the ability to check for match exhaustiveness. This seems mostly relevant when querying about OTHER objects. We could modify the match syntax to look like this:
match b {
in Proposed {
…
}
in Purchased {
…
}
}
The purpose of the match construct would be to enforce exhaustiveness among the in clauses and also abbreviate the in clauses so they need not mention b each time.