Stage-2 REQ-4: classifier ops half (Rust) + differential battery (#326) #227

Workflow file for this run

	name: ci

	on:
	push:
	branches: [main]
	pull_request:

	# Cancel a PR's superseded in-flight run when a new commit is pushed (the
	# kickoff-agent loop waits on this CI, so stale runs are pure latency). Main
	# pushes are NOT cancelled: those runs are the verification record of record.
	concurrency:
	group: ci-${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: ${{ github.event_name == 'pull_request' }}

	# Two jobs, run in parallel (REQ-5 — the full gauntlet still runs; a non-zero
	# exit in any step fails CI, R-DEFER-6):
	#
	# checks — the compile-light gates: fmt, clippy, the python doc-drift gate,
	# the skill-budget gate, and doctests. Run once.
	# test — the Verus/Z3-backed conformance suite, which dominates wall-clock
	# (~100 of the workspace's integration-test binaries invoke the real
	# solver). Profiling showed this is test EXECUTION time, not compile
	# time, so it is sharded across N runners with cargo-nextest's
	# partitioning; wall-clock drops ~linearly with the shard count.
	#
	# Both jobs install the pinned toolchain (rust-toolchain.toml channel, 1.95.0)
	# and restore the shared Rust build cache + the pinned Verus distribution; on a
	# warm cache the per-job compile is seconds. Verus is the L3 verification gate
	# (it bundles the matching rust toolchain + z3); tests resolve it via VERUS_BIN.
	# The skill-budget gate fails CI if the generated THERMITE.skill.md exceeds its
	# 6,000-token budget (design §2.2 / §10).
	jobs:
	checks:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# Full history: the doc-drift tripwire's commit-set predicate
	# (`git log --full-history <pin>..HEAD`) and pin validation
	# (`merge-base --is-ancestor`) need the pinned commits present; a
	# shallow clone would mis-class every pin as INVALID-PIN.
	fetch-depth: 0

	- name: Install toolchain (pinned to rust-toolchain.toml channel)
	uses: dtolnay/rust-toolchain@1.95.0
	with:
	components: rustfmt, clippy

	# Fail-fast: the cheap, no-compile gates first.
	- name: cargo fmt
	run: cargo fmt --all --check

	- name: doc-drift gate tests (tooling/tests)
	run: python3 -m unittest discover -s tooling/tests
	- name: doc-drift tripwire (design-doc freshness)
	run: python3 tooling/doc-drift.py
	- name: req-status lint (source-comment status consistency)
	run: python3 tooling/req-status.py
	- name: req-registry gate (canonical status inventory)
	run: tooling/reqs check

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	# Distinct cache slot from the test job: this job builds with
	# `--all-targets` for clippy, a different artifact set.
	key: checks

	# Verus is restored here too so doctests that exercise the solver path
	# still run (the old single-job `cargo test --workspace` ran doctests).
	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	- name: cargo clippy
	run: cargo clippy --workspace --all-targets -- -D warnings

	# nextest does not run doctests; run them here so coverage matches the
	# previous `cargo test --workspace`.
	- name: cargo test --doc
	run: cargo test --doc --workspace

	- name: skill budget gate (issue #7, design §2.2 / §10)
	run: cargo run -p thermite-skill -- --check-budget

	test:
	runs-on: ubuntu-latest
	strategy:
	# Surface every shard's failures, not just the first.
	fail-fast: false
	matrix:
	shard: [1, 2, 3, 4]
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# Some conformance tests (audit/doc-drift) read git history.
	fetch-depth: 0

	- name: Install toolchain (pinned to rust-toolchain.toml channel)
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: test

	- name: Install cargo-nextest
	uses: taiki-e/install-action@v2
	with:
	tool: nextest

	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	# Shard the suite across the matrix: nextest assigns each test to one
	# partition deterministically, so the union of shards is the full suite.
	- name: cargo nextest run (shard ${{ matrix.shard }}/4)
	run: cargo nextest run --workspace --partition count:${{ matrix.shard }}/4

	# The Lean spine + axiom probe (trust-audit finding F4: until now `lake build` and the
	# `#print axioms` gate ran only in a local `make audit`, so a commit breaking the Lean
	# build or a relax-spine lemma acquiring a disallowed axiom would go unseen in CI). This
	# job runs the SAME shared probe (scripts/lean-axiom-probe.sh) check [1] runs, so local
	# and CI cannot drift. lean-smt is pinned to a SHA in lean/lakefile.toml, so the build
	# is reproducible. Mathlib oleans are fetched from the cloud cache (`lake exe cache
	# get`); the probe builds only the spine modules it imports, not the cvc5-FFI SmtDemo.
	lean:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# forge's audit/doc-drift conformance tests read git history
	fetch-depth: 0

	- name: Install elan (Lean toolchain manager)
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build (.lake)
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	# Keyed on the dep lockfile + toolchain pin: a lean-smt/Mathlib bump or a
	# toolchain change busts the cache; spine edits reuse it (lake rebuilds only the
	# changed modules).
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch prebuilt Mathlib cache (oleans)
	working-directory: lean
	# Without this the relax island's `import Mathlib.Data.Real.Basic` would compile a
	# large slice of Mathlib from source (hours). The cache makes it olean loads.
	run: lake exe cache get

	- name: Lean spine build + axiom probe (lake build + #print axioms gate)
	run: bash scripts/lean-axiom-probe.sh

	# Audit F4 (#309): the `test` shards above run WITHOUT the Lean spine, so every
	# `lake`-gated live test (the end-to-end L3/L4 forge discharges, the seven-verdict
	# live cases, the merge-class G1 cert) self-skips there and was only verified
	# locally. This job is the one place the spine + lake exist, so it also installs
	# Rust + Verus and runs the forge suite HERE, where those tests actually execute —
	# the `lake_present()` guards take the RUN branch. (Redundant with the shards for
	# the non-spine forge tests; can be filtered/sharded later — #309.)
	- name: Install Rust toolchain (pinned)
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: lean-spine-tests

	- name: Install cargo-nextest
	uses: taiki-e/install-action@v2
	with:
	tool: nextest

	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	- name: Build the spine modules forge's --engine lean discharge imports
	working-directory: lean
	# The axiom probe builds only its own subset; forge's lean export imports
	# `Thermite.Stabilize` / `Exec.Stmt` / `Exec.WhileBody` (NOT the root `Thermite`,
	# which pulls the cvc5-FFI `SmtDemo`). Without these oleans on the search path the
	# `--engine lean` auto-discharge fails with "unknown module prefix 'Thermite'" —
	# which `engine_lean_attaches_smaller_trust_base_live` correctly catches.
	run: lake build Thermite.Stabilize Thermite.Exec.Stmt Thermite.Exec.WhileBody

	- name: forge tests WITH the spine (the lake-gated live tests run here, not skipped)
	# lake is on PATH (elan), the spine modules forge imports are built, Verus is
	# installed: the live `lake_present()`/spine-dependent tests take their RUN branch.
	run: cargo nextest run -p forge

Navigation Menu

Uh oh!

Stage-2 REQ-4: classifier ops half (Rust) + differential battery (#326) #227

Workflow file

Stage-2 REQ-4: classifier ops half (Rust) + differential battery (#326) #227

Uh oh!

Workflow file for this run