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 1/2] 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 00000000..cc713437 --- /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)." From ad722e7d989f72fbb028afebf619e5cf28a7dc00 Mon Sep 17 00:00:00 2001 From: hyperpolymath Date: Tue, 19 May 2026 18:31:34 +0100 Subject: [PATCH 2/2] port(session-management-standards/src/ui/tea/system_update_gui.affine): ReScript surface -> AffineScript (Refs #229) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Oracle-validated Tier-1 port (affinescript main @ #229 canonical map, docs/RESCRIPT-ELIMINATION.adoc): - List(T) -> [T] (1 occurrence) - expression-position record literals { ... } -> #{ ... } (the record sigil, spec.md:414-421). Match record-PATTERNS and struct/enum/type decl bodies correctly left as { } (sigil is expression-literal-only, oracle-confirmed). - ReScript string `+` -> AffineScript `++` where present (concat is `++`; `+` is numeric — left a String/Int unify error beneath the parse wall; numeric `+`/`-` untouched). Verified: `affinescript main check session-management-standards/src/ui/tea/system_update_gui.affine` -> Type checking passed (was: parse error / DRIFT-SYNTAX pre-port). Self-contained file, no imports. Refs #229 (estate-wide, sequenced, human-gated — not Closes). Co-Authored-By: Claude Opus 4.7 (1M context) --- .../src/ui/tea/system_update_gui.affine | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/session-management-standards/src/ui/tea/system_update_gui.affine b/session-management-standards/src/ui/tea/system_update_gui.affine index 40a251a1..541b27be 100644 --- a/session-management-standards/src/ui/tea/system_update_gui.affine +++ b/session-management-standards/src/ui/tea/system_update_gui.affine @@ -37,7 +37,7 @@ struct UpdateStep { struct Model { current_stage: UpdateStage, - steps: List(UpdateStep), + steps: [UpdateStep], is_running: Bool, log_output: String, history_depth: Int @@ -56,7 +56,7 @@ enum Msg { // ── TEA Logic ──────────────────────────────────────────────────────────────── fn system_update_init() -> Model { - { + #{ current_stage: UpdateStage::RpmOstree, steps: [], is_running: false, @@ -70,7 +70,7 @@ fn system_update_update(@linear msg: Msg, @linear model: Model) -> Model { { current_stage: cs, steps: s, is_running: ir, log_output: lo, history_depth: h } => { match msg { StartUpdate => { - { + #{ current_stage: UpdateStage::RpmOstree, steps: s, is_running: true, @@ -80,7 +80,7 @@ fn system_update_update(@linear msg: Msg, @linear model: Model) -> Model { } StageStarted(stage) => { - { + #{ current_stage: stage, steps: s, is_running: true, @@ -90,7 +90,7 @@ fn system_update_update(@linear msg: Msg, @linear model: Model) -> Model { } StageFinished(stage, status, elapsed) => { - { + #{ current_stage: stage, // Next stage logic would be here steps: s, is_running: true, @@ -100,18 +100,18 @@ fn system_update_update(@linear msg: Msg, @linear model: Model) -> Model { } UpdateLog(new_line) => { - { + #{ current_stage: cs, steps: s, is_running: ir, - log_output: lo + "\n" + new_line, + log_output: lo ++ "\n" ++ new_line, history_depth: h } } PopState => { if h > 0 { - { + #{ current_stage: UpdateStage::RpmOstree, steps: s, is_running: false, @@ -119,7 +119,7 @@ fn system_update_update(@linear msg: Msg, @linear model: Model) -> Model { history_depth: h - 1 } } else { - { + #{ current_stage: cs, steps: s, is_running: ir,