Nightly (heavy gates) #83

Workflow file for this run

.github/workflows/nightly.yml at 9fd2025

	name: Nightly (heavy gates)

	# Heavy verification gates that are too slow for the per-PR `ci.yml` but must
	# still run on a regular cadence (SOTA 2026-06 §3/§6; docs/STATUS.md §B):
	#
	# * kani — bounded model-checking of the parsers / cap-monotonicity
	# (downloads a checker via `cargo kani setup`, minutes).
	# * verify-repro — two full release cross-builds + byte-diff of the secure +
	# nonsecure ELFs (the canonical reproducibility gate).
	#
	# Runs nightly + on manual dispatch. The fast invariant/host/secure/contracts
	# gates stay in ci.yml on every push/PR.
	#
	# * checkct — cargo-checkct (binsec relational-CT proof of the 5 secure
	# drivers + the by-design-INSECURE shuffle control). The
	# binsec OCaml backend is the heavy part (opam, minutes).
	# * ui-golden-render — the render-only golden gate (the "dedicated
	# short-capture" the note below used to call for): renders the
	# curated screen corpus via the production renderers + diffs
	# [UI-FP] fingerprints, no keygen/sign (seconds, not minutes).
	# * proof-mutation — proof-side cargo-mutants (anti-vacuity V4): delete each
	# load-bearing axiom / weaken a key lemma and assert the
	# rebuild reacts as AXIOM_STATUS.json claims. 8 full
	# `lake build`s — too slow for per-PR; the fast sibling
	# verify-ledger-consistency runs in lean-fv.yml.
	#
	# Still NOT here: the FULL `make ui-golden` (all 24 e2e scenarios over the QEMU
	# semihosting backend, 10+ min — the C10 signs over software SHA-256 dominate).
	# `ui-golden-render` (above) is the CI-viable replacement; the full e2e variant
	# stays a LOCAL/manual gate.

	on:
	schedule:
	- cron: '27 4 * * *' # 04:27 UTC daily
	workflow_dispatch:

	permissions:
	contents: read

	concurrency:
	group: nightly-${{ github.ref }}
	cancel-in-progress: true

	jobs:
	kani:
	name: Kani (bounded model-checking)
	runs-on: ubuntu-latest
	# Restored after being lost collaterally: it was originally added in the
	# same commit as a kissat experiment, so reverting the experiment threw away
	# this unrelated hygiene fix too. Bundling an experiment with a fix is how
	# you lose the fix.
	#
	# 240 was a guess and the job outran it; this is now sized from the observed
	# run rather than invented. Split from the mutation gate below, so the two
	# no longer share one budget.
	timeout-minutes: 300
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	- name: Install Kani
	run: \|
	cargo install --locked --version 0.67.0 kani-verifier
	cargo kani setup
	# INSTRUMENTATION, added 2026-07-31 — do not remove until the Kani OOM is
	# settled. The job has been dying with "The runner has received a
	# shutdown signal", which is what GitHub prints when the agent is killed
	# and says NOTHING about why. Two hypotheses are live and they have
	# different fixes:
	# RAM — no_hidden_value peaks at 13.05 GiB and cow_presign_precedence
	# at 11.5 GiB (both measured locally, both VERIFY SUCCESSFULLY).
	# A public-repo runner has 16 GB, so these are close to but under
	# the ceiling.
	# DISK — a public-repo runner has only 14 GB of SSD, and this job
	# installs the whole Kani/CBMC toolchain on top of the preinstalled
	# image before building the workspace.
	# Print both before and after so the next failure names its own cause
	# instead of requiring another round of guessing.
	- name: capacity before (RAM + disk)
	run: \|
	echo "--- memory"; free -m
	echo "--- disk"; df -h /
	- name: make kani
	run: /usr/bin/time -v make kani
	- name: capacity after (RAM + disk, and any OOM kill)
	if: always()
	run: \|
	echo "--- memory"; free -m
	echo "--- disk"; df -h /
	echo "--- kernel OOM evidence (empty means it was NOT an OOM kill)"
	sudo dmesg 2>/dev/null \| grep -iE "out of memory\|oom-kill\|killed process" \|\| echo "none"

	kani-mutation:
	# SPLIT OUT of the `kani` job 2026-08-01, for the same reason
	# verify-extracted-heavy was split off the 16 GB runner: two independent
	# gates sharing one job share one failure. When the harness suite OOM-killed
	# the runner, this gate produced no evidence either — not because it was
	# broken, but because it was standing behind something that died.
	#
	# Also 43 mutations x (recompile a crate + run one harness) is a multi-hour
	# workload on its own. Running the two serially in one job is what pushed
	# the combined job past four hours; in parallel each gets a full budget and
	# its own timing, so the next timeout value can be set from evidence instead
	# of guessed.
	name: Kani mutation (anti-vacuity — break a decoder, expect a harness to redden)
	runs-on: ubuntu-latest
	timeout-minutes: 300
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	- name: Install Kani
	run: \|
	cargo install --locked --version 0.67.0 kani-verifier
	cargo kani setup
	# Kani-side mirror of the Lean verify-proof-mutation gate: each mutation
	# recompiles a crate + runs one harness (~1-4 min), all reverted. See
	# scripts/kani_mutations.json + docs/verification/fv-adversarial-review-playbook.md.
	- name: make verify-kani-mutation
	run: /usr/bin/time -v make verify-kani-mutation

	verify-repro:
	name: Reproducible-build byte-diff
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	targets: thumbv8m.main-none-eabi
	- name: Install arm-none-eabi toolchain (arm-none-eabi-ld)
	run: sudo apt-get update && sudo apt-get install -y gcc-arm-none-eabi
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	- name: make verify-repro
	run: make verify-repro

	checkct:
	name: cargo-checkct (binsec relational CT proof)
	runs-on: ubuntu-latest
	# Manual-dispatch only (not the nightly schedule): it can't go green yet
	# (see RESIDUAL below), so running it every night would just burn CI minutes
	# on a yellow job. Run it with `gh workflow run nightly.yml` while working
	# the from-source binsec build.
	if: github.event_name == 'workflow_dispatch'
	# NON-BLOCKING (WIP). Root cause FULLY DIAGNOSED (2026-06-29, reproduced in a
	# throwaway opam switch — see tools/sca/DONJON-RUST-TOOLING.md §1 "CI recipe"):
	# the opam-released `binsec` package builds with `dune build -p binsec`, which
	# builds the optional ARM decoder (binsec.isa.armv7, a dune `(select)` on
	# unisim_archisec) XOR the checkct plugin (gated on a solver) — never BOTH at
	# once, so it always rejects either `-arm-supported-modes` or `-checkct`. The
	# working LOCAL binsec is built FROM SOURCE (`dune build @install`, no `-p`)
	# with unisim_archisec + a solver (z3/bitwuzla) present, which compiles both.
	# The remaining CI work is a from-source binsec in a CLEAN switch (no
	# opam-`binsec` ever installed — a mixed install dynlinks a plugin .cmxs built
	# against a different binsec base → `undefined symbol camlBinsec_base__Logger`).
	# PROVEN in CI: opam/ocaml + binsec/unisim install + cargo-checkct build +
	# binsec invocation. Until the from-source job lands, the validated gate is
	# LOCAL `make checkct`; this documents the exact recipe without a red nightly.
	continue-on-error: true
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	targets: thumbv8m.main-none-eabi
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	# binsec (+ unisim_archisec, bitwuzla) is the relational-CT backend —
	# OCaml, not on crates.io, installed via opam. This is the heavy step
	# (minutes); setup-ocaml caches the opam root across runs.
	- uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1
	with:
	ocaml-compiler: "4.14.2"
	# Pin to the exact locally-validated backend set (the DONJON doc's 0.10.0
	# is stale; the working pair is binsec 0.11.1 + unisim_archisec 0.0.14).
	# ORDER MATTERS: binsec compiles its ARM decoder (-arm-supported-modes,
	# needed for thumbv8m) only when unisim_archisec is present at binsec
	# BUILD time. Install unisim first, then (re)build binsec against it.
	- name: opam install binsec backend (unisim first → binsec gets ARM)
	run: \|
	opam install -y unisim_archisec.0.0.14
	opam reinstall -y binsec.0.11.1 2>/dev/null \|\| opam install -y binsec.0.11.1
	# The checkct driver crates reference `checkct_macros` at a path relative
	# to a SIBLING `cargo-checkct/` (../../../../../cargo-checkct/...), so the
	# tool must be cloned NEXT TO the repo checkout, not under $HOME — and
	# pinned to the commit whose binsec-script template matches binsec 0.11.1.
	- name: build cargo-checkct (Ledger-Donjon, pinned)
	run: \|
	dest="$(dirname "$GITHUB_WORKSPACE")/cargo-checkct"
	git clone https://github.com/Ledger-Donjon/cargo-checkct "$dest"
	cd "$dest" && git checkout f7bc61f5ad08dedece61ec199911f6ecd3272eeb && cargo build --release
	# `cargo-checkct run` ALWAYS exits non-zero: the by-design-INSECURE
	# fisher_yates shuffle (`driver`) is the CONTROL that proves the tool
	# detects leaks. So gate on the per-driver RESULTS, not the exit code —
	# the 5 real drivers (kdf/fors/th/saes/ct_eq) must be secure AND the shuffle
	# control must still report insecure (5 secure + 1 insecure).
	- name: cargo-checkct relational CT proof (5 secure + shuffle control)
	run: \|
	eval "$(opam env)"
	# Declared and assigned separately: `export X="$(...)"` masks the
	# command's exit status behind export's own (SC2155).
	checkct_bin="$(dirname "$GITHUB_WORKSPACE")/cargo-checkct/target/release"
	export PATH="$checkct_bin:$PATH"
	out=$(cargo-checkct run --dir tools/sca --timeout 300 2>&1 \|\| true)
	echo "$out"
	secure=$(printf '%s\n' "$out" \| grep -c 'Program status is : secure')
	insecure=$(printf '%s\n' "$out" \| grep -c 'Program status is : insecure')
	echo "==> secure=$secure (expect 5: kdf/fors/th/saes/ct_eq) insecure=$insecure (expect 1: shuffle control)"
	if [ "$secure" -eq 5 ] && [ "$insecure" -eq 1 ]; then
	echo "==> checkct: PASS"
	else
	echo "==> checkct: FAIL — a secure driver leaked or the shuffle control stopped firing"; exit 1
	fi

	firmware-check:
	name: Firmware target compile-check (stm32u585, both worlds)
	runs-on: ubuntu-latest
	# No CI job compiled a real stm32u585 image before this (2026-07-02): every
	# cross-build used the QEMU feature set (mock-se/ui-semihosting), and the
	# prod-config gate is cargo-tree-only — so a compile break anywhere in the
	# large `#[cfg(feature = "stm32u585")]` surface (SE drivers, HW MMIO, CMSE
	# veneers, LCD) shipped silently until someone built at the bench. `cargo
	# check` (not a full build) is fast and catches exactly that. The pinned
	# nightly is auto-selected via rust-toolchain.toml (CMSE
	# `C-cmse-nonsecure-entry` needs it) — the action just provides the target.
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	targets: thumbv8m.main-none-eabi
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	- name: cargo check — secure world (dual-SE hardened bench set)
	run: \|
	cargo check --locked -p sphincs-tz-secure --target thumbv8m.main-none-eabi \
	--no-default-features \
	--features dual-se,optiga-hw-counter,saes-dhuk,ui-lcd,stm32u585,usb,legacy-fw-rollback-unsafe,erc7730-dev-unattested
	- name: cargo check — non-secure world (USB)
	run: \|
	cargo check --locked -p sphincs-tz-nonsecure --target thumbv8m.main-none-eabi \
	--no-default-features --features stm32u585,usb
	# TZP-10 (#481): the prodtest feature set (secure prodtest,dev-testkey,
	# saes-dhuk / nonsecure stm32u585,usb,prodtest) compiled in NO workflow —
	# factory-image bit-rot would surface only at the line. Unlike the cargo
	# checks above this is a full release cross-build, so it links via
	# arm-none-eabi-ld and needs the ARM bare-metal toolchain.
	- name: Install arm-none-eabi toolchain (arm-none-eabi-ld)
	run: sudo apt-get update && sudo apt-get install -y gcc-arm-none-eabi
	- name: make build-hw-prodtest (factory prodtest image compiles)
	run: make build-hw-prodtest
	# Host-side factory fixture runner unit tests (unittest, offline — same
	# invocation form as the erc8176-coverage-test Makefile target).
	- name: factory prodtest runner unit tests
	run: PYTHONDONTWRITEBYTECODE=1 python3 -m unittest tools/test_factory_prodtest_runner.py

	ui-golden-render:
	name: UI golden (render-only)
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
	with:
	toolchain: stable
	targets: thumbv8m.main-none-eabi
	- name: Install arm-none-eabi + qemu
	run: sudo apt-get update && sudo apt-get install -y gcc-arm-none-eabi qemu-system-arm
	- uses: Swatinem/rust-cache@e18b497796c12c097a38f9edb9d0641fb99eee32 # v2
	- name: make ui-golden-render
	run: make ui-golden-render

	proof-mutation:
	name: Proof-mutation (anti-vacuity V4 — dead axiom/lemma)
	runs-on: ubuntu-latest
	# Too slow for per-PR (default tier = 8 mutations, each a full
	# `lake build SphincsCVerify`); the fast sibling verify-ledger-consistency
	# runs per-PR in lean-fv.yml. See docs/verification/fv-adversarial-review-playbook.md §B.
	timeout-minutes: 90
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	- name: install elan (toolchain pinned by lean-toolchain)
	run: \|
	# Pinned + verified, not `curl \| sh` from a moving branch. `master`
	# is mutable: whoever controls that ref controls the toolchain
	# installer on every FV runner, which is the trust root the
	# verification Makefile builds on. Pin the commit, check the bytes,
	# and only then execute. (#562)
	set -euo pipefail
	ELAN_REF=464c9d28395000a2a0128e07081e4956d50eced2
	ELAN_SHA256=a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53
	curl --proto '=https' --tlsv1.2 -fsSL \
	"https://raw.githubusercontent.com/leanprover/elan/${ELAN_REF}/elan-init.sh" \
	-o elan-init.sh
	echo "${ELAN_SHA256} elan-init.sh" \| sha256sum -c -
	sh elan-init.sh -y --default-toolchain none
	rm -f elan-init.sh
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
	- name: restore .lake build (warm baseline from the lean-fv gate; RESTORE-ONLY)
	# restore-only: a mutation run leaves the last mutant's stale olean in
	# .lake, so this job must NOT write back to the shared lean-fv cache key.
	uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
	with:
	path: contracts/verification/lean/.lake/build
	key: lean-fv-lake-${{ hashFiles('contracts/verification/lean/lean-toolchain', 'contracts/verification/lean/lakefile.toml') }}-${{ hashFiles('contracts/verification/lean/SphincsCVerify/*/.lean') }}
	restore-keys: \|
	lean-fv-lake-${{ hashFiles('contracts/verification/lean/lean-toolchain', 'contracts/verification/lean/lakefile.toml') }}-
	lean-fv-lake-
	- name: make verify-proof-mutation (default tier; reverts every mutation)
	run: make -C contracts/verification verify-proof-mutation

	protocol-models:
	name: Protocol models (ProVerif + Tamarin symbolic gate)
	runs-on: ubuntu-latest
	# The 8 design-layer symbolic models (dual-SE seed-split, three-way
	# PIN-lockstep, SCP03 + OPTIGA-shield tunnels, FW-update authenticity).
	# `make proverif`/`tamarin` exit 0 whether a query is true or false and the
	# models carry designed `is false` residuals, so this runs the assert-the-
	# verdicts gate (scripts/check_protocol_models.py), NOT a bare run.
	# CryptoVerif is EXPLICITLY excluded here (PROTOCOL_MODELS=proverif,tamarin):
	# it installs cleanly only via nix (its `-lib` path is nix-layout-specific)
	# and its one property is already gated by tamarin/seed_split_xor.spthy.
	timeout-minutes: 45
	steps:
	- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
	with:
	persist-credentials: false
	# ProVerif is OCaml, installed via opam. PINNED to 2.05 — the exact
	# version the scripts/check_protocol_models.py verdict baseline was
	# produced with; an unpinned bump could shift the counts spuriously.
	# setup-ocaml caches opam.
	- uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3.6.1
	with:
	ocaml-compiler: "4.14.2"
	# GTK2 headers. We do NOT want ProVerif's GUI, but `lablgtk` is a HARD
	# dependency of the proverif opam package (not a depopt), and lablgtk's
	# `conf-gtk2` runs `pkg-config --exists gtk+-2.0` in its BUILD step.
	#
	# This step replaces `--assume-depexts`, which was here before and could
	# never have worked: that flag tells opam to assume system deps are
	# already installed and skip installing them — it does not stop
	# conf-gtk2 from probing pkg-config and failing. This job has been red
	# since it was added on 2026-07-01 with:
	# ERROR while compiling conf-gtk2.1
	# command /usr/bin/pkg-config --exists gtk+-2.0
	# exit-code 1
	- name: install GTK2 headers (lablgtk is a hard dep of proverif)
	run: sudo apt-get update && sudo apt-get install -y libgtk2.0-dev
	- name: opam install proverif 2.05
	run: opam install -y proverif.2.05
	# Tamarin + its Maude backend: upstream prebuilt linux64 binaries, PINNED
	# to the exact versions the baseline used (1.12.0 / 3.5.1). No sudo/GHC.
	- name: install tamarin-prover 1.12.0 + maude 3.5.1 (prebuilt binaries)
	run: \|
	mkdir -p "$HOME/.local/bin"
	curl -fsSL https://github.com/tamarin-prover/tamarin-prover/releases/download/1.12.0/tamarin-prover-1.12.0-linux64-ubuntu.tar.gz \| tar xz
	install -m755 tamarin-prover "$HOME/.local/bin/tamarin-prover"
	curl -fsSL -o maude.zip https://github.com/maude-lang/Maude/releases/download/Maude3.5.1/Maude-3.5.1-linux-x86_64.zip
	unzip -oq maude.zip
	m="$(find . -name maude -type f \| head -1)"
	install -m755 "$m" "$HOME/.local/bin/maude"
	# Maude loads its *.maude prelude from alongside the binary (or MAUDE_LIB).
	find "$(dirname "$m")" -maxdepth 1 -name '*.maude' -exec cp {} "$HOME/.local/bin/" \;
	echo "$HOME/.local/bin" >> "$GITHUB_PATH"
	echo "MAUDE_LIB=$HOME/.local/bin" >> "$GITHUB_ENV"
	- name: verify-protocol-models (proverif + tamarin — the 8 symbolic models)
	run: \|
	eval "$(opam env)"
	make verify-protocol-models PROTOCOL_MODELS=proverif,tamarin

Navigation Menu

Nightly (heavy gates) #83

Workflow file

Nightly (heavy gates) #83

Uh oh!

Workflow file for this run