Warum Rocq bei der Programmverifikation besser ist als Lean

 (joomy.korkutblech.com)
1 Punkte von GN⁺ 2 시간 전 | Noch keine Kommentare. | Auf WhatsApp teilen
  • Auch wenn Leans Wachstum bei der Formalisierung von Mathematik deutlich ist, eignet sich Rocq mit nativer Koinduktion, verschiedenen Extraktionspfaden und einem gewachsenen Verifikations-Ökosystem besser für die Verifikation ausführbarer Programme
  • Rocq deklariert Codaten mit CoInductive und CoFixpoint, prüft die Guardedness und extrahiert sie anschließend als verzögert ausgeführten Code; in Lean muss man sich dagegen zwischen Library-Encoding, Iteratoren, Thunk und partial def entscheiden
  • Leans Prüfer für verschachtelte induktive Typen weist einige Verifikationsrelationen zurück, die Rocq zulässt; im JSON-Schema-Beispiel muss daher ein einzelner Forall₂-Beweis in mehrere Relationen aufgeteilt und ein eigenes Induktionsprinzip bereitgestellt werden
  • Rocq bietet Programmextraktionspfade nach OCaml, Haskell, Rust, C++, WebAssembly usw. sowie Verifikationsgrundlagen wie Iris, CompCert und Interaction Trees, sodass verifizierte Logik eines realen Spiels mit ausführbarem Code verbunden werden kann
  • Auch AI-Agenten können Rocq-Code schreiben, wenn Dokumentation und Beispiele vorhanden sind; ein Wechsel zu Lean müsste nicht nur Definitionen ersetzen, sondern auch Extraktionspipeline, Libraries sowie regulatorische und institutionelle Historie, weshalb er für die aktuelle Arbeit zu wenig praktischen Nutzen bringt

Vergleich aus Sicht der Programmverifikation

  • Gegenstand des Vergleichs ist nicht die Formalisierung von Mathematik, sondern Programmverifikation; in der Mathematik hat Lean tatsächlich eine eigene Wachstumsdynamik
  • „Besser“ meint keine absolute Überlegenheit, sondern dass Rocq besser zu der derzeit ausgeführten Arbeit passt
  • Mit den Erfolgen von AI in der Mathematik und dem wachsenden Interesse an Lean wurde häufig gefragt, warum Rocq weiter genutzt wird; die Argumentation geht von Folien einer LangSec-Keynote aus

