Skip to content

Commit 9a3b315

Browse files
hyperpolymathhyperpolymath
authored
docs(adr): promote proposals 0001 + 0002 → ADR-0002 + ADR-0003 (#116)
## Summary Stacks on #115. Promotes the two `[accepted]` (2026-05-30) proposals to architecture decision records under `docs/decisions/`. Closes the last open gating item from PR #115's LEVEL-STATUS rewrite (#4 — "ADR promotion"). ## Changes **New files:** - `docs/decisions/0002-multi-producer-carrier-sections.adoc` — ADR for `typedwasm.regions` + `typedwasm.capabilities` carriers, plus reserved slots for access-sites (→ ADR-0003) and region-imports (→ proposal 0003 `[draft]`). Adopted pins: WBool 4B wire, LEB128 per field (option B), cardinality-1 producer surface in v1, opt-in Cargo features. - `docs/decisions/0003-access-site-carrier.adoc` — ADR for `typedwasm.access-sites` per-instruction `(region_id, field_id)` carrier (proposal 0001 OQ §5 → option A). Realised by `verify_access_sites_from_module` in PR #109. **Updated files:** - `docs/decisions/README.adoc` — rewritten from 2-line stub to proper ADR index (ADR-0001 RSR + new ADR-0002 / 0003 + authoring guidance + cross-refs). - `docs/proposals/README.adoc` — index entries gain promotion arrows; NOTE block updated to reflect the promotion instead of the deferral. - `docs/proposals/0001-multi-producer-carrier-section.adoc`, `docs/proposals/0002-access-site-carrier.adoc` — add `Promoted to` metadata row + inline NOTE under the metadata table. Proposal content is unchanged; they remain canonical wire-format references. - `LEVEL-STATUS.md` — Open-gating item #4 (ADR promotion) → DONE with file-path pointers. ## Why now #115 flipped proposals 0001 + 0002 to `[accepted]` but deliberately deferred ADR promotion as a separate auditable PR (file moves + numbering choices). This PR closes that follow-up: - Existing ADR 0001 is `adopt-rsr-standard` (2026-02-14). New ADRs pick up at 0002 / 0003 in chronological order without renumbering anything else. - Proposal files are **retained** rather than removed — the ADRs are short decision records; the proposals carry the wire-format detail, error variants, and producer-readiness checklists. Cross-references point in both directions. ## Stacking note Branched off PR #115's head commit `d9869bb` so the proposal status fields and `docs/proposals/README.adoc` are already at the `[accepted]` baseline. Will rebase cleanly when #115 merges; no content conflict with #115. ## Test plan - [ ] AsciiDoc renders without broken anchors - [ ] `docs/decisions/README.adoc` index entries link to the right files - [ ] Proposal `Promoted to` rows resolve to the new ADRs - [ ] CI green (no source changes; docs-only) 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent 5e932bd commit 9a3b315

7 files changed

Lines changed: 340 additions & 9 deletions

‎LEVEL-STATUS.md‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -163,9 +163,11 @@ pins affinescript SHA for drift detection).
163163
3. **L15-C (call-graph monotonicity)** — proposal 0004 `[draft]`
164164
(`docs/proposals/0004`). Gated on producer-side L15-A emission
165165
(Roadmap C2 not started in either producer).
166-
4. **ADR promotion** — proposals 0001 + 0002 remain in
167-
`docs/proposals/` post-acceptance; promotion to
168-
`docs/decisions/` is a follow-up file-restructure.
166+
4. **ADR promotion** — DONE (2026-05-30): proposals 0001 + 0002
167+
promoted to `docs/decisions/0002-multi-producer-carrier-sections.adoc`
168+
(ADR-0002) and `docs/decisions/0003-access-site-carrier.adoc`
169+
(ADR-0003). Proposal files retained as canonical wire-format
170+
references.
169171

