💻 computer science

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Dieser Beitrag stellt BitModEq vor, eine neuartige Lean-Taktik, die Äquivalenzbeweise zwischen Bitvektoren und endlichen Körpern mittels Bereichslemmata und Fallunterscheidungen automatisiert und dabei die State-of-the-Art-SMT-Löser bei der Verifizierung von Zero-Knowledge-Proof-Schaltkreiskodierungen übertrifft.

Ursprüngliche Autoren: Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

Veröffentlicht 2026-05-15

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Ganze: Zwei verschiedene Sprachen für Mathematik

Stellen Sie sich vor, Sie möchten überprüfen, ob ein geheimes Rezept (ein Zero-Knowledge-Beweis) korrekt funktioniert. Das Problem ist, dass das Rezept in zwei verschiedenen Sprachen geschrieben ist, die sich nicht gut mischen:

Endliche Körper: Denken Sie daran als eine Welt der "Uhrzeit-Mathematik". Wenn Sie eine Uhr mit 17 Stunden haben, ergibt 10 plus 10 nicht 20, sondern 3 (weil Sie umschlagen). So rechnen viele moderne kryptografische Systeme (wie die in Kryptowährungen verwendeten).
Bitvektoren: Denken Sie daran als "Computer-Mathematik". Computer schlagen nicht wie Uhren um; sie haben lediglich eine feste Anzahl von Schaltern (Bits), die entweder an oder aus sind. Wenn Sie Zahlen addieren und die Schalter ausgehen, werden die zusätzlichen Bits einfach abgeschnitten.

Das Problem:
Wenn Entwickler diese kryptografischen Systeme erstellen, müssen sie die "Uhrzeit-Mathematik" in "Computer-Mathematik" übersetzen, damit sie auf echter Hardware läuft. Diese Übersetzung nennt man Arithmetisierung.

Wenn die Übersetzung falsch ist, ist das gesamte Sicherheitssystem kaputt.
Zu überprüfen, ob die Übersetzung korrekt ist, ist unglaublich schwierig.
Manuelle Prüfung ist wie das Korrekturlesen eines Romans, bei dem man jedes Wort mit einer Lupe liest: Es ist genau, dauert aber ewig und ist anfällig für menschliche Fehler.
Automatische Prüfung (mit Standard-Computersolvern) ist wie die Verwendung einer Rechtschreibprüfung: Sie ist schnell, wird aber oft von den seltsamen Regeln der "Uhrzeit-Mathematik" verwirrt und gibt bei komplexen Sätzen auf.

Die Lösung: Der "BitModEq"-Übersetzer

Die Autoren haben ein neues Werkzeug namens BitModEq innerhalb eines Systems namens Lean entwickelt (das wie ein super-strenger Mathe-Nachhilfelehrer ist, der jeden Schritt eines Beweises überprüft).

Stellen Sie sich BitModEq als einen spezialisierten Übersetzer vor, der nicht nur Wörter austauscht, sondern die Logik hinter den Wörtern versteht. Es verwendet einen dreistufigen Prozess, um zu beweisen, dass das "Uhrzeit-Mathematik"-Rezept exakt dem "Computer-Mathematik"-Rezept entspricht:

Schritt 1: Das "Auspacken" (Übersetzung)

Das Werkzeug nimmt die "Uhrzeit-Mathematik" (Endliche Körper) und versucht, sie in normale Zahlen (Natürliche Zahlen) "auszupacken".

Die Herausforderung: In der Uhrzeit-Mathematik könnte $5 - 10$ eine positive Zahl sein, wegen des Umschlagens. In der normalen Mathematik ist sie negativ.
Der Trick: Das Werkzeug betrachtet die Zahlen und fragt: "Ist es möglich, dass diese Zahl umschlägt?" Wenn die Zahlen klein genug sind (wie Bits in einem Computer), weiß es, dass ein Umschlagen nicht passieren wird. Es entfernt sicher die "Uhrzeit"-Regeln und behandelt sie als normale Mathematik. Wenn es sich nicht sicher ist, behält es die "Uhrzeit"-Regeln bei, fügt jedoch eine Sicherheitsprüfung hinzu.

Schritt 2: Das "Sicherheitsnetz" (Bereichsanalyse)

Dies ist das Geheimnis des Papers. Bevor das Werkzeug versucht, die Mathematik in Computer-Bits umzuwandeln, führt es eine Bereichsanalyse durch.

