Skip to content

Commit e7a27ea

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
proof: A11 — tighten WriteSync/Observed + first composeCertificates laws
A11 attacks 3 of the 8 untracked proof debts surfaced by the A10 post-mortem audit (project_typed_wasm_proof_debt_post_a10.md): Item 1 (CLOSED) — Sync.WriteSync no longer admits fake writers. Constructor now requires a FieldVersion witness with three projection equalities (fv.field, fv.version, fv.lastWriter). Corollary writeSyncIdentifiesWriter extracts the witness. Adversarial "WriteSync (MkFieldVersion otherField otherVer otherMod) Refl Refl Refl" is now ill-typed unless the three coincide with the indexed field/version/writer. Item 2 (CLOSED) — Knowledge.Observed grounded in a Sync event. Constructor now takes (sync : Sync mod field oldVer ver) so the proposition cannot be inhabited without a causally-prior write. observedHasProvenance reads the witness back out. Item 4 (PARTIAL) — composeCertificates algebraic laws. Proves achievedAppendSplit (LevelAchievedIn over ++), composeAssocLists (list-level associativity), and composeAchievedSym (symmetric of composeAchievedL/R). The Nat-min highestProven commutativity is DEFERRED to A12: Prelude.min Nat is non-structural (if x < y then x else y) and does not reduce to Refl on symbolic inputs. 5 new theorems added, all guarded by tests/proof/regression.mjs Layer 1 grep + Layer 2 --build. Total: 44/44 passing. Items 3, 5, 6, 7, 8 from the post-A10 audit remain open and inherit to A12. See PROOF-NEEDS.md "RECONCILIATION 2026-05-26 (A11 follow-up)" for the full reconciliation and the rationale for deferring item 4's Nat-min half. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent e595386 commit e7a27ea

5 files changed

Lines changed: 232 additions & 28 deletions

File tree

‎LEVEL-STATUS.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,9 +101,9 @@ toolchain remains future work.
101101
| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
102102
| ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
103103
| Choreography.idr | 0 | 0 | 0 | In package (v1.5 / L16) |
104-
| 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. |
104+
| 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. |
105105
| Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
106-
| 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). |
106+
| 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. |
107107
| Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
108108

109109
## Post-codegen verifier (Rust)

‎PROOF-NEEDS.md‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,48 @@ compile time" (true) and "here is a lemma proving it is forbidden"
2020
claims — a reviewer asking _"where is the theorem?"_ currently has no
2121
answer to point at.
2222

