-- AVM ISA v1 (Lean-only): Step semantics

import SilverSight.AVMIsa.State

namespace SilverSight.AVMIsa

/-- Error tags for rejected states (ill-typed, underflow, etc.). -/
inductive StepError : Type where
  | stackUnderflow
  | typeMismatch
  | invalidJump
  | missingLocal
  | divisionByZero    -- V3: explicit div-by-zero (no silent sentinel)
  | stackOverflow     -- V7: stack depth exceeded maxStackDepth
  deriving Inhabited, DecidableEq, BEq, Repr

/-- Outcome type for AVM execution.

We avoid Float and avoid exceptions. Backends should mirror this boundary.
-/
inductive Outcome (α : Type) : Type where
  | ok : α → Outcome α
  | err : StepError → Outcome α
  deriving Inhabited, Repr

/-- Bounded/symmetric Q16 construction.
    V5 mitigation: clamps raw values to [-2147483647, 2147483647] internally.
    This guarantees that the negative boundary is symmetric, making negation
    a perfect involution for all VM values. -/
def ofAvmRaw (raw : Int) : SilverSight.Q16_16 :=
  let clamped :=
    if raw > 2147483647 then 2147483647
    else if raw < -2147483647 then -2147483647
    else raw
  SilverSight.FixedPoint.Q16_16.ofRawInt clamped

/-- Bounded/symmetric Q0 construction.
    V5 mitigation: clamps raw values to [-32767, 32767] internally. -/
def ofAvmRawQ0 (raw : Int) : SilverSight.Q0_16 :=
  let clamped :=
    if raw > 32767 then 32767
    else if raw < -32767 then -32767
    else raw
  SilverSight.FixedPoint.Q0_16.ofRawInt clamped

/-- Pop one element from stack. -/
def pop1 (s : State) : Outcome (AnyVal × State) :=
  match s.stack with
  | [] => Outcome.err StepError.stackUnderflow
  | x :: xs => Outcome.ok (x, { s with stack := xs })

/-- Maximum stack depth.
    V7 mitigation: bounds stack growth to prevent runaway push loops from
    consuming unbounded memory. 1024 values × ~12 bytes each = ~12 KB max.
    Programs needing deeper stacks should use locals or restructure. -/
def maxStackDepth : Nat := 1024

/-- Unchecked push (used in proofs for structural reasoning). -/
def push1_unchecked (s : State) (v : AnyVal) : State :=
  { s with stack := v :: s.stack }

/-- Push one element onto stack, checking depth bound.
    V7 mitigation: returns `Outcome.err stackOverflow` if limit is exceeded. -/
def push1 (s : State) (v : AnyVal) : Outcome State :=
  if s.stack.length ≥ maxStackDepth then
    Outcome.err StepError.stackOverflow
  else
    Outcome.ok (push1_unchecked s v)

/-- When stack is below limit, push1 succeeds and equals push1_unchecked. -/
theorem push1_ok_of_lt {s : State} {v : AnyVal}
    (h : s.stack.length < maxStackDepth) :
    push1 s v = Outcome.ok (push1_unchecked s v) := by
  unfold push1
  rw [if_neg (by omega)]

/-- Evaluate a primitive.

