Adding Intermediate Assertions

Breaking complex proofs into smaller, provable steps.

When the verifier fails on a postcondition or invariant, the error often points to the final specification without revealing which intermediate step broke. Intermediate assert statements act as proof checkpoints that help you isolate exactly where verification fails.

The Problem

Consider a function with a complex postcondition:

public func processTransaction(deposit : Int, withdraw : Int) : async Int
  modifies balance, deposits, withdrawals
  ensures result == old(balance) + deposit - withdraw;
{
  deposits := deposits + deposit;
  withdrawals := withdrawals + withdraw;
  balance := balance + deposit - withdraw;
  balance
}

If verification fails with "Postcondition might not hold," you know the end result is wrong but not which step caused the problem. Was it the deposits update? The withdrawals? The balance calculation?

The Solution: Proof Checkpoints

Insert assert statements at key points to create verification checkpoints:

assert-checkpoint-basic.sr9

// Intermediate assertions as proof checkpoints
persistent actor {
  var balance : Int = 0;
  var deposits : Int = 0;
  var withdrawals : Int = 0;
  invariant balance == deposits - withdrawals;

  public func processTransaction(deposit : Int, withdraw : Int) : async Int
    modifies balance, deposits, withdrawals
    entry_requires deposit >= 0 and withdraw >= 0 and withdraw <= balance + deposit;
    requires deposit >= 0;
    requires withdraw >= 0;
    requires withdraw <= balance + deposit;
    ensures result == old(balance) + deposit - withdraw;
  {
    // Checkpoint 1: verify preconditions hold
    assert deposit >= 0;
    assert withdraw >= 0;

    deposits := deposits + deposit;

    // Checkpoint 2: partial state is consistent
    assert balance == deposits - deposit - withdrawals;

    withdrawals := withdrawals + withdraw;

    // Checkpoint 3: final state satisfies invariant
    assert balance == deposits - withdrawals - deposit + withdraw;

    balance := balance + deposit - withdraw;

    // Checkpoint 4: postcondition will hold
    assert balance == old(balance) + deposit - withdraw;

    balance
  };
}

Each assertion gives the verifier an intermediate goal. When verification fails, the error now points to the specific checkpoint that cannot be proven, narrowing your search.

When to Add Intermediate Assertions

Add assertions when you encounter:

1. Postcondition failures - Insert assertions before the return to verify each component of the postcondition
2. Invariant failures - Add assertions after each state mutation to track when the invariant breaks
3. Precondition failures at call sites - Assert the callee's preconditions before the call
4. Loop failures - Add assertions inside loops to verify the invariant holds after each step
5. Complex arithmetic - Break down multi-step calculations with assertions after each operation

Technique 1: Narrowing Failure Location

When a postcondition fails, work backwards by asserting each part of the result:

assert-narrow-failure_unsat.sr9

// Using assertions to narrow down verification failures
persistent actor {
  var x : Int = 0;
  var y : Int = 0;

  private func compute(a : Int, b : Int) : Int
    requires b != 0;
    ensures result == a / b + a % b;
  {
    // Without assertions, a failing ensures is hard to debug.
    // Add assertions to isolate which part fails.

    let quotient = a / b;
    assert quotient * b <= a;  // Checkpoint: division property

    let remainder = a % b;
    assert remainder >= 0 or remainder <= 0;  // Checkpoint: remainder exists
    assert a == quotient * b + remainder;  // Checkpoint: division identity

    quotient + remainder
  };

  public func test() : async Int modifies x, y {
    x := 10;
    y := 3;
    compute(x, y)
  };
}

Run verification after adding each assertion. The first assertion that fails reveals the problematic step.

Technique 2: Debugging Loops

Loop invariants are common failure points. Add assertions inside the loop body to verify the invariant is maintained after each iteration:

assert-loop-debug.sr9

// Using assertions to debug loop verification
persistent actor {
  var total : Int = 0;

  public func sumToN(n : Int) : async Int
    modifies total
    entry_requires n >= 0;
    requires n >= 0;
    ensures result == n * (n + 1) / 2;
  {
    var i = 0;
    var sum = 0;

    while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant sum == i * (i + 1) / 2;

      i := i + 1;
      sum := sum + i;

      // Debug assertion: verify invariant holds after each iteration
      assert sum == i * (i + 1) / 2;
    };

    // Debug assertion: verify loop achieved its goal
    assert i == n;
    assert sum == n * (n + 1) / 2;

    sum
  };
}

If the in-loop assertion fails, the loop body violates the invariant. If only the post-loop assertion fails, the invariant may be too weak to imply the postcondition.

Technique 3: Verifying Call Site Preconditions

When a precondition failure occurs at a call site, assert the callee's preconditions explicitly before the call:

assert-call-chain.sr9

// Using assertions to verify preconditions at call sites
persistent actor {
  var counter : Nat = 0;

  private func increment(amount : Nat) : ()
    modifies counter
    requires amount > 0;
    requires counter + amount <= 1000;
    ensures counter == old(counter) + amount;
  {
    counter := counter + amount;
  };

  public func safeIncrement(n : Nat) : async Nat
    modifies counter
    entry_requires n > 0;
    entry_requires n <= 100;
    requires n > 0;
    requires n <= 100;
    ensures result == old(counter) + n;
  {
    // Before calling increment, assert its preconditions
    assert n > 0;  // Matches requires amount > 0
    assert counter + n <= 1000;  // Matches requires counter + amount <= 1000

    increment(n);

    // After call, assert the postcondition we depend on
    assert counter == old(counter) + n;

    counter
  };
}