170172
**Spec-of-record alignment (2026-05-27, PR #79).** The
171173
`TypedWasm.ABI.VerifierSpec` Idris2 module now states the

‎docs/decisions/0002-multi-producer-carrier-sections.adoc‎

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
= Architecture Decision Record: 0002-multi-producer-carrier-sections
2+
<!-- SPDX-License-Identifier: MPL-2.0 -->
3+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
4+
5+
# 2. Adopt Multi-Producer Carrier Sections for L2–L6 and L15
6+
7+
Date: 2026-05-30
8+
9+
## Status
10+
11+
Accepted
12+
13+
Promoted from link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
14+
0001] (`[accepted]` 2026-05-30). The proposal file remains canonical for
15+
wire-format detail, error variants, and producer obligations; this ADR
16+
records the decision and its consequences.
17+
18+
## Context
19+
20+
Before this decision, the post-codegen verifier
21+
(`crates/typed-wasm-verify/`) could enforce **L7 (aliasing)**,
22+
**L10 (linearity)**, and **L13 (module isolation, negative form)** on
23+
emitted wasm via the single `typedwasm.ownership` carrier section, but
24+
**L2 (region-binding)**, **L3 (type-compatible access)**, **L4 (null
25+
safety)**, **L5 (bounds-proof)**, **L6 (result-type)**, and
26+
**L15 (resource capabilities)** had no wire surface at all. The
27+
source-level Idris2 spec (`Region.idr`, `Pointer.idr`,
28+
`MultiModule.idr`, `ResourceCapabilities.idr`) modelled all the
29+
required structure, but the moment a producer emitted `.wasm` bytes
30+
the schema and capability data was gone — the source-level checker was
31+
the only line of defence.
32+
33+
Two producers — AffineScript and Ephapax — share `typedwasm` as their
34+
emission target. Without a wire-level agreement, cross-language module
35+
linking (the project's load-bearing differentiator: ADR-0001 RSR
36+
template plus typed shared memory) had no enforcement story on
37+
post-link binaries.
38+
39+
This was an **ABI** problem, not an enforcement problem: the
40+
algorithms existed; the carriers did not.
41+
42+
## Decision
43+
44+
Adopt two new wasm custom sections as the v1 carriers for L2–L6 and
45+
L15 schema/capability data, plus reserve two additional carriers for
46+
the access-site and cross-module follow-ups:
47+
48+
[cols="1,2,3"]
49+
|===
50+
| Section name | Carries | Status
51+
52+
| `typedwasm.regions`
53+
| Region schemas (fields × types × nullability × cardinality)
54+
| Adopted v1 (this ADR); realised in `crates/typed-wasm-verify` PR #107
55+
56+
| `typedwasm.capabilities`
57+
| Capability sets per function signature
58+
| Adopted v1 (this ADR); realised in `crates/typed-wasm-verify` PR #109
59+
60+
| `typedwasm.access-sites`
61+
| Per-instruction `(region_id, field_id)` for typed load/store
62+
| Promoted in link:0003-access-site-carrier.adoc[ADR-0003]
63+
(realises Open Question §5 of proposal 0001)
64+
65+
| `typedwasm.region-imports`
66+
| Cross-module schema agreement (foreign-key regions)
67+
| `[draft]` at link:../proposals/0003-region-imports-carrier.adoc[Proposal
68+
0003]; tracks issue
69+
https://github.com/hyperpolymath/typed-wasm/issues/95[#95]
70+
|===
71+
72+
Wire-format detail (encoding, LEB128 boundaries, error variants,
73+
acceptance criteria) lives in proposal 0001 §"Wire format" and §"Error
74+
variants". Producer obligations and canonical emit order live in
75+
proposal 0001 Appendix B ("Producer-readiness checklist") and
76+
§"Producer obligations".
77+
78+
Key adopted pins:
79+
80+
* **WBool wire width** is **4 bytes** (`i32.store` / `i32.load`)
81+
matching both shipping producers; the Idris2 `sizeOf WBool` is
82+
aligned to 4 in PR #113. A 1-byte `WBoolPacked` is reserved as a
83+
separate `WasmType` constructor, not a width flag on `WBool`.
84+
* **LEB128 per field** (encoding option B) for all variable-width
85+
integer fields in the new carriers — uniform with existing wasm
86+
conventions.
87+
* **Cardinality-1 producer surface in v1**: both shipping producers
88+
emit exactly one of each carrier per module; multi-section behaviour
89+
is reserved for a future amendment.
90+
* Carriers are **opt-in via Cargo features** (`unstable-l2`,
91+
`unstable-l15`) until Phase 3.
92+
93+
## Consequences
94+
95+
### Positive
96+
97+
- Verifier can re-check L2–L6 and L15 on emitted bytes; the
98+
source-level checker is no longer the only line of defence.
99+
- Producers in different source languages (AffineScript, Ephapax,
100+
future) can interoperate through typed shared memory with a single
101+
wire contract.
102+
- The carrier-based design generalises: ADR-0003 (access-sites) and
103+
proposal 0003 (region-imports) and proposal 0004 (capability-grants)
104+
all reuse the same custom-section pattern.
105+
- Idris2 spec and Rust verifier converge on a single source of truth
106+
per carrier (mapping recorded in proposal 0001 Appendix A
107+
"Wire-vs-Idris2-spec mapping").
108+
- Producer-readiness checklist (proposal 0001 Appendix B) gives both
109+
shipping producers a concrete acceptance test before v1 stabilises.
110+
111+
### Negative
112+
113+
- Two carriers add ~400-line emitter surface per producer. Both
114+
AffineScript codegen and Ephapax codegen now have a per-feature debt
115+
to track (AffineScript Roadmap C1/C2/C3; Ephapax
116+
`Codegen.region_stack` dead-code removal).
117+
- Until Phase 3 stabilisation (and feature-gating drop), verifier
118+
consumers must opt in via `unstable-l2` / `unstable-l15`.
119+
- Adding two carriers in v1 means the wire-format error surface grows
120+
by ~12 variants total (proposal 0001 §"Error variants"); each
121+
variant needs a regression test before stabilisation.
122+
123+
### Neutral
124+
125+
- The existing `typedwasm.ownership` carrier (4-kind ownership per
126+
function signature) is unchanged; this ADR is purely additive on
127+
the wire.
128+
- L7, L10, L13 (negative form) enforcement is unaffected — the
129+
ownership carrier still drives them.
130+
- ADRs 0001 (RSR template) and 0002 (this) are orthogonal: this
131+
decision lives at the wasm-ABI layer; RSR lives at the
132+
repo-structure layer.
133+
134+
## Cross-references
135+
136+
* link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
137+
0001] — full wire-format spec (canonical reference)
138+
* link:0003-access-site-carrier.adoc[ADR-0003] — access-site carrier
139+
(companion decision)
140+
* link:../proposals/0003-region-imports-carrier.adoc[Proposal 0003] —
141+
region-imports carrier (cross-module, `[draft]`)
142+
* link:../proposals/0004-capability-grants-carrier.adoc[Proposal 0004]
143+
— capability-grants carrier (L15-C, `[draft]`)
144+
* https://github.com/hyperpolymath/typed-wasm/issues/34[issue #34] —
145+
tracking issue (closed when proposals 0001+0002 reached `[accepted]`)
146+
* https://github.com/hyperpolymath/typed-wasm/issues/50[issue #50] —
147+
Phase 2 (multi-producer adoption)

