zk-SNARKs: التحقق الرسمي لطرق إثبات الذاكرة

عند إجراء التحقق الرسمي لنظام zk-SNARKs، فإن معالجة نظام الذاكرة الفرعي تعتبر تحديًا رئيسيًا. على عكس الآلات الافتراضية التقليدية، يستخدم zkVM جدول التنفيذ والجدول المساعد لتمثيل حالة الذاكرة، مما يتطلب طرق تحقق خاصة.

نظام الذاكرة في zkWasm يتكون من جدول التنفيذ وجدول الذاكرة. يسجل جدول التنفيذ عملية تنفيذ التعليمات، بينما يحتفظ جدول الذاكرة بسجل كامل لجميع الوصولات إلى الذاكرة. لتبسيط التطوير، يوفر zkWasm طبقة تجريدية، من خلال دالتين alloc_memory_table_lookup_write_cell و alloc_memory_table_lookup_read_cell للتعامل مع الذاكرة.

خلال عملية التحقق، نعتبر جدول الذاكرة هيكل بيانات متغير، من خلال وظيفة memory_at نبني خريطة بيانات العنوان. هذا يمكن أن يثبت أن القيود التي ينتجها دالة alloc تعادل العمليات set و get التي تتم على الخريطة، مما يبسط التحقق من التعليمات إلى شكل مشابه لمفسر غير ZK.

لتجنب تلاعب المهاجمين بجدول الذاكرة، يعتمد zkWasm آلية عد لتتبع عدد الإدخالات الفعالة. تحتفظ جداول التنفيذ وجداول الذاكرة بعدادات بشكل منفصل، مع ضمان التوافق بين الاثنين من خلال القيود. يتطلب ذلك دقة أكبر أثناء التحقق، حيث يحتاج إلى إثبات أن كل تعليمة تتوافق مع العدد الصحيح من إدخالات جدول الذاكرة.

عملية التحقق تعتمد على نهج من أعلى إلى أسفل، وتشمل ثلاث خطوات:

1. يجب تقدير عدد الإدخالات التي يجب على الأمر إنشاؤها
2. يجب ألا يتجاوز عدد الإدخالات في جدول الإثبات التوقعات
3. إثبات أن cum_mops و instructions_mops متسقة دائمًا في الجدول من خلال البرهان بالاستقراء

تساعد هذه الطريقة التفصيلية للتحقق في اكتشاف الأخطاء المحتملة، مثل مشكلة رئيسية في آلية عد جدول القفز.

لتحقيق التحقق المعياري، قمنا بتقسيم النظام إلى ثلاثة أجزاء مستقلة: تحقق دائرة التعليمات، تحقق جدول التنفيذ، وتنفيذ جدول الذاكرة. هذه الهيكلية تتيح للعديد من المهندسين العمل بشكل متوازٍ، مما يزيد من كفاءة التحقق.

بشكل عام، على الرغم من أن zkVM تحقق يظهر اختلافات عند التعامل مع الحالة الديناميكية، إلا أنه من خلال مطابقة طبقة التجريد في التنفيذ، لا يزال من الممكن اعتماد نهج معياري مشابه للتحقق من المفسرات التقليدية. تقلل هذه الطريقة من تأثير الاختلافات إلى الحد الأدنى، مما يسمح بالتحقق المستقل لكل تعليمة بناءً على واجهة get-set.