Skip to main content

State Machines

Proving transition guards, valid state invariants, and history tracking for protocol state machines.

State machines model systems that progress through discrete phases with controlled transitions. In smart contracts, state machines enforce protocol logic: an order must be confirmed before shipping, a loan must be approved before disbursement, an auction must close before settlement. Sector9 lets you prove these constraints using variant types, runtime entry guards, logical preconditions, and invariants.

Modeling States with Variants​

Use variant types to define the possible states. Each variant constructor represents a distinct state, optionally carrying data relevant to that state.

state-machine-basic.sr9
// Basic state machine with variant type and transition guards
persistent actor {
  type OrderStatus = { #pending; #confirmed; #shipped; #delivered };

  var status : OrderStatus = #pending;

  public func confirm() : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #confirmed;
  {
    status := #confirmed
  };

  public func ship() : async ()
    modifies status
    entry_requires status == #confirmed;
    requires status == #confirmed;
    ensures status == #shipped;
  {
    status := #shipped
  };

  public func deliver() : async ()
    modifies status
    entry_requires status == #shipped;
    requires status == #shipped;
    ensures status == #delivered;
  {
    status := #delivered
  };
}

Key elements:

  • type OrderStatus defines four discrete states
  • var status holds the current state
  • Each exported transition has an entry_requires runtime guard and a matching requires logical guard
  • Each transition function has an ensures clause that specifies the target state

The verifier proves that ship() can only be called when status is #confirmed, preventing invalid transitions like shipping an unconfirmed order. The state type is just a variant, and the proof comes from contracts plus invariant preservation.

Transition Guards​

For exported actor methods, entry_requires acts as the runtime transition guard and requires acts as the logical proof assumption. They specify which states are valid starting points for each transition.

// Guard: can only ship confirmed orders
public func ship() : async ()
  modifies status
  entry_requires status == #confirmed  // Runtime transition guard
  requires status == #confirmed  // Transition guard
  ensures status == #shipped;
{
  status := #shipped
}

If a caller invokes ship() when status == #pending, the runtime entry_requires guard rejects the call. If internal code calls a helper without establishing its requires, verification fails.

Complex Guards with Switch​

For states with payloads, use switch expressions in guards:

requires switch (loan) { case (#applied amt) amt > 0; case _ false };

This guard accepts only the #applied state with a positive amount.

States with Payloads​

Variant constructors can carry data that flows through the state machine. Use switch expressions to extract and verify payloads.

state-machine-payload.sr9
// State machine with payloads carrying data through transitions
persistent actor {
  type LoanStatus = {
    #applied : Nat;           // Requested amount
    #approved : (Nat, Nat);   // (amount, rate)
    #disbursed : Nat;         // Outstanding balance
    #closed
  };

  var loan : LoanStatus = #applied(0);

  public func apply(amount : Nat) : async ()
    modifies loan
    entry_requires (switch (loan) { case (#applied _) true; case _ false });
    entry_requires amount > 0;
    requires (switch (loan) { case (#applied _) true; case _ false });
    requires amount > 0;
    ensures loan == #applied(amount);
  {
    loan := #applied(amount)
  };

  public func approve(rate : Nat) : async ()
    modifies loan
    entry_requires (switch (loan) { case (#applied amt) amt > 0; case _ false });
    requires (switch (loan) { case (#applied amt) amt > 0; case _ false });
    ensures (switch (old(loan)) {
      case (#applied amt) loan == #approved(amt, rate);
      case _ false
    });
  {
    switch (loan) {
      case (#applied amt) { loan := #approved(amt, rate) };
      case _ { assert false };
    }
  };

  public func disburse() : async ()
    modifies loan
    entry_requires (switch (loan) { case (#approved _) true; case _ false });
    requires (switch (loan) { case (#approved _) true; case _ false });
    ensures (switch (old(loan)) {
      case (#approved (amt, _)) loan == #disbursed(amt);
      case _ false
    });
  {
    switch (loan) {
      case (#approved (amt, _)) { loan := #disbursed(amt) };
      case _ { assert false };
    }
  };
}

Key elements:

  • #applied : Nat carries the requested loan amount
  • #approved : (Nat, Nat) carries amount and interest rate
  • #disbursed : Nat carries the outstanding balance
  • Postconditions reference old(loan) to verify data flows correctly through transitions

The postcondition ensures switch (old(loan)) { case (#applied amt) loan == #approved(amt, rate); ... } proves that the approved amount equals the originally applied amount. Use pattern matching and exhaustiveness checking to keep these state cases explicit.

State-Dependent Invariants​

Actor invariants can reference the current state to express properties that must hold in specific phases.

state-machine-invariant.sr9
// State machine with state-dependent invariants
persistent actor {
  type AuctionState = { #open; #closed; #settled };

  var state : AuctionState = #open;
  var highBid : Nat = 0;
  var settled : Bool = false;

  // Invariant: bids only accepted while open, settlement only when closed
  invariant state == #settled ==> settled == true;
  invariant state == #open ==> settled == false;
  invariant state == #closed ==> settled == false;

  public func bid(amount : Nat) : async ()
    modifies highBid
    reads state, settled
    entry_requires state == #open;
    entry_requires amount > highBid;
    requires state == #open;
    requires amount > highBid;
    ensures highBid == amount;
  {
    highBid := amount
  };

  public func close() : async ()
    modifies state
    reads settled
    entry_requires state == #open;
    requires state == #open;
    ensures state == #closed;
  {
    state := #closed
  };

  public func settle() : async ()
    modifies state, settled
    entry_requires state == #closed;
    requires state == #closed;
    ensures state == #settled;
    ensures settled == true;
  {
    state := #settled;
    settled := true;
  };
}

Key elements:

  • invariant state == #settled ==> settled == true - if settled state, the flag must be set
  • invariant state == #open ==> settled == false - if open, settlement cannot have occurred
  • The verifier checks these invariants hold after every public function

State-dependent invariants encode the meaning of each state. They connect abstract state machine phases to concrete runtime properties, and they are rechecked with the normal invariant preservation rule.

History Tracking with Ghost State​

Ghost variables track properties across transitions without runtime cost. Use them to count transitions, record that certain states were visited, or maintain audit logs.

state-machine-history.sr9
// State machine with ghost history tracking
persistent actor {
  type Phase = { #init; #running; #paused; #stopped };

  var currentPhase : Phase = #init;
  ghost var transitionCount : Nat = 0;
  ghost var hasEverRun : Bool = false;

  invariant currentPhase == #init ==> transitionCount == 0;
  invariant hasEverRun ==> transitionCount > 0;

  public func start() : async ()
    modifies currentPhase, transitionCount, hasEverRun
    entry_requires currentPhase == #init or currentPhase == #paused;
    requires currentPhase == #init or currentPhase == #paused;
    ensures currentPhase == #running;
    ensures transitionCount == old(transitionCount) + 1;
    ensures hasEverRun == true;
  {
    currentPhase := #running;
    ghost {
      transitionCount := transitionCount + 1;
      hasEverRun := true;
    };
  };

  public func pause() : async ()
    modifies currentPhase, transitionCount
    entry_requires currentPhase == #running;
    requires currentPhase == #running;
    ensures currentPhase == #paused;
    ensures transitionCount == old(transitionCount) + 1;
  {
    currentPhase := #paused;
    ghost { transitionCount := transitionCount + 1; };
  };

  public func stop() : async ()
    modifies currentPhase, transitionCount
    entry_requires currentPhase == #running or currentPhase == #paused;
    requires currentPhase == #running or currentPhase == #paused;
    ensures currentPhase == #stopped;
    ensures transitionCount == old(transitionCount) + 1;
  {
    currentPhase := #stopped;
    ghost { transitionCount := transitionCount + 1; };
  };
}

Key elements:

  • ghost var transitionCount tracks total transitions
  • ghost var hasEverRun records whether #running was ever reached
  • Invariants relate ghost state to current state: phase == #init ==> transitionCount == 0
  • Each transition updates both runtime and ghost state

The invariant hasEverRun ==> transitionCount > 0 proves that the history flag is consistent with the transition count.

Combining State Machines with Access Control​

State machines often combine with access control: only certain roles can trigger certain transitions.

state-machine-combined.sr9
// State machine combined with access control
persistent actor {
  type ProposalState = { #draft; #review; #approved; #rejected };

  var proposal : ProposalState = #draft;
  var author : ?Principal = null;
  var reviewer : ?Principal = null;

  pure func isReviewer(reviewer : ?Principal, principal : Principal) : Bool {
    reviewer == ?principal
  };

  // First caller becomes the author
  public shared({caller}) func claimAuthor() : async ()
    modifies author
    entry_requires author == null;
    requires author == null;
    ensures author == ?caller;
  {
    author := ?caller
  };

  // Author assigns the reviewer
  public shared({caller}) func assignReviewer(newReviewer : Principal) : async ()
    modifies reviewer
    reads author
    entry_requires author == ?caller;
    requires author == ?caller;
    ensures reviewer == ?newReviewer;
  {
    reviewer := ?newReviewer
  };

  // Only author can submit for review
  public shared({caller}) func submit() : async ()
    modifies proposal
    reads author
    entry_requires author == ?caller;
    entry_requires proposal == #draft;
    requires author == ?caller;
    requires proposal == #draft;
    ensures proposal == #review;
  {
    proposal := #review
  };

  // Only reviewers can approve
  public shared({caller}) func approve() : async ()
    modifies proposal
    reads reviewer
    entry_requires isReviewer(reviewer, caller);
    entry_requires proposal == #review;
    requires isReviewer(reviewer, caller);
    requires proposal == #review;
    ensures proposal == #approved;
  {
    proposal := #approved
  };

  // Only reviewers can reject
  public shared({caller}) func reject() : async ()
    modifies proposal
    reads reviewer
    entry_requires isReviewer(reviewer, caller);
    entry_requires proposal == #review;
    requires isReviewer(reviewer, caller);
    requires proposal == #review;
    ensures proposal == #rejected;
  {
    proposal := #rejected
  };

  // Author can revise rejected proposals
  public shared({caller}) func revise() : async ()
    modifies proposal
    reads author
    entry_requires author == ?caller;
    entry_requires proposal == #rejected;
    requires author == ?caller;
    requires proposal == #rejected;
    ensures proposal == #draft;
  {
    proposal := #draft
  };
}

This pattern separates concerns:

  • State guards: entry_requires proposal == #draft rejects invalid exported calls; requires proposal == #draft gives the verifier the same logical fact
  • Access guards: entry_requires author == ?caller rejects unauthorized calls; requires author == ?caller gives the verifier the same fact
  • Both must pass: transitions require both valid state and proper authorization

The verifier proves that only the author can submit, only reviewers can approve/reject, and each transition starts from the correct state.

Invalid Transitions​

When an internal transition guard is violated, verification fails. For external callers, the matching entry_requires guard is preserved as the runtime check.

state-machine-invalid_unsat.sr9
// Invalid state transition - skipping required intermediate state
persistent actor {
  type OrderStatus = { #pending; #confirmed; #shipped; #delivered };

  var status : OrderStatus = #pending;

  // WRONG: Tries to ship directly from pending, skipping confirmed
  public func shipDirectly() : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #confirmed;  // Expected next state
  {
    status := #shipped  // Invalid: can't ship unconfirmed order
  };
}

The verifier rejects this code because the body assigns #shipped while the contract promises #confirmed. The _unsat suffix indicates this file intentionally fails verification.

Common Mistakes​

Missing Transition Guards​

// Wrong - no guard, any state can transition
public func ship() : async ()
  modifies status
  ensures status == #shipped;
{
  status := #shipped  // Can ship unconfirmed orders!
}

// Correct - explicit guard
public func ship() : async ()
  modifies status
  entry_requires status == #confirmed
  requires status == #confirmed
  ensures status == #shipped;
{
  status := #shipped
}

Incomplete State Coverage​

When using switch in postconditions, cover all cases:

// Wrong - missing case
ensures switch (r) {
  case (#ok n) result == n;
  // Missing: case (#err _) ...
};

// Correct - exhaustive
ensures switch (r) {
  case (#ok n) result == n;
  case (#err _) result == 0;
};

Payload Mismatches​

Ensure postconditions match what the code actually does:

// Wrong - postcondition claims n+1 but code returns n
public func process(r : Result) : async Nat
  ensures switch (r) { case (#ok n) result == n + 1; case _ result == 0 };
{
  switch (r) { case (#ok n) n; case _ 0 }  // Returns n, not n+1
}

Forgetting Modifies for Ghost State​

// Wrong - missing ghost field in modifies
public func start() : async ()
  modifies phase
{
  phase := #running;
  ghost { transitionCount := transitionCount + 1; };  // Error: transitionCount not in modifies
}

// Correct - all modified fields listed
public func start() : async ()
  modifies phase, transitionCount
{
  phase := #running;
  ghost { transitionCount := transitionCount + 1; };
}

Async and State Machines​

State machine invariants persist across await boundaries. After an await, the invariant is re-established, but specific state values may have changed due to interference. For the full rule, see async interference and commit points.

public func processOrder() : async ()
  modifies status
  entry_requires status == #pending
  requires status == #pending
{
  let confirmation = try { await getConfirmation() } catch (_) { false };
  // After await: invariant holds, but status may have changed
  // by concurrent calls during the await
  if (status == #pending) {
    status := #confirmed;
  };
}

For methods with multiple awaits, recheck state guards after each await when concurrent modifications are possible. The invariant is restored after the commit point, but the exact field value you saw before the await may no longer be current.

State Machine Design Patterns​

Linear State Machines​

States progress in one direction without backtracking:

#pending → #confirmed → #shipped → #delivered

Each transition moves forward; no function transitions backward.

Branching State Machines​

Multiple paths from a single state:

        ┌→ #approved
#review ┤
        └→ #rejected → #draft (revision loop)

Use separate functions for each branch, each with its own guard.

Terminal States​

Some states have no outgoing transitions:

// Terminal state - no transition functions accept #delivered
type OrderStatus = { #pending; #confirmed; #shipped; #delivered };

The absence of a function with requires status == #delivered makes #delivered terminal.

Summary​

  • Model states with variant types: type Status = { #pending; #active; #done }
  • Guard exported transitions with entry guards plus preconditions: entry_requires status == #pending; requires status == #pending
  • Specify targets with postconditions: ensures status == #active
  • Express state meaning with invariants: invariant status == #done ==> completed == true
  • Track history with ghost state: ghost var transitionCount : Nat = 0
  • Combine state guards with access control for real protocols: entry_requires owner == ?caller and status == #draft; requires owner == ?caller and status == #draft
  • Use switch expressions to handle states with payloads
  • Invalid internal transitions fail during verification; invalid external calls are rejected by entry_requires