/-
  RollupEvent.lean — Serialize Adjugate Matrix verification into a single
  verifiable payload for the consensus engine.

  Architecture:
    Prover (off-chain, heavy):     detQ, adjugate, inv-gap-Sidon checks
    Verifier (on-chain/consensus):  matrix multiply, threshold, Sidon check, Ξ=0

  This uses the Prop/Bool reflection pattern:
    verifyRollupProp  — logical specification (Prop, used in proofs)
    verifyRollupBool  — executable check     (Bool, run by consensus)
    verifyRollup_spec — bridge theorem (↔)
-/

import CoreFormalism.FixedPoint
import SilverSight.AdjugateMatrix
import SilverSight.ColdReviewer

set_option linter.dupNamespace false

namespace SilverSight.Rollup

open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16
open SilverSight.AdjugateMatrix
open SilverSight.ColdReviewer

abbrev Matrix8 := SilverSight.AdjugateMatrix.Matrix8

-- ═══════════════════════════════════════════════════════════════════════════
-- §1  The Rollup Event Struct
-- ═══════════════════════════════════════════════════════════════════════════

/-- The single serialised event payload. Every field is either a raw network
    input (from the consensus state) or a Prover-supplied witness/claim. -/
structure OracleRollupEvent where
  -- ── 1. Raw network state  ──
  M       : Matrix8        -- the matrix being verified
  sigma   : Q16_16         -- spectral gap (threshold ≥ 1/7)
  strands : Array Nat      -- strand set (size 8, Sidon property)

  -- ── 2. Prover's witness (heavy computations, done off-chain)  ──
  adjM    : Matrix8        -- claimed adjugate of M
  detM    : Q16_16         -- claimed determinant of M

  -- ── 3. Audit metrics (claimed)  ──
  psiInv  : Q16_16         -- claimed Ψ_inv = ‖M·adjM − detM·I‖_∞
  psiGap  : Q16_16         -- claimed Ψ_gap = max(0, τ−σ)²
  psiSidon: Q16_16         -- claimed Ψ_Sidon = 0 if Sidon, 1 otherwise

  -- ── 4. The unified score  ──
  xiScore : Q16_16         -- claimed Ξ = ψInv + ψGap + ψSidon
  deriving Repr, DecidableEq

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  The Verifier  (no detQ — only O(n³) matrix multiply)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Propositional specification: the mathematical validity condition. -/
def verifyRollupProp (e : OracleRollupEvent) : Prop :=
  let actualInv   : Q16_16 := psiInversion e.M e.adjM e.detM
  let actualGap   : Q16_16 := psiSpectral e.sigma
  let actualSidon : Q16_16 := ofInt (psiSidon e.strands : Int)
  let actualXi    : Q16_16 := add actualInv (add actualGap actualSidon)
  e.psiInv = actualInv ∧ e.psiGap = actualGap ∧ e.psiSidon = actualSidon ∧
  e.xiScore = actualXi ∧ e.xiScore = zero

/-- Executable check (Bool): what the consensus network actually runs. -/
def verifyRollupBool (e : OracleRollupEvent) : Bool :=
  let actualInv   : Q16_16 := psiInversion e.M e.adjM e.detM
  let actualGap   : Q16_16 := psiSpectral e.sigma
  let actualSidon : Q16_16 := ofInt (psiSidon e.strands : Int)
  let actualXi    : Q16_16 := add actualInv (add actualGap actualSidon)
  (e.psiInv == actualInv)     &&
  (e.psiGap == actualGap)     &&
  (e.psiSidon == actualSidon) &&
  (e.xiScore == actualXi)     &&
  (e.xiScore == zero)

