synth verify advertised in CLI but inert unless built with --features verify

[avrabe]

Summary

synth verify is listed as a subcommand in synth --help and shown in the top-level usage examples, but on a stock cargo install'd binary it does no verification — it prints a "rebuild" hint and exits.

Repro

cargo install --path crates/synth-cli
synth verify input.wasm output.elf

Actual output:

  Binary: output.elf
  Backend: arm
  Strategy: Per-rule SMT verification (ASIL D path)

  Rebuild with verification support:
    cargo build --features verify

No Z3 translation-validation runs; exit is success-shaped.

Why it matters

synth verify is the Z3 translation-validation step — the "did the ARM lowering preserve WASM semantics" oracle. In the pulseengine verification story (overdoing-the-verification-chain) this is the translation-validation layer. A user following the CLI help reasonably believes they ran it. Silent no-op verification in an ASIL-D-positioned toolchain is a trust hazard.

Suggested fix (any one)

1. Compile verify support into the default release build (drop the verify feature gate, or make it default).
2. If the feature must stay optional, gate the subcommand itself behind #[cfg(feature = "verify")] so it isn't advertised in --help when unavailable.
3. At minimum, exit non-zero when verify is invoked without support, so CI can't mistake a no-op for a pass.

Option 1 is preferable for a verification-first tool.

Environment

• synth cargo install'd from crates/synth-cli, v0.1.0
• macOS arm64
• Found while bringing up the falcon WASM→ARM pipeline (pulseengine/relay, falcon v0.6)