Die Analogie: Stellen Sie sich vor, Sie packen einen Koffer. Sie werfen die Kleidung nicht einfach hinein; Sie prüfen die Größe des Koffers und die Größe der Kleidung.
Wie es funktioniert: Das Werkzeug betrachtet die Variablen und fragt: "Wie groß kann diese Zahl höchstens sein?"
- Wenn es weiß, dass eine Zahl zwischen 0 und 1 liegt (wie ein einzelner Lichtschalter), kann es die komplexen "Uhrzeit"-Regeln vollständig ignorieren.
- Dieser Schritt ist entscheidend, weil er das Problem so stark vereinfacht, dass der Computer es leicht lösen kann. Ohne diesen "Sicherheitsnetz"-Check wird der Computer von der Komplexität überwältigt.

Schritt 3: Das "Bit-Explodieren" (Finale Beweisführung)

Sobald das Werkzeug das Problem in reine "Computer-Mathematik" (Bits) vereinfacht hat, verwendet es eine Technik namens Bit-Blasting.

Die Analogie: Dies ist wie das Aufbrechen eines komplexen Schlosses, indem man jede einzelne Kombination von Schlüsseln durchprobiert, bis man diejenige findet, die es öffnet.
Da das Werkzeug das Problem in Schritt 2 vereinfacht hat, ist das "Schloss" nun klein genug, damit der Computer jede Kombination sofort durchprobiert und beweist, dass die Mathematik korrekt ist.

Warum das wichtig ist (Die Ergebnisse)

Die Autoren testeten ihr Werkzeug an realen kryptografischen Systemen (speziell Jolt und CirC).

Der Wettbewerb: Sie verglichen ihr Werkzeug mit den besten vorhandenen automatischen Solvern (wie cvc5).
Das Ergebnis: Die bestehenden Solver blieben oft stecken oder liefen aus, wenn die Probleme groß wurden (wie 32-Bit-Zahlen). Sie waren wie eine Rechtschreibprüfung, die versucht, ein Wörterbuch zu lesen.
Der Sieg von BitModEq: Das neue Werkzeug löste 19 % mehr Probleme als die besten vorhandenen Tools. Es konnte viel größere Zahlen (bis zu 32 Bit) bewältigen, bei denen die anderen versagten.
Bonus: Da es innerhalb von Lean läuft, ist der Beweis kernelgeprüft. Das bedeutet, der Computer hat nicht nur geraten; er folgte einem strengen Satz logischer Regeln, von denen garantiert ist, dass sie korrekt sind, was das Risiko versteckter Fehler verringert.

Eine reale Entdeckung

Während ihrer Tests fand das Werkzeug tatsächlich einen Fehler im CirC-Compiler. Der Compiler hatte einen Fehler darin, wie er mit großen Zahlen umgeht (speziell bei einem 32-Bit-Rechtsverschiebungs-Vorgang). Der Fehler zeigte sich nur bei großen Zahlen, weshalb frühere Tests in kleinerem Maßstab ihn übersehen hatten. Die Entwickler behoben den Fehler, nachdem die Autoren ihn gemeldet hatten.

Zusammenfassung

Das Paper stellt eine neue Methode vor, um automatisch zu verifizieren, dass kryptografische Mathematik korrekt funktioniert. Anstatt mühsam zwischen "Uhrzeit-Mathematik" und "Computer-Mathematik" manuell oder mit unhandlichen Werkzeugen zu übersetzen, bauten sie einen intelligenten Übersetzer, der:

Zuerst die Größe der Zahlen prüft (Bereichsanalyse).
Die Mathematik vereinfacht, indem er unnötige "Uhrzeit"-Regeln entfernt.
Brute-Force-Logik verwendet, um das Endergebnis als korrekt zu beweisen.

Dies macht die Verifizierung komplexer Sicherheitssysteme schneller, zuverlässiger und fähig, Fehler zu entdecken, die andere Tools übersehen.

Technische Zusammenfassung: Automatisierung von Bitvektor- und Endkörper-Äquivalenzbeweisen in Lean

Problemstellung

Die Verifikation von Zero-Knowledge-Proof (ZKP)-Schaltungs-Codierungen steht vor einer kritischen Herausforderung: dem Beweis der Korrektheit quantorenfreier Aussagen, die gleichzeitig Bitvektor-Operationen (Standard-Maschinenarithmetik modulo $2^N$ ) und Endkörper-Operationen (Arithmetik modulo einer großen Primzahl $P$ ) nutzen. ZKP-Systeme erfordern oft „Arithmetisierungen", die Bitvektor-Logik als Polynome über Endkörpern codieren. Die Sicherstellung der Korrektheit dieser Codierungen ist für die Zuverlässigkeit von ZKP-Systemen von entscheidender Bedeutung, doch ihre Konstruktion ist fehleranfällig.

Bestehende Verifikationsworkflows leiden unter zwei primären Einschränkungen:

