ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131)

.github/bdd-parts.json

@@ -0,0 +1,178 @@
+{
+  "remainder": "rest",
+  "parts": {
+    "compiler": [
+      "GC-02",
+      "GN-02",
+      "GN-03",
+      "GN-07",
+      "RS-01",
+      "RS-02",
+      "RS-03",
+      "RS-04",
+      "RS-05",
+      "RS-06",
+      "RS-07",
+      "RS-08",
+      "RS-09",
+      "RS-10",
+      "RS-11",
+      "RS-12",
+      "RS-13",
+      "RS-14",
+      "TC-03",
+      "TC-04",
+      "TC-05"
+    ],
+    "preservation": [
+      "GC-09",
+      "SP-01",
+      "SP-02",
+      "SP-03",
+      "SP-04",
+      "SP-06",
+      "SP-07",
+      "SP-08",
+      "SP-09",
+      "SP-10",
+      "SP-11",
+      "SP-12",
+      "SP-13",
+      "SP-14"
+    ],
+    "production": [
+      "CL-01",
+      "CL-03",
+      "CL-04",
+      "CL-06",
+      "CL-07",
+      "CL-08",
+      "CL-09",
+      "CL-10",
+      "CL-11",
+      "CL-12",
+      "CL-17",
+      "CL-23",
+      "EX-07",
+      "MD-01",
+      "MD-02",
+      "MD-03",
+      "MD-04",
+      "MD-05",
+      "MD-06",
+      "MD-07",
+      "MD-08",
+      "MD-09",
+      "MD-10",
+      "MD-11",
+      "MD-12",
+      "PX-01",
+      "PX-02",
+      "PX-03",
+      "PX-04",
+      "PX-05",
+      "PX-06",
+      "PX-07",
+      "PX-08",
+      "PX-09",
+      "PX-10",
+      "PX-11",
+      "PX-12",
+      "PX-13",
+      "SP-05"
+    ],
+    "verification": [
+      "AR-01",
+      "AR-02",
+      "AR-03",
+      "AR-04",
+      "AR-05",
+      "AR-06",
+      "AR-07",
+      "AR-08",
+      "AR-09",
+      "AR-10",
+      "AR-11",
+      "AR-12",
+      "AR-13",
+      "AR-14",
+      "AU-01",
+      "AU-02",
+      "AU-03",
+      "AU-04",
+      "AU-05",
+      "AU-06",
+      "AU-07",
+      "AU-08",
+      "AU-09",
+      "AU-10",
+      "AU-11",
+      "AU-12",
+      "EX-01",
+      "EX-02",
+      "GL-12",
+      "LN-01",
+      "LN-02",
+      "LN-03",
+      "LN-04",
+      "LN-05",
+      "LN-06",
+      "LN-07",
+      "LN-08",
+      "LN-09",
+      "LN-10",
+      "LN-11",
+      "LN-12",
+      "NE-01",
+      "NE-02",
+      "NE-03",
+      "NE-04",
+      "NE-05",
+      "NE-06",
+      "OR-01",
+      "OR-02",
+      "OR-03",
+      "OR-04",
+      "OR-05",
+      "OR-06",
+      "OR-07",
+      "OR-08",
+      "PF-18",
+      "SE-01",
+      "SE-02",
+      "SE-03",
+      "SE-04",
+      "SE-05",
+      "SE-06",
+      "SE-07",
+      "SE-08",
+      "SE-09",
+      "SE-10",
+      "SE-11",
+      "SE-12",
+      "VR-01",
+      "VR-02",
+      "VR-03",
+      "VR-04",
+      "VR-05",
+      "VR-06",
+      "VR-07",
+      "VR-08",
+      "VR-09",
+      "VR-10",
+      "VR-11",
+      "VR-12",
+      "VR-13",
+      "VR-14",
+      "VR-15",
+      "VR-16",
+      "VR-17",
+      "VR-18",
+      "VR-19",
+      "VR-20",
+      "VR-21",
+      "VR-22",
+      "VR-23"
+    ]
+  }
+}

.github/workflows/ci.yml

@@ -4,10 +4,20 @@
 # `just vv` is the single gate, run from a clean checkout on Linux x86-64 with
 # the exact pinned toolchains and no build cache: §9.4 says "from a clean
 # checkout", and a restored target directory is not one. CI runs its twelve
