Wave 3: fast certificate data builders (#177), release follow-ups (#187), and the Census windows as 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:
@@ -809,15 +811,14 @@ jobs:
           - { os: macos-15, target: aarch64-apple-darwin }
           - { os: windows-2022, target: x86_64-pc-windows-msvc }
     runs-on: ${{ matrix.os }}
-    # The Intel macOS runner is the slowest host: 51 to 61 minutes for this job
-    # before certificates A and B were kernel data, and past 120 minutes (the
-    # limit it then had, cancelled) once the stress families of SP-02 and the
-    # 9000-arm match of SP-08 built them (the suite took 2.9 times as long on
-    # the arm Linux runner, 1064 to 3051 seconds). A leg cancelled at the limit
-    # says nothing about the code, and the only defence against it was to run
-    # the leg again. Twice the slowest observed time leaves the limit a bound on
-    # a hung job, not a race with the runner's speed.
-    timeout-minutes: 300
+    # The Intel macOS runner took 51 to 61 minutes for this job before the data
+    # certificates, 100 with their stress arithmetic (#177), and 140 with BS-02's
+    # differential beside it (#190). A leg cancelled at the limit says nothing
+    # about the code, and the only defence against it was to run the leg again.
+    # Twice the slowest observed time leaves the limit a bound on a hung job,
+    # not a race with the runner's speed; the first gate run after #177's fix
+    # measures the new slowest time, and the limit follows it down.
+    timeout-minutes: 240
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - name: Install the pinned Rust toolchain

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
@@ -56,8 +68,13 @@ versions, and the entries below say what each tag does and does not claim.
   state. Certificates A and B are kernel data in which a repeated type is one
   node, so the chain verifies (it did not fit under `max_file_bytes` as text)
   and the lower bound counts no type node; what a small source still makes
-  large is the pairs of arms of a match, which the fixture now uses. The
-  fixture is refused with `LLS8002` in lowering, as before.
+  large is the pairs of arms of a match, which the fixture now uses. With
+  certificate A as kernel data, a pair of arms costs about 5.7 times its text
+  cost (`1018` against `180` sixteenths of a byte), so the widest match that
+  fits the default `max_file_bytes` falls from about `420` to `240`
+  constructors (`SP-02`, SPEC.md §17.17; a project with a wider match raises
+  `max_file_bytes`). The fixture is refused with `LLS8002` in lowering, as
+  before.
 - The preservation library's statement of
   `LexLeanTarget.TargetSemantics.fromOrdering.eq_1` is the one the elaborator
   makes for the generated module under the explicit byte-literal spelling
@@ -77,7 +94,7 @@ versions, and the entries below say what each tag does and does not claim.
   `Bytes` forms) to `(sign, mantissa, exponent)` over `nat` and `int`,
   rejecting out-of-width patterns and the non-finite biased exponents, and
   derives `round(a * b / c * 2^32)` scale ratios (ties to even) by exact
-  integer division; 43 theorems (39 in `Models.Recognizer`, 4 in `Models.Main`) are closed by `decide`. The change is to the
+  integer division; 47 theorems (43 in `Models.Recognizer`, 4 in `Models.Main`) are closed by `decide`. The change is to the
   `models` example and the register only: no compiler source moves.
 
 - Widening conversions (#114, SPEC.md §17.12 *Widening conversions*, `SM-32`,

CONFORMANCE.md

@@ -353,7 +353,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | ID | Level | Statement |
 | --- | --- | --- |
 | `SP-01` | `build` | Every production root of the committed examples lowers to a valid realization program in first-binding order, byte-identical across two lowerings, with an origin for every function and document type and exactly the root's eligibility closure; the lowering and certificate sources match no construct by default; a planted closure disagreement fails with LLI9001 and a planted default arm is refused. |
-| `SP-02` | `build` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it, and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; and in every case by generating each certificate under the limit, which stops it at the limit; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. |
+| `SP-02` | `build` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it (and a mixed shape that fits at its full scale of 256 is checked to fit and not edge-checked), and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; during certificate B's derivation at 12 bytes a kernel node; and for every certificate by weighing the finished module in the authoring notation it is recorded in against max_file_bytes before any file is staged; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. |
 | `SP-03` | `build` | On seeded inputs to every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning, the calculus interpreter's outcome on the lowered program equals the certificate's observation evaluated by Lean, and a planted disagreement is detected. |
 | `SP-04` | `build` | Every declaration of the preservation library is a row of a native module that pins its axioms exactly and depends on exactly them under the pinned Lean, the statement vocabulary SPEC.md quotes equals what the pinned Lean prints of the generated library, the shipped calculus modules are byte-equal to the compiler project's golden modules, and a library module or certificate with a forbidden token, a disallowed option, or a foreign import is refused. |
 | `SP-05` | `build` | Verification checks certificate A for every production root after named-root extraction and publishes each certificate, its audit output and process records, and a preservation.json valid against its schema whose digest the attestation binds; the lowered program and each target's crate the certificates are about are published and bound by that record, which also states the function each crate is invoked through and agrees with certificate E and the crate; a certificate the pinned Lean rejects fails with LLV7013 and a drifted preservation environment with LLV7014, before publication; and a pinned Lean that gives up on a certificate by heartbeats or recursion depth is reported as that rejection unless the module is at least a quarter of max_file_bytes, in which case, as when it is killed or out of memory, it is an exhausted resource, LLS8002. |