इस प्रोजेक्ट के बारे में

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), और -b aarch64 के माध्यम से चयनित होस्ट-नेटिव टारगेट के रूप में AArch64 के लिए अतिरिक्त बैकएंड शामिल हैं। AArch64 बैकएंड ऐसा relocatable आउटपुट भी बना सकता है जो एक सामान्य arm64-Linux स्टैटिक लाइब्रेरी में लिंक होता है, जिसके परिणामस्वरूप ET_REL को CI में एक C हार्नेस के विरुद्ध लिंक करके और arm64-Linux रनर पर wasmtime, qemu-user और unicorn के तहत निष्पादित करके सत्यापित किया जाता है; एम्बेडर कॉन्ट्रैक्ट को अलग से प्रलेखित किया गया है। कंपाइलेशन पाइपलाइन एक सीधा क्रम है: wasmparser/wat के माध्यम से पार्स और डिकोड, WASM-to-ARM इंस्ट्रक्शन सिलेक्शन, पीपहोल ऑप्टिमाइज़ेशन (redundant-op एलिमिनेशन, NOP रिमूवल, इंस्ट्रक्शन फ्यूजन, कॉन्स्टेंट प्रोपेगेशन), ARM/Thumb-2 एन्कोडिंग, और .text, .isr_vector, .data, .bss और एक सिंबल टेबल के साथ ELF32 आउटपुट। Cortex-M के लिए वैकल्पिक वेक्टर टेबल और रिसेट हैंडलर प्रदान किए गए हैं, और STM32, nRF52840 और जेनेरिक बोर्ड के लिए लिंकर स्क्रिप्ट जेनरेट किए जाते हैं। कोडबेस को क्रेट्स (crates) में विभाजित किया गया है जो CLI, कोर टाइप्स और बैकएंड ट्रेट, फ्रंटएंड पार्सिंग, आर्किटेक्चर बैकएंड, इंस्ट्रक्शन सिलेक्शन, CFG और IR ऑप्टिमाइज़ेशन पासेस, SMT वेरिफिकेशन, ABI lift/lower, मेमोरी एब्स्ट्रैक्शन, QEMU इंटीग्रेशन, WAST-to-Robot टेस्ट जनरेशन, और WIT पार्सिंग को कवर करते हैं। प्रोजेक्ट का एक केंद्रीय दावा कार्यात्मक सुरक्षा (functional safety) को एक सर्टिफिकेशन समस्या के रूप में मानना है, जिसमें WASM से एक छोटे टारगेट ISA तक सत्यापन योग्य कोड जनरेशन शामिल है। Rocq में मैकेनाइज्ड प्रूफ i32 और i64 इंस्ट्रक्शन सिलेक्शन को रिज़ल्ट-कॉरेस्पोंडेंस (T1) थ्योरम्स के साथ कवर करते हैं, जबकि फ्लोट और SIMD सिलेक्शन में वर्तमान में केवल अस्तित्व-मात्र (T2) प्रूफ हैं। Selector-DSL नियम थ्योरम्स सीधे जेनरेटेड मॉडल के बारे में बताए गए हैं, जो शिप किए गए नियम सेट से सिंगल-सोर्स्ड हैं ताकि सेलेक्टर-टेबल में बदलाव होने पर मैचिंग प्रूफ टूट जाए। प्रूफ और नियम गणना मशीन-व्युत्पन्न होकर एक स्टेटस JSON फ़ाइल में जाती है और हाथ से टाइप करने के बजाय CI-गेटेड होती है। ट्रांसलेशन वैलिडेशन synth-verify क्रेट का उपयोग करता है, जो WASM और ARM सिमेंटिक्स को QF_BV फॉर्मूला के रूप में एनकोड करता है। v0.27.0 से डिफॉल्ट इंजन ordeal है, जो एक शुद्ध-Rust QF_BV सॉल्वर है जिसे किसी C++ टूलचेन की आवश्यकता नहीं होती; Z3 एक फीचर-गेटेड डिफरेंशियल ओरेकल है। प्रोजेक्ट ने Kani बाउंडेड मॉडल चेकिंग हार्नेस और Verus स्पेक फंक्शन्स पर काम शुरू करने की सूचना भी दी है, जबकि Lean पर काम शुरू नहीं हुआ है। टेस्टिंग में Rust यूनिट टेस्ट, Renode और QEMU इम्यूलेशन, wasmtime के विरुद्ध एक्जीक्यूशन डिफरेंशियल्स, और वास्तविक Cortex-M सिलिकॉन (NUCLEO-G474RE, STM32F100) पर फिक्स्चर-स्कोप साइकिल और शुद्धता रन शामिल हैं। एक CI वर्कफ़्लो प्रति बैकएंड WebAssembly स्पेक टेस्ट सूट को कंपाइल करता है और त्रुटियों से अलग गिरावट (declines) की गणना करता है, जिसमें गणना सटीक रूप से पिन की गई है और केवल सिंगल-मॉड्यूल पाथ पर जांची जाती है। README स्पष्ट रूप से बताता है कि अभी क्या काम नहीं करता है: व्यापक बोर्ड मैट्रिक्स के बिना सीमित हार्डवेयर कवरेज, मल्टी-मेमोरी अभी भी चरण 1 में है, एम्बेडेड पर कोई WASI नहीं, बिना kiln-builtins क्रेट (जो अभी मौजूद नहीं है) के कोई कंपोनेंट मॉडल निष्पादन नहीं, spill-on-exhaustion अभी भी opt-in है, कोई टेल-कॉल ऑप्टिमाइज़ेशन नहीं, और SIMD/Helium एन्कोडिंग लागू है लेकिन M55 सिलिकॉन या इम्यूलेटर पर कभी नहीं चलाया गया। आर्टिफैक्ट्स फ़ाइल से पुन: उत्पन्न मापा गया साइज़ बेंचमार्क, डिफॉल्ट पाथ को -Os पर नेटिव C/Rust की तुलना में 1.64x-3.48x बड़ा बताता है, जो एक प्रमाणित प्रिमिस सर्टिफिकेट दिए जाने पर क्लैंप शेप पर 0.54x तक गिर जाता है; सिलिकॉन DWT माप लंबित होने तक हर साइकिल सेल अभी भी ओपन चिह्नित है। बिल्ड्स के लिए Cargo के साथ Rust 1.88+ (संस्करण 2024), या Rust, Rocq प्रूफ और Renode टेस्ट के हर्मेटिक बिल्ड्स के लिए Nix के साथ Bazel 8.x की आवश्यकता होती है। प्रोजेक्ट Apache-2.0 के तहत लाइसेंस प्राप्त है और PulseEngine टूलचेन का हिस्सा है, जिसमें Loom (Z3 वेरिफिकेशन के साथ WASM ऑप्टिमाइज़र), Meld (कंपोनेंट मॉडल स्टैटिक फ्यूज़र), Kiln (सुरक्षा-महत्वपूर्ण प्रणालियों के लिए WASM रनटाइम) और Sigil (सप्लाई चेन एटेस्टेशन और साइनिंग) शामिल हैं।