docs(proposals/0001): Criterion 2 appendix — wire↔Idris2-spec mapping

[hyperpolymath]

Summary

Closes proposal 0001 §"Acceptance criteria" Criterion 2 — the last write-up gate before [review] → [accepted]. Adds a 247-line "Appendix A — Wire-vs-Idris2-spec mapping" to docs/proposals/0001-multi-producer-carrier-section.adoc.

Appendix structure

Section	Coverage
A.1	typedwasm.regions wire fields ↔ Region.idr + Pointer.idr — per-field table (version, region_count, name, field_count, field_name, kind, wasm_ty, target_region, nullability, cardinality, region_byte_size)
A.2	typedwasm.capabilities wire fields ↔ ResourceCapabilities.idr — capability table + per-function required list; documents that strict-increasing required[] encodes DistinctCaps + ContainedIn + canonical-order at once
A.3	What is NOT carried on the wire (deliberate): ContainedIn proof witnesses (verifier reconstructs), CallCompatible (L15-C deferred to #96), LayoutValid (verifier recomputes), SchemaEq (single-module v1), RegionDisjoint (runtime concern), ExclusiveWitness (in ownership section)
A.4	Soundness shape — single NOTE listing per-emission proof obligations PR #107 (codec) + PR #109 (verifier) already enforce

Criterion 2 line in §"Acceptance criteria" updated to "(Satisfied — see Appendix A below.)".

Why a write-up not a property test

Criterion 2's text reads "every wire field maps cleanly to a spec witness" — a write-up satisfies it (and is what a reviewer reads). A future task (filed in the appendix's closing paragraph, not blocking [accepted]) is to encode the same mapping as Idris2 property tests in src/abi/ (WireSchemaEquiv.idr showing encode/decode round-trips preserve the spec witnesses).

Acceptance-roadmap state after this PR

	0001 (regions+capabilities)	0002 (access-sites)
Codec	✅ #107	✅ #107
Verifier	✅ #109	✅ #109
Spec doc	✅ #108	✅ #108
Wire-vs-spec review	✅ this PR	n/a
Cross-repo issues	✅ affinescript#444 + ephapax#221	✅ affinescript#462 / ephapax pending
Open Qs	⚠️ #94, #95, #96 still open	n/a

After this lands, proposal 0001's only remaining gate is the open questions converging (WBool wire-width pin, region-imports proposal placeholder, capability-grants v1.4.x). The acceptance criteria themselves are all green.

Test plan

• Local proof-doc render check: appendix renders with cleanly-formatted cols=2,3,2 + cols=2,3 tables.
• Cross-reference links resolve (Region.idr:253, Region.idr:127, Pointer.idr:74, ResourceCapabilities.idr:67/104/218/241/248/312, etc.).
• No code changes — no Cargo build required.
• Reviewer cross-check: confirm A.3 is exhaustive (no missed spec-side relation that v1 silently drops).

Related

• 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)
• PR docs(proposals): promote 0001 + 0002 status [draft] → [review] #104 ([draft] → [review])
• PR feat(verify): L15 capabilities + L2 access-sites codecs (proposals 0001 §3 + 0002 §3) #107 (codec) / PR docs(spec): document wire-level carrier sections (proposals 0001 §4 + 0002 §5) #108 (spec doc) / PR feat(verify): verify_capabilities + verify_access_sites passes (proposal 0002 §Gate 4) #109 (verifier)
• spec: pin WBool wire width in proposal 0001 (canonical 4-byte or lenient mixed-width validation) #94 / tracking: proposal 0003 — typedwasm.region-imports (cross-module region foreign keys) #95 / tracking: typedwasm.capability-grants (L15-C per-call-site, v1.4.x follow-up) #96 (acceptance preconditions filed)

🤖 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