-- AVM ISA v1 — Goal A: run a canary, construct an RRC record, emit JSON.
--
-- This module is the first end-to-end connection between:
--   AVMIsa.Run     (fuel-bounded execution, Outcome State)
--   ReceiptCore    (receipt ledger, leanBuildReceipt, hasProofReceipt)
--   RRCLogogramProjection (projection/merge admission gates, LogogramReceipt)
--
-- The #eval at the bottom is the "rainbow raccoon compiler" proof-of-life:
-- it runs the boolean-not canary through the AVM, checks the result, mints
-- a receipt, gates it through the RRC projection discipline, and prints the
-- whole bundle as a JSON string that a Python harness can validate.

import SilverSight.AVMIsa.Run
import SilverSight.ReceiptCore
import SilverSight.RRCLogogramProjection
import SilverSight.RRC.Emit
import SilverSight.RRC.Q16_16Manifold

namespace SilverSight.AVMIsa.Emit

open SilverSight.AVMIsa
open SilverSight.ReceiptCore
open SilverSight.RRCLogogramProjection

-- ─────────────────────────────────────────────────────────────────────────────
-- §1  Canary programs
-- ─────────────────────────────────────────────────────────────────────────────

/-- Canary 1: boolean NOT.  Push false → NOT → halt; expect true on stack. -/
def progNot : List Instr :=
  [ Instr.push ⟨AvmTy.bool, AvmVal.b false⟩
  , Instr.prim Prim.not
  , Instr.halt ]

/-- Canary 2: boolean AND.  Push true, push false → AND → halt; expect false. -/
def progAnd : List Instr :=
  [ Instr.push ⟨AvmTy.bool, AvmVal.b true⟩
  , Instr.push ⟨AvmTy.bool, AvmVal.b false⟩
  , Instr.prim Prim.and
  , Instr.halt ]

/-- Canary 3: boolean OR.  Push false, push false → OR → halt; expect false. -/
def progOr : List Instr :=
  [ Instr.push ⟨AvmTy.bool, AvmVal.b false⟩
  , Instr.push ⟨AvmTy.bool, AvmVal.b false⟩
  , Instr.prim Prim.or
  , Instr.halt ]

/-- Canary 4: Q16_16 multiplication (ncDerived computation).
    Push residualRisk=0.47 (raw 30802) → Push scaleBand=0.4 (raw 26214)
    → mulSatQ16 → halt.
    Expected: (30802 * 26214) / 65536 = 12320 (≈ 0.188 in Q16_16). -/
def progMulQ16 : List Instr :=
  [ Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 30802)⟩
  , Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 26214)⟩
  , Instr.prim Prim.mulSatQ16
  , Instr.halt ]

/-- Canary 5: Q16_16 addition (commutativity check).
    Push 0.47 (30802) → Push 0.4 (26214) → addSatQ16 → halt.
    Expected: 30802 + 26214 = 57016 (≈ 0.8698 in Q16_16). -/
def progAddQ16 : List Instr :=
  [ Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 30802)⟩
  , Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 26214)⟩
  , Instr.prim Prim.addSatQ16
  , Instr.halt ]

/-- Canary 6: Q16_16 subtraction (self-inverse check).
    Push 0.47 (30802) → Push 0.47 (30802) → subSatQ16 → halt.
    Expected: 0 (zero). -/
def progSubQ16Self : List Instr :=
  [ Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 30802)⟩
  , Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 30802)⟩
  , Instr.prim Prim.subSatQ16
  , Instr.halt ]

/-- Canary 7: Q16_16 division (inverse of multiplication).
    Push 0.5 (32768) → Push 2.0 (131072) → divSatQ16 → halt.
    Expected: 131072 / (32768/65536) = 131072 * 65536 / 32768 = 262144 (4.0). -/
def progDivQ16 : List Instr :=
  [ Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩
  , Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 131072)⟩
  , Instr.prim Prim.divSatQ16
  , Instr.halt ]

def initState : State :=
  { pc := 0, stack := [], locals := [], halted := false }

-- ─────────────────────────────────────────────────────────────────────────────
-- §2  Canary result classifier
-- ─────────────────────────────────────────────────────────────────────────────

/-- Expected bool value on top of stack after halt. -/
def checkTopBool (outcome : Outcome State) (expected : Bool) : Bool :=
  match outcome with
  | Outcome.err _ => false
  | Outcome.ok s =>
      match s.stack with
      | ⟨AvmTy.bool, AvmVal.b b⟩ :: _ => b == expected && s.halted
      | _ => false

