Case Study: State Transitions and Invariants

Establish safety using the same definitions that drive the program.

19.1 Put updates in one function

To reason about the safety of state updates, make the possible states and operations explicit. Consider a gate that authorizes or revokes permission to spend.

import std::Nat

inductive GateState: Type {
  GateClosed(balance: Nat): GateState
  GateOpen(balance: Nat): GateState
}

inductive GateCommand: Type {
  GateAuthorize: GateCommand
  GateRevoke: GateCommand
  GateSpend: GateCommand
}

fn gate_balance(state: GateState): Nat {
  match state: Nat {
    GateClosed(n) => n
    GateOpen(n) => n
  }
}

// Represent authorization and the balance explicitly in the state.

✓ inductive GateState : Type
✓ inductive GateCommand : Type
✓ def gate_balance : (GateState) -> Nat

GateOpen permits spending; GateClosed does not. A Nat represents the balance.

19.2 Make the transition the specification

fn gate_step(state: GateState, cmd: GateCommand): GateState {
  match cmd: GateState {
    GateAuthorize => GateOpen(gate_balance(state))
    GateRevoke => GateClosed(gate_balance(state))
    GateSpend => match state: GateState {
      GateClosed(n) => GateClosed(n)
      GateOpen(n) => GateOpen(Nat::pred(n))
    }
  }
}

// Keep all state changes in the same pure transition function.

✓ def gate_step : (GateState) -> (GateCommand) -> GateState

GateSpend leaves a closed gate unchanged. If the gate is open, it reduces the balance by one. Nat::pred operates on natural numbers, so its behavior at zero is defined too.

19.3 Declare an invariant

def GateInvariant(capacity: Nat, state: GateState): Prop :=
  gate_balance(state) <= capacity = true

// State that the balance never exceeds the supplied capacity.

✓ def GateInvariant : (Nat) -> (GateState) -> Prop

This proposition says that the current balance is at most the initial capacity: the Boolean comparison must equal true. Prove preservation by each operation, and you can establish preservation over any finite sequence of operations.

The property that GateRevoke always closes the gate follows by computation alone.

import std::Base

theorem revoke_closes(s: GateState): gate_step(s, GateRevoke) = GateClosed(gate_balance(s)) {
  Refl
}

// Computation shows that revocation always produces a closed gate.

✓ theorem revoke_closes : ∀ s: GateState. gate_step(s, GateRevoke) = GateClosed(gate_balance(s))

19.4 Execute the transition you proved

Proving a pure transition does not guarantee an application that uses a separately written, unproved update function. Design the runtime to call the same gate_step that the proof concerns. The repository's examples/certified-state/ demonstrates this arrangement.

Adapters that assign to external mutable cells, extraction, and native runtimes remain separate parts of the trusted system. A mathematical proof of a transition is not the same as mechanical verification of all those components.

Exercise 19.1: What parameters and result type would express that spending at a closed gate leaves the entire state unchanged?