# 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.