💻 computer science

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

Die Autoren stellen Foxtrot vor, die erste höherstufige Trennungslogik zur Verifikation der kontextuellen Verfeinerung höherstufiger, nebenläufiger probabilistischer Programme mit höherstufigem lokalem Zustand, die in den Rocq-Beweisassistenten mechanisiert wurde.

Ursprüngliche Autoren: Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal

Veröffentlicht 2026-04-20

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal

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

Stellen Sie sich vor, Sie sind ein Chefkoch in einer extrem chaotischen, aber hochmodernen Küche. In dieser Küche gibt es zwei besondere Herausforderungen:

Das Zufallselement: Manchmal müssen Sie Zutaten auswählen, die Sie nicht selbst bestimmen können. Sie werfen einen Würfel, um zu entscheiden, ob Sie Salz oder Pfeffer nehmen. Das ist die Wahrscheinlichkeit.
Das Chaos der Köche: Es gibt nicht nur einen Koch, sondern viele, die gleichzeitig arbeiten. Sie müssen sich nicht absprechen, wer wann was macht. Der Küchenchef (der "Scheduler") entscheidet im letzten Moment, welcher Koch als nächstes den Herd bedient. Das ist die Parallelität.

Die Aufgabe dieses Forschungsprojekts (genannt Foxtrot) war es, ein neues Regelwerk zu erfinden, mit dem man beweisen kann, dass zwei verschiedene Rezepte (Programme) am Ende genau das gleiche Gericht liefern – auch wenn sie völlig unterschiedlich gekocht wurden und mitten im Chaos der Küche stattgefunden haben.

Hier ist die Erklärung der wichtigsten Ideen, übersetzt in einfache Sprache:

1. Das Problem: Warum ist das so schwer?

Stellen Sie sich vor, Sie haben zwei Rezepte für einen Kuchen:

Rezept A: Ein Koch würfelt eine 3 und ein anderer würfelt eine 5. Dann werden die Zahlen zusammengelegt.
Rezept B: Ein Koch würfelt einfach direkt eine 8.

Mathematisch gesehen ist das Ergebnis bei beiden Rezepten gleich (eine zufällige Zahl zwischen 0 und 255). Aber wie beweist man das formell?
Das Problem ist, dass in einer parallelen Küche (Concurrency) der Zufall (Probability) und die Reihenfolge der Handlungen sich gegenseitig beeinflussen. Wenn Sie versuchen, die beiden Rezepte zu vergleichen, müssen Sie sich vorstellen, dass ein "böser" Küchenchef (ein Gegner) versucht, die Reihenfolge der Würfe so zu manipulieren, dass die Ergebnisse unterschiedlich aussehen.

Bisher gab es keine Werkzeuge, die stark genug waren, um diese komplexe Mischung aus Zufall, Parallelität und komplexen Funktionen (wie verschachtelte Kochanweisungen) zu beweisen.

2. Die Lösung: Foxtrot – Der neue Koch-Check

Die Autoren haben Foxtrot entwickelt. Man kann sich Foxtrot wie einen super-intelligenten, unsichtbaren Qualitätskontrolleur vorstellen, der über der Küche schwebt. Foxtrot hat drei magische Werkzeuge im Gepäck:

A. Die "Vorschau-Bänder" (Presampling Tapes)

Stellen Sie sich vor, Sie wollen zwei verschiedene Rezepte vergleichen, bei denen im einen Rezept zwei Würfe nacheinander gemacht werden, im anderen aber nur einer.
Foxtrot nutzt ein Trick: Es schreibt sich die Ergebnisse der Würfe im Voraus auf ein imaginäres Band (ein "Tape").

Beispiel: Beim Vergleich von Rezept A (zwei Würfe) und Rezept B (ein Wurf) schreibt Foxtrot auf das Band: "Wenn der erste Wurf eine 3 ist und der zweite eine 5, dann ist das Ergebnis 35".
Dann kann Foxtrot das "einzelne" Rezept von B so tun, als würde es auch auf dieses Band zugreifen. So können sie die beiden völlig unterschiedlichen Abläufe direkt miteinander vergleichen, als wären sie das Gleiche.
Wichtig: Das Band existiert nur im Kopf des Qualitätskontrolleurs, nicht in der echten Küche. Es ändert nichts am eigentlichen Kochen, hilft aber beim Beweis.

B. Die "Fehler-Guthaben" (Error Credits)

Manchmal sind Rezepte nicht 100 % identisch, sondern nur "fast" identisch.

