Step Lemmas

Step lemmas break complex loop invariant proofs into manageable inductive steps that the SMT solver can verify.

The Inductive Gap Problem

When verifying loops, the verifier must prove that the loop invariant holds after each iteration. For simple arithmetic, this works automatically. For non-trivial mathematical relationships, the SMT solver often cannot bridge the gap between the current state and the next state.

Consider computing the triangular number (sum 1 + 2 + ... + n). The loop invariant states acc == triangular(i). After adding i + 1 to acc, we need to show acc == triangular(i + 1). This requires proving:

triangular(i) + (i + 1) == triangular(i + 1)

The SMT solver knows the definition triangular(n) == n * (n + 1) / 2 through the helper contract, but cannot always use that algebraic identity at the exact point where the loop needs it. A step lemma makes the relationship explicit at the call site.

The Step Lemma Pattern

Step lemmas follow a three-part structure:

1. Proof helper: Define the closed-form mathematical formula
2. Step lemma: Prove how the formula evolves from iteration i to i + 1
3. Loop: Call the lemma before updating the accumulator

lemma-step.sr9

// Step lemma for loop invariant maintenance
module {
  // Proof-only abstract helper defining the closed-form formula
  public ghost abstract func triangular(n : Nat) : Nat
    requires true;
    ensures result == n * (n + 1) / 2;

  // Step lemma: proves how triangular evolves at each iteration
  public lemma triangularStep(i : Nat) : ()
    ensures triangular(i) + (i + 1) == triangular(i + 1);
  {
  };

  // Sum 1 + 2 + ... + n using the step lemma
  public func sumToN(n : Nat) : Nat
    ensures result == triangular(n);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant acc == triangular(i);

      triangularStep(i);  // Establishes: triangular(i) + (i+1) == triangular(i+1)
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

The key is line 24: triangularStep(i) establishes the fact that triangular(i) + (i + 1) == triangular(i + 1). Combined with the loop invariant acc == triangular(i), the verifier can prove the invariant holds after the update.

Anatomy of a Step Lemma

A step lemma has these characteristics:

Property	Description
Parameters	Current loop variable(s)
Preconditions	Usually none (or bounds from the loop)
Postcondition	Relates state at i to state at i + 1
Body	Often empty, or a short chain of lemma/axiom calls
Call site	Inside the loop, before the state update

The postcondition captures the inductive step: given what holds at iteration i, what holds at iteration i + 1.

Parameterized Step Lemmas

Step lemmas can take additional parameters beyond the loop counter. This makes them reusable across different configurations:

step-linear.sr9

// Step lemma for linear progression with arbitrary step size
module {
  pure func lin(start : Int, step : Int, n : Int) : Int { start + n * step };

  public lemma linStep(start : Int, step : Int, i : Int) : ()
    ensures lin(start, step, i) + step == lin(start, step, i + 1);
  {
  };

  public func linear(start : Int, step : Int, n : Int) : Int
    requires n >= 0;
    ensures result == lin(start, step, n);
  {
    var i : Int = 0;
    var acc : Int = start;

    while (i < n) {
      loop:invariant i >= 0;
      loop:invariant i <= n;
      loop:invariant acc == lin(start, step, i);
      linStep(start, step, i);  // Parameterized step lemma
      acc += step;
      i += 1;
    };

    acc
  };
}

The linStep lemma takes three parameters: start, step, and i. It proves the relationship for any starting value and step size, not just specific constants.

Step Lemmas for Non-Obvious Identities

Some algorithms rely on mathematical identities that are not obvious to the SMT solver. Computing n^2 by summing odd numbers demonstrates this:

step-square.sr9

// Step lemma proving n^2 = 1 + 3 + 5 + ... + (2n-1)
module {
  pure func square(n : Nat) : Nat { n * n };
  pure func odd(i : Nat) : Nat { 2 * i + 1 };

  public lemma squareStep(i : Nat) : ()
    ensures square(i + 1) == square(i) + odd(i);
  {
  };

  public func squareByOdds(n : Nat) : Nat
    ensures result == square(n);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant acc == square(i);
      squareStep(i);  // square(i+1) == square(i) + odd(i)
      acc += odd(i);
      i += 1;
    };

    acc
  };
}

The identity (i+1)^2 = i^2 + (2i+1) is the key insight. The step lemma squareStep encodes this, allowing the verifier to connect the loop invariant to the postcondition.

