💻 computer science

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

Dit artikel presenteert een nieuwe, correcte beslissingsprocedure voor de SMT-theorie van extensionele arrays met constante arrays die willekeurige indexdomeinen ondersteunt, waardoor eerdere beperkingen tot eindige of oneindige gevallen worden overwonnen, en toont de effectiviteit daarvan aan door implementatie in de Bitwuzla-oplosser.

Oorspronkelijke auteurs: Mathias Preiner, Aina Niemetz, Clark Barrett

Gepubliceerd 2026-05-20

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Mathias Preiner, Aina Niemetz, Clark Barrett

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een detective bent die probeert een mysterie op te lossen in een enorme, oneindige bibliotheek van boeken (een array). Elk boek heeft een specifiek vaknummer (een index) en bevat een verhaal (een element).

In de wereld van computerverificatie moeten we vaak vragen stellen zoals: "Als ik het verhaal in vak 5 verander, verandert het verhaal in vak 10 dan?" of "Zijn deze twee bibliotheken exact hetzelfde?"

Lange tijd hadden de hulpmiddelen die gebruikt worden om deze vragen te beantwoorden (zogenaamde SMT-oplossers) een groot blinde vlek. Ze waren uitstekend in het hanteren van bibliotheken waarin je individuele boeken kon veranderen, maar ze hadden moeite wanneer de bibliotheek begon met een "standaardverhaal" dat op elke enkele pagina was geschreven, nog voordat je begon.

Het Probleem: Het Dilemma van de "Blanke Pagina"

Stel je een bibliotheek voor waar elk boek begint met hetzelfde standaardverhaal: "Het Einde."

De Oude Manier: Als je de computer wilde vertellen: "Oké, houd 'Het Einde' overal, maar verander vak 5 naar 'Hoofdstuk 1'", dan moest de computer een enorme, geneste lijst uitschrijven: "Verander vak 5, verander dan vak 6, verander dan vak 7..." tot in het oneindige.
Het Resultaat: Dit maakte de computer traag, verward en vatbaar voor fouten. Het was alsof je probeerde een witte muur te beschrijven door elke individuele witte pixel apart op te sommen.

Bovendien konden eerdere hulpmiddelen dit concept van een "standaardverhaal" alleen hanteren als de bibliotheek oneindig was. Als de bibliotheek eindig was (zoals een klein boekenrek met slechts 4 vakken), gaven de oude hulpmiddelen vaak het verkeerde antwoord. Ze konden niet begrijpen dat als je elk vak op een klein rek overschrijft, het "standaardverhaal" niet langer van belang is.

De Oplossing: De "Magische Stempel"

De auteurs van dit artikel, Mathias Preiner, Aina Niemetz en Clark Barrett, bouwden een nieuwe beslissingsprocedure (een nieuwe set regels voor de detective) genaamd CAEXT.

Beschouw hun oplossing als een Magische Stempel.
In plaats van elk boek apart op te sommen, kun je nu zeggen: "Dit hele rek is gestempeld met het verhaal 'Het Einde'."

De Innovatie: Hun nieuwe systeem kan deze "Magische Stempel" hanteren, of het rek nu oneindig is of gewoon een klein, eindig boekenrek.
De Truc: Ze beseften dat voor een eindig rek je alleen hoeft te controleren of je elk vak hebt gestempeld. Als je dat hebt gedaan, is het rek nu gewoon het nieuwe verhaal. Als je dat niet hebt gedaan, geldt het "standaardverhaal" nog steeds voor de lege plekken.

Hoe Het Werkt (Het "Doorgeven van de Baton"-Spel)

Het artikel beschrijft hun methode als een spel van Doorgeven van de Baton.

