Repository navigation
feat(recovery): EchoPartialSection + EchoFibreIntersection; wire EchoTruncation (squeakwell R3/R8/R9/R12/R13) - #370
Open
hyperpolymath wants to merge 2 commits into
Open
hyperpolymath wants to merge 2 commits into
hyperpolymath wants to merge 2 commits into
Conversation
…Truncation (squeakwell R3/R8/R9/R12/R13) The Agda source of truth for the repaired recovery invariants of hyperpolymath/squeakwell (database recovery through cross-modal constraint propagation on VeriSimDB), rechecked in Rocq as verisimdb formal/Recovery.v (verisimdb#350) with the Lean side in tropical-types Resource/HubCeiling.lean (tropical-types#67). - EchoPartialSection.agda (Tier 1: Echo + stdlib). Partial sections (m : M) → Maybe (V m) of a modality bundle — the octad as an instance; the information order (refl, trans); the resolve-parametric merge with the pointwise R1–R3 twins of Octad.v (merge-comm / merge-assoc / merge-idem, implications from resolve, not CRDT laws); guarded fill as the left-biased merge against an oracle proposal — never overwrites (fill-guarded), inflationary (fill-inflationary), and NOT monotone (FillNotMonotone.fill-not-monotone, two-modality counter-model); restriction to an observed mask and its Echo fibre (restrict-echo, restrict-fibre-agree, restrict-blind — the fragment-granularity observation-fidelity shape). Funext-free: every law is pointwise. - EchoFibreIntersection.agda (Tier 2: Echo + EchoFiberCount). Binary narrowing is the fibre of the pairing (fibre-intersection-iso, a K-free _↔_ with refl round-trips); forgetting or adding a constraint keeps the witness (forget-*-witness, narrow-fin-step-to/from and their witness lemmas); on a finite domain the honest count never grows when an observation is added (narrow-shrinks, via dec-× and lock-step recursion with FiberSize-fin). Not claimed: inhabitation, or "covering masks ⇒ subsingleton" (needs extensionality). - EchoTruncation.agda, until now compiled only through its example corollaries, is wired into All.agda and pinned (isProp, echo-witnesses-distinct, preimages⇒distinct-echoes, echo-not-prop) — with the FiberSize-fin ≡ 0 ⇔ ¬Echo pair it is the review-queue completeness kernel. Docs: echo-kernel-note classification row, MAP Direction "Database recovery — squeakwell / VeriSimDB bridge", bridge-status Tracks row and revision entry, CHANGELOG Added entry. Verified here with the CI-pinned toolchain (Agda 2.7.0.1, agda-stdlib 8326c74, absolute-zero f486c29): both new modules, All.agda and Smoke.agda exit 0 under --safe --without-K --cubical-compatible (warnings: UnsupportedIndexedMatch only, as the existing suite emits); zero postulates; scripts/kernel-guard.sh PASS. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 47 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 23:19
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The Agda source of truth for the repaired recovery invariants of hyperpolymath/squeakwell (database recovery through cross-modal constraint propagation on VeriSimDB; route plan rungs R3, R8, R9, R12, R13). Rocq recheck: verisimdb
formal/Recovery.v(verisimdb#350). Lean side: tropical-typesResource/HubCeiling.lean(tropical-types#67). This also lands the "join-semilattice of partial sections" abstraction that verisimdb'sCROSS-REPO-MAP.adocflagged as the missing echo-types companion toOctad.vR1–R3.What lands
EchoPartialSection.agda(Tier 1:Echo+ stdlib). Partial sections(m : M) → Maybe (V m)of a modality bundle — the octad is an instance. Information order (⊑-refl,⊑-trans). Resolve-parametricmergewith the pointwise R1–R3 twins ofOctad.v(merge-comm/merge-assoc/merge-idem: implications fromresolve, not CRDT laws). Guarded fill as the left-biased merge against an oracle proposal:fill-guarded,fill-inflationary, and the counter-modelFillNotMonotone.fill-not-monotone(two modalities). Restriction to an observed mask and its Echo fibre:restrict-echo,restrict-fibre-agree(a candidate inEcho (restrict T) obsreproducesobson every observed modality — the fragment-granularity observation-fidelity shape),restrict-blind. Every law is pointwise; no funext.EchoFibreIntersection.agda(Tier 2:Echo+EchoFiberCount).fibre-intersection-iso : Echo < f , g > (y , z) ↔ Narrow f g y z(K-free,reflround-trips). Forgetting or adding a constraint keeps the witness (forget-*-witness,narrow-fin-step-to/from+ witness lemmas; theFin nstep is deliberately not a_↔_, since the function-side round trip would need funext).narrow-shrinks: on a finite domain with decidable equality,FiberSize-fin < f , g > (y , z) ≤ FiberSize-fin f y(viadec-×, lock-step with the count's recursion).EchoTruncation.agdawired. Until now compiled only through its corollaries; now inAll.agdaand pinned (isProp,echo-witnesses-distinct,preimages⇒distinct-echoes,echo-not-prop). WithFiberSize-fin≡0⇒no-echo/no-echo⇒FiberSize-fin≡0it is the review-queue completeness kernel (R13 theory half).Not claimed: inhabitation of the narrowed fibre; "covering masks ⇒ subsingleton" (needs extensionality over opaque identifiers — dropped in the route plan); termination of the recovery round (Rocq-only, needs the finite octad:
iter_9_fixpointinRecovery.v).Docs
echo-kernel-note.adocclassification row ("Derived — recovery ladder (2026-11-09)");MAP.adocDirection "Database recovery — squeakwell / VeriSimDB bridge[REAL]";cross-repo-bridge-status.adocTracks row + revision entry;CHANGELOG.adocAdded entry.Verification (this environment, CI-pinned toolchain via
scripts/setup-agda.sh)Agda 2.7.0.1 (checksum-pinned), agda-stdlib
8326c7475af1fa456ca04a0203c168d5d7ff842b, absolute-zerof486c29903434589117fa0662c6f29b0f17d1d5f:Warnings are
UnsupportedIndexedMatchonly (the class the existing suite already emits). Zero postulates, no escape pragmas.Generated by Claude Code