From afc14b7362d75d6cb9643189783cc6b08d21e039 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 13:45:20 +0000 Subject: [PATCH] feat(gates): strict Rust CI, Creusot, SPARK and miniKanren reusable gates 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 Claude-Session: https://claude.ai/code/session_01Xn9nqHVbUTRLgBdedoXAc8 --- .github/workflows/actions.lock | 2 + .github/workflows/creusot-gate.yml | 309 +++++++++ .github/workflows/kanren-gate.yml | 134 ++++ .../workflows/language-gates-self-test.yml | 108 +++ .github/workflows/rust-ci.yml | 641 ++++++++++++++++++ .github/workflows/spark-gate.yml | 272 ++++++++ ARCHITECTURE.adoc | 27 + README.adoc | 103 +++ actions/creusot-check/action.yml | 36 + actions/creusot-check/check.sh | 246 +++++++ actions/creusot-check/test.sh | 134 ++++ actions/kanren-check/action.yml | 36 + actions/kanren-check/check.sh | 199 ++++++ actions/kanren-check/test.sh | 182 +++++ actions/rust-ci-check/action.yml | 55 ++ actions/rust-ci-check/check.sh | 141 ++++ actions/rust-ci-check/resolve.sh | 110 +++ actions/rust-ci-check/test.sh | 175 +++++ actions/spark-check/action.yml | 45 ++ actions/spark-check/check.sh | 174 +++++ actions/spark-check/test.sh | 134 ++++ rollout_language_gates.sh | 73 ++ scripts/deonboard-estate-audit.sh | 51 +- scripts/deonboard-workflow.sh | 61 ++ scripts/verify-suite-checkout.sh | 36 + templates/creusot-gate-caller.yml | 33 + templates/kanren-gate-caller.yml | 33 + templates/rust-ci-caller.yml | 44 ++ templates/spark-gate-caller.yml | 37 + templates/track-estate-audit.yml | 59 +- tests/lock-transitive-closure.sh | 39 +- 31 files changed, 3653 insertions(+), 76 deletions(-) create mode 100644 .github/workflows/creusot-gate.yml create mode 100644 .github/workflows/kanren-gate.yml create mode 100644 .github/workflows/language-gates-self-test.yml create mode 100644 .github/workflows/rust-ci.yml create mode 100644 .github/workflows/spark-gate.yml create mode 100644 actions/creusot-check/action.yml create mode 100755 actions/creusot-check/check.sh create mode 100755 actions/creusot-check/test.sh create mode 100644 actions/kanren-check/action.yml create mode 100755 actions/kanren-check/check.sh create mode 100755 actions/kanren-check/test.sh create mode 100644 actions/rust-ci-check/action.yml create mode 100755 actions/rust-ci-check/check.sh create mode 100755 actions/rust-ci-check/resolve.sh create mode 100755 actions/rust-ci-check/test.sh create mode 100644 actions/spark-check/action.yml create mode 100755 actions/spark-check/check.sh create mode 100755 actions/spark-check/test.sh create mode 100755 rollout_language_gates.sh create mode 100755 scripts/deonboard-workflow.sh create mode 100755 scripts/verify-suite-checkout.sh create mode 100644 templates/creusot-gate-caller.yml create mode 100644 templates/kanren-gate-caller.yml create mode 100644 templates/rust-ci-caller.yml create mode 100644 templates/spark-gate-caller.yml diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 0d0455a..6fecabc 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -9,6 +9,8 @@ workflows: - 'hyperpolymath/k9-ecosystem@2155aa26a21758f2ba119f61bc7e0e1981c106fb' '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] + '.github/workflows/language-gates-self-test.yml': + - 'actions/checkout@v7.0.1' dependencies: 'actions/checkout@v7.0.1': ref: 'v7.0.1' diff --git a/.github/workflows/creusot-gate.yml b/.github/workflows/creusot-gate.yml new file mode 100644 index 0000000..e63a7ba --- /dev/null +++ b/.github/workflows/creusot-gate.yml @@ -0,0 +1,309 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# creusot-gate.yml — Rust deductive verification (Creusot), as a reusable +# workflow. The Rust twin of spark-gate.yml, and the "reusable verifier gate +# with a planted failing contract" that hyperpolymath/standards#692 asks for. +# +# detect facts about the tree (obligations? claims? which crates?) +# theatre a "verified with Creusot" claim with no contracts behind it is +# a hard failure (T1); a creusot-std dependency that annotates +# nothing is named (T2, warning unless enforce_hollow); every +# #[trusted] axiom is listed (T3, the proof's residue) +# prove installs Creusot at a PINNED release (opam switch cached), proves +# a planted FALSE contract and REQUIRES the prover to refuse it, +# proves a planted TRUE one and requires success, and only then +# runs `cargo creusot prove` in every crate with obligations +# verdict one context to require; a skipped prove with obligations present +# is VOID, not green +# +# Creusot + nightly pairing: Creusot is built against one specific nightly +# (its rust-toolchain file). v0.14.0 (2026-10-12) pairs with +# nightly-2026-08-03. Move both inputs together; the install step installs +# the clone's own pin regardless, so a mismatch costs time, not soundness. +# +# Gate scripts are pinned at the caller's own `uses:` SHA — see rust-ci.yml. + +name: Creusot Gate (reusable) + +on: + workflow_call: + inputs: + runs-on: + type: string + required: false + default: ubuntu-24.04 + working_directory: + description: Tree root to scan (Cargo manifests are found beneath it) + type: string + required: false + default: "." + creusot_version: + description: Creusot release tag to install (without the leading v) + type: string + required: false + default: "0.14.0" + rust_nightly: + description: The nightly Creusot is built against (must match the release) + type: string + required: false + default: "nightly-2026-08-03" + enforce_hollow: + description: Fail (not warn) when creusot-std is a dependency but no contract exists + type: boolean + required: false + default: false + prove_args: + description: Extra arguments for `cargo creusot prove` + type: string + required: false + default: "" + +permissions: + contents: read + +# Every `run:` step gets bash with -e AND pipefail. GitHub's default when no +# shell is named is `bash -e` without pipefail, which would let a failing +# gate script hide behind the `| tee` that records its facts. +defaults: + run: + shell: bash + +jobs: + detect: + name: Detect Creusot obligations + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + permissions: + contents: read + outputs: + obligations: ${{ steps.facts.outputs.obligations }} + claims: ${{ steps.facts.outputs.claims }} + creusot_version: ${{ steps.facts.outputs.creusot_version }} + contract_count: ${{ steps.facts.outputs.contract_count }} + trusted_count: ${{ steps.facts.outputs.trusted_count }} + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: creusot-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Facts + id: facts + env: + CREUSOT_GATE_PHASE: detect + WORKING_DIRECTORY: ${{ inputs.working_directory }} + run: bash .cicd-suite/actions/creusot-check/check.sh | tee -a "$GITHUB_OUTPUT" + + theatre: + name: Creusot theatre gate + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + needs: detect + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: creusot-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Claims must be backed by contracts + env: + CREUSOT_GATE_PHASE: theatre + WORKING_DIRECTORY: ${{ inputs.working_directory }} + ENFORCE_HOLLOW: ${{ inputs.enforce_hollow }} + run: bash .cicd-suite/actions/creusot-check/check.sh + + prove: + name: Creusot proofs (cargo creusot prove) + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 90 + needs: [detect, theatre] + if: ${{ needs.detect.outputs.obligations == 'true' }} + permissions: + contents: read + env: + CREUSOT_VERSION: ${{ inputs.creusot_version }} + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: creusot-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install the nightly Creusot ${{ inputs.creusot_version }} is built against + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ inputs.rust_nightly }} + components: rustfmt, rustc-dev, llvm-tools + - name: Install opam and Creusot's system dependencies + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y --no-install-recommends opam libzmq3-dev libgmp-dev pkg-config autoconf + - name: Cache the Creusot opam switch, provers and cargo-creusot + id: cache + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: | + ~/.local/share/creusot + ~/.cargo/bin/cargo-creusot + ~/.cargo/bin/creusot-rustc + ~/.config/creusot + key: creusot-${{ inputs.creusot_version }}-${{ inputs.rust_nightly }}-${{ runner.os }}-${{ runner.arch }} + - name: Install Creusot v${{ inputs.creusot_version }} (clone at the tag, ./INSTALL) + if: ${{ steps.cache.outputs.cache-hit != 'true' }} + run: | + set -euo pipefail + opam init --bare -y --disable-sandboxing + git clone --depth 1 --branch "v${CREUSOT_VERSION}" https://github.com/creusot-rs/creusot "$RUNNER_TEMP/creusot" + cd "$RUNNER_TEMP/creusot" + ./INSTALL + - name: cargo creusot is on PATH + run: | + set -euo pipefail + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + export PATH="$HOME/.cargo/bin:$PATH" + cargo creusot --help >/dev/null + cargo creusot setup status || true + - name: Planted controls, then every crate with obligations + env: + CREUSOT_GATE_PHASE: prove + WORKING_DIRECTORY: ${{ inputs.working_directory }} + PROVE_ARGS: ${{ inputs.prove_args }} + run: bash .cicd-suite/actions/creusot-check/check.sh + + verdict: + name: Creusot verdict + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + needs: [detect, theatre, prove] + if: ${{ always() }} + permissions: + contents: read + env: + OBLIGATIONS: ${{ needs.detect.outputs.obligations }} + CLAIMS: ${{ needs.detect.outputs.claims }} + TRUSTED: ${{ needs.detect.outputs.trusted_count }} + R_DETECT: ${{ needs.detect.result }} + R_THEATRE: ${{ needs.theatre.result }} + R_PROVE: ${{ needs.prove.result }} + steps: + - name: Adjudicate + run: | + set -euo pipefail + fail=0 + [ "$R_DETECT" = success ] || { echo "::error::detect: $R_DETECT"; fail=1; } + [ "$R_THEATRE" = success ] || { echo "::error::theatre: $R_THEATRE"; fail=1; } + case "$R_PROVE" in + success) echo " ok prove (trusted axioms: ${TRUSTED:-?})" ;; + failure|cancelled) echo "::error::prove: $R_PROVE"; fail=1 ;; + skipped) + if [ "$OBLIGATIONS" = true ]; then + echo "::error::prove was SKIPPED although obligations exist — VOID, not green."; fail=1 + else + echo "::notice::No Creusot obligations in this tree: nothing was proved. This verdict is silent, not green-as-assurance (claims=${CLAIMS:-false})." + fi ;; + *) echo "::error::prove: unknown result '$R_PROVE'"; fail=1 ;; + esac + [ "$fail" -eq 0 ] || { echo "::error::Creusot verdict: RED."; exit 1; } + echo "Creusot verdict: GREEN." diff --git a/.github/workflows/kanren-gate.yml b/.github/workflows/kanren-gate.yml new file mode 100644 index 0000000..117f327 --- /dev/null +++ b/.github/workflows/kanren-gate.yml @@ -0,0 +1,134 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# kanren-gate.yml — miniKanren / relational code, as a reusable workflow. +# +# One job: actions/kanren-check/check.sh finds relational sources (Scheme +# family and Rust kanren crates), fails when relations have no goal-level +# test, EXECUTES every relational test with the interpreter the file's +# dialect names, lists impure operators (conda/condu/project/…), and names a +# miniKanren claim that has no relations behind it. A missing interpreter is +# exit 2 — no check was performed — never a pass. +# +# `interpreters` installs what the sources need. The estate's miniKanren is +# Guile Scheme (archived state-kanren.scm; cicd-squabbler's Reasoner design), +# so guile is the default; add chez and/or racket for those dialects. +# +# Gate scripts are pinned at the caller's own `uses:` SHA — see rust-ci.yml. + +name: miniKanren Gate (reusable) + +on: + workflow_call: + inputs: + runs-on: + type: string + required: false + default: ubuntu-24.04 + working_directory: + type: string + required: false + default: "." + interpreters: + description: Space-separated subset of "guile chez racket" to install + type: string + required: false + default: "guile" + require_tests: + description: Fail when relational sources have no relational test + type: boolean + required: false + default: true + enforce_purity: + description: Fail on conda/condu/project/onceo/ifa/ifu/copy-term + type: boolean + required: false + default: false + enforce_claims: + description: Fail on a miniKanren claim with no relational sources + type: boolean + required: false + default: false + +permissions: + contents: read + +# Every `run:` step gets bash with -e AND pipefail. GitHub's default when no +# shell is named is `bash -e` without pipefail, which would let a failing +# gate script hide behind the `| tee` that records its facts. +defaults: + run: + shell: bash + +jobs: + kanren: + name: miniKanren gate + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 30 + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: kanren-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install the requested interpreters + env: + INTERPRETERS: ${{ inputs.interpreters }} + run: | + set -euo pipefail + pkgs="" + for i in $INTERPRETERS; do + case "$i" in + guile) pkgs="$pkgs guile-3.0" ;; + chez) pkgs="$pkgs chezscheme" ;; + racket) pkgs="$pkgs racket" ;; + *) echo "::error::unknown interpreter '$i' (guile|chez|racket)"; exit 2 ;; + esac + done + if [ -n "$pkgs" ]; then + sudo apt-get update + # shellcheck disable=SC2086 + sudo apt-get install -y --no-install-recommends $pkgs + fi + - name: Run the relations + env: + WORKING_DIRECTORY: ${{ inputs.working_directory }} + REQUIRE_TESTS: ${{ inputs.require_tests }} + ENFORCE_PURITY: ${{ inputs.enforce_purity }} + ENFORCE_CLAIMS: ${{ inputs.enforce_claims }} + run: bash .cicd-suite/actions/kanren-check/check.sh diff --git a/.github/workflows/language-gates-self-test.yml b/.github/workflows/language-gates-self-test.yml new file mode 100644 index 0000000..1e715d5 --- /dev/null +++ b/.github/workflows/language-gates-self-test.yml @@ -0,0 +1,108 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# language-gates-self-test.yml — the four language gates must be able to +# FAIL, for each thing they claim to check, before any consumer calls them. +# +# This repository has no Rust, Ada or Scheme of its own, so a self-run of +# the reusables would be silent and prove nothing. Instead each gate's +# test.sh builds a fixture, plants a defect, asserts the gate goes red for +# that defect under the exact composite shell, and kills a mutant where one +# exists (tests/composite-shell-contract.sh explains the -e trap that made +# that necessary). The prover tiers run against stand-in oracles here; the +# planted controls inside the check scripts exercise the real provers on +# every live run. + +name: Language Gates Self-Test + +on: + push: + branches: [main] + paths: + - "actions/rust-ci-check/**" + - "actions/creusot-check/**" + - "actions/spark-check/**" + - "actions/kanren-check/**" + - "scripts/verify-suite-checkout.sh" + - "scripts/deonboard-workflow.sh" + - ".github/workflows/rust-ci.yml" + - ".github/workflows/creusot-gate.yml" + - ".github/workflows/spark-gate.yml" + - ".github/workflows/kanren-gate.yml" + - ".github/workflows/language-gates-self-test.yml" + - "templates/**" + pull_request: + paths: + - "actions/rust-ci-check/**" + - "actions/creusot-check/**" + - "actions/spark-check/**" + - "actions/kanren-check/**" + - "scripts/verify-suite-checkout.sh" + - "scripts/deonboard-workflow.sh" + - ".github/workflows/rust-ci.yml" + - ".github/workflows/creusot-gate.yml" + - ".github/workflows/spark-gate.yml" + - ".github/workflows/kanren-gate.yml" + - ".github/workflows/language-gates-self-test.yml" + - "templates/**" + +permissions: + contents: read + +# Every `run:` step gets bash with -e AND pipefail. GitHub's default when no +# shell is named is `bash -e` without pipefail, which would let a failing +# gate script hide behind the `| tee` that records its facts. +defaults: + run: + shell: bash + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + gates: + name: Each gate can fail for what it checks + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - name: Interpreters and linters the suites need + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y --no-install-recommends guile-3.0 shellcheck + rustup component add clippy rustfmt + - name: Every gate script parses and is shellcheck-clean + run: | + set -euo pipefail + for f in actions/rust-ci-check/*.sh actions/creusot-check/*.sh actions/spark-check/*.sh actions/kanren-check/*.sh scripts/verify-suite-checkout.sh scripts/deonboard-workflow.sh rollout_language_gates.sh; do + bash -n "$f" + done + shellcheck -S warning actions/rust-ci-check/*.sh actions/creusot-check/*.sh actions/spark-check/*.sh actions/kanren-check/*.sh scripts/verify-suite-checkout.sh scripts/deonboard-workflow.sh rollout_language_gates.sh + - name: The suite-checkout verifier refuses an empty or wrong SHA + run: | + set -euo pipefail + rc=0; EXPECTED= SUITE_DIR=. bash scripts/verify-suite-checkout.sh || rc=$? + [ "$rc" -eq 2 ] || { echo "verifier accepted an empty SHA (rc=$rc)"; exit 1; } + rc=0; EXPECTED=0000000000000000000000000000000000000000 SUITE_DIR=. bash scripts/verify-suite-checkout.sh || rc=$? + [ "$rc" -eq 2 ] || { echo "verifier accepted a wrong SHA (rc=$rc)"; exit 1; } + EXPECTED="$(git rev-parse HEAD)" SUITE_DIR=. bash scripts/verify-suite-checkout.sh + - name: Rust gate + run: bash actions/rust-ci-check/test.sh + - name: Creusot gate + run: bash actions/creusot-check/test.sh + - name: SPARK gate + run: bash actions/spark-check/test.sh + - name: miniKanren gate + run: bash actions/kanren-check/test.sh + - name: Caller templates carry the placeholder, a full-SHA form and no secrets + run: | + set -euo pipefail + for t in templates/rust-ci-caller.yml templates/creusot-gate-caller.yml templates/spark-gate-caller.yml templates/kanren-gate-caller.yml; do + grep -qE 'uses: hyperpolymath/cicd-suite/\.github/workflows/[a-z-]+\.yml@__CICD_SUITE_SHA__' "$t" \ + || { echo "$t does not call a cicd-suite reusable at __CICD_SUITE_SHA__"; exit 1; } + ! grep -qE '^\s*secrets:' "$t" || { echo "$t hands secrets to a reusable that consumes none"; exit 1; } + done diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml new file mode 100644 index 0000000..1fa9aab --- /dev/null +++ b/.github/workflows/rust-ci.yml @@ -0,0 +1,641 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# rust-ci.yml — the estate's strict Rust gate, as a reusable workflow. +# +# WHY THIS EXISTS. From 2026-09-29 every `rust-ci / Cargo check + clippy + +# fmt` in the estate that called hyperpolymath/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, so the action exited 1 with "'toolchain' is a +# required input" before a compiler existed (plasma-parser-writer#105, +# run 38564229091). The fix landed in standards; the callers stayed pinned +# behind it. This workflow makes that class of failure impossible by +# construction: the channel is RESOLVED by actions/rust-ci-check/resolve.sh +# before any action runs and the gate refuses an empty value. +# +# WHAT IS STRICTER THAN BEFORE (actions/rust-ci-check/check.sh has the why): +# * every compile denies warnings (RUSTFLAGS/RUSTDOCFLAGS -D warnings), +# not only clippy; +# * doctests run (`cargo test --all-targets` never ran a single `///`); +# * `cargo doc` with broken intra-doc links fails; +# * the declared `rust-version` (MSRV) must actually build; +# * cargo-deny runs by default: advisories, bans, sources (licences only +# with an owner-authored deny.toml — the gate never invents licence +# policy, doctrine #6); +# * a missing Cargo.lock fails with the fix named, before cargo runs; +# * a final `Rust CI verdict` job turns a SKIPPED mandatory job into a +# failure: a gate that did not run is VOID, not green +# (proven-tests-and-benches, corpus unit cancelled-gate-void). +# +# CONTEXT NAMES ARE PRESERVED. Callers keep the job id `rust-ci`, so the +# contexts `rust-ci / Detect Cargo.toml`, `rust-ci / Cargo check + clippy + +# fmt` and `rust-ci / Cargo test` are the same strings branch rules already +# require (standards docs/CICD-SIGNAL-DISCIPLINE.adoc: never rename and +# re-require in one step). New contexts are additive. +# +# HOW THE GATE SCRIPTS ARE PINNED. Every 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/, verifies the checkout is +# that commit, and runs the scripts from there. A caller pinned at a SHA therefore runs exactly that +# commit's scripts: no second pin to drift, no repin commit after every +# change to actions/ (the defect tests/lock-transitive-closure.sh guards +# against for `uses:`-form composites). The caller's tree is untouched: the +# scripts read `git ls-files`, and .cicd-suite/ is untracked. +# +# CONSUMING IT. templates/rust-ci-caller.yml, pinned at a full cicd-suite +# SHA and DE-ONBOARDED from the caller's actions.lock (an onboarded +# cross-repo reusable startup-fails with zero jobs under +# sha_pinning_required — see main-estate-audit.yml's header for the +# witnessed matrix). This file is likewise de-onboarded here: every `uses:` +# below is a full SHA. + +name: Rust CI (reusable) + +on: + workflow_call: + inputs: + runs-on: + description: Runner label for every job + type: string + required: false + default: ubuntu-24.04 + working_directory: + description: Directory containing Cargo.toml (relative to the repo root) + type: string + required: false + default: "." + toolchain: + description: >- + Rust channel for the gate. "auto" (default) reads rust-toolchain.toml / + rust-toolchain and falls back to stable. Never empty: an empty channel + fails the detect job. + type: string + required: false + default: auto + components: + description: rustup components for the check job + type: string + required: false + default: "clippy, rustfmt" + check_args: + description: Args appended to `cargo check` + type: string + required: false + default: "--all-targets" + clippy_args: + description: Args appended to `cargo clippy` + type: string + required: false + default: "--all-targets -- -D warnings" + test_args: + description: Args appended to `cargo test` + type: string + required: false + default: "--all-targets" + doctests: + description: Also run `cargo test --doc --workspace` (recommended; --all-targets skips doctests) + type: boolean + required: false + default: true + deny_warnings: + description: Export RUSTFLAGS/RUSTDOCFLAGS "-D warnings" for every compile + type: boolean + required: false + default: true + doc_check: + description: Run `cargo doc --no-deps --document-private-items` with warnings denied + type: boolean + required: false + default: true + msrv_check: + description: Build with the declared `rust-version` when the manifest declares one + type: boolean + required: false + default: true + deny_check: + description: Run cargo-deny (advisories, bans, sources; licences only with a deny.toml) + type: boolean + required: false + default: true + deny_args: + description: Global cargo-deny arguments (placed before the command) + type: string + required: false + default: "--all-features --locked --warn unmaintained --warn yanked" + enable_audit: + description: >- + Accepted for compatibility with standards' rust-ci-reusable; advisories + now always run through cargo-deny (see deny_check), so this input is a + no-op. + type: boolean + required: false + default: false + enable_coverage: + description: Measure line coverage with cargo-llvm-cov and enforce coverage_floor + type: boolean + required: false + default: false + coverage_floor: + description: Minimum line-coverage percent when enable_coverage is set; ratchet upward, never lower + type: string + required: false + default: "0" + zig_version: + description: Exact Zig version for a crate with a Zig-native build; empty for pure Rust + type: string + required: false + default: "" + +# Only `contents: read`. A reusable may narrow the caller's permissions, never +# widen them: asking for more than the caller granted is a startup_failure +# with zero jobs (standards rust-ci-reusable.yml, header). +permissions: + contents: read + +# Every `run:` step gets bash with -e AND pipefail. GitHub's default when no +# shell is named is `bash -e` without pipefail, which would let a failing +# gate script hide behind the `| tee` that records its facts. +defaults: + run: + shell: bash + +jobs: + detect: + name: Detect Cargo.toml + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + permissions: + contents: read + outputs: + has_cargo: ${{ steps.facts.outputs.has_cargo }} + toolchain: ${{ steps.facts.outputs.toolchain }} + toolchain_source: ${{ steps.facts.outputs.toolchain_source }} + msrv: ${{ steps.facts.outputs.msrv }} + has_lock: ${{ steps.facts.outputs.has_lock }} + has_deny_toml: ${{ steps.facts.outputs.has_deny_toml }} + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: rust-ci.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Resolve toolchain, MSRV and lockfile facts + id: facts + env: + WORKING_DIRECTORY: ${{ inputs.working_directory }} + TOOLCHAIN: ${{ inputs.toolchain }} + run: bash .cicd-suite/actions/rust-ci-check/resolve.sh | tee -a "$GITHUB_OUTPUT" + + check: + name: Cargo check + clippy + fmt + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 30 + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: rust-ci.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install Rust ${{ needs.detect.outputs.toolchain }} (${{ needs.detect.outputs.toolchain_source }}) + # `toolchain:` is ALWAYS passed: a SHA-pinned dtolnay/rust-toolchain + # has no channel of its own and fails without it. detect refuses to + # emit an empty value, so this can never be the silent "" that + # killed the estate's rust-ci on 2026-09-29. + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ needs.detect.outputs.toolchain }} + components: ${{ inputs.components }} + - name: Install Zig for a native build + if: ${{ inputs.zig_version != '' }} + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + with: + version: ${{ inputs.zig_version }} + - name: Cache cargo registry and build + uses: swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 + with: + workspaces: ${{ inputs.working_directory }} + - name: cargo check, cargo fmt --check, cargo clippy -D warnings (all --locked) + env: + RUST_GATE_PHASE: check + WORKING_DIRECTORY: ${{ inputs.working_directory }} + CHECK_ARGS: ${{ inputs.check_args }} + CLIPPY_ARGS: ${{ inputs.clippy_args }} + DENY_WARNINGS: ${{ inputs.deny_warnings }} + run: bash .cicd-suite/actions/rust-ci-check/check.sh + + test: + name: Cargo test + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 30 + needs: [detect, check] + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: rust-ci.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install Rust ${{ needs.detect.outputs.toolchain }} + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ needs.detect.outputs.toolchain }} + - name: Install Zig for a native build + if: ${{ inputs.zig_version != '' }} + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + with: + version: ${{ inputs.zig_version }} + - name: Cache cargo registry and build + uses: swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 + with: + workspaces: ${{ inputs.working_directory }} + - name: cargo test (all targets) and cargo test --doc, --locked + env: + RUST_GATE_PHASE: test + WORKING_DIRECTORY: ${{ inputs.working_directory }} + TEST_ARGS: ${{ inputs.test_args }} + DOCTESTS: ${{ inputs.doctests }} + DENY_WARNINGS: ${{ inputs.deny_warnings }} + run: bash .cicd-suite/actions/rust-ci-check/check.sh + + doc: + name: Cargo doc (warnings denied) + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 20 + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' && inputs.doc_check }} + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: rust-ci.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install Rust ${{ needs.detect.outputs.toolchain }} + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ needs.detect.outputs.toolchain }} + - name: Install Zig for a native build + if: ${{ inputs.zig_version != '' }} + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + with: + version: ${{ inputs.zig_version }} + - name: Cache cargo registry and build + uses: swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 + with: + workspaces: ${{ inputs.working_directory }} + - name: cargo doc --no-deps --document-private-items, RUSTDOCFLAGS -D warnings + env: + RUST_GATE_PHASE: doc + WORKING_DIRECTORY: ${{ inputs.working_directory }} + DENY_WARNINGS: ${{ inputs.deny_warnings }} + run: bash .cicd-suite/actions/rust-ci-check/check.sh + + msrv: + name: MSRV check (rust-version ${{ needs.detect.outputs.msrv }}) + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 30 + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' && inputs.msrv_check && needs.detect.outputs.msrv != '' }} + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: rust-ci.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Install the declared rust-version ${{ needs.detect.outputs.msrv }} + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ needs.detect.outputs.msrv }} + - name: Install Zig for a native build + if: ${{ inputs.zig_version != '' }} + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + with: + version: ${{ inputs.zig_version }} + - name: Cache cargo registry and build + uses: swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 + with: + workspaces: ${{ inputs.working_directory }} + key: msrv-${{ needs.detect.outputs.msrv }} + - name: cargo +${{ needs.detect.outputs.msrv }} check --locked + env: + RUST_GATE_PHASE: msrv + MSRV: ${{ needs.detect.outputs.msrv }} + WORKING_DIRECTORY: ${{ inputs.working_directory }} + CHECK_ARGS: ${{ inputs.check_args }} + DENY_WARNINGS: ${{ inputs.deny_warnings }} + run: bash .cicd-suite/actions/rust-ci-check/check.sh + + deny: + name: cargo-deny (advisories, bans, sources) + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 15 + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' && inputs.deny_check }} + permissions: + contents: read + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: cargo-deny — advisories, bans, sources + uses: EmbarkStudios/cargo-deny-action@3c6349835b2b7b196a839186cb8b78e02f7b5f25 # v2.1.1 + with: + command: check advisories bans sources + arguments: ${{ inputs.deny_args }} + manifest-path: ${{ inputs.working_directory }}/Cargo.toml + - name: cargo-deny — licences (only against an owner-authored deny.toml) + # Licence policy is manual and owner-only (doctrine #6). With no + # deny.toml there is no policy to check against, and the gate does + # not invent one. + if: ${{ needs.detect.outputs.has_deny_toml == 'true' }} + uses: EmbarkStudios/cargo-deny-action@3c6349835b2b7b196a839186cb8b78e02f7b5f25 # v2.1.1 + with: + command: check licenses + arguments: ${{ inputs.deny_args }} + manifest-path: ${{ inputs.working_directory }}/Cargo.toml + + coverage: + name: llvm-cov line coverage + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 30 + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' && inputs.enable_coverage }} + permissions: + contents: read + defaults: + run: + working-directory: ${{ inputs.working_directory }} + env: + FLOOR: ${{ inputs.coverage_floor }} + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Install Rust ${{ needs.detect.outputs.toolchain }} with llvm-tools + uses: dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f # master 2026-08-04 (v1) + with: + toolchain: ${{ needs.detect.outputs.toolchain }} + components: llvm-tools-preview + - name: Install Zig for a native build + if: ${{ inputs.zig_version != '' }} + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + with: + version: ${{ inputs.zig_version }} + - name: Install cargo-llvm-cov (prebuilt, pinned) + uses: taiki-e/install-action@1168f6810a3cb30a3514bf5756a3b7f0422c6df8 # v2.87.28 + with: + tool: cargo-llvm-cov + - name: Measure line coverage + id: cov + run: | + set -euo pipefail + cargo llvm-cov --workspace --locked --json --output-path cov.json + PCT=$(jq -r '.data[0].totals.lines.percent' cov.json) + printf '### Line coverage: %.2f%% (floor %s%%)\n' "$PCT" "$FLOOR" >> "$GITHUB_STEP_SUMMARY" + echo "pct=$PCT" >> "$GITHUB_OUTPUT" + - name: Enforce the ratchet floor + env: + PCT: ${{ steps.cov.outputs.pct }} + run: | + set -euo pipefail + awk -v p="$PCT" -v f="$FLOOR" 'BEGIN { + if (p + 0 < f + 0) { printf "FAIL: line coverage %.2f%% is below floor %s%%\n", p, f; exit 1 } + printf "OK: line coverage %.2f%% >= floor %s%%\n", p, f + }' + + verdict: + # One context to require. Red if any gate failed, was cancelled, or was + # SKIPPED while expected to run: a job that never ran proved nothing, and + # a green tick over it would be the cancelled-gate-void defect. + name: Rust CI verdict + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + needs: [detect, check, test, doc, msrv, deny, coverage] + if: ${{ always() }} + permissions: + contents: read + env: + HAS_CARGO: ${{ needs.detect.outputs.has_cargo }} + MSRV: ${{ needs.detect.outputs.msrv }} + R_DETECT: ${{ needs.detect.result }} + R_CHECK: ${{ needs.check.result }} + R_TEST: ${{ needs.test.result }} + R_DOC: ${{ needs.doc.result }} + R_MSRV: ${{ needs.msrv.result }} + R_DENY: ${{ needs.deny.result }} + R_COVERAGE: ${{ needs.coverage.result }} + WANT_DOC: ${{ inputs.doc_check }} + WANT_MSRV: ${{ inputs.msrv_check }} + WANT_DENY: ${{ inputs.deny_check }} + WANT_COVERAGE: ${{ inputs.enable_coverage }} + steps: + - name: Adjudicate + run: | + set -euo pipefail + fail=0 + verdict() { # + local job="$1" result="$2" expected="$3" + case "$result" in + success) echo " ok $job" ;; + failure|cancelled) echo "::error::$job: $result"; fail=1 ;; + skipped) + if [ "$expected" = true ]; then + echo "::error::$job was SKIPPED but was expected to run — a gate that did not run is VOID, not green (proven-tests-and-benches: cancelled-gate-void)." + fail=1 + else + echo " skipped $job (not requested)" + fi ;; + *) echo "::error::$job: unknown result '$result'"; fail=1 ;; + esac + } + [ "$R_DETECT" = success ] || { echo "::error::detect: $R_DETECT — the toolchain/MSRV facts were not established."; fail=1; } + if [ "$HAS_CARGO" != true ]; then + echo "::notice::No Cargo.toml at the configured working_directory: no Rust gate ran. This verdict is silent, not green-as-assurance." + exit "$fail" + fi + verdict check "$R_CHECK" true + verdict test "$R_TEST" true + verdict doc "$R_DOC" "$WANT_DOC" + if [ -n "$MSRV" ]; then verdict msrv "$R_MSRV" "$WANT_MSRV"; else echo " skipped msrv (no rust-version declared)"; fi + verdict deny "$R_DENY" "$WANT_DENY" + verdict coverage "$R_COVERAGE" "$WANT_COVERAGE" + [ "$fail" -eq 0 ] || { echo "::error::Rust CI verdict: RED."; exit 1; } + echo "Rust CI verdict: GREEN — every requested gate ran and passed." diff --git a/.github/workflows/spark-gate.yml b/.github/workflows/spark-gate.yml new file mode 100644 index 0000000..8736f89 --- /dev/null +++ b/.github/workflows/spark-gate.yml @@ -0,0 +1,272 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# spark-gate.yml — Ada/SPARK formal verification, as a reusable workflow. +# The Ada twin of creusot-gate.yml. +# +# theatre hyperpolymath/standards' SPARK Theatre Gate (the claims side): +# a SPARK_Mode-On unit whose header claims "formally verified" +# with no GNATprove in the repository is a hard failure, and a +# zero-contract SPARK_Mode is named (escalates with +# enforce_zero_contract). Called as a nested reusable, pinned, +# rather than copied: solutions at source. +# detect counts SPARK_Mode-On units and names the project GNATprove gets; +# with several .gpr and no `gpr` input it fails rather than guess +# prove installs GNAT + GNATprove at PINNED versions through Alire, +# proves a planted FALSE postcondition and REQUIRES refusal, proves +# a planted TRUE one and requires success, then runs +# gnatprove -P --mode=all --level=N --checks-as-errors=on +# --warnings=error --report=all --timeout=T -j0 +# failing on any unproved check +# verdict one context to require; a skipped prove with units present is +# VOID, not green +# +# Gate scripts are pinned at the caller's own `uses:` SHA — see rust-ci.yml. +# +# Permissions: the theatre job calls a standards reusable that declares +# `actions: read` + `contents: read`; a nested call may not request more +# than its caller holds, so this file and its callers grant both. + +name: SPARK Gate (reusable) + +on: + workflow_call: + inputs: + runs-on: + type: string + required: false + default: ubuntu-24.04 + working_directory: + description: Tree root to scan + type: string + required: false + default: "." + gpr: + description: Project file for gnatprove (required when several .gpr files exist) + type: string + required: false + default: "" + level: + description: gnatprove --level (0..4) + type: string + required: false + default: "2" + timeout: + description: gnatprove --timeout, seconds per verification condition + type: string + required: false + default: "60" + extra_args: + description: Extra gnatprove arguments + type: string + required: false + default: "" + enforce_zero_contract: + description: Escalate the theatre gate's T2 (SPARK_Mode with no contracts) to a failure + type: boolean + required: false + default: false + gnat_version: + description: Alire gnat_native crate version + type: string + required: false + default: "16.1.0" + gnatprove_version: + description: Alire gnatprove crate version + type: string + required: false + default: "16.1.0" + +permissions: + actions: read + contents: read + +# Every `run:` step gets bash with -e AND pipefail. GitHub's default when no +# shell is named is `bash -e` without pipefail, which would let a failing +# gate script hide behind the `| tee` that records its facts. +defaults: + run: + shell: bash + +jobs: + theatre: + name: SPARK theatre gate (standards) + uses: hyperpolymath/standards/.github/workflows/spark-theatre-gate.yml@95de3dfc3fcf09a1cf3325ab42723e3d81682b45 # standards main 2026-10-14 + permissions: + actions: read + contents: read + with: + paths: ${{ inputs.working_directory }} + enforce_zero_contract: ${{ inputs.enforce_zero_contract }} + + detect: + name: Detect SPARK units + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + permissions: + contents: read + outputs: + spark_units: ${{ steps.facts.outputs.spark_units }} + project: ${{ steps.facts.outputs.project }} + gpr_count: ${{ steps.facts.outputs.gpr_count }} + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: spark-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Facts + id: facts + env: + SPARK_GATE_PHASE: detect + WORKING_DIRECTORY: ${{ inputs.working_directory }} + GPR: ${{ inputs.gpr }} + run: bash .cicd-suite/actions/spark-check/check.sh | tee -a "$GITHUB_OUTPUT" + + prove: + name: GNATprove + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 60 + needs: detect + if: ${{ needs.detect.outputs.spark_units != '0' && needs.detect.outputs.spark_units != '' }} + permissions: + contents: read + env: + GNATPROVE_VERSION: ${{ inputs.gnatprove_version }} + GNATPROVE_PREFIX: ${{ github.workspace }}/.gnatprove-prefix + steps: + - name: Check out the calling repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Resolve the cicd-suite commit this caller pins + id: suite + env: + SUITE_WORKFLOW: spark-gate.yml + # Inside a reusable workflow the `github` context is the CALLER's, so + # GITHUB_WORKFLOW_REF names the caller's workflow file — which is in + # the tree just checked out and holds the very `uses:` line GitHub + # resolved to reach this file. That SHA pins the gate scripts: one + # pin, held by the caller, selects both the workflow and its scripts. + # (`github.job_workflow_sha` is an OIDC claim, not a context property, + # and reading the token would need id-token: write from every caller.) + run: | + set -euo pipefail + path="${GITHUB_WORKFLOW_REF#"$GITHUB_REPOSITORY"/}"; path="${path%@*}" + [ -f "$path" ] || { echo "::error::caller workflow '$path' is not in the checkout, so the gate scripts cannot be pinned. NO CHECK WAS PERFORMED."; exit 2; } + shas="$(grep -oE "uses:[[:space:]]*hyperpolymath/cicd-suite/\.github/workflows/${SUITE_WORKFLOW}@[0-9a-f]{40}" "$path" | sed 's/.*@//' | sort -u || true)" + n="$(printf '%s' "$shas" | grep -c . || true)" + if [ "$n" -ne 1 ]; then + echo "::error::$path pins hyperpolymath/cicd-suite/.github/workflows/${SUITE_WORKFLOW} at $n distinct full SHAs; exactly one is required (a branch or tag ref does not count). NO CHECK WAS PERFORMED." + exit 2 + fi + echo "sha=$shas" >> "$GITHUB_OUTPUT" + echo "cicd-suite pinned at $shas by $path" + - name: Check out cicd-suite at that commit + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ steps.suite.outputs.sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse gate scripts from an unverified cicd-suite commit + env: + EXPECTED: ${{ steps.suite.outputs.sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Set up Alire with GNAT ${{ inputs.gnat_version }} and gprbuild + uses: alire-project/setup-alire@fc4c8ce471aa30b3af0d39ce15add1ee9eaf28f2 # v6.0.0 + with: + toolchain: gnat_native=${{ inputs.gnat_version }} gprbuild + - name: Cache the GNATprove ${{ inputs.gnatprove_version }} install + id: cache + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: ${{ env.GNATPROVE_PREFIX }} + key: gnatprove-${{ inputs.gnatprove_version }}-${{ runner.os }}-${{ runner.arch }} + - name: Install GNATprove ${{ inputs.gnatprove_version }} (alr install) + if: ${{ steps.cache.outputs.cache-hit != 'true' }} + run: | + set -euo pipefail + alr -n install "gnatprove=${GNATPROVE_VERSION}" --prefix "$GNATPROVE_PREFIX" + - name: gnatprove is on PATH + run: | + set -euo pipefail + echo "$GNATPROVE_PREFIX/bin" >> "$GITHUB_PATH" + export PATH="$GNATPROVE_PREFIX/bin:$PATH" + gnatprove --version + - name: Planted controls, then the project + env: + SPARK_GATE_PHASE: prove + WORKING_DIRECTORY: ${{ inputs.working_directory }} + GPR: ${{ inputs.gpr }} + LEVEL: ${{ inputs.level }} + TIMEOUT: ${{ inputs.timeout }} + EXTRA_ARGS: ${{ inputs.extra_args }} + run: bash .cicd-suite/actions/spark-check/check.sh + + verdict: + name: SPARK verdict + runs-on: ${{ inputs.runs-on }} + timeout-minutes: 5 + needs: [theatre, detect, prove] + if: ${{ always() }} + permissions: + contents: read + env: + UNITS: ${{ needs.detect.outputs.spark_units }} + R_THEATRE: ${{ needs.theatre.result }} + R_DETECT: ${{ needs.detect.result }} + R_PROVE: ${{ needs.prove.result }} + steps: + - name: Adjudicate + run: | + set -euo pipefail + fail=0 + [ "$R_THEATRE" = success ] || { echo "::error::theatre: $R_THEATRE"; fail=1; } + [ "$R_DETECT" = success ] || { echo "::error::detect: $R_DETECT"; fail=1; } + case "$R_PROVE" in + success) echo " ok prove ($UNITS SPARK unit(s))" ;; + failure|cancelled) echo "::error::prove: $R_PROVE"; fail=1 ;; + skipped) + if [ "${UNITS:-0}" != 0 ] && [ -n "${UNITS:-}" ]; then + echo "::error::prove was SKIPPED although $UNITS SPARK unit(s) exist — VOID, not green."; fail=1 + else + echo "::notice::No SPARK_Mode-On unit in this tree: nothing was proved. This verdict is silent, not green-as-assurance." + fi ;; + *) echo "::error::prove: unknown result '$R_PROVE'"; fail=1 ;; + esac + [ "$fail" -eq 0 ] || { echo "::error::SPARK verdict: RED."; exit 1; } + echo "SPARK verdict: GREEN." diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index 6305a32..89c8798 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -14,12 +14,39 @@ templates/estate-audit-caller.yml the ten-line caller each repository holds templates/track-estate-audit.yml weekly bot: moves the caller's pin to HEAD scripts/deonboard-estate-audit.sh removes the caller from a repo's actions.lock rollout_estate.sh installs the three above in every estate clone +actions/rust-ci-check/ the strict Rust gate (resolve.sh, check.sh, test.sh) +actions/creusot-check/ Creusot: detect · theatre · prove (planted controls) +actions/spark-check/ SPARK: detect · GNATprove (planted controls) +actions/kanren-check/ miniKanren: detect · run · purity +.github/workflows/rust-ci.yml reusable; jobs run the scripts above +.github/workflows/creusot-gate.yml reusable +.github/workflows/spark-gate.yml reusable; theatre half is standards' gate, nested +.github/workflows/kanren-gate.yml reusable +.github/workflows/language-gates-self-test.yml each gate's test.sh, every PR +templates/*-caller.yml the thin callers for the four gates +scripts/verify-suite-checkout.sh proves the self-checkout is the caller's pin +scripts/deonboard-workflow.sh general form of deonboard-estate-audit.sh +rollout_language_gates.sh installs the callers by what a tree contains .... Consumers call the reusable workflow at a full SHA. They do not copy its steps. A copy froze at whatever commit its lock held, so fixes made here never arrived. The caller is one line to move, and the track bot moves it. +== Two ways a reusable reaches its scripts + +The estate audit pins each composite as `+uses: hyperpolymath/cicd-suite/actions/x@+`, +which is why `+tests/lock-transitive-closure.sh+` insists the pinned commit +serves the current `+actions/+` tree — a cure landed here was inert downstream +until a repin commit followed. The language gates avoid the second pin: every +job reads the SHA the caller pins the reusable at back out of the caller's own +workflow file, checks this repository out at that SHA and runs the scripts from +that checkout after +`+scripts/verify-suite-checkout.sh+` has proved it IS that commit. One pin, +held by the caller, selects both the workflow and its scripts. An empty or +wrong SHA is exit 2 — no check was performed — because a silent fall-through +to the default branch would be the `+@main+` hazard by another route. + == Why composite, and why bash A composite action needs no packaging, no container pull and no marketplace diff --git a/README.adoc b/README.adoc index a132235..19ee76a 100644 --- a/README.adoc +++ b/README.adoc @@ -53,6 +53,11 @@ missing Keybase link would be worse than not checking. 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. @@ -182,6 +187,104 @@ because `+GITHUB_TOKEN+` may not write under `+.github/workflows/+`. `+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. + +[cols="1,2,2",options="header"] +|=== +|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/.yml+` with `+__CICD_SUITE_SHA__+` replaced; +`+scripts/deonboard-workflow.sh +` 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. + === Licence Code MPL-2.0, prose CC-BY-SA-4.0. See link:LICENSE[`+LICENSE+`]. diff --git a/actions/creusot-check/action.yml b/actions/creusot-check/action.yml new file mode 100644 index 0000000..f61023a --- /dev/null +++ b/actions/creusot-check/action.yml @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: MPL-2.0 +name: 'Creusot Gate' +description: >- + Rust deductive-verification gate (Creusot). detect: facts; theatre: a + "verified with Creusot" claim must be backed by contracts (T1 hard fail), + a hollow dependency is named (T2); prove: planted controls, then + `cargo creusot prove` in every crate carrying obligations. The reusable + workflow .github/workflows/creusot-gate.yml installs Creusot (pinned) and + runs all three. +inputs: + phase: + description: 'detect | theatre | prove' + required: true + working_directory: + description: 'Tree root to scan' + required: false + default: '.' + enforce_hollow: + description: 'Escalate T2 (dependency without contracts) to a failure' + required: false + default: 'false' + prove_args: + description: 'Args appended to cargo creusot prove' + required: false + default: '' +runs: + using: 'composite' + steps: + - name: Run Creusot gate phase + shell: bash + env: + CREUSOT_GATE_PHASE: ${{ inputs.phase }} + WORKING_DIRECTORY: ${{ inputs.working_directory }} + ENFORCE_HOLLOW: ${{ inputs.enforce_hollow }} + PROVE_ARGS: ${{ inputs.prove_args }} + run: bash "$GITHUB_ACTION_PATH/check.sh" diff --git a/actions/creusot-check/check.sh b/actions/creusot-check/check.sh new file mode 100755 index 0000000..dec206e --- /dev/null +++ b/actions/creusot-check/check.sh @@ -0,0 +1,246 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check.sh — the Creusot gate for Rust, parallel to the SPARK gate for Ada. +# +# Creusot (https://github.com/creusot-rs/creusot) is a deductive verifier for +# Rust: a crate depends on `creusot-std` (named `creusot-contracts` before +# v0.9.0), annotates functions with `#[requires(..)]` / `#[ensures(..)]`, and +# `cargo creusot prove` discharges the obligations through Why3 and SMT +# solvers. "Verified with Creusot" is therefore a claim with an oracle, and +# this gate makes the claim and the oracle agree. Three phases: +# +# CREUSOT_GATE_PHASE=detect +# Prints `key=value` facts: obligations (true when any crate carries a +# Creusot dependency or contract attribute), claims (true when prose or a +# source header asserts Creusot verification), crates (the manifest +# directories carrying obligations, newline-separated in a file), +# creusot_version (from the dependency spec, else ""). +# +# CREUSOT_GATE_PHASE=theatre (the anti-theatre tier, mirrors +# standards' SPARK Theatre Gate T1/T2) +# T1 a claim with no obligations behind it: hard failure, always. +# T2 a Creusot dependency with ZERO contract attributes anywhere: a +# hollow dependency proves nothing. Warning by default; a hard +# failure when ENFORCE_HOLLOW=true. +# T3 every `#[trusted]` is printed. `trusted` is an axiom the prover +# takes on faith; the gate never fails on it, but it never lets one +# pass unlisted either (the residue list of the proof). +# +# CREUSOT_GATE_PHASE=prove +# Requires `cargo creusot` on PATH (the workflow installs it, pinned). +# FIRST proves a planted known-failing contract and REQUIRES a non-zero +# exit; then a planted known-good one and requires zero. A prover that +# cannot say no is not a prover, and the verdict over the caller's +# crate would be VOID — so the gate refuses (exit 2) rather than report +# green. Only then does it run `cargo creusot prove` in every crate +# directory that carries obligations, failing on any non-zero exit. +# +# Exit codes: 0 silent, 1 defect found, 2 NO CHECK WAS PERFORMED (tool +# missing, planted control misbehaved, unreadable tree). 2 is never a pass. +# +# Env: WORKING_DIRECTORY (default "."), ENFORCE_HOLLOW (default false), +# PROVE_ARGS (appended to `cargo creusot prove`), CREUSOT_FACTS (path +# the detect phase writes its crate list to; default $RUNNER_TEMP or +# /tmp). +set -uo pipefail + +phase="${CREUSOT_GATE_PHASE:?CREUSOT_GATE_PHASE is required: detect|theatre|prove}" +dir="${WORKING_DIRECTORY:-.}" +enforce_hollow="${ENFORCE_HOLLOW:-false}" +prove_args="${PROVE_ARGS:-}" +facts_dir="${CREUSOT_FACTS:-${RUNNER_TEMP:-/tmp}/creusot-facts}" +mkdir -p "$facts_dir" + +cd "$dir" || { echo "::error::creusot-check[$phase]: cannot enter $dir — NO CHECK WAS PERFORMED." >&2; exit 2; } + +# Tracked files only: an untracked checkout of this suite (.cicd-suite/) or a +# target/ tree must never count as the caller's sources. +list_files() { # + if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + git ls-files -z | tr '\0' '\n' | grep -E "$1" || true + else + find . -type f -not -path '*/.git/*' -not -path '*/target/*' -not -path '*/.cicd-suite/*' \ + | sed 's#^\./##' | grep -E "$1" || true + fi +} + +# ---------------------------------------------------------------- facts ---- +manifests="$(list_files '(^|/)Cargo\.toml$')" +obligation_manifests="" +creusot_version="" +while IFS= read -r m; do + [ -n "$m" ] || continue + # A dependency line for the proof library, under any dependency table. + if grep -qE '^[[:space:]]*(creusot-std|creusot-contracts)[[:space:]]*=' "$m" \ + || grep -qE '^[[:space:]]*\[(workspace\.)?dependencies\.(creusot-std|creusot-contracts)\]' "$m"; then + obligation_manifests="${obligation_manifests}${m}"$'\n' + if [ -z "$creusot_version" ]; then + creusot_version="$(sed -nE 's/^[[:space:]]*(creusot-std|creusot-contracts)[[:space:]]*=[[:space:]]*(\{[^}]*version[[:space:]]*=[[:space:]]*)?"([^"]+)".*$/\3/p' "$m" | head -n 1 || true)" + fi + fi +done <<< "$manifests" + +contract_re='#\[(requires|ensures|invariant|variant|logic|law|open|predicate|terminates|pure|trusted)(\(|\])|proof_assert!|#\[creusot::' +rust_sources="$(list_files '\.rs$')" +contract_files="" +contract_count=0 +trusted_count=0 +if [ -n "$rust_sources" ]; then + contract_files="$(printf '%s\n' "$rust_sources" | xargs -r grep -lE "$contract_re" 2>/dev/null || true)" + contract_count="$({ printf '%s\n' "$rust_sources" | xargs -r grep -cE '#\[(requires|ensures)\(' 2>/dev/null || true; } | awk -F: '{s+=$NF} END {print s+0}')" + trusted_count="$({ printf '%s\n' "$rust_sources" | xargs -r grep -cE '#\[trusted\]' 2>/dev/null || true; } | awk -F: '{s+=$NF} END {print s+0}')" +fi + +obligations=false +if [ -n "$obligation_manifests" ] || [ -n "$contract_files" ]; then obligations=true; fi + +# A claim is a sentence in prose or a source HEADER that asserts the proof +# exists. Scoped to README*/docs/** and to the leading comment block of a +# Rust file, like the SPARK gate's header rule: a design note deep in a body, +# or a proposal that mentions Creusot as a plan, is not a claim about this +# tree. The negative lookbehind words ("planned", "proposal", "would", "not +# yet") are the honest-roadmap vocabulary and are excluded by hand below. +claim_re='(verified (with|by|using) creusot|creusot[- ]verified|proved (with|by|using) creusot|creusot proofs? (pass|discharged)|creusot: (all|every) (goal|obligation)s? (proved|discharged))' +plan_re='(planned|proposal|proposed|roadmap|not yet|would|future|todo|intend)' +claim_sites="" +prose="$(list_files '(^|/)(README[^/]*|[^/]*\.(adoc|md))$' | grep -vE '^(\.cicd-suite|target)/' || true)" +while IFS= read -r f; do + [ -n "$f" ] || continue + while IFS= read -r hit; do + [ -n "$hit" ] || continue + printf '%s' "$hit" | grep -qiE "$plan_re" && continue + claim_sites="${claim_sites}${f}:${hit%%:*}"$'\n' + done < <(grep -niE "$claim_re" "$f" 2>/dev/null || true) +done <<< "$prose" +while IFS= read -r f; do + [ -n "$f" ] || continue + header="$(awk '/^[[:space:]]*(\/\/|\/\*|\*)/ || /^[[:space:]]*$/ { print; next } { exit }' "$f")" + if printf '%s\n' "$header" | grep -qiE "$claim_re" \ + && ! printf '%s\n' "$header" | grep -qiE "$plan_re"; then + claim_sites="${claim_sites}${f}:1"$'\n' + fi +done <<< "$rust_sources" +claims=false +[ -n "$claim_sites" ] && claims=true + +crate_dirs="$(printf '%s' "$obligation_manifests" | sed -E 's#(^|/)Cargo\.toml$##; s#^$#.#' | sort -u)" +printf '%s\n' "$crate_dirs" | sed '/^$/d' > "$facts_dir/crates" +printf '%s' "$claim_sites" > "$facts_dir/claims" + +case "$phase" in + detect) + printf 'obligations=%s\n' "$obligations" + printf 'claims=%s\n' "$claims" + printf 'creusot_version=%s\n' "$creusot_version" + printf 'contract_count=%s\n' "$contract_count" + printf 'trusted_count=%s\n' "$trusted_count" + printf 'crates_file=%s\n' "$facts_dir/crates" + exit 0 + ;; + + theatre) + fail=0 + if [ "$claims" = true ] && [ "$obligations" = false ]; then + while IFS= read -r site; do + [ -n "$site" ] || continue + echo "::error file=${site%%:*},line=${site##*:}::T1 Creusot theatre: this says the code is verified with Creusot, but no crate depends on creusot-std and no #[requires]/#[ensures] exists. Add the contracts and the dependency, or remove the claim (standards#692: Rust + Creusot, without proof theatre)." + done <<< "$claim_sites" + fail=1 + fi + if [ "$obligations" = true ] && [ "$contract_count" -eq 0 ]; then + msg="T2 hollow Creusot dependency: creusot-std/creusot-contracts is a dependency but no #[requires]/#[ensures] appears in any tracked .rs file, so 'cargo creusot prove' would discharge nothing. Write a contract on at least one function, or drop the dependency." + if [ "$enforce_hollow" = true ]; then + echo "::error::$msg"; fail=1 + else + echo "::warning::$msg (escalates to a failure with enforce_hollow: true)" + fi + fi + if [ "$trusted_count" -gt 0 ]; then + echo "::notice::T3 residue: $trusted_count #[trusted] item(s) are taken as axioms by the prover. They are listed below; a proof is only as strong as its trusted set." + printf '%s\n' "$rust_sources" | xargs -r grep -nE '#\[trusted\]' 2>/dev/null | sed 's/^/ trusted: /' || true + fi + if [ "$obligations" = false ] && [ "$claims" = false ]; then + echo "::notice::creusot-check: no Creusot obligations and no verification claims in this tree. Nothing was proved and nothing claims to be — this gate is silent, not green-as-assurance." + fi + [ "$fail" -eq 0 ] || { echo "::error::creusot-check[theatre]: FAILED — see annotations."; exit 1; } + echo "creusot-check[theatre]: no theatre found (obligations=$obligations claims=$claims contracts=$contract_count trusted=$trusted_count)." + exit 0 + ;; + + prove) + if [ "$obligations" = false ]; then + echo "::error::creusot-check[prove]: no Creusot obligations in this tree — NO PROOF WAS PERFORMED. The prove job must only run when detect reported obligations=true." >&2 + exit 2 + fi + command -v cargo >/dev/null 2>&1 && cargo creusot --help >/dev/null 2>&1 || { + echo "::error::creusot-check[prove]: 'cargo creusot' is not available — NO PROOF WAS PERFORMED. The workflow installs Creusot (pinned) before this step." >&2 + exit 2 + } + + # ---- planted controls: the prover must be able to say NO ------------- + ctl="$(mktemp -d)" + plant() { # + mkdir -p "$ctl/$1/src" + cat > "$ctl/$1/Cargo.toml" < "$ctl/$1/src/lib.rs" + } + plant creusot-control-failing 'use creusot_std::prelude::*; +#[ensures(result == 0u32)] +pub fn planted_must_fail() -> u32 { 1 }' + plant creusot-control-passing 'use creusot_std::prelude::*; +#[ensures(result == 2u32)] +pub fn planted_must_pass() -> u32 { 2 }' + echo "::group::planted control: a false postcondition must NOT prove" + # shellcheck disable=SC2086 + if (cd "$ctl/creusot-control-failing" && cargo creusot prove $prove_args); then + echo "::endgroup::" + echo "::error::creusot-check[prove]: the planted FALSE contract was reported proved (exit 0). This prover cannot fail, so any verdict it gives over the caller's crate is VOID. NO PROOF WAS PERFORMED." >&2 + rm -rf "$ctl"; exit 2 + fi + echo "::endgroup::" + echo "planted control: false contract refused — the oracle can say no." + echo "::group::planted control: a true postcondition must prove" + # shellcheck disable=SC2086 + if ! (cd "$ctl/creusot-control-passing" && cargo creusot prove $prove_args); then + echo "::endgroup::" + echo "::error::creusot-check[prove]: the planted TRUE contract did not prove. The toolchain is broken (solver or prelude), so a red on the caller's crate would be misattributed. NO PROOF WAS PERFORMED." >&2 + rm -rf "$ctl"; exit 2 + fi + echo "::endgroup::" + rm -rf "$ctl" + echo "planted control: true contract proved — the oracle can say yes." + + # ---- the caller's crates --------------------------------------------- + fail=0 + while IFS= read -r crate; do + [ -n "$crate" ] || continue + echo "::group::cargo creusot prove — $crate" + # shellcheck disable=SC2086 + if (cd "$crate" && cargo creusot prove $prove_args); then + echo "::endgroup::" + echo "ok: $crate — every obligation discharged" + else + rc=$? + echo "::endgroup::" + echo "::error file=$crate/Cargo.toml::creusot-check[prove]: 'cargo creusot prove' exited $rc in $crate — at least one obligation is unproved. Fix the contract or the code; never mark it #[trusted] to get green." + fail=1 + fi + done < "$facts_dir/crates" + [ "$fail" -eq 0 ] || exit 1 + echo "creusot-check[prove]: all Creusot obligations discharged (trusted axioms: $trusted_count)." + exit 0 + ;; + *) + echo "::error::creusot-check: unknown phase '$phase' (detect|theatre|prove)" >&2 + exit 2 + ;; +esac diff --git a/actions/creusot-check/test.sh b/actions/creusot-check/test.sh new file mode 100755 index 0000000..9f87bfa --- /dev/null +++ b/actions/creusot-check/test.sh @@ -0,0 +1,134 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# test.sh — the Creusot gate must fail for each thing it claims to check, +# under the exact composite shell (bash --noprofile --norc -e -o pipefail). +# +# The prove phase is exercised against a stand-in `cargo-creusot` on PATH. The +# stub says "unproved" for any crate whose lib.rs contains the planted +# failing marker or a `// UNPROVED` line, and "proved" otherwise — which is +# exactly the contract the real tool must honour (exit code is the oracle). +# A second stub that can only say yes must make the gate refuse (exit 2). +# This does NOT prove Why3/SMT integration; the planted controls in check.sh +# do that at runtime, against the real tool, on every run. +set -uo pipefail + +here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +checker="$here/check.sh" +PASS=0; FAIL=0 +ok() { printf ' ok %s\n' "$1"; PASS=$((PASS+1)); } +bad() { printf ' FAIL %s\n' "$1"; FAIL=$((FAIL+1)); } +command -v cargo >/dev/null || { echo "cargo is required (it dispatches 'cargo creusot' to cargo-creusot on PATH)"; exit 2; } + +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT +OUT="$WORK/out" +FIX="$WORK/fixture" + +fresh_fixture() { + rm -rf "$FIX"; mkdir -p "$FIX/src" "$FIX/docs" + git -C "$FIX" init -q + git -C "$FIX" config user.email t@example.invalid + git -C "$FIX" config user.name t + printf '[package]\nname = "fx"\nversion = "0.1.0"\nedition = "2021"\n\n[dependencies]\n' > "$FIX/Cargo.toml" + printf '//! fixture\npub fn id(x: u32) -> u32 { x }\n' > "$FIX/src/lib.rs" + printf '= fx\n\nA small crate.\n' > "$FIX/README.adoc" + git -C "$FIX" add -A && git -C "$FIX" commit -qm fixture +} +commit() { git -C "$FIX" add -A && git -C "$FIX" commit -qm change >/dev/null; } +run_phase() { # [env...] + ( cd "$FIX" && env CREUSOT_GATE_PHASE="$1" CREUSOT_FACTS="$WORK/facts" "${@:2}" \ + bash --noprofile --norc -e -o pipefail "$checker" ) > "$OUT" 2>&1 + RC=$? +} + +echo "== a plain crate: no obligations, no claims, silent ==" +fresh_fixture +run_phase detect +[ "$RC" -eq 0 ] && ok "detect exits 0" || { bad "detect exits $RC"; cat "$OUT"; } +grep -qx 'obligations=false' "$OUT" && ok "obligations=false" || bad "obligations misreported: $(cat "$OUT")" +grep -qx 'claims=false' "$OUT" && ok "claims=false" || bad "claims misreported" +run_phase theatre +[ "$RC" -eq 0 ] && ok "theatre exits 0" || bad "theatre exits $RC" +grep -q 'nothing claims to be' "$OUT" && ok "says it is silent, not green-as-assurance" || bad "no silence notice" +run_phase prove +[ "$RC" -eq 2 ] && ok "prove on a crate without obligations is exit 2 (no proof performed)" || bad "prove exits $RC, expected 2" + +echo "== T1: a README claim with nothing behind it is a hard failure ==" +printf '= fx\n\nThis crate is verified with Creusot.\n' > "$FIX/README.adoc"; commit +run_phase detect +grep -qx 'claims=true' "$OUT" && ok "detect sees the claim" || bad "claim not seen: $(cat "$OUT")" +run_phase theatre +[ "$RC" -eq 1 ] && ok "theatre exits 1" || bad "theatre exits $RC, expected 1" +grep -q '::error file=README.adoc,line=3::T1 Creusot theatre' "$OUT" && ok "annotates the claim at its line" || bad "T1 annotation missing: $(cat "$OUT")" + +echo "== a roadmap sentence is not a claim ==" +printf '= fx\n\nIt is planned to have this crate verified with Creusot.\n' > "$FIX/README.adoc"; commit +run_phase theatre +[ "$RC" -eq 0 ] && ok "planned work does not fire T1" || bad "a plan fired T1 (exit $RC)" + +echo "== T2: a Creusot dependency with no contracts is hollow ==" +printf '= fx\n\nA small crate.\n' > "$FIX/README.adoc" +printf '[package]\nname = "fx"\nversion = "0.1.0"\nedition = "2021"\n\n[dependencies]\ncreusot-std = "0.14"\n' > "$FIX/Cargo.toml"; commit +run_phase detect +grep -qx 'obligations=true' "$OUT" && ok "the dependency counts as an obligation" || bad "dependency not seen" +grep -qx 'creusot_version=0.14' "$OUT" && ok "reads the creusot-std version" || bad "version not read: $(cat "$OUT")" +run_phase theatre +[ "$RC" -eq 0 ] && ok "hollow is a warning by default" || bad "hollow failed by default (exit $RC)" +grep -q '::warning::T2 hollow' "$OUT" && ok "and is named" || bad "T2 warning missing" +run_phase theatre ENFORCE_HOLLOW=true +[ "$RC" -eq 1 ] && ok "hollow is a failure with ENFORCE_HOLLOW=true" || bad "ENFORCE_HOLLOW did not fail (exit $RC)" + +echo "== contracts present: T2 silent, T3 lists trusted ==" +cat > "$FIX/src/lib.rs" <<'RS' +//! fixture +use creusot_std::prelude::*; +#[ensures(result == x)] +pub fn id(x: u32) -> u32 { x } +#[trusted] +pub fn oracle() -> u32 { 7 } +RS +commit +run_phase detect +grep -qx 'contract_count=1' "$OUT" && ok "counts one contract" || bad "contract count wrong: $(cat "$OUT")" +grep -qx 'trusted_count=1' "$OUT" && ok "counts one trusted" || bad "trusted count wrong" +run_phase theatre ENFORCE_HOLLOW=true +[ "$RC" -eq 0 ] && ok "theatre exits 0 with a real contract" || bad "theatre exits $RC" +grep -q 'T3 residue: 1 #\[trusted\]' "$OUT" && ok "the trusted residue is listed" || bad "residue not listed" + +echo "== prove: stub oracle that CAN say no ==" +STAND_IN="$WORK/bin"; mkdir -p "$STAND_IN" +cat > "$STAND_IN/cargo-creusot" <<'SH' +#!/usr/bin/env bash +# stub: 'cargo creusot prove' → exit 1 when the crate is marked unproved +[ "${2:-}" = "prove" ] || exit 0 # cargo passes the subcommand name as $1 +if grep -qE 'planted_must_fail|// UNPROVED' src/lib.rs 2>/dev/null; then + echo "stub: 1 goal unproved"; exit 1 +fi +echo "stub: all goals proved"; exit 0 +SH +chmod +x "$STAND_IN/cargo-creusot" +run_phase prove PATH="$STAND_IN:$PATH" +[ "$RC" -eq 0 ] && ok "prove exits 0 when every crate proves" || { bad "prove exits $RC"; cat "$OUT"; } +grep -q 'false contract refused' "$OUT" && ok "planted failing control was exercised" || bad "failing control not run" +grep -q 'true contract proved' "$OUT" && ok "planted passing control was exercised" || bad "passing control not run" +printf '// UNPROVED\n' >> "$FIX/src/lib.rs"; commit +run_phase prove PATH="$STAND_IN:$PATH" +[ "$RC" -eq 1 ] && ok "an unproved crate fails the gate" || bad "unproved crate exits $RC, expected 1" +grep -q "::error file=./Cargo.toml::creusot-check\[prove\]" "$OUT" && ok "the failing crate is annotated" || bad "crate not annotated: $(cat "$OUT")" + +echo "== prove: an oracle that can only say yes makes the verdict VOID ==" +printf '#!/usr/bin/env bash\necho yes; exit 0\n' > "$STAND_IN/cargo-creusot" +run_phase prove PATH="$STAND_IN:$PATH" +[ "$RC" -eq 2 ] && ok "exits 2 (NO PROOF WAS PERFORMED)" || bad "exits $RC, expected 2" +grep -q 'cannot fail' "$OUT" && ok "says the prover cannot fail" || bad "no explanation" + +echo "== prove: no cargo creusot at all is exit 2 ==" +rm -f "$STAND_IN/cargo-creusot" +run_phase prove PATH="$STAND_IN:/usr/bin:/bin" +[ "$RC" -eq 2 ] && ok "exits 2 without the tool" || bad "exits $RC without the tool, expected 2" + +echo +echo "PASS=$PASS FAIL=$FAIL" +[ "$FAIL" -eq 0 ] diff --git a/actions/kanren-check/action.yml b/actions/kanren-check/action.yml new file mode 100644 index 0000000..ac35153 --- /dev/null +++ b/actions/kanren-check/action.yml @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: MPL-2.0 +name: 'miniKanren Gate' +description: >- + Relational-code gate: finds miniKanren sources (Scheme family, Rust kanren + crates), fails on a claim with no relations (optional), on relations with + no goal-level test, and on a failing relational test run; lists impure + operators (conda/condu/project/…) and can fail on them. Needs the + interpreter the sources name (guile, Chez scheme, racket) on PATH. +inputs: + working_directory: + description: 'Tree root' + required: false + default: '.' + require_tests: + description: 'Fail when relational sources have no relational test (true|false)' + required: false + default: 'true' + enforce_purity: + description: 'Fail on conda/condu/project/onceo/ifa/ifu/copy-term' + required: false + default: 'false' + enforce_claims: + description: 'Fail on a miniKanren claim with no relational sources' + required: false + default: 'false' +runs: + using: 'composite' + steps: + - name: Run miniKanren gate + shell: bash + env: + WORKING_DIRECTORY: ${{ inputs.working_directory }} + REQUIRE_TESTS: ${{ inputs.require_tests }} + ENFORCE_PURITY: ${{ inputs.enforce_purity }} + ENFORCE_CLAIMS: ${{ inputs.enforce_claims }} + run: bash "$GITHUB_ACTION_PATH/check.sh" diff --git a/actions/kanren-check/check.sh b/actions/kanren-check/check.sh new file mode 100755 index 0000000..87c731c --- /dev/null +++ b/actions/kanren-check/check.sh @@ -0,0 +1,199 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check.sh — the miniKanren gate: relational code is RUN, not admired. +# +# A relation that is never executed is a claim, not a check, and a +# relational program that reaches for committed choice (conda/condu), +# projection or copy-term has quietly stopped being relational — it no +# longer runs backwards, which is the property the estate wants from +# miniKanren (cicd-squabbler's Reasoner design; the archived +# state-kanren.scm). Four tiers, one invocation: +# +# DETECT tracked relational sources: Scheme-family files (.scm .ss .sls +# .sld .rkt) that both build goals (run/run*/fresh/conde/==) and +# load or define a miniKanren; Rust crates depending on a kanren +# crate (canrun, ukanren, kanren, mukanren, minikanren). +# T1 claim a README/docs sentence saying this tree USES miniKanren or a +# relational reasoner, with zero relational sources behind it. +# Warning by default (proposals and roadmaps mention it +# legitimately — the plan vocabulary is excluded); a failure +# with ENFORCE_CLAIMS=true. +# T2 tests every relational source set must have at least one relational +# test file (under test/ tests/ spec/, named *-test.* / *.test.* +# / *_test.*, or containing assert/test-* forms). Failure by +# default (REQUIRE_TESTS=true); a warning when false. +# RUN every relational test file is executed with the interpreter its +# dialect names: .rkt → racket; (use-modules …) → guile; +# (import (…))/(library …) → Chez `scheme --script`; otherwise +# guile. A missing interpreter is exit 2 — NO CHECK WAS +# PERFORMED — never a pass. Rust kanren crates run +# `cargo test --locked -p `. +# T3 purity occurrences of conda, condu, project, onceo, ifa, ifu, +# copy-term in relational sources are listed as warnings; failures +# with ENFORCE_PURITY=true. +# +# Exit codes: 0 silent, 1 defect, 2 NO CHECK WAS PERFORMED. +# +# Env: WORKING_DIRECTORY (default "."), REQUIRE_TESTS (default true), +# ENFORCE_PURITY (default false), ENFORCE_CLAIMS (default false). +set -uo pipefail + +dir="${WORKING_DIRECTORY:-.}" +require_tests="${REQUIRE_TESTS:-true}" +enforce_purity="${ENFORCE_PURITY:-false}" +enforce_claims="${ENFORCE_CLAIMS:-false}" + +cd "$dir" || { echo "::error::kanren-check: cannot enter $dir — NO CHECK WAS PERFORMED." >&2; exit 2; } + +list_files() { # + if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + git ls-files -z | tr '\0' '\n' | grep -E "$1" || true + else + find . -type f -not -path '*/.git/*' -not -path '*/target/*' -not -path '*/.cicd-suite/*' \ + | sed 's#^\./##' | grep -E "$1" || true + fi +} + +goal_re='\((run\*?[[:space:]]|run[[:space:]]+[0-9]|fresh[[:space:]]*\(|conde[[:space:]]|==[[:space:]])' +mk_re='(minikanren|mini-kanren|microkanren|mk\.scm|\(define-syntax[[:space:]]+(run\*?|fresh|conde)|\(define[[:space:]]+\(==[[:space:]])' +test_path_re='(^|/)(test|tests|spec)/|[-_.](test|tests|spec)\.(scm|ss|sls|sld|rkt)$' +test_form_re='\((assert|test-assert|test-equal|test-eq|test-begin|check-equal\?|check-expect|check-true|rackunit|srfi[[:space:]]+64)' +impure_re='\((conda|condu|project|onceo|ifa|ifu|copy-term)[[:space:]]' +claim_re='(uses? (a )?(minikanren|mini-kanren)|relational (reasoner|rule base|rules engine|programming)|minikanren(-| )based|implemented (in|with) minikanren)' +plan_re='(planned|proposal|proposed|roadmap|not yet|would|future|todo|intend|optional|adopt|whether)' +kanren_crates='(canrun|ukanren|kanren|mukanren|minikanren)' + +# ------------------------------------------------------------- DETECT ------ +scheme_files="$(list_files '\.(scm|ss|sls|sld|rkt)$')" +engine_re='\(define-syntax[[:space:]]+(run\*?|fresh|conde)[[:space:]]' +rel_files="" +engine_files="" +while IFS= read -r f; do + [ -n "$f" ] || continue + # The file that DEFINES run/fresh/conde is the engine, not a relation over it. + if grep -qE "$engine_re" "$f"; then + engine_files="${engine_files}${f}"$'\n' + elif grep -qE "$goal_re" "$f" && grep -qiE "$mk_re" "$f"; then + rel_files="${rel_files}${f}"$'\n' + fi +done <<< "$scheme_files" + +rel_tests="" +while IFS= read -r f; do + [ -n "$f" ] || continue + if printf '%s' "$f" | grep -qE "$test_path_re" || grep -qE "$test_form_re" "$f"; then + rel_tests="${rel_tests}${f}"$'\n' + fi +done <<< "$rel_files" + +rust_crates="" +while IFS= read -r m; do + [ -n "$m" ] || continue + if grep -qE "^[[:space:]]*${kanren_crates}[[:space:]]*=" "$m" \ + || grep -qE "^[[:space:]]*\[(workspace\.)?dependencies\.${kanren_crates}\]" "$m"; then + name="$(sed -nE 's/^[[:space:]]*name[[:space:]]*=[[:space:]]*"([^"]+)".*$/\1/p' "$m" | head -n 1 || true)" + [ -n "$name" ] && rust_crates="${rust_crates}${name}"$'\n' + fi +done <<< "$(list_files '(^|/)Cargo\.toml$')" + +n_rel="$(printf '%s' "$rel_files" | grep -c . || true)" +n_tests="$(printf '%s' "$rel_tests" | grep -c . || true)" +n_rust="$(printf '%s' "$rust_crates" | grep -c . || true)" +echo "kanren-check: relational Scheme files=$n_rel (tests=$n_tests), Rust kanren crates=$n_rust" +printf '%s' "$rel_files" | sed '/^$/d; s/^/ relational: /' +printf '%s' "$engine_files" | sed '/^$/d; s/^/ engine: /' +printf '%s' "$rust_crates" | sed '/^$/d; s/^/ rust crate: /' + +fail=0 +warn() { echo "::warning::kanren-check: $*"; } +err() { echo "::error::kanren-check: $*"; fail=1; } + +# ------------------------------------------------------------- T1 claim ---- +if [ "$n_rel" -eq 0 ] && [ "$n_rust" -eq 0 ]; then + while IFS= read -r f; do + [ -n "$f" ] || continue + while IFS= read -r hit; do + [ -n "$hit" ] || continue + printf '%s' "$hit" | grep -qiE "$plan_re" && continue + msg="T1 claim without relations: $f:${hit%%:*} says this tree uses miniKanren / a relational reasoner, but no relational source exists. Write the relations (and their tests), or word it as a plan." + if [ "$enforce_claims" = true ]; then err "$msg"; else warn "$msg"; fi + done < <(grep -niE "$claim_re" "$f" 2>/dev/null || true) + done <<< "$(list_files '(^|/)(README[^/]*|[^/]*\.(adoc|md))$' | grep -vE '^(\.cicd-suite|target)/' || true)" + if [ "$fail" -eq 0 ]; then + echo "::notice::kanren-check: no relational sources in this tree. Nothing was run — this gate is silent, not green-as-assurance." + exit 0 + fi + exit 1 +fi + +# ------------------------------------------------------------- T2 tests ---- +if [ "$n_rel" -gt 0 ] && [ "$n_tests" -eq 0 ]; then + msg="T2 relations without a goal-level test: $n_rel relational file(s) and no relational test file (tests/ or *-test.scm, or a file with assert/test-* forms). A relation never run is a claim, not a check." + if [ "$require_tests" = true ]; then err "$msg"; else warn "$msg (REQUIRE_TESTS=false)"; fi +fi + +# ------------------------------------------------------------- RUN --------- +interpreter_for() { # → prints command words or nothing + case "$1" in + *.rkt) command -v racket >/dev/null 2>&1 && echo "racket" ;; + *) + if grep -qE '\(use-modules' "$1"; then + command -v guile >/dev/null 2>&1 && echo "guile --no-auto-compile -s" + elif grep -qE '\((import|library)[[:space:]]*\(' "$1"; then + command -v scheme >/dev/null 2>&1 && echo "scheme --script" + else + command -v guile >/dev/null 2>&1 && echo "guile --no-auto-compile -s" + fi + ;; + esac +} +ran=0 +while IFS= read -r t; do + [ -n "$t" ] || continue + cmd="$(interpreter_for "$t" || true)" # a missing interpreter is a RESULT, not a -e kill + if [ -z "$cmd" ]; then + echo "::error file=$t::kanren-check: no interpreter on PATH for $t (racket for .rkt; guile for (use-modules …); Chez 'scheme' for R6RS) — NO CHECK WAS PERFORMED." >&2 + exit 2 + fi + echo "::group::$cmd $t" + # Run from the file's directory so relative (load "../mk.scm") resolves. + # shellcheck disable=SC2086 # cmd is deliberately word-split + if (cd "$(dirname "$t")" && $cmd "$(basename "$t")"); then + echo "::endgroup::"; echo "ok: $t"; ran=$((ran+1)) + else + rc=$? + echo "::endgroup::" + err "relational test $t failed (exit $rc). The relation does not hold — fix the relation or the expectation; never delete the test." + fi +done <<< "$rel_tests" + +if [ "$n_rust" -gt 0 ]; then + command -v cargo >/dev/null 2>&1 || { echo "::error::kanren-check: Rust kanren crate(s) present but cargo is not on PATH — NO CHECK WAS PERFORMED." >&2; exit 2; } + while IFS= read -r c; do + [ -n "$c" ] || continue + echo "::group::cargo test --locked -p $c" + if cargo test --locked -p "$c"; then + echo "::endgroup::"; echo "ok: crate $c"; ran=$((ran+1)) + else + rc=$?; echo "::endgroup::" + err "cargo test --locked -p $c failed (exit $rc)." + fi + done <<< "$rust_crates" +fi + +# ------------------------------------------------------------- T3 purity --- +while IFS= read -r f; do + [ -n "$f" ] || continue + while IFS= read -r hit; do + [ -n "$hit" ] || continue + op="$(printf '%s' "$hit" | grep -oE "$impure_re" | head -n 1 | tr -d '( ' || true)" + msg="T3 impure operator '$op' at $f:${hit%%:*} — committed choice / projection / copy-term breaks the relation's reversibility. Prefer conde, ==, =/= and fresh." + if [ "$enforce_purity" = true ]; then err "$msg"; else warn "$msg (escalates with enforce_purity: true)"; fi + done < <(grep -nE "$impure_re" "$f" 2>/dev/null || true) +done <<< "$rel_files" + +[ "$fail" -eq 0 ] || { echo "::error::kanren-check: FAILED — see annotations."; exit 1; } +echo "kanren-check: $ran relational test run(s) passed over $n_rel relational file(s) and $n_rust Rust crate(s)." +exit 0 diff --git a/actions/kanren-check/test.sh b/actions/kanren-check/test.sh new file mode 100755 index 0000000..c04aecc --- /dev/null +++ b/actions/kanren-check/test.sh @@ -0,0 +1,182 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# test.sh — the miniKanren gate must fail for each thing it claims to check, +# under the exact composite shell, against a REAL relational program: a +# microKanren (Hemann & Friedman 2013) with the usual run/fresh/conde layer, +# executed by Guile. A planted wrong expectation must fail; a planted +# `conda` must be listed; a claim with no relations must be named. +set -uo pipefail + +here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +checker="$here/check.sh" +PASS=0; FAIL=0 +ok() { printf ' ok %s\n' "$1"; PASS=$((PASS+1)); } +bad() { printf ' FAIL %s\n' "$1"; FAIL=$((FAIL+1)); } +command -v guile >/dev/null || { echo "guile is required (apt-get install guile-3.0)"; exit 2; } + +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT +OUT="$WORK/out" +FIX="$WORK/fixture" + +fresh_fixture() { + rm -rf "$FIX"; mkdir -p "$FIX/tests" + git -C "$FIX" init -q + git -C "$FIX" config user.email t@example.invalid + git -C "$FIX" config user.name t + cat > "$FIX/mk.scm" <<'SCM' +;; mk.scm — microKanren (Hemann & Friedman 2013) + the run/fresh/conde layer. +(define (var c) (vector c)) +(define (var? x) (vector? x)) +(define (var=? a b) (= (vector-ref a 0) (vector-ref b 0))) +(define (assp p l) (cond ((null? l) #f) ((p (caar l)) (car l)) (else (assp p (cdr l))))) +(define (walk u s) + (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s)))) + (if pr (walk (cdr pr) s) u))) +(define (ext-s x v s) (cons (cons x v) s)) +(define mzero '()) +(define (unit s/c) (cons s/c mzero)) +(define (unify u v s) + (let ((u (walk u s)) (v (walk v s))) + (cond ((and (var? u) (var? v) (var=? u v)) s) + ((var? u) (ext-s u v s)) + ((var? v) (ext-s v u s)) + ((and (pair? u) (pair? v)) + (let ((s (unify (car u) (car v) s))) (and s (unify (cdr u) (cdr v) s)))) + (else (and (eqv? u v) s))))) +(define (== u v) + (lambda (s/c) (let ((s (unify u v (car s/c)))) (if s (unit (cons s (cdr s/c))) mzero)))) +(define (call/fresh f) + (lambda (s/c) (let ((c (cdr s/c))) ((f (var c)) (cons (car s/c) (+ c 1)))))) +(define (mplus $1 $2) + (cond ((null? $1) $2) + ((procedure? $1) (lambda () (mplus $2 ($1)))) + (else (cons (car $1) (mplus (cdr $1) $2))))) +(define (bind $ g) + (cond ((null? $) mzero) + ((procedure? $) (lambda () (bind ($) g))) + (else (mplus (g (car $)) (bind (cdr $) g))))) +(define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c)))) +(define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2))) +(define-syntax Zzz (syntax-rules () ((_ g) (lambda (s/c) (lambda () (g s/c)))))) +(define-syntax conj+ (syntax-rules () ((_ g) (Zzz g)) ((_ g0 g ...) (conj (Zzz g0) (conj+ g ...))))) +(define-syntax disj+ (syntax-rules () ((_ g) (Zzz g)) ((_ g0 g ...) (disj (Zzz g0) (disj+ g ...))))) +(define-syntax conde (syntax-rules () ((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...)))) +(define-syntax fresh + (syntax-rules () + ((_ () g0 g ...) (conj+ g0 g ...)) + ((_ (x0 x ...) g0 g ...) (call/fresh (lambda (x0) (fresh (x ...) g0 g ...)))))) +(define empty-state (cons '() 0)) +(define (pull $) (if (procedure? $) (pull ($)) $)) +(define (take-all $) (let (($ (pull $))) (if (null? $) '() (cons (car $) (take-all (cdr $)))))) +(define (take n $) + (if (zero? n) '() + (let (($ (pull $))) (if (null? $) '() (cons (car $) (take (- n 1) (cdr $))))))) +(define (walk* v s) + (let ((v (walk v s))) + (cond ((var? v) v) ((pair? v) (cons (walk* (car v) s) (walk* (cdr v) s))) (else v)))) +(define (reify-name n) (string->symbol (string-append "_." (number->string n)))) +(define (reify-s v s) + (let ((v (walk v s))) + (cond ((var? v) (cons (cons v (reify-name (length s))) s)) + ((pair? v) (reify-s (cdr v) (reify-s (car v) s))) + (else s)))) +(define (reify-1st s/c) (let ((v (walk* (var 0) (car s/c)))) (walk* v (reify-s v '())))) +(define (call/empty-state g) (g empty-state)) +(define-syntax run + (syntax-rules () ((_ n (x ...) g0 g ...) (map reify-1st (take n (call/empty-state (fresh (x ...) g0 g ...))))))) +(define-syntax run* + (syntax-rules () ((_ (x ...) g0 g ...) (map reify-1st (take-all (call/empty-state (fresh (x ...) g0 g ...))))))) +SCM + cat > "$FIX/appendo.scm" <<'SCM' +;; appendo.scm — the canonical relation, over mk.scm. +(load "mk.scm") +(define (appendo l s out) + (conde + ((== '() l) (== s out)) + ((fresh (a d res) + (== (cons a d) l) + (== (cons a res) out) + (appendo d s res))))) +SCM + cat > "$FIX/tests/appendo-test.scm" <<'SCM' +;; appendo-test.scm — run the relation forwards and backwards. +(load "../mk.scm") +(load "../appendo.scm") +(define (check name got want) + (unless (equal? got want) + (display name) (display ": expected ") (write want) (display ", got ") (write got) (newline) + (exit 1))) +(check "forwards" (run* (q) (appendo '(1 2) '(3) q)) '((1 2 3))) +(check "backwards" (run 3 (q) (fresh (x y) (appendo x y '(1 2)) (== (cons x y) q))) + '((() 1 2) ((1) 2) ((1 2)))) +(display "appendo: 2 goals hold") (newline) +SCM + printf '= fx\n\nA relational fixture.\n' > "$FIX/README.adoc" + git -C "$FIX" add -A && git -C "$FIX" commit -qm fixture +} +commit() { git -C "$FIX" add -A && git -C "$FIX" commit -qm change >/dev/null; } +run_gate() { ( cd "$FIX" && env "$@" bash --noprofile --norc -e -o pipefail "$checker" ) > "$OUT" 2>&1; RC=$?; } + +echo "== the fixture relation really runs, forwards and backwards ==" +fresh_fixture +run_gate WORKING_DIRECTORY=. +[ "$RC" -eq 0 ] && ok "gate exits 0" || { bad "gate exits $RC"; cat "$OUT"; } +grep -q 'relational Scheme files=2 (tests=1)' "$OUT" && grep -q ' engine: mk.scm' "$OUT" \ + && ok "detects 2 relational files, 1 test, and the engine" || bad "detection wrong: $(head -4 "$OUT")" +grep -q 'appendo: 2 goals hold' "$OUT" && ok "Guile executed the relational test" || bad "test did not run" +grep -q 'ok: tests/appendo-test.scm' "$OUT" && ok "the test is reported ok" || bad "test not reported" + +echo "== a wrong expectation fails the gate (the relation is the oracle) ==" +sed -i "s/'((1 2 3)))/'((1 2 4)))/" "$FIX/tests/appendo-test.scm"; commit +run_gate WORKING_DIRECTORY=. +[ "$RC" -eq 1 ] && ok "exits 1" || bad "exits $RC, expected 1" +grep -q 'forwards: expected ((1 2 4)), got ((1 2 3))' "$OUT" && ok "the failing goal is in the log" || bad "goal not logged" +grep -q '::error::kanren-check: relational test tests/appendo-test.scm failed' "$OUT" && ok "the test file is annotated" || bad "not annotated" +sed -i "s/'((1 2 4)))/'((1 2 3)))/" "$FIX/tests/appendo-test.scm"; commit + +echo "== T2: relations with no test file ==" +git -C "$FIX" rm -q tests/appendo-test.scm; commit +run_gate WORKING_DIRECTORY=. +[ "$RC" -eq 1 ] && ok "exits 1 by default" || bad "exits $RC, expected 1" +grep -q 'T2 relations without a goal-level test' "$OUT" && ok "names T2" || bad "T2 not named" +run_gate WORKING_DIRECTORY=. REQUIRE_TESTS=false +[ "$RC" -eq 0 ] && ok "a warning with REQUIRE_TESTS=false" || bad "exits $RC with REQUIRE_TESTS=false" +git -C "$FIX" checkout -q HEAD~1 -- tests/appendo-test.scm; commit + +echo "== T3: an impure operator is listed, and fails when enforced ==" +printf '\n(define (bad x) (conda ((== x 1)) ((== x 2))))\n' >> "$FIX/appendo.scm"; commit +run_gate WORKING_DIRECTORY=. +[ "$RC" -eq 0 ] && ok "conda is a warning by default" || bad "conda failed by default (exit $RC)" +grep -q "::warning::kanren-check: T3 impure operator 'conda' at appendo.scm:" "$OUT" && ok "conda is named with its location" || bad "conda not named: $(grep T3 "$OUT")" +run_gate WORKING_DIRECTORY=. ENFORCE_PURITY=true +[ "$RC" -eq 1 ] && ok "conda fails with ENFORCE_PURITY=true" || bad "ENFORCE_PURITY did not fail (exit $RC)" +git -C "$FIX" checkout -q HEAD~1 -- appendo.scm; commit + +echo "== no interpreter is exit 2, never a pass ==" +BASH_BIN="$(command -v bash)" +# A PATH with every tool the gate needs EXCEPT an interpreter (/bin is /usr/bin +# on merged-usr systems, so a plain /bin would still find guile). +NOBIN="$WORK/nobin"; mkdir -p "$NOBIN" +for t in git grep sed awk tr dirname basename head wc xargs find sort cat mktemp env; do ln -sf "$(command -v "$t")" "$NOBIN/$t"; done +( cd "$FIX" && env WORKING_DIRECTORY=. PATH="$NOBIN" "$BASH_BIN" --noprofile --norc -e -o pipefail "$checker" ) > "$OUT" 2>&1; RC=$? +[ "$RC" -eq 2 ] && ok "exits 2 without guile" || bad "exits $RC without guile, expected 2 ($(tail -1 "$OUT"))" + +echo "== T1: a claim with no relations ==" +git -C "$FIX" rm -q mk.scm appendo.scm tests/appendo-test.scm; commit +printf '= fx\n\nThe rule base uses miniKanren for all decisions.\n' > "$FIX/README.adoc"; commit +run_gate WORKING_DIRECTORY=. +[ "$RC" -eq 0 ] && ok "a claim is a warning by default" || bad "claim failed by default (exit $RC)" +grep -q 'T1 claim without relations: README.adoc:3' "$OUT" && ok "the claim is located" || bad "claim not located: $(cat "$OUT")" +run_gate WORKING_DIRECTORY=. ENFORCE_CLAIMS=true +[ "$RC" -eq 1 ] && ok "and fails with ENFORCE_CLAIMS=true" || bad "ENFORCE_CLAIMS did not fail (exit $RC)" +printf '= fx\n\nA miniKanren reasoner is proposed as the default; see the roadmap.\n' > "$FIX/README.adoc"; commit +run_gate WORKING_DIRECTORY=. ENFORCE_CLAIMS=true +[ "$RC" -eq 0 ] && ok "a proposal is not a claim" || bad "a proposal fired T1 (exit $RC)" +grep -q 'silent, not green-as-assurance' "$OUT" && ok "says it is silent" || bad "no silence notice" + +echo +echo "PASS=$PASS FAIL=$FAIL" +[ "$FAIL" -eq 0 ] diff --git a/actions/rust-ci-check/action.yml b/actions/rust-ci-check/action.yml new file mode 100644 index 0000000..75addf7 --- /dev/null +++ b/actions/rust-ci-check/action.yml @@ -0,0 +1,55 @@ +# SPDX-License-Identifier: MPL-2.0 +name: 'Rust CI Gate' +description: >- + Strict Rust gate: cargo check/fmt/clippy, tests AND doctests, cargo doc with + warnings denied, and an MSRV build — every call --locked, every compile -D + warnings. One phase per step (RUST_GATE_PHASE). The reusable workflow + .github/workflows/rust-ci.yml is the recommended entry point; this composite + is the same script for callers that want a single job. +inputs: + phase: + description: 'check | test | doc | msrv' + required: true + working_directory: + description: 'Directory containing Cargo.toml' + required: false + default: '.' + check_args: + description: 'Args appended to cargo check' + required: false + default: '--all-targets' + clippy_args: + description: 'Args appended to cargo clippy' + required: false + default: '--all-targets -- -D warnings' + test_args: + description: 'Args appended to cargo test' + required: false + default: '--all-targets' + doctests: + description: 'Run cargo test --doc as well (true|false)' + required: false + default: 'true' + deny_warnings: + description: 'Export RUSTFLAGS/RUSTDOCFLAGS=-D warnings for every compile' + required: false + default: 'true' + msrv: + description: 'Toolchain for the msrv phase (the declared rust-version)' + required: false + default: '' +runs: + using: 'composite' + steps: + - name: Run Rust gate phase + shell: bash + env: + RUST_GATE_PHASE: ${{ inputs.phase }} + WORKING_DIRECTORY: ${{ inputs.working_directory }} + CHECK_ARGS: ${{ inputs.check_args }} + CLIPPY_ARGS: ${{ inputs.clippy_args }} + TEST_ARGS: ${{ inputs.test_args }} + DOCTESTS: ${{ inputs.doctests }} + DENY_WARNINGS: ${{ inputs.deny_warnings }} + MSRV: ${{ inputs.msrv }} + run: bash "$GITHUB_ACTION_PATH/check.sh" diff --git a/actions/rust-ci-check/check.sh b/actions/rust-ci-check/check.sh new file mode 100755 index 0000000..2ff16e2 --- /dev/null +++ b/actions/rust-ci-check/check.sh @@ -0,0 +1,141 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check.sh — the strict Rust gate, one phase per invocation. +# +# RUST_GATE_PHASE=check cargo check --locked, cargo fmt --check, cargo clippy -D warnings +# RUST_GATE_PHASE=test cargo test --locked (all targets) AND cargo test --doc +# RUST_GATE_PHASE=doc cargo doc --no-deps --document-private-items, RUSTDOCFLAGS=-D warnings +# RUST_GATE_PHASE=msrv cargo + check --locked (the declared rust-version must build) +# +# What "strict" means here, and why each rule exists: +# +# * `--locked` on every cargo call. Cargo.lock is a hard constraint: a lock +# that needs updating fails the gate instead of being re-resolved in CI +# (standards#295; the echidna#92 24-hour masked break). +# * A MISSING Cargo.lock fails before cargo runs, with the fix named. Without +# a lock `--locked` cannot hold and every run resolves afresh. +# * `RUSTFLAGS=-D warnings` (and RUSTDOCFLAGS) for every compile, not only +# clippy's: a rustc warning in a test target is a defect the old gate let +# through because only `cargo clippy -- -D warnings` denied anything. +# * Doctests run as their own step. `cargo test --all-targets` does NOT run +# doctests (cargo's documented behaviour), so the previous gate never +# executed a single `///` example. The one tolerated outcome is a +# workspace with no library target at all — cargo reports exactly +# "no library targets found" and nothing else — which is a fact about the +# crate, not a swallowed failure, and is printed as a ::notice. +# * `cargo doc` with warnings denied: a broken intra-doc link is a defect. +# * The MSRV phase builds with the toolchain the manifest PROMISES. A crate +# that says `rust-version = "1.74"` and needs 1.80 lies to every consumer. +# +# No step here may swallow an exit code. If a command cannot run (tool +# missing), that is exit 2 — "no check was performed" — never a pass. +# +# Env: WORKING_DIRECTORY (default "."), CHECK_ARGS, CLIPPY_ARGS, TEST_ARGS, +# DOCTESTS (true|false, default true), DENY_WARNINGS (true|false, +# default true), MSRV (msrv phase only). +set -uo pipefail + +phase="${RUST_GATE_PHASE:?RUST_GATE_PHASE is required: check|test|doc|msrv}" +dir="${WORKING_DIRECTORY:-.}" +check_args="${CHECK_ARGS:---all-targets}" +clippy_args="${CLIPPY_ARGS:---all-targets -- -D warnings}" +test_args="${TEST_ARGS:---all-targets}" +doctests="${DOCTESTS:-true}" +deny_warnings="${DENY_WARNINGS:-true}" + +fail=0 +err() { echo "::error::rust-ci-check[$phase]: $*" >&2; fail=1; } + +command -v cargo >/dev/null 2>&1 || { + echo "::error::rust-ci-check[$phase]: cargo is not on PATH — NO CHECK WAS PERFORMED. The workflow must install a toolchain before this step." >&2 + exit 2 +} +[ -f "$dir/Cargo.toml" ] || { + echo "::error::rust-ci-check[$phase]: $dir/Cargo.toml not found — NO CHECK WAS PERFORMED. Set working_directory to the crate root." >&2 + exit 2 +} +cd "$dir" || { echo "::error::rust-ci-check[$phase]: cannot enter $dir — NO CHECK WAS PERFORMED." >&2; exit 2; } + +if [ ! -f Cargo.lock ]; then + echo "::error file=$dir/Cargo.toml::Cargo.lock is not committed. The gate runs every cargo command with --locked so dependency drift fails the first push it happens; without a lock there is nothing to hold. Run 'cargo generate-lockfile', commit Cargo.lock, and push." >&2 + exit 1 +fi + +if [ "$deny_warnings" = true ]; then + export RUSTFLAGS="${RUSTFLAGS:-} -D warnings" + export RUSTDOCFLAGS="${RUSTDOCFLAGS:-} -D warnings" +fi +export CARGO_TERM_COLOR="${CARGO_TERM_COLOR:-always}" + +run() { #