/-
  SilverSight Core — The Self-Indexing Dual-Domain Machine
  ========================================================

  This is the MINIMAL core. Nothing else belongs here.

  The core defines:
    1. The 8 Hachimoji states (the alphabet of classification)
    2. The receipt format (the interface between core and libraries)
    3. The AVM transition function δ : S × I → S'
    4. The TIC axiom (TIC is derived, not a driver)
    5. The loop invariant (computation generates time)

  What this file does NOT contain:
    - Chaos game implementation (library: SearchLib)
    - Finsler metric computation (library: MetricLib)
    - QUBO/QAOA optimization (library: OptimizeLib)
    - Token parsing (library: LexLib)
    - PVGS bridge (library: QuantumLib)
    - Chirality classification (library: StructureLib)
    - TIC counter implementation (library: EventLib)
    - Receipt validation (library: AuditLib)

  Library method: core defines the contract. Libraries implement it.
  No library code in core. No core code depends on libraries.

  Author: allaunthefox
  Date: 2026-06-21
  License: MIT
-/

import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.DeriveFintype
import Mathlib.Tactic

namespace SilverSight.Core

-- =============================================================================
-- §1. THE 8 HACHIMOJI STATES
-- =============================================================================

/-  The 8 Hachimoji states are the classification alphabet.
    Every mathematical expression resolves to one of these 8 states.
    This is the OUTPUT of the core machine.

    Φ (Phi)    — trivial, well-understood, admits immediately
    Λ (Lambda) — room for exploration, interesting but tractable
    Ρ (Rho)    — tight, requires specific tools or conditions
    Κ (Kappa)  — marginal, edge case, may need special handling
    Ω (Omega)  — collision, contradiction, quarantine
    Σ (Sigma)  — symmetric, balanced, multiple valid interpretations
    Π (Pi)     — potential, promising direction for further work
    Ζ (Zeta)   — zero, undefined, no-information state
-/

inductive HachimojiState
  | Φ | Λ | Ρ | Κ | Ω | «Σ» | «Π» | Ζ
  deriving DecidableEq, Repr, Fintype, BEq

def HachimojiState.toString : HachimojiState → String
  | .Φ => "Φ" | .Λ => "Λ" | .Ρ => "Ρ" | .Κ => "Κ"
  | .Ω => "Ω" | .«Σ» => "Σ" | .«Π» => "Π" | .Ζ => "Ζ"

instance : ToString HachimojiState := ⟨HachimojiState.toString⟩

-- =============================================================================
-- §2. THE RECEIPT FORMAT (interface between core and libraries)
-- =============================================================================

/-  The Receipt is the ONLY interface between the core and libraries.
    Libraries produce receipts. The core consumes them.
    Nothing else crosses the boundary.

    receiptID     — unique identifier for this classification
    expression    — the input expression (as a string)
    finalState    — the Hachimoji state assigned
    ticCount      — how many events occurred during classification
    fuelUsed      — how many iterations were expended
    pathCost      — Finsler distance traversed (if available)
    libraryRefs   — which libraries contributed to the classification
    verified      — whether the result has been independently checked
-/

structure Receipt where
  receiptID     : String
  expression    : String
  finalState    : HachimojiState
  ticCount      : Nat
  fuelUsed      : Nat
  pathCost      : Option Nat   -- raw integer cost metric (Q16_16 raw value or 0); never Float
  libraryRefs   : List String
  verified      : Bool
  deriving DecidableEq, Repr, BEq

-- Empty receipt (no classification performed)
def Receipt.empty : Receipt :=
  { receiptID     := ""
  , expression    := ""
  , finalState    := .Ζ
  , ticCount      := 0
  , fuelUsed      := 0
  , pathCost      := none
  , libraryRefs   := []
  , verified      := false
  }

-- Receipt is valid if it has an ID and a non-zero state
@[simp] def Receipt.isValid (r : Receipt) : Bool :=
  r.receiptID.length > 0 && r.finalState != .Ζ

-- =============================================================================
-- §3. THE AVM TRANSITION FUNCTION δ : S × I → S'
-- =============================================================================

/-  The AVM (Abstract Virtual Machine) is a stack machine with:
    - A single stack of HachimojiStates
    - A fuel counter (prevents infinite loops)
    - An instruction type

    Instructions are what libraries produce. The core only executes them.
-/

inductive Instruction
  | Classify    (expr : String)              -- classify expression, push result
  | LookupLib   (name : String)              -- reference a library
  | Merge       (s1 s2 : HachimojiState)     -- combine two states
  | Reflect     (fuel : Nat)                 -- chaos game reflection step
  | Verify      (receipt : Receipt)          -- verify a receipt
  | Halt                                      -- stop execution
  deriving DecidableEq, Repr

