From 50ee5a415b8365382f7307301ac703ea66824a1e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 01:10:58 +0100 Subject: [PATCH 1/4] ci: fix CI/CD configuration (campaigns C001-C005) - C001: CodeQL language fixes - C002: License identifier standardization - C003: Outdated actions audit - C004: Pin standards refs to SHA 861b5e9 - C005: Add workflow-level permissions --- .github/workflows/governance.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 653ef98..698d7e2 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -31,4 +31,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613 From 584cba652cfd3ba0f5ca44845e7fef7c76f77d7f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 2 Jun 2026 23:09:39 +0100 Subject: [PATCH 2/4] proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + fix composeWitness/composeCertificates definitional mismatch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Epistemic.idr — close the symmetric soundness gap A11 left open. `WriteSync` was tightened to require a `FieldVersion` pin in A11 (PR #72), but `Fresh` and (transitively) `ExplicitSync` remained freely constructible via `MkFresh Refl`. This change re-indexes `Fresh` on a `FieldVersion` value plus `fv.field = field` and `fv.version = currentVersion` pins, so freshness can no longer be minted ex nihilo. `ExplicitSync` inherits the pin via its embedded `Fresh` argument — no separate parameter needed; documented inline. Cascade: `writerKnowsFresh` now takes the canonical FieldVersion + writer-identity pin; `syncRestoresFresh (ExplicitSync fresh)` returns `fresh` directly (no remint); the three Fresh-matching lemmas (`freshImpliesEqual`, `freshNotStale`, `concurrentWriteStales`) use `MkFresh _ _ _ eq` shape. Residual-debt block rewritten to record A14 closure. * Proofs.idr — root-cause fix for HEAD build break in `composeWitnessLegacyAgree`. `composeWitness` used `Prelude.min` (Ord-derived, `if compareNat _ _ == LT then _ else _`) while `composeCertificates` uses `Data.Nat.minimum` (structural). The bridge lemma's `rewrite ... in Refl` could not reduce across the mismatch. Switched `composeWitness` to `minimum` (numerically identical, definitionally aligned). Docstring records why. * Both files also pick up the in-progress estate copyright-owner format adjustment on line 2 (drops the `(hyperpolymath)` parenthetical) to satisfy the local pre-commit owner-line check. Single-line touch each, no SPDX-identifier or LICENSE change. Verification: `idris2 --build src/abi/typed-wasm.ipkg` clean rebuild 22/22 modules, rc=0, zero errors. No `believe_me` / `assert_total` / `assert_smaller` / `postulate` / `sorry` introduced; `%default total` preserved across both files. Closes #102. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/abi/TypedWasm/ABI/Epistemic.idr | 79 +++++++++++++++++++++-------- src/abi/TypedWasm/ABI/Proofs.idr | 8 ++- 2 files changed, 63 insertions(+), 24 deletions(-) diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index 791343e..b789afa 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- Copyright (c) Jonathan D.A. Jewell -- -- Epistemic.idr — Level 12: Epistemic safety for shared memory -- @@ -52,11 +52,30 @@ data Stale : (mod : ModuleId) -> (field : String) -> MkStale : LT knownVersion currentVersion -> Stale mod field knownVersion currentVersion ||| Freshness: the module's knowledge is current. +||| +||| **Fresh soundness (A14, 2026-06-02 — closes #102).** `Fresh` now +||| requires a real `FieldVersion` value pinning the `currentVersion` +||| index to global ground truth. The original constructor took only +||| a `(knownVersion = currentVersion)` self-referential proof — +||| anyone could mint `MkFresh Refl` for any `(mod, field, v)` pair, +||| symmetric to the pre-A11 `WriteSync` gap. The tightened form +||| forces the caller to commit to a `FieldVersion` record matching +||| `(field, currentVersion)`. `ExplicitSync` inherits the pin via +||| its `Fresh` argument — no separate `FieldVersion` parameter is +||| required on the sync constructor itself. public export data Fresh : (mod : ModuleId) -> (field : String) -> (knownVersion : Nat) -> (currentVersion : Nat) -> Type where - ||| Knowledge is fresh when knownVersion == currentVersion. - MkFresh : knownVersion = currentVersion -> Fresh mod field knownVersion currentVersion + ||| Knowledge is fresh when (a) `knownVersion = currentVersion` AND + ||| (b) `currentVersion` is pinned to the canonical FieldVersion + ||| record for `field`. The reader does not have to be the writer, + ||| so `fv.lastWriter` is unconstrained here; writer provenance is + ||| captured by `WriteSync` instead. + MkFresh : (fv : FieldVersion) -> + fv.field = field -> + fv.version = currentVersion -> + knownVersion = currentVersion -> + Fresh mod field knownVersion currentVersion -- ============================================================================ -- Synchronisation Points @@ -148,11 +167,21 @@ record Level12Proof where -- Key Theorems -- ============================================================================ -||| A writer always has fresh knowledge of what it wrote. +||| A writer always has fresh knowledge of what it wrote, given the +||| canonical `FieldVersion` at the post-write state. Post-A14 +||| (#102 closure), `Fresh` requires a `FieldVersion` pin — so this +||| lemma must thread that record through. The writer-identity pin +||| (`fv.lastWriter = writer`) is also taken for the obvious-but- +||| previously-implicit reason: a writer's freshness comes from being +||| the one named in `lastWriter`. export writerKnowsFresh : (writer : ModuleId) -> (field : String) -> (ver : Nat) -> + (fv : FieldVersion) -> + fv.field = field -> + fv.version = ver -> + fv.lastWriter = writer -> Fresh writer field ver ver -writerKnowsFresh _ _ _ = MkFresh Refl +writerKnowsFresh _ _ _ fv fp vp _ = MkFresh fv fp vp Refl ||| Staleness is decidable: given two versions, knowledge is either fresh, ||| stale-forward (known < current), or stale-backward (current < known). @@ -170,10 +199,16 @@ freshOrStale (S k) (S c) = case freshOrStale k c of Right (Right gt) => Right (Right (LTESucc gt)) ||| Sync restores freshness. +||| +||| Post-A14: both branches must supply the `FieldVersion` pin. The +||| `ExplicitSync` branch returns its embedded `Fresh` witness +||| directly (the pin is already inside). The `WriteSync` branch +||| rebuilds a `Fresh` using the same `FieldVersion` that the write +||| committed to. export syncRestoresFresh : Sync mod field old new -> Fresh mod field new new -syncRestoresFresh (ExplicitSync fresh) = MkFresh Refl -syncRestoresFresh (WriteSync _ _ _ _) = MkFresh Refl +syncRestoresFresh (ExplicitSync fresh) = fresh +syncRestoresFresh (WriteSync fv fp vp _) = MkFresh fv fp vp Refl -- ============================================================================ -- Concurrent-write propagation theorems (A10, 2026-05-26 — closes @@ -185,7 +220,7 @@ syncRestoresFresh (WriteSync _ _ _ _) = MkFresh Refl ||| downstream proofs about reads. export freshImpliesEqual : Fresh mod field known current -> known = current -freshImpliesEqual (MkFresh eq) = eq +freshImpliesEqual (MkFresh _ _ _ eq) = eq ||| Stale witnesses a strict ordering on versions. Dual projector to ||| `freshImpliesEqual`. @@ -206,7 +241,7 @@ ltIrreflexive (LTESucc rest) = ltIrreflexive rest ||| handles the case where `current` actually advances. export freshNotStale : Fresh mod field v v' -> Stale mod field v v' -> Void -freshNotStale (MkFresh Refl) (MkStale lt) = ltIrreflexive lt +freshNotStale (MkFresh _ _ _ Refl) (MkStale lt) = ltIrreflexive lt ||| Concurrent-write staleness. If module `mod`'s view of `field` was ||| fresh at version `v` and the global current version subsequently @@ -216,7 +251,7 @@ freshNotStale (MkFresh Refl) (MkStale lt) = ltIrreflexive lt export concurrentWriteStales : Fresh mod field v v -> LT v v' -> Stale mod field v v' -concurrentWriteStales (MkFresh Refl) lt = MkStale lt +concurrentWriteStales (MkFresh _ _ _ Refl) lt = MkStale lt ||| Re-synchronisation after a concurrent write restores freshness. If ||| `mod`'s view is stale at `(v, cur)` and `mod` performs a Sync to @@ -308,17 +343,17 @@ observedHasProvenance Unknown = Nothing observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync) -- ---------------------------------------------------------------------------- --- Residual debt note (A11) +-- Residual debt note — A11 ➞ A14 closure (2026-06-02, #102) -- ---------------------------------------------------------------------------- -- --- The constructor-soundness tightening above plugs the most pointed --- leaks but does not fully close the chain. `Fresh` and `ExplicitSync` --- remain freely constructible: --- - `MkFresh Refl : Fresh mod field v v` for any (mod, field, v) --- - `ExplicitSync (writerKnowsFresh _ _ _) : Sync mod field _ v` --- so a caller can still synthesise a `Sync` (and hence an `Observed`) --- by chaining trivial constructions. Full tightening requires --- re-indexing `Fresh` on a `FieldVersion` value so that the --- `currentVersion` index is pinned to global ground truth — the next --- residual-debt item, tracked in --- `~/.claude/projects/-home-hyperpolymath/memory/project_typed_wasm_proof_debt_post_a10.md`. +-- A11 (2026-05-26) tightened only `WriteSync` to require a +-- `FieldVersion` pin. A14 (2026-06-02) closes the symmetric gap by +-- re-indexing `Fresh` on a `FieldVersion` value too — the +-- `currentVersion` index is now pinned to global ground truth, so +-- `MkFresh Refl` no longer types and a caller cannot mint freshness +-- ex nihilo. `ExplicitSync` does NOT need a separate `FieldVersion` +-- parameter: its `Fresh` argument now carries the pin, and +-- `ExplicitSync (writerKnowsFresh _ _ _ fv ..)` only types if the +-- caller has supplied a real `FieldVersion`. `Observed` likewise +-- inherits the pin via its `Sync` argument. No remaining +-- constructor in this file admits an unfounded version claim. diff --git a/src/abi/TypedWasm/ABI/Proofs.idr b/src/abi/TypedWasm/ABI/Proofs.idr index 0cd98b3..d76bcb8 100644 --- a/src/abi/TypedWasm/ABI/Proofs.idr +++ b/src/abi/TypedWasm/ABI/Proofs.idr @@ -1,5 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- Copyright (c) Jonathan D.A. Jewell -- -- Proofs.idr — Top-level proof combinators for typed-wasm ABI -- @@ -1445,11 +1445,15 @@ witnessToLegacy (MkWitnessCert ls hi mm) = -- the projections equals projection of the witness composition. ||| Compose two witness certificates by concatenation + minimum. +||| +||| Uses `Data.Nat.minimum` (not `Prelude.min`) to keep the highest-proven +||| component definitionally aligned with `composeCertificates` so the +||| `composeWitnessLegacyAgree` bridge lemma reduces to a single rewrite. public export composeWitness : WitnessCertificate -> WitnessCertificate -> WitnessCertificate composeWitness (MkWitnessCert ls1 h1 mm1) (MkWitnessCert ls2 h2 mm2) = - MkWitnessCert (ls1 ++ ls2) (min h1 h2) (mm1 ++ mm2) + MkWitnessCert (ls1 ++ ls2) (minimum h1 h2) (mm1 ++ mm2) -- ---------------------------------------------------------------------------- -- Bridge / composition compatibility lemma From aa7ee2576ccf738c70247d405163492d32335230 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 3 Jun 2026 00:14:01 +0100 Subject: [PATCH 3/4] =?UTF-8?q?proof(epistemic):=20A15=20=E2=80=94=20name?= =?UTF-8?q?=20the=20write=20=E2=9F=B6=20knows=20=E2=9F=B6=20fresh=20chain?= =?UTF-8?q?=20corollaries?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three named lemmas composing the post-A11+A14 pinned chain: * `syncImpliesKnowledge : Sync mod field old new -> Knowledge mod field new` — names the `Observed` step. * `writerKnowsPostWrite : (fv : FieldVersion) -> fv.field = field -> fv.lastWriter = writer -> Knowledge writer field fv.version` — a writer who commits to the canonical FieldVersion at the post-write state has Knowledge at that version; the writer-identity pin (`fv.lastWriter = writer`) flows through from WriteSync, so no caller can claim post-write knowledge for a module it does not own the write of. * `knowsImpliesFresh : Knows mod field ver -> Fresh mod field ver ver` — closes the chain: any non-trivial `Knows` witness yields a Fresh witness at the same version. The `Unknown` branch is dispatched via `absurd p` (the `MkKnows` precondition `ver > 0 = True` reduces to `False = True` when ver = 0). These are pure corollaries of A11 (WriteSync pin), A14 (Fresh pin), and the existing `syncRestoresFresh` / `Observed` machinery — no new constructors, no soundness change, just named composition for downstream callers. Residual-debt note extended to record A15. Verification: `idris2 --build src/abi/typed-wasm.ipkg` clean rebuild 22/22 modules, rc=0, zero errors. No `believe_me` / `assert_total` / `assert_smaller` / `postulate` / `sorry` introduced; `%default total` preserved. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/abi/TypedWasm/ABI/Epistemic.idr | 57 ++++++++++++++++++++++++++++- 1 file changed, 56 insertions(+), 1 deletion(-) diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index b789afa..49447ad 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -342,8 +342,58 @@ observedHasProvenance : observedHasProvenance Unknown = Nothing observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync) +-- ============================================================================ +-- Knowledge chain corollaries (A15, 2026-06-03 — composes A11 + A14) +-- ============================================================================ +-- +-- Now that `Sync` (via A11) and `Fresh` (via A14) are both pinned to +-- canonical `FieldVersion` records, the chain from a write to a +-- knower's freshness is fully witness-carrying. The three lemmas +-- below name the chain steps so callers can quote them directly +-- rather than re-deriving each composition at every use site. + +||| A `Sync` event immediately establishes `Knowledge` at the new +||| version. Trivial corollary of the `Observed` constructor, named +||| so the post-sync read protocol can be spelled out lemma-by-lemma. +public export +syncImpliesKnowledge : + {old : Nat} -> + Sync mod field old new -> Knowledge mod field new +syncImpliesKnowledge {old} sync = Observed {oldVer = old} sync + +||| A writer who supplies the canonical `FieldVersion` for its write +||| has `Knowledge` at the post-write version. Composes `WriteSync` +||| with `syncImpliesKnowledge`; the writer's identity flows in via +||| the `fv.lastWriter = writer` pin, so no caller can claim +||| post-write knowledge for a module it does not own the write of. +public export +writerKnowsPostWrite : + (fv : FieldVersion) -> + fv.field = field -> + fv.lastWriter = writer -> + Knowledge writer field fv.version +writerKnowsPostWrite fv fp wp = + Observed (WriteSync {oldVersion = 0} fv fp Refl wp) + +||| Any non-trivial `Knows` witness entails a `Fresh` witness at the +||| same version. Closes the chain `Sync ⟶ Knowledge ⟶ Knows ⟶ +||| Fresh`: a module that knows a field's version is, by construction, +||| fresh at that version (because the `Sync` that established the +||| knowledge restored freshness; A11+A14 pinning guarantees the +||| `FieldVersion` threads through end-to-end). +||| +||| The `Unknown` branch is impossible by the `MkKnows` precondition +||| `ver > 0 = True`: `Unknown` inhabits only `Knowledge mod field 0`, +||| at which point `0 > 0` reduces to `False`, contradicting the +||| `= True` proof. +public export +knowsImpliesFresh : + Knows mod field ver -> Fresh mod field ver ver +knowsImpliesFresh (MkKnows (Observed sync) _) = syncRestoresFresh sync +knowsImpliesFresh (MkKnows Unknown p) = absurd p + -- ---------------------------------------------------------------------------- --- Residual debt note — A11 ➞ A14 closure (2026-06-02, #102) +-- Residual debt note — A11 ➞ A14 ➞ A15 closure (2026-06-03) -- ---------------------------------------------------------------------------- -- -- A11 (2026-05-26) tightened only `WriteSync` to require a @@ -357,3 +407,8 @@ observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync) -- caller has supplied a real `FieldVersion`. `Observed` likewise -- inherits the pin via its `Sync` argument. No remaining -- constructor in this file admits an unfounded version claim. +-- +-- A15 (2026-06-03) names the chain corollaries `syncImpliesKnowledge`, +-- `writerKnowsPostWrite`, and `knowsImpliesFresh`, so the +-- write ⟶ sync ⟶ knowledge ⟶ knows ⟶ fresh chain can be quoted +-- step-by-step rather than re-derived at each use site. From cbe32d47b0ea177fae96c5d110eac7380fa75da5 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 3 Jun 2026 00:41:56 +0100 Subject: [PATCH 4/4] =?UTF-8?q?proof(epistemic):=20A16=20=E2=80=94=20publi?= =?UTF-8?q?c=20FieldVersion=20pin=20projectors?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `freshHasPin`, `syncHasPin`, `level12HasPin` expose the canonical `FieldVersion` record that A11+A14 embedded in `Sync`, `Fresh`, and `Level12Proof` — both equalities (`fv.field`, `fv.version`) are surfaced alongside the record so downstream `rewrite` proofs can quote them directly without re-deriving the case split. `syncHasPin` is total (no `Maybe`): post-A14 both `Sync` branches carry a pin — `ExplicitSync` inherits via embedded `Fresh`, `WriteSync` supplies it directly. Idris2 0.8.0 `--build` rc=0, 22/22 modules to TTC, zero errors, zero new dangerous patterns, `%default total` preserved. Refs #102 (A14 closure stack). Co-Authored-By: Claude Opus 4.7 (1M context) --- src/abi/TypedWasm/ABI/Epistemic.idr | 55 ++++++++++++++++++++++++++++- 1 file changed, 54 insertions(+), 1 deletion(-) diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr index 49447ad..25f94c3 100644 --- a/src/abi/TypedWasm/ABI/Epistemic.idr +++ b/src/abi/TypedWasm/ABI/Epistemic.idr @@ -392,8 +392,55 @@ knowsImpliesFresh : knowsImpliesFresh (MkKnows (Observed sync) _) = syncRestoresFresh sync knowsImpliesFresh (MkKnows Unknown p) = absurd p +-- ============================================================================ +-- FieldVersion pin projectors (A16, 2026-06-03 — surfaces the embedded +-- canonical FieldVersion record from any pin-bearing witness) +-- ============================================================================ +-- +-- A11 + A14 made the dependent indices on `Sync` and `Fresh` line up +-- with a real `FieldVersion` value, but the record itself was only +-- reachable by case-splitting on the data constructor inside this +-- module. The three projectors below expose the pin publicly so +-- downstream code (e.g. read-protocol clients that need to ask "what +-- is the canonical record for my read?") can quote a single named +-- lemma instead of duplicating the case split. + +||| Project the canonical `FieldVersion` out of a `Fresh` witness. +||| Both equalities (`fv.field = field`, `fv.version = currentVersion`) +||| are returned alongside the record itself — the caller can rewrite +||| with them directly when substituting versions or fields downstream. +public export +freshHasPin : + Fresh mod field k c -> + (fv : FieldVersion ** (fv.field = field, fv.version = c)) +freshHasPin (MkFresh fv fp vp _) = (fv ** (fp, vp)) + +||| Project the canonical `FieldVersion` out of a `Sync` witness. +||| Both branches carry a pin: the `ExplicitSync` branch inherits it +||| via its embedded `Fresh` (re-projected here through `freshHasPin`), +||| while the `WriteSync` branch supplies it directly. Total — every +||| `Sync` carries a pin post-A14, so no `Maybe` wrapping is needed. +public export +syncHasPin : + Sync mod field old new -> + (fv : FieldVersion ** (fv.field = field, fv.version = new)) +syncHasPin (ExplicitSync fresh) = freshHasPin fresh +syncHasPin (WriteSync fv fp vp _) = (fv ** (fp, vp)) + +||| Project the canonical `FieldVersion` out of a `Level12Proof`. +||| Composes `epistemicFreshness` (which extracts the proof's `Fresh` +||| field) with `freshHasPin`. Returned indices are tied to the +||| record's own fields (`p.field`, `p.currentVersion`) so callers +||| holding only a `Level12Proof` can immediately quote the +||| ground-truth record without case-splitting the proof. +public export +level12HasPin : + (p : Level12Proof) -> + (fv : FieldVersion ** (fv.field = p.field, fv.version = p.currentVersion)) +level12HasPin p = freshHasPin (epistemicFreshness p) + -- ---------------------------------------------------------------------------- --- Residual debt note — A11 ➞ A14 ➞ A15 closure (2026-06-03) +-- Residual debt note — A11 ➞ A14 ➞ A15 ➞ A16 closure (2026-06-03) -- ---------------------------------------------------------------------------- -- -- A11 (2026-05-26) tightened only `WriteSync` to require a @@ -412,3 +459,9 @@ knowsImpliesFresh (MkKnows Unknown p) = absurd p -- `writerKnowsPostWrite`, and `knowsImpliesFresh`, so the -- write ⟶ sync ⟶ knowledge ⟶ knows ⟶ fresh chain can be quoted -- step-by-step rather than re-derived at each use site. +-- +-- A16 (2026-06-03) publishes pin projectors `freshHasPin`, +-- `syncHasPin`, and `level12HasPin` — every pin-bearing witness +-- now has a named extractor for the canonical `FieldVersion` it +-- carries, with both field/version equalities surfaced alongside +-- so downstream `rewrite` proofs can quote them directly.