synth

Synth es un compilador ahead-of-time que toma WebAssembly (binario o texto WAT) y emite binarios ELF bare-metal para objetivos embebidos. Su backend principal es código máquina ARM Cortex-M (Thumb-2), con backends adicionales para ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3) y AArch64 como objetivo nativo del host seleccionado mediante -b aarch64. El backend AArch64 también puede producir una salida reubicable que se vincula a una biblioteca estática normal de arm64-Linux, con el ET_REL resultante verificado en CI vinculándolo contra un arnés de C y ejecutándolo contra wasmtime en un ejecutor de arm64-Linux, bajo qemu-user y bajo unicorn; el contrato del embebedor se documenta por separado. El pipeline de compilación es una cadena directa: análisis y decodificación a través de wasmparser/wat, selección de instrucciones WASM-to-ARM, optimización peephole (eliminación de operaciones redundantes, eliminación de NOP, fusión de instrucciones, propagación de constantes), codificación ARM/Thumb-2 y salida ELF32 con .text, .isr_vector, .data, .bss y una tabla de símbolos. Se proporcionan una tabla de vectores y un manejador de reset opcionales para Cortex-M, y se generan scripts de enlazador para STM32, nRF52840 y placas genéricas. El código base se divide en crates que cubren la CLI, tipos principales y trait de backend, análisis de frontend, backends de arquitectura, selección de instrucciones, pases de optimización de CFG e IR, verificación SMT, elevación/descenso de ABI, abstracción de memoria, integración con QEMU, generación de pruebas WAST-to-Robot y análisis de WIT. Una afirmación central del proyecto es la seguridad funcional tratada como un problema de certificación, con generación de código verificable desde WASM hacia una ISA de destino pequeña. Las pruebas mecanizadas en Rocq cubren la selección de instrucciones i32 e i64 con teoremas de correspondencia de resultados (T1), mientras que la selección de float y SIMD actualmente tiene pruebas solo de existencia (T2). Los teoremas de reglas de Selector-DSL se establecen directamente sobre el modelo generado, provenientes de una única fuente del conjunto de reglas enviado, de modo que un cambio en la tabla de selectores rompe la prueba de coincidencia. Los recuentos de pruebas y reglas se derivan mediante máquina en un archivo JSON de estado y están restringidos por CI en lugar de escribirse a mano. La validación de la traducción utiliza el crate synth-verify, que codifica la semántica de WASM y ARM como fórmulas QF_BV. Desde la v0.27.0, el motor predeterminado es ordeal, un solver QF_BV puro en Rust que no requiere toolchain de C++; Z3 es un oráculo diferencial restringido por feature. El proyecto también informa el inicio del trabajo en arneses de model checking acotado de Kani y funciones de especificación de Verus, mientras que Lean no ha comenzado. Las pruebas combinan pruebas unitarias de Rust, emulación de Renode y QEMU, diferenciales de ejecución contra wasmtime y ejecuciones de corrección y ciclos con alcance de fixture en silicio Cortex-M real (NUCLEO-G474RE, STM32F100). Un flujo de trabajo de CI compila la suite de pruebas de la especificación de WebAssembly por backend y cuenta las declinaciones separadamente de los errores, con recuentos fijados exactamente y verificados solo en la ruta de módulo único. El README es explícito sobre lo que aún no funciona: cobertura de hardware limitada sin una matriz amplia de placas, multi-memoria aún en fase 1, sin WASI en embebidos, sin ejecución del modelo de componentes sin el crate kiln-builtins (aún inexistente), spill-on-exhaustion aún opcional, sin optimización de tail-call, y la codificación SIMD/Helium implementada pero nunca ejecutada en silicio o emulador M55. El benchmark de tamaño medido, regenerado desde un archivo de artefactos, reporta que la ruta predeterminada es entre 1.64x y 3.48x más grande que C/Rust nativo en -Os, bajando a 0.54x en una forma de clamp cuando se suministra un certificado de premisa probado; cada celda de ciclo sigue marcada como abierta a la espera de mediciones DWT de silicio. Las compilaciones requieren Rust 1.88+ (edición 2024) con Cargo, o Bazel 8.x con Nix para compilaciones herméticas de Rust, pruebas de Rocq y pruebas de Renode. El proyecto tiene licencia Apache-2.0 y es parte de la toolchain PulseEngine junto con Loom (optimizador WASM con verificación Z3), Meld (fusor estático de Component Model), Kiln (runtime WASM para sistemas críticos de seguridad) y Sigil (atestación y firma de la cadena de suministro).