Beispiel: Ein Rezept (Rejektions-Sampling) wirft einen Würfel immer wieder, bis eine bestimmte Zahl kommt. Das andere Rezept wirft einfach nur einmal.
Foxtrot nutzt eine Art "Guthaben-Konto" für Fehler. Es sagt: "Okay, wir akzeptieren einen winzigen Fehler von 0,001 %." Wenn das Rezept mit dem wiederholten Wurf scheitert, wird dieses Guthaben verbraucht. Aber Foxtrot beweist, dass man dieses Guthaben immer wieder so klein machen kann, dass es am Ende gegen Null geht. So wird aus "fast gleich" ein "wirklich gleich".

C. Die "Geister-Resourcen" (Ghost Resources)

In der Küche gibt es Dinge, die man nicht sehen kann, aber die wichtig sind (wie eine geheime Zutat, die nur der Chef weiß). Foxtrot erlaubt es, diese unsichtbaren Dinge in den Beweis einzubauen, um zu zeigen, dass zwei verschiedene Wege zum selben Ziel führen, auch wenn sie unterschiedliche "Geister" (Zustände) durchlaufen.

3. Warum ist das eine große Leistung?

Bisher gab es Werkzeuge, die entweder nur den Zufall verstanden ODER nur die Parallelität. Foxtrot ist das erste Werkzeug, das beides gleichzeitig beherrscht, und zwar für sehr komplexe Programme (die Funktionen als Daten verwenden können, also "Higher-Order").

Ein konkretes Beispiel aus dem Papier:
Die Autoren haben Foxtrot benutzt, um die Sicherheit einer echten Verschlüsselungssoftware (Sodium) zu beweisen. Diese Software muss zufällige Zahlen generieren, um Schlüssel zu erstellen.

Die Herausforderung: Die Software macht das in einer parallelen Umgebung. Ein Angreifer könnte versuchen, die Reihenfolge der Zufallszahlen zu manipulieren.
Der Beweis mit Foxtrot: Sie konnten beweisen, dass die Software, egal wie der Angreifer die parallelen Threads durcheinanderwirbelt, am Ende immer noch eine perfekt zufällige Zahl liefert. Das ist wie ein Beweis, dass Ihr Kuchen immer perfekt schmeckt, egal ob der Koch zuerst den Ofen anmacht oder zuerst den Teig knetet.

4. Das Geheimnis hinter den Kulissen (Die Mathematik)

Um Foxtrot zu bauen, mussten die Autoren eine sehr knifflige mathematische Regel anwenden (ein Axiom der Wahl), das in der Welt der Logik normalerweise verboten ist, weil es zu paradoxen Ergebnissen führen kann. Aber sie haben es so clever verpackt, dass es nur für die "Beweis-Logik" gilt und nicht die eigentliche Programmierung verdirbt. Man kann sich das vorstellen wie einen Zaubertrick, der nur im Hintergrund funktioniert, damit der Magier (der Beweis) seine Arbeit erledigen kann, ohne dass das Publikum (der Programmierer) es merkt.

Zusammenfassung

Foxtrot ist wie ein neuer, super-starker Übersetzer für Programmierer. Er nimmt zwei völlig unterschiedliche, chaotische und zufallsbasierte Programme und sagt Ihnen mit mathematischer Sicherheit: "Diese beiden Programme sind im Grunde dasselbe."

Das ist extrem wichtig für die Sicherheit von Software, besonders in der Kryptographie, wo ein kleiner Fehler im Zufallsgenerator dazu führen kann, dass geheime Nachrichten geknackt werden. Mit Foxtrot können Ingenieure jetzt beweisen, dass ihre komplexen, parallelen Systeme sicher sind, bevor sie sie in die reale Welt entlassen.

1. Problemstellung und Motivation

Die Arbeit adressiert die formale Verifikation von Programmen, die zwei komplexe und oft schwer zu kombinierende Sprachfeatures vereinen: Konkurrenz (Parallelität) und Probabilistik (Zufälligkeit).

Herausforderung: Während es etablierte Methoden für die Verifikation von reinen probabilistischen Programmen (z. B. mittels probabilistischer Kopplung) oder reinen konkurrenten Programmen (z. B. mittels Separation Logic und Invarianten) gibt, fehlt es an ausdrucksstarken Methoden für die Kombination beider.
Das Kernproblem: Die semantische Komposition von Nichtdeterminismus (durch Thread-Scheduling) und probabilistischer Wahl ist nicht trivial. Insbesondere bei höherstufigen Programmen (Higher-Order) mit lokalem Zustand (Heap) und dynamisch allokierten Threads ist es schwierig, eine kontextuelle Verfeinerung (Contextual Refinement) zu beweisen.
Definition: Kontextuelle Verfeinerung bedeutet, dass ein Programm $e_1$ in jedem möglichen Kontext $C$ ein Verhalten zeigt, das durch ein anderes Programm $e_2$ „abgedeckt" wird (hier: die Wahrscheinlichkeit des Terminierens von $C[e_1]$ ist kleiner oder gleich der von $C[e_2]$ ).
Lücken in der aktuellen Forschung: Bisherige Ansätze konnten entweder keine höheren Funktionen, keinen lokalen Zustand oder keine komplexe Interaktion zwischen Parallelität und Zufall gleichzeitig behandeln. Es gab keine mechanisierte Logik für höherstufige, konkurrente und probabilistische Programme.

