Formal Verification

[illuzen]

Summary

This PR does two things: shrinks the dependency footprint, and adds a machine-checked Lean 4 proof that the hand-optimized Goldilocks field arithmetic in src/goldilocks.rs is correct.

Dependency cleanup

• upgrade rand — bump rand to the current release.
• trim criterion — build criterion with default-features = false + cargo_bench_support only. This drops 28 packages from Cargo.lock (the html_reports feature pulled in the whole plotters stack). Benchmarks still run; only HTML report generation is lost.

Formal verification (formal/)

A new Lean 4 package proving the trickiest code in this crate — the overflow/underflow tricks, NEG_ORDER corrections, unreachable_unchecked compiler hints, and the 128-bit reduction in goldilocks.rs — correct modulo p = 2^64 − 2^32 + 1. It follows the same conventions as the formal/ packages in qp-zk-circuits and qp-plonky2: Lean v4.30.0, mathlib-free (builds in ~3 s, no cache to fetch in CI), kernel-checked end to end.

For every operation (add, sub, mul/reduce128, neg, halve, exp7, square, double, as_canonical_u64, is_zero, ==), assuming only that inputs are u64s — canonicality is not assumed, matching the crate's non-canonical representation:

• Congruence — the result equals the mathematical field operation mod p (e.g. rustAdd a b % P = (a + b) % P). reduce128 is proven correct on the entire u128 range.
• Closure — the result fits back in a u64.
• No undefined behavior — every unchecked claim in the Rust is now a theorem:
  • the assume(self.value > P && rhs.value > P) hints in add/sub are implied by their branch conditions, so the unreachable_unchecked inside assume is dead code;
  • the += NEG_ORDER / -= NEG_ORDER fix-ups annotated "Cannot overflow"/"Cannot underflow", and halve's wrapping_add, genuinely never wrap;
  • add_no_canonicalize_trashing_input's safety contract (x + y < 2^64 + P) is proven to hold at its call site in reduce128.

Layout:

File	Contents
formal/GoldilocksSpec/Model.lean	Line-by-line transcription of goldilocks.rs into Nat-level definitions; each cites the Rust lines it mirrors. Wrapping ops are modeled as actually wrapping, so a wrong "cannot overflow" comment would make the theorems unprovable.
formal/GoldilocksSpec/Correctness.lean	All proofs, the capstone theorem goldilocks_tier1 bundling every claim, and kernel-evaluated cross-checks of the model against the crate's own test_against_p3_expected_values vectors (guards the hand-transcription trust seam).
formal/ci/AxiomsCheck.lean	Import-only file CI uses to read the capstone's axiom footprint.

Correctness is stated as Nat congruences (% P) rather than mathlib's ZMod p; the statements are equivalent (casting Nat → ZMod P identifies x with x % P) and keeping the package dependency-free means CI needs no mathlib cache.

CI

New formal-spec job mirroring the qp-zk-circuits/qp-plonky2 pattern:

• lake build via leanprover/lean-action (pinned to a full commit SHA), with an independent leanchecker re-check of the compiled environment;
• a grep gate asserting no proof placeholder anywhere under formal/;
• an axiom-footprint gate asserting goldilocks_tier1 depends on exactly {propext, Classical.choice, Quot.sound} — the standard Lean axioms, nothing else.

Test plan

• lake build clean from scratch (no warnings, ~3 s)
• Axiom check: goldilocks_tier1 depends on exactly propext, Classical.choice, Quot.sound
• No-placeholder grep gate passes locally
• Model cross-checked against the Rust test vectors (test_against_p3_expected_values, test_multiplication_large, test_canonical_reduction) by kernel evaluation
• cargo test / benches unaffected by the criterion trim (Rust code untouched by the formal work)
• formal-spec CI job green on this PR

---

Note

Low Risk
No changes to production Rust crypto code; risk is mainly CI maintenance and lockfile churn from dev-dependency updates.

Overview
Adds a mathlib-free Lean 4 package under formal/ that models src/goldilocks.rs and proves tier-1 properties (mod-P congruence, u64 closure, and soundness of overflow/assume paths) for non-canonical representatives, capped by goldilocks_tier1 with decide cross-checks against the Rust test vectors.

CI gains a formal-spec job: pinned lean-action with lake build + leanchecker, a no-sorry/admit grep, and an axiom-footprint check via formal/ci/AxiomsCheck.lean.

Rust dev-deps: criterion is trimmed to default-features = false + cargo_bench_support (drops HTML/plotters from the lockfile); Cargo.lock reflects routine transitive bumps.

^{Reviewed by Cursor Bugbot for commit bf06652. Configure here.}

[n13]

The axiom-footprint gate does not cover the PR’s core no-UB/no-wrap claims. goldilocks_tier1 bundles the functional congruence/closure results, but it does not reference rustAdd_assume_sound, rustAdd_fixup_no_overflow, rustSub_assume_sound, rustSub_fixup_no_underflow, reduce_borrow_fixup_no_underflow, or addNoCanonicalize_fixup_no_overflow. Since lake build accepts declared axioms and the separate grep only rejects sorry/admit/sorryAx, any of those safety proofs could depend on a new custom axiom while the exact-footprint job still passes. This contradicts both the CI comment that the check catches stray axioms and the PR claim that the capstone bundles every claim. Please include the safety theorems in goldilocks_tier1 (or create a separate safety capstone) and run #print axioms on the complete assurance surface.

Verdict: request changes. All current checks pass, and I found no production Rust regression, but the formal-verification gate is incomplete for the guarantees this PR says it enforces.

[n13]

Re-reviewed the updated head (c5ce1202). The prior blocker is resolved: goldilocks_tier1_safety now bundles the add/sub assume soundness, add/sub fixup bounds, halve no-wrap, reduce borrow/product bounds, and unsafe-add fixup bound, while CI runs #print axioms against both the functional and safety capstones with the exact standard-axiom allowlist.

The revised formal-spec job passes, including Lean build and independent kernel checking, and the complete Rust, formatting, analysis, security, CodeQL, macOS, and Ubuntu checks are green. I found no remaining blocking issue.

Verdict: approve.