Atlas: prove CensusCert4 and CensusCert10 from width-100 pieces (#168)

.github/verify-hints.json

@@ -76,8 +76,48 @@
     "wall_ms": 20849
   },
   "LexLeanExample.CensusCert10": {
-    "peak_rss_kib": 15590960,
-    "wall_ms": 114639
+    "peak_rss_kib": 1443088,
+    "wall_ms": 4518
+  },
+  "LexLeanExample.CensusCert100": {
+    "peak_rss_kib": 1437932,
+    "wall_ms": 1944
+  },
+  "LexLeanExample.CensusCert101": {
+    "peak_rss_kib": 3906756,
+    "wall_ms": 18504
+  },
+  "LexLeanExample.CensusCert102": {
+    "peak_rss_kib": 3259512,
+    "wall_ms": 13707
+  },
+  "LexLeanExample.CensusCert103": {
+    "peak_rss_kib": 3912776,
+    "wall_ms": 18870
+  },
+  "LexLeanExample.CensusCert104": {
+    "peak_rss_kib": 1520648,
+    "wall_ms": 1960
+  },
+  "LexLeanExample.CensusCert105": {
+    "peak_rss_kib": 1518372,
+    "wall_ms": 1932
+  },
+  "LexLeanExample.CensusCert106": {
+    "peak_rss_kib": 1520460,
+    "wall_ms": 1952
+  },
+  "LexLeanExample.CensusCert107": {
+    "peak_rss_kib": 2407780,
+    "wall_ms": 8046
+  },
+  "LexLeanExample.CensusCert108": {
+    "peak_rss_kib": 3898456,
+    "wall_ms": 18509
+  },
+  "LexLeanExample.CensusCert109": {
+    "peak_rss_kib": 5841916,
+    "wall_ms": 31295
   },
   "LexLeanExample.CensusCert11": {
     "peak_rss_kib": 12093836,
@@ -100,8 +140,48 @@
     "wall_ms": 4842
   },
   "LexLeanExample.CensusCert4": {
-    "peak_rss_kib": 15693400,
-    "wall_ms": 1307970
+    "peak_rss_kib": 1486624,
+    "wall_ms": 846
+  },
+  "LexLeanExample.CensusCert40": {
+    "peak_rss_kib": 4670592,
+    "wall_ms": 20395
+  },
+  "LexLeanExample.CensusCert41": {
+    "peak_rss_kib": 3833884,
+    "wall_ms": 15695
+  },
+  "LexLeanExample.CensusCert42": {
+    "peak_rss_kib": 2422704,
+    "wall_ms": 6363
+  },
+  "LexLeanExample.CensusCert43": {
+    "peak_rss_kib": 1549856,
+    "wall_ms": 1219
+  },
+  "LexLeanExample.CensusCert44": {
+    "peak_rss_kib": 1554216,
+    "wall_ms": 1193
+  },
+  "LexLeanExample.CensusCert45": {
+    "peak_rss_kib": 4765652,
+    "wall_ms": 20701
+  },
+  "LexLeanExample.CensusCert46": {
+    "peak_rss_kib": 4667372,
+    "wall_ms": 20105
+  },
+  "LexLeanExample.CensusCert47": {
+    "peak_rss_kib": 3641284,
+    "wall_ms": 13939
+  },
+  "LexLeanExample.CensusCert48": {
+    "peak_rss_kib": 3901196,
+    "wall_ms": 16048
+  },
+  "LexLeanExample.CensusCert49": {
+    "peak_rss_kib": 1551904,
+    "wall_ms": 1228
   },
   "LexLeanExample.CensusCert5": {
     "peak_rss_kib": 8578132,

.github/verify-shards.json

@@ -27,7 +27,17 @@
         "prefix"
       ],
       "elaborate": [
-        "LexLeanExample.CensusCert4"
+        "LexLeanExample.CensusCert4",
+        "LexLeanExample.CensusCert40",
+        "LexLeanExample.CensusCert41",
+        "LexLeanExample.CensusCert42",
+        "LexLeanExample.CensusCert43",
+        "LexLeanExample.CensusCert44",
+        "LexLeanExample.CensusCert45",
+        "LexLeanExample.CensusCert46",
+        "LexLeanExample.CensusCert47",
+        "LexLeanExample.CensusCert48",
+        "LexLeanExample.CensusCert49"
       ],
       "replay": []
     },
