# AVM ISA v1 — R Port (Strict Functional Execution)
#
# Mirrors `formal/SilverSight/AVMIsa/` (Lean 4) and `rust/src/avm/` (Rust).
# Pure functions: step(state, program) -> state, run(state, program, fuel) -> state

# ── Instruction type ─────────────────────────────────────────────────

# Instr is a list with fields:
#   op: integer code (0=push_q16, 1=push_bool, 2=pop, 3=dup, 4=swap,
#                     5=load, 6=store, 7=jump, 8=jump_if, 9=prim, 10=halt)
#   arg: integer payload

INSTR_PUSH_Q16  <- 0L
INSTR_PUSH_BOOL <- 1L
INSTR_PUSH_Q0   <- 2L
INSTR_POP       <- 3L
INSTR_DUP       <- 4L
INSTR_SWAP      <- 5L
INSTR_LOAD      <- 6L
INSTR_STORE     <- 7L
INSTR_JUMP      <- 8L
INSTR_JUMP_IF   <- 9L
INSTR_PRIM      <- 10L
INSTR_HALT      <- 11L

# ── Primitives ───────────────────────────────────────────────────────

PRIM_ADD_Q0  <- 0L
PRIM_SUB_Q0  <- 1L
PRIM_ADD_Q16 <- 2L
PRIM_SUB_Q16 <- 3L
PRIM_MUL_Q16 <- 4L
PRIM_DIV_Q16 <- 5L
PRIM_LT_Q16  <- 6L
PRIM_EQ_Q16  <- 7L
PRIM_AND     <- 8L
PRIM_OR      <- 9L
PRIM_NOT     <- 10L

# ── Step Error codes ─────────────────────────────────────────────────

ERR_EMPTY_STACK     <- "empty_stack"
ERR_STACK_UNDERFLOW <- "stack_underflow"
ERR_TYPE_MISMATCH   <- "type_mismatch"
ERR_MISSING_LOCAL   <- "missing_local"
ERR_DIV_BY_ZERO     <- "division_by_zero"
ERR_JUMP_OOB        <- "jump_out_of_bounds"
ERR_STACK_OVERFLOW  <- "stack_overflow"
ERR_HALTED          <- "halted"

# ── AVM constants ───────────────────────────────────────────────────

AVM_CLAMP_MIN <- -2147483647L
AVM_CLAMP_MAX <- 2147483647L
AVM_Q0_MIN    <- -32767L
AVM_Q0_MAX    <- 32767L
AVM_MAX_STACK <- 1024L

# ── Instruction constructors ─────────────────────────────────────────

instr_push_q16  <- function(x) list(op = INSTR_PUSH_Q16,  arg = as.integer(x))
instr_push_bool <- function(x) list(op = INSTR_PUSH_BOOL, arg = as.integer(x))
instr_push_q0   <- function(x) list(op = INSTR_PUSH_Q0,   arg = as.integer(x))
instr_pop       <- function()  list(op = INSTR_POP,        arg = 0L)
instr_dup       <- function()  list(op = INSTR_DUP,        arg = 0L)
instr_swap      <- function()  list(op = INSTR_SWAP,       arg = 0L)
instr_load      <- function(i) list(op = INSTR_LOAD,       arg = as.integer(i))
instr_store     <- function(i) list(op = INSTR_STORE,      arg = as.integer(i))
instr_jump      <- function(t) list(op = INSTR_JUMP,       arg = as.integer(t))
instr_jump_if   <- function(t) list(op = INSTR_JUMP_IF,    arg = as.integer(t))
instr_prim      <- function(p) list(op = INSTR_PRIM,       arg = as.integer(p))
instr_halt      <- function()  list(op = INSTR_HALT,        arg = 0L)

# ── State constructor ────────────────────────────────────────────────

new_state <- function(n_locals = 0L) {
  list(
    pc = 1L,
    stack = list(),       # each element: list(type="q16", val=integer) or list(type="bool", val=logical)
    locals = vector("list", n_locals),  # elements can be NULL
    local_types = vector("list", n_locals),
    halted = FALSE
  )
}