/-- Expected Q16_16 raw value on top of stack after halt. -/
def checkTopQ16 (outcome : Outcome State) (expectedRaw : Int) : Bool :=
  match outcome with
  | Outcome.err _ => false
  | Outcome.ok s =>
      match s.stack with
      | ⟨AvmTy.q16_16, AvmVal.q16 x⟩ :: _ => x.toInt == expectedRaw && s.halted
      | _ => false

-- ─────────────────────────────────────────────────────────────────────────────
-- §3  Canary → ReceiptCore bridge
-- ─────────────────────────────────────────────────────────────────────────────

/-- Run a canary program and mint a leanBuildReceipt keyed on `targetId`. -/
def canaryReceipt (targetId : String) (prog : List Instr) (expected : Bool) : Receipt :=
  let outcome := run 16 prog initState
  let passed  := checkTopBool outcome expected
  leanBuildReceipt targetId passed

/-- Run a Q16_16 canary program and mint a receipt. -/
def canaryReceiptQ16 (targetId : String) (prog : List Instr) (expectedRaw : Int) : Receipt :=
  let outcome := run 32 prog initState
  let passed  := checkTopQ16 outcome expectedRaw
  leanBuildReceipt targetId passed

/-- The baseline canary receipts (boolean + Q16_16 arithmetic). -/
def canaryReceipts : List Receipt :=
  [ canaryReceipt "avm.canary.not" progNot true
  , canaryReceipt "avm.canary.and" progAnd false
  , canaryReceipt "avm.canary.or"  progOr  false
  -- Q16_16 arithmetic canaries (cross-verified with SymPy)
  , canaryReceiptQ16 "avm.canary.mul_q16" progMulQ16 12320    -- 0.47 * 0.4 = 0.188
  , canaryReceiptQ16 "avm.canary.add_q16" progAddQ16 57016    -- 0.47 + 0.4 = 0.87
  , canaryReceiptQ16 "avm.canary.sub_q16_self" progSubQ16Self 0  -- x - x = 0
  , canaryReceiptQ16 "avm.canary.div_q16" progDivQ16 262144   -- 2.0 / 0.5 = 4.0
  ]

-- ─────────────────────────────────────────────────────────────────────────────
-- §4  RRC LogogramReceipt for the AVM canary bundle
-- ─────────────────────────────────────────────────────────────────────────────

/-- Build an RRC LogogramReceipt reflecting whether all canaries passed.
    If all three pass → normal projection (uglyAsymmetricPruning, no tear).
    If any fail → horribleManifoldTearing (force into quarantine projection). -/
def canaryLogogramReceipt (allPassed : Bool) : LogogramReceipt :=
  if allPassed then
    { shape               := RRCShape.logogramProjection
      status              := WitnessStatus.candidate
      regime              := SemanticRegime.uglyAsymmetricPruning
      payloadBound        := true
      contradictionWitness := false
      tearBoundary        := false
      detachedMass        := false
      residualLane        := false }
  else
    { shape               := RRCShape.logogramProjection
      status              := WitnessStatus.candidate
      regime              := SemanticRegime.horribleManifoldTearing
      payloadBound        := true
      contradictionWitness := false
      tearBoundary        := false
      detachedMass        := false
      residualLane        := false }

-- ─────────────────────────────────────────────────────────────────────────────
-- §5  Minimal JSON serializer (no Float, no external deps)
-- ─────────────────────────────────────────────────────────────────────────────

private def jsonBool (b : Bool) : String := if b then "true" else "false"

private def jsonStr (s : String) : String :=
  -- Escape the handful of chars that appear in our strings
  let escaped := s.replace "\\" "\\\\" |>.replace "\"" "\\\""
  s!"\"{escaped}\""

private def jsonReceiptKind : ReceiptKind → String
  | .leanBuild        => "\"leanBuild\""
  | .benchmark        => "\"benchmark\""
  | .sourceAudit      => "\"sourceAudit\""
  | .reverseCollapse  => "\"reverseCollapse\""
  | .deltaPhiAudit    => "\"deltaPhiAudit\""
  | .adversarialTrial => "\"adversarialTrial\""
  | .humanReview      => "\"humanReview\""
  | .wardenEmission   => "\"wardenEmission\""
  | .externalProof    => "\"externalProof\""

private def jsonReceipt (r : Receipt) : String :=
  s!"\{\"kind\":{jsonReceiptKind r.kind},\"targetId\":{jsonStr r.targetId}," ++
  s!"\"summary\":{jsonStr r.summary},\"valid\":{jsonBool r.valid}," ++
  s!"\"authority\":{jsonStr r.authority},\"timestamp\":{r.timestamp}}"

