---
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.