From 103db891e0636dab9188e8a376f09f755e894bec Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 15 May 2026 04:10:57 +0100 Subject: [PATCH] feat(verify): per-path use-range analysis + intra-fn verifier (C3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ports `Tw_verify.count_uses_range` + `verify_function` + `verify_from_module` from hyperpolymath/affinescript/lib/tw_verify.ml. After this commit the C1 `verify_from_module` stub is gone — calling it on a wasm module that carries an `affinescript.ownership` custom section actually enforces the L7 (aliasing) and L10 (linearity) constraints. The algorithm ------------- OCaml walks an in-memory instruction tree recursively. wasmparser hands us a flat operator stream with structured-control delimiters, so we run the same per-path `(min, max)` algorithm with an explicit frame stack: Frame::Plain — Block, Loop, or the implicit body scope Frame::IfThen — `If` before any `Else` is seen Frame::IfElse — `If` after `Else`; then-side totals are frozen Frame transitions on the structured-control operators: Block / Loop → push Plain If → push IfThen Else → top must be IfThen; transition to IfElse, freezing the then-side totals End → pop, collapse to (m, x), add into parent Plain → (min, max) IfThen, no else seen → (0, then_max) IfElse → (min(t,e), max(t,e)) LocalGet n → if n matches the counter, add (1, 1) to the top frame's currently-active side Anything else → no-op The function body's terminating `End` pops the bottom frame and the collapse becomes the final result. The frame state is split out as a private `OpCounter` trait so C4 can reuse the exact same machinery with a `Call`-based counter for cross-module verification. Per-function rules (mirroring OCaml `verify_function`) ------------------------------------------------------ For each param at index `i`, compute `(min_uses, max_uses)` then apply: Linear: max == 0 → LinearNotUsed min == 0, max ≥ 1 → LinearDroppedOnSomePath max > 1 → LinearUsedMultiple { count: max } (both "drop" and "dup" can fire for the same param if min=0, max>1) ExclBorrow: max > 1 → ExclBorrowAliased { count: max } Unrestricted | SharedBorrow: no constraints Module-level entry ------------------ `verify_from_module(wasm_bytes)`: 1. Single wasmparser pass over the module: - Tally import_count for the function index space - Capture the `affinescript.ownership` custom section (if any) - Collect every `Payload::CodeSectionEntry` body in order 2. If no ownership section: trivially `Ok(())`. 3. Parse the section (C2's `parse_ownership_section_payload`). 4. For each entry, translate `func_idx` (global) to a body index by subtracting `import_count`. Skip imports (no body) and out-of- range entries — matches OCaml's short-circuit behaviour. 5. Aggregate all per-function violations into one `VerifyError::Ownership` vector, or return `Ok(())` if clean. Tests ----- 29/29 unit tests pass: count_uses_range layer (range_in helper synthesises a 1-fn module via wasm-encoder and pulls the body out for direct analysis): no_uses → (0, 0) one_use → (1, 1) two_uses_same_path → (2, 2) use_in_both_if_branches → (1, 1) use_in_then_only → (0, 1) use_twice_in_then_once_in_else → (1, 2) use_inside_block_passthrough → (1, 1) use_inside_loop_passthrough → (1, 1) nested_if_use_in_inner_then_only → (0, 1) verify_from_module end-to-end (synthetic modules with ownership custom sections, hitting each error variant + the clean paths): linear_used_exactly_once_is_clean linear_not_used_at_all_errors → LinearNotUsed linear_dropped_on_some_path_errors → LinearDroppedOnSomePath linear_used_twice_errors → LinearUsedMultiple excl_borrow_used_twice_errors → ExclBorrowAliased excl_borrow_used_once_is_clean unrestricted_used_arbitrarily_is_clean module_without_ownership_section_is_trivially_clean empty_module_is_trivially_clean $ cargo test -p typed-wasm-verify running 29 tests ... all pass ... test result: ok. 29 passed; 0 failed; 0 ignored Stacked on top of #20 (C2 section codec). Next: C4 — port the cross-module boundary verifier (the same `(min, max)` frame stack applied to `Call` operators against a callee's exported interface). Co-Authored-By: Claude Opus 4.7 --- crates/typed-wasm-verify/src/lib.rs | 6 +- crates/typed-wasm-verify/src/verify.rs | 664 +++++++++++++++++++++++++ 2 files changed, 668 insertions(+), 2 deletions(-) create mode 100644 crates/typed-wasm-verify/src/verify.rs diff --git a/crates/typed-wasm-verify/src/lib.rs b/crates/typed-wasm-verify/src/lib.rs index 2e3f62d..c1ecab2 100644 --- a/crates/typed-wasm-verify/src/lib.rs +++ b/crates/typed-wasm-verify/src/lib.rs @@ -17,7 +17,9 @@ use thiserror::Error; pub mod section; +pub mod verify; pub use section::{build_ownership_section_payload, parse_ownership_section_payload, OwnershipEntry}; +pub use verify::{count_uses_range, verify_function}; /// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum. /// Wire encoding in the `affinescript.ownership` custom section: a single @@ -111,8 +113,8 @@ pub const OWNERSHIP_SECTION_NAME: &str = "affinescript.ownership"; /// 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") +pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> { + verify::verify_from_module(wasm_bytes) } /// Extract ownership-annotated export interfaces from a wasm module. diff --git a/crates/typed-wasm-verify/src/verify.rs b/crates/typed-wasm-verify/src/verify.rs new file mode 100644 index 0000000..2480d83 --- /dev/null +++ b/crates/typed-wasm-verify/src/verify.rs @@ -0,0 +1,664 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// +// Intra-function L7+L10 verifier. +// +// Rust port of `Tw_verify.count_uses_range` + `verify_function` + +// `verify_from_module` from hyperpolymath/affinescript/lib/tw_verify.ml. +// +// The OCaml original walks an in-memory instruction tree recursively. +// wasmparser hands us a flat operator stream with structured-control +// delimiters (Block/Loop/If/Else/End), so we run the same per-path +// `(min, max)` algorithm with an explicit control-flow frame stack. +// +// For each control structure: +// - Block / Loop: a single path; uses inside accumulate into the +// enclosing frame's running total when the End fires. +// - If with no Else: implicit (0, 0) else-arm, so the contribution +// is (min(t_min, 0), max(t_max, 0)) = (0, t_max). +// - If/Else: contributes (min(t_min, e_min), max(t_max, e_max)). +// +// Then verification rules per ownership kind: +// - Linear: exactly once on every path +// - ExclBorrow: at most once on any path +// - Unrestricted / SharedBorrow: unconstrained + +use wasmparser::{BinaryReaderError, FunctionBody, Operator, Parser, Payload}; + +use crate::section::{parse_ownership_section_payload, OwnershipEntry}; +use crate::{OwnershipError, OwnershipKind, VerifyError, OWNERSHIP_SECTION_NAME}; + +// ---------------------------------------------------------------------- +// Per-path use-range analysis +// ---------------------------------------------------------------------- + +/// Frame in the control-flow stack while walking a function body. +/// +/// Each frame tracks the running `(min, max)` use-count for the side of +/// the control structure that is currently being scanned. For an `If` +/// before its `Else` (or before `End` if there is no else), that side +/// is the then-arm; after `Else`, it's the else-arm and the then-arm's +/// totals are frozen in `then_min` / `then_max`. +#[derive(Debug)] +enum Frame { + /// Block, Loop, or the implicit body scope. Single execution path. + Plain { min: u32, max: u32 }, + /// `If` before any `Else` is seen. Current side = then-arm. + IfThen { then_min: u32, then_max: u32 }, + /// `If` after `Else`. Then-side totals are frozen; current side = else-arm. + IfElse { + then_min: u32, + then_max: u32, + else_min: u32, + else_max: u32, + }, +} + +impl Frame { + /// Add `(m, x)` uses to the frame's currently-active side. + fn add_uses(&mut self, m: u32, x: u32) { + match self { + Frame::Plain { min, max } => { + *min += m; + *max += x; + } + Frame::IfThen { then_min, then_max } => { + *then_min += m; + *then_max += x; + } + Frame::IfElse { else_min, else_max, .. } => { + *else_min += m; + *else_max += x; + } + } + } + + /// Collapse this frame's contribution to `(min, max)` as if its + /// scope just closed. + fn collapse(&self) -> (u32, u32) { + match *self { + Frame::Plain { min, max } => (min, max), + // No `Else` seen: the else-arm is implicitly empty (0, 0). + // min(then_min, 0) = 0; max(then_max, 0) = then_max. + Frame::IfThen { then_max, .. } => (0, then_max), + Frame::IfElse { + then_min, + then_max, + else_min, + else_max, + } => (then_min.min(else_min), then_max.max(else_max)), + } + } +} + +/// Predicate distinguishing the operator we're counting from everything +/// else. C3 uses one of these (`local_get == local_idx`); C4 will use a +/// `Call`-based one (`call == import_idx`). +trait OpCounter { + fn matches(&self, op: &Operator<'_>) -> bool; +} + +struct LocalGetOf(u32); + +impl OpCounter for LocalGetOf { + fn matches(&self, op: &Operator<'_>) -> bool { + matches!(op, Operator::LocalGet { local_index } if *local_index == self.0) + } +} + +/// Compute the per-path `(min_uses, max_uses)` count for the operator +/// described by `counter` across a function body's instruction stream. +/// +/// Streaming equivalent of OCaml `Tw_verify.count_uses_range`. The body +/// reader must yield every operator in order including the final `End` +/// (which is what `wasmparser::FunctionBody::get_operators_reader` +/// produces). +fn count_op_range( + body: FunctionBody<'_>, + counter: &C, +) -> Result<(u32, u32), BinaryReaderError> { + let mut stack: Vec = vec![Frame::Plain { min: 0, max: 0 }]; + let mut final_result: Option<(u32, u32)> = None; + + let reader = body.get_operators_reader()?; + for op_result in reader { + let op = op_result?; + + if counter.matches(&op) { + stack + .last_mut() + .expect("frame stack underflow on counted op") + .add_uses(1, 1); + continue; + } + + match op { + Operator::Block { .. } | Operator::Loop { .. } => { + stack.push(Frame::Plain { min: 0, max: 0 }); + } + Operator::If { .. } => { + stack.push(Frame::IfThen { + then_min: 0, + then_max: 0, + }); + } + Operator::Else => { + let top = stack + .last_mut() + .expect("frame stack underflow at Else"); + match *top { + Frame::IfThen { then_min, then_max } => { + *top = Frame::IfElse { + then_min, + then_max, + else_min: 0, + else_max: 0, + }; + } + _ => unreachable!("Else without matching If"), + } + } + Operator::End => { + let popped = stack.pop().expect("frame stack underflow at End"); + let (m, x) = popped.collapse(); + if let Some(parent) = stack.last_mut() { + parent.add_uses(m, x); + } else { + // Outermost frame just closed: this was the final End + // of the function body. + final_result = Some((m, x)); + } + } + _ => {} + } + } + + // wasmparser emits the function-body terminating End as part of the + // operator stream, so `final_result` is normally set when the loop + // exits. If a fixture omits that End (synthetic / malformed input), + // fall back to the bottom-frame accumulator so we still produce a + // total. + if let Some(r) = final_result { + Ok(r) + } else { + Ok(stack + .into_iter() + .next() + .map(|f| f.collapse()) + .unwrap_or((0, 0))) + } +} + +/// Compute the per-path `(min, max)` count for `local_get local_idx` +/// across a function body. Convenience wrapper around `count_op_range` +/// for the L7+L10 intra-function checks. +pub fn count_uses_range( + body: FunctionBody<'_>, + local_idx: u32, +) -> Result<(u32, u32), BinaryReaderError> { + count_op_range(body, &LocalGetOf(local_idx)) +} + +// ---------------------------------------------------------------------- +// Per-function verification +// ---------------------------------------------------------------------- + +/// Verify the L7+L10 ownership constraints on a single function body. +/// Returns every violation found; an empty result means the function +/// is clean for its declared param kinds. +/// +/// Rust port of OCaml `Tw_verify.verify_function`. +pub fn verify_function( + body: FunctionBody<'_>, + param_kinds: &[OwnershipKind], + func_idx: u32, +) -> Result, BinaryReaderError> { + let mut errors = Vec::new(); + for (param_idx, kind) in param_kinds.iter().enumerate() { + let param_idx = param_idx as u32; + // get_operators_reader takes the body by reference internally but + // FunctionBody is `Copy`, so cloning is cheap. + let (min_uses, max_uses) = count_uses_range(body.clone(), param_idx)?; + match kind { + OwnershipKind::Linear => { + if max_uses == 0 { + errors.push(OwnershipError::LinearNotUsed { + func_idx, + param_idx, + }); + } else if min_uses == 0 { + errors.push(OwnershipError::LinearDroppedOnSomePath { + func_idx, + param_idx, + }); + } + if max_uses > 1 { + errors.push(OwnershipError::LinearUsedMultiple { + func_idx, + param_idx, + count: max_uses, + }); + } + } + OwnershipKind::ExclBorrow => { + if max_uses > 1 { + errors.push(OwnershipError::ExclBorrowAliased { + func_idx, + param_idx, + count: max_uses, + }); + } + } + OwnershipKind::Unrestricted | OwnershipKind::SharedBorrow => {} + } + } + Ok(errors) +} + +// ---------------------------------------------------------------------- +// Module-level entry +// ---------------------------------------------------------------------- + +/// Verify the L7+L10 ownership constraints across an entire wasm +/// module by reading its embedded `affinescript.ownership` custom +/// section. 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> { + // First pass: locate the ownership section (if any) and collect + // every function body alongside its global function index. + let mut ownership_payload: Option> = None; + let mut bodies: Vec> = Vec::new(); + let mut import_count: u32 = 0; + + let parser = Parser::new(0); + for payload in parser.parse_all(wasm_bytes) { + match payload? { + Payload::ImportSection(reader) => { + // We need import_count to translate global func indices + // (used in the ownership section) to body indices. + // wasmparser yields imports of every kind; filter to functions. + for import in reader { + let import = import?; + if matches!(import.ty, wasmparser::TypeRef::Func(_)) { + import_count += 1; + } + } + } + Payload::CustomSection(reader) if reader.name() == OWNERSHIP_SECTION_NAME => { + ownership_payload = Some(reader.data().to_vec()); + } + Payload::CodeSectionEntry(body) => { + bodies.push(body); + } + _ => {} + } + } + + let Some(payload) = ownership_payload else { + // No ownership section: nothing constrained, verify trivially. + return Ok(()); + }; + let entries = parse_ownership_section_payload(&payload); + + let mut all_errors = Vec::new(); + for OwnershipEntry { func_idx, param_kinds, .. } in entries { + // Global func index → body index: skip imports. + let Some(body_idx) = func_idx.checked_sub(import_count) else { + // Imported function: no body to inspect (the import's host + // implementation is opaque). Matches OCaml's + // `local_idx < 0` short-circuit. + continue; + }; + let body_idx = body_idx as usize; + if body_idx >= bodies.len() { + // Entry refers to a function we never saw (malformed module + // or section). Skip silently — matches OCaml's + // `local_idx >= List.length funcs` short-circuit. + continue; + } + let errs = verify_function(bodies[body_idx].clone(), ¶m_kinds, func_idx)?; + all_errors.extend(errs); + } + + if all_errors.is_empty() { + Ok(()) + } else { + Err(VerifyError::Ownership(all_errors)) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::section::build_ownership_section_payload; + use crate::OwnershipEntry; + use wasm_encoder::{ + CodeSection, CustomSection, Function, FunctionSection, ImportSection, Instruction, + Module, TypeSection, ValType, + }; + + /// Build a single-function wasm module with the given function body + /// (as a sequence of instructions, NOT including the trailing `End` + /// — `wasm_encoder::Function` adds it automatically). The function + /// has `n_params` i32 params, no return value. + /// + /// Optionally embeds an `affinescript.ownership` custom section + /// claiming the function (at global index 0, since there are no + /// imports) has the given param kinds. + fn module_with_body( + n_params: u32, + body: &[Instruction<'_>], + ownership: Option>, + ) -> Vec { + let mut module = Module::new(); + + let mut types = TypeSection::new(); + types + .ty() + .function((0..n_params).map(|_| ValType::I32), [ValType::I32]); + module.section(&types); + + let mut funcs = FunctionSection::new(); + funcs.function(0); + module.section(&funcs); + + let mut code = CodeSection::new(); + let mut f = Function::new([]); + for instr in body { + f.instruction(instr); + } + // Must end with the body's trailing End for valid wasm; do not + // double up here — `wasm_encoder::Function` documents this + // requirement. + f.instruction(&Instruction::End); + code.function(&f); + module.section(&code); + + if let Some(kinds) = ownership { + let payload = build_ownership_section_payload(&[OwnershipEntry { + func_idx: 0, + param_kinds: kinds, + ret_kind: OwnershipKind::Unrestricted, + }]); + let custom = CustomSection { + name: OWNERSHIP_SECTION_NAME.into(), + data: payload.as_slice().into(), + }; + module.section(&custom); + } + + module.finish() + } + + // ------------------------------------------------------------------ + // count_uses_range — the algorithmic core + // ------------------------------------------------------------------ + + /// Return the (min, max) range for `local_idx` across a body built + /// from `body` (instructions; trailing `End` added by the helper). + fn range_in(body: &[Instruction<'_>], local_idx: u32) -> (u32, u32) { + let wasm = module_with_body(2, body, None); + let parser = Parser::new(0); + for payload in parser.parse_all(&wasm) { + if let Payload::CodeSectionEntry(body) = payload.unwrap() { + return count_uses_range(body, local_idx).unwrap(); + } + } + panic!("no code section entry in synthetic module") + } + + #[test] + fn no_uses() { + let body = [Instruction::I32Const(0), Instruction::Return]; + assert_eq!(range_in(&body, 0), (0, 0)); + } + + #[test] + fn one_use() { + let body = [Instruction::LocalGet(0), Instruction::Return]; + assert_eq!(range_in(&body, 0), (1, 1)); + } + + #[test] + fn two_uses_same_path() { + let body = [ + Instruction::LocalGet(0), + Instruction::LocalGet(0), + Instruction::I32Add, + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (2, 2)); + } + + #[test] + fn use_in_both_if_branches() { + // if (lg1) { lg0 } else { lg0 } — used exactly once on every path + let body = [ + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::Else, + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, // closes If + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (1, 1)); + } + + #[test] + fn use_in_then_only() { + // if (lg1) { lg0 } — partial drop: (min=0, max=1) + let body = [ + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (0, 1)); + } + + #[test] + fn use_twice_in_then_once_in_else() { + // if (lg1) { lg0; lg0 } else { lg0 } — (min=1, max=2) + let body = [ + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::Else, + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (1, 2)); + } + + #[test] + fn use_inside_block_passthrough() { + // block { lg0 } — Block is a single path, so the inner (1,1) + // propagates as (1,1). + let body = [ + Instruction::Block(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (1, 1)); + } + + #[test] + fn use_inside_loop_passthrough() { + // loop { lg0 } — Loop is also a single path for this static + // counter (the analysis does not model iteration). + let body = [ + Instruction::Loop(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (1, 1)); + } + + #[test] + fn nested_if_use_in_inner_then_only() { + // if (lg1) { if (lg1) { lg0 } } — innermost If is (0, 1), outer + // also (0, 1) — outer is then-only so the implicit-else rule + // gives (min(then=0, 0), max(then=1, 0)) = (0, 1). + let body = [ + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, // inner If + Instruction::End, // outer If + Instruction::I32Const(0), + Instruction::Return, + ]; + assert_eq!(range_in(&body, 0), (0, 1)); + } + + // ------------------------------------------------------------------ + // verify_from_module — end-to-end + // ------------------------------------------------------------------ + + #[test] + fn linear_used_exactly_once_is_clean() { + let body = [Instruction::LocalGet(0), Instruction::Return]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::Linear])); + assert!(verify_from_module(&wasm).is_ok()); + } + + #[test] + fn linear_not_used_at_all_errors() { + let body = [Instruction::I32Const(0), Instruction::Return]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::Linear])); + match verify_from_module(&wasm) { + Err(VerifyError::Ownership(errs)) => { + assert!(matches!( + errs.as_slice(), + [OwnershipError::LinearNotUsed { func_idx: 0, param_idx: 0 }] + )); + } + other => panic!("expected LinearNotUsed, got {:?}", other), + } + } + + #[test] + fn linear_dropped_on_some_path_errors() { + // if (lg1) { lg0 } — Linear used in then-only. + let body = [ + Instruction::LocalGet(1), + Instruction::If(wasm_encoder::BlockType::Empty), + Instruction::LocalGet(0), + Instruction::Drop, + Instruction::End, + Instruction::I32Const(0), + Instruction::Return, + ]; + let wasm = module_with_body( + 2, + &body, + Some(vec![OwnershipKind::Linear, OwnershipKind::Unrestricted]), + ); + match verify_from_module(&wasm) { + Err(VerifyError::Ownership(errs)) => { + assert!(matches!( + errs.as_slice(), + [OwnershipError::LinearDroppedOnSomePath { func_idx: 0, param_idx: 0 }] + )); + } + other => panic!("expected LinearDroppedOnSomePath, got {:?}", other), + } + } + + #[test] + fn linear_used_twice_errors() { + let body = [ + Instruction::LocalGet(0), + Instruction::LocalGet(0), + Instruction::I32Add, + Instruction::Return, + ]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::Linear])); + match verify_from_module(&wasm) { + Err(VerifyError::Ownership(errs)) => { + assert!(matches!( + errs.as_slice(), + [OwnershipError::LinearUsedMultiple { func_idx: 0, param_idx: 0, count: 2 }] + )); + } + other => panic!("expected LinearUsedMultiple, got {:?}", other), + } + } + + #[test] + fn excl_borrow_used_twice_errors() { + let body = [ + Instruction::LocalGet(0), + Instruction::LocalGet(0), + Instruction::I32Add, + Instruction::Return, + ]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::ExclBorrow])); + match verify_from_module(&wasm) { + Err(VerifyError::Ownership(errs)) => { + assert!(matches!( + errs.as_slice(), + [OwnershipError::ExclBorrowAliased { func_idx: 0, param_idx: 0, count: 2 }] + )); + } + other => panic!("expected ExclBorrowAliased, got {:?}", other), + } + } + + #[test] + fn excl_borrow_used_once_is_clean() { + let body = [Instruction::LocalGet(0), Instruction::Return]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::ExclBorrow])); + assert!(verify_from_module(&wasm).is_ok()); + } + + #[test] + fn unrestricted_used_arbitrarily_is_clean() { + let body = [ + Instruction::LocalGet(0), + Instruction::LocalGet(0), + Instruction::LocalGet(0), + Instruction::I32Add, + Instruction::I32Add, + Instruction::Return, + ]; + let wasm = module_with_body(1, &body, Some(vec![OwnershipKind::Unrestricted])); + assert!(verify_from_module(&wasm).is_ok()); + } + + #[test] + fn module_without_ownership_section_is_trivially_clean() { + // No section ⇒ no constraints ⇒ Ok. + let body = [Instruction::I32Const(0), Instruction::Return]; + let wasm = module_with_body(1, &body, None); + assert!(verify_from_module(&wasm).is_ok()); + } + + #[test] + fn empty_module_is_trivially_clean() { + let module = Module::new().finish(); + assert!(verify_from_module(&module).is_ok()); + } +}