Skip to main content

The loop:invariant Annotation

A loop invariant is a property that must hold before each iteration of a loop. The verifier checks that it holds initially and that the loop body preserves it.

Syntax​

Place the loop:invariant annotation inside the loop body, typically at the beginning:

while (condition) {
  loop:invariant property;
  // loop body
};

For multiple invariants, use separate annotations:

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

How Verification Works​

The verifier proves three things about each loop invariant:

  1. Initialization: The invariant holds before the loop starts
  2. Preservation: If the invariant holds at the start of an iteration and the loop condition is true, it still holds after the loop body executes
  3. Conclusion: When the loop exits (condition is false), the invariant plus the negated condition imply the postcondition

This is inductive reasoning: prove the base case (initialization) and the inductive step (preservation), then conclude the property holds when the loop terminates.

Basic Example​

A countdown loop that returns zero:

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

The invariant i <= n holds:

  • Initially: i = n, so i <= n is true
  • Each iteration: decrementing i keeps i <= n true
  • At exit: i <= n and not (i > 0) means i == 0, proving the postcondition

Multiple Invariants​

Complex loops often need multiple invariants. One tracks progress, another tracks the computation:

persistent actor {
  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
  };
}

The first invariant tracks bounds (i <= n). The second tracks the mathematical relationship between the accumulator and the loop counter.

Invariants with Actor Fields​

Loop invariants can reference actor fields using old() to relate current values to method-entry values:

persistent actor {
  var counter : Int = 0;

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

The invariant counter == old(counter) + i relates the current counter value to both the starting value and the loop progress.

For Loops​

Loop invariants also work with for loops over arrays:

persistent actor {
  public func sumArray(arr : [Nat]) : async Nat
    ensures result >= 0;
  {
    var total : Nat = 0;

    for (x in arr.values()) {
      loop:invariant total >= 0;
      total += x;
    };

    total
  };
}

Nested Loops​

Each level of nesting needs its own invariants. The inner loop's invariant must account for the outer loop's state:

persistent actor {
  public func sumGrid(rows : Nat, cols : Nat) : async Nat
    entry_requires rows <= 3 and cols <= 3;
    requires rows <= 3 and cols <= 3;
    ensures result == rows * cols;
  {
    var total : Nat = 0;
    var r : Nat = 0;

    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;
        total += 1;
        c += 1;
      };

      r += 1;
    };

    total
  };
}

The inner invariant total == r * cols + c accounts for both the outer loop's completed rows and the inner loop's progress.

What Can Appear in Invariants​

Invariants support specification expressions similar to ensures clauses. They are proof-only facts, so they can call pure helpers, use old(), and state quantified facts over processed ranges.

AllowedExamples
Comparisonsi >= 0, x == y, n < 10
Logical operatorsa and b, a or b, not a, ==>
Arithmeticsum == i * (i + 1) / 2
Field accesscounter == old(counter) + i
Array accessarr[i] >= 0
Pure function callsisValid(x)
Quantifiersforall<Nat>(pure func (j : Nat) : Bool = j < i ==> processed[j])

Restrictions​

No Allocations​

Loop invariants cannot contain allocation expressions:

// This is rejected:
while (i < n) {
  loop:invariant (([] : [Nat]).size()) == 0;  // Error: allocation in invariant
  i += 1;
};

Array literals and object literals allocate memory, which is not allowed in invariants.

old() Still Means Method Entry​

old() is allowed in loop invariants when the invariant is a verification-only context, but it still refers to method entry. It does not mean "the value before this iteration." Use a normal local variable if the loop needs to remember a per-iteration value.

This matters for actor fields: counter == old(counter) + i means "relative to method entry", not "relative to the previous pass through the loop." For async loops, a suspending await can re-open actor interleaving, so facts about actor fields must either be protected by actor invariants or re-established after the await.

Verification Mode Required​

The loop:invariant annotation is only available in verification mode. In normal compilation, it produces an error.

Common Mistakes​

Non-Inductive Invariant​

The invariant must be preserved by the loop body. If the body invalidates the invariant, verification fails:

// This fails verification:
public func wrong(n : Int) : async Int
  modifies counter
  ensures counter == old(counter);  // Claims counter is unchanged
{
  var i = n;
  while (i > 0) {
    loop:invariant counter == old(counter);  // But we modify counter below!
    counter := counter + 1;  // Breaks the invariant
    i := i - 1;
  };
  i
}

The invariant claims counter is unchanged, but the body increments it. This is not inductive.

Missing Bounds​

Forgetting to bound loop variables is a common error:

// May have issues:
while (i < n) {
  loop:invariant sum == i * (i + 1) / 2;  // Missing: i >= 0 and i <= n
  // ...
};

Always include bounds invariants like i >= 0 and i <= n.

Invariant Too Weak​

The invariant must be strong enough to prove the postcondition:

// Too weak:
public func sumTo(n : Nat) : async Nat
  ensures result == n * (n + 1) / 2;
{
  var i : Nat = 0;
  var acc : Nat = 0;
  while (i < n) {
    loop:invariant i <= n;  // Not enough! Missing relationship to acc
    acc += i + 1;
    i += 1;
  };
  acc
}

Add the invariant relating acc to i: loop:invariant acc == i * (i + 1) / 2;

Loops with Control Flow​

Continue and Break​

Invariants must hold even when the loop uses continue or break:

persistent actor {
  public func countOdd(n : Int) : async Int
    entry_requires n >= 0;
    requires n >= 0;
    ensures result >= 0;
  {
    var count : Int = 0;
    var i : Int = 0;

    label counter while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant count >= 0;
      i += 1;
      if (i % 2 == 0) {
        continue counter;
      };
      count += 1;
    };

    count
  };
}

The invariants are checked before each iteration, including when continue jumps back to the loop head.

Working with Lemmas​

For complex mathematical properties, use lemmas to establish invariant preservation:

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

  public lemma tri2Step(i : Nat) : ()
    ensures tri2(i) + 2 * (i + 1) == tri2(i + 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);
      tri2Step(i);  // Lemma call helps verifier
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

The lemma tri2Step establishes the step property that makes the invariant inductive.

Inferred Facts​

Sector9 infers some facts around loops:

  • Type facts: Nat values are non-negative by type
  • Array access obligations: arr[i] creates an obligation to prove i < arr.size()
  • Framing facts: fields outside a method's modifies footprint remain stable while the method executes atomically

These are not a substitute for the invariants that connect loop progress to your postcondition. Write the bounds and property invariants that make the proof readable.

Summary​

  • loop:invariant declares a property preserved by each loop iteration
  • Place invariants at the start of the loop body
  • Verification checks: initialization, preservation, and conclusion
  • Use multiple invariants: one for bounds, one for the computed property
  • Common mistake: non-inductive invariant that the loop body breaks
  • Include bounds invariants like i >= 0 and i <= n
  • Invariants work with for loops, nested loops, and control flow