proof: A13 — close last post-A10 audit items (5a/5b/leave-behind/7/8)

Per coordinator pre-clearance for items 5 + 7 + 8 (and the small A12
leave-behind), this round closes the remaining post-A10 audit items
at the statement level.  Same PR (#72) as A10+A11+A12.

* Item 5a closed (L13 x L10): ModuleIsolation.idr imports Linear and
  gains LinearAcrossBoundary + acrossWitness / acrossHandle +
  linearTransferRequiresBoundary (no-bypass) + linearTransferLocal
  (local-case).

* Item 5b closed (L14 x L13): SessionProtocol.idr imports
  ModuleIsolation and gains SessionAcrossBoundary +
  sessionAcrossPreservesState + sessionTransferRequiresBoundary +
  sessionTransferLocal.

* A12 leave-behind closed (RegionDisjoint x byte separation):
  Region.idr gains RegionsOverlap + disjointImpliesNoOverlap +
  regionsOverlapSym.

* Items 7 + 8 stated as obligations (full proofs multi-week): new
  module TypedWasm.ABI.VerifierSpec introduces SpecAccepts /
  VerifierAccepts / SourceAccepts predicates,
  IntentsLinearAcceptable structural witness,
  VerifierSpecAgreement (item 7) and SourceVerifierAgreement
  (item 8) records each bundling soundness + completeness, plus
  sourceImpliesSpec / specImpliesSource composition lemmas.

18 new regression entries (50 -> 68 assertions).  Package size
21 -> 22 modules.  Build green under Idris2 0.8.0.  PROOF-NEEDS,
LEVEL-STATUS, CHANGELOG, STATE.a2ml all updated.

Original 8-item post-A10 audit fully closed; items 7+8 at statement
level (full proof bodies are tracked long-tail).

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -8,7 +8,7 @@ project = "typed-wasm"
 version = "0.1.0"
 last-updated = "2026-05-26"
 status = "active"  # active | paused | archived
-session = "2026-05-26 — Proof-debt pass A10+A11+A12 (PR #72). A10 closes the last 2 NAMED deferred items from PROOF-NEEDS (L12 freshness propagation under concurrent writes via 8 theorems incl. `freshnessPropagatesUnderWrites` + `epistemicFreshness` projector; `compatCommute` mutual-subschema case + `noSpoofingBidir` corollary + 2nd worked example). Also fixed `tests/proof/regression.mjs` Layer 2 from silent no-op `--check` to real `--build`. A11 closes 3 of 8 untracked debts: (1) `Sync.WriteSync` now requires a `FieldVersion` witness; (2) `Knowledge.Observed` grounded in a `Sync` event; (4-partial) first algebraic laws for `composeCertificates`. A12 (post coordinator A12 go-ahead) closes 3 MORE untracked items in same PR: item 4 FULL (switched `composeCertificates` to `Data.Nat.minimum` → `composeAssoc` + `composeHighProvenComm`); item 6 (`RegionDisjoint` + `regionDisjointSym` in Region.idr); item 3 (`containedConcat` + `jointBudgetCompose` — L8↔L15 joint composition in ResourceCapabilities.idr). 19 new theorems total across A10+A11+A12 (8+5+6), regression 25→50. Items 5, 7, 8 inherit to A13. Previous session (2026-05-24/25): Phase 0 closure pass landed 11 PRs (#46..#63)."
+session = "2026-05-26 — Proof-debt pass A10+A11+A12+A13 (PR #72). A10 closes the last 2 NAMED deferred items from PROOF-NEEDS (L12 freshness propagation under concurrent writes via 8 theorems incl. `freshnessPropagatesUnderWrites` + `epistemicFreshness` projector; `compatCommute` mutual-subschema case + `noSpoofingBidir` corollary + 2nd worked example). Also fixed `tests/proof/regression.mjs` Layer 2 from silent no-op `--check` to real `--build`. A11 closes 3 of 8 untracked debts: (1) `Sync.WriteSync` now requires a `FieldVersion` witness; (2) `Knowledge.Observed` grounded in a `Sync` event; (4-partial) first algebraic laws for `composeCertificates`. A12 closes 3 MORE untracked items: item 4 FULL (`Data.Nat.minimum` → `composeAssoc` + `composeHighProvenComm`); item 6 (`RegionDisjoint` + `regionDisjointSym`); item 3 (`jointBudgetCompose` — L8↔L15). A13 (post coordinator pre-clearance for items 5+7+8) closes the rest: item 5a `LinearAcrossBoundary` + `linearTransferRequiresBoundary` (L13×L10 cross-level in ModuleIsolation.idr); item 5b `SessionAcrossBoundary` + `sessionAcrossPreservesState` + `sessionTransferRequiresBoundary` (L14×L13 in SessionProtocol.idr); A12 leave-behind `RegionsOverlap` + `disjointImpliesNoOverlap` (RegionDisjoint→byte-separation in Region.idr); items 7+8 stated as typed obligations in new `TypedWasm.ABI.VerifierSpec` module (`SpecAccepts` / `VerifierAccepts` / `SourceAccepts` predicates, `VerifierSpecAgreement` / `SourceVerifierAgreement` records, `sourceImpliesSpec` / `specImpliesSource` composition lemmas). 34 new theorems total across A10+A11+A12+A13 (8+5+6+15), regression 25→68, package 17→22 modules. Original 8-item post-A10 audit fully closed (items 7+8 at statement level; full proof bodies are multi-week and tracked as long-tail). Previous session (2026-05-24/25): Phase 0 closure pass landed 11 PRs (#46..#63)."
 
 [project-context]
 name = "typed-wasm"
@@ -57,6 +57,11 @@ milestones = [
   { name = "composeCertificates algebraic laws", completion = 100 },  # 2026-05-26 — A11 list-side + A12 full assoc/comm (PR #72) — switched to Data.Nat.minimum, closes audit item 4
   { name = "Region byte-disjointness predicate + symmetry", completion = 100 },  # 2026-05-26 (A12, PR #72) — closes audit item 6; L7/L10 cross-level theorem deferred
   { name = "L8 ↔ L15 joint budget composition theorem", completion = 100 },  # 2026-05-26 (A12, PR #72) — closes audit item 3 via jointBudgetCompose
+  { name = "L13 × L10 cross-level (linear handle across boundary)", completion = 100 },  # 2026-05-26 (A13, PR #72) — closes audit item 5a via LinearAcrossBoundary + linearTransferRequiresBoundary
+  { name = "L14 × L13 cross-level (session handle across boundary)", completion = 100 },  # 2026-05-26 (A13, PR #72) — closes audit item 5b via SessionAcrossBoundary + sessionAcrossPreservesState + sessionTransferRequiresBoundary
+  { name = "RegionDisjoint → byte non-overlap theorem (L7/L10 cross-level)", completion = 100 },  # 2026-05-26 (A13, PR #72) — A12 leave-behind via RegionsOverlap + disjointImpliesNoOverlap
+  { name = "Verifier ↔ Idris2 spec equivalence — STATEMENT", completion = 50 },  # 2026-05-26 (A13, PR #72) — VerifierSpec.idr: VerifierSpecAgreement obligation typed; full bodies multi-week
+  { name = "Source-checker ↔ verifier coverage agreement — STATEMENT", completion = 50 },  # 2026-05-26 (A13, PR #72) — VerifierSpec.idr: SourceVerifierAgreement obligation typed; full bodies multi-week
 ]
 
 [blockers-and-issues]
@@ -87,22 +92,22 @@ actions = [
 
 [maintenance-status]
 last-run-utc = "2026-05-26T20:00:00Z"
-last-report = "PROOF-NEEDS.md (RECONCILIATION 2026-05-26 A12 banner)"   # A10+A11+A12 are the active record; A12 banner is at the top
+last-report = "PROOF-NEEDS.md (RECONCILIATION 2026-05-26 A13 banner)"   # A10+A11+A12+A13 are the active record; A13 banner is at the top; A13 closes the original post-A10 8-item audit at statement level
 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
+total-assertions = 563  # 545→563: proof-regression bumped 50→68 by A13 (PR #72)
 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 = 50,  file = "tests/proof/regression.mjs" },        # 25→44 (A10+A11) → 50 (A12, PR #72): +composeAssoc +composeHighProvenComm +RegionDisjoint +regionDisjointSym +containedConcat +jointBudgetCompose; Layer 2 fixed from --check no-op to --build
+  { name = "proof regression",                assertions = 68,  file = "tests/proof/regression.mjs" },        # 25→44 (A10+A11) → 50 (A12) → 68 (A13, PR #72): +LinearAcrossBoundary+linearTransferRequiresBoundary+linearTransferLocal (5a) +SessionAcrossBoundary+sessionAcrossPreservesState+sessionTransferRequiresBoundary+sessionTransferLocal (5b) +RegionsOverlap+disjointImpliesNoOverlap+regionsOverlapSym (leave-behind) +SpecAccepts+VerifierAccepts+SourceAccepts+IntentsLinearAcceptable+VerifierSpecAgreement+SourceVerifierAgreement+sourceImpliesSpec+specImpliesSource (items 7+8); Layer 2 fixed from --check no-op to --build at A10
   { 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,69 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Proof-debt pass A13 (2026-05-26, same-day continuation)
+
+Per coordinator pre-clearance for items 5 + 7 + 8, this round closes
+the last of the post-A10 audit items at the **statement level**
+(same PR [#72](https://github.com/hyperpolymath/typed-wasm/pull/72)).
+No items remain from that audit; items 7 + 8 are stated as typed
+obligations (full proofs are multi-week and out of one-session
+scope).
+
+- **Item 5a closed** (L13 × L10 cross-level).
+  `ModuleIsolation.idr` imports `Linear` and gains
+  `LinearAcrossBoundary from to regName bs token` (an L13
+  `AccessWitness` paired with an L10 `LinHandle`) plus three
+  theorems: `linearTransferRequiresBoundary` (no-bypass — any
+  non-local handle move requires a concrete boundary in `bs`),
+  `linearTransferLocal` (local-case constructor), and projections
+  `acrossWitness` / `acrossHandle`.
+- **Item 5b closed** (L14 × L13 cross-level).
+  `SessionProtocol.idr` imports `ModuleIsolation` and gains
+  `SessionAcrossBoundary` with `sessionAcrossPreservesState` (the
+  state index survives transfer), `sessionTransferRequiresBoundary`
+  (no-bypass), `sessionTransferLocal` (local-case), and projections.
+  Together they prove a session handle cannot silently change state
+  or escape its module without an L13 witness.
+- **A12 leave-behind closed.**  `Region.idr` gains `RegionsOverlap`
+  (an address inside both region footprints) and
+  `disjointImpliesNoOverlap`, the L7/L10-flavour cross-level lemma
+  that `RegionDisjoint` implies byte-level non-overlap.  Closes the
+  link the A12 disjointness section header explicitly deferred.
+- **Items 7 + 8 stated as obligations.**  New module
+  `TypedWasm.ABI.VerifierSpec` introduces three predicates —
+  `SpecAccepts m` (Idris2 L7+L10 structural acceptance on
+  `ModuleSummary`), `VerifierAccepts m` (opaque; witnessed only by
+  the Rust differential harness via `differentialAccepted`), and
+  `SourceAccepts m` (opaque; witnessed by the source-side harness)
+  — plus two agreement records: `VerifierSpecAgreement` (item 7,
+  Rust verifier ↔ Idris2 spec) and `SourceVerifierAgreement` (item
+  8, source-checker ↔ verifier coverage).  Each record bundles
+  soundness + completeness so partial proofs can land one face at
+  a time.  `sourceImpliesSpec` / `specImpliesSource` are the
+  composition lemmas under both agreements.  The opaque acceptance
+  predicates make the trust boundary inspectable: every
+  `VerifierAccepts` / `SourceAccepts` use traces back to a named
+  fixture id.
+
+**15 new named items added** (`LinearAcrossBoundary`,
+`linearTransferRequiresBoundary`, `linearTransferLocal`,
+`SessionAcrossBoundary`, `sessionAcrossPreservesState`,
+`sessionTransferRequiresBoundary`, `sessionTransferLocal`,
+`RegionsOverlap`, `disjointImpliesNoOverlap`, `regionsOverlapSym`,
+`SpecAccepts`, `VerifierAccepts`, `SourceAccepts`,
+`IntentsLinearAcceptable`, `VerifierSpecAgreement` /
+`SourceVerifierAgreement` / `sourceImpliesSpec` /
+`specImpliesSource`).  Regression: **68/68** under Idris2 0.8.0
+(both layers: source grep + `idris2 --build`).  Package now 22
+modules (was 21 — `VerifierSpec` is the only addition).
+
+**Closed after A13** (post-A10 audit complete): items 5a, 5b, 6
+leave-behind, 7-statement, 8-statement.  Long-tail: full proofs of
+the two agreement records; `LevelAttestation` reindexed-by-witness
+redesign (standards#130 / epic standards#124); WasmCert-Isabelle
+tie-back; emitted-wasm byte-equality.
+
 ### Proof-debt pass A12 (2026-05-26, same-day continuation)
 
 Per coordinator clearance, three more untracked items from the post-A10

LEVEL-STATUS.md

@@ -89,22 +89,23 @@ toolchain remains future work.
 
 | File | believe_me | postulate | assert_total | Checked status |
 |------|-----------|-----------|--------------|----------------|
-| Region.idr | 0 | 0 | 0 | In package.  Structural injectivity added A8 (2026-04-18): `fieldNameInj` / `fieldTypeInj` / `fieldInj` (MkField constructor injectivity), `schemaEqSym` / `schemaEqTrans` (making SchemaEq a full equivalence relation with the pre-existing `schemaEqRefl`), `lookupFieldName` (L2 soundness — `FieldIn name schema` implies `fieldName (lookupField prf) = name`).  A12 (2026-05-26): byte-disjointness layer added — `RegionDisjoint r1 r2` (two constructors covering both orderings of footprint endpoints) plus `regionDisjointSym` proving symmetry.  Closes post-A10 audit item 6.  Cross-level theorem linking disjointness to L7 aliasing-safety and L10 linearity deferred to a future pass. |
+| Region.idr | 0 | 0 | 0 | In package.  Structural injectivity added A8 (2026-04-18): `fieldNameInj` / `fieldTypeInj` / `fieldInj` (MkField constructor injectivity), `schemaEqSym` / `schemaEqTrans` (making SchemaEq a full equivalence relation with the pre-existing `schemaEqRefl`), `lookupFieldName` (L2 soundness — `FieldIn name schema` implies `fieldName (lookupField prf) = name`).  A12 (2026-05-26): byte-disjointness layer added — `RegionDisjoint r1 r2` (two constructors covering both orderings of footprint endpoints) plus `regionDisjointSym` proving symmetry.  Closes post-A10 audit item 6.  A13 (2026-05-26): byte-separation cross-level layer added — `RegionsOverlap r1 r2` (an address inside both region footprints), `disjointImpliesNoOverlap` proving `RegionDisjoint r1 r2 -> Not (RegionsOverlap r1 r2)`, plus `regionsOverlapSym`.  Closes the L7/L10 cross-level link explicitly deferred at A12. |
 | TypedAccess.idr | 0 | 0 | 0 | In package |
 | Levels.idr | 0 | 0 | 0 | In package |
 | Pointer.idr | 0 | 0 | 0 | In package |
 | Effects.idr | 0 | 0 | 0 | In package |
 | Lifetime.idr | 0 | 0 | 0 | In package |
 | Linear.idr | 0 | 0 | 0 | In package |
 | MultiModule.idr | 0 | 0 | 0 | In package.  Flagship no-spoofing theorem proven A6 (2026-04-18): `FieldMatches`, `SchemaSub` preorder (`schemaSubRefl`, `schemaSubTrans`), `ModuleCompat` indexed on modules + schemas (`compatRefl`, `compatTrans`), and the flagship `noSpoofing : ModuleCompat from to imp exp -> FieldMatches f imp -> FieldMatches f exp`.  Worked Rust-exports / AffineScript-imports example (4-field export, 2-field import subset) constructs a live certificate and applies the theorem.  A10 (2026-05-26) closes the deferred `compatCommute` item: mutual-subschema commutativity `compatCommute : ModuleCompat from to imp exp -> SchemaSub exp imp -> ModuleCompat to from exp imp`, plus the `noSpoofingBidir` corollary returning a pair of field-transport functions.  Second worked example (`serviceA`/`serviceB` with permuted schemas) demonstrates `compatCommute` on a case where both `SchemaSub` directions hold. |
-| ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13) |
-| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
+| ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13).  A13 (2026-05-26): L13×L10 cross-level layer added — imports `Linear`, exposes `LinearAcrossBoundary from to regName bs token` (an L13 `AccessWitness` paired with an L10 `LinHandle`) plus accessors `acrossWitness` / `acrossHandle`, the no-bypass theorem `linearTransferRequiresBoundary` (any non-local linear-handle transfer requires a concrete boundary in `bs`, proved by reusing `crossAccessImpliesBoundary`), and `linearTransferLocal` (local-case constructor).  Closes post-A10 audit item 5a. |
+| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14).  A13 (2026-05-26): L14×L13 cross-level layer added — imports `ModuleIsolation`, exposes `SessionAcrossBoundary from to proto state regName bs` plus accessors, `sessionAcrossPreservesState` (the state index survives the transfer), `sessionTransferRequiresBoundary` (no-bypass, same shape as the L10 version one level up), and `sessionTransferLocal`.  Closes post-A10 audit item 5b. |
 | ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15).  A12 (2026-05-26): `containedConcat` proves `ContainedIn` distributes over `++`; `jointBudgetCompose` proves the L8 ↔ L15 **joint** budget composition theorem — given individual `EffectSubsumes` witnesses and individual `FunctionCaps` witnesses for two functions sharing an owner module, the compound function still satisfies both the combined L8 envelope (via `subsumeCompose`) AND the combined L15 module envelope (via `containedConcat` + `l15bSoundness`).  Closes post-A10 audit item 3. |
 | 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.  A11 (2026-05-26): partial laws for `composeCertificates` itself — `achievedAppendSplit` decomposes a `LevelAchievedIn n (xs ++ ys)` into one side; `composeAssocLists` proves the list-level associativity of three-way composition; `composeAchievedSym` is the symmetric counterpart of `composeAchievedL`/`R`, recovering the achieved-side from a composed certificate.  A12 (2026-05-26): switched `composeCertificates` from Ord-derived `Prelude.min` to structural `Data.Nat.minimum` so structural lemmas apply; **full** `composeAssoc` proves three-way associativity across list parts, multi-module parts, AND `highestProven` Nat side (via `minimumAssociative`); `composeHighProvenComm` proves Nat-side commutativity (via `minimumCommutative`).  Closes post-A10 audit item 4 in full. |
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18).  A10 (2026-05-26): propagation theorems added — `freshImpliesEqual`, `staleImpliesLT`, `freshNotStale` (mutual exclusion via local `ltIrreflexive`), `concurrentWriteStales`, `resyncRecoversFresh`, the flagship `freshnessPropagatesUnderWrites`, `syncChainEndsFresh`, and the `epistemicFreshness` projector on `Level12Proof` (closes PROOF-NEEDS §P1.2).  A11 (2026-05-26): constructor-tightening pass — `WriteSync` now demands a `FieldVersion` witness with three equality components (`field`/`version`/`lastWriter`), and `Knowledge.Observed` is grounded in a `Sync` event (no more unfounded versions).  Corollaries: `writeSyncIdentifiesWriter` returns the `FieldVersion` (+ the three projections) for an explicit-or-implicit Sync; `observedHasProvenance` extracts the witnessing prior-version and `Sync` from any `Observed` value. |
 | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
+| VerifierSpec.idr | 0 | 0 | 0 | New module A13 (2026-05-26).  Spec-of-record for items 7+8 of the post-A10 audit at the statement level.  Exposes the abstract `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` shapes shared by the Rust verifier and the Idris2 spec; the structural L10 single-consumption predicate `IntentsLinearAcceptable` and its `TokenFresh` underpinning; the L7+L10 acceptance predicate `SpecAccepts m`; the opaque `VerifierAccepts m` / `SourceAccepts m` predicates (witnessed only by named fixture ids via `differentialAccepted` / `sourceAccepted` to keep the trust boundary inspectable); the two agreement records `VerifierSpecAgreement` (item 7) / `SourceVerifierAgreement` (item 8) each bundling soundness + completeness directions; and composition lemmas `sourceImpliesSpec` / `specImpliesSource` under both agreements.  Statement-only — full proof bodies are multi-week long-tail. |
 
 ## Post-codegen verifier (Rust)