synth

Synth is an ahead-of-time compiler that takes WebAssembly (binary or WAT text) and emits bare-metal ELF binaries for embedded targets. Its primary backend is ARM Cortex-M (Thumb-2) machine code, with additional backends for ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 as a host-native target selected via -b aarch64. The AArch64 backend can also produce relocatable output that links into a normal arm64-Linux static library, with the resulting ET_REL verified in CI by linking against a C harness and executing against wasmtime on an arm64-Linux runner, under qemu-user and under unicorn; the embedder contract is documented separately. The compilation pipeline is a straightforward chain: parse and decode via wasmparser/wat, WASM-to-ARM instruction selection, peephole optimization (redundant-op elimination, NOP removal, instruction fusion, constant propagation), ARM/Thumb-2 encoding, and ELF32 output with .text, .isr_vector, .data, .bss and a symbol table. Optional vector table and reset handler are provided for Cortex-M, and linker scripts for STM32, nRF52840 and generic boards are generated. The codebase is split into crates covering the CLI, core types and backend trait, frontend parsing, architecture backends, instruction selection, CFG and IR optimization passes, SMT verification, ABI lift/lower, memory abstraction, QEMU integration, WAST-to-Robot test generation, and WIT parsing. A central claim of the project is functional safety treated as a certification problem, with verifiable code generation from WASM to a small target ISA. Mechanized proofs in Rocq cover i32 and i64 instruction selection with result-correspondence (T1) theorems, while float and SIMD selection currently has existence-only (T2) proofs. Selector-DSL rule theorems are stated directly about the generated model, single-sourced from the shipped rule set so that a selector-table change breaks the matching proof. Proof and rule counts are machine-derived into a status JSON file and CI-gated rather than hand-typed. Translation validation uses the synth-verify crate, which encodes WASM and ARM semantics as QF_BV formulas. Since v0.27.0 the default engine is ordeal, a pure-Rust QF_BV solver requiring no C++ toolchain; Z3 is a feature-gated differential oracle. The project also reports starting work on Kani bounded model checking harnesses and Verus spec functions, with Lean not started. Testing combines Rust unit tests, Renode and QEMU emulation, execution differentials against wasmtime, and fixture-scoped cycle and correctness runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100). A CI workflow compiles the WebAssembly spec test suite per backend and counts declines separately from errors, with counts pinned exactly and checked on the single-module path only. The README is explicit about what does not work yet: narrow hardware coverage with no broad board matrix, multi-memory still in phase 1, no WASI on embedded, no component model execution without the not-yet-existing kiln-builtins crate, spill-on-exhaustion still opt-in, no tail-call optimization, and SIMD/Helium encoding implemented but never run on M55 silicon or emulator. The measured size benchmark, regenerated from an artifacts file, reports the default path at 1.64x-3.48x larger than native C/Rust at -Os, falling to 0.54x on a clamp shape when supplied a proven premise certificate; every cycle cell is still marked open pending silicon DWT measurements. Builds require Rust 1.88+ (edition 2024) with Cargo, or Bazel 8.x with Nix for hermetic builds of Rust, Rocq proofs and Renode tests. The project is licensed Apache-2.0 and is part of the PulseEngine toolchain alongside Loom (WASM optimizer with Z3 verification), Meld (Component Model static fuser), Kiln (WASM runtime for safety-critical systems) and Sigil (supply chain attestation and signing).