Clean: Eine eingebettete DSL und ein formales Verifikationsframework für ZK-Schaltungen in Lean4

Forscher haben Clean entwickelt, eine eingebettete domänenspezifische Sprache (DSL) und ein formales Verifikationsframework in Lean4 zum Erstellen von Zero-Knowledge (ZK)-Schaltungen. ZK-Schaltungen sind anfällig für Fehler, und Clean zielt darauf ab, die Korrektheit zu verbessern, indem es Benutzern ermöglicht, Schaltungen in Lean4 zu definieren, ihre gewünschten Eigenschaften anzugeben und sie formal zu beweisen. Dieses Projekt ist Teil des zkEVM Formal Verification Project, das darauf abzielt, Infrastruktur und Tools für die formale Verifikation von zkEVMs bereitzustellen. Clean unterstützt vier grundlegende Operationen zum Definieren von Schaltungen: witness, assert, lookup und subcircuit, und bietet eine monadische Schnittstelle für verbesserte Benutzerfreundlichkeit. Der Kern ist die FormalCircuit-Struktur, die die Schaltungsdefinition, Annahmen, Spezifikation, Soundness- und Completeness-Beweise in einer stark typisierten Weise eng zusammenfasst. Große Schaltungen können formal verifiziert werden, indem die Einschränkungen von Unterschaltungen rekursiv durch ihre (formal verifizierten) Spezifikationen ersetzt werden. Das Framework hat bereits einfache Schaltungen wie die 8-Bit-Addition erfolgreich verifiziert, mit zukünftigen Plänen, weitere Low-Level-Gadgets hinzuzufügen, gemeinsame Hash-Funktions-Schaltungen zu definieren und eine formal verifizierte minimale VM für eine Teilmenge von RISC-V zu erstellen.