Complete Syntax Reference

This reference documents Sector9 verification syntax: function headers, contracts, ghost code, abstract declarations, assertions, invariants, proof collections, and common actor forms.

Function Headers

Function declarations use Sector9 syntax, derived from Motoko, with verification clauses in the header:

[public|private|system] [shared|shared query|shared sr9] [inline] [pure] [abstract] [trusted] func name<T>(params) : ReturnType
  reads field1, field2
  modifies field3, field4
  entry_requires runtimeGuard;
  requires logicalPrecondition;
  ensures postcondition;
{
  body
};

Common exported actor method:

public shared({caller}) func transfer(to : Principal, amount : Nat) : async Bool
  reads owner
  modifies balance
  entry_requires owner == ?caller;
  entry_requires amount > 0;
  requires owner == ?caller;
  requires amount > 0;
  ensures result == true;
{
  // implementation
  true
};

Rules:

• reads and modifies list actor fields and do not take semicolons.
• Contract clauses such as entry_requires, requires, ensures, and traps_if are written after access clauses and are separated with semicolons.
• shared({caller}) binds the IC caller as a Principal. Do not model caller identity as a user-supplied argument.
• shared query({caller}) binds caller for a query.
• shared sr9 func marks a verified shared boundary. It is required for shared signatures that expose shareable token values.

Contracts

Contracts describe entry guards, caller obligations, return guarantees, and trap behavior.

entry_requires

Runtime entry guard for exported runtime methods.

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

Use entry_requires for facts that an external caller must satisfy at runtime. If the verifier also needs the fact in the body, add the matching requires.

Rules:

• Preserved as a runtime check on exported actor methods.
• Checked by the verifier before the method body.
• Must not depend on ghost-only state.
• Not allowed on declaration-only abstract or bodyless trusted functions.
• Follows normal reads rules when it mentions actor fields.

requires

Logical precondition for verification.

func helper(n : Nat) : Nat
  requires n > 0;
  ensures result > n;
{
  n + 1
};

Callers must prove every requires clause before calling the function. requires is not emitted as a runtime check by itself.

ensures

Postcondition. Use result for the returned value and old(expr) for method-entry state.

public func deposit(amount : Nat) : async ()
  modifies balance
  entry_requires amount > 0;
  requires amount > 0;
  ensures balance == old(balance) + amount;
{
  balance += amount;
};

Multiple ensures clauses are conjoined.

traps_if and aborts_if

Trap/abort summaries for functions that may fail instead of returning normally.

func checkedDiv(a : Nat, b : Nat) : Nat
  traps_if b == 0;
  requires b != 0;
  ensures result == a / b;
{
  a / b
};

aborts_if is accepted as an alias for trap-style summaries.

decreases

decreases is parsed, but Sector9 currently verifies partial correctness only. In verification mode, decreases clauses are rejected; remove them.

Access Clauses

modifies

Declares actor fields a function may write.

public func setLimit(n : Nat) : async ()
  modifies limit
  ensures limit == n;
{
  limit := n;
};

reads

Declares actor fields a function may read without modifying.

public func getLimit() : async Nat
  reads limit
  ensures result == limit;
{
  limit
};

reads and modifies may appear in either order:

public func boundedDeposit(amount : Nat) : async ()
  reads limit
  modifies balance
  entry_requires amount <= limit;
  requires amount <= limit;
{
  balance += amount;
};

Function Forms

Runtime Functions

Ordinary functions have bodies and are checked unless marked trusted.

public func name(params) : async ReturnType
  entry_requires runtimeGuard;
  requires logicalGuard;
  ensures postcondition;
{
  body
};

Shared Functions and Caller Binding

public shared({caller}) func ownerOnly() : async ()
  reads owner
  entry_requires owner == ?caller;
  requires owner == ?caller;
{
  // only the current owner reaches here
};

Other shared forms:

public shared func noCallerNeeded() : async () { };

public shared query({caller}) func queryCaller() : async Principal {
  caller
};

public shared sr9 func verifiedBoundary(t : Token.Token) : async Token.Token {
  t
};

Pure Functions

Pure functions have no side effects and can be used in specifications.

pure func clamp(x : Int, lo : Int, hi : Int) : Int
  requires lo <= hi;
  ensures result >= lo;
  ensures result <= hi;
{
  if (x < lo) lo else if (x > hi) hi else x
};

Restrictions:

• No state mutation.
• No async/await.
• No runtime assert, runtime:assert, or trap.
• Non-ghost pure functions cannot access actor fields.
• Plain pure recursion is not allowed; use a verified iterative form or an explicit trusted boundary.

Inline Pure Functions

inline pure func toNat(x : Nat8) : Nat {
  x
};

inline functions must be pure, must have a body, and cannot be trusted, abstract, or declaration-only.

Ghost Functions

Ghost functions are proof-only helpers. They are erased from runtime code.

