Contracts, implementations and proofs

The three roles every checked component plays, how they become store objects, and the three jobs theorems do in an application.

Every checked component in Lema has three parts: a contract that says what must be true, an implementation that computes, and a proof that the implementation meets the contract. These are roles. Lema has no object kind called contract or implementation. In the store, the parts become statements, templates, proofs and satisfactions (objects and identity). A contract can itself be a definition, as the counter contract further down is.

From an open question to a theorem

The standard library’s sort shows how the three roles relate. It is in lean/std/Canonical.lean, where SigV4 uses it to put query parameters and headers in canonical order:

/-- Insert before the first element that `x` is at most. -/
def insertBy {α : Type} (le : α → α → Bool) (x : α) : List α → List α
  | [] => [x]
  | y :: ys => if le x y then x :: y :: ys else y :: insertBy le x ys

def sortBy {α : Type} (le : α → α → Bool) (l : List α) : List α := l.foldr (insertBy le) []

On its own, a contract is a question you can ask of any implementation. For sorting, the question is: given a comparison le, does a function s always return a permutation of its input, and is the result in order when le is transitive and total? Until you name a function, the question has no answer. The library does not define this contract as a separate object. It states the two properties of sortBy directly.

Applied to an implementation, the contract becomes a statement, which is a proposition that is true or false. For sortBy, the two statements are the types of these theorems:

theorem sortBy_perm {α : Type} (le : α → α → Bool) : ∀ l : List α, (sortBy le l).Perm l

theorem sortBy_sorted {α : Type} (le : α → α → Bool)
    (trans : ∀ a b c, le a b = true → le b c = true → le a c = true)
    (total : ∀ a b, le a b = true ∨ le b a = true) :
    ∀ l : List α, (sortBy le l).Pairwise (fun a b => le a b = true)

In the store, each statement is a statement object whose type cites sortBy by the ID of its template.

Add a proof that the pinned Lean 4.34.1 kernel accepts, and the statement becomes a theorem. Both proofs are in the same file, and both theorems were accepted through the API on 16 Oct 2026 (crates/lema-cli/tests/std_canonical.rs). Each theorem is stored as a declaration whose binding is a satisfaction object. The satisfaction ties together the statement, the template, the proof and a list of realizations. The realizations say which declaration each citation means, and sortBy itself is among them. The declaration’s receipt records the checker, the axiom footprint and the call in which the kernel replayed it. Because the declaration names its satisfaction, the receipt covers exactly this proof of this statement, with these realizations.

The statements say nothing about cost. sortBy is a quadratic insertion sort, chosen because the kernel can evaluate it. The file notes that Lean’s List.mergeSort is defined by well-founded recursion, and that decide +kernel did not reduce it on a ten-element list. The same two statements could be proved of a faster sort, and they would not tell you which sort is faster.

Bundled and unbundled contracts

Lean offers two ways to tie a contract to an implementation, and Lema uses both.

A bundled contract is a structure that carries its properties as fields. Std.Map takes its key order this way:

/-- A lawful total order on keys. -/
structure Order (K : Type) where
  compare : K → K → Ordering
  eq_iff : ∀ a b, compare a b = .eq ↔ a = b
  swap : ∀ a b, compare b a = (compare a b).swap
  trans : ∀ a b c, compare a b = .lt → compare b c = .lt → compare a c = .lt

You cannot build an Order without the three proofs. natOrder in the same file supplies them for Nat. The operation and its properties travel as one value, so a map cannot be handed a comparison that lacks them. In the store, the proof fields of a value like natOrder become numbered slots in its template, and the proofs are separate objects. Proving trans a different way therefore does not change the template of natOrder.

An unbundled contract keeps the contract, the implementation and the theorem as separate declarations. The Program core works this way. Here is the Core v2 counter from lean/core/ReplaceV2.lean:

/-- A counter: each tick replies with the count so far. -/
def counter : Received.Contract Unit (fun _ => Nat) Nat :=
  Received.mkContract (fun _ _ => True) (fun s _ _ => s + 1) (fun s _ r => r = s)

