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

Ports `Tw_interface.extract_exports` + `Tw_interface.verify_cross_module`
from `hyperpolymath/affinescript/lib/tw_interface.ml`, plus a small
`CallOf(import_idx)` counter that reuses the `(min, max)` frame stack
from the C3 intra-function pass.

After this commit the C1 `extract_exports` and `verify_cross_module`
stubs are gone — the full L7+L10 boundary check is live.

What changed in `verify.rs`
---------------------------

- `OpCounter` trait and `LocalGetOf` made `pub(crate)`.
- Added `CallOf(u32)` counter (matches `Operator::Call { function_index }`).
- `count_op_range` promoted to `pub(crate)` so `cross.rs` can reuse it.

New module `cross.rs`
---------------------

  - `extract_exports(wasm_bytes) -> Result<Vec<FuncInterface>, VerifyError>`
    walks the module, filters exports to `ExternalKind::Func`, joins
    them with the ownership section by `func_idx`. Functions without an
    entry default to `(params=[], ret=Unrestricted)` — matches OCaml
    fallback.

  - `verify_cross_module(callee_iface, caller_bytes) -> Result<(), VerifyError>`:

      1. Builds a `name → &FuncInterface` lookup from `callee_iface`.
      2. Walks the caller module, tracking function-import slots in
         order (matters for the function index space). For each
         function-typed import whose name matches a callee export with
         at least one Linear param, records `(slot, name)` as a
         Linear-import-to-check.
      3. Collects every `Payload::CodeSectionEntry` body.
      4. For every (Linear import, local function body) pair, runs
         `count_op_range` with `CallOf(slot)` to compute
         `(min_calls, max_calls)`. Then:

           max_calls == 0    → skip (function doesn't call this import)
           min_calls == 0    → `LinearImportDroppedOnSomePath`
           max_calls > 1     → `LinearImportCalledMultiple { count: max_calls }`

         Both fire for `min=0, max>1` — matches OCaml.

      5. Aggregates everything into `VerifyError::Cross(Vec<CrossError>)`
         or returns `Ok(())`.

Note on the function index space: imports occupy the lowest indices, in
import-section order; local functions come after. `caller_func_idx` in
the emitted error is the **global** index (`import_count + local_idx`)
so it lines up with the callee's `func_idx` convention.

Tests
-----

40/40 unit tests pass (29 from C1-C3 + 11 new for C4):

  extract_exports
    - finds_linear_param
    - module_without_ownership_section (fallback to Unrestricted + [])
    - empty_module → []

  verify_cross_module end-to-end
    - 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 one calls the import; the other two are
         not flagged — functions aren't required to invoke every import)
    - non_linear_import_unconstrained
        (Unrestricted callee export; caller calls 3× → clean)
    - excl_borrow_import_unconstrained_at_boundary
        (ExclBorrow is intra-function only; the boundary verifier
         doesn't check it — matches the affinescript design)
    - 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 fire)

  $ cargo test -p typed-wasm-verify
  running 40 tests
  ... all pass ...
  test result: ok. 40 passed; 0 failed; 0 ignored

Crate API after this commit
---------------------------

  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>;

Follow-up
---------

  C5 (#40) — cross-compat regression test against affinescript-emitted
             modules (proves Rust verifier and OCaml verifier produce
             identical verdicts on real source-level fixtures)
  C6 (#41) — ephapax-wasm emits the `affinescript.ownership` section
             from linear-typed bindings
  C7 (#42) — ephapax-cli gets `--verify-ownership`

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: hyperpolymath