Repository navigation
docs(proofs): bring PROOF-STATUS up to PROOF-POLICY §1.2, §6 and §8 - #474
Conversation
PROOF-STATUS predated two policy amendments (§8 Proof Witness Grades, 2026-11-04; §1.2 Creusot, Pearlite and Verus, 2026-11-07) and understated two legs that CI already proves. - Grades: replace the bare "Mathesis Grade 3" wording, which §8 forbids, with a PWG table. Only theory theorems are graded; Receipt is PWG-3 with both recheck legs open. - R1: name Creusot, Pearlite and Verus, with the status of each. - R2 (Idris 2): proven, citing the Dogfood "Idris2 (verification)" job, which builds all eleven modules of echidna-verif-proofs.ipkg. - R3 (Lean): proven-with-postulates, citing the "Lean 4 (verification)" job and a local Lean 4.13.0 recheck. Of 167 theorems, 109 use no axiom and 58 use only propext, Quot.sound and Classical.choice. The Mathlib question is closed by §2. - R4: cite the hosted Agda Meta-Checker run on 2ab7574 (exact commit), corroborated locally, and record the owner's §1 decision to split the meta-checker (theory to Agda, echidna types to Idris 2, Rust verified with Creusot/Pearlite and Verus). - R10: no clamp_trust exists in the Rust, so the row is model-only; the module header's "no idris2 in CI" reason is out of date. - §6: add the missing deviation records for the Agda, Idris 2 and Lean lanes, in PROOF-STATUS and as comments in the installing scripts and workflows. Comments only; no uses: changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
|
Caution Review failedThe pull request is closed. Summary
Merge Risk:
 |
