Skip to main content

12. Specification Ergonomics & "Phase Blocks"

1. Introduction: The "Async Gap" in Specification​

Most formal specification languages (like Dafny or Move's spec blocks) are designed for Synchronous Logic. They excel at proving that a single function correctly updates state. However, on the Internet Computer, the most critical protocols (like a multi-stage DEX swap or a DAO proposal vote) are Multi-Step Asynchronous Processes.

Standard Hoare logic struggles here because the "Handler" suspends. The developer must manually track the protocol's state using a state machine (e.g., var step : { #Phase1; #Phase2 }). This is error-prone and leads to "State Machine Duplication," where the spec and the implementation both try to manage the protocol's progress.

Sector9 introduces Authored Phase Blocks to solve this. It provides a first-class syntax for interleaving implementation and specification on the async timeline. This research analyzes the implementation in src/verify_shared/phase_surface.ml and the design goals in doc.tla.spec.md.

2. The phase Syntax: Anchoring the Timeline​

Sector9 extends its Motoko-derived language with a dedicated phase construct:

public shared func multi_step_transfer() : async () {
  phase setup modifies this.pending; ensures this.pending == old(this.pending) + 1; do {
    this.pending += 1;
  };

  let res = try { await ledger.transfer(...) } catch (e) { ... };

  phase completion modifies this.pending, this.completed; requires res == #ok; do {
    this.pending -= 1;
    this.completed += 1;
  };
}

Semantic Segmentation​

The phase_surface.ml module acts as the "Extractor" for these blocks. It segments the method body into a Top-Level Layout.

  • Atomic Steps: Each phase block is treated as an atomic transition by both the Viper and TLA+ backends.
  • Separators: The await calls (wrapped in try/catch) are treated as Separators. They mark the points where the protocol yields control to the network.

By using phases, the developer doesn't have to manually manage a step variable. The verifier uses the code's execution pointer (PC) as the implicit state of the protocol.

3. Continuation Bindings and Carried State​

A major ergonomic challenge in multi-step async code is Variable Persistence. In ordinary async code, a variable let x = ... defined before an await is available after the await. But for the verifier, actor state was "havoced" (Subject 1).

The carried Surface​

In phase_surface.ml, Sector9 implements Continuation Bindings.

type continuation_binding = {
  name : M.id;
  visible_from_phase : int;
  (* ... *)
}

If a variable is defined in an earlier phase or as a result of an await (the "separator result"), the system automatically "carries" it into later phase contracts.

  • Viper: Threads carried bindings through the phase contract surface so later phase checks can refer to stable local values without treating actor heap state as unchanged.
  • TLA+: Emits the variable as part of the in-flight message state, ensuring it is available when the second phase of the handler resumes.

This provides the Ergonomic Illusion of Continuity. The developer writes code as if it were synchronous, while the verifier handles the complex cross-await plumbing.

4. Phase-Scoped Temporal Properties​

The true power of phase blocks is revealed in the TLA+ lane. Because each phase has a Label, developers can write temporal properties that refer to these labels.

Example: "No Ghost Completions"​

property #always(Actor.completion ==> Actor.setup happened) This is much easier to write and read than a property that refers to raw line numbers or internal state variables. The phase labels serve as the Semantic API of the protocol for the model checker.

5. Implementation Policy: Straight-Line Restriction​

To keep verification "Push-Button" and stable, Sector9 currently enforces a Straight-Line Policy for authored phases (doc.tla.spec.md).

  • Constraint: A phase-bearing body is currently supported only on shared function bodies and must be a top-level block of phase blocks, optional pure immutable pre-phase bindings, single await try/catch separators, optional suspend-result bindings, and an optional final pure return tail.
  • Reasoning: If phases were allowed inside complex loops or nested if statements, the "Phase Graph" would become an arbitrary CFG. This would make the generated TLA+ model significantly larger and slower to check.

Phase blocks are standalone statements. They cannot contain suspending awaits directly, and phase-bearing bodies do not yet support suspending await*; use explicit await separators when the protocol needs an interleaving point. Phase contracts also keep a restricted expression surface: they can mention parameters, result where allowed, explicit state paths, carried separator values, and array .size() projections, but not arbitrary calls.

By restricting phases to the top-level "Happy Path" and "Error Path," Sector9 focuses on the most common source of protocol bugs: the high-level async schedule.

6. Synthesis: Implicit Phases for Legacy Code​

For code that doesn't use the phase keyword, phase_surface.ml implements Implicit Synthesis.

let synthesize_implicit_top_level_layout_from_decs ...

It looks for AssignE nodes and AwaitE nodes and tries to "Guess" the phases. While useful for bootstrapping, implicit phases lack the descriptive power of authored phases (e.g., they cannot easily carry complex ensures clauses).

7. Evaluation & Comparison​

vs. Solidity (State Machine Pattern)​

In Solidity, developers must manually implement state machines: if (state == State.Pending) { ... }.

  • Solidity: Error-prone. Easy to forget to update the state variable or to allow a function to be called in the wrong state.
  • Sector9: The authored phase is the protocol state marker. The verifier and TLA+ lane can check that later phases only rely on facts carried from earlier phases and modeled await results.

vs. Move (Atomic Scripts)​

Move transactions are atomic. Multi-step protocols must be handled by the client (sending multiple transactions).

  • Move: The protocol logic is often split between the contract (on-chain) and the client (off-chain), making it hard to verify the Whole Protocol.
  • Sector9: The multi-step protocol can be defined in a single Sector9 function. The Viper lane checks local phase contracts, while the TLA+ lane checks modeled async gaps and interleavings.

vs. Session Types (Scribble / P)​

Languages like P use "Session Types" or "State Machines" to define communication protocols.

  • P: Excellent for protocol modeling, but the "Implementation" is often a separate C/Java file that must be manually linked.
  • Sector9: The phase block is the implementation and the spec. There is no mapping gap.

8. Conclusion​

Authored Phase Blocks are one of Sector9's main features for protocol security. They bridge the ergonomic gap between implementation and formal specification, allowing developers to document async intent directly in the code. By automating variable carrying and providing semantic anchors for TLA+, Sector9 reduces the effort required to check complex multi-canister protocols.

Strengths:

  1. Directness: Spec and code live together in the same syntax.
  2. Continuity: Automated carrying of variables across awaits reduces boilerplate.
  3. TLA+ Integration: Phase labels provide a high-level vocabulary for temporal properties.

Weaknesses:

  1. Flexibility: The straight-line restriction prevents modeling more complex branching protocols (though these can often be refactored into multiple public methods).
  2. Verbosity: Large protocols with many phases and carried variables can lead to long function bodies.