pulseengine · avrabe · Mar 21, 2026 · Mar 21, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,23 +5,50 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
-## [Unreleased]
-
-### Changed
-- Reorganized documentation structure - consolidated 41 root docs into organized `docs/` subdirectories
-- Documentation now organized by category: status, sessions, analysis, planning, research, build-systems, validation, architecture
+## [0.1.0] - 2026-03-21
 
 ### Added
-- GitHub project infrastructure: 40 labels, 4 milestones, 24 issues
-- Project board for tracking reorganization progress
 
-## [0.1.0] - TBD
+#### Compiler
+- WebAssembly-to-ARM Cortex-M AOT compiler
+- 197+ WASM opcodes supported (i32, i64, f32, f64, SIMD/Helium)
+- Full control flow (block, loop, if/else, br, br_if, br_table, call)
+- Sub-word memory operations (load8/16, store8/16)
+- memory.size / memory.grow
+- Globals, select, i64 register pairs
+- ARM Thumb-2 instruction encoding
+- VFP/FPU support (f32, f64)
+- WASM SIMD to ARM Helium MVE (Cortex-M55)
+
+#### Output
+- ELF binary output with vector table and startup code
+- Linker script generation (STM32, nRF52840, generic)
+- MPU region configuration
+- `synth compile --link` cross-compilation pipeline via arm-none-eabi-gcc
+
+#### CLI
+- `synth compile` -- compile WASM/WAT to ARM ELF
+- `synth disasm` -- disassemble ARM ELF binaries
+- `synth verify` -- Z3 SMT translation validation
+- `synth backends` -- list available compilation backends
+- Target profiles: cortex-m3, cortex-m4, cortex-m4f, cortex-m7, cortex-m7dp, cortex-m55
+
+#### Verification
+- Rocq mechanized proofs (188 Qed / 52 Admitted)
+- All i32 operations (arithmetic, division, comparison, bit-manip, shift/rotate) have T1 result-correspondence proofs
+- Z3 SMT translation validation (53 verification tests)
+- STPA safety analysis (losses, hazards, UCAs, constraints)
+- Rivet SDLC artifact traceability (250+ artifacts)
+
+#### Testing
+- 851 tests, all passing
+- 227/257 WebAssembly spec test files compile
+- Renode ARM Cortex-M4 emulation tests via Bazel
 
-### Planned
-- Working CLI: `synth compile input.wasm -o output.elf`
-- Calculator demo running on Zephyr/QEMU
-- Complete CI/CD pipeline
-- Comprehensive documentation
+#### Examples & Integrations
+- Zephyr RTOS integration examples
+- Anti-pinch window controller (automotive safety demo)
+- OSxCAR WASM compilation test
 
 ---
 

diff --git a/Cargo.toml b/Cargo.toml
@@ -26,6 +26,9 @@ rust-version = "1.88"
 authors = ["PulseEngine Team"]
 license = "Apache-2.0"
 repository = "https://github.com/pulseengine/synth"
+homepage = "https://github.com/pulseengine/synth"
+keywords = ["webassembly", "arm", "cortex-m", "compiler", "embedded"]
+categories = ["compilers", "embedded", "wasm", "no-std"]
 
 [workspace.dependencies]
 # WebAssembly tooling

diff --git a/README.md b/README.md
@@ -2,7 +2,7 @@
 
 # Synth
 
-<sup>WebAssembly-to-ARM compiler with mechanized correctness proofs</sup>
+<sup>WebAssembly-to-ARM Cortex-M AOT compiler with mechanized correctness proofs</sup>
 
 &nbsp;
 
@@ -29,7 +29,7 @@
 
 &nbsp;
 
