feat(verify): scaffold typed-wasm-verify Rust crate (C1)#19
Merged
Conversation
This was referenced May 15, 2026
hyperpolymath
force-pushed
the
feat/typed-wasm-verify-rust-port
branch
from
3ff5eae to
2d63b52
Compare
Adds a new Cargo workspace at the repo root with one member:
`crates/typed-wasm-verify`. The crate is the Rust home for typed-wasm's
post-codegen L7 (aliasing) + L10 (linearity) verifier. This commit lands
the scaffolding only — public types, error enums, and stubbed entry
points. Real implementations come in follow-ups C2/C3/C4.
Why a Rust crate here?
----------------------
- The ReScript parser/checker in `src/parser/*.res` is on the way out
(ReScript ban across hyperpolymath repos), so the canonical
surface-level checker will be Rust. Starting with the post-codegen
verifier — a self-contained piece that operates on emitted wasm
rather than on `.twasm` source — lets the port begin without first
needing a `.twasm` parser.
- Downstream consumers want a Rust dependency: ephapax (already Rust)
to call into directly via a Cargo path/git dep, and affinescript
(OCaml) to invoke as a subprocess until full FFI lands.
Spec of record
--------------
Both modules are direct ports of:
- hyperpolymath/affinescript:lib/tw_verify.ml (~246 LOC OCaml)
- hyperpolymath/affinescript:lib/tw_interface.ml (~245 LOC OCaml)
Until the cross-compat suite (C5) is green, those OCaml files remain
authoritative.
Public surface (this commit)
----------------------------
- `OwnershipKind` — 4-variant enum with `from_byte` decoder matching the
OCaml fallback semantics (anything outside 0..=3 → Unrestricted).
- `OwnershipError` — 4 variants for intra-function violations
(LinearNotUsed / LinearDroppedOnSomePath / LinearUsedMultiple /
ExclBorrowAliased), each carrying `func_idx` + `param_idx` and a
`thiserror`-derived Display matching the OCaml `pp_error` output.
- `CrossError` — 2 variants for cross-module boundary violations
(LinearImportCalledMultiple / LinearImportDroppedOnSomePath) carrying
`caller_func_idx`, `import_func_idx`, `import_name`.
- `FuncInterface` — exported-function signature carrying its ownership
kinds, mirroring `Tw_interface.func_interface`.
- `VerifyError` — top-level error type covering wasmparser failures plus
the two violation vectors.
- `OWNERSHIP_SECTION_NAME` — the `affinescript.ownership` custom-section
name constant.
- Three stubbed entry points (`verify_from_module`, `extract_exports`,
`verify_cross_module`) — all `todo!()` until C2/C3/C4 land. Signatures
are pinned now so consumers can already start writing call sites.
Dependencies
------------
- wasmparser 0.221 — for module/instruction walking in C3/C4
- thiserror 2 — error-enum derive
- wasm-encoder 0.221 (dev) — for synthesising test fixtures in C2/C3
Build status
------------
$ cargo build -p typed-wasm-verify
Finished `dev` profile [unoptimized + debuginfo] target(s)
$ cargo test -p typed-wasm-verify
running 1 test
test tests::ownership_kind_byte_roundtrip ... ok
test result: ok. 1 passed; 0 failed; 0 ignored
Follow-up tasks
---------------
C2 (#37) — wire the `affinescript.ownership` custom-section parser
(u32le count + per-entry header)
C3 (#38) — port `tw_verify.count_uses_range` over wasmparser ops and
implement the per-fn / per-module verifier proper
C4 (#39) — port `tw_interface.{extract_exports, verify_cross_module}`
C5 (#40) — cross-compat test against affinescript-emitted modules
C6 (#41) — ephapax-wasm emits the custom section
C7 (#42) — ephapax-cli gets `--verify-ownership`
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
hyperpolymath
force-pushed
the
feat/typed-wasm-verify-rust-port
branch
from
2d63b52 to
1e247de
Compare
hyperpolymath
added a commit
that referenced
this pull request
May 15, 2026
Implements the parser and encoder for the `affinescript.ownership`
custom-section wire format. The parser is a faithful port of OCaml
`Tw_verify.parse_ownership_section_payload`; the encoder mirrors the
matching emitter on the affinescript side (`Codegen.build_ownership_section`)
so downstream emitters in ephapax (C6) and elsewhere can reuse it.
Wire format
-----------
Little-endian, byte-aligned:
u32le count
for each entry:
u32le func_idx
u8 n_params
u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
u8 ret_kind
Cross-impl parity decision
--------------------------
The OCaml parser is lenient: reading past the end of the payload yields
zero bytes (interpreted as `Unrestricted` kinds and `func_idx = 0`).
This Rust port preserves that exactly. A correctly-emitted section
will never be truncated, but matching the leniency means the C5
cross-compat suite sees identical results on every payload the OCaml
side accepts. Stricter validation is a future opt-in (`parse_strict`),
not the default.
The `OwnershipKind::from_byte` fallback (anything outside 0..=3 →
`Unrestricted`) was already in C1 and is reused here.
New API
-------
- `OwnershipEntry { func_idx, param_kinds, ret_kind }` — named struct
replacing the OCaml 3-tuple for readability.
- `parse_ownership_section_payload(&[u8]) -> Vec<OwnershipEntry>` —
lenient parser (matches OCaml).
- `build_ownership_section_payload(&[OwnershipEntry]) -> Vec<u8>` —
inverse encoder; panics if any entry has >255 params (the n_params
field is u8, but real wasm modules don't hit this limit).
- `OwnershipKind::to_byte(self) -> u8` — encode side of the existing
`from_byte`.
Tests
-----
11/11 unit tests, covering:
- empty payload
- count=0 with no entries
- single entry with zero params
- single entry with all four kind values (encode + decode)
- multi-entry round-trip
- unknown kind byte falls back to `Unrestricted` (parity guard)
- truncated payload reads zeros past EOF (parity guard)
- empty round-trip (entries → bytes → entries)
- realistic 2-entry round-trip
- exact wire-format byte sequence for a known input
$ cargo test -p typed-wasm-verify
running 11 tests
test section::tests::build_emits_correct_wire_format ... ok
test section::tests::empty_payload_yields_no_entries ... ok
test section::tests::roundtrip_empty ... ok
test section::tests::count_zero_yields_no_entries ... ok
test section::tests::multiple_entries ... ok
test section::tests::roundtrip_realistic ... ok
test section::tests::single_entry_no_params ... ok
test section::tests::single_entry_with_all_kinds ... ok
test section::tests::truncated_payload_reads_zeros_past_end ... ok
test section::tests::unknown_kind_byte_decodes_to_unrestricted ... ok
test tests::ownership_kind_byte_roundtrip ... ok
test result: ok. 11 passed; 0 failed; 0 ignored
Stacked on top of #19 (C1 scaffold). Next: C3 — port the per-path
use-range analysis and intra-function verifier.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 15, 2026
Implements the parser and encoder for the `affinescript.ownership`
custom-section wire format. The parser is a faithful port of OCaml
`Tw_verify.parse_ownership_section_payload`; the encoder mirrors the
matching emitter on the affinescript side (`Codegen.build_ownership_section`)
so downstream emitters in ephapax (C6) and elsewhere can reuse it.
Wire format
-----------
Little-endian, byte-aligned:
u32le count
for each entry:
u32le func_idx
u8 n_params
u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
u8 ret_kind
Cross-impl parity decision
--------------------------
The OCaml parser is lenient: reading past the end of the payload yields
zero bytes (interpreted as `Unrestricted` kinds and `func_idx = 0`).
This Rust port preserves that exactly. A correctly-emitted section
will never be truncated, but matching the leniency means the C5
cross-compat suite sees identical results on every payload the OCaml
side accepts. Stricter validation is a future opt-in (`parse_strict`),
not the default.
The `OwnershipKind::from_byte` fallback (anything outside 0..=3 →
`Unrestricted`) was already in C1 and is reused here.
New API
-------
- `OwnershipEntry { func_idx, param_kinds, ret_kind }` — named struct
replacing the OCaml 3-tuple for readability.
- `parse_ownership_section_payload(&[u8]) -> Vec<OwnershipEntry>` —
lenient parser (matches OCaml).
- `build_ownership_section_payload(&[OwnershipEntry]) -> Vec<u8>` —
inverse encoder; panics if any entry has >255 params (the n_params
field is u8, but real wasm modules don't hit this limit).
- `OwnershipKind::to_byte(self) -> u8` — encode side of the existing
`from_byte`.
Tests
-----
11/11 unit tests, covering:
- empty payload
- count=0 with no entries
- single entry with zero params
- single entry with all four kind values (encode + decode)
- multi-entry round-trip
- unknown kind byte falls back to `Unrestricted` (parity guard)
- truncated payload reads zeros past EOF (parity guard)
- empty round-trip (entries → bytes → entries)
- realistic 2-entry round-trip
- exact wire-format byte sequence for a known input
$ cargo test -p typed-wasm-verify
running 11 tests
test section::tests::build_emits_correct_wire_format ... ok
test section::tests::empty_payload_yields_no_entries ... ok
test section::tests::roundtrip_empty ... ok
test section::tests::count_zero_yields_no_entries ... ok
test section::tests::multiple_entries ... ok
test section::tests::roundtrip_realistic ... ok
test section::tests::single_entry_no_params ... ok
test section::tests::single_entry_with_all_kinds ... ok
test section::tests::truncated_payload_reads_zeros_past_end ... ok
test section::tests::unknown_kind_byte_decodes_to_unrestricted ... ok
test tests::ownership_kind_byte_roundtrip ... ok
test result: ok. 11 passed; 0 failed; 0 ignored
Stacked on top of #19 (C1 scaffold). Next: C3 — port the per-path
use-range analysis and intra-function verifier.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 15, 2026
…#20) Implements the parser and encoder for the `affinescript.ownership` custom-section wire format. The parser is a faithful port of OCaml `Tw_verify.parse_ownership_section_payload`; the encoder mirrors the matching emitter on the affinescript side (`Codegen.build_ownership_section`) so downstream emitters in ephapax (C6) and elsewhere can reuse it. Wire format ----------- Little-endian, byte-aligned: u32le count for each entry: u32le func_idx u8 n_params u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow) u8 ret_kind Cross-impl parity decision -------------------------- The OCaml parser is lenient: reading past the end of the payload yields zero bytes (interpreted as `Unrestricted` kinds and `func_idx = 0`). This Rust port preserves that exactly. A correctly-emitted section will never be truncated, but matching the leniency means the C5 cross-compat suite sees identical results on every payload the OCaml side accepts. Stricter validation is a future opt-in (`parse_strict`), not the default. The `OwnershipKind::from_byte` fallback (anything outside 0..=3 → `Unrestricted`) was already in C1 and is reused here. New API ------- - `OwnershipEntry { func_idx, param_kinds, ret_kind }` — named struct replacing the OCaml 3-tuple for readability. - `parse_ownership_section_payload(&[u8]) -> Vec<OwnershipEntry>` — lenient parser (matches OCaml). - `build_ownership_section_payload(&[OwnershipEntry]) -> Vec<u8>` — inverse encoder; panics if any entry has >255 params (the n_params field is u8, but real wasm modules don't hit this limit). - `OwnershipKind::to_byte(self) -> u8` — encode side of the existing `from_byte`. Tests ----- 11/11 unit tests, covering: - empty payload - count=0 with no entries - single entry with zero params - single entry with all four kind values (encode + decode) - multi-entry round-trip - unknown kind byte falls back to `Unrestricted` (parity guard) - truncated payload reads zeros past EOF (parity guard) - empty round-trip (entries → bytes → entries) - realistic 2-entry round-trip - exact wire-format byte sequence for a known input $ cargo test -p typed-wasm-verify running 11 tests test section::tests::build_emits_correct_wire_format ... ok test section::tests::empty_payload_yields_no_entries ... ok test section::tests::roundtrip_empty ... ok test section::tests::count_zero_yields_no_entries ... ok test section::tests::multiple_entries ... ok test section::tests::roundtrip_realistic ... ok test section::tests::single_entry_no_params ... ok test section::tests::single_entry_with_all_kinds ... ok test section::tests::truncated_payload_reads_zeros_past_end ... ok test section::tests::unknown_kind_byte_decodes_to_unrestricted ... ok test tests::ownership_kind_byte_roundtrip ... ok test result: ok. 11 passed; 0 failed; 0 ignored Stacked on top of #19 (C1 scaffold). Next: C3 — port the per-path use-range analysis and intra-function verifier. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
crates/typed-wasm-verify.hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml.Why
The ReScript parser/checker at
src/parser/*.resis on its way out — ReScript is banned across the org. typed-wasm's Rust toolchain has to start somewhere; the verifier is the most self-contained piece (operates on emitted wasm, not on.twasmsource), so it doesn't block on a.twasmparser. Downstream consumers (hyperpolymath/ephapaxdirectly,hyperpolymath/affinescriptvia subprocess) want a Rust home for this code.Spec of record
Until the cross-compat suite (C5) is green, the OCaml files in
hyperpolymath/affinescript:lib/tw_verify.ml(~246 LOC) — per-fn min/max use-range analysislib/tw_interface.ml(~245 LOC) — cross-module boundary checksremain authoritative.
Build
Follow-up
count_uses_rangeand the intra-function verifierextract_exports+verify_cross_modulehyperpolymath/ephapaxconsumer wiring (separate PR there)