1# 2026-11-01 — Stage 5: formal verification (Lean 4.35.0, core only, `bv_decide`)23Host: Apple M5 Max laptop, macOS 27, elan toolchain `leanprover/lean4:v4.35.0`4(Lean commit `eb6cafb7`, Lake 5.0.0). Project: `formal/` (library `Wp34`, no Mathlib).5Command: `cd formal && lake clean && lake build` → exit 0, **32 s wall** (log: `formal/build.log`).6Gate: `tests/test_formal_lean.py` (11 passed with `WP34_LEAN_BUILD=1`).78## What was proven (all `theorem`, no `sorry`, no user `axiom`; see `formal/README.md` for the table)9101. **SHA-256 word identities** (`Wp34/Sha256Words.lean`, 2.5 s): optimised `Ch`/`Maj` forms;11 GF(2)-linearity of Σ0, Σ1, σ0, σ1; injectivity of all four by `bv_decide`; **explicit inverses**12 (Σ0⁻¹, Σ1⁻¹ = XOR of 17 rotations each; σ0⁻¹, σ1⁻¹ = 32×32 GF(2) matrices computed by13 `formal/scripts/gf2_rank.py`), hence bijectivity of all four.14 *Finding that contradicts the brief:* σ0 and σ1 **are** bijective on 32 bits (rank 32, trivial15 kernel, no counter-example — the brief anticipated non-bijectivity and a counter-example). The16 controls `shr3_not_injective` and `sigma0_rotations_not_injective` show that each of the two17 summands of σ0 is singular while their sum is a unit. This is a known property of SHA-256.182. **Step bijection** (`Wp34/Sha256Step.lean`, 27 s): `stepInv (step s k w) k w = s` and the19 converse, plus the iterated version (`steps_bijective`: any number of rounds with known20 `(K_t, W_t)` is a bijection of the 256-bit state).213. **Message schedule** (`Wp34/Schedule.lean`): `W_{t−16} = W_t − σ1(W_{t−2}) − W_{t−7} − σ0(W_{t−15})`22 both as a one-liner on `scheduleStep` and on the well-founded `schedule` definition.234. **9-step linearised local collision** (`Wp34/LocalCollision.lean`): for two explicit24 linearisations of Ch/Maj (`absorb`: Ch = Maj = 0, Gilbert–Handschuh-style absorbing conditions;25 `xor3`: Ch = Maj = x⊕y⊕z, Chabaud–Joux-style), the full-value statement26 `lin9 f s K W = lin9 f s K (W ⊕ corr δ)` for **all** `s, K, W, δ` (864 bits), obtained from the27 difference-only version by the proven linearity of `lin9`. Correction vectors:28 `absorb`: (δ, Σ1δ⊕Σ0δ, Σ1Σ0δ, 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ). The brief's sketch δW_{i+1} = Σ1(δ) is29 incomplete (the Σ0(δ) term coming from the `a` register must be cancelled too).30 Negative control, machine-checked by `decide`: the same corrections are **not** a collision of the31 real modular step (zero state, δ = 1); `scripts/local_collision.py` sees 0/20 000 random hits.325. **Abstract signatures** (`Wp34/Group.lean`): axiomatised `CyclicGroup G` (all fields listed in33 the README); Schnorr correctness `s•G = R + e•P` for `s = (k + e·d) mod n`; ECDSA correctness;34 **ECDSA malleability** `(r, s) ⟹ (r, n − s)` with the modular inverse as an explicit witness and35 `Nat` modular arithmetic proven from core lemmas (`sub_mul_sub_mod`).3637Trust base: Lean kernel + Lean compiler (the LRAT certificate checker runs natively; Lean 4.3538records each such use as an axiom `<thm>._native.bv_decide.ax_…`, listed by `Wp34/Audit.lean` in39`build.log`). CaDiCaL itself is not trusted. Non-SAT theorems (`rotr_xor`, all of `Group.lean`, the40`decide` counter-example) depend only on `propext`/`Quot.sound`/`Classical.choice`.4142## What failed and why4344* Direct `bv_decide` on every **pure-parity** goal timed out (10 s default; 240 s + `acNf` for45 `Sigma0Inv_Sigma0`): inverse compositions (51 XOR terms per bit), linearity of the 17-rotation46 inverses, the 864-bit local-collision statements, the `xor3` difference version, `corrXor3_xor`.47 CDCL solvers have no XOR reasoning; these identities need Gaussian elimination, which we replaced48 by rewriting with proven linearity lemmas (`rotr_xor`, `Sigma0_xor`, `linStep_xor_*`) and49 `ac_rfl`, plus SAT only on byte-restricted instances (8 free variables).50* The direct 320-bit step-bijection goal timed out; `bv_omega` on the abstracted goal did not51 terminate (killed at 35 CPU-min). Resolution: abstract Σ0+Maj, Σ1, Ch and prove the two52 addition-chain lemmas (`add4_sub4`, `sub4_add4`, ~2 s each) by SAT — the "per-component split"53 the mandate anticipated.54* 16-bit SAT splits produced ≈ 100 MB LRAT certificates each (`Sha256Words.olean` reached 1.3 GB);55 byte splits bring it to 31 MB. `.lake/` is ≈ 470 MB after a clean build (certificates live in56 the oleans; `Sha256Step.olean` 150 MB).57* The Python→Lean handoff had no failures: every rank/inverse/correction vector computed in58 Python was confirmed by `bv_decide` or `decide` as stated.5960## Classification6162All items: **`known_reproduced`** (none of these statements is new mathematics; the contribution is63the machine-checked status, the explicit sigma inverses, and the tractability map for `bv_decide`).64No conjecture is represented as a theorem: the Gilbert–Handschuh probability estimate and the65historical attributions are confined to comments and the README prose.6667## Artefacts6869`formal/` (Lake project, `build.log`, `README.md`, `scripts/{gf2_rank,local_collision,aig_sizes}.py`,70`scripts/aig_sizes.tsv`), `tests/test_formal_lean.py`. Note: the repository `.gitignore` ignores71`*.log`, so `formal/build.log` needs a `!formal/build.log` exception to be committed.72