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 desired 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. Inference: 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, pp.3–4).
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 constraints on the fixed memory assignment (Section 3, p.6).
5. Let Lean rewriting and numeric evaluation step through concrete instruction blocks (Section 3, p.6).

Inference: a possible Verus adaptation is an explicit operational model over immutable memory and register states, with proofs about transitions and bounded traces. Connecting that model to compiled Rust would require a separate justification.

technique 2: generate specifications and proofs with weakest preconditions

What it is: read off a naive specification from high-level CairoZero instructions using weakest preconditions, then generate a proof by stepping through the corresponding assembly instructions. Inference: 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. Use existing compiler data for identifiers and add verification-mode hooks for compound assertions and their 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.9).
5. Generate a theorem whose hypotheses describe code/dependencies/arguments and whose conclusion is ensures with register-restoration and range-check conditions for the user specification (Section 4, pp.7–8).
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 [12] to read off a specification.” (Section 4, p.8) Inference: a possible Verus adaptation is to generate contracts and proof code from a Rust intermediate representation, then prove that the generated contracts imply the intended ones. This is a proposed adaptation, not a result of the paper.

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. Inference: use it when code has cycles and the machine certificate already establishes termination.

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

1. Initialize the recursive function’s user specification to a trivially true predicate and place it before the autogenerated 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, pp.9–10).
3. Prove correctness by induction on a bound on the length of halting executions; build a control-flow graph and split code into basic blocks at function starts, labels, jumps, returns, and label flows (Section 4, pp.9–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) Inference: a possible Verus adaptation is to use loop invariants and recursive function contracts. Termination requirements would need to be checked separately for that adaptation.

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. Inference: 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. Use compiler flow information for allocation-pointer offsets; the compiler reports a revoked reference when it cannot determine an allocation-pointer-based variable’s address (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 range-check hypotheses so the top-level specification covers all recursive calls (Section 5, p.11).
5. Bound the number of range-checked elements µ by the execution-step parameter κ to prevent finite-field wraparound (Section 5, p.12).

Evidence: “Our verification tool claims and proves the relevant identities while stepping through the code, and uses those identities as rewriting rules when verifying assertions.” (Section 5, p.11)

Inference: a possible Verus adaptation is to state address and arithmetic bounds explicitly and prove the finite-field-to-integer correspondence.

technique 5: layered mathematical contracts for cryptographic code

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

Steps (Sections 6–7, pp.14–17):

1. Represent each secp-field element with three Cairo-field elements (BigInt3), link these to bounded integers, and interpret their base-2^86 value modulo the secp prime (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; for secp256r1, account for the table of the first sixteen multiples of the input point and check that the scalar represents a 256-bit unsigned integer (Section 6, p.16).
5. Verify ECDSA public-key recovery under its input-representation preconditions: the output represents Q = −u1 · G + u2 · (r, y), with the specified modular relations for u1 and u2 and parity condition for y (Section 7, pp.16–17).

Evidence: “The elliptic curve operations and the signature validation procedure run about 800 lines of CairoZero code and our specification files run about 3,200 lines of Lean code, on top of about 150 lines in our definition of the elliptic curve group.” “The dependency chain of recover_public_key consists of 24 CairoZero functions, which compile to about 900 lines of assembly code, i.e. 900 field elements.” “Our autogenerated correctness proofs run about 7,500 lines of Lean code.” (Section 7, p.18) These figures concern the secp256k1 operations and signature validation.

The paper also reports: “The error, which does not allow the prover to fake a signature but does allow it to claim that a valid signature is invalid, was fixed in the next CairoZero release.” This concerns parameter v in recover_public_key (Section 7, p.18).

Inference: a possible Verus adaptation is to use limb structures, mathematical mappings to integers and curve points, and proofs of representation invariants. The required mathematical library would need separate investigation.

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. Inference: 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 accessed keys and, for each key, a sorted list of locations of its accesses as witness data (Section 8, p.20).
3. Check key and access lists, establish an injection into the input entries, and check equal total counts to obtain a bijection; check that each squashed entry uses the first previous and last next value (Section 8, p.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 spec_squash_dict: sorted output keys, equal input/output key sets, and a consistent access history summarized by each output entry (Section 8, pp.19–20).

Evidence: “The fact that we can show that the value of n asserted to exist in the specification is bounded by κ provides that guarantee.” Here the guarantee is that access-location lists do not wrap around the finite field and reuse an input entry (Section 8, p.20).

Inference: a possible Verus adaptation is to model an access sequence, prove per-key consistency and first/last-value properties, and verify coverage of all input accesses by the witness lists.

what is proved, measured, and trusted

The paper states: “all our theorems are stated in the context of a precise axiomatic foundation and the proofs are checked by a small trusted kernel, for which independent reference checkers are available.” (Section 9, p.21) It also says: “We do not verify the STARK protocol itself, but, in prior work [4], we have verified the encoding scheme for Cairo execution traces, in other words, the reduction of the execution claim to the polynomial equations.” (Section 2, p.4)

Inference: the result relies on the foundational proof checker and on the adequacy of the CPU model and user specifications. Applying it to actual compiled code also requires matching the generated code description to the deployed numeric instructions. The paper explains that users can evaluate the Lean assembly definitions and compare their numeric values to the compiler output (Section 3, p.6): “Our soundness proofs start with the assumption that these values are stored in memory and that the program counter is set accordingly.” Compiler-extracted data is used to construct proofs checked by Lean; the paper does not identify that data as an additional trusted proof oracle.

The control-flow limitation is explicit: “Our verification tooling is designed to work on regular control flow graphs, and will simply fail otherwise.” (Section 9, p.21) Timing concerns the signature application: “For the application described in Section 7, compiling and checking all the files in Lean requires only a few minutes on an ordinary desktop.” “Compiling and checking the specification files alone, with the user specifications and correctness proofs, takes less than two minutes from scratch.” (Section 9, p.22)

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

Last edited: 2026-10-19