feat(l13): region-imports carrier — proposal 0003 accepted, codec + link-graph verifier + producer emission (#140) (#198)

Increment 1 of 3 on the independence construction path (owner-ratified
sequence).

Closes the **L13 positive-form** gap: `typedwasm.region-imports` now
exists end-to-end — codec + module-local pass + `verify_link_graph`
cross-module `SchemaSub` certification in `typed-wasm-verify` (behind
`unstable-l13-imports`), and producer emission from real `.twasm` source
(`import region Entity from "physics" { … }`) in `typed-wasm-codegen`.
The examples/02 killer feature — one module exports a schema, others
import subsets, agreement certified before anything runs — round-trips
in-process for the first time.

- Proposal 0003: `[draft]` → `[accepted]` (2026-07-07) → **ADR-0007**;
wire format as specced (LEB128 + u16le version), with an implementation
note pinning sibling-codec conventions.
- `target_region` v1.1 high-bit value-space extension implemented
(`TARGET_REGION_IMPORT_BIT`), non-breaking for v1 consumers.
- Full `RegionImportsError` taxonomy from the proposal's §Consumer
obligations; 15 new L13 tests + 5 codec tests; **162 workspace tests, 0
failures**.
- Union-merge rule for repeated `(producer, region)` imports in one file
(examples/02 holds three conceptual modules) — keeps the carrier's
uniqueness obligation.
- Cross-repo adoption issues for affinescript + ephapax drafted in
`docs/developer/cross-repo-issues-proposal-0003-adoption.adoc`
(automated filing was permission-blocked — ready to paste).
- Parser module header rewritten per ADR-0006 (still said "stopgap until
the AffineScript front-end").

Part of #140 (remaining there: producer-emitted c5_real differential
fixture pair; per-module split of multi-file sources).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

LEVEL-STATUS.md

@@ -1,4 +1,5 @@
 # SPDX-License-Identifier: CC-BY-SA-4.0
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # typed-wasm Level Achievement Status
 
 ## Versioning Scheme (revised 2026-04-13 — typed-wasm-first rollout)
@@ -143,7 +144,7 @@ pins affinescript SHA for drift detection).
 | L7 (aliasing) | **YES** | `verify_function` per-path use-range |
 | L10 (linearity) | **YES** | `verify_function` per-path use-range |
 | L13 (module isolation, negative form) | **YES** | `verify_from_module`, gated on ownership-section presence (PR #37, 2026-05-19) |
-| L13 (cross-module schema agreement, positive form) | **proposal-stage** | `typedwasm.region-imports` carrier — proposal 0003 `[draft]` (`docs/proposals/0003`); blocked on producer-side multi-module emission |
+| L13 (cross-module schema agreement, positive form) | **YES (import-bound, carrier-backed)** | `typedwasm.region-imports` carrier — proposal 0003 `[accepted]` 2026-07-07 → ADR-0007; `verify_region_imports_from_module` (module-local) + `verify_link_graph` (cross-module `SchemaSub` → `CompatCertificate`s); gated `cargo feature = "unstable-l13-imports"`; in-tree producer emits from `import region … from "…" { … }` source (`tests/example02.rs`) |
 | L2 (region binding) | **YES** (carrier-backed) | `verify_access_sites_from_module` PR #109; reads `typedwasm.regions` + `typedwasm.access-sites` (proposals 0001 + 0002 `[accepted]` 2026-05-30; codec PR #107; gated `cargo feature = "unstable-l2"`) |
 | L3–L6 (type-compat, null, bounds, result-type) | **YES** (carrier-backed, schema half) | `typedwasm.regions` codec PR #107; cross-checks against `Region.idr::WasmType`, `Pointer.idr::Nullability`, cardinality. Per-access enforcement gated on producer codegen of access-sites (`affinescript#462`, `ephapax#251`). |
 | L15 (resource capabilities, L15-A/B) | **YES** (carrier-backed) | `verify_capabilities_from_module` PR #109; reads `typedwasm.capabilities` (proposal 0001 `[accepted]`; codec PR #107; gated `cargo feature = "unstable-l15"`). L15-C deferred to proposal 0004 `[draft]`. |
@@ -158,9 +159,11 @@ pins affinescript SHA for drift detection).
    (access-sites codegen, open), `ephapax#221` (Ty::Borrow surfacing,
    open), `ephapax#251` (access-sites codegen, filed 2026-05-30),
    `ephapax#250` (Codegen dead-fields cleanup, ✅ merged 2026-05-30).
