hyperpolymath · hyperpolymath · May 30, 2026 · May 30, 2026
@@ -20,6 +20,60 @@ compile time" (true) and "here is a lemma proving it is forbidden"
 claims — a reviewer asking _"where is the theorem?"_ currently has no
 answer to point at.
 
+## RECONCILIATION 2026-05-30 (carrier-ABI proposals 0001 + 0002 accepted + ADR'd — read this FIRST)
+
+> **The "verifier L1-L6 + L13-L16 coverage on emitted wasm" long-tail
+> item shrinks substantially.** The 2026-05-27 banner below listed
+> this as "in progress on PRs #76 / #77 in a parallel session"; the
+> arc has now closed end-to-end:
+>
+> * **Proposal 0001** (`docs/proposals/0001-multi-producer-carrier-section.adoc`)
+>   — `typedwasm.regions` + `typedwasm.capabilities` carrier sections.
+>   `[accepted]` 2026-05-30 (PR #115) → promoted to
+>   `docs/decisions/0002-multi-producer-carrier-sections.adoc`
+>   (ADR-0002) in PR #116.
+> * **Proposal 0002** (`docs/proposals/0002-access-site-carrier.adoc`)
+>   — `typedwasm.access-sites` per-instruction carrier for L2
+>   enforcement. `[accepted]` 2026-05-30 (PR #115) → promoted to
+>   `docs/decisions/0003-access-site-carrier.adoc` (ADR-0003) in PR
+>   #116.
+> * Verifier passes shipped: `verify_regions_from_module` (PR #107),
+>   `verify_capabilities_from_module` and
+>   `verify_access_sites_from_module` (PR #109) — all behind
+>   `unstable-l2` / `unstable-l15` Cargo features in
+>   `crates/typed-wasm-verify/`.
+>
+> **What this closes.** L2-the-enforcement, L3, L4, L5, L6 (regions
+> half), and L15-A/B on emitted wasm now have carrier-backed verifier
+> passes. `LEVEL-STATUS.md` rows updated from "proposal-stage" to
+> "YES (carrier-backed)" in PR #115.
+>
+> **What is still open in the long-tail.**
+>
+> * **L13 cross-module schema agreement (positive form)** — proposal
+>   0003 (`docs/proposals/0003-region-imports-carrier.adoc`) is
+>   `[draft]`. Wire format defined; gated on producer-side
+>   multi-module emission (AffineScript Roadmap C3 / Ephapax not yet
+>   on roadmap).
+> * **L15-C (per-call-site capability monotonicity)** — proposal
+>   0004 (`docs/proposals/0004-capability-grants-carrier.adoc`) is
+>   `[draft]`. Wire format defined; gated on producer-side L15-A
+>   emission.
+> * **WasmCert-Isabelle tie-back** — unchanged (multi-week external
+>   dependency).
+> * **Emitted-wasm byte-equality (P3.1(a))** — unchanged (blocked
+>   on `.twasm → .wasm` emitter not yet existing).
+> * **Idris2 parser round-trip** — unchanged (blocked on AffineScript
+>   parser port to Idris2).
+> * **Producer-side codegen of access-sites** — AffineScript at
+>   affinescript#462; Ephapax counterpart owner-action pending
+>   (auto-mode classifier blocked the cross-repo create on 2026-05-30).
+>
+> **No `believe_me` / `assert_total` / `postulate` / `sorry` /
+> `assert_smaller` introduced; `%default total` preserved across the
+> arc. The acceptance work was design-doc + ADR + verifier-pass
+> codecs, not new proof obligations.**
+
 ## RECONCILIATION 2026-05-27 (post-A10 items 7 + 8 bodies closed — read this FIRST)
 
 > **The two agreement records introduced by PR #72 / A13 are now

@@ -107,7 +107,7 @@ climb to C without TRG promotion because TRG is already C.
 
 | *Community C1-C5*
 | PARTIAL
-| CONTRIBUTING + CoC + SECURITY present. Discussion venues + RFC list partial: `docs/proposals/0001-*.md`, `docs/proposals/0002-*.md` are the current RFC process.
+| CONTRIBUTING + CoC + SECURITY present. Discussion venues + RFC list partial: `docs/proposals/0001-*.adoc` + `docs/proposals/0002-*.adoc` (`[accepted]` 2026-05-30 → ADR-0002 + ADR-0003); `docs/proposals/0003-*.adoc` + `docs/proposals/0004-*.adoc` are the current `[draft]` RFC corpus.
 
 | *Distribution Δ1-Δ5*
 | PARTIAL

@@ -50,7 +50,7 @@ or vendored artefact.
 | `typed-wasm-verify` (Rust crate) v0.1.0
 | *D*
 | Pre-alpha (workspace-internal, unpublished)
-| `crates/typed-wasm-verify/Cargo.toml`. Post-codegen verifier for L7 (aliasing) + L10 (linearity). 2221 lines (cross 535, lib 180, section 681, verify 825). Feature gate `unstable-l2` pre-stages the L2 region-binding carrier codec for proposal #76. Pinned to wasmparser =0.250.0 / wasm-encoder =0.250.0.
+| `crates/typed-wasm-verify/Cargo.toml`. Post-codegen verifier covering L7 (aliasing), L10 (linearity), L2/L3-L6 (regions + access-sites), and L15-A/B (capabilities). Feature gate `unstable-l2` enables the regions + access-sites carriers and their verifier passes (`verify_regions_from_module` / `verify_access_sites_from_module`); `unstable-l15` enables the capabilities carrier + `verify_capabilities_from_module`. Both gates retained while Phase 3 stabilisation is open. Carrier ABIs accepted 2026-05-30 (proposals 0001 + 0002 → ADR-0002 + ADR-0003). Pinned to wasmparser =0.251.0 / wasm-encoder =0.251.0.
 
 | Idris2 ABI surface at `src/abi/`
 | *C*
@@ -81,7 +81,7 @@ requirements (CRG §4.5+) are not yet met:
 * No `audits/audit-typed-wasm-verify.md` exists.
 * `crates/typed-wasm-verify/README.md` covers usage; no per-file
   CRG annotation.
-* CI runs the verifier against the proposal-0001 4-fixture corpus
+* CI runs the verifier against the proposal-0001 / -0002 fixture corpus
   (per the standards#130 long-tail tracker referenced in
   CHANGELOG.md).
 

@@ -121,7 +121,7 @@ Hygiene status (per `PROOF-NEEDS.md` audit 2026-04-13):
 
 | *C1 — Documented design rationale*
 | YES
-| `README.adoc` "Proofs and implementation" section + `spec/type-safety-levels-for-wasm.adoc` + `docs/proposals/0001-*.md` + `docs/proposals/0002-*.md`.
+| `README.adoc` "Proofs and implementation" section + `spec/type-safety-levels-for-wasm.adoc` + `docs/proposals/0001-*.adoc` + `docs/proposals/0002-*.adoc` (now `[accepted]` + promoted to `docs/decisions/0002-*.adoc` / `0003-*.adoc`).
 
 | *C2 — Documented proof-debt*
 | YES

@@ -83,7 +83,7 @@ the compilation-target interpretation noted above.
 | M2 | Type checker            | *C*  | Per-level type judgements in `src/abi/TypedWasm/ABI/{Levels,Region,Lifetime,Effects,Layout,Linear,Pointer,Tropical,Epistemic,ModuleIsolation,SessionProtocol,ResourceCapabilities,Choreography}.idr` (14 typed-AST files).
 | M3 | Type-checker oracle     | *C*  | The Idris2 ABI files act as the oracle: the Rust verifier (`typed-wasm-verify`) checks emitted WASM against the Idris2-encoded properties; A10 closure (PR #79) inhabits `VerifierSpecAgreement` + `SourceVerifierAgreement`.
 | M4 | Proof dispatcher        | *D*  | Differential constructor at `VerifierAccepts` (per PROOF-NEEDS.md reconciliation block) packages structural witnesses inline via `TrustedFixture`. Not an automated dispatcher in the Coq/Lean sense; oracle-side encoding is the operational equivalent.
-| M5 | Semantics document      | *B*  | `spec/type-safety-levels-for-wasm.adoc` is the canonical operational + denotational doc; `spec/async-convergence-abi.adoc` covers async; `docs/proposals/0001-*.md` + `docs/proposals/0002-*.md` are the live RFC corpus. Strongest M5 in the audit cohort.
+| M5 | Semantics document      | *B*  | `spec/type-safety-levels-for-wasm.adoc` is the canonical operational + denotational doc; `spec/async-convergence-abi.adoc` covers async; `docs/proposals/0001-*.adoc` + `docs/proposals/0002-*.adoc` (`[accepted]` 2026-05-30 → ADR-0002 + ADR-0003) and `docs/proposals/0003-*.adoc` + `docs/proposals/0004-*.adoc` (`[draft]`) are the RFC corpus. Strongest M5 in the audit cohort.
 |===
 
 === Back-end (TRG §3.3)