Review: noir-lang/noir#13787 — Lean FV proofs for ACIR integer circuits

review.md

Review: noir-lang/noir#13787 — feat(fv): machine-checked proofs that Noir's integer circuits are not underconstrained

AztecBot · cb/acir-lean-gadget-proofs → master · head 7c47f02 · 62 files, +25379 −1 · OPEN, REVIEW_REQUIRED · CI 137 passing, 0 failing, 2 skipped · behind base by 31 commits · Linear: none Reviewed 2026-09-30.

At a glance

This PR adds no compiler behavior change — only a new, CI-gated Lean proof that specific ACIR circuits are sound, plus the Rust/script glue that pins Lean's model to the real compiler. Nothing here can silently miscompile Noir code; the risk is narrower — that the proof claims more, or less, than it actually establishes, or that its own safety net has a gap.

• No blockers. Everything found is minor: small gaps in the enforcement scripts and CI, not in the compiler or in what's already proved.
• Worth the author's attention before merge: B1 (a real, if unexploited, hole in the "Templates need no review" guarantee) and B2 (one claim is missing the non-vacuity check every sibling claim has).
• Design: D1–D2 point at duplicated/divergent "meaning" definitions in the trusted Spec/ layer, which is exactly the part this project depends on humans getting right; D2 is a real, if minor, gap in what's proved (accepts a zero-divisor result of 0 in some claims).
• No open discussion threads or unaddressed review asks.

1. What this PR does, and why

A Noir program compiles to a circuit: a list of constraints a prover must satisfy. An underconstrained circuit accepts more than the honest answer — a cheating prover can find values that satisfy every constraint while producing a wrong result, and the verifier still accepts. Ordinary tests can't catch this, because tests only feed the circuit honest values.

This PR adds mathematical proofs, checked by the Lean proof assistant, that specific circuits nargo compile ships cannot be cheated this way: for every witness assignment that satisfies the circuit, the values it encodes are the right ones. The proofs cover the integer gadgets inside AcirContext (division, truncation, comparison, for widths 8–128), signed div/mod/lt on i8–i64, whole compiled functions before and after the ACVM optimizer, and 125 of the 127 scalar programs in test_programs/execution_success. They run in CI and fail if the compiler starts emitting a circuit the proofs no longer cover or no longer prove.

Before / after. Before this PR, a regression like #7895 (the truncation gadget's constraint q ≤ q0 was dropped) could only be caught by a test with the specific forged witness in hand. After this PR, fv/acir_lean/AcirLean/Examples/Bug7895.lean constructs that exact forged witness once, proves it satisfies the buggy circuit but not the gadget's own soundness claim, and Check.lean requires AllClaims to hold — so removing the bound again would make the PR that removes it fail CI, without anyone having to write a new test.

What to keep in mind while reviewing.

• The proofs (AcirLean/Proofs/) are checked by Lean and the pinned data (AcirLean/Templates/) is byte-compared to compiler output — neither can silently be wrong. The part that can be silently wrong is the hand-written meaning in AcirLean/Spec/ (~935 lines) and the Rust/CI glue that ties it to the real compiler: that's the actual review surface, and it's what this review concentrates on.
• What's not covered, by the PR's own account: arrays, memory ops, cross-function calls, black boxes, and anything before ACIR (SSA passes, frontend). Only soundness is proved, not completeness — a circuit that wrongly rejects some honest input would still pass.
• The author's own PR comment flags a real cost: adding a new test program or changing a covered gadget needs a regeneration script run (just fv-regen), which is friction for future PRs.

2. How it does it

Three pieces work together, in one direction only: the compiler never depends on Lean, only CI does. First, a small hand-reviewed Lean file says what each ACIR opcode and SSA instruction means (AssertZero is "equals zero", RANGE is "below 2^k", division rounds toward zero, and so on) and states the one proposition, AllClaims, that is the whole promise. Second, two Rust test files print the compiler's actual output — gadget constraints, whole-function ACIR, optimized circuits, real test-program artifacts — as plain text, and Lean prints its own copy of the same data in the same text format; a golden-file byte comparison is the only thing tying the two together, so Lean is always reasoning about exactly what the compiler emits, never a hand transcription. Third, the bulk of the new code is machine-checked Lean proof that AllClaims follows from that pinned data; nothing there needs a human reader, because a wrong or incomplete proof simply doesn't compile.

