1---2id: H203title: The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage4 problems on the compression function are trivial5axis: C6kind: sha2567statement: For fixed (K_t, W_t) the step function is a bijection with an explicit inverse; W_{t−16} is determined by W_{t−15..t};8 hence for any target state and any chosen message one can invert the full 64-step compression (without feed-forward) and9 choose the IV — the Merkle–Damgård feed-forward is what makes preimages hard.10motivation: Distinguish the compression function from the hash (mandate §6).11assumptions: None.12expected_contribution: Machine-checked statements (Lean 4 bv_decide) and an executable demonstration.13related_work:14- nist2015fips18015- merkle1989one16- damgard1989design17- aoki2009preimages18possible_counterexamples: None (theorem).19verification_strategy: formal/ theorems + tests/test_core.py step inverse test.20computational_budget: minutes21status: evaluated22classification: known_reproduced23evidence:24- formal/README.md25- formal/build.log26- tests/test_formal_lean.py27- tests/test_core.py28verdict: 'Machine-checked: stepInv ∘ step = id and step ∘ stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps_bijective29 for any number of rounds, scheduleStep_inv and schedule_backward; executable demonstration in tests/test_core.py. Consequence30 (pseudo-preimages of the feed-forward-free compression function are free) stated informally.'31---3233# H20 — The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial3435For fixed (K_t, W_t) the step function is a bijection with an explicit inverse; W_{t−16} is determined by W_{t−15..t}; hence for any target state and any chosen message one can invert the full 64-step compression (without feed-forward) and choose the IV — the Merkle–Damgård feed-forward is what makes preimages hard.36