chore(release): v1.3.0 — proof-carrying output, trap gate on the runtime path, solver migration Tier-1, loadable Linux binary

.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:

.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,70 @@ 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
+          # 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 || true)
+          need_cxx=$(printf '%s' "$vers" | grep -oE 'GLIBCXX_3\.4\.[0-9]+' | sed 's/GLIBCXX_//' | sort -V | tail -1 || true)
+          # 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 [ "$(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"
+
+      # #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

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.

Cargo.toml

@@ -9,7 +9,7 @@ members = [
 ]
 
 [workspace.package]
-version = "1.2.0"
+version = "1.3.0"
 authors = ["PulseEngine <https://github.com/pulseengine>"]
 edition = "2024"
 license = "Apache-2.0"
@@ -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"] }

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