/-
  WP34 — XOR-linearised SHA-256 and the 9-step local collision
  (Chabaud–Joux 1998 linearisation technique; Gilbert–Handschuh 2003 local collision for SHA-256).

  Linearised model. Every modular addition of the step function is replaced by XOR; Σ0 and Σ1
  are already GF(2)-linear (`Sigma0_xor`, `Sigma1_xor`). The two Boolean functions are replaced
  by a GF(2)-linear substitute `boolf`; we prove the local collision for two standard choices:

  * `absorb` : Ch, Maj ↦ 0. This is the difference-domain reading of Gilbert–Handschuh 2003
    (SAC 2003, "Security analysis of SHA-256 and sisters", §4): their 9-step local collision is
    computed under the conditions that the Boolean functions *absorb* every incoming difference
    (a difference in exactly one input of Ch/Maj is cancelled when the other two inputs are
    equal on the active bits / when the relevant bit of the selector has the right value); the
    corrections then only have to cancel the Σ0 / Σ1 images, which are linear. In a linear model
    "Ch and Maj absorb all differences" is exactly "Ch = Maj = 0".
  * `xor3`   : Ch, Maj ↦ x ^ y ^ z. This is the Chabaud–Joux 1998 (CRYPTO) linearisation used
    for SHA-0, where the IF / MAJ functions are replaced by the XOR of their inputs. The
    corrections differ (derived below) but a 9-step local collision still exists.

  Derivation (model `absorb`; δ is the perturbation, ΔW the correction injected in W):
    step i   : ΔW = δ                      → Δa = δ, Δe = δ
    step i+1 : a has δ ⇒ ΔT2 = Σ0(δ); e has δ ⇒ Σ1(δ) in ΔT1.
               Choose ΔW = Σ1(δ) ^ Σ0(δ) so that ΔT1 = Σ0(δ) = ΔT2 ⇒ Δa_new = 0, Δe_new = Σ0(δ)
               (the Σ1(δ) term alone — "through the e-register" — would leave Σ0(δ) in `a`).
    step i+2 : e has Σ0(δ) ⇒ ΔW = Σ1(Σ0(δ)) cancels ΔT1; registers: c = δ, f = Σ0(δ), g = δ
    step i+3 : ΔW = 0;                   registers: d = δ, g = Σ0(δ), h = δ
    step i+4 : h has δ ⇒ ΔW = δ (ΔT1 = 0); d has δ ⇒ Δe_new = δ. registers: e = δ, h = Σ0(δ)
    step i+5 : h = Σ0(δ), e = δ ⇒ ΔW = Σ0(δ) ^ Σ1(δ);   registers: f = δ
    step i+6 : ΔW = 0;                   registers: g = δ
    step i+7 : ΔW = 0;                   registers: h = δ
    step i+8 : ΔW = δ                    ⇒ all registers zero.
  Correction vector (absorb): (δ, Σ1δ^Σ0δ, Σ1(Σ0δ), 0, δ, Σ0δ^Σ1δ, 0, 0, δ).
  Correction vector (xor3)  : (δ, Σ1δ^Σ0δ, Σ1(Σ0δ^δ)^Σ0δ^δ, Σ1δ^Σ0δ, Σ1δ^Σ0δ, Σ0δ^Σ1δ, δ, 0, δ)
  (same bookkeeping with ΔCh = ΔMaj = XOR of the register differences).

  Both vectors were first checked by simulation (`scripts/local_collision.py`); the theorems
  below are the universal statements, machine-checked by `bv_decide` for every state, every
  round-constant vector, every message-word vector and every δ.
-/
import Wp34.Sha256Step

namespace Wp34

/-- Nine consecutive words (round constants `K_i..K_{i+8}` or message words `W_i..W_{i+8}`). -/
structure Words9 where
  w0 : Word
  w1 : Word
  w2 : Word
  w3 : Word
  w4 : Word
  w5 : Word
  w6 : Word
  w7 : Word
  w8 : Word
  deriving DecidableEq, Repr

/-- Component-wise XOR (injecting a difference vector into the message words). -/
def Words9.xor (u v : Words9) : Words9 :=
  ⟨u.w0 ^^^ v.w0, u.w1 ^^^ v.w1, u.w2 ^^^ v.w2, u.w3 ^^^ v.w3, u.w4 ^^^ v.w4,
   u.w5 ^^^ v.w5, u.w6 ^^^ v.w6, u.w7 ^^^ v.w7, u.w8 ^^^ v.w8⟩

