Skip to main content

Finding Loop Invariants

A systematic approach to discovering the invariants your loop needs.

The Two-Invariant Pattern​

Most loops require two kinds of invariants:

  1. Bounds invariant: Constrains the loop counter to its valid range
  2. Property invariant: Relates computed values to the loop counter

Start by identifying both.

while (i < n) {
  loop:invariant i >= 0 and i <= n;      // Bounds
  loop:invariant acc == f(i);            // Property: acc is some function of i
  // body
};

The bounds invariant tracks loop progress. The property invariant captures what has been computed so far.

Step 1: Identify the Postcondition​

The invariant must be strong enough to prove the postcondition when the loop exits. Work backwards from what you need to prove.

Example: Prove the sum of 1 to n equals n*(n+1)/2.

public func sumTo(n : Nat) : async Nat
  ensures 2 * result == n * (n + 1);

The postcondition mentions result and n. At loop exit, you need enough information to prove this relationship.

Step 2: Parameterize the Postcondition​

Replace constants with the loop counter to form a candidate invariant.

The postcondition is:

2 * result == n * (n + 1)

Replace n with the loop counter i and result with the accumulator acc:

2 * acc == i * (i + 1)

This is your property invariant.

Step 3: Add Bounds​

Every loop counter needs bounds. For a loop counting up to n:

loop:invariant i >= 0 and i <= n;

For counting down from n:

loop:invariant i >= 0 and i <= n;

Nat variables automatically satisfy >= 0; include the lower bound only when it helps the proof read clearly or when the counter is signed.

Step 4: Verify Initialization​

Check that your invariants hold before the loop starts. Trace through the initial values:

var i : Nat = 0;
var acc : Nat = 0;

while (i < n) {
  loop:invariant i <= n;                    // 0 <= n? Yes
  loop:invariant 2 * acc == i * (i + 1);    // 2*0 == 0*1? Yes
  acc += i + 1;
  i += 1;
};

Both invariants hold when i = 0 and acc = 0.

Step 5: Verify Preservation​

Check that one iteration preserves the invariant. Assume the invariant holds, execute the body symbolically, and check the invariant with new values.

Before iteration: 2 * acc == i * (i + 1) and i < n

After body:

  • acc becomes acc + (i + 1)
  • i becomes i + 1

Check: Does 2 * (acc + i + 1) == (i + 1) * (i + 2)?

Expand:

  • Left: 2*acc + 2*(i+1)
  • Substitute 2*acc = i*(i+1): i*(i+1) + 2*(i+1) = (i+1)*(i+2)
  • Right: (i+1)*(i+2)

Equal. The invariant is preserved.

Common Invariant Patterns​

Pattern: Accumulator Sum​

When computing a sum, relate the accumulator to partial sums:

public func sum(arr : [Nat]) : async Nat
  ensures result == arraySum(arr, arr.size());
{
  var total : Nat = 0;
  var i : Nat = 0;

  while (i < arr.size()) {
    loop:invariant i <= arr.size();
    loop:invariant total == arraySum(arr, i);
    total += arr[i];
    i += 1;
  };

  total
};

The invariant total == arraySum(arr, i) says: after processing i elements, total is the sum of those elements.

Pattern: Countdown​

When counting down, track progress from the starting value:

public func countdown(n : Nat) : async Nat
  ensures result == 0;
{
  var i : Nat = n;
  while (i > 0) {
    loop:invariant i <= n;
    i -= 1;
  };
  i
};

At exit: i <= n and not (i > 0). For Nat, this means i == 0.

Pattern: Field Modification with old()​

When a loop modifies actor fields, use old() to track cumulative changes:

persistent actor {
  var counter : Int = 0;

  public func addN(n : Int) : async ()
    modifies counter
    entry_requires n >= 0;
    requires n >= 0;
    ensures counter == old(counter) + n;
  {
    var i = 0;
    while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant counter == old(counter) + i;
      counter += 1;
      i += 1;
    };
  };
}

The invariant counter == old(counter) + i expresses: after i iterations, counter has increased by i from its entry value.

Pattern: Conservation​

When values move between variables but the total is preserved:

loop:invariant a + b == old(a) + old(b);

Or for fields:

loop:invariant available + locked == total;

Pattern: Nested Loops​

