Commit 67006ed
feat(verify): cross-compat integration suite (C5) (#23)
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 3e9d4bc commit 67006ed
1 file changed
Lines changed: 680 additions & 0 deletions
0 commit comments