Skip to content

feat(verify): cross-compat integration suite (C5)#23

Merged
hyperpolymath merged 1 commit into
mainfrom
feat/typed-wasm-verify-c5-cross-compat
May 15, 2026
Merged

feat(verify): cross-compat integration suite (C5)#23
hyperpolymath merged 1 commit into
mainfrom
feat/typed-wasm-verify-c5-cross-compat

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

  • Adds crates/typed-wasm-verify/tests/cross_compat.rs — a 10-fixture integration test suite.
  • Each fixture models a representative AffineScript source program through the wasm shape that affinescript's codegen would emit.
  • Each fixture's doc comment includes the conceptual AffineScript source, a hand-trace of the OCaml verifier (tw_verify.ml / tw_interface.ml) over the wasm structure, and the expected verdict.
  • 50/50 tests pass (40 unit + 10 new integration).

Why this design

Original C5 scope was "drive affinescript build to produce real OCaml-emitted .wasm files, compare verdicts byte-for-byte." That requires a built affinescript binary in PATH (dune build of hyperpolymath/affinescript), which isn't currently wired into typed-wasm CI.

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 payload (via the C2 encoder)
  • Same function-index conventions (imports first in declaration order, locals after)
  • Same control-flow patterns (Block / Loop / If / Else / End delimiters)

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 source program — and OCaml-emitted .wasm files get vendored alongside.

Fixture inventory

# Test Expected verdict
1 Clean Linear consumer (drop s) pass
2 Duplicated Linear (s + s) LinearUsedMultiple{count:2}
3 Dropped Linear in else (if(t) drop s) LinearDroppedOnSomePath
4 Aliased ExclBorrow (b.len() + b.len()) ExclBorrowAliased{count:2}
5 Multi-fn: one clean, one buggy single error on fn 1
6 Cross-mod: clean Linear call pass
7 Cross-mod: Linear called twice LinearImportCalledMultiple{count:2}
8 Cross-mod: 3 fns, only last misuses single error on caller_fn_idx=3
9 extract_exports of 3 different shapes correct param_kinds
10 Realistic multi-fn clean module pass

Test infrastructure

The test file includes an internal ModuleBuilder that constructs affinescript-shaped modules with multiple functions, imports, exports, and the ownership section. Keeps each fixture ~30 lines, so the conceptual-source → wasm-bytes 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

Stacking

Stacked on #22 (C4 cross-module verifier). Merge order: #22 → this.

Follow-up

  • C5.1 (future): vendor real OCaml-emitted .wasm files alongside these synthetic ones once affinescript build is part of CI; assert byte-for-byte parity in section payloads and verdict-for-verdict parity in verifier output.
  • C6 (#41): ephapax-wasm emits the affinescript.ownership custom section from linear-typed bindings.
  • C7 (#42): ephapax-cli gets --verify-ownership flag.

Closes #40 once merged.

@hyperpolymath hyperpolymath changed the base branch from feat/typed-wasm-verify-c4-cross-module to main May 15, 2026 07:07
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>
@hyperpolymath hyperpolymath force-pushed the feat/typed-wasm-verify-c5-cross-compat branch from bafec75 to 554364c Compare May 15, 2026 07:07
@hyperpolymath hyperpolymath merged commit 67006ed into main May 15, 2026
19 of 28 checks passed
@hyperpolymath hyperpolymath deleted the feat/typed-wasm-verify-c5-cross-compat branch May 15, 2026 07:08
hyperpolymath added a commit that referenced this pull request May 15, 2026
)

The Rust verifier crate at `crates/typed-wasm-verify/` landed across
PRs #19 (C1) → #23 (C5) on 2026-05-15 but the repo-level documentation
didn't catch up. This commit fixes that.

Changes
-------

* CHANGELOG.md `[Unreleased] → Added`: one entry summarising the
  crate, plus a sub-bullet per phase (C1-C5) with PR refs.
* CHANGELOG.md `[Unreleased] → Changed`: note that the repo is now
  polyglot Idris2 + Zig + Rust (root Cargo workspace).
* LEVEL-STATUS.md: new "Post-codegen verifier (Rust)" section after
  the Idris2 proof inventory, explaining the verifier's place in the
  three-layer story (spec proofs / source checker / post-codegen) and
  documenting coverage (L7 + L10 only for now). Lists current
  consumers (ephapax-wasm + ephapax-cli).
* ROADMAP.adoc: v0.4 (ecosystem) gets a [x] bullet for the Rust crate;
  v1.0 gets two new entries — [x] for the post-codegen verifier
  itself (partial v1.0 deliverable, separate from `.twasm` parsing),
  [ ] for the cross-compat parity proof against affinescript's OCaml
  reference (deferred as "C5.1").
* 0-AI-MANIFEST.a2ml: new `verify_rust` entry in `[canonical_locations]`
  so AI agents reading the manifest can find the crate.

No code changes — this is pure-docs cleanup. The crate itself, its
tests, and consumer integrations are already on `main`.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant