mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
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).
This commit is contained in:
parent
aeb87d86c8
commit
1ae311c63f
5 changed files with 203 additions and 112 deletions
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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) ────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue