1/-2 WP34 — the SHA-256 step function is a bijection of the 256-bit state for fixed (K_t, W_t).3 `step` and `stepInv` are transcribed from `step` / `step_inverse` in `src/wp34/sha256.py`.4-/5import Wp34.Sha256Words67namespace Wp3489/-- The eight 32-bit working registers `(a, b, c, d, e, f, g, h)`. -/10structure State where11 a : Word12 b : Word13 c : Word14 d : Word15 e : Word16 f : Word17 g : Word18 h : Word19 deriving DecidableEq, Repr2021/-- One SHA-256 step (FIPS 180-4 §6.2.2 step 3) with round constant `k` and message word `w`. -/22def step (s : State) (k w : Word) : State :=23 let T1 := s.h + Sigma1 s.e + Ch s.e s.f s.g + k + w24 let T2 := Sigma0 s.a + Maj s.a s.b s.c25 { a := T1 + T2, b := s.a, c := s.b, d := s.c, e := s.d + T1, f := s.e, g := s.f, h := s.g }2627/-- Inverse step (`step_inverse` in the Python reference): the new state is28`(a₁, a, b, c, e₁, e, f, g)`; recover `T2` from `(a, b, c)`, then `T1 = a₁ − T2`, `d = e₁ − T1`,29`h = T1 − Σ1(e) − Ch(e,f,g) − k − w`. -/30def stepInv (n : State) (k w : Word) : State :=31 let T2 := Sigma0 n.b + Maj n.b n.c n.d32 let T1 := n.a - T233 { a := n.b, b := n.c, c := n.d, d := n.e - T1,34 e := n.f, f := n.g, g := n.h, h := T1 - Sigma1 n.f - Ch n.f n.g n.h - k - w }3536/-! #### Proof strategy3738The direct `bv_decide` call on the 320-bit goal exceeds the SAT timeout (see README): the39instance mixes the non-linear Σ/Ch/Maj sub-terms with the re-association of five chained 32-bit40additions. The statement is *linear* in the sub-terms `T2 = Σ0(a) + Maj(a,b,c)`, `Σ1(e)` and41`Ch(e,f,g)`, so we abstract them with `generalize`; the two surviving components are then closed42by two small SAT lemmas on the pure addition chains (`add4_sub4`, `sub4_add4`, 160-bit43instances, ~1.5 s each) and core's `BitVec.add_sub_cancel` / `sub_add_cancel`. The other six44components are definitional. -/4546/-- `h + A + B + k + w − A − B − k − w = h` (SAT). -/47theorem add4_sub4 (h A B k w : Word) : h + A + B + k + w - A - B - k - w = h := by48 bv_decide (config := { timeout := 120 })4950/-- `x − A − B − k − w + A + B + k + w = x` (SAT). -/51theorem sub4_add4 (x A B k w : Word) : x - A - B - k - w + A + B + k + w = x := by52 bv_decide (config := { timeout := 120 })5354/-- `stepInv` is a left inverse of `step`: every SHA-256 step can be undone given `(k, w)`. -/55theorem stepInv_step (s : State) (k w : Word) : stepInv (step s k w) k w = s := by56 obtain ⟨a, b, c, d, e, f, g, h⟩ := s57 simp only [step, stepInv, State.mk.injEq]58 generalize Sigma0 a + Maj a b c = T259 generalize Sigma1 e = A60 generalize Ch e f g = B61 simp only [BitVec.add_sub_cancel, add4_sub4, and_self]6263/-- `stepInv` is a right inverse of `step`. -/64theorem step_stepInv (n : State) (k w : Word) : step (stepInv n k w) k w = n := by65 obtain ⟨a₁, a, b, c, e₁, e, f, g⟩ := n66 simp only [step, stepInv, State.mk.injEq]67 generalize Sigma0 a + Maj a b c = T268 generalize Sigma1 e = A69 generalize Ch e f g = B70 simp only [sub4_add4, BitVec.sub_add_cancel, and_self]7172/-- For fixed `(k, w)` the step function is injective on the state. -/73theorem step_injective (k w : Word) : Function.Injective (fun s => step s k w) := by74 intro s s' h75 have := congrArg (fun t => stepInv t k w) h76 simpa only [stepInv_step] using this7778/-- For fixed `(k, w)` the step function is surjective on the state. -/79theorem step_surjective (k w : Word) : ∀ n, ∃ s, step s k w = n :=80 fun n => ⟨stepInv n k w, step_stepInv n k w⟩8182/-- The step function is a bijection of the 256-bit state for every fixed `(k, w)`. -/83theorem step_bijective (k w : Word) : Bijective (fun s => step s k w) :=84 ⟨step_injective k w, step_surjective k w⟩8586/-! ### Iterated steps: any number of rounds with known `(K_t, W_t)` is invertible. -/8788/-- Apply the steps for the list of `(k, w)` pairs, first element first. -/89def steps (s : State) : List (Word × Word) → State90 | [] => s91 | (k, w) :: rest => steps (step s k w) rest9293/-- Undo the steps, last element first. -/94def stepsInv (n : State) : List (Word × Word) → State95 | [] => n96 | (k, w) :: rest => stepInv (stepsInv n rest) k w9798theorem stepsInv_steps (kws : List (Word × Word)) : ∀ s, stepsInv (steps s kws) kws = s := by99 induction kws with100 | nil => intro s; rfl101 | cons kw rest ih =>102 intro s103 obtain ⟨k, w⟩ := kw104 simp only [steps, stepsInv, ih, stepInv_step]105106theorem steps_stepsInv (kws : List (Word × Word)) : ∀ n, steps (stepsInv n kws) kws = n := by107 induction kws with108 | nil => intro n; rfl109 | cons kw rest ih =>110 intro n111 obtain ⟨k, w⟩ := kw112 simp only [steps, stepsInv, step_stepInv, ih]113114/-- The `r`-round compression core (before the Davies–Meyer feed-forward) is a bijection of the115state for every fixed sequence of round constants and message words. -/116theorem steps_bijective (kws : List (Word × Word)) : Bijective (fun s => steps s kws) :=117 ⟨fun s s' h => by118 have := congrArg (fun t => stepsInv t kws) h119 simpa only [stepsInv_steps] using this,120 fun n => ⟨stepsInv n kws, steps_stepsInv kws n⟩⟩121122end Wp34123