synth

Synth는 WebAssembly(바이너리 또는 WAT 텍스트)를 입력받아 임베디드 타겟을 위한 베어메탈 ELF 바이너리를 생성하는 AOT(ahead-of-time) 컴파일러입니다. 주요 백엔드는 ARM Cortex-M (Thumb-2) 머신 코드이며, ARM Cortex-R5 (A32), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), 그리고 -b aarch64를 통해 선택 가능한 호스트 네이티브 타겟인 AArch64 백엔드를 추가로 지원합니다. AArch64 백엔드는 일반적인 arm64-Linux 정적 라이브러리에 링크되는 재배치 가능 출력을 생성할 수 있으며, 결과물인 ET_REL은 C 하네스와 링크하여 arm64-Linux 러너 상의 wasmtime, qemu-user 및 unicorn에서 실행함으로써 CI에서 검증됩니다. 임베더 계약(embedder contract)은 별도로 문서화되어 있습니다. 컴파일 파이프라인은 단순한 체인 구조입니다: wasmparser/wat를 통한 파싱 및 디코딩, WASM-to-ARM 명령어 선택, 피프홀 최적화(중복 연산 제거, NOP 제거, 명령어 융합, 상수 전파), ARM/Thumb-2 인코딩, 그리고 .text, .isr_vector, .data, .bss 및 심볼 테이블을 포함한 ELF32 출력 순으로 진행됩니다. Cortex-M을 위한 선택적 벡터 테이블과 리셋 핸들러가 제공되며, STM32, nRF52840 및 일반 보드용 링커 스크립트가 생성됩니다. 코드베이스는 CLI, 코어 타입 및 백엔드 트레이트, 프론트엔드 파싱, 아키텍처 백엔드, 명령어 선택, CFG 및 IR 최적화 패스, SMT 검증, ABI lift/lower, 메모리 추상화, QEMU 통합, WAST-to-Robot 테스트 생성, WIT 파싱을 담당하는 크레이트(crates)들로 나뉘어 있습니다. 이 프로젝트의 핵심 주장은 기능적 안전성을 인증 문제로 취급하여, WASM에서 소규모 타겟 ISA로의 검증 가능한 코드 생성을 구현하는 것입니다. Rocq의 기계화 증명은 결과 대응(T1) 정리와 함께 i32 및 i64 명령어 선택을 다루며, 부동 소수점 및 SIMD 선택은 현재 존재 증명(T2)만 제공합니다. Selector-DSL 규칙 정리는 배포된 규칙 세트에서 단일 소스로 생성된 모델에 대해 직접 기술되므로, 셀렉터 테이블이 변경되면 일치하는 증명이 깨지게 됩니다. 증명 및 규칙 수는 수동으로 입력하지 않고 머신을 통해 JSON 상태 파일로 도출되어 CI 게이트로 관리됩니다. 번역 검증은 WASM 및 ARM 시맨틱을 QF_BV 공식으로 인코딩하는 synth-verify 크레이트를 사용합니다. v0.27.0부터는 C++ 툴체인이 필요 없는 순수 Rust QF_BV 솔버인 ordeal이 기본 엔진으로 사용되며, Z3는 기능 게이트가 설정된 차분 오라클(differential oracle)로 작동합니다. 또한 Kani 유한 모델 체킹 하네스와 Verus 사양 함수 작업에 착수했음을 보고했으며, Lean은 아직 시작되지 않았습니다. 테스트는 Rust 유닛 테스트, Renode 및 QEMU 에뮬레이션, wasmtime과의 실행 차분 분석, 그리고 실제 Cortex-M 실리콘(NUCLEO-G474RE, STM32F100)에서의 픽스처 범위 사이클 및 정확성 실행을 결합하여 수행합니다. CI 워크플로우는 백엔드별로 WebAssembly 사양 테스트 스위트를 컴파일하며, 오류와 별개로 거부(declines) 횟수를 집계하고, 이 횟수를 정확히 고정하여 단일 모듈 경로에서만 확인합니다. README에는 아직 작동하지 않는 사항들이 명시되어 있습니다: 광범위한 보드 매트릭스가 없는 좁은 하드웨어 커버리지, 1단계에 머물러 있는 멀티 메모리, 임베디드 환경의 WASI 미지원, 아직 존재하지 않는 kiln-builtins 크레이트 없이는 컴포넌트 모델 실행 불가, 선택 사항인 spill-on-exhaustion, 꼬리 호출 최적화(tail-call optimization) 미지원, 그리고 구현은 되었으나 M55 실리콘이나 에뮬레이터에서 실행된 적 없는 SIMD/Helium 인코딩 등이 그것입니다. 아티팩트 파일에서 재생성된 크기 벤치마크에 따르면, 기본 경로는 -Os 기준 네이티브 C/Rust보다 1.64배~3.48배 크지만, 증명된 전제 인증서가 제공되는 clamp shape에서는 0.54배까지 떨어집니다. 모든 사이클 셀은 실리콘 DWT 측정이 완료될 때까지 'open' 상태로 표시됩니다. 빌드에는 Cargo와 함께 Rust 1.88+(edition 2024) 또는 Rust, Rocq 증명 및 Renode 테스트의 허메틱 빌드를 위한 Nix 기반 Bazel 8.x가 필요합니다. 이 프로젝트는 Apache-2.0 라이선스를 따르며, Loom(Z3 검증 기반 WASM 최적화 도구), Meld(컴포넌트 모델 정적 퓨저), Kiln(안전 필수 시스템용 WASM 런타임), Sigil(공급망 증명 및 서명)과 함께 PulseEngine 툴체인의 일부입니다.