The README claimed one postulate (funext), which --safe rules out and which no module contains. It also listed four of the nine modules, counted "30+ properties" that nobody had counted, gave run steps without the PROOF-POLICY §2.1 flags, and said a green check guarantees that the system's invariants hold. It now lists all nine modules, says they prove properties of a model rather than of the Rust, records that only Receipt is theory under §1, documents the pinned setup and check scripts, and points to PROOF-STATUS for receipts. Mathesis's reconciliation register cites the stale funext note as an open ECHIDNA item; this removes it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
A statement-by-statement comparison of the Agda meta-checker with the Rust, the Idris 2 corpus and the Lean corpus found problems that a passing kernel check does not reveal: - Dispatch.compute-trust gives Level 2 for a cross-checked result without a certificate; the Rust and Idris 2 give Level 3. - Integrity.check maps an uninitialised manifest to Missing; the Rust and Lean give Uninitialized. - Portfolio.portfolio-trust and ClampTrust.clamp-trust have no Rust counterpart. - comment-skip-sound ignores its hypothesis, real-pattern-classified only proves totality, and two "determinism" theorems are cong. - Idris 2 lacks Level 5 necessity and clamp idempotence. The rows keep their proven token (the kernel did accept these proofs); the review lists what the planned split must fix. The README now points readers to it instead of implying the names are the guarantees. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
Port of the rmcp lockfile change from #465 so this docs PR's dependency audit is not red for a reason unrelated to it. Regenerated with `cargo update -p rmcp --precise 3.9.0`; the windows-sys lines are resolver output, identical to #465. No-op once #465 lands. Verified locally: scripts/ci/audit-dependencies.sh passes for both lockfiles; `cargo check -p echidna-mcp` builds. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
|
Dependency audit failed on #465 already contains the fix, and I have ported its rmcp part here as 45c0c93. That commit runs The red Generated by Claude Code |
The owner chose #477's reading of PROOF-POLICY §1 for the split. Generic theory (Receipt; E9 composition in #471) stays in Agda. Echidna-specific statements are verified on the Rust with Creusot/Pearlite and Verus, not restated in Idris 2. Each meta-checker module retires once its Rust contracts carry a receipt. R1 now points at #477's trust kernel as the first Creusot target. R10 has no Rust target (there is no clamp_trust), so it retires with its module. The Lean re-homing note distinguishes Rust behaviour (Creusot/Verus) from API/ABI properties (Idris 2). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
Validate Hypatia Baseline fails on this PR. It reports four unannotated zig_ptr_cast/zig_align_cast findings in src/zig_ffi/, which are also red on main and unrelated to this docs PR. This ports #465's fix unchanged: - inline `hypatia: allow` annotations with a justification on each cast (comments only; the code is unchanged); - its rustfmt reflow of src/rust/proof_search.rs. Both become no-ops once #465 lands. `rustfmt --check` passes on proof_search.rs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
|
governance / Validate Hypatia Baseline is failing because of #465 has the fix, so I ported it here unchanged as d4ef769:
Both changes become no-ops once #465 lands. Generated by Claude Code |
|
@coderabbitai review Generated by Claude Code |
Action not completed
|
|
Static Analysis / Patch Bridge CVE triage is red, and the cause is on There's no fix to port. #478 moves the pin to 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. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
![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: d4ef769802
ℹ️ 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".
…a recipe Fixes two Codex review findings on #474: - R10 said no Rust clamp_trust exists. One does: echidna_core_creusot::clamp_trust(level, min, max), with a written but undischarged Creusot bounds contract and the exhaustive unit test PO-7. R10 now records how it corresponds to the Agda model. Only the bounds statement carries over; the Agda model clamps ℕ, so its ℕ-specific statements do not. The split targets the Rust function, not retirement. - The README's local recipe did not work. Outside Actions, setup-agda.sh only prints the paths. The recipe now provides GITHUB_ENV/GITHUB_PATH files and loads them, so it goes through the script's own export code. The loading step was tested here with values in the script's format. The full setup was not run locally, because the agda-stdlib archive host is blocked in this sandbox. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
## Summary The Static Analysis Gate fails in two different ways, depending on the branch. 1. **On PR branches behind main (for example #474):** `panic-attack assail` exits 2 with `incomplete coverage (partial)`. Then `deposit` fails with "Incomplete scanner evidence". The branch still pins panic-attack `410a8f8`, which predates panic-attack #258. That version has no adapter for TOML, YAML, JSON, Containerfile, Justfile, HTML, CSS or Forth, so it marks 190 of echidna's 908 candidate files "unsupported". **main already fixes this**: it pins `f2a6a70`, which includes #258. Those branches need main merged in. 2. **On main:** coverage is complete and `deposit` passes. But the `panic-attack assail` job fails with "Critical scanner findings block merge". The only 2 critical findings are PA021 ProofDrift: one open `sorry` each, in `tests/corpus_fixtures/isabelle/Smoke.thy` and `tests/corpus_fixtures/minif2f/algebra.lean`. This PR fixes item 2. ## Changes - `audits/assail-classifications.a2ml`: add 2 entries, one per fixture, with category `ProofDrift`. The `sorry`s are deliberate: `tests/corpus_hazard_fixtures.rs` checks that the corpus adapters flag them as hazards, and those tests fail if they are removed. Each entry names its test. - This is an addition only. No existing entry and no licence header changes. ## RSR Quality Checklist ### Required - [x] No banned functions added. The 2 `sorry`s are existing fixtures; this PR only classifies them. - [x] No secrets, credentials, or `.env` files included ## Testing I built panic-attack main (`4f51cca`, `--locked --features http`) and ran it on echidna main with this change: - `assail --fail-on-incomplete`: exit 0, coverage `complete` 913/913, unsuppressed findings: 0 critical, 43 high, 65 medium, 1 low. - The report meets `scripts/ci/static-analysis-evidence.sh`'s panic-attack contract (schema `2.6`). - `bridge triage`: exit 0, schema `0.3.0`, `vulnerability_data: queried`. This matches the Patch Bridge contract. - Without this change, the same scan has 2 unsuppressed critical findings: exactly the 2 fixtures. --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4)_ Co-authored-by: Claude <noreply@anthropic.com>
docs/PROOF-STATUS.adoc conflicted with #482, which refreshed the same file against PROOF-POLICY §1.2 and §8. Owner ruling: keep main, salvage the rest. - Main's text wins in all 11 conflicts (R3 stays open; R12 SPARK row, A5 and the trust-kernel note kept). - Salvaged from this branch: the Receipt PWG table, the 2026-11-09 transport-first decision for the recheck legs (R5), and everything that merged cleanly (R4 receipt and classification, R10 model-versus-code, §6 toolchain deviations, meta-checker README, workflow comments). - The R4 design review is dated to 2ab7574, before #477 retired TrustKernelMonotonicity.idr. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d82b69f616
ℹ️ 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".
| * *No Rust counterpart.* `+Portfolio.portfolio-trust+` (the Rust | ||
| `+compute_trust_level+` never reads `+portfolio_confidence+`) and | ||
| `+ClampTrust.clamp-trust+` (R10). |
There was a problem hiding this comment.
This newly added design-review bullet still classifies ClampTrust.clamp-trust as having no Rust counterpart, but at the stated audit commit 2ab7574, crates/echidna-core-creusot/src/lib.rs:274 already defines clamp_trust, and the corrected R10 row later in this same file records its contracts and semantic mismatch. The contradictory classification can cause the existing Rust verification target to be overlooked or retired. Fresh evidence relative to the earlier review is that the false classification remains in this newly added bullet even though the R10 row itself was corrected.
Useful? React with 👍 / 👎.
| |`+Echidna.MetaChecker+` | ||
| |The entry point that imports the eight modules above. |
There was a problem hiding this comment.
The entry point now imports nine modules, including Echidna.Composition in MetaChecker.agda, but the rewritten module table omits Composition and explicitly says that only the eight listed modules are imported. Readers using this README as the advertised inventory therefore miss the checked E9 composition theory and get an incorrect picture of the current Agda closure; add a Composition row and update the count.
Useful? React with 👍 / 👎.
| |`+manifests/live-provers.scm+` records Idris 2 as absent from its baseline. No | ||
| container stage installs it. |
There was a problem hiding this comment.
The statement that no container stage installs Idris 2 is false: both .containerization/Containerfile and .containerization/Containerfile.full define an idris2-builder stage that runs the Idris2 Pack installer. Those stages are optional and build src/idris rather than the R2 proof packages, so they may still be unsuitable for this lane, but the deviation record should describe those limitations or explicitly refer to the sealed Wave-3 container instead of claiming that no stage exists.
Useful? React with 👍 / 👎.
| |=== | ||
|
|
||
| === Lean 4 — cross-checks and algebraic properties (§4 exceptions) | ||
| === Lean 4 — engineering properties held outside Idris 2 (§3 re-homing pending) |
There was a problem hiding this comment.
The new heading labels the unresolved Lean placement as a §3 matter, but this row's own analysis says §1 assigns these engineering statements to Idris 2 or Rust verification and §4 governs any exception; elsewhere in this file §3 is explicitly the exclusion for prover corpora. Referring to §3 here misclassifies the policy issue and can send maintainers to the wrong requirements when deciding whether to move the proofs or record an exception.
Useful? React with 👍 / 👎.
| Owner decision 2026-11-09: try the §2 *transport* route first (Agda → | ||
| Dedukti/Lambdapi → Rocq), record how it performs, then re-prove in Lean (core |
There was a problem hiding this comment.
The proposed Agda → Dedukti/Lambdapi → Rocq transport route is not currently executable with the capability cited immediately above it. A repository-wide search finds no Agda importer or translator: src/rust/exchange/dedukti.rs only converts ECHIDNA's internal ProofState terms, and its import path explicitly substitutes an empty proof rather than translating proof bodies. Following this plan for Receipt.agda therefore first requires a real Agda-to-Dedukti bridge and correspondence work; record that as missing instead of treating transport as an already available route.
Useful? React with 👍 / 👎.
PROOF-STATUS.adoc, PROOF-NEEDS.adoc and meta-checker/README.adoc conflicted with #482, #474, #472 and #471. Owner ruling: main's file is the base, this branch's unique content is salvaged, and main's row numbering stays (no R2a/R2b or R4a/R4b split). - PROOF-STATUS: adds this branch's theory census and §8.2 cone receipt, widened to the five Composition.agda theorems (R6, argued and ungraded until a receipt covers that module): PWG-3 10/15, ungraded 5/15. Adds the 2026-11-09 audit findings to R1 (four dispatch fail-open paths, integrity run after proving), R2 (verification/proofs/idris2 modules that prove less than their names) and R3 (PI-11, digest injectivity, PO-12). - PROOF-NEEDS and meta-checker/README: main's (this branch's E9 and postulate-count text is stale after #471). - DEBT.adoc cites R9, not R4b; EXPLAINME counts two theory results. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
Update 2026-11-10: merged with main after #482
#482 refreshed
docs/PROOF-STATUS.adocagainst the same policy sections, and the two conflicted in 11 places. The owner chose to keep main's text and salvage the rest (merge commitd82b69f):open, with the verifier placement unresolved, so the R3 change below no longer applies. Main's R12 SPARK row, its A5 list and its trust-kernel note are kept.ReceiptPWG table, the owner's 2026-11-09 transport-first decision for the R5 recheck legs, and everything that merged cleanly: the R4 receipt and §1 classification, the R10 model-versus-code note, the §6 toolchain deviation records, the meta-checker README, and the workflow andsetup-agda.shcomments.2ab7574, before fix(trust): one trust kernel; Level 4 needs a certificate, Level 5 needs two small kernels #477 retiredTrustKernelMonotonicity.idr.Cargo.lock,proof_search.rsand Zig changes are already on main, so they drop out of this diff.Summary (original)
docs/PROOF-STATUS.adocpredated two PROOF-POLICY amendments: §8 Proof Witness Grades (4 Nov) and §1.2 Creusot, Pearlite and Verus (7 Nov). It also understated two legs that CI already proves.Policy read at standards commit
b8f60511e76c9015d86990317162dce653c92fe1.Changes
ReceiptisPWG-3, with its Rocq and Lean legsopen/BRIDGE-PENDING.argued→proven. (Main makes the same change.)R3 (Lean):Superseded by main: R3 staysopen→proven-with-postulates.open.2ab7574(42551607796), and records the owner's §1 decision to split the meta-checker.clamp_trustand the Agda model differ, so the row is model-only.setup-agda.sh,dogfood-proofs-ci.ymlandidris2-abi-ci.yml. They are comments only, with nouses:changes, soactions.lockis unaffected.Testing
bash -n scripts/ci/setup-agda.shandcheck-workflow-duplicate-keys.shpass on the merge.2ab7574(Agda 13/13 under--safe --without-K --cubical-compatible, the meta-checker 9/9, the Lean build) are unchanged by the merge.🤖 Generated with Claude Code
https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4