ci: verify UOR Atlas as the parts of one run (#131)

[humuhumu33]

Part of #131: steps 2 and 3 of the order agreed there, for UOR Atlas. #131 stays open for the bdd certificates partition (the second PR, as said on #131) and for step 1, slimming Census/CensusCert4.

Step 2 of the order agreed on #131, for UOR Atlas, with step 3: the examples leg verifies every example but Atlas, and Atlas is verified as the parts of one run, from a committed plan, with every process still run exactly once and the join publishing what the whole verification publishes. §9.4's sentence on caches is unchanged, and no attestation or proof result crosses a run.

What changes

• Verifier (crates/lexlean/src/verify/partition.rs, verify::run_part, lexlean::verify_part): a verification runs as Part::Whole (unchanged), Part::Shard (the plan's elaborations, replays, and audit members, with the .olean files of the shards it needs, written to an output directory, nothing published), or Part::Join (its own plan, every other part's records judged as their stages judge their own, then policy, the attestation over the records in the canonical order of §22.11, publication). A module without a record from any part, a record no module owns, a duplicate .olean or record, and a shard whose plan elaborates a module before its imports are refused. Defined for projects without production roots and without PDF.
• Plan (.github/verify-shards.json, cargo xtask ci-shards, repo_conformance::shards): fourteen shards and a join over Atlas's import graph, read from the committed generated Lean (public import lines). Checked: every module elaborated by exactly one shard and replayed by exactly one; every import of a module a shard elaborates or replays is elaborated by that shard or one it needs; join needs every other shard.
• cargo xtask verify-examples runs the part LEXLEAN_EXAMPLES_PART names (without:<example>, shard:<example>:<shard>, join:<example>; unset, the recipe is unchanged), exchanging parts through LEXLEAN_EXAMPLES_PARTS.
• ci.yml: the examples leg at without:uor-atlas; Atlas jobs atlas-prefix → atlas-l1 (cert4, census-a..d) → atlas-closure, atlas-cert4-replay → atlas-l3 (orbit, pairs-a..d) → atlas-join, each a clean checkout on ubuntu-24.04 at the examples profile. The prefix job builds the gate's executable once; the other jobs take it and the shards' output from the run (pattern: atlas-*, never a run-id). The Atlas jobs run after their needs and not while a pull request is a draft; ready_for_review reruns them.
• SPEC §9.4, §22.11; RP-14 rewritten; VR-23 new (the join of shards of peano-arithmetic equals its whole verification byte for byte with the same attestation ID, and the three refusals). Register 381 → 382. CHANGELOG, VERIFICATION.md (narrative and plants).

What does not change

just vv, its twelve recipes and their order, release.yml (runs just vv whole, Atlas at width 1), the verifier's behaviour as Part::Whole, every example's expected/verify, the compiler-semantics IDs.

Measured on this PR's first run (38870906361, head df2f6bb)

Side	Wall time
Atlas, prefix start to join end	83 min (08:01:16 → 09:24:35 UTC)
examples leg (every example but Atlas)	15 min
rest leg	85 min
main at 514e95a, examples leg, for comparison	178 min

Critical path as run: prefix 22 min → cert4 28 → closure 6 → pairs-* ≤ 14 → join 2.5, with cert4-replay (31 min) the branch the join waited on. The join published Atlas and found its 267 normalized records equal to expected/verify. The rest leg is now the longer side; bdd's certificates partition is the next PR. That run's rest and host legs failed on two cases of this PR, fixed in the follow-up commits (CL-13: verify_part left the Engine impl; RP-11: the README's VR range).

Expected effect, before the measurement

On main at 514e95ad the examples leg took 178 min (Atlas 156). The critical path of the partition is prefix (23 min of elaboration) → cert4 (22) → closure (3) → pairs-* (11) → join (2) plus per-job set-up (Lean toolchain; the Rust build once), estimated at 80 to 90 minutes for the Atlas side, after which the rest leg (76 min) is the longer one. Runner-minutes rise (14 Atlas jobs). This PR's own CI run is the measurement; the numbers will be posted here when it lands.

Local verification (WSL, pinned toolchains)

cargo test -p lexlean --lib, cargo fmt --check, cargo clippy -D warnings, cargo xtask validate-model, validate-spec-links, check-test-inventory, ci-shards, cargo test -p repo-conformance --test bdd, and conformance_rp_14, conformance_rp_05, conformance_vr_21..23 pass; an end-to-end run of verify-examples as two shards and a join of peano-arithmetic through the plan file publishes records equal to the committed expected/verify.

Not done here: the bdd certificates partition (second PR, as said on #131) and step 1 (slimming Census/CensusCert4).

🤖 Generated with Claude Code

---

Generated by Claude Code

[afflom]

Merged as 2a3c6f7d (merge commit), on the tested head 55583ba7, which already contained main 32afe5da (#144); all 22 checks of run 38905653756 are green.

What the run measured (the numbers this PR promised to post):

Side	Wall time
Atlas, prefix start to join end	95.9 min (13:09:07 → 14:45:00Z)
rest leg	111.5 min (13:09:07 → 15:00:37Z)
examples leg (every example but Atlas)	23.4 min
Intel macOS host leg	64 min
main at 514e95ad, examples leg	178 min

The gate is now the rest leg, 111.5 min against 178 for the old examples leg (−37%). The estimate for the Atlas side was 80 to 90 minutes and the first run measured 83; this run took 96, because cert4 took 36 minutes (28 on the first run) and cert4-replay 28. So the estimate holds in kind and not to the minute, and the next gain is the rest leg (bdd's certificates stage), as the PR says. The join published Atlas with attestation fa0885f9… and found its 267 normalized records equal to expected/verify.

Review. Read and sound: verify::partition and the join's judging of imported records, the SPEC §9.4 and §22.11 text, RP-14 and VR-23 and their plants, the job graph (the Atlas jobs run on every push to main and on non-draft pull requests; needs is complete). One hardening, not a blocker, for your next PR on this code (the bdd partition): the join judges an imported elaboration, replay or audit record by exit code and silence, but does not compare its executable_sha256 with the join's own toolchain digests (lean for elaboration and audit, leanchecker for replay). In a whole run that holds by construction; across jobs it holds because every job installs the same pinned toolchain, which is a practice and not a check. The comparison is a few lines and one plant.

I changed the description's Closes #131 to Part of #131, because #131 still has the bdd partition and step 1 open; nothing else in the PR was touched.

---

Generated by Claude Code