Inductive Reasoning

Loop verification uses the same technique as mathematical induction: prove a base case, prove the inductive step, and conclude the property holds for all iterations.

The Three Phases

The verifier checks every loop invariant in three phases:

Phase	What the Verifier Checks	Mathematical Analogy
Initialization	The invariant holds before the loop starts	Base case: P(0) is true
Preservation	If the invariant holds and the condition is true, the body preserves it	Inductive step: P(k) implies P(k+1)
Conclusion	The invariant plus negated condition implies the postcondition	Conclusion: P(n) is true for all n

Understanding these phases helps you write correct invariants and debug verification failures. The same model applies whether the invariant mentions local variables, actor fields with old(), or pure specification helpers.

Phase 1: Initialization

Before the loop executes, the invariant must already be true. The verifier inserts an assertion at the loop entry point.

Consider a countdown loop:

var i : Nat = n;
while (i > 0) {
  loop:invariant i <= n;
  i -= 1;
};

Initialization check: When i = n, is i <= n true? Yes, because n <= n.

If initialization fails, the invariant does not hold before the first iteration:

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

The invariant i <= 5 is false when i = 10, so the base case fails.

Phase 2: Preservation

The preservation check is the core of inductive reasoning. The verifier must prove:

If the invariant holds at the start of an iteration and the loop condition is true, then the invariant still holds after executing the loop body.

For the countdown example:

while (i > 0) {
  loop:invariant i <= n;
  i -= 1;
};

Preservation reasoning:

• Assume: i <= n (invariant holds) and i > 0 (condition true)
• After body: i becomes i - 1
• Prove: i - 1 <= n
• Since i <= n, and i - 1 < i, we have i - 1 <= n

The invariant is preserved by the loop body.

When Preservation Fails

The loop body must not break the invariant:

var i : Nat = 0;
while (i < n) {
  loop:invariant i < 5;  // FAILS when i reaches 5
  i += 1;
};

When n >= 5:

• Assume: i < 5 and i < n
• After body: i becomes i + 1
• When i = 4, after increment i = 5
• Prove: 5 < 5? No.

The invariant is not preserved because incrementing i can make i >= 5.

Phase 3: Conclusion

When the loop exits, two facts are known:

1. The invariant holds (it was preserved through all iterations)
2. The loop condition is false

The verifier uses both facts to prove the postcondition.

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

Conclusion reasoning:

• After loop: i <= n (invariant) and not (i > 0) (condition false)
• not (i > 0) means i <= 0
• Since i : Nat, we have i >= 0
• Combined: i == 0
• Therefore result == 0

The postcondition follows from the invariant plus the negated condition.

A Complete Inductive Proof

Trace through all three phases for a sum computation:

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;
    loop:invariant 2 * acc == i * (i + 1);
    acc += i + 1;
    i += 1;
  };

  acc
};

Initialization

Before the loop:

• i = 0, acc = 0
• Check i <= n: 0 <= n is true for any Nat n
• Check 2 * acc == i * (i + 1): 2 * 0 == 0 * 1 is 0 == 0, true

Both invariants hold initially.

Preservation

Assume invariants hold and i < n:

• i <= n and 2 * acc == i * (i + 1) and i < n

After body:

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

Check first invariant with new values:

• (i + 1) <= n? Since i < n, we have i + 1 <= n. Preserved.

Check second invariant with new values:

• 2 * (acc + i + 1) == (i + 1) * (i + 2)?
• Left side: 2 * acc + 2 * (i + 1)
• Using 2 * acc == i * (i + 1): i * (i + 1) + 2 * (i + 1)
• Factor: (i + 1) * (i + 2)
• Right side: (i + 1) * (i + 2). Equal. Preserved.

Conclusion

After loop:

• i <= n and 2 * acc == i * (i + 1) and not (i < n)
• not (i < n) means i >= n
• Combined with i <= n: i == n
• Substituting: 2 * acc == n * (n + 1)
• Since result = acc: 2 * result == n * (n + 1)

The postcondition is exactly what we needed.

The Invariant Must Be Inductive

An invariant is inductive if the loop body preserves it. Non-inductive invariants fail verification even if they describe a true property:

public func example(n : Nat) : async Nat
  ensures result <= n;
{
  var i : Nat = n;
  while (i > 0) {
    loop:invariant i >= 0;  // True, but too weak
    i -= 1;
  };
  i
};

The invariant i >= 0 follows from the Nat type and is inductive, but it is too weak to prove result <= n. You need loop:invariant i <= n to connect the final value to n.

Strengthening Invariants

When verification fails, the invariant is often too weak. Strengthen it by adding more facts:

If This Fails	Add This
Postcondition not provable	An invariant that connects loop state to the postcondition
Missing bounds	i >= 0 and i <= n for loop counters
Missing relationship	An equation relating accumulator to counter

Example: Weak to Strong

This fails:

public func sumArray(arr : [Nat]) : async Nat
  ensures result >= 0;
{
  var sum : Nat = 0;
  var i : Nat = 0;
  while (i < arr.size()) {
    loop:invariant i <= arr.size();  // Missing sum invariant
    sum += arr[i];
    i += 1;
  };
  sum
};

The invariant tracks i but says nothing about sum. Add:

while (i < arr.size()) {
  loop:invariant i <= arr.size();
  loop:invariant sum >= 0;  // Now the postcondition is provable
  sum += arr[i];
  i += 1;
};

Two Invariants Are Often Needed

Most loops need two kinds of invariants:

1. Bounds invariant: Tracks the loop counter's valid range
2. Property invariant: Relates computed values to the loop counter

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

The bounds invariant establishes that the loop progresses correctly. The property invariant captures what has been computed so far.

Relating Actor Fields with old()

When a loop modifies actor fields, use old() to relate current values to entry values:

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 says: after i iterations, counter has increased by exactly i from its entry value.

Conclusion:

• At exit: i == n
• Substituting: counter == old(counter) + n

This matches the postcondition.

Debugging Inductive Failures

When verification fails, identify which phase failed. A targeted assert before or after the loop body is often the fastest way to tell whether the problem is initialization, preservation, or the final connection to the postcondition.

Initialization Failure

Error points to the loop header. The invariant is false before the loop starts.

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

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

Preservation Failure

Error points to the loop body. The invariant does not survive one iteration.

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

while (i < n) {
  loop:invariant i < 5;  // Fails when body increments i past 5
  i += 1;
};

Postcondition Failure

Error points to the ensures clause. The invariant is too weak to prove the postcondition.

Fix: Add an invariant that directly relates to the postcondition.

Summary

• Inductive reasoning proves loops correct through three phases: initialization, preservation, conclusion
• Initialization: The invariant must be true before the loop starts
• Preservation: If the invariant holds and the condition is true, the body must maintain it
• Conclusion: The invariant plus negated condition must imply the postcondition
• An invariant is inductive if the loop body preserves it
• Most loops need both a bounds invariant and a property invariant
• Use old() to relate modified fields to their entry values
• When debugging, identify which of the three phases failed

Related Topics

• Loop annotations for syntax and allowed expressions
• Finding loop invariants for deriving candidates from postconditions
• assert for isolating failed proof phases
• old() patterns for cumulative field updates
• Footprints for the actor fields a loop body is allowed to change