From fcf6de2e8d46b1b8b36801708452b1f0c26e224d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 13:32:09 +0100 Subject: [PATCH 1/4] [0.4] #260 RP-18: the lexlean crate that goes to crates.io is the crate the release attaches (skeleton) R3 order: the register row, its SPEC.md section 31 entry and the section 30.3 paragraph, the scenario, and the named test conformance_rp_18 with its case. The test fails here: the workflows and the script it reads are not written yet. The register is 449 IDs. RP-17 is #288, on release/v0.5, so this row takes RP-18 and the forward merge needs no renumbering. Part of #260. Co-Authored-By: Claude Sonnet 5.5 --- CONFORMANCE.md | 1 + SPEC.md | 5 +- crates/conformance/src/cases/repository.rs | 494 ++++++++++++++++++++- crates/conformance/tests/conformance.rs | 5 + features/suites/repository.feature | 8 + model/ids.toml | 6 + 6 files changed, 517 insertions(+), 2 deletions(-) diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 0826270f36..8f182f83de 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -487,6 +487,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | `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; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main or to a release line run every job, and a push to main or to a release line that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing. | | `RP-15` | `build` | Every match over a closed semantic enum (the IR, the production realization calculus, and its Rust AST) that names at least five of the enum's variants names all of them, with no wildcard or binding catch-all arm, so that a variant added to the enum is a compile error in each Lean, LaTeX, validation, charge, and calculus consumer and never a silent fallback; the audit rejects a catch-all planted in each consumer group and fails when a consumer it must read has no such match left. | | `RP-16` | `build` | The development container installs, at image build, exactly the Rust toolchain that rust-toolchain.toml pins and exactly the Lean toolchain that lean-toolchain pins and selects no other default, so that nothing is fetched when a session starts, and a Dockerfile that names another version of either, installs a second toolchain, or selects an unpinned default is refused. | +| `RP-18` | `build` | The release workflow packages the lexlean crate twice to the same bytes, runs cargo publish --dry-run, and refuses a crate whose SHA-256 differs from the one release/checksums.txt lists for it or from the bytes cargo would upload, or whose archive lacks the metadata and size crates.io requires, and uploads to crates.io only when a CARGO_REGISTRY_TOKEN secret or trusted publishing authorises it; a commit of a release line release/vX.Y is published as the pre-release X.Y.0-dev.N, N being its number of first-parent commits, and a plant in each of these checks is refused. | ## runtime diff --git a/SPEC.md b/SPEC.md index 7c2115c3fa..cab4dfcdfa 100644 --- a/SPEC.md +++ b/SPEC.md @@ -10268,6 +10268,8 @@ compiler-semantics lean-toolchain leanprover/lean4:v4.32.1 ``` +The crate package MUST be the crate `cargo publish` would upload: the release workflow packages the crate twice to the same bytes, runs `cargo publish --dry-run`, and refuses a package whose SHA-256 differs from the one `checksums.txt` lists for the crate, from the dry-run package, or from what crates.io requires of an archive (a description, a license, a repository, the readme it names, and at most 10 MiB). It uploads to crates.io only when a `CARGO_REGISTRY_TOKEN` secret or trusted publishing authorises it, and otherwise creates the release without the upload and says so. A commit of a release line `release/vX.Y` is published as the pre-release `X.Y.0-dev.N`, `N` being the number of first-parent commits of the line at that commit, so that a release `X.Y.0` supersedes every one of them; `RP-18` reads the workflows and runs the script that decides each of these. + ### 30.4 Completion criterion The project is complete for LexLean 1.0 only when: @@ -10324,6 +10326,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `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; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main or to a release line run every job, and a push to main or to a release line that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing. | §9.4 | | `RP-15` | `repository` | Every match over a closed semantic enum (the IR, the production realization calculus, and its Rust AST) that names at least five of the enum's variants names all of them, with no wildcard or binding catch-all arm, so that a variant added to the enum is a compile error in each Lean, LaTeX, validation, charge, and calculus consumer and never a silent fallback; the audit rejects a catch-all planted in each consumer group and fails when a consumer it must read has no such match left. | §27.2 | | `RP-16` | `repository` | The development container installs, at image build, exactly the Rust toolchain that rust-toolchain.toml pins and exactly the Lean toolchain that lean-toolchain pins and selects no other default, so that nothing is fetched when a session starts, and a Dockerfile that names another version of either, installs a second toolchain, or selects an unpinned default is refused. | §9.3 | +| `RP-18` | `repository` | The release workflow packages the lexlean crate twice to the same bytes, runs cargo publish --dry-run, and refuses a crate whose SHA-256 differs from the one release/checksums.txt lists for it or from the bytes cargo would upload, or whose archive lacks the metadata and size crates.io requires, and uploads to crates.io only when a CARGO_REGISTRY_TOKEN secret or trusted publishing authorises it; a commit of a release line release/vX.Y is published as the pre-release X.Y.0-dev.N, N being its number of first-parent commits, and a plant in each of these checks is refused. | §30.3 | | `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 | @@ -10758,7 +10761,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `LM-09` | `language-models` | No prompt is code: no member of the closed language maps `string` or `bytes` to a function, a term, or source — every operation of the primitive registry that takes a `string` or `bytes` operand is classified by the audit with a data result, the registry's schema enumeration and the production registry's primitive rows equal one another and equal that classified set, and the text declarations of `lexlean/semantic-module/2` state no `string`-typed member, so a prompt reaches a model only as the tokens `encodeText` makes of it; a planted operation or text member of that shape is caught by the audit with its name. | §17.12 | | `LM-13` | `language-models` | The text laws a tokenizer elaborates through are LexLean source and not authored text: the module that states them is one language-1.2 native core module of the embedded `language/text-1.2` project, the project holds no file of Lean source, no independently authored Lean file anywhere in the release tree declares the `LexLeanText` namespace or lies under its module root, and the one-time migration input is absent; the registry lists only that module, the declarations and their exact axiom policies are read from its native data, which the compiler embeds and hashes into the language-1.2 semantics, and a module that declares a text component imports the generated module rather than splicing any Lean text. | §17.10, §17.12 | -**Total required capability IDs:** 448. +**Total required capability IDs:** 449. No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors. diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index 2136763797..a4e2fb26c5 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -1,4 +1,4 @@ -//! The `repository` suite: RP-01..RP-16. +//! The `repository` suite: RP-01..RP-16 and RP-18. use std::collections::BTreeSet; @@ -2021,6 +2021,9 @@ pub(crate) fn run(id: &str) { ); } } + // §30.3: the crate that goes to crates.io is the crate the release + // attaches, proved on every run, and uploaded only with a credential. + "RP-18" => rp_18(), other => panic!("no repository case is wired for {other}"), } } @@ -2158,3 +2161,492 @@ fn rp_15() { .contains(path)); } } + +/// The body of the job `name` of a workflow: the lines after its key at two +/// spaces of indentation, up to the next line at that indentation. +fn workflow_job(workflow: &str, name: &str) -> Result { + let header = format!("\n {name}:\n"); + let start = workflow + .find(&header) + .ok_or_else(|| format!("no job `{name}`"))? + + header.len(); + let body: Vec<&str> = workflow[start..] + .lines() + .take_while(|line| line.is_empty() || line.starts_with(" ")) + .collect(); + Ok(body.join("\n")) +} + +/// Where `needle` first appears in `text`, or the refusal that names it. +fn position_of(text: &str, needle: &str, context: &str) -> Result { + text.find(needle) + .ok_or_else(|| format!("{context} has no `{needle}`")) +} + +/// RP-18 (§30.3, #260): the workflows prove the crate on every run and gate its +/// upload. The crate job packages twice to the same bytes, dry-runs, checks the +/// archive against what crates.io needs, and compares the bytes with the crate +/// the release attaches and the checksum it lists; the tag's `publish` job +/// repeats the comparison against the dry-run package before it asks how the +/// upload is authorised, and the one step that runs `cargo publish` without +/// `--dry-run` there, and the one in the pre-release job, run only when it is. +fn crate_publication_workflows(release: &str, crate_workflow: &str) -> Result<(), String> { + let in_order = |text: &str, context: &str, needles: &[&str]| -> Result<(), String> { + let mut previous = 0; + for needle in needles { + let at = position_of(text, needle, context)?; + if at < previous { + return Err(format!("{context}: `{needle}` comes before the step it must follow")); + } + previous = at; + } + Ok(()) + }; + let uploads = |text: &str| -> usize { + text.lines() + .filter(|line| line.contains("cargo publish ") && !line.contains("--dry-run")) + .filter(|line| !line.trim_start().starts_with('#') && !line.trim_start().starts_with("echo")) + .count() + }; + + // release.yml: every run calls the crate workflow, and the tag waits for it. + let crate_job = workflow_job(release, "crate")?; + for needle in [ + "needs: identity", + "uses: ./.github/workflows/crate.yml", + "prerelease: false", + ] { + position_of(&crate_job, needle, "release.yml job `crate`")?; + } + let publish = workflow_job(release, "publish")?; + let needs = publish + .lines() + .find(|line| line.trim_start().starts_with("needs:")) + .ok_or("release.yml job `publish` has no needs")?; + if !needs.contains("crate,") { + return Err("release.yml job `publish` does not wait for the `crate` job".to_owned()); + } + in_order( + &publish, + "release.yml job `publish`", + &[ + "cargo xtask release-artifacts", + "cargo publish --dry-run --locked --package lexlean", + ".github/crate-publication.sh identity release", + ".github/crate-publication.sh mode", + "if: steps.upload.outputs.mode == 'trusted'", + "if: steps.upload.outputs.mode != 'none'", + "cargo publish --locked --package lexlean", + ], + )?; + position_of(&publish, "needs.crate.outputs.sha256", "release.yml job `publish`")?; + if uploads(&publish) != 1 { + return Err("release.yml job `publish` runs `cargo publish` without --dry-run other than once".to_owned()); + } + for guarded in [ + "- name: Publish the exact verified crate to crates.io\n if: steps.upload.outputs.mode != 'none'\n", + "- name: Acquire crates.io trusted-publisher token\n if: steps.upload.outputs.mode == 'trusted'\n", + ] { + position_of(&publish, guarded, "release.yml job `publish`")?; + } + // The token reaches cargo in the one step that uploads. + let token_uses = publish.matches("secrets.CARGO_REGISTRY_TOKEN").count(); + if token_uses != 2 { + return Err(format!( + "release.yml job `publish` reads the token {token_uses} times: once to learn it exists and once to upload" + )); + } + + // crate.yml: the proof, then the guarded upload of a pre-release. + let readiness = workflow_job(crate_workflow, "readiness")?; + in_order( + &readiness, + "crate.yml job `readiness`", + &[ + ".github/crate-publication.sh prepare", + "cargo package --locked \"${dirty[@]}\" --package lexlean --target-dir \"$a\"", + "cargo package --locked --no-verify \"${dirty[@]}\" --package lexlean --target-dir \"$b\"", + "cmp \"$a/package/$crate\" \"$b/package/$crate\"", + "cargo publish --dry-run --locked \"${dirty[@]}\" --package lexlean --target-dir \"$dry\"", + "cmp \"$a/package/$crate\" \"$dry/package/$crate\"", + ".github/crate-publication.sh metadata \"$dry/package/$crate\"", + "cargo xtask release-artifacts", + ".github/crate-publication.sh identity release \"$dry/package/$crate\"", + ], + )?; + if uploads(&readiness) != 0 { + return Err("crate.yml job `readiness` uploads".to_owned()); + } + let prerelease = workflow_job(crate_workflow, "prerelease")?; + position_of( + &prerelease, + "if: ${{ github.event_name == 'workflow_dispatch' && inputs.prerelease }}", + "crate.yml job `prerelease`", + )?; + in_order( + &prerelease, + "crate.yml job `prerelease`", + &[ + ".github/crate-publication.sh mode", + "- name: Upload the exact checked crate\n if: ${{ steps.upload.outputs.mode != 'none' }}\n", + "test \"$(sha256sum \"${RUNNER_TEMP}/upload/package/lexlean-${VERSION}.crate\"", + "cargo publish --locked --allow-dirty --package lexlean", + ], + )?; + if uploads(&prerelease) != 1 { + return Err("crate.yml job `prerelease` runs `cargo publish` without --dry-run other than once".to_owned()); + } + position_of( + &prerelease, + "- name: Acquire crates.io trusted-publisher token\n if: ${{ steps.upload.outputs.mode == 'trusted' }}\n", + "crate.yml job `prerelease`", + )?; + Ok(()) +} + +/// What `.github/crate-publication.sh` decides for planted inputs (RP-18): the +/// script runs in scratch directories, so that each decision is shown and each +/// way of being wrong is refused. It is bash with `sha256sum`, `tar` and `sed`, +/// run where the gate runs (§8.3, §9.4: the normative host is Linux). +fn crate_publication_decisions() { + use std::process::Command; + if !cfg!(target_os = "linux") { + return; + } + let root = support::repo_root(); + let script = root.join(".github/crate-publication.sh"); + let scratch = tempfile::tempdir().expect("tempdir"); + let dir = scratch.path(); + let run = |args: &[&str], environment: &[(&str, &str)]| -> (i32, String, String) { + let mut command = Command::new("bash"); + command + .arg(script.as_std_path()) + .args(args) + .current_dir(dir) + .env_remove("HAS_CARGO_REGISTRY_TOKEN") + .env_remove("TRUSTED_PUBLISHING"); + for (key, value) in environment { + command.env(key, value); + } + let output = command.output().expect("bash runs"); + ( + output.status.code().expect("an exit code"), + String::from_utf8_lossy(&output.stdout).trim().to_owned(), + String::from_utf8_lossy(&output.stderr).trim().to_owned(), + ) + }; + + // How the upload is authorised: a token, trusted publishing, or neither. + for (environment, expected) in [ + (vec![("HAS_CARGO_REGISTRY_TOKEN", "true")], "token"), + ( + vec![("HAS_CARGO_REGISTRY_TOKEN", "true"), ("TRUSTED_PUBLISHING", "true")], + "token", + ), + (vec![("TRUSTED_PUBLISHING", "true")], "trusted"), + ( + vec![("HAS_CARGO_REGISTRY_TOKEN", "false"), ("TRUSTED_PUBLISHING", "false")], + "none", + ), + (vec![("HAS_CARGO_REGISTRY_TOKEN", "")], "none"), + (vec![], "none"), + ] { + let (status, out, _) = run(&["mode"], &environment); + assert_eq!((status, out.as_str()), (0, expected), "mode for {environment:?}"); + } + + // A commit of a release line is a development pre-release of its release. + assert_eq!(run(&["prerelease", "release/v0.4", "242"], &[]).1, "0.4.0-dev.242"); + assert_eq!(run(&["prerelease", "release/v12.3", "7"], &[]).1, "12.3.0-dev.7"); + for (reference, count) in [ + ("main", "242"), + ("release/v0.4.1", "242"), + ("refs/heads/release/v0.4", "242"), + ("release/v0.4", "x"), + ("release/v0.4", ""), + ("release/v0.4", "-1"), + ] { + let (status, _, error) = run(&["prerelease", reference, count], &[]); + assert_ne!(status, 0, "{reference} at {count:?} names no pre-release: {error}"); + } + + // The workspace and its crates take the stamped version, and nothing else does. + let manifest = root_file("Cargo.toml"); + let stamped = dir.join("stamped"); + std::fs::create_dir(&stamped).expect("mkdir"); + std::fs::write(stamped.join("Cargo.toml"), &manifest).expect("write"); + let (status, previous, error) = run(&["stamp", "0.4.0-dev.242", stamped.to_str().expect("utf8")], &[]); + assert_eq!(status, 0, "{error}"); + let after = std::fs::read_to_string(stamped.join("Cargo.toml")).expect("read"); + assert_eq!(after.matches("0.4.0-dev.242").count(), 4, "the workspace and its three crates"); + assert!(!after.contains(&format!("version = \"{previous}\"")), "no version stays"); + assert_eq!( + after.replace("0.4.0-dev.242", &previous), + manifest, + "stamping changes the four versions and nothing else" + ); + for version in ["0.4", "v0.4.0", "0.4.0-rc.1", "latest", ""] { + let (status, _, _) = run(&["stamp", version, stamped.to_str().expect("utf8")], &[]); + assert_ne!(status, 0, "{version:?} is no version a pre-release may take"); + } + let bare = dir.join("bare"); + std::fs::create_dir(&bare).expect("mkdir"); + std::fs::write(bare.join("Cargo.toml"), "[workspace]\nmembers = []\n").expect("write"); + assert_ne!(run(&["stamp", "0.4.0-dev.1", bare.to_str().expect("utf8")], &[]).0, 0); + + // The crate cargo would upload is the crate the release holds and lists. + let release = dir.join("release"); + std::fs::create_dir(&release).expect("mkdir"); + let crate_bytes: Vec = (0..4096u32).map(|n| (n * 31 % 251) as u8).collect(); + std::fs::write(release.join("lexlean.crate"), &crate_bytes).expect("write"); + let digest = |bytes: &[u8]| -> String { + let output = Command::new("sha256sum") + .current_dir(dir) + .stdin(std::process::Stdio::piped()) + .stdout(std::process::Stdio::piped()) + .spawn() + .and_then(|mut child| { + use std::io::Write; + child.stdin.take().expect("stdin").write_all(bytes)?; + child.wait_with_output() + }) + .expect("sha256sum runs"); + String::from_utf8_lossy(&output.stdout) + .split_whitespace() + .next() + .expect("a digest") + .to_owned() + }; + let good = digest(&crate_bytes); + let packaged = dir.join("packaged.crate"); + let release_arg = release.to_str().expect("utf8"); + let packaged_arg = packaged.to_str().expect("utf8"); + let other_hash = format!("{}{}", if good.starts_with('0') { "1" } else { "0" }, &good[1..]); + let mut altered = crate_bytes.clone(); + altered[100] ^= 1; + let cases: [(&str, Vec, String, bool); 6] = [ + ("the crate the release lists and holds", crate_bytes.clone(), format!("{good} lexlean.crate\n"), true), + ("a package one byte from the crate the release holds", altered.clone(), format!("{good} lexlean.crate\n"), false), + ("a checksum line of another digest", crate_bytes.clone(), format!("{other_hash} lexlean.crate\n"), false), + ("no line for the crate", crate_bytes.clone(), format!("{good} SPEC.md\n"), false), + ( + "two lines for the crate", + crate_bytes.clone(), + format!("{good} lexlean.crate\n{good} lexlean.crate\n"), + false, + ), + ("an empty checksum list", crate_bytes.clone(), String::new(), false), + ]; + for (label, package, checksums, accepted) in cases { + std::fs::write(&packaged, &package).expect("write"); + std::fs::write(release.join("checksums.txt"), &checksums).expect("write"); + let (status, out, error) = run(&["identity", release_arg, packaged_arg], &[]); + if accepted { + assert_eq!((status, out.as_str()), (0, good.as_str()), "{label}: {error}"); + } else { + assert_ne!(status, 0, "{label} is refused"); + assert!(error.starts_with("identity:"), "{label}: {error}"); + } + } + // The release without the crate, without its list, and without a package. + std::fs::write(&packaged, &crate_bytes).expect("write"); + std::fs::write(release.join("checksums.txt"), format!("{good} lexlean.crate\n")).expect("write"); + for missing in ["lexlean.crate", "checksums.txt"] { + let kept = std::fs::read(release.join(missing)).expect("read"); + std::fs::remove_file(release.join(missing)).expect("remove"); + assert_ne!(run(&["identity", release_arg, packaged_arg], &[]).0, 0, "{missing} is missing"); + std::fs::write(release.join(missing), kept).expect("restore"); + } + assert_ne!( + run(&["identity", release_arg, dir.join("absent.crate").to_str().expect("utf8")], &[]).0, + 0, + "no package" + ); + + // What crates.io needs from an archive. + let archive = |name: &str, manifest: &[&str], files: &[(&str, Vec)]| -> String { + let folder = dir.join(format!("{name}-1.0.0")); + std::fs::create_dir_all(&folder).expect("mkdir"); + let mut text = format!("[package]\nname = \"{name}\"\nversion = \"1.0.0\"\n"); + for line in manifest { + text.push_str(line); + text.push('\n'); + } + std::fs::write(folder.join("Cargo.toml"), text).expect("write"); + for (file, bytes) in files { + std::fs::write(folder.join(file), bytes).expect("write"); + } + let path = dir.join(format!("{name}.crate")); + let status = Command::new("tar") + .current_dir(dir) + .args(["-czf", path.to_str().expect("utf8"), &format!("{name}-1.0.0")]) + .status() + .expect("tar runs"); + assert!(status.success()); + path.to_str().expect("utf8").to_owned() + }; + let complete = [ + "description = \"A sample\"", + "license = \"MIT\"", + "repository = \"https://example.test/sample\"", + "readme = \"README.md\"", + ]; + let readme: Vec<(&str, Vec)> = vec![("README.md", b"# sample\n".to_vec())]; + let without = |field: &str| -> Vec<&str> { + complete + .iter() + .copied() + .filter(|line| !line.starts_with(field)) + .collect() + }; + let (status, _, error) = run(&["metadata", &archive("complete", &complete, &readme)], &[]); + assert_eq!(status, 0, "an archive with what crates.io needs: {error}"); + // Incompressible bytes, so that the archive is as large as its contents. + let mut state = 0x2545_F491_4F6C_DD1Du64; + let large: Vec = (0..11 * 1024 * 1024) + .map(|_| { + state ^= state << 13; + state ^= state >> 7; + state ^= state << 17; + (state >> 24) as u8 + }) + .collect(); + let mut oversize = readme.clone(); + oversize.push(("padding.bin", large)); + for (label, path, says) in [ + ("no description", archive("nodescription", &without("description"), &readme), "no `description`"), + ("no license", archive("nolicense", &without("license"), &readme), "neither `license` nor `license-file`"), + ("no repository", archive("norepository", &without("repository"), &readme), "no `repository`"), + ("a readme it lacks", archive("noreadme", &complete, &[]), "names a file the archive does not carry"), + ("more than 10 MiB", archive("oversize", &complete, &oversize), "exceeds the crates.io limit"), + ] { + let (status, _, error) = run(&["metadata", &path], &[]); + assert_ne!(status, 0, "{label} is refused"); + assert!(error.contains(says), "{label}: {error}"); + } +} + +/// RP-18: see [`crate_publication_workflows`] and +/// [`crate_publication_decisions`]. The workflows are read as committed and +/// then with one check removed or reversed at a time; a removal that changes +/// nothing is itself a failure, because it would plant nothing. +fn rp_18() { + let release = root_file(".github/workflows/release.yml"); + let crate_workflow = root_file(".github/workflows/crate.yml"); + crate_publication_workflows(&release, &crate_workflow) + .expect("the committed workflows prove the crate and gate its upload"); + + let replaced = |text: &str, from: &str, to: &str| -> String { + assert!(text.contains(from), "the plant `{from}` is in the workflow"); + text.replacen(from, to, 1) + }; + let publish_dry_run = "cargo publish --dry-run --locked --package lexlean --target-dir \"${RUNNER_TEMP}/dry\""; + let release_plants: Vec<(&str, String)> = vec![ + ( + "a tag that does not wait for the crate job", + replaced(&release, "needs: [identity, crate, gate, binaries, manifest]", "needs: [identity, gate, binaries, manifest]"), + ), + ( + "a release that does not call the crate workflow", + replaced(&release, "uses: ./.github/workflows/crate.yml", "uses: ./.github/workflows/other.yml"), + ), + ( + "an upload without the dry run first", + replaced(&release, publish_dry_run, "true"), + ), + ( + "an upload without the identity check", + replaced(&release, ".github/crate-publication.sh identity release", "true"), + ), + ( + "an upload that ignores how it is authorised", + replaced( + &release, + "- name: Publish the exact verified crate to crates.io\n if: steps.upload.outputs.mode != 'none'\n", + "- name: Publish the exact verified crate to crates.io\n", + ), + ), + ( + "an upload whose guard is always true", + replaced( + &release, + "if: steps.upload.outputs.mode != 'none'\n env:\n CARGO_REGISTRY_TOKEN", + "if: always()\n env:\n CARGO_REGISTRY_TOKEN", + ), + ), + ( + "trusted publishing acquired without being selected", + replaced( + &release, + "- name: Acquire crates.io trusted-publisher token\n if: steps.upload.outputs.mode == 'trusted'\n", + "- name: Acquire crates.io trusted-publisher token\n", + ), + ), + ( + "a second upload step", + format!("{release}\n - run: cargo publish --locked --package lexlean\n"), + ), + ( + "the token read where it is not needed", + replaced(&release, " TRUSTED_PUBLISHING:", " EXTRA: ${{ secrets.CARGO_REGISTRY_TOKEN }}\n TRUSTED_PUBLISHING:"), + ), + ]; + for (why, text) in &release_plants { + assert!( + crate_publication_workflows(text, &crate_workflow).is_err(), + "release.yml with {why} is refused" + ); + } + let cmp_ab = "cmp \"$a/package/$crate\" \"$b/package/$crate\""; + let crate_plants: Vec<(&str, String)> = vec![ + ("packages once, so never compared", replaced(&crate_workflow, cmp_ab, "true")), + ( + "no dry run", + replaced( + &crate_workflow, + "cargo publish --dry-run --locked \"${dirty[@]}\" --package lexlean --target-dir \"$dry\"", + "true", + ), + ), + ( + "no archive metadata check", + replaced(&crate_workflow, ".github/crate-publication.sh metadata \"$dry/package/$crate\"", "true"), + ), + ( + "no comparison with the checksum the release lists", + replaced(&crate_workflow, ".github/crate-publication.sh identity release \"$dry/package/$crate\"", "true"), + ), + ( + "a pre-release uploaded by a call from the release workflow", + replaced( + &crate_workflow, + "if: ${{ github.event_name == 'workflow_dispatch' && inputs.prerelease }}", + "if: ${{ inputs.prerelease }}", + ), + ), + ( + "a pre-release uploaded without a credential", + replaced( + &crate_workflow, + "- name: Upload the exact checked crate\n if: ${{ steps.upload.outputs.mode != 'none' }}\n", + "- name: Upload the exact checked crate\n", + ), + ), + ( + "a pre-release uploaded without comparing its bytes", + replaced(&crate_workflow, "test \"$(sha256sum \"${RUNNER_TEMP}/upload/package/lexlean-${VERSION}.crate\"", "true \"$(sha256sum \"${RUNNER_TEMP}/upload/package/lexlean-${VERSION}.crate\""), + ), + ( + "the readiness job uploading", + replaced(&crate_workflow, " cmp \"$a/package/$crate\" \"$dry/package/$crate\"\n", " cmp \"$a/package/$crate\" \"$dry/package/$crate\"\n cargo publish --locked --package lexlean\n"), + ), + ]; + for (why, text) in &crate_plants { + assert!( + crate_publication_workflows(&release, text).is_err(), + "crate.yml with {why} is refused" + ); + } + + crate_publication_decisions(); +} diff --git a/crates/conformance/tests/conformance.rs b/crates/conformance/tests/conformance.rs index 126a292f4d..2d8bcb08b3 100644 --- a/crates/conformance/tests/conformance.rs +++ b/crates/conformance/tests/conformance.rs @@ -85,6 +85,11 @@ fn conformance_rp_16() { repo_conformance::cases::run("RP-16"); } +#[test] +fn conformance_rp_18() { + repo_conformance::cases::run("RP-18"); +} + #[test] fn conformance_cf_01() { repo_conformance::cases::run("CF-01"); diff --git a/features/suites/repository.feature b/features/suites/repository.feature index 3152c2df7f..f46691fb20 100644 --- a/features/suites/repository.feature +++ b/features/suites/repository.feature @@ -120,3 +120,11 @@ Feature: repository Then the Rust toolchain it installs is the channel rust-toolchain.toml pins and the Lean toolchain it installs is the one lean-toolchain pins And it installs no other toolchain and selects no unpinned default And a Dockerfile that names another version of either, a second toolchain, or an unpinned default is refused + + @RP-18 @build + Scenario: The release workflow packages the lexlean crate twice to the same bytes, runs cargo publish --dry-run, and refuses a crate whose SHA-256 differs from the one release/checksums.txt lists for it or from the bytes cargo would upload, or whose archive lacks the metadata and size crates.io requires, and uploads to crates.io only when a CARGO_REGISTRY_TOKEN secret or trusted publishing authorises it; a commit of a release line release/vX.Y is published as the pre-release X.Y.0-dev.N, N being its number of first-parent commits, and a plant in each of these checks is refused. + Given .github/workflows/release.yml, .github/workflows/crate.yml, and .github/crate-publication.sh + When the workflows are read and the script is run against planted release directories, archives, refs, and environments + Then the crate is packaged twice to the same bytes and dry-run on every run, and the crate cargo would upload is the crate release/lexlean.crate holds and release/checksums.txt lists + And the only step that uploads to crates.io runs after those checks, and only when a token or trusted publishing is present + And a commit of a release line is named X.Y.0-dev.N, and a package, checksum, metadata, version, or credential check that is removed or planted is refused diff --git a/model/ids.toml b/model/ids.toml index a801209b81..38447f0a8d 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -103,6 +103,12 @@ level = "build" suite = "repository" statement = "The development container installs, at image build, exactly the Rust toolchain that rust-toolchain.toml pins and exactly the Lean toolchain that lean-toolchain pins and selects no other default, so that nothing is fetched when a session starts, and a Dockerfile that names another version of either, installs a second toolchain, or selects an unpinned default is refused." +[[id]] +id = "RP-18" +level = "build" +suite = "repository" +statement = "The release workflow packages the lexlean crate twice to the same bytes, runs cargo publish --dry-run, and refuses a crate whose SHA-256 differs from the one release/checksums.txt lists for it or from the bytes cargo would upload, or whose archive lacks the metadata and size crates.io requires, and uploads to crates.io only when a CARGO_REGISTRY_TOKEN secret or trusted publishing authorises it; a commit of a release line release/vX.Y is published as the pre-release X.Y.0-dev.N, N being its number of first-parent commits, and a plant in each of these checks is refused." + [[id]] id = "CF-01" level = "build" From e55eadbe27fe9f9b2331140643269a7c86a39b5e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 14:26:39 +0100 Subject: [PATCH 2/4] [0.4] #260 RP-18: prove the lexlean crate before anyone uploads it, upload only with a credential Part of #260; the first upload is the owner's. Implements the skeleton commit. .github/workflows/crate.yml, called by release.yml on every run, packages the crate twice to the same bytes, runs cargo publish --dry-run, checks the archive for what crates.io needs, and requires its SHA-256 to equal release/lexlean.crate and the line checksums.txt lists for it. The publish job of release.yml repeats the comparison against its own dry-run package and uploads only with a CARGO_REGISTRY_TOKEN secret or trusted publishing; with neither it creates the release and says the crate was not uploaded, where the first run used to fail after the tag was pushed. Dispatched on a release line, crate.yml does the same for X.Y.0-dev.N, N being the commit's number of first-parent commits. .github/crate-publication.sh holds each decision so the case can plant it. The register is 449 IDs: README.md, xtask/src/spec_links.rs and RP-07's case count it. Co-Authored-By: Claude Sonnet 5.5 --- .github/crate-publication.sh | 164 ++++++++++++++++++ .github/workflows/crate.yml | 165 ++++++++++++++++++ .github/workflows/release.yml | 54 +++++- CHANGELOG.md | 2 + README.md | 2 +- crates/conformance/src/cases/repository.rs | 191 +++++++++++++++++---- xtask/src/spec_links.rs | 4 +- 7 files changed, 539 insertions(+), 43 deletions(-) create mode 100755 .github/crate-publication.sh create mode 100644 .github/workflows/crate.yml diff --git a/.github/crate-publication.sh b/.github/crate-publication.sh new file mode 100755 index 0000000000..a5f0d0ce46 --- /dev/null +++ b/.github/crate-publication.sh @@ -0,0 +1,164 @@ +#!/usr/bin/env bash +# The decisions of publishing the lexlean crate to crates.io (RP-18, #260), kept +# in one script so that each can be run against planted inputs. release.yml +# calls it; nothing here uploads, and nothing here reads or prints a token. +# +# crate-publication.sh identity RELEASE_DIR PACKAGED +# PACKAGED, the crate `cargo publish` would upload, must have the SHA-256 +# of RELEASE_DIR/lexlean.crate and the SHA-256 that RELEASE_DIR/checksums.txt +# lists for it. Prints the digest. +# crate-publication.sh metadata PACKAGED... +# What crates.io needs from an archive: description, license, repository, +# a readme the archive carries, and at most 10 MiB. +# crate-publication.sh mode +# How the upload is authorised, from HAS_CARGO_REGISTRY_TOKEN and +# TRUSTED_PUBLISHING (each `true` or anything else): token, trusted, or none. +# crate-publication.sh prerelease REF COUNT +# The version of a commit of a release line: `release/v0.4` and a count of +# first-parent commits give `0.4.0-dev.`. +# crate-publication.sh stamp VERSION [ROOT] +# Rewrite the workspace version, and the version of the workspace's own +# crates, in ROOT/Cargo.toml (a throwaway checkout, never a commit). +set -euo pipefail + +fail() { + printf '%s\n' "$1" >&2 + exit 1 +} + +digest() { + sha256sum "$1" | cut -d' ' -f1 +} + +# The tag a pre-release names must be a SemVer pre-release of a release line. +semver_prerelease='^[0-9]+\.[0-9]+\.[0-9]+-dev\.[0-9]+$' +semver_release='^[0-9]+\.[0-9]+\.[0-9]+$' + +identity() { + release=$1 packaged=$2 + [[ -f "$release/lexlean.crate" ]] || fail "identity: $release/lexlean.crate is missing" + [[ -f "$release/checksums.txt" ]] || fail "identity: $release/checksums.txt is missing" + [[ -f "$packaged" ]] || fail "identity: $packaged is missing" + actual=$(digest "$packaged") + staged=$(digest "$release/lexlean.crate") + [[ "$actual" == "$staged" ]] || + fail "identity: cargo would upload $actual, and the release attaches lexlean.crate $staged" + listed=$(sed -n 's/^\([0-9a-f]\{64\}\) lexlean\.crate$/\1/p' "$release/checksums.txt") + [[ -n "$listed" ]] || fail "identity: checksums.txt lists no lexlean.crate" + [[ "$(printf '%s\n' "$listed" | wc -l)" -eq 1 ]] || fail "identity: checksums.txt lists lexlean.crate twice" + [[ "$listed" == "$actual" ]] || + fail "identity: cargo would upload $actual, and checksums.txt lists $listed for lexlean.crate" + printf '%s\n' "$actual" +} + +metadata() { + limit=10485760 + status=0 + for archive in "$@"; do + if [[ ! -f "$archive" ]]; then + printf '%s: no such archive\n' "$archive" >&2 + status=1 + continue + fi + size=$(wc -c < "$archive" | tr -d ' ') + if ((size > limit)); then + printf '%s: %s bytes exceeds the crates.io limit of %s\n' "$archive" "$size" "$limit" >&2 + status=1 + fi + manifest=$(tar -xzOf "$archive" --wildcards '*/Cargo.toml' 2>/dev/null || true) + if [[ -z "$manifest" ]]; then + printf '%s: no Cargo.toml in the archive\n' "$archive" >&2 + status=1 + continue + fi + package=$(printf '%s\n' "$manifest" | sed -n '/^\[package\]/,/^\[/p') + field() { + printf '%s\n' "$package" | sed -n "s/^$1 = \"\\(.*\\)\"\$/\\1/p" | head -1 + } + for required in description repository; do + if [[ -z "$(field "$required")" ]]; then + printf '%s: Cargo.toml has no `%s`\n' "$archive" "$required" >&2 + status=1 + fi + done + if [[ -z "$(field license)" && -z "$(field license-file)" ]]; then + printf '%s: Cargo.toml has neither `license` nor `license-file`\n' "$archive" >&2 + status=1 + fi + readme=$(field readme) + # The listing is read whole: `grep -q` leaves a pipe early, and pipefail + # would then call a present readme missing. + listing=$(tar -tzf "$archive") + if [[ -n "$readme" ]] && ! grep -q -- "/$readme\$" <<<"$listing"; then + printf '%s: `readme = "%s"` names a file the archive does not carry\n' "$archive" "$readme" >&2 + status=1 + fi + done + return "$status" +} + +mode() { + if [[ "${HAS_CARGO_REGISTRY_TOKEN:-}" == true ]]; then + echo token + elif [[ "${TRUSTED_PUBLISHING:-}" == true ]]; then + echo trusted + else + echo none + fi +} + +prerelease() { + ref=$1 count=$2 + [[ "$ref" =~ ^release/v([0-9]+)\.([0-9]+)$ ]] || + fail "prerelease: $ref is not a release line (release/vX.Y)" + major=${BASH_REMATCH[1]} minor=${BASH_REMATCH[2]} + [[ "$count" =~ ^[0-9]+$ ]] || fail "prerelease: the commit count $count is not a number" + printf '%s.%s.0-dev.%s\n' "$major" "$minor" "$count" +} + +stamp() { + version=$1 root=${2:-.} + [[ "$version" =~ $semver_prerelease || "$version" =~ $semver_release ]] || + fail "stamp: $version is not a SemVer version" + manifest=$root/Cargo.toml + current=$(sed -n '/^\[workspace\.package\]/,/^\[/s/^version = "\(.*\)"$/\1/p' "$manifest" | head -1) + [[ -n "$current" ]] || fail "stamp: $manifest has no workspace version" + escaped=${current//./\\.} + sed -i \ + -e "/^\\[workspace\\.package\\]/,/^\\[/s/^version = \"$escaped\"\$/version = \"$version\"/" \ + -e "s/^\\(repo-model\\|repo-conformance\\|lexlean\\) = { version = \"$escaped\", path/\\1 = { version = \"$version\", path/" \ + "$manifest" + # The workspace version and its three crates, and nothing at the old version. + stamped=$(grep -c "version = \"$version\"" "$manifest" || true) + [[ "$stamped" -eq 4 ]] || fail "stamp: expected 4 versions at $version in $manifest, found $stamped" + printf '%s\n' "$current" +} + +# The checkout the crate is packaged from. For a pre-release it is a throwaway +# copy of a release line at one commit: the commit count and the line name give +# the version, and the stamped manifest and lock are never committed. +prepare() { + pre=$1 + if [[ "$pre" == true ]]; then + [[ "$(git rev-parse --is-shallow-repository)" == false ]] || + fail "prepare: the commit count needs the whole history (fetch-depth: 0)" + version=$(prerelease "${GITHUB_REF_NAME:?prepare: GITHUB_REF_NAME names the release line}" \ + "$(git rev-list --first-parent --count HEAD)") + stamp "$version" . > /dev/null + cargo update --workspace --quiet + printf '%s\n' "$version" + else + sed -n '/^\[workspace\.package\]/,/^\[/s/^version = "\(.*\)"$/\1/p' Cargo.toml | head -1 + fi +} + +command=${1:-} +case "$command" in + prepare) [[ $# -eq 2 ]] || fail "usage: $0 prepare true|false"; prepare "$2" ;; + identity) [[ $# -eq 3 ]] || fail "usage: $0 identity RELEASE_DIR PACKAGED"; identity "$2" "$3" ;; + metadata) [[ $# -ge 2 ]] || fail "usage: $0 metadata PACKAGED..."; shift; metadata "$@" ;; + mode) [[ $# -eq 1 ]] || fail "usage: $0 mode"; mode ;; + prerelease) [[ $# -eq 3 ]] || fail "usage: $0 prerelease REF COUNT"; prerelease "$2" "$3" ;; + stamp) [[ $# -ge 2 && $# -le 3 ]] || fail "usage: $0 stamp VERSION [ROOT]"; stamp "$2" "${3:-.}" ;; + *) fail "usage: $0 identity|metadata|mode|prerelease|stamp ..." ;; +esac diff --git a/.github/workflows/crate.yml b/.github/workflows/crate.yml new file mode 100644 index 0000000000..971c8e7695 --- /dev/null +++ b/.github/workflows/crate.yml @@ -0,0 +1,165 @@ +# The lexlean crate on crates.io (#260): what must hold before anyone uploads it, +# and the upload of a development pre-release of a release line. +# +# `release.yml` calls this workflow for every run, so a rehearsal and a tag both +# prove the crate: it packages twice to the same bytes, the bytes `cargo publish +# --dry-run` would send are those bytes, they meet what crates.io needs from an +# archive, and they are the `lexlean.crate` that `cargo xtask release-artifacts` +# attaches, with the SHA-256 its `checksums.txt` lists. A tag's upload is the +# `publish` job of release.yml. +# +# Dispatched on a release line (`release/vX.Y`) with `prerelease`, it does the +# same for `X.Y.0-dev.`, n being the number of first-parent commits of the +# line at the dispatched commit, and uploads that version when a credential +# exists. The upload needs a `CARGO_REGISTRY_TOKEN` secret in the crates.io +# environment, or the repository variable CRATES_IO_TRUSTED_PUBLISHING set to +# `true` once the owner has configured trusted publishing for the crate. With +# neither, nothing is uploaded and the run says so. The first upload of a name +# is the owner's: trusted publishing cannot be configured for a crate that does +# not exist. +name: crate + +on: + workflow_call: + inputs: + prerelease: + description: Package a development pre-release of the release line instead of the workspace version + type: boolean + default: false + outputs: + sha256: + description: The SHA-256 of the crate every check agreed on + value: ${{ jobs.readiness.outputs.sha256 }} + version: + description: The crate version + value: ${{ jobs.readiness.outputs.version }} + workflow_dispatch: + inputs: + prerelease: + description: Package, and upload when authorised, X.Y.0-dev. of the release line this is dispatched on + type: boolean + default: true + +permissions: + contents: read + +env: + CARGO_TERM_COLOR: never + +jobs: + readiness: + name: crate readiness + runs-on: ubuntu-24.04 + timeout-minutes: 90 + outputs: + sha256: ${{ steps.prove.outputs.sha256 }} + version: ${{ steps.prove.outputs.version }} + steps: + # The whole history: a pre-release is named by its commit count. + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 0 + - name: Install the pinned Rust toolchain + run: rustup toolchain install + - id: prove + shell: bash + env: + PRERELEASE: ${{ inputs.prerelease }} + run: | + set -euo pipefail + version="$(.github/crate-publication.sh prepare "$PRERELEASE")" + a="${RUNNER_TEMP}/package-a" b="${RUNNER_TEMP}/package-b" dry="${RUNNER_TEMP}/dry" + crate="lexlean-${version}.crate" + # A pre-release is packaged from a stamped copy of the commit, which + # cargo calls dirty; the crate records the commit it was cut from + # and that it was stamped (`.cargo_vcs_info.json`). + dirty=() + if [ "$PRERELEASE" = true ]; then dirty=(--allow-dirty); fi + cargo package --locked "${dirty[@]}" --package lexlean --target-dir "$a" + cargo package --locked --no-verify "${dirty[@]}" --package lexlean --target-dir "$b" + cmp "$a/package/$crate" "$b/package/$crate" + cargo publish --dry-run --locked "${dirty[@]}" --package lexlean --target-dir "$dry" + cmp "$a/package/$crate" "$dry/package/$crate" + .github/crate-publication.sh metadata "$dry/package/$crate" + if [ "$PRERELEASE" = true ]; then + sha256="$(sha256sum "$dry/package/$crate" | cut -d' ' -f1)" + agreed="three packagings of the same commit" + else + # The crate the release attaches and the checksum it lists for it. + cargo xtask release-artifacts + sha256="$(.github/crate-publication.sh identity release "$dry/package/$crate")" + agreed="the crate release-artifacts attaches and the checksum checksums.txt lists" + fi + echo "sha256=$sha256" >> "$GITHUB_OUTPUT" + echo "version=$version" >> "$GITHUB_OUTPUT" + { + echo "## lexlean ${version}" + echo + echo "Packaged, dry-run, and checked against crates.io's metadata; ${agreed} agree:" + echo + echo '```text' + echo "${sha256} ${crate}" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" + + prerelease: + name: upload the development pre-release + needs: readiness + # Only a dispatch uploads from here; a call from release.yml proves the + # crate and uploads nothing. + if: ${{ github.event_name == 'workflow_dispatch' && inputs.prerelease }} + runs-on: ubuntu-24.04 + timeout-minutes: 45 + environment: crates.io + env: + HAS_CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN != '' }} + TRUSTED_PUBLISHING: ${{ vars.CRATES_IO_TRUSTED_PUBLISHING == 'true' }} + permissions: + contents: read + id-token: write + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 0 + - name: Install the pinned Rust toolchain + run: rustup toolchain install + - name: Decide how the upload is authorised + id: upload + shell: bash + run: echo "mode=$(.github/crate-publication.sh mode)" >> "$GITHUB_OUTPUT" + - name: Acquire crates.io trusted-publisher token + if: ${{ steps.upload.outputs.mode == 'trusted' }} + uses: rust-lang/crates-io-auth-action@c6f97d42243bad5fab37ca0427f495c86d5b1a18 + id: crates-auth + - name: No upload credential + if: ${{ steps.upload.outputs.mode == 'none' }} + env: + VERSION: ${{ needs.readiness.outputs.version }} + CRATE_SHA256: ${{ needs.readiness.outputs.sha256 }} + run: echo "::notice::lexlean ${VERSION} (sha256 ${CRATE_SHA256}) was packaged and dry-run; no CARGO_REGISTRY_TOKEN and no trusted publishing, so nothing was uploaded" + - name: Upload the exact checked crate + if: ${{ steps.upload.outputs.mode != 'none' }} + env: + CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN || steps.crates-auth.outputs.token }} + VERSION: ${{ needs.readiness.outputs.version }} + CRATE_SHA256: ${{ needs.readiness.outputs.sha256 }} + shell: bash + run: | + set -euo pipefail + [ "$(.github/crate-publication.sh prepare true)" = "$VERSION" ] + cargo package --locked --no-verify --allow-dirty --package lexlean --target-dir "${RUNNER_TEMP}/upload" + test "$(sha256sum "${RUNNER_TEMP}/upload/package/lexlean-${VERSION}.crate" | cut -d' ' -f1)" = "$CRATE_SHA256" + cargo publish --locked --allow-dirty --package lexlean --target-dir "${RUNNER_TEMP}/upload" + for attempt in $(seq 1 30); do + printf 'checking crates.io visibility (attempt %s/30)\n' "$attempt" + if curl --fail --location --silent --show-error \ + "https://crates.io/api/v1/crates/lexlean/${VERSION}/download" \ + --output "${RUNNER_TEMP}/lexlean-public.crate"; then + test "$(sha256sum "${RUNNER_TEMP}/lexlean-public.crate" | cut -d' ' -f1)" = "$CRATE_SHA256" + echo "lexlean ${VERSION} is on crates.io with sha256 ${CRATE_SHA256}" + exit 0 + fi + sleep 2 + done + echo "::error::lexlean ${VERSION} did not become publicly downloadable" >&2 + exit 1 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index e454f25ec0..905e0d479b 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -13,9 +13,14 @@ # the container image: `ghcr.io//lexlean`, carrying the compiler and the # pinned Lean toolchain its `verify` command needs. The host binaries, the # packaged crate, the software bill of materials, the checksums, and the gate -# evidence are attached to the GitHub Release; the byte-identical verified -# crate is also published to crates.io through short-lived trusted-publisher -# credentials. +# evidence are attached to the GitHub Release. The crate is proved on every run +# (`crate.yml`: packaged to the same bytes twice, dry-run, checked against the +# checksum the release lists), and a tag uploads the byte-identical crate to +# crates.io only when a credential exists: a `CARGO_REGISTRY_TOKEN` secret in +# the crates.io environment for the owner's first upload, or trusted publishing +# once the owner has configured it (the repository variable +# CRATES_IO_TRUSTED_PUBLISHING). With neither, the release is created without +# the upload and says so (RP-18, #260). name: release on: @@ -81,6 +86,15 @@ jobs: echo "lexlean $workspace (rehearsal at ${GITHUB_SHA:0:7}; nothing is published)" fi + # The crate on crates.io is the crate this release attaches (#260): proved on + # every run, a rehearsal included, so a tag is not the first time it is tried. + crate: + name: crate readiness + needs: identity + uses: ./.github/workflows/crate.yml + with: + prerelease: false + # §30.3 CI evidence: the normative acceptance gate on the normative host, # from a clean checkout, naming the tagged commit. gate: @@ -260,13 +274,14 @@ jobs: # publish. This is the only job that writes to the repository. publish: name: publish the release - needs: [identity, gate, binaries, manifest] + needs: [identity, crate, gate, binaries, manifest] # Only a tag is a release. A manual run has already proved the gate, the # binaries, and the image by reaching here. - if: needs.identity.outputs.tagged == 'true' + if: needs.identity.outputs.tagged == 'true' environment: crates.io env: HAS_CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN != '' }} + TRUSTED_PUBLISHING: ${{ vars.CRATES_IO_TRUSTED_PUBLISHING == 'true' }} permissions: contents: write id-token: write @@ -358,11 +373,38 @@ jobs: run: tar -czf "release/lexlean-${VERSION}-binaries.tar.gz" -C release bin - name: Checksum every assembled file run: cargo xtask release-artifacts + # What cargo would send is what the release attaches and lists (#260): + # the dry run is cargo's own packaging of the upload, so equality here is + # equality of the bytes, and the crate job proved the same digest. + - name: The crate cargo would upload is the crate this release attaches + env: + VERSION: ${{ needs.identity.outputs.version }} + CRATE_SHA256: ${{ needs.crate.outputs.sha256 }} + shell: bash + run: | + set -euo pipefail + cargo publish --dry-run --locked --package lexlean --target-dir "${RUNNER_TEMP}/dry" + sha256="$(.github/crate-publication.sh identity release "${RUNNER_TEMP}/dry/package/lexlean-${VERSION}.crate")" + if [ "$sha256" != "$CRATE_SHA256" ]; then + echo "::error::the crate packaged here ($sha256) is not the one the crate job checked ($CRATE_SHA256)" + exit 1 + fi + echo "lexlean ${VERSION} sha256 ${sha256}" + - name: Decide how the upload is authorised + id: upload + shell: bash + run: echo "mode=$(.github/crate-publication.sh mode)" >> "$GITHUB_OUTPUT" - name: Acquire crates.io trusted-publisher token - if: env.HAS_CARGO_REGISTRY_TOKEN != 'true' + if: steps.upload.outputs.mode == 'trusted' uses: rust-lang/crates-io-auth-action@c6f97d42243bad5fab37ca0427f495c86d5b1a18 id: crates-auth + - name: No upload credential + if: steps.upload.outputs.mode == 'none' + env: + VERSION: ${{ needs.identity.outputs.version }} + run: echo "::notice::lexlean ${VERSION} was packaged and dry-run, and is on the GitHub release; no CARGO_REGISTRY_TOKEN and no trusted publishing, so it was not uploaded to crates.io" - name: Publish the exact verified crate to crates.io + if: steps.upload.outputs.mode != 'none' env: CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN || steps.crates-auth.outputs.token }} VERSION: ${{ needs.identity.outputs.version }} diff --git a/CHANGELOG.md b/CHANGELOG.md index e2e39dfe4b..2a66e40f97 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,8 @@ and Unreleased holds what has landed since. ## Unreleased +- The `lexlean` crate that goes to crates.io is the crate the release attaches (`RP-18`, #260). `.github/workflows/crate.yml`, which `release.yml` calls on every run, packages the crate twice to the same bytes, runs `cargo publish --dry-run`, checks the archive for what crates.io needs (description, license, repository, the readme it names, at most 10 MiB), and compares its SHA-256 with `release/lexlean.crate` and the line `checksums.txt` lists for it; the tag's `publish` job repeats the comparison against the dry-run package and uploads to crates.io only when a `CARGO_REGISTRY_TOKEN` secret or trusted publishing (the repository variable `CRATES_IO_TRUSTED_PUBLISHING`) authorises it, and otherwise creates the release and says the crate was not uploaded, where before the first run failed after the tag was pushed because no `lexlean` crate and no trusted publisher existed. Dispatched on a `release/vX.Y` line, `crate.yml` does the same for the pre-release `X.Y.0-dev.N`, `N` being the commit's number of first-parent commits, and uploads it under the same authority. The decisions are in `.github/crate-publication.sh`, which the case runs against planted archives, checksums, refs and environments. SPEC.md §30.3 states the rule. Register 449. + - The Rust runtime as source, #91 stage 4 (SPEC.md §17.16, §17.17, `SP-21`, `RB-15`, `SP-23`, `SM-35`, `SM-36`, `RB-16`, `SP-22`, `RB-17`, `SP-25`, `RB-19`). The declared Rust machine grows by the primitives the runtime is written in diff --git a/README.md b/README.md index 83e75038de..d900227a02 100644 --- a/README.md +++ b/README.md @@ -147,7 +147,7 @@ just vv # the complete normative acceptance gate (SPEC.md §9.2) just release # vv, then the §30 release criterion; refused until 1.0.0 ``` -All 448 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed. +All 449 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed. The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement. diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index a4e2fb26c5..7452fba3e5 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -760,7 +760,7 @@ pub(crate) fn run(id: &str) { let model = repo_model::Model::load(&root.join("model").into_std_path_buf()) .expect("the model loads"); let table = spec_table(); - assert_eq!(table.len(), 448, "§31 has 448 rows"); + assert_eq!(table.len(), 449, "§31 has 449 rows"); assert_eq!(model.ids.id.len(), table.len(), "register row count"); for ((spec_id, spec_suite, spec_statement), row) in table.iter().zip(model.ids.id.iter()) @@ -2196,7 +2196,9 @@ fn crate_publication_workflows(release: &str, crate_workflow: &str) -> Result<() for needle in needles { let at = position_of(text, needle, context)?; if at < previous { - return Err(format!("{context}: `{needle}` comes before the step it must follow")); + return Err(format!( + "{context}: `{needle}` comes before the step it must follow" + )); } previous = at; } @@ -2205,7 +2207,9 @@ fn crate_publication_workflows(release: &str, crate_workflow: &str) -> Result<() let uploads = |text: &str| -> usize { text.lines() .filter(|line| line.contains("cargo publish ") && !line.contains("--dry-run")) - .filter(|line| !line.trim_start().starts_with('#') && !line.trim_start().starts_with("echo")) + .filter(|line| { + !line.trim_start().starts_with('#') && !line.trim_start().starts_with("echo") + }) .count() }; @@ -2239,9 +2243,16 @@ fn crate_publication_workflows(release: &str, crate_workflow: &str) -> Result<() "cargo publish --locked --package lexlean", ], )?; - position_of(&publish, "needs.crate.outputs.sha256", "release.yml job `publish`")?; + position_of( + &publish, + "needs.crate.outputs.sha256", + "release.yml job `publish`", + )?; if uploads(&publish) != 1 { - return Err("release.yml job `publish` runs `cargo publish` without --dry-run other than once".to_owned()); + return Err( + "release.yml job `publish` runs `cargo publish` without --dry-run other than once" + .to_owned(), + ); } for guarded in [ "- name: Publish the exact verified crate to crates.io\n if: steps.upload.outputs.mode != 'none'\n", @@ -2294,7 +2305,10 @@ fn crate_publication_workflows(release: &str, crate_workflow: &str) -> Result<() ], )?; if uploads(&prerelease) != 1 { - return Err("crate.yml job `prerelease` runs `cargo publish` without --dry-run other than once".to_owned()); + return Err( + "crate.yml job `prerelease` runs `cargo publish` without --dry-run other than once" + .to_owned(), + ); } position_of( &prerelease, @@ -2340,24 +2354,40 @@ fn crate_publication_decisions() { for (environment, expected) in [ (vec![("HAS_CARGO_REGISTRY_TOKEN", "true")], "token"), ( - vec![("HAS_CARGO_REGISTRY_TOKEN", "true"), ("TRUSTED_PUBLISHING", "true")], + vec![ + ("HAS_CARGO_REGISTRY_TOKEN", "true"), + ("TRUSTED_PUBLISHING", "true"), + ], "token", ), (vec![("TRUSTED_PUBLISHING", "true")], "trusted"), ( - vec![("HAS_CARGO_REGISTRY_TOKEN", "false"), ("TRUSTED_PUBLISHING", "false")], + vec![ + ("HAS_CARGO_REGISTRY_TOKEN", "false"), + ("TRUSTED_PUBLISHING", "false"), + ], "none", ), (vec![("HAS_CARGO_REGISTRY_TOKEN", "")], "none"), (vec![], "none"), ] { let (status, out, _) = run(&["mode"], &environment); - assert_eq!((status, out.as_str()), (0, expected), "mode for {environment:?}"); + assert_eq!( + (status, out.as_str()), + (0, expected), + "mode for {environment:?}" + ); } // A commit of a release line is a development pre-release of its release. - assert_eq!(run(&["prerelease", "release/v0.4", "242"], &[]).1, "0.4.0-dev.242"); - assert_eq!(run(&["prerelease", "release/v12.3", "7"], &[]).1, "12.3.0-dev.7"); + assert_eq!( + run(&["prerelease", "release/v0.4", "242"], &[]).1, + "0.4.0-dev.242" + ); + assert_eq!( + run(&["prerelease", "release/v12.3", "7"], &[]).1, + "12.3.0-dev.7" + ); for (reference, count) in [ ("main", "242"), ("release/v0.4.1", "242"), @@ -2367,7 +2397,10 @@ fn crate_publication_decisions() { ("release/v0.4", "-1"), ] { let (status, _, error) = run(&["prerelease", reference, count], &[]); - assert_ne!(status, 0, "{reference} at {count:?} names no pre-release: {error}"); + assert_ne!( + status, 0, + "{reference} at {count:?} names no pre-release: {error}" + ); } // The workspace and its crates take the stamped version, and nothing else does. @@ -2375,11 +2408,21 @@ fn crate_publication_decisions() { let stamped = dir.join("stamped"); std::fs::create_dir(&stamped).expect("mkdir"); std::fs::write(stamped.join("Cargo.toml"), &manifest).expect("write"); - let (status, previous, error) = run(&["stamp", "0.4.0-dev.242", stamped.to_str().expect("utf8")], &[]); + let (status, previous, error) = run( + &["stamp", "0.4.0-dev.242", stamped.to_str().expect("utf8")], + &[], + ); assert_eq!(status, 0, "{error}"); let after = std::fs::read_to_string(stamped.join("Cargo.toml")).expect("read"); - assert_eq!(after.matches("0.4.0-dev.242").count(), 4, "the workspace and its three crates"); - assert!(!after.contains(&format!("version = \"{previous}\"")), "no version stays"); + assert_eq!( + after.matches("0.4.0-dev.242").count(), + 4, + "the workspace and its three crates" + ); + assert!( + !after.contains(&format!("version = \"{previous}\"")), + "no version stays" + ); assert_eq!( after.replace("0.4.0-dev.242", &previous), manifest, @@ -2387,12 +2430,18 @@ fn crate_publication_decisions() { ); for version in ["0.4", "v0.4.0", "0.4.0-rc.1", "latest", ""] { let (status, _, _) = run(&["stamp", version, stamped.to_str().expect("utf8")], &[]); - assert_ne!(status, 0, "{version:?} is no version a pre-release may take"); + assert_ne!( + status, 0, + "{version:?} is no version a pre-release may take" + ); } let bare = dir.join("bare"); std::fs::create_dir(&bare).expect("mkdir"); std::fs::write(bare.join("Cargo.toml"), "[workspace]\nmembers = []\n").expect("write"); - assert_ne!(run(&["stamp", "0.4.0-dev.1", bare.to_str().expect("utf8")], &[]).0, 0); + assert_ne!( + run(&["stamp", "0.4.0-dev.1", bare.to_str().expect("utf8")], &[]).0, + 0 + ); // The crate cargo would upload is the crate the release holds and lists. let release = dir.join("release"); @@ -2421,28 +2470,61 @@ fn crate_publication_decisions() { let packaged = dir.join("packaged.crate"); let release_arg = release.to_str().expect("utf8"); let packaged_arg = packaged.to_str().expect("utf8"); - let other_hash = format!("{}{}", if good.starts_with('0') { "1" } else { "0" }, &good[1..]); + let other_hash = format!( + "{}{}", + if good.starts_with('0') { "1" } else { "0" }, + &good[1..] + ); let mut altered = crate_bytes.clone(); altered[100] ^= 1; let cases: [(&str, Vec, String, bool); 6] = [ - ("the crate the release lists and holds", crate_bytes.clone(), format!("{good} lexlean.crate\n"), true), - ("a package one byte from the crate the release holds", altered.clone(), format!("{good} lexlean.crate\n"), false), - ("a checksum line of another digest", crate_bytes.clone(), format!("{other_hash} lexlean.crate\n"), false), - ("no line for the crate", crate_bytes.clone(), format!("{good} SPEC.md\n"), false), + ( + "the crate the release lists and holds", + crate_bytes.clone(), + format!("{good} lexlean.crate\n"), + true, + ), + ( + "a package one byte from the crate the release holds", + altered.clone(), + format!("{good} lexlean.crate\n"), + false, + ), + ( + "a checksum line of another digest", + crate_bytes.clone(), + format!("{other_hash} lexlean.crate\n"), + false, + ), + ( + "no line for the crate", + crate_bytes.clone(), + format!("{good} SPEC.md\n"), + false, + ), ( "two lines for the crate", crate_bytes.clone(), format!("{good} lexlean.crate\n{good} lexlean.crate\n"), false, ), - ("an empty checksum list", crate_bytes.clone(), String::new(), false), + ( + "an empty checksum list", + crate_bytes.clone(), + String::new(), + false, + ), ]; for (label, package, checksums, accepted) in cases { std::fs::write(&packaged, &package).expect("write"); std::fs::write(release.join("checksums.txt"), &checksums).expect("write"); let (status, out, error) = run(&["identity", release_arg, packaged_arg], &[]); if accepted { - assert_eq!((status, out.as_str()), (0, good.as_str()), "{label}: {error}"); + assert_eq!( + (status, out.as_str()), + (0, good.as_str()), + "{label}: {error}" + ); } else { assert_ne!(status, 0, "{label} is refused"); assert!(error.starts_with("identity:"), "{label}: {error}"); @@ -2450,15 +2532,31 @@ fn crate_publication_decisions() { } // The release without the crate, without its list, and without a package. std::fs::write(&packaged, &crate_bytes).expect("write"); - std::fs::write(release.join("checksums.txt"), format!("{good} lexlean.crate\n")).expect("write"); + std::fs::write( + release.join("checksums.txt"), + format!("{good} lexlean.crate\n"), + ) + .expect("write"); for missing in ["lexlean.crate", "checksums.txt"] { let kept = std::fs::read(release.join(missing)).expect("read"); std::fs::remove_file(release.join(missing)).expect("remove"); - assert_ne!(run(&["identity", release_arg, packaged_arg], &[]).0, 0, "{missing} is missing"); + assert_ne!( + run(&["identity", release_arg, packaged_arg], &[]).0, + 0, + "{missing} is missing" + ); std::fs::write(release.join(missing), kept).expect("restore"); } assert_ne!( - run(&["identity", release_arg, dir.join("absent.crate").to_str().expect("utf8")], &[]).0, + run( + &[ + "identity", + release_arg, + dir.join("absent.crate").to_str().expect("utf8") + ], + &[] + ) + .0, 0, "no package" ); @@ -2479,7 +2577,11 @@ fn crate_publication_decisions() { let path = dir.join(format!("{name}.crate")); let status = Command::new("tar") .current_dir(dir) - .args(["-czf", path.to_str().expect("utf8"), &format!("{name}-1.0.0")]) + .args([ + "-czf", + path.to_str().expect("utf8"), + &format!("{name}-1.0.0"), + ]) .status() .expect("tar runs"); assert!(status.success()); @@ -2514,11 +2616,31 @@ fn crate_publication_decisions() { let mut oversize = readme.clone(); oversize.push(("padding.bin", large)); for (label, path, says) in [ - ("no description", archive("nodescription", &without("description"), &readme), "no `description`"), - ("no license", archive("nolicense", &without("license"), &readme), "neither `license` nor `license-file`"), - ("no repository", archive("norepository", &without("repository"), &readme), "no `repository`"), - ("a readme it lacks", archive("noreadme", &complete, &[]), "names a file the archive does not carry"), - ("more than 10 MiB", archive("oversize", &complete, &oversize), "exceeds the crates.io limit"), + ( + "no description", + archive("nodescription", &without("description"), &readme), + "no `description`", + ), + ( + "no license", + archive("nolicense", &without("license"), &readme), + "neither `license` nor `license-file`", + ), + ( + "no repository", + archive("norepository", &without("repository"), &readme), + "no `repository`", + ), + ( + "a readme it lacks", + archive("noreadme", &complete, &[]), + "names a file the archive does not carry", + ), + ( + "more than 10 MiB", + archive("oversize", &complete, &oversize), + "exceeds the crates.io limit", + ), ] { let (status, _, error) = run(&["metadata", &path], &[]); assert_ne!(status, 0, "{label} is refused"); @@ -2540,7 +2662,8 @@ fn rp_18() { assert!(text.contains(from), "the plant `{from}` is in the workflow"); text.replacen(from, to, 1) }; - let publish_dry_run = "cargo publish --dry-run --locked --package lexlean --target-dir \"${RUNNER_TEMP}/dry\""; + let publish_dry_run = + "cargo publish --dry-run --locked --package lexlean --target-dir \"${RUNNER_TEMP}/dry\""; let release_plants: Vec<(&str, String)> = vec![ ( "a tag that does not wait for the crate job", diff --git a/xtask/src/spec_links.rs b/xtask/src/spec_links.rs index 9ee47a38f5..464ddf38b8 100644 --- a/xtask/src/spec_links.rs +++ b/xtask/src/spec_links.rs @@ -61,8 +61,8 @@ fn parse_table(spec: &str) -> Result, Fail> { pub fn validate(root: &Path) -> Result<(), Fail> { let spec = std::fs::read_to_string(root.join("SPEC.md"))?; let rows = parse_table(&spec)?; - if rows.len() != 448 { - return Err(format!("RP-07: the §31 table has {} rows, not 448", rows.len()).into()); + if rows.len() != 449 { + return Err(format!("RP-07: the §31 table has {} rows, not 449", rows.len()).into()); } // The prose total under the table is part of the contract a reader // relies on; a row added without it would leave §31 contradicting itself. From ea09920190c7ecf0c664bef5c01e241050347dd4 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 14:28:00 +0100 Subject: [PATCH 3/4] [0.4] #260 RP-18: record the planted defects in VERIFICATION.md Co-Authored-By: Claude Sonnet 5.5 --- VERIFICATION.md | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/VERIFICATION.md b/VERIFICATION.md index aa4fca819c..b1c201da53 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -11149,3 +11149,50 @@ pins [] The plant was restored with `git checkout`. The same verification with the fix in place is the regeneration of the bootstrap records in this change. + +## Planted defects for the crate that goes to crates.io (`RP-18`, #260) + +`conformance_rp_18` reads `.github/workflows/release.yml` and +`.github/workflows/crate.yml`, requires the order of their steps (package twice +and compare, dry-run, archive metadata, identity, then credential, then the one +upload), and runs `.github/crate-publication.sh` against planted archives, +checksum lists, refs and environments. It plants nine changes in `release.yml` +and eight in `crate.yml` in memory, and each must be refused. Each case below was +also planted in the committed tree, one at a time, with the real test, on Linux +x86-64 (WSL, Rust 1.97.1), and the file restored with `git checkout` +(§27.9). The skeleton commit, with the workflows and script set aside, fails: +`.github/workflows/crate.yml: No such file or directory`. + +| Case | Command | Observed | +| --- | --- | --- | +| the committed tree | `cargo test -p repo-conformance --test conformance conformance_rp_18 -- --exact` | ok | +| the upload step loses its `if: steps.upload.outputs.mode != 'none'` | same | ``release.yml job `publish` has no `if: steps.upload.outputs.mode != 'none'` `` | +| the tag does not run `cargo publish --dry-run` | same | ``release.yml job `publish` has no `cargo publish --dry-run --locked --package lexlean` `` | +| the readiness job does not compare its two packagings | same | ``crate.yml job `readiness` has no `cmp "$a/package/$crate" "$b/package/$crate"` `` | +| `identity` ignores the digest `checksums.txt` lists | same | `a checksum line of another digest is refused` failed | +| `mode` answers `token` when no credential exists | same | `mode for [("HAS_CARGO_REGISTRY_TOKEN", "false"), ("TRUSTED_PUBLISHING", "false")]` failed | +| a pre-release named `X.Y.0-rc.N` | same | `left: "0.4.0-rc.242"` | +| the 10 MiB limit lifted | same | `more than 10 MiB is refused` failed | + +The script, run by hand on the crate of PrismPM's vendored copy: a package one +byte from the released one gives `identity: cargo would upload a05cb178…, and +the release attaches lexlean.crate 6d235250…` (exit 1); a checksum list naming +another digest gives `identity: … checksums.txt lists 0d235250… for +lexlean.crate` (exit 1); `prerelease main 242` gives `prerelease: main is not a +release line (release/vX.Y)`; `stamp 0.4` gives `stamp: 0.4 is not a SemVer +version`. + +The pre-release path was rehearsed on a throwaway worktree of this branch: +`crate-publication.sh prepare true` on `release/v0.4` printed `0.4.0-dev.243` +and rewrote the four versions of the root `Cargo.toml` and the matching lock +entries; two `cargo package --locked --allow-dirty` runs gave byte-identical +5.0 MiB archives, `cargo publish --dry-run` ended with "aborting upload due to +dry run", the metadata check passed, and `.cargo_vcs_info.json` named the commit +with `"dirty": true`. + +*What the evidence is.* The case reads text and runs a script; it cannot show +that GitHub runs the workflows as written. Neither workflow has run on GitHub, +so the call of `crate.yml` from `release.yml`, `cargo xtask release-artifacts` +in a clean checkout of the called workflow, and the `--allow-dirty` pre-release +packaging are first exercised by the first rehearsal or dispatch. No upload was +attempted and no token was requested or stored. From 6802d705b9647b795c4920bf99f0b0182e746e92 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 16:51:44 +0100 Subject: [PATCH 4/4] [0.4] #260 RP-18: the README range of the repository suite ends at RP-18 RP-11 reads the range against the register: RP-17 is #288 on release/v0.5, so on this line the last RP ID is RP-18. Co-Authored-By: Claude Sonnet 5.5 --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d900227a02..1aac8a134c 100644 --- a/README.md +++ b/README.md @@ -161,7 +161,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row, | Capability | IDs | Level | | --- | --- | --- | -| Exact repository identity, layout, generated documents, release gate, total classification of every closed enum by every consumer, and the devcontainer pinned to the toolchains | `RP-01`..`RP-16` | `build` | +| Exact repository identity, layout, generated documents, release gate, total classification of every closed enum by every consumer, and the devcontainer pinned to the toolchains | `RP-01`..`RP-18` | `build` | | Closed project configuration, canonical lock file, and offline dependency policy | `CF-01`..`CF-18` | `build` | | Total lexical closure: every accepted atom is covered by exactly one declared origin | `LX-01`..`LX-14` | `build` | | Versioned lexicon packages with closed schemas, denotations, and renderer tokens | `GL-01`..`GL-18` | `build` |