public ghost func addEntry(m : Map<Nat, Int>, k : Nat, v : Int) : Map<Nat, Int>
  ensures Map.getOr(result, k, 0) == v;
{
  Map.update(m, k, v)
};

Ghost functions may use proof-only types such as Map, Set, Seq, and Multiset.

Abstract Functions

abstract functions are bodyless verifier placeholders. Use them for VDD stubs and proof interfaces.

public ghost abstract func distance(a : Int, b : Int) : Nat
  requires true;
  ensures result >= 0;

Other valid forms:

public pure abstract func specValue(x : Int) : Int
  requires true;
  ensures result == x + 1;

public abstract ghost func chooseGreater(x : Int) : Int
  requires true;
  ensures result > x;

Rules:

• No body.
• Not compiled or run; refine by removing abstract and adding a body.
• Cannot be combined with trusted.
• Cannot be inline.
• Cannot use entry_requires.
• Preconditions are still checked at every call site; postconditions are assumed while abstract.

Lemmas

Lemmas are proof-only functions. They are implicitly pure and erased from runtime.

public lemma addPositive(x : Nat, y : Nat) : ()
  requires x > 0;
  requires y > 0;
  ensures x + y > x;
{
};

Call lemmas from proof code to establish their postconditions:

public lemma useLemma(a : Nat, b : Nat) : ()
  requires a > 0;
  requires b > 0;
  ensures a + b > a;
{
  addPositive(a, b);
};

Abstract lemmas state a proof obligation without a body:

public abstract lemma monotonic(a : Nat, b : Nat) : ()
  requires a <= b;
  ensures a + 1 <= b + 1;

Trusted Functions

trusted functions skip body verification and assume their contracts.

public trusted func externalHash(x : Blob) : Nat
  requires true;
  ensures result >= 0;
{
  0
};

Trusted bodyless declarations are still accepted for explicit trusted assumptions:

public ghost trusted func externalFact(x : Nat) : Nat
  requires true;
  ensures result >= x;

Prefer abstract for temporary VDD placeholders. Use trusted only for deliberate trusted-base assumptions or unchecked implementations.

Assertions and Traps

assert

Verification-only proof obligation. It does not generate a runtime check.

assert condition;

runtime:assert

Both a proof obligation and a runtime check.

runtime:assert condition;

trap

Runtime trap. Verification treats the trapped path as non-returning and checks that invariants are preserved where required.

trap true;
trap true "error message";

Invariants

Actor Invariants

Actor invariants must hold at public method boundaries and await boundaries.

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

  invariant balance <= totalDeposits;

  public func deposit(amount : Nat) : async ()
    modifies balance, totalDeposits
    entry_requires amount > 0;
    requires amount > 0;
  {
    totalDeposits += amount;
    balance += amount;
  };
}

Loop Invariants

Loop invariants are written inside loop bodies.

while (i < n) {
  loop:invariant i <= n;
  loop:invariant sum >= 0;
  sum += i;
  i += 1;
};

Ghost State

Ghost state is proof-only and erased from compiled output.

Ghost Variables

ghost var name : Type = initialValue;

Example:

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

  invariant balance <= totalMinted;
}

Ghost variables can appear in verifier-only clauses such as requires, ensures, invariant, reads, and modifies. They cannot appear in entry_requires, because entry guards are runtime checks.

Ghost Blocks

ghost {
  statement;
};

Example:

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

Ghost Let Bindings

ghost let snapshot = expression;

Phase Blocks

Phase blocks describe verified chunks of shared-method execution around suspension points.

phase name
  reads field1
  modifies field2
  requires precondition;
  ensures postcondition;
do {
  body
};

Compact form:

phase start modifies counter; ensures counter == old(counter) + 1; do {
  counter += 1;
};

Rules:

• Phase blocks are for shared function bodies.
• Phase blocks are not allowed on trusted or declaration-only functions.
• Clauses may include reads, modifies, requires, and ensures.
• old() in a phase refers to the method-entry state, not the previous phase.

Logical Operators

Operator	Meaning
a ==> b	implication
a <==> b	biconditional
a and b	conjunction
a or b	disjunction
not a	negation

Examples:

requires amount > 0 and amount <= balance;
ensures old(balance) >= amount ==> balance == old(balance) - amount;
ensures result <==> count == 0;

old()

Captures method-entry state.

old(expression)

Allowed mainly in:

• ensures clauses.
• Ghost/proof code.
• Phase postconditions.

Not allowed in:

• requires.
• entry_requires.
• Actor invariants.
• Pure function contracts.

Example:

ensures balance == old(balance) + amount;

Quantifiers

forall

forall<T>(pure func (x : T) : Bool = property)

Example:

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

forallWith

Explicit trigger form:

forallWith<T>(
  pure func (x : T) : Bool = property,
  [pure func (x : T) : Bool = triggerExpression]
)

Example:

assert forallWith<Nat>(
  pure func (i : Nat) : Bool = i < data.size() ==> data[i] >= 0,
  [pure func (i : Nat) : Bool = data[i]]
);

