chore(release): v1.3.0 — proof-carrying output, trap gate on the runtime path, solver migration Tier-1, loadable Linux binary - #312
Open
avrabe wants to merge 3 commits into
Open
chore(release): v1.3.0 — proof-carrying output, trap gate on the runtime path, solver migration Tier-1, loadable Linux binary#312avrabe wants to merge 3 commits into
avrabe wants to merge 3 commits into
Conversation
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
…e binary 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
avrabe
force-pushed
the
chore/release-v1.3.0
branch
from
August 7, 2026 17:08
34fa677 to
dc37e5f
Compare
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
avrabe
force-pushed
the
chore/release-v1.3.0
branch
from
August 7, 2026 17:08
dc37e5f to
316fd28
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Cuts v1.3.0 (1.2.0 → 1.3.0 — minor: new output artifact + new verification backend, no breaking API change). First release in 24 days.
Scope — closed in rivet
rivet release status v1.3.0→ ✓ Cuttable, 3 artifacts, all verified.TEST-WSC-FACTS-EMITTER(new)wsc.*trust boundaryTEST-RULE-SOLVER-DIFFERENTIAL(new)TEST-TRAP-GATE-RUNTIME-PATHThe two new artifacts close a real gap the release gate surfaced: #231 and #277 had shipped with passing tests but no requirement→verification node, so the V was open for both.
rivet validatePASS (42 warnings — unchanged baseline); both new artifacts resolve in theverification-evidenceoracle.Fixes #311 — the Linux binary was unloadable
Reproduced from the shipped v1.2.0 artifact, not taken on report: it requires
GLIBC_2.38+GLIBCXX_3.4.31, so it dies in the dynamic linker on ubuntu-22.04 (2.35). Cause: the build ran onubuntu-latest, so the floor silently tracked GitHub's newest image.Fix is a pin plus an assertion —
ubuntu-22.04, and the floor is checked after the build so the release fails rather than shipping an unloadable binary. A pin with only a comment is precisely what a dependency bump undid to thecranelift-islepin last week; this one can't regress silently.Measured, not quoted
bothmode the harness panics on divergence and did not.Two inherited numbers failed re-measurement while preparing this and were corrected (a "57 rules" that measured 38; a stale test count) — both had come from a report rather than a run.
Not done — in the CHANGELOG, not implied closed
Core validator still proves value equivalence over a total model (refinement, #300, specified not built); trap gate covers div/rem only; the fact source is unwired; only the rule verifier has been migrated.
Known systemic reds:
Rocq Formal Proofs,Verification Gate.