From 2c7e7a09501cf6188d82193591ecc8c6504284a6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 21 Mar 2026 21:59:50 +0100 Subject: [PATCH] docs: refresh AGENTS.md via rivet init --agents MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Honest README: - Pre-release warning — not tested on real hardware - Features table distinguishes Tested/Implemented/Experimental - "What doesn't work yet" section added - Rocq proofs: only i32 has T1, 52 admits are all float - SIMD/Helium marked experimental (untested on M55) - Cross-compilation marked as not CI-tested - Spec tests: compile-only, not executed on emulator - Meld/Kiln descriptions corrected Co-Authored-By: Claude Opus 4.6 (1M context) --- README.md | 63 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 38 insertions(+), 25 deletions(-) diff --git a/README.md b/README.md index 965a91d..2cf68b7 100644 --- a/README.md +++ b/README.md @@ -29,16 +29,19 @@   -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. +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/f64 (via VFP), control flow, and memory operations. Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 instruction selection; i64/float/SIMD proofs are not yet done. -Part of [PulseEngine](https://github.com/pulseengine) -- a WebAssembly toolchain for safety-critical systems with mechanized verification: +**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](https://github.com/pulseengine) -- a WebAssembly toolchain for safety-critical embedded systems: | Project | Role | |---------|------| -| [**Synth**](https://github.com/pulseengine/synth) | WASM-to-ARM compiler with Rocq proofs | +| [**Synth**](https://github.com/pulseengine/synth) | WASM-to-ARM AOT compiler with Rocq proofs | | [**Loom**](https://github.com/pulseengine/loom) | WASM optimizer with Z3 verification | -| [**Meld**](https://github.com/pulseengine/meld) / [**Kiln**](https://github.com/pulseengine/kiln) | Platform runtime and build orchestration | -| [**Sigil**](https://github.com/pulseengine/sigil) | Attestation and signing | +| [**Meld**](https://github.com/pulseengine/meld) | WASM Component Model static fuser | +| [**Kiln**](https://github.com/pulseengine/kiln) | WASM runtime for safety-critical systems | +| [**Sigil**](https://github.com/pulseengine/sigil) | Supply chain attestation and signing | ## Installation @@ -77,22 +80,32 @@ 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 | +| 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/f64 via VFP | Implemented | Requires FPU-equipped target (M4F, M7); Rocq proofs admitted | +| 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 | 188 Qed / 52 Admitted | Only i32 has result-correspondence (T1); all 52 admits are float/VFP | +| 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 @@ -167,12 +180,12 @@ Mechanized proofs in Rocq 9 show that `compile_wasm_to_arm` preserves WASM seman ``` 188 Qed / 52 Admitted - T1: 39 result-correspondence (ARM output = WASM result) - T2: 95 existence-only (ARM execution succeeds) - T3: 52 admitted (VFP/float semantics) + T1: 39 result-correspondence (ARM output = WASM result) — i32 only + T2: 95 existence-only (ARM execution succeeds, no result claim) + T3: 52 admitted (VFP/float semantics — not yet proven) ``` -All i32 operations (arithmetic, division, comparison, bit-manip, shift/rotate) have full T1 proofs. +Only i32 operations have full T1 (result-correspondence) proofs. The i64, f32, f64, and SIMD instruction selection has NO mechanized proofs — correctness relies on unit tests and the Z3 translation validation. The 52 admitted theorems all require VFP floating-point semantics that are not yet modeled in Rocq. Build the proofs: