Formally Verified Linear-Time Invertible Lexing

Die Arbeit stellt ZipLex vor, ein in Stainless verifiziertes Framework für invertible lineare lexikalische Analyse, das durch den Einsatz von Zippern und verifizierter Memoisierung nicht nur die längste Übereinstimmung garantiert, sondern auch die Linearzeitkomplexität und die Umkehrbarkeit von Lexing und Printing nachweist.

Das Wesentliche

Stellen Sie sich vor, Sie haben einen sehr strengen, aber genialen Übersetzer namens ZipLex. Seine Aufgabe ist es, einen Haufen roher Buchstaben (wie einen Text in einer Datei) in sinnvolle Wörter und Symbole zu zerlegen, damit ein Computer sie verstehen kann. Das nennt man „Lexing" oder „Tokenisierung".

Aber ZipLex ist nicht irgendein Übersetzer. Er ist formal verifiziert. Das bedeutet, er hat nicht nur einen guten Riecher für Fehler, sondern er hat einen mathematischen Beweis in seiner Tasche, der garantiert: „Ich mache genau das, was ich sagen soll, und zwar immer."

Hier ist die Geschichte von ZipLex, erzählt mit ein paar einfachen Bildern:

1. Das Problem: Der „Verlust" beim Zurückübersetzen

Stellen Sie sich vor, Sie haben einen Satz aus Lego-Steinen gebaut. Ein normaler Übersetzer (ein herkömmlicher Lexer) nimmt die Buchstaben und baut daraus einen Lego-Turm. Das funktioniert gut.
Aber was passiert, wenn Sie den Turm wieder auseinandernehmen, ihn ein bisschen umbauen (z. B. ein paar Lücken schließen) und dann versuchen, ihn zurück in Buchstaben zu verwandeln?

Bei normalen Übersetzern kann das schiefgehen.

• Beispiel: Sie haben die Wörter val, x, =, 1.
• Wenn Sie die Leerzeichen entfernen und schreiben val x=1, denkt der Computer vielleicht: „Aha, x= ist ein einziges Wort!" und baut einen völlig anderen Turm.
• Das ist wie wenn Sie ein Foto machen, es in Photoshop ein wenig bearbeiten und dann versuchen, das Originalfoto aus dem bearbeiteten Bild wiederherzustellen – aber es fehlen Teile oder es sieht anders aus.

ZipLex löst dieses Problem. Er garantiert, dass das, was er aus Buchstaben baut, und das, was er aus den Bausteinen wieder in Buchstaben verwandelt, exakt dasselbe ist. Man nennt das „invertierbar". Es ist wie ein magischer Spiegel: Was hineingeht, kommt unverändert wieder heraus, egal wie oft Sie es drehen.

2. Die Magie: Wie macht er das so schnell?

Normalerweise sind solche perfekten Übersetzer extrem langsam. Sie müssen oft den ganzen Text mehrmals durchlesen, um sicherzugehen, dass sie nichts falsch gemacht haben. Das ist wie ein Detektiv, der jeden Tatort dreimal absucht, bevor er weitergeht.

ZipLex ist aber ein Super-Detektiv, der zwei Tricks beherrscht:

• Trick 1: Der Notizblock (Memoization)
  ZipLex führt einen Notizblock mit. Wenn er ein Wort schon einmal analysiert hat, schreibt er das Ergebnis auf. Wenn er das Wort später wieder sieht, schaut er nur auf den Notizblock, statt es neu zu berechnen.

  • Analogie: Statt jedes Mal den Weg durch den Wald neu zu suchen, markiert er die Wege, die er schon kennt. Das macht ihn linear schnell: Je länger der Text, desto mehr Zeit braucht er, aber er wird nicht viel langsamer, sondern nur proportional. Andere verifizierte Übersetzer werden bei langen Texten quadratisch langsamer (wie wenn man bei jedem Schritt doppelt so viel Zeit braucht wie beim vorherigen).

• Trick 2: Der Reißverschluss (Zippers)
  Um die Buchstaben schnell zu sortieren, nutzt ZipLex eine Technik namens „Zippers" (Reißverschlüsse). Stellen Sie sich vor, Sie haben einen langen Text auf einem Papierband. Ein normaler Computer muss das ganze Band aufrollen, um ein Wort zu finden. ZipLex hingegen hat einen Reißverschluss, den er genau dort öffnen kann, wo er gerade ist. Er kann Teile des Textes schnell herausnehmen, bearbeiten und wieder einstecken, ohne das ganze Band neu zu lesen.

3. Die „Trennlinie" (Separability)

Damit ZipLex sicher ist, dass er beim Zurückverwandeln nichts vermischt, braucht er eine Regel: Die Trennlinie.
Stellen Sie sich vor, Sie haben zwei Lego-Steine nebeneinander. Damit sie nicht zu einem einzigen riesigen Stein verschmelzen, muss zwischen ihnen eine klare Grenze sein.
ZipLex prüft mathematisch: „Wenn ich diesen Stein hier und den nächsten dort zusammenlege, wird daraus ein neues, falsches Wort?"

