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

safety/requirements/verification.yaml

@@ -1264,3 +1264,64 @@ 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"
+      steps:
+        - run: |
+            gh run list --workflow ci.yml --limit 1 --json jobs --jq '.[].jobs[]|select(.name|test("ubuntu-22.04-arm"))|.conclusion'
+        - run: |
+            gh release view <tag> --json assets --jq '.assets[].name' | grep aarch64-unknown-linux-gnu
+    status: draft
+    release: v1.5.0
+    tags: [v150, release-engineering, portability]
+    links:
+      - type: verifies
+        target: REQ-18
+      - type: verifies
+        target: REQ-12