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..0f461ed7 100644 --- a/README.adoc +++ b/README.adoc @@ -217,12 +217,21 @@ 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)` is the +prover's file-level result, not a theorem count. The gate's zero trusted-axiom +field counts only tracked Rust lines containing the literal `#[trusted]`; +it does not count axioms from dependencies or the prover. That checkout combines +PR head +`1fd9db9bb94d9ac8ed54f7a6ef4f8c51ff35a848` with base +`17284299184fd31a10c7bf382f02262cd0ab308c`. This receipt covers the separate +contract crate at that revision; later revisions and the operational engine +need their own validation. The gate still reports *no proof performed* when +it cannot establish a working prover. Scope, historical environment failures +and the licence note: `docs/CREUSOT.adoc`. == Downstream integration contracts (pinned, immutable revisions) @@ -280,7 +289,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-cli/src/zero_job.rs b/crates/squabble-cli/src/zero_job.rs index 5b2a7427..e87b8e17 100644 --- a/crates/squabble-cli/src/zero_job.rs +++ b/crates/squabble-cli/src/zero_job.rs @@ -38,13 +38,15 @@ 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, }; 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; @@ -135,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); } @@ -214,7 +212,7 @@ pub fn run(rest: &[String]) -> ExitCode { } else { collect( &slug, - &snapshot.files, + &snapshot, runs, &GhRest, allow_list.as_ref(), @@ -274,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>, @@ -288,7 +286,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, snapshot) { for edge in extract_edges(&RepoId::new(slug), file) { repos.insert(edge.to); } @@ -325,7 +323,7 @@ fn collect( attributions: attribute_run( slug, &run, - files, + snapshot, &canonical, allow_list, source.head_sha.as_deref(), @@ -490,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; @@ -506,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, @@ -705,6 +714,228 @@ 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)); + } + } + + 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; + 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/chains.rs b/crates/squabble-core/src/chains.rs index 66ee8569..f2b00052 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,48 @@ 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 +1119,40 @@ 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"); @@ -1548,7 +1625,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-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/chains.rs b/crates/squabble-fight/src/chains.rs index 71f8eb85..07e5fbaa 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,90 @@ 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()?; @@ -297,7 +376,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 +502,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 @@ -462,6 +651,144 @@ 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 21ead9af..3849fde3 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, @@ -79,7 +79,56 @@ pub fn attribute_workflow( out } -/// Attribute one failed run from the repo's already-read workflow files. +/// 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 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 for an incomplete source population, no matching workflow +/// or more than one filename/ref interpretation. +pub fn resolve_run_workflow<'a>( + run: &ZeroJobRun, + source: &'a RepoSnapshot, +) -> Result<&'a WorkflowFile, String> { + 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")) + { + 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 snapshot. /// /// Attribution requires an observed zero job count and a full run commit ID /// matching `checkout_revision`, which the caller must establish from a @@ -92,10 +141,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 @@ -105,7 +154,7 @@ pub fn attribute_workflow( pub fn attribute_run( repo: &str, run: &ZeroJobRun, - files: &[WorkflowFile], + source: &RepoSnapshot, canonical: &BTreeMap, allow_list: Option<&AllowList>, checkout_revision: Option<&str>, @@ -137,6 +186,7 @@ pub fn attribute_run( ), )]; } + 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, @@ -145,16 +195,21 @@ 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 +218,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 +248,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 +304,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,11 +350,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); - 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) @@ -351,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)]; @@ -469,10 +593,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), @@ -483,7 +608,7 @@ mod tests { let other = attribute_run( CALLER, &run(43, "other.yml"), - &[], + &files, &BTreeMap::new(), None, Some(SHA), @@ -495,7 +620,7 @@ mod tests { attribute_run( CALLER, &run(42, "ci.yml"), - &[], + &files, &BTreeMap::new(), None, Some(SHA), @@ -766,7 +891,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] @@ -812,23 +937,248 @@ 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 source = snapshot(&files); + let resolved: Vec<_> = runs + .iter() + .map(|run| resolve_run_workflow(run, &source).unwrap().path.as_str()) + .collect(); + assert_eq!(resolved, ["gov.yml", "ci.yml", "build.yml", "build.yml"]); + } + + #[test] + 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", + "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@refs/heads/main", + "release@refs.yml", + "release@nightly.yml@refs/heads/topic@refs/heads/main", + ] + ); + 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@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": [{ + "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_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, &snapshot(&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, &snapshot(&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, &snapshot(&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] diff --git a/crates/squabble-forge/src/lib.rs b/crates/squabble-forge/src/lib.rs index 7c3f6a3d..12af879f 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,62 +255,135 @@ 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 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 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 { - revision, - workflow_files: files.len(), - }, - files, - notes, - canonical, - } + files } /// Read the workflow directories of `repos` in batches. Returns one snapshot @@ -457,6 +553,89 @@ 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 67ca03b8..ac141406 100644 --- a/docs/CREUSOT.adoc +++ b/docs/CREUSOT.adoc @@ -9,46 +9,69 @@ 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. 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] + 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. |=== -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. +`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 +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 +252,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 +274,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 +287,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..f103b2a3 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,9 +2,25 @@ // 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`. 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, +the whole operational engine, or separate mirror-test execution. + +== Template obligation summary [cols="2,1,1,1,1,1", options="header"] |=== @@ -20,7 +36,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 +49,7 @@ |=== | ID | Proof | Prover | File | Date | Verified By -| — | No proofs completed yet | — | — | — | — +| — | No template obligations recorded complete | — | — | — | — |=== == Proofs In Progress @@ -98,4 +115,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/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/README.adoc b/verification/squabble-creusot/README.adoc index 4e4da403..da27e2f4 100644 --- a/verification/squabble-creusot/README.adoc +++ b/verification/squabble-creusot/README.adoc @@ -5,7 +5,18 @@ 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`. 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 +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 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 bbb19984..32f812d2 100644 --- a/verification/squabble-creusot/src/lib.rs +++ b/verification/squabble-creusot/src/lib.rs @@ -19,16 +19,20 @@ //! 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), 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. +//! 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 //!