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 98102d7..be602b5 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. @@ -184,34 +189,103 @@ 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. -If a file carries a manifest extension but is not a manifest, the -`+manifests+` check will fail on it. Panic-attack's suppression registry -at `+audits/assail-classifications.a2ml+` is one such file. Name it in the -caller rather than editing or moving it: +=== Language gates (Rust, Creusot, SPARK, miniKanren) -[source,yaml] ----- -jobs: - estate: - uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@<40-hex sha> # cicd-suite main - with: - manifest-deed-paths-ignore: | - vendor/ - vendored/ - verified-container-spec/ - .audittraining/ - integration/fixtures/ - test/fixtures/ - tests/fixtures/ - audits/assail-classifications.a2ml ----- +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. +|=== -The list goes to the DEED validator as its `+paths-ignore+` and -*replaces* its defaults, so repeat the defaults you still want, as above. -`+manifest-k9-paths-ignore+` does the same for the K9 validator. That -validator has a different default list, which is why the two lists are -separate. Each fragment is matched as a substring of the file's path. -Leave both unset and each validator keeps its own defaults. +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 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() { #