Repository navigation
proof(actions-lock): Idris2 closure model with the corpus verdicts as equations - #1026
Open
hyperpolymath wants to merge 5 commits into
Open
hyperpolymath wants to merge 5 commits into
hyperpolymath wants to merge 5 commits into
Conversation
… equations standards#963 criterion 5 left closure with Hypatia as the authority and a shared five-row corpus binding it to standards' close-lock.sh --check. That corpus is test evidence. This adds the formal half that PROOF-POLICY §1 assigns to an engineering property of one wire format: Idris2. verification/proofs/idris2/ActionsLockClosure.idr models a lock as its workflow refs plus its records (key, nested uses) over any type with decidable equality, and proves: - closedIffNoDangling: closed exactly when the dangling list is empty; - danglingSound / danglingComplete: the reported list is exactly the named refs without a record; - decClosed: closure is decidable. The five corpus rows are transcribed into the model and their verdicts are Refl equations (rowClosedV00x, rowClosedCaseVariant, rowDanglingNested, rowDanglingWorkflowRef). If expected.tsv and the model ever disagree, this file stops type-checking. PROOF-STATUS records three rows with honest tokens: - the model is OPEN until Verify Proofs' idris2 --check receipt is recorded (no idris2 in this session; the CI lane is the checker); - the Elixir and Bash implementations are TESTED against the corpus, with bounds (5 locks, 6 refs); - the owner/repo fold at the parse boundary is ASSUMED in the model and TESTED by closed-case-variant.lock. Runtime refinement is not claimed. Engineering proofs carry no PWG. scripts/check-proof-status.sh: 42 files, 77 identifiers, 0 mismatches. No believe_me / assert_total / postulate in the new file. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi
The owner ruling of 2026-11-04 adopted the Mathesis grade ladder as standards' PROOF-POLICY §8, the normative source. That ruling forbids a bare "Grade 3" or "Grade 2" in a status line, because it collides with the CRG/TRG/ARG/FRG letter grades and with ECHIDNA's TrustLevel, which counts the other way. This file still cited the Mathesis brief as the definition and wrote "Grade 3" five times. - The policy bullet now cites §8 as normative and the brief as provenance. It states PWG-3, PWG-2i, PWG-2ii and PWG-1, says lower is stronger, and says engineering proofs carry §5 tokens only. - LogtalkMigration.agda is relabelled PWG-3 in its row, in P8 and in the coverage map. Its recorded receipt already met PWG-3: pinned Agda 2.8.0.2, the §2.1 flags, builtins only, success at a recorded commit. The import cone, builtins only with zero postulates under --safe, is now stated explicitly. No grade moved. scripts/check-proof-status.sh agrees with the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi
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 23 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: 83c2334ea6
ℹ️ 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".
Codex review on #1026 raised two P2 findings: 1. The closure file claimed it would stop checking if the model and expected.tsv disagreed. Nothing tied its hand-transcribed rows to the fixtures or the table, so changing both together could leave every Refl green. The corpus test now reads the model file's ref table and its new `-- corpus: <fixture> <row>` lines, and checks three things: - the model names exactly the corpus locks; - each fixture's workflow refs and records (with nested uses), after the owner/repo fold, equal its MkLock row; - each expected.tsv row equals the model's equation for that row. The type checker binds the equations to the model, so drift on either side now fails one of the two checks. 2. The doc comment on `dangling` said it is what Hypatia's error payload carries. That is false in general: ActionsLock checks workflow refs before nested uses, stops at the first failing phase, and reports (source, ref) pairs. The comment now says so. The model's list is the set close-lock.sh --check prints, and Hypatia reports a subset of it when a lock is missing refs of both kinds. PROOF-STATUS says the same. Verification, run standalone because hex.pm is unreachable: - the corpus test passes 17/17; - a mutant transcription (danglingNested's nested uses changed) fails exactly that row's edge test; - a mutant equation (danglingNested = [5]) fails exactly that row's equation test; - the formatter leaves the test unchanged; - check-proof-status.sh agrees with the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi
|
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. |
Verify Proofs run 42623006244, job 129179628830: Idris 2 0.7.0 (from source, Chez Scheme 10.0.0+dfsg-5build1) type-checked verification/proofs/idris2/ActionsLockClosure.idr under %default total, at source commit 71d1160, as the PR merge commit 8db0f43 on main c639c46. The model row moves from OPEN to PROVEN, model only; runtime refinement is still not claimed. The implementation rows stay TESTED and the parse-boundary row stays ASSUMED. Only this document changes. The .idr is byte-identical to the checked commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi
|
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. |
check-proof-status.sh reads `+...+` spans that name a file as paths. The receipt wrote `+idris2 --check ActionsLockClosure.idr+`, which no tree path matches, so the currency check went red. The receipt now writes `+idris2 --check+` on this file. The check passes again: 42 files, 77 identifiers, 0 mismatches. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi
|
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. |
|
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 23:07
hyperpolymath
added a commit
to metadatastician/standards
that referenced
this pull request
Nov 9, 2026
…ons (#1432) This fixes a self-review finding on #1318, which became visible after #1420 rewrote `close-lock.sh`. It also records this thread's gate obligations in the repository's proof ledger. ## 1. An unreadable lock is UNEXAMINED, not a dangling edge (`b5077c8`, `dd2af9f`) `lock-selfcheck.sh` treated every non-zero exit of `close-lock.sh --check` as dangling edges. The two exit codes mean different things: - **Exit 1:** the lock has dangling edges. - **Exit 2:** the closure was never examined. That happens when there is no lock, when the strict parser from #1420 refuses the lock (duplicate keys, multiple documents), or when `yq`/`jq` is missing. The exit-2 case was reported as `POISON — 1 dangling edge(s)`, which named the wrong cause. It already failed closed, so no unsafe SHA passed. - **`scripts/lock-selfcheck.sh`:** - Exit 1 still lists the dangling refs. - Any other non-zero exit now gives `VERDICT: UNEXAMINED — close-lock.sh --check exited N`, followed by close-lock's message. - An unparseable workflow and an unreadable lock are independent causes, so each gets its own UNEXAMINED verdict (CodeRabbit). Either one still fails the SHA. - **`.githooks/pre-commit`:** the message now says "failed the closure check", because close-lock's output above it names the cause. - **Tests:** - `lock-selfcheck-test` passes 11/11. - `expect` now also takes strings that must be absent. The unreadable-lock case asserts close-lock's diagnostic and that no `VERDICT: POISON` appears. A new case covers both UNEXAMINED causes at once. - The old script fails the new cases. - `close-lock-test` passes 74/74, and `lock-selfcheck.sh HEAD` reports SELF-CONSISTENT. ## 2. Gate obligations in `3-practice/PROOF-NEEDS.adoc` #1436 rewrote this file as a proof ledger. This branch merges that and adds a **Gate obligations** table in the ledger's own columns. The census is updated to 18 rows: 2 proven, 1 argued, 3 tested-only and 12 open. | Obligation | Status | Bounds | |---|---|---| | `close-lock.sh --check` closure | tested-only | 5 corpus locks, 6 refs | | `lock-selfcheck.sh` verdicts | tested-only | 11 cases; a workflow with no lock entry is deliberately outside the verdict (narrowed after Codex review) | | panic-attack `scope-excludes` partition | tested-only | 3 cases | All three tests run in the Self Test workflow, through `scripts/run-shell-test-suite.sh`. The formal closure model belongs to Hypatia, the closure authority. hyperpolymath/hypatia#1026 adds `ActionsLockClosure.idr`, which evaluates the same corpus rows as equations, and Hypatia's `PROOF-STATUS.adoc` records its status. No PWG grade applies, because these are engineering obligations (§8.1). ## Known red: `Call CI Pipeline / Nickel` This failure is not from this PR. A file under `9-archive/` is not formatted, and the same check is red on every recent PR. The proposed fix is to exclude `9-archive/` from that check's file list, in a separate PR. No licence content is touched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
disabled auto-merge
November 10, 2026 01:46
This branch has not been deployed
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.
Formal half of standards#963 criterion 5. That decision kept Hypatia as the authority for
actions.lockclosure, with standards'close-lock.sh --checkbound to it through a shared five-row corpus (#941). The corpus is test evidence. Under PROOF-POLICY §1, an engineering property of one wire format belongs in Idris2, so this PR adds the model.verification/proofs/idris2/ActionsLockClosure.idrThe model represents a lock as its workflow refs plus its records (each a key with its nested
uses:), over any type with decidable equality. It proves:closedIffNoDanglingdanglingSounddanglingCompletedecClosedThe five corpus locks are transcribed into the model, and each verdict is a
Reflequation that includes the exact dangling refs.The file has
%default totaland nobelieve_me,assert_totalorpostulate.Receipt. Idris 2 0.7.0, built from source on Chez Scheme 10.0.0+dfsg-5build1, ran
idris2 --checkon this file successfully. That was Verify Proofs run 42623006244, job 129179628830, on source commit71d1160, checked as the merge commit8db0f43on mainc639c46. The commits after that change onlyPROOF-STATUS.adoc.Binding the transcription to the corpus (Codex review,
71d1160)The type checker cannot read the fixtures. So
test/rules/actions_lock_closure_corpus_test.exsreads this file's ref table and its-- corpus: <fixture> <row>lines, and checks three things:MkLockrow;expected.tsvrow equals the model's equation for that row.A mutant transcription fails exactly that row's edge test, and a mutant equation fails exactly its equation test.
The comment on
danglingnow states Hypatia's actual behaviour: it checks workflow refs before nesteduses:, stops at the first failing phase, and reports(source, ref)pairs. So for a lock missing refs of both kinds it reports a subset of this list.verification/PROOF-STATUS.adocThese rows use §5 tokens only, since engineering proofs carry no PWG:
ActionsLock.parse/1and Bashclose-lock.sh --checkagainst the modelclosed-case-variant.lock.A separate commit applies standards PROOF-POLICY §8 (owner ruling 2026-11-04):
PWG-3.LogtalkMigration.agda: its existing receipt already metPWG-3, so no grade moved. Its import cone is now stated explicitly.Checks
scripts/check-proof-status.sh: 42 files and 77 identifiers, with no mismatches.ActionsLock.parse/1and standards'close-lock.sh --check: both reproduceexpected.tsv.No licence content is touched.
🤖 Generated with Claude Code
https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi