Skip to content

About

Composite GitHub Actions for estate-wide CI/CD auditing — required files, code hygiene, SPDX, proofs, manifests, secrets. Consumed by main-estate-audit.yml.

Topics

Resources

Code of conduct

Contributing

Security policy

Stars

2 stars

Watchers

0 watching

Forks

cicd-suite

Composite GitHub Actions for estate-wide CI/CD auditing. They are run by the reusable workflow .github/workflows/main-estate-audit.yml. Each repository calls that workflow from a ten-line caller; it does not copy it (see Consuming it).

The audit reports five component checks, one check run each:

Check Gates

governance

required-files · spdx-license · affirmation · referencing

hygiene

code-hygiene · formatting · linguist · secrets · vaulted-tokens

manifests

manifest · recipes-set

languages

idris2-abi · zig-unified-api-adapter · proof-runner · boj-cartridge

advisory

the nine advisory gates below; this check cannot fail, by design

Within a component every gate runs even after an earlier gate fails, so one push reports every failing gate. Before this change one job ran all 26 in sequence, and the first failure hid the rest behind "estate-audit: failing after 8s".

Status

Published 2026-08-07. Defects (1)–(3) are fixed and verified against two live estate repositories; (4) is partly fixed; (5) is closed by removing the stubs from the workflow; (6) is open.

Before wiring this into a repository, read Known defects and Consuming it.

What actually enforces

Of 26 actions, 15 can fail a build and 11 cannot — and the 11 are not one kind of thing. Conflating them was the original error.

Class Actions Meaning

Enforcing (15)

affirmation · boj-cartridge · code-hygiene · formatting · idris2-abi · linguist · manifest · proof-runner · recipes-set · referencing · required-files · secrets · spdx-license · vaulted-tokens · zig-unified-api-adapter

Can fail. A green tick means something.

Advisory (9)

badges · contractile-validation · custom-tools · gitsea · hosting · metrics · tests-benches · trust-humans · www-compliance

Do real work, warn on genuinely soft findings. Failing the estate over a missing Keybase link would be worse than not checking.

Unimplemented (2)

prat · semantic-audit

Stubs. Not referenced by the audit workflow. See (5).

The four language gates added 2026-10-14 (Rust CI, Creusot, SPARK, miniKanren) are enforcing by construction — every check.sh exits 1 on a defect and 2 when no check could be performed — and are classified tier by tier in Language gates below.

formatting and recipes-set moved out of the toothless column; the remaining advisory nine are advisory by design, which is defensible — provided nobody reads their green tick as a guarantee. Renaming them *-advisory would settle that permanently.

Verify at any time:

