Repository navigation
docs(proofs): bring PROOF-STATUS up to PROOF-POLICY §1.2, §6 and §8 - #474
hyperpolymath wants to merge 7 commits into
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
|
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 36 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. |
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
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. This PR is the first in a stacked series. The later ones split the meta-checker under §1, add Verus/Creusot contracts on the Rust, and do the Rocq/Lean rechecks.Policy read at standards commit
b8f60511e76c9015d86990317162dce653c92fe1.Changes
ReceiptisPWG-3, with its Rocq and Lean legsopen/BRIDGE-PENDING.argued→proven. Cites the Dogfood Idris2 (verification) job (127501094018). It builds all 11 modules ofechidna-verif-proofs.ipkg.open→proven-with-postulates.Lean.collectAxiomsover every theorem: 167 theorems; 109 use no axiom; 58 use onlypropext,Quot.soundandClassical.choice. There is nosorryAxand no project axiom.2ab7574(42551607796). It also records the owner's §1 decision: onlyReceiptis theory, and the rest of the meta-checker is split into parametric Agda theory plus Idris 2 specs, with the Rust then verified by Creusot/Pearlite and Verus.clamp_trustexists in the Rust, so the row is model-only. The module header's "no idris2 in CI" reason is out of date.setup-agda.sh,dogfood-proofs-ci.ymlandidris2-abi-ci.yml. They are comments only, with nouses:changes, soactions.lockis unaffected.RSR Quality Checklist
Required
actionlintwith shellcheck clean on both workflows;bash -nonsetup-agda.shunsafeblocks without// SAFETY:comments: n/a.envfiles includedAs Applicable
docs/decisions// proof ledger updated: PROOF-STATUS is the §5 ledgerTesting
Local rechecks on main
2ab7574(2026-11-09):scripts/ci/check-agda.sh(Agda 2.7.0.1, executable sha2566de41437…, stdlib v2.1 @97bc55e)UnsupportedIndexedMatchat the same 6 sites; receipt controls accept 2, reject 3proofs/agdaunder--safe --without-K --cubical-compatiblelake build+ axiom census2ab7574vs the 2026-11-04 receipttest-issue-regressions.sh,check-allow-fail-expiry.sh,check-workflow-duplicate-keys.sh,check-lock-sync.shasciidoctor --failure-level WARN docs/PROOF-STATUS.adocOne local deviation, recorded in the file: this session's network refuses
codeload.github.com, so stdlib was fetched by its git tag rather than by the archive digest. It affects only the local corroboration; the hosted receipt is unaffected.Generated by Claude Code