proof: A12 — close 3 more untracked items (4-full, 6, 3) per coordinator clearance

Per coordinator-routed go-ahead for A12 priority list 1->6 (with items
7+8 cleared as "yours, in typed-wasm"), this round closes three more
untracked items from the post-A10 audit in the same PR #72.

Item 4 (CLOSED IN FULL — supersedes A11 partial).
  Switched composeCertificates from Prelude.min (Ord-derived) to
  Data.Nat.minimum (structural Nat) so the structural lemmas apply
  directly. Coordinator hint pointed at minimum_Comm/Assoc as the
  right primitives.

  New theorems:
    - composeAssoc           : three-way associativity of composition
                               across list parts, multi-module parts,
                               AND highestProven Nat side.
    - composeHighProvenComm  : Nat-side commutativity of composition.

  composeAssocLists is retained as a back-compat corollary.

Item 6 (CLOSED).
  Region.idr gains RegionDisjoint r1 r2 (two constructors capturing
  both orderings of LTE (baseAddr + totalSize) baseAddr', proving
  byte-footprint non-overlap) plus regionDisjointSym proving the
  predicate is symmetric. Cross-level theorem linking disjointness
  to L7 (aliasing-safety) and L10 (linearity) deferred to a future
  pass — the predicate itself was the missing primitive.

Item 3 (CLOSED).
  ResourceCapabilities.idr gains:
    - containedConcat     : ContainedIn distributes over ++
    - jointBudgetCompose  : L8 <-> L15 joint composition theorem.
                            Given individual EffectSubsumes witnesses +
                            individual FunctionCaps witnesses for two
                            functions sharing an owner module, the
                            compound function satisfies both the
                            combined L8 envelope (via subsumeCompose)
                            AND the combined L15 module envelope (via
                            containedConcat + l15bSoundness).

Verification:
  - idris2 --build typed-wasm.ipkg   clean (21 modules, EXIT=0)
  - node tests/proof/regression.mjs  50 passed / 0 failed
    (Layer 1 grep + Layer 2 --build, 6 new theorem assertions)

Docs updated:
  - LEVEL-STATUS.md: Proofs.idr, Region.idr, ResourceCapabilities.idr
    inventory rows extended with A12 attribution
  - PROOF-NEEDS.md: new "RECONCILIATION 2026-05-26 (A12 follow-up)"
    banner above the A11 one
  - CHANGELOG.md [Unreleased]: new "Proof-debt pass A12" subsection
  - .machine_readable/6a2/STATE.a2ml: session field summarises
    A10+A11+A12, 3 new completed milestones, proof-regression
    bumped 44 -> 50

Memory updated:
  - project_typed_wasm_proof_debt_post_a10.md: items 4 (full), 6, 3
    marked CLOSED; remaining open list reduced to {5, 7, 8}

