From 7b377f929f5022ba9cb1f90c33a4917f1d4056ca Mon Sep 17 00:00:00 2001 From: humuhumu33 <68450279+humuhumu33@users.noreply.github.com> Date: Fri, 16 Oct 2026 18:58:42 +0100 Subject: [PATCH 1/2] fix(#131): the join refuses a record of another executable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An imported elaboration or audit record must name the join's own digest of `lean`, and a replay record its digest of `leanchecker` (`partition::check_toolchain`, called as the join imports the parts' records); a mismatch is LLI9001, naming the record and both digests. In a whole verification this holds by construction; across the jobs of a run it held because every job installs the same pinned toolchain, which was a practice and not a check (the review of #152). VR-23 plants a replay record whose executable_sha256 is not the join's leanchecker and expects the refusal; the statement moves in SPEC.md §31, model/ids.toml, and the feature alike. SPEC.md §9.4 and §22.11 say what the join requires. Plant in VERIFICATION.md (the check removed, VR-23 fails at its refusal), CHANGELOG. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 7 +++ CONFORMANCE.md | 2 +- SPEC.md | 6 +-- VERIFICATION.md | 23 ++++++-- crates/conformance/src/cases/operational.rs | 35 +++++++++++++ crates/lexlean/src/verify/mod.rs | 8 +++ crates/lexlean/src/verify/partition.rs | 58 +++++++++++++++++++++ features/suites/verification.feature | 3 +- model/ids.toml | 2 +- 9 files changed, 135 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 23d894155..81dc0a160 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,13 @@ versions, and the entries below say what each tag does and does not claim. ## Unreleased +- The join of a verification run as parts refuses a record of another + executable (#131, the review of #152; SPEC.md §9.4, §22.11, `VR-23`; no new + diagnostic code, no new ID). An imported elaboration or audit record must + name the join's own digest of `lean`, and a replay record its digest of + `leanchecker`; a mismatch is `LLI9001`, naming the record and both digests. + Every CI job installs the same pinned toolchain, so this held by practice + and is now checked. - The runtime gates read what they claimed to (#154, follow-up to #144; no new diagnostic code, no new ID). `RT-04` finds a Lean runtime text in any string literal of the compiler's source outside unit-test items, in production code diff --git a/CONFORMANCE.md b/CONFORMANCE.md index ebd6819ec..1328c9216 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -549,7 +549,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | `VR-20` | `build` | The verifier process width is an operational resource profile selected only by the environment, defaulting to 1 and refusing any malformed value with LLV7017, and it enters no lock, identity, or verified artifact. | | `VR-21` | `build` | A multi-module project whose imports form nontrivial frontiers verifies at width 1 and at a larger width to byte-identical verified directories and the same attestation identity, observed axiom sets, and policy rows, and no completion order orders a record or changes which failure is reported. | | `VR-22` | `build` | Performance telemetry is written only to the CI evidence directory the environment names, a verification with telemetry on publishes byte-identical artifacts to one without, and telemetry planted in a verified artifact fails the gate. | -| `VR-23` | `build` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, or a join missing a record, is refused. | +| `VR-23` | `build` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, a join missing a record, or a join reading a record of an executable other than its own, is refused. | ## Cited authorities diff --git a/SPEC.md b/SPEC.md index ef60ba078..05dcab087 100644 --- a/SPEC.md +++ b/SPEC.md @@ -681,7 +681,7 @@ Its post-create command MUST install the pinned Lean toolchain explicitly and MU The job runs the recipes as two legs of one matrix, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas, and the other eleven recipes in the order of `vv`. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv` exactly once and every example once, and the gate passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. -UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and not while a pull request is a draft: they run when it is opened, pushed to, reopened, or marked ready. +UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, requires each to name the executable the join itself hashed for the tool that produced it (`lean` for an elaboration or an audit member, `leanchecker` for a replay), judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, a record whose `executable_sha256` is not the join's digest of its tool (`LLI9001`, naming the record and both digests), or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and not while a pull request is a draft: they run when it is opened, pushed to, reopened, or marked ready. Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other leg names no profile and runs at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of `just vv`; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. @@ -7568,7 +7568,7 @@ The profile changes how processes are scheduled and nothing else: For every project, the directory published at any profile equals, byte for byte, the directory published at width 1 without hints and without a budget, on the same host and toolchain; in particular the attestation ID, the observed axiom sets, the policy rows, the canonical compiler input, and every normalized verification record (§29.5) are identical. -A verification may also run as the parts of one run (§9.4): each part runs the processes of its plan at the profile of its own host, a part reads from another only the `.olean` files and process records that part's processes produced, and the join judges every record it reads as the stage that produced it judges its own. The directory the join publishes equals, byte for byte, the one the whole verification publishes, attestation ID included (`VR-23`); a part is defined for a project without production roots and without PDF rendering. +A verification may also run as the parts of one run (§9.4): each part runs the processes of its plan at the profile of its own host, a part reads from another only the `.olean` files and process records that part's processes produced, and the join judges every record it reads as the stage that produced it judges its own, after requiring it to name the join's own digest of the executable that stage runs. The directory the join publishes equals, byte for byte, the one the whole verification publishes, attestation ID included (`VR-23`); a part is defined for a project without production roots and without PDF rendering. ### 22.12 Performance telemetry @@ -9100,7 +9100,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `VR-20` | `verification` | The verifier process width is an operational resource profile selected only by the environment, defaulting to 1 and refusing any malformed value with LLV7017, and it enters no lock, identity, or verified artifact. | §22.11, §23.1 | | `VR-21` | `verification` | A multi-module project whose imports form nontrivial frontiers verifies at width 1 and at a larger width to byte-identical verified directories and the same attestation identity, observed axiom sets, and policy rows, and no completion order orders a record or changes which failure is reported. | §22.3, §22.4, §22.11 | | `VR-22` | `verification` | Performance telemetry is written only to the CI evidence directory the environment names, a verification with telemetry on publishes byte-identical artifacts to one without, and telemetry planted in a verified artifact fails the gate. | §22.12 | -| `VR-23` | `verification` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, or a join missing a record, is refused. | §9.4, §22.11 | +| `VR-23` | `verification` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, a join missing a record, or a join reading a record of an executable other than its own, is refused. | §9.4, §22.11 | | `CL-01` | `cli-api` | Global options and upward project discovery obey the exact CLI contract. | §23.1, §23.2 | | `CL-02` | `cli-api` | Init creates the complete canonical skeleton only in an absent or empty destination and never overwrites. | §23.4 | | `CL-03` | `cli-api` | Lock check, local update, and explicit network acquisition obey their exact mutually exclusive behavior. | §23.4 | diff --git a/VERIFICATION.md b/VERIFICATION.md index 84913c5ec..060d5aa9d 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -7721,14 +7721,23 @@ order, then replays in sorted name, then the family) from whichever part produced each record. A module without a record from any part, a record of a process no module owns, two parts that wrote the same `.olean` or record, and a shard whose plan elaborates a module before its imports (`module order did -not converge: … imports …`) are refused. A part is defined for a project -without production roots and without PDF rendering; Atlas is such a project. +not converge: … imports …`) are refused. Before it judges any imported +record, the join requires its `executable_sha256` to be the join's own digest +of the tool that produced it (`partition::check_toolchain`): `lean` for an +elaboration or an audit member, `leanchecker` for a replay, else `LLI9001` +naming the record and both digests. In a whole verification that holds by +construction; across the jobs of a run it held because every job installs the +same pinned toolchain, which was a practice and not a check (the maintainer's +review of #152). A part is defined for a project without production roots and +without PDF rendering; Atlas is such a project. `VR-23` verifies `peano-arithmetic` whole and as two shards and a join over its committed import graph (the first frontier; the second, replaying both; the rest), and requires the join's verified directory to equal the whole's byte for byte with the same attestation ID, then refuses the three plans -above. `RP-14` reads `ci.yml` against the plan: every shard run by exactly one +above and a join handed the second shard's replay record of a module with its +`executable_sha256` rewritten to zeros (`` the imported replay record of +`PeanoArithmetic.…` ``, with both digests). `RP-14` reads `ci.yml` against the plan: every shard run by exactly one job, each job waiting (through the job graph) for the jobs of the shards its shard needs and never for a row of its own matrix, the examples profile on every Atlas job, the one `cargo build` in the `prefix` job and every other job @@ -7769,6 +7778,14 @@ the same line), and the failure, after which the file was restored. - **a cache action in a shard job**: `` ci.yml has no `actions/cache` ``. - **the join reading another run's artifacts** (`run-id` on its download): `` §9.4: `atlas-join` reads the artifacts of this run only ``. +- **the join no longer checking the toolchain of what it imports** (the + `partition::check_toolchain` call removed from `verify::run_part`), then + `cargo test -p repo-conformance --all-features --test conformance -- --exact + conformance_vr_23`: the join accepted the replay record of another + `leanchecker` and published, and the case failed at its refusal, `a record + of another leanchecker: ()`. The unit test + `verify::partition::tests::a_part_output_round_trips_its_oleans_and_records` + holds the same refusal on the function itself. Two defects were found by the cases and not by review: a shard exported the `.olean` files it had imported along with its own, so the join refused the diff --git a/crates/conformance/src/cases/operational.rs b/crates/conformance/src/cases/operational.rs index ce3ca8a7e..5719b0f8a 100644 --- a/crates/conformance/src/cases/operational.rs +++ b/crates/conformance/src/cases/operational.rs @@ -905,4 +905,39 @@ fn parts_equal_the_whole() { text.contains("from any part of the run") && text.contains(&rest[0]), "{text}" ); + // A join refuses a record that another `leanchecker` ran: the second + // shard's replay record of a module names an executable that is not the + // join's, as a part on a different toolchain would have written it. + let replayed = &first[0]; + let record_path = dir("b") + .join("process") + .join("leanchecker") + .join(format!("{replayed}.json")); + let text = std::fs::read_to_string(record_path.as_std_path()).expect("the replay record"); + let recorded = serde_json::from_str::(&text).expect("the record parses") + ["executable_sha256"] + .as_str() + .expect("the record names its executable") + .to_owned(); + let planted = "0".repeat(recorded.len()); + assert_ne!(recorded, planted); + std::fs::write( + record_path.as_std_path(), + text.replacen(&recorded, &planted, 1), + ) + .expect("plant another executable"); + let error = run_part(VerifyPart::Join { + plan: plan(&rest, &rest), + parts: vec![dir("a"), dir("b")], + }) + .map(|_| ()) + .expect_err("a record of another leanchecker"); + support::expect_code(&error, "LLI9001"); + let text = error.to_string(); + assert!( + text.contains(&format!("replay record of `{replayed}`")) + && text.contains(&planted) + && text.contains(&recorded), + "{text}" + ); } diff --git a/crates/lexlean/src/verify/mod.rs b/crates/lexlean/src/verify/mod.rs index b85c11777..10ff0c653 100644 --- a/crates/lexlean/src/verify/mod.rs +++ b/crates/lexlean/src/verify/mod.rs @@ -1278,6 +1278,14 @@ pub fn run_part( stages.enter("part-import"); let mut imported = partition::import(part.inputs(), &olean_root, part.publishes()).map_err(fail)?; + // Every record another part wrote was run by the toolchain this run's + // preflight hashed: the attestation lists them under its digests. + partition::check_toolchain( + &imported, + toolchain.lean.sha256, + toolchain.leanchecker.sha256, + ) + .map_err(fail)?; // The leanchecker identity (module documentation), before any replay: // the preflight's toolchain-relative path and digest line, then the diff --git a/crates/lexlean/src/verify/partition.rs b/crates/lexlean/src/verify/partition.rs index cc55d8402..b50a1c205 100644 --- a/crates/lexlean/src/verify/partition.rs +++ b/crates/lexlean/src/verify/partition.rs @@ -22,6 +22,7 @@ use std::collections::{BTreeMap, BTreeSet}; use camino::{Utf8Path, Utf8PathBuf}; use crate::artifact::canonical_json::Json; +use crate::artifact::content_id::Sha256Digest; use crate::diagnostic::Diagnostic; use crate::verify::child::ChildRecord; @@ -221,6 +222,48 @@ pub fn import( Ok(imported) } +/// Require every imported record to name the executable the join itself +/// runs: `lean` for an elaboration or an audit member, `leanchecker` for a +/// replay (§9.4, §22.9). +/// +/// In a whole verification every record carries the digest of the toolchain +/// the run's preflight hashed, by construction. Across the parts of a run it +/// holds only because every job installs the same pinned toolchain, which is +/// a practice and not a check: a part whose `lean` or `leanchecker` differed +/// from the join's would otherwise contribute records the attestation then +/// lists under the join's toolchain digests. +/// +/// # Errors +/// +/// The first record, in the order elaborations, replays, audit members, and +/// by name within each, whose `executable_sha256` is not the join's digest of +/// the tool that produced it, naming the record and both digests. +pub fn check_toolchain( + imported: &Imported, + lean: Sha256Digest, + leanchecker: Sha256Digest, +) -> Result<(), Diagnostic> { + for (what, tool, expected, records) in [ + ("elaboration", "lean", lean, &imported.lean), + ("replay", "leanchecker", leanchecker, &imported.leanchecker), + ("audit", "lean", lean, &imported.audit), + ] { + for (name, record) in records { + if record.executable_sha256 != expected { + return Err(malformed( + &format!("the imported {what} record of `{name}`"), + format!( + "its executable_sha256 is {}, but the `{tool}` of this run's toolchain is {}; every part of a run must run the join's pinned toolchain", + record.executable_sha256.to_hex(), + expected.to_hex() + ), + )); + } + } + } + Ok(()) +} + /// Read every `` of `directory` as a process record keyed by /// ``. fn read_records( @@ -521,6 +564,21 @@ mod tests { assert!(imported.lean.contains_key("X.M")); assert!(imported.leanchecker.is_empty()); assert!(imported.audit.contains_key("LexLeanAudit.X.M")); + // The records name the join's `lean`; a join whose `lean` is another + // executable refuses them, naming the record and both digests. + let lean = crate::artifact::content_id::Sha256Digest::of(b"lean"); + let other = crate::artifact::content_id::Sha256Digest::of(b"another lean"); + check_toolchain(&imported, lean, other).expect("the records name the join's lean"); + let refused = check_toolchain(&imported, other, other) + .expect_err("a record of another lean is refused"); + let message = format!("{refused:?}"); + assert!( + message.contains("LLI9001") + && message.contains("elaboration record of `X.M`") + && message.contains(&lean.to_hex()) + && message.contains(&other.to_hex()), + "{message}" + ); // The same part imported twice is a process that ran twice. let again = import(&[output.clone(), output.clone()], &olean_root, false); assert!(again.is_err(), "a duplicate olean is refused"); diff --git a/features/suites/verification.feature b/features/suites/verification.feature index c8055b02a..0444b94c7 100644 --- a/features/suites/verification.feature +++ b/features/suites/verification.feature @@ -162,8 +162,9 @@ Feature: verification And a verified directory in which a telemetry key is planted is refused @VR-23 @build - Scenario: A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, or a join missing a record, is refused. + Scenario: A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, a join missing a record, or a join reading a record of an executable other than its own, is refused. Given a committed multi-module example project and a plan of two shards and a join over its import graph When it is verified whole and as the parts of one run Then the join publishes a verified directory byte-identical to the whole verification's, with the same attestation identity And a shard whose plan elaborates a module before its imports, and a join that is handed one shard too few, are refused + And a join reading a replay record whose executable digest is not its own leanchecker's is refused diff --git a/model/ids.toml b/model/ids.toml index d3fabb8f4..7ef804a79 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -1260,7 +1260,7 @@ statement = "Performance telemetry is written only to the CI evidence directory id = "VR-23" level = "build" suite = "verification" -statement = "A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, or a join missing a record, is refused." +statement = "A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, a join missing a record, or a join reading a record of an executable other than its own, is refused." [[id]] id = "CL-01" From cfa02f41183d7a7b411e4c01831c55d6be65e871 Mon Sep 17 00:00:00 2001 From: humuhumu33 <68450279+humuhumu33@users.noreply.github.com> Date: Fri, 16 Oct 2026 19:11:05 +0100 Subject: [PATCH 2/2] ci(#131): run the bdd recipe as the parts of one run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The rest leg took 111.5 minutes on the run that merged #152 (38905653756), 95.7 of them bdd: one test process whose cases sum to 22,708 s over four threads. .github/bdd-parts.json names four parts of the repo-conformance suite by conformance ID, grouped so the cases that share a fixture built once per test process (preservation's certified reports, verified_compiler, the production export, verified/broken_proof) run in one part, and a remainder, rest, that runs every test no part names. The recipe is `cargo xtask bdd`. With LEXLEAN_BDD_PART unset it runs `cargo test -p repo-conformance --all-features`, as just vv and release.yml do; with a part named it adds the part's harness filters (--exact and its tests, or --exact and a --skip of every named test). check-test-inventory lists every part with its filters and requires them disjoint with union bdd's list (RP-13, inventory::compare_parts); ci.yml runs each named part on a bdd- row of the gate matrix and the remainder on the rest leg, every part on exactly one row (RP-14). SPEC.md §9.2 (the bdd line), §9.4, and the RP-13 and RP-14 statements are reworded alike in §31, model/ids.toml, and the feature; CONFORMANCE.md regenerated. VERIFICATION.md: the measurement, the groups, the mechanism, and eight plants. CHANGELOG. No time target in normative text. Co-Authored-By: Claude Opus 5.5 --- .github/bdd-parts.json | 177 +++++++++++++ .github/workflows/ci.yml | 32 ++- CHANGELOG.md | 15 ++ CONFORMANCE.md | 4 +- Justfile | 8 +- SPEC.md | 14 +- VERIFICATION.md | 114 ++++++++- crates/conformance/src/bdd_parts.rs | 281 +++++++++++++++++++++ crates/conformance/src/cases/repository.rs | 161 ++++++++++-- crates/conformance/src/inventory.rs | 125 +++++++++ crates/conformance/src/lib.rs | 1 + features/suites/repository.feature | 11 +- model/ids.toml | 4 +- xtask/Cargo.toml | 2 +- xtask/src/ci.rs | 104 +++++++- xtask/src/main.rs | 6 +- 16 files changed, 1005 insertions(+), 54 deletions(-) create mode 100644 .github/bdd-parts.json create mode 100644 crates/conformance/src/bdd_parts.rs diff --git a/.github/bdd-parts.json b/.github/bdd-parts.json new file mode 100644 index 000000000..5fb223dd3 --- /dev/null +++ b/.github/bdd-parts.json @@ -0,0 +1,177 @@ +{ + "remainder": "rest", + "parts": { + "compiler": [ + "GC-02", + "GN-02", + "GN-03", + "GN-07", + "RS-01", + "RS-02", + "RS-03", + "RS-04", + "RS-05", + "RS-06", + "RS-07", + "RS-08", + "RS-09", + "RS-10", + "RS-11", + "RS-12", + "RS-13", + "RS-14", + "TC-03", + "TC-04", + "TC-05" + ], + "preservation": [ + "GC-09", + "SP-01", + "SP-02", + "SP-03", + "SP-04", + "SP-06", + "SP-07", + "SP-08", + "SP-09", + "SP-10", + "SP-11", + "SP-12", + "SP-13" + ], + "production": [ + "CL-01", + "CL-03", + "CL-04", + "CL-06", + "CL-07", + "CL-08", + "CL-09", + "CL-10", + "CL-11", + "CL-12", + "CL-17", + "CL-23", + "EX-07", + "MD-01", + "MD-02", + "MD-03", + "MD-04", + "MD-05", + "MD-06", + "MD-07", + "MD-08", + "MD-09", + "MD-10", + "MD-11", + "MD-12", + "PX-01", + "PX-02", + "PX-03", + "PX-04", + "PX-05", + "PX-06", + "PX-07", + "PX-08", + "PX-09", + "PX-10", + "PX-11", + "PX-12", + "PX-13", + "SP-05" + ], + "verification": [ + "AR-01", + "AR-02", + "AR-03", + "AR-04", + "AR-05", + "AR-06", + "AR-07", + "AR-08", + "AR-09", + "AR-10", + "AR-11", + "AR-12", + "AR-13", + "AR-14", + "AU-01", + "AU-02", + "AU-03", + "AU-04", + "AU-05", + "AU-06", + "AU-07", + "AU-08", + "AU-09", + "AU-10", + "AU-11", + "AU-12", + "EX-01", + "EX-02", + "GL-12", + "LN-01", + "LN-02", + "LN-03", + "LN-04", + "LN-05", + "LN-06", + "LN-07", + "LN-08", + "LN-09", + "LN-10", + "LN-11", + "LN-12", + "NE-01", + "NE-02", + "NE-03", + "NE-04", + "NE-05", + "NE-06", + "OR-01", + "OR-02", + "OR-03", + "OR-04", + "OR-05", + "OR-06", + "OR-07", + "OR-08", + "PF-18", + "SE-01", + "SE-02", + "SE-03", + "SE-04", + "SE-05", + "SE-06", + "SE-07", + "SE-08", + "SE-09", + "SE-10", + "SE-11", + "SE-12", + "VR-01", + "VR-02", + "VR-03", + "VR-04", + "VR-05", + "VR-06", + "VR-07", + "VR-08", + "VR-09", + "VR-10", + "VR-11", + "VR-12", + "VR-13", + "VR-14", + "VR-15", + "VR-16", + "VR-17", + "VR-18", + "VR-19", + "VR-20", + "VR-21", + "VR-22", + "VR-23" + ] + } +} diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f10d4ccdd..e29f6ed8a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,10 +4,20 @@ # `just vv` is the single gate, run from a clean checkout on Linux x86-64 with # the exact pinned toolchains and no build cache: §9.4 says "from a clean # checkout", and a restored target directory is not one. CI runs its twelve -# recipes as two legs at once, each its own clean checkout: `examples`, which -# here verifies every example but UOR Atlas, and the other eleven in the order -# of `vv`. Together they run every recipe of `vv` exactly once, so the gate is -# the same and the wall time is the longer leg rather than the sum. +# recipes as legs at once, each its own clean checkout: `examples`, which here +# verifies every example but UOR Atlas, and `rest`, the other eleven in the +# order of `vv`. Together they run every recipe of `vv` exactly once, so the +# gate is the same and the wall time is the longest leg rather than the sum. +# +# `bdd`, the conformance suite, was most of the `rest` leg's time, and it runs +# as the parts of `.github/bdd-parts.json` (§9.4): each `bdd-` row runs +# the recipe for the cases of one part, grouped so the cases that share a +# fixture (a verified project, an export, a compiled environment) run in one +# test process, and the `rest` leg runs the remainder, every test no other part +# names. The part is named by the row through `LEXLEAN_BDD_PART`, the harness +# selects its tests, and `inventory` proves from the harness's own lists that +# the parts are the whole suite with every test in one part (RP-13). Each row +# is its own clean checkout and build; nothing passes between rows or runs. # # UOR Atlas, whose native verification was most of the gate's time, is verified # as the parts of one run (§9.4): the shards of `.github/verify-shards.json`, @@ -70,13 +80,17 @@ env: jobs: vv: name: just vv (${{ matrix.part }}) - # A failing leg does not cancel the other: each leg's evidence is complete. + # A failing leg does not cancel the others: each leg's evidence is complete. strategy: fail-fast: false matrix: include: - - { part: examples, recipes: "examples", examples_part: "without:uor-atlas", width: "2", memory_kib: "12582912", hints: ".github/verify-hints.json" } - - { part: rest, recipes: "fmt-check model spec-links lint test features bdd inventory golden repro deny", examples_part: "", width: "", memory_kib: "", hints: "" } + - { part: examples, recipes: "examples", examples_part: "without:uor-atlas", bdd_part: "", width: "2", memory_kib: "12582912", hints: ".github/verify-hints.json" } + - { part: rest, recipes: "fmt-check model spec-links lint test features bdd inventory golden repro deny", examples_part: "", bdd_part: "rest", width: "", memory_kib: "", hints: "" } + - { part: bdd-compiler, recipes: "bdd", examples_part: "", bdd_part: "compiler", width: "", memory_kib: "", hints: "" } + - { part: bdd-preservation, recipes: "bdd", examples_part: "", bdd_part: "preservation", width: "", memory_kib: "", hints: "" } + - { part: bdd-production, recipes: "bdd", examples_part: "", bdd_part: "production", width: "", memory_kib: "", hints: "" } + - { part: bdd-verification, recipes: "bdd", examples_part: "", bdd_part: "verification", width: "", memory_kib: "", hints: "" } runs-on: ubuntu-24.04 # Complete proof coverage is intentionally the long pole. GitHub-hosted # jobs permit six hours; a shorter local-style timeout would turn complete @@ -90,6 +104,10 @@ jobs: # but the one the Atlas jobs below verify as parts; the other leg names # none, and runs no example. LEXLEAN_EXAMPLES_PART: ${{ matrix.examples_part }} + # The part of the `bdd` recipe this row runs (§9.4): a part of + # `.github/bdd-parts.json` on the `bdd-` rows, its remainder on the + # `rest` leg; the `examples` leg runs no `bdd` and names none. + LEXLEAN_BDD_PART: ${{ matrix.bdd_part }} # The leg's resource profile (§22.11), read from its matrix row; an empty # value is the default. Operational only, like the telemetry: no artifact # records it and no identity contains it. diff --git a/CHANGELOG.md b/CHANGELOG.md index 81dc0a160..20cf07a47 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,21 @@ versions, and the entries below say what each tag does and does not claim. ## Unreleased +- The `bdd` recipe runs in CI as the parts of one run (SPEC.md §9.2, §9.4, + `RP-13`, `RP-14`, #131; no new diagnostic code, no new ID). The `rest` leg + took 111.5 minutes on the run that merged #152 (CI run 38905653756), 95.7 of + them `bdd`, one test process whose cases sum to 22,708 s over four threads. + `.github/bdd-parts.json` names four parts of the `repo-conformance` suite by + conformance ID, grouped so the cases that share a fixture built once per test + process run in one part, and a remainder, `rest`, that runs every test no + part names. The recipe is `cargo xtask bdd`: unset, `LEXLEAN_BDD_PART` leaves + it `cargo test -p repo-conformance --all-features`, which `just vv` and + `release.yml` run; named, it adds the part's harness filters (`--exact` and + its tests, or `--exact` and a `--skip` of every named test). `cargo xtask + check-test-inventory` lists every part with its filters and requires the + parts to be disjoint and their union to be `bdd`'s list (`RP-13`); `ci.yml` + runs each named part on a `bdd-` row of the gate's matrix and the + remainder on the `rest` leg, every part on exactly one row (`RP-14`). - The join of a verification run as parts refuses a record of another executable (#131, the review of #152; SPEC.md §9.4, §22.11, `VR-23`; no new diagnostic code, no new ID). An imported elaboration or audit record must diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 1328c9216..8b7af7e33 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -428,8 +428,8 @@ the error registry does not sanction (R5, `ERRORS.md`). | `RP-10` | `build` | The embedded compiler-semantics ID equals a clean recomputation from normative language and schema inputs. | | `RP-11` | `build` | Every public README capability claim is tied to a registered model ID and honesty level. | | `RP-12` | `build` | A release is refused unless the complete release criterion and all required artifacts are satisfied. | -| `RP-13` | `build` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice. | -| `RP-14` | `build` | The normative CI job runs every recipe of just vv exactly once, in two parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other leg at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | +| `RP-13` | `build` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. | +| `RP-14` | `build` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | ## runtime diff --git a/Justfile b/Justfile index 9ab2fe314..73dba5bb4 100644 --- a/Justfile +++ b/Justfile @@ -44,11 +44,15 @@ features: # recipe, and `inventory` proves that between them nothing was lost or run # twice. The meta-gate target alone, which needs no Lean, is what the # honesty workflow runs (`cargo test -p repo-conformance --test bdd`). +# `cargo xtask bdd` runs `cargo test -p repo-conformance --all-features`; in +# CI, `LEXLEAN_BDD_PART` names the part of `.github/bdd-parts.json` a job runs +# (§9.4), and unset, as here, the recipe runs the whole suite. bdd: - cargo test -p repo-conformance --all-features + cargo xtask bdd # RP-13: `test` and `bdd` partition `cargo test --workspace --all-features`, -# test by test (listed with `-- --list`, not inferred from flags). +# and the parts of `.github/bdd-parts.json` partition `bdd`, test by test +# (listed with `-- --list`, not inferred from flags). inventory: cargo xtask check-test-inventory diff --git a/SPEC.md b/SPEC.md index 05dcab087..93b743264 100644 --- a/SPEC.md +++ b/SPEC.md @@ -651,7 +651,7 @@ spec-links cargo xtask validate-spec-links lint cargo clippy --workspace --all-targets --all-features -- -D warnings test cargo test --workspace --exclude repo-conformance --all-features features cargo check --workspace --all-features --all-targets -bdd cargo test -p repo-conformance --all-features +bdd cargo xtask bdd inventory cargo xtask check-test-inventory examples cargo xtask verify-examples golden cargo xtask check-golden @@ -660,7 +660,7 @@ deny cargo deny --all-features check vv all recipes above, in order ``` -`test` runs every test target of every workspace crate except `repo-conformance`, and `bdd` is the sole owner of the complete `repo-conformance` suite: its library tests and doctests, its `conformance` target (one test per registered ID, §27.8), and its `bdd` meta-gate target. The two phases partition the workspace test set: `inventory` lists the tests of `cargo test --workspace --all-features`, of `test`, and of `bdd` (RP-13), and requires the last two to be disjoint, their union to equal the first, and every test target of `repo-conformance` to be in `bdd`'s list, so that no test is lost and none runs twice in `vv`. The honesty workflow (§9.4) runs the meta-gate target alone, as a separate signal that is not part of `vv`. `just model-write` regenerates `CONFORMANCE.md` and `ERRORS.md`. Golden files are rewritten only by the explicit `just golden-write` recipe. No acceptance recipe rewrites source or expected output. +`test` runs every test target of every workspace crate except `repo-conformance`, and `bdd` is the sole owner of the complete `repo-conformance` suite: its library tests and doctests, its `conformance` target (one test per registered ID, §27.8), and its `bdd` meta-gate target. `cargo xtask bdd` runs `cargo test -p repo-conformance --all-features`, the whole suite; when `LEXLEAN_BDD_PART` names a part of `.github/bdd-parts.json`, it runs the same command with that part's harness filters, which is how CI runs it (§9.4). The two phases partition the workspace test set: `inventory` lists the tests of `cargo test --workspace --all-features`, of `test`, and of `bdd` (RP-13), and requires the last two to be disjoint, their union to equal the first, and every test target of `repo-conformance` to be in `bdd`'s list, so that no test is lost and none runs twice in `vv`. It also lists the tests of every part of the `bdd` plan with that part's harness filters, and requires the parts' lists to be disjoint, their union to equal `bdd`'s list, and every test a part names to be in that part's list, so that every test of `bdd` runs in exactly one part. The honesty workflow (§9.4) runs the meta-gate target alone, as a separate signal that is not part of `vv`. `just model-write` regenerates `CONFORMANCE.md` and `ERRORS.md`. Golden files are rewritten only by the explicit `just golden-write` recipe. No acceptance recipe rewrites source or expected output. ### 9.3 Development container @@ -679,11 +679,13 @@ Its post-create command MUST install the pinned Lean toolchain explicitly and MU `ci.yml` MUST run every recipe of `just vv` from a clean checkout on Linux x86-64. It MUST install the exact Rust toolchain, Lean 4.32.1 through `elan`, `just`, and `cargo-deny`. -The job runs the recipes as two legs of one matrix, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas, and the other eleven recipes in the order of `vv`. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv` exactly once and every example once, and the gate passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. +The job runs the recipes as legs of one matrix, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas; `rest`, the other eleven recipes in the order of `vv`; and one `bdd-` row for each named part of the `bdd` plan below, which runs `bdd` alone. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv`, every example, and every test of `bdd` exactly once, and the gate passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, requires each to name the executable the join itself hashed for the tool that produced it (`lean` for an elaboration or an audit member, `leanchecker` for a replay), judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, a record whose `executable_sha256` is not the join's digest of its tool (`LLI9001`, naming the record and both digests), or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and not while a pull request is a draft: they run when it is opened, pushed to, reopened, or marked ready. -Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other leg names no profile and runs at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of `just vv`; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. +The `bdd` recipe runs as the parts of one run as well. `.github/bdd-parts.json` names parts of the `repo-conformance` suite by conformance ID, and a remainder, `rest`, that names none; the cases that share a fixture built once per test process, such as a verified project, an exported package set, or a compiled environment, are named by one part, so that a fixture is built in one part and not once per part. `cargo xtask bdd` runs `cargo test -p repo-conformance --all-features` with the harness filters of the part `LEXLEAN_BDD_PART` names: `--exact` and the test of every ID the part names, or for the remainder `--exact` and a `--skip` of every test another part names, so that the remainder runs the library tests, the doctests, the meta-gate target, and every conformance test no other part names, an ID added to the register included. The part a job runs is named by its matrix row and by nothing else: a `bdd-` row names its part, the `rest` leg names the remainder, and the `examples` leg runs no `bdd` and names none; unset or empty, which is what `just vv` and `release.yml` run, the recipe runs the whole suite. The harness selects the tests, and no case decides whether it runs. `inventory` proves from the harness's own lists that the parts are disjoint and together are `bdd` (§9.2), and every part, the remainder included, is run by exactly one row. Each row builds from its own clean checkout; nothing passes between rows, and nothing crosses runs. + +Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other legs name no profile and run at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of `just vv`; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. `honesty.yml` MUST run the model/honesty gate separately so claim drift is distinguishable from code failure. @@ -8904,8 +8906,8 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `RP-10` | `repository` | The embedded compiler-semantics ID equals a clean recomputation from normative language and schema inputs. | §21.2 | | `RP-11` | `repository` | Every public README capability claim is tied to a registered model ID and honesty level. | §27 | | `RP-12` | `repository` | A release is refused unless the complete release criterion and all required artifacts are satisfied. | §30 | -| `RP-13` | `repository` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice. | §9.2 | -| `RP-14` | `repository` | The normative CI job runs every recipe of just vv exactly once, in two parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other leg at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | §9.4 | +| `RP-13` | `repository` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. | §9.2 | +| `RP-14` | `repository` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | §9.4 | | `CF-01` | `configuration-lock` | Project configuration accepts exactly the project/1 schema and rejects unknown or missing fields. | §10.1 | | `CF-02` | `configuration-lock` | Every operational limit is explicit, positive, parsed with checked arithmetic, and has no hidden default. | §10.2 | | `CF-03` | `configuration-lock` | Configured paths resolve within the project under the specified UTF-8 and nonsymlink rules. | §10.1, §25.1 | diff --git a/VERIFICATION.md b/VERIFICATION.md index 060d5aa9d..eeaa11466 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -14,8 +14,8 @@ How this repository's claims are checked, which recipe enforces which rule, and | `lint` | `cargo clippy --workspace --all-targets --all-features -- -D warnings` | no tolerated warnings | | `test` | `cargo test --workspace --exclude repo-conformance --all-features` | §28.1 classes 1–2 and 4–5 (unit, property, integration, CLI) of every crate but `repo-conformance`, and the model crate's own tests. `repo-conformance` is excluded, not skipped: `bdd` owns it (RP-13) | | `features` | `cargo check --workspace --all-features --all-targets` | every target compiles | -| `bdd` | `cargo test -p repo-conformance --all-features` | R3, §27.7, §27.8: the sole owner of the complete `repo-conformance` suite — its library tests, the `bdd` meta-gate target (register ↔ scenario ↔ test bijection and its own falsifiability test), and the `conformance` target with all 351 conformance tests, which include the §28.2 fixture suite (`conformance_ex_07`) and the crate-packaging round trip (`conformance_rp_12`) | -| `inventory` | `cargo xtask check-test-inventory` | RP-13: the tests listed by `test` and by `bdd` (`cargo test … -- --list`) are disjoint and their union is the list of `cargo test --workspace --all-features`: no test lost, none run twice | +| `bdd` | `cargo xtask bdd` | `cargo test -p repo-conformance --all-features`, or in CI the part of `.github/bdd-parts.json` that `LEXLEAN_BDD_PART` names (§9.4). R3, §27.7, §27.8: the sole owner of the complete `repo-conformance` suite — its library tests, the `bdd` meta-gate target (register ↔ scenario ↔ test bijection and its own falsifiability test), and the `conformance` target with all 351 conformance tests, which include the §28.2 fixture suite (`conformance_ex_07`) and the crate-packaging round trip (`conformance_rp_12`) | +| `inventory` | `cargo xtask check-test-inventory` | RP-13: the tests listed by `test` and by `bdd` (`cargo test … -- --list`) are disjoint and their union is the list of `cargo test --workspace --all-features`: no test lost, none run twice; the lists of the parts of `.github/bdd-parts.json`, each with its harness filters, are disjoint and their union is `bdd`'s list | | `examples` | `cargo xtask verify-examples` | §28.6, EX-01: every example directory and the `compiler` project (§17.14, §17.15) format, lock, check, build, and verify with real Lean 4.32.1; when an example commits `expected/verify/`, its normalized verification records must equal it (§29.5) | | `golden` | `cargo xtask check-golden` | R10, §28.3: the *published* build tree of a real `build` in a fresh directory equals the committed oracles byte for byte | | `repro` | `cargo xtask check-reproducibility` | AR-13, §28.4: two clean `build`s in distinct absolute directories publish byte-identical trees with no absolute path inside | @@ -8032,3 +8032,113 @@ prereleases, unrelated occurrences of the pin, and malformed banners. Validated after the fix: the unit case and `conformance_vr_02` pass (the latter in 4.76 s), as do formatting, workspace/all-target Clippy with warnings denied, model/spec-link audits, and all five BDD meta-gate tests. + +## The `bdd` recipe as the parts of one run (Issue #131) + +With UOR Atlas verified as the parts of one run, the `rest` leg became the +gate's longest. On the run that merged #152 (CI run 38905653756, head +`55583ba7`) it took 111.5 minutes, of which `bdd` took 5,741 s and the other +ten recipes 903 s. `bdd` is one `cargo test` process, and its harness runs four +test threads on the four-CPU runner. The cases' own wall times +(`cases-telemetry.jsonl`) sum to 22,708 s over those threads, so the threads +were busy for the whole recipe and its time is its work divided by four. + +The cases are not independent. A case that needs a verified project, an +exported package set, or a compiled environment reads it from a `OnceLock` +that the first case to ask builds, once per test process. Splitting such a +group across processes builds the fixture once per process. Which fixtures each +case reaches was read from the crate's code, following calls from each case's +arm of its suite's `run` to the functions holding a `OnceLock`, and checked by +hand for the heavy ones. The groups, with the case time of their members on +that run: + +| Group | Cases | Case seconds | +| --- | --- | ---: | +| preservation: `reports` (four projects certified side by side), `shipped`, the certification library | `SP-*` but `SP-05`, `GC-09` | 6,890 | +| `verified_compiler`, `verified_reasoning`, the planted calculus verification | `GC-02`, `GN-02/03/07`, `TC-03..05`, `RS-*` | 5,558 | +| the production export, `verified_models`, and `EX-07` | the `CL-*` cases of the export, `PX-*`, `MD-*`, `SP-05`, `EX-07` | 4,595 | +| `verified`, `broken_proof`, the oracle | `VR-*`, `AR-*`, `AU-*`, `LN-*`, `NE-*`, `OR-*`, `SE-*`, `EX-01/02`, `GL-12`, `PF-18` | 4,089 | +| everything else | 223 cases | 1,563 | + +These are the parts of `.github/bdd-parts.json`: `preservation`, `compiler`, +`production`, `verification`, and the remainder `rest`. Some fixtures are +still built in more than one part. The shipped preservation environment and the +certification environment are built in `preservation` and `compiler`, because +`GC-02` needs them beside `verified_compiler`, and moving it would verify the +`compiler` project twice instead. The GNAF requests and pairs, the committed +certificate fixtures, and the native certification registry are built in two +or three parts; the host computes them without Lean. +The SPEC text and `axioms_insufficient` are read or verified in two. The +estimate of each part, its case +seconds over four threads plus about seven minutes of checkout, toolchains, and +build, is 36 minutes for `preservation`, 30 for `compiler`, 36 for +`production` (bound by `EX-07`, 29 minutes alone), 24 for `verification`, and +22 for the `rest` leg (15 minutes of its other recipes and 7 of the +remainder). These are estimates; the measurement is the first green run of the +change. + +`cargo xtask bdd` is the recipe (`repo_conformance::bdd_parts`, SPEC.md §9.2, +§9.4). With `LEXLEAN_BDD_PART` unset or empty it runs `cargo test -p +repo-conformance --all-features`, the command the recipe always was. With a +part named, it adds that part's harness filters: `--exact` and the part's test +names, or for the remainder `--exact` and a `--skip` of every named test. On +this toolchain `--exact` makes `--skip` exact too: `--exact --skip +conformance_rp_1` still lists `conformance_rp_10` to `conformance_rp_14`, and +without `--exact` lists none of them. The remainder therefore runs the +library tests, the doctests, the meta-gate target, and every conformance test +no part names, an ID added later included. The harness selects the tests; no +case decides whether it runs. + +`cargo xtask check-test-inventory` proves the partition from the tests +themselves. It lists `bdd` whole and each part with its filters (`cargo test … +-- --list `) and requires the parts to be disjoint, their union to be +`bdd`'s list, and every test a part names to be in that part's list +(`inventory::compare_parts`). On this branch it reports the 425 tests of `bdd` +as the parts' 21, 13, 39, 91, and 261 (the remainder's 261 are 223 conformance +tests and the 38 tests of the library and meta-gate targets). `RP-14` reads +`ci.yml`: a row names a part exactly when it runs `bdd`, every part of the +plan, the remainder included, is run by exactly one row, a row that runs `bdd` +alone is named `bdd-`, `LEXLEAN_BDD_PART` is set once on the gate job and +from the row, and every other recipe of `vv` still runs exactly once. `RP-13` +holds the recipe line, the arguments the task and the inventory share +(`bdd_parts::CARGO_ARGUMENTS`), that every ID the plan names has its test, and +the comparison's refusals. + +What does not change: `just vv`, which runs `bdd` whole; `release.yml`; the +suite and every case in it; the host matrix, which runs the whole workspace on +every host. + +### the bdd partition can fail + +Each record is a defect planted on this branch, the command that ran, and its +failure, after which the file was restored. + +- **an ID named by two parts** (`SP-02` added to `compiler`), `cargo xtask + check-test-inventory`: `` .github/bdd-parts.json: `SP-02` is named by the + parts `compiler` and `preservation` ``. +- **an ID with no test** (`SP-99` added to `preservation`), the same command: + `` RP-13: the part `preservation` of .github/bdd-parts.json names `SP-99`, + and runs no test `conformance_sp_99` ``. +- **the remainder skipping nothing** (the `--skip` loop removed from + `Plan::harness_filters`), the same command: `` RP-13: `conformance_ar_01` of + tests/conformance.rs [conformance] is run by the parts `verification` and + `rest` of .github/bdd-parts.json ``. +- **a part run by no row** (the `bdd-verification` row removed from `ci.yml`), + `cargo test -p repo-conformance --all-features --test conformance -- --exact + conformance_rp_14`: `` §9.4: the part `verification` of bdd is run by no row + ``. +- **a part run by two rows** (the `bdd-compiler` row naming `production`), the + same command: `` §9.4: a row that runs bdd alone is named `bdd-production` ``. +- **the `rest` leg running `bdd` with no part** (its `bdd_part` emptied), the + same command: `§9.4: a row names a part of bdd exactly when it runs bdd`. +- **the part chosen outside the matrix row** (`LEXLEAN_BDD_PART: compiler` on + the gate job), the same command: `` §9.4: `LEXLEAN_BDD_PART` is read from the + matrix row ``. +- **the recipe back to the bare `cargo test`** (`bdd:` running `cargo test -p + repo-conformance --all-features` again), `cargo test -p repo-conformance + --all-features --test conformance -- --exact conformance_rp_13`: the + recipe-line assertion (`left: "cargo test -p repo-conformance + --all-features"`, `right: "cargo xtask bdd"`). `cargo xtask + check-test-inventory` refuses it as well: `` RP-13: the `bdd` recipe is + `cargo test -p repo-conformance --all-features`, not `cargo xtask bdd`, the + command whose arguments the inventory lists ``. diff --git a/crates/conformance/src/bdd_parts.rs b/crates/conformance/src/bdd_parts.rs new file mode 100644 index 000000000..35ed89d9e --- /dev/null +++ b/crates/conformance/src/bdd_parts.rs @@ -0,0 +1,281 @@ +//! The parts of the `bdd` recipe in one CI run (SPEC.md §9.2, §9.4): the +//! committed plan and the harness filters each part runs with. +//! +//! The plan is data, committed as `.github/bdd-parts.json`. It names parts of +//! the `repo-conformance` suite by conformance ID, so that the cases that +//! share a fixture (a verified project, an export, a compiled environment, all +//! built once per test process) run in one part and the fixture is not built +//! once per part. One part, the remainder, names no ID: it runs every test of +//! the suite no other part names, its library tests, doctests, and meta-gate +//! target included, so an ID added to the register runs there until the plan +//! moves it. +//! +//! `cargo xtask bdd` runs `cargo test` with [`CARGO_ARGUMENTS`] and, when +//! [`PART_VARIABLE`] names a part, that part's [`Plan::harness_filters`]: +//! `--exact` and the part's test names, or for the remainder `--exact` and a +//! `--skip` of every named test. The harness selects the tests; no case +//! decides whether it runs. That the parts are disjoint and together are the +//! whole suite is not argued from the filters but proved from the tests the +//! harness lists for each (`cargo xtask check-test-inventory`, RP-13). + +use std::collections::{BTreeMap, BTreeSet}; +use std::path::Path; + +/// The committed plan, repository-relative. +pub const PLAN_FILE: &str = ".github/bdd-parts.json"; + +/// The variable that names the part a job runs (§9.4). Unset or empty, the +/// recipe runs the whole suite. +pub const PART_VARIABLE: &str = "LEXLEAN_BDD_PART"; + +/// The arguments of the `cargo test` that is the whole `bdd` phase (§9.2): the +/// one command the recipe was before its parts, and still is when no part is +/// named. +pub const CARGO_ARGUMENTS: [&str; 3] = ["-p", "repo-conformance", "--all-features"]; + +/// The test of a conformance ID (§27.8): `RP-13` is `conformance_rp_13`. +#[must_use] +pub fn test_name(id: &str) -> String { + format!("conformance_{}", id.to_ascii_lowercase().replace('-', "_")) +} + +/// The plan: the named parts and the remainder. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Plan { + /// The name of the part that runs every test no other part names. + pub remainder: String, + /// The named parts: each the conformance IDs whose tests it runs. + pub parts: BTreeMap>, +} + +fn is_name(name: &str) -> bool { + !name.is_empty() + && name + .bytes() + .all(|byte| byte.is_ascii_lowercase() || byte.is_ascii_digit() || byte == b'-') +} + +fn is_id(id: &str) -> bool { + let bytes = id.as_bytes(); + bytes.len() == 5 + && bytes[..2].iter().all(u8::is_ascii_uppercase) + && bytes[2] == b'-' + && bytes[3..].iter().all(u8::is_ascii_digit) +} + +impl Plan { + /// Parse the plan file's text and check its shape. + /// + /// # Errors + /// + /// Text that is not the plan's shape, or a plan [`Self::check`] refuses. + pub fn parse(text: &str) -> Result { + let value: serde_json::Value = + serde_json::from_str(text).map_err(|error| format!("{PLAN_FILE}: {error}"))?; + let object = value + .as_object() + .ok_or_else(|| format!("{PLAN_FILE}: an object is required"))?; + if let Some(unknown) = object + .keys() + .find(|key| !["remainder", "parts"].contains(&key.as_str())) + { + return Err(format!( + "{PLAN_FILE}: `{unknown}` is not a field of the plan" + )); + } + let remainder = object + .get("remainder") + .and_then(serde_json::Value::as_str) + .ok_or_else(|| format!("{PLAN_FILE}: `remainder` is a required string"))? + .to_owned(); + let mut parts = BTreeMap::new(); + for (name, ids) in object + .get("parts") + .and_then(serde_json::Value::as_object) + .ok_or_else(|| format!("{PLAN_FILE}: `parts` is a required object"))? + { + let ids: Vec = ids + .as_array() + .ok_or_else(|| format!("{PLAN_FILE}: part `{name}` is an array of IDs"))? + .iter() + .map(|id| { + id.as_str() + .map(str::to_owned) + .ok_or_else(|| format!("{PLAN_FILE}: part `{name}` holds strings")) + }) + .collect::>()?; + parts.insert(name.clone(), ids); + } + let plan = Self { remainder, parts }; + plan.check()?; + Ok(plan) + } + + /// Read the committed plan of a repository. + /// + /// # Errors + /// + /// A plan file that cannot be read, parsed, or checked. + pub fn read(root: &Path) -> Result { + let path = root.join(PLAN_FILE); + let text = std::fs::read_to_string(&path) + .map_err(|error| format!("{}: {error}", path.display()))?; + Self::parse(&text) + } + + /// The plan's own rules: every part has a name of lowercase letters, + /// digits, and hyphens, the remainder is not also a named part, every + /// named part names at least one ID, every ID is of the register's form, + /// and no ID is named twice. Whether every ID has a test, and whether the + /// parts are the whole suite, is the inventory's proof (RP-13). + /// + /// # Errors + /// + /// The first rule broken, naming the part and the ID. + pub fn check(&self) -> Result<(), String> { + if !is_name(&self.remainder) { + return Err(format!( + "{PLAN_FILE}: the remainder `{}` is not a part name (lowercase letters, digits, hyphens)", + self.remainder + )); + } + if self.parts.contains_key(&self.remainder) { + return Err(format!( + "{PLAN_FILE}: `{}` is both the remainder and a named part", + self.remainder + )); + } + let mut owner: BTreeMap<&str, &str> = BTreeMap::new(); + for (name, ids) in &self.parts { + if !is_name(name) { + return Err(format!( + "{PLAN_FILE}: `{name}` is not a part name (lowercase letters, digits, hyphens)" + )); + } + if ids.is_empty() { + return Err(format!("{PLAN_FILE}: part `{name}` names no ID")); + } + for id in ids { + if !is_id(id) { + return Err(format!( + "{PLAN_FILE}: part `{name}` names `{id}`, which is not a conformance ID" + )); + } + if let Some(first) = owner.insert(id, name) { + return Err(format!( + "{PLAN_FILE}: `{id}` is named by the parts `{first}` and `{name}`" + )); + } + } + } + Ok(()) + } + + /// Every part's name, the remainder last. + #[must_use] + pub fn names(&self) -> Vec { + let mut names: Vec = self.parts.keys().cloned().collect(); + names.push(self.remainder.clone()); + names + } + + /// The test names the named parts run, in sorted order. + #[must_use] + pub fn named_tests(&self) -> BTreeSet { + self.parts + .values() + .flatten() + .map(|id| test_name(id)) + .collect() + } + + /// The harness arguments (after `--`) that select one part: `--exact` + /// and the part's test names, or for the remainder `--exact` and a + /// `--skip` of every test a named part runs. + /// + /// # Errors + /// + /// A part the plan does not have. + pub fn harness_filters(&self, part: &str) -> Result, String> { + let mut filters = vec!["--exact".to_owned()]; + if part == self.remainder { + for name in self.named_tests() { + filters.push("--skip".to_owned()); + filters.push(name); + } + } else { + let ids = self.parts.get(part).ok_or_else(|| { + format!( + "{PLAN_FILE} has no part `{part}`; its parts are {}", + self.names().join(", ") + ) + })?; + let mut names: Vec = ids.iter().map(|id| test_name(id)).collect(); + names.sort(); + filters.extend(names); + } + Ok(filters) + } +} + +#[cfg(test)] +mod tests { + use super::{test_name, Plan}; + + const PLAN: &str = r#"{ + "remainder": "rest", + "parts": { + "heavy": ["SP-02", "SP-03"], + "other": ["EX-07"] + } +}"#; + + #[test] + fn a_part_runs_its_tests_and_the_remainder_skips_every_named_one() { + let plan = Plan::parse(PLAN).expect("the plan parses"); + assert_eq!(test_name("RP-13"), "conformance_rp_13"); + assert_eq!(plan.names(), ["heavy", "other", "rest"]); + assert_eq!( + plan.harness_filters("heavy").expect("a part"), + ["--exact", "conformance_sp_02", "conformance_sp_03"] + ); + assert_eq!( + plan.harness_filters("rest").expect("the remainder"), + [ + "--exact", + "--skip", + "conformance_ex_07", + "--skip", + "conformance_sp_02", + "--skip", + "conformance_sp_03" + ] + ); + let unknown = plan.harness_filters("none").expect_err("no such part"); + assert!(unknown.contains("heavy, other, rest"), "{unknown}"); + } + + #[test] + fn every_defect_of_a_plan_is_named() { + for (text, expected) in [ + ( + PLAN.replace("\"EX-07\"", "\"SP-02\""), + "`SP-02` is named by the parts `heavy` and `other`", + ), + (PLAN.replace("\"EX-07\"", "\"EX7\""), "`EX7`, which is not"), + (PLAN.replace("\"EX-07\"", ""), "part `other` names no ID"), + ( + PLAN.replace("\"remainder\": \"rest\"", "\"remainder\": \"other\""), + "both the remainder and a named part", + ), + (PLAN.replace("\"other\"", "\"Other\""), "is not a part name"), + ( + PLAN.replace("\"parts\"", "\"shards\""), + "is not a field of the plan", + ), + ] { + let error = Plan::parse(&text).expect_err(expected); + assert!(error.contains(expected), "{expected}: {error}"); + } + } +} diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index 42288fe02..deab42f80 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -311,7 +311,7 @@ pub(crate) fn run(id: &str) { "features", "cargo check --workspace --all-features --all-targets", ), - ("bdd", "cargo test -p repo-conformance --all-features"), + ("bdd", "cargo xtask bdd"), ("inventory", "cargo xtask check-test-inventory"), ("examples", "cargo xtask verify-examples"), ("golden", "cargo xtask check-golden"), @@ -795,11 +795,13 @@ pub(crate) fn run(id: &str) { ); } // §9.2: the ordinary test phase excludes repo-conformance, `bdd` alone - // owns its complete suite, and the inventory proves the partition. The - // inventory itself lists tests with `cargo test -- --list`; it is a - // recipe of `vv`, one line of the log that runs once after both - // phases, and this case holds the rest: the recipe lines, the - // comparison it applies, and that the documents say what runs. + // owns its complete suite, and the inventory proves the partition, of + // the workspace into the two phases and of `bdd` into the parts of its + // committed plan (§9.4). The inventory itself lists tests with `cargo + // test -- --list`; it is a recipe of `vv`, one line of the log that + // runs once after both phases, and this case holds the rest: the + // recipe lines, the comparisons it applies, and that the documents say + // what runs. "RP-13" => { let justfile = root_file("Justfile"); let recipes = just_recipes(&justfile); @@ -815,12 +817,16 @@ pub(crate) fn run(id: &str) { test, "cargo test --workspace --exclude repo-conformance --all-features" ); - assert_eq!(bdd, "cargo test -p repo-conformance --all-features"); + assert_eq!(bdd, "cargo xtask bdd"); assert_eq!(inventory, "cargo xtask check-test-inventory"); + // The recipe runs one `cargo test`, the one the phase always was, + // whose arguments the task and the inventory read from one place. + let bdd_command = format!("cargo test {}", crate::bdd_parts::CARGO_ARGUMENTS.join(" ")); + assert_eq!(bdd_command, "cargo test -p repo-conformance --all-features"); let test_arguments = crate::inventory::recipe_arguments(&test).expect("test is cargo test"); let bdd_arguments = - crate::inventory::recipe_arguments(&bdd).expect("bdd is cargo test"); + crate::inventory::recipe_arguments(&bdd_command).expect("bdd is cargo test"); assert!( test_arguments .windows(2) @@ -896,12 +902,74 @@ pub(crate) fn run(id: &str) { .expect_err("tests lost"); assert!(lost.contains("neither phase"), "{lost}"); + // The parts of `bdd` (§9.4): the committed plan reads, every ID it + // names has its test, and the comparison the inventory applies to + // the parts' lists refuses a test two parts run and one no part + // runs. + let plan = crate::bdd_parts::Plan::read(support::repo_root().as_std_path()) + .expect("§9.4: the committed bdd plan reads"); + let tests = root_file("crates/conformance/tests/conformance.rs"); + for name in plan.named_tests() { + assert!( + tests.contains(&format!("fn {name}()")), + "§9.4: the bdd plan names `{name}`, which is no conformance test" + ); + } + let plants = crate::bdd_parts::Plan::parse( + r#"{ "remainder": "rest", "parts": { "first": ["RP-01"] } }"#, + ) + .expect("a plan"); + let first = list(&[( + "tests/conformance.rs", + "conformance-0123456789abcdef", + &["conformance_rp_01"][..], + )]); + let remainder = list(&[ + ( + "tests/conformance.rs", + "conformance-0123456789abcdef", + &["conformance_rp_02"][..], + ), + bdd_target, + ]); + let parts = |first: &crate::inventory::Parsed, rest: &crate::inventory::Parsed| { + vec![ + ("first".to_owned(), first.clone()), + ("rest".to_owned(), rest.clone()), + ] + }; + crate::inventory::compare_parts(&owned, &parts(&first, &remainder), &plants) + .expect("parts that partition bdd are accepted"); + let twice = crate::inventory::compare_parts(&owned, &parts(&first, &owned), &plants) + .expect_err("a test two parts run"); + assert!(twice.contains("parts `first` and `rest`"), "{twice}"); + let lost = crate::inventory::compare_parts( + &owned, + &parts(&first, &list(&[bdd_target])), + &plants, + ) + .expect_err("a test no part runs"); + assert!(lost.contains("run in no part"), "{lost}"); + // The task runs the part the variable names through the plan's + // filters, after the arguments of the whole phase, and the + // inventory lists with the same filters. + let task = root_file("xtask/src/ci.rs"); + assert!( + task.contains(".args(CARGO_ARGUMENTS)") + && task.contains("std::env::var(PART_VARIABLE)") + && task.contains("plan.harness_filters(part)") + && task.contains("plan.harness_filters(&name)") + && task.contains("inventory::compare_parts("), + "the bdd task and the inventory select a part through the plan's filters" + ); + // The documents say what runs. let xtask = root_file("xtask/src/main.rs"); assert!(xtask.contains("\"check-test-inventory\" =>")); + assert!(xtask.contains("\"bdd\" => ci::bdd(&root)")); let spec = root_file("SPEC.md"); let verification = root_file("VERIFICATION.md"); - for recipe_command in [&test, &bdd, &inventory] { + for recipe_command in [&test, &bdd, &bdd_command, &inventory] { assert!( verification.contains(&format!("`{recipe_command}`")), "VERIFICATION.md names the command `{recipe_command}`" @@ -989,6 +1057,10 @@ pub(crate) fn run(id: &str) { "LEXLEAN_EXAMPLES_PART", " LEXLEAN_EXAMPLES_PART: ${{ matrix.examples_part }}\n", ), + ( + crate::bdd_parts::PART_VARIABLE, + " LEXLEAN_BDD_PART: ${{ matrix.bdd_part }}\n", + ), ] { assert_eq!(vv.matches(variable).count(), 1, "§9.4: `{variable}` is set once on the gate job"); assert!(vv.contains(line), "§9.4: `{variable}` is read from the matrix row"); @@ -1010,8 +1082,9 @@ pub(crate) fn run(id: &str) { ); } // The gate is one matrix job whose legs run the recipes of `vv` - // (§9.4): every recipe exactly once, in the order of `vv` within a - // leg, each leg through the one gate command. + // (§9.4): every recipe exactly once, but `bdd`, which runs once per + // part of its committed plan, in the order of `vv` within a leg, + // each leg through the one gate command. let recipes_of_vv: Vec = just_recipes(&root_file("Justfile")) .get("vv") .expect("§9.2: the Justfile defines vv") @@ -1020,7 +1093,8 @@ pub(crate) fn run(id: &str) { .map(str::to_owned) .collect(); // A matrix row: `- { part: , recipes: "...", examples_part: - // "...", width: "...", memory_kib: "...", hints: "..." }`. + // "...", bdd_part: "...", width: "...", memory_kib: "...", hints: + // "..." }`. let field = |row: &str, name: &str| -> Option { let start = row.find(&format!(" {name}: \""))? + name.len() + 4; Some(row[start..start + row[start..].find('"')?].to_owned()) @@ -1086,7 +1160,53 @@ pub(crate) fn run(id: &str) { ); } } - let mut ran: Vec<&String> = legs.iter().flatten().collect(); + // `bdd` runs as the parts of its committed plan (§9.4): a row runs + // the recipe exactly when it names a part, every part of the plan, + // the remainder included, is named by exactly one row, and a row + // that runs `bdd` alone is named after its part. + let bdd_plan = crate::bdd_parts::Plan::read(support::repo_root().as_std_path()) + .expect("§9.4: the committed bdd plan reads"); + let mut bdd_rows: std::collections::BTreeMap = + std::collections::BTreeMap::new(); + for (row, leg) in rows.iter().zip(&legs) { + let part = field(row, "bdd_part") + .unwrap_or_else(|| panic!("§9.4: the row {row} names `bdd_part`")); + let runs_bdd = leg.iter().any(|recipe| recipe == "bdd"); + assert_eq!( + runs_bdd, + !part.is_empty(), + "§9.4: a row names a part of bdd exactly when it runs bdd: {row}" + ); + if !runs_bdd { + continue; + } + assert!( + bdd_plan.names().contains(&part), + "§9.4: the row {row} runs `{part}`, which is no part of {}", + crate::bdd_parts::PLAN_FILE + ); + if leg.len() == 1 { + assert!( + row.starts_with(&format!(" - {{ part: bdd-{part}, ")), + "§9.4: a row that runs bdd alone is named `bdd-{part}`: {row}" + ); + } + assert!( + bdd_rows.insert(part.clone(), (*row).to_owned()).is_none(), + "§9.4: the part `{part}` of bdd is run by two rows" + ); + } + for part in bdd_plan.names() { + assert!( + bdd_rows.contains_key(&part), + "§9.4: the part `{part}` of bdd is run by no row" + ); + } + let mut ran: Vec<&String> = legs + .iter() + .flatten() + .filter(|recipe| *recipe != "bdd") + .collect(); for leg in &legs { let positions: Vec = leg .iter() @@ -1102,11 +1222,22 @@ pub(crate) fn run(id: &str) { ); } ran.sort(); - let mut all: Vec<&String> = recipes_of_vv.iter().collect(); + let mut all: Vec<&String> = recipes_of_vv + .iter() + .filter(|recipe| *recipe != "bdd") + .collect(); all.sort(); assert_eq!( ran, all, - "§9.4: the legs run every recipe of vv exactly once" + "§9.4: the legs run every recipe of vv but bdd exactly once" + ); + assert_eq!( + legs.iter() + .flatten() + .filter(|recipe| *recipe == "bdd") + .count(), + bdd_plan.names().len(), + "§9.4: the legs run bdd once per part of its plan" ); assert_eq!( ci.matches( diff --git a/crates/conformance/src/inventory.rs b/crates/conformance/src/inventory.rs index 824ba5f43..ef6828508 100644 --- a/crates/conformance/src/inventory.rs +++ b/crates/conformance/src/inventory.rs @@ -9,6 +9,12 @@ //! lists below come from `cargo test -- --list` for the whole //! workspace and for each phase, and [`compare`] requires the phases' //! lists to be disjoint and their union to equal the whole. +//! +//! The `bdd` phase itself runs in CI as the parts of `.github/bdd-parts.json` +//! (§9.4), each selected by the harness's own filters; [`compare_parts`] +//! requires the parts' lists, made with those filters, to be disjoint and +//! their union to equal the `bdd` phase's list, so that every test of the +//! phase runs in exactly one part. use std::collections::{BTreeMap, BTreeSet}; @@ -227,6 +233,67 @@ pub fn compare( }) } +/// Require the parts of the `bdd` plan to partition the `bdd` phase (§9.4): +/// each part's listing, made with that part's harness filters, disjoint from +/// every other part's, their union the whole phase's listing, and every test a +/// named part names among the tests that part lists. +/// +/// `parts` holds each part's name and listing, in the plan's order. +/// +/// # Errors +/// +/// A test two parts run, a test of `bdd` no part runs, a test a part runs that +/// `bdd` does not list, or a named test its part does not list. +pub fn compare_parts( + owned: &Parsed, + parts: &[(String, Parsed)], + plan: &crate::bdd_parts::Plan, +) -> Result { + use crate::bdd_parts::PLAN_FILE; + let mut runner: BTreeMap<&Entry, &str> = BTreeMap::new(); + for (name, listed) in parts { + for entry in &listed.entries { + if let Some(first) = runner.insert(entry, name) { + return Err(format!( + "RP-13: `{}` of {} is run by the parts `{first}` and `{name}` of {PLAN_FILE}", + entry.name, entry.target + )); + } + } + } + let whole: BTreeSet<&Entry> = owned.entries.iter().collect(); + let union: BTreeSet<&Entry> = runner.keys().copied().collect(); + if let Some(lost) = whole.difference(&union).next() { + let count = whole.difference(&union).count(); + return Err(format!( + "RP-13: {count} test(s) of `bdd` run in no part of {PLAN_FILE}, e.g. `{}` of {}", + lost.name, lost.target + )); + } + if let Some(extra) = union.difference(&whole).next() { + return Err(format!( + "RP-13: the part `{}` of {PLAN_FILE} runs `{}` of {}, which `bdd` does not list", + runner[extra], extra.name, extra.target + )); + } + for (name, ids) in &plan.parts { + let listed: BTreeSet<&str> = parts + .iter() + .filter(|(part, _)| part == name) + .flat_map(|(_, listed)| listed.entries.iter().map(|entry| entry.name.as_str())) + .collect(); + for id in ids { + let test = crate::bdd_parts::test_name(id); + if !listed.contains(test.as_str()) { + return Err(format!( + "RP-13: the part `{name}` of {PLAN_FILE} names `{id}`, and runs no test `{test}`" + )); + } + } + } + Ok(parts.len()) +} + /// The arguments of a recipe line `cargo test `. /// /// # Errors @@ -381,6 +448,64 @@ conformance_rp_02: test assert!(compare(&empty, &empty, &empty, &crates()).is_err()); } + #[test] + fn the_parts_of_bdd_partition_it_and_every_defect_is_named() { + use super::compare_parts; + let plan = crate::bdd_parts::Plan::parse( + r#"{ "remainder": "rest", "parts": { "first": ["RP-01"] } }"#, + ) + .expect("a plan"); + let suite = parse(owned()).expect("parses"); + let first = parse( + " Running tests/conformance.rs (target/debug/deps/conformance-aec8e4616fa41234)\nconformance_rp_01: test\n", + ) + .expect("parses"); + let rest = parse(&owned().replace("conformance_rp_01: test\n", "")).expect("parses"); + let parts = |first: &super::Parsed, rest: &super::Parsed| { + vec![ + ("first".to_owned(), first.clone()), + ("rest".to_owned(), rest.clone()), + ] + }; + assert_eq!( + compare_parts(&suite, &parts(&first, &rest), &plan).expect("a partition"), + 2 + ); + // Twice: the remainder also runs the named test. + let error = compare_parts(&suite, &parts(&first, &suite), &plan).expect_err("twice"); + assert!( + error.contains("`conformance_rp_01`") && error.contains("parts `first` and `rest`"), + "{error}" + ); + // Lost: the remainder drops the meta-gate target's test. + let fewer = parse( + &owned() + .replace("bdd_one: test\n", "") + .replace("conformance_rp_01: test\n", ""), + ) + .expect("parses"); + let error = compare_parts(&suite, &parts(&first, &fewer), &plan).expect_err("lost"); + assert!( + error.contains("run in no part") && error.contains("bdd_one"), + "{error}" + ); + // Invented: a part runs a test `bdd` does not list. + let invented = parse(&format!( + "{}conformance_rp_99: test\n", + owned().replace("conformance_rp_01: test\n", "") + )) + .expect("parses"); + let error = compare_parts(&suite, &parts(&first, &invented), &plan).expect_err("invented"); + assert!(error.contains("which `bdd` does not list"), "{error}"); + // A named ID whose test the part does not run. + let missing = crate::bdd_parts::Plan::parse( + r#"{ "remainder": "rest", "parts": { "first": ["RP-01", "RP-77"] } }"#, + ) + .expect("a plan"); + let error = compare_parts(&suite, &parts(&first, &rest), &missing).expect_err("missing"); + assert!(error.contains("names `RP-77`"), "{error}"); + } + #[test] fn a_test_before_any_target_is_not_understood() { assert!(parse("orphan: test\n").is_err()); diff --git a/crates/conformance/src/lib.rs b/crates/conformance/src/lib.rs index 938e547a1..a59fe81d3 100644 --- a/crates/conformance/src/lib.rs +++ b/crates/conformance/src/lib.rs @@ -8,6 +8,7 @@ #![deny(missing_docs)] +pub mod bdd_parts; pub mod calculus; pub mod cases; pub mod certification; diff --git a/features/suites/repository.feature b/features/suites/repository.feature index 32e93ed99..170501ef0 100644 --- a/features/suites/repository.feature +++ b/features/suites/repository.feature @@ -88,18 +88,19 @@ Feature: repository And the Justfile release recipe depends on vv and runs `cargo xtask release-check` @RP-13 @build - Scenario: The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice. - Given the Justfile test and bdd recipes and the test list of cargo test --workspace --all-features + Scenario: The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. + Given the Justfile test and bdd recipes, .github/bdd-parts.json, and the test list of cargo test --workspace --all-features When the test lists of the test recipe and of the bdd recipe are taken Then the two lists are disjoint and their union equals the workspace list And no test of repo-conformance is in the test recipe's list and every conformance_ test is in the bdd recipe's list exactly once And a test recipe that includes repo-conformance, or a bdd recipe that runs fewer targets, fails the inventory + And the test lists of the parts of the bdd plan, each taken with the part's harness filters, are disjoint and their union equals the bdd recipe's list, so that a test two parts run or a test no part runs fails the inventory @RP-14 @build - Scenario: The normative CI job runs every recipe of just vv exactly once, in two parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other leg at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. - Given .github/workflows/ci.yml and .github/verify-shards.json + Scenario: The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. + Given .github/workflows/ci.yml, .github/verify-shards.json, and .github/bdd-parts.json When the runner, the environment, the job steps, and the plan are read Then every gate job runs on ubuntu-24.04 with the 360-minute limit, and each verification profile variable is set once per job, from the leg's matrix row or as the examples profile on an Atlas job - And the leg that runs examples names width 2, a 12 GiB budget, and the committed hints, which the verifier parses, verifies every example but uor-atlas, and the other leg names no profile and no part, and the two legs run the recipes of vv, each exactly once, in the order of vv within a leg, through the one gate command + And the leg that runs examples names width 2, a 12 GiB budget, and the committed hints, which the verifier parses, verifies every example but uor-atlas, and every other leg names no profile and no example part, and the legs run the recipes of vv, each exactly once but bdd, which runs once per part of the bdd plan on the one row that names the part, in the order of vv within a leg, through the one gate command And the Atlas jobs run every shard of the plan exactly once, each after the jobs of the shards it needs, from the one executable the prefix job built, the join asserts that Atlas verified, and the plan elaborates and replays every Atlas module exactly once with every import elaborated by the shard or by one it needs And the vv job has no path filter, no cache action, and no condition on a recipe, the Atlas jobs wait only for a pull request to leave draft, and each job uploads its ci-evidence under a name of its own diff --git a/model/ids.toml b/model/ids.toml index 7ef804a79..9a8e49fa2 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -84,13 +84,13 @@ statement = "A release is refused unless the complete release criterion and all id = "RP-13" level = "build" suite = "repository" -statement = "The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice." +statement = "The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part." [[id]] id = "RP-14" level = "build" suite = "repository" -statement = "The normative CI job runs every recipe of just vv exactly once, in two parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other leg at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence." +statement = "The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence." [[id]] id = "CF-01" diff --git a/xtask/Cargo.toml b/xtask/Cargo.toml index 9ae0de1ac..f6090f378 100644 --- a/xtask/Cargo.toml +++ b/xtask/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "xtask" -description = "Repository gates: validate-model, validate-spec-links, verify-examples, check-golden, check-reproducibility, check-fixtures, check-calculus, check-production-export, check-package, check-test-inventory, ci-summary, ci-hints, ci-shards, release-artifacts, release-check, validate." +description = "Repository gates: validate-model, validate-spec-links, verify-examples, check-golden, check-reproducibility, check-fixtures, check-calculus, check-production-export, check-package, check-test-inventory, bdd, ci-summary, ci-hints, ci-shards, release-artifacts, release-check, validate." version.workspace = true edition.workspace = true rust-version.workspace = true diff --git a/xtask/src/ci.rs b/xtask/src/ci.rs index 5b64e4778..97c3c5c8d 100644 --- a/xtask/src/ci.rs +++ b/xtask/src/ci.rs @@ -35,11 +35,17 @@ fn recipe_command(justfile: &str, name: &str) -> Result { Err(format!("RP-13: the Justfile has no recipe `{name}` with a command").into()) } -/// Run `cargo test -- --list` and return what it wrote, stdout -/// and stderr in the order they were written: `cargo` announces each target on -/// stderr and the harness lists its tests on stdout, so the two have to share -/// one file to be read together. -fn list_tests(root: &Path, arguments: &[String]) -> Result { +/// Run `cargo test -- --list ` and return what it +/// wrote, stdout and stderr in the order they were written: `cargo` announces +/// each target on stderr and the harness lists its tests on stdout, so the two +/// have to share one file to be read together. `harness` holds the filters of +/// a part of `bdd` (§9.4), which select the tests listed as they select the +/// tests run. +fn list_tests( + root: &Path, + arguments: &[String], + harness: &[String], +) -> Result { let cargo = std::env::var_os("CARGO").unwrap_or_else(|| "cargo".into()); let mut file = tempfile::tempfile()?; let status = Command::new(cargo) @@ -48,6 +54,7 @@ fn list_tests(root: &Path, arguments: &[String]) -> Result Result = output.lines().rev().take(20).collect(); return Err(format!( - "RP-13: `cargo test {} -- --list` failed:\n{}", + "RP-13: `cargo test {} -- --list{}` failed:\n{}", arguments.join(" "), + if harness.is_empty() { + String::new() + } else { + format!(" {}", harness.join(" ")) + }, tail.into_iter().rev().collect::>().join("\n") ) .into()); @@ -67,6 +79,54 @@ fn list_tests(root: &Path, arguments: &[String]) -> Result Result<(), Fail> { + use repo_conformance::bdd_parts::{Plan, CARGO_ARGUMENTS, PART_VARIABLE, PLAN_FILE}; + let part = std::env::var(PART_VARIABLE) + .ok() + .filter(|value| !value.is_empty()); + let mut harness: Vec = Vec::new(); + if let Some(part) = &part { + let plan = Plan::read(root)?; + harness.push("--".to_owned()); + harness.extend(plan.harness_filters(part)?); + let what = if *part == plan.remainder { + format!( + "every test but the {} the other parts name", + plan.named_tests().len() + ) + } else { + format!("{} conformance cases", plan.parts[part].len()) + }; + println!("bdd: the part `{part}` of {PLAN_FILE}: {what} (§9.4)"); + } + let cargo = std::env::var_os("CARGO").unwrap_or_else(|| "cargo".into()); + let status = Command::new(cargo) + .current_dir(root) + .arg("test") + .args(CARGO_ARGUMENTS) + .args(&harness) + .stdin(Stdio::null()) + .status()?; + if !status.success() { + return Err(format!( + "bdd: `cargo test {}`{} failed", + CARGO_ARGUMENTS.join(" "), + part.map(|part| format!(" (the part `{part}`)")) + .unwrap_or_default() + ) + .into()); + } + Ok(()) +} + /// The names of the binaries that carry the tests of `repo-conformance`: /// its library and each of its test targets, from `cargo metadata`. fn owned_crates(root: &Path) -> Result, Fail> { @@ -104,24 +164,46 @@ fn owned_crates(root: &Path) -> Result, Fail> { Ok(crates) } -/// RP-13: `test` and `bdd` partition `cargo test --workspace --all-features`. +/// RP-13: `test` and `bdd` partition `cargo test --workspace --all-features`, +/// and the parts of `.github/bdd-parts.json` partition `bdd`. pub fn check_test_inventory(root: &Path) -> Result<(), Fail> { + use repo_conformance::bdd_parts::{Plan, CARGO_ARGUMENTS, PLAN_FILE}; let justfile = std::fs::read_to_string(root.join("Justfile"))?; let ordinary_line = recipe_command(&justfile, "test")?; let owned_line = recipe_command(&justfile, "bdd")?; + if owned_line != "cargo xtask bdd" { + return Err(format!( + "RP-13: the `bdd` recipe is `{owned_line}`, not `cargo xtask bdd`, the command whose arguments the inventory lists" + ) + .into()); + } let reference: Vec = inventory::REFERENCE .iter() .map(|s| (*s).to_owned()) .collect(); - let workspace = list_tests(root, &reference)?; - let ordinary = list_tests(root, &inventory::recipe_arguments(&ordinary_line)?)?; - let owned = list_tests(root, &inventory::recipe_arguments(&owned_line)?)?; + let owned_arguments: Vec = CARGO_ARGUMENTS.iter().map(|s| (*s).to_owned()).collect(); + let workspace = list_tests(root, &reference, &[])?; + let ordinary = list_tests(root, &inventory::recipe_arguments(&ordinary_line)?, &[])?; + let owned = list_tests(root, &owned_arguments, &[])?; let summary = inventory::compare(&workspace, &ordinary, &owned, &owned_crates(root)?)?; + let plan = Plan::read(root)?; + let mut parts = Vec::new(); + for name in plan.names() { + let listed = list_tests(root, &owned_arguments, &plan.harness_filters(&name)?)?; + parts.push((name, listed)); + } + let count = inventory::compare_parts(&owned, &parts, &plan)?; println!( - "check-test-inventory: the {} tests of `cargo test {}` are the {} of `test` and the {} of `bdd`, disjoint, none lost (RP-13)", + "check-test-inventory: the {} tests of `cargo test {}` are the {} of `test` and the {} of `bdd`, disjoint, none lost; the {count} parts of {PLAN_FILE} ({}) are the {} of `bdd`, each in one part (RP-13)", summary.workspace, inventory::REFERENCE.join(" "), summary.ordinary, + summary.owned, + parts + .iter() + .map(|(name, listed)| format!("{name} {}", listed.entries.len())) + .collect::>() + .join(", "), summary.owned ); Ok(()) diff --git a/xtask/src/main.rs b/xtask/src/main.rs index 01af57ad5..0789e7314 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -37,6 +37,7 @@ fn main() -> ExitCode { "check-production-export" => check_production_export(write), "check-package" => check_package(&root), "check-test-inventory" => ci::check_test_inventory(&root), + "bdd" => ci::bdd(&root), "ci-summary" => ci::ci_summary(&root, &std::env::args().skip(2).collect::>()), "ci-hints" => ci::ci_hints(&std::env::args().skip(2).collect::>()), "ci-shards" => ci::ci_shards(&root), @@ -60,7 +61,10 @@ fn main() -> ExitCode { check-production-export §24.7: the consumer's exported packages equal the committed\n\ packages under tests/production-export\n\ check-package §30.3, RP-12: package lexlean crate, verify offline build & identity\n\ - check-test-inventory RP-13: the `test` and `bdd` recipes partition the workspace tests\n\ + check-test-inventory RP-13: the `test` and `bdd` recipes partition the workspace tests,\n\ + and the parts of .github/bdd-parts.json partition `bdd`\n\ + bdd §9.2: the repo-conformance suite, or the part LEXLEAN_BDD_PART\n\ + names (§9.4)\n\ ci-summary §9.4: summarize ci-evidence/ (recipe, stage, module times; memory)\n\ ci-hints §22.11: scheduling hints from a verifier telemetry file\n\ (--from verify-telemetry.jsonl --out hints.json)\n\