1---2id: H213title: Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations4axis: D5kind: formal6statement: Ch(x,y,z) = ((y ⊕ z) ∧ x) ⊕ z, two Maj forms, GF(2)-linearity of Σ0, Σ1, σ0, σ1, bijectivity of Σ0, Σ1 and of the7 step function are theorems checked with LRAT certificates.8motivation: 'Stage 5: separate machine-checked statements from informal proofs.'9assumptions: Lean 4.35 core BitVec semantics.10expected_contribution: A reusable formal library of SHA-256 identities.11related_work:12- demoura2021lean13- nist2015fips18014possible_counterexamples: A false identity would produce a counterexample from the SAT solver.15verification_strategy: lake build in formal/16computational_budget: minutes17status: evaluated18classification: known_reproduced19evidence:20- formal/README.md21- formal/build.log22- tests/test_formal_lean.py23verdict: 'Lean 4.35 bv_decide (LRAT certificates re-checked in Lean): Ch_opt, Maj_opt_or, Maj_opt_xor, GF(2)-linearity of24 Σ0, Σ1, σ0, σ1, injectivity and explicit inverses (Σ0⁻¹ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry,25 no user axiom, no Mathlib.'26---2728# H21 — Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations2930Ch(x,y,z) = ((y ⊕ z) ∧ x) ⊕ z, two Maj forms, GF(2)-linearity of Σ0, Σ1, σ0, σ1, bijectivity of Σ0, Σ1 and of the step function are theorems checked with LRAT certificates.31