From 9339d6edaf945039121d43892d885fb4c7c09432 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 16:21:55 +0100 Subject: [PATCH] docs(adr): promote proposals 0001 + 0002 to ADR-0002 + ADR-0003 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Promotes the two `[accepted]` (2026-05-30) proposals to architecture decision records. - Add `docs/decisions/0002-multi-producer-carrier-sections.adoc` — ADR for `typedwasm.regions` + `typedwasm.capabilities` carriers (and reserved slots for access-sites + region-imports). - Add `docs/decisions/0003-access-site-carrier.adoc` — ADR for `typedwasm.access-sites` per-instruction `(region_id, field_id)` carrier (proposal 0001 Open Question §5 → option A). - Cross-link proposals 0001 + 0002 to their ADRs via new `Promoted to` row in each metadata table + inline NOTE. - Rewrite `docs/decisions/README.adoc` from stub to proper ADR index (was a 2-line placeholder; now lists ADR-0001/0002/0003 with authoring guidance and cross-refs). - Update `docs/proposals/README.adoc` to show promotion arrow + revise NOTE block. - LEVEL-STATUS.md Open-gating item #4 (ADR promotion) → DONE. Proposal files are retained as canonical wire-format / producer- obligation references; the ADRs record the decision and consequences in the standard `Context / Decision / Consequences` shape. Existing ADR 0001 (`adopt-rsr-standard`, 2026-02-14) is unaffected — this is purely additive, with new ADR numbers picking up from 0002 in chronological order. --- LEVEL-STATUS.md | 8 +- .../0002-multi-producer-carrier-sections.adoc | 147 ++++++++++++++++++ docs/decisions/0003-access-site-carrier.adoc | 120 ++++++++++++++ docs/decisions/README.adoc | 48 +++++- .../0001-multi-producer-carrier-section.adoc | 7 + docs/proposals/0002-access-site-carrier.adoc | 7 + docs/proposals/README.adoc | 12 +- 7 files changed, 340 insertions(+), 9 deletions(-) create mode 100644 docs/decisions/0002-multi-producer-carrier-sections.adoc create mode 100644 docs/decisions/0003-access-site-carrier.adoc diff --git a/LEVEL-STATUS.md b/LEVEL-STATUS.md index db8c62d..d6d393b 100644 --- a/LEVEL-STATUS.md +++ b/LEVEL-STATUS.md @@ -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 diff --git a/docs/decisions/0002-multi-producer-carrier-sections.adoc b/docs/decisions/0002-multi-producer-carrier-sections.adoc new file mode 100644 index 0000000..e294424 --- /dev/null +++ b/docs/decisions/0002-multi-producer-carrier-sections.adoc @@ -0,0 +1,147 @@ += Architecture Decision Record: 0002-multi-producer-carrier-sections + + + +# 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) diff --git a/docs/decisions/0003-access-site-carrier.adoc b/docs/decisions/0003-access-site-carrier.adoc new file mode 100644 index 0000000..92daeb4 --- /dev/null +++ b/docs/decisions/0003-access-site-carrier.adoc @@ -0,0 +1,120 @@ += Architecture Decision Record: 0003-access-site-carrier + + + +# 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` diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc index 153a5e7..af477c1 100644 --- a/docs/decisions/README.adoc +++ b/docs/decisions/README.adoc @@ -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 diff --git a/docs/proposals/0001-multi-producer-carrier-section.adoc b/docs/proposals/0001-multi-producer-carrier-section.adoc index 9bdeb01..b2557d2 100644 --- a/docs/proposals/0001-multi-producer-carrier-section.adoc +++ b/docs/proposals/0001-multi-producer-carrier-section.adoc @@ -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 diff --git a/docs/proposals/0002-access-site-carrier.adoc b/docs/proposals/0002-access-site-carrier.adoc index 3a0a5f9..6b6ccae 100644 --- a/docs/proposals/0002-access-site-carrier.adoc +++ b/docs/proposals/0002-access-site-carrier.adoc @@ -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 diff --git a/docs/proposals/README.adoc b/docs/proposals/README.adoc index 0a43625..4278192 100644 --- a/docs/proposals/README.adoc +++ b/docs/proposals/README.adoc @@ -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