منصوبے کے بارے میں

Synth ایک ahead-of-time کمپائلر ہے جو WebAssembly (بائنری یا WAT ٹیکسٹ) کو لیتا ہے اور ایمبیڈڈ ٹارگٹس کے لیے bare-metal ELF بائنریز جاری کرتا ہے۔ اس کا بنیادی بیک اینڈ ARM Cortex-M (Thumb-2) مشین کوڈ ہے، جس کے ساتھ ARM Cortex-R5 (A32)، RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3)، اور AArch64 کے لیے اضافی بیک اینڈز موجود ہیں جسے -b aarch64 کے ذریعے منتخب کیا جاتا ہے۔ AArch64 بیک اینڈ ایسی relocatable آؤٹ پٹ بھی پیدا کر سکتا ہے جو ایک عام arm64-Linux اسٹیٹک لائبریری میں لنک ہو جاتی ہے، جس کے نتیجے میں حاصل ہونے والے ET_REL کی تصدیق CI میں ایک C harness کے خلاف لنک کرنے اور arm64-Linux رنر پر wasmtime، qemu-user اور unicorn کے تحت چلانے سے کی جاتی ہے؛ ایمبیڈر کنٹریکٹ کی دستاویزات علیحدہ طور پر موجود ہیں۔ کمپائلیشن پائپ لائن ایک سادہ زنجیر ہے: wasmparser/wat کے ذریعے پارس اور ڈی کوڈ، WASM-to-ARM انسٹرکشن سلیکشن، peephole optimization (redundant-op خاتمہ، NOP خاتمہ، انسٹرکشن فیوژن، constant propagation)، ARM/Thumb-2 انکوڈنگ، اور .text، .isr_vector، .data، .bss اور ایک سمبل ٹیبل کے ساتھ ELF32 آؤٹ پٹ۔ Cortex-M کے لیے اختیاری vector table اور reset handler فراہم کیے گئے ہیں، اور STM32، nRF52840 اور generic بورڈز کے لیے لنکر اسکرپٹس تیار کیے جاتے ہیں۔ کوڈ بیس کو مختلف crates میں تقسیم کیا گیا ہے جو CLI، کور ٹائپس اور بیک اینڈ trait، فرنٹ اینڈ پارسنگ، آرکیٹیکچر بیک اینڈز، انسٹرکشن سلیکشن، CFG اور IR optimization پاسز، SMT ویریفیکیشن، ABI lift/lower، میموری abstraction، QEMU انٹیگریشن، WAST-to-Robot ٹیسٹ جنریشن، اور WIT پارسنگ کا احاطہ کرتے ہیں۔ پروجیکٹ کا ایک مرکزی دعویٰ فنکشنل سیفٹی ہے جسے سرٹیفیکیشن کے مسئلے کے طور پر دیکھا گیا ہے، جس میں WASM سے ایک چھوٹے ٹارگٹ ISA تک قابل تصدیق کوڈ جنریشن شامل ہے۔ Rocq میں میکنائزڈ ثبوت i32 اور i64 انسٹرکشن سلیکشن کو result-correspondence (T1) تھیورمز کے ساتھ کور کرتے ہیں، جبکہ float اور SIMD سلیکشن کے لیے فی الحال صرف existence-only (T2) ثبوت موجود ہیں۔ Selector-DSL رول تھیورمز براہ راست تیار کردہ ماڈل کے بارے میں بیان کیے گئے ہیں، جو فراہم کردہ رول سیٹ سے سنگل-سورسڈ ہیں تاکہ سلیکٹر-ٹیبل میں تبدیلی میچنگ پروف کو توڑ دے۔ پروف اور رولز کی تعداد مشین کے ذریعے ایک status JSON فائل میں اخذ کی جاتی ہے اور ہاتھ سے ٹائپ کرنے کے بجائے CI-gated ہوتی ہے۔ ٹرانسلیشن ویلیڈیشن synth-verify crate کا استعمال کرتی ہے، جو WASM اور ARM سیمیٹکس کو QF_BV فارمولوں کے طور پر انکوڈ کرتا ہے۔ v0.27.0 سے ڈیفالٹ انجن ordeal ہے، جو ایک خالص-Rust QF_BV سالور ہے جس کے لیے کسی C++ ٹول چین کی ضرورت نہیں؛ Z3 ایک feature-gated differential oracle ہے۔ پروجیکٹ نے Kani bounded model checking harnesses اور Verus spec functions پر کام شروع کرنے کی اطلاع بھی دی ہے، جبکہ Lean پر کام شروع نہیں ہوا۔ ٹیسٹنگ میں Rust یونٹ ٹیسٹ، Renode اور QEMU ایمولیشن، wasmtime کے خلاف execution differentials، اور حقیقی Cortex-M سلیکون (NUCLEO-G474RE, STM32F100) پر fixture-scoped سائیکل اور درستگی کے رنز شامل ہیں۔ ایک CI ورک فلو ہر بیک اینڈ کے لیے WebAssembly spec ٹیسٹ سویٹ کو کمپائل کرتا ہے اور declines کو غلطیوں سے الگ گنتا ہے، جس کی تعداد بالکل پن کی گئی ہے اور صرف سنگل-ماڈیول پاتھ پر چیک کی جاتی ہے۔ README واضح طور پر بتاتا ہے کہ ابھی کیا کام نہیں کرتا: محدود ہارڈ ویئر کوریج جس میں کوئی وسیع بورڈ میٹرکس نہیں ہے، multi-memory ابھی مرحلہ 1 میں ہے، ایمبیڈڈ پر کوئی WASI نہیں، kiln-builtins crate (جو ابھی موجود نہیں ہے) کے بغیر کوئی component model execution نہیں، spill-on-exhaustion ابھی opt-in ہے، کوئی tail-call optimization نہیں، اور SIMD/Helium انکوڈنگ نافذ ہے لیکن M55 سلیکون یا ایمولیٹر پر کبھی نہیں چلائی گئی۔ پیمائش شدہ سائز بینچ مارک، جو ایک artifacts فائل سے دوبارہ تیار کیا گیا ہے، رپورٹ کرتا ہے کہ ڈیفالٹ پاتھ -Os پر نیٹو C/Rust سے 1.64x-3.48x بڑا ہے، جو کہ ایک proven premise سرٹیفکیٹ فراہم کیے جانے پر clamp shape پر 0.54x تک گر جاتا ہے؛ ہر سائیکل سیل ابھی سلیکون DWT پیمائشوں کے انتظار میں کھلا ہے بلڈز کے لیے Rust 1.88+ (ایڈیشن 2024) Cargo کے ساتھ، یا Bazel 8.x Nix کے ساتھ Rust، Rocq پروفز اور Renode ٹیسٹ کے hermetic بلڈز کے لیے درکار ہیں۔ پروجیکٹ Apache-2.0 لائسنس کے تحت ہے اور PulseEngine ٹول چین کا حصہ ہے جس میں Loom (Z3 ویریفیکیشن کے ساتھ WASM آپٹیمائزر)، Meld (Component Model اسٹیٹک فیوژر)، Kiln (سیفٹی-کریٹیکل سسٹمز کے لیے WASM رن ٹائم) اور Sigil (سپلائی چین تصدیق اور سائننگ) شامل ہیں۔