-# recipes as two legs at once, each its own clean checkout: `examples`, which
-# here verifies every example but UOR Atlas, and the other eleven in the order
-# of `vv`. Together they run every recipe of `vv` exactly once, so the gate is
-# the same and the wall time is the longer leg rather than the sum.
+# recipes as legs at once, each its own clean checkout: `examples`, which here
+# verifies every example but UOR Atlas, and `rest`, the other eleven in the
+# order of `vv`. Together they run every recipe of `vv` exactly once, so the
+# gate is the same and the wall time is the longest leg rather than the sum.
+#
+# `bdd`, the conformance suite, was most of the `rest` leg's time, and it runs
+# as the parts of `.github/bdd-parts.json` (§9.4): each `bdd-<part>` row runs
+# the recipe for the cases of one part, grouped so the cases that share a
+# fixture (a verified project, an export, a compiled environment) run in one
+# test process, and the `rest` leg runs the remainder, every test no other part
+# names. The part is named by the row through `LEXLEAN_BDD_PART`, the harness
+# selects its tests, and `inventory` proves from the harness's own lists that
+# the parts are the whole suite with every test in one part (RP-13). Each row
+# is its own clean checkout and build; nothing passes between rows or runs.
 #
 # UOR Atlas, whose native verification was most of the gate's time, is verified
 # as the parts of one run (§9.4): the shards of `.github/verify-shards.json`,
@@ -70,13 +80,17 @@ env:
 jobs:
   vv:
     name: just vv (${{ matrix.part }})
-    # A failing leg does not cancel the other: each leg's evidence is complete.
+    # A failing leg does not cancel the others: each leg's evidence is complete.
     strategy:
       fail-fast: false
       matrix:
         include:
-          - { part: examples, recipes: "examples", examples_part: "without:uor-atlas", width: "2", memory_kib: "12582912", hints: ".github/verify-hints.json" }
-          - { part: rest, recipes: "fmt-check model spec-links lint test features bdd inventory golden repro deny", examples_part: "", width: "", memory_kib: "", hints: "" }
+          - { part: examples, recipes: "examples", examples_part: "without:uor-atlas", bdd_part: "", width: "2", memory_kib: "12582912", hints: ".github/verify-hints.json" }
+          - { part: rest, recipes: "fmt-check model spec-links lint test features bdd inventory golden repro deny", examples_part: "", bdd_part: "rest", width: "", memory_kib: "", hints: "" }
+          - { part: bdd-compiler, recipes: "bdd", examples_part: "", bdd_part: "compiler", width: "", memory_kib: "", hints: "" }
+          - { part: bdd-preservation, recipes: "bdd", examples_part: "", bdd_part: "preservation", width: "", memory_kib: "", hints: "" }
+          - { part: bdd-production, recipes: "bdd", examples_part: "", bdd_part: "production", width: "", memory_kib: "", hints: "" }
+          - { part: bdd-verification, recipes: "bdd", examples_part: "", bdd_part: "verification", width: "", memory_kib: "", hints: "" }
     runs-on: ubuntu-24.04
     # Complete proof coverage is intentionally the long pole. GitHub-hosted
     # jobs permit six hours; a shorter local-style timeout would turn complete
@@ -90,6 +104,10 @@ jobs:
       # but the one the Atlas jobs below verify as parts; the other leg names
       # none, and runs no example.
       LEXLEAN_EXAMPLES_PART: ${{ matrix.examples_part }}
+      # The part of the `bdd` recipe this row runs (§9.4): a part of
+      # `.github/bdd-parts.json` on the `bdd-<part>` rows, its remainder on the
+      # `rest` leg; the `examples` leg runs no `bdd` and names none.
+      LEXLEAN_BDD_PART: ${{ matrix.bdd_part }}
       # The leg's resource profile (§22.11), read from its matrix row; an empty
       # value is the default. Operational only, like the telemetry: no artifact
       # records it and no identity contains it.

CHANGELOG.md

