Trap Behavior

When execution fails, the Internet Computer rolls back uncommitted state changes and cancels pending outgoing messages from the current uncommitted segment. Understanding trap behavior is essential for writing robust actors.

What Causes a Trap

A trap occurs when:

Cause	Example
Explicit trap statement	trap balance < 0;
Explicit runtime:assert failure	runtime:assert x > 0; when x == 0
Division by zero	100 / 0
Nat subtraction underflow	5 - 10 on Nat type
Array out of bounds	arr[10] when arr.size() == 5
Option unwrap on null	opt! when opt == null
Integer overflow (fixed-width)	Nat8 exceeding 255

The verifier proves modeled trap conditions cannot occur. If verification succeeds without trusted gaps, these traps are unreachable on verified paths; environment failures, resource exhaustion, and trusted-code mistakes remain outside that guarantee.

State Rollback

When a trap occurs, all uncommitted state changes are reverted. The rollback scope depends on where commit points occur.

Before Any Commit Point

If a trap happens before any await, return, or function exit, all state changes are reverted:

trap-rollback-all.sr9

// Trap before any commit point - ALL state changes reverted
persistent actor {
  var balance : Int = 100;
  var transfers : Int = 0;
  invariant balance >= 0;

  public func withdraw(amount : Int) : async Int
    modifies balance, transfers
    entry_requires amount > 0 and amount <= balance;
    requires amount > 0;
    requires amount <= balance;
    ensures result == old(balance) - amount;
  {
    balance -= amount;
    transfers += 1;

    // Guard: negative balance is an error
    trap balance < 0;

    // If trap triggered above:
    // - balance reverts to 100
    // - transfers reverts to 0
    // - Caller sees the error

    balance
  };
}

The caller receives an error, and the actor state is unchanged from before the call.

After a Commit Point

If a trap happens after an await, only changes made after that await are reverted. Changes committed at the await are permanent:

trap-partial-commit.sr9

// Trap after commit point - prior changes survive
persistent actor {
  var phase1Done : Bool = false;
  var phase2Done : Bool = false;

  public func twoPhaseProcess() : async ()
    modifies phase1Done, phase2Done
  {
    // Phase 1
    phase1Done := true;
    try { await checkpoint(); } catch (_) {};  // COMMIT: phase1Done = true is permanent

    // Phase 2
    phase2Done := true;

    // If trap happens here:
    // - phase1Done stays true (committed at await)
    // - phase2Done reverts to false (uncommitted)
    trap false;  // Never actually traps, but shows the principle
  };

  private func checkpoint() : async () { };
}

This creates a partial failure scenario where some work survives.

Message Cancellation

Pending outgoing messages are cancelled when a trap occurs. If your method queues an async call but traps before reaching a commit point, that call never happens:

trap-messages-cancelled.sr9

// Pending messages are cancelled on trap
persistent actor {
  var notified : Bool = false;

  public func riskyOperation(amount : Int) : async ()
    modifies notified
    entry_requires amount > 0 and amount <= 1000;
    requires amount > 0;
    requires amount <= 1000;
  {
    // Construct an outgoing message future. Verified code must either await it
    // with a catch-all or avoid creating fire-and-forget futures.
    try { await sendNotification(); } catch (_) {};

    // If this guard were violated, the call would trap; verified code proves
    // it cannot fire.
    trap amount > 1000;

    notified := true;
  };

  private func sendNotification() : async () { };
}

The notification message is discarded. The target canister never receives it.

Implicit Traps

Many Sector9 operations can trap at runtime. The verifier requires preconditions that prevent these:

trap-implicit.sr9

