deep-checks #119
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: AGPL-3.0-only | |
| # Copyright (C) 2026 RS-Key contributors | |
| # Scheduled deep checks — the slow adversarial suites that are deliberately | |
| # not part of the merge gate (docs/testing.md). | |
| # | |
| # Two cadences, because the suites no longer fit one. Every row that answers | |
| # "did today's tree break something" runs daily; the slower assurance sweeps run | |
| # on Sunday, where their runners do not compete with the daily rows. | |
| # | |
| # DAILY | |
| # miri — fuzz/tests/miri.rs: every fuzz target's logic under Miri's UB | |
| # checker, sharded (scripts/miri-all.sh). MIRIFLAGS policy comes from | |
| # the .#fuzz dev shell. | |
| # fuzz — a timed libFuzzer pass over every cargo-fuzz target, sharded | |
| # (scripts/fuzz-all.sh). The corpus is carried between runs via the | |
| # actions cache, so its coverage accumulates day over day; crash | |
| # artifacts are uploaded. | |
| # fuzz-coverage — per-target libFuzzer region/line coverage over that | |
| # accumulated corpus (scripts/fuzz-coverage.sh): a summary table on the | |
| # step page and the per-target HTML uploaded. Advisory, not a gate. | |
| # repro — `nix build .#firmware` twice (`--rebuild` diffs every output | |
| # byte): proves the hermetic image is bit-reproducible and publishes | |
| # the canonical sha256 for this flake.lock (docs/build.md). | |
| # coverage — `cargo llvm-cov` line coverage over the host crates, floored: | |
| # a regression alarm on the host-testable surface (the embedded | |
| # firmware image is not host-measurable). scripts/metrics.sh is the | |
| # separate, un-gated refactor-reconnaissance tool. | |
| # | |
| # WEEKLY (Sunday) | |
| # kani — every #[kani::proof] harness, one runner per tier: the three `light*` | |
| # shards and `heavy`, which together are the `all` roster of | |
| # `scripts/kani.sh` (docs/testing.md). The fast tier of that same script runs | |
| # per-PR in ci.yml; these four owe the whole roster between them. They | |
| # are separate jobs for two measured reasons — `rsk-phy`'s | |
| # round-trip peaks at 11.1 GB and takes the runner down with it, so its | |
| # death costs its own crate only; and the rest, run in one job, cost the | |
| # sum of every crate's solving rather than the slowest shard's. Kani is | |
| # not in nixpkgs and its setup downloads a prebuilt CBMC bundle, so | |
| # these jobs are rustup-based, not nix. | |
| # mutants — cargo-mutants over the host crates, sharded | |
| # (scripts/mutants-all.sh). Coverage says a line ran; this says a test | |
| # would notice if it changed. **Advisory**, for the reason that script | |
| # states at length: most survivors are not defects, so a gating row | |
| # would be red every week. | |
| # comutants — the semantic model mutants re-injected into production Rust | |
| # (`scripts/comutate.py run`). Gating: every recorded code-level kill | |
| # must still go red, and a new GAP is an abstraction-fidelity finding. | |
| # formal — TLC over formal/: the model, its 44 mutants, their floors and the | |
| # vacuity check (formal/run-tlc.sh `safety`). Gating. It also runs on | |
| # any push touching formal/, so an edit to the model is checked at once | |
| # rather than up to a week later. The `liveness` tier is deliberately | |
| # not here — it needs a 12g heap, and 11.1 GB is where the kani `heavy` | |
| # runner already died twice. | |
| # | |
| # `complexity` used to be here and is gone: scripts/check.sh already runs | |
| # scripts/complexity_gate.sh on every pull request, so the row re-proved a merge | |
| # gate a day later. | |
| # | |
| # Runs on both schedules, on demand (workflow_dispatch, with a per-target time | |
| # knob), and self-tests on any push that edits this file — a dispatch or a push | |
| # runs BOTH cadences, which is what makes an edit here self-testing. Local | |
| # equivalents: | |
| # nix develop .#fuzz -c ./scripts/miri-all.sh (MIRI_SHARD=2/3 for one shard) | |
| # nix develop .#fuzz -c ./scripts/fuzz-all.sh (FUZZ_SECONDS=30 to shorten) | |
| # nix develop .#fuzz -c ./scripts/fuzz-coverage.sh | |
| # ./scripts/kani.sh all (needs `cargo install kani-verifier` first — not nix) | |
| # ./scripts/kani.sh light1 ./scripts/kani.sh heavy # what the weekly rows run | |
| # nix develop -c ./scripts/mutants-all.sh (MUTANTS_SHARD=2/12 for one shard) | |
| # nix develop -c python scripts/comutate.py run | |
| # nix develop -c cargo llvm-cov --summary-only --fail-under-lines 80 --target <host> --workspace --exclude firmware --exclude rsk-wipe | |
| name: deep-checks | |
| on: | |
| schedule: | |
| - cron: "17 5 * * *" # 05:17 UTC daily | |
| - cron: "41 5 * * 0" # 05:41 UTC Sunday — the weeks-scale rows | |
| workflow_dispatch: | |
| inputs: | |
| fuzz_seconds: | |
| description: seconds of fuzzing per target | |
| default: "120" | |
| push: | |
| branches: [main] | |
| paths: | |
| [ | |
| ".github/workflows/deep-checks.yml", | |
| "nix/devshells.nix", | |
| "nix/firmware.nix", | |
| "scripts/fuzz-coverage.sh", | |
| "scripts/fuzz-all.sh", | |
| "scripts/miri-all.sh", | |
| "scripts/mutants-all.sh", | |
| "scripts/comutate.py", | |
| "scripts/kani.sh", | |
| "formal/**", | |
| ] | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: deep-checks | |
| cancel-in-progress: true | |
| # Each job names the cadence it is NOT, rather than the one it is: a scheduled run | |
| # carries the cron that started it, and a dispatch or a push carries none, so | |
| # "not the other one" runs everything by hand and everything on an edit. | |
| jobs: | |
| miri: | |
| if: github.event.schedule != '41 5 * * 0' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 240 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| shard: [1, 2, 3] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-fuzz-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: | | |
| nix-fuzz-${{ runner.os }}- | |
| nix-${{ runner.os }}- | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| fuzz/target | |
| key: miri-${{ runner.os }}-${{ hashFiles('fuzz/Cargo.lock', 'flake.lock') }} | |
| restore-keys: miri-${{ runner.os }}- | |
| - name: miri — every fuzz target's logic under the UB checker | |
| run: nix develop .#fuzz -c ./scripts/miri-all.sh | |
| env: | |
| MIRI_SHARD: ${{ matrix.shard }}/3 | |
| fuzz: | |
| if: github.event.schedule != '41 5 * * 0' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 240 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| shard: [1, 2, 3, 4] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-fuzz-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: | | |
| nix-fuzz-${{ runner.os }}- | |
| nix-${{ runner.os }}- | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| fuzz/target | |
| key: fuzz-${{ runner.os }}-${{ hashFiles('fuzz/Cargo.lock', 'flake.lock') }} | |
| restore-keys: fuzz-${{ runner.os }}- | |
| # One corpus entry per shard: four jobs cannot write one key, and a shard | |
| # only ever fuzzes its own slice of the roster. The slice is positional, so | |
| # adding a target shifts the ones after it into a neighbouring shard and | |
| # costs them their accumulated inputs once — see the comment in | |
| # scripts/fuzz-all.sh for why balance won that trade. | |
| - uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s${{ matrix.shard }}-${{ github.run_id }} | |
| restore-keys: fuzz-corpus-s${{ matrix.shard }}- | |
| - name: build every fuzz target | |
| run: nix develop .#fuzz -c cargo fuzz build | |
| # A script, not an inline `-c bash -c '…'`: that form loses the dev shell's | |
| # PATH here and `cargo` falls through to the image's rustup shim, which | |
| # syncs stable and answers "no such command: fuzz". Measured in one run, | |
| # same image, same minute — the `fuzz-coverage` row below, which already | |
| # calls its script this way, listed 53 targets while this one listed 0 and | |
| # tripped its own roster floor. The floor did its job; the shape was wrong. | |
| - name: fuzz this shard's targets | |
| run: nix develop .#fuzz -c ./scripts/fuzz-all.sh | |
| env: | |
| FUZZ_SECONDS: ${{ inputs.fuzz_seconds || '120' }} | |
| FUZZ_SHARD: ${{ matrix.shard }}/4 | |
| - name: upload crash artifacts | |
| if: failure() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: fuzz-artifacts-${{ github.run_id }}-s${{ matrix.shard }} | |
| path: fuzz/artifacts/ | |
| if-no-files-found: ignore | |
| - uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| if: always() | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s${{ matrix.shard }}-${{ github.run_id }} | |
| fuzz-coverage: | |
| if: github.event.schedule != '41 5 * * 0' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 120 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-fuzz-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: | | |
| nix-fuzz-${{ runner.os }}- | |
| nix-${{ runner.os }}- | |
| # The instrumented coverage build lives in fuzz/coverage/.build (a distinct | |
| # target-dir from the fuzzing build), so cache it under its own key. | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| fuzz/coverage/.build | |
| key: fuzz-cov-${{ runner.os }}-${{ hashFiles('fuzz/Cargo.lock', 'flake.lock') }} | |
| restore-keys: fuzz-cov-${{ runner.os }}- | |
| # Read (never write) the corpora the `fuzz` shards accumulated on the | |
| # previous run: coverage measures those saved inputs, not a fresh fuzzing | |
| # pass. One restore per shard, because that is how they are stored; they | |
| # extract into the same tree and the per-target directories are disjoint. | |
| # Restoring only one would measure a quarter of the roster against a floor | |
| # written for all of it. | |
| - uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s1-${{ github.run_id }} | |
| restore-keys: fuzz-corpus-s1- | |
| - uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s2-${{ github.run_id }} | |
| restore-keys: fuzz-corpus-s2- | |
| - uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s3-${{ github.run_id }} | |
| restore-keys: fuzz-corpus-s3- | |
| - uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: fuzz/corpus | |
| key: fuzz-corpus-s4-${{ github.run_id }} | |
| restore-keys: fuzz-corpus-s4- | |
| - name: per-target libFuzzer coverage over the accumulated corpus | |
| run: nix develop .#fuzz -c ./scripts/fuzz-coverage.sh | |
| - name: upload the per-target HTML reports | |
| if: always() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: fuzz-coverage-${{ github.run_id }} | |
| path: fuzz/coverage/*/html | |
| if-no-files-found: ignore | |
| repro: | |
| if: github.event.schedule != '41 5 * * 0' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: nix-${{ runner.os }}- | |
| - name: build the firmware image | |
| run: nix build .#firmware -o result-repro | |
| - name: rebuild and require bit-identical outputs | |
| run: nix build .#firmware --rebuild | |
| - name: publish the reproducible hashes | |
| run: | | |
| { | |
| echo "### Reproducible firmware (this flake.lock, x86_64-linux)" | |
| echo '```' | |
| (cd result-repro && sha256sum firmware.uf2 firmware.elf) | |
| echo '```' | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| coverage: | |
| if: github.event.schedule != '41 5 * * 0' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: nix-${{ runner.os }}- | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: coverage-${{ runner.os }}-${{ hashFiles('Cargo.lock') }} | |
| restore-keys: coverage-${{ runner.os }}- | |
| # Host crates only — the embedded firmware image is not host-measurable, so | |
| # its coverage is 0 by construction. firmware and rsk-wipe are the two | |
| # workspace members that are not under crates/ and the two that are | |
| # thumbv8m-only, so the exclusion is the whole of it; scripts/roster_gate.py | |
| # holds this row and the header's copy of it to that pair. The 80% floor is | |
| # a regression alarm, not a target: 85.0% line over the host crates | |
| # (aarch64-apple-darwin), so a real drop fails and noise does not. | |
| - name: llvm-cov — host-crate line coverage, floored at 80% | |
| run: | | |
| nix develop -c cargo llvm-cov --summary-only --fail-under-lines 80 \ | |
| --target x86_64-unknown-linux-gnu \ | |
| --workspace --exclude firmware --exclude rsk-wipe | |
| kani: | |
| if: github.event.schedule != '17 5 * * *' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 360 | |
| env: | |
| KANI_VERSION: "0.67.0" | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| tier: [light1, light2, light3, heavy] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.kani | |
| ~/.cargo/bin/cargo-kani | |
| ~/.cargo/bin/kani | |
| ~/.cargo/registry | |
| key: kani-${{ runner.os }}-${{ env.KANI_VERSION }} | |
| - name: install kani (rustup-based — not packaged in nixpkgs) | |
| run: | | |
| command -v cargo-kani >/dev/null || cargo install --locked kani-verifier --version "$KANI_VERSION" | |
| cargo kani setup | |
| # The tier names come from the matrix and the crates from `scripts/kani.sh`; | |
| # scripts/kani_gate.py resolves the one to reach the other, and refuses a | |
| # `-p` roster written anywhere but that script. | |
| # | |
| # The script floors the harness count and the `kani::cover!` count, because | |
| # a roster that selects nothing exits 0 and so does a cover nothing reaches. | |
| # `--harness-timeout`, which it passes, is per harness and not per row — | |
| # Kani runs the rest and fails at the end. It is set to this job's own 6 h, | |
| # so `timeout-minutes` is the real bound and the per-harness cap exists only | |
| # to keep the flag from being unset: a cap that fires on these tiers costs | |
| # more than it saves, because the non-zero exit ends the script at the `tee` | |
| # and the harness and cover floors below it are never read. | |
| - name: prove this tier's harnesses | |
| run: ./scripts/kani.sh ${{ matrix.tier }} | |
| mutants: | |
| if: github.event.schedule != '17 5 * * *' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 350 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| shard: [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: nix-${{ runner.os }}- | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: mutants-${{ runner.os }}-${{ hashFiles('Cargo.lock') }} | |
| restore-keys: mutants-${{ runner.os }}- | |
| # 12 shards, measured rather than estimated. `--shard` takes a CONTIGUOUS | |
| # slice, not every n-th mutant, so a shard's crate mix — and with it the | |
| # build output that accumulates on the runner's ~14 GB — is decided by where | |
| # its boundaries fall. At 8 the 6th slice was `rsk-piv` … `rsk-rsa-asm` … | |
| # `rsk-slip39`, 1802 mutants over 6 crates, and it took the runner down with | |
| # it twice (SIGTERM at 85 % of the shard, the same 358 survivors both times, | |
| # the tool healthy to the last line). At 12 it is ~1201 over 5, a third less | |
| # accumulated build per job. A reduction in pressure, NOT a proven fix: what | |
| # killed the host was never measurable from the log. | |
| # The denominator is `strategy.job-total` and not a second hand-kept 12 — | |
| # two numbers that must agree is how the shard space silently loses a slice. | |
| - name: mutants — would a test notice if this line changed? | |
| run: nix develop -c ./scripts/mutants-all.sh | |
| env: | |
| MUTANTS_SHARD: ${{ matrix.shard }}/${{ strategy.job-total }} | |
| MUTANTS_JOBS: "3" | |
| HOST_TARGET: x86_64-unknown-linux-gnu | |
| comutants: | |
| if: github.event.schedule != '17 5 * * *' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 120 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: nix-${{ runner.os }}- | |
| - uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: comutants-${{ runner.os }}-${{ hashFiles('Cargo.lock', 'formal/comutants.toml') }} | |
| restore-keys: comutants-${{ runner.os }}- | |
| - name: co-refutation — inject every semantic defect into production Rust | |
| run: | | |
| set -o pipefail | |
| nix develop -c python scripts/comutate.py run | tee "$RUNNER_TEMP/comutants.log" | |
| - name: publish the fidelity matrix | |
| if: always() | |
| run: | | |
| { | |
| echo "### Co-refutation — model defects at code level" | |
| echo '```' | |
| cat "$RUNNER_TEMP/comutants.log" | |
| echo '```' | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| # The TLA+ model checker. It ran in no workflow at all until now: `floors.txt`, | |
| # the vacuity check and the 44-mutant matrix were ratchets whose only puller was | |
| # whoever remembered `./formal/run-tlc.sh`, on the one machine that had a jar at | |
| # a hardcoded store path. The tool is pinned in the dev shell now, which is what | |
| # makes this row possible. | |
| # | |
| # `safety`, not `all`: the liveness family needs the 12g heap `floors.txt` gives | |
| # it, and 11.1 GB is where the kani `heavy` runner already died twice. The tier | |
| # membership lives in formal/run-tlc.sh and nowhere else, so this row cannot | |
| # drift from it — see that file for what `liveness` costs and where to run it. | |
| # | |
| # The row fails on RED (a mutant that should fire and did not, or an invariant | |
| # that broke), on FLOOR (a GREEN that got smaller than its recorded floor) and | |
| # on VACUOUS (a spec nothing enabled). `scripts/test_run_tlc.py`, collected by | |
| # the merge gate, keeps the roadmap's four corruptions: broken jar, a Solo | |
| # invariant that misses its mutant, one-state VACUOUS, and a muted Mut switch. | |
| # Direct RED and FLOOR cases make all three job verdict boundaries explicit. | |
| formal: | |
| if: github.event.schedule != '17 5 * * *' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 120 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22 | |
| - uses: nix-community/cache-nix-action@7df957e333c1e5da7721f60227dbba6d06080569 # v7.0.2 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }} | |
| restore-prefixes-first-match: nix-${{ runner.os }}- | |
| # Shipped.cfg alone is 61 M distinct states at 1137 s on the author's | |
| # machine; the rest of the matrix is seconds apiece. Two workers is what | |
| # run-tlc.sh caps at, and the runner has four cores. | |
| # `set -o pipefail` is load-bearing: a `run:` block is `bash -e` WITHOUT it, | |
| # so the pipe below would report tee's exit code and a RED matrix would pass | |
| # as green — the exact hole this row exists to close, in the row itself. | |
| - name: formal — TLC over the model, its mutants and their floors | |
| run: | | |
| set -o pipefail | |
| nix develop -c ./formal/run-tlc.sh safety | tee "$RUNNER_TEMP/formal.log" | |
| - name: publish the matrix | |
| if: always() | |
| run: | | |
| { | |
| echo "### TLA+ — safety tier" | |
| echo '```' | |
| cat "$RUNNER_TEMP/formal.log" | |
| echo '```' | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| if: failure() | |
| with: | |
| name: formal-logs-${{ github.run_id }} | |
| path: formal/out/ | |
| if-no-files-found: ignore |