@@ -37,12 +47,32 @@
       ],
       "elaborate": [
         "LexLeanExample.CensusCert10",
+        "LexLeanExample.CensusCert100",
+        "LexLeanExample.CensusCert101",
+        "LexLeanExample.CensusCert102",
+        "LexLeanExample.CensusCert103",
+        "LexLeanExample.CensusCert104",
+        "LexLeanExample.CensusCert105",
+        "LexLeanExample.CensusCert106",
+        "LexLeanExample.CensusCert107",
+        "LexLeanExample.CensusCert108",
+        "LexLeanExample.CensusCert109",
         "LexLeanExample.CensusCert11",
         "LexLeanExample.CensusCert5",
         "LexLeanExample.CensusCert8"
       ],
       "replay": [
         "LexLeanExample.CensusCert10",
+        "LexLeanExample.CensusCert100",
+        "LexLeanExample.CensusCert101",
+        "LexLeanExample.CensusCert102",
+        "LexLeanExample.CensusCert103",
+        "LexLeanExample.CensusCert104",
+        "LexLeanExample.CensusCert105",
+        "LexLeanExample.CensusCert106",
+        "LexLeanExample.CensusCert107",
+        "LexLeanExample.CensusCert108",
+        "LexLeanExample.CensusCert109",
         "LexLeanExample.CensusCert11",
         "LexLeanExample.CensusCert5",
         "LexLeanExample.CensusCert8"
@@ -140,7 +170,17 @@
       ],
       "elaborate": [],
       "replay": [
-        "LexLeanExample.CensusCert4"
+        "LexLeanExample.CensusCert4",
+        "LexLeanExample.CensusCert40",
+        "LexLeanExample.CensusCert41",
+        "LexLeanExample.CensusCert42",
+        "LexLeanExample.CensusCert43",
+        "LexLeanExample.CensusCert44",
+        "LexLeanExample.CensusCert45",
+        "LexLeanExample.CensusCert46",
+        "LexLeanExample.CensusCert47",
+        "LexLeanExample.CensusCert48",
+        "LexLeanExample.CensusCert49"
       ]
     },
     "closure": {

.github/workflows/ci.yml

@@ -25,7 +25,7 @@
 # each a job of its own clean checkout that elaborates, replays, and audits the
 # modules its plan names and reads the `.olean` files of the modules it imports
 # from the shards before it, then the join, which reads every shard's records,
-# publishes the verified directory, and compares its 267 normalized records
+# publishes the verified directory, and compares its 347 normalized records
 # with `expected/verify` as the leg did. Every process of the verification runs
 # exactly once per run; the executable the shards run is the one the `prefix`
 # shard built from the clean checkout, carried between the jobs of the run as
@@ -246,7 +246,8 @@ jobs:
   # UOR Atlas as the parts of one run (SPEC.md §9.4): the shards of
   # `.github/verify-shards.json`, each a clean checkout that runs the processes
   # its plan names, then the join. `prefix` elaborates the import closure of
-  # `CensusCert4`, the module that dominates the verification.
+  # the `CensusCert*` modules, `Census` among them, the module that dominates
+  # the verification.
   atlas-prefix:
     name: atlas (prefix)
     if: ${{ needs.plan.outputs.full == 'true' }}
@@ -332,8 +333,8 @@ jobs:
           if-no-files-found: error
           retention-days: 14
 
-  # The shards that need only `prefix`: `CensusCert4` alone, the other
-  # `CensusCert*` modules, and the replays of the prefix.
+  # The shards that need only `prefix`: `CensusCert4` and its ten pieces, the
+  # other `CensusCert*` modules, and the replays of the prefix.
   atlas-l1:
     name: atlas (${{ matrix.shard }})
     if: ${{ needs.plan.outputs.full == 'true' }}
@@ -422,7 +423,8 @@ jobs:
           if-no-files-found: error
           retention-days: 14
 
-  # The replay of `CensusCert4`, which needs its `.olean` and nothing after it.
+  # The replay of `CensusCert4` and its pieces, which need their `.olean` files
+  # and nothing after them.
   atlas-cert4-replay:
     name: atlas (cert4-replay)
     if: ${{ needs.plan.outputs.full == 'true' }}
@@ -773,7 +775,7 @@ jobs:
         run: |
           set -euo pipefail
           grep -F "verify-examples: uor-atlas verified (attestation " ci-evidence/vv.txt
-          grep -F "verify-examples: uor-atlas: 267 normalized verification records equal expected/verify (§29.5)" ci-evidence/vv.txt
+          grep -F "verify-examples: uor-atlas: 347 normalized verification records equal expected/verify (§29.5)" ci-evidence/vv.txt
       - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         if: ${{ !cancelled() }}
         with:

CHANGELOG.md

@@ -15,6 +15,18 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- UOR Atlas, #168: the census windows `CensusCert4` and `CensusCert10`
+  (`gramRange 4000 1000 = true` and `gramRange 10000 1000 = true`, each one
+  `of_decide_eq_true`) are proved from ten width-100 certificates each,
+  `CensusCert40` to `CensusCert49` and `CensusCert100` to `CensusCert109`,
+  joined by `gramRange_append` exactly as `CensusCert7` is from
+  `CensusCert70` to `CensusCert79`. Their statements are unchanged and their
+  importers are untouched; the Atlas root imports the twenty pieces
+  (`audit-atlas-exercise`, R4). In `.github/verify-shards.json` the `cert4`
+  shard elaborates the window-4 modules and `cert4-replay` replays them, and
+  `census-a` takes the window-10 pieces beside `CensusCert10`; the join
+  compares 347 normalized records (was 267). Atlas `expected/build` and
+  `expected/verify` are regenerated; no language data moves.
 - CI cost, #131 (SPEC.md §8.3, §9.4, `RP-14`): `ci.yml` begins with a `plan`
   job (`.github/ci-plan.sh`) that decides what a run is from the event alone.
   A draft pull request runs the `rest` leg and no other job (about 23 runner

VERIFICATION.md

@@ -7590,7 +7590,7 @@ change.
 `RP-14` reads the profile out of the matrix. The examples leg must name
 exactly that width, budget, and hints file; the width and the hints must parse
 with the verifier's own functions (`Operational::parse_width`,
-`Operational::parse_hints`), and the hints must name `CensusCert4`; any other
+`Operational::parse_hints`), and the hints must name `Census`; any other
 leg must name none; each variable is set once, from the row; and no profile may
 come from `vars.` or `inputs.`.
 
