3354465adf
joule-code-remediate's formal gate shells out to z3, and neither job that tests it installed a solver: joule-code-rs in standards-build, and the joule-code conformance gate. Its z3 tests used to return early without a solver, so CI passed without ever running the real-solver path. sandbox-meter/cpu-rail-liveness (#114) makes those tests assert in both branches, and adds JOULE_FIX_EXPECT_Z3=1 to turn a missing solver into a failure. joule-code-rs now joins the `z3: true` matrix entries, as joulecontract-rs already does on the same runner kind. The conformance gate installs z3 the same way. Both set JOULE_FIX_EXPECT_Z3=1 where z3 was installed. Elsewhere the variable is empty, and only joule-code- remediate reads it. Co-Authored-By: Claude Opus 5.5 <[email protected]>
93 lines
3.7 KiB
YAML
93 lines
3.7 KiB
YAML
name: joule-code conformance gate
|
||
|
||
# Enforces the Joule Code conformance contract on every change: the reference
|
||
# library must build and pass its tests, and the published C1–C4 wire vectors
|
||
# must round-trip (SPEC §8). "Conformant = round-trips the vectors" — checked,
|
||
# not asserted.
|
||
|
||
on:
|
||
pull_request:
|
||
paths:
|
||
- 'joule-code/**'
|
||
# joule-moq's receipt tests pin leaves, roots and signatures copied from WAI's
|
||
# jwp-conformance corpus, and run every leaf, group and object vector in it:
|
||
# a change there must re-run them.
|
||
- 'wai/jwp-conformance/**'
|
||
- '.github/workflows/joule-code-conformance.yml'
|
||
push:
|
||
branches:
|
||
- main
|
||
paths:
|
||
- 'joule-code/**'
|
||
# joule-moq's receipt tests pin leaves, roots and signatures copied from WAI's
|
||
# jwp-conformance corpus, and run every leaf, group and object vector in it:
|
||
# a change there must re-run them.
|
||
- 'wai/jwp-conformance/**'
|
||
- '.github/workflows/joule-code-conformance.yml'
|
||
|
||
jobs:
|
||
conformance:
|
||
name: Build + round-trip C1-C4 vectors
|
||
runs-on: linux
|
||
steps:
|
||
- name: Checkout
|
||
uses: actions/checkout@v4
|
||
|
||
# Bootstrap rustup: the docker runner image ships no Rust, and
|
||
# dtolnay/rust-toolchain cannot help — it calls `rustup`, which is absent.
|
||
- name: Install Rust 1.98.0
|
||
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 --default-toolchain 1.98.0
|
||
rustup toolchain install 1.98.0 --profile minimal
|
||
rustup default 1.98.0
|
||
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
|
||
|
||
- name: Cache cargo
|
||
uses: actions/cache@v4
|
||
with:
|
||
path: |
|
||
~/.cargo/registry
|
||
~/.cargo/git
|
||
joule-code/joule-code-rs/target
|
||
key: joule-code-${{ runner.os }}-${{ hashFiles('joule-code/joule-code-rs/Cargo.lock') }}
|
||
|
||
# joule-code-remediate's formal gate shells out to `z3`, and the runner
|
||
# image has no solver. Its tests assert in both branches. With a solver
|
||
# installed here, JOULE_FIX_EXPECT_Z3=1 makes its absence a failure, so
|
||
# this gate runs the real-solver branch rather than the fail-closed one.
|
||
- name: Install 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
|
||
|
||
- name: Reference library tests
|
||
working-directory: joule-code/joule-code-rs
|
||
env:
|
||
JOULE_FIX_EXPECT_Z3: '1'
|
||
run: cargo test --workspace
|
||
|
||
# joule-moq's QUIC transport and its example compile only with `quic`. Named
|
||
# here so they stay built and tested whatever the workspace's other members
|
||
# happen to enable; this also runs tests/wai_jwp_corpus.rs, every leaf, group
|
||
# and object vector of wai/jwp-conformance through the crate.
|
||
- name: joule-moq with the QUIC transport, every target
|
||
working-directory: joule-code/joule-code-rs
|
||
run: cargo test -p joule-moq --features quic --all-targets
|
||
|
||
- name: Round-trip the v1 conformance pack (C1-C4)
|
||
working-directory: joule-code/joule-code-rs
|
||
run: |
|
||
set -e
|
||
out="$(cargo run -q -p joule-code-conformance -- verify ../conformance/v1)"
|
||
echo "$out"
|
||
# The pack must pass with zero failures.
|
||
echo "$out" | grep -Eq '0 failed' || { echo "::error::conformance pack reported failures"; exit 1; }
|
||
|
||
- name: L3 JouleClaw binding example builds + tests
|
||
working-directory: joule-code/examples/l3-jouleclaw
|
||
run: cargo test
|