/-- GF(2)-linearised step: every `+` of `step` becomes `^^^`, `Ch`/`Maj` become `boolf`. -/
def linStep (boolf : Word → Word → Word → Word) (s : State) (k w : Word) : State :=
  let T1 := s.h ^^^ Sigma1 s.e ^^^ boolf s.e s.f s.g ^^^ k ^^^ w
  let T2 := Sigma0 s.a ^^^ boolf s.a s.b s.c
  { 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 }

/-- Linearisation "the Boolean functions absorb every difference" (Gilbert–Handschuh 2003). -/
def absorb (_x _y _z : Word) : Word := 0
/-- Linearisation "Boolean function ↦ XOR of its inputs" (Chabaud–Joux 1998). -/
def xor3 (x y z : Word) : Word := x ^^^ y ^^^ z

/-- Nine linearised steps `i, i+1, …, i+8`. -/
def lin9 (boolf : Word → Word → Word → Word) (s : State) (K W : Words9) : State :=
  linStep boolf (linStep boolf (linStep boolf (linStep boolf (linStep boolf (linStep boolf
    (linStep boolf (linStep boolf (linStep boolf s K.w0 W.w0) K.w1 W.w1) K.w2 W.w2) K.w3 W.w3)
    K.w4 W.w4) K.w5 W.w5) K.w6 W.w6) K.w7 W.w7) K.w8 W.w8

/-- Nine real (modular, non-linear) SHA-256 steps, for the negative control below. -/
def real9 (s : State) (K W : Words9) : State :=
  step (step (step (step (step (step (step (step (step s K.w0 W.w0) K.w1 W.w1) K.w2 W.w2)
    K.w3 W.w3) K.w4 W.w4) K.w5 W.w5) K.w6 W.w6) K.w7 W.w7) K.w8 W.w8

/-- Correction vector of the 9-step local collision in the `absorb` model. -/
def corrAbsorb (δ : Word) : Words9 :=
  ⟨δ, Sigma1 δ ^^^ Sigma0 δ, Sigma1 (Sigma0 δ), 0, δ, Sigma0 δ ^^^ Sigma1 δ, 0, 0, δ⟩

/-- Correction vector of the 9-step local collision in the `xor3` model. -/
def corrXor3 (δ : Word) : Words9 :=
  ⟨δ, Sigma1 δ ^^^ Sigma0 δ, Sigma1 (Sigma0 δ ^^^ δ) ^^^ Sigma0 δ ^^^ δ,
   Sigma1 δ ^^^ Sigma0 δ, Sigma1 δ ^^^ Sigma0 δ, Sigma0 δ ^^^ Sigma1 δ, δ, 0, δ⟩

/-! #### Proof strategy

The 9-step statements are pure parity (XOR) identities: a direct `bv_decide` call times out
(CDCL solvers do not reason about XOR chains; see README). Instead we exploit linearity, exactly
as the Chabaud–Joux method does on paper:
1. `linStep_xor_*` — one linearised step is a XOR-homomorphism in `(state, k, w)` (SAT, small);
2. `lin9_xor_*` — hence nine steps are (rewriting, no SAT);
3. `corr*_xor` — the correction vector is linear in δ (SAT, small);
4. `diff_*_b0..b3` — the difference-only statement for δ restricted to each byte (SAT with 8 free
   variables);
5. `localCollision_*_diff` — the difference-only statement for every δ, by 3 + 4;
6. `localCollision_*` — the full-value statement, by 2 + 5.
-/

/-- Component-wise XOR of states. -/
def State.xor (s t : State) : State :=
  ⟨s.a ^^^ t.a, s.b ^^^ t.b, s.c ^^^ t.c, s.d ^^^ t.d, s.e ^^^ t.e, s.f ^^^ t.f, s.g ^^^ t.g,
   s.h ^^^ t.h⟩
/-- The all-zero state. -/
def State.zero : State := ⟨0, 0, 0, 0, 0, 0, 0, 0⟩
/-- The all-zero word vector. -/
def Words9.zero : Words9 := ⟨0, 0, 0, 0, 0, 0, 0, 0, 0⟩