‎docs/decisions/0003-access-site-carrier.adoc‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
= Architecture Decision Record: 0003-access-site-carrier
2+
<!-- SPDX-License-Identifier: MPL-2.0 -->
3+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
4+
5+
# 3. Adopt Access-Site Carrier (`typedwasm.access-sites`) for L2 Enforcement
6+
7+
Date: 2026-05-30
8+
9+
## Status
10+
11+
Accepted
12+
13+
Promoted from link:../proposals/0002-access-site-carrier.adoc[Proposal
14+
0002] (`[accepted]` 2026-05-30). The proposal file remains canonical
15+
for wire-format detail, error variants, and producer obligations; this
16+
ADR records the decision and its consequences.
17+
18+
Builds on link:0002-multi-producer-carrier-sections.adoc[ADR-0002].
19+
20+
## Context
21+
22+
link:0002-multi-producer-carrier-sections.adoc[ADR-0002] adopts
23+
`typedwasm.regions` as the schema carrier: it tells the verifier *which
24+
regions exist* and *which fields each region declares with what type,
25+
nullability, and cardinality*. It does **not** tell the verifier
26+
**which `(region_id, field_id)` any individual `i32.load` /
27+
`i32.store` is supposed to be against**.
28+
29+
The source-level checker has no problem: it sees `region.get $r .f`
30+
directly in the AST and resolves `$r → region`, `.f → field` at
31+
compile time. After codegen, that statement is some sequence ending in
32+
`i32.load offset=N align=A` — and the `($r, .f)` annotation is gone.
33+
The verifier can re-derive *which region's offset window N falls into*
34+
only if the producer tells it which base pointer (region instance)
35+
was loaded, and a single function may touch several regions.
36+
37+
This was Open Question §5 in proposal 0001, resolved on 2026-05-27 in
38+
favour of option A (per-instruction access-site carrier). The L2
39+
verifier pass `verify_region_binding` was deliberately omitted from PR
40+
#77 because the carrier did not yet exist; this ADR formalises the
41+
decision.
42+
43+
Without this carrier, **L2-the-enforcement** (every typed access
44+
resolves to a declared region/field) could not fire on emitted bytes
45+
— even though **L2-the-spec** (regions/fields exist; cross-module
46+
schema agreement) was fully covered by `typedwasm.regions`.
47+
48+
## Decision
49+
50+
Adopt a third wasm custom section, `typedwasm.access-sites`, that
51+
carries, per typed load/store instruction, the resolved
52+
`(region_id, field_id)` pair the producer intended.
53+
54+
Realised in PR #109 (`verify_access_sites_from_module`).
55+
56+
Key adopted pins:
57+
58+
* Wire format: per-entry `(function_index, instruction_byte_offset,
59+
region_id, field_id)`, all LEB128 (encoding option B uniform with
60+
ADR-0002).
61+
* Entries are **strictly ordered** by `(function_index,
62+
instruction_byte_offset)` so the verifier can binary-search.
63+
* Each typed load/store **must** have exactly one access-site entry;
64+
missing entries are an error (`UnboundAccess`), not a silent skip.
65+
* Cardinality-1 producer surface in v1; same opt-in feature gate as
66+
ADR-0002 (`unstable-l2`).
67+
68+
Error variants and acceptance criteria live in proposal 0002 §"Error
69+
variants" and §"Acceptance criteria".
70+
71+
## Consequences
72+
73+
### Positive
74+
75+
- L2 enforcement (`verify_region_binding`) fires on emitted bytes.
76+
- Carrier is **independent** of `typedwasm.regions`: a producer that
77+
emits regions but not access-sites still gets L3–L6 spec-level
78+
checking; access-sites is what unlocks per-instruction L2.
79+
- Per-instruction granularity means the carrier composes with the
80+
L15-C per-call-site grants design in proposal 0004 (both key off
81+
`(function_index, instruction_byte_offset)`).
82+
- The decision unblocks AffineScript Roadmap C2 (access-site
83+
emission) and the Ephapax counterpart (owner action — classifier
84+
blocked the cross-repo issue; tracked in `#106` comment).
85+
86+
### Negative
87+
88+
- Producer codegen must thread `(region, field)` annotations through
89+
to every typed load/store call-site and serialise them in
90+
carrier-emit order. Both shipping producers have outstanding
91+
codegen work for this.
92+
- Wire-format size: every typed memory access adds ~6–12 bytes of
93+
carrier data (function_index + offset + region_id + field_id, all
94+
LEB128). Acceptable for v1; benchmarked in proposal 0002 §"Wire
95+
format" estimate.
96+
- Cardinality-1 means a producer cannot split access-sites across
97+
multiple sections for incremental emission; reserved for a future
98+
amendment.
99+
100+
### Neutral
101+
102+
- `typedwasm.access-sites` is **opt-in via `unstable-l2`** until
103+
Phase 3, matching ADR-0002.
104+
- The access-site carrier is conceptually simpler than the regions
105+
carrier — no schema, just a sorted lookup table — but it shares
106+
the same feature-gate and the same producer-readiness checklist
107+
entry as proposal 0001 Appendix B.
108+
109+
## Cross-references
110+
111+
* link:../proposals/0002-access-site-carrier.adoc[Proposal 0002] —
112+
full wire-format spec (canonical reference)
113+
* link:0002-multi-producer-carrier-sections.adoc[ADR-0002] — the
114+
schema-carrier decision this ADR builds on
115+
* link:../proposals/0001-multi-producer-carrier-section.adoc[Proposal
116+
0001] — origin of Open Question §5 (resolved into this ADR)
117+
* https://github.com/hyperpolymath/typed-wasm/issues/78[issue #78] —
118+
tracking issue
119+
* https://github.com/hyperpolymath/typed-wasm/pull/109[PR #109] —
120+
realising pass `verify_access_sites_from_module`

