💻 computer science

Automated Reasoning with Nested Datatypes

Dieses Papier führt eine Theorie verschachtelter Datentypen ein, die die Kombination von Datentypen und Arrays einschränkt, um nicht-standardmäßige Modelle zu verhindern, stellt ein nachweislich korrektes Entscheidungsverfahren dafür bereit und evaluiert eine Implementierung dieses Verfahrens anhand von realen und handgefertigten Benchmarks.

Ursprüngliche Autoren: Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Veröffentlicht 2026-07-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

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 bauen eine komplexe digitale Stadt mit zwei verschiedenen Arten von Lego-Steinen: Datentypen und Arrays.

Datentypen sind wie Stammbäume oder Organigramme. Sie sind hierarchisch. Eine „Person“ kann ein „Kind“ haben, und dieses Kind kann wiederum ein eigenes „Kind“ haben. Die Regel hier ist einfach: Niemand kann sein eigener Vorfahre sein. Man kann keinen Stammbaum haben, in dem eine Person ihr eigener Großelternteil ist; das erzeugt eine logische Schleife (einen Zyklus), die die Struktur zerstört.
Arrays sind wie Briefkästen oder Schließfächer. Sie sind flach und ermöglichen es, jedes Element sofort über seine Nummer (Index) abzugreifen. Man kann alles in einen Briefkasten legen, sogar einen ganzen Stammbaum.

Das Problem: Die „Endlosschleifen“-Falle

Das Paper beginnt mit dem Hinweis auf einen gefährlichen Fehler, der auftritt, wenn man diese beiden Systeme unbedacht kombiniert.

Stellen Sie sich vor, Sie haben eine Person (einen Datentyp), die ein Feld namens „Familie“ besitzt. In einer normalen Welt ist „Familie“ eine Liste von Personen. Aber in dieser fehlerhaften Welt ist „Familie“ ein Array (ein Schließfach).

Sie legen eine bestimmte Person (nennen wir ihn Bob) in Schließfach #5.
Dann definieren Sie Bobs „Familie“-Feld als Schließfach #5.

Schauen Sie nun, was passiert:

Um Bobs Familie zu finden, öffnen Sie Schließfach #5.
In Schließfach #5 finden Sie Bob.
Um Bobs Familie zu finden, öffnen Sie erneut Schließfach #5.
Sie finden Bob erneut.

Sie stecken in einer Endlosschleife fest. In der Informatik wird dies als nicht-standardmäßiges Modell bezeichnet. Es ist wie eine Schlange, die sich selbst in den Schwanz beißt. Während ein Computer dies technisch gesehen zulassen könnte, bricht es die intuitiven Regeln dafür, wie Datenstrukturen funktionieren sollten. Es erzeugt einen „Zyklus“, der eigentlich nicht existieren dürfte.

Die Lösung: Die Theorie der „Verschachtelten Datentypen“

Die Autoren, Tomer Hakak und sein Team, sagen: „Wir brauchen ein Regelwerk, das dieses Szenario der Schlange, die ihren eigenen Schwanz frisst, verhindert.“

Sie führen eine neue Theorie namens Verschachtelte Datatypen (Nested Datatypes) ein. Betrachten Sie dies als einen strengen Bauplan für Ihre digitale Stadt.

Die Regel: Sie können einen Stammbaum in ein Schließfach legen, und Sie können ein Schließfach in einen Stammbaum legen, ABER Sie dürfen keinen Pfad erstellen, der Sie wieder an den Ausgangspunkt zurückführt.
Das Ziel: Wenn Sie einem Pfad von einer Person über ihr Familien-Array zu einer anderen Person folgen und durch deren Familien-Array zurückkehren, dürfen Sie niemals wieder bei der ursprünglichen Person ankommen.

Wie sie es gelöst haben: Die „Übersetzer“-Maschine

Die schwierige Aufgabe besteht darin, dass Computer sehr gut darin sind zu prüfen, ob ein Stammbaum gültig ist, und sehr gut darin, ob Schließfächer gültig sind. Aber sie sind schlecht darin zu prüfen, ob eine Kombination aus beiden einen Zyklus erzeugt.