Manuelle Verifikation: Die Einbettung ganzer ZKP-Systeme in Interaktive Theorembeweiser (ITPs) wie Lean bietet starke Garantien, erfordert jedoch erheblichen menschlichen Aufwand. Da ZKP-Optimierungen sich rasch weiterentwickeln, müssen diese manuellen Beweise häufig erheblich überarbeitet werden.
Automatisierte SMT-Verifikation: Die Reduktion der Verifikation auf Satisfiability Modulo Theories (SMT)-Abfragen bietet eine höhere Automatisierung, kämpft jedoch mit zwei grundlegenden Problemen:
- Theoriekonvertierung: SMT-Löser verfügen nicht über native Unterstützung für die Konvertierung zwischen Endkörpern und Bitvektoren. Workarounds wie Bit-Aufspaltung führen zu einer übermäßigen Anzahl von Variablen, und Bereichsprüfungen erfordern komplexe Polynome, die die Leistung des Löser beeinträchtigen.
- Vertrauenswürdige Codebasis (TCB): SMT-Löser haben eine deutlich größere TCB als ITPs, was das Risiko verpasster Bugs erhöht.

Methodik

Die Autoren stellen BitModEq vor, eine neuartige Lean-Taktik, die entwickelt wurde, um die Äquivalenz zwischen Endkörper-Codierungen und ihren entsprechenden Bitvektor-Semantiken automatisch zu beweisen. Der Ansatz nutzt die reichhaltige Semantik von ITPs, um direkte Typkonvertierungen durchzuführen, und behält gleichzeitig die Automatisierung der SMT-Lösung durch einen spezialisierten Workflow bei.

Kern-Workflow

BitModEq arbeitet in vier distincten Phasen (illustriert in Abbildung 1 des Papers):

Konvertierung von Endkörper zu natürlichen Zahlen: Alle Terme vom Sorten Endkörper ($FP$) werden in natürliche Zahlen ( $N$ ) umgewandelt. Dies beinhaltet das Einpushen von Konvertierungsoperatoren (wie toNat) nach innen durch arithmetische Ausdrücke.
Bereichsanalyse: Ungleicherungen über natürliche Zahlen, die während der Konvertierung erzeugt werden, werden mithilfe eines dedizierten Bereichsanalyse-Algorithmus entladen.
Konvertierung von natürlichen Zahlen zu Bitvektoren: Verbleibende Terme natürlicher Zahlen werden in Bitvektoren ( $BV_N$ ) umgewandelt.
Bit-Blasting: Die finalen Bitvektor-Gleichheitsziele werden mit bv_decide entladen, einem in Lean implementierten Bit-Blasting-Entscheidungsverfahren.

Schlüsseltechnische Komponenten

1. Übersetzungskalkül (Abschnitte 4.2)
Die Taktik verwendet eine Reihe von Übersetzungsregeln, um zwischen Domänen zu wechseln:

$FP \to N$ : Regeln wie distNat verteilen toNat über Addition und Multiplikation. Entscheidend ist, dass die Taktik zwischen Fällen unterscheidet, in denen ein modulares Überlaufen ausgeschlossen werden kann (was eine einfache Subtraktion erlaubt), und Fällen, in denen dies nicht möglich ist (was das Hinzufügen des Moduls $P$ gefolgt von einer Modulo-Operation erfordert). Regeln wie sqrBds erkennen Bit-Codierungen (wo $x^2 = x$ ) und übersetzen sie in Schranken ( $x \le 1$ ).
$N \to BV$ : Regeln wie distBV verteilen toBV über Operationen. Im Gegensatz zum Schritt $FP \to N$ erfordern diese Regeln kein Hinzufügen eines Modulo-Operators, da der Zielraum natürlicherweise modulo $2^N$ ist.

2. Bereichsanalyse (Abschnitt 4.3)
Standard-Lean-Taktiken (z. B. omega, linarith) scheitern häufig an ZKP-Arithmetisierungen aufgrund großer Koeffizienten und komplexer Variablenabhängigkeiten. BitModEq führt einen benutzerdefinierten, syntaxgesteuerten Bereichsanalyse-Kalkül ein:

Platzhalter-Variablen: Der Algorithmus führt existenzielle Platzhalter-Variablen ein, um komplexe Ungleicherungen zu zerlegen.
Zerlegung und Elimination: Regeln zerlegen Ungleicherungen (z. B. wird $a + b \le w$ zu $a \le w_1, b \le w_2, w_1+w_2 \le w$ ) und eliminieren Platzhalter, indem sie diese mit Schranken instanziieren, die aus Hypothesen oder bekannten Eigenschaften abgeleitet werden (z. B. sind Endkörperelemente durch $P-1$ beschränkt).
Umgang mit Abhängigkeiten: Spezialisierte Regeln (ineqCases, ineqXOR) führen gezielte Fallanalysen an Variablen durch, die Bits simulieren (0 oder 1), um Abhängigkeiten aufzulösen, die Standardarithmetik-Löser übersehen.