private def jsonRRCShape : RRCShape → String
  | .signalShapedRouteCompiler          => "\"signalShapedRouteCompiler\""
  | .projectableGeometryTopology        => "\"projectableGeometryTopology\""
  | .cognitiveLoadField                 => "\"cognitiveLoadField\""
  | .cadForceProbeReceipt               => "\"cadForceProbeReceipt\""
  | .logogramProjection                 => "\"logogramProjection\""
  | .holdForUnlawfulOrUnderspecifiedShape => "\"holdForUnlawfulOrUnderspecifiedShape\""

private def jsonRegime : SemanticRegime → String
  | .beautifulTopologicalFolding => "\"beautifulTopologicalFolding\""
  | .uglyAsymmetricPruning       => "\"uglyAsymmetricPruning\""
  | .horribleManifoldTearing     => "\"horribleManifoldTearing\""

private def jsonLane : ProjectionLane → String
  | .normalProjection    => "\"normalProjection\""
  | .quarantineProjection => "\"quarantineProjection\""

private def jsonLogogramReceipt (lr : LogogramReceipt) : String :=
  s!"\{\"shape\":{jsonRRCShape lr.shape},\"regime\":{jsonRegime lr.regime}," ++
  s!"\"projectionAdmissible\":{jsonBool (projectionAdmissible lr)}," ++
  s!"\"mergeAdmissible\":{jsonBool (mergeAdmissible lr)}," ++
  s!"\"lane\":{jsonLane (projectionLane lr)}}"

private def jsonReceiptList (rs : List Receipt) : String :=
  "[" ++ String.intercalate "," (rs.map jsonReceipt) ++ "]"

-- ─────────────────────────────────────────────────────────────────────────────
-- §6  Top-level emit
-- ─────────────────────────────────────────────────────────────────────────────

structure EmitResult where
  allPassed        : Bool
  receipts         : List Receipt
  logogramReceipt  : LogogramReceipt
  projectionPassed : Bool
  json             : String
  deriving Repr

def emit : EmitResult :=
  let rs         := canaryReceipts
  let allPassed  := rs.all (·.valid)
  let lr         := canaryLogogramReceipt allPassed
  let projOk     := projectionAdmissible lr
  let jsonBody   :=
    s!"\{\"schema\":\"avm_canary_emit_v1\"," ++
    s!"\"all_canaries_passed\":{jsonBool allPassed}," ++
    s!"\"receipts\":{jsonReceiptList rs}," ++
    s!"\"rrc_logogram\":{jsonLogogramReceipt lr}," ++
    s!"\"projection_passed\":{jsonBool projOk}}"
  { allPassed       := allPassed
    receipts        := rs
    logogramReceipt := lr
    projectionPassed := projOk
    json            := jsonBody }

-- ─────────────────────────────────────────────────────────────────────────────
-- §7  RRC fixture corpus stamping (6-row fixture corpus → AVM-stamped receipt bundle)
--
--     Architecture:
--       SilverSight.RRC.Emit       — alignment gate (Lean classifies)
--       SilverSight.AVMIsa.Emit    — AVM stamps final receipt + emits JSON (here)
--
--     The AVM is the sole output boundary.  RRC.Emit feeds it; AVMIsa.Emit
--     stamps it.  Promotion remains not_promoted at this stage.
-- ─────────────────────────────────────────────────────────────────────────────

open SilverSight.RRC.Emit in
/-- Stamp the 6-row fixture corpus: run the alignment gate (RRC.Emit), then
    mint an AVM-authority receipt for the whole bundle, and emit JSON.

    The AVM canary suite must pass for the bundle receipt to be valid.
    Individual row receipts reflect alignment-gate pass/fail independently. -/
def emitFixtureCorpus : String :=
  -- 1. Classify all 6 fixture rows through the alignment gate
  let classified := emitCorpus "rrc_emit_fixture_v1" fixtureCorpus
  -- 2. Run AVM canaries — AVM must be live for the bundle to be valid
  let avmOk      := canaryReceipts.all (·.valid)
  -- 3. Mint AVM-authority bundle receipt
  let bundleReceipt := leanBuildReceipt "avm.rrc_fixture.bundle" avmOk
  -- 4. Compute summary statistics
  let total      := classified.totalRows
  let passed     := classified.candidateRows
  let held       := total - passed
  -- 5. Emit JSON — AVM is the output boundary.
  let summaryStr :=
    s!"\{\"total\":{total},\"passed_alignment\":{passed},\"held\":{held}," ++
    s!"\"not_promoted\":{total}}"
  s!"\{\"schema\":\"avm_rrc_fixture_v1\"," ++
  s!"\"claim_boundary\":\"admissibility-and-routing-pass-only;not-promoted\"," ++
  s!"\"avm_canaries_passed\":{jsonBool avmOk}," ++
  s!"\"bundle_receipt_valid\":{jsonBool bundleReceipt.valid}," ++
  s!"\"summary\":{summaryStr}," ++
  s!"\"rows\":{classified.rowsJson}}"

