open-standards/.github/workflows/standards-build.yml
Transaction Science 0efe3e6569
All checks were successful
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 5s
standards workspaces build + test / joule-ui-rs (joule-ui/joule-ui-rs, joule-ui-rs, linux) (pull_request) Successful in 29s
standards workspaces build + test / sense-rs (sense/sense-rs, sense-rs, linux) (pull_request) Successful in 34s
standards workspaces build + test / proof-rs (proof/conformance/v1/joulespec.toml, proof-conformance, proof/proof-rs, proof-rs, linux, true) (pull_request) Successful in 1m2s
standards workspaces build + test / arl-rs (arl/arl-rs, arl-rs, linux) (pull_request) Successful in 1m11s
standards workspaces build + test / jcp-rs (jcp-conformance, jcp/jcp-rs, -p jcp-energy --features nvml, jcp-rs, linux) (pull_request) Successful in 1m17s
standards workspaces build + test / joulespec-rs (true, joulespec/joulespec-rs, true, joulespec-rs, linux) (pull_request) Successful in 58s
standards workspaces build + test / pool-rs (pool/pool-rs, pool-rs, linux) (pull_request) Successful in 1m29s
standards workspaces build + test / sandbox-rs (sandbox-conformance, sandbox/sandbox-rs, -p sandbox-tee --features amd-kds,intel-pcs, sandbox-rs, linux) (pull_request) Successful in 1m31s
standards workspaces build + test / joulehook-rs (joulehook/joulehook-rs, joulehook-rs, linux) (pull_request) Successful in 1m49s
standards workspaces build + test / smart-byte-rs (smart-byte/smart-byte-rs, smart-byte-rs, linux) (pull_request) Successful in 2m19s
standards workspaces build + test / eoc-rs (eoc/eoc-rs, -p eoc-meter --features cuda, eoc-rs, linux) (pull_request) Successful in 2m22s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 6m3s
standards workspaces build + test / jouledesk-rs (jouledesk/jouledesk-rs, jouledesk-rs, macos) (pull_request) Successful in 1m34s
standards workspaces build + test / joulespec-proofs (joulespec/joulespec-rs, joulespec-proofs, true, macos) (pull_request) Successful in 1m23s
standards workspaces build + test / joulecontract-rs (joulecontract/joulecontract-rs, joulecontract-rs, linux-arm64, true) (pull_request) Successful in 48s
standards workspaces build + test / map-rs (map-conformance, map/map-rs, map-rs, linux-arm64) (pull_request) Successful in 30s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 13m21s
standards workspaces build + test / mesh-rs (mesh/mesh-rs, -p mesh-engine-gguf -p mesh-openai --features mesh-engine-gguf/gguf,mesh-openai/server, mesh-rs, linux-arm64) (pull_request) Successful in 30s
standards workspaces build + test / openpay (openpay, openpay, linux-arm64) (pull_request) Successful in 1m47s
standards workspaces build + test / aac-rs (aac-conformance, aac/aac-rs, aac-rs, linux-arm64) (pull_request) Successful in 34m16s
standards workspaces build + test / jouleclaw-rs (-nodebug, jouleclaw/jouleclaw-rs, -p jouleclaw-energy --features rapl,nvml, jouleclaw-rs, linux-arm64, -C target-feature=+fp16) (pull_request) Successful in 43m54s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 59m18s
standards-build: the plan job decided what to build from the longest queue
`plan` is the job every other leg of this workflow declares in `needs` -- it
runs `scripts/standards-touched.py` and emits the matrix. It ran on
`linux-arm64`, which is the label the fleet cannot spare: measured while this
was queued, `linux-arm64` was 282 runs deep and `linux` was idle on a 20-core
host. So the small job that decides what to build waited behind the heavy jobs
it was deciding about, and every leg of the build waited on it.

It is pure Python over a git diff and needs no particular architecture, so it
moves to `linux`.

This is one line of the same fix #598 applies to all 55 path gates in the
repository, taken here because the proof-gate fix in this pull request cannot
land without it: that fix unblocks every branch whose proofs leg currently
turns a verified proof into a failure, and it was itself sitting behind the
queue it needs to clear. #598 remains the general change; the two diffs are
identical on this line and merge as one.

Co-Authored-By: Claude Opus 5 <[email protected]>
2026-11-03 06:40:53 -05:00

794 lines
43 KiB
YAML

