Repository navigation
CI: the lock is accepted at job setup again (required checks, Scorecard) - #34
Merged
Merged
Conversation
#33 locked scorecard.yml's call into hyperpolymath/standards as `standards@main`, fixed at one commit, with no list of the actions that reusable workflow uses. Push and manual runs still passed, but every scheduled run since (2026-10-16 to 2026-10-19) died at job setup: "lockfile verification did not produce a result for this action ... github/codeql-action@b96794f0: invalid lockfile pin". Before #33 the scheduled run got through setup. scorecard.yml now calls scorecard-reusable.yml at standards 75bd599, the commit a manual run on main passed with on 2026-10-19 (run 39247942827). Its lock record lists the four actions the reusable workflow uses, as the standards lock does for that file, and the two not yet recorded here (upload-artifact v7.0.2, scorecard-action v2.4.4) get records copied from the standards lock. The `standards@main` record goes. The lock header no longer says 36 workflows or cites a script this repository does not have. The lock is sorted with no dangling or unused entries; actionlint is clean; the documentation guard and 27 tests pass. A scheduled run can only be exercised on main, so the first 04:10 UTC run after merge is the decisive check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
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 34 minutes. View limit details
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info
📝 Walkthrough
Merge Risk: ⚪ Minimal · up to
|
| Check name | Status | Explanation |
|---|---|---|
| Description Check |  |
Check skipped - CodeRabbit’s high-level summary is enabled. |
| Docstring Coverage | |
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0… |
| Linked Issues check | |
Check skipped because no linked issues were found for this pull request. |
| Out of Scope Changes check | |
Check skipped because no linked issues were found for this pull request. |
| Title check | |
The title clearly identifies the CI lockfile and Scorecard job-setup fix, which matches the main change. |
Full details: Docstring Coverage
-
Explanation
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0 files. (1 skipped: 1 unsupported.)
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Warning
CI annotation context is incomplete: annotation collection unavailable or limited
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.
Comment @coderabbitai help to get the list of available commands.
hyperpolymath
marked this pull request as ready for review
October 19, 2026 12:13
Codex Review SummaryThis 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. |
Every job that resolves actions/checkout from this lock now dies at job setup: "Unable to resolve action actions/checkout@3d3c42e5: invalid lockfile pin". That covers the required Agda proof gate and scan / gitleaks, on this PR and on main (a manual run of proofs.yml on main at f5a4177 failed the same way today, run 39251522875; the same commit passed on 2026-10-15). The scheduled Scorecard failures since 2026-10-16 are the same error on the codeql-action record. Both records repeat the SHA as `ref`: checkout since #33, which changed it from 'v7.0.1', and codeql-action since #31. The standards lock, which gh actions-lock writes, records these SHA-keyed actions with their release tags as `ref` ('v7.0.1', 'v4.38.0'), and this lock did so for checkout until #33. Both records get their tags back; git ls-remote confirms v7.0.1 is 3d3c42e5 and v4.38.0 peels to b96794f0. The untagged workflow pins (cicd-suite, standards) keep the SHA as `ref`, as in the standards lock; the estate audit resolved its record fine on this PR. The lock stays sorted with no dangling or unused entries; the documentation guard passes. This PR's own runs are the check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
hyperpolymath
changed the title
With the refs fixed, the Agda gate and CodeQL get past job setup, but the three scan / * jobs (scan / gitleaks is required) still die there: "Unable to resolve action actions/checkout@3d3c42e5: invalid lockfile pin". That checkout is nested in secret-scanner-reusable.yml, and the metadatastician/standards@94572e6 record lists no nested actions. The Scorecard record, which lists its four, got past setup on this PR. The record now lists actions/checkout@3d3c42e5, the one action that workflow uses at 94572e6, as the standards lock at that commit records for it. The lock header says why such lists are needed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
The record's nested list did not help: scan / gitleaks (required), rust-secrets and shell-secrets still died at job setup on checkout. The actions a reusable workflow uses are resolved against the called repository's lock at the pinned commit, and the standards lock at 94572e6 records checkout and codeql-action with the SHA repeated as `ref`, the form job setup now refuses. At 75bd599 the standards lock records their tags, and Scorecard, pinned there, passes job setup on this PR. secret-scanner.yml moves to 75bd599. Between the two commits secret-scanner-reusable.yml changed only in its header, which now says callers must not pass `secrets: inherit`: the workflow declares and reads no secrets, and inherit forwards every secret the caller can see (CWE-250, standards#1108 6b). The caller drops it, and its own comment claiming inherit was required. The 94572e6 record goes; the 75bd599 record already lists checkout. The lock header now states the rule as observed, and scorecard.yml points to it. Lock sorted, no dangling or unused entries; actionlint clean; the documentation guard passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
|
7 of 13 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 19, 2026
…35) ## Summary Ladder increment I3a: asynchrony. The first commit is the pre-registration (`docs/pre-registration-addendum-2026-10-19.adoc`). It fixes the model, the accounting, the reading of the 2026-10-12 falsifier, and claims Y-1 to Y-8 with their falsifiers, before any proof. The second commit is the proofs. **All eight claims came out as pre-registered.** The headline: **K-CUT-LOSS survives asynchrony unchanged, and the transport half of K-CUT-WARRANT becomes directional.** - The receiver of a message knows it was sent. - Its sender does not know it was received, at any world where the receiver has done nothing since. In the synchronous frame the same proposition is a theorem. - A reply restores the sender's knowledge. That is the falsifier pre-registered on 2026-10-12, confirmed. ## Type of change - [ ] 🐛 Bug fix - [x] ✨ New feature - [ ] 🕳️ Soundness fix - [x] 📖 Documentation - [ ] 🔧 Build / CI / tooling - [ ] ♻️ Refactor - [ ] 🔒 Security - [ ] 🧪 Tests only ## What is proved | Row | Claim | Where | |---|---|---| | Y-1 | Synchronous cuts are exactly the asynchronous cuts with nothing in flight (embed/complete are inverse on them), and projection, consistency, causality and the restricted grade agree there | `Async.agda` | | Y-2 | Asynchronous K-CUT-LOSS: `grade↾ₐ p G κ ≡ lgrade (aview p G κ)` for every causal cut consistent for p. The sender pays at send, the receiver at receipt. Parametric, discharged at Loss/MaxPlus/HWM, from the same two laws as K-1 | `Async.agda`, `Instances.agda`; `scripts/minimal-laws.sh` now also checks `Async.agda` | | Y-3 | Delivering a message or selection in flight changes only its receiver's local cut | `Async.agda` | | Y-4 | In the asynchronous frame, LOSS ⇒ WARRANT (a `SoundWarrant` in epistemic-types' interface) and knowledge of the own frontier survive | `AsyncKnowledge.agda` | | Y-5 | The receiver of a protocol's first message knows it was delivered, hence sent | `AsyncKnowledge.agda` | | Y-6 | Its sender does not know it was received while the receiver has done nothing since. The synchronous frame proves the opposite | `AsyncKnowledge.agda`, `Instances.agda`, `tests/reject/SenderKnowsReceipt.agda` | | Y-7 | Both bounds (W-4, W-5) survive against the sent-so-far grade, the completion's; discharged as W-6 | `AsyncBound.agda`, `Instances.agda` | | Y-8 | In `0 → 1 : a . 1 → 0 : b`, a received reply gives the sender knowledge of receipt; a reply in flight does not (any algebra, any grades) | `Instances.agda` | PROOF-STATUS gains the "Asynchrony" section and a short "What Y-6 says about the keystone". README, EXPLAINME, ARCHITECTURE and the changelog no longer list asynchrony as open. Each now says what remains: the position-indexed form of Y-5/Y-6, the general form of Y-8 (message chains), queues as data, and asynchrony with recursion. ## How has this been verified? All of the following were re-run on this branch after it was rebuilt on `main` at `08f8f00`. - `scripts/check.sh`, locally in Agda 2.6.4.3 with agda-stdlib 2.1-4 (the gate's pins): it passes for the core, the echo-additive instance and 5 expected rejections. The new rejection fails at its `invalid` line with `⊤ !=< Delivered (AWorld.acut w')`. - `scripts/minimal-laws.sh` passes for `KCut.agda` and now for `Async.agda`. - `--safe --without-K`; no postulates under `src/` or `tests/`; no matching on equalities of abstract grades. - `node scripts/check-repository.mjs` passes. The ledger binding was checked to catch a broken Y-row citation. - All 27 tests pass, and the 25 locally runnable estate gates pass. ## Checklist - [x] Commits are signed (SSH, verified by GitHub) - [x] Local checks pass - [x] SPDX headers on the new files (code MPL-2.0, prose CC-BY-SA-4.0) - [x] Docs do not overstate. The scope limits are in the ledger ("Not claimed" under Asynchrony) and in the addendum. - [x] No soundness hole: `--safe --without-K`, no postulates, every cited definition carries its `-- Ledger Y-n.` line ## Notes for reviewers - **The falsifier's reading.** The 2026-10-12 addendum named `sender-knows` as the falsifier. Read literally, the T-2 fixtures are "a party knows its own frontier", and that cannot break. The pre-registration fixes the reading before any proof: the sender knows the message was received. - **The accounting is a choice, stated up front.** The sender pays at send, the receiver at receipt, and the bounds use the sent-so-far grade. A received-so-far grade is not a prefix of the global type and is not defined. - **Causality.** `Quiet` reads the receiver's local cut, which at a choice it is outside of shows only the left branch. Worlds also require plain merge for every party, which makes the branches agree. The module comment says so. - **Branch.** Restarted from `main` after #34 merged. Two commits, pre-registration first; please keep them separate (rebase or merge commit) so the order stays on record. --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ <!-- This is an auto-generated comment: release notes by coderabbit.ai --> ## Summary by CodeRabbit * **New Features** * Added support for reasoning about messages and choices that are in flight, alongside delivered interactions. * Established asynchronous results for resource accounting and bounds, including how senders and receivers can know whether a message was sent or received. * Demonstrated that a delivered reply can give a sender knowledge of receipt in a two-message protocol; a reply still in flight is not sufficient. * **Documentation** * Updated the architecture, proof-status, and reference documents with these results and the remaining limitations, including recursion and full merge. * **Tests** * Expanded certification checks to cover the asynchronous proofs. <!-- end of auto-generated comment: release notes by coderabbit.ai --> --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Oct 19, 2026
Merged
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
mainis currently broken. Since 16 Oct, any job that resolves a lock record repeating its SHA asrefdies at "Set up job" with:That covers two required checks, the Agda proof gate and
scan / gitleaks. A manual run ofproofs.ymlonmainatf5a4177failed this way today (39251522875); the same commit passed on 15 Oct. Until this merges, no PR can pass its required checks. The scheduled OSSF Scorecard runs (16 to 19 Oct) fail with the same error, onupload-sarif.What job setup now refuses is a tagged action whose lock record repeats the SHA as
ref.gh actions-lockrecords the release tag there. The check applies in two places:actions/checkoutrecord has had the SHA asrefsince ci: close the lock, bump the standards pin #33, which changed it fromv7.0.1. Thegithub/codeql-actionrecord has had it since CI: CodeQL and OSSF Scorecard start again #31.94572e6, the commit the Secret Scanner was pinned to, the standards lock has the same SHA form. By75bd599standards had fixed its lock.Type of change
📌 New pins
hyperpolymath/standardsat75bd5994470661a099df562d6d5ad2fe744dbd66for bothscorecard-reusable.yml(was@main) andsecret-scanner-reusable.yml(was94572e6). Between94572e6and75bd599the scanner workflow changed only in its header.actions/upload-artifact@cf430e03…(v7.0.2) andossf/scorecard-action@2d114668…(v2.4.4).What changes
actions.lock:actions/checkoutgetsref: 'v7.0.1'back, andgithub/codeql-actiongetsref: 'v4.38.0'.git ls-remoteconfirms both tags.ref, as the standards lock does.standards@75bd599record, listing the actions both workflows use, replacesstandards@mainandstandards@94572e6.secret-scanner.yml:75bd599.secrets: inherit. The scanner workflow's header at that commit says callers must not pass it: the workflow declares and reads no secrets, andinheritforwards every secret the caller can see (CWE-250, standards#1108 §6b).inheritrequired is corrected.scorecard.yml: pinned at75bd599.How has this been verified?
node scripts/check-repository.mjspasses, and all 27 tests pass.scan / gitleakspass.main, and Scorecard refuses manual runs on other branches ("Only the default branch main is supported"). The first 04:10 UTC run after merge settles it.Checklist
Notes for reviewers
uses:list on the 94572e6 record) did not fix the scanner, and commit 4 removes that record. Squash on merge.mainatf5a4177after CI: pin the estate audit to cicd-suite 376898b #32 merged.🤖 Generated with Claude Code
https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV