Skip to content

Commit bafec75

Browse files
hyperpolymathclaude
andcommitted
feat(verify): cross-compat integration suite (C5)
Adds `crates/typed-wasm-verify/tests/cross_compat.rs` — a 10-fixture integration test suite that exercises the verifier on realistic multi-function modules modelled on what affinescript's codegen (`hyperpolymath/affinescript:lib/codegen.ml`) emits for representative AffineScript source programs. Each fixture's doc comment includes: 1. The conceptual AffineScript source it represents. 2. A trace of `tw_verify.ml` / `tw_interface.ml` over the wasm structure, computing what the OCaml verifier should say. 3. The expected Rust verdict (must match the OCaml one). The assertion in each test pins the Rust verdict to that expected match. Any future change to the verifier that subtly alters its output on a realistic module fails this suite before reaching `main`. Scope decision: synthetic fixtures, not OCaml-emitted ----------------------------------------------------- The original C5 scope called for invoking `affinescript build` to produce real OCaml-emitted .wasm fixtures and asserting byte-for-byte parity. That requires a built `affinescript` binary in PATH (dune build of hyperpolymath/affinescript). The OCaml toolchain isn't currently wired into the typed-wasm CI surface, so this PR delivers the regression-net value now using wasm-encoder fixtures that emit the same byte shape affinescript produces — same `affinescript.ownership` custom section bytes, same function-index conventions, same control- flow patterns. When the OCaml-emitter integration lands (call it C5.1), these synthetic fixtures stay — they cover codegen-bug edge cases that may not appear in any AS source program — and the OCaml-emitted ones get added alongside. Fixture coverage ---------------- 1. Clean Linear consumer (`drop s`) — pass 2. Duplicated Linear (`s + s`) — LinearUsedMultiple 3. Dropped Linear in else (`if(take) drop s else ()`) — LinearDroppedOnSomePath 4. Aliased ExclBorrow (`b.len() + b.len()`) — ExclBorrowAliased 5. Multi-fn module, one clean + one duplicated — single LinearUsedMultiple on fn 1 (verifies error aggregation across functions) 6. Cross-mod: clean Linear call (`consume(s)`) — pass 7. Cross-mod: Linear called twice — LinearImportCalledMultiple 8. Cross-mod: 3 caller fns, only the last misuses — single LinearImportCalledMultiple on caller_func_idx=3 (verifies that functions which never call the import are not flagged) 9. extract_exports on a module exporting Linear + ExclBorrow + Unrestricted shapes — correct param_kinds per export 10. Realistic multi-fn clean module — pass across all four functions Builder ------- Adds an internal `ModuleBuilder` to the test file that constructs `affinescript`-shaped modules with multiple functions, imports, exports, and an `affinescript.ownership` section. Keeps each fixture ~30 lines so the conceptual source / wasm mapping stays legible. Build status ------------ $ cargo test -p typed-wasm-verify ... unit tests ... running 40 tests test result: ok. 40 passed; 0 failed; 0 ignored Running tests/cross_compat.rs running 10 tests test fixture_aliased_excl_borrow ... ok test fixture_dropped_linear_in_else ... ok test fixture_clean_linear_consumer ... ok test fixture_duplicated_linear ... ok test fixture_extract_exports_three_shapes ... ok test fixture_multi_function_one_buggy ... ok test fixture_xmod_clean_linear_call ... ok test fixture_realistic_clean_module ... ok test fixture_xmod_linear_called_twice ... ok test fixture_xmod_mixed_correctness ... ok test result: ok. 10 passed; 0 failed; 0 ignored Stacked on top of #22 (C4). Next: C6 — ephapax-wasm emits the `affinescript.ownership` custom section from linear-typed bindings, then C7 — ephapax-cli gets `--verify-ownership`. Follow-up (separate PR, future) ------------------------------- C5.1 — Once `affinescript build` is wired into typed-wasm CI: vendor real OCaml-emitted .wasm files alongside these synthetic ones; assert byte-for-byte parity in the section payload and verdict-for-verdict parity in the verifier output. Captures any drift between the two implementations after either evolves. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 parent f0dba5b commit bafec75

1 file changed

Lines changed: 680 additions & 0 deletions

File tree

0 commit comments

Comments
 (0)