From 08d367560c411c279ed756f544056f6446259c1f Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:38:30 +0000 Subject: [PATCH 1/7] xtask: select every crate on a tier or CI workflow change; narrow parts to a selection A change to a crate's tier or target-tier, or to .github/workflows/ci.yml, now selects every crate (rule 7 wants a full verification for a tier raise). 'crates --changed', 'verify --part base|miri --changed' and 'verify --part assemble --only' let a pull request verify only the selected crates; assemble then ends in CHANGED CRATES PASSED, never ALL CHECKS PASSED. Co-Authored-By: Claude Sonnet 5.5 --- xtask/src/changed.rs | 148 ++++++++++++++++--- xtask/src/main.rs | 329 ++++++++++++++++++++++++++++++++----------- 2 files changed, 381 insertions(+), 96 deletions(-) diff --git a/xtask/src/changed.rs b/xtask/src/changed.rs index 9d2ec832..05456d80 100644 --- a/xtask/src/changed.rs +++ b/xtask/src/changed.rs @@ -6,12 +6,19 @@ //! because its proofs and tests may rest on the changed one. A change to any //! file outside every crate and outside the list in [`is_inert`] selects //! every crate: `Cargo.lock`, the workspace `Cargo.toml`, the toolchain -//! pins, `scripts/` and `xtask/` itself (which decides what passing means) -//! can change any crate's result. +//! pins, `scripts/`, `xtask/` itself (which decides what passing means) and +//! the CI workflow (which decides what CI runs) can change any crate's +//! result. //! -//! This narrows only what a local run checks. CI runs `cargo xtask verify` -//! in full on every push and pull request, and that run is the gate -//! (docs/VERIFICATION.md, "Local and CI runs"). +//! So can a change to a crate's `tier` or `target-tier` (see +//! [`tier_lines_differ`]): CLAUDE.md rule 7 requires a tier raise to pass a +//! full verification on its pull request, so such a change selects every +//! crate, the safest choice. +//! +//! The same selection narrows a pull request's CI run (`cargo xtask crates +//! --changed`, `.github/workflows/ci.yml`). `main` is always verified in +//! full, and that run is the gate (docs/VERIFICATION.md, "Local and CI +//! runs"). use std::collections::BTreeSet; use std::path::Path; @@ -31,21 +38,59 @@ pub enum Selection { Some(BTreeSet), } +/// The CI workflow. It decides what CI runs, so a change to it is a change +/// to everything: it is not inert. +const CI_WORKFLOW: &str = ".github/workflows/ci.yml"; + /// Paths outside every crate whose changes cannot alter any crate's build, /// proofs, tests or measurements. Everything they feed is re-checked by the /// static checks, which `--changed` always runs in full: `docs/` holds the /// dependency allowlist, spec reviews and `clazel-sys` audits, and -/// README.md's status table is compared row by row. +/// README.md's status table is compared row by row. The rest of `.github/` +/// is inert, but not [`CI_WORKFLOW`]. fn is_inert(path: &str) -> bool { path.starts_with("docs/") - || path.starts_with(".github/") + || (path.starts_with(".github/") && path != CI_WORKFLOW) || path.starts_with(".claude/") || matches!(path, "README.md" | "CLAUDE.md" | "LICENSE" | ".gitignore") } +/// The lines of a manifest that mention a tier (`tier = 2`, +/// `target-tier = 2`, a dotted `metadata.clazel.tier = 2`, an inline table), +/// comments dropped and whitespace removed, sorted. Deliberately loose: it +/// can only over-report a change, which selects more, never less. +fn tier_lines(manifest: &str) -> Vec { + let mut lines: Vec = manifest + .lines() + .map(|l| l.split('#').next().unwrap_or("")) + .filter(|l| l.contains("tier")) + .map(|l| l.split_whitespace().collect::()) + .collect(); + lines.sort(); + lines +} + +/// Whether the tier declarations differ between two versions of a crate's +/// `Cargo.toml` (`None`: the file did not exist). +pub fn tier_lines_differ(old: Option<&str>, new: Option<&str>) -> bool { + old.map(tier_lines) != new.map(tier_lines) +} + /// The crates to check for `changed` paths (relative to the repository -/// root, `/`-separated). -pub fn select_paths(crates: &[Crate], root: &Path, changed: &[String]) -> Selection { +/// root, `/`-separated). `tier_changed` are the crate manifests among them +/// whose tier declarations differ ([`tier_lines_differ`]); any selects +/// every crate. +pub fn select_paths( + crates: &[Crate], + root: &Path, + changed: &[String], + tier_changed: &[String], +) -> Selection { + if let Some(path) = tier_changed.first() { + return Selection::All(format!( + "{path} changed its tier or target-tier (a tier change needs a full verification, CLAUDE.md rule 7)" + )); + } let dirs: Vec<(String, String)> = crates .iter() .filter_map(|c| { @@ -84,7 +129,7 @@ pub fn select_paths(crates: &[Crate], root: &Path, changed: &[String]) -> Select /// Paths that differ between the merge base of HEAD and `base` and the /// working tree: committed, staged, unstaged and untracked (not ignored). -fn changed_paths(base: &str) -> Result<(String, Vec), String> { +fn changed_paths(base: &str) -> Result<(String, Vec, Vec), String> { let git = |args: &[&str]| -> Result { let out = Command::new("git") .args(args) @@ -108,20 +153,32 @@ fn changed_paths(base: &str) -> Result<(String, Vec), String> { ] { paths.extend(out.lines().map(str::to_owned)); } - Ok((merge_base, paths.into_iter().collect())) + // Crate manifests whose tier declarations changed (or that are new). + let mut tier_changed = Vec::new(); + for path in paths.iter().filter(|p| p.ends_with("/Cargo.toml")) { + let old = git(&["show", &format!("{merge_base}:{path}")]).ok(); + let new = std::fs::read_to_string(path).ok(); + if tier_lines_differ(old.as_deref(), new.as_deref()) { + tier_changed.push(path.clone()); + } + } + Ok((merge_base, paths.into_iter().collect(), tier_changed)) } /// The selection for this checkout against `base`, and the merge base used. pub fn select(crates: &[Crate], root: &Path, base: &str) -> Result<(String, Selection), String> { - let (merge_base, paths) = changed_paths(base)?; - Ok((merge_base, select_paths(crates, root, &paths))) + let (merge_base, paths, tier_changed) = changed_paths(base)?; + Ok(( + merge_base, + select_paths(crates, root, &paths, &tier_changed), + )) } #[cfg(test)] mod tests { use std::path::PathBuf; - use super::{Selection, select_paths}; + use super::{Selection, select_paths, tier_lines_differ}; use crate::workspace::Crate; fn krate(name: &str, deps: &[&str]) -> Crate { @@ -162,7 +219,13 @@ mod tests { fn sel(paths: &[&str]) -> Selection { let paths: Vec = paths.iter().map(|p| (*p).to_owned()).collect(); - select_paths(&ws(), std::path::Path::new("/r"), &paths) + select_paths(&ws(), std::path::Path::new("/r"), &paths, &[]) + } + + fn sel_tier(paths: &[&str], tier_changed: &[&str]) -> Selection { + let paths: Vec = paths.iter().map(|p| (*p).to_owned()).collect(); + let tier: Vec = tier_changed.iter().map(|p| (*p).to_owned()).collect(); + select_paths(&ws(), std::path::Path::new("/r"), &paths, &tier) } fn some(names: &[&str]) -> Selection { @@ -187,12 +250,65 @@ mod tests { #[test] fn docs_and_readme_select_nothing() { assert_eq!( - sel(&["docs/ROADMAP.md", "README.md", ".github/workflows/ci.yml"]), + sel(&[ + "docs/ROADMAP.md", + "README.md", + ".github/dependabot.yml", + ".github/workflows/other.yml" + ]), some(&[]) ); assert_eq!(sel(&[]), some(&[])); } + #[test] + fn a_change_to_the_ci_workflow_selects_everything() { + for paths in [ + &[".github/workflows/ci.yml"][..], + &["crates/sandbox/src/lib.rs", ".github/workflows/ci.yml"][..], + ] { + assert!(matches!(sel(paths), Selection::All(_)), "{paths:?}"); + } + } + + #[test] + fn a_tier_change_selects_everything() { + // The manifest alone would select only `sandbox`. + assert_eq!(sel(&["crates/sandbox/Cargo.toml"]), some(&["sandbox"])); + assert!(matches!( + sel_tier( + &["crates/sandbox/Cargo.toml"], + &["crates/sandbox/Cargo.toml"] + ), + Selection::All(_) + )); + } + + #[test] + fn tier_declarations_are_compared_line_by_line() { + let base = + "[package]\nname = \"a\"\n[package.metadata.clazel]\ntier = 1 # now\ntarget-tier = 2\n"; + // Other edits, comments and spacing are not tier changes. + let edited = "[package]\nname = \"a\"\nversion = \"0.1.0\"\n[package.metadata.clazel]\ntier=1\ntarget-tier = 2 # goal\n"; + assert!(!tier_lines_differ(Some(base), Some(edited))); + assert!(!tier_lines_differ(None, None)); + // A raise, a lowered target, a dotted key, a new or removed manifest. + assert!(tier_lines_differ( + Some(base), + Some(&base.replace("tier = 1", "tier = 2")) + )); + assert!(tier_lines_differ( + Some(base), + Some(&base.replace("target-tier = 2", "target-tier = 1")) + )); + assert!(tier_lines_differ( + Some(base), + Some(&format!("{base}metadata.clazel.tier = 2\n")) + )); + assert!(tier_lines_differ(None, Some(base))); + assert!(tier_lines_differ(Some(base), None)); + } + #[test] fn shared_inputs_select_everything() { for p in [ diff --git a/xtask/src/main.rs b/xtask/src/main.rs index ff3ed373..89684989 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -6,12 +6,16 @@ //! - `cargo xtask verify --changed [base]`: the same checks, but tests, Miri, //! Kani, Verus, mutations and conformance only for the crates that changed //! since `base` (default `origin/main`) and their dependents (`changed.rs`). -//! Ends in `CHANGED CRATES PASSED`; CI's full run is the gate. -//! - `cargo xtask verify --part (base|crate --metrics |assemble -//! --metrics [--write])`: the same checks split into parts for -//! separate CI jobs (`parts.rs`); `cargo xtask crates` lists the crates for -//! them. `assemble --write` writes README.md's table from the parts, which -//! CI does on main. +//! Ends in `CHANGED CRATES PASSED`; the full run on `main` is the gate. +//! - `cargo xtask verify --part (base|miri [--changed [base]]|crate +//! --metrics |assemble --metrics [--write|--only ])`: the +//! same checks split into parts for separate CI jobs (`parts.rs`); +//! `cargo xtask crates [--names] [--changed [base]]` lists the crates for +//! them, only the changed ones with `--changed`, which CI uses on pull +//! requests. `assemble --write` writes README.md's table from the parts, +//! which CI does on main. `assemble --only` requires just those crates' +//! parts, for a pull request's partial run, and ends in `CHANGED CRATES +//! PASSED`. //! - `cargo xtask check`: only the fast static checks (no build, no proofs). //! - `cargo xtask mutate`: only the proof mutation tests (also part of //! `verify`). @@ -47,6 +51,7 @@ mod unicode; mod verus; mod workspace; +use std::collections::BTreeSet; use std::path::{Path, PathBuf}; use std::process::{Command, ExitCode}; @@ -919,30 +924,59 @@ fn generate_tables() -> ExitCode { } } +/// The crates a `--changed` run repeats proofs and tests for, against +/// `base`, recorded as a step; `None` means every crate (or a failure, +/// which the step records). Also returns the merge base used. +fn changed_selection( + r: &mut Runner, + crates: &[Crate], + root: &Path, + base: &str, +) -> Option<(String, Vec)> { + match changed::select(crates, root, base) { + Ok((merge_base, changed::Selection::All(why))) => { + r.step( + "select changed crates", + Outcome::Pass(vec![format!( + "every crate is checked: {why} since {base} ({merge_base})" + )]), + ); + None + } + Ok((merge_base, changed::Selection::Some(names))) => { + let picked: Vec = crates + .iter() + .filter(|c| names.contains(&c.name)) + .cloned() + .collect(); + r.step( + "select changed crates", + Outcome::Pass(vec![format!( + "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", + picked.len(), + crates.len(), + if names.is_empty() { + "none".to_owned() + } else { + names.iter().cloned().collect::>().join(", ") + } + )]), + ); + Some((merge_base, picked)) + } + Err(e) => { + r.step("select changed crates", Outcome::Fail(vec![e])); + None + } + } +} + fn main() -> ExitCode { let args: Vec = std::env::args().skip(1).collect(); let args: Vec<&str> = args.iter().map(String::as_str).collect(); - // `verify --part ...` (parts.rs) and `crates` are handled apart. - let part = match args.as_slice() { - ["verify", "--part", "base"] => Some(Part::Base), - ["verify", "--part", "miri"] => Some(Part::Miri), - ["verify", "--part", "crate", names, "--metrics", dir] => Some(Part::Crate( - names.split(',').map(str::to_owned).collect(), - PathBuf::from(dir), - )), - ["verify", "--part", "assemble", "--metrics", dir] => { - Some(Part::Assemble(PathBuf::from(dir), false)) - } - ["verify", "--part", "assemble", "--metrics", dir, "--write"] => { - Some(Part::Assemble(PathBuf::from(dir), true)) - } - ["crates"] => Some(Part::ListCrates), - _ => None, - }; - let args = if part.is_some() { vec!["check"] } else { args }; - // `mutate ` runs one crate's mutations, for iterating on them. - let mut only_crate: Option<&str> = None; - // `verify` and `report` take `--changed []` (changed.rs). + // `verify` and `report` take `--changed []` (changed.rs), and so do + // the `base` and `miri` parts and `crates`, which CI runs that way on + // pull requests. let (args, base) = match args.iter().position(|a| *a == "--changed") { Some(i) => { let (head, tail) = args.split_at(i); @@ -954,6 +988,56 @@ fn main() -> ExitCode { } None => (args.as_slice(), None), }; + let base_owned = base.map(str::to_owned); + // `verify --part ...` (parts.rs) and `crates` are handled apart. + let part = match (args, base) { + (["verify", "--part", "base"], _) => Some(Part::Base(base_owned)), + (["verify", "--part", "miri"], _) => Some(Part::Miri(base_owned)), + (["verify", "--part", "crate", names, "--metrics", dir], None) => Some(Part::Crate( + names.split(',').map(str::to_owned).collect(), + PathBuf::from(dir), + )), + (["verify", "--part", "assemble", "--metrics", dir], None) => { + Some(Part::Assemble(PathBuf::from(dir), false, None)) + } + (["verify", "--part", "assemble", "--metrics", dir, "--write"], None) => { + Some(Part::Assemble(PathBuf::from(dir), true, None)) + } + // A pull request's partial run: only these crates' measurements. + // Never together with `--write`: the table comes from full runs. + ( + [ + "verify", + "--part", + "assemble", + "--metrics", + dir, + "--only", + names, + ], + None, + ) => Some(Part::Assemble( + PathBuf::from(dir), + false, + Some( + names + .split(',') + .filter(|n| !n.is_empty()) + .map(str::to_owned) + .collect(), + ), + )), + (["crates"], _) => Some(Part::ListCrates(false, base_owned)), + (["crates", "--names"], _) => Some(Part::ListCrates(true, base_owned)), + _ => None, + }; + let (args, base) = if part.is_some() { + (&["check"][..], None) + } else { + (args, base) + }; + // `mutate ` runs one crate's mutations, for iterating on them. + let mut only_crate: Option<&str> = None; let (full, only_mutate, report_mode, write) = match (args, base) { (["testdata"], None) => return generate_testdata(), (["tables"], None) => return generate_tables(), @@ -968,7 +1052,7 @@ fn main() -> ExitCode { (["report", "--write"], _) => (false, false, true, true), _ => { eprintln!( - "usage: cargo xtask --metrics |assemble --metrics [--write])|crates|check|mutate [crate]|testdata|tables|report [--write] [--changed [base]]>" + "usage: cargo xtask --metrics |assemble --metrics [--write|--only ])|crates [--names] [--changed [base]]|check|mutate [crate]|testdata|tables|report [--write] [--changed [base]]>" ); return ExitCode::from(64); } @@ -1013,36 +1097,7 @@ fn main() -> ExitCode { // `None` means every crate. let mut partial: Option<(String, Vec)> = None; if let Some(base) = base { - match changed::select(&crates, &root, base) { - Ok((merge_base, changed::Selection::All(why))) => r.step( - "select changed crates", - Outcome::Pass(vec![format!( - "every crate is checked: {why} since {base} ({merge_base})" - )]), - ), - Ok((merge_base, changed::Selection::Some(names))) => { - let picked: Vec = crates - .iter() - .filter(|c| names.contains(&c.name)) - .cloned() - .collect(); - r.step( - "select changed crates", - Outcome::Pass(vec![format!( - "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", - picked.len(), - crates.len(), - if names.is_empty() { - "none".to_owned() - } else { - names.iter().cloned().collect::>().join(", ") - } - )]), - ); - partial = Some((merge_base, picked)); - } - Err(e) => r.step("select changed crates", Outcome::Fail(vec![e])), - } + partial = changed_selection(&mut r, &crates, &root, base); } let checked: &[Crate] = partial.as_ref().map_or(&crates, |(_, p)| p.as_slice()); let only = partial.as_ref().map(|(_, p)| p.as_slice()); @@ -1090,23 +1145,38 @@ fn main() -> ExitCode { /// One part of a split verification (parts.rs). enum Part { - Base, - Miri, + /// With a base ref (`--changed`), tests only for the changed crates. + Base(Option), + /// With a base ref (`--changed`), Miri only for the changed crates. + Miri(Option), /// One or more crates (comma-separated on the command line; CI groups /// the crates with no proofs into one job, see [`crate_groups`]). Crate(Vec, PathBuf), - /// The crate parts' directory, and whether to write README.md's table - /// from them (CI does, on main, after every part passed). - Assemble(PathBuf, bool), + /// The crate parts' directory, whether to write README.md's table + /// from them (CI does, on main, after every part passed), and, for a + /// pull request's partial run, the only crates whose measurements are + /// required (never together with writing). + Assemble(PathBuf, bool, Option>), /// `cargo xtask crates`: the crate groups as a JSON array of - /// comma-separated names, for CI's matrix of `crate` parts. - ListCrates, + /// comma-separated names, for CI's matrix of `crate` parts; with a base + /// ref (`--changed`), only the groups of the changed crates. With + /// `--names` (the flag), the crates themselves, comma-separated. + ListCrates(bool, Option), } /// CI's crate parts: one per crate with proof work (Verus, Kani harnesses or /// mutations), and one for all the others together, which finish in about /// a minute each and would otherwise each hold a runner for its setup. -fn crate_groups(crates: &[Crate]) -> Vec { +/// +/// Only the crates in `selected` are grouped (a pull request's job list); +/// a group left empty is dropped. +fn crate_groups(crates: &[Crate], selected: &BTreeSet<&str>) -> Vec { + let crates: Vec = crates + .iter() + .filter(|c| selected.contains(c.name.as_str())) + .cloned() + .collect(); + let crates = crates.as_slice(); let light = |c: &Crate| { !c.verus && !mutate::has_mutations(c) @@ -1129,19 +1199,85 @@ fn crate_groups(crates: &[Crate]) -> Vec { } fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Path) -> ExitCode { - if let Part::ListCrates = part { - println!("{}", serde_json::Value::from(crate_groups(crates))); + if let Part::ListCrates(names, base) = part { + // The selection goes to stderr (the CI log); stdout is the list. + let selected: BTreeSet<&str> = match base { + None => crates.iter().map(|c| c.name.as_str()).collect(), + Some(base) => match changed::select(crates, root, &base) { + Ok((merge_base, changed::Selection::All(why))) => { + eprintln!("every crate: {why} since {base} ({merge_base})"); + crates.iter().map(|c| c.name.as_str()).collect() + } + Ok((merge_base, changed::Selection::Some(sel))) => { + eprintln!( + "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", + sel.len(), + crates.len(), + sel.iter().cloned().collect::>().join(", ") + ); + crates + .iter() + .map(|c| c.name.as_str()) + .filter(|n| sel.contains(*n)) + .collect() + } + Err(e) => { + eprintln!("select changed crates: {e}"); + return ExitCode::from(1); + } + }, + }; + if names { + println!( + "{}", + crates + .iter() + .map(|c| c.name.as_str()) + .filter(|n| selected.contains(n)) + .collect::>() + .join(",") + ); + } else { + println!( + "{}", + serde_json::Value::from(crate_groups(crates, &selected)) + ); + } return ExitCode::SUCCESS; } static_checks(r, crates, pins); let done = match part { - Part::Base => { - build_checks(r, None); - "BASE PART PASSED (static checks, rustfmt, clippy and tests; Miri runs in the miri part, proofs in the crate parts)".to_owned() + Part::Base(base) => { + // Rustfmt and clippy always cover the whole workspace; only the + // tests narrow to the changed crates and their dependents. + let picked = base + .as_deref() + .and_then(|b| changed_selection(r, crates, root, b)); + let only = picked.as_ref().map(|(_, p)| p.as_slice()); + build_checks(r, only); + match &picked { + Some((_, p)) => format!( + "BASE PART PASSED (static checks, rustfmt and clippy over the workspace; tests of {} of {} crates, the changed ones and their dependents)", + p.len(), + crates.len() + ), + None => "BASE PART PASSED (static checks, rustfmt, clippy and tests; Miri runs in the miri part, proofs in the crate parts)".to_owned(), + } } - Part::Miri => { - miri(r, pins, None); - "MIRI PART PASSED (static checks and the tests under Miri)".to_owned() + Part::Miri(base) => { + let picked = base + .as_deref() + .and_then(|b| changed_selection(r, crates, root, b)); + let only = picked.as_ref().map(|(_, p)| p.as_slice()); + miri(r, pins, only); + match &picked { + Some((_, p)) => format!( + "MIRI PART PASSED (static checks and the tests of {} of {} crates under Miri, the changed ones and their dependents)", + p.len(), + crates.len() + ), + None => "MIRI PART PASSED (static checks and the tests under Miri)".to_owned(), + } } Part::Crate(names, dir) => { let mut selected: Vec = Vec::new(); @@ -1179,10 +1315,33 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa names.join(", ") ) } - Part::Assemble(dir, write) => { + Part::Assemble(dir, write, only) => { + // With `only` (a pull request's partial run) just those crates + // are required; every other crate is not claimed at all. + let mut required: Vec = Vec::new(); + match &only { + None => required = crates.to_vec(), + Some(names) => { + for name in names { + match crates.iter().find(|c| &c.name == name) { + Some(c) => required.push(c.clone()), + None => { + r.step( + "select crate", + Outcome::Fail(vec![format!( + "no workspace crate named {name:?}" + )]), + ); + println!("RESULT: FAILED"); + return ExitCode::from(1); + } + } + } + } + } let res = parts::head().and_then(|commit| { let mut problems = Vec::new(); - for c in crates { + for c in &required { let path = dir.join(format!("{}.json", c.name)); let entry = r.metrics.entry(c.name.clone()).or_default(); let read = std::fs::read_to_string(&path) @@ -1194,7 +1353,8 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa } if problems.is_empty() { Ok(vec![format!( - "{} crate parts, all from {commit}", + "{} of {} crate parts, all from {commit}", + required.len(), crates.len() )]) } else { @@ -1203,11 +1363,20 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa }); r.step("read crate parts", from_result(res)); if !r.failed { - readme_table(r, write, None); + readme_table(r, write, only.as_ref().map(|_| required.as_slice())); + } + match &only { + None => "PARTS ASSEMBLED (every crate part present and from this commit; the gate is this and every part passing on the same commit)".to_owned(), + // Never "ALL CHECKS PASSED" or "PARTS ASSEMBLED": most + // crates' proofs did not run. + Some(_) => format!( + "CHANGED CRATES PASSED ({} of {} crates' parts present and from this commit; the other crates' proofs did not run here, and the full verification runs on main after merge)", + required.len(), + crates.len() + ), } - "PARTS ASSEMBLED (every crate part present and from this commit; the gate is this and every part passing on the same commit)".to_owned() } - Part::ListCrates => String::new(), + Part::ListCrates(..) => String::new(), }; if r.failed { println!("RESULT: FAILED"); From 7377846a88f04c1fa2c07ce0e7a1b0d6fce4477a Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:38:30 +0000 Subject: [PATCH 2/7] ci: verify only the changed crates and their dependents on pull requests Pushes to main and manual runs still verify every crate. The job named Full verification keeps its name and reports a partial run as such. Co-Authored-By: Claude Sonnet 5.5 --- .github/workflows/ci.yml | 138 ++++++++++++++++++++++++++++++++------- CLAUDE.md | 14 ++-- README.md | 3 +- docs/VERIFICATION.md | 58 +++++++++++----- 4 files changed, 169 insertions(+), 44 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3fb4a90e..2bdee4c5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,16 +1,24 @@ -# Runs the checks in docs/VERIFICATION.md on every push to main and every -# pull request. The full verification is split into parts (xtask/src/parts.rs) -# so that no job comes near GitHub's six-hour limit: +# Runs the checks in docs/VERIFICATION.md. Every push to main (and every +# manual run) is verified in full. A pull request is verified in part: the +# crates it changes and the crates that depend on them (below). The +# verification is split into parts (xtask/src/parts.rs) so that no job comes +# near GitHub's six-hour limit: # # crates `cargo xtask check`, the fast static checks (unsafe, lint # overrides, escape hatches, tier declarations, pins, allowlist), # which fail in a minute or two so obvious mistakes show up early; # then the crate groups (`cargo xtask crates`) for the matrix -# below, so a new crate cannot be left out. +# below, so a new crate cannot be left out. On a pull request the +# groups are only those of the selected crates +# (`cargo xtask crates --changed origin/main`, below). # base `verify --part base`: static checks, rustfmt, clippy and tests -# over the whole workspace. -# miri `verify --part miri`: the workspace's tests under Miri. -# base-macos the base and Miri parts on macOS arm64, one after the other: +# over the whole workspace. On a pull request the tests narrow to +# the selected crates (`--changed origin/main`); the static +# checks, rustfmt and clippy still cover the whole workspace. +# miri `verify --part miri`: the workspace's tests under Miri. On a +# pull request, the selected crates' tests only. +# base-macos the base and Miri parts on macOS arm64, one after the other +# (narrowed the same way on a pull request): # the Seatbelt sandbox, the demo, the host and escape tests, and # the macOS-only code under clippy and Miri. Proofs and harnesses # are not repeated there: Verus and Kani give the same answer for @@ -20,10 +28,17 @@ # conformance. One job per crate with proof work; the crates # with none share one job. Each uploads what it measured, one # file per crate, tagged with the commit. -# assemble `verify --part assemble`: needs every job above to pass, then -# checks that every crate's measurements are present and from -# this commit, and reports whether README.md's table matches them. -# table on pushes to main only, after `assemble` passed: writes +# assemble `verify --part assemble`, the job named `Full verification`: +# needs every job above to pass, then checks that every crate's +# measurements are present and from this commit, and reports +# whether README.md's table matches them. On a pull request it +# checks only the selected crates (`--only`), says so, and ends +# in `CHANGED CRATES PASSED`, never `ALL CHECKS PASSED`: it +# verified n of m crates, not all. The job keeps its name because +# CLAUDE.md and the branch protection refer to it; only its +# result line tells a partial run from a full one. +# table on pushes to main only (which are always full runs), after +# `assemble` passed: writes # README.md's table from the same measurements # (`verify --part assemble --write`) and, if it changed, commits # it to main as github-actions[bot]. Changes therefore never need @@ -38,11 +53,27 @@ # binaries are only as verified as the commit's Full # verification says. # -# Together the parts run exactly the checks of one `scripts/verify.sh`, which -# still runs them all on one machine. Verification has passed only when every -# job above is green; `assemble` cannot be, unless the others were. Every -# part exits non-zero when a tool is missing and checks were skipped, so a -# skipped check is never green. +# Which crates a pull request verifies is chosen by `xtask/src/changed.rs`, +# the same selection as `cargo xtask verify --changed`: the crates with a +# changed file, and every crate that depends on one of them, against the +# merge base of the pull request and `origin/main`. Stacked pull requests have +# other bases than main; selecting against main also includes the lower pull +# requests' crates, which is conservative and fine. A change to anything +# shared (Cargo.lock, the workspace manifest, the toolchain pins, scripts/, +# xtask/) or to this workflow selects every crate. So does any change to a +# crate's `tier` or `target-tier`: CLAUDE.md rule 7 requires a tier raise to +# pass a full verification on its pull request, and the safest way to keep +# that true is to run one for every tier change. Pushes to main and manual +# runs always select every crate, so main is verified in full after every +# merge. +# +# With every crate selected, the parts together run exactly the checks of one +# `scripts/verify.sh`, which still runs them all on one machine. Full +# verification has passed only when every job above is green on a run that +# selected every crate (a push to main, a manual run, or a pull request that +# touched something shared); `assemble` cannot be green unless the others +# were. Every part exits non-zero when a tool is missing and checks were +# skipped, so a skipped check is never green. # # The crate parts run on Linux x86-64 only: it is the platform the # Dockerfile reproduces, and Verus publishes no Linux arm64 build. macOS @@ -52,6 +83,10 @@ # setup.sh's download cache is cached: setup.sh re-checks every cached file # against scripts/checksums.txt before using it, so a stale or tampered cache # entry cannot reach the proof tools. Build output is never cached. +# +# The `crates` and `base*`/`miri` jobs check out the full history on a pull +# request (`fetch-depth: 0`): the default depth of 1 has no merge base with +# main to select against. name: CI @@ -77,19 +112,37 @@ jobs: runs-on: ubuntu-24.04 timeout-minutes: 15 outputs: + # The matrix of crate groups, and the crates in it, comma-separated + # (for `assemble`). Both are everything unless this is a pull request. list: ${{ steps.list.outputs.list }} + names: ${{ steps.list.outputs.names }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false + fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} # rustup reads rust-toolchain.toml and installs the pinned toolchain. - name: Install Rust run: rustup toolchain install - name: cargo xtask check run: cargo xtask check + # Pull requests: only the crates they change and their dependents (see + # the header). The selection is printed to the log. Assigned apart from + # the echo so that a failing xtask fails the step. - id: list name: cargo xtask crates - run: echo "list=$(cargo xtask crates)" >> "$GITHUB_OUTPUT" + env: + EVENT: ${{ github.event_name }} + run: | + if [ "$EVENT" = pull_request ]; then + list=$(cargo xtask crates --changed origin/main) + names=$(cargo xtask crates --names --changed origin/main) + else + list=$(cargo xtask crates) + names=$(cargo xtask crates --names) + fi + echo "list=$list" >> "$GITHUB_OUTPUT" + echo "names=$names" >> "$GITHUB_OUTPUT" base: name: Verify (base) @@ -99,6 +152,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false + fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -113,7 +167,7 @@ jobs: - name: Allow the sandbox's user namespace run: sudo packaging/apparmor/allow-userns.sh clazel-test "$GITHUB_WORKSPACE/target/{debug,release}/{clazel-renderer,clazel-adversary,deps/sandbox-*}" - name: Verify (base) - run: cargo xtask verify --part base + run: cargo xtask verify --part base ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} base-macos: name: Verify (base, macOS) @@ -123,6 +177,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false + fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -133,11 +188,11 @@ jobs: # No AppArmor step: the renderer's macOS sandbox is Seatbelt, which an # unprivileged process enters without any setup. - name: Verify (base) - run: cargo xtask verify --part base + run: cargo xtask verify --part base ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} # Miri runs here after the base part rather than in a job of its own: # macOS runners are few (5 at once), and this job is not the slowest. - name: Verify (Miri) - run: cargo xtask verify --part miri + run: cargo xtask verify --part miri ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} miri: name: Verify (Miri) @@ -147,6 +202,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false + fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -157,12 +213,15 @@ jobs: # No AppArmor step: tests that spawn the sandboxed renderer are # ignored under Miri. - name: Verify (Miri) - run: cargo xtask verify --part miri + run: cargo xtask verify --part miri ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} crate: # A group of crates with no proofs is one job (`cargo xtask crates`). name: Verify ${{ contains(matrix.crate, ',') && 'crates without proofs' || matrix.crate }} needs: crates + # A pull request that selects no crate has an empty matrix, which GitHub + # rejects; the job is skipped, and `assemble` accepts that only then. + if: needs.crates.outputs.list != '[]' runs-on: ubuntu-24.04 timeout-minutes: 360 strategy: @@ -199,24 +258,59 @@ jobs: retention-days: 7 assemble: + # Named `Full verification` for CLAUDE.md and the branch protection. On a + # pull request it verifies only the selected crates and ends in + # `CHANGED CRATES PASSED`; see the header. name: Full verification needs: [crates, base, base-macos, miri, crate] + # Runs even when a job it needs failed or was skipped, and fails then: + # a skipped job is not a pass, and a skipped required check would count + # as one. Only a cancelled run is not judged. + if: ${{ !cancelled() }} runs-on: ubuntu-24.04 timeout-minutes: 30 steps: + - name: Every job passed + env: + NEEDS: ${{ toJSON(needs) }} + LIST: ${{ needs.crates.outputs.list }} + run: | + # `crate` may be skipped only when no crate was selected. + bad=$(echo "$NEEDS" | jq -r --arg list "$LIST" ' + to_entries[] + | select(.value.result != "success") + | select(.key != "crate" or $list != "[]" or .value.result != "skipped") + | "\(.key): \(.value.result)"') + if [ -n "$bad" ]; then + echo "Not every job passed:" + echo "$bad" + exit 1 + fi - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - name: Install Rust run: rustup toolchain install - name: Download measurements + # Nothing was measured when no crate was selected. + if: needs.crates.outputs.list != '[]' uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: pattern: part-* path: parts merge-multiple: true + # Pull requests require the selected crates' measurements only. Pushes + # to main and manual runs require every crate's. - name: Assemble - run: cargo xtask verify --part assemble --metrics parts + env: + EVENT: ${{ github.event_name }} + NAMES: ${{ needs.crates.outputs.names }} + run: | + if [ "$EVENT" = pull_request ]; then + cargo xtask verify --part assemble --metrics parts --only "$NAMES" + else + cargo xtask verify --part assemble --metrics parts + fi table: name: Update README table diff --git a/CLAUDE.md b/CLAUDE.md index 5aecfc27..2f3a3296 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -53,7 +53,8 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. crate's `Cargo.toml` requires all of the following, and `cargo xtask check` rejects the claim otherwise: - every proof and harness passing in a full `cargo xtask verify`, which - for a tier change means CI's green run on the pull request (a local + for a tier change means CI's green run on the pull request, which + verifies every crate whenever a `tier` or `target-tier` changes (a local `--changed` run does not count); - Tier 1: Kani harnesses; - Tier 2: Verus enabled; every mutation in `mutations.json` a `killed` with @@ -85,9 +86,14 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. them; a change to anything shared (`Cargo.lock`, the workspace manifest, toolchain pins, `scripts/`, `xtask/`) makes it check every crate. It ends in `CHANGED CRATES PASSED`, which is not `ALL CHECKS PASSED` and must not - be reported as such. Work is **done** only when CI's full verification - (every job of `.github/workflows/ci.yml`, ending in `Full verification`) - is green on its pull request; say so if it has not run yet. To repeat CI's run locally, use `scripts/verify.sh` or the + be reported as such. Work is **done** only when CI (every job of + `.github/workflows/ci.yml`, ending in `Full verification`) is green on its + pull request, and the full run on `main` after the merge is green. A pull + request's CI verifies only the crates it changes and their dependents, and + its `Full verification` then ends in `CHANGED CRATES PASSED`, which is not + `ALL CHECKS PASSED`; a change to anything shared, to `ci.yml` or to a + crate's tier verifies every crate, and `main` is always verified in full. + Say so if CI has not run yet. To repeat CI's run locally, use `scripts/verify.sh` or the Docker command in README.md. `cargo xtask check` runs only the fast static checks (unsafe, the `clazel-sys` audit, lint overrides, escape hatches, tier declarations, pins); use it while iterating, never as the final diff --git a/README.md b/README.md index 135d876d..8934ea0b 100644 --- a/README.md +++ b/README.md @@ -159,7 +159,8 @@ and much of it is work only a person can do. `phase3/tls` branch until it passes CI. Contributions go through the same machine checks as everything else, whoever (or whatever) wrote them: read [CLAUDE.md](CLAUDE.md) first, and expect `cargo xtask verify --changed` and - CI's full verification to be the bar. + CI to be the bar (a pull request's changed crates and their dependents; `main` + in full). ## License diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 83c12415..8f7a36e4 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -83,40 +83,59 @@ installs nothing if a checksum differs. The full `cargo xtask verify` takes hours, so it runs where it is the gate: in CI (`.github/workflows/ci.yml`), on Linux x86-64 with the pinned -toolchain, on every push to `main` and every pull request. Nothing is done, -and no tier is raised, until that run is green. +toolchain. Every push to `main` is verified in full. A pull request is +verified in part: the crates it changes and every crate that depends on one +(the selection of `--changed`, below, against the merge base with `origin/main`; +for a stacked pull request that also includes the lower pull requests' +crates, which is conservative). A change to anything shared, to +`.github/workflows/ci.yml`, or to any crate's `tier` or `target-tier` +selects every crate, so a pull request that raises a tier gets a full +verification. Nothing is done, and no tier is raised, until that run is +green, and `main`'s full run after the merge is green too. CI splits the run into parts, one job each, so no job comes near GitHub's six-hour limit (`xtask/src/parts.rs`): - `verify --part base`: static checks, rustfmt, clippy and tests over the - whole workspace. + whole workspace. On a pull request, `--changed origin/main` narrows the + tests to the selected crates; the static checks, rustfmt and clippy still + cover the whole workspace. - `verify --part miri`: static checks, then the workspace's tests under - Miri. On macOS it runs in the same job as `base`, after it. + Miri (on a pull request, the selected crates' only). On macOS it runs in + the same job as `base`, after it. - `verify --part crate --metrics `, where `` is one crate or several separated by commas: static checks, then Kani, Verus, line counts, mutations and conformance for those crates. CI runs one job per crate with proof work (Verus, Kani harnesses or mutations) and one job for all the others together; the groups come from `cargo xtask - crates`. Mutants run several at a time, each in its own sandbox + crates` (on a pull request `cargo xtask crates --changed origin/main`, the + groups of the selected crates only). Mutants run several at a time, each in its own sandbox (`CLAZEL_MUTANT_JOBS`, default one per core up to 4). On success it writes what it measured to `/.json` for each crate, tagged with the commit (with `+dirty` if tracked files have uncommitted changes). -- `verify --part assemble --metrics `, which runs only after every - other job passed: static checks, then it requires a file for every - workspace crate from this commit, and reports whether README.md's table - matches them. +- `verify --part assemble --metrics `, the `Full verification` job, + which fails unless every other job passed: static checks, then it + requires a file for every workspace crate from this commit, and reports + whether README.md's table matches them. On a pull request it gets + `--only ` and requires the selected crates' files only; it then + ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL + CHECKS PASSED`, as `verify --changed` does. The job keeps the name `Full + verification` in both cases; the result line says which it was. - On pushes to `main` only, the `table` job runs the same part with `--write` after `assemble` passed, and commits README.md's regenerated table to `main` as github-actions[bot] if it changed. So the committed table always comes from CI's own measurements of a fully verified commit, - and no change has to carry it. + and no change has to carry it. A push to `main` always selects every + crate, and `--write` cannot be combined with `--only`. The parts together run exactly the checks of one `cargo xtask verify`, which `scripts/verify.sh` and the Docker command in README.md still run on one machine. "CI is green" means every job passed on the same commit, the -`Full verification` (assemble) job included. +`Full verification` (assemble) job included. On a pull request that is a +verification of the selected crates; only a run that selected every crate +(`main`, a manual run, a change to something shared or to a tier) is a full +one. Locally, `cargo xtask verify --changed [base]` runs the same checks over less. `base` defaults to `origin/main`, the last commit CI verified, and @@ -128,10 +147,15 @@ untracked files) with HEAD's merge base with it (`xtask/src/changed.rs`): - Tests, Miri, Kani, Verus, mutations and conformance run only for the crates with a changed file and every crate that depends on one of them, directly or not, dev-dependencies included. -- A change anywhere else, except `docs/`, `.github/`, `.claude/`, README.md, - CLAUDE.md, LICENSE and `.gitignore`, checks every crate. That covers - `Cargo.lock`, the workspace `Cargo.toml`, `rust-toolchain.toml`, - `scripts/` and `xtask/`, which decides what passing means. +- A change anywhere else, except `docs/`, `.github/` (but not + `.github/workflows/ci.yml`), `.claude/`, README.md, CLAUDE.md, LICENSE and + `.gitignore`, checks every crate. That covers `Cargo.lock`, the workspace + `Cargo.toml`, `rust-toolchain.toml`, `scripts/`, `xtask/`, which decides + what passing means, and the CI workflow, which decides what CI runs. +- So does any change to a line of a crate's `Cargo.toml` that mentions a + tier (`tier`, `target-tier`), or a new or removed crate manifest: rule 7 + requires a tier raise to pass a full verification, so the safest choice + is a full one for every tier change. - The run ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL CHECKS PASSED`. @@ -149,8 +173,8 @@ What this relies on: that a crate's proofs and tests depend only on its own files, the workspace crates it depends on, and the shared files listed above. Verus, Kani and the tests read nothing else, but a crate that read a file outside its directory (say, another crate's vendored data through -`include_str!`) would not be re-checked when that file changed. CI's full -run catches it; the local run may not. +`include_str!`) would not be re-checked when that file changed. The full +run on `main` catches it; a local run or a pull request's CI may not. ## Trusted computing base (what we do *not* prove) From e066ff6b1de9897defab15955ff40bb4ee2276f1 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:40:14 +0000 Subject: [PATCH 3/7] xtask: a partial assemble keeps the host shell size check, skips the table comparison README.md's table can lack rows for crates a pull request did not measure (and lags main until the table job commits), so comparing it there would fail spuriously. Main's full run compares and writes it. Co-Authored-By: Claude Sonnet 5.5 --- .github/workflows/ci.yml | 4 +++- docs/VERIFICATION.md | 5 +++-- xtask/src/main.rs | 34 ++++++++++++++++++++++++++-------- 3 files changed, 32 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2bdee4c5..7c6bbacd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -32,7 +32,9 @@ # needs every job above to pass, then checks that every crate's # measurements are present and from this commit, and reports # whether README.md's table matches them. On a pull request it -# checks only the selected crates (`--only`), says so, and ends +# checks only the selected crates (`--only`) and not README.md's +# table (too few rows were measured; main's full run compares +# and writes it), says so, and ends # in `CHANGED CRATES PASSED`, never `ALL CHECKS PASSED`: it # verified n of m crates, not all. The job keeps its name because # CLAUDE.md and the branch protection refer to it; only its diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 8f7a36e4..1c16955f 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -118,8 +118,9 @@ six-hour limit (`xtask/src/parts.rs`): which fails unless every other job passed: static checks, then it requires a file for every workspace crate from this commit, and reports whether README.md's table matches them. On a pull request it gets - `--only ` and requires the selected crates' files only; it then - ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL + `--only ` and requires the selected crates' files only, and does + not compare README.md's table (it has too few rows measured; the full run + on `main` compares and writes it); it then ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL CHECKS PASSED`, as `verify --changed` does. The job keeps the name `Full verification` in both cases; the result line says which it was. - On pushes to `main` only, the `table` job runs the same part with diff --git a/xtask/src/main.rs b/xtask/src/main.rs index 89684989..7f98fe6e 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -754,12 +754,9 @@ fn conformance_suites(r: &mut Runner, crates: &[Crate]) { } } -/// Compare (or, with `write`, update) README.md's status table against what -/// this run measured. With `only` (a `--changed` run), the other crates' -/// proof and test columns are carried over from README.md's current table, -/// since their inputs did not change; CI's full run re-measures them all. -fn readme_table(r: &mut Runner, write: bool, only: Option<&[Crate]>) { - const NAME: &str = "README status table"; +/// The host shell's size against its limit, as a step; its line count when +/// it could be counted (`None` if the directory does not exist). +fn host_shell_size(r: &mut Runner) -> Option> { let host_shell_count = report::host_shell_lines(std::path::Path::new(report::HOST_SHELL_DIR)); if let Some(counted) = host_shell_count.as_ref() { match counted { @@ -777,6 +774,16 @@ fn readme_table(r: &mut Runner, write: bool, only: Option<&[Crate]>) { Err(e) => r.step("host shell size", Outcome::Fail(vec![e.clone()])), } } + host_shell_count +} + +/// Compare (or, with `write`, update) README.md's status table against what +/// this run measured. With `only` (a `--changed` run), the other crates' +/// proof and test columns are carried over from README.md's current table, +/// since their inputs did not change; CI's full run re-measures them all. +fn readme_table(r: &mut Runner, write: bool, only: Option<&[Crate]>) { + const NAME: &str = "README status table"; + let host_shell_count = host_shell_size(r); let carried = match only { None => report::Rows::new(), Some(cs) => { @@ -1362,8 +1369,19 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa } }); r.step("read crate parts", from_result(res)); - if !r.failed { - readme_table(r, write, only.as_ref().map(|_| required.as_slice())); + if only.is_some() { + // A partial run has measured too few rows to compare the + // table, whose rows the full run on main checks and writes. + // The host shell's size limit does not depend on them. + host_shell_size(r); + r.step( + "README status table", + Outcome::Pass(vec![ + "compared only in a full run (main), which measures every row".into(), + ]), + ); + } else if !r.failed { + readme_table(r, write, None); } match &only { None => "PARTS ASSEMBLED (every crate part present and from this commit; the gate is this and every part passing on the same commit)".to_owned(), From f1d7fb5af314db86e81ed8515d8619bae6b401d4 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Wed, 28 Oct 2026 16:22:06 +0000 Subject: [PATCH 4/7] ci: quote the pull request fetch depth so it is 0, not 1 `github.event_name == 'pull_request' && 0 || 1` is always 1: the number 0 is falsy in an expression. Every pull request job got a shallow clone with no origin/main, so `cargo xtask crates --changed origin/main` and the base and Miri parts' `--changed` failed in `git merge-base`. The string '0' is truthy. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7c6bbacd..fdf782a3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -88,7 +88,9 @@ # # The `crates` and `base*`/`miri` jobs check out the full history on a pull # request (`fetch-depth: 0`): the default depth of 1 has no merge base with -# main to select against. +# main to select against. The depths are quoted strings: in an expression the +# number 0 is falsy, so `cond && 0 || 1` is always 1, while the string '0' is +# truthy. name: CI @@ -122,7 +124,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} + fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} # rustup reads rust-toolchain.toml and installs the pinned toolchain. - name: Install Rust run: rustup toolchain install @@ -154,7 +156,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} + fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -179,7 +181,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} + fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -204,7 +206,7 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && 0 || 1 }} + fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: From 6e6e1720654127e5d19c5660d121af73bc1af377 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Wed, 28 Oct 2026 16:47:12 +0000 Subject: [PATCH 5/7] Revert the partial pull request verification in xtask, CI and docs Spamming pull requests that touch xtask/ would still start a full run each. The next commits replace it with pull request checks that run no proofs, and a full verification on main and on manual runs only. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 142 +++------------- CLAUDE.md | 14 +- README.md | 25 ++- docs/VERIFICATION.md | 59 ++----- xtask/src/changed.rs | 148 ++-------------- xtask/src/main.rs | 359 ++++++++++----------------------------- 6 files changed, 156 insertions(+), 591 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fdf782a3..3fb4a90e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,24 +1,16 @@ -# Runs the checks in docs/VERIFICATION.md. Every push to main (and every -# manual run) is verified in full. A pull request is verified in part: the -# crates it changes and the crates that depend on them (below). The -# verification is split into parts (xtask/src/parts.rs) so that no job comes -# near GitHub's six-hour limit: +# Runs the checks in docs/VERIFICATION.md on every push to main and every +# pull request. The full verification is split into parts (xtask/src/parts.rs) +# so that no job comes near GitHub's six-hour limit: # # crates `cargo xtask check`, the fast static checks (unsafe, lint # overrides, escape hatches, tier declarations, pins, allowlist), # which fail in a minute or two so obvious mistakes show up early; # then the crate groups (`cargo xtask crates`) for the matrix -# below, so a new crate cannot be left out. On a pull request the -# groups are only those of the selected crates -# (`cargo xtask crates --changed origin/main`, below). +# below, so a new crate cannot be left out. # base `verify --part base`: static checks, rustfmt, clippy and tests -# over the whole workspace. On a pull request the tests narrow to -# the selected crates (`--changed origin/main`); the static -# checks, rustfmt and clippy still cover the whole workspace. -# miri `verify --part miri`: the workspace's tests under Miri. On a -# pull request, the selected crates' tests only. -# base-macos the base and Miri parts on macOS arm64, one after the other -# (narrowed the same way on a pull request): +# over the whole workspace. +# miri `verify --part miri`: the workspace's tests under Miri. +# base-macos the base and Miri parts on macOS arm64, one after the other: # the Seatbelt sandbox, the demo, the host and escape tests, and # the macOS-only code under clippy and Miri. Proofs and harnesses # are not repeated there: Verus and Kani give the same answer for @@ -28,19 +20,10 @@ # conformance. One job per crate with proof work; the crates # with none share one job. Each uploads what it measured, one # file per crate, tagged with the commit. -# assemble `verify --part assemble`, the job named `Full verification`: -# needs every job above to pass, then checks that every crate's -# measurements are present and from this commit, and reports -# whether README.md's table matches them. On a pull request it -# checks only the selected crates (`--only`) and not README.md's -# table (too few rows were measured; main's full run compares -# and writes it), says so, and ends -# in `CHANGED CRATES PASSED`, never `ALL CHECKS PASSED`: it -# verified n of m crates, not all. The job keeps its name because -# CLAUDE.md and the branch protection refer to it; only its -# result line tells a partial run from a full one. -# table on pushes to main only (which are always full runs), after -# `assemble` passed: writes +# assemble `verify --part assemble`: needs every job above to pass, then +# checks that every crate's measurements are present and from +# this commit, and reports whether README.md's table matches them. +# table on pushes to main only, after `assemble` passed: writes # README.md's table from the same measurements # (`verify --part assemble --write`) and, if it changed, commits # it to main as github-actions[bot]. Changes therefore never need @@ -55,27 +38,11 @@ # binaries are only as verified as the commit's Full # verification says. # -# Which crates a pull request verifies is chosen by `xtask/src/changed.rs`, -# the same selection as `cargo xtask verify --changed`: the crates with a -# changed file, and every crate that depends on one of them, against the -# merge base of the pull request and `origin/main`. Stacked pull requests have -# other bases than main; selecting against main also includes the lower pull -# requests' crates, which is conservative and fine. A change to anything -# shared (Cargo.lock, the workspace manifest, the toolchain pins, scripts/, -# xtask/) or to this workflow selects every crate. So does any change to a -# crate's `tier` or `target-tier`: CLAUDE.md rule 7 requires a tier raise to -# pass a full verification on its pull request, and the safest way to keep -# that true is to run one for every tier change. Pushes to main and manual -# runs always select every crate, so main is verified in full after every -# merge. -# -# With every crate selected, the parts together run exactly the checks of one -# `scripts/verify.sh`, which still runs them all on one machine. Full -# verification has passed only when every job above is green on a run that -# selected every crate (a push to main, a manual run, or a pull request that -# touched something shared); `assemble` cannot be green unless the others -# were. Every part exits non-zero when a tool is missing and checks were -# skipped, so a skipped check is never green. +# Together the parts run exactly the checks of one `scripts/verify.sh`, which +# still runs them all on one machine. Verification has passed only when every +# job above is green; `assemble` cannot be, unless the others were. Every +# part exits non-zero when a tool is missing and checks were skipped, so a +# skipped check is never green. # # The crate parts run on Linux x86-64 only: it is the platform the # Dockerfile reproduces, and Verus publishes no Linux arm64 build. macOS @@ -85,12 +52,6 @@ # setup.sh's download cache is cached: setup.sh re-checks every cached file # against scripts/checksums.txt before using it, so a stale or tampered cache # entry cannot reach the proof tools. Build output is never cached. -# -# The `crates` and `base*`/`miri` jobs check out the full history on a pull -# request (`fetch-depth: 0`): the default depth of 1 has no merge base with -# main to select against. The depths are quoted strings: in an expression the -# number 0 is falsy, so `cond && 0 || 1` is always 1, while the string '0' is -# truthy. name: CI @@ -116,37 +77,19 @@ jobs: runs-on: ubuntu-24.04 timeout-minutes: 15 outputs: - # The matrix of crate groups, and the crates in it, comma-separated - # (for `assemble`). Both are everything unless this is a pull request. list: ${{ steps.list.outputs.list }} - names: ${{ steps.list.outputs.names }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} # rustup reads rust-toolchain.toml and installs the pinned toolchain. - name: Install Rust run: rustup toolchain install - name: cargo xtask check run: cargo xtask check - # Pull requests: only the crates they change and their dependents (see - # the header). The selection is printed to the log. Assigned apart from - # the echo so that a failing xtask fails the step. - id: list name: cargo xtask crates - env: - EVENT: ${{ github.event_name }} - run: | - if [ "$EVENT" = pull_request ]; then - list=$(cargo xtask crates --changed origin/main) - names=$(cargo xtask crates --names --changed origin/main) - else - list=$(cargo xtask crates) - names=$(cargo xtask crates --names) - fi - echo "list=$list" >> "$GITHUB_OUTPUT" - echo "names=$names" >> "$GITHUB_OUTPUT" + run: echo "list=$(cargo xtask crates)" >> "$GITHUB_OUTPUT" base: name: Verify (base) @@ -156,7 +99,6 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -171,7 +113,7 @@ jobs: - name: Allow the sandbox's user namespace run: sudo packaging/apparmor/allow-userns.sh clazel-test "$GITHUB_WORKSPACE/target/{debug,release}/{clazel-renderer,clazel-adversary,deps/sandbox-*}" - name: Verify (base) - run: cargo xtask verify --part base ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} + run: cargo xtask verify --part base base-macos: name: Verify (base, macOS) @@ -181,7 +123,6 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -192,11 +133,11 @@ jobs: # No AppArmor step: the renderer's macOS sandbox is Seatbelt, which an # unprivileged process enters without any setup. - name: Verify (base) - run: cargo xtask verify --part base ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} + run: cargo xtask verify --part base # Miri runs here after the base part rather than in a job of its own: # macOS runners are few (5 at once), and this job is not the slowest. - name: Verify (Miri) - run: cargo xtask verify --part miri ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} + run: cargo xtask verify --part miri miri: name: Verify (Miri) @@ -206,7 +147,6 @@ jobs: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - fetch-depth: ${{ github.event_name == 'pull_request' && '0' || '1' }} - name: Cache tool downloads uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: @@ -217,15 +157,12 @@ jobs: # No AppArmor step: tests that spawn the sandboxed renderer are # ignored under Miri. - name: Verify (Miri) - run: cargo xtask verify --part miri ${{ github.event_name == 'pull_request' && '--changed origin/main' || '' }} + run: cargo xtask verify --part miri crate: # A group of crates with no proofs is one job (`cargo xtask crates`). name: Verify ${{ contains(matrix.crate, ',') && 'crates without proofs' || matrix.crate }} needs: crates - # A pull request that selects no crate has an empty matrix, which GitHub - # rejects; the job is skipped, and `assemble` accepts that only then. - if: needs.crates.outputs.list != '[]' runs-on: ubuntu-24.04 timeout-minutes: 360 strategy: @@ -262,59 +199,24 @@ jobs: retention-days: 7 assemble: - # Named `Full verification` for CLAUDE.md and the branch protection. On a - # pull request it verifies only the selected crates and ends in - # `CHANGED CRATES PASSED`; see the header. name: Full verification needs: [crates, base, base-macos, miri, crate] - # Runs even when a job it needs failed or was skipped, and fails then: - # a skipped job is not a pass, and a skipped required check would count - # as one. Only a cancelled run is not judged. - if: ${{ !cancelled() }} runs-on: ubuntu-24.04 timeout-minutes: 30 steps: - - name: Every job passed - env: - NEEDS: ${{ toJSON(needs) }} - LIST: ${{ needs.crates.outputs.list }} - run: | - # `crate` may be skipped only when no crate was selected. - bad=$(echo "$NEEDS" | jq -r --arg list "$LIST" ' - to_entries[] - | select(.value.result != "success") - | select(.key != "crate" or $list != "[]" or .value.result != "skipped") - | "\(.key): \(.value.result)"') - if [ -n "$bad" ]; then - echo "Not every job passed:" - echo "$bad" - exit 1 - fi - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - name: Install Rust run: rustup toolchain install - name: Download measurements - # Nothing was measured when no crate was selected. - if: needs.crates.outputs.list != '[]' uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: pattern: part-* path: parts merge-multiple: true - # Pull requests require the selected crates' measurements only. Pushes - # to main and manual runs require every crate's. - name: Assemble - env: - EVENT: ${{ github.event_name }} - NAMES: ${{ needs.crates.outputs.names }} - run: | - if [ "$EVENT" = pull_request ]; then - cargo xtask verify --part assemble --metrics parts --only "$NAMES" - else - cargo xtask verify --part assemble --metrics parts - fi + run: cargo xtask verify --part assemble --metrics parts table: name: Update README table diff --git a/CLAUDE.md b/CLAUDE.md index 2f3a3296..5aecfc27 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -53,8 +53,7 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. crate's `Cargo.toml` requires all of the following, and `cargo xtask check` rejects the claim otherwise: - every proof and harness passing in a full `cargo xtask verify`, which - for a tier change means CI's green run on the pull request, which - verifies every crate whenever a `tier` or `target-tier` changes (a local + for a tier change means CI's green run on the pull request (a local `--changed` run does not count); - Tier 1: Kani harnesses; - Tier 2: Verus enabled; every mutation in `mutations.json` a `killed` with @@ -86,14 +85,9 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. them; a change to anything shared (`Cargo.lock`, the workspace manifest, toolchain pins, `scripts/`, `xtask/`) makes it check every crate. It ends in `CHANGED CRATES PASSED`, which is not `ALL CHECKS PASSED` and must not - be reported as such. Work is **done** only when CI (every job of - `.github/workflows/ci.yml`, ending in `Full verification`) is green on its - pull request, and the full run on `main` after the merge is green. A pull - request's CI verifies only the crates it changes and their dependents, and - its `Full verification` then ends in `CHANGED CRATES PASSED`, which is not - `ALL CHECKS PASSED`; a change to anything shared, to `ci.yml` or to a - crate's tier verifies every crate, and `main` is always verified in full. - Say so if CI has not run yet. To repeat CI's run locally, use `scripts/verify.sh` or the + be reported as such. Work is **done** only when CI's full verification + (every job of `.github/workflows/ci.yml`, ending in `Full verification`) + is green on its pull request; say so if it has not run yet. To repeat CI's run locally, use `scripts/verify.sh` or the Docker command in README.md. `cargo xtask check` runs only the fast static checks (unsafe, the `clazel-sys` audit, lint overrides, escape hatches, tier declarations, pins); use it while iterating, never as the final diff --git a/README.md b/README.md index 4ab5441d..f60caf7d 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Status: Phases 0 (foundations) and 1 (verified primitives) are complete: UTF-8 (`clazel-encoding`), percent-encoding (`clazel-percent`), forgiving base64 (`clazel-base64`), MIME types and sniffing (`clazel-mime`), IDNA (`clazel-idna`) and URLs (`clazel-url`) are at Tier 2, on macOS and on -Linux CI. Phase 2 (kernel and IPC) is in progress; see the table below and +Linux CI. Phase 2 (kernel and IPC) is complete; see the table below and [docs/phases/phase-2.md](docs/phases/phase-2.md). Phase 3 (networking) has HTTP field syntax, HTTP/1.1 response framing and request serialization (`clazel-http`), DNS (`clazel-dns`) and the request builder (`clazel-fetch`) @@ -77,15 +77,13 @@ rows for the Phase 3 crates, which stay at tier 0. **Phase 2 process tests: where they have run.** The demo (`cargo run -p clazel -- demo`), the sandbox escape attempts, the hostile-renderer test and the WPT -`cookies/` run through real processes (item 2.16) have been run on macOS arm64 -only, locally: macOS is not in CI. On Linux they have never run (they were -written on a Mac), and CI on `ubuntu-24.04` cannot run them until a maintainer -decides how to allow unprivileged user namespaces for the renderer, which -otherwise fails closed (see item 2.16 in -[docs/phases/phase-2.md](docs/phases/phase-2.md)). Attempts to `fork` and to -`ptrace` a sibling are not made yet: they need a `clazel-sys` addition and its -audit. The table has rows for `clazel` and `clazel-renderer` once CI next -updates it. +`cookies/` run through real processes (item 2.16) run in CI on Linux x86-64 +(`ubuntu-24.04`) and on macOS arm64. On Ubuntu the renderer needs an AppArmor +profile that allows unprivileged user namespaces, or it fails closed; CI loads +it, and so does the release tarball's `install.sh` (see item 2.16 in +[docs/phases/phase-2.md](docs/phases/phase-2.md)). The escape attempts include +`fork` and `ptrace` of a sibling. Where Yama restricts `ptrace` on Linux, the +`ptrace` result shows less than it does on macOS. Formalizing the standards has already found one spec bug: see [docs/ERRATA.md](docs/ERRATA.md). @@ -151,8 +149,8 @@ and much of it is work only a person can do. and independent engines (`tests/conformance*.rs`). Point us at suites we have not vendored, or at engines worth differential testing against. - **Run it where we have not.** The Phase 2 process tests (the sandbox, the - hostile renderer) have only run on macOS arm64, and never on Linux. The README - says why under the status table. + hostile renderer) run in CI on `ubuntu-24.04` and macOS arm64 only. Other + Linux distributions and kernels are untested. - **Read `clazel-sys`.** It is the only crate with `unsafe`: 14 blocks that enter the OS sandbox. Every change is audited by a second model ([docs/SYS-AUDITS.md](docs/SYS-AUDITS.md)); a person reading it too is @@ -162,8 +160,7 @@ and much of it is work only a person can do. `phase3/tls` branch until it passes CI. Contributions go through the same machine checks as everything else, whoever (or whatever) wrote them: read [CLAUDE.md](CLAUDE.md) first, and expect `cargo xtask verify --changed` and - CI to be the bar (a pull request's changed crates and their dependents; `main` - in full). + CI's full verification to be the bar. ## License diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 1c16955f..83c12415 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -83,60 +83,40 @@ installs nothing if a checksum differs. The full `cargo xtask verify` takes hours, so it runs where it is the gate: in CI (`.github/workflows/ci.yml`), on Linux x86-64 with the pinned -toolchain. Every push to `main` is verified in full. A pull request is -verified in part: the crates it changes and every crate that depends on one -(the selection of `--changed`, below, against the merge base with `origin/main`; -for a stacked pull request that also includes the lower pull requests' -crates, which is conservative). A change to anything shared, to -`.github/workflows/ci.yml`, or to any crate's `tier` or `target-tier` -selects every crate, so a pull request that raises a tier gets a full -verification. Nothing is done, and no tier is raised, until that run is -green, and `main`'s full run after the merge is green too. +toolchain, on every push to `main` and every pull request. Nothing is done, +and no tier is raised, until that run is green. CI splits the run into parts, one job each, so no job comes near GitHub's six-hour limit (`xtask/src/parts.rs`): - `verify --part base`: static checks, rustfmt, clippy and tests over the - whole workspace. On a pull request, `--changed origin/main` narrows the - tests to the selected crates; the static checks, rustfmt and clippy still - cover the whole workspace. + whole workspace. - `verify --part miri`: static checks, then the workspace's tests under - Miri (on a pull request, the selected crates' only). On macOS it runs in - the same job as `base`, after it. + Miri. On macOS it runs in the same job as `base`, after it. - `verify --part crate --metrics `, where `` is one crate or several separated by commas: static checks, then Kani, Verus, line counts, mutations and conformance for those crates. CI runs one job per crate with proof work (Verus, Kani harnesses or mutations) and one job for all the others together; the groups come from `cargo xtask - crates` (on a pull request `cargo xtask crates --changed origin/main`, the - groups of the selected crates only). Mutants run several at a time, each in its own sandbox + crates`. Mutants run several at a time, each in its own sandbox (`CLAZEL_MUTANT_JOBS`, default one per core up to 4). On success it writes what it measured to `/.json` for each crate, tagged with the commit (with `+dirty` if tracked files have uncommitted changes). -- `verify --part assemble --metrics `, the `Full verification` job, - which fails unless every other job passed: static checks, then it - requires a file for every workspace crate from this commit, and reports - whether README.md's table matches them. On a pull request it gets - `--only ` and requires the selected crates' files only, and does - not compare README.md's table (it has too few rows measured; the full run - on `main` compares and writes it); it then ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL - CHECKS PASSED`, as `verify --changed` does. The job keeps the name `Full - verification` in both cases; the result line says which it was. +- `verify --part assemble --metrics `, which runs only after every + other job passed: static checks, then it requires a file for every + workspace crate from this commit, and reports whether README.md's table + matches them. - On pushes to `main` only, the `table` job runs the same part with `--write` after `assemble` passed, and commits README.md's regenerated table to `main` as github-actions[bot] if it changed. So the committed table always comes from CI's own measurements of a fully verified commit, - and no change has to carry it. A push to `main` always selects every - crate, and `--write` cannot be combined with `--only`. + and no change has to carry it. The parts together run exactly the checks of one `cargo xtask verify`, which `scripts/verify.sh` and the Docker command in README.md still run on one machine. "CI is green" means every job passed on the same commit, the -`Full verification` (assemble) job included. On a pull request that is a -verification of the selected crates; only a run that selected every crate -(`main`, a manual run, a change to something shared or to a tier) is a full -one. +`Full verification` (assemble) job included. Locally, `cargo xtask verify --changed [base]` runs the same checks over less. `base` defaults to `origin/main`, the last commit CI verified, and @@ -148,15 +128,10 @@ untracked files) with HEAD's merge base with it (`xtask/src/changed.rs`): - Tests, Miri, Kani, Verus, mutations and conformance run only for the crates with a changed file and every crate that depends on one of them, directly or not, dev-dependencies included. -- A change anywhere else, except `docs/`, `.github/` (but not - `.github/workflows/ci.yml`), `.claude/`, README.md, CLAUDE.md, LICENSE and - `.gitignore`, checks every crate. That covers `Cargo.lock`, the workspace - `Cargo.toml`, `rust-toolchain.toml`, `scripts/`, `xtask/`, which decides - what passing means, and the CI workflow, which decides what CI runs. -- So does any change to a line of a crate's `Cargo.toml` that mentions a - tier (`tier`, `target-tier`), or a new or removed crate manifest: rule 7 - requires a tier raise to pass a full verification, so the safest choice - is a full one for every tier change. +- A change anywhere else, except `docs/`, `.github/`, `.claude/`, README.md, + CLAUDE.md, LICENSE and `.gitignore`, checks every crate. That covers + `Cargo.lock`, the workspace `Cargo.toml`, `rust-toolchain.toml`, + `scripts/` and `xtask/`, which decides what passing means. - The run ends in `RESULT: CHANGED CRATES PASSED (n of m crates …)`, never `ALL CHECKS PASSED`. @@ -174,8 +149,8 @@ What this relies on: that a crate's proofs and tests depend only on its own files, the workspace crates it depends on, and the shared files listed above. Verus, Kani and the tests read nothing else, but a crate that read a file outside its directory (say, another crate's vendored data through -`include_str!`) would not be re-checked when that file changed. The full -run on `main` catches it; a local run or a pull request's CI may not. +`include_str!`) would not be re-checked when that file changed. CI's full +run catches it; the local run may not. ## Trusted computing base (what we do *not* prove) diff --git a/xtask/src/changed.rs b/xtask/src/changed.rs index 05456d80..9d2ec832 100644 --- a/xtask/src/changed.rs +++ b/xtask/src/changed.rs @@ -6,19 +6,12 @@ //! because its proofs and tests may rest on the changed one. A change to any //! file outside every crate and outside the list in [`is_inert`] selects //! every crate: `Cargo.lock`, the workspace `Cargo.toml`, the toolchain -//! pins, `scripts/`, `xtask/` itself (which decides what passing means) and -//! the CI workflow (which decides what CI runs) can change any crate's -//! result. +//! pins, `scripts/` and `xtask/` itself (which decides what passing means) +//! can change any crate's result. //! -//! So can a change to a crate's `tier` or `target-tier` (see -//! [`tier_lines_differ`]): CLAUDE.md rule 7 requires a tier raise to pass a -//! full verification on its pull request, so such a change selects every -//! crate, the safest choice. -//! -//! The same selection narrows a pull request's CI run (`cargo xtask crates -//! --changed`, `.github/workflows/ci.yml`). `main` is always verified in -//! full, and that run is the gate (docs/VERIFICATION.md, "Local and CI -//! runs"). +//! This narrows only what a local run checks. CI runs `cargo xtask verify` +//! in full on every push and pull request, and that run is the gate +//! (docs/VERIFICATION.md, "Local and CI runs"). use std::collections::BTreeSet; use std::path::Path; @@ -38,59 +31,21 @@ pub enum Selection { Some(BTreeSet), } -/// The CI workflow. It decides what CI runs, so a change to it is a change -/// to everything: it is not inert. -const CI_WORKFLOW: &str = ".github/workflows/ci.yml"; - /// Paths outside every crate whose changes cannot alter any crate's build, /// proofs, tests or measurements. Everything they feed is re-checked by the /// static checks, which `--changed` always runs in full: `docs/` holds the /// dependency allowlist, spec reviews and `clazel-sys` audits, and -/// README.md's status table is compared row by row. The rest of `.github/` -/// is inert, but not [`CI_WORKFLOW`]. +/// README.md's status table is compared row by row. fn is_inert(path: &str) -> bool { path.starts_with("docs/") - || (path.starts_with(".github/") && path != CI_WORKFLOW) + || path.starts_with(".github/") || path.starts_with(".claude/") || matches!(path, "README.md" | "CLAUDE.md" | "LICENSE" | ".gitignore") } -/// The lines of a manifest that mention a tier (`tier = 2`, -/// `target-tier = 2`, a dotted `metadata.clazel.tier = 2`, an inline table), -/// comments dropped and whitespace removed, sorted. Deliberately loose: it -/// can only over-report a change, which selects more, never less. -fn tier_lines(manifest: &str) -> Vec { - let mut lines: Vec = manifest - .lines() - .map(|l| l.split('#').next().unwrap_or("")) - .filter(|l| l.contains("tier")) - .map(|l| l.split_whitespace().collect::()) - .collect(); - lines.sort(); - lines -} - -/// Whether the tier declarations differ between two versions of a crate's -/// `Cargo.toml` (`None`: the file did not exist). -pub fn tier_lines_differ(old: Option<&str>, new: Option<&str>) -> bool { - old.map(tier_lines) != new.map(tier_lines) -} - /// The crates to check for `changed` paths (relative to the repository -/// root, `/`-separated). `tier_changed` are the crate manifests among them -/// whose tier declarations differ ([`tier_lines_differ`]); any selects -/// every crate. -pub fn select_paths( - crates: &[Crate], - root: &Path, - changed: &[String], - tier_changed: &[String], -) -> Selection { - if let Some(path) = tier_changed.first() { - return Selection::All(format!( - "{path} changed its tier or target-tier (a tier change needs a full verification, CLAUDE.md rule 7)" - )); - } +/// root, `/`-separated). +pub fn select_paths(crates: &[Crate], root: &Path, changed: &[String]) -> Selection { let dirs: Vec<(String, String)> = crates .iter() .filter_map(|c| { @@ -129,7 +84,7 @@ pub fn select_paths( /// Paths that differ between the merge base of HEAD and `base` and the /// working tree: committed, staged, unstaged and untracked (not ignored). -fn changed_paths(base: &str) -> Result<(String, Vec, Vec), String> { +fn changed_paths(base: &str) -> Result<(String, Vec), String> { let git = |args: &[&str]| -> Result { let out = Command::new("git") .args(args) @@ -153,32 +108,20 @@ fn changed_paths(base: &str) -> Result<(String, Vec, Vec), Strin ] { paths.extend(out.lines().map(str::to_owned)); } - // Crate manifests whose tier declarations changed (or that are new). - let mut tier_changed = Vec::new(); - for path in paths.iter().filter(|p| p.ends_with("/Cargo.toml")) { - let old = git(&["show", &format!("{merge_base}:{path}")]).ok(); - let new = std::fs::read_to_string(path).ok(); - if tier_lines_differ(old.as_deref(), new.as_deref()) { - tier_changed.push(path.clone()); - } - } - Ok((merge_base, paths.into_iter().collect(), tier_changed)) + Ok((merge_base, paths.into_iter().collect())) } /// The selection for this checkout against `base`, and the merge base used. pub fn select(crates: &[Crate], root: &Path, base: &str) -> Result<(String, Selection), String> { - let (merge_base, paths, tier_changed) = changed_paths(base)?; - Ok(( - merge_base, - select_paths(crates, root, &paths, &tier_changed), - )) + let (merge_base, paths) = changed_paths(base)?; + Ok((merge_base, select_paths(crates, root, &paths))) } #[cfg(test)] mod tests { use std::path::PathBuf; - use super::{Selection, select_paths, tier_lines_differ}; + use super::{Selection, select_paths}; use crate::workspace::Crate; fn krate(name: &str, deps: &[&str]) -> Crate { @@ -219,13 +162,7 @@ mod tests { fn sel(paths: &[&str]) -> Selection { let paths: Vec = paths.iter().map(|p| (*p).to_owned()).collect(); - select_paths(&ws(), std::path::Path::new("/r"), &paths, &[]) - } - - fn sel_tier(paths: &[&str], tier_changed: &[&str]) -> Selection { - let paths: Vec = paths.iter().map(|p| (*p).to_owned()).collect(); - let tier: Vec = tier_changed.iter().map(|p| (*p).to_owned()).collect(); - select_paths(&ws(), std::path::Path::new("/r"), &paths, &tier) + select_paths(&ws(), std::path::Path::new("/r"), &paths) } fn some(names: &[&str]) -> Selection { @@ -250,65 +187,12 @@ mod tests { #[test] fn docs_and_readme_select_nothing() { assert_eq!( - sel(&[ - "docs/ROADMAP.md", - "README.md", - ".github/dependabot.yml", - ".github/workflows/other.yml" - ]), + sel(&["docs/ROADMAP.md", "README.md", ".github/workflows/ci.yml"]), some(&[]) ); assert_eq!(sel(&[]), some(&[])); } - #[test] - fn a_change_to_the_ci_workflow_selects_everything() { - for paths in [ - &[".github/workflows/ci.yml"][..], - &["crates/sandbox/src/lib.rs", ".github/workflows/ci.yml"][..], - ] { - assert!(matches!(sel(paths), Selection::All(_)), "{paths:?}"); - } - } - - #[test] - fn a_tier_change_selects_everything() { - // The manifest alone would select only `sandbox`. - assert_eq!(sel(&["crates/sandbox/Cargo.toml"]), some(&["sandbox"])); - assert!(matches!( - sel_tier( - &["crates/sandbox/Cargo.toml"], - &["crates/sandbox/Cargo.toml"] - ), - Selection::All(_) - )); - } - - #[test] - fn tier_declarations_are_compared_line_by_line() { - let base = - "[package]\nname = \"a\"\n[package.metadata.clazel]\ntier = 1 # now\ntarget-tier = 2\n"; - // Other edits, comments and spacing are not tier changes. - let edited = "[package]\nname = \"a\"\nversion = \"0.1.0\"\n[package.metadata.clazel]\ntier=1\ntarget-tier = 2 # goal\n"; - assert!(!tier_lines_differ(Some(base), Some(edited))); - assert!(!tier_lines_differ(None, None)); - // A raise, a lowered target, a dotted key, a new or removed manifest. - assert!(tier_lines_differ( - Some(base), - Some(&base.replace("tier = 1", "tier = 2")) - )); - assert!(tier_lines_differ( - Some(base), - Some(&base.replace("target-tier = 2", "target-tier = 1")) - )); - assert!(tier_lines_differ( - Some(base), - Some(&format!("{base}metadata.clazel.tier = 2\n")) - )); - assert!(tier_lines_differ(None, Some(base))); - assert!(tier_lines_differ(Some(base), None)); - } - #[test] fn shared_inputs_select_everything() { for p in [ diff --git a/xtask/src/main.rs b/xtask/src/main.rs index 7f98fe6e..ff3ed373 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -6,16 +6,12 @@ //! - `cargo xtask verify --changed [base]`: the same checks, but tests, Miri, //! Kani, Verus, mutations and conformance only for the crates that changed //! since `base` (default `origin/main`) and their dependents (`changed.rs`). -//! Ends in `CHANGED CRATES PASSED`; the full run on `main` is the gate. -//! - `cargo xtask verify --part (base|miri [--changed [base]]|crate -//! --metrics |assemble --metrics [--write|--only ])`: the -//! same checks split into parts for separate CI jobs (`parts.rs`); -//! `cargo xtask crates [--names] [--changed [base]]` lists the crates for -//! them, only the changed ones with `--changed`, which CI uses on pull -//! requests. `assemble --write` writes README.md's table from the parts, -//! which CI does on main. `assemble --only` requires just those crates' -//! parts, for a pull request's partial run, and ends in `CHANGED CRATES -//! PASSED`. +//! Ends in `CHANGED CRATES PASSED`; CI's full run is the gate. +//! - `cargo xtask verify --part (base|crate --metrics |assemble +//! --metrics [--write])`: the same checks split into parts for +//! separate CI jobs (`parts.rs`); `cargo xtask crates` lists the crates for +//! them. `assemble --write` writes README.md's table from the parts, which +//! CI does on main. //! - `cargo xtask check`: only the fast static checks (no build, no proofs). //! - `cargo xtask mutate`: only the proof mutation tests (also part of //! `verify`). @@ -51,7 +47,6 @@ mod unicode; mod verus; mod workspace; -use std::collections::BTreeSet; use std::path::{Path, PathBuf}; use std::process::{Command, ExitCode}; @@ -754,9 +749,12 @@ fn conformance_suites(r: &mut Runner, crates: &[Crate]) { } } -/// The host shell's size against its limit, as a step; its line count when -/// it could be counted (`None` if the directory does not exist). -fn host_shell_size(r: &mut Runner) -> Option> { +/// Compare (or, with `write`, update) README.md's status table against what +/// this run measured. With `only` (a `--changed` run), the other crates' +/// proof and test columns are carried over from README.md's current table, +/// since their inputs did not change; CI's full run re-measures them all. +fn readme_table(r: &mut Runner, write: bool, only: Option<&[Crate]>) { + const NAME: &str = "README status table"; let host_shell_count = report::host_shell_lines(std::path::Path::new(report::HOST_SHELL_DIR)); if let Some(counted) = host_shell_count.as_ref() { match counted { @@ -774,16 +772,6 @@ fn host_shell_size(r: &mut Runner) -> Option> { Err(e) => r.step("host shell size", Outcome::Fail(vec![e.clone()])), } } - host_shell_count -} - -/// Compare (or, with `write`, update) README.md's status table against what -/// this run measured. With `only` (a `--changed` run), the other crates' -/// proof and test columns are carried over from README.md's current table, -/// since their inputs did not change; CI's full run re-measures them all. -fn readme_table(r: &mut Runner, write: bool, only: Option<&[Crate]>) { - const NAME: &str = "README status table"; - let host_shell_count = host_shell_size(r); let carried = match only { None => report::Rows::new(), Some(cs) => { @@ -931,59 +919,30 @@ fn generate_tables() -> ExitCode { } } -/// The crates a `--changed` run repeats proofs and tests for, against -/// `base`, recorded as a step; `None` means every crate (or a failure, -/// which the step records). Also returns the merge base used. -fn changed_selection( - r: &mut Runner, - crates: &[Crate], - root: &Path, - base: &str, -) -> Option<(String, Vec)> { - match changed::select(crates, root, base) { - Ok((merge_base, changed::Selection::All(why))) => { - r.step( - "select changed crates", - Outcome::Pass(vec![format!( - "every crate is checked: {why} since {base} ({merge_base})" - )]), - ); - None - } - Ok((merge_base, changed::Selection::Some(names))) => { - let picked: Vec = crates - .iter() - .filter(|c| names.contains(&c.name)) - .cloned() - .collect(); - r.step( - "select changed crates", - Outcome::Pass(vec![format!( - "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", - picked.len(), - crates.len(), - if names.is_empty() { - "none".to_owned() - } else { - names.iter().cloned().collect::>().join(", ") - } - )]), - ); - Some((merge_base, picked)) - } - Err(e) => { - r.step("select changed crates", Outcome::Fail(vec![e])); - None - } - } -} - fn main() -> ExitCode { let args: Vec = std::env::args().skip(1).collect(); let args: Vec<&str> = args.iter().map(String::as_str).collect(); - // `verify` and `report` take `--changed []` (changed.rs), and so do - // the `base` and `miri` parts and `crates`, which CI runs that way on - // pull requests. + // `verify --part ...` (parts.rs) and `crates` are handled apart. + let part = match args.as_slice() { + ["verify", "--part", "base"] => Some(Part::Base), + ["verify", "--part", "miri"] => Some(Part::Miri), + ["verify", "--part", "crate", names, "--metrics", dir] => Some(Part::Crate( + names.split(',').map(str::to_owned).collect(), + PathBuf::from(dir), + )), + ["verify", "--part", "assemble", "--metrics", dir] => { + Some(Part::Assemble(PathBuf::from(dir), false)) + } + ["verify", "--part", "assemble", "--metrics", dir, "--write"] => { + Some(Part::Assemble(PathBuf::from(dir), true)) + } + ["crates"] => Some(Part::ListCrates), + _ => None, + }; + let args = if part.is_some() { vec!["check"] } else { args }; + // `mutate ` runs one crate's mutations, for iterating on them. + let mut only_crate: Option<&str> = None; + // `verify` and `report` take `--changed []` (changed.rs). let (args, base) = match args.iter().position(|a| *a == "--changed") { Some(i) => { let (head, tail) = args.split_at(i); @@ -995,56 +954,6 @@ fn main() -> ExitCode { } None => (args.as_slice(), None), }; - let base_owned = base.map(str::to_owned); - // `verify --part ...` (parts.rs) and `crates` are handled apart. - let part = match (args, base) { - (["verify", "--part", "base"], _) => Some(Part::Base(base_owned)), - (["verify", "--part", "miri"], _) => Some(Part::Miri(base_owned)), - (["verify", "--part", "crate", names, "--metrics", dir], None) => Some(Part::Crate( - names.split(',').map(str::to_owned).collect(), - PathBuf::from(dir), - )), - (["verify", "--part", "assemble", "--metrics", dir], None) => { - Some(Part::Assemble(PathBuf::from(dir), false, None)) - } - (["verify", "--part", "assemble", "--metrics", dir, "--write"], None) => { - Some(Part::Assemble(PathBuf::from(dir), true, None)) - } - // A pull request's partial run: only these crates' measurements. - // Never together with `--write`: the table comes from full runs. - ( - [ - "verify", - "--part", - "assemble", - "--metrics", - dir, - "--only", - names, - ], - None, - ) => Some(Part::Assemble( - PathBuf::from(dir), - false, - Some( - names - .split(',') - .filter(|n| !n.is_empty()) - .map(str::to_owned) - .collect(), - ), - )), - (["crates"], _) => Some(Part::ListCrates(false, base_owned)), - (["crates", "--names"], _) => Some(Part::ListCrates(true, base_owned)), - _ => None, - }; - let (args, base) = if part.is_some() { - (&["check"][..], None) - } else { - (args, base) - }; - // `mutate ` runs one crate's mutations, for iterating on them. - let mut only_crate: Option<&str> = None; let (full, only_mutate, report_mode, write) = match (args, base) { (["testdata"], None) => return generate_testdata(), (["tables"], None) => return generate_tables(), @@ -1059,7 +968,7 @@ fn main() -> ExitCode { (["report", "--write"], _) => (false, false, true, true), _ => { eprintln!( - "usage: cargo xtask --metrics |assemble --metrics [--write|--only ])|crates [--names] [--changed [base]]|check|mutate [crate]|testdata|tables|report [--write] [--changed [base]]>" + "usage: cargo xtask --metrics |assemble --metrics [--write])|crates|check|mutate [crate]|testdata|tables|report [--write] [--changed [base]]>" ); return ExitCode::from(64); } @@ -1104,7 +1013,36 @@ fn main() -> ExitCode { // `None` means every crate. let mut partial: Option<(String, Vec)> = None; if let Some(base) = base { - partial = changed_selection(&mut r, &crates, &root, base); + match changed::select(&crates, &root, base) { + Ok((merge_base, changed::Selection::All(why))) => r.step( + "select changed crates", + Outcome::Pass(vec![format!( + "every crate is checked: {why} since {base} ({merge_base})" + )]), + ), + Ok((merge_base, changed::Selection::Some(names))) => { + let picked: Vec = crates + .iter() + .filter(|c| names.contains(&c.name)) + .cloned() + .collect(); + r.step( + "select changed crates", + Outcome::Pass(vec![format!( + "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", + picked.len(), + crates.len(), + if names.is_empty() { + "none".to_owned() + } else { + names.iter().cloned().collect::>().join(", ") + } + )]), + ); + partial = Some((merge_base, picked)); + } + Err(e) => r.step("select changed crates", Outcome::Fail(vec![e])), + } } let checked: &[Crate] = partial.as_ref().map_or(&crates, |(_, p)| p.as_slice()); let only = partial.as_ref().map(|(_, p)| p.as_slice()); @@ -1152,38 +1090,23 @@ fn main() -> ExitCode { /// One part of a split verification (parts.rs). enum Part { - /// With a base ref (`--changed`), tests only for the changed crates. - Base(Option), - /// With a base ref (`--changed`), Miri only for the changed crates. - Miri(Option), + Base, + Miri, /// One or more crates (comma-separated on the command line; CI groups /// the crates with no proofs into one job, see [`crate_groups`]). Crate(Vec, PathBuf), - /// The crate parts' directory, whether to write README.md's table - /// from them (CI does, on main, after every part passed), and, for a - /// pull request's partial run, the only crates whose measurements are - /// required (never together with writing). - Assemble(PathBuf, bool, Option>), + /// The crate parts' directory, and whether to write README.md's table + /// from them (CI does, on main, after every part passed). + Assemble(PathBuf, bool), /// `cargo xtask crates`: the crate groups as a JSON array of - /// comma-separated names, for CI's matrix of `crate` parts; with a base - /// ref (`--changed`), only the groups of the changed crates. With - /// `--names` (the flag), the crates themselves, comma-separated. - ListCrates(bool, Option), + /// comma-separated names, for CI's matrix of `crate` parts. + ListCrates, } /// CI's crate parts: one per crate with proof work (Verus, Kani harnesses or /// mutations), and one for all the others together, which finish in about /// a minute each and would otherwise each hold a runner for its setup. -/// -/// Only the crates in `selected` are grouped (a pull request's job list); -/// a group left empty is dropped. -fn crate_groups(crates: &[Crate], selected: &BTreeSet<&str>) -> Vec { - let crates: Vec = crates - .iter() - .filter(|c| selected.contains(c.name.as_str())) - .cloned() - .collect(); - let crates = crates.as_slice(); +fn crate_groups(crates: &[Crate]) -> Vec { let light = |c: &Crate| { !c.verus && !mutate::has_mutations(c) @@ -1206,85 +1129,19 @@ fn crate_groups(crates: &[Crate], selected: &BTreeSet<&str>) -> Vec { } fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Path) -> ExitCode { - if let Part::ListCrates(names, base) = part { - // The selection goes to stderr (the CI log); stdout is the list. - let selected: BTreeSet<&str> = match base { - None => crates.iter().map(|c| c.name.as_str()).collect(), - Some(base) => match changed::select(crates, root, &base) { - Ok((merge_base, changed::Selection::All(why))) => { - eprintln!("every crate: {why} since {base} ({merge_base})"); - crates.iter().map(|c| c.name.as_str()).collect() - } - Ok((merge_base, changed::Selection::Some(sel))) => { - eprintln!( - "{} of {} crates changed since {base} ({merge_base}), or depend on one that did: {}", - sel.len(), - crates.len(), - sel.iter().cloned().collect::>().join(", ") - ); - crates - .iter() - .map(|c| c.name.as_str()) - .filter(|n| sel.contains(*n)) - .collect() - } - Err(e) => { - eprintln!("select changed crates: {e}"); - return ExitCode::from(1); - } - }, - }; - if names { - println!( - "{}", - crates - .iter() - .map(|c| c.name.as_str()) - .filter(|n| selected.contains(n)) - .collect::>() - .join(",") - ); - } else { - println!( - "{}", - serde_json::Value::from(crate_groups(crates, &selected)) - ); - } + if let Part::ListCrates = part { + println!("{}", serde_json::Value::from(crate_groups(crates))); return ExitCode::SUCCESS; } static_checks(r, crates, pins); let done = match part { - Part::Base(base) => { - // Rustfmt and clippy always cover the whole workspace; only the - // tests narrow to the changed crates and their dependents. - let picked = base - .as_deref() - .and_then(|b| changed_selection(r, crates, root, b)); - let only = picked.as_ref().map(|(_, p)| p.as_slice()); - build_checks(r, only); - match &picked { - Some((_, p)) => format!( - "BASE PART PASSED (static checks, rustfmt and clippy over the workspace; tests of {} of {} crates, the changed ones and their dependents)", - p.len(), - crates.len() - ), - None => "BASE PART PASSED (static checks, rustfmt, clippy and tests; Miri runs in the miri part, proofs in the crate parts)".to_owned(), - } + Part::Base => { + build_checks(r, None); + "BASE PART PASSED (static checks, rustfmt, clippy and tests; Miri runs in the miri part, proofs in the crate parts)".to_owned() } - Part::Miri(base) => { - let picked = base - .as_deref() - .and_then(|b| changed_selection(r, crates, root, b)); - let only = picked.as_ref().map(|(_, p)| p.as_slice()); - miri(r, pins, only); - match &picked { - Some((_, p)) => format!( - "MIRI PART PASSED (static checks and the tests of {} of {} crates under Miri, the changed ones and their dependents)", - p.len(), - crates.len() - ), - None => "MIRI PART PASSED (static checks and the tests under Miri)".to_owned(), - } + Part::Miri => { + miri(r, pins, None); + "MIRI PART PASSED (static checks and the tests under Miri)".to_owned() } Part::Crate(names, dir) => { let mut selected: Vec = Vec::new(); @@ -1322,33 +1179,10 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa names.join(", ") ) } - Part::Assemble(dir, write, only) => { - // With `only` (a pull request's partial run) just those crates - // are required; every other crate is not claimed at all. - let mut required: Vec = Vec::new(); - match &only { - None => required = crates.to_vec(), - Some(names) => { - for name in names { - match crates.iter().find(|c| &c.name == name) { - Some(c) => required.push(c.clone()), - None => { - r.step( - "select crate", - Outcome::Fail(vec![format!( - "no workspace crate named {name:?}" - )]), - ); - println!("RESULT: FAILED"); - return ExitCode::from(1); - } - } - } - } - } + Part::Assemble(dir, write) => { let res = parts::head().and_then(|commit| { let mut problems = Vec::new(); - for c in &required { + for c in crates { let path = dir.join(format!("{}.json", c.name)); let entry = r.metrics.entry(c.name.clone()).or_default(); let read = std::fs::read_to_string(&path) @@ -1360,8 +1194,7 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa } if problems.is_empty() { Ok(vec![format!( - "{} of {} crate parts, all from {commit}", - required.len(), + "{} crate parts, all from {commit}", crates.len() )]) } else { @@ -1369,32 +1202,12 @@ fn run_part(r: &mut Runner, part: Part, crates: &[Crate], pins: &Pins, root: &Pa } }); r.step("read crate parts", from_result(res)); - if only.is_some() { - // A partial run has measured too few rows to compare the - // table, whose rows the full run on main checks and writes. - // The host shell's size limit does not depend on them. - host_shell_size(r); - r.step( - "README status table", - Outcome::Pass(vec![ - "compared only in a full run (main), which measures every row".into(), - ]), - ); - } else if !r.failed { + if !r.failed { readme_table(r, write, None); } - match &only { - None => "PARTS ASSEMBLED (every crate part present and from this commit; the gate is this and every part passing on the same commit)".to_owned(), - // Never "ALL CHECKS PASSED" or "PARTS ASSEMBLED": most - // crates' proofs did not run. - Some(_) => format!( - "CHANGED CRATES PASSED ({} of {} crates' parts present and from this commit; the other crates' proofs did not run here, and the full verification runs on main after merge)", - required.len(), - crates.len() - ), - } + "PARTS ASSEMBLED (every crate part present and from this commit; the gate is this and every part passing on the same commit)".to_owned() } - Part::ListCrates(..) => String::new(), + Part::ListCrates => String::new(), }; if r.failed { println!("RESULT: FAILED"); From 28638ad171be9cef5877edc1d401b20172e6fa43 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Wed, 28 Oct 2026 16:49:04 +0000 Subject: [PATCH 6/7] ci: pull requests skip the proofs; main and manual runs verify in full Opening pull requests, however many, now starts only the cheap jobs (static checks, rustfmt, clippy, tests, Miri, release build). The `crate` proof jobs run on pushes to main and on manual runs, which need write access. On a pull request the last job is named `Pull request checks` and ends in PULL REQUEST CHECKS PASSED, never a full verification. That job now runs even when a job it needs failed or was skipped, and fails then, so a skipped required check cannot count as a pass. A tier raise needs a green manual run on its branch before merging (CLAUDE.md rule 7). Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 61 ++++++++++++++++++++++++++++++++++------ CLAUDE.md | 16 +++++++---- README.md | 3 +- docs/VERIFICATION.md | 28 +++++++++++------- 4 files changed, 83 insertions(+), 25 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3fb4a90e..4fc9595e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,6 +1,12 @@ -# Runs the checks in docs/VERIFICATION.md on every push to main and every -# pull request. The full verification is split into parts (xtask/src/parts.rs) -# so that no job comes near GitHub's six-hour limit: +# Runs the checks in docs/VERIFICATION.md. Every push to main and every +# manual run (Actions, "Run workflow", which needs write access to the +# repository) is the full verification. A pull request runs every part except +# the proofs: the `crate` jobs, which take hours, are skipped, so anyone who +# can open a pull request can start only the cheap jobs, however many pull +# requests they open. A pull request that needs the full verification on its +# own commit (a tier raise, CLAUDE.md rule 7) gets it from a manual run on its +# branch. The full verification is split into parts (xtask/src/parts.rs) so +# that no job comes near GitHub's six-hour limit: # # crates `cargo xtask check`, the fast static checks (unsafe, lint # overrides, escape hatches, tier declarations, pins, allowlist), @@ -19,10 +25,14 @@ # mutations (several mutants at once, xtask/src/mutate.rs) and # conformance. One job per crate with proof work; the crates # with none share one job. Each uploads what it measured, one -# file per crate, tagged with the commit. -# assemble `verify --part assemble`: needs every job above to pass, then -# checks that every crate's measurements are present and from -# this commit, and reports whether README.md's table matches them. +# file per crate, tagged with the commit. Not on pull requests. +# assemble `verify --part assemble`, the job named `Full verification`: +# fails unless every job above passed, then checks that every +# crate's measurements are present and from this commit, and +# reports whether README.md's table matches them. On a pull +# request it is named `Pull request checks` instead and only +# requires the other jobs to have passed: no proof ran, so it +# never reports a full verification there. # table on pushes to main only, after `assemble` passed: writes # README.md's table from the same measurements # (`verify --part assemble --write`) and, if it changed, commits @@ -40,7 +50,8 @@ # # Together the parts run exactly the checks of one `scripts/verify.sh`, which # still runs them all on one machine. Verification has passed only when every -# job above is green; `assemble` cannot be, unless the others were. Every +# job above is green on a push to main or a manual run; `assemble` cannot be, +# unless the others were. Every # part exits non-zero when a tool is missing and checks were skipped, so a # skipped check is never green. # @@ -163,6 +174,8 @@ jobs: # A group of crates with no proofs is one job (`cargo xtask crates`). name: Verify ${{ contains(matrix.crate, ',') && 'crates without proofs' || matrix.crate }} needs: crates + # The proofs take hours; pull requests skip them (see the header). + if: github.event_name != 'pull_request' runs-on: ubuntu-24.04 timeout-minutes: 360 strategy: @@ -199,23 +212,53 @@ jobs: retention-days: 7 assemble: - name: Full verification + # A pull request runs no proofs, so its run is never named a full + # verification; a manual run on its branch is (see the header). + name: ${{ github.event_name == 'pull_request' && 'Pull request checks' || 'Full verification' }} needs: [crates, base, base-macos, miri, crate] + # Runs even when a job it needs failed or was skipped, and fails then: + # a skipped job is not a pass, and a skipped required check would count + # as one. Only a cancelled run is not judged. + if: ${{ !cancelled() }} runs-on: ubuntu-24.04 timeout-minutes: 30 steps: + - name: Every job passed + env: + NEEDS: ${{ toJSON(needs) }} + EVENT: ${{ github.event_name }} + run: | + # `crate` is skipped on pull requests, and only there. + bad=$(echo "$NEEDS" | jq -r --arg event "$EVENT" ' + to_entries[] + | select(.value.result != "success") + | select(.key != "crate" or $event != "pull_request" or .value.result != "skipped") + | "\(.key): \(.value.result)"') + if [ -n "$bad" ]; then + echo "Not every job passed:" + echo "$bad" + exit 1 + fi + - name: Pull request result + if: github.event_name == 'pull_request' + run: | + echo "RESULT: PULL REQUEST CHECKS PASSED (static checks, rustfmt, clippy, tests and Miri; no proofs ran: the full verification runs on main, or on this branch from Actions, Run workflow)" - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + if: github.event_name != 'pull_request' with: persist-credentials: false - name: Install Rust + if: github.event_name != 'pull_request' run: rustup toolchain install - name: Download measurements + if: github.event_name != 'pull_request' uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: pattern: part-* path: parts merge-multiple: true - name: Assemble + if: github.event_name != 'pull_request' run: cargo xtask verify --part assemble --metrics parts table: diff --git a/CLAUDE.md b/CLAUDE.md index 5aecfc27..33b23e71 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -53,8 +53,10 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. crate's `Cargo.toml` requires all of the following, and `cargo xtask check` rejects the claim otherwise: - every proof and harness passing in a full `cargo xtask verify`, which - for a tier change means CI's green run on the pull request (a local - `--changed` run does not count); + for a tier change means a green `Full verification` from a manual CI + run on the pull request's branch, at its head commit (pull request + runs skip the proofs, and a local `--changed` run does not count; a + manual run needs someone with write access, so ask for one); - Tier 1: Kani harnesses; - Tier 2: Verus enabled; every mutation in `mutations.json` a `killed` with a certificate that Verus checks; conformance tests @@ -85,9 +87,13 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. them; a change to anything shared (`Cargo.lock`, the workspace manifest, toolchain pins, `scripts/`, `xtask/`) makes it check every crate. It ends in `CHANGED CRATES PASSED`, which is not `ALL CHECKS PASSED` and must not - be reported as such. Work is **done** only when CI's full verification - (every job of `.github/workflows/ci.yml`, ending in `Full verification`) - is green on its pull request; say so if it has not run yet. To repeat CI's run locally, use `scripts/verify.sh` or the + be reported as such. A pull request's CI runs every job of + `.github/workflows/ci.yml` except the proofs, ending in `Pull request + checks`, which is not a full verification and must not be reported as + one. Work is **done** only when that is green on its pull request and, + after the merge, the `Full verification` of `main` is green (or a manual + run's on its branch, which a tier raise needs before merging); say so if + either has not run yet. To repeat CI's full run locally, use `scripts/verify.sh` or the Docker command in README.md. `cargo xtask check` runs only the fast static checks (unsafe, the `clazel-sys` audit, lint overrides, escape hatches, tier declarations, pins); use it while iterating, never as the final diff --git a/README.md b/README.md index f60caf7d..94a42e4d 100644 --- a/README.md +++ b/README.md @@ -160,7 +160,8 @@ and much of it is work only a person can do. `phase3/tls` branch until it passes CI. Contributions go through the same machine checks as everything else, whoever (or whatever) wrote them: read [CLAUDE.md](CLAUDE.md) first, and expect `cargo xtask verify --changed` and - CI's full verification to be the bar. + CI to be the bar (on a pull request every check but the proofs; on `main`, + and on manual runs, the full verification). ## License diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 83c12415..0a0ea495 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -83,8 +83,13 @@ installs nothing if a checksum differs. The full `cargo xtask verify` takes hours, so it runs where it is the gate: in CI (`.github/workflows/ci.yml`), on Linux x86-64 with the pinned -toolchain, on every push to `main` and every pull request. Nothing is done, -and no tier is raised, until that run is green. +toolchain, on every push to `main` and on every manual run (Actions, "Run +workflow", which needs write access to the repository). A pull request runs +every part except the proofs (the `crate` parts below), so that opening pull +requests, however many, never starts hours of proof jobs; its last job is +named `Pull request checks`, not `Full verification`. Nothing is done until +`main`'s full run after the merge is green, and no tier is raised until a +manual run on the pull request's branch is green at its head commit. CI splits the run into parts, one job each, so no job comes near GitHub's six-hour limit (`xtask/src/parts.rs`): @@ -102,11 +107,13 @@ six-hour limit (`xtask/src/parts.rs`): (`CLAZEL_MUTANT_JOBS`, default one per core up to 4). On success it writes what it measured to `/.json` for each crate, tagged with the commit (with `+dirty` if tracked files have uncommitted - changes). -- `verify --part assemble --metrics `, which runs only after every - other job passed: static checks, then it requires a file for every - workspace crate from this commit, and reports whether README.md's table - matches them. + changes). Not on pull requests. +- `verify --part assemble --metrics `, the `Full verification` job, + which fails unless every other job passed: static checks, then it + requires a file for every workspace crate from this commit, and reports + whether README.md's table matches them. On a pull request the job is + named `Pull request checks`, only requires the other jobs to have passed, + and ends in `RESULT: PULL REQUEST CHECKS PASSED`. - On pushes to `main` only, the `table` job runs the same part with `--write` after `assemble` passed, and commits README.md's regenerated table to `main` as github-actions[bot] if it changed. So the committed @@ -115,8 +122,9 @@ six-hour limit (`xtask/src/parts.rs`): The parts together run exactly the checks of one `cargo xtask verify`, which `scripts/verify.sh` and the Docker command in README.md still run on one -machine. "CI is green" means every job passed on the same commit, the -`Full verification` (assemble) job included. +machine. "CI is green" means every job passed on the same commit of a push +to `main` or a manual run, the `Full verification` (assemble) job included. +A pull request's green `Pull request checks` is not that. Locally, `cargo xtask verify --changed [base]` runs the same checks over less. `base` defaults to `origin/main`, the last commit CI verified, and @@ -150,7 +158,7 @@ files, the workspace crates it depends on, and the shared files listed above. Verus, Kani and the tests read nothing else, but a crate that read a file outside its directory (say, another crate's vendored data through `include_str!`) would not be re-checked when that file changed. CI's full -run catches it; the local run may not. +run (on `main`, or a manual run) catches it; the local run may not. ## Trusted computing base (what we do *not* prove) From ba3c4b0b1336bc257f32c4dcad483cd02198650d Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Wed, 28 Oct 2026 18:22:01 +0000 Subject: [PATCH 7/7] ci: pull requests run the proofs after a reviewer approves them Instead of skipping the proofs on pull requests, the `crate` jobs now need an `approval` job that uses the `full-verification` environment, whose required reviewers approve the run ("Review deployments"). Until then only the cheap jobs run and `Full verification` stays pending, so spam pull requests start no proof jobs, and an approved pull request gets the same full verification as main. Every push needs a new approval. The last job is named `Full verification` again in every run, and fails if a job it needs failed or was skipped (`approval` may be skipped outside pull requests only). The docs go back to main's wording, plus the approval. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 82 +++++++++++++++++++++++----------------- CLAUDE.md | 19 ++++------ README.md | 3 +- docs/VERIFICATION.md | 37 +++++++++--------- 4 files changed, 76 insertions(+), 65 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4fc9595e..b42bbebf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,18 +1,24 @@ -# Runs the checks in docs/VERIFICATION.md. Every push to main and every -# manual run (Actions, "Run workflow", which needs write access to the -# repository) is the full verification. A pull request runs every part except -# the proofs: the `crate` jobs, which take hours, are skipped, so anyone who -# can open a pull request can start only the cheap jobs, however many pull -# requests they open. A pull request that needs the full verification on its -# own commit (a tier raise, CLAUDE.md rule 7) gets it from a manual run on its -# branch. The full verification is split into parts (xtask/src/parts.rs) so -# that no job comes near GitHub's six-hour limit: +# Runs the checks in docs/VERIFICATION.md, in full, on every push to main, +# every manual run (Actions, "Run workflow", which needs write access to the +# repository) and every pull request. On a pull request the proofs (the +# `crate` jobs, which take hours) wait for a person to approve them: they +# need the `approval` job, which uses the `full-verification` environment, +# whose required reviewers are set in the repository's settings +# (Environments). Until one of them approves ("Review deployments" on the +# run), the proofs do not start and `Full verification` stays pending, so +# opening pull requests, however many, starts only the cheap jobs. Every push +# to a pull request starts a new run, which needs a new approval. The full +# verification is split into parts (xtask/src/parts.rs) so that no job comes +# near GitHub's six-hour limit: # # crates `cargo xtask check`, the fast static checks (unsafe, lint # overrides, escape hatches, tier declarations, pins, allowlist), # which fail in a minute or two so obvious mistakes show up early; # then the crate groups (`cargo xtask crates`) for the matrix # below, so a new crate cannot be left out. +# approval pull requests only, after `crates` passed: waits for a +# reviewer of the `full-verification` environment to approve +# the proof jobs, and does nothing else. It checks out no code. # base `verify --part base`: static checks, rustfmt, clippy and tests # over the whole workspace. # miri `verify --part miri`: the workspace's tests under Miri. @@ -25,14 +31,13 @@ # mutations (several mutants at once, xtask/src/mutate.rs) and # conformance. One job per crate with proof work; the crates # with none share one job. Each uploads what it measured, one -# file per crate, tagged with the commit. Not on pull requests. +# file per crate, tagged with the commit. On a pull request, +# only once `approval` passed. # assemble `verify --part assemble`, the job named `Full verification`: -# fails unless every job above passed, then checks that every -# crate's measurements are present and from this commit, and -# reports whether README.md's table matches them. On a pull -# request it is named `Pull request checks` instead and only -# requires the other jobs to have passed: no proof ran, so it -# never reports a full verification there. +# fails unless every job above passed (`approval` is skipped +# outside pull requests), then checks that every crate's +# measurements are present and from this commit, and reports +# whether README.md's table matches them. # table on pushes to main only, after `assemble` passed: writes # README.md's table from the same measurements # (`verify --part assemble --write`) and, if it changed, commits @@ -50,8 +55,7 @@ # # Together the parts run exactly the checks of one `scripts/verify.sh`, which # still runs them all on one machine. Verification has passed only when every -# job above is green on a push to main or a manual run; `assemble` cannot be, -# unless the others were. Every +# job above is green; `assemble` cannot be, unless the others were. Every # part exits non-zero when a tool is missing and checks were skipped, so a # skipped check is never green. # @@ -170,12 +174,30 @@ jobs: - name: Verify (Miri) run: cargo xtask verify --part miri + approval: + # The proofs take hours: on a pull request a reviewer of this + # environment approves them first (see the header). One job holds the + # approval, so one review starts every proof job of the run. + name: Approve the proofs + needs: crates + if: github.event_name == 'pull_request' + environment: full-verification + runs-on: ubuntu-24.04 + timeout-minutes: 5 + steps: + - name: Approved + run: echo "A reviewer approved the proof jobs for this run." + crate: # A group of crates with no proofs is one job (`cargo xtask crates`). name: Verify ${{ contains(matrix.crate, ',') && 'crates without proofs' || matrix.crate }} - needs: crates - # The proofs take hours; pull requests skip them (see the header). - if: github.event_name != 'pull_request' + needs: [crates, approval] + # After an approval on a pull request; `approval` is skipped, and not + # needed, everywhere else. + if: >- + ${{ !cancelled() && needs.crates.result == 'success' && + (needs.approval.result == 'success' || + (github.event_name != 'pull_request' && needs.approval.result == 'skipped')) }} runs-on: ubuntu-24.04 timeout-minutes: 360 strategy: @@ -212,10 +234,8 @@ jobs: retention-days: 7 assemble: - # A pull request runs no proofs, so its run is never named a full - # verification; a manual run on its branch is (see the header). - name: ${{ github.event_name == 'pull_request' && 'Pull request checks' || 'Full verification' }} - needs: [crates, base, base-macos, miri, crate] + name: Full verification + needs: [crates, approval, base, base-macos, miri, crate] # Runs even when a job it needs failed or was skipped, and fails then: # a skipped job is not a pass, and a skipped required check would count # as one. Only a cancelled run is not judged. @@ -228,37 +248,29 @@ jobs: NEEDS: ${{ toJSON(needs) }} EVENT: ${{ github.event_name }} run: | - # `crate` is skipped on pull requests, and only there. + # `approval` is skipped outside pull requests, and only there. bad=$(echo "$NEEDS" | jq -r --arg event "$EVENT" ' to_entries[] | select(.value.result != "success") - | select(.key != "crate" or $event != "pull_request" or .value.result != "skipped") + | select(.key != "approval" or $event == "pull_request" or .value.result != "skipped") | "\(.key): \(.value.result)"') if [ -n "$bad" ]; then echo "Not every job passed:" echo "$bad" exit 1 fi - - name: Pull request result - if: github.event_name == 'pull_request' - run: | - echo "RESULT: PULL REQUEST CHECKS PASSED (static checks, rustfmt, clippy, tests and Miri; no proofs ran: the full verification runs on main, or on this branch from Actions, Run workflow)" - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - if: github.event_name != 'pull_request' with: persist-credentials: false - name: Install Rust - if: github.event_name != 'pull_request' run: rustup toolchain install - name: Download measurements - if: github.event_name != 'pull_request' uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 with: pattern: part-* path: parts merge-multiple: true - name: Assemble - if: github.event_name != 'pull_request' run: cargo xtask verify --part assemble --metrics parts table: diff --git a/CLAUDE.md b/CLAUDE.md index 33b23e71..e95bb0c4 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -53,10 +53,8 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. crate's `Cargo.toml` requires all of the following, and `cargo xtask check` rejects the claim otherwise: - every proof and harness passing in a full `cargo xtask verify`, which - for a tier change means a green `Full verification` from a manual CI - run on the pull request's branch, at its head commit (pull request - runs skip the proofs, and a local `--changed` run does not count; a - manual run needs someone with write access, so ask for one); + for a tier change means CI's green run on the pull request (a local + `--changed` run does not count); - Tier 1: Kani harnesses; - Tier 2: Verus enabled; every mutation in `mutations.json` a `killed` with a certificate that Verus checks; conformance tests @@ -87,13 +85,12 @@ to trust the agents. Read `docs/VERIFICATION.md` and `docs/ROADMAP.md` first. them; a change to anything shared (`Cargo.lock`, the workspace manifest, toolchain pins, `scripts/`, `xtask/`) makes it check every crate. It ends in `CHANGED CRATES PASSED`, which is not `ALL CHECKS PASSED` and must not - be reported as such. A pull request's CI runs every job of - `.github/workflows/ci.yml` except the proofs, ending in `Pull request - checks`, which is not a full verification and must not be reported as - one. Work is **done** only when that is green on its pull request and, - after the merge, the `Full verification` of `main` is green (or a manual - run's on its branch, which a tier raise needs before merging); say so if - either has not run yet. To repeat CI's full run locally, use `scripts/verify.sh` or the + be reported as such. Work is **done** only when CI's full verification + (every job of `.github/workflows/ci.yml`, ending in `Full verification`) + is green on its pull request; say so if it has not run yet. On a pull + request the proof jobs wait until a reviewer of the `full-verification` + environment approves the run, and every push needs a new approval: ask + for one, and never report a run whose proofs are waiting as passed. To repeat CI's run locally, use `scripts/verify.sh` or the Docker command in README.md. `cargo xtask check` runs only the fast static checks (unsafe, the `clazel-sys` audit, lint overrides, escape hatches, tier declarations, pins); use it while iterating, never as the final diff --git a/README.md b/README.md index 94a42e4d..f60caf7d 100644 --- a/README.md +++ b/README.md @@ -160,8 +160,7 @@ and much of it is work only a person can do. `phase3/tls` branch until it passes CI. Contributions go through the same machine checks as everything else, whoever (or whatever) wrote them: read [CLAUDE.md](CLAUDE.md) first, and expect `cargo xtask verify --changed` and - CI to be the bar (on a pull request every check but the proofs; on `main`, - and on manual runs, the full verification). + CI's full verification to be the bar. ## License diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 0a0ea495..02f373d4 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -83,13 +83,17 @@ installs nothing if a checksum differs. The full `cargo xtask verify` takes hours, so it runs where it is the gate: in CI (`.github/workflows/ci.yml`), on Linux x86-64 with the pinned -toolchain, on every push to `main` and on every manual run (Actions, "Run -workflow", which needs write access to the repository). A pull request runs -every part except the proofs (the `crate` parts below), so that opening pull -requests, however many, never starts hours of proof jobs; its last job is -named `Pull request checks`, not `Full verification`. Nothing is done until -`main`'s full run after the merge is green, and no tier is raised until a -manual run on the pull request's branch is green at its head commit. +toolchain, on every push to `main`, every manual run (Actions, "Run +workflow") and every pull request. Nothing is done, and no tier is raised, +until that run is green. + +On a pull request the proofs (the `crate` parts below) wait for a person: +they need CI's `approval` job, which uses the `full-verification` +environment, and a reviewer set in that environment's settings approves it +("Review deployments" on the run). Until then only the cheap jobs run and +`Full verification` stays pending, so opening pull requests, however many, +never starts hours of proof jobs. Every push to a pull request starts a new +run, which needs a new approval. CI splits the run into parts, one job each, so no job comes near GitHub's six-hour limit (`xtask/src/parts.rs`): @@ -107,13 +111,13 @@ six-hour limit (`xtask/src/parts.rs`): (`CLAZEL_MUTANT_JOBS`, default one per core up to 4). On success it writes what it measured to `/.json` for each crate, tagged with the commit (with `+dirty` if tracked files have uncommitted - changes). Not on pull requests. + changes). - `verify --part assemble --metrics `, the `Full verification` job, - which fails unless every other job passed: static checks, then it - requires a file for every workspace crate from this commit, and reports - whether README.md's table matches them. On a pull request the job is - named `Pull request checks`, only requires the other jobs to have passed, - and ends in `RESULT: PULL REQUEST CHECKS PASSED`. + which fails unless every other job passed (a skipped job included, but + `approval`, which runs on pull requests only): static checks, then it + requires a file for every + workspace crate from this commit, and reports whether README.md's table + matches them. - On pushes to `main` only, the `table` job runs the same part with `--write` after `assemble` passed, and commits README.md's regenerated table to `main` as github-actions[bot] if it changed. So the committed @@ -122,9 +126,8 @@ six-hour limit (`xtask/src/parts.rs`): The parts together run exactly the checks of one `cargo xtask verify`, which `scripts/verify.sh` and the Docker command in README.md still run on one -machine. "CI is green" means every job passed on the same commit of a push -to `main` or a manual run, the `Full verification` (assemble) job included. -A pull request's green `Pull request checks` is not that. +machine. "CI is green" means every job passed on the same commit, the +`Full verification` (assemble) job included. Locally, `cargo xtask verify --changed [base]` runs the same checks over less. `base` defaults to `origin/main`, the last commit CI verified, and @@ -158,7 +161,7 @@ files, the workspace crates it depends on, and the shared files listed above. Verus, Kani and the tests read nothing else, but a crate that read a file outside its directory (say, another crate's vendored data through `include_str!`) would not be re-checked when that file changed. CI's full -run (on `main`, or a manual run) catches it; the local run may not. +run catches it; the local run may not. ## Trusted computing base (what we do *not* prove)