# 2026-11-01 — Stage 5: formal verification (Lean 4.35.0, core only, bv_decide)

Host: Apple M5 Max laptop, macOS 27, elan toolchain leanprover/lean4:v4.35.0 (Lean commit eb6cafb7, Lake 5.0.0). Project: formal/ (library Wp34, no Mathlib). Command: cd formal && lake clean && lake build → exit 0, 32 s wall (log: formal/build.log). Gate: tests/test_formal_lean.py (11 passed with WP34_LEAN_BUILD=1).

# What was proven (all theorem, no sorry, no user axiom; see formal/README.md for the table)

1. SHA-256 word identities (Wp34/Sha256Words.lean, 2.5 s): optimised Ch/Maj forms; GF(2)-linearity of Σ0, Σ1, σ0, σ1; injectivity of all four by bv_decide; explicit inverses (Σ0⁻¹, Σ1⁻¹ = XOR of 17 rotations each; σ0⁻¹, σ1⁻¹ = 32×32 GF(2) matrices computed by formal/scripts/gf2_rank.py), hence bijectivity of all four. Finding that contradicts the brief: σ0 and σ1 are bijective on 32 bits (rank 32, trivial kernel, no counter-example — the brief anticipated non-bijectivity and a counter-example). The controls shr3_not_injective and sigma0_rotations_not_injective show that each of the two summands of σ0 is singular while their sum is a unit. This is a known property of SHA-256.
2. Step bijection (Wp34/Sha256Step.lean, 27 s): stepInv (step s k w) k w = s and the converse, plus the iterated version (steps_bijective: any number of rounds with known (K_t, W_t) is a bijection of the 256-bit state).
3. Message schedule (Wp34/Schedule.lean): W_{t−16} = W_t − σ1(W_{t−2}) − W_{t−7} − σ0(W_{t−15}) both as a one-liner on scheduleStep and on the well-founded schedule definition.
4. 9-step linearised local collision (Wp34/LocalCollision.lean): for two explicit linearisations of Ch/Maj (absorb: Ch = Maj = 0, Gilbert–Handschuh-style absorbing conditions; xor3: Ch = Maj = x⊕y⊕z, Chabaud–Joux-style), the full-value statement lin9 f s K W = lin9 f s K (W ⊕ corr δ) for all s, K, W, δ (864 bits), obtained from the difference-only version by the proven linearity of lin9. Correction vectors: absorb: (δ, Σ1δ⊕Σ0δ, Σ1Σ0δ, 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ). The brief's sketch δW_{i+1} = Σ1(δ) is incomplete (the Σ0(δ) term coming from the a register must be cancelled too). Negative control, machine-checked by decide: the same corrections are not a collision of the real modular step (zero state, δ = 1); scripts/local_collision.py sees 0/20 000 random hits.
5. Abstract signatures (Wp34/Group.lean): axiomatised CyclicGroup G (all fields listed in the README); Schnorr correctness s•G = R + e•P for s = (k + e·d) mod n; ECDSA correctness; ECDSA malleability (r, s) ⟹ (r, n − s) with the modular inverse as an explicit witness and Nat modular arithmetic proven from core lemmas (sub_mul_sub_mod).

Trust base: Lean kernel + Lean compiler (the LRAT certificate checker runs natively; Lean 4.35 records each such use as an axiom <thm>._native.bv_decide.ax_…, listed by Wp34/Audit.lean in build.log). CaDiCaL itself is not trusted. Non-SAT theorems (rotr_xor, all of Group.lean, the decide counter-example) depend only on propext/Quot.sound/Classical.choice.

# What failed and why

• Direct bv_decide on every pure-parity goal timed out (10 s default; 240 s + acNf for Sigma0Inv_Sigma0): inverse compositions (51 XOR terms per bit), linearity of the 17-rotation inverses, the 864-bit local-collision statements, the xor3 difference version, corrXor3_xor. CDCL solvers have no XOR reasoning; these identities need Gaussian elimination, which we replaced by rewriting with proven linearity lemmas (rotr_xor, Sigma0_xor, linStep_xor_*) and ac_rfl, plus SAT only on byte-restricted instances (8 free variables).
• The direct 320-bit step-bijection goal timed out; bv_omega on the abstracted goal did not terminate (killed at 35 CPU-min). Resolution: abstract Σ0+Maj, Σ1, Ch and prove the two addition-chain lemmas (add4_sub4, sub4_add4, ~2 s each) by SAT — the "per-component split" the mandate anticipated.
• 16-bit SAT splits produced ≈ 100 MB LRAT certificates each (Sha256Words.olean reached 1.3 GB); byte splits bring it to 31 MB. .lake/ is ≈ 470 MB after a clean build (certificates live in the oleans; Sha256Step.olean 150 MB).
• The Python→Lean handoff had no failures: every rank/inverse/correction vector computed in Python was confirmed by bv_decide or decide as stated.

# Classification

All items: known_reproduced (none of these statements is new mathematics; the contribution is the machine-checked status, the explicit sigma inverses, and the tractability map for bv_decide). No conjecture is represented as a theorem: the Gilbert–Handschuh probability estimate and the historical attributions are confined to comments and the README prose.

# Artefacts

formal/ (Lake project, build.log, README.md, scripts/{gf2_rank,local_collision,aig_sizes}.py, scripts/aig_sizes.tsv), tests/test_formal_lean.py. Note: the repository .gitignore ignores *.log, so formal/build.log needs a !formal/build.log exception to be committed.