Clean: بيئة تطوير متكاملة (DSL) وإطار عمل للتحقق الرسمي من دوائر ZK في Lean4

طور الباحثون Clean، وهي لغة محددة للغة المجال (DSL) مضمنة وإطار عمل للتحقق الرسمي في Lean4 لبناء دوائر المعرفة الصفرية (ZK). دوائر ZK عرضة للأخطاء، ويهدف Clean إلى تحسين الصحة من خلال السماح للمستخدمين بتعريف الدوائر في Lean4، وتحديد خصائصها المطلوبة، وإثباتها رسميًا. هذا المشروع جزء من مشروع التحقق الرسمي من zkEVM، الذي يهدف إلى توفير البنية التحتية والأدوات للتحقق الرسمي من zkEVMs. يدعم Clean أربع عمليات أساسية لتعريف الدوائر: witness، assert، lookup، و subcircuit، ويوفر واجهة أحادية لتحسين قابلية الاستخدام. جوهر النظام هو بنية FormalCircuit، التي تجمع بشكل قوي من حيث النوع، تعريف الدائرة، والافتراضات، والمواصفات، وإثباتات الصحة والاكتمال. يمكن التحقق رسميًا من الدوائر الكبيرة من خلال استبدال قيود الدوائر الفرعية بشكل متكرر بمواصفاتها (التي تم التحقق منها رسميًا). وقد نجح الإطار بالفعل في التحقق من دوائر بسيطة مثل الجمع 8 بت، مع خطط مستقبلية لإضافة المزيد من الأدوات منخفضة المستوى، وتحديد دوائر دوال التجزئة الشائعة، وبناء آلة افتراضية صغيرة تم التحقق منها رسميًا لمجموعة فرعية من RISC-V.