/-- The Bridge Theorem: the Bool check is equivalent to the Prop spec. -/
theorem verifyRollup_spec (e : OracleRollupEvent) :
    verifyRollupBool e = true ↔ verifyRollupProp e := by
  unfold verifyRollupBool verifyRollupProp
  -- beq_iff_eq rewrites `a == b` to `a = b` (on the Bool side).
  -- Subtype.ext_iff bridges `a.val = b.val` (from DecidableEq) to `a = b`.
  simp [Bool.and_eq_true, beq_iff_eq, and_assoc, Subtype.ext_iff]

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  Auxiliary lemmas about Q16_16 equality and non-negativity
-- ═══════════════════════════════════════════════════════════════════════════

/-- `ofRawInt` returns `zero` iff the input is 0. -/
lemma ofRawInt_eq_zero_iff (x : Int) : ofRawInt x = zero ↔ x = 0 := by
  constructor
  · intro h
    unfold ofRawInt zero at h
    split at h <;> try split at h
    · -- x > q16MaxRaw → ofRawInt = ⟨q16MaxRaw, …⟩ but that can't equal ⟨0, …⟩
      have : q16MaxRaw ≠ 0 := by norm_num [q16MaxRaw]
      exact absurd (by simpa using h) this
    · -- x < q16MinRaw → ofRawInt = ⟨q16MinRaw, …⟩ ≠ ⟨0, …⟩
      have : q16MinRaw ≠ 0 := by norm_num [q16MinRaw]
      exact absurd (by simpa using h) this
    · -- normal case: ⟨x, …⟩ = ⟨0, …⟩ → x = 0
      simpa using h
  · intro h; subst h; rfl

/-- `add a b = zero` iff `a.val + b.val = 0`. -/
lemma add_eq_zero_iff_val_sum_zero (a b : Q16_16) : add a b = zero ↔ a.val + b.val = 0 := by
  unfold add
  have h : a.toInt + b.toInt = a.val + b.val := by simp [toInt]
  rw [h]
  exact ofRawInt_eq_zero_iff _

/-- If `x ≥ 0` (as Int), then `(ofRawInt x).val ≥ 0`. -/
lemma ofRawInt_val_nonneg (x : Int) (hx : 0 ≤ x) : (ofRawInt x).val ≥ 0 := by
  unfold ofRawInt
  split <;> try split
  · -- x > q16MaxRaw → result = ⟨q16MaxRaw, …⟩, and q16MaxRaw ≥ 0
    have : 0 ≤ q16MaxRaw := by norm_num [q16MaxRaw]
    simpa
  · -- x < q16MinRaw → result = ⟨q16MinRaw, …⟩. But x ≥ 0 contradicts x < min!
    have : q16MinRaw < 0 := by norm_num [q16MinRaw]
    omega
  · -- normal case
    simpa

/-- `(add a b).val ≥ 0` when both `a.val ≥ 0` and `b.val ≥ 0`. -/
lemma add_val_nonneg (a b : Q16_16) (ha : a.val ≥ 0) (hb : b.val ≥ 0) : (add a b).val ≥ 0 := by
  unfold add
  have hsum : 0 ≤ a.val + b.val := by omega
  have h_eq : a.toInt + b.toInt = a.val + b.val := by simp [toInt]
  rw [h_eq]
  exact ofRawInt_val_nonneg (a.val + b.val) hsum

-- ═══════════════════════════════════════════════════════════════════════════
-- §4  Non-negativity lemmas
-- ═══════════════════════════════════════════════════════════════════════════