2. Methodik: Foxtrot

Die Autoren stellen Foxtrot vor, die erste höherstufige Separation Logic, die speziell für den Nachweis kontextueller Verfeinerung in diesem Setting entwickelt wurde. Foxtrot ist auf dem Iris-Framework (einer Erweiterung der Separation Logic für höhere Funktionen und Invarianten) und dem Rocq (ehemals Coq) Beweisassistenten implementiert.

2.1 Sprachmodell (ConcRandML)

Die Logik basiert auf der Sprache ConcRandML, einer ML-ähnlichen Sprache mit:

Höherstufigen Funktionen und polymorphen Typen.
Dynamisch allokiertem lokalem Zustand (Referenzen).
Diskreter probabilistischer Sampling-Operation (rand).
Unstrukturierter Parallelität via fork.
Einem semantischen Modell, das probabilistische, zustandsbehaftete Scheduler verwendet, um Nichtdeterminismus aufzulösen. Die Verfeinerung wird über die „obere Terminierungswahrscheinlichkeit" (Supremum über alle Scheduler) definiert.

2.2 Logische Struktur

Foxtrot nutzt binäre logische Relationen, um die Verfeinerung zu definieren. Ein Urteil $\Delta \models e \sqsubseteq e' : \tau$ besagt, dass $e$ $e'$ verfeinert.

Hoare-Tripel: Die Logik verwendet annotierte Hoare-Tripel $\{P\} e \{Q\}$ , die auf einer Schwächsten-Vorbedingung (Weakest Precondition, wp) basieren.
Ghost State & Ressourcen: Wie in Iris üblich, werden Invarianten und Ghost-Ressourcen genutzt, um den Zustand zwischen den beiden zu vergleichenden Programmen (Implementierung und Spezifikation) zu verknüpfen.

2.3 Schlüsseltechniken und Fortschritte

Foxtrot integriert und erweitert bestehende Konzepte, um die spezifischen Schwierigkeiten der Kombination von Konkurrenz und Wahrscheinlichkeit zu lösen:

Probabilistische Update-Modality ( $|\!\!\leadsto$ ):
Ermöglicht das symbolische Ausführen der rechten Seite (Spezifikation) innerhalb der Logik. Dies ist entscheidend, um Kopplungen zwischen den beiden Programmen herzustellen.
Presampling Tapes (Bänder):
Inspiriert von der Logik Clutch. Um mehrere unabhängige Zufallsziehungen in verschiedenen Threads der linken Seite (Implementierung) mit einer einzigen Ziehung auf der rechten Seite zu koppeln, werden „Presampling Tapes" verwendet.
- Die Logik erlaubt es, Zufallswerte im Voraus auf ein Band zu schreiben (nur im Beweis, nicht in der Ausführung).
- Dies erlaubt es, komplexe Verteilungen, die durch parallele Threads entstehen, als eine einzige deterministische Sequenz zu behandeln.
- Wichtige Einschränkung: Im Gegensatz zu früheren Logiken ist Presampling auf der rechten Seite (Spezifikation) in Foxtrot unsound, da dies Scheduler erlauben würde, auf zukünftige Zufallsentscheidungen zu reagieren, was gegen die Semantik von ConcRandML verstößt.
Fragmented Couplings (Gebrochene Kopplungen):
Für Algorithmen wie Rejection Sampling (z. B. rand N, falls Ergebnis $\le M$ , sonst neu versuchen), die unendliche Schleifen beinhalten können, werden gebrochene Kopplungen verwendet. Diese erlauben es, nur bei akzeptierten Werten eine Kopplung herzustellen und bei abgelehnten Werten die rechte Seite nicht zu schrittweise zu führen.
Fehlerkredite und Induktion durch Fehlerverstärkung (Error Amplification):
Inspiriert von Eris und Approxis. Um die Konvergenz von Rejection Samplern zu beweisen, werden Ressourcen namens „Error Credits" $E(\varepsilon)$ verwendet.
- Man beweist, dass die Programme für einen beliebigen kleinen Fehler $\varepsilon$ äquivalent sind.
- Durch eine Induktionsregel (ind-err-amp) wird der Fehler bei jedem Schleifendurchlauf um einen Faktor $k > 1$ verstärkt. Da der Fehler gegen 0 konvergiert, wird die exakte Äquivalenz bewiesen.
Das Axiom der Wahl (Axiom of Choice):
Ein zentraler technischer Durchbruch ist die Verwendung einer Version des Axioms der Wahl innerhalb der Iris-Logik.
- Problem: Um die Korrektheit zu beweisen, muss für jeden Scheduler der linken Seite ein entsprechender Scheduler der rechten Seite konstruiert werden. Da probabilistische Verzweigungen eine Familie von Scheduling-Entscheidungen erzeugen, müssen diese Familien „zusammengesetzt" werden.
- Lösung: Die Autoren nutzen das Axiom der Wahl, um aus der Existenz von Scheduling-Familien eine globale Funktion (einen Scheduler) zu konstruieren. Dies ist in früheren Iris-basierten Logiken nicht vorgekommen und erfordert eine sorgfältige Behandlung, um die Intuitionistik der Logik nicht zu verletzen (durch Einschränkung auf Meta-Level-Typen).

3. Wichtige Beiträge

Foxtrot: Die erste höherstufige Separation Logic für kontextuelle Verfeinerung von konkurrenten probabilistischen Programmen mit lokalem Zustand.
Soundness-Beweis: Ein vollständiger mechanisierter Beweis der Korrektheit der Logik, der auf einem neuartigen semantischen Modell basiert, das „Full-Information Scheduler" und das Axiom der Wahl integriert.
Erweiterte Beweisregeln: Einführung und Verifizierung von Regeln für Presampling Tapes (nur links), gebrochene Kopplungen und Fehlerverstärkung in einem konkurrenten Kontext.
Mechanisierung: Alle Ergebnisse sind im Rocq-Beweisassistenten (mit Iris-Framework und Coquelicot für reelle Analysis) formalisiert.

4. Ergebnisse und Fallstudien

Die Autoren demonstrieren die Ausdruckskraft von Foxtrot an mehreren komplexen Beispielen, die mit vorherigen Techniken nicht verifizierbar waren:

Adversarial von Neumann Coin: Ein Programm, das eine verzerrte Münze (deren Bias durch einen adversarischen Thread dynamisch geändert werden kann) in eine faire Münze umwandelt. Foxtrot beweist die kontextuelle Äquivalenz zu einer fairen Münze, selbst in Anwesenheit von Angreifern, die den Zustand manipulieren.
Sodium randombytes_uniform: Eine Verifikation der Implementierung einer gleichverteilten Zufallszahlengenerierung in der Kryptographie-Bibliothek Sodium. Der Beweis zeigt, dass die komplexe Implementierung (die Rejection Sampling und nicht-atomare Operationen nutzt) auch in konkurrenten Umgebungen korrekt und thread-sicher ist.
Batch Sampling: Der Nachweis, dass das parallele Ziehen zweier Zufallszahlen und deren Kombination äquivalent zum Ziehen einer einzigen, größeren Zufallszahl ist. Dies erfordert die Nutzung von Presampling Tapes, um die parallelen Threads auf der linken Seite zu „komprimieren".

5. Bedeutung und Ausblick

Durchbruch: Die Arbeit schließt eine signifikante Lücke in der formalen Verifikation. Sie zeigt, dass es möglich ist, hochkomplexe Eigenschaften (Kombination von Higher-Order, State, Concurrency, Probability) mechanisch zu beweisen.
Sicherheit: Die Ergebnisse sind besonders relevant für die Verifikation von kryptographischen Protokollen und verteilten Systemen, die oft auf Zufall und Parallelität angewiesen sind.
Theoretische Tiefe: Die Integration des Axioms der Wahl in die Iris-Logik öffnet neue Türen für die Konstruktion semantischer Modelle, die bisher als zu komplex galten.
Zukünftige Arbeiten: Die Autoren planen, die Logik auf Scheduler mit eingeschränkter Macht (für Sicherheitsgarantien) zu erweitern, Prophezeiungsvariablen (Prophecy Variables) einzuführen und „Must-Termination" (garantierte Terminierung) zu behandeln.

Zusammenfassend stellt Foxtrot einen Meilenstein in der Programmverifikation dar, der die Grenzen dessen, was formal über probabilistische und konkurrente Systeme bewiesen werden kann, erheblich erweitert.