chore(planning): record TAS-composition soundness NO-GO + simulator-floor gate (#141) #734

Workflow file for this run

	name: CI

	# Cancel superseded PR runs; never cancel runs on main / tags / scheduled
	# events. See docs/ci-concurrency.md (or the org-wide CI concurrency brief)
	# for rationale.
	concurrency:
	group: ${{ github.workflow }}-${{ github.head_ref \|\| github.ref }}
	cancel-in-progress: ${{ github.event_name == 'pull_request' }}

	on:
	push:
	branches: [main]
	pull_request:
	branches: [main]

	env:
	CARGO_TERM_COLOR: always
	RUSTFLAGS: "-D warnings"

	jobs:
	# ── Fast checks ───────────────────────────────────────────────────────
	fmt:
	name: Format
	runs-on: [self-hosted, linux, x64, light]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	with:
	components: rustfmt
	- run: cargo fmt --all -- --check

	clippy:
	name: Clippy
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	with:
	components: clippy
	- uses: Swatinem/rust-cache@v2
	- run: cargo clippy --workspace --all-targets -- -D warnings

	# ── Tests ─────────────────────────────────────────────────────────────
	test:
	name: Test
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	- name: Install cargo-nextest
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-nextest
	- name: Run tests (JUnit XML output)
	run: cargo nextest run --workspace --profile ci
	- name: Upload test results
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: test-results
	path: target/nextest/ci/junit.xml
	if-no-files-found: ignore

	# ── Bench compile smoke (fast regression gate) ──────────────────────
	bench-smoke:
	name: Bench compile smoke
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	- name: Verify benches compile
	# --no-run builds the bench binaries without executing them. This
	# catches API drift in criterion harnesses on every PR with only
	# the cost of a `cargo check`-like compile.
	run: cargo bench --workspace --no-run

	# ── Security audits ──────────────────────────────────────────────────
	audit:
	name: Security Audit (RustSec)
	# Stays on ubuntu-latest temporarily: smithy ships cargo-audit
	# v0.21.2 whose bundled rustsec parser still rejects RUSTSEC-2026-0037
	# ("unsupported CVSS version: 4.0"). v0.22.1 fixes it but the
	# `cargo install --locked cargo-audit` build trips over our
	# sccache-on-cc setup (aws-lc-sys C compile fails through sccache).
	# Follow-up: drop sccache from ralf's profile before bumping the
	# toolchains-role version, then move this back to [self-hosted, light].
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- uses: rustsec/audit-check@v2
	with:
	token: ${{ secrets.GITHUB_TOKEN }}

	deny:
	name: Cargo Deny
	# Smithy has cargo-deny installed (toolchains role, v0.16.4).
	# We avoid EmbarkStudios/cargo-deny-action@v2 because it launches
	# a rootless container, which fails on our hardened systemd unit:
	# newuidmap is setuid but NoNewPrivileges=true blocks the escalation
	# (newuidmap: write to uid_map failed: Operation not permitted).
	runs-on: [self-hosted, linux, x64, light]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	- run: cargo deny --version
	# Skip the `advisories` check because both cargo-deny and
	# cargo-audit share the same rustsec parser, which currently
	# rejects RUSTSEC-2026-0037 ("unsupported CVSS version: 4.0").
	# bans / licenses / sources still gate. Re-add `advisories`
	# once smithy ships an upgraded rustsec; the audit job (still
	# on ubuntu-latest) covers vulnerability matching meanwhile.
	- run: cargo deny check bans licenses sources

	# ── Code coverage ────────────────────────────────────────────────────
	coverage:
	name: Code Coverage
	needs: [test]
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	with:
	components: llvm-tools-preview
	- uses: Swatinem/rust-cache@v2
	- name: Install cargo-llvm-cov
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-llvm-cov
	- name: Generate coverage (LCOV + HTML)
	run: \|
	cargo llvm-cov --workspace --lcov --output-path lcov.info
	cargo llvm-cov --workspace --html --output-dir coverage-html
	- name: Upload LCOV to Codecov
	if: env.CODECOV_TOKEN != ''
	uses: codecov/codecov-action@v4
	with:
	files: lcov.info
	fail_ci_if_error: false
	env:
	CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
	- name: Upload HTML coverage report
	uses: actions/upload-artifact@v4
	with:
	name: coverage-html
	path: coverage-html/

	# ── Miri (undefined behavior, pointer provenance) ───────────────────
	miri:
	name: Miri
	# lean-mem class — Miri allocates aggressively and benefits from the 24G
	# MemoryHigh ceiling on smithy lean-mem runners over the 12G rust-cpu cap.
	runs-on: [self-hosted, linux, x64, lean-mem]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	with:
	components: miri
	- uses: Swatinem/rust-cache@v2
	- name: Run Miri (instance model tests)
	# Filter to instance:: tests to avoid known rowan UB (rust-analyzer/rowan issue 192).
	# rowan's custom Arc implementation has a retag issue in HeaderSlice that
	# triggers Miri's borrow stack check. This is upstream, not our code.
	# Once rowan ships a fix, expand to full --lib.
	run: "cargo miri test -p spar-hir-def --lib -- instance::"
	env:
	MIRIFLAGS: "-Zmiri-strict-provenance -Zmiri-disable-isolation"

	# ── Property-based testing (extended) ───────────────────────────────
	# Runs on every PR + main push (the workflow's top-level on:) — per
	# issue #135 acceptance: proptest gating must be PR-blocking, not just
	# a nightly. PROPTEST_CASES=1000 is 10× the default (100) so subtle
	# parser/scheduler invariants get exercised on every change.
	proptest:
	name: Proptest (extended)
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	- name: Run proptest with 10x cases
	run: cargo test --workspace
	env:
	PROPTEST_CASES: "1000"

	# ── Mutation testing ────────────────────────────────────────────────
	mutants:
	name: Mutation Testing
	needs: [test]
	# lean-mem — many parallel cargo invocations, RAM pressure under -j 4.
	# The full-workspace exhaustive run lives in mutants-weekly.yml; this
	# gating job stays narrow (spar-analysis) with a survivor ratchet.
	runs-on: [self-hosted, linux, x64, lean-mem]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	- name: Install cargo-mutants
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-mutants
	- name: Run cargo-mutants on spar-analysis
	run: cargo mutants -p spar-analysis --timeout 120 --jobs 4 --output mutants-out -- --lib \|\| true
	- name: Check surviving mutants
	run: \|
	MISSED=$(grep -c '^MISSED' mutants-out/caught.txt 2>/dev/null \|\| echo 0)
	if [ -f mutants-out/missed.txt ]; then
	MISSED=$(wc -l < mutants-out/missed.txt \| tr -d ' ')
	fi
	echo "Surviving mutants: $MISSED"
	# Ratchet gate: fail if more mutants survive than the threshold.
	# Lower this number as tests improve. Target: 0.
	MAX_MISSED=142
	if [ "$MISSED" -gt "$MAX_MISSED" ]; then
	echo "::error::$MISSED mutant(s) survived (threshold: $MAX_MISSED) — add tests to kill them"
	cat mutants-out/missed.txt 2>/dev/null \| head -30
	exit 1
	fi
	echo "Mutant survivors ($MISSED) within threshold ($MAX_MISSED). Target: 0."
	- name: Upload mutants report
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: mutants-report
	path: mutants-out/

	# ── Fuzz smoke (60s per target on PRs) ──────────────────────────────
	fuzz-smoke:
	name: Fuzz smoke (60s/target)
	runs-on: [self-hosted, linux, x64, rust-cpu]
	# Only run on PRs — pushes to main hit the nightly workflow instead.
	if: github.event_name == 'pull_request'
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	with:
	workspaces: fuzz
	- name: Install cargo-fuzz
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-fuzz
	# cargo-fuzz defaults to x86_64-unknown-linux-musl, whose statically-
	# linked libc is incompatible with ASan ("sanitizer is incompatible
	# with statically linked libc"). Pin to the GNU triple explicitly.
	- name: fuzz_aadl_parse (60s)
	run: cargo +nightly fuzz run --target x86_64-unknown-linux-gnu fuzz_aadl_parse -- -max_total_time=60 -timeout=10
	- name: fuzz_scheduler_solver (60s)
	run: cargo +nightly fuzz run --target x86_64-unknown-linux-gnu fuzz_scheduler_solver -- -max_total_time=60 -timeout=5
	- name: fuzz_codegen_roundtrip (60s)
	run: cargo +nightly fuzz run --target x86_64-unknown-linux-gnu fuzz_codegen_roundtrip -- -max_total_time=60 -timeout=10

	# ── Supply chain verification ───────────────────────────────────────
	supply-chain:
	name: Supply Chain (cargo-vet)
	runs-on: [self-hosted, linux, x64, light]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	- name: Install cargo-vet
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-vet
	- name: Verify supply chain
	run: cargo vet --locked

	# ── Rivet artifact validation ───────────────────────────────────────
	# Per AGENTS.md: every artifact change must pass `rivet validate`.
	# Mirrors the local pre-commit check so CI catches schema regressions
	# in artifacts/, safety/stpa/, and rivet.yaml.
	rivet-validate:
	name: Rivet validate (artifacts)
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	- uses: Swatinem/rust-cache@v2
	- name: Install rivet CLI
	# The binary `rivet` ships in the `rivet-cli` package (renamed
	# in the 0.4.x rework). v0.1.0 used a single `rivet` package
	# and treated unknown fields as errors, which fails on legitimate
	# schema-extension fields used by Track A/B/D/E artifacts.
	run: cargo install --locked --git https://github.com/pulseengine/rivet --tag v0.4.3 rivet-cli
	- name: rivet validate
	run: rivet validate --format text

	# ── Bazel test sweep ───────────────────────────────────────────────
	# Issue #135 acceptance: `bazel test //...` to pick up Rust + Lean
	# targets via tools/bazel/rules_lean and rules_wasm_component.
	#
	# NOTE: Currently informational (continue-on-error: true) until a
	# MODULE.bazel / BUILD.bazel surface lands at the workspace root.
	# The job is wired up now so the moment those files appear, CI gates
	# them automatically — no follow-up workflow edit needed.
	#
	# Time budget: cold cache ≤30 min, warm ≤5 min (per #135).
	bazel-test:
	name: Bazel test (//...)
	# Stays on ubuntu-latest until Bazel is installed on the smithy host.
	# Tracked as a follow-up: smithy/group_vars/all.yml could add a
	# bazel apt-installable. Until then, hosted handles this.
	runs-on: ubuntu-latest
	continue-on-error: true
	timeout-minutes: 35
	steps:
	- uses: actions/checkout@v4
	- uses: bazelbuild/setup-bazelisk@v3
	- name: Cache Bazel
	uses: actions/cache@v4
	with:
	path: \|
	~/.cache/bazel
	~/.cache/bazelisk
	# Key on whichever workspace marker exists. Falls back to a
	# stable key when none are present so the cache still warms
	# across runs and lights up automatically once a workspace
	# marker lands.
	key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel.lock', 'MODULE.bazel', 'WORKSPACE', 'WORKSPACE.bazel', 'tools/bazel//BUILD.bazel', 'tools/bazel//*.bzl') }}
	restore-keys: \|
	bazel-${{ runner.os }}-
	- name: bazel test //...
	run: \|
	set -euo pipefail
	if [ ! -f MODULE.bazel ] && [ ! -f WORKSPACE ] && [ ! -f WORKSPACE.bazel ]; then
	echo "::warning title=Bazel sweep::No MODULE.bazel/WORKSPACE at repo root; skipping bazel test //... (informational)."
	echo "tools/bazel/rules_lean exists but is consumed by generated BUILD files."
	echo "Add a root MODULE.bazel to enable this gate."
	exit 0
	fi
	bazel test //... --test_output=errors

	# ── Bounded model checking (Kani) ───────────────────────────────────
	# First-pass Kani harnesses for spar-solver + spar-codegen invariants.
	# Each harness mirrors a theorem in proofs/Proofs/Scheduling/ (RMBound,
	# EDF, RTA) and verifies the same invariant over bounded integer
	# arithmetic that Kani's CBMC backend can enumerate exactly.
	#
	# continue-on-error: true — these harnesses are first-pass; unwind
	# bounds may need tuning as we evolve them. The eventual hard-gate plan
	# is:
	# 1. Land harnesses + observe stable runtime over 2-3 weeks of CI.
	# 2. Once all three solver harnesses + the codegen harness complete
	# in <5 min wall time with no unwind-assertion failures, flip
	# continue-on-error to false and add to the required-checks list.
	# 3. At that point, extend MAX_TASKS from 4 to 8 and re-tune unwinds.
	kani:
	name: Kani Bounded Model Checking
	# Stays on ubuntu-latest because kani-verifier bundles CBMC (~100 MB)
	# which we don't pre-install on smithy. Once smithy ships Kani as a
	# toolchain, switch to rust-cpu (the verification is RAM-modest but
	# CPU-bound; CBMC is single-threaded per harness).
	runs-on: ubuntu-latest
	continue-on-error: true
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	- uses: Swatinem/rust-cache@v2
	- name: Install Kani
	# Pinned: 0.63.0's bundled nightly-2025-06-03 cannot compile
	# smol_str 0.3.6 ([0; _] / generic_arg_infer); 0.67.0 ships
	# nightly-2025-11-21 which can. Validated locally (#252).
	run: \|
	cargo install --locked kani-verifier --version 0.67.0
	cargo kani setup
	- name: Run Kani on spar-solver
	run: cargo kani --tests -p spar-solver
	- name: Run Kani on spar-codegen (schedule harness)
	run: cargo kani --tests -p spar-codegen --harness kani_emit_preserves_schedule
	- name: Run Kani on spar-codegen (AADL contract harnesses)
	# prove_thread_period_preserved_d1..d10 — period round-trip, stratified
	# by decimal digit count; union of bands = (0, 10^9] ns exactly (the
	# single full-domain harness OOM'd CBMC / 6h-timed-out CI, #252)
	# prove_port_direction_preserved — WIT direction token mapping
	# prove_access_right_preserved — Read_Only never widens to &mut
	# kissat: ~2x faster than the default SAT backend on these
	# bitvector-heavy instances (measured: d9 378s kissat / never
	# finished with cadical+u64, #252). `_d` prefix-matches all ten
	# period bands.
	run: >-
	cargo kani --tests -p spar-codegen --solver kissat
	--harness prove_thread_period_preserved_d
	--harness prove_port_direction_preserved
	--harness prove_access_right_preserved

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

chore(planning): record TAS-composition soundness NO-GO + simulator-floor gate (#141) #734

Workflow file

chore(planning): record TAS-composition soundness NO-GO + simulator-floor gate (#141) #734

Uh oh!

Workflow file for this run