Repository navigation
feat(proofs): faithful trust-rule model in Agda with a Rocq recheck - #484
hyperpolymath wants to merge 2 commits into
Conversation
Echidna.TrustRule transcribes compute_trust_level from src/rust/verification/confidence.rs: separate certificate flags, the confirming-prover count, and the four rules in Rust order. It proves the two Level1 guards, what Level5 requires, and monotonicity in every factor. It is in the MetaChecker closure, so agda-meta-checker.yml checks it with the section 2.1 flags. The existing Dispatch.compute-trust model is not faithful: with two confirming provers and no certificate, Rust returns Level3 and the model returns Level2. dispatch-model-diverges states this as a theorem; the older model is left in place. verification/proofs/rocq/TrustRule.v re-proves the same statements. just proofs-verif-rocq compiles it and fails unless Print Assumptions reports every theorem closed; just proofs-coq, which the CI Coq job runs, now depends on it. The Lean leg is open. Two findings in the Rust rule are recorded in PROOF-STATUS R12 for an owner decision, not changed here: Level5 does not enforce "2+ small-kernel provers", and Level4/5 do not check has_certificate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16
|
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 27 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. |
|
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: dbeb616e33
ℹ️ 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".
proofs-verif-rocq took theorem names from unindented Theorem/Lemma lines and ran Print Assumptions on each. An admitted Fact, Corollary, Remark or indented lemma was never checked, and a file with no matching line passed vacuously. The recipe now runs coqchk -o, Rocq's separate checker kernel, over every compiled library. Its context summary lists each Axiom, Parameter and Admitted declaration whatever its keyword or position, and whether or not a theorem uses it. The recipe requires all four "relying on" lines to read <none>; any other output, including none, fails. Checked: the real file passes; an indented admitted Fact, an admitted Corollary, an Axiom, and an admitted Remark in a section each fail; a coqchk that prints nothing or exits non-zero fails. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16
|
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. |
|
|
Closing. Generated by Claude Code |
Pull request was closed
Summary
The meta-checker's
Dispatch.compute-trustis not a faithful model of the Rustcompute_trust_level(src/rust/verification/confidence.rs). Given two confirming provers and no certificate, Rust returns Level3 and the model returns Level2. The model also uses one flag for both "certificate produced" and "certificate verified". The existing theorems hold for the model, but they do not carry over to the Rust code on that input.This PR adds a model that follows the Rust code line for line and proves it in Agda. It then re-proves the same statements in Rocq: the first Rocq leg under PROOF-POLICY §2. It is new ledger row R12.
Changes
meta-checker/src/Echidna/TrustRule.agda(new, part of theMetaCheckerclosure)dangerous-gives-level1andintegrity-failure-gives-level1;level5-sound;compute-mono, monotone in every factor;level5-without-certificateanddispatch-model-diverges.UnsupportedIndexedMatchwarning: equality and order proofs are matched only in absurd clauses, or through stdlib≤-pred.verification/proofs/rocq/TrustRule.v(new): re-proves the same statements under the same names.Justfile:proofs-verif-rocq. It compiles each file in a temporary directory, then runscoqchk -o(Rocq's separate checker kernel) over the compiled libraries. It fails unless coqchk reports no axioms and no unsafe flags. EveryAxiom,ParameterorAdmitteddeclaration counts, whatever its keyword or position and whether or not a theorem uses it.proofs-coq(the CI Coq job) now depends on it.proofsaggregate includes it.dogfood-proofs-ci.yml:verification/proofs/rocq/**added to the push and pull_request path filters. Nouses:change, soactions.lockis untouched.docs/PROOF-STATUS.adoc:provenfor the model.argued.COQ-CHECKEDandBRIDGE-PENDING.open.CHANGELOG.adoc: an Unreleased entry.Findings in the Rust code (owner decision, not changed here)
TrustFactorscarries only the primary prover's kernel and a count of agreeing provers, so that condition is never checked.certificate_verifiedbut nothas_certificate. So a verified flag with no certificate behind it reaches Level5 (level5-without-certificate).RSR Quality Checklist
Required
just testwas not run: no Rust is touched. The proof recipes were run (see Testing).--failure-level WARNis clean on both.adocfiles.unsafeblocks.postulate,TERMINATING,Admittedoradmitin the new files.As Applicable
CHANGELOGupdated.docs/PROOF-STATUS.adoc).Testing
These are session checks, not receipts. The session toolchains are older than CI's:
agda --safe --without-K --cubical-compatibleonEchidna/MetaChecker.agda, fresh interfacesTrustRuleLevel2 != Level3inrule-mono-skjust proofs-verif-rocqAxioms: <none>Fact, an admittedCorollary, anAxiom, an admittedRemarkin aSectioncoqchkstub that prints nothing, or exits 3just proofs-coq, the CI Coq job's commandCI checks the Agda side with Agda 2.7.0.1 and stdlib 2.1 (
agda-meta-checker.yml), which I could not run here. Watch that job:Data.Nat.Properties.≤-predis the one new stdlib import.No Lean toolchain could be run in this environment, so the Lean leg is still open.
🤖 Generated with Claude Code
https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16