Quick Reference Card

A concise cheatsheet of Sector9 verification syntax.

Contracts

public func example(x : Nat) : async Nat
  entry_requires x > 0;       // Runtime entry guard for exported methods
  requires x > 0;             // Logical precondition
  ensures result == x + 1;    // Postcondition
{
  x + 1
}

Clause	Purpose	Can Use
entry_requires	Runtime guard for exported actor methods	Parameters, current state, runtime pure calls
requires	Logical caller obligation	Parameters, state, pure calls
ensures	Function guarantee	Parameters, state, result, old(), pure calls

Multiple contracts are conjoined (AND-ed together).

For exported actor methods, pair nontrivial logical requires clauses with entry_requires. entry_requires is runtime-executable, so it cannot use ghost state, old(), result, or proof-only helpers.

Caller Identity

Use Sector9's Motoko-derived shared caller pattern for authorization. Do not pass caller as a normal argument.

persistent actor {
  var owner : ?Principal = null;

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

The result Keyword

ensures result == expected;          // Primitive
ensures result.0 == x;               // Tuple element
ensures result.fieldName == y;       // Record field

Only valid in ensures clauses.

The old() Expression

ensures counter == old(counter) + 1; // Capture pre-state
ensures balance >= old(balance);     // Monotonicity

Captures values at method entry. Valid in postconditions, verification assert statements, ghost/proof code, lemma bodies, and phase postconditions. It is not available in requires, entry_requires, actor invariants, runtime code, or pure function contracts.

Footprints

public func update() : async ()
  reads otherField                   // Read-only access
  modifies counter, balance          // Write access
{
  counter := counter + 1
}

Clause	Permission	Framing
reads	Read	Unchanged after call
modifies	Read + Write	May change

Assertions

assert condition;              // Verification-only (erased at runtime)
runtime:assert condition;      // Verification + runtime trap if false
trap condition;                // Runtime trap if true, proves unreachable
trap condition("message");     // With error message

Type	Verification	Runtime
assert	Proves true	Erased
runtime:assert	Proves true	Traps if false
trap	Proves false	Traps if true

Actor Invariants

persistent actor {
  var balance : Nat = 0;
  var debt : Nat = 0;

  invariant balance >= debt;          // Checked at entry, exit, and before await
  invariant balance <= 1_000_000;     // Multiple invariants AND-ed

  public func getBalance() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  };
}

Loop Invariants

while (i < n) {
  loop:invariant i <= n;              // Must hold before each iteration
  loop:invariant sum == partial(i);   // Inductive property

  sum += arr[i];
  i += 1;
}

Pure Functions

pure func square(x : Int) : Int {
  x * x
}

pure func max(a : Int, b : Int) : Int {
  if (a > b) { a } else { b }
}

Restrictions: No actor-state access, no mutation, no await, and no assert/trap. Plain recursive pure definitions are not the normal verified lane; use an iterative proof, a lemma, or a deliberate trusted boundary when recursion is part of the model.

Ghost State

persistent actor {
  var balance : Nat = 0;
  ghost var totalDeposits : Nat = 0;   // Verification-only field

  public func deposit(amount : Nat) : async ()
    modifies balance, totalDeposits
  {
    balance += amount;
    ghost { totalDeposits += amount; };  // Ghost block
  };
}

Feature	Syntax	Purpose
Ghost variable	ghost var x : T = v	Abstract state tracking
Ghost block	ghost { ... }	Update ghost state
Ghost let	ghost let x = v	Local ghost binding

Ghost Functions

ghost func addModel(current : Nat, amount : Nat) : Nat
  ensures result == current + amount;
{
  current + amount
}

Use ghost func for proof-only pure helpers in contracts, invariants, lemmas, and ghost code. Ghost functions are erased from runtime output and cannot be called by runtime code.

Lemmas

public lemma addPositive(x : Nat, y : Nat) : ()
  requires x > 0;
  requires y > 0;
  ensures x + y > x;
{
  // Body can be empty
}

Call lemmas to establish facts for the verifier.

Abstract Functions

public ghost abstract func balanceModel(account : Principal) : Nat
  ensures result >= 0;

Use abstract func for contract-only specification surfaces while designing or modeling an API. The verifier assumes the written contract, and there is no runtime body.

Trusted Functions

public trusted func fastDivide(a : Nat, b : Nat) : Nat
  requires b > 0;
  ensures result == a / b;
{
  a / b  // Body not verified, contracts assumed
}

Use trusted only for deliberate trusted-base assumptions or unchecked implementations. Prefer ghost func, lemma, or abstract func for proof-only modeling.

Trap Contracts

import Runtime "mo:core/Runtime";

persistent actor {
  public func parsePositive(n : Nat) : async Nat
    traps_if n == 0;
    ensures n != 0 ==> result == n;
  {
    if (n == 0) {
      Runtime.trap("zero")
    };
    n
  };
}

