synth

Synth est un compilateur ahead-of-time qui prend du WebAssembly (binaire ou texte WAT) et émet des binaires ELF bare-metal pour des cibles embarquées. Son backend principal est le code machine ARM Cortex-M (Thumb-2), avec des backends supplémentaires pour ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), et AArch64 en tant que cible native hôte sélectionnée via -b aarch64. Le backend AArch64 peut également produire une sortie relocatable qui se lie à une bibliothèque statique arm64-Linux normale, l'ET_REL résultant étant vérifié en CI par liaison avec un harnais C et exécution contre wasmtime sur un runner arm64-Linux, sous qemu-user et sous unicorn ; le contrat de l'embedder est documenté séparément. Le pipeline de compilation est une chaîne simple : analyse et décodage via wasmparser/wat, sélection d'instructions WASM-to-ARM, optimisation peephole (élimination d'opérations redondantes, suppression de NOP, fusion d'instructions, propagation de constantes), encodage ARM/Thumb-2, et sortie ELF32 avec .text, .isr_vector, .data, .bss et une table de symboles. Une table de vecteurs et un gestionnaire de reset optionnels sont fournis pour Cortex-M, et des scripts de liaison pour STM32, nRF52840 et des cartes génériques sont générés. La base de code est divisée en crates couvrant le CLI, les types de base et le trait backend, l'analyse frontend, les backends d'architecture, la sélection d'instructions, les passes d'optimisation CFG et IR, la vérification SMT, le lift/lower ABI, l'abstraction mémoire, l'intégration QEMU, la génération de tests WAST-to-Robot, et l'analyse WIT. Une affirmation centrale du projet est la sécurité fonctionnelle traitée comme un problème de certification, avec une génération de code vérifiable de WASM vers un petit ISA cible. Des preuves mécanisées dans Rocq couvrent la sélection d'instructions i32 et i64 avec des théorèmes de correspondance de résultat (T1), tandis que la sélection float et SIMD ne possède actuellement que des preuves d'existence (T2). Les théorèmes de règles Selector-DSL sont énoncés directement sur le modèle généré, sourcés unique depuis l'ensemble de règles expédié afin qu'un changement de table de sélection brise la preuve correspondante. Les nombres de preuves et de règles sont dérivés par machine dans un fichier JSON de statut et verrouillés par CI plutôt que saisis manuellement. La validation de la traduction utilise la crate synth-verify, qui encode les sémantiques WASM et ARM sous forme de formules QF_BV. Depuis la v0.27.0, le moteur par défaut est ordeal, un solveur QF_BV en pur Rust ne nécessitant aucune chaîne d'outils C++ ; Z3 est un oracle différentiel activé par feature. Le projet signale également le début des travaux sur des harnais de model checking borné Kani et des fonctions de spécification Verus, Lean n'ayant pas encore débuté. Les tests combinent des tests unitaires Rust, l'émulation Renode et QEMU, des différentiels d'exécution contre wasmtime, et des exécutions de cycles et de correction basées sur des fixtures sur du silicium Cortex-M réel (NUCLEO-G474RE, STM32F100). Un workflow CI compile la suite de tests de spécification WebAssembly par backend et compte les déclins séparément des erreurs, avec des comptes fixés exactement et vérifiés uniquement sur le chemin module unique. Le README est explicite sur ce qui ne fonctionne pas encore : une couverture matérielle étroite sans matrice large de cartes, le multi-mémoire toujours en phase 1, pas de WASI sur l'embarqué, pas d'exécution du modèle de composants sans la crate kiln-builtins inexistante, le spill-on-exhaustion toujours optionnel, pas d'optimisation de tail-call, et l'encodage SIMD/Helium implémenté mais jamais exécuté sur du silicium M55 ou émulateur. Le benchmark de taille mesurée, régénéré à partir d'un fichier d'artefacts, rapporte que le chemin par défaut est 1,64x à 3,48x plus grand que le C/Rust natif en -Os, tombant à 0,54x sur une forme clamp lorsqu'un certificat de prémisse prouvé est fourni ; chaque cellule de cycle est toujours marquée ouverte en attendant les mesures DWT du silicium. Les builds nécessitent Rust 1.88+ (édition 2024) avec Cargo, ou Bazel 8.x avec Nix pour des builds hermétiques de Rust, des preuves Rocq et des tests Renode. Le projet est sous licence Apache-2.0 et fait partie de la chaîne d'outils PulseEngine aux côtés de Loom (optimiseur WASM avec vérification Z3), Meld (fuseur statique de Component Model), Kiln (runtime WASM pour systèmes critiques) et Sigil (attestation et signature de la chaîne d'approvisionnement).