Native koinduktive Typen und cofixpoint

  • Was Leans coinductive abdeckt

    • Die von Wojciech Różowski und Joachim Breitner von Lean FRO entwickelte Unterstützung für koinduktive Prädikate ist im Befehl coinductive von Lean 4.25 enthalten
    • Diese Funktion ist für Bisimulation und koinduktive Beweise nützlich, bietet aber keine ausführbaren cofixpoints in Type und keine extrahierbaren Programme
    • Rocqs CoInductive und CoFixpoint stellen ausführbare Codaten (codata) direkt in Type bereit
    • In Lean gibt es keine entsprechende Kernel-Deklaration, daher müssen allgemeine Funktionen, Strukturen oder Library-Encodings verwendet werden

  • Deklarationsbeschränkungen von QPFTypes

    • Alex Keizers QPFTypes ist ein Proof-of-Concept-Paket für allgemeine Codaten, das aus einer codata-Spezifikation Destruktoren, Corecursoren und Bisimulationsprinzipien erzeugt
    • Anders als Rocqs CoInductive ist es keine Kernel-Deklaration, sondern ein Library-Encoding
    • Die Beispiele verwenden eine auf Lean 4.25.0 festgelegte Toolchain, damals die neueste unterstützte Version
    • In Rocq funktionieren die folgenden drei gewöhnlichen Deklarationen, in QPFTypes jedoch nicht
      • Parameterlose Codaten schlagen wegen eines Implementierungsfehlers fehl
      • Wechselseitige koinduktive Deklarationen wie tree und forest werden wegen Leans Beschränkungen für mutual blocks nicht unterstützt
      • Indizierte koinduktive Familien wie istream, bei denen der Clock-Index bei jedem Schritt fortschreitet, werden aufgrund einer Grenze von QPF selbst nicht unterstützt
    • Auch bei Protokollen, Phasen, Größen und Zustandsautomaten werden indizierte koinduktive Muster verwendet; sobald man jedoch den einfachen, nicht wechselseitigen und nicht indizierten Bereich von QPFTypes verlässt, muss man die Low-Level-APIs MvQPF.Cofix.corec und bisim direkt verwenden, oder die Umsetzung ist nicht möglich
    • Auch Rocqs Guardedness-Prüfer ist schwer zu handhaben, doch die genannten Fälle lassen sich ohne separates Encoding deklarieren
    • Paco und Damien Pous’ coinduction unterstützen koinduktive Prädikate und Relationsbeweise, ersetzen aber kein CoFixpoint für Programme

  • Unterschiede bei extrahierten Programmen

    • Rocqs native cofixpoints werden als echte verzögerte OCaml-Werte extrahiert
    • unfold_cotree aus der game tree library wird zu einem mit Lazy.t umschlossenen Baum und einer rekursiven verzögerten Erzeugungsfunktion
    • Das Ergebnis kommt einer von Hand geschriebenen verzögerten Baumstruktur nahe
    • In QPFTypes laufen Erzeugung und Beobachtung über MvQPF.Cofix.corec und MvQPF.Cofix.dest, und auch das extrahierte Programm behält die verallgemeinerte Cofix-Darstellung bei
    • BadCoinduction.lean enthält Colist und Cotree, die erzeugten Interfaces, Fehlschläge für parameterlose, wechselseitige und indizierte Codaten sowie den QPFTypes-Commit und die Befehle zur Reproduktion

In Lean wählbare Alternativen

  • Streams und Iteratoren

    • Stream' aus mathlib ist eine Funktion Nat → α
    • Man kann das Element an Position n berechnen; außerdem werden Corecursoren, Extensionalität, Bisimulation und Hilfslemmata zur Koinduktion bereitgestellt
    • Es handelt sich jedoch nicht um einen verzögerten Konstruktor, dessen Tail ein weiterer Stream ist, und beliebige gegenseitige oder indizierte Kodaten werden damit nicht gelöst
    • Auch eine Zustandsmaschine mit explizitem Zustand und step-Funktion kann als Corecursor dienen
    • Leans Iter ist ein sequenzielles Interface, das auf Anfrage jeweils einen Schritt berechnet
    • Iteratoren können einen Productive-Beweis besitzen, der die Erzeugung eines Werts oder die Terminierung garantiert; für Iter.repeat ist er bereits vorhanden
    • Für benutzerdefinierte Iteratoren muss man das step-Interface, Invarianten und bei Bedarf einen Produktivitätsbeweis selbst liefern
    • Rocqs CoFixpoint prüft die Guardedness rekursiver Aufrufe und gibt einen koinduktiven Wert zurück, ohne eine separate Verknüpfung zwischen Zustandsmaschine und Sequenz zu erfordern

  • Thunk, partial def, unsafe def

    • Leans Thunk berechnet in kompiliertem Code beim ersten Erzwingen und cached das Ergebnis, bietet aber keine Koinduktion
    • In der Logik erscheint es als Unit → α, sodass die gesamte Definition in Beweisen verwendet werden kann, der Cache ist jedoch nicht sichtbar
    • Es erlaubt auch keine Rekursion und prüft nicht, ob Rekursion letztlich einen Konstruktor produziert
    • Auch von Rocq extrahierter Code nutzt Laufzeit-Laziness, besteht aber zuvor die Guardedness-Prüfung
    • partial def kann rekursive Rümpfe ausführen, in der Logik bleibt jedoch nur eine opake Konstante übrig
    • Da Terminierung oder Produktivität nicht geprüft werden, werden sowohl Produzenten für natürliche Zahlen als auch Produzenten akzeptiert, die sofort in unendliche Rekursion laufen
    • Auch unsafe def kann ausgeführt werden, darf aber in theorem-sicheren Deklarationen nicht referenziert werden
    • MLList aus Batteries kombiniert eine private unsafe Lazy-Implementierung, ein opakes öffentliches Interface sowie mit partial def geschriebene Produzenten fix und iterate
    • Solche Produzenten lassen sich in Beweisen nicht wie beobachtete Rocq-CoFixpoints entfalten
    • partial_fixpoint erhält Gleichungen, akzeptiert aber keine Rekursion, die Konstruktoren und Thunks kombiniert
    • QPFTypes stellt Corecursoren und Bisimulationsprinzipien bereit und vermeidet damit Opazität, erfordert aber eine verallgemeinerte Cofix-Darstellung und entsprechende Deklarationsbeschränkungen