Remaining open (-> A13, coordinator pre-cleared as mine in typed-wasm):
  - Item 5: L13xL10 + L14xL13 cross-level theorems
  - Item 7: Rust verifier <-> Idris2 spec equivalence
  - Item 8: source-checker <-> verifier coverage agreement

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 (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 the A10 audit surfaced: (1) `Sync.WriteSync` now requires a `FieldVersion` witness with 3 projection equalities — adversarial writers ill-typed; (2) `Knowledge.Observed` now grounded in a `Sync` event — unfounded versions unconstructable; (4-partial) first algebraic laws for `composeCertificates` — `achievedAppendSplit`, list-level `composeAssocLists`, `composeAchievedSym`. Nat-min half deferred to A12 (`Prelude.min Nat` is non-structural). 13 new theorems, 44/44 regression passing. Items 3, 5, 6, 7, 8 + Nat-min-of-4 inherit to A12. 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 (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)."
 
 [project-context]
 name = "typed-wasm"
@@ -54,7 +54,9 @@ milestones = [
   { name = "L12 (Epistemic) freshness propagation proof", completion = 100 },  # 2026-05-26 (A10, PR #72) — closes PROOF-NEEDS §P1.2
   { name = "MultiModule mutual-subschema commutativity (compatCommute)", completion = 100 },  # 2026-05-26 (A10, PR #72)
   { name = "Sync/Knowledge constructor provenance tightening", completion = 100 },  # 2026-05-26 (A11, PR #72) — closes post-A10 audit items 1 + 2
-  { name = "composeCertificates algebraic laws", completion = 50 },  # 2026-05-26 (A11, PR #72) — list-level done, Nat-min half deferred to A12
+  { 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
 ]
 
 [blockers-and-issues]
@@ -84,8 +86,8 @@ actions = [
 ]
 
 [maintenance-status]
-last-run-utc = "2026-05-26T19:30:00Z"
-last-report = "PROOF-NEEDS.md (RECONCILIATION 2026-05-26 A11 banner)"   # supersedes prior PRODUCTION-PATH-as-last-report; A10+A11 are the active record
+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-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
@@ -100,7 +102,7 @@ surfaces = [
   { 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 = 44,  file = "tests/proof/regression.mjs" },        # 25→36 (A10, PR #72) → 44 (A11, PR #72): +8 L12 theorems +1 compatCommute +1 noSpoofingBidir +2 A11-Epistemic corollaries +3 A11-Proofs laws; Layer 2 fixed from --check no-op to --build
+  { 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 = "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,43 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Proof-debt pass A12 (2026-05-26, same-day continuation)
+
+Per coordinator clearance, three more untracked items from the post-A10
+audit are closed in the same PR ([#72](https://github.com/hyperpolymath/typed-wasm/pull/72)):
+
+- **Item 4 closed IN FULL.** A11's partial `composeAssocLists`
+  (list-side only) is superseded by `composeAssoc`, which proves
+  three-way associativity of `composeCertificates` across all three
+  fields. Enabled by switching `composeCertificates` from
+  `Prelude.min` to `Data.Nat.minimum` (structural Nat), making
+  `minimumAssociative` apply directly. `composeHighProvenComm` adds
+  Nat-side commutativity via `minimumCommutative`. The old
+  `composeAssocLists` kept as a back-compat corollary.
+- **Item 6 closed.** `Region.idr` gains `RegionDisjoint r1 r2` (two
+  constructors for byte-footprint non-overlap, both orderings) plus
+  `regionDisjointSym` proving symmetry. Cross-level theorem linking
+  disjointness to L7 + L10 deferred to a future pass — the predicate
+  itself was the missing primitive.
+- **Item 3 closed.** `ResourceCapabilities.idr` gains `containedConcat`
+  (proving `ContainedIn` distributes over `++`) plus
+  `jointBudgetCompose`, the L8 ↔ L15 joint composition theorem.
+  Composing two functions with individual `EffectSubsumes` and
+  `FunctionCaps` witnesses yields a single function whose combined
+  effects subsume combined actuals (via L8 `subsumeCompose`) AND
+  whose combined required caps are contained in the owner module's
+  declared caps (via the new `containedConcat` + the existing
+  `l15bSoundness`).
+
+**6 new theorems added** (`composeAssoc`, `composeHighProvenComm`,
+`RegionDisjoint`, `regionDisjointSym`, `containedConcat`,
+`jointBudgetCompose`). Regression: **50/50** under Idris2 0.8.0
+(both layers: source grep + `idris2 --build`).
+
+Open after A12 (→ A13): post-A10 audit items 5 (L13×L10, L14×L13
+cross-level), 7 (Rust verifier ↔ Idris2 spec equivalence), 8
+(source-checker ↔ verifier coverage agreement).
+
 ### Proof-debt pass A10 + A11 (2026-05-26)
 
 Two same-day rounds attacking proof debt against `PROOF-NEEDS.md`. PR

LEVEL-STATUS.md

@@ -89,7 +89,7 @@ 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`). |
+| 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. |
 | TypedAccess.idr | 0 | 0 | 0 | In package |
 | Levels.idr | 0 | 0 | 0 | In package |
 | Pointer.idr | 0 | 0 | 0 | In package |
@@ -99,9 +99,9 @@ toolchain remains future work.
 | 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) |
-| ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
+| 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. |
+| 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) |

PROOF-NEEDS.md

@@ -20,7 +20,51 @@ 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-26 (A11 follow-up — read this FIRST)
+## RECONCILIATION 2026-05-26 (A12 follow-up — read this FIRST)
+
+> **A12 follows A11 in the same calendar day.**  Per coordinator-routed
+> A12 go-ahead, this round closes **3 more** of the 8 untracked gaps
+> from `project_typed_wasm_proof_debt_post_a10.md`:
+>
+> 1. **Item 4 closed IN FULL.**  The A11 partial (`composeAssocLists`
+>    was list-side only) is now superseded by `composeAssoc` proving
+>    three-way associativity of `composeCertificates` across all three
+>    fields (list parts, multi-module parts, AND the `highestProven`
+>    Nat).  Made possible by switching `composeCertificates` from the
+>    Ord-derived `Prelude.min` to the structural `Data.Nat.minimum`
+>    (per coordinator hint), which makes `minimumAssociative` apply
+>    directly.  `composeHighProvenComm` adds Nat-side commutativity
+>    via `minimumCommutative`.  The original `composeAssocLists` is
+>    kept as a back-compat corollary.
+>
+> 2. **Item 6 closed.**  `RegionDisjoint r1 r2` in `Region.idr` —
+>    a two-constructor data type witnessing that two regions' byte
+>    footprints `[baseAddr, baseAddr + totalSize)` don't overlap in
+>    either ordering.  `regionDisjointSym` proves symmetry.  The
+>    cross-level theorem linking disjointness to L7 aliasing-safety
+>    and L10 linearity is left for a future pass — disjointness as a
+>    predicate is the missing primitive the audit flagged.
+>
+> 3. **Item 3 closed.**  `jointBudgetCompose` in
+>    `ResourceCapabilities.idr` proves L8 ↔ L15 joint composition:
+>    given individual `EffectSubsumes` witnesses + individual
+>    `FunctionCaps` witnesses for two functions sharing an owner
+>    module, the compound function satisfies both the combined L8
+>    envelope (via `subsumeCompose`) AND the combined L15 module
+>    envelope (via the new `containedConcat` + the existing
+>    `l15bSoundness`).
+>
+> All five new theorems (`composeAssoc`, `composeHighProvenComm`,
+> `RegionDisjoint`, `regionDisjointSym`, `jointBudgetCompose`,
+> `containedConcat`) are guarded by `tests/proof/regression.mjs`.
+> Regression now **50/50**.
+>
+> Items remaining from the original post-A10 audit (all explicitly
+> A12 → A13 inheritance per coordinator clearance): item 5 (L13×L10,
+> L14×L13 cross-level), item 7 (Rust verifier ↔ Idris2 spec
+> equivalence), item 8 (source-checker ↔ verifier coverage agreement).
+
+## RECONCILIATION 2026-05-26 (A11 follow-up)
 
 > **A11 follows A10 in the same calendar day.**  Where A10 closed the
 > *named* deferred items, A11 attacks three of the **untracked** gaps