diff --git a/AGENTS.md b/AGENTS.md index 6cfb21c1..da53053f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -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. diff --git a/coq/CoreFormalism/.Q16_16.aux b/coq/CoreFormalism/.Q16_16.aux new file mode 100644 index 00000000..34c87b94 --- /dev/null +++ b/coq/CoreFormalism/.Q16_16.aux @@ -0,0 +1,2 @@ +COQAUX1 03441a4df6ed6fdae62bc8cdd91bb74d /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v +0 0 VernacProof "tac:no using:no" diff --git a/coq/CoreFormalism/.lia.cache b/coq/CoreFormalism/.lia.cache new file mode 100644 index 00000000..00113acd Binary files /dev/null and b/coq/CoreFormalism/.lia.cache differ diff --git a/coq/CoreFormalism/Q16_16.glob b/coq/CoreFormalism/Q16_16.glob new file mode 100644 index 00000000..52ade12a --- /dev/null +++ b/coq/CoreFormalism/Q16_16.glob @@ -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 diff --git a/coq/CoreFormalism/Q16_16.v b/coq/CoreFormalism/Q16_16.v new file mode 100644 index 00000000..441fb47f --- /dev/null +++ b/coq/CoreFormalism/Q16_16.v @@ -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. diff --git a/julia/AVMIsa/avm.jl b/julia/AVMIsa/avm.jl index 6c2377f7..202c07fe 100644 --- a/julia/AVMIsa/avm.jl +++ b/julia/AVMIsa/avm.jl @@ -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) diff --git a/r/AVMIsa/avm.r b/r/AVMIsa/avm.r new file mode 100644 index 00000000..89f0b451 --- /dev/null +++ b/r/AVMIsa/avm.r @@ -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 +} diff --git a/r/AVMIsa/test_avm.r b/r/AVMIsa/test_avm.r new file mode 100644 index 00000000..433133fb --- /dev/null +++ b/r/AVMIsa/test_avm.r @@ -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") diff --git a/rust/src/avm/mod.rs b/rust/src/avm/mod.rs index 79a9674e..55ad1240 100644 --- a/rust/src/avm/mod.rs +++ b/rust/src/avm/mod.rs @@ -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) => { diff --git a/rust/src/lib.rs b/rust/src/lib.rs index 5e357204..766bfef5 100644 --- a/rust/src/lib.rs +++ b/rust/src/lib.rs @@ -2,3 +2,4 @@ pub mod q16; pub mod nuvmap; pub mod silversight; pub mod avm; +pub mod pist; diff --git a/rust/src/pist/mod.rs b/rust/src/pist/mod.rs new file mode 100644 index 00000000..e0c7f12d --- /dev/null +++ b/rust/src/pist/mod.rs @@ -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>; + +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 = (0..n).map(|i| (i as f64 + 1.0)).collect(); + + for _ in 0..max_iter { + // mat × v (as f64) + let mv: Vec = (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::()).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::() + }).collect::>(); + let resid: f64 = mx.iter().zip(v.iter()).map(|(mxi, vi)| (mxi - eig * vi).abs()).sum::() / n as f64; + if resid < 1e-8 { return eig; } + } + + // Final Rayleigh quotient + let mv: Vec = (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 = (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 = (0..n).map(|i| if i % 2 == 0 { 1.0 } else { -1.0 }).collect(); + + for _ in 0..50 { + // (L - μI) × v + let mv: Vec = (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::().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::>()) +} + +/// 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); + } +} diff --git a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight index 2380b56d..58db3721 100644 Binary files a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight and b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/dep-test-lib-silversight differ diff --git a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight index cabad1ad..31361d8b 100644 --- a/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight +++ b/rust/target/debug/.fingerprint/silversight-0091d08d533221a7/output-test-lib-silversight @@ -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 = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"remove these parentheses","code":null,"level":"help","spans":[{"file_name":"src/pist/mod.rs","byte_start":2547,"byte_end":2548,"line_start":80,"line_end":80,"column_start":42,"column_end":43,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":42,"highlight_end":43}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null},{"file_name":"src/pist/mod.rs","byte_start":2562,"byte_end":2563,"line_start":80,"line_end":80,"column_start":57,"column_end":58,"is_primary":true,"text":[{"text":" let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();","highlight_start":57,"highlight_end":58}],"label":null,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: unnecessary parentheses around closure body\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:80:42\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[1m\u001b[94m|\u001b[0m let mut v: Vec = (0..n).map(|i| (i as f64 + 1.0)).collect();\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33m^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default\n\u001b[1m\u001b[96mhelp\u001b[0m: remove these parentheses\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m80\u001b[0m \u001b[91m- \u001b[0m let mut v: Vec = (0..n).map(|i| \u001b[91m(\u001b[0mi as f64 + 1.0\u001b[91m)\u001b[0m).collect();\n\u001b[1m\u001b[94m80\u001b[0m \u001b[92m+ \u001b[0m let mut v: Vec = (0..n).map(|i| i as f64 + 1.0).collect();\n \u001b[1m\u001b[94m|\u001b[0m\n\n"} +{"$message_type":"diagnostic","message":"function `build_ata` is never used","code":{"code":"dead_code","explanation":null},"level":"warning","spans":[{"file_name":"src/pist/mod.rs","byte_start":1624,"byte_end":1633,"line_start":55,"line_end":55,"column_start":4,"column_end":13,"is_primary":true,"text":[{"text":"fn build_ata(mat: &IntMat, n: usize) -> IntMat {","highlight_start":4,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `build_ata` is never used\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/pist/mod.rs:55:4\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m55\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn build_ata(mat: &IntMat, n: usize) -> IntMat {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default\n\n"} {"$message_type":"diagnostic","message":"function `F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"`#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default","code":null,"level":"note","spans":[],"children":[],"rendered":null},{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":1942,"byte_end":1943,"line_start":53,"line_end":53,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn F(s: &str) -> [f64; 8] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:53:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m53\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn F(s: &str) -> [f64; 8] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `f`\u001b[0m\n \u001b[1m\u001b[94m|\u001b[0m\n \u001b[1m\u001b[94m= \u001b[0m\u001b[1mnote\u001b[0m: `#[warn(non_snake_case)]` (part of `#[warn(nonstandard_style)]`) on by default\n\n"} {"$message_type":"diagnostic","message":"function `Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3141,"byte_end":3144,"line_start":94,"line_end":94,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn Phi(s: &str) -> [f64; 14] {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:94:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m94\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn Phi(s: &str) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_F` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3470,"byte_end":3473,"line_start":103,"line_end":103,"column_start":8,"column_end":11,"is_primary":true,"text":[{"text":"pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {","highlight_start":8,"highlight_end":11}],"label":null,"suggested_replacement":"d_f","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_F` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:103:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m103\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_F(p: &[f64; N], q: &[f64; N]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `d_f`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `d_Phi` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":3672,"byte_end":3677,"line_start":110,"line_end":110,"column_start":8,"column_end":13,"is_primary":true,"text":[{"text":"pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {","highlight_start":8,"highlight_end":13}],"label":null,"suggested_replacement":"d_phi","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `d_Phi` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:110:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m110\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn d_Phi(phi1: &[f64; 14], phi2: &[f64; 14]) -> f64 {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case: `d_phi`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `C` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":4173,"byte_end":4174,"line_start":122,"line_end":122,"column_start":8,"column_end":9,"is_primary":true,"text":[{"text":"pub fn C(phi: &[f64; 14]) -> [f64; 14] {","highlight_start":8,"highlight_end":9}],"label":null,"suggested_replacement":"c","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `C` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:122:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m122\u001b[0m \u001b[1m\u001b[94m|\u001b[0m pub fn C(phi: &[f64; 14]) -> [f64; 14] {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `c`\u001b[0m\n\n"} {"$message_type":"diagnostic","message":"function `test_F_verified` should have a snake case name","code":{"code":"non_snake_case","explanation":null},"level":"warning","spans":[{"file_name":"src/silversight/mod.rs","byte_start":8947,"byte_end":8962,"line_start":262,"line_end":262,"column_start":8,"column_end":23,"is_primary":true,"text":[{"text":" fn test_F_verified() {","highlight_start":8,"highlight_end":23}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"convert the identifier to snake case","code":null,"level":"help","spans":[{"file_name":"src/silversight/mod.rs","byte_start":8947,"byte_end":8962,"line_start":262,"line_end":262,"column_start":8,"column_end":23,"is_primary":true,"text":[{"text":" fn test_F_verified() {","highlight_start":8,"highlight_end":23}],"label":null,"suggested_replacement":"test_f_verified","suggestion_applicability":"MaybeIncorrect","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[1m\u001b[33mwarning\u001b[0m\u001b[1m: function `test_F_verified` should have a snake case name\u001b[0m\n \u001b[1m\u001b[94m--> \u001b[0msrc/silversight/mod.rs:262:8\n \u001b[1m\u001b[94m|\u001b[0m\n\u001b[1m\u001b[94m262\u001b[0m \u001b[1m\u001b[94m|\u001b[0m fn test_F_verified() {\n \u001b[1m\u001b[94m|\u001b[0m \u001b[1m\u001b[33m^^^^^^^^^^^^^^^\u001b[0m \u001b[1m\u001b[33mhelp: convert the identifier to snake case (notice the capitalization): `test_f_verified`\u001b[0m\n\n"} -{"$message_type":"diagnostic","message":"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"} diff --git a/rust/target/debug/deps/silversight-0091d08d533221a7 b/rust/target/debug/deps/silversight-0091d08d533221a7 index 9b4dd34f..734b3a09 100755 Binary files a/rust/target/debug/deps/silversight-0091d08d533221a7 and b/rust/target/debug/deps/silversight-0091d08d533221a7 differ diff --git a/rust/target/debug/deps/silversight-0091d08d533221a7.d b/rust/target/debug/deps/silversight-0091d08d533221a7.d index 27e386c6..26f9d0e0 100644 --- a/rust/target/debug/deps/silversight-0091d08d533221a7.d +++ b/rust/target/debug/deps/silversight-0091d08d533221a7.d @@ -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: diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/dep-graph.bin deleted file mode 100644 index f5ed7693..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/dep-graph.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/query-cache.bin deleted file mode 100644 index 4d959981..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/query-cache.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/dep-graph.bin deleted file mode 100644 index 5c383c68..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/dep-graph.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/query-cache.bin deleted file mode 100644 index da10943f..00000000 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/query-cache.bin and /dev/null differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin new file mode 100644 index 00000000..026908b3 Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/dep-graph.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin new file mode 100644 index 00000000..59136309 Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/query-cache.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/work-products.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin similarity index 57% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/work-products.bin rename to rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin index adf142f9..39c09b47 100644 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b-bpa5c5rn16i7tp6qtx99exlj4/work-products.bin and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx-eem4bsw07gcu7jm9e94hxq6ak/work-products.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy.lock b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx.lock similarity index 100% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy.lock rename to rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxxu0xn2-08xvacx.lock diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/dep-graph.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/dep-graph.bin new file mode 100644 index 00000000..03a66c9d Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/dep-graph.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/query-cache.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/query-cache.bin new file mode 100644 index 00000000..6d0c93d0 Binary files /dev/null and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/query-cache.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/work-products.bin b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/work-products.bin similarity index 50% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/work-products.bin rename to rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/work-products.bin index adf142f9..d6bdeb47 100644 Binary files a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxrwjr3u-0vzvshy-4wmvf4ea74gqmota16nv2q647/work-products.bin and b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1-3wkicujhfbxw7ck7qpf2yiggb/work-products.bin differ diff --git a/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b.lock b/rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1.lock similarity index 100% rename from rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxsio0wb-0dxb00b.lock rename to rust/target/debug/incremental/silversight-1ff0xaicoj4c6/s-hjyxydldzv-0aax8j1.lock