Skip to main content

Choosing the Right Assertion

Sector9 provides three assertion forms with distinct verification and runtime behavior. This guide helps you choose the right one.

Quick Decision​

QuestionAnswer
Need runtime protection?Use runtime:assert or trap
Only documenting a proof step?Use assert
Marking an error state as impossible?Use trap
Need an error message?Use trap
Guarding a positive condition?Use runtime:assert

Comparison Table​

Aspectassertruntime:asserttrap
VerificationProves condition trueProves condition trueProves condition false
RuntimeErased (no effect)Traps if falseTraps if true
Performance costZeroNon-zeroNon-zero
Error messageNoNoYes (optional)
Pure/lemma allowedNoNoNo

Decision Flowchart​

Is this for runtime protection or proof documentation?
│
├─► Proof documentation only
│   └─► Use assert
│
└─► Runtime protection
    │
    ├─► Guarding something that MUST be true?
    │   └─► Use runtime:assert
    │
    └─► Marking an error condition as impossible?
        └─► Use trap

When to Use assert​

Use assert when you need zero-cost documentation or proof guidance. The verifier proves the condition, but no runtime code is generated.

Breaking Down Complex Proofs​

public func spread() : async Nat
  ensures result == 1;
{
  let a = { x = 1; y = 2 };
  let b = { z = 3 };
  let c = { ...a; ...b };

  // Document field values after spreading
  assert c.x == 1;
  assert c.y == 2;
  assert c.z == 3;

  1
}

Documenting Type Properties​

public func checkBounds(n : Nat) : async ()
{
  // Nat is always non-negative - verifier proves this
  assert n >= 0;
}

Intermediate Proof Steps​

public func bump(n : Nat) : async Nat
  ensures result == n + 1;
{
  var acc : Nat = 0;
  acc += n;
  assert acc == n;  // Document intermediate state
  acc += 1;
  assert acc == n + 1;  // Matches postcondition
  acc
}

When to Use runtime:assert​

Use runtime:assert for defense-in-depth: the verifier proves the condition, and runtime traps if it fails. This catches unexpected violations. On exported public methods, use entry_requires for the entry guard when outside callers must be rejected before method execution.

Guarding Division​

public func div(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
  ensures result == a / b;
{
  runtime:assert b != 0;  // Proved + runtime guard
  a / b
}

Guarding Array Access​

public func get(i : Nat) : async Int
  reads data
  entry_requires i < data.size();
  requires i < data.size();
  ensures result == data[i];
{
  runtime:assert i < data.size();  // Bounds check
  data[i]
}

Echoing Preconditions​

public func process(opt : ?Nat) : async Nat
  entry_requires opt != null;
  requires opt != null;
{
  runtime:assert opt != null;  // Echo the precondition
  switch opt {
    case (?v) v;
    case null 0;
  }
}

When to Use trap​

Use trap to mark error conditions as unreachable. The verifier proves the condition is false, and runtime traps if it becomes true.

Marking Impossible Branches​

public func unwrap(opt : ?Nat) : async Nat
  entry_requires opt != null;
  requires opt != null;
{
  switch opt {
    case (?v) v;
    case null {
      trap true("Reached null case with non-null precondition");
    };
  }
}

Expressing Negative Invariants​

public func withdraw(amount : Nat) : async ()
  modifies balance
  entry_requires amount <= balance;
  requires amount <= balance;
{
  trap amount > balance;  // Underflow is impossible
  balance := balance - amount;
}

Error Conditions with Messages​

public func transfer(from : Nat, to : Nat, amount : Nat) : async ()
  entry_requires from != to;
  requires from != to;
{
  trap from == to("Cannot transfer to self");
}

runtime:assert vs trap​

These are proof inverses:

  • runtime:assert P - asserts P is true (traps if false)
  • trap P - asserts P is false (traps if true)

Choose based on how you think about the condition:

ConditionUse
"This must be true"runtime:assert
"This must never happen"trap
// These create equivalent proof obligations:
runtime:assert b != 0;
trap b == 0;

// Choose based on intent:
runtime:assert balance >= amount;  // "Balance must cover amount"
trap amount > balance;             // "Underflow must not happen"

Common Patterns​

Precondition Echo Pattern​

Echo preconditions with runtime:assert for defense-in-depth:

public func safeDiv(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;  // Contract for callers
{
  runtime:assert b != 0;  // Runtime guard
  a / b
}

Proof Checkpoint Pattern​

Use assert to document what the verifier knows at each point:

public func compute(x : Nat, y : Nat) : async Nat
  entry_requires x > 0;
  entry_requires y > 0;
  requires x > 0;
  requires y > 0;
  ensures result > 0;
{
  assert x > 0;  // From precondition
  assert y > 0;  // From precondition
  let sum = x + y;
  assert sum >= x;  // Nat addition property
  assert sum > 0;   // Follows from above
  sum
}

Unreachable Branch Pattern​

Use trap for branches that preconditions make impossible:

public func getFirst(arr : [Nat]) : async Nat
  entry_requires arr.size() > 0;
  requires arr.size() > 0;
{
  if (arr.size() == 0) {
    trap true("Empty array with non-empty precondition");
  };
  arr[0]
}

Restrictions​

All three assertion forms are rejected in pure functions and lemmas:

// REJECTED - Error M0240
public pure func bad(x : Nat) : Nat {
  assert x > 0;  // Not allowed in pure functions
  x
}

Use requires/ensures for pure function contracts instead.

The old() expression cannot appear in runtime:assert conditions:

// REJECTED - old() not allowed
public func bad() : async () modifies x {
  x := x + 1;
  runtime:assert x == old(x) + 1;  // Error
}

// CORRECT - use local variable
public func good() : async () modifies x {
  let prev = x;
  x := x + 1;
  runtime:assert x == prev + 1;  // OK
}

Summary​

  • Use assert for zero-cost proof documentation and intermediate steps
  • Use runtime:assert for defense-in-depth when guarding conditions that must be true
  • Use trap for marking error conditions as impossible, especially with error messages
  • All three are rejected in pure functions and lemmas
  • runtime:assert cannot use old() expressions