Repository navigation
fix(proofs): DOM-1/DOM-2 corrected, checked in CI with pinned Agda, graded PWG-3 from receipts - #127
Merged
Merged
Conversation
…rapper, no silent skips
Follow-up to the 2026-11-09 proof audit of DOM-1/DOM-2 and its skeptic
re-check.
- Burrow.Trust: epi-is-not-factive was `λ f → f : ¬X → ¬X`, the identity,
so DOM-1's claim that a warrant is not factive had no declaration
stating it. It is now `¬ (∀ {A} → Epi A → A)`, proved from the legacy
countermodel. revalidate drops an implicit argument it never used and
no caller could infer.
- Burrow.Ledger: promote takes its stored record explicitly. A
projection cannot be inverted, so the implicit argument was never
inferable at a call site.
- scripts/agda-safe-check.sh used to cd into the file's own directory,
so every hierarchical module failed (Burrow/Burrow/Trust.agda). It
now reads the module name and checks from the include root, and it
refuses a module whose name does not match its path. The test gains
a hierarchical case and a mismatch case.
- The Justfile proof-check-{idris2,lean4,agda,coq} recipes now exit 1
with "NOT RUN" when the prover is missing, instead of printing SKIP
and exiting 0 (PROOF-POLICY §2.1).
- proof-scan-dangerous now runs scripts/proof-scan-dangerous.sh, which
removes comments per language before matching. The old grep failed on
main with eight header-comment false positives, which drowned any real
hit. It now passes on the tree and flags every planted escape hatch in
the Agda, Lean and Coq controls.
- docs/status/PROOF-STATUS.adoc and CLAUDE.md:
- Restate grades as PROOF-POLICY §8 PWG. DOM-1/DOM-2 are ungraded
until a receipt lands here.
- Correct the proof dates to 2026-11-03 (#119).
- Record DOM-2 as a specification the Rust read path does not yet meet.
- Name Creusot with Pearlite, and Verus, for first-party Rust.
Checked locally with Agda 2.7.0.1 and agda-stdlib 2.1 under --safe
--without-K --cubical-compatible: Burrow.Trust and Burrow.Ledger exit 0,
the wrapper checks both, and a probe module that applies revalidate and
promote type-checks.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
…e receipts The audit found that no workflow type-checked any file under verification/proofs/, so DOM-1 and DOM-2 had no CI receipt, and that nothing pinned the Agda version or the standard library (PROOF-POLICY §2.1, §8.2). - verification/proofs/agda/burrow.agda-lib pins the include root and the dependency on standard-library-2.1. - scripts/ci/setup-agda.sh, ported from echidna, installs Agda 2.7.0.1 and agda-stdlib 2.1 from digest-checked upstream archives, and fails closed. - scripts/ci/agda-cone-receipt.sh and test-agda-cone-receipt.sh, ported from echidna, write the §8.2/§8.4 receipt: toolchain digests, flags, the import cone with a SHA-256 per file, and a comment-aware postulate scan. The test checks the scan on a fixture. - proof-safety.yml gains an `agda` job. It type-checks both modules through the fixed wrapper and records a receipt for each, using only the already-locked actions/checkout. Local run with the same pins: Burrow.Trust has a cone of 34 modules, Burrow.Ledger 35, both scans are clean, and Agda.Primitive's level primitives are the only kernel postulates. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
…OM-1 and DOM-2 docs/reports/2026-11-09-agda-cone-receipts.jsonl holds one JCS receipt per theorem module. Both were written by scripts/ci/agda-cone-receipt.sh at 22f6f72, with no uncommitted change under verification/proofs/agda/. They record the pinned Agda 2.7.0.1 and agda-stdlib 2.1, the policy flags, import cones of 34 and 35 modules, and clean postulate scans. The census in PROOF-STATUS and the CLAUDE.md status line now read PWG-3 2/2, derived from those receipts. Neither module has a Rocq or Lean leg yet. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
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 59 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. |
…'s W0 gate reads Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
The new agda-proofs job failed with "Library 'standard-library-2.1' not found". burrow.agda-lib depends on the stdlib, and Agda resolves that through --library-file or ~/.config/agda/libraries. It reads no AGDA_LIBRARIES_FILE variable. The receipt script already passed --library-file; the safe-check wrapper did not. It now does, with --no-default-libraries, whenever AGDA_LIBRARIES_FILE is set, and fails closed when that file is missing. Reproduced the CI failure locally with a clean HOME (rc 42). After the fix, Burrow.Trust and Burrow.Ledger check under pinned Agda 2.7.0.1 and stdlib 2.1, with and without the -i include. The cone receipt still reports 34 modules, clean. tests/agda-safe-check.sh gains a positive argv check and a missing-file negative control, and now unsets the toolchain variables so a CI job environment cannot leak into it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
|
❌ The last analysis has failed. |
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:40
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 22:56
hyperpolymath
disabled auto-merge
November 10, 2026 01:48
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 2026-11-09 proof audit and its skeptic re-check found several problems in this repository's two Agda theory results, DOM-1 (
Burrow.Trust) and DOM-2 (Burrow.Ledger), and in the tooling around them:This PR fixes all six.
Changes
epi-is-not-factivewasλ f → f : ¬X → ¬X. It is now¬ (∀ {A} → Epi A → A), proved from the legacy countermodel, so DOM-1's claim that a warrant is not factive is finally stated.revalidatedrops an implicit argument it never used and no caller could infer.promotetakes its stored record explicitly, because a projection cannot be inverted.scripts/agda-safe-check.sh. It reads the module name and checks from the include root, so hierarchical modules work. It refuses a module whose name does not match its path. The test gains a hierarchical case and a mismatch case.proof-check-{idris2,lean4,agda,coq}exit 1 with "NOT RUN" when the prover is missing.proof-scan-dangerousnow callsscripts/proof-scan-dangerous.sh, which strips comments per language before matching.proof-safety.ymlgains anagdajob, using only the already-lockedactions/checkout. It installs the pinned toolchain from digest-checked archives (scripts/ci/setup-agda.sh, ported from echidna), type-checks both modules through the wrapper, and writes a receipt for each.scripts/ci/agda-cone-receipt.shand its fixture test are ported from docs(proofs): PROOF-STATUS under strict §1, a §8.2 cone receipt, and a PWG census echidna#479. The receipt records the toolchain, the flags, the import cone with a digest per file, and a comment-aware postulate scan.docs/reports/2026-11-09-agda-cone-receipts.jsonl.verification/proofs/agda/burrow.agda-libpins the include root andstandard-library-2.1.docs/status/PROOF-STATUS.adocandCLAUDE.mdrestate grades as PROOF-POLICY §8 PWG. The census, derived from the receipts, isPWG-32/2 by obligation.Ledger::read_alldoes not yet meet; that obligation belongs to Rust verification.RSR Quality Checklist
Required
tests/agda-safe-check.shpasses.scripts/ci/test-agda-cone-receipt.shpasses.--safe --without-K --cubical-compatible.shellcheckis clean on all new and changed scripts. The workflow parses.As Applicable
Testing
All checks below were run locally with Agda 2.7.0.1 and agda-stdlib 2.1 (archive SHA-256
72ca3ea2…).Burrow.TrustandBurrow.Ledgerexit 0 under the policy flags, both directly and through the fixed wrapper.revalidate legacy-epiandpromote legacy-storedtype-checks. Before this change, both failed with "Unsolved metas".22f6f723with no uncommitted change underverification/proofs/agda/. The import cones are 34 and 35 modules, which matches the skeptic's independent count. Both scans are clean; the only postulates areAgda.Primitive's universe-level primitives.agdajob's first run is on this PR.Generated by Claude Code