feat(verify): L13 region-imports codec + self-consistency pass (proposal 0003) (#154)

## Summary

Pre-stages typed-wasm **proposal 0003** (`typedwasm.region-imports`
custom section) behind a new `unstable-l13-imports` cargo feature.
Closes the verifier-pass slice of **#140** bullet 1.

- **Codec** (`section.rs`): `RegionImportEntry` / `ImportedFieldEntry`,
`parse_/build_region_imports_section_payload`, `IMPORT_TABLE_BASE` (=
`0x8000_0000`).
- **Public API** (`lib.rs`): `REGION_IMPORTS_SECTION_NAME`,
`RegionImportsError` enum (5 variants),
`verify_region_imports_from_module` entry point.
- **In-module self-consistency pass** (`verify.rs`):
- `MissingDependentRegions` — region-imports without regions (producer
obligation #1)
- `MissingDependentRegionImports` — regions has import-bit
`target_region` but no region-imports section
- `DuplicateImport` — non-unique `(producer_module_name, region_name)`
pairs
- `PointerInImportNotSupportedInV1` — v1 restriction (producer
obligation #5)
- `ImportTargetOutOfRange` — import-bit `target_region` resolves past
the import-table bounds

## Scope (deliberately partial)

This is the unblocking half of #140 bullet 1. **Out of scope:**

- Cross-module schema agreement (`SchemaSub expected actual` from
`MultiModule.idr`). Defers to a future `verify_link_graph(modules:
&[Module])` pass per proposal 0003 §"Open questions" #4 default option
a.
- Producer codegen for the new section. AffineScript and Ephapax still
emit single-module — codegen for both lands separately (AffineScript
roadmap C3 etc., proposal 0003 §"Coordination with downstream
producers").
- Wiring `examples/02-multi-module.twasm` through the producer — blocked
by #127 (front-end → IR seam), per #140 bullet 3.

## Feature gate

`unstable-l13-imports = ["unstable-l2"]` — implies l2 because the
import-bit convention extends `typedwasm.regions`'s `target_region`
value space. Default verifier surface is unchanged; this is opt-in until
proposal 0003 leaves `[draft]`.

## Test plan

- [x] `cargo check -p typed-wasm-verify` (default features) — clean
- [x] `cargo check -p typed-wasm-verify --all-features` — clean
- [x] `cargo check -p typed-wasm-verify --features unstable-l13-imports`
— clean
- [x] `cargo test -p typed-wasm-verify --features unstable-l13-imports`
— **85 tests pass** (66 baseline + 19 new):
- 9 codec tests (roundtrip, truncation, UTF-8-lossy, version mismatch,
pointer-kinds tolerance, large field counts)
- 10 verifier-pass tests (all 5 error variants + clean path +
NO_TARGET_REGION sentinel safety + empty-table)
- [x] `cargo clippy -p typed-wasm-verify --features
unstable-l13-imports` — clippy-clean for new code (one pre-existing
collapsible-match warning at `verify.rs:323`)

## Refs

Refs #140 (bullet 1 verifier-pass slice), refs #95, refs #50, part of
proposal 0003 §"Acceptance criteria" items 3 + 4.

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

crates/typed-wasm-verify/Cargo.toml

@@ -30,6 +30,18 @@ unstable-l2 = []
 # `FunctionCapabilities` + `verify_capabilities_from_module` (PR #109).
 # L15-C (per-call-site grants) is a separate proposal 0004 (`[draft]`).
 unstable-l15 = []
+# L13 cross-module region-imports carrier for typed-wasm proposal 0003
+# (`[draft]`, typed-wasm#140 refs #95). Implies `unstable-l2`: the import
+# table cross-references `typedwasm.regions` field entries via the
+# high-bit `target_region` convention. Enables:
+#   - `parse_region_imports_section_payload` /
+#     `build_region_imports_section_payload` +
+#     `RegionImportEntry` / `ImportedFieldEntry` + `IMPORT_TABLE_BASE`
+#   - `verify_region_imports_from_module` (this PR) — self-consistency
+#     only; cross-module schema agreement (`SchemaSub`) defers to a
+#     later `verify_link_graph` pass per proposal 0003 §"Open
+#     questions" #4 default option a.
+unstable-l13-imports = ["unstable-l2"]
 
 [dependencies]
 # Exact pins: wasmparser's 0.x line ships API breaks on every minor bump

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

@@ -1,4 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 //
 // typed-wasm post-codegen verifier.
 //
@@ -31,6 +32,12 @@ pub use section::{
     Nullability, RegionEntry, WasmTy, REGIONS_SECTION_VERSION,
 };
 
+#[cfg(feature = "unstable-l13-imports")]
+pub use section::{
+    build_region_imports_section_payload, parse_region_imports_section_payload,
+    ImportedFieldEntry, RegionImportEntry, IMPORT_TABLE_BASE, REGION_IMPORTS_SECTION_VERSION,
+};
+
 /// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum.
 /// Wire encoding in the `typedwasm.ownership` custom section: a single
 /// u8 per kind, values 0/1/2/3 as below.
@@ -148,6 +155,14 @@ pub const CAPABILITIES_SECTION_NAME: &str = "typedwasm.capabilities";
 #[cfg(feature = "unstable-l2")]
 pub const ACCESS_SITES_SECTION_NAME: &str = "typedwasm.access-sites";
 
+/// Custom-section name carrying cross-module region-import declarations
+/// (proposal 0003, typed-wasm#140 refs #95). Companion to
+/// `typedwasm.regions`: a module's `target_region` foreign keys with the
+/// import-table bit set (`>= IMPORT_TABLE_BASE`) resolve through this
+/// section's entries. UNSTABLE.
+#[cfg(feature = "unstable-l13-imports")]
+pub const REGION_IMPORTS_SECTION_NAME: &str = "typedwasm.region-imports";
+
 /// L15 capability-section violation (parsing succeeded, content invalid).
 #[cfg(feature = "unstable-l15")]
 #[derive(Debug, Clone, PartialEq, Eq, Error)]
@@ -203,6 +218,62 @@ pub enum AccessSiteError {
     },
 }
 
+/// L13 region-imports section violation. Self-consistency only; cross-
+/// module schema-agreement (`SchemaSub expected actual`, `SchemaImportMismatch`)
+/// belongs to a future `verify_link_graph` pass (proposal 0003 §"Open
+/// questions" #4 default option a).
+#[cfg(feature = "unstable-l13-imports")]
+#[derive(Debug, Clone, PartialEq, Eq, Error)]
+pub enum RegionImportsError {
+    /// Proposal 0003 §"Producer obligations" #1: a module emitting
+    /// `typedwasm.region-imports` MUST also emit `typedwasm.regions` (the
+    /// import-table foreign keys in `typedwasm.regions`'s field entries
+    /// would otherwise dangle).
+    #[error("Level 13 violation: typedwasm.region-imports section emitted without companion typedwasm.regions section (MissingDependentCarrier)")]
+    MissingDependentRegions,
+
+    /// Inverse companion check: a `typedwasm.regions` field entry has a
+    /// `target_region` value with the import-table bit set, but no
+    /// `typedwasm.region-imports` section is present to resolve it
+    /// against. Emitted at most once per module (further occurrences
+    /// would spam).
+    #[error("Level 13 violation: typedwasm.regions has target_region with import-table bit set (value {target_region:#010x}) but no typedwasm.region-imports section present to resolve it")]
+    MissingDependentRegionImports { target_region: u32 },
+
+    /// Proposal 0003 §"Wire format" Notes: imports MUST have unique
+    /// `(producer_module_name, region_name)` pairs.
+    #[error("Level 13 violation: duplicate import: (producer_module_name = {producer_module_name:?}, region_name = {region_name:?}) appears at import-table indices {first_idx} and {duplicate_idx}")]
+    DuplicateImport {
+        first_idx: u32,
+        duplicate_idx: u32,
+        producer_module_name: String,
+        region_name: String,
+    },
+
+    /// Proposal 0003 §"Producer obligations" #5: imported regions MUST
+    /// have scalar-only expected schemas in v1. Transitive pointer-chain
+    /// resolution is deferred to v2 (see proposal 0003 §"Open questions" #1).
+    #[error("Level 13 violation: import-table entry {import_idx}: expected field {field_idx} ({field_name:?}) has pointer kind {kind:?}; pointer fields are not supported in imported regions in v1 (proposal 0003 §Producer obligations 5)")]
+    PointerInImportNotSupportedInV1 {
+        import_idx: u32,
+        field_idx: u32,
+        field_name: String,
+        kind: FieldKind,
+    },
+
+    /// A `typedwasm.regions` field entry has a `target_region` value
+    /// with the import-table bit set, but the resolved index points past
+    /// the end of the `typedwasm.region-imports` table.
+    #[error("Level 13 violation: typedwasm.regions region {region_idx} field {field_idx}: target_region value {target_region:#010x} resolves to import-table index {resolved_idx} but only {import_count} imports are declared")]
+    ImportTargetOutOfRange {
+        region_idx: u32,
+        field_idx: u32,
+        target_region: u32,
+        resolved_idx: u32,
+        import_count: u32,
+    },
+}
+
 // ----------------------------------------------------------------------
 // Public entry points (stubbed in C1; implementations land in C2-C4).
 // ----------------------------------------------------------------------
@@ -260,6 +331,36 @@ pub fn verify_access_sites_from_module(
     verify::verify_access_sites_from_module(wasm_bytes)
 }
 
+/// Verify the L13 region-imports section's in-module self-consistency by
+/// reading its embedded `typedwasm.region-imports` and `typedwasm.regions`
+/// custom sections. Modules emitting neither section verify trivially.
+///
+/// Checks:
+///
+/// 1. `MissingDependentRegions`: region-imports present without regions
+///    is a hard error (proposal 0003 §"Producer obligations" #1).
+/// 2. `MissingDependentRegionImports`: regions present with at least one
+///    `target_region` value `>= IMPORT_TABLE_BASE` (i.e. claiming an
+///    import) without region-imports is a hard error (emitted at most
+///    once per module).
+/// 3. `DuplicateImport`: imports MUST have unique
+///    `(producer_module_name, region_name)` pairs.
+/// 4. `PointerInImportNotSupportedInV1`: imported regions' expected
+///    fields MUST all be `kind == Scalar` in v1.
+/// 5. `ImportTargetOutOfRange`: every `target_region` value with the
+///    import-table bit set MUST resolve within the import-table bounds.
+///
+/// Does NOT verify cross-module schema agreement (`SchemaSub expected
+/// actual` from `MultiModule.idr`); that requires the producer module's
+/// bytes and is the subject of a future `verify_link_graph(modules)` pass
+/// (proposal 0003 §"Open questions" #4 default option a).
+#[cfg(feature = "unstable-l13-imports")]
+pub fn verify_region_imports_from_module(
+    wasm_bytes: &[u8],
+) -> Result<Vec<RegionImportsError>, VerifyError> {
+    verify::verify_region_imports_from_module(wasm_bytes)
+}
+
 /// Ownership-annotated signature for one exported function.
 /// Mirrors OCaml `Tw_interface.func_interface`.
 #[derive(Debug, Clone, PartialEq, Eq)]