# WP34 — Stage 5: machine-checked statements (Lean 4, core only)

Lean 4 project wp34 (library Wp34). No Mathlib: only the Lean core library (BitVec, Nat, List) and the core tactics bv_decide, decide, omega, simp, ac_rfl. Toolchain pinned in lean-toolchain: leanprover/lean4:v4.35.0 (Lean 4.35.0, commit eb6cafb7, arm64-apple-darwin; Lake 5.0.0).

bv_decide bit-blasts a BitVec/Bool goal to an And-Inverter Graph (AIG), hands the CNF to the CaDiCaL SAT solver bundled with Lean and asks it for an LRAT unsatisfiability certificate, which is then re-checked by Lean's verified LRAT checker. The solver is never trusted; the checker is executed on the native (compiled) code path, which Lean 4.35 records as a per-theorem axiom named <theorem>._native.bv_decide.ax_… (same trust base as Lean.ofReduceBool: Lean kernel + Lean compiler). Everything else depends only on propext, Quot.sound, Classical.choice. The complete #print axioms output for the headline theorems is in build.log (module Wp34.Audit).

cd formal
export PATH=$HOME/.elan/bin:$PATH
lake clean && lake build            # 32 s wall on an Apple M5 Max, exit code 0 (see build.log)

Tail of build.log (2026-11-01, lake clean && lake build):

✔ [2/9] Built Wp34.Group (315ms)
✔ [3/9] Built Wp34.Sha256Words (2.5s)
✔ [4/9] Built Wp34.Schedule (1.5s)
✔ [5/9] Built Wp34.Sha256Step (27s)
✔ [6/9] Built Wp34.LocalCollision (1.7s)
✔ [8/9] Built Wp34 (193ms)
# exit code 0 — wall time 32 s