Die Autoren haben einen Übersetzer (ein Entscheidungsverfahren) gebaut. So funktioniert er, unter Verwendung einer Metapher:

Stellen Sie sich vor, Sie haben ein Puzzle mit zwei verschiedenen Arten von Teilen: Baum-Teilen und Box-Teilen. Der Computer weiß nicht, wie er nach Schleifen suchen soll, wenn diese gemischt sind.

Die Übersetzung: Der Algorithmus der Autoren nimmt das gemischte Puzzle und übersetzt es in eine Sprache, die der Computer tatsächlich versteht. Er verwandelt die „Box-Teile“ in spezielle „Baum-Teile“, die wie Boxen aussehen, aber wie Bäume funktionieren.
Das Sicherheitsnetz: Sie fügen der Übersetzung zusätzliche „Leitplanken“ (Lemmata) hinzu. Diese Leitplanken stellen sicher, dass, falls in dem ursprünglichen gemischten Puzzle eine Schleife existiert hätte, die übersetzte Baum-Version sofort einen Widerspruch aufzeigt (wie der Versuch, einen Turm zu bauen, der der Schwerkraft trotzt).
Die Prüfung: Der Computer prüft das übersetzte Puzzle.
- Wenn das übersetzte Puzzle unmöglich ist (unerfüllbar), bedeutet dies, dass das ursprüngliche gemischte Puzzle eine verbotene Schleife enthielt.
- Wenn das übersetzte Puzzle funktioniert, ist das ursprüngliche Puzzle sicher.

Warum das wichtig ist (laut dem Paper)

Die Autoren haben nicht nur eine Theorie geschrieben; sie haben einen Prototyp innerhalb eines realen Computerprogramms namens cvc5 (ein Werkzeug zur Verifizierung von Software) gebaut.

Realwelt-Test: Sie haben es mit Benchmarks aus dem Move Prover getestet, einem Werkzeug zur Verifizierung von Smart Contracts (digitalen Geldvereinbarungen). Diese Verträge nutzen oft komplexe verschachtelte Daten.
Synthetischer Test: Sie haben künstliche Puzzles erstellt, die speziell darauf ausgelegt sind, andere Solver in Endlosschleifen zu locken.
Das Ergebnis: Ihre neue Methode hat erfolgreich die Schleifen erkannt, die andere Methoden übersehen haben. In vielen Fällen war sie schneller und genauer als das bestehende Tool Z3, das für ähnliche Aufgaben eingesetzt wird.

Zusammenfassung

Kurz gesagt geht es in diesem Paper darum, einen Fehler zu beheben, der auftritt, wenn Computer komplexe Daten verstehen.

Der Fehler: Die Mischung von „Stammbäumen“ und „Briefkästen“ kann versehentlich Endlosschleifen erzeugen, in denen eine Person ihr eigener Vorfahre ist.
Die Lösung: Ein neues Regelwerk (Theorie der Verschachtelten Datentypen), das diese Schleifen strikt verbietet.
Das Werkzeug: Ein Übersetzer, der diese komplexen gemischten Regeln in ein Format umwandelt, das Computer leicht auf Sicherheit prüfen können, um sicherzustellen, dass Ihre digitalen Datenstrukturen logisch und frei von Schleifen bleiben.

Technisches Resümee: Automatisiertes Schließen mit verschachtelten Datentypen

1. Problemstellung

Die SMT-LIB-Theorie der Datentypen bietet eine praktische Kodierung für Datenstrukturen wie Listen und Bäume, die für die Softwareverifizierung essenziell sind. Ihre Ausdrucksstärke ist jedoch durch das Fehlen von Update-Operatoren und Random-Access-Funktionen begrenzt. Um dies zu adressieren, wird oft eine naive Kombination von Datentypen mit der Theorie der Arrays versucht.