-Synth compiles WebAssembly to native ARM Cortex-M machine code, producing bare-metal ELF binaries for embedded targets. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation -- with mechanized correctness proofs in [Rocq](https://rocq-prover.org/) (formerly Coq) and SMT-based translation validation via Z3.
+Synth compiles WebAssembly to native ARM Cortex-M machine code, producing bare-metal ELF binaries for embedded targets. It supports 197+ WASM opcodes (i32, i64, f32, f64, SIMD/Helium), full control flow, memory operations, and globals. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation -- with mechanized correctness proofs in [Rocq](https://rocq-prover.org/) (formerly Coq) and SMT-based translation validation via Z3.
 
 Part of [PulseEngine](https://github.com/pulseengine) -- a WebAssembly toolchain for safety-critical systems with mechanized verification:
 
@@ -44,7 +44,7 @@ Part of [PulseEngine](https://github.com/pulseengine) -- a WebAssembly toolchain
 
 ### From source (Cargo)
 
-Requires Rust 1.85+ (edition 2024).
+Requires Rust 1.88+ (edition 2024).
 
 ```bash
 git clone https://github.com/pulseengine/synth.git
@@ -62,6 +62,38 @@ Bazel 8.x builds Rust, Rocq proofs, and Renode emulation tests hermetically via
 bazel build //crates:synth
 ```
 
+## Quick Start
+
+```bash
+# 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
+
+# Formally verify the translation
+synth verify examples/wat/simple_add.wat firmware.elf
+```
+
+## Features
+
+| Category | Status |
+|----------|--------|
+| i32 arithmetic, bitwise, comparison, shift/rotate | Supported |
+| i64 arithmetic (register pairs) | Supported |
+| f32/f64 via VFP | Supported |
+| WASM SIMD via ARM Helium MVE | Supported (Cortex-M55) |
+| Control flow (block, loop, if/else, br, br_if, br_table) | Supported |
+| Function calls (direct, indirect) | Supported |
+| Memory (load/store, sub-word, size/grow) | Supported |
+| Globals, select, unreachable, nop | Supported |
+| ELF output with vector table | Supported |
+| Linker scripts (STM32, nRF52840, generic) | Supported |
+| Cross-compilation via arm-none-eabi-gcc | Supported |
+| Rocq mechanized proofs | 188 Qed / 52 Admitted |
+| Z3 translation validation | 53 tests passing |
+| WebAssembly spec test suite | 227/257 files compile |
+
 ## Usage
 
 ### Compile WASM/WAT to ARM ELF
@@ -120,7 +152,7 @@ graph LR
 **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 integer ops; f32/f64/i64 rejected at compile time)
+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
@@ -134,12 +166,14 @@ Synth employs two complementary verification strategies.
 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.
 
 ```
-154 Qed  /  71 Admitted  /  12 axioms
-  T1: 19 result-correspondence (ARM output = WASM result)
+188 Qed  /  52 Admitted
+  T1: 39 result-correspondence (ARM output = WASM result)
   T2: 95 existence-only (ARM execution succeeds)
-  T3: 71 admitted (VFP, flags, shifts)
+  T3: 52 admitted (VFP/float semantics)
 ```
 
+All i32 operations (arithmetic, division, comparison, bit-manip, shift/rotate) have full T1 proofs.
+
 Build the proofs:
 
 ```bash
@@ -173,7 +207,7 @@ The `synth-verify` crate encodes WASM and ARM semantics as Z3 formulas and check
 ## Testing
 
 ```bash
-# Run all Rust tests (521 tests across workspace)
+# Run all Rust tests (851 tests across workspace)
 cargo test --workspace
 
 # Lint

diff --git a/crates/synth-abi/Cargo.toml b/crates/synth-abi/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "WebAssembly Component Model ABI (lift/lower) for the Synth compiler"
 
 [dependencies]
 synth-wit = { path = "../synth-wit" }
diff --git a/crates/synth-analysis/Cargo.toml b/crates/synth-analysis/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "SSA and control flow analysis for the Synth compiler"
 
 [dependencies]
 synth-core = { path = "../synth-core" }

diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "aWsm backend integration for the Synth compiler"
 
 [dependencies]
 synth-core = { path = "../synth-core" }

diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "Wasker backend integration for the Synth compiler"
 
 [dependencies]
 synth-core = { path = "../synth-core" }

diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "ARM encoder, ELF builder, vector table, linker scripts, and MPU configuration"
 
 [features]
 default = ["arm-cortex-m"]

diff --git a/crates/synth-cfg/Cargo.toml b/crates/synth-cfg/Cargo.toml
@@ -5,5 +5,6 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "Control flow graph representation for the Synth compiler"
 
 [dependencies]
diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "CLI for Synth, the WebAssembly-to-ARM Cortex-M AOT compiler"
 
 [[bin]]
 name = "synth"

diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs
@@ -1,6 +1,7 @@
-//! Synth CLI - WebAssembly Component Synthesizer
+//! Synth CLI - WebAssembly-to-ARM Cortex-M AOT Compiler
 //!
-//! Command-line interface for the Synth synthesizer.
+//! Command-line interface for the Synth compiler. Compiles WASM/WAT files
+//! to bare-metal ARM Cortex-M ELF binaries with optional formal verification.
 
 use anyhow::{Context, Result};
 use clap::{Parser, Subcommand};
@@ -23,7 +24,17 @@ use wast::{Wast, WastDirective};
 
 #[derive(Parser)]
 #[command(name = "synth")]
-#[command(about = "WebAssembly Component Synthesizer for Embedded Systems", long_about = None)]
+#[command(about = "WebAssembly-to-ARM Cortex-M AOT compiler")]
+#[command(
+    long_about = "Synth compiles WebAssembly (WASM/WAT) to native ARM Cortex-M machine code,\n\
+producing bare-metal ELF binaries for embedded targets.\n\n\
+Examples:\n  \
+synth compile input.wat -o output.elf\n  \
+synth compile input.wat --cortex-m -o firmware.elf\n  \
+synth compile input.wat --cortex-m --link -o firmware.elf\n  \
+synth disasm firmware.elf\n  \
+synth verify input.wat firmware.elf"
+)]
 #[command(version)]
 struct Cli {
     #[command(subcommand)]
@@ -90,7 +101,7 @@ enum Commands {
         target: String,
     },
 
-    /// Compile WASM/WAT to ARM ELF
+    /// Compile WASM/WAT to ARM ELF (e.g., synth compile input.wat --cortex-m -o fw.elf)
     Compile {
         /// Input WASM or WAT file (optional, use --demo for built-in demos)
         #[arg(value_name = "INPUT")]
@@ -155,7 +166,7 @@ enum Commands {
         builtins: Option<PathBuf>,
     },
 
-    /// Disassemble an ARM ELF file
+    /// Disassemble an ARM ELF file (e.g., synth disasm output.elf)
     Disasm {
         /// Input ELF file
         #[arg(value_name = "INPUT")]
@@ -165,7 +176,7 @@ enum Commands {
     /// List available compilation backends and their status
     Backends,
 
-    /// Verify compilation correctness (translation validation)
+    /// Verify compilation correctness via Z3 (e.g., synth verify input.wat output.elf)
     Verify {
         /// Input WASM or WAT file (source)
         #[arg(value_name = "WASM")]

diff --git a/crates/synth-core/Cargo.toml b/crates/synth-core/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "Core types, error handling, and backend trait for the Synth compiler"
 
 [dependencies]
 serde.workspace = true

diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "WASM/WAT parser and module decoder frontend for the Synth compiler"
 
 [dependencies]
 synth-core = { path = "../synth-core" }

diff --git a/crates/synth-memory/Cargo.toml b/crates/synth-memory/Cargo.toml
@@ -2,8 +2,10 @@
 name = "synth-memory"
 version.workspace = true
 edition.workspace = true
+authors.workspace = true
 license.workspace = true
-description = "Portable memory management for Synth WASM-to-ARM compiler"
+repository.workspace = true
+description = "Portable memory abstraction (Zephyr, Linux, bare-metal) for the Synth compiler"
 
 [dependencies]
 bitflags = "2.4"

diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "Peephole optimization passes for the Synth compiler"
 
 [dependencies]
 synth-cfg = { path = "../synth-cfg" }

diff --git a/crates/synth-qemu/Cargo.toml b/crates/synth-qemu/Cargo.toml
@@ -5,5 +5,6 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "QEMU integration utilities for testing Synth-compiled ARM binaries"
 
 [dependencies]
diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "WASM-to-ARM instruction selection and peephole optimizer"
 
 [dependencies]
 synth-core = { path = "../synth-core" }

diff --git a/crates/synth-test/Cargo.toml b/crates/synth-test/Cargo.toml
@@ -4,7 +4,8 @@ version.workspace = true
 edition.workspace = true
 authors.workspace = true
 license.workspace = true
-description = "WAST-driven test runner for Synth"
+repository.workspace = true
+description = "WAST-to-Robot Framework test generator for Renode emulation"
 
 [dependencies]
 wast = { workspace = true }

diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml
@@ -5,6 +5,7 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "Z3 SMT translation validation for the Synth compiler"
 
 [features]
 default = ["z3-solver", "arm"]

diff --git a/crates/synth-wit/Cargo.toml b/crates/synth-wit/Cargo.toml
@@ -5,5 +5,6 @@ edition.workspace = true
 authors.workspace = true
 license.workspace = true
 repository.workspace = true
+description = "WIT (WebAssembly Interface Types) support for the Synth compiler"
 
 [dependencies]