Example Gallery

A curated collection of complete, runnable examples demonstrating Sector9 verification patterns. Each example is self-contained and can be verified independently.

---

Getting Started Examples

Basic examples to understand core verification concepts.

Verified Counter

The simplest verified actor: a counter with postconditions proving correctness.

counter.sr9

// Your first verified program
// A simple counter with a postcondition

persistent actor {
  var count : Nat = 0;

  // The `ensures` clause proves the return value equals count
  public func get() : async Nat
    reads count
    ensures result == count;
  {
    count
  };

  // Proves that count increases by exactly 1
  public func increment() : async Nat
    modifies count
    ensures count == old(count) + 1;
    ensures result == count;
  {
    count += 1;
    count
  };
}

Key Points:

• ensures result == count proves the return value matches the field
• ensures count == old(count) + 1 proves increment adds exactly one
• modifies count declares which fields change
• reads count declares which fields are accessed

---

Token and Balance Systems

Patterns for financial applications requiring conservation laws.

Token Conservation

Track minting and burning with ghost variables to prove tokens are never created from nothing.

token-conservation-basic.sr9

// Basic token conservation pattern
persistent actor {
  var balance : Nat = 0;
  var totalMinted : Nat = 0;
  var totalBurned : Nat = 0;

  // Conservation invariant: minted tokens are either live or burned
  invariant balance + totalBurned == totalMinted;

  public func mint(amount : Nat) : async ()
    modifies balance, totalMinted
    reads totalBurned
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;
    ensures totalMinted == old(totalMinted) + amount;
  {
    balance += amount;
    totalMinted += amount;
  };

  public func burn(amount : Nat) : async ()
    modifies balance, totalBurned
    reads totalMinted
    entry_requires amount > 0;
    entry_requires amount <= balance;
    requires amount > 0;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
    ensures totalBurned == old(totalBurned) + amount;
  {
    balance -= amount;
    totalBurned += amount;
  };
}

Key Points:

• ghost var declares verification-only state (erased at runtime)
• invariant balance == totalMinted - totalBurned enforces conservation
• Ghost blocks (ghost { ... }) update ghost state alongside runtime state
• The invariant is checked at every public function entry and exit

Multi-Account Token Transfer Model

For systems with multiple accounts, keep deployable balances in runtime state and use ghost maps as proof models. The helper below is proof-only; it models the abstract map update for a transfer.

module {
  public ghost func transferModel(
    balances : Map<Nat, Nat>,
    from : Nat,
    to : Nat,
    amount : Nat
  ) : Map<Nat, Nat>
    requires from != to;
    requires Map.getOr(balances, from, 0) >= amount;
    ensures Map.getOr(result, from, 0) == Map.getOr(balances, from, 0) - amount;
    ensures Map.getOr(result, to, 0) == Map.getOr(balances, to, 0) + amount;
  {
    let afterDebit = Map.update(balances, from, Map.getOr(balances, from, 0) - amount);
    Map.update(afterDebit, to, Map.getOr(balances, to, 0) + amount)
  };
}

Key Points:

• Map<Nat, Nat> is a proof-only spec collection for key-value reasoning
• Map.getOr provides a default for missing keys
• Runtime ledgers should pair deployable storage with a ghost model

---

Access Control Patterns

Patterns for authorization and permission checking.

Single Owner Pattern

Restrict operations to a single owner with ownership transfer capability.

access-owner-pattern.sr9

