docs: comprehensive update for 2026-05-27 proof-debt closure pass (stacked on #80)

.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 — Proof-debt closure pass.  3 PRs auto-merge SQUASH armed: #79 (TypedWasm.ABI.VerifierSpec, total bodies for VerifierSpecAgreement / SourceVerifierAgreement closing post-A10 items 7 + 8 — design: VADifferential / SADifferential carry inline TrustedFixture so the structural witness travels with fixture metadata, making all four agreement directions total by case analysis; first total no-believe_me agreement values in the codebase); #80 (Proofs.idr LevelAttestationW + WitnessCertificate closing standards#130 long-tail flagged in PROOF-NEEDS 2026-05-18 reconciliation banner — design: 15-ctor witness-indexed GADT with per-level extractors discharging the 'attestation entails the level's semantic property' claim, plus existential SomeAttestationW wrapper enabling WitnessCertificate as the heterogeneous-list lift of ProofCertificate); PR #83 (the second slice) instant-merged into #80's branch because the stacked base wasn't protected, so #80's squashed commit carries both slices.  #74 closed as superseded by #79 (competing Maybe-bridge design replaced by witness-carrying ctor design).  PRs #76 / #77 (verifier L1-L6 carrier section proposal + L2 codec pre-staging) IN PROGRESS by a parallel session — left untouched per parallel-session policy.  Test surface 545 → 627+ assertions (proof regression 25 → 107).  Previous session 2026-05-24/25 = Phase 0 closure pass (11 PRs landed, gates 1 + 3 met; gate 2 codegen v0 is the Phase-1-handoff item)."
 
 [project-context]
 name = "typed-wasm"
@@ -51,6 +51,9 @@ 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 = "VerifierSpecAgreement / SourceVerifierAgreement bodies (post-A10 items 7 + 8)", completion = 100 },  # 2026-05-27 (PR #79, auto-merge armed)
+  { name = "LevelAttestation reindexed-by-witness (standards#130 long-tail)", completion = 100 },  # 2026-05-27 (PR #80, auto-merge armed)
+  { name = "WitnessCertificate lift (heterogeneous-list certificate)", completion = 100 },  # 2026-05-27 (#83 folded into #80)
 ]
 
 [blockers-and-issues]
@@ -79,24 +82,48 @@ actions = [
   "ADRs for the 6 load-bearing decisions D1-D6 from docs/PRODUCTION-PATH.adoc §'Load-bearing decisions' (especially D2: producer-side-only vs runtime-aware, which gates whether Phase 3 happens).",
 ]
 
