feat(tw-verify): #10 — enforce L13 module-isolation on emitted wasm (typed-wasm contract widening) (#280)

First Stage-E widening slice (the agent-scoped doable-now, high-value
level). Emitted-wasm enforcement was L7(aliasing)+L10(linearity) only.
This adds **L13 module isolation, negative form**:

- `Tw_verify.ModuleNotIsolated` + `verify_module_isolation`: a module
  that owns its own linear memory yet also imports a memory or table
  has a cross-module shared-state channel outside the declared
  function-import boundary. AffineScript codegen always emits a private
  memory and never imports one, so a violation is a codegen/isolation
  regression — exactly the class tw_verify catches on emitted wasm.
- Wired into `verify_from_module`, gated behind the same
  `affinescript.ownership` presence so the "no section ⇒ Ok" contract
  is preserved. `pp_error` case added.
- **Carrier-free**: reads only the standard wasm import/memory
  sections — NO ownership-section wire-format change, so the
  multi-producer ABI (ephapax + typed-wasm) is untouched (no unilateral
  ABI change, per the ECOSYSTEM contract).

Tests: `test/test_tw_isolation.ml` (5 cases — clean module Ok;
imported memory + own memory ⇒ ModuleNotIsolated; imported table ⇒
flagged; pure-consumer shim not in scope; no-ownership-section ⇒ Ok
contract). `dune test --force` 295/295. Zero regression.

ECOSYSTEM/TECH-DEBT coverage truthed. L1–6/L14–16 need a new
region/capability carrier section = a multi-producer ABI proposal
(filed for typed-wasm; explicitly NOT implemented unilaterally). The
Rust-verifier mirror (typed-wasm crates/typed-wasm-verify) and INT-12
C5.1 are tracked cross-repo follow-ups.

Refs #234 #235. Stage-E typed-wasm convergence widening (CONV-04).
Not Closes — Stage E continues; owner closes per ISSUE-CLOSURE.

Author: hyperpolymath

docs/ECOSYSTEM.adoc

@@ -123,10 +123,16 @@ The contract is *narrower than older prose claimed* and is exactly this:
   remain the spec of record until the cross-compat suite is supplemented
   with real AffineScript-emitted fixtures (typed-wasm "C5.1", deferred).
 . *Coverage today.* Emitted-wasm enforcement is *Level 7 (aliasing) +
-  Level 10 (linearity) only*. L1–6 and L13–16 (module isolation, session
-  protocols, resource capabilities, agent choreography) are proven at the
-  spec level but *not* enforced on AffineScript-emitted wasm. Widening this
-  is Stage E.
+  Level 10 (linearity)*, plus *Level 13 (module isolation, negative
+  form)* — `Tw_verify.verify_module_isolation` rejects a module that
+  owns linear memory yet also imports a memory/table (carrier-free; no
+  ownership-section ABI change). L1–6, L14–16 (region schema, session
+  protocols, resource capabilities, agent choreography) remain proven
+  at the spec level but *not* enforced on AffineScript-emitted wasm:
+  they require a *new carrier section* (region/type-schema or
+  capability data), which is a multi-producer ABI change coordinated
+  with `hyperpolymath/typed-wasm` + `ephapax` — not made unilaterally
+  here. Further widening + INT-12 is the rest of Stage E.
 . *Other producers.* `ephapax` (`src/ephapax-wasm`) already emits the same
   `affinescript.ownership` section and exposes the verifier via
   `ephapax compile --verify-ownership`. Any change to the section format is

docs/TECH-DEBT.adoc

@@ -225,7 +225,11 @@ structural-conservative recogniser) |S2 |open #234
 |CONV-03 |#225/#160 convergence ABI matured to "shared with Ephapax" |S1
 |partial (PR3a/b/c merged)
 |CONV-04 |Widen emitted-wasm enforcement beyond L7+L10 toward L1–6/L13–16 |S2
-|planned (Stage E)
+|L13 (module isolation, negative form) DONE —
+`Tw_verify.verify_module_isolation` (carrier-free, no ABI change).
+L1–6/L14–16 need a new carrier section = multi-producer ABI proposal
+(filed for typed-wasm; NOT unilateral). Rust-verifier mirror + C5.1 =
+cross-repo follow-ups
 |CONV-05 |INT-12: AffineScript-emitted fixtures into typed-wasm
 `crates/typed-wasm-verify/tests/cross_compat.rs` (typed-wasm "C5.1") |S1
 |planned — coordinate Refs `hyperpolymath/typed-wasm`

