1/-2 WP34 — SHA-256 message schedule (FIPS 180-4 §6.2.2 step 1):3 W_t = σ1(W_{t−2}) + W_{t−7} + σ0(W_{t−15}) + W_{t−16} for 16 ≤ t < 64.4 Each schedule step is invertible in its oldest input: W_{t−16} is determined by W_{t−15..t}.5-/6import Wp34.Sha256Words78namespace Wp34910/-- One schedule step, argument order `(W_{t−16}, W_{t−15}, W_{t−7}, W_{t−2})`11(`message_schedule` in the Python reference). -/12def scheduleStep (w16 w15 w7 w2 : Word) : Word := sigma1 w2 + w7 + sigma0 w15 + w161314/-- `W_{t−16} = W_t − σ1(W_{t−2}) − W_{t−7} − σ0(W_{t−15})`. -/15theorem scheduleStep_inv (w16 w15 w7 w2 : Word) :16 scheduleStep w16 w15 w7 w2 - sigma1 w2 - w7 - sigma0 w15 = w16 := by17 unfold scheduleStep sigma0 sigma1 rotr; bv_decide1819/-- For fixed `(W_{t−15}, W_{t−7}, W_{t−2})`, the map `W_{t−16} ↦ W_t` is a bijection. -/20theorem scheduleStep_bijective (w15 w7 w2 : Word) :21 Bijective (fun w16 => scheduleStep w16 w15 w7 w2) :=22 ⟨fun x y h => by23 have hx := scheduleStep_inv x w15 w7 w224 have hy := scheduleStep_inv y w15 w7 w225 simp only at h26 rw [h] at hx; exact hx.symm.trans hy,27 fun wt => ⟨wt - sigma1 w2 - w7 - sigma0 w15, by28 unfold scheduleStep sigma0 sigma1 rotr; bv_decide⟩⟩2930/-- The expanded message schedule as a function of the 16 message words `M`31(well-founded recursion on `t`). -/32def schedule (M : Fin 16 → Word) : Nat → Word33 | t =>34 if h : t < 16 then M ⟨t, h⟩35 else scheduleStep (schedule M (t - 16)) (schedule M (t - 15)) (schedule M (t - 7))36 (schedule M (t - 2))37 decreasing_by all_goals omega3839theorem schedule_lt (M : Fin 16 → Word) (t : Nat) (h : t < 16) : schedule M t = M ⟨t, h⟩ := by40 rw [schedule]; simp [h]4142theorem schedule_ge (M : Fin 16 → Word) (t : Nat) (h : 16 ≤ t) :43 schedule M t = scheduleStep (schedule M (t - 16)) (schedule M (t - 15))44 (schedule M (t - 7)) (schedule M (t - 2)) := by45 rw [schedule]; simp [Nat.not_lt.mpr h]4647/-- Backward schedule: `W_{t−16}` is determined by `(W_{t−15}, W_{t−7}, W_{t−2}, W_t)`.48Consequently the 64-word expanded schedule is determined by ANY 16 consecutive words. -/49theorem schedule_backward (M : Fin 16 → Word) (t : Nat) (h : 16 ≤ t) :50 schedule M (t - 16) =51 schedule M t - sigma1 (schedule M (t - 2)) - schedule M (t - 7)52 - sigma0 (schedule M (t - 15)) := by53 rw [schedule_ge M t h, scheduleStep_inv]5455end Wp3456