From 56e78668b87528100f4d085238a485abc393163d Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 13:39:33 +0100 Subject: [PATCH] ci(spark): add SPARK Theatre Gate reusable workflow (#135) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Estate anti-theatre lint, sub-issue of the proof-debt epic. Per SPARK_Mode-On Ada unit, with no repo-wide GNATprove evidence: T1 (hard fail): a strong proof assertion ("formally verified", "SPARK Proof Level", "(Gold)", "all preconditions and postconditions are verified", "proving the invariant holds") in the FILE HEADER BANNER. Header-scoped so an incidental phrase in a body comment (e.g. an enum-literal description) does not false-fire — verified against ambientops strategy_matrix.ads:53. T2 (warn; hard fail when enforce_zero_contract: true): SPARK_Mode (On) with zero Pre/Post/Global/Depends/Contract_Cases. Warning by default so the ~13 repos mid Ada/SPARK->Rust/SPARK migration are not broken on rollout; escalates to failure per #135 end-state. Genuine SPARK repos pass: GNATprove evidence (CI ref / build recipe / gnatprove output) suppresses both rules. Verified locally: * standards self-run -> PASS * ambientops post-demotion -> PASS (T2 warn only, no T1) * ambientops w/ pre-demotion safety_boundary banner -> T1-FAIL (regression caught) Reusable via workflow_call; also self-runs on push/PR to main. Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#135 Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/workflows/spark-theatre-gate.yml | 137 +++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 .github/workflows/spark-theatre-gate.yml diff --git a/.github/workflows/spark-theatre-gate.yml b/.github/workflows/spark-theatre-gate.yml new file mode 100644 index 0000000..cc71343 --- /dev/null +++ b/.github/workflows/spark-theatre-gate.yml @@ -0,0 +1,137 @@ +# SPDX-License-Identifier: PMPL-1.0 +name: SPARK Theatre Gate + +# Estate anti-theatre lint (hyperpolymath/standards#135, sub-issue of #124). +# +# Kills "SPARK proof theatre": an Ada unit that declares SPARK_Mode (On) +# and banners itself "formally verified" / "(Gold)" / "SPARK Proof Level" +# while no GNATprove run has ever discharged an obligation for it. +# +# Per SPARK_Mode-On compilation unit, with no repo-wide prover evidence: +# +# T1 HEADER PROOF-CLAIM WITHOUT PROVER (hard fail, always) +# A strong proof assertion ("formally verified", "SPARK Proof +# Level", "(Gold)", "all preconditions and postconditions are +# verified", "proving the invariant holds") appears in the file +# HEADER BANNER (the comment block before the first code token) of a +# SPARK_Mode-On unit. Header-scoped on purpose: an incidental phrase +# in a comment deep in the body (e.g. an enum-literal description) is +# NOT a claim about the unit and must not trip the gate. +# +# T2 ZERO-CONTRACT SPARK_Mode (issue #135 verbatim; warn by default) +# SPARK_Mode (On) with no Pre/Post/Global/Depends/Contract_Cases. +# Hollow SPARK_Mode that proves nothing. Emitted as a warning so +# repos mid Ada/SPARK->Rust/SPARK migration are not broken on +# rollout; escalates to a hard failure when the caller passes +# enforce_zero_contract: true (target end-state per #135). +# +# Genuine SPARK repos (echidna, stapeln, ...) pass: GNATprove runs in CI, +# so "prover evidence" is present and neither T1 nor T2 fires. The gate +# only bites a regression that re-introduces a hollow "verified" claim. +# +# Reusable: a consumer repo adds a 3-line caller (see ambientops +# .github/workflows/spark-proof-gate.yml). It also self-runs on standards. + +on: + workflow_call: + inputs: + paths: + description: "Space-separated roots to scan (default: repo root)." + required: false + type: string + default: "." + enforce_zero_contract: + description: "Escalate T2 (zero-contract SPARK_Mode) from warning to hard failure." + required: false + type: boolean + default: false + push: + branches: [main, master] + pull_request: + branches: [main, master] + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + spark-theatre-gate: + name: SPARK Theatre Gate + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Scan for SPARK proof theatre + env: + SCAN_PATHS: ${{ inputs.paths || '.' }} + ENFORCE_T2: ${{ inputs.enforce_zero_contract && 'on' || 'off' }} + run: | + set -uo pipefail + + # --- Repo-wide: is GNATprove ever actually run? ------------------- + prover_evidence=0 + if grep -rIlE 'gnatprove' .github/workflows 2>/dev/null | grep -q .; then + prover_evidence=1 + fi + for bf in Justfile justfile Mustfile Dustfile; do + [ -f "$bf" ] && grep -qI 'gnatprove' "$bf" && prover_evidence=1 + done + if find . \( -name 'gnatprove.out' -o -name '*.spark' \ + -o -path '*/gnatprove/*.json' \) \ + -not -path '*/.git/*' 2>/dev/null | grep -q .; then + prover_evidence=1 + fi + echo "prover_evidence=$prover_evidence enforce_t2=$ENFORCE_T2" + + claim_re='formally verified|SPARK Proof Level|\(Gold\)|all preconditions and postconditions are verified|proving the invariant holds' + contract_re='Pre[[:space:]]*=>|Post[[:space:]]*=>|Global[[:space:]]*=>|Depends[[:space:]]*=>|Contract_Cases' + sparkon_re='pragma[[:space:]]+SPARK_Mode[[:space:]]*\([[:space:]]*On[[:space:]]*\)|with[[:space:]]+SPARK_Mode[[:space:]]*=>[[:space:]]*On' + + fail=0 + while IFS= read -r f; do + [ -z "$f" ] && continue + + # Active SPARK_Mode-On aspect, ignoring commented-out lines. + grep -vE '^[[:space:]]*--' "$f" | grep -qE "$sparkon_re" || continue + + # Header banner = the leading run of comment / blank lines up to + # (but excluding) the first non-comment, non-blank code token. + header="$(awk ' + /^[[:space:]]*--/ || /^[[:space:]]*$/ { print; next } + { exit }' "$f")" + + has_header_claim=0 + printf '%s\n' "$header" | grep -qiE "$claim_re" && has_header_claim=1 + has_contract=0 + grep -qE "$contract_re" "$f" && has_contract=1 + + [ "$prover_evidence" -eq 1 ] && continue # prover runs: not theatre + + if [ "$has_header_claim" -eq 1 ]; then + echo "::error file=$f::T1 SPARK theatre: header banner claims formal proof but no GNATprove run exists in this repo. Wire gnatprove into CI, or remove the claim and set SPARK_Mode Off (see proven#24 / ambientops safety_boundary for the honest-demotion pattern)." + fail=1 + elif [ "$has_contract" -eq 0 ]; then + if [ "$ENFORCE_T2" = "on" ]; then + echo "::error file=$f::T2 zero-contract SPARK_Mode (standards#135): SPARK_Mode (On) with no Pre/Post/Global/Depends/Contract_Cases and no prover. Add real contracts + a gnatprove gate, or set SPARK_Mode Off." + fail=1 + else + echo "::warning file=$f::T2 zero-contract SPARK_Mode (standards#135): SPARK_Mode (On) proves nothing here (no contracts, no prover). Demote to SPARK_Mode Off or add contracts. Escalates to a hard failure once enforce_zero_contract is set." + fi + fi + done < <( + for root in $SCAN_PATHS; do + find "$root" \( -name '*.ads' -o -name '*.adb' \) \ + -not -path '*/.git/*' -not -path '*/obj/*' \ + -not -path '*/node_modules/*' 2>/dev/null + done + ) + + if [ "$fail" -ne 0 ]; then + echo "::error::SPARK Theatre Gate FAILED — see annotations. Doctrine: a SPARK_Mode-On unit must either be genuinely proved (GNATprove in CI) or honestly demoted (SPARK_Mode Off + tracked obligation). No hollow 'verified' claims." + exit 1 + fi + echo "✓ SPARK Theatre Gate passed (no hollow header proof claims found)."