Synth

^{WebAssembly-to-ARM Cortex-M AOT compiler with mechanized correctness proofs}

 

 

Meld · Loom · Synth · Kiln · Sigil

 

Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code. It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), f32 (via VFP), control flow, and memory operations. Mechanized correctness proofs in Rocq cover the i32 instruction selection; i64/float/SIMD proofs are not yet done.

This is pre-release software. It has not been tested on real hardware. The generated ARM code passes unit tests and compiles 227/257 WebAssembly spec test files, but execution on Cortex-M silicon is unverified. 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

Installation

From source (Cargo)

Requires Rust 1.88+ (edition 2024).

git clone https://github.com/pulseengine/synth.git
cd synth
cargo build --release -p synth-cli

The binary is at target/release/synth. Add it to your PATH or invoke directly.

With Bazel

Bazel 8.x builds Rust, Rocq proofs, and Renode emulation tests hermetically via Nix.

bazel build //crates:synth

Quick Start

# 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.elf

To use Z3 translation validation, rebuild with the verify feature (requires Z3 on your system):

cargo build --release -p synth-cli --features verify
synth verify examples/wat/simple_add.wat firmware.elf

Features

Category	Status	Notes
i32 arithmetic, bitwise, comparison, shift/rotate	Tested	Full Rocq T1 proofs, Renode execution tests
i64 arithmetic (register pairs)	Tested	ADDS/ADC, SUBS/SBC, UMULL; unit tests only
f32 via VFP	Implemented	Requires FPU-equipped target (M4F, M7); Rocq T2 existence proofs
f64 via VFP	Not implemented	Decoded but rejected by instruction selector
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	233 Qed / 10 Admitted	i32 T1 proofs; division/constant proofs re-admitted for trap guard alignment
Z3 translation validation	53 tests passing	Covers i32 arithmetic and comparison rules
WebAssembly spec test suite	227/257 compile	Compilation only — not executed on emulator

What doesn't work yet

• No real hardware testing — all testing is unit tests and Renode emulation
• 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
• Register allocator is naive — wrapping allocation with reserved register exclusion, no graph coloring
• 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

Usage

Compile WASM/WAT to ARM ELF

# 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.elf

Disassemble

synth disasm add.elf

Translation validation

# Standalone verification: check that an ELF faithfully preserves WASM semantics
synth verify input.wat output.elf

List backends

synth backends

Compilation Pipeline

graph 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

Loading

Pipeline stages:

1. Parse -- decode WASM binary or WAT text via wasmparser/wat crates
2. Instruction selection -- pattern-match WASM ops to ARM instruction sequences (i32, i64, f32, f64, SIMD)
3. Peephole optimization -- redundant-op elimination, NOP removal, instruction fusion, constant propagation (0-25% code reduction)
4. ARM encoding -- emit 32-bit ARM / Thumb-2 machine code
5. ELF builder -- produce ELF32 with .text, .isr_vector, .data, .bss, symbol table; optional vector table and reset handler for Cortex-M

Formal Verification

Verification status

Per the PulseEngine Verification Guide, projects target multi-track verification. Current status:

Track	Status	Coverage
Rocq	Partial	233 Qed / 10 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).

Rocq proof suite

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.

233 Qed  /  10 Admitted
  T1: 35 result-correspondence (ARM output = WASM result)  — i32 only
  T2: 142 existence-only (ARM execution succeeds, no result claim)
  T3: 10 admitted (4 division trap guards, 1 constant encoding, 2 examples,
                    2 ArmRefinement Sail, 1 Integers.v Rocq 9 migration)
  Infrastructure: 56 (integer properties, state lemmas, flag lemmas, semantics helpers)

Only i32 arithmetic/bitwise operations have full T1 (result-correspondence) proofs. 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 i64, 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 proofs

See coq/STATUS.md for the per-file coverage matrix.

Z3 SMT translation validation

The synth-verify crate encodes WASM and ARM semantics as Z3 formulas and checks per-rule equivalence. The --verify CLI flag invokes this after compilation; synth verify provides standalone validation. 53 Z3 verification tests pass in CI.

Crate Map

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 encoder, ELF builder, vector table, linker scripts, MPU
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	Z3 SMT translation validation
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

Testing

# Run all Rust tests (895 tests across workspace)
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/...

Documentation

• 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

License

Apache-2.0 -- see LICENSE.

---

_{Part of PulseEngine — WebAssembly toolchain for safety-critical systems}