feat(verify): per-path use-range analysis + intra-fn verifier (C3)

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 <noreply@anthropic.com>

Author: hyperpolymath

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.