Valid triggers include array accesses, field accesses, pure function calls, and spec-collection operations. Comparisons, arithmetic, and logical operators are not valid triggers.

exists

exists<T>(pure func (x : T) : Bool = property)

Example:

assert exists<Nat>(pure func (n : Nat) : Bool = n == 42);

Spec Collections

Spec collections are immutable mathematical values for verification. They are proof-oriented and require spec-immutable element/key/value types, except that opaque/token handles may appear by identity.

Map

Map.empty<K, V>()
Map.update(m, k, v)
Map.get(m, k)
Map.getOr(m, k, default)
Map.contains(k, m)
Map.domain(m)
Map.card(m)

Set

Set.empty<T>()
Set.singleton(e)
Set.contains(e, s)
Set.card(s)
Set.union(s1, s2)
Set.intersect(s1, s2)
Set.minus(s1, s2)
Set.subset(s1, s2)

Seq

Seq.empty<T>()
Seq.singleton<T>(e)
Seq.len(s)
Seq.get(s, i)
Seq.concat(s1, s2)
Seq.update(s, i, v)
Seq.take(s, n)
Seq.drop(s, n)
Seq.slice(s, i, j)
Seq.contains(e, s)
Seq.sorted(s)
Seq.permutes(a, b)

Multiset

Multiset.empty<T>()
Multiset.singleton(e)
Multiset.count(m, e)
Multiset.contains(e, m)
Multiset.card(m)
Multiset.union(m1, m2)
Multiset.intersect(m1, m2)
Multiset.minus(m1, m2)

Rejected element/key/value types include mutable records, mutable arrays, functions, actors, and async types.

Verification Type Wrappers

opaque

public type Handle = opaque { id : Nat; var amount : Nat };

opaque T is module-owned and verification-only. Outside the defining module, it cannot be inspected structurally. It can still be stored, compared, and passed as a handle identity. Non-owner modules may route it through synchronous module APIs, including nested inside ordinary carriers and supported collections, when the verifier has the relevant handle-capability summary. Validity is implicit in the folded owner carrier; there is no generated public valid(handle) observer.

token

public type Token = token { ticker : Text; minter : Principal; var amount : Nat };

token T is module-owned and can be transported through verified shared sr9 boundaries using the generated shared wrapper rules. Outside shared boundaries it follows the same sealed-handle rule as opaque: non-owner code can hold and pass the identity, but only the owner module can inspect or mutate the payload directly. Stable token state persists as raw token state under the same defining-module CHASH, not through toShared or fromShared.

Operators

Comparison

Operator	Meaning
==	equality
!=	not equal
<	less than
>	greater than
<=	less or equal
>=	greater or equal

Arithmetic

Operator	Meaning
+	addition
-	subtraction
*	multiplication
/	division
%	modulo
**	exponentiation

Division and modulo require non-zero guards:

entry_requires b != 0;
requires b != 0;
ensures result == a / b;

Precedence

From highest to lowest:

1. **
2. *, /, %
3. +, -
4. ==, !=, <, >, <=, >=
5. and
6. or
7. ==>, <==>

Use parentheses to make proof conditions explicit.

Actor Skeleton

persistent actor {
  var runtimeField : Nat = 0;
  var owner : ?Principal = null;
  ghost var proofField : Nat = 0;

  invariant runtimeField <= proofField;

  public shared({caller}) func method(amount : Nat) : async Nat
    reads owner
    modifies runtimeField, proofField
    entry_requires owner == ?caller;
    entry_requires amount > 0;
    requires owner == ?caller;
    requires amount > 0;
    ensures result == runtimeField;
  {
    runtimeField += amount;
    ghost { proofField := proofField + amount; };
    runtimeField
  };

  public ghost abstract func proofInterface(x : Nat) : Nat
    requires true;
    ensures result >= x;
}

Summary

Construct	Placement	Verified	Runtime
entry_requires	Function header	Yes	Yes
requires	Function header	Yes	No
ensures	Function header	Yes	No
traps_if / aborts_if	Function header	Yes	Summary only
reads	Function header	Yes	No
modifies	Function header	Yes	No
assert	Statement	Yes	No
runtime:assert	Statement	Yes	Yes
trap	Statement	Yes	Yes
invariant	Actor/module body	Yes	No
loop:invariant	Loop body	Yes	No
ghost var	Actor/module/function	Yes	No
ghost { }	Statement	Yes	No
ghost func	Declaration	Yes	No
pure func	Declaration	Yes	Yes if reachable
abstract func	Declaration	Assumed contract	No
lemma	Declaration	Yes	No
abstract lemma	Declaration	Assumed contract	No
trusted func	Declaration	Contract assumed	Body exists if provided
phase ... do	Shared method body	Yes	Body is runtime
old()	Postconditions/ghost/phase postconditions	Yes	No
forall / exists	Specifications and ghost code	Yes	No
shared({caller})	Shared function header	Yes	Yes
shared sr9	Shared function header/type	Yes	Yes