def Instruction.toString : Instruction → String
  | .Classify expr    => s!"Classify({expr})"
  | .LookupLib name   => s!"LookupLib({name})"
  | .Merge s1 s2      => s!"Merge({s1}, {s2})"
  | .Reflect fuel     => s!"Reflect({fuel})"
  | .Verify r         => s!"Verify({r.receiptID})"
  | .Halt             => "Halt"

instance : ToString Instruction := ⟨Instruction.toString⟩

-- The AVM state
structure AVMState where
  stack      : List HachimojiState  -- computation stack
  fuel       : Nat                  -- remaining fuel
  tic        : Nat                  -- current TIC count
  history    : List Instruction     -- executed instructions
  deriving Repr, BEq

def AVMState.initial (fuel : Nat) : AVMState :=
  { stack := [], fuel := fuel, tic := 0, history := [] }

-- δ : S × I → S'  (state transition function)
def δ (s : AVMState) (i : Instruction) : AVMState :=
  if s.fuel = 0 then
    -- Out of fuel: halt
    { s with history := s.history ++ [.Halt] }
  else
    let s' := { s with fuel := s.fuel - 1, tic := s.tic + 1,
                       history := s.history ++ [i] }
    match i with
    | .Classify _expr    => { s' with stack := .Φ :: s'.stack }  -- default: Φ
    | .LookupLib _name   => s'  -- library lookup (no stack change)
    | .Merge s1 s2       =>
        -- Merge: take the "more informative" state
        let merged := match (s1, s2) with
          | (.Ω, _) | (_, .Ω) => .Ω  -- contradiction dominates
          | (.Ζ, s) | (s, .Ζ) => s   -- non-zero dominates
          | (s, _)             => s   -- first wins (default)
        { s' with stack := merged :: s'.stack.tailD [] }
    | .Reflect _fuel     => { s' with tic := s'.tic + 1 }  -- reflection costs extra
    | .Verify _receipt   => s'  -- verification (no stack change)
    | .Halt              => { s' with fuel := 0 }  -- force halt

-- Run a program (list of instructions) from initial state
def runAVM (program : List Instruction) (fuel : Nat) : AVMState :=
  let initial := AVMState.initial fuel
  program.foldl δ initial

-- Extract the top of stack as the final state
def AVMState.result (s : AVMState) : HachimojiState :=
  s.stack.headD .Ζ

-- =============================================================================
-- §4. THE TIC AXIOM (TIC is derived, not a driver)
-- =============================================================================

/-  AXIOM: The TIC clock is strictly derived from physical events.
    It is NEVER the driver of computation.

    Formally:
      T_{n+1} = T_n + E(S_n, τ)

    Where:
      T_n     = TIC count at step n
      S_n     = AVM state at step n
      τ       = metric distance (parameter)
      E       = event detection function (E ≥ 0)

    CRITICAL: There is NO inverse function:
      ∄ F such that T_n → S_n

    The TIC counts events. It does not cause them.
-/

-- Event detection: every state transition produces exactly 1 event
@[simp] def eventDetect (s s' : AVMState) : Nat :=
  if s != s' then 1 else 0

-- TIC update: derived from events
@[simp] def ticUpdate (T : Nat) (events : Nat) : Nat :=
  T + events

-- TIC is monotonically non-decreasing
lemma tic_monotone (T : Nat) (events : Nat) :
    ticUpdate T events ≥ T := by
  simp [ticUpdate]

-- δ never decreases TIC. When fuel > 0, it strictly increases TIC.
lemma δ_tic_monotone (s : AVMState) (i : Instruction) :
    (δ s i).tic ≥ s.tic := by
  simp [δ]
  split_ifs with h_fuel
  · -- fuel = 0: δ appends Halt and changes nothing else
    simp
  · -- fuel > 0: δ decrements fuel, increments tic, records instruction
    cases i <;> simp
    all_goals omega

-- foldl preserves the TIC lower bound
lemma foldl_tic_monotone (s : AVMState) (program : List Instruction) :
    (List.foldl δ s program).tic ≥ s.tic := by
  induction program generalizing s with
  | nil => simp
  | cons i rest ih =>
      simp [List.foldl]
      have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
      have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i)
      exact Nat.le_trans h_step h_rest

-- The TIC axiom: TIC never decreases
theorem tic_never_decreases (program : List Instruction) (fuel : Nat) :
    (runAVM program fuel).tic ≥ (AVMState.initial fuel).tic := by
  simp [runAVM]
  -- Invariant: foldl preserves tic ≥ starting tic
  generalize AVMState.initial fuel = s
  induction program generalizing s with
  | nil => simp
  | cons i rest ih =>
    simp [List.foldl]
    have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
    have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i)
    exact Nat.le_trans h_step h_rest

-- =============================================================================
-- §5. LOOP INVARIANT (computation generates time)
-- =============================================================================