lemma maxAbsEntry_nonneg (m : Matrix8) : (maxAbsEntry m).val ≥ 0 := by
  unfold maxAbsEntry
  have hax_nonneg (x : Q16_16) : (if x.toInt < 0 then neg x else x).val ≥ 0 := by
    split
    · unfold neg ofRawInt
      have h_nonneg : 0 ≤ -x.toInt := by omega
      split
      · -- clamped to q16MaxRaw (≥ 0)
        have h0 : 0 ≤ q16MaxRaw := by norm_num [q16MaxRaw]
        simpa
      · split
        · -- impossible: -x.toInt ≥ 0 can't be < q16MinRaw which is < 0
          have : q16MinRaw < 0 := by norm_num [q16MinRaw]
          omega
        · dsimp; exact h_nonneg
    · have hx0 : 0 ≤ x.toInt := by omega
      simpa [toInt]
  have h_step_nonneg (ax acc : Q16_16) (hax : ax.val ≥ 0) (hacc : acc.val ≥ 0) :
      (if ax.toInt > acc.toInt then ax else acc).val ≥ 0 := by
    split <;> assumption
  -- Generic lemma: a foldl over any list preserves non-negativity
  have h_fold (l : List Nat) (f : Q16_16 → Nat → Q16_16)
      (hf : ∀ acc i, acc.val ≥ 0 → (f acc i).val ≥ 0)
      (acc : Q16_16) (hacc : acc.val ≥ 0) : ((l.foldl f acc).val) ≥ 0 := by
    induction l generalizing acc with
    | nil => exact hacc
    | cons hd tl ih =>
      have h1 : (f acc hd).val ≥ 0 := hf acc hd hacc
      simpa [List.foldl] using ih (f acc hd) h1
  -- Apply h_fold twice: outer loop over rows, inner loop over columns
  apply h_fold (List.range 8) (fun accI i =>
    (List.range 8).foldl (fun accJ j =>
      let x := getEntry m i j
      let ax := if x.toInt < 0 then neg x else x
      if ax.toInt > accJ.toInt then ax else accJ
    ) accI
  ) ?_ 0 (by
    have h0 : ((0 : Q16_16).val : Int) = (0 : Int) := rfl
    rw [h0])
  intro accI i h_accI
  apply h_fold (List.range 8) (fun accJ j =>
    let x := getEntry m i j
    let ax := if x.toInt < 0 then neg x else x
    if ax.toInt > accJ.toInt then ax else accJ
  ) ?_ accI h_accI
  intro accJ j h_accJ
  dsimp
  apply h_step_nonneg (if (getEntry m i j).toInt < 0 then neg (getEntry m i j) else getEntry m i j) accJ
  · exact hax_nonneg (getEntry m i j)
  · exact h_accJ

/-- `psiInversion` always returns a non-negative value. -/
lemma psiInversion_nonneg (M adjM : Matrix8) (detM : Q16_16) : (psiInversion M adjM detM).val ≥ 0 := by
  unfold psiInversion
  exact maxAbsEntry_nonneg _

/-- `psiSpectral sigma` returns either zero or `ofRawInt (diff*diff)`, both ≥ 0. -/
lemma psiSpectral_nonneg (sigma : Q16_16) : (psiSpectral sigma).val ≥ 0 := by
  unfold psiSpectral
  split
  · rename_i h_lt
    have h_sq_nonneg : 0 ≤ (threshold_1_7.toInt - sigma.toInt) * (threshold_1_7.toInt - sigma.toInt) :=
      mul_nonneg (by omega) (by omega)
    dsimp
    apply ofRawInt_val_nonneg ((threshold_1_7.toInt - sigma.toInt) * (threshold_1_7.toInt - sigma.toInt))
    exact h_sq_nonneg
  · simpa [zero]

/-- `ofInt (psiSidon s : Int)` is always ≥ 0. -/
lemma psiSidon_nonneg (strands : Array Nat) : (ofInt (psiSidon strands : Int)).val ≥ 0 := by
  unfold psiSidon
  split
  · simpa [ofInt, q16Scale, zero]
  · simp [ofInt, q16Scale, q16Clamp, q16MaxRaw, q16MinRaw]

-- ═══════════════════════════════════════════════════════════════════════════
-- §5  The Soundness Theorem  ("God Theorem")
-- ═══════════════════════════════════════════════════════════════════════════

/-- If three non-negative integers sum to zero, each must be zero. -/
lemma sum_zero_of_nonneg {a b c : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c)
    (hsum : a + b + c = 0) : a = 0 ∧ b = 0 ∧ c = 0 := by
  have ha0 : a = 0 := by omega
  have hb0 : b = 0 := by omega
  have hc0 : c = 0 := by omega
  exact ⟨ha0, hb0, hc0⟩

