From 77c47248a545063cd5885032b1b76d8ddf4aeaa2 Mon Sep 17 00:00:00 2001
From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com>
Date: Thu, 2 Jul 2026 03:38:49 +0200
Subject: [PATCH] Remove avm_ports_audit.md

---
 docs/avm_ports_audit.md | 97 -----------------------------------------
 1 file changed, 97 deletions(-)
 delete mode 100644 docs/avm_ports_audit.md

diff --git a/docs/avm_ports_audit.md b/docs/avm_ports_audit.md
deleted file mode 100644
index 51806352..00000000
--- a/docs/avm_ports_audit.md
+++ /dev/null
@@ -1,97 +0,0 @@
-# AVM ISA Ports — Cross-Implementation Audit
-
-**Date:** 2026-06-30
-**Reference:** `formal/SilverSight/AVMIsa/Step.lean` (Lean 4)
-**Ports audited:** Rust, Julia, R
-
-## 1. Critical: Integer Division Semantics (ALL PORTS)
-
-**Lean 4 uses `Int.ediv` which rounds toward NEGATIVE INFINITY (floor).**
-All three ports use truncation-toward-zero division.
-
-| Expression | Lean (ediv) | Rust/R/Julia | Impact |
-|-----------|------------|--------------|--------|
-| `(-5 * 65536) / 3` | `-109227` (floor) | `-109226` (trunc) | ❌ Off by 1 |
-| `(-1 * 65536) / 65536` | `-1` | `-1` | ✅ Same |
-| `(5 * 65536) / 3` | `109226` | `109226` | ✅ Same |
-| `(5 * 65536) / -3` | `-109227` | `-109226` | ❌ Off by 1 |
-
-**Fix:** All ports must match Lean's floor division for negative values.
-
-The Q16_16 multiplication `(a * b) / 65536` only differs when `(a*b)` is negative
-and not evenly divisible by 65536 — a 1-LSB error in the fractional part. While
-small, this breaks the determinism contract.
-
-## 2. Rust port (`rust/src/avm/mod.rs`)
-
-| Issue | Severity | Detail |
-|-------|----------|--------|
-| Division semantics | **HIGH** | Uses truncation, not floor |
-| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` instead of V6 sign-decomposition (functionally equivalent for the symmetric range `[-2147483647, 2147483647]`, but deviates from spec) |
-| Q16_16 clamp range | **MEDIUM** | Uses `INT32_MIN`/`INT32_MAX` instead of symmetric `[-2147483647, 2147483647]` |
-| Q0_16 clamp range | **MEDIUM** | Uses `[-32768, 32767]` instead of `[-32767, 32767]` |
-| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` check |
-| No StackOverflow error | **MEDIUM** | Missing error variant |
-| Q0_16 `Not` operator | **LOW** | Using a simplified version; Lean has no Q0_16 Not |
-
-### Good:
-- Tagged union types (faithful to Lean)
-- Result-based error handling
-- Fuel-bounded run loop
-- Proper test coverage
-
-## 3. Julia port (`julia/AVMIsa/avm.jl`)
-
-| Issue | Severity | Detail |
-|-------|----------|--------|
-| Division semantics | **HIGH** | Uses truncation, not floor |
-| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
-| Q16_16 clamp range | **MEDIUM** | Uses `typemin(Int32)` = `-2147483648` instead of `-2147483647` |
-| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type with saturated add/sub |
-| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
-| No StackOverflow error | **MEDIUM** | Missing error variant |
-| Error handling via exceptions | **LOW** | Uses `error()` instead of Result types — loses functional purity |
-| Instr encoding | **LOW** | Uses flat opcode + arg scheme instead of tagged union; fragile |
-
-### Good:
-- Delegates to `Q16_16.q_mul`/`q_div` for correct Q16_16 arithmetic
-- Fuel-bounded run loop
-
-## 4. R port (`r/AVMIsa/avm.r`)
-
-| Issue | Severity | Detail |
-|-------|----------|--------|
-| Division semantics | **HIGH** | Uses `round()` NOT integer truncation; different from both Lean and truncation |
-| Signed comparison (ltQ16) | **MEDIUM** | Uses raw `<` (functionally equivalent for symmetric range) |
-| Q16_16 clamp range | **MEDIUM** | Uses `-2147483648` instead of `-2147483647` |
-| Multiplication rounding | **MEDIUM** | Uses `round()` not integer division — gives different results |
-| `as.integer()` overflow | **MEDIUM** | Silently produces NA for out-of-range values |
-| Missing Q0_16 support | **HIGH** | Lean has `q0_16` type |
-| No stack depth limit | **MEDIUM** | Missing `maxStackDepth = 1024` |
-| No StackOverflow error | **MEDIUM** | Missing error variant |
-
-### Good:
-- Functional style (pure step function)
-- Fuel-bounded run loop
-- Runtime type checking on primitives
-
-## 5. Summary
-
-| Issue | Rust | Julia | R |
-|-------|------|-------|---|
-| Division = floor (Lean ediv) | ❌ | ❌ | ❌ |
-| Signed comparison (V6) | ❌ | ❌ | ❌ |
-| Symmetric Q16_16 clamp | ❌ | ❌ | ❌ |
-| Q0_16 support | ⚠️ | ❌ | ❌ |
-| Stack depth limit | ❌ | ❌ | ❌ |
-| StackOverflow error | ❌ | ❌ | ❌ |
-
-**No port is fully compliant with the Lean reference.** All three have the same
-three systemic issues: division rounding, comparison algorithm, and clamp range.
-
-The floor-vs-truncation issue is the most dangerous — it's a silent 1-LSB error
-on negative values that will accumulate across multiple operations.
-
-Recommendation: fix the division semantics in all three ports first, then the
-comparison and clamp issues. These are all small patches; the port structure
-itself is sound.