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.

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

• state constructors (but only addresses part of the problem)
• lift code lexically outside states
• prohibit operations after state change (unworkable)