synth

Synth представляет собой AOT-компилятор, который принимает WebAssembly (в бинарном виде или в формате WAT) и генерирует bare-metal ELF-бинарные файлы для встраиваемых целей. Основным бэкендом является машинный код ARM Cortex-M (Thumb-2), также доступны бэкенды для ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3) и AArch64 в качестве хост-нативного таргета, выбираемого через -b aarch64. Бэкенд AArch64 также может создавать переносимый вывод, который линкуется в обычную статическую библиотеку arm64-Linux; полученный ET_REL проверяется в CI путем линковки с C-harness и выполнения с помощью wasmtime на раннере arm64-Linux, под qemu-user и unicorn; контракт эмбеддера документирован отдельно. Конвейер компиляции представляет собой простую цепочку: парсинг и декодирование через wasmparser/wat, выбор инструкций WASM-to-ARM, peephole-оптимизация (удаление избыточных операций, удаление NOP, слияние инструкций, распространение констант), кодирование ARM/Thumb-2 и вывод ELF32 с секциями .text, .isr_vector, .data, .bss и таблицей символов. Для Cortex-M предоставляются опциональная таблица векторов и обработчик сброса, а также генерируются скрипты линковщика для STM32, nRF52840 и универсальных плат. Кодовая база разделена на крейты, охватывающие CLI, основные типы и трейт бэкенда, фронтенд-парсинг, архитектурные бэкенды, выбор инструкций, проходы оптимизации CFG и IR, SMT-верификацию, подъем/понижение ABI, абстракцию памяти, интеграцию с QEMU, генерацию тестов WAST-to-Robot и парсинг WIT. Центральным утверждением проекта является отношение к функциональной безопасности как к проблеме сертификации с верифицируемой генерацией кода из WASM в небольшой целевой ISA. Механизированные доказательства в Rocq охватывают выбор инструкций i32 и i64 с теоремами о соответствии результатов (T1), в то время как выбор float и SIMD в настоящее время имеет доказательства только существования (T2). Теоремы правил Selector-DSL формулируются непосредственно для сгенерированной модели и извлекаются из одного источника (поставляемого набора правил), так что изменение таблицы селектора нарушает соответствующее доказательство. Количество доказательств и правил выводится машинным способом в JSON-файл статуса и контролируется через CI, а не вводится вручную. Валидация трансляции использует крейт synth-verify, который кодирует семантику WASM и ARM в виде формул QF_BV. Начиная с версии v0.27.0, движком по умолчанию является ordeal — чистый Rust-солвер QF_BV, не требующий C++ toolchain; Z3 доступен как дифференциальный оракул через feature-gate. Также сообщается о начале работы над harness-тестами ограниченной проверки моделей Kani и спецификациями функций Verus; работа с Lean еще не начата. Тестирование сочетает в себе модульные тесты Rust, эмуляцию Renode и QEMU, дифференциальное выполнение относительно wasmtime, а также прогоны на циклы и корректность в рамках фикстур на реальном железе Cortex-M (NUCLEO-G474RE, STM32F100). CI-воркфлоу компилирует набор тестов спецификации WebAssembly для каждого бэкенда и раздельно подсчитывает отклонения и ошибки, при этом количество строго зафиксировано и проверяется только для пути с одним модулем. В README четко указано, что еще не работает: ограниченный охват оборудования без широкой матрицы плат, многопамязевая модель (multi-memory) все еще находится на фазе 1, отсутствие WASI для встраиваемых систем, невозможность исполнения модели компонентов без еще не существующего крейта kiln-builtins, spill-on-exhaustion доступен только опционально, отсутствует оптимизация хвостовых вызовов (tail-call), а кодирование SIMD/Helium реализовано, но никогда не запускалось на железе или эмуляторе M55. Бенчмарк по размеру, регенерируемый из файла артефактов, показывает, что стандартный путь в 1.64x-3.48x больше, чем нативный C/Rust при -Os, снижаясь до 0.54x при использовании формы clamp с предоставленным сертификатом доказанного посыла; каждая ячейка циклов все еще помечена как открытая в ожидании измерений DWT на железе. Сборка требует Rust 1.88+ (edition 2024) с Cargo или Bazel 8.x с Nix для герметичных сборок Rust, доказательств Rocq и тестов Renode. Проект лицензирован под Apache-2.0 и является частью инструментария PulseEngine наряду с Loom (оптимизатор WASM с верификацией Z3), Meld (статический фьюзер Component Model), Kiln (WASM-рантайм для критически важных систем) и Sigil (аттестация и подпись цепочки поставок).