عن المشروع

Synth هو مترجم ahead-of-time يأخذ WebAssembly (سواء بصيغة ثنائية أو نصية WAT) ويصدر ملفات ELF ثنائية bare-metal للأهداف المدمجة. الواجهة الخلفية الأساسية له هي كود الآلة ARM Cortex-M (Thumb-2)، مع واجهات خلفية إضافية لـ ARM Cortex-R5 (A32)، و RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3)، و AArch64 كهدف أصلي للمضيف يتم اختياره عبر -b aarch64. يمكن للواجهة الخلفية AArch64 أيضاً إنتاج مخرجات قابلة للنقل يتم ربطها بمكتبة ثابتة arm64-Linux عادية، مع التحقق من ET_REL الناتج في CI عن طريق الربط مع C harness والتنفيذ مقابل wasmtime على مشغل arm64-Linux، وتحت qemu-user و unicorn؛ أما عقد المدمج (embedder contract) فموثق بشكل منفصل. خط أنابيب الترجمة هو سلسلة مباشرة: التحليل وفك التشفير عبر wasmparser/wat، واختيار التعليمات من WASM إلى ARM، وتحسين peephole (إزالة العمليات الزائدة، إزالة NOP، دمج التعليمات، ونشر الثوابت)، وتشفير ARM/Thumb-2، ومخرجات ELF32 تحتوي على .text و .isr_vector و .data و .bss وجدول رموز. يتم توفير جدول متجه اختياري ومعالج إعادة ضبط لـ Cortex-M، كما يتم إنشاء نصوص ربط (linker scripts) لـ STM32 و nRF52840 واللوحات العامة. تنقسم قاعدة الكود إلى crates تغطي واجهة السطر البرمجي (CLI)، الأنواع الأساسية و backend trait، تحليل الواجهة الأمامية، الواجهات الخلفية للمعمارية، اختيار التعليمات، تمريرات تحسين CFG و IR، التحقق من SMT، رفع/خفض ABI، تجريد الذاكرة، التكامل مع QEMU، توليد الاختبارات من WAST-to-Robot، وتحليل WIT. الادعاء المركزي للمشروع هو التعامل مع السلامة الوظيفية كمسألة شهادات، مع توليد كود قابل للتحقق من WASM إلى ISA هدف صغيرة. تغطي البراهين الميكانيكية في Rocq اختيار تعليمات i32 و i64 مع نظريات تطابق النتائج (T1)، بينما يمتلك اختيار float و SIMD حالياً براهين وجود فقط (T2). يتم صياغة نظريات قواعد Selector-DSL مباشرة حول النموذج المولد، والمستمد من مجموعة القواعد المشحونة بحيث يؤدي أي تغيير في جدول selector إلى كسر البرهان المطابق. يتم اشتقاق أعداد البراهين والقواعد آلياً في ملف JSON للحالة ويتم التحكم بها عبر CI بدلاً من كتابتها يدوياً. يستخدم التحقق من الترجمة crate المسمى synth-verify، والذي يشفر دلالات WASM و ARM كصيغ QF_BV. منذ الإصدار v0.27.0، المحرك الافتراضي هو ordeal، وهو حل QF_BV مكتوب بلغة Rust خالصة ولا يتطلب سلسلة أدوات C++؛ بينما يعد Z3 أوراكل تفاضلي محكوم بميزة (feature-gated). كما يشير المشروع إلى بدء العمل على Kani bounded model checking harnesses ودوال مواصفات Verus، بينما لم يبدأ العمل على Lean بعد. تجمع الاختبارات بين اختبارات الوحدة في Rust، ومحاكاة Renode و QEMU، والفروقات التنفيذية مقابل wasmtime، وتشغيلات الدورة والصحة المحددة بنطاق fixture على رقاقات Cortex-M حقيقية (NUCLEO-G474RE, STM32F100). يقوم سير عمل CI بترجمة مجموعة اختبارات مواصفات WebAssembly لكل واجهة خلفية ويقوم بحساب حالات الرفض بشكل منفصل عن الأخطاء، مع تثبيت الأعداد بدقة والتحقق منها في مسار الوحدة الواحدة فقط. يوضح ملف README صراحة ما لا يعمل بعد: تغطية محدودة للأجهزة دون مصفوفة لوحات واسعة، الذاكرة المتعددة لا تزال في المرحلة الأولى، لا يوجد WASI على الأنظمة المدمجة، لا يوجد تنفيذ لنموذج المكونات (component model) بدون crate المسمى kiln-builtins غير الموجود حالياً، خاصية spill-on-exhaustion لا تزال اختيارية، لا يوجد تحسين tail-call، وتشفير SIMD/Helium مُنفذ ولكن لم يتم تشغيله أبداً على رقاقة M55 أو محاكي. يشير معيار الحجم المقاس، الذي تمت إعادة توليده من ملف artifacts، أن المسار الافتراضي أكبر بـ 1.64x-3.48x من C/Rust الأصلي عند -Os، وينخفض إلى 0.54x في شكل clamp عند تزويده بشهادة مقدمة مثبتة؛ لا تزال كل خلية دورة (cycle cell) معلمة كمفتوحة بانتظار قياسات DWT للرقاقة. تتطلب عمليات البناء Rust 1.88+ (إصدار 2024) مع Cargo، أو Bazel 8.x مع Nix لبناءات محكمة (hermetic) لـ Rust وبراهين Rocq واختبارات Renode. المشروع مرخص بموجب Apache-2.0 وهو جزء من مجموعة أدوات PulseEngine إلى جانب Loom (محسن WASM مع تحقق Z3)، و Meld (دمج استاتيكي لنموذج المكونات)، و Kiln (بيئة تشغيل WASM للأنظمة ذات السلامة الحرجة) و Sigil (توثيق وتوقيع سلسلة التوريد).