Repository navigation
fix(ci): call the estate audit and standards reusables by their current names - #104
Merged
Merged
Conversation
hypatia-scan.yml has failed at startup with zero jobs on every run since at least 2026-10-26, on push, pull_request and schedule. governance.yml and secret-scanner.yml do the same on every push to main. All of them call reusables in the standards repository, which moved from hyperpolymath to the metadatastician organisation. Its repo id is unchanged (1116521501), but actions.lock still recorded the old owner id (6759885). standards' own lock records the repository under owner 297579217. This re-pins the four callers to metadatastician/standards at the same commit (8f2ee50) and records the current owner id. Nothing else changes. The caller permissions are not the cause: hypatia-scan already grants the security-events: write its reusable declares, and the other reusables declare no write permission. This is a test of that cause. If these callers now start, the same fix applies to every estate repository that still pins hyperpolymath/standards. Also corrects main-estate-audit.yml's header, which claimed these callers start normally. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16
Contributor
|
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. |
hyperpolymath/cicd-suite was renamed to hyperpolymath/proven-cicd-and-workflows on 2026-11-09 at 09:59 UTC. The estate-audit caller started and passed on 2026-11-05 (7a84707), and has failed at startup with zero jobs since the rename, on this branch and on #103, which does not touch workflows. This tests whether the caller starts again when it names the repository by its new name at the same commit (354c425, same owner and repository ids). The reusable at that commit still names cicd-suite for the gate actions it pins, so those nested refs are unchanged. The standards re-pin in the previous commit did not make hypatia-scan, secret-scanner or governance start, so that hypothesis is disproved. That cause is tracked separately. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16
Owner
Author
|
Result of the first test: the hypothesis this PR set out to test is disproved. Re-pinned to Two findings since then:
SonarCloud. Its three S7635 findings are the existing Generated by Claude Code |
hyperpolymath
pushed a commit
that referenced
this pull request
Nov 9, 2026
CodeRabbit's review of 94c6922 found three cases where the new scan was wrong; each now has a regression test that fails on 94c6922: - A Lean character literal such as '"' opened a phantom string that hid a later `sorry`. Character literals are now dropped before strings are read. - An Agda identifier containing `--` (`f--g`) was read as a line comment that hid a later `postulate`. In Agda, `--` opens a comment only at the start of a token. - `admit` was flagged in Agda, where it is an ordinary name. Escape-hatch patterns are now chosen per language. Also: - a relative AGDA_STDLIB is made absolute before the checkers change directory, and a linked proof directory is copied as its contents (cp -L); - toolchain.kyaml gives Verus's own Z3 a verus-z3 entry (the closure rule makes everything a tool loads an entry); - DESIGN.adoc: deviation records are written by the bundle build, which owns the lock, and travel with it into the prefix; the exemption follows the install route, not the tool; - the cartridge proposal's receipts carry the Agda library pin and import cone (PROOF-POLICY §1.1, §8.2). Ported from #104: main-estate-audit.yml calls the audit under cicd-suite's new name, hyperpolymath/proven-cicd-and-workflows. Since the rename on 2026-11-09 the old name failed at startup with zero jobs on this PR too. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16
10 of 15 tasks
hyperpolymath
changed the title
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:50
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. |
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 23:19
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
## Summary A review of this repository's proof artefacts against the estate PROOF-POLICY (`metadatastician/standards` at `9bdf864`) found ten places where they broke it. This PR fixes all ten: - `just proof-check-all` could never pass. Its escape-hatch scan matched the template's own "no postulate" and "NO Admitted" comments in all 8 proof files. No CI job ran it, so nobody noticed. - The Agda recipe ran without the §2.1 flags, and every recipe exited 0 when its prover was missing. - The status pages used template vocabulary and a percentage. They listed obligations with no subject here, and one of them gave API typing to Lean, which §1 gives to Idris2. - The toolchain manifest had no Verus, which the 2026-11-07 ruling made a default Rust verifier. - The design never said which §6 deviation records an installer must write. - The cartridge proposal predates §2.2 correspondence states and §8 Proof Witness Grades. It also carries the estate-audit fix proven on #104. `hyperpolymath/cicd-suite` was renamed to `hyperpolymath/proven-cicd-and-workflows` on 2026-11-09, after which the old name failed at startup. ## Changes - **`scripts/proof-check.sh`**, called by every `proof-check-*` recipe: - Agda runs as `agda --safe --without-K --cubical-compatible` (§2.1). - A missing checker is `UNAVAILABLE` and the run exits 3, never a pass. - The scan reads code only. Comments, Idris2 `|||` doc comments, string literals and character literals are ignored, and Agda pragmas are kept, so `{-# TERMINATING #-}` is caught. - In Agda, `--` starts a comment only at the start of a token. - Escape-hatch words are chosen per language, so `admit` is fine in Agda but caught in Coq and Lean. - Checkers run on a copy (`cp -RL`), so `.agdai` and `.vo` files never land in the tree. - A relative `AGDA_STDLIB` is made absolute. - **`tests/proof_check_test.sh`** uses stub checkers and planted escape hatches, and compares checksums of the proof tree before and after a run. - **`verification/proofs/agda/bofj-kitt-proofs.agda-lib`** lets Agda find the standard library; `AGDA_STDLIB` overrides it with an explicit path. - **`docs/status/PROOF-STATUS.adoc`** uses the §5 vocabulary with no percentage. - The ledger is empty: this repository is shell and configuration with no ABI, FFI, typed API or theory. - Template proof files and prover smoke fixtures (§3) are listed separately, with the session results below. - Obligations the proposals name for other repositories are recorded as `OPEN` there. - **`docs/status/PROOF-NEEDS.adoc`**: - Tier T5, exempt. - The template's ABI and typing obligations are withdrawn, with the reason given for each. - The template's prover guide recommended Lean "for mathlib support", which §2 forbids. It is replaced by a summary of §1. - **`tools/proof-toolchain/toolchain.kyaml`** gains `verus` (§1.2) and `verus-z3`, Verus's own pinned Z3, kept separate from the backend Z3. - **`tools/proof-toolchain/DESIGN.adoc`**: - Adds Verus to the roles. - Adds the §6 deviation records. The bundle build writes them into the lock it owns, and they travel with it to `$PREFIX/toolchain.lock.json`. - Bases the exemption on the install route, not the tool. - Names Mathesis as a consumer of lock versions for receipts. - **Cartridge proposal**: - `provers_recheck` records each leg's §2.2 fields and keeps the §5 status and the correspondence state in separate fields. - Cartridges never write a Proof Witness Grade; Mathesis derives grades from receipts. - Agda receipts carry the library pin and import cone. - echidna trust levels are not grades. - Creusot and Verus are named for Rust, with their shared solver trust recorded. - **Other proposals**: the environment proposal's silent-SKIP finding and experiment X5 are marked done for the script; the awesome-lists gap table adds Verus. - **`.github/workflows/main-estate-audit.yml`** calls the audit under its new repository name, ported from #104. ## RSR Quality Checklist ### Required - [x] Tests pass: all 7 `tests/*_test.sh` and `tests/workflows/*_test.sh` pass locally. - [x] Code is formatted: `bash -n` is clean, every changed AsciiDoc file builds with `asciidoctor --failure-level WARN`, and the manifest parses. - [x] Linter is clean: the repo gate scripts and the 21 estate-audit gates pass locally. - [x] No banned language patterns: the new script and test are Bash with awk. - [x] No `unsafe` blocks - [x] No banned functions - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `.machine_readable/STATE.a2ml` updated: not needed - [ ] `.machine_readable/ECOSYSTEM.a2ml` updated: not needed - [ ] `.machine_readable/META.a2ml` updated: not needed - [x] Documentation updated for user-facing changes - [ ] `TOPOLOGY.md` updated: no architecture change - [x] `CHANGELOG` or release notes updated: Unreleased, Added and Fixed - [ ] New dependencies reviewed for license compatibility: none ## Testing - **Real provers** (Ubuntu packages, this session): - Agda 2.6.3 with standard library 1.7.3 checks `Properties.agda` under the §2.1 flags, both through `AGDA_STDLIB` and through a registered library. With no standard library, the check fails. - Coq 8.18 checks `TypeSafety.v`. `Print Assumptions type_soundness` reports it closed under the global context. - A planted broken Agda proof fails, and a planted `Admitted` (which `coqc` accepts) is caught by the scan. - **Mutation checks**: `tests/proof_check_test.sh` fails against each of three mutants: - Agda run with `--safe` only. - The scan reading raw files instead of stripped code. - A missing checker counted as a pass. - **Review regressions**: each defect CodeRabbit found in the first version (the Lean character literal, an Agda `--` identifier, Agda `admit`, a relative `AGDA_STDLIB`) reproduces on `94c6922` and passes now. - **Smoke fixtures**: ACL2 8.5 and HOL Light (2023-10-21) pass, and a deliberately false copy of each fails on its intended check. - **Not run**: Lean, Idris2, HOL4, Mizar, PVS and TLC. This session's policy refused to build or run them from outside downloads, and Ubuntu doesn't package them. `PROOF-STATUS.adoc` says so instead of claiming them. - **Gates**: - Locally, all 21 estate-audit gates pass, run at the commits the reusable workflow pins. `check-root-shape`, `check-no-md-in-docs`, `check-lock-sync` and `just --summary` (108 recipes) pass too. - In CI on `e8a2b78`, all five `estate / …` jobs pass. **Not this PR's:** `hypatia-scan.yml`, `secret-scanner.yml` and `governance.yml` fail at startup here and on `main`. See #104 and the comment below. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16 --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
|
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
Four cross-repository workflow callers here name repositories that have moved:
hyperpolymath/cicd-suitewas renamed tohyperpolymath/proven-cicd-and-workflowson 2026-11-09 at 09:59 UTC. Since then, the estate-audit caller has failed at startup with zero jobs. It last passed onmainat7a84707on 2026-11-05.hyperpolymathto themetadatasticianorganisation. Its repo id is unchanged (1116521501), butactions.lockstill recorded the old owner id (6759885).This PR names both by their current names and records current ids.
Results
hyperpolymath/proven-cicd-and-workflowsat the same commit (354c425) makes it start again. All fiveestate / …jobs pass ond276fe0. The same change is ported into fix(proofs): align proof artefacts with the estate PROOF-POLICY #103.hypatia-scan.yml,secret-scanner.ymlandgovernance.ymlstill fail at startup when re-pinned tometadatastician/standardswith its current owner id (297579217, taken from standards' own lock). So the stale id was not their cause.hypatia-scan.ymlalready grants thesecurity-events: writeits reusable declares, and the other two declare no write permission.hyperpolymath. Only the owner can check that, under Settings → Actions → General.main-estate-audit.yml's header no longer claims these callers "start normally"; that was the error corrected on fix(ci): clear the estate-audit and Hypatia failures at their source #102.SonarCloud fails this PR on three S7635 findings. They sit on the existing
secrets: inheritlines, which the standards reusables currently need:hypatia-scan-reusable.ymlreads an undeclaredHYPATIA_SCAN_PAT, andsecret-scanner-reusable.yml's header requires inheritance. The fix is upstream: the reusables should declare their secrets so callers can pass them by name.RSR Quality Checklist
Required
tests/workflows/*_test.shpass locally.scripts/check-lock-sync.shpasses; lock records stay sorted.unsafeblocks.envfiles includedAs Applicable
.machine_readable/STATE.a2mlupdated: not needed.machine_readable/ECOSYSTEM.a2mlupdated: not needed.machine_readable/META.a2mlupdated: not neededTOPOLOGY.mdupdated: no architecture changeCHANGELOGor release notes updated: CI-only; fix(proofs): align proof artefacts with the estate PROOF-POLICY #103 records the audit renameTesting
d276fe0the estate-audit workflow starts and all fiveestate / …jobs pass. On7942d3eand on fix(proofs): align proof artefacts with the estate PROOF-POLICY #103 before the port, it failed at startup.Beyond this repository
hyperpolymath/cicd-suite/.github/workflows/...will have failed at startup since the rename. This repository's fix is the one to port, andproven-cicd-and-workflows' rollout tooling is the natural place to do it.secrets: inherit.🤖 Generated with Claude Code
https://claude.ai/code/session_01J4QvDjbjhwmFbcYz4FKn16