(The [7/9] Wp34.Audit line is absent from the tail because Lake prints that module's #print axioms messages instead of a ✔ line; it is built — see build.log.) Build artefacts: .lake/ ≈ 470 MB (the LRAT certificates are stored inside the .olean files; Sha256Step.olean 150 MB, LocalCollision.olean 34 MB, Sha256Words.olean 31 MB).

Reproducibility gate: tests/test_formal_lean.py (static: no sorry, no axiom, no native_decide, no Mathlib, toolchain pinned; WP34_LEAN_BUILD=1 additionally runs lake build). Helper scripts: scripts/gf2_rank.py (GF(2) rank/kernel of Σ0, Σ1, σ0, σ1 and generation of the explicit inverses), scripts/local_collision.py (simulation of the linearised local collisions and the real-step counter-example), scripts/aig_sizes.py (per-theorem AIG sizes → scripts/aig_sizes.tsv).

# What is machine-checked and what is not

Machine-checked (every theorem below compiles with lake build; no sorry; no user axiom except the fields of the structure CyclicGroup, which are the explicit axioms of the abstract group model in §5 and are listed there).

Not machine-checked / informal: the historical attributions (Gilbert–Handschuh 2003, Chabaud–Joux 1998) and the probabilistic reading of the local collision (the 2⁻³⁹ estimate) are literature statements, not theorems; the Python simulations in scripts/ are sanity checks, not proofs; the "SAT instance size" column is a measurement, not a proof artefact.

Column "AIG" = number of AIG nodes of the bit-blasted instance given to CaDiCaL (from scripts/aig_sizes.tsv); "—" = no SAT call. Build time is per module (whole file).

# 1. SHA-256 word functions — Wp34/Sha256Words.lean (2.5 s)

Definitions transcribed from src/wp34/sha256.py: rotr, Sigma0, Sigma1, sigma0, sigma1, Ch, Maj on Word := BitVec 32.

Result for item 1(e): σ0 and σ1 are bijections of BitVec 32 — the logical shift does not make them singular (GF(2) rank 32, trivial kernel, scripts/gf2_rank.py), and bv_decide found no counter-example (UNSAT, certificate checked). The task brief expected them to be non-bijective; that expectation was wrong, and the controls show why the intuition fails: each of the two parts of σ0 (x >>> 3 alone; rotr 7 ^ rotr 18 alone, which has kernel {0, 0xFFFFFFFF} since ρ⁷ + ρ¹⁸ = ρ⁷(1 + ρ¹¹) is not a unit) is non-injective, but their sum is a unit.

# 2. Step function bijection — Wp34/Sha256Step.lean (27 s)

State = 8 registers; step / stepInv transcribed from step / step_inverse in sha256.py.

The direct 320-bit bv_decide call (cases s; simp only [...]; bv_decide) timed out (10 s default) and bv_omega on the abstracted goal did not terminate (killed after 35 CPU-minutes); the per-component split suggested in the brief is what is implemented, with the two addition-chain lemmas proven by SAT.

# 3. Message schedule — Wp34/Schedule.lean (1.5 s)

# 4. XOR-linearised 9-step local collision — Wp34/LocalCollision.lean (1.7 s)

linStep boolf replaces every + of step by ^^^ and Ch, Maj by boolf. Two linearisations are formalised (the choice is stated explicitly in the file header): absorb (Ch = Maj = 0: the Boolean functions absorb all differences — the difference-domain reading of the Gilbert–Handschuh 2003 conditions) and xor3 (Ch = Maj = x ^ y ^ z: the Chabaud–Joux 1998 linearisation). Σ0, Σ1 are kept exactly (they are linear). Correction vectors derived in the file header (the derivation is a comment, not a theorem):

• corrAbsorb δ = (δ, Σ1δ^Σ0δ, Σ1(Σ0δ), 0, δ, Σ0δ^Σ1δ, 0, 0, δ);
• corrXor3 δ = (δ, Σ1δ^Σ0δ, Σ1(Σ0δ^δ)^Σ0δ^δ, Σ1δ^Σ0δ, Σ1δ^Σ0δ, Σ0δ^Σ1δ, δ, 0, δ).

Note: the brief's sketch "δW_{i+1} = Σ1(δ) through the e-register" is incomplete — at step i+1 the a register also carries δ and injects Σ0(δ) through T2, so δW_{i+1} must be Σ1(δ) ⊕ Σ0(δ); bv_decide confirms the vectors above and the simulation in scripts/local_collision.py agrees.

The full-value statements were first attempted directly with bv_decide and timed out (they are pure parity identities; see §Failures). They are proven exactly as the brief's fallback suggests — via the linear difference-propagation version — and then lifted to the full-value statement by the proven linearity of lin9, so the general statement is machine-checked after all.

# 5. Abstract signature correctness — Wp34/Group.lean (0.3 s)

structure CyclicGroup (G : Type) — every field is an axiom of the model: zero, add, neg, nsmul : Nat → G → G, xcoord : G → Nat, gen, order; add_assoc, add_comm, zero_add, add_neg (commutative group); nsmul_zero, nsmul_succ (recursive definition of n•P); one_lt_order, nsmul_order : order•gen = 0; xcoord_neg : xcoord (−P) = xcoord P. Nothing else is assumed; in particular there is no field about modular inverses, about xcoord being injective up to sign, or about order being prime. Modular arithmetic is done on Nat with core lemmas (Nat.mul_mod, Nat.div_add_mod, …).

Derived (theorems, manual proofs): add_zero, neg_add, eq_neg_of_add_eq_zero, neg_add_rev, nsmul_add ((m+k)•a = m•a + k•a), nsmul_zero_point, nsmul_mul ((m·k)•a = m•(k•a)), add_add_add_comm, nsmul_add_point, nsmul_neg, nsmul_one, InSubgroup, gen_inSubgroup, nsmul_inSubgroup, nsmul_order_of_mem (order•P = 0 on the subgroup), nsmul_mod (scalars act modulo order), nsmul_congr_mod, nsmul_order_sub ((n−u)•P = −(u•P)), sub_mul_sub_mod ((n−s)(n−w) ≡ s·w (mod n)).

ecdsaVerify P e r s := 0 < r < n ∧ 0 < s < n ∧ ∃ w, s·w mod n = 1 ∧ xcoord((e·w)•G + (r·w)•P) mod n = r. Scope: this is the abstract ECDSA/Schnorr verification equation in a cyclic group with an xcoord map; BIP340's x-only keys/even-y normalisation and the "low-s" rule are not modelled.

# Failures and timeouts (honest record)

Lesson: CDCL SAT (CaDiCaL) is instantaneous on the mixed and/or/add goals of SHA-256 but systematically fails on pure-parity (XOR-chain) identities, which is where linear algebra over GF(2) — here encoded as rewriting with proven linearity lemmas — is the right tool.

# Classification

Every statement above is known_reproduced: the Ch/Maj identities, linearity and invertibility of the sigma functions, invertibility of the step function and of the message schedule, the linearised local collision, and Schnorr/ECDSA correctness and malleability are all standard facts. The contribution of this stage is their machine-checked status in Lean 4 core with a 32-second build, the explicit inverses of Σ0, Σ1, σ0, σ1, and the documentation of which formulations are and are not tractable for bv_decide.

# References (informal; keys from paper/references.bib where they exist)

• FIPS 180-4, Secure Hash Standard — nist2015fips180 (definitions of Σ0, Σ1, σ0, σ1, Ch, Maj, the step and the schedule).
• F. Chabaud, A. Joux, "Differential collisions in SHA-0", CRYPTO 1998 — chabaud1998differential (XOR-linearisation technique, xor3 model).
• H. Gilbert, H. Handschuh, "Security analysis of SHA-256 and sisters", SAC 2003 — the 9-step local collision and its absorbing conditions (absorb model). No entry in references.bib yet — to be added and verified at Stage 6; not cited in the Lean sources.
• FIPS 186-5 (ECDSA) — nist2023fips186; BIP340 (Schnorr) — abstract model only.