-2. **L13 cross-module (positive form)** — proposal 0003 `[draft]`
-   (`docs/proposals/0003`). Gated on producer-side multi-module
-   emission (AffineScript Roadmap C3 / Ephapax not yet on roadmap).
+2. **L13 cross-module (positive form)** — DONE in-tree (2026-07-07):
+   proposal 0003 `[accepted]` → ADR-0007; codec + `verify_link_graph`
+   behind `unstable-l13-imports`; in-tree producer emits from source.
+   Sibling-producer adoption (AffineScript Roadmap C3 / Ephapax)
+   tracked by cross-repo issues.
 3. **L15-C (call-graph monotonicity)** — proposal 0004 `[draft]`
    (`docs/proposals/0004`). Gated on producer-side L15-A emission
    (Roadmap C2 not started in either producer).

crates/typed-wasm-codegen/Cargo.toml

@@ -25,7 +25,7 @@ wasmprinter = "=0.252.0"
 # The producer reuses the verifier's own carrier encoders so the emitted
 # typedwasm.regions / typedwasm.access-sites bytes cannot drift from the
 # decoder the verifier runs. `unstable-l2` gates those encoders.
-typed-wasm-verify = { path = "../typed-wasm-verify", features = ["unstable-l2"] }
+typed-wasm-verify = { path = "../typed-wasm-verify", features = ["unstable-l2", "unstable-l13-imports"] }
 
 [dev-dependencies]
 # Round-trip test validates the emitted module is well-formed wasm before

crates/typed-wasm-codegen/README.md

@@ -58,4 +58,4 @@ cargo test -p typed-wasm-codegen
 
 - **#127** — codegen coverage across all 10 levels × all 6 examples (and the front-end → IR JSON seam).
 - **#130** — promote the round-trip tests into the ECHIDNA property corpus.
-- **L13 positive-form / region-imports** — shared-region schema agreement (`examples/02`); rides the `typedwasm.region-imports` carrier (proposal 0003 `[draft]`, no verifier pass yet).
+- **L13 positive-form / region-imports** — **done** (issue #140): `import region … from "…" { … }` parses into `Module::region_imports`, emits the `typedwasm.region-imports` carrier (proposal 0003 `[accepted]` / ADR-0007), and `verify_link_graph` certifies cross-module schema agreement (`tests/example02.rs`).

crates/typed-wasm-codegen/src/lib.rs

@@ -38,10 +38,13 @@ use typed_wasm_verify::section::{
     build_access_sites_section_payload, AccessSiteEntry, ACCESS_SITE_UNPINNED, NO_TARGET_REGION,
 };
 use typed_wasm_verify::{
-    build_ownership_section_payload, build_regions_section_payload, CrossError, FieldEntry, FieldKind,
-    Nullability, OwnershipError, OwnershipEntry, OwnershipKind, RegionEntry, VerifyError, WasmTy,
+    build_ownership_section_payload, build_region_imports_section_payload,
+    build_regions_section_payload, CrossError, FieldEntry, FieldKind,
+    Nullability, OwnershipError, OwnershipEntry, OwnershipKind, RegionEntry,
+    RegionImportEntry, VerifyError, WasmTy,
     verify_access_sites_from_module, verify_from_module,
     ACCESS_SITES_SECTION_NAME, OWNERSHIP_SECTION_NAME, REGIONS_SECTION_NAME,
+    REGION_IMPORTS_SECTION_NAME,
 };
 use wasm_encoder::{
     CodeSection, CustomSection, EntityType, ExportKind, ExportSection, Function, FunctionSection,
@@ -321,6 +324,12 @@ pub struct Module {
     /// param_kinds, ret_kind)`. Emitted as the `typedwasm.ownership`
     /// carrier; empty = no L7/L10 carrier.
     pub ownership: Vec<(usize, Vec<Ownership>, Ownership)>,
+    /// Cross-module region imports (`import region X from "module"`),
+    /// each carrying the EXPECTED schema. Emitted as the
+    /// `typedwasm.region-imports` carrier (proposal 0003 / ADR-0007,
+    /// L13 positive form); empty = no carrier. Entries reuse the
+    /// verifier's own type so bytes cannot drift from its decoder.
+    pub region_imports: Vec<RegionImportEntry>,
 }
 
 // ----------------------------------------------------------------------
@@ -522,13 +531,23 @@ pub fn emit(module: &Module) -> Vec<u8> {
             data: payload.as_slice().into(),
         });
     }
