Replace policy-violating CI helpers with tested native Rust contracts

Author: hyperpolymath

.github/workflows/ci-integrity.yml

@@ -117,6 +117,13 @@ jobs:
           done
           exit "$fail"
 
+      - name: Native CI helper contracts
+        run: |
+          set -euo pipefail
+          cargo test --locked --manifest-path tools/ci/Cargo.toml
+          cargo clippy --locked --manifest-path tools/ci/Cargo.toml --all-targets -- -D warnings
+          bash scripts/ci/test-inventory-failure.sh
+
       - name: Repository path portability
         run: |
           set -euo pipefail

.github/workflows/proven-tests.yml

@@ -81,7 +81,7 @@ jobs:
       - name: Derive the run report (cells must select real tests)
         run: |
           bash scripts/ci/annotate.sh "proven:ledger" -- \
-          python3 scripts/proven/verify-ledger.py \
+          bash scripts/proven/verify-ledger.sh \
             --inventory /tmp/inventory.json \
             --ledger proven/ledger.json \
             --root . \
@@ -101,19 +101,8 @@ jobs:
             --proven-tests-root . \
             --fail-on-defect \
             --output /tmp/proven-aggregate.json
-          python3 - <<'PY'
-          import json
-          agg = json.load(open('/tmp/proven-aggregate.json'))
-          records = agg['proven_tests']
-          assert len(records) == 1, records
-          record = records[0]
-          assert record['defects'] == [], record['defects']
-          summary = record['summary']
-          assert summary['total'] > 0, summary
-          print(f"proven-tests: {summary['passed']}/{summary['total']} passed, "
-                f"{summary['covered_cells']}/{summary['cat_aspect_cells']} cells, "
-                f"{summary['actually_proven']} actually-proven")
-          PY
+          jq -e '.proven_tests | type == "array" and length == 1 and (.[0].defects == []) and (.[0].summary.total | type == "number" and . > 0)' /tmp/proven-aggregate.json > /dev/null
+          jq -r '.proven_tests[0].summary | "proven-tests: \(.passed)/\(.total) passed, \(.covered_cells)/\(.cat_aspect_cells) cells, \(.actually_proven) actually-proven"' /tmp/proven-aggregate.json
 
       - name: Publish to the job summary
         if: always()

.github/workflows/recon.yml

@@ -142,7 +142,7 @@ jobs:
           if [ "${{ github.event_name }}" = "workflow_dispatch" ] && [ "${{ inputs.fail_on_new }}" = "false" ]; then
             args="--no-fail"
           fi
-          python3 scripts/recon/compare.py \
+          bash scripts/recon/compare.sh \
             --baseline recon/baseline.json \
             --assail "$SARIF_DIR/assail.json" \
             --pons "$SARIF_DIR/pons.json" \

.gitignore

@@ -1,5 +1,6 @@
 # RSR-compliant .gitignore
 /target
+/tools/ci/target/
 /reports/
 /verisimdb-data/
 /runtime/

Justfile

@@ -305,7 +305,7 @@ proven:
     set -euo pipefail
     cargo build --locked --release
     bash scripts/proven/inventory.sh /tmp/panic-attack-tests.json
-    python3 scripts/proven/verify-ledger.py \
+    bash scripts/proven/verify-ledger.sh \
       --inventory /tmp/panic-attack-tests.json \
       --ledger proven/ledger.json \
       --root . \
@@ -324,7 +324,7 @@ recon:
     set -euo pipefail
     mkdir -p recon-out
     cargo run --release --quiet -- assail . --output recon-out/assail.json --quiet
-    python3 scripts/recon/compare.py \
+    bash scripts/recon/compare.sh \
       --baseline recon/baseline.json \
       --assail recon-out/assail.json \
       --pons /dev/null \

docs/CI-CD.adoc

@@ -201,7 +201,7 @@ never declared**, so:
 
 * `scripts/proven/inventory.sh` asks the test runner what tests exist, per
   binary;
