diff --git a/PORTING_MANIFEST.md b/PORTING_MANIFEST.md index 1e1c787c..e39d8825 100644 --- a/PORTING_MANIFEST.md +++ b/PORTING_MANIFEST.md @@ -7,7 +7,7 @@ All other languages provide independent cross-validation. | Lean module | R | Julia | Rust | Coq | |---|---|---|---|---| -| `CoreFormalism/FixedPoint.lean` (Q16_16) | — | ✅ | ✅ | — | +| `CoreFormalism/FixedPoint.lean` (Q16_16) | — | ✅ | ✅ | ✅ | | `CoreFormalism/BraidCross.lean` | — | — | — | — | | `CoreFormalism/BraidStrand.lean` | — | — | — | — | | `CoreFormalism/BraidBracket.lean` | — | — | — | — | @@ -16,10 +16,10 @@ All other languages provide independent cross-validation. | `CoreFormalism/SieveLemmas.lean` | — | — | — | — | | `CoreFormalism/InteractionGraphSidon.lean` | — | — | — | — | | `CoreFormalism/SidonSets.lean` | — | — | — | — | -| `CoreFormalism/Q16_16Numerics.lean` | — | — | — | — | -| `SilverSight/PIST/Spectral.lean` | — | — | — | — | +| `CoreFormalism/Q16_16Numerics.lean` | — | — | ✅ | ✅ | +| `SilverSight/PIST/Spectral.lean` | — | — | ✅ | — | | `SilverSight/PIST/Classify.lean` | — | — | — | — | -| `SilverSight/AVMIsa/Types.lean` (AVM) | — | ✅ | ✅ | — | +| `SilverSight/AVMIsa/Types.lean` (AVM) | ✅ | ✅ | ✅ | — | | `SilverSight/RRC/Emit.lean` | — | — | — | — | | `python/nuvmap/projection_engine.py` | ✅ | ✅ | ✅ | — | diff --git a/c/avm.c b/c/avm.c new file mode 100644 index 00000000..60a8f09a --- /dev/null +++ b/c/avm.c @@ -0,0 +1,197 @@ +/* AVM ISA v1 — C Port (Strict Functional Execution) */ + +#include +#include +#include +#include + +/* ── Constants ─────────────────────────────────────────────── */ +#define AVM_CLAMP_MIN (-2147483647) +#define AVM_CLAMP_MAX 2147483647 +#define AVM_Q0_MIN (-32767) +#define AVM_Q0_MAX 32767 +#define Q16_SCALE 65536 +#define AVM_MAX_STACK 1024 +#define AVM_MAX_LOCALS 256 + +/* ── Clamp ─────────────────────────────────────────────────── */ +static inline int32_t avm_clamp(int64_t x) { + if (x > AVM_CLAMP_MAX) return AVM_CLAMP_MAX; + if (x < AVM_CLAMP_MIN) return AVM_CLAMP_MIN; + return (int32_t)x; +} + +static inline int32_t avm_q0_clamp(int64_t x) { + if (x > AVM_Q0_MAX) return AVM_Q0_MAX; + if (x < AVM_Q0_MIN) return AVM_Q0_MIN; + return (int32_t)x; +} + +/* Floor division matching Lean Int.ediv (rounds toward -inf) */ +static inline int32_t floor_div(int64_t a, int64_t b) { + if (b == 0) return 0; + int64_t q = a / b; + int64_t r = a % b; + if (r != 0 && ((a ^ b) < 0)) q--; + return (int32_t)q; +} + +static inline bool lt_q16_v6(int32_t a, int32_t b) { + bool sa = a < 0, sb = b < 0; + return (sa != sb) ? sa : (a < b); +} + +/* ── Types ─────────────────────────────────────────────────── */ +typedef enum { TY_Q0, TY_Q16, TY_BOOL } AvmTy; + +typedef struct { + AvmTy ty; + union { int32_t i; bool b; } val; +} AnyVal; + +/* ── Instructions ──────────────────────────────────────────── */ +typedef enum { + OP_PUSH_Q16, OP_PUSH_BOOL, OP_PUSH_Q0, + OP_POP, OP_DUP, OP_SWAP, OP_LOAD, OP_STORE, + OP_JUMP, OP_JUMP_IF, OP_PRIM, OP_HALT +} OpCode; + +typedef enum { + PRIM_ADD_Q0, PRIM_SUB_Q0, PRIM_ADD_Q16, PRIM_SUB_Q16, + PRIM_MUL_Q16, PRIM_DIV_Q16, PRIM_LT_Q16, PRIM_EQ_Q16, + PRIM_AND, PRIM_OR, PRIM_NOT +} PrimCode; + +typedef struct { OpCode op; int32_t arg; bool arg2; } Instr; + +/* ── State ─────────────────────────────────────────────────── */ +typedef struct { + int pc; + AnyVal stack[AVM_MAX_STACK]; + int sp; + AnyVal locals[AVM_MAX_LOCALS]; + bool local_set[AVM_MAX_LOCALS]; + bool halted; +} State; + +void init_state(State *s, int n_locals) { + s->pc = 0; s->sp = 0; s->halted = false; + for (int i = 0; i < n_locals && i < AVM_MAX_LOCALS; i++) s->local_set[i] = false; +} + +/* ── Primitive execution ───────────────────────────────────── */ +AnyVal eval_prim(PrimCode p, AnyVal a, AnyVal b) { + AnyVal r = { .ty = TY_Q0, .val.i = 0 }; + if (p == PRIM_ADD_Q0) { + if (a.ty != TY_Q0 || b.ty != TY_Q0) return r; + r.ty = TY_Q0; r.val.i = avm_q0_clamp((int64_t)a.val.i + b.val.i); + } else if (p == PRIM_SUB_Q0) { + if (a.ty != TY_Q0 || b.ty != TY_Q0) return r; + r.ty = TY_Q0; r.val.i = avm_q0_clamp((int64_t)a.val.i - b.val.i); + } else if (p == PRIM_ADD_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16) return r; + r.ty = TY_Q16; r.val.i = avm_clamp((int64_t)a.val.i + b.val.i); + } else if (p == PRIM_SUB_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16) return r; + r.ty = TY_Q16; r.val.i = avm_clamp((int64_t)a.val.i - b.val.i); + } else if (p == PRIM_MUL_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16) return r; + r.ty = TY_Q16; + r.val.i = avm_clamp(floor_div((int64_t)a.val.i * b.val.i, Q16_SCALE)); + } else if (p == PRIM_DIV_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16 || b.val.i == 0) return r; + r.ty = TY_Q16; + r.val.i = avm_clamp(floor_div((int64_t)a.val.i * Q16_SCALE, b.val.i)); + } else if (p == PRIM_LT_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16) return r; + r.ty = TY_BOOL; r.val.b = lt_q16_v6(a.val.i, b.val.i); + } else if (p == PRIM_EQ_Q16) { + if (a.ty != TY_Q16 || b.ty != TY_Q16) return r; + r.ty = TY_BOOL; r.val.b = (a.val.i == b.val.i); + } else if (p == PRIM_AND) { + if (a.ty != TY_BOOL || b.ty != TY_BOOL) return r; + r.ty = TY_BOOL; r.val.b = a.val.b && b.val.b; + } else if (p == PRIM_OR) { + if (a.ty != TY_BOOL || b.ty != TY_BOOL) return r; + r.ty = TY_BOOL; r.val.b = a.val.b || b.val.b; + } else if (p == PRIM_NOT) { + if (a.ty != TY_BOOL) return r; + r.ty = TY_BOOL; r.val.b = !a.val.b; + } + return r; +} + +/* ── Step ──────────────────────────────────────────────────── */ +int step(State *s, const Instr *prog, int prog_len) { + if (s->halted) return -1; + if (s->pc < 0 || s->pc >= prog_len) { s->halted = true; return 0; } + + Instr instr = prog[s->pc]; + int npc = s->pc + 1; + + /* Check stack depth for growing ops */ + if (instr.op <= OP_PUSH_Q0 || instr.op == OP_DUP || instr.op == OP_LOAD) { + if (s->sp >= AVM_MAX_STACK) return -2; /* stack overflow */ + } + + if (instr.op == OP_PUSH_Q16) { + s->stack[s->sp].ty = TY_Q16; s->stack[s->sp].val.i = avm_clamp(instr.arg); s->sp++; + } else if (instr.op == OP_PUSH_BOOL) { + s->stack[s->sp].ty = TY_BOOL; s->stack[s->sp].val.b = instr.arg2; s->sp++; + } else if (instr.op == OP_PUSH_Q0) { + s->stack[s->sp].ty = TY_Q0; s->stack[s->sp].val.i = avm_q0_clamp(instr.arg); s->sp++; + } else if (instr.op == OP_POP) { + if (s->sp <= 0) return -3; /* empty stack */ + s->sp--; + } else if (instr.op == OP_DUP) { + if (s->sp <= 0) return -3; + s->stack[s->sp] = s->stack[s->sp - 1]; s->sp++; + } else if (instr.op == OP_SWAP) { + if (s->sp < 2) return -4; /* underflow */ + AnyVal tmp = s->stack[s->sp - 1]; + s->stack[s->sp - 1] = s->stack[s->sp - 2]; + s->stack[s->sp - 2] = tmp; + } else if (instr.op == OP_LOAD) { + int i = instr.arg; + if (i < 0 || i >= AVM_MAX_LOCALS || !s->local_set[i]) return -5; /* missing local */ + s->stack[s->sp] = s->locals[i]; s->sp++; + } else if (instr.op == OP_STORE) { + if (s->sp <= 0) return -3; + int i = instr.arg; + if (i < 0 || i >= AVM_MAX_LOCALS) return -5; + s->locals[i] = s->stack[--s->sp]; s->local_set[i] = true; + } else if (instr.op == OP_JUMP) { + if (instr.arg < 0 || instr.arg >= prog_len) return -6; /* jump OOB */ + npc = instr.arg; + } else if (instr.op == OP_JUMP_IF) { + if (s->sp <= 0) return -3; + AnyVal v = s->stack[--s->sp]; + if (v.ty != TY_BOOL) return -7; /* type mismatch */ + if (v.val.b) { + if (instr.arg < 0 || instr.arg >= prog_len) return -6; + npc = instr.arg; + } + } else if (instr.op == OP_PRIM) { + PrimCode p = (PrimCode)instr.arg; + int arity = (p == PRIM_NOT) ? 1 : 2; + if (s->sp < arity) return -4; + AnyVal b = (arity >= 2) ? s->stack[--s->sp] : (AnyVal){0}; + AnyVal a = s->stack[--s->sp]; + s->stack[s->sp++] = eval_prim(p, a, b); + } else if (instr.op == OP_HALT) { + s->halted = true; + } + + s->pc = npc; + return 0; +} + +/* ── Run (fuel-bounded) ────────────────────────────────────── */ +int run(State *s, const Instr *prog, int prog_len, int fuel) { + for (int i = 0; i < fuel; i++) { + if (s->halted) return 0; + int err = step(s, prog, prog_len); + if (err) return err; + } + return 0; +} diff --git a/coq/AVMIsa/avm.v b/coq/AVMIsa/avm.v new file mode 100644 index 00000000..595695bd --- /dev/null +++ b/coq/AVMIsa/avm.v @@ -0,0 +1,165 @@ +(* AVM ISA v1 — Coq Port (Strict Functional Execution) + Mirrors formal/SilverSight/AVMIsa/Step.lean *) + +Require Import ZArith. +Require Import List. +Import ListNotations. + +(* ── Constants ──────────────────────────────────────────────────── *) +Definition AVM_CLAMP_MIN : Z := -2147483647. +Definition AVM_CLAMP_MAX : Z := 2147483647. +Definition AVM_Q0_MIN : Z := -32767. +Definition AVM_Q0_MAX : Z := 32767. +Definition Q16_SCALE : Z := 65536. + +Definition avm_clamp (x : Z) : Z := + Z.min AVM_CLAMP_MAX (Z.max AVM_CLAMP_MIN x). + +Definition avm_q0_clamp (x : Z) : Z := + Z.min AVM_Q0_MAX (Z.max AVM_Q0_MIN x). + +Definition lt_q16_v6 (a b : Z) : bool := + let sa := a AvmVal +| Vq16 : Z -> AvmVal +| Vbool : bool -> AvmVal. + +(* ── Primitives ──────────────────────────────────────────────────── *) +Inductive Prim : Type := +| AddSatQ0 | SubSatQ0 +| AddSatQ16 | SubSatQ16 | MulSatQ16 | DivSatQ16 +| LtQ16 | EqQ16 +| And | Or | Not. + +(* ── Instructions ────────────────────────────────────────────────── *) +Inductive Instr : Type := +| PushQ16 (x : Z) | PushBool (b : bool) | PushQ0 (x : Z) +| Pop | Dup | Swap +| Load (i : nat) | Store (i : nat) +| Jump (t : nat) | JumpIf (t : nat) +| Primitive (p : Prim) +| Halt. + +(* ── State ───────────────────────────────────────────────────────── *) +Definition Local := option AvmVal. + +Record State : Type := mkState { + pc : nat; + stack : list AvmVal; + locals : list Local; + halted : bool +}. + +Definition init_state (n : nat) : State := + mkState 0 [] (repeat None n) false. + +(* ── Primitive execution ────────────────────────────────────────── *) +Definition div_floor (a b : Z) : Z := + if b =? 0 then 0 else + let q := a / b in + let r := a mod b in + if (r ? 0) && (b ? 0) then q - 1 + else q. + +Definition exec_prim (p : Prim) (a b : AvmVal) : AvmVal := + match p, a, b with + | AddSatQ0, Vq0 x, Vq0 y => Vq0 (avm_q0_clamp (x + y)) + | SubSatQ0, Vq0 x, Vq0 y => Vq0 (avm_q0_clamp (x - y)) + | AddSatQ16, Vq16 x, Vq16 y => Vq16 (avm_clamp (x + y)) + | SubSatQ16, Vq16 x, Vq16 y => Vq16 (avm_clamp (x - y)) + | MulSatQ16, Vq16 x, Vq16 y => Vq16 (avm_clamp (div_floor (x * y) Q16_SCALE)) + | DivSatQ16, Vq16 x, Vq16 y => Vq16 (avm_clamp (div_floor (x * Q16_SCALE) y)) + | LtQ16, Vq16 x, Vq16 y => Vbool (lt_q16_v6 x y) + | EqQ16, Vq16 x, Vq16 y => Vbool (x =? y) + | And, Vbool x, Vbool y => Vbool (x && y) + | Or, Vbool x, Vbool y => Vbool (x || y) + | Not, Vbool x, _ => Vbool (negb x) + | _, _, _ => Vbool false + end. + +(* ── Step ────────────────────────────────────────────────────────── *) +Definition step (s : State) (prog : list Instr) : option State := + if halted s then None else + if Nat.leb (length prog) (pc s) then + Some (mkState (pc s) (stack s) (locals s) true) + else + let instr := nth (pc s) prog Halt in + let stk := stack s in + let loc := locals s in + let npc := S (pc s) in + match instr with + | PushQ16 x => Some (mkState npc (Vq16 (avm_clamp x) :: stk) loc false) + | PushBool b => Some (mkState npc (Vbool b :: stk) loc false) + | PushQ0 x => Some (mkState npc (Vq0 (avm_q0_clamp x) :: stk) loc false) + | Pop => match stk with + | [] => None + | _ :: xs => Some (mkState npc xs loc false) + end + | Dup => match stk with + | [] => None + | x :: xs => Some (mkState npc (x :: x :: xs) loc false) + end + | Swap => match stk with + | a :: b :: xs => Some (mkState npc (b :: a :: xs) loc false) + | _ => None + end + | Load i => + match nth_error loc i with + | None => None + | Some None => None + | Some (Some v) => Some (mkState npc (v :: stk) loc false) + end + | Store i => + match stk with + | [] => None + | v :: xs => + if Nat.leb (length loc) i then None + else + let new_loc := set_nth loc i (Some v) in + Some (mkState npc xs new_loc false) + end + | Jump t => + if Nat.leb (length prog) t then None + else Some (mkState t stk loc false) + | JumpIf t => + match stk with + | Vbool true :: xs => + if Nat.leb (length prog) t then None + else Some (mkState t xs loc false) + | Vbool false :: xs => Some (mkState npc xs loc false) + | _ => None + end + | Primitive p => + let arity := if p = Not then 1 else 2 in + match stk with + | a :: xs when arity = 1 => + Some (mkState npc (exec_prim p a a :: xs) loc false) + | b :: a :: xs when arity = 2 => + Some (mkState npc (exec_prim p a b :: xs) loc false) + | _ => None + end + | Halt => Some (mkState (pc s) stk loc true) + end. + +(* ── Run (fuel-bounded) ─────────────────────────────────────────── *) +Fixpoint run (s : State) (prog : list Instr) (fuel : nat) : option State := + match fuel with + | O => Some s + | S n => + if halted s then Some s + else match step s prog with + | None => None + | Some s' => run s' prog n + end + end. diff --git a/coq/CoreFormalism/.Q16_16.aux b/coq/CoreFormalism/.Q16_16.aux index 1f7759e2..6d97249b 100644 --- a/coq/CoreFormalism/.Q16_16.aux +++ b/coq/CoreFormalism/.Q16_16.aux @@ -1,17 +1,62 @@ -COQAUX1 ceddd47b5a988a61f1c6220b6dcc1771 /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v +COQAUX1 674cb8319be2cff2e3564b20efcaccb5 /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" +226 230 proof_build_time "0.000" +0 0 le_0_2147483647 "0.000" +221 225 context_used "" +226 230 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +292 296 proof_build_time "0.000" +0 0 le_neg2147483648_0 "0.000" +287 291 context_used "" +292 296 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +373 377 proof_build_time "0.000" 0 0 le_2147483647_2147483647 "0.000" -240 244 context_used "" -245 249 proof_check_time "0.000" +368 372 context_used "" +373 377 proof_check_time "0.000" 0 0 VernacProof "tac:no using:no" -1092 1096 proof_build_time "0.002" +1220 1224 proof_build_time "0.002" 0 0 clamp_bounded "0.002" -1055 1089 context_used "" -1092 1096 proof_check_time "0.001" +1183 1217 context_used "" +1220 1224 proof_check_time "0.001" 0 0 VernacProof "tac:no using:no" +1560 1564 proof_build_time "0.001" +0 0 clamp_idempotent "0.001" +1545 1557 context_used "" +1560 1564 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +2259 2263 proof_build_time "0.000" +0 0 add_comm "0.000" +2214 2258 context_used "" +2259 2263 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +2445 2449 proof_build_time "0.000" +0 0 add_in_range "0.000" +2396 2442 context_used "" +2445 2449 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +2708 2712 proof_build_time "0.001" +0 0 sub_self "0.001" +2647 2705 context_used "" +2708 2712 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +2818 2822 proof_build_time "0.000" +0 0 mul_comm "0.000" +2773 2817 context_used "" +2818 2822 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +2973 2977 proof_build_time "0.000" +0 0 in_range_zero "0.000" +2914 2972 context_used "" +2973 2977 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" +3127 3131 proof_build_time "0.000" +0 0 in_range_one "0.000" +3068 3126 context_used "" +3127 3131 proof_check_time "0.000" +0 0 vo_compile_time "0.140" diff --git a/coq/CoreFormalism/Q16_16.glob b/coq/CoreFormalism/Q16_16.glob index 0069ab77..6db297cd 100644 --- a/coq/CoreFormalism/Q16_16.glob +++ b/coq/CoreFormalism/Q16_16.glob @@ -1,82 +1,263 @@ -DIGEST ceddd47b5a988a61f1c6220b6dcc1771 +DIGEST 674cb8319be2cff2e3564b20efcaccb5 FQ16_16 R72:77 Stdlib.ZArith.ZArith <> <> lib R79:81 Stdlib.micromega.Lia <> <> lib 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 -def 391:399 Q16_16 q16_scale -R404:404 Corelib.Numbers.BinNums <> Z ind -def 430:437 Q16_16 in_range +prf 175:189 <> le_0_2147483647 +R195:198 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +prf 237:254 <> le_neg2147483648_0 +R270:273 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +prf 304:327 <> le_2147483647_2147483647 +R342:345 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +mod 386:391 <> Q16_16 +def 430:440 Q16_16 q16_min_raw 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 +def 475:485 Q16_16 q16_max_raw +R489:489 Corelib.Numbers.BinNums <> Z ind +def 519:527 Q16_16 q16_scale +R532:532 Corelib.Numbers.BinNums <> Z ind +def 558:565 Q16_16 in_range +R572:572 Corelib.Numbers.BinNums <> Z ind +binder 568:568 <> x:1 +R605:608 Corelib.Init.Logic <> ::type_scope:x_'/\'_x not +R600:603 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +R589:599 Q16_16 Q16_16 q16_min_raw def +R604:604 Q16_16 <> x:1 var +R610:613 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not +R609:609 Q16_16 <> x:1 var +R614:624 Q16_16 Q16_16 q16_max_raw def +def 641:649 Q16_16 clamp_raw +R656:656 Corelib.Numbers.BinNums <> Z ind +binder 652:652 <> i:2 +R661:661 Corelib.Numbers.BinNums <> Z ind +R673:680 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R694:694 Q16_16 <> i:2 var +R682:692 Q16_16 Q16_16 q16_max_raw def +R725:732 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R736:746 Q16_16 Q16_16 q16_min_raw def +R734:734 Q16_16 <> i:2 var +R774:774 Q16_16 <> i:2 var +R753:763 Q16_16 Q16_16 q16_min_raw def +R701:711 Q16_16 Q16_16 q16_max_raw def +prf 788:800 Q16_16 clamp_bounded +R807:807 Corelib.Numbers.BinNums <> Z ind +binder 803:803 <> x:3 +R812:819 Q16_16 Q16_16 in_range def +R822:830 Q16_16 Q16_16 clamp_raw def +R832:832 Q16_16 <> x:3 var +R856:864 Q16_16 Q16_16 clamp_raw def +R867:874 Q16_16 Q16_16 in_range def +R887:894 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R896:906 Q16_16 Q16_16 q16_max_raw def +R887:894 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R896:906 Q16_16 Q16_16 q16_max_raw def +R936:946 Q16_16 Q16_16 q16_min_raw def +R949:959 Q16_16 Q16_16 q16_max_raw def +R976:1002 Q16_16 <> le_neg2147483648_2147483647 thm +R1012:1020 Stdlib.ZArith.BinInt Z le_refl thm +R976:1002 Q16_16 <> le_neg2147483648_2147483647 thm +R1012:1020 Stdlib.ZArith.BinInt Z le_refl thm +R1036:1043 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1047:1057 Q16_16 Q16_16 q16_min_raw def +R1036:1043 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1047:1057 Q16_16 Q16_16 q16_min_raw def +R1087:1097 Q16_16 Q16_16 q16_min_raw def +R1100:1110 Q16_16 Q16_16 q16_max_raw def +R1127:1135 Stdlib.ZArith.BinInt Z le_refl thm +R1145:1171 Q16_16 <> le_neg2147483648_2147483647 thm +R1127:1135 Stdlib.ZArith.BinInt Z le_refl thm +R1145:1171 Q16_16 <> le_neg2147483648_2147483647 thm +R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm +R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm +R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm +prf 1236:1251 Q16_16 clamp_idempotent +R1258:1258 Corelib.Numbers.BinNums <> Z ind +binder 1254:1254 <> x:4 +R1266:1273 Q16_16 Q16_16 in_range def +R1275:1275 Q16_16 <> x:4 var +binder 1262:1262 <> h:5 +R1291:1293 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R1280:1288 Q16_16 Q16_16 clamp_raw def +R1290:1290 Q16_16 <> x:4 var +R1294:1294 Q16_16 <> x:4 var +R1346:1354 Q16_16 Q16_16 clamp_raw def +R1367:1374 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1376:1386 Q16_16 Q16_16 q16_max_raw def +R1421:1430 Stdlib.ZArith.Zorder <> Zlt_not_le thm +R1367:1374 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1376:1386 Q16_16 Q16_16 q16_max_raw def +R1421:1430 Stdlib.ZArith.Zorder <> Zlt_not_le thm +R1459:1466 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1470:1480 Q16_16 Q16_16 q16_min_raw def +R1513:1522 Stdlib.ZArith.Zorder <> Zlt_not_le thm +R1459:1466 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def +R1470:1480 Q16_16 Q16_16 q16_min_raw def +R1513:1522 Stdlib.ZArith.Zorder <> Zlt_not_le thm +def 1579:1582 Q16_16 zero +R1586:1586 Corelib.Numbers.BinNums <> Z ind +def 1607:1609 Q16_16 one +R1613:1613 Corelib.Numbers.BinNums <> Z ind +def 1638:1644 Q16_16 epsilon +R1648:1648 Corelib.Numbers.BinNums <> Z ind +def 1669:1672 Q16_16 half +R1676:1676 Corelib.Numbers.BinNums <> Z ind +def 1701:1704 Q16_16 pct1 +R1710:1710 Corelib.Numbers.BinNums <> Z ind +def 1733:1737 Q16_16 pct70 +R1742:1742 Corelib.Numbers.BinNums <> Z ind +def 1767:1771 Q16_16 pct30 +R1776:1776 Corelib.Numbers.BinNums <> Z ind +def 1801:1805 Q16_16 one50 +R1810:1810 Corelib.Numbers.BinNums <> Z ind +def 1836:1838 Q16_16 add +R1847:1847 Corelib.Numbers.BinNums <> Z ind +binder 1841:1841 <> a:6 +binder 1843:1843 <> b:7 +R1852:1852 Corelib.Numbers.BinNums <> Z ind +R1857:1865 Q16_16 Q16_16 clamp_raw def +R1869:1871 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R1868:1868 Q16_16 <> a:6 var +R1872:1872 Q16_16 <> b:7 var +def 1889:1891 Q16_16 sub +R1900:1900 Corelib.Numbers.BinNums <> Z ind +binder 1894:1894 <> a:8 +binder 1896:1896 <> b:9 +R1905:1905 Corelib.Numbers.BinNums <> Z ind +R1910:1918 Q16_16 Q16_16 clamp_raw def +R1922:1924 Stdlib.ZArith.BinInt <> ::Z_scope:x_'-'_x not +R1921:1921 Q16_16 <> a:8 var +R1925:1925 Q16_16 <> b:9 var +def 1942:1944 Q16_16 neg +R1951:1951 Corelib.Numbers.BinNums <> Z ind +binder 1947:1947 <> a:10 +R1956:1956 Corelib.Numbers.BinNums <> Z ind +R1961:1969 Q16_16 Q16_16 clamp_raw def +R1972:1972 Stdlib.ZArith.BinInt <> ::Z_scope:'-'_x not +R1973:1973 Q16_16 <> a:10 var +def 1990:1992 Q16_16 mul +R2001:2001 Corelib.Numbers.BinNums <> Z ind +binder 1995:1995 <> a:11 +binder 1997:1997 <> b:12 +R2006:2006 Corelib.Numbers.BinNums <> Z ind +R2011:2019 Q16_16 Q16_16 clamp_raw def +R2022:2026 Stdlib.ZArith.BinInt Z div def +R2030:2032 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R2029:2029 Q16_16 <> a:11 var +R2033:2033 Q16_16 <> b:12 var +R2036:2044 Q16_16 Q16_16 q16_scale def +def 2061:2063 Q16_16 div +R2072:2072 Corelib.Numbers.BinNums <> Z ind +binder 2066:2066 <> a:13 +binder 2068:2068 <> b:14 +R2077:2077 Corelib.Numbers.BinNums <> Z ind +R2089:2096 Stdlib.ZArith.BinInt Z eq_dec def +R2098:2098 Q16_16 <> b:14 var +R2117:2125 Q16_16 Q16_16 clamp_raw def +R2128:2132 Stdlib.ZArith.BinInt Z div def +R2136:2138 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not +R2135:2135 Q16_16 <> a:13 var +R2139:2147 Q16_16 Q16_16 q16_scale def +R2150:2150 Q16_16 <> b:14 var +R2107:2110 Q16_16 Q16_16 zero def +prf 2165:2172 Q16_16 add_comm +R2181:2181 Corelib.Numbers.BinNums <> Z ind +binder 2175:2175 <> a:15 +binder 2177:2177 <> b:16 +R2193:2195 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2186:2188 Q16_16 Q16_16 add def +R2190:2190 Q16_16 <> a:15 var +R2192:2192 Q16_16 <> b:16 var +R2196:2198 Q16_16 Q16_16 add def +R2200:2200 Q16_16 <> b:16 var +R2202:2202 Q16_16 <> a:15 var +R2221:2223 Q16_16 Q16_16 add def +R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm +R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm +R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm +prf 2275:2286 Q16_16 add_in_range +R2295:2295 Corelib.Numbers.BinNums <> Z ind +binder 2289:2289 <> a:17 +binder 2291:2291 <> b:18 +R2304:2311 Q16_16 Q16_16 in_range def +R2313:2313 Q16_16 <> a:17 var +binder 2299:2300 <> ha:19 +R2322:2329 Q16_16 Q16_16 in_range def +R2331:2331 Q16_16 <> b:18 var +binder 2317:2318 <> hb:20 +R2346:2353 Q16_16 Q16_16 in_range def +R2357:2359 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R2356:2356 Q16_16 <> a:17 var +R2360:2360 Q16_16 <> b:18 var +binder 2339:2342 <> hsum:21 +R2373:2375 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2366:2368 Q16_16 Q16_16 add def +R2370:2370 Q16_16 <> a:17 var +R2372:2372 Q16_16 <> b:18 var +R2377:2379 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not +R2376:2376 Q16_16 <> a:17 var +R2380:2380 Q16_16 <> b:18 var +R2403:2405 Q16_16 Q16_16 add def +R2416:2431 Q16_16 Q16_16 clamp_idempotent thm +R2416:2431 Q16_16 Q16_16 clamp_idempotent thm +R2416:2431 Q16_16 Q16_16 clamp_idempotent thm +R2416:2431 Q16_16 Q16_16 clamp_idempotent thm +prf 2461:2468 Q16_16 sub_self +R2475:2475 Corelib.Numbers.BinNums <> Z ind +binder 2471:2471 <> a:22 +R2484:2491 Q16_16 Q16_16 in_range def +R2493:2493 Q16_16 <> a:22 var +binder 2479:2480 <> ha:23 +R2505:2507 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2498:2500 Q16_16 Q16_16 sub def +R2502:2502 Q16_16 <> a:22 var +R2504:2504 Q16_16 <> a:22 var +R2508:2511 Q16_16 Q16_16 zero def +R2534:2536 Q16_16 Q16_16 sub def +R2539:2542 Q16_16 Q16_16 zero def +R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm +R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm +R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm +R2575:2590 Q16_16 Q16_16 clamp_idempotent thm +R2600:2607 Q16_16 Q16_16 in_range def +R2617:2627 Q16_16 Q16_16 q16_min_raw def +R2630:2640 Q16_16 Q16_16 q16_max_raw def +R2575:2590 Q16_16 Q16_16 clamp_idempotent thm +R2661:2678 Q16_16 <> le_neg2147483648_0 thm +R2688:2702 Q16_16 <> le_0_2147483647 thm +R2661:2678 Q16_16 <> le_neg2147483648_0 thm +R2688:2702 Q16_16 <> le_0_2147483647 thm +prf 2724:2731 Q16_16 mul_comm +R2740:2740 Corelib.Numbers.BinNums <> Z ind +binder 2734:2734 <> a:24 +binder 2736:2736 <> b:25 +R2752:2754 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2745:2747 Q16_16 Q16_16 mul def +R2749:2749 Q16_16 <> a:24 var +R2751:2751 Q16_16 <> b:25 var +R2755:2757 Q16_16 Q16_16 mul def +R2759:2759 Q16_16 <> b:25 var +R2761:2761 Q16_16 <> a:24 var +R2780:2782 Q16_16 Q16_16 mul def +R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm +R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm +R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm +prf 2834:2846 Q16_16 in_range_zero +R2850:2857 Q16_16 Q16_16 in_range def +R2878:2885 Q16_16 Q16_16 in_range def +R2888:2898 Q16_16 Q16_16 q16_min_raw def +R2901:2911 Q16_16 Q16_16 q16_max_raw def +R2928:2945 Q16_16 <> le_neg2147483648_0 thm +R2955:2969 Q16_16 <> le_0_2147483647 thm +R2928:2945 Q16_16 <> le_neg2147483648_0 thm +R2955:2969 Q16_16 <> le_0_2147483647 thm +prf 2989:3000 Q16_16 in_range_one +R3004:3011 Q16_16 Q16_16 in_range def +R3032:3039 Q16_16 Q16_16 in_range def +R3042:3052 Q16_16 Q16_16 q16_min_raw def +R3055:3065 Q16_16 Q16_16 q16_max_raw def +R3082:3099 Q16_16 <> le_neg2147483648_0 thm +R3109:3123 Q16_16 <> le_0_2147483647 thm +R3082:3099 Q16_16 <> le_neg2147483648_0 thm +R3109:3123 Q16_16 <> le_0_2147483647 thm +R3137:3142 Q16_16 Q16_16 <> mod diff --git a/coq/CoreFormalism/Q16_16.v b/coq/CoreFormalism/Q16_16.v index ee37679b..4459af43 100644 --- a/coq/CoreFormalism/Q16_16.v +++ b/coq/CoreFormalism/Q16_16.v @@ -3,6 +3,10 @@ Require Import ZArith Lia. Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z. Proof. lia. Qed. +Lemma le_0_2147483647 : (0 <= 2147483647)%Z. +Proof. lia. Qed. +Lemma le_neg2147483648_0 : (-2147483648 <= 0)%Z. +Proof. lia. Qed. Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z. Proof. lia. Qed. @@ -70,16 +74,16 @@ Module Q16_16. Proof. unfold sub, zero; rewrite Z.sub_diag. apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw. - split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. + split; [apply le_neg2147483648_0 | apply le_0_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. split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. Qed. + Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed. Theorem in_range_one : in_range 1. - Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_2147483647 | apply le_2147483647_2147483647]. Qed. + Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed. End Q16_16. diff --git a/coq/CoreFormalism/Q16_16.vo b/coq/CoreFormalism/Q16_16.vo new file mode 100644 index 00000000..7acd557a Binary files /dev/null and b/coq/CoreFormalism/Q16_16.vo differ diff --git a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf.lock b/coq/CoreFormalism/Q16_16.vok similarity index 100% rename from rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf.lock rename to coq/CoreFormalism/Q16_16.vok diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx.lock b/coq/CoreFormalism/Q16_16.vos similarity index 100% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx.lock rename to coq/CoreFormalism/Q16_16.vos diff --git a/cpp/avm.hpp b/cpp/avm.hpp new file mode 100644 index 00000000..b004d34d --- /dev/null +++ b/cpp/avm.hpp @@ -0,0 +1,204 @@ +// AVM ISA v1 — C++ Port (Strict Functional Execution) +#pragma once +#include +#include +#include +#include +#include + +namespace avm { + +// ── Constants ──────────────────────────────────────────────────── +constexpr int32_t AVM_CLAMP_MIN = -2147483647; +constexpr int32_t AVM_CLAMP_MAX = 2147483647; +constexpr int32_t AVM_Q0_MIN = -32767; +constexpr int32_t AVM_Q0_MAX = 32767; +constexpr int64_t Q16_SCALE = 65536; +constexpr size_t AVM_MAX_STACK = 1024; + +inline int32_t avm_clamp(int64_t x) { + if (x > AVM_CLAMP_MAX) return AVM_CLAMP_MAX; + if (x < AVM_CLAMP_MIN) return AVM_CLAMP_MIN; + return static_cast(x); +} + +inline int32_t avm_q0_clamp(int64_t x) { + if (x > AVM_Q0_MAX) return AVM_Q0_MAX; + if (x < AVM_Q0_MIN) return AVM_Q0_MIN; + return static_cast(x); +} + +inline int32_t floor_div(int64_t a, int64_t b) { + if (b == 0) throw std::runtime_error("division by zero"); + int64_t q = a / b; + if (a % b != 0 && ((a ^ b) < 0)) q--; + return static_cast(q); +} + +inline bool lt_q16_v6(int32_t a, int32_t b) { + bool sa = a < 0, sb = b < 0; + return (sa != sb) ? sa : (a < b); +} + +// ── Types ────────────────────────────────────────────────────── +enum class Ty : uint8_t { Q0_16, Q16_16, Bool }; +using Val = std::variant; + +struct AnyVal { Ty ty; Val val; }; + +// ── Primitives ──────────────────────────────────────────────── +enum class Prim : uint8_t { + AddSatQ0, SubSatQ0, + AddSatQ16, SubSatQ16, MulSatQ16, DivSatQ16, + LtQ16, EqQ16, And, Or, Not +}; + +inline int prim_arity(Prim p) { + return (p == Prim::Not) ? 1 : 2; +} + +// ── Instructions ────────────────────────────────────────────── +enum class Op : uint8_t { + PushQ16, PushBool, PushQ0, + Pop, Dup, Swap, Load, Store, + Jump, JumpIf, Primitive, Halt +}; + +struct Instr { + Op op; + int32_t arg; + bool arg2; +}; + +// ── Primitive execution ────────────────────────────────────── +inline AnyVal exec_prim(Prim p, const AnyVal& a, const AnyVal& b) { + auto check = [](const AnyVal& v, Ty t) { if (v.ty != t) throw std::runtime_error("type mismatch"); }; + switch (p) { + case Prim::AddSatQ0: + check(a, Ty::Q0_16); check(b, Ty::Q0_16); + return {Ty::Q0_16, avm_q0_clamp(static_cast(std::get(a.val)) + std::get(b.val))}; + case Prim::SubSatQ0: + check(a, Ty::Q0_16); check(b, Ty::Q0_16); + return {Ty::Q0_16, avm_q0_clamp(static_cast(std::get(a.val)) - std::get(b.val))}; + case Prim::AddSatQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Q16_16, avm_clamp(static_cast(std::get(a.val)) + std::get(b.val))}; + case Prim::SubSatQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Q16_16, avm_clamp(static_cast(std::get(a.val)) - std::get(b.val))}; + case Prim::MulSatQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Q16_16, avm_clamp(floor_div(static_cast(std::get(a.val)) * std::get(b.val), Q16_SCALE))}; + case Prim::DivSatQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Q16_16, avm_clamp(floor_div(static_cast(std::get(a.val)) * Q16_SCALE, std::get(b.val)))}; + case Prim::LtQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Bool, lt_q16_v6(std::get(a.val), std::get(b.val))}; + case Prim::EqQ16: + check(a, Ty::Q16_16); check(b, Ty::Q16_16); + return {Ty::Bool, std::get(a.val) == std::get(b.val)}; + case Prim::And: + check(a, Ty::Bool); check(b, Ty::Bool); + return {Ty::Bool, std::get(a.val) && std::get(b.val)}; + case Prim::Or: + check(a, Ty::Bool); check(b, Ty::Bool); + return {Ty::Bool, std::get(a.val) || std::get(b.val)}; + case Prim::Not: + check(a, Ty::Bool); + return {Ty::Bool, !std::get(a.val)}; + } + throw std::runtime_error("unknown prim"); +} + +// ── State ───────────────────────────────────────────────────── +struct State { + int pc = 0; + std::vector stack; + std::vector> locals; + bool halted = false; +}; + +inline State init_state(size_t n_locals = 0) { + return {0, {}, std::vector>(n_locals), false}; +} + +// ── Step ───────────────────────────────────────────────────── +inline std::optional step(const State& s, const std::vector& prog) { + if (s.halted) return std::nullopt; + if (s.pc < 0 || static_cast(s.pc) >= prog.size()) + return State{s.pc, s.stack, s.locals, true}; + + auto instr = prog[s.pc]; + State ns = s; + int npc = s.pc + 1; + + auto growing = (instr.op == Op::PushQ16 || instr.op == Op::PushBool || instr.op == Op::PushQ0 || instr.op == Op::Dup || instr.op == Op::Load); + if (growing && ns.stack.size() >= AVM_MAX_STACK) return std::nullopt; // overflow + + switch (instr.op) { + case Op::PushQ16: ns.stack.push_back({Ty::Q16_16, avm_clamp(instr.arg)}); break; + case Op::PushBool: ns.stack.push_back({Ty::Bool, instr.arg2}); break; + case Op::PushQ0: ns.stack.push_back({Ty::Q0_16, avm_q0_clamp(instr.arg)}); break; + case Op::Pop: + if (ns.stack.empty()) return std::nullopt; + ns.stack.pop_back(); break; + case Op::Dup: + if (ns.stack.empty()) return std::nullopt; + ns.stack.push_back(ns.stack.back()); break; + case Op::Swap: + if (ns.stack.size() < 2) return std::nullopt; + std::swap(ns.stack[ns.stack.size()-1], ns.stack[ns.stack.size()-2]); break; + case Op::Load: { + size_t i = instr.arg; + if (i >= ns.locals.size() || !ns.locals[i].has_value()) return std::nullopt; + ns.stack.push_back(ns.locals[i].value()); break; + } + case Op::Store: { + size_t i = instr.arg; + if (ns.stack.empty() || i >= ns.locals.size()) return std::nullopt; + ns.locals[i] = ns.stack.back(); ns.stack.pop_back(); break; + } + case Op::Jump: + if (instr.arg < 0 || static_cast(instr.arg) >= prog.size()) return std::nullopt; + npc = instr.arg; break; + case Op::JumpIf: { + if (ns.stack.empty()) return std::nullopt; + auto v = ns.stack.back(); ns.stack.pop_back(); + if (v.ty != Ty::Bool) return std::nullopt; + if (std::get(v.val)) { + if (instr.arg < 0 || static_cast(instr.arg) >= prog.size()) return std::nullopt; + npc = instr.arg; + } + break; + } + case Op::Primitive: { + auto p = static_cast(instr.arg); + int arity = prim_arity(p); + if (static_cast(ns.stack.size()) < arity) return std::nullopt; + AnyVal b{Ty::Bool, false}; + if (arity >= 2) { b = ns.stack.back(); ns.stack.pop_back(); } + AnyVal a = ns.stack.back(); ns.stack.pop_back(); + try { ns.stack.push_back(exec_prim(p, a, b)); } + catch (...) { return std::nullopt; } + break; + } + case Op::Halt: ns.halted = true; break; + } + ns.pc = npc; + return ns; +} + +// ── Run (fuel-bounded) ─────────────────────────────────────── +inline std::optional run(const State& init, const std::vector& prog, int fuel = 10000) { + State s = init; + for (int i = 0; i < fuel; i++) { + if (s.halted) return s; + auto next = step(s, prog); + if (!next.has_value()) return std::nullopt; + s = next.value(); + } + return s; +} + +} // namespace avm diff --git a/fortran/avm.f90 b/fortran/avm.f90 new file mode 100644 index 00000000..eff61a07 --- /dev/null +++ b/fortran/avm.f90 @@ -0,0 +1,198 @@ +! AVM ISA v1 — Fortran Port (Strict Functional Execution) +module avm + implicit none + + ! ── Constants ────────────────────────────────────────────── + integer, parameter :: AVM_CLAMP_MIN = -2147483647 + integer, parameter :: AVM_CLAMP_MAX = 2147483647 + integer, parameter :: AVM_Q0_MIN = -32767 + integer, parameter :: AVM_Q0_MAX = 32767 + integer, parameter :: Q16_SCALE = 65536 + integer, parameter :: AVM_MAX_STACK = 1024 + integer, parameter :: AVM_MAX_LOCALS = 256 + + ! ── Types ────────────────────────────────────────────────── + integer, parameter :: TY_Q0 = 0, TY_Q16 = 1, TY_BOOL = 2 + + type :: AnyVal + integer :: ty = TY_Q0 + integer :: i = 0 + logical :: b = .false. + end type AnyVal + + ! ── Instruction encoding ─────────────────────────────────── + integer, parameter :: OP_PUSH_Q16 = 0, OP_PUSH_BOOL = 1, OP_PUSH_Q0 = 2 + integer, parameter :: OP_POP = 3, OP_DUP = 4, OP_SWAP = 5 + integer, parameter :: OP_LOAD = 6, OP_STORE = 7 + integer, parameter :: OP_JUMP = 8, OP_JUMP_IF = 9, OP_PRIM = 10, OP_HALT = 11 + + integer, parameter :: PRIM_ADD_Q0 = 0, PRIM_SUB_Q0 = 1 + integer, parameter :: PRIM_ADD_Q16 = 2, PRIM_SUB_Q16 = 3 + integer, parameter :: PRIM_MUL_Q16 = 4, PRIM_DIV_Q16 = 5 + integer, parameter :: PRIM_LT_Q16 = 6, PRIM_EQ_Q16 = 7 + integer, parameter :: PRIM_AND = 8, PRIM_OR = 9, PRIM_NOT = 10 + + type :: Instr + integer :: op = OP_HALT + integer :: arg = 0 + logical :: arg2 = .false. + end type Instr + + type :: State + integer :: pc = 0 + type(AnyVal) :: stack(AVM_MAX_STACK) + integer :: sp = 0 + type(AnyVal) :: locals(AVM_MAX_LOCALS) + logical :: local_set(AVM_MAX_LOCALS) = .false. + logical :: halted = .false. + end type State + +contains + + ! ── Helpers ──────────────────────────────────────────────── + function avm_clamp(x) result(r) + integer(kind=8), intent(in) :: x + integer :: r + if (x > AVM_CLAMP_MAX) then; r = AVM_CLAMP_MAX + else if (x < AVM_CLAMP_MIN) then; r = AVM_CLAMP_MIN + else; r = int(x); end if + end function avm_clamp + + function avm_q0_clamp(x) result(r) + integer(kind=8), intent(in) :: x + integer :: r + if (x > AVM_Q0_MAX) then; r = AVM_Q0_MAX + else if (x < AVM_Q0_MIN) then; r = AVM_Q0_MIN + else; r = int(x); end if + end function avm_q0_clamp + + function floor_div(a, b) result(r) + integer(kind=8), intent(in) :: a, b + integer :: r + integer(kind=8) :: q + q = a / b + if (mod(a, b) /= 0 .and. ieor(a, b) < 0) q = q - 1 + r = int(q) + end function floor_div + + function lt_q16_v6(a, b) result(r) + integer, intent(in) :: a, b + logical :: r + logical :: sa, sb + sa = a < 0; sb = b < 0 + if (sa .neqv. sb) then; r = sa; else; r = a < b; end if + end function lt_q16_v6 + + ! ── Primitive execution ──────────────────────────────────── + function eval_prim(p, a, b) result(r) + integer, intent(in) :: p + type(AnyVal), intent(in) :: a, b + type(AnyVal) :: r + r%ty = TY_Q0; r%i = 0; r%b = .false. + + if (p == PRIM_ADD_Q0) then + if (a%ty /= TY_Q0 .or. b%ty /= TY_Q0) return + r%ty = TY_Q0; r%i = avm_q0_clamp(int(a%i, 8) + int(b%i, 8)) + else if (p == PRIM_SUB_Q0) then + if (a%ty /= TY_Q0 .or. b%ty /= TY_Q0) return + r%ty = TY_Q0; r%i = avm_q0_clamp(int(a%i, 8) - int(b%i, 8)) + else if (p == PRIM_ADD_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return + r%ty = TY_Q16; r%i = avm_clamp(int(a%i, 8) + int(b%i, 8)) + else if (p == PRIM_SUB_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return + r%ty = TY_Q16; r%i = avm_clamp(int(a%i, 8) - int(b%i, 8)) + else if (p == PRIM_MUL_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return + r%ty = TY_Q16; r%i = avm_clamp(int(floor_div(int(a%i,8)*int(b%i,8), int(Q16_SCALE,8)), 8)) + else if (p == PRIM_DIV_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16 .or. b%i == 0) return + r%ty = TY_Q16; r%i = avm_clamp(int(floor_div(int(a%i,8)*Q16_SCALE, int(b%i,8)), 8)) + else if (p == PRIM_LT_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return + r%ty = TY_BOOL; r%b = lt_q16_v6(a%i, b%i) + else if (p == PRIM_EQ_Q16) then + if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return + r%ty = TY_BOOL; r%b = (a%i == b%i) + else if (p == PRIM_AND) then + if (a%ty /= TY_BOOL .or. b%ty /= TY_BOOL) return + r%ty = TY_BOOL; r%b = a%b .and. b%b + else if (p == PRIM_OR) then + if (a%ty /= TY_BOOL .or. b%ty /= TY_BOOL) return + r%ty = TY_BOOL; r%b = a%b .or. b%b + else if (p == PRIM_NOT) then + if (a%ty /= TY_BOOL) return + r%ty = TY_BOOL; r%b = .not. a%b + end if + end function eval_prim + + ! ── Step ────────────────────────────────────────────────── + function step(s, prog, prog_len) result(err) + type(State), intent(inout) :: s + type(Instr), intent(in) :: prog(*) + integer, intent(in) :: prog_len + integer :: err, npc, arity + type(AnyVal) :: a, b, res + type(Instr) :: instr + + err = 0 + if (s%halted) then; err = -1; return; end if + if (s%pc < 0 .or. s%pc >= prog_len) then; s%halted = .true.; return; end if + + instr = prog(s%pc + 1) + npc = s%pc + 1 + + ! Stack depth check + if (instr%op <= OP_PUSH_Q0 .or. instr%op == OP_DUP .or. instr%op == OP_LOAD) then + if (s%sp >= AVM_MAX_STACK) then; err = -2; return; end if + end if + + if (instr%op == OP_PUSH_Q16) then + s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_Q16; s%stack(s%sp)%i = avm_clamp(int(instr%arg, 8)) + else if (instr%op == OP_PUSH_BOOL) then + s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_BOOL; s%stack(s%sp)%b = instr%arg2 + else if (instr%op == OP_PUSH_Q0) then + s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_Q0; s%stack(s%sp)%i = avm_q0_clamp(int(instr%arg, 8)) + else if (instr%op == OP_POP) then + if (s%sp <= 0) then; err = -3; return; end if; s%sp = s%sp - 1 + else if (instr%op == OP_DUP) then + if (s%sp <= 0) then; err = -3; return; end if + s%sp = s%sp + 1; s%stack(s%sp) = s%stack(s%sp - 1) + else if (instr%op == OP_SWAP) then + if (s%sp < 2) then; err = -4; return; end if + a = s%stack(s%sp); s%stack(s%sp) = s%stack(s%sp-1); s%stack(s%sp-1) = a + else if (instr%op == OP_LOAD) then + if (instr%arg < 0 .or. instr%arg >= AVM_MAX_LOCALS .or. .not. s%local_set(instr%arg+1)) then + err = -5; return + end if + s%sp = s%sp + 1; s%stack(s%sp) = s%locals(instr%arg+1) + else if (instr%op == OP_STORE) then + if (s%sp <= 0) then; err = -3; return; end if + if (instr%arg < 0 .or. instr%arg >= AVM_MAX_LOCALS) then; err = -5; return; end if + s%locals(instr%arg+1) = s%stack(s%sp); s%local_set(instr%arg+1) = .true. + s%sp = s%sp - 1 + else if (instr%op == OP_JUMP) then + if (instr%arg < 0 .or. instr%arg >= prog_len) then; err = -6; return; end if + npc = instr%arg + else if (instr%op == OP_JUMP_IF) then + if (s%sp <= 0) then; err = -3; return; end if + a = s%stack(s%sp); s%sp = s%sp - 1 + if (a%ty /= TY_BOOL) then; err = -7; return; end if + if (a%b) then + if (instr%arg < 0 .or. instr%arg >= prog_len) then; err = -6; return; end if + npc = instr%arg + end if + else if (instr%op == OP_PRIM) then + arity = 2; if (instr%arg == PRIM_NOT) arity = 1 + if (s%sp < arity) then; err = -4; return; end if + if (arity >= 2) then; b = s%stack(s%sp); s%sp = s%sp - 1; end if + a = s%stack(s%sp); s%sp = s%sp - 1 + res = eval_prim(instr%arg, a, b) + s%sp = s%sp + 1; s%stack(s%sp) = res + else if (instr%op == OP_HALT) then + s%halted = .true. + end if + s%pc = npc + end function step + +end module avm diff --git a/go/avm.go b/go/avm.go new file mode 100644 index 00000000..2d5b95de --- /dev/null +++ b/go/avm.go @@ -0,0 +1,225 @@ +// AVM ISA v1 — Go Port (Strict Functional Execution) +package avm + +import "errors" + +// ── Constants ──────────────────────────────────────────────────── +const ( + AVMClampMin = -2147483647 + AVMClampMax = 2147483647 + AVMQ0Min = -32767 + AVMQ0Max = 32767 + Q16Scale = 65536 + AVMMaxStack = 1024 +) + +func avmClamp(x int64) int32 { + if x > AVMClampMax { return AVMClampMax } + if x < AVMClampMin { return AVMClampMin } + return int32(x) +} + +func avmQ0Clamp(x int64) int32 { + if x > AVMQ0Max { return AVMQ0Max } + if x < AVMQ0Min { return AVMQ0Min } + return int32(x) +} + +func floorDiv(a, b int64) int32 { + if b == 0 { panic("division by zero") } + q := a / b + r := a % b + if r != 0 && ((a ^ b) < 0) { q-- } + return int32(q) +} + +func ltQ16V6(a, b int32) bool { + sa, sb := a < 0, b < 0 + if sa != sb { return sa } + return a < b +} + +// ── Types ────────────────────────────────────────────────────── +type Ty uint8 +const ( + Q0_16 Ty = 0 + Q16_16 Ty = 1 + Bool Ty = 2 +) + +type Val struct { + Ty Ty + Q int32 + Bval bool +} + +// ── Primitives ──────────────────────────────────────────────── +type Prim uint8 +const ( + AddSatQ0 Prim = iota; SubSatQ0; AddSatQ16; SubSatQ16 + MulSatQ16; DivSatQ16; LtQ16; EqQ16 + And; Or; Not +) + +func primArity(p Prim) int { + if p == Not { return 1 } + return 2 +} + +// ── Instructions ────────────────────────────────────────────── +type Op uint8 +const ( + PushQ16 Op = iota; PushBool; PushQ0; Pop; Dup; Swap + Load; Store; Jump; JumpIf; Primitive; Halt +) + +type Instr struct { + Op Op + Arg int32 + Arg2 bool +} + +// ── Primitive execution ────────────────────────────────────── +func execPrim(p Prim, a, b Val) (Val, error) { + check := func(v Val, t Ty) error { + if v.Ty != t { return errors.New("type mismatch") } + return nil + } + switch p { + case AddSatQ0: + if err := check(a, Q0_16); err != nil { return Val{}, err } + if err := check(b, Q0_16); err != nil { return Val{}, err } + return Val{Ty: Q0_16, Q: avmQ0Clamp(int64(a.Q) + int64(b.Q))}, nil + case SubSatQ0: + if err := check(a, Q0_16); err != nil { return Val{}, err } + if err := check(b, Q0_16); err != nil { return Val{}, err } + return Val{Ty: Q0_16, Q: avmQ0Clamp(int64(a.Q) - int64(b.Q))}, nil + case AddSatQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Q16_16, Q: avmClamp(int64(a.Q) + int64(b.Q))}, nil + case SubSatQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Q16_16, Q: avmClamp(int64(a.Q) - int64(b.Q))}, nil + case MulSatQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Q16_16, Q: avmClamp(floorDiv(int64(a.Q)*int64(b.Q), Q16Scale))}, nil + case DivSatQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Q16_16, Q: avmClamp(floorDiv(int64(a.Q)*Q16Scale, int64(b.Q)))}, nil + case LtQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Bool, Bval: ltQ16V6(a.Q, b.Q)}, nil + case EqQ16: + if err := check(a, Q16_16); err != nil { return Val{}, err } + if err := check(b, Q16_16); err != nil { return Val{}, err } + return Val{Ty: Bool, Bval: a.Q == b.Q}, nil + case And: + if err := check(a, Bool); err != nil { return Val{}, err } + if err := check(b, Bool); err != nil { return Val{}, err } + return Val{Ty: Bool, Bval: a.Bval && b.Bval}, nil + case Or: + if err := check(a, Bool); err != nil { return Val{}, err } + if err := check(b, Bool); err != nil { return Val{}, err } + return Val{Ty: Bool, Bval: a.Bval || b.Bval}, nil + case Not: + if err := check(a, Bool); err != nil { return Val{}, err } + return Val{Ty: Bool, Bval: !a.Bval}, nil + } + return Val{}, errors.New("unknown prim") +} + +// ── State ───────────────────────────────────────────────────── +type State struct { + Pc int + Stack []Val + Locals []*Val + Halted bool +} + +func NewState(nLocals int) State { + return State{Pc: 0, Stack: []Val{}, Locals: make([]*Val, nLocals), Halted: false} +} + +// ── Step ───────────────────────────────────────────────────── +func Step(s State, prog []Instr) (*State, error) { + if s.Halted { return nil, errors.New("halted") } + if s.Pc < 0 || s.Pc >= len(prog) { + return &State{Pc: s.Pc, Stack: s.Stack, Locals: s.Locals, Halted: true}, nil + } + + instr := prog[s.Pc] + stack := s.Stack + npc := s.Pc + 1 + + growing := instr.Op == PushQ16 || instr.Op == PushBool || instr.Op == PushQ0 || instr.Op == Dup || instr.Op == Load + if growing && len(stack) >= AVMMaxStack { return nil, errors.New("stack overflow") } + + switch instr.Op { + case PushQ16: + stack = append(stack, Val{Ty: Q16_16, Q: avmClamp(instr.Arg)}) + case PushBool: + stack = append(stack, Val{Ty: Bool, Bval: instr.Arg2}) + case PushQ0: + stack = append(stack, Val{Ty: Q0_16, Q: avmQ0Clamp(instr.Arg)}) + case Pop: + if len(stack) == 0 { return nil, errors.New("empty stack") } + stack = stack[:len(stack)-1] + case Dup: + if len(stack) == 0 { return nil, errors.New("empty stack") } + stack = append(stack, stack[len(stack)-1]) + case Swap: + if len(stack) < 2 { return nil, errors.New("stack underflow") } + stack[len(stack)-1], stack[len(stack)-2] = stack[len(stack)-2], stack[len(stack)-1] + case Load: + i := int(instr.Arg) + if i >= len(s.Locals) || s.Locals[i] == nil { return nil, errors.New("missing local") } + stack = append(stack, *s.Locals[i]) + case Store: + if len(stack) == 0 { return nil, errors.New("empty stack") } + i := int(instr.Arg) + if i >= len(s.Locals) { return nil, errors.New("missing local") } + s.Locals[i] = &stack[len(stack)-1] + stack = stack[:len(stack)-1] + case Jump: + if instr.Arg < 0 || int(instr.Arg) >= len(prog) { return nil, errors.New("jump OOB") } + npc = int(instr.Arg) + case JumpIf: + if len(stack) == 0 { return nil, errors.New("empty stack") } + v := stack[len(stack)-1]; stack = stack[:len(stack)-1] + if v.Ty != Bool { return nil, errors.New("type mismatch") } + if v.Bval { + if instr.Arg < 0 || int(instr.Arg) >= len(prog) { return nil, errors.New("jump OOB") } + npc = int(instr.Arg) + } + case Primitive: + p := Prim(instr.Arg) + arity := primArity(p) + if len(stack) < arity { return nil, errors.New("stack underflow") } + var b Val + if arity >= 2 { b = stack[len(stack)-1]; stack = stack[:len(stack)-1] } + a := stack[len(stack)-1]; stack = stack[:len(stack)-1] + r, err := execPrim(p, a, b) + if err != nil { return nil, err } + stack = append(stack, r) + case Halt: + s.Halted = true + } + return &State{Pc: npc, Stack: stack, Locals: s.Locals, Halted: s.Halted}, nil +} + +// ── Run (fuel-bounded) ─────────────────────────────────────── +func Run(init State, prog []Instr, fuel int) (*State, error) { + s := init + for i := 0; i < fuel; i++ { + if s.Halted { return &s, nil } + next, err := Step(s, prog) + if err != nil { return nil, err } + s = *next + } + return &s, nil +} diff --git a/octave/avm.m b/octave/avm.m new file mode 100644 index 00000000..505d97ed --- /dev/null +++ b/octave/avm.m @@ -0,0 +1,170 @@ +% 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 = struct('pc', int32(0), 'stack', {}, 'locals', cell(n_locals, 1), '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 diff --git a/python/avm.py b/python/avm.py new file mode 100644 index 00000000..2749b3aa --- /dev/null +++ b/python/avm.py @@ -0,0 +1,209 @@ +""" +AVM ISA v1 — Python Port (Strict Functional Execution) +Mirrors formal/SilverSight/AVMIsa/Step.lean +""" +from __future__ import annotations +from dataclasses import dataclass, field +from enum import IntEnum, auto +from typing import Union, Optional +import sys + +from q16_canonical import Q16_SCALE, float_to_q16, q16_to_float + +# ── Constants ──────────────────────────────────────────────────────── +AVM_CLAMP_MIN = -2147483647 +AVM_CLAMP_MAX = 2147483647 +AVM_Q0_MIN = -32767 +AVM_Q0_MAX = 32767 +AVM_MAX_STACK = 1024 + +def avm_clamp(x: int) -> int: + return max(AVM_CLAMP_MIN, min(AVM_CLAMP_MAX, x)) + +def avm_q0_clamp(x: int) -> int: + return max(AVM_Q0_MIN, min(AVM_Q0_MAX, x)) + +def floor_div(a: int, b: int) -> int: + """Floor division matching Lean Int.ediv.""" + if b == 0: + raise ValueError("division by zero") + return -((-a) // b) if (a < 0) != (b < 0) and a % b != 0 else a // b + +def lt_q16_v6(a: int, b: int) -> bool: + sa = a < 0 + sb = b < 0 + return sa if sa != sb else a < b + +# ── Types ──────────────────────────────────────────────────────────── +class AvmTy(IntEnum): + Q0_16 = 0 + Q16_16 = 1 + BOOL = 2 + +# ── Values ─────────────────────────────────────────────────────────── +@dataclass +class AnyVal: + ty: AvmTy + val: Union[int, bool] + + @staticmethod + def q16(x: int) -> 'AnyVal': + return AnyVal(AvmTy.Q16_16, avm_clamp(x)) + @staticmethod + def q0(x: int) -> 'AnyVal': + return AnyVal(AvmTy.Q0_16, avm_q0_clamp(x)) + @staticmethod + def b(x: bool) -> 'AnyVal': + return AnyVal(AvmTy.BOOL, x) + +# ── Instructions ───────────────────────────────────────────────────── +class Prim(IntEnum): + ADD_SAT_Q0 = 0 + SUB_SAT_Q0 = 1 + ADD_SAT_Q16 = 2 + SUB_SAT_Q16 = 3 + MUL_SAT_Q16 = 4 + DIV_SAT_Q16 = 5 + LT_Q16 = 6 + EQ_Q16 = 7 + AND = 8 + OR = 9 + NOT = 10 + + @property + def arity(self) -> int: + return 1 if self == Prim.NOT else 2 + +class Instr: + PUSH_Q16, PUSH_BOOL, PUSH_Q0, POP, DUP, SWAP, LOAD, STORE, JUMP, JUMP_IF, PRIM, HALT = range(12) + +# ── Primitive execution ────────────────────────────────────────────── +def eval_prim(p: Prim, a: AnyVal, b: Optional[AnyVal] = None) -> AnyVal: + if p == Prim.ADD_SAT_Q0: + assert a.ty == b.ty == AvmTy.Q0_16 + return AnyVal.q0(a.val + b.val) + elif p == Prim.SUB_SAT_Q0: + assert a.ty == b.ty == AvmTy.Q0_16 + return AnyVal.q0(a.val - b.val) + elif p == Prim.ADD_SAT_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + return AnyVal.q16(a.val + b.val) + elif p == Prim.SUB_SAT_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + return AnyVal.q16(a.val - b.val) + elif p == Prim.MUL_SAT_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + return AnyVal.q16(floor_div(a.val * b.val, Q16_SCALE)) + elif p == Prim.DIV_SAT_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + if b.val == 0: + raise ValueError("division by zero") + return AnyVal.q16(floor_div(a.val * Q16_SCALE, b.val)) + elif p == Prim.LT_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + return AnyVal.b(lt_q16_v6(a.val, b.val)) + elif p == Prim.EQ_Q16: + assert a.ty == b.ty == AvmTy.Q16_16 + return AnyVal.b(a.val == b.val) + elif p == Prim.AND: + assert a.ty == b.ty == AvmTy.BOOL + return AnyVal.b(a.val and b.val) + elif p == Prim.OR: + assert a.ty == b.ty == AvmTy.BOOL + return AnyVal.b(a.val or b.val) + elif p == Prim.NOT: + assert a.ty == AvmTy.BOOL + return AnyVal.b(not a.val) + +# ── Errors ─────────────────────────────────────────────────────────── +class StepError(Exception): + def __init__(self, kind: str): + self.kind = kind + +# ── State ──────────────────────────────────────────────────────────── +@dataclass +class State: + pc: int = 0 + stack: list = field(default_factory=list) + locals: list = field(default_factory=list) + halted: bool = False + + @staticmethod + def new(n_locals: int = 0): + return State(pc=0, stack=[], locals=[None] * n_locals, halted=False) + +# ── Step ───────────────────────────────────────────────────────────── +def step(s: State, prog: list) -> State: + if s.halted: + raise StepError("halted") + if s.pc < 0 or s.pc >= len(prog): + return State(pc=s.pc, stack=list(s.stack), locals=list(s.locals), halted=True) + + instr = prog[s.pc] + stack = list(s.stack) + pc = s.pc + 1 + halted = False + + GROW_OPS = {Instr.PUSH_Q16, Instr.PUSH_BOOL, Instr.PUSH_Q0, Instr.DUP, Instr.LOAD} + if instr[0] in GROW_OPS and len(stack) >= AVM_MAX_STACK: + raise StepError("stack_overflow") + + op = instr[0] + arg = instr[1] + arg2 = instr[2] if len(instr) > 2 else None + + if op == Instr.PUSH_Q16: + stack.append(AnyVal.q16(arg)) + elif op == Instr.PUSH_BOOL: + stack.append(AnyVal.b(arg2)) + elif op == Instr.PUSH_Q0: + stack.append(AnyVal.q0(arg)) + elif op == Instr.POP: + if not stack: raise StepError("empty_stack") + stack.pop() + elif op == Instr.DUP: + if not stack: raise StepError("empty_stack") + stack.append(stack[-1]) + elif op == Instr.SWAP: + if len(stack) < 2: raise StepError("stack_underflow") + stack[-1], stack[-2] = stack[-2], stack[-1] + elif op == Instr.LOAD: + if arg >= len(s.locals) or s.locals[arg] is None: + raise StepError("missing_local") + stack.append(s.locals[arg]) + elif op == Instr.STORE: + if not stack: raise StepError("empty_stack") + if arg >= len(s.locals): raise StepError("missing_local") + s.locals[arg] = stack.pop() + elif op == Instr.JUMP: + if arg < 0 or arg >= len(prog): raise StepError("jump_out_of_bounds") + pc = arg + elif op == Instr.JUMP_IF: + if not stack: raise StepError("empty_stack") + cond = stack.pop() + if cond.ty != AvmTy.BOOL: raise StepError("type_mismatch") + if cond.val: + if arg < 0 or arg >= len(prog): raise StepError("jump_out_of_bounds") + pc = arg + elif op == Instr.PRIM: + p = Prim(arg) + arity = p.arity + if len(stack) < arity: raise StepError("stack_underflow") + b = stack.pop() if arity >= 2 else None + a = stack.pop() + stack.append(eval_prim(p, a, b)) + elif op == Instr.HALT: + halted = True + else: + raise StepError("unknown_instr") + + return State(pc=pc, stack=stack, locals=list(s.locals), halted=halted) + +# ── Run (fuel-bounded) ────────────────────────────────────────────── +def run(initial: State, prog: list, fuel: int = 10000) -> State: + s = initial + for _ in range(fuel): + if s.halted: + return s + s = step(s, prog) + return s diff --git a/rust/src/avm/mod.rs b/rust/src/avm/mod.rs index 55ad1240..2db92d82 100644 --- a/rust/src/avm/mod.rs +++ b/rust/src/avm/mod.rs @@ -136,12 +136,12 @@ fn lt_q16_v6(a: i32, b: i32) -> bool { } // Q0_16 binary (symmetric clamp) (Prim::AddSatQ0, AvmVal::Q0_16(x), Some(AvmVal::Q0_16(y))) => { - let r = (x as i64) + (*y as i64); + let r = (*x as i64) + (*y as i64); Ok(AvmVal::Q0_16(if r > AVM_Q0_MAX as i64 { AVM_Q0_MAX } else if r < AVM_Q0_MIN as i64 { AVM_Q0_MIN } else { r as i32 })) } (Prim::SubSatQ0, AvmVal::Q0_16(x), Some(AvmVal::Q0_16(y))) => { - let r = (x as i64) - (*y as i64); + let r = (*x as i64) - (*y as i64); Ok(AvmVal::Q0_16(if r > AVM_Q0_MAX as i64 { AVM_Q0_MAX } else if r < AVM_Q0_MIN as i64 { AVM_Q0_MIN } else { r as i32 })) } diff --git a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight index 58db3721..a5391c02 100644 Binary files a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight and b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight differ diff --git a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight index 31361d8b..5bd85afc 100644 --- a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight +++ b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight @@ -1,11 +1,12 @@ {"$message_type":"diagnostic","message":"unused imports: `max` and `min`","code":{"code":"unused_imports","explanation":null},"level":"warning","spans":[{"file_name":"src/q16/mod.rs","byte_start":553,"byte_end":556,"line_start":14,"line_end":14,"column_start":16,"column_end":19,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":16,"highlight_end":19}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null},{"file_name":"src/q16/mod.rs","byte_start":558,"byte_end":561,"line_start":14,"line_end":14,"column_start":21,"column_end":24,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":21,"highlight_end":24}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(unused_imports)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"remove the whole `use` item","code":null,"level":"help","spans":[{"file_name":"src/q16/mod.rs","byte_start":538,"byte_end":564,"line_start":14,"line_end":15,"column_start":1,"column_end":1,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":1,"highlight_end":26},{"text":"","highlight_start":1,"highlight_end":1}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unused imports: `max` and `min`\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/q16/mod.rs:14:16\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m14\u001b[0m \u001b[1m\u001b[94m|\u001b[0m use std::cmp::{max, min};\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(unused_imports)]` (part of `#[warn(unused)]`) on by default\n\n"} {"$message_type":"diagnostic","message":"unused import: `crate::q16::*`","code":{"code":"unused_imports","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":291,"byte_end":304,"line_start":10,"line_end":10,"column_start":5,"column_end":18,"is_primary":true,"text":[{"text":"use crate::q16::*;","highlight_start":5,"highlight_end":18}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"remove the whole `use` item","code":null,"level":"help","spans":[{"file_name":"src/pist/mod.rs","byte_start":287,"byte_end":306,"line_start":10,"line_end":11,"column_start":1,"column_end":1,"is_primary":true,"text":[{"text":"use crate::q16::*;","highlight_start":1,"highlight_end":19},{"text":"","highlight_start":1,"highlight_end":1}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unused import: `crate::q16::*`\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:10:5\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m10\u001b[0m \u001b[1m\u001b[94m|\u001b[0m use crate::q16::*;\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^^^^^\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"unnecessary parentheses around closure body","code":{"code":"unused_parens","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":2547,"byte_end":2548,"line_start":80,"line_end":80,"column_start":42,"column_end":43,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"remove these parentheses","code":null,"level":"help","spans":[{"file_name":"src/pist/mod.rs","byte_start":2547,"byte_end":2548,"line_start":80,"line_end":80,"column_start":42,"column_end":43,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unnecessary parentheses around closure body\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:80:42\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[1m\u001b[94m|\u001b[0m let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33m^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default\n\u001b[1m\u001b[96mhelp\u001b[0m: remove these parentheses\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[91m- \u001b[0m let mut v: Vec = (0..n).map(|i| \u001b[91m(\u001b[0mi as f64 + 1.0\u001b[91m)\u001b[0m).collect();\n\u001b[1m\u001b[94m80\u001b[0m \u001b[92m+ \u001b[0m let mut v: Vec = (0..n).map(|i| i as f64 + 1.0).collect();\n \u001b[1m\u001b[94m|\u001b[0m\n\n"} -{"$message_type":"diagnostic","message":"function `build_ata` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":1624,"byte_end":1633,"line_start":55,"line_end":55,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn build_ata(mat: &IntMat, n: usize) -> IntMat {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `build_ata` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:55:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m55\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn build_ata(mat: &IntMat, n: usize) -> IntMat {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default\n\n"} +{"$message_type":"diagnostic","message":"function `floor_div` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/avm/mod.rs","byte_start":1008,"byte_end":1017,"line_start":24,"line_end":24,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn floor_div(a: i32, b: i32) -> i32 {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `floor_div` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/avm/mod.rs:24:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m24\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn floor_div(a: i32, b: i32) -> i32 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default\n\n"} +{"$message_type":"diagnostic","message":"function `build_ata` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":1624,"byte_end":1633,"line_start":55,"line_end":55,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn build_ata(mat: &IntMat, n: usize) -> IntMat {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `build_ata` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:55:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m55\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn build_ata(mat: &IntMat, n: usize) -> IntMat {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:53:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m53\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn F(s: &str) -> [f64; 8] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `f`\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default\n\n"} {"$message_type":"diagnostic","message":"function `Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:94:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m94\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn Phi(s: &str) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"d_f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:103:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m103\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `d_f`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":"d_phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:110:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m110\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `d_phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `C` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"c","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `C` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:122:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m122\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn C(phi: &[f64; 14]) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `c`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `test_F_verified` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":8947,"byte_end":8962,"line_start":262,"line_end":262,"column_start":8,"column_end":23,"is_primary":true,"text":[{"text":" fn test_F_verified() {","highlight_start":8,"highlight_end":23}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":8947,"byte_end":8962,"line_start":262,"line_end":262,"column_start":8,"column_end":23,"is_primary":true,"text":[{"text":" fn test_F_verified() {","highlight_start":8,"highlight_end":23}],"label":null,"suggested_replacement":"test_f_verified","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `test_F_verified` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:262:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m262\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn test_F_verified() {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^^^^^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `test_f_verified`\u001b[0m\n\n"} -{"$message_type":"diagnostic","message":"10 warnings emitted","code":null,"level":"warning","spans":[],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: 10 warnings emitted\u001b[0m\n\n"} +{"$message_type":"diagnostic","message":"11 warnings emitted","code":null,"level":"warning","spans":[],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: 11 warnings emitted\u001b[0m\n\n"} diff --git a/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/dep-lib-silversight b/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/dep-lib-silversight index 3e1c99ad..d00a530c 100644 Binary files a/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/dep-lib-silversight and b/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/dep-lib-silversight differ diff --git a/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/output-lib-silversight b/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/output-lib-silversight index 71c23355..5ab2291b 100644 --- a/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/output-lib-silversight +++ b/rust/target/debug/.fingerprint/silversight-84f93a17283a98b6/output-lib-silversight @@ -1,7 +1,11 @@ {"$message_type":"diagnostic","message":"unused imports: `max` and `min`","code":{"code":"unused_imports","explanation":null},"level":"warning","spans":[{"file_name":"src/q16/mod.rs","byte_start":553,"byte_end":556,"line_start":14,"line_end":14,"column_start":16,"column_end":19,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":16,"highlight_end":19}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null},{"file_name":"src/q16/mod.rs","byte_start":558,"byte_end":561,"line_start":14,"line_end":14,"column_start":21,"column_end":24,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":21,"highlight_end":24}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(unused_imports)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"remove the whole `use` item","code":null,"level":"help","spans":[{"file_name":"src/q16/mod.rs","byte_start":538,"byte_end":564,"line_start":14,"line_end":15,"column_start":1,"column_end":1,"is_primary":true,"text":[{"text":"use std::cmp::{max, min};","highlight_start":1,"highlight_end":26},{"text":"","highlight_start":1,"highlight_end":1}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unused imports: `max` and `min`\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/q16/mod.rs:14:16\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m14\u001b[0m \u001b[1m\u001b[94m|\u001b[0m use std::cmp::{max, min};\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(unused_imports)]` (part of `#[warn(unused)]`) on by default\n\n"} +{"$message_type":"diagnostic","message":"unused import: `crate::q16::*`","code":{"code":"unused_imports","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":291,"byte_end":304,"line_start":10,"line_end":10,"column_start":5,"column_end":18,"is_primary":true,"text":[{"text":"use crate::q16::*;","highlight_start":5,"highlight_end":18}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"remove the whole `use` item","code":null,"level":"help","spans":[{"file_name":"src/pist/mod.rs","byte_start":287,"byte_end":306,"line_start":10,"line_end":11,"column_start":1,"column_end":1,"is_primary":true,"text":[{"text":"use crate::q16::*;","highlight_start":1,"highlight_end":19},{"text":"","highlight_start":1,"highlight_end":1}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unused import: `crate::q16::*`\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:10:5\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m10\u001b[0m \u001b[1m\u001b[94m|\u001b[0m use crate::q16::*;\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^^^^^\u001b[0m\n\n"} +{"$message_type":"diagnostic","message":"unnecessary parentheses around closure body","code":{"code":"unused_parens","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":2547,"byte_end":2548,"line_start":80,"line_end":80,"column_start":42,"column_end":43,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"remove these parentheses","code":null,"level":"help","spans":[{"file_name":"src/pist/mod.rs","byte_start":2547,"byte_end":2548,"line_start":80,"line_end":80,"column_start":42,"column_end":43,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unnecessary parentheses around closure body\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:80:42\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[1m\u001b[94m|\u001b[0m let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33m^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default\n\u001b[1m\u001b[96mhelp\u001b[0m: remove these parentheses\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[91m- \u001b[0m let mut v: Vec = (0..n).map(|i| \u001b[91m(\u001b[0mi as f64 + 1.0\u001b[91m)\u001b[0m).collect();\n\u001b[1m\u001b[94m80\u001b[0m \u001b[92m+ \u001b[0m let mut v: Vec = (0..n).map(|i| i as f64 + 1.0).collect();\n \u001b[1m\u001b[94m|\u001b[0m\n\n"} +{"$message_type":"diagnostic","message":"function `floor_div` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/avm/mod.rs","byte_start":1008,"byte_end":1017,"line_start":24,"line_end":24,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn floor_div(a: i32, b: i32) -> i32 {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `floor_div` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/avm/mod.rs:24:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m24\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn floor_div(a: i32, b: i32) -> i32 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default\n\n"} +{"$message_type":"diagnostic","message":"function `build_ata` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":1624,"byte_end":1633,"line_start":55,"line_end":55,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn build_ata(mat: &IntMat, n: usize) -> IntMat {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `build_ata` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:55:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m55\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn build_ata(mat: &IntMat, n: usize) -> IntMat {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:53:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m53\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn F(s: &str) -> [f64; 8] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `f`\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default\n\n"} {"$message_type":"diagnostic","message":"function `Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:94:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m94\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn Phi(s: &str) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"d_f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:103:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m103\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `d_f`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":"d_phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:110:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m110\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `d_phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `C` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"c","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `C` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:122:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m122\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn C(phi: &[f64; 14]) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `c`\u001b[0m\n\n"} -{"$message_type":"diagnostic","message":"6 warnings emitted","code":null,"level":"warning","spans":[],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: 6 warnings emitted\u001b[0m\n\n"} +{"$message_type":"diagnostic","message":"10 warnings emitted","code":null,"level":"warning","spans":[],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: 10 warnings emitted\u001b[0m\n\n"} diff --git a/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib b/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib index b444a710..8e677d09 100644 Binary files a/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib and b/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib differ diff --git a/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta b/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta index 9eeb3de9..2bbe3742 100644 Binary files a/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta and b/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta differ diff --git a/rust/target/debug/deps/nuvmap_integration-018a05e077788a7d b/rust/target/debug/deps/nuvmap_integration-018a05e077788a7d index 3dcfe6bf..d5531048 100755 Binary files a/rust/target/debug/deps/nuvmap_integration-018a05e077788a7d and b/rust/target/debug/deps/nuvmap_integration-018a05e077788a7d differ diff --git a/rust/target/debug/deps/silversight-0091d08d533221a7 b/rust/target/debug/deps/silversight-0091d08d533221a7 index 734b3a09..9520c8f4 100755 Binary files a/rust/target/debug/deps/silversight-0091d08d533221a7 and b/rust/target/debug/deps/silversight-0091d08d533221a7 differ diff --git a/rust/target/debug/deps/silversight-84f93a17283a98b6.d b/rust/target/debug/deps/silversight-84f93a17283a98b6.d index 0f0fb5fd..72cd4bcd 100644 --- a/rust/target/debug/deps/silversight-84f93a17283a98b6.d +++ b/rust/target/debug/deps/silversight-84f93a17283a98b6.d @@ -1,11 +1,12 @@ -/home/allaun/SilverSight/rust/target/debug/deps/silversight-84f93a17283a98b6.d: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs +/home/allaun/SilverSight/rust/target/debug/deps/silversight-84f93a17283a98b6.d: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs src/pist/mod.rs -/home/allaun/SilverSight/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs +/home/allaun/SilverSight/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rlib: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs src/pist/mod.rs -/home/allaun/SilverSight/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs +/home/allaun/SilverSight/rust/target/debug/deps/libsilversight-84f93a17283a98b6.rmeta: src/lib.rs src/q16/mod.rs src/nuvmap/mod.rs src/silversight/mod.rs src/avm/mod.rs src/pist/mod.rs src/lib.rs: src/q16/mod.rs: src/nuvmap/mod.rs: src/silversight/mod.rs: src/avm/mod.rs: +src/pist/mod.rs: diff --git a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/dep-graph.bin b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/dep-graph.bin deleted file mode 100644 index 2ae10337..00000000 Binary files a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/dep-graph.bin and /dev/null differ diff --git a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/dep-graph.bin b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/dep-graph.bin new file mode 100644 index 00000000..c3407a40 Binary files /dev/null and b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/dep-graph.bin differ diff --git a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/query-cache.bin b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/query-cache.bin similarity index 58% rename from rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/query-cache.bin rename to rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/query-cache.bin index f02d0d0a..bc779f0f 100644 Binary files a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/query-cache.bin and b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/query-cache.bin differ diff --git a/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/work-products.bin b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/work-products.bin similarity index 100% rename from rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyxrwm77y-1qtfovf-7lkovhici2lbkkpz16o5m1bid/work-products.bin rename to rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6-bt72sk6uc8ylyh4bwqt8cmpw9/work-products.bin diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz.lock b/rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6.lock similarity index 100% rename from rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz.lock rename to rust/target/debug/incremental/nuvmap_integration-2kb1deze146qv/s-hjyy8t0h8f-1128yd6.lock diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin deleted file mode 100644 index 026908b3..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin deleted file mode 100644 index 59136309..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/dep-graph.bin new file mode 100644 index 00000000..8fdcda92 Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/dep-graph.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/query-cache.bin new file mode 100644 index 00000000..b9ad950d Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/query-cache.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/work-products.bin similarity index 86% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin rename to rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/work-products.bin index 39c09b47..d6bdeb47 100644 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb-bjrkggecxdmrtm0ugf8rimpwl/work-products.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb.lock b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyy8swzi8-1mjjuxb.lock new file mode 100644 index 00000000..e69de29b diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/dep-graph.bin b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/dep-graph.bin deleted file mode 100644 index 72185026..00000000 Binary files a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/dep-graph.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/metadata.rmeta b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/metadata.rmeta deleted file mode 100644 index a8e99f16..00000000 Binary files a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/metadata.rmeta and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/query-cache.bin b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/query-cache.bin deleted file mode 100644 index 36b2662c..00000000 Binary files a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/query-cache.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/dep-graph.bin b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/dep-graph.bin new file mode 100644 index 00000000..481935bd Binary files /dev/null and b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/dep-graph.bin differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/metadata.rmeta b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/metadata.rmeta new file mode 100644 index 00000000..2bbe3742 Binary files /dev/null and b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/metadata.rmeta differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/query-cache.bin b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/query-cache.bin new file mode 100644 index 00000000..ba8215cb Binary files /dev/null and b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/query-cache.bin differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/work-products.bin b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/work-products.bin similarity index 60% rename from rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/work-products.bin rename to rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/work-products.bin index 6f39b58c..604fec94 100644 Binary files a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyxrwjr3t-1753zgz-81sj5frb52l3juiw1vfwyzmov/work-products.bin and b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia-58n8nmg5v6vln385b76ag5mtj/work-products.bin differ diff --git a/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia.lock b/rust/target/debug/incremental/silversight-2soli35ikbvf4/s-hjyy8swzi8-0m0g2ia.lock new file mode 100644 index 00000000..e69de29b diff --git a/scala/avm.scala b/scala/avm.scala new file mode 100644 index 00000000..c80ac829 --- /dev/null +++ b/scala/avm.scala @@ -0,0 +1,135 @@ +// AVM ISA v1 — Scala Port (Strict Functional Execution) +package silversight.avm + +object AVM { + // ── Constants ────────────────────────────────────────────────── + val AVMClampMin = -2147483647 + val AVMClampMax = 2147483647 + val AVMQ0Min = -32767 + val AVMQ0Max = 32767 + val Q16Scale = 65536L + val AVMMaxStack = 1024 + + def avmClamp(x: Long): Int = math.min(AVMClampMax, math.max(AVMClampMin, x.toInt)) + def avmQ0Clamp(x: Long): Int = math.min(AVMQ0Max, math.max(AVMQ0Min, x.toInt)) + + def floorDiv(a: Long, b: Long): Int = { + if (b == 0) throw new ArithmeticException("division by zero") + val q = a / b; val r = a % b + (if (r != 0 && ((a ^ b) < 0)) q - 1 else q).toInt + } + + def ltQ16V6(a: Int, b: Int): Boolean = { + val sa = a < 0; val sb = b < 0 + if (sa != sb) sa else a < b + } + + // ── Types ──────────────────────────────────────────────────── + sealed trait Ty + case object Q0_16 extends Ty; case object Q16_16 extends Ty; case object BoolTy extends Ty + + case class Val(ty: Ty, i: Int = 0, b: Boolean = false) + object Val { def q16(x: Int) = Val(Q16_16, i = avmClamp(x)) + def q0(x: Int) = Val(Q0_16, i = avmQ0Clamp(x)) + def bool(x: Boolean) = Val(BoolTy, b = x) } + + // ── Primitives ────────────────────────────────────────────── + sealed trait Prim + case object AddSatQ0 extends Prim; case object SubSatQ0 extends Prim + case object AddSatQ16 extends Prim; case object SubSatQ16 extends Prim + case object MulSatQ16 extends Prim; case object DivSatQ16 extends Prim + case object LtQ16 extends Prim; case object EqQ16 extends Prim + case object And extends Prim; case object Or extends Prim; case object Not extends Prim + + def primArity(p: Prim): Int = if (p == Not) 1 else 2 + + def execPrim(p: Prim, a: Val, b: Val): Val = (p, a.ty, b.ty) match { + case (AddSatQ0, Q0_16, Q0_16) => Val.q0(avmQ0Clamp(a.i.toLong + b.i)) + case (SubSatQ0, Q0_16, Q0_16) => Val.q0(avmQ0Clamp(a.i.toLong - b.i)) + case (AddSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(a.i.toLong + b.i)) + case (SubSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(a.i.toLong - b.i)) + case (MulSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(floorDiv(a.i.toLong * b.i, Q16Scale))) + case (DivSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(floorDiv(a.i.toLong * Q16Scale, b.i))) + case (LtQ16, Q16_16, Q16_16) => Val.bool(ltQ16V6(a.i, b.i)) + case (EqQ16, Q16_16, Q16_16) => Val.bool(a.i == b.i) + case (And, BoolTy, BoolTy) => Val.bool(a.b && b.b) + case (Or, BoolTy, BoolTy) => Val.bool(a.b || b.b) + case (Not, BoolTy, _) => Val.bool(!a.b) + case _ => throw new RuntimeException("type mismatch") + } + + // ── Instructions ──────────────────────────────────────────── + sealed trait Op + case class PushQ16(x: Int) extends Op; case class PushBool(b: Boolean) extends Op + case class PushQ0(x: Int) extends Op; case object Pop extends Op + case object Dup extends Op; case object Swap extends Op + case class Load(i: Int) extends Op; case class Store(i: Int) extends Op + case class Jump(t: Int) extends Op; case class JumpIf(t: Int) extends Op + case class Primitive(p: Prim) extends Op; case object Halt extends Op + + // ── State ─────────────────────────────────────────────────── + case class State(pc: Int, stack: List[Val], locals: Vector[Option[Val]], halted: Boolean) + def initState(nLocals: Int = 0): State = State(0, Nil, Vector.fill(nLocals)(None), false) + + // ── Step ──────────────────────────────────────────────────── + def step(s: State, prog: Vector[Op]): Option[State] = { + if (s.halted) return None + if (s.pc < 0 || s.pc >= prog.length) return Some(State(s.pc, s.stack, s.locals, true)) + + val instr = prog(s.pc); var stack = s.stack; val npc = s.pc + 1 + + val growing = instr match { + case _: PushQ16 | _: PushBool | _: PushQ0 | Dup | Load => true; case _ => false + } + if (growing && stack.length >= AVMMaxStack) return None + + instr match { + case PushQ16(x) => stack = Val.q16(x) :: stack + case PushBool(b) => stack = Val.bool(b) :: stack + case PushQ0(x) => stack = Val.q0(x) :: stack + case Pop => stack match { + case Nil => return None; case _ :: xs => stack = xs} + case Dup => stack match { + case Nil => return None; case x :: xs => stack = x :: x :: xs} + case Swap => stack match { + case a :: b :: xs => stack = b :: a :: xs; case _ => return None} + case Load(i) => + if (i >= s.locals.length || s.locals(i).isEmpty) return None + stack = s.locals(i).get :: stack + case Store(i) => stack match { + case Nil => return None + case v :: xs => + if (i >= s.locals.length) return None + val newLocals = s.locals.updated(i, Some(v)) + return Some(State(npc, xs, newLocals, false)) + } + case Jump(t) => if (t < 0 || t >= prog.length) return None + else return Some(State(t, stack, s.locals, false)) + case JumpIf(t) => stack match { + case Val(BoolTy, _, true) :: xs => + if (t < 0 || t >= prog.length) return None + return Some(State(t, xs, s.locals, false)) + case Val(BoolTy, _, false) :: xs => stack = xs + case _ => return None + } + case Primitive(p) => + val arity = primArity(p) + if (stack.length < arity) return None + val b = if (arity >= 2) { val (v, rest) = (stack.head, stack.tail); stack = rest; v } else Val.bool(false) + val a = stack.head; stack = stack.tail + try { stack = execPrim(p, a, b) :: stack } catch { case _: Throwable => return None } + case Halt => return Some(State(s.pc, stack, s.locals, true)) + } + Some(State(npc, stack, s.locals, false)) + } + + // ── Run (fuel-bounded) ───────────────────────────────────── + @annotation.tailrec + def run(s: State, prog: Vector[Op], fuel: Int = 10000): Option[State] = { + if (fuel <= 0 || s.halted) return Some(s) + step(s, prog) match { + case None => None + case Some(next) => run(next, prog, fuel - 1) + } + } +}