From Motoko

Migrating from standard Motoko to Sector9 verification.

Sector9 is Motoko-like and accepts legacy .mo files, but verification has a stricter supported subset. This guide shows how to migrate Motoko-shaped code into the verified Sector9 surface.

The main shift is not syntax. It is responsibility. In Motoko, many protocol facts live in comments, tests, or developer memory. In Sector9, the facts that other code depends on should move into contracts, state footprints, invariants, verified shared boundaries, and proof-only models. For the broader conceptual overview, read Differences From Motoko.

What Changes

Sector9 derives from Motoko, but its verified surface is now its own language. Compared with standard Motoko, Sector9 adds verification constructs and stricter proof-oriented semantics:

Construct	Purpose	Example
requires	Precondition (caller obligation)	requires x > 0
entry_requires	Runtime entry guard for exported methods	entry_requires x > 0
ensures	Postcondition (function guarantee)	ensures result > 0
modifies	Fields the function may write	modifies balance
reads	Fields the function may read	reads total
invariant	Actor-level property that always holds	invariant balance >= 0
loop:invariant	Property maintained across loop iterations	loop:invariant i <= n
old()	Capture pre-state value in postconditions	ensures balance == old(balance) + 1
assert	Static verification assertion	assert x > 0
runtime:assert	Runtime assertion (traps if false)	runtime:assert x > 0
trap	Runtime trap when condition is true	trap (x == 0)
ghost var	Verification-only variable	ghost var history : Seq<Nat>
ghost func	Proof-only pure helper	ghost func valid(x) { ... }
ghost { }	Verification-only block	ghost { history := ... }
pure	Side-effect-free function	pure func max(a, b)
lemma	Proof helper function	public lemma addCommutes()
trusted	Assumed-correct function	public trusted func external()
==>	Logical implication	x > 0 ==> result > 0
<==>	Logical equivalence	x == 0 <==> result == 0

There are also larger language changes that do not fit neatly into a syntax table: async*/await* control whether an async helper creates an extra interference boundary, token and opaque create module-owned values, sr9 shared methods carry proof meaning at cross-canister boundaries, and the verified type system rejects coercions that would hide mutable identity or drop required contracts.

File Extension

Both .mo and .sr9 extensions work. .sr9 is canonical for new Sector9 sources, while .mo remains legacy-compatible. The suffix does not select a different verifier language; byte-identical sources are intended to parse, typecheck, and verify the same way.

Gradual Adoption Path

Start small and build up. Each step adds more verification without changing runtime behavior, except where you intentionally add runtime entry guards or runtime assertions.

Step 1: Add Simple Postconditions

Start with pure computations. Add ensures to document what functions return:

// Before: Unverified Motoko
public func add(a : Int, b : Int) : async Int {
  a + b
};

// After: Add postcondition
public func add(a : Int, b : Int) : async Int
  ensures result == a + b;
{
  a + b
};

The verifier proves the postcondition holds for all inputs.

Step 2: Add Preconditions

Constrain inputs when necessary:

public func divide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
  ensures result == a / b;
{
  a / b
};

Internal callers must satisfy preconditions. Public actor entrypoints with nontrivial logical requires also need entry_requires guards so the runtime entry facts imply the verifier preconditions.

This is one of the most important migration rules. A Motoko public method can quietly assume that callers behave. A Sector9 public method must either make that assumption trivial, prove it from actor state, or guard it with entry_requires.

Step 3: Declare State Modifications

When functions modify actor state, add modifies clauses:

