From 535698248eb60a12475b27591207e5542138e928 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 06:12:19 +0200 Subject: [PATCH 1/2] feat(ci): build and ship aarch64-unknown-linux-gnu MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v1.4.1 shipped four binaries — x86_64-linux, both macOS arches, Windows. ARM Linux had none: servers, arm64 containers, ARM CI runners and single board machines all had to build from source with a C++ toolchain, which is the dependency #313 exists to remove. The deferral note in release.yml 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. z3-sys vendors and statically compiles z3, so it needs no host libz3 on any runner, ARM included, and those runners are free for public repositories — which this one is. --- where the evidence lives is the load-bearing decision --- `release.yml` only fires on a tag push. A target added THERE ALONE would ship on the strength of a job that had never run: the unexercised-gate shape this repository keeps finding, and precisely what v1.4.1 was cut to punish. So the target is also built on EVERY PR via the CI matrix, and a toolchain or z3-sys regression on ARM fails a check immediately instead of surfacing during a release. --- both #311 gates extended, not left x86_64-only --- The glibc/libstdc++ floor is now asserted from the ARM binary's OWN symbols (the step no longer hardcodes the x86_64 path), and the binary is SMOKE-RUN natively on the ARM image it was built for rather than merely inspected. A shipped target whose floor is only hoped-for is exactly how v1.2.0 went out unloadable. The rivet artifact is deliberately `draft`, not `verified`: the workflow edit is not evidence. It flips when the ARM job has actually run green. Refs #311, #313 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RZof1M5HMBSYVZPeoT4MEn --- .github/workflows/ci.yml | 9 ++++- .github/workflows/release.yml | 38 ++++++++++++++++----- safety/requirements/verification.yaml | 49 +++++++++++++++++++++++++++ 3 files changed, 87 insertions(+), 9 deletions(-) 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/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index 77ebfbe..9ac49a5 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -1264,3 +1264,52 @@ 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: > + PLANNED — status flips to verified once the ARM build has actually run + green, not on the strength of the workflow edit. + 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: + - "Given any PR, the aarch64-linux build runs and succeeds in CI" + - "Given a release tag, an aarch64-unknown-linux-gnu archive is published alongside the others" + - "Given the ARM binary, its glibc/libstdc++ floor is asserted from its own symbols, fail-closed" + - "Given the ARM binary, it 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 --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 From e4c0ac86a402b8aef17a018fe230d5d88a808284 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 06:29:10 +0200 Subject: [PATCH 2/2] chore(rivet): record what the ARM job proved, and what it did not MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Build (ubuntu-22.04-arm)` ran green on PR #364. That settles the three things actually in doubt: arm64 Linux runners are available to this repository, z3-sys compiles its vendored C++ natively on ARM, and loom builds for the target. It settles nothing about the release path. Publishing the archive, asserting the glibc floor from the ARM binary's symbols, and smoke-running it all live in release.yml, which fires only on a tag push. That code is written and reviewed; none of it has executed. So the artifact stays `draft` with each criterion labelled PROVEN or PENDING A TAG. Flipping it to `verified` on the strength of the CI job would assert an untested gate — the exact defect class v1.4.1 was cut to remove, and it would be a poor way to celebrate that. Refs #311, #313 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RZof1M5HMBSYVZPeoT4MEn --- safety/requirements/verification.yaml | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index 9ac49a5..84bc1c2 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -1269,8 +1269,20 @@ artifacts: type: feature title: aarch64-unknown-linux-gnu is built, gated and shipped like every other Linux target description: > - PLANNED — status flips to verified once the ARM build has actually run - green, not on the strength of the workflow edit. + 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 @@ -1296,10 +1308,10 @@ artifacts: fields: method: automated-test acceptance-criteria: - - "Given any PR, the aarch64-linux build runs and succeeds in CI" - - "Given a release tag, an aarch64-unknown-linux-gnu archive is published alongside the others" - - "Given the ARM binary, its glibc/libstdc++ floor is asserted from its own symbols, fail-closed" - - "Given the ARM binary, it is executed on the ARM runner, not merely inspected" + - "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'