-* `scripts/proven/verify-ledger.py` fails when a cell selects no executed test,
+* `scripts/proven/verify-ledger.sh` fails when a cell selects no executed test,
   when an executed test is claimed by nothing, or when a stronger tier is
   claimed than the evidence supports;
 * the resulting report is fed to `panic-attack aggregate --proven-tests

docs/native-ci-helper-migration.adoc

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Native CI helper migration — 7 November 2026
+
+Fresh governance execution exposed two production Python helpers that violate
+the estate language policy. They are replaced by the Rust programs in
+`tools/ci`, called through the existing-purpose shell entrypoints. Workflow,
+Justfile and ledger pointers are updated together; no language-policy waiver
+or scanner exclusion is added. The workflow's inline aggregate check uses
+its already required jq, with the original nonempty/defect-free assertions.
+
+The standalone dev-tool workspace has its own generated lockfile and is not
+an application binary or a new root test binary. It retains the ledger's
+coordinate selectors, first matching buckets, remainder ratchet, declared
+absence conflict check and proof-file requirements. Test identities now name
+both the test binary and test name so equal names cannot collapse across
+binaries. Empty inventories, missing coordinates and invalid proof tiers
+remain failures; a failed claim does not overwrite an existing report.
+
+Recon preserves category-debt comparison, bootstrap baselines and explicit
+`--no-fail` advisory mode. Missing, invalid or unrecognised scanner reports
+are unavailable, never clean: strict mode fails and no replacement baseline
+is proposed. SARIF rule identifiers are recognised alongside JSON categories.
+
+The inventory producer now preserves a failed Cargo enumeration instead of
+turning it into an empty successful list. It does not write an empty/partial
+inventory. A dedicated CI fault test injects a failing test binary and an
+empty suite; this Bash control is a hosted Linux check, not a claimed Windows
+execution.
+
+Local Windows evidence: six library controls and three CLI integration tests
+pass. They cover stale/empty claims, binary-name collisions, absent/covered
+conflicts, missing proof warrants, remainder bounds, malformed scanner data,
+debt regressions and unavailable/advisory behaviour. The actual repository
+ledger's taxonomy and selectors are checked. CI runs these controls and
+all-targets Clippy with warnings denied before testing the real inventory.
+
+Creusot with Pearlite contracts: `OPEN`, not run for these CI utilities.
+Verus: `OPEN`, not run. Executable contract tests are not formal proofs;
+framework provenance tiers are retained and no independent witness is claimed.

proven/ledger.json

@@ -42,7 +42,7 @@
   },
   "doctrine": [
     "A cell is covered only when a test that actually ran selected it. Nothing",
-    "here declares coverage; scripts/proven/verify-ledger.py derives it from a",
+    "here declares coverage; scripts/proven/verify-ledger.sh derives it from a",
     "test inventory produced by `cargo test -- --list` in the same commit.",
     "Tiers are the framework's three: Actually-Proven (a machine-checked proof",
     "ladder exists), Provisionally-Proven (typed assertions, example/property",

scripts/ci/test-inventory-failure.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+set -euo pipefail
+root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+mkdir -p "$work/bin" "$work/repo/tests"
+printf '' > "$work/repo/tests/broken.rs"
+cat > "$work/bin/cargo" <<'MOCK'
+#!/usr/bin/env bash
+case " $* " in
+  *' --lib '*) printf 'library_control: test\n' ;;
+  *) exit 42 ;;
+esac
+MOCK
+chmod +x "$work/bin/cargo"
+cd "$work/repo"
+set +e
+PATH="$work/bin:$PATH" bash "$root/scripts/proven/inventory.sh" "$work/inventory.json"
+status=$?
+set -e
+[ "$status" -eq 42 ] || { echo 'failed enumeration was not preserved' >&2; exit 1; }
+[ ! -e "$work/inventory.json" ] || { echo 'partial inventory was emitted' >&2; exit 1; }
+cat > "$work/bin/cargo" <<'MOCK'
+#!/usr/bin/env bash
+exit 0
+MOCK
+set +e
+PATH="$work/bin:$PATH" bash "$root/scripts/proven/inventory.sh" "$work/empty.json"
+status=$?
+set -e
+[ "$status" -eq 1 ] && [ ! -e "$work/empty.json" ] || { echo 'empty inventory was certified' >&2; exit 1; }
+echo 'Inventory failure and empty-suite controls passed.'

scripts/proven/inventory.sh

@@ -30,7 +30,10 @@ add() {
 }
 
 # Library unit tests (module::path::name).
-add "panic_attack" "$(cargo test --locked --lib -- --list 2>/dev/null || true)"
+names="$(cargo test --locked --lib -- --list)" || {
+  code=$?; echo 'inventory: library test enumeration failed' >&2; exit "$code";
+}
+add "panic_attack" "$names"
 
 # Integration test binaries, one per tests/*.rs file.
 for f in tests/*.rs; do
@@ -40,11 +43,14 @@ for f in tests/*.rs; do
     # shell-driven fixtures, not Rust test binaries
     verisimdb_e2e) continue ;;
   esac
-  add "$bin" "$(cargo test --locked --test "$bin" -- --list 2>/dev/null || true)"
+  names="$(cargo test --locked --test "$bin" -- --list)" || {
+    code=$?; echo "inventory: test enumeration failed for $bin" >&2; exit "$code";
+  }
+  add "$bin" "$names"
 done
 
+total="$(jq '[.[] | length] | add // 0' "$tmp")"
+bins="$(jq 'length' "$tmp")"
+[ "$total" -gt 0 ] || { echo "inventory: no tests found — refusing to certify an empty suite" >&2; exit 1; }
 jq -S . "$tmp" > "$OUT"
-total="$(jq '[.[] | length] | add // 0' "$OUT")"
-bins="$(jq 'length' "$OUT")"
 echo "inventory: $total test(s) in $bins binar(ies) -> $OUT"
-[ "$total" -gt 0 ] || { echo "inventory: no tests found — refusing to certify an empty suite" >&2; exit 1; }