-- AVM ISA v1 (Lean-only): Run semantics (fuel-bounded)

import SilverSight.AVMIsa.Step

namespace SilverSight.AVMIsa

/-- Fuel for total execution. -/
abbrev Fuel := Nat

/-- Fuel-bounded run.

Stops when:
- fuel exhausted
- machine halted
- an error occurs
-/
def run (fuel : Fuel) (program : List Instr) (s : State) : Outcome State :=
  match fuel with
  | 0 => Outcome.ok s
  | Nat.succ f =>
      if s.halted then Outcome.ok s
      else
        match step program s with
        | Outcome.err e => Outcome.err e
        | Outcome.ok s1 => run f program s1

/-- Canary: boolean not.

#eval should produce `true` on top of stack.
-/
def canaryNot : List Instr :=
  [
    Instr.push ⟨AvmTy.bool, AvmVal.b false⟩,
    Instr.prim Prim.not,
    Instr.halt
  ]

/-- Canary: Q16.16 multiplication.
    Push 1.0 (65536) → Push 0.5 (32768) → mulSatQ16 → halt.
    Expect 0.5 (32768) on top of stack. -/
def canaryMul : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
    Instr.prim Prim.mulSatQ16,
    Instr.halt
  ]

/-- Canary: Q16.16 division.
    Push 2.0 (131072) → Push 0.5 (32768) → divSatQ16 → halt.
    Divides second by first: 2.0 / 0.5 = 4.0 (262144).
    Expect 4.0 (262144) on top of stack. -/
def canaryDiv : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 131072)⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
    Instr.prim Prim.divSatQ16,
    Instr.halt
  ]

/-- Canary: Q16.16 comparison.
    Push 1.0 (65536) → Push 0.5 (32768) → ltQ16 → halt.
    Compares second < first: 1.0 < 0.5 = false.
    Expect false on top of stack. -/
def canaryLt : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 32768)⟩,
    Instr.prim Prim.ltQ16,
    Instr.halt
  ]

/-- Canary initial state. -/
def canaryState : State :=
  { pc := 0, stack := [], locals := [], halted := false }

#eval run 8 canaryNot canaryState
#eval run 8 canaryMul canaryState
#eval run 8 canaryDiv canaryState
#eval run 8 canaryLt canaryState

-- ─────────────────────────────────────────────────────────────────────────────
-- §V1/V2  Overflow safety witnesses
-- ─────────────────────────────────────────────────────────────────────────────

-- V1 witness: worst-case mul intermediate fits Int64.
-- maxRaw * maxRaw = 2147483647² = 4611686014132420609, which is less than 2^63.
#eval do
  let maxRaw : Int := 2147483647
  let prod := maxRaw * maxRaw
  -- 2^63 = 9223372036854775808
  let int64Max : Int := 9223372036854775808
  let fits := if prod < int64Max then "true" else "false"
  IO.println s!"V1 mul worst-case intermediate: {prod}, fits Int64: {fits}"

-- V2 witness: worst-case div intermediate fits Int64.
-- maxRaw * 65536 = 2147483647 * 65536 = 140737488289792, which is less than 2^63.
#eval do
  let maxRaw : Int := 2147483647
  let prod := maxRaw * 65536
  let int64Max : Int := 9223372036854775808
  let fits := if prod < int64Max then "true" else "false"
  IO.println s!"V2 div worst-case intermediate: {prod}, fits Int64: {fits}"

-- ─────────────────────────────────────────────────────────────────────────────
-- §V4  Rounding direction conformance witness
-- ─────────────────────────────────────────────────────────────────────────────

-- V4 witness: Lean Int.div is EUCLIDEAN (remainder always ≥ 0).
--   -6 / 65536 = -1 (not 0 as in C99 truncation, not -1 as in floor [same here]).
--   For POSITIVE divisors, Euclidean matches Python's //.
--   For NEGATIVE divisors, they diverge:
--     Lean ediv: 65536 / (-3) = -21845  (rem 1, r ≥ 0)
--     Python //: 65536 // (-3) = -21846  (rem -2, floor)
--   Python backends MUST use _ediv() for q16_div when b may be negative.
#eval do
  let r1 := (-6 : Int) / (65536 : Int)
  IO.println s!"V4a: (-6) / 65536 = {r1} (Euclidean, expect -1)"
  let r2 := (65536 : Int) / (-3 : Int)
  IO.println s!"V4b: 65536 / (-3) = {r2} (Euclidean, expect -21845)"

-- ─────────────────────────────────────────────────────────────────────────────
-- §V3  Division by zero canary
-- ─────────────────────────────────────────────────────────────────────────────

/-- V3 canary: dividing by zero must return StepError.divisionByZero.
    Push 1.0 (65536) → Push 0.0 (0) → divSatQ16 → should error. -/
def canaryDivByZero : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 0)⟩,
    Instr.prim Prim.divSatQ16,
    Instr.halt
  ]

-- V3 witness: division by zero returns error, not a sentinel.
#eval run 8 canaryDivByZero canaryState
-- Expected: Outcome.err StepError.divisionByZero

-- ─────────────────────────────────────────────────────────────────────────────
-- §V7  Stack overflow canary
-- ─────────────────────────────────────────────────────────────────────────────

-- V7 witness: maxStackDepth is 1024.
#eval maxStackDepth  -- expect 1024

-- ─────────────────────────────────────────────────────────────────────────────
-- §V5  Symmetric negation involution canary
-- ─────────────────────────────────────────────────────────────────────────────

/-- V5 canary: subtraction 0 - x is symmetric and clamps -2147483648 to 2147483647.
    Push 0.0 → Push -2147483648 → subSatQ16 → should result in 2147483647 (maxVal). -/
def canaryV5Negation : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 0)⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt (-2147483648))⟩,
    Instr.prim Prim.subSatQ16,
    Instr.halt
  ]

#eval run 8 canaryV5Negation canaryState
-- Expected: Outcome.ok with stack containing 2147483647

-- ─────────────────────────────────────────────────────────────────────────────
-- §V6  Signed comparison signedness canary
-- ─────────────────────────────────────────────────────────────────────────────

/-- V6 canary: checks that -2000000000 < 65536 is true (signed comparison).
    Push -2000000000 → Push 65536 → ltQ16 → should result in true. -/
def canaryV6SignedLt : List Instr :=
  [
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt (-2000000000))⟩,
    Instr.push ⟨AvmTy.q16_16, AvmVal.q16 (SilverSight.Q16_16.ofRawInt 65536)⟩,
    Instr.prim Prim.ltQ16,
    Instr.halt
  ]

#eval run 8 canaryV6SignedLt canaryState
-- Expected: Outcome.ok with stack containing bool true

end SilverSight.AVMIsa