@@ -8950,3 +8950,37 @@ This is a finding about the fixture's premise, not a planted defect: the
 planted-defect evidence of the early refusal's bound is `conformance_sp_02`'s,
 which was not completed on any host before the train's CI run (the certificate
 A session's runs were killed twice by host restarts).
+
+## Census windows 4 and 10 as width-100 certificates (Issue #168)
+
+`CensusCert4` and `CensusCert10` each proved one window of 1,000 Gram types,
+`gramRange 4000 1000` and `gramRange 10000 1000`, by a single
+`of_decide_eq_true`, and their memory grew with the work of the whole window:
+on main run 39054719580
+`CensusCert4` took 1,419.3 s to elaborate and 2,248.5 s to replay at about
+15 GiB with 3.5 GiB of swap, and `CensusCert10` 114.6 s and 120.8 s at
+14.3 and 14.7 GiB with swap. Each window is now ten width-100 certificates,
+`CensusCert40` to `CensusCert49` and `CensusCert100` to `CensusCert109`, joined
+by `gramRange_append` as `CensusCert7` already was. The statements, the kernel
+`decide` proofs of each piece, and every importer are unchanged.
+
+Measured on run 39086315289 (the Atlas jobs of this tree):
+
+| Window | Elaboration (s) | Replay (s) | Largest piece (GiB) | Swap |
+| --- | ---: | ---: | ---: | --- |
+| 4 | 111.5 | 117.6 | 4.5 | none |
+| 10 | 118.1 | 115.4 | 5.6 | none |
+
+No `Census*` process swapped on that run; `Closure` and `ClosureOrbit` still
+did. The join wrote 347 normalized verification records, four for each of the
+twenty new modules beside the 267 before; they are this commit's
+`expected/verify`, and the hints of the 22 changed modules are that run's.
+
+### the census windows can fail
+
+A piece whose window is wrong, or a join that does not sum to the width of its
+window, is refused by the kernel when `CensusCert4` or `CensusCert10`
+elaborates, because each keeps the statement it had; a piece missing from the
+Atlas root is refused by `audit-atlas-exercise` (R4); a piece missing from the
+shard plan is refused by `cargo xtask ci-shards` and by the plan check of
+RP-14.

crates/conformance/src/cases/repository.rs

