بررسی Lean در Jolt اعتماد به zkVM را به مرز گسترش دستورها منتقل می‌کند

LayerZero در ۲۳ سپتامبر اعلام کرد که فرایند گسترش بایت‌کد Jolt به‌صورت رسمی در Lean بررسی شده است. این نتیجه یک مرز محدود اما مهم را هدف می‌گیرد: وقتی Jolt با دستور RISC-Vای روبه‌رو می‌شود که مستقیماً آن را پیاده‌سازی نکرده، آن دستور را با توالی‌ای از دستورهای Jolt جایگزین می‌کند. این بررسی نشان می‌دهد که توالی جدید برای همهٔ ورودی‌ها، دستور اصلی را به‌درستی شبیه‌سازی می‌کند؛ نه فقط برای نمونه‌های آزمایشی.

اهمیت موضوع از این‌جا می‌آید که اثبات zkVM تنها زمانی مفید است که ماشینی که اثبات می‌شود با ماشینی که توسعه‌دهنده قصد اجرای آن را داشته، یکسان باشد. معماری Jolt بایت‌کد را به‌عنوان منبعی مبتنی بر lookup برای داده‌های دستور در نظر می‌گیرد و سیستم اثبات آن ادعاهای اجرا را به فیلدهایی مانند عملوندها، پرچم‌ها و نشانی‌ها متصل می‌کند. اگر گسترش دستور معنا را تغییر دهد، بررسی‌های بعدی ممکن است از نظر داخلی سازگار بمانند اما محاسبه‌ای نادرست را تأیید کنند.

درس عملی برای سازندگان ICP که برنامه‌های مبتنی بر zkVM را ارزیابی می‌کنند این است که پیش از توجه به عملکرد اعلام‌شدهٔ سیستم اثبات، مرز ترجمه را بررسی کنند. باید پرسید کدام دستورهای مهمان بومی هستند، کدام‌یک گسترش می‌یابند، گسترش چگونه از پیاده‌سازی استخراج می‌شود و آیا اثبات‌کننده و بررسی‌کننده از یک تعریف واحد برای مجموعه‌دستور استفاده می‌کنند یا نه. اثبات معادل‌بودنِ بررسی‌شده با ماشین در این نقطه ارزشمند است، چون fuzzing می‌تواند نمونهٔ خطا پیدا کند اما نمی‌تواند درستی همهٔ ورودی‌ها را ثابت کند.

این رویداد همچنین الگویی برای زیرساخت‌های دارای اثبات فراهم می‌کند: بررسی رسمی فقط برای بررسی‌کنندهٔ رمزنگاری نهایی نیست و می‌تواند روی تبدیل شبه‌کامپایلری‌ای اعمال شود که ورودی سیستم اثبات را می‌سازد. بااین‌حال، این دستاورد به معنای بررسی‌شدن کل پشته نیست. LayerZero می‌گوید بررسی اجزای دیگر Jolt هنوز ادامه دارد و مخزن Jolt همچنان پروژه را آلفا و نامناسب برای استفادهٔ تولیدی توصیف می‌کند. بنابراین این milestone یک مرز اعتماد را تقویت می‌کند، اما گواهی آمادگی تولید برای Jolt یا یکپارچه‌سازی آن با ICP نیست.