synth

Synth 是一款提前编译（AOT）编译器，它将 WebAssembly（二进制或 WAT 文本）转换为面向嵌入式目标的裸机 ELF 二进制文件。其主要后端是 ARM Cortex-M (Thumb-2) 机器码，此外还支持 ARM Cortex-R5 (A32)、RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3)，以及通过 -b aarch64 选择的 AArch64 主机原生目标。AArch64 后端还可以生成可重定位输出，以便链接到标准的 arm64-Linux 静态库；生成的 ET_REL 在 CI 中通过链接 C 引导程序并在 arm64-Linux 运行器上针对 wasmtime、qemu-user 和 unicorn 执行来验证；嵌入式合约另有文档说明。 编译流水线是一个简单的链条：通过 wasmparser/wat 进行解析和解码，执行 WASM-to-ARM 指令选择，进行 peephole 优化（冗余操作消除、NOP 移除、指令融合、常量传播），进行 ARM/Thumb-2 编码，最后输出包含 .text、.isr_vector、.data、.bss 和符号表的 ELF32 文件。为 Cortex-M 提供了可选的向量表和复位处理程序，并生成了适用于 STM32、nRF52840 和通用开发板的链接脚本。代码库分为多个 crate，涵盖 CLI、核心类型和后端 trait、前端解析、架构后端、指令选择、CFG 和 IR 优化 pass、SMT 验证、ABI 提升/降低、内存抽象、QEMU 集成、WAST-to-Robot 测试生成以及 WIT 解析。 该项目的一个核心主张是将功能安全视为一个认证问题，实现从 WASM 到小型目标 ISA 的可验证代码生成。Rocq 中的机械化证明涵盖了具有结果对应（T1）定理的 i32 和 i64 指令选择，而浮点和 SIMD 选择目前仅具有存在性（T2）证明。Selector-DSL 规则定理直接针对生成的模型进行陈述，且与交付的规则集单源同步，因此选择表（selector-table）的任何更改都会导致匹配证明失效。证明和规则计数由机器导出到状态 JSON 文件中并通过 CI 门控，而非手动输入。 翻译验证使用 synth-verify crate，它将 WASM 和 ARM 语义编码为 QF_BV 公式。自 v0.27.0 起，默认引擎是 ordeal（一个无需 C++ 工具链的纯 Rust QF_BV 求解器）；Z3 则作为一个特性门控的差异化预言机（differential oracle）。项目还报告已开始开发 Kani 有界模型检查引导程序和 Verus 规范函数，而 Lean 尚未开始。 测试结合了 Rust 单元测试、Renode 和 QEMU 仿真、针对 wasmtime 的执行差异分析，以及在真实 Cortex-M 芯片（NUCLEO-G474RE, STM32F100）上进行的固定范围周期和正确性运行。CI 工作流按后端编译 WebAssembly 规范测试套件，并将拒绝数与错误数分开计数，计数被精确固定且仅在单模块路径上检查。 README 明确列出了目前尚未实现的功能：硬件覆盖范围狭窄，缺乏广泛的开发板矩阵；多内存（multi-memory）仍处于第一阶段；嵌入式端不支持 WASI；在尚未存在的 kiln-builtins crate 之前不支持组件模型执行；耗尽时溢出（spill-on-exhaustion）仍为可选配置；不支持尾调用优化；SIMD/Helium 编码已实现但从未在 M55 芯片或仿真器上运行。根据 artifacts 文件重新生成的尺寸基准测试报告，在 -Os 优化下，默认路径比原生 C/Rust 大 1.64x-3.48x，但在提供证明前提证书的 clamp 形状下可降至 0.54x；在等待芯片 DWT 测量之前，每个周期单元仍标记为 open。构建需要 Rust 1.88+ (edition 2024) 及 Cargo，或使用 Bazel 8.x 和 Nix 以实现 Rust、Rocq 证明和 Renode 测试的密封构建（hermetic builds）。该项目采用 Apache-2.0 许可，是 PulseEngine 工具链的一部分，其他组件包括 Loom（带 Z3 验证的 WASM 优化器）、Meld（组件模型静态融合器）、Kiln（面向安全关键系统的 WASM 运行时）和 Sigil（供应链证明与签名）。