// Implicit traps from Motoko operations
persistent actor {
  var data : [var Int] = [var 10, 20, 30];

  // Division by zero - implicit trap
  public func safeDivide(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
  {
    a / b  // Would trap if b == 0
  };

  // Nat underflow - implicit trap
  public func safeSubtract(a : Nat, b : Nat) : async Nat
    entry_requires b <= a;
    requires b <= a;
  {
    a - b  // Would trap if b > a
  };

  // Array bounds - implicit trap
  public func safeAccess(i : Nat) : async Int
    reads data
    entry_requires i < data.size();
    requires i < data.size();
  {
    data[i]  // Would trap if i >= size
  };
}

Without the requires clauses, these operations would be unsafe. The verifier proves the preconditions guarantee safety.

Operations That Can Trap

Operation	Trap Condition	Required Guard
a / b	b == 0	requires b != 0
a % b	b == 0	requires b != 0
a - b (Nat)	b > a	requires b <= a
arr[i]	i >= arr.size()	requires i < arr.size()
opt!	opt == null	requires opt != null
Nat8 overflow	value > 255	bounds check

Atomic Failure Model

The IC guarantees atomic failure: either all changes in an atomic unit commit, or none do. An atomic unit spans from method entry (or the previous await) to the next commit point.

Method entry
  │
  ├── State change A (tentative)
  ├── State change B (tentative)
  │
  └── COMMIT POINT (await/return)
        │
        ├── A and B are now permanent
        ├── State change C (tentative)
        │
        └── TRAP HERE
              │
              └── Only C reverts, A and B survive

This model ensures you can reason about partial progress in multi-step operations.

Verification vs Runtime

The verifier and runtime handle traps differently:

Aspect	Verification	Runtime
trap cond	Proves cond is false	Traps if cond is true
runtime:assert P	Proves P is true	Traps if P is false
Implicit traps	Proves impossible	Aborts execution
State rollback	Reasoned about through commit-point obligations	Happens automatically

The verifier turns explicit traps and runtime assertions into proof obligations. If a trap still occurs because of trusted code, external failures, resource exhaustion, or a bug outside the modeled surface, the IC handles rollback automatically.

Error Codes

When a trap reaches the IC boundary, the caller sees error code IC0503:

IC0503: Error from Canister ...: Canister called `ic0.trap` with message: '...'

The message comes from explicit traps like trap cond("message"). Implicit traps (division, bounds) have system-generated messages.

Designing for Failure

Validate Before Commit

Check conditions before reaching a commit point:

public func safeTransfer(to : Principal, amount : Nat) : async Bool
  modifies balance
{
  // Validate first - no state changes yet
  if (amount > balance) {
    return false;  // No changes committed
  };

  balance -= amount;
  try {
    await sendTo(to, amount);  // Commit point
    true
  } catch (_) {
    false
  }
}

Use Staged Commits

For multi-step operations, commit intermediate progress:

public func process() : async ()
  modifies step1, step2, step3
{
  step1 := doStep1();
  try { await checkpoint(); } catch (_) { return };  // step1 survives any later trap

  step2 := doStep2();
  try { await checkpoint(); } catch (_) { return };  // step2 survives any later trap

  step3 := doStep3();  // step3 commits at return
}

Guard Risky Operations

Use preconditions to prevent traps:

public func divide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0  // Caller must guarantee this
{
  a / b  // Safe: precondition rules out b == 0
}

Traps and Invariants

Actor invariants must hold at commit points. A trap does not violate invariants because:

1. If trap is before any commit point, all changes revert (invariant preserved)
2. If trap is after a commit point, that commit already verified the invariant

The verifier ensures invariants hold at every reachable commit point.

Limitations

Sector9 models the logical properties of traps but does not verify:

• Trap recovery - How callers handle errors
• Message ordering - Which pending messages are cancelled
• Resource exhaustion - Cycle depletion, memory limits
• External traps - Failures in inter-canister calls beyond the local catch/fallback path

These are runtime concerns handled by the IC execution environment.

Summary

• Traps abort execution and roll back uncommitted state changes
• State changes before an await are committed; after, they are tentative
• Pending outgoing messages are cancelled on trap
• The verifier proves traps are unreachable
• Design methods to validate before committing
• Actor invariants are preserved through atomic rollback

See Also

• Commit Points - When state becomes permanent
• Atomicity Between Awaits - No interleaving within atomic blocks
• Trap Conditions (trap) - The trap statement syntax
• At-Most-Once Delivery - Message delivery guarantees