open SilverSight.RRC.Q16_16Manifold in
/-- Stamp the full manifold: run the alignment gate (RRC.Emit), then
    mint an AVM-authority receipt for the whole bundle, and emit JSON.

    The AVM canary suite must pass for the bundle receipt to be valid.
    Individual row receipts reflect alignment-gate pass/fail independently. -/
def emitManifold : String :=
  let classified := SilverSight.RRC.Emit.emitCorpus "rrc_emit_manifold_v1" allFixtures
  let avmOk      := canaryReceipts.all (·.valid)
  let bundleReceipt := leanBuildReceipt "avm.rrc.manifold.bundle" avmOk
  let total      := classified.totalRows
  let passed     := classified.candidateRows
  let held       := total - passed
  let summaryStr :=
    s!"\{\"total\":{total},\"passed_alignment\":{passed},\"held\":{held}," ++
    s!"\"not_promoted\":{total}}"
  s!"\{\"schema\":\"avm_rrc_manifold_v1\"," ++
    s!"\"claim_boundary\":\"admissibility-and-routing-pass-only;not-promoted\"," ++
    s!"\"avm_canaries_passed\":{jsonBool avmOk}," ++
    s!"\"bundle_receipt_valid\":{jsonBool bundleReceipt.valid}," ++
    s!"\"summary\":{summaryStr}," ++
    s!"\"rows\":{classified.rowsJson}}"

-- ─────────────────────────────────────────────────────────────────────────────
-- §8  Proof-of-life eval witnesses
-- ─────────────────────────────────────────────────────────────────────────────

-- Individual canary checks
#eval checkTopBool (run 16 progNot initState) true    -- expect: true
#eval checkTopBool (run 16 progAnd initState) false   -- expect: true
#eval checkTopBool (run 16 progOr  initState) false   -- expect: true

-- Q16_16 arithmetic canary checks (cross-verified with SymPy)
-- 0.47 * 0.4 = 0.188; raw = (30802 * 26214) / 65536 = 12320
#eval checkTopQ16 (run 32 progMulQ16 initState) 12320     -- expect: true
-- 0.47 + 0.4 = 0.87; raw = 30802 + 26214 = 57016
#eval checkTopQ16 (run 32 progAddQ16 initState) 57016     -- expect: true
-- 0.47 - 0.47 = 0; raw = 0
#eval checkTopQ16 (run 32 progSubQ16Self initState) 0      -- expect: true
-- 2.0 / 0.5 = 4.0; raw = (131072 * 65536) / 32768 = 262144
#eval checkTopQ16 (run 32 progDivQ16 initState) 262144    -- expect: true

-- Receipt validity: all canaries (boolean + Q16_16) must be valid
-- expect: 7 receipts, all true
#eval canaryReceipts.length  -- expect: 7
#eval canaryReceipts.map (fun r => (r.targetId, r.valid))

-- Full canary JSON bundle: schema="avm_canary_emit_v1", all_canaries_passed=true, 7 receipts
-- expect: JSON with schema "avm_canary_emit_v1", all_canaries_passed=true, projection_passed=true
#eval emit.json

-- 6-row fixture corpus: AVM stamps the bundle, RRC.Emit classifies rows.
-- expect: (6, 3, 3)
open SilverSight.RRC.Emit in
#eval
  let r := emitCorpus "rrc_emit_fixture_v1" fixtureCorpus
  (r.totalRows, r.candidateRows, r.totalRows - r.candidateRows)

-- Full fixture-corpus JSON: AVM-stamped, 6 rows, claim_boundary, schema=avm_rrc_fixture_v1.
-- expect: JSON string starting with {"schema":"avm_rrc_fixture_v1",...}
#eval emitFixtureCorpus

-- Full manifold receipt: schema, claim boundary, row count, bundle validity.
-- expect: all true
#eval String.contains emitManifold "avm_rrc_manifold_v1"
#eval String.contains emitManifold "admissibility-and-routing-pass-only"
#eval String.contains emitManifold "\"total\":278"
#eval String.contains emitManifold "\"bundle_receipt_valid\":true"

end SilverSight.AVMIsa.Emit
