hyperpolymath · hyperpolymath · May 30, 2026 · May 30, 2026
@@ -163,9 +163,11 @@ pins affinescript SHA for drift detection).
 3. **L15-C (call-graph monotonicity)** — proposal 0004 `[draft]`
    (`docs/proposals/0004`). Gated on producer-side L15-A emission
    (Roadmap C2 not started in either producer).
-4. **ADR promotion** — proposals 0001 + 0002 remain in
-   `docs/proposals/` post-acceptance; promotion to
-   `docs/decisions/` is a follow-up file-restructure.
+4. **ADR promotion** — DONE (2026-05-30): proposals 0001 + 0002
+   promoted to `docs/decisions/0002-multi-producer-carrier-sections.adoc`
+   (ADR-0002) and `docs/decisions/0003-access-site-carrier.adoc`
+   (ADR-0003). Proposal files retained as canonical wire-format
+   references.
 
 **Spec-of-record alignment (2026-05-27, PR #79).**  The
 `TypedWasm.ABI.VerifierSpec` Idris2 module now states the

@@ -0,0 +1,147 @@
+= Architecture Decision Record: 0002-multi-producer-carrier-sections
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# 2. Adopt Multi-Producer Carrier Sections for L2–L6 and L15
+
+Date: 2026-05-30
+
+## Status
+
+Accepted
+
+Promoted from link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
+0001] (`[accepted]` 2026-05-30). The proposal file remains canonical for
+wire-format detail, error variants, and producer obligations; this ADR
+records the decision and its consequences.
+
+## Context
+
+Before this decision, the post-codegen verifier
+(`crates/typed-wasm-verify/`) could enforce **L7 (aliasing)**,
+**L10 (linearity)**, and **L13 (module isolation, negative form)** on
+emitted wasm via the single `typedwasm.ownership` carrier section, but
+**L2 (region-binding)**, **L3 (type-compatible access)**, **L4 (null
+safety)**, **L5 (bounds-proof)**, **L6 (result-type)**, and
+**L15 (resource capabilities)** had no wire surface at all. The
+source-level Idris2 spec (`Region.idr`, `Pointer.idr`,
+`MultiModule.idr`, `ResourceCapabilities.idr`) modelled all the
+required structure, but the moment a producer emitted `.wasm` bytes
+the schema and capability data was gone — the source-level checker was
+the only line of defence.
+
+Two producers — AffineScript and Ephapax — share `typedwasm` as their
+emission target. Without a wire-level agreement, cross-language module
+linking (the project's load-bearing differentiator: ADR-0001 RSR
+template plus typed shared memory) had no enforcement story on
+post-link binaries.
+
+This was an **ABI** problem, not an enforcement problem: the
+algorithms existed; the carriers did not.
+
+## Decision
+
+Adopt two new wasm custom sections as the v1 carriers for L2–L6 and
+L15 schema/capability data, plus reserve two additional carriers for
+the access-site and cross-module follow-ups:
+
+[cols="1,2,3"]
+|===
+| Section name | Carries | Status
+
+| `typedwasm.regions`
+| Region schemas (fields × types × nullability × cardinality)
+| Adopted v1 (this ADR); realised in `crates/typed-wasm-verify` PR #107
+
+| `typedwasm.capabilities`
+| Capability sets per function signature
+| Adopted v1 (this ADR); realised in `crates/typed-wasm-verify` PR #109
+
+| `typedwasm.access-sites`
+| Per-instruction `(region_id, field_id)` for typed load/store
+| Promoted in link:0003-access-site-carrier.adoc[ADR-0003]
+(realises Open Question §5 of proposal 0001)
+
+| `typedwasm.region-imports`
+| Cross-module schema agreement (foreign-key regions)
+| `[draft]` at link:../proposals/0003-region-imports-carrier.adoc[Proposal
+0003]; tracks issue
+https://github.com/hyperpolymath/typed-wasm/issues/95[#95]
+|===
+
+Wire-format detail (encoding, LEB128 boundaries, error variants,
+acceptance criteria) lives in proposal 0001 §"Wire format" and §"Error
+variants". Producer obligations and canonical emit order live in
+proposal 0001 Appendix B ("Producer-readiness checklist") and
+§"Producer obligations".
+
+Key adopted pins:
+
+* **WBool wire width** is **4 bytes** (`i32.store` / `i32.load`)
+  matching both shipping producers; the Idris2 `sizeOf WBool` is
+  aligned to 4 in PR #113. A 1-byte `WBoolPacked` is reserved as a
+  separate `WasmType` constructor, not a width flag on `WBool`.
+* **LEB128 per field** (encoding option B) for all variable-width
+  integer fields in the new carriers — uniform with existing wasm
+  conventions.
+* **Cardinality-1 producer surface in v1**: both shipping producers
+  emit exactly one of each carrier per module; multi-section behaviour
+  is reserved for a future amendment.
+* Carriers are **opt-in via Cargo features** (`unstable-l2`,
+  `unstable-l15`) until Phase 3.
+
+## Consequences
+
+### Positive
+
+- Verifier can re-check L2–L6 and L15 on emitted bytes; the
+  source-level checker is no longer the only line of defence.
+- Producers in different source languages (AffineScript, Ephapax,
+  future) can interoperate through typed shared memory with a single
+  wire contract.
+- The carrier-based design generalises: ADR-0003 (access-sites) and
+  proposal 0003 (region-imports) and proposal 0004 (capability-grants)
+  all reuse the same custom-section pattern.
+- Idris2 spec and Rust verifier converge on a single source of truth
+  per carrier (mapping recorded in proposal 0001 Appendix A
+  "Wire-vs-Idris2-spec mapping").
+- Producer-readiness checklist (proposal 0001 Appendix B) gives both
+  shipping producers a concrete acceptance test before v1 stabilises.
+
+### Negative
+
+- Two carriers add ~400-line emitter surface per producer. Both
+  AffineScript codegen and Ephapax codegen now have a per-feature debt
+  to track (AffineScript Roadmap C1/C2/C3; Ephapax
+  `Codegen.region_stack` dead-code removal).
+- Until Phase 3 stabilisation (and feature-gating drop), verifier
+  consumers must opt in via `unstable-l2` / `unstable-l15`.
+- Adding two carriers in v1 means the wire-format error surface grows
+  by ~12 variants total (proposal 0001 §"Error variants"); each
+  variant needs a regression test before stabilisation.
+
+### Neutral
+
+- The existing `typedwasm.ownership` carrier (4-kind ownership per
+  function signature) is unchanged; this ADR is purely additive on
+  the wire.
+- L7, L10, L13 (negative form) enforcement is unaffected — the
+  ownership carrier still drives them.
+- ADRs 0001 (RSR template) and 0002 (this) are orthogonal: this
+  decision lives at the wasm-ABI layer; RSR lives at the
+  repo-structure layer.
+
+## Cross-references
+
+* link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
+  0001] — full wire-format spec (canonical reference)
+* link:0003-access-site-carrier.adoc[ADR-0003] — access-site carrier
+  (companion decision)
+* link:../proposals/0003-region-imports-carrier.adoc[Proposal 0003] —
+  region-imports carrier (cross-module, `[draft]`)
+* link:../proposals/0004-capability-grants-carrier.adoc[Proposal 0004]
+  — capability-grants carrier (L15-C, `[draft]`)
+* https://github.com/hyperpolymath/typed-wasm/issues/34[issue #34] —
+  tracking issue (closed when proposals 0001+0002 reached `[accepted]`)
+* https://github.com/hyperpolymath/typed-wasm/issues/50[issue #50] —
+  Phase 2 (multi-producer adoption)
@@ -0,0 +1,120 @@
+= Architecture Decision Record: 0003-access-site-carrier
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# 3. Adopt Access-Site Carrier (`typedwasm.access-sites`) for L2 Enforcement
+
+Date: 2026-05-30
+
+## Status
+
+Accepted
+
+Promoted from link:../proposals/0002-access-site-carrier.adoc[Proposal
+0002] (`[accepted]` 2026-05-30). The proposal file remains canonical
+for wire-format detail, error variants, and producer obligations; this
+ADR records the decision and its consequences.
+
+Builds on link:0002-multi-producer-carrier-sections.adoc[ADR-0002].
+
+## Context
+
+link:0002-multi-producer-carrier-sections.adoc[ADR-0002] adopts
+`typedwasm.regions` as the schema carrier: it tells the verifier *which
+regions exist* and *which fields each region declares with what type,
+nullability, and cardinality*. It does **not** tell the verifier
+**which `(region_id, field_id)` any individual `i32.load` /
+`i32.store` is supposed to be against**.
+
+The source-level checker has no problem: it sees `region.get $r .f`
+directly in the AST and resolves `$r → region`, `.f → field` at
+compile time. After codegen, that statement is some sequence ending in
+`i32.load offset=N align=A` — and the `($r, .f)` annotation is gone.
+The verifier can re-derive *which region's offset window N falls into*
+only if the producer tells it which base pointer (region instance)
+was loaded, and a single function may touch several regions.
+
+This was Open Question §5 in proposal 0001, resolved on 2026-05-27 in
+favour of option A (per-instruction access-site carrier). The L2
+verifier pass `verify_region_binding` was deliberately omitted from PR
+#77 because the carrier did not yet exist; this ADR formalises the
+decision.
+
+Without this carrier, **L2-the-enforcement** (every typed access
+resolves to a declared region/field) could not fire on emitted bytes
+— even though **L2-the-spec** (regions/fields exist; cross-module
+schema agreement) was fully covered by `typedwasm.regions`.
+
+## Decision
+
+Adopt a third wasm custom section, `typedwasm.access-sites`, that
+carries, per typed load/store instruction, the resolved
+`(region_id, field_id)` pair the producer intended.
+
+Realised in PR #109 (`verify_access_sites_from_module`).
+
+Key adopted pins:
+
+* Wire format: per-entry `(function_index, instruction_byte_offset,
+  region_id, field_id)`, all LEB128 (encoding option B uniform with
+  ADR-0002).
+* Entries are **strictly ordered** by `(function_index,
+  instruction_byte_offset)` so the verifier can binary-search.
+* Each typed load/store **must** have exactly one access-site entry;
+  missing entries are an error (`UnboundAccess`), not a silent skip.
+* Cardinality-1 producer surface in v1; same opt-in feature gate as
+  ADR-0002 (`unstable-l2`).
+
+Error variants and acceptance criteria live in proposal 0002 §"Error
+variants" and §"Acceptance criteria".
+
+## Consequences
+
+### Positive
+
+- L2 enforcement (`verify_region_binding`) fires on emitted bytes.
+- Carrier is **independent** of `typedwasm.regions`: a producer that
+  emits regions but not access-sites still gets L3–L6 spec-level
+  checking; access-sites is what unlocks per-instruction L2.
+- Per-instruction granularity means the carrier composes with the
+  L15-C per-call-site grants design in proposal 0004 (both key off
+  `(function_index, instruction_byte_offset)`).
+- The decision unblocks AffineScript Roadmap C2 (access-site
+  emission) and the Ephapax counterpart (owner action — classifier
+  blocked the cross-repo issue; tracked in `#106` comment).
+
+### Negative
+
+- Producer codegen must thread `(region, field)` annotations through
+  to every typed load/store call-site and serialise them in
+  carrier-emit order. Both shipping producers have outstanding
+  codegen work for this.
+- Wire-format size: every typed memory access adds ~6–12 bytes of
+  carrier data (function_index + offset + region_id + field_id, all
+  LEB128). Acceptable for v1; benchmarked in proposal 0002 §"Wire
+  format" estimate.
+- Cardinality-1 means a producer cannot split access-sites across
+  multiple sections for incremental emission; reserved for a future
+  amendment.
+
+### Neutral
+
+- `typedwasm.access-sites` is **opt-in via `unstable-l2`** until
+  Phase 3, matching ADR-0002.
+- The access-site carrier is conceptually simpler than the regions
+  carrier — no schema, just a sorted lookup table — but it shares
+  the same feature-gate and the same producer-readiness checklist
+  entry as proposal 0001 Appendix B.
+
+## Cross-references
+
+* link:../proposals/0002-access-site-carrier.adoc[Proposal 0002] —
+  full wire-format spec (canonical reference)
+* link:0002-multi-producer-carrier-sections.adoc[ADR-0002] — the
+  schema-carrier decision this ADR builds on
+* link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
+  0001] — origin of Open Question §5 (resolved into this ADR)
+* https://github.com/hyperpolymath/typed-wasm/issues/78[issue #78] —
+  tracking issue
+* https://github.com/hyperpolymath/typed-wasm/pull/109[PR #109] —
+  realising pass `verify_access_sites_from_module`
@@ -1 +1,47 @@
-= decisions Unit
+// SPDX-License-Identifier: MPL-2.0
+= Architecture Decision Records (ADRs)
+
+Accepted decisions that shape typed-wasm's architecture. Proposals
+that have hardened past the design-doc stage live here; forward-looking
+proposals still under discussion live in link:../proposals/[`docs/proposals/`].
+
+== Index
+
+[cols="1,4,1,1"]
+|===
+| Number | Title | Date | Status
+
+| link:0001-adopt-rsr-standard.adoc[0001]
+| Adopt Rhodium Standard Repository (RSR) template
+| 2026-02-14
+| Accepted
+
+| link:0002-multi-producer-carrier-sections.adoc[0002]
+| Adopt multi-producer carrier sections for L2–L6 and L15
+| 2026-05-30
+| Accepted
+
+| link:0003-access-site-carrier.adoc[0003]
+| Adopt access-site carrier (`typedwasm.access-sites`) for L2 enforcement
+| 2026-05-30
+| Accepted
+|===
+
+== Authoring an ADR
+
+. Use link:0000-template.adoc[`0000-template.adoc`] as the starting
+  template.
+. Filename: `NNNN-short-slug.adoc` (numbering continues from the highest
+  current ADR; pad to 4 digits).
+. If the ADR promotes a proposal, link back to the proposal file and
+  keep the proposal as the canonical wire-format / detail reference.
+. Add a row to the index above.
+
+== Related
+
+* link:../proposals/[`docs/proposals/`] — forward-looking proposals
+  (pre-ADR design docs)
+* link:../architecture/[`docs/architecture/`] — current architecture
+  documentation
+* link:../PRODUCTION-PATH.adoc[`docs/PRODUCTION-PATH.adoc`] —
+  strategic plan; D1–D6 decisions land directly as ADRs here
@@ -12,10 +12,17 @@
 | Date         | 2026-05-27
 | Last-updated | 2026-05-30 (review → accepted; owner-decision after all gates ✅)
 | Accepted-by  | hyperpolymath (owner), 2026-05-30
