//! AVM ISA v1 — Strict Functional Execution Engine
//!
//! Mirrors `formal/SilverSight/AVMIsa/` (Lean 4).
//! The instruction set IS the execution — no interpreter dispatch table.
//!
//! Design rules:
//!   - Closed-world type universe: Q0_16, Q16_16, Bool
//!   - Pure functions: step(State) -> State, run(State) -> State
//!   - No Float in compute paths (Q16_16 fixed-point only)
//!   - Fuel-bounded run loop (total termination)

use crate::q16::*;

// ── AVM-specific constants ──────────────────────────────────────────
// AVM uses symmetric clamping [-2147483647, 2147483647] (excludes INT32_MIN)
// to guarantee negation is a perfect involution.
const AVM_CLAMP_MIN: i32 = -2147483647;
const AVM_CLAMP_MAX: i32 = 2147483647;
const AVM_Q0_MIN: i32 = -32767;
const AVM_Q0_MAX: i32 = 32767;
const AVM_MAX_STACK: usize = 1024;

/// Floor division matching Lean `Int.ediv` (rounds toward negative infinity).
fn floor_div(a: i32, b: i32) -> i32 {
    let d = a / b;
    let r = a % b;
    if r != 0 && ((a ^ b) < 0) { d - 1 } else { d }
}

/// AVM saturating clamp: [-2147483647, 2147483647]
fn avm_clamp(v: i64) -> i32 {
    if v > AVM_CLAMP_MAX as i64 { AVM_CLAMP_MAX }
    else if v < AVM_CLAMP_MIN as i64 { AVM_CLAMP_MIN }
    else { v as i32 }
}