Das Kernproblem, das in dieser Arbeit identifiziert wird, ist, dass eine solche naive Kombination nicht-standardmäßige Modelle einführt. Speziell wird das Prinzip der Azyklizität – welches besagt, dass ein Datentyp-Wert sich nicht selbst enthalten darf – umgangen, wenn Arrays im Spiel sind. Ein Datentyp-Wert kann als Element eines Arrays erscheinen, wobei dieses Array wiederum ein Feld desselben Datentyp-Wertes ist. Dies erzeugt einen Zyklus, den die Standardkombination von Theorien (via Nelson-Oppen) nicht erkennt, da der Zyklus zwischen dem Datentyp- und dem Array-Komponenten „gespalten“ ist. Diese nicht-standardmäßigen Modelle sind unerwünscht, da sie nicht mit der intuitiven Semantik verschachtelter Datenstrukturen übereinstimmen, die für die Verifizierung vorgesehen sind.

2. Methodik

Die Autoren schlagen eine Theorie der verschachtelten Datentypen vor, die diese nicht-standardmäßigen Modelle explizit ausschließt. Die Methodologie besteht aus zwei Hauptkomponenten: einer formalen Definition der Theorie und einem Entscheidungsverfahren basierend auf Reduktion.

2.1. Formale Definition

Die Theorie wird durch die Einschränkung der Standardkombination von Datentypen und Arrays definiert.

Wohldefiniertheit: Die Autoren führen eine neue Definition von wohldefinierten Sorten (Definition 10) ein, die die Anwesenheit von Array-Sorten berücksichtigt. Dies stellt sicher, dass die rekursive Struktur von Datentypen wohldefiniert bleibt, selbst wenn Array-Elemente involviert sind.
NDT-Relation: Um nicht-standardmäßige Modelle auszuschließen, definieren die Autoren eine Relation $\mathcal{R}_{\mathcal{A}}$ auf den Strukturen (Definition 16). Diese Relation verbindet Terme mit ihren Untertermen und Arrays mit ihren Elementen. Eine Struktur gilt nur dann als gültige NDT-Struktur, wenn diese Relation wohldefiniert ist. Dies schließt effektiv Zyklen aus, in denen ein Datentyp-Wert indirekt über ein Array auf sich selbst verweist.

2.2. Entscheidungsverfahren

Das Paper präsentiert ein Entscheidungsverfahren, das das Erfüllbarkeitsproblem für verschachtelte Datentypen auf die (naive) Kombination von Datentypen, Arrays und uninterpretierten Funktionen (EUF) reduziert. Das Verfahren arbeitet wie folgt:

