Loop Invariant Discovery

Systematic approach to finding the right invariant when verification fails.

Loop invariants are the most challenging part of verification for many developers. When the verifier reports "Loop invariant might not be preserved" or "Postcondition might not hold," you need a systematic approach to discover or strengthen the invariant. This guide provides practical techniques for finding invariants that work.

The Two-Invariant Pattern

Most loops require two types of invariants working together:

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

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

Missing either causes verification to fail. Bounds alone cannot prove properties about computed values. Properties alone may not be verifiable without knowing the counter's range.

The Five-Step Discovery Process

When you need to find a loop invariant, follow these steps systematically.

Step 1: Identify the Postcondition

Start from what you need to prove. The postcondition is your target:

ensures result == n * (n + 1) / 2;

Step 2: Parameterize the Postcondition

Replace the final value (n) with the loop counter (i). This gives you the property invariant:

// Postcondition: result == n * (n + 1) / 2
// Property invariant: acc == i * (i + 1) / 2

The invariant says "after processing i iterations, acc holds the partial result."

Step 3: Add Bounds

Every loop counter needs bounds. The standard pattern is:

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

The lower bound comes from initialization. The upper bound comes from the loop condition.

Step 4: Verify Initialization

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

Initial: i = 0, acc = 0
Bounds: 0 >= 0 and 0 <= n? Yes (n >= 0 from requires)
Property: 0 == 0 * 1 / 2? Yes

If initialization fails, your invariant does not match the initial state.

Step 5: Verify Preservation

Execute one iteration symbolically. Assume the invariant holds at the start, then check it holds after the body:

Assume: acc == i * (i + 1) / 2, i < n
Body: i := i + 1; acc := acc + i;
After: acc' = acc + (i + 1), i' = i + 1

Check: acc' == i' * (i' + 1) / 2
Expand: acc + (i + 1) == (i + 1) * (i + 2) / 2
Substitute: i * (i + 1) / 2 + (i + 1) == (i + 1) * (i + 2) / 2
Factor: (i + 1) * (i / 2 + 1) == (i + 1) * (i + 2) / 2
Simplify: (i + 1) * (i + 2) / 2 == (i + 1) * (i + 2) / 2 Yes

invariant-discovery-steps.sr9

// Step-by-step invariant discovery
persistent actor {
  // Goal: Compute n * (n + 1) / 2 by repeated addition

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

    // Step 1: Start with postcondition
    //   ensures result == n * (n + 1) / 2
    //
    // Step 2: Replace n with loop counter i
    //   property: acc == i * (i + 1) / 2
    //
    // Step 3: Add bounds for the counter
    //   bounds: i >= 0 and i <= n
    //
    // Step 4: Verify initialization (i=0, acc=0)
    //   0 <= n? Yes (from requires)
    //   0 == 0 * 1 / 2? Yes
    //
    // Step 5: Verify preservation
    //   If acc == i * (i + 1) / 2 and i < n
    //   After: i' = i + 1, acc' = acc + i + 1
    //   Check: acc + (i+1) == (i+1) * (i+2) / 2
    //   Expand: i*(i+1)/2 + (i+1) == (i+1)*(i+2)/2
    //   Factor: (i+1) * (i/2 + 1) == (i+1)*(i+2)/2
    //   Simplify: (i+1)*(i+2)/2 == (i+1)*(i+2)/2 Yes

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

      i := i + 1;
      acc := acc + i;
    };

    // At exit: i >= n (from condition false) and i <= n (from invariant)
    // Therefore: i == n
    // From property invariant: acc == n * (n + 1) / 2

    acc
  };
}

Common Failure Patterns

Problem: "Postcondition might not hold"

Diagnosis: Your invariant is too weak. It holds through the loop but does not imply the postcondition at exit.

invariant-weak-initial.sr9 (fails)