3. Implementierung
Die Taktik ist in Lean 4.23.0 implementiert und nutzt mathlib für Lemmata sowie bv_decide für den finalen Bit-Blasting-Schritt. Sie verlässt sich auf den Lean-Kernel zur Beweisprüfung, was eine minimale Trusted Computing Base sicherstellt.

Hauptbeiträge

BitModEq-Taktik: Eine Lean-Taktik, die Endkörper-Operationen in Bitvektoren übersetzt und die daraus resultierenden Ziele durch Bit-Blasting löst, wobei die Korrektheitsgarantien von ITPs erhalten bleiben.
Beschränkte Verifikation realer Codierungen: Ein Proof-of-Concept für die Verifikation zweier realer ZKP-Systeme (Jolt und CirC), das höhere Bitbreiten-Schranken als frühere Techniken erreicht.
Spezialisierte Bereichsanalyse: Eine neue Lean-Taktik zum Beweis von Zielen, die aus der Übersetzung resultieren, die speziell entwickelt wurde, um die Variablenabhängigkeiten und Ungleicherungsbeschränkungen zu behandeln, die bei ZKP-Arithmetisierungen üblich sind.

Ergebnisse und Evaluation

Die Autoren evaluierten BitModEq gegenüber State-of-the-Art-SMT-Lösern (insbesondere cvc5 mit vollständigen und aufgeteilten Gröbner-Basen) an Benchmarks, die aus Jolt (ein zkVM) und CirC (ein zkVM-Compiler) extrahiert wurden.

Leistung: BitModEq löste 19 % mehr Benchmarks als die am besten performenden SMT-Konfigurationen.
- Bei Jolt-Benchmarks (8-Bit- und 32-Bit-Lookup-Tabellen) löste BitModEq 3 weitere 8-Bit- und 7 weitere 32-Bit-Instanzen mehr als cvc5 (schwache Codierung).
- Bei CirC-Benchmarks löste BitModEq bei 13 von 17 getesteten Bitbreiten mehr Instanzen.
Skalierbarkeit: Während cvc5 bei kleineren Bitbreiten besser performte, verschlechterte sich seine Leistung bei steigenden Bitbreiten signifikant aufgrund der Explosion der Variablen durch Bit-Aufspaltung. BitModEq skalierte effektiv bis zu 32-Bit-Eingaben.
Effizienz: Eine Ablationsstudie zeigte, dass die benutzerdefinierte Bereichsanalyse kritisch ist; das Entfernen von Fallunterscheidungen reduzierte die Anzahl der gelösten Benchmarks erheblich (z. B. von 737 auf 720 bei CirC und von 24 auf 21 bei Jolt). Der Ersatz der benutzerdefinierten Analyse durch Standard-Lean-Taktiken (ring_nf, linarith usw.) führte zu einem drastischen Rückgang gelöster Instanzen (z. B. 434 vs. 737 bei CirC).
Laufzeit: Die Bereichsanalyse macht etwa 52 % der gesamten Laufzeit aus, gefolgt von der Übersetzung (23 %) und dem Bit-Blasting (21 %).
Fehlerentdeckung: Während der Evaluation von CirC identifizierten die Autoren einen Soundness-Bug in der Implementierung des arithmetischen Rechts-Shifts für 32-Bit, der mit Integer-Überlauf zusammenhing und bei kleineren Bitbreiten nicht erkannt wurde.

Bedeutung und Behauptungen

Das Paper behauptet, dass BitModEq die spezifischen Einschränkungen aktueller ZKP-Verifikationsworkflows adressiert, indem es die Soundness von ITPs mit automatischem Schlussfolgern kombiniert. Durch die Übersetzung von Endkörper-Beschränkungen zurück zu Bitvektoren vermeidet der Ansatz die Leistungsengpässe der SMT-Theoriekonvertierung und die große TCB von SMT-Lösern.

Die Autoren betonen, dass ihr Ansatz besonders effektiv für ZKP-Arithmetisierungen ist, die Bit-Ebenen-Operationen innerhalb eines Endkörpers simulieren, ein häufiges Muster in modernen ZK-Systemen. Obwohl die Methode nicht vollständig ist (sie kann bei bestimmten komplexen Abhängigkeiten oder feldspezifischen Operationen wie Inversen „unbekannt" zurückgeben), verifiziert sie erfolgreich reale Codierungen, die für automatische Werkzeuge zuvor unlösbar waren, und liefert kernelgeprüfte Beweise für die Korrektheit dieser kritischen kryptografischen Komponenten.