For nested loops, the inner invariant must account for outer loop state:

while (r < rows) {
  loop:invariant r <= rows;
  loop:invariant total == r * cols;

  var c : Nat = 0;
  while (c < cols) {
    loop:invariant c <= cols;
    loop:invariant total == r * cols + c;  // Includes outer progress
    total += 1;
    c += 1;
  };

  r += 1;
};

The inner invariant total == r * cols + c includes both the completed rows (r * cols) and the current column progress (c).

Debugging Failed Invariants​

Initialization Failure​

Symptom: Error points to the loop header.

Cause: The invariant is false before the loop starts.

Fix: Check the initial values of all variables in the invariant.

var i : Nat = 10;
while (i < n) {
  loop:invariant i <= 5;  // FAILS: 10 is not <= 5
  i += 1;
};

Preservation Failure​

Symptom: Error points to the loop body.

Cause: The loop body breaks the invariant.

Fix: Trace one iteration manually. What values does the body produce?

while (i < n) {
  loop:invariant i < 5;  // FAILS when i reaches 4 and increments to 5
  i += 1;
};

The invariant i < 5 is not preserved when i = 4 because after increment i = 5.

Postcondition Failure​

Symptom: Error points to the ensures clause.

Cause: The invariant is too weak to imply the postcondition.

Fix: Add an invariant that directly relates to what you need to prove.

public func sumTo(n : Nat) : async Nat
  ensures 2 * result == n * (n + 1);
{
  var i : Nat = 0;
  var acc : Nat = 0;
  while (i < n) {
    loop:invariant i <= n;  // Too weak! No mention of acc
    acc += i + 1;
    i += 1;
  };
  acc
};

Add the property invariant: loop:invariant 2 * acc == i * (i + 1);

Strengthening Checklist​

When verification fails, check these in order:

If This FailsAdd This
Postcondition not provableAn invariant that connects loop state to the postcondition
Missing boundsi >= 0 and i <= n for loop counters
Missing relationshipAn equation relating accumulator to counter
Actor field changesfield == old(field) + delta
Values preservedx == old(x) for unchanged variables

Using Pure Functions​

Complex invariants benefit from pure helper functions. Keep these helpers expression-oriented: pure functions cannot mutate local variables or run imperative loops. For recursive or loop-like specifications, use a trusted pure helper with a contract, a lemma, or a spec collection model.

module {
  pure func tri2(n : Nat) : Nat { n * (n + 1) };

  public func sumTo(n : Nat) : Nat
    ensures 2 * result == tri2(n);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant 2 * acc == tri2(i);
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

The named function tri2(i) is clearer than i * (i + 1) repeated everywhere, and avoiding division keeps the arithmetic proof simpler.

Algorithm Examples​

Multiplication by Repeated Addition​

public func mul(a : Nat, b : Nat) : async Nat
  ensures result == a * b;
{
  var i : Nat = 0;
  var acc : Nat = 0;

  while (i < b) {
    loop:invariant i <= b;
    loop:invariant acc == a * i;
    acc += a;
    i += 1;
  };

  acc
};

Discovery process:

  1. Postcondition: result == a * b
  2. Parameterize with loop counter: acc == a * i
  3. At exit: i == b, so acc == a * b

Division by Repeated Subtraction​

public func div(n : Nat, d : Nat) : async (Nat, Nat)
  entry_requires d > 0;
  requires d > 0;
  ensures result.0 * d + result.1 == n;
  ensures result.1 < d;
{
  var q : Nat = 0;
  var r : Nat = n;

  while (r >= d) {
    loop:invariant q * d + r == n;
    loop:invariant r >= 0;
    r -= d;
    q += 1;
  };

  (q, r)
};

Discovery process:

  1. Postcondition: q * d + r == n
  2. This is exactly the invariant needed
  3. At exit: r < d (loop condition false), satisfying second postcondition

Summary​

  • Most loops need two invariants: bounds and property
  • Work backwards from the postcondition to discover the property invariant
  • Parameterize the postcondition by replacing final values with loop state
  • Verify initialization: invariants must hold before the loop starts
  • Verify preservation: trace one iteration to check the body maintains invariants
  • Use old() to track cumulative changes to actor fields
  • Debug by identifying which phase fails: initialization, preservation, or conclusion
  • Pure functions make complex invariants more readable