A Verified Algebraic Representation of Cairo Program Execution

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

what the paper proves or measures

The paper formalizes the algebraic intermediate representation (AIR) used by the Cairo STARK prover and proves that satisfying the AIR constraints implies a valid Cairo execution trace. The abstract states: “Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.” (Abstract, p. 1)

The result is an implication theorem, not a proof of the cryptographic protocol or a proof that every Cairo program meets a high-level specification. The authors state: “This paper reports on the successful completion of the second task, a fully verified proof that data satisfying the AIR implies the corresponding computational claim.” (Introduction, p. 2) The AIR is generated directly from the Cairo implementation, so the formalization can be rerun as the production encoding changes.

technique 1: formalize the machine semantics before the algebraic encoding

what it is: define Cairo instructions, registers, read-only memory, and a nondeterministic next-state relation in Lean. The machine state has pc, ap, and fp in a finite field; an instruction has three 16-bit offsets and 15 flags. A state transition is valid when the memory at pc encodes an instruction and the instruction’s next registers and assertions agree.

how to do it:

1. define instruction with off_dst, off_op0, off_op1, and flags bitvectors, and define register_state with pc, ap, and fp (Section 3, pp. 3–4)
2. define instruction-specific option-valued functions for next pc, ap, and fp; none represents undefined behavior (Section 3, p. 4)
3. define instruction.next_state as agreement of these option results plus the instruction’s assertions, then define next_state by existentially selecting the instruction stored at mem s.pc (Section 3, p. 4)
4. prove helper lemmas for each flag case. The paper’s next_fp definition maps call to ap+2, return to the decoded destination, ordinary instructions to unchanged fp, and invalid flag combinations to none (Section 3, p. 4)
5. use the resulting relation as the target semantics for the AIR correctness theorem.

The model deliberately uses read-only memory. The paper says: “The fact that memory is read only means that we do not need to verify claims about memory management.” (Section 3, p. 3) It also does not prove high-level termination; the trace certificate supplies a finite claimed run.

Verus form: Inference: define a Rust ghost state struct and a spec fn next_state relation. Use requires for finite-field and well-formed-instruction assumptions, ensures for each deterministic flag branch, and a proof function for the existential instruction step. Keep the relation nondeterministic where the Cairo semantics allows undefined instructions. Verus can model bitvectors and finite fields only through suitable libraries or mathematical abstractions; those abstractions become trusted assumptions unless separately proved.

evidence and limits: the CPU file is reported as less than 200 lines, but the paper provides no proof-time or defect-count benchmark. The formal theorem depends on the CPU semantics matching the intended Cairo machine and on Lean’s foundations.

technique 2: compile trace meaning into AIR polynomial constraints

what it is: encode a trace of T+1 register states, instruction data, memory accesses, and auxiliary values in a 16(T+1) × 25 field array. Each constraint is a polynomial equation required on a specified set of rows. The main correctness theorem says that a satisfying table, under public assumptions and nonexceptional interaction elements, yields a Cairo execution trace.

how to do it:

