# SHA-256 — notes (paper §7)

Step inverse (given K_t, W_t and the new state (a', a, b, c, e', e, f, g)): T₂ = Σ₀(a) ⊞ Maj(a,b,c); T₁ = a' ⊟ T₂; d = e' ⊟ T₁; h = T₁ ⊟ Σ₁(e) ⊟ Ch(e,f,g) ⊟ K_t ⊟ W_t. (src/wp34/sha256.py::step_inverse, tested; Lean theorem in formal/.)

Schedule inversion: W_{t−16} = W_t ⊟ σ₁(W_{t−2}) ⊟ W_{t−7} ⊟ σ₀(W_{t−15}).

Consequence: for any target state S and any message block M, the IV H with Steps₆₄(H, M) = S is computable (pseudo-preimage of the compression function without feed-forward is free); the Davies–Meyer feed-forward H ⊞ Steps₆₄(H, M) is what blocks this.

XOR-linearised local collision: replace ⊞ by ⊕ in the step and linearise Ch, Maj (Gilbert–Handschuh 2003); a difference δ in W_i propagates to a_{i+1} and e_{i+1} and is cancelled by corrections in W_{i+1..i+8}; the exact pattern and the probability with the real step function are measured in experiments/reduced_round_sha256/ and the linear statement is machine-checked in formal/.