feat(#1000): ship 'synth verify' in released artifacts + non-vacuity smoke gate (RQ-58-SHIPVERIFY) - #1002
Merged
Conversation
…ategy line from a binary that cannot verify Red-first: tests/verify_banner_1000.rs (no required-features) fails on the pre-fix ordering — the incapable binary printed all four 'Translation validation:' lines including 'Strategy: Per-rule SMT verification (ASIL D path)' before bailing. Exit code was already correct (#124); now nothing verification-shaped precedes the failure. The verify half (wired into fact-spec-oracle) pins that a capable binary still prints the banner and ends in a real verdict. Also de-stales the 'via Z3' help line (measured: 0 z3 nodes under --features verify). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ity smoke gate (RQ-58-SHIPVERIFY) release.yml: all four platform builds now pass --features verify (pure-Rust ordeal since #553 — re-measured: 0 z3 nodes; the z3 differential oracle stays a separate synth-verify/z3-solver opt-in). The npm channel inherits the feature: the @pulseengine/synth wrapper downloads and checksum-verifies these same tarballs at install time. Non-vacuity gate: scripts/release_verify_smoke.sh runs against the binary EXTRACTED FROM EACH PACKAGED TARBALL (aarch64-linux under qemu-user; the x86_64 macOS tarball under Rosetta on the arm64 runner) — compiles a module, runs 'synth verify' on it, and asserts a real verdict (exit 0, verdict line, synth-verify-v1 report with >=1 verified / 0 failed). Red-first, demonstrated at authoring AND pinned in CI: the fact-spec-oracle job builds a verify-less binary and asserts the script FAILS with exactly the capability error, then re-runs it green on the verify build. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Aug 19, 2026
…ildcard was a LIVE executed miscompile (RQ-58-WILDCARD) (#1003) * fix(#946): i64-width vstack drift — if/br_if/br_table/memory.copy/call args never left the width stack The RQ-58-WILDCARD classification pass found the live hole the lane brief predicted, and it is worse than latent: an EXECUTED cross-shape miscompile. wasm_stack_effect listed If | BrIf | BrTable as (0, 0) although each pops one i32 (condition / table index), let the `_ => (0, 0)` wildcard absorb MemoryCopy/MemoryFill (which pop 3), and its Call row (0, 1) never popped call arguments. Every one of those stale entries shifts infer_i64_locals' width stack, so an i64 local set past one of these shapes was inferred i32, given a 4-byte slot and a single-word STR/LDR — hi half silently dropped. The inference is shared with the RV32 selector (#312), so the drift was cross-backend. Executed proof (unicorn vs wasmtime, cortex-m4 --relocatable --no-optimize), all returning (0x1_0000_0005 >> 32), expected 1: br_if shape -> 32 if shape -> 32 br_table shape -> 32 memory.copy shape -> 0 All four return 1 after the fix. Fix: * wasm_stack_effect: If | BrIf | BrTable -> (1, 0); MemoryCopy | MemoryFill -> (3, 0); the trailing `_ => (0, 0)` wildcard is GONE — the match is fully enumerated over all 279 WasmOp variants (SIMD rows stated per shape), so a new variant fails to COMPILE until its stack effect is stated (#615 expand-or-loud-reject pattern). * infer_i64_locals: pops call ARGUMENTS against the real arg-count tables (func_arg_counts / type_arg_counts, one slot per value — the decoder's unit) and call_indirect's table-index operand; empty tables degrade to the pre-#946 zero-arg approximation, matching lower_call's own #195 fallback. Signature threaded through compute_local_layout, both ARM call sites, and the RV32 selector (which has no type table; call_indirect is Unsupported there, so the empty slice cannot under-pop on anything that compiles). * Approximation residuals STATED, not hidden, at the structural row: post-Br/Return/Unreachable polymorphic tracking and the Else join (an if-with-result double-counts its result) need a control-frame-aware walk — named follow-up. Gates: * tests/i64_width_vstack_946.rs — 7 shape pins red on the pre-fix behavior (verified by temporary revert), 2 controls (i64-returning call #311, i32-stays-i32) green on both. * tests/selector_stack_effect_no_wildcard_946.rs — the #615-style tripwire (same scanner set as wcet_sp_no_wildcard_946.rs): no catch-all arm may regrow, every WasmOp variant must be NAMED in the body, count pinned 279, negative controls + verified red on an injected `_ =>` in the real function. * scripts/repro/i64_width_vstack_946.wat — the four executable shapes, picked up by the wired #973 ARM corpus sweep Phase B (ran locally: 4 exports x 12 vectors compared, 0 mismatches, sweep PASS with the EXPECTED_DECLINES exact-set unchanged); i64_width_vstack_mem_946.wat carries the memory.copy/fill shapes (memory section excludes it from Phase B — Phase A compile + unit pins cover it). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#946): loud-convert the silent last-variant maps + move the wildcard ratchet 56 -> 55 Classification-driven follow-through on the RQ-58-WILDCARD lane (the fix itself is the previous commit): * 8 silent-map refinements converted to expand-or-loud-reject: the six float inner matches whose `_ =>` silently lowered as the LAST variant (F32Div/F32Ge/F64Div/F64Sqrt/F64Ge/F64Nearest — a widened outer arm would have become a silent wrong lowering) now name the final variant and panic on drift; the two access-size fallbacks that silently widened any unexpected width to a WORD load/store now panic. Byte-identical by construction (whole workspace incl. all frozen anchors green, rc=0). Deliberately count-neutral: `_ => unreachable!()` still matches the ratchet regex, and swapping it for a bare-binding arm to game the count is exactly what the tripwire scanners flag. * claims.yaml: selector_wildcard_arms_code 56 -> 55 banked (value + baseline; the wasm_stack_effect wildcard is gone), arms_total 91 -> 90, lines_code 17,897 -> 17,991 with a bound waiver (the 279-variant enumeration + call-arg threading: lines traded for exhaustiveness, the trade this release wants), lines_total 28,495 -> 28,599. The remaining 55 arms' classification is recorded at the pin. status.json regenerated via --emit-status. * Ledger re-grades: RQ-58-WILDCARD proposed -> implemented (this lane); RQ-58-SHIPVERIFY proposed -> implemented (PR #1002 merged 2026-08-19 — the ledger had drifted behind the merge). * CLAUDE.md: the pin-rationale sentence kept v0.57 numbers as if live; now dated at pin creation with the live figures delegated to the pins. Gates: cargo test --workspace rc=0, clippy -D warnings clean, fmt --check clean, claim_check 49/49. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Sep 23, 2026
… every PR RQ-71-MUSL (#1349). Both refuting commands were re-run first and BOTH confirmed the premise: * the v0.70.0 x86_64 asset, downloaded and measured with the issue's own two commands — dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, max of 17 GLIBC_ symbols = GLIBC_2.39. The runner image did not move under us; * `grep musl .github/workflows/*.yml` — one hit, in fuzz-smoke.yml, and it is there to FORCE the GNU target. No musl release target existed. 2.39 excludes Ubuntu 22.04, Debian 12, RHEL 9, Amazon Linux 2023, Ubuntu 20.04 and Alpine entirely. These feed the varve `pulseengine` rolling layer, whose portability is the MAXIMUM floor across its payloads — one payload sets it for everything pinned beside it. `x86_64-unknown-linux-musl`, statically linked: no loader, no glibc floor at all rather than a lower one. ADDITIVE — the gnu assets keep their names, consumers and attestation path, so nothing that works today changes. THE PART THAT IS NOT PLUMBING. release.yml runs only on a TAG PUSH, so a target added there is unverified until the tag, and editing the release workflow between an RC and its tag is the unreviewed late change this process exists to prevent. So a per-PR job (`musl-portable-asset`) builds the same target with the same feature set and runs the issue's two acceptance commands on the result: statically linked, no interpreter, ZERO GLIBC_ symbols. WITH A POTENCY CONTROL, because those assertions could pass on anything: the same job builds the GNU target on the same runner and asserts they FAIL there. A FALSE DOC STATEMENT FOUND ON THE WAY, corrected in place. `docs/release-process.md` said the `verify` feature is "not" enabled in release builds and that enabling it "remains a deliberate follow-up decision". It was taken in v0.58 (RQ-58-SHIPVERIFY #1000/#1002, which put `--features verify` on both build lines), so the sentence had been false for thirteen releases. Measured on the shipped v0.70.0 asset: 20 `ordeal` strings, ZERO occurrences of the degraded-path message. RESIDUAL, NAMED: arm64 Linux is still glibc-floored. Only the x86_64 musl asset is published; aarch64-unknown-linux-musl needs the cross path and its own measurement, and is not claimed. Refs #1349
avrabe
added a commit
that referenced
this pull request
Sep 23, 2026
…n every PR — and correct a release doc that has been false since v0.58 (#1357) * feat(musl): publish a static musl Linux asset, and prove it builds on every PR RQ-71-MUSL (#1349). Both refuting commands were re-run first and BOTH confirmed the premise: * the v0.70.0 x86_64 asset, downloaded and measured with the issue's own two commands — dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, max of 17 GLIBC_ symbols = GLIBC_2.39. The runner image did not move under us; * `grep musl .github/workflows/*.yml` — one hit, in fuzz-smoke.yml, and it is there to FORCE the GNU target. No musl release target existed. 2.39 excludes Ubuntu 22.04, Debian 12, RHEL 9, Amazon Linux 2023, Ubuntu 20.04 and Alpine entirely. These feed the varve `pulseengine` rolling layer, whose portability is the MAXIMUM floor across its payloads — one payload sets it for everything pinned beside it. `x86_64-unknown-linux-musl`, statically linked: no loader, no glibc floor at all rather than a lower one. ADDITIVE — the gnu assets keep their names, consumers and attestation path, so nothing that works today changes. THE PART THAT IS NOT PLUMBING. release.yml runs only on a TAG PUSH, so a target added there is unverified until the tag, and editing the release workflow between an RC and its tag is the unreviewed late change this process exists to prevent. So a per-PR job (`musl-portable-asset`) builds the same target with the same feature set and runs the issue's two acceptance commands on the result: statically linked, no interpreter, ZERO GLIBC_ symbols. WITH A POTENCY CONTROL, because those assertions could pass on anything: the same job builds the GNU target on the same runner and asserts they FAIL there. A FALSE DOC STATEMENT FOUND ON THE WAY, corrected in place. `docs/release-process.md` said the `verify` feature is "not" enabled in release builds and that enabling it "remains a deliberate follow-up decision". It was taken in v0.58 (RQ-58-SHIPVERIFY #1000/#1002, which put `--features verify` on both build lines), so the sentence had been false for thirteen releases. Measured on the shipped v0.70.0 asset: 20 `ordeal` strings, ZERO occurrences of the degraded-path message. RESIDUAL, NAMED: arm64 Linux is still glibc-floored. Only the x86_64 musl asset is published; aarch64-unknown-linux-musl needs the cross path and its own measurement, and is not claimed. Refs #1349 * fix(#1337): render a MODIFIED artifact, not its Python dict, in the release notes RQ-70-RIVETNOTES (#1337) shipped `release_notes_from_rivet.py` in v0.70 to derive the CHANGELOG's artifact section instead of re-typing it. Its modified-artifact path had never run. `rivet diff` reports `added` and `removed` as bare id STRINGS but `modified` as `{"id": ..., "changes": [...]}`. The renderer f-stringed the entry directly, so running it for THIS release printed: - *(modified)* **{'changes': ['field changed: issue-scope'], 'id': 'RQ-70-NPA'}** straight into the notes. v0.71 is the first release to modify a PRIOR release's artifact — RQ-71-ISSUESCOPE applies `issue-scope: outlives` to RQ-70-NPA and RQ-70-FALCONCORPUS — so the defect shipped behind a code path nothing reached. Same shape as the four gates v0.70 found that could not fail, one layer out: a renderer arm that could not render. Found by running the derivation against a SIMULATION of the merged tree before cutting, rather than discovering it in the CHANGELOG. The `changes` list is kept rather than dropped — "which field moved on a shipped artifact" is what a reader of a release note actually needs, and it is why a modified entry is richer than an added one: - *(modified)* **RQ-70-FALCONCORPUS** — field changed: issue-scope - *(modified)* **RQ-70-NPA** — field changed: issue-scope Refs #1337 * fix(#1250): name the PR in `landed:` so R10 does not depend on the squash subject MEASURED at the #1356 merge, which reddened main. `gh pr merge --squash` uses the PR TITLE as the subject only when the branch has MORE THAN ONE commit; with exactly one it uses THAT COMMIT'S subject. #1356 had one commit, so main landed feat(issuescope): let an artifact say its ISSUE outlives its delivery ... (#1356) while the four-check ritual's CHECK4 had simulated the PR title "RQ-71-ISSUESCOPE (#1250): ...". The gate passed on a tree that was never created, and main went red on R10 — a delivery-shaped commit attributable to no artifact. Exactly v0.70's squash-simulation lesson, one level deeper: it is not enough to simulate a squash, the simulated SUBJECT has to be the one that will actually land. Two fixes, and only the second is durable: * RQ-71-ISSUESCOPE `landed:` now names PR #1356, and RQ-71-MUSL names #1357. R10 accepts EITHER an artifact id / issue number in the subject OR an artifact whose `landed:` names the PR. Naming the PR makes attribution independent of whatever subject GitHub chooses — the general fix, applied here to both. * the merge ritual now passes `gh pr merge --subject "<pr title> (#N)"`, so the simulated tree and the real one agree BY CONSTRUCTION rather than by a prediction of GitHub's default. Never simulate one subject and merge another. Refs #1250, #1349 * fix(#1349): the musl gate could not pass, and it was on the wrong runner pool Two corrections to RQ-71-MUSL, one from the v0.71 cold review and one from the maintainer. Both are recorded in the artifact rather than quietly applied. 1. THE GATE COULD NOT PASS — the class this release keeps finding, this time built by me. The acceptance step asserted file "$BIN" | grep -q 'statically linked' rustc's musl target NEVER produces that string. Its spec sets `crt-static-default` AND `static-position-independent-executables`, so the link is `-static-pie` and `file` reports "static-pie linked". The gate would have REFUSED A CORRECT ARTIFACT — and `create-release` has `needs: [build-binaries]`, so that is not one missing archive, it is NO RELEASE AT ALL. A gate that cannot pass, in the workflow that publishes the release, in the lane whose entire point is that the asset is checkable. The fix is not a better string. `file`'s wording is a presentation detail of a tool this repo does not control; the PROPERTY is "asks no loader to run it", which is exactly "no PT_INTERP program header". `scripts/elf_static_check.py` reads it from the ELF with nothing beyond the stdlib, and was validated BOTH ways before being wired: the real published v0.70.0 gnu asset -> PT_INTERP=1, GLIBC_ x17, rc=1 a synthesised static-pie shape -> PT_INTERP=0, GLIBC_ x0, rc=0 The potency control was widened with it: the gnu leg now runs the SAME check and must FAIL it, so BOTH assertions have a negative control. Previously the gnu block never asserted a loader was present, so the musl `interpreter` assertion had none. 2. THE RUNNER POOL — raised by the maintainer while this very PR sat queued. I put the job on `ubuntu-latest` by copying the surrounding convention without thinking about capacity. Measured: 56 of ci.yml's 67 jobs target `ubuntu-latest` and only 8 use self-hosted, which is exactly what RQ-61-CICAP identified as THE bottleneck — runs queue for hours beside idle machines because the constraint is the GitHub-hosted quota, not the fleet. Adding another ubuntu-latest job makes that worse for every other lane. Now `[self-hosted, linux, x64, rust-cpu]`. The apt step is conditional and non-fatal: whether rust's bundled musl crt and `rust-lld` make `musl-tools` unnecessary for a pure-Rust workspace is UNVERIFIED here — it cannot be checked on this macOS host (no musl std, no nightly for `--print target-spec-json`) — so it is not asserted either way, and the build step is left to answer it loudly. Refs #1349 * docs(#1349): correct the `ordeal` string count — 19, not 20 The v0.71 prose-truth cold review checked this number and it is wrong in both readings. Re-derived on the downloaded v0.70.0 x86_64 asset: case-sensitive b"ordeal" -> 19 case-insensitive -> 21 "20" is neither. The figure appeared twice — in RQ-71-MUSL and in the docs/release-process.md paragraph this lane corrected — so it is fixed in both, with the counting method stated so the next reader can reproduce it rather than guess which convention produced the number. The load-bearing half of that sentence is unaffected and was independently re-verified: ZERO occurrences of the degraded-path message, which is what shows `synth verify` genuinely works in a released binary and that the doc claiming `--features verify` is off had been false since v0.58. Refs #1349
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.
Closes #1000 (RQ-58-SHIPVERIFY).
synth verifyexisted in the tree and in--help, failed closed with an exemplary message — and was in no artifact any user could obtain (confirmed on 0.55.0 and 0.57.0: all four platform tarballs lacked--features verify). For a compiler whose whole argument is verified code generation, this ships the feature and gates it so it cannot silently regress to help text.1. Released binaries carry
verifyrelease.yml: all four platform builds (x86_64/aarch64Linux,x86_64/aarch64macOS) now build-p synth-cli --features verify; the stale "deliberate follow-up decision" comment is replaced with the measured basis.cargo tree -p synth-cli --features verify→ 0 z3 nodes;--features verify,synth-verify/z3-solver→ 2.verify = ["synth-verify"](pure-Rust ordeal since Adopt ordeal (pure-Rust QF_BV) in synth-verify; demote Z3 to differential oracle, then drop static-link-z3 #553/v0.27); the Z3 differential oracle remains a separate opt-in that links the system libz3 and is not enabled here.@pulseengine/synthwrapper downloads and checksum-verifies these same release tarballs at install time (npm/install.js), so it inherits the feature.cargo install synth-cliusers still choose features themselves (verifyis deliberately not made a default feature — that would change every workspace build; named residual, not silently dropped).2. The non-vacuity gate (the part that matters)
scripts/release_verify_smoke.shruns against the binary extracted from each packaged tarball (not a dev build): compiles a module with it, runssynth verifyon that module, and asserts a real verdict — exit 0, the verdict line, and asynth-verify-v1report whose summary provesverified >= 1 && failed == 0(counts, not sentence-greps). All four tarballs are executed: linux-x86_64 + both macOS natively (x86_64-darwin under Rosetta on the arm64 runner), the cross-built aarch64-linux tarball underqemu-aarch64 -L /usr/aarch64-linux-gnu.Red-first evidence (local, this branch):
And the red direction is CI-pinned, not authoring-time-only: the
fact-spec-oraclejob now builds a verify-less binary, asserts the smoke script FAILS with exactly the capability error (wrong-reason failures are also red), then re-runs it green on the verify build. A gate whose red leg is not exercised goes vacuous silently — this repo has shipped that class.3. Capability check before the banner
Previously the four
Translation validation:lines — includingStrategy: Per-rule SMT verification (ASIL D path)— printed before the tool discovered it could not verify, so a log-scraper found the ASIL-D strategy line in a run that verified nothing (exit code was already correct, #124). The check now runs before the banner: an incapable binary prints nothing verification-shaped before failing.Red-first:
tests/verify_banner_1000.rs(norequired-features; the missing-capability half runs in the plain workspace suite) fails on the pre-fix ordering — observed:ASIL-D strategy line printed by a binary that cannot verify— and passes with the fix. The#[cfg(feature = "verify")]half (wired intofact-spec-oracle) pins that a capable binary still prints the banner and ends inAll functions verified successfully..Also de-staled the
synth verifyhelp line ("via Z3" → SMT translation validation, pure-Rust ordeal) — measured above.Out of scope, named not silently dropped
#1000's
synthesize-vs-compiledescription overlap,--format json, help-line width (real, minor, not this lane's subject); makingverifya default cargo feature; README:98's stale Z3 sentence (corrected in #1001 — not duplicated here).Step 5 — witness MC/DC (#978 floors)
The reordered capability check adds one decision — in
synth-cli, which is outside the scored scope. The harness's full in-workspace closure issynth-mcdc-harness+synth-core/synth-cfg/synth-opt/synth-synthesis/synth-backend-riscv(percargo tree), andgit diff --name-only main...HEADintersects it in 0 files (Cargo.lock also unchanged, rustc pinned 1.96.1): the harness wasm this branch produces is byte-for-byte main's, so the counts cannot move.I re-derived locally anyway at rustc 1.96.1 and READ THE GAP ROWS rather than trusting the argument: every gap-row function is in the untouched crates (
validate_final_allocation_rv32,ensure_supported_target,compile_function_with_opts,static_data_addr::resolve_owner/validate_reloc_resolutions*) — none is this lane's code. Honest boundary on the local numbers: my localwitness-mcdcis 0.28.0, not the CI-pinned 0.42.0, and the local run reports 122 cond / 50 proved / 51 dead vs floors 130/57/≤50 — since the harness inputs are provably identical to main's, that local red is the unpinned local witness version measuring differently, not a delta from this change (it would reproduce identically on main). The PR'smcdc-structural-coveragejob (pinned witness 0.42.0, pinned host) is the authoritative floors gate — read its result, not my local one.Step 6 — sigil / attestation
Assessed, not defaulted to N/A: this PR changes what the released tarballs contain (a larger binary with the ordeal solver linked in). The existing attestation chain covers the new content without modification — SLSA provenance is generated per-release over
release-assets/*.tar.gz(subject digests are computed from the new bytes) and the cosign-signedSHA256SUMS.txttransitively covers them; the smoke step runs before upload/attestation and does not modify the archives. No new artifact type or build stage is introduced, and synth's native tarballs are not sigil-signed wasm (sigil is not part of this repo's release chain). Nothing to add.🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L