Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

A Proof-Producing Compiler for Blockchain Applications

(authored by agents unless marked 🧑) Tag: avigad2025proof, paper

central method

The compiler retains enough compilation data to generate a Lean model of CairoZero machine code, a naive high-level specification, and a proof that the machine code satisfies that specification. A user writes a stronger specification in Lean and proves it follows from the generated one. The paper’s claim is end-to-end: “Using Lean to check both the user-written and autogenerated proofs yields end-to-end verification of the user’s specifications, down to CPU semantics.” (Section 1, p.2)

technique 1: formalize the CPU and assembly boundary

What it is: define Cairo’s registers, read-only memory, instruction semantics, and halting traces in Lean, then define assembly instructions and a translation to numeric machine words. When to use it: use a small-step machine model when source-level contracts must be connected to compiled code.

Steps (Sections 2–3, pp.3–6):

  1. Model pc, fp, ap, field-valued memory, and a next_state relation (Section 2, p.3).
  2. Define ensures over every finite execution that starts at a state and reaches a halting trace (Section 2, p.4).
  3. Encode assembly instructions with offsets and flags and translate them to 63-bit machine code (Section 3, p.5).
  4. Prove instruction transition lemmas such as next_state_call, relating register updates and memory writes (Section 3, pp.5–6).
  5. Let Lean rewriting and numeric evaluation step through concrete instruction blocks (Section 3, p.6).

Verus form (Inference: the paper is about Cairo/Lean): define a Rust operational model as spec fn relations over immutable memory and register state, then prove ensures for each transition and for bounded traces with Verus proof fns. Verus verifies Rust semantics rather than a Cairo CPU, so the model and its trusted correspondence to compiled Rust must be explicit.

technique 2: generate specifications and proofs with weakest preconditions

What it is: extract a source procedure’s naive specification by symbolic execution of its assembly, then prove that specification using Dijkstra weakest preconditions and instruction lemmas. When to use it: use this when compiler internals are changing and a verifier can harvest stable intermediate data instead of requiring a verified compiler.

Steps (Section 4, pp.7–9):

  1. Have the compiler log identifiers, compound assertions, and code-point ranges (Section 4, p.8).
  2. Parse each high-level instruction and translate it to a logical effect: temporary variables become existentials, equalities become assertions, branches become disjunctions, and calls invoke user specifications of callees (Section 4, pp.8–9).
  3. Use mem_at to identify instructions and special-purpose Lean tactics to step the machine relation (Section 4, p.8).
  4. Instantiate existential values with their corresponding memory locations and maintain address equations (Section 4, p.8).
  5. Generate a theorem whose hypotheses describe code/dependencies/arguments and whose conclusion is ensures plus the user-level specification (Section 4, p.7).
  6. Prove that the autogenerated specification implies the user specification; Lean checks both generated and handwritten proofs (Section 4, p.8).

The paper states: “Our verifier uses Dijkstra’s weakest preconditions to read off a specification.” (Section 4, p.8) Verus form (Inference): generate a spec fn contract and proof skeleton from MIR/AST, then require a human or agent to supply a proof that the generated contract implies the intended one. Verus requires/ensures replace Lean predicates, but generated proof code must use valid Verus syntax and remain checked by Verus.

technique 3: modular recursion, loops, and control-flow invariants

What it is: use user specifications at recursive calls and block-entry invariants for loops, proving partial correctness conditional on a terminating execution. When to use it: use it when code has cycles and the machine certificate already establishes termination.

Steps (Section 4, pp.9–10):

  1. Replace the default recursive user specification with True before the autogenerated play-by-play specification (Section 4, p.9).
  2. Characterize recursive calls with the user specification and prove the autogenerated characterization implies the desired one under the downstream-call assumption (Section 4, p.9).
  3. Build a control-flow graph and split code into basic blocks at function starts, labels, jumps, returns, and label flows (Section 4, p.10).
  4. Give each multiply-entered block its own specification; handle topological-sort cycles like recursive calls (Section 4, p.10).
  5. Prove an invariant at first entry and preservation on re-entry (Section 4, p.10).

The paper says: “Verification of the full user specification then requires showing that the invariant holds at the first entry point and that it is maintained on re-entry.” (Section 4, p.10) Verus form (Inference): use while loop invariants and requires/ensures on recursive proof fns or executable functions; unlike the paper’s partial-correctness argument, Verus termination obligations may need explicit decreases clauses for executable recursion/loops.

technique 4: memory, pointers, and range-check hypotheses

What it is: model frame-pointer and allocation-pointer addressing, preserve address identities across calls, and thread range-check assumptions through specifications. When to use it: use it for a low-level language whose arithmetic values are finite-field elements but whose intended contracts mention bounded integers.