If the assertion before the call fails, your caller does not establish the precondition. If it succeeds but the call still fails, check that your assertion matches the callee's actual requires clause.

Technique 4: Debugging Frame Conditions

Frame failures are subtle: a field changes when it should not, or is assumed unchanged when it might change. Use assertions to verify frame conditions explicitly:

assert-frame-debug.sr9

// Using assertions to debug framing issues
persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  var c : Int = 100;

  private func modifyAB() : ()
    modifies a, b
    ensures a == old(a) + 1;
    ensures b == old(b) + 1;
  {
    a := a + 1;
    b := b + 1;
  };

  public func testFraming() : async Int
    reads c
    modifies a, b
    ensures c == 100;  // c should be unchanged
    ensures result == old(a) + old(b) + 2;
  {
    // Snapshot values before call
    let a0 = a;
    let b0 = b;
    let c0 = c;

    modifyAB();

    // Assert frame condition: c was not modified
    assert c == c0;
    assert c == 100;

    // Assert postconditions of the call
    assert a == a0 + 1;
    assert b == b0 + 1;

    // Assert the final result
    assert a + b == a0 + b0 + 2;

    a + b
  };
}

Capture values before a call, then assert they are unchanged after. This reveals whether the verifier lacks information about what the call modifies.

Technique 5: Bounds and Index Verification

For array access and arithmetic bounds, assert that indices and values are within expected ranges at each step:

assert-binary-search.sr9

// Debugging bounds in a search loop with intermediate assertions
persistent actor {
  public func find(arr : [Int], target : Int) : async ?Nat
    ensures switch (result) { case null true; case (?i) i < arr.size() };
  {
    var i : Nat = 0;
    var found : ?Nat = null;

    while (i < arr.size()) {
      loop:invariant i <= arr.size();
      loop:invariant switch (found) { case null true; case (?j) j < arr.size() };

      // Debug assertions: the next array access is in bounds.
      assert i < arr.size();
      let value = arr[i];

      if (value == target) {
        found := ?i;
        assert switch (found) { case null false; case (?j) j < arr.size() };
        i := arr.size();
      } else {
        i := i + 1;
        assert i <= arr.size();
      };
    };

    assert switch (found) { case null true; case (?j) j < arr.size() };
    found
  };
}

Assertions on the loop index and result option reveal exactly which bound is violated when array access fails.

Systematic Debugging Workflow

1. Start with the failing obligation - Note whether it's a postcondition, precondition, invariant, or assertion failure

2. Identify the relevant code section - For postconditions, focus on the function body. For preconditions, focus on the call site

3. Add assertions at boundaries:

   • Before and after function calls
   • At loop entry and exit
   • After each state mutation

4. Binary search for the failure - If many assertions pass, remove half and check again. Narrow down to the exact failing step

5. Once found, strengthen the proof - Add preconditions, strengthen invariants, or fix the implementation

Assertions vs Other Debugging Tools

Tool	Use When
assert	Breaking down proofs, verifying intermediate state
--counterexample	Understanding concrete failing values
Strengthening requires	Ruling out impossible inputs
Strengthening loop:invariant	Loop body proofs fail

Assertions complement --counterexample. A counterexample tells you what values cause failure; assertions tell you where in the code the failure occurs.

Common Assertion Patterns

Assert Postcondition Components

public func combine(a : Int, b : Int) : async Int
  ensures result == a + b + 1;
{
  let sum = a + b;
  assert sum == a + b;  // Checkpoint: sum computed correctly
  let result = sum + 1;
  assert result == a + b + 1;  // Checkpoint: postcondition holds
  result
}

Assert Invariant After Each Mutation

public func transfer(amount : Int) : async ()
  modifies balance, pending
{
  balance := balance - amount;
  assert balance + pending == old(balance) + old(pending) - amount;

  pending := pending + amount;
  assert balance + pending == old(balance) + old(pending);  // Conservation
}

Assert Call Results

let value = helper(x);
assert value >= 0;  // Verify helper's postcondition
assert value <= 100;  // Verify expected bounds

Assert Loop Progress

while (i < n) {
  loop:invariant i <= n;
  let old_i = i;
  i := i + 1;
  assert i == old_i + 1;  // Progress was made
  assert i <= n + 1;  // Within expected range
}

When to Remove Assertions

After debugging, consider which assertions to keep:

• Keep assertions that document non-obvious invariants
• Keep assertions that help the verifier with complex proofs
• Remove assertions that duplicate obvious facts (e.g., assert x >= 0 for a Nat)
• Remove assertions added purely for debugging once the issue is fixed

Static assertions are verification-only, so they do not add deployed runtime checks. However, too many assertions can clutter code and slow verification.

Summary

• Intermediate assertions create proof checkpoints that isolate verification failures
• Add assertions before/after calls, inside loops, and after state mutations
• Use binary search to narrow down the failing step
• Assertions complement counterexamples: counterexamples show failing values, assertions show failing locations
• Keep assertions that document important properties; remove pure debugging artifacts
• Static assert is verification-only; use runtime:assert for deployed runtime checks