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