De Opstelling: Je hebt een rek met een "Magische Stempel" (een constante array) en enkele specifieke wijzigingen (updates).
De Achtervolging: Het systeem probeert het pad van informatie te traceren. Als je vak 1 verandert, heeft die verandering dan invloed op vak 2?
Het Conflict: Soms vindt het systeem een tegenstrijdigheid. Bijvoorbeeld, het ziet dat "Vak 1 is 'Het Einde'" maar ook "Vak 1 is 'Hoofdstuk 1'."
De Oplossing: De nieuwe regels staan het systeem toe om te zeggen: "Wacht, als het rek slechts 4 vakken heeft, en ik heb 4 verschillende vakken veranderd, dan is de 'Magische Stempel' volledig verdwenen. Het rek bestaat nu alleen uit de nieuwe verhalen."

Het artikel bewijst wiskundig dat deze nieuwe set regels sound (geldig) is. Dit betekent:

Refutational Soundness: Als het systeem zegt "Dit is onmogelijk", dan is het 100% correct. Het liegt nooit over een tegenstrijdigheid.
Satisfiability Soundness: Als het systeem zegt "Dit is mogelijk", dan is het 100% correct. Het liegt nooit over het bestaan van een oplossing.

De Wereldse Test

De auteurs schreven niet alleen theorie; ze bouwden een hulpmiddel genaamd Bitwuzla en testten dit tegen andere topdetectivehulpmiddelen (zoals Z3, cvc5 en MathSAT5).

De Resultaten: Hun nieuwe hulpmiddel loste aanzienlijk meer puzzels op dan de anderen.
De "Gotcha": Ze ontdekten dat andere hulpmiddelen, wanneer ze geconfronteerd werden met deze "eindig-rek"-puzzels, vaak verkeerde antwoorden gaven. Ze zouden zeggen dat een puzzel oplosbaar was terwijl dat niet zo was, of andersom. Bitwuzla, met hun nieuwe "Magische Stempel"-logica, kreeg het elke keer goed.
Waar het werd gebruikt: Ze testten dit op echte problemen zoals het controleren van hardwareontwerpen en het verifiëren van slimme contracten (digitale overeenkomsten) op de Ethereum-blockchain.

Samenvatting

In eenvoudige termen introduceert dit artikel een slimmere manier voor computers om te redeneren over datastructuren die beginnen met een standaardwaarde.