-    if !region_entries.is_empty() {
+    // Region imports require their dependent regions carrier (proposal
+    // 0003 §Producer obligations #1) — emit regions (even if empty)
+    // whenever an import table is present.
+    if !region_entries.is_empty() || !module.region_imports.is_empty() {
         let payload = build_regions_section_payload(&region_entries);
         wasm.section(&CustomSection {
             name: REGIONS_SECTION_NAME.into(),
             data: payload.as_slice().into(),
         });
     }
+    if !module.region_imports.is_empty() {
+        let payload = build_region_imports_section_payload(&module.region_imports);
+        wasm.section(&CustomSection {
+            name: REGION_IMPORTS_SECTION_NAME.into(),
+            data: payload.as_slice().into(),
+        });
+    }
     if !access_entries.is_empty() {
         let payload = build_access_sites_section_payload(&access_entries);
         wasm.section(&CustomSection {
@@ -670,6 +689,7 @@ pub fn example01() -> Module {
         imports: vec![],
         funcs,
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 
@@ -820,6 +840,7 @@ pub fn paint_type_tile() -> Module {
         imports: vec![],
         funcs,
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 
@@ -945,6 +966,7 @@ pub fn paint_type_layer() -> Module {
         imports: vec![],
         funcs,
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 
@@ -986,6 +1008,7 @@ pub fn multimodule_callee() -> Module {
             export: true,
         }],
         ownership: vec![(0, vec![Ownership::Linear], Ownership::Unrestricted)],
+        region_imports: vec![],
     }
 }
 
@@ -1017,6 +1040,7 @@ pub fn multimodule_caller(call_count: u32) -> Module {
             export: false,
         }],
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 

crates/typed-wasm-codegen/src/parser.rs

@@ -1,16 +1,21 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 //
-//! Minimal .twasm text parser for codegen v0.
+//! The canonical `.twasm` front-end (ADR-0006).
 //!
-//! This module provides a Rust-native parser for the typed-wasm surface syntax
-//! as a stopgap until the AffineScript front-end (ADR-0004, issue #127) lands.
-//! It is intentionally limited to the subset needed by paint-type schemas and
-//! example-01, not the full .twasm language.
+//! Hand-written Rust parser for the typed-wasm surface syntax: the
+//! `source → IR → emit → verify` reference path. Parses all six
+//! canonical `examples/*.twasm` (round-tripped by `tests/corpus.rs`),
+//! recording region schemas, ownership qualifiers (`own`/`&mut`/`&` →
+//! the `typedwasm.ownership` carrier) and cross-module region imports
+//! (`import region … from "…" { … }` → the `typedwasm.region-imports`
+//! carrier, ADR-0007).
 //!
-//! This parser does NOT duplicate the full AffineScript front-end — it only handles
-//! the specific schemas needed to unblock paint-type#39 and demonstrate the
-//! codegen path. Full .twasm parsing remains deferred to the AffineScript front-end.
+//! Known gaps against `spec/grammar.ebnf` are tracked debt (ADR-0006
+//! §Consequences): non-lowerable statement bodies fall back to
+//! type-correct stubs, and `if`/`else` / `region.scan` control flow is
+//! simplified. The AffineScript front-end (`src/parser/*.affine`) is a
+//! reference implementation, not a dependency.
 
 use crate::{Field, FieldTy, Memory, Module, PtrKind, Region, Scalar, Wty};
 use std::collections::HashMap;
@@ -31,6 +36,7 @@ struct Parser<'a> {
     imports: Vec<crate::Import>,
     funcs: Vec<crate::Func>,
     ownership: Vec<(usize, Vec<crate::Ownership>, crate::Ownership)>,
+    region_imports: Vec<typed_wasm_verify::RegionImportEntry>,
 }
 
 impl<'a> Parser<'a> {
@@ -44,6 +50,7 @@ impl<'a> Parser<'a> {
             imports: Vec::new(),
             funcs: Vec::new(),
             ownership: Vec::new(),
+            region_imports: Vec::new(),
         }
     }
 
@@ -78,6 +85,7 @@ impl<'a> Parser<'a> {
             imports: self.imports,
             funcs: self.funcs,
             ownership: self.ownership,
+            region_imports: self.region_imports,
         })
     }
 
