[humuhumu33]

What

Every bdd part that runs a bootstrap case exported the bootstrap project itself, which verifies it whole. In run 43046966603 that verification shows in 19 jobs (18 bdd-bootstrap-* parts and bdd-compiler) at 1,173-2,205 s each, about 569 runner-minutes per gate, and it grows by one per slice (27 parts after the BS-25..34 batch).

This PR exports it once per run:

• New job bootstrap export (after honesty, whole-gate runs only, width 2, committed hints, 12 GiB budget). It runs the new cargo xtask export-bootstrap --output DIR, which exports, requires every package to equal the committed package (the comparison PX-01 and BS-01/BS-03 make), and writes the bundle plus custody.json (lexlean/ci-bootstrap-export/1). The record binds repository, run id, attempt, commit, tree, SHA-256 of rust-toolchain.toml/lean-toolchain/Cargo.lock, rustc -vV and lean --version, the bundle path, and the bundle digest.
• The legs do not wait for that job. In a whole-gate run each leg starts .github/scripts/take-bootstrap-export.sh, which makes no API call until a case first wants the export, then downloads this run's bootstrap-export artifact (or records that the export job ended without it). So each part's differential runs in parallel with the one export.
• production_export::exported("bootstrap") reads it when LEXLEAN_BOOTSTRAP_EXPORT names a directory. Before any case reads it, the record must match the job's own repository, run, commit, tree, pins and toolchains, and the bundle's digest, with an attempt at most the job's and a path below the project. The bundle is also replayed. When the variable is unset (just vv, draft runs), the case exports itself as before.
• SPEC.md §9.4: a paragraph on the same-run transfer; the export job joins the jobs that require honesty.
• RP-14: the job, the legs' fetcher and the custody check are checked against planted changes: missing honesty, another width, another artifact name, another run, no actions: read, an unconditional fetch, and each custody field changed.

Measurement

