feat(verify): cross-module boundary verifier (C4)

[hyperpolymath]

Summary

• Ports Tw_interface.extract_exports + Tw_interface.verify_cross_module from hyperpolymath/affinescript/lib/tw_interface.ml.
• Replaces the C1 extract_exports / verify_cross_module stubs — the full L7+L10 boundary check is now live.
• Reuses the C3 (min, max) frame-stack machinery via a new CallOf(import_idx) OpCounter — no algorithm duplication.
• 40/40 tests pass (29 from C1-C3 + 11 new for C4).

How the boundary check works

verify_cross_module(callee_iface, caller_bytes):

1. Build name → &FuncInterface map from callee_iface.
2. Walk caller module; for each function-typed import whose name matches a callee export with a Linear param, record (slot, name).
3. Collect every local function body in caller.
4. For each (Linear import × local fn) pair, run count_op_range with CallOf(slot):

(min, max)	Verdict
max == 0	skipped (fn doesn't call this import)
min == 0, max ≥ 1	LinearImportDroppedOnSomePath
max > 1	LinearImportCalledMultiple { count }
min == 0, max > 1	both above fire (matches OCaml)

5. Aggregate into VerifyError::Cross(Vec<CrossError>) or Ok(()).

Test coverage (11 new)

extract_exports (3)

• finds Linear-param export through the ownership section
• module without ownership section → exports show as Unrestricted with empty param_kinds (matches OCaml fallback)
• empty module → empty result

verify_cross_module end-to-end (8)

• linear_import_called_exactly_once_is_clean
• linear_import_called_twice_errors → LinearImportCalledMultiple{count:2}
• linear_import_dropped_on_some_path_errors → LinearImportDroppedOnSomePath
• linear_import_never_called_by_some_caller_fns_is_clean (3 caller fns; only the first calls the import; the others aren't flagged — fns aren't obligated to invoke every import)
• non_linear_import_unconstrained (Unrestricted callee → caller can call freely)
• excl_borrow_import_unconstrained_at_boundary (ExclBorrow is intra-function only by design; boundary verifier skips it — matches affinescript)
• linear_import_unmatched_export_is_ignored (caller imports a name the callee doesn't export → trivially Ok)
• linear_import_drop_and_dup_both_fire (if(lg0){call;call} → min=0, max=2 → both error variants emitted for the same pair)

Crate API after this PR

pub mod cross;
pub mod section;
pub mod verify;
pub use cross::{extract_exports, verify_cross_module};
pub use section::{build_ownership_section_payload, parse_ownership_section_payload, OwnershipEntry};
pub use verify::{count_uses_range, verify_function};

pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError>;

Stub functions are gone; every public surface from C1 is now backed by a real implementation.

Stacking

This is the first non-stacked PR in the C-series — branches off main (which already has C1+C2+C3 merged). Self-contained.

Follow-up

• C5 — cross-compat regression test against affinescript-emitted modules (proves Rust and OCaml verifiers agree on real source fixtures)
• C6/C7 — hyperpolymath/ephapax consumer wiring (separate PRs there)

Closes #39 once merged.