• Wenn ja: Er fügt eine unsichtbare Trennlinie (wie ein Leerzeichen) ein.
• Wenn nein: Er lässt sie zusammen.

Das Besondere an ZipLex ist, dass er diese Prüfung im Voraus macht und speichert. Wenn Sie später zwei Textteile zusammenfügen (z. B. beim Sortieren von JSON-Daten), prüft er nur an der Nahtstelle, ob die Trennlinie noch stimmt. Das geht blitzschnell.

4. Warum ist das wichtig?

Bisher waren verifizierte Compiler (wie der berühmte CompCert) sehr sicher, aber ihr erster Schritt (das Lexing) war oft ein „vertrauenswürdiges" Bauteil, das nicht überprüft war. Wie ein Fundament, das man einfach für stabil hält, ohne es zu testen.

ZipLex ist das erste Fundament, das:

1. Mathematisch bewiesen sicher ist (keine Fehler möglich).
2. Rückwärts lesbar ist (man kann Code ändern und wiederherstellen, ohne Daten zu verlieren – super für IDEs und Refactoring-Tools).
3. Schnell genug für die echte Welt ist (er ist sogar 100-mal schneller als andere verifizierte Übersetzer).

Zusammenfassung in einem Satz

ZipLex ist wie ein unfehlbarer, superschneller Übersetzer, der garantiert, dass Sie einen Text in Bausteine zerlegen, diese Bausteine sortieren und bearbeiten können, und am Ende wieder den exakt gleichen Text zurückbekommen – alles ohne dass die Geschwindigkeit ins Stocken gerät.

Es ist der Beweis, dass man in der Softwareentwicklung nicht zwischen „sicher" und „schnell" wählen muss; man kann beides haben, wenn man die richtigen Werkzeuge (wie verifizierte Hash-Tabellen und Reißverschlüsse) benutzt.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Formally Verified Linear-Time Invertible Lexing" auf Deutsch:

1. Problemstellung

Lexikalische Analyse (Lexing) ist ein kritischer Schritt in Compiler-Pipelines und Datenanalyse-Tools. Bestehende verifizierte Lexer (wie Coqlex oder Verbatim++) garantieren zwar die Korrektheit bezüglich regulärer Ausdrücke und der „Longest Match"-Semantik (maximale Übereinstimmung), leiden jedoch unter zwei wesentlichen Mängeln:

1. Fehlende Invertierbarkeit: In vielen Anwendungen (z. B. IDE-Refactoring, Programmsynthese) müssen Token-Sequenzen wieder in Text umgewandelt (gedruckt) und erneut geparst werden. Bestehende Systeme garantieren nicht, dass lex(print(ts)) == ts gilt. Das Entfernen von Whitespace oder das Umordnen von Token kann dazu führen, dass beim erneuten Lexing Token verschmelzen (z. B. wird val x = 1 zu val x=1, was als ein Identifier x= geparst werden könnte), wodurch Informationen verloren gehen.
2. Performance: Viele verifizierte Ansätze haben eine quadratische Zeitkomplexität ($O(n^2)$) in Bezug auf die Eingabelänge, insbesondere bei adversarischen Grammatiken, oder benötigen aufwendige Vorverarbeitungsschritte (wie DFA-Konstruktion).

Das Ziel ist ein Lexer, der formal verifiziert, invertierbar (Drucken und Lexen sind zueinander inverse Operationen) und linear in der Zeit ($O(n)$) ist.

2. Methodik und Architektur

Die Autoren stellen ZipLex vor, einen in Scala implementierten und mit dem deduktiven Verifizierer Stainless verifizierten Lexer. Die Architektur basiert auf folgenden Kernideen:

A. Invertierbarkeit und Trennbarkeit (Separability)

Um Invertierbarkeit zu garantieren, wird eine Bedingung für trennbare Token-Sequenzen definiert.

• Das Problem: Zwei benachbarte Token können beim Drucken zu einem neuen, längeren Token verschmelzen, wenn keine Trennung vorhanden ist.
• Die Lösung (R-Path Prädikate): Die Autoren führen das Konzept der R-Path-Bedingungen ein. Eine Token-Sequenz ist trennbar, wenn für jedes benachbarte Token-Paar $(t_i, t_{i+1})$ eine Relation $sep(t_i, t_{i+1})$ gilt.
• Die Relation $sep$: Zwei Token sind trennbar, wenn das erste Zeichen des zweiten Tokens sicherstellt, dass das erste Token bereits als das längstmögliche Match erkannt wurde, unabhängig von nachfolgenden Token. Dies wird durch eine Prüfung der Präfix-Mengen aller regulären Ausdrücke der Regeln bestimmt.
• Abstraktion: Ein neuer Datentyp PrintableTokens kapselt Token-Sequenzen und erhält die Invariante der Trennbarkeit. Beim Slicen bleibt die Invariante erhalten; beim Konkatenieren wird nur eine konstante Zeit-Prüfung an der Grenze durchgeführt.

B. Reguläre Ausdrücke und Matching

