4 commits

Author	SHA1	Message	Date
allaun	069e54d8e9	fix(coq): migrate all files to Rocq 9.0 imports (ZCompat, no ZArith) ... All 5 Coq files now use: From Corelib Require Import BinNums PosDef NatDef IntDef. Require Import SilverSight.coq.ZCompat. instead of Require Import ZArith Lia. Build: 5 Coq files, 0 errors	2026-07-01 23:21:29 -05:00
allaun	c7c7809ffb	feat(tests): add Coq test harness, milestone: 12/12 ports have tests	2026-06-30 17:59:38 -05:00
allaun	f6cbddcbf2	feat(tests): Python AVM port rewrite + test harness, Go test harness ... Python port rewritten to match spec: - Added Q0_16, PUSH_Q0, PUSH_BOOL as separate opcodes - Added V6 comparison (lt_q16_v6) - Added floor division (Lean Int.ediv) - Added stack depth limit (AVM_MAX_STACK = 1024) - Added type checking in exec_prim - All 10 tests passing Go AVM port: added test_avm_test.go with 8 test cases Milestone: Python → ✅, Go → 🔄	2026-06-30 17:56:09 -05:00
allaun	863da04f21	feat(avm-ports): port AVM ISA to all 12 scientific languages ... Lean (reference), Python, Rust, C, C++, Go, Julia, R, Scala, Fortran, Coq, Octave — all implementing the same AVM ISA v1 specification. Every port implements: - Full type universe: Q0_16, Q16_16, Bool - 11 primitives with floor division (Lean Int.ediv), V6 signed comparison, symmetric clamping [-2147483647, 2147483647] - 12 instruction opcodes with stack depth limit (1024) - Fuel-bounded run loop - Error handling (stack under/overflow, type mismatch, div-by-zero, jump OOB)	2026-06-30 17:42:38 -05:00