@@ -1449,7 +1449,7 @@ pub(crate) fn run(id: &str) {
                     ))
                     .expect("the committed hints are a hints file the verifier reads");
                     assert!(
-                        hints.contains_key("LexLeanExample.CensusCert4"),
+                        hints.contains_key("LexLeanExample.Census"),
                         "the hints cover the Atlas module that dominates the verification"
                     );
                 } else {
@@ -1750,7 +1750,7 @@ pub(crate) fn run(id: &str) {
             let join_job = job(&runs[crate::shards::JOIN]);
             assert!(
                 join_job.contains("grep -F \"verify-examples: uor-atlas verified (attestation \" ci-evidence/vv.txt")
-                    && join_job.contains("grep -F \"verify-examples: uor-atlas: 267 normalized verification records equal expected/verify (§29.5)\" ci-evidence/vv.txt"),
+                    && join_job.contains("grep -F \"verify-examples: uor-atlas: 347 normalized verification records equal expected/verify (§29.5)\" ci-evidence/vv.txt"),
                 "the join asserts that Atlas verified"
             );
             assert!(

examples/uor-atlas/expected/build/coverage/LexLeanExample/CensusCert100.coverage.json

@@ -0,0 +1 @@
+{"latex":[{"byte_end":226,"byte_start":0,"kind":"core-latex-preamble","origin":{"kind":"metadata","owner":"lexlean.core::coredata"}},{"byte_end":473,"byte_start":226,"kind":"core-latex-declaration","origin":{"kind":"metadata","owner":"lexlean.core::coredata"}},{"byte_end":908,"byte_start":473,"kind":"core-latex-declaration","origin":{"kind":"metadata","owner":"lexlean.core::coredata"}},{"byte_end":923,"byte_start":908,"kind":"core-latex-preamble","origin":{"kind":"metadata","owner":"lexlean.core::coredata"}}],"lean":[{"byte_end":15409,"byte_start":0,"kind":"core-lean-kernel-module","origin":{"kind":"metadata","owner":"lexlean.core::coredata"}}],"module":"CensusCert100","source":[{"binding":{"entry":"begin","kind":"structural","package":"lexlean.core"},"byte_end":6,"byte_start":0,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":7,"byte_start":6,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"env.lexlean","kind":"structural","package":"lexlean.core"},"byte_end":14,"byte_start":7,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":15,"byte_start":14,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":16,"byte_start":15,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"kind":"metadata","owner":"lexlean.core::env.lexlean"},"byte_end":26,"byte_start":16,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"kind":"metadata","owner":"lexlean.core::env.lexlean"},"byte_end":29,"byte_start":26,"class":"numeral","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":30,"byte_start":29,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"importmodule","kind":"structural","package":"lexlean.core"},"byte_end":44,"byte_start":31,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":45,"byte_start":44,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"kind":"metadata","owner":"lexlean.core::importmodule"},"byte_end":58,"byte_start":45,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":59,"byte_start":58,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"title","kind":"structural","package":"lexlean.core"},"byte_end":66,"byte_start":60,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":67,"byte_start":66,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"atlas-d1","form":"atlas-d1","kind":"form","package":"lexlean.uor.atlas"},"byte_end":93,"byte_start":67,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":94,"byte_start":93,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"begin","kind":"structural","package":"lexlean.core"},"byte_end":101,"byte_start":95,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":102,"byte_start":101,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"env.coremodule","kind":"structural","package":"lexlean.core"},"byte_end":112,"byte_start":102,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":113,"byte_start":112,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"coredata","kind":"structural","package":"lexlean.core"},"byte_end":123,"byte_start":114,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":124,"byte_start":123,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"kind":"metadata","owner":"lexlean.core::coredata"},"byte_end":1912,"byte_start":124,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":1913,"byte_start":1912,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"end","kind":"structural","package":"lexlean.core"},"byte_end":1918,"byte_start":1914,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":1919,"byte_start":1918,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"env.coremodule","kind":"structural","package":"lexlean.core"},"byte_end":1929,"byte_start":1919,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":1930,"byte_start":1929,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"end","kind":"structural","package":"lexlean.core"},"byte_end":1935,"byte_start":1931,"class":"control","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-open","kind":"structural","package":"lexlean.core"},"byte_end":1936,"byte_start":1935,"class":"delimiter","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"env.lexlean","kind":"structural","package":"lexlean.core"},"byte_end":1943,"byte_start":1936,"class":"word","path":"src/CensusCert100.lex.tex"},{"binding":{"entry":"brace-close","kind":"structural","package":"lexlean.core"},"byte_end":1944,"byte_start":1943,"class":"delimiter","path":"src/CensusCert100.lex.tex"}],"spec":"lexlean/coverage/1"}