theorem State.xor_zero (s : State) : s.xor State.zero = s := by
  cases s; simp only [State.xor, State.zero, State.mk.injEq]; bv_decide
theorem Words9.xor_zero (K : Words9) : K.xor Words9.zero = K := by
  cases K; simp only [Words9.xor, Words9.zero, Words9.mk.injEq]; bv_decide

/-- One linearised step (`absorb` model) is a XOR-homomorphism in `(state, k, w)`. -/
theorem linStep_xor_absorb (s t : State) (k k' w w' : Word) :
    linStep absorb (s.xor t) (k ^^^ k') (w ^^^ w') =
      (linStep absorb s k w).xor (linStep absorb t k' w') := by
  cases s; cases t
  simp only [linStep, absorb, State.xor, State.mk.injEq, Sigma0, Sigma1, rotr]
  bv_decide

/-- One linearised step (`xor3` model) is a XOR-homomorphism in `(state, k, w)`. -/
theorem linStep_xor_xor3 (s t : State) (k k' w w' : Word) :
    linStep xor3 (s.xor t) (k ^^^ k') (w ^^^ w') =
      (linStep xor3 s k w).xor (linStep xor3 t k' w') := by
  cases s; cases t
  simp only [linStep, xor3, State.xor, State.mk.injEq, Sigma0, Sigma1, rotr]
  bv_decide

/-- Nine linearised steps are a XOR-homomorphism (pure rewriting with `linStep_xor_absorb`). -/
theorem lin9_xor_absorb (s t : State) (K K' W W' : Words9) :
    lin9 absorb (s.xor t) (K.xor K') (W.xor W') =
      (lin9 absorb s K W).xor (lin9 absorb t K' W') := by
  cases K; cases K'; cases W; cases W'
  simp only [lin9, Words9.xor, linStep_xor_absorb]

theorem lin9_xor_xor3 (s t : State) (K K' W W' : Words9) :
    lin9 xor3 (s.xor t) (K.xor K') (W.xor W') =
      (lin9 xor3 s K W).xor (lin9 xor3 t K' W') := by
  cases K; cases K'; cases W; cases W'
  simp only [lin9, Words9.xor, linStep_xor_xor3]

/-- The correction vectors are GF(2)-linear in δ (rewriting with `Sigma0_xor`/`Sigma1_xor`
then associativity–commutativity of XOR; no SAT — the `xor3` instance is a 24-literal parity
problem on which `bv_decide` times out). -/
theorem corrAbsorb_xor (x y : Word) : corrAbsorb (x ^^^ y) = (corrAbsorb x).xor (corrAbsorb y) := by
  simp only [corrAbsorb, Words9.xor, Words9.mk.injEq, Sigma0_xor, Sigma1_xor]
  repeat' apply And.intro
  all_goals (first | trivial | ac_rfl)
theorem corrXor3_xor (x y : Word) : corrXor3 (x ^^^ y) = (corrXor3 x).xor (corrXor3 y) := by
  simp only [corrXor3, Words9.xor, Words9.mk.injEq, Sigma0_xor, Sigma1_xor]
  repeat' apply And.intro
  all_goals (first | trivial | ac_rfl)

/-- The difference map `δ ↦ lin9 f 0 0 (corr δ)` is linear in δ. -/
theorem diff_xor_absorb (x y : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb (x ^^^ y)) =
      (lin9 absorb State.zero Words9.zero (corrAbsorb x)).xor
        (lin9 absorb State.zero Words9.zero (corrAbsorb y)) := by
  rw [corrAbsorb_xor, ← lin9_xor_absorb, State.xor_zero, Words9.xor_zero]
theorem diff_xor_xor3 (x y : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 (x ^^^ y)) =
      (lin9 xor3 State.zero Words9.zero (corrXor3 x)).xor
        (lin9 xor3 State.zero Words9.zero (corrXor3 y)) := by
  rw [corrXor3_xor, ← lin9_xor_xor3, State.xor_zero, Words9.xor_zero]