/-- A verified rollup event guarantees that ALL three Ψ invariants are
    simultaneously zero — meaning the prover's witness is correct AND the
    network state satisfies all cold-review conditions.

    This is the "God Theorem": one check replaces three independent proofs. -/
theorem verified_rollup_sound (e : OracleRollupEvent)
    (h_verify : verifyRollupProp e) :
    e.psiInv = zero ∧ e.psiGap = zero ∧ e.psiSidon = zero := by
  rcases h_verify with ⟨h_inv, h_gap, h_sidon, h_xi_sum, h_xi_zero⟩

  -- Ξ = 0 = ψInv + ψGap + ψSidon
  have h_sum_zero : add e.psiInv (add e.psiGap e.psiSidon) = zero := by
    calc
      add e.psiInv (add e.psiGap e.psiSidon)
          = add (psiInversion e.M e.adjM e.detM) (add (psiSpectral e.sigma) (ofInt (psiSidon e.strands : Int))) := by
        simp [h_inv, h_gap, h_sidon]
      _ = e.xiScore := by symm; exact h_xi_sum
      _ = zero := h_xi_zero

  -- Each component is non-negative (by the lemmas in §4)
  have h_nonneg_inv  : e.psiInv.val ≥ 0 := by rw [h_inv]; exact psiInversion_nonneg _ _ _
  have h_nonneg_gap  : e.psiGap.val ≥ 0 := by rw [h_gap]; exact psiSpectral_nonneg _
  have h_nonneg_sidon : e.psiSidon.val ≥ 0 := by rw [h_sidon]; exact psiSidon_nonneg _

  -- The inner add (psiGap + psiSidon) is also non-negative
  have h_nonneg_inner : (add e.psiGap e.psiSidon).val ≥ 0 :=
    add_val_nonneg e.psiGap e.psiSidon h_nonneg_gap h_nonneg_sidon

  -- From `add psiInv (add psiGap psiSidon) = zero`, we get:
  --   psiInv.val + (add psiGap psiSidon).val = 0
  have h_val_sum : e.psiInv.val + (add e.psiGap e.psiSidon).val = 0 :=
    (add_eq_zero_iff_val_sum_zero e.psiInv (add e.psiGap e.psiSidon)).mp h_sum_zero

  -- Both terms are ≥ 0, so each must be 0
  have h_inv_val0 : e.psiInv.val = 0 := by omega
  have h_inner_val0 : (add e.psiGap e.psiSidon).val = 0 := by omega

  -- From `add psiGap psiSidon = zero`, we get psiGap.val + psiSidon.val = 0
  have h_inner_eq_zero : add e.psiGap e.psiSidon = zero := by
    apply Subtype.ext
    simpa using h_inner_val0

  have h_gap_sidon_sum : e.psiGap.val + e.psiSidon.val = 0 :=
    (add_eq_zero_iff_val_sum_zero e.psiGap e.psiSidon).mp h_inner_eq_zero

  -- Both are ≥ 0, so each must be 0
  have h_gap_val0 : e.psiGap.val = 0 := by omega
  have h_sidon_val0 : e.psiSidon.val = 0 := by omega

  -- Lift val=0 to Q16_16 equality
  have h_inv_eq : e.psiInv = zero := by
    apply Subtype.ext; simp [h_inv_val0, zero]
  have h_gap_eq : e.psiGap = zero := by
    apply Subtype.ext; simp [h_gap_val0, zero]
  have h_sidon_eq : e.psiSidon = zero := by
    apply Subtype.ext; simp [h_sidon_val0, zero]

  exact ⟨h_inv_eq, h_gap_eq, h_sidon_eq⟩

-- ═══════════════════════════════════════════════════════════════════════════
-- §6  The executable verifier API (for the consensus layer)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Single-entry point: runs the Bool check and returns the Prop guarantee.
    This is what the consensus node calls after `verifyRollupBool` passes. -/