# ── Stack helpers ────────────────────────────────────────────────────

make_q16  <- function(x) list(type = "q16",  val = as.integer(x))
make_q0   <- function(x) list(type = "q0",   val = as.integer(x))
make_bool <- function(x) list(type = "bool", val = as.logical(x))

is_q16  <- function(v) identical(v$type, "q16")
is_q0   <- function(v) identical(v$type, "q0")
is_bool <- function(v) identical(v$type, "bool")

# ── Q16_16 helpers ───────────────────────────────────────────────────

Q16_SCALE <- 65536L

# AVM symmetric clamp
avm_clamp <- function(x) {
  min(AVM_CLAMP_MAX, max(AVM_CLAMP_MIN, as.integer(x)))
}

# V6 signed comparison
lt_q16_v6 <- function(a, b) {
  sa <- a < 0L
  sb <- b < 0L
  if (sa != sb) sa else a < b
}

q16_mul <- function(a, b) {
  # Floor division matching Lean Int.ediv: (a * b) %/% 65536
  prod <- as.numeric(a) * as.numeric(b)
  avm_clamp(prod %/% Q16_SCALE)
}

q16_div <- function(a, b) {
  if (b == 0L) stop(ERR_DIV_BY_ZERO)
  # Floor division matching Lean Int.ediv: (y * 65536) %/% x
  num <- as.numeric(a) * Q16_SCALE
  avm_clamp(num %/% as.numeric(b))
}

# ── Primitive execution ──────────────────────────────────────────────

avm_q0_clamp <- function(x) {
  min(AVM_Q0_MAX, max(AVM_Q0_MIN, as.integer(x)))
}

exec_prim <- function(op, a, b = NULL) {
  if (op == PRIM_ADD_Q0) {
    if (!is_q0(a) || !is_q0(b)) stop(ERR_TYPE_MISMATCH)
    make_q0(avm_q0_clamp(as.numeric(a$val) + as.numeric(b$val)))
  } else if (op == PRIM_SUB_Q0) {
    if (!is_q0(a) || !is_q0(b)) stop(ERR_TYPE_MISMATCH)
    make_q0(avm_q0_clamp(as.numeric(a$val) - as.numeric(b$val)))
  } else if (op == PRIM_ADD_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    x <- as.numeric(a$val) + as.numeric(b$val)
    make_q16(avm_clamp(x))
  } else if (op == PRIM_SUB_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    x <- as.numeric(a$val) - as.numeric(b$val)
    make_q16(avm_clamp(x))
  } else if (op == PRIM_MUL_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    make_q16(q16_mul(a$val, b$val))
  } else if (op == PRIM_DIV_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    make_q16(q16_div(a$val, b$val))
  } else if (op == PRIM_LT_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    make_bool(lt_q16_v6(a$val, b$val))
  } else if (op == PRIM_EQ_Q16) {
    if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
    make_bool(a$val == b$val)
  } else if (op == PRIM_AND) {
    if (!is_bool(a) || !is_bool(b)) stop(ERR_TYPE_MISMATCH)
    make_bool(a$val && b$val)
  } else if (op == PRIM_OR) {
    if (!is_bool(a) || !is_bool(b)) stop(ERR_TYPE_MISMATCH)
    make_bool(a$val || b$val)
  } else if (op == PRIM_NOT) {
    if (!is_bool(a)) stop(ERR_TYPE_MISMATCH)
    make_bool(!a$val)
  } else {
    stop("unknown prim")
  }
}

# ── Step (pure function) ─────────────────────────────────────────────