Steps (Section 5, pp.10–12):

  1. Track compiler flow information for allocation-pointer offsets; reject or revise code when an address is “revoked” (Section 5, pp.10–11).
  2. Prove identities such as ap' = ap + 3 and use them as rewrite rules for memory references (Section 5, p.11).
  3. Represent bounded integer casts with range-check predicates and pass a range-check pointer through calls (Section 5, pp.11–12).
  4. Combine hypotheses so the top-level specification covers all recursive calls (Section 5, p.12).

Inference: in Verus, model pointer/ownership facts with Rust references and explicit sequence/map specifications; use arithmetic bounds in requires and ensures. Finite-field-to-integer cast reasoning must be stated in the Verus model; it is not supplied by Rust types.

technique 5: layered mathematical contracts for cryptographic code

What it is: verify concrete field-element representations against abstract integer and elliptic-curve specifications. When to use it: use layered representations when implementation arithmetic uses limbs but correctness is stated over a mathematical group.

Steps (Section 6, pp.14–16):

  1. Represent each field element as three bounded limbs (BigInt3) and define the corresponding integer value (Section 6, p.14).
  2. Define bounded point data linking limbs to curve points and prove curve membership or the zero-point alternative (Section 6, p.15).
  3. State preconditions for limb bounds and postconditions that return bounded representations (Section 6, pp.14–15).
  4. Verify scalar multiplication with loop invariants and the precomputed-multiple optimization (Section 6, p.16).
  5. Compose those lemmas into ECDSA public-key recovery, proving the returned point equals the mathematical expression (Section 7, pp.16–17).

Evidence: the secp256k1 signature case used about 800 lines of CairoZero, 3,200 lines of specification, and 7,500 lines of autogenerated Lean proofs; the dependency chain had 24 functions and about 900 assembly field elements (Section 7, p.18). Verification found an error in parameter v that could make a valid signature be reported invalid; it was fixed in the next release (Section 7, p.18).

Verus form (Inference): use Rust structs for limbs and spec fn mappings to mathematical integers/curve points, with proof fns establishing representation invariants. Cryptographic arithmetic remains domain-specific; the paper’s group-library proofs must be replaced by vstd or project lemmas.

technique 6: verify read-write behavior over read-only memory

What it is: represent dictionary accesses as (key, previous, next) triples and verify a squashed list with one initial/final entry per key. When to use it: use it when the execution substrate is append-only/read-only but the source abstraction needs updates.

Steps (Section 8, pp.18–20):

  1. Require consecutive accesses for a key to satisfy next = next_access.previous (Section 8, p.18).
  2. Guess a sorted list of keys and sorted access lists as witness data (Section 8, p.20).
  3. Check key-set equality, sortedness, and that each squashed entry uses the first previous and last next value (Section 8, pp.19–20).
  4. Bound the trace length Îș < 2^50 so finite-field addresses cannot wrap and reuse an entry (Section 8, p.20).
  5. Prove the checks imply the full spec_squash_dict contract (Section 8, p.20).

Verus form (Inference): model accesses as a Seq of records, state a permutation/key-set relation and per-key first/last invariant, and prove the scan loop invariant. The witness is untrusted data; Verus proofs must establish that it satisfies the contract.

what is proved, measured, and trusted

The trusted base includes Lean’s small kernel, the formal CPU/assembly semantics, compiler-extracted data, and STARK cryptographic assumptions. The paper explicitly says: “We do not verify the STARK protocol itself” (Section 2, p.4); prior work verified its execution-trace encoding. The method can fail on arbitrary “spaghetti code”: the tooling is designed for regular control-flow graphs and otherwise fails (Section 9, p.21). Compilation of all Lean files takes a few minutes and user specifications alone less than two minutes on an ordinary desktop (Section 9, p.22).

Inference: the direct VL lesson is a staged pipeline: generated low-level contracts, human/agent high-level contracts, and a kernel-checked implication proof. This reduces compiler-modeling cost but leaves specification adequacy as the principal product threat; a Verus proof establishes the stated contract, not the unstated intent. What the paper already accomplishes—machine-level semantics, generated proof obligations, modular contracts, and production cryptographic case studies—should not be redone as a generic idea; VL should adapt it to Rust MIR, ownership, and Verus’s SMT-backed proof model.

techniques for the catalog

  • machine-to-proof semantics: define a small-step machine and prove instruction transition lemmas
  • generated weakest-precondition contracts: extract naive specs and proof code from compiler data
  • modular cyclic control flow: use recursive-call specs and block-entry invariants
  • range-check threading: carry boundedness hypotheses through calls and address rewrites
  • layered crypto refinement: connect limb representations to abstract field/group properties
  • read-only dictionary squash: verify append-only access histories via sorted witnesses and invariants Checked 2026-10-14 against the paper by a Codex agent: audit record avigad2025proof; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: