Repository navigation
fix(proofs): fail the proof gate on Admitted, sorry and postulate (WO 1.3) - #57
Merged
Merged
Conversation
… 1.3) scripts/check-proofs.sh passed a Rocq file with Admitted and a Lean file with sorry, because it checked only that the file compiled. Each gated module that compiles is now audited as well (PROOF-POLICY 8.4, "Axioms travel with the grade"), and each audit fails closed when it cannot show that it ran: - Rocq: Print Assumptions for every Theorem, Lemma, Corollary, Proposition, Fact and Remark the file declares must print "Closed under the global context". - Lean: every theorem the source declares must depend on no axiom (Lean.collectAxioms, behind #print axioms). The lemmas Lean generates for an inductive (injEq, inj, sizeOf_spec) have no declaration range and are not witnesses. - Agda: --safe already refuses postulate. The comment-aware postulate scan of hyperpolymath/januskey (989a747, scripts/scan-postulates.sh, the reference gate PROOF-POLICY 8.4 names) now runs over the first-party modules of the import cone that agda --dependency-graph reports. tests/proofs/gate_controls_test.sh plants an Admitted, a sorry and a postulate. Each fails the new gate, and the Rocq and Lean ones pass the old gate, so the test detects the gap. A clean module passes. The Agda lane runs the Agda controls; the Rocq and Lean lanes come with WO 1.4. Checked locally with Rocq 8.18.0 and Lean 4.29.0 (the versions the pinned Guix gives) and Agda 2.6.3 with its distribution stdlib: all gated modules pass. Under Lean 4.29.0, simp brought propext into the two ApiResult laws of ApiTypes.lean, a template file; both now hold by rfl after cases. The gate and ApiTypes.lean are template files: the same fix belongs in rsr-template-repo. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM
|
hyperpolymath
marked this pull request as ready for review
November 10, 2026 18:29
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. |
|
Caution Review failedThe pull request is closed.
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. |
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
Work order 1.3 of
docs/proposals/mathesis-re-anchoring.adoc.scripts/check-proofs.shpassed a Rocq file withAdmittedand a Lean file withsorry, because it checked only that the file compiled. Now each gated module that compiles is also audited (PROOF-POLICY §8.4, "Axioms travel with the grade"). Each audit fails closed when it cannot show that it ran.Changes
Print Assumptionsfor each declared Theorem, Lemma, Corollary, Proposition, Fact and Remark must print "Closed under the global context".Lean.collectAxioms, the function behind#print axioms). The lemmas Lean generates for an inductive (injEq,inj,sizeOf_spec) have no declaration range, so they are not checked as witnesses.--safealready refusespostulate. The januskey postulate scan (scripts/scan-postulates.sh, the reference gate that §8.4 names) now runs over the first-party modules of the import cone thatagda --dependency-graphreports.tests/proofs/gate_controls_test.sh <prover>plants anAdmitted, asorryand apostulate. Each one fails the new gate. On the old gate, the Rocq and Lean controls pass, so the test detects the gap. A clean module with a decoy in a comment passes. The Agda lane runs it now; the Rocq and Lean lanes come with WO 1.4.ApiTypes.lean: under Lean 4.29.0 (the version in the pinned Guix),simpbroughtpropextinto the twoApiResultlaws. Both now hold byrflaftercases.The gate and
ApiTypes.leanare template files, so the same fix belongs in rsr-template-repo.RSR Quality Checklist
Required
Testing
Checked locally with Rocq 8.18.0, Lean 4.29.0 and Agda 2.6.3 (with its distribution stdlib):
bash scripts/check-proofs.sh agda|coq|lean4: PASS for every gated module.bash tests/proofs/gate_controls_test.sh agda|coq|lean4: both controls behave for each prover.just validate-repo-map: up to date.Generated by Claude Code