Effektvolle und nicht terminierende Programme

  • Interaction Trees stellen Programme, die Effekte haben und möglicherweise nicht terminieren, als koinduktive Bäume dar
    • Mit demselben Baum kann man Programme schreiben, interpretieren und extrahieren sowie in der Regel Gleichungen einschließlich weak bisimulation beweisen
  • Stream' und Iter liefern nur Sequenzen und können daher die für Effekte nötigen verzweigenden Continuations nicht ausdrücken
  • Wenn man Effektbäume mit Thunk und partial def ausführt, werden rekursive Produzenten in Beweisen opak; um Berechnung und Beweise gemeinsam zu unterstützen, braucht es eine Kodaten-Library-Codierung
  • lean4-itree von MIT PLV implementiert Interaction Trees als finale Coalgebra PFunctor.M aus Mathlib
  • PolyFun ergänzt Handler, rekursive Prozeduren, Ausführungsspuren, strong/weak bisimulation sowie Beweise für Monad- und Iterationsgesetze
    • In Lean kann man Bäume berechnen und über sie Beweise führen, dennoch bleiben sie als M-Type in einer Library codiert
    • Es gibt keine nativen Kodaten-Deklarationen, und statt direkter Lazy-Programme bleibt eine generische Darstellung erhalten
  • Auch HITrees umgehen diese Einschränkung nicht
    • Da Lean keine nativen koinduktiven Typen hat, wird nicht der koinduktive Delay-Monad-Ansatz von ITrees verwendet
    • Die Bäume sind induktiv, und Nichtterminierung wird zu einem Effekt höherstufiger Rekursion
    • Rekursive Berechnungen erhalten ihre Bedeutung, wenn ein Handler den Effekt interpretiert, nicht als unendliche Bäume, die sich beobachten und entfalten lassen
    • Ausführung ist über monadische Interpretation möglich und Beweise über Zustandsmaschinen-Interpretation, doch die Gleichungstheorie von HITree liefert keine allgemeinen Gleichungen zum Entfalten von Rekursion
  • Rocq unterstützt Kodaten-Deklarationen, guarded Producer, beobachtungsbasiertes Schließen und direkte Extraktion von Lazy-Code in einem einzigen Ablauf

Verschachtelte induktive Typen und Prädikate

  • Fallbeispiel: JSON-Schema-Validierung

    • Lean erlaubt mehrere verschachtelte induktive Definitionen, lehnt aber einige Definitionen ab, die Rocq akzeptiert
    • Dieser Unterschied wurde in A Rose Tree Is Blooming genutzt und lässt sich mit einem kleineren JSON-Schema-Beispiel reproduzieren
    • JSON und die Schemas selbst lassen sich in beiden Sprachen problemlos definieren
    • Bei der Validierung von Objekt-Schemas muss paarweise geprüft werden, ob die Feldnamen übereinstimmen und ob jeder JSON-Wert für das entsprechende Unterschema gültig ist
    • Rocq kann Namensgleichheit und rekursive Validierung in einer einzigen Forall2-Ableitung speichern
    • Rocq 9.0 lehnt eine Tuple-Pattern-Lambda um rekursive Vorkommen herum als Verstoß gegen strict positivity ab; verwendet man statt Patterns jedoch Projections, kompiliert es
    • Lean 4.32.1 lehnt in demselben Objekt-Konstruktor ein inneres And fälschlich als ungültigen verschachtelten induktiven Datentyp ab, wenn ein rekursives Vorkommen sowohl durch Forall₂ als auch durch And läuft
    • Benachbarte Formen wie Forall₂ ParRed, direkte Rekursion über And·Exists und Forall₂ (fun sf jf => Valid sf.2 jf.2) werden akzeptiert
    • Forall₂ (Eval env), wobei der Relationsparameter die konstruktorlokale Variable env erfasst, scheitert bereits beim Forall₂-Schritt

  • Workarounds und Beweiskosten

    • In Lean lässt sich die Objektvalidierung in zwei Forall₂-Ableitungen aufteilen
      • Eine bewahrt die Gleichheit der Feldnamen
      • Die andere bewahrt die rekursive Validierung der entsprechenden Werte
    • Ohne separate Indizes oder Längenbeweise kann die Listenstruktur beibehalten und auch das Entfernen des Heads strukturell bewiesen werden, allerdings müssen beide Ableitungen zerlegt werden
    • Trennt man die Relationen, verliert man das einzelne Beweisobjekt, in dem jede Namensgleichheit und rekursive Validierung als Paar gebündelt ist
    • Über eine wechselseitige ValidFields-Relation lässt sich die Kopplung wiederherstellen, doch Leans induction-Taktik unterstützt keine wechselseitigen induktiven Typen, und der erzeugte Recursor verlangt für jede Relation ein eigenes Motive
    • Mit einem benutzerdefinierten Induktionstheorem kann man diese Einrichtung verbergen
    • Rocq behält die Standarddarstellung mit Forall2 bei und kann, falls wechselseitige Definitionen nötig sind, mit Scheme ein kombiniertes Prinzip erzeugen
    • Auch Lean kann dieselbe Aussage ohne indexbasierte Codierung ausdrücken, muss dafür aber Deklarationen umstellen und mehr Beweisapparat erstellen
    • Die vollständigen Vergleichsdateien sind NestedPain.v für Rocq 9.0.0 und NestedPain.lean für Lean 4.32.1; Leans erwartete Fehlschläge werden beim Kompilieren mit #guard_msgs geprüft

  • Starke Induktionsprinzipien für verschachtelte Argumente

    • In Beweisen, die elementweise Annahmen über verschachtelte Daten benötigen, etwa wenn Term eine list Term enthält, brauchten beide Systeme einen stärkeren Recursor
    • Rocq 9.2 erzeugt Induktionsannahmen für verschachtelte Argumente, wenn man für den Nesting-Typ ein All-Prädikat und Theoreme registriert
    • Die Standardbibliothek registriert dies nicht standardmäßig, daher muss vor der Deklaration von Term eine Zeile Scheme All for list. hinzugefügt werden
    • Das erzeugte Term_ind und Term_rect erhalten im app-Fall die Annahme list_all Term P l, und der Rumpf ruft list_all_forall auf
    • Fügt man Scheme All for Forall2. hinzu, liefert auch ParRed_ind Induktionsannahmen für die Voraussetzung Forall2 ParRed args args'
    • Ohne Registrierung erscheint neben dem bisherigen schwachen Prinzip eine Warnung [register-all]
    • In Lean muss man weiterhin selbst einen starken Recursor bereitstellen

Optionen zur Programmextraktion

  • Die Lean-Standard-Toolchain kompiliert über eine eigene Runtime; das hat Vorteile, wenn man Lean-Bibliotheken erstellt und das Runtime-Design passt
  • Kim Morrisons verifiziertes lean-zip kann sogar schneller komprimieren als das reine Rust-miniz_oxide, was in Sachen Performance beeindruckend ist
  • Lean bietet jedoch keine mehreren alternativen Extraktions-Backends, und die aktuelle Compiler-Pipeline besitzt keinen End-to-End-Korrektheitsbeweis
    • Seltene Probleme wie der von Kiran Gopinathan entdeckte Runtime-Bug können auftreten
    • Der generierte Code ist auf die Runtime zugeschnitten und nicht darauf ausgelegt, von Menschen gelesen zu werden
  • Rocq bietet mehrere Wege mit unterschiedlichen Kompromissen zwischen Vertrauensbasis und Lesbarkeit

