ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131)

[humuhumu33]

Part of #131: the second PR of step 2, as posted on #131. It partitions the rest leg's bdd recipe across rows of the gate's matrix, and adds the hardening @afflom asked for in the merge comment on #152. #131 stays open for step 1, slimming Census and CensusCert4.

1. The join checks the toolchain of what it imports (7b377f9)

Where the join imports another part's records (partition::import), it now requires each record's executable_sha256 to be the join's own digest of the tool that produced it. That is lean for an elaboration or an audit member, and leanchecker for a replay (partition::check_toolchain). A mismatch is LLI9001, naming the record and both digests. The check sits at the one point all three record kinds enter, so the assembly before the attestation and the imported-audit loop only ever see checked records.

• VR-23 gains the refusal. It rewrites the second shard's replay record of a module to another digest and expects LLI9001 with both digests. The statement moves alike in SPEC §31, model/ids.toml, and the feature.
• SPEC §9.4 and §22.11 say what the join requires.
• Plant. With the call removed, conformance_vr_23 fails at its refusal: the join accepted the other leanchecker's record and published. It is recorded in VERIFICATION.md's "the partition can fail" list.

2. bdd as the parts of one run (cfa02f4)

On the run that merged #152 (38905653756), the rest leg took 111.5 min. bdd was 95.7 min of it: one test process whose cases sum to 22,708 s over four threads.

Part	Cases	Shared fixtures	Case seconds on that run
preservation	13	reports (four projects certified), shipped, certification library	6,890
compiler	21	verified_compiler, verified_reasoning, planted calculus verification	5,558
production	39	production export, verified_models, and EX-07	4,595
verification	91	verified, broken_proof, the oracle	4,089
rest (remainder)	223, plus the library and meta-gate tests		1,563

• Plan. .github/bdd-parts.json names the four parts by conformance ID. The remainder names none and runs every test no part names, so a new ID lands there with no plan change.
• Recipe. bdd is now cargo xtask bdd. With LEXLEAN_BDD_PART unset or empty, as in just vv and release.yml, it runs cargo test -p repo-conformance --all-features exactly as before. With a part named, it adds harness filters: --exact and the part's tests, or --exact plus a --skip of every named test for the remainder. On this toolchain --exact also makes --skip exact. The harness selects the tests; no case decides whether it runs.
• Proof (RP-13). check-test-inventory lists every part with its filters. It requires the parts to be disjoint, their union to equal bdd's list, and every named test to be in its part. Here it reads: "the 5 parts … (compiler 21, preservation 13, production 39, verification 91, rest 261) are the 425 of bdd, each in one part".
• ci.yml (RP-14). Each named part runs on a bdd-<part> row of the vv matrix, and the remainder on the rest leg. RP-14 requires every part on exactly one row, a part named exactly when a row runs bdd, the variable set once from the row, and every other recipe still once. There is no cache and no artifact; each row builds from its own clean checkout.
• Docs. SPEC §9.2 (the bdd table line and the inventory prose) and §9.4 are reworded. The RP-13 and RP-14 statements change in §31, ids.toml, and the feature, and CONFORMANCE.md is regenerated. VERIFICATION.md has the measurement, the grouping method, the mechanism, and eight plants, each caught. CHANGELOG has entries for both commits. No normative text has a time target, and the register stays at 387.

Fixtures built in more than one part. The preservation and certification environments are built in both preservation and compiler: GC-02 needs them beside verified_compiler, and moving it would verify the compiler project twice instead. Host-only fixtures (GNAF requests and pairs, certificate fixtures, native registry), the SPEC text, and axioms_insufficient are cheap.

Estimate, not a measurement: each bdd row takes about 24 to 36 min, bound by preservation and by EX-07, which takes 29 min alone. The rest leg should take about 22 min. The Atlas side (83 to 96 min) then becomes the gate's pole. This PR's first green run is the measurement, posted below.

Local verification (WSL, pinned toolchains)

These pass: cargo fmt --check, cargo clippy --workspace --all-targets --all-features -D warnings, cargo xtask validate-model, validate-spec-links, and check-test-inventory. So do cargo test -p repo-conformance --test bdd, --lib, and cargo test -p xtask. On the conformance target, conformance_rp_01..14 and conformance_vr_23 pass, and the verify::partition unit tests pass.

Left to CI: the long legs (test, golden, repro, examples, Atlas) and the four bdd part rows.

🤖 Generated with Claude Code

[humuhumu33]

Measured on this PR's first run (38945603499, head cfa02f41, all 26 checks green). The baseline is the run that merged #152 (38905653756). Each job is timed from its own start to its own end, so time spent waiting for a runner is excluded.

Job	This run	Its bdd recipe	Baseline
rest leg, its ten other recipes plus the rest part	23.0 min	450 s	111.5 min (bdd 5,741 s)
bdd-preservation	31.2 min	1,825 s
bdd-production	28.4 min	1,656 s
bdd-compiler	21.7 min	1,255 s
bdd-verification	15.8 min	901 s