1. agree on input data: trace length, initial and final pc/ap, and a partial memory map m* (Section 4, pp. 6–7)
2. generate the polynomial constraints from the Cairo implementation. The autogenerated file constraints_autogen.lean is also used to produce verifier code (Section 4, p. 7)
3. split constraints into decoding, operand and register updates, opcodes, memory, range checks, public memory, and initial/final conditions (Section 5, p. 9)
4. prove in Lean that the constraints imply an execution trace. Glue the whitepaper layout to the autogenerated layout with glue.lean (Section 4, p. 7)
5. state the probabilistic side condition using bad sets. If interaction elements avoid bad1, bad2, and bad3, and the field and trace assumptions hold, conclude existence of a memory extension and a trace of T=(T'−1)/16 steps (Section 5, pp. 8–9).

The theorem bounds the bad sets by (T'/2)^2, T'/2, and T' respectively (Section 5, p. 8). The bounds are symbolic in the paper; no measured field size or empirical failure probability is reported. The STARK protocol and its hash security are treated as a black box, as stated: “For the purposes of this paper, the details of the STARK protocol and the precise complexity and probabilistic claims can be treated as a black box.” (Section 4, p. 6)

Verus form: Inference: represent each polynomial constraint as a spec fn over a ghost trace and prove local-to-global lemmas over row indices. Use invariant clauses on loops that scan rows, assert for polynomial equalities, and ensures for the reconstructed state relation. Do not place ensures on a spec fn; the executable checker and cryptographic assumptions remain external to the Verus proof.

technique 3: decode packed instructions with finite-field identities

what it is: recover a unique Cairo instruction from field elements encoding offsets and flags. Offsets are shifted into [0,2^16). The flags are represented by cumulative values f~i; the identity fi = f~i − 2 f~i+1 recovers each bit. The packed instruction is a base-2^16 expression over the three offsets and flag word (Section 7, pp. 10–11).

how to do it:

1. assume field constraints that each recovered bit is 0 or 1 and that the final cumulative flag is zero (Section 7, p. 10)
2. define the_instruction from the constrained field elements
3. prove inst_eq, showing the field element equals the cast of the_instruction.to_nat, and prove component-cast lemmas such as off_dst_tilde_eq (Section 7, p. 11)
4. prove inst_unique, which establishes that no two instructions share an encoding under the constraints (Section 7, p. 11)
5. use the decoded instruction in the next-state proof.

Verus form: Inference: encode the bit and range conditions as ghost predicates and prove uniqueness by arithmetic lemmas over a bounded integer representation. Rust bitvector operations can execute, but the field-cast correspondence needs a separate specification lemma. The Cairo paper’s uniqueness is stronger than the final trace-existence theorem and is useful when proving a particular program’s behavior.

evidence and limits: uniqueness is independently important but “is not required for the correctness theorem in Figure 1” (Section 7, p. 11). The field characteristic assumption, at least 2^63, is essential for unique instruction representation (Sections 3 and 5, pp. 3, 8).

technique 4: use polynomial fingerprints for permutations

what it is: replace a global sequence-equality or permutation claim with a polynomial identity checked at a random interaction element. If two sequences differ, their difference polynomial has at most n roots, so a random field point catches the mismatch except on a small exceptional set.

how to do it:

1. define p(x)=∏(x−ai) and p'(x)=∏(x−a'i) for the original and reordered sequences (Section 9, p. 13)
2. prove that equality at a point outside exceptional_set(a,b) implies equality of the polynomials using all_eq_of_not_mem_exceptional_set
3. prove the exceptional set cardinality bound card_exceptional_set_le ≤ fintype.card n (Section 9, p. 13)
4. use the STARK hash output as the interaction element and put the resulting equality into the AIR constraints.

Verus form: Inference: model the fingerprint as a ghost fold over a finite sequence and prove the exceptional-root bound with a finite-field polynomial library. The random/hash sampling argument is outside Verus unless the cryptographic model is formalized; state it as an explicit assumption in the top-level contract.

evidence and limits: the theorem’s bad sets are existentially quantified and need only be small; the paper does not provide a concrete probability estimate for a deployed field. The method requires the field to be much larger than the sequence length.

technique 5: range-check and memory-consistency encodings

range checks: sort or permute offset values into a sequence from rc_min to rc_max; constrain adjacent values to stay equal or increase by one, and constrain endpoints to the declared minimum and maximum (Section 10, p. 14). The permutation fingerprint then proves every original offset occurs in that interval, yielding off_op0_tilde and analogous in-range lemmas.

memory: pair each accessed address with its value, permute the pairs into an ordered sequence, require adjacent addresses to be equal or increase by one, and require equal adjacent addresses to have equal values (Section 11, pp. 15–16). To bind a partial assignment m* without adding a constraint per public entry, add dummy (0,0) pairs and replace the final fingerprint condition with a product over mem_dom mem_star (Section 11, p. 16). Define the reconstructed memory mem by selecting the unique value associated with an address and return zero when absent.

Verus form: Inference: use ghost sequences and sortedness/adjacency invariants for range and memory proofs. A Verus invariant can maintain uniqueness of equal addresses and consistency with the partial map; a final lemma can show every CPU access returns its encoded value. The hash fingerprint still needs an explicit cryptographic assumption.

evidence and limits: these constraints prove consistency of the formal memory extension, not memory safety of arbitrary Cairo programs. The model’s read-only memory and finite trace assumptions remain in force.

trusted boundary, contradictions, and VL implications

The formal proof checks the CPU semantics, generated constraints, glue, finite-field facts, and Lean’s proof kernel. The trusted boundary also includes the code generator that emits constraints_autogen.lean, the production verifier’s use of the same polynomials, the STARK protocol and hash assumptions, the correctness of the Cairo whitepaper formalization, and the claim that a high-level program has the intended specification. The authors list these directly in Section 5: “What needs to be trusted?”

The paper’s numerical bounds are symbolic, so there is no denominator-based experimental success rate to reconcile. The 16(T+1) × 25 array and T=(T'−1)/16 relation are definitions of the encoding, not measurements (Section 4, p. 7). Inference: a VL implementation should copy the architecture of a small executable semantics plus generated constraints and a proved glue layer, but it should not treat a Verus proof of algebraic constraints as a proof of the cryptographic verifier or of application-level intent. Threat to agent-written verified Rust is high where the specification-to-encoding boundary is generated or opaque: a wrong generator can produce a consistently proved but wrong algebraic model unless generation and correspondence are checked.

What VL should not redo (Inference): the polynomial fingerprint pattern for proving permutations, bounded bit decoding, and memory consistency are established techniques. A useful adaptation would make the generated Rust/Verus constraints auditable and prove the generator’s correspondence to the executable verifier.

techniques for the catalog

• machine semantics first — define instructions, registers, memory, and next-state relations before proving the encoding
• AIR-to-execution theorem — prove that satisfying generated polynomial constraints yields a valid Cairo trace
• packed-instruction decoding — recover unique bitvector instructions from finite-field encodings
• polynomial permutation fingerprints — reduce sequence permutation claims to random evaluations outside bounded bad sets
• range-check encoding — prove integer intervals with sorted adjacency and permutation constraints
• memory-consistency encoding — reconstruct a read-only memory map from permuted address/value pairs Checked 2026-10-14 against the paper by a Codex agent: audit record avigad2022verified; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15