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

• lift code lexically outside states
• prohibit operations after state change (unworkable)