Signatur-Translation: Eine neue Signatur $\Sigma_{\varphi}$ wird konstruiert.
- Array-Sorten werden in zwei Komponenten aufgeteilt: eine Datentyp-Sort ( $\sigma^*$ ), die zur Zyklusprüfung verwendet wird, und eine Array-Sort ( $\sigma'$ ), die für das Standard-Array-Reasoning verwendet wird.
- Datentyp-Konstruktoren werden kopiert, um auf den neuen Sorten zu operieren.
- Spezielle Konstruktoren werden eingeführt, um Arrays als endliche Tupel darzustellen, welche die durch Indizes in der Eingabeformel aufgerufenen Elemente erfassen.
- Uninterpretierte Funktionen ( $f_A, g_A$ ) werden hinzugefügt, um die Array-Sort-Repräsentationen ( $\sigma'$ ) mit den Datentyp-Sort-Repräsentationen ( $\sigma^*$ ) zu verknüpfen.
Formel-Translation: Die Eingabeformel $\varphi$ wird in $\text{trFormula}(\varphi)$ übersetzt.
- Standard-Literale (z. B. $x = \text{select}(a, i)$ ) werden auf ihre Gegenstücke in der neuen Signatur abgebildet.
- Lemmata: Entscheidend ist, dass die Translation durch eine Menge von Lemmata ( $L(\varphi)$ ) ergänzt wird, die die Korrespondenz zwischen den Array-Operationen in der ursprünglichen Formel und der Tupel-basierten Repräsentation in der neuen Signatur erzwingen. Diese Lemmata stellen sicher, dass die „verborgenen Zyklen“ in der translatierten Formel offengelegt werden.
Lösen: Die resultierende Formel $\text{trFormula}(\varphi)$ wird auf Erfüllbarkeit geprüft, indem bestehende SMT-Solver verwendet werden, die in der Lage sind, die Kombination von Datentypen, Arrays und EUF zu handhaben (z. B. via der Nelson-Oppen-Methode).

2.3. Korrektheit und Entscheidbarkeit

Das Paper beweist, dass die Translation die Erfüllbarkeit bewahrt (Theorem 31), unter der Annahme, dass die Datentyp-Theorie bezüglich der gemeinsamen Sorten stabil unendlich ist. Infolgedessen ist die Theorie der verschachtelten Datentypen entscheidbar (Theorem 32).

3. Hauptbeiträge

Das Paper leistet drei primäre Beiträge:

Theorie-Definition: Die Einführung einer präzisen Theorie der verschachtelten Datentypen, die nicht-standardmäßige zyklische Modelle verhindert, die aus der Interaktion zwischen Datentypen und Arrays entstehen.
Entscheidungsverfahren: Ein Reduktions-basiertes Entscheidungsverfahren, das Probleme verschachtelter Datentypen in Standard-Theoriekombinationen transformiert, die um uninterpretierte Funktionen erweitert sind.
Implementierung und Evaluierung: Eine Prototyp-Implementierung innerhalb des cvc5 SMT-Solvers und eine empirische Evaluierung, die die Effektivität des Ansatzes demonstriert.

4. Experimentelle Ergebnisse

Die Autoren evaluierten ihre Implementierung anhand zweier Benchmark-Suites:

Synthetische Benchmarks: Formeln, die systematisch darauf ausgelegt sind, Zyklen variabler Größe zwischen Datentypen und Arrays zu erzeugen.
- Bei unerfüllbaren Instanzen (Zyklen vorhanden) löste cvc5 alle 500 Benchmarks und übertraf damit Z3 (welches im Durchschnitt 299,8 löste, obwohl die Tabelle angibt, dass Z3 insgesamt weniger Instanzen löste).
- Bei erfüllbaren Instanzen (Zyklen gebrochen) löste cvc5 25 von 50, während Z3 nur 1 löste.
Real-World Benchmarks: Formeln, die vom Move Prover Verifizierungstool abgeleitet wurden, welches verschachtelte Datentypen verwendet, um persistente Datenstrukturen in Smart Contracts zu modellieren.
- Beide Solver lösten alle Move Prover Benchmarks schnell.
- cvc5 war bei erfüllbaren Instanzen vergleichbar mit oder geringfügig schneller als Z3.

5. Bedeutung und Behauptungen

Das Paper behauptet, dass die vorgeschlagene Theorie und das Entscheidungsverfahren das Problem der nicht-standardmäßigen Modelle in der Kombination von Datentypen und Arrays erfolgreich adressieren – ein Problem, das bestehende Solver (wie Z3) zwar implizit handhaben könnten, aber ohne eine präzise theoretische Definition oder garantierte Korrektheit hinsichtlich der Azyklizität.

Die Autoren geben an, dass ihr Ansatz „vielversprechend“ ist und zeigt, dass er bei Real-World-Benchmarks konkurrenzfähig und bei synthetischen Benchmarks, die auf die Detektion von Zyklen getestet wurden, überlegen ist. Sie betonen, dass die Arbeit durch die Bedürfnisse des Move Prover motiviert wurde, wo solche verschachtelten Strukturen häufig vorkommen.

Das Paper schließt bescheiden mit dem Hinweis, dass die aktuelle Arbeit spezifisch den Fall von Arrays löst, das breitere Problem unentdeckter Zyklen jedoch auch für andere Datenstrukturen (Sequenzen, Mengen etc.) existiert. Die Autoren schlagen vor, dass ihre Lösung für Arrays als Basis für eine allgemeinere Lösung naiver Theoriekombinationsprobleme dienen kann. Als zukünftige Arbeit wird die Erweiterung der Unterstützung für inkrementelles Lösen und Quantoren identifiziert.