@@ -15,6 +15,28 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- The `bdd` recipe runs in CI as the parts of one run (SPEC.md §9.2, §9.4,
+  `RP-13`, `RP-14`, #131; no new diagnostic code, no new ID). The `rest` leg
+  took 111.5 minutes on the run that merged #152 (CI run 38905653756), 95.7 of
+  them `bdd`, one test process whose cases sum to 22,708 s over four threads.
+  `.github/bdd-parts.json` names four parts of the `repo-conformance` suite by
+  conformance ID, grouped so the cases that share a fixture built once per test
+  process run in one part, and a remainder, `rest`, that runs every test no
+  part names. The recipe is `cargo xtask bdd`: unset, `LEXLEAN_BDD_PART` leaves
+  it `cargo test -p repo-conformance --all-features`, which `just vv` and
+  `release.yml` run; named, it adds the part's harness filters (`--exact` and
+  its tests, or `--exact` and a `--skip` of every named test). `cargo xtask
+  check-test-inventory` lists every part with its filters and requires the
+  parts to be disjoint and their union to be `bdd`'s list (`RP-13`); `ci.yml`
+  runs each named part on a `bdd-<part>` row of the gate's matrix and the
+  remainder on the `rest` leg, every part on exactly one row (`RP-14`).
+- The join of a verification run as parts refuses a record of another
+  executable (#131, the review of #152; SPEC.md §9.4, §22.11, `VR-23`; no new
+  diagnostic code, no new ID). An imported elaboration or audit record must
+  name the join's own digest of `lean`, and a replay record its digest of
+  `leanchecker`; a mismatch is `LLI9001`, naming the record and both digests.
+  Every CI job installs the same pinned toolchain, so this held by practice
+  and is now checked.
 - Certificate E as kernel-term data (SPEC.md §17.17, `SP-14`; stage 1 of #89,
   stage 5 of #27). The composition certificate of every production root is no
   longer written as Lean text by `production/certificate.rs`: the compiler

CONFORMANCE.md

@@ -433,8 +433,8 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `RP-10` | `build` | The embedded compiler-semantics ID equals a clean recomputation from normative language and schema inputs. |
 | `RP-11` | `build` | Every public README capability claim is tied to a registered model ID and honesty level. |
 | `RP-12` | `build` | A release is refused unless the complete release criterion and all required artifacts are satisfied. |
-| `RP-13` | `build` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice. |
-| `RP-14` | `build` | The normative CI job runs every recipe of just vv exactly once, in two parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other leg at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. |
+| `RP-13` | `build` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. |
+| `RP-14` | `build` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. |
 
 ## runtime
 
@@ -554,7 +554,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `VR-20` | `build` | The verifier process width is an operational resource profile selected only by the environment, defaulting to 1 and refusing any malformed value with LLV7017, and it enters no lock, identity, or verified artifact. |
 | `VR-21` | `build` | A multi-module project whose imports form nontrivial frontiers verifies at width 1 and at a larger width to byte-identical verified directories and the same attestation identity, observed axiom sets, and policy rows, and no completion order orders a record or changes which failure is reported. |
 | `VR-22` | `build` | Performance telemetry is written only to the CI evidence directory the environment names, a verification with telemetry on publishes byte-identical artifacts to one without, and telemetry planted in a verified artifact fails the gate. |
-| `VR-23` | `build` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, or a join missing a record, is refused. |
+| `VR-23` | `build` | A project verified as the parts of one run, each shard running the processes its plan names with the oleans of the shards it needs and the join reading every shard's records, publishes a verified directory byte-identical to the whole verification's with the same attestation identity, and a shard whose plan leaves a module without its imports, a join missing a record, or a join reading a record of an executable other than its own, is refused. |
 
 ## Cited authorities
 

Justfile

@@ -44,11 +44,15 @@ features:
 # recipe, and `inventory` proves that between them nothing was lost or run
 # twice. The meta-gate target alone, which needs no Lean, is what the
 # honesty workflow runs (`cargo test -p repo-conformance --test bdd`).
+# `cargo xtask bdd` runs `cargo test -p repo-conformance --all-features`; in
+# CI, `LEXLEAN_BDD_PART` names the part of `.github/bdd-parts.json` a job runs
+# (§9.4), and unset, as here, the recipe runs the whole suite.
 bdd:
-    cargo test -p repo-conformance --all-features
+    cargo xtask bdd
 
 # RP-13: `test` and `bdd` partition `cargo test --workspace --all-features`,
-# test by test (listed with `-- --list`, not inferred from flags).
+# and the parts of `.github/bdd-parts.json` partition `bdd`, test by test
+# (listed with `-- --list`, not inferred from flags).
 inventory:
     cargo xtask check-test-inventory