Spiele mit verifizierter Logik ausführen

  • In Rocq werden Eigenschaften desselben Quellcodes wie des ausführbaren Programms maschinell verifiziert; anschließend werden Logik und Event-Loop mit Crane nach C++ extrahiert und über rocq-crane-sdl2 an SDL2 angebunden

  • Rocqman

    • Rocqman beweist die Spielzustandsübergänge, die der Frame-Loop nutzt
      • Der Punktestand sinkt nicht
      • Leben und verbleibende Sammelobjekte nehmen nicht zu
      • Ein Endzustand ist ein Fixpunkt von tick
      • Übergänge für Pause und Endbildschirm werden geprüft

  • Rocqsweeper

    • Rocqsweeper beweist Minesweeper-Regeln und die Eingabeschicht
      • Der erste Klick ist sicher
      • Flaggen erhalten Minen- und Nachbarschaftsdaten
      • Flood Fill erhält Minen und erhöht nicht die Zahl versteckter sicherer Felder
      • Der Cursor verlässt die Grenzen nicht
      • Mausereignisse werden als die erwarteten Zellen interpretiert

  • Reversirocq

    • Reversirocq nutzt die koinduktive Alpha-Beta-KI der game tree library, ebenso wie die von Charles C. Norton hinzugefügten Reversi-Regeln
    • Theoreme behandeln die Aufzählung legaler Züge und Spielergebnisse und verbinden Alpha-Beta mit Minimax auf dem durchsuchten endlichen Prefix

  • Verifikationsgrenze

    • Die Beweisgrenze endet beim Rocq-Quellcode; SDL, Crane, das generierte C++ und die native Runtime sind nicht eingeschlossen
    • Innerhalb dieser Grenze werden Eigenschaften der tatsächlich ausgeführten Logik bewiesen, nicht die eines vom ausführbaren Programm getrennten Modells