def plain : Received.Impl Unit (fun _ => Nat) Nat := Received.mkImpl (fun m _ => (m, m + 1))
def offset : Received.Impl Unit (fun _ => Nat) Nat :=
  Received.mkImpl (fun n _ => (n - 5, n + 1))

counter says nothing about any implementation, and neither implementation mentions counter. The theorems that connect them come later, separately. Core’s Safe (a program follows a contract) and Implements (an implementation keeps a contract’s promises) are propositions of this kind.

Each form has a cost. Bundling makes the properties impossible to forget, but it fixes them when the structure is defined, so adding a property means a new structure. Unbundling lets you prove more about an implementation later without changing its ID, and lets one implementation meet several contracts. But nothing forces the theorem to exist. A consumer has to ask for it, by taking it as an argument or receiving it by ID.

The three jobs of theorems

In an application built from contracts and implementations, theorems do three different jobs.

Satisfaction

A satisfaction theorem says that an implementation meets its contract. sortBy_perm and sortBy_sorted are satisfaction theorems. So are the two in the reuse example (lean/examples/reuse/), where the contract is ∀ x, f x = x for a function f : Nat → Nat:

def implA : Nat → Nat := fun x => x

theorem implA_law : ∀ x, implA x = x := fun _ => rfl

def implB : Nat → Nat := fun x => 0 + x

theorem implB_law : ∀ x, implB x = x := fun x => Nat.zero_add x

Composition

A composition theorem proves something about a larger piece from the contracts of its parts, without looking inside them. The canonical query string in Std.Canonical is sorted because the sort is:

theorem queryPairs_sorted (qs : List (List UInt8 × List UInt8)) :
    (queryPairs qs).Pairwise (fun p q => pairLe p q = true) :=
  sortBy_sorted pairLe pairLe_trans pairLe_total _

The proof applies sortBy_sorted to three facts about the comparison pairLe. Nothing in it depends on how sortBy inserts. The reuse example’s consumer does the same with a general theorem, twice_id, proved once for every f that meets the contract:

theorem par_twice : ∀ x, Received.f (Received.f x) = x :=
  Received.twice_id Received.f Received.f_law

Received.f and Received.f_law are bindings to accepted objects, chosen when the source is elaborated (authoring rules).

Replacement

A replacement theorem says that one implementation can stand in for another without any client noticing. For pure functions that meet the same contract, the contract often does this job by itself. Parametric.lean uses only the contract. Bound to implB and implB_law, the same source proves the same fact for implB, with no new proof. The concrete control, Concrete.lean, proves the statement by rfl, which unfolds the body of implA. Bound to implB it fails to elaborate, and a new proof (ConcreteB.lean) had to be written. docs/research/minimal-reuse.md measures both paths (native run of 16 Oct 2026). A client that depends on the contract can switch implementations, and one that depends on a body cannot.

Programs with state need a separate claim. The two implementations keep different private states, and the claim has to relate them. offset holds the count plus five, so the relation is Shifted, and the claim starts from count 0:

/-- `offset` holds the count plus five. -/
def Shifted (s m n : Nat) : Prop := m = s ∧ n = s + 5

def PlainOffset : Prop := Received.Replaces 0 0 5 counter plain offset Shifted

theorem plain_offset : PlainOffset := ⟨⟨rfl, rfl⟩, shifted_steps⟩

shifted_steps, proved in the same file, shows that the two agree on every tick from related states. replaces_runs in lean/core/Replaces.lean turns such a claim into a guarantee for clients: from those start states, every program that is safe on counter returns the same result on plain and on offset. The store’s replace method moves an alias from one implementation to the other only when given an accepted proof of exactly such a claim. crates/lema-cli/tests/replace_v2.rs moves counter.impl from plain to offset this way.

The start states are part of the claim because Simulates on its own has none, and a relation that is never true proves it for any two implementations. Whoever relies on a replacement checks that its start states match the deployment.

Replace an implementation gives the steps, and Publish your first proof starts from the beginning.