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

.github/workflows/ci.yml

@@ -1537,8 +1537,42 @@ jobs:
         run: cargo test -p synth-cli --features verify --test fact_spec_div_494
       - name: Run verify rule-inventory non-vacuity gate (#935 decline denominator)
         run: cargo test -p synth-cli --features verify --test verify_report_935
+      # #1000 (RQ-58-SHIPVERIFY): the capable half of the banner-ordering gate
+      # — a verify-capable binary must still print the strategy banner AND end
+      # in a real verdict. (The missing-capability half runs in the plain
+      # workspace test job, where the test binary is built without `verify`.)
+      - name: Run verify banner/verdict gate (#1000, verify half)
+        run: cargo test -p synth-cli --features verify --test verify_banner_1000
+      # #1000 red leg — keep the released-artifact smoke gate falsifiable on
+      # every push, not just at authoring time: against a binary built WITHOUT
+      # the `verify` feature, scripts/release_verify_smoke.sh (the script
+      # release.yml runs against each packaged tarball) must FAIL, and fail
+      # for exactly the capability reason. A gate whose red direction is not
+      # exercised goes vacuous silently — this repo has shipped that class.
+      - name: Build synth WITHOUT verify (#1000 red-leg binary)
+        run: cargo build -p synth-cli
+      - name: Red leg — release smoke gate must fail on a verify-less binary
+        run: |
+          set -euo pipefail
+          if bash scripts/release_verify_smoke.sh target/debug/synth \
+              > /tmp/smoke_red.log 2>&1; then
+            echo "VACUOUS GATE: release_verify_smoke.sh passed against a binary built without the verify feature" >&2
+            cat /tmp/smoke_red.log >&2
+            exit 1
+          fi
+          grep -q 'built without the `verify` feature' /tmp/smoke_red.log || {
+            echo "release_verify_smoke.sh failed for the WRONG reason:" >&2
+            cat /tmp/smoke_red.log >&2
+            exit 1
+          }
+          echo "red leg OK: smoke gate fails with the capability error on a verify-less binary"
       - name: Build synth (verify feature)
         run: cargo build -p synth-cli --features verify
+      # #1000 green leg — the same script release.yml runs against the
+      # packaged tarballs, here against the freshly built verify binary so a
+      # pre-tag push catches script/CLI drift instead of the release run.
+      - name: Green leg — release smoke gate passes on the verify binary
+        run: bash scripts/release_verify_smoke.sh target/debug/synth
       - uses: actions/setup-python@v7
         with:
           python-version: "3.x"

.github/workflows/release.yml

@@ -30,13 +30,17 @@ env:
 
 jobs:
   # ── Cross-platform binary builds ──────────────────────────────────────
-  # synth-cli builds with `--features riscv` only (the workspace default).
-  # The `verify` feature is intentionally NOT enabled here. Historically it
-  # pulled z3-sys (vendored C++ Z3 build — slow, network-hungry); since #553
-  # it is pure Rust (ordeal engine), so enabling it is now feasible but is a
-  # deliberate follow-up decision, not a build constraint. The CLI degrades
-  # gracefully without it (`synth verify` fails loudly with "rebuild with
-  # --features verify").
+  # synth-cli builds with the workspace default (`riscv`) PLUS `verify`
+  # (#1000, RQ-58-SHIPVERIFY): every released tarball can run `synth verify`
+  # to a real verdict. Historically `verify` pulled z3-sys (vendored C++ Z3
+  # build — slow, network-hungry); since #553 it is pure Rust (ordeal
+  # engine, re-measured for v0.58: `cargo tree -p synth-cli --features
+  # verify` has 0 z3 nodes — Z3 remains a separate `synth-verify/z3-solver`
+  # opt-in that never ships here). The smoke step below is the non-vacuity
+  # gate: it extracts the just-packaged tarball and asserts `synth verify`
+  # reaches a verdict, so dropping this feature flag reds the release run
+  # instead of silently regressing the artifact to help-text-only
+  # (the 0.55.0/0.57.0 state issue #1000 reported).
   build-binaries:
     name: Build ${{ matrix.target }}
     runs-on: ${{ matrix.os }}
@@ -79,11 +83,11 @@ jobs:
 
       - name: Build synth (native)
         if: ${{ !matrix.cross }}
-        run: cargo build --release --target ${{ matrix.target }} -p synth-cli
+        run: cargo build --release --target ${{ matrix.target }} -p synth-cli --features verify
 
       - name: Build synth (cross)
         if: matrix.cross
-        run: cross build --release --target ${{ matrix.target }} -p synth-cli
+        run: cross build --release --target ${{ matrix.target }} -p synth-cli --features verify
 
       - name: Strip binary
         if: ${{ !matrix.cross }}
@@ -107,6 +111,38 @@ jobs:
           tar -czf "$ARCHIVE" -C staging .
           echo "ARCHIVE=$ARCHIVE" >> "$GITHUB_ENV"
 
+      # ── #1000 non-vacuity gate: the TARBALL can `synth verify` ──────────
+      # Extracts the archive packaged above (the artifact a user downloads,
+      # not the loose build output) and asserts `synth verify` runs to a
+      # REAL verdict on a module the same binary just compiled — exit 0,
+      # the verdict line, and a synth-verify-v1 report with >= 1 verified /
+      # 0 failed rule kinds. Red direction proven at authoring and re-proven
+      # on every push by the fact-spec-oracle CI job's red leg: against a
+      # binary built without `--features verify` the script fails with the
+      # capability error. Without this step, "we ship the feature" regresses
+      # silently to "we ship the help text" — the exact #1000 class.
+      #
+      # Execution per target: linux-x86_64 + both macOS tarballs run natively
+      # (x86_64-apple-darwin under Rosetta 2 on the arm64 macos-14 runner);
+      # the cross-built aarch64-linux tarball runs under qemu-user against
+      # the gcc-aarch64-linux-gnu sysroot — all four tarballs are EXECUTED,
+      # none is exempt.
+      - name: Install qemu-user + aarch64 sysroot (cross smoke)
+        if: matrix.cross
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y qemu-user gcc-aarch64-linux-gnu
+
+      - name: Smoke-test the packaged tarball runs `synth verify`
+        env:
+          SYNTH_RUNNER: ${{ matrix.cross && 'qemu-aarch64 -L /usr/aarch64-linux-gnu' || '' }}
+        run: |
+          set -euo pipefail
+          mkdir -p smoke-extract
+          tar -xzf "$ARCHIVE" -C smoke-extract
+          bash scripts/release_verify_smoke.sh smoke-extract/synth
+
       - uses: actions/upload-artifact@v7
         with:
           name: binary-${{ matrix.target }}

crates/synth-cli/src/main.rs

@@ -572,8 +572,9 @@ enum Commands {
     /// List available compilation backends and their status
     Backends,
 
-    /// Verify compilation correctness via Z3 — requires a build with
-    /// `--features verify` (e.g., synth verify input.wat output.elf)
+    /// Verify compilation correctness via SMT translation validation
+    /// (pure-Rust ordeal engine) — requires the `verify` feature
+    /// (e.g., synth verify input.wat output.elf)
     Verify {
         /// Input WASM or WAT file (source)
         #[arg(value_name = "WASM")]
@@ -7174,6 +7175,31 @@ fn verify_command(
 
     let caps = backend.capabilities();
 
+    // #1000: capability check BEFORE the banner. This used to live after the
+    // four `Translation validation:` lines below, so a binary built without
+    // the `verify` feature printed `Strategy: Per-rule SMT verification
+    // (ASIL D path)` and only THEN discovered it could not verify — a
+    // log-scraper grepping for the strategy line would find it in a run that
+    // verified nothing. The exit code was already correct (1, issue #124);
+    // now the output is too: a binary that cannot verify prints nothing
+    // verification-shaped before failing.
+    #[cfg(not(feature = "verify"))]
+    if caps.supports_rule_verification {
+        // This binary was built without the `verify` feature, so no SMT
+        // translation validation can run. Returning Ok here would make
+        // `synth verify` exit success-shaped while doing nothing — a
+        // script or CI step gating on `synth verify` would silently
+        // believe the binary was validated (issue #124). Fail loudly
+        // with a non-zero exit instead.
+        anyhow::bail!(
+            "this `synth` binary was built without the `verify` feature — \
+             SMT translation validation is unavailable.\n  \
+             Rebuild with verification support:\n    \
+             cargo build --features verify\n  \
+             (or `cargo install --path crates/synth-cli --features verify`)"
+        );
+    }
+
     println!("Translation validation:");
     println!("  Source: {}", wasm_input.display());
     println!("  Binary: {}", elf_input.display());
@@ -7329,23 +7355,6 @@ fn verify_command(
                 }
             }
         }
-
-        #[cfg(not(feature = "verify"))]
-        {
-            // This binary was built without the `verify` feature, so no SMT
-            // translation validation can run. Returning Ok here would make
-            // `synth verify` exit success-shaped while doing nothing — a
-            // script or CI step gating on `synth verify` would silently
-            // believe the binary was validated (issue #124). Fail loudly
-            // with a non-zero exit instead.
-            anyhow::bail!(
-                "this `synth` binary was built without the `verify` feature — \
-                 SMT translation validation is unavailable.\n  \
-                 Rebuild with verification support:\n    \
-                 cargo build --features verify\n  \
-                 (or `cargo install --path crates/synth-cli --features verify`)"
-            );
-        }
     } else if caps.supports_binary_verification {
         println!("  Strategy: Binary-level translation validation (ASIL B path)");
         println!("\n  Binary verification not yet implemented.");

crates/synth-cli/tests/verify_banner_1000.rs

@@ -0,0 +1,143 @@
+//! #1000 (RQ-58-SHIPVERIFY) — `synth verify` capability check runs BEFORE the
+//! banner, and a verify-capable binary reports a real verdict.
+//!
+//! Two halves, selected by how the test binary was built (deliberately NO
+//! `required-features`, so the plain workspace test run exercises the
+//! missing-capability half):
+//!
+//! - WITHOUT `verify` (the plain `cargo test --workspace` build): `synth
+//!   verify` must fail (exit != 0) WITHOUT printing any of the
+//!   `Translation validation:` banner lines — in particular not
+//!   `Strategy: Per-rule SMT verification (ASIL D path)`. Before #1000 the
+//!   banner printed first and the capability check ran after it, so a
+//!   log-scraper grepping for the ASIL-D strategy line found it in a run
+//!   that verified nothing (the exit code was already correct, #124).
+//!   RED-FIRST: under the pre-#1000 ordering this half fails.
+//!
+//! - WITH `verify` (`cargo test -p synth-cli --features verify --test
+//!   verify_banner_1000`, wired into the fact-spec-oracle CI job): the
+//!   banner including the strategy line must still print, and the run must
+//!   end in a REAL verdict on a module synth itself just compiled — not the
+//!   capability-missing error. This is the in-tree twin of
+//!   `scripts/release_verify_smoke.sh`, the released-artifact gate release.yml
+//!   runs against the packaged tarballs.
+
+use std::process::Command;
+
+fn synth() -> &'static str {
+    env!("CARGO_BIN_EXE_synth")
+}
+
+/// Small module with an exported function whose ops are all on the verified
+/// ARM path (and/add) — the same shape the release smoke script compiles.
+const FIXTURE_WAT: &str = r#"(module
+  (func (export "mix") (param i32 i32) (result i32)
+    local.get 0
+    i32.const 255
+    i32.and
+    local.get 1
+    i32.add))
+"#;
+
+/// Compile the fixture with the binary under test; returns (wat, elf) paths.
+fn compile_fixture(tag: &str) -> (std::path::PathBuf, std::path::PathBuf, std::path::PathBuf) {
+    let dir = std::env::temp_dir().join(format!(
+        "synth_verify_banner_1000_{}_{}",
+        tag,
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&dir).expect("create temp dir");
+    let wat = dir.join("mix.wat");
+    let elf = dir.join("mix.elf");
+    std::fs::write(&wat, FIXTURE_WAT).expect("write fixture wat");
+    let compile = Command::new(synth())
+        .args([
+            "compile",
+            wat.to_str().unwrap(),
+            "-o",
+            elf.to_str().unwrap(),
+            "--all-exports",
+        ])
+        .output()
+        .expect("run synth compile");
+    assert!(
+        compile.status.success(),
+        "fixture compile failed:\n{}\n{}",
+        String::from_utf8_lossy(&compile.stdout),
+        String::from_utf8_lossy(&compile.stderr)
+    );
+    (dir, wat, elf)
+}
+
+fn run_verify(wat: &std::path::Path, elf: &std::path::Path) -> std::process::Output {
+    Command::new(synth())
+        .args(["verify", wat.to_str().unwrap(), elf.to_str().unwrap()])
+        .output()
+        .expect("run synth verify")
+}
+
+/// The missing-capability half: fail loudly BEFORE anything
+/// verification-shaped is printed.
+#[cfg(not(feature = "verify"))]
+#[test]
+fn verify_without_feature_fails_before_banner() {
+    let (dir, wat, elf) = compile_fixture("nofeat");
+    let out = run_verify(&wat, &elf);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let stderr = String::from_utf8_lossy(&out.stderr);
+
+    // #124 contract, unchanged: non-zero exit, loud capability error.
+    assert!(
+        !out.status.success(),
+        "`synth verify` must fail on a build without the `verify` feature\nstdout:\n{stdout}"
+    );
+    assert!(
+        stderr.contains("built without the `verify` feature"),
+        "capability error must name the missing feature\nstderr:\n{stderr}"
+    );
+
+    // #1000 contract, new: the check runs BEFORE the banner, so none of the
+    // four `Translation validation:` lines — above all the ASIL-D strategy
+    // line — may appear in a run that verified nothing.
+    assert!(
+        !stdout.contains("Strategy: Per-rule SMT verification"),
+        "ASIL-D strategy line printed by a binary that cannot verify:\n{stdout}"
+    );
+    assert!(
+        !stdout.contains("Translation validation:"),
+        "verification banner printed by a binary that cannot verify:\n{stdout}"
+    );
+
+    let _ = std::fs::remove_dir_all(&dir);
+}
+
+/// The capable half: banner still prints, and the run ends in a real verdict.
+#[cfg(feature = "verify")]
+#[test]
+fn verify_with_feature_reports_real_verdict() {
+    let (dir, wat, elf) = compile_fixture("feat");
+    let out = run_verify(&wat, &elf);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let stderr = String::from_utf8_lossy(&out.stderr);
+
+    assert!(
+        out.status.success(),
+        "`synth verify` must succeed on a verify-capable build\nstdout:\n{stdout}\nstderr:\n{stderr}"
+    );
+    // The #1000 reorder must NOT cost the capable binary its banner.
+    assert!(
+        stdout.contains("Strategy: Per-rule SMT verification (ASIL D path)"),
+        "strategy banner missing on a verify-capable build:\n{stdout}"
+    );
+    // A real verdict, not the capability-missing error.
+    assert!(
+        stdout.contains("All functions verified successfully."),
+        "expected a real verification verdict:\n{stdout}"
+    );
+    assert!(
+        !stderr.contains("built without the `verify` feature"),
+        "capability error on a build that HAS the feature:\n{stderr}"
+    );
+
+    let _ = std::fs::remove_dir_all(&dir);
+}