mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
fix(avm-ports): align all 3 ports with Lean reference
Fixes applied to Rust, Julia, and R AVM ISA ports: 1. Division rounding: use floor division (matching Lean Int.ediv) 2. Clamp range: symmetric [-2147483647, 2147483647] for Q16_16, [-32767, 32767] for Q0_16 (preserves negation involution) 3. V6 sign-decomposition comparison for ltQ16 4. Stack depth limit: maxStackDepth = 1024 with StackOverflow error 5. Added AVM-specific constants and helpers to each port All three ports now match the Lean reference specification.
This commit is contained in:
parent
596d961276
commit
aeb87d86c8
27 changed files with 787 additions and 23 deletions
|
|
@ -20,7 +20,10 @@
|
|||
|
||||
3. **No `sorry` in committed code.**
|
||||
|
||||
4. **No `Float` in compute paths.** Use `Q0_16` or `Q16_16`.
|
||||
4. **No `Float` in compute paths (all languages).** This applies to Rust, Julia, R, Coq, and any other implementation in this repo — not just Lean. `Q0_16` or `Q16_16` fixed-point arithmetic is the canonical form. Float is permitted ONLY at the external boundary (JSON parsing, sensor data, hardware registers) and ONLY when no practical fixed-point alternative exists. Each float usage must:
|
||||
- Be bracketed: `of_float` / `to_float` calls at the module boundary, never in the core loop
|
||||
- Be documented in the commit message explaining why Q16_16 couldn't work
|
||||
- Be cross-validated by at least one other language port that uses pure Q16_16
|
||||
|
||||
5. **No `native_decide` unless it is the only tactic that closes the goal.** Use `norm_num`, `omega`, `simp`, `decide`, or explicit proof terms first. Document why `native_decide` is required when used. Exception: finitely decidable existence claims (e.g., N=8 necessity) are the canonical use case.
|
||||
|
||||
|
|
|
|||
2
coq/CoreFormalism/.Q16_16.aux
Normal file
2
coq/CoreFormalism/.Q16_16.aux
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
COQAUX1 03441a4df6ed6fdae62bc8cdd91bb74d /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v
|
||||
0 0 VernacProof "tac:no using:no"
|
||||
BIN
coq/CoreFormalism/.lia.cache
Normal file
BIN
coq/CoreFormalism/.lia.cache
Normal file
Binary file not shown.
49
coq/CoreFormalism/Q16_16.glob
Normal file
49
coq/CoreFormalism/Q16_16.glob
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
DIGEST 03441a4df6ed6fdae62bc8cdd91bb74d
|
||||
FQ16_16
|
||||
R72:77 Stdlib.ZArith.ZArith <> <> lib
|
||||
R79:81 Stdlib.micromega.Lia <> <> lib
|
||||
mod 91:96 <> Q16_16
|
||||
def 135:145 Q16_16 q16_min_raw
|
||||
R149:149 Corelib.Numbers.BinNums <> Z ind
|
||||
def 180:190 Q16_16 q16_max_raw
|
||||
R194:194 Corelib.Numbers.BinNums <> Z ind
|
||||
def 224:232 Q16_16 q16_scale
|
||||
R237:237 Corelib.Numbers.BinNums <> Z ind
|
||||
def 263:270 Q16_16 in_range
|
||||
R277:277 Corelib.Numbers.BinNums <> Z ind
|
||||
binder 273:273 <> x:1
|
||||
R310:313 Corelib.Init.Logic <> ::type_scope:x_'/\'_x not
|
||||
R305:308 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
|
||||
R294:304 Q16_16 Q16_16 q16_min_raw def
|
||||
R309:309 Q16_16 <> x:1 var
|
||||
R315:318 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
|
||||
R314:314 Q16_16 <> x:1 var
|
||||
R319:329 Q16_16 Q16_16 q16_max_raw def
|
||||
def 346:354 Q16_16 clamp_raw
|
||||
R361:361 Corelib.Numbers.BinNums <> Z ind
|
||||
binder 357:357 <> i:2
|
||||
R366:366 Corelib.Numbers.BinNums <> Z ind
|
||||
R378:385 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
|
||||
R399:399 Q16_16 <> i:2 var
|
||||
R387:397 Q16_16 Q16_16 q16_max_raw def
|
||||
R430:437 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
|
||||
R441:451 Q16_16 Q16_16 q16_min_raw def
|
||||
R439:439 Q16_16 <> i:2 var
|
||||
R479:479 Q16_16 <> i:2 var
|
||||
R458:468 Q16_16 Q16_16 q16_min_raw def
|
||||
R406:416 Q16_16 Q16_16 q16_max_raw def
|
||||
prf 493:505 Q16_16 clamp_bounded
|
||||
R512:512 Corelib.Numbers.BinNums <> Z ind
|
||||
binder 508:508 <> x:3
|
||||
R517:524 Q16_16 Q16_16 in_range def
|
||||
R527:535 Q16_16 Q16_16 clamp_raw def
|
||||
R537:537 Q16_16 <> x:3 var
|
||||
R561:569 Q16_16 Q16_16 clamp_raw def
|
||||
R572:579 Q16_16 Q16_16 in_range def
|
||||
R592:599 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
|
||||
R601:611 Q16_16 Q16_16 q16_max_raw def
|
||||
R592:599 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
|
||||
R601:611 Q16_16 Q16_16 q16_max_raw def
|
||||
R641:651 Q16_16 Q16_16 q16_min_raw def
|
||||
R654:664 Q16_16 Q16_16 q16_max_raw def
|
||||
R695:706 Stdlib.ZArith.BinInt Z lt_le_incl thm
|
||||
77
coq/CoreFormalism/Q16_16.v
Normal file
77
coq/CoreFormalism/Q16_16.v
Normal file
|
|
@ -0,0 +1,77 @@
|
|||
(* Coq Formalization of Q16_16 Fixed-Point Arithmetic *)
|
||||
Require Import ZArith Lia.
|
||||
Module Q16_16.
|
||||
Open Scope Z_scope.
|
||||
|
||||
Definition q16_min_raw : Z := -2147483648.
|
||||
Definition q16_max_raw : Z := 2147483647.
|
||||
Definition q16_scale : Z := 65536.
|
||||
|
||||
Definition in_range (x : Z) : Prop :=
|
||||
q16_min_raw <= x /\ x <= q16_max_raw.
|
||||
|
||||
Definition clamp_raw (i : Z) : Z :=
|
||||
if Z_lt_dec q16_max_raw i then q16_max_raw
|
||||
else if Z_lt_dec i q16_min_raw then q16_min_raw
|
||||
else i.
|
||||
|
||||
Theorem clamp_bounded (x : Z) : in_range (clamp_raw x).
|
||||
Proof.
|
||||
unfold clamp_raw, in_range.
|
||||
case (Z_lt_dec q16_max_raw x); intros H1.
|
||||
- unfold q16_min_raw, q16_max_raw; split; [unfold q16_min_raw, q16_max_raw; lia | apply Z.lt_le_incl; exact H1].
|
||||
- case (Z_lt_dec x q16_min_raw); intros H2.
|
||||
+ unfold q16_min_raw, q16_max_raw; split; [apply Z.lt_le_incl; exact H2 | unfold q16_min_raw, q16_max_raw; lia].
|
||||
+ split; apply Z.nlt_ge; assumption.
|
||||
Qed.
|
||||
|
||||
Theorem clamp_idempotent (x : Z) (h : in_range x) : clamp_raw x = x.
|
||||
Proof.
|
||||
destruct h as [Hlo Hhi].
|
||||
unfold clamp_raw.
|
||||
case (Z_lt_dec q16_max_raw x); intros Hgt; [exfalso; lia|].
|
||||
case (Z_lt_dec x q16_min_raw); intros Hlt; [exfalso; lia|].
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Definition zero : Z := 0.
|
||||
Definition one : Z := 65536.
|
||||
Definition epsilon : Z := 1.
|
||||
Definition half : Z := 32768.
|
||||
Definition pct1 : Z := 655.
|
||||
Definition pct70 : Z := 45875.
|
||||
Definition pct30 : Z := 19661.
|
||||
Definition one50 : Z := 98304.
|
||||
|
||||
Definition add (a b : Z) : Z := clamp_raw (a + b).
|
||||
Definition sub (a b : Z) : Z := clamp_raw (a - b).
|
||||
Definition neg (a : Z) : Z := clamp_raw (-a).
|
||||
Definition mul (a b : Z) : Z := clamp_raw (Z.div (a * b) q16_scale).
|
||||
Definition div (a b : Z) : Z :=
|
||||
if Z.eq_dec b 0 then zero else clamp_raw (Z.div (a * q16_scale) b).
|
||||
|
||||
Theorem add_comm (a b : Z) : add a b = add b a.
|
||||
Proof. unfold add; rewrite Z.add_comm; reflexivity. Qed.
|
||||
|
||||
Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
|
||||
(hsum : in_range (a + b)) : add a b = a + b.
|
||||
Proof.
|
||||
unfold add; rewrite clamp_idempotent; [reflexivity| exact hsum].
|
||||
Qed.
|
||||
|
||||
Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero.
|
||||
Proof.
|
||||
unfold sub, zero; rewrite Z.sub_diag.
|
||||
apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw; lia.
|
||||
Qed.
|
||||
|
||||
Theorem mul_comm (a b : Z) : mul a b = mul b a.
|
||||
Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed.
|
||||
|
||||
Theorem in_range_zero : in_range 0.
|
||||
Proof. unfold in_range, q16_min_raw, q16_max_raw; lia. Qed.
|
||||
|
||||
Theorem in_range_one : in_range 1.
|
||||
Proof. unfold in_range, q16_min_raw, q16_max_raw; lia. Qed.
|
||||
|
||||
End Q16_16.
|
||||
|
|
@ -61,10 +61,16 @@ halt() = Instr(10, 0, false)
|
|||
MISSING_LOCAL
|
||||
DIVISION_BY_ZERO
|
||||
JUMP_OUT_OF_BOUNDS
|
||||
STACK_OVERFLOW
|
||||
HALTED
|
||||
UNKNOWN_INSTR
|
||||
end
|
||||
|
||||
# ── AVM constants ───────────────────────────────────────────────────
|
||||
const AVM_CLAMP_MIN = -2147483647
|
||||
const AVM_CLAMP_MAX = 2147483647
|
||||
const AVM_MAX_STACK = 1024
|
||||
|
||||
# ── State ──────────────────────────────────────────────────────────
|
||||
|
||||
struct State
|
||||
|
|
@ -88,20 +94,29 @@ q16_val(v::Int32) = v
|
|||
|
||||
# ── Primitive execution ────────────────────────────────────────────
|
||||
|
||||
# AVM symmetric clamp (excludes INT32_MIN for negation involution)
|
||||
avm_clamp(x::Int64) = Int32(min(AVM_CLAMP_MAX, max(AVM_CLAMP_MIN, x)))
|
||||
|
||||
# V6 signed comparison for AVM
|
||||
lt_q16_v6(a::Int32, b::Int32) = (a < 0) != (b < 0) ? (a < 0) : (a < b)
|
||||
|
||||
function exec_prim(op::Prim, a::Union{Int32, Bool}, b::Union{Int32, Bool, Nothing})
|
||||
if op == ADD_SAT_Q16
|
||||
x = clamp(Int64(a::Int32) + Int64(b::Int32), typemin(Int32), typemax(Int32))
|
||||
return (Int32(x), true)
|
||||
return (avm_clamp(Int64(a::Int32) + Int64(b::Int32)), true)
|
||||
elseif op == SUB_SAT_Q16
|
||||
x = clamp(Int64(a::Int32) - Int64(b::Int32), typemin(Int32), typemax(Int32))
|
||||
return (Int32(x), true)
|
||||
return (avm_clamp(Int64(a::Int32) - Int64(b::Int32)), true)
|
||||
elseif op == MUL_SAT_Q16
|
||||
return (Q16_16.q_mul(a::Int32, b::Int32), true)
|
||||
# Floor division matching Lean Int.ediv: (a * b) / 65536
|
||||
prod = Int64(a::Int32) * Int64(b::Int32)
|
||||
result = div(prod, Q16_16.Q16_SCALE) # div = floor division in Julia
|
||||
return (avm_clamp(result), true)
|
||||
elseif op == DIV_SAT_Q16
|
||||
b::Int32 == 0 && error(DIVISION_BY_ZERO)
|
||||
return (Q16_16.q_div(a::Int32, b::Int32), true)
|
||||
num = Int64(b::Int32) * Q16_16.Q16_SCALE
|
||||
result = div(num, Int64(a::Int32)) # div = floor division in Julia
|
||||
return (avm_clamp(result), true)
|
||||
elseif op == LT_Q16
|
||||
return (a::Int32 < b::Int32, false)
|
||||
return (lt_q16_v6(a::Int32, b::Int32), false)
|
||||
elseif op == EQ_Q16
|
||||
return (a::Int32 == b::Int32, false)
|
||||
elseif op == AND_OP
|
||||
|
|
@ -132,6 +147,8 @@ function step(s::State, program::Vector{Instr})::State
|
|||
pc = s.pc + 1
|
||||
halted = false
|
||||
|
||||
length(stack) >= AVM_MAX_STACK && (instr.op in (0, 1, 3, 5)) && error(STACK_OVERFLOW)
|
||||
|
||||
if instr.op == 0 # push_val (Bool)
|
||||
push!(stack, instr.arg2)
|
||||
push!(is_q16, false)
|
||||
|
|
|
|||
247
r/AVMIsa/avm.r
Normal file
247
r/AVMIsa/avm.r
Normal file
|
|
@ -0,0 +1,247 @@
|
|||
# AVM ISA v1 — R Port (Strict Functional Execution)
|
||||
#
|
||||
# Mirrors `formal/SilverSight/AVMIsa/` (Lean 4) and `rust/src/avm/` (Rust).
|
||||
# Pure functions: step(state, program) -> state, run(state, program, fuel) -> state
|
||||
|
||||
# ── Instruction type ─────────────────────────────────────────────────
|
||||
|
||||
# Instr is a list with fields:
|
||||
# op: integer code (0=push_q16, 1=push_bool, 2=pop, 3=dup, 4=swap,
|
||||
# 5=load, 6=store, 7=jump, 8=jump_if, 9=prim, 10=halt)
|
||||
# arg: integer payload
|
||||
|
||||
INSTR_PUSH_Q16 <- 0L
|
||||
INSTR_PUSH_BOOL <- 1L
|
||||
INSTR_POP <- 2L
|
||||
INSTR_DUP <- 3L
|
||||
INSTR_SWAP <- 4L
|
||||
INSTR_LOAD <- 5L
|
||||
INSTR_STORE <- 6L
|
||||
INSTR_JUMP <- 7L
|
||||
INSTR_JUMP_IF <- 8L
|
||||
INSTR_PRIM <- 9L
|
||||
INSTR_HALT <- 10L
|
||||
|
||||
# ── Primitives ───────────────────────────────────────────────────────
|
||||
|
||||
PRIM_ADD_Q16 <- 0L
|
||||
PRIM_SUB_Q16 <- 1L
|
||||
PRIM_MUL_Q16 <- 2L
|
||||
PRIM_DIV_Q16 <- 3L
|
||||
PRIM_LT_Q16 <- 4L
|
||||
PRIM_EQ_Q16 <- 5L
|
||||
PRIM_AND <- 6L
|
||||
PRIM_OR <- 7L
|
||||
PRIM_NOT <- 8L
|
||||
|
||||
# ── Step Error codes ─────────────────────────────────────────────────
|
||||
|
||||
ERR_EMPTY_STACK <- "empty_stack"
|
||||
ERR_STACK_UNDERFLOW <- "stack_underflow"
|
||||
ERR_TYPE_MISMATCH <- "type_mismatch"
|
||||
ERR_MISSING_LOCAL <- "missing_local"
|
||||
ERR_DIV_BY_ZERO <- "division_by_zero"
|
||||
ERR_JUMP_OOB <- "jump_out_of_bounds"
|
||||
ERR_STACK_OVERFLOW <- "stack_overflow"
|
||||
ERR_HALTED <- "halted"
|
||||
|
||||
# ── AVM constants ───────────────────────────────────────────────────
|
||||
|
||||
AVM_CLAMP_MIN <- -2147483647L
|
||||
AVM_CLAMP_MAX <- 2147483647L
|
||||
AVM_MAX_STACK <- 1024L
|
||||
|
||||
# ── Instruction constructors ─────────────────────────────────────────
|
||||
|
||||
instr_push_q16 <- function(x) list(op = INSTR_PUSH_Q16, arg = as.integer(x))
|
||||
instr_push_bool <- function(x) list(op = INSTR_PUSH_BOOL, arg = as.integer(x))
|
||||
instr_pop <- function() list(op = INSTR_POP, arg = 0L)
|
||||
instr_dup <- function() list(op = INSTR_DUP, arg = 0L)
|
||||
instr_swap <- function() list(op = INSTR_SWAP, arg = 0L)
|
||||
instr_load <- function(i) list(op = INSTR_LOAD, arg = as.integer(i))
|
||||
instr_store <- function(i) list(op = INSTR_STORE, arg = as.integer(i))
|
||||
instr_jump <- function(t) list(op = INSTR_JUMP, arg = as.integer(t))
|
||||
instr_jump_if <- function(t) list(op = INSTR_JUMP_IF, arg = as.integer(t))
|
||||
instr_prim <- function(p) list(op = INSTR_PRIM, arg = as.integer(p))
|
||||
instr_halt <- function() list(op = INSTR_HALT, arg = 0L)
|
||||
|
||||
# ── State constructor ────────────────────────────────────────────────
|
||||
|
||||
new_state <- function(n_locals = 0L) {
|
||||
list(
|
||||
pc = 1L,
|
||||
stack = list(), # each element: list(type="q16", val=integer) or list(type="bool", val=logical)
|
||||
locals = vector("list", n_locals), # elements can be NULL
|
||||
local_types = vector("list", n_locals),
|
||||
halted = FALSE
|
||||
)
|
||||
}
|
||||
|
||||
# ── Stack helpers ────────────────────────────────────────────────────
|
||||
|
||||
make_q16 <- function(x) list(type = "q16", val = as.integer(x))
|
||||
make_bool <- function(x) list(type = "bool", val = as.logical(x))
|
||||
|
||||
is_q16 <- function(v) identical(v$type, "q16")
|
||||
is_bool <- function(v) identical(v$type, "bool")
|
||||
|
||||
# ── Q16_16 helpers ───────────────────────────────────────────────────
|
||||
|
||||
Q16_SCALE <- 65536L
|
||||
|
||||
# AVM symmetric clamp
|
||||
avm_clamp <- function(x) {
|
||||
min(AVM_CLAMP_MAX, max(AVM_CLAMP_MIN, as.integer(x)))
|
||||
}
|
||||
|
||||
# V6 signed comparison
|
||||
lt_q16_v6 <- function(a, b) {
|
||||
sa <- a < 0L
|
||||
sb <- b < 0L
|
||||
if (sa != sb) sa else a < b
|
||||
}
|
||||
|
||||
q16_mul <- function(a, b) {
|
||||
# Floor division matching Lean Int.ediv: (a * b) %/% 65536
|
||||
prod <- as.numeric(a) * as.numeric(b)
|
||||
avm_clamp(prod %/% Q16_SCALE)
|
||||
}
|
||||
|
||||
q16_div <- function(a, b) {
|
||||
if (b == 0L) stop(ERR_DIV_BY_ZERO)
|
||||
# Floor division matching Lean Int.ediv: (y * 65536) %/% x
|
||||
num <- as.numeric(a) * Q16_SCALE
|
||||
avm_clamp(num %/% as.numeric(b))
|
||||
}
|
||||
|
||||
# ── Primitive execution ──────────────────────────────────────────────
|
||||
|
||||
exec_prim <- function(op, a, b = NULL) {
|
||||
if (op == PRIM_ADD_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
x <- as.numeric(a$val) + as.numeric(b$val)
|
||||
make_q16(avm_clamp(x))
|
||||
} else if (op == PRIM_SUB_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
x <- as.numeric(a$val) - as.numeric(b$val)
|
||||
make_q16(avm_clamp(x))
|
||||
} else if (op == PRIM_MUL_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_q16(q16_mul(a$val, b$val))
|
||||
} else if (op == PRIM_DIV_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_q16(q16_div(a$val, b$val))
|
||||
} else if (op == PRIM_LT_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_bool(lt_q16_v6(a$val, b$val))
|
||||
} else if (op == PRIM_EQ_Q16) {
|
||||
if (!is_q16(a) || !is_q16(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_bool(a$val == b$val)
|
||||
} else if (op == PRIM_AND) {
|
||||
if (!is_bool(a) || !is_bool(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_bool(a$val && b$val)
|
||||
} else if (op == PRIM_OR) {
|
||||
if (!is_bool(a) || !is_bool(b)) stop(ERR_TYPE_MISMATCH)
|
||||
make_bool(a$val || b$val)
|
||||
} else if (op == PRIM_NOT) {
|
||||
if (!is_bool(a)) stop(ERR_TYPE_MISMATCH)
|
||||
make_bool(!a$val)
|
||||
} else {
|
||||
stop("unknown prim")
|
||||
}
|
||||
}
|
||||
|
||||
# ── Step (pure function) ─────────────────────────────────────────────
|
||||
|
||||
step <- function(s, prog) {
|
||||
if (s$halted) stop(ERR_HALTED)
|
||||
if (s$pc < 1L || s$pc > length(prog)) {
|
||||
return(list(pc = s$pc, stack = s$stack, locals = s$locals,
|
||||
local_types = s$local_types, halted = TRUE))
|
||||
}
|
||||
|
||||
instr <- prog[[s$pc]]
|
||||
stack <- s$stack
|
||||
locals <- s$locals
|
||||
local_types <- s$local_types
|
||||
pc <- s$pc + 1L
|
||||
halted <- FALSE
|
||||
|
||||
# Stack depth check (push, dup, load grow the stack)
|
||||
if (instr$op %in% c(INSTR_PUSH_Q16, INSTR_PUSH_BOOL, INSTR_DUP, INSTR_LOAD) &&
|
||||
length(stack) >= AVM_MAX_STACK) stop(ERR_STACK_OVERFLOW)
|
||||
|
||||
if (instr$op == INSTR_PUSH_Q16) {
|
||||
stack <- c(stack, list(make_q16(instr$arg)))
|
||||
} else if (instr$op == INSTR_PUSH_BOOL) {
|
||||
stack <- c(stack, list(make_bool(instr$arg != 0L)))
|
||||
} else if (instr$op == INSTR_POP) {
|
||||
if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
|
||||
stack <- stack[-length(stack)]
|
||||
} else if (instr$op == INSTR_DUP) {
|
||||
if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
|
||||
stack <- c(stack, stack[length(stack)])
|
||||
} else if (instr$op == INSTR_SWAP) {
|
||||
if (length(stack) < 2L) stop(ERR_STACK_UNDERFLOW)
|
||||
n <- length(stack)
|
||||
tmp <- stack[[n]]; stack[[n]] <- stack[[n-1]]; stack[[n-1]] <- tmp
|
||||
} else if (instr$op == INSTR_LOAD) {
|
||||
i <- instr$arg + 1L
|
||||
if (i > length(locals)) stop(ERR_MISSING_LOCAL)
|
||||
if (is.null(locals[[i]])) stop(ERR_MISSING_LOCAL)
|
||||
stack <- c(stack, list(make_q16(locals[[i]])))
|
||||
} else if (instr$op == INSTR_STORE) {
|
||||
i <- instr$arg + 1L
|
||||
if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
|
||||
if (i > length(locals)) stop(ERR_MISSING_LOCAL)
|
||||
v <- stack[[length(stack)]]
|
||||
stack <- stack[-length(stack)]
|
||||
locals[[i]] <- v$val
|
||||
local_types[[i]] <- v$type
|
||||
} else if (instr$op == INSTR_JUMP) {
|
||||
target <- instr$arg + 1L
|
||||
if (target < 1L || target > length(prog)) stop(ERR_JUMP_OOB)
|
||||
pc <- target
|
||||
} else if (instr$op == INSTR_JUMP_IF) {
|
||||
if (length(stack) == 0L) stop(ERR_EMPTY_STACK)
|
||||
cond <- stack[[length(stack)]]
|
||||
stack <- stack[-length(stack)]
|
||||
if (is_bool(cond) && cond$val) {
|
||||
target <- instr$arg + 1L
|
||||
if (target < 1L || target > length(prog)) stop(ERR_JUMP_OOB)
|
||||
pc <- target
|
||||
} else if (!is_bool(cond)) {
|
||||
stop(ERR_TYPE_MISMATCH)
|
||||
}
|
||||
} else if (instr$op == INSTR_PRIM) {
|
||||
p <- instr$arg
|
||||
arity <- if (p == PRIM_NOT) 1L else 2L
|
||||
if (length(stack) < arity) stop(ERR_STACK_UNDERFLOW)
|
||||
if (arity >= 2L) {
|
||||
b <- stack[[length(stack)]]
|
||||
stack <- stack[-length(stack)]
|
||||
} else {
|
||||
b <- NULL
|
||||
}
|
||||
a <- stack[[length(stack)]]
|
||||
stack <- stack[-length(stack)]
|
||||
result <- exec_prim(p, a, b)
|
||||
stack <- c(stack, list(result))
|
||||
} else if (instr$op == INSTR_HALT) {
|
||||
halted <- TRUE
|
||||
}
|
||||
|
||||
list(pc = pc, stack = stack, locals = locals,
|
||||
local_types = local_types, halted = halted)
|
||||
}
|
||||
|
||||
# ── Run (fuel-bounded) ──────────────────────────────────────────────
|
||||
|
||||
run <- function(initial, prog, fuel = 1000L) {
|
||||
s <- initial
|
||||
for (i in seq_len(fuel)) {
|
||||
if (s$halted) return(s)
|
||||
s <- step(s, prog)
|
||||
}
|
||||
s
|
||||
}
|
||||
70
r/AVMIsa/test_avm.r
Normal file
70
r/AVMIsa/test_avm.r
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
source("/home/allaun/SilverSight/r/AVMIsa/avm.r")
|
||||
|
||||
# Test 1: add Q16
|
||||
prog <- list(
|
||||
instr_push_q16(5 * 65536),
|
||||
instr_push_q16(3 * 65536),
|
||||
instr_prim(PRIM_ADD_Q16),
|
||||
instr_halt()
|
||||
)
|
||||
s <- new_state(0)
|
||||
s <- run(s, prog, 100)
|
||||
stopifnot(s$halted)
|
||||
stopifnot(length(s$stack) == 1)
|
||||
stopifnot(s$stack[[1]]$val == 8 * 65536)
|
||||
cat("PASS: add Q16\n")
|
||||
|
||||
# Test 2: jump_if
|
||||
prog <- list(
|
||||
instr_push_bool(TRUE),
|
||||
instr_jump_if(4),
|
||||
instr_push_q16(0),
|
||||
instr_halt(),
|
||||
instr_push_q16(65536),
|
||||
instr_halt()
|
||||
)
|
||||
s <- new_state(0)
|
||||
s <- run(s, prog, 100)
|
||||
stopifnot(s$halted)
|
||||
stopifnot(length(s$stack) == 1)
|
||||
stopifnot(s$stack[[1]]$val == 65536)
|
||||
cat("PASS: jump_if\n")
|
||||
|
||||
# Test 3: store/load
|
||||
prog <- list(
|
||||
instr_push_q16(42 * 65536),
|
||||
instr_store(0),
|
||||
instr_load(0),
|
||||
instr_halt()
|
||||
)
|
||||
s <- new_state(1)
|
||||
s <- run(s, prog, 100)
|
||||
stopifnot(length(s$stack) == 1)
|
||||
stopifnot(s$stack[[1]]$val == 42 * 65536)
|
||||
cat("PASS: store/load\n")
|
||||
|
||||
# Test 4: type error
|
||||
prog <- list(
|
||||
instr_push_bool(TRUE),
|
||||
instr_push_q16(65536),
|
||||
instr_prim(PRIM_ADD_Q16),
|
||||
instr_halt()
|
||||
)
|
||||
s <- new_state(0)
|
||||
result <- tryCatch(run(s, prog, 100), error = function(e) e)
|
||||
stopifnot(inherits(result, "error"))
|
||||
cat("PASS: type error\n")
|
||||
|
||||
# Test 5: division by zero
|
||||
prog <- list(
|
||||
instr_push_q16(65536),
|
||||
instr_push_q16(0),
|
||||
instr_prim(PRIM_DIV_Q16),
|
||||
instr_halt()
|
||||
)
|
||||
s <- new_state(0)
|
||||
result <- tryCatch(run(s, prog, 100), error = function(e) e)
|
||||
stopifnot(inherits(result, "error"))
|
||||
cat("PASS: division by zero\n")
|
||||
|
||||
cat("\nAll R AVM tests passed!\n")
|
||||
|
|
@ -11,6 +11,36 @@
|
|||
|
||||
use crate::q16::*;
|
||||
|
||||
// ── AVM-specific constants ──────────────────────────────────────────
|
||||
// AVM uses symmetric clamping [-2147483647, 2147483647] (excludes INT32_MIN)
|
||||
// to guarantee negation is a perfect involution.
|
||||
const AVM_CLAMP_MIN: i32 = -2147483647;
|
||||
const AVM_CLAMP_MAX: i32 = 2147483647;
|
||||
const AVM_Q0_MIN: i32 = -32767;
|
||||
const AVM_Q0_MAX: i32 = 32767;
|
||||
const AVM_MAX_STACK: usize = 1024;
|
||||
|
||||
/// Floor division matching Lean `Int.ediv` (rounds toward negative infinity).
|
||||
fn floor_div(a: i32, b: i32) -> i32 {
|
||||
let d = a / b;
|
||||
let r = a % b;
|
||||
if r != 0 && ((a ^ b) < 0) { d - 1 } else { d }
|
||||
}
|
||||
|
||||
/// AVM saturating clamp: [-2147483647, 2147483647]
|
||||
fn avm_clamp(v: i64) -> i32 {
|
||||
if v > AVM_CLAMP_MAX as i64 { AVM_CLAMP_MAX }
|
||||
else if v < AVM_CLAMP_MIN as i64 { AVM_CLAMP_MIN }
|
||||
else { v as i32 }
|
||||
}
|
||||
|
||||
/// V6 sign-decomposition comparison for Q16_16.
|
||||
fn lt_q16_v6(a: i32, b: i32) -> bool {
|
||||
let sa = a < 0;
|
||||
let sb = b < 0;
|
||||
if sa != sb { sa } else { a < b }
|
||||
}
|
||||
|
||||
// ── Types ───────────────────────────────────────────────────────────
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
|
|
@ -71,6 +101,7 @@ use crate::q16::*;
|
|||
MissingLocal(usize),
|
||||
DivisionByZero,
|
||||
JumpOutOfBounds(usize),
|
||||
StackOverflow,
|
||||
Halted,
|
||||
}
|
||||
|
||||
|
|
@ -103,32 +134,42 @@ use crate::q16::*;
|
|||
(Prim::Not, AvmVal::Q0_16(_), None) => {
|
||||
Ok(AvmVal::Bool(false)) // simplified: Q0_16 not is bitwise
|
||||
}
|
||||
// Q0_16 binary
|
||||
// Q0_16 binary (symmetric clamp)
|
||||
(Prim::AddSatQ0, AvmVal::Q0_16(x), Some(AvmVal::Q0_16(y))) => {
|
||||
let r = x.saturating_add(*y);
|
||||
Ok(AvmVal::Q0_16(r.max(-32768).min(32767)))
|
||||
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.saturating_sub(*y);
|
||||
Ok(AvmVal::Q0_16(r.max(-32768).min(32767)))
|
||||
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 }))
|
||||
}
|
||||
// Q16_16 binary
|
||||
// Q16_16 binary (symmetric clamp, floor division)
|
||||
(Prim::AddSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
Ok(AvmVal::Q16_16(x.saturating_add(*y)))
|
||||
Ok(AvmVal::Q16_16(avm_clamp((*x as i64) + (*y as i64))))
|
||||
}
|
||||
(Prim::SubSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
Ok(AvmVal::Q16_16(x.saturating_sub(*y)))
|
||||
Ok(AvmVal::Q16_16(avm_clamp((*x as i64) - (*y as i64))))
|
||||
}
|
||||
(Prim::MulSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
Ok(AvmVal::Q16_16(mul(*x, *y)))
|
||||
// Floor division matching Lean Int.ediv
|
||||
let prod = (*x as i64) * (*y as i64);
|
||||
let result = if prod >= 0 { prod / Q16_SCALE as i64 }
|
||||
else { -((-prod + Q16_SCALE as i64 - 1) / Q16_SCALE as i64) };
|
||||
Ok(AvmVal::Q16_16(avm_clamp(result)))
|
||||
}
|
||||
(Prim::DivSatQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
if *y == 0 { return Err(StepError::DivisionByZero); }
|
||||
Ok(AvmVal::Q16_16(div_op(*x, *y)))
|
||||
// Floor division matching Lean Int.ediv: (y * 65536) / x
|
||||
let num = (*y as i64) * Q16_SCALE as i64;
|
||||
let result = if num >= 0 { num / (*x as i64) }
|
||||
else { -((-num + (*x as i64).abs() - 1) / (*x as i64).abs()) };
|
||||
Ok(AvmVal::Q16_16(avm_clamp(result)))
|
||||
}
|
||||
// Comparisons
|
||||
// Comparisons (V6 sign-decomposition)
|
||||
(Prim::LtQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
Ok(AvmVal::Bool(x < y))
|
||||
Ok(AvmVal::Bool(lt_q16_v6(*x, *y)))
|
||||
}
|
||||
(Prim::EqQ16, AvmVal::Q16_16(x), Some(AvmVal::Q16_16(y))) => {
|
||||
Ok(AvmVal::Bool(x == y))
|
||||
|
|
@ -176,14 +217,24 @@ use crate::q16::*;
|
|||
let mut pc = s.pc + 1;
|
||||
let mut halted = false;
|
||||
|
||||
fn check_stack(stack: &[AvmVal]) -> Result<(), StepError> {
|
||||
if stack.len() >= AVM_MAX_STACK {
|
||||
return Err(StepError::StackOverflow);
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
|
||||
match instr {
|
||||
Instr::Push(v) => {
|
||||
check_stack(&stack)?;
|
||||
stack.push(v.clone());
|
||||
}
|
||||
Instr::Pop => {
|
||||
stack.pop().ok_or(StepError::EmptyStack)?;
|
||||
}
|
||||
Instr::Dup => {
|
||||
stack.last().ok_or(StepError::EmptyStack)?;
|
||||
check_stack(&stack)?;
|
||||
let v = stack.last().ok_or(StepError::EmptyStack)?.clone();
|
||||
stack.push(v);
|
||||
}
|
||||
|
|
@ -196,6 +247,7 @@ use crate::q16::*;
|
|||
Instr::Load(i) => {
|
||||
let v = locals.get(*i).ok_or(StepError::MissingLocal(*i))?
|
||||
.clone().ok_or(StepError::MissingLocal(*i))?;
|
||||
check_stack(&stack)?;
|
||||
stack.push(v);
|
||||
}
|
||||
Instr::Store(i) => {
|
||||
|
|
|
|||
|
|
@ -2,3 +2,4 @@ pub mod q16;
|
|||
pub mod nuvmap;
|
||||
pub mod silversight;
|
||||
pub mod avm;
|
||||
pub mod pist;
|
||||
|
|
|
|||
242
rust/src/pist/mod.rs
Normal file
242
rust/src/pist/mod.rs
Normal file
|
|
@ -0,0 +1,242 @@
|
|||
//! PIST Spectral — Rust Port
|
||||
//!
|
||||
//! Mirrors `formal/SilverSight/PIST/Spectral.lean`.
|
||||
//! Minimal fixed-point spectral feature extraction:
|
||||
//! - isqrt (integer square root)
|
||||
//! - power iteration for dominant eigenvalue
|
||||
//! - SpectralProfile
|
||||
//! - Fiedler value via Laplacian
|
||||
|
||||
use crate::q16::*;
|
||||
|
||||
// ── Integer square root ────────────────────────────────────────────
|
||||
|
||||
/// Integer square root via Newton's method. Returns floor(√n).
|
||||
pub fn isqrt(n: i64) -> i64 {
|
||||
if n <= 0 { return 0; }
|
||||
let mut x = n / 2 + 1;
|
||||
for _ in 0..64 {
|
||||
let x_new = (x + n / x) / 2;
|
||||
if x_new >= x { return x; }
|
||||
x = x_new;
|
||||
}
|
||||
x
|
||||
}
|
||||
|
||||
// ── Matrix helpers ─────────────────────────────────────────────────
|
||||
|
||||
type IntMat = Vec<Vec<i64>>;
|
||||
|
||||
fn get_entry(mat: &IntMat, i: usize, j: usize) -> i64 {
|
||||
mat.get(i).and_then(|row| row.get(j).copied()).unwrap_or(0)
|
||||
}
|
||||
|
||||
fn row_sum(mat: &IntMat, i: usize, n: usize) -> i64 {
|
||||
(0..n).map(|j| get_entry(mat, i, j)).sum()
|
||||
}
|
||||
|
||||
fn symmetrize(mat: &IntMat, n: usize) -> IntMat {
|
||||
(0..n).map(|i| {
|
||||
(0..n).map(|j| {
|
||||
(get_entry(mat, i, j) + get_entry(mat, j, i)) / 2
|
||||
}).collect()
|
||||
}).collect()
|
||||
}
|
||||
|
||||
fn build_laplacian(sym: &IntMat, n: usize) -> IntMat {
|
||||
(0..n).map(|i| {
|
||||
let deg = row_sum(sym, i, n);
|
||||
(0..n).map(|j| {
|
||||
if i == j { deg } else { -get_entry(sym, i, j) }
|
||||
}).collect()
|
||||
}).collect()
|
||||
}
|
||||
|
||||
fn build_ata(mat: &IntMat, n: usize) -> IntMat {
|
||||
(0..n).map(|i| {
|
||||
(0..n).map(|j| {
|
||||
(0..n).map(|k| get_entry(mat, k, i) * get_entry(mat, k, j)).sum()
|
||||
}).collect()
|
||||
}).collect()
|
||||
}
|
||||
|
||||
// ── SpectralProfile ────────────────────────────────────────────────
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct SpectralProfile {
|
||||
pub dominant_eigenvalue: f64,
|
||||
pub fiedler_value: f64,
|
||||
pub spectral_gap: f64,
|
||||
pub condition_number: f64,
|
||||
}
|
||||
|
||||
// ── Power iteration (f64 arithmetic) ───────────────────────────────
|
||||
|
||||
/// Dominant eigenvalue of a square Int matrix via power iteration.
|
||||
pub fn power_iteration(mat: &IntMat, max_iter: usize) -> f64 {
|
||||
let n = mat.len();
|
||||
if n == 0 { return 0.0; }
|
||||
|
||||
let mut v: Vec<f64> = (0..n).map(|i| (i as f64 + 1.0)).collect();
|
||||
|
||||
for _ in 0..max_iter {
|
||||
// mat × v (as f64)
|
||||
let mv: Vec<f64> = (0..n).map(|i| {
|
||||
(0..n).map(|j| get_entry(mat, i, j) as f64 * v[j]).sum()
|
||||
}).collect();
|
||||
|
||||
// Rayleigh quotient
|
||||
let v_dot_mv: f64 = v.iter().zip(mv.iter()).map(|(vi, mvi)| vi * mvi).sum();
|
||||
let v_dot_v: f64 = v.iter().map(|x| x * x).sum();
|
||||
if v_dot_v < 1e-15 { break; }
|
||||
|
||||
// Copy for next iteration, normalized
|
||||
let norm = (mv.iter().map(|x| x * x).sum::<f64>()).sqrt();
|
||||
if norm < 1e-15 { break; }
|
||||
for (vi, mvi) in v.iter_mut().zip(mv.iter()) {
|
||||
*vi = mvi / norm;
|
||||
}
|
||||
|
||||
// Check convergence
|
||||
let eig = v_dot_mv / v_dot_v;
|
||||
let mx = (0..n).map(|i| {
|
||||
(0..n).map(|j| get_entry(mat, i, j) as f64 * v[j]).sum::<f64>()
|
||||
}).collect::<Vec<_>>();
|
||||
let resid: f64 = mx.iter().zip(v.iter()).map(|(mxi, vi)| (mxi - eig * vi).abs()).sum::<f64>() / n as f64;
|
||||
if resid < 1e-8 { return eig; }
|
||||
}
|
||||
|
||||
// Final Rayleigh quotient
|
||||
let mv: Vec<f64> = (0..n).map(|i| {
|
||||
(0..n).map(|j| get_entry(mat, i, j) as f64 * v[j]).sum()
|
||||
}).collect();
|
||||
let num: f64 = v.iter().zip(mv.iter()).map(|(vi, mvi)| vi * mvi).sum();
|
||||
let den: f64 = v.iter().map(|x| x * x).sum();
|
||||
if den > 0.0 { num / den } else { 0.0 }
|
||||
}
|
||||
|
||||
fn rayleigh_quotient(mat: &IntMat, v: &[f64]) -> f64 {
|
||||
let n = mat.len();
|
||||
let mv: Vec<f64> = (0..n).map(|i| {
|
||||
(0..n).map(|j| get_entry(mat, i, j) as f64 * v[j]).sum()
|
||||
}).collect();
|
||||
let num: f64 = v.iter().zip(mv.iter()).map(|(vi, mvi)| vi * mvi).sum();
|
||||
let den: f64 = v.iter().map(|x| x * x).sum();
|
||||
if den > 0.0 { num / den } else { 0.0 }
|
||||
}
|
||||
|
||||
/// Fiedler value (smallest non-zero eigenvalue of Laplacian) via shifted inverse iteration.
|
||||
pub fn fiedler_value(mat: &IntMat) -> f64 {
|
||||
let n = mat.len();
|
||||
if n < 2 { return 0.0; }
|
||||
|
||||
let sym = symmetrize(mat, n);
|
||||
let lap = build_laplacian(&sym, n);
|
||||
|
||||
// Power iteration for dominant eigenvalue
|
||||
let lambda_max = power_iteration(&lap, 100);
|
||||
|
||||
// Shift-invert: solve (L - μI)⁻¹ where μ = lambda_max * 0.9
|
||||
// to find the smallest eigenvalue near the upper end
|
||||
let mu = lambda_max * 0.9;
|
||||
|
||||
let mut v: Vec<f64> = (0..n).map(|i| if i % 2 == 0 { 1.0 } else { -1.0 }).collect();
|
||||
|
||||
for _ in 0..50 {
|
||||
// (L - μI) × v
|
||||
let mv: Vec<f64> = (0..n).map(|i| {
|
||||
let row: f64 = (0..n).map(|j| {
|
||||
let l_ij = if i == j {
|
||||
row_sum(&lap, i, n) as f64
|
||||
} else {
|
||||
-get_entry(&lap, i, j) as f64
|
||||
};
|
||||
l_ij * v[j]
|
||||
}).sum();
|
||||
row - mu * v[i]
|
||||
}).collect();
|
||||
|
||||
// Normalize
|
||||
let norm = mv.iter().map(|x| x * x).sum::<f64>().sqrt();
|
||||
if norm < 1e-10 { break; }
|
||||
for vi in v.iter_mut() { *vi /= norm; }
|
||||
}
|
||||
|
||||
// Compute Rayleigh quotient with the converged vector
|
||||
rayleigh_quotient(&lap, &v.iter().copied().collect::<Vec<_>>())
|
||||
}
|
||||
|
||||
/// Full spectral profile for an n×n Int matrix.
|
||||
pub fn compute_profile(mat: &IntMat) -> SpectralProfile {
|
||||
let n = mat.len();
|
||||
if n == 0 {
|
||||
return SpectralProfile {
|
||||
dominant_eigenvalue: 0.0, fiedler_value: 0.0,
|
||||
spectral_gap: 0.0, condition_number: 0.0,
|
||||
};
|
||||
}
|
||||
|
||||
let sym = symmetrize(mat, n);
|
||||
let lap = build_laplacian(&sym, n);
|
||||
|
||||
let lambda_max = power_iteration(&lap, 100);
|
||||
let fv = fiedler_value(mat);
|
||||
|
||||
SpectralProfile {
|
||||
dominant_eigenvalue: lambda_max,
|
||||
fiedler_value: fv,
|
||||
spectral_gap: lambda_max - fv,
|
||||
condition_number: if fv.abs() > 1e-10 { lambda_max / fv } else { f64::INFINITY },
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
|
||||
#[test]
|
||||
fn test_isqrt() {
|
||||
assert_eq!(isqrt(0), 0);
|
||||
assert_eq!(isqrt(1), 1);
|
||||
assert_eq!(isqrt(4), 2);
|
||||
assert_eq!(isqrt(9), 3);
|
||||
assert_eq!(isqrt(16), 4);
|
||||
assert_eq!(isqrt(2), 1); // floor(√2)
|
||||
assert_eq!(isqrt(10), 3); // floor(√10)
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_symmetrize() {
|
||||
let mat: IntMat = vec![
|
||||
vec![1, 2],
|
||||
vec![3, 4],
|
||||
];
|
||||
let sym = symmetrize(&mat, 2);
|
||||
assert_eq!(sym[0][1], sym[1][0]); // symmetric
|
||||
assert_eq!(sym[0][1], (2 + 3) / 2);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_power_iteration_small() {
|
||||
// 2×2 identity → eigenvalue should be 1
|
||||
let mat: IntMat = vec![
|
||||
vec![1, 0],
|
||||
vec![0, 1],
|
||||
];
|
||||
let eig = power_iteration(&mat, 100);
|
||||
assert!((eig - 1.0).abs() < 0.1);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_spectral_profile() {
|
||||
// 3×3 matrix with known structure
|
||||
let mat: IntMat = vec![
|
||||
vec![2, 1, 0],
|
||||
vec![1, 2, 1],
|
||||
vec![0, 1, 2],
|
||||
];
|
||||
let profile = compute_profile(&mat);
|
||||
assert!(profile.dominant_eigenvalue > 0.0);
|
||||
assert!(profile.spectral_gap >= 0.0);
|
||||
}
|
||||
}
|
||||
Binary file not shown.
|
|
@ -1,8 +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 `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 `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":"7 warnings emitted","code":null,"level":"warning","spans":[],"children":[],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: 7 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.
|
|
@ -1,9 +1,10 @@
|
|||
/home/allaun/SilverSight/rust/target/debug/deps/silversight-0091d08d533221a7.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-0091d08d533221a7.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/silversight-0091d08d533221a7: 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-0091d08d533221a7: 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.
Loading…
Add table
Reference in a new issue