// Single owner pattern with ownership transfer
persistent actor {
  var balance : Nat = 0;
  var owner : ?Principal = null;

  // First caller claims ownership
  public shared({caller}) func claimOwnership() : async ()
    modifies owner
    entry_requires owner == null;
    requires owner == null;
    ensures owner == ?caller;
  {
    owner := ?caller;
  };

  // Only owner can deposit
  public shared({caller}) func deposit(amount : Nat) : async ()
    modifies balance
    reads owner
    entry_requires owner == ?caller;
    entry_requires amount > 0;
    requires owner == ?caller;
    requires amount > 0;
    ensures balance == old(balance) + amount;
  {
    balance := balance + amount;
  };

  // Only owner can withdraw
  public shared({caller}) func withdraw(amount : Nat) : async ()
    modifies balance
    reads owner
    entry_requires owner == ?caller;
    entry_requires amount <= balance;
    requires owner == ?caller;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance := balance - amount;
  };

  // Only owner can transfer ownership
  public shared({caller}) func transferOwnership(newOwner : Principal) : async ()
    modifies owner
    entry_requires owner == ?caller;
    requires owner == ?caller;
    ensures owner == ?newOwner;
  {
    owner := ?newOwner;
  };

  // Anyone can check the owner
  public func getOwner() : async ?Principal
    reads owner
    ensures result == owner;
  {
    owner
  };
}

Key Points:

• entry_requires owner == ?caller enforces owner-only entry at runtime
• requires owner == ?caller gives the verifier the matching proof fact
• Ownership transfer changes who can perform protected operations
• Runtime state tracks authorization; ghost state can mirror proof models

Role-Based Access Control

For more complex systems, use runtime role state for authorization. Ghost sets can mirror role membership for proofs, but they are not deployable access-control state.

persistent actor {
  var admin : ?Principal = null;
  var operator : ?Principal = null;

  public shared({caller}) func claimAdmin() : async ()
    modifies admin
    entry_requires admin == null;
    requires admin == null;
    ensures admin == ?caller;
  {
    admin := ?caller;
  };

  public shared({caller}) func setOperator(account : Principal) : async ()
    modifies operator
    reads admin
    entry_requires admin == ?caller;
    requires admin == ?caller;
    ensures operator == ?account;
  {
    operator := ?account;
  };

  public shared({caller}) func operatorAction() : async ()
    reads operator
    entry_requires operator == ?caller;
    requires operator == ?caller;
  {
    // Operator-only action
  };
}

Key Points:

• entry_requires performs the deployable access check
• Runtime fields or runtime collections store live roles
• Ghost sets are useful for proofs about roles, not runtime authorization

---

State Machine Patterns

Model valid state transitions with variant types and guards.

Order State Machine

Enforce a linear progression through order states.

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 Points:

