Repository navigation
Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii) - #34
Merged
Merged
Conversation
…des as PWG-3 PROOF-POLICY §2.1 names `agda --safe --without-K --cubical-compatible` as the canonical invocation, and §8.2 (owner ruling 2026-11-04) makes PWG-3 conditional on it. The gate lacked the flag (waiver W-1), so the proved rows were `ungraded` under §8, although PROOF-STATUS said "mathesis Grade 3". The last blocker was 13 `-WUnsupportedIndexedMatch` warnings: the proofs matched `exec fuel c s ≡ just t` against `refl`, which needs injectivity of `just`. W-1 said only a relational semantics would remove them, at the cost of restating N-5. That was unnecessary. SecretTypes.Prelude now defines `from-just` and `just-injective e = cong (from-just a) e`, a retraction (the same move `suc-dec` makes with `pred`), and Noninterference.Generic routes the six affected clauses through one helper, `≈-just`. The semantics, N-5 and every theorem statement are unchanged. - scripts/proof-flags.sh: adds --cubical-compatible to the single flag set. check.sh, minimal-laws.sh and the receipt all read it. - Receipt renamed agda-grade3_praxis.deed to agda-pwg_praxis.deed. It records `cubical-compatible "met"` and a §8.5 `:pwg` per claim: 3 for the theorems, n/a for the checked demonstrations (§8.1). - PROOF-STATUS, README, EXPLAINME and proof-debt now say PWG-3, never a bare grade. W-1 is recorded closed, with the history and the corrected arm. The Rocq and Lean legs stay `unavailable`, and PWG-3 is stated not to discharge them (§8.4). Checked locally on Agda 2.6.4.3: scripts/check.sh (core proofs, all 4 expected rejections at their intended declarations), scripts/minimal-laws.sh (3 laws, each needed), grade-receipt.sh --check (15 modules), and DEED lint of the new receipt against standards@8e48b1c. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
…o Canon lockstep goes green here) Canon lockstep is red on main. standards' canon.lock records 2.1.5 (#1424: gate table 0.3.1 and the applicability policy changed; the criteria did not), and this deed declared 2.1.3. Port of hyperpolymath/rsr-template-repo#298, the spine's adoption. - secret-types_chora.deed (canon): :version 2.1.3 to 2.1.5, and :gates-sha256 2f31f46d… to 5c510bba…. The criteria hash is unchanged. The (provenance) clause keeps 2.1.3: it records the canon this repository was minted against, which is history. - tests/workflows/governance_policy_test.sh expects the 2.1.5 tuple. That test already fails on main earlier, on the governance.yml pull_request filter that #15's caller carries; this does not change that. canon.lock marks 2.1.5 status "draft"; this adopts the identity the lock records, which is what the lockstep gate compares. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
PROOF-POLICY §2 asks for every Agda theory proof to be rechecked in Rocq and in Lean, transport first and hand re-proof as the fallback. Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and there is no released Dedukti/Lambdapi exporter to Lean 4. So both legs are hand re-proofs: - verification/legs/rocq/SecretTypes.v: Coq 8.18.0, prelude only (no Require); 11 theorems, Print Assumptions "Closed under the global context" for each. - verification/legs/lean/: Lean 4.24.0, core only (no require, no Mathlib); 11 theorems, #print axioms "does not depend on any axioms". exec is defined structurally through run, so no well-founded recursion brings in propext. - scripts/check-legs.sh pins both checkers, refuses any library, any sorry/admit/Admitted/Axiom/Parameter, and any axiom line that is not clean. CI runs it as the new legs job (Coq by Ubuntu package version, Lean by release tarball sha256). - verification/legs/README.adoc is the §2.2 correspondence record: route and reason, versions, invocations, universe discipline, the statement comparison (exec, Option, the Signature/Lattice split, Observer, Vars) and the claim-by-claim name map, state RECONCILED. The comparison is provisional until owner review. - The receipt gains a (legs) block (pins, invocations, axioms, sha256 of every leg input) and the claims move to re-proved/re-proved at PWG-2ii; grade-receipt.sh refuses a counted leg without a correspondence row, and the reverse. - PROOF-STATUS, README, EXPLAINME and proof-debt follow. Not PWG-1: no per-commit receipt of each checker's observed result yet. Not +foundation-diverse: all three provers are dependent type theories. No Agda module or statement changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
lean-toolchain cannot carry one: Lean reads the whole file as the toolchain name. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
…des as PROOF-POLICY §8 PWG PROOF-POLICY §2.1 names `agda --safe --without-K --cubical-compatible` as the canonical invocation; waiver W-1 kept the flag off, on the belief that only a relational big-step semantics could remove the last 13 warnings (`just`-injectivity in Noninterference.Generic). That belief was wrong: - Prelude: `just-inj` defined by `cong` through the computing projection `from-just`, which needs no unification rule. - Noninterference.Generic: the six clauses that matched `refl` against `exec … ≡ just t` now carry agreement along `just-inj` (`just-≈`, `just-≈₂`). No statement, semantics or fixture changed. - scripts/proof-flags.sh: `--cubical-compatible` added. Gate, laws certificate and receipt all run under it. - tests/flag-control/IndexedMatch.agda + scripts/check.sh: a correct proof that only the flag refuses; the gate fails if it is ever accepted. Removing the flag was tested to fail the gate. The relational route would not have sufficed on its own: a probe proving determinism of `c , s ⇓ t` raised 22 UnsupportedIndexedMatch warnings (inverting two derivations of one command needs Cmd injectivity). Grades: "mathesis Grade 3" was the unratified brief's wording. PROOF-POLICY §8 (2026-11-04) supersedes it and makes PWG-3 depend on the §2.1 invocation, so the theorems were `ungraded` while W-1 was open; they are PWG-3 now. The receipt carries the §8.5 fields (pwg, foundation-diverse, per-leg route, token and §2.2 state), derives the grade from leg states (tested: one RECONCILED leg -> 2i, two -> 2ii, BRIDGE-PENDING does not count), pins the PROOF-POLICY commit (§7), and moves from agda-grade3_praxis.deed to agda_praxis.deed because a grade is derived and can change. EXPLAINME listed --cubical-compatible as a checker flag while it was waived; that line is now true. README's Lintel pin corrected (ee01db4 -> d1d843b). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP
A list-item continuation beginning "11. The prelude's ..." parsed as an ordered list (asciidoctor: list item index: expected 1, got 11), which check-adoc-renders.sh fails. Rewrapped; the text is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
The owner chose #32 as the base for the cubical-compatible change, so this branch now builds on it instead of #26. - Proof code, proof-flags.sh: #32's version (Prelude.just-inj, tests/flag-control/IndexedMatch.agda). The legs do not depend on the Agda helper names. - Receipt: verification/receipts/agda_praxis.deed (#32's name), written by grade-receipt.sh --write. #32 derives each PWG from the legs' §2.2 states, so N-1..3 and N-7..9 now carry route re-proved and state RECONCILED for both legs, and their grade derives as 2ii. A RECONCILED leg's token is proven. This branch's (legs) block, leg input hashes and the correspondence-record check are carried over. - proofs.yml: #32's receipt step plus this branch's legs job. - PROOF-STATUS, README, EXPLAINME, proof-debt: #32's wording, with this branch's leg facts and the new receipt path. Checked locally with Agda 2.6.4.3, Coq 8.18.0 and Lean 4.24.0: check.sh (core proofs, 4 rejections, flag control), minimal-laws.sh, check-legs.sh (both legs), grade-receipt.sh --check (15 modules), check-escape-hatches.sh and the invisible-character scan. Negative control: removing the N-9 row from verification/legs/README.adoc makes grade-receipt.sh --check fail with "only in grade-receipt.sh: N-9". check-adoc-renders.sh was not run here (no asciidoctor in this session). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>
My earlier merge (ba2484f) took #32's head before #32 was updated (3bf7f8e), because the local ref was stale. So this branch lacked main's later changes (the template sync #28, canon 2.1.5 #27, https-only edges #25) and kept some #26-only text. This merge corrects that. Each conflicted file is a 3-way merge on 3bf7f8e (the #32 commit the earlier merge used), so only this PR's legs changes are carried onto main. Files the legs work does not own take main's version: tests/workflows/governance_policy_test.sh, and docs/proof-debt.adoc except its legs bullet (this restores #32's dated W-1 record). The receipt is regenerated. The diff against main is now the legs work: the Rocq and Lean sources, check-legs.sh, the legs CI job, the receipt's (legs) block and RECONCILED leg states (PWG-2ii derived), and the matching doc lines. Checked with Agda 2.6.4.3, Coq 8.18.0 and Lean 4.24.0: check.sh, minimal-laws.sh, check-legs.sh, grade-receipt.sh --check (15 modules), check-escape-hatches.sh, the invisible-character scan and tests/workflows/governance_policy_test.sh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>
6 tasks done
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 50 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. |
9 of 10 tasks
|
🟠 indeterminate · the verdict grid could not be rendered · The renderer pinned in metadatastician/standards@8e48b1caade0 was missing or did not match its recorded sha256. Orange means the evidence for this lane was unavailable, not that the repository passed. |
S7688 (4, check-legs.sh): the version-pin and axiom-count tests use [[ ]] instead of [ ]. S7679 (grade-receipt.sh): leg_token reads its argument into a local variable. Behaviour is unchanged. Checked: check-legs.sh passes (Coq 8.18.0, Lean 4.24.0), and with the Lean pin set to a wrong version it still exits 2. grade-receipt.sh --check passes (15 modules). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>
|
Owner
Author
|
It fails in the verdict-grid lane suite with Cause: This PR touches neither file. No fix exists yet: the choice is between adopting the template's inline The orange verdict-grid comment above ("the renderer pinned in metadatastician/standards@8e48b1c was missing or did not match its recorded sha256") is also about the repository's workflow pins, not about this diff. Generated by Claude Code |
hyperpolymath
marked this pull request as ready for review
November 10, 2026 19:10
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. |
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 replaces #29, on the same branch. #29 was stacked on #26, and GitHub refuses to move a stacked PR's base. #26 is superseded by #30 and #32, which are both on
main, so this PR targetsmaindirectly.It adds the two recheck legs that
PROOF-POLICY§2 asks for, Rocq and Lean, for every proved theory claim: N-1, N-2, N-3, N-7, N-8 and N-9. They are hand re-proofs, because transport is not available: Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and no Dedukti or Lambdapi exporter to Lean 4 has been released. Both legs check with no library and no axioms, and the statements are compared in a §2.2 record.main(#32) derives each grade from the legs' §2.2 states, and onlyRECONCILEDcounts. With both legsRECONCILED, the 6 claims derivePWG-2ii.For the owner to review (doctrine 4): the statement comparison in
verification/legs/README.adocwas written by Claude Code and is labelled provisional until you review it. No tool checks it. ThePWG-2iigrade rests on it.Changes
verification/legs/rocq/SecretTypes.v: Coq 8.18.0, prelude only, with noRequire. 11 theorems.Print Assumptionsreports "Closed under the global context" for each.verification/legs/lean/: Lean 4.24.0, core only (the lakefile has norequire, so no Mathlib). 11 theorems.#print axiomsreports "does not depend on any axioms" for each.execis defined structurally throughrun, so no well-founded recursion brings inpropext.scripts/check-legs.sh: pins both checker versions, refuses any library and anysorry,admit,Admitted,AxiomorParameter, and fails unless all 22 axiom lines are clean..github/workflows/proofs.yml: newlegsjob. Coq is pinned by its Ubuntu package version, Lean by the sha256 of its release tarball. It uses only the already-lockedactions/checkoutpin.verification/legs/README.adoc: the §2.2 correspondence record (route and reason, versions and invocations, residual assumptions (none), universe discipline, a point-by-point statement comparison, and a claim-by-claim map from each Agda name to its Lean and Rocq names). State:RECONCILED.scripts/grade-receipt.shandverification/receipts/agda_praxis.deed:re-provedand stateRECONCILEDfor both legs, so their grade derives as2ii; aRECONCILEDleg's token isproven;(legs)block: pins, invocations, axioms, and the sha256 of every leg input;RECONCILEDleg without a row in the correspondence record, and the reverse.PROOF-STATUS.adoc,README.adoc,docs/EXPLAINME.adoc,docs/proof-debt.adoc: the new grade and legs. NotPWG-1: no per-commit receipt captures each checker's observed result yet. Not foundation-diverse: Agda, Rocq and Lean are all dependent type theories.RSR Quality Checklist
Required
check.sh(core proofs, 4 expected rejections, flag control),minimal-laws.sh,check-legs.sh,grade-receipt.sh --check(15 modules),check-escape-hatches.sh, the invisible-character scan,tests/workflows/governance_policy_test.sh, andtests/e2e/use_template_mint_test.sh(self-skips: this is a minted tree).lake-manifest.jsonis git-ignored.check-legs.shrefusessorry,admit,Admitted,AxiomandParameter.lean-toolchain, which Lean reads whole as the toolchain name.As Applicable
Testing
Negative controls:
verification/legs/README.adocmakesgrade-receipt.sh --checkfail withonly in grade-receipt.sh: N-9.Not run locally:
scripts/check-adoc-renders.sh(no asciidoctor in the authoring session). CI runs it.Generated by Claude Code