Skip to main content

Runtime Assertions (runtime:assert)

The runtime:assert statement both proves a condition at verification time and traps at runtime if the condition is false.

Syntax​

runtime:assert condition;

The verifier checks that condition is provable from preconditions and program state. At runtime, if condition is false, the program traps before the following operation executes.

Dual Behavior​

Unlike assert which is erased from compiled output, runtime:assert has both verification and runtime effects:

PhaseBehavior
VerificationProves condition is true (proof obligation)
RuntimeTraps if condition is false

This makes runtime:assert useful when you want mathematical proof and runtime protection as a safety net. For public exported methods, pair caller-facing proof preconditions with entry_requires when the same guard must be enforced before external callers enter the method.

When to Use runtime:assert​

Use runtime:assert for safety-critical checks where you want both verification and runtime enforcement:

Guarding Division​

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

The verifier proves b != 0 from the precondition. At runtime, the assertion provides defense-in-depth.

Guarding Array Access​

persistent actor {
  var data : [var Int] = [var 1, 2, 3];

  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();
    data[i]
  };
}

The precondition guarantees bounds safety. The runtime assertion documents and enforces this at runtime.

Guarding Option Unwrapping​

persistent actor {
  public func get(opt : ?Nat) : async Nat
    entry_requires opt != null;
    requires opt != null;
  {
    runtime:assert opt != null;
    switch opt {
      case (?v) v;
      case null { 0 };
    }
  };
}

The verifier knows opt is non-null, and the runtime check enforces this guarantee.

Verification Requirements​

The condition must be provable from:

  • Preconditions (requires clauses)
  • Actor invariants
  • Previous assertions in the function
  • Known properties of the program state

If the verifier cannot prove the condition, verification fails.

Provable Assertion​

persistent actor {
  public func ok(x : Nat) : async Nat
    entry_requires x > 0;
    requires x > 0;
  {
    runtime:assert x > 0;  // Provable from precondition
    x
  };
}

This verifies because requires x > 0 implies x > 0.

Unprovable Assertion​

persistent actor {
  public func bad(x : Nat) : async Nat {
    runtime:assert x == 0;  // Cannot be proven - x could be any Nat
    x
  };
}

This fails verification. The function accepts any Nat, so x == 0 is not guaranteed.

Compared to assert​

Aspectassertruntime:assert
VerificationProves conditionProves condition
RuntimeNo effect (erased)Traps if false
Use caseDocumentation, proof stepsSafety-critical guards

Use assert for pure documentation and proof guidance. Use runtime:assert when you need runtime enforcement.

Compared to trap​

Aspectruntime:assert Ptrap cond
VerificationProves P is trueProves cond is false
RuntimeTraps if P is falseTraps if cond is true
Meaning"P must hold here""cond is an error state"

runtime:assert says "this condition is guaranteed." trap says "this error condition is unreachable."

Restrictions​

Not in Pure Functions​

Pure functions cannot contain runtime:assert:

// This is rejected:
pure func bad(x : Nat) : Nat {
  runtime:assert x > 0;  // Error M0240
  x
};

Pure functions are side-effect free and used in specifications. Use requires clauses instead:

pure func good(x : Nat) : Nat
  requires x > 0;
{
  x
};

Not in Lemmas​

Lemma functions also reject runtime:assert:

// This is rejected:
lemma func bad() {
  runtime:assert true;  // Error M0240
};

No old() in Condition​

The old() expression captures state at method entry. Since runtime:assert is runtime code (not ghost), you cannot use old() in its condition:

// This is rejected:
public func bad() : async () modifies x {
  let prev = x;
  x := x + 1;
  runtime:assert x == old(x) + 1;  // Error: old() not allowed
};

Use a local variable to capture the previous value if you need a runtime comparison, or use old() in an ensures clause or static assert when you only need a proof obligation:

public func good() : async () modifies x {
  let prev = x;
  x := x + 1;
  runtime:assert x == prev + 1;  // Works
};

Common Patterns​

Precondition Echo​

Echo the precondition as a runtime assertion:

public func transfer(amount : Nat) : async ()
  modifies balance
  entry_requires amount > 0;
  requires amount > 0;
{
  runtime:assert amount > 0;  // Document and enforce
  balance := balance - amount;
};

Invariant Checkpoint​

Assert an invariant property after state changes:

public func deposit(amount : Nat) : async ()
  modifies balance
{
  balance := balance + amount;
  runtime:assert balance >= amount;  // Cannot underflow
};

Safety Guard Before Dangerous Operation​

Assert safety before operations that could fail:

public func pop() : async Int
  modifies stack
  entry_requires stack.size() > 0;
  requires stack.size() > 0;
{
  runtime:assert stack.size() > 0;
  let last = stack.size() - 1;
  let value = stack[last];
  // ... remove element
  value
};

When Verification Fails​

If verification fails on a runtime:assert, check:

  1. Missing preconditions - Add a requires clause that guarantees the condition
  2. Incorrect assertion - The condition might not actually hold in all cases
  3. Missing intermediate steps - Add assert statements to guide the proof

A failing runtime:assert means either the code has a bug or the specification is incomplete.

Summary​

  • runtime:assert condition proves a property AND traps if false at runtime
  • Must be provable from preconditions, invariants, or program state
  • Use for safety-critical guards (division, bounds, null checks)
  • Cannot appear in pure functions or lemmas
  • Cannot use old() in the condition
  • Provides defense-in-depth: verification catches bugs, runtime catches the unexpected