Call Placement

Usually call the step lemma before updating the accumulator:

while (i < n) {
  loop:invariant acc == formula(i);

  stepLemma(i);   // First: establish the relationship
  acc += update;  // Then: update matches the lemma's postcondition
  i += 1;
}

Calling after the update usually does not work because the lemma establishes facts about the pre-update state. The verifier needs those facts before reasoning about the assignment. If the lemma is about a post-update value, name that value first and call the lemma before the invariant check point.

When Step Lemmas Are Needed

Use step lemmas when:

• The loop invariant involves multiplication or division
• The formula has a closed form different from the iterative computation
• The relationship between iterations is algebraic, not structural
• The verifier fails with "postcondition might not hold" for a loop
• Quantified loop invariants need a reusable one-step preservation fact

You do not need step lemmas when:

• The invariant is purely additive (e.g., acc == i * constant)
• The update matches the invariant structure directly
• Simple bounds checking suffices
• A local assertion already gives the solver enough information

Missing Step Lemma Example

Omitting the step lemma causes verification to fail:

step-missing_unsat.sr9

// Missing step lemma causes verification failure
module {
  public pure trusted func triangular(n : Nat) : Nat
    requires true;
    ensures result == n * (n + 1) / 2;

  public lemma triangularStep(i : Nat) : ()
    ensures triangular(i) + (i + 1) == triangular(i + 1);
  {
  };

  public func sumToN(n : Nat) : Nat
    ensures result == triangular(n);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant acc == triangular(i);
      // WRONG: Missing triangularStep(i);
      // The verifier cannot prove: acc + (i+1) == triangular(i+1)
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

The verifier reports that the loop invariant might not be preserved. It knows acc == triangular(i) and acc' == acc + (i + 1), but cannot prove acc' == triangular(i + 1) without the explicit step lemma.

Multiple Step Lemmas

Complex loops may require multiple step lemmas to maintain different invariants:

while (i < n) {
  loop:invariant sum == formula1(i);
  loop:invariant product == formula2(i);

  stepSum(i);      // Maintains sum invariant
  stepProduct(i);  // Maintains product invariant

  sum += next1;
  product *= next2;
  i += 1;
}

Each lemma focuses on one relationship, keeping the proofs modular.

Step Lemmas with Preconditions

Some step lemmas require preconditions from the loop context:

public lemma divStep(num : Nat, denom : Nat, i : Nat) : ()
  requires denom > 0;  // Required for division
  requires i < num / denom;
  ensures formula(i) + denom == formula(i + 1);
{
};

The preconditions must be provable at the call site. Loop invariants often establish the necessary facts. If the lemma uses division, include guards such as denom > 0; see division verification.

Deriving Step Lemmas

To derive a step lemma for a formula f(i):

1. Write out f(i + 1) expanded
2. Write out f(i) expanded
3. Express the difference or relationship between them
4. That relationship becomes the postcondition

For triangular numbers:

• f(i + 1) = (i + 1) * (i + 2) / 2
• f(i) = i * (i + 1) / 2
• f(i + 1) - f(i) = i + 1
• Postcondition: f(i) + (i + 1) == f(i + 1)

Common Mistakes

Wrong Variable in Lemma Call

// Wrong: using j instead of i
stepLemma(j);  // Establishes facts about j, not the loop variable i
acc += update;
i += 1;

Step Lemma After Update

// Wrong: lemma called after the update
acc += update;
stepLemma(i);  // Too late - verifier already failed to prove invariant
i += 1;

Missing Parameters

// Wrong: not passing all loop-relevant values
stepLemma(i);  // If step depends on start/step, those must be passed

Summary

• Step lemmas prove the inductive step that the SMT solver cannot derive automatically
• Follow the pattern: pure function, step lemma, loop with lemma call before update
• The postcondition relates state at iteration i to iteration i + 1
• Call the lemma inside the loop, before updating the accumulator
• Parameterize lemmas for reusability across different configurations
• Derive lemmas by comparing f(i + 1) to f(i) algebraically
• Add preconditions for division, bounds, or collection membership facts the lemma needs

Related Topics

• Using lemmas for call placement and debugging
• Inductive loop invariants for the verifier's loop proof obligations
• Numeric verification when multiplication or division identities need extra proof structure
• Quantifier patterns for loop invariants over arrays and collections