From e40872231b08c0312b84872c2d894974746d080e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 06:45:01 +0200 Subject: [PATCH 1/3] chore(release): v1.3.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proof-carrying output, a trap gate on the runtime path, the first tier of the solver migration, and a Linux binary that loads on the runners people use. Version 1.2.0 -> 1.3.0 (minor: new output artifact + new verification backend, no breaking API change). Release scope closed in rivet — `rivet release status v1.3.0` reports cuttable, 3 artifacts, all verified: - TEST-WSC-FACTS-EMITTER (new) #231 proof-carrying facts + wsc.* trust boundary - TEST-RULE-SOLVER-DIFFERENTIAL (new) #277 rule verifier on a certificate-checked solver - TEST-TRAP-GATE-RUNTIME-PATH #288 gate proven to be the runtime authority The two new artifacts close a traceability gap the release gate found: both features had shipped with passing tests but no requirement->verification node. Also fixes #311: the v1.2.0 linux-gnu binary required GLIBC 2.38 / GLIBCXX 3.4.31 (reproduced from the shipped artifact) and would not load on ubuntu-22.04. Pinned the build image and ASSERTED the floor, because the cranelift-isle pin proved that a comment does not hold a pin in place. Measured, re-run rather than quoted: 38/38 rules proven (identical under both engines; `both` mode panics on divergence and did not), 10 wsc.facts tests, 481 pass / 0 fail / 2 ignored. Fixes #311 Verifies TEST-WSC-FACTS-EMITTER Verifies TEST-RULE-SOLVER-DIFFERENTIAL Refs #231 Refs #277 Refs #288 --- .github/workflows/release.yml | 44 +++++++++++++- CHANGELOG.md | 82 ++++++++++++++++++++++++++ Cargo.toml | 2 +- safety/requirements/verification.yaml | 84 +++++++++++++++++++++++++++ 4 files changed, 210 insertions(+), 2 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 8ce3ad8..cafda1e 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -46,8 +46,17 @@ jobs: fail-fast: false matrix: include: + # #311: pinned, NOT `ubuntu-latest`. The runner image sets the glibc + # floor of the shipped binary, and `ubuntu-latest` silently follows + # GitHub's newest image — which is how v1.2.0 shipped requiring GLIBC + # 2.38 and failed to load on ubuntu-22.04 (2.35) with an + # unresolved-symbol dump rather than a usable message. A comment alone + # is not enough: the cranelift-isle pin was re-floated by a dependency + # bump for exactly this reason, so the floor is ASSERTED after the + # build below. Raising this image is a deliberate act that must also + # raise the asserted ceiling. - target: x86_64-unknown-linux-gnu - os: ubuntu-latest + os: ubuntu-22.04 archive: tar.gz binary: loom # x86_64-apple-darwin cross-compiles on the arm64 macos-14 @@ -80,6 +89,39 @@ jobs: - name: Build loom (native) run: cargo build --release --target ${{ matrix.target }} -p loom-cli + # #311: assert the runtime floor instead of trusting the pin above. + # The ceiling is what ubuntu-22.04 provides; if the image is raised, or a + # dependency starts requiring newer symbols, this fails the RELEASE rather + # than shipping a binary that dies in the dynamic linker at the consumer. + # 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' + shell: bash + env: + BIN_PATH: target/x86_64-unknown-linux-gnu/release/loom + MAX_GLIBC: "2.35" + MAX_GLIBCXX: "3.4.30" + run: | + set -euo pipefail + vers=$(readelf -V "$BIN_PATH") + need_glibc=$(printf '%s' "$vers" | grep -oE 'GLIBC_2\.[0-9]+' | sed 's/GLIBC_//' | sort -V | tail -1) + need_cxx=$(printf '%s' "$vers" | grep -oE 'GLIBCXX_3\.4\.[0-9]+' | sed 's/GLIBCXX_//' | sort -V | tail -1 || true) + echo "requires GLIBC ${need_glibc:-none} / GLIBCXX ${need_cxx:-none}" + echo "ceiling GLIBC ${MAX_GLIBC} / GLIBCXX ${MAX_GLIBCXX} (ubuntu-22.04)" + fail=0 + if [ -n "${need_glibc:-}" ] && \ + [ "$(printf '%s\n%s\n' "$MAX_GLIBC" "$need_glibc" | sort -V | tail -1)" != "$MAX_GLIBC" ]; then + echo "::error::binary requires GLIBC $need_glibc > $MAX_GLIBC — will not load on ubuntu-22.04 (#311)" + fail=1 + fi + if [ -n "${need_cxx:-}" ] && \ + [ "$(printf '%s\n%s\n' "$MAX_GLIBCXX" "$need_cxx" | sort -V | tail -1)" != "$MAX_GLIBCXX" ]; then + echo "::error::binary requires GLIBCXX $need_cxx > $MAX_GLIBCXX — will not load on ubuntu-22.04 (#311)" + fail=1 + fi + exit "$fail" + - name: Strip binary if: runner.os != 'Windows' run: strip "target/${{ matrix.target }}/release/${{ matrix.binary }}" 2>/dev/null || true diff --git a/CHANGELOG.md b/CHANGELOG.md index b110a18..0ef7773 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,88 @@ All notable changes to LOOM will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [1.3.0] - 2026-08-04 + +Proof-carrying output, a trap gate that is actually on the runtime path, and the +first tier of the solver migration. + +Every figure below was measured on this tree, not quoted from a prior report. + +### Added + +- **Proof-carrying `wsc.facts` output (#231, P1).** loom no longer discards the + invariants its validator discharges — it emits them as a custom section for the + downstream ahead-of-time compiler, which re-proves its own specialization + *under* the fact rather than trusting it. Two properties are load-bearing and + both are asserted by tests: facts are attached to **values** (an index-keyed + fact is silently re-pointed by the next renumbering pass, which is a + correctness bug — a dropped fact only costs performance), and the schema-v1 + wire format is asserted **byte-for-byte** against the consumer's frozen + encoding so producer and consumer cannot drift. With no facts present the + output is byte-identical to the previous encoder. +- **`wsc.*` namespace trust boundary (#231).** loom now strips the loom-owned + `wsc.*` namespace from input on re-emit, **unconditionally** — including on the + facts-off default path. Previously an inherited, stale or forged `wsc.facts` + in the input survived re-encode and, under the consumer's first-wins rule, + could preempt or masquerade as facts loom had actually proved. A tool that + emits trusted metadata into a namespace has to own that namespace on input. + +### Changed + +- **Trap-equivalence gate wired onto the runtime path (#288, closing #279).** + The systemic gate added in 1.2.x shipped with passing unit tests, green CI and + **zero callers** — it provided no runtime protection, while the per-pass static + guards it was described as superseding were still the only thing standing. + `trap_backstop::accept_div_const_folds` is now invoked by the `constant_folding` + pass and reverts any div/rem constant-fold whose trap-freedom cannot be proven. + The regression test bypasses the static guard in-test and asserts that the + **gate** blocks a trapping fold, so it fails if the gate ever leaves the runtime + path again. +- **All four integer div/rem forms are now gated (#290).** `div_s`, `div_u`, + `rem_u` and — once the upstream solver stopped over-approximating its overflow + trap — `rem_s`. The static guards are retained as a feature-independent floor; + the gate is additive, so behaviour with the `verification` feature off is + unchanged. +- **Algebraic rule verifier migrated to a certificate-checked solver (#277, + Tier-1).** The rule verifier now runs behind a swappable backend + (`LOOM_VERIFY_BACKEND=z3|ordeal|both`) on a pure-Rust QF_BV engine that + re-checks each `Unsat` certificate before the verdict is believed. Measured: + **38/38 rules proven (100.0%)**, reported identically by both engines; in + `both` mode the harness runs both per obligation and panics on any divergence + — it did not. + +### Fixed + +- **Linux release binary loads on ubuntu-22.04 again (#311).** v1.2.0's + `x86_64-unknown-linux-gnu` artifact required **GLIBC 2.38** and **GLIBCXX + 3.4.31** and died in the dynamic linker on ubuntu-22.04 (GLIBC 2.35) — an + unresolved-symbol dump for a binary the consumer had just downloaded and + checksummed, with nothing pointing at the real cause. The build ran on + `ubuntu-latest`, so the floor silently tracked GitHub's newest image. Pinned + to `ubuntu-22.04`, and the floor is now **asserted after the build** (the + release fails rather than shipping an unloadable binary) because a pin plus a + comment is exactly what a later "modernize the runners" edit undoes. The + libstdc++ coupling comes from linking Z3; it goes away with the solver + migration. +- **`wasm32-wasip2` build restored (#304).** A dependency bump had re-floated the + `cranelift-isle` constraint past the pin documented directly above it, pulling a + version whose MSRV exceeds the toolchain CI runs; the wasm build had been red + since. Re-pinned to the known-good line. + +### Not done — stated so it is not implied + +- The core translation validator still proves **value equivalence over a total + operation model**; trap preservation is a gate beside it plus static guards, + not the encoding. Refinement with traps as first-class state (#300) is + specified, not implemented — until it lands, a newly added rewrite is + trap-unsafe by default. +- The trap gate covers division and remainder. The memory-discard and + select-arm-discard fold sites remain on their static guards. +- The `wsc.facts` **emitter** is complete and byte-verified; the fact *source* + that would populate it at volume is not yet wired. +- Only the rule verifier has been migrated. The core verifier is still on the + incumbent solver. + ## [1.2.0] - 2026-07-14 Correctness backstop + trap preservation + algebraic mid-end. diff --git a/Cargo.toml b/Cargo.toml index dc81e29..79f0149 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ members = [ ] [workspace.package] -version = "1.2.0" +version = "1.3.0" authors = ["PulseEngine "] edition = "2024" license = "Apache-2.0" diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index cc38b95..cf07f7c 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -440,6 +440,7 @@ artifacts: - run: | cargo test --release --lib -p loom-core --features verification -- test_288_ trap_gate::tests::div_discard trap_gate::tests::rem status: verified + release: v1.3.0 tags: [v122, verification, trap-gate, safety] links: - type: verifies @@ -454,3 +455,86 @@ artifacts: target: CC-4 - type: verifies target: CC-20 + + # ============================================================================ + # #231 — proof-carrying facts. loom does not discard the invariants its + # validator discharges: it emits them for the downstream AOT compiler, which + # re-proves its own specialization UNDER the fact rather than trusting it. + # Two properties are load-bearing and both are asserted here: facts are + # attached to VALUES (an index-keyed fact is silently re-pointed by the next + # renumbering pass), and loom OWNS the `wsc.*` namespace on input (an + # inherited or forged section must never be re-emitted as though loom had + # proved it). + # ============================================================================ + + - id: TEST-WSC-FACTS-EMITTER + type: feature + title: proof-carrying wsc.facts emitter + wsc.* trust boundary (#231 P1) + description: > + Verifies the producer side of the wsc.facts channel. Golden-bytes: the + schema-v1 value-range encoding is asserted byte-for-byte against the + consumer's frozen wire format, so producer and consumer cannot drift. + Drop-safety: a fact whose value_id is out of range for the final body, or + which names an imported/nonexistent function, is DROPPED — never emitted + against a different operator (a mis-keyed fact is a correctness bug, an + absent one only costs performance). Identity: with facts absent the + encoder output is byte-identical to the default path. Trust boundary: an + input `wsc.facts` is stripped UNCONDITIONALLY on re-emit — including on + the facts-off default path — so an inherited or forged section can never + preempt (first-wins) or masquerade as facts loom proved this run; + non-`wsc.*` custom sections still round-trip. Under-P discharge: a range + premise licenses a fits-below-bit obligation, and an insufficient premise + does not. + fields: + method: automated-test + steps: + - run: | + cargo test --release --lib -p loom-core --features verification -- wsc_facts + status: verified + release: v1.3.0 + tags: [v130, verification, proof-carrying-facts] + links: + - type: verifies + target: REQ-12 + - type: verifies + target: REQ-14 + - type: verifies + target: REQ-5 + + # ============================================================================ + # #277 — Tier-1 of the solver migration. The algebraic rule verifier runs on + # our own certificate-checked QF_BV engine, with the incumbent kept as a + # differential oracle. The evidence is not a summary line: in `both` mode the + # harness runs BOTH engines on every obligation and PANICS on any divergence, + # so a green run is the assertion. + # ============================================================================ + + - id: TEST-RULE-SOLVER-DIFFERENTIAL + type: feature + title: algebraic rule verifier on a certificate-checked solver, differentially cross-checked (#277 Tier-1) + description: > + Verifies that loom's algebraic rewrite rules are discharged by a swappable + solver backend (LOOM_VERIFY_BACKEND = z3 | ordeal | both) and that the two + engines agree. The rule verifier reports 38/38 rules proven (100.0%) under + the incumbent AND under our own engine, which additionally re-checks each + UNSAT certificate (LRAT) before the verdict is believed. In `both` mode the + differential solver runs both engines per obligation and panics on any + disagreement; the suite passing IS the no-divergence assertion. Scope: this + is the rule verifier only — the core translation validator has not been + migrated, and that gap is stated in the release notes rather than implied + to be closed. + fields: + method: automated-test + steps: + - run: | + LOOM_VERIFY_BACKEND=both cargo test --release --lib -p loom-core --features verification -- test_verify_all_rules + status: verified + release: v1.3.0 + tags: [v130, verification, solver-migration] + links: + - type: verifies + target: REQ-6 + - type: verifies + target: REQ-1 + - type: verifies + target: REQ-4 From d0db5fdc2b5912165efe19014c111f2e21a60e9f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 07:25:55 +0200 Subject: [PATCH 2/3] fix(release): make the #311 floor gate fail-closed + actually load the binary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two changes, both because the consumer who reported #311 tests only released artifacts in CI — they cannot catch a bad build before we publish, so the release workflow has to be the thing that catches it. 1. FAIL-CLOSED. The first draft guarded each comparison with `[ -n "$need" ]`, so a readelf that produced no match (missing tool, changed output, wrong path) skipped the comparison and the step went green having tested nothing. That is the vacuous-check defect this repo keeps finding, reintroduced in the gate written to prevent a recurrence. A dynamically linked gnu binary always requires some GLIBC version; finding none now means the probe broke, and the step errors instead of passing. 2. SMOKE-RUN. The symbol check is static reasoning about the binary; this executes it. The runner is ubuntu-22.04, so `loom --version` succeeding there is direct evidence for the exact case that failed in #311, rather than an inference from symbol tables. Verified by replay against the shipped v1.2.0 artifact (which requires GLIBC 2.38): the gate reports CAUGHT — the release would have failed instead of publishing an unloadable binary. Comparison logic checked at 2.34 / 2.35 / 2.38 / 2.39 against the 2.35 ceiling. Refs #311 --- .github/workflows/release.yml | 39 +++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index cafda1e..5eb61aa 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -104,14 +104,28 @@ jobs: MAX_GLIBCXX: "3.4.30" run: | set -euo pipefail + # FAIL-CLOSED. An earlier draft of this step guarded each comparison + # with `[ -n "$need" ]`, so a readelf that produced no match — missing + # tool, changed output, wrong path — skipped the comparison and the + # step went green having tested nothing. That is the same vacuous-check + # defect this repo keeps finding (a gate that cannot fail looks exactly + # like a gate that passed), so: if the floor cannot be DETERMINED, that + # is an error, not a pass. + command -v readelf >/dev/null || { echo "::error::readelf missing — cannot determine floor"; exit 1; } + test -f "$BIN_PATH" || { echo "::error::binary not found at $BIN_PATH"; exit 1; } vers=$(readelf -V "$BIN_PATH") - need_glibc=$(printf '%s' "$vers" | grep -oE 'GLIBC_2\.[0-9]+' | sed 's/GLIBC_//' | sort -V | tail -1) + need_glibc=$(printf '%s' "$vers" | grep -oE 'GLIBC_2\.[0-9]+' | sed 's/GLIBC_//' | sort -V | tail -1 || true) need_cxx=$(printf '%s' "$vers" | grep -oE 'GLIBCXX_3\.4\.[0-9]+' | sed 's/GLIBCXX_//' | sort -V | tail -1 || true) - echo "requires GLIBC ${need_glibc:-none} / GLIBCXX ${need_cxx:-none}" + # A dynamically linked gnu binary always requires some GLIBC version. + # Finding none means the probe broke, not that the binary is portable. + if [ -z "${need_glibc:-}" ]; then + echo "::error::could not determine the GLIBC requirement — probe broken, refusing to pass vacuously" + exit 1 + fi + echo "requires GLIBC ${need_glibc} / GLIBCXX ${need_cxx:-none}" echo "ceiling GLIBC ${MAX_GLIBC} / GLIBCXX ${MAX_GLIBCXX} (ubuntu-22.04)" fail=0 - if [ -n "${need_glibc:-}" ] && \ - [ "$(printf '%s\n%s\n' "$MAX_GLIBC" "$need_glibc" | sort -V | tail -1)" != "$MAX_GLIBC" ]; then + if [ "$(printf '%s\n%s\n' "$MAX_GLIBC" "$need_glibc" | sort -V | tail -1)" != "$MAX_GLIBC" ]; then echo "::error::binary requires GLIBC $need_glibc > $MAX_GLIBC — will not load on ubuntu-22.04 (#311)" fail=1 fi @@ -122,6 +136,23 @@ jobs: fi exit "$fail" + # #311: the symbol check above is static reasoning about the binary. This + # actually LOADS it. The consumer who reported #311 only tests released + # artifacts in CI, so they cannot catch a bad build before we publish — + # which makes executing it here the last chance to see the dynamic-linker + # 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' + shell: bash + env: + BIN_PATH: target/x86_64-unknown-linux-gnu/release/loom + run: | + set -euo pipefail + echo "runner glibc: $(ldd --version | head -1)" + "$BIN_PATH" --version + "$BIN_PATH" --help >/dev/null + - name: Strip binary if: runner.os != 'Windows' run: strip "target/${{ matrix.target }}/release/${{ matrix.binary }}" 2>/dev/null || true From 316fd2859b9ed7e0fc66bb8a345a0ec068460012 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 19:08:01 +0200 Subject: [PATCH 3/3] fix(ci): re-pin cranelift-isle and stop automation re-floating it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dependabot #310 widened the workspace cranelift-isle constraint from 0.132 back to 0.134 — the second time this pin has been reverted by automation (#298 was the first, fixed in #304). Both times the bump left the comment directly above the constraint intact, a comment whose text explains exactly why not to widen it. main's wasm32-wasip2 build is red again as a result, and because these PRs auto-merge, no human saw the warning on either occasion. A pin defended only by prose is not defended. Two changes: - Re-pin to ^0.132 (0.133+ needs rustc 1.94.0, not stable on the CI image). - Add a dependabot "ignore" entry for cranelift-isle on the root cargo ecosystem, so the bot cannot propose the change at all. The removal condition is written next to it: stable rustc 1.94, or the committed lockfile (#142). This is the mechanical half of the same lesson as the release floor gate in this branch — an invariant that only exists in a comment will be undone by something that does not read comments. Refs #142, #304, #311 --- .github/dependabot.yml | 16 ++++++++++++++++ Cargo.toml | 2 +- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/.github/dependabot.yml b/.github/dependabot.yml index 0cac770..ed48070 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -12,6 +12,22 @@ updates: interval: weekly labels: - dependencies + ignore: + # cranelift-isle is PINNED to the 0.132.x line: 0.133+ raises its MSRV to + # rustc 1.94.0, which is not yet stable, so a wider constraint breaks the + # wasm32-wasip2 build and reddens main. + # + # This entry exists because the pin was re-floated TWICE by automation + # (#298 → fixed in #304, then #310 again) — both times past a comment in + # Cargo.toml that explained precisely why not to. Dependabot does not read + # comments, and these PRs auto-merge, so no human saw the warning either + # time. A pin defended only by prose is not defended; this makes it + # mechanical. + # + # Remove this ignore ONLY when rustc 1.94 is stable on the CI image, or + # when the lockfile is committed (#142) — and raise the release workflow's + # asserted glibc ceiling in the same change if the runner image moves. + - dependency-name: cranelift-isle - package-ecosystem: cargo directory: /fuzz schedule: diff --git a/Cargo.toml b/Cargo.toml index 79f0149..3ab2708 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -32,7 +32,7 @@ wit-component = "0.255" # rustc 1.94.0) and reddened the wasm32-wasip2 build again — re-pinned here. Do # not widen the `^0.132` constraint without a stable rustc 1.94 or the committed # lockfile (#142); the float is what keeps reintroducing this red. -cranelift-isle = "0.134" +cranelift-isle = "0.132" # CLI clap = { version = "4.5", features = ["derive", "cargo"] }