# AVMIsa Manual Math Audit — Vulnerability Report

This report walks through every arithmetic path in the AVM ISA step-by-step,
identifies how each can go wrong, and proposes concrete mitigations.

---

## Source Files Under Audit

| File | Role |
|------|------|
| [FixedPoint.lean](file:///home/allaun/SilverSight/Core/SilverSight/FixedPoint.lean) | Q16_16 type definition + arithmetic kernels |
| [Step.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Step.lean) | AVM instruction semantics |
| [State.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/State.lean) | Machine state (stack, locals, pc) |
| [Run.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Run.lean) | Fuel-bounded execution loop |

---

## §1 — Arithmetic Vulnerability Surfaces

### V1. Multiplication Intermediate Overflow ⚠️ CRITICAL

**Definition:**
```lean
def mul (a b : Q16_16) : Q16_16 := ofRawInt ((a.toInt * b.toInt) / q16Scale)
```

**The problem:** `a.toInt` and `b.toInt` are both in $[-2^{31}, 2^{31}-1]$.
Their product can reach $2^{62}$, which is fine in Lean (arbitrary-precision `Int`),
but **any backend using 32-bit integers will silently overflow**.

**Worked example:**
- $a = 32767.0$ (raw $2147418112$), $b = 2.0$ (raw $131072$)
- Intermediate: $2147418112 \times 131072 = 2.81 \times 10^{17}$ → overflows `int32`
- Even `int64` handles this, but a 32-bit C/Verilog backend will produce garbage

**Mitigation:**
1. **Backend spec rule:** All AVM backends MUST use ≥ 64-bit intermediate storage for `mul` and `div`
2. **Lean-side:** Add a `#eval` witness confirming the worst-case product fits in `Int64`:
   ```lean
   #eval (q16MaxRaw * q16MaxRaw) -- should be ≤ 2^62, fits Int64
   ```

---

### V2. Division Intermediate Overflow ⚠️ CRITICAL

**Definition:**
```lean
def div (a b : Q16_16) : Q16_16 :=
  if b.toInt = 0 then infinity else ofRawInt ((a.toInt * q16Scale) / b.toInt)
```

**The problem:** `a.toInt * 65536` can reach $2^{31} \times 2^{16} = 2^{47}$,
which overflows `int32` but fits `int64`.

**Worked example:**
- $a = \text{maxVal}$ (raw $2147483647$), $b = 1.0$ (raw $65536$)
- Intermediate: $2147483647 \times 65536 = 1.407 \times 10^{14}$ → overflows `int32`

**Mitigation:** Same as V1 — mandate 64-bit intermediates for all backends.

---

### V3. Division by Zero Sentinel ⚠️ MEDIUM

**Definition:** `div(a, 0)` returns `infinity` (which is `maxVal = 2147483647`).

**The problem:** This is a **silent sentinel** — the caller cannot distinguish
"the result was legitimately very large" from "division by zero occurred."
In a bidirectional encoding pipeline, this could silently corrupt a DNA sequence
if a zero denominator arises from a degenerate AST.

**Mitigation options (pick one):**
1. **Add a `StepError.divisionByZero`** error variant and make `divSatQ16` return
   `Outcome.err StepError.divisionByZero` instead of a sentinel value
2. **Add a `Prim.isDivSafe`** instruction that pushes `true` if TOS ≠ 0, allowing
   programs to guard division explicitly
3. **Accept the sentinel** but document it as a backend invariant and add a
   `#eval` witness confirming `div maxVal zero = maxVal`

> [!IMPORTANT]
> Option 1 is the most rigid but changes the `Outcome` contract.
> Option 2 preserves totality while giving programs the ability to guard.

---

### V4. Rounding Direction Mismatch ⚠️ CRITICAL (Cross-Platform)

**Lean's integer division:** Truncation toward zero (same as C99 `/`).
- $-7 / 2 = -3$ (truncates toward zero)

**Python's `//` operator:** Floor division (rounds toward $-\infty$).
- $-7 // 2 = -4$ (floors)

**Impact on `mul`:**
- $a = -1$ (raw $-65536$), $b = 0.5$ (raw $32768$)
- Lean: $(-65536 \times 32768) / 65536 = -2147483648 / 65536 = -32768$ (truncation)
- Python: $(-65536 \times 32768) // 65536 = -32768$ (same here, but...)

- $a$ raw $= -3$, $b$ raw $= 2$:
- Lean: $(-3 \times 2) / 65536 = -6 / 65536 = 0$ (truncates toward zero)
- Python: $(-6) // 65536 = -1$ (floors toward $-\infty$)
- **Result differs by 1 LSB** → DNA sequence divergence

**Mitigation:**
1. **BioSight Python shim MUST use `int(x / y)` (truncation) instead of `x // y` (floor)**
   for all Q16_16 operations
2. Add a cross-platform conformance test: compute `mul(ofRawInt(-3), ofRawInt(2))`
   in both Lean and Python and assert identical raw values

---

### V5. Saturation Asymmetry ⚠️ LOW

**Range:** $[-2147483648, 2147483647]$ — the negative range has 1 more value than
the positive range. This means:
- `neg(minVal)` = `ofRawInt(2147483648)` → saturates to `maxVal` ($2147483647$)
- So `neg(neg(minVal)) ≠ minVal` — negation is not an involution at the boundary

**Impact:** For bidirectional encoding, if a DNA base encodes `minVal` and the
decoder negates twice, it will get `maxVal - 1` instead. This is a 1-LSB error
at the extreme boundary.

**Mitigation:**
1. Document this as a known boundary: the extreme negative value $-2^{31}$ is
   outside the invertible range
2. Restrict the encoding domain to $[-2^{31}+1, 2^{31}-1]$ so negation is always invertible

---

### V6. Comparison Signedness ⚠️ LOW

**`ltQ16` in Step.lean:**
```lean
let res := y.toInt < x.toInt
```

This uses `Int` comparison which is correct for signed Q16_16. However, if a
backend implements this using unsigned comparison on the raw bits, large negative
values would appear positive and comparisons would be inverted.

**Mitigation:** Backend spec must state: "All Q16_16 comparisons use **signed**
integer comparison on the raw representation."

---

## §2 — Execution & Memory Vulnerability Surfaces

### V7. Unbounded Stack Growth ⚠️ MEDIUM

**State definition:**
```lean
structure State where
  pc : Nat
  stack : List AnyVal
  locals : List (Option AnyVal)
  halted : Bool
```

The stack is an unbounded `List`. A malicious or buggy program could push
indefinitely (e.g., `push; jump 0` loop), consuming unbounded memory before
fuel runs out.

**Worst case:** With fuel $= N$, the stack can grow to depth $N$ values
($N \times 12$ bytes for the tag+payload). At fuel $= 2^{20}$, that's ~12 MB.

**Mitigation:**
1. Add a `maxStackDepth : Nat` field to `State` and check it on every `push`
2. Add a new `StepError.stackOverflow` variant
3. Or: accept fuel as the implicit bound and document the relationship
   $\text{max\_stack} \leq \text{fuel}$

---

### V8. Local Frame Silent No-Op on Out-of-Bounds Store ⚠️ MEDIUM

**`setLocal` definition:**
```lean
def setLocal (s : State) (i : Nat) (v : AnyVal) : State :=
  if i < s.locals.length then
    { s with locals := s.locals.set i (some v) }
  else
    s  -- silent no-op!
```

If `i ≥ locals.length`, the store is silently dropped. The program continues
with stale data, which could lead to incorrect DNA encodings without any error signal.

**Mitigation:**
1. Return `Outcome.err StepError.missingLocal` on out-of-bounds store (matching
   the behavior of `load`, which already returns `missingLocal`)
2. Or: pre-allocate the local frame to a fixed size at program start

---

## §3 — Summary Matrix

| ID | Surface | Severity | Status |
|----|---------|----------|--------|
| V1 | mul intermediate overflow (32-bit backends) | 🔴 Critical | Open |
| V2 | div intermediate overflow (32-bit backends) | 🔴 Critical | Open |
| V3 | div-by-zero returns silent sentinel | 🟡 Medium | Open |
| V4 | Rounding direction mismatch (Lean vs Python) | 🔴 Critical | Open |
| V5 | Negation non-involution at minVal boundary | 🟢 Low | Documented |
| V6 | Comparison signedness in backends | 🟢 Low | Documented |
| V7 | Unbounded stack growth | 🟡 Medium | Open |
| V8 | Silent no-op on out-of-bounds store | 🟡 Medium | Open |

## §4 — Recommended Priority Order

1. **V4 (Rounding)** — Fix the Python shim first. This is the most likely source
   of real DNA sequence divergence between Lean and Python today.
2. **V1/V2 (Overflow)** — Add 64-bit mandate to backend spec + `#eval` witnesses.
3. **V8 (Silent store)** — Change `setLocal` to error on out-of-bounds.
4. **V3 (Div-by-zero)** — Add `isDivSafe` guard primitive or error variant.
5. **V7 (Stack growth)** — Add stack depth limit or accept fuel as bound.
6. **V5/V6** — Document as known boundaries.