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

[avrabe]

v1.4.1 shipped four binaries — x86_64-linux, both macOS arches, Windows. ARM Linux had none: servers, arm64 containers, ARM CI runners and SBCs all had to build from source with a C++ toolchain, which is the dependency #313 exists to remove.

The stated blocker no longer applies

release.yml carried this note:

No aarch64-linux for now: … cross-compiling z3-sys for aarch64-linux is untested.

True when written, and now moot. The target builds natively on a GitHub-hosted arm64 Linux runner — 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 repo 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. A toolchain or z3-sys regression on ARM now fails a check immediately, instead of surfacing during a release when it is most expensive.

This PR's own CI is that evidence. If the ubuntu-22.04-arm build is not green here, the release entry does not belong on main.

Both #311 gates extended, not left x86_64-only

• Floor assertion — now reads the ARM binary's own symbols; the step no longer hardcodes the x86_64 path. Still fail-closed: an undeterminable floor is an error, not a pass.
• Smoke run — the ARM binary is executed on the ARM image it was built for, not merely inspected.

A shipped target whose floor is only hoped-for is exactly how v1.2.0 went out unloadable.

Status is draft, deliberately

TEST-AARCH64-LINUX-RELEASE-TARGET is filed against v1.5.0 as draft, not verified. The workflow edit is not evidence. It flips when the ARM job has actually run green — and the release gate correctly reads ✗ NOT cuttable until then.

Refs #311, #313

[avrabe]

This PR now also addresses #353 — including my own contribution to it

#353 landed while this was open: the Verification Gate has 0 successful runs in 60 across six weeks, every run over its 30-minute cap (floor 30.4 min), on a main whose required_checks is empty.

I should own the part of that which is mine. I merged past this check repeatedly, calling it systemic alongside Rocq, including for the v1.4.1 release — whose two gate runs were cancelled at 30.5 and 39.2 minutes. #332 was a check that could not go red; this is a check that cannot go green. Same defect class, and treating it as ambient noise is how it survived six weeks.

I also made it measurably worse

The filter matches every TEST-* feature artifact. It matched 23 when #353 was measured; it matches 35 now, and 13 of those are mine from this week.

Worse, one of them — TEST-AARCH64-LINUX-RELEASE-TARGET, added in this PR — carried this as a verification step:

gh release view <tag> --json assets --jq '.assets[].name' | grep aarch64-unknown-linux-gnu

<tag> is a literal placeholder, and < is shell redirection. That command can never succeed. A draft artifact for correctly-unfinished work would have held the gate red on its own. That is almost certainly part of why this PR's gate is failing.

Three changes

1. solver-differential becomes its own job. TEST-RULE-SOLVER-DIFFERENTIAL is the artifact whose green run carries a claim — under LOOM_VERIFY_BACKEND=both any divergence panics, so the run passing is the no-divergence assertion. It was riding behind 30+ unrelated artifacts, inheriting their runtime and their verdict. Now one test binary, one filter, 45-minute budget — deliberately not 25, since the sweep's floor implies a ~20-minute build and setting a budget the job might miss is the exact mistake being corrected.

2. Sweep cap 30 → 120, so it can finish and report. Advisory by nature, but its failures should be readable rather than ambient — two of them (loom optimize smoke, measure_corpus) are real and were invisible behind six weeks of cancellations.

3. run_verification.py skips draft artifacts. A draft is unfinished by declaration; running its steps can only fail, and a gate red because planned work is planned cannot be told apart from a gate red because something broke.

Not claimed fixed

The gate has not yet gone green in CI. That is the only evidence that counts, and it arrives on this PR — which is the same standard I applied to the ARM build here.

Deliberately not done: making the differential job required on main. That changes merge policy and is your call, not a side effect of a CI edit. It is step 3 of what #353 asks for, and I'd rather ask than quietly tighten how the repo merges.