From e54ffe62706ecd3b6be8bdb8e2e980e6caa50941 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 21:11:17 +0000 Subject: [PATCH 1/7] fix: preserve workflow filenames containing @ in startup diagnosis Strip only the explicit @refs/ suffix in run paths. Add parser and source/job-count attribution regressions, plus a CLI details regression distinguishing confirmed from unconfirmed consumers. Correct the standards pin comment and record the independently inspected Creusot receipt for merge checkout f9499a8de0b8c525459a669e2cdbcacf83a49b85. Preserve historical environment failures and unfinished template obligations; the receipt is not a proof of later source or the operational engine. Candidate prepared through repository connectors after workspace loss. Source preimage hashes verified; Rust compilation, tests, rustfmt and Clippy for this candidate have not run. Store this commit for review only; no branch/reference update is part of its creation. --- .github/workflows/creusot.yml | 8 +- .github/workflows/standards-pipeline.yml | 2 +- README.adoc | 20 ++-- crates/squabble-cli/src/chains.rs | 36 +++++++ crates/squabble-fight/src/startup.rs | 91 ++++++++++++++++- docs/CREUSOT.adoc | 116 +++++++++++++--------- docs/status/PROOF-STATUS.adoc | 24 ++++- verification/squabble-creusot/README.adoc | 11 +- 8 files changed, 238 insertions(+), 70 deletions(-) diff --git a/.github/workflows/creusot.yml b/.github/workflows/creusot.yml index 756803e0..0222b36a 100644 --- a/.github/workflows/creusot.yml +++ b/.github/workflows/creusot.yml @@ -9,10 +9,10 @@ # can say no, proves a planted TRUE one, and only then runs # `cargo creusot prove` in every crate that carries contracts. # -# What it covers here: verification/squabble-creusot. Obligations are -# **stated, not discharged** — no run has reached Why3 yet (see -# docs/CREUSOT.adoc). A green on this check means the obligations were -# discharged on that run, not that they were ever stated before. +# What it covers here: verification/squabble-creusot. Hosted run 41909189438 +# discharged its obligations at merge checkout f9499a8de0b8c525459a669e2cdbcacf83a49b85 +# after rejecting the false control and proving the true one (docs/CREUSOT.adoc). +# Each later source still needs its own proof run; this is not a whole-engine proof. # # Full-SHA pin, DE-ONBOARDED from actions.lock — same rule as rust-ci.yml: the # gate scripts are pinned by the caller's own `uses:` SHA, so this line is the diff --git a/.github/workflows/standards-pipeline.yml b/.github/workflows/standards-pipeline.yml index d999ee8d..7aaa8a98 100644 --- a/.github/workflows/standards-pipeline.yml +++ b/.github/workflows/standards-pipeline.yml @@ -33,7 +33,7 @@ permissions: jobs: pipeline: - # metadatastician/standards @ 8e48b1ca (standards main 2026-10-25; see actions.lock). + # metadatastician/standards @ a797d308c0517d4e2d21cc7f1cb08d41f82b1a12 (see actions.lock). # # NO `secrets:` block, deliberately. ci-pipeline.yml declares # `workflow_call.inputs` only, has no `secrets:` block and references no diff --git a/README.adoc b/README.adoc index a9ecaae6..827e35c7 100644 --- a/README.adoc +++ b/README.adoc @@ -217,12 +217,18 @@ just verify-mirror # stable Rust: the model vs the real engine just verify-creusot # the prover: discharge the obligations ---- -**Stated, not proved.** No obligation has been discharged, and this repository's -own `Rust CI` currently ends as a zero-job `startup_failure`, so CI has not -compiled the workspace either. `.github/workflows/creusot.yml` calls the estate's -`creusot-gate.yml`, which fails a claim of proof with no contracts behind it and -reports *no proof performed* rather than a verdict when the prover cannot be -shown to work. Details and the licence note: `docs/CREUSOT.adoc`. +**Hosted proof recorded for an exact source revision.** On 2026-11-04, +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[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)`; the gate +reported zero trusted axioms). 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`. == Downstream integration contracts (pinned, immutable revisions) @@ -280,7 +286,7 @@ check away, or any override are provably *not* paths to green. | `crates/squabble-app` | The loopback HTTP backend (axum, `127.0.0.1:7741`): serves the shared planner to the boj-server `cicd-squabbler-mcp` cartridge. The GitHub App *webhook* leg (trigger button + octocrab) is still to come — no webhook route is registered. | `crates/squabble-forge`| Forge access: GitHub GraphQL via `gh api graphql`, batched, validated against a committed schema snapshot. REST where GraphQL has no equivalent — notably `repos/{o}/{n}` for canonical `full_name` resolution (redirects followed, names compared). | `spark/` | The formal heart. `Gate_Machine` + the proved theorem `green ⇔ (non-empty ∧ all passed)`. -| `verification/squabble-creusot` | The Rust twin of `spark/`: Creusot contracts for the same invariants, plus a stable-Rust mirror that fails if the engine drifts from them. **Stated, not proved** — no obligation has been discharged yet. See `docs/CREUSOT.adoc`. +| `verification/squabble-creusot` | 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 `f9499a8…` on 2026-11-04; this does not certify later source or the whole engine. Exact receipt and scope: `docs/CREUSOT.adoc`. |=== == Verify it yourself diff --git a/crates/squabble-cli/src/chains.rs b/crates/squabble-cli/src/chains.rs index 76fcaf49..b7908a35 100644 --- a/crates/squabble-cli/src/chains.rs +++ b/crates/squabble-cli/src/chains.rs @@ -667,6 +667,42 @@ mod tests { .any(|f| f.severity() == Severity::Blocking)); } + #[test] + fn moved_details_label_only_unconfirmed_consumers() { + use squabble_core::chains::{Edge, EdgeKind, Pin}; + + let edge = |from: &str, file: &str, pin: &str| Edge { + from: RepoId::new(from), + file: file.into(), + to: RepoId::new("old/tool"), + kind: EdgeKind::Action, + path: None, + pin: Pin::parse(pin), + version_hint: None, + }; + let finding = Finding::MovedUpstream { + written: RepoId::new("old/tool"), + canonical: RepoId::new("new/tool"), + consumers: vec![edge( + "me/app", + "ci.yml", + "1111111111111111111111111111111111111111", + )], + unconfirmed_consumers: vec![edge( + "me/shared", + "build.yml", + "2222222222222222222222222222222222222222", + )], + }; + assert_eq!( + details(&finding), + [ + "me/app:ci.yml @111111111111", + "me/shared:build.yml @222222222222 (upstream revision unconfirmed)", + ] + ); + } + #[test] fn a_dead_upstream_is_found_by_rest_even_without_follow() { let r = collect( diff --git a/crates/squabble-fight/src/startup.rs b/crates/squabble-fight/src/startup.rs index 21ead9af..014e6c27 100644 --- a/crates/squabble-fight/src/startup.rs +++ b/crates/squabble-fight/src/startup.rs @@ -299,10 +299,12 @@ pub fn parse_startup_runs(body: &str) -> Result, String> { .get("path") .and_then(serde_json::Value::as_str) .unwrap_or(""); - // Drop a `@ref` suffix before taking the filename: `.github/ - // workflows/ci.yml@refs/heads/main` must yield `ci.yml`, not - // `main`. The ref is not evidence of which file ran. - let path = path.split('@').next().unwrap_or(path); + // Drop only an explicit `@refs/` suffix before taking the filename. + // `release@nightly.yml` is a valid filename, including when followed + // by `@refs/heads/main`. The ref is not source-revision evidence. + let path = path + .split_once("@refs/") + .map_or(path, |(workflow, _)| workflow); let workflow_file = path.rsplit('/').next().unwrap_or(path).to_string(); let workflow_name = r .get("name") @@ -831,6 +833,87 @@ jobs: assert_eq!(runs[1].workflow_file, "ci.yml"); } + #[test] + fn an_at_sign_in_the_workflow_filename_survives_ref_suffix_removal() { + let body = serde_json::json!({ + "workflow_runs": [ + {"id": 31, "conclusion": "startup_failure", + "path": ".github/workflows/release@nightly.yml"}, + {"id": 32, "conclusion": "startup_failure", + "path": ".github/workflows/release@nightly.yml@refs/heads/main"}, + {"id": 33, "conclusion": "startup_failure", + "path": ".github/workflows/release@refs.yml"}, + {"id": 34, "conclusion": "startup_failure", + "path": ".github/workflows/release@nightly.yml@refs/heads/topic@refs/heads/main"} + ] + }) + .to_string(); + let runs = parse_startup_runs(&body).expect("parse"); + let files: Vec<_> = runs.iter().map(|r| r.workflow_file.as_str()).collect(); + assert_eq!( + files, + [ + "release@nightly.yml", + "release@nightly.yml", + "release@refs.yml", + "release@nightly.yml", + ] + ); + assert!(runs.iter().all(|r| r.jobs.is_none())); + } + + #[test] + fn an_at_named_workflow_still_requires_matching_source_and_zero_jobs() { + let files = [wf("release@nightly.yml", WORKFLOW)]; + let names = canonical(&[( + "old/standards", + CanonicalResolution::Moved { + canonical: "new/standards".into(), + }, + )]); + for path in [ + ".github/workflows/release@nightly.yml", + ".github/workflows/release@nightly.yml@refs/heads/main", + ] { + let body = serde_json::json!({ + "workflow_runs": [{ + "id": 35, "conclusion": "startup_failure", + "head_sha": SHA, "path": path + }] + }) + .to_string(); + let mut observed = parse_startup_runs(&body).expect("parse").remove(0); + for jobs in [None, Some(0), Some(1)] { + observed.jobs = jobs; + for checkout in [ + None, + Some("0000000000000000000000000000000000000000"), + Some(SHA), + ] { + let out = + attribute_run(CALLER, &observed, &files, &names, None, checkout, None); + assert_eq!(out.len(), 1, "{path}: {out:#?}"); + if jobs == Some(0) && checkout == Some(SHA) { + assert_eq!(out[0].workflow, "release@nightly.yml"); + assert_eq!(out[0].class, StartupFailureClass::MovedCoordinate); + assert_eq!( + out[0].coordinate, + format!("old/standards/.github/workflows/hypatia-scan.yml@{SHA}") + ); + assert!(matches!( + out[0].proposed_move(), + Some(Move::RepointToCanonical { pin, .. }) if pin == SHA + )); + } else { + assert_eq!(out[0].class, StartupFailureClass::Unattributed); + assert!(out[0].proposed_move().is_none()); + assert!(out[0].required_allow_list_pattern.is_none()); + } + } + } + } + } + #[test] fn a_startup_failure_without_a_usable_id_is_an_error_not_a_skip() { // Skipping it would leave an empty result, and `zero-job` would then exit diff --git a/docs/CREUSOT.adoc b/docs/CREUSOT.adoc index 67ca03b8..f8d430e4 100644 --- a/docs/CREUSOT.adoc +++ b/docs/CREUSOT.adoc @@ -9,46 +9,64 @@ The estate requires Rust that carries deductive-verification obligations, the Rust twin of the SPARK proofs in `spark/`. This page records what exists here, what it means, and — plainly — what has *not* happened yet. -== Status: stated, not proved +== Hosted proof receipt: 2026-11-04 -[cols="2,1,3"] +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438[Run 41909189438] +completed successfully. Its +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[proof job 126852164109] +records the following source and execution evidence: + +[cols="2,3",options="header"] |=== -| Item | State | Meaning - -| Contracts in `verification/squabble-creusot` -| written -| Six obligations state the engine's load-bearing invariants to Creusot. - -| Stable-Rust mirror (`src/model.rs`) -| written, not yet run -| The same statements as ordinary functions — one mirror function per contract - (`accepted`, `has_evidence`, `after_diagnosis`, `after_admission`, `admits`, - `requires_admission`) — with `#[test]`s that compare them to the real - `squabble-core`, that check the post-event statements over *both* values of - `diagnosed` and of `admitted`, and that pin the arithmetic at the `u32` - boundaries. Needs only a stable toolchain. - -| `cargo creusot prove` -| **never run** -| No obligation has reached Why3. No run has discharged anything. - -| Estate gate (`Creusot Gate` workflow) -| wired -| Calls `hyperpolymath/cicd-suite`'s `creusot-gate.yml`, phase-verified locally - (see <<_what_was_actually_checked>>). It cannot pass until a runner installs - the toolchain and the obligations discharge. - -| Rust CI on this repository -| **not running at all** -| `Rust CI` concludes `startup_failure` with **zero jobs** on `main` and on - branches, so nothing here has been compiled in CI either. That is the class - `squabble zero-job` exists to name (see `README.adoc`); until it is fixed, no - Rust in this repository is built by CI. +| Evidence | Observed value + +| Checked-out merge revision +| `f9499a8de0b8c525459a669e2cdbcacf83a49b85` + +| Pull-request head +| `1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848` + +| Merge base +| `17284299184fd31a10c7bf382f02262cd0ab308c` + +| Gate source checked out by the job +| `hyperpolymath/cicd-suite@47a5fe0aa1039ad8a6a0614137d575e66649a174` + +| Toolchain +| Creusot 0.14.0 with `nightly-2026-08-03` + +| False control +| The planted false postcondition was refused. + +| True control +| The planted true postcondition was proved. + +| Calling crate +| `verification/squabble-creusot`: `Proved (13 files)` at + 20:55:09 UTC; the gate reported every obligation discharged and zero + trusted axioms. + +| Verdict +| Job `126858835478` concluded success after detection, theatre and proof jobs + succeeded. |=== -The honest phrase is **stated, not proved**. Do not upgrade it until a `prove` -run discharges every obligation on a real toolchain; the estate gate fails a -claim of proof that has no contracts behind it, and that gate is right to. +This receipt discharges the contracts in the separate verification crate at +the named merge revision. It is not a proof of all operational Rust code, and +it does not certify later commits or the default branch merely because they +contain this document. The stable mirror tests, which compare the model with +`squabble-core`, remain a separate validation step; this proof receipt does +not report their execution. The ABI/Idris2/Lean4 template obligations in +`docs/status/PROOF-STATUS.adoc` are also outside this receipt. + +The contract crate has six scalar obligations and a stable-Rust mirror +(`src/model.rs`). The mirror contains one function per contract +(`accepted`, `has_evidence`, `after_diagnosis`, `after_admission`, `admits`, +`requires_admission`), tests both values of `diagnosed` and `admitted`, and +checks `u32` arithmetic boundaries. Those executable comparisons must pass +when validating later source; the recorded prover result does not replace +them. Earlier local toolchain failures are preserved below as historical +receipts, not as the current status of the hosted proof. == What the obligations say @@ -229,13 +247,12 @@ prebuilt image. `apt-get update` cannot write `/var/lib/apt/lists` and the Debian mirrors are not on the allow-list. `why3` does not exist on PyPI or npm (HTTP 404), so layer 4 cannot be improvised from the reachable channels either. -**What this means for a verdict: nothing, which is the point.** With no -toolchain, `just verify-status` reports every layer MISSING and exits `2`; the -estate gate's prove phase exits `2` with NO PROOF WAS PERFORMED; and the status -of the obligations is unchanged — STATED, NOT PROVED. What must *not* happen, -and did not, is an installer that reports success because it skipped a layer. -Run `just verify-install` on a host with dist access to move any of this -forward. +That 2026-10-28 environment produced no proof verdict: `just verify-status` +reported every layer MISSING and exited `2`; the estate gate's prove phase +exited `2` with NO PROOF WAS PERFORMED. The obligations remained stated but +unproved in that local attempt. The installer did not report success by +skipping a layer. This historical failure is distinct from the successful +hosted receipt recorded above; other hosts still require the full toolchain. == Running the obligations @@ -252,10 +269,10 @@ just verify-gate $(grep -oE 'cicd-suite/\.github/workflows/creusot-gate\.yml@[0- .github/workflows/creusot.yml | head -1 | sed 's/.*@//') ---- -== What was actually checked +== Historical local gate-wiring check -Run against this tree with the estate script -(`cicd-suite/actions/creusot-check/check.sh`), tracked files only: +Before the hosted proof receipt above, a local attempt exercised the estate +script (`cicd-suite/actions/creusot-check/check.sh`) over tracked files: [source,text] ---- @@ -265,9 +282,10 @@ $ CREUSOT_GATE_PHASE=prove ... -> exit 2: 'cargo creusot' is not available — NO PROOF WAS PERFORMED. ---- -So: the wiring is exercised end to end, the anti-theatre checks pass honestly, -and the prove phase fails closed rather than reporting a verdict it cannot -support. **No obligation has been discharged.** +That attempt exercised detection and anti-theatre checks, then the prove phase +failed closed because its toolchain was unavailable. It discharged no +obligation. The later hosted proof receipt above supplies the separate, +source-bound execution evidence. == Why a separate crate, and the licence position diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index aca702cf..2ec7342e 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,9 +2,23 @@ // Copyright (c) Jonathan D.A. Jewell // Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc // Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — {{PROJECT}} += Proof Status — cicd-squabbler -== Summary +== Recorded Creusot result + +On 2026-11-04, +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[proof job 126852164109] +rejected the planted false control, proved the true control, and discharged +the contracts in `verification/squabble-creusot` at merge checkout +`f9499a8de0b8c525459a669e2cdbcacf83a49b85`. It reported `Proved (13 files)`; +the gate reported zero trusted axioms. The exact head, base and gate source +are recorded in `../CREUSOT.adoc`. + +This result applies to that contract crate and source revision. It does not +complete the ABI/typing template obligations below or certify later source, +the whole operational engine, or separate mirror-test execution. + +== Template obligation summary [cols="2,1,1,1,1,1", options="header"] |=== @@ -20,7 +34,8 @@ | *Total* | *7* | *0* | *0* | *0* | *7* |=== -*Overall*: 0% proven +*Template obligations*: 0 of 7 recorded complete. The separate Creusot receipt +above is not counted as completion of any template obligation. == Proofs Done @@ -32,7 +47,7 @@ |=== | ID | Proof | Prover | File | Date | Verified By -| — | No proofs completed yet | — | — | — | — +| — | No template obligations recorded complete | — | — | — | — |=== == Proofs In Progress @@ -98,4 +113,5 @@ panic-attack assail --proofs-only | Date | Change | By | 2026-04-04 | Initial proof status tracking | Template +| 2026-11-04 | Record bounded Creusot hosted receipt; retain template obligations as uncompleted | Hosted run 41909189438 |=== diff --git a/verification/squabble-creusot/README.adoc b/verification/squabble-creusot/README.adoc index 4e4da403..ce1defd9 100644 --- a/verification/squabble-creusot/README.adoc +++ b/verification/squabble-creusot/README.adoc @@ -5,7 +5,16 @@ The Rust twin of `spark/`: a parallel verification artefact that states the engine's load-bearing invariants to a prover instead of only testing them. -**Status: stated, not proved.** No obligation has been discharged. +**Status: obligations discharged at the recorded merge checkout.** +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[Hosted job 126852164109] +on 2026-11-04 rejected the false control, proved the true control, and reported +`Proved (13 files)` for this crate at +`f9499a8de0b8c525459a669e2cdbcacf83a49b85`, with zero trusted axioms reported +by the gate. This is the merge of PR head +`1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848` into base +`17284299184fd31a10c7bf382f02262cd0ab308c`. The receipt covers these contracts +at that source, not later revisions or the full operational engine. The stable +mirror tests are a separate validation step. * `src/model.rs` — the invariants as ordinary Rust, plus `#[test]`s that compare them with the real `squabble-core`. Runs on **stable** Rust; no Creusot From 99a98599758dfdfa30111b8885ea6da6205c7475 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 21:25:17 +0000 Subject: [PATCH 2/7] fix: resolve run ref suffixes against exact source filenames Retain workflow-relative API paths, including documented @main suffixes and refs containing slashes. Resolve a workflow only when exactly one source filename fits the plain path or filename-plus-nonempty-ref form. Ambiguous literal @ filenames remain unattributed. Use the same resolver for CLI coordinate collection, source attribution and workflow-specific native-lock findings. Preserve zero-job and source-revision guards and independent malformed-lock evidence. Add parser, attribution, native-coverage and no-coordinate-read regressions. Prepared through connectors after the prior runtime was lost. Source blob preimages verified; Rust compilation, tests, rustfmt and Clippy have not run for this candidate. Unreferenced review object only; no branch update is part of creation. --- crates/squabble-cli/src/zero_job.rs | 89 +++++++- crates/squabble-core/src/startup.rs | 6 +- crates/squabble-fight/src/startup.rs | 293 ++++++++++++++++++++++----- 3 files changed, 331 insertions(+), 57 deletions(-) diff --git a/crates/squabble-cli/src/zero_job.rs b/crates/squabble-cli/src/zero_job.rs index 5b2a7427..8a82dfeb 100644 --- a/crates/squabble-cli/src/zero_job.rs +++ b/crates/squabble-cli/src/zero_job.rs @@ -44,7 +44,9 @@ use squabble_core::startup::{ ZeroJobRun, ZeroJobRunAttribution, }; use squabble_fight::chains::{extract_edges, snapshot_local}; -use squabble_fight::startup::{attribute_run, parse_job_count, parse_startup_runs}; +use squabble_fight::startup::{ + attribute_run, parse_job_count, parse_startup_runs, resolve_run_workflow, +}; use squabble_forge::rest::{resolve_canonical, GhRest, RestTransport}; use std::collections::BTreeSet; use std::path::Path; @@ -288,7 +290,7 @@ fn collect( { continue; } - if let Some(file) = files.iter().find(|f| f.path == run.workflow_file) { + if let Ok(file) = resolve_run_workflow(run, files) { for edge in extract_edges(&RepoId::new(slug), file) { repos.insert(edge.to); } @@ -705,6 +707,89 @@ mod tests { ) } + #[test] + fn ref_suffixes_resolve_the_source_file_before_upstream_collection() { + let mut file = moved_workflow(); + file.path = "release@nightly.yml".into(); + let files = [file]; + let rest = Rest(vec![( + "old/standards", + CanonicalResolution::Moved { + canonical: "new/standards".into(), + }, + )]); + for path in [ + ".github/workflows/release@nightly.yml@main", + ".github/workflows/release@nightly.yml@feature/topic", + ".github/workflows/release@nightly.yml@refs/heads/main", + ] { + let body = json!({"workflow_runs": [{ + "id": 44, "head_sha": SHA, "conclusion": "startup_failure", "path": path + }]}) + .to_string(); + let mut observed = parse_startup_runs(&body).unwrap().remove(0); + observed.jobs = Some(0); + let report = collect( + "me/app", + &files, + vec![observed], + &rest, + None, + Vec::new(), + ); + let finding = &report.runs[0].attributions[0]; + assert_eq!(finding.workflow, "release@nightly.yml"); + assert_eq!(finding.class, StartupFailureClass::MovedCoordinate); + assert!(matches!( + finding.proposed_move(), + Some(Move::RepointToCanonical { pin, .. }) if pin == SHA + )); + assert!(report.has_findings()); + assert_eq!(exit_for(&report), ExitCode::from(BLOCKING_EXIT)); + } + } + + #[test] + fn ambiguous_workflow_names_cannot_trigger_coordinate_reads_or_moves() { + struct NoCoordinateReads; + impl RestTransport for NoCoordinateReads { + fn get(&self, path: &str) -> Result { + panic!("ambiguous workflow must not resolve any coordinate: {path}"); + } + } + + let files = [ + wf("release.yml", &moved_workflow().text), + wf("release.yml@nightly.yml", &moved_workflow().text), + ]; + for path in [ + ".github/workflows/release.yml@nightly.yml", + ".github/workflows/release.yml@nightly.yml@main", + ".github/workflows/release.yml@nightly.yml@refs/heads/main", + ] { + let body = json!({"workflow_runs": [{ + "id": 45, "head_sha": SHA, "conclusion": "startup_failure", "path": path + }]}) + .to_string(); + let mut observed = parse_startup_runs(&body).unwrap().remove(0); + observed.jobs = Some(0); + let report = collect( + "me/app", + &files, + vec![observed], + &NoCoordinateReads, + Some(&AllowList::default()), + Vec::new(), + ); + let finding = &report.runs[0].attributions[0]; + assert_eq!(finding.class, StartupFailureClass::Unattributed); + assert!(finding.evidence.contains("ambiguous")); + assert!(finding.proposed_move().is_none()); + assert!(finding.required_allow_list_pattern.is_none()); + assert_eq!(exit_for(&report), ExitCode::from(BLOCKING_EXIT)); + } + } + #[test] fn a_moved_reusable_run_reports_every_attribution_field() { let files = vec![moved_workflow()]; diff --git a/crates/squabble-core/src/startup.rs b/crates/squabble-core/src/startup.rs index bf313485..5349b990 100644 --- a/crates/squabble-core/src/startup.rs +++ b/crates/squabble-core/src/startup.rs @@ -639,7 +639,9 @@ pub struct ZeroJobRun { /// The failed run's immutable source revision, when supplied by GitHub. #[serde(default)] pub head_sha: Option, - /// Workflow file relative to `.github/workflows/`. + /// Observed path relative to `.github/workflows/`, retaining any API ref + /// suffix. `@` may also belong to the filename: the host must resolve this + /// against the matching source tree before attributing a particular file. pub workflow_file: String, /// The workflow's display name, when the API reports one. #[serde(default)] @@ -656,6 +658,8 @@ pub struct ZeroJobRunAttribution { pub run_id: u64, #[serde(default)] pub head_sha: Option, + /// Observed workflow path, including any unresolved API ref suffix. + /// Qualified source filenames are recorded in individual attributions. pub workflow: String, #[serde(default)] pub jobs: Option, diff --git a/crates/squabble-fight/src/startup.rs b/crates/squabble-fight/src/startup.rs index 014e6c27..b184a07f 100644 --- a/crates/squabble-fight/src/startup.rs +++ b/crates/squabble-fight/src/startup.rs @@ -79,6 +79,54 @@ pub fn attribute_workflow( out } +/// Resolve an observed workflow path against a source checkout's file names. +/// +/// GitHub reports both plain paths and paths ending in short or full refs. +/// Since `@` is legal in a workflow filename, splitting it without the source +/// tree loses evidence. Retain every exact filename or filename + nonempty +/// `@ref` interpretation and require exactly one match. A collision such as +/// `release.yml@nightly.yml` when both it and `release.yml` exist is ambiguous. +/// +/// The caller must supply the complete, unmodified workflow tree and establish +/// the run's zero job count and matching source revision before attribution. This function does not +/// resolve or trust the ref suffix as a source revision. +/// +/// # Errors +/// +/// Returns an error when no source workflow matches or more than one matches. +pub fn resolve_run_workflow<'a>( + run: &ZeroJobRun, + files: &'a [WorkflowFile], +) -> Result<&'a WorkflowFile, String> { + let mut candidates = files.iter().filter(|file| { + // Actions workflow files live directly in .github/workflows. + if file.path.contains('/') + || !(file.path.ends_with(".yml") || file.path.ends_with(".yaml")) + { + return false; + } + run.workflow_file == file.path + || run + .workflow_file + .strip_prefix(file.path.as_str()) + .and_then(|suffix| suffix.strip_prefix('@')) + .is_some_and(|reference| !reference.is_empty()) + }); + match (candidates.next(), candidates.next()) { + (Some(file), None) => Ok(file), + (None, _) => Err(format!( + "workflow path `{}` has no matching file in the source checkout; \ + retain the run and read its exact workflow before attributing coordinates", + run.workflow_file + )), + (Some(_), Some(_)) => Err(format!( + "workflow path `{}` is ambiguous between source filenames and ref suffixes; \ + no particular workflow or coordinate is attributed", + run.workflow_file + )), + } +} + /// Attribute one failed run from the repo's already-read workflow files. /// /// Attribution requires an observed zero job count and a full run commit ID @@ -92,10 +140,10 @@ pub fn attribute_workflow( /// attribution. A verified lock, or a coverage mismatch for another workflow, /// also permits coordinate attribution to continue. /// -/// When the run's workflow file is not among `files` (an unreadable checkout, a -/// workflow deleted since the run), the run still gets an honest -/// `Unattributed` entry with the reason — absence of evidence is never -/// evidence of a clean start. +/// A workflow path with no source match or multiple filename/ref interpretations +/// remains `Unattributed`. A source-bound malformed lock is still an independent +/// repository-level defect; workflow-specific lock findings require a unique +/// source filename. Absence or ambiguity is never evidence of a clean start. /// /// When coordinate attribution finds no moved or unadmitted coordinate, the /// result is a single `Unattributed` entry rather than one per coordinate. The @@ -137,6 +185,7 @@ pub fn attribute_run( ), )]; } + let workflow = resolve_run_workflow(run, files); if let Some(lock) = lock { if !same_source_revision(Some(&lock.head_sha), checkout_revision) { return vec![unattributed(repo, &run.workflow_file, @@ -145,16 +194,18 @@ pub fn attribute_run( let class = match lock.status { NativeLockStatus::Malformed => Some(StartupFailureClass::InvalidActionsLock), NativeLockStatus::CoverageMismatch => { - let path = format!(".github/workflows/{}", run.workflow_file); - let affected = serde_json::from_str::(&lock.stdout) - .ok() - .and_then(|report| report.get("workflows").and_then(|v| v.as_array()).cloned()) - .is_some_and(|workflows| { - workflows.iter().any(|workflow| { - workflow.get("path").and_then(|v| v.as_str()) == Some(path.as_str()) - && workflow.get("valid").and_then(|v| v.as_bool()) == Some(false) + let affected = workflow.as_ref().is_ok_and(|file| { + let path = format!(".github/workflows/{}", file.path); + serde_json::from_str::(&lock.stdout) + .ok() + .and_then(|report| report.get("workflows").and_then(|v| v.as_array()).cloned()) + .is_some_and(|workflows| { + workflows.iter().any(|workflow| { + workflow.get("path").and_then(|v| v.as_str()) == Some(path.as_str()) + && workflow.get("valid").and_then(|v| v.as_bool()) == Some(false) + }) }) - }); + }); affected.then_some(StartupFailureClass::ActionsLockMismatch) } NativeLockStatus::Unverified => None, @@ -163,7 +214,9 @@ pub fn attribute_run( if let Some(class) = class { let mut finding = unattributed( repo, - &run.workflow_file, + workflow + .as_ref() + .map_or(run.workflow_file.as_str(), |file| file.path.as_str()), format!( "{} at source {} ({} exit {:?}); the complete official output is retained. \ This reproduces a source defect, not proof of the sole GitHub startup cause.", @@ -191,20 +244,14 @@ pub fn attribute_run( } findings }; - let Some(file) = files.iter().find(|f| f.path == run.workflow_file) else { - return retain_probe_failure(vec![unattributed( - repo, - &run.workflow_file, - format!( - "workflow `{}` is not in the local checkout, so its `uses:` coordinates cannot \ - be read. The run is still a zero-job startup failure — read the workflow at \ - the run's commit before changing anything.", - run.workflow_file - ), - )]); + let file = match workflow { + Ok(file) => file, + Err(reason) => { + return retain_probe_failure(vec![unattributed(repo, &run.workflow_file, reason)]); + } }; - let all = attribute_workflow(repo, &run.workflow_file, &file.text, canonical, allow_list); + let all = attribute_workflow(repo, &file.path, &file.text, canonical, allow_list); let (mut primary, mut unexplained): (Vec, Vec) = all .into_iter() .partition(|a| a.class != StartupFailureClass::Unattributed); @@ -253,12 +300,12 @@ fn unattributed(repo: &str, workflow: &str, evidence: String) -> ZeroJobAttribut /// `jobs` is left `None` here: the count comes from a second read and is the /// host's evidence, not something this parser may assume. /// Matching is case-insensitive. A failed entry without an unsigned integer -/// run ID is an error; a missing or non-string path becomes an empty filename, -/// otherwise the ref suffix is dropped and only the final path component is -/// kept. GitHub reports `path` either as `.github/workflows/ci.yml` or as -/// `.github/workflows/ci.yml@refs/heads/main`; taking the last slash-separated -/// component of the second form would name the file `main`, so every run would -/// fail to match the checkout and be attributed to nothing. +/// run ID is an error; a missing or non-string path becomes an empty string. +/// Only the literal `.github/workflows/` prefix is removed. The remaining +/// filename and optional suffix are retained losslessly: GitHub documents +/// `build.yml@main` and also returns full refs. Filenames and refs can both +/// contain `@`, and refs can contain slashes. Source-backed disambiguation +/// belongs to [`resolve_run_workflow`], after revision and job evidence checks. /// /// # Errors /// @@ -299,13 +346,12 @@ pub fn parse_startup_runs(body: &str) -> Result, String> { .get("path") .and_then(serde_json::Value::as_str) .unwrap_or(""); - // Drop only an explicit `@refs/` suffix before taking the filename. - // `release@nightly.yml` is a valid filename, including when followed - // by `@refs/heads/main`. The ref is not source-revision evidence. - let path = path - .split_once("@refs/") - .map_or(path, |(workflow, _)| workflow); - let workflow_file = path.rsplit('/').next().unwrap_or(path).to_string(); + // Preserve both the filename and any short/full ref suffix. Neither + // an '@' split nor a basename operation can distinguish them safely. + let workflow_file = path + .strip_prefix(".github/workflows/") + .unwrap_or(path) + .to_string(); let workflow_name = r .get("name") .and_then(serde_json::Value::as_str) @@ -471,10 +517,11 @@ mod tests { {"path": ".github/workflows/other.yml", "valid": true} ]}) .to_string(); + let files = [wf("ci.yml", "jobs: {}"), wf("other.yml", "jobs: {}")]; let out = attribute_run( CALLER, &run(42, "ci.yml"), - &[], + &files, &BTreeMap::new(), None, Some(SHA), @@ -485,7 +532,7 @@ mod tests { let other = attribute_run( CALLER, &run(43, "other.yml"), - &[], + &files, &BTreeMap::new(), None, Some(SHA), @@ -497,7 +544,7 @@ mod tests { attribute_run( CALLER, &run(42, "ci.yml"), - &[], + &files, &BTreeMap::new(), None, Some(SHA), @@ -768,7 +815,7 @@ jobs: ); assert_eq!(out.len(), 1); assert_eq!(out[0].class, StartupFailureClass::Unattributed); - assert!(out[0].evidence.contains("not in the local checkout")); + assert!(out[0].evidence.contains("no matching file")); } #[test] @@ -814,27 +861,43 @@ jobs: } #[test] - fn a_run_path_carrying_a_ref_suffix_still_names_the_workflow_file() { - // GitHub reports `path` both ways. Taking the last slash-separated - // component of the suffixed form would name the file after the ref and - // silently attribute nothing, so the suffix must go first. + fn run_paths_retain_short_and_full_refs_until_source_resolution() { + // The official workflow-runs example uses build.yml@main. Branches + // can contain slashes, so basename extraction also loses evidence. let body = serde_json::json!({ "workflow_runs": [ {"id": 21, "conclusion": "startup_failure", "path": ".github/workflows/gov.yml@refs/heads/main"}, {"id": 22, "conclusion": "startup_failure", - "path": ".github/workflows/ci.yml@refs/pull/140/merge"} + "path": ".github/workflows/ci.yml@refs/pull/140/merge"}, + {"id": 23, "conclusion": "startup_failure", + "path": ".github/workflows/build.yml@main"}, + {"id": 24, "conclusion": "startup_failure", + "path": ".github/workflows/build.yml@feature/topic"} ] }) .to_string(); let runs = parse_startup_runs(&body).expect("parse"); - assert_eq!(runs.len(), 2); - assert_eq!(runs[0].workflow_file, "gov.yml"); - assert_eq!(runs[1].workflow_file, "ci.yml"); + assert_eq!(runs.len(), 4); + assert_eq!(runs[0].workflow_file, "gov.yml@refs/heads/main"); + assert_eq!(runs[1].workflow_file, "ci.yml@refs/pull/140/merge"); + assert_eq!(runs[2].workflow_file, "build.yml@main"); + assert_eq!(runs[3].workflow_file, "build.yml@feature/topic"); + + let files = [ + wf("gov.yml", WORKFLOW), + wf("ci.yml", WORKFLOW), + wf("build.yml", WORKFLOW), + ]; + let resolved: Vec<_> = runs + .iter() + .map(|run| resolve_run_workflow(run, &files).unwrap().path.as_str()) + .collect(); + assert_eq!(resolved, ["gov.yml", "ci.yml", "build.yml", "build.yml"]); } #[test] - fn an_at_sign_in_the_workflow_filename_survives_ref_suffix_removal() { + fn an_at_sign_in_the_filename_and_the_ref_suffix_are_both_preserved() { let body = serde_json::json!({ "workflow_runs": [ {"id": 31, "conclusion": "startup_failure", @@ -854,9 +917,9 @@ jobs: files, [ "release@nightly.yml", - "release@nightly.yml", + "release@nightly.yml@refs/heads/main", "release@refs.yml", - "release@nightly.yml", + "release@nightly.yml@refs/heads/topic@refs/heads/main", ] ); assert!(runs.iter().all(|r| r.jobs.is_none())); @@ -873,7 +936,10 @@ jobs: )]); for path in [ ".github/workflows/release@nightly.yml", + ".github/workflows/release@nightly.yml@main", + ".github/workflows/release@nightly.yml@feature/topic", ".github/workflows/release@nightly.yml@refs/heads/main", + ".github/workflows/release@nightly.yml@refs/tags/v1", ] { let body = serde_json::json!({ "workflow_runs": [{ @@ -914,6 +980,125 @@ jobs: } } + #[test] + fn a_literal_at_filename_is_preserved_and_collisions_are_unattributed() { + let literal = wf("release.yml@nightly.yml", WORKFLOW); + let short = wf("release.yml", WORKFLOW); + let observed = run(36, "release.yml@nightly.yml"); + let literal_only = [literal.clone()]; + assert_eq!( + resolve_run_workflow(&observed, &literal_only).unwrap().path, + "release.yml@nightly.yml" + ); + + let names = canonical(&[( + "old/standards", + CanonicalResolution::Moved { + canonical: "new/standards".into(), + }, + )]); + let literal_result = attribute_run( + CALLER, + &observed, + &literal_only, + &names, + None, + Some(SHA), + None, + ); + assert_eq!(literal_result[0].workflow, "release.yml@nightly.yml"); + assert_eq!(literal_result[0].class, StartupFailureClass::MovedCoordinate); + + let files = [short, literal]; + for path in [ + "release.yml@nightly.yml", + "release.yml@nightly.yml@main", + "release.yml@nightly.yml@refs/heads/main", + ] { + let observed = run(37, path); + assert!(resolve_run_workflow(&observed, &files) + .unwrap_err() + .contains("ambiguous")); + let out = attribute_run( + CALLER, + &observed, + &files, + &names, + Some(&AllowList::default()), + Some(SHA), + None, + ); + assert_eq!(out.len(), 1); + assert_eq!(out[0].class, StartupFailureClass::Unattributed); + assert!(out[0].evidence.contains("ambiguous")); + assert!(out[0].proposed_move().is_none()); + assert!(out[0].required_allow_list_pattern.is_none()); + } + } + + #[test] + fn unmatched_paths_and_empty_refs_do_not_borrow_a_source_basename() { + let files = [wf("build.yml", WORKFLOW)]; + for path in [ + ".github/workflows/missing.yml@main", + ".github/workflows/build.yml@", + ".github/workflows/nested/build.yml", + ".github/workflows/../build.yml", + "somewhere/build.yml", + ] { + let body = serde_json::json!({"workflow_runs": [{ + "id": 38, "conclusion": "startup_failure", + "head_sha": SHA, "path": path + }]}) + .to_string(); + let observed = parse_startup_runs(&body).unwrap().remove(0); + assert!( + resolve_run_workflow(&observed, &files).is_err(), + "{path}" + ); + } + } + + #[test] + fn native_coverage_uses_only_a_uniquely_resolved_source_filename() { + let mut lock = native_lock(NativeLockStatus::CoverageMismatch); + lock.exit_code = Some(1); + lock.stdout = serde_json::json!({"workflows": [ + {"path": ".github/workflows/ci.yml", "valid": false} + ]}) + .to_string(); + let files = [wf("ci.yml", WORKFLOW)]; + for path in ["ci.yml@main", "ci.yml@refs/heads/main"] { + let out = attribute_run( + CALLER, + &run(39, path), + &files, + &BTreeMap::new(), + None, + Some(SHA), + Some(&lock), + ); + assert_eq!(out[0].workflow, "ci.yml"); + assert_eq!(out[0].class, StartupFailureClass::ActionsLockMismatch); + assert!(out[0].proposed_move().is_none()); + } + + let ambiguous = [wf("ci.yml", WORKFLOW), wf("ci.yml@nightly.yml", WORKFLOW)]; + let out = attribute_run( + CALLER, + &run(40, "ci.yml@nightly.yml"), + &ambiguous, + &BTreeMap::new(), + Some(&AllowList::default()), + Some(SHA), + Some(&lock), + ); + assert_eq!(out[0].class, StartupFailureClass::Unattributed); + assert!(out[0].evidence.contains("ambiguous")); + assert!(out[0].proposed_move().is_none()); + assert!(out[0].required_allow_list_pattern.is_none()); + } + #[test] fn a_startup_failure_without_a_usable_id_is_an_error_not_a_skip() { // Skipping it would leave an empty result, and `zero-job` would then exit From ac26aa51f748548a7fe468f7150c94715095eb03 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 21:41:16 +0000 Subject: [PATCH 3/7] test: use extracted workflow paths in two-hop chain controls Correct the inherited fixture to Edge.file's directory-relative contract; retain its blocking assertion. Exercise actual extraction through two pinned reusable hops, with wrong-revision and wrong-file negative cases. Apply the six exact rustfmt changes reported by run41916274555. Production classification and severity rules are unchanged. --- crates/squabble-cli/src/zero_job.rs | 9 +-- crates/squabble-core/src/chains.rs | 3 +- crates/squabble-fight/src/chains.rs | 112 ++++++++++++++++++++++++++- crates/squabble-fight/src/startup.rs | 20 ++--- 4 files changed, 125 insertions(+), 19 deletions(-) diff --git a/crates/squabble-cli/src/zero_job.rs b/crates/squabble-cli/src/zero_job.rs index 8a82dfeb..0ba8647c 100644 --- a/crates/squabble-cli/src/zero_job.rs +++ b/crates/squabble-cli/src/zero_job.rs @@ -729,14 +729,7 @@ mod tests { .to_string(); let mut observed = parse_startup_runs(&body).unwrap().remove(0); observed.jobs = Some(0); - let report = collect( - "me/app", - &files, - vec![observed], - &rest, - None, - Vec::new(), - ); + let report = collect("me/app", &files, vec![observed], &rest, None, Vec::new()); let finding = &report.runs[0].attributions[0]; assert_eq!(finding.workflow, "release@nightly.yml"); assert_eq!(finding.class, StartupFailureClass::MovedCoordinate); diff --git a/crates/squabble-core/src/chains.rs b/crates/squabble-core/src/chains.rs index 66ee8569..c87c8938 100644 --- a/crates/squabble-core/src/chains.rs +++ b/crates/squabble-core/src/chains.rs @@ -1548,7 +1548,8 @@ mod tests { ), edge( "me/shared", - ".github/workflows/ci.yml", + // Edge.file is relative to .github/workflows; Edge.path below is not. + "ci.yml", "me/inner", EdgeKind::ReusableWorkflow, Some(".github/workflows/ci.yml"), diff --git a/crates/squabble-fight/src/chains.rs b/crates/squabble-fight/src/chains.rs index 71f8eb85..b28589dc 100644 --- a/crates/squabble-fight/src/chains.rs +++ b/crates/squabble-fight/src/chains.rs @@ -297,7 +297,7 @@ fn is_sha(s: &str) -> bool { #[cfg(test)] mod tests { use super::*; - use squabble_core::chains::{analyse, Finding}; + use squabble_core::chains::{analyse, Finding, Severity}; const SHA: &str = "8f2ee50841e216cd8c192eeb68953118190f105c"; @@ -423,6 +423,116 @@ jobs: .any(|f| matches!(f, Finding::Diamond { target, .. } if target == &RepoId::new("actions/checkout")))); } + #[test] + fn extracted_two_hop_routes_require_both_pins_and_the_called_file() { + let other_sha = "0000000000000000000000000000000000000000"; + let at_revision = |repo: &str, files: Vec, revision: &str| { + let mut snapshot = snap(repo, files); + snapshot.status = ScanStatus::Scanned { + revision: Some(revision.to_string()), + workflow_files: snapshot.files.len(), + }; + snapshot + }; + for (shared_revision, inner_revision, called_file, expected) in [ + (SHA, SHA, "leaf.yml", Some(Severity::Blocking)), + (other_sha, SHA, "leaf.yml", Some(Severity::Warning)), + (SHA, other_sha, "leaf.yml", Some(Severity::Warning)), + (SHA, SHA, "other.yml", None), + ] { + let app = at_revision( + "me/app", + vec![wf( + "ci.yml", + &format!( + "jobs:\n call:\n uses: me/shared/.github/workflows/reuse.yml@{SHA}\n" + ), + )], + SHA, + ); + let shared = at_revision( + "me/shared", + vec![wf( + "reuse.yml", + &format!( + "jobs:\n call:\n uses: me/inner/.github/workflows/{called_file}@{SHA}\n" + ), + )], + shared_revision, + ); + let inner = at_revision( + "me/inner", + vec![ + wf( + "leaf.yml", + &format!( + "jobs:\n check:\n runs-on: ubuntu-latest\n steps:\n - uses: old/tool@{SHA}\n" + ), + ), + wf( + "other.yml", + "jobs:\n check:\n runs-on: ubuntu-latest\n steps:\n - run: echo no external action\n", + ), + ], + inner_revision, + ); + + let first = graph_from_snapshots([(&app, Role::Subject)]); + let shared_role = upstream_roles(&first) + .into_iter() + .find(|(repo, _)| repo == &RepoId::new("me/shared")) + .expect("outer reusable") + .1; + let second = + graph_from_snapshots([(&app, Role::Subject), (&shared, shared_role.clone())]); + let inner_role = upstream_roles(&second) + .into_iter() + .find(|(repo, _)| repo == &RepoId::new("me/inner")) + .expect("inner reusable") + .1; + let mut graph = graph_from_snapshots([ + (&app, Role::Subject), + (&shared, shared_role), + (&inner, inner_role), + ]); + graph.record_canonical(RepoId::new("old/tool"), RepoId::new("new/tool")); + let report = analyse(&graph, None); + let finding = report + .findings + .iter() + .find(|finding| matches!(finding, Finding::MovedUpstream { .. })); + assert_eq!( + finding.map(Finding::severity), + expected, + "{shared_revision} {inner_revision} {called_file}" + ); + assert_eq!(report.has_blocking(), expected == Some(Severity::Blocking)); + if let Some(Finding::MovedUpstream { + consumers, + unconfirmed_consumers, + .. + }) = finding + { + assert_eq!( + consumers.len(), + usize::from(expected == Some(Severity::Blocking)) + ); + assert_eq!( + unconfirmed_consumers.len(), + usize::from(expected == Some(Severity::Warning)) + ); + let observed = consumers.first().or(unconfirmed_consumers.first()).unwrap(); + assert_eq!(observed.from, RepoId::new("me/inner")); + assert_eq!(observed.file, "leaf.yml"); + } else { + assert!(graph + .edges + .iter() + .all(|edge| edge.to != RepoId::new("old/tool"))); + } + } + } + #[test] fn snapshot_canonical_names_are_recorded_as_moves() { // The GraphQL source compares `nameWithOwner`, so a snapshot can carry diff --git a/crates/squabble-fight/src/startup.rs b/crates/squabble-fight/src/startup.rs index b184a07f..2636b4d3 100644 --- a/crates/squabble-fight/src/startup.rs +++ b/crates/squabble-fight/src/startup.rs @@ -100,8 +100,7 @@ pub fn resolve_run_workflow<'a>( ) -> Result<&'a WorkflowFile, String> { let mut candidates = files.iter().filter(|file| { // Actions workflow files live directly in .github/workflows. - if file.path.contains('/') - || !(file.path.ends_with(".yml") || file.path.ends_with(".yaml")) + if file.path.contains('/') || !(file.path.ends_with(".yml") || file.path.ends_with(".yaml")) { return false; } @@ -198,11 +197,14 @@ pub fn attribute_run( let path = format!(".github/workflows/{}", file.path); serde_json::from_str::(&lock.stdout) .ok() - .and_then(|report| report.get("workflows").and_then(|v| v.as_array()).cloned()) + .and_then(|report| { + report.get("workflows").and_then(|v| v.as_array()).cloned() + }) .is_some_and(|workflows| { workflows.iter().any(|workflow| { workflow.get("path").and_then(|v| v.as_str()) == Some(path.as_str()) - && workflow.get("valid").and_then(|v| v.as_bool()) == Some(false) + && workflow.get("valid").and_then(|v| v.as_bool()) + == Some(false) }) }) }); @@ -1007,7 +1009,10 @@ jobs: None, ); assert_eq!(literal_result[0].workflow, "release.yml@nightly.yml"); - assert_eq!(literal_result[0].class, StartupFailureClass::MovedCoordinate); + assert_eq!( + literal_result[0].class, + StartupFailureClass::MovedCoordinate + ); let files = [short, literal]; for path in [ @@ -1052,10 +1057,7 @@ jobs: }]}) .to_string(); let observed = parse_startup_runs(&body).unwrap().remove(0); - assert!( - resolve_run_workflow(&observed, &files).is_err(), - "{path}" - ); + assert!(resolve_run_workflow(&observed, &files).is_err(), "{path}"); } } From 81d8103727a8fd7bf094a52a6172b044e0733770 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 22:00:44 +0000 Subject: [PATCH 4/7] fix: require complete workflow populations before coordinate attribution Reject local enumeration, decoding and file-read gaps and partial GraphQL populations before selecting workflows, extracting edges or probing moves. Keep partial text and diagnostics without treating omissions as absence. Validate snapshot counts and filenames at the shared resolver boundary. Add actual tracked-file and source-adapter regressions for hosted execution. Synchronize Creusot status surfaces to the existing source-bound historical proof receipt; distinguish the prover job from the aggregate verdict. --- crates/squabble-cli/src/zero_job.rs | 175 ++++++++++++++- crates/squabble-core/src/chains.rs | 74 ++++++- crates/squabble-fight/src/chains.rs | 267 ++++++++++++++++++++--- crates/squabble-fight/src/startup.rs | 105 +++++++-- crates/squabble-forge/src/lib.rs | 232 ++++++++++++++++---- docs/CREUSOT.adoc | 9 +- verification/README.adoc | 11 +- verification/squabble-creusot/Cargo.toml | 2 +- verification/squabble-creusot/src/lib.rs | 21 +- 9 files changed, 782 insertions(+), 114 deletions(-) diff --git a/crates/squabble-cli/src/zero_job.rs b/crates/squabble-cli/src/zero_job.rs index 0ba8647c..e87b8e17 100644 --- a/crates/squabble-cli/src/zero_job.rs +++ b/crates/squabble-cli/src/zero_job.rs @@ -38,7 +38,7 @@ use crate::chains::BLOCKING_EXIT; use crate::fetch; use crate::lock_verifier; -use squabble_core::chains::{RepoId, ScanStatus, WorkflowFile}; +use squabble_core::chains::{RepoId, RepoSnapshot}; use squabble_core::startup::{ same_source_revision, AllowList, CanonicalResolution, NativeLockVerification, ZeroJobReport, ZeroJobRun, ZeroJobRunAttribution, @@ -137,11 +137,7 @@ pub fn run(rest: &[String]) -> ExitCode { let before = lock_verifier::checkout_revision(root); let snapshot = snapshot_local(root, args.slug.as_deref()); let slug = snapshot.repo.as_str().to_string(); - if !matches!(snapshot.status, ScanStatus::Scanned { .. }) { - let reason = match &snapshot.status { - ScanStatus::Unavailable { reason } => reason.clone(), - other => format!("{other:?}"), - }; + if let Err(reason) = snapshot.workflow_files() { eprintln!("squabble zero-job: cannot read workflows for `{slug}`: {reason}"); return ExitCode::from(2); } @@ -216,7 +212,7 @@ pub fn run(rest: &[String]) -> ExitCode { } else { collect( &slug, - &snapshot.files, + &snapshot, runs, &GhRest, allow_list.as_ref(), @@ -276,7 +272,7 @@ fn probe_allow_list(slug: &str, notes: &mut Vec) -> Option { /// native lock evidence used for attribution. No IO occurs beyond `rest`. fn collect( slug: &str, - files: &[WorkflowFile], + snapshot: &RepoSnapshot, runs: Vec, rest: &dyn RestTransport, allow_list: Option<&AllowList>, @@ -290,7 +286,7 @@ fn collect( { continue; } - if let Ok(file) = resolve_run_workflow(run, files) { + if let Ok(file) = resolve_run_workflow(run, snapshot) { for edge in extract_edges(&RepoId::new(slug), file) { repos.insert(edge.to); } @@ -327,7 +323,7 @@ fn collect( attributions: attribute_run( slug, &run, - files, + snapshot, &canonical, allow_list, source.head_sha.as_deref(), @@ -492,6 +488,7 @@ fn fetch_startup_runs( mod tests { use super::*; use serde_json::json; + use squabble_core::chains::{ScanStatus, WorkflowFile}; use squabble_core::moves::Move; use squabble_core::startup::StartupFailureClass; use squabble_forge::rest::RestResponse; @@ -508,9 +505,19 @@ mod tests { allow_list: Option<&AllowList>, notes: Vec, ) -> ZeroJobReport { + let snapshot = RepoSnapshot { + repo: RepoId::new(slug), + status: ScanStatus::Scanned { + revision: Some(SHA.into()), + workflow_files: files.len(), + }, + files: files.to_vec(), + notes: Vec::new(), + canonical: None, + }; super::collect( slug, - files, + &snapshot, runs, rest, allow_list, @@ -742,6 +749,152 @@ mod tests { } } + struct SourceCheckout(std::path::PathBuf); + + impl SourceCheckout { + fn new() -> Self { + let stamp = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .unwrap() + .as_nanos(); + let root = std::env::temp_dir() + .join(format!("squabble-source-{}-{stamp}", std::process::id())); + std::fs::create_dir_all(root.join(".github/workflows")).unwrap(); + let checkout = Self(root); + checkout.git(&["init", "-q"]); + checkout + } + + fn git(&self, args: &[&str]) { + let output = std::process::Command::new("git") + .current_dir(&self.0) + .args(args) + .env_remove("GIT_DIR") + .env_remove("GIT_WORK_TREE") + .env_remove("GIT_INDEX_FILE") + .output() + .unwrap(); + assert!( + output.status.success(), + "{}", + String::from_utf8_lossy(&output.stderr) + ); + } + + fn commit(&self) { + self.git(&["add", "--all"]); + // Disposable fixture only; no real repository configuration changes. + self.git(&[ + "-c", + "user.name=Fixture", + "-c", + "user.email=fixture@example.invalid", + "-c", + "commit.gpgsign=false", + "commit", + "-qm", + "fixture", + ]); + } + } + + impl Drop for SourceCheckout { + fn drop(&mut self) { + std::fs::remove_dir_all(&self.0).unwrap(); + } + } + + #[test] + fn a_clean_tracked_non_utf8_workflow_cannot_make_a_prefix_match_unique() { + struct NoCoordinateReads; + impl RestTransport for NoCoordinateReads { + fn get(&self, path: &str) -> Result { + panic!("incomplete workflow population must not resolve a coordinate: {path}"); + } + } + + let checkout = SourceCheckout::new(); + let workflows = checkout.0.join(".github/workflows"); + std::fs::write(workflows.join("release.yml"), moved_workflow().text).unwrap(); + std::fs::write(workflows.join("release.yml@nightly.yml"), [0xff, 0xfe]).unwrap(); + checkout.commit(); + let before = lock_verifier::checkout_revision(&checkout.0).unwrap(); + let snapshot = snapshot_local(&checkout.0, Some("me/app")); + let after = lock_verifier::checkout_revision(&checkout.0).unwrap(); + assert_eq!(before, after); + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert_eq!(snapshot.files.len(), 1); + assert_eq!(snapshot.files[0].path, "release.yml"); + + let mut observed = run(46, "release.yml@nightly.yml"); + observed.head_sha = Some(before.clone()); + let report = super::collect( + "me/app", + &snapshot, + vec![observed], + &NoCoordinateReads, + Some(&AllowList::default()), + snapshot.notes.clone(), + &SourceEvidence { + head_sha: Some(before), + lock: None, + }, + ); + let finding = &report.runs[0].attributions[0]; + assert_eq!(finding.class, StartupFailureClass::Unattributed); + assert!(finding.evidence.contains("incomplete")); + assert!(finding.proposed_move().is_none()); + assert!(finding.required_allow_list_pattern.is_none()); + assert_eq!(exit_for(&report), ExitCode::from(BLOCKING_EXIT)); + } + + #[test] + fn an_incomplete_graphql_population_cannot_authorize_coordinate_probes() { + struct NoCoordinateReads; + impl RestTransport for NoCoordinateReads { + fn get(&self, path: &str) -> Result { + panic!("incomplete GraphQL population must not resolve a coordinate: {path}"); + } + } + + let response = json!({"data": {"r0": { + "nameWithOwner": "me/app", + "defaultBranchRef": {"target": { + "oid": SHA, + "file": {"object": {"entries": [ + {"name": "release.yml", "type": "blob", "object": { + "text": moved_workflow().text, "isBinary": false, "isTruncated": false + }}, + {"name": "release.yml@nightly.yml", "type": "blob", "object": { + "text": null, "isBinary": true, "isTruncated": false + }} + ]}} + }} + }}}); + let (snapshots, _) = + squabble_forge::parse_chains_response(&[RepoId::new("me/app")], &response); + let snapshot = &snapshots[0]; + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert_eq!(snapshot.files.len(), 1); + let report = super::collect( + "me/app", + snapshot, + vec![run(47, "release.yml@nightly.yml")], + &NoCoordinateReads, + Some(&AllowList::default()), + snapshot.notes.clone(), + &SourceEvidence { + head_sha: Some(SHA.into()), + lock: None, + }, + ); + let finding = &report.runs[0].attributions[0]; + assert_eq!(finding.class, StartupFailureClass::Unattributed); + assert!(finding.proposed_move().is_none()); + assert!(finding.required_allow_list_pattern.is_none()); + assert_eq!(exit_for(&report), ExitCode::from(BLOCKING_EXIT)); + } + #[test] fn ambiguous_workflow_names_cannot_trigger_coordinate_reads_or_moves() { struct NoCoordinateReads; diff --git a/crates/squabble-core/src/chains.rs b/crates/squabble-core/src/chains.rs index c87c8938..fb959a3a 100644 --- a/crates/squabble-core/src/chains.rs +++ b/crates/squabble-core/src/chains.rs @@ -215,7 +215,8 @@ impl Edge { #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] #[serde(tag = "status", rename_all = "kebab-case")] pub enum ScanStatus { - /// Read successfully. `revision` is the commit the files came from, when + /// The complete workflow population was read successfully. `revision` is + /// the commit the files came from, when /// the source knows it (GraphQL always does; a local tree may not). Scanned { #[serde(default)] @@ -259,6 +260,46 @@ pub struct RepoSnapshot { } impl RepoSnapshot { + /// Access workflow files only when the producer reports a complete read and + /// its count agrees with the retained population. A missing Git revision + /// does not make an otherwise complete local read unavailable. + /// + /// This validates snapshot metadata, not the producer's honesty: source + /// adapters must report enumeration, decoding and truncation failures. + /// + /// # Errors + /// + /// Returns an error for unavailable reads, inconsistent counts, duplicate + /// filenames or entries outside the workflow-directory filename contract. + pub fn workflow_files(&self) -> Result<&[WorkflowFile], String> { + match &self.status { + ScanStatus::Scanned { workflow_files, .. } if *workflow_files == self.files.len() => {} + ScanStatus::Scanned { .. } => { + return Err( + "workflow source population count does not match the retained files".into(), + ); + } + ScanStatus::Unavailable { reason } => { + return Err(format!("workflow source population is incomplete: {reason}")); + } + ScanStatus::NotFound => { + return Err( + "workflow source population is unavailable: repository not found".into(), + ); + } + } + let mut names = BTreeSet::new(); + for file in &self.files { + if file.path.contains('/') + || !(file.path.ends_with(".yml") || file.path.ends_with(".yaml")) + || !names.insert(file.path.as_str()) + { + return Err("workflow source population has invalid or duplicate filenames".into()); + } + } + Ok(&self.files) + } + /// The canonical identity, defaulting to the requested one when the source /// could not tell. pub fn canonical_id(&self) -> RepoId { @@ -1076,6 +1117,37 @@ mod tests { edge(from, "ci.yml", to, EdgeKind::Action, None, pin) } + #[test] + fn workflow_population_requires_complete_consistent_metadata_not_a_git_revision() { + let mut snapshot = RepoSnapshot { + repo: r("me/app"), + status: ScanStatus::Scanned { + revision: None, + workflow_files: 1, + }, + files: vec![WorkflowFile { + path: "release.yml".into(), + text: "jobs: {}\n".into(), + }], + notes: Vec::new(), + canonical: None, + }; + assert_eq!(snapshot.workflow_files().unwrap().len(), 1); + snapshot.status = ScanStatus::Scanned { + revision: None, + workflow_files: 2, + }; + assert!(snapshot.workflow_files().unwrap_err().contains("count")); + snapshot.files.push(snapshot.files[0].clone()); + assert!(snapshot.workflow_files().unwrap_err().contains("duplicate")); + snapshot.status = ScanStatus::Unavailable { + reason: "literal workflow could not be decoded".into(), + }; + assert!(snapshot.workflow_files().unwrap_err().contains("incomplete")); + snapshot.status = ScanStatus::NotFound; + assert!(snapshot.workflow_files().is_err()); + } + #[test] fn repo_identity_is_case_insensitive_but_keeps_spelling() { let a = r("Hyperpolymath/MetaManifold-WebUI"); diff --git a/crates/squabble-fight/src/chains.rs b/crates/squabble-fight/src/chains.rs index b28589dc..07882868 100644 --- a/crates/squabble-fight/src/chains.rs +++ b/crates/squabble-fight/src/chains.rs @@ -111,7 +111,14 @@ pub fn graph_from_snapshots<'a>( ) -> ChainGraph { let mut g = ChainGraph::new(); for (snap, role) in snapshots { - g.record_scan(snap.repo.clone(), snap.status.clone()); + let files = snap.workflow_files(); + let status = match (&files, &snap.status) { + (Err(reason), ScanStatus::Scanned { .. }) => ScanStatus::Unavailable { + reason: reason.clone(), + }, + _ => snap.status.clone(), + }; + g.record_scan(snap.repo.clone(), status); if matches!(role, Role::Subject) { g.record_subject(snap.repo.clone()); } @@ -122,10 +129,10 @@ pub fn graph_from_snapshots<'a>( for n in &snap.notes { g.notes.push(format!("{}: {n}", snap.repo)); } - if !matches!(snap.status, ScanStatus::Scanned { .. }) { + let Ok(files) = files else { continue; - } - for f in &snap.files { + }; + for f in files { let counts = match &role { Role::Subject => true, Role::Upstream(files) => files.contains(&f.path), @@ -163,8 +170,10 @@ pub fn upstream_roles(graph: &ChainGraph) -> Vec<(RepoId, Role)> { /// Read a local checkout. `slug` overrides identity; otherwise it is taken /// from the `origin` remote in `.git/config`. Missing identity or a root that -/// is not a directory becomes [`ScanStatus::Unavailable`]. Unreadable workflow -/// directories yield no files; unreadable files are skipped with notes. +/// is not a directory becomes [`ScanStatus::Unavailable`]. A genuinely absent +/// workflow directory is a complete empty read. Enumeration, filename, file +/// type or text-read errors make the snapshot unavailable; retained files are +/// partial diagnostics and cannot qualify edges or filename disambiguation. /// Canonical names are not resolved locally. pub fn snapshot_local(root: &Path, slug: Option<&str>) -> RepoSnapshot { let repo = match slug.map(str::to_string).or_else(|| origin_slug(root)) { @@ -200,34 +209,20 @@ pub fn snapshot_local(root: &Path, slug: Option<&str>) -> RepoSnapshot { }; } - let dir = root.join(".github/workflows"); - let mut files = Vec::new(); - let mut notes = Vec::new(); - if let Ok(entries) = std::fs::read_dir(&dir) { - let mut paths: Vec<_> = entries - .flatten() - .map(|e| e.path()) - .filter(|p| matches!(p.extension().and_then(|e| e.to_str()), Some("yml" | "yaml"))) - .collect(); - paths.sort(); - for p in paths { - let name = p - .file_name() - .and_then(|f| f.to_str()) - .unwrap_or("") - .to_string(); - match std::fs::read_to_string(&p) { - Ok(text) => files.push(WorkflowFile { path: name, text }), - Err(e) => notes.push(format!("could not read {name}: {e}")), - } + let (files, notes) = read_local_workflows(root); + let status = if notes.is_empty() { + ScanStatus::Scanned { + revision: head_revision(root), + workflow_files: files.len(), } - } + } else { + ScanStatus::Unavailable { + reason: notes.join("; "), + } + }; RepoSnapshot { repo, - status: ScanStatus::Scanned { - revision: head_revision(root), - workflow_files: files.len(), - }, + status, files, notes, // A checkout cannot tell whether its own name moved; that needs the @@ -236,6 +231,87 @@ pub fn snapshot_local(root: &Path, slug: Option<&str>) -> RepoSnapshot { } } +fn read_local_workflows(root: &Path) -> (Vec, Vec) { + // Inspect each component so a dangling link or a non-directory cannot + // masquerade as a genuinely absent workflow directory. + for component in [".github", ".github/workflows"] { + let path = root.join(component); + match std::fs::symlink_metadata(&path) { + Ok(metadata) if metadata.is_dir() => {} + Err(error) if error.kind() == std::io::ErrorKind::NotFound => { + return (Vec::new(), Vec::new()); + } + Ok(_) => { + return ( + Vec::new(), + vec![format!("{component} is not a regular directory")], + ); + } + Err(error) => { + return ( + Vec::new(), + vec![format!("could not inspect {component}: {error}")], + ); + } + } + } + + let dir = root.join(".github/workflows"); + let entries = match std::fs::read_dir(&dir) { + Ok(entries) => entries, + Err(error) => { + return ( + Vec::new(), + vec![format!("could not enumerate .github/workflows: {error}")], + ); + } + }; + let mut files = Vec::new(); + let mut notes = Vec::new(); + for entry in entries { + let entry = match entry { + Ok(entry) => entry, + Err(error) => { + notes.push(format!("could not read workflow directory entry: {error}")); + continue; + } + }; + let path = entry.path(); + if !matches!( + path.extension(), + Some(extension) if extension == "yml" || extension == "yaml" + ) { + continue; + } + let name = entry.file_name(); + let Some(name) = name.to_str() else { + notes.push(format!("workflow filename is not UTF-8: {}", path.display())); + continue; + }; + match entry.file_type() { + Ok(kind) if kind.is_dir() => continue, + Ok(kind) if kind.is_file() => {} + Ok(_) => { + notes.push(format!("{name}: workflow is not a regular file")); + continue; + } + Err(error) => { + notes.push(format!("could not inspect {name}: {error}")); + continue; + } + } + match std::fs::read_to_string(&path) { + Ok(text) => files.push(WorkflowFile { + path: name.to_string(), + text, + }), + Err(error) => notes.push(format!("could not read {name}: {error}")), + } + } + files.sort_by(|a, b| a.path.cmp(&b.path)); + (files, notes) +} + /// `owner/repo` from `[remote "origin"] url = …github.com[:/]owner/repo(.git)`. fn origin_slug(root: &Path) -> Option { let cfg = std::fs::read_to_string(root.join(".git/config")).ok()?; @@ -572,6 +648,135 @@ jobs: assert!(g.notes.iter().any(|n| n.contains("partial"))); } + struct LocalSource(std::path::PathBuf); + + impl LocalSource { + fn new() -> Self { + let stamp = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .unwrap() + .as_nanos(); + let root = std::env::temp_dir() + .join(format!("squabble-population-{}-{stamp}", std::process::id())); + std::fs::create_dir(&root).unwrap(); + Self(root) + } + + fn workflows(&self) -> std::path::PathBuf { + let path = self.0.join(".github/workflows"); + std::fs::create_dir_all(&path).unwrap(); + path + } + } + + impl Drop for LocalSource { + fn drop(&mut self) { + std::fs::remove_dir_all(&self.0).unwrap(); + } + } + + #[test] + fn complete_local_reads_without_git_keep_their_unknown_revision() { + let source = LocalSource::new(); + let empty = snapshot_local(&source.0, Some("me/app")); + assert_eq!( + empty.status, + ScanStatus::Scanned { + revision: None, + workflow_files: 0, + } + ); + assert!(empty.workflow_files().unwrap().is_empty()); + + std::fs::create_dir(source.0.join(".github")).unwrap(); + assert!(snapshot_local(&source.0, Some("me/app")) + .workflow_files() + .unwrap() + .is_empty()); + std::fs::write(source.workflows().join("release.yml"), CALLER).unwrap(); + let complete = snapshot_local(&source.0, Some("me/app")); + assert!(matches!( + complete.status, + ScanStatus::Scanned { + revision: None, + workflow_files: 1, + } + )); + assert_eq!(complete.workflow_files().unwrap().len(), 1); + assert!(!graph_from_snapshots([(&complete, Role::Subject)]).edges.is_empty()); + } + + #[test] + fn non_utf8_workflow_contents_make_the_retained_population_unavailable() { + let source = LocalSource::new(); + let workflows = source.workflows(); + std::fs::write(workflows.join("release.yml"), CALLER).unwrap(); + std::fs::write(workflows.join("release.yml@nightly.yml"), [0xff, 0xfe]).unwrap(); + let snapshot = snapshot_local(&source.0, Some("me/app")); + + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert_eq!(snapshot.files.len(), 1); + assert_eq!(snapshot.files[0].path, "release.yml"); + assert!(snapshot.notes.iter().any(|note| note.contains("release.yml@nightly.yml"))); + assert!(snapshot.workflow_files().is_err()); + assert!(graph_from_snapshots([(&snapshot, Role::Subject)]).edges.is_empty()); + } + + #[cfg(unix)] + #[test] + fn an_unrepresentable_workflow_filename_is_not_silently_omitted() { + use std::os::unix::ffi::OsStringExt; + + let source = LocalSource::new(); + let name = std::ffi::OsString::from_vec(b"release\xff.yml".to_vec()); + std::fs::write(source.workflows().join(name), CALLER).unwrap(); + let snapshot = snapshot_local(&source.0, Some("me/app")); + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert!(snapshot.notes.iter().any(|note| note.contains("filename is not UTF-8"))); + assert!(snapshot.workflow_files().is_err()); + } + + #[test] + fn a_workflow_directory_path_that_is_a_file_is_not_an_empty_scan() { + let source = LocalSource::new(); + std::fs::create_dir(source.0.join(".github")).unwrap(); + std::fs::write(source.0.join(".github/workflows"), "not a directory").unwrap(); + let snapshot = snapshot_local(&source.0, Some("me/app")); + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert!(snapshot.workflow_files().is_err()); + } + + #[cfg(unix)] + #[test] + fn a_dangling_workflow_link_is_unavailable_without_a_permission_fixture() { + let source = LocalSource::new(); + let workflows = source.workflows(); + std::fs::write(workflows.join("release.yml"), CALLER).unwrap(); + std::os::unix::fs::symlink( + "missing-target", + workflows.join("release.yml@nightly.yml"), + ) + .unwrap(); + let snapshot = snapshot_local(&source.0, Some("me/app")); + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert!(snapshot.workflow_files().is_err()); + } + + #[test] + fn inconsistent_snapshot_counts_do_not_qualify_graph_edges() { + let mut snapshot = snap("me/app", vec![wf("ci.yml", CALLER)]); + snapshot.status = ScanStatus::Scanned { + revision: Some(SHA.into()), + workflow_files: 2, + }; + let graph = graph_from_snapshots([(&snapshot, Role::Subject)]); + assert!(graph.edges.is_empty()); + assert!(matches!( + graph.scans.get(&RepoId::new("me/app")), + Some(ScanStatus::Unavailable { .. }) + )); + } + #[test] fn local_snapshot_of_a_missing_dir_is_unavailable() { let s = snapshot_local(Path::new("/definitely/not/here"), Some("me/x")); diff --git a/crates/squabble-fight/src/startup.rs b/crates/squabble-fight/src/startup.rs index 2636b4d3..6d4e8d06 100644 --- a/crates/squabble-fight/src/startup.rs +++ b/crates/squabble-fight/src/startup.rs @@ -21,7 +21,7 @@ //! gate. The attribution feeds a report; the run stays failed until the //! workflow genuinely starts and passes. -use squabble_core::chains::{Edge, RepoId, WorkflowFile}; +use squabble_core::chains::{Edge, RepoId, RepoSnapshot, WorkflowFile}; use squabble_core::startup::{ attribute_zero_job, same_source_revision, AllowList, CanonicalResolution, NativeLockStatus, NativeLockVerification, StartupFailureClass, ZeroJobAttribution, ZeroJobRun, @@ -87,18 +87,20 @@ pub fn attribute_workflow( /// `@ref` interpretation and require exactly one match. A collision such as /// `release.yml@nightly.yml` when both it and `release.yml` exist is ambiguous. /// -/// The caller must supply the complete, unmodified workflow tree and establish -/// the run's zero job count and matching source revision before attribution. This function does not -/// resolve or trust the ref suffix as a source revision. +/// The snapshot must report a complete population with consistent metadata. +/// The caller must separately establish the unmodified workflow tree, the run's +/// zero job count and its matching source revision before attribution. This +/// function does not resolve or trust the ref suffix as a source revision. /// /// # Errors /// -/// Returns an error when no source workflow matches or more than one matches. +/// Returns an error for an incomplete source population, no matching workflow +/// or more than one filename/ref interpretation. pub fn resolve_run_workflow<'a>( run: &ZeroJobRun, - files: &'a [WorkflowFile], + source: &'a RepoSnapshot, ) -> Result<&'a WorkflowFile, String> { - let mut candidates = files.iter().filter(|file| { + let mut candidates = source.workflow_files()?.iter().filter(|file| { // Actions workflow files live directly in .github/workflows. if file.path.contains('/') || !(file.path.ends_with(".yml") || file.path.ends_with(".yaml")) { @@ -126,7 +128,7 @@ pub fn resolve_run_workflow<'a>( } } -/// Attribute one failed run from the repo's already-read workflow files. +/// Attribute one failed run from the repo's already-read workflow snapshot. /// /// Attribution requires an observed zero job count and a full run commit ID /// matching `checkout_revision`, which the caller must establish from a @@ -152,7 +154,7 @@ pub fn resolve_run_workflow<'a>( pub fn attribute_run( repo: &str, run: &ZeroJobRun, - files: &[WorkflowFile], + source: &RepoSnapshot, canonical: &BTreeMap, allow_list: Option<&AllowList>, checkout_revision: Option<&str>, @@ -184,7 +186,7 @@ pub fn attribute_run( ), )]; } - let workflow = resolve_run_workflow(run, files); + let workflow = resolve_run_workflow(run, source); if let Some(lock) = lock { if !same_source_revision(Some(&lock.head_sha), checkout_revision) { return vec![unattributed(repo, &run.workflow_file, @@ -401,12 +403,84 @@ pub fn parse_job_count(body: &str) -> Result { #[cfg(test)] mod tests { use super::*; - use squabble_core::chains::EdgeKind; + use squabble_core::chains::{EdgeKind, ScanStatus}; use squabble_core::moves::Move; const CALLER: &str = "hyperpolymath/hypatia"; const SHA: &str = "8f2ee50841e216cd8c192eeb68953118190f105c"; + /// Synthetic complete populations for policy tests, not filesystem receipts. + fn snapshot(files: &[WorkflowFile]) -> RepoSnapshot { + RepoSnapshot { + repo: RepoId::new(CALLER), + status: ScanStatus::Scanned { + revision: Some(SHA.into()), + workflow_files: files.len(), + }, + files: files.to_vec(), + notes: Vec::new(), + canonical: None, + } + } + + fn attribute_run( + repo: &str, + run: &ZeroJobRun, + files: &[WorkflowFile], + canonical: &BTreeMap, + allow_list: Option<&AllowList>, + checkout_revision: Option<&str>, + lock: Option<&NativeLockVerification>, + ) -> Vec { + super::attribute_run( + repo, + run, + &snapshot(files), + canonical, + allow_list, + checkout_revision, + lock, + ) + } + + #[test] + fn incomplete_population_cannot_select_coordinates_or_workflow_lock_findings() { + let mut source = snapshot(&[wf("release.yml", WORKFLOW)]); + source.status = ScanStatus::Unavailable { + reason: "release.yml@nightly.yml could not be decoded".into(), + }; + let observed = run(42, "release.yml@nightly.yml"); + let names = canonical(&[( + "old/standards", + CanonicalResolution::Moved { + canonical: "new/standards".into(), + }, + )]); + assert!(resolve_run_workflow(&observed, &source) + .unwrap_err() + .contains("incomplete")); + + let mut coverage = native_lock(NativeLockStatus::CoverageMismatch); + coverage.exit_code = Some(1); + coverage.stdout = + r#"{"workflows":[{"path":".github/workflows/release.yml","valid":false}]}"#.into(); + for lock in [None, Some(&coverage)] { + let out = super::attribute_run( + CALLER, + &observed, + &source, + &names, + Some(&AllowList::default()), + Some(SHA), + lock, + ); + assert_eq!(out[0].class, StartupFailureClass::Unattributed); + assert!(out[0].evidence.contains("incomplete")); + assert!(out[0].proposed_move().is_none()); + assert!(out[0].required_allow_list_pattern.is_none()); + } + } + #[test] fn missing_or_different_source_cannot_borrow_current_workflow_attribution() { let files = [wf("ci.yml", WORKFLOW)]; @@ -891,9 +965,10 @@ jobs: wf("ci.yml", WORKFLOW), wf("build.yml", WORKFLOW), ]; + let source = snapshot(&files); let resolved: Vec<_> = runs .iter() - .map(|run| resolve_run_workflow(run, &files).unwrap().path.as_str()) + .map(|run| resolve_run_workflow(run, &source).unwrap().path.as_str()) .collect(); assert_eq!(resolved, ["gov.yml", "ci.yml", "build.yml", "build.yml"]); } @@ -989,7 +1064,7 @@ jobs: let observed = run(36, "release.yml@nightly.yml"); let literal_only = [literal.clone()]; assert_eq!( - resolve_run_workflow(&observed, &literal_only).unwrap().path, + resolve_run_workflow(&observed, &snapshot(&literal_only)).unwrap().path, "release.yml@nightly.yml" ); @@ -1021,7 +1096,7 @@ jobs: "release.yml@nightly.yml@refs/heads/main", ] { let observed = run(37, path); - assert!(resolve_run_workflow(&observed, &files) + assert!(resolve_run_workflow(&observed, &snapshot(&files)) .unwrap_err() .contains("ambiguous")); let out = attribute_run( @@ -1057,7 +1132,7 @@ jobs: }]}) .to_string(); let observed = parse_startup_runs(&body).unwrap().remove(0); - assert!(resolve_run_workflow(&observed, &files).is_err(), "{path}"); + assert!(resolve_run_workflow(&observed, &snapshot(&files)).is_err(), "{path}"); } } diff --git a/crates/squabble-forge/src/lib.rs b/crates/squabble-forge/src/lib.rs index 7c3f6a3d..c7f284a8 100644 --- a/crates/squabble-forge/src/lib.rs +++ b/crates/squabble-forge/src/lib.rs @@ -25,6 +25,7 @@ pub mod pr_done; use serde_json::{json, Value}; use squabble_core::chains::{RepoId, RepoSnapshot, ScanStatus, SourceCost, WorkflowFile}; +use std::collections::BTreeSet; use std::io::Write; use std::process::{Command, Stdio}; @@ -140,6 +141,15 @@ pub fn parse_chains_response( }) }); + if resp.get("errors").is_some_and(|errors| !errors.is_array()) { + return ( + batch + .iter() + .map(|repo| unavailable(repo, "malformed GraphQL error population".into())) + .collect(), + rate, + ); + } let errors: Vec<&Value> = resp .get("errors") .and_then(Value::as_array) @@ -151,7 +161,7 @@ pub fn parse_chains_response( .and_then(Value::as_array) .and_then(|p| p.first()) .and_then(Value::as_str) - == Some(alias) + .is_none_or(|first| first == alias) }) }; let top_level_reason = || { @@ -176,7 +186,19 @@ pub fn parse_chains_response( return unavailable(repo, top_level_reason()); }; match data.get(&alias) { - Some(node) if node.is_object() => parse_repo(repo, node), + Some(node) if node.is_object() => { + let mut snapshot = parse_repo(repo, node); + if let Some(error) = error_for(&alias) { + let reason = error + .get("message") + .and_then(Value::as_str) + .unwrap_or("GraphQL field error without a message"); + let reason = format!("workflow source has a GraphQL read error: {reason}"); + snapshot.notes.push(reason.clone()); + snapshot.status = ScanStatus::Unavailable { reason }; + } + snapshot + } _ => match error_for(&alias) { Some(e) if e.get("type").and_then(Value::as_str) == Some("NOT_FOUND") => { RepoSnapshot { @@ -214,12 +236,13 @@ fn unavailable(repo: &RepoId, reason: String) -> RepoSnapshot { } } -/// Build a scanned snapshot from a repository node, retaining the requested -/// identity and any different canonical name. Missing branches or workflow -/// entries yield no files; unreadable blobs are skipped with notes, while -/// truncated text is retained with a caveat. +/// Build a snapshot from the complete workflow-directory response. Explicitly +/// absent branches or directories are empty reads. Missing/malformed entries, +/// unreadable or binary blobs and truncated text are unavailable reads; retain +/// partial text, canonical identity and diagnostics without qualifying edges. fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { let mut notes = Vec::new(); + let mut incomplete = Vec::new(); let mut canonical = None; if let Some(canon) = node.get("nameWithOwner").and_then(Value::as_str) { if RepoId::new(canon) != *repo { @@ -232,58 +255,116 @@ fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { )); } } - let commit = node.pointer("/defaultBranchRef/target"); + let branch = node.get("defaultBranchRef"); + let commit = branch + .and_then(|branch| branch.get("target")) + .filter(|target| target.is_object()); let revision = commit - .and_then(|c| c.get("oid")) + .and_then(|commit| commit.get("oid")) .and_then(Value::as_str) .map(str::to_ascii_lowercase); - if node.get("defaultBranchRef").is_none_or(Value::is_null) { - notes.push("no default branch (empty repository?)".into()); - } + let entries = match branch { + Some(Value::Null) => { + notes.push("no default branch (empty repository?)".into()); + None + } + Some(Value::Object(_)) => match commit { + Some(commit) => match commit.get("file") { + Some(Value::Null) => None, + Some(file) => match file.pointer("/object/entries").and_then(Value::as_array) { + Some(entries) => Some(entries), + None => { + incomplete + .push("workflow directory entries are missing or malformed".into()); + None + } + }, + None => { + incomplete.push("workflow directory result is missing".into()); + None + } + }, + None => { + incomplete.push("default branch commit is missing or malformed".into()); + None + } + }, + _ => { + incomplete.push("default branch result is missing or malformed".into()); + None + } + }; let mut files = Vec::new(); - let entries = commit - .and_then(|c| c.pointer("/file/object/entries")) - .and_then(Value::as_array); + let mut names = BTreeSet::new(); for entry in entries.into_iter().flatten() { - let name = entry - .get("name") - .and_then(Value::as_str) - .unwrap_or_default(); - let is_blob = entry.get("type").and_then(Value::as_str) == Some("blob"); - if !is_blob || !(name.ends_with(".yml") || name.ends_with(".yaml")) { + let name = match entry.get("name").and_then(Value::as_str) { + Some(name) if !name.is_empty() && !name.contains('/') => name, + _ => { + incomplete.push("workflow directory entry has no valid filename".into()); + continue; + } + }; + if !names.insert(name) { + incomplete.push(format!("{name}: duplicate workflow directory entry")); + continue; + } + match entry.get("type").and_then(Value::as_str) { + Some("blob") => {} + Some("tree" | "commit") => continue, + _ => { + incomplete.push(format!("{name}: workflow directory entry has an unknown type")); + continue; + } + } + if !(name.ends_with(".yml") || name.ends_with(".yaml")) { continue; } let blob = entry.get("object"); - let text = blob.and_then(|b| b.get("text")).and_then(Value::as_str); + let text = blob.and_then(|blob| blob.get("text")).and_then(Value::as_str); + let binary = blob + .and_then(|blob| blob.get("isBinary")) + .and_then(Value::as_bool); let truncated = blob - .and_then(|b| b.get("isTruncated")) - .and_then(Value::as_bool) - .unwrap_or(false); + .and_then(|blob| blob.get("isTruncated")) + .and_then(Value::as_bool); + match truncated { + Some(false) => {} + Some(true) => incomplete.push(format!( + "{name}: text truncated by the API; references past the cut are missing" + )), + None => incomplete.push(format!("{name}: truncation status is missing or malformed")), + } + match binary { + Some(false) => {} + Some(true) => incomplete.push(format!("{name}: workflow blob is binary")), + None => incomplete.push(format!("{name}: binary status is missing or malformed")), + } match text { - Some(t) => { - if truncated { - notes.push(format!( - "{name}: text truncated by the API; references past the cut are missing" - )); - } - files.push(WorkflowFile { - path: name.to_string(), - text: t.to_string(), - }); - } - None => notes.push(format!( + Some(text) => files.push(WorkflowFile { + path: name.to_string(), + text: text.to_string(), + }), + None => incomplete.push(format!( "{name}: no text returned (binary or unreadable); skipped" )), } } - RepoSnapshot { - repo: repo.clone(), - status: ScanStatus::Scanned { + let status = if incomplete.is_empty() { + ScanStatus::Scanned { revision, workflow_files: files.len(), - }, + } + } else { + ScanStatus::Unavailable { + reason: incomplete.join("; "), + } + }; + notes.extend(incomplete); + RepoSnapshot { + repo: repo.clone(), + status, files, notes, canonical, @@ -457,6 +538,77 @@ mod tests { assert!(notes.contains("big.yml: text truncated")); assert!(notes.contains("odd.yml: no text returned")); assert_eq!(snaps[0].files.len(), 1); + assert!(matches!(snaps[0].status, ScanStatus::Unavailable { .. })); + assert!(snaps[0].workflow_files().is_err()); + } + + #[test] + fn malformed_or_omitted_population_fields_are_not_complete_empty_reads() { + let valid = json!({ + "name": "release.yml", "type": "blob", + "object": {"text": "jobs: {}\n", "isBinary": false, "isTruncated": false} + }); + let mut missing_file = tree(json!([])); + missing_file["defaultBranchRef"]["target"] + .as_object_mut() + .unwrap() + .remove("file"); + let mut missing_flag = valid.clone(); + missing_flag["object"] + .as_object_mut() + .unwrap() + .remove("isTruncated"); + for node in [ + json!({}), + json!({"defaultBranchRef": {}}), + missing_file, + tree(Value::Null), + tree(json!([null])), + tree(json!([{"name": "release.yml", "object": {}}])), + tree(json!([{"name": "../release.yml", "type": "blob", "object": {}}])), + tree(json!([valid.clone(), valid.clone()])), + tree(json!([missing_flag])), + ] { + let response = json!({"data": {"r0": node}}); + let (snapshots, _) = parse_chains_response(&repos(&["me/app"]), &response); + assert!(matches!(snapshots[0].status, ScanStatus::Unavailable { .. })); + assert!(snapshots[0].workflow_files().is_err()); + assert!(!snapshots[0].notes.is_empty()); + } + } + + #[test] + fn graphql_field_errors_disqualify_partial_data_without_losing_identity_or_text() { + let mut node = tree(json!([{ + "name": "release.yml", "type": "blob", + "object": {"text": "jobs: {}\n", "isBinary": false, "isTruncated": false} + }])); + node["nameWithOwner"] = json!("me/new-name"); + for path in [json!(["r0", "defaultBranchRef", "target", "file"]), Value::Null] { + let response = json!({ + "data": {"r0": node.clone()}, + "errors": [{"path": path, "message": "workflow read interrupted"}] + }); + let (snapshots, _) = parse_chains_response(&repos(&["me/old-name"]), &response); + let snapshot = &snapshots[0]; + assert_eq!(snapshot.repo, RepoId::new("me/old-name")); + assert_eq!(snapshot.canonical.as_deref(), Some("me/new-name")); + assert_eq!(snapshot.files.len(), 1); + assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); + assert!(snapshot.notes.iter().any(|note| note.contains("read interrupted"))); + assert!(snapshot.workflow_files().is_err()); + } + } + + #[test] + fn malformed_error_populations_cannot_qualify_apparently_complete_data() { + let response = json!({ + "data": {"r0": tree(json!([]))}, + "errors": {"message": "wrong shape"} + }); + let (snapshots, _) = parse_chains_response(&repos(&["me/app"]), &response); + assert!(matches!(snapshots[0].status, ScanStatus::Unavailable { .. })); + assert!(snapshots[0].workflow_files().is_err()); } #[test] diff --git a/docs/CREUSOT.adoc b/docs/CREUSOT.adoc index f8d430e4..a3d0c173 100644 --- a/docs/CREUSOT.adoc +++ b/docs/CREUSOT.adoc @@ -46,9 +46,12 @@ records the following source and execution evidence: 20:55:09 UTC; the gate reported every obligation discharged and zero trusted axioms. -| Verdict -| Job `126858835478` concluded success after detection, theatre and proof jobs - succeeded. +| Aggregate verdict (separate from prover execution) +| https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126858835478[Verdict job 126858835478] + adjudicated the successful detection, theatre and proof results. The actual + planted controls and caller proof ran in + https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[proof job 126852164109] + linked above. |=== This receipt discharges the contracts in the separate verification crate at diff --git a/verification/README.adoc b/verification/README.adoc index 7e4d0a67..5b7970a4 100644 --- a/verification/README.adoc +++ b/verification/README.adoc @@ -5,8 +5,15 @@ == Rust: the Creusot complement Rust obligations live in `squabble-creusot/` (the Rust twin of `spark/` and of -the proofs under `proofs/`). They are **stated, not proved**: no obligation has -been discharged yet. See `../docs/CREUSOT.adoc` and `squabble-creusot/README.adoc`. +the proofs under `proofs/`). A hosted proof run discharged the verification +crate's obligations at merge revision +`f9499a8de0b8c525459a669e2cdbcacf83a49b85`: +https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[the proof job] +rejected the false control, proved the true control and reported +`Proved (13 files)` with zero trusted axioms. This receipt applies to that +source, not every later commit or the whole operational engine. Stable mirror +execution is a separate obligation. See link:../docs/CREUSOT.adoc[the source-bound +receipt] and link:squabble-creusot/README.adoc[the crate's scope]. [source,sh] ---- diff --git a/verification/squabble-creusot/Cargo.toml b/verification/squabble-creusot/Cargo.toml index 2c2a8a8f..a7fc4a55 100644 --- a/verification/squabble-creusot/Cargo.toml +++ b/verification/squabble-creusot/Cargo.toml @@ -4,7 +4,7 @@ name = "squabble-creusot" version = "0.1.0" edition = "2021" -description = "Creusot contracts for the squabbler's load-bearing invariants — stated, not yet discharged" +description = "Creusot contracts for the squabbler's load-bearing invariants; source-bound proof receipt in docs/CREUSOT.adoc" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell (hyperpolymath) "] repository = "https://github.com/hyperpolymath/cicd-squabbler" diff --git a/verification/squabble-creusot/src/lib.rs b/verification/squabble-creusot/src/lib.rs index bbb19984..0f4b36a5 100644 --- a/verification/squabble-creusot/src/lib.rs +++ b/verification/squabble-creusot/src/lib.rs @@ -19,16 +19,17 @@ //! a **literal** `#[requires]`/`#[ensures]` pair per obligation, which is what //! the estate gate counts. //! -//! # Status: stated, not discharged -//! -//! These obligations have been **written, never proved**. No run has reached -//! Why3: the environment this crate was added in has no Rust toolchain, and -//! this repository's own Rust CI currently dies as a zero-job -//! `startup_failure`, so CI has not compiled the workspace either. The estate -//! gate (`hyperpolymath/cicd-suite`'s `creusot-check`) reports exactly that -//! distinction — it fails a claim of proof that has no contracts behind it, and -//! refuses to report a verdict when the prover cannot be shown to work. Do not describe this crate as verified until a `prove` run -//! discharges every obligation; the honest phrase is **stated, not proved**. +//! # Status: source-bound hosted proof receipt +//! +//! Run 41909189438, proof job 126852164109, discharged this verification crate +//! at merge revision f9499a8de0b8c525459a669e2cdbcacf83a49b85. It rejected the +//! false control, proved the true control, and reported Proved (13 files) with +//! zero trusted axioms. See docs/CREUSOT.adoc for the full source and gate pins: +//! . +//! +//! That receipt does not prove the whole operational engine or later source. +//! The stable mirror tests remain a separate validation step, and a new +//! revision needs its own qualification before receiving a proof claim. //! //! # Why a separate crate //! From 4ee55d146023c8b07a53926c306c722b439c1295 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 22:05:05 +0000 Subject: [PATCH 5/7] style: apply hosted formatter output for workflow population guards Apply the exact sixteen rustfmt hunks from job126894630388. No source contract, assertion or check is removed. --- crates/squabble-core/src/chains.rs | 9 +++++-- crates/squabble-fight/src/chains.rs | 36 ++++++++++++++++++---------- crates/squabble-fight/src/startup.rs | 9 +++++-- crates/squabble-forge/src/lib.rs | 28 +++++++++++++++++----- 4 files changed, 60 insertions(+), 22 deletions(-) diff --git a/crates/squabble-core/src/chains.rs b/crates/squabble-core/src/chains.rs index fb959a3a..f2b00052 100644 --- a/crates/squabble-core/src/chains.rs +++ b/crates/squabble-core/src/chains.rs @@ -280,7 +280,9 @@ impl RepoSnapshot { ); } ScanStatus::Unavailable { reason } => { - return Err(format!("workflow source population is incomplete: {reason}")); + return Err(format!( + "workflow source population is incomplete: {reason}" + )); } ScanStatus::NotFound => { return Err( @@ -1143,7 +1145,10 @@ mod tests { snapshot.status = ScanStatus::Unavailable { reason: "literal workflow could not be decoded".into(), }; - assert!(snapshot.workflow_files().unwrap_err().contains("incomplete")); + assert!(snapshot + .workflow_files() + .unwrap_err() + .contains("incomplete")); snapshot.status = ScanStatus::NotFound; assert!(snapshot.workflow_files().is_err()); } diff --git a/crates/squabble-fight/src/chains.rs b/crates/squabble-fight/src/chains.rs index 07882868..07e5fbaa 100644 --- a/crates/squabble-fight/src/chains.rs +++ b/crates/squabble-fight/src/chains.rs @@ -285,7 +285,10 @@ fn read_local_workflows(root: &Path) -> (Vec, Vec) { } let name = entry.file_name(); let Some(name) = name.to_str() else { - notes.push(format!("workflow filename is not UTF-8: {}", path.display())); + notes.push(format!( + "workflow filename is not UTF-8: {}", + path.display() + )); continue; }; match entry.file_type() { @@ -656,8 +659,10 @@ jobs: .duration_since(std::time::UNIX_EPOCH) .unwrap() .as_nanos(); - let root = std::env::temp_dir() - .join(format!("squabble-population-{}-{stamp}", std::process::id())); + let root = std::env::temp_dir().join(format!( + "squabble-population-{}-{stamp}", + std::process::id() + )); std::fs::create_dir(&root).unwrap(); Self(root) } @@ -703,7 +708,9 @@ jobs: } )); assert_eq!(complete.workflow_files().unwrap().len(), 1); - assert!(!graph_from_snapshots([(&complete, Role::Subject)]).edges.is_empty()); + assert!(!graph_from_snapshots([(&complete, Role::Subject)]) + .edges + .is_empty()); } #[test] @@ -717,9 +724,14 @@ jobs: assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); assert_eq!(snapshot.files.len(), 1); assert_eq!(snapshot.files[0].path, "release.yml"); - assert!(snapshot.notes.iter().any(|note| note.contains("release.yml@nightly.yml"))); + assert!(snapshot + .notes + .iter() + .any(|note| note.contains("release.yml@nightly.yml"))); assert!(snapshot.workflow_files().is_err()); - assert!(graph_from_snapshots([(&snapshot, Role::Subject)]).edges.is_empty()); + assert!(graph_from_snapshots([(&snapshot, Role::Subject)]) + .edges + .is_empty()); } #[cfg(unix)] @@ -732,7 +744,10 @@ jobs: std::fs::write(source.workflows().join(name), CALLER).unwrap(); let snapshot = snapshot_local(&source.0, Some("me/app")); assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); - assert!(snapshot.notes.iter().any(|note| note.contains("filename is not UTF-8"))); + assert!(snapshot + .notes + .iter() + .any(|note| note.contains("filename is not UTF-8"))); assert!(snapshot.workflow_files().is_err()); } @@ -752,11 +767,8 @@ jobs: let source = LocalSource::new(); let workflows = source.workflows(); std::fs::write(workflows.join("release.yml"), CALLER).unwrap(); - std::os::unix::fs::symlink( - "missing-target", - workflows.join("release.yml@nightly.yml"), - ) - .unwrap(); + std::os::unix::fs::symlink("missing-target", workflows.join("release.yml@nightly.yml")) + .unwrap(); let snapshot = snapshot_local(&source.0, Some("me/app")); assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); assert!(snapshot.workflow_files().is_err()); diff --git a/crates/squabble-fight/src/startup.rs b/crates/squabble-fight/src/startup.rs index 6d4e8d06..3849fde3 100644 --- a/crates/squabble-fight/src/startup.rs +++ b/crates/squabble-fight/src/startup.rs @@ -1064,7 +1064,9 @@ jobs: let observed = run(36, "release.yml@nightly.yml"); let literal_only = [literal.clone()]; assert_eq!( - resolve_run_workflow(&observed, &snapshot(&literal_only)).unwrap().path, + resolve_run_workflow(&observed, &snapshot(&literal_only)) + .unwrap() + .path, "release.yml@nightly.yml" ); @@ -1132,7 +1134,10 @@ jobs: }]}) .to_string(); let observed = parse_startup_runs(&body).unwrap().remove(0); - assert!(resolve_run_workflow(&observed, &snapshot(&files)).is_err(), "{path}"); + assert!( + resolve_run_workflow(&observed, &snapshot(&files)).is_err(), + "{path}" + ); } } diff --git a/crates/squabble-forge/src/lib.rs b/crates/squabble-forge/src/lib.rs index c7f284a8..ad24c4e0 100644 --- a/crates/squabble-forge/src/lib.rs +++ b/crates/squabble-forge/src/lib.rs @@ -313,7 +313,9 @@ fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { Some("blob") => {} Some("tree" | "commit") => continue, _ => { - incomplete.push(format!("{name}: workflow directory entry has an unknown type")); + incomplete.push(format!( + "{name}: workflow directory entry has an unknown type" + )); continue; } } @@ -321,7 +323,9 @@ fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { continue; } let blob = entry.get("object"); - let text = blob.and_then(|blob| blob.get("text")).and_then(Value::as_str); + let text = blob + .and_then(|blob| blob.get("text")) + .and_then(Value::as_str); let binary = blob .and_then(|blob| blob.get("isBinary")) .and_then(Value::as_bool); @@ -571,7 +575,10 @@ mod tests { ] { let response = json!({"data": {"r0": node}}); let (snapshots, _) = parse_chains_response(&repos(&["me/app"]), &response); - assert!(matches!(snapshots[0].status, ScanStatus::Unavailable { .. })); + assert!(matches!( + snapshots[0].status, + ScanStatus::Unavailable { .. } + )); assert!(snapshots[0].workflow_files().is_err()); assert!(!snapshots[0].notes.is_empty()); } @@ -584,7 +591,10 @@ mod tests { "object": {"text": "jobs: {}\n", "isBinary": false, "isTruncated": false} }])); node["nameWithOwner"] = json!("me/new-name"); - for path in [json!(["r0", "defaultBranchRef", "target", "file"]), Value::Null] { + for path in [ + json!(["r0", "defaultBranchRef", "target", "file"]), + Value::Null, + ] { let response = json!({ "data": {"r0": node.clone()}, "errors": [{"path": path, "message": "workflow read interrupted"}] @@ -595,7 +605,10 @@ mod tests { assert_eq!(snapshot.canonical.as_deref(), Some("me/new-name")); assert_eq!(snapshot.files.len(), 1); assert!(matches!(snapshot.status, ScanStatus::Unavailable { .. })); - assert!(snapshot.notes.iter().any(|note| note.contains("read interrupted"))); + assert!(snapshot + .notes + .iter() + .any(|note| note.contains("read interrupted"))); assert!(snapshot.workflow_files().is_err()); } } @@ -607,7 +620,10 @@ mod tests { "errors": {"message": "wrong shape"} }); let (snapshots, _) = parse_chains_response(&repos(&["me/app"]), &response); - assert!(matches!(snapshots[0].status, ScanStatus::Unavailable { .. })); + assert!(matches!( + snapshots[0].status, + ScanStatus::Unavailable { .. } + )); assert!(snapshots[0].workflow_files().is_err()); } From 4534cf1dde4d16e3e70e242a8b62369394d74ded Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 22:23:20 +0000 Subject: [PATCH 6/7] docs: scope Creusot receipts to their source and counted evidence --- README.adoc | 7 +++++-- docs/CREUSOT.adoc | 10 ++++++---- docs/status/PROOF-STATUS.adoc | 8 +++++--- verification/squabble-creusot/README.adoc | 6 ++++-- verification/squabble-creusot/src/contracts.rs | 9 ++++++--- verification/squabble-creusot/src/lib.rs | 7 +++++-- 6 files changed, 31 insertions(+), 16 deletions(-) diff --git a/README.adoc b/README.adoc index 827e35c7..0f461ed7 100644 --- a/README.adoc +++ b/README.adoc @@ -221,8 +221,11 @@ just verify-creusot # the prover: discharge the obligations https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[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)`; the gate -reported zero trusted axioms). That checkout combines PR head +`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 diff --git a/docs/CREUSOT.adoc b/docs/CREUSOT.adoc index a3d0c173..ac141406 100644 --- a/docs/CREUSOT.adoc +++ b/docs/CREUSOT.adoc @@ -43,8 +43,9 @@ records the following source and execution evidence: | Calling crate | `verification/squabble-creusot`: `Proved (13 files)` at - 20:55:09 UTC; the gate reported every obligation discharged and zero - trusted axioms. + 20:55:09 UTC; the gate reported every obligation discharged. Its + `trusted axioms: 0` field counted lines containing the literal `#[trusted]` + in tracked Rust files, not axioms from dependencies or the prover. | Aggregate verdict (separate from prover execution) | https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126858835478[Verdict job 126858835478] @@ -54,8 +55,9 @@ records the following source and execution evidence: linked above. |=== -This receipt discharges the contracts in the separate verification crate at -the named merge revision. It is not a proof of all operational Rust code, and +`Proved (13 files)` is the prover's file-level result for this crate, not a +count of independent theorems. This receipt discharges the contracts in the +separate verification crate at the named merge revision. It is not a proof of all operational Rust code, and it does not certify later commits or the default branch merely because they contain this document. The stable mirror tests, which compare the model with `squabble-core`, remain a separate validation step; this proof receipt does diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 2ec7342e..f103b2a3 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -10,9 +10,11 @@ On 2026-11-04, https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[proof job 126852164109] rejected the planted false control, proved the true control, and discharged the contracts in `verification/squabble-creusot` at merge checkout -`f9499a8de0b8c525459a669e2cdbcacf83a49b85`. It reported `Proved (13 files)`; -the gate reported zero trusted axioms. The exact head, base and gate source -are recorded in `../CREUSOT.adoc`. +`f9499a8de0b8c525459a669e2cdbcacf83a49b85`. Its `Proved (13 files)` result +counts files, not independent theorems. 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. The exact head, base and +gate source are recorded in `../CREUSOT.adoc`. This result applies to that contract crate and source revision. It does not complete the ABI/typing template obligations below or certify later source, diff --git a/verification/squabble-creusot/README.adoc b/verification/squabble-creusot/README.adoc index ce1defd9..da27e2f4 100644 --- a/verification/squabble-creusot/README.adoc +++ b/verification/squabble-creusot/README.adoc @@ -9,8 +9,10 @@ engine's load-bearing invariants to a prover instead of only testing them. https://github.com/hyperpolymath/cicd-squabbler/actions/runs/41909189438/job/126852164109[Hosted job 126852164109] on 2026-11-04 rejected the false control, proved the true control, and reported `Proved (13 files)` for this crate at -`f9499a8de0b8c525459a669e2cdbcacf83a49b85`, with zero trusted axioms reported -by the gate. This is the merge of PR head +`f9499a8de0b8c525459a669e2cdbcacf83a49b85`. That is a 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. This is the merge of PR head `1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848` into base `17284299184fd31a10c7bf382f02262cd0ab308c`. The receipt covers these contracts at that source, not later revisions or the full operational engine. The stable diff --git a/verification/squabble-creusot/src/contracts.rs b/verification/squabble-creusot/src/contracts.rs index 4c95ca16..b169be13 100644 --- a/verification/squabble-creusot/src/contracts.rs +++ b/verification/squabble-creusot/src/contracts.rs @@ -7,9 +7,12 @@ //! mirrors one function in [`crate::model`] — keep the pair in step; the model //! carries the tests that fail when the real implementation drifts. //! -//! **Status: stated, not discharged.** No obligation here has been proved: this -//! environment has no Rust toolchain at all, and the repository's own Rust CI -//! does not start (zero-job `startup_failure`). See `../../docs/CREUSOT.adoc`. +//! **Status: source-bound hosted proof recorded.** Proof job 126852164109 +//! discharged this verification crate at merge revision +//! f9499a8de0b8c525459a669e2cdbcacf83a49b85. That historical receipt qualifies +//! that checkout only; later revisions require their own proof evidence. +//! See docs/CREUSOT.adoc for the recorded source, gate and scope: +//! . use creusot_std::prelude::*; diff --git a/verification/squabble-creusot/src/lib.rs b/verification/squabble-creusot/src/lib.rs index 0f4b36a5..32f812d2 100644 --- a/verification/squabble-creusot/src/lib.rs +++ b/verification/squabble-creusot/src/lib.rs @@ -23,8 +23,11 @@ //! //! Run 41909189438, proof job 126852164109, discharged this verification crate //! at merge revision f9499a8de0b8c525459a669e2cdbcacf83a49b85. It rejected the -//! false control, proved the true control, and reported Proved (13 files) with -//! zero trusted axioms. See docs/CREUSOT.adoc for the full source and gate pins: +//! false control, proved the true control, and reported Proved (13 files), a +//! file-level result rather than a theorem count. The gate's zero trusted-axiom +//! field counts lines with the exact trusted-attribute spelling in tracked Rust +//! files only; it does not count dependency or prover axioms. See docs/CREUSOT.adoc +//! for the spelling, full source and gate pins: //! . //! //! That receipt does not prove the whole operational engine or later source. From 36a150d99d39a7c18a34e6e4fa4d067549d44296 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 22:42:02 +0000 Subject: [PATCH 7/7] refactor(forge): separate workflow-entry parsing from repository metadata Retain partial-read diagnostics and the complete-population refusal contract while reducing the parser's cognitive complexity. --- crates/squabble-forge/src/lib.rs | 49 +++++++++++++++++++------------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/crates/squabble-forge/src/lib.rs b/crates/squabble-forge/src/lib.rs index ad24c4e0..12af879f 100644 --- a/crates/squabble-forge/src/lib.rs +++ b/crates/squabble-forge/src/lib.rs @@ -295,6 +295,35 @@ fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { } }; + let files = read_workflow_entries(entries.map(Vec::as_slice), &mut incomplete); + + let status = if incomplete.is_empty() { + ScanStatus::Scanned { + revision, + workflow_files: files.len(), + } + } else { + ScanStatus::Unavailable { + reason: incomplete.join("; "), + } + }; + notes.extend(incomplete); + RepoSnapshot { + repo: repo.clone(), + status, + files, + notes, + canonical, + } +} + +/// Read each workflow blob while retaining every population-completeness error. +/// Partial text remains diagnostic input; the caller refuses a scanned status +/// whenever this helper records a missing, duplicate, binary or truncated entry. +fn read_workflow_entries( + entries: Option<&[Value]>, + incomplete: &mut Vec, +) -> Vec { let mut files = Vec::new(); let mut names = BTreeSet::new(); for entry in entries.into_iter().flatten() { @@ -354,25 +383,7 @@ fn parse_repo(repo: &RepoId, node: &Value) -> RepoSnapshot { )), } } - - let status = if incomplete.is_empty() { - ScanStatus::Scanned { - revision, - workflow_files: files.len(), - } - } else { - ScanStatus::Unavailable { - reason: incomplete.join("; "), - } - }; - notes.extend(incomplete); - RepoSnapshot { - repo: repo.clone(), - status, - files, - notes, - canonical, - } + files } /// Read the workflow directories of `repos` in batches. Returns one snapshot