Rocq-Ökosystem für Programmverifikation

  • Abstraktionen zur Programmdarstellung

    • Interaction Trees: Stellen Programme mit Effekten, die möglicherweise nicht terminieren, als koinduktive Bäume externer Ereignisse dar und bieten denotationale Semantik sowie gleichungsbasiertes Schließen für unreinen Code
    • Choice Trees: Erweitern dies um interne nichtdeterministische Entscheidungen, um nichtdeterministische Systeme wie Nebenläufigkeit zu modellieren

  • Frameworks für Programmverifikation

    • Iris: Ein Framework für Higher-Order Concurrent Separation Logic für zustandsbehaftete und nebenläufige Programme
    • Iris-Lean entwickelt sich ebenfalls schnell weiter und unterstützt viele Funktionen, ist aber nicht so breit genutzt wie Rocq Iris
    • CFML: Importiert OCaml-Quellcode nach Rocq, erzeugt characteristic formulae und stellt Taktiken für Spezifikationen in Higher-Order Separation Logic bereit
    • Perennial: Ein Iris-basiertes Framework zur Verifikation von Nebenläufigkeit, crash-sicheren Speichern und verteilten Systemen; über Goose wird es mit ausführbaren Programmen eines Go-Subsets verbunden
    • VST: Die Verified Software Toolchain, die funktionale Korrektheit von C-Programmen auf Basis der CompCert-Semantik beweist
    • BRiCk: Programmlogik und Toolchain für reale C++-Programme

  • Tools mit Rocq-Backend oder -Komponenten

    • Frama-C: Plattform für C-Analyse und deduktive Verifikation, die Beweisverpflichtungen an Rocq übergeben kann
    • Why3: Kann Ziele aus seiner eigenen Sprache an mehrere Beweiser schicken und interaktive Beweisverpflichtungen für Rocq exportieren
    • Cerberus: Ausführbare formale Semantik für ein praxisnahes, großes C-Subset, mit einer Rocq-Implementierung für das CHERI-C-Speichermodell

  • Semantiken realer Sprachen und verifizierte Compiler

    • CompCert: Formal verifizierter optimierender C-Compiler
    • Vellvm: Bietet eine Rocq-Spezifikation und abstrakte Semantik von LLVM IR sowie einen ausführbaren Interpreter, dessen Verfeinerung darauf bewiesen ist
    • Vélus: Verifizierter Compiler von Lustre nach CompCerts Clight
    • WasmCert: Mechanisierte formale Semantik von WebAssembly
    • JSCert: Formale JavaScript-Semantik, die der ECMAScript-5-Spezifikation folgt

  • Leichtgewichtige Verifikation durch Übersetzung

    • hs-to-coq: Übersetzt Haskell-Quellcode nach Rocq
    • rocq-of-ocaml: Übersetzt OCaml-Quellcode nach Rocq
    • rocq-of-python: Übersetzt Python-Quellcode nach Rocq
    • rocq-of-rust: Übersetzt Rust-Quellcode nach Rocq
    • Aeneas: Wandelt Rust, das den Borrow Check bestanden hat, in ein reines Funktionsmodell zur Verifikation um und unterstützt auch Lean als Ziel

  • Programmsynthese und Parsing

    • Fiat Crypto: Leitet hochperformante Kryptografie-Arithmetik für Browser und TLS-Bibliotheken correct-by-construction her
    • Rupicola: Relationales Compiler-Tool, das niedrigstufige funktionale Gallina-Programme in imperative Bedrock2-Programme umwandelt
    • Narcissus: Leitet correct-by-construction Encoder und Decoder für Binärformate her
    • Verbatim: Verifizierter Lexer auf Basis regulärer Ausdrücke
    • CoStar: Verifizierter Parser auf Basis des ALL(*)-Algorithmus

  • Wartungsstatus

    • Einige Projekte werden nicht aktiv gepflegt, konnten aber an Agenten übergeben und wieder gebaut und ausgeführt werden
    • Selbst wenn ein benötigter Baustein kurzfristig nach Lean portiert werden kann, werden die im gesamten Ökosystem angesammelten Funktionen und Nutzungshistorien nicht automatisch mit übertragen

Regulierung und Zertifizierungshistorie

  • Es gibt keine direkte Zertifizierungserfahrung zur regulatorischen Akzeptanz; das kann insbesondere für Akteure in Europa ein wichtigerer Faktor sein
  • Die französische ANSSI hat Kriterien für den Einsatz von Rocq in Common-Criteria-Evaluierungen veröffentlicht
  • CompCert gibt an, durch Arbeiten von AbsInt nach Vorgaben von Airbus für den MFC_NG-Computer der ATR-42/72-Flugzeuge im Jahr 2026 erfolgreich qualifiziert worden zu sein
  • Es ist nicht klar, welche Anforderungen ein Lean-Port in derselben Umgebung erfüllen müsste; auch eine saubere Portierung erbt die bestehende Zertifizierungshistorie nicht automatisch

AI-Agenten und Umstellungskosten

  • Entgegen der Annahme, dass AI-Agenten nur Lean gut schreiben, können sie auch Rocq-Code ausreichend gut schreiben
  • Rocq existiert seit den späten 1980er-Jahren, entsprechend umfangreich sind Codebasis und Dokumentation
  • Da heutige Modelle sich bei bereitgestellter Dokumentation und Beispielen auch gut an unvertraute Sprachen anpassen, ist die Begründung, sie kennten nur populäre Sprachen, keine langfristige Grundlage für einen Wechsel des Proof Assistants
  • Auch in Lean laufen ernsthafte Arbeiten zur Programmverifikation, etwa mvcgen und Velvet
  • Um die aktuelle Arbeit nach Lean zu übertragen, müssten Definitionen neu aufgebaut sowie Extraktions-Pipeline, Bibliotheken und institutionelle Historie ersetzt werden; daher ist Rocq derzeit besser geeignet

Verwandte Beiträge

Noch keine Kommentare.

Noch keine Kommentare.