• Brzozowski-Derivate: Der Lexer nutzt Brzozowski-Derivate für das Matching regulärer Ausdrücke, was eine elegante formale Basis bietet.
• Huet-Zipper: Um die Ineffizienz naiver Derivate (Explosion der Ausdrucksgröße) zu vermeiden, wird eine Optimierung mittels Huet-Zippern implementiert. Zipper repräsentieren reguläre Ausdrücke als Mengen von Kontexten. Dies ermöglicht effizientes Matching und ist besonders gut für Memoisierung geeignet, da die Menge der erreichbaren Zipper endlich ist.

C. Verifizierte Memoisierung und Performance

Um lineare Zeitkomplexität zu erreichen, wird eine verifizierte Memoisierung eingesetzt:

• Datenstrukturen: Anstelle von Standard-Listen wird eine effiziente, verifizierte Datenstruktur namens BalanceConc (basierend auf balancierten Binärbäumen) für die Laufzeit verwendet, während List für die Spezifikation und Beweise genutzt wird.
• Hash-Tabellen: Ein verifizierbarer, veränderlicher Hash-Map (LongMap-Basis) dient als Cache für die Derivate und die längsten Übereinstimmungen.
• Tail-Rekursion: Alle rekursiven Funktionen wurden in tail-rekursive Versionen umgewandelt, um Stack-Overflow-Fehler auf der JVM zu vermeiden, wobei die Äquivalenz zur ursprünglichen Spezifikation bewiesen wurde.
• Algorithmus: Durch die Memoisierung der „furthest nullable position" (ähnlich Reps [29]) wird sichergestellt, dass das Lexing in $O(n)$ Zeit erfolgt, selbst bei adversarischen Grammatiken, die naive Ansätze in $O(n^2)$ treiben würden.

3. Wichtige Beiträge

1. Definition der Trennbarkeit: Eine formale Definition von sep(ts) mit effizienten Mechanismen zur Überprüfung und Durchsetzung, die sicherstellt, dass lex(print(ts)) = ts.
2. ZipLex-Framework: Ein vollständig verifizierter Lexer, der reguläre Ausdrücke, Longest-Match-Semantik, Invertierbarkeit und lineare Laufzeit vereint.
3. Verifizierte Optimierungen: Die Kombination aus Huet-Zippern, verifizierter Memoisierung und effizienten Datenstrukturen (BalanceConc, verifizierte Hash-Map) in einem einzigen System.
4. Implementierung und Evaluation: Eine vollständige Implementierung in Scala, die mit Stainless verifiziert wurde und mit realen Anwendungen (JSON-Parser, Sortierung von JSON-Objekten) getestet wurde.

4. Ergebnisse und Evaluation

Die Evaluation wurde auf einem Server mit AMD EPYC-Prozessoren durchgeführt und vergleicht ZipLex mit flex, Coqlex, Verbatim++ und OCamllex.

• Komplexität: ZipLex zeigt ein lineares Laufzeitverhalten ($O(n)$) auch bei adversarischen Grammatiken (z. B. $r_1 = a$, $r_2 = a^*b$), bei denen flex und Coqlex quadratisch ($O(n^2)$) skalieren. Verbatim++ stürzt bei großen Eingaben aufgrund von Stack-Overflows ab.
• Performance-Vergleich:
  • ZipLex ist etwa 100-mal (zwei Größenordnungen) schneller als Verbatim++.
  • ZipLex ist etwa 8-mal langsamer als Coqlex, bietet aber im Gegensatz dazu Invertierbarkeit und lineare Laufzeitgarantien.
  • Der Overhead für die Berechnung der Trennbarkeit (sep) ist gering, da der Derivat-Cache bereits während des Lexings gefüllt wird.
• Anwendbarkeit: Das System wurde erfolgreich auf JSON-Verarbeitung und das Sortieren von JSON-Objekten angewendet, wobei die Invertierbarkeit (Lexen -> Sortieren -> Drucken -> Lexen) formal garantiert wurde.

5. Bedeutung

Das Paper demonstriert, dass formal verifizierte, invertible und lineare Lexing-Verfahren ohne prohibitive Kosten realisierbar sind.

• Es schließt die Lücke zwischen theoretischer Verifizierung und praktischer Anwendbarkeit in modernen Compiler-Pipelines und Refactoring-Tools.
• Es beweist, dass Invertierbarkeit auf der Ebene der lexikalischen Analyse (nicht nur beim Parsing) erreicht werden kann, was für verifizierte Compiler und Kommunikationssysteme essenziell ist.
• Die Arbeit zeigt, dass verifizierte Memoisierung und effiziente Datenstrukturen kombiniert werden können, um sowohl Korrektheitsgarantien als auch hohe Performance zu liefern.

Zusammenfassend stellt ZipLex einen Meilenstein dar, der zeigt, dass hochverifizierte Softwarekomponenten nicht zwangsläufig ineffizient sein müssen und dass komplexe Eigenschaften wie Invertierbarkeit formal bewiesen und praktisch nutzbar gemacht werden können.