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

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

diff --git a/docs/avm_isa_audit.md b/docs/avm_isa_audit.md
deleted file mode 100644
index 45752c03..00000000
--- a/docs/avm_isa_audit.md
+++ /dev/null
@@ -1,111 +0,0 @@
-# AVM ISA v1 — Wolfram Alpha Audit Report
-
-**Date:** 2026-06-30
-**Tool:** Wolfram Alpha API (appid: HYJE3R3R63)
-**Target:** `SilverSight/formal/SilverSight/AVMIsa/`
-
-## 1. Type Universe
-| Property | Result |
-|----------|--------|
-| Finite types: `q0_16`, `q16_16`, `bool` | Closed-world; verified complete |
-| No Float | Compliant |
-
-## 2. Q16_16 Arithmetic (Step.lean)
-
-### 2.1 Clamping (`ofAvmRaw`)
-```
-Clamp range: [-2147483647, 2147483647]
-```
-Wolfram: `INT32_MAX = 2147483647` ✅  
-Range is **symmetric**: `INT32_MIN = -2147483648` is excluded. This ensures:
-
-**Theorem: negation is a perfect involution**
-```
-For all x in [-2147483647, 2147483647]: -(-x) = x
-```
-Wolfram: **True** ✅
-
-Without this design, `neg(INT32_MIN) = INT32_MIN` would break the involution.
-
-### 2.2 Saturated Addition (`addSatQ16`)
-```
-result = clamp(y + x)  where clamp(v) = min(2147483647, max(-2147483647, v))
-```
-Wolfram: `min(2147483647, max(-2147483647, 2147483645 + 10)) = 2147483647` ✅  
-Saturates correctly; overflow → max bound.
-
-### 2.3 Saturated Subtraction (`subSatQ16`)
-```
-result = clamp(y - x)  where clamp(v) = min(2147483647, max(-2147483647, v))
-```
-Structural equivalent to add with negated operand.
-
-### 2.4 Saturated Multiplication (`mulSatQ16`)
-```
-result = clamp((y * x) / 65536)
-```
-Wolfram: `(2147483647)^2 / 65536 = 70368744112128 1/65536` (≈ 7.04×10¹³)  
-Clamped to `2147483647` ✅
-
-### 2.5 Saturated Division (`divSatQ16`)
-```
-if x = 0 → divisionByZero error
-else result = clamp((y * 65536) / x)
-```
-Wolfram: `(5 × 65536) / 2 = 163840` (→ 2.5 in Q16_16) ✅  
-Wolfram: `(-5 × 65536) / 2 = -163840` (→ -2.5 in Q16_16) ✅
-
-### 2.6 Signed Comparison (`ltQ16`) — V6 algorithm
-```
-signA = (a < 0), signB = (b < 0)
-if signA != signB → signA        (different signs → negative is less)
-else → a < b                      (same sign → numeric compare)
-```
-Verified test cases:
-| Expression | Expected | Result |
-|-----------|----------|--------|
-| `-5 < -3` | True | True ✅ |
-| `-3 < 5` | True | True ✅ |
-| `5 < -3` | False | False ✅ |
-| `7 < 7` | False | False ✅ |
-| `-7 < -5` | True | True ✅ |
-| `-5 < -7` | False | False ✅ |
-
-### 2.7 Equality (`eqQ16`)
-```
-result = (y.val == x.val)
-```
-Structural: compares raw Q16_16 values. No Wolfram verification needed.
-
-## 3. Q0_16 Arithmetic
-### 3.1 Clamping (`ofAvmRawQ0`)
-```
-Clamp range: [-32767, 32767]
-```
-Symmetric: `Q0_16` min value `-32768` excluded to preserve negation involution.  
-Wolfram: `32767` is standard Q0_16 max ✅
-
-## 4. Stack Safety (V7 mitigations)
-| Property | Value | Wolfram |
-|----------|-------|---------|
-| `maxStackDepth` | 1024 | — |
-| Max memory (worst case) | 1024 × ~12 bytes = 12.29 kB | ✅ Wolfram verified |
-
-## 5. Scaling Constant
-```
-65536 = 2^16
-```
-Wolfram: **True** ✅
-
-## 6. Known Gaps (not Wolfram-verifiable)
-1. **Type safety** — requires Lean proof, not arithmetic
-2. **Program termination** — requires fuel argument, not arithmetic
-3. **Correctness of Q16_16 rounding** — Lean `native_decide` verification needed
-4. **Stack depth bound interaction** — structural property, not arithmetic
-
-## 7. Conclusion
-
-All AVM ISA arithmetic properties audited by Wolfram Alpha. No arithmetic errors found.
-
-The symmetric clamping design (`-2147483647` instead of `-2147483648`) is the correct
-choice — verified by Wolfram that negation is a perfect involution over the full range.