Skip to content

Commit 2f36f51

Browse files
docs(proposals): producer-readiness checklist + canonical emit order (closes #97) (#114)
## Summary Closes [#97](#97) — addresses both halves of the paired-review meander finding. ## (A) Producer-readiness checklist — Appendix B in proposal 0001 (~120 LOC) Tabulates each carrier section's IR prerequisites, current producer-side status, and roadmap-issue identifier in each producer's tracker where the gap is named: | Carrier | IR prerequisites | Status | |---------|-----------------|--------| | `typedwasm.ownership` | per-fn ownership-kind tracking | **SHIPPING** | | `typedwasm.regions` | region decls + field offsets + stable indices | **NOT YET EMITTABLE** (AS Roadmap C1 deferred; Ephapax dead code) | | `typedwasm.capabilities` | per-fn cap decl + module budget + effect IR | **NOT YET EMITTABLE** (AS Roadmap C2 not started; Ephapax Perform/Handle stubbed) | | `typedwasm.region-imports` (0003) | + cross-module region tracking + wasm-module-name resolution | **NOT YET EMITTABLE** | | `typedwasm.access-sites` (0002) | + per-instr tracking + post-rewrite hook | **NOT YET EMITTABLE** (depends on regions) | | `typedwasm.capability-grants` (0004) | + per-callsite grant tracking | **NOT YET EMITTABLE** (depends on capabilities) | NOTE block surfaces the all-or-nothing implication: **do not emit a section you cannot populate.** Proposal 0002 gains a §"Producer-readiness (cross-reference)" subsection (~28 LOC) pointing to 0001's Appendix B plus three access-sites-specific items: per-instruction tracking, post-rewrite hook discipline, region-index stability across sections. ## (B) Canonical emit ordering — extends 0001 §"Producer obligations" New 5th item specifying the recommended emit order matching the runtime dependency graph: ``` 1. typedwasm.ownership 2. typedwasm.regions 3. typedwasm.region-imports (proposal 0003) 4. typedwasm.capabilities 5. typedwasm.access-sites (proposal 0002) 6. typedwasm.capability-grants (proposal 0004) ``` **Consumers MUST NOT depend on this order** — the verifier reads sections by custom-section name, so any order is parseable. The canonical order exists for cross-producer module comparability (byte-equal carrier sequences for two producers of the same logical module — useful for `cmp` / `diff` / content-addressing). ## Acceptance update for #97 - [x] Proposal 0001 gains §"Producer-readiness checklist" appendix listing the IR prerequisites for each section. - [x] Proposal 0002 gains a one-line cross-reference (expanded to a full subsection with access-sites-specific items) to 0001's checklist. - [x] Proposal 0001 §"Producer obligations" specifies the canonical emit order with a "consumer MAY accept any order" note. - [ ] When AffineScript / Ephapax start their respective Roadmap C1/C2/C3 implementations, those issues cross-reference this checklist. *(Producer-side action, not a typed-wasm gate.)* ## What this closes Together with #94, #95, #96 (resolved in PRs #110/#111/#112/#113), this completes all the documentation-side gates around proposals 0001 and 0002. Both proposals are now fully ready for `[review] → [accepted]` owner decision. ## Test plan - [x] AsciiDoc renders cleanly (cols-tables, lower-alpha sub-list, code-block fences). - [x] Cross-reference link to Appendix B from proposal 0002 uses AsciiDoc anchor format. - [x] No code changes — no Cargo/Idris2 build required. ## Related - #97 (this PR closes it) - #34 (proposal 0001 umbrella) - #106 (acceptance roadmap tracker) - ephapax#165 §3+§6 / affinescript#402 §4+§7 — paired reviews surfacing the gap - affinescript#462 (access-sites codegen issue — referenced from Appendix B) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 81a5af8 commit 2f36f51

2 files changed

Lines changed: 148 additions & 0 deletions

File tree

docs/proposals/0001-multi-producer-carrier-section.adoc

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,6 +247,26 @@ A conforming producer that emits either new section MUST:
247247
unlisted fields" and L2 will flag any access to an unlisted field.
248248
. For L15: emit only capabilities actually declared by the source
249249
module; do not synthesise.
250+
. **Canonical emit order** (recommended, not enforced):
251+
+
252+
[loweralpha]
253+
.. `typedwasm.ownership`
254+
.. `typedwasm.regions`
255+
.. `typedwasm.region-imports` (proposal 0003)
256+
.. `typedwasm.capabilities`
257+
.. `typedwasm.access-sites` (proposal 0002)
258+
.. `typedwasm.capability-grants` (proposal 0004)
259+
+
260+
Rationale: matches the runtime dependency graph — `access-sites`
261+
foreign-keys into `regions`, `capability-grants` foreign-keys into
262+
`capabilities`, and `region-imports` companions `regions`.
263+
**Consumers MUST NOT depend on this order**: the verifier reads
264+
sections by custom-section name, so a non-conforming producer that
265+
emits in any other order is still parseable. The canonical order
266+
exists solely so that two producers' emission of the same logical
267+
module produces byte-equal carrier-section sequences (useful for
268+
cross-producer module comparison via `cmp` or `diff`, and for
269+
deterministic content-addressing of typed-wasm modules).
250270

251271
=== Consumer obligations (verifier)
252272

@@ -670,3 +690,103 @@ required for `[accepted]` — is to encode the same mapping as Idris2
670690
property tests (`src/abi/` would gain a `WireSchemaEquiv.idr` showing
671691
`encode/decode` round-trips preserve the spec witnesses listed in A.1
672692
+ A.2). That work is filed as a follow-up after acceptance.
693+
694+
== Appendix B — Producer-readiness checklist (closes #97)
695+
696+
Surfaced in the paired producer reviews of proposals 0001 + 0002
697+
(ephapax#165 §3 + §6 + affinescript#402 §4 + §7, both 2026-05-30):
698+
the §"Producer obligations" section enumerates what a conforming
699+
producer must *do at emission time*, but understates **what a producer
700+
must already have in its IR** to be capable of emitting populated
701+
sections at all.
702+
703+
This appendix tabulates the IR prerequisites for each carrier
704+
section, the producer-side status at v1, and the roadmap-issue
705+
identifier in each producer's tracker where the gap is named.
706+
707+
NOTE: A producer that emits a carrier section without satisfying its
708+
IR prerequisites will emit an empty or synthetic section that the
709+
verifier will treat as "no claim made about anything," falsifying
710+
the intent of the carrier. **The all-or-nothing rule from §"Producer
711+
obligations" ¶3 implies: do not emit a section you cannot populate.**
712+
713+
=== B.1 Per-carrier IR prerequisites
714+
715+
[cols="2,3,2,3", options="header"]
716+
|===
717+
| Carrier
718+
| IR prerequisites in the producer
719+
| Status (v1)
720+
| Roadmap reference
721+
722+
| `typedwasm.ownership`
723+
| Per-function-parameter + per-return ownership-kind tracking
724+
(`Unrestricted` / `Linear` / `SharedBorrow` / `ExclBorrow`)
725+
| **SHIPPING** in both producers
726+
| AffineScript `lib/borrow.ml`; Ephapax `src/ephapax-types/`
727+
728+
| `typedwasm.regions`
729+
| Per-region declaration in source language (field names + wasm
730+
types + nullability + cardinality); stable per-module region
731+
index assignment; field offset computation from schema
732+
| **NOT YET EMITTABLE**
733+
| AffineScript Roadmap C1 (region inference) DEFERRED at
734+
`lib/borrow.ml:1724-1730`; Ephapax `Codegen.region_stack` DEAD
735+
CODE at `src/ephapax-wasm/src/lib.rs:271`
736+
737+
| `typedwasm.capabilities`
738+
| Per-function capability declaration; module-level capability
739+
budget; effect-tracking IR for capability-affecting operations
740+
| **NOT YET EMITTABLE**
741+
| AffineScript Roadmap C2 (capability tracking) NOT STARTED;
742+
Ephapax `ExprKind::Perform` / `Handle` codegen stubs to
743+
`Instruction::Unreachable` (`src/ephapax-wasm/src/lib.rs`)
744+
745+
| `typedwasm.region-imports` (proposal 0003)
746+
| All `typedwasm.regions` prerequisites **plus** cross-module
747+
region declaration tracking; wasm-module-name resolution; the
748+
high-bit `target_region` convention from proposal 0003
749+
| **NOT YET EMITTABLE**
750+
| AffineScript `lib/tw_interface.ml` has L10/L13 boundary
751+
scaffolding but Roadmap C3 (multi-module region emission) is
752+
the prerequisite; Ephapax cross-module emission not on roadmap
753+
754+
| `typedwasm.access-sites` (proposal 0002)
755+
| All `typedwasm.regions` prerequisites **plus** per-instruction
756+
tracking of typed accesses through codegen; post-rewrite byte
757+
offset recording (must run AFTER `wasm-opt` etc.); stable
758+
`(region_id, field_id)` matching the regions section
759+
| **NOT YET EMITTABLE**
760+
| Depends on regions carrier landing first;
761+
affinescript#462 / ephapax issue pending
762+
763+
| `typedwasm.capability-grants` (proposal 0004)
764+
| All `typedwasm.capabilities` prerequisites **plus**
765+
per-call-site grant tracking IR; post-rewrite call-instruction
766+
byte offset recording; stable capability-index matching
767+
| **NOT YET EMITTABLE**
768+
| Depends on capabilities carrier landing first
769+
|===
770+
771+
=== B.2 Status legend
772+
773+
* **SHIPPING** — producer emits this carrier on every module today;
774+
consumers can rely on its presence.
775+
* **NOT YET EMITTABLE** — producer-side IR cannot populate this
776+
carrier; emitting an empty section would falsify the all-or-nothing
777+
contract.
778+
779+
=== B.3 Use this checklist
780+
781+
When any producer's tracker (AffineScript Roadmap C1/C2/C3 issues,
782+
Ephapax codegen issues, future third-party producer tickets) opens
783+
a work item for emitting a new carrier, that issue SHOULD
784+
cross-reference this appendix and the corresponding §B.1 row. This
785+
makes the multi-quarter IR work explicit rather than discovering it
786+
ad-hoc during downstream codegen sessions.
787+
788+
The verifier-side adoption (codecs + verify passes in
789+
`crates/typed-wasm-verify/`) is INDEPENDENT of producer-side
790+
readiness — the verifier can ship parsing + validation for a carrier
791+
that no producer yet emits (the verifier just sees an absent section
792+
and returns `Ok(())`). This appendix only tracks the producer side.

docs/proposals/0002-access-site-carrier.adoc

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -209,6 +209,34 @@ A conforming producer that emits `typedwasm.access-sites` MUST:
209209
system). The verifier interprets an entry as a claim that the
210210
access IS typed.
211211

212+
=== Producer-readiness (cross-reference)
213+
214+
See link:0001-multi-producer-carrier-section.adoc#_appendix_b_producer_readiness_checklist_closes_97[proposal 0001 §"Appendix B — Producer-readiness checklist"]
215+
for the IR prerequisites of all carrier sections. Access-sites
216+
specifically requires (in addition to that appendix's
217+
`typedwasm.regions` row):
218+
219+
* **Per-instruction tracking of typed accesses** through the
220+
codegen pipeline. A typed `region.get $r .f` (or equivalent)
221+
produces a wasm opcode somewhere in the function body; the
222+
producer must record at which **post-rewrite** byte offset the
223+
opcode lands.
224+
* **Post-rewrite hook**. The access-site list must be finalised
225+
AFTER every wasm-rewrite pass the producer runs (`wasm-opt`,
226+
`snip`, `wasm-gc`, custom passes). Producers using `wasm-encoder`
227+
directly can record byte offsets during emission; producers
228+
using an IR-to-wasm lowering pass need to capture offsets at the
229+
lowering boundary and re-validate post-rewrite.
230+
* **Region-index stability across sections**. The `(region_id,
231+
field_id)` foreign keys in `typedwasm.access-sites` MUST match
232+
the indices the producer emits in `typedwasm.regions` for the
233+
same module (proposal 0001 §"Producer obligations" ¶2).
234+
235+
Status (v1): **NOT YET EMITTABLE** in either AffineScript or
236+
Ephapax — both depend on the `typedwasm.regions` IR prerequisites
237+
landing first. Tracked at affinescript#462 and the ephapax
238+
companion issue (per #106).
239+
212240
=== Consumer obligations (verifier)
213241

214242
`crates/typed-wasm-verify/` will gain (gated behind

0 commit comments

Comments
 (0)