A standalone, per-repo CI/CD fighter that drives a stuck pipeline to a legitimate green — or improves red→yellow, or fails and hands the human a structured report. It wins the gate; it never cheats past it.
|
Note
|
Status — v0.1 in active development (updated 2026-10-28). The engine and
its formal invariant are real and verified (see below); live gate fetch via gh
landed in #6; squabble fight (classify each red as self-win | escalate |
assign-owner), the squabble-app loopback HTTP backend, and the boj-server
expert summoning (--summon, feature boj) landed in #13. squabble fight
--apply now enacts the first appliable self-win — stripping an on..paths
trigger filter that strands a required check — by writing the workflow file
(propose remains the default; --apply never commits, pushes, or re-runs CI).
The fetch reads *both gate surfaces — branch rulesets AND classic branch
protection (#100) — and probes the repository’s Actions permissions whenever a
required context refuses to start, so a STARTUP_FAILURE is attributed to the
posture that caused it rather than to the reusable’s owner or a security scan
(#15). Still open: applying the other self-wins (required-context reconcile,
reusable-workflow re-pin — these need the GitHub ruleset API / a target SHA) and
the GitHub App webhook leg (pending the owner’s hosting decision). Zero-job
startup_failure runs — no job, therefore no check run, therefore nothing in a
PR check list — are now first-class: squabble zero-job attempts to attribute
each observed run to a moved coordinate or an allow-list gap, and reports
Unattributed — with the probe failure quoted, and exit 4 — when the evidence
does not support a class; squabble chains compares
canonical upstream names through REST so a move is named before a run proves
it. Both are diagnosis only; squabble ≠ bypass still holds. See
docs/CHARTER.adoc for the design and open owner decisions.
|
- Chains: cross-repo CI dependencies (read-only)
- Zero-job startup failures: the CI that never reports
- Where a run stopped: preflight is not a finding
- Rust deductive verification (Creusot)
- Downstream integration contracts (pinned, immutable revisions)
- Core principle: squabble ≠ bypass
- What’s in the box
- Verify it yourself
- The v0.1 fight playbook (gate-deadlock class only)
- Licensing
squabble chains maps which repos' CI depends on which, through reusable
workflows and pinned actions. Nothing is written anywhere.
squabble chains . ../standards gh:hyperpolymath/typed-wasm --follow 1-
Blocking (exit 4): dependency cycles, dead upstreams, and moved upstream coordinates confirmed in requested subjects or through exact pinned dependency routes. A deleted reusable workflow can fail before any job reports.
-
Warnings: diamonds (one repo’s CI receives an upstream at two pins, one of them via a reusable workflow), pin skew across repos, and tag/branch pins.
-
It also prints an upstreams-first landing order and the longest chain.
Every upstream coordinate is resolved through REST with redirects followed, and
its canonical full_name is compared with the name as written — names, never
pins. A difference is reported as a moved upstream: a reusable coordinate under
a renamed/transferred owner can die as a zero-job startup_failure ("workflow
was not found") that no PR check list shows, so it is named before CI goes
quiet. A confirmed reference blocks even when the repository API follows a
redirect: Actions does not redirect the uses: reference. A reference found
only on an upstream’s default branch remains an unconfirmed warning unless
every hop from a requested subject matches the scanned revision and called
workflow file. The report retains both confirmed and unconfirmed locations.
squabble zero-job separately reports
the failed runs that were actually observed. The same canonicalisation groups
pin skew, so the old and new
spellings of one upstream cannot hide a split. --no-canonical skips the REST
reads and says so — a deliberate blind spot, not a clean bill.
An upstream that was never probed is listed on the frontier, not assumed
healthy. See docs/proposals/squabble-modes-and-app-layer.adoc for where
this is heading: upstream conformance, custodian rulesets, and the app-aware
layer.
Some workflows fail before any job exists. GitHub creates no check run, the PR check list stays tidy, and a required context is simply absent. Two first-class coordinate classes are modelled, each with its own move. Optional native lock verification adds source diagnoses which never propose permission changes:
| Class | Move | What it means |
|---|---|---|
moved coordinate |
|
A reusable coordinate names an owner/repo that was renamed or transferred. Repoint to the canonical name carrying the same pin — repointing is not re-pinning, and no pin is ever resolved on the way. |
allow-list admission required |
|
The coordinate (or its canonical target) is refused by the caller’s
|
invalid native Actions lock |
Diagnosis only |
The official native parser rejected the lock at the failed run’s exact source revision. Retain its exit and diagnostic, then review a candidate produced by the repository’s official regeneration chain. |
Actions lock/workflow mismatch |
Diagnosis only |
The official offline verifier reported coverage findings for this workflow at the failed run’s exact source revision. This is separate from malformed lock syntax and from a tool or setup failure. |
squabble zero-job . --limit 30 # attribute the latest zero-job runs
squabble zero-job . --limit 30 --json # the same, machine-readable
squabble zero-job . --actions-lock-verifier /verified/gh-actions-lock --jsonPer run it reports the repo, the workflow, the coordinate as written, the
canonical target, and the required allow-list pattern — plus the sequencing: fix
the repoint first, then admit the canonical pattern if the run is still refused.
Both startup_failure and ordinary failure conclusions are investigated;
GitHub reports both for runs which created no jobs. The jobs endpoint must
independently establish a zero count before source attribution. Ordinary
failures with observed jobs belong to execution-phase diagnosis. Unreadable
counts and contradictory startup evidence remain visible and blocking without
inventing a zero count or proposing a repair.
The run’s full commit ID must match the local repository root and its
unmodified workflow tree. A different revision, nested directory, unreadable
source, or changed workflow stays Unattributed; a current checkout cannot
explain a historical run by coincidence. Exit 4 means a failed candidate
remains in the report, attributed or not. Exit 0 speaks only for the scanned
window.
--actions-lock-verifier takes an absolute path to an independently verified
official gh-actions-lock v0.2.0 binary. It invokes only --version and
--verify-local --json --hostname github.com: no download, resolution, auth,
network request or write mode. Tokens and subject-override environment variables
are removed from that child process. The JSON report retains the tool version,
exact source, exit, stdout, stderr and classification.
The native probe requires a pristine full checkout, including ignored and
untracked files, with no symlink/gitlink inputs or hidden index changes. Use a
fresh checkout at the failed run’s commit. This stricter opt-in requirement
includes same-repository $/… action definitions outside workflows: an
ignored action.yml can shadow a committed action.yaml. If that complete
input set cannot be bound to the source, the probe is explicitly unverified.
The command never removes or changes a dirty file to meet the requirement.
An unavailable optional lock probe is retained beside any independently
established coordinate attribution; it neither hides that diagnosis nor
establishes a lock repair or a successful verification.
The native reader checks the official exit/JSON contract and complete workflow population. Empty, malformed, partial, duplicate-key, contradictory or unknown verifier-version output cannot become verified. A local verification pass is coverage evidence only; a reproduced source defect is not proof of the sole GitHub startup cause. Neither is a CI pass, repair outcome or training success.
zero-job is outside squabble-contract/1.0.0: that revision’s surface stays
at four subcommands, and nothing here adds meaning to it. Like chains, the
command is read-only and writes nothing, so its absence from the pinned
contract costs a consumer nothing.
Both moves only let a check start. Neither drops a required context, weakens a
check, nor edits settings: squabble ≠ bypass holds, and nothing here is a
green. A missing or skipped check cannot be made green by a diagnosis.
A red check says that a run failed; it never says whether the policy ran. A job that dies in runner setup, provisioning or lock resolution is not a verdict on the code, and attributing it by the workflow’s shape dispatches work nobody can do.
gh api repos/o/r/actions/jobs/12345 > job.json
squabble phase job.json --repo . # class · step · handoff · ownersquabble phase classifies step evidence into the outcomes an estate report must
keep distinct — not started (zero jobs: attributed by zero-job/chains),
preflight, prerequisite missing, policy step failed (where, never why: read
the policy’s own report), and verified (still subject to polarity’s vacuity
check) — or refuses with a reason (`Unclassified). Step names live in
.machine_readable/bot_directives/execution_taxonomy.a2ml, never in the engine.
No class constructs a check, drops a context or reaches green: squabble ≠
bypass holds, and phase has no exit code that means green.
The role, ownership map, gaps and handoffs across cicd-suite, standards,
reposystem, proven-tests-and-benches, Hypatia and gitbot-fleet:
docs/reports/estate-integration/2026-10-31-ci-diagnosis-coverage.adoc.
The estate requires its Rust to carry verification obligations, the twin of the
SPARK proofs. verification/squabble-creusot states the engine’s load-bearing
invariants — acceptance ⇔ every requirement satisfied and the set non-empty, a
skip is not evidence, no diagnosis is a green, admission is refused exactly when
it is required, a repoint carries the pin verbatim — to
Creusot, and mirrors them as ordinary
`#[test]`s against the real code so drift is caught on stable Rust.
just verify-status # which toolchain and prover are present
just verify-install # stable + Creusot's pinned nightly + Creusot itself
just verify-mirror # stable Rust: the model vs the real engine
just verify-creusot # the prover: discharge the obligationsHosted proof recorded for an exact source revision. On 2026-11-04,
job 126852164109
rejected the planted false contract, proved the true control, then discharged
the obligations in verification/squabble-creusot at merge checkout
f9499a8de0b8c525459a669e2cdbcacf83a49b85. Proved (13 files) is the
prover’s file-level result, not a theorem count. The gate’s zero trusted-axiom
field counts only tracked Rust lines containing the literal #[trusted];
it does not count axioms from dependencies or the prover. That checkout combines
PR head
1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848 with base
17284299184fd31a10c7bf382f02262cd0ab308c. This receipt covers the separate
contract crate at that revision; later revisions and the operational engine
need their own validation. The gate still reports no proof performed when
it cannot establish a working prover. Scope, historical environment failures
and the licence note: docs/CREUSOT.adoc.
contracts/ publishes two contracts that other repositories integrate against.
Both are consumed by revision id plus a sha256 manifest, never by a branch:
|
The read-only CI invocation: which subcommands are in contract, the six read
permissions the gate needs (and the |
|
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. |
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.0Nothing 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.
Every "green" the squabbler declares is backed by the gate’s own required
check passing legitimately — never by an admin override, an enforce_admins
toggle, or removal/rename-away of a required context. An admin-merge cheats past
the gate; a squabble wins it.
This is not a code-review promise. It is a machine-checked invariant: the
SPARK package in spark/ proves that the only transition into Green is "a
required check actually ran and passed" — dropping the required set, renaming a
check away, or any override are provably not paths to green.
|
The fight engine. Pure, detachable, no hypatia/estate dependency — |
|
The shared host brain: a2ml ecosystem-context reader + workflow ground-truth + the fight planner. One planner for the CLI and the App, so they cannot drift. |
|
|
|
The loopback HTTP backend (axum, |
|
Forge access: GitHub GraphQL via |
|
The formal heart. |
|
Creusot contracts for the scalar invariants, plus a stable-Rust mirror that tests for drift from the engine. A hosted proof discharged the contract crate at merge checkout |
just test # 7 engine tests pass
just prove # gnatprove: postcondition proved (squabble ≠ bypass)
just demo # diagnose a stale-required-context deadlockMined from the 2026-06-22 rsr-template-repo lockdown (effectively a manual
squabbler run). Every move satisfies the gate:
-
Stale required-context — reconcile the required name to the real emitted name.
-
Path-filter deadlock — inject the documented job-level pass-through.
-
Reusable-workflow pin drift — re-pin a stale/broken SHA to current.
-
Modify/delete & rebase conflicts — resolve and re-run.
-
Check-name ground-truthing — the shared substrate for moves 1 and 2.
-
Licence-policy drift — doctrine-constrained: adding a missing canonical
LICENSES/text is authoring (may apply); rewriting an existing file’s SPDX header is relicensing (flag, owner-only — never edit). -
Non-functional gate — the required check’s own script fails unconditionally (cannot be won from the PR side; mined from
hypatia#566): recognise, stop re-diagnosing, escalate with evidence. -
Actions-policy
startup_failuredeadlock (issue #15) — the repository’s own posture refuses to start a required check: an empty/lackingselectedallowlist (ReconcileActionsPolicy/SetActionsAllowedAll— estate posture of record isallowed_actions=allwithsha_pinning_required=trueKEPT), or a tag-pinneduses:under enforced SHA pinning (PinWorkflowActions). The fetch probesactions/permissionswhenever a required context resolves toSTARTUP_FAILURE, so the fight proposes the settings/pin move instead of mis-attributing to the reusable’s owner or a security scan. These moves only let a required check start; none weakens the gate. -
Zero-job
startup_failure— a workflow that dies before any job exists, so no check run is created and no PR check list shows it. Two distinct classes: a moved coordinate (reusable owner renamed/transferred) →RepointToCanonicalwith the same pin; and allow-list admission required (canonical coordinate refused by the caller’sselectedallow-list) →AllowListAdmissionRequirednaming the exactowner/repo@*pattern.squabble chainsresolves every upstream’s canonicalfull_nameand flags moved upstreams and canonical-grouped pin skew before a run proves it;squabble zero-jobreports attribution per observed zero-job run. Diagnosis and sequencing only — neither move makes anything green.
Red→green code fixes are deliberately out of scope for v0.1: "fixing" a failing test by weakening it would violate squabble ≠ bypass.
