id: H20 title: 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 trivial axis: C kind: sha256 statement: 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}; 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. motivation: Distinguish the compression function from the hash (mandate §6). assumptions: None. expected_contribution: Machine-checked statements (Lean 4 bv_decide) and an executable demonstration. related_work:
- nist2015fips180
- merkle1989one
- damgard1989design
- aoki2009preimages possible_counterexamples: None (theorem). verification_strategy: formal/ theorems + tests/test_core.py step inverse test. computational_budget: minutes status: evaluated classification: known_reproduced evidence:
- formal/README.md
- formal/build.log
- tests/test_formal_lean.py
- tests/test_core.py verdict: 'Machine-checked: stepInv ∘ step = id and step ∘ stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps_bijective for any number of rounds, scheduleStep_inv and schedule_backward; executable demonstration in tests/test_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally.'
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 trivial
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}; 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.