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

[hyperpolymath]

Summary

• Ports Tw_verify.count_uses_range + verify_function + verify_from_module from hyperpolymath/affinescript/lib/tw_verify.ml.
• Replaces C1's todo!() stub: verify_from_module(wasm_bytes) now actually enforces L7 (aliasing) and L10 (linearity).
• 29/29 tests pass (10 algorithmic + 9 end-to-end + 10 inherited from C1/C2).

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	Meaning
Plain { min, max }	Block, Loop, or the implicit body scope
IfThen { then_min, then_max }	If before any Else is seen
IfElse { then_min, then_max, else_min, else_max }	If after Else (then-side frozen)

Transitions:

Block / Loop      → push Plain
If                → push IfThen
Else              → IfThen → IfElse (freeze then-totals)
End               → pop, collapse, add to parent:
                      Plain                 → (min,  max)
                      IfThen, no else seen  → (0,    then_max)
                      IfElse                → (min(t,e), max(t,e))
LocalGet n        → if n matches, add (1,1) to top frame's active side
Other             → no-op

The per-counter logic sits behind a private OpCounter trait so C4 can reuse the same machinery with a Call-based counter.

Per-function rules (verbatim port of OCaml verify_function)

Kind	Rule
Linear	max=0 → LinearNotUsed; min=0, max≥1 → LinearDroppedOnSomePath; max>1 → LinearUsedMultiple. Both drop+dup can fire for min=0, max>1.
ExclBorrow	max>1 → ExclBorrowAliased
Unrestricted / SharedBorrow	no constraints

Module-level entry

verify_from_module(wasm_bytes):

1. Single wasmparser pass over the module:
   • Tally import_count for function-index translation
   • Capture affinescript.ownership custom section (if any)
   • Collect every Payload::CodeSectionEntry body in order
2. No section ⇒ trivially Ok(())
3. Parse the section (using C2's parse_ownership_section_payload)
4. For each entry: translate global func_idx to body index by subtracting import_count; skip imports + out-of-range entries (matches OCaml short-circuits)
5. Aggregate per-fn violations into VerifyError::Ownership(Vec<OwnershipError>) or return Ok(())

Tests

$ cargo test -p typed-wasm-verify
running 29 tests
... (10 section + 1 kind + 18 verify) ...
test result: ok. 29 passed; 0 failed; 0 ignored

Coverage:

• count_uses_range layer — every transition (no uses, one use, two same-path, both-branches, then-only, asymmetric-counts, Block passthrough, Loop passthrough, nested-If-inner-then-only)
• verify_from_module end-to-end — every error variant + clean paths (Linear×{used-once,not-used,dropped,used-twice}, ExclBorrow×{once,twice}, Unrestricted unconstrained, no-section, empty-module)

Stacking

Stacked on top of #20 (C2 section codec) → on top of #19 (C1 scaffold). Merge order: #19 → #20 → this. Each downstream PR's base retargets to main automatically as the upstream merges.

Follow-up

• C4 — port the cross-module boundary verifier (same (min,max) frame stack applied to Call operators)
• C5 — cross-compat regression test against affinescript-emitted modules
• C6/C7 — hyperpolymath/ephapax consumer wiring

Closes #38 once merged.