Declaring Lemmas

Lemmas are proof helpers that establish facts for the verifier without affecting runtime behavior.

What is a Lemma?

A lemma is a function marked with the lemma keyword that serves as a proof method. Unlike regular functions, lemmas:

• Are proof-only declarations used by the verifier
• Operate in a ghost context and can use verifier-only expressions such as ==>, <==>, and old()
• Have their postconditions verified by the SMT solver unless they are marked trusted
• Are erased from runtime output

Use lemmas when the verifier needs help connecting preconditions to postconditions, especially in loops, quantified arguments, and algebraic facts around spec collections.

Syntax

public lemma name(param1 : Type1, param2 : Type2) : ()
  requires precondition1;
  requires precondition2;
  ensures postcondition1;
  ensures postcondition2;
{
  // Body can be empty or contain calls to other lemmas
};

Key syntax points:

• Return type is typically () (unit)
• Multiple requires and ensures clauses are allowed
• Body can be empty if the postconditions follow from the preconditions
• public lemma is useful in modules; actor-local helper lemmas are usually private because public actor fields must be shared methods
• Lemmas that read or write actor fields use the same reads and modifies clauses as other verified code

Basic Lemma Declaration

The simplest lemma states a fact that the verifier can prove from its preconditions:

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
  };
}

The lemma addPositive establishes that adding two positive numbers produces a result greater than either input. Calling the lemma in sumPositive makes these facts available to prove the postconditions.

Abstract and Trusted Signature-Only Lemmas

For verification-driven development, lemmas can be declared without bodies when they are marked abstract:

public abstract lemma squareNonNeg(x : Nat) : ()
  requires true;
  ensures x * x >= 0;

The verifier checks preconditions at call sites and assumes the lemma postconditions until the abstract lemma is refined with a body.

Use trusted only for a permanent unchecked proof assumption:

public trusted lemma squareNonNeg(x : Nat) : ()
  requires true;
  ensures x * x >= 0;

Signature-only lemmas are useful when:

• The property is mathematically obvious but tedious to prove
• You want to bootstrap verification before proving all supporting facts
• The proof exists externally (on paper or in another system)

Prefer abstract lemma for temporary VDD scaffolding. Use trusted signature-only lemmas sparingly; they expand the trusted base since their correctness is assumed permanently, not verified.

Trusted lemmas must still declare at least one requires and one ensures clause. Use requires true; or ensures true; if the contract is intentionally unconditional.

Step Lemmas for Loops

Step lemmas are the most common lemma pattern. They prove how a property evolves from one loop iteration to the next:

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 triangularStep lemma proves the key inductive step: if acc == triangular(i), then after adding i + 1, we have acc == triangular(i + 1). This bridges the gap that the verifier cannot cross on its own.

Lemma Chaining

Lemmas can call other lemmas in their bodies to build up complex proofs:

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 calls nonNegative twice to establish facts about both inputs before concluding that their sum is also non-negative.

Lemma Body Rules

Lemmas are proof-only, but they are not identical to pure functions. A lemma body is lowered as verifier proof code, so it may contain local proof steps, assertions, local variables, and calls to other lemmas.

Allowed	Not Allowed
Calling other lemmas	State mutation (var :=)
Calling pure functions	await expressions
Static assert proof steps	Runtime message sends
Local variables and local assignment	trap, runtime:assert
==>, <==>, and old()	inline lemma
Empty bodies	Public actor exposure as a non-shared method
Actor field effects with reads/modifies	Missing footprints for field effects

If a lemma writes actor state for a proof model, declare the field in modifies. If it calls an impure or async function, verification rejects the call just as it would in other proof-only contexts.

Incorrect Lemmas

If a lemma's postcondition is false, verification fails:

lemma-wrong_unsat.sr9

// Incorrect lemma postcondition - verification fails
module {
  // This lemma has a false postcondition
  // The verifier will reject it (UNSAT)
  public lemma wrongFact(x : Nat, y : Nat) : ()
    requires y > 0;
    ensures x + y < x;  // FALSE: adding positive y cannot decrease x
  {
  };
}

The verifier rejects this lemma because adding a positive number cannot decrease the result.

Lemmas vs Pure Functions vs Trusted Functions

Feature	lemma	pure func	trusted func
Body verified	Yes	Yes	No
Can use old()	Yes	No	Only in trusted proof/spec contexts
Can be recursive	Supported as proof calls, but use carefully	No	Yes
Erased at runtime	Yes	No	No
Use case	Proof helpers	Spec predicates	External code or unchecked assumptions

Choose lemma when you need to establish proof facts. Choose pure when you need a helper function in contracts. Choose trusted when you need to assume correctness of external or complex code.

Related Topics

• Using lemmas for call-site patterns
• Step lemmas for loop induction
• Trusted signature-only declarations for permanent assumptions
• Abstract functions for VDD placeholders that are not lemmas

Summary

• Declare lemmas with the lemma keyword in place of func, for example public lemma step(...) : ()
• Lemmas are proof-only and operate in ghost context
• Bodies can be empty when postconditions follow from preconditions
• Abstract signature-only lemmas are VDD placeholders; trusted signature-only lemmas are trusted-base assumptions
• Trusted lemmas need explicit requires and ensures clauses
• Step lemmas help verify loops by proving the inductive step
• Lemmas can call other lemmas to build complex proofs