From 1ae311c63f119c253be550dd05d4a71f718df566 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 30 Jun 2026 17:39:06 -0500 Subject: [PATCH] fix(avm-ports): add Q0_16 support to Julia and R ports 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). --- coq/CoreFormalism/.Q16_16.aux | 17 ++++- coq/CoreFormalism/Q16_16.glob | 123 +++++++++++++++++++++------------- coq/CoreFormalism/Q16_16.v | 24 ++++--- julia/AVMIsa/avm.jl | 87 +++++++++++++----------- r/AVMIsa/avm.r | 64 ++++++++++++------ 5 files changed, 203 insertions(+), 112 deletions(-) diff --git a/coq/CoreFormalism/.Q16_16.aux b/coq/CoreFormalism/.Q16_16.aux index 34c87b94..1f7759e2 100644 --- a/coq/CoreFormalism/.Q16_16.aux +++ b/coq/CoreFormalism/.Q16_16.aux @@ -1,2 +1,17 @@ -COQAUX1 03441a4df6ed6fdae62bc8cdd91bb74d /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v +COQAUX1 ceddd47b5a988a61f1c6220b6dcc1771 /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v +0 0 VernacProof "tac:no using:no" +164 168 proof_build_time "0.001" +0 0 le_neg2147483648_2147483647 "0.001" +159 163 context_used "" +164 168 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +245 249 proof_build_time "0.000" +0 0 le_2147483647_2147483647 "0.000" +240 244 context_used "" +245 249 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +1092 1096 proof_build_time "0.002" +0 0 clamp_bounded "0.002" +1055 1089 context_used "" +1092 1096 proof_check_time "0.001" 0 0 VernacProof "tac:no using:no" diff --git a/coq/CoreFormalism/Q16_16.glob b/coq/CoreFormalism/Q16_16.glob index 52ade12a..0069ab77 100644 --- a/coq/CoreFormalism/Q16_16.glob +++ b/coq/CoreFormalism/Q16_16.glob @@ -1,49 +1,82 @@ -DIGEST 03441a4df6ed6fdae62bc8cdd91bb74d +DIGEST ceddd47b5a988a61f1c6220b6dcc1771 FQ16_16 R72:77 Stdlib.ZArith.ZArith <> <> lib R79:81 Stdlib.micromega.Lia <> <> lib -mod 91:96 <> Q16_16 -def 135:145 Q16_16 q16_min_raw -R149:149 Corelib.Numbers.BinNums <> Z ind -def 180:190 Q16_16 q16_max_raw -R194:194 Corelib.Numbers.BinNums <> Z ind -def 224:232 Q16_16 q16_scale -R237:237 Corelib.Numbers.BinNums <> Z ind -def 263:270 Q16_16 in_range -R277:277 Corelib.Numbers.BinNums <> Z ind -binder 273:273 <> x:1 -R310:313 Corelib.Init.Logic <> ::type_scope:x_'/\'_x not -R305:308 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not -R294:304 Q16_16 Q16_16 q16_min_raw def -R309:309 Q16_16 <> x:1 var -R315:318 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not -R314:314 Q16_16 <> x:1 var -R319:329 Q16_16 Q16_16 q16_max_raw def -def 346:354 Q16_16 clamp_raw +prf 91:117 <> le_neg2147483648_2147483647 +R133:136 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +prf 176:199 <> le_2147483647_2147483647 +R214:217 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +mod 258:263 <> Q16_16 +def 302:312 Q16_16 q16_min_raw +R316:316 Corelib.Numbers.BinNums <> Z ind +def 347:357 Q16_16 q16_max_raw R361:361 Corelib.Numbers.BinNums <> Z ind -binder 357:357 <> i:2 -R366:366 Corelib.Numbers.BinNums <> Z ind -R378:385 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def -R399:399 Q16_16 <> i:2 var -R387:397 Q16_16 Q16_16 q16_max_raw def -R430:437 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def -R441:451 Q16_16 Q16_16 q16_min_raw def -R439:439 Q16_16 <> i:2 var -R479:479 Q16_16 <> i:2 var -R458:468 Q16_16 Q16_16 q16_min_raw def -R406:416 Q16_16 Q16_16 q16_max_raw def -prf 493:505 Q16_16 clamp_bounded -R512:512 Corelib.Numbers.BinNums <> Z ind -binder 508:508 <> x:3 -R517:524 Q16_16 Q16_16 in_range def -R527:535 Q16_16 Q16_16 clamp_raw def -R537:537 Q16_16 <> x:3 var -R561:569 Q16_16 Q16_16 clamp_raw def -R572:579 Q16_16 Q16_16 in_range def -R592:599 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def -R601:611 Q16_16 Q16_16 q16_max_raw def -R592:599 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def -R601:611 Q16_16 Q16_16 q16_max_raw def -R641:651 Q16_16 Q16_16 q16_min_raw def -R654:664 Q16_16 Q16_16 q16_max_raw def -R695:706 Stdlib.ZArith.BinInt Z lt_le_incl thm +def 391:399 Q16_16 q16_scale +R404:404 Corelib.Numbers.BinNums <> Z ind +def 430:437 Q16_16 in_range +R444:444 Corelib.Numbers.BinNums <> Z ind +binder 440:440 <> x:1 +R477:480 Corelib.Init.Logic <> ::type_scope:x_'/\'_x not +R472:475 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +R461:471 Q16_16 Q16_16 q16_min_raw def +R476:476 Q16_16 <> x:1 var +R482:485 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +R481:481 Q16_16 <> x:1 var +R486:496 Q16_16 Q16_16 q16_max_raw def +def 513:521 Q16_16 clamp_raw +R528:528 Corelib.Numbers.BinNums <> Z ind +binder 524:524 <> i:2 +R533:533 Corelib.Numbers.BinNums <> Z ind +R545:552 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R566:566 Q16_16 <> i:2 var +R554:564 Q16_16 Q16_16 q16_max_raw def +R597:604 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R608:618 Q16_16 Q16_16 q16_min_raw def +R606:606 Q16_16 <> i:2 var +R646:646 Q16_16 <> i:2 var +R625:635 Q16_16 Q16_16 q16_min_raw def +R573:583 Q16_16 Q16_16 q16_max_raw def +prf 660:672 Q16_16 clamp_bounded +R679:679 Corelib.Numbers.BinNums <> Z ind +binder 675:675 <> x:3 +R684:691 Q16_16 Q16_16 in_range def +R694:702 Q16_16 Q16_16 clamp_raw def +R704:704 Q16_16 <> x:3 var +R728:736 Q16_16 Q16_16 clamp_raw def +R739:746 Q16_16 Q16_16 in_range def +R759:766 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R768:778 Q16_16 Q16_16 q16_max_raw def +R759:766 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R768:778 Q16_16 Q16_16 q16_max_raw def +R808:818 Q16_16 Q16_16 q16_min_raw def +R821:831 Q16_16 Q16_16 q16_max_raw def +R848:874 Q16_16 <> le_neg2147483648_2147483647 thm +R884:892 Stdlib.ZArith.BinInt Z le_refl thm +R848:874 Q16_16 <> le_neg2147483648_2147483647 thm +R884:892 Stdlib.ZArith.BinInt Z le_refl thm +R908:915 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R919:929 Q16_16 Q16_16 q16_min_raw def +R908:915 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R919:929 Q16_16 Q16_16 q16_min_raw def +R959:969 Q16_16 Q16_16 q16_min_raw def +R972:982 Q16_16 Q16_16 q16_max_raw def +R999:1007 Stdlib.ZArith.BinInt Z le_refl thm +R1017:1043 Q16_16 <> le_neg2147483648_2147483647 thm +R999:1007 Stdlib.ZArith.BinInt Z le_refl thm +R1017:1043 Q16_16 <> le_neg2147483648_2147483647 thm +R1068:1075 Stdlib.ZArith.BinInt Z nlt_ge thm +R1068:1075 Stdlib.ZArith.BinInt Z nlt_ge thm +R1068:1075 Stdlib.ZArith.BinInt Z nlt_ge thm +prf 1108:1123 Q16_16 clamp_idempotent +R1130:1130 Corelib.Numbers.BinNums <> Z ind +binder 1126:1126 <> x:4 +R1138:1145 Q16_16 Q16_16 in_range def +R1147:1147 Q16_16 <> x:4 var +binder 1134:1134 <> h:5 +R1163:1165 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R1152:1160 Q16_16 Q16_16 clamp_raw def +R1162:1162 Q16_16 <> x:4 var +R1166:1166 Q16_16 <> x:4 var +R1218:1226 Q16_16 Q16_16 clamp_raw def +R1239:1246 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1248:1258 Q16_16 Q16_16 q16_max_raw def diff --git a/coq/CoreFormalism/Q16_16.v b/coq/CoreFormalism/Q16_16.v index 441fb47f..ee37679b 100644 --- a/coq/CoreFormalism/Q16_16.v +++ b/coq/CoreFormalism/Q16_16.v @@ -1,5 +1,12 @@ (* Coq Formalization of Q16_16 Fixed-Point Arithmetic *) Require Import ZArith Lia. + +Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z. +Proof. lia. Qed. + +Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z. +Proof. lia. Qed. + Module Q16_16. Open Scope Z_scope. @@ -19,9 +26,9 @@ Module Q16_16. Proof. unfold clamp_raw, in_range. case (Z_lt_dec q16_max_raw x); intros H1. - - unfold q16_min_raw, q16_max_raw; split; [unfold q16_min_raw, q16_max_raw; lia | apply Z.lt_le_incl; exact H1]. + - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Z.le_refl]. - case (Z_lt_dec x q16_min_raw); intros H2. - + unfold q16_min_raw, q16_max_raw; split; [apply Z.lt_le_incl; exact H2 | unfold q16_min_raw, q16_max_raw; lia]. + + unfold q16_min_raw, q16_max_raw; split; [apply Z.le_refl | apply le_neg2147483648_2147483647]. + split; apply Z.nlt_ge; assumption. Qed. @@ -29,8 +36,8 @@ Module Q16_16. Proof. destruct h as [Hlo Hhi]. unfold clamp_raw. - case (Z_lt_dec q16_max_raw x); intros Hgt; [exfalso; lia|]. - case (Z_lt_dec x q16_min_raw); intros Hlt; [exfalso; lia|]. + case (Z_lt_dec q16_max_raw x); intros Hgt; [exfalso; exact (Zlt_not_le _ _ Hgt Hhi) |]. + case (Z_lt_dec x q16_min_raw); intros Hlt; [exfalso; exact (Zlt_not_le _ _ Hlt Hlo) |]. reflexivity. Qed. @@ -56,22 +63,23 @@ Module Q16_16. Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b) (hsum : in_range (a + b)) : add a b = a + b. Proof. - unfold add; rewrite clamp_idempotent; [reflexivity| exact hsum]. + unfold add; rewrite clamp_idempotent; trivial. Qed. Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero. Proof. unfold sub, zero; rewrite Z.sub_diag. - apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw; lia. + apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw. + split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. Qed. Theorem mul_comm (a b : Z) : mul a b = mul b a. Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed. Theorem in_range_zero : in_range 0. - Proof. unfold in_range, q16_min_raw, q16_max_raw; lia. Qed. + Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. Qed. Theorem in_range_one : in_range 1. - Proof. unfold in_range, q16_min_raw, q16_max_raw; lia. Qed. + Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. Qed. End Q16_16. diff --git a/julia/AVMIsa/avm.jl b/julia/AVMIsa/avm.jl index 202c07fe..e0cbed73 100644 --- a/julia/AVMIsa/avm.jl +++ b/julia/AVMIsa/avm.jl @@ -69,22 +69,29 @@ end # ── AVM constants ─────────────────────────────────────────────────── const AVM_CLAMP_MIN = -2147483647 const AVM_CLAMP_MAX = 2147483647 +const AVM_Q0_MIN = -32767 +const AVM_Q0_MAX = 32767 const AVM_MAX_STACK = 1024 +# Type tags: 0=Bool, 1=Q16_16, 2=Q0_16 +const TYPE_BOOL = Int8(0) +const TYPE_Q16 = Int8(1) +const TYPE_Q0 = Int8(2) + # ── State ────────────────────────────────────────────────────────── struct State pc::Int stack::Vector{Union{Int32, Bool}} - is_q16::Vector{Bool} # true=Q16_16, false=Bool + types::Vector{Int8} # 0=Bool, 1=Q16_16, 2=Q0_16 locals::Vector{Union{Nothing, Union{Int32, Bool}}} - local_types::Vector{Bool} # true=Q16_16, false=Bool (or nothing) + local_types::Vector{Int8} halted::Bool end function State(n_locals::Int=0) - State(1, Union{Int32, Bool}[], Bool[], - [nothing for _ in 1:n_locals], [false for _ in 1:n_locals], + State(1, Union{Int32, Bool}[], Int8[], + [nothing for _ in 1:n_locals], zeros(Int8, n_locals), false) end @@ -94,37 +101,41 @@ q16_val(v::Int32) = v # ── Primitive execution ──────────────────────────────────────────── -# AVM symmetric clamp (excludes INT32_MIN for negation involution) avm_clamp(x::Int64) = Int32(min(AVM_CLAMP_MAX, max(AVM_CLAMP_MIN, x))) +avm_q0_clamp(x::Int64) = Int32(min(AVM_Q0_MAX, max(AVM_Q0_MIN, x))) -# V6 signed comparison for AVM lt_q16_v6(a::Int32, b::Int32) = (a < 0) != (b < 0) ? (a < 0) : (a < b) function exec_prim(op::Prim, a::Union{Int32, Bool}, b::Union{Int32, Bool, Nothing}) - if op == ADD_SAT_Q16 - return (avm_clamp(Int64(a::Int32) + Int64(b::Int32)), true) + if op == ADD_SAT_Q0 + a::Int32; b::Int32 + return (avm_q0_clamp(Int64(a) + Int64(b)), TYPE_Q0) + elseif op == SUB_SAT_Q0 + a::Int32; b::Int32 + return (avm_q0_clamp(Int64(a) - Int64(b)), TYPE_Q0) + elseif op == ADD_SAT_Q16 + return (avm_clamp(Int64(a::Int32) + Int64(b::Int32)), TYPE_Q16) elseif op == SUB_SAT_Q16 - return (avm_clamp(Int64(a::Int32) - Int64(b::Int32)), true) + return (avm_clamp(Int64(a::Int32) - Int64(b::Int32)), TYPE_Q16) elseif op == MUL_SAT_Q16 - # Floor division matching Lean Int.ediv: (a * b) / 65536 prod = Int64(a::Int32) * Int64(b::Int32) - result = div(prod, Q16_16.Q16_SCALE) # div = floor division in Julia - return (avm_clamp(result), true) + result = div(prod, Q16_16.Q16_SCALE) + return (avm_clamp(result), TYPE_Q16) elseif op == DIV_SAT_Q16 b::Int32 == 0 && error(DIVISION_BY_ZERO) num = Int64(b::Int32) * Q16_16.Q16_SCALE - result = div(num, Int64(a::Int32)) # div = floor division in Julia - return (avm_clamp(result), true) + result = div(num, Int64(a::Int32)) + return (avm_clamp(result), TYPE_Q16) elseif op == LT_Q16 - return (lt_q16_v6(a::Int32, b::Int32), false) + return (lt_q16_v6(a::Int32, b::Int32), TYPE_BOOL) elseif op == EQ_Q16 - return (a::Int32 == b::Int32, false) + return (a::Int32 == b::Int32, TYPE_BOOL) elseif op == AND_OP - return (a::Bool && b::Bool, false) + return (a::Bool && b::Bool, TYPE_BOOL) elseif op == OR_OP - return (a::Bool || b::Bool, false) + return (a::Bool || b::Bool, TYPE_BOOL) elseif op == NOT_OP - return (!a::Bool, false) + return (!a::Bool, TYPE_BOOL) else error(TYPE_MISMATCH) end @@ -134,14 +145,14 @@ end function step(s::State, program::Vector{Instr})::State s.halted && error(HALTED) - s.pc < 1 && return State(s.pc, copy(s.stack), copy(s.is_q16), + s.pc < 1 && return State(s.pc, copy(s.stack), copy(s.types), copy(s.locals), copy(s.local_types), true) - s.pc > length(program) && return State(s.pc, copy(s.stack), copy(s.is_q16), + s.pc > length(program) && return State(s.pc, copy(s.stack), copy(s.types), copy(s.locals), copy(s.local_types), true) instr = program[s.pc] stack = copy(s.stack) - is_q16 = copy(s.is_q16) + types = copy(s.types) locals = copy(s.locals) local_types = copy(s.local_types) pc = s.pc + 1 @@ -151,39 +162,39 @@ function step(s::State, program::Vector{Instr})::State if instr.op == 0 # push_val (Bool) push!(stack, instr.arg2) - push!(is_q16, false) + push!(types, TYPE_BOOL) elseif instr.op == 1 # push_q16 push!(stack, instr.arg) - push!(is_q16, true) + push!(types, TYPE_Q16) elseif instr.op == 2 # pop isempty(stack) && error(EMPTY_STACK) - pop!(stack); pop!(is_q16) + pop!(stack); pop!(types) elseif instr.op == 3 # dup isempty(stack) && error(EMPTY_STACK) - push!(stack, stack[end]); push!(is_q16, is_q16[end]) + push!(stack, stack[end]); push!(types, types[end]) elseif instr.op == 4 # swap length(stack) < 2 && error(STACK_UNDERFLOW) - a = pop!(stack); ta = pop!(is_q16) - b = pop!(stack); tb = pop!(is_q16) - push!(stack, a); push!(is_q16, ta) - push!(stack, b); push!(is_q16, tb) + a = pop!(stack); ta = pop!(types) + b = pop!(stack); tb = pop!(types) + push!(stack, a); push!(types, ta) + push!(stack, b); push!(types, tb) elseif instr.op == 5 # load i = Int(instr.arg) + 1 i > length(locals) && error(MISSING_LOCAL) locals[i] === nothing && error(MISSING_LOCAL) - push!(stack, locals[i]); push!(is_q16, local_types[i]) + push!(stack, locals[i]); push!(types, local_types[i]) elseif instr.op == 6 # store i = Int(instr.arg) + 1 isempty(stack) && error(EMPTY_STACK) i > length(locals) && error(MISSING_LOCAL) - locals[i] = pop!(stack); local_types[i] = pop!(is_q16) + locals[i] = pop!(stack); local_types[i] = pop!(types) elseif instr.op == 7 # jump target = Int(instr.arg) + 1 (target < 1 || target > length(program)) && error(JUMP_OUT_OF_BOUNDS) pc = target elseif instr.op == 8 # jump_if isempty(stack) && error(EMPTY_STACK) - cond = pop!(stack)::Bool; pop!(is_q16) + cond = pop!(stack)::Bool; pop!(types) if cond target = Int(instr.arg) + 1 (target < 1 || target > length(program)) && error(JUMP_OUT_OF_BOUNDS) @@ -193,17 +204,17 @@ function step(s::State, program::Vector{Instr})::State p = Prim(instr.arg) arity = (p == NOT_OP) ? 1 : 2 length(stack) < arity && error(STACK_UNDERFLOW) - b = arity >= 2 ? pop!(stack) : nothing; if arity >= 2; pop!(is_q16); end - a = pop!(stack); pop!(is_q16) - result, is_q = exec_prim(p, a, b) - push!(stack, result); push!(is_q16, is_q) + b = arity >= 2 ? pop!(stack) : nothing; if arity >= 2; pop!(types); end + a = pop!(stack); pop!(types) + result, type_tag = exec_prim(p, a, b) + push!(stack, result); push!(types, type_tag) elseif instr.op == 10 # halt halted = true else error(UNKNOWN_INSTR) end - State(pc, stack, is_q16, locals, local_types, halted) + State(pc, stack, types, locals, local_types, halted) end # ── Run (fuel-bounded) ──────────────────────────────────────────── diff --git a/r/AVMIsa/avm.r b/r/AVMIsa/avm.r index 89f0b451..e2203cc2 100644 --- a/r/AVMIsa/avm.r +++ b/r/AVMIsa/avm.r @@ -12,27 +12,30 @@ INSTR_PUSH_Q16 <- 0L INSTR_PUSH_BOOL <- 1L -INSTR_POP <- 2L -INSTR_DUP <- 3L -INSTR_SWAP <- 4L -INSTR_LOAD <- 5L -INSTR_STORE <- 6L -INSTR_JUMP <- 7L -INSTR_JUMP_IF <- 8L -INSTR_PRIM <- 9L -INSTR_HALT <- 10L +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_Q16 <- 0L -PRIM_SUB_Q16 <- 1L -PRIM_MUL_Q16 <- 2L -PRIM_DIV_Q16 <- 3L -PRIM_LT_Q16 <- 4L -PRIM_EQ_Q16 <- 5L -PRIM_AND <- 6L -PRIM_OR <- 7L -PRIM_NOT <- 8L +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 ───────────────────────────────────────────────── @@ -49,12 +52,15 @@ ERR_HALTED <- "halted" 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) @@ -80,9 +86,11 @@ new_state <- function(n_locals = 0L) { # ── 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 ─────────────────────────────────────────────────── @@ -116,8 +124,18 @@ q16_div <- function(a, 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_Q16) { + 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)) @@ -175,6 +193,8 @@ step <- function(s, prog) { 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)] @@ -189,7 +209,11 @@ step <- function(s, prog) { i <- instr$arg + 1L if (i > length(locals)) stop(ERR_MISSING_LOCAL) if (is.null(locals[[i]])) stop(ERR_MISSING_LOCAL) - stack <- c(stack, list(make_q16(locals[[i]]))) + # 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)