Skip to main content

Static Assertions (assert)

The assert statement declares a property that the verifier must prove. It has no runtime effect.

Syntax​

assert condition;

The verifier checks that condition is true at the point where the assertion appears. If verification succeeds, the condition holds for all modeled executions that reach that point under the current specifications and trusted assumptions. If verification fails, the condition might be false in some execution.

Verification-Only​

Static assertions exist only during verification. They are completely erased from compiled output:

public func example(x : Nat) : async Nat {
  assert x >= 0;  // Proven at verification time, removed at runtime
  x + 1
};

This is different from runtime:assert, which both verifies the condition and traps at runtime if it is false.

Using Assert to Document Knowledge​

Assertions serve as machine-checked documentation. When you know a property holds, assert it:

public func add_values(a : Nat, b : Nat) : async Nat
  ensures result >= 0;
  ensures result == a + b;
{
  assert a >= 0;  // Nat is always non-negative
  assert b >= 0;  // Same for b
  a + b
};

The verifier confirms your understanding is correct. If you're wrong, verification fails.

Using Assert to Break Down Proofs​

Complex postconditions often require intermediate steps. Insert assertions to guide the verifier:

public func omitPick() : async Nat
  ensures result == 1;
{
  let a = mkA(1, 2);
  let b = mkB(3, 4);
  let c = mkC(5, 6, 7);
  let r = { ...a; ...b; ...c; c = 9 };
  let ab : AB = { v = r.v; c = r.c; d = r.d };
  let ac : AC = { v = r.v; e = r.e };

  // Document field values after spreading
  assert ab.c == 9;
  assert ab.d == 4;
  assert ac.v == 5;
  assert ac.e == 7;

  1
};

Each assertion gives the verifier a checkpoint, making complex proofs easier.

Common Patterns​

Type Bounds​

Assert bounds that follow from types:

public func check_nat_lower_bound() : async () modifies value {
  let v = value;  // value : Nat
  assert v >= 0;  // Always true for Nat
};

For bounded types, assert both bounds:

public func check_nat8_bounds(x : Nat8) : async () {
  assert x >= 0;
  assert x <= 255;
};

Nested Field Access​

Assert properties of nested data:

public func check_nested_nat() : async () modifies nested {
  let n = nested.inner.n;
  assert n >= 0;
};

Arithmetic Properties​

Assert relationships between values:

public func multiply(a : Nat, b : Nat) : async Nat
  ensures result >= 0;
{
  let product = a * b;
  assert product >= 0;  // Non-negative times non-negative
  product
};

Expressions in Assertions​

Assertions accept boolean expressions. You can use:

  • Comparisons: x >= 0, a == b, n < 10
  • Logical operators: a and b, a or b, not a
  • Implication: a ==> b (if a then b)
  • Biconditional: a <==> b (a if and only if b)
  • Field access: record.field >= 0
  • Function calls to pure functions: isValid(x)

Assertions can call pure functions because they are part of the specification language. They cannot perform an impure method call or any expression with runtime side effects. If you need to reason about a method's result, call the method in normal code and bind the returned value first:

// Wrong: assert someMethod() == 5;

// Correct:
let result = someMethod();
assert result == 5;

Restrictions​

Not in Pure Functions​

Pure functions cannot contain assertions:

// This is rejected:
pure func bad(x : Nat) : Nat {
  assert x >= 0;  // Error: pure functions cannot contain assertions
  x + 1
};

Use requires and ensures clauses instead:

pure func good(x : Nat) : Nat
  requires x >= 0;
  ensures result >= x;
{
  x + 1
};

Not in Lemmas​

Lemma functions also cannot contain assertions:

// This is rejected:
lemma func bad() {
  assert true;  // Error: lemma functions cannot contain assertions
};

Verification Mode Required​

The assert keyword is only available in verification mode. In normal compilation, it produces error M0181.

Assert vs Other Assertions​

StatementVerificationRuntime
assert PProves P is trueNo effect (erased)
runtime:assert PProves P is trueTraps if P is false
trap condProves cond is falseTraps if cond is true

Use assert when you want to prove a property without any runtime overhead. Use runtime:assert when you want both proof and runtime protection. Use trap to mark error conditions as unreachable.

When Verification Fails​

If the verifier cannot prove an assertion, check:

  1. Missing preconditions - Does the caller need to guarantee something?
  2. Missing invariants - Should the actor have an invariant for this property?
  3. Incorrect assumption - Is the assertion actually true in all cases?

A failing assertion often reveals a real bug or an incomplete specification.

Summary​

  • assert condition proves a property at verification time
  • No runtime effect - completely erased from compiled output
  • Use to document knowledge and break down complex proofs
  • Cannot appear in pure functions or lemmas
  • If verification fails, either the code or the assertion needs fixing