NOTE: This v1 skeleton implements only a small subset. Extend strictly by
adding Lean semantics; do not delegate meaning to backends.
-/
def evalPrim (p : Prim) (s : State) : Outcome State :=
  match p with
  | Prim.not =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v, s1) =>
          match v with
          | ⟨AvmTy.bool, AvmVal.b x⟩ =>
              push1 s1 ⟨AvmTy.bool, AvmVal.b (!x)⟩
          | _ => Outcome.err StepError.typeMismatch
  | Prim.and =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
                  push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 && b1)⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.or =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.bool, AvmVal.b b1⟩, ⟨AvmTy.bool, AvmVal.b b2⟩ =>
                  push1 s2 ⟨AvmTy.bool, AvmVal.b (b2 || b1)⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.addSatQ0 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
                  push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (ofAvmRawQ0 (y.toInt + x.toInt))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.subSatQ0 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q0_16, AvmVal.q0 x⟩, ⟨AvmTy.q0_16, AvmVal.q0 y⟩ =>
                  push1 s2 ⟨AvmTy.q0_16, AvmVal.q0 (ofAvmRawQ0 (y.toInt - x.toInt))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.addSatQ16 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw (y.toInt + x.toInt))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.subSatQ16 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw (y.toInt - x.toInt))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.mulSatQ16 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw ((y.toInt * x.toInt) / 65536))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.divSatQ16 =>
      -- V3 mitigation: explicit division-by-zero error
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  if x.toInt = 0 then
                    Outcome.err StepError.divisionByZero
                  else
                    push1 s2 ⟨AvmTy.q16_16, AvmVal.q16 (ofAvmRaw ((y.toInt * 65536) / x.toInt))⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.ltQ16 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  -- V6: Explicit signed comparison via sign decomposition
                  let sa := y.toInt < 0
                  let sb := x.toInt < 0
                  let res := if sa != sb then sa else y.toInt < x.toInt
                  push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩
              | _, _ => Outcome.err StepError.typeMismatch
  | Prim.eqQ16 =>
      match pop1 s with
      | Outcome.err e => Outcome.err e
      | Outcome.ok (v1, s1) =>
          match pop1 s1 with
          | Outcome.err e => Outcome.err e
          | Outcome.ok (v2, s2) =>
              match v1, v2 with
              | ⟨AvmTy.q16_16, AvmVal.q16 x⟩, ⟨AvmTy.q16_16, AvmVal.q16 y⟩ =>
                  let res := y.val == x.val
                  push1 s2 ⟨AvmTy.bool, AvmVal.b res⟩
              | _, _ => Outcome.err StepError.typeMismatch

/-- One-step execution.

`Program` is modeled as a list for v1.
-/
def step (program : List Instr) (s : State) : Outcome State :=
  if s.halted then
    Outcome.ok s
  else
    match program[s.pc]? with
    | none => Outcome.err StepError.invalidJump
    | some instr =>
        match instr with
        | Instr.halt => Outcome.ok { s with halted := true }
        | Instr.push v =>
            -- V7: check stack depth on push
            if s.stack.length ≥ maxStackDepth then
              Outcome.err StepError.stackOverflow
            else
              Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
        | Instr.pop =>
            match pop1 s with
            | Outcome.err e => Outcome.err e
            | Outcome.ok (_, s1) => Outcome.ok { s1 with pc := s.pc + 1 }
        | Instr.dup =>
            match s.stack with
            | [] => Outcome.err StepError.stackUnderflow
            | x :: xs =>
                -- V7: check stack depth on dup (grows stack by 1)
                if s.stack.length ≥ maxStackDepth then
                  Outcome.err StepError.stackOverflow
                else
                  Outcome.ok { s with pc := s.pc + 1, stack := x :: x :: xs }
        | Instr.swap =>
            match s.stack with
            | a :: b :: xs => Outcome.ok { s with pc := s.pc + 1, stack := b :: a :: xs }
            | _ => Outcome.err StepError.stackUnderflow
        | Instr.load i =>
            match getLocal? s i with
            | none => Outcome.err StepError.missingLocal
            | some v =>
                if s.stack.length ≥ maxStackDepth then
                  Outcome.err StepError.stackOverflow
                else
                  Outcome.ok { s with pc := s.pc + 1, stack := v :: s.stack }
        | Instr.store i =>
            match pop1 s with
            | Outcome.err e => Outcome.err e
            | Outcome.ok (v, s1) =>
                match setLocal? s1 i v with
                | some s2 => Outcome.ok { s2 with pc := s.pc + 1 }
                | none => Outcome.err StepError.missingLocal
        | Instr.jump target =>
            if target < program.length then
              Outcome.ok { s with pc := target }
            else
              Outcome.err StepError.invalidJump
        | Instr.jumpIf target =>
            match pop1 s with
            | Outcome.err e => Outcome.err e
            | Outcome.ok (v, s1) =>
                match v with
                | ⟨AvmTy.bool, AvmVal.b b⟩ =>
                    if b then
                      if target < program.length then
                        Outcome.ok { s1 with pc := target }
                      else
                        Outcome.err StepError.invalidJump
                    else
                      Outcome.ok { s1 with pc := s.pc + 1 }
                | _ => Outcome.err StepError.typeMismatch
        | Instr.prim p =>
            match evalPrim p s with
            | Outcome.err e => Outcome.err e
            | Outcome.ok s1 => Outcome.ok { s1 with pc := s.pc + 1 }

end SilverSight.AVMIsa
