docs(spec): document wire-level carrier sections (proposals 0001 §4 + 0002 §5) (#108)

## Summary

Closes the remaining doc gate for both proposals:
- Proposal 0001 §Acceptance criterion 4 (spec section in
\`spec/type-safety-levels-for-wasm.adoc\`)
- Proposal 0002 §Gate 5 (same)

Adds a new top-level **\"Wire-Level Carrier Sections\"** section after
\"Implementation Architecture\" with all 4 carriers documented:
\`typedwasm.ownership\` (existing), \`typedwasm.regions\` +
\`typedwasm.capabilities\` (proposal 0001 \`[review]\`),
\`typedwasm.access-sites\` (proposal 0002 \`[review]\`).

## Content

Per-section: full wire format (verbatim from the proposals), Idris2
spec-type mappings, codec entry points (\`parse_*\` / \`build_*\` in
\`crates/typed-wasm-verify/src/section.rs\`). Plus overview table,
versioning policy, and cross-references to #106 roadmap + #94 / #95 /
#96 / #97 open questions.

Net +187 lines of doc, no code change.

## What this leaves for [accepted]

Per proposal 0001 §Acceptance criteria:
- [x] Criterion 1 — paired producer sign-off (4 review comments on #165
+ #402)
- [ ] Criterion 2 — wire format mapped against \`Region.idr\` /
\`Pointer.idr\` / \`ResourceCapabilities.idr\` (could land as proof-side
review)
- [x] Criterion 3 — codec landed (regions via #77, capabilities +
access-sites via #107)
- [x] Criterion 4 — **this PR**
- [x] Criterion 5 — cross-repo producer issues filed (ephapax#221,
affinescript#444 shipped)

Per proposal 0002 §Acceptance criteria:
- [x] Gate 1 — ADR-021 v2 emit-flip protocol drafted
- [x] Gate 2 — paired producer review (ephapax#222 + affinescript#449)
- [x] Gate 3 — codec landed (via #107)
- [ ] Gate 4 — \`verify_access_sites\` verifier pass (needs
cross-section MissingDependentCarrier check)
- [x] Gate 5 — **this PR**
- [ ] Gate 6 — cross-repo producer codegen issues

Remaining for both proposals to flip to \`[accepted]\`: the
verifier-pass plumbing (\`verify_capabilities\` for 0001,
\`verify_access_sites\` for 0002 — both cross-section). Tracked under
#106.

## Test plan

- [x] AsciiDoc renders cleanly (table columns balanced, code blocks
valid)
- [x] No path/file references break (verified against current section.rs
API names)
- [x] No collisions with existing spec doc sections
- [x] Doc-only change — no code, no CI implications beyond aspect tests
(which now pass after #105 root-cause fix)

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

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

Author: hyperpolymath

spec/type-safety-levels-for-wasm.adoc

@@ -686,3 +686,190 @@ does NOT address:
 | Rust
 | Makes typed-wasm a TypedQLiser target language
 |===
+
+== Wire-Level Carrier Sections
+
+The post-codegen verifier (`crates/typed-wasm-verify/`) re-enforces a
+subset of these levels on emitted wasm bytes. To do that without
+re-parsing source, producers emit small custom sections — wasm's
+extension mechanism — that carry just enough of the source-level type
+information for the verifier to reconstruct the relevant judgments.
+
+All carrier sections are independently optional from the verifier's
+perspective: absence is "no claim made," not "claim of compliance." A
+producer that emits only `typedwasm.ownership` is conforming with
+respect to L7 / L10 but makes no L2-L6 / L15 claims that the verifier
+can re-check.
+
+[cols="1,1,1,2"]
+|===
+| Section | Covers | Status (2026-05) | Codec entry point
+
+| `typedwasm.ownership`
+| L7 aliasing, L10 linearity
+| Shipped; canonical wire format
+| `parse_ownership_section_payload` / `build_ownership_section_payload`
+
+| `typedwasm.regions`
+| L2 region-binding, L3 type-compatible access, L4 null-safety, L5 bounds-proof, L6 result-type
+| Proposal 0001 `[review]`; codec behind `unstable-l2`
+| `parse_regions_section_payload` / `build_regions_section_payload`
+
+| `typedwasm.capabilities`
+| L15 resource capabilities (lattice + per-function requirements; excluding L15-C per-call-site grants)
+| Proposal 0001 `[review]`; codec behind `unstable-l15`
+| `parse_capabilities_section_payload` / `build_capabilities_section_payload`
+
+| `typedwasm.access-sites`
+| L2 enforcement on emitted bytes (per-instruction `(func_idx, byte_offset) -> (region_id, field_id)` mapping)
+| Proposal 0002 `[review]`; codec behind `unstable-l2`
+| `parse_access_sites_section_payload` / `build_access_sites_section_payload`
+|===
+
+=== `typedwasm.ownership` (L7 / L10)
+
+Wire format (little-endian, byte-aligned):
+
+----
+u32le  count
+for each entry:
+    u32le  func_idx
+    u8     n_params
+    u8[]   param_kinds  (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
+    u8     ret_kind
+----
+
+The verifier reconstructs each function's ownership-annotated signature
+and checks the body against it for L7 (no aliasing of `ExclBorrow`) and
+L10 (`Linear` consumed exactly once on every code path). The 4-kind
+enum (`OwnershipKind`) is fixed at v1.
+
+Lenient on truncation: a short read yields zeros for the missing
+bytes (interpreted as `Unrestricted` kinds and `func_idx = 0`). This
+defence-in-depth choice preserves cross-implementation parity with
+the OCaml reference parser in AffineScript's `lib/tw_verify.ml`.
+
+=== `typedwasm.regions` (L2-L6)
+
+Wire format (little-endian, byte-aligned, lenient on truncation):
+
+----
+u16le   version              (= REGIONS_SECTION_VERSION = 1)
+u32le   region_count
+for each region (in index order, 0..region_count-1):
+    u32le  name_len
+    u8[]   name              (UTF-8, no NUL terminator)
+    u32le  field_count
+    for each field (in declaration order):
+        u32le  field_name_len
+        u8[]   field_name    (UTF-8)
+        u8     kind          (0=Scalar, 1=PtrOwning, 2=PtrBorrow, 3=PtrExclusive)
+        u8     wasm_ty       (0..10 = U8..WBool, 0xFF = N/A for ptr kinds)
+        u32le  target_region (0xFFFFFFFF if Scalar; else index into region table)
+        u8     nullability   (0=NonNull, 1=Nullable)
+        u32le  cardinality   (1=single, n>1=fixed array, 0=unbounded/dynamic)
+    u32le  region_byte_size  (sum-check; verifier may cross-check)
+----
+
+Maps to Idris2 spec types: `region_count` + region table → `List Region`
+(lookup-by-index); `field_count` + field table → `Schema` per region;
+`wasm_ty` → `WasmType` (11 variants); `kind` → `PtrKind` extended with
+`Scalar`; `nullability` → `Nullability`; `cardinality` feeds
+`InBounds idx count` for L5; `target_region` is the foreign-key for L2.
+
+v0 producer surface narrowness — across AffineScript + ephapax, no
+producer emits v128/SIMD / 128-bit ints / reference types /
+variable-cardinality fields. See proposal 0001 §"v0 producer surface"
+for the full reserved-codepoint enumeration.
+
+=== `typedwasm.capabilities` (L15)
+
+Wire format (little-endian, byte-aligned):
+
+----
+u16le   version              (= CAPABILITIES_SECTION_VERSION = 1)
+u32le   capability_count
+for each capability (in index order, 0..capability_count-1):
+    u32le  name_len
+    u8[]   name              (UTF-8)
+u32le   function_count
+for each function:
+    u32le  func_idx          (index into wasm function section)
+    u32le  required_count
+    u32le[required_count]    required_capability_indices
+                             (indices into capability table above;
+                              MUST be strictly increasing → trivially
+                              encodes ResourceCapabilities.DistinctCaps)
+----
+
+Maps to `ResourceCapabilities.idr`: the flat capability table is
+`CapabilitySet`; strictly-increasing `required_capability_indices`
+structurally encodes `DistinctCaps`; per-function indices are the raw
+data the verifier feeds to `ContainedIn`.
+
+L15-C (call-graph monotonicity / `CallCompatible`) is deferred to a
+v1.4.x follow-up section `typedwasm.capability-grants` — see
+typed-wasm#96.
+
+The codec's parser defensively sorts and dedups `required` indices on
+read, so a future producer that regresses on the producer obligation
+still yields a `DistinctCaps`-conforming structure to downstream
+verification.
+
+=== `typedwasm.access-sites` (L2 enforcement)
+
+Wire format (little-endian fixed-width header, LEB128 per entry):
+
+----
+u16le         version                  (= ACCESS_SITES_SECTION_VERSION = 1)
+u32_leb128    entry_count
+for each entry (in producer-emission order):
+    u32_leb128  func_idx
+    u32_leb128  instruction_byte_offset  (within function body, post-codegen,
+                                           post any wasm-opt rewrite)
+    u32_leb128  region_id                (index into typedwasm.regions table)
+    u32_leb128  field_id                 (index into target region's field table)
+----
+
+Encoding B (LEB128 per field) per proposal 0002 measurement: ~5
+B/entry on average, ~1.1% module overhead at the 6-fixture spec scale.
+Encoding A (flat 4× `u32le`, 16 B/entry, ~2.9% overhead) was rejected;
+encoding C (per-function batched delta offsets, ~3.5 B/entry,
+substantially more complex codec) is deferred to a possible v2.
+
+Entries are NOT required to be sorted in v1; a future v2 MAY require
+sorted-by-`(func_idx, offset)` to enable binary search. v1 consumers
+build a `HashMap<(u32, u32), (u32, u32)>` at parse time.
+
+The verifier resolves a typed access by looking up the entry in the
+access-sites map, then cross-referencing `region_id` + `field_id`
+against `typedwasm.regions`. Without this section, L2-the-enforcement
+(every typed access resolves to a declared region/field) cannot fire
+on emitted bytes even though L2-the-spec (regions/fields exist;
+cross-module schema agreement) is fully covered by
+`typedwasm.regions`.
+
+`MissingDependentCarrier` semantics: emitting `typedwasm.access-sites`
+without `typedwasm.regions` is a hard error — the access-sites entries
+reference region/field indices that no companion table resolves.
+
+=== Versioning policy
+
+`typedwasm.ownership` is unversioned (the original carrier; renamed
+from `affinescript.ownership` in PR #65). The three carriers added by
+proposals 0001 + 0002 all begin with `u16le version`. Forward-compat
+contract:
+
+* *Additive* changes (new trailing fields per record) ship as the same
+  major version; the lenient reader silently ignores the new bytes on a
+  v1 consumer.
+* *Breaking* changes bump the version and the verifier rejects unknown
+  versions with a fresh `*SectionError`-style variant (per-section).
+
+=== Cross-references
+
+* Codec: `crates/typed-wasm-verify/src/section.rs`
+* Proposal 0001 (regions + capabilities): `docs/proposals/0001-multi-producer-carrier-section.adoc`
+* Proposal 0002 (access-sites): `docs/proposals/0002-access-site-carrier.adoc`
+* Pre-stage roadmap: typed-wasm#106 (`[review]` → `[accepted]` tracker)
+* Open questions: typed-wasm#94 (WBool wire width), #95 (region-imports v0.3), #96 (capability-grants L15-C), #97 (producer-readiness checklist)