Repository navigation
[0.5.0] Split CensusCert4's 4,000 window into ten width-100 certificates #168
Description
Follow-up to #131, which #166 resolved. The closing comment there left this lever open for v0.5.
CensusCert4 is one theorem, UorAtlas.Census.gramWin4 : gramRange 4000 1000 = true, proved by of_decide_eq_true. On the main run of 16 October it took 1,161 s to elaborate and 1,419 s to replay, at about 15 GiB. That is about 43 minutes of the Atlas side's longest path. Its siblings of the same width take 7 to 104 s.
The tree already has the pattern: CensusCert7 is split into CensusCert70 to CensusCert79, joined by gramRange_append. My plan copies it:
CensusCert40toCensusCert49: each provesgramRange (4000 + 100k) 100 = truewith the samedecideproof asCensusCert76.CensusCert4keeps its statement exactly. It is proved from the ten pieces the wayCensusCert7is.CensusCompleteandAtlasstill import it unchanged.Atlasalso imports the ten pieces, as audit-atlas-exercise (R4) requires.- I regenerate the Atlas
expected/buildandexpected/verify, plus.github/verify-shards.jsonandverify-hints.json. Language data and the language-1.2 identity stay the same. - First I measure one width-100 piece. If it is still heavy, I switch to width 50.
The PR stays a draft until its head is final and contains main. I'll take this unless you'd rather hold it until the v0.4 train lands.
Activity
humuhumu33 commentedon Oct 17, 2026
Before I measure a piece, here is what the logs already show. CensusCert4 is not a large proof: it runs out of memory and swaps.
Evidence (main run 39054719580, the merge of #155, the "Processes that swapped" table of each job):
The runner has 16 GiB of RAM plus the 4 GiB swap file. CensusCert4 needs about 18.5 GiB.
Cost model. The kernel keeps its caches for one declaration, so memory grows with the work in that declaration. Without swap, the cost of a window is linear in its positive Gram types (the keys of
gramInverseRows), about 1.6 to 1.7 s each at any width:Prediction for the split. At width 100, window 4's positive types fall 15, 11, 4, 0, 0, 15, 15, 10, 11, 0 across CensusCert40 to 49. The heaviest pieces (40, 45, 46) should match CensusCert70 (15 types, 23.7 s, 4.0 GiB). The whole window should take about 135 s per pass instead of 1,419 s and 2,249 s, so about 270 s in total instead of 3,668 s, with no swap. The
cert4andcert4-replayjobs then have nothing left to do, and the pieces fit in the census shards. I will check this against the first measured piece, as planned.CensusCert10. It already touches swap at 14.7 to 15.0 GiB, so it is the next window to cross the line. I suggest splitting it in the same PR, the same way. Each piece's source differs from CensusCert70's only in the module name, the window's start number, the
gramWinname, and the internal declaration name (used twice).The statements, the kernel
decideproofs, thegramRange_appendjoin, and every replay and audit record stay as they are.Atlas: expected/verify and hints for the split census windows (#168)
VERIFICATION.md: CensusCert10 peaks in GiB, not MiB/1000 (#168)