Repository navigation
feat(gates): strict Rust CI, Creusot, SPARK and miniKanren reusable gates - #54
Merged
Merged
Conversation
…ates Four reusable workflows, each consumed like the estate audit (thin caller at a full SHA, de-onboarded from actions.lock), each able to fail for what it claims to check, each with a verdict that treats a skipped mandatory job as void. Rust CI (rust-ci.yml): replaces callers of standards' rust-ci-reusable.yml. Root cause of the estate-wide "Cargo check + clippy + fmt: failing after 6s" (plasma-parser-writer#105): a SHA-pinned dtolnay/rust-toolchain with no `toolchain:` input exits before cargo runs. resolve.sh now computes the channel first and refuses an empty one. Stricter than before: -D warnings on every compile, doctests (--all-targets never ran one), cargo doc with warnings denied, the declared rust-version built, cargo-deny advisories/ bans/sources by default (licences only with an owner-authored deny.toml), a missing Cargo.lock named before cargo runs. Existing context names kept. Creusot (creusot-gate.yml): detect, theatre (a "verified with Creusot" claim with no contracts is a hard failure; a hollow dependency is named), prove (Creusot at a pinned release; a planted false contract must be refused and a planted true one proved before the caller's crates are proved, else the verdict is void). Answers standards#692. SPARK (spark-gate.yml): standards' SPARK Theatre Gate nested at a pin for the claims side, GNATprove via Alire at pinned versions with --checks-as-errors=on --warnings=error and the same planted controls. miniKanren (kanren-gate.yml): relational sources must have goal-level tests, every relational test is executed by the interpreter its dialect names, impure operators are listed (enforceable), claims without relations are named. Scripts are pinned by reading the caller's own `uses:` SHA back out of the caller's checked-out workflow file, so one pin selects both the workflow and its scripts; scripts/verify-suite-checkout.sh refuses anything else. tests/lock-transitive-closure.sh now compares the composites a pin actually references rather than the whole actions/ tree. Self-tests under the exact composite shell with planted defects and mutants: rust 31, creusot 27, spark 19, kanren 19 assertions. Templates, a generalised pin-tracking bot, deonboard-workflow.sh and rollout_language_gates.sh complete the consumption path. Not yet witnessed live: the Creusot and GNATprove installs and the provers' exit-code contracts; the planted controls make the gate report void rather than green if either assumption fails on a runner. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8
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 15 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. Comment |
hyperpolymath
marked this pull request as ready for review
October 14, 2026 13:53
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
|
This was referenced Oct 19, 2026
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 19, 2026
Move all 24 hyperpolymath/cicd-suite/actions/* refs in .github/workflows/main-estate-audit.yml from 1aa6bfb (#48) to 9a947fa, the current main HEAD (#54's merge commit). #51 changed actions/manifest-check and left the pins at 1aa6bfb, so main's "Composite shell contract" has been red since 8bf6d92: tests/lock-transitive-closure.sh reports that manifest-check is pinned at 1aa6bfb, which differs from HEAD's. The pin moves to 9a947fa rather than 8bf6d92 so it serves everything on main, including #54's additions. This also makes #51's manifest-deed-paths-ignore and manifest-k9-paths-ignore inputs take effect: manifest-check@1aa6bfb does not declare them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 (cherry picked from commit 80bea8c)
This was referenced Oct 19, 2026
hyperpolymath
added a commit
that referenced
this pull request
Oct 19, 2026
## Why #51 changed `actions/manifest-check` and, by design, left the gate pins at `1aa6bfb` (#48). Since then main's **Composite shell contract** has been red on every push (runs on 8bf6d92, fe13738 and 9a947fa). `tests/lock-transitive-closure.sh` reports: ``` FAIL main-estate-audit.yml pins actions/manifest-check at 1aa6bfb, which differs from HEAD's PASS=30 FAIL=1 ``` Until the repin, #51's `manifest-deed-paths-ignore` / `manifest-k9-paths-ignore` inputs have no effect, because `manifest-check@1aa6bfb` does not declare them. ## What All 24 `hyperpolymath/cicd-suite/actions/*` refs in `.github/workflows/main-estate-audit.yml` move from `1aa6bfb` to `9a947faad4f7f6640148980dd892b39f216fd091`. That is current main HEAD, #54's merge commit. I chose it over #51's merge commit (`8bf6d92`) so the pin serves everything now on main. The diff is 24 lines out and 24 in, nothing else. Pins stay full SHAs, and the workflow stays de-onboarded from `actions.lock`. ## Verification - **Reproduced on main first:** `tests/lock-transitive-closure.sh` PASS=30 FAIL=1, the failure above. - **On this branch:** - `tests/lock-transitive-closure.sh`: PASS=31 FAIL=0. - `tests/composite-shell-contract.sh`: PASS=28 FAIL=0. - `tests/deonboard-lock-schemas.sh`: PASS=33 FAIL=0. - `tests/deonboard-estate-audit.sh`: PASS=9 FAIL=0. - **Structure:** exactly 24 refs, all at `9a947fa…`; no `1aa6bfb` or `@main` refs remain. `9a947fa` is an ancestor of `origin/main`. - **actionlint:** clean on `main-estate-audit.yml`. ## Next januskey's thin caller pins this PR's merge commit and passes `manifest-deed-paths-ignore` for `audits/assail-classifications.a2ml`. That clears januskey's red `manifests` check. --- _Generated by [Claude Code](https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 19, 2026
…; pin Alire by hash; re-pin the theatre gate (#57) ## What the first live caller showed The first cross-repository call of `rust-ci.yml` (hyperpolymath/plasma-parser-writer#108, [run 39251770946](https://github.com/hyperpolymath/plasma-parser-writer/actions/runs/39251770946)) died at startup: > The action EmbarkStudios/cargo-deny-action@3c63498 is not allowed in hyperpolymath/plasma-parser-writer because all actions must be from a repository owned by hyperpolymath, created by GitHub, verified in the GitHub Marketplace, or match one of the patterns: … `creusot-gate.yml` from the same commit resolved and ran on that PR (detect, theatre gate and verdict all green), which also answers the callee-lock question #54 left open: a gate workflow that is deliberately not keyed in this repository's lock resolves fine. The Actions policy is evaluated in the **caller's** repository, so a reusable may only use what every caller is allowed, and nothing in this repository's own CI could ever see the refusal. ## What this PR does * **`rust-ci.yml`** — cargo-deny is installed through `taiki-e/install-action` (the installer the coverage job and hypatia's green workflows already use) at the version cargo-deny-action shipped (`0.20.2`, new input `cargo_deny_version`), and run as plain `cargo deny` steps with the argument shape the action used (global args, `--manifest-path`, command). * **`spark-gate.yml`** — Alire is a sha256-pinned release binary (alr `2.1.1` x86_64 Linux, the version `setup-alire` v6.0.0 defaults to; new inputs `alr_version` / `alr_sha256`, hash recorded from the downloaded asset) followed by `alr -n toolchain --select gnat_native=<v> gprbuild`, which is what `alire-project/setup-alire` does on Linux. That action is also outside the allowed owners, and it nests `actions/cache/restore@v4` and `actions/setup-node@v4`, floating tags no caller under `sha_pinning_required` may carry. The nested standards theatre gate moves from `95de3df` to `75bd599`: since about 2026-10-15 GitHub validates a called reusable against the callee's `actions.lock` and rejects records whose `ref:` is their own SHA; `95de3df`'s lock has them (hypatia PIN-003, hyperpolymath/hypatia#931, lists the 545 such standards commits), `75bd599` is the first that does not. The theatre gate's content is identical at both commits. * **`tests/gate-action-owners.sh`**, run by `language-gates-self-test.yml` — every `uses:` in the four gates names an owner in {actions, github, hyperpolymath, dtolnay, swatinem, goto-bus-stop, taiki-e} at a full SHA; a planted disallowed owner and a planted tag pin must both be refused or the guard reports NO CHECK (exit 2). * **README** — what a gate may use, what the callee lock must look like, and how a consumer with a lock-sync gate onboards a caller (hyperpolymath/cicd-squabbler#135 is the worked example for its standards callers). ## Evidence actionlint clean on the three workflows; shellcheck clean on the guard; the four gate test suites (31/27/19/19) and the composite shell contract (28) still pass; the owners guard passes with its planted control tripping. `tests/lock-transitive-closure.sh` fails 6 checks on this branch **and on main alike** (`manifest-check` pinned at `1aa6bfb` in `main-estate-audit.yml`, the subject of #56); nothing here touches it. ## Not yet witnessed live The pinned-alr path and `cargo deny` through install-action run for the first time on the first consumer that pins this commit; the planted controls still make a broken install report void, never green. After this merges, plasma-parser-writer#108's pin moves to the merged SHA and `Rust CI` runs there for the first time; cicd-squabbler can then onboard the Rust and SPARK gates with a closure that no longer needs ids this session could not obtain. Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Co-authored-by: CodeRabbit <noreply@coderabbit.ai>
hyperpolymath
added a commit
that referenced
this pull request
Oct 19, 2026
… the schema guard and the case fix (#56) ## What was wrong `scripts/deonboard-workflow.sh` (#54) is a copy of the estate-audit de-onboard script, taken before #52 and #53 landed. It has neither fix: 1. **No schema guard.** It accepts any `actions.lock` schema. On a `v9.9.9` lock it exits 0 and edits the lock. #53's fail-closed guard (exit 3) lives only in `deonboard-estate-audit.sh`. 2. **Case-sensitive prune.** It compares dependency keys byte for byte. Take a lock where the `hyperpolymath/standards` record reaches `swatinem/rust-cache@6323deb…` but the record key is `Swatinem/rust-cache@6323deb…`. The script prunes that record and leaves a dangling edge, which startup-fails the run. This is the januskey shape #52 fixed, but only in the estate-audit copy. **Who was exposed:** `rollout_language_gates.sh` de-onboards every Rust CI, Creusot, SPARK and miniKanren caller through `deonboard-workflow.sh`. Rust CI callers are exactly the repositories whose locks carry the `standards` → `rust-cache` edge. As far as this session knows, no rollout has run since #54 merged, so this is a latent defect rather than a broken estate. That is ASSUMED: I have no rollout logs. The `deonboard-workflow.sh` header and README line 273 on main already said the estate-audit script "now delegates" to it. It did not; it was a second copy. ## The change - **`scripts/deonboard-workflow.sh`** is now the one implementation. It carries #53's `known_versions` guard and #52's `lower_repo` prune, with their comments carried over verbatim. - **`scripts/deonboard-estate-audit.sh`** is now just a usage check and one `exec …/deonboard-workflow.sh "$repo" .github/workflows/main-estate-audit.yml`. `rollout_estate.sh`, the templates and the README keep working through it unchanged. - **`tests/deonboard-lock-schemas.sh`**: - It reads `known_versions` from the generic script. - Every fixture and the v9.9.9 control run through both entry points. - The prune-skipping mutant is applied to the generic script and must be killed through the wrapper as well, which fails if the wrapper ever stops delegating. - The optional argument is now a scripts directory. - **`tests/deonboard-estate-audit.sh`** (#52): - Both entry points run the same checks. - The two entry points must produce byte-identical locks. - The `| lower_repo` mutant is applied to the generic script and must be killed through both. - **CI** (`code-hygiene-self-test.yml`): - `tests/deonboard-estate-audit.sh` was never run in CI. It now runs in the Composite shell contract job. - The workflow also triggers on `scripts/deonboard-workflow.sh`. - No `uses:` added. - **Docs:** README and ARCHITECTURE now describe the delegation as it is. - **Ported from #55:** `3325927` is #55's repin, cherry-picked with `-x`; the diff is byte-identical. - **Why:** main's `lock-transitive-closure` failure would otherwise stop the Composite shell contract job before the de-onboard steps run. - **If #55 merges first:** this commit becomes a no-op. ## Evidence (TESTED) I copied the new suites into a tree of `origin/main` (`9a947fa`) and ran them against main's scripts. `tests/deonboard-estate-audit.sh`: PASS=14 FAIL=4 - `FAIL pruned Swatinem/rust-cache, which the standards record still reaches` - `FAIL dangling edge(s): Swatinem/rust-cache@6323deb` - `FAIL the entry points disagree: …` - `FAIL mutant is identical to the script: the case-folding the test exists for is gone` `tests/deonboard-lock-schemas.sh`: PASS=57 FAIL=4 - `FAIL script declares no known_versions` - `FAIL exit 0 on schema v9.9.9 (want 3)` - `FAIL lock modified despite refusal` - `FAIL orphan check passed a mutant that does not prune` (main's wrapper does not delegate) On this branch: | Check | Result | | --- | --- | | `tests/deonboard-estate-audit.sh` | PASS=19 FAIL=0 | | `tests/deonboard-lock-schemas.sh` | PASS=63 FAIL=0 | | `tests/lock-transitive-closure.sh` | PASS=31 FAIL=0 | | `tests/composite-shell-contract.sh` | PASS=28 FAIL=0 | | `bash -n` | clean | | `shellcheck -S warning` | clean (default severity: same SC2015/SC2016 counts as main) | | `actionlint` | no new findings (the 8 `"$/actions/…"` findings in the hygiene self-test are also on main) | 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
to hyperpolymath/gitbot-fleet
that referenced
this pull request
Oct 20, 2026
…in this repo's standards callers (#615) ## Why Three defect classes killed Rust CI across the estate this fortnight, each a setup failure that reads as a code failure. hyperpolymath/cicd-suite#54 built gates in which they cannot occur; hypatia (hyperpolymath/hypatia, companion PR) detects them; this is the actuation half: a fix script per class, a registry row, and a contract test run by `rust.yml`. | Class | Rule | Script | |---|---|---| | SHA-pinned `dtolnay/rust-toolchain` with no `toolchain:` input (`'toolchain' is a required input`; hyperpolymath/plasma-parser-writer#105) | WF026 | `scripts/fix-rust-toolchain-input.sh` | | Caller pinned at a reusable revision the estate has **measured** dead (June 2026 toolchain window, 83 commits; 2026-08-19..10-19 lock window, 545 commits) | WF027, PIN-003, WF016 | `scripts/fix-stale-reusable-pin.sh` + `scripts/lib/stale-reusable-pins.tsv` | | `actions.lock` record whose `ref:` is its own SHA, which GitHub rejects at `Set up job` since ~2026-10-15 (`invalid lockfile pin`) | PI006 | `scripts/fix-lock-self-sha-refs.sh` + `scripts/lib/action-ref-tags.tsv` | Design points worth a reviewer's eye: * The stale-pin script moves a pin **only** to the replacement the table names, never to "newest" (standards' `lock-selfcheck.sh` exists because newer can be less usable). The table was generated from a walk of standards' history, file content and lock records checked per commit, not dates. * If the caller's `actions.lock` names the stale SHA, it follows the pin; two dead SHAs moving to one replacement are merged into one record. The nested `uses:` list is **not** recomputed here and the script says so (that closure is the `gh actions-lock` / `check-lock-sync.sh` step). * The self-SHA script takes tags from a map whose every row comes from the lock GitHub accepts (standards@`75bd599`), falling back to `git ls-remote --tags`; a commit with no tag is reported and left, exit 1. Reusable-workflow records keep their SHA ref, as the accepted lock does. * `AGENTIC.a2ml` names what an agent may and may not do with these: never choose a replacement SHA, never recompute a closure here, always idempotent. ## Dogfooded on this repository The five standards callers (governance, hypatia-scan, mirror, scorecard, secret-scanner) were pinned inside the lock window (`da2c748`, `571cc73`) and have been dying at `Set up job` since 2026-10-16 ([Governance run 39105727502](https://github.com/hyperpolymath/gitbot-fleet/actions/runs/39105727502) and every run after). They now pin `75bd599`; `actions.lock` holds one `standards@75bd599` record whose nested list is the union of what those five reusables use at that commit, every third-party record copied verbatim from standards' own lock, the seven self-SHA refs given their tags, and the three Dependabot bumps the lock had missed (`download-artifact` v8.0.2, `upload-artifact` v7.0.2) resynced. `scripts/check-lock-sync.sh`: in sync, transitively closed. ## Evidence * `scripts/tests/fix-workflow-pins.sh`: 28 checks — planted defects fixed, planted non-defects untouched, second runs byte-identical, controls with an empty table. Wired into `rust.yml`'s `dispatch-contracts` job. * `scripts/tests/dispatch-paths.sh` still passes. `bash -n` and the fleet's JSON registry parse. No bot slot, manifest or quarantine change; `[mass-delete-ok]` not needed (no deletions). Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ <!-- This is an auto-generated comment: release notes by coderabbit.ai --> ## Summary by CodeRabbit * **Chores** * Updated shared governance, security scanning, mirroring, and scorecard workflows, with explicit secret mappings where needed. * Added tools to repair stale workflow references, missing Rust toolchain settings, and lockfile references. * **Bug Fixes** * Rust formatting checks now block CI when formatting requirements are not met. * **Tests** * Added offline checks for workflow maintenance tools, including verification that repeated runs leave corrected files unchanged. * CI now runs these checks. <!-- end of auto-generated comment: release notes by coderabbit.ai --> --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
hyperpolymath
added a commit
to hyperpolymath/cicd-squabbler
that referenced
this pull request
Oct 20, 2026
…sure (#135) ## What was failing Rust CI has been red on every run since 2026-10-16 ([run 38846539059](https://github.com/hyperpolymath/cicd-squabbler/actions/runs/38846539059) and each one after it), dying in `rust-ci / Detect Cargo.toml` at **Set up job**: ``` Unable to resolve action `actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1`: invalid lockfile pin. Run `gh actions-lock` to update the lockfile ``` Nothing in this repository changed between the last green run (`60e8f7a`, 2026-10-15) and the first red one: the lock and the workflows are byte-identical across the flip. GitHub began validating a called reusable workflow against the **callee** repository's `actions.lock` at the called SHA, and rejects a dependency record whose `ref:` is the bare commit SHA instead of the tag it was resolved from. standards' lock at `8f2ee50` and `da2c748` records `actions/checkout@3d3c42e5…` with `ref: '3d3c42e5…'`; at `75bd599` (standards main, 2026-10-19) the same record reads `ref: 'v7.0.1'`, and callers pinned there create jobs again (hyperpolymath/hypatia#929 witnessed it first). A walk of standards' first-parent history shows 454 main commits from 2026-08-19 to 2026-10-19 carry such a record; `75bd599` is the first that does not. Governance, Mirror, Secret Scanner, Hypatia Scan, Scorecard and the standards pipeline were dying the same way, so all seven callers move together. ## What this PR does * Re-pins the seven standards callers to `75bd5994470661a099df562d6d5ad2fe744dbd66`. The pipeline caller passes no inputs, so the inputs `ci-pipeline.yml` dropped since `ed5e3f6` do not affect it. * Rebuilds `actions.lock` instead of patching it: one `hyperpolymath/standards@75bd599` record whose `uses:` is the union of what the seven called reusables use at that commit, and every third-party record copied verbatim from standards' own lock at `75bd599`, which GitHub accepts. The two actions this repository pins directly by SHA (`actions/attest-build-provenance`, `softprops/action-gh-release`) now carry the tag that resolves to their commit (`v4.2.2`, `v3.0.3`). Records nothing references are pruned. `scripts/check-lock-sync.sh`: in sync and transitively closed. * Resyncs two Dependabot bumps the lock had been missing since #133 (`smtp-notify-action` v0.5.0; `upload-artifact` v7.0.2 / `download-artifact` v8.0.2), which were startup-failing `push-email-notify.yml` and `static-analysis-gate.yml`. * Two rustdoc fixes in `squabble-core` for the strict warnings-denied doc build of cicd-suite's Rust gate (hyperpolymath/cicd-suite#54): public docs linked the private items `step_concluded` and `propose_for`. ## Verified locally `cargo fmt --check`, `cargo clippy --all-targets --locked -D warnings`, doctests, `cargo +1.85 check --workspace --locked` (the declared MSRV) and `cargo doc --document-private-items` with `RUSTDOCFLAGS=-D warnings` all pass. `scripts/check-lock-sync.sh` exits 0. ## Not in this PR Calling cicd-suite's strict Rust gate and the SPARK gate (for `spark/squabble_gate.gpr`) from here. This repository's lock-sync gate requires every called reusable's transitive closure in `actions.lock`, and that closure needs records for `EmbarkStudios/cargo-deny-action` and `alire-project/setup-alire` whose numeric repository ids this session cannot obtain (the GitHub API is scoped to the estate's own repositories). hyperpolymath/plasma-parser-writer#108 is the first live caller of the cicd-suite gate under the new callee-lock validation; what it shows decides whether cicd-suite must key its gate workflows in its own lock first. Either way the adoption here is a follow-up, with those two ids or with `gh actions-lock` run by someone who can. Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
hyperpolymath
added a commit
to hyperpolymath/proven-tests-and-benches
that referenced
this pull request
Oct 20, 2026
…-suite#54 (#96) ## What Three new proven-exact corpus units under `corpus/provenance/reflexive/`, each a bare `module Test` with base-library imports only (R-43), total lemmas as the warrant, and the 0/1/2 fixture triple. They are the defect classes hyperpolymath/cicd-suite#54's gates exist to refuse, stated once and firable forever: | Unit | Fires when | Ground truth | |---|---|---| | `setup-failure-reported-as-subject-failure` | a gate claims **FAIL** while every failure it records is a setup failure (toolchain install, checkout, action input validation) — the subject was never checked, so the honest verdict is VOID | plasma-parser-writer `rust-ci / Cargo check + clippy + fmt`, red on every run 2026-09-29 to 2026-10-14 from `'toolchain' is a required input` (run 38564229091); hyperpolymath/plasma-parser-writer#105 | | `skipped-mandatory-reported-as-pass` | a gate claims **PASS** while a job it declared mandatory concluded `skipped` — the skipped twin of `cancelled-gate-void` | platform behaviour (a required check concluded `skipped` does not block a merge), the reason every cicd-suite gate ends in a verdict job; the manifest's `warrant_class` says so until a dated estate firing exists | | `proof-claim-without-prover` | a gate claims **PASS** while a prover the tree advertises never ran or ran over no obligations (proof theatre) | the contract of standards' SPARK Theatre Gate and hyperpolymath/standards#692; cicd-suite's `creusot-gate`/`spark-gate` theatre jobs | Lemmas, named in each `error-model.a2ml` and checked by `check_unit_ledger`: `firesOnSetupOnlyFail` / `silentOnSubjectFail` / `silentOnNoFailure` / `voidClaimNeverFires`; `firesOnSkippedMandatoryPass` / `silentOnCleanPass` / `optionalSkipIsNotMandatory` / `failedMandatoryIsNotSkipped`; `firesOnTheatrePass` / `silentOnHonestPass` / `unclaimedIsNotTheatre` / `dischargedClaimIsNotTheatre`. Registries: the three `covering main` entry points are allowlisted in `scripts/check-escape-hatches.sh`; the firing and calibration fixtures are registered in `.machine_readable/testing/adversarial-content.a2ml`; `corpus/COUNT.a2ml` is regenerated (deployed 4, fired_with_date 4, diagnosticity_complete 4, proven_exact 4, repeat_tested 4); DEBT S-9 names all four units. ## Evidence Scripted on 2026-10-19: each unit compiled three times from a clean `build/` under the three-signal predicate (rc 0, zero `^Error:` lines, binary present) and fired its triple identically each time — silent 0, firing 1, calibration 2. `stability.a2ml` carries the timestamps and the `Test.idr` sha256. From the repository root: `check-doc-facts.sh corpus` compiles and fires all four units; `corpus-selftest` passes its 20 trees (with `en_US.UTF-8` present for the collation tree); `check-doc-facts.sh source` and `check-escape-hatches.sh` pass. ## Stated, not claimed The authoring machine had Idris2 **0.8.0** only; the repository pins **0.7.0**. Every new `stability.a2ml` says the first compile at the pinned toolchain is this PR's `corpus-check` job, and `[reproduce]`/`[replicate]` remain `no` (DEBT S-9). If `corpus-check` is red here on something 0.7.0-specific, that is the first finding of this PR and I will fix it here. Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
to hyperpolymath/plasma-parser-writer
that referenced
this pull request
Oct 20, 2026
…ate (#108) ## Why `rust-ci / Cargo check + clippy + fmt` was red for a fortnight on every PR (#105, fixed by the one-line re-pin in #107). The red was a setup failure read as a code failure: a SHA-pinned `dtolnay/rust-toolchain` given no `toolchain:` input died before a compiler existed. hyperpolymath/cicd-suite#54 built a Rust gate in which that class cannot occur (the toolchain is resolved before any action runs and an empty resolution is refused), made it stricter, and added a parallel Creusot gate. This PR makes this repository a consumer of both. ## What * `.github/workflows/rust-ci.yml` now calls `hyperpolymath/cicd-suite/.github/workflows/rust-ci.yml@9a947fa` (cicd-suite main, the merge of #54). The job id and the contexts `rust-ci / Cargo check + clippy + fmt` and `rust-ci / Cargo test` are unchanged, so existing branch rules keep matching. `rust-ci / Rust CI verdict` is the context to require from now on: it goes red when any gate failed **or was skipped while expected**. * `.github/workflows/creusot-gate.yml`: the Rust deductive-verification gate. This tree carries no Creusot obligations, so it reports a notice, not assurance. * `.github/workflows/track-estate-audit.yml`: weekly PR that moves every cicd-suite pin here to cicd-suite HEAD, so a fix in the gate arrives as a reviewable PR. Needs the `AUTOMATION_TOKEN` secret described in its header to open PRs that trigger CI. ## What the stricter gate found, fixed at source * **`cargo doc` with warnings denied**: three doc comments in `plasma-parser/src/zone/boundary.rs` wrote `[project]`, `[[zone]]` and `[family]` as bare brackets, which rustdoc reads as unresolved intra-doc links. They are code spans now. * **The declared MSRV was false**: `rust-version = "1.74"` while a dependency needs edition 2024. Verified: `cargo +1.78 check --locked` fails on `edition2024`; `cargo +1.85 check --locked` passes. The gate's MSRV job builds the declared version, so the declaration now says 1.85. ## Evidence Run locally on rustc 1.97 against this tree: `cargo fmt --check`, `cargo clippy --all-targets --locked -D warnings`, `cargo test --locked --all-targets`, `cargo test --locked --doc`, and `cargo doc --no-deps --document-private-items` with `RUSTDOCFLAGS=-D warnings` all pass; `cargo +1.85 check --workspace --locked` passes. ## Not yet witnessed live This is the first cross-repository call of the cicd-suite Rust gate since GitHub began validating a called workflow against the callee repository's `actions.lock` (around 2026-10-15). cicd-suite's gate workflows are deliberately not keyed in cicd-suite's own lock. If this PR's `rust-ci` run dies at `Set up job` with "invalid lockfile pin" or a workflow-file error, the fix belongs in cicd-suite (key the gate workflows in its lock), not here, and I will report it on this PR. Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
to hyperpolymath/hypatia
that referenced
this pull request
Oct 20, 2026
…estate's dead Rust CI (#931) ## Why Three defect classes killed Rust CI across the estate between 2026-09-29 and 2026-10-19, each a setup failure that reads as a code failure. hyperpolymath/cicd-suite#54 built gates in which they cannot occur; this PR is hypatia's half of the propagation architecture (hypatia detects → gitbot-fleet actuates, hyperpolymath/gitbot-fleet#615 → .git-private-farm propagates, hyperpolymath/.git-private-farm#166). Every rule here has a fleet fix script carrying the same facts. ## What | Rule | Where | Fires on | Fleet repair | |---|---|---|---| | **WF026** | `workflow_audit.ex` | a SHA-pinned `dtolnay/rust-toolchain` step with no `toolchain:` input — the step exits with `'toolchain' is a required input` before any cargo command runs (hyperpolymath/plasma-parser-writer#105; standards#439 fixed the reusable). Step bodies are bounded by indentation; tag pins never fire. | `fix-rust-toolchain-input.sh` | | **WF027** | `workflow_audit.ex` | a caller pinned at a reusable revision the estate has **measured** dead for that reusable — a data table keyed by reusable path; first row: the 83 standards main commits of June 2026 whose `rust-ci-reusable.yml` carries the WF026 defect (every first-parent commit `d73c93e0..49ed4715`, file content checked). Unlike WF016 these commits resolve: the run starts and the reusable's first step fails. | `fix-stale-reusable-pin.sh` (Window A) | | **PIN-003** | `pr-automerge-policy.json` (read by PI001 and PA001) | the 545 standards commits reachable from main, 2026-08-19..2026-10-19, whose `actions.lock` carries an action record with its own SHA as `ref:`. Since ~2026-10-15 GitHub validates a called reusable against the **callee's** lock at the called SHA and rejects those records (`invalid lockfile pin`), so every standards reusable at those revisions dies at `Set up job` for every caller (#929; cicd-squabbler run 38846539059, byte-identical to its last green run). `known_good_sha` is `75bd599`, the first main commit with a clean lock. | `fix-stale-reusable-pin.sh` (Window B) | | `known_reusables` | `sha_bump_propagation.ex` | cicd-suite's estate audit and the Rust, Creusot, SPARK and miniKanren gates, so a cicd-suite bump feeds the propagator like a standards bump. | — | A note on PIN-003's provenance: standards' own `scripts/lock-selfcheck.sh` rates those commits SELF-CONSISTENT, because it checks that every ref is *keyed*, not that a key's `ref:` is a tag. The list was produced by a walk of every reachable commit, lock content parsed per commit. ## Tests * `test/rules/workflow_audit_pins_test.exs` (new, 13 tests): fires / silent / the indentation boundary / the per-reusable window / the table's edges (83 rows, edges in, replacement out) / the audit's counts. * `test/rules/pin_integrity_test.exs`: reads the committed policy with OTP's `:json`; PIN-003 denylists `8f2ee50` through a reusable path, while `75bd599` and the June revisions are not denylisted. * `test/rules/sha_bump_propagation_test.exs`: the cicd-suite rows. Hex is unreachable from this session, so `mix test` could not run here. The WF026/WF027 tests were run against a scratch build of the new functions (13/13), and the pin-integrity, lock and SHA-bump suites against the compiled modules (all pass; the two pre-existing `actions_lock_test` failures outside Mix — v0.0.3 lock, `Hypatia.Rules` not loaded — are unrelated). `mix format --check-formatted` passes on every changed file. CI's `mix test` is the first full run; if it finds something, I fix it here. `AGENTIC.a2ml` records the contract: tables extend only from a measured walk, an agent never names a replacement revision, and the WF027 table / PIN-003 mirror gitbot-fleet's `stale-reusable-pins.tsv` windows A and B and are regenerated together. Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge. --- _Generated by [Claude Code](https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8)_ --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Co-authored-by: CodeRabbit <noreply@coderabbit.ai>
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
2 participants
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.
Why
Every
rust-ci / Cargo check + clippy + fmtthat callshyperpolymath/standardsrust-ci-reusable.ymlat a pre-fix SHA has been red for six seconds since 2026-09-29 (hyperpolymath/plasma-parser-writer#105, run 38564229091). The reusable pinneddtolnay/rust-toolchainby commit and passed notoolchain:; a SHA ref carries no channel, so the action exits 1 with'toolchain' is a required inputbefore a compiler exists. The fix landed in standards (edbe311), and the callers stayed pinned behind it. That is a class of failure, not an instance: a gate that dies in setup and reads as a code failure.This PR makes the class impossible by construction and, as asked, makes the Rust gate stricter, adds a parallel Creusot gate, and adds Ada/SPARK and miniKanren gates to this suite so the estate has one place to call them from. It also answers hyperpolymath/standards#692 (Rust + Creusot without proof theatre, with a planted failing contract).
What
Four reusable workflows, each consumed like the estate audit (thin caller at a full SHA, de-onboarded from
actions.lock), each with a verdict job that turns a skipped mandatory job into red (a gate that did not run is void, not green — proven-tests-and-benches, corpus unitcancelled-gate-void):.github/workflows/rust-ci.ymlactions/rust-ci-check: toolchain resolved before any action runs and refused when empty; every call--locked;RUSTFLAGS/RUSTDOCFLAGS-D warnings; doctests (--all-targetsnever ran one);cargo docwith warnings denied; the declaredrust-versionbuilt; cargo-deny advisories/bans/sources by default (licences only against an owner-authoreddeny.toml); a missingCargo.locknamed before cargo runs. Existing context names kept..github/workflows/creusot-gate.ymlactions/creusot-check: detect → theatre (a "verified with Creusot" claim with no contracts is a hard failure; a hollowcreusot-stddependency is named;#[trusted]axioms listed) → prove (Creusot v0.14.0 at its pinned nightly; a planted FALSE contract must be refused and a planted TRUE one proved before the caller's crates are proved, else the verdict is void)..github/workflows/spark-gate.ymlactions/spark-check: GNATprove 16.1.0 via Alire,--checks-as-errors=on --warnings=error, same planted controls; refuses to guess between several.gprfiles..github/workflows/kanren-gate.ymlactions/kanren-check: relational sources (Scheme family, Rust kanren crates) must have goal-level tests; every relational test is executed by the interpreter its dialect names; impure operators (conda/condu/project/…) listed and enforceable; a miniKanren claim with no relations named.How the scripts are pinned: each job reads the caller's own
uses:SHA back out of the caller's checked-out workflow file (GITHUB_WORKFLOW_REFnames it; inside a reusable thegithubcontext is the caller's), checks this repository out at that SHA and verifies it (scripts/verify-suite-checkout.sh), then runs the scripts from there. One pin, held by the caller, selects both the workflow and its scripts; no repin commit after a change toactions/.tests/lock-transitive-closure.shnow compares the composites a pin actually references rather than the wholeactions/tree, so unrelated additions underactions/no longer force a repin of the estate audit.Consumption:
templates/{rust-ci,creusot-gate,spark-gate,kanren-gate}-caller.yml,scripts/deonboard-workflow.sh(the estate-audit script now delegates to it),templates/track-estate-audit.ymlgeneralised to move every cicd-suite pin weekly,rollout_language_gates.shinstalls callers by what a tree contains.Evidence
Run locally under the exact composite shell (
bash --noprofile --norc -e -o pipefail):actions/rust-ci-check/test.sh: 31 assertions, 0 failures (planted fmt, clippy, doctest, intra-doc-link, missing-lock and empty-toolchain defects all go red; a mutant that swallows cargo's exit goes green, proving the red was not vacuous).actions/creusot-check/test.sh: 27/0.actions/spark-check/test.sh: 19/0.actions/kanren-check/test.sh: 19/0 (a real microKanren executed by Guile, a planted wrong expectation fails,condais listed).tests/lock-transitive-closure.sh: 31/0 at the new HEAD.tests/composite-shell-contract.sh: 28/0. actionlint clean on the five new workflows. The estate-audit composites (code-hygiene, spdx, formatting, linguist, secrets, required-files) pass against this tree.Not yet witnessed live
The Creusot and GNATprove install steps and the exit-code contracts of
cargo creusot proveandgnatprove --checks-as-errors=onwere validated against the tools' documentation and against stand-in oracles, not on a runner. The planted controls are the safeguard: if either prover cannot refuse a false contract on the runner, the gate reports void (exit 2), never green. The first live SPARK subject is cicd-squabbler'sspark/squabble_gate.gpr; no repository in the first rollout carries Creusot obligations yet. The.github/workflows/language-gates-self-test.ymlrun on this PR is the first live run of the four self-tests.Commits on this branch are unsigned: no signing key is available in this session (the configured key file is empty). GitHub signs the squash merge.
Consumers
Callers pinned at this branch's head are opened in plasma-parser-writer (replacing the broken standards pin and closing hyperpolymath/plasma-parser-writer#105 once green), cicd-squabbler (Rust, Creusot, SPARK, miniKanren), hypatia, gitbot-fleet and proven-tests-and-benches. After this PR merges, their pins move to the merged commit (the weekly
track-estate-audit.ymlbot does this by PR, or a one-line repin).🤖 Generated with Claude Code
https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8
Generated by Claude Code