name: standards workspaces build + test
# Build gate for every Rust workspace in the repo.
#
# It started as three. Then a toolchain bump compiled the rest for the first
# time and found FIVE more that did not build — smart-byte (47k LOC), openpay
# (six separate breakages across five crates), eoc, mesh and joule-ui — all
# broken by the same handful of upstream migrations (hmac -> KeyInit, reqwest
# feature-gating, cipher 0.4 -> 0.5, a struct gaining fields), and all invisible
# because nothing ever compiled them. Partial coverage is how that happens, so
# the matrix now covers everything.
#
# The original case, still the clearest: smart-byte-rs had never been compiled by
# anything, and it did not build. A single wrong `rand` pin — 0.10 against code
# written for 0.8, whose crypto stack requires rand_core 0.6 — silently disabled
# the entire identity pillar, BBS+ included. `cargo check` would have caught it
# on day one. An unbuilt standard is not a standard, so this workflow is the
# floor under every claim the specs make.
#
# One workflow with a matrix rather than sixteen files: the bootstrap step is
# identical everywhere, and a shared dependency change should rebuild all of
# them anyway. `fail-fast: false` so one red workspace does not mask the others.
# One run per branch at a time. A push supersedes the run before it.
#
# There is one `macos` runner and it is the dev Mac, so every macOS job in this
# repo queues on it. With no concurrency group, a session pushing four versions
# of a branch queued four complete sets of runs and every one of them had to
# drain: on 2026-10-05 a PR's 21 contexts settled none in 70 minutes behind a
# backlog of 25 runs, and the queue grew faster than it cleared. Only the newest
# commit's verdict is wanted, so the older runs are cancelled.
#
# Verified on this forge (Forgejo 16.0.5) in `ci-test` before being added here:
# the key parses, and a newer push moves an older run to `cancelled` even while
# it is still queued, which is the case that matters.
#
# `cancel-in-progress: true` also applies to `main`. That is deliberate and
# safe here: main advances by merge commits whose tree contains the commits
# before them, so the newer run covers the older one's changes.
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
on:
pull_request:
# Deliberately NO `paths:` filter.
#
# The first attempt used `**/*.rs` and `**/Cargo.toml`, and the workflow then
# silently did not fire — pushes touching exactly those files triggered other
# workflows but not this one, so `**`-prefixed globs evidently do not match here
# the way they do on GitHub. A build gate that quietly fails to run is worse than
# no gate at all: it reports nothing and everyone assumes green.
#
# This is the repo-wide floor. The nightly schedule builds every workspace; a merge to
# main does not run it again, since the pull request already built what it touched. A pull request
# builds the workspaces its own diff touches (the `plan` job, scripts/
# standards-touched.py): a workspace's own area, the areas of everything it depends on
# by path, any file outside them its sources name, and everything every leg shares (this
# file, the toolchain pin, the cargo configuration). Building all 17 for every pull
# request filled the one x86_64 runner's queue with builds no change could affect. The
# plan reads the pull request's diff, not the push delta, so a merge of main into a
# branch does not rebuild everything, and anything it cannot determine builds all.
schedule:
- cron: '7 4 * * *'
jobs:
# Which workspaces this change touches. The list of workspaces is here, one
# `- { ... }` line each, read by scripts/standards-touched.py; the build job's
# matrix is the entries it selects.
plan:
name: which workspaces this change touches
runs-on: linux
outputs:
include: ${{ steps.plan.outputs.include }}
any: ${{ steps.plan.outputs.any }}
energy: ${{ steps.plan.outputs.energy }}
env:
WORKSPACES: |
- { name: jcp-rs, dir: jcp/jcp-rs, runner: linux, conformance: jcp-conformance, feature_tests: "-p jcp-energy --features nvml" }
# sandbox-tee's certificate-chain verifiers sit behind features (their
# X.509 and RSA dependencies are heavy), so a plain `cargo test` never
# runs their tests: `amd-kds` (SEV-SNP's VCEK to AMD's root) and
# `intel-pcs` (TDX's PCK to Intel's root).
- { name: sandbox-rs, dir: sandbox/sandbox-rs, runner: linux, conformance: sandbox-conformance, feature_tests: "-p sandbox-tee --features amd-kds,intel-pcs" }
- { name: smart-byte-rs, dir: smart-byte/smart-byte-rs, runner: linux }
- { name: pool-rs, dir: pool/pool-rs, runner: linux }
# `clippy: true` adds the zero-warning gate below. It is opt-in per
# entry rather than repo-wide because several workspaces are not at
# zero yet, and a gate that fails on arrival teaches people to pass
# `--no-verify`. A workspace that reaches zero adds the flag and
# cannot regress; joulespec-rs starts there.
# `harvest: true` runs the standard against its own implementation:
# every conformance item of its SPEC §7 is mapped to a check, and
# each mapping declares a counter-artifact that must make that check
# FAIL before the evidence counts. It is slow (a rebuild per
# mutation) and it is the only gate that keeps the suite's
# falsifiability from decaying, which inspection does not catch --
# it found a test whose assertion could not fail and a branch that
# could not change a verdict.
- { name: joulespec-rs, dir: joulespec/joulespec-rs, runner: linux, clippy: true, harvest: true }
# The same workspace again on a host that has a model checker, to
# gate the proof path. The `linux` leg above cannot: with no prover
# installed the harvest reports the proof entries as not run, which
# is the right behaviour and no gate at all. `proofs: true` runs the
# harnesses live and, more importantly, checks that a
# counter-artifact still refutes one -- a proof that survives
# breaking the thing it proves is a proof of nothing, and that can
# decay silently in a way the parser's unit tests cannot see.
- { name: joulespec-proofs, dir: joulespec/joulespec-rs, runner: macos, proofs: true }
- { name: openpay, dir: openpay, runner: linux-arm64 }
- { name: joule-code-rs, dir: joule-code/joule-code-rs, runner: linux-arm64, z3: true }
- { name: map-rs, dir: map/map-rs, runner: linux-arm64, conformance: map-conformance }
- { name: aac-rs, dir: aac/aac-rs, runner: linux-arm64, conformance: aac-conformance }
- { name: joulecontract-rs, dir: joulecontract/joulecontract-rs, runner: linux-arm64, z3: true }
# Runner placement is by what a workspace actually needs, not by
# habit. The dev Mac hosts BOTH the `macos` runner and the
# `linux-arm64` colima VM, so it served 13 of this repo's 21
# contexts while jetson-hub (`linux`) sat idle — which is why a PR's
# macOS contexts could wait indefinitely while its `linux` ones
# returned in minutes.
#
# `arl-rs`, `sense-rs`, `joulehook-rs` and `joule-ui-rs` moved to
# `linux` on that basis: each has zero `target_os = "macos"` cfgs,
# zero Apple dependencies, and zero Apple crates in its Cargo.lock,
# so running them on macOS asserted nothing the repo relies on.
# `jouledesk-rs` stays, because it does need it — `libwebrtc` and 19
# Apple crates in its lockfile. `linux-arm64` placements stay too:
# arm64 is the deployment target, and `jouleclaw-rs` needs
# `+fp16`.
- { name: jouledesk-rs, dir: jouledesk/jouledesk-rs, runner: macos }
- { name: arl-rs, dir: arl/arl-rs, runner: linux }
- { name: sense-rs, dir: sense/sense-rs, runner: linux }
# `applied:` points the joulespec producer at this standard's own
# conformance items (SPEC §8), mapped to real checks with a
# counter-artifact each. It is the only gate that keeps those
# mappings honest: a refactor that moves the code a mutation was
# aimed at makes the harvest refuse, and a check that stops being
# able to fail becomes a finding rather than staying green.
- { name: proof-rs, dir: proof/proof-rs, runner: linux, z3: true, conformance: proof-conformance, applied: proof/conformance/v1/joulespec.toml }
- { name: joulehook-rs, dir: joulehook/joulehook-rs, runner: linux }
- { name: eoc-rs, dir: eoc/eoc-rs, runner: linux, feature_tests: "-p eoc-meter --features cuda" }
# mesh-openai's `serve_example` test (the reference server seals what
# its meter read, never a fixture's figure) has required-features
# `server`, so `cargo test --workspace` builds none of it; naming the
# package here is what runs it. Selecting mesh-engine-gguf alone
# compiles mesh-openai with `server` but runs none of its tests.
- { name: mesh-rs, dir: mesh/mesh-rs, runner: linux-arm64, feature_tests: "-p mesh-engine-gguf -p mesh-openai --features mesh-engine-gguf/gguf,mesh-openai/server" }
- { name: joule-ui-rs, dir: joule-ui/joule-ui-rs, runner: linux }
# jouleclaw-rs is the one entry whose runner IS a correctness choice.
# It reaches candle → ug → gemm, which uses inline aarch64 assembly
# (`fmla {0:v}.8h, ...`) requiring the ARMv8.2 FP16 extension.
# `aarch64-apple-darwin` carries target_feature="fp16" in its baseline
# because Apple Silicon guarantees it; `aarch64-unknown-linux-gnu`
# baselines at ARMv8.0-A and does not, so the same asm fails to
# ASSEMBLE — a codegen error `cargo check` never reaches. Verified on a
# native arm64 Linux container (rustc 1.98.0): without the flag, 12
# errors; with it, 4457 tests pass.
#
# CAPACITY: this is by far the largest entry — its target tree is
# ~16 GB, against a 120 GB volume on tx-dev-linux-arm64 that already
# holds ~74 GB of other workspaces' caches. If linux-arm64 jobs start
# failing for no apparent reason, check `df -h /mnt/lima-colima-txarm`
# on the txarm VM before suspecting the code: a full cache volume
# fails whatever happens to be building, not whatever changed.
- { name: jouleclaw-rs, dir: jouleclaw/jouleclaw-rs, runner: linux-arm64, rustflags: "-C target-feature=+fp16", cache_suffix: "-nodebug", feature_tests: "-p jouleclaw-energy --features rapl,nvml" }
steps:
- uses: actions/checkout@v5
with:
fetch-depth: 0
- name: The decision fails closed (self-test)
run: bash scripts/standards-touched-selftest.sh
- id: plan
name: Which workspaces this change touches
run: |
set -euo pipefail
python3 scripts/standards-touched.py --github-output \
"${{ github.event.pull_request.base.sha }}" \
"${{ github.event.pull_request.head.sha }}"
build:
name: ${{ matrix.name }}
needs: plan
if: needs.plan.outputs.any == 'true'
# Spread across the fleet's runners rather than pinning every job to `linux`.
# For most of these the runner is a capacity choice, not a correctness one —
# and every job on one runner queues behind whatever else is using it.
# `jouleclaw-rs` is the exception: see its matrix entry.
runs-on: ${{ matrix.runner }}
strategy:
fail-fast: false
matrix:
include: ${{ fromJSON(needs.plan.outputs.include) }}
steps:
- uses: actions/checkout@v5
# Three workspaces shell out to `z3`, and the runner image has no solver.
#
# This step used to be load-bearing for correctness: without a solver the
# ladder escalated past its real rungs into a model STAND-IN that reported
# Proved, so every goal on a solverless machine came back proved. That is
# now fixed at the source — the real ladders hold decision procedures only
# and an absent rung yields Unproved (proof-solvers `ladder_is_sound` and
# `ladder_never_fabricates_a_proof_when_a_rung_is_absent`).
#
# So the suites pass with or without z3, and this step is kept purely for
# COVERAGE: with a solver present the real T1 rung actually runs, and the
# SMT paths are exercised rather than skipped. The absent-rung semantics
# stay covered either way — that regression test uses a goal z3 cannot
# parse, so it asserts the same thing on a machine that has one.
#
# joule-code-remediate's formal gate is the third. Its tests assert in both
# branches, so they pass without a solver, and JOULE_FIX_EXPECT_Z3=1 below
# makes a missing z3 fail them where this step installed one. Otherwise CI
# would only ever run the no-solver branch.
#
# The z3 jobs are pinned to Linux runners deliberately: the macOS runner is
# a host executor with no apt. `sudo` may or may not exist depending on
# whether the container runs as root, so fall back to a bare invocation.
- name: Install z3
if: matrix.z3
shell: bash
run: |
SUDO=""; [ "$(id -u)" -ne 0 ] && SUDO="sudo"
$SUDO apt-get update -qq
$SUDO apt-get install -y -qq z3
z3 --version
# The docker runner image ships no Rust at all, so rustup is bootstrapped
# here. dtolnay/rust-toolchain cannot be used: it shells out to `rustup`,
# which the image lacks. Harmless where cargo already exists.
- name: Install Rust (workspace pin)
shell: bash
run: |
export PATH="$HOME/.cargo/bin:$PATH"
command -v rustup >/dev/null 2>&1 || \
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
# jouleclaw-rs is the CAPACITY entry above. Linux embeds full DWARF in every
# test binary, so with default debuginfo its aarch64 test target outgrows
# the ~15 GB left on the shared txarm volume and the link fails with
# "No space left on device" (reproduced with the same toolchain, flags and
# image). Without debuginfo the same target is ~6 GB and the whole suite
# passes. Panic messages keep their file:line: that comes from the panic
# location, not from DWARF.
#
# Set through $GITHUB_ENV rather than a matrix field on purpose: a matrix
# field would hand every other job CARGO_PROFILE_DEV_DEBUG="", which cargo
# can reject. `cache_suffix` gives this job a fresh cache namespace so it
# cannot restore a full-debuginfo target and hold both builds at once;
# for every other job the suffix is empty and its key string is unchanged.
- name: Trim debuginfo (arm64 jouleclaw)
if: matrix.name == 'jouleclaw-rs'
shell: bash
run: echo "CARGO_PROFILE_DEV_DEBUG=0" >> "$GITHUB_ENV"
# aac-rs builds its page sets in its tests (tools/pagesets: build.py,
# phrases/build.py) and checks them against the committed catalogue
# (catalog.py --check, below). Those need Python 3.11+ with PyYAML; the
# runner image has Python 3.10 and no PyYAML, and with neither the
# tests would only report that they could not build anything. uv puts
# a Python 3.12 and PyYAML in a venv of the job's own, on Linux or
# macOS; the tests use it through AAC_PYTHON and fail, not skip, when
# CI is set and there is none. Verified in catthehacker/ubuntu:act-22.04
# on arm64: Python 3.12.15, PyYAML 6.0.3.
- name: Python 3.11+ and PyYAML for the page sets
if: matrix.name == 'aac-rs'
shell: bash
run: |
export PATH="$HOME/.local/bin:$HOME/.cargo/bin:$PATH"
command -v uv >/dev/null 2>&1 || curl -LsSf https://astral.sh/uv/install.sh | sh
uv venv -q --python 3.12 "$HOME/.pagesets-py"
uv pip install -q --python "$HOME/.pagesets-py/bin/python" pyyaml
"$HOME/.pagesets-py/bin/python" -c 'import sys, yaml; assert sys.version_info >= (3, 11); print(sys.version, "PyYAML", yaml.__version__)'
echo "AAC_PYTHON=$HOME/.pagesets-py/bin/python" >> "$GITHUB_ENV"
- name: Cache cargo registry + target
uses: actions/cache@v4
with:
path: |
~/.cargo/registry
~/.cargo/git
${{ matrix.dir }}/target
key: standards-${{ matrix.name }}${{ matrix.cache_suffix }}-${{ hashFiles(format('{0}/Cargo.lock', matrix.dir), 'rust-toolchain.toml') }}
restore-keys: |
standards-${{ matrix.name }}${{ matrix.cache_suffix }}-
# --all-targets is load-bearing: a plain `cargo check` does not build test
# targets, and smart-byte's dev-dependencies drifted independently of its
# normal ones (rand_chacha 0.10 against rand 0.8). The library compiled
# while the tests did not.
- name: Check (all targets)
working-directory: ${{ matrix.dir }}
env:
RUSTFLAGS: ${{ matrix.rustflags }}
run: cargo check --workspace --all-targets
- name: Test
working-directory: ${{ matrix.dir }}
env:
RUSTFLAGS: ${{ matrix.rustflags }}
# Where z3 was installed above, its absence is a failure, not a skip.
JOULE_FIX_EXPECT_Z3: ${{ matrix.z3 && '1' || '' }}
run: cargo test --workspace
# The zero-warning gate, on the workspace's own runner.
#
# Deliberately not in the macOS lint step: that one exists for code only
# a macOS host can compile, and the matrix comments above are about not
# sending platform-neutral work to the contended Mac. A workspace that
# needs no Apple anything is linted where it is built.
- name: Clippy (all targets, warnings denied)
if: matrix.clippy
working-directory: ${{ matrix.dir }}
env:
RUSTFLAGS: ${{ matrix.rustflags }}
run: cargo clippy --workspace --all-targets -- -D warnings
# The standard applied to its own implementation. Exits 2 on a finding
# (a check that did not run, or one that passed while its subject was
# broken) and 3 when an obligation falls below the bar, so a decayed
# suite fails here rather than being discovered by a reader.
#
# It mutates files in the checkout and reverts them; the revert runs on
# drop, so a panic cannot leave a mutation in place. The step asserts the
# tree is clean afterwards rather than trusting that.
- name: Self-conformance harvest
if: matrix.harvest
working-directory: ${{ matrix.dir }}
run: |
set -euo pipefail
cargo build --release -p joulespec-cli
target="$(cargo metadata --no-deps --format-version 1 \
| python3 -c 'import json,sys; print(json.load(sys.stdin)["target_directory"])')"
"$target/release/joulespec" harvest \
--manifest ../conformance/v1/harvest.toml --require-grade E3
- name: The harvest left no mutation behind
if: matrix.harvest
run: |
set -euo pipefail
if ! git diff --quiet; then
echo "the harvest did not revert cleanly:"
git diff --stat
exit 1
fi
# The same producer, pointed at a *different* standard.
#
# `applied: <manifest>` names a manifest that lives with the standard it
# describes, so this measures how well that standard's own conformance
# items are evidenced. It is deliberately a separate step from the one
# above: that one builds the producer from the workspace under test,
# which only works where the workspace under test *is* the producer's.
# Here the producer is built from its own workspace and then run against
# someone else's.
#
# No `--out`: a receipt written here would dirty the tree and fail the
# revert check below, and its energy figures differ every run anyway.
- name: JouleSpec applied to this standard
if: matrix.applied
run: |
set -euo pipefail
# Built and located in separate commands on purpose: folded into
# one substitution, a build failure yields an empty path and the
# step fails with "no such file" instead of the compiler error.
( cd joulespec/joulespec-rs && cargo build --release -p joulespec-cli )
target="$(cd joulespec/joulespec-rs \
&& cargo metadata --no-deps --format-version 1 \
| python3 -c 'import json,sys; print(json.load(sys.stdin)["target_directory"])')"
test -x "$target/release/joulespec" \
|| { echo "the producer did not build at $target/release/joulespec"; exit 1; }
"$target/release/joulespec" harvest \
--manifest "${{ matrix.applied }}" --require-grade E3
- name: The applied harvest left no mutation behind
if: matrix.applied
run: |
set -euo pipefail
if ! git diff --quiet; then
echo "the applied harvest did not revert cleanly:"
git diff --stat
exit 1
fi
# Both directions of the proof path, live.
#
# The first run must verify with every declared reachability cover
# satisfied -- a checker reports success for an over-constrained harness
# in the same words it uses for one that examined everything, so the
# cover line is what distinguishes them and is asserted here directly.
#
# The second run is the one that matters. It narrows the ratio rule's
# arithmetic from 128 bits to 64 and requires the prover to FAIL. The
# entire test suite passes under that same mutation, so this step is the
# only place in CI where the rung above `E3` is shown to be doing
# anything.
- name: Proof harnesses verify, with every cover reached
if: matrix.proofs
working-directory: ${{ matrix.dir }}
run: |
set -euo pipefail
export PATH="$HOME/.cargo/bin:$PATH"
cargo kani --version
for h in the_ratio_rule_is_total_over_every_input \
widening_a_set_can_only_lower_its_cap; do
echo "== $h =="
out="$(cargo kani -p joulespec-core --harness "$h" 2>&1)"
echo "$out" | grep -E '^ \*\* |^VERIFICATION'
# A here-string, not `echo | grep -q`: grep -q exits at the first
# match, echo then dies of SIGPIPE (141), and `set -o pipefail`
# turns a match into a failure. It is a race on how much of $out
# fits the pipe buffer, so it passed while this harness reported 15
# properties and failed at 336.
grep -q '^VERIFICATION:- SUCCESSFUL' <<<"$out" \
|| { echo "$h did not verify"; exit 1; }
# "N of M cover properties satisfied". Both numbers are read with
# their own expression rather than by splitting one capture, so
# the gate does not depend on the shell's word-splitting rules.
line="$(echo "$out" | grep -E '^ \*\* [0-9]+ of [0-9]+ cover properties satisfied$' || true)"
[ -n "$line" ] || { echo "$h declared no cover"; exit 1; }
got="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\1/')"
want="$(echo "$line" | sed -E 's/^ \*\* ([0-9]+) of ([0-9]+) .*$/\2/')"
[ "$got" = "$want" ] \
|| { echo "$h: only $got of $want covers reached -- proved over an empty domain"; exit 1; }
done
- name: A counter-artifact still refutes a proof
if: matrix.proofs
working-directory: ${{ matrix.dir }}
run: |
set -euo pipefail
export PATH="$HOME/.cargo/bin:$PATH"
f=crates/joulespec-core/src/conform.rs
before="$(grep -c 'u128::from(part)' "$f")"
[ "$before" = "1" ] || { echo "expected one anchor, found $before"; exit 1; }
trap 'git checkout -- "$f"' EXIT
sed -i.ci -e 's|^ Some(((u128::from(part).*$| Some((part * 1_000_000) / total)|' "$f"
rm -f "$f.ci"
grep -q 'u128::from(part)' "$f" && { echo "the mutation did not apply"; exit 1; }
echo "mutation applied: the scale is now computed in 64 bits"
out="$(cargo kani -p joulespec-core --harness the_ratio_rule_is_total_over_every_input 2>&1 || true)"
echo "$out" | grep -E '^ \*\* |^VERIFICATION'
grep -q '^VERIFICATION:- FAILED' <<<"$out" \
|| { echo "the prover did not refute an overflowing ratio rule"; exit 1; }
# The NVML backends sit behind features no workspace member enables
# (jcp-energy `nvml`, eoc-meter `cuda`, jouleclaw-energy `nvml`), so the
# step above never compiles them, let alone runs their tests. Here they
# build and their tests run, as do mesh-rs's feature-gated tests (the
# gguf engines; mesh-openai's `server` and its serve_example test). The container has no GPU and Docker masks
# powercap, so the hardware tests take their "unavailable, and the
# oracle agrees" branch; the rule's unit tests run in full.
- name: Feature-gated energy tests
if: matrix.feature_tests
working-directory: ${{ matrix.dir }}
env:
RUSTFLAGS: ${{ matrix.rustflags }}
run: cargo test ${{ matrix.feature_tests }}
# The page-set packages are not committed; their catalogue is, naming
# each package by its content. Any change to what they are built from —
# the sources, the app's translations and gloss audits, the symbol
# index and sprites, the navigation words, vocabulary.rs, i18n.rs, the
# language packs — changes the packages, and the committed catalogue
# must change with them (catalog.py --write), or the app would offer
# packages it would then refuse to use.
- name: Page-set catalogue is current
if: matrix.name == 'aac-rs'
working-directory: ${{ matrix.dir }}
shell: bash
run: |
"$AAC_PYTHON" tools/pagesets/catalog.py --check
"$AAC_PYTHON" tools/pagesets/phrases/build.py --check
# Run each standard's conformance suite.
#
# These suites live in a binary's `main()`, not in `#[test]`, so
# `cargo test` never executes them — verified, not assumed:
# `cargo test -p aac-conformance` runs **0 tests** while
# `cargo run -p aac-conformance` runs **40 checks**; map is 1 test vs 15
# checks. Same shape for jcp, proof and sandbox. The suites include
# negative vectors (`C-neg`, `Cneg`), which are the ones that catch a
# verifier ACCEPTING what it must reject.
#
# This is the `main()` instance of the same bug as a feature-gated test:
# the code compiles under `--all-targets`, reports nothing, and looks
# covered. Compiling a suite is not running it.
#
# `--bin` is explicit because these crates also ship a `gen-vectors`
# binary; `cargo run -p <crate>` is ambiguous with two binaries and fails
# rather than choosing — which is how this step would silently never run.
#
# No path argument: these binaries take none. They check the
# implementation against in-code expectations, which is a different claim
# from validating the published `conformance/v1` files on disk.
#
# That second claim is made elsewhere, by tests inside the reference
# implementations that read `conformance/v1` off disk, which the `Test`
# step above already runs — so it needs no entry here and a missing
# `conformance:` key is not evidence a standard's pack is unchecked.
#
# Deliberately not "a `tests/pack.rs` in each conformance crate": that
# is the convention in several of them, not a rule, and some crates read
# the pack from a test named something else or from another crate
# entirely. So counting files by that name does not audit pack coverage,
# and finding a crate without one is not a finding. The question is
# which tests read the published bytes:
#
# grep -rl --include=*.rs -E 'conformance/v[0-9]' <standard>/
#
# That mistake has been made here twice, both times concluding standards
# were uncovered when they were not.
#
# `joule-code` is deliberately absent from that key. Its verifier does read
# the published pack, but it requires a `verify <pack-dir>` argument and
# prints usage with a non-zero exit when given none, so it cannot be
# invoked by this step's no-argument form. It has its own workflow,
# `joule-code-conformance.yml`, plus a `tests/pack.rs` that the `Test` step
# above runs — the latter because that workflow is `paths:`-filtered to
# `joule-code/**`, while the crate depends on `jcp-*` across workspaces.
- name: Conformance suite
if: matrix.conformance
working-directory: ${{ matrix.dir }}
env:
RUSTFLAGS: ${{ matrix.rustflags }}
run: cargo run -q -p ${{ matrix.conformance }} --bin ${{ matrix.conformance }}
# ── The macOS energy backends are exercised NOWHERE otherwise ─────────────
#
# Five crates carry an Apple Silicon IOReport energy meter: jcp-energy,
# proof-cascade, eoc-meter, jouleclaw-energy and sandbox-meter. Each is
# behind `#[cfg(target_os = "macos")]` (jouleclaw-energy also behind its
# `ioreport` feature), and every workspace holding one is pinned to a linux
# runner above. A platform-gated test on a single-platform runner is zero
# coverage, and it is indistinguishable from passing.
#
# What this job checks, and why it used to flake. On macOS 27 an unprivileged
# reader does not see the IOReport "Energy Model" CPU rails (`CPU Energy`,
# `DIE_<n>_CPU Energy`) move under load. They are republished only in rare
# lumps: on the M3 Ultra both dies held for over 22 minutes, then jumped
# about 1.3 kJ each in a single 100 ms sample. On the M5 Max the GPU rail
# stays live. The old jcp-energy test asserted that the *summed* rails
# advanced during a CPU burn, and the GPU rail satisfied that whenever
# something drew on screen. It passed by day and failed at night. The
# 2026-09-19 zero that "healed" by 09-21 was this effect, not a recovery.
#
# Every meter now uses IOReport only when the CPU rail itself keeps
# advancing while the probe burns CPU: in at least 5 sample intervals, at
# least 4 in every 5, over at least 300 ms. A lump is published in steps (one
# was caught as +61.8 kJ, then +3.4 J 64 ms later), so two advancing
# intervals are still just a lump. Otherwise the meter falls back to its
# estimator rung. Its tests assert against an independent oracle that reads
# the CPU rail directly, so this job is deterministic:
# - green while each meter declines a rail that does not keep moving;
# - red if any meter selects one;
# - on a host whose rail is live, red unless CPU work meters non-zero.
#
# Each step fails unless its test printed the `ioreport liveness:` line. That
# line is the only proof the platform-gated test ran and asserted a branch,
# rather than a filter, a feature or a cfg leaving zero tests to pass. It goes
# to stderr and is captured on success, hence `--nocapture` and `2>&1`.
macos-energy-backend:
name: macOS energy backends
# Runs when the change touches a workspace whose energy backend it tests (the plan's
# `energy`), and on the nightly schedule.
needs: plan
if: needs.plan.outputs.energy == 'true'
runs-on: macos
steps:
- uses: actions/checkout@v4
- name: Install Rust (workspace pin)
shell: bash
run: |
export PATH="$HOME/.cargo/bin:$PATH"
command -v rustup >/dev/null 2>&1 || \
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
- name: Cache cargo registry + targets
uses: actions/cache@v4
with:
path: |
~/.cargo/registry
~/.cargo/git
jcp/jcp-rs/target
proof/proof-rs/target
eoc/eoc-rs/target
jouleclaw/jouleclaw-rs/target
sandbox/sandbox-rs/target
joule-code/joule-code-rs/target
key: standards-macos-energy-${{ hashFiles('jcp/jcp-rs/Cargo.lock', 'proof/proof-rs/Cargo.lock', 'eoc/eoc-rs/Cargo.lock', 'jouleclaw/jouleclaw-rs/Cargo.lock', 'sandbox/sandbox-rs/Cargo.lock', 'joule-code/joule-code-rs/Cargo.lock', 'rust-toolchain.toml') }}
restore-keys: |
standards-macos-energy-
# Each crate's lib tests plus its integration tests. Each crate has a
# tests/ file that checks the liveness probe runs exactly once per process,
# and that check only holds in a fresh process. `--lib` would skip it.
- name: jcp-energy
shell: bash
working-directory: jcp/jcp-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p jcp-energy -- --nocapture 2>&1 | tee "$log"
grep -q 'ioreport liveness:' "$log"
- name: proof-cascade
shell: bash
working-directory: proof/proof-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p proof-cascade -- --nocapture 2>&1 | tee "$log"
grep -q 'ioreport liveness:' "$log"
- name: eoc-meter
shell: bash
working-directory: eoc/eoc-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p eoc-meter -- --nocapture 2>&1 | tee "$log"
grep -q 'ioreport liveness:' "$log"
# Double-gated: `cfg(all(feature = "ioreport", target_os = "macos"))`.
# A macOS runner alone reaches none of it.
- name: jouleclaw-energy (feature AND platform gated)
shell: bash
working-directory: jouleclaw/jouleclaw-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p jouleclaw-energy --features ioreport -- --nocapture 2>&1 | tee "$log"
grep -q 'ioreport liveness:' "$log"
- name: sandbox-meter
shell: bash
working-directory: sandbox/sandbox-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p sandbox-meter -- --nocapture 2>&1 | tee "$log"
grep -q 'ioreport liveness:' "$log"
# The tree meter's real-process tests (tests/tree_energy.rs) are
# gated to Apple Silicon macOS too; each prints this line.
grep -q 'tree meter:' "$log"
# jcp-gateway meters each gated call on the upstream server's own
# process tree with that meter. The jcp-rs matrix entry runs on Linux,
# where there is no tree meter and every call is metered machine-wide,
# so its real-process test (tests/upstream_tree.rs, Apple Silicon macOS
# only) runs nowhere else. Each call it meters on a real server's tree
# prints this line (the machine-wide fallback test prints another), so
# the grep fails if a cfg or a filter left none of them to run.
- name: jcp-gateway (upstream process tree)
shell: bash
working-directory: jcp/jcp-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p jcp-gateway -- --nocapture 2>&1 | tee "$log"
grep -q 'upstream tree:' "$log"
# proof-solvers reads each resident z3 decision off z3's own process
# tree with that meter (tests/z3_tree.rs, Apple Silicon macOS only, on a
# real z3: Homebrew's, on this runner's PATH). The proof-rs matrix entry
# runs on Linux, where there is no tree meter, so these run nowhere
# else. Each decision they meter prints this line; a missing z3, or a
# per-process counter that is not live, prints another, and the grep
# fails.
- name: proof-solvers (resident z3 process tree)
shell: bash
working-directory: proof/proof-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p proof-solvers -- --nocapture 2>&1 | tee "$log"
grep -q 'z3 tree meter:' "$log"
# sandbox-proof's local inference proof meters the engine on its own
# process tree, spawned suspended and read before it is reaped. Its
# real-engine tests are gated to Apple Silicon macOS; each run they
# meter prints this line.
# sandbox-exec-os earns S1 only where its probe shows the operating
# system's sandbox confining a program on this host, and that branch
# exists only on macOS: every other runner takes the S0 branch. The step
# fails unless the test printed the confinement it found, the only proof
# the S1 branch ran rather than the S0 one passing in its place.
- name: sandbox-exec-os (Seatbelt confinement at S1)
shell: bash
working-directory: sandbox/sandbox-rs
env:
SANDBOX_EXEC_OS_EXPECT_S1: "1"
run: |
set -o pipefail
log=$(mktemp)
cargo test -p sandbox-exec-os -- --nocapture 2>&1 | tee "$log"
grep -q 'sandbox-exec-os: confinement seatbelt/' "$log"
grep -q 'denied a read outside the grants' "$log"
- name: sandbox-proof (local engine process tree)
shell: bash
working-directory: sandbox/sandbox-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p sandbox-proof -- --nocapture 2>&1 | tee "$log"
grep -q 'local engine tree:' "$log"
# joule-fix meters its L3 model on the model's own process tree. The
# joule-code-rs matrix entry runs on linux-arm64, where there is no tree
# meter, so its oracle test (the model's reading against the stand-in's
# own energy count) takes its fallback branch there and runs nowhere
# else. It prints this line only where it checked the reading.
- name: joule-code-remediate (L3 model process tree)
shell: bash
working-directory: joule-code/joule-code-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p joule-code-remediate l3_ -- --nocapture 2>&1 | tee "$log"
grep -q 'l3 model process:' "$log"
# Feature AND platform gated: `fabric-meter`, which no other job passes,
# and macOS. The fabric calibration rows' macOS stamp, and a CPU member
# priced on this process's own counters against its own energy count
# (tests/process_calibration.rs), each print their line only there.
#
# The calibration test meters the GPU counter only once a GPU liveness load has run, and
# that load gives up after 500 ms on a GPU too busy to grant it. The test then takes its
# refusal branch and passes, but prints no `process calibration:` line, so the grep fails
# on host load alone (seen 2026-10-25, the runner's host at load 55). Its own retries
# keep that from costing a whole pull request's rerun: up to three runs, 20 s apart, and
# the line must still come from a run on live counters. A failing assertion fails the
# step at once, as before.
- name: jouleclaw-loader-gguf (fabric-meter, process calibration)
shell: bash
working-directory: jouleclaw/jouleclaw-rs
run: |
set -o pipefail
log=$(mktemp)
cargo test -p jouleclaw-loader-gguf --features "rayon fabric-meter" marginal_energy -- --nocapture 2>&1 | tee "$log"
for attempt in 1 2 3; do
cargo test -p jouleclaw-loader-gguf --features "rayon fabric-meter" --test process_calibration -- --nocapture 2>&1 | tee -a "$log"
grep -q 'process calibration: CPU member' "$log" && break
echo "process calibration: attempt $attempt ran without live GPU counters (a busy GPU); trying again in 20 s"
sleep 20
done
grep -q 'calibration row stamped on macOS:' "$log"
grep -q 'process calibration: CPU member' "$log"
# The meter code the steps above test compiles only on macOS (IOReport,
# proc_pid_rusage, the process-tree readers), so no Linux job lints it.
# Lints in it went unseen until a macOS sweep found them (#244). Each
# crate is linted here, on its own platform and with the features its
# tests use, and a warning fails the step.
- name: clippy on the macOS meter code
shell: bash
run: |
set -eu
lint() { (cd "$1" && shift && cargo clippy --all-targets --no-deps "$@" -- -D warnings); }
lint jcp/jcp-rs -p jcp-energy -p jcp-gateway
lint proof/proof-rs -p proof-cascade -p proof-solvers
lint eoc/eoc-rs -p eoc-meter
lint jouleclaw/jouleclaw-rs -p jouleclaw-energy --features ioreport
# And the DEFAULT build. Linting only the featured one hid a real
# clippy error for as long as it existed: every hardware meter in
# `detect_meter` is behind a `cfg`, so the default build is a
# different program, and a lint pass that never compiles it cannot
# speak for it.
lint jouleclaw/jouleclaw-rs -p jouleclaw-energy
# The metal feature makes ~19k lines reachable that no Linux job can
# see. It was at 10983 warnings when first linted; it is at 0.
#
# The caveat above applies here too, and bit: this covers
# `--features metal` alone, so an item it calls unused may still be
# required under another configuration. A label whose `break` sits
# behind `cfg(feature = "fabric")` was deleted on exactly that
# evidence and broke the fabric-meter build in this very job.
lint jouleclaw/jouleclaw-rs -p jouleclaw-omni --features metal
# And the crate omni loads its weights through, which was linted
# by nothing at all: 161 warnings when first measured, now 0.
#
# Both configurations. `--no-deps` does not exclude workspace path
# dependencies, so the fabric-meter line also covers
# jouleclaw-backend-apple, which is why that crate is linted on its
# own below rather than only incidentally.
lint jouleclaw/jouleclaw-rs -p jouleclaw-loader-gguf
lint jouleclaw/jouleclaw-rs -p jouleclaw-loader-gguf --features "rayon fabric-meter"
# The Apple backend: 84 warnings when first measured on its own, now
# 0. It has no features, only a macOS-conditional dependency block,
# so there is one configuration to keep clean.
lint jouleclaw/jouleclaw-rs -p jouleclaw-backend-apple
lint sandbox/sandbox-rs -p sandbox-meter -p sandbox-proof