+| Promoted to  | link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002] (2026-05-30)
 | Tracks issue | https://github.com/hyperpolymath/typed-wasm/issues/34[#34]
 | Phase        | Phase 2 (https://github.com/hyperpolymath/typed-wasm/issues/50[#50]) — multi-producer adoption
 |===
 
+NOTE: This proposal was promoted to
+link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002]
+on 2026-05-30. The proposal file is retained as the canonical
+reference for wire-format detail, error variants, and producer
+obligations; the ADR records the decision and consequences.
+
 == Context
 
 The post-codegen verifier (`crates/typed-wasm-verify/`) enforces **L7

@@ -12,11 +12,18 @@
 | Date         | 2026-05-28
 | Last-updated | 2026-05-30 (review → accepted; owner-decision after all 6 gates ✅)
 | Accepted-by  | hyperpolymath (owner), 2026-05-30
+| Promoted to  | link:../decisions/0003-access-site-carrier.adoc[ADR-0003] (2026-05-30)
 | Tracks issue | https://github.com/hyperpolymath/typed-wasm/issues/78[#78]
 | Phase        | Phase 2 (https://github.com/hyperpolymath/typed-wasm/issues/50[#50]) — multi-producer adoption
 | Builds on    | link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (multi-producer carrier sections)
 |===
 
+NOTE: This proposal was promoted to
+link:../decisions/0003-access-site-carrier.adoc[ADR-0003] on
+2026-05-30. The proposal file is retained as the canonical reference
+for wire-format detail, error variants, and producer obligations; the
+ADR records the decision and consequences.
+
 == Context
 
 link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (PR

@@ -22,11 +22,11 @@ Status legend:
 
 | link:0001-multi-producer-carrier-section.adoc[0001]
 | Multi-producer carrier sections for L2–L6 and L15
-| `[accepted]` (2026-05-30)
+| `[accepted]` (2026-05-30) → promoted to link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002]
 
 | link:0002-access-site-carrier.adoc[0002]
 | Access-site carrier section (`typedwasm.access-sites`) for L2 enforcement
-| `[accepted]` (2026-05-30)
+| `[accepted]` (2026-05-30) → promoted to link:../decisions/0003-access-site-carrier.adoc[ADR-0003]
 
 | link:0003-region-imports-carrier.adoc[0003]
 | Region imports carrier section (`typedwasm.region-imports`) for L13 cross-module schema agreement
@@ -37,9 +37,11 @@ Status legend:
 | `[draft]`
 |===
 
-NOTE: Proposals 0001 and 0002 are `[accepted]` as of 2026-05-30. They
-remain in `docs/proposals/` for now; ADR promotion to
-`docs/decisions/` is a separate file-restructure follow-up.
+NOTE: Proposals 0001 and 0002 were promoted to
+link:../decisions/[ADR-0002 and ADR-0003] on 2026-05-30. The proposal
+files remain in `docs/proposals/` as the canonical wire-format and
+producer-obligation references; the ADRs record the decisions and
+their consequences.
 
 The strategic decisions (D1–D6) from
 link:../PRODUCTION-PATH.adoc[`docs/PRODUCTION-PATH.adoc`] §"Load-bearing