synth

Synth é um compilador ahead-of-time que recebe WebAssembly (binário ou texto WAT) e emite binários ELF bare-metal para alvos embarcados. Seu backend principal é o código de máquina ARM Cortex-M (Thumb-2), com backends adicionais para ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3) e AArch64 como um alvo nativo do host selecionado via -b aarch64. O backend AArch64 também pode produzir saída relocável que se vincula a uma biblioteca estática arm64-Linux normal, com o ET_REL resultante verificado em CI vinculando-se a um harness em C e executando contra o wasmtime em um executor arm64-Linux, sob qemu-user e sob unicorn; o contrato do embedder é documentado separadamente. O pipeline de compilação é uma cadeia direta: análise e decodificação via wasmparser/wat, seleção de instruções WASM-para-ARM, otimização peephole (eliminação de op redundante, remoção de NOP, fusão de instruções, propagação de constantes), codificação ARM/Thumb-2 e saída ELF32 com .text, .isr_vector, .data, .bss e uma tabela de símbolos. Tabela de vetores opcional e manipulador de reset são fornecidos para Cortex-M, e scripts de linker para STM32, nRF52840 e placas genéricas são gerados. A base de código é dividida em crates que cobrem a CLI, tipos principais e trait de backend, parsing de frontend, backends de arquitetura, seleção de instruções, passes de otimização de CFG e IR, verificação SMT, lift/lower de ABI, abstração de memória, integração QEMU, geração de testes WAST-to-Robot e parsing de WIT. Uma reivindicação central do projeto é a segurança funcional tratada como um problema de certificação, com geração de código verificável de WASM para uma ISA de alvo pequena. Provas mecanizadas em Rocq cobrem a seleção de instruções i32 e i64 com teoremas de correspondência de resultado (T1), enquanto a seleção de float e SIMD possui atualmente apenas provas de existência (T2). Teoremas de regras de Selector-DSL são declarados diretamente sobre o modelo gerado, com fonte única do conjunto de regras enviado, de modo que uma alteração na tabela de seletores quebra a prova de correspondência. As contagens de provas e regras são derivadas por máquina em um arquivo JSON de status e controladas por CI, em vez de digitadas manualmente. A validação de tradução utiliza a crate synth-verify, que codifica a semântica de WASM e ARM como fórmulas QF_BV. Desde a v0.27.0, o motor padrão é o ordeal, um solver QF_BV em Rust puro que não requer toolchain C++; o Z3 é um oráculo diferencial controlado por feature. O projeto também relata o início do trabalho em harnesses de bounded model checking do Kani e funções de especificação Verus, com o Lean ainda não iniciado. Os testes combinam testes unitários em Rust, emulação Renode e QEMU, diferenciais de execução contra o wasmtime e execuções de ciclo e correção com escopo de fixture em silício Cortex-M real (NUCLEO-G474RE, STM32F100). Um workflow de CI compila a suíte de testes de especificação WebAssembly por backend e conta declínios separadamente de erros, com contagens fixadas exatamente e verificadas apenas no caminho de módulo único. O README é explícito sobre o que ainda não funciona: cobertura de hardware limitada sem uma matriz ampla de placas, multi-memória ainda na fase 1, sem WASI em embarcados, sem execução de modelo de componentes sem a crate kiln-builtins (ainda inexistente), spill-on-exhaustion ainda opcional, sem otimização de tail-call, e codificação SIMD/Helium implementada, mas nunca executada em silício ou simulador M55. O benchmark de tamanho medido, regenerado a partir de um arquivo de artefatos, relata o caminho padrão entre 1,64x e 3,48x maior que C/Rust nativo em -Os, caindo para 0,54x em uma forma de clamp quando fornecido um certificado de premissa provada; cada célula de ciclo ainda está marcada como aberta aguardando medições DWT de silício. As builds requerem Rust 1.88+ (edição 2024) com Cargo, ou Bazel 8.x com Nix para builds herméticas de Rust, provas Rocq e testes Renode. O projeto é licenciado sob Apache-2.0 e faz parte da toolchain PulseEngine ao lado de Loom (otimizador WASM com verificação Z3), Meld (fuser estático de Component Model), Kiln (runtime WASM para sistemas críticos de segurança) e Sigil (atestação e assinatura de cadeia de suprimentos).