From 56b734cbc3c3aa74a61c797f75569437b0733901 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 30 Jun 2026 17:50:02 -0500
Subject: [PATCH] docs: add milestone for AVM ISA 1:1 port coverage across all
 LSP languages

---
 docs/milestone_avm_11_port_coverage.md | 62 ++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 docs/milestone_avm_11_port_coverage.md

diff --git a/docs/milestone_avm_11_port_coverage.md b/docs/milestone_avm_11_port_coverage.md
new file mode 100644
index 00000000..6d2abba5
--- /dev/null
+++ b/docs/milestone_avm_11_port_coverage.md
@@ -0,0 +1,62 @@
+# Milestone: AVM ISA 1:1 Port Coverage
+
+**Goal:** Every language with an LSP installed on the build infrastructure
+must have a complete, Lean-validated AVM ISA v1 port with cross-implementation
+test harness.
+
+## Coverage Matrix
+
+| # | Language | LSP | AVM Port | Tests | Wolfram Validated | Status |
+|---|----------|-----|----------|-------|-------------------|--------|
+| 1 | Lean | `lean --server` | `formal/SilverSight/AVMIsa/` | `E2E.lean` | ✅ | **Reference** |
+| 2 | Rust | `rust-analyzer` | `rust/src/avm/mod.rs` | `test_add_q16` | ✅ | ✅ |
+| 3 | Python | `pyright` | `python/avm.py` | ❌ | ❌ | 🔄 |
+| 4 | Coq | `coq-lsp` | `coq/AVMIsa/avm.v` | ❌ | ❌ | 🔄 |
+| 5 | R | — | `r/AVMIsa/avm.r` | `test_avm.r` | ✅ | ✅ |
+| 6 | Julia | — | `julia/AVMIsa/avm.jl` | `test_avm.jl` | ✅ | ✅ |
+| 7 | Scala | `metals` | `scala/avm.scala` | ❌ | ❌ | 🔄 |
+| 8 | Go | — | `go/avm.go` | ❌ | ❌ | 🔄 |
+| 9 | C | `clangd` | `c/avm.c` | ❌ | ❌ | 🔄 |
+| 10 | C++ | `clangd` | `cpp/avm.hpp` | ❌ | ❌ | 🔄 |
+| 11 | Fortran | `fortls` | `fortran/avm.f90` | ❌ | ❌ | 🔄 |
+| 12 | Octave | — | `octave/avm.m` | ❌ | ❌ | 🔄 |
+
+## 1:1 Verification Protocol
+
+For each port, run the same test vector through every implementation:
+
+```python
+test_vector = [
+    # (op, a, b, expected_q16)
+    ("add", 5*65536, 3*65536, 8*65536),         # 5 + 3 = 8
+    ("sub", 10*65536, 3*65536, 7*65536),         # 10 - 3 = 7
+    ("mul", 5*65536, 3*65536, 15*65536),          # 5 * 3 = 15
+    ("div", 10*65536, 2*65536, 5*65536),          # 10 / 2 = 5
+    ("lt",  5*65536, 3*65536, False),             # 5 < 3 = false
+    ("lt",  -5*65536, -3*65536, True),            # -5 < -3 = true
+    ("add_sat", cload_max-1, 2, cload_max),       # saturation
+    ("div_neg", -5*65536, 3*65536, -1*65536),     # floor division: -5/3 = -2
+]
+```
+
+All results must match Lean `#eval` witnesses to pass.
+
+## Action Items
+
+1. **Python** — Write `tests/test_avm_python.py` with Lean-cross-validated test vector
+2. **Coq** — Write `coq/AVMIsa/test_avm.v` with `Example` witnesses
+3. **Scala** — Write test harness in `scala/src/test/`
+4. **Go** — Write `go/avm_test.go`
+5. **C** — Write `c/test_avm.c`
+6. **C++** — Write `cpp/test_avm.cpp`
+7. **Fortran** — Write `fortran/test_avm.f90`
+8. **Octave** — Write `octave/test_avm.m`
+9. **CI** — Add a GitHub Actions workflow that runs all port tests on every push
+10. **Wolfram Alpha** — Re-audit all ports against the Lean reference
+
+## Definition of Done
+
+- [ ] All 12 ports pass the same cross-validated test vector
+- [ ] Test outputs match Lean `#eval` witnesses for every operation
+- [ ] CI pipeline runs all port tests on push
+- [ ] Audit report (`docs/avm_ports_audit.md`) updated with "1:1" status