@@ -1242,36 +1250,163 @@ impl<'a> Parser<'a> {
         self.expect("import")?;
         self.skip_whitespace();
         // Optional `region` keyword: `import region Name from "module" ...`
-        if self.peek_word("region") {
+        let is_region_import = if self.peek_word("region") {
             self.expect("region")?;
             self.skip_whitespace();
-        }
-        let _name = self.parse_ident();
+            true
+        } else {
+            false
+        };
+        let name = self.parse_ident();
         self.skip_whitespace();
         self.expect("from")?;
         self.skip_whitespace();
         // Module source: a quoted string ("game_server") or a bare ident.
-        if self.peek_char('"') {
+        let producer_module = if self.peek_char('"') {
             self.expect("\"")?;
+            let start = self.pos;
             while self.pos < self.src.len() && self.src.as_bytes()[self.pos] != b'"' {
                 self.pos += 1;
             }
+            let module = self.src.get(start..self.pos).unwrap_or("").to_string();
             self.expect("\"")?;
+            module
         } else {
-            let _module = self.parse_ident();
-        }
+            self.parse_ident()
+        };
         self.skip_whitespace();
-        // Either a re-declaration body `{ ... }` (multi-module) or a `;`.
+        // Either an expected-schema body `{ ... }` (multi-module region
+        // import, L13 positive form — recorded into the
+        // `typedwasm.region-imports` carrier) or a bare `;`.
         if self.peek_char('{') {
             self.expect("{")?;
-            self.skip_to_brace_close();
+            if is_region_import {
+                let expected = self.parse_expected_import_fields()?;
+                self.record_region_import(producer_module, name, expected)?;
+            } else {
+                self.skip_to_brace_close();
+            }
         } else if self.peek_char(';') {
             self.expect(";")?;
+            if is_region_import {
+                // No expected schema listed: the import asserts presence
+                // only (zero expected fields — vacuous agreement).
+                self.record_region_import(producer_module, name, Vec::new())?;
+            }
+        }
+        Ok(())
+    }
+
+    /// Parse the field list of an `import region … from "…" { … }` body
+    /// into EXPECTED-schema entries (proposal 0003). Cursor is just past
+    /// the `{`; consumes through the matching `}`. v1 restriction:
+    /// scalar fields only.
+    fn parse_expected_import_fields(
+        &mut self,
+    ) -> Result<Vec<typed_wasm_verify::FieldEntry>, String> {
+        let mut fields = Vec::new();
+        loop {
+            self.skip_whitespace();
+            if self.peek_char('}') {
+                self.expect("}")?;
+                break;
+            }
+            if self.pos >= self.src.len() {
+                return Err("unterminated import region body".into());
+            }
+            let fname = self.parse_ident();
+            if fname.is_empty() {
+                return Err("expected field name in import region body".into());
+            }
+            self.skip_whitespace();
+            self.expect(":")?;
+            self.skip_whitespace();
+            let (fty, cardinality) = self.parse_field_type()?;
+            let wasm_ty = match fty {
+                FieldTy::Scalar(s) => scalar_to_wire_ty(&s),
+                FieldTy::Ptr { .. } => {
+                    return Err(format!(
+                        "import region field '{fname}' is pointer-typed — \
+                         pointer fields in imported region schemas are not \
+                         supported in v1 (proposal 0003)"
+                    ));
+                }
+            };
+            fields.push(typed_wasm_verify::FieldEntry {
+                name: fname,
+                kind: typed_wasm_verify::FieldKind::Scalar,
+                wasm_ty,
+                target_region: crate::NO_TARGET_REGION,
+                nullability: typed_wasm_verify::Nullability::NonNull,
+                cardinality,
+            });
+            self.skip_whitespace();
+            if self.peek_char(';') {
+                self.expect(";")?;
+            }
+        }
+        Ok(fields)
+    }
+
+    /// Record a region import, union-merging repeated imports of the
+    /// same `(producer, region)` pair — a single `.twasm` file may hold
+    /// several conceptual modules (examples/02) that each declare their
+    /// own expected subset. Conflicting declarations for the same field
+    /// are a source error; the emitted carrier keeps pairs unique
+    /// (proposal 0003 `DuplicateImport` obligation).
+    fn record_region_import(
+        &mut self,
+        producer_module: String,
+        region_name: String,
+        expected: Vec<typed_wasm_verify::FieldEntry>,
+    ) -> Result<(), String> {
+        if let Some(existing) = self
+            .region_imports
+            .iter_mut()
+            .find(|e| e.producer_module == producer_module && e.region_name == region_name)
+        {
+            for f in expected {
+                match existing.expected_fields.iter().find(|e| e.name == f.name) {
+                    None => existing.expected_fields.push(f),
+                    Some(prev) if *prev == f => {}
+                    Some(prev) => {
+                        return Err(format!(
+                            "conflicting expected types for imported field \
+                             '{}.{}' from \"{}\": {:?} vs {:?}",
+                            region_name, f.name, producer_module, prev.wasm_ty, f.wasm_ty
+                        ));
+                    }
+                }
+            }
+        } else {
+            self.region_imports.push(typed_wasm_verify::RegionImportEntry {
+                producer_module,
+                region_name,
+                expected_fields: expected,
+            });
         }
         Ok(())
     }
 }
 
