Using Lemmas

Calling lemmas establishes facts that help the verifier prove your code correct.

Calling Lemmas

A lemma call looks like a regular function call, but it exists only for verification. The call establishes the lemma's postconditions as facts the verifier can use.

addPositive(a, b);  // After this call, verifier knows: a + b > a and a + b > b

Lemma calls are erased from runtime output. They have no runtime cost, but they still matter to verification because their requires clauses must hold and their ensures clauses become available afterward.

Where Lemmas Can Be Called

Lemmas can be called from ordinary function bodies, ghost blocks, and other lemmas. Calls are proof steps, so they are erased from runtime output, but their preconditions must still be proven at the call site.

Location	Valid	Example
Function body	Yes	Before return to establish postconditions
Loop body	Yes	To maintain loop invariants
Conditional branches	Yes	Different lemmas for different cases
Ghost blocks	Yes	Alongside ghost state updates
Other lemmas	Yes	To build layered proofs
Contracts	No	Lemmas are statements, not expressions

For readability, many teams put lemma calls in ghost { } blocks when the call is only there to shape a proof. That is optional; the call is proof-only either way.

Establishing Facts for Postconditions

The most common use is calling a lemma right before a function returns to help prove the postcondition:

lemma-basic.sr9

// Basic lemma declaration with preconditions and postconditions
module {
  // A lemma establishing an arithmetic fact
  public lemma addPositive(x : Nat, y : Nat) : ()
    requires x > 0;
    requires y > 0;
    ensures x + y > x;
    ensures x + y > y;
  {
    // Body can be empty - verifier proves postconditions from preconditions
  };

  // Using the lemma to help verify a function
  public func sumPositive(a : Nat, b : Nat) : Nat
    requires a > 0;
    requires b > 0;
    ensures result > a;
    ensures result > b;
  {
    addPositive(a, b);  // Call lemma to establish facts
    a + b
  };
}

Line 20 calls addPositive(a, b). After this call, the verifier knows that a + b > a and a + b > b. These facts match the function's ensures clauses on lines 17-18, so verification succeeds.

Without the lemma call, the verifier might not automatically connect the preconditions to the postconditions, and verification would fail. This is the same proof-shaping role that pure helper functions play in contracts, but lemmas establish facts through calls instead of returning values.

Maintaining Loop Invariants

Step lemmas are called inside loop bodies to prove that the invariant holds after each iteration:

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 critical call is on line 24: triangularStep(i). This establishes:

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

The verifier knows acc == triangular(i) from the loop invariant. After the lemma call, it can prove that the updated acc equals triangular(i + 1), maintaining the invariant.

The Step Lemma Pattern

1. Define a proof/spec helper for the closed-form property
2. Write a step lemma proving how the property evolves
3. Call the lemma inside the loop, before the update
4. The verifier connects the dots

This pattern works because the lemma establishes exactly the inductive step the verifier needs. If the loop also mutates actor state, make sure the enclosing method has the right modifies clause.

Chaining Lemma Calls

Lemmas can call other lemmas. Build complex proofs from simpler facts:

lemma-chain.sr9

// Lemma chaining: lemmas can call other lemmas
module {
  // Base lemma
  public lemma nonNegative(x : Nat) : ()
    ensures x >= 0;
  {
  };

  // Derived lemma calling the base lemma
  public lemma sumNonNegative(a : Nat, b : Nat) : ()
    ensures a >= 0;
    ensures b >= 0;
    ensures a + b >= 0;
  {
    nonNegative(a);
    nonNegative(b);
  };

  // Function using the derived lemma
  public func addNats(x : Nat, y : Nat) : Nat
    ensures result >= 0;
  {
    sumNonNegative(x, y);
    x + y
  };
}

The sumNonNegative lemma (lines 10-17) calls nonNegative twice. Each call establishes a fact. Together, they prove all three postconditions.

Building Proof Layers

For complex properties, structure your lemmas hierarchically:

// Level 1: Basic facts
public lemma fact1(x : Nat) : ()
  ensures x >= 0;
{ };

public lemma fact2(x : Nat, y : Nat) : ()
  requires x < y;
  ensures y - x > 0;
{ };

// Level 2: Derived properties using level 1
public lemma combined(a : Nat, b : Nat) : ()
  requires a < b;
  ensures a >= 0;
  ensures b - a > 0;
{
  fact1(a);       // Establishes: a >= 0
  fact2(a, b);    // Establishes: b - a > 0
};

