import Semantics.FixedPoint
import Semantics.BraidStrand
import Semantics.BraidBracket
import Semantics.MeshRouting
import Semantics.BraidField
import Semantics.BraidEigensolid
import Semantics.BraidDiatCodec

/-!
# BraidVCNBridge — Map braid operations to VCN frame encoding.

Bridges the braid algebra (BraidStrand, BraidBracket) to the VCN video encode
substrate for GPU-accelerated computation.

Convergence, invertibility, mountain merge, and PISTField frame encoding are
delegated to the canonical proven modules:
  - `Semantics.BraidEigensolid`  — `eigensolid_convergence`, `receipt_invertible`
  - `Semantics.BraidDiatCodec`   — `MountainPacked`, `BraidDiatFrame.encode`/`decode`,
                                    `encode_decode_roundtrip`
-/

namespace Semantics.BraidVCNBridge

open Semantics
open Semantics.BraidBracket
open Semantics.BraidBracket.BraidBracket
open Semantics.BraidStrand

def encodeBraidStrand (s : BraidStrand) : Array UInt8 :=
  let px := s.phaseAcc.x.val.toNat
  let py := s.phaseAcc.y.val.toNat
  let mag := s.magnitude.val.toNat
  let gap := s.bracket.gap.val.toNat
  let packQ16 (v : Nat) : Array UInt8 :=
    #[ UInt8.ofNat (v % 256),
       UInt8.ofNat ((v / 256) % 256),
       UInt8.ofNat ((v / 65536) % 256),
       UInt8.ofNat ((v / 16777216) % 256) ]
  packQ16 px ++ packQ16 py ++ packQ16 mag ++ packQ16 gap

def encodeBraidCrossing (bij bi bj : BraidBracket) : Array UInt8 :=
  let res := crossingResidual bij bi bj
  let packQ16 (v : Q16_16) : Array UInt8 :=
    let n := v.val.toNat
    #[ UInt8.ofNat (n % 256),
       UInt8.ofNat ((n / 256) % 256),
       UInt8.ofNat ((n / 65536) % 256),
       UInt8.ofNat ((n / 16777216) % 256) ]
  packQ16 res.lower ++ packQ16 res.upper ++
  packQ16 res.gap ++ packQ16 res.kappa ++ packQ16 res.phi

-- ============================================================
-- §2. MOUNTAIN MERGE ENCODING (delegates to BraidDiatCodec)
-- ============================================================

/-- Mountain merge encoding — delegates to the proven `MountainPacked.fromMountain`
    in `Semantics.BraidDiatCodec`. The `BraidDiatFrame.encode_decode_roundtrip`
    theorem covers the mountain merge layer's roundtrip. -/
def encodeMountain (m : BraidField.Mountain) : BraidDiatCodec.MountainPacked :=
  BraidDiatCodec.MountainPacked.fromMountain m

/-- Decode a packed mountain back to `BraidField.Mountain` (inner MMR reattached
    as empty by the codec; full MMR is reconstructed at the frame level). -/
def decodeMountain (p : BraidDiatCodec.MountainPacked) : BraidField.Mountain :=
  BraidDiatCodec.MountainPacked.toMountain p

-- ============================================================
-- §3. PISTFIELD FRAME ENCODING (delegates to BraidDiatCodec)
-- ============================================================

/-- PISTField frame encoding — delegates to `BraidDiatFrame.encode` in
    `Semantics.BraidDiatCodec`, which packages `SpherionState` + `BraidReceipt`
    into a VCN-compatible frame. The `encode_decode_roundtrip` theorem proves
    the frame bijectively recovers the recoverable fields. -/
def encodeFrame (state : BraidField.SpherionState)
                (receipt : BraidEigensolid.BraidReceipt)
                (slotChirality : EntropyMeasures.Chirality)
                (slotN : UInt32)
                (residuals : Array BraidDiatCodec.BraidResidualPacked)
                (qr : Option BraidDiatCodec.QRPacked := none) :
                Option BraidDiatCodec.BraidDiatFrame :=
  BraidDiatCodec.BraidDiatFrame.encode state receipt slotChirality slotN residuals qr

/-- PISTField frame decoding — delegates to `BraidDiatFrame.decode` in
    `Semantics.BraidDiatCodec`. -/
def decodeFrame (frame : BraidDiatCodec.BraidDiatFrame) :
    Option (BraidField.SpherionState × BraidEigensolid.BraidReceipt ×
            EntropyMeasures.Chirality × UInt32 × Option BraidDiatCodec.QRPacked) :=
  BraidDiatCodec.BraidDiatFrame.decode frame

-- ============================================================
-- §4. EIGENSOLID CONVERGENCE (delegates to BraidEigensolid)
-- ============================================================

/-- Eigensolid convergence — delegates to the proven theorem in
    `Semantics.BraidEigensolid`. The braid crossing loop stabilizes once
    `crossStep s` is an eigensolid:
      `∀ i, (crossStep (crossStep s)).strands i = (crossStep s).strands i` -/
theorem eigensolid_convergence
    (s : BraidEigensolid.BraidState)
    (h_eig : BraidEigensolid.IsEigensolid (BraidEigensolid.crossStep s)) :
    ∀ i : Fin 8,
      (BraidEigensolid.crossStep (BraidEigensolid.crossStep s)).strands i =
      (BraidEigensolid.crossStep s).strands i :=
  BraidEigensolid.eigensolid_convergence s h_eig

-- ============================================================
-- §5. RECEIPT INVERTIBILITY (delegates to BraidEigensolid)
-- ============================================================

/-- Receipt invertibility — delegates to the proven theorem in
    `Semantics.BraidEigensolid`. Equal receipts ⇒ equal per-strand residues,
    strand-0 bracket, strand-7 slot, and step counts. -/
theorem receipt_invertible
    (s1 s2 : BraidEigensolid.BraidState)
    (h_eig1 : BraidEigensolid.IsEigensolid s1)
    (h_eig2 : BraidEigensolid.IsEigensolid s2)
    (h_receipt : BraidEigensolid.encodeReceipt s1 = BraidEigensolid.encodeReceipt s2) :
    (∀ i : Fin 8, (s1.strands i).residue = (s2.strands i).residue) ∧
    (s1.strands ⟨0, by decide⟩).bracket = (s2.strands ⟨0, by decide⟩).bracket ∧
    (s1.strands ⟨7, by decide⟩).slot = (s2.strands ⟨7, by decide⟩).slot ∧
    s1.step_count = s2.step_count :=
  BraidEigensolid.receipt_invertible s1 s2 h_eig1 h_eig2 h_receipt

end Semantics.BraidVCNBridge