docs: proposals 0001 + 0002 → [accepted] (owner decision 2026-05-30) (#115)

## Summary

Owner-decision close of the proposal-acceptance arc. Both proposals
satisfied every acceptance gate this session ([see #106 wrap-up
comment](#106 (comment)));
this PR applies the status flip.

## Status changes

- `docs/proposals/0001-multi-producer-carrier-section.adoc` — `review →
accepted`
- `docs/proposals/0002-access-site-carrier.adoc` — `review → accepted`
- `docs/proposals/README.adoc` — "Current proposals" table updated; NOTE
block clarifies files remain in `docs/proposals/` (ADR promotion is a
separate file-restructure follow-up).

## LEVEL-STATUS.md updates

| Level | Before | After |
|-------|--------|-------|
| L2 (region binding) | proposal-stage | **YES** (carrier-backed) —
`verify_access_sites_from_module` (PR #109); gated `unstable-l2` |
| L3–L6 (type-compat, null, bounds, result-type) | proposal-stage |
**YES** (carrier-backed, schema half) — regions codec PR #107;
per-access enforcement gated on producer codegen |
| L15-A/B (capabilities) | proposal-stage | **YES** (carrier-backed) —
`verify_capabilities_from_module` (PR #109); gated `unstable-l15` |
| L13 cross-module (positive form) | — | proposal-stage — proposal 0003
`[draft]` (new row) |

"Open gating items" section rewritten to remove obsolete pre-acceptance
gates (all shipped via #107/#109) and enumerate the remaining
producer-side prerequisites + [draft] proposal 0003/0004 work.

## What this DOES NOT change

- **File locations**: proposals stay in `docs/proposals/`. ADR promotion
to `docs/decisions/` (with renumbering — existing ADR 0001 is
"adopt-rsr-standard", so proposals 0001/0002 would become ADRs
0002/0003) is a deliberate separate PR to keep the status flip cleanly
auditable.
- **Code**: no source or test changes. Verifier passes already shipped
in #107/#109 behind `unstable-l2` / `unstable-l15` feature flags.
- **Producer-side codegen**: still pending per Appendix B prerequisites
in proposal 0001.

## Test plan

- [x] Status field flipped on both proposals.
- [x] README table reflects new statuses with date.
- [x] LEVEL-STATUS L2/L3-L6/L15 rows show carrier-backed YES.
- [x] Open gating items rewritten (4 items: producer codegen, L13
cross-module, L15-C, ADR promotion).
- [ ] CI passes (doc-only changes; no Cargo/Idris2 build risk).

## Related

- #34 (proposal 0001 umbrella)
- #78 (proposal 0002 RFC)
- #106 (acceptance roadmap tracker — full wrap-up comment)
- This session's 5-PR sprint that satisfied every gate: #107 (codec),
#108 (spec doc), #109 (verifier), #110 (Criterion 2 appendix), #111
(proposal 0004 draft for #96), #112 (proposal 0003 draft for #95), #113
(WBool pin for #94), #114 (producer-readiness for #97).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

LEVEL-STATUS.md

@@ -143,28 +143,29 @@ pins affinescript SHA for drift detection).
 | L7 (aliasing) | **YES** | `verify_function` per-path use-range |
 | L10 (linearity) | **YES** | `verify_function` per-path use-range |
 | L13 (module isolation, negative form) | **YES** | `verify_from_module`, gated on ownership-section presence (PR #37, 2026-05-19) |
-| L2–L6 (region binding, type-compat, null, bounds, result-type) | **proposal-stage** | Carrier-section ABI draft at PR #76 (`docs/proposals/0001`); codec pre-staged behind `cargo feature = "unstable-l2"` at PR #77 |
-| L15 (resource capabilities, L15-A/B) | **proposal-stage** | Same proposal 0001 (separate `typedwasm.capabilities` section) |
+| L13 (cross-module schema agreement, positive form) | **proposal-stage** | `typedwasm.region-imports` carrier — proposal 0003 `[draft]` (`docs/proposals/0003`); blocked on producer-side multi-module emission |
+| L2 (region binding) | **YES** (carrier-backed) | `verify_access_sites_from_module` PR #109; reads `typedwasm.regions` + `typedwasm.access-sites` (proposals 0001 + 0002 `[accepted]` 2026-05-30; codec PR #107; gated `cargo feature = "unstable-l2"`) |
+| L3–L6 (type-compat, null, bounds, result-type) | **YES** (carrier-backed, schema half) | `typedwasm.regions` codec PR #107; cross-checks against `Region.idr::WasmType`, `Pointer.idr::Nullability`, cardinality. Per-access enforcement gated on producer codegen of access-sites (`affinescript#462`, ephapax pending). |
+| L15 (resource capabilities, L15-A/B) | **YES** (carrier-backed) | `verify_capabilities_from_module` PR #109; reads `typedwasm.capabilities` (proposal 0001 `[accepted]`; codec PR #107; gated `cargo feature = "unstable-l15"`). L15-C deferred to proposal 0004 `[draft]`. |
 | L14, L16 | **out of scope** | Gated on AffineScript surface work (no `session`/`choreography` producer emission yet) |
 
-**Open gating items** (post proposal 0001 acceptance):
-
-1. **Access-site carrier** — issue #78. Proposal 0001's region/schema
-   carrier says *which regions exist*; it does not say which
-   `(region_id, field_id)` any individual wasm `i32.load offset=N`
-   targets. Owner-resolved 2026-05-27 as **option A**
-   (per-instruction `typedwasm.access-sites` carrier mapping
-   `(func_idx, instruction_byte_offset) → (region_id, field_id)`).
-   Wire-format design lands as `docs/proposals/0002-access-site-carrier.adoc`
-   (future session). Encoding-B size measurement recorded on issue #78
-   (~5 B/access, ~1.1% module overhead vs ~3.5 B raw access).
-2. **Cross-repo wire-format review** — affinescript#402, ephapax#165.
-   Both producers must sign off on the `typedwasm.regions` and
-   `typedwasm.capabilities` formats before proposal 0001 moves from
-   `[draft]` → `[review]` → `[accepted]`.
-3. **`verify_region_binding` Rust pass** — explicitly omitted from
-   PR #77; gated on proposal 0002's acceptance (needs the access-site
-   carrier to bind individual loads/stores back to regions).
+**Open gating items** (post proposals 0001 + 0002 acceptance, 2026-05-30):
+
+1. **Producer codegen** — verifier passes ship; producer-side emission
+   lags. See proposal 0001 §"Appendix B — Producer-readiness checklist"
+   for IR prerequisites of each carrier. Tracking:
+   `affinescript#444` (Tw_section dedup, ✅ merged), `affinescript#462`
+   (access-sites codegen), `ephapax#221` (Ty::Borrow surfacing) +
+   ephapax access-sites issue (owner action pending).
+2. **L13 cross-module (positive form)** — proposal 0003 `[draft]`
+   (`docs/proposals/0003`). Gated on producer-side multi-module
+   emission (AffineScript Roadmap C3 / Ephapax not yet on roadmap).
+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.
 
 **Spec-of-record alignment (2026-05-27, PR #79).**  The
 `TypedWasm.ABI.VerifierSpec` Idris2 module now states the

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

@@ -7,10 +7,11 @@
 
 [cols="1,3"]
 |===
-| Status       | review
+| Status       | accepted
 | Author       | hyperpolymath
 | Date         | 2026-05-27
-| Last-updated | 2026-05-30 (+ Criterion 2 wire↔spec review appendix)
+| Last-updated | 2026-05-30 (review → accepted; owner-decision after all gates ✅)
+| Accepted-by  | hyperpolymath (owner), 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
 |===

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

@@ -7,10 +7,11 @@
 
 [cols="1,3"]
 |===
-| Status       | review
+| Status       | accepted
 | Author       | hyperpolymath
 | Date         | 2026-05-28
-| Last-updated | 2026-05-30
+| Last-updated | 2026-05-30 (review → accepted; owner-decision after all 6 gates ✅)
+| Accepted-by  | hyperpolymath (owner), 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)

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
-| `[review]`
+| `[accepted]` (2026-05-30)
 
 | link:0002-access-site-carrier.adoc[0002]
 | Access-site carrier section (`typedwasm.access-sites`) for L2 enforcement
-| `[review]`
+| `[accepted]` (2026-05-30)
 
 | link:0003-region-imports-carrier.adoc[0003]
 | Region imports carrier section (`typedwasm.region-imports`) for L13 cross-module schema agreement
@@ -37,6 +37,10 @@ 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.
+
 The strategic decisions (D1–D6) from
 link:../PRODUCTION-PATH.adoc[`docs/PRODUCTION-PATH.adoc`] §"Load-bearing
 decisions" are tracked there directly; each will land an ADR under