// Demonstrating a weak invariant that fails
persistent actor {
  public func sumWrong(n : Int) : async Int
    requires n >= 0;
    ensures result == n * (n + 1) / 2;
  {
    var i = 0;
    var sum = 0;

    while (i < n) {
      // WEAK: Only bounds, no relationship to sum
      loop:invariant i >= 0 and i <= n;
      // Missing: loop:invariant sum == i * (i + 1) / 2;

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

    sum  // Postcondition cannot be proven without the property invariant
  };
}

Solution: Add a property invariant that directly relates to the postcondition:

invariant-strengthened.sr9 (verifies)

// Strengthened invariant that verifies
persistent actor {
  public func sumCorrect(n : Int) : async Int
    entry_requires n >= 0;
    requires n >= 0;
    ensures result == n * (n + 1) / 2;
  {
    var i = 0;
    var sum = 0;

    while (i < n) {
      // Bounds invariant: tracks loop progress
      loop:invariant i >= 0 and i <= n;
      // Property invariant: relates sum to loop counter
      loop:invariant sum == i * (i + 1) / 2;

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

    sum  // Now verifies: i == n and sum == n * (n + 1) / 2
  };
}

Problem: "Loop invariant might not be preserved"

Diagnosis: The invariant is not inductive. It breaks after executing the loop body.

invariant-non-inductive_unsat.sr9 (fails)

// Non-inductive invariant: claims field unchanged but we modify it
persistent actor {
  var counter : Int = 0;

  public func countdownWrong(n : Int) : async Int
    modifies counter
    requires n >= 0;
    ensures counter == old(counter);  // Claims unchanged
  {
    var i = n;

    while (i > 0) {
      loop:invariant i >= 0 and i <= n;
      // NON-INDUCTIVE: claims counter unchanged
      loop:invariant counter == old(counter);

      counter := counter + 1;  // This breaks the invariant!
      i := i - 1;
    };

    i
  };
}

Solution: Make the invariant track cumulative progress rather than claiming no change:

invariant-inductive.sr9 (verifies)

// Inductive invariant: tracks cumulative progress
persistent actor {
  var counter : Int = 0;

  public func countdownCorrect(n : Int) : async Int
    modifies counter
    entry_requires n >= 0;
    requires n >= 0;
    ensures result == 0;
    ensures counter == old(counter) + n;
  {
    var i = n;

    while (i > 0) {
      loop:invariant i >= 0 and i <= n;
      // INDUCTIVE: relates counter to progress made (n - i)
      loop:invariant counter == old(counter) + (n - i);

      counter := counter + 1;
      i := i - 1;
    };

    i
  };
}

Problem: "Loop invariant might not hold on entry"

Diagnosis: The invariant does not hold with initial values.

Solution: Check your initial variable values against the invariant. Either fix initialization or adjust the invariant to match the actual starting state.

Tracking Field Modifications

When loops modify actor fields, use old() to relate current values to entry values:

invariant-field-tracking.sr9

// Tracking field modifications with old()
persistent actor {
  var total : Int = 0;
  var count : Int = 0;

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

    while (i < n) {
      // Bounds: track loop progress
      loop:invariant i >= 0 and i <= n;
      // Property: relate local accumulator to counter
      loop:invariant sum == i * (i + 1) / 2;
      // Field tracking: relate fields to old values and progress
      loop:invariant total == old(total) + sum;
      loop:invariant count == old(count) + i;

      i := i + 1;
      sum := sum + i;
      total := total + i;
      count := count + 1;
    };

    sum
  };
}

The pattern field == old(field) + progress connects three pieces:

• Entry state (old(field))
• Current progress (accumulator or counter)
• Current field value

Nested Loop Invariants

For nested loops, inner invariants must account for outer loop progress:

invariant-nested-loop.sr9

// Nested loop invariants
persistent actor {
  public func gridSum(rows : Int, cols : Int) : async Int
    entry_requires rows >= 0 and cols >= 0;
    requires rows >= 0 and cols >= 0;
    ensures result == rows * cols;
  {
    var r = 0;
    var total = 0;

    while (r < rows) {
      // Outer bounds
      loop:invariant r >= 0 and r <= rows;
      // Outer property: total equals completed rows times cols
      loop:invariant total == r * cols;

      var c = 0;
      while (c < cols) {
        // Inner bounds
        loop:invariant c >= 0 and c <= cols;
        // Inner property: total includes outer progress plus inner progress
        loop:invariant total == r * cols + c;

        total := total + 1;
        c := c + 1;
      };

      r := r + 1;
    };

    total
  };
}

The inner invariant total == r * cols + c combines:

• Completed outer iterations: r * cols
• Current inner progress: c

Strengthening Checklist

When verification fails, try adding these in order:

If This Fails	Add This
Postcondition not provable	Property invariant relating accumulator to counter
Missing bounds	i >= 0 and i <= n for loop counter
Field modification tracking	field == old(field) + delta
Values should be unchanged	x == old(x) for unmodified variables
Array element properties	Quantified invariant over indices

Debugging Workflow

1. Identify the failure phase:

   • "might not hold on entry" → Initialization failure
   • "might not be preserved" → Preservation failure
   • "Postcondition might not hold" → Conclusion failure (invariant too weak)

2. For initialization failures: Print initial values, check against each invariant clause

3. For preservation failures: Trace one iteration by hand, identify which statement breaks the invariant

4. For postcondition failures: The invariant is too weak. Add a property invariant that directly matches the postcondition structure

5. Use intermediate assertions: Add assert statements inside the loop body to verify the invariant holds at specific points

Common Invariant Patterns

Accumulator Sum

loop:invariant sum == i * (i + 1) / 2;

Countdown Progress

loop:invariant progress == old(progress) + (start - i);

Array Range Property

loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
  j < i ==> processed(arr[j]));

Conservation

loop:invariant sum + remaining == total;

State Machine

loop:invariant state == #Running or state == #Done;

When Invariants Are Not Enough

Some verification failures indicate problems beyond the invariant:

• Wrong algorithm: The code does not compute what the postcondition claims
• Missing precondition: The caller must provide stronger requires guarantees
• Unsupported pattern: Some aliasing or mutation patterns are beyond current verification scope

If you have traced through the invariant manually and it should work, check that the implementation actually matches your mental model.

Summary

• Most loops need two invariants: bounds and property
• Work backwards from the postcondition to derive the property invariant
• An inductive invariant must hold after executing the loop body
• Use old() to track field modifications relative to method entry
• Nested loops require inner invariants that include outer progress
• Initialization, preservation, and conclusion failures each have distinct fixes
• For actor-level state, pair loop invariants with actor invariants and old expressions