Trap Conditions (trap)

The trap statement marks an error condition as unreachable. It traps at runtime if the condition is true, and the verifier proves the condition cannot be true at that program point.

Syntax

trap condition;
trap condition("error message");

The verifier checks that condition is provably false at the point where the trap appears. At runtime, if condition is true, the program traps. State rollback follows normal Sector9/Motoko trap semantics: uncommitted effects roll back, while effects already committed before an await are outside that local rollback.

Dual Behavior

Like runtime:assert, the trap statement has both verification and runtime effects:

Phase	Behavior
Verification	Proves condition is false (proof obligation)
Runtime	Traps if condition is true

The key difference from runtime:assert is the direction: trap asserts something is unreachable (the condition should never be true), while runtime:assert asserts something is guaranteed (the condition should always be true).

When to Use trap

Use trap to mark error states that your code should never reach:

Marking Impossible Branches

persistent actor {
  public func upgrade(from : ?Data) : async Data
    entry_requires from != null;
    requires from != null;
  {
    switch from {
      case (?data) data;
      case null {
        trap true("Upgrading from non-existing data");
      };
    }
  };
}

The precondition guarantees from is non-null. The trap marks the null branch as unreachable, and the verifier proves this is true.

Guarding Error Conditions

persistent actor {
  public func ok(x : Nat) : async Nat
    entry_requires x > 0;
    requires x > 0;
  {
    trap x == 0;  // Error condition: division by zero would follow
    100 / x
  };
}

The precondition x > 0 means x == 0 is impossible. The trap documents and enforces this.

Expressing Negative Invariants

persistent actor {
  var balance : Nat = 0;

  public func withdraw(amount : Nat) : async ()
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
  {
    trap amount > balance;  // Underflow would be an error
    balance := balance - amount;
  };
}

The trap asserts that the underflow condition is impossible given the precondition.

Verification Requirements

The condition must be provably false from:

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

If the verifier cannot prove the condition is false, verification fails.

Provable Trap

persistent actor {
  public func ok(x : Nat) : async Nat
    entry_requires x > 0;
    requires x > 0;
  {
    trap x == 0;  // Provable: x > 0 implies x != 0
    x
  };
}

This verifies because requires x > 0 implies x == 0 is false.

Unprovable Trap

persistent actor {
  public func bad(x : Nat) : async Nat {
    trap x > 0;  // Cannot be proven false - x could be any positive Nat
    x
  };
}

This fails verification. The function accepts any Nat, so x > 0 is not guaranteed to be false.

Optional Message

You can include an error message that describes the error condition:

trap x == 0("x must be non-zero");

The message has type text and appears in the runtime error if the trap executes. The message is not used during verification.

Compared to assert

Aspect	assert P	trap cond
Verification	Proves P is true	Proves cond is false
Runtime	No effect (erased)	Traps if cond is true
Meaning	"P holds here"	"cond is an error state"

Use assert for documentation and proof guidance. Use trap to mark unreachable error states.

Compared to runtime:assert

Aspect	runtime:assert P	trap cond
Verification	Proves P is true	Proves cond is false
Runtime	Traps if P is false	Traps if cond is true
Meaning	"P must hold here"	"cond is an error state"
Semantic equivalent	Proves P	Proves not cond

runtime:assert P and trap (not P) create equivalent proof obligations but opposite runtime checks. Choose based on intent:

• Use runtime:assert when expressing what should be true
• Use trap when expressing what should never happen

Restrictions

Not in Pure Functions

Pure functions cannot contain trap:

// This is rejected:
pure func bad(x : Nat) : Nat {
  trap 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 trap:

// This is rejected:
lemma func bad(x : Nat) {
  trap x == 0;  // Error M0240
};

Not for Prim.trap or Runtime.trap in Pure/Lemma

The restrictions apply equally to Prim.trap() and Runtime.trap():

// All of these are rejected in pure/lemma functions:
pure func bad1() : Nat { trap true; 0 };
pure func bad2() : Nat { Prim.trap("error"); 0 };
pure func bad3() : Nat { Runtime.trap("error"); 0 };

Trap vs Implicit Runtime Traps

The trap keyword differs from implicit runtime traps in Sector9/Motoko operations:

Operation	Runtime Behavior	Verification
trap cond	Traps if cond is true	Proves cond is false
Nat subtraction underflow	Traps if result < 0	Proves result >= 0
Division by zero	Traps if divisor == 0	Proves divisor != 0
Array out of bounds	Traps if index >= size	Proves index < size

The trap keyword is for explicit error conditions. Implicit traps from operations like division or array access are handled separately by the verifier's built-in reasoning. In both cases, verification asks you to prove the dangerous condition cannot happen.

Common Patterns

Unreachable Code in Switch

Mark branches that should never execute:

public func access(opt : ?Data) : async Data
  entry_requires opt != null;
  requires opt != null;
{
  switch opt {
    case (?data) data;
    case null {
      loop { trap true("Unreachable: opt is non-null") };
    };
  }
}

Error Condition Before Risky Operation

Document why an operation is safe:

public func safeDivide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
{
  trap b == 0;  // Mark division-by-zero as impossible
  a / b
}

Asserting Invariant Negation

Use trap to express what should never happen:

persistent actor {
  var supply : Nat = 0;

  invariant supply <= 1000000;

  public func mint(amount : Nat) : async ()
    modifies supply
    entry_requires supply + amount <= 1000000;
    requires supply + amount <= 1000000;
  {
    trap supply + amount > 1000000;  // Overflow is impossible
    supply := supply + amount;
  };
}

When Verification Fails

If verification fails on a trap, check:

1. Missing preconditions - Add a requires clause that rules out the condition
2. Weak invariants - Strengthen the actor invariant to exclude the error state
3. Incorrect trap condition - The condition might actually be possible
4. Missing intermediate steps - Add assert statements to guide the proof

A failing trap means either:

• The error condition is actually reachable (bug in code)
• The specification is incomplete (missing preconditions/invariants)

Summary

• trap condition proves an error condition is unreachable
• Traps at runtime if condition is true (error state reached)
• Must be provable from preconditions, invariants, or program state
• Use for marking impossible branches and error conditions
• Cannot appear in pure functions or lemmas
• Optional message describes the error: trap cond("message")
• Opposite of runtime:assert: trap proves false, runtime:assert proves true

Related Topics

• runtime:assert for positive runtime guards
• Trap behavior in message execution for rollback and commit-point behavior
• Pure function restrictions for why trap, Prim.trap, and Runtime.trap are rejected in spec helpers
• Runtime limitations for checks that remain runtime concerns