theorem verify_rollup (e : OracleRollupEvent) (h_ok : verifyRollupBool e = true) :
    e.psiInv = zero ∧ e.psiGap = zero ∧ e.psiSidon = zero :=
  verified_rollup_sound e ((verifyRollup_spec e).mp h_ok)

-- ═══════════════════════════════════════════════════════════════════════════
-- §7  Byte Serialization  (for ledger commitment / Merkle leaf)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Pack a Q16_16 into 4 bytes (big-endian). -/
def packQ16_16 (x : Q16_16) : ByteArray :=
  let v := x.val
  ByteArray.mk (Array.mk [
    (((v / 16777216) % 256).toNat).toUInt8,
    (((v / 65536) % 256).toNat).toUInt8,
    (((v / 256) % 256).toNat).toUInt8,
    ((v % 256).toNat).toUInt8
  ])

/-- Pack a Matrix8 (64 Q16_16 entries → 256 bytes). -/
def packMatrix (m : Matrix8) : ByteArray :=
  (List.range 8).foldl (fun buf i =>
    (List.range 8).foldl (fun buf' j =>
      buf' ++ (packQ16_16 (getEntry m i j))
    ) buf
  ) (ByteArray.mk #[])

/-- Serialize the entire rollup event.

    Layout (bytes):
       0..255    M (64 × 4)
     256..511    adjM (64 × 4)
     512..515    detM (4)
     516..519    sigma (4)
     520..523    psiInv (4)
     524..527    psiGap (4)
     528..531    psiSidon (4)
     532..535    xiScore (4)
     536+        strands (variable, 8 × Nat)

    Total fixed portion: 536 bytes + strands encoding. -/
def serialize (event : OracleRollupEvent) : ByteArray :=
  let buf := packMatrix event.M
  let buf := buf ++ packMatrix event.adjM
  let buf := buf ++ packQ16_16 event.detM
  let buf := buf ++ packQ16_16 event.sigma
  let buf := buf ++ packQ16_16 event.psiInv
  let buf := buf ++ packQ16_16 event.psiGap
  let buf := buf ++ packQ16_16 event.psiSidon
  let buf := buf ++ packQ16_16 event.xiScore
  event.strands.foldl (fun buf' a =>
    buf' ++ (ByteArray.mk (Array.mk [
      (((a / 16777216) % 256).toUInt8),
      (((a / 65536) % 256).toUInt8),
      (((a / 256) % 256).toUInt8),
      ((a % 256).toUInt8)
    ]))
  ) buf

-- ═══════════════════════════════════════════════════════════════════════════
-- §8  Helper: construct the canonical verified event
-- ═══════════════════════════════════════════════════════════════════════════

/-- Build the canonical rollup event (identity8, σ ≥ τ, Golomb strands)
    with the prover supplying identity8 as adjugate and 1 as determinant.
    The `_h_gap` argument enforces the proof obligation at construction site. -/
def canonicalEvent (sigma : Q16_16) (_h_gap : sigma.val ≥ (threshold_1_7).val) : OracleRollupEvent :=
  { M       := identity8
  , sigma   := sigma
  , strands := #[0,1,3,7,12,20,30,44]
  , adjM    := identity8
  , detM    := one
  , psiInv  := zero
  , psiGap  := zero
  , psiSidon := zero
  , xiScore := zero
  }

theorem canonicalEvent_verifies (sigma : Q16_16) (h_gap : sigma.val ≥ (threshold_1_7).val) :
    verifyRollupBool (canonicalEvent sigma h_gap) = true := by
  unfold canonicalEvent verifyRollupBool
  have h_inv : psiInversion identity8 identity8 one = zero := psiInversion_identity
  have h_gap' : psiSpectral sigma = zero := psiSpectral_above sigma (by
    simpa [toInt] using h_gap)
  have h_sidon : psiSidon (#[0,1,3,7,12,20,30,44]) = 0 := psiSidon_canonical
  simp [h_inv, h_gap', h_sidon, add, zero, ofInt, q16Scale]
  dec_trivial

end SilverSight.Rollup
