mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
1ae311c63f
Julia port: - Extended type tracking from Bool (is_q16) to Int8 tri-state (TYPE_BOOL/Q16/Q0) - Added ADD_SAT_Q0 / SUB_SAT_Q0 primitive handling - Added avm_q0_clamp for symmetric Q0_16 range [-32767, 32767] R port: - Added PRIM_ADD_Q0 / PRIM_SUB_Q0 primitives - Added push_q0 instruction, make_q0 / is_q0 helpers - Added avm_q0_clamp for symmetric Q0_16 range - Fixed LOAD to preserve type tag on restore All three ports now support the full AVM ISA type universe (Q0_16, Q16_16, Bool).
271 lines
10 KiB
R
271 lines
10 KiB
R
# 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
|
|
}
|