Full-gate dispatch 43127877709 on 3da2bd3 (release 7eb8162 + this change): all jobs passed. The branch has since merged release/v0.4 5dccf9e (#469); the only conflict was CHANGELOG.md, and the RP cases, validate-model and validate-spec-links pass on the merge.

Done criterion: in all 18 bdd-bootstrap-* parts and in bdd-compiler (BS-01/BS-03), the telemetry shows no bootstrap verification. In 43046966603 each showed one, of 1,173-2,205 s. The bootstrap export job verified it once: 1,966 s, 36.2 min for the whole job. Its line: the bootstrap project exported once for run 43127877709 attempt 1 ...; its packages equal the committed packages (§24.7); bundle sha256 36b0f6e0... (337 files).

This branch does not contain #470 (parallel evaluator), so 42946701043 is the like-for-like baseline for the differential-heavy parts; 43046966603 is the brief's baseline.

Job	42946701043 (no #470)	43046966603 (#470)	43127877709 (this PR)
host (x86_64-pc-windows-msvc)	106.1	126.0	124.4
(bdd-bootstrap-package)	145.3	100.8	121.2
(rest)	70.7	45.3	72.9
(examples)	53.0	85.2	68.1
(bdd-bootstrap-tooling-latex)	113.2	60.9	66.4
(bdd-bootstrap-check)	97.6	73.3	52.5
(bdd-compiler)	42.0	45.0	39.2
(bdd-bootstrap-moves)	39.1	39.3	37.1
(bdd-bootstrap-print)	60.6	53.3	37.1
(bdd-bootstrap-succeed)	30.7	32.7	37.0
(bdd-bootstrap-surface-lex)	34.8	42.2	37.0
(bdd-bootstrap-surface-doc)	47.0	49.5	36.9
(bdd-bootstrap-bodies)	25.0	24.2	36.9
(bdd-bootstrap-runtime)	33.2	24.6	36.9
(bdd-bootstrap-assemble)	49.4	51.3	36.8
(bdd-bootstrap-gnaf)	37.1	36.6	36.8
(bdd-bootstrap-validate)	52.0	56.6	36.8
(bdd-bootstrap-lower)	61.7	78.6	36.7
(bdd-bootstrap-terms)	35.7	37.0	36.2
bootstrap export	n/a	n/a	36.2
(bdd-bootstrap-surface-generic)	34.1	41.6	34.6
(bdd-bootstrap-structural-grammar)	45.3	57.6	33.2
(bdd-bootstrap-loops)	40.0	32.4	31.6
sum of the 18 bootstrap parts	982	892	782 (+36 export)

Whole run:

	42946701043	43046966603	43127877709
wall (created to last job)	149.6 min	133.4 min	128.2 min
Linux runner-min	1,550	1,485	1,384
macOS runner-min	289	297	306
Windows runner-min	106	126	124
$ per gate (Linux $0.006, macOS $0.062, Windows $0.012 assumed)	$28.48	$28.81	$28.75

What this shows:

• The bootstrap parts' floor is now the export job (36 min). Fifteen of the 18 parts finished between 01:11:37 and 01:12:10, within a minute of the export arriving (01:11:13). Short parts that took 24-33 min before now take about 37: they finish their differential and wait. Long parts got shorter: BS-07 78.6→36.7, BS-05 56.6→36.8, BS-14 51.3→36.8, BS-04 73.3→52.5, BS-21 57.6→33.2; BS-15 145.3→121.2 and BS-20 113.2→66.4 against the no-conformance: the BS evaluator differential runs on every processor #470 run.
• Wall clock is unchanged in substance (128 min), because the Windows host job (124 min) is the longest job; ci: run the Windows host's tests as five lanes (SPEC.md §8.3) #477 splits it. With conformance: the BS evaluator differential runs on every processor #470 and this PR together, BS-15 should land near 100.8 - 32 ≈ 69 min.
• Cost moves little: Linux -101 runner-min against 43046966603 and -166 against 42946701043, about -$0.6 to -$1.0 per gate. Parts that wait for the export bill the wait, and the export job costs 36 min.
• Next lever: the export's certificate stage, 1,397 s of its 1,966. In crates/lexlean/src/verify/mod.rs (for file in &stage.certificates) each certificate is compiled and replayed one after another, so LEXLEAN_VERIFY_WIDTH=2 does not apply; the job never went below 10.8 GB free. Running those certificates through the verifier's pool would lower the floor for every short part and turn their wait into saved minutes. That is a verifier change and is not part of this PR.

Queueing: the export job and the legs are created together when honesty passes, and the export job comes first in the file. A leg waits only once a case asks for the export, so it holds a runner while waiting only if the export job is still queued; under FIFO assignment the export job is queued no later than the legs that wait on it.

Not verified

• A rerun of failed jobs in a later attempt (custody accepts an attempt at most the job's own); covered by the RP-14 plant, not by a real rerun.
• The fetcher's failure path (the export job failing) in CI; covered by the script's failed marker and the harness's refusal, not exercised by a run.

Not verified locally

The export job and the cross-job transfer only run in CI; the dispatch above is their first run. Locally: fmt, clippy (repo-conformance, xtask), validate-model, validate-spec-links, all 17 RP cases.

🤖 Generated with Claude Code

[afflom]

[P2] Preserve the shared environment guard in the new bootstrap consumer. At this exact head, production_export::exported() takes the bootstrap shortcut directly into export_custody::take(), bypassing export()'s support::env_shared(). take() then runs git status/rev-parse, tool-version resolution and verify_artifact without that guard. The parallel production harness also runs PX-08/PX-10/CL-23 through offline(), which holds with_env's exclusive lock while putting a failing git sentinel first on PATH. The new unguarded consumer can enter that legitimate window, falsely reject custody and trip the offline sentinel assertion. This is a source-backed reachable race, not a claimed observed CI failure.

The small fix is to use the existing shared guard for the consumer's identity/tool-resolution/replay interval, after the asynchronous wait and environment-independent bundle digest. Do not hold it across the potentially long artifact wait or wrap the whole exported() initializer: the fallback already takes this guard, and lock ordering must remain intact. No competing patch or new full-gate run is requested.

The remainder of this bounded review found no demonstrated acceptance bypass in the inspected custody/hash/path/replay and same-run attempt checks. Full manual43127877709 is still incomplete; its bootstrap export job is active. Keep that evidence distinct from the draft-event skips. The reported historical export cost is not yet measured savings from this implementation. Existing owner retains repair, transfer qualification and landing; this is not full acceptance or completion of the broader #468 factory work.

[afflom]

Bounded current-release delta review: 8ab6fe6 has ordered parents [3da2bd3, actual5dcc]. The bootstrap custody/consumer code is unchanged, so the narrow env_shared finding in review5867372298 remains unresolved. The minimum next source step is still the existing shared guard around identity/tool resolution and replay after the asynchronous wait and environment-independent digest; do not hold it across the long wait or recursively wrap the fallback exporter.

The original3da manual CI43127877709 now completed SUCCESS:55/55 jobs and611/611 reported steps, including same-run honesty; exact3da repro43127931880 passed. This is useful positive transfer execution evidence for that head, not proof that the scheduling-dependent race is absent or qualification of8ab. Current8ab draft CI skips bootstrap export and other required groups; its repro passed. No completed producer, test or log was repeated by this review. Existing owner retains repair and resulting-head qualification.