id: H21 title: Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations axis: D kind: formal statement: 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 the step function are theorems checked with LRAT certificates. motivation: 'Stage 5: separate machine-checked statements from informal proofs.' assumptions: Lean 4.35 core BitVec semantics. expected_contribution: A reusable formal library of SHA-256 identities. related_work:

• demoura2021lean
• nist2015fips180 possible_counterexamples: A false identity would produce a counterexample from the SAT solver. verification_strategy: lake build in formal/ computational_budget: minutes status: evaluated classification: known_reproduced evidence:
• formal/README.md
• formal/build.log
• tests/test_formal_lean.py verdict: 'Lean 4.35 bv_decide (LRAT certificates re-checked in Lean): Ch_opt, Maj_opt_or, Maj_opt_xor, GF(2)-linearity of Σ0, Σ1, σ0, σ1, injectivity and explicit inverses (Σ0⁻¹ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib.'

# H21 — Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations

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 the step function are theorems checked with LRAT certificates.