SilverSight/docs/avm_ports_audit.md

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.