+/// `.twasm` scalar type → wire `WasmTy` (typedwasm.regions enum).
+fn scalar_to_wire_ty(s: &Scalar) -> typed_wasm_verify::WasmTy {
+    use typed_wasm_verify::WasmTy as W;
+    match s {
+        Scalar::I8 => W::I8,
+        Scalar::I16 => W::I16,
+        Scalar::I32 => W::I32,
+        Scalar::I64 => W::I64,
+        Scalar::U8 => W::U8,
+        Scalar::U16 => W::U16,
+        Scalar::U32 => W::U32,
+        Scalar::U64 => W::U64,
+        Scalar::F32 => W::F32,
+        Scalar::F64 => W::F64,
+        Scalar::Bool => W::WBool,
+    }
+}
+
 fn scalar_byte_size(s: &Scalar) -> u32 {
     match s {
         Scalar::I8 | Scalar::U8 => 1,

crates/typed-wasm-codegen/tests/access_typing.rs

@@ -91,6 +91,7 @@ fn rig(region: Region, func: Func) -> Module {
         imports: vec![],
         funcs: vec![func],
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 

crates/typed-wasm-codegen/tests/corpus.rs

@@ -154,6 +154,7 @@ fn gen_valid(seed: u64) -> Module {
         imports: vec![],
         funcs,
         ownership: vec![],
+        region_imports: vec![],
     }
 }
 
@@ -619,6 +620,7 @@ fn one_func_module(kind: Ownership, body: Vec<Op>) -> Module {
             export: true,
         }],
         ownership: vec![(0, vec![kind], Ownership::Unrestricted)],
+        region_imports: vec![],
     }
 }
 

crates/typed-wasm-codegen/tests/errors.rs

@@ -39,6 +39,7 @@ fn double_free_gives_named_actionable_message() {
             export: true,
         }],
         ownership: vec![(0, vec![Ownership::Linear], Ownership::Unrestricted)],
+        region_imports: vec![],
     };
     let diagnostics = self_verify(&module).expect_err("double-free must be rejected");
     let joined = diagnostics.join("\n");