From bb9bf562217628459a8b1b02e36ebb8ffc40977b Mon Sep 17 00:00:00 2001 From: humuhumu33 <68450279+humuhumu33@users.noreply.github.com> Date: Fri, 16 Oct 2026 08:57:02 +0100 Subject: [PATCH 1/2] ci: verify UOR Atlas as the parts of one run (#131) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The examples leg was 178 minutes on main, 156 of them UOR Atlas, whose import chain through Census and CensusCert4 bounds any single-runner schedule at about 65 minutes. Atlas is now verified as the shards of a committed plan (.github/verify-shards.json, checked by `cargo xtask ci-shards` against the import graph of the committed build) and a join, each a job of its own clean checkout in ci.yml, every process run exactly once per run and nothing crossing runs; the examples leg verifies every other example. The verifier runs as one part through `Engine::verify_part` (verify::partition): a shard elaborates, replays, and audits the modules of its plan with the oleans of the shards it needs and writes its records; the join reads every shard's records, judges each as its stage does, and publishes through the same policy, attestation, and publication as the whole verification. VR-23: the join of shards of peano-arithmetic equals its whole verification byte for byte with the same attestation identity, and three plans that cannot run are refused. RP-14 reads ci.yml against the plan. SPEC.md §9.4 and §22.11, the register (382 IDs), CHANGELOG, VERIFICATION.md with plants. The Atlas jobs do not run while a pull request is a draft. Co-Authored-By: Claude Fable 5.1 --- .github/verify-shards.json | 292 +++++++++ .github/workflows/ci.yml | 603 ++++++++++++++++++- CHANGELOG.md | 23 + CONFORMANCE.md | 3 +- README.md | 2 +- SPEC.md | 13 +- VERIFICATION.md | 117 ++++ crates/conformance/src/cases/operational.rs | 149 +++++ crates/conformance/src/cases/repository.rs | 374 ++++++++++-- crates/conformance/src/cases/verification.rs | 2 +- crates/conformance/src/lib.rs | 1 + crates/conformance/src/shards.rs | 435 +++++++++++++ crates/conformance/tests/conformance.rs | 5 + crates/lexlean/src/api.rs | 128 +++- crates/lexlean/src/lib.rs | 2 +- crates/lexlean/src/verify/child.rs | 74 +++ crates/lexlean/src/verify/mod.rs | 348 ++++++++++- crates/lexlean/src/verify/partition.rs | 536 +++++++++++++++++ features/suites/repository.feature | 14 +- features/suites/verification.feature | 7 + model/ids.toml | 8 +- xtask/Cargo.toml | 2 +- xtask/src/ci.rs | 41 ++ xtask/src/main.rs | 319 +++++++++- xtask/src/spec_links.rs | 4 +- 25 files changed, 3354 insertions(+), 148 deletions(-) create mode 100644 .github/verify-shards.json create mode 100644 crates/conformance/src/shards.rs create mode 100644 crates/lexlean/src/verify/partition.rs diff --git a/.github/verify-shards.json b/.github/verify-shards.json new file mode 100644 index 000000000..2f2e04651 --- /dev/null +++ b/.github/verify-shards.json @@ -0,0 +1,292 @@ +{ + "project": "uor-atlas", + "shards": { + "prefix": { + "needs": [], + "elaborate": [ + "LexLeanExample.Blocks", + "LexLeanExample.Category", + "LexLeanExample.Census", + "LexLeanExample.CensusClosure", + "LexLeanExample.Glue", + "LexLeanExample.Group", + "LexLeanExample.Parameters", + "LexLeanExample.Places", + "LexLeanExample.Prelude.Algebra", + "LexLeanExample.Prelude.Bitset", + "LexLeanExample.Prelude.Linear", + "LexLeanExample.Prelude.NumInstances", + "LexLeanExample.Prelude.Perm", + "LexLeanExample.Prelude.RingLemmas", + "LexLeanExample.Roots" + ], + "replay": [] + }, + "cert4": { + "needs": [ + "prefix" + ], + "elaborate": [ + "LexLeanExample.CensusCert4" + ], + "replay": [] + }, + "census-a": { + "needs": [ + "prefix" + ], + "elaborate": [ + "LexLeanExample.CensusCert10", + "LexLeanExample.CensusCert11", + "LexLeanExample.CensusCert5", + "LexLeanExample.CensusCert8" + ], + "replay": [ + "LexLeanExample.CensusCert10", + "LexLeanExample.CensusCert11", + "LexLeanExample.CensusCert5", + "LexLeanExample.CensusCert8" + ] + }, + "census-b": { + "needs": [ + "prefix" + ], + "elaborate": [ + "LexLeanExample.CensusCert0", + "LexLeanExample.CensusCert12", + "LexLeanExample.CensusCert13", + "LexLeanExample.CensusCert14", + "LexLeanExample.CensusCert15", + "LexLeanExample.CensusCert6", + "LexLeanExample.CensusCert7", + "LexLeanExample.CensusCert70", + "LexLeanExample.CensusCert71", + "LexLeanExample.CensusCert72", + "LexLeanExample.CensusCert73", + "LexLeanExample.CensusCert74", + "LexLeanExample.CensusCert75", + "LexLeanExample.CensusCert76", + "LexLeanExample.CensusCert77", + "LexLeanExample.CensusCert78", + "LexLeanExample.CensusCert79", + "LexLeanExample.CensusCert9" + ], + "replay": [ + "LexLeanExample.CensusCert0", + "LexLeanExample.CensusCert12", + "LexLeanExample.CensusCert13", + "LexLeanExample.CensusCert14", + "LexLeanExample.CensusCert15", + "LexLeanExample.CensusCert6", + "LexLeanExample.CensusCert7", + "LexLeanExample.CensusCert70", + "LexLeanExample.CensusCert71", + "LexLeanExample.CensusCert72", + "LexLeanExample.CensusCert73", + "LexLeanExample.CensusCert74", + "LexLeanExample.CensusCert75", + "LexLeanExample.CensusCert76", + "LexLeanExample.CensusCert77", + "LexLeanExample.CensusCert78", + "LexLeanExample.CensusCert79", + "LexLeanExample.CensusCert9", + "LexLeanExample.Group" + ] + }, + "census-c": { + "needs": [ + "prefix" + ], + "elaborate": [], + "replay": [ + "LexLeanExample.Blocks", + "LexLeanExample.Category", + "LexLeanExample.Census", + "LexLeanExample.CensusClosure", + "LexLeanExample.Glue", + "LexLeanExample.Parameters", + "LexLeanExample.Places", + "LexLeanExample.Prelude.Algebra", + "LexLeanExample.Prelude.Bitset", + "LexLeanExample.Prelude.Linear", + "LexLeanExample.Prelude.NumInstances", + "LexLeanExample.Prelude.Perm", + "LexLeanExample.Prelude.RingLemmas", + "LexLeanExample.Roots" + ] + }, + "census-d": { + "needs": [ + "prefix" + ], + "elaborate": [ + "LexLeanExample.ClosureOrbitCount", + "LexLeanExample.Functor", + "LexLeanExample.GroupSeries", + "LexLeanExample.Scales" + ], + "replay": [ + "LexLeanExample.ClosureOrbitCount", + "LexLeanExample.Functor", + "LexLeanExample.GroupSeries", + "LexLeanExample.Scales" + ] + }, + "cert4-replay": { + "needs": [ + "prefix", + "cert4" + ], + "elaborate": [], + "replay": [ + "LexLeanExample.CensusCert4" + ] + }, + "closure": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b" + ], + "elaborate": [ + "LexLeanExample.CensusComplete", + "LexLeanExample.Closure", + "LexLeanExample.ClosurePairs" + ], + "replay": [] + }, + "orbit": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "closure" + ], + "elaborate": [ + "LexLeanExample.ClosureOrbit" + ], + "replay": [ + "LexLeanExample.CensusComplete", + "LexLeanExample.Closure", + "LexLeanExample.ClosureOrbit", + "LexLeanExample.ClosurePairs" + ] + }, + "pairs-a": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "closure" + ], + "elaborate": [ + "LexLeanExample.ClosurePairCert0", + "LexLeanExample.ClosurePairCert1", + "LexLeanExample.ClosurePairCert2", + "LexLeanExample.ClosurePairCert3" + ], + "replay": [ + "LexLeanExample.ClosurePairCert0", + "LexLeanExample.ClosurePairCert1", + "LexLeanExample.ClosurePairCert2", + "LexLeanExample.ClosurePairCert3" + ] + }, + "pairs-b": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "closure" + ], + "elaborate": [ + "LexLeanExample.ClosurePairCert4", + "LexLeanExample.ClosurePairCert5", + "LexLeanExample.ClosurePairCert6", + "LexLeanExample.ClosurePairCert7" + ], + "replay": [ + "LexLeanExample.ClosurePairCert4", + "LexLeanExample.ClosurePairCert5", + "LexLeanExample.ClosurePairCert6", + "LexLeanExample.ClosurePairCert7" + ] + }, + "pairs-c": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "closure" + ], + "elaborate": [ + "LexLeanExample.ClosurePairCert10", + "LexLeanExample.ClosurePairCert11", + "LexLeanExample.ClosurePairCert8", + "LexLeanExample.ClosurePairCert9" + ], + "replay": [ + "LexLeanExample.ClosurePairCert10", + "LexLeanExample.ClosurePairCert11", + "LexLeanExample.ClosurePairCert8", + "LexLeanExample.ClosurePairCert9" + ] + }, + "pairs-d": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "closure" + ], + "elaborate": [ + "LexLeanExample.ClosurePairCert12", + "LexLeanExample.ClosurePairCert13", + "LexLeanExample.ClosurePairCert14", + "LexLeanExample.ClosurePairCert15" + ], + "replay": [ + "LexLeanExample.ClosurePairCert12", + "LexLeanExample.ClosurePairCert13", + "LexLeanExample.ClosurePairCert14", + "LexLeanExample.ClosurePairCert15" + ] + }, + "join": { + "needs": [ + "prefix", + "cert4", + "census-a", + "census-b", + "census-c", + "census-d", + "cert4-replay", + "closure", + "orbit", + "pairs-a", + "pairs-b", + "pairs-c", + "pairs-d" + ], + "elaborate": [ + "LexLeanExample.Atlas", + "LexLeanExample.ClosureGauge", + "LexLeanExample.ClosureOrbitTransport", + "LexLeanExample.ClosurePairComplete" + ], + "replay": [ + "LexLeanExample.Atlas", + "LexLeanExample.ClosureGauge", + "LexLeanExample.ClosureOrbitTransport", + "LexLeanExample.ClosurePairComplete" + ] + } + } +} diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b0c7f3e37..f10d4ccdd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,24 +4,36 @@ # `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`, whose -# native Atlas verification is most of the gate's time, 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. -# `honesty` is split out so a claim that has drifted from its evidence reads -# differently from broken code. +# 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. +# +# 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`, +# 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 +# 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 +# an artifact with the shards' output, and nothing crosses runs. The Atlas +# jobs do not run while a pull request is a draft; they run when it is marked +# ready, which the `pull_request` types below include. `honesty` is split out +# so a claim that has drifted from its evidence reads differently from broken +# code. # # The gate runs on the standard GitHub-hosted runner (SPEC.md §9.4); no larger -# runner is part of it. The `examples` leg verifies at the resource profile its -# matrix row names (§22.11): width 2, the scheduling hints committed in -# `.github/verify-hints.json`, and a 12 GiB budget for the summed expected +# runner is part of it. The `examples` leg and every Atlas shard verify at the +# resource profile named here (§22.11): width 2, the scheduling hints committed +# in `.github/verify-hints.json`, and a 12 GiB budget for the summed expected # peaks of the proof processes running at once. A profile changes the order and # overlap of processes and nothing they prove: the directory a project -# publishes is byte for byte the one of width 1, and the leg compares every -# example's records with `expected/verify` as it always did. The other leg -# names no profile, so it runs at the default. What the run cost, by recipe, -# stage, and module, is written to `ci-evidence/` (§22.12) and uploaded with -# the log. +# publishes is byte for byte the one of width 1, and the join compares Atlas's +# records with `expected/verify` as it always did. The other leg names no +# profile, so it runs at the default. What the run cost, by recipe, stage, and +# module, is written to `ci-evidence/` (§22.12) and uploaded with the log. # # Every version this file needs is read from the file that pins it — # `rust-toolchain.toml` through `rustup toolchain install`, `lean-toolchain` @@ -35,6 +47,7 @@ name: ci on: push: { branches: [main] } pull_request: + types: [opened, synchronize, reopened, ready_for_review] workflow_dispatch: # Read-only: nothing in this workflow writes to the repository or publishes a @@ -62,18 +75,21 @@ jobs: fail-fast: false matrix: include: - - { part: examples, recipes: "examples", 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", width: "", memory_kib: "", hints: "" } + - { 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: "" } runs-on: ubuntu-24.04 - # Native Atlas elaboration, per-module kernel replay, and per-module axiom - # audit are intentionally the long pole. GitHub-hosted jobs permit six - # hours; a shorter local-style timeout would turn complete proof coverage - # into a CI failure mode. + # Complete proof coverage is intentionally the long pole. GitHub-hosted + # jobs permit six hours; a shorter local-style timeout would turn complete + # proof coverage into a CI failure mode. timeout-minutes: 360 env: # Operational only (SPEC.md §22.12): no artifact records it, and the # telemetry directory is CI evidence, uploaded below. LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the `examples` recipe this leg runs (§9.4): every example + # 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 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. @@ -150,14 +166,17 @@ jobs: # evidence without running the expensive verifier a second time. # The leg that runs `examples` is chosen by the matrix, not by the log, # so a leg that should have verified Atlas and did not fails here. - - name: Assert native Atlas was verified by the acceptance gate + - name: Assert the leg verified every example but Atlas shell: bash run: | set -euo pipefail case " ${{ matrix.recipes }} " in *" examples "*) - 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: nat-add-zero verified (attestation " ci-evidence/vv.txt + if grep -F "verify-examples: uor-atlas" ci-evidence/vv.txt; then + echo "::error::the examples leg verified Atlas, which the Atlas jobs verify as parts (SPEC.md §9.4)" + exit 1 + fi ;; esac - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 @@ -168,6 +187,544 @@ jobs: if-no-files-found: error retention-days: 14 + # 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. + atlas-prefix: + name: atlas (prefix) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: shard:uor-atlas:prefix + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install the pinned Rust toolchain + run: rustup toolchain install + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # The one build of the gate's executable: every other Atlas job of the + # run takes it from the artifact rather than building it again, so a + # shard that waits on another pays the Lean toolchain and not a second + # clean Rust build. It is built from this clean checkout and crosses no + # run. + - name: Build the gate's executable from the clean checkout + run: cargo build --locked --package xtask + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the shard + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + target/debug/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: target/debug/xtask ci-summary --evidence ci-evidence + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-xtask + path: target/debug/xtask + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-part-prefix + path: ci-parts/prefix + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-prefix + path: ci-evidence + 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. + atlas-l1: + name: atlas (${{ matrix.shard }}) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + needs: [atlas-prefix] + strategy: { fail-fast: false, matrix: { shard: [cert4, census-a, census-b, census-c, census-d] } } + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: shard:uor-atlas:${{ matrix.shard }} + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # What the jobs of this run before this one wrote: the gate's executable + # and every shard's output so far, each under the name it was uploaded + # with. The verifier reads the shards this one needs and no other. + - name: Take the gate's executable and the shards before this one from the run + uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 + with: + pattern: atlas-* + path: ci-parts + - name: Place the parts under the names of their shards + shell: bash + run: | + set -euo pipefail + chmod +x ci-parts/atlas-xtask/xtask + for part in ci-parts/atlas-part-*; do + mv "$part" "ci-parts/${part#ci-parts/atlas-part-}" + done + ls ci-parts + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the shard + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: ci-parts/atlas-xtask/xtask ci-summary --evidence ci-evidence + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-part-${{ matrix.shard }} + path: ci-parts/${{ matrix.shard }} + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-${{ matrix.shard }} + path: ci-evidence + if-no-files-found: error + retention-days: 14 + + # The replay of `CensusCert4`, which needs its `.olean` and nothing after it. + atlas-cert4-replay: + name: atlas (cert4-replay) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + needs: [atlas-prefix, atlas-l1] + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: shard:uor-atlas:cert4-replay + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # What the jobs of this run before this one wrote: the gate's executable + # and every shard's output so far, each under the name it was uploaded + # with. The verifier reads the shards this one needs and no other. + - name: Take the gate's executable and the shards before this one from the run + uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 + with: + pattern: atlas-* + path: ci-parts + - name: Place the parts under the names of their shards + shell: bash + run: | + set -euo pipefail + chmod +x ci-parts/atlas-xtask/xtask + for part in ci-parts/atlas-part-*; do + mv "$part" "ci-parts/${part#ci-parts/atlas-part-}" + done + ls ci-parts + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the shard + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: ci-parts/atlas-xtask/xtask ci-summary --evidence ci-evidence + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-part-cert4-replay + path: ci-parts/cert4-replay + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-cert4-replay + path: ci-evidence + if-no-files-found: error + retention-days: 14 + + # `CensusComplete`, `Closure`, and `ClosurePairs`, which every module after + # them imports. + atlas-closure: + name: atlas (closure) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + needs: [atlas-prefix, atlas-l1] + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: shard:uor-atlas:closure + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # What the jobs of this run before this one wrote: the gate's executable + # and every shard's output so far, each under the name it was uploaded + # with. The verifier reads the shards this one needs and no other. + - name: Take the gate's executable and the shards before this one from the run + uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 + with: + pattern: atlas-* + path: ci-parts + - name: Place the parts under the names of their shards + shell: bash + run: | + set -euo pipefail + chmod +x ci-parts/atlas-xtask/xtask + for part in ci-parts/atlas-part-*; do + mv "$part" "ci-parts/${part#ci-parts/atlas-part-}" + done + ls ci-parts + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the shard + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: ci-parts/atlas-xtask/xtask ci-summary --evidence ci-evidence + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-part-closure + path: ci-parts/closure + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-closure + path: ci-evidence + if-no-files-found: error + retention-days: 14 + + # The shards after `closure`: `ClosureOrbit` with the replays of the + # closure modules, and the `ClosurePairCert*` modules in four bins. + atlas-l3: + name: atlas (${{ matrix.shard }}) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + needs: [atlas-closure] + strategy: { fail-fast: false, matrix: { shard: [orbit, pairs-a, pairs-b, pairs-c, pairs-d] } } + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: shard:uor-atlas:${{ matrix.shard }} + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # What the jobs of this run before this one wrote: the gate's executable + # and every shard's output so far, each under the name it was uploaded + # with. The verifier reads the shards this one needs and no other. + - name: Take the gate's executable and the shards before this one from the run + uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 + with: + pattern: atlas-* + path: ci-parts + - name: Place the parts under the names of their shards + shell: bash + run: | + set -euo pipefail + chmod +x ci-parts/atlas-xtask/xtask + for part in ci-parts/atlas-part-*; do + mv "$part" "ci-parts/${part#ci-parts/atlas-part-}" + done + ls ci-parts + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the shard + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: ci-parts/atlas-xtask/xtask ci-summary --evidence ci-evidence + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: atlas-part-${{ matrix.shard }} + path: ci-parts/${{ matrix.shard }} + if-no-files-found: error + retention-days: 1 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-${{ matrix.shard }} + path: ci-evidence + if-no-files-found: error + retention-days: 14 + + # The join: the last four modules, then every shard's records in the + # canonical order, the attestation, publication, and the comparison with + # `expected/verify`. + atlas-join: + name: atlas (join) + if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + needs: [atlas-prefix, atlas-l1, atlas-cert4-replay, atlas-closure, atlas-l3] + runs-on: ubuntu-24.04 + timeout-minutes: 360 + env: + LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence + # The part of the examples recipe this job runs (§9.4), and where the + # parts of the run exchange their output. + LEXLEAN_EXAMPLES_PART: join:uor-atlas + LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts + # The resource profile of the examples leg (§22.11), the same for every + # shard; operational only. + LEXLEAN_VERIFY_WIDTH: "2" + LEXLEAN_VERIFY_MEMORY_KIB: "12582912" + LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install elan and the pinned Lean toolchain + run: | + set -euo pipefail + curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + "$HOME/.elan/bin/elan" toolchain install "$(cat lean-toolchain)" + # What the jobs of this run before this one wrote: the gate's executable + # and every shard's output so far, each under the name it was uploaded + # with. The verifier reads the shards this one needs and no other. + - name: Take the gate's executable and the shards before this one from the run + uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2 + with: + pattern: atlas-* + path: ci-parts + - name: Place the parts under the names of their shards + shell: bash + run: | + set -euo pipefail + chmod +x ci-parts/atlas-xtask/xtask + for part in ci-parts/atlas-part-*; do + mv "$part" "ci-parts/${part#ci-parts/atlas-part-}" + done + ls ci-parts + - name: Reserve bounded overflow memory for native Atlas + run: | + set -euo pipefail + sudo fallocate -l 4G "$RUNNER_TEMP/lexlean-atlas.swap" + sudo chmod 600 "$RUNNER_TEMP/lexlean-atlas.swap" + sudo mkswap "$RUNNER_TEMP/lexlean-atlas.swap" + sudo swapon "$RUNNER_TEMP/lexlean-atlas.swap" + sudo sysctl vm.swappiness=10 + swapon --show + - name: Run the join (the last modules, every shard's records, the attestation) + shell: bash + run: | + set -euo pipefail + mkdir -p ci-evidence ci-parts + sample_resources() { + set +e + while true; do + avail=$(awk '/^MemAvailable:/ {print $2}' /proc/meminfo) + swap=$(awk '/^SwapTotal:/ {t=$2} /^SwapFree:/ {f=$2} END {print t-f}' /proc/meminfo) + top=$( (ps -eo rss= --sort=-rss || true) | awk 'NR==1 {print $1}') + printf '%s\t%s\t%s\t%s\n' "$(date +%s.%N | cut -c1-14)" "$avail" "$swap" "${top:-0}" + sleep 5 + done + } + sample_resources > ci-evidence/resources.tsv & + sample_pid=$! + trap 'kill "$sample_pid" 2>/dev/null || true; wait "$sample_pid" 2>/dev/null || true' EXIT + ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt + - name: Summarize the run's timing and memory + if: ${{ !cancelled() }} + run: ci-parts/atlas-xtask/xtask ci-summary --evidence ci-evidence + # The join publishes Atlas's verified directory and compares its records + # with `expected/verify` as the examples leg did; these lines are what it + # prints when it has, and a join that did not print them fails here. + - name: Assert native Atlas was verified by the acceptance gate + shell: bash + 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 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + if: ${{ !cancelled() }} + with: + name: acceptance-gate-evidence-atlas-join + path: ci-evidence + if-no-files-found: error + retention-days: 14 + # §8.3: the crate builds and its non-Lean tests pass on every supported # host. This job installs no Lean toolchain on purpose — that is the # property under test. A case whose assertions need the pinned toolchain diff --git a/CHANGELOG.md b/CHANGELOG.md index 45ff6c084..fb0db6ae9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,29 @@ versions, and the entries below say what each tag does and does not claim. ## Unreleased +- UOR Atlas is verified in CI as the parts of one run (SPEC.md §9.4, §22.11, + `RP-14`, `VR-23`, #131; no new diagnostic code). The examples leg, 178 + minutes on `main` at 514e95ad (CI run 38716449420), was 156 minutes of + Atlas, whose import chain through `Census` and `CensusCert4` no schedule on + one runner finishes in under about 65 minutes. `.github/verify-shards.json` + partitions Atlas's verification into fourteen shards and a join, checked by + `cargo xtask ci-shards` against the import graph of the committed build: + every module elaborated by one shard and replayed by one, every import + elaborated by the shard or by one it needs. The verifier runs as one part + through `Engine::verify_part` (`verify::partition`): a shard runs the + prelude whole, then elaborates, replays, and audits the modules of its plan + with the `.olean` files of the shards it needs, and writes its records; the + join reads every shard's records, judges each as its stage does, and + publishes through the same policy, attestation, and publication as the whole + verification, byte-identical to it and with the same attestation identity + (`VR-23`, on `peano-arithmetic`). `cargo xtask verify-examples` runs the + part `LEXLEAN_EXAMPLES_PART` names: `without:uor-atlas` on the examples leg, + `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs; unset, the + recipe is unchanged. `ci.yml` runs the shards as jobs after the jobs of the + shards they need, from the one executable the `prefix` job builds, with the + shards' output as artifacts of the run and nothing across runs, and not while + a pull request is a draft. The register has 382 IDs. + - Certificates write a list of any length as a term Lean elaborates without binders (SPEC.md §17.17, `SP-13`, #97; no new diagnostic code). Lean's `[…]` macro splits a literal of more than 32 elements in halves under diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 6bdb88140..554953931 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -428,7 +428,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | `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 the other at the default, with no cache, path filter, or skipped recipe, and each leg uploads its CI evidence. | +| `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. | ## rust-backend @@ -539,6 +539,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. | ## Cited authorities diff --git a/README.md b/README.md index e3b19b843..f631c0323 100644 --- a/README.md +++ b/README.md @@ -137,7 +137,7 @@ just vv # the complete normative acceptance gate (SPEC.md §9.2) just release # vv, then the §30 release criterion; refused until 1.0.0 ``` -All 381 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed. +All 382 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed. The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement. diff --git a/SPEC.md b/SPEC.md index 009cc3dfd..84bf45a61 100644 --- a/SPEC.md +++ b/SPEC.md @@ -679,9 +679,11 @@ Its post-create command MUST install the pinned Lean toolchain explicitly and MU `ci.yml` MUST run every recipe of `just vv` from a clean checkout on Linux x86-64. It MUST install the exact Rust toolchain, Lean 4.32.1 through `elan`, `just`, and `cargo-deny`. -The job runs the recipes as two legs of one matrix, at once, each from its own clean checkout: `examples` alone, and the other eleven recipes in the order of `vv`. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. Together the legs run every recipe of `vv` exactly once, and the gate passes only when both legs pass, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longer leg rather than the sum (on the runner, `examples` is about 77% of the recipes' time). `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. +The job runs the recipes as two legs of one matrix, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas, and the other eleven recipes in the order of `vv`. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv` exactly once and every example once, and the gate passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. -Both legs run on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of each leg is named by its matrix row and by nothing else, no repository or workflow variable and no input: the `examples` leg verifies at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other leg names no profile and runs at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg still requires every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. 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. Each leg writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it: the gate log (`just --timestamp` stamps each recipe's first command, which is how a recipe is timed without changing it), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when `just vv` failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. +UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and not while a pull request is a draft: they run when it is opened, pushed to, reopened, or marked ready. + +Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other leg names no profile and runs at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. 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`; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. `honesty.yml` MUST run the model/honesty gate separately so claim drift is distinguishable from code failure. @@ -7522,6 +7524,8 @@ The profile changes how processes are scheduled and nothing else: For every project, the directory published at any profile equals, byte for byte, the directory published at width 1 without hints and without a budget, on the same host and toolchain; in particular the attestation ID, the observed axiom sets, the policy rows, the canonical compiler input, and every normalized verification record (§29.5) are identical. +A verification may also run as the parts of one run (§9.4): each part runs the processes of its plan at the profile of its own host, a part reads from another only the `.olean` files and process records that part's processes produced, and the join judges every record it reads as the stage that produced it judges its own. The directory the join publishes equals, byte for byte, the one the whole verification publishes, attestation ID included (`VR-23`); a part is defined for a project without production roots and without PDF rendering. + ### 22.12 Performance telemetry Wall time, resident-set and swap measurements, scheduling and completion order, and the host's memory and processor count depend on the host. `lexlean verify` records them only when the environment variable `LEXLEAN_CI_TELEMETRY` names a directory, as JSON lines appended to `verify-telemetry.jsonl` in it: one line for the start of a verification, one for each stage, each frontier of module elaboration, and each process (with the peak resident set and swap of the process and what it started, where the host exposes them), and one for the end. `cargo xtask verify-examples` appends one line per example to `examples-telemetry.jsonl` of the same directory, and the conformance runner one line per case, with its wall time, to `cases-telemetry.jsonl`. The directory is CI evidence, `ci-evidence/` in CI (§9.4). @@ -8857,7 +8861,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `RP-11` | `repository` | Every public README capability claim is tied to a registered model ID and honesty level. | §27 | | `RP-12` | `repository` | A release is refused unless the complete release criterion and all required artifacts are satisfied. | §30 | | `RP-13` | `repository` | 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. | §9.2 | -| `RP-14` | `repository` | 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 the other at the default, with no cache, path filter, or skipped recipe, and each leg uploads its CI evidence. | §9.4 | +| `RP-14` | `repository` | 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. | §9.4 | | `CF-01` | `configuration-lock` | Project configuration accepts exactly the project/1 schema and rejects unknown or missing fields. | §10.1 | | `CF-02` | `configuration-lock` | Every operational limit is explicit, positive, parsed with checked arithmetic, and has no hidden default. | §10.2 | | `CF-03` | `configuration-lock` | Configured paths resolve within the project under the specified UTF-8 and nonsymlink rules. | §10.1, §25.1 | @@ -9052,6 +9056,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `VR-20` | `verification` | 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. | §22.11, §23.1 | | `VR-21` | `verification` | 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. | §22.3, §22.4, §22.11 | | `VR-22` | `verification` | 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. | §22.12 | +| `VR-23` | `verification` | 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. | §9.4, §22.11 | | `CL-01` | `cli-api` | Global options and upward project discovery obey the exact CLI contract. | §23.1, §23.2 | | `CL-02` | `cli-api` | Init creates the complete canonical skeleton only in an absent or empty destination and never overwrites. | §23.4 | | `CL-03` | `cli-api` | Lock check, local update, and explicit network acquisition obey their exact mutually exclusive behavior. | §23.4 | @@ -9227,7 +9232,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `AU-11` | `authoring` | Malformed core notation fails closed and never panics: an unclosed delimiter, a keyword used as a name, a label that is not the number of its node, a reference to a node not yet written, a numeral with a redundant leading zero, a statement that defines no node, a nesting beyond the bound, and every single-token deletion and duplication of a committed module fail with a registered code at a position in the notation or link to a module that decodes. | §17.21.8 | | `AU-12` | `authoring` | A core module written with names for its statements and its variables reads to exactly the module its canonical notation reads to, and the canonical notation keeps the names of the binders and writes the numbers of the statements: a variable is written by the name of its binder exactly when no nearer binder has the name, a constant a binder in scope is named like is written as a string, a theorem added to the certification library by name reads to the committed module and is written as the committed bytes, and an unknown or repeated statement name and a variable given universe levels are refused with a position. | §17.21.8 | -**Total required capability IDs:** 381. +**Total required capability IDs:** 382. No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors. diff --git a/VERIFICATION.md b/VERIFICATION.md index 6e462c205..71b444e07 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -7434,3 +7434,120 @@ Removed: each edit was restored; `conformance_au_01`..`conformance_au_12` pass. arbitrary canonical JSON values (`surface::generic`), and every alternative of the schema its own sample (`surface::semantic`), as unit tests of the `lexlean` crate. + +## UOR Atlas as the parts of one run (Issue #131) + +Issue #131 asked why every pull request's gate takes three hours and what +would shorten it without a weaker proof obligation. On `main` at `514e95ad` +(CI run 38716449420) the `examples` leg took 178 minutes, 156 of them the +verification of UOR Atlas (elaboration 5,047 s, replay 4,286 s); the `rest` +leg took 76 minutes. Atlas's 66 modules are not independent: 63 of its sources +declare `\importmodule`, the generated Lean imports them as `public import`, +and the chain `Roots → Blocks → Places → Group → Census → CensusCert4`, then +`CensusComplete → Closure → ClosurePairs → ClosurePairCert* → … → Atlas`, is 20 +deep. From the committed hints and the measured replays, the elaboration of +that chain up to `CensusCert4` (2,687 s) and the replay of `CensusCert4` +(1,229 s) bound any schedule of today's modules at about 65 minutes, however +many runners it has; a single 16 GB runner at width 2 cannot overlap the four +modules that peak near 15 GiB with anything, which is where the other 90 +minutes went. The maintainer's reading on the issue, that a content-addressed +certificate of main's proof would skip Atlas on five of the 34 merged pull +requests once its key covered the compiler sources, stands; `§9.4`'s sentence +on caches is unchanged. + +What changed is where the processes run, not which run. Atlas's verification +is partitioned into the shards of `.github/verify-shards.json`, each a job of +its own clean checkout on the standard runner: `prefix` elaborates the import +closure of `CensusCert4` (15 modules, 1,399 s of elaboration); `cert4` that +module alone; `census-a` to `census-d` the other `CensusCert*` modules, the +replays of the prefix, and the modules that import only the prefix; `closure` +the three modules every later one imports; `orbit` and `pairs-a` to `pairs-d` +the rest; `cert4-replay` the one replay that takes 20 minutes; and the `join` +the last four modules, then every shard's records, the attestation, and the +comparison with `expected/verify`. The critical path is `prefix` (23 minutes +of elaboration at width 2), `cert4` (22), `closure` (3), the `pairs` shards (11 +each), the join (under 2), plus each job's set-up: the Lean toolchain and, +once, the Rust build of the gate's executable, which the `prefix` job uploads +and the other jobs take from the run. That is an estimate of 80 to 90 minutes +for the Atlas side against 178; the first CI run of the change is the +measurement, and the `rest` leg (76 minutes, 64 of them `bdd`) is then the +longer one. + +The verifier runs as one part through `Engine::verify_part` +(`verify::partition`, SPEC.md §9.4, §22.11). A shard runs the prelude whole +(certificate generation, the preflights, staging, the generated-source audit, +the probe), seeds the placed set with the modules whose `.olean` arrived from +the shards it needs, elaborates the modules of its plan in the same +topological frontiers, replays and audits the modules its plan names, and +moves its `.olean` tree (intermediates included, a later shard's elaboration +reads them) and its process records to its output directory; it publishes +nothing. The join does the same for its own plan, reads every other part's +records (`ChildRecord::from_json`, which checks each stream against its +digest), judges an imported elaboration as the elaboration stage judges its +own (exit 0, silent), an imported replay as the replay stage does (exit 0, +else `LLV7003`), and an imported audit member as the audit stage does (exit 0, +silent, its printed set parsed against the member's declarations, else +`LLV7004`), and assembles the attestation's process list in the canonical +order of §22.11 (`partition::elaboration_order`: the frontiers in module +order, then replays in sorted name, then the family) from whichever part +produced each record. A module without a record from any part, a record of a +process no module owns, two parts that wrote the same `.olean` or record, and +a shard whose plan elaborates a module before its imports (`module order did +not converge: … imports …`) are refused. A part is defined for a project +without production roots and without PDF rendering; Atlas is such a project. + +`VR-23` verifies `peano-arithmetic` whole and as two shards and a join over +its committed import graph (the first frontier; the second, replaying both; +the rest), and requires the join's verified directory to equal the whole's +byte for byte with the same attestation ID, then refuses the three plans +above. `RP-14` reads `ci.yml` against the plan: every shard run by exactly one +job, each job waiting (through the job graph) for the jobs of the shards its +shard needs and never for a row of its own matrix, the examples profile on +every Atlas job, the one `cargo build` in the `prefix` job and every other job +taking the executable and the shards' output from the run (`pattern: +atlas-*`, never a `run-id`), the shard output uploaded under the shard's name, +the join asserting Atlas's two lines, the draft condition on every Atlas job +and no other, and the `ready_for_review` type that reruns them. The plan +itself is checked by `cargo xtask ci-shards` and inside `RP-14` by +`repo_conformance::shards::check`. + +### the partition can fail + +Each record is a defect planted in `.github/verify-shards.json` or `ci.yml`, +then `cargo test -p repo-conformance --test conformance -- --exact +conformance_rp_14` (the plan's defects also fail `cargo xtask ci-shards` with +the same line), and the failure, after which the file was restored. + +- **a module replayed by two shards** (`CensusCert4` added to `census-a`'s + replay): `` `LexLeanExample.CensusCert4` is replayed by `census-a` and by + `cert4-replay` ``. +- **a shard elaborating a module before its imports** (`cert4` with no needs): + `` shard `cert4` elaborates `LexLeanExample.CensusCert4`, whose import + `LexLeanExample.CensusClosure` is elaborated by no shard it needs ``. +- **a module elaborated by no shard** (`Atlas` dropped from the join): + `` `LexLeanExample.Atlas` is elaborated by no shard ``. +- **a job that no longer waits for the shards it needs** (`atlas-closure` with + `needs: [atlas-prefix]`): `` §9.4: `closure` runs in `atlas-closure`, which + does not wait for `atlas-l1`, the job of `cert4` it needs ``. +- **an Atlas job without the draft condition** (`atlas-l3`): `` §9.4: + `atlas-l3` waits only for a pull request to leave draft ``. +- **a second `cargo build`** (in `atlas-closure`): `ci.yml builds the gate's + executable once` (`left: 2, right: 1`). +- **a shard run by two jobs** (`pairs-a` added to `atlas-l1`'s matrix): + `` §9.4: the shard `pairs-a` is run by two jobs ``. +- **the examples leg verifying every example** (`examples_part` emptied): + `§9.4: the examples leg's profile and part` (`left: [.., ""]`, `right: [.., + "without:uor-atlas"]`). +- **a cache action in a shard job**: `` ci.yml has no `actions/cache` ``. +- **the join reading another run's artifacts** (`run-id` on its download): + `` §9.4: `atlas-join` reads the artifacts of this run only ``. + +Two defects were found by the cases and not by review: a shard exported the +`.olean` files it had imported along with its own, so the join refused the +duplicate (`` `oleans/PeanoArithmetic/Addition.ir` was written by two parts of +the run ``; `export` now moves only the modules of the shard's plan), and the +join assembled the imported elaboration and replay records into the +attestation without publishing them, so the directory it published had no +`process/lean/PeanoArithmetic.Addition.json` and `verify-examples` refused it +against `expected/verify` (R10). Both are what `VR-23` and the end-to-end run +of `verify-examples` as two shards and a join of `peano-arithmetic` now check. diff --git a/crates/conformance/src/cases/operational.rs b/crates/conformance/src/cases/operational.rs index a2d8c31b6..e42ce5ff5 100644 --- a/crates/conformance/src/cases/operational.rs +++ b/crates/conformance/src/cases/operational.rs @@ -24,6 +24,7 @@ pub(crate) fn run(id: &str) { "VR-20" => width_is_operational(), "VR-21" => width_invariance(), "VR-22" => telemetry_is_noncanonical(), + "VR-23" => parts_equal_the_whole(), other => panic!("no operational case for {other}"), } } @@ -756,3 +757,151 @@ fn telemetry_is_noncanonical() { .expect("an unwritable sink does not fail verification"); assert_eq!(unwritable.attestation_id, without.attestation_id); } + +/// VR-23: a verification run as the parts of one run (SPEC.md §9.4) equals +/// the whole, and a plan that cannot run is refused. +fn parts_equal_the_whole() { + use lexlean::{VerifyPart, VerifyPartOutcome, VerifyPlan}; + if !support::lean_backed("VR-23") { + return; + } + let example = "peano-arithmetic"; + let whole_project = P::copy_example(example); + let whole = verify_at(&whole_project, Operational::new(1, None).expect("width 1")) + .expect("the whole verification"); + + // The plan, from the example's committed build: its first topological + // frontier is one shard, its second another that also replays the first, + // and the rest is the join's. + let graph = crate::shards::import_graph( + support::repo_root() + .join("examples") + .join(example) + .as_std_path(), + ) + .expect("the import graph reads from the committed build"); + let mut placed: std::collections::BTreeSet = std::collections::BTreeSet::new(); + let mut remaining: Vec = graph.keys().cloned().collect(); + let mut frontiers: Vec> = Vec::new(); + while !remaining.is_empty() { + let ready: Vec = remaining + .iter() + .filter(|module| graph[*module].iter().all(|import| placed.contains(import))) + .cloned() + .collect(); + assert!(!ready.is_empty(), "the import graph converges"); + placed.extend(ready.iter().cloned()); + remaining.retain(|module| !ready.contains(module)); + frontiers.push(ready); + } + assert!( + frontiers.len() >= 3, + "the fixture has at least three frontiers: {frontiers:?}" + ); + let first = frontiers[0].clone(); + let second = frontiers[1].clone(); + let rest: Vec = frontiers[2..].concat(); + let parts = tempfile::tempdir().expect("tempdir"); + let dir = |name: &str| { + camino::Utf8PathBuf::from_path_buf(parts.path().join(name)).expect("utf8 tempdir") + }; + // Each part verifies its own copy of the project; the copies live until + // the end of the case, as the join's published directory is inside one. + let copies: std::cell::RefCell> = std::cell::RefCell::new(Vec::new()); + let run_part = |part: VerifyPart| -> Result { + let _environment = support::env_shared(); + let project = P::copy_example(example); + let outcome = Operational::new(1, None).expect("width 1").scoped(|| { + project.engine().verify_part( + VerifyRequest { + selection: Selection::Entrypoints, + }, + part, + ) + }); + copies.borrow_mut().push(project); + outcome + }; + let plan = |elaborate: &[String], replay: &[String]| VerifyPlan { + elaborate: elaborate.to_vec(), + replay: replay.to_vec(), + }; + + let a = run_part(VerifyPart::Shard { + plan: plan(&first, &[]), + imports: vec![], + output: dir("a"), + }) + .expect("the first shard"); + assert!( + matches!(a, VerifyPartOutcome::Shard { processes, .. } if processes == first.len()), + "the first shard ran its elaborations and nothing else" + ); + let mut first_and_second = first.clone(); + first_and_second.extend(second.iter().cloned()); + let b = run_part(VerifyPart::Shard { + plan: plan(&second, &first_and_second), + imports: vec![dir("a")], + output: dir("b"), + }) + .expect("the second shard, with the first's oleans"); + assert!( + matches!(b, VerifyPartOutcome::Shard { processes, .. } if processes == second.len() + 2 * first_and_second.len()), + "the second shard ran its elaborations and the replays and audits of both" + ); + let joined = match run_part(VerifyPart::Join { + plan: plan(&rest, &rest), + parts: vec![dir("a"), dir("b")], + }) + .expect("the join") + { + VerifyPartOutcome::Verified(verified) => verified, + VerifyPartOutcome::Shard { .. } => panic!("the join publishes"), + }; + assert_eq!( + joined.attestation_id, whole.attestation_id, + "the join and the whole verification have one attestation identity" + ); + assert_trees_equal(&tree(&joined.root), &tree(&whole.root), "whole and joined"); + + // A shard whose plan elaborates a module before its imports does not + // converge, and names the import. + let error = run_part(VerifyPart::Shard { + plan: plan(&second, &[]), + imports: vec![], + output: dir("c"), + }) + .map(|_| ()) + .expect_err("a module elaborated before its imports"); + let text = error.to_string(); + assert!( + text.contains("module order did not converge") && text.contains(&first[0]), + "{text}" + ); + // A join that is handed one shard too few has no record of a process. + let error = run_part(VerifyPart::Join { + plan: plan(&rest, &rest), + parts: vec![dir("b")], + }) + .map(|_| ()) + .expect_err("a join missing a shard"); + let text = error.to_string(); + assert!( + text.contains("from any part of the run") || text.contains("module order did not converge"), + "{text}" + ); + // A join whose plan leaves a replay to no part has no record of it. + let error = run_part(VerifyPart::Join { + plan: plan(&rest, &rest[1..]), + parts: vec![dir("a"), dir("b")], + }) + .map(|_| ()) + .expect_err("a replay no part ran"); + let text = error.to_string(); + // The audit member of the module is placed with its replay, so the hole + // is seen at the audit stage, before the records are assembled. + assert!( + text.contains("from any part of the run") && text.contains(&rest[0]), + "{text}" + ); +} diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index d9e416a14..45397902a 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -411,7 +411,7 @@ pub(crate) fn run(id: &str) { let model = repo_model::Model::load(&root.join("model").into_std_path_buf()) .expect("the model loads"); let table = spec_table(); - assert_eq!(table.len(), 381, "§31 has 381 rows"); + assert_eq!(table.len(), 382, "§31 has 382 rows"); assert_eq!(model.ids.id.len(), table.len(), "register row count"); for ((spec_id, spec_suite, spec_statement), row) in table.iter().zip(model.ids.id.iter()) @@ -999,19 +999,59 @@ pub(crate) fn run(id: &str) { // width and keeps no cache, filter, or skipped recipe. "RP-14" => { let ci = root_file(".github/workflows/ci.yml"); - assert!( - ci.contains(" runs-on: ubuntu-24.04\n # Native Atlas"), - "the normative job runs on the standard runner" - ); for variable in ["vars.", "inputs."] { assert!( !ci.contains(variable), "the gate selects no runner and no profile from outside the file: `{variable}`" ); } + // The jobs of the file, each with its lines: a key at two spaces + // of indentation under `jobs:` opens one. + let jobs_text = &ci[ci.find("\njobs:\n").expect("a jobs section") + 7..]; + let mut jobs: Vec<(String, String)> = Vec::new(); + for line in jobs_text.lines() { + if line.starts_with(" ") + && !line.starts_with(" ") + && line.trim_end().ends_with(':') + { + jobs.push((line.trim().trim_end_matches(':').to_owned(), String::new())); + } else if let Some((_, body)) = jobs.last_mut() { + body.push_str(line); + body.push('\n'); + } + } + let job = |name: &str| -> &str { + &jobs + .iter() + .find(|(key, _)| key == name) + .unwrap_or_else(|| panic!("§9.4: the job `{name}`")) + .1 + }; + let atlas_jobs: Vec<&(String, String)> = jobs + .iter() + .filter(|(key, _)| key.starts_with("atlas-")) + .collect(); + assert!(!atlas_jobs.is_empty(), "§9.4: the Atlas jobs"); + // Every gate job runs on the standard runner (§9.4); only the host + // matrix runs elsewhere, on the hosts of §8.3. + for (key, body) in &jobs { + if key == "host-matrix" { + continue; + } + assert!( + body.contains("\n runs-on: ubuntu-24.04\n"), + "§9.4: the job `{key}` runs on the standard runner" + ); + assert!( + body.contains("\n timeout-minutes: 360\n"), + "§9.4: the job `{key}` has the six-hour limit" + ); + } // The resource profile (§22.11) is chosen by the leg's matrix row - // and by nothing else: each variable is set once, on the gate job, - // from the row. + // and by nothing else: each variable is set once on the gate job, + // from the row. An Atlas job names the examples profile itself, + // once, the same on every shard. + let vv = job("vv"); for (variable, line) in [ ("LEXLEAN_VERIFY_WIDTH", " LEXLEAN_VERIFY_WIDTH: ${{ matrix.width }}\n"), ( @@ -1022,29 +1062,47 @@ pub(crate) fn run(id: &str) { "LEXLEAN_VERIFY_HINTS", " LEXLEAN_VERIFY_HINTS: ${{ matrix.hints && format('{0}/{1}', github.workspace, matrix.hints) || '' }}\n", ), + ( + "LEXLEAN_EXAMPLES_PART", + " LEXLEAN_EXAMPLES_PART: ${{ matrix.examples_part }}\n", + ), ] { - assert_eq!(ci.matches(variable).count(), 1, "§9.4: `{variable}` is set once"); - assert!(ci.contains(line), "§9.4: `{variable}` is read from the matrix row"); + assert_eq!(vv.matches(variable).count(), 1, "§9.4: `{variable}` is set once on the gate job"); + assert!(vv.contains(line), "§9.4: `{variable}` is read from the matrix row"); + } + for (key, body) in &atlas_jobs { + for line in [ + " LEXLEAN_VERIFY_WIDTH: \"2\"\n", + " LEXLEAN_VERIFY_MEMORY_KIB: \"12582912\"\n", + " LEXLEAN_VERIFY_HINTS: ${{ github.workspace }}/.github/verify-hints.json\n", + " LEXLEAN_EXAMPLES_PARTS: ${{ github.workspace }}/ci-parts\n", + " LEXLEAN_CI_TELEMETRY: ${{ github.workspace }}/ci-evidence\n", + ] { + assert_eq!(body.matches(line).count(), 1, "§9.4: `{key}` sets {line:?} once"); + } + assert_eq!( + body.matches("LEXLEAN_EXAMPLES_PART:").count(), + 1, + "§9.4: `{key}` names its part once" + ); } - assert!(ci.contains("timeout-minutes: 360")); // The gate is one matrix job whose legs run the recipes of `vv` // (§9.4): every recipe exactly once, in the order of `vv` within a // leg, each leg through the one gate command. - let vv: Vec = just_recipes(&root_file("Justfile")) + let recipes_of_vv: Vec = just_recipes(&root_file("Justfile")) .get("vv") .expect("§9.2: the Justfile defines vv") .0 .split_whitespace() .map(str::to_owned) .collect(); - let job = &ci[..ci.find("\n host-matrix:").expect("the host matrix")]; - // A matrix row: `- { part: , recipes: "...", width: "...", - // memory_kib: "...", hints: "..." }`. + // A matrix row: `- { part: , recipes: "...", examples_part: + // "...", width: "...", memory_kib: "...", hints: "..." }`. let field = |row: &str, name: &str| -> Option { let start = row.find(&format!(" {name}: \""))? + name.len() + 4; Some(row[start..start + row[start..].find('"')?].to_owned()) }; - let rows: Vec<&str> = job + let rows: Vec<&str> = vv .lines() .filter(|line| line.trim().starts_with("- { part: ")) .collect(); @@ -1062,20 +1120,27 @@ pub(crate) fn run(id: &str) { ); assert!(legs.len() >= 2, "the gate runs in legs: {legs:?}"); // The leg that runs `examples` verifies at width 2 with the - // committed hints and a 12 GiB budget; every other leg names no - // profile, which is the default (§9.4, §22.11). The values are the + // committed hints and a 12 GiB budget, and every example but the + // one the Atlas jobs verify as parts; every other leg names no + // profile and no part (§9.4, §22.11). The values are the // verifier's to accept: a width it refuses, or hints it cannot // read, would fail the gate as `LLV7017` before any stage ran, so // they are parsed here with the verifier's own functions. for (row, leg) in rows.iter().zip(&legs) { - let profile = ["width", "memory_kib", "hints"].map(|name| { + let profile = ["width", "memory_kib", "hints", "examples_part"].map(|name| { field(row, name).unwrap_or_else(|| panic!("§9.4: the row {row} names `{name}`")) }); if leg.iter().any(|recipe| recipe == "examples") { assert_eq!( profile, - ["2", "12582912", ".github/verify-hints.json"].map(str::to_owned), - "§9.4: the examples leg's profile" + [ + "2", + "12582912", + ".github/verify-hints.json", + "without:uor-atlas" + ] + .map(str::to_owned), + "§9.4: the examples leg's profile and part" ); assert_eq!( lexlean::verify::operational::Operational::parse_width(Some(&profile[0])) @@ -1088,13 +1153,13 @@ pub(crate) fn run(id: &str) { .expect("the committed hints are a hints file the verifier reads"); assert!( hints.contains_key("LexLeanExample.CensusCert4"), - "the hints cover the Atlas module that dominates the leg" + "the hints cover the Atlas module that dominates the verification" ); } else { assert_eq!( profile, - ["", "", ""].map(str::to_owned), - "§9.4: a leg that does not run examples names no profile: {row}" + ["", "", "", ""].map(str::to_owned), + "§9.4: a leg that does not run examples names no profile and no part: {row}" ); } } @@ -1103,7 +1168,7 @@ pub(crate) fn run(id: &str) { let positions: Vec = leg .iter() .map(|recipe| { - vv.iter().position(|name| name == recipe).unwrap_or_else(|| { + recipes_of_vv.iter().position(|name| name == recipe).unwrap_or_else(|| { panic!("§9.4: the leg {leg:?} runs `{recipe}`, which is not a recipe of vv") }) }) @@ -1114,7 +1179,7 @@ pub(crate) fn run(id: &str) { ); } ran.sort(); - let mut all: Vec<&String> = vv.iter().collect(); + let mut all: Vec<&String> = recipes_of_vv.iter().collect(); all.sort(); assert_eq!( ran, all, @@ -1135,12 +1200,206 @@ pub(crate) fn run(id: &str) { )), "a leg marks the end of its last recipe as the summary reads it" ); - // The Atlas assertions are chosen by the leg's recipes, never by - // what the log happens to hold. + // The leg's assertion is chosen by its recipes, never by what the + // log happens to hold, and it refuses a leg that verified Atlas, + // which the join verifies. + assert!( + vv.contains("case \" ${{ matrix.recipes }} \" in") + && vv.contains("*\" examples \"*)") + && vv.contains( + "if grep -F \"verify-examples: uor-atlas\" ci-evidence/vv.txt; then" + ), + "the leg that runs examples asserts that it verified the examples and not Atlas" + ); + // The Atlas jobs run every shard of the committed plan exactly + // once, each after the jobs of the shards it needs, and the join + // asserts that Atlas verified (§9.4). The plan itself is checked + // as `cargo xtask ci-shards` checks it. + let plan = crate::shards::Plan::read(support::repo_root().as_std_path()) + .expect("§9.4: the committed plan reads"); + assert_eq!(plan.project, "uor-atlas"); + let graph = crate::shards::import_graph( + support::repo_root() + .join("examples") + .join(&plan.project) + .as_std_path(), + ) + .expect("the Atlas import graph reads from its committed build"); + crate::shards::check(&plan, &graph) + .expect("§9.4: the plan runs every process once in import order"); + // Which job runs which shard: a literal part, or the rows of a + // `matrix: { shard: [...] }` with the part naming `matrix.shard`. + let mut runs: std::collections::BTreeMap = + std::collections::BTreeMap::new(); + let mut needs: std::collections::BTreeMap> = + std::collections::BTreeMap::new(); + for (key, body) in &atlas_jobs { + let listed: Vec = body + .lines() + .find_map(|line| line.trim().strip_prefix("needs: [")) + .map(|rest| { + rest.trim_end_matches(']') + .split(',') + .map(|name| name.trim().to_owned()) + .filter(|name| !name.is_empty()) + .collect() + }) + .unwrap_or_default(); + needs.insert((*key).clone(), listed); + let part = body + .lines() + .find_map(|line| line.trim().strip_prefix("LEXLEAN_EXAMPLES_PART: ")) + .unwrap_or_else(|| panic!("§9.4: `{key}` names its part")); + let shards: Vec = if part == "join:uor-atlas" { + vec![crate::shards::JOIN.to_owned()] + } else if part == "shard:uor-atlas:${{ matrix.shard }}" { + let matrix = body + .lines() + .find_map(|line| { + line.trim() + .strip_prefix("strategy: { fail-fast: false, matrix: { shard: [") + }) + .unwrap_or_else(|| panic!("§9.4: `{key}` runs the shards of its matrix")); + matrix + .split(']') + .next() + .unwrap_or_default() + .split(',') + .map(|name| name.trim().to_owned()) + .collect() + } else { + let name = part.strip_prefix("shard:uor-atlas:").unwrap_or_else(|| { + panic!("§9.4: `{key}` runs a shard of Atlas or the join: {part}") + }); + assert!( + !body.contains("matrix:"), + "§9.4: `{key}` runs one shard and has no matrix" + ); + vec![name.to_owned()] + }; + for shard in shards { + assert!( + plan.shards.contains_key(&shard), + "§9.4: `{key}` runs `{shard}`, which is no shard of the plan" + ); + assert!( + runs.insert(shard.clone(), (*key).clone()).is_none(), + "§9.4: the shard `{shard}` is run by two jobs" + ); + } + assert!( + body.contains( + " if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }}\n" + ), + "§9.4: `{key}` waits only for a pull request to leave draft" + ); + assert!( + body.contains("name: acceptance-gate-evidence-atlas-") + && body.contains("path: ci-evidence\n"), + "§9.4: `{key}` uploads its evidence under a name of its own" + ); + assert!( + body.contains(" ci-summary --evidence ci-evidence\n"), + "§9.4: `{key}` summarizes its run" + ); + } + for shard in plan.shards.keys() { + assert!( + runs.contains_key(shard), + "§9.4: the shard `{shard}` is run by no job" + ); + } + // The job graph orders each shard after the jobs of the shards it + // needs, directly or through another job; a shard never needs one + // of its own job's rows, which run at once. + let after = |job_key: &str| -> std::collections::BTreeSet { + let mut closure = std::collections::BTreeSet::new(); + let mut stack = vec![job_key.to_owned()]; + while let Some(key) = stack.pop() { + for need in needs.get(&key).map(Vec::as_slice).unwrap_or_default() { + if closure.insert(need.clone()) { + stack.push(need.clone()); + } + } + } + closure + }; + for (shard, plan_shard) in &plan.shards { + let job_key = &runs[shard]; + let before = after(job_key); + for need in &plan_shard.needs { + let need_job = &runs[need]; + assert!( + need_job != job_key && before.contains(need_job), + "§9.4: `{shard}` runs in `{job_key}`, which does not wait for `{need_job}`, the job of `{need}` it needs" + ); + } + } + // The one build of the gate's executable is the prefix job's, from + // its clean checkout; every other Atlas job takes it and the + // shards' output from the run, and the shards upload their output + // under their names. Nothing crosses runs: no cache action, no + // artifact of another run. + let prefix_job = &runs["prefix"]; + assert_eq!( + ci.matches("cargo build").count(), + 1, + "ci.yml builds the gate's executable once" + ); + assert!( + job(prefix_job).contains(" run: cargo build --locked --package xtask\n") + && job(prefix_job).contains("name: atlas-xtask\n") + && job(prefix_job).contains("path: target/debug/xtask\n"), + "§9.4: the prefix job builds the executable from its clean checkout and uploads it" + ); + for (key, body) in &atlas_jobs { + if key == prefix_job { + assert!( + !body.contains("download-artifact"), + "the prefix job takes nothing from the run" + ); + continue; + } + assert!( + body.contains(" pattern: atlas-*\n") + && body.contains(" path: ci-parts\n") + && body.contains("chmod +x ci-parts/atlas-xtask/xtask\n") + && body.contains("ci-parts/atlas-xtask/xtask verify-examples 2>&1 | tee ci-evidence/vv.txt\n"), + "§9.4: `{key}` takes the executable and the shards from the run and runs the gate's recipe through it" + ); + assert!( + !body.contains("run-id") && !body.contains("github-token"), + "§9.4: `{key}` reads the artifacts of this run only" + ); + } + for (shard, job_key) in &runs { + if shard == crate::shards::JOIN { + assert!( + !job(job_key).contains("name: atlas-part-"), + "the join uploads no part" + ); + continue; + } + let body = job(job_key); + let uploaded = if body.contains("matrix: { shard: [") { + "name: atlas-part-${{ matrix.shard }}\n".to_owned() + } else { + format!("name: atlas-part-{shard}\n") + }; + assert!( + body.contains(&uploaded), + "§9.4: `{job_key}` uploads the output of `{shard}`" + ); + } + 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"), + "the join asserts that Atlas verified" + ); assert!( - ci.contains("case \" ${{ matrix.recipes }} \" in") - && ci.contains("*\" examples \"*)"), - "the leg that runs examples asserts that Atlas verified" + ci.contains(" pull_request:\n types: [opened, synchronize, reopened, ready_for_review]\n"), + "§9.4: a pull request marked ready runs the jobs that waited for it" ); for forbidden in [ "actions/cache", @@ -1152,25 +1411,37 @@ pub(crate) fn run(id: &str) { ] { assert!(!ci.contains(forbidden), "ci.yml has no `{forbidden}`"); } - // A condition appears only on the two evidence steps, in exactly - // one form, as a step's own key: not on the job (a skipped job is a - // skipped gate), not on the gate step, and never one that is - // narrower than "unless the run was cancelled" (a gate that is - // skipped on pull requests is the weaker PR-only gate). - let mut conditions = 0; + // A condition appears in two forms and nowhere else: a step's + // `if: ${{ !cancelled() }}` on the summary and evidence steps, so + // that a failed run still reports, and a job's draft condition on + // the Atlas jobs. Never on the gate step, and never one narrower + // than those (a gate skipped on pull requests is the weaker + // PR-only gate). + let mut step_conditions = 0; + let mut draft_conditions = 0; for (index, line) in ci.lines().enumerate() { if line.trim_start().starts_with("if:") { - conditions += 1; - assert_eq!( - line, " if: ${{ !cancelled() }}", - "ci.yml:{}: the only condition allowed is a step's `if: ${{{{ !cancelled() }}}}`", - index + 1 - ); + match line { + " if: ${{ !cancelled() }}" => step_conditions += 1, + " if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }}" => { + draft_conditions += 1; + } + other => panic!( + "ci.yml:{}: a condition other than a step's `!cancelled()` or an Atlas job's draft condition: {other}", + index + 1 + ), + } } } assert_eq!( - conditions, 2, - "the summary step and the evidence upload carry it" + step_conditions, + 2 + 2 * atlas_jobs.len(), + "the summary step and the evidence upload of every gate job carry it" + ); + assert_eq!( + draft_conditions, + atlas_jobs.len(), + "every Atlas job and no other waits for a pull request to leave draft" ); let gate_step = &ci[ci .find(" - name: Run the normative acceptance gate") @@ -1201,7 +1472,7 @@ pub(crate) fn run(id: &str) { // profile, locking, and features build the crate's library and // binary, so a separate build step is time spent on nothing the // test does not already require (§8.3). - let matrix = &ci[ci.find("\n host-matrix:").expect("the host matrix")..]; + let matrix = job("host-matrix"); assert_eq!( matrix .matches("cargo test --locked --workspace --all-features --no-fail-fast\n") @@ -1209,19 +1480,6 @@ pub(crate) fn run(id: &str) { 1, "the host matrix runs the workspace's tests once, and reports every failing test of the host, not the first binary's" ); - assert!( - !ci.contains("cargo build"), - "ci.yml has no `cargo build` step: the host matrix's `cargo test` builds the crate" - ); - // The supported-host matrix keeps its four other legs. - for host in [ - "ubuntu-24.04-arm", - "macos-15-intel", - "macos-15", - "windows-2022", - ] { - assert!(ci.contains(host), "the host matrix keeps {host}"); - } // The honesty and reproducibility workflows stay separate. assert!(root_file(".github/workflows/honesty.yml").contains("just model spec-links")); assert!(root_file(".github/workflows/reproducibility.yml").contains("run: just repro")); diff --git a/crates/conformance/src/cases/verification.rs b/crates/conformance/src/cases/verification.rs index 211f52712..da686acc8 100644 --- a/crates/conformance/src/cases/verification.rs +++ b/crates/conformance/src/cases/verification.rs @@ -37,7 +37,7 @@ const LEAN_BACKED: [&str; 14] = [ pub(crate) fn run(id: &str) { // The operational cases (§22.11, §22.12) gate their own Lean-backed halves. - if matches!(id, "VR-20" | "VR-21" | "VR-22") { + if matches!(id, "VR-20" | "VR-21" | "VR-22" | "VR-23") { super::operational::run(id); return; } diff --git a/crates/conformance/src/lib.rs b/crates/conformance/src/lib.rs index 41caf902c..938e547a1 100644 --- a/crates/conformance/src/lib.rs +++ b/crates/conformance/src/lib.rs @@ -36,6 +36,7 @@ pub mod rust_differential; pub mod rust_harness; pub mod rust_packages; pub mod schema; +pub mod shards; pub mod stress; pub mod tl; pub mod tooling; diff --git a/crates/conformance/src/shards.rs b/crates/conformance/src/shards.rs new file mode 100644 index 000000000..e55150ac1 --- /dev/null +++ b/crates/conformance/src/shards.rs @@ -0,0 +1,435 @@ +//! The partition of one example's verification into the parts of one CI run +//! (SPEC.md §9.4): the committed plan, the import graph it is checked +//! against, and the checks. +//! +//! The plan is data, committed as `.github/verify-shards.json` and read by +//! `cargo xtask verify-examples` on each part's job and by `cargo xtask +//! ci-shards`, which checks it. It names one project and its shards: each +//! shard the shards it needs (whose `.olean` files it imports), the modules it +//! elaborates, and the modules it replays and audits. The shard named `join` +//! is the one that publishes; it needs every other shard, directly or through +//! another. The checks are the ones the verifier itself would fail on when a +//! part ran, made before any part runs: every module is elaborated by exactly +//! one shard and replayed by exactly one, every import of a module a shard +//! elaborates is elaborated by that shard or one it needs, a module a shard +//! replays is one whose `.olean` it has, and the needs form no cycle. +//! +//! The import graph is read from the example's committed `expected/build/ +//! modules/`, the generated Lean the `golden` recipe holds equal to the +//! build: a module's `import` and `public import` lines that name another +//! module of the project. + +use std::collections::{BTreeMap, BTreeSet}; +use std::path::Path; + +/// The committed plan, repository-relative. +pub const PLAN_FILE: &str = ".github/verify-shards.json"; + +/// The name of the shard that publishes. +pub const JOIN: &str = "join"; + +/// One shard of the plan. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Shard { + /// The shards whose output this one imports. + pub needs: Vec, + /// The full Lean module names this shard elaborates. + pub elaborate: Vec, + /// The full Lean module names this shard replays and audits. + pub replay: Vec, +} + +/// The plan: one project, its shards by name. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Plan { + /// The example directory name under `examples/`. + pub project: String, + /// The shards, by name. + pub shards: BTreeMap, +} + +impl Plan { + /// Parse the plan file's text. + /// + /// # Errors + /// + /// Text that is not the plan's shape. + pub fn parse(text: &str) -> Result { + let value: serde_json::Value = + serde_json::from_str(text).map_err(|error| format!("{PLAN_FILE}: {error}"))?; + let object = value + .as_object() + .ok_or_else(|| format!("{PLAN_FILE}: an object is required"))?; + let project = object + .get("project") + .and_then(serde_json::Value::as_str) + .ok_or_else(|| format!("{PLAN_FILE}: `project` is a required string"))? + .to_owned(); + let shards_value = object + .get("shards") + .and_then(serde_json::Value::as_object) + .ok_or_else(|| format!("{PLAN_FILE}: `shards` is a required object"))?; + let strings = + |shard: &str, value: &serde_json::Value, field: &str| -> Result, String> { + value + .get(field) + .and_then(serde_json::Value::as_array) + .ok_or_else(|| { + format!("{PLAN_FILE}: shard `{shard}`: `{field}` is a required array") + })? + .iter() + .map(|item| { + item.as_str().map(str::to_owned).ok_or_else(|| { + format!("{PLAN_FILE}: shard `{shard}`: `{field}` holds strings") + }) + }) + .collect() + }; + let mut shards = BTreeMap::new(); + for (name, value) in shards_value { + if let Some(unknown) = value + .as_object() + .map(|fields| { + fields + .keys() + .find(|key| !["needs", "elaborate", "replay"].contains(&key.as_str())) + }) + .unwrap_or(None) + { + return Err(format!( + "{PLAN_FILE}: shard `{name}`: `{unknown}` is not a field of a shard" + )); + } + shards.insert( + name.clone(), + Shard { + needs: strings(name, value, "needs")?, + elaborate: strings(name, value, "elaborate")?, + replay: strings(name, value, "replay")?, + }, + ); + } + if let Some(unknown) = object + .keys() + .find(|key| !["project", "shards"].contains(&key.as_str())) + { + return Err(format!( + "{PLAN_FILE}: `{unknown}` is not a field of the plan" + )); + } + Ok(Self { project, shards }) + } + + /// Read the committed plan of a repository. + /// + /// # Errors + /// + /// A plan file that cannot be read or parsed. + pub fn read(root: &Path) -> Result { + let path = root.join(PLAN_FILE); + let text = std::fs::read_to_string(&path) + .map_err(|error| format!("{}: {error}", path.display()))?; + Self::parse(&text) + } + + /// The shards a shard needs, directly or through another, in sorted + /// order. + /// + /// # Errors + /// + /// A need that names no shard, or a cycle. + pub fn needs_closure(&self, name: &str) -> Result, String> { + let mut closure = BTreeSet::new(); + let mut stack: Vec<(String, Vec)> = vec![(name.to_owned(), vec![name.to_owned()])]; + while let Some((shard, path)) = stack.pop() { + let shard_plan = self.shards.get(&shard).ok_or_else(|| { + format!("shard `{shard}` is needed by `{name}` and is not in the plan") + })?; + for need in &shard_plan.needs { + if path.contains(need) { + return Err(format!( + "the needs of the shards form a cycle through `{need}`: {}", + path.join(" -> ") + )); + } + if closure.insert(need.clone()) { + let mut next = path.clone(); + next.push(need.clone()); + stack.push((need.clone(), next)); + } + } + } + Ok(closure) + } + + /// The modules whose `.olean` a shard has: the ones it elaborates and + /// the ones the shards it needs elaborate. + /// + /// # Errors + /// + /// What [`Self::needs_closure`] reports. + pub fn available(&self, name: &str) -> Result, String> { + let shard = self + .shards + .get(name) + .ok_or_else(|| format!("shard `{name}` is not in the plan"))?; + let mut available: BTreeSet = shard.elaborate.iter().cloned().collect(); + for need in self.needs_closure(name)? { + available.extend(self.shards[&need].elaborate.iter().cloned()); + } + Ok(available) + } +} + +/// The import graph of an example from its committed generated Lean: each +/// module's full Lean name to the modules of the project it imports. +/// +/// # Errors +/// +/// A modules directory that cannot be read. +pub fn import_graph(example_dir: &Path) -> Result>, String> { + let modules_dir = example_dir.join("expected").join("build").join("modules"); + let mut sources: BTreeMap = BTreeMap::new(); + for entry in walkdir::WalkDir::new(&modules_dir).sort_by_file_name() { + let entry = entry.map_err(|error| format!("{}: {error}", modules_dir.display()))?; + if !entry.file_type().is_file() || entry.path().extension().is_none_or(|ext| ext != "lean") + { + continue; + } + let relative = entry + .path() + .strip_prefix(&modules_dir) + .map_err(|error| error.to_string())? + .with_extension(""); + let name = relative + .components() + .map(|component| component.as_os_str().to_string_lossy().into_owned()) + .collect::>() + .join("."); + let text = std::fs::read_to_string(entry.path()) + .map_err(|error| format!("{}: {error}", entry.path().display()))?; + sources.insert(name, text); + } + if sources.is_empty() { + return Err(format!("{}: no generated modules", modules_dir.display())); + } + let mut graph = BTreeMap::new(); + for (name, text) in &sources { + let mut imports = Vec::new(); + for line in text.lines() { + let line = line.trim(); + let imported = line + .strip_prefix("public import ") + .or_else(|| line.strip_prefix("import ")) + .map(str::trim); + if let Some(imported) = imported { + if sources.contains_key(imported) && !imports.contains(&imported.to_owned()) { + imports.push(imported.to_owned()); + } + } + } + graph.insert(name.clone(), imports); + } + Ok(graph) +} + +/// Check a plan against an import graph. The lines returned describe each +/// shard: what it needs, how many modules it elaborates and replays. +/// +/// # Errors +/// +/// The first check that fails, named. +pub fn check(plan: &Plan, graph: &BTreeMap>) -> Result, String> { + let modules: BTreeSet<&String> = graph.keys().collect(); + let join = plan + .shards + .get(JOIN) + .ok_or_else(|| format!("the plan has no shard named `{JOIN}`, the one that publishes"))?; + let _ = join; + let mut elaborated: BTreeMap<&String, &String> = BTreeMap::new(); + let mut replayed: BTreeMap<&String, &String> = BTreeMap::new(); + for (name, shard) in &plan.shards { + for module in &shard.elaborate { + if !modules.contains(module) { + return Err(format!( + "shard `{name}` elaborates `{module}`, which is no module of the project" + )); + } + if let Some(other) = elaborated.insert(module, name) { + return Err(format!( + "`{module}` is elaborated by `{other}` and by `{name}`" + )); + } + } + for module in &shard.replay { + if !modules.contains(module) { + return Err(format!( + "shard `{name}` replays `{module}`, which is no module of the project" + )); + } + if let Some(other) = replayed.insert(module, name) { + return Err(format!( + "`{module}` is replayed by `{other}` and by `{name}`" + )); + } + } + } + for module in &modules { + if !elaborated.contains_key(module) { + return Err(format!("`{module}` is elaborated by no shard")); + } + if !replayed.contains_key(module) { + return Err(format!("`{module}` is replayed by no shard")); + } + } + let mut lines = Vec::new(); + for (name, shard) in &plan.shards { + let available = plan.available(name)?; + for module in &shard.elaborate { + for import in &graph[module] { + if !available.contains(import) { + return Err(format!( + "shard `{name}` elaborates `{module}`, whose import `{import}` is elaborated by no shard it needs" + )); + } + } + } + for module in &shard.replay { + if !available.contains(module) { + return Err(format!( + "shard `{name}` replays `{module}`, whose olean comes from no shard it needs" + )); + } + for import in &graph[module] { + if !available.contains(import) { + return Err(format!( + "shard `{name}` replays `{module}`, whose import `{import}` is elaborated by no shard it needs" + )); + } + } + } + lines.push(format!( + "{name}: needs {}; elaborates {}; replays {}", + if shard.needs.is_empty() { + "nothing".to_owned() + } else { + shard.needs.join(", ") + }, + shard.elaborate.len(), + shard.replay.len() + )); + } + let others: BTreeSet = plan + .shards + .keys() + .filter(|name| *name != JOIN) + .cloned() + .collect(); + if plan.needs_closure(JOIN)? != others { + return Err(format!( + "`{JOIN}` must need every other shard, directly or through another" + )); + } + Ok(lines) +} + +#[cfg(test)] +mod tests { + use super::*; + + fn plan(text: &str) -> Plan { + Plan::parse(text).expect("parses") + } + + fn graph() -> BTreeMap> { + [("P.A", vec![]), ("P.B", vec!["P.A"]), ("P.C", vec!["P.B"])] + .into_iter() + .map(|(name, imports)| { + ( + name.to_owned(), + imports.into_iter().map(str::to_owned).collect(), + ) + }) + .collect() + } + + const GOOD: &str = r#"{"project":"p","shards":{ + "one":{"needs":[],"elaborate":["P.A"],"replay":[]}, + "two":{"needs":["one"],"elaborate":["P.B"],"replay":["P.A","P.B"]}, + "join":{"needs":["two"],"elaborate":["P.C"],"replay":["P.C"]}}}"#; + + #[test] + fn a_plan_that_runs_every_process_once_in_order_passes() { + let lines = check(&plan(GOOD), &graph()).expect("checks"); + assert_eq!(lines.len(), 3); + assert_eq!( + plan(GOOD).needs_closure("join").expect("closure"), + ["one", "two"].into_iter().map(str::to_owned).collect() + ); + } + + #[test] + fn every_defect_of_a_plan_is_named() { + let cases: [(&str, &str); 7] = [ + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.A","P.B"],"replay":["P.A","P.B"]},"join":{"needs":["one"],"elaborate":["P.C"],"replay":["P.C","P.A"]}}}"#, + "replayed by `join` and by `one`", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.A"],"replay":["P.A"]},"join":{"needs":["one"],"elaborate":["P.C"],"replay":["P.B","P.C"]}}}"#, + "`P.B` is elaborated by no shard", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.B"],"replay":["P.B"]},"join":{"needs":["one"],"elaborate":["P.A","P.C"],"replay":["P.A","P.C"]}}}"#, + "whose import `P.A` is elaborated by no shard it needs", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.A"],"replay":["P.B"]},"join":{"needs":["one"],"elaborate":["P.B","P.C"],"replay":["P.A","P.C"]}}}"#, + "whose olean comes from no shard it needs", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":["two"],"elaborate":["P.A"],"replay":["P.A"]},"two":{"needs":["one"],"elaborate":["P.B"],"replay":["P.B"]},"join":{"needs":["two"],"elaborate":["P.C"],"replay":["P.C"]}}}"#, + "form a cycle", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.A","P.B"],"replay":["P.A","P.B"]},"two":{"needs":[],"elaborate":[],"replay":[]},"join":{"needs":["one"],"elaborate":["P.C"],"replay":["P.C"]}}}"#, + "must need every other shard", + ), + ( + r#"{"project":"p","shards":{"one":{"needs":[],"elaborate":["P.A","P.B","P.C"],"replay":["P.A","P.B","P.C"]}}}"#, + "no shard named `join`", + ), + ]; + for (text, expected) in cases { + let error = check(&plan(text), &graph()).expect_err(expected); + assert!(error.contains(expected), "{expected}: {error}"); + } + assert!(Plan::parse( + r#"{"project":"p","shards":{"a":{"needs":[],"elaborate":[],"replay":[],"width":2}}}"# + ) + .is_err()); + assert!(Plan::parse(r#"{"project":"p","shards":{},"extra":1}"#).is_err()); + } + + #[test] + fn the_import_graph_reads_both_import_forms_of_the_generated_lean() { + let dir = tempfile::tempdir().expect("tempdir"); + let modules = dir.path().join("expected/build/modules/P"); + std::fs::create_dir_all(&modules).expect("mkdir"); + std::fs::write( + modules.join("A.lean"), + "module\npublic import Init\nimport Lean\n", + ) + .expect("write"); + std::fs::write( + modules.join("B.lean"), + "module\npublic import Init\npublic import P.A\nimport Lean\n", + ) + .expect("write"); + std::fs::write(modules.join("C.lean"), "import P.B\nimport P.A\n").expect("write"); + let graph = import_graph(dir.path()).expect("graph"); + assert_eq!(graph["P.A"], Vec::::new()); + assert_eq!(graph["P.B"], vec!["P.A".to_owned()]); + assert_eq!(graph["P.C"], vec!["P.B".to_owned(), "P.A".to_owned()]); + } +} diff --git a/crates/conformance/tests/conformance.rs b/crates/conformance/tests/conformance.rs index 49ba14129..83e2edd6d 100644 --- a/crates/conformance/tests/conformance.rs +++ b/crates/conformance/tests/conformance.rs @@ -1045,6 +1045,11 @@ fn conformance_vr_22() { repo_conformance::cases::run("VR-22"); } +#[test] +fn conformance_vr_23() { + repo_conformance::cases::run("VR-23"); +} + #[test] fn conformance_cl_01() { repo_conformance::cases::run("CL-01"); diff --git a/crates/lexlean/src/api.rs b/crates/lexlean/src/api.rs index 46a353511..133093e4e 100644 --- a/crates/lexlean/src/api.rs +++ b/crates/lexlean/src/api.rs @@ -47,6 +47,54 @@ pub struct VerifyRequest { pub selection: Selection, } +/// Which modules one part of a verification runs (SPEC.md §9.4): full Lean +/// module names, as the verifier labels its processes (§22.11). +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct VerifyPlan { + /// The modules the part elaborates. + pub elaborate: Vec, + /// The modules the part replays and audits. + pub replay: Vec, +} + +/// One part of a verification run as several parts on several hosts of one +/// run (SPEC.md §9.4). Every process of the verification runs exactly once +/// across the parts; the join publishes what a whole verification publishes. +pub enum VerifyPart { + /// A shard: the plan's processes, written to `output`; nothing published. + Shard { + /// The processes of this shard. + plan: VerifyPlan, + /// The output directories of the parts whose `.olean` files this + /// shard's elaborations import. + imports: Vec, + /// Where the shard writes its `.olean` files and process records; it + /// must not exist or must be empty. + output: Utf8PathBuf, + }, + /// The join: the plan's processes, every other part's records, then the + /// attestation and publication. + Join { + /// The processes of the join itself. + plan: VerifyPlan, + /// The output directories of every other part. + parts: Vec, + }, +} + +/// What a part of a verification produced. +pub enum VerifyPartOutcome { + /// A shard's output directory, and the number of processes it ran. + Shard { + /// The output directory. + output: Utf8PathBuf, + /// The elaborations, replays, and audit members it ran. + processes: usize, + }, + /// The join's published verification. + Verified(VerifiedProject), +} + /// A format request. pub struct FormatRequest { /// The selection. @@ -933,6 +981,66 @@ impl Engine { } fn verify_inner(&self, request: &VerifyRequest) -> Result { + match self.verify_part_inner(request, &crate::verify::Part::Whole)? { + VerifyPartOutcome::Verified(verified) => Ok(verified), + VerifyPartOutcome::Shard { .. } => Err(host_failure( + "the whole verification published no verified directory".to_owned(), + )), + } + } + + /// Verify a selection as one part of a verification run as several + /// parts (SPEC.md §9.4): a shard runs the processes its plan names and + /// writes them to its output directory; the join runs its own, reads + /// every other part's, and publishes through the same pipeline as + /// [`Self::verify`]. A part is defined for a project without production + /// roots and without PDF rendering. + pub fn verify_part( + &self, + request: VerifyRequest, + part: VerifyPart, + ) -> Result { + let plan_of = |plan: &VerifyPlan| crate::verify::Plan { + elaborate: plan.elaborate.iter().cloned().collect(), + replay: plan.replay.iter().cloned().collect(), + }; + match &part { + VerifyPart::Shard { + plan, + imports, + output, + } => { + let plan = plan_of(plan); + self.bound( + "verify", + self.verify_part_inner( + &request, + &crate::verify::Part::Shard { + plan: &plan, + imports, + output, + }, + ), + ) + } + VerifyPart::Join { plan, parts } => { + let plan = plan_of(plan); + self.bound( + "verify", + self.verify_part_inner( + &request, + &crate::verify::Part::Join { plan: &plan, parts }, + ), + ) + } + } + } + + fn verify_part_inner( + &self, + request: &VerifyRequest, + part: &crate::verify::Part<'_>, + ) -> Result { // The operational settings (§22.11, §22.12) are resolved before any // work, so that a malformed width is refused without a build having // been published, and they are handed to the verifier whole: nothing @@ -962,10 +1070,22 @@ impl Engine { // stage, and the verified-set publication (§21.8). let guard = acquire_lock(&self.project)?; publish_build_locked(&self.project, &rendered, &guard)?; - let outcome = - crate::verify::run(&self.project, &lock, &checked, &mut rendered, &operational)?; + let outcome = crate::verify::run_part( + &self.project, + &lock, + &checked, + &mut rendered, + &operational, + part, + )?; drop(guard); - Ok(VerifiedProject { + let outcome = match outcome { + crate::verify::PartOutcome::Shard { output, processes } => { + return Ok(VerifyPartOutcome::Shard { output, processes }); + } + crate::verify::PartOutcome::Verified(outcome) => outcome, + }; + Ok(VerifyPartOutcome::Verified(VerifiedProject { source_id: checked.source_id, semantic_id: checked.semantic_id, build_id: rendered.build_id, @@ -984,7 +1104,7 @@ impl Engine { ) }) .collect(), - }) + })) } /// Format a selection canonically, or exact-byte compare (§23.5). The diff --git a/crates/lexlean/src/lib.rs b/crates/lexlean/src/lib.rs index 640d1e15e..6cfa379ae 100644 --- a/crates/lexlean/src/lib.rs +++ b/crates/lexlean/src/lib.rs @@ -64,7 +64,7 @@ pub mod verify; pub use api::{ BuildRequest, BuiltUnit, CheckRequest, CheckedUnit, CheckedUnitSummary, Engine, FormatRequest, FormatResultSet, LockRequest, LockResult, ModuleArtifacts, ProjectResultSet, Selection, - VerifiedProject, VerifiedUnit, VerifyRequest, + VerifiedProject, VerifiedUnit, VerifyPart, VerifyPartOutcome, VerifyPlan, VerifyRequest, }; pub use artifact::content_id::Sha256Digest; pub use artifact::snapshot::{ diff --git a/crates/lexlean/src/verify/child.rs b/crates/lexlean/src/verify/child.rs index 26708a7c7..4126db206 100644 --- a/crates/lexlean/src/verify/child.rs +++ b/crates/lexlean/src/verify/child.rs @@ -3,6 +3,7 @@ //! deterministic allow-list environment, checked limits, and the exact //! path-replacement normalization. +use std::collections::BTreeSet; use std::io::Read; use std::process::{Command, Stdio}; use std::time::{Duration, Instant}; @@ -223,6 +224,79 @@ impl ChildRecord { } Json::object(fields) } + + /// A record read back from the JSON [`Self::to_json`] wrote, as a later + /// part of a verification reads an earlier part's (§9.4). The stream + /// digests are checked against the streams: a record whose text and + /// digest disagree was not written by the verifier. + /// + /// # Errors + /// + /// A value that is not a process record. + pub fn from_json(json: &Json) -> Result { + let Json::Obj(fields) = json else { + return Err("a process record is an object".to_owned()); + }; + let text = |name: &str| -> Result { + match fields.get(name) { + Some(Json::Str(text)) => Ok(text.clone()), + _ => Err(format!("`{name}` is a required string")), + } + }; + let argv = match fields.get("argv") { + Some(Json::Arr(items)) => items + .iter() + .map(|item| match item { + Json::Str(text) => Ok(text.clone()), + _ => Err("`argv` holds strings".to_owned()), + }) + .collect::, String>>()?, + _ => return Err("`argv` is a required array".to_owned()), + }; + let exit_code = match fields.get("exit_code") { + Some(Json::Int(code)) => { + i32::try_from(*code).map_err(|_| "`exit_code` is an i32".to_owned())? + } + _ => return Err("`exit_code` is a required integer".to_owned()), + }; + let stdout = text("stdout")?; + let stderr = text("stderr")?; + for (name, stream) in [("stdout_sha256", &stdout), ("stderr_sha256", &stderr)] { + if text(name)? != Sha256Digest::of(stream.as_bytes()).to_hex() { + return Err(format!("`{name}` is not the digest of the stream")); + } + } + let module = match fields.get("module") { + None => None, + Some(Json::Str(module)) => Some(module.clone()), + Some(_) => return Err("`module` is a string".to_owned()), + }; + let known: BTreeSet<&str> = [ + "tool", + "argv", + "exit_code", + "executable_sha256", + "stdout", + "stderr", + "stdout_sha256", + "stderr_sha256", + "module", + ] + .into_iter() + .collect(); + if let Some(unknown) = fields.keys().find(|key| !known.contains(key.as_str())) { + return Err(format!("`{unknown}` is not a field of a process record")); + } + Ok(Self { + tool: text("tool")?, + module, + argv, + exit_code, + stdout, + stderr, + executable_sha256: Sha256Digest::from_hex(&text("executable_sha256")?)?, + }) + } } /// The home a child sees (§25.4). diff --git a/crates/lexlean/src/verify/mod.rs b/crates/lexlean/src/verify/mod.rs index 66a9fd332..ec6401cea 100644 --- a/crates/lexlean/src/verify/mod.rs +++ b/crates/lexlean/src/verify/mod.rs @@ -25,6 +25,7 @@ pub mod child; pub mod leanchecker; pub mod lifeline; pub mod operational; +pub mod partition; pub mod pool; pub mod source_audit; pub mod telemetry; @@ -55,6 +56,7 @@ use crate::project::Project; use crate::source::coverage::Origin; use crate::verify::child::{run as run_child, ChildHome, ChildRecord, ChildSpec, Normalizer}; use crate::verify::operational::Operational; +pub use crate::verify::partition::{Part, Plan}; use crate::verify::toolchain::Toolchain; /// The outcome of a successful verification. @@ -65,6 +67,19 @@ pub struct VerifyOutcome { pub root: Utf8PathBuf, } +/// What one part of a verification produced (§9.4). +pub enum PartOutcome { + /// A published verified directory: the whole verification, or the join. + Verified(VerifyOutcome), + /// A shard's output directory, and the number of processes it ran. + Shard { + /// Where the shard wrote its `.olean` files and process records. + output: Utf8PathBuf, + /// The elaborations, replays, and audit members it ran. + processes: usize, + }, +} + fn fail(diagnostic: Diagnostic) -> LexLeanError { LexLeanError::from_diagnostic(diagnostic) } @@ -758,6 +773,62 @@ pub fn run( build: &mut RenderedBuild, operational: &Operational, ) -> Result { + match run_part(project, lock, checked, build, operational, &Part::Whole)? { + PartOutcome::Verified(outcome) => Ok(outcome), + PartOutcome::Shard { .. } => Err(fail(internal( + "the whole verification published no verified directory", + ))), + } +} + +/// [`run`], as the whole verification or as one part of it (§9.4): a shard +/// runs the processes its plan names and writes them to its output +/// directory; the join runs its own, reads every other part's, and +/// publishes. A part is defined for a project without production roots and +/// without PDF rendering, whose verification is the probe, the elaborations, +/// the replays, and the audit members and nothing else. +/// +/// # Errors +/// +/// What [`run`] reports, a plan that names a module the project has not, a +/// part whose imports leave a module of its plan without the `.olean` it +/// imports, and a join for which some process has no record from any part. +#[allow(clippy::too_many_lines)] +pub fn run_part( + project: &Project, + lock: &Lock, + checked: &CheckedProject, + build: &mut RenderedBuild, + operational: &Operational, + part: &Part<'_>, +) -> Result { + if let Some(plan) = part.plan() { + let has_roots = checked + .modules + .values() + .filter_map(|module| module.production.as_ref()) + .any(|report| !report.roots.is_empty()); + if has_roots || project.config.pdf.is_some() { + return Err(fail(internal( + "a part of a verification is defined for a project without production roots and without PDF rendering", + ))); + } + let names: BTreeSet<&str> = build + .modules + .iter() + .map(|module| module.lean_module.as_str()) + .collect(); + if let Some(unknown) = plan + .elaborate + .iter() + .chain(&plan.replay) + .find(|name| !names.contains(name.as_str())) + { + return Err(fail(internal(format!( + "the plan of a verification part names `{unknown}`, which is no module of the project" + )))); + } + } let limits = project.config.limits; let width = operational.width(); let hints = operational.hints(); @@ -1134,7 +1205,19 @@ pub fn run( } release_non_diagnostic_buffers(build); let lean_path_env = format!("{olean_root}"); - let mut process_records: Vec = Vec::new(); + // The records of this run's processes, by what they are and the module + // or audit member they are of, and the records of the remaining stages + // in the order they ran. The attestation lists them in the canonical + // order of §22.11 whichever part of the run produced them. + let mut lean_records: BTreeMap = BTreeMap::new(); + let mut replay_records: BTreeMap = BTreeMap::new(); + let mut audit_records: BTreeMap = BTreeMap::new(); + let mut tail_records: Vec = Vec::new(); + // What the parts before this one wrote (§9.4): their `.olean` files into + // the staged tree, and, for the part that publishes, their records. + stages.enter("part-import"); + let mut imported = + partition::import(part.inputs(), &olean_root, part.publishes()).map_err(fail)?; // The leanchecker identity (module documentation), before any replay: // the preflight's toolchain-relative path and digest line, then the @@ -1212,15 +1295,25 @@ pub fn run( "probe/process.json", &probe_record.to_json().to_file_bytes(), )?; - process_records.push(probe_record); stages.enter("elaboration"); // Stage 7: module elaboration in topological import order (§22.3). // A topological frontier contains no dependency edges, so its members // may run concurrently without making an imported olean observable - // before the process that owns it has completed successfully. + // before the process that owns it has completed successfully. A part + // elaborates the modules its plan names; a module it does not elaborate + // is placed when its `.olean` arrived from an earlier part of the run + // (§9.4), and a module of the plan whose import is neither stops the + // order from converging, with the import named. let mut placed: BTreeSet = BTreeSet::new(); - let mut remaining: Vec = (0..build.modules.len()).collect(); + let mut remaining: Vec = Vec::new(); + for (index, module) in build.modules.iter().enumerate() { + if part.elaborates(&module.lean_module) { + remaining.push(index); + } else if imported.oleans.contains(&module.lean_module) { + placed.insert(module.module.clone()); + } + } // The names are copied out so that the workers of a frontier hold no // borrow of `build`, which the consumer of their results releases // buffers of while later members are still running. @@ -1243,7 +1336,35 @@ pub fn run( }) .collect(); if ready.is_empty() { - return Err(fail(internal("module order did not converge"))); + let waiting: Vec = remaining + .iter() + .map(|index| { + let module = &build.modules[*index]; + let document = &checked.modules[&module.module].document; + // The imports by their Lean module names, the labels of + // the verifier's processes and of a plan. + let missing: Vec = document + .imports + .iter() + .filter(|import| !placed.contains(*import)) + .map(|import| { + build + .modules + .iter() + .find(|other| other.module == *import) + .map_or_else( + || import.to_string(), + |other| other.lean_module.clone(), + ) + }) + .collect(); + format!("`{}` imports {}", module.lean_module, missing.join(", ")) + }) + .collect(); + return Err(fail(internal(format!( + "module order did not converge: {}", + waiting.join("; ") + )))); } let frontier_started = std::time::Instant::now(); for &module_index in &ready { @@ -1344,7 +1465,7 @@ pub fn run( &format!("process/lean/{module_name}.json"), &record.to_json().to_file_bytes(), )?; - process_records.push(record); + lean_records.insert(module_name, record); release_module_diagnostic_buffers(&mut build.modules[module_index]); Ok(()) }, @@ -1365,7 +1486,9 @@ pub fn run( stages.enter("replay"); // Stage 8: separate-process leanchecker replay per module, sorted // (§22.4). - let mut sorted_modules: Vec = (0..build.modules.len()).collect(); + let mut sorted_modules: Vec = (0..build.modules.len()) + .filter(|index| part.replays(&build.modules[*index].lean_module)) + .collect(); sorted_modules.sort_by(|a, b| { build.modules[*a] .lean_module @@ -1406,7 +1529,7 @@ pub fn run( &format!("process/leanchecker/{module_name}.json"), &record.to_json().to_file_bytes(), )?; - process_records.push(record); + replay_records.insert(module_name.clone(), record); Ok(()) }, )?; @@ -1425,7 +1548,9 @@ pub fn run( .iter() .map(|audit| audit.name.clone()) .collect(); - let audit_indices: Vec = (0..audit_modules.len()).collect(); + let audit_indices: Vec = (0..audit_modules.len()) + .filter(|index| part.replays(&audit_modules[*index].generated_module)) + .collect(); pool::run_ordered_with( width, &audit_indices, @@ -1488,16 +1613,74 @@ pub fn run( )))); } } - audit_output.push_str(&audit_record.stdout); write_staged( staging.path(), &format!("audit/{}.process.json", audit.name), &audit_record.to_json().to_file_bytes(), )?; - process_records.push(audit_record); + audit_records.insert(audit.name.clone(), audit_record); Ok(()) }, )?; + // A shard has run what its plan names: what it ran leaves with it, and + // nothing is published (§9.4). + if let Part::Shard { output, .. } = part { + stages.enter("part-output"); + let own: BTreeSet = part + .plan() + .map(|plan| plan.elaborate.clone()) + .unwrap_or_default(); + partition::export(staging.path(), output, &own).map_err(fail)?; + telemetry_run.succeeded(); + return Ok(PartOutcome::Shard { + output: (*output).to_owned(), + processes: lean_records.len() + replay_records.len() + audit_records.len(), + }); + } + // The members other parts of the run audited, judged as the stage above + // judges its own: a member that failed, spoke, or printed a set the + // parser refuses is refused here with the same diagnostic, whichever + // part ran it (§9.4). + for audit in &audit_modules { + if part.replays(&audit.generated_module) { + continue; + } + let audit_record = imported.audit.get(&audit.name).ok_or_else(|| { + fail(internal(format!( + "no audit record of `{}` from any part of the run", + audit.name + ))) + })?; + if audit_record.exit_code != 0 { + return Err(fail(Diagnostic::new( + code!("LLV7004"), + format!( + "axiom audit member `{}` for `{}` failed: {}{}", + audit.name, + audit.generated_module, + audit_record.stdout.trim_end(), + audit_record.stderr.trim_end() + ), + ))); + } + let stage = format!("axiom audit member `{}`", audit.name); + require_silent(audit_record, &stage, true).map_err(fail)?; + let member_observed = axiom::parse_audit_output(&audit_record.stdout, &audit.declarations) + .map_err(|failure| fail(audit_diagnostic(&declaration_spans, failure)))?; + for (name, axioms) in member_observed { + if observed.insert(name.clone(), axioms).is_some() { + return Err(fail(internal(format!( + "axiom audit member `{}` repeated declaration `{name}`", + audit.name + )))); + } + } + write_staged( + staging.path(), + &format!("audit/{}.process.json", audit.name), + &audit_record.to_json().to_file_bytes(), + )?; + } if observed.len() != declaration_names.len() { return Err(fail(internal(format!( "axiom audit family observed {} of {} declarations", @@ -1505,6 +1688,20 @@ pub fn run( declaration_names.len() )))); } + // The audit output in the order of the family, as one process would + // have printed it member after member. + for audit in &audit_modules { + let record = audit_records + .get(&audit.name) + .or_else(|| imported.audit.get(&audit.name)) + .ok_or_else(|| { + fail(internal(format!( + "no audit record of `{}` from any part of the run", + audit.name + ))) + })?; + audit_output.push_str(&record.stdout); + } write_staged(staging.path(), "audit/output.txt", audit_output.as_bytes())?; stages.enter("policy"); @@ -1818,7 +2015,7 @@ pub fn run( ("byte_length", Json::from_usize(bytes.len())), ("sha256", Json::Str(Sha256Digest::of(&bytes).to_hex())), ])); - process_records.push(record); + tail_records.push(record); } stages.enter("certificates"); @@ -2006,7 +2203,7 @@ pub fn run( &format!("process/preserve/{}.json", file.module), &record.to_json().to_file_bytes(), )?; - process_records.push(record); + tail_records.push(record); } for file in &stage.certificates { let record = compile(file, true).map_err(fail)?; @@ -2027,7 +2224,7 @@ pub fn run( &format!("process/preserve/{}.json", file.module), &record.to_json().to_file_bytes(), )?; - process_records.push(record); + tail_records.push(record); let replay = leanchecker::run_leanchecker( &toolchain, &file.module, @@ -2051,7 +2248,7 @@ pub fn run( &format!("process/leanchecker/{}.json", file.module), &replay.to_json().to_file_bytes(), )?; - process_records.push(replay); + tail_records.push(replay); } let audit_record = compile(&stage.audit, false).map_err(fail)?; let audit_output = format!("{}{}", audit_record.stdout, audit_record.stderr); @@ -2079,7 +2276,7 @@ pub fn run( &format!("process/preserve/{}.json", stage.audit.module), &audit_record.to_json().to_file_bytes(), )?; - process_records.push(audit_record); + tail_records.push(audit_record); for file in &stage.certificates { write_staged( staging.path(), @@ -2168,12 +2365,119 @@ pub fn run( ("version", version_record.to_json()), ("compile", compile_record.to_json()), ])); - process_records.push(version_record); - process_records.push(compile_record); + tail_records.push(version_record); + tail_records.push(compile_record); } } stages.enter("attestation"); + // The records of the whole verification in its canonical order (§22.11): + // the probe, the elaborations frontier by frontier in module order, the + // replays in sorted module name, the audit members in the order of the + // family, then the remaining stages in the order they ran. A part that + // publishes ran some of them and read the rest from the parts of its + // run (§9.4); a record read is judged as the stage that produced it + // judges its own, and a process without a record from any part, or a + // record of a process no module owns, is a verification with a hole. + let frontiers = partition::elaboration_order( + build.modules.len(), + &|index| build.modules[index].module.clone(), + &|index| { + checked.modules[&build.modules[index].module] + .document + .imports + .to_vec() + }, + ) + .map_err(fail)?; + let mut process_records: Vec = vec![probe_record]; + let missing = |what: &str, key: &str| { + fail(internal(format!( + "no {what} record of `{key}` from any part of the run" + ))) + }; + for index in frontiers.into_iter().flatten() { + let name = &build.modules[index].lean_module; + let record = match lean_records.remove(name) { + Some(record) => record, + None => { + let record = imported + .lean + .remove(name) + .ok_or_else(|| missing("elaboration", name))?; + if record.exit_code != 0 + || !record.stdout.trim().is_empty() + || !record.stderr.trim().is_empty() + { + return Err(fail(internal(format!( + "a part of the run recorded an elaboration of `{name}` that was not silent and successful" + )))); + } + // An imported record is published with the join's own. + write_staged( + staging.path(), + &format!("process/lean/{name}.json"), + &record.to_json().to_file_bytes(), + )?; + record + } + }; + process_records.push(record); + } + let mut sorted_names: Vec<&String> = build + .modules + .iter() + .map(|module| &module.lean_module) + .collect(); + sorted_names.sort(); + for name in sorted_names { + let record = match replay_records.remove(name) { + Some(record) => record, + None => { + let record = imported + .leanchecker + .remove(name) + .ok_or_else(|| missing("replay", name))?; + if record.exit_code != 0 { + return Err(fail(Diagnostic::new( + code!("LLV7003"), + format!( + "leanchecker replay of `{name}` exited {}: {}{}", + record.exit_code, + record.stdout.trim_end(), + record.stderr.trim_end() + ), + ))); + } + write_staged( + staging.path(), + &format!("process/leanchecker/{name}.json"), + &record.to_json().to_file_bytes(), + )?; + record + } + }; + process_records.push(record); + } + for audit in &audit_modules { + let record = audit_records + .remove(&audit.name) + .or_else(|| imported.audit.remove(&audit.name)) + .ok_or_else(|| missing("audit", &audit.name))?; + process_records.push(record); + } + process_records.extend(tail_records); + if let Some(stray) = imported + .lean + .keys() + .chain(imported.leanchecker.keys()) + .chain(imported.audit.keys()) + .next() + { + return Err(fail(internal(format!( + "a part of the run recorded `{stray}`, which no module of the project owns" + )))); + } // Stage 14: no unexpected absolute paths in successful output (§22.7), // over every process record. for record in &process_records { @@ -2366,10 +2670,10 @@ pub fn run( return match validate_existing(staging.path(), &target) { Ok(()) => { telemetry_run.succeeded(); - Ok(VerifyOutcome { + Ok(PartOutcome::Verified(VerifyOutcome { attestation_id: this_attestation_id, root: target, - }) + })) } Err(reason) => Err(fail(Diagnostic::new( code!("LLB6003"), @@ -2389,10 +2693,10 @@ pub fn run( })?; crate::artifact::fsync_dir(verified_root.as_std_path()); telemetry_run.succeeded(); - Ok(VerifyOutcome { + Ok(PartOutcome::Verified(VerifyOutcome { attestation_id: this_attestation_id, root: target, - }) + })) } /// The SHA-256 of the running executable, read once per process that succeeds diff --git a/crates/lexlean/src/verify/partition.rs b/crates/lexlean/src/verify/partition.rs new file mode 100644 index 000000000..cc55d8402 --- /dev/null +++ b/crates/lexlean/src/verify/partition.rs @@ -0,0 +1,536 @@ +//! The parts of one verification (SPEC.md §9.4, §22.11). +//! +//! A verification is one sequence of processes: the probe, the elaboration of +//! every module in topological frontiers, the replay of every module, and the +//! audit member of every module. The normative CI gate may run that sequence +//! as several parts on several hosts of one run: a *shard* elaborates, +//! replays, and audits the modules its plan names, reading the `.olean` +//! files of the modules it imports from the parts before it, and writes what +//! it ran to an output directory; the *join* runs its own plan, takes the +//! `.olean` files and the process records of every part, re-judges each +//! record as the stage that produced it did, and then continues through +//! policy, the attestation, and publication exactly as the whole +//! verification does. Every process of the verification runs exactly once +//! across the parts, and the attestation the join publishes is a function of +//! the same records in the same canonical order as a whole verification's. +//! +//! Nothing here is a cache: a part reads only what the parts of the same run +//! wrote, and a module without a record from any part fails the join. + +use std::collections::{BTreeMap, BTreeSet}; + +use camino::{Utf8Path, Utf8PathBuf}; + +use crate::artifact::canonical_json::Json; +use crate::diagnostic::Diagnostic; +use crate::verify::child::ChildRecord; + +/// Which modules one part elaborates, and which it replays and audits. +/// +/// Both sets hold full Lean module names (the labels of the verifier's +/// processes, §22.11). A module replayed by a part must have been elaborated +/// by that part or by a part whose output it imports. +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct Plan { + /// The modules this part elaborates (§22.3). + pub elaborate: BTreeSet, + /// The modules this part replays (§22.4) and audits (§22.5). + pub replay: BTreeSet, +} + +/// What one run of the verifier is. +pub enum Part<'a> { + /// The whole verification: every process, then the attestation. + Whole, + /// One shard: the plan's processes, written to `output`, nothing + /// published. + Shard { + /// The processes of this shard. + plan: &'a Plan, + /// The output directories of the parts whose `.olean` files this + /// shard imports. + imports: &'a [Utf8PathBuf], + /// Where this shard writes its `.olean` files and process records. + output: &'a Utf8Path, + }, + /// The join: the plan's processes, every other part's records, then the + /// attestation and publication. + Join { + /// The processes of the join itself. + plan: &'a Plan, + /// The output directories of every other part. + parts: &'a [Utf8PathBuf], + }, +} + +impl Part<'_> { + /// The plan, when this is a part and not the whole. + #[must_use] + pub fn plan(&self) -> Option<&Plan> { + match self { + Self::Whole => None, + Self::Shard { plan, .. } | Self::Join { plan, .. } => Some(plan), + } + } + + /// The output directories this part reads. + #[must_use] + pub fn inputs(&self) -> &[Utf8PathBuf] { + match self { + Self::Whole => &[], + Self::Shard { imports, .. } => imports, + Self::Join { parts, .. } => parts, + } + } + + /// Does this part publish a verified directory? + #[must_use] + pub fn publishes(&self) -> bool { + matches!(self, Self::Whole | Self::Join { .. }) + } + + /// Is a module one this part elaborates? + #[must_use] + pub fn elaborates(&self, lean_module: &str) -> bool { + self.plan() + .is_none_or(|plan| plan.elaborate.contains(lean_module)) + } + + /// Is a module one this part replays and audits? + #[must_use] + pub fn replays(&self, lean_module: &str) -> bool { + self.plan() + .is_none_or(|plan| plan.replay.contains(lean_module)) + } +} + +/// What earlier parts of the run wrote, read back. +#[derive(Debug, Default)] +pub struct Imported { + /// The modules whose `.olean` arrived, by full Lean module name. + pub oleans: BTreeSet, + /// Elaboration records by module. + pub lean: BTreeMap, + /// Replay records by module. + pub leanchecker: BTreeMap, + /// Audit records by audit member name. + pub audit: BTreeMap, +} + +fn io(what: &str, error: &std::io::Error) -> Diagnostic { + Diagnostic::new( + crate::code!("LLB6003"), + format!("verification part: {what}: {error}"), + ) +} + +fn malformed(what: &str, reason: impl std::fmt::Display) -> Diagnostic { + Diagnostic::new( + crate::code!("LLI9001"), + format!("phase verify: verification part: {what}: {reason}"), + ) +} + +/// Copy the `.olean` tree and, when asked, read the process records of each +/// part in `parts` into the staging tree at `olean_root`. +/// +/// A module's `.olean` may come from one part only, and a record of one +/// process from one part only: two parts that both wrote one is a plan that +/// ran a process twice, which is refused rather than resolved. +/// +/// # Errors +/// +/// A part that cannot be read, a duplicate `.olean` or record, or a record +/// that does not parse as the verifier wrote it. +pub fn import( + parts: &[Utf8PathBuf], + olean_root: &Utf8Path, + with_records: bool, +) -> Result { + let mut imported = Imported::default(); + for part in parts { + if !part.as_std_path().is_dir() { + return Err(malformed( + part.as_str(), + "the output directory of a part is required and is not a directory", + )); + } + let oleans = part.join("oleans"); + if oleans.as_std_path().is_dir() { + for entry in walkdir::WalkDir::new(oleans.as_std_path()) + .sort_by_file_name() + .into_iter() + { + let entry = entry.map_err(|error| { + malformed(oleans.as_str(), format!("reading the olean tree: {error}")) + })?; + if !entry.file_type().is_file() { + continue; + } + let relative = entry + .path() + .strip_prefix(oleans.as_std_path()) + .map_err(|error| malformed(oleans.as_str(), error))?; + let relative = Utf8Path::from_path(relative).ok_or_else(|| { + malformed(oleans.as_str(), "a non-UTF-8 path in the olean tree") + })?; + let destination = olean_root.join(relative); + if destination.as_std_path().exists() { + return Err(malformed( + part.as_str(), + format!("`oleans/{relative}` was written by two parts of the run"), + )); + } + if let Some(parent) = destination.parent() { + std::fs::create_dir_all(parent.as_std_path()) + .map_err(|error| io("staging an imported olean", &error))?; + } + std::fs::copy(entry.path(), destination.as_std_path()) + .map_err(|error| io("copying an imported olean", &error))?; + if relative.extension() == Some("olean") { + let module = relative + .with_extension("") + .as_str() + .replace(['/', '\\'], "."); + imported.oleans.insert(module); + } + } + } + if !with_records { + continue; + } + read_records( + &part.join("process").join("lean"), + ".json", + &mut imported.lean, + part, + )?; + read_records( + &part.join("process").join("leanchecker"), + ".json", + &mut imported.leanchecker, + part, + )?; + read_records( + &part.join("audit"), + ".process.json", + &mut imported.audit, + part, + )?; + } + Ok(imported) +} + +/// Read every `` of `directory` as a process record keyed by +/// ``. +fn read_records( + directory: &Utf8Path, + suffix: &str, + into: &mut BTreeMap, + part: &Utf8Path, +) -> Result<(), Diagnostic> { + if !directory.as_std_path().is_dir() { + return Ok(()); + } + let mut names: Vec = Vec::new(); + for entry in std::fs::read_dir(directory.as_std_path()) + .map_err(|error| io("reading a part's records", &error))? + { + let entry = entry.map_err(|error| io("reading a part's records", &error))?; + let name = entry.file_name().to_string_lossy().into_owned(); + if let Some(stem) = name.strip_suffix(suffix) { + names.push(stem.to_owned()); + } + } + names.sort(); + for name in names { + let path = directory.join(format!("{name}{suffix}")); + let bytes = std::fs::read(path.as_std_path()) + .map_err(|error| io("reading a process record", &error))?; + let json = Json::parse(&bytes).map_err(|reason| malformed(path.as_str(), reason))?; + let record = + ChildRecord::from_json(&json).map_err(|reason| malformed(path.as_str(), reason))?; + if record.module.as_deref() != Some(name.as_str()) { + return Err(malformed( + path.as_str(), + "the record's module is not the one its file names", + )); + } + if into.insert(name.clone(), record).is_some() { + return Err(malformed( + part.as_str(), + format!("the record of `{name}` was written by two parts of the run"), + )); + } + } + Ok(()) +} + +/// Move what a shard ran out of its staging tree into `output`: the +/// `.olean` files of the modules in `own`, with their module-system +/// intermediates (a later part's elaboration reads them), the elaboration +/// and replay records, and the audit records. The `.olean` files the shard +/// imported stay behind: they are the part that produced them's to export, +/// once. Nothing else leaves the staging tree, which is removed with it. +/// +/// # Errors +/// +/// An output directory that exists and is not empty, or a move that fails. +pub fn export( + staging: &std::path::Path, + output: &Utf8Path, + own: &BTreeSet, +) -> Result<(), Diagnostic> { + if output.as_std_path().exists() { + let mut entries = std::fs::read_dir(output.as_std_path()) + .map_err(|error| io("reading the part's output directory", &error))?; + if entries.next().is_some() { + return Err(malformed( + output.as_str(), + "the output directory of a part must be empty", + )); + } + } + std::fs::create_dir_all(output.as_std_path()) + .map_err(|error| io("creating the part's output directory", &error))?; + let oleans = staging.join("oleans"); + if oleans.is_dir() { + for entry in walkdir::WalkDir::new(&oleans).sort_by_file_name() { + let entry = entry.map_err(|error| malformed("oleans", error))?; + if !entry.file_type().is_file() { + continue; + } + let relative = entry.path().strip_prefix(&oleans).unwrap_or(entry.path()); + // `X/M.olean`, `X/M.olean.private`, `X/M.ir`: the module is the + // path up to the file name's first dot. + let module = { + let text = relative.to_string_lossy().replace('\\', "/"); + let stem = text.split_once('.').map_or(text.as_str(), |(stem, _)| stem); + stem.replace('/', ".") + }; + if !own.contains(&module) { + continue; + } + let destination = + output + .join("oleans") + .join(Utf8Path::from_path(relative).ok_or_else(|| { + malformed("oleans", "a non-UTF-8 path in the olean tree") + })?); + if let Some(parent) = destination.parent() { + std::fs::create_dir_all(parent.as_std_path()) + .map_err(|error| io("creating the part's olean directory", &error))?; + } + move_file(entry.path(), destination.as_std_path())?; + } + } + let process = staging.join("process"); + if process.is_dir() { + move_tree(&process, output.join("process").as_std_path())?; + } + let audit = staging.join("audit"); + if audit.is_dir() { + let to = output.join("audit"); + std::fs::create_dir_all(to.as_std_path()) + .map_err(|error| io("creating the part's audit directory", &error))?; + for entry in + std::fs::read_dir(&audit).map_err(|error| io("reading the audit records", &error))? + { + let entry = entry.map_err(|error| io("reading the audit records", &error))?; + let name = entry.file_name().to_string_lossy().into_owned(); + if name.ends_with(".process.json") { + move_file(&entry.path(), to.join(&name).as_std_path())?; + } + } + } + Ok(()) +} + +fn move_tree(from: &std::path::Path, to: &std::path::Path) -> Result<(), Diagnostic> { + if std::fs::rename(from, to).is_ok() { + return Ok(()); + } + // Across file systems a rename fails; copy file by file and remove. + for entry in walkdir::WalkDir::new(from).into_iter().flatten() { + let relative = entry.path().strip_prefix(from).unwrap_or(entry.path()); + let destination = to.join(relative); + if entry.file_type().is_dir() { + std::fs::create_dir_all(&destination) + .map_err(|error| io("copying the part's output", &error))?; + } else if entry.file_type().is_file() { + if let Some(parent) = destination.parent() { + std::fs::create_dir_all(parent) + .map_err(|error| io("copying the part's output", &error))?; + } + std::fs::copy(entry.path(), &destination) + .map_err(|error| io("copying the part's output", &error))?; + } + } + std::fs::remove_dir_all(from).map_err(|error| io("removing the staged copy", &error)) +} + +fn move_file(from: &std::path::Path, to: &std::path::Path) -> Result<(), Diagnostic> { + if std::fs::rename(from, to).is_ok() { + return Ok(()); + } + std::fs::copy(from, to).map_err(|error| io("copying a part's record", &error))?; + std::fs::remove_file(from).map_err(|error| io("removing the staged copy", &error)) +} + +/// The order in which a whole verification consumes its elaborations (§22.11): +/// topological frontiers of the import graph, the members of each in module +/// order. A part's attestation lists its elaboration records in this order +/// whichever part ran them. +/// +/// `imports(index)` gives the project module names a module imports; +/// `name(index)` its project module name. +/// +/// # Errors +/// +/// A graph that does not converge (an import cycle, or an import of no +/// module), as the elaboration stage reports it. +pub fn elaboration_order( + count: usize, + name: &dyn Fn(usize) -> String, + imports: &dyn Fn(usize) -> Vec, +) -> Result>, Diagnostic> { + let mut placed: BTreeSet = BTreeSet::new(); + let mut remaining: Vec = (0..count).collect(); + let mut frontiers = Vec::new(); + while !remaining.is_empty() { + let ready: Vec = remaining + .iter() + .copied() + .filter(|index| imports(*index).iter().all(|import| placed.contains(import))) + .collect(); + if ready.is_empty() { + return Err(malformed("module order", "module order did not converge")); + } + for &index in &ready { + placed.insert(name(index)); + } + remaining.retain(|index| !ready.contains(index)); + frontiers.push(ready); + } + Ok(frontiers) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn a_plan_names_what_a_part_runs_and_the_whole_runs_everything() { + let plan = Plan { + elaborate: ["A.M".to_owned()].into_iter().collect(), + replay: ["A.N".to_owned()].into_iter().collect(), + }; + let shard = Part::Shard { + plan: &plan, + imports: &[], + output: Utf8Path::new("out"), + }; + assert!(shard.elaborates("A.M") && !shard.elaborates("A.N")); + assert!(shard.replays("A.N") && !shard.replays("A.M")); + assert!(!shard.publishes()); + let join = Part::Join { + plan: &plan, + parts: &[], + }; + assert!(join.publishes()); + assert!(Part::Whole.elaborates("anything") && Part::Whole.replays("anything")); + assert!(Part::Whole.publishes() && Part::Whole.inputs().is_empty()); + } + + #[test] + fn the_elaboration_order_is_the_frontiers_in_module_order() { + // 0 imports nothing, 1 imports 0, 2 imports nothing, 3 imports 1 and 2. + let names = ["A", "B", "C", "D"].map(str::to_owned); + let imports = |index: usize| -> Vec { + match index { + 1 => vec!["A".to_owned()], + 3 => vec!["B".to_owned(), "C".to_owned()], + _ => vec![], + } + }; + let order = elaboration_order(4, &|index| names[index].clone(), &imports).expect("order"); + assert_eq!(order, vec![vec![0, 2], vec![1], vec![3]]); + let cyclic = |index: usize| -> Vec { + match index { + 0 => vec!["B".to_owned()], + 1 => vec!["A".to_owned()], + _ => vec![], + } + }; + assert!(elaboration_order(2, &|index| names[index].clone(), &cyclic).is_err()); + } + + #[test] + fn a_part_output_round_trips_its_oleans_and_records() { + let staging = tempfile::tempdir().expect("tempdir"); + let olean = staging.path().join("oleans/X/M.olean"); + std::fs::create_dir_all(olean.parent().expect("parent")).expect("mkdir"); + std::fs::write(&olean, b"olean").expect("write"); + std::fs::write(staging.path().join("oleans/X/M.olean.private"), b"private").expect("write"); + std::fs::write(staging.path().join("oleans/X/N.olean"), b"imported").expect("write"); + let record = ChildRecord { + tool: "lean".to_owned(), + module: Some("X.M".to_owned()), + argv: vec!["env".to_owned(), "lean".to_owned()], + exit_code: 0, + stdout: "\n".to_owned(), + stderr: String::new(), + executable_sha256: crate::artifact::content_id::Sha256Digest::of(b"lean"), + }; + let audit_record = ChildRecord { + module: Some("LexLeanAudit.X.M".to_owned()), + ..record.clone() + }; + for (relative, written) in [ + ("process/lean/X.M.json", &record), + ("audit/LexLeanAudit.X.M.process.json", &audit_record), + ] { + let path = staging.path().join(relative); + std::fs::create_dir_all(path.parent().expect("parent")).expect("mkdir"); + std::fs::write(&path, written.to_json().to_file_bytes()).expect("write"); + } + std::fs::write( + staging.path().join("audit/LexLeanAudit.X.M.lean"), + b"source", + ) + .expect("write"); + let out = tempfile::tempdir().expect("tempdir"); + let output = Utf8PathBuf::from_path_buf(out.path().join("part")).expect("utf8"); + let own: BTreeSet = ["X.M".to_owned()].into_iter().collect(); + export(staging.path(), &output, &own).expect("exports"); + assert!( + staging.path().join("oleans/X/N.olean").exists() + && !staging.path().join("oleans/X/M.olean").exists(), + "an imported olean stays behind and an own one leaves" + ); + assert!( + staging.path().join("audit/LexLeanAudit.X.M.lean").exists(), + "the audit source stays with the staging tree" + ); + let into = tempfile::tempdir().expect("tempdir"); + let olean_root = Utf8PathBuf::from_path_buf(into.path().join("oleans")).expect("utf8"); + let imported = import(std::slice::from_ref(&output), &olean_root, true).expect("imports"); + assert_eq!(imported.oleans, ["X.M".to_owned()].into_iter().collect()); + assert!(olean_root.join("X/M.olean.private").as_std_path().is_file()); + assert_eq!(imported.lean.len(), 1); + assert!(imported.lean.contains_key("X.M")); + assert!(imported.leanchecker.is_empty()); + assert!(imported.audit.contains_key("LexLeanAudit.X.M")); + // The same part imported twice is a process that ran twice. + let again = import(&[output.clone(), output.clone()], &olean_root, false); + assert!(again.is_err(), "a duplicate olean is refused"); + // A record whose module is not the one its file names is refused. + let wrong = out.path().join("wrong/process/lean/X.N.json"); + std::fs::create_dir_all(wrong.parent().expect("parent")).expect("mkdir"); + std::fs::write(&wrong, record.to_json().to_file_bytes()).expect("write"); + let wrong_part = Utf8PathBuf::from_path_buf(out.path().join("wrong")).expect("utf8"); + let fresh = tempfile::tempdir().expect("tempdir"); + let fresh_root = Utf8PathBuf::from_path_buf(fresh.path().join("oleans")).expect("utf8"); + assert!(import(std::slice::from_ref(&wrong_part), &fresh_root, true).is_err()); + } +} diff --git a/features/suites/repository.feature b/features/suites/repository.feature index 5c6611d4a..32e93ed99 100644 --- a/features/suites/repository.feature +++ b/features/suites/repository.feature @@ -96,10 +96,10 @@ Feature: repository And a test recipe that includes repo-conformance, or a bdd recipe that runs fewer targets, fails the inventory @RP-14 @build - Scenario: 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 the other at the default, with no cache, path filter, or skipped recipe, and each leg uploads its CI evidence. - Given .github/workflows/ci.yml - When the runner, the environment, and the job steps are read - Then the job runs on ubuntu-24.04 with the 360-minute limit, and each verification profile variable is set once, from the leg's matrix row - And the leg that runs examples names width 2, a 12 GiB budget, and the committed hints, which the verifier parses, and the other leg names no profile - And its two legs run the recipes of vv, each exactly once, in the order of vv within a leg, and the leg that runs examples asserts that Atlas verified - And the vv job has no path filter, no cache action, no condition on a recipe, and each leg uploads its ci-evidence under a name of its own + Scenario: 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. + Given .github/workflows/ci.yml and .github/verify-shards.json + When the runner, the environment, the job steps, and the plan are read + Then every gate job runs on ubuntu-24.04 with the 360-minute limit, and each verification profile variable is set once per job, from the leg's matrix row or as the examples profile on an Atlas job + And the leg that runs examples names width 2, a 12 GiB budget, and the committed hints, which the verifier parses, verifies every example but uor-atlas, and the other leg names no profile and no part, and the two legs run the recipes of vv, each exactly once, in the order of vv within a leg, through the one gate command + And the Atlas jobs run every shard of the plan exactly once, each after the jobs of the shards it needs, from the one executable the prefix job built, the join asserts that Atlas verified, and the plan elaborates and replays every Atlas module exactly once with every import elaborated by the shard or by one it needs + And the vv job has no path filter, no cache action, and no condition on a recipe, the Atlas jobs wait only for a pull request to leave draft, and each job uploads its ci-evidence under a name of its own diff --git a/features/suites/verification.feature b/features/suites/verification.feature index 9ccc88292..b2c7026eb 100644 --- a/features/suites/verification.feature +++ b/features/suites/verification.feature @@ -160,3 +160,10 @@ Feature: verification When it is verified with and without telemetry Then the verified directories are byte-identical and the telemetry directory holds stage, frontier and process lines of the closed vocabulary And a verified directory in which a telemetry key is planted is refused + + @VR-23 @build + Scenario: 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. + Given a committed multi-module example project and a plan of two shards and a join over its import graph + When it is verified whole and as the parts of one run + Then the join publishes a verified directory byte-identical to the whole verification's, with the same attestation identity + And a shard whose plan elaborates a module before its imports, and a join that is handed one shard too few, are refused diff --git a/model/ids.toml b/model/ids.toml index 549859942..c9fa6428e 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -90,7 +90,7 @@ statement = "The ordinary workspace test phase excludes repo-conformance, the bd id = "RP-14" level = "build" suite = "repository" -statement = "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 the other at the default, with no cache, path filter, or skipped recipe, and each leg uploads its CI evidence." +statement = "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." [[id]] id = "CF-01" @@ -1256,6 +1256,12 @@ level = "build" suite = "verification" statement = "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." +[[id]] +id = "VR-23" +level = "build" +suite = "verification" +statement = "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." + [[id]] id = "CL-01" level = "build" diff --git a/xtask/Cargo.toml b/xtask/Cargo.toml index d0851b264..9ae0de1ac 100644 --- a/xtask/Cargo.toml +++ b/xtask/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "xtask" -description = "Repository gates: validate-model, validate-spec-links, verify-examples, check-golden, check-reproducibility, check-fixtures, check-calculus, check-production-export, check-package, check-test-inventory, ci-summary, ci-hints, release-artifacts, release-check, validate." +description = "Repository gates: validate-model, validate-spec-links, verify-examples, check-golden, check-reproducibility, check-fixtures, check-calculus, check-production-export, check-package, check-test-inventory, ci-summary, ci-hints, ci-shards, release-artifacts, release-check, validate." version.workspace = true edition.workspace = true rust-version.workspace = true diff --git a/xtask/src/ci.rs b/xtask/src/ci.rs index 9b3bd3578..5b64e4778 100644 --- a/xtask/src/ci.rs +++ b/xtask/src/ci.rs @@ -244,6 +244,47 @@ pub fn ci_hints(arguments: &[String]) -> Result<(), Fail> { Ok(()) } +/// Check the committed partition of an example's verification (SPEC.md §9.4): +/// every module elaborated by one shard and replayed by one, every import +/// elaborated by the shard or one it needs, the join needing every other +/// shard. With the committed hints, print what each shard is expected to +/// elaborate, as a reader of the plan would want to know; the estimate is +/// evidence, never an input. +pub fn ci_shards(root: &Path) -> Result<(), Fail> { + use repo_conformance::shards::{check, import_graph, Plan, PLAN_FILE}; + let plan = Plan::read(root)?; + let example = root.join("examples").join(&plan.project); + if !example.join("lexlean.toml").is_file() { + return Err(format!("{PLAN_FILE}: `{}` is no example directory", plan.project).into()); + } + let graph = import_graph(&example)?; + let lines = check(&plan, &graph)?; + let hints = std::fs::read_to_string(root.join(".github/verify-hints.json")) + .ok() + .and_then(|text| lexlean::verify::operational::Operational::parse_hints(&text).ok()); + for (line, (name, shard)) in lines.iter().zip(&plan.shards) { + let expected: u64 = hints.as_ref().map_or(0, |hints| { + shard + .elaborate + .iter() + .filter_map(|module| hints.get(module).map(|hint| hint.wall_ms)) + .sum() + }); + println!( + "ci-shards: {line}; elaboration expected {} s", + expected / 1000 + ); + let _ = name; + } + println!( + "ci-shards: {PLAN_FILE}: {} shards run the {} modules of `{}` once each (§9.4)", + plan.shards.len(), + graph.len(), + plan.project + ); + Ok(()) +} + #[cfg(test)] mod tests { use super::hints_from_telemetry; diff --git a/xtask/src/main.rs b/xtask/src/main.rs index 4aed8e1cb..c009259be 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -39,6 +39,7 @@ fn main() -> ExitCode { "check-test-inventory" => ci::check_test_inventory(&root), "ci-summary" => ci::ci_summary(&root, &std::env::args().skip(2).collect::>()), "ci-hints" => ci::ci_hints(&std::env::args().skip(2).collect::>()), + "ci-shards" => ci::ci_shards(&root), "release-artifacts" => release_artifacts(&root), "release-check" => release_check(&root), "validate" => codegen::check_model(&root, false).and_then(|()| spec_links::validate(&root)), @@ -63,6 +64,8 @@ fn main() -> ExitCode { ci-summary §9.4: summarize ci-evidence/ (recipe, stage, module times; memory)\n\ ci-hints §22.11: scheduling hints from a verifier telemetry file\n\ (--from verify-telemetry.jsonl --out hints.json)\n\ + ci-shards §9.4: the committed partition of an example's verification\n\ + runs every process once in import order\n\ release-artifacts §30.3: derive the release/ artifact set from the repository\n\ release-check RP-12: refuse release until §30.3/§30.4 are fully satisfied\n\ validate validate-model then validate-spec-links\n\ @@ -159,7 +162,18 @@ fn engine_for(dir: &Path) -> Result { /// probe and audit modules, process records with the platform-bound fields /// normalized) must equal it, and `--write` regenerates them. fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { - let dirs = example_dirs(root)?; + let part = ExamplesPart::from_environment()?; + let dirs: Vec = example_dirs(root)? + .into_iter() + .filter(|dir| part.includes(&dir.file_name().unwrap_or_default().to_string_lossy())) + .collect(); + if dirs.is_empty() { + return Err(format!( + "§9.4: the part `{}` names no example directory", + part.describe() + ) + .into()); + } for dir in dirs { let started = std::time::Instant::now(); let name = dir @@ -224,11 +238,84 @@ fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { }) .map_err(|error| format!("{name}: build: {error}"))?; lap("build"); - let verified = engine - .verify(lexlean::VerifyRequest { - selection: lexlean::Selection::Entrypoints, - }) - .map_err(|error| format!("{name}: verify: {error}"))?; + // The part of the gate this job is (§9.4): a shard of one example's + // verification runs the processes its plan names and leaves; the join + // publishes and is compared like a whole verification. + let verified = match &part { + ExamplesPart::Shard { + example, + shard, + parts, + } if *example == name => { + let plan = repo_conformance::shards::Plan::read(root)?; + let shard_plan = shard_plan(&plan, &name, shard)?; + let imports: Vec = plan + .needs_closure(shard)? + .into_iter() + .map(|need| utf8(&parts.join(need))) + .collect::>()?; + let output = utf8(&parts.join(shard))?; + let outcome = engine + .verify_part( + lexlean::VerifyRequest { + selection: lexlean::Selection::Entrypoints, + }, + lexlean::VerifyPart::Shard { + plan: shard_plan, + imports, + output, + }, + ) + .map_err(|error| format!("{name}: verify (shard {shard}): {error}"))?; + lap("verify"); + let lexlean::VerifyPartOutcome::Shard { output, processes } = outcome else { + return Err(format!("{name}: shard `{shard}` published a verification").into()); + }; + println!( + "verify-examples: {name} took {} s", + started.elapsed().as_secs() + ); + println!( + "verify-examples: {name}: shard `{shard}` ran {processes} processes into {output}" + ); + append_example_telemetry(&name, started, &steps, Some(shard)); + continue; + } + ExamplesPart::Join { example, parts } if *example == name => { + let plan = repo_conformance::shards::Plan::read(root)?; + let join_plan = shard_plan(&plan, &name, repo_conformance::shards::JOIN)?; + let others: Vec = plan + .shards + .keys() + .filter(|shard| shard.as_str() != repo_conformance::shards::JOIN) + .map(|shard| utf8(&parts.join(shard))) + .collect::>()?; + let outcome = engine + .verify_part( + lexlean::VerifyRequest { + selection: lexlean::Selection::Entrypoints, + }, + lexlean::VerifyPart::Join { + plan: join_plan, + parts: others, + }, + ) + .map_err(|error| format!("{name}: verify (join): {error}"))?; + let lexlean::VerifyPartOutcome::Verified(verified) = outcome else { + return Err(format!("{name}: the join published no verification").into()); + }; + println!( + "verify-examples: {name}: joined {} shards", + plan.shards.len() - 1 + ); + verified + } + _ => engine + .verify(lexlean::VerifyRequest { + selection: lexlean::Selection::Entrypoints, + }) + .map_err(|error| format!("{name}: verify: {error}"))?, + }; lap("verify"); // The wall-clock of each example is printed so that a run that // approaches the CI job limit shows where its time went. @@ -256,22 +343,7 @@ fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { "verify-examples: {name} verified-digest {}", ci::tree_digest(verified.root.as_std_path())? ); - if let Some(directory) = std::env::var_os(lexlean::verify::operational::TELEMETRY_VARIABLE) - .filter(|value| !value.is_empty()) - { - lexlean::verify::telemetry::append( - Path::new(&directory), - "examples-telemetry.jsonl", - &serde_json::json!({ - "event": "example", - "example": name, - "wall_ms": u64::try_from(started.elapsed().as_millis()).unwrap_or(u64::MAX), - "process_width": lexlean::verify::operational::Operational::from_environment() - .map_or(0, |operational| operational.width()), - "steps": steps, - }), - ); - } + append_example_telemetry(&name, started, &steps, None); let records = normalized_verify_records(verified.root.as_std_path())?; let expected_root = dir.join("expected").join("verify"); @@ -307,6 +379,156 @@ fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { Ok(()) } +/// The variable that names the part of the `examples` recipe a CI job runs +/// (SPEC.md §9.4). Unset or empty, the recipe verifies every example whole. +pub const EXAMPLES_PART_VARIABLE: &str = "LEXLEAN_EXAMPLES_PART"; + +/// The variable that names the directory the parts of a sharded example +/// exchange their output through: one subdirectory per shard, named after +/// it. Required by a shard or join part. +pub const EXAMPLES_PARTS_VARIABLE: &str = "LEXLEAN_EXAMPLES_PARTS"; + +/// Which part of the `examples` recipe a job runs (§9.4). +#[derive(Debug, Clone, PartialEq, Eq)] +enum ExamplesPart { + /// Every example, whole. + All, + /// Every example but one, whole. + Without(String), + /// One shard of one example's verification. + Shard { + example: String, + shard: String, + parts: PathBuf, + }, + /// The join of one example's verification. + Join { example: String, parts: PathBuf }, +} + +impl ExamplesPart { + /// Read the part from the environment: `without:`, + /// `shard::`, or `join:`; unset or empty is + /// every example whole. + fn from_environment() -> Result { + let value = std::env::var_os(EXAMPLES_PART_VARIABLE).unwrap_or_default(); + let text = value + .to_str() + .ok_or_else(|| format!("{EXAMPLES_PART_VARIABLE}: the value is not Unicode"))?; + Self::parse(text, || { + std::env::var_os(EXAMPLES_PARTS_VARIABLE) + .filter(|value| !value.is_empty()) + .map(PathBuf::from) + .ok_or_else(|| { + format!("{EXAMPLES_PARTS_VARIABLE}: a shard or join part names the directory the parts exchange their output through").into() + }) + }) + } + + fn parse(text: &str, parts: impl Fn() -> Result) -> Result { + let fields: Vec<&str> = text.split(':').collect(); + let malformed = || -> Fail { + format!( + "{EXAMPLES_PART_VARIABLE}: `{text}` is not a part: expected empty, `without:`, `shard::`, or `join:`" + ) + .into() + }; + let named = |field: &str| -> Result { + if field.is_empty() || field.contains(['/', '\\', '.']) { + return Err(malformed()); + } + Ok(field.to_owned()) + }; + match fields.as_slice() { + [""] => Ok(Self::All), + ["without", example] => Ok(Self::Without(named(example)?)), + ["shard", example, shard] => Ok(Self::Shard { + example: named(example)?, + shard: named(shard)?, + parts: parts()?, + }), + ["join", example] => Ok(Self::Join { + example: named(example)?, + parts: parts()?, + }), + _ => Err(malformed()), + } + } + + /// Does this part run the example directory named `name`? + fn includes(&self, name: &str) -> bool { + match self { + Self::All => true, + Self::Without(example) => example != name, + Self::Shard { example, .. } | Self::Join { example, .. } => example == name, + } + } + + fn describe(&self) -> String { + match self { + Self::All => "all".to_owned(), + Self::Without(example) => format!("without:{example}"), + Self::Shard { example, shard, .. } => format!("shard:{example}:{shard}"), + Self::Join { example, .. } => format!("join:{example}"), + } + } +} + +/// The plan of one shard of `example`, as the verifier takes it. +fn shard_plan( + plan: &repo_conformance::shards::Plan, + example: &str, + shard: &str, +) -> Result { + if plan.project != example { + return Err(format!( + "§9.4: {} partitions `{}`, and the part names `{example}`", + repo_conformance::shards::PLAN_FILE, + plan.project + ) + .into()); + } + let found = plan.shards.get(shard).ok_or_else(|| { + format!( + "§9.4: {} has no shard `{shard}`", + repo_conformance::shards::PLAN_FILE + ) + })?; + Ok(lexlean::VerifyPlan { + elaborate: found.elaborate.clone(), + replay: found.replay.clone(), + }) +} + +/// One `example` event of the CI evidence (§22.12): the example, what each +/// step took, and the part that ran it when the example ran as a part. +fn append_example_telemetry( + name: &str, + started: std::time::Instant, + steps: &serde_json::Map, + shard: Option<&str>, +) { + if let Some(directory) = std::env::var_os(lexlean::verify::operational::TELEMETRY_VARIABLE) + .filter(|value| !value.is_empty()) + { + let mut event = serde_json::json!({ + "event": "example", + "example": name, + "wall_ms": u64::try_from(started.elapsed().as_millis()).unwrap_or(u64::MAX), + "process_width": lexlean::verify::operational::Operational::from_environment() + .map_or(0, |operational| operational.width()), + "steps": steps, + }); + if let Some(shard) = shard { + event["shard"] = serde_json::Value::String(shard.to_owned()); + } + lexlean::verify::telemetry::append( + Path::new(&directory), + "examples-telemetry.jsonl", + &event, + ); + } +} + /// The verification records that are platform independent after /// normalization (§22.7, §29.5): the audit output, the probe, audit, and /// extraction modules, the canonical compiler input, the preservation @@ -977,3 +1199,56 @@ mod tests { ); } } + +#[cfg(test)] +mod examples_part_tests { + use super::ExamplesPart; + use std::path::PathBuf; + + #[test] + fn a_part_is_read_from_its_text_and_a_shard_needs_the_parts_directory() { + let parts = || Ok(PathBuf::from("parts")); + assert_eq!( + ExamplesPart::parse("", parts).expect("empty"), + ExamplesPart::All + ); + assert_eq!( + ExamplesPart::parse("without:uor-atlas", parts).expect("without"), + ExamplesPart::Without("uor-atlas".to_owned()) + ); + assert_eq!( + ExamplesPart::parse("shard:uor-atlas:pairs-a", parts).expect("shard"), + ExamplesPart::Shard { + example: "uor-atlas".to_owned(), + shard: "pairs-a".to_owned(), + parts: PathBuf::from("parts"), + } + ); + assert_eq!( + ExamplesPart::parse("join:uor-atlas", parts).expect("join"), + ExamplesPart::Join { + example: "uor-atlas".to_owned(), + parts: PathBuf::from("parts"), + } + ); + for malformed in [ + "all", + "shard:uor-atlas", + "join:", + "without:../x", + "shard:a:b:c", + ] { + assert!( + ExamplesPart::parse(malformed, parts).is_err(), + "{malformed}" + ); + } + let no_parts = || Err("no parts directory".into()); + assert!(ExamplesPart::parse("join:uor-atlas", no_parts).is_err()); + assert!(ExamplesPart::parse("without:uor-atlas", no_parts).is_ok()); + let shard = ExamplesPart::parse("shard:uor-atlas:prefix", parts).expect("shard"); + assert!(shard.includes("uor-atlas") && !shard.includes("compiler")); + assert!(ExamplesPart::Without("uor-atlas".to_owned()).includes("compiler")); + assert_eq!(shard.describe(), "shard:uor-atlas:prefix"); + } +} diff --git a/xtask/src/spec_links.rs b/xtask/src/spec_links.rs index d2b81b421..36fe0aa47 100644 --- a/xtask/src/spec_links.rs +++ b/xtask/src/spec_links.rs @@ -61,8 +61,8 @@ fn parse_table(spec: &str) -> Result, Fail> { pub fn validate(root: &Path) -> Result<(), Fail> { let spec = std::fs::read_to_string(root.join("SPEC.md"))?; let rows = parse_table(&spec)?; - if rows.len() != 381 { - return Err(format!("RP-07: the §31 table has {} rows, not 381", rows.len()).into()); + if rows.len() != 382 { + return Err(format!("RP-07: the §31 table has {} rows, not 382", rows.len()).into()); } // The prose total under the table is part of the contract a reader // relies on; a row added without it would leave §31 contradicting itself. From 9ea7d556cf2df8020341c4381b226103d0d48bdc Mon Sep 17 00:00:00 2001 From: humuhumu33 <68450279+humuhumu33@users.noreply.github.com> Date: Fri, 16 Oct 2026 13:57:30 +0100 Subject: [PATCH 2/2] fix(#131): verify_part is repository tooling beside the stable entry points, and the VR range ends at VR-23 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CL-13 counts the seven public entry points of Engine (§24.1); verify_part is now a free function, lexlean::verify_part, used by xtask and VR-23. RP-11: the README's verification range ends at the register's last VR ID. Co-Authored-By: Claude Fable 5.1 --- CHANGELOG.md | 2 +- README.md | 2 +- VERIFICATION.md | 2 +- crates/conformance/src/cases/operational.rs | 3 +- crates/conformance/src/cases/verification.rs | 2 +- crates/lexlean/src/api.rs | 93 ++++++++++---------- crates/lexlean/src/lib.rs | 1 + xtask/src/main.rs | 46 +++++----- 8 files changed, 76 insertions(+), 75 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bd5be693..60bfc9cd9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,7 +24,7 @@ versions, and the entries below say what each tag does and does not claim. `cargo xtask ci-shards` against the import graph of the committed build: every module elaborated by one shard and replayed by one, every import elaborated by the shard or by one it needs. The verifier runs as one part - through `Engine::verify_part` (`verify::partition`): a shard runs the + through `lexlean::verify_part` (`verify::partition`): a shard runs the prelude whole, then elaborates, replays, and audits the modules of its plan with the `.olean` files of the shards it needs, and writes its records; the join reads every shard's records, judges each as its stage does, and diff --git a/README.md b/README.md index 374e321ff..e3d3a22aa 100644 --- a/README.md +++ b/README.md @@ -160,7 +160,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row, | Prose-free deterministic generated Lean with complete token traceability | `LN-01`..`LN-12` | `build` | | Canonical LaTeX regeneration and the optional hash-checked PDF provider | `TX-01`..`TX-12` | `build` | | Canonical diagnostics, source maps, coverage, manifests, and reproducible builds | `AR-01`..`AR-14` | `build` | -| Fifteen-stage verification with leanchecker replay and exact axiom audit | `VR-01`..`VR-22` | `build` | +| Fifteen-stage verification with leanchecker replay and exact axiom audit | `VR-01`..`VR-23` | `build` | | The exact CLI contract, the stable seven-method Rust `Engine` API, the host-driven end of the children the library started, and the `production` subcommands | `CL-01`..`CL-23` | `build` | | Filesystem confinement, no shell, no hidden network, closed failure model | `SE-01`..`SE-12` | `build` | | Language-1.2 production eligibility: closed targets, effects, and construct dispositions; runtime closures; target-dependent, fail-closed root analysis; deterministic eligibility reports; an exhaustiveness audit | `PD-01`..`PD-07` | `build` | diff --git a/VERIFICATION.md b/VERIFICATION.md index 1fa8bcb90..0873054c3 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -7701,7 +7701,7 @@ for the Atlas side against 178; the first CI run of the change is the measurement, and the `rest` leg (76 minutes, 64 of them `bdd`) is then the longer one. -The verifier runs as one part through `Engine::verify_part` +The verifier runs as one part through `lexlean::verify_part` (`verify::partition`, SPEC.md §9.4, §22.11). A shard runs the prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), seeds the placed set with the modules whose `.olean` arrived from diff --git a/crates/conformance/src/cases/operational.rs b/crates/conformance/src/cases/operational.rs index e42ce5ff5..ce3ca8a7e 100644 --- a/crates/conformance/src/cases/operational.rs +++ b/crates/conformance/src/cases/operational.rs @@ -812,7 +812,8 @@ fn parts_equal_the_whole() { let _environment = support::env_shared(); let project = P::copy_example(example); let outcome = Operational::new(1, None).expect("width 1").scoped(|| { - project.engine().verify_part( + lexlean::verify_part( + &project.engine(), VerifyRequest { selection: Selection::Entrypoints, }, diff --git a/crates/conformance/src/cases/verification.rs b/crates/conformance/src/cases/verification.rs index 87c5a752e..8d28789c8 100644 --- a/crates/conformance/src/cases/verification.rs +++ b/crates/conformance/src/cases/verification.rs @@ -1,4 +1,4 @@ -//! The `verification` suite: VR-01..VR-22. +//! The `verification` suite: VR-01..VR-23. use lexlean::{Selection, VerifyRequest}; diff --git a/crates/lexlean/src/api.rs b/crates/lexlean/src/api.rs index 133093e4e..6e1a185ad 100644 --- a/crates/lexlean/src/api.rs +++ b/crates/lexlean/src/api.rs @@ -989,53 +989,6 @@ impl Engine { } } - /// Verify a selection as one part of a verification run as several - /// parts (SPEC.md §9.4): a shard runs the processes its plan names and - /// writes them to its output directory; the join runs its own, reads - /// every other part's, and publishes through the same pipeline as - /// [`Self::verify`]. A part is defined for a project without production - /// roots and without PDF rendering. - pub fn verify_part( - &self, - request: VerifyRequest, - part: VerifyPart, - ) -> Result { - let plan_of = |plan: &VerifyPlan| crate::verify::Plan { - elaborate: plan.elaborate.iter().cloned().collect(), - replay: plan.replay.iter().cloned().collect(), - }; - match &part { - VerifyPart::Shard { - plan, - imports, - output, - } => { - let plan = plan_of(plan); - self.bound( - "verify", - self.verify_part_inner( - &request, - &crate::verify::Part::Shard { - plan: &plan, - imports, - output, - }, - ), - ) - } - VerifyPart::Join { plan, parts } => { - let plan = plan_of(plan); - self.bound( - "verify", - self.verify_part_inner( - &request, - &crate::verify::Part::Join { plan: &plan, parts }, - ), - ) - } - } - } - fn verify_part_inner( &self, request: &VerifyRequest, @@ -1471,3 +1424,49 @@ pub fn command_result_json( } Json::object(fields) } + +/// Verify a project as one part of a verification run as several +/// parts (SPEC.md §9.4): a shard runs the processes its plan names and +/// writes them to its output directory; the join runs its own, reads +/// every other part's, and publishes through the same pipeline as +/// [`Engine::verify`]. It is repository tooling for the CI gate, not one of +/// the stable entry points of §24.1. A part is defined for a project without production +/// roots and without PDF rendering. +pub fn verify_part( + engine: &Engine, + request: VerifyRequest, + part: VerifyPart, +) -> Result { + let plan_of = |plan: &VerifyPlan| crate::verify::Plan { + elaborate: plan.elaborate.iter().cloned().collect(), + replay: plan.replay.iter().cloned().collect(), + }; + match &part { + VerifyPart::Shard { + plan, + imports, + output, + } => { + let plan = plan_of(plan); + engine.bound( + "verify", + engine.verify_part_inner( + &request, + &crate::verify::Part::Shard { + plan: &plan, + imports, + output, + }, + ), + ) + } + VerifyPart::Join { plan, parts } => { + let plan = plan_of(plan); + engine.bound( + "verify", + engine + .verify_part_inner(&request, &crate::verify::Part::Join { plan: &plan, parts }), + ) + } + } +} diff --git a/crates/lexlean/src/lib.rs b/crates/lexlean/src/lib.rs index 6cfa379ae..6556d1abc 100644 --- a/crates/lexlean/src/lib.rs +++ b/crates/lexlean/src/lib.rs @@ -61,6 +61,7 @@ pub mod surface; #[doc(hidden)] pub mod verify; +pub use api::verify_part; pub use api::{ BuildRequest, BuiltUnit, CheckRequest, CheckedUnit, CheckedUnitSummary, Engine, FormatRequest, FormatResultSet, LockRequest, LockResult, ModuleArtifacts, ProjectResultSet, Selection, diff --git a/xtask/src/main.rs b/xtask/src/main.rs index c009259be..01af57ad5 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -255,18 +255,18 @@ fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { .map(|need| utf8(&parts.join(need))) .collect::>()?; let output = utf8(&parts.join(shard))?; - let outcome = engine - .verify_part( - lexlean::VerifyRequest { - selection: lexlean::Selection::Entrypoints, - }, - lexlean::VerifyPart::Shard { - plan: shard_plan, - imports, - output, - }, - ) - .map_err(|error| format!("{name}: verify (shard {shard}): {error}"))?; + let outcome = lexlean::verify_part( + &engine, + lexlean::VerifyRequest { + selection: lexlean::Selection::Entrypoints, + }, + lexlean::VerifyPart::Shard { + plan: shard_plan, + imports, + output, + }, + ) + .map_err(|error| format!("{name}: verify (shard {shard}): {error}"))?; lap("verify"); let lexlean::VerifyPartOutcome::Shard { output, processes } = outcome else { return Err(format!("{name}: shard `{shard}` published a verification").into()); @@ -290,17 +290,17 @@ fn verify_examples(root: &Path, write: bool) -> Result<(), Fail> { .filter(|shard| shard.as_str() != repo_conformance::shards::JOIN) .map(|shard| utf8(&parts.join(shard))) .collect::>()?; - let outcome = engine - .verify_part( - lexlean::VerifyRequest { - selection: lexlean::Selection::Entrypoints, - }, - lexlean::VerifyPart::Join { - plan: join_plan, - parts: others, - }, - ) - .map_err(|error| format!("{name}: verify (join): {error}"))?; + let outcome = lexlean::verify_part( + &engine, + lexlean::VerifyRequest { + selection: lexlean::Selection::Entrypoints, + }, + lexlean::VerifyPart::Join { + plan: join_plan, + parts: others, + }, + ) + .map_err(|error| format!("{name}: verify (join): {error}"))?; let lexlean::VerifyPartOutcome::Verified(verified) = outcome else { return Err(format!("{name}: the join published no verification").into()); };