‎docs/decisions/README.adoc‎

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,47 @@
1-
= decisions Unit
1+
// SPDX-License-Identifier: MPL-2.0
2+
= Architecture Decision Records (ADRs)
3+
4+
Accepted decisions that shape typed-wasm's architecture. Proposals
5+
that have hardened past the design-doc stage live here; forward-looking
6+
proposals still under discussion live in link:../proposals/[`docs/proposals/`].
7+
8+
== Index
9+
10+
[cols="1,4,1,1"]
11+
|===
12+
| Number | Title | Date | Status
13+
14+
| link:0001-adopt-rsr-standard.adoc[0001]
15+
| Adopt Rhodium Standard Repository (RSR) template
16+
| 2026-02-14
17+
| Accepted
18+
19+
| link:0002-multi-producer-carrier-sections.adoc[0002]
20+
| Adopt multi-producer carrier sections for L2–L6 and L15
21+
| 2026-05-30
22+
| Accepted
23+
24+
| link:0003-access-site-carrier.adoc[0003]
25+
| Adopt access-site carrier (`typedwasm.access-sites`) for L2 enforcement
26+
| 2026-05-30
27+
| Accepted
28+
|===
29+
30+
== Authoring an ADR
31+
32+
. Use link:0000-template.adoc[`0000-template.adoc`] as the starting
33+
template.
34+
. Filename: `NNNN-short-slug.adoc` (numbering continues from the highest
35+
current ADR; pad to 4 digits).
36+
. If the ADR promotes a proposal, link back to the proposal file and
37+
keep the proposal as the canonical wire-format / detail reference.
38+
. Add a row to the index above.
39+
40+
== Related
41+
42+
* link:../proposals/[`docs/proposals/`] — forward-looking proposals
43+
(pre-ADR design docs)
44+
* link:../architecture/[`docs/architecture/`] — current architecture
45+
documentation
46+
* link:../PRODUCTION-PATH.adoc[`docs/PRODUCTION-PATH.adoc`] —
47+
strategic plan; D1–D6 decisions land directly as ADRs here

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,17 @@
1212
| Date | 2026-05-27
1313
| Last-updated | 2026-05-30 (review → accepted; owner-decision after all gates ✅)
1414
| Accepted-by | hyperpolymath (owner), 2026-05-30
15+
| Promoted to | link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002] (2026-05-30)
1516
| Tracks issue | https://github.com/hyperpolymath/typed-wasm/issues/34[#34]
1617
| Phase | Phase 2 (https://github.com/hyperpolymath/typed-wasm/issues/50[#50]) — multi-producer adoption
1718
|===
1819

20+
NOTE: This proposal was promoted to
21+
link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002]
22+
on 2026-05-30. The proposal file is retained as the canonical
23+
reference for wire-format detail, error variants, and producer
24+
obligations; the ADR records the decision and consequences.
25+
1926
== Context
2027