lib/tw_verify.ml

@@ -54,6 +54,17 @@ type ownership_error =
   | ExclBorrowAliased of { func_idx : int; param_idx : int; count : int }
   (** Level 7: ExclBorrow parameter was loaded [count] times — aliasing violation.
       An exclusive borrow must not have multiple simultaneous references. *)
+  | ModuleNotIsolated of { reason : string }
+  (** Level 13 (module isolation — the typed-wasm contract widening,
+      issue #234/#10). The emitted module owns its own linear memory
+      yet ALSO imports a memory or table: a cross-module shared-state
+      channel outside the declared function-import boundary.
+      AffineScript codegen always emits a private memory and never
+      imports one, so this is the negative L13 property and a violation
+      is a codegen/isolation regression — exactly the class
+      [tw_verify] exists to catch on emitted wasm. Additive: NO
+      ownership-section wire-format change, so the multi-producer ABI
+      (ephapax + typed-wasm) is untouched. *)
 
 (* ============================================================================
    Per-path use-range analysis
@@ -222,6 +233,40 @@ let parse_ownership_section_payload
     (func_idx, param_kinds, ret_kind)
   )
 
+(** Level 13 — module isolation (negative form). A well-isolated
+    module owns its private linear memory and reaches other modules
+    ONLY through the declared function-import boundary. If the module
+    has its own memory yet also imports a memory or a table, that
+    imported entity is a shared-state channel outside the boundary —
+    not isolated. (A module with no own memory that imports one is a
+    pure consumer shim, not in scope here; AffineScript codegen never
+    emits that shape.) Carrier-free: read only the standard wasm
+    import/memory sections, so no multi-producer ABI change. *)
+let verify_module_isolation
+    (wasm_mod : Wasm.wasm_module)
+  : ownership_error list =
+  if wasm_mod.Wasm.mems = [] then []
+  else
+    List.filter_map
+      (fun (im : Wasm.import) ->
+        match im.Wasm.i_desc with
+        | Wasm.ImportMemory ->
+          Some (ModuleNotIsolated {
+            reason =
+              Printf.sprintf
+                "module owns linear memory yet imports memory '%s.%s' \
+                 (cross-module shared memory breaks L13 isolation)"
+                im.Wasm.i_module im.Wasm.i_name })
+        | Wasm.ImportTable ->
+          Some (ModuleNotIsolated {
+            reason =
+              Printf.sprintf
+                "module owns linear memory yet imports table '%s.%s' \
+                 (externally-backed table breaks L13 isolation)"
+                im.Wasm.i_module im.Wasm.i_name })
+        | Wasm.ImportFunc _ -> None)
+      wasm_mod.Wasm.imports
+
 (** Verify a Wasm module using the embedded [affinescript.ownership] custom
     section.  This is the primary entry point for the pipeline and the CLI.
 
@@ -236,7 +281,12 @@ let verify_from_module
     Ok ()
   | Some payload ->
     let annots = parse_ownership_section_payload payload in
-    let errors = verify_module wasm_mod annots in
+    (* L7/L10 (ownership) + L13 (module isolation). The isolation check
+       is gated behind the same ownership-section presence so the
+       "no section ⇒ Ok" contract is preserved. *)
+    let errors =
+      verify_module wasm_mod annots @ verify_module_isolation wasm_mod
+    in
     if errors = [] then Ok () else Error errors
 
 (* ============================================================================
@@ -266,6 +316,8 @@ let pp_error (fmt : Format.formatter) (err : ownership_error) : unit =
       "Level 7 violation: function %d, param %d — ExclBorrow (mut) param \
        aliased (%d simultaneous references; at most 1 permitted)"
       func_idx param_idx count
+  | ModuleNotIsolated { reason } ->
+    Format.fprintf fmt "Level 13 violation: %s" reason
 
 (** Format a full verification report. Prints "OK" if no errors. *)
 let pp_report (fmt : Format.formatter) (errs : ownership_error list) : unit =

test/test_main.ml

@@ -12,4 +12,5 @@ let () =
       ("Examples", Test_golden.example_tests);
       ("Effects (#59)", Test_effects.tests);
       ("Effect-sites (#234 S2a)", Test_effect_sites.tests);
+      ("TW L13 isolation (#10)", Test_tw_isolation.tests);
     ] @ Test_e2e.tests @ Test_stdlib_aot.tests)

test/test_tw_isolation.ml

@@ -0,0 +1,94 @@
+(* SPDX-License-Identifier: PMPL-1.0-or-later *)
+(* SPDX-FileCopyrightText: 2026 hyperpolymath *)
+
+(* #10 / typed-wasm contract widening: L13 module-isolation (negative
+   form) enforced on emitted wasm by [Tw_verify.verify_module_isolation]
+   / [verify_from_module]. Additive — no ownership-section ABI change. *)
+
+open Affinescript
+
+let mem () : Wasm.memory = { Wasm.mem_type = { Wasm.lim_min = 1; lim_max = None } }
+
+let imp m n d : Wasm.import = { Wasm.i_module = m; i_name = n; i_desc = d }
+
+(* count=0 ownership payload (u32le 0) — present so verify_from_module
+   does not short-circuit on "no ownership section ⇒ Ok". *)
+let own_section = ("affinescript.ownership", Bytes.make 4 '\000')
+
+let is_isolation_err = function
+  | Tw_verify.ModuleNotIsolated _ -> true
+  | _ -> false
+
+let test_clean_module_ok () =
+  let m =
+    { (Wasm.empty_module ()) with
+      Wasm.mems = [ mem () ];
+      imports = [ imp "Other" "callee" (Wasm.ImportFunc 0) ];
+      custom_sections = [ own_section ] }
+  in
+  match Tw_verify.verify_from_module m with
+  | Ok () -> ()
+  | Error errs ->
+    Alcotest.failf "clean isolated module flagged: %d errs" (List.length errs)
+
+let test_imported_memory_flagged () =
+  let m =
+    { (Wasm.empty_module ()) with
+      Wasm.mems = [ mem () ];
+      imports = [ imp "Host" "memory" Wasm.ImportMemory ];
+      custom_sections = [ own_section ] }
+  in
+  match Tw_verify.verify_from_module m with
+  | Ok () -> Alcotest.fail "imported memory + own memory must violate L13"
+  | Error errs ->
+    Alcotest.(check bool) "ModuleNotIsolated reported" true
+      (List.exists is_isolation_err errs)
+
+let test_imported_table_flagged () =
+  let m =
+    { (Wasm.empty_module ()) with
+      Wasm.mems = [ mem () ];
+      imports = [ imp "Host" "tbl" Wasm.ImportTable ];
+      custom_sections = [ own_section ] }
+  in
+  Alcotest.(check bool) "imported table flagged" true
+    (List.exists is_isolation_err (Tw_verify.verify_module_isolation m))
+
+let test_no_own_memory_not_in_scope () =
+  (* A pure consumer shim (no own memory) importing a memory is not the
+     negative-L13 shape AffineScript emits; not flagged. *)
+  let m =
+    { (Wasm.empty_module ()) with
+      Wasm.mems = [];
+      imports = [ imp "Host" "memory" Wasm.ImportMemory ];
+      custom_sections = [ own_section ] }
+  in
+  Alcotest.(check int) "no isolation errors" 0
+    (List.length (Tw_verify.verify_module_isolation m))
+
+let test_no_ownership_section_contract () =
+  (* Even a would-be violation: no ownership section ⇒ Ok (the
+     pre-existing contract is preserved; isolation is gated behind it). *)
+  let m =
+    { (Wasm.empty_module ()) with
+      Wasm.mems = [ mem () ];
+      imports = [ imp "Host" "memory" Wasm.ImportMemory ];
+      custom_sections = [] }
+  in
+  match Tw_verify.verify_from_module m with
+  | Ok () -> ()
+  | Error _ -> Alcotest.fail "no ownership section must remain Ok"
+
+let tests =
+  [
+    Alcotest.test_case "clean isolated module is Ok" `Quick
+      test_clean_module_ok;
+    Alcotest.test_case "imported memory + own memory violates L13" `Quick
+      test_imported_memory_flagged;
+    Alcotest.test_case "imported table violates L13" `Quick
+      test_imported_table_flagged;
+    Alcotest.test_case "no-own-memory consumer not in scope" `Quick
+      test_no_own_memory_not_in_scope;
+    Alcotest.test_case "no ownership section ⇒ Ok (contract)" `Quick
+      test_no_ownership_section_contract;
+  ]