docs: sync human+machine docs to 2026-05-27 session (LEVEL-STATUS + CHANGELOG + STATE.a2ml + PRODUCTION-PATH) (#85)

## Summary

Documentation rollup for the 2026-05-27 L2-L6 / L15 carrier-ABI session.
**No new logic** — mirrors what already landed in PRs #76, #77, #78, #81
into the docs surface so future readers and AI agents see the same story
everywhere.

## Files touched

### Human-readable

- **`LEVEL-STATUS.md`** — Coverage section gets a per-level enforcement
table (L7/L10/L13 ✓ enforced; L2–L6/L15 proposal-stage; L14/L16 out of
scope). Open gating items numbered with issue/PR refs.
- **`CHANGELOG.md`** — new `[Unreleased]` section "2026-05-27 Phase 2
carrier-ABI design + C5.1 corpus" listing 3 PRs, 1 resolved issue, 2
cross-repo reviews, test-surface deltas.
- **`docs/PRODUCTION-PATH.adoc`** — §Phase 2 cross-links proposal 0001,
the `unstable-l2` codec pre-stage, and the access-site option A
decision.

### Machine-readable

- **`.machine_readable/6a2/STATE.a2ml`** — `last-updated` bumped,
session line rewritten, milestones added (L13 enforcement 100%, proposal
0001 30%, `unstable-l2` codec 100%, L15 carrier 30%, access-site carrier
15%, C5.1 corpus 100%), test-surface split (default 47 + opt-in 9),
`critical-next-actions` reordered around the proposal sequence. New
`[carrier-abi]` and `[c5-real-fixtures]` sections.

## What this PR does NOT do

- No code changes in `crates/typed-wasm-verify/`.
- No proposal-content edits (PR #76's `7520f00` amendment already added
Open Question #6).
- No new tests.
- Doesn't promote proposal 0001 — still `[draft]` until cross-repo
reviewers respond.

## Test plan

- [x] AsciiDoc / Markdown render cleanly
- [x] No git-cliff regeneration needed (manual `[Unreleased]` edit per
the existing convention)
- [ ] CI green

Refs typed-wasm#76 (proposal 0001)
Refs typed-wasm#77 (unstable-l2 codec)
Refs typed-wasm#78 (access-site carrier — option A)
Refs typed-wasm#81 (C5.1 corpus)

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

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 [metadata]
 project = "typed-wasm"
 version = "0.1.0"
-last-updated = "2026-05-25"
+last-updated = "2026-05-27"
 status = "active"  # active | paused | archived
-session = "2026-05-24/25 — Phase 0 closure pass. 11 PRs landed (#46 CI triage, #47 PRODUCTION-PATH doc, #55 cargo-audit CI, #57 Track C complete +64 assertions and 2 real bugs fixed, #58 tree-sitter scaffold, #59 CI hardening non-blocking, #60 ROADMAP truthfulness audit + drift-detection aspect §8, #61 wiki source-of-truth + STATE.a2ml comprehensive, #62 tree-sitter v1 parses example 01 end-to-end with 0 ERROR, #63 repo tidy RSR-aligned + smoke fix + duplication scrub). Phase 0 gates 1 + 3 met; gate 2 (codegen v0) is the terminal Phase-1-handoff item."
+session = "2026-05-27 — Phase 2 carrier-ABI kickoff. 3 PRs filed + 1 issue resolved. #76 proposal 0001 multi-producer carrier sections (typedwasm.regions for L2-L6, typedwasm.capabilities for L15) [draft]; #77 unstable-l2 codec pre-stage (no verifier pass yet); #81 C5.1 real-AffineScript fixture corpus closes typed-wasm#35 part 2. #78 access-site carrier resolved option A (per-instruction (func_idx, instruction_byte_offset) -> (region_id, field_id)); Encoding B (LEB128) recommended for proposal 0002 (size measurement on issue). Cross-repo review opened: affinescript#402 + ephapax#165 gate proposal 0001 promotion. Previous: 2026-05-24/25 Phase 0 closure pass (11 PRs)."
 
 [project-context]
 name = "typed-wasm"
@@ -51,6 +51,12 @@ milestones = [
   { name = "Wiki source-of-truth at docs/wiki/", completion = 100 },  # 2026-05-25 (PR #61)
   { name = "RSR-template taxonomy alignment (AUDIT.adoc + onboarding/status/proposals stubs)", completion = 100 },  # 2026-05-25 (PR #63)
   { name = "Parser migration ReScript -> AffineScript -> Idris2", completion = 50 },  # ReScript->AffineScript landed; AffineScript->Idris2 still ahead
+  { name = "L13 module isolation enforcement on emitted wasm", completion = 100 },  # PR #37, 2026-05-19
+  { name = "L2-L6 carrier ABI proposal (proposal 0001)", completion = 30 },  # PR #76 filed 2026-05-27; [draft], blocked on affinescript+ephapax review
+  { name = "L2 region-binding codec pre-stage (unstable-l2 feature)", completion = 100 },  # PR #77, 2026-05-27 — codec only, no verifier pass yet
+  { name = "L15 capability carrier ABI", completion = 30 },  # bundled into proposal 0001 (typedwasm.capabilities section)
+  { name = "Access-site carrier (proposal 0002)", completion = 15 },  # issue #78 resolved option A; size measurement done (Encoding B recommended); proposal not yet authored
+  { name = "C5.1 real-AffineScript fixture corpus", completion = 100 },  # PR #81, 2026-05-27 — 4 fixtures + regenerate workflow
 ]
 
 [blockers-and-issues]
@@ -69,6 +75,9 @@ issues = [
 
 [critical-next-actions]
 actions = [
+  "Phase 2: cross-repo review of proposal 0001 carrier-section ABI — externally gated (affinescript#402 + ephapax#165 sit in maintainers' queues).",
+  "Phase 2: after proposal 0001 [accepted], author proposal 0002 (access-site carrier — option A); use Encoding B per the size measurement on issue #78.",
+  "Phase 2: after proposal 0002 [accepted], unstable-l2 codec gets the verify_region_binding pass (deliberately omitted from PR #77).",
   "Track A: extend tree-sitter grammar from region-decls v0 to full spec/grammar.ebnf parity.",
   "Track A: Idris2 parser at 188-test parity with the ReScript parser.",
   "Track A: ReScript cut single PR (auto-closes anti-pattern policy red).",
@@ -80,18 +89,19 @@ actions = [
 ]
 
 [maintenance-status]
-last-run-utc = "2026-05-25T20:00:00Z"
+last-run-utc = "2026-05-27T10:30:00Z"
 last-report = "docs/PRODUCTION-PATH.adoc"   # the canonical strategic doc supersedes one-off audit reports
 last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 4  # Build+E2E + A2ML + K9 non-blocking advisories (PR #59) + anti-pattern policy (fixed by Track A's ReScript cut)
 open-failures = 0  # all gating CI is green; previously-red jobs are explicitly advisory now
 
 [test-surface]
-# Test surface as of 2026-05-24; ~545 assertions across 11 surfaces.
-total-assertions = 545
+# Test surface as of 2026-05-27; ~559 assertions across 12 surfaces.
+total-assertions = 559
 surfaces = [
   { name = "ParserTests.res",                 assertions = 88,  file = "tests/parser/ParserTests.res" },
-  { name = "typed-wasm-verify (Rust)",        assertions = 53,  file = "crates/typed-wasm-verify/" },        # 43 unit + 10 cross-compat
+  { name = "typed-wasm-verify (Rust, default)", assertions = 47, file = "crates/typed-wasm-verify/" },     # 42 unit/cross-compat + 5 C5.1 real-fixture (PR #81, 2026-05-27)
+  { name = "typed-wasm-verify (--features unstable-l2)", assertions = 9, file = "crates/typed-wasm-verify/src/section.rs (regions_tests)" },  # PR #77, 2026-05-27 — opt-in, not run by default CI
   { name = "Per-level tests",                 assertions = 56,  file = "tests/levels/L1.mjs..L10.mjs" },
   { name = "claim-envelope aspect",           assertions = 53,  file = "tests/aspect/claim-envelope.mjs" }, # bumped 49→53 in PR #60 (new section 8 drift detection)
   { name = "security-envelope aspect",        assertions = 10,  file = "tests/aspect/security-envelope.mjs" },  # added 2026-05-24 (PR #57)
@@ -118,3 +128,34 @@ phase-3 = 51
 phase-4 = 52
 phase-5 = 53
 phase-6 = 54
+
+[carrier-abi]
+# Multi-producer carrier sections for L2-L6 and L15.
+# Status as of 2026-05-27.
+proposal-0001-pr = 76
+proposal-0001-status = "draft"
+proposal-0001-acceptance-gates = [
+  "hyperpolymath/affinescript review (issue #402)",
+  "hyperpolymath/ephapax review (issue #165)",
+]
+codec-pre-stage-pr = 77
+codec-feature-flag = "unstable-l2"
+codec-section-name = "typedwasm.regions"
+capabilities-section-name = "typedwasm.capabilities"
+access-site-issue = 78
+access-site-decision = "option A — per-instruction (func_idx, instruction_byte_offset) -> (region_id, field_id)"
+access-site-recommended-encoding = "B (LEB128 per field, ~5 B/access, ~1.1% module overhead)"
+proposal-0002-status = "not yet authored — wait until proposal 0001 [accepted]"
+
+[c5-real-fixtures]
+# Real-AffineScript-emitted .wasm corpus, PR #81 landed 2026-05-27.
+pr = 81
+closes-issue = 35  # part 2
+fixture-dir = "crates/typed-wasm-verify/tests/fixtures/c5_real/"
+fixture-count = 4
+affinescript-sha-pinned = "21edc159caee06a930cb7339b3e729ed5627b823"
+regenerate-workflow = ".github/workflows/c5-regenerate.yml"
+deferred-fixture-gaps = [
+  "Duplicate-Linear violation (source-level borrow checker rejects double-move; needs hand-built fixture outside C5.1)",
+  "Multi-module clean / Linear-twice / isolated-vs-shared-memory (needs multi-module affinescript build harness)",
+]

CHANGELOG.md

@@ -10,6 +10,67 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### 2026-05-27 — Phase 2 carrier-ABI design + C5.1 corpus
+
+Multi-PR session opening the L2–L6 / L15 enforcement path on emitted
+wasm. The verifier today covers L7+L10 (PR #21) + L13 (PR #37);
+proposal 0001 below addresses why L2–L6 / L15 cannot follow without
+a carrier-format ABI, and lands the codec pre-stage + the long-deferred
+real-AffineScript fixture corpus.
+
+**3 PRs filed, auto-merge SQUASH armed:**
+
+- **#76** — `docs/proposals/0001-multi-producer-carrier-section.adoc`.
+  Proposes two new producer-neutral custom sections
+  (`typedwasm.regions` for L2–L6, `typedwasm.capabilities` for L15)
+  alongside the existing `typedwasm.ownership`. Versioned,
+  lenient-readable, field-by-field mapping to `Region.idr` /
+  `Pointer.idr` / `ResourceCapabilities.idr`. Status `[draft]` —
+  blocked on cross-repo review by affinescript and ephapax (both
+  producers of `typedwasm.ownership`). Includes an amendment commit
+  (`7520f00`) recording the resolved Open Question #6 (access-site
+  carrier — option A).
+- **#77** — `cargo feature = "unstable-l2"` codec pre-stage:
+  `typedwasm.regions` parse + build (`section.rs`), 9 round-trip
+  tests, no `verify_region_binding` pass (deliberately omitted —
+  see issue #78). Default surface unchanged; opt-in build for the
+  unstable feature.
+- **#81** — C5.1 real-AffineScript fixture corpus: 4 `.affine`
+  sources + paired `.wasm` bytes + `tests/cross_compat_real.rs`
+  (5 verdict tests) + `.github/workflows/c5-regenerate.yml` drift-
+  detection workflow pinning `affinescript` HEAD
+  `21edc159caee06a930cb7339b3e729ed5627b823`. Closes typed-wasm#35
+  part 2.
+
+**1 issue resolved on the spot:**
+
+- **#78** — access-site carrier gap (discovered while writing the
+  L2 codec; proposal 0001 names regions but does not say how the
+  verifier maps a wasm-level `i32.load offset=N` back to
+  `(region_id, field_id)`). Owner-resolved as option A
+  (per-instruction `typedwasm.access-sites` carrier).
+  Size-measurement comment posted to the issue: across the 6
+  spec examples, Encoding B (LEB128 per field) is the v1
+  recommendation — ~5 B per access, ~1.1% module overhead.
+
+**2 cross-repo review issues filed** (gating proposal 0001
+promotion to `[review]`):
+
+- affinescript#402 — review request, AffineScript-specific
+  producer touchpoints called out (`lib/tw_verify.ml`,
+  `lib/tw_interface.ml`, codegen path).
+- ephapax#165 — review request with the disambiguation note,
+  ephapax-wasm-specific touchpoints (`src/ephapax-wasm/`,
+  `src/ephapax-cli/`).
+
+**Test surface deltas:**
+
+- `typed-wasm-verify` Rust crate: 42 → 47 default tests
+  (+5 C5.1 real-fixture verdict tests).
+- With `--features unstable-l2`: 47 → 52 (+5 with the regions
+  codec round-trip tests; 9 codec tests minus 4 overlap with the
+  base set).
+
 ### Phase 0 closure pass (2026-05-24 / 2026-05-25)
 
 Two sessions of focused engineering-surface stabilisation, closing the

LEVEL-STATUS.md

@@ -128,12 +128,42 @@ this crate re-checks them on the emitted IR to catch codegen bugs.
 | **Post-codegen verifier** | **Emitted wasm respects discipline** | **`crates/typed-wasm-verify/` (Rust)** + `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml` (OCaml, reference impl) |
 
 The Rust crate is a faithful port of the OCaml reference; the OCaml
-files remain the spec of record until the cross-compat suite at
-`crates/typed-wasm-verify/tests/cross_compat.rs` is supplemented with
-real affinescript-emitted fixtures (deferred work, "C5.1").
-
-**Coverage:** L7 (ExclBorrow) + L10 (Linear) only.
-L1-L6, L13-L16 enforcement on emitted wasm is future work.
+files remain the spec of record. The synthetic-fixture cross-compat
+suite at `crates/typed-wasm-verify/tests/cross_compat.rs` is the
+parity oracle; **C5.1** (`tests/cross_compat_real.rs`, landed
+2026-05-27 via PR #81) cross-checks it against real
+`affinescript`-emitted bytes (4-fixture corpus, regenerate workflow
+pins affinescript SHA for drift detection).
+
+**Coverage** (2026-05-27):
+
+| Level | Enforced on emitted wasm? | Where |
+|-------|---------------------------|-------|
+| 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) |
+| 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).
 
 **Consumers** (live as of 2026-05-15):
 

docs/PRODUCTION-PATH.adoc

@@ -159,6 +159,25 @@ Gate to Phase 2:
 Today AffineScript is the only realistic adopter (and only via Track B).
 For typed-wasm to be a real target, other compilers must target it.
 
+Active design work:
+
+* **Proposal 0001** —
+  link:proposals/0001-multi-producer-carrier-section.adoc[Multi-producer
+  carrier sections for L2–L6 and L15] (PR #76, `[draft]` 2026-05-27).
+  Proposes two new producer-neutral custom sections
+  (`typedwasm.regions`, `typedwasm.capabilities`) alongside the
+  existing `typedwasm.ownership`. Blocks L2–L6 / L15 enforcement on
+  emitted wasm. Cross-repo review at affinescript#402 + ephapax#165
+  gates promotion to `[review]`.
+* **Codec pre-stage** (PR #77) — `cargo feature = "unstable-l2"`
+  enables the `typedwasm.regions` codec ahead of `[accepted]` so
+  the wire format gets stress-tested through round-trip tests.
+* **Access-site carrier** — issue #78 (resolved option A;
+  proposal 0002 to be authored once 0001 settles). Closes the
+  "L2-the-enforcement" gap (region/field carriers say *what
+  exists*; access-site carrier says *which load/store hits which
+  field*).
+
 Deliverables:
 
 * **Producer specification document.** Normative: what a third-party