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

[hyperpolymath]

Summary

Closes #95's 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

• AsciiDoc renders cleanly (cols-tables, code-blocks, cross-refs).
• Cross-references resolve (MultiModule.idr line numbers; sibling proposal links; tracker issue links).
• Rebased onto main after PR docs(proposals): add 0004 [draft] — typedwasm.capability-grants (L15-C) #111 merge (no conflicts).
• 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

• tracking: proposal 0003 — typedwasm.region-imports (cross-module region foreign keys) #95 (tracker — this PR closes the [draft] acceptance bullet)
• Multi-producer ABI proposal: region/type-schema + capability carrier section (unblocks L2-6 / L15 on emitted wasm) #34 (proposal 0001 umbrella)
• meta: roadmap from [review] to [accepted] for proposals 0001 + 0002 #106 (acceptance roadmap tracker for 0001/0002)
• PR docs(proposals): 0001 multi-producer carrier sections for L2–L6 and L15 (Refs #34) #76 (proposal 0001 — source of the deferral)
• PR feat(verify): mirror L13 module-isolation from the OCaml verifier (Refs #35) #37 (L13 single-module isolation — positive companion is 0003's cross-module)
• PR docs(proposals): add 0004 [draft] — typedwasm.capability-grants (L15-C) #111 (proposal 0004 draft — sibling cross-module question for capabilities)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 96 issues detected

Severity	Count
🔴 Critical	8
🟠 High	19
🟡 Medium	69

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in c5-regenerate.yml",
    "type": "unknown",
    "file": "c5-regenerate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "unknown",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence