% AVM ISA v1 — Octave/MATLAB Port (Strict Functional Execution)
% Mirrors formal/SilverSight/AVMIsa/Step.lean

classdef AVM
    properties (Constant)
        AVM_CLAMP_MIN = -2147483647
        AVM_CLAMP_MAX = 2147483647
        AVM_Q0_MIN = -32767
        AVM_Q0_MAX = 32767
        Q16_SCALE = 65536
        AVM_MAX_STACK = 1024

        TY_Q0 = 0; TY_Q16 = 1; TY_BOOL = 2

        OP_PUSH_Q16 = 0; OP_PUSH_BOOL = 1; OP_PUSH_Q0 = 2
        OP_POP = 3; OP_DUP = 4; OP_SWAP = 5
        OP_LOAD = 6; OP_STORE = 7; OP_JUMP = 8
        OP_JUMP_IF = 9; OP_PRIM = 10; OP_HALT = 11

        PRIM_ADD_Q0 = 0; PRIM_SUB_Q0 = 1
        PRIM_ADD_Q16 = 2; PRIM_SUB_Q16 = 3
        PRIM_MUL_Q16 = 4; PRIM_DIV_Q16 = 5
        PRIM_LT_Q16 = 6; PRIM_EQ_Q16 = 7
        PRIM_AND = 8; PRIM_OR = 9; PRIM_NOT = 10
    end

    methods (Static)
        function r = avm_clamp(x)
            if x > AVM.AVM_CLAMP_MAX; r = AVM.AVM_CLAMP_MAX;
            elseif x < AVM.AVM_CLAMP_MIN; r = AVM.AVM_CLAMP_MIN;
            else; r = int32(x); end
        end

        function r = avm_q0_clamp(x)
            if x > AVM.AVM_Q0_MAX; r = AVM.AVM_Q0_MAX;
            elseif x < AVM.AVM_Q0_MIN; r = AVM.AVM_Q0_MIN;
            else; r = int32(x); end
        end

        function r = floor_div(a, b)
            if b == 0; error('division by zero'); end
            q = idivide(a, b, 'floor');
            r = int32(q);
        end

        function r = lt_q16_v6(a, b)
            sa = a < 0; sb = b < 0;
            if sa ~= sb; r = sa; else; r = a < b; end
        end

        function v = val_q16(x)
            v = struct('ty', AVM.TY_Q16, 'i', AVM.avm_clamp(x), 'b', false);
        end

        function v = val_q0(x)
            v = struct('ty', AVM.TY_Q0, 'i', AVM.avm_q0_clamp(x), 'b', false);
        end

        function v = val_bool(x)
            v = struct('ty', AVM.TY_BOOL, 'i', int32(0), 'b', x);
        end

        function s = init_state(n_locals)
            if nargin < 1; n_locals = 0; end
            s.pc = int32(1);  % 1-indexed for Octave
            s.stack = {};
            s.locals = cell(n_locals, 1);
            s.halted = false;
        end

        function r = exec_prim(p, a, b)
            r = AVM.val_q0(0);
            if p == AVM.PRIM_ADD_Q0
                if a.ty ~= AVM.TY_Q0 || b.ty ~= AVM.TY_Q0; return; end
                r = AVM.val_q0(double(a.i) + double(b.i));
            elseif p == AVM.PRIM_SUB_Q0
                if a.ty ~= AVM.TY_Q0 || b.ty ~= AVM.TY_Q0; return; end
                r = AVM.val_q0(double(a.i) - double(b.i));
            elseif p == AVM.PRIM_ADD_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16; return; end
                r = AVM.val_q16(double(a.i) + double(b.i));
            elseif p == AVM.PRIM_SUB_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16; return; end
                r = AVM.val_q16(double(a.i) - double(b.i));
            elseif p == AVM.PRIM_MUL_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16; return; end
                r = AVM.val_q16(AVM.floor_div(double(a.i) * double(b.i), AVM.Q16_SCALE));
            elseif p == AVM.PRIM_DIV_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16 || b.i == 0; return; end
                r = AVM.val_q16(AVM.floor_div(double(a.i) * AVM.Q16_SCALE, double(b.i)));
            elseif p == AVM.PRIM_LT_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16; return; end
                r = AVM.val_bool(AVM.lt_q16_v6(a.i, b.i));
            elseif p == AVM.PRIM_EQ_Q16
                if a.ty ~= AVM.TY_Q16 || b.ty ~= AVM.TY_Q16; return; end
                r = AVM.val_bool(a.i == b.i);
            elseif p == AVM.PRIM_AND
                if a.ty ~= AVM.TY_BOOL || b.ty ~= AVM.TY_BOOL; return; end
                r = AVM.val_bool(a.b && b.b);
            elseif p == AVM.PRIM_OR
                if a.ty ~= AVM.TY_BOOL || b.ty ~= AVM.TY_BOOL; return; end
                r = AVM.val_bool(a.b || b.b);
            elseif p == AVM.PRIM_NOT
                if a.ty ~= AVM.TY_BOOL; return; end
                r = AVM.val_bool(~a.b);
            end
        end

        function [s, err] = step(s, prog)
            err = 0; n = length(prog);
            if s.halted; err = -1; return; end
            if s.pc < 1 || s.pc > n; s.halted = true; return; end

            instr = prog{s.pc}; npc = s.pc + 1;

            growing = any(instr.op == [AVM.OP_PUSH_Q16, AVM.OP_PUSH_BOOL, AVM.OP_PUSH_Q0, AVM.OP_DUP, AVM.OP_LOAD]);
            if growing && length(s.stack) >= AVM.AVM_MAX_STACK; err = -2; return; end

            if instr.op == AVM.OP_PUSH_Q16
                s.stack{end+1} = AVM.val_q16(instr.arg);
            elseif instr.op == AVM.OP_PUSH_BOOL
                s.stack{end+1} = AVM.val_bool(instr.arg2);
            elseif instr.op == AVM.OP_PUSH_Q0
                s.stack{end+1} = AVM.val_q0(instr.arg);
            elseif instr.op == AVM.OP_POP
                if isempty(s.stack); err = -3; return; end; s.stack(end) = [];
            elseif instr.op == AVM.OP_DUP
                if isempty(s.stack); err = -3; return; end
                s.stack{end+1} = s.stack{end};
            elseif instr.op == AVM.OP_SWAP
                if length(s.stack) < 2; err = -4; return; end
                tmp = s.stack{end}; s.stack{end} = s.stack{end-1}; s.stack{end-1} = tmp;
            elseif instr.op == AVM.OP_LOAD
                i = instr.arg + 1;
                if i > length(s.locals) || isempty(s.locals{i}); err = -5; return; end
                s.stack{end+1} = s.locals{i};
            elseif instr.op == AVM.OP_STORE
                if isempty(s.stack); err = -3; return; end
                i = instr.arg + 1;
                if i > length(s.locals); err = -5; return; end
                s.locals{i} = s.stack{end}; s.stack(end) = [];
            elseif instr.op == AVM.OP_JUMP
                t = instr.arg + 1;
                if t < 1 || t > n; err = -6; return; end; npc = t;
            elseif instr.op == AVM.OP_JUMP_IF
                if isempty(s.stack); err = -3; return; end
                v = s.stack{end}; s.stack(end) = [];
                if v.ty ~= AVM.TY_BOOL; err = -7; return; end
                if v.b; t = instr.arg + 1;
                    if t < 1 || t > n; err = -6; return; end; npc = t; end
            elseif instr.op == AVM.OP_PRIM
                arity = 2; if instr.arg == AVM.PRIM_NOT; arity = 1; end
                if length(s.stack) < arity; err = -4; return; end
                b = []; if arity >= 2; b = s.stack{end}; s.stack(end) = []; end
                a = s.stack{end}; s.stack(end) = [];
                s.stack{end+1} = AVM.exec_prim(instr.arg, a, b);
            elseif instr.op == AVM.OP_HALT
                s.halted = true;
            end
            s.pc = npc;
        end

        function s = run(init, prog, fuel)
            if nargin < 3; fuel = 10000; end
            s = init;
            for i = 1:fuel
                if s.halted; return; end
                [s, err] = AVM.step(s, prog);
                if err; error(['AVM error: ' num2str(err)]); end
            end
        end
    end
end