Repository navigation
Creusot red = prerequisite failure, and 'Creusot verdict' adjudicates a proof that never ran #148
Description
On PR #145 (ca306ba and since), the Creusot gate reports two red checks, and neither is a statement about this repository's contracts:
| check | failing step | what it actually says |
|---|---|---|
creusot / Creusot proofs (cargo creusot prove) |
Install Creusot v0.14.0 (clone at the tag, ./INSTALL) at run 41220124068 job 124592955217 |
the prover could not be installed; no proof was attempted |
creusot / Creusot verdict |
Adjudicate at run 41220124068 job 124593340911 |
a verdict is produced for proofs that never ran |
The second is the interesting one. It is a preflight failure presented as a verdict — the exact class squabble-core::execution exists to name (PrerequisiteMissing), and the exact reason a reader must not treat this red as "the contracts failed". A verdict job that can conclude without the proofs having been produced is evidence-free by construction, and should say no proof was performed rather than adjudicate.
Where the fix belongs
This repository is a thin caller: .github/workflows/creusot.yml calls
hyperpolymath/cicd-suite/.github/workflows/creusot-gate.yml@bf7dd95cf49733019343ff485c2f45c6b261839c
so the install failure and the adjudication shape are both inside the shared gate. No workflow copy is being made here — that would be a competing implementation, and the whole point of the reusable is one owner. The gate's own validation is tracked as hyperpolymath/proven-cicd-and-workflows#71, where the evidence has been posted.
Acceptance criteria
- cicd-suite#71 resolves the
Install Creusot v0.14.0step, or the gate pins a version/installer that installs -
creusot / Creusot verdictcannot conclude whenCreusot proofsdid not run: it must report "no proof was performed" and be classifiedPrerequisiteMissing, not failure - Once the gate runs,
verification/squabble-creusotobligations are exercised for the first time (they are currently stated, not discharged — seedocs/CREUSOT.adoc) - Nothing in this repository claims a discharged obligation until a run reaches that step
Deliberately not in scope
Disabling the gate, marking it non-required, or closing the PRs it reddens. The red is real; it is the attribution that is wrong.
Activity
coderabbitai commentedon Oct 31, 2026
🔗 Related PRs
#145 - feat(diagnosis): classify where a run stopped — preflight ≠ finding [open]
📝 Issue Planner
Check the box below or use the
@coderabbitai plancommand to generate an implementation plan and prompts that you can use with your favorite coding assistant.🧪 Issue enrichment is currently in open beta.
You can configure auto-planning by selecting labels in the issue_enrichment configuration.
To disable automatic issue enrichment, add the following to your
.coderabbit.yaml:💬 Have feedback or questions? Drop into our discord!
fix(policy): align the approved ClusterFuzzLite action paths (#1393)
fix(creusot): require scoped execution evidence before adjudicating (#80