1# WP34 — Stage 5: machine-checked statements (Lean 4, core only)23Lean 4 project `wp34` (library `Wp34`). **No Mathlib**: only the Lean core library (`BitVec`,4`Nat`, `List`) and the core tactics `bv_decide`, `decide`, `omega`, `simp`, `ac_rfl`.5Toolchain pinned in `lean-toolchain`: `leanprover/lean4:v4.35.0`6(Lean 4.35.0, commit `eb6cafb7`, arm64-apple-darwin; Lake 5.0.0).78`bv_decide` bit-blasts a `BitVec`/`Bool` goal to an And-Inverter Graph (AIG), hands the CNF to the9**CaDiCaL SAT solver bundled with Lean** and asks it for an **LRAT unsatisfiability certificate**,10which is then re-checked by Lean's verified LRAT checker. The solver is never trusted; the checker11is executed on the native (compiled) code path, which Lean 4.35 records as a per-theorem axiom12named `<theorem>._native.bv_decide.ax_…` (same trust base as `Lean.ofReduceBool`: Lean kernel +13Lean compiler). Everything else depends only on `propext`, `Quot.sound`, `Classical.choice`.14The complete `#print axioms` output for the headline theorems is in `build.log` (module `Wp34.Audit`).1516```17cd formal18export PATH=$HOME/.elan/bin:$PATH19lake clean && lake build # 32 s wall on an Apple M5 Max, exit code 0 (see build.log)20```2122Tail of `build.log` (2026-11-01, `lake clean && lake build`):2324```25✔ [2/9] Built Wp34.Group (315ms)26✔ [3/9] Built Wp34.Sha256Words (2.5s)27✔ [4/9] Built Wp34.Schedule (1.5s)28✔ [5/9] Built Wp34.Sha256Step (27s)29✔ [6/9] Built Wp34.LocalCollision (1.7s)30✔ [8/9] Built Wp34 (193ms)31# exit code 0 — wall time 32 s32```3334(The `[7/9] Wp34.Audit` line is absent from the tail because Lake prints that module's35`#print axioms` messages instead of a `✔` line; it is built — see `build.log`.)36Build artefacts: `.lake/` ≈ 470 MB (the LRAT certificates are stored inside the `.olean` files;37`Sha256Step.olean` 150 MB, `LocalCollision.olean` 34 MB, `Sha256Words.olean` 31 MB).3839Reproducibility gate: `tests/test_formal_lean.py` (static: no `sorry`, no `axiom`, no40`native_decide`, no Mathlib, toolchain pinned; `WP34_LEAN_BUILD=1` additionally runs `lake build`).41Helper scripts: `scripts/gf2_rank.py` (GF(2) rank/kernel of Σ0, Σ1, σ0, σ1 and generation of the42explicit inverses), `scripts/local_collision.py` (simulation of the linearised local collisions and43the real-step counter-example), `scripts/aig_sizes.py` (per-theorem AIG sizes → `scripts/aig_sizes.tsv`).4445## What is machine-checked and what is not4647**Machine-checked** (every `theorem` below compiles with `lake build`; no `sorry`; no user `axiom`48except the *fields of the structure* `CyclicGroup`, which are the explicit axioms of the abstract49group model in §5 and are listed there).5051**Not machine-checked / informal**: the historical attributions (Gilbert–Handschuh 2003,52Chabaud–Joux 1998) and the probabilistic reading of the local collision (the 2⁻³⁹ estimate) are53literature statements, not theorems; the Python simulations in `scripts/` are sanity checks, not54proofs; the "SAT instance size" column is a measurement, not a proof artefact.5556Column "AIG" = number of AIG nodes of the bit-blasted instance given to CaDiCaL (from57`scripts/aig_sizes.tsv`); "—" = no SAT call. Build time is per module (whole file).5859### 1. SHA-256 word functions — `Wp34/Sha256Words.lean` (2.5 s)6061Definitions transcribed from `src/wp34/sha256.py`: `rotr`, `Sigma0`, `Sigma1`, `sigma0`,62`sigma1`, `Ch`, `Maj` on `Word := BitVec 32`.6364| Theorem | Informal statement | Method | AIG |65|---|---|---|---|66| `Ch_opt` | `Ch x y z = ((y ^ z) & x) ^ z` | `bv_decide` | 608 |67| `Maj_opt_or` | `Maj x y z = (x & (y \| z)) \| (y & z)` | `bv_decide` | 608 |68| `Maj_opt_xor` | `Maj x y z = ((x ^ y) & (y ^ z)) ^ y` | `bv_decide` | 768 |69| `Maj_comm` | `Maj` symmetric in its arguments | `bv_decide` | 704 |70| `Sigma0_xor`, `Sigma1_xor`, `sigma0_xor`, `sigma1_xor` | GF(2)-linearity `f (x ^ y) = f x ^ f y` | `bv_decide` | 960 / 960 / 933 / 870 |71| `Sigma0_zero`, …, `sigma1_zero` | `f 0 = 0` | `bv_decide` (closed by preprocessing) | — |72| `Sigma0_injective`, `Sigma1_injective` | `Function.Injective` | `bv_decide` | 704 / 704 |73| **`sigma0_injective`, `sigma1_injective`** | σ0, σ1 are injective on 32 bits (UNSAT certificate) | `bv_decide` | 686 / 644 |74| `shr3_not_injective` | control: `x >>> 3` is not injective (`0`, `1`) | `decide` | — |75| `sigma0_rotations_not_injective` | control: `rotr x 7 ^ rotr x 18` kills `0xFFFFFFFF` | `decide` | — |76| `sigma1_rotations_not_injective` | control: `rotr x 17 ^ rotr x 19` kills `0xFFFFFFFF` | `decide` | — |77| `rotr_xor` | `rotr (x ^ y) k = rotr x k ^ rotr y k` for every `k` | bit-level `simp` (`getLsbD_rotateRight`) | — |78| `bitMask_xor`, `xor_and_right` | helpers for the matrix-form inverses | `simp` / `bv_decide` | — / 512 |79| `Sigma0Inv_xor`, `Sigma1Inv_xor`, `sigma0Inv_xor`, `sigma1Inv_xor` | the explicit inverses are GF(2)-linear | `simp [rotr_xor]` + `ac_rfl` | — |80| `inv_of_quarters` | two linear maps whose composite fixes each byte compose to `id` | `bv_decide` (byte split) + rewriting | 33 |81| `Sigma0Inv_Sigma0_b0..b3`, … (32 lemmas) | `g (f (x & byte_i)) = x & byte_i` for the 8 (map, inverse) pairs | `bv_decide` | 508 – 4817 |82| `Sigma0Inv_Sigma0`, `Sigma0_Sigma0Inv`, `Sigma1Inv_Sigma1`, `Sigma1_Sigma1Inv` | Σ0⁻¹ = XOR of 17 rotations `{0,1,2,5,7,8,9,10,12,16,17,19,22,23,25,29,30}`, Σ1⁻¹ = XOR of 17 rotations `{2,3,5,7,9,11,12,13,18,21,22,23,24,26,27,29,30}` | `inv_of_quarters` | — |83| `sigma0Inv_sigma0`, `sigma0_sigma0Inv`, `sigma1Inv_sigma1`, `sigma1_sigma1Inv` | σ0⁻¹, σ1⁻¹ given as explicit 32×32 GF(2) matrices (column tables) | `inv_of_quarters` | — |84| **`Sigma0_bijective`, `Sigma1_bijective`, `sigma0_bijective`, `sigma1_bijective`** | injective ∧ surjective (`Bijective`, defined locally since core lacks `Function.Bijective`) | from the above | — |8586Result for item 1(e): **σ0 and σ1 are bijections of `BitVec 32`** — the logical shift does *not*87make them singular (GF(2) rank 32, trivial kernel, `scripts/gf2_rank.py`), and `bv_decide` found no88counter-example (UNSAT, certificate checked). The task brief expected them to be non-bijective;89that expectation was wrong, and the controls show *why* the intuition fails: each of the two parts90of σ0 (`x >>> 3` alone; `rotr 7 ^ rotr 18` alone, which has kernel `{0, 0xFFFFFFFF}` since91`ρ⁷ + ρ¹⁸ = ρ⁷(1 + ρ¹¹)` is not a unit) is non-injective, but their sum is a unit.9293### 2. Step function bijection — `Wp34/Sha256Step.lean` (27 s)9495`State` = 8 registers; `step` / `stepInv` transcribed from `step` / `step_inverse` in `sha256.py`.9697| Theorem | Informal statement | Method | AIG |98|---|---|---|---|99| `add4_sub4` | `h + A + B + k + w − A − B − k − w = h` | `bv_decide` (120 s cap, ~2 s) | 2048 |100| `sub4_add4` | `x − A − B − k − w + A + B + k + w = x` | `bv_decide` | 2420 |101| **`stepInv_step`** | `stepInv (step s k w) k w = s` | `generalize` Σ0+Maj, Σ1, Ch; `simp [add_sub_cancel, add4_sub4]` | — |102| **`step_stepInv`** | `step (stepInv n k w) k w = n` | `generalize`; `simp [sub4_add4, sub_add_cancel]` | — |103| `step_injective`, `step_surjective`, **`step_bijective`** | the step is a bijection of the 256-bit state for fixed `(k, w)` | from the two above | — |104| `stepsInv_steps`, `steps_stepsInv`, **`steps_bijective`** | any number of rounds with known `(K_t, W_t)` is a bijection | induction on the list | — |105106The direct 320-bit `bv_decide` call (`cases s; simp only [...]; bv_decide`) **timed out** (10 s107default) and `bv_omega` on the abstracted goal did not terminate (killed after 35 CPU-minutes); the108per-component split suggested in the brief is what is implemented, with the two addition-chain109lemmas proven by SAT.110111### 3. Message schedule — `Wp34/Schedule.lean` (1.5 s)112113| Theorem | Informal statement | Method | AIG |114|---|---|---|---|115| **`scheduleStep_inv`** | `W_{t−16} = W_t − σ1(W_{t−2}) − W_{t−7} − σ0(W_{t−15})` | `bv_decide` | 1921 |116| `scheduleStep_bijective` | `W_{t−16} ↦ W_t` is a bijection for fixed other inputs | `bv_decide` + rewriting | 2200 |117| `schedule`, `schedule_lt`, `schedule_ge` | the expanded schedule as a well-founded recursion on `t` | definition / `simp` | — |118| **`schedule_backward`** | for the real schedule, `W_{t−16}` is determined by `W_{t−15..t}` (hence the 64 words by any 16 consecutive ones) | rewriting | — |119120### 4. XOR-linearised 9-step local collision — `Wp34/LocalCollision.lean` (1.7 s)121122`linStep boolf` replaces every `+` of `step` by `^^^` and `Ch`, `Maj` by `boolf`. Two123linearisations are formalised (the choice is stated explicitly in the file header):124`absorb` (`Ch = Maj = 0`: the Boolean functions absorb all differences — the difference-domain125reading of the Gilbert–Handschuh 2003 conditions) and `xor3` (`Ch = Maj = x ^ y ^ z`: the126Chabaud–Joux 1998 linearisation). Σ0, Σ1 are kept exactly (they are linear).127Correction vectors derived in the file header (the derivation is a comment, not a theorem):128129* `corrAbsorb δ = (δ, Σ1δ^Σ0δ, Σ1(Σ0δ), 0, δ, Σ0δ^Σ1δ, 0, 0, δ)`;130* `corrXor3 δ = (δ, Σ1δ^Σ0δ, Σ1(Σ0δ^δ)^Σ0δ^δ, Σ1δ^Σ0δ, Σ1δ^Σ0δ, Σ0δ^Σ1δ, δ, 0, δ)`.131132Note: the brief's sketch "δW_{i+1} = Σ1(δ) through the e-register" is incomplete — at step i+1 the133`a` register also carries δ and injects Σ0(δ) through T2, so δW_{i+1} must be Σ1(δ) ⊕ Σ0(δ);134`bv_decide` confirms the vectors above and the simulation in `scripts/local_collision.py` agrees.135136| Theorem | Informal statement | Method | AIG |137|---|---|---|---|138| `State.xor_zero`, `Words9.xor_zero` | `s ⊕ 0 = s` | `bv_decide` | 257 / 289 |139| `linStep_xor_absorb`, `linStep_xor_xor3` | one linearised step is a XOR-homomorphism in `(state, k, w)` | `bv_decide` | 4000 / 6368 |140| `lin9_xor_absorb`, `lin9_xor_xor3` | nine linearised steps are a XOR-homomorphism | `simp` rewriting | — |141| `corrAbsorb_xor`, `corrXor3_xor` | the correction vectors are linear in δ | `simp [Sigma0_xor, Sigma1_xor]` + `ac_rfl` | — |142| `diff_absorb_b0..b3`, `diff_xor3_b0..b3` | difference-only statement with δ restricted to one byte | `bv_decide` | 5049 / 8769 |143| `byte_split` | `δ = ⊕ of its four bytes` | `bv_decide` | 33 |144| **`localCollision_absorb_diff`, `localCollision_xor3_diff`** | `lin9 f 0 0 (corr δ) = 0` for every δ (difference propagation) | linearity + bytes | — |145| **`localCollision_absorb`, `localCollision_xor3`** | `lin9 f s K W = lin9 f s K (W ⊕ corr δ)` for **every** `s`, `K`, `W`, `δ` (864 bits universally quantified) | `lin9_xor_*` + `*_diff` | — |146| **`absorb_corrections_not_real_collision`** | negative control: with the *real* modular step, zero state/constants/words and δ = 1, the two 9-step outputs differ | `decide` (kernel evaluation) | — |147148The full-value statements were first attempted directly with `bv_decide` and **timed out** (they149are pure parity identities; see §Failures). They are proven exactly as the brief's fallback150suggests — via the linear difference-propagation version — and then *lifted* to the full-value151statement by the proven linearity of `lin9`, so the general statement is machine-checked after all.152153### 5. Abstract signature correctness — `Wp34/Group.lean` (0.3 s)154155`structure CyclicGroup (G : Type)` — **every field is an axiom of the model**:156`zero`, `add`, `neg`, `nsmul : Nat → G → G`, `xcoord : G → Nat`, `gen`, `order`;157`add_assoc`, `add_comm`, `zero_add`, `add_neg` (commutative group); `nsmul_zero`,158`nsmul_succ` (recursive definition of `n•P`); `one_lt_order`, `nsmul_order : order•gen = 0`;159`xcoord_neg : xcoord (−P) = xcoord P`. Nothing else is assumed; in particular there is **no**160field about modular inverses, about `xcoord` being injective up to sign, or about `order` being161prime. Modular arithmetic is done on `Nat` with core lemmas (`Nat.mul_mod`, `Nat.div_add_mod`, …).162163Derived (theorems, manual proofs): `add_zero`, `neg_add`, `eq_neg_of_add_eq_zero`, `neg_add_rev`,164`nsmul_add` (`(m+k)•a = m•a + k•a`), `nsmul_zero_point`, `nsmul_mul` (`(m·k)•a = m•(k•a)`),165`add_add_add_comm`, `nsmul_add_point`, `nsmul_neg`, `nsmul_one`, `InSubgroup`, `gen_inSubgroup`,166`nsmul_inSubgroup`, `nsmul_order_of_mem` (`order•P = 0` on the subgroup), `nsmul_mod`167(scalars act modulo `order`), `nsmul_congr_mod`, `nsmul_order_sub` (`(n−u)•P = −(u•P)`),168`sub_mul_sub_mod` (`(n−s)(n−w) ≡ s·w (mod n)`).169170| Theorem | Informal statement | Method |171|---|---|---|172| **`schnorr_correct`** | `P = d•G`, `R = k•G`, `s = (k + e·d) mod n` ⟹ `s•G = R + e•P` (`schnorrVerify`) | `nsmul_mod`, `nsmul_add`, `nsmul_mul` |173| `schnorr_correct_nat` | same with `s = k + e·d` unreduced | rewriting |174| **`ecdsa_malleable`** | `ecdsaVerify P e r s → ecdsaVerify P e r (n − s)` for `P` in the subgroup; the verification point becomes its negative and `xcoord` is unchanged | manual (witness `w' = n − (w mod n)`, `sub_mul_sub_mod`, `neg_add_rev`, `xcoord_neg`) |175| **`ecdsa_correct`** | `r = x(k•G) mod n`, `k·s ≡ e + r·d`, `s·w ≡ 1` ⟹ `ecdsaVerify (d•G) e r s` | manual (`Nat.mul_mod`, `ac_rfl`, `nsmul_congr_mod`) |176177`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`.178Scope: this is the *abstract* ECDSA/Schnorr verification equation in a cyclic group with an179`xcoord` map; BIP340's x-only keys/even-y normalisation and the "low-s" rule are not modelled.180181## Failures and timeouts (honest record)182183| Attempt | Outcome | Resolution |184|---|---|---|185| `Sigma0Inv (Sigma0 x) = x` by direct `bv_decide` (32 free bits, 51 rotation terms per bit) | SAT timeout at 10 s; also at 240 s with `acNf := true` (256 s wall) | linearity (`rotr_xor` proven bit-wise) + byte split (`inv_of_quarters`) |186| `Sigma0Inv_xor` by `bv_decide` | timeout at 60 s (34-literal parity) | `simp [rotr_xor]; ac_rfl` |187| 16-bit halves instead of bytes | proven, but each LRAT certificate ≈ 100 MB in the `.olean` (`Sha256Words.olean` was 1.3 GB) | bytes: ≈ 0.6 MB each, file now 31 MB |188| `stepInv_step` by direct 320-bit `bv_decide` | timeout at 10 s | abstraction of Σ0+Maj, Σ1, Ch + two 160-bit SAT lemmas + rewriting |189| `stepInv_step` by `generalize` + `bv_omega` | did not terminate (killed after 35 CPU-min) | as above |190| `localCollision_absorb` / `_xor3` (864-bit) by direct `bv_decide` | timeout at 10 s | linearity of `lin9` + difference version |191| `localCollision_xor3_diff` (32-bit δ) by direct `bv_decide` | timeout at 10 s (`absorb` version passed) | byte split in δ |192| `corrXor3_xor` by `bv_decide` | timeout at 10 s (24-literal parity) | `simp [Sigma0_xor, Sigma1_xor]; ac_rfl` |193| Re-elaborating `LocalCollision.lean` with `trace.Meta.Tactic.bv` on | heartbeat timeouts in the trace printer for the last 4 theorems (no SAT there); normal build unaffected | reported as-is in `scripts/aig_sizes.py` |194195Lesson: CDCL SAT (CaDiCaL) is instantaneous on the mixed and/or/add goals of SHA-256 but196systematically fails on pure-parity (XOR-chain) identities, which is where linear algebra over GF(2)197— here encoded as rewriting with proven linearity lemmas — is the right tool.198199## Classification200201Every statement above is **`known_reproduced`**: the Ch/Maj identities, linearity and202invertibility of the sigma functions, invertibility of the step function and of the message203schedule, the linearised local collision, and Schnorr/ECDSA correctness and malleability are all204standard facts. The contribution of this stage is their *machine-checked* status in Lean 4 core205with a 32-second build, the explicit inverses of Σ0, Σ1, σ0, σ1, and the documentation of which206formulations are and are not tractable for `bv_decide`.207208## References (informal; keys from `paper/references.bib` where they exist)209210* FIPS 180-4, Secure Hash Standard — `nist2015fips180` (definitions of Σ0, Σ1, σ0, σ1, Ch, Maj, the step and the schedule).211* F. Chabaud, A. Joux, "Differential collisions in SHA-0", CRYPTO 1998 — `chabaud1998differential` (XOR-linearisation technique, `xor3` model).212* 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.213* FIPS 186-5 (ECDSA) — `nist2023fips186`; BIP340 (Schnorr) — abstract model only.214