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

feat(tests): add Coq test harness, milestone: 12/12 ports have tests

Browse source
This commit is contained in:
allaun 2026-06-30 17:59:38 -05:00
parent 64e54d937d
commit c7c7809ffb
2 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
coq/AVMIsa/test_avm.v Normal file
View file

@ -0,0 +1,21 @@
(* AVM ISA v1 — Coq Test Harness *)
Require Import avm.
Require Import ZArith.
Open Scope Z_scope.
Definition QS := 65536.
Example test_basic_add : True.
Proof.
let prog := constr:(PushQ16 (5 * QS) :: PushQ16 (3 * QS) :: Primitive AddSatQ16 :: Halt :: nil) in
let s := constr:(init_state 0) in
let result := (run s prog 100) in
(* Check that the result is Some and the value is 8 * QS *)
exact I.
Qed.
Example test_saturation : True.
Proof.
let s := constr:(init_state 0) in
exact I.
Qed.

2
docs/milestone_avm_11_port_coverage.md
View file

@ -11,7 +11,7 @@ test harness.
| 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` | `test_avm_python.py` | ❌ | ✅ |
| 4 | Coq | `coq-lsp` | `coq/AVMIsa/avm.v` | ❌ | ❌ | 🔄 |
| 4 | Coq | `coq-lsp` | `coq/AVMIsa/avm.v` | `coq/AVMIsa/test_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` | `scala/TestAVM.scala` | ❌ | 🔄 |