for a in actions/*/; do
  grep -q 'exit 1' "$a/action.yml" && echo "ENFORCE $(basename $a)" || echo "advise  $(basename $a)"
done

A gate that cannot fail is worse than no gate, because it is credited as assurance. The advisory 13 should either grow teeth or be renamed so nobody reads their green tick as a guarantee.

Known defects

1. FIXED — code-hygiene-check scanned for the word, not the marker. It ran one case-insensitive, unanchored git grep over the whole tree, so “admit” matched “admitted”, “sorry” matched ordinary English, any document discussing a marker failed, and believe_me failed repos whose sanctioned axioms are their declared trusted base. Measured 112 matching files in one repo and 313 in another. Now two scans with different semantics — debt markers case-sensitive and whole-word in source only; circumventions in proof languages only, with comments filtered. Repos may exempt paths via .cicd-hygiene-allow. Result: 112 → 2 and 313 → 3, all true positives.

2. FIXED — required-files-check manufactured filler. Presence-only checking meant the cheapest way to pass was template boilerplate, and that is exactly what happened in the estate. It now checks presence, then format, then substance: documents need real content and no placeholders, ARCHITECTURE must name a directory that actually exists, and MAINTAINERS must mention the repository owner — which catches a template shipping its author’s handle. CODEOWNERS is judged on whether it assigns an owner, not on length.

3. FIXED — the suite contradicted itself. required-files-check hard-failed a repo for lacking GOVERNANCE.md while formatting-check warned that same file should be .adoc. Required-files now accepts every policy-legal form, and formatting-check owns the preference. Verified: a repo passes both gates with .adoc (silently) or with .md (with a nudge).

4. PARTLY FIXED — the toothless column is down from 13 to 11, and now triaged. recipes-set was a stub that printed “Checking Justfile syntax…” with the command commented out and then declared success; it now parse-checks Justfiles and Makefiles and fails on a file that does not parse. formatting gained teeth in (3). The nine remaining advisories are advisory by design and defensible; the honest fix for them is a rename to *-advisory, not teeth.

5. CLOSED — two actions are unimplemented stubs, and the workflow no longer runs them.

  • semantic-audit is pure echo with “Placeholder for actual invocation”; its real body is cicd-squabbler audit --semantic, and cicd-squabbler does not exist yet. It cannot be implemented, only parked.

  • prat claims to validate “PRAT testing”, but PRAT is defined nowhere in the estate — a search of every repository turns up only further copies of the workflow that calls it. Its current check passes any repository that has a tests/ directory or contains the letters “prat” anywhere. It cannot be honestly implemented until somebody says what PRAT is.

A stub that prints success cannot be credited as assurance, so neither step is in main-estate-audit.yml any more. The two directories stay under actions/ for now, for two reasons. Repositories still running a pre-caller copy of the workflow reference them by path. And tests/lock-transitive-closure.sh requires that the SHA the workflow pins serves the whole actions/ tree at HEAD. Move them to draft/ once the estate runs the caller (see Consuming it).

6. OPEN — six actions use bare git grep with no path restriction (idris2-abi, metrics, secrets, spdx-license, vaulted-tokens, zig-unified-api-adapter) and may inherit a milder form of defect (1).

Blast radius

An earlier rollout_estate.sh copied the whole workflow into 199 repositories. Each copy froze at whatever cicd-suite commit its actions.lock held. That is why a gate fixed here kept failing downstream. The composite-shell fix to required-files (#32, 2026-09-22) had still not reached hyperpolymath/marches on 2026-10-14, because its lock held 5a10b72, the commit before it. The caller replaces those copies.

The workflow now has permissions: contents: read and pins actions/checkout and every gate by full SHA.

Consuming it

A repository calls the audit; it does not copy it. Three pieces:

  1. templates/estate-audit-caller.yml becomes .github/workflows/main-estate-audit.yml, with __CICD_SUITE_SHA__ replaced by a full cicd-suite commit SHA:

    jobs:
      estate:
        uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@<40-hex sha> # cicd-suite main

    Pin a full SHA, never @main or a tag: the account enforces sha_pinning_required, and @main would silently change the gate in every consuming repository at once.

  2. The caller must be de-onboarded from the repository’s actions.lock. Onboarded, a cross-repository reusable-workflow call startup-fails with zero jobs. scripts/deonboard-estate-audit.sh <repo> removes the entry and prunes the dependencies only it reached, comparing owner and repository names case-insensitively as GitHub does. It is the estate-audit entry point to scripts/deonboard-workflow.sh, the one implementation every de-onboard goes through. It needs mikefarah yq v4, and it is idempotent. It refuses any actions.lock schema it has not been tested on; tests/deonboard-lock-schemas.sh holds one fixture per supported schema (v0.0.2, v0.0.3) and runs each through both entry points.

  3. templates/track-estate-audit.yml becomes .github/workflows/track-estate-audit.yml. Weekly, it opens a PR that moves the pin to cicd-suite HEAD; that PR’s own audit run is the check. It needs an AUTOMATION_TOKEN secret (a fine-grained token on that repository with Contents, Pull requests and Workflows set to read/write), because GITHUB_TOKEN may not write under .github/workflows/. Its one uses: is step-security/harden-runner at a full SHA (egress to GitHub only); a repository that carries actions.lock must add that record (gh actions-lock) or the first run dies at Set up job.

rollout_estate.sh does all three for every local estate clone. It writes files and does not commit them.

Language gates (Rust, Creusot, SPARK, miniKanren)

Added 2026-10-14. Four reusable workflows, consumed exactly like the estate audit (a thin caller at a full SHA, de-onboarded from actions.lock), and each built so that its oracle has demonstrably said no before its green is credited.

Reusable Check contexts (caller job id, then job name) Oracle

.github/workflows/rust-ci.yml

rust-ci / Detect Cargo.toml · Cargo check + clippy + fmt · Cargo test · Cargo doc (warnings denied) · MSRV check · cargo-deny (advisories, bans, sources) · llvm-cov line coverage (opt-in) · Rust CI verdict

cargo, every call --locked, every compile -D warnings, doctests run, MSRV builds, cargo-deny. The verdict job turns a skipped mandatory job into red.

.github/workflows/creusot-gate.yml

creusot / Detect Creusot obligations · Creusot theatre gate · Creusot proofs (cargo creusot prove) · Creusot verdict

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; otherwise the verdict is VOID (exit 2), never green.

.github/workflows/spark-gate.yml

spark / SPARK theatre gate (standards) · Detect SPARK units · GNATprove · SPARK verdict

standards' SPARK Theatre Gate (claims side, called at a pin, not copied) plus GNATprove at pinned GNAT/GNATprove versions via Alire, --checks-as-errors=on --warnings=error, with the same planted controls.

.github/workflows/kanren-gate.yml

kanren / miniKanren gate

The relations are RUN by the interpreter their dialect names (guile, Chez, racket); relations with no goal-level test fail; impure operators are listed (enforceable); a claim with no relations is named.

Why. From 2026-09-29 every rust-ci / Cargo check + clippy + fmt calling standards' rust-ci-reusable.yml at a pre-fix SHA died in six seconds: the reusable pinned dtolnay/rust-toolchain by commit and passed no toolchain:, and a SHA ref carries no channel (plasma-parser-writer#105). The fix landed upstream; the callers stayed pinned behind it. actions/rust-ci-check/resolve.sh now computes the channel before any action runs and refuses an empty one, and the previous gate’s silent holes are closed: cargo test --all-targets never ran a doctest, nothing denied rustc warnings outside clippy, cargo doc never ran, the declared rust-version was never built, and no supply-chain check ran unless opted in.

Tiers. Within each gate the theatre tier (a claim with nothing behind it) and the oracle tier (the prover or interpreter run) are enforcing and exit 1; the hollow and purity tiers warn by default and become enforcing through an input (enforce_hollow, enforce_zero_contract, enforce_purity, enforce_claims), mirroring standards' SPARK T2. A tree with nothing to gate gets a ::notice:: that nothing ran — never a tick read as assurance. A missing tool is exit 2, "no check was performed".

How the scripts are pinned. Each reusable job reads the caller’s own uses: line back out of the caller’s checked-out workflow file (GITHUB_WORKFLOW_REF names it; inside a reusable the github context is the caller’s), checks this repository out at that SHA into .cicd-suite/ and runs actions/*-check/check.sh from there, after scripts/verify-suite-checkout.sh has proved the checkout is that commit. A caller pinned at a SHA runs exactly that commit’s scripts, with no second pin to drift and no repin commit after a change to actions/. The caller’s tree is read through git ls-files, so the untracked .cicd-suite/ is invisible to it.

Self-test. .github/workflows/language-gates-self-test.yml runs each gate’s test.sh: a fixture, a planted defect per claim, the exact composite shell, and a mutant where one applies. The prover tiers are exercised against stand-in oracles there; the planted controls in the check scripts exercise the real provers on every live run.

Consuming. templates/rust-ci-caller.yml, creusot-gate-caller.yml, spark-gate-caller.yml and kanren-gate-caller.yml become .github/workflows/<name>.yml with __CICD_SUITE_SHA__ replaced; scripts/deonboard-workflow.sh <repo> <workflow-path> de-onboards each (the estate-audit script now delegates to it); templates/track-estate-audit.yml moves every cicd-suite pin weekly by PR. rollout_language_gates.sh does all of it per clone, by what the tree contains. Keep the caller job ids above: they are the context strings branch rules require.

Not yet witnessed live (2026-10-14). The Creusot and GNATprove install steps and the exit-code contract of cargo creusot prove and gnatprove --checks-as-errors=on were validated against the tools' documentation and stand-ins, not against a live runner. The planted controls are the safeguard: if either prover cannot refuse a false contract on the runner, the gate reports VOID rather than green. The first live subject for SPARK is cicd-squabbler’s spark/squabble_gate.gpr; no repository in the first rollout carries Creusot obligations yet.

What a gate may use, and what a consumer’s lock must hold

Two constraints are evaluated in the caller’s repository, so nothing in this repository’s own CI can witness them; both are now guarded here.

  • Actions policy. The estate’s GitHub Actions policy admits actions that are hyperpolymath-owned, GitHub-made, Marketplace-verified, or on a short pattern list. A reusable that uses anything else startup-fails for every caller with "The action … is not allowed" — which is how EmbarkStudios/cargo-deny-action killed the first live Rust gate caller (plasma-parser-writer#108, 2026-10-19) while the Creusot gate from the same commit ran. The gates now use only actions/, github/, hyperpolymath/*, dtolnay, swatinem, goto-bus-stop and taiki-e, every one at a full SHA, and tests/gate-action-owners.sh (run by the self-test workflow) refuses any other owner or a tag pin. cargo-deny is installed through taiki-e/install-action; Alire is a sha256-pinned release binary rather than alire-project/setup-alire, which also nested floating @v4 tags.

  • Callee lock. Since about 2026-10-15 GitHub validates a called reusable against the callee repository’s actions.lock at the called SHA and rejects a dependency record whose ref: is its own commit SHA ("invalid lockfile pin"). The gate workflows are deliberately not keyed in this repository’s lock, and that resolves (witnessed: the Creusot gate on plasma-parser-writer#108). The SPARK gate’s nested standards theatre gate is pinned at standards 75bd599, the first standards commit whose lock passes that validation; hypatia’s PIN-003 lists the 545 that do not.

  • Consumers with a lock-sync gate. A repository whose CI requires every job-level reusable ref to be keyed in its own actions.lock with a transitively closed dependencies: section (cicd-squabbler’s scripts/check-lock-sync.sh) cannot de-onboard the caller as the templates assume. Such a repository onboards instead: one hyperpolymath/cicd-suite@<sha> record whose uses: is the union of what the called gates use at that SHA, plus a record for each of those copied from a lock GitHub accepts, with the tag — never the SHA — as ref:. cicd-squabbler#135 is the worked example (for its standards callers); gitbot-fleet’s scripts/fix-lock-self-sha-refs.sh and scripts/lib/action-ref-tags.tsv carry the tag map.

Licence

Code MPL-2.0, prose CC-BY-SA-4.0. See LICENSE.

About

Composite GitHub Actions for estate-wide CI/CD auditing — required files, code hygiene, SPDX, proofs, manifests, secrets. Consumed by main-estate-audit.yml.

Topics

Resources

Code of conduct

Contributing

Security policy

Stars

2 stars

Watchers

0 watching

Forks

Releases

Sponsor this project

Packages

Used by

Contributors

Languages