diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index cccd651..1da2965 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -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 diff --git a/spec/ARG-PROFILE.adoc b/spec/ARG-PROFILE.adoc index b08a2af..3629555 100644 --- a/spec/ARG-PROFILE.adoc +++ b/spec/ARG-PROFILE.adoc @@ -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 diff --git a/spec/CRG-PROFILE.adoc b/spec/CRG-PROFILE.adoc index 01b2041..cef68b9 100644 --- a/spec/CRG-PROFILE.adoc +++ b/spec/CRG-PROFILE.adoc @@ -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). diff --git a/spec/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc index 88af79f..2aae40f 100644 --- a/spec/FRG-PROFILE.adoc +++ b/spec/FRG-PROFILE.adoc @@ -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 diff --git a/spec/TRG-PROFILE.adoc b/spec/TRG-PROFILE.adoc index c495136..70dc8e5 100644 --- a/spec/TRG-PROFILE.adoc +++ b/spec/TRG-PROFILE.adoc @@ -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)