/-  THEOREM: Computation generates its own temporal index.

    For any terminating program P:
      finalState(P) ≠ Ζ  →  ticCount > 0

    Meaningful computation always consumes at least 1 unit of "time"
    (where time is measured in events, not seconds).
-/

-- If the final TIC equals the starting TIC, the stack never changed.
lemma foldl_tic_eq_start (s : AVMState) (program : List Instruction)
    (h : (List.foldl δ s program).tic = s.tic) :
    (List.foldl δ s program).stack = s.stack := by
  induction program generalizing s with
  | nil =>
    simp at h ⊢
  | cons i rest ih =>
    simp [List.foldl] at h ⊢
    have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i
    have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic :=
      foldl_tic_monotone (δ s i) rest
    have h_eq : (δ s i).tic = s.tic := by linarith
    have h_fuel0 : s.fuel = 0 := by
      by_contra h_fuel
      have hf : s.fuel > 0 := by omega
      have h_ne : s.fuel ≠ 0 := by omega
      have h_strict : (δ s i).tic > s.tic := by
        simp [δ, h_ne]
        cases i <;> simp
      linarith
    have h_stack : (δ s i).stack = s.stack := by simp [δ, h_fuel0]
    have h_fuel : (δ s i).fuel = s.fuel := by simp [δ, h_fuel0]
    have h_tic : (δ s i).tic = s.tic := h_eq
    have h_final_eq : (List.foldl δ (δ s i) rest).tic = (δ s i).tic := by linarith
    have h_final_stack : (List.foldl δ (δ s i) rest).stack = (δ s i).stack :=
      ih (δ s i) h_final_eq
    rw [h_stack] at h_final_stack
    exact h_final_stack

-- Corollary: if the starting TIC is 0 and the final TIC is 0, the stack is empty.
lemma runAVM_tic_zero_stack_empty (program : List Instruction) (fuel : Nat)
    (h : (runAVM program fuel).tic = 0) :
    (runAVM program fuel).stack = [] := by
  simp [runAVM] at h ⊢
  have h_eq : (List.foldl δ (AVMState.initial fuel) program).tic = (AVMState.initial fuel).tic := by
    simp [AVMState.initial] at h ⊢
    linarith
  have h_stack : (List.foldl δ (AVMState.initial fuel) program).stack = (AVMState.initial fuel).stack :=
    foldl_tic_eq_start (AVMState.initial fuel) program h_eq
  rw [h_stack]
  simp [AVMState.initial]

theorem computation_generates_time (program : List Instruction) (fuel : Nat)
    (h_nonzero : (runAVM program fuel).result ≠ .Ζ)
    (_h_terminates : (runAVM program fuel).fuel > 0 ∨ program.length > 0) :
    (runAVM program fuel).tic > 0 := by
  -- Contrapositive: if final TIC is 0, the stack stayed empty, so result = Ζ.
  by_contra h
  have h_tic : (runAVM program fuel).tic = 0 := by omega
  have h_stack : (runAVM program fuel).stack = [] :=
    runAVM_tic_zero_stack_empty program fuel h_tic
  have h_result : (runAVM program fuel).result = .Ζ := by
    simp [AVMState.result, h_stack]
  contradiction

-- =============================================================================
-- §6. LIBRARY INTERFACE
-- =============================================================================

/-  Libraries plug into the core via the Receipt interface.
    A library is any function that takes an expression and produces a Receipt.

    Core types:
      Library : String → Receipt

    No library code in core. No core code depends on libraries.
    This is the library method.
-/

-- Library function type
abbrev Library := String → Receipt

-- Execute a library and return the receipt
def execLibrary (lib : Library) (expr : String) : Receipt :=
  lib expr

-- Compose libraries: try lib1, fall back to lib2
def Library.orElse (lib1 lib2 : Library) : Library :=
  fun expr =>
    let r1 := lib1 expr
    if r1.isValid then r1 else lib2 expr

-- Run multiple libraries and merge their receipts
def runLibraries (libs : List Library) (expr : String) : Receipt :=
  let receipts := libs.map (fun lib => lib expr)
  -- Take the first valid receipt, or empty
  receipts.find? (fun r => r.isValid) |>.getD Receipt.empty

-- =============================================================================
-- §7. CORE RECEIPT VALIDATORS (part of the core, not a library)
-- =============================================================================

/-  The core includes basic receipt validators because receipt integrity
    is part of the machine's correctness, not a library concern.
-/

-- Receipt has consistent TIC count (non-negative, matches fuel used)
def Receipt.ticConsistent (r : Receipt) : Bool :=
  r.ticCount > 0 → r.fuelUsed > 0

-- Receipt references only known states
def Receipt.stateValid (r : Receipt) : Bool :=
  r.finalState != .Ζ

-- Full receipt validation (core only)
def Receipt.coreValid (r : Receipt) : Bool :=
  r.isValid && r.ticConsistent && r.stateValid

end SilverSight.Core