-- Difference-only statement for δ restricted to one byte (8 free variables each).
theorem diff_absorb_b0 (δ : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x000000FF#32)) = State.zero := by
  simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_absorb_b1 (δ : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x0000FF00#32)) = State.zero := by
  simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_absorb_b2 (δ : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0x00FF0000#32)) = State.zero := by
  simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_absorb_b3 (δ : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb (δ &&& 0xFF000000#32)) = State.zero := by
  simp only [lin9, linStep, absorb, corrAbsorb, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_xor3_b0 (δ : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x000000FF#32)) = State.zero := by
  simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_xor3_b1 (δ : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x0000FF00#32)) = State.zero := by
  simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_xor3_b2 (δ : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0x00FF0000#32)) = State.zero := by
  simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide
theorem diff_xor3_b3 (δ : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 (δ &&& 0xFF000000#32)) = State.zero := by
  simp only [lin9, linStep, xor3, corrXor3, State.zero, Words9.zero, State.mk.injEq,
    Sigma0, Sigma1, rotr]
  bv_decide

theorem byte_split (δ : Word) :
    δ = (δ &&& 0x000000FF#32) ^^^ (δ &&& 0x0000FF00#32) ^^^ (δ &&& 0x00FF0000#32)
      ^^^ (δ &&& 0xFF000000#32) := by bv_decide

/-- **9-step local collision, `absorb` model, difference-only statement**: injecting the
correction vector into the zero state with zero constants yields the zero difference, for every δ. -/
theorem localCollision_absorb_diff (δ : Word) :
    lin9 absorb State.zero Words9.zero (corrAbsorb δ) = State.zero := by
  rw [byte_split δ, diff_xor_absorb, diff_xor_absorb, diff_xor_absorb,
    diff_absorb_b0, diff_absorb_b1, diff_absorb_b2, diff_absorb_b3, State.xor_zero,
    State.xor_zero, State.xor_zero]

/-- **9-step local collision, `xor3` (Chabaud–Joux) model, difference-only statement.** -/
theorem localCollision_xor3_diff (δ : Word) :
    lin9 xor3 State.zero Words9.zero (corrXor3 δ) = State.zero := by
  rw [byte_split δ, diff_xor_xor3, diff_xor_xor3, diff_xor_xor3,
    diff_xor3_b0, diff_xor3_b1, diff_xor3_b2, diff_xor3_b3, State.xor_zero,
    State.xor_zero, State.xor_zero]

/-- **9-step local collision, `absorb` model, full-value statement**: for every state `s`,
every round-constant vector `K`, every message-word vector `W` and every difference `δ`, the
linearised state after nine steps is unchanged when `W` is replaced by `W ⊕ corrAbsorb δ`
(an 8·32 + 9·32 + 9·32 + 32 = 864-bit universally quantified statement). -/
theorem localCollision_absorb (s : State) (K W : Words9) (δ : Word) :
    lin9 absorb s K W = lin9 absorb s K (W.xor (corrAbsorb δ)) := by
  have h := lin9_xor_absorb s State.zero K Words9.zero W (corrAbsorb δ)
  rw [State.xor_zero, Words9.xor_zero, localCollision_absorb_diff, State.xor_zero] at h
  exact h.symm

/-- **9-step local collision, `xor3` (Chabaud–Joux) model, full-value statement.** -/
theorem localCollision_xor3 (s : State) (K W : Words9) (δ : Word) :
    lin9 xor3 s K W = lin9 xor3 s K (W.xor (corrXor3 δ)) := by
  have h := lin9_xor_xor3 s State.zero K Words9.zero W (corrXor3 δ)
  rw [State.xor_zero, Words9.xor_zero, localCollision_xor3_diff, State.xor_zero] at h
  exact h.symm

/-- **Negative control (machine-checked counter-example).** The linearised local collision is
NOT a collision of the real step function: with the zero state, zero constants, zero words and
δ = 1, the real 9-step outputs differ (the XOR characteristic holds on the modular function only
with some probability — Gilbert–Handschuh estimate 2⁻³⁹ for a one-bit δ with modular
corrections; `scripts/local_collision.py` observes 0/20000 with XOR corrections). -/
theorem absorb_corrections_not_real_collision :
    real9 State.zero Words9.zero Words9.zero ≠
      real9 State.zero Words9.zero (Words9.zero.xor (corrAbsorb 1)) := by
  decide

end Wp34