Repository navigation
docs(proofs): PROOF-STATUS under strict §1, a §8.2 cone receipt, and a PWG census - #479
Open
hyperpolymath wants to merge 14 commits into
Open
hyperpolymath wants to merge 14 commits into
hyperpolymath wants to merge 14 commits into
Conversation
cargo audit fails on rmcp 3.5.0 (crates/echidna-mcp) with RUSTSEC-2026-0457 (fixed >=3.7.0), RUSTSEC-2026-0461 (>=3.6.0) and RUSTSEC-2026-0462 (>=3.9.0), published after main last passed the Dependency audit check. `cargo update -p rmcp` moves rmcp and rmcp-macros to 3.9.0, inside the existing "3" requirement; no other entry changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
`cargo fmt --check` fails on main (2ab7574) in five places in src/rust/proof_search.rs, so rust-ci 'Cargo check + clippy + fmt' is red on every PR. Formatting only; no code change. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
Hypatia's code_safety/zig_ptr_cast and zig_align_cast now flag the nine `@ptrCast(@aligncast(raw))` lines in src/zig_ffi/chapel_bridge.zig and src/zig_ffi/runtime_owner.zig as high, and the governance Hypatia baseline gate is red on main (2ab7574) as a result. Each of those lines recovers a callback's own `*@this()` from the type-erased `*anyopaque` it was registered with (runtime_owner.Work .context, or a std.mem.Allocator vtable's ptr), so the cast restores the original type and alignment. Fixed at source with a reasoned inline `hypatia: allow` per rule on each line, as the scanner documents, rather than a baseline entry. No code change: comments only. Checked by simulating ScannerSuppression.inline_allowed?/4 and directive_re at hypatia 82396d81 (the CI pin): 18 unsuppressed findings on main, 0 with this change. The scanner itself could not be built here (hex.pm is unreachable). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
…oof-search' into claude/new-session-th4e9w-rustsec-rmcp
…st-audit' into claude/new-session-th4e9w-rustsec-rmcp
…o small kernels
The 2026-11-09 proof audit found two defects in compute_trust_level. Both
were present identically in src/rust/verification/confidence.rs and in
its copy in crates/echidna-core-creusot, and no proof caught either.
- Level 4 fired on certificate_verified without has_certificate.
- Level 5 checked only the producing prover's kernel class, never the
confirmers'. One small-kernel prover plus an SMT confirmer scored
Level 5.
Fixed at the source: the kernel crate (echidna_core::trust).
- Level 3 and above count a certificate only when it was produced and
verified.
- Level 5 needs two or more small-kernel confirmations. They are given by
a new TrustFactors input, small_kernel_confirmations: how many of the
confirming provers are small-kernel systems with a verified certificate,
the producing prover included. Read at most confirming_provers;
#[serde(default)] = 0.
One kernel, not two: confidence.rs re-exports the kernel's TrustLevel and
delegates compute_trust_level to it. It keeps its ProverKind-shaped
TrustFactors and maps the prover to a kernel class with
is_small_kernel_prover.
Contracts stated on the kernel, as Creusot ensures:
- TK-4: Level 4 and above imply a small kernel, has_certificate and
certificate_verified.
- TK-5: Level 5 implies small_kernel_confirmations >= 2 and
confirming_provers >= 2.
They are not yet discharged by Creusot. Stable-Rust tests check them over
every input with counts 0..=4 (tk4, tk5, and tk6 for monotonicity in the
evidence), plus regressions for both defects. With the old logic put back
in place, three of these tests fail.
This departs from the ruling's wording ("every confirming prover is small
kernel"). Level 5 instead counts small-kernel confirmations, at least
two. Requiring every confirmer to be a small kernel would let one extra
SMT agreement lower a result from Level 5 to Level 4, breaking
monotonicity. The count also matches the Level 5 definition already in
the code: "cross-checked by 2+ independent small-kernel systems".
The shipped dispatch paths pass 0 for the new input. They already
reported no certificate, so their results do not change. Every other
TrustFactors literal gains the field with 0. The confidence.rs Level 5
test now states two small-kernel confirmations, and three tests are new:
one small-kernel confirmation is Level 4, a verified flag without a
certificate is Level 2, and the kernel's small-kernel class follows
is_small_kernel_prover.
Retired: verification/proofs/idris2/TrustKernelMonotonicity.idr. It
dropped has_certificate and proved the defective Level 5 rule as a
property. Under PROOF-POLICY §1, Rust behaviour is verified on the code.
PROOF-STATUS R1 records TK-4/TK-5 as tested-only. Creusot is not
discharged and Verus is not yet applied, both with their scope. R1 stays
open. PROOF-NEEDS marks the Idris row retired. CHANGELOG notes the
behaviour change.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
…ne receipt Owner ruling 2026-11-09: apply PROOF-POLICY §1 strictly. A statement that names one of this repository's types, functions or wire formats is engineering, whichever prover it is written in. The ledger is reworked to match, using the findings of the 2026-11-09 proof audit and its skeptic re-checks. Classification: - Theory: Receipt.agda, ten theorems (R4a). It owes the Rocq and Lean rechecks (R5). - Engineering models with no standing as evidence for the Rust code, which stays open under R1 (Creusot with Pearlite, and Verus, §1.2): - the other eight meta-checker modules (R4b); - the five Lean files, which are not §4 exceptions (R3); - the Idris 2 files under verification/proofs/idris2 (R2b). - The Idris 2 ABI package keeps its §1 home (R2a). Corrections: - R3: the Lean files build green in CI (job 127501093731 at a81467b, the same tree as main). The "all five fail to compile" row was stale. - R2a: cites its CI receipt (run 38496490567, 20/20 modules plus the falsifier fixtures). It also records the coverage gap (10 of 30 .idr files never type-checked) and the narrow dangerous-pattern grep. - R6/E9: ProofComposition.agda proves only list-append associativity and left identity. Moving it would not discharge E9, which no theorem states. PROOF-NEEDS is corrected to match. - The models' disagreements with the Rust code are listed for R1: - Dispatch.compute-trust; - the Integrity "sharpness" claim; - ClampTrust, which models a function Rust does not have; - IntegrityVerification PI-11 against the four fail-open dispatch paths; - Pareto PO-12's no-duplicates assumption; - ProverKindInjectivity, whose encoding differs from the Rust function for 79 of 107 variants. Grades: - PROOF-POLICY §8 Proof Witness Grades replace the Mathesis-brief "Grade 3" wording. - A §8.5 census lists the ten theory theorems, each with its §5 token, PWG, foundation_diverse flag and both recheck legs. Receipt tooling: - scripts/ci/agda-cone-receipt.sh writes the §8.2/§8.4 receipt as one JCS object: toolchain, flags, the import cone with a SHA-256 per file, and a comment-aware scan of that cone for postulates, unsafe pragmas and primTrustMe. Postulates in Agda's own primitives are listed, not counted. - scripts/ci/test-agda-cone-receipt.sh is its fixture test. - The agda-meta-checker job runs both and prints the receipt to the log and the step summary. - Local run with the pinned Agda 2.7.0.1 and stdlib 2.1: the cone of Receipt.agda is 211 modules, the scan is clean, and Agda.Primitive's two universe-level postulate blocks are the only kernel primitives. Adjacent docs: - EXPLAINME no longer calls the Agda models "independent formal verification of the Rust trust-pipeline properties", and no longer lists proofs/agda/ (a §3 fixture tree) as the meta-checker. - DEBT's R9 reference now points at R4b. - meta-checker/README.adoc no longer claims one funext postulate. --safe refuses any postulate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
…e theory theorems docs/reports/2026-11-09-agda-cone-receipt.json was written by scripts/ci/agda-cone-receipt.sh at 4c3ea68, with no uncommitted change under meta-checker/: - toolchain: pinned Agda 2.7.0.1 (executable SHA-256 6de41437…) and agda-stdlib 2.1 (archive SHA-256 72ca3ea2…); - flags --safe --without-K --cubical-compatible on Receipt.agda, which the kernel accepted; - an import cone of 211 modules, each with its digest; - a clean comment-aware postulate scan. scripts/ci/check-agda.sh passed at the same commit, with 9/9 fresh interfaces. From that receipt, the census derives PWG-3 for 10/10 theory theorems. None reaches PWG-2i or above, because R5's Rocq and Lean legs do not exist. 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 30 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. |
…assert TK-4/TK-5 The fuzz crate is outside the workspace, so the new TrustFactors field was missed there and the OSS-Fuzz "PR (address)" build failed (E0063). The field is now fuzzed independently, so inconsistent inputs (more small-kernel confirmations than confirmations) are covered too. The target now also asserts the kernel contracts on every input: TK-4 (level >= 4 needs a small kernel and a produced, verified certificate) and TK-5 (level 5 needs two small-kernel confirmations). Checked with `cargo check --manifest-path fuzz/Cargo.toml --bins` (stable 1.99). It was not run under cargo-fuzz: no nightly toolchain here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
…-trust' into claude/zen-brahmagupta-opqqle-w0-ledger
…c-rmcp' into claude/zen-brahmagupta-opqqle-w0-trust
…en-brahmagupta-opqqle-w0-ledger
Owner
Author
|
This PR is stacked on #477, so it had the same red checks. Its base fixes are now merged in, head 2af9113: the fuzz-target fix (3c70abb) and the port of #465 (rmcp 3.9.0 and rustfmt, both also red on There is overlap you should know about. #474 and #482 also rewrite Generated by Claude Code |
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2af9113465
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| run: | | ||
| set -euo pipefail | ||
| PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls)\.sh$|\.github/workflows/agda-meta-checker\.yml$)' | ||
| PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls|agda-cone-receipt|test-agda-cone-receipt)\.sh$|\.github/workflows/agda-meta-checker\.yml$)' |
There was a problem hiding this comment.
When a push to main changes only agda-cone-receipt.sh or test-agda-cone-receipt.sh, this detector never executes because the workflow-level path scripts/ci/*agda.sh matches filenames ending in agda.sh, not either newly listed receipt script. Consequently, direct or merge pushes affecting only this receipt tooling skip the proof workflow despite being classified as relevant here; add these scripts to the push.paths filter (or broaden that filter consistently).
Useful? React with 👍 / 👎.
… scripts The `push` path filter `scripts/ci/*agda.sh` matches neither agda-cone-receipt.sh nor test-agda-cone-receipt.sh. A push to main that changes only the receipt tooling therefore skipped the workflow, even though the in-job detector counts those files as relevant (Codex P2 on this PR). Both scripts are now listed explicitly. actionlint 1.7.7 is clean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
|
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autofix |
Base automatically changed from
claude/zen-brahmagupta-opqqle-w0-trust
to
main
November 9, 2026 23:48
hyperpolymath
added a commit
to hyperpolymath/proof-burrower
that referenced
this pull request
Nov 10, 2026
…raded PWG-3 from receipts (#127) ## 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: - One "theorem" was the identity function. - Two functions could never be called, because Agda could not infer their implicit arguments at a call site. - The wrapper script failed on any module in a subdirectory. - No CI job checked any proof, and the proof recipes printed SKIP and exited 0 when a prover was missing. - The dangerous-pattern scan failed on main because it matched header comments. - Nothing pinned the Agda version or the standard library, so no grade could be derived. This PR fixes all six. ## Changes - **Proof fixes.** - `epi-is-not-factive` was `λ 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. - `revalidate` drops an implicit argument it never used and no caller could infer. - `promote` takes 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. - **Justfile.** - `proof-check-{idris2,lean4,agda,coq}` exit 1 with "NOT RUN" when the prover is missing. - `proof-scan-dangerous` now calls `scripts/proof-scan-dangerous.sh`, which strips comments per language before matching. - **CI.** `proof-safety.yml` gains an `agda` job, using only the already-locked `actions/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. - **Receipts and grades.** - `scripts/ci/agda-cone-receipt.sh` and its fixture test are ported from hyperpolymath/echidna#479. The receipt records the toolchain, the flags, the import cone with a digest per file, and a comment-aware postulate scan. - Committed receipts: `docs/reports/2026-11-09-agda-cone-receipts.jsonl`. - `verification/proofs/agda/burrow.agda-lib` pins the include root and `standard-library-2.1`. - **Docs.** - `docs/status/PROOF-STATUS.adoc` and `CLAUDE.md` restate grades as PROOF-POLICY §8 PWG. The census, derived from the receipts, is `PWG-3` 2/2 by obligation. - The proof dates are corrected to 2026-11-03 (#119). - DOM-2 is recorded as a specification that `Ledger::read_all` does not yet meet; that obligation belongs to Rust verification. - Rust verification is named as Creusot with Pearlite, and Verus (§1.2). ## RSR Quality Checklist ### Required - [x] **Tests pass:** - `tests/agda-safe-check.sh` passes. - `scripts/ci/test-agda-cone-receipt.sh` passes. - Both Agda modules exit 0 under `--safe --without-K --cubical-compatible`. - [x] **Lint:** `shellcheck` is clean on all new and changed scripts. The workflow parses. - [x] **No banned functions:** this PR removes a vacuous theorem and adds no escape hatch. - [x] SPDX headers on new files. - [x] No secrets. ### As Applicable - [x] Documentation updated. ## Testing All checks below were run locally with Agda 2.7.0.1 and agda-stdlib 2.1 (archive SHA-256 `72ca3ea2…`). - **Type-checking.** `Burrow.Trust` and `Burrow.Ledger` exit 0 under the policy flags, both directly and through the fixed wrapper. - **Call sites.** A probe module that applies `revalidate legacy-epi` and `promote legacy-stored` type-checks. Before this change, both failed with "Unsolved metas". - **Receipts.** Both were written at `22f6f723` with no uncommitted change under `verification/proofs/agda/`. The import cones are 34 and 35 modules, which matches the skeptic's independent count. Both scans are clean; the only postulates are `Agda.Primitive`'s universe-level primitives. - **Escape-hatch scan.** It passes on the tree. On planted Agda, Lean and Coq files it flags exactly the real escape hatches and ignores the commented ones, including nested comments. - **Not run here.** The new CI `agda` job's first run is on this PR. --- _Generated by [Claude Code](https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
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
This PR is stacked on #477 (the trust-kernel fix), because both edit PROOF-STATUS R1. Review or merge #477 first, and this PR's diff then reduces to the ledger work.
The owner ruled on 2026-11-09 that PROOF-POLICY §1 applies strictly: a statement that names one of this repository's types, functions or wire formats is engineering, whatever prover it is written in. This PR reworks
docs/PROOF-STATUS.adocto match, using the 2026-11-09 proof audit and its skeptic re-checks. It also adds the tooling for the §8.2 receipt, records one receipt, and derives the Proof Witness Grade census from that receipt.Changes
Classification
Theory.
Receipt.agdais the only theory module. It has 10 theorems (R4a), and those owe the Rocq and Lean rechecks (R5).Engineering models. These describe Rust behaviour but are not evidence for the Rust code:
verification/proofs/idris2/(R2b).The Rust obligations they describe stay
openunder R1. Under §1.2, those belong to Creusot with Pearlite, and Verus.ABI package. The Idris 2 ABI package keeps its home under §1 (R2a). It cites its CI receipt (20/20 modules plus the falsifier fixtures) and records its coverage gap: 10 of the 30
.idrfiles are never type-checked.Corrections
ProofComposition.agdaproves only list-append associativity and left identity. Moving the file would not discharge E9. PROOF-NEEDS is corrected to match.Dispatch.compute-trustdisagrees with the Rust trust rule.Integrity's "sharpness" claim does not hold.ClampTrustmodels a function Rust does not have.ProverKindInjectivity's encoding disagrees with the Rust function for 79 of 107 variants.EXPLAINME.adocno longer claims "independent formal verification of the Rust trust-pipeline properties".DEBT.adocreference now points at R4b.meta-checker/README.adocno longer claims a funext postulate;--saferefuses any postulate.Receipt tooling (PROOF-POLICY §8.2, §8.4)
scripts/ci/agda-cone-receipt.shwrites one JCS receipt. It records:primTrustMe. Postulates in Agda's own primitives are listed but not counted.scripts/ci/test-agda-cone-receipt.shis the fixture test for the scan.agda-meta-checkerjob runs both and prints the receipt to the log and the step summary.Grades. "Grade 3" wording is replaced by the §8 PWG prefix. The §8.5 census reads
PWG-310/10, derived fromdocs/reports/2026-11-09-agda-cone-receipt.json. Nothing reaches PWG-2i or above, because the Rocq and Lean legs do not exist.RSR Quality Checklist
Required
scripts/ci/check-agda.sh, run locally with the pinned Agda 2.7.0.1 and stdlib 2.1: exit 0, 9/9 fresh interfaces, receipt controls passed.scripts/ci/test-agda-cone-receipt.sh: ok.shellcheckpasses on both new scripts. The workflow parses.As Applicable
PROOF-STATUS,PROOF-NEEDS,EXPLAINME,DEBT,meta-checker/README.adoc.Testing
4c3ea688, with no uncommitted change undermeta-checker/. It records:6de41437…, which matches the repository pin;72ca3ea2…;Agda.Primitive's universe-level primitives.postulates-namedoes not count as thepostulatekeyword.--saferemains the check that refuses escape hatches.Generated by Claude Code