Skip to content

Commit 3ff5eae

Browse files
hyperpolymathclaude
andcommitted
feat(verify): scaffold typed-wasm-verify Rust crate (C1)
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>
1 parent 5456b1e commit 3ff5eae

5 files changed

Lines changed: 399 additions & 0 deletions

File tree

Cargo.lock

Lines changed: 177 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
[workspace]
3+
resolver = "2"
4+
members = [
5+
"crates/typed-wasm-verify",
6+
]
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
[package]
3+
name = "typed-wasm-verify"
4+
version = "0.1.0"
5+
edition = "2021"
6+
license = "PMPL-1.0-or-later"
7+
description = "Post-codegen verifier for typed-wasm L7 (aliasing) and L10 (linearity) constraints on emitted wasm modules"
8+
repository = "https://github.com/hyperpolymath/typed-wasm"
9+
readme = "README.md"
10+
11+
[dependencies]
12+
wasmparser = "0.221"
13+
thiserror = "2"
14+
15+
[dev-dependencies]
16+
wasm-encoder = "0.221"

crates/typed-wasm-verify/README.md

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
# typed-wasm-verify
3+
4+
Post-codegen verifier for typed-wasm **L7 (aliasing safety)** and **L10 (linearity)** constraints on emitted wasm modules.
5+
6+
## What it does
7+
8+
Given a wasm module that carries an `affinescript.ownership` custom section, this crate:
9+
10+
1. **Intra-function check** — walks every function body and computes per-path `(min_uses, max_uses)` for each parameter. Linear params must be `(1, 1)` on every path; ExclBorrow params must have `max_uses ≤ 1`.
11+
2. **Cross-module check** — given a callee's exported ownership interface plus a caller module that imports those functions, verifies that Linear-param imports are invoked exactly once per execution path.
12+
13+
The custom-section binary format:
14+
15+
```
16+
u32le count
17+
for each entry:
18+
u32le func_idx
19+
u8 n_params
20+
u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
21+
u8 ret_kind
22+
```
23+
24+
## Spec of record
25+
26+
This crate is a Rust port of `hyperpolymath/affinescript`:
27+
28+
- `lib/tw_verify.ml` — intra-function verifier (~246 LOC OCaml)
29+
- `lib/tw_interface.ml` — cross-module boundary verifier (~245 LOC OCaml)
30+
31+
The OCaml files remain the spec of record until behavioural parity is established by the cross-compat test suite (workspace task C5).
32+
33+
## Consumers
34+
35+
- `hyperpolymath/ephapax` — calls into this crate as a Cargo dependency to verify its compile-eph output.
36+
- `hyperpolymath/affinescript` — invokes the built binary as a subprocess, eventually replacing its OCaml verifier.
37+
38+
## Status
39+
40+
- [x] C1 — Scaffold (types, error enums, public entry stubs)
41+
- [ ] C2 — Custom-section parser
42+
- [ ] C3 — Per-path use-range analysis (L7+L10 intra-function)
43+
- [ ] C4 — Cross-module boundary verifier
44+
- [ ] C5 — Cross-compat test against affinescript-emitted wasm

0 commit comments

Comments
 (0)