persistent actor Counter {
  var count : Nat = 0;

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

The old() expression captures the value at method entry.

Step 4: Add Actor Invariants

Express properties that must always hold:

persistent actor Wallet {
  var balance : Nat = 0;

  invariant balance >= 0;

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
};

The verifier checks that every public method preserves the invariant.

Step 5: Add Loop Invariants

When verifying loops, add loop:invariant annotations:

public func sum(n : Nat) : async Nat
  entry_requires n <= 100;
  requires n <= 100;
  ensures result == n * (n + 1) / 2;
{
  var i : Nat = 0;
  var acc : Nat = 0;
  while (i < n) {
    loop:invariant i <= n;
    loop:invariant acc == i * (i + 1) / 2;
    i += 1;
    acc += i;
  };
  acc
};

Loop invariants must be:

• True before the loop starts
• Preserved by each iteration
• Strong enough to prove the postcondition

Step 6: Use Ghost State

Track verification-only properties with ghost variables:

persistent actor TokenLedger {
  var balance : Nat = 0;
  ghost var totalMinted : Nat = 0;

  invariant balance <= totalMinted;

  public func mint(amount : Nat) : async ()
    modifies balance, totalMinted
    ensures balance == old(balance) + amount;
  {
    balance += amount;
    ghost { totalMinted := totalMinted + amount; };
  };
};

Ghost state is erased at compile time but enables richer specifications.

Step 7: Make Shared Boundaries Explicit

When a Motoko actor calls another actor, the type system checks the Candid-level shape of the remote interface. It does not prove that the remote actor preserves the contracts your code is relying on. Sector9 keeps ordinary actor imports, then adds stronger tools for verified interfaces:

• Use shared({caller}) for authorization based on caller identity.
• Use entry_requires for deployed public-entry checks.
• Use sr9 shared methods when a proof-enabled boundary matters, especially around token-bearing signatures.
• Use module hashes when asset or protocol identity must be tied to compiled code identity.

This is the path from "my canister is verified in isolation" to "my canister can depend on other verified Sector9 canisters through explicit proof-aware interfaces."

Common Patterns

Option Handling

Use pattern matching in postconditions:

public func increment(opt : ?Nat) : async ?Nat
  ensures
    switch (opt, result) {
      case (null, null) true;
      case (?n, ?m) m == n + 1;
      case (_, _) false;
    };
{
  switch (opt) {
    case (null) null;
    case (?n) ?(n + 1);
  }
};

Conditional Guarantees

Use implication for conditional postconditions:

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

Module Verification

Module functions can have contracts too:

module Math {
  public func max(a : Int, b : Int) : Int
    ensures result >= a;
    ensures result >= b;
    ensures result == a or result == b;
  {
    if (a >= b) { a } else { b }
  };
};

Cross-Canister Verification Mindset

When migrating multi-canister Motoko code, do not start by translating every remote call mechanically. First identify what the caller assumes about the callee: balance conservation, authorization, token identity, result coupling, or a state-machine transition. Put those assumptions into the callee's contracts, public entry guards, and, when relevant, proof-aware sr9 boundaries.

The caller should reason from the callee interface and contracts, not from an unwritten belief about the callee body. For protocol schedules involving several actors and interleavings, use the semantic bridge and TLA/protocol lane alongside local Viper proofs.

What to Avoid

Restrictions on old()

old() captures method entry state. It is only allowed in:

• ensures clauses
• assert statements
• Ghost blocks

Not allowed in:

• requires clauses (there is no prior state at entry)
• Actor invariants
• Pure function contracts
• Runtime code

// WRONG: old() in requires
public func bad() : async Int
  requires old(counter) >= 0  // Error: no prior state at entry
{ ... }

// CORRECT: use current value
public func good() : async Int
  entry_requires counter >= 0;
  requires counter >= 0;
  ensures counter == old(counter) + 1;
{ ... }

Pure Function Restrictions

Pure functions cannot:

• Access actor/module state
• Mutate variables
• Use assert, trap, or runtime:assert
• Call async functions
• Be recursive
• Call uncontracted or effectful function parameters

// WRONG: pure function accessing state
persistent actor {
  var count : Nat = 0;
  pure func bad() : Nat { count }  // Error
};

// CORRECT: pass state as parameter
pure func good(count : Nat) : Nat { count + 1 };

Ghost Block Restrictions

Ghost blocks cannot modify runtime state:

// WRONG: modifying runtime state in ghost block
ghost { balance := 100; };  // Error

// CORRECT: modify in runtime, track in ghost
balance := 100;
ghost { ghostBalance := 100; };

Collection Updates

Spec collections (Map, Set, Seq, Multiset) are persistent values. Updates return new values and do not consume the old version:

ghost {
  let m0 = Map.empty<Nat, Nat>();
  let m1 = Map.update(m0, 1, 10);
  let m2 = Map.update(m0, 2, 20);  // ok: m0 still valid
  assert Map.card(m0) == 0;
}

Unsupported Constructs

The following are not yet supported:

• decreases clauses (termination proofs)
• for loops over iterators whose next() method has no type contract
• Disjunctive patterns in verification-heavy code paths; prefer explicit cases when targeting Viper
• Nested mutable arrays in actor fields, and other deep mutable shapes outside the owned/fresh lanes
• Mutable records in spec collections

Common Errors

Error	Meaning	Fix
M0240	Pure function violation	Remove state access, assertions, or async calls
M0242	Mutable type in collection	Use immutable types in Set/Map/Seq
M0247	Public method has logical requires without entry guard	Add entry_requires, or make the logical precondition trivial
M0313	old() in wrong context	Move to ensures or ghost block
M0314	Ghost variable in runtime	Wrap assignment in ghost { }
M0317	Pure function state access	Pass state as parameter instead
M0335	decreases unsupported	Remove termination clause

Verification Workflow

1. Type check first: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --check file.sr9
2. Verify: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify file.sr9
3. Debug failures: Use --counterexample for failing inputs when the Silicon/Viper server JAR is available
4. Inspect translation: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper file.sr9 shows the Viper IR

Mindset Shift

Testing asks: "Does this work for my test cases?"

Verification asks: "Does this work for ALL possible inputs?"

Write contracts that express your intent:

1. Specify first: Write ensures before implementation
2. Think universally: Consider all inputs, not just common ones
3. Trust contracts: Rely on postconditions, not implementations
4. Strengthen when needed: Add preconditions to rule out invalid cases

Next Steps

After basic contracts work:

• Add actor invariants for state properties
• Use ghost state for abstract properties
• Add loop invariants for verified loops
• Use quantifiers for collection properties
• Read Differences From Motoko for the full language-level comparison
• Use Digital Asset Shared Boundaries before exposing token values or relying on proof-enabled remote calls

Summary

• Sector9 is Motoko-like, with .sr9 canonical and .mo legacy-compatible
• Start with simple requires and ensures clauses
• Add modifies and old() for stateful functions
• Use invariant for actor-level properties
• Add loop:invariant for loops
• Use ghost state for verification-only tracking
• Treat actor imports and shared calls as proof boundaries, not just type signatures
• Avoid common pitfalls: old() placement, pure function restrictions, collection immutability restrictions