Verified-zkEVM / clean: 32-Bit Addition Gadget (`Addition32/Theorems.lean`)
Four 8-bit limb addition constraints with carries over a prime field F_p compute 32-bit addition modulo 2^32 and the carry-out bit.
What was claimed: Four 8-bit limb addition constraints with carries over a prime field F_p compute 32-bit addition modulo 2^32 and the carry-out bit.
What Lean states: add32_soundness in Clean/Gadgets/Addition32/Theorems.lean (Verified-zkEVM/clean at f8a4194c) — add32_soundness over F p ([Fact p.Prime], [Fact (p > 512)]): limb sum equals (x + y + carry_in) % 2^32 and c3 = ... / 2^32.
Prose only / the gap: Definitions of F p and IsBool live in imported Clean.Utils.Field / Clean.Gadgets.Boolean; prime bound p > 512 is a section variable.
Verification & replays: Static scan & 13 mutants generated by SeamCert (risk: low · 8). Kernel replay not run.
What the public sources report
Every item below is attributed to the published paper, replay, or commentary that reported it.
| Main theorem | add32_soundness: given twelve byte-range hypotheses (x0.val < 256, …, z3.val < 256), five IsBool carry hypotheses, and four limb equations x_i + y_i + c_{i-1} = c_i * 256 + z_i, proves the recombined 32-bit value and carry-out. [1] |
|---|---|
| Field assumptions | Declared as section variables {p : ℕ} [Fact p.Prime] and [p_large_enough: Fact (p > 512)], which prevent wrap-around in the single-limb sum x + y + b < 512 < p. [1] |
| Escape hatches in file | None (0 sorry, 0 axiom, 0 native_decide). Proof discharges over ℤ via zify, ring, and omega. [1] |
| Planted variants | 13 variants generated in Mutants.lean (vacuity probes and constant perturbations on 256 and 32). Because p and p_large_enough are section variables, running Mutants.lean requires keeping them inside the section. [1] |
Open specification seams (our reading)
Our reading of the sources above: the places where the formal Lean statement and the informal headline claim can still come apart.
- The statement imports
Clean.Types.U32,Clean.Utils.Field, andClean.Gadgets.Boolean: a reader must check thatF pisZMod pandIsBool bmeansb = 0 ∨ b = 1. - The twelve
x_i.val < 256hypotheses are caller obligations: soundness of the full circuit depends on the caller gadget enforcing byte range checks on all inputs and outputs.
Footnotes & Sources
Sources read on 7 November 2026. Spotted an error or a newer independent replay? Write to [email protected].