۶۰ دستورالعمل تأییدشده Jolt روشن می‌کنند که یک اثبات zkVM واقعاً چه چیزی را پوشش می‌دهد

LayerZero پروژه Jolt-QED را منتشر کرده است؛ پروژه‌ای برای راستی‌آزمایی صوری ماشین مجازی دانش صفر Jolt با استفاده از Lean. نتیجه فعلی به معنای راستی‌آزمایی کامل zkVM نیست. این پروژه نشان می‌دهد که ۶۰ مورد از ۶۷ دستورالعمل قابل‌گسترش Jolt، معنای متناظر خود در RISC-V را به‌درستی پیاده‌سازی می‌کنند.

این تفاوت مهم است، چون Jolt مستقیماً برنامه اصلی RISC-V را اثبات نمی‌کند. ردیاب Jolt ابتدا دستورالعمل‌هایی را که برای سیستم اثبات مناسب نیستند، به دنباله‌ای از دستورالعمل‌های Jolt تبدیل می‌کند. سپس برنامه حاصل اجرا و اثبات می‌شود. اگر این تبدیل معنای برنامه را تغییر دهد، یک اثبات رمزنگاری‌شده معتبر همچنان می‌تواند محاسبه‌ای نادرست را تأیید کند.

مقاله Jolt-QED ماشین مرجع RISC-V و مجموعه دستورالعمل Jolt را در Lean مدل می‌کند. همچنین فرایندی را توضیح می‌دهد که گسترش‌های بایت‌کد را از پیاده‌سازی Rust استخراج می‌کند تا گزاره‌های اثبات‌شده با تعریف دستورالعمل‌ها در کد واقعی ارتباط داشته باشند. برای دستورالعمل‌های تأییدشده، ادعای صوری این است که اگر هر دو اجرا از وضعیت یکسانی آغاز شوند، دنباله گسترش‌یافته و دستورالعمل اصلی به وضعیت نهایی یکسانی در RISC-V می‌رسند.

این موضوع برای سازندگان zkVM یک مرز امنیتی مهم است. تست و فازینگ می‌توانند ناهماهنگی‌های مشخص را پیدا کنند، اما نمی‌توانند نبودن همه ناهماهنگی‌ها را برای تمام ورودی‌ها ثابت کنند. اثبات‌های صوری برای مدل و فرضیه‌های دقیق خود، تضمین قوی‌تری ارائه می‌دهند. مخزن پروژه نیز این فرض‌ها را آشکار می‌کند و راستی‌آزمایی صوری را به‌عنوان تضمینی نامحدود برای امنیت معرفی نمی‌کند.

محدودیت پروژه جدی است: هفت مورد از ۶۷ دستورالعمل قابل‌گسترش هنوز اثبات نشده‌اند. مخزن همچنین بخش‌های پایین‌دستی Jolt، از جمله قیود، sumcheckها، کاهش‌ها و طرح تعهد را ناتمام یا در حال توسعه نشان می‌دهد. بنابراین نتیجه جدید یک حلقه از زنجیره اثبات را تقویت می‌کند؛ اما به‌تنهایی درستی همه اجزایی را که اثبات Jolt را تولید یا بررسی می‌کنند، ثابت نمی‌کند. این محدودیت در این مقاله و مقاله انگلیسی صریحاً اعلام شده است.

برای توسعه‌دهندگان ICP که یک مؤلفه مبتنی بر zkVM را ارزیابی می‌کنند، درس عملی این است که باید نقشه سطح اعتماد را درخواست کنند، نه فقط یک بنچمارک. بررسی کنید چه دستورالعمل‌هایی پشتیبانی می‌شوند، آیا لایه ترجمه نسبت به ISA مرجع هم‌ارزی اثبات‌شده دارد، به کدام کامپایلرها و مدل‌های تولیدشده اعتماد می‌شود، و آیا باینری مستقرشده با کد تأییدشده مطابقت دارد یا نه. یک سیستم اثبات می‌تواند از نظر ریاضی sound باشد، اما مرحله ترجمه پیش از اثبات همچنان محاسبه نادرستی را هدف بگیرد.

Jolt-QED نشانه تغییری مفید در مهندسی ZK است: ادعاهای راستی‌آزمایی به مصنوعات ماژولار و قابل‌بررسی تبدیل می‌شوند. پرسش مهم دیگر فقط این نیست که آیا یک zkVM «به‌صورت صوری تأیید شده» است؛ بلکه باید پرسید کدام تبدیل، در برابر کدام مشخصات، تأیید شده و چه چیزهایی هنوز بیرون از دامنه اثبات قرار دارند.