diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 9fe6340..2c2d136 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,6 +7,19 @@ Changelog]. === [Unreleased] +==== Added (2026-11-09) + +* _squeakwell / VeriSimDB recovery ladder._ `+EchoPartialSection.agda+` +(partial sections of a modality bundle; information order; resolve-parametric +merge with the pointwise R1–R3 twins of verisimdb `+Octad.v+`; guarded fill as +left-biased merge, inflationary and provably not monotone; restriction to an +observed mask and its Echo fibre) and `+EchoFibreIntersection.agda+` (binary +narrowing as the fibre of a pairing, witness-preserving `+Fin n+` steps, +`+narrow-shrinks+` on `+FiberSize-fin+`). `+EchoTruncation.agda+`, until now +compiled only through its corollaries, is wired into `+All.agda+` and pinned. +Rocq recheck: verisimdb `+formal/Recovery.v+`; Lean side: tropical-types +`+Resource/HubCeiling.lean+`. + ==== Changed (2026-11-06) * Recorded the owner's prospective licence policy: CC-BY-SA-4.0 for new diff --git a/docs/bridges/cross-repo-bridge-status.adoc b/docs/bridges/cross-repo-bridge-status.adoc index a0bdcf0..b3cc4d4 100644 --- a/docs/bridges/cross-repo-bridge-status.adoc +++ b/docs/bridges/cross-repo-bridge-status.adoc @@ -227,6 +227,25 @@ path; citation-level — echo-types proves the general aggregation principle (and its macro instance), oikos’s alib will _consume_ it. The alib library itself is not yet built (design-note stage; Route A vs B pending owner decision). +|squeakwell / VeriSimDB recovery ladder +|`+proofs/agda/EchoPartialSection.agda+`, `+EchoFibreIntersection.agda+`, +`+EchoTruncation.agda+` (wired 2026-11-09) +|verisimdb `+formal/Recovery.v+` (Rocq recheck of R2/R3/R4/R9/R10 over +`+Octad.v+`), tropical-types `+Resource/HubCeiling.lean+` (reach grades, +hub ceilings, weighted residue measure), squeakwell `+docs/ROUTE-PLAN.adoc+` +|*Theory landed, pointwise.* Partial sections with the resolve-parametric +merge (the join-semilattice-of-partial-sections abstraction verisimdb’s +CROSS-REPO-MAP flagged), guarded fill (inflationary, not monotone), the +restriction fibre (fragment observation fidelity), binary and `+Fin n+` +narrowing with `+narrow-shrinks+` on the honest count. Checked here with +Agda 2.7.0.1 and the pinned stdlib / absolute-zero; Recovery.v with Coq +8.18.0; HubCeiling with Lean 4.35.0. +|Correspondence is a refinement, not same-statement: Agda proves the merge +laws pointwise, Rocq as function equalities under +`+functional_extensionality_dep+`. Termination (nine rounds) is Rocq-only +(needs the finite octad). The Creusot export/queue postconditions (R11–R13 +engineering half) and the Idris2 wire contracts (R1, R15, R16) are not +started; see squeakwell `+PROOF-STATUS.adoc+`. |=== === Immediate next actions @@ -347,6 +366,16 @@ to paper over this in the relational model. === Revision history +* 2026-11-09: *squeakwell / VeriSimDB recovery ladder.* Added +`+EchoPartialSection.agda+` (partial sections, information order, +resolve-parametric merge = pointwise R1–R3 twins of verisimdb `+Octad.v+`, +guarded fill inflationary-not-monotone, restriction fibre) and +`+EchoFibreIntersection.agda+` (binary / `+Fin n+` narrowing, +`+narrow-shrinks+`); wired the orphan `+EchoTruncation.agda+` into +`+All.agda+`. New Tracks row. Rocq recheck lands as verisimdb +`+formal/Recovery.v+`; Lean side as tropical-types +`+Resource/HubCeiling.lean+`. `+--safe --without-K --cubical-compatible+`, +zero postulates, funext-free. * 2026-06-18: *EchoAggregation general/macro split.* Generalised `+EchoAggregation.agda+` from the macro-economics-specific module into the general monoid-aggregation form requested by issue #175 (`+Monoid+` diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index e6b825d..3f80a52 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -512,6 +512,46 @@ Connect echo types with MAA's reversibility proofs * Docs: `roadmap.adoc` §"Deferred research track", `docs/bridges/EchoJanusBridge.adoc`. +=== Database recovery — squeakwell / VeriSimDB bridge `[REAL]` + +The Agda source of truth for the repaired recovery invariants of +https://github.com/hyperpolymath/squeakwell[squeakwell] (database +recovery through cross-modal constraint propagation on VeriSimDB; route +plan rungs R3, R8, R9, R12, R13). Landed 2026-11-09, `--safe --without-K +--cubical-compatible`, zero postulates, pointwise (funext-free): + +* *Partial sections* — `EchoPartialSection.agda`: a VeriSimDB octad is a + partial section `(m : M) → Maybe (V m)` of a modality bundle. Information + order; `merge resolve` inherits exactly the algebra of `resolve` + (`merge-comm` / `merge-assoc` / `merge-idem`, the pointwise twins of + verisimdb `Octad.v` R1–R3 — implications, not CRDT laws); guarded fill + is the left-biased merge against an oracle proposal, never overwrites + (`fill-guarded`), is inflationary (`fill-inflationary`) and is NOT + monotone (`fill-not-monotone`, two-modality counter-model); restriction + to an observed mask and its Echo fibre (`restrict-fibre-agree`, + `restrict-blind`) — the fragment-granularity observation-fidelity shape. +* *Multi-witness narrowing* — `EchoFibreIntersection.agda`: the fibre of a + pairing is the intersection of fibres over one witness + (`fibre-intersection-iso`); forgetting or adding a constraint keeps the + witness; `narrow-shrinks`: the `EchoFiberCount` count never grows when + an observation is added. +* *Truncation wired* — `EchoTruncation.agda` is now in `All.agda` and + pinned (`echo-not-prop`); with `FiberSize-fin≡0⇒no-echo` / + `no-echo⇒FiberSize-fin≡0` it is the review-queue completeness kernel. + +Not claimed: inhabitation of the narrowed fibre; covering masks ⇒ +subsingleton (needs extensionality over opaque identifiers; dropped); +termination of the recovery round (finite index set and a conflict test — +proved in Rocq as `iter_9_fixpoint` in verisimdb `formal/Recovery.v`, not +restated over an arbitrary `M`). Lean side (reach grades, hub ceilings, +weighted residue measure): tropical-types `Resource/HubCeiling.lean`. +Ledger of grades per rung: squeakwell `PROOF-STATUS.adoc`. + +* Proofs: `proofs/agda/EchoPartialSection.agda`, + `proofs/agda/EchoFibreIntersection.agda`, `proofs/agda/EchoTruncation.agda`. +* Cross-repo: verisimdb `formal/Recovery.v` + `formal/CROSS-REPO-MAP.adoc`; + tropical-types `Resource/HubCeiling.lean`; squeakwell `docs/ROUTE-PLAN.adoc`. + === Shannon / information theory `[REAL*]` Partial. The *discrete non-distinguishing* form lands as `EchoEntropy.agda` — the fibre-count shadow (uniform-prior Shannon diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index 5b357cd..6e1631d 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -226,6 +226,18 @@ kernel** — the boundary is real and lives outside this core. flat `Echo*.agda` glob that Check B lints; recorded here for discoverability. Not kernel (the kernel remains exactly `Echo`). +| *Derived — recovery ladder (2026-11-09)* +| `EchoPartialSection` (Tier 1), `EchoFibreIntersection` (Tier 2) +| squeakwell / VeriSimDB recovery bridge. `EchoPartialSection` imports only + `Echo` and stdlib: partial sections of a modality bundle, the information + order, the resolve-parametric merge (pointwise R1–R3 twins of verisimdb + `Octad.v`), guarded fill as left-biased merge (inflationary, not + monotone) and the restriction fibre. `EchoFibreIntersection` imports + `Echo` and `EchoFiberCount`: binary narrowing as the fibre of a pairing, + witness-preserving constraint steps, and `narrow-shrinks` on the honest + count. Both funext-free; Rocq recheck in verisimdb `formal/Recovery.v`. + `EchoTruncation` (Tier 1, already classified) is now wired into `All.agda`. + | *Derived — Tier 1 additions (2026-11-06)* | `EchoSourcePreserving`, `EchoDependentPushforward` | Each imports only `Echo` and stdlib. The former proves the source-preserving diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 79ffb39..70d741d 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -50,6 +50,12 @@ open import EchoSearchInstance open import EchoSearchExample open import EchoAccess open import EchoFiberCount +-- squeakwell recovery ladder (2026-11-09): wires the once-orphan truncation +-- lemma, multi-witness narrowing (R8) and partial sections / guarded fill / +-- restriction fibre (R3, R9, R12). Rocq recheck: verisimdb formal/Recovery.v. +open import EchoTruncation +open import EchoFibreIntersection +open import EchoPartialSection open import EchoEpistemicResidue open import EchoRelational open import EchoCategorical diff --git a/proofs/agda/EchoFibreIntersection.agda b/proofs/agda/EchoFibreIntersection.agda new file mode 100644 index 0000000..8a6a13b --- /dev/null +++ b/proofs/agda/EchoFibreIntersection.agda @@ -0,0 +1,230 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoFibreIntersection: multi-witness narrowing (squeakwell rung R8). +-- +-- A recovery engine that has observed several modalities of one entity +-- asks for the witnesses satisfying ALL the observations at once. In +-- Echo terms that is the intersection of fibres over one shared +-- witness: `Σ A (λ x → f x ≡ y × g x ≡ z)`. This module pins the three +-- facts hyperpolymath/squeakwell's proof ladder (docs/ROUTE-PLAN.adoc, +-- rung R8) needs about that intersection: +-- +-- * Binary narrowing is a fibre. Intersecting the fibres of `f` at +-- `y` and of `g` at `z` IS the fibre of the pairing `< f , g >` at +-- `(y , z)`: `fibre-intersection-iso`, a K-free `_↔_` with `refl` +-- round-trips (no funext — the equations are on pairs, not on +-- functions). +-- * Narrowing never changes the witness. Forgetting either +-- constraint is witness-preserving (`forget-left-witness`, +-- `forget-right-witness`), and adding one more constraint to a +-- family of `n` constraints is again witness-preserving in both +-- directions (`narrow-fin-step-to`, `narrow-fin-step-from`). The +-- `Fin n` family form is stated with pointwise equations, so it +-- needs no funext; it is NOT packaged as a `_↔_` because the +-- round-trip on the function side would. +-- * Narrowing shrinks the candidate fibre. On a finite domain with +-- decidable equality, the honest count of `EchoFiberCount` can +-- only go down when a constraint is added: `narrow-shrinks` +-- (`FiberSize-fin < f , g > (y , z) ≤ FiberSize-fin f y`). This is +-- the quantitative statement behind squeakwell's review queue: +-- every extra observed modality narrows the candidates. +-- +-- Honest scope. The survey's proposed "covering masks ⇒ subsingleton +-- fibre" is NOT here: over an opaque value type two full sections that +-- agree on every modality need not be equal without extensionality, and +-- squeakwell's identifiers are opaque. The route plan dropped it; so +-- does this module. Nothing here claims the intersection is inhabited: +-- observations can be jointly unsatisfiable, and the count can be 0. +-- +-- Headlines (pinned in Smoke.agda): +-- +-- * fibre-intersection-iso -- Echo < f , g > (y , z) ↔ Narrow f g y z +-- * forget-left-witness -- forgetting a constraint keeps the witness +-- * forget-right-witness +-- * narrow-fin-step-to -- Fin (suc n) family = one more binary step +-- * narrow-fin-step-from +-- * narrow-shrinks -- FiberSize-fin of the pairing ≤ FiberSize-fin of f + +module EchoFibreIntersection where + +open import Function.Base using (_∘_) +open import Level using (Level; _⊔_) +open import Data.Empty using (⊥; ⊥-elim) +import Data.Nat.Base as ℕ +open ℕ using (ℕ; _≤_; z≤n; s≤s) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂; <_,_>) +open import Function.Bundles using (_↔_; mk↔ₛ′) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) + +open import Echo using (Echo) +open import EchoFiberCount using (FiberSize-fin) + +private + variable + ℓa ℓb ℓc : Level + A : Set ℓa + B : Set ℓb + C : Set ℓc + +---------------------------------------------------------------------- +-- Binary narrowing: two constraints on one witness. +---------------------------------------------------------------------- + +-- The witnesses `x` with `f x ≡ y` AND `g x ≡ z`: the intersection of +-- the two fibres over a shared witness. +Narrow : (f : A → B) (g : A → C) → B → C → Set _ +Narrow {A = A} f g y z = Σ A (λ x → (f x ≡ y) × (g x ≡ z)) + +pair-fibre→narrow : + {f : A → B} {g : A → C} {y : B} {z : C} → + Echo < f , g > (y , z) → Narrow f g y z +pair-fibre→narrow (x , p) = x , cong proj₁ p , cong proj₂ p + +narrow→pair-fibre : + {f : A → B} {g : A → C} {y : B} {z : C} → + Narrow f g y z → Echo < f , g > (y , z) +narrow→pair-fibre (x , p , q) = x , cong₂ _,_ p q + +-- Round trips. Both close by matching the equation on `refl`; the +-- indices `y`, `z` are variables, so this is `--without-K`-safe. +narrow-to-from : + {f : A → B} {g : A → C} {y : B} {z : C} → + (e : Echo < f , g > (y , z)) → + narrow→pair-fibre {f = f} {g = g} (pair-fibre→narrow e) ≡ e +narrow-to-from (x , refl) = refl + +narrow-from-to : + {f : A → B} {g : A → C} {y : B} {z : C} → + (w : Narrow f g y z) → + pair-fibre→narrow {f = f} {g = g} (narrow→pair-fibre w) ≡ w +narrow-from-to (x , refl , refl) = refl + +-- Headline 1: binary narrowing IS the fibre of the pairing. +fibre-intersection-iso : + (f : A → B) (g : A → C) (y : B) (z : C) → + Echo < f , g > (y , z) ↔ Narrow f g y z +fibre-intersection-iso f g y z = + mk↔ₛ′ pair-fibre→narrow narrow→pair-fibre + (narrow-from-to {f = f} {g = g}) (narrow-to-from {f = f} {g = g}) + +---------------------------------------------------------------------- +-- Forgetting a constraint keeps the witness. +---------------------------------------------------------------------- + +forget-left : + {f : A → B} {g : A → C} {y : B} {z : C} → Narrow f g y z → Echo g z +forget-left (x , _ , q) = x , q + +forget-right : + {f : A → B} {g : A → C} {y : B} {z : C} → Narrow f g y z → Echo f y +forget-right (x , p , _) = x , p + +-- Headline 2: narrowing is a refinement of the SAME candidate, never a +-- different one. Both are definitional. +forget-left-witness : + {f : A → B} {g : A → C} {y : B} {z : C} (w : Narrow f g y z) → + proj₁ (forget-left {f = f} w) ≡ proj₁ w +forget-left-witness _ = refl + +forget-right-witness : + {f : A → B} {g : A → C} {y : B} {z : C} (w : Narrow f g y z) → + proj₁ (forget-right {g = g} w) ≡ proj₁ w +forget-right-witness _ = refl + +---------------------------------------------------------------------- +-- Families of constraints indexed by `Fin n`. +---------------------------------------------------------------------- + +-- `n` observations `fs i x ≡ ys i` on one witness `x`, stated pointwise +-- (no function equality, hence no funext). +NarrowFin : ∀ {n} (fs : Fin n → A → B) (ys : Fin n → B) → Set _ +NarrowFin {A = A} fs ys = Σ A (λ x → ∀ i → fs i x ≡ ys i) + +-- Headline 3: a family of `suc n` constraints is one binary narrowing +-- step on top of a family of `n`, in both directions, and the witness +-- is untouched (both maps are `refl` on `proj₁`). +narrow-fin-step-to : + ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) → + NarrowFin fs ys → + Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i))) +narrow-fin-step-to fs ys (x , h) = x , h zero , (λ i → h (suc i)) + +narrow-fin-step-from : + ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) → + Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i))) → + NarrowFin fs ys +narrow-fin-step-from fs ys (x , p , h) = x , step + where + step : ∀ i → fs i x ≡ ys i + step zero = p + step (suc i) = h i + +narrow-fin-step-to-witness : + ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) + (w : NarrowFin fs ys) → + proj₁ (narrow-fin-step-to fs ys w) ≡ proj₁ w +narrow-fin-step-to-witness _ _ _ = refl + +narrow-fin-step-from-witness : + ∀ {n} (fs : Fin (ℕ.suc n) → A → B) (ys : Fin (ℕ.suc n) → B) + (w : Σ A (λ x → (fs zero x ≡ ys zero) × (∀ i → fs (suc i) x ≡ ys (suc i)))) → + proj₁ (narrow-fin-step-from fs ys w) ≡ proj₁ w +narrow-fin-step-from-witness _ _ _ = refl + +---------------------------------------------------------------------- +-- Narrowing shrinks the honest fibre count. +---------------------------------------------------------------------- + +-- Decidable equality on pairs from decidable equality on the components. +dec-× : + ((b₁ b₂ : B) → Dec (b₁ ≡ b₂)) → + ((c₁ c₂ : C) → Dec (c₁ ≡ c₂)) → + (p q : B × C) → Dec (p ≡ q) +dec-× _≟B_ _≟C_ (b , c) (b′ , c′) with b ≟B b′ | c ≟C c′ +... | yes refl | yes refl = yes refl +... | yes _ | no ¬q = no (λ e → ¬q (cong proj₂ e)) +... | no ¬p | yes _ = no (λ e → ¬p (cong proj₁ e)) +... | no ¬p | no _ = no (λ e → ¬p (cong proj₁ e)) + +private + ≤-step : ∀ {m n} → m ≤ n → m ≤ ℕ.suc n + ≤-step z≤n = z≤n + ≤-step (s≤s p) = s≤s (≤-step p) + +-- Headline 4: adding an observation never enlarges the enumerated +-- candidate fibre. Walks the `FiberSize-fin` recursion on both sides in +-- lock-step: a hit for the pair is a hit for `f`; a hit for `f` alone +-- is a candidate the extra observation has ruled out. +narrow-shrinks : + ∀ {n} (f : Fin n → B) (g : Fin n → C) (y : B) (z : C) + (_≟B_ : (b₁ b₂ : B) → Dec (b₁ ≡ b₂)) + (_≟C_ : (c₁ c₂ : C) → Dec (c₁ ≡ c₂)) → + FiberSize-fin < f , g > (y , z) (dec-× _≟B_ _≟C_) ≤ FiberSize-fin f y _≟B_ +narrow-shrinks {n = ℕ.zero} f g y z _≟B_ _≟C_ = z≤n +narrow-shrinks {n = ℕ.suc m} f g y z _≟B_ _≟C_ + with f zero ≟B y | dec-× _≟B_ _≟C_ (< f , g > zero) (y , z) +... | yes _ | yes _ = s≤s (narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_) +... | yes _ | no _ = ≤-step (narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_) +... | no ¬p | yes q = ⊥-elim (¬p (cong proj₁ q)) +... | no _ | no _ = narrow-shrinks (f ∘ suc) (g ∘ suc) y z _≟B_ _≟C_ + +---------------------------------------------------------------------- +-- Companion remark. +-- +-- What is deliberately NOT claimed: +-- +-- * Inhabitation. `Narrow f g y z` may be empty; joint observations +-- can be inconsistent. squeakwell reports that as an empty +-- candidate fibre, routed to review (rung R13), not as a theorem. +-- * Covering ⇒ subsingleton. The survey's "if the observed masks +-- cover every modality the fibre is a subsingleton" needs equality +-- of full sections from pointwise equality, i.e. extensionality, and +-- opaque identifiers. Dropped in the route plan; not here. +-- * A `_↔_` for the `Fin n` family step. The pointwise maps exist and +-- preserve the witness; the function-side round trip would need +-- funext and is left out rather than taken as a hypothesis. +---------------------------------------------------------------------- diff --git a/proofs/agda/EchoPartialSection.agda b/proofs/agda/EchoPartialSection.agda new file mode 100644 index 0000000..48a784e --- /dev/null +++ b/proofs/agda/EchoPartialSection.agda @@ -0,0 +1,260 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoPartialSection: partial sections of a modality bundle, their +-- information order, resolve-parametric merge, guarded fill, and the +-- restriction fibre. The Agda source of truth for the recovery +-- invariants of hyperpolymath/squeakwell (docs/ROUTE-PLAN.adoc rungs +-- R3, R9, R12), rechecked in Rocq as verisimdb `formal/Recovery.v`. +-- +-- The object. A VeriSimDB octad is a partial section of a bundle +-- `V : M → Set` over a finite index set `M` of modalities: each +-- modality carries a value or bot. Here that is +-- `PartialSection M V = (m : M) → Maybe (V m)`, with no assumption on +-- `M` (so the eight-slot octad is one instance). This is the +-- "join-semilattice of partial sections" abstraction that +-- verisimdb/formal/CROSS-REPO-MAP.adoc flagged as the missing +-- echo-types companion to Octad.v's R1–R3. +-- +-- Everything is stated POINTWISE (equalities at each `m`), never as an +-- equality of functions, so the module is funext-free. Octad.v proves +-- the same laws as function equalities using Coq's +-- functional_extensionality; the pointwise forms here are the ones +-- that survive `--safe --without-K` without that axiom. +-- +-- What is proved: +-- +-- * Information order `_⊑_` (present-in-s ⇒ present-and-equal-in-t): +-- reflexive, transitive. +-- * `merge resolve` — the per-point merge kernel of Octad.v +-- (`mcombine`), parametric in the conflict resolver — inherits +-- exactly the algebra of `resolve`: commutative / associative / +-- idempotent WHEN `resolve` is (`merge-comm`, `merge-assoc`, +-- `merge-idem`). These are the R1–R3 twins; they are implications, +-- not unconditional CRDT laws. +-- * Guarded fill is the LEFT-BIASED merge against an oracle's +-- proposal (`fill`): it never overwrites a present value +-- (`fill-guarded`), is inflationary on `_⊑_` (`fill-inflationary`), +-- and is NOT monotone on `_⊑_` (`fill-not-monotone`, a two-modality +-- counter-model). Rung R3. +-- * Restriction to an observed mask `T` and its Echo fibre: an echo +-- of `restrict T` at an observation agrees with the observation on +-- every observed modality (`restrict-fibre-agree`) and is blind off +-- the mask (`restrict-blind`). This is the fragment-granularity +-- observation-fidelity shape of rung R12: `e : Echo (restrict T) obs` +-- says exactly "the candidate reproduces what was observed, on T". +-- +-- Headlines (pinned in Smoke.agda): +-- +-- * ⊑-refl, ⊑-trans +-- * merge-comm, merge-assoc, merge-idem +-- * fill-guarded, fill-inflationary, fill-not-monotone +-- * restrict-fibre-agree, restrict-blind, restrict-echo + +module EchoPartialSection where + +open import Level using (Level; _⊔_) +open import Data.Bool.Base using (Bool; true; false; if_then_else_) +open import Data.Maybe.Base using (Maybe; just; nothing) +open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂) +open import Data.Empty using (⊥) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) + +open import Echo using (Echo; echo-intro) + +private + variable + ℓm ℓv : Level + +---------------------------------------------------------------------- +-- Partial sections. +---------------------------------------------------------------------- + +-- A partial section of the bundle `V` over `M`: a value or bot at each +-- index. An octad is the instance `M = the eight modalities`. +PartialSection : (M : Set ℓm) (V : M → Set ℓv) → Set (ℓm ⊔ ℓv) +PartialSection M V = (m : M) → Maybe (V m) + +module _ {M : Set ℓm} {V : M → Set ℓv} where + + ---------------------------------------------------------------------- + -- Information order. + ---------------------------------------------------------------------- + + -- `s ⊑ t`: every value present in `s` is present, unchanged, in `t`. + _⊑_ : PartialSection M V → PartialSection M V → Set (ℓm ⊔ ℓv) + s ⊑ t = ∀ m (v : V m) → s m ≡ just v → t m ≡ just v + + ⊑-refl : ∀ {s} → s ⊑ s + ⊑-refl m v p = p + + ⊑-trans : ∀ {s t u} → s ⊑ t → t ⊑ u → s ⊑ u + ⊑-trans p q m v h = q m v (p m v h) + + ---------------------------------------------------------------------- + -- Resolve-parametric merge (Octad.v `mcombine` / `merge`). + ---------------------------------------------------------------------- + + Resolver : Set (ℓm ⊔ ℓv) + Resolver = ∀ {m} → V m → V m → V m + + mcombine : Resolver → ∀ {m} → Maybe (V m) → Maybe (V m) → Maybe (V m) + mcombine resolve nothing nothing = nothing + mcombine resolve (just a) nothing = just a + mcombine resolve nothing (just b) = just b + mcombine resolve (just a) (just b) = just (resolve a b) + + merge : Resolver → PartialSection M V → PartialSection M V → PartialSection M V + merge resolve s t m = mcombine resolve (s m) (t m) + + -- R1 twin: merge is commutative when resolve is. + merge-comm : + (resolve : Resolver) → + (∀ {m} (a b : V m) → resolve a b ≡ resolve b a) → + ∀ s t m → merge resolve s t m ≡ merge resolve t s m + merge-comm resolve rc s t m with s m | t m + ... | nothing | nothing = refl + ... | just a | nothing = refl + ... | nothing | just b = refl + ... | just a | just b = cong just (rc a b) + + -- R2 twin: merge is associative when resolve is. + merge-assoc : + (resolve : Resolver) → + (∀ {m} (a b c : V m) → resolve a (resolve b c) ≡ resolve (resolve a b) c) → + ∀ s t u m → + merge resolve (merge resolve s t) u m ≡ merge resolve s (merge resolve t u) m + merge-assoc resolve ra s t u m with s m | t m | u m + ... | nothing | nothing | nothing = refl + ... | nothing | nothing | just c = refl + ... | nothing | just b | nothing = refl + ... | nothing | just b | just c = refl + ... | just a | nothing | nothing = refl + ... | just a | nothing | just c = refl + ... | just a | just b | nothing = refl + ... | just a | just b | just c = cong just (sym (ra a b c)) + + -- R3 twin: merge is idempotent when resolve is. + merge-idem : + (resolve : Resolver) → + (∀ {m} (a : V m) → resolve a a ≡ a) → + ∀ s m → merge resolve s s m ≡ s m + merge-idem resolve ri s m with s m + ... | nothing = refl + ... | just a = cong just (ri a) + + ---------------------------------------------------------------------- + -- Guarded fill: left-biased merge against an oracle's proposal. + ---------------------------------------------------------------------- + + keep-left : Resolver + keep-left a _ = a + + -- The oracle proposes a (partial) section from the current one; fill + -- takes a proposal only where the current section is bot. + fill : (propose : PartialSection M V → PartialSection M V) → + PartialSection M V → PartialSection M V + fill propose s = merge keep-left s (propose s) + + -- A present value is never overwritten. + fill-guarded : + ∀ propose s m (v : V m) → s m ≡ just v → fill propose s m ≡ just v + fill-guarded propose s m v p with s m | propose s m + fill-guarded propose s m v refl | just .v | nothing = refl + fill-guarded propose s m v refl | just .v | just _ = refl + + -- Guarded fill is inflationary on the information order. + fill-inflationary : ∀ propose s → s ⊑ fill propose s + fill-inflationary propose s m v p = fill-guarded propose s m v p + + ---------------------------------------------------------------------- + -- Restriction to an observed mask, and its Echo fibre. + ---------------------------------------------------------------------- + + -- Keep the observed modalities, forget the rest (Octad.v `project`). + restrict : (T : M → Bool) → PartialSection M V → PartialSection M V + restrict T s m = if T m then s m else nothing + + -- Every section is a candidate for its own restriction. + restrict-echo : (T : M → Bool) (s : PartialSection M V) → + Echo (restrict T) (restrict T s) + restrict-echo T s = echo-intro (restrict T) s + + restrict-on : (T : M → Bool) (s : PartialSection M V) (m : M) → + T m ≡ true → restrict T s m ≡ s m + restrict-on T s m Tm rewrite Tm = refl + + -- R12 shape: a candidate in the fibre of `restrict T` at an observation + -- `o` reproduces `o` on every observed modality. + restrict-fibre-agree : + (T : M → Bool) {o : PartialSection M V} (e : Echo (restrict T) o) → + ∀ m → T m ≡ true → proj₁ e m ≡ o m + restrict-fibre-agree T (s , p) m Tm = + trans (sym (restrict-on T s m Tm)) (cong (λ f → f m) p) + + -- Off the mask, restriction forgets everything: any two sections + -- restrict to the same (bot) value there. + restrict-blind : + (T : M → Bool) (s t : PartialSection M V) (m : M) → + T m ≡ false → restrict T s m ≡ restrict T t m + restrict-blind T s t m Tm rewrite Tm = refl + +---------------------------------------------------------------------- +-- Counter-model: guarded fill is NOT monotone on the information order. +-- +-- Two modalities (`Bool`), Boolean values. The oracle proposes `true` +-- for modality `true` only while modality `false` is still bot. Then +-- the empty section ⊑ the section with modality `false` set, but their +-- fills are incomparable: the first gains a value at `true` that the +-- second never does. +---------------------------------------------------------------------- + +module FillNotMonotone where + + V₂ : Bool → Set + V₂ _ = Bool + + is-bot : Maybe Bool → Bool + is-bot nothing = true + is-bot (just _) = false + + propose₂ : PartialSection Bool V₂ → PartialSection Bool V₂ + propose₂ s true = if is-bot (s false) then just true else nothing + propose₂ s false = nothing + + empty₂ : PartialSection Bool V₂ + empty₂ _ = nothing + + one₂ : PartialSection Bool V₂ + one₂ false = just true + one₂ true = nothing + + empty⊑one : empty₂ ⊑ one₂ + empty⊑one m v () + + -- Monotonicity would force `fill propose₂ one₂ true ≡ just true`, but + -- it is `nothing`. + fill-not-monotone : ¬ (_⊑_ {M = Bool} {V = V₂} (fill propose₂ empty₂) (fill propose₂ one₂)) + fill-not-monotone mono = absurd (mono true true refl) + where + absurd : fill propose₂ one₂ true ≡ just true → ⊥ + absurd () + +---------------------------------------------------------------------- +-- Companion remark. +-- +-- * `merge-*` are implications from properties of `resolve`. The only +-- kernel squeakwell can reach through verisim-api today (PUT +-- overwrite, `resolve a b = b`) is commutative only on a singleton +-- value type; Recovery.v states that negative half +-- (`put_commutative_iff_trivial`). +-- * The termination argument (lexicographic progress on +-- `(|missing|, nconflicts)`, nine-round bound) needs a FINITE index +-- set and a conflict test; it lives in Recovery.v over the concrete +-- eight-modality octad and is not restated here over an arbitrary +-- `M`. +-- * Audit modalities (provenance / temporal hash chains) move by chain +-- prefix, not by this fill; that is verisimdb/formal/Provenance.v. +---------------------------------------------------------------------- diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index fe6ac1e..7ed6715 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -611,6 +611,54 @@ open import EchoFiberCount using ; no-echo⇒FiberSize-fin≡0 ) +-- EchoTruncation — the generic "non-injective ⇒ Echo not a proposition" +-- lemma, previously compiled only through its example corollaries; wired +-- and pinned for the squeakwell review-queue argument (rung R13). +open import EchoTruncation using + ( isProp + ; echo-witnesses-distinct + ; preimages⇒distinct-echoes + ; echo-not-prop + ) + +-- EchoFibreIntersection — multi-witness narrowing (squeakwell R8): the +-- fibre of a pairing IS the intersection of fibres over one witness +-- (`fibre-intersection-iso`, K-free `_↔_`); forgetting a constraint keeps +-- the witness; a `Fin (suc n)` family is one binary step on a `Fin n` +-- family; and on a finite domain the honest count can only shrink +-- (`narrow-shrinks`). +open import EchoFibreIntersection using + ( Narrow + ; fibre-intersection-iso + ; forget-left-witness + ; forget-right-witness + ; narrow-fin-step-to + ; narrow-fin-step-from + ; narrow-shrinks + ) + +-- EchoPartialSection — partial sections of a modality bundle (the octad as +-- an instance), information order, resolve-parametric merge (the pointwise +-- R1–R3 twins of verisimdb Octad.v), guarded fill as left-biased merge +-- (inflationary, not monotone), and the restriction fibre (fragment +-- observation fidelity, R12). Rocq recheck: verisimdb formal/Recovery.v. +open import EchoPartialSection using + ( PartialSection + ; ⊑-refl + ; ⊑-trans + ; merge-comm + ; merge-assoc + ; merge-idem + ; fill-guarded + ; fill-inflationary + ; restrict-echo + ; restrict-fibre-agree + ; restrict-blind + ) +open EchoPartialSection.FillNotMonotone using + ( fill-not-monotone + ) + open import EchoThermodynamics using ( landauer-bound ; fiber-erasure-bound