/// V6 sign-decomposition comparison for Q16_16.
fn lt_q16_v6(a: i32, b: i32) -> bool {
    let sa = a < 0;
    let sb = b < 0;
    if sa != sb { sa } else { a < b }
}

    // ── Types ───────────────────────────────────────────────────────────

    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
    pub enum AvmTy { Q0_16, Q16_16, Bool }

    // ── Values ──────────────────────────────────────────────────────────

    #[derive(Debug, Clone, PartialEq)]
    pub enum AvmVal {
        Q0_16(i32),    // raw Q0_16: [-32767, 32767] symmetric
        Q16_16(i32),   // raw Q16_16: [-2147483647, 2147483647] symmetric
        Bool(bool),
    }

    impl AvmVal {
        pub fn ty(&self) -> AvmTy {
            match self {
                AvmVal::Q0_16(_) => AvmTy::Q0_16,
                AvmVal::Q16_16(_) => AvmTy::Q16_16,
                AvmVal::Bool(_) => AvmTy::Bool,
            }
        }
    }

    // ── Primitives ──────────────────────────────────────────────────────

    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
    pub enum Prim {
        AddSatQ0, SubSatQ0,
        AddSatQ16, SubSatQ16, MulSatQ16, DivSatQ16,
        LtQ16, EqQ16,
        And, Or, Not,
    }

    // ── Instructions ────────────────────────────────────────────────────

    #[derive(Debug, Clone, PartialEq)]
    pub enum Instr {
        Push(AvmVal),
        Pop,
        Dup,
        Swap,
        Load(usize),
        Store(usize),
        Jump(usize),
        JumpIf(usize),
        Prim(Prim),
        Halt,
    }

    // ── Step Error ─────────────────────────────────────────────────────

    #[derive(Debug, Clone, PartialEq)]
    pub enum StepError {
        EmptyStack,
        StackUnderflow(&'static str),  // operation needs N items, has <N
        TypeMismatch { expected: AvmTy, got: AvmTy },
        MissingLocal(usize),
        DivisionByZero,
        JumpOutOfBounds(usize),
        StackOverflow,
        Halted,
    }

    // ── State ──────────────────────────────────────────────────────────

    #[derive(Debug, Clone, PartialEq)]
    pub struct State {
        pub pc: usize,
        pub stack: Vec<AvmVal>,
        pub locals: Vec<Option<AvmVal>>,
        pub halted: bool,
    }

    impl State {
        pub fn new(locals_size: usize) -> Self {
            Self {
                pc: 0,
                stack: Vec::new(),
                locals: vec![None; locals_size],
                halted: false,
            }
        }
    }

    // ── Primitive execution (strict functional) ─────────────────────────

    fn exec_prim(op: Prim, a: &AvmVal, b: Option<&AvmVal>) -> Result<AvmVal, StepError> {
        match (op, a, b) {
            // Q0_16 binary (symmetric clamp)
            (Prim::AddSatQ0, AvmVal::Q0_16(x), Some(AvmVal::Q0_16(y))) => {
                let r = (*x as i64) + (*y as i64);
                Ok(AvmVal::Q0_16(if r > AVM_Q0_MAX as i64 { AVM_Q0_MAX }
                    else if r < AVM_Q0_MIN as i64 { AVM_Q0_MIN } else { r as i32 }))
            }
            (Prim::SubSatQ0, AvmVal::Q0_16(x), Some(AvmVal::Q0_16(y))) => {
                let r = (*x as i64) - (*y as i64);
                Ok(AvmVal::Q0_16(if r > AVM_Q0_MAX as i64 { AVM_Q0_MAX }
                    else if r < AVM_Q0_MIN as i64 { AVM_Q0_MIN } else { r as i32 }))
            }
            // Q16_16 binary (symmetric clamp, floor division)
            (Prim::AddSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                Ok(AvmVal::Q16_16(avm_clamp((*x as i64) + (*y as i64))))
            }
            (Prim::SubSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                Ok(AvmVal::Q16_16(avm_clamp((*x as i64) - (*y as i64))))
            }
            (Prim::MulSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                Ok(AvmVal::Q16_16(avm_clamp(floor_div((*x as i64) * (*y as i64), Q16_SCALE as i64))))
            }
            (Prim::DivSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                if *y == 0 { return Err(StepError::DivisionByZero); }
                Ok(AvmVal::Q16_16(avm_clamp(floor_div((*x as i64) * Q16_SCALE as i64, *y as i64))))
            }
            // Comparisons (V6 sign-decomposition)
            (Prim::LtQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                Ok(AvmVal::Bool(lt_q16_v6(*x, *y)))
            }
            (Prim::EqQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
                Ok(AvmVal::Bool(x == y))
            }
            // Boolean
            (Prim::And, AvmVal::Bool(x), Some(AvmVal::Bool(y))) => {
                Ok(AvmVal::Bool(*x && *y))
            }
            (Prim::Or, AvmVal::Bool(x), Some(AvmVal::Bool(y))) => {
                Ok(AvmVal::Bool(*x || *y))
            }
            (Prim::Not, AvmVal::Bool(x), None) => {
                Ok(AvmVal::Bool(!*x))
            }
            // Type mismatches
            _ => {
                let expected = match op {
                    Prim::AddSatQ0 | Prim::SubSatQ0 => AvmTy::Q0_16,
                    Prim::AddSatQ16 | Prim::SubSatQ16
                    | Prim::MulSatQ16 | Prim::DivSatQ16
                    | Prim::LtQ16 | Prim::EqQ16 => AvmTy::Q16_16,
                    Prim::And | Prim::Or | Prim::Not => AvmTy::Bool,
                };
                Err(StepError::TypeMismatch { expected, got: a.ty() })
            }
        }
    }

    // ── Step (pure function: State → Result<State, StepError>) ─────────

    pub fn step(s: &State, program: &[Instr]) -> Result<State, StepError> {
        if s.halted { return Err(StepError::Halted); }
        if s.pc >= program.len() {
            return Ok(State {
                pc: s.pc,
                stack: s.stack.clone(),
                locals: s.locals.clone(),
                halted: true,
            });
        }

        let instr = &program[s.pc];
        let mut stack = s.stack.clone();
        let mut locals = s.locals.clone();
        let mut pc = s.pc + 1;
        let mut halted = false;

        fn check_stack(stack: &[AvmVal]) -> Result<(), StepError> {
            if stack.len() >= AVM_MAX_STACK {
                return Err(StepError::StackOverflow);
            }
            Ok(())
        }

        match instr {
            Instr::Push(v) => {
                check_stack(&stack)?;
                stack.push(v.clone());
            }
            Instr::Pop => {
                stack.pop().ok_or(StepError::EmptyStack)?;
            }
            Instr::Dup => {
                stack.last().ok_or(StepError::EmptyStack)?;
                check_stack(&stack)?;
                let v = stack.last().ok_or(StepError::EmptyStack)?.clone();
                stack.push(v);
            }
            Instr::Swap => {
                let a = stack.pop().ok_or(StepError::StackUnderflow("swap"))?;
                let b = stack.pop().ok_or(StepError::StackUnderflow("swap"))?;
                stack.push(a);
                stack.push(b);
            }
            Instr::Load(i) => {
                let v = locals.get(*i).ok_or(StepError::MissingLocal(*i))?
                    .clone().ok_or(StepError::MissingLocal(*i))?;
                check_stack(&stack)?;
                stack.push(v);
            }
            Instr::Store(i) => {
                let v = stack.pop().ok_or(StepError::EmptyStack)?;
                if *i >= locals.len() {
                    return Err(StepError::MissingLocal(*i));
                }
                locals[*i] = Some(v);
            }
            Instr::Jump(target) => {
                if *target >= program.len() {
                    return Err(StepError::JumpOutOfBounds(*target));
                }
                pc = *target;
            }
            Instr::JumpIf(target) => {
                let cond = stack.pop().ok_or(StepError::EmptyStack)?;
                match cond {
                    AvmVal::Bool(true) => {
                        if *target >= program.len() {
                            return Err(StepError::JumpOutOfBounds(*target));
                        }
                        pc = *target;
                    }
                    AvmVal::Bool(false) => { /* fallthrough */ }
                    _ => return Err(StepError::TypeMismatch { expected: AvmTy::Bool, got: cond.ty() }),
                }
            }
            Instr::Prim(p) => {
                let arity = match p {
                    Prim::Not => 1,
                    _ => 2,
                };
                let b = if arity >= 2 { Some(stack.pop().ok_or(StepError::StackUnderflow("prim"))?) } else { None };
                let a = stack.pop().ok_or(StepError::StackUnderflow("prim"))?;
                let result = exec_prim(*p, &a, b.as_ref())?;
                stack.push(result);
            }
            Instr::Halt => {
                halted = true;
            }
        }

        Ok(State { pc, stack, locals, halted })
    }

    // ── Run (fuel-bounded, pure) ──────────────────────────────────────

    pub fn run(initial: &State, program: &[Instr], fuel: usize) -> Result<State, StepError> {
        let mut state = initial.clone();
        for _ in 0..fuel {
            if state.halted { return Ok(state); }
            state = step(&state, program)?;
        }
        Ok(state)
    }

#[cfg(test)]
mod tests {
    use super::*;

    fn make_program() -> (Vec<Instr>, State) {
        // Program: push Q16(5), push Q16(3), add, halt
        let prog = vec![
            Instr::Push(AvmVal::Q16_16(5 * 65536)),
            Instr::Push(AvmVal::Q16_16(3 * 65536)),
            Instr::Prim(Prim::AddSatQ16),
            Instr::Halt,
        ];
        let state = State::new(0);
        (prog, state)
    }

    #[test]
    fn test_add_q16() {
        let (prog, state) = make_program();
        let final_state = run(&state, &prog, 100).unwrap();
        assert!(final_state.halted);
        assert_eq!(final_state.stack.len(), 1);
        assert_eq!(final_state.stack[0], AvmVal::Q16_16(8 * 65536));
    }

    #[test]
    fn test_jump_if() {
        // Program: push Bool(true), jump_if(4), push Q16(0), halt, push Q16(1), halt
        let prog = vec![
            Instr::Push(AvmVal::Bool(true)),
            Instr::JumpIf(4),
            Instr::Push(AvmVal::Q16_16(0)),
            Instr::Halt,
            Instr::Push(AvmVal::Q16_16(65536)),
            Instr::Halt,
        ];
        let state = State::new(0);
        let final_state = run(&state, &prog, 100).unwrap();
        assert!(final_state.halted);
        assert_eq!(final_state.stack[0], AvmVal::Q16_16(65536));
        assert_eq!(final_state.pc, 6);
    }

    #[test]
    fn test_store_load() {
        // Program: push 42, store(0), load(0), halt
        let prog = vec![
            Instr::Push(AvmVal::Q16_16(42 * 65536)),
            Instr::Store(0),
            Instr::Load(0),
            Instr::Halt,
        ];
        let state = State::new(1);
        let final_state = run(&state, &prog, 100).unwrap();
        assert_eq!(final_state.stack[0], AvmVal::Q16_16(42 * 65536));
    }

    #[test]
    fn test_prim_type_checking() {
        // Program: push Bool(true), push Q16(5), add → type error
        let prog = vec![
            Instr::Push(AvmVal::Bool(true)),
            Instr::Push(AvmVal::Q16_16(65536)),
            Instr::Prim(Prim::AddSatQ16),
            Instr::Halt,
        ];
        let state = State::new(0);
        let result = run(&state, &prog, 100);
        assert!(result.is_err());
        match result {
            Err(StepError::TypeMismatch { .. }) => {} // expected
            _ => panic!("Expected TypeMismatch, got {:?}", result),
        }
    }

    #[test]
    fn test_division_by_zero() {
        let prog = vec![
            Instr::Push(AvmVal::Q16_16(65536)),
            Instr::Push(AvmVal::Q16_16(0)),
            Instr::Prim(Prim::DivSatQ16),
            Instr::Halt,
        ];
        let state = State::new(0);
        let result = run(&state, &prog, 100);
        assert_eq!(result, Err(StepError::DivisionByZero));
    }
}