2128
The post-codegen verifier (`crates/typed-wasm-verify/`) enforces **L7

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,18 @@
1212
| Date | 2026-05-28
1313
| Last-updated | 2026-05-30 (review → accepted; owner-decision after all 6 gates ✅)
1414
| Accepted-by | hyperpolymath (owner), 2026-05-30
15+
| Promoted to | link:../decisions/0003-access-site-carrier.adoc[ADR-0003] (2026-05-30)
1516
| Tracks issue | https://github.com/hyperpolymath/typed-wasm/issues/78[#78]
1617
| Phase | Phase 2 (https://github.com/hyperpolymath/typed-wasm/issues/50[#50]) — multi-producer adoption
1718
| Builds on | link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (multi-producer carrier sections)
1819
|===
1920

21+
NOTE: This proposal was promoted to
22+
link:../decisions/0003-access-site-carrier.adoc[ADR-0003] on
23+
2026-05-30. The proposal file is retained as the canonical reference
24+
for wire-format detail, error variants, and producer obligations; the
25+
ADR records the decision and consequences.
26+
2027
== Context
2128

2229
link:0001-multi-producer-carrier-section.adoc[Proposal 0001] (PR

‎docs/proposals/README.adoc‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,11 @@ Status legend:
2222

2323
| link:0001-multi-producer-carrier-section.adoc[0001]
2424
| Multi-producer carrier sections for L2–L6 and L15
25-
| `[accepted]` (2026-05-30)
25+
| `[accepted]` (2026-05-30) → promoted to link:../decisions/0002-multi-producer-carrier-sections.adoc[ADR-0002]
2626

2727
| link:0002-access-site-carrier.adoc[0002]
2828
| Access-site carrier section (`typedwasm.access-sites`) for L2 enforcement
29-
| `[accepted]` (2026-05-30)
29+
| `[accepted]` (2026-05-30) → promoted to link:../decisions/0003-access-site-carrier.adoc[ADR-0003]
3030

3131
| link:0003-region-imports-carrier.adoc[0003]
3232
| Region imports carrier section (`typedwasm.region-imports`) for L13 cross-module schema agreement
@@ -37,9 +37,11 @@ Status legend:
3737
| `[draft]`
3838
|===
3939

40-
NOTE: Proposals 0001 and 0002 are `[accepted]` as of 2026-05-30. They
41-
remain in `docs/proposals/` for now; ADR promotion to
42-
`docs/decisions/` is a separate file-restructure follow-up.
40+
NOTE: Proposals 0001 and 0002 were promoted to
41+
link:../decisions/[ADR-0002 and ADR-0003] on 2026-05-30. The proposal
42+
files remain in `docs/proposals/` as the canonical wire-format and
43+
producer-obligation references; the ADRs record the decisions and
44+
their consequences.
4345

4446
The strategic decisions (D1–D6) from
4547
link:../PRODUCTION-PATH.adoc[`docs/PRODUCTION-PATH.adoc`] §"Load-bearing

0 commit comments

Comments
 (0)