feat(#1000): ship 'synth verify' in released artifacts + non-vacuity smoke gate (RQ-58-SHIPVERIFY)

[avrabe]

Closes #1000 (RQ-58-SHIPVERIFY). synth verify existed 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 verify

• release.yml: all four platform builds (x86_64/aarch64 Linux, x86_64/aarch64 macOS) now build -p synth-cli --features verify; the stale "deliberate follow-up decision" comment is replaced with the measured basis.
• No Z3 ships. Re-measured on this base: 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.
• npm channel: no change needed — the @pulseengine/synth wrapper downloads and checksum-verifies these same release tarballs at install time (npm/install.js), so it inherits the feature.
• crates.io publish path: source-only publish, untouched. cargo install synth-cli users still choose features themselves (verify is 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.sh runs against the binary extracted from each packaged tarball (not a dev build): compiles a module with it, runs synth verify on that module, and asserts a real verdict — exit 0, the verdict line, and a synth-verify-v1 report whose summary proves verified >= 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 under qemu-aarch64 -L /usr/aarch64-linux-gnu.

Red-first evidence (local, this branch):

$ cargo build -p synth-cli   # WITHOUT verify
$ bash scripts/release_verify_smoke.sh target/debug/synth ; echo rc=$?
FAIL: synth verify exited non-zero — this artifact cannot verify
Error: this `synth` binary was built without the `verify` feature — ...
rc=1

$ cargo build -p synth-cli --features verify
$ bash scripts/release_verify_smoke.sh target/debug/synth ; echo rc=$?
verdict: 2 verified / 0 failed / 0 unknown / 3 declined across 5 applied rule kinds
PASS: released artifact runs 'synth verify' to a real verdict
rc=0

And the red direction is CI-pinned, not authoring-time-only: the fact-spec-oracle job 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 — including Strategy: 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 (no required-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 into fact-spec-oracle) pins that a capable binary still prints the banner and ends in All functions verified successfully..

Also de-staled the synth verify help line ("via Z3" → SMT translation validation, pure-Rust ordeal) — measured above.

Out of scope, named not silently dropped

#1000's synthesize-vs-compile description overlap, --format json, help-line width (real, minor, not this lane's subject); making verify a 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 is synth-mcdc-harness + synth-core/synth-cfg/synth-opt/synth-synthesis/synth-backend-riscv (per cargo tree), and git diff --name-only main...HEAD intersects 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 local witness-mcdc is 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's mcdc-structural-coverage job (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-signed SHA256SUMS.txt transitively 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

[codecov]

Codecov Report

❌ Patch coverage is 66.66667% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	66.66%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!