প্রকল্প সম্পর্কে

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 স্ট্যাটিক লাইব্রেরিতে লিঙ্ক করা যায়; resulting ET_REL-টি একটি C হারনেস-এর বিপরীতে লিঙ্ক করে এবং arm64-Linux রানারে wasmtime, qemu-user এবং unicorn-এর বিপরীতে এক্সিকিউট করে CI-তে যাচাই করা হয়; এমবেডার কন্ট্রাক্টটি আলাদাভাবে ডকুমেন্ট করা হয়েছে। কম্পাইলেশন পাইপলাইনটি একটি সহজ চেইন: 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 পার্সিং কভার করে। প্রজেক্টটির একটি কেন্দ্রীয় দাবি হলো ফাংশনাল সেফটি-কে একটি সার্টিফিকেশন সমস্যা হিসেবে বিবেচনা করা, যেখানে WASM থেকে একটি ছোট টার্গেট ISA-তে ভেরিফিয়েবল কোড জেনারেশন করা হয়। Rocq-এর মেকানাইজড প্রুফগুলো i32 এবং i64 ইন্সট্রাকশন সিলেকশনকে result-correspondence (T1) থিওরেম দিয়ে কভার করে, যেখানে ফ্লোট এবং SIMD সিলেকশনের জন্য বর্তমানে শুধুমাত্র existence-only (T2) প্রুফ রয়েছে। Selector-DSL রুল থিওরেমগুলো সরাসরি জেনারেটেড মডেলের উপর স্টেট করা হয়, যা শিপড রুল সেট থেকে সিঙ্গেল-সোর্স করা যাতে সিলেক্টর-টেবিল পরিবর্তন হলে ম্যাচিং প্রুফটি ভেঙে যায়। প্রুফ এবং রুলের সংখ্যাগুলো হাতে টাইপ করার পরিবর্তে একটি স্ট্যাটাস JSON ফাইলে মেশিন-ডেরাইভড করা হয় এবং CI-গেটেড থাকে। ট্রান্সলেশন ভ্যালিডেশনের জন্য synth-verify ক্রেট ব্যবহৃত হয়, যা WASM এবং ARM সেমানটিকসকে QF_BV ফর্মুলা হিসেবে এনকোড করে। v0.27.0 থেকে ডিফল্ট ইঞ্জিন হলো ordeal, যা একটি পিওর-রাস্ট QF_BV সলভার এবং এর জন্য কোনো C++ টুলচেইনের প্রয়োজন হয় না; Z3 একটি ফিচার-গেটেড ডিফারেনশিয়াল ওরাকল হিসেবে কাজ করে। প্রজেক্টটি Kani বাউন্ডেড মডেল চেকিং হারনেস এবং Verus স্পেক ফাংশনের কাজ শুরু করার কথা জানিয়েছে, তবে Lean-এর কাজ শুরু হয়নি। টেস্টিং-এ রাস্ট ইউনিট টেস্ট, Renode এবং QEMU এমুলেশন, wasmtime-এর বিপরীতে এক্সিকিউশন ডিফারেনশিয়াল এবং আসল Cortex-M সিলিকনে (NUCLEO-G474RE, STM32F100) ফিক্সচার-স্কোপড সাইকেল এবং কারেক্টনেস রান অন্তর্ভুক্ত। একটি CI ওয়ার্কফ্লো প্রতি ব্যাকএন্ড অনুযায়ী WebAssembly স্পেক টেস্ট স্যুট কম্পাইল করে এবং এর এরর থেকে আলাদাভাবে ডিক্লাইন গণনা করে, যেখানে গণনাগুলো নির্দিষ্টভাবে পিন করা থাকে এবং শুধুমাত্র সিঙ্গেল-মডিউল পাথে চেক করা হয়। README-তে স্পষ্টভাবে উল্লেখ করা হয়েছে যে কোন বিষয়গুলো এখনও কাজ করছে না: সীমিত হার্ডওয়্যার কভারেজ এবং কোনো বিস্তৃত বোর্ড ম্যাট্রিক্স নেই, মাল্টি-মেমোরি এখনও ফেজ ১-এ আছে, এমবেডেডে কোনো WASI নেই, এখনও বিদ্যমান নয় এমন kiln-builtins ক্রেট ছাড়া কম্পোনেন্ট মডেল এক্সিকিউশন নেই, spill-on-exhaustion এখনও অপ্ট-ইন, কোনো টেইল-কল অপ্টিমাইজেশন নেই, এবং SIMD/Helium এনকোডিং ইমপ্লিমেন্ট করা হলেও M55 সিলিকন বা এমুলেটরে কখনও চালানো হয়নি। একটি আর্টিফ্যাক্ট ফাইল থেকে পুনরুৎপাদিত মেজারড সাইজ বেঞ্চমার্ক রিপোর্ট করে যে, ডিফল্ট পাথ -Os-এ নেটিভ C/Rust-এর তুলনায় ১.৬৪ গুণ থেকে ৩.৪৮ গুণ বড়, তবে একটি প্রুভেন প্রিমিস সার্টিফিকেট প্রদান করা হলে এটি ০.৫৪ গুণ হয়ে আসে; সিলিকন DWT মেজারমেন্ট pending থাকায় প্রতিটি সাইকেল সেল এখনও ওপেন হিসেবে চিহ্নিত। বিল্ডের জন্য Cargo-সহ Rust 1.88+ (edition 2024), অথবা রাস্ট, Rocq প্রুফ এবং Renode টেস্টের হারমেটিক বিল্ডের জন্য Nix-সহ Bazel 8.x প্রয়োজন। প্রজেক্টটি Apache-2.0 লাইসেন্সপ্রাপ্ত এবং এটি PulseEngine টুলচেইনের অংশ, যার সাথে Loom (Z3 ভেরিফিকেশনসহ WASM অপ্টিমাইজার), Meld (Component Model স্ট্যাটিক ফিউজার), Kiln (সেফটি-ক্রিটিক্যাল সিস্টেমের জন্য WASM রানটাইম) এবং Sigil (সাপ্লাই চেইন অ্যাটেস্টেশন এবং সাইনিং) রয়েছে।