Part	Job	Lives in
The trusted meaning	Defines what an opcode/SSA instruction means and the final claim	fv/acir_lean/AcirLean/Spec/
The compiler↔Lean pin	Prints compiler output as text on both sides; CI fails on any byte difference	compiler/noirc_evaluator/src/acir/acir_context/fv_templates.rs, fv_semantics.rs, fv/acir_lean/Emit*.lean
The proofs	Proves AllClaims from the pinned data; Lean-checked, no review needed	fv/acir_lean/AcirLean/Proofs/
The generated data	The actual circuits/SSA, produced by scripts from real compiler output	fv/acir_lean/AcirLean/Templates/, fv/acir_lean/scripts/gen_*.py
The gate	Runs every check (build, escape-hatch grep, golden diffs, REVIEWING.md sync, axiom check)	fv/acir_lean/scripts/check.sh, Check.lean
CI wiring	Runs the gate on fv/** changes; separately rebuilds and diffs test-program data on every PR	.github/workflows/fv-lean.yml, .github/workflows/fv-test-programs.yml

Mechanical: mod.rs wires in the two new #[cfg(test)] modules; tests/mod.rs factors try_ssa_to_acir to expose try_ssa_value_to_acir for reuse on already-built SSA; justfile gains fv-check/fv-regen/fv-regen-all; CLAUDE.md gains a pointer to fv/acir_lean/CLAUDE.md and the rule that a Spec/ change must update REVIEWING.md in the same PR.

Breaking or externally visible changes. None found — no compiler behavior changes; only new test modules, new CI workflows, and a new top-level fv/ directory.

Tests. The PR's own test plan mutates the compiler in several ways (dropping the q ≤ q0 truncation bound, dropping a range-optimizer check, dropping the signed MIN / -1 check, deleting single constraints from the 125 proved circuits) and confirms each failure is caught. Left untested here, by design: correctness of the hand-written Spec/ meaning itself is checked only against a fixed grid of ~11,000 interpreter calls, not exhaustively.

3. Bugs

All four findings are minor: gaps in the enforcement machinery, not wrong proofs or a miscompile. Verified against the code; none were refuted.

B1. A plain def in an unreviewed Templates file can shadow a name the trusted claims rely on — minor, confidence medium

fv/acir_lean/scripts/check.sh:41 · fv/acir_lean/AcirLean/Spec/Claims.lean:166 at head · introduced by this PR

The whole "no review needed" promise for AcirLean/Templates/ rests on it holding only data. Claims.lean:166,168 name Int.tdiv/Int.tmod unqualified, inside namespace AcirLean, and every Templates file is imported into that same namespace. Lean resolves an unqualified name in the current namespace before falling back to the root, so a Templates file containing a plain def Int.tdiv (a b : ℤ) : ℤ := … would declare AcirLean.Int.tdiv and silently become what the signed-division claim is proved against — no golden file prints Int.tdiv, so nothing would catch it.

The guard meant to prevent exactly this, check.sh's keyword grep, only matches at the start of a line (^\s*(@\[|instance|…|theorem|…)\b), so def passes as intended, but so does anything the regex doesn't anchor for: noncomputable instance …, private instance …, protected theorem …, or keywords missing from the list like unif_hint. Nothing is wrong today — no Templates file defines Int.tdiv/Int.tmod or uses one of these prefixes — but the safety net has a hole where the PR's own docs say there is none. Fix by writing _root_.Int.tdiv/_root_.Int.tmod in Claims.lean, or by making the Templates guard an allowlist (def/abbrev only, no other prefix) instead of a keyword blocklist.

B2. The test-program claim is the one claim in AllClaims with no non-vacuity check — minor, confidence high

fv/acir_lean/AcirLean/Spec/Claims.lean:171 at head · introduced by this PR

The module doc and the AllClaims docstring both say every claim is paired with a non-vacuity check "so the assumptions cannot be contradictory," and every other conjunct in AllClaims (lines 132–169) carries Satisfiable, SatisfiableFunction, or AllHold e.assignment. The last one doesn't:

(∀ e ∈ testPrograms, e.name ∉ uncoveredPrograms → SoundFunction e.fn (ProgramSpec e.prog))

If a shipped circuit for one of the 125 covered test programs ever contained a contradiction (for example an optimizer bug emitting zero 1*[]), SoundFunction would hold of it vacuously, and the claim would count that program as covered when it proves nothing about it. Add ∧ SatisfiableFunction e.fn to this conjunct, or say explicitly in the doc comment that this one claim is the exception.

B3. The forbidden-pattern grep never scans lakefile.toml — minor, confidence medium

fv/acir_lean/scripts/check.sh:27 at head · introduced by this PR

check.sh greps AcirLean AcirLean.lean Check.lean EmitTemplates.lean EmitPrograms.lean EmitSemantics.lean for escape hatches like skipKernelTC and debug.*, but never lakefile.toml. A [leanOptions] entry such as debug.skipKernelTC = true there would weaken kernel checking for every module lake build compiles, and #print axioms in Check.lean wouldn't reveal it. The current lakefile.toml is clean, so nothing is exploited today. Add it to the grep, or reject any leanOptions/moreLeanArgs table in it.

B4. The FV Lean workflow pipes an unpinned installer from a mutable ref into sh — minor, confidence high

.github/workflows/fv-lean.yml:37 at head · introduced by this PR

curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none

This fetches and executes whatever is on elan's master branch at run time, on both pull_request and push-to-master triggers (the workflow's own actions/checkout step, two lines above, is pinned to a commit SHA per this repo's convention). Impact is limited today — permissions: {} at the workflow level and contents: read on the job, no secrets in the job — but it's the one script-execution step in either new workflow that isn't pinned. Pin to an elan release tag or commit SHA. (No other injection issue: neither new workflow interpolates untrusted ${{ }} values into a run: step; the only interpolations feed concurrency.group and save-if.)

While you are here (pre-existing, not introduced by this PR):

• compiler/noirc_evaluator/src/ssa/ir/instruction/binary.rs:354: truncate_field is wrong for bit_size > 256 when bit_size isn't a multiple of 8 — take(num_bytes) caps at 32 bytes but the partial-byte mask still applies to the most significant of those bytes, so truncating to, say, 257 bits clears real high bits instead of keeping them. Confirmed present byte-for-byte at base. The compiler never emits such a width today and this PR's own semantics grid tops out at 254 bits, so it doesn't affect anything proved here — noted only because it surfaced while reading the file this PR pins against.

4. Design and simplification

D1. Lean has two canonicalizers of ACIR constraints, and only one is proved to preserve meaning

fv/acir_lean/AcirLean/Spec/Pin.lean:53 · fv/acir_lean/AcirLean/Proofs/Canon.lean:38

The same term-sort/filter/sign-flip logic exists three times: Rust's canonical(), the reviewed Spec/Pin.lean's Opcode.render, and the unreviewed Proofs/Canon.lean's Opcode.canon — the last one alone comes with a proof (canon_sat) that it preserves what the constraint means. A reviewer of render has to check that sort/filter/sign-flip by eye; Lean already proved the equivalent for canon. The two Lean copies also disagree in one respect — Rust merges terms that share a witness list before dropping zero terms, neither Lean copy does — which today can only produce a (fail-closed) golden mismatch, but the doc comments describe the two forms as one and Pin.lean's doesn't mention merging at all.

Move canon (a plain definition, no theorems) into Spec/, keep canon_sat in Proofs/, and make render print c.canon rather than repeat its logic — that puts the "does this preserve meaning" question under a machine-checked proof instead of a second by-eye reading, at the cost of moving insertBy/isort/a modulus helper into the reviewed file.

D2. TRADEOFF: the SSA div claims accept a zero-divisor result of 0, understating what the corresponding gadget claims already prove

fv/acir_lean/AcirLean/Spec/Ssa.lean:53 · fv/acir_lean/AcirLean/Spec/Claims.lean:146

Spec/ models "what SSA means" three separate times — Programs.lean (corpus programs, over ℕ), Ssa.lean (the signed-lt subset, over ℕ), Programs2.lean (the full scalar subset, over F) — and only the last is checked against the real interpreter by fv_semantics.rs. The other two are trusted by eye, and they already disagree with each other and with the shipped circuit's actual behavior: Ssa.lean's SsaBinOp.eval .div a b = a / b is plain ℕ division, so a divisor of 0 evaluates to 0, while Programs.lean's corpus semantics and Programs2.lean's interpreter model both fail on a zero divisor. Since acirGenDiv/shippedDiv (Claims.lean:146,156) are stated with Computes2 n (SsaBinOp.eval .div), those claims accept a circuit that returns 0 for b = 0 instead of rejecting it — even though the shipped circuit (confirmed in templates.golden's 1 - b·inv = 0 constraint) does reject it. This isn't a false claim, just a weaker one than the rest of the project states.

Folding Ssa.lean/Programs.lean into Programs2.lean (adding xor, expressing the signed-lt and corpus programs as Program, stating the div/lt/corpus claims with ProgramSpec) would put every SSA meaning under the one interpreter-checked model and close this gap as a side effect.

• Lost: this is strictly more work than a pure refactor — the div claims become stronger (need a new proof that acirGenDiv/shippedDiv reject b = 0, at 5 widths each), the signed-lt claim (ComputesSignedLt) needs restating over Option/F instead of a total ℕ equation, and the golden rendering for signedLtSsa needs to still come out byte-identical.
• Who hits it: the author only, as implementation work — no reviewer- or compiler-facing behavior changes either way. A cheaper partial fix that doesn't require the merge: change SsaBinOp.eval to return Option and fail on b = 0, so the three models at least stop disagreeing with each other.

D3. fv_templates.rs's emitted() pastes the same width list and the same SSA source twice

compiler/noirc_evaluator/src/acir/acir_context/fv_templates.rs:247

The flat, one-section-per-stage shape is right — each section pins a genuinely distinct gadget or pipeline stage. But [8, 16, 32, 64, 128] is written out 13 times where Lean has one pinnedWidths, and the div/lt/truncate SSA source strings are pasted twice each (once for the acir_* section, once for the matching shipped_* section) — editing one copy and not the other would silently break "the same function before and after optimize". Pulling the width list and the three SSA-source builders into shared constants/closures keeps the golden output identical while removing that trap; Spec/Pin.lean's renderAll has the same opportunity (it defines a sec helper but only uses it for four of its sections).

D4. Three near-duplicate "print a circuit" functions disagree on what inputs means, harmlessly today

compiler/noirc_evaluator/src/acir/acir_context/fv_templates.rs:147 · fv_templates.rs:349

shipped_of_ssa prints only private_parameters as inputs; dump_artifacts prints private and public parameters, sorted, matching Spec/Semantics.lean's doc ("private and public, in witness order"). This only doesn't matter because every Ssa::from_str test function in this file happens to have no public parameters — a reader has to notice the difference and work out why it's safe. A single circuit_lines helper matching the Lean doc, shared by both, removes the need to notice.

D5. A few names a newcomer would misread

fv/acir_lean/AcirLean/Spec/Programs2.lean:124

• Programs.lean holds the corpus types; the general scalar-program model is in Programs2.lean — the "2" reads as "newer copy" rather than describing either file (D2's merge would remove the question; short of that, Spec/Corpus.lean / Spec/SsaSemantics.lean would read better).
• truncate_field names two different things: a Rust test helper around AcirContext::truncate_var in fv_templates.rs, and the interpreter's own low-bits function in Programs2.lean. The gadget already has a distinct Lean name (truncateGadget); renaming the Rust helper to truncate_var would match the existing div_var/more_than_eq convention.
• The PR states a Rust↔Lean naming rule ("Lean names follow Rust's ACIR where there is a counterpart") that the SSA types don't follow: Rust's one NumericType has two different Lean spellings (IntType.u/.i in Ssa.lean, ValueType.uint/.sint/.field in Programs2.lean), and Rust's one BinaryOp has three (CorpusOp, SsaBinOp, BinaryOp).

D6. Regenerating the corpus means scraping a panic message with sed; regenerating test programs has a real script

fv/acir_lean/README.md:250

Test-program regeneration has a real path: an #[ignore]d dump_artifacts test → gen_programs.py → just fv-regen. Corpus regeneration has none — the README instead pipes cargo test output through three sed commands to pull the emitted text out of a test-failure panic message, and there's no just recipe for it. That panic message (integer_gadgets_match_lean_templates's failure text) also always says "Update AcirLean/Templates/Gadgets.lean", which is the wrong instruction when it's actually the corpus, shipped_*, or acir_* section that changed. Since any change to shipped div/lt circuits or to ACVM solving can change the corpus, this is the regeneration path a compiler developer is most likely to need and least likely to have documented for them. Adding an #[ignore]d dump_emitted test (mirroring dump_artifacts) plus a just fv-regen-corpus recipe would give it the same shape as the test-program path.

D7. CLAUDE.md's formal-verification section is written for people already inside fv/

CLAUDE.md:79 · fv/acir_lean/CLAUDE.md:8

The top-level CLAUDE.md section says the one rule reaching beyond fv/ is "keep REVIEWING.md in sync" — but that rule only fires on a Spec/ edit, which is already inside fv/. The rule a compiler developer working on, say, AcirContext's gadgets, expand_signed_math, the ACVM optimizer, or the SSA interpreter actually needs — that touching any of these can turn integer_gadgets_match_lean_templates, fv_semantics, or the FV test programs CI job red, and that just fv-regen (plus updating the Lean templates/proofs) is the fix — isn't stated anywhere outside fv/acir_lean/CLAUDE.md. Separately, that file's own "reviewed" list omits fv_templates.rs, fv_semantics.rs, and regen_programs.sh, all three marked REVIEWED in their own file headers and listed in README.md's table — worth pointing at one canonical list instead of keeping two.

5. Discussion status

Only one top-level conversation comment exists, and it doesn't ask for anything actionable — it's the PR author (asterite) telling @TomAFrench the PR is ready for review, noting as a known cost that new programs need a regeneration script run. No open thread, so no table.

Not verified

• B1's shadowing mechanism. Both the fork and a separate cold-verification pass traced Lean's name-resolution order (namespace lookup before root) in the Lean source itself, but neither ran the toolchain end-to-end (this repo pins Lean v4.29.1; the source read was v4.21.0). If the resolution order changed between those versions, B1 could be moot. Worth a quick manual check — add a throwaway def Int.tdiv to a Templates file locally and see whether lake build picks it up — before treating it as confirmed enough to act on.
• Whether the review burden table in the PR body is exhaustive. The PR says only Spec/ needs review, "short[ly]" extending to Check.lean, the Emit*.lean entry points, check.sh, check_reviewing.py, regen_programs.sh, the two CI workflows, and the two Rust pin files. D7 shows fv/acir_lean/CLAUDE.md's own list is narrower than that; I didn't independently re-derive the full reviewed set from first principles, only cross-checked the two lists against each other and against each file's own header comment.
• Whether Lean's Mathlib proofs (AcirLean/Proofs/) are internally consistent with the stated gadget behavior beyond what AllClaims's type signature requires — e.g., whether a proof could exploit Classical.choice/propext in a way that's technically one of the three allowed axioms but still surprising. Check.lean's #print axioms guard is the intended defense here; I read it and trust it, but did not independently re-derive why exactly those three axioms are the right bar.