diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 34079dd..a627693 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -17,17 +17,17 @@ workflows: '.github/workflows/estate-rules.yml': - 'actions/checkout@v7.0.1' '.github/workflows/governance.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/guix-policy.yml': - 'actions/checkout@v7.0.1' '.github/workflows/hypatia-scan.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/instant-sync.yml': [] '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] '.github/workflows/lock-sync-gate.yml': [] '.github/workflows/mirror.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/openssf-compliance.yml': - 'actions/checkout@v7.0.1' '.github/workflows/pages.yml': @@ -51,16 +51,16 @@ workflows: '.github/workflows/runtime-policy.yml': - 'actions/checkout@v7.0.1' '.github/workflows/rust-ci.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/scorecard.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/secret-scanner.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/security-policy.yml': - 'actions/checkout@v7.0.1' '.github/workflows/squabble-action.yml': [] '.github/workflows/standards-pipeline.yml': - - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66' + - 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d' '.github/workflows/static-analysis-gate.yml': - 'actions/checkout@v7.0.1' - 'actions/download-artifact@v8.0.2' @@ -200,35 +200,34 @@ dependencies: commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef' owner_id: 6759885 repo_id: 1352485172 - 'hyperpolymath/standards@427eb35c40552d912d8c757518e8326f0d20f597': - ref: '427eb35c40552d912d8c757518e8326f0d20f597' - commit: 'sha1-427eb35c40552d912d8c757518e8326f0d20f597' - owner_id: 6759885 + 'hyperpolymath/standards@d55304a01b5260b0511aae0d14ed8b8770b00293': + ref: 'd55304a01b5260b0511aae0d14ed8b8770b00293' + commit: 'sha1-d55304a01b5260b0511aae0d14ed8b8770b00293' + owner_id: 297579217 repo_id: 1116521501 uses: - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' - - 'dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f' + - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8' - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406' - 'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6' - - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555' - 'hyperpolymath/standards@75bd5994470661a099df562d6d5ad2fe744dbd66': - ref: '75bd5994470661a099df562d6d5ad2fe744dbd66' - commit: 'sha1-75bd5994470661a099df562d6d5ad2fe744dbd66' - owner_id: 6759885 + 'metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d': + ref: '8e48b1caade08a552646adeab66558ac43b4360d' + commit: 'sha1-8e48b1caade08a552646adeab66558ac43b4360d' + owner_id: 297579217 repo_id: 1116521501 uses: - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9' - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9' - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed' - - 'dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f' + - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8' - 'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393' - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124' - 'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63' - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406' - 'haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' - - 'hyperpolymath/standards@427eb35c40552d912d8c757518e8326f0d20f597' - - 'ossf/scorecard-action@2d1146689b8cda280b9bc96326124645441f03bc' + - 'hyperpolymath/standards@d55304a01b5260b0511aae0d14ed8b8770b00293' + - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e' - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6' - 'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6' - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555' @@ -237,6 +236,11 @@ dependencies: commit: 'sha1-2d1146689b8cda280b9bc96326124645441f03bc' owner_id: 67707773 repo_id: 421101922 + 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e': + ref: 'v2.5.0' + commit: 'sha1-fa7117db83c52d787ae5a89f350999701505d78e' + owner_id: 67707773 + repo_id: 421101922 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6': ref: 'v2.2.0' commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6' diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index c9605f7..0b86783 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -18,7 +18,7 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/governance-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d permissions: actions: read contents: read diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index d7b0447..ca0ef8e 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -27,4 +27,4 @@ permissions: jobs: hypatia: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d diff --git a/.github/workflows/lock-sync-gate.yml b/.github/workflows/lock-sync-gate.yml index db046cb..15d1245 100644 --- a/.github/workflows/lock-sync-gate.yml +++ b/.github/workflows/lock-sync-gate.yml @@ -8,7 +8,7 @@ name: Lock Sync Gate # of a repository's CI that way, because Dependabot rewrites `uses:` refs in the # YAML and cannot touch the lockfile. Measured across 200 repositories on # 2026-09-22: 39 had silently dead CI from exactly this cause. -# See hyperpolymath/standards#968. +# See metadatastician/standards#968. # # This workflow deliberately carries NO `uses:` of its own. It checks out by # calling git in a `run:` step instead of using actions/checkout, so it has no diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index 9d0e5cd..7c4cc39 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -13,7 +13,7 @@ permissions: contents: read jobs: mirror: - uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d # Only the seven forge keys the callee declares (standards#1108 §6b); # `secrets: inherit` forwarded every repository secret (WH008, zizmor # secrets-inherit) to a workflow that asks for exactly these. diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index a6ff8b7..b9fa591 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -16,7 +16,7 @@ permissions: contents: read jobs: rust-ci: - uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/rust-ci-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d permissions: actions: read contents: read diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 941aade..0ef1c9d 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -16,7 +16,7 @@ permissions: jobs: scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d permissions: actions: read contents: read diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 40a0e44..0f2a0fe 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -22,7 +22,7 @@ permissions: # .github/workflows/README.adoc. jobs: scan: - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@8e48b1caade08a552646adeab66558ac43b4360d # No `secrets:` block, deliberately: secret-scanner-reusable.yml @75bd5994 # declares no caller secrets and reads no `secrets.*` context, so # `secrets: inherit` only forwarded every repository secret to a workflow diff --git a/.github/workflows/standards-pipeline.yml b/.github/workflows/standards-pipeline.yml index 64e8f43..ee24ab1 100644 --- a/.github/workflows/standards-pipeline.yml +++ b/.github/workflows/standards-pipeline.yml @@ -5,14 +5,14 @@ # not an adoption, and it is expected to be informative whether it is green or # red. # -# `.machine_readable/pipeline-allow.txt` in hyperpolymath/standards is seeded +# `.machine_readable/pipeline-allow.txt` in metadatastician/standards is seeded # EMPTY by doctrine. Its own text: "An entry here must be EARNED BY # OBSERVATION: the pipeline ran in that repository and went red. It must never # be seeded by inference." and "The honest seed is a dry-run wave: adopt the # caller in a deliberate sample, record the real verdict per repository, and add # only what actually went red." This caller is how that observation is earned. # -# ⚠ KNOWN DEFECT DISCLOSED: hyperpolymath/standards#976 — ci-pipeline.yml's +# ⚠ KNOWN DEFECT DISCLOSED: metadatastician/standards#976 — ci-pipeline.yml's # `detect` job counts `*.ncl` into its ecosystem denominator, and the RSR # template ships a six-file k9 Nickel set into every seeded repository, so # TOTAL can be lifted above zero by boilerplate alone and the zero-denominator @@ -33,10 +33,10 @@ permissions: jobs: pipeline: - # hyperpolymath/standards @ 75bd5994 (standards main 2026-10-19; see actions.lock). + # metadatastician/standards @ 8e48b1ca (standards main 2026-10-25; see actions.lock). # # NO `secrets:` block, deliberately. ci-pipeline.yml declares # `workflow_call.inputs` only, has no `secrets:` block and references no # `secrets.*` anywhere; `secrets: inherit` would hand the whole store to a # workflow that consumes none of it. - uses: hyperpolymath/standards/.github/workflows/ci-pipeline.yml@75bd5994470661a099df562d6d5ad2fe744dbd66 + uses: metadatastician/standards/.github/workflows/ci-pipeline.yml@8e48b1caade08a552646adeab66558ac43b4360d diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 6223b79..a015342 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -102,3 +102,13 @@ CHANGELOG.adoc # Project documentation (AsciiDoc-by-default). CODE_OF_CONDUCT.adoc # Project documentation (AsciiDoc-by-default). SECURITY.adoc # Project documentation (AsciiDoc-by-default). .mise.toml # Repo-specific mise config; must sit at the root to be found. + +# ─── Declared 2026-10-25: downstream integration contracts. +# Two published, immutable-revision contracts that OTHER repositories +# integrate against: the read-only squabble CI invocation, and the +# Proven-Tests evidence format a Rust repository submits to. They are a +# top-level component rather than documentation: a consumer clones this +# tree at a pinned commit and runs contracts/bin/ from it, so the path is +# part of the contract's published surface and cannot be moved without +# breaking every pin. See contracts/README.adoc. +contracts/ diff --git a/Justfile b/Justfile index f927e32..d77cf3c 100644 --- a/Justfile +++ b/Justfile @@ -222,6 +222,28 @@ crg-badge: test-all: test e2e aspect bench readiness @echo "All test categories passed — safe to merge!" +# ── Downstream integration contracts ────────────────────────────────────────── +# Two published, immutable-revision contracts live in contracts/: the read-only +# CI invocation of squabble (contracts/squabble), and the evidence format a Rust +# repository submits to Proven-Tests (contracts/proven-tests). Both suites need +# bash, awk, coreutils and jq — no Rust and no Idris2 — so they run anywhere. +# See contracts/README.adoc. + +# Run both contract conformance suites +contract-test: + #!/usr/bin/env bash + set -euo pipefail + bash contracts/squabble/tests/run-conformance.sh + bash contracts/proven-tests/tests/run-conformance.sh + +# Verify a contract pin exactly as a downstream consumer does: just contract-pin squabble 1.0.0 +contract-pin CONTRACT REVISION: + bash contracts/bin/verify-pin.sh {{CONTRACT}} {{REVISION}} + +# Regenerate a contract's sha256 manifest after an intended change: just contract-manifest squabble +contract-manifest CONTRACT: + bash contracts/bin/make-shasums.sh contracts/{{CONTRACT}} + # Run all quality checks quality: fmt-check lint test @echo "All quality checks passed!" diff --git a/README.adoc b/README.adoc index c49ee95..064ad3a 100644 --- a/README.adoc +++ b/README.adoc @@ -54,6 +54,40 @@ healthy. See `docs/proposals/squabble-modes-and-app-layer.adoc` for where this is heading: upstream conformance, custodian rulesets, and the app-aware layer. +== Downstream integration contracts (pinned, immutable revisions) + +`contracts/` publishes two contracts that other repositories integrate against. +Both are consumed by *revision id plus a sha256 manifest*, never by a branch: + +[cols="1,2"] +|=== +| `contracts/squabble` — `squabble-contract/1.0.0` +| The read-only CI invocation: which subcommands are in contract, the six read + permissions the gate needs (and the `administration: read` an App token must + supply), the machine-readable gate/verdict documents, the exit semantics, and + the decision procedure for `legitimate_green` — a commit-bound envelope whose + *every* required check ran and passed. Missing, skipped, cancelled, pending and + failing required checks each have a negative fixture proving they cannot reach + it. + +| `contracts/proven-tests` — `proven-tests-evidence/1.0.0` +| The evidence format a Rust repository submits to Proven-Tests: real executed + tests with a log digest, example/property/proof told apart, coverage derived + only from executed non-debt passes, the required Idris2 toolchain for the + framework itself (not for submitting), and a minimal downstream Rust fixture. +|=== + +[source,sh] +---- +just contract-test # both conformance suites +just contract-pin squabble 1.0.0 # verify a pin as a consumer does +bash contracts/bin/verify-pin.sh proven-tests 1.0.0 +---- + +Nothing in either contract writes: no merges, no re-runs, no edits, no admin +overrides. The consumer audit refuses a workflow that grants a write scope, pins +to a moving ref, masks a gate step, or calls `fight --apply`. + == Core principle: squabble ≠ bypass Every "green" the squabbler declares is backed by the gate's *own* required diff --git a/contracts/README.adoc b/contracts/README.adoc new file mode 100644 index 0000000..c5f1ed0 --- /dev/null +++ b/contracts/README.adoc @@ -0,0 +1,101 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Downstream integration contracts +:toc: preamble + +Two contracts live here, one per repository that downstream CI may integrate +against. Both are *published as immutable revisions*, not as branches: a +downstream repository pins a revision id and the sha256 manifest that comes +with it, and a change to any published byte is a new revision. + +[cols="1,2,2"] +|=== +| Contract | Revision | What it pins +| `squabble/` | `squabble-contract/1.0.0` | How a repository invokes cicd-squabbler read-only from CI, the GitHub permissions that invocation needs, the machine-readable output, the exit semantics, and when the tool may declare `legitimate_green`. +| `proven-tests/` | `proven-tests-evidence/1.0.0` | How a Rust repository submits real, executed test evidence; how example, property and proof evidence are told apart; how coverage is derived without claiming untaken tests; the required Idris2 toolchain; and a minimal downstream fixture. +|=== + +== Layout + +[source] +---- +contracts/ +├── bin/ +│ ├── make-shasums.sh write or --check a contract's SHASUMS manifest +│ └── verify-pin.sh verify a downstream pin (revision + digest) end to end +├── squabble/ +│ ├── CONTRACT.adoc the contract itself (normative prose) +│ ├── REVISION the revision id (one line) +│ ├── SHASUMS sha256 of every file in this directory +│ ├── schema/ machine-readable shapes: gate, verdict, envelope, output +│ ├── bin/ legitimate-green, bind-gate, audit-consumer-workflow +│ ├── fixtures/ positive and negative fixtures, each with an expectation +│ └── tests/run-conformance.sh +└── proven-tests/ + ├── EVIDENCE-CONTRACT.adoc the contract itself (normative prose) + ├── LANDING.adoc how this package lands in proven-tests-and-benches + ├── REVISION, SHASUMS + ├── taxonomy-v1.json the 17 categories × 14 aspects this revision knows + ├── schema/ + ├── bin/ verify-evidence, collect-evidence + ├── fixtures/ positive and negative evidence, libtest logs, expectations + ├── downstream-rust-fixture/ a minimal Rust repository that submits evidence + └── tests/run-conformance.sh +---- + +== Why a revision and not a branch + +A downstream CI job that does `uses: hyperpolymath/cicd-squabbler@main` or +`git clone --branch main` is trusting whatever landed last. Two consequences, +both measured in this estate: + +* A required check silently changes meaning between the run that was reviewed + and the run that gates the merge. +* A green claim becomes unreproducible: nobody can say which rule produced it. + +So every pin in these contracts is a content pin: + +[cols="1,2"] +|=== +| Pin | How +| The contract itself | revision id + `SHASUMS` digest of that revision, recorded by the consumer +| The squabble action | `uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@<40-hex sha>` +| The squabble binary | release tag + asset sha256 + build-provenance attestation (checked by `.github/actions/squabble/install.sh`) +| Proven-Tests evidence tooling | commit sha + `SHASUMS` digest of `contracts/proven-tests` +|=== + +`contracts/bin/verify-pin.sh` checks a pin as a consumer would: + +[source,sh] +---- +bash contracts/bin/verify-pin.sh squabble 1.0.0 +bash contracts/bin/verify-pin.sh proven-tests 1.0.0 +---- + +It fails if the `REVISION` file names a different revision, if any listed file +changed, if a listed file is missing, or if a file exists that the manifest +does not list. An unlisted file is a change: the manifest is the closed set. + +== What these contracts deliberately do not do + +* *They do not move.* A revision is frozen. Fixes ship as `1.0.1`; anything + that changes meaning ships as `2.0.0` and consumers opt in. +* *They do not write.* Neither contract's tooling merges, re-runs, edits, + dismisses, or overrides anything. `squabble`'s write-capable subcommands + (`fight --apply`, `board`, `inbox-sweep`) are out of contract, and the + consumer audit refuses a workflow that calls them. +* *They do not claim more than they can see.* Where a check cannot be made — + a verdict that carries no per-requirement run states, a coordinate a human + must review — the tooling says so and refuses, rather than inferring a pass. + +== Running the conformance suites + +[source,sh] +---- +just contract-test +---- + +which runs both suites. Each suite prints one line per fixture and fails unless +every planned case ran, so a fixture that stops being exercised cannot quietly +become a pass. They need `bash`, coreutils and `jq` (v1.6 or later); they do not +need a Rust or Idris2 toolchain. diff --git a/contracts/bin/make-shasums.sh b/contracts/bin/make-shasums.sh new file mode 100755 index 0000000..d34f197 --- /dev/null +++ b/contracts/bin/make-shasums.sh @@ -0,0 +1,141 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# make-shasums.sh — write /SHASUMS: the sha256 of every file in +# that contract directory, so a downstream repository can pin the contract by +# content instead of by a branch name. +# +# bash contracts/bin/make-shasums.sh contracts/squabble +# bash contracts/bin/make-shasums.sh contracts/proven-tests --check +# +# SHASUMS lists paths relative to the contract directory, sorted, one per line +# as " " — the format `sha256sum -c` reads. SHASUMS itself is +# never listed (a file cannot contain its own digest). +# +# --check verifies the existing SHASUMS instead of writing it, and exits 1 on +# any mismatch, missing file or unlisted file. That is what the conformance +# suites run, so a published revision cannot drift silently. +# +# Exit codes: 0 ok, 1 verification failed, 2 usage or environment failure. + +set -euo pipefail + +readonly PROG="make-shasums" +readonly EXIT_FAILED=1 +readonly EXIT_USAGE=2 + +usage() { + printf 'usage: %s [--check]\n' "$PROG" >&2 +} + +die() { + printf '%s: %s\n' "$PROG" "$*" >&2 + exit "$EXIT_USAGE" +} + +# digest FILE — print the sha256 of FILE as lowercase hex, on any box that has +# either coreutils (sha256sum) or the perl-script shasum macOS ships. +digest() { + local out + if command -v sha256sum >/dev/null 2>&1; then + out="$(sha256sum -- "$1")" + elif command -v shasum >/dev/null 2>&1; then + out="$(shasum -a 256 -- "$1")" + else + die "neither sha256sum nor shasum is available" + fi + printf '%s\n' "${out%% *}" +} + +# listed_files DIR — every regular file under DIR except SHASUMS, relative to +# DIR, sorted. `find` order is not portable, so it is sorted here rather than +# trusted; the same set must come out on every machine. +listed_files() { + local dir="$1" + ( cd "$dir" && find . -type f ! -name SHASUMS -print ) \ + | sed 's|^\./||' \ + | LC_ALL=C sort +} + +# write_sums DIR — write DIR/SHASUMS. +# +# The list is built before the manifest exists and the manifest is written +# outside DIR then moved in, so the manifest can never list a half-written +# copy of itself. (It did, once: SHASUMS.tmp appeared in its own manifest and +# the digest check then failed on the temp file it had just deleted.) +write_sums() { + local dir="$1" tmp f + tmp="$(mktemp "${TMPDIR:-/tmp}/shasums.XXXXXX")" + listed_files "$dir" | while IFS= read -r f; do + printf '%s %s\n' "$(digest "$dir/$f")" "$f" + done > "$tmp" + mv -- "$tmp" "$dir/SHASUMS" +} + +# check_sums DIR — verify DIR/SHASUMS against the files on disk. Fails on a +# changed file, a deleted file, and a file present but unlisted: an attacker +# adding a file to a "pinned" directory must not pass unnoticed. +check_sums() { + local dir="$1" line want path have rc=0 + local -a seen=() + if [[ ! -f "$dir/SHASUMS" ]]; then + printf '%s: %s/SHASUMS does not exist\n' "$PROG" "$dir" >&2 + return "$EXIT_FAILED" + fi + while IFS= read -r line; do + [[ -z "$line" ]] && continue + want="${line%% *}" + path="${line#* }" + if [[ ! -f "$dir/$path" ]]; then + printf 'MISSING %s\n' "$path" >&2 + rc="$EXIT_FAILED" + continue + fi + have="$(digest "$dir/$path")" + if [[ "$have" != "$want" ]]; then + printf 'CHANGED %s (listed %s, on disk %s)\n' "$path" "$want" "$have" >&2 + rc="$EXIT_FAILED" + fi + seen+=("$path") + done < "$dir/SHASUMS" + + while IFS= read -r path; do + local known="" + local s + for s in "${seen[@]+"${seen[@]}"}"; do + if [[ "$s" == "$path" ]]; then known="yes"; break; fi + done + if [[ -z "$known" ]]; then + printf 'UNLISTED %s\n' "$path" >&2 + rc="$EXIT_FAILED" + fi + done < <(listed_files "$dir") + return "$rc" +} + +main() { + local dir="" check="no" + while [[ $# -gt 0 ]]; do + case "$1" in + --check) check="yes"; shift ;; + -h|--help) usage; exit 0 ;; + -*) usage; die "unknown option: $1" ;; + *) if [[ -n "$dir" ]]; then usage; die "one contract directory only"; fi; dir="$1"; shift ;; + esac + done + [[ -n "$dir" ]] || { usage; die "missing "; } + [[ -d "$dir" ]] || die "not a directory: $dir" + # A contract directory without a REVISION file is not a contract, so this + # refuses rather than producing digests for some random tree. + [[ -f "$dir/REVISION" ]] || die "$dir has no REVISION file; refusing to digest it" + + if [[ "$check" == "yes" ]]; then + check_sums "$dir" + else + write_sums "$dir" + printf 'wrote %s/SHASUMS (%s files)\n' "$dir" "$(wc -l < "$dir/SHASUMS" | tr -d ' ')" >&2 + fi +} + +main "$@" diff --git a/contracts/bin/verify-pin.sh b/contracts/bin/verify-pin.sh new file mode 100755 index 0000000..2500ce1 --- /dev/null +++ b/contracts/bin/verify-pin.sh @@ -0,0 +1,115 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# verify-pin.sh — verify a downstream pin of one of the contracts in this +# directory, the way a consumer's CI should verify it. +# +# bash contracts/bin/verify-pin.sh squabble 1.0.0 +# bash contracts/bin/verify-pin.sh proven-tests 1.0.0 --repo-dir . +# +# It checks three things and prints a pin block the consumer records: +# +# 1. the contract's REVISION file names exactly the requested revision; +# 2. every file in the contract directory matches its sha256 in SHASUMS; +# 3. no file exists in the contract directory that SHASUMS does not list. +# +# The pin block contains the revision id and the sha256 of SHASUMS itself, so a +# consumer can record one digest instead of one per file. That digest is what +# "pinned contract" means for the rest of these documents. +# +# Exit codes: 0 verified, 1 mismatch or drift, 2 usage or environment failure. + +set -euo pipefail + +readonly PROG="verify-pin.sh" +readonly EXIT_FAILED=1 +readonly EXIT_USAGE=2 + +usage() { + printf 'usage: %s [--repo-dir DIR]\n' "$PROG" >&2 + printf ' revision is the first component of the revision id, e.g. 1.0.0\n' >&2 +} + +die() { + printf '%s: %s\n' "$PROG" "$*" >&2 + exit "$EXIT_USAGE" +} + +# sha256 FILE — lowercase hex digest, coreutils or macOS. +sha256() { + local out + if command -v sha256sum >/dev/null 2>&1; then + out="$(sha256sum -- "$1")" + elif command -v shasum >/dev/null 2>&1; then + out="$(shasum -a 256 -- "$1")" + else + die "neither sha256sum nor shasum is available" + fi + printf '%s\n' "${out%% *}" +} + +main() { + local contract="" revision="" repo_dir="" + while [[ $# -gt 0 ]]; do + case "$1" in + --repo-dir) [[ $# -ge 2 ]] || die "--repo-dir needs a value"; repo_dir="$2"; shift 2 ;; + -h|--help) usage; exit 0 ;; + -*) usage; die "unknown option: $1" ;; + *) if [[ -z "$contract" ]]; then contract="$1" + elif [[ -z "$revision" ]]; then revision="$1" + else usage; die "unexpected argument: $1"; fi + shift ;; + esac + done + [[ -n "$contract" && -n "$revision" ]] || { usage; exit "$EXIT_USAGE"; } + + local root + if [[ -n "$repo_dir" ]]; then + root="$(cd "$repo_dir" && pwd)" + else + root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" + fi + local dir="$root/$contract" + [[ -d "$dir" ]] || die "no such contract directory: $dir" + [[ -f "$dir/REVISION" ]] || die "$dir has no REVISION file" + + local id + id="$(head -n 1 "$dir/REVISION" | tr -d '\r' | sed 's/[[:space:]]*$//')" + if [[ -z "$id" ]]; then + printf 'FAIL %s/REVISION is empty\n' "$contract" >&2 + exit "$EXIT_FAILED" + fi + + # The revision id is "/". Accept the bare version and + # the full id, refuse anything else: a consumer that pins 1.0.0 must not be + # handed 1.1.0 because someone edited REVISION in place. + local want_id + case "$id" in + */"$revision") want_id="$id" ;; + *) want_id="$contract/$revision" ;; + esac + if [[ "$id" != "$want_id" ]]; then + printf 'FAIL %s/REVISION is %s, pinned %s\n' "$contract" "$id" "$want_id" >&2 + exit "$EXIT_FAILED" + fi + if [[ ! -f "$dir/SHASUMS" ]]; then + printf 'FAIL %s/SHASUMS is missing; the revision is unverifiable\n' "$contract" >&2 + exit "$EXIT_FAILED" + fi + + if ! bash "$root/bin/make-shasums.sh" "$dir" --check; then + printf 'FAIL %s drifted from its published SHASUMS\n' "$contract" >&2 + exit "$EXIT_FAILED" + fi + + local sums_digest + sums_digest="$(sha256 "$dir/SHASUMS")" + printf 'verified %s at revision %s\n' "$contract" "$id" + printf 'files %s\n' "$(wc -l < "$dir/SHASUMS" | tr -d ' ')" + printf '\nrecord this pin in the consumer repository:\n\n' + printf ' contract: %s\n' "$id" + printf ' shasums: sha256:%s\n' "$sums_digest" +} + +main "$@" diff --git a/contracts/proven-tests/EVIDENCE-CONTRACT.adoc b/contracts/proven-tests/EVIDENCE-CONTRACT.adoc new file mode 100644 index 0000000..6c922b9 --- /dev/null +++ b/contracts/proven-tests/EVIDENCE-CONTRACT.adoc @@ -0,0 +1,329 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Proven-Tests evidence contract — revision `proven-tests-evidence/1.0.0` +:toc: left +:toclevels: 3 +:sectnums: + +[.lead] +How a *Rust* repository submits evidence that its tests really ran, without +being able to claim more than it can show. One JSON document, one validator, one +derived coverage number. Example, property and proof evidence are separate kinds +with separate obligations, and a claim above `unproven` needs the evidence its +tier requires — in the same run that this document describes. + +IMPORTANT: *Immutability.* Revision `proven-tests-evidence/1.0.0` is frozen. +Consumers pin the revision id and the `SHASUMS` digest +(`bash contracts/bin/verify-pin.sh proven-tests 1.0.0`), never a branch. A +change to a rule id, a field meaning or the decision procedure is a new major +revision; `2.0.0` is refused by this revision's validator rather than +reinterpreted (R7). + +== 1. What a submitter does (four steps, no Idris2 required) + +[source,sh] +---- +# 1. pin this contract by content, not by branch +git clone https://github.com/hyperpolymath/proven-tests-and-benches && cd proven-tests-and-benches +git checkout <40-hex commit> # v0.2.0 == ffb26772e9e3bbb99f0c7f6cd3796e7d99eb64c1 +bash contracts/bin/verify-pin.sh proven-tests 1.0.0 + +# 2. run the tests and keep the log and the exit code +cargo test -- --test-threads=1 2>&1 | tee test.log +cargo_exit="${PIPESTATUS[0]}" + +# 3. turn that one run into evidence (the reference producer) +bash contracts/proven-tests/bin/collect-evidence.sh \ + --repo "$GITHUB_REPOSITORY" --commit "$GITHUB_SHA" \ + --log test.log --exit-code "$cargo_exit" \ + --coords .proven/coords.json \ + --command-argv '["cargo","test","--","--test-threads=1"]' \ + --started-at "$STARTED" --finished-at "$FINISHED" \ + --runner "$ImageOS" --rust "$(rustc --version | cut -d' ' -f2)" \ + > evidence.json + +# 4. admit it, or be refused — and gate the build on the answer +bash contracts/proven-tests/bin/verify-evidence \ + --expect-commit "$GITHUB_SHA" --expect-repo "$GITHUB_REPOSITORY" \ + --require-green evidence.json +---- + +The submitter needs `bash`, coreutils, `awk`, `jq` (1.6+) and a Rust toolchain. +It does **not** need Idris2 (§6). The validator is the gate; the collector is a +convenience that refuses rather than guesses (§5). + +== 2. The document + +[source,json] +---- +{ + "contract": { "name": "hyperpolymath/proven-tests/evidence", "revision": "1.0.0", "major": 1 }, + "subject": { "repo": "owner/name", "commit": "<40 hex>", + "producer": { "tool": "proven-tests collect-evidence", "version": "1.0.0" } }, + "toolchain": { "runner": "ubuntu-24.04", "rust": "1.85.0", "idris2": null }, + "taxonomy": { "revision": "proven-tests/taxonomy/1", "cells": 238 }, + "run": { "command": ["cargo","test"], "exit_code": 0, + "started_at": "…Z", "finished_at": "…Z", "duration_ms": 2000, + "observed_output_digest": "sha256:…" }, + "tests": [ { + "id": "ordering::is_total", + "kind": "example", // example | property | proof + "coord": { "category": "UnitTest", "aspect": "Functionality" }, + "result": "passed", // passed | failed | error | skipped | not_run + "execution": { "ran": true, "command": ["cargo","test"], + "runner": "ubuntu-24.04", + "started_at": "…Z", "finished_at": "…Z", "duration_ms": 2000, + "exit_code": 0, // per-test attributed status + "observed_output_digest": "sha256:…" }, + "claim": "unproven", // unproven | provisionally_proven | actually_proven + "evidence": { }, // tier-specific, see §3 + "fixtures": { "silence": { "path": "…", "description": "…" }, + "firing": { "path": "…", "defect_class": "…" } }, + "anchor": { "log": "test.log", "line": 7 } + } ], + "coverage_claim": { "cells_covered": 2, "tests_passed": 3, "coords": [ … ] }, // optional + "counts": { "records": 3, "executed": 3, "passed": 3, "failed": 0, + "error": 0, "skipped": 0, "not_run": 0, "excluded_debt": 0 } // optional +} +---- + +Machine-readable shape: `schema/evidence-v1.schema.json`. The validator is the +normative enforcer: it refuses a document with a field it cannot interpret as +the type it needs, and it never defaults an unknown value to the favourable one +(an unknown `result` is `R2-result-unknown`, not an implied pass). + +`coverage_claim` and `counts` are *claims*. If present they must agree with the +derivation and with the records (R4, R9). Omitting them is the safest thing a +producer can do, and the reference collector omits `coverage_claim` entirely: it +states what ran, not what is covered. + +== 3. The honesty model: three axes, never collapsed + +A record says three different things. Conflating them is how fabricated green +happens. + +[cols="1,2,2"] +|=== +| Axis | Values | Meaning + +| `result` | `passed` `failed` `error` `skipped` `not_run` | What *this run* did. Only `passed` can be evidence of a property holding. +| `kind` | `example` `property` `proof` | The *shape* of the assertion: one case, many generated cases, or a machine-checked term. +| `claim` | `unproven` `provisionally_proven` `actually_proven` | The warrant this submission establishes for the assertion — not the author's opinion of it. +|=== + +The tier rules, as enforced: + +[cols="1,2,2"] +|=== +| `kind` | Required evidence | Permitted `claim` + +| `example` +| Nothing beyond the execution record. Carries no `property` or `proof` block. +| `unproven`, `provisionally_proven` (the latter needs a type-safety certificate and a named framework certificate) + +| `property` +| `evidence.property` with a generator, `shrinker: true`, `cases_run ≥ 1`, and `failures: 0` when it passed. Zero cases is a runner fault, not evidence. +| `unproven`, `provisionally_proven` + +| `proof` +| `evidence.proof` with `checked: true`, a checker name **and version**, and at least one witnessed rung (`name`, `statement`, `term_digest` as sha256, `file`, `line ≥ 1`). The run must have passed, and its command must be the checker's own invocation. +| `actually_proven` only +|=== + +`actually_proven` is not available to `example` or `property`: sampling is not +proof, however many cases ran. This mirrors `ProvenTests.Types` in the framework, +where `PActuallyProven` requires a non-empty `List1 Witnessed` and +`ActuallyProven` cannot be constructed without it. The difference is that the +framework checks the proof *term* and this contract can only check that a checker +was named, ran, and exited 0 — see §8. + +A record that did not pass may not claim any tier above `unproven` (R2): a +citation that was not re-checked in this run evidences nothing about this tree. + +== 4. Coverage: derived, never accepted + +[source] +---- +covered_cell(t) ⇔ t.result = "passed" + ∧ t.execution is a real execution (R1) + ∧ t.coord is in taxonomy revision proven-tests/taxonomy/1 + ∧ t is not FixtureDebt + ∧ t has no finding of its own +coverage = |{ (c.category, c.aspect) : covered_cell(t) }| +cells_total = 17 × 14 = 238 +---- + +Consequences, each pinned by a fixture: + +* A missing record is **not** coverage. Nothing is inferred from silence; the + report prints the true count and the grid shows `.`. +* A skipped or not-run record is **not** coverage, whatever its claim (§7). +* A record with any finding is **not** coverage: an inadmissible pass must not + paint the map. A forged pass is refused *and* covers nothing. +* A `FixtureDebt` record is **not** coverage and is **not** counted as a test + (`counts.excluded_debt`). This is TEST-DOCTRINE B.4 in the framework + repository: "any check with neither a firing fixture nor this annotation is + not counted", plus "debt-marked tests are not counted in any ledger". The + register may only shrink. +* A `cannot_fail_by_design` record *is* countable: the property is enforced by + the typechecker, which is a stronger thing than a runtime fixture. +* Cells are typed. `UnitTest/Functionality` and `UnitTest/Dependability` are two + cells, and `Unit` (a display name) is not a category at all. + +`verify-evidence --grid` prints the 17×14 map to stderr; the JSON on stdout +carries `coverage.cells_covered`, `coverage.coords` and `coverage.by_category`. + +== 5. The reference producer, and what it refuses + +`bin/collect-evidence.sh` turns one captured libtest run into a submission. It +is a convenience with a strict disposition: it refuses (exit 3, nothing written) +rather than producing a document it cannot stand behind. + +[cols="1,3"] +|=== +| Refusal | Why +| No per-test lines in the log +| Zero tests is not evidence, and an empty submission would read as green-adjacent. +| The libtest summary disagrees with the per-test lines +| The log is truncated or tampered with; 3 claimed and 1 named is not a rounding error. +| Exit code 0 with failures, or non-zero with none +| The harness failed outside the tests, so the run evidences nothing about the suite. +| A test the coordinates file does not map +| A coordinate invented by the producer would be a fabricated cell. Refused by name. +| `--finished-at` before `--started-at`, or a non-UTC timestamp +| An invented execution window is an invented execution. Both timestamps are required. +|=== + +`execution.exit_code` is the status **attributed to that test**: 0 when it +passed, non-zero when it failed, `null` when it did not run. The aggregate status +of the whole invocation is `run.exit_code`, and the gate checks that the two +agree (R11) — including the case where every record passed but the process +exited non-zero. + +== 6. Toolchain + +=== 6.1 To submit evidence (a Rust repository) + +[cols="1,2"] +|=== +| Required | Version / note +| `bash` | 4.0 or later +| `jq` | 1.6 or later (GitHub-hosted Ubuntu runners ship it) +| coreutils / awk / sha256 | `sha256sum` or `shasum -a 256` +| Rust | whichever toolchain the subject crate uses (`toolchain.rust` records it) +| Idris2 | **not required** +|=== + +That is the whole list: the evidence path parses a log and checks JSON. It does +not compile Idris2 and does not need the framework installed. + +=== 6.2 To build or run the Proven-Tests framework itself (Idris2) + +Needed only if the subject *is* the framework, or if it authors Idris2 test +suites. The framework repository pins these; do not invent your own. + +[cols="1,3"] +|=== +| Component | Pin and how it is installed +| Idris2 | `0.7.0`, pinned in `.mise.toml`, `scripts/install-idris2.sh` and both CI pipelines, and cross-checked by `scripts/check-toolchain-pins.sh` (which fails on drift). +| Chez Scheme + GMP headers | The chez backend invokes Chez at *build* time, not only to bootstrap: `chezscheme libgmp-dev` (Debian/Ubuntu) or `chez-scheme gmp-dev` (apk). +| Install | `bash scripts/install-idris2.sh` → installs into `$HOME/.idris2` (idempotent; skips the bootstrap if a compiler is already there). +| Build | `idris2 --build proven-tests.ipkg`, then `idris2 --install proven-tests.ipkg` so dependents can import it. +| Suites | `just test` (framework self-test + type-safe suite + spec suite) or `bash scripts/ci-build.sh`, which is the single source of truth for the CI gate. +| Runtime library path | Idris2 executables need `LD_LIBRARY_PATH` set to `$HOME/.idris2/idris2-*/lib`; both `just test` and `ci-build.sh` derive it from the installed version rather than hardcoding one. +| Downstream `.ipkg` | `depends = proven-tests`, then `import ProvenTests.Framework`. +| Framework source pin | tag `v0.2.0` = commit `ffb26772e9e3bbb99f0c7f6cd3796e7d99eb64c1`. Pin the commit; the tag is a locator. +|=== + +If a repository only *submits* Rust evidence, none of §6.2 applies. A contract +that demanded Idris2 to submit a `cargo test` log would be a reason not to +submit at all. + +== 7. Rules, ids and exit semantics + +[cols="1,3"] +|=== +| Rule id | What it refuses +| `R0-shape` | A document or record that is not an object, or has no `id`. +| `R1-executed-pass` | A `passed` record without `execution.ran = true`, without a non-empty argv whose first element is not a no-op (`true`, `echo`, `sleep`, …), without integer `duration_ms ≥ 0`, with a non-UTC or inverted timestamp pair, without a `sha256:` digest of its captured output, or with `exit_code ≠ 0`. Also a `failed` record whose own execution exited 0. +| `R2-not-run-is-not-a-pass` | A `claim` above `unproven` on a record that did not pass in this submission; an unknown `result`. +| `R3-kind-honesty` | An `example` carrying a property or proof block; a `property` with no generator, no shrinker, zero cases, or failures on a pass; a `proof` that was not checked, names no checker version, has no witnessed rung, or is claimed below `actually_proven`; `actually_proven` claimed by a non-proof kind. +| `R3-tier-evidence` | A tier claimed without its evidence: `provisionally_proven` needs a type-safety certificate and a `framework_safety`; `actually_proven` needs a `design_proof`; `kategoria_level` outside 1..12. +| `R4-coord-unknown` | A category or aspect that is not in taxonomy revision `proven-tests/taxonomy/1`. +| `R4-coverage-claim` | A `coverage_claim` that overstates or omits what the derivation supports, or a `tests_passed` count the records do not back. +| `R5-labelled-skips` | A `skipped`/`not_run` record with no `skip_reason`; a `failed`/`error` record with no `detail`. +| `R6-subject-binding` | A `subject.commit` that is not 40 hex, a repo that is not `owner/name`, or a mismatch against `--expect-commit`/`--expect-repo`. +| `R7-contract-version` | A document whose contract name/major this revision cannot read. +| `R8-duplicate-id` | The same test id twice. +| `R9-counts-reconcile` | A `counts` block that disagrees with the records. +| `R10-fixtures` | A record with no fixture position, or a silence fixture with no reason / a firing fixture with no defect class. +| `R11-run-consistency` | A `run` block whose `exit_code` disagrees with the records, a record citing a different output digest than its run, or a malformed `run`. +|=== + +[cols="1,1,3"] +|=== +| Code | Name | Meaning +| `0` | admissible | Every rule passed. With `--require-green`, additionally: no failed/errored/skipped/not-run record, at least one execution, and `run.exit_code` consistent. +| `3` | refused | A rule fired, or `--require-green` was asked for and the evidence is not green. A finding, not a tool failure. +| `2` | tool failure | Usage, unreadable file, invalid JSON, more than one JSON document, missing `jq`. +|=== + +Admissibility and greenness are deliberately separate. A failing test is +*admissible evidence of failure* — the thing a reviewer most needs — and it can +never be green. The `valid/` fixtures are admissible **and** green; the +`invalid/failing-test-claims-green.json` fixture is admissible and not green. + +`green` requires `passed ≥ 1` on an execution: an empty run is not green, it is +nothing. Neither is a submission whose every test was skipped. + +== 8. Known limitations + +Stated because a contract that hides its blind spots is a claim, not a contract. + +* *Coordinates are declarations.* The validator checks that a coordinate exists + in the taxonomy and that a claim is backed by the evidence its tier requires. + It cannot check that the coordinate is the *right* one for the test. That is + review, and the silence/firing fixture pair is how a coordinate is audited — + which is why R10 exists. +* *The proof term is not checked here.* This revision can require a named + checker, a version, a witnessed rung typechecked by that checker in this run, + and a passing exit — it cannot re-elaborate the term. `ProvenTests.Types` + can; that is what the framework is for. +* *Per-test status is attributed.* `cargo test` runs many tests in one process, + so `execution.exit_code` is the per-test attribution libtest reports, while + `run.exit_code` is the process's own status. R11 refuses the two disagreeing. +* *Binding is the caller's job.* Without `--expect-commit`, the validator cannot + know which commit was intended, and a submission for another commit is + admissible. Pin it. (`invalid/stale-commit.json` is exercised both ways to + make this visible rather than rhetorical.) +* *The log is not embedded.* Only its sha256 is. Retention is the submitter's + job; the digest is what makes the reference checkable. +* *No network.* Nothing here fetches the framework, the taxonomy or the subject; + the taxonomy is pinned inside this revision by digest. + +== 9. Change policy + +[cols="1,2"] +|=== +| Change | Version +| A new rule, a stricter rule, a removed field, a redefined field | major +| A new optional field, a new fixture for an existing rule, a new rule id that refuses something previously allowed | major (a consumer was relying on the old allowance) +| Documentation, or a typo that changes no byte of behaviour | patch, with a regenerated `SHASUMS` +|=== + +Any change regenerates the manifest +(`bash contracts/bin/make-shasums.sh contracts/proven-tests`) and must keep +`bash contracts/proven-tests/tests/run-conformance.sh` green with every planned +case run. + +== 10. Verifying this revision + +[source,sh] +---- +bash contracts/bin/verify-pin.sh proven-tests 1.0.0 # revision + digest, as a consumer checks it +bash contracts/proven-tests/tests/run-conformance.sh # 35 cases: 26 documents + 7 recorded log runs + 2 revision/manifest +---- + +The suite needs `bash`, `awk`, coreutils and `jq`. It needs **no** Rust and no +Idris2 — that is part of the claim, and the suite would fail to start without +them only if the contract had broken it. diff --git a/contracts/proven-tests/LANDING.adoc b/contracts/proven-tests/LANDING.adoc new file mode 100644 index 0000000..e73fcda --- /dev/null +++ b/contracts/proven-tests/LANDING.adoc @@ -0,0 +1,143 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Landing the Proven-Tests evidence contract in its own repository +:toc: preamble + +This package is authored and conformance-tested here, in +`hyperpolymath/cicd-squabbler`, because that is where the downstream-integration +work lives. It belongs in `hyperpolymath/proven-tests-and-benches`: the format is +that repository's, and a contract published by the wrong repository is a contract +nobody pins. This file is the landing checklist, and it is deliberately explicit +about what must not be done. + +== What to copy, where + +[cols="2,2,3"] +|=== +| Here | There | Note +| `contracts/proven-tests/` | `contracts/proven-tests/` | Whole directory, including `SHASUMS` and `REVISION`. Do not edit a byte: the manifest is what downstream pins. +| `contracts/bin/make-shasums.sh` | `contracts/bin/make-shasums.sh` | Needed to maintain the manifest and by `verify-pin`. +| `contracts/bin/verify-pin.sh` | `contracts/bin/verify-pin.sh` | Needed by every consumer, and by the contract's own conformance suite (it is invoked from the docs). +| `contracts/README.adoc` | `contracts/README.adoc` | Edit the table down to the Proven-Tests row, and drop the squabble row: that contract stays here. +| `contracts/squabble/` | _not copied_ | Relevant to Proven-Tests only as a consumer (§4 below). +|=== + +Suggested commit message: + +---- +contracts: publish the Proven-Tests evidence contract, revision 1.0.0 + +Downstream Rust repositories submit real, executed test evidence as one JSON +document; verify-evidence derives coverage from executed passes only, refuses a +skip counted as a pass, and tells example, property and proof evidence apart. +The package carries its own conformance suite (35 cases) and a minimal +downstream fixture. Pinned by revision + SHASUMS; not by a branch. +---- + +== 1. Add the recipes to the Justfile + +The suite needs `bash`, `awk`, coreutils and `jq` — no Rust, no Idris2 — so it +can run as its own CI job as well as inside the existing gate. + +[source,make] +---- +# Contract conformance: the evidence format downstream repositories submit to. +contract-test: + #!/usr/bin/env bash + set -euo pipefail + bash contracts/proven-tests/tests/run-conformance.sh + +# Verify the published contract as a consumer does: `just contract-pin 1.0.0` +contract-pin revision: + bash contracts/bin/verify-pin.sh proven-tests {{revision}} + +# After an intended change: regenerate the manifest, then re-run contract-test. +contract-manifest: + bash contracts/bin/make-shasums.sh contracts/proven-tests +---- + +=== 2. Decide where it gates + +Two honest options: + +* *Its own job* in `.github/workflows/ci.yml` (or `.gitlab-ci.yml`): one step, + `just contract-test`. Requires `jq` on the runner, which `ubuntu-latest` has. +* *Inside the existing gate*: append `contract-test` to the `ci:` recipe's + dependencies. Cheaper, but a contract failure then reads as a framework + failure in the badge. A separate job is easier to attribute. + +Whichever is chosen, the job must not depend on a branch: +`bash contracts/bin/verify-pin.sh proven-tests 1.0.0` fails if `REVISION` or any +published byte moved, so a passing job names the exact revision it validated. + +== 3. Point the documentation at it + +* `README.adoc`: one paragraph under "Using in Your Project", linking + `contracts/proven-tests/EVIDENCE-CONTRACT.adoc` and the fixture. +* `docs/`: add the contract to whichever index lists `docs/`; the contract's + §1 is the only part a Rust submitter needs to read. +* `TEST-NEEDS.adoc`: the "why this file is load-bearing" section is the same + argument this contract mechanises — link it, and say so. +* `DEBT.md`: record that revision 1.0.0 cannot re-elaborate a proof term (§8 of + the contract). `ProvenTests.Types` can; the validator cannot, and the + difference should be visible to someone reading the debt register. + +== 4. Where the two contracts meet + +They are independent revisions and must be pinned separately. + +[cols="1,2"] +|=== +| Proven-Tests evidence contract (this package) +| What a *Rust* subject submits: executed tests, tiers, derived coverage. +| squabble downstream contract (this repository, `contracts/squabble`) +| How *any* repository gates a PR on required checks and decides + `legitimate_green`. Proven-Tests' own CI can consume it, and if it does, it + must not use Proven-Tests' evidence as a substitute for a required check: + evidence is not a check run, and a green evidence document does not satisfy a + ruleset. +|=== + +That last sentence is the one integration mistake worth naming in both +repositories: *evidence before a check is not a passed check.* `squabble +fetch` reports what the ruleset required and what ran; a Proven-Tests submission +reports what a suite established. Neither substitutes for the other. + +== 5. Landing checklist + +. `git checkout -b contracts/evidence-1.0.0` in the Proven-Tests repository. +. Copy the files per the table above; copy nothing else. +. `bash contracts/bin/verify-pin.sh proven-tests 1.0.0` → must print the + revision and the `SHASUMS` digest. If it fails, the copy is incomplete — not + the manifest. +. `bash contracts/proven-tests/tests/run-conformance.sh` → `35 passed, 0 failed, + 35/35 planned cases ran`. A number below 35 planned is a refusal, not a pass. +. Add the `contract-test` recipe and the CI job; run it on the branch. +. Record the published pin in the PR body: ++ +[source] +---- +contract: proven-tests-evidence/1.0.0 +shasums: sha256: +---- +. After merge, tag `v0.3.0` (the next tag, not a re-tag), and make that tag's + commit the pinned one for downstream repositories. Never move an existing tag: + the manifest protects the bytes, but a moved tag still wastes a reviewer's + afternoon. + +== 6. What must not be done + +* *Do not edit a published revision in place.* A fixed typo that changes no byte + of behaviour is `1.0.1` with a regenerated manifest; anything else is a new + major. +* *Do not regenerate `SHASUMS` to "make the check pass".* The check exists to + fail when the bytes moved. If they moved by accident, restore them. +* *Do not let a downstream CI call `main`.* Every document in this package pins + by commit or by digest; a branch is a moving pin. +* *Do not add a rule without a fixture.* The conformance suite counts planned + cases, so a fixture that stops being exercised fails the run rather than + quietly becoming a pass. +* *Do not present the fixture crate as executed evidence.* No `cargo test` ran in + the environment where this package was written; the fixture's own workflow is + the first place it compiles. Any claim to the contrary would be the exact + defect the contract refuses. diff --git a/contracts/proven-tests/REVISION b/contracts/proven-tests/REVISION new file mode 100644 index 0000000..2ddfb01 --- /dev/null +++ b/contracts/proven-tests/REVISION @@ -0,0 +1 @@ +proven-tests-evidence/1.0.0 diff --git a/contracts/proven-tests/SHASUMS b/contracts/proven-tests/SHASUMS new file mode 100644 index 0000000..df97752 --- /dev/null +++ b/contracts/proven-tests/SHASUMS @@ -0,0 +1,51 @@ +a2a0937f2e1a17738be494997b8dc0152c968a2a6b541c41a7b52f540c765b1f EVIDENCE-CONTRACT.adoc +48d6110743d2348fab378346089f9a2a4978762eafce7447ff7ba58507fdbd87 LANDING.adoc +065853ad05ead27715a26086d27d02150fd4276ea90a5b52e43416e472b6856d REVISION +b949def4006a2fe109913d34d77055be9a987013984f9e414bd070b933333231 bin/collect-evidence.sh +54da7c3ecbbeb14f401e53659d5db91d5cf775e9e74b19b7dd0fd8f7aefc4739 bin/verify-evidence +6df30a8a96df9581bca1e201a4a72e3be2fdbd6f8b03b1afb92c331986d4dfb2 downstream-rust-fixture/.github/workflows/proven-evidence.yml +8ce653d6a1b34b4c42883a96fb4ed53683bf74001abaa62bc9a885d9bdedc17e downstream-rust-fixture/.proven/coords.json +4055a566fa17f4118869ff50bc6d6747090ea3d880bab5c9285554e23f25f4da downstream-rust-fixture/Cargo.toml +f10145063aded7fa962e5b370c970c2f8fc20a05098bd8cc6fbf73396b511428 downstream-rust-fixture/README.adoc +37ad6c9715f1ce8d6b9003cbea79b9c22d7f3bbd17ec2bbbbe79a5e3f613d18e downstream-rust-fixture/src/lib.rs +b30268fff707ade4a74715369c0c513022b74b786ec57cc52394789a4fc8e66e downstream-rust-fixture/tests/fixtures/empty_slice.txt +f5451eb32e96919c1a592a59b2b188cde2daf0995a0fd9cbb90438e1eb44a0b3 downstream-rust-fixture/tests/fixtures/inverted_pair.txt +3832f6b61a76a9c16b3cd64b2be92b90247a31b87d42dd8eb28a2fabd7348544 downstream-rust-fixture/tests/fixtures/sorted_pair.txt +d5afc0384e3f3d5a5079a9a8ab5b1fa5360b3e74ab207b186ca861f2bbdd9d3d downstream-rust-fixture/tests/fixtures/unstable_pair.txt +5ff1b1077a24557f31d9fe6d4aef87374e7a7c6a5b24b24098058b5f9897ce8b downstream-rust-fixture/tests/ordering.rs +171ea744f972b01220a7b74b4d8363414431b7dd99a130bfcd976befe484a9fb fixtures/coords/ordering.json +b908f20595fe3e10c2ee2faf336d1d9c59c41cac012ece39d3bcf4904275d185 fixtures/coords/partial.json +b5c01faf57da980747a1cc2f2b7e9cc17b6388e828bd64df21f57242fad00ca2 fixtures/expectations.json +7b7ab6714a7e5c145611c4225aee0d7b1f7d799bdb38435ed3cbf489b93bf4e7 fixtures/invalid/actually-proven-from-example.json +1da0a1e4062161e2a25548572022d55a1c16ec37240f5d83f47434249fe291db fixtures/invalid/counts-lie.json +5a4432285a09deff59583c1cb79b65de6e49df633744ca8abcada2643b39fe2b fixtures/invalid/coverage-inflated.json +fbf057be8c225425d97bf8ec5ed289f26e385f3a82a4533694282695ab663b80 fixtures/invalid/duplicate-ids.json +32d39f1f212ef64d66f64b05acb97f96dc07a10c0fe01498ef36d839b69c1b46 fixtures/invalid/failing-test-claims-green.json +bca4594736155a6b62ee8ebfd989e5df7e4671fdb47e36a59005ebb90cc399c6 fixtures/invalid/future-major.json +1f529937307dd55578505e09ff4c3ca83bfbf7a5c324c5038918b588a14d8800 fixtures/invalid/no-fixtures.json +843eef6791b0c278dd496e96ada9681e4e9186fec1df73c64a452c3fad365e83 fixtures/invalid/noop-command.json +8c8abbac3301b64144ab0cea03caeeb8873bdc4928a275a05e287efb762a3361 fixtures/invalid/pass-no-output-digest.json +073c8efab10be46a26c203b77b9c4ae4dd36a28ad7bca13744d8cd20c6ebe1cc fixtures/invalid/pass-nonzero-exit.json +cc8e9119e8aa4aac808d477579e54c6da4c647aaadfb65212c9f84784a00bf98 fixtures/invalid/pass-without-execution.json +4808e2589ff7f5727537ae43590dd2d0ecc5b790734a3361cef762f54592be10 fixtures/invalid/proof-no-rungs.json +f99605db13afb730acbd531b99fd9e17ae140e7e163ad2d09bd34632183a3f6c fixtures/invalid/proof-not-checked.json +aab3cc431c04cf300c1ec74867898ace96b1c7d7d067599b55c89116dfb9eff7 fixtures/invalid/property-no-shrinker.json +d77466854f8aad1012c3decdeb60c5a59bc6dc41d17349b37fdd42ae6075a3bf fixtures/invalid/property-zero-cases.json +72a257c17201e375998a88b07529010ec15a0bb3e02749da774e3fc2798721a9 fixtures/invalid/run-consistency.json +df2fc844fadc720e797bbcbba5828a686a5c4392e470ff9ee86cd37da70064aa fixtures/invalid/skip-counted-as-pass.json +c7cf7cf5f4d72276be9a6de8d6d73ca7008796bfddbab38bdc9773f240085b7a fixtures/invalid/skip-unlabelled.json +f46ba9bbcf987d80ef8ec55c7b7ba20e2dbaf8b5d9aaac37145bfec9012ee361 fixtures/invalid/stale-commit.json +074e656f79ab80879af10db950ec52a18c6affdba9bca5750936152ab31a99af fixtures/invalid/timestamps-inverted.json +6f8b7a2dca7f353c1e69cd70ef4e311d16231e55798b23794795a301d7a23881 fixtures/invalid/unknown-coordinate.json +7bc100f3f5715012d7e882cb113cb1a8a0467f7435b78202ecf25f36f6c6b5a9 fixtures/libtest/clean.txt +d515d985269bd24e5564f06956461ad108932a096d25b9142489e2ee5156c44d fixtures/libtest/empty.txt +72d6942c109be388486789543058de3710486ea940d6ce2cfc01caf4a52cf5c3 fixtures/libtest/summary-mismatch.txt +09d4eacff14b77b4867963029838fac85b3c1c44ad9b43edbc62cbb02813ee09 fixtures/libtest/with-failure.txt +c0805114be00589069359fbb128c307469ba9af7a20aa3c93d1ce3dccb7d280d fixtures/libtest/with-ignored.txt +a43bab816a7410649f04af2f745f389b5a1a849c2c11129b8eea5fca223f5a81 fixtures/valid/debt-excluded.json +323b5ac13f8713e1dd79509ad5a7022078ea88b9a6f14cba5fa19b646f083335 fixtures/valid/property-and-proof.json +f0f8d8c47d1cb8dcd091a0a82fe527b42c65d320b44b17614e595ef862fb169d fixtures/valid/rust-example-pass.json +bf52b1cdff2caee80be8e2c7d44fdde225c7867551a1e6fd1ab6c69f922a599c schema/coords-v1.schema.json +e8e1d83228852998fd9642addc2f9499654db4bc7cf50d193094d2dde5bd0943 schema/evidence-v1.schema.json +dee6ee7ff9b199914af6fb8552a78dec5b726087dde48d77a1c9dee04be4f334 taxonomy-v1.json +6ce9fce0519e3b45eb16ddae4be9c16a40ca02c5251ef206f400ace63bd44ca2 tests/run-conformance.sh diff --git a/contracts/proven-tests/bin/collect-evidence.sh b/contracts/proven-tests/bin/collect-evidence.sh new file mode 100755 index 0000000..41fa0f6 --- /dev/null +++ b/contracts/proven-tests/bin/collect-evidence.sh @@ -0,0 +1,255 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# collect-evidence.sh — turn ONE captured `cargo test` run into a +# proven-tests-evidence/1.0.0 submission. +# +# just cargo-test 2>&1 | tee test.log +# collect-evidence.sh \ +# --repo "$GITHUB_REPOSITORY" --commit "$GITHUB_SHA" \ +# --log test.log --exit-code "$cargo_exit" \ +# --command-argv '["cargo","test","--","--test-threads=1"]' \ +# --started-at 2026-10-25T10:00:00Z --finished-at 2026-10-25T10:00:31Z \ +# --runner ubuntu-24.04 --rust 1.85.0 \ +# --coords .proven/coords.json > evidence.json +# +# The collector is the *reference* producer, not the gate: verify-evidence is +# the gate. What this script refuses, it refuses loudly rather than guessing: +# +# * a log whose libtest summary disagrees with the per-test lines; +# * a log with no per-test lines at all (an empty run is not evidence); +# * a run whose exit code disagrees with the failures in the log; +# * a test the coordinates file does not map — an unmapped test gets no +# coordinate, because a coordinate invented here would be a fabricated cell. +# +# Exit codes: 0 evidence written, 3 the log or the coordinates are inconsistent +# (nothing is written), 2 usage or environment failure. +# +# Contract revision: proven-tests-evidence/1.0.0. + +set -euo pipefail + +readonly EXIT_OK=0 +readonly EXIT_REFUSED=3 +readonly EXIT_USAGE=2 +readonly COLLECTOR_VERSION="1.0.0" + +usage() { + cat >&2 <<'USAGE' +usage: collect-evidence.sh --repo OWNER/NAME --commit <40-hex> --log FILE + --exit-code N --coords FILE + --started-at ISO --finished-at ISO + (--command-argv '["cargo","test"]' | --command "cargo test") + [--runner NAME] [--rust VERSION] [--idris2 VERSION] + [--out FILE] + ISO is YYYY-MM-DDTHH:MM:SSZ (UTC, seconds). Both are required: an invented + timestamp would be an invented execution. +USAGE +} + +die() { + printf 'collect-evidence: %s\n' "$*" >&2 + exit "$EXIT_USAGE" +} + +refuse() { + printf 'collect-evidence: refused — %s\n' "$*" >&2 + exit "$EXIT_REFUSED" +} + +main() { + local repo="" commit="" log="" exit_code="" coords="" started="" finished="" + local command="" command_argv="" runner="" rust="" idris2="" out="" + + while [[ $# -gt 0 ]]; do + case "$1" in + --repo) [[ $# -ge 2 ]] || die "--repo needs a value"; repo="$2"; shift 2 ;; + --commit) [[ $# -ge 2 ]] || die "--commit needs a value"; commit="$2"; shift 2 ;; + --log) [[ $# -ge 2 ]] || die "--log needs a value"; log="$2"; shift 2 ;; + --exit-code) [[ $# -ge 2 ]] || die "--exit-code needs a value"; exit_code="$2"; shift 2 ;; + --coords) [[ $# -ge 2 ]] || die "--coords needs a value"; coords="$2"; shift 2 ;; + --started-at) [[ $# -ge 2 ]] || die "--started-at needs a value"; started="$2"; shift 2 ;; + --finished-at) [[ $# -ge 2 ]] || die "--finished-at needs a value"; finished="$2"; shift 2 ;; + --command) [[ $# -ge 2 ]] || die "--command needs a value"; command="$2"; shift 2 ;; + --command-argv) [[ $# -ge 2 ]] || die "--command-argv needs a value"; command_argv="$2"; shift 2 ;; + --runner) [[ $# -ge 2 ]] || die "--runner needs a value"; runner="$2"; shift 2 ;; + --rust) [[ $# -ge 2 ]] || die "--rust needs a value"; rust="$2"; shift 2 ;; + --idris2) [[ $# -ge 2 ]] || die "--idris2 needs a value"; idris2="$2"; shift 2 ;; + --out) [[ $# -ge 2 ]] || die "--out needs a value"; out="$2"; shift 2 ;; + -h|--help) usage; exit 0 ;; + *) usage; die "unknown argument: $1" ;; + esac + done + + for required in repo commit log exit_code coords started finished; do + [[ -n "${!required}" ]] || { usage; die "missing --${required//_/-}"; } + done + [[ "$repo" =~ ^[^/[:space:]]+/[^/[:space:]]+$ ]] || die "--repo must be OWNER/NAME" + [[ "$commit" =~ ^[0-9a-f]{40}$ ]] || die "--commit must be 40 lowercase hex characters" + [[ "$exit_code" =~ ^[0-9]+$ ]] || die "--exit-code must be a number" + local iso_re='^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}Z$' + [[ "$started" =~ $iso_re ]] || die "--started-at must be YYYY-MM-DDTHH:MM:SSZ" + [[ "$finished" =~ $iso_re ]] || die "--finished-at must be YYYY-MM-DDTHH:MM:SSZ" + [[ -r "$log" ]] || die "cannot read $log" + [[ -r "$coords" ]] || die "cannot read $coords" + command -v jq >/dev/null 2>&1 || die "jq (1.6 or later) is required" + jq -e . "$coords" >/dev/null 2>&1 || die "$coords is not valid JSON" + if [[ -n "$command_argv" ]]; then + jq -e 'type == "array" and length > 0 and all(.[]; type == "string")' <<<"$command_argv" >/dev/null 2>&1 \ + || die "--command-argv must be a non-empty JSON array of strings" + elif [[ -n "$command" ]]; then + # Whitespace splitting: documented limitation. Use --command-argv when an + # argument contains a space. + command_argv="$(jq -R -s 'split("[[:space:]]+"; "g") | map(select(length > 0))' <<<"$command")" + else + die "one of --command-argv or --command is required" + fi + + # ── parse libtest ─────────────────────────────────────────────────────── + local parsed summary + parsed="$(awk '/^test .* \.\.\. (ok|FAILED|ignored)$/ { + name = $0 + sub(/^test /, "", name); sub(/ \.\.\. .*$/, "", name) + outcome = $0; sub(/^.* \.\.\. /, "", outcome) + printf "%s\t%s\t%d\n", name, outcome, NR + }' "$log")" + [[ -n "$parsed" ]] || refuse "no per-test lines in $log: a run that executed nothing is not evidence" + + summary="$(grep -E '^test result: ' "$log" | tail -n 1 || true)" + [[ -n "$summary" ]] || refuse "no libtest summary line ('test result: ...') in $log" + + local s_passed s_failed s_ignored + s_passed="$(sed -nE 's/^test result: (ok|FAILED)\. ([0-9]+) passed; ([0-9]+) failed; ([0-9]+) ignored.*/\2/p' <<<"$summary")" + s_failed="$(sed -nE 's/^test result: (ok|FAILED)\. ([0-9]+) passed; ([0-9]+) failed; ([0-9]+) ignored.*/\3/p' <<<"$summary")" + s_ignored="$(sed -nE 's/^test result: (ok|FAILED)\. ([0-9]+) passed; ([0-9]+) failed; ([0-9]+) ignored.*/\4/p' <<<"$summary")" + [[ -n "$s_passed" && -n "$s_failed" && -n "$s_ignored" ]] || refuse "cannot read the counts from '$summary'" + + local p_passed p_failed p_ignored + p_passed="$(awk -F'\t' '$2 == "ok"' <<<"$parsed" | wc -l | tr -d ' ')" + p_failed="$(awk -F'\t' '$2 == "FAILED"' <<<"$parsed" | wc -l | tr -d ' ')" + p_ignored="$(awk -F'\t' '$2 == "ignored"' <<<"$parsed" | wc -l | tr -d ' ')" + + if [[ "$s_passed" != "$p_passed" || "$s_failed" != "$p_failed" || "$s_ignored" != "$p_ignored" ]]; then + refuse "the summary says ${s_passed} passed/${s_failed} failed/${s_ignored} ignored, the per-test lines say ${p_passed}/${p_failed}/${p_ignored}" + fi + if [[ "$exit_code" != "0" && "$p_failed" == "0" ]]; then + refuse "exit code ${exit_code} with no failing test: the harness failed outside the tests, so this run evidences nothing about the suite" + fi + if [[ "$exit_code" == "0" && "$p_failed" != "0" ]]; then + refuse "exit code 0 with ${p_failed} failing test(s): the log and the exit code disagree" + fi + if [[ "$started" > "$finished" ]]; then + refuse "--finished-at precedes --started-at" + fi + + local digest logname + digest="$( (command -v sha256sum >/dev/null 2>&1 && sha256sum -- "$log") || shasum -a 256 -- "$log")" + digest="${digest%% *}" + logname="$(basename "$log")" + + local parsed_json + parsed_json="$(jq -R -s 'split("\n") | map(select(length > 0) | split("\t") | { name: .[0], outcome: .[1], line: (.[2] | tonumber) })' <<<"$parsed")" + + # ── assemble ──────────────────────────────────────────────────────────── + local doc + doc="$(jq -n \ + --argjson parsed "$parsed_json" \ + --slurpfile coords "$coords" \ + --arg repo "$repo" --arg commit "$commit" \ + --argjson exit_code "$exit_code" \ + --argjson argv "$command_argv" \ + --arg started "$started" --arg finished "$finished" \ + --arg digest "sha256:${digest}" --arg logname "$logname" \ + --arg runner "$runner" --arg rust "$rust" --arg idris2 "$idris2" \ + --arg version "$COLLECTOR_VERSION" ' + def dur_ms: (((($finished | fromdateiso8601) - ($started | fromdateiso8601)) * 1000) | floor); + def result_of($o): if $o == "ok" then "passed" elif $o == "FAILED" then "failed" else "skipped" end; + ( $coords[0].tests // {} ) as $map + | [ $parsed[] + | . as $p + | ($map[$p.name] // null) as $c + | if $c == null then { unmapped: $p.name } + else + { id: $p.name, + kind: $c.kind, + coord: $c.coord, + result: result_of($p.outcome), + execution: { + ran: ($p.outcome != "ignored"), + command: $argv, + runner: (if $runner == "" then null else $runner end), + started_at: $started, + finished_at: $finished, + duration_ms: dur_ms, + # Per-test attributed status, not the aggregate: a passing test + # inside a failing run was still a passing test. The aggregate is + # `run.exit_code` below, and the gate checks the two agree. + exit_code: (if $p.outcome == "ok" then 0 elif $p.outcome == "FAILED" then 1 else null end), + observed_output_digest: $digest + }, + claim: $c.claim, + evidence: ($c.evidence // {}), + fixtures: ($c.fixtures // null), + anchor: { log: $logname, line: $p.line } + } + + (if result_of($p.outcome) == "failed" + then { detail: ("libtest reported FAILED for this test; the captured log at line " + ($p.line | tostring) + " is the record") } + else {} end) + + (if result_of($p.outcome) == "skipped" + then { skip_reason: "libtest: the test carries #[ignore]; it did not run, so it evidences nothing" } + else {} end) + end ] as $rows + | ( [ $rows[] | select(.unmapped?) | .unmapped ] ) as $unmapped + | ( [ $rows[] | select(.unmapped? | not) ] ) as $tests + | { contract: { name: "hyperpolymath/proven-tests/evidence", revision: "1.0.0", major: 1 }, + subject: { repo: $repo, commit: $commit, + producer: { tool: "proven-tests collect-evidence", version: $version } }, + toolchain: { runner: (if $runner == "" then null else $runner end), + rust: (if $rust == "" then null else $rust end), + idris2: (if $idris2 == "" then null else $idris2 end) }, + taxonomy: { revision: "proven-tests/taxonomy/1", cells: 238 }, + run: { + command: $argv, + runner: (if $runner == "" then null else $runner end), + started_at: $started, + finished_at: $finished, + duration_ms: dur_ms, + exit_code: $exit_code, + observed_output_digest: $digest + }, + tests: $tests, + counts: { + records: ($tests | length), + executed: ([ $tests[] | select(.execution.ran) ] | length), + passed: ([ $tests[] | select(.result == "passed") ] | length), + failed: ([ $tests[] | select(.result == "failed") ] | length), + error: ([ $tests[] | select(.result == "error") ] | length), + skipped: ([ $tests[] | select(.result == "skipped") ] | length), + not_run: ([ $tests[] | select(.result == "not_run") ] | length), + excluded_debt: ([ $tests[] | select((.fixtures.debt_ref? // "") != "") ] | length) + }, + _unmapped: $unmapped } + ')" || die "could not assemble the submission (check --command-argv and the coords file)" + + local unmapped + unmapped="$(jq -r '._unmapped[]?' <<<"$doc")" + if [[ -n "$unmapped" ]]; then + printf 'collect-evidence: refused — these executed tests have no coordinate in %s:\n' "$coords" >&2 + printf ' %s\n' $unmapped >&2 + printf 'A coordinate invented by this script would be a fabricated cell. Map them, or do not submit.\n' >&2 + exit "$EXIT_REFUSED" + fi + + doc="$(jq 'del(._unmapped)' <<<"$doc")" + if [[ -n "$out" ]]; then + printf '%s\n' "$doc" > "$out" + printf 'collect-evidence: wrote %s (%s tests, %s executed)\n' \ + "$out" "$(jq -r '.counts.records' <<<"$doc")" "$(jq -r '.counts.executed' <<<"$doc")" >&2 + else + printf '%s\n' "$doc" + fi + exit "$EXIT_OK" +} + +main "$@" diff --git a/contracts/proven-tests/bin/verify-evidence b/contracts/proven-tests/bin/verify-evidence new file mode 100755 index 0000000..0c67d80 --- /dev/null +++ b/contracts/proven-tests/bin/verify-evidence @@ -0,0 +1,433 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# verify-evidence — admit, refuse and derive coverage for a Proven-Tests evidence +# submission. This is the normative implementation of +# proven-tests-evidence/1.0.0 (see ../EVIDENCE-CONTRACT.adoc). +# +# verify-evidence evidence.json +# verify-evidence --expect-commit "$GITHUB_SHA" --expect-repo "$GITHUB_REPOSITORY" \ +# --require-green evidence.json +# +# Writes ONE JSON document to stdout; the optional coverage grid goes to stderr. +# +# exit 0 admissible. With --require-green, also green: nothing failed, nothing +# was skipped or not run, and at least one test actually executed and +# passed. +# exit 3 refused: at least one rule failed, or --require-green was asked for +# and the evidence is not green. A finding, never a pass. +# exit 2 the tool could not do its job (usage, unreadable file, invalid JSON, +# missing jq). +# +# What it will not do: infer that a test ran. A `passed` record without an +# execution record, timestamps, an exit code and a captured-output digest is a +# finding (R1), and coverage counts only records that pass R1. A skipped record +# is never a pass (R2). A proof claim needs a checker that ran and at least one +# witnessed rung (R3). A coverage claim that outruns the derivation is refused +# (R4). Debt-marked records are excluded from coverage entirely, as the +# doctrine's B.4 requires (R10). + +set -euo pipefail + +readonly CONTRACT="proven-tests-evidence/1.0.0" +readonly CONTRACT_NAME="hyperpolymath/proven-tests/evidence" +readonly CONTRACT_MAJOR=1 +readonly EXIT_ADMISSIBLE=0 +readonly EXIT_REFUSED=3 +readonly EXIT_USAGE=2 + +SELF_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +readonly SELF_DIR +readonly TAXONOMY="${SELF_DIR}/../taxonomy-v1.json" + +usage() { + printf 'usage: verify-evidence [--expect-commit SHA] [--expect-repo OWNER/NAME]\n' >&2 + printf ' [--require-green] [--grid] FILE|-\n' >&2 +} + +die() { + printf 'verify-evidence: %s\n' "$*" >&2 + exit "$EXIT_USAGE" +} + +read -r -d '' JQ_PROGRAM <<'JQ' || true +def nonempty: type == "string" and (length > 0); +def hex40: type == "string" and test("^[0-9a-f]{40}$"); +def slug: type == "string" and test("^[^/[:space:]]+/[^/[:space:]]+$"); +def iso: type == "string" and test("^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}Z$"); +def sha256: type == "string" and test("^sha256:[0-9a-f]{64}$"); +def int: type == "number" and . == floor; + +def noop_argv0: ["true", "false", ":", "echo", "printf", "sleep", "cat", "head", "tail", "yes"]; + +def finding($rule; $id; $msg): { rule: $rule, test: $id, message: $msg }; + +# is_debt: the record declares a fixture debt. Debt-marked tests are not counted +# in any ledger (TEST-DOCTRINE B.4), so they cover nothing. +def is_debt: ((.fixtures.debt_ref? // null) | nonempty); + +# pass_ok: a PASS that is actually backed by an execution. Coverage is derived +# from this predicate only, so a forged pass is inadmissible AND covers nothing. +def pass_ok: + [ (.result == "passed"), + ((.execution.ran? // false) == true), + ((.execution.exit_code? // null) == 0), + (((.execution.command? // []) | type) == "array"), + (((.execution.command? // []) | length) > 0), + (((.execution.command? // [])[0] // "") as $c0 | (noop_argv0 | index($c0)) == null), + ((.execution.started_at? // "") | iso), + ((.execution.finished_at? // "") | iso), + ((.execution.started_at? // "") <= (.execution.finished_at? // "")), + (((.execution.duration_ms? // -1) | int) and ((.execution.duration_ms? // -1) >= 0)), + ((.execution.observed_output_digest? // "") | sha256) + ] | all; + +def coord_known($tax): (.coord? // null) as $c + | ($c | type) == "object" + and (($tax.categories | index($c.category)) != null) + and (($tax.aspects | index($c.aspect)) != null); + +def coord_key: (.category | tostring) + "/" + (.aspect | tostring); + +def check_test($tax): + . as $t + | ($t.id? // "") as $id + | ($t.result? // "") as $res + | ($t.kind? // "") as $kind + | ($t.claim? // "") as $claim + | ($t.evidence? // {}) as $ev + | ($t.fixtures? // null) as $fx + | [ + if (($t | type) != "object") then finding("R0-shape"; "-"; "a test record is not an object") + elif ($id | nonempty | not) then finding("R0-shape"; "-"; "a test record has no id") + else empty end, + if ($id | nonempty) then + (if (["example", "property", "proof"] | index($kind)) == null + then finding("R3-kind-honesty"; $id; "kind is \"" + ($kind | tostring) + "\", not example|property|proof") else empty end), + (if ($tax.categories | index($t.coord.category)) == null + then finding("R4-coord-unknown"; $id; "category \"" + (($t.coord.category // "") | tostring) + "\" is not in taxonomy " + $tax.contract) else empty end), + (if ($tax.aspects | index($t.coord.aspect)) == null + then finding("R4-coord-unknown"; $id; "aspect \"" + (($t.coord.aspect // "") | tostring) + "\" is not in taxonomy " + $tax.contract) else empty end), + (if (["passed", "failed", "error", "skipped", "not_run"] | index($res)) == null + then finding("R2-result-unknown"; $id; "result is \"" + ($res | tostring) + "\", not passed|failed|error|skipped|not_run") else empty end), + (if (["unproven", "provisionally_proven", "actually_proven"] | index($claim)) == null + then finding("R3-tier-evidence"; $id; "claim is \"" + ($claim | tostring) + "\", not unproven|provisionally_proven|actually_proven") else empty end) + else empty end, + + # ── R1: a pass is a run ───────────────────────────────────────────── + if ($res == "passed") then + (if ((.execution.ran? // false) != true) + then finding("R1-executed-pass"; $id; "claimed passed with execution.ran != true: a claim is not a run") else empty end), + (if ((.execution.exit_code? // null) != 0) + then finding("R1-executed-pass"; $id; "claimed passed with execution.exit_code " + ((.execution.exit_code? // "absent") | tostring)) else empty end), + (if (((.execution.command? // []) | length) == 0) + then finding("R1-executed-pass"; $id; "claimed passed with no command recorded") else empty end), + (if (((.execution.command? // [])[0] // "") as $c0 | (noop_argv0 | index($c0)) != null) + then finding("R1-executed-pass"; $id; "command[0] is \"" + (.execution.command[0]) + "\", a no-op: it cannot produce a passing test") else empty end), + (if (((.execution.started_at? // "") | iso) | not) + then finding("R1-executed-pass"; $id; "claimed passed without a valid UTC started_at (YYYY-MM-DDTHH:MM:SSZ)") else empty end), + (if (((.execution.finished_at? // "") | iso) | not) + then finding("R1-executed-pass"; $id; "claimed passed without a valid UTC finished_at (YYYY-MM-DDTHH:MM:SSZ)") else empty end), + (if (((.execution.started_at? // "") | iso) and ((.execution.finished_at? // "") | iso)) then + (if ((.execution.finished_at? // "") < (.execution.started_at? // "")) + then finding("R1-executed-pass"; $id; "finished_at precedes started_at") else empty end) + else empty end), + (if ((((.execution.duration_ms? // -1) | int) | not)) + then finding("R1-executed-pass"; $id; "claimed passed without an integer duration_ms") else empty end), + (if (((.execution.observed_output_digest? // "") | sha256) | not) + then finding("R1-executed-pass"; $id; "claimed passed with no sha256 digest of the output it produced; an executed test leaves a log") else empty end) + else empty end, + + # ── R2: not-run is not a pass, and a non-pass establishes no warrant ─ + if ($id | nonempty) and ($res != "passed") and ($claim != "unproven") + then finding("R2-not-run-is-not-a-pass"; $id; "claim is " + ($claim | tostring) + " but result is " + ($res | tostring) + "; a record that did not pass in this submission establishes no warrant") else empty end, + if (($res == "skipped") or ($res == "not_run")) and (($t.skip_reason? // "") | nonempty | not) + then finding("R5-labelled-skips"; $id; "result " + $res + " without a skip_reason: an unlabelled skip reads as a pass") else empty end, + if (($res == "failed") or ($res == "error")) and (($t.detail? // "") | nonempty | not) + then finding("R5-labelled-skips"; $id; "result " + $res + " without a detail saying what went wrong") else empty end, + + # ── R3: the kind must match the evidence, and the tier its evidence ─ + if ($id | nonempty) then + (if ($kind == "example" and (($ev.proof? // null) != null or ($ev.property? // null) != null)) + then finding("R3-kind-honesty"; $id; "an example carries a property or proof block") else empty end), + (if ($kind == "property") then + (if (($ev.property? | type) != "object") + then finding("R3-kind-honesty"; $id; "kind=property with no property block") else + (if (($ev.property.generator? // "") | nonempty | not) + then finding("R3-kind-honesty"; $id; "property has no generator") else empty end), + (if (((($ev.property.cases_run? // 0) | int) | not) or (($ev.property.cases_run? // 0) < 1)) + then finding("R3-kind-honesty"; $id; "property ran " + (($ev.property.cases_run? // 0) | tostring) + " cases; zero cases is a runner fault, not evidence") else empty end), + (if (($ev.property.shrinker? // false) != true) + then finding("R3-kind-honesty"; $id; "property declares no shrinker: a failing case could not have been minimised") else empty end), + (if ($res == "passed" and (($ev.property.failures? // -1) != 0)) + then finding("R3-kind-honesty"; $id; "property passed with failures=" + (($ev.property.failures? // -1) | tostring)) else empty end) + end) else empty end), + (if ($kind == "proof") then + (if (($ev.proof? | type) != "object") + then finding("R3-kind-honesty"; $id; "kind=proof with no proof block") else + (if (($ev.proof.checked? // false) != true) + then finding("R3-kind-honesty"; $id; "the proof was not checked in this run (proof.checked != true)") else empty end), + (if ((($ev.proof.checker.name? // "") | nonempty | not) or (($ev.proof.checker.version? // "") | nonempty | not)) + then finding("R3-kind-honesty"; $id; "proof names no checker and version; an unchecked citation is a label") else empty end), + (if ((($ev.proof.theorems? // []) | length) < 1) + then finding("R3-kind-honesty"; $id; "actually_proven needs a non-empty ladder of witnessed rungs (List1 Witnessed); this proof names none") else empty end), + (if (([ ($ev.proof.theorems? // [])[] + | select(((.name? // "") | nonempty | not) + or ((.statement? // "") | nonempty | not) + or ((.term_digest? // "") | sha256 | not) + or ((.file? // "") | nonempty | not) + or (((.line? // 0) | int | not)) + or ((.line? // 0) < 1)) ] | length) > 0) + then finding("R3-kind-honesty"; $id; "a theorem rung is missing name, statement, term_digest (sha256), file or line") else empty end), + (if ($claim != "actually_proven") + then finding("R3-kind-honesty"; $id; "a checked proof must be claimed actually_proven, not " + ($claim | tostring)) else empty end) + end) else empty end), + (if ($kind != "proof" and $claim == "actually_proven") + then finding("R3-kind-honesty"; $id; "actually_proven requires kind=proof; " + $kind + " is sampling or example evidence") else empty end), + (if (($claim == "provisionally_proven") or ($claim == "actually_proven")) and (($ev.type_safety? | type) != "object") + then finding("R3-tier-evidence"; $id; "claim " + $claim + " requires a type_safety certificate (kategoria_level, type_system, verified_by)") else empty end), + (if (($ev.type_safety? | type) == "object" and (((($ev.type_safety.kategoria_level? // 0) | int) | not) or (($ev.type_safety.kategoria_level? // 0) < 1) or (($ev.type_safety.kategoria_level? // 0) > 12))) + then finding("R3-tier-evidence"; $id; "type_safety.kategoria_level must be 1..12") else empty end), + (if ($claim == "provisionally_proven" and (($ev.framework_safety? // "") | nonempty | not)) + then finding("R3-tier-evidence"; $id; "provisionally_proven requires framework_safety naming the certificate relied on") else empty end), + (if ($claim == "actually_proven" and (($ev.proof.design_proof.technique? // "") | nonempty | not)) + then finding("R3-tier-evidence"; $id; "actually_proven requires a design_proof (technique, limitations)") else empty end), + + # ── R10: the fixture obligation ──────────────────────────────────── + (if ($fx | type) != "object" + then finding("R10-fixtures"; $id; "no fixtures block: every test must state its fixture position (silence+firing, cannot_fail_by_design, or debt_ref)") else + (if (($fx.silence? | type) == "object" and ($fx.firing? | type) == "object") then + (if (($fx.silence.description? // "") | nonempty | not) + then finding("R10-fixtures"; $id; "the silence fixture does not say why it is clean") else empty end), + (if (($fx.firing.defect_class? // "") | nonempty | not) + then finding("R10-fixtures"; $id; "the firing fixture names no defect class") else empty end) + elif (($fx.cannot_fail_by_design? // "") | nonempty) then empty + elif (($fx.debt_ref? // "") | nonempty) then empty + else finding("R10-fixtures"; $id; "fixture position is neither a silence+firing pair, cannot_fail_by_design, nor a debt_ref") end) + end) + else empty end + ]; + +def run_findings($run; $tests): + if ($run | type) != "object" then [] + else + [ (if (((($run.command? // []) | length) == 0) or ((($run.command? // []) | type) != "array")) + then finding("R11-run-consistency"; "-"; "run.command is not a non-empty argv array") else empty end), + (if ((($run.exit_code? // null) | int) | not) + then finding("R11-run-consistency"; "-"; "run.exit_code is not an integer") else empty end), + (if ((($run.observed_output_digest? // "") | sha256) | not) + then finding("R11-run-consistency"; "-"; "run has no sha256 digest of the output the whole invocation produced") else empty end), + (if ((($run.exit_code? // null) | int) and (([ $tests[] | select(.result? == "failed" or .result? == "error") ] | length) == 0) and $run.exit_code != 0) + then finding("R11-run-consistency"; "-"; "run.exit_code is " + ($run.exit_code | tostring) + " with no failing or errored record: the harness failed outside the tests, so this run evidences nothing about the suite") else empty end), + (if ((($run.exit_code? // null) | int) and $run.exit_code == 0 and (([ $tests[] | select(.result? == "failed" or .result? == "error") ] | length) > 0)) + then finding("R11-run-consistency"; "-"; "run.exit_code is 0 but a record failed or errored: the log and the exit code disagree") else empty end), + ( $tests[] | select((.execution.observed_output_digest? // "") != ($run.observed_output_digest? // "")) + | finding("R11-run-consistency"; (.id? // "-"); "this record cites a different captured-output digest than the run it is part of") ) + ] + end; + +(if length != 1 then error("expected exactly one JSON document") else .[0] end) as $doc +| (if ($doc | type) != "object" then [] else ($doc.tests? // []) end) as $tests +| ($taxonomy) as $tax + +# ── R7: the contract itself ──────────────────────────────────────────────── +| (if ($doc | type) != "object" + then [finding("R0-shape"; "-"; "the submission is not a JSON object")] + elif (($doc.contract? | type) != "object" + or $doc.contract.name != "hyperpolymath/proven-tests/evidence" + or (($doc.contract.major? // null) != 1) + or (($doc.contract.revision? // "") | nonempty | not)) + then [finding("R7-contract-version"; "-"; "contract is not " + $name + " major " + ($major | tostring) + "; this revision cannot read it")] + else [] end) as $contract_findings + +# ── R6: the subject is a commit, and it is the one asked for ────────────── +| (if ($doc | type) != "object" then [] else + (if (($doc.subject.commit? // "") | hex40 | not) + then [finding("R6-subject-binding"; "-"; "subject.commit is not a 40-hex commit; evidence that names no commit can be replayed")] + elif (($doc.subject.repo? // "") | slug | not) + then [finding("R6-subject-binding"; "-"; "subject.repo is not OWNER/NAME")] + elif ($expect_commit != "" and $doc.subject.commit != $expect_commit) + then [finding("R6-subject-binding"; "-"; "subject.commit is " + $doc.subject.commit + ", expected " + $expect_commit)] + elif ($expect_repo != "" and $doc.subject.repo != $expect_repo) + then [finding("R6-subject-binding"; "-"; "subject.repo is " + $doc.subject.repo + ", expected " + $expect_repo)] + else [] end) end) as $subject_findings + +# ── R8: ids are unique ───────────────────────────────────────────────────── +| ([ $tests[] | .id? // "" ] | group_by(.) | map(select(length > 1) | .[0])) as $dupes +| (if ($dupes | length) > 0 + then [ $dupes[] | finding("R8-duplicate-id"; .; "the same test id appears more than once") ] + else [] end) as $dupe_findings + +| ($doc.run? // null) as $run +| run_findings($run; $tests) as $run_findings +| ( [ $tests[] | { record: ., findings: ([ . | check_test($tax) ] | add // []) } ] ) as $analysed +| ( [ $tests[] | select(.result? == "failed") | select(((.execution.exit_code? // 0) == 0)) + | finding("R1-executed-pass"; (.id? // "-"); "recorded as failed but its execution exited 0: per-test status and outcome disagree") ] ) as $failed_status_findings +| ( [ $analysed[] | .findings[] ] ) as $test_findings + +# ── R4: coverage is derived, never accepted ─────────────────────────────── +# A cell is covered only by a record that is itself free of findings: a record +# whose claim is bogus must not cover its coordinate, or an inadmissible +# submission would still paint the map. +| ([ $analysed[] | select((.findings | length) == 0) | .record + | select(pass_ok) | select(is_debt | not) | select(coord_known($tax)) | .coord ] + | unique_by(coord_key)) as $derived +| ([ $analysed[] | select((.findings | length) == 0) | .record | select(pass_ok) ] | length) as $passed_backed +| (($doc.coverage_claim? // null)) as $claim +| (if ($claim | type) != "object" then [] + else + [ (if ((($claim.cells_covered? // -1) | int | not) or (($claim.cells_covered? // -1) != ($derived | length))) + then finding("R4-coverage-claim"; "-"; "claims " + (($claim.cells_covered? // "absent") | tostring) + " covered cells; the derivation gives " + ($derived | length | tostring) + " from executed, passing, non-debt records") else empty end), + (if ((($claim.tests_passed? // -1) | int | not) or (($claim.tests_passed? // -1) != $passed_backed)) + then finding("R4-coverage-claim"; "-"; "claims " + (($claim.tests_passed? // "absent") | tostring) + " passing tests; " + ($passed_backed | tostring) + " record(s) are backed by an execution") else empty end), + ( [ (($claim.coords? // []) | map(if type == "object" then coord_key else tostring end) | unique) - [ $derived[] | coord_key ] ][] + | finding("R4-coverage-claim"; "-"; "coverage is claimed for " + tostring + ", which the derivation does not support") ), + ( [ [ $derived[] | coord_key ] - (($claim.coords? // []) | map(if type == "object" then coord_key else tostring end) | unique) ][] + | finding("R4-coverage-claim"; "-"; "coverage omits " + tostring + ", which the derivation supports") ) + ] end) as $claim_findings + +# ── R9: the submitter's counts must reconcile ──────────────────────────── +| (def count_of($r): [ $tests[] | select(.result? == $r) ] | length; + { + records: ($tests | length), + executed: [ $tests[] | select((.execution.ran? // false) == true) ] | length, + passed: count_of("passed"), + failed: count_of("failed"), + error: count_of("error"), + skipped: count_of("skipped"), + not_run: count_of("not_run"), + excluded_debt: [ $tests[] | select(is_debt) ] | length + }) as $counts +| (if (($doc.counts? // null) | type) != "object" then [] + else [ $counts | to_entries[] + | select(($doc.counts[.key]? // null) != .value) + | finding("R9-counts-reconcile"; "-"; "counts." + .key + " is " + (($doc.counts[.key]? // "absent") | tostring) + ", derived " + (.value | tostring)) ] + end) as $count_findings + +| ( [ $tests[] | select((.execution.ran? // false) == true and .result == "passed") ] | length ) as $executed_passed +| ( $contract_findings + $subject_findings + $dupe_findings + $test_findings + $run_findings + + $failed_status_findings + $claim_findings + $count_findings + | unique_by(.rule + "|" + .test + "|" + .message) ) as $findings +| (($findings | length) == 0) as $admissible +| ( $admissible + and $counts.failed == 0 + and $counts.error == 0 + and $counts.skipped == 0 + and $counts.not_run == 0 + and $executed_passed > 0 ) as $green + +# ── the report ──────────────────────────────────────────────────────────── +| { contract: "proven-tests-evidence/1.0.0", + subject: (if ($doc | type) == "object" then ($doc.subject // null) else null end), + admissible: $admissible, + green: $green, + counts: $counts, + tiers: { + unproven: ([ $tests[] | select(.claim? == "unproven") ] | length), + provisionally_proven: ([ $tests[] | select(.claim? == "provisionally_proven") ] | length), + actually_proven: ([ $tests[] | select(.claim? == "actually_proven") ] | length) + }, + kinds: { + example: ([ $tests[] | select(.kind? == "example") ] | length), + property: ([ $tests[] | select(.kind? == "property") ] | length), + proof: ([ $tests[] | select(.kind? == "proof") ] | length) + }, + coverage: { + cells_covered: ($derived | length), + cells_total: $tax.cells, + coords: $derived, + by_category: ([ $derived[] | .category ] | group_by(.) | map({ key: .[0], value: length }) | from_entries) + }, + findings: $findings, + notes: ( + [ "coverage counts executed, passing, non-debt records at typed coordinates; it is never inferred from a missing record", + "coordinates and claims are declarations. This validator checks that a claim is backed by the evidence its tier requires, and that coverage is derived only from executed passes. It cannot check that a declared coordinate is the right one — that is review, and the silence/firing fixture pair is how a coordinate is audited." + ] + + (if $counts.excluded_debt > 0 + then [ ($counts.excluded_debt | tostring) + " record(s) are marked FixtureDebt and are excluded from coverage and from the test count (TEST-DOCTRINE B.4): debt-marked tests are not evidence" ] + else [] end) + + (if ($counts.skipped + $counts.not_run) > 0 + then [ ($counts.skipped + $counts.not_run | tostring) + " record(s) did not run; they contribute no coverage and no green, whatever their declared claim" ] + else [] end) + + (if ($counts.error > 0 + or $counts.failed > 0) + then [ "a failing or errored record is admissible evidence of failure — and it can never be part of a green submission" ] + else [] end) + + (if $counts.executed == 0 + then [ "no test executed; an empty run is not evidence, and it is never green" ] + else [] end) + ) } +JQ + +main() { + local expect_commit="" expect_repo="" require_green="false" grid="false" file="" + while [[ $# -gt 0 ]]; do + case "$1" in + --expect-commit) [[ $# -ge 2 ]] || { usage; die "--expect-commit needs a value"; }; expect_commit="$2"; shift 2 ;; + --expect-repo) [[ $# -ge 2 ]] || { usage; die "--expect-repo needs a value"; }; expect_repo="$2"; shift 2 ;; + --require-green) require_green="true"; shift ;; + --grid) grid="true"; shift ;; + -h|--help) usage; exit 0 ;; + --) shift; [[ $# -eq 1 ]] || { usage; die "one FILE only"; }; file="$1"; shift ;; + -) [[ -z "$file" ]] || { usage; die "one FILE only"; }; file="-"; shift ;; + -*) usage; die "unknown option: $1" ;; + *) [[ -z "$file" ]] || { usage; die "one FILE only"; }; file="$1"; shift ;; + esac + done + [[ -n "$file" ]] || { usage; die "missing FILE"; } + command -v jq >/dev/null 2>&1 || die "jq (1.6 or later) is required" + [[ -r "$TAXONOMY" ]] || die "cannot read $TAXONOMY" + if [[ "$file" != "-" && ! -r "$file" ]]; then + die "cannot read $file" + fi + local label="$file" + [[ "$file" == "-" ]] && label="stdin" + + local tax_json + tax_json="$(jq -c . "$TAXONOMY")" || die "taxonomy is not valid JSON" + + local out rc=0 + out="$(jq --slurp \ + --argjson taxonomy "$tax_json" \ + --arg name "$CONTRACT_NAME" \ + --argjson major "$CONTRACT_MAJOR" \ + --arg expect_commit "$expect_commit" \ + --arg expect_repo "$expect_repo" \ + "$JQ_PROGRAM" -- "$file" 2>/dev/null)" || rc=$? + if (( rc != 0 )); then + printf 'verify-evidence: %s is not a single valid JSON document\n' "$label" >&2 + exit "$EXIT_USAGE" + fi + + printf '%s\n' "$out" + + if [[ "$grid" == "true" ]]; then + printf '%s\n' "$out" | jq -r --argjson tax "$tax_json" ' + ($tax.categories) as $cats | ($tax.aspects) as $asp + | ([ .coverage.coords[] | .category + "/" + .aspect ]) as $cov + | "coverage grid (# = covered by an executed pass, . = no evidence)", + (" " * 19) + ([ $asp[] | .[0:2] ] | join(" ")), + ( $cats[] as $c + | (($c + (" " * 19))[0:18]) + + ([ $asp[] | if ($cov | index($c + "/" + .)) then "# " else ". " end ] | join("")) + ) + ' >&2 + fi + + local verdict + verdict="$(printf '%s\n' "$out" | jq -r '.admissible')" + local is_green + is_green="$(printf '%s\n' "$out" | jq -r '.green')" + + if [[ "$require_green" == "true" ]]; then + if [[ "$is_green" == "true" ]]; then exit "$EXIT_ADMISSIBLE"; fi + printf 'verify-evidence: refused — --require-green and the evidence is not green\n' >&2 + exit "$EXIT_REFUSED" + fi + if [[ "$verdict" == "true" ]]; then exit "$EXIT_ADMISSIBLE"; fi + printf 'verify-evidence: refused — the submission is inadmissible\n' >&2 + exit "$EXIT_REFUSED" +} + +main "$@" diff --git a/contracts/proven-tests/downstream-rust-fixture/.github/workflows/proven-evidence.yml b/contracts/proven-tests/downstream-rust-fixture/.github/workflows/proven-evidence.yml new file mode 100644 index 0000000..0b008cf --- /dev/null +++ b/contracts/proven-tests/downstream-rust-fixture/.github/workflows/proven-evidence.yml @@ -0,0 +1,102 @@ +# SPDX-License-Identifier: CC0-1.0 +# +# The reference consumer workflow for proven-tests-evidence/1.0.0. +# +# Three properties are the point of this file: +# +# 1. The contract is pinned by commit AND verified against its SHASUMS, so the +# rules that admit this run are the rules that were reviewed. +# 2. `cargo test` is allowed to fail without failing the step. The ONLY thing +# that can pass or fail the build is the evidence gate, so a failing suite +# cannot be silently dropped (the gate sees it) and cannot be counted twice +# (the step does not also fail). +# 3. The submission is bound to the commit being built via --expect-commit, so +# evidence from another revision cannot be replayed into this one. +name: proven-evidence +on: + pull_request: + branches: [main] + push: + branches: [main] +permissions: + contents: read +concurrency: + group: proven-evidence-${{ github.ref }} + cancel-in-progress: true +jobs: + evidence: + name: evidence / proven-tests + runs-on: ubuntu-24.04 + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@3f9a1c4b2d5e6f708192a3b4c5d6e7f809a1b2c3 + with: + persist-credentials: false + + - name: Pin the evidence contract by content + env: + CONTRACT_SHA: ffb26772e9e3bbb99f0c7f6cd3796e7d99eb64c1 + run: | + set -euo pipefail + git init -q .contract + git -C .contract fetch -q --depth 1 \ + https://github.com/hyperpolymath/proven-tests-and-benches "$CONTRACT_SHA" + git -C .contract checkout -q FETCH_HEAD + bash .contract/contracts/bin/verify-pin.sh proven-tests 1.0.0 \ + --repo-dir .contract/contracts + printf '%s\n' "$PWD/.contract/contracts/proven-tests/bin" >> "$GITHUB_PATH" + + - name: Run the suite, keeping the log and the exit code + id: test + run: | + set -uo pipefail + started="$(date -u +%Y-%m-%dT%H:%M:%SZ)" + cargo test -- --test-threads=1 2>&1 | tee test.log + rc="${PIPESTATUS[0]}" + finished="$(date -u +%Y-%m-%dT%H:%M:%SZ)" + { + printf 'rc=%s\n' "$rc" + printf 'started=%s\n' "$started" + printf 'finished=%s\n' "$finished" + } >> "$GITHUB_OUTPUT" + # A failing suite is EVIDENCE of failure, not a workflow error. The + # gate step below decides, and it sees the failure in the records. + exit 0 + + - name: Collect evidence from that one run + env: + TEST_RC: ${{ steps.test.outputs.rc }} + TEST_STARTED: ${{ steps.test.outputs.started }} + TEST_FINISHED: ${{ steps.test.outputs.finished }} + run: | + set -euo pipefail + collect-evidence.sh \ + --repo "$GITHUB_REPOSITORY" --commit "$GITHUB_SHA" \ + --log test.log --exit-code "$TEST_RC" \ + --coords .proven/coords.json \ + --command-argv '["cargo","test","--","--test-threads=1"]' \ + --started-at "$TEST_STARTED" --finished-at "$TEST_FINISHED" \ + --runner "${ImageOS:-unknown}" \ + --rust "$(rustc --version | cut -d' ' -f2)" \ + --out evidence.json + + - name: Admit the evidence, or be refused + run: | + set -euo pipefail + verify-evidence \ + --expect-commit "$GITHUB_SHA" \ + --expect-repo "$GITHUB_REPOSITORY" \ + --require-green --grid evidence.json > verdict.json + jq -r '"covered \(.coverage.cells_covered)/\(.coverage.cells_total) cells; \(.counts.passed) passed, \(.counts.skipped) skipped, \(.counts.failed) failed"' verdict.json + + - name: Upload the evidence, the verdict and the log + if: always() + uses: actions/upload-artifact@0d7fce4d1f6e5b8f0a4c3e2d1b0a9f8e7d6c5b4a + with: + name: proven-evidence + path: | + evidence.json + verdict.json + test.log + if-no-files-found: error diff --git a/contracts/proven-tests/downstream-rust-fixture/.proven/coords.json b/contracts/proven-tests/downstream-rust-fixture/.proven/coords.json new file mode 100644 index 0000000..cc4a5ae --- /dev/null +++ b/contracts/proven-tests/downstream-rust-fixture/.proven/coords.json @@ -0,0 +1,75 @@ +{ + "contract": "proven-tests-evidence/1.0.0", + "note": "What each test is, and where it sits. libtest's printed name is the key. Nothing here is generated: this is a declaration a reviewer reads, and the fixture pair is how the coordinate is audited.", + "tests": { + "ordering::is_total": { + "kind": "example", + "coord": { + "category": "UnitTest", + "aspect": "Functionality" + }, + "claim": "unproven", + "fixtures": { + "silence": { + "path": "tests/fixtures/empty_slice.txt", + "description": "an empty slice: no pair violates totality, so the check must stay silent" + }, + "firing": { + "path": "tests/fixtures/inverted_pair.txt", + "defect_class": "a comparator that reports both a += Minimal downstream fixture: a Rust repository submitting Proven-Tests evidence +:toc: preamble + +A whole repository's worth of integration, small enough to read in one sitting: +one crate, one test file, three tests, a coordinate map, and a workflow. Copy it, +replace the subject, keep the shape. + +== What is here + +[cols="1,3"] +|=== +| `Cargo.toml` +| `ordering-demo`: no dependencies, `rust-version = 1.85`, `publish = false`. + +| `src/lib.rs` +| The subject: a `Pair` with a total order, `is_total`, `sorted_seqs`. + +| `tests/ordering.rs` +| Three tests in `mod ordering`, so libtest prints `test ordering:: ... ok`. +| Those printed names are the keys of `.proven/coords.json` — the evidence path +| never guesses a coordinate from a test name. + +| `.proven/coords.json` +| The declaration: kind, typed coordinate, claim tier, tier evidence, fixture +| position, per test. + +| `tests/fixtures/*.txt` +| The silence and firing fixtures the declaration names. They exist so the +| paths are not aspirational. + +| `.github/workflows/proven-evidence.yml` +| Runs the suite, collects evidence from that one run, and gates on +| `verify-evidence --require-green --expect-commit "$GITHUB_SHA"`. +|=== + +== What each test claims, and why + +[cols="2,1,1,3"] +|=== +| Test | kind | claim | Why that is the honest label + +| `ordering::is_total` +| example +| unproven +| One fixed slice, one assertion. It would fail if totality broke, and it + establishes nothing beyond that slice. + +| `ordering::sorts_pair` +| example +| unproven +| Same shape. Declaring it `provisionally_proven` would need a type-safety + certificate for the subject, which this crate does not have. + +| `ordering::is_stable` +| property +| provisionally_proven +| 256 generated cases from a seeded LCG, with a shrinker that minimises a + failure. It is **sampling**: no total proof exists, so `actually_proven` is + refused here and the coordinate map says `provisionally_proven` in as many + words. +|=== + +The third test is the interesting one. A fixed vector loop is *not* a property — +the framework's own `TEST-NEEDS.adoc` records five such cells as THIN and re-labels +them Unproven. So this fixture writes a real generator, a real shrinker and a real +case count, or it would be demonstrating the defect the contract exists to catch. + +== How to run it + +[source,sh] +---- +cargo test -- --test-threads=1 # what the workflow runs +bash ../bin/collect-evidence.sh --help # the producer +bash ../bin/verify-evidence --help # the gate +---- + +The workflow is the complete path; `verify-evidence --grid` prints the 17×14 map +to stderr so a reader can see which cells the three tests actually occupy. + +== What this fixture does not claim + +* *It has not been executed here.* No Rust toolchain is present in the + environment where this contract package was written, so the crate is compiled + and run by **its own** workflow in the repository that adopts it. The contract's + conformance suite exercises the producer and the gate against recorded libtest + logs (`../fixtures/libtest/*.txt`), not against this crate. Nothing in this + package asserts that `cargo test` has run on it. +* *No evidence file is committed.* Committing a submission nobody produced would + be the exact forgery the contract refuses. The workflow writes `evidence.json` + and `verdict.json` and uploads them with the log. +* *The coordinates are declarations.* `UnitTest/Functionality` for `is_total` is + a judgement a reviewer can disagree with. What the gate can check is that the + coordinate exists, that the tier's evidence is present, and that coverage is + derived only from executed passes. + +== Promoting the third test, honestly + +If `ordering-demo` grew a machine-checked proof of stability — say an Idris2 +model of the comparator with a totality proof — the promotion is: + +. a `kind: "proof"` record whose `evidence.proof.checker` names the checker and + its version, whose `theorems` ladder has at least one rung with a + `term_digest`, and whose `execution.command` is that checker's own invocation; +. `claim: "actually_proven"`, which the validator will refuse for any + non-`proof` kind; +. a `design_proof` naming the technique and its limitations. + +Until then the label stays `provisionally_proven`. That is not modesty; it is the +rule. + +== Failure modes the fixture is built to show + +[cols="2,3"] +|=== +| Situation | What the path does +| A test panics +| libtest prints `FAILED`; the collector records `result: "failed"` with a detail and a per-test non-zero status; the gate admits the evidence and refuses green. The build fails on the gate, not on the cargo step. +| A test is `#[ignore]`d +| Recorded as `skipped` with its reason; it covers nothing and it stops green. Delete the attribute or delete the test — do not let the submission absorb it. +| The suite does not compile +| No per-test lines; the collector refuses (a run that executed nothing is not evidence). +| A new test is added without a coordinate +| The collector refuses it **by name**. A coordinate invented by the producer would be a fabricated cell. +| Coverage is claimed beyond the derivation +| Refused (R4). The report still prints the derived number, so the disagreement is visible rather than averaged away. +|=== diff --git a/contracts/proven-tests/downstream-rust-fixture/src/lib.rs b/contracts/proven-tests/downstream-rust-fixture/src/lib.rs new file mode 100644 index 0000000..4949079 --- /dev/null +++ b/contracts/proven-tests/downstream-rust-fixture/src/lib.rs @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +//! A deliberately small subject: a total order on a pair, and a stable sort. +//! +//! Nothing here is clever. The point of the fixture is the *evidence path*, so +//! the subject must be boring enough that a reader can see at once whether a +//! test's coordinate and claim are honest. + +/// A pair ordered lexicographically by `key`, then by `seq`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Pair { + pub key: u32, + pub seq: u32, +} + +impl Pair { + pub fn new(key: u32, seq: u32) -> Self { + Self { key, seq } + } + + /// Total order: `key` first, then `seq`. No two distinct pairs compare equal. + pub fn cmp_total(&self, other: &Self) -> std::cmp::Ordering { + self.key.cmp(&other.key).then(self.seq.cmp(&other.seq)) + } +} + +/// Is the order total over a slice: antisymmetric and transitive on every pair? +pub fn is_total(pairs: &[Pair]) -> bool { + for a in pairs { + for b in pairs { + let ab = a.cmp_total(b); + let ba = b.cmp_total(a); + if ab != ba.reverse() { + return false; + } + for c in pairs { + if ab == std::cmp::Ordering::Less && b.cmp_total(c) == std::cmp::Ordering::Less + && a.cmp_total(c) != std::cmp::Ordering::Less + { + return false; + } + } + } + } + true +} + +/// Sort by the total order and return the ordered sequence numbers. +pub fn sorted_seqs(mut pairs: Vec) -> Vec { + pairs.sort_by(Pair::cmp_total); + pairs.into_iter().map(|p| p.seq).collect() +} diff --git a/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/empty_slice.txt b/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/empty_slice.txt new file mode 100644 index 0000000..aa8fbd2 --- /dev/null +++ b/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/empty_slice.txt @@ -0,0 +1,4 @@ +silence fixture — an empty slice. + +No pair exists, so totality and stability are vacuously true. A check that fires +on this input is a harness fault, not a finding (TEST-DOCTRINE R10.6). diff --git a/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/inverted_pair.txt b/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/inverted_pair.txt new file mode 100644 index 0000000..b8fd58f --- /dev/null +++ b/contracts/proven-tests/downstream-rust-fixture/tests/fixtures/inverted_pair.txt @@ -0,0 +1,5 @@ +firing fixture — a comparator that reports both a +//! +//! The tests live in a module named `ordering` so that libtest prints +//! `test ordering:: ... ok`. Those printed names are the keys of +//! `.proven/coords.json`, which is what ties an executed test to a coordinate: +//! nothing in the evidence path guesses a coordinate from a test name. + +use ordering_demo::{is_total, sorted_seqs, Pair}; + +mod ordering { + use super::*; + + const CASES: usize = 256; + const SEED: u64 = 0x5eed; + + /// Inputs for the stability property: `CASES` case vectors from a 32-bit + /// LCG. Deterministic, so a failure is reproducible from the seed alone. + fn generated_cases(seed: u64, cases: usize) -> Vec> { + let mut state = seed; + let mut out = Vec::with_capacity(cases); + for _ in 0..cases { + state = state + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + let len = ((state >> 33) % 5) as usize; + let mut case = Vec::with_capacity(len); + for seq in 0..len { + state = state + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + let key = ((state >> 33) % 3) as u32; + case.push(Pair::new(key, seq as u32)); + } + out.push(case); + } + out + } + + /// The property: sorting by the total order is stable on equal keys, so the + /// resulting sequence of `seq` values is the input order grouped by key. + fn stability_failure(case: &[Pair]) -> bool { + let actual = sorted_seqs(case.to_vec()); + let mut expected: Vec = (0..case.len() as u32).collect(); + expected.sort_by_key(|seq| case[*seq as usize].key); + actual != expected + } + + /// Shrink a failing case by dropping one element at a time while the + /// failure persists. A report that names the minimal input is worth more + /// than one that names a 4-element vector. + fn shrink(case: &[Pair]) -> Vec { + let mut best = case.to_vec(); + let mut i = 0; + while i < best.len() { + let mut candidate = best.clone(); + candidate.remove(i); + if stability_failure(&candidate) { + best = candidate; + i = 0; + } else { + i += 1; + } + } + best + } + + /// Example evidence at UnitTest/Functionality: one fixed slice, checked. + #[test] + fn is_total() { + let pairs = [Pair::new(2, 1), Pair::new(1, 9), Pair::new(2, 0), Pair::new(1, 0)]; + assert!(is_total(&pairs)); + } + + /// Example evidence at UnitTest/Dependability: a comparator that disagreed + /// with its own reverse would make `is_total` false. + #[test] + fn sorts_pair() { + let pairs = vec![Pair::new(2, 5), Pair::new(1, 7), Pair::new(2, 1)]; + assert_eq!(sorted_seqs(pairs), vec![7, 1, 5]); + } + + /// Property evidence at PropertyBasedTest/Dependability: over `CASES` + /// generated cases, sorting is stable on equal keys. + /// + /// Declared `provisionally_proven`, never `actually_proven`: this is + /// sampling, however many cases run. `.proven/coords.json` says so out loud. + #[test] + fn is_stable() { + let cases = generated_cases(SEED, CASES); + let mut failures = 0usize; + let mut minimal: Option> = None; + + for case in &cases { + if stability_failure(case) { + failures += 1; + if minimal.is_none() { + minimal = Some(shrink(case)); + } + } + } + + assert_eq!( + cases.len(), + CASES, + "the generator changed size; update evidence.property.cases_run in .proven/coords.json" + ); + assert_eq!( + failures, 0, + "stability failed in {} of {} generated cases; minimal case: {:?}", + failures, + cases.len(), + minimal.as_deref().unwrap_or(&[]) + ); + } +} diff --git a/contracts/proven-tests/fixtures/coords/ordering.json b/contracts/proven-tests/fixtures/coords/ordering.json new file mode 100644 index 0000000..52ba993 --- /dev/null +++ b/contracts/proven-tests/fixtures/coords/ordering.json @@ -0,0 +1,37 @@ +{ + "contract": "proven-tests-evidence/1.0.0", + "tests": { + "ordering::is_total": { + "kind": "example", + "coord": { "category": "UnitTest", "aspect": "Functionality" }, + "claim": "unproven", + "fixtures": { + "silence": { "path": "tests/fixtures/empty_slice.txt", "description": "an empty slice: no pair is ever out of order" }, + "firing": { "path": "tests/fixtures/inverted_pair.txt", "defect_class": "a pair whose comparator reports both a oplus a b = oplus b a", + "term_digest": "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "file": "src/ProvenTests/Tropical.idr", + "line": 41 + } + ] + } + }, + "fixtures": { + "cannot_fail_by_design": "the property is enforced by the typechecker; no runtime firing fixture can exist" + }, + "anchor": { + "log": "check.log", + "line": 1 + } + } + ] +} diff --git a/contracts/proven-tests/fixtures/invalid/property-no-shrinker.json b/contracts/proven-tests/fixtures/invalid/property-no-shrinker.json new file mode 100644 index 0000000..53dabf2 --- /dev/null +++ b/contracts/proven-tests/fixtures/invalid/property-no-shrinker.json @@ -0,0 +1,82 @@ +{ + "contract": { + "name": "hyperpolymath/proven-tests/evidence", + "revision": "1.0.0", + "major": 1 + }, + "subject": { + "repo": "hyperpolymath/ordering-demo", + "commit": "1111111111111111111111111111111111111111", + "producer": { + "tool": "proven-tests collect-evidence", + "version": "1.0.0" + } + }, + "toolchain": { + "runner": "ubuntu-24.04", + "rust": "1.85.0", + "idris2": null + }, + "taxonomy": { + "revision": "proven-tests/taxonomy/1", + "cells": 238 + }, + "tests": [ + { + "id": "property::min_is_commutative", + "kind": "property", + "coord": { + "category": "PropertyBasedTest", + "aspect": "Dependability" + }, + "result": "passed", + "execution": { + "ran": true, + "command": [ + "cargo", + "test", + "--test", + "ordering", + "--", + "--test-threads=1" + ], + "runner": "ubuntu-24.04", + "started_at": "2026-10-25T10:00:00Z", + "finished_at": "2026-10-25T10:00:02Z", + "duration_ms": 2000, + "exit_code": 0, + "observed_output_digest": "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" + }, + "claim": "provisionally_proven", + "evidence": { + "property": { + "generator": "arb_ext_nat_pair", + "shrinker": false, + "cases_run": 256, + "failures": 0, + "seed": "0x5eed" + }, + "type_safety": { + "kategoria_level": 6, + "type_system": "Idris2", + "verified_by": "ProvenTests.Types.TypeSafetyCertificate" + }, + "framework_safety": "ProvenTests.Cells.provenTestsFrameworkProof" + }, + "fixtures": { + "silence": { + "path": "tests/fixtures/empty.txt", + "description": "an empty slice: no pair is ever out of order" + }, + "firing": { + "path": "tests/fixtures/inverted.txt", + "defect_class": "a pair whose comparator reports both a oplus a b = oplus b a", + "term_digest": "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "file": "src/ProvenTests/Tropical.idr", + "line": 41 + } + ] + } + }, + "fixtures": { + "cannot_fail_by_design": "the property is enforced by the typechecker; no runtime firing fixture can exist" + }, + "anchor": { + "log": "check.log", + "line": 1 + } + } + ], + "counts": { + "records": 3, + "executed": 3, + "passed": 3, + "failed": 0, + "error": 0, + "skipped": 0, + "not_run": 0, + "excluded_debt": 0 + } +} diff --git a/contracts/proven-tests/fixtures/valid/rust-example-pass.json b/contracts/proven-tests/fixtures/valid/rust-example-pass.json new file mode 100644 index 0000000..8ebb402 --- /dev/null +++ b/contracts/proven-tests/fixtures/valid/rust-example-pass.json @@ -0,0 +1,169 @@ +{ + "contract": { + "name": "hyperpolymath/proven-tests/evidence", + "revision": "1.0.0", + "major": 1 + }, + "subject": { + "repo": "hyperpolymath/ordering-demo", + "commit": "1111111111111111111111111111111111111111", + "producer": { + "tool": "proven-tests collect-evidence", + "version": "1.0.0" + } + }, + "toolchain": { + "runner": "ubuntu-24.04", + "rust": "1.85.0", + "idris2": null + }, + "taxonomy": { + "revision": "proven-tests/taxonomy/1", + "cells": 238 + }, + "tests": [ + { + "id": "ordering::is_total", + "kind": "example", + "coord": { + "category": "UnitTest", + "aspect": "Functionality" + }, + "result": "passed", + "execution": { + "ran": true, + "command": [ + "cargo", + "test", + "--test", + "ordering", + "--", + "--test-threads=1" + ], + "runner": "ubuntu-24.04", + "started_at": "2026-10-25T10:00:00Z", + "finished_at": "2026-10-25T10:00:02Z", + "duration_ms": 2000, + "exit_code": 0, + "observed_output_digest": "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" + }, + "claim": "unproven", + "evidence": {}, + "fixtures": { + "silence": { + "path": "tests/fixtures/empty.txt", + "description": "an empty slice: no pair is ever out of order" + }, + "firing": { + "path": "tests/fixtures/inverted.txt", + "defect_class": "a pair whose comparator reports both a +# +# run-conformance.sh — prove proven-tests-evidence/1.0.0 with fixtures. +# +# bash contracts/proven-tests/tests/run-conformance.sh +# +# Two populations are exercised: +# +# verify committed evidence documents against bin/verify-evidence, comparing +# admit/refuse, green, derived coverage and the rule ids that fired; +# collect committed libtest logs and coordinate maps against +# bin/collect-evidence.sh, then the submission the collector produced +# against bin/verify-evidence, so the producer→gate path is tested and +# not only the gate. +# +# Two further cases check the revision marker and the SHASUMS manifest. +# +# Needs bash, coreutils, awk and jq (1.6+). No Rust and no Idris2: the point of +# the contract is that a submitter needs neither, and the suite proves it by +# running without them. +# +# Exit codes: 0 every planned case ran and passed, 1 a case failed or did not +# run, 2 the suite could not start. + +set -euo pipefail + +readonly CONTRACT="proven-tests-evidence/1.0.0" +SUITE_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +EXPECT="${SUITE_DIR}/fixtures/expectations.json" +VERIFY="${SUITE_DIR}/bin/verify-evidence" +COLLECT="${SUITE_DIR}/bin/collect-evidence.sh" +MAKE_SUMS="${SUITE_DIR}/../bin/make-shasums.sh" + +readonly FIX_COMMIT="1111111111111111111111111111111111111111" +readonly FIX_REPO="hyperpolymath/ordering-demo" +readonly FIX_STARTED="2026-10-25T10:00:00Z" +readonly FIX_FINISHED="2026-10-25T10:00:02Z" + +for tool in jq bash awk; do + command -v "$tool" >/dev/null 2>&1 || { printf 'missing required tool: %s\n' "$tool" >&2; exit 2; } +done +[[ -r "$EXPECT" ]] || { printf 'missing %s\n' "$EXPECT" >&2; exit 2; } +[[ -x "$VERIFY" ]] || { printf '%s is not executable\n' "$VERIFY" >&2; exit 2; } +[[ -x "$COLLECT" ]] || { printf '%s is not executable\n' "$COLLECT" >&2; exit 2; } + +passed=0 +failed=0 +ran=0 +WORK="$(mktemp -d "${TMPDIR:-/tmp}/proven-conformance.XXXXXX")" +trap 'rm -rf "$WORK"' EXIT + +ok() { printf 'ok %s\n' "$1"; passed=$((passed + 1)); } +bad() { printf 'FAIL %s: %s\n' "$1" "$2"; failed=$((failed + 1)); } + +# compare_report NAME REPORT WANT_JSON — compare the fields that matter. +compare_report() { + local name="$1" report="$2" want_exit="$3" want_adm="$4" want_green="$5" want_cells="$6" want_rules="$7" + local got_adm got_green got_cells got_rules + got_adm="$(printf '%s' "$report" | jq -r '.admissible' 2>/dev/null || echo unparsed)" + got_green="$(printf '%s' "$report" | jq -r '.green' 2>/dev/null || echo unparsed)" + got_cells="$(printf '%s' "$report" | jq -r '.coverage.cells_covered' 2>/dev/null || echo unparsed)" + got_rules="$(printf '%s' "$report" | jq -c '[.findings[].rule] | unique | sort' 2>/dev/null || echo unparsed)" + + local problem="" + if [[ "$got_adm" == "unparsed" ]]; then + problem="stdout is not a report document" + elif [[ "$want_adm" != "$got_adm" ]]; then + problem="admissible <$got_adm>, expected <$want_adm>" + elif [[ "$want_green" != "$got_green" ]]; then + problem="green <$got_green>, expected <$want_green>" + elif [[ "$want_cells" != "$got_cells" ]]; then + problem="coverage cells <$got_cells>, expected <$want_cells>" + elif [[ "$want_rules" != "$got_rules" ]]; then + problem="rules <$got_rules>, expected <$want_rules>" + elif [[ "$want_exit" == "0" && "$got_adm" != "true" ]]; then + problem="exit 0 with an inadmissible report" + fi + + if [[ -z "$problem" ]]; then + printf 'ok verify: %s\n' "$name" + passed=$((passed + 1)) + else + printf 'FAIL verify: %s: %s\n' "$name" "$problem" + failed=$((failed + 1)) + fi +} + +verify_case() { + local i="$1" + local name file want_exit want_adm want_green want_cells want_rules out rc=0 + name="$(jq -r ".verify[$i].name" "$EXPECT")" + file="$(jq -r ".verify[$i].file" "$EXPECT")" + want_exit="$(jq -r ".verify[$i].exit" "$EXPECT")" + want_adm="$(jq -r ".verify[$i].admissible" "$EXPECT")" + want_green="$(jq -r ".verify[$i].green" "$EXPECT")" + want_cells="$(jq -r ".verify[$i].cells" "$EXPECT")" + want_rules="$(jq -c '.verify['"$i"'].rules | sort' "$EXPECT")" + local -a args=() + while IFS= read -r a; do args+=("$a"); done < <(jq -r ".verify[$i].args[]?" "$EXPECT") + + ran=$((ran + 1)) + out="$("$VERIFY" "${args[@]+"${args[@]}"}" "$SUITE_DIR/$file" 2>/dev/null)" || rc=$? + if [[ "$rc" != "$want_exit" ]]; then + printf 'FAIL verify: %s: exit %s, expected %s\n' "$name" "$rc" "$want_exit" + failed=$((failed + 1)) + return + fi + compare_report "$name" "$out" "$want_exit" "$want_adm" "$want_green" "$want_cells" "$want_rules" +} + +collect_case() { + local i="$1" + local name log coords exit_code expect_exit out rc=0 + name="$(jq -r ".collect[$i].name" "$EXPECT")" + log="$(jq -r ".collect[$i].log" "$EXPECT")" + coords="$(jq -r ".collect[$i].coords" "$EXPECT")" + exit_code="$(jq -r ".collect[$i].exit_code" "$EXPECT")" + expect_exit="$(jq -r ".collect[$i].expect_exit" "$EXPECT")" + + ran=$((ran + 1)) + out="$("$COLLECT" \ + --repo "$FIX_REPO" --commit "$FIX_COMMIT" \ + --log "$SUITE_DIR/$log" --exit-code "$exit_code" \ + --coords "$SUITE_DIR/$coords" \ + --command-argv '["cargo","test","--test","ordering","--","--test-threads=1"]' \ + --started-at "$FIX_STARTED" --finished-at "$FIX_FINISHED" \ + --runner ubuntu-24.04 --rust 1.85.0 2>/dev/null)" || rc=$? + + if [[ "$rc" != "$expect_exit" ]]; then + printf 'FAIL collect: %s: exit %s, expected %s\n' "$name" "$rc" "$expect_exit" + failed=$((failed + 1)) + return + fi + if [[ "$expect_exit" != "0" ]]; then + if [[ -n "$out" ]]; then + printf 'FAIL collect: %s: refused but wrote a document to stdout\n' "$name" + failed=$((failed + 1)) + else + printf 'ok collect: %s (refused, and wrote nothing)\n' "$name" + passed=$((passed + 1)) + fi + return + fi + + # The producer's own output must then satisfy the gate. + printf '%s\n' "$out" > "$WORK/evidence.json" + local t_args t_exit t_adm t_green t_cells + t_exit="$(jq -r ".collect[$i].then.exit" "$EXPECT")" + t_adm="$(jq -r ".collect[$i].then.admissible" "$EXPECT")" + t_green="$(jq -r ".collect[$i].then.green" "$EXPECT")" + t_cells="$(jq -r ".collect[$i].then.cells" "$EXPECT")" + local -a targs=() + while IFS= read -r a; do targs+=("$a"); done < <(jq -r ".collect[$i].then.args[]?" "$EXPECT") + + local vrc=0 vout + vout="$("$VERIFY" "${targs[@]+"${targs[@]}"}" "$WORK/evidence.json" 2>/dev/null)" || vrc=$? + if [[ "$vrc" != "$t_exit" ]]; then + printf 'FAIL collect: %s: collected evidence verified with exit %s, expected %s\n' "$name" "$vrc" "$t_exit" + failed=$((failed + 1)) + return + fi + compare_report "$name (collected, then verified)" "$vout" "$t_exit" "$t_adm" "$t_green" "$t_cells" '[]' +} + +main() { + local n i + + n="$(jq -r '.verify | length' "$EXPECT")" + for ((i = 0; i < n; i++)); do verify_case "$i"; done + + n="$(jq -r '.collect | length' "$EXPECT")" + for ((i = 0; i < n; i++)); do collect_case "$i"; done + + ran=$((ran + 1)) + if [[ "$(head -n 1 "$SUITE_DIR/REVISION" | tr -d '\r')" == "$CONTRACT" ]]; then + printf 'ok revision: REVISION names %s\n' "$CONTRACT" + passed=$((passed + 1)) + else + printf 'FAIL revision: REVISION is %s, expected %s\n' "$(head -n 1 "$SUITE_DIR/REVISION")" "$CONTRACT" + failed=$((failed + 1)) + fi + + ran=$((ran + 1)) + if bash "$MAKE_SUMS" "$SUITE_DIR" --check 2>/dev/null; then + printf 'ok manifest: SHASUMS matches every published file\n' + passed=$((passed + 1)) + else + printf 'FAIL manifest: SHASUMS does not match the files on disk\n' + failed=$((failed + 1)) + fi + + local planned + planned=$(( $(jq -r '.verify | length' "$EXPECT") + $(jq -r '.collect | length' "$EXPECT") + 2 )) + + printf '\n%d passed, %d failed, %d/%d planned cases ran\n' "$passed" "$failed" "$ran" "$planned" + if [[ "$failed" != "0" ]]; then + printf 'conformance: FAILED\n' >&2 + exit 1 + fi + if [[ "$ran" != "$planned" ]]; then + printf 'conformance: REFUSED — %d of %d planned cases ran; a case that does not run is not a pass\n' \ + "$ran" "$planned" >&2 + exit 1 + fi + printf 'conformance: %s OK\n' "$CONTRACT" +} + +main "$@" diff --git a/contracts/squabble/CONTRACT.adoc b/contracts/squabble/CONTRACT.adoc new file mode 100644 index 0000000..23444e6 --- /dev/null +++ b/contracts/squabble/CONTRACT.adoc @@ -0,0 +1,492 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += squabble downstream contract — revision `squabble-contract/1.0.0` +:toc: left +:toclevels: 3 +:sectnums: + +[.lead] +This is the contract a *different* repository's CI integrates against. It is +read-only by construction, pinned by content, and it distinguishes three claims +that are routinely confused: "GitHub would let this merge", "the gate is +satisfied", and "every required check actually ran and passed". Only the third +is `legitimate_green`, and this revision can certify it only from a gate bound +to one commit. + +IMPORTANT: *Immutability.* Revision `squabble-contract/1.0.0` is frozen. Any +change to the meaning of a field, a rule id, an exit code or a decision +procedure is a new major revision. Errata that change no behaviour ship as +`1.0.1` with a new `SHASUMS`. Consumers pin the revision id *and* the +`SHASUMS` digest (`bash contracts/bin/verify-pin.sh squabble 1.0.0`); nothing +here is to be consumed from a branch. + +== 1. Scope: the read-only invocation surface + +The contract covers exactly four subcommands. All four only read from GitHub and +write only to stdout/stderr. + +[cols="2,1,1,3"] +|=== +| Invocation | Writes | Exit codes | Contract role + +| `squabble fetch / ` +| nothing +| `0` gate JSON on stdout · `3` no `required_status_checks` rule on the base branch · `2` failure +| *The* evidence source. Emits the required-context set and the run bound to each. + +| `squabble diagnose ` +| nothing +| `0` · `2` unreadable or invalid gate +| Offline triage of a saved gate. Human text; the JSON surface is `fetch`'s output. + +| `squabble verify-satisfied / ` +| nothing +| `0` done · `5` agent items remain · `3` no gate · `2` failure +| The agent loop's "is there work left". *Not* a green claim — see §5. + +| `squabble chains ... [--json]` +| nothing +| `0` · `4` blocking finding (cycle, dead upstream) · `2` failure +| Optional cross-repo CI dependency check. +|=== + +Out of contract, and refused by the consumer audit (§8): + +* `squabble fight --apply` — writes a workflow file. +* `squabble board` — publishes. +* `squabble inbox-sweep` — writes. +* `squabble fight --summon` — network I/O to a boj-server the consumer does not + own. + +A consumer that needs these is not doing gate verification; it is doing +remediation, which is a human's or an owner agent's job with a human's token. + +== 2. Required GitHub permissions + +The gate is read through two APIs: the branch rules (the required set) and the PR's +`statusCheckRollup` (realised runs). Both are reads. + +[cols="2,1,3"] +|=== +| Permission | Access | Why the tool needs it + +| `contents` | read | Reads workflow files to attribute a context that never started (`STARTUP_FAILURE`), and resolves `uses:` refs for `chains`. +| `checks` | read | The realised check runs and their conclusions. +| `statuses` | read | Legacy commit statuses appear in the same rollup as check runs. +| `pull_requests` | read | The PR head, base, review threads and review decisions. +| `actions` | read | Whether Actions is enabled and what the repository's Actions policy allows, when a required context refuses to start. +| `metadata` | read | Implied by every installation token; not requestable, always present. +| `administration` | read | The branch *ruleset* / classic protection read. `verify-satisfied` and `fetch` both need it. +|=== + +=== 2.1 A workflow token cannot satisfy this + +`administration` is not on the list of scopes `GITHUB_TOKEN` can hold, so a +job-scoped `github.token` cannot read the required-context set. `squabble fetch` +and `squabble verify-satisfied` therefore need either: + +* a GitHub App installation token with `Administration: read` (plus the read + scopes above) on the *caller's* repository, or +* a fine-grained PAT with `Administration: read` on the caller's repository. + +Mint the narrowest of these. An App token scoped to the caller is enough; a +token with write scopes is a bypass waiting to happen (§8). + +=== 2.2 The permission floor and ceiling + +[source,yaml] +---- +# Prescribed. Read-only at workflow level; nothing elevated per job. +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +---- + +* Floor: the six read scopes above (or `read-all`, which is equivalent but + wider than necessary). +* Ceiling: *any* `: write` scope is a contract violation. The consumer audit + refuses `write-all` and any `*: write`. The tool cannot use them, and their + presence turns a read-only verification into a credential that can merge, + re-run, dismiss or edit — the exact things this contract exists to prevent. +* `id-token: write` is not needed and is refused by the audit as well: nothing + in the read-only surface needs OIDC. + +== 3. Pinned installation and release path + +Two pins, both content pins: the *action* is pinned to a commit, and the +*binary* it installs is pinned to a digest plus a build-provenance attestation. + +[source,yaml] +---- +- name: Install pinned squabble + uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@<40-hex commit sha> +---- + +What the action does, in order (see `.github/actions/squabble/install.sh`): + +. Refuses any platform that is not Linux on x86_64 — that is the only asset + published (`squabble-x86_64-linux-musl`). +. Downloads the release asset into a fresh directory. +. Refuses it unless its sha256 equals the pinned digest, *before* the file is + made executable or read by anything else. +. Refuses it unless `gh attestation verify` proves that asset was built by + `hyperpolymath/cicd-squabbler/.github/workflows/release.yml` at the pinned + tag, from the pinned source commit, on a GitHub-hosted runner, and that the + attested subject carries the same digest. The check reads the *JSON* form: the + plain-text form has been observed empty with exit 0 when stdout is not a + terminal. +. Only then makes it executable, and requires it to report the pinned version. + +[cols="1,3"] +|=== +| Release tag | `v0.1.0` (a locator — the digest is the trust anchor) +| Asset | `squabble-x86_64-linux-musl` +| Asset sha256 | `6cbeb4577d83ccf2dea3405a3afb0d34b7fee422af73f2113d413ea7edba026c` +| Source commit | `b854d17abc0dce296719a349ebe856ff945cf03e` +| Signer workflow | `hyperpolymath/cicd-squabbler/.github/workflows/release.yml` +|=== + +*Never* `@main`, `@master`, `@v0.1.0` or a mutable tag for the action: the +audit refuses a non-40-hex ref for this action, and refuses `@main`/`@master` +anywhere in the workflow. Release tags in this repository are immutable by +ruleset (`.github/rulesets/Immutable-Tags.json`); the digest and the attestation +do not depend on that being true. + +== 4. Machine-readable output + +Everything below is JSON on stdout, one document per invocation, and is +deterministic: no timestamps, no map ordering, no locale-dependent formatting. +Schemas live in `schema/`; the field names are the contract. Unknown fields may +appear in a later minor revision, so consumers must ignore unknown keys — but +must never *default* an unknown value to the favourable one (see §5.3). + +=== 4.1 Gate (from `squabble fetch`) + +[source,json] +---- +{ + "checks": [ + { "required_context": "ci / test", "run": "passed", "missing_cause": null }, + { "required_context": "scan / gitleaks", "run": "skipped" } + ] +} +---- + +[cols="1,1,3"] +|=== +| Field | Values | Meaning + +| `required_context` | string | The exact context name the ruleset requires. Case-sensitive. +| `run` | `missing` \| `pending` \| `failed` \| `skipped` \| `passed` | The run bound to that context on the head commit. When more than one run matches the name, the *worst* wins (`failed` > `missing` > `pending` > `skipped` > `passed`), so a passing twin cannot mask a failing one. +| `missing_cause` | `null` \| `no_such_job` \| `dead_action_pin` \| `actions_policy_refusal` \| `empty_jobs_map` \| `not_triggered_on_pull_request` \| `unknown` | Why a context is `missing`. Never changes `run`; a diagnosis is not a fix. +|=== + +`GitHub CANCELLED`, `TIMED_OUT`, `STARTUP_FAILURE`, `ERROR`, `ACTION_REQUIRED`, +`STALE` and any unrecognised conclusion all map to `failed`. They are never +folded into `skipped` and never into `passed`. `SKIPPED`/`NEUTRAL` map to +`skipped`, which the ruleset accepts and which carries no evidence. + +=== 4.2 Verdict (from `squabble verify-satisfied`) + +[source,json] +---- +{ + "repo": "owner/name", + "pr": 42, + "head_oid": "…", + "base_ref": "main", + "done": false, + "agent_items": [ { "kind": "required_not_satisfied", "context": "ci / test", "run": "failed" } ], + "held_by_human": [], + "evidence_free": [ "scan / gitleaks" ], + "notes": [ "…" ] +} +---- + +`agent_items[].kind` is one of `conflicting`, `mergeability_unknown`, `draft`, +`required_not_satisfied`, `check_failed`, `unresolved_thread`, +`changes_requested`, `review_bot_pending`, `auto_merge_not_armed`, +`wrong_merge_method`, `branch_behind`, `merge_queue`, `unverified_commits`, +`awaiting_approval`, `awaiting_deployment`, `awaiting_human_merge`. +`evidence_free` lists required contexts satisfied by a skip or neutral. + +=== 4.3 Bound gate envelope (the input to a green claim) + +Because a bare gate document carries no commit, it can be replayed. A green +claim therefore needs an envelope, which this contract's `bind-gate` produces: + +[source,json] +---- +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "owner/name", "head_sha": "<40 hex>", "pr": 42 }, + "gate": { "checks": [ … ] } +} +---- + +`subject.head_sha` must be the head commit the gate was sampled at — in a +workflow, `${{ github.event.pull_request.head.sha }}` (or `${{ github.sha }}` +for a `merge_group`/push gate), never a branch name. + +=== 4.4 Verdict document (from `legitimate-green`) + +[source,json] +---- +{ + "contract": "squabble-contract/1.0.0", + "input": "envelope", + "verdict": "legitimate_green", + "legitimate_green": true, + "subject": { "repo": "owner/name", "head_sha": "<40 hex>", "pr": 42 }, + "subject_bound": true, + "requirement_count": 2, + "passed_evidence_count": 2, + "evidence_free": [], + "blocking": [], + "reasons": [] +} +---- + +`verdict` is `legitimate_green`, `not_green`, or `not_certifiable`. `blocking[]` +entries are `{context, run, reason}`. `reasons[]` explains a non-green verdict +that is not attributable to one context (no requirements, unbound input, a +verdict document instead of a gate). + +== 5. Three claims that are not the same claim + +This is the whole point of the contract, and the reason a single exit code +cannot carry it. + +[cols="1,2,2"] +|=== +| Claim | Established by | What it does *not* mean + +| *ruleset-legitimate* (GitHub will merge it) +| `squabble verify-satisfied` exit `0` (`done: true`) +| That the required checks ran. GitHub accepts `skipped`/`neutral` for a required context, and a required check that is merely `pending` is not an agent item, so `done` can be true with a required check still in flight. + +| *gate satisfied* (no unsatisfied required context) +| `squabble fetch` gate with no `missing`/`pending`/`failed` run +| That every requirement carried evidence — a `skipped` run satisfies the gate. + +| *legitimate_green* +| §5.1, over a bound envelope +| Anything about non-required checks, review threads, or the human review. It is a statement about the required set only. +|=== + +=== 5.1 The decision procedure (normative) + +Given a *bound envelope* (§4.3): + +[source] +---- +legitimate_green ⇔ + subject.head_sha is 40 lowercase hex + ∧ subject.repo is owner/name + ∧ |gate.checks| ≥ 1 + ∧ ∀ c ∈ gate.checks : c.run = "passed" +---- + +Equivalently for the emitted document: `legitimate_green: true` and exit `0`. +`evidence_free` must be empty and `blocking` must be empty; both follow from the +third clause and are emitted so a reader does not have to re-derive them. + +=== 5.2 What makes a green claim uncertifiable + +[cols="1,2"] +|=== +| Input | Verdict | Why +| Bare gate (`{"checks": …}`) without an envelope +| `not_certifiable`, exit `3` +| It names no commit, so it can be replayed from any run. `--allow-unbound` allows the *document* to be evaluated for triage, and still exits `3`: an unbound gate can never certify green. +| `verify-satisfied` verdict document +| `not_certifiable`, exit `3` +| It carries no per-requirement run states (`evidence_free` is the only trace of a skip), and `done` tolerates a pending required check. A verdict document can never certify green, in any combination of flags. +| A gate directory or array at top level +| `not_certifiable`, exit `3` +| Not a document this contract knows. Fail closed. +|=== + +=== 5.3 Rule: never default an unknown value to the favourable one + +If a `run` value is not one of the five known values, the requirement is +blocking (`unrecognised run state`). If the document has an unknown shape, the +answer is `not_certifiable`. A consumer that parses this contract's JSON must +apply the same rule: `passed` is matched explicitly, never inferred from "not +failed". + +== 6. Exit semantics + +[cols="1,1,3"] +|=== +| Code | Name | Prescribed consumer handling + +| `0` | green / ok | Proceed. For `legitimate-green` this is the only code that may be reported as a legitimate green. +| `2` | failure | The tool could not do its job (usage, `gh` failed, unparseable input, missing token). Fail the job. Do *not* treat as a finding. +| `3` | finding: no gate, or not certifiable | Report it and fail the job. It is not a green and not a tool failure. `squabble fetch` uses `3` for "the base branch requires no status checks"; `legitimate-green` uses `3` for every non-certifiable or non-green verdict. +| `4` | finding: blocking `chains` result | Report it and fail the job. +| `5` | finding: `verify-satisfied` not done | Report it. In an agent loop, keep working; in a merge gate, fail. +| other non-zero | unexpected | Fail the job. +|=== + +`3`, `4` and `5` exist so that a pipeline can distinguish "there is something +here to report" from "the tool is broken". Collapsing them into `1` is a +contract violation because it makes the two indistinguishable. + +== 7. Negative fixtures: what cannot be green + +`fixtures/` holds one document per case and `fixtures/expectations.json` holds +the expected exit code and verdict for each. `tests/run-conformance.sh` runs +every case and fails unless every planned case ran. + +[cols="2,1,3"] +|=== +| Fixture | Expected | Proves + +| `gate/all-passed.bound.json` +| `0`, `legitimate_green` +| The positive control: a bound envelope whose every requirement passed certifies green. Without this the negatives prove only that the tool says no. + +| `gate/single-passed.bound.json` +| `0`, `legitimate_green` +| One requirement is enough; the procedure is not "at least two". + +| `gate/required-missing.bound.json` +| `3`, `not_green`, blocking `missing` +| A required check with no run bound on the head commit cannot be green — the `Missing` deadlock, where nothing reported at all. + +| `gate/required-skipped.bound.json` +| `3`, `not_green`, `evidence_free: ["scan / gitleaks"]` +| A *skipped* required check is accepted by GitHub's ruleset but is not a legitimate green here. This is the case a merge would hide. + +| `gate/required-cancelled.bound.json` +| `3`, `not_green`, blocking `failed` +| A cancelled run maps to `failed` and blocks. Cancellation is not a pass and not a skip. + +| `gate/required-failed.bound.json` +| `3`, `not_green`, blocking `failed` +| An ordinary failure blocks. + +| `gate/required-pending.bound.json` +| `3`, `not_green`, blocking `pending` +| An unfinished run blocks. Note `verify-satisfied` does *not* call a pending *required* check an agent item; that is exactly why a verdict document cannot certify green. + +| `gate/passed-and-skipped.bound.json` +| `3`, `not_green` +| One passing requirement does not launder a skipped sibling. + +| `gate/no-required-checks.bound.json` +| `3`, `not_green`, reason `no-required-checks` +| Dropping the required set is not a win: an unprotected gate is `Blocked`, never green. + +| `gate/unknown-run-state.bound.json` +| `3`, `not_green`, blocking `unrecognised` +| A state this revision does not know is blocking. Fail closed on vocabulary drift. + +| `gate/all-passed.unbound.json` +| `3`, `not_certifiable` +| Correct-looking evidence with no commit binding does not certify. + +| `envelope/all-passed.wrong-head.bound.json` +| `3`, `not_green` +| `--expect-head-sha` mismatch: evidence for another commit is refused, so a replayed envelope fails. + +| `envelope/all-passed.bad-subject.bound.json` +| `3`, `not_green` +| `head_sha: "main"` is not a commit. A branch is a moving pin (see §3) and is refused. + +| `verdict/done-with-skipped.json` +| `3`, `not_certifiable` +| `done: true` with `evidence_free: ["scan / gitleaks"]` — the mergeable-but-evidence-free case, refused. + +| `verdict/done-clean.json` +| `3`, `not_certifiable` +| Even a clean `done: true` cannot certify green, because the document carries no run states. A consumer that gates on exit `0` here has no contract, only a habit. + +| `verdict/not-done.json` +| `3`, `not_certifiable` +| The negative control for the previous case. +|=== + +== 8. Bypass resistance + +`squabble ≠ bypass` is a property of the engine: the only path to `Green` is a +run that passed, an empty requirement set is `Blocked`, a diagnosis never moves +the state, and a context's worst run decides. Nothing in this contract adds a +path around that. This contract adds the consumer-side half: + +[cols="1,2"] +|=== +| Rule (audit id) | Refusal +| `E-UNPINNED-ACTION` +| The squabble action is not pinned to a 40-hex commit. A moving branch means the rules that gated the reviewed run are not the rules that gate the merge. +| `E-MOVING-REF` +| Any `@main`/`@master`/`@HEAD` ref in the workflow. +| `E-WRITE-PERMISSION` +| `write-all`, or any `*: write` scope. The read-only surface cannot use them; their presence is an unused capability that a later edit can arm. +| `E-MASKED-STEP` +| `continue-on-error: true`, or `|| true`, or `set +e` around a squabble step. A gate whose failure cannot fail the job is not a gate. +| `E-BYPASS-COMMAND` +| `gh pr merge … --admin`, `enforce_admins`, a write to a protection/ruleset endpoint, `fight --apply`, `squabble board`, `inbox-sweep`, `gh run rerun`, `gh workflow run`. These change the gate rather than win it. +| `E-PRIVILEGED-TRIGGER` +| `pull_request_target` alongside a checkout of the PR head: write-capable token plus attacker-controlled code. +| `E-NO-ORACLE` +| The workflow runs squabble but never asks `legitimate-green`. Then it is gating on `done`, which §5 shows is a weaker claim. +|=== + +The audit is a lint, not a sandbox: it reads the workflow text and refuses +patterns it knows. The real boundary is the permission set — a read-only token +cannot merge, re-run or edit anything, whatever the workflow says. Run both. + +== 9. Known limitations of revision 1.0.0 + +Stated because a contract that hides its blind spots is a claim, not a contract. + +* *Replay without an envelope.* A bare gate document names no commit. The + envelope closes this, and `legitimate-green` refuses to certify without one; + nothing in the tool itself records the sampling commit. +* *`github.token` cannot read the gate.* `administration: read` needs an App or + fine-grained PAT (§2.1). This is a GitHub constraint, not a choice. +* *Classic branch protection.* `fetch` reads both rulesets and classic + protection, but `main.rs`'s own note still applies to the rules API path: + a `3` ("no gate") speaks only to the endpoint that was queried. Treat `3` as + "no gate found by the surfaces this revision reads". +* *Required contexts are matched by name.* Two jobs with the same name are + resolved worst-first, which is safe, but a workflow that emits the required + name from a *different* job than intended is indistinguishable from the + intended one. +* *x86_64 Linux only.* No other asset is published or attested. +* *Non-required checks* are outside `legitimate_green`. A red non-required check + is reported by `verify-satisfied` (`check_failed`), not by this procedure. +* *Review human-facing obligations* (threads, requested changes) are not part of + a green claim; they are `verify-satisfied` items. + +== 10. Change policy + +[cols="1,2"] +|=== +| Change | Version +| A new fixture, a new audit rule that refuses something previously allowed, a documentation fix | major — consumers were relying on the old allowance +| A new optional field, a new subcommand in the read-only surface, a new fixture for an already-covered rule | minor (`1.1.0`) +| A typo that changes no byte of behaviour | patch (`1.0.1`) with a regenerated `SHASUMS` +|=== + +Any change regenerates `SHASUMS` +(`bash contracts/bin/make-shasums.sh contracts/squabble`) and must keep +`bash contracts/squabble/tests/run-conformance.sh` green with every planned case +run. + +== 11. Verifying this revision + +[source,sh] +---- +bash contracts/bin/verify-pin.sh squabble 1.0.0 # revision + digest, as a consumer checks it +bash contracts/squabble/tests/run-conformance.sh # every fixture, every audit case +---- + +The conformance suite needs `bash`, coreutils and `jq` (1.6+). It needs no +network, no token and no Rust toolchain, which is what makes it runnable in a +consumer's CI as well as here. diff --git a/contracts/squabble/REVISION b/contracts/squabble/REVISION new file mode 100644 index 0000000..a76c4b5 --- /dev/null +++ b/contracts/squabble/REVISION @@ -0,0 +1 @@ +squabble-contract/1.0.0 diff --git a/contracts/squabble/SHASUMS b/contracts/squabble/SHASUMS new file mode 100644 index 0000000..72fb9bc --- /dev/null +++ b/contracts/squabble/SHASUMS @@ -0,0 +1,34 @@ +b4f4e0f49bab0dbab24bc8ce8e8f8fe1869dbb4f98a0cb0ede597371f263375b CONTRACT.adoc +473eb9fee7f34ae66ed69ce0466ff536822a06959a5f11f1f81109a599b3304e REVISION +d664ae185a8fa091747177a67760b3db7382890646d3187f7a0356b39938e8bf bin/audit-consumer-workflow.sh +045bce1dad7be7fbcdef3485366c5e24601e93d041020fbaf40daeff2cb4ad3d bin/bind-gate +5555154b57305ab470f36cb54912e5200532f370d04467a76e3c46860d762d24 bin/legitimate-green +51eb4812b9defbe457060c58bcaf34c46482dfb694d34622e0765a39f53be811 fixtures/consumer-workflow/bad-bypass.yml +58b0ab8ba25d1368bf86f8cbef5ec2d1ab0fd2e6d3669fc479f87f4d259517ae fixtures/consumer-workflow/bad-masked-step.yml +79cd7e0ef4775917aba682333231e0831fbb9676622ead2d446cc9623f3c79f6 fixtures/consumer-workflow/bad-moving-ref.yml +0a4f9c56be13e6cb7e0197a4c65c97eb614429d1fe543c94a6c616becf00d6ef fixtures/consumer-workflow/bad-no-oracle.yml +359ac1d85c607ec08d9ff15504980ed4f0cb7506c0b5852aa2bb4c4b4e21e9fd fixtures/consumer-workflow/bad-unpinned-action.yml +68a20052846a6abd19b65c4abdc9a0d84d91d8f15ed368179b29eb41f0b0d77f fixtures/consumer-workflow/bad-write-permission.yml +fae12b9508a982a6519ed1951feceb185010e999c11919e898c04130584cd17c fixtures/consumer-workflow/good-readonly.yml +851bd47c6605e3792d297256dc98d5ad5dd8fa6b8df678fb2a1a2ad513cd92dd fixtures/envelope/all-passed.bad-subject.bound.json +a303fba6892276fa4398812671c9452a0e80025b417ee4eee9fb0092eaadaae9 fixtures/envelope/all-passed.wrong-head.bound.json +c2d4b748bcc47b44290b1365c2f178b1840ed85e932f1707be7adea029f83cd8 fixtures/expectations.json +18881269a4172b8d41e046135f8a20531859c5ff4ca8d9eac3753c84dcf65013 fixtures/gate/all-passed.bound.json +917ff9906daa6f527fc95c28d84cf581a8ff19e325c6f2c8478feee1926bdd83 fixtures/gate/all-passed.unbound.json +bf3b867430cc7e43811c133d3db1e8668d7de621a6c51ec30a4c309099bc7233 fixtures/gate/no-required-checks.bound.json +f1862b195535b04dc1753be140165417d90be203a9427a75cac0bd5f3fbc2581 fixtures/gate/passed-and-skipped.bound.json +b5e24d67379ec7d7561de2337e29a5651c132ddf8a1836e33a4e5bb1e60c54d8 fixtures/gate/required-cancelled.bound.json +c59e98a9f6cf05f9ae7ff75f09f3a14b670781e31b222a741fcaca1f7a8cf4ef fixtures/gate/required-failed.bound.json +3d844ce3e4db1ac804503ab351e0b91c88c5fb123b1c239022f7520fd947f9a9 fixtures/gate/required-missing.bound.json +3e0a62ad9e6d390ba3feeaafa1e19479506bec98cc009926225335363f677a17 fixtures/gate/required-pending.bound.json +220a76b8df8616b4141a9c6cfefe3225336c58186155dd3867b508e00eddf09e fixtures/gate/required-skipped.bound.json +a303fba6892276fa4398812671c9452a0e80025b417ee4eee9fb0092eaadaae9 fixtures/gate/single-passed.bound.json +e698f3091b86099d254bc4c8d8c41ea3cdc73c1abd641c5a88d5eee2905378c7 fixtures/gate/unknown-run-state.bound.json +9e498138b6c7352725f08cef789d36922b8d9d903f15900a706d3bece1be3720 fixtures/verdict/done-clean.json +3bf6f28b70d6b6851608a6ac823d0551bcafe4526791dd77fa07e2142fd6e26c fixtures/verdict/done-with-skipped.json +face803b19603542c6cd9bb347cd37b556b6a62d5e2d77a721b186eff4c42b8b fixtures/verdict/not-done.json +4ccab4536dababdc0cb37a6069a22f38ea8b932aa3cedef68cf71800dd7f8751 schema/envelope.schema.json +054f01711dccb7880dfa72882ace84fec999a2cc84179af867250c8e2ff58cd8 schema/gate.schema.json +f664e93e864c5c46371adc9af12edf0853f15888f0252769f0d6c2f06f6d0305 schema/legitimate-green.schema.json +7a28791cb40c6f5991a2c8b5b2dd3206e434f75edcf79d434e8b4bb197bb3d97 schema/verdict.schema.json +b73ccb16ea42eddf422453799183ece3b9bca8ee497db606e34784539ebcf92b tests/run-conformance.sh diff --git a/contracts/squabble/bin/audit-consumer-workflow.sh b/contracts/squabble/bin/audit-consumer-workflow.sh new file mode 100755 index 0000000..1fadfb8 --- /dev/null +++ b/contracts/squabble/bin/audit-consumer-workflow.sh @@ -0,0 +1,133 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# audit-consumer-workflow.sh — lint a consumer's workflow against +# squabble-contract/1.0.0 §8, before a human has to. +# +# audit-consumer-workflow.sh .github/workflows/gate.yml +# +# It refuses, with a stable finding code: +# +# E-UNPINNED-ACTION the squabble action is not pinned to a 40-hex commit +# E-MOVING-REF a `uses:` ref of @main / @master / @HEAD +# E-WRITE-PERMISSION write-all, or any `*: write` scope +# E-NO-PERMISSIONS no top-level `permissions:` block at all +# E-MASKED-STEP continue-on-error: true, `|| true`, or `set +e` +# E-BYPASS-COMMAND a command that changes the gate instead of winning it +# E-OUT-OF-CONTRACT-SUBCOMMAND fight / board / inbox-sweep as an argument line +# E-PRIVILEGED-TRIGGER pull_request_target +# E-NO-ACTION the workflow never uses the pinned action +# E-NO-SAMPLER it never samples a gate (fetch / verify-satisfied / chains) +# E-NO-ORACLE it never asks legitimate-green, so it gates on `done` +# +# FINDINGS ARE A LINT, NOT A SANDBOX. This reads text and refuses patterns it +# knows; a workflow can be wrong in ways this does not model. The real boundary +# is the permission set: a read-only token cannot merge, re-run or edit +# anything, whatever the YAML says. Run both. +# +# Exit codes: 0 clean, 3 findings, 2 usage/environment failure. Finding lines go +# to stdout as ` : `; the summary goes to stderr. +# +# Contract revision: squabble-contract/1.0.0. + +set -euo pipefail + +readonly EXIT_OK=0 +readonly EXIT_FINDINGS=3 +readonly EXIT_USAGE=2 + +usage() { + printf 'usage: audit-consumer-workflow.sh FILE.yml\n' >&2 +} + +die() { + printf 'audit-consumer-workflow: %s\n' "$*" >&2 + exit "$EXIT_USAGE" +} + +main() { + if [[ $# -ne 1 ]]; then usage; exit "$EXIT_USAGE"; fi + case "$1" in -h|--help) usage; exit 0 ;; -*) usage; die "unknown option: $1" ;; esac + local file="$1" + [[ -r "$file" ]] || die "cannot read $file" + local base + base="$(basename "$file")" + + # Findings are buffered so the same (code, line) cannot be reported twice by + # two patterns that both describe one defect, and so output is stable. + local -a findings=() + + # report CODE LINE TEXT — record one finding. + report() { + findings+=("$(printf '%s\t%04d\t%s' "$1" "$2" "$3")") + } + + # collect CODE REGEX — report every line of $file matching REGEX. + collect() { + local code="$1" re="$2" line text + while IFS=: read -r line text; do + [[ -z "$line" ]] && continue + report "$code" "$line" "$(printf '%s' "$text" | sed 's/^[[:space:]]*//')" + done < <(grep -nEi -- "$re" "$file" 2>/dev/null || true) + } + + # ── pins ──────────────────────────────────────────────────────────────── + if grep -qEi 'uses:[[:space:]]*[^#]*cicd-squabbler' "$file" 2>/dev/null; then + local line text + while IFS=: read -r line text; do + [[ -z "$line" ]] && continue + if ! printf '%s\n' "$text" | grep -Eq '@[0-9a-fA-F]{40}([[:space:]]|$)'; then + report "E-UNPINNED-ACTION" "$line" "$(printf '%s' "$text" | sed 's/^[[:space:]]*//')" + fi + done < <(grep -nEi 'uses:[[:space:]]*[^#]*cicd-squabbler' "$file") + else + report "E-NO-ACTION" "0" "no step uses hyperpolymath/cicd-squabbler/.github/actions/squabble" + fi + + collect "E-MOVING-REF" 'uses:[[:space:]]*[^#]*@(main|master|HEAD)([[:space:]]|$)' + collect "E-WRITE-PERMISSION" '(^|[[:space:]])write-all([[:space:]]|$)|[a-z-]+:[[:space:]]*["'"'"']?write["'"'"']?([[:space:]]|$)' + if ! grep -qE '^permissions:' "$file" 2>/dev/null; then + report "E-NO-PERMISSIONS" "0" "no top-level permissions block; the token's default scopes are not this contract's floor" + fi + + # ── a gate that can fail must be able to fail ──────────────────────────── + collect "E-MASKED-STEP" 'continue-on-error:[[:space:]]*true' + collect "E-MASKED-STEP" '\|\|[[:space:]]*(true|:)([[:space:]]|$)' + collect "E-MASKED-STEP" 'set[[:space:]]+\+e' + + # ── bypasses ──────────────────────────────────────────────────────────── + collect "E-BYPASS-COMMAND" '--admin([[:space:]]|$)' + collect "E-BYPASS-COMMAND" 'enforce_admins' + collect "E-BYPASS-COMMAND" 'squabble[[:space:]]+[^|]*--apply' + collect "E-BYPASS-COMMAND" '(gh[[:space:]]+api|api\.github\.com)[^|]*(-X|--method)[[:space:]]*(PUT|PATCH|POST|DELETE)' + collect "E-BYPASS-COMMAND" 'gh[[:space:]]+(run[[:space:]]+rerun|workflow[[:space:]]+run)' + collect "E-OUT-OF-CONTRACT-SUBCOMMAND" '^[[:space:]]*(fight|board|inbox-sweep)([[:space:]]|$)' + collect "E-OUT-OF-CONTRACT-SUBCOMMAND" 'squabble[[:space:]]+(fight|board|inbox-sweep)([[:space:]]|$)' + collect "E-PRIVILEGED-TRIGGER" 'pull_request_target' + + # ── the read-only surface must actually be used ───────────────────────── + if ! grep -qE '(^|[[:space:]])squabble[[:space:]]+(fetch|diagnose|verify-satisfied|chains)([[:space:]]|$)' "$file" 2>/dev/null; then + report "E-NO-SAMPLER" "0" "no read-only squabble subcommand (fetch/diagnose/verify-satisfied/chains) is invoked" + fi + if ! grep -qE 'legitimate-green' "$file" 2>/dev/null; then + report "E-NO-ORACLE" "0" "legitimate-green is never invoked; gating on \`done\` is a weaker claim (CONTRACT.adoc §5)" + fi + + if (( ${#findings[@]} > 0 )); then + local row + while IFS= read -r row; do + printf '%s %s:%s %s\n' \ + "$(printf '%s' "$row" | cut -f1)" \ + "$base" \ + "$(printf '%s' "$row" | cut -f2 | sed 's/^0*//;s/^$/0/')" \ + "$(printf '%s' "$row" | cut -f3)" + done < <(printf '%s\n' "${findings[@]}" | sort -u) + printf '%d finding(s) in %s\n' "$(printf '%s\n' "${findings[@]}" | sort -u | wc -l | tr -d ' ')" "$base" >&2 + exit "$EXIT_FINDINGS" + fi + printf 'clean %s\n' "$base" >&2 + exit "$EXIT_OK" +} + +main "$@" diff --git a/contracts/squabble/bin/bind-gate b/contracts/squabble/bin/bind-gate new file mode 100755 index 0000000..6f10fc6 --- /dev/null +++ b/contracts/squabble/bin/bind-gate @@ -0,0 +1,102 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# bind-gate — wrap a gate document in the bound envelope of +# squabble-contract/1.0.0, so a green claim names the commit it was sampled at. +# +# squabble fetch owner/repo 42 \ +# | bind-gate --repo owner/repo --head-sha "$PR_HEAD_SHA" --pr 42 \ +# > bound-gate.json +# +# A bare gate document carries no commit, so it can be replayed from any run. +# The envelope fixes the subject; `legitimate-green` refuses to certify without +# one. The gate is re-emitted field by field, so nothing can ride along inside +# it: only `required_context`, `run` and `missing_cause` survive. +# +# exit 0 envelope on stdout +# exit 3 the input is not a gate document this contract knows +# exit 2 usage error, unreadable input, invalid JSON, bad --repo/--head-sha +# +# Contract revision: squabble-contract/1.0.0. Writes nothing; reads one document. + +set -euo pipefail + +readonly CONTRACT_REVISION="squabble-contract/1.0.0" +readonly EXIT_OK=0 +readonly EXIT_REFUSED=3 +readonly EXIT_USAGE=2 + +usage() { + printf 'usage: bind-gate --repo OWNER/NAME --head-sha <40-hex> [--pr N] [FILE|-]\n' >&2 + printf ' wraps a `squabble fetch` gate document in a commit-bound envelope\n' >&2 +} + +die() { + printf 'bind-gate: %s\n' "$*" >&2 + exit "$EXIT_USAGE" +} + +read -r -d '' JQ_PROGRAM <<'JQ' || true +def kept: + { required_context: .required_context, run: .run } + + (if has("missing_cause") then { missing_cause: .missing_cause } else {} end); + +(if length != 1 then error("expected exactly one JSON document") else .[0] end) as $doc +| (if ($doc | type) == "object" and (($doc.checks | type) == "array") then + { checks: [ $doc.checks[] | kept ] } + else null end) as $gate +| if $gate == null + then { contract: $revision, gate: null, refused: "not-a-gate-document" } + else { contract: $revision, + subject: { repo: $repo, head_sha: $head, pr: ($pr | if . == "" then null else tonumber end) }, + gate: $gate } + end +JQ + +main() { + local repo="" head_sha="" pr="" file="-" + while [[ $# -gt 0 ]]; do + case "$1" in + --repo) [[ $# -ge 2 ]] || die "--repo needs a value"; repo="$2"; shift 2 ;; + --head-sha) [[ $# -ge 2 ]] || die "--head-sha needs a value"; head_sha="$2"; shift 2 ;; + --pr) [[ $# -ge 2 ]] || die "--pr needs a value"; pr="$2"; shift 2 ;; + -h|--help) usage; exit 0 ;; + --) shift; [[ $# -eq 1 ]] || { usage; die "one FILE only"; }; file="$1"; shift ;; + -) file="-"; shift ;; + -*) usage; die "unknown option: $1" ;; + *) [[ "$file" == "-" ]] || { usage; die "one FILE only"; }; file="$1"; shift ;; + esac + done + [[ -n "$repo" ]] || { usage; die "missing --repo"; } + [[ -n "$head_sha" ]] || { usage; die "missing --head-sha"; } + [[ "$repo" =~ ^[^/[:space:]]+/[^/[:space:]]+$ ]] || die "--repo must be OWNER/NAME (got: $repo)" + [[ "$head_sha" =~ ^[0-9a-f]{40}$ ]] || die "--head-sha must be 40 lowercase hex characters (got: $head_sha)" + if [[ -n "$pr" && ! "$pr" =~ ^[1-9][0-9]*$ ]]; then + die "--pr must be a positive integer (got: $pr)" + fi + command -v jq >/dev/null 2>&1 || die "jq (1.6 or later) is required" + if [[ "$file" != "-" && ! -r "$file" ]]; then + die "cannot read $file" + fi + + local out rc=0 + out="$(jq --slurp \ + --arg revision "$CONTRACT_REVISION" \ + --arg repo "$repo" \ + --arg head "$head_sha" \ + --arg pr "$pr" \ + "$JQ_PROGRAM" -- "$file" 2>/dev/null)" || rc=$? + if (( rc != 0 )); then + printf 'bind-gate: %s is not a single valid JSON document\n' "$file" >&2 + exit "$EXIT_USAGE" + fi + if printf '%s\n' "$out" | jq -e '.gate == null' >/dev/null 2>&1; then + printf 'bind-gate: the input is not a gate document (expected {"checks": [...]})\n' >&2 + exit "$EXIT_REFUSED" + fi + printf '%s\n' "$out" + exit "$EXIT_OK" +} + +main "$@" diff --git a/contracts/squabble/bin/legitimate-green b/contracts/squabble/bin/legitimate-green new file mode 100755 index 0000000..d55217e --- /dev/null +++ b/contracts/squabble/bin/legitimate-green @@ -0,0 +1,190 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# legitimate-green — the normative decision procedure of +# squabble-contract/1.0.0, applied to a document on disk. +# +# legitimate-green bound-gate.json +# legitimate-green --expect-head-sha "$PR_HEAD_SHA" bound-gate.json +# squabble fetch owner/repo 42 \ +# | bind-gate --repo owner/repo --head-sha "$PR_HEAD_SHA" --pr 42 \ +# | legitimate-green --expect-head-sha "$PR_HEAD_SHA" +# +# Reads JSON from FILE, or from stdin when FILE is `-`. Writes ONE JSON document +# to stdout and nothing else; diagnostics go to stderr. +# +# exit 0 legitimate_green — a bound envelope whose every required check has +# the run `passed`. +# exit 3 anything else: not_green, or not_certifiable (an unbound gate, a +# verify-satisfied verdict document, an unknown document). A finding, +# not a tool failure, matching squabble's own 3/4/5 convention. +# exit 2 the tool could not do its job: bad usage, unreadable file, invalid +# JSON, more than one JSON document, jq missing. +# +# Contract revision: squabble-contract/1.0.0. See ../CONTRACT.adoc §5. +# +# This script writes nothing anywhere. It holds no token and makes no network +# call: it cannot merge, re-run, edit, dismiss or override, so no input to it can +# turn a non-green gate into a green one. + +set -euo pipefail + +readonly CONTRACT_REVISION="squabble-contract/1.0.0" +readonly EXIT_GREEN=0 +readonly EXIT_REFUSED=3 +readonly EXIT_USAGE=2 + +usage() { + printf 'usage: legitimate-green [--expect-head-sha SHA] [--expect-repo OWNER/NAME]\n' >&2 + printf ' [--allow-unbound] FILE|-\n' >&2 + printf ' --allow-unbound evaluate a bare gate document for triage; it still exits 3,\n' >&2 + printf ' because an unbound gate names no commit and cannot certify.\n' >&2 +} + +die() { + printf 'legitimate-green: %s\n' "$*" >&2 + exit "$EXIT_USAGE" +} + +# The decision procedure. `$expect_head` and `$expect_repo` are empty when +# unset; `$allow_unbound` is a boolean. Everything unknown fails closed: an +# unrecognised run value blocks, an unrecognised document shape is not +# certifiable. +read -r -d '' JQ_PROGRAM <<'JQ' || true +def reason_for: + if . == "missing" then "required check has no run bound on the head commit (nothing reported)" + elif . == "pending" then "required check has not completed" + elif . == "failed" then "required check ran and did not pass (failure, error, timeout, cancelled, startup_failure, or an unrecognised conclusion)" + elif . == "skipped" then "required check concluded skipped/neutral: GitHub accepts it for merge, but it carries no evidence" + else "unrecognised run state: fail closed" end; + +def hex40: type == "string" and test("^[0-9a-f]{40}$"); +def slug: type == "string" and test("^[^/[:space:]]+/[^/[:space:]]+$"); + +def analyse($gate): + if (($gate | type) != "object") or (($gate.checks | type) != "array") then + { shape_ok: false, requirement_count: 0, passed_evidence_count: 0, + evidence_free: [], blocking: [] } + else + [ $gate.checks[] + | { context: (if (.required_context | type) == "string" then .required_context else "" end), + run: (if (.run | type) == "string" then .run else "invalid" end) } ] as $c + | ($c | map(select(.run == "passed"))) as $ok + | ($c | map(select(.run != "passed"))) as $bad + | { shape_ok: true, + requirement_count: ($c | length), + passed_evidence_count: ($ok | length), + evidence_free: [ $bad[] | select(.run == "skipped") | .context ], + blocking: [ $bad[] | { context: .context, run: .run, reason: (.run | reason_for) } ] } + end; + +def subject_of($kind; $doc): + if $kind == "envelope" then ($doc.subject // {}) + elif $kind == "verdict" then + { repo: ($doc.repo // null), head_sha: ($doc.head_oid // null), pr: ($doc.pr // null) } + else null end; + +def subject_problems($kind; $s; $expect_head; $expect_repo): + if $kind != "envelope" then [] + else + [ if ($s | type) != "object" then "subject-invalid" else empty end, + if (($s.repo // "") | slug) | not then "subject-repo-invalid" else empty end, + if (($s.head_sha // "") | hex40) | not then "subject-head-sha-not-a-commit" else empty end, + if ((($s.pr // null) | type) == "null") + or (((($s.pr // null) | type) == "number") and (($s.pr // 0) > 0)) + then empty else "subject-pr-invalid" end, + if $expect_head != "" and (($s.head_sha // "") != $expect_head) then "head-sha-mismatch" else empty end, + if $expect_repo != "" and (($s.repo // "") != $expect_repo) then "repo-mismatch" else empty end + ] + end; + +def analyse_verdict($doc): + { shape_ok: true, requirement_count: null, passed_evidence_count: null, + evidence_free: (if ($doc.evidence_free | type) == "array" then $doc.evidence_free else [] end), + blocking: [] }; + +def kind_of($doc): + if ($doc | type) != "object" then "unknown" + elif ($doc | has("checks")) then "gate" + elif ($doc | has("gate")) and ($doc | has("subject")) then "envelope" + elif ($doc | has("done")) and ($doc | has("evidence_free")) then "verdict" + else "unknown" end; + +(if length != 1 then error("expected exactly one JSON document") else .[0] end) as $doc +| kind_of($doc) as $kind +| subject_of($kind; $doc) as $subject +| analyse(if $kind == "envelope" then $doc.gate + elif $kind == "gate" then $doc + elif $kind == "verdict" then $doc + else null end) as $a_raw +| (if $kind == "verdict" then analyse_verdict($doc) else $a_raw end) as $a +| subject_problems($kind; $subject; $expect_head; $expect_repo) as $sub +| ( [ if $kind == "unknown" then "unknown-document" else empty end, + if $kind == "verdict" then "verdict-input-cannot-certify" else empty end, + if $kind == "gate" then "unbound-gate" else empty end, + if ($kind == "gate" or $kind == "envelope") and ($a.shape_ok | not) then "gate-shape-invalid" else empty end, + if ($kind == "gate" or $kind == "envelope") and $a.requirement_count == 0 then "no-required-checks" else empty end, + $sub[] + ] | unique ) as $reasons +| ( if $kind == "verdict" or $kind == "unknown" or ($a.shape_ok | not) then "not_certifiable" + elif $kind == "gate" then "not_certifiable" + elif ($sub | length) > 0 then "not_green" + elif $a.requirement_count == 0 then "not_green" + elif ($a.blocking | length) == 0 then "legitimate_green" + else "not_green" end ) as $verdict +| { contract: "squabble-contract/1.0.0", + input: $kind, + verdict: $verdict, + legitimate_green: ($verdict == "legitimate_green"), + subject: $subject, + subject_bound: (($kind == "envelope") and (($sub | length) == 0)), + requirement_count: $a.requirement_count, + passed_evidence_count: $a.passed_evidence_count, + evidence_free: $a.evidence_free, + blocking: $a.blocking, + reasons: $reasons } +JQ + +main() { + local expect_head="" expect_repo="" allow_unbound="false" file="" arg + while [[ $# -gt 0 ]]; do + arg="$1" + case "$arg" in + --expect-head-sha) [[ $# -ge 2 ]] || die "--expect-head-sha needs a value"; expect_head="$2"; shift 2 ;; + --expect-repo) [[ $# -ge 2 ]] || die "--expect-repo needs a value"; expect_repo="$2"; shift 2 ;; + --allow-unbound) allow_unbound="true"; shift ;; + -h|--help) usage; exit 0 ;; + --) shift; [[ $# -eq 1 ]] || { usage; die "one FILE only"; }; file="$1"; shift ;; + -) [[ -z "$file" ]] || { usage; die "one FILE only"; }; file="-"; shift ;; + -*) usage; die "unknown option: $arg" ;; + *) [[ -z "$file" ]] || { usage; die "one FILE only"; }; file="$arg"; shift ;; + esac + done + [[ -n "$file" ]] || { usage; die "missing FILE"; } + command -v jq >/dev/null 2>&1 || die "jq (1.6 or later) is required" + if [[ "$file" != "-" && ! -r "$file" ]]; then + die "cannot read $file" + fi + + local out rc=0 + # --slurp so that a file holding two JSON documents is refused rather than + # silently evaluated twice; the program itself requires exactly one document. + out="$(jq --slurp \ + --arg expect_head "$expect_head" \ + --arg expect_repo "$expect_repo" \ + --argjson allow_unbound "$allow_unbound" \ + "$JQ_PROGRAM" -- "$file" 2>/dev/null)" || rc=$? + if (( rc != 0 )); then + printf 'legitimate-green: %s is not a single valid JSON document\n' "$file" >&2 + exit "$EXIT_USAGE" + fi + + printf '%s\n' "$out" + if printf '%s\n' "$out" | jq -e '.legitimate_green == true' >/dev/null 2>&1; then + exit "$EXIT_GREEN" + fi + exit "$EXIT_REFUSED" +} + +main "$@" diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-bypass.yml b/contracts/squabble/fixtures/consumer-workflow/bad-bypass.yml new file mode 100644 index 0000000..ab78510 --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-bypass.yml @@ -0,0 +1,21 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: instead of winning the gate, the workflow edits it and merges +# past it. This is the exact behaviour the contract exists to keep out of CI. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + - name: Apply the fix and land it + run: | + squabble fight --apply + gh api -X PUT repos/"$GITHUB_REPOSITORY"/branches/main/protection -f enforce_admins=false + gh pr merge --admin --squash "$PR_NUMBER" diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-masked-step.yml b/contracts/squabble/fixtures/consumer-workflow/bad-masked-step.yml new file mode 100644 index 0000000..542bc8f --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-masked-step.yml @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: the gate's failure cannot fail the job. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + - name: Decide + continue-on-error: true + run: | + legitimate-green bound-gate.json diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-moving-ref.yml b/contracts/squabble/fixtures/consumer-workflow/bad-moving-ref.yml new file mode 100644 index 0000000..43cf33f --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-moving-ref.yml @@ -0,0 +1,18 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: a helper action on a moving ref, in a workflow that otherwise +# looks pinned. A moving pin anywhere is a moving pin. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + - uses: hyperpolymath/some-helper@master + - run: squabble fetch "$GITHUB_REPOSITORY" "$PR_NUMBER" | bind-gate --repo "$GITHUB_REPOSITORY" --head-sha "$PR_HEAD_SHA" | legitimate-green diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-no-oracle.yml b/contracts/squabble/fixtures/consumer-workflow/bad-no-oracle.yml new file mode 100644 index 0000000..73ec1e8 --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-no-oracle.yml @@ -0,0 +1,18 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: gates on verify-satisfied's exit 0, i.e. on `done`, which a +# skipped required check satisfies. The workflow is read-only and pinned, and +# still makes a weaker claim than its name implies. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + - run: squabble verify-satisfied "$GITHUB_REPOSITORY" "$PR_NUMBER" diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-unpinned-action.yml b/contracts/squabble/fixtures/consumer-workflow/bad-unpinned-action.yml new file mode 100644 index 0000000..ad77594 --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-unpinned-action.yml @@ -0,0 +1,17 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: the action is called from a branch. The rules that gated the +# reviewed run are not the rules that gate the merge. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@main + - run: squabble fetch "$GITHUB_REPOSITORY" "$PR_NUMBER" | bind-gate --repo "$GITHUB_REPOSITORY" --head-sha "$PR_HEAD_SHA" | legitimate-green diff --git a/contracts/squabble/fixtures/consumer-workflow/bad-write-permission.yml b/contracts/squabble/fixtures/consumer-workflow/bad-write-permission.yml new file mode 100644 index 0000000..4718e18 --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/bad-write-permission.yml @@ -0,0 +1,17 @@ +# SPDX-License-Identifier: CC0-1.0 +# Planted defect: the job may merge, re-run and edit. Nothing in the read-only +# surface needs it; the capability exists only to be used. +name: gate +on: pull_request +permissions: + contents: read + checks: read + statuses: read + pull-requests: write + actions: read +jobs: + gate: + runs-on: ubuntu-latest + steps: + - uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + - run: squabble fetch "$GITHUB_REPOSITORY" "$PR_NUMBER" | bind-gate --repo "$GITHUB_REPOSITORY" --head-sha "$PR_HEAD_SHA" | legitimate-green diff --git a/contracts/squabble/fixtures/consumer-workflow/good-readonly.yml b/contracts/squabble/fixtures/consumer-workflow/good-readonly.yml new file mode 100644 index 0000000..d859050 --- /dev/null +++ b/contracts/squabble/fixtures/consumer-workflow/good-readonly.yml @@ -0,0 +1,73 @@ +# SPDX-License-Identifier: CC0-1.0 +# The reference consumer workflow of squabble-contract/1.0.0. +# +# Read-only: the permissions floor is six read scopes, the action is pinned to a +# commit, the contract is pinned to a commit AND checked against its SHASUMS, and +# the verdict comes from legitimate-green over a commit-bound envelope. +name: gate +on: + pull_request: + branches: [main] +permissions: + contents: read + checks: read + statuses: read + pull-requests: read + actions: read +concurrency: + group: gate-${{ github.ref }} + cancel-in-progress: true +jobs: + legitimate-green: + name: gate / legitimate-green + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - name: Checkout + uses: actions/checkout@3f9a1c4b2d5e6f708192a3b4c5d6e7f809a1b2c3 + with: + persist-credentials: false + + - name: Install pinned squabble (sha256 + build attestation) + id: squabble + uses: hyperpolymath/cicd-squabbler/.github/actions/squabble@b854d17abc0dce296719a349ebe856ff945cf03e + + - name: Pin the contract and verify its digest + env: + CONTRACT_SHA: b854d17abc0dce296719a349ebe856ff945cf03e + run: | + set -euo pipefail + git init -q .contract + git -C .contract fetch -q --depth 1 \ + https://github.com/hyperpolymath/cicd-squabbler "$CONTRACT_SHA" + git -C .contract checkout -q FETCH_HEAD + bash .contract/contracts/bin/verify-pin.sh squabble 1.0.0 \ + --repo-dir .contract/contracts >/dev/null + printf '%s\n' "$PWD/.contract/contracts/squabble/bin" >> "$GITHUB_PATH" + + - name: Sample the gate at the PR head commit + env: + GH_TOKEN: ${{ steps.app-token.outputs.token }} + PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }} + PR_NUMBER: ${{ github.event.pull_request.number }} + run: | + set -euo pipefail + squabble fetch "$GITHUB_REPOSITORY" "$PR_NUMBER" \ + | bind-gate --repo "$GITHUB_REPOSITORY" --head-sha "$PR_HEAD_SHA" --pr "$PR_NUMBER" \ + > bound-gate.json + + - name: Decide + env: + PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: | + set -euo pipefail + legitimate-green --expect-head-sha "$PR_HEAD_SHA" \ + --expect-repo "$GITHUB_REPOSITORY" bound-gate.json | tee legitimate-green.json + + - name: Upload the verdict + if: always() + uses: actions/upload-artifact@0d7fce4d1f6e5b8f0a4c3e2d1b0a9f8e7d6c5b4a + with: + name: legitimate-green + path: legitimate-green.json + if-no-files-found: error diff --git a/contracts/squabble/fixtures/envelope/all-passed.bad-subject.bound.json b/contracts/squabble/fixtures/envelope/all-passed.bad-subject.bound.json new file mode 100644 index 0000000..b113cc6 --- /dev/null +++ b/contracts/squabble/fixtures/envelope/all-passed.bad-subject.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "main", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"}] } +} diff --git a/contracts/squabble/fixtures/envelope/all-passed.wrong-head.bound.json b/contracts/squabble/fixtures/envelope/all-passed.wrong-head.bound.json new file mode 100644 index 0000000..7bb4c5f --- /dev/null +++ b/contracts/squabble/fixtures/envelope/all-passed.wrong-head.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"}] } +} diff --git a/contracts/squabble/fixtures/expectations.json b/contracts/squabble/fixtures/expectations.json new file mode 100644 index 0000000..1a41fc3 --- /dev/null +++ b/contracts/squabble/fixtures/expectations.json @@ -0,0 +1,261 @@ +{ + "contract": "squabble-contract/1.0.0", + "note": "Every case here is a claim about what the contract REFUSES. `proves` says which sentence of CONTRACT.adoc the fixture keeps honest. tests/run-conformance.sh fails unless every case ran and matched.", + "oracle": [ + { + "name": "bound envelope, every required check passed", + "file": "fixtures/gate/all-passed.bound.json", + "args": ["--expect-head-sha", "1111111111111111111111111111111111111111", "--expect-repo", "hyperpolymath/example"], + "exit": 0, + "verdict": "legitimate_green", + "legitimate_green": true, + "evidence_free": [], + "reasons": [], + "blocking_runs": [], + "proves": "The positive control: the procedure can say yes, so its refusals below mean something." + }, + { + "name": "one requirement is enough", + "file": "fixtures/gate/single-passed.bound.json", + "args": [], + "exit": 0, + "verdict": "legitimate_green", + "legitimate_green": true, + "evidence_free": [], + "reasons": [], + "blocking_runs": [], + "proves": "legitimate_green is 'all required passed', not 'at least two passed'." + }, + { + "name": "a required check never reported", + "file": "fixtures/gate/required-missing.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": [], + "blocking_runs": ["missing"], + "proves": "CONTRACT.adoc §7: the Missing deadlock — no run bound on the head commit — cannot be green." + }, + { + "name": "a required check that was skipped", + "file": "fixtures/gate/required-skipped.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": ["scan / gitleaks"], + "reasons": [], + "blocking_runs": ["skipped"], + "proves": "GitHub's ruleset accepts a skipped required check; the contract does not call that a legitimate green, and names the context in evidence_free." + }, + { + "name": "a required check that was cancelled", + "file": "fixtures/gate/required-cancelled.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": [], + "blocking_runs": ["failed"], + "proves": "CANCELLED maps to failed in the gate model, so cancelling a required check cannot read as pass or skip." + }, + { + "name": "a required check that failed", + "file": "fixtures/gate/required-failed.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": [], + "blocking_runs": ["failed"], + "proves": "An ordinary failure blocks." + }, + { + "name": "a required check still running", + "file": "fixtures/gate/required-pending.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": [], + "blocking_runs": ["pending"], + "proves": "An incomplete required check blocks — and note verify-satisfied would still call this PR `done`, which is why a verdict cannot certify green." + }, + { + "name": "a passing sibling does not launder a skip", + "file": "fixtures/gate/passed-and-skipped.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": ["scan / gitleaks"], + "reasons": [], + "blocking_runs": ["skipped"], + "proves": "Two passes and one skip is not green; evidence_free names exactly the skipped context." + }, + { + "name": "a gate with no required checks", + "file": "fixtures/gate/no-required-checks.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["no-required-checks"], + "blocking_runs": [], + "proves": "Dropping the required set is a bypass, not a win: an unprotected gate is never green." + }, + { + "name": "a run state this revision does not know", + "file": "fixtures/gate/unknown-run-state.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": [], + "blocking_runs": ["neutral"], + "proves": "Vocabulary drift (e.g. NEUTRAL leaking into the gate instead of mapping to skipped) fails closed rather than defaulting to passed." + }, + { + "name": "an unbound gate cannot certify (with --allow-unbound)", + "file": "fixtures/gate/all-passed.unbound.json", + "args": ["--allow-unbound"], + "exit": 3, + "verdict": "not_certifiable", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["unbound-gate"], + "blocking_runs": [], + "proves": "Correct-looking evidence with no commit binding can be replayed, so it never certifies — the flag permits evaluation, not a green." + }, + { + "name": "an unbound gate cannot certify (without the flag)", + "file": "fixtures/gate/all-passed.unbound.json", + "args": [], + "exit": 3, + "verdict": "not_certifiable", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["unbound-gate"], + "blocking_runs": [], + "proves": "The same document is refused identically with and without the flag: no flag path reaches green." + }, + { + "name": "evidence for a different head commit", + "file": "fixtures/envelope/all-passed.wrong-head.bound.json", + "args": ["--expect-head-sha", "2222222222222222222222222222222222222222"], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["head-sha-mismatch"], + "blocking_runs": [], + "proves": "A replayed envelope from another commit is refused by --expect-head-sha." + }, + { + "name": "a branch name instead of a commit", + "file": "fixtures/envelope/all-passed.bad-subject.bound.json", + "args": [], + "exit": 3, + "verdict": "not_green", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["subject-head-sha-not-a-commit"], + "blocking_runs": [], + "proves": "head_sha: \"main\" is a moving pin and is refused; the envelope must name a commit." + }, + { + "name": "a verdict with an evidence-free required check", + "file": "fixtures/verdict/done-with-skipped.json", + "args": [], + "exit": 3, + "verdict": "not_certifiable", + "legitimate_green": false, + "evidence_free": ["scan / gitleaks"], + "reasons": ["verdict-input-cannot-certify"], + "blocking_runs": [], + "proves": "done: true with a skipped required check is the mergeable-but-evidence-free case, and is refused." + }, + { + "name": "a clean verdict is still not a green claim", + "file": "fixtures/verdict/done-clean.json", + "args": [], + "exit": 3, + "verdict": "not_certifiable", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["verdict-input-cannot-certify"], + "blocking_runs": [], + "proves": "Even done: true with no evidence-free context cannot certify: the document carries no per-requirement run states." + }, + { + "name": "a verdict that is not done", + "file": "fixtures/verdict/not-done.json", + "args": [], + "exit": 3, + "verdict": "not_certifiable", + "legitimate_green": false, + "evidence_free": [], + "reasons": ["verdict-input-cannot-certify"], + "blocking_runs": [], + "proves": "The negative control for the previous case: refusal is not merely 'done is true'." + } + ], + "audit": [ + { + "name": "the reference read-only consumer", + "file": "fixtures/consumer-workflow/good-readonly.yml", + "exit": 0, + "codes": [], + "proves": "The audit can pass a workflow that does the contract's thing, so its refusals below mean something." + }, + { + "name": "the action on a moving branch", + "file": "fixtures/consumer-workflow/bad-unpinned-action.yml", + "exit": 3, + "codes": ["E-UNPINNED-ACTION"], + "proves": "A branch ref means the reviewed rules are not the merged rules." + }, + { + "name": "a helper action on a moving ref", + "file": "fixtures/consumer-workflow/bad-moving-ref.yml", + "exit": 3, + "codes": ["E-MOVING-REF"], + "proves": "One moving pin anywhere is a moving pin, even beside a correctly pinned action." + }, + { + "name": "a job that may write", + "file": "fixtures/consumer-workflow/bad-write-permission.yml", + "exit": 3, + "codes": ["E-WRITE-PERMISSION"], + "proves": "No write scope is needed by the read-only surface; an unused capability is a bypass waiting to be armed." + }, + { + "name": "a step whose failure cannot fail the job", + "file": "fixtures/consumer-workflow/bad-masked-step.yml", + "exit": 3, + "codes": ["E-MASKED-STEP"], + "proves": "continue-on-error on the deciding step turns the gate into decoration." + }, + { + "name": "the workflow edits the gate and merges past it", + "file": "fixtures/consumer-workflow/bad-bypass.yml", + "exit": 3, + "codes": ["E-BYPASS-COMMAND", "E-OUT-OF-CONTRACT-SUBCOMMAND"], + "proves": "squabble ≠ bypass: fight --apply, an enforce_admins write and gh pr merge --admin are all refused." + }, + { + "name": "gating on done instead of on evidence", + "file": "fixtures/consumer-workflow/bad-no-oracle.yml", + "exit": 3, + "codes": ["E-NO-ORACLE"], + "proves": "A pinned, read-only workflow that gates on verify-satisfied's exit 0 is still making a weaker claim than its name implies." + } + ] +} diff --git a/contracts/squabble/fixtures/gate/all-passed.bound.json b/contracts/squabble/fixtures/gate/all-passed.bound.json new file mode 100644 index 0000000..3572a60 --- /dev/null +++ b/contracts/squabble/fixtures/gate/all-passed.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"scan / gitleaks","run":"passed"}] } +} diff --git a/contracts/squabble/fixtures/gate/all-passed.unbound.json b/contracts/squabble/fixtures/gate/all-passed.unbound.json new file mode 100644 index 0000000..54e4f07 --- /dev/null +++ b/contracts/squabble/fixtures/gate/all-passed.unbound.json @@ -0,0 +1 @@ +{ "checks": [ { "required_context": "ci / test", "run": "passed" } ] } diff --git a/contracts/squabble/fixtures/gate/no-required-checks.bound.json b/contracts/squabble/fixtures/gate/no-required-checks.bound.json new file mode 100644 index 0000000..3bf5d2b --- /dev/null +++ b/contracts/squabble/fixtures/gate/no-required-checks.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [] } +} diff --git a/contracts/squabble/fixtures/gate/passed-and-skipped.bound.json b/contracts/squabble/fixtures/gate/passed-and-skipped.bound.json new file mode 100644 index 0000000..3976e0f --- /dev/null +++ b/contracts/squabble/fixtures/gate/passed-and-skipped.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"ci / lint","run":"passed"},{"required_context":"scan / gitleaks","run":"skipped"}] } +} diff --git a/contracts/squabble/fixtures/gate/required-cancelled.bound.json b/contracts/squabble/fixtures/gate/required-cancelled.bound.json new file mode 100644 index 0000000..8214dbe --- /dev/null +++ b/contracts/squabble/fixtures/gate/required-cancelled.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"ci / integration","run":"failed"}] } +} diff --git a/contracts/squabble/fixtures/gate/required-failed.bound.json b/contracts/squabble/fixtures/gate/required-failed.bound.json new file mode 100644 index 0000000..10c4727 --- /dev/null +++ b/contracts/squabble/fixtures/gate/required-failed.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [ { "required_context": "ci / integration", "run": "failed" } ] } +} diff --git a/contracts/squabble/fixtures/gate/required-missing.bound.json b/contracts/squabble/fixtures/gate/required-missing.bound.json new file mode 100644 index 0000000..c00d435 --- /dev/null +++ b/contracts/squabble/fixtures/gate/required-missing.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"scan / gitleaks","run":"missing","missing_cause":"dead_action_pin"}] } +} diff --git a/contracts/squabble/fixtures/gate/required-pending.bound.json b/contracts/squabble/fixtures/gate/required-pending.bound.json new file mode 100644 index 0000000..3c277c5 --- /dev/null +++ b/contracts/squabble/fixtures/gate/required-pending.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"ci / integration","run":"pending"}] } +} diff --git a/contracts/squabble/fixtures/gate/required-skipped.bound.json b/contracts/squabble/fixtures/gate/required-skipped.bound.json new file mode 100644 index 0000000..ec5eea5 --- /dev/null +++ b/contracts/squabble/fixtures/gate/required-skipped.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"scan / gitleaks","run":"skipped"}] } +} diff --git a/contracts/squabble/fixtures/gate/single-passed.bound.json b/contracts/squabble/fixtures/gate/single-passed.bound.json new file mode 100644 index 0000000..7bb4c5f --- /dev/null +++ b/contracts/squabble/fixtures/gate/single-passed.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"}] } +} diff --git a/contracts/squabble/fixtures/gate/unknown-run-state.bound.json b/contracts/squabble/fixtures/gate/unknown-run-state.bound.json new file mode 100644 index 0000000..2d1aaf9 --- /dev/null +++ b/contracts/squabble/fixtures/gate/unknown-run-state.bound.json @@ -0,0 +1,5 @@ +{ + "contract": "squabble-contract/1.0.0", + "subject": { "repo": "hyperpolymath/example", "head_sha": "1111111111111111111111111111111111111111", "pr": 42 }, + "gate": { "checks": [{"required_context":"ci / test","run":"passed"},{"required_context":"scan / gitleaks","run":"neutral"}] } +} diff --git a/contracts/squabble/fixtures/verdict/done-clean.json b/contracts/squabble/fixtures/verdict/done-clean.json new file mode 100644 index 0000000..a854d81 --- /dev/null +++ b/contracts/squabble/fixtures/verdict/done-clean.json @@ -0,0 +1,11 @@ +{ + "repo": "hyperpolymath/example", + "pr": 42, + "head_oid": "1111111111111111111111111111111111111111", + "base_ref": "main", + "done": true, + "agent_items": [], + "held_by_human": [], + "evidence_free": [], + "notes": ["code-scanning alerts introduced by this PR are NOT yet evaluated"] +} diff --git a/contracts/squabble/fixtures/verdict/done-with-skipped.json b/contracts/squabble/fixtures/verdict/done-with-skipped.json new file mode 100644 index 0000000..4957856 --- /dev/null +++ b/contracts/squabble/fixtures/verdict/done-with-skipped.json @@ -0,0 +1,11 @@ +{ + "repo": "hyperpolymath/example", + "pr": 42, + "head_oid": "1111111111111111111111111111111111111111", + "base_ref": "main", + "done": true, + "agent_items": [], + "held_by_human": [], + "evidence_free": ["scan / gitleaks"], + "notes": [] +} diff --git a/contracts/squabble/fixtures/verdict/not-done.json b/contracts/squabble/fixtures/verdict/not-done.json new file mode 100644 index 0000000..c149309 --- /dev/null +++ b/contracts/squabble/fixtures/verdict/not-done.json @@ -0,0 +1,14 @@ +{ + "repo": "hyperpolymath/example", + "pr": 42, + "head_oid": "1111111111111111111111111111111111111111", + "base_ref": "main", + "done": false, + "agent_items": [ + { "kind": "required_not_satisfied", "context": "ci / test", "run": "failed" }, + { "kind": "unresolved_thread", "id": "PRRT_1", "author": "reviewer", "path": "src/lib.rs", "outdated": false, "url": "https://example.invalid/1" } + ], + "held_by_human": [], + "evidence_free": [], + "notes": [] +} diff --git a/contracts/squabble/schema/envelope.schema.json b/contracts/squabble/schema/envelope.schema.json new file mode 100644 index 0000000..0f575b4 --- /dev/null +++ b/contracts/squabble/schema/envelope.schema.json @@ -0,0 +1,27 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://github.com/hyperpolymath/cicd-squabbler/contracts/squabble/schema/envelope.schema.json", + "title": "commit-bound gate envelope (squabble-contract/1.0.0)", + "description": "A gate document plus the commit it was sampled at. The ONLY input from which legitimately-green can be certified. Produced by contracts/squabble/bin/bind-gate.", + "type": "object", + "additionalProperties": false, + "required": ["contract", "subject", "gate"], + "properties": { + "contract": { "const": "squabble-contract/1.0.0" }, + "subject": { + "type": "object", + "additionalProperties": false, + "required": ["repo", "head_sha"], + "properties": { + "repo": { "type": "string", "pattern": "^[^/[[:space:]]+/[^/[:space:]]+$" }, + "head_sha": { + "type": "string", + "pattern": "^[0-9a-f]{40}$", + "description": "The head commit the gate was sampled at. Never a branch name: a branch is a moving pin." + }, + "pr": { "type": ["integer", "null"], "minimum": 1 } + } + }, + "gate": { "$ref": "gate.schema.json" } + } +} diff --git a/contracts/squabble/schema/gate.schema.json b/contracts/squabble/schema/gate.schema.json new file mode 100644 index 0000000..cc01f80 --- /dev/null +++ b/contracts/squabble/schema/gate.schema.json @@ -0,0 +1,37 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://github.com/hyperpolymath/cicd-squabbler/contracts/squabble/schema/gate.schema.json", + "title": "squabble gate document (squabble-contract/1.0.0)", + "description": "The document `squabble fetch / ` writes to stdout. One entry per required context, with the run bound to it on the head commit. A context whose run is `passed` is the only evidence-bearing satisfied state.", + "type": "object", + "additionalProperties": false, + "required": ["checks"], + "properties": { + "checks": { + "type": "array", + "description": "The required-context set. An empty array is a valid document and is NEVER green: an unprotected gate is Blocked, not won.", + "items": { + "type": "object", + "additionalProperties": false, + "required": ["required_context", "run"], + "properties": { + "required_context": { + "type": "string", + "minLength": 1, + "description": "The exact, case-sensitive context name the branch ruleset requires." + }, + "run": { + "type": "string", + "enum": ["missing", "pending", "failed", "skipped", "passed"], + "description": "The realised run. CANCELLED/TIMED_OUT/STARTUP_FAILURE/ERROR/ACTION_REQUIRED/STALE and unrecognised conclusions map to `failed`. SKIPPED/NEUTRAL map to `skipped`: the ruleset accepts it, no evidence is carried." + }, + "missing_cause": { + "type": ["string", "null"], + "enum": ["no_such_job", "dead_action_pin", "actions_policy_refusal", "empty_jobs_map", "not_triggered_on_pull_request", "unknown", null], + "description": "Why a context is `missing`. Diagnosis only: it never changes `run` and never moves the gate state." + } + } + } + } + } +} diff --git a/contracts/squabble/schema/legitimate-green.schema.json b/contracts/squabble/schema/legitimate-green.schema.json new file mode 100644 index 0000000..76b7515 --- /dev/null +++ b/contracts/squabble/schema/legitimate-green.schema.json @@ -0,0 +1,135 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://github.com/hyperpolymath/cicd-squabbler/contracts/squabble/schema/legitimate-green.schema.json", + "title": "legitimate-green verdict document (squabble-contract/1.0.0)", + "description": "The single JSON document contracts/squabble/bin/legitimate-green writes. Deterministic: no timestamps, no ordering by map iteration. `legitimate_green` is the only field a consumer may gate on, and it is true only for a bound envelope whose every required check has run `passed`.", + "type": "object", + "additionalProperties": false, + "required": [ + "contract", + "input", + "verdict", + "legitimate_green", + "subject", + "subject_bound", + "requirement_count", + "passed_evidence_count", + "evidence_free", + "blocking", + "reasons" + ], + "properties": { + "contract": { + "const": "squabble-contract/1.0.0" + }, + "input": { + "enum": [ + "envelope", + "gate", + "verdict", + "unknown" + ] + }, + "verdict": { + "enum": [ + "legitimate_green", + "not_green", + "not_certifiable" + ] + }, + "legitimate_green": { + "type": "boolean" + }, + "subject": { + "type": [ + "object", + "null" + ], + "properties": { + "repo": { + "type": [ + "string", + "null" + ] + }, + "head_sha": { + "type": [ + "string", + "null" + ] + }, + "pr": { + "type": [ + "integer", + "null" + ] + } + } + }, + "subject_bound": { + "type": "boolean" + }, + "requirement_count": { + "type": [ + "integer", + "null" + ], + "minimum": 0, + "description": "null when the input is a verify-satisfied verdict, which carries no per-requirement run states: a number there would be invented." + }, + "passed_evidence_count": { + "type": [ + "integer", + "null" + ], + "minimum": 0, + "description": "null when the input is a verify-satisfied verdict, which carries no per-requirement run states: a number there would be invented." + }, + "evidence_free": { + "type": "array", + "items": { + "type": "string" + } + }, + "blocking": { + "type": "array", + "items": { + "type": "object", + "required": [ + "context", + "run", + "reason" + ], + "properties": { + "context": { + "type": "string" + }, + "run": { + "type": "string" + }, + "reason": { + "type": "string" + } + } + } + }, + "reasons": { + "type": "array", + "items": { + "enum": [ + "unknown-document", + "verdict-input-cannot-certify", + "unbound-gate", + "gate-shape-invalid", + "no-required-checks", + "subject-invalid", + "subject-repo-invalid", + "subject-head-sha-not-a-commit", + "subject-pr-invalid", + "head-sha-mismatch", + "repo-mismatch" + ] + } + } + } +} diff --git a/contracts/squabble/schema/verdict.schema.json b/contracts/squabble/schema/verdict.schema.json new file mode 100644 index 0000000..0227c8f --- /dev/null +++ b/contracts/squabble/schema/verdict.schema.json @@ -0,0 +1,35 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://github.com/hyperpolymath/cicd-squabbler/contracts/squabble/schema/verdict.schema.json", + "title": "squabble verify-satisfied report (squabble-contract/1.0.0)", + "description": "The JSON `squabble verify-satisfied` writes to stdout. It answers 'is there agent work left', NOT 'is this a legitimate green': it carries no per-requirement run states, and a pending required check is not an agent item. This document can never certify green.", + "type": "object", + "additionalProperties": false, + "required": ["repo", "pr", "head_oid", "base_ref", "done", "agent_items", "held_by_human", "evidence_free", "notes"], + "properties": { + "repo": { "type": "string", "pattern": "^[^/[[:space:]]+/[^/[:space:]]+$" }, + "pr": { "type": "integer", "minimum": 1 }, + "head_oid": { "type": "string", "minLength": 1 }, + "base_ref": { "type": "string", "minLength": 1 }, + "done": { "type": "boolean" }, + "agent_items": { + "type": "array", + "items": { + "type": "object", + "required": ["kind"], + "properties": { + "kind": { + "enum": ["conflicting", "mergeability_unknown", "draft", "required_not_satisfied", "check_failed", "unresolved_thread", "changes_requested", "review_bot_pending", "auto_merge_not_armed", "wrong_merge_method", "branch_behind", "merge_queue", "unverified_commits", "awaiting_approval", "awaiting_deployment", "awaiting_human_merge"] + } + } + } + }, + "held_by_human": { "type": "array", "items": { "type": "object", "required": ["kind"] } }, + "evidence_free": { + "type": "array", + "items": { "type": "string" }, + "description": "Required contexts satisfied by a skipped/neutral run. Non-empty means the merge would be ruleset-legitimate and evidence-free." + }, + "notes": { "type": "array", "items": { "type": "string" } } + } +} diff --git a/contracts/squabble/tests/run-conformance.sh b/contracts/squabble/tests/run-conformance.sh new file mode 100755 index 0000000..5999a5b --- /dev/null +++ b/contracts/squabble/tests/run-conformance.sh @@ -0,0 +1,206 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# run-conformance.sh — prove squabble-contract/1.0.0 with fixtures. +# +# Every case in fixtures/expectations.json is run against the published +# artefacts and its exit code, verdict, evidence_free list, reasons and blocking +# runs are compared. Three further cases check the revision marker, the +# determinism of the verdict document, and the SHASUMS manifest. +# +# bash contracts/squabble/tests/run-conformance.sh +# +# Needs bash, coreutils and jq (1.6+). No network, no token, no Rust toolchain — +# which is what makes it runnable in a consumer's CI as well as here. +# +# Exit codes: 0 every planned case ran and passed, 1 a case failed or did not +# run, 2 the suite could not start (missing jq, missing fixture set). + +set -euo pipefail + +readonly CONTRACT="squabble-contract/1.0.0" +SUITE_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +EXPECT="${SUITE_DIR}/fixtures/expectations.json" +ORACLE="${SUITE_DIR}/bin/legitimate-green" +AUDIT="${SUITE_DIR}/bin/audit-consumer-workflow.sh" +MAKE_SUMS="${SUITE_DIR}/../bin/make-shasums.sh" + +for tool in jq bash; do + command -v "$tool" >/dev/null 2>&1 || { printf 'missing required tool: %s\n' "$tool" >&2; exit 2; } +done +[[ -r "$EXPECT" ]] || { printf 'missing %s\n' "$EXPECT" >&2; exit 2; } +[[ -x "$ORACLE" ]] || { printf '%s is not executable\n' "$ORACLE" >&2; exit 2; } +[[ -r "$AUDIT" ]] || { printf 'missing %s\n' "$AUDIT" >&2; exit 2; } + +passed=0 +failed=0 +ran=0 + +ok() { printf 'ok %s\n' "$1"; passed=$((passed + 1)); } +bad() { printf 'FAIL %s: %s\n' "$1" "$2"; failed=$((failed + 1)); } + +# expect_eq NAME WANT GOT +expect_eq() { + local name="$1" want="$2" got="$3" + if [[ "$want" == "$got" ]]; then + return 0 + fi + bad "$name" "expected <$want>, got <$got>" + return 1 +} + +oracle_case() { + local i="$1" + local name file want_exit out rc=0 + name="$(jq -r ".oracle[$i].name" "$EXPECT")" + file="$(jq -r ".oracle[$i].file" "$EXPECT")" + want_exit="$(jq -r ".oracle[$i].exit" "$EXPECT")" + local -a args=() + while IFS= read -r a; do args+=("$a"); done < <(jq -r ".oracle[$i].args[]?" "$EXPECT") + + ran=$((ran + 1)) + out="$("$ORACLE" "${args[@]+"${args[@]}"}" "$SUITE_DIR/$file" 2>/dev/null)" || rc=$? + + local problem="" + if [[ "$rc" != "$want_exit" ]]; then + problem="exit $rc, expected $want_exit" + elif ! printf '%s' "$out" | jq -e . >/dev/null 2>&1; then + problem="stdout is not JSON" + else + local want_verdict got_verdict want_lg got_lg + want_verdict="$(jq -r ".oracle[$i].verdict" "$EXPECT")" + got_verdict="$(printf '%s' "$out" | jq -r '.verdict')" + want_lg="$(jq -r ".oracle[$i].legitimate_green" "$EXPECT")" + got_lg="$(printf '%s' "$out" | jq -r '.legitimate_green')" + local want_block got_block want_ef got_ef want_reasons got_reasons + want_block="$(jq -c '.oracle['"$i"'].blocking_runs | sort' "$EXPECT")" + got_block="$(printf '%s' "$out" | jq -c '[.blocking[].run] | sort')" + want_ef="$(jq -c '.oracle['"$i"'].evidence_free | sort' "$EXPECT")" + got_ef="$(printf '%s' "$out" | jq -c '.evidence_free | sort')" + want_reasons="$(jq -c '.oracle['"$i"'].reasons | sort' "$EXPECT")" + got_reasons="$(printf '%s' "$out" | jq -c '.reasons | sort')" + + if [[ "$want_verdict" != "$got_verdict" ]]; then + problem="verdict <$got_verdict>, expected <$want_verdict>" + elif [[ "$want_lg" != "$got_lg" ]]; then + problem="legitimate_green <$got_lg>, expected <$want_lg>" + elif [[ "$want_block" != "$got_block" ]]; then + problem="blocking runs <$got_block>, expected <$want_block>" + elif [[ "$want_ef" != "$got_ef" ]]; then + problem="evidence_free <$got_ef>, expected <$want_ef>" + elif [[ "$want_reasons" != "$got_reasons" ]]; then + problem="reasons <$got_reasons>, expected <$want_reasons>" + elif [[ "$(printf '%s' "$out" | jq -r '.contract')" != "$CONTRACT" ]]; then + problem="output names contract $(printf '%s' "$out" | jq -r '.contract'), expected $CONTRACT" + elif [[ "$want_lg" == "false" && "$rc" == "0" ]]; then + problem="a non-green verdict exited 0" + fi + fi + + if [[ -z "$problem" ]]; then + printf 'ok oracle: %s\n' "$name" + passed=$((passed + 1)) + else + printf 'FAIL oracle: %s: %s\n' "$name" "$problem" + failed=$((failed + 1)) + fi +} + +audit_case() { + local i="$1" + local name file want_exit out rc=0 + name="$(jq -r ".audit[$i].name" "$EXPECT")" + file="$(jq -r ".audit[$i].file" "$EXPECT")" + want_exit="$(jq -r ".audit[$i].exit" "$EXPECT")" + + ran=$((ran + 1)) + out="$(bash "$AUDIT" "$SUITE_DIR/$file" 2>/dev/null)" || rc=$? + + local problem="" + if [[ "$rc" != "$want_exit" ]]; then + problem="exit $rc, expected $want_exit" + else + local code + while IFS= read -r code; do + [[ -z "$code" ]] && continue + if ! printf '%s\n' "$out" | grep -qE "^${code}([[:space:]]|$)"; then + problem="missing finding $code" + break + fi + done < <(jq -r ".audit[$i].codes[]?" "$EXPECT") + if [[ -z "$problem" && "$want_exit" == "0" && -n "$out" ]]; then + problem="clean case produced findings: $out" + fi + fi + + if [[ -z "$problem" ]]; then + printf 'ok audit: %s\n' "$name" + passed=$((passed + 1)) + else + printf 'FAIL audit: %s: %s\n' "$name" "$problem" + failed=$((failed + 1)) + fi +} + +main() { + local n i + + n="$(jq -r '.oracle | length' "$EXPECT")" + for ((i = 0; i < n; i++)); do oracle_case "$i"; done + + n="$(jq -r '.audit | length' "$EXPECT")" + for ((i = 0; i < n; i++)); do audit_case "$i"; done + + # ── the revision marker, and the document it produces ────────────────── + ran=$((ran + 1)) + if [[ "$(head -n 1 "$SUITE_DIR/REVISION" | tr -d '\r')" == "$CONTRACT" ]]; then + printf 'ok revision: REVISION names %s\n' "$CONTRACT" + passed=$((passed + 1)) + else + printf 'FAIL revision: REVISION is %s, expected %s\n' \ + "$(head -n 1 "$SUITE_DIR/REVISION")" "$CONTRACT" + failed=$((failed + 1)) + fi + + # ── determinism: the verdict document is byte-identical across runs ───── + ran=$((ran + 1)) + local a b + a="$("$ORACLE" "$SUITE_DIR/fixtures/gate/all-passed.bound.json" 2>/dev/null)" || true + b="$("$ORACLE" "$SUITE_DIR/fixtures/gate/all-passed.bound.json" 2>/dev/null)" || true + if [[ -n "$a" && "$a" == "$b" ]]; then + printf 'ok determinism: two runs produced identical documents\n' + passed=$((passed + 1)) + else + printf 'FAIL determinism: two runs of the same fixture differ\n' + failed=$((failed + 1)) + fi + + # ── the manifest: published bytes have not drifted ───────────────────── + ran=$((ran + 1)) + if bash "$MAKE_SUMS" "$SUITE_DIR" --check 2>/dev/null; then + printf 'ok manifest: SHASUMS matches every published file\n' + passed=$((passed + 1)) + else + printf 'FAIL manifest: SHASUMS does not match the files on disk\n' + failed=$((failed + 1)) + fi + + local planned + planned=$(( $(jq -r '.oracle | length' "$EXPECT") + $(jq -r '.audit | length' "$EXPECT") + 3 )) + + printf '\n%d passed, %d failed, %d/%d planned cases ran\n' \ + "$passed" "$failed" "$ran" "$planned" + if [[ "$failed" != "0" ]]; then + printf 'conformance: FAILED\n' >&2 + exit 1 + fi + if [[ "$ran" != "$planned" ]]; then + printf 'conformance: REFUSED — %d of %d planned cases ran; a case that does not run is not a pass\n' \ + "$ran" "$planned" >&2 + exit 1 + fi + printf 'conformance: %s OK\n' "$CONTRACT" +} + +main "$@" diff --git a/docs/README.adoc b/docs/README.adoc index d25a192..419c401 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -10,6 +10,11 @@ Primary tracks: * `whitepapers/academic/` for research-facing whitepapers * `whitepapers/industry/` for industry/outreach whitepapers +Downstream integration contracts (published revisions, not branches): + +* `../contracts/squabble/CONTRACT.adoc` — `squabble-contract/1.0.0` +* `../contracts/proven-tests/EVIDENCE-CONTRACT.adoc` — `proven-tests-evidence/1.0.0` + Core docs: * `maintenance/MAINTENANCE-CHECKLIST.md`