Vroeger: Computers waren traag en verward bij het omgaan met "standaardwaarden" op kleine, eindige datasets.
Nu: De nieuwe methode behandelt deze standaarden als een "Magische Stempel" die eenvoudig kan worden gevolgd en overschreven, en werkt perfect voor zowel oneindige als eindige scenario's.
Impact: Dit maakt de computertools die worden gebruikt om veiligheidskritieke software te verifiëren (zoals zelfrijdende auto's of blockchain-contracten) sneller, nauwkeuriger en in staat om problemen op te lossen die voorheen onmogelijk waren.

Technische Samenvatting: Satisfiability Modulo Extensional Constant Arrays

Probleemstelling

Redeneren over array-gegevensstructuren, met name in combinatie met machine-integers, is een fundamentele vereiste voor hardware- en softwareverificatie. De standaard Satisfiability Modulo Theories (SMT)-theorie van extensionele arrays, zoals gedefinieerd in SMT-LIB en geaxiomatiseerd door McCarthy, biedt select (lezen) en store (schrijven) operatoren samen met een extensionaliteitsaxioma. Hoewel dit toereikend is voor veel verificatietaken, mist deze theorie beknoptheid bij het modelleren van arrays die zijn geïnitieerd met een standaardwaarde (bijvoorbeeld nul-geïnitialiseerd geheugen).

In de standaardtheorie moet dergelijke initialisatie worden uitgedrukt via diep geneste store-expressies die de standaardwaarde naar elke relevante index schrijven. Dit leidt tot modelleeronnauwkeurigheden (indices kunnen alleen expliciet worden overschreven) en ernstige inefficiënties in oplossingsprocedures vanwege de diepte van de opslagketens.

Het uitbreiden van de theorie met constante arrays—arrays die op elke index één enkel element opslaan—biedt een beknopte oplossing. Bestaande beslissingsprocedures voor extensionele constante arrays zijn echter beperkt tot oneindige indexdomeinen. Voor eindige indexdomeinen ondersteunen bestaande SMT-oplossers ofwel alleen niet-extensionele fragmenten, of ze leveren in het geval van sommige oplossers onjuiste antwoorden op bij redeneren over extensionaliteit over constante arrays met eindige indices. De kernuitdaging ligt in het bepalen of twee reeksen store-bewerkingen over verschillende constante arrays met eindige domeinen gelijk kunnen worden gemaakt door voldoende indices bij te werken, een probleem dat zich in het oneindige geval niet voordoet.

Methodologie

De auteurs presenteren een nieuwe beslissingsprocedure voor de theorie van extensionele constante arrays ( $T_{\langle A \rangle}$ ) die willekeurige indexdomeinen ondersteunt, inclusief eindige. De procedure is geformaliseerd als een abstract calculus, CAEXT, dat de Lemmas on Demand (LOD)-procedure voor extensionele arrays (DPA), zoals gepresenteerd in eerder werk, generaliseert en uitbreidt.

De Calculus CAEXT

De calculus werkt op configuraties $\langle A, I, \pi \rangle$ , waarbij $A$ een verzameling vlakke literals is, $I$ een interpretatie is in de lege theorie ( $T_E$ ), en $\pi$ een kaart van propagatiestappen is. De procedure vermijdt het introduceren van virtuele lezingen voor alle indices (wat onhaalbaar is voor oneindige domeinen en computationeel duur voor grote eindige domeinen) door standaardwaarden te propageren en bijgewerkte indices bij te houden.

Belangrijke componenten van de calculus zijn:

Basis Calculus (AEXT): Generaliseert de LOD-procedure naar willekeurige index- en elementsorten, waardoor deze wordt ontkoppeld van specifieke theoriecombinaties. Het propagatieleesinformatie op basis van McCarthy's read-over-write axioma's (row-eq, row-ne) en het extensionaliteitsaxioma (ext).
Extensie voor Constante Arrays:
- Propagatie van Standaardwaarden: In plaats van lezingen voor elke index te genereren, propageert de calculus de standaardwaarde $v$ van een constante array $\langle v \rangle$ naar andere arrays. Het onderhoudt een verzameling bijgewerkte indices $I(a, \langle v \rangle)$ , die indices vertegenwoordigen waar de array $a$ verschilt van de standaardwaarde $\langle v \rangle$ langs het propagatiepad.
- Conflictdetectie (CongC): Wanneer twee verschillende standaardwaarden $v$ en $w$ naar dezelfde array $a$ worden gepropageerd, controleert de calculus of de verzameling bijgewerkte indices $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ het volledige indexdomein dekt. Als het domein eindig is en de bijgewerkte indices niet alle mogelijke indices dekken, ontstaat er een conflict tenzij $v \approx w$ .
- DistinctN-codering: Om de gekwantificeerde formule $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (controleren of er een niet-bijgewerkte index bestaat) efficiënt te verwerken, codeert de implementatie dit als een gespecialiseerde distinctN-beperking. Dit controleert of de verzameling bijgewerkte indices ten minste $n$ verschillende waarden bevat, waarbij $n$ de grootte van het indexdomein is.

Implementatie

De beslissingsprocedure is geïmplementeerd in de state-of-the-art SMT-oplosser Bitwuzla. Het integreert naadloos met de bestaande LOD-architectuur van Bitwuzla, waarbij de bit-vector-oplosser de interpretatie $I$ levert. De implementatie bevat optimalisaties zoals trage expansie van distinctN-beperkingen en breedte-zoekopdrachten voor propagatiepaden om het geheugengebruik te minimaliseren.

Belangrijkste Bijdragen

Generalisatie van LOD: De auteurs generaliseren de LOD-procedure voor extensionele arrays met vaste grootte bit-vectors naar willekeurige index- en elementsorten.
Abstracte Calculus AEXT: Ze presenteren AEXT als een ontkoppelde, abstracte calculus voor de extensionele theorie van arrays, onafhankelijk van het LOD-oplossingsparadigma.
Extensie naar Constante Arrays (CAEXT): Ze breiden AEXT uit om extensionele constante arrays te verwerken, en bewijzen refutational soundness (als onvoldoende wordt gemeld, is de invoer onvoldoende) en satisfiability soundness (als een verzadigde configuratie wordt bereikt zonder onvoldoende, is de invoer voldoen).
Implementatie en Evaluatie: De procedure is geïmplementeerd in Bitwuzla en geëvalueerd op diverse benchmarks, waarbij aanzienlijke prestatieverbeteringen worden aangetoond ten opzichte van de baseline Bitwuzla en andere toonaangevende oplossers (Z3, cvc5, MathSAT5).

Resultaten

De evaluatie is uitgevoerd op vijf benchmarksets: smtlib (gekwantificeerde logica), mbqi (subqueries van modelgebaseerde kwantificatorinstantiatie), k-ind (incrementele hardwaremodelcontrole), hevm (Ethereum Virtual Machine) en crafted (synthetische benchmarks die specifiek zijn ontworpen om extensionaliteit van eindige constante arrays te testen).

Prestaties: Bitwuzla met de nieuwe procedure (Bitwuzla⟨A⟩) presteerde aanzienlijk beter dan alle andere oplossers. Op de smtlib-set nam het aantal opgeloste benchmarks toe met een factor 5 ten opzichte van de baseline Bitwuzla (3.545 versus 717). Op de mbqi-set loste Bitwuzla⟨A⟩ alle 4.147 queries op, terwijl de baseline slechts 4 oploste.
Juistheid: Op de crafted⟨A⟩-set, die gelijkheden encodeert over eindige constante arrays met verschillende standaardwaarden, was Bitwuzla⟨A⟩ de enige oplossing die voor alle instanties correcte antwoorden gaf. Z3 en MathSAT5 accepteerden de invoer maar rapporteerden voor een significant aantal benchmarks verkeerde antwoorden. cvc5 en de baseline Bitwuzla verwierpen de invoer volledig vanwege gebrek aan ondersteuning.
Soundness-verificatie: De auteurs verifieerden de modellen die door de oplossers op de crafted⟨A⟩-set werden geproduceerd. Alleen Bitwuzla⟨A⟩ produceerde modellen die consistent waren met zijn eigen claims over vervulling. Z3 en MathSAT5 produceerden modellen die, wanneer ze terug werden geasserteerd naar de oorspronkelijke formules, leidden tot tegenstrijdigheden.

Betekenis

Het artikel beweert dat de voorgestelde beslissingsprocedure de oplossingsmogelijkheden van Bitwuzla aanzienlijk uitbreidt, waardoor het problemen kan aanpakken die extensionele constante arrays met eindige indexdomeinen betreffen en die eerder onoplosbaar waren of onjuist werden behandeld door andere tools.

Het werk adresseert een kritieke kloof in SMT-oplossing: hoewel constante arrays een standaard modelleerpatroon zijn voor geheugeninitialisatie, ontbreekt het bestaande oplossers ofwel aan ondersteuning voor deze in eindige domeinen, of ze leveren onjuiste resultaten. Door een sound en complete beslissingsprocedure te bieden voor de volledige theorie van extensionele constante arrays (zowel eindig als oneindig), maakt dit werk nauwkeurigere en efficiëntere verificatie mogelijk in toepassingen zoals hardwaremodelcontrole en smart contract-verificatie (specifiek voor de Ethereum Virtual Machine). De auteurs merken op dat hoewel hun evaluatie zich richtte op eindige domeinen, de procedure agnostisch is ten opzichte van de onderliggende oplosserarchitectuur en volledig het oneindige domein geval eveneens ondersteunt.