step <- function(s, prog) {
  if (s$halted) stop(ERR_HALTED)
  if (s$pc < 1L || s$pc > length(prog)) {
    return(list(pc = s$pc, stack = s$stack, locals = s$locals,
                local_types = s$local_types, halted = TRUE))
  }

  instr <- prog[[s$pc]]
  stack <- s$stack
  locals <- s$locals
  local_types <- s$local_types
  pc <- s$pc + 1L
  halted <- FALSE

  # Stack depth check (push, dup, load grow the stack)
  if (instr$op %in% c(INSTR_PUSH_Q16, INSTR_PUSH_BOOL, INSTR_DUP, INSTR_LOAD) &&
      length(stack) >= AVM_MAX_STACK) stop(ERR_STACK_OVERFLOW)

  if (instr$op == INSTR_PUSH_Q16) {
    stack <- c(stack, list(make_q16(instr$arg)))
  } else if (instr$op == INSTR_PUSH_BOOL) {
    stack <- c(stack, list(make_bool(instr$arg != 0L)))
  } else if (instr$op == INSTR_PUSH_Q0) {
    stack <- c(stack, list(make_q0(instr$arg)))
  } else if (instr$op == INSTR_POP) {
    if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
    stack <- stack[-length(stack)]
  } else if (instr$op == INSTR_DUP) {
    if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
    stack <- c(stack, stack[length(stack)])
  } else if (instr$op == INSTR_SWAP) {
    if (length(stack) < 2L) stop(ERR_STACK_UNDERFLOW)
    n <- length(stack)
    tmp <- stack[[n]]; stack[[n]] <- stack[[n-1]]; stack[[n-1]] <- tmp
  } else if (instr$op == INSTR_LOAD) {
    i <- instr$arg + 1L
    if (i > length(locals)) stop(ERR_MISSING_LOCAL)
    if (is.null(locals[[i]])) stop(ERR_MISSING_LOCAL)
    # Restore from local type tag
    lt <- local_types[[i]]
    if (identical(lt, "q16")) stack <- c(stack, list(make_q16(locals[[i]])))
    else if (identical(lt, "q0")) stack <- c(stack, list(make_q0(locals[[i]])))
    else stack <- c(stack, list(make_bool(locals[[i]])))
  } else if (instr$op == INSTR_STORE) {
    i <- instr$arg + 1L
    if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
    if (i > length(locals)) stop(ERR_MISSING_LOCAL)
    v <- stack[[length(stack)]]
    stack <- stack[-length(stack)]
    locals[[i]] <- v$val
    local_types[[i]] <- v$type
  } else if (instr$op == INSTR_JUMP) {
    target <- instr$arg + 1L
    if (target < 1L || target > length(prog)) stop(ERR_JUMP_OOB)
    pc <- target
  } else if (instr$op == INSTR_JUMP_IF) {
    if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
    cond <- stack[[length(stack)]]
    stack <- stack[-length(stack)]
    if (is_bool(cond) && cond$val) {
      target <- instr$arg + 1L
      if (target < 1L || target > length(prog)) stop(ERR_JUMP_OOB)
      pc <- target
    } else if (!is_bool(cond)) {
      stop(ERR_TYPE_MISMATCH)
    }
  } else if (instr$op == INSTR_PRIM) {
    p <- instr$arg
    arity <- if (p == PRIM_NOT) 1L else 2L
    if (length(stack) < arity) stop(ERR_STACK_UNDERFLOW)
    if (arity >= 2L) {
      b <- stack[[length(stack)]]
      stack <- stack[-length(stack)]
    } else {
      b <- NULL
    }
    a <- stack[[length(stack)]]
    stack <- stack[-length(stack)]
    result <- exec_prim(p, a, b)
    stack <- c(stack, list(result))
  } else if (instr$op == INSTR_HALT) {
    halted <- TRUE
  }

  list(pc = pc, stack = stack, locals = locals,
       local_types = local_types, halted = halted)
}

# ── Run (fuel-bounded) ──────────────────────────────────────────────

run <- function(initial, prog, fuel = 1000L) {
  s <- initial
  for (i in seq_len(fuel)) {
    if (s$halted) return(s)
    s <- step(s, prog)
  }
  s
}