+[proof-debt-closure-pass-2026-05-27]
+# Snapshot of the 2026-05-27 proof-debt closure pass.  Three PRs auto-merge
+# SQUASH armed at the time of writing.  When all three land, this section
+# can move to history (or be summarised in the session note).
+prs = [
+  { number = 79, title = "VerifierSpec.idr — total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8)", state = "open-auto-merge-armed", branch = "proof/verifier-spec-agreement-bodies", closes-audit-items = ["7", "8"], lines-added = 670, new-regression-assertions = 33 },
+  { number = 80, title = "LevelAttestationW + WitnessCertificate (standards#130 long-tail)",                               state = "open-auto-merge-armed", branch = "proof/level-attestation-witness-indexed", closes-audit-items = ["standards#130 stronger reindexed claim"], lines-added = 828, new-regression-assertions = 49 },
+  { number = 74, title = "items 7+8 design pass + Maybe-returning bridges (superseded by #79)",                            state = "closed", reason = "superseded — competing design with weaker provability of the agreement records" },
+]
+test-surface-delta = "proof regression 25 → 107 (+82); total 545 → 627+"
+banned-pattern-delta = "zero new (believe_me/assert_total/postulate/sorry/assert_smaller); %default total preserved"
+build-oracle = "IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --build src/abi/typed-wasm.ipkg → 22/22 modules under #79, 21/21 under #80, rc=0"
+
+[long-tail-open-after-2026-05-27]
+items = [
+  "WasmCert-Isabelle tie-back (requires external Isabelle/HOL install + bridge — multi-week)",
+  "Emitted-wasm byte-equality P3.1(a) — blocked on .twasm→.wasm emitter not yet existing",
+  "Parser round-trip in Idris2 — blocked on AffineScript parser port to Idris2",
+  "Verifier L1-L6 + L13-L16 coverage on emitted wasm (#34, #35) — IN PROGRESS on PRs #76 / #77 by a parallel session, do not interfere",
+]
+
 [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; ~627 assertions across 11 surfaces.
+# Proof regression jumped 25 → 107 in the 2026-05-27 proof-debt closure
+# pass: +33 from PR #79 (VerifierSpec) and +49 from PR #80
+# (LevelAttestationW + WitnessCertificate).
+total-assertions = 627
 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 = "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)
   { name = "property tests",                  assertions = 29,  file = "tests/property/property_test.mjs" }, # added 2026-05-24 (PR #57)
-  { name = "proof regression",                assertions = 25,  file = "tests/proof/regression.mjs" },        # added 2026-05-24 (PR #57)
+  { name = "proof regression",                assertions = 107, file = "tests/proof/regression.mjs" },        # 25 from PR #57, +33 from PR #79 (VerifierSpec), +49 from PR #80 (LevelAttestationW + WitnessCertificate) — all 2026-05-27
   { name = "smoke E2E",                       assertions = 40,  file = "tests/smoke/e2e-smoke.mjs" },
   { name = "structural E2E",                  assertions = 53,  file = "tests/e2e.sh" },
   { name = "integration (airborne-step)",     assertions = 14,  file = "tests/contracts/airborne-step-state-contract.mjs" },

CHANGELOG.md

@@ -10,6 +10,82 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Proof-debt closure pass (2026-05-27)
+
+Post-Phase-0 sweep of the long-tail items the 2026-05-18 PROOF-NEEDS
+reconciliation banner deferred. Closes the named obligations against
+post-A10 audit items 7 + 8 (verifier ↔ spec, source ↔ verifier
+agreement records) and the standards#130 "LevelAttestation reindexed
+by witness" long-tail. All work additive (no existing definitions
+touched, no prior proofs can regress) and all changes preserve
+`%default total` with zero new `believe_me` / `assert_total` /
+`postulate` / `sorry` / `assert_smaller`.
+
+**3 PRs landed/in flight, all auto-merge SQUASH armed**:
+
+- **#79** — `TypedWasm.ABI.VerifierSpec`: total bodies for
+  `VerifierSpecAgreement` and `SourceVerifierAgreement` (post-A10
+  audit items 7 + 8). New module (~620 LOC) defining the shared
+  spec-of-record surface (`ModuleSummary` / `FunctionSummary` /
+  `OwnershipIntent`), structural acceptance predicates
+  (`TokenFresh` / `IntentsLinearAcceptable` / `FunctionsAccepted`),
+  three acceptance predicates (`SpecAccepts`, `VerifierAccepts`,
+  `SourceAccepts`), the two agreement records with totally-proven
+  bodies, and concrete inhabitants `verifierSpecAgreement` /
+  `sourceVerifierAgreement` (the first total no-`believe_me`
+  agreement values in the codebase). Design choice that unblocked
+  the bodies: `VADifferential` / `SADifferential` carry an inline
+  `TrustedFixture` so the structural witness travels with the
+  fixture metadata — trust-injection moment moves to
+  `MkTrustedFixture` (single audit grep). End-to-end demo through
+  `fixtureCleanLinearConsumerModule` (cross_compat row 1).
+  Discrimination proofs across both ctors show L10 has teeth and
+  the differential escape hatch can't smuggle a bad module past
+  the verifier. **+33 Layer 1 regression assertions.**
+  Side-fix: latent `idris2 --check typed-wasm.ipkg` bug in
+  `regression.mjs` Layer 2 corrected to `--build` (Idris2 0.8.0
+  `--check` rejects ipkg paths; CI was unaffected because Layer 2
+  skips when idris2 not on PATH, but local strict runs failed).
+- **#74** — closed as superseded by #79 (competing `Maybe`-returning
+  bridge design; the witness-carrying ctor design in #79 closes the
+  full bodies that #74's design explicitly framed as "multi-week
+  residual").
+- **#80** — `Proofs.idr` `LevelAttestationW` + `WitnessCertificate`:
+  closes the standards#130 long-tail flagged in PROOF-NEEDS
+  2026-05-18 reconciliation banner ("Stronger 'attestation entails
+  the level's semantic property' (needs `LevelAttestation` reindexed
+  by witness) remains tracked future work under standards#130").
+  Two stacked slices (PR #83 instant-merged into #80's branch
+  because the stacked base wasn't protected; the squashed commit
+  carries both):
+    - **`LevelAttestationW : (n : Nat) -> Type`** — witness-indexed
+      attestation GADT, one constructor per level (15 total). Each
+      packages the level-specific witness. 15 `attestLNW_*` smart
+      ctors. 15 `attestLNW_Entails<Property>` extractors (the
+      "entails-semantic-property" lemmas). `toLegacy` bridge. 15
+      round-trip `Refl`s. Uniform `attestLW_AchievedIn` subsuming
+      the A9 `attestLN_Sound` family.
+    - **`WitnessCertificate`** — `ProofCertificate` lifted to
+      witness-carrying form via existential `SomeAttestationW`.
+      Mirror record. `witnessToLegacy` bridge. `composeWitness`
+      mirror of `composeCertificates`. `composeWitnessLegacyAgree`
+      composition-compat lemma. `WitnessAchieved` predicate lifted.
+      Empty + singleton smart ctors.
+  **+49 Layer 1 regression assertions.**
+
+**Test surface after this pass**: 627+ assertions (up from 545+).
+Per-surface delta: proof regression 25 → 107 (33 from #79 + 49 from
+#80, plus the existing 25).
+
+**What this does NOT close**:
+
+- WasmCert-Isabelle tie-back (requires external Isabelle install)
+- Emitted-wasm byte-equality, P3.1(a) (blocked on `.twasm`→`.wasm`
+  emitter)
+- Parser round-trip in Idris2 (blocked on AffineScript parser port)
+- Verifier L1–L6 + L13–L16 coverage (in progress on PRs #76 / #77 in
+  a parallel session — wire-format proposal + L2 codec pre-staging)
+
 ### Phase 0 closure pass (2026-05-24 / 2026-05-25)
 
 Two sessions of focused engineering-surface stabilisation, closing the

LEVEL-STATUS.md

@@ -101,10 +101,11 @@ toolchain remains future work.
 | SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
 | ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
 | Choreography.idr | 0 | 0 | 0 | In package (v1.5 / L16) |
-| Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts.  Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition. |
+| Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts.  Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition.  Attestation soundness A9 (2026-05-18): per-level `attestLN_Sound` family proving `LevelAchievedIn N [attestLN_X w]` — the weak "certificate claims level N" face.  **Witness-indexed redesign 2026-05-27 (PR #80, closes standards#130 long-tail)**: `LevelAttestationW : (n : Nat) -> Type` GADT with one ctor per level packaging the actual witness; 15 `attestLNW_*` smart ctors; 15 `attestLNW_Entails<Property>` extractors (the "attestation entails the level's semantic property" lemmas — a consumer holding `LevelAttestationW 7` can now discharge L7 alias-freeness via `ExclusiveWitness s`, not just the weak claim-predicate); `toLegacy` bridge; 15 round-trip `Refl`s; uniform `attestLW_AchievedIn` subsuming the A9 family.  **`WitnessCertificate` lift 2026-05-27 (PR #80, folded from #83)**: existential `SomeAttestationW` wrapper, `record WitnessCertificate` mirror of `ProofCertificate` with witness-carrying levels, `witnessToLegacy` bridge, `composeWitness` mirror, `composeWitnessLegacyAgree` compat lemma, `WitnessAchieved` predicate. |
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
+| VerifierSpec.idr | 0 | 0 | 0 | In package (2026-05-27, PR #79).  Spec-of-record for the Rust post-codegen verifier and the source-side checker.  Defines `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` (mirrors the `typedwasm.ownership` custom section), structural acceptance predicates `TokenFresh` / `IntentsLinearAcceptable` / `FunctionsAccepted`, three acceptance predicates `SpecAccepts` / `VerifierAccepts` / `SourceAccepts` (the latter two carry a `TrustedFixture` inline so the differential ctor still terminates in a structural witness), the two **agreement records `VerifierSpecAgreement` (item 7) and `SourceVerifierAgreement` (item 8)** with totally-proven bodies, the concrete inhabitants `verifierSpecAgreement` / `sourceVerifierAgreement` (the first total no-`believe_me` agreement values in the codebase), end-to-end composition lemmas `sourceImpliesSpec` / `specImpliesSource` and `*Concrete` specialisations, demo modules (empty / `allocFreeModule` / `allocFreeWithBorrowModule` / `fixtureCleanLinearConsumerModule` mirrored from cross_compat row 1), and four discrimination proofs (`notSpecAcceptsBadDoubleConsume`, `notVerifierAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSourceAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSpecAcceptsBadDoubleProduce`) showing L10 has teeth and the differential escape hatch cannot smuggle a bad module past the verifier. |
 
 ## Post-codegen verifier (Rust)
 
@@ -133,7 +134,23 @@ files remain the spec of record until the cross-compat suite at
 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.
+L1-L6, L13-L16 enforcement on emitted wasm is future work
+(in progress on PRs #76 / #77 — wire-format proposal + L2 codec
+pre-staging behind `cfg(feature = "unstable-l2")`).
+
+**Spec-of-record alignment (2026-05-27, PR #79).**  The
+`TypedWasm.ABI.VerifierSpec` Idris2 module now states the
+**verifier ↔ spec ↔ source** agreement as totally-proven
+inhabitants of two records (`VerifierSpecAgreement`,
+`SourceVerifierAgreement`).  Closes the multi-week residual flagged
+by PR #74 ("Items 7 + 8 stated as obligations" from PR #72).  The
+Rust verifier's accept-verdicts on differential-harness fixtures are
+modelled via `TrustedFixture m` values that package the structural
+witness inline — the trust-injection moment is `MkTrustedFixture`
+construction (single grep point for audit).  A drift between this
+module and the Rust verifier's behaviour now shows up as either a
+failing differential-harness fixture or as an absent
+`TrustedFixture` registration.
 
 **Consumers** (live as of 2026-05-15):