feat(ci): build and ship aarch64-unknown-linux-gnu

.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

.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)"

.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

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(()),

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 <tag> ...` — a literal
+      # placeholder, and `<tag>` 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

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:
+    <command>` 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: