State Transitions

Syntax and semantics of 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?

Option 1: simple sequencing. Disadvantage: lexical confusion

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;
  }
}

Option 2: tail-call style.

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;
  }
}

Option 3: move post-state-transition code to appropriate states.

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;
    }
  }
}

Option 4: Lift code outside states.

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})
  }
}

Option 5: explicitly assigning to "this"

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.

5.1: exploring sets of possible state results.

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 | S2) {
      (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. }
      }
    }
  }

  state S1 {
    money m1;
  }

  state S2 {
    money m2;
  }
}