allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Remove avm_isa_audit.md

Browse source
This commit is contained in:
Allaun Silverfox 2026-07-02 03:38:36 +02:00
parent cac5534d57
commit 9772cb99a8
1 changed files with 0 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

111
docs/avm_isa_audit.md
View file

@ -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.