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で検証されます。エンベッダー契約については別途ドキュメント化されています。 コンパイルパイプラインはシンプルなチェーン構造になっています。wasmparser/watによるパースとデコード、WASMからARMへの命令選択、ピープホール最適化（冗長操作の排除、NOP削除、命令融合、定数伝播）、ARM/Thumb-2エンコーディング、そして.text、.isr_vector、.data、.bssおよびシンボルテーブルを含むELF32出力という流れです。Cortex-M向けにはオプションのベクトルテーブルとリセットハンドラが提供され、STM32、nRF52840、および汎用ボード用のリンカスクリプトが生成されます。コードベースは、CLI、コア型とバックエンドトレイト、フロントエンドパース、アーキテクチャバックエンド、命令選択、CFGおよびIR最適化パス、SMT検証、ABIリフト/ロウア、メモリ抽象化、QEMU統合、WAST-to-Robotテスト生成、およびWITパースをカバーするクレートに分割されています。 本プロジェクトの中心的な主張は、機能安全性を認証問題として扱い、WASMから小規模なターゲットISAへの検証可能なコード生成を行うことです。Rocqによる機械化証明は、結果対応（T1）定理を伴うi32およびi64の命令選択をカバーしており、浮動小数点およびSIMDの選択については、現在は存在証明（T2）のみとなっています。Selector-DSLルールの定理は生成されたモデルに対して直接記述され、出荷されるルールセットからシングルソースで提供されるため、セレクタテーブルの変更は対応する証明を破綻させます。証明数とルール数は機械的に導出されてステータスJSONファイルに書き込まれ、手入力ではなくCIでゲート管理されています。 翻訳検証にはsynth-verifyクレートを使用し、WASMとARMのセマンティクスをQF_BV論理式としてエンコードします。v0.27.0以降、デフォルトエンジンはC++ツールチェーンを必要としない純Rust製QF_BVソルバーであるordealとなっており、Z3は機能ゲート付きの差分オラクルとして機能します。また、Kaniによる有界モデル検査ハーネスとVerus仕様関数の作業に着手したことが報告されており、Leanについては未着手です。 テストは、Rustユニットテスト、RenodeおよびQEMUエミュレーション、wasmtimeに対する実行差分、および実機Cortex-Mシリコン（NUCLEO-G474RE, STM32F100）でのフィクスチャ範囲のサイクルおよび正当性実行を組み合わせて行われます。CIワークフローでは、バックエンドごとにWebAssembly仕様テストスイートをコンパイルし、エラーとは別に拒否数をカウントし、その数は厳密に固定され、シングルモジュールパスでのみチェックされます。 READMEでは、未実装の事項が明記されています。ハードウェアカバレッジが狭く広範なボードマトリクスがないこと、マルチメモリがまだフェーズ1であること、組み込みでのWASI未対応、未実装のkiln-builtinsクレートなしでのコンポーネントモデル実行不可、spill-on-exhaustionが依然としてオプトインであること、末尾呼び出し最適化の不在、およびSIMD/Heliumエンコーディングは実装済みだがM55シリコンやエミュレータで実行されていないことなどが挙げられます。アーティファクトファイルから再生成されたサイズベンチマークでは、デフォルトパスは-Os時のネイティブC/Rustより1.64倍〜3.48倍大きく、証明済み前提証明書が提供されたクランプ形状では0.54倍まで低下します。すべてのサイクルセルは、シリコンDWT測定待ちのため依然としてオープンとされています。ビルドには、Cargoを伴うRust 1.88+ (edition 2024)、またはRust、Rocq証明、RenodeテストのハーメティックビルドのためのNixを伴うBazel 8.xが必要です。本プロジェクトはApache-2.0ライセンスであり、Loom（Z3検証付きWASM最適化器）、Meld（コンポーネントモデル静的フューザー）、Kiln（安全クリティカルシステム向けWASMランタイム）、Sigil（サプライチェーン証明および署名）と共にPulseEngineツールチェーンの一部を構成しています。