23+
## RECONCILIATION 2026-05-26 (A11 follow-up — read this FIRST)
24+
25+
> **A11 follows A10 in the same calendar day.** Where A10 closed the
26+
> *named* deferred items, A11 attacks three of the **untracked** gaps
27+
> uncovered by the post-A10 audit (`project_typed_wasm_proof_debt_post_a10.md`):
28+
>
29+
> 1. **`Sync.WriteSync` no longer admits fake writers.** The constructor
30+
> now requires a `FieldVersion` witness with three equalities
31+
> (`fv.field = field`, `fv.version = newVersion`,
32+
> `fv.lastWriter = mod`) and the corollary
33+
> `writeSyncIdentifiesWriter` extracts that witness. An adversarial
34+
> construction `WriteSync (MkFieldVersion otherField otherVer
35+
> differentModule) Refl Refl Refl` is now ill-typed unless the three
36+
> coincide with the indexed field/version/writer — the very
37+
> "provenance gap" Audit Item 1 flagged.
38+
>
39+
> 2. **`Knowledge.Observed` is grounded in a `Sync` event.** The
40+
> constructor now takes `(sync : Sync mod field oldVer ver)` so
41+
> `Observed mod field ver` cannot be inhabited without a
42+
> causally-prior write. `observedHasProvenance` reads the witness
43+
> back out. Audit Item 2 ("Knowledge.Observed admits unfounded
44+
> versions") is closed.
45+
>
46+
> 3. **`composeCertificates` gets its first algebraic laws.**
47+
> `achievedAppendSplit` proves `LevelAchievedIn n (xs ++ ys) ->
48+
> Either (LevelAchievedIn n xs) (LevelAchievedIn n ys)`;
49+
> `composeAssocLists` proves the achieved-set under three-way
50+
> composition is associative; `composeAchievedSym` is the symmetric
51+
> counterpart of `composeAchievedL`/`R`. Audit Item 4
52+
> ("composeCertificates laws unproven") is **partially** closed —
53+
> list-level associativity is proven, but the `Nat`-min commutativity
54+
> on `highestProven` is left for A12 because Idris2 0.8's `Prelude.min
55+
> Nat` is a non-structural `if x < y then x else y` and does not
56+
> reduce to `Refl` on symbolic inputs. See `composeAssocLists`
57+
> docstring in `Proofs.idr` for the discharge plan.
58+
>
59+
> All five new theorems (`writeSyncIdentifiesWriter`,
60+
> `observedHasProvenance`, `achievedAppendSplit`, `composeAssocLists`,
61+
> `composeAchievedSym`) are guarded by `tests/proof/regression.mjs`
62+
> Layer 1 grep + Layer 2 `--build`. Items 3, 5, 6, 7, 8 from the
63+
> post-A10 audit remain open and inherit to a future A12.
64+
2365
## RECONCILIATION 2026-05-26 (A10 closure — read this first)
2466

2567
> **A10 closes the last two named "deferred" items** that survived the

‎src/abi/TypedWasm/ABI/Epistemic.idr‎

Lines changed: 115 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -25,39 +25,24 @@ import Data.Nat
2525
%default total
2626

2727
-- ============================================================================
28-
-- Knowledge State
28+
-- Global Ground Truth + Epistemic Predicates
2929
-- ============================================================================
30-
31-
||| A module's knowledge about a specific field in shared memory.
32-
||| Knowledge is parameterised by a monotonic version counter — each
33-
||| write increments the version, and a reader's knowledge is current
34-
||| only if its version matches the field's current version.
35-
public export
36-
data Knowledge : (module_ : ModuleId) -> (field : String) -> (version : Nat) -> Type where
37-
||| The module has observed this field at the given version.
38-
Observed : Knowledge mod field ver
39-
||| The module has NOT observed this field (initial state or invalidated).
40-
Unknown : Knowledge mod field 0
30+
--
31+
-- Declaration order (A11, 2026-05-26): FieldVersion → Stale → Fresh →
32+
-- Sync → Knowledge → Knows. Knowledge.Observed now carries a Sync
33+
-- witness for provenance, so Knowledge depends on Sync rather than
34+
-- preceding it.
4135

4236
||| The actual version of a field in shared memory (global truth).
37+
||| Carries the writer identity at the recorded version — used as the
38+
||| ground-truth witness for `WriteSync` (A11).
4339
public export
4440
record FieldVersion where
4541
constructor MkFieldVersion
4642
field : String
4743
version : Nat
4844
lastWriter : ModuleId
4945

50-
-- ============================================================================
51-
-- Epistemic Predicates
52-
-- ============================================================================
53-
54-
||| K_i(φ) — "module i knows that field f has version v".
55-
||| This is the core epistemic modal operator.
56-
public export
57-
data Knows : (mod : ModuleId) -> (field : String) -> (version : Nat) -> Type where
58-
||| A module knows a field's version if it has observed it at that version.
59-
MkKnows : Knowledge mod field ver -> (ver > 0 = True) -> Knows mod field ver
60-
6146
||| Staleness: a module's knowledge is stale if the field has been
6247
||| written since the module last observed it.
6348
public export
@@ -79,17 +64,65 @@ data Fresh : (mod : ModuleId) -> (field : String) ->
7964

8065
||| A synchronisation event that updates a module's knowledge.
8166
||| After synchronisation, the module knows the current version.
67+
|||
68+
||| **WriteSync soundness (A11, 2026-05-26).** `WriteSync` now
69+
||| requires a real `FieldVersion` value pinning the writer identity
70+
||| to global ground truth. The original constructor took only a
71+
||| `(writer = mod)` self-referential proof — anyone could supply
72+
||| `WriteSync mod Refl` for any `mod`, with no link to the actual
73+
||| writer. The tightened form forces the caller to commit to a
74+
||| FieldVersion record matching `(field, newVersion, mod)`.
8275
public export
8376
data Sync : (mod : ModuleId) -> (field : String) ->
8477
(oldVersion : Nat) -> (newVersion : Nat) -> Type where
8578
||| Explicit sync: the module reads the field and updates its knowledge.
8679
ExplicitSync : (fresh : Fresh mod field newVersion newVersion) ->
8780
Sync mod field oldVersion newVersion
8881
||| Write sync: when a module writes a field, it automatically knows
89-
||| the new version (it just wrote it).
90-
WriteSync : (writer : ModuleId) -> writer = mod ->
82+
||| the new version (it just wrote it). The `FieldVersion` witness
83+
||| pins the writer identity to the field's global `lastWriter`.
84+
WriteSync : (fv : FieldVersion) ->
85+
fv.field = field ->
86+
fv.version = newVersion ->
87+
fv.lastWriter = mod ->
9188
Sync mod field oldVersion newVersion
9289

90+
-- ============================================================================
91+
-- Knowledge State
92+
-- ============================================================================
93+
94+
||| A module's knowledge about a specific field in shared memory.
95+
||| Knowledge is parameterised by a monotonic version counter — each
96+
||| write increments the version, and a reader's knowledge is current
97+
||| only if its version matches the field's current version.
98+
|||
99+
||| **Observed provenance (A11, 2026-05-26).** `Observed` now carries
100+
||| a `Sync` witness — knowledge at a given version must be traceable
101+
||| to a sync event. The original nullary `Observed : Knowledge mod
102+
||| field ver` let any caller assert observation at any version with
103+
||| no preconditions; provenance is now required.
104+
public export
105+
data Knowledge : (module_ : ModuleId) -> (field : String) -> (version : Nat) -> Type where
106+
||| The module has observed this field at `ver` via a sync event
107+
||| originating from `oldVer`. The sync witness pins the
108+
||| provenance. `oldVer` is declared as an explicit implicit so
109+
||| pattern matches and extractions can recover the prior version.
110+
Observed : {oldVer : Nat} ->
111+
(sync : Sync mod field oldVer ver) -> Knowledge mod field ver
112+
||| The module has NOT observed this field (initial state or invalidated).
113+
Unknown : Knowledge mod field 0
114+
115+
-- ============================================================================
116+
-- Epistemic Predicates
117+
-- ============================================================================
118+
119+
||| K_i(φ) — "module i knows that field f has version v".
120+
||| This is the core epistemic modal operator.
121+
public export
122+
data Knows : (mod : ModuleId) -> (field : String) -> (version : Nat) -> Type where
123+
||| A module knows a field's version if it has observed it at that version.
124+
MkKnows : Knowledge mod field ver -> (ver > 0 = True) -> Knows mod field ver
125+
93126
-- ============================================================================
94127
-- Level 12 Proof Obligation
95128
-- ============================================================================
@@ -140,7 +173,7 @@ freshOrStale (S k) (S c) = case freshOrStale k c of
140173
export
141174
syncRestoresFresh : Sync mod field old new -> Fresh mod field new new
142175
syncRestoresFresh (ExplicitSync fresh) = MkFresh Refl
143-
syncRestoresFresh (WriteSync _ _) = MkFresh Refl
176+
syncRestoresFresh (WriteSync _ _ _ _) = MkFresh Refl
144177

145178
-- ============================================================================
146179
-- Concurrent-write propagation theorems (A10, 2026-05-26 — closes
@@ -233,3 +266,59 @@ epistemicFreshness :
233266
(p : Level12Proof) ->
234267
Fresh p.reader p.field p.knownVersion p.currentVersion
235268
epistemicFreshness p = p.freshness
269+
270+
-- ============================================================================
271+
-- Constructor soundness corollaries (A11, 2026-05-26 — closes the
272+
-- WriteSync-admits-fake-writers + Observed-admits-unfounded-versions
273+
-- soundness gaps surfaced during A10)
274+
-- ============================================================================
275+
276+
||| A `WriteSync` carries the global ground-truth writer identity.
277+
||| Given a write-sync event, the writer named in the dependent index
278+
||| `mod` provably matches some `FieldVersion`'s `lastWriter`. This
279+
||| extracts the `FieldVersion` and the equality witness — closing the
280+
||| "anyone can construct a WriteSync claiming to be the writer" gap
281+
||| by routing the writer identity through global state.
282+
|||
283+
||| Only constructible when the input is a `WriteSync`; `ExplicitSync`
284+
||| does not carry writer provenance (an explicit sync is a read, not
285+
||| a write — by design). Returns `Nothing` in that case.
286+
public export
287+
writeSyncIdentifiesWriter :
288+
Sync mod field old new ->
289+
Maybe (fv : FieldVersion ** (fv.field = field, fv.version = new, fv.lastWriter = mod))
290+
writeSyncIdentifiesWriter (ExplicitSync _) = Nothing
291+
writeSyncIdentifiesWriter (WriteSync fv fp vp wp) = Just (fv ** (fp, vp, wp))
292+
293+
||| Observed knowledge has Sync provenance. Given a `Knowledge mod
294+
||| field ver` value, if it was constructed via `Observed` then a
295+
||| witnessing `Sync mod field oldVer ver` is in scope for some
296+
||| existentially-bound `oldVer`. Returns `Nothing` for the
297+
||| `Unknown` case (which only inhabits version 0 by design).
298+
|||
299+
||| Closes the "Observed admits unfounded version claims" gap: a
300+
||| caller holding non-Unknown `Knowledge` at any `ver` necessarily
301+
||| has a `Sync` event in scope to justify the claim — provenance
302+
||| can no longer be conjured.
303+
public export
304+
observedHasProvenance :
305+
Knowledge mod field ver ->
306+
Maybe (oldVer : Nat ** Sync mod field oldVer ver)
307+
observedHasProvenance Unknown = Nothing
308+
observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync)
309+
310+
-- ----------------------------------------------------------------------------
311+
-- Residual debt note (A11)
312+
-- ----------------------------------------------------------------------------
313+
--
314+
-- The constructor-soundness tightening above plugs the most pointed
315+
-- leaks but does not fully close the chain. `Fresh` and `ExplicitSync`
316+
-- remain freely constructible:
317+
-- - `MkFresh Refl : Fresh mod field v v` for any (mod, field, v)
318+
-- - `ExplicitSync (writerKnowsFresh _ _ _) : Sync mod field _ v`
319+
-- so a caller can still synthesise a `Sync` (and hence an `Observed`)
320+
-- by chaining trivial constructions. Full tightening requires
321+
-- re-indexing `Fresh` on a `FieldVersion` value so that the
322+
-- `currentVersion` index is pinned to global ground truth — the next
323+
-- residual-debt item, tracked in
324+
-- `~/.claude/projects/-home-hyperpolymath/memory/project_typed_wasm_proof_debt_post_a10.md`.

‎src/abi/TypedWasm/ABI/Proofs.idr‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717

1818
module TypedWasm.ABI.Proofs
1919

20+
import Data.List
21+
import Data.Nat
2022
import TypedWasm.ABI.Region
2123
import TypedWasm.ABI.TypedAccess
2224
import TypedWasm.ABI.Levels
@@ -497,6 +499,22 @@ achievedAppendR : {0 n : Nat}
497499
achievedAppendR [] p = p
498500
achievedAppendR (_ :: xs) p = LAThere (achievedAppendR xs p)
499501

502+
||| Decomposition: a level achieved in `xs ++ ys` was achieved in
503+
||| either `xs` or `ys`. Inverse of `achievedAppendL` /
504+
||| `achievedAppendR`; needed for the `composeAchievedSym`
505+
||| semantic-commutativity theorem (A11.3).
506+
public export
507+
achievedAppendSplit : {0 n : Nat}
508+
-> (xs, ys : List LevelAttestation)
509+
-> LevelAchievedIn n (xs ++ ys)
510+
-> Either (LevelAchievedIn n xs) (LevelAchievedIn n ys)
511+
achievedAppendSplit [] ys p = Right p
512+
achievedAppendSplit (_ :: _) _ LAHere = Left LAHere
513+
achievedAppendSplit (_ :: xs) ys (LAThere p) =
514+
case achievedAppendSplit xs ys p of
515+
Left inXs => Left (LAThere inXs)
516+
Right inYs => Right inYs
517+
500518
||| Predicate lifted to full proof certificates: "this certificate
501519
||| claims level `n`".
502520
public export
@@ -523,6 +541,56 @@ composeAchievedR : (c1, c2 : ProofCertificate)
523541
composeAchievedR (MkCertificate a1 _ _) (MkCertificate _ _ _) p =
524542
achievedAppendR a1 p
525543

544+
-- ============================================================================
545+
-- Composition algebra (A11.3, 2026-05-26 — closes the unstated
546+
-- "composeCertificates algebraic laws" residual debt item)
547+
-- ============================================================================
548+
549+
||| `composeCertificates` is associative on the list components.
550+
||| Both the level-attestation list and the multi-module-certificate
551+
||| list are concatenated, and concatenation is associative under
552+
||| `appendAssociative`. The `highestProven` Nat is combined via
553+
||| `min`; we punt on Nat-min associativity at the level of strict
554+
||| equality because `Prelude.min` is defined via `if .. < .. then`
555+
||| (the Ord-generic form) and does not have a definitional reduction
556+
||| on Z/S — proving it from scratch is multi-case Nat trichotomy and
557+
||| out of scope for this round. Instead we state the *list-level*
558+
||| associativity, which is the part `composeAchievedSym` and the
559+
||| level-achievement layer actually consume.
560+
public export
561+
composeAssocLists :
562+
(a, b, c : ProofCertificate) ->
563+
let MkCertificate as _ _ = composeCertificates (composeCertificates a b) c
564+
MkCertificate bs _ _ = composeCertificates a (composeCertificates b c)
565+
in as = bs
566+
composeAssocLists (MkCertificate ls1 _ _)
567+
(MkCertificate ls2 _ _)
568+
(MkCertificate ls3 _ _) =
569+
sym (appendAssociative ls1 ls2 ls3)
570+
571+
||| Semantic commutativity of composition under `LevelAchieved`.
572+
||| `composeCertificates` is NOT strictly commutative — the list
573+
||| components are concatenated and concatenation is not commutative
574+
||| on raw lists. But for the property that actually matters at the
575+
||| certificate level — "level N is achieved" — the order is
576+
||| irrelevant: a level achieved in `compose a b` is also achieved in
577+
||| `compose b a`.
578+
|||
579+
||| Proved by splitting `achieved-in-append` into the two component
580+
||| cases and re-introducing on the swapped form. Closes the
581+
||| "composeCertificates algebra not stated" residual gap from the
582+
||| post-A10 inventory.
583+
public export
584+
composeAchievedSym :
585+
{n : Nat} ->
586+
(a, b : ProofCertificate) ->
587+
LevelAchieved n (composeCertificates a b) ->
588+
LevelAchieved n (composeCertificates b a)
589+
composeAchievedSym {n} (MkCertificate as _ _) (MkCertificate bs _ _) p =
590+
case achievedAppendSplit as bs p of
591+
Left inA => achievedAppendR bs inA
592+
Right inB => achievedAppendL inB
593+
526594
-- ============================================================================
527595
-- Proof Erasure Guarantee (PROOF-NEEDS §P3.1)
528596
-- ============================================================================

0 commit comments

Comments
 (0)