WebAssembly-to-ARM/RISC-V AOT compiler with mechanized correctness proofs
Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, --target cortex-r5), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, integer subset, -b aarch64). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), control flow, and memory operations; scalar float ops are rejected loudly rather than miscompiled (#369, #554). Mechanized correctness proofs in Rocq cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
This is pre-release software. Generated code is validated by unit tests, Renode/QEMU emulation, execution differentials against wasmtime, and — for specific fixtures — cycle- and correctness-gated runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100, via the gale test loop). Broad hardware validation is still missing. Use at your own risk.
Part of PulseEngine -- a WebAssembly toolchain for safety-critical embedded systems:
| Project | Role |
|---|---|
| Synth | WASM-to-ARM AOT compiler with Rocq proofs |
| Loom | WASM optimizer with Z3 verification |
| Meld | WASM Component Model static fuser |
| Kiln | WASM runtime for safety-critical systems |
| Sigil | Supply chain attestation and signing |
Synth's pitch is that functional safety is a certification problem, not a processor problem: the right unit of evidence is verifiable code generation from a small, well-defined source language (WASM) to a small, well-defined target ISA (Thumb-2 / RV32), not a verified silicon core. Synth contributes the codegen half of that workflow: a compiler whose lowering steps come with mechanized proofs and an explicit Spectre / speculative-execution policy per lowering rule.
Requires Rust 1.88+ (edition 2024).
git clone https://github.com/pulseengine/synth.git
cd synth
cargo build --release -p synth-cliThe binary is at target/release/synth. Add it to your PATH or invoke directly.
Bazel 8.x builds Rust, Rocq proofs, and Renode emulation tests hermetically via Nix.
bazel build //crates:synth# Compile a WAT file to a Cortex-M ELF binary
synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf
# Disassemble the result
synth disasm firmware.elfTranslation validation (synth verify, --verify) is feature-gated in the CLI. Since v0.27.0 the default verification engine is ordeal, a pure-Rust QF_BV solver — synth-verify itself no longer needs a C++ toolchain. The CLI verify feature currently also enables the feature-gated Z3 differential oracle (statically linked):
cargo build --release -p synth-cli --features verify
synth verify examples/wat/simple_add.wat firmware.elf| Category | Status | Notes |
|---|---|---|
| i32 arithmetic, bitwise, comparison, shift/rotate | Tested | Full Rocq T1 proofs, Renode execution tests |
| i64 (register pairs): arithmetic, shifts, rotates, div/rem, compare | Tested | full pair lowering — right shifts fixed v0.28.0 (#599), rot/div/rem v0.30.1 (#610), A32 completeness v0.30.2 (#615); differential vs wasmtime |
| f32/f64 via VFP | Not implemented | Decoded → loud reject, never silent miscompile (#369, #554); VFP encoder exists as a disconnected prototype |
| WASM SIMD via ARM Helium MVE | Experimental | Cortex-M55 only; encoding untested on hardware |
| Control flow (block, loop, if/else, br, br_table) | Tested | Renode execution tests, complex test suite |
| Function calls (direct, indirect) | Implemented | Unit tests; inter-function calls not Renode-tested |
| Memory (load/store, sub-word, size/grow) | Implemented | memory.grow returns -1 on embedded (fixed memory) |
| Globals, select | Implemented | R9-based globals; unit tests only |
| ELF output with vector table | Implemented | Thumb bit set on symbols; not linked on real hardware |
| Linker scripts (STM32, nRF52840, generic) | Implemented | Generated, not tested with real boards |
Cross-compilation (--link flag) |
Implemented | Requires arm-none-eabi-gcc in PATH; not CI-tested |
| Rocq mechanized proofs | 298 Qed / 9 Admitted | i32 + i64 T1 proofs; division proofs re-admitted for trap guard alignment |
| SMT translation validation | ordeal (pure-Rust QF_BV) default | v0.27.0 (#553); Z3 demoted to feature-gated differential oracle — 141/141 agreement |
| WebAssembly spec test suite | 227/257 compile | Compilation only — not executed on emulator |
- Narrow hardware coverage — silicon validation is fixture-scoped (gale's NUCLEO-G474RE / STM32F100 cycle and correctness gates); there is no broad board matrix
- No multi-memory — fused components from meld need single-memory mode
- No WASI on embedded — kiln-builtins crate doesn't exist yet
- No component model execution — components compile but can't run without kiln-builtins + cabi_realloc
- Spill-on-exhaustion is opt-in — Belady spilling is default-on (v0.24.0, VCR-RA-001), but replacing the register-exhaustion decline with allocation-time spilling (
SYNTH_SPILL_ON_EXHAUST, #580) is held for silicon numbers - No tail call optimization — return_call compiles but doesn't optimize the call frame
- SIMD/Helium is untested — MVE instruction encoding implemented but never run on M55 silicon or emulator
# Compile a WAT file to an ARM ELF binary
synth compile examples/wat/simple_add.wat -o add.elf
# Compile with a built-in demo (add, mul, calc, calc-ext)
synth compile --demo add -o demo.elf
# Compile a complete Cortex-M binary (vector table, startup code)
synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf
# Compile all exported functions
synth compile input.wat --all-exports -o multi.elf
# Compile and formally verify the translation
synth compile input.wat --verify -o verified.elfsynth disasm add.elf# Standalone verification: check that an ELF faithfully preserves WASM semantics
synth verify input.wat output.elfsynth backendsgraph LR
A["WAT / WASM"] --> B["Parse &<br/>Decode"]
B --> C["Instruction<br/>Selection"]
C --> D["Peephole<br/>Optimizer"]
D --> E["ARM<br/>Encoder"]
E --> F["ELF<br/>Builder"]
F --> G["ARM ELF<br/>Binary"]
style A fill:#654FF0,color:#fff
style G fill:#CE422B,color:#fff
Pipeline stages:
- Parse -- decode WASM binary or WAT text via
wasmparser/watcrates - Instruction selection -- pattern-match WASM ops to ARM instruction sequences (i32, i64, f32, f64, SIMD)
- Peephole optimization -- redundant-op elimination, NOP removal, instruction fusion, constant propagation (0-25% code reduction)
- ARM encoding -- emit 32-bit ARM / Thumb-2 machine code
- ELF builder -- produce ELF32 with
.text,.isr_vector,.data,.bss, symbol table; optional vector table and reset handler for Cortex-M
Per the PulseEngine Verification Guide, projects target multi-track verification. Current status:
| Track | Status | Coverage |
|---|---|---|
| Rocq | Partial | 298 Qed / 9 Admitted — division proofs re-admitted for trap guard alignment |
| Kani | Starting | 18 bounded model checking harnesses for ARM encoder |
| Verus | Starting | 8 spec functions in synth-synthesis/src/contracts.rs; Bazel integration via rules_verus |
| Lean | Not started | — |
See artifacts/verification-gaps.yaml for the detailed gap analysis (VG-001 through VG-008).
Mechanized proofs in Rocq 9 show that compile_wasm_to_arm preserves WASM semantics for each operation. The proof suite lives in coq/Synth/ and covers ARM instruction semantics, WASM stack-machine semantics, and per-operation correctness theorems.
298 Qed / 9 Admitted (+2 admit. tactics)
T1 result-correspondence (ARM output = WASM result): all i32 ops and all
i64 ops — i64 T1 parity since v0.11.0, 0 i64 admits (coq/STATUS.md)
T2 existence-only: f32/f64 and remaining categories
T3 admitted (9): 4 i32 division trap guards (exec_program model gap, #73),
2 Compilation.v, 1 CorrectnessSimple.v, 2 ArmRefinement.v
+ 7 Qed VCR-SEL-001 pilot lemmas (Synth/VcrSelPilot.v, #386)
i32 and i64 operations have full T1 (result-correspondence) proofs; i64 parity landed in v0.11.0. Division proofs were re-admitted after updating Compilation.v to emit trap guard sequences (CMP+BCondOffset+UDF) matching the actual compiler — the sequential exec_program model needs PC-relative branching support to verify these. The f32, f64, and SIMD instruction selection has T2 existence proofs but not T1 result-correspondence.
Build the proofs:
# Hermetic build via Bazel + Nix
bazel test //coq:verify_proofs
# Or locally with Rocq 9
cd coq && make proofsSee coq/STATUS.md for the per-file coverage matrix.
The synth-verify crate encodes WASM and ARM semantics as QF_BV formulas and checks per-rule equivalence. Since v0.27.0 (#553/#595) the default engine is ordeal, a pure-Rust QF_BV solver (139/139 validator tests, ~2 s; no C++ toolchain required); Z3 is demoted to a feature-gated (z3-solver) differential oracle — 141/141 cases, zero disagreements with ordeal. The --verify CLI flag invokes validation after compilation; synth verify provides standalone validation.
Replace synth's patch-accreting code generator with foundationally-verified, allocator-robust infrastructure — so correctness comes from construction, not from an ever-growing pile of locally-correct patches.
The recurring greedy fixes (the reciprocal-multiply cost-gate, the register-exhaustion hard-fail, the "selector missed an op" class behind #223/#226/#232) are all symptoms of one root cause: two single-pass, hand-written components — the instruction selector and the register allocator. The fix is filed as a phased, parallelizable rivet program (VCR-*, epic #242, artifacts/verified-codegen-roadmap.yaml), built incrementally alongside the per-issue cadence — never a big-bang rewrite, behavior frozen and oracle-gated at every step.
The one-sentence version: moving synth's correctness from "we patched every bug we found" to "the structure makes the bug unrepresentable."
Historical motivation (gale, #209, on NUCLEO-G474RE, mid-2026): the fully-composed flat_flight ran 315 cyc vs 99 native (3.18×) with 61 % redundant constant materializations and 17 stack spills. Those numbers set the allocator track's agenda; the v0.19–v0.30 arc has since retired them.
VCR-RA-001— allocator with liveness-based Belady spilling:verified, default-on since v0.24.0 (SYNTH_SPILL_REALLOC).flat_flightreaches its Belady optimum — 412→388 B, hot-segment frame traffic 3 ld + 3 st → 0 — with every re-pinned fixture execution-proven vs wasmtime first.- const-CSE default-on (v0.29.0, #604) — the redundant-materialization datum retired; gale-confirmed on its kernel (
gust_mix90→86 B loom-inlined, direct-compilefunc_170→66 B). - The lever ladder, all default-on and evidence-gated with CI-pinned
=0/escape-hatch opt-outs: cmp→select fusion (ARM v0.13.0, RV32 v0.28.0), i32 local promotion (v0.14.0, with the v0.15.1 never-cause-a-compile-failure fallback), immediate-shift folding (ARM v0.15.0, RV32 v0.30.0), base-CSE into R11 (v0.27.0), dead-frame-elim + uxth-fold (v0.30.0). - i64 completeness arc: direct-path i64 stack params + pair spill-pool growth (#503, v0.29.0), pair right-shifts (#599, v0.28.0), rotl/rotr/div/rem silent-zero fix (#610, v0.30.1), and the A32 (
cortex-r5) i64 family — previously silently encoding to NOP — rebuilt with a 221-variant no-wildcard tripwire so no silent-NOP arm can regrow (#615, v0.30.2). - Verification substrate: ordeal (pure-Rust QF_BV) is the default translation-validation engine since v0.27.0; Z3 demoted to a feature-gated differential oracle (141/141 agreement). Track C's differential oracles are CI-gated jobs (cmp-select, RV32 shift-fold/const-addr-fold, callee-saved, spill-frame, control_step/flight_seam symtab-based fixtures, …).
| Track | Item | What it does | Status |
|---|---|---|---|
| A — codegen core | VCR-SEL-001 |
Rocq-discharged verified selector DSL — "ISLE with a proof-assistant backend"; a missing lowering rule becomes an enumerable coverage gap, not a silent miscompile | increment 1 in review (PR #623: 6-op i32 ALU class + rotl behind SYNTH_SEL_DSL); 7 Qed pilot lemmas in coq/Synth/Synth/VcrSelPilot.v |
VCR-PERF-002 |
Proof-carrying specialization (#494): loom's wsc.facts invariants become premises for per-elision proof obligations, certificate-checked by the ordeal-backed validator — toward gale's measured 0.45× (below-native) floor |
design traced (v0.30.0); phase 1 (facts ingestion) in review (PR #624) | |
SYNTH_SPILL_ON_EXHAUST |
Replace the register-exhaustion decline with allocation-time Belady spilling (#580) — the last piece of the exhaustion hard-fail | built, flag-off; default-on held for silicon cycle numbers | |
| B — authoritative semantics | VCR-ISA-001 |
Re-base ARM/RISC-V semantics on Sail-generated Rocq (the official ISA spec) | proposed |
VCR-WASM-001 |
Anchor WASM source semantics on WasmCert-Coq | proposed | |
| Gate | VCR-VER-001 |
Success = a previously load-bearing greedy-fix becomes revertable, with the full differential bit-identical and cycles equal-or-better | proposed |
Honest open items: the RV32 local-promotion flip is held on a failed no-grow gate (#601); f32/f64 remain loud-reject (#369); SIMD/Helium is untested on hardware.
What it buys us: synth stops being a real-ish compiler held together by oracle-gated patches and becomes a genuinely best-in-class verified compiler — and the verified selector DSL is the part that is potentially novel/publishable, not just catching up to Cranelift.
| Crate | Purpose |
|---|---|
synth-cli |
CLI entry point (synth compile, synth verify, synth disasm) |
synth-core |
Shared types, error handling, Backend trait, WASM decoder |
synth-frontend |
WASM Component Model parser and validator |
synth-backend |
ARM Thumb-2 (Cortex-M) + A32 (Cortex-R5) encoder, ELF builder, vector table, linker scripts, MPU |
synth-backend-riscv |
RISC-V RV32IMAC backend (selector, encoder, relocatable ELF) — qemu_riscv32 / ESP32-C3 |
synth-backend-aarch64 |
AArch64 (A64) host-native backend — integer subset, -b aarch64 |
synth-backend-awsm |
aWsm backend integration (WASM-to-native via aWsm) |
synth-backend-wasker |
Wasker backend integration (WASM-to-Rust transpiler) |
synth-synthesis |
WASM-to-ARM instruction selection, peephole optimizer, pattern matcher |
synth-cfg |
Control flow graph construction and analysis |
synth-opt |
IR-level optimization passes (CSE, constant folding, DCE) |
synth-verify |
SMT translation validation — ordeal (pure-Rust QF_BV) default, Z3 feature-gated differential oracle |
synth-analysis |
SSA, control flow analysis, call graph |
synth-abi |
WebAssembly Component Model ABI (lift/lower) |
synth-memory |
Portable memory abstraction (Zephyr, Linux, bare-metal) |
synth-qemu |
QEMU integration for testing |
synth-test |
WAST-to-Robot Framework test generator for Renode |
synth-wit |
WIT (WebAssembly Interface Types) parser |
# Run all Rust tests
cargo test --workspace
# Lint
cargo clippy --workspace --all-targets -- -D warnings
cargo fmt --check
# Bazel: Rocq proofs + Renode ARM Cortex-M4 emulation tests
bazel test //coq:verify_proofs
bazel test //tests/...- Architecture -- compilation pipeline, ARM instruction mapping, benchmarks
- Architecture Vision -- full system design and roadmap
- Synth & Loom -- two-tier architecture
- Feature Matrix -- what works, what doesn't
- Requirements -- functional and non-functional requirements
- Research -- literature review, formal methods, Sail/ARM analysis
- Roadmap -- development phases
- Changelog -- version history
- Contributing -- how to contribute
Apache-2.0 -- see LICENSE.
Part of PulseEngine — WebAssembly toolchain for safety-critical systems