synth-cli 0.65.0

CLI for Synth, the WebAssembly-to-ARM Cortex-M AOT compiler
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

[package]
name = "synth-cli"
version.workspace = true
edition.workspace = true
authors.workspace = true
license.workspace = true
repository.workspace = true
homepage.workspace = true
keywords.workspace = true
categories.workspace = true
description = "CLI for Synth, the WebAssembly-to-ARM Cortex-M AOT compiler"

[[bin]]
name = "synth"
path = "src/main.rs"

# VCR-PERF-002 Phase 2 (#494): the fact-spec end-to-end gate needs the synth
# binary built WITH the ordeal-backed solver (feature `verify`), so it is a
# dedicated test target the fact-spec CI job runs via
# `cargo test -p synth-cli --features verify --test fact_spec_clamp_494`.
# Plain `cargo test --workspace` skips it (required-features unmet); the pass
# itself is unit-tested unconditionally in synth-verify.
[[test]]
name = "fact_spec_clamp_494"
required-features = ["verify"]

# #494 phase 2b (divisor-nonzero): same contract — the guard-elision byte
# gates need the solver-carrying binary; the fact-spec CI job runs it via
# `cargo test -p synth-cli --features verify --test fact_spec_div_494`.
[[test]]
name = "fact_spec_div_494"
required-features = ["verify"]

# #494 bounds-elision (#390 guard_bool): same contract — the memory
# bounds-guard byte gates need the solver-carrying binary; the fact-spec CI
# job runs it via
# `cargo test -p synth-cli --features verify --test fact_spec_bounds_494`.
[[test]]
name = "fact_spec_bounds_494"
required-features = ["verify"]

# #935 non-vacuity gate: `synth verify` must report APPLIED-AND-DECLINED rules
# (with machine reasons + Rocq join keys), so a consumer can compute a coverage
# denominator. Needs the solver-carrying binary; the fact-spec CI job runs it
# via `cargo test -p synth-cli --features verify --test verify_report_935`.
[[test]]
name = "verify_report_935"
required-features = ["verify"]

[features]
default = ["riscv"]
awsm = ["synth-backend-awsm"]
wasker = ["synth-backend-wasker"]
riscv = ["synth-backend-riscv"]
verify = ["synth-verify"]
# #275 non-vacuity probe (NEVER default): builds an `EXPORTS_ONLY_275` env hatch
# that reverts compile_all_exports to the pre-#235 exports-only drop, so the
# reachable-callgraph EXECUTION differential can prove it catches the historical
# #275 drop (the RED direction). #1168: the hatch covers the .wast merge path
# too, so the wast_callgraph_closure_1168 differential can prove the
# generalized not-placed refusal stands when the closure is bypassed.
# Excluded from every release/default build — the release binary physically
# cannot carry a "regress to a fixed defect" switch.
exports_only_275_probe = []
# Uncomment when loom crate is available:
# loom = ["dep:loom-opt"]

[dependencies]
# Path deps carry `version` so `cargo publish` rewrites them to the
# crates.io coordinate. Bumping the workspace version requires
# updating these in lockstep — see docs/release-process.md.
synth-core = { path = "../synth-core", version = "0.65.0" }
synth-frontend = { path = "../synth-frontend", version = "0.65.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.65.0" }
synth-backend = { path = "../synth-backend", version = "0.65.0" }

# AArch64 host-native backend (#538) — small pure-Rust crate, always on.
synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.65.0" }

# Optional external backends
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.65.0", optional = true }
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.65.0", optional = true }
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.65.0", optional = true }

# Optional translation validation — pure-Rust ordeal engine by default (#553),
# no C++ toolchain needed. For the Z3 differential oracle build with
# `--features verify,synth-verify/z3-solver` (+ SYNTH_SOLVER_DIFF=1 at runtime).
synth-verify = { path = "../synth-verify", version = "0.65.0", optional = true, features = ["arm"] }

# Optional PulseEngine WASM optimizer
# Uncomment when loom crate is available:
# loom-opt = { workspace = true, optional = true }

clap.workspace = true
anyhow.workspace = true
tracing.workspace = true
tracing-subscriber.workspace = true
serde.workspace = true
serde_json.workspace = true
wat.workspace = true
wast.workspace = true

[dev-dependencies]
object.workspace = true
# VCR-DBG-001 Tier-1 (#394) — oracle E parses the INPUT wasm's `.debug_*` custom
# sections independently (mirroring the production reader) to derive, at runtime,
# the real source basenames its `.debug_line` rows reference — so the emitted
# file-table check is robust vs hardcoding. Test-only; matches synth-core's pin.
# Bazel globs src/ only, so no MODULE.bazel pin is needed for a dev-dependency.
wasmparser.workspace = true
# VCR-ORACLE-001 (#242) — the frozen-codegen byte gate hashes each fixture's
# `.text` to lock it against accidental drift (e.g. a dependabot parser bump
# shifting lowering). Already in the lock tree; test-only ⇒ no production pull,
# no MODULE.bazel pin (Bazel globs src/ only).
sha2 = "0.11"
# VCR-DBG-001 step 4 (#394) — oracle B parses the EMITTED `.debug_line` back with
# gimli::read to prove the section is real debugger-readable DWARF (addresses in
# `.text` range, lines non-zero). Test-only; the production read+emit lives in
# synth-core. Matches synth-core's gimli pin.
gimli = { version = "0.34", default-features = false, features = ["read", "std"] }
# VCR-MEM-001 (#383) layer-2 substrate: scry's sound shadow-stack-depth analysis,
# verified in-tree against a real module. DEV-dependency only — the production
# binary does not pull scry until the gated consumption step (the .bss shrink /
# prologue elision) lands. Test-only ⇒ Bazel (which globs src/ only) never sees
# it, so no MODULE.bazel pin is needed yet. See scry#51.
# Tracks scry 2.x (SCPV v3): the major bump reshaped the provenance wire format,
# but synth's consumed surface (call_graph / function_summaries / stack_usage /
# reachable_from_exports / operand_stack) is unchanged and additive-only, so the
# bump is transparent here. See scry#63 / scry v2.0.0. Empirically re-verified
# against scry v2.3.0, v2.5.0 (2026-06-27), then v2.6.0 (2026-06-30, lockfile
# bumped) — scry_shadow_stack_budget stays GREEN, so the "transparent" claim is
# tested, not just asserted. v2.4.0 (FEAT-038) models memory.size/grow; v2.5.0
# (FEAT-039) makes reachable_from_exports sound in the open world (escaped
# funcref) — the superset synth's shadow-stack pruning relies on; pinned by
# scry_reachable_superset_is_open_world_sound_383_feat039. v2.6.0 adds the
# machine-readable `gaps` field (FEAT-040) + hardens the shadow-stack bound by the
# resolved call_indirect target set (FEAT-043); consumed surface unchanged
# (msgq_put Bytes(32) bound unchanged), now re-verified with a gap-observability
# assertion (value-domain gaps ⇒ the finite bound is sound).
scry-sai-core = "3.0"