• The rest side. The longest job doing what the rest leg used to do is now 31.2 min (bdd-preservation), against 111.5. That is in line with the estimate in the description: 22 min for the leg, 24 to 36 for the rows. bdd-production is bound by EX-07, which took 1,592 s alone.
• No fixture was paid twice in any material way. The cases' summed wall time across the five parts is 22,335 s, against 22,708 s for the one process on the baseline. The bdd recipes sum to 6,087 s, against 5,741.
• Runner-minutes. The rest side rose from 111.5 to 120.1 job-minutes (+8.6), which is the four extra checkouts and builds. The whole run took 465 job-minutes against 507 on the baseline. The rest of the difference comes from other jobs' own variance (examples 17 against 23 min, the host matrix 130 against 160), not from this change.
• The gate's wall time on this run was set by runner queueing, not by work. Most jobs waited 20 to 70 minutes for a runner. The Atlas side ran from 19:01 to 20:59, with waits between its jobs. The bdd rows were all done by 20:01. With runners free, the pole is now the Atlas side (83 to 96 min of work on ci: verify UOR Atlas as the parts of one run (#131) #152's runs), as expected.

---

Generated by Claude Code

[afflom]

@humuhumu33, #146 is merged: main is 097b9b97, a merge commit whose tree is 3b25b10a7 (22 of 22 green). This PR's head 085b65a5 lacks it, so it needs main merged once more before it can land.

• The merge is not mechanical in one file this PR and feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 both edit: crates/lexlean/src/verify/mod.rs (your check_toolchain call in run_part; feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146's changes are in the staging path). Also crates/conformance/src/cases/repository.rs, model/ids.toml, SPEC.md, CONFORMANCE.md (regenerate), VERIFICATION.md and CHANGELOG.md. The register is 392; this PR adds none.
• Your run on 085b65a5 (38969781688) tests main without feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146, so it will not be the run that lands; the new push cancels it. Better to push the merge soon than to wait for it.
• Then I give the formal approving review on the green head that contains main. The design had no blocker from me (see my comment on Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4) #131); what I check on the final head is that the RP-13 and RP-14 cases and the four bdd-* rows are green and that check-test-inventory reads the parts' counts from the combined tree.

---

Generated by Claude Code

[humuhumu33]

@afflom, main 097b9b97 (#146) is merged into this branch as 1c04cf36 and pushed. CI is running on that head.

• crates/lexlean/src/verify/mod.rs merged without a conflict. Against main, its only change is this PR's partition::check_toolchain call right after partition::import in run_part, and feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146's staging changes are unchanged. The verify::partition unit tests and conformance_vr_23 pass on the combined tree.
• SP-14 is new in feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 and reaches preservation::shipped, so it is named in the preservation part. Left to the remainder, it would build that environment a third time. That is the one change to .github/bdd-parts.json.
• check-test-inventory on the combined tree: "the 5 parts of .github/bdd-parts.json (compiler 21, preservation 14, production 39, verification 91, rest 265) are the 430 of bdd, each in one part (RP-13)". VERIFICATION.md's counts now say the same.
• The rest, locally: CHANGELOG keeps both entries, CONFORMANCE.md is regenerated (392 IDs), and these pass: fmt, clippy, validate-model, validate-spec-links, the meta-gate target, and conformance_rp_01..14. The register is 392, and this PR adds no ID.

---

🤖 Addressed by Claude Code

[afflom]

Approved at 1c04cf36, as a non-author, on the head that ran.

CI. Run 38980348859: all 26 checks green (host legs, examples, rest, the four bdd-* rows, the 14 Atlas jobs, repro, honesty). The head contains main 097b9b97 (#146), which is still main's tip. Main's own push run on 097b9b97 is also green.

What I read.

• The join checks the toolchain of what it imports (partition::check_toolchain, called at the one point where all three record kinds enter, LLI9001 naming the record and both digests): the VR-23 case plants a replay record of another leanchecker and the join refuses it; the plant is in VERIFICATION.md. This is the hardening I asked for on #152.
• bdd as the parts of one run. .github/bdd-parts.json names four parts by conformance ID and one remainder that runs every test no part names, so a new ID lands in rest with no plan change. cargo xtask bdd with LEXLEAN_BDD_PART unset or empty is the command it always was. compare_parts proves from the harness's own --list that the parts are disjoint and their union is bdd; RP-13 plants a test two parts run and a test none runs; RP-14 requires every part on exactly one matrix row and every other recipe still once. No normative text carries a time target.
• Measured, not estimated. Its first run's job times (mine from the API agree with the PR's table): the rest leg 23.0 min against 111.5, the four rows 15.8 to 31.2 min, the rest side's job-minutes 120 against 114. The cost is about 6 runner-minutes; the longest path of a ready run is now the Atlas side.

Not blocking, for the record. The first commit of the part (7b377f92, then cfa02f41) is a fix and then a CI change; the register rows (RP-13, RP-14, VR-23) change statements only, so there is no new-row R3 order to read.

Merging with a merge commit pinned to this head.

---

Generated by Claude Code