• Variant types ({ #pending; #confirmed; ... }) enumerate valid states
• requires status == #pending ensures valid transitions
• ensures status == #confirmed guarantees the new state
• Invalid transitions (e.g., pending -> delivered) are statically rejected

State Machine with Payload

Track additional data that depends on the current state.

persistent actor {
  type State = {
    #idle;
    #active : { startTime : Nat };
    #completed : { startTime : Nat; endTime : Nat };
  };

  var state : State = #idle;

  invariant switch (state) {
    case (#completed({ startTime; endTime })) { startTime <= endTime };
    case (_) { true };
  };

  public func start(now : Nat) : async ()
    modifies state
    entry_requires state == #idle;
    requires state == #idle;
    ensures state == #active({ startTime = now });
  {
    state := #active({ startTime = now });
  };

  public func complete(now : Nat) : async ()
    modifies state
    entry_requires switch (state) { case (#active(_)) { true }; case (_) { false } };
    entry_requires switch (state) { case (#active({ startTime })) { now >= startTime }; case (_) { false } };
    requires switch (state) { case (#active(_)) { true }; case (_) { false } };
    requires switch (state) { case (#active({ startTime })) { now >= startTime }; case (_) { false } };
  {
    switch (state) {
      case (#active({ startTime })) {
        state := #completed({ startTime; endTime = now });
      };
      case (_) { };
    };
  };
}

Key Points:

• Payload data varies by state
• Invariants can use pattern matching to express state-dependent properties
• Preconditions extract and validate payload values

---

Ghost State Patterns

Use ghost state for abstract reasoning about program behavior.

Shadow Variable

Mirror runtime state with ghost state to establish relationships.

ghost-var-basic.sr9

// Basic ghost variable example

persistent actor {
  // Runtime state
  var counter : Nat = 0;

  // Ghost state - exists only for verification
  ghost var shadow : Nat = 0;

  // Invariant relates ghost and runtime state
  invariant counter == shadow;

  public func increment() : async ()
    modifies counter, shadow
    ensures counter == old(counter) + 1;
  {
    counter += 1;
    ghost { shadow := shadow + 1; };
  };

  public func get() : async Nat
    reads counter
    ensures result == counter;
  {
    counter
  };
}

Key Points:

• Ghost variables track abstract properties not needed at runtime
• Invariants relate ghost and runtime state
• Ghost updates must maintain invariants

History Tracking

Record operation history for audit or verification purposes.

persistent actor {
  var balance : Int = 0;
  ghost var history : Seq<Int> = Seq.empty();

  // History records all changes for proof/debugging.

  public func deposit(amount : Int) : async ()
    modifies balance, history
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
    ghost {
      history := Seq.append(history, amount);
    };
  };

  public func withdraw(amount : Int) : async ()
    modifies balance, history
    entry_requires amount > 0;
    entry_requires amount <= balance;
    requires amount > 0;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
    ghost {
      history := Seq.append(history, -amount);
    };
  };
}

Key Points:

• Seq<Int> tracks ordered history of changes
• Sum of history equals current balance (conservation)
• History can support audit requirements in postconditions

---

Quantifier Patterns

Express properties over collections and ranges.

Universal Quantification

Prove a property holds for all values.

forall-basic.sr9

// Prove that addition is commutative for all natural numbers
persistent actor {
  public func check() : async () {
    ghost {
      assert forall<Nat>(pure func (i : Nat) : Bool =
        forall<Nat>(pure func (j : Nat) : Bool =
          i + j == j + i));
    };
  };
}

Key Points:

• forall<T>(pure func (x : T) : Bool = ...) expresses universal properties
• Nested forall handles multi-variable properties
• Quantified assertions guide the SMT solver

Array Range Properties

Prove properties about array elements.

persistent actor {
  var data : [var Nat] = [var];

  // All elements are non-negative (trivially true for Nat, but shows pattern)
  pure func allNonNegative(arr : [Nat]) : Bool {
    forall<Nat>(pure func (i : Nat) : Bool =
      i >= arr.size() or arr[i] >= 0)
  };

  // All elements at even indices are even
  pure func evenAtEvenIndices(arr : [Nat]) : Bool {
    forall<Nat>(pure func (i : Nat) : Bool =
      i >= arr.size() or i % 2 != 0 or arr[i] % 2 == 0)
  };

  public func checkProperties() : async ()
    reads data
    ensures allNonNegative(Array.freeze(data));
  {
    // Verification proves the property holds
  };
}

Key Points:

• Pure functions encapsulate quantified properties
• Guard with i >= arr.size() to handle out-of-bounds
• Use ==> to create implications: i < size ==> property

---

Lemma Patterns

Use lemmas to establish facts the verifier needs help proving.

Basic Lemma

Establish arithmetic facts for use in verification.

lemma-basic.sr9

// Basic lemma declaration with preconditions and postconditions
module {
  // A lemma establishing an arithmetic fact
  public lemma addPositive(x : Nat, y : Nat) : ()
    requires x > 0;
    requires y > 0;
    ensures x + y > x;
    ensures x + y > y;
  {
    // Body can be empty - verifier proves postconditions from preconditions
  };

  // Using the lemma to help verify a function
  public func sumPositive(a : Nat, b : Nat) : Nat
    requires a > 0;
    requires b > 0;
    ensures result > a;
    ensures result > b;
  {
    addPositive(a, b);  // Call lemma to establish facts
    a + b
  };
}

Key Points:

• Lemmas have requires and ensures like functions
• Bodies can be empty if the verifier proves postconditions from preconditions
• Call lemmas to inject their postconditions as known facts

Step Lemma for Induction

Break complex proofs into steps.

module {
  // Step lemma: if n squares are at most n^2, so is n+1
  public lemma squareStep(n : Nat) : ()
    requires n > 0;
    ensures (n + 1) * (n + 1) == n * n + 2 * n + 1;
  {
    // Algebraic identity - verifier can prove this
  };

  // Use the step lemma in a loop
  public func sumOfSquares(limit : Nat) : Nat
    ensures result <= limit * limit * limit;
  {
    var sum : Nat = 0;
    var i : Nat = 0;

    while (i < limit) {
      loop:invariant i <= limit;
      loop:invariant sum <= i * i * i;
      if (i > 0) { squareStep(i); };
      sum += i * i;
      i += 1;
    };
    sum
  };
}

Key Points:

• Step lemmas help with inductive arguments
• Call the lemma where its facts are needed
• Loop invariants build on lemma-established facts

---

Spec Collection Patterns

Use Map, Set, Seq, and Multiset for abstract reasoning.

Map Operations

Key-value storage with functional updates.

map-basic.sr9

// Basic Map operations: empty, update, get, contains
persistent actor {
  public func demo() : async () {
    ghost {
      // Create an empty Map
      let m0 : Map<Nat, Int> = Map.empty();

      // Update adds a key-value pair, returns a new Map
      let m1 = Map.update(m0, 1, 10);
      let m2 = Map.update(m1, 2, 20);

      // Check membership
      assert Map.contains(1, m2);
      assert Map.contains(2, m2);
      assert not Map.contains(3, m2);

      // Get values
      assert Map.get(m2, 1) == 10;
      assert Map.get(m2, 2) == 20;
    };
  };
}

Key Points:

• Map.empty() creates an empty map
• Map.update(m, k, v) returns a new map with the binding
• Map.get(m, k) retrieves a value
• Map.contains(k, m) checks membership

Set Operations

persistent actor {
  public func setDemo() : async () {
    ghost {
      let s0 : Set<Nat> = Set.empty();
      let s1 = Set.union(s0, Set.singleton(1));
      let s2 = Set.union(s1, Set.singleton(2));
      let s3 = Set.union(s2, Set.singleton(3));

      // Membership
      assert Set.contains(1, s3);
      assert Set.contains(2, s3);
      assert not Set.contains(4, s3);

      // Cardinality
      assert Set.card(s3) == 3;

      // Set operations
      let s4 = Set.union(Set.union(Set.empty(), Set.singleton(2)), Set.singleton(4));
      let inter = Set.intersect(s3, s4);  // {2}
      let union = Set.union(s3, s4);      // {1, 2, 3, 4}

      assert Set.contains(2, inter);
      assert not Set.contains(1, inter);
      assert Set.card(union) == 4;
    };
  };
}

Sequence Operations

persistent actor {
  public func seqDemo() : async () {
    ghost {
      let s0 : Seq<Nat> = Seq.empty();
      let s1 = Seq.append(s0, 1);
      let s2 = Seq.append(s1, 2);
      let s3 = Seq.append(s2, 3);

      // Length and indexing
      assert Seq.len(s3) == 3;
      assert Seq.get(s3, 0) == 1;
      assert Seq.get(s3, 2) == 3;

      // Slicing
      let slice = Seq.slice(s3, 1, 3);  // [2, 3]
      assert Seq.len(slice) == 2;

      // Concatenation
      let s4 = Seq.concat(s3, s3);  // [1, 2, 3, 1, 2, 3]
      assert Seq.len(s4) == 6;
    };
  };
}

---

Loop Invariant Patterns

Verify loops with inductive invariants.

Array Processing Loop

Track progress through an array with quantified invariants.

persistent actor {
  public func doubleAll(data : [var Nat]) : async ()
    modifies data
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      i >= data.size() or data[i] == old(data[i]) * 2);
  {
    var idx : Nat = 0;

    while (idx < data.size()) {
      loop:invariant idx <= data.size();
      // Processed elements are doubled
      loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
        j >= idx or data[j] == old(data[j]) * 2);
      // Unprocessed elements are unchanged
      loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
        j < idx or j >= data.size() or data[j] == old(data[j]));
      data[idx] := data[idx] * 2;
      idx += 1;
    };
  };
}

Key Points:

• loop:invariant annotates while loops
• Track both processed and unprocessed regions
• Bounds invariant (idx <= data.size()) prevents overflow

Accumulator Loop

Track accumulated values.

persistent actor {
  public func count(data : [Nat]) : async Nat
    ensures result == data.size();
  {
    var total : Nat = 0;
    var idx : Nat = 0;

    while (idx < data.size()) {
      loop:invariant idx <= data.size();
      loop:invariant total == idx;
      total += 1;
      idx += 1;
    };
    total
  };
}

---

Async Verification Patterns

Handle verification across await points.

Invariant Preservation Across Await

Actor invariants must hold before and after await.

persistent actor {
  var balance : Nat = 0;
  var locked : Bool = false;

  invariant not locked ==> balance >= 0;

  public func processPayment(amount : Nat) : async ()
    modifies balance, locked
    entry_requires not locked and balance >= amount;
    requires not locked;
    requires balance >= amount;
  {
    locked := true;

    // Before await: invariant must hold
    // locked = true, so invariant is trivially satisfied

    try { await someExternalCall(); } catch (_) {
      locked := false;
      return;
    };

    // After await: invariant must be re-established
    // External code may have run; recheck state before using it
    if (balance < amount) {
      locked := false;
      return;
    };

    balance -= amount;
    locked := false;
    // Now: not locked and balance >= 0
  };

  func someExternalCall() : async () { };
}

Key Points:

• Invariants are checked at await boundaries
• Design invariants that remain true even after interference
• Use lock flags to weaken invariants during critical sections

---

Pure Function Patterns

Side-effect-free functions usable in specifications.

Pure Predicates

Define reusable conditions for contracts.

module Validation {
  public pure func isValidAmount(amount : Nat) : Bool {
    amount > 0 and amount <= 1_000_000
  };

  public pure func isValidAccount(account : Nat) : Bool {
    account > 0
  };
}

persistent actor {
  var balance : Nat = 0;

  public func deposit(account : Nat, amount : Nat) : async ()
    modifies balance
    entry_requires Validation.isValidAmount(amount);
    entry_requires Validation.isValidAccount(account);
    requires Validation.isValidAmount(amount);
    requires Validation.isValidAccount(account);
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };
}

Key Points:

• Pure functions cannot mutate state or await
• They can appear in requires, ensures, and invariant
• Extract complex conditions into named predicates for clarity

---

Common Mistakes and How to Fix Them

Missing Modifies Clause

// Wrong: modifies clause missing
public func increment() : async ()
  ensures count == old(count) + 1;  // Error: cannot write to count
{
  count += 1;
}

// Correct: declare what you modify
public func increment() : async ()
  modifies count
  ensures count == old(count) + 1;
{
  count += 1;
}

Unguarded Division

// Wrong: division by zero possible
public func average(total : Nat, count : Nat) : async Nat
  ensures result == total / count;
{
  total / count
}

// Correct: explicit non-zero guard
public func average(total : Nat, count : Nat) : async Nat
  entry_requires count > 0;
  requires count > 0;
  ensures result == total / count;
{
  total / count
}

Non-Inductive Loop Invariant

// Wrong: invariant not preserved by loop body
while (i < n)
  loop:invariant sum == i * i;  // Not true after i += 1
{
  sum += 2 * i + 1;
  i += 1;
}

// Correct: invariant holds before and after each iteration
while (i < n)
  loop:invariant sum == i * i;  // (i+1)^2 = i^2 + 2i + 1
{
  sum += 2 * i + 1;  // sum becomes (i+1)^2
  i += 1;            // i becomes i+1, invariant restored
}

---

Summary

This gallery demonstrates the core patterns for Sector9 verification:

Pattern	Key Constructs	Use Case
Token Conservation	ghost var, invariant	Financial correctness
Access Control	entry_requires owner == ?caller plus requires owner == ?caller	Authorization
State Machine	Variant types, transition guards	Protocol states
Ghost State	ghost { }, shadow variables	Abstract properties
Quantifiers	forall, exists	Collection properties
Lemmas	lemma, step functions	Complex proofs
Spec Collections	Map, Set, Seq	Abstract data
Loop Invariants	loop:invariant	Iterative algorithms
Async Safety	Invariants at await	Concurrency
Pure Functions	pure func	Reusable predicates

For more details on any pattern, see the corresponding section in the main documentation.