From 1e247dee54d3ea41eb5eb7438f4d955f5a465435 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 15 May 2026 03:55:37 +0100 Subject: [PATCH] feat(verify): scaffold typed-wasm-verify Rust crate (C1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- Cargo.lock | 177 ++++++++++++++++++++++++++++ Cargo.toml | 6 + crates/typed-wasm-verify/Cargo.toml | 16 +++ crates/typed-wasm-verify/README.md | 44 +++++++ crates/typed-wasm-verify/src/lib.rs | 156 ++++++++++++++++++++++++ 5 files changed, 399 insertions(+) create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 crates/typed-wasm-verify/Cargo.toml create mode 100644 crates/typed-wasm-verify/README.md create mode 100644 crates/typed-wasm-verify/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..d6ddcf8 --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,177 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "bitflags" +version = "2.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "foldhash" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + +[[package]] +name = "hashbrown" +version = "0.15.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" +dependencies = [ + "foldhash", + "serde", +] + +[[package]] +name = "hashbrown" +version = "0.17.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" + +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.1", + "serde", + "serde_core", +] + +[[package]] +name = "leb128" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6cc46bac87ef8093eed6f272babb833b6443374399985ac8ed28471ee0918545" + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "thiserror" +version = "2.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "2.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "typed-wasm-verify" +version = "0.1.0" +dependencies = [ + "thiserror", + "wasm-encoder", + "wasmparser", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "wasm-encoder" +version = "0.221.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc8444fe4920de80a4fe5ab564fff2ae58b6b73166b89751f8c6c93509da32e5" +dependencies = [ + "leb128", + "wasmparser", +] + +[[package]] +name = "wasmparser" +version = "0.221.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d06bfa36ab3ac2be0dee563380147a5b81ba10dd8885d7fbbc9eb574be67d185" +dependencies = [ + "bitflags", + "hashbrown 0.15.5", + "indexmap", + "semver", + "serde", +] diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..131ac88 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +[workspace] +resolver = "2" +members = [ + "crates/typed-wasm-verify", +] diff --git a/crates/typed-wasm-verify/Cargo.toml b/crates/typed-wasm-verify/Cargo.toml new file mode 100644 index 0000000..e353fc8 --- /dev/null +++ b/crates/typed-wasm-verify/Cargo.toml @@ -0,0 +1,16 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +[package] +name = "typed-wasm-verify" +version = "0.1.0" +edition = "2021" +license = "PMPL-1.0-or-later" +description = "Post-codegen verifier for typed-wasm L7 (aliasing) and L10 (linearity) constraints on emitted wasm modules" +repository = "https://github.com/hyperpolymath/typed-wasm" +readme = "README.md" + +[dependencies] +wasmparser = "0.221" +thiserror = "2" + +[dev-dependencies] +wasm-encoder = "0.221" diff --git a/crates/typed-wasm-verify/README.md b/crates/typed-wasm-verify/README.md new file mode 100644 index 0000000..31ee338 --- /dev/null +++ b/crates/typed-wasm-verify/README.md @@ -0,0 +1,44 @@ + +# typed-wasm-verify + +Post-codegen verifier for typed-wasm **L7 (aliasing safety)** and **L10 (linearity)** constraints on emitted wasm modules. + +## What it does + +Given a wasm module that carries an `affinescript.ownership` custom section, this crate: + +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`. +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. + +The custom-section binary format: + +``` +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 +``` + +## Spec of record + +This crate is a Rust port of `hyperpolymath/affinescript`: + +- `lib/tw_verify.ml` — intra-function verifier (~246 LOC OCaml) +- `lib/tw_interface.ml` — cross-module boundary verifier (~245 LOC OCaml) + +The OCaml files remain the spec of record until behavioural parity is established by the cross-compat test suite (workspace task C5). + +## Consumers + +- `hyperpolymath/ephapax` — calls into this crate as a Cargo dependency to verify its compile-eph output. +- `hyperpolymath/affinescript` — invokes the built binary as a subprocess, eventually replacing its OCaml verifier. + +## Status + +- [x] C1 — Scaffold (types, error enums, public entry stubs) +- [ ] C2 — Custom-section parser +- [ ] C3 — Per-path use-range analysis (L7+L10 intra-function) +- [ ] C4 — Cross-module boundary verifier +- [ ] C5 — Cross-compat test against affinescript-emitted wasm diff --git a/crates/typed-wasm-verify/src/lib.rs b/crates/typed-wasm-verify/src/lib.rs new file mode 100644 index 0000000..4b3707e --- /dev/null +++ b/crates/typed-wasm-verify/src/lib.rs @@ -0,0 +1,156 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// +// typed-wasm post-codegen verifier. +// +// Statically verifies typed-wasm L7 (aliasing safety) and L10 (linearity) +// on emitted wasm modules. Reads the `affinescript.ownership` custom +// section, then runs per-path min/max use-range analysis on every +// function body in the module. +// +// Rust port of hyperpolymath/affinescript: +// - lib/tw_verify.ml (intra-function verifier, ~246 lines OCaml) +// - lib/tw_interface.ml (cross-module boundary verifier, ~245 lines OCaml) +// +// The OCaml files are the spec of record until this crate reaches +// behavioural parity (tracked by C5 in the workspace task list). + +use thiserror::Error; + +/// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum. +/// Wire encoding in the `affinescript.ownership` custom section: a single +/// u8 per kind, values 0/1/2/3 as below. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum OwnershipKind { + Unrestricted = 0, + Linear = 1, + SharedBorrow = 2, + ExclBorrow = 3, +} + +impl OwnershipKind { + /// Decode a wire byte. Any value outside 0..=3 maps to `Unrestricted` + /// — matches the OCaml `kind_of_byte` fallback. + pub fn from_byte(b: u8) -> Self { + match b { + 1 => OwnershipKind::Linear, + 2 => OwnershipKind::SharedBorrow, + 3 => OwnershipKind::ExclBorrow, + _ => OwnershipKind::Unrestricted, + } + } +} + +/// An ownership violation found in a wasm function body. +/// Mirrors OCaml `Tw_verify.ownership_error`. +#[derive(Debug, Clone, PartialEq, Eq, Error)] +pub enum OwnershipError { + #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on all paths (must be consumed exactly once)")] + LinearNotUsed { func_idx: u32, param_idx: u32 }, + + #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param dropped on some paths (per-path min uses = 0; must be consumed on every path)")] + LinearDroppedOnSomePath { func_idx: u32, param_idx: u32 }, + + #[error("Level 10 violation: function {func_idx}, param {param_idx} — Linear (own) param loaded {count} times on some path (exactly 1 required; possible duplication)")] + LinearUsedMultiple { func_idx: u32, param_idx: u32, count: u32 }, + + #[error("Level 7 violation: function {func_idx}, param {param_idx} — ExclBorrow (mut) param aliased ({count} simultaneous references; at most 1 permitted)")] + ExclBorrowAliased { func_idx: u32, param_idx: u32, count: u32 }, +} + +/// A cross-module ownership violation found in a caller's function body. +/// Mirrors OCaml `Tw_interface.cross_error`. +#[derive(Debug, Clone, PartialEq, Eq, Error)] +pub enum CrossError { + #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' {count} time(s) on some path (Linear param; must be called at most once)")] + LinearImportCalledMultiple { + caller_func_idx: u32, + import_func_idx: u32, + import_name: String, + count: u32, + }, + + #[error("Level 10 boundary violation: caller fn {caller_func_idx} calls import '{import_name}' on some paths but not others (Linear param dropped on zero-call path)")] + LinearImportDroppedOnSomePath { + caller_func_idx: u32, + import_func_idx: u32, + import_name: String, + }, +} + +/// Top-level verification failures (parse + verify). +#[derive(Debug, Error)] +pub enum VerifyError { + #[error("wasm parse error: {0}")] + Parse(#[from] wasmparser::BinaryReaderError), + + #[error("ownership violations: {0:?}")] + Ownership(Vec), + + #[error("cross-module boundary violations: {0:?}")] + Cross(Vec), +} + +/// Custom-section name carrying ownership annotations. Matches the OCaml +/// emitter (`Codegen.build_ownership_section`) and reader. +pub const OWNERSHIP_SECTION_NAME: &str = "affinescript.ownership"; + +// ---------------------------------------------------------------------- +// Public entry points (stubbed in C1; implementations land in C2-C4). +// ---------------------------------------------------------------------- + +/// Verify the L7+L10 ownership constraints on a wasm module by reading its +/// embedded `affinescript.ownership` custom section. Returns `Ok(())` when +/// no violations are found; modules without the section verify trivially. +/// +/// Rust port of OCaml `Tw_verify.verify_from_module`. +pub fn verify_from_module(_wasm_bytes: &[u8]) -> Result<(), VerifyError> { + todo!("C3: implement intra-function verifier") +} + +/// Extract ownership-annotated export interfaces from a wasm module. +/// Returns one entry per exported function; non-function exports are +/// filtered out. +/// +/// Rust port of OCaml `Tw_interface.extract_exports`. +pub fn extract_exports(_wasm_bytes: &[u8]) -> Result, VerifyError> { + todo!("C4: implement export interface extraction") +} + +/// Verify that a caller module's local function bodies respect the +/// ownership annotations of a callee's exported interface. +/// +/// Rust port of OCaml `Tw_interface.verify_cross_module`. +pub fn verify_cross_module( + _callee_iface: &[FuncInterface], + _caller_bytes: &[u8], +) -> Result<(), VerifyError> { + todo!("C4: implement cross-module boundary verifier") +} + +/// Ownership-annotated signature for one exported function. +/// Mirrors OCaml `Tw_interface.func_interface`. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct FuncInterface { + pub name: String, + pub func_idx: u32, + pub param_kinds: Vec, + pub ret_kind: OwnershipKind, +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn ownership_kind_byte_roundtrip() { + for (b, k) in [ + (0, OwnershipKind::Unrestricted), + (1, OwnershipKind::Linear), + (2, OwnershipKind::SharedBorrow), + (3, OwnershipKind::ExclBorrow), + ] { + assert_eq!(OwnershipKind::from_byte(b), k); + } + assert_eq!(OwnershipKind::from_byte(99), OwnershipKind::Unrestricted); + } +}