mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-11 15:00:34 +00:00
feat(avm-ports): port AVM ISA to all 12 scientific languages
Lean (reference), Python, Rust, C, C++, Go, Julia, R, Scala, Fortran, Coq, Octave — all implementing the same AVM ISA v1 specification. Every port implements: - Full type universe: Q0_16, Q16_16, Bool - 11 primitives with floor division (Lean Int.ediv), V6 signed comparison, symmetric clamping [-2147483647, 2147483647] - 12 instruction opcodes with stack depth limit (1024) - Fuel-bounded run loop - Error handling (stack under/overflow, type mismatch, div-by-zero, jump OOB)
This commit is contained in:
parent
1ae311c63f
commit
863da04f21
44 changed files with 1837 additions and 98 deletions
|
|
@ -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` | ✅ | ✅ | ✅ | — |
|
||||
|
||||
|
|
|
|||
197
c/avm.c
Normal file
197
c/avm.c
Normal file
|
|
@ -0,0 +1,197 @@
|
|||
/* AVM ISA v1 — C Port (Strict Functional Execution) */
|
||||
|
||||
#include <stdint.h>
|
||||
#include <stdbool.h>
|
||||
#include <stdlib.h>
|
||||
#include <string.h>
|
||||
|
||||
/* ── 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;
|
||||
}
|
||||
165
coq/AVMIsa/avm.v
Normal file
165
coq/AVMIsa/avm.v
Normal file
|
|
@ -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 <? 0 in
|
||||
let sb := b <? 0 in
|
||||
if Bool.eqb sa sb then a <? b else sa.
|
||||
|
||||
(* ── Types ──────────────────────────────────────────────────────── *)
|
||||
Inductive AvmTy : Type :=
|
||||
| Q0_16 | Q16_16 | Bool.
|
||||
|
||||
(* ── Values ──────────────────────────────────────────────────────── *)
|
||||
Inductive AvmVal : Type :=
|
||||
| Vq0 : Z -> 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 if (r >? 0) && (b <? 0) then q - 1
|
||||
else 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.
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
BIN
coq/CoreFormalism/Q16_16.vo
Normal file
BIN
coq/CoreFormalism/Q16_16.vo
Normal file
Binary file not shown.
204
cpp/avm.hpp
Normal file
204
cpp/avm.hpp
Normal file
|
|
@ -0,0 +1,204 @@
|
|||
// AVM ISA v1 — C++ Port (Strict Functional Execution)
|
||||
#pragma once
|
||||
#include <cstdint>
|
||||
#include <vector>
|
||||
#include <variant>
|
||||
#include <optional>
|
||||
#include <stdexcept>
|
||||
|
||||
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<int32_t>(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<int32_t>(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<int32_t>(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<int32_t, bool>;
|
||||
|
||||
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<int64_t>(std::get<int32_t>(a.val)) + std::get<int32_t>(b.val))};
|
||||
case Prim::SubSatQ0:
|
||||
check(a, Ty::Q0_16); check(b, Ty::Q0_16);
|
||||
return {Ty::Q0_16, avm_q0_clamp(static_cast<int64_t>(std::get<int32_t>(a.val)) - std::get<int32_t>(b.val))};
|
||||
case Prim::AddSatQ16:
|
||||
check(a, Ty::Q16_16); check(b, Ty::Q16_16);
|
||||
return {Ty::Q16_16, avm_clamp(static_cast<int64_t>(std::get<int32_t>(a.val)) + std::get<int32_t>(b.val))};
|
||||
case Prim::SubSatQ16:
|
||||
check(a, Ty::Q16_16); check(b, Ty::Q16_16);
|
||||
return {Ty::Q16_16, avm_clamp(static_cast<int64_t>(std::get<int32_t>(a.val)) - std::get<int32_t>(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<int64_t>(std::get<int32_t>(a.val)) * std::get<int32_t>(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<int64_t>(std::get<int32_t>(a.val)) * Q16_SCALE, std::get<int32_t>(b.val)))};
|
||||
case Prim::LtQ16:
|
||||
check(a, Ty::Q16_16); check(b, Ty::Q16_16);
|
||||
return {Ty::Bool, lt_q16_v6(std::get<int32_t>(a.val), std::get<int32_t>(b.val))};
|
||||
case Prim::EqQ16:
|
||||
check(a, Ty::Q16_16); check(b, Ty::Q16_16);
|
||||
return {Ty::Bool, std::get<int32_t>(a.val) == std::get<int32_t>(b.val)};
|
||||
case Prim::And:
|
||||
check(a, Ty::Bool); check(b, Ty::Bool);
|
||||
return {Ty::Bool, std::get<bool>(a.val) && std::get<bool>(b.val)};
|
||||
case Prim::Or:
|
||||
check(a, Ty::Bool); check(b, Ty::Bool);
|
||||
return {Ty::Bool, std::get<bool>(a.val) || std::get<bool>(b.val)};
|
||||
case Prim::Not:
|
||||
check(a, Ty::Bool);
|
||||
return {Ty::Bool, !std::get<bool>(a.val)};
|
||||
}
|
||||
throw std::runtime_error("unknown prim");
|
||||
}
|
||||
|
||||
// ── State ─────────────────────────────────────────────────────
|
||||
struct State {
|
||||
int pc = 0;
|
||||
std::vector<AnyVal> stack;
|
||||
std::vector<std::optional<AnyVal>> locals;
|
||||
bool halted = false;
|
||||
};
|
||||
|
||||
inline State init_state(size_t n_locals = 0) {
|
||||
return {0, {}, std::vector<std::optional<AnyVal>>(n_locals), false};
|
||||
}
|
||||
|
||||
// ── Step ─────────────────────────────────────────────────────
|
||||
inline std::optional<State> step(const State& s, const std::vector<Instr>& prog) {
|
||||
if (s.halted) return std::nullopt;
|
||||
if (s.pc < 0 || static_cast<size_t>(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<size_t>(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<bool>(v.val)) {
|
||||
if (instr.arg < 0 || static_cast<size_t>(instr.arg) >= prog.size()) return std::nullopt;
|
||||
npc = instr.arg;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case Op::Primitive: {
|
||||
auto p = static_cast<Prim>(instr.arg);
|
||||
int arity = prim_arity(p);
|
||||
if (static_cast<int>(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<State> run(const State& init, const std::vector<Instr>& 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
|
||||
198
fortran/avm.f90
Normal file
198
fortran/avm.f90
Normal file
|
|
@ -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
|
||||
225
go/avm.go
Normal file
225
go/avm.go
Normal file
|
|
@ -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
|
||||
}
|
||||
170
octave/avm.m
Normal file
170
octave/avm.m
Normal file
|
|
@ -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
|
||||
209
python/avm.py
Normal file
209
python/avm.py
Normal file
|
|
@ -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
|
||||
|
|
@ -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 }))
|
||||
}
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<const N: usize>(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<const N: usize>(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<const N: usize>(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"}
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<f64> = (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<const N: usize>(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<const N: usize>(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<const N: usize>(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"}
|
||||
|
|
|
|||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
|
|
@ -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:
|
||||
|
|
|
|||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
135
scala/avm.scala
Normal file
135
scala/avm.scala
Normal file
|
|
@ -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)
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue