diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 83f5221..366f13b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -83,7 +83,14 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-latest, macos-latest, windows-latest] + # ubuntu-22.04-arm is here so the aarch64-linux RELEASE target has + # continuous evidence rather than first running at tag time. + # `release.yml` only fires on a tag push, so a target added there + # alone would ship on the strength of an unrun job — the same + # unexercised-gate shape this repository keeps finding. Building it + # on every PR means a toolchain or z3-sys regression on ARM fails a + # check now, not during a release. + os: [ubuntu-latest, ubuntu-22.04-arm, macos-latest, windows-latest] steps: - uses: actions/checkout@v7 - uses: dtolnay/rust-toolchain@stable diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 5eb61aa..d5c81bc 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -35,10 +35,18 @@ jobs: # so no host libz3 is required on the runner. The build succeeds on # every target in the CI matrix. # - # No aarch64-linux for now: the rocq-of-rust + bazel/nix stack used by - # the Rocq Formal Proofs job already constrains this repo's CI runners, - # and cross-compiling z3-sys for aarch64-linux is untested. Add it as - # a follow-up once the standard matrix is green again. + # aarch64-linux IS built (see the matrix entry below). The earlier + # deferral note here said cross-compiling z3-sys for aarch64-linux was + # untested — which was true, and is now moot: the target builds NATIVELY + # on a GitHub-hosted arm64 Linux runner, so nothing is cross-compiled. + # z3-sys vendors and statically compiles z3, so it needs no host libz3 on + # any runner, ARM included. Those runners are free for public repos, and + # this repository is public. + # + # The gap was real for consumers: v1.4.1 shipped x86_64-linux, both macOS + # arches and Windows, so ARM Linux — servers, arm64 containers, ARM CI + # runners, SBCs — had no binary at all and had to build from source with a + # C++ toolchain, which is the very thing #313 exists to remove. build-binaries: name: Build ${{ matrix.target }} runs-on: ${{ matrix.os }} @@ -59,6 +67,15 @@ jobs: os: ubuntu-22.04 archive: tar.gz binary: loom + # Same 22.04 image family as x86_64 above, and for the same #311 + # reason: the runner image sets the shipped binary's glibc floor, + # so it is pinned rather than `-latest`, and the floor is ASSERTED + # below for this target too. A target that ships without that + # assertion is exactly how v1.2.0 went out unloadable. + - target: aarch64-unknown-linux-gnu + os: ubuntu-22.04-arm + archive: tar.gz + binary: loom # x86_64-apple-darwin cross-compiles on the arm64 macos-14 # runner — matches pulseengine/synth, rivet, witness. - target: x86_64-apple-darwin @@ -96,10 +113,13 @@ jobs: # The libstdc++ requirement exists only because loom links Z3 (C++) — it # disappears with the ordeal migration, and so does this whole step. - name: Assert glibc / libstdc++ floor - if: matrix.target == 'x86_64-unknown-linux-gnu' + # BOTH linux-gnu targets. Adding a shipped target without extending + # this gate would leave it asserted for one architecture and merely + # hoped-for on the other. + if: matrix.target == 'x86_64-unknown-linux-gnu' || matrix.target == 'aarch64-unknown-linux-gnu' shell: bash env: - BIN_PATH: target/x86_64-unknown-linux-gnu/release/loom + BIN_PATH: target/${{ matrix.target }}/release/loom MAX_GLIBC: "2.35" MAX_GLIBCXX: "3.4.30" run: | @@ -143,10 +163,12 @@ jobs: # failure ourselves instead of shipping it. The runner is ubuntu-22.04, so # a successful run here is direct evidence for the case that failed. - name: Smoke-run the binary (proves it loads on ubuntu-22.04) - if: matrix.target == 'x86_64-unknown-linux-gnu' + # Runs natively on both linux runners, so each architecture's binary + # is executed on the image it is built for — not merely inspected. + if: matrix.target == 'x86_64-unknown-linux-gnu' || matrix.target == 'aarch64-unknown-linux-gnu' shell: bash env: - BIN_PATH: target/x86_64-unknown-linux-gnu/release/loom + BIN_PATH: target/${{ matrix.target }}/release/loom run: | set -euo pipefail echo "runner glibc: $(ldd --version | head -1)" diff --git a/.github/workflows/verification-gate.yml b/.github/workflows/verification-gate.yml index 44918bd..56008d9 100644 --- a/.github/workflows/verification-gate.yml +++ b/.github/workflows/verification-gate.yml @@ -14,10 +14,65 @@ permissions: pull-requests: write jobs: + # #353 — THE job whose green run carries a claim, split out so it can + # actually produce one. + # + # `TEST-RULE-SOLVER-DIFFERENTIAL` asserts that the incumbent solver and the + # certificate-checked engine agree on every rule obligation: under + # `LOOM_VERIFY_BACKEND=both` any divergence panics, so THE RUN PASSING IS + # THE ASSERTION. That claim was riding behind 30-plus other artifacts in the + # sweep below, inheriting both their runtime and their verdict — 0 green + # runs in 60 over six weeks, every one over the 30-minute budget, floor + # 30.4 minutes. A check that cannot go green is the mirror image of #332's + # check that could not go red, and it was reported as green-adjacent noise + # for long enough that a release shipped past it. + # + # This job builds one test binary and runs one filter. It is small enough to + # finish, which is the whole point: it is the one that should be REQUIRED on + # main. + solver-differential: + name: Solver differential (both engines must agree) + runs-on: [self-hosted, linux, x64, rust-cpu] + # 45, not 25. The sweep's observed FLOOR was 30.4 minutes for a build plus + # 23 artifacts, which puts the build alone near 20 — so a 25-minute budget + # here would be tight on a warm cache and impossible on a cold one. Setting + # a budget the job might not meet is the precise mistake this change + # exists to correct, and it would be a poor one to repeat in the fix. + timeout-minutes: 45 + env: + CARGO_TERM_COLOR: always + CARGO_INCREMENTAL: 0 + Z3_SYS_Z3_HEADER: /usr/include/z3.h + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - uses: Swatinem/rust-cache@v2 + - name: Ensure Z3 header present + run: | + if [ ! -f "$Z3_SYS_Z3_HEADER" ]; then + sudo apt-get update && sudo apt-get install -y libz3-dev || true + fi + - name: Both engines must agree on every rule obligation + env: + LOOM_VERIFY_BACKEND: both + run: | + set -euo pipefail + # Divergence panics, so a clean exit IS the no-divergence assertion. + cargo test --release --lib -p loom-core --features verification -- \ + test_verify_all_rules + rivet-verification: name: Verification Gate (rivet-driven) runs-on: [self-hosted, linux, x64, rust-cpu] - timeout-minutes: 30 + # #353: raised from 30. Observed durations for this sweep ran 30.4-102.5 + # minutes against a 30-minute cap, so EVERY run was killed — the minimum + # exceeded the budget by 24 seconds. A budget the floor cannot meet is not + # a budget, it is a guaranteed cancellation wearing one. + # + # This sweep is broad and advisory by nature; the claim-bearing check is + # the dedicated job above. Raising this lets it finish and REPORT, which is + # what makes its failures readable instead of ambient. + timeout-minutes: 120 env: CARGO_TERM_COLOR: always RUSTFLAGS: -D warnings diff --git a/loom-cli/src/main.rs b/loom-cli/src/main.rs index 808abbe..6284c24 100644 --- a/loom-cli/src/main.rs +++ b/loom-cli/src/main.rs @@ -400,9 +400,19 @@ fn write_validated_output( fn maybe_differential_gate( original: Option<&[u8]>, - optimized_wasm: &[u8], - output_path: &str, + // Underscored: these are read only inside the `differential` cfg block + // below, so without that feature they are genuinely unused. The + // verification gate builds with `RUSTFLAGS: -D warnings`, which turned + // three such warnings into hard errors and stopped `loom-cli` compiling + // there at all — so every artifact whose evidence is a `cargo test -p + // loom-cli` invocation failed, while being marked `verified`. The + // warnings were long-standing and looked ignorable in a normal build; + // they were only ever visible in the one environment that had not + // completed a run in six weeks (#353). + #[cfg_attr(not(feature = "differential"), allow(unused_variables))] optimized_wasm: &[u8], + #[cfg_attr(not(feature = "differential"), allow(unused_variables))] output_path: &str, ) -> Result<()> { + #[cfg_attr(not(feature = "differential"), allow(unused_variables))] let original = match original { Some(o) => o, None => return Ok(()), diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index 77ebfbe..515c50a 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -1264,3 +1264,68 @@ artifacts: target: REQ-14 - type: verifies target: REQ-3 + + - id: TEST-AARCH64-LINUX-RELEASE-TARGET + type: feature + title: aarch64-unknown-linux-gnu is built, gated and shipped like every other Linux target + description: > + PARTIALLY EVIDENCED. One of the four criteria below is now proven and + three are not, so this stays `draft`. + PROVEN (PR #364 CI): the `Build (ubuntu-22.04-arm)` job ran and + SUCCEEDED, which establishes the three things that were actually in + doubt — that arm64 Linux runners are available to this repository, that + `z3-sys` compiles its vendored C++ natively on ARM, and that loom builds + for the target at all. + NOT YET PROVEN: the three release-side criteria. The archive being + published, the glibc floor being asserted from the ARM binary's symbols, + and the binary being smoke-run all live in `release.yml`, which fires + only on a tag push. Their code is written and reviewed; none of it has + executed. Marking this `verified` on the CI job alone would assert + exactly the kind of untested gate the rest of this release exists to + remove, so it flips only after a tag has actually produced the asset. + v1.4.1 shipped four binaries: x86_64-linux, both macOS arches and + Windows. ARM Linux — servers, arm64 containers, ARM CI runners, single + board machines — had no binary at all and had to build from source with + a C++ toolchain, which is the dependency #313 exists to remove. The + earlier deferral note in the release workflow gave the reason as + "cross-compiling z3-sys for aarch64-linux is untested". That was true and + is now moot: the target builds NATIVELY on a GitHub-hosted arm64 Linux + runner, so nothing is cross-compiled, and those runners are free for + public repositories, which this one is. z3-sys vendors and statically + compiles z3, so no host libz3 is needed on any runner, ARM included. + The load-bearing decision is WHERE the evidence lives. `release.yml` + only fires on a tag push, so adding the target there alone would ship it + on the strength of a job that had never run — the unexercised-gate shape + this repository keeps finding, and the one v1.4.1 exists to punish. The + target is therefore also built on EVERY PR via the CI matrix, so a + toolchain or z3-sys regression on ARM fails a check immediately rather + than during a release. + Both #311 gates are extended to the new target rather than left + x86_64-only: the glibc/libstdc++ floor is ASSERTED from the ARM binary's + own symbols, and the binary is SMOKE-RUN natively on the ARM image it + was built for. A shipped target whose floor is merely hoped-for is how + v1.2.0 went out unloadable. + fields: + method: automated-test + acceptance-criteria: + - "PROVEN: given any PR, the aarch64-linux build runs and succeeds in CI" + - "PENDING A TAG: an aarch64-unknown-linux-gnu archive is published alongside the others" + - "PENDING A TAG: the ARM binary's glibc/libstdc++ floor is asserted from its own symbols, fail-closed" + - "PENDING A TAG: the ARM binary is executed on the ARM runner, not merely inspected" + # No `steps:` deliberately. Every criterion below is either evidenced by + # a CI job that this artifact cannot re-run from inside the gate, or is + # PENDING A TAG and has no command that can pass yet. An earlier draft of + # this artifact carried `gh release view ...` — a literal + # placeholder, and `` is shell redirection, so the command could + # never succeed. That would have made the verification gate permanently + # red on account of work that is correctly marked unfinished, which is + # the failure #353 is about. An artifact with no steps is SKIPPED, which + # is the honest state for one that is not yet verifiable. + status: draft + release: v1.5.0 + tags: [v150, release-engineering, portability] + links: + - type: verifies + target: REQ-18 + - type: verifies + target: REQ-12 diff --git a/tools/run_verification.py b/tools/run_verification.py index 7cb5a40..2b53610 100755 --- a/tools/run_verification.py +++ b/tools/run_verification.py @@ -53,6 +53,23 @@ def rivet_list_ids(filter_sexp: str) -> list[str]: return [a["id"] for a in data.get("artifacts", [])] +def rivet_get_status(artifact_id: str) -> str: + """The artifact's lifecycle status, or "" when it declares none. + + Used to skip `draft` artifacts (#353). A draft describes work that is + deliberately unfinished; running its steps produces a red gate that + reports nothing except that the work is not done yet — which the status + field already says, more cheaply and without burning the budget. + """ + proc = subprocess.run( + ["rivet", "get", artifact_id, "--format", "json"], + capture_output=True, + text=True, + check=True, + ) + return json.loads(proc.stdout).get("status", "") or "" + + def rivet_get_steps(artifact_id: str) -> list[str]: proc = subprocess.run( ["rivet", "get", artifact_id, "--format", "json"], @@ -64,14 +81,51 @@ def rivet_get_steps(artifact_id: str) -> list[str]: return [s["run"] for s in data.get("fields", {}).get("steps", []) if "run" in s] +# How many lines of a failing step's output to echo. Enough for a Rust test +# summary plus the assertion that produced it; short enough that a dozen +# failures do not bury the run. +FAILURE_OUTPUT_LINES = 40 + + def run_one_step(cmd: str, shell: str) -> bool: - """Return True iff exit code is 0.""" + """Return True iff exit code is 0; on failure, echo the tail of the output. + + Output used to go to DEVNULL, so a failing artifact reported `✗ failed: + ` and nothing else. That is most of why this gate taught nobody + anything for six weeks (#353): the runs that were not cancelled produced a + verdict with no evidence attached, so the only way to learn why something + failed was to reproduce it by hand — and the environment differs from a + developer machine in exactly the ways that matter (`-D warnings`, a + different libz3, a different core count). + + A gate that says a thing failed without saying how is a weaker version of + the same problem as a gate that cannot fail at all. + """ proc = subprocess.run( [shell, "-c", cmd], - stdout=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True, + errors="replace", ) - return proc.returncode == 0 + if proc.returncode == 0: + return True + + output = (proc.stdout or "").rstrip().splitlines() + if output: + shown = output[-FAILURE_OUTPUT_LINES:] + if len(output) > FAILURE_OUTPUT_LINES: + print( + f" ---- last {FAILURE_OUTPUT_LINES} of {len(output)} output lines ----" + ) + else: + print(" ---- output ----") + for line in shown: + print(f" | {line}") + print(" ----------------") + else: + print(" (the command produced no output)") + return False def main() -> int: @@ -117,6 +171,20 @@ def main() -> int: result.total = len(ids) for artifact_id in ids: + # #353: a `draft` artifact is unfinished BY DECLARATION. Executing its + # steps can only fail, and a gate that is red because planned work is + # planned is indistinguishable from a gate that is red because + # something broke. The status field already carries that information. + try: + if rivet_get_status(artifact_id) == "draft": + print(f"[SKIP] {artifact_id} (draft — not claimed verified)") + result.skipped.append(artifact_id) + continue + except subprocess.CalledProcessError as e: + print(f"[FAIL] {artifact_id}: rivet get failed: {e.stderr}") + result.failed.append(artifact_id) + continue + try: steps = rivet_get_steps(artifact_id) except subprocess.CalledProcessError as e: