Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions .github/workflows/ci-integrity.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 3 additions & 14 deletions .github/workflows/proven-tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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 . \
Expand All @@ -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()
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/recon.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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" \
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# RSR-compliant .gitignore
/target
/tools/ci/target/
/reports/
/verisimdb-data/
/runtime/
Expand Down
4 changes: 2 additions & 2 deletions Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -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 . \
Expand All @@ -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 \
Expand Down
2 changes: 1 addition & 1 deletion docs/CI-CD.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
39 changes: 39 additions & 0 deletions docs/native-ci-helper-migration.adoc
Original file line number Diff line number Diff line change
@@ -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.
2 changes: 1 addition & 1 deletion proven/ledger.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
33 changes: 33 additions & 0 deletions scripts/ci/test-inventory-failure.sh
Original file line number Diff line number Diff line change
@@ -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; }

Check failure on line 22 in scripts/ci/test-inventory-failure.sh

View check run for this annotation

SonarQubeCloud / SonarCloud Code Analysis

Use '[[' instead of '[' for conditional tests. The '[[' construct is safer and more feature-rich.

See more on https://sonarcloud.io/project/issues?id=hyperpolymath_panic-attacker&issues=AaG2FUpGT8I3H7DQ5bED&open=AaG2FUpGT8I3H7DQ5bED&pullRequest=270
[ ! -e "$work/inventory.json" ] || { echo 'partial inventory was emitted' >&2; exit 1; }

Check failure on line 23 in scripts/ci/test-inventory-failure.sh

View check run for this annotation

SonarQubeCloud / SonarCloud Code Analysis

Use '[[' instead of '[' for conditional tests. The '[[' construct is safer and more feature-rich.

See more on https://sonarcloud.io/project/issues?id=hyperpolymath_panic-attacker&issues=AaG2FUpGT8I3H7DQ5bEE&open=AaG2FUpGT8I3H7DQ5bEE&pullRequest=270
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; }

Check failure on line 32 in scripts/ci/test-inventory-failure.sh

View check run for this annotation

SonarQubeCloud / SonarCloud Code Analysis

Use '[[' instead of '[' for conditional tests. The '[[' construct is safer and more feature-rich.

See more on https://sonarcloud.io/project/issues?id=hyperpolymath_panic-attacker&issues=AaG2FUpGT8I3H7DQ5bEG&open=AaG2FUpGT8I3H7DQ5bEG&pullRequest=270

Check failure on line 32 in scripts/ci/test-inventory-failure.sh

View check run for this annotation

SonarQubeCloud / SonarCloud Code Analysis

Use '[[' instead of '[' for conditional tests. The '[[' construct is safer and more feature-rich.

See more on https://sonarcloud.io/project/issues?id=hyperpolymath_panic-attacker&issues=AaG2FUpGT8I3H7DQ5bEF&open=AaG2FUpGT8I3H7DQ5bEF&pullRequest=270
echo 'Inventory failure and empty-suite controls passed.'
16 changes: 11 additions & 5 deletions scripts/proven/inventory.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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; }
Loading
Loading