Calling Lemmas in Conditionals

Different cases may need different lemmas:

public lemma greaterCase(x : Nat, y : Nat) : ()
  requires x > y;
  ensures x - y > 0;
{ };

public lemma equalCase(x : Nat, y : Nat) : ()
  requires x == y;
  ensures x - y == 0;
{ };

public func diff(a : Nat, b : Nat) : Nat
  requires a >= b;
  ensures (a > b) ==> (result > 0);
  ensures (a == b) ==> (result == 0);
{
  if (a > b) {
    greaterCase(a, b);  // Lemma for this branch
    a - b
  } else {
    equalCase(a, b);    // Different lemma for this branch
    0
  }
};

Each branch calls the lemma whose preconditions match the branch condition.

Passing Arguments to Lemmas

Lemma arguments scope the established facts to specific values:

public lemma bounded(x : Nat, limit : Nat) : ()
  requires x < limit;
  ensures x + 1 <= limit;
{ };

public func increment(value : Nat, max : Nat) : Nat
  requires value < max;
  ensures result <= max;
{
  bounded(value, max);  // Establishes: value + 1 <= max
  value + 1
};

The call bounded(value, max) establishes facts about value and max specifically, not about arbitrary values.

When to Use Lemmas

Use a lemma when:

• The verifier fails to prove a postcondition that follows from available facts
• A loop invariant involves a mathematical formula
• You need to connect scattered facts into a conclusion
• The proof step is not obvious to the SMT solver
• You want to name and reuse a quantified or arithmetic proof step across several methods

You likely do not need a lemma when:

• The postcondition directly follows from the computation
• The property is purely structural (type-based)
• Simple arithmetic suffices
• A pure helper can express the predicate directly in the contract

Common Mistakes

Calling Without Preconditions

If a lemma has preconditions, they must hold at the call site:

Wrong

public lemma positive(x : Nat) : ()
  requires x > 0;
  ensures x >= 1;
{ };

public func use(n : Nat) : Nat {  // n might be 0
  positive(n);  // ERROR: precondition x > 0 might not hold
  n
};

Correct

public lemma positive(x : Nat) : ()
  requires x > 0;
  ensures x >= 1;
{ };

public func use(n : Nat) : Nat
  requires n > 0;  // Ensure precondition is satisfied
{
  positive(n);  // Now valid
  n
};

Missing Lemma Calls

If verification fails unexpectedly, check whether you forgot to call a needed lemma:

public func sumTo(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);
    // Missing: triangularStep(i);  <-- Verification will fail
    acc += i + 1;
    i += 1;
  };

  acc
};

Wrong Lemma Arguments

Passing wrong arguments establishes facts about the wrong values:

// Wrong: passing constants instead of loop variables
mulStep(1, 2);  // Establishes facts about 1 and 2, not a and i

// Correct: passing the actual loop variables
mulStep(a, i);  // Establishes facts about a and i

Debugging Failed Lemma Calls

If verification fails at a lemma call:

1. Check preconditions - Are all requires clauses satisfied?
2. Check argument types - Are you passing the right values?
3. Add intermediate assertions - Use assert to check what the verifier knows
4. Simplify - Try a minimal example to isolate the issue
5. Check trust mode - A trusted lemma assumes postconditions, while an ordinary lemma must verify them

public func debug(x : Nat, y : Nat) : Nat
  requires x > 0;
  requires y > 0;
{
  assert x > 0;         // Verify precondition
  assert y > 0;         // Verify precondition
  addPositive(x, y);    // Call should now succeed
  assert x + y > x;     // Verify postcondition was established
  x + y
};

Summary

• Call lemmas like functions to establish their postconditions as facts
• Lemmas can be called anywhere in function bodies, not just ghost blocks
• Step lemmas inside loops prove invariant maintenance
• Lemma calls can be chained to build complex proofs
• Preconditions must hold at the call site
• Lemma calls are erased at runtime and have no runtime cost
• Use ghost blocks for clarity when lemma calls are only proof scaffolding

Related Topics

• Declaring lemmas for syntax and restrictions
• Debugging preconditions when a lemma call fails
• Reading verification errors for counterexample-driven lemma placement
• Trusted base for the cost of trusted lemmas