WIP: Dilithium Tier-1 Lean spec

[illuzen]

Summary

• Starts a mathlib-free Lean 4 package under dilithium/formal/ that models Dilithium field arithmetic (same Phase 0 style as qp-poseidon).
• montgomery_reduce / reduce32 / caddq are transcribed and proved (congruence, Montgomery half-open domain, Barrett range). FIPS 204 Algs 35–40 and rounding.rs are drafted; NTT, capstones, and SPEC.md are not in yet.
• Adds a CI formal-spec job. It will fail on this draft: Fips204.lean does not currently lake build, and ci/AxiomsCheck.lean / capstone theorems are still missing.

Test plan

• cd dilithium/formal && lake build (currently fails in Fips204.lean)
• Finish rounding proofs (Algs 35–40, MakeHint equivalence)
• Finish NTT (Algs 41–42, zetas, KATs, bounds)
• Add mldsa_arith_tier1 / _safety + ci/AxiomsCheck.lean + SPEC.md so the new CI job is green
• Confirm rustfmt/taplo still pass (./clippy.sh was run before opening this PR)

Made with Cursor

[n13]

Reviewer model: GPT Sol

Verdict: REQUEST_CHANGES — the new required formal gate is not runnable at this head, the checked-in package does not yet contain the artifacts that gate promises to verify, and one of the new formal range claims is inaccurate.

Blocking findings:

1. [P1] Make the committed Lean target build (dilithium/formal/MlDsaArith/Fips204.lean:69-71). Under the pinned Lean 4.30 toolchain, simp [geomSum] closes the n = 0 goal, so the following omega produces No goals to be solved. The exact-head Formal Spec (Lean) job fails here and skips every later assurance step. Remove the redundant tactic and require lake build to pass before this gate lands.

2. [P1] Check in the capstone/NTT assurance surface before enabling its CI gate (.github/workflows/ci.yml:229-250). After the build error is fixed, the job is still guaranteed to fail because dilithium/formal/ci/AxiomsCheck.lean is absent and neither mldsa_arith_tier1 nor mldsa_arith_tier1_safety exists. More broadly, this head contains rounding definitions but no rounding refinement theorems, and no Rust NTT model/refinement at all, while the workflow says it verifies reduce.rs, rounding.rs, and ntt.rs against Algorithms 35–42. Add the promised proofs, capstones, and axiom-check file, or scope/defer the gate to what this phase actually provides.

3. [P2] Correct the claimed tight reduce32 range (dilithium/formal/MlDsaArith/ReduceCorrectness.lean:287-293). The proved interval is a valid loose bound, but it is not tight and the explanation for its lower end is false. For a = -2143289344, the implementation computes t = -255 and reduce32(a) = -6283009, which is the actual minimum over the stated i32 domain; at i32::MIN, the cited t = -256 case returns only -2096896. Tighten the theorem/comment to [-6283009, 6283008] and update the Rust contract's current off-by-one lower bound so the formal artifact does not institutionalize a second, looser number.

Validation:

• Reviewed exact base 3b1464f751d536aba023a53df2a4f4533ab94f62 through head 1b34f32cf49beda70ea7128d7b56d03912e7a5be; git diff --check passed.
• cargo test --locked -p qp-rusty-crystals-dilithium --all-features passed: 161 unit tests, the integration targets, and 11 doctests.
• Exact-head CI has passing format, Clippy/docs, no-std, stack-budget, security-audit, and CodeQL checks; Formal Spec (Lean) fails at the line above.
• The no-sorry/admit scan passed locally; the axiom-footprint step cannot run because its checked-in input and target theorems are missing.
• Cross-checked the new FIPS models against FIPS 204 Algorithms 35–43 and NIST's July 2026 potential-updates sheet.