Runtime Traps

System-level failures like out-of-memory (OOM), garbage collection failures, inter-canister errors, and stable memory issues are outside the verification model. This page explains what Sector9 does and does not verify about runtime failures.

What Sector9 Verifies

Sector9 verifies explicit runtime checks and trap conditions:

Statement	Verification	Runtime
assert P	Proves P is true	No effect (erased)
runtime:assert P	Proves P is true	Traps if P is false
trap cond	Proves cond is false	Traps if cond is true
Prim.trap("msg")	Proves call is unreachable	Traps unconditionally

These are all proof obligations - the verifier proves the condition holds at that program point.

What Sector9 Does Not Verify

Sector9 does not model or verify system-level runtime failures:

Failure Type	Description	Verification
OOM	Out-of-memory on heap allocation	Not modeled
GC failures	Garbage collection issues	Not modeled
RTS failures	Runtime system errors	Not modeled
Inter-canister errors	Cross-canister call failures	Not modeled
Stable memory failures	Stable memory read/write errors	Not modeled
Cycle exhaustion	Running out of computational cycles	Not modeled

These failures are assumed not to occur. The verification model treats memory allocation, system calls, and infrastructure as reliable.

Implicit vs Explicit Traps

Explicit Traps (Verified)

Explicit trap conditions are proof obligations. The verifier proves they cannot occur:

runtime-trap-explicit.sr9

// Explicit trap with precondition
persistent actor {
  public func requirePositive(x : Nat) : async Nat
    entry_requires x > 0;
    requires x > 0;
  {
    trap x == 0;  // Proven unreachable by precondition
    100 / x
  };
}

The trap x == 0 generates a proof obligation: prove x == 0 is false. The precondition requires x > 0 provides this proof.

Implicit Traps (Require Guards)

Built-in operations that can trap at runtime are not automatically verified. You must guard them with explicit preconditions:

Operation	Runtime Trap Condition	Required Guard
Division a / b	b == 0	requires b != 0
Modulo a % b	b == 0	requires b != 0
Array access arr[i]	i >= arr.size()	requires i < arr.size()
Nat subtraction a - b	a < b	requires a >= b
Fixed-width overflow	Value out of range	requires bounds check

Without explicit guards, the verifier rejects the program or verification fails.

Division and Modulo

Division by zero is a common runtime trap. You must guard divisors:

Guarded (Verifies)

runtime-division-guarded.sr9

// Division with explicit precondition guard
module {
  public func divide(a : Int, b : Int) : Int
    requires b != 0;
    ensures result == a / b;
  {
    a / b
  };
}

Unguarded (Fails)

runtime-division-unguarded_unsat.sr9

// Division without precondition - verification fails
module {
  public func divide(a : Int, b : Int) : Int
    ensures result == a / b;
  {
    a / b  // ERROR: divisor could be zero
  };
}

The guarded version requires b != 0 at the contract level. The unguarded version fails translation to the Viper lane because the divisor could be zero.

Array Bounds

Array access requires bounds checking via preconditions:

runtime-array-bounds.sr9

// Array access with bounds precondition
persistent actor {
  var data : [var Nat] = [var 1, 2, 3];

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

The precondition requires i < data.size() ensures the index is valid. Without this guard, verification fails with a permission error.

Nat Subtraction Underflow

Natural number subtraction traps if the result would be negative:

runtime-nat-underflow.sr9

// Nat subtraction requires non-negative result
persistent actor {
  var balance : Nat = 100;

  public func withdraw(amount : Nat) : async Nat
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
    ensures result == old(balance) - amount;
  {
    let prev = balance;
    balance := balance - amount;  // Safe: precondition guards underflow
    prev - amount
  };
}

The precondition requires amount <= balance ensures the subtraction is safe.

Defense-in-Depth Pattern

For critical operations, combine contract-level guards with runtime checks:

runtime-defense-in-depth.sr9

// Defense-in-depth: contract + runtime check
persistent actor {
  public func safeDiv(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
    ensures result == a / b;
  {
    runtime:assert b != 0;  // Backup for contract violations
    a / b
  };
}

The requires clause is the logical guard that callers must prove. For public actor methods, mirror caller-controlled obligations with entry_requires so the exported runtime entry point enforces them too. runtime:assert provides a local backup that traps if the condition is somehow violated, for example through trusted code or during testing.

Trap Semantics on the IC

On the Internet Computer, traps have specific message semantics:

• Atomic failure: Before any await, a trap rolls back all state changes
• Commit points: After an await, prior state changes are committed and cannot be rolled back
• Message revocation: Pending outgoing messages are cancelled on trap

Sector9 models the atomicity guarantee but does not verify trap recovery or message handling.

Verification Boundaries

The key distinction is between what the verifier proves and what the runtime handles:

Verifier Domain (Proof Obligations)          Runtime Domain (Trusted)
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━    ━━━━━━━━━━━━━━━━━━━━━━━━━━━
✓ trap / runtime:assert / Prim.trap         ✗ OOM / heap allocation
✓ assert (proof-only, no runtime cost)      ✗ GC failures
✓ Division guards via requires              ✗ RTS / system failures
✓ Array bounds guards via requires          ✗ Inter-canister errors
✓ Nat underflow guards via requires         ✗ Stable memory failures
✓ Overflow checks (in checked mode)         ✗ Cycle exhaustion

Practical Guidance

Situation	Recommendation
Division in public method body	Add entry_requires divisor != 0 and requires divisor != 0
Array indexing	Add entry_requires i < arr.size() and requires i < arr.size() when caller-controlled
Nat subtraction	Add entry_requires a >= b and requires a >= b when caller-controlled
Critical operations	Use defense-in-depth with both requires and runtime:assert
System failures	Handle through runtime error handling, not verification

Why This Boundary Exists

The verification model focuses on algebraic reasoning - proving properties about values, control flow, and state. System-level failures depend on:

• Memory availability (unpredictable)
• Runtime system implementation (not formally specified)
• Inter-canister messaging (external system)
• IC infrastructure (trusted platform)

These are outside the scope of what SMT-based verification can reason about. The boundary is deliberate: Sector9 verifies what it can prove, and trusts the runtime for everything else.

Summary

• System failures (OOM, GC, RTS, inter-canister) are outside the verification model
• Explicit traps (trap, runtime:assert, Prim.trap) are verified as proof obligations
• Implicit traps (division, bounds, underflow) require explicit precondition guards
• Use defense-in-depth for critical operations: combine requires with runtime:assert
• The verification boundary is between algebraic reasoning (verifier) and system reliability (runtime)