traps_if declares the cases where the function is allowed to trap. Normal returns must establish the negation of the trap condition.

Quantifiers

Universal (forall)

// All elements satisfy property
assert forall<Nat>(pure func (i : Nat) : Bool =
  (i < arr.size()) ==> (arr[i] >= 0));

// With explicit trigger
assert forallWith<Nat>(
  pure func (i : Nat) : Bool = (i < arr.size()) ==> (arr[i] >= 0),
  [pure func (i : Nat) : Bool = arr[i]]
);

Existential (exists)

// At least one element satisfies property
assert exists<Nat>(pure func (i : Nat) : Bool =
  (i < arr.size()) and (arr[i] == target));

Pattern: Use ==> with forall, use and with exists.

Spec Collections

Map

let m : Map<Nat, Int> = Map.empty();
let m2 = Map.update(m, key, value);    // Add/update
let v = Map.get(m, key);               // Spec get; usually guard with contains
let v = Map.getOr(m, key, default);    // Get with default
let exists = Map.contains(key, m);     // Check key
let size = Map.card(m);                // Count keys
let keys = Map.domain(m);              // Keys as Set

Set

let s : Set<Nat> = Set.empty();
let s = Set.singleton(elem);           // Single element
let exists = Set.contains(elem, s);    // Check membership
let size = Set.card(s);                // Count elements
let u = Set.union(s1, s2);             // Union
let i = Set.intersect(s1, s2);         // Intersection
let d = Set.minus(s1, s2);             // Difference
let sub = Set.subset(s1, s2);          // Subset check

Seq

let s : Seq<Nat> = Seq.empty();
let s = Seq.singleton<Nat>(elem);      // Single element
let len = Seq.len(s);                  // Length
let elem = Seq.get(s, index);          // Get element
let exists = Seq.contains(elem, s);    // Check membership
let s2 = Seq.concat(s1, s2);           // Concatenate
let prefix = Seq.take(s, n);           // First n elements
let suffix = Seq.drop(s, n);           // Remove first n
let slice = Seq.slice(s, i, j);        // Elements [i..j)
let s2 = Seq.update(s, i, val);        // Update at index

Multiset

let m : Multiset<Nat> = Multiset.empty();
let m = Multiset.singleton(elem);      // Single element
let exists = Multiset.contains(elem, m); // Check membership
let count = Multiset.count(m, elem);   // Count of element
let total = Multiset.card(m);          // Total count
let u = Multiset.union(m1, m2);        // Union (adds counts)
let i = Multiset.intersect(m1, m2);    // Intersection (min counts)
let d = Multiset.minus(m1, m2);        // Difference (subtracts counts)

Logical Operators

a and b                    // Conjunction
a or b                     // Disjunction
not a                      // Negation
a ==> b                    // Implication (if a then b)
a <==> b                   // Biconditional (a iff b)

Common Patterns

Increment Proof

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

Conditional Postcondition

public func abs(x : Int) : async Int
  ensures x >= 0 ==> result == x;
  ensures x < 0 ==> result == -x;
{
  if (x >= 0) { x } else { -x }
}

Conservation Invariant

ghost var totalIn : Nat = 0;
ghost var totalOut : Nat = 0;
invariant balance == totalIn - totalOut;

Division Safety

public func safeDivide(a : Int, b : Int) : async Int
  entry_requires b != 0;     // Runtime entry guard
  requires b != 0;           // Logical verifier fact
  ensures result == a / b;
{
  a / b
}

Array Bounds

assert forall<Nat>(pure func (i : Nat) : Bool =
  (i < arr.size()) ==> (arr[i] >= 0));

CLI Commands

sector9 --check file.sr9     # Source/import hygiene check, no SMT solving
sector9 --verify file.sr9    # Full Viper verification
sector9 --viper file.sr9     # Emit Viper code
sector9 --verify --tla file.protocol.sr9  # Verify a protocol root with TLA+
sector9 -c file.sr9          # Compile to Wasm

Test Naming

Suffix	Expected Outcome
_sat	Verification succeeds
_unsat	Verification fails
_reject	Type check fails

Summary

• Contracts: entry_requires (exported runtime guard), requires (logical caller obligation), and ensures (function guarantee) in headers
• State: old() for pre-state, result for return value
• Footprints: reads and modifies declare field access
• Assertions: assert (proof), runtime:assert (proof + trap), trap (unreachable)
• Invariants: invariant (actor), loop:invariant (loop)
• Ghost: ghost var, ghost { } for verification-only state
• Ghost functions: ghost func for proof-only helper functions
• Pure: pure func for spec helpers (no side effects)
• Abstract: abstract func for contract-only specification surfaces
• Traps: traps_if / aborts_if for declared trap cases
• Quantifiers: forall (all), exists (some), forallWith (explicit trigger)
• Collections: Map, Set, Seq, Multiset (proof-only/spec immutable values)