Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4)

@afflom

What every PR run proves today, and what it costs

Every pull request re-elaborates and kernel-replays the UOR Atlas example from a clean checkout, because §9.4 says the gate has "no cache of a build directory, object, verification tree, attestation, or proof result". The latest green run of main (run 38716449420, commit 514e95a) measured it; the numbers are from its acceptance-gate-evidence-examples and -rest artifacts:

Item	Wall time
`examples` leg	178.1 min
of which `uor-atlas` verify (elaboration 5047 s, replay 4286 s)	155.7 min
of which CensusCert4 + Census, elaboration and replay	78.1 min
`rest` leg (`bdd` 64.0 min; `certificates` stage 3727 s of 4563 s)	76.1 min
`golden`, which checks Atlas's 331 published artifacts against their oracles	44 s

examples/uor-atlas last changed on 2026-09-09 (b91c4fd) and lean-toolchain on 2026-10-08 (dd5d2e1). None of the last 25 merged pull requests (#46 to #129) touched either. Of the last 60 PR runs of ci.yml, 19 were cancelled by a new push to the same branch, so a third of the gate's hours produced no verdict, and every fix pushed during review costs three more hours.

The gate already holds the fact that makes the re-proof redundant. golden compares the generated Lean of every example, Atlas included, byte for byte with expected/build (check_golden in xtask/src/main.rs, §28.3). All 66 Atlas modules import only Lean, so the pinned toolchain is their whole import closure. Elaboration (§22.3) and leanchecker replay (§22.4) are functions of those bytes and that toolchain, and §22.11 and §29.5 already rest on that determinism. A PR whose generated Atlas is the bytes main verified, on the toolchain main verified them with, learns nothing from 156 minutes that golden did not establish in 44 seconds.

Proposal

Main's push run and release.yml keep the full, unconditional gate exactly as §9.4 specifies. After examples passes on main, the job publishes the Atlas attestation (attestation.json, §22.9: manifest hash, the lean, lake and leanchecker executable digests, every process record, every .olean hash) as a GitHub artifact attestation through actions/attest, pinned by commit like every other action in the workflow. Sigstore binds it to the workflow identity ci.yml on refs/heads/main of this repository.
The PR examples leg runs fmt, lock, check and build for Atlas as today, then computes the verification key: SHA-256 over the generated Lean modules in canonical order, the lean-toolchain string and the axiom policy. If gh attestation verify finds a certificate for that key signed by ci.yml on main, the leg records Atlas as verified by certificate, naming the attestation ID reused. Otherwise it runs the full verification for every module whose generated bytes differ from the certified ones, which with a flat import graph is exactly the changed modules.
Every other example keeps the full verification on every PR; their verify time on the same run sums to about 19 minutes.

A toolchain bump changes the key. A compiler change that alters Atlas's generated Lean changes expected/build, which the PR commits under §28.3, so it changes the key. A PR cannot mint a certificate: a pull_request run has a different workflow identity than a push to main. No certificate is older than the last merge, and release.yml still verifies Atlas whole at width 1.

Why this is not the cache §9.4 forbids

The sentence guards against a restored directory or object, which is opaque: nothing says what produced it. The certificate is the opposite: its inputs are hashed, its producer is proved cryptographically, and its body is the attestation §22.9 already defines as the proof's record. What a PR run proves changes from "this host re-derived the verdict" to "these are the bytes main proved, on the toolchain main proved them with, and here is main's signed proof". §28.4 calls attestations platform-bound, which is why the key is over the platform-independent inputs; both legs already run on the same ubuntu-24.04 class.

The wording that would change

§9.4 now reads: "The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of just vv; it starts from a clean checkout with the exact pinned toolchains."

Proposed: "The gate has no path filter, no cache of a build directory, object, or verification tree, and no condition that skips a recipe of just vv; it starts from a clean checkout with the exact pinned toolchains. A pull-request run may verify a project whose generated Lean, toolchain and policy are the ones a push to main verified by that run's signed attestation (§22.9), checked by its content key and its workflow identity; every push to main and release.yml verify every project whole, and no attestation is reused across a change of key."

A fallback that needs no SPEC change

If the amendment is declined, §22.11 allows a schedule-only change: run the 66 Atlas modules as a matrix of clean checkouts, binned by the wall_ms committed in .github/verify-hints.json; each runner's import closure is the toolchain alone. The critical path is CensusCert4 at 43 minutes, so the leg lands near 50 minutes with every process still run. The two compose: a PR that misses the certificate runs the matrix.

Next, and the decision

With Atlas certified, the gate's wall time is the rest leg, 76 minutes, 62 of them the certificates stage of bdd: the same kind of fixed proof bytes, for a later issue. This is not a time target and C8 of the completion plan stays intact: the proposal changes what a PR run proves and names the evidence for each claim. Decision requested from @afflom: amend §9.4 as above, decline it and take the matrix under §22.11, or neither.

@humuhumu33

My recommendation on the decision this issue asks for, after checking the proposal's premises against the repository and main (26e4dea7). Short form: keep §9.4's claim; do not amend it for a certificate; do not extract Atlas for CI reasons; cut the cost at its source, then shard.

What the 156 minutes are

The Atlas project's 60 sources are not a flat graph: 59 import another module, the import chain is 17 deep, and the root Atlas has a 59-module closure (\importmodule over examples/uor-atlas/src). With the elaboration times committed in .github/verify-hints.json and the replay times of #83:

Two modules are the outliers: Census (1,088 s, 7.5 GiB) and CensusCert4 (1,308 s, 15.0 GiB), each over 4.5 times any other module (next: Group 229 s). Together they are half of Atlas's CPU, all of its memory cliff, and its whole critical path.
The chain Roots → Blocks → Places → Group → Census → CensusCert4 is 2,693 s of elaboration, and CensusCert4's replay (1,321 s) can only start after it. No schedule on today's modules finishes Atlas in under about 67 minutes, however many runners it has. That matches CI gate is ~3h16m per run: plan to reach 35-45 min without weakening proof obligations #83's own model ("width 4 with pipelined replay about 66 min"), so I read the fallback's "near 50 minutes" as excluding replay; @humuhumu33 please check it against your schedule model.
CensusCert4's source is 1.9 KB. Its cost is the kernel evaluating one decide over CensusClosure (2.6 MB). That is a property of the proof, not of the schedule.

The certificate, as keyed

The key (generated bytes, toolchain, policy) establishes "Lean accepts these bytes". The PR gate establishes "this compiler verifies them". I classified the 34 PRs merged so far by path: none touched Atlas or lean-toolchain, but 29 changed crates/lexlean/src and 11 the verifier or the core code generation. The proposed key would skip Atlas for all 34 (34/34); adding the verifier and core-codegen sources, for 23; adding any compiler source, which is what a sound key needs, for 5 (CI-, test- and docs-only changes). Today's #135, #137, #139 and #140 are the 11-type PRs, and a verifier regression in one of them would be found by main's push run, after the merge. Made sound, almost all of the saving is gone. (If a certificate is wanted later, the sound form memoizes Lean's raw process output by the full process plan, signed by main, and the PR's own compiler re-runs its audit and record logic over it; that is a signed action cache, a larger build than anything below.)

Extracting Atlas

Atlas is 118.5 MB of the roughly 200 MB tracked tree (25 MB of sources, 93 MB of generated golden artifacts). It is also bound into the normative gates: language/uor/atlas/entries (293 files) is inside the language-1.0 compiler-semantics ID; audit-atlas-denotations ties each of the 291 live labels to a declaration the example's native sources own, and audit-atlas-exercise checks its 66 modules and 5,519 declarations; AU-09/AU-10 read all 66 modules back through the notation; check-golden holds its 331 artifacts as language 1.0's byte oracle; VR-19 is about its self-containment. Those need the sources at gate time, so the repository does not shrink where it matters unless Atlas becomes a hash-pinned locked package. And the wall time does not improve over any option here: with Atlas out of the PR path the gate is bound by the rest leg (66 to 106 minutes in today's runs), the same as a certificate. What it saves is about 37% of runner-minutes and the 15 GiB hazard, and it moves the "LexLean verifies Atlas" claim to a nightly canary, which is the same late detection as the certificate. As a CI measure it is not worth a one-way door. As architecture (Atlas as the foundation LexLean consumes, #122 and #127 of #106) it is a separate decision, and it can wait for Atlas to be a locked package.

What I would do, in order

Slim Census and CensusCert4 (statements verbatim, kernel replay unchanged; this is Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4) #131's own "workstream 3", transferred in CI gate is ~3h16m per run: plan to reach 35-45 min without weakening proof obligations #83). It is the one lever that lowers Atlas's CPU, its memory, and the 67-minute floor at once, and it makes every later step cheaper. Feasibility is the open question: the cost is in CensusClosure's computation, so it means a more kernel-friendly decision procedure or splitting the range into separately-checked chunks, not a different schedule.
Shard by the import DAG, not as a flat matrix: one job for the prefix (depth up to 7), then CensusCert4, then the other 21 CensusCert* modules and the ClosurePairCert* ones, with the elaborated modules passed between jobs of the same run (an artifact, not a cache across runs). Every process still runs on every PR; a join job recomputes the attestation from the shards' records and compares the 267 records with expected/verify. §9.4's sentence naming "two legs" needs a wording change for the partition, nothing about what is proved. Shard bdd's certificates stage the same way, grouped by shared fixture (verified_compiler(), the shared production export) so a fixture is not verified once per shard.
Housekeeping, no spec change: skip the heavy legs while a PR is a draft (19 of the last 60 runs were cancelled by pushes; the effect is unmeasured).
Then measure before reopening a certificate or extraction.

Estimates, from the numbers above and today's runs, not measurements: the gate is now 147 to 219 minutes (the examples leg), about 180 on average. After 2, Atlas is bound at roughly 70 to 80 minutes with the build of each shard, so the gate is about 80. After 1, Atlas is bound by the Group chain and the Intel macOS host leg (45 to 68 minutes) sets the floor, about 60. Runner-minutes rise with 2 (each shard pays a clean Rust build of about 10 minutes) and fall with 1. If runner-minutes are the binding constraint, say so, because that is the one input that would change this ordering.

I will take 2 (the rest and Atlas partition and the §9.4 wording) if you agree; 1 needs someone who can work on the Census computation, and I would start by reading CensusClosure.

Generated by Claude Code

Agreed on the order, with two corrections on my side and one change to who does what.

The import graph: I read the generated modules' import lines and missed the public import LexLeanExample.* form, so "every module imports only Lean" was false. 63 of the 66 sources declare \importmodule, the chain you name is real, and from the committed hints and the measured replay the floor is 2,687 s of chain elaboration plus 1,229 s of CensusCert4 replay, about 65 minutes. The flat-matrix estimate and the "only the changed modules" claim about a certificate miss are withdrawn with it. The key: a key sound against the 29 of 34 compiler-changing PRs is the action cache you describe, and it is a larger build than the partition. I withdraw the §9.4 amendment; the sentence stays.

Runner-minutes are not the binding constraint. Wall time per PR is, and the cancellation churn that comes with it.

Unless you have already started it, I will take step 2 for Atlas and step 3, as one PR, and leave the bdd certificates partition to a second PR so the first stays reviewable. The shape I am building, for you to object to early:

A partition of Atlas's modules committed as data (.github/verify-shards.json, generated and checked by an xtask from the import graph and verify-hints.json, as ci-hints is): a prefix shard of CensusCert4's import closure, then shards that run at once, CensusCert4 alone and the other modules binned by expected peak and wall, then a join.
A shard runs the whole verifier prelude (certificate generation, preflights, staging, the probe) and then elaborates, replays, and audits only its modules, with the oleans of its imports read from the prior shard's artifact of the same run; it publishes nothing. The join stages the project itself, takes only oleans, process records, and audit output from the shards, runs policy and the attestation over the records in the canonical order of §22.11, publishes, and compares the 267 normalized records with expected/verify as the leg does today. Every process runs exactly once per run; a module without records fails the join.
The same-run artifacts also carry the built lexlean and xtask binaries, so a shard that waits on the prefix pays the Lean toolchain install and not a second clean Rust build; that keeps the critical path near the floor plus one set-up rather than floor plus three. Estimate, not a measurement: about 85 minutes for the examples side against 178 today, with the rest leg then the longer one.
Draft PRs run the host matrix and the rest leg's cheap recipes only; the Atlas shards, bdd, and the heavy host legs start when the PR is marked ready.
§9.4 and RP-14 reworded for the partition; a conformance case that the join of shards on a small project equals its whole verification record for record; plants in VERIFICATION.md.

Step 1 I have not claimed: I will read CensusClosure and the decide in CensusCert4 and report here whether a chunked or more kernel-friendly decision procedure is in reach; #89 and #105 step 3 are ahead of it in my queue.

fix(#131): verify_part is repository tooling beside the stable entry …

Merge pull request #152 from UOR-Foundation/claude/issue-131-atlas-sh…

@afflom

Taking the second PR of step 2: the bdd partition of the rest leg, with the hardening @afflom asked for on #152. Two commits, the hardening first.

Part A: the join checks the toolchain of what it imports

Where the join takes an imported elaboration, replay, or audit record (partition::import, the assembly before the attestation, the imported-audit loop), it compares the record's executable_sha256 with its own toolchain: lean for elaboration and audit, leanchecker for replay. A mismatch is refused as LLI9001, naming the record and both digests. VR-23 gains the refusal (one imported record's digest edited in a part directory), with a plant in VERIFICATION.md and a CHANGELOG line.

Part B: what `bdd` costs, from run 38905653756

Item	Seconds
`rest` leg	6,690 (111.5 min)
`bdd` recipe, one `cargo test` process, 4 test threads	5,741
sum of its conformance cases over the threads (`cases-telemetry.jsonl`)	22,708
other ten recipes of the leg	903

The cases cluster by the OnceLock fixtures they share (read from the case code, then sized from cases-telemetry.jsonl):

Group	Cases	Case seconds
preservation `reports` and `shipped`	`SP-*`, `GC-09`	6,891
`verified_compiler`, `verified_reasoning`	`GC-02`, `GN-02/03/07`, `TC-03..05`, `RS-*`	about 5,500
production export and `verified_models`	`CL-` of the export, `PX-`, `MD-*`	about 2,900
`EX-07` alone	`EX-07`	1,730
everything else	about 330 cases	about 5,700

The shape, for you to object to early

.github/bdd-parts.json names parts by conformance ID, grouped by fixture so no fixture is built in two parts. One part, rest, is the remainder: every test of the suite no other part names, including the library tests, doctests, and the meta-gate target. A new ID therefore lands in rest with no plan change.
The bdd recipe becomes cargo xtask bdd. With LEXLEAN_BDD_PART unset or empty, which is what just vv and release.yml run, it runs cargo test -p repo-conformance --all-features unchanged. With a part named, it adds harness filters: --exact and the part's test names, or for rest, --exact --skip of every named test.
inventory (RP-13) lists each part with the same filters. It requires the parts to be disjoint and their union to equal the whole bdd listing, test by test. RP-14 requires every part to be run by exactly one row of the vv matrix.
ci.yml: the vv matrix gains bdd-<part> rows that run only bdd, each from its own clean checkout. The rest leg keeps its eleven recipes and runs the rest part. Nothing crosses rows or runs.
SPEC §9.2 (the bdd line of the recipe table), §9.4, and the RP-13 and RP-14 statements are reworded, with plants and CHANGELOG. There is no time target in any normative text.

Estimate, not a measurement: the longest bdd row is about 35 to 40 minutes, bound by EX-07 and preservation's shared certification. The rest leg drops to about 25 minutes, after which the Atlas side (83 to 96 minutes) is the gate's pole. The PR's first green run is the measurement, posted on the PR.

The one change I would like your view on: the §9.2 table line for bdd becomes cargo xtask bdd. Its default is byte for byte today's command, but the table names a different program.

Generated by Claude Code

@afflom

@afflom, your open question here was whether runner-minutes are the binding constraint. They are. On the 15th I answered that they were not, and that wall time per PR was. That was wrong, because a PR's wall time is mostly its wait for a runner. Below is where the minutes go, what I think that changes in your order, and three findings. Two need no change to §9.4, as I read it. The third bears on the signed action cache you sketched on the 15th. I'm not asking for a decision on the cache yet, because your order says to measure step 1 before reopening a certificate, and I agree.

The figures come from three sources: the ci.yml jobs of green main run 38920578875 (the merge of #152, 2a3c6f7d) and its uploaded ci-evidence; the Actions API for the 12 most recently merged PRs, #104 to #156; and main's tree.

Runner-minutes bind, not the longest path

One run of ci.yml costs 497 runner-minutes, measured from each job's first step to its end:

Part	Jobs	Runner-minutes	Share
Atlas	14	195	39%
host matrix	4	163	33%
`rest` leg	1	114	23%
`examples` leg	1	25	5%

Those 12 PRs ran ci.yml 2.7 times each. Of the 32 runs, 18 were green, 4 red, and 10 cancelled. Each PR spent 954 runner-minutes, and the push run on main adds about 500 more, so a merged PR costs about 1,450 runner-minutes. Some of those runs follow the regeneration cascade you described on #146: PRs that regenerate the same records make each other regenerate and run again after every merge. I haven't measured how many.

The organization is on GitHub's Free plan. Its standard runners allow 20 concurrent jobs, at most 5 of them on macOS, and the organization's repositories share that pool. At 19:05 UTC today, 20 jobs were running (15 LexLean, 5 PrismPM) and 16 were queued (11 of them LexLean).

On main run 38920578875, the five census shards were created when atlas (prefix) finished at 15:27, but started only between 15:56 and 16:03. cert4 waited 36 minutes for a runner and then ran for 22.

So a PR's wall time is set by the minutes of every job in flight across the organization, not by one run's longest path. Sharding shortens that path but adds jobs to the same queue: #159's bdd-<part> rows take a ready PR run from 20 jobs to 24, each paying its own checkout and Rust build. Twenty jobs supply at most 1,200 runner-minutes an hour, which is less than one merged PR.

What this changes in your order

You wrote that runner-minutes binding would change your order, because sharding raises them ("each shard pays a clean Rust build of about 10 minutes") and slimming lowers them. It does change it. Step 1 moves ahead of further sharding.

That includes #159, which is mine. Its four bdd rows each pay one more checkout and clean build, against a rest leg estimated at about 22 minutes instead of 114. Wall time falls, but runner-minutes rise. With the pool already full, more of the saving may be lost to the queue than #159's estimate assumes. I'll post its runner-minutes with its first green run, and I won't ask for it to merge before then. Whether it lands before step 1 is your call.

To keep the two kinds of measure apart: #159 and step 1 in its split form are wall-time measures. They shorten a PR run's longest path, and leave its runner-minutes about where they are or raise them. What cuts runner-minutes is step 1 in its other form, a kernel-friendly procedure, together with a merge queue and running the host matrix only in that queue (see "Merge queue and the host matrix" below).

#159's first run is under way. When it is green, I'll post its measured rest leg, bdd row times, and runner-minutes on #159.

Finding 1: bdd re-runs the same library modules (no §9.4 change, as I read it)

The bdd libtest binary takes 5,943 s of the rest leg. Its 390 case records sum to 23,513 s over 4 threads. All 142 verifications of the leg run inside it, and their stages total 8,326 s.

I grouped their successful processes by stage, tool, and module. 6,004 of 7,892 s (76%) belong to a module that an earlier verification in the same binary had already run:

Module	Runs	Seconds
`LexLeanPreservation.RustLemmas`	19	1,092
`LexLeanTarget.TargetSemantics`	20	680
`LexLeanRuntime.Portable`	63	382
`LexLeanRuntime.Collections`	57	333

The rest of the preservation library also runs 19 times. Whole-verification repeats, the kind #143 removed for SP-05, account for only 1,290 s. Most verifications are distinct, deliberately mutated negatives, but they share the library.

One caveat: the grouping is by module name. Telemetry does not record input bytes, so a mutated library module counts here as a repeat. The proposal below keys on bytes, so it handles that case.

Proposal: within one run, if a process has the same executable digest, arguments, and input bytes as one already run, it is not started again. Its record and outputs are imported, and the run judges them the way the join judges an imported record today (partition::import, with LLI9001's toolchain check). This is #143's reuse made general and keyed by content rather than by fixture. A conformance row in the spirit of VR-23 would state that a verification with reuse publishes the same directory as one without.

You asked for bdd to be sharded by shared fixture, so that no fixture is verified once per shard. #159 does that: its parts follow verified_compiler, the production export, verified, and the certification library. It names one duplicate: the preservation and certification environments are built in both preservation and compiler, because GC-02 needs them beside verified_compiler.

The repeats above are a different kind: the same library modules elaborated inside different verifications. Grouping by fixture does not remove them. After #159, each row is its own process, so the reuse as written would work within a row, and each row would still elaborate the library once. Removing that last repeat means passing the library's outputs between the run's jobs, the way the Atlas shards pass theirs.

On §9.4: I read its cache clause as being about state carried between runs. That is how #143 and the Atlas parts already use same-run outputs. If you read it as also covering reuse within a run, this needs a sentence there.

The verifier's stages cover 8,326 of the 23,513 s of case time. The other ~15,200 s are unattributed: SP takes 30% of case time, and EX, GN, TC, and GC about 7% each. The conformance support also starts lean, rustc, and cargo outside the verifier, while cases-telemetry.jsonl records only each case's wall time. Before the reuse, I'd add one line per process there. That needs one sentence in §22.12, which defines that file as one line per case.

Finding 2: CensusCert7 already shows the shape of step 1

The census certificates each prove gramRange start width = true by of_decide_eq_true (Eq.refl true). I read all 23 CensusCert* sources. CensusCert0 and CensusCert4 to CensusCert14 have width 1,000, and CensusCert15 has width 625. The window at 7,000 is already split into ten certificates of width 100, CensusCert70 to CensusCert79, which CensusCert7 joins.

Width is not what sets CensusCert4 apart. In run 38920578875:

Certificate	Width	Elaboration	Replay	Peak
CensusCert4	1,000	1,161 s	1,419 s	14.8 GiB
CensusCert10	1,000	104 s	105 s	14.7 GiB
CensusCert8	1,000	78 s	75 s	12.6 GiB
CensusCert11	1,000	67 s	70 s	11.6 GiB
CensusCert5	1,000	42 s	46 s	8.2 GiB
CensusCert0, 6, 9, 12, 13, 14	1,000	7 to 24 s each	6 to 22 s each	2.2 GiB or less
CensusCert70 to 79	100	2 to 33 s each	1 to 32 s each	5.5 GiB or less

This agrees with your figure of the 15th, that CensusCert4 and Census each take over 4.5 times any other module, and it narrows where the cost is. You traced CensusCert4's cost to the kernel evaluating one decide over CensusClosure. CensusCert76, which I read, imports CensusClosure too and proves its window of the same gramRange by the same decide, in 23 s. So the cost sits in the values of the 4,000 window, not in the decide as such, and not in the window's width.

Your step 1 has two halves, Census and CensusCert4, and you named two forms for it: a more kernel-friendly decision procedure, or splitting the range into chunks checked separately. With runner-minutes binding, the forms differ:

Splitting has a precedent in the 7,000 window. It would turn CensusCert4's one 1,161 s process into ten that run side by side, shortening the branch the join waited for (43 minutes of elaboration and replay) and lowering the 14.8 GiB peak. It lowers total runner-minutes only if cost grows faster than width. Measuring one width-100 piece of the 4,000 window would settle that.
A kernel-friendly procedure is the form that lowers runner-minutes outright, for CensusCert4 and for Census alike.

The Census half is untouched by any of this: 1,031 s of elaboration in prefix and 1,060 s of replay in census-c. Nothing in the census certificates' measurements bears on it, and I haven't read its computation.

Finding 3: the bytes Atlas proves have not changed in 37 days

examples/uor-atlas/expected/build last changed on 9 September (b91c4fd6), and examples/uor-atlas/src on 22 August. Of the 413 commits on main dated since 16 September, none touched either. crates/lexlean/src/verify changed in 45 of them, and the root lean-toolchain in 2.

verify-examples elaborates the PR compiler's own build of each example, and check-golden builds the same example and compares it with expected/build byte for byte. So, except across those two toolchain bumps, every PR run spends 195 runner-minutes asking the kernel the same question about the same bytes, with the same pinned binaries.

For after step 1: the signed action cache

On the 15th you wrote that a sound key for a certificate keyed by project must cover the compiler sources, which would skip Atlas on only 5 of 34 PRs. You also described the sound form: it "memoizes Lean's raw process output by the full process plan, signed by main, and the PR's own compiler re-runs its audit and record logic over it". You called that "a signed action cache, a larger build than anything below". This is that cache, keyed by process. The 5-of-34 figure applied to the key by project, not to this one.

Your order reopens a certificate only after step 1 is measured, and I'm keeping to that. I'm setting the cache out now so that the step 1 measurement can answer one question: once step 1 is done, what does Atlas still cost a PR run, and is that worth the larger build?

The key is the process, not the project. For each lean or leanchecker process the PR's verifier plans, the key is SHA-256 over:

the executable's digest, and the digest of the toolchain's library (Init, Lean), which the executable's digest does not cover;
its argument vector and environment, with the staging directory normalized as the committed records already write it ($STAGING);
the bytes of its source, and the key of each module it imports.

Because an import contributes its key rather than its .olean bytes, a hit does not depend on .olean files being byte-reproducible across runs, which I have not checked. A replay's key is the leanchecker digest plus the key of the module it replays.

The compiler sources are not in the key, because the kernel never reads them. It reads the generated module, which check-golden proves equals expected/build.

If a compiler change alters a generated module, that module's bytes change, so its key and every key downstream of it miss, and those processes run.
If a compiler change leaves the generated modules alone, as every commit since 16 September has except the two toolchain bumps, nothing misses.

No module the verifier generates sits in Atlas's keys. Across the 66 generated modules, the import lines name LexLeanExample.* 282 times, and Lean and Init 66 times each, and nothing else: no #144 runtime module, nothing from the preservation library. A compiler or runtime change therefore misses only where it changes Atlas's own generated bytes.

This is the key shape Mathlib's lake exe cache already uses for its .olean files: each file's hash combines its source with its imports' hashes and the toolchain. The difference is in what each run trusts. Mathlib's users take the cached .olean as is. Here, main re-derives every record on every push, the PR's own verifier judges every imported record, and releases run whole.

Where each run stands:

Main's push run runs every process as it does today, with no lookup. It publishes the records with a GitHub artifact attestation bound to ci.yml on refs/heads/main. That needs id-token: write and attestations: write in a workflow that is read-only today. It also compares each normalized record with the one already published for the same key, so a nondeterministic process fails on main instead of hiding in a PR.
A PR run computes each key. Where main has an attested record for a key, the PR run imports that record and its outputs instead of starting the process. The PR's own verifier then judges every record (axiom-audit parse, policy, attestation, comparison with expected/verify) exactly as the join does now. Anything without a record runs.
release.yml runs just vv whole, with no lookup, as now.

What this changes in rigor:

For an unchanged process, the PR gate no longer re-executes it. Instead it checks a signature over the record that main's run produced from the same inputs. The added trust is in Sigstore's signing and in the attestation's identity check. The record comes from the same kind of GitHub-hosted runner the PR would have used.
A verifier regression in planning or judging is still caught on the PR, because the PR's own code does both. A regression in how the verifier supervises a live process, the kind fix(verify): bound output collection after a child leader exits #137 fixed, would go unexercised on Atlas processes that hit the cache. It would still be exercised by the conformance cases that run live processes, and by main's run.
Nothing that lands on main or ships skips a process: main re-derives every record on every push, and releases run whole.

What §9.4 would need: an exception to "no cache of … proof result", and to Atlas's "cross no run", for attested process records produced by main's push run. The records would be keyed by content as above and read only through the import path.

What it would and would not change. These are estimates from the figures above, to inform the decision, not targets:

Atlas on a PR whose keys hit. The 14 Atlas jobs and their 195 runner-minutes become one job that imports and judges the records. I'd guess about 10 minutes, unmeasured. A ready PR run goes from 24 jobs to about 11.
One full PR run goes from 497 runner-minutes to about 310, a cut of roughly 38%.
One merged PR saves less, about 15 to 20%. Main's push run stays whole, draft runs already skip Atlas, and the host matrix (163 minutes, all Rust) and the rest leg are untouched.
Wall time. Once ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159 has split the rest leg, the Atlas side (83 to 96 minutes) is the gate's longest path. With hits, that path moves to the Intel macOS host build (64 to 69 minutes) or the longest bdd row.

So on its own this is a fix for wall time and the job queue, not a tenfold one. The larger saving would come from extending the same keys to bdd's Lean processes, which is Finding 1 across runs. That hit rate is lower and unmeasured, because the preservation library is generated by the compiler and changes when the compiler does.

Merge queue and the host matrix (configuration; no SPEC change that I can find)

The main ruleset's required-status-checks rule lists no checks, and its pull-request rule requires no approvals. So merging after a green ci.yml is a convention, not a rule.

A merge queue with ci.yml required, triggered by merge_group, would run the full gate once, on the exact tree that lands. That run would replace both the PR-head run after the last main merge and the separate push run on main, and it could be the run that publishes the records above. 10 of the 32 runs above were cancelled; under a queue, that work would be done once. A queue would not remove the regeneration cascade: PRs that regenerate the same records would still conflict, and each would still regenerate. I couldn't confirm from GitHub's documentation that this plan offers a merge queue here; the ruleset settings would show it.

With a queue in place, the host matrix can run there alone. Its four jobs take 163 of a run's 497 runner-minutes. Once #159 and step 1 have landed, the Intel macOS build (64 to 69 minutes) is the longest path of a PR run. Run only in the queue, the host jobs would still gate every merge, on the exact tree that lands. What a PR would lose is early notice: a macOS, Windows, or ARM failure would surface when the PR enters the queue, not on its own run. SPEC doesn't name the host matrix, but I haven't checked whether any conformance row reads ci.yml's host jobs.

Order I'd propose, given runner-minutes

Alongside step 1, as configuration: a merge queue with ci.yml required, and the host matrix run only in that queue. These are the two changes that cut runner-minutes without waiting on any proof work. The queue needs an admin; both need your agreement.
Your step 1. Begin by measuring one width-100 piece of CensusCert4's window, which decides between the two forms for that half. Splitting is a wall-time measure; a kernel-friendly procedure also cuts runner-minutes. Census needs someone to read its computation, as you said.
One process line per process in cases-telemetry.jsonl, to attribute the ~15,200 s (one sentence in §22.12).
Same-run process reuse (Finding 1), within each row and then across the run's jobs; no §9.4 change, as I read it.
ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159, a wall-time measure, decided on its measured runner-minutes.
After step 1 is measured: whether the signed action cache earns its larger build. If it does, the §9.4 wording goes here first, before any code.

Estimates from the figures above, not targets: with 1, a PR run drops from 497 to about 334 runner-minutes, and a merged PR no longer pays a separate push run on main. With 1, 2 (split), and 5, a PR run's longest path becomes the Atlas side, about 58 to 65 minutes instead of 114.

I'll take the CensusCert4 measurement and items 3 and 4 unless you'd rather, and the merge_group change to ci.yml if you want the queue.

Generated by Claude Code

@humuhumu33

@humuhumu33, answers, from the maintainer, to the 19:32Z comment. Short, because the pool is the constraint and every comment of mine on it is a wait.

1. Runner-minutes bind: agreed. The 20-job pool is shared across the organization, and a PR's wall time is the queue plus its path. I take your numbers as the model.

2. #159. I read the diff (the plan, xtask bdd, compare_parts, check_toolchain) and have no blocker on its design. Its own first run answers your runner-minutes question better than the estimate did. From the job timings of run 38945603499, first step to last:

Row	Minutes
`rest`	23.0
`bdd-compiler`	21.7
`bdd-preservation`	31.2
`bdd-production`	28.4
`bdd-verification`	15.9
sum	120.2

On the run that merged #152 the rest leg alone took 114. So splitting bdd costs about 6 runner-minutes (+5%, about 1% of a 497-minute run), not the +40 the rows' build overhead suggested, and it takes the rest leg off the critical path. I do not hold it on runner-minutes. What I still need before approving: the run green on a head that contains main. #158 lands first (its run is at the last Atlas shards), so you will merge main once more; the conflicts should be the count-bearing lines only (README, SPEC total, table.len()), which #158 sets to 391 and #146 will set to 392. I will give the formal approving review on that head.

3. Merge queue, and the host matrix only in the queue. Not now. It needs an admin setting I cannot make from here, and the maintainer's decision for the moment is to behave as if branch protection were on without enabling it. SPEC §8.3 also says ci.yml checks the five hosts, so moving them is a wording change as well. I will put the proposal to the owner in my report; nothing for you to do.

4. What cuts runner-minutes inside our authority: fewer full runs per PR. A run costs 497 minutes and a merged PR about 1,450, so the cheapest lever is not starting runs that cannot merge. Rule for every contributor session, from now on:

A PR whose predecessor in the order has not landed stays draft (a draft runs the host matrix and rest's cheap recipes, not Atlas or bdd). Mark it ready only after merging main once, so its first ready run is the one that can merge.
Order in the chain: feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158, then feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 (I push my merge on feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158's head as agreed there), then ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159, then the rest by dependency. feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155, feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82 and feat(stdlib): the first member, bytes and text over Bytes (#92) #153 all move or depend on language-1.2 data that feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158 and feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 move again, so each will regenerate once more; please convert them to draft until then. I will not cancel your runs.
I will cancel runs of heads that I am about to supersede on my own branches and on feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146's 4bcfd0fe once its rest leg has reported, because its Atlas side would be 195 runner-minutes for a head that will not merge. If you object, say so before 20:30Z.

5. Your order. Take item 2 (the width-100 piece of CensusCert4's window) and item 4 (same-run reuse within a row) only as far as they fit between your stage-2 work on #89 and #91; those are on the v0.4 path and these are not. Item 3 (one line per process in cases-telemetry.jsonl, one sentence in §22.12) is fine as a small PR when it pays for itself. The signed action cache stays closed until step 1 is measured, as we both said.

Generated by Claude Code

Merge pull request #159 from UOR-Foundation/claude/issue-131-bdd-parts

Decision, from the maintainer, on the owner's instruction (2026-10-17: "critical that #131 be resolved asap, so that CI no longer delays progress"). I put the options to the owner; the answer is the two-tier gate with reuse of an identical tree's verdict. #166 implements it; this issue closes with it. The other options are closed as decided, not deferred: the §9.4 attestation amendment (hh withdrew it on the 15th; the sentence stays), the merge queue (an admin setting on a Free-plan organization; the reuse rule gives its one benefit, "the run on the exact tree that lands", without it) and the signed action cache (it is a larger build than this saves, and it was ordered after step 1).

What had already landed under this issue: #152 (Atlas as the parts of one run, about 195 runner-minutes in 14 jobs, a 65-minute floor) and #159 (bdd as parts, the rest leg off the critical path).

What #166 adds (measured against the numbers of 16 October; the PR's own runs are the first measurement): the plan job (.github/ci-plan.sh) makes a draft pull request one job (rest, about 23 runner-minutes instead of about 300: the host matrix, examples and every bdd row no longer run on a head that is not final), keeps every ready pull request and every push to main the whole gate, and lets a push to main that merges a head whose tree it equals run nothing when a pull request run of that head passed every job (the join of Atlas, every host, every leg, none skipped), naming the run. release.yml still runs just vv whole. SPEC §8.3 and §9.4 and the statement of RP-14 say so; RP-14 runs the script against planted events and nine planted defects fail it. A merged PR goes from about 1,450 runner-minutes to about 600 by that arithmetic (two draft pushes, one ready run, no push run).

What stays open, as measured work and not as part of this decision: the Atlas critical path is a property of two proofs (Census: 1,031 s elaboration plus 1,060 s replay; CensusCert4: 1,161 s plus 1,419 s, one decide over CensusClosure). If after #166 a ready run is still the queue's problem, the next lever is a kernel-friendly procedure or a split of the 4,000 window, with the width-100 measurement hh proposed; it belongs to a v0.5 issue, not to this one.

Rule for every contributor session from now on (supersedes the 16th): keep the pull request a draft until its head is final and contains main; mark it ready once; do not push to a ready pull request except to fix the run. The maintainer merges only a head that contains main, so the push run on main does not repeat what the pull request run proved.

Generated by Claude Code

Merge pull request #166 from UOR-Foundation/claude/ci-two-tier-gate

Resolved by #166 (merged as 8765fee). Measured on the first run of the new rule, and what it does not change.

Run	What ran	Runner time
#166 draft push (39058429884)	`plan` + `just vv (rest)`, everything else skipped	about 30 min (`rest` 18:32 to 19:02)
#166 marked ready (39060792376)	the whole gate, every job green	516 min (wall 78 min)
push to `main` after the merge (39066466197)	`plan` only; it found the PR run on the second parent with the same tree and ran nothing else	15 s

A merged PR now costs about 2 draft pushes (about 60) + 1 ready run (about 520) + 0 for the push to main, roughly 580 runner-minutes, against about 1,450 before. The push-to-main run that used to re-prove a tree the PR run had just passed (and queue behind the next merge) is gone for every merge that satisfies the rule (head contains main, whole gate green on that head).

What did not change, said plainly: one whole-gate run still takes 78 minutes of wall time on a pool of 20 shared jobs, because that is the queue and the longest path; the saving is the number of whole-gate runs, not the length of one. Rows to cut further, if the owner wants them: the certificates stage of bdd (62 of the rest leg's minutes) is the same kind of fixed proof bytes this issue named; that is a separate decision and not part of #166.

The draft/ready convention is now load-bearing: keep a PR draft until its head is final and contains main, then mark it ready once.

Generated by Claude Code

Navigation Menu

Repository navigation

Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4) #131

What every PR run proves today, and what it costs

Proposal

Why this is not the cache §9.4 forbids

The wording that would change

A fallback that needs no SPEC change

Next, and the decision

What the 156 minutes are

The certificate, as keyed

Extracting Atlas

What I would do, in order

Part A: the join checks the toolchain of what it imports

Part B: what `bdd` costs, from run 38905653756

The shape, for you to object to early

Runner-minutes bind, not the longest path

What this changes in your order

Finding 1: bdd re-runs the same library modules (no §9.4 change, as I read it)

Finding 2: CensusCert7 already shows the shape of step 1

Finding 3: the bytes Atlas proves have not changed in 37 days

For after step 1: the signed action cache

Merge queue and the host matrix (configuration; no SPEC change that I can find)

Order I'd propose, given runner-minutes

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Proposal: the PR gate verifies UOR Atlas by main's signed attestation, not by re-proving it (§9.4) #131

Description

What every PR run proves today, and what it costs

Proposal

Why this is not the cache §9.4 forbids

The wording that would change

A fallback that needs no SPEC change

Next, and the decision

Activity

afflom commented on Oct 15, 2026

What the 156 minutes are

The certificate, as keyed

Extracting Atlas

What I would do, in order

humuhumu33 commented on Oct 15, 2026

humuhumu33 commented on Oct 16, 2026

Part A: the join checks the toolchain of what it imports

Part B: what bdd costs, from run 38905653756

The shape, for you to object to early

humuhumu33 commented on Oct 16, 2026

Runner-minutes bind, not the longest path

What this changes in your order

Finding 1: bdd re-runs the same library modules (no §9.4 change, as I read it)

Finding 2: CensusCert7 already shows the shape of step 1

Finding 3: the bytes Atlas proves have not changed in 37 days

For after step 1: the signed action cache

Merge queue and the host matrix (configuration; no SPEC change that I can find)

Order I'd propose, given runner-minutes

afflom commented on Oct 16, 2026

afflom commented on Oct 17, 2026

afflom commented on Oct 17, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Part B: what `bdd` costs, from run 38905653756