docs(proposals): add 0003 [draft] — typedwasm.region-imports (L13 cross-module) (#112)

## Summary

Closes [#95](#95
third acceptance bullet ("if [draft] proposal 0003 is authored, it
tracks back here"). Closes the **latent seam** flagged in proposal 0001
§"Open questions" #5 (cross-module region foreign keys) and the
symmetric gap noted in proposal 0002 §"Open questions" #3.

## What 0003 specifies

A third producer-neutral carrier (slotting between 0001's
regions/capabilities and 0002's access-sites):

- **`typedwasm.region-imports`** carries per-module table of imported
regions: source module name, region name, expected schema (for
cross-module schema-agreement verification).
- **Companion non-breaking extension to `typedwasm.regions`**:
`target_region` foreign keys gain a high-bit convention for import-table
indices:
  - `0x00000000..0x7FFFFFFE` — local region index
- `0x80000000..0xFFFFFFFE` — imported region (index = value -
`0x80000000`)
  - `0xFFFFFFFF` — `Scalar` sentinel (unchanged)

v1 typedwasm.regions consumers see "region_id out of range" on high-bit
values and recover via lenient codec; v1.1 consumers interpret the high
bit as import-table indicator. **No wire breaking change.**

## Wire format

Mirrors 0001/0002/0004 conventions (LEB128 per field, UTF-8 strings,
lenient on truncation):

```
u16le         version                (= 1)
u32le_leb128  import_count
for each import:
    u32le_leb128  producer_module_name_len
    u8[]          producer_module_name      (wasm module name)
    u32le_leb128  region_name_len
    u8[]          region_name               (exported region name)
    u32le_leb128  expected_field_count
    for each expected field:
        u32le_leb128  field_name_len
        u8[]          field_name
        u8            kind                  (FieldKind: Scalar only in v1)
        u8            wasm_ty               (same enum as regions)
        u8            nullability
        u32le_leb128  cardinality
```

## Section structure

| Section | Coverage |
|---------|----------|
| Context | L13 cross-module gap in 0001, `MultiModule.idr` spec already
covers it, latent-seam framing |
| Proposal | high-bit `target_region` extension; wire format; spec-type
mapping; versioning; producer/consumer obligations; coordination |
| Producer obligations | 6 items (companion regions section mandatory,
high-bit convention, wasm-module-name matching, omit-if-empty,
no-pointer-fields-in-v1, only-real-imports) |
| Consumer obligations | `verify_region_imports_from_module` pass + 7
error variants (`MissingDependentRegions`, `DuplicateImport`,
`UnresolvedProducerModule`, `UnresolvedExportedRegion`,
`SchemaImportMismatch`, `ImportTargetOutOfRange`,
`PointerInImportNotSupportedInV1`) |
| Alternatives considered | B extend-regions (rejected — conflates
concerns); C component-model (deferred); D wasm-imports (rejected —
confuses linkers); E string-table (deferred to v2) |
| Open questions | (1) pointer-typed expected fields (deferred); (2)
cross-module access sites — recommend folding 0002 §OQ3 in; (3)
cross-module capability grants (0004 §OQ4 — may differ); (4) link-time
vs verify-time (default: separate `verify_link_graph` pass); (5)
producer module name normalisation (NFC deferred); (6) empty import
table semantics |
| Acceptance criteria | 6 gates mirroring 0001/0002/0004 |

## Spec-side mapping

Realises `MultiModule.idr`'s:

| Idris2 type | Wire realisation |
|------------|------------------|
| `ImportedRegion.source` (line 54) | `producer_module_name` |
| `ImportedRegion.regionName` (line 56) | `region_name` |
| `ImportedRegion.expectedSchema` (line 57) | per-field table |
| `SchemaSub` (line 249) | verifier reconstructs from wire + producer's
regions |
| `ModuleCompat from to imp exp` (line 318) | verifier output (one per
resolved import) |
| `noSpoofing` (line 374, flagship) | the L13 property the verifier
realises on emitted bytes |
| `CompatCertificate` (line 142) | verifier-emitted per resolved import
|
| `SchemaMismatch` (line 185) | `SchemaImportMismatch` error variant |

## Why `[draft]` not `[review]`

Neither producer can emit `typedwasm.region-imports` today:

- **AffineScript** — `lib/tw_interface.ml` has cross-module verification
scaffolding for L10/L13 boundary (reads `typedwasm.ownership`
cross-module), but Roadmap C3 (multi-module region emission) is the
prerequisite.
- **Ephapax** — cross-module region emission isn't on the roadmap yet;
`src/ephapax-wasm/` is single-module.

## README update

Adds 0003 entry to `docs/proposals/README.adoc`'s "Current proposals"
table; removes the "Proposal 0003 ... reserved" note (now occupied).

## Test plan

- [x] AsciiDoc renders cleanly (cols-tables, code-blocks, cross-refs).
- [x] Cross-references resolve (`MultiModule.idr` line numbers; sibling
proposal links; tracker issue links).
- [x] Rebased onto `main` after PR #111 merge (no conflicts).
- [x] No code changes — no Cargo build required.
- [ ] Reviewer cross-check: confirm the high-bit `target_region`
convention doesn't break any v1 consumer (existing tests).

## Related

- #95 (tracker — this PR closes the [draft] acceptance bullet)
- #34 (proposal 0001 umbrella)
- #106 (acceptance roadmap tracker for 0001/0002)
- PR #76 (proposal 0001 — source of the deferral)
- PR #37 (L13 single-module isolation — positive companion is 0003's
cross-module)
- PR #111 (proposal 0004 draft — sibling cross-module question for
capabilities)

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

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

Author: hyperpolymath