Anatomie van een Lean-bewijs voor software engineers

Introductie

Omdat dit sterk lijkt op programmaverificatie, leek het me interessant om te kijken wat er nodig is om dit bewijs te formaliseren. Lean is hiervoor een goede keuze, omdat de bijbehorende bibliotheek, Mathlib, alle benodigde stellingen bevat. Na het voltooien van het formele bewijs besloot ik dit uit te schrijven, omdat ik denk dat het software engineers goed inzicht geeft in wat er nodig is om eigenschappen van een systeem formeel te bewijzen.

Ik heb geprobeerd dit artikel toegankelijk te maken. Als je bekend bent met een moderne statisch getypeerde programmeertaal (zoals TypeScript of Rust), binaire rekenkunde, basis propositielogica en inductieve bewijzen, zou je dit moeten kunnen volgen.

Achtergrond: DFA's en reguliere talen

Je kunt deze sectie overslaan als je al bekend bent met DFA's en reguliere talen.

Eindige automaten bieden een theoretisch computatiemodel met een vast geheugen. Naast de theorie hebben eindige automaten belangrijke praktische toepassingen; ze zijn bijvoorbeeld relevant voor parsers en reguliere expressies (regex), waar een bug ooit een aanzienlijk deel van het internet platlegde.

Deterministische Eindige Automaat (DFA)

Een deterministische eindige automaat (DFA) is een machine met een vaste, eindige set toestanden die zijn input één symbool per keer leest, van links naar rechts. Bij elk symbool werkt de machine zijn toestand bij met behulp van een deterministische transitiefunctie. Na het laatste symbool bevindt de machine zich ofwel in een accepterende toestand (de input wordt geaccepteerd) of niet (de input wordt geweigerd).

Als je ooit een eenvoudige reguliere expressie hebt geschreven zoals -?[0-9]+, dan heb je een DFA geconstrueerd. Deze regex matcht integer-literalen zoals 12 en -123. De bijbehorende DFA ziet er als volgt uit:

Toestanden van de DFA voor een decimaal integer-literal:

  • Start: Hier beginnen we voordat het eerste teken wordt verwerkt. Aangezien de starttoestand niet accepterend is, wordt een lege string geweigerd.
  • Sign (Teken): We gaan naar deze toestand bij een - teken. We kunnen deze toestand overslaan en direct naar 'digits' gaan, omdat het tekentoestandsoptioneel is (-?). Als we hier eindigen, wordt de string geweigerd.
  • Digits (Cijfers): We gaan van 'start' of 'sign' naar 'digits' bij een cijfer ([0-9]). In deze toestand blijven we zolang we cijfers tegenkomen. Dit is de enige accepterende toestand.
  • Dead (Dood): We komen hier terecht bij elk ander teken. Dit is een 'sink state': zodra we hier zijn, blijven we hier, en de string wordt geweigerd.

De set van input-symbolen voor de machine wordt gedefinieerd door de set $\Sigma$. In ons regex-voorbeeld is $\Sigma = \{-, 0, 1, 2, \ldots, 9\}$.

Reguliere talen

Een taal is simpelweg een set strings (ook wel woorden genoemd). Een taal wordt regulier genoemd als er een DFA is die precies de strings in die set accepteert.

Het herkennen van reguliere talen is de klasse van beslissingsproblemen die oplosbaar zijn met een hoeveelheid geheugen die niet meegroeit met de input. Reguliere talen hebben nuttige sluitingseigenschappen: de unie en intersectie van twee reguliere talen zijn regulier, en dat geldt ook voor het complement en (belangrijk voor ons) de omkering (reversal) van een reguliere taal.

De standaardmanier om te bewijzen dat een taal regulier is, is door een DFA te bouwen en aan te tonen dat deze precies die taal accepteert. We kunnen een taal $A$ beschrijven met set-builder notatie: $A = \{ w \in \Sigma^* \mid P(w) \}$

Hierbij is $\Sigma^*$ de set van alle mogelijke concatenaties van symbolen in $\Sigma$, en $P(w)$ is de voorwaarde waaraan een string $w$ moet voldoen om tot de taal te behoren.

Het probleem

Het probleem dat we gaan oplossen is afkomstig uit Introduction to the Theory of Computation (3e ed.) door Michael Sipser:

1.32 Laat $\Sigma_3 = \left\{ \begin{bmatrix}0\\0\\0\end{bmatrix}, \begin{bmatrix}0\\0\\1\end{bmatrix}, \begin{bmatrix}0\\1\\0\end{bmatrix}, \ldots, \begin{bmatrix}1\\1\\1\end{bmatrix} \right\}$.
$\Sigma3$ is de set van alle kolommen van 0'en en 1'en met een hoogte van 3. Een string over $\Sigma3$ bepaalt dus drie rijen bits. Definieer, door elke rij als een binair getal te lezen:
$B = \{ w \in \Sigma_3^* \mid P(w) \}$
waarbij $P(w)$ de propositie is dat de onderste rij van $w$ gelijk is aan de som van de bovenste twee rijen.
Bewijs dat $B$ regulier is. (Hint: het is makkelijker om te werken met $B^{\mathcal{R}}$.)

Het probleem definieert een ongebruikelijk alfabet. In plaats van gewone tekens bestaat het alfabet uit kolommen van drie bits. De regel om te bepalen of een string in de taal zit, is om de eerste twee rijen op te tellen en te controleren of ze overeenkomen met de derde.

Bijvoorbeeld, de volgende string zit in de taal:

011 # x rij: eerste addend is 3 in decimaal
001 # y rij: tweede addend is 1 in decimaal
100 # z rij: som is 4, wat gelijk is aan 3 + 1

Maar deze string niet:

01 # x rij: eerste addend is 1 in decimaal
00 # y rij: tweede addend is 0
11 # z rij: som is 3, wat niet gelijk is aan 1 + 0

De uitdaging is dat we dit moeten doen met een vaste hoeveelheid geheugen voor willekeurig lange strings.

De oplossing

De truc is om te onthouden hoe je getallen met de hand optelt: je werkt van het minst significante cijfer naar het meest significante. Het enige dat je van de ene kolom naar de volgende meeneemt, is de carry (overdracht).

Een DFA leest echter van links naar rechts, en het probleem presenteert de getallen met het meest significante bit eerst. Daarom herkennen we $B$ niet direct. In plaats daarvan bouwen we een DFA om de omkering $B^{\mathcal{R}}$ te herkennen. Deze bestaat uit de strings van $B$ in omgekeerde volgorde, zodat de machine het minst significante kolom eerst ziet.

Als we een DFA kunnen bouwen die $B^{\mathcal{R}}$ herkent, kunnen we concluderen dat $B^{\mathcal{R}}$ een reguliere taal is. Omdat de omkering van $B^{\mathcal{R}}$ weer $B$ is, kunnen we de sluitingseigenschap van de omkering van reguliere talen gebruiken om te concluderen dat $B$ eveneens regulier is.

Adder-rekenkunde

Bij het kolom-voor-kolom optellen berekenen we de som-bit bij elke stap met de adder-vergelijking: $xi \oplus yi \oplus c{\mathrm{in}} = zi$

Waarbij $xi, yi$ de addend-bits zijn, $zi$ de som-bit is, $i$ de index van de huidige kolom is, en $c{\mathrm{in}}$ de input carry van de vorige stap is. De output carry ($c{\mathrm{out}}$) voor de volgende stap berekenen we als volgt: $c{\mathrm{out}} = (xi \wedge yi) \vee (c{\mathrm{in}} \wedge (xi \oplus y_i))$

Dit betekent dat er een carry is als ofwel beide addenden 1 zijn, of als er een input carry was en precies één van de addenden 1 is. Een simpelere manier om $c{\mathrm{out}}$ te berekenen is door te controleren of ten minste twee van $xi, yi$ en $c{\mathrm{in}}$ gelijk zijn aan 1.

De Adder-DFA

Hier is de DFA die $B^{\mathcal{R}}$ herkent. De DFA heeft drie toestanden:

  • Carry 0: We zijn in deze toestand als de carry 0 is voor de volgende kolom. Dit is zowel de start- als de accepterende toestand, aangezien een resterende carry aan het eind zou betekenen dat de som de onderste rij is overgestegen (overflow).
  • Carry 1: We zijn in deze toestand als de carry 1 is. Deze toestand is niet-accepterend. We kunnen deze toestand echter verlaten als een $\begin{smallmatrix}\mathtt{0}\\\mathtt{0}\\\mathtt{1}\end{smallmatrix}$ kolom de carry absorbeert en ons terugbrengt naar 'Carry 0'.
  • Dead: We komen hier terecht als de som niet overeenkomt. Dit is een sink state.

Voorbeelden

Voorbeeld 1 (Geaccepteerd): Input: $x=3, y=1, z=4$. De DFA leest de kolommen achterstevoren. De run verloopt als volgt: Carry 0 $\xrightarrow{(1,1,0)}$ Carry 1 $\xrightarrow{(1,0,0)}$ Carry 1 $\xrightarrow{(0,0,1)}$ Carry 0. De run eindigt in Carry 0 (accepterend), dus de string is in $B^{\mathcal{R}}$, en dus is het origineel in $B$.

Voorbeeld 2 (Geweigerd): Input: $x=1, y=0, z=3$. De run verloopt als volgt: Carry 0 $\xrightarrow{(1,0,1)}$ Carry 0 $\xrightarrow{(0,0,1)}$ Dead. De tweede kolom faalt: bij geen carry moet $0+0$ een $0$ produceren, maar de onderste rij claimt een $1$. De run eindigt in de dead state en wordt geweigerd.

Het Lean-bewijs

Ons doel is om aan te tonen dat de taal $B$ regulier is. Het Lean-bewijs bestaat uit drie delen:

  1. Een specificatie van de taal $B$.
  2. Een uitvoerbare implementatie van de Adder-DFA.
  3. Een bewijs dat de implementatie overeenkomt met de specificatie.

De specificatie

Het alfabet bestaat uit kolommen van drie bits. In Lean representeren we dit als een tuple van drie booleans: abbrev Sigma3 := Bool × Bool × Bool

Vervolgens definiëren we $B$ met behulp van Mathlib.Computability.Language: def B : Language Sigma3 := { wBE | row3BE wBE = row1BE wBE + row2BE wBE }

Hierbij is rowNBE een functie die de $n$-de rij selecteert en deze interpreteert als een natuurlijk getal (big-endian). De predicate is simpelweg $z = x + y$.

In Lean is Language in feite een Set, en een Set is een functie die test of een element in de set zit. De return-type is Prop (een propositie), niet Bool. In Lean is een propositie zelf een type, en de waarden ervan zijn bewijzen van die propositie. Een lidmaatschapstest is dus in feite een type-check, geen berekening tijdens runtime.

De implementatie

We definiëren de toestanden van de DFA als een sum-type:

inductive DFAState where
| carry (c : Bool)
| dead
deriving DecidableEq, Fintype

Fintype is essentieel; het bewijst dat het type een eindig aantal waarden heeft, wat nodig is om te claimen dat de taal regulier is.

De transitiefunctie wordt als volgt gedefinieerd:

def dfaStep : DFAState → Sigma3 → DFAState
| .dead, _ => .dead
| .carry c, (x, y, z) =>
  if z = (x ^^ y ^^ c) then  -- ^^ is XOR
    .carry (Bool.atLeastTwo x y c)
  else
    .dead

Ten slotte gebruiken we de DFA structuur uit Mathlib om de start- en acceptietoestanden vast te leggen:

def adderDFA : DFA Sigma3 DFAState where
  step := dfaStep
  start := .carry false
  accept := {.carry false}

Hoe bewijzen werken

In Lean schakelt het keyword by over naar de tactic mode. Een tactic zoals decide bewijst een propositie door de beslissingsprocedure ervan uit te voeren binnen de type-checker.

Een bewijs in Lean is in feite een term waarvan het type de propositie is. Een propositie is "waar" als het type minstens één waarde (een bewijs) heeft. Een onware propositie is als een lege enum: er is simpelweg geen waarde die je kunt construeren om het te bewijzen.

Het bewijs

Om te bewijzen dat $B$ regulier is, moeten we aantonen dat adderDFA.accepts = B.reverse.

Run-invariant

Omdat de DFA willekeurig lange strings kan verwerken, gebruiken we inductie. We hebben een inductiehypothese nodig die voor elke stap geldt. We stellen de volgende equivalentie op: Het uitvoeren van de adder-DFA over een (little-endian) woord $w$ beginnend met carry $c{\mathrm{in}}$ eindigt in toestand $c{\mathrm{out}}$ dan en slechts dan als: $\mathrm{row}1(w) + \mathrm{row}2(w) + c{\mathrm{in}} = \mathrm{row}3(w) + c_{\mathrm{out}} \cdot 2^{|w|}$

Bewijs van de run-invariant

Het bewijs gebeurt via inductie op het woord $wLE$.

Base case (leeg woord): De DFA blijft in de starttoestand (.carry carryIn = .carry carryOut). De rekenkundige zijde wordt 0 + 0 + carryIn = 0 + carryOut * 2^0. Beide zijden vereisen simpelweg dat carryIn = carryOut.

Inductieve stap: We moeten bewijzen dat als de invariant geldt voor een lijst, deze ook geldt voor die lijst met één extra element ervoor. We volgen vier stappen:

  1. De run splitsen: We splitsen de run in de eerste stap (één kolom) en de rest van de run.
  2. De eerste stap telt op: We vertalen de eerste DFA-stap naar de rekenkundige adder-vergelijking: $x + y + c{\mathrm{in}} = z + 2 \cdot c{\mathrm{mid}}$.
  3. De rest van de run: We gebruiken de inductiehypothese om de rest van de run te vertalen naar rekenkunde.
  4. Splitsing van het minst significante bit: We tonen aan dat de som van het hele woord gelijk is aan de som van het eerste bit plus de som van de rest.

$B^{\mathcal{R}}$ is regulier

Nu we de runinvariant hebben bewezen, kunnen we aantonen dat adderDFA.accepts = B.reverse. Beide zijn sets; we bewijzen dat ze dezelfde leden hebben. De lidmaatschapsregel voor de DFA is dat de run eindigt in de accepterende toestand (carry false), en voor $B^{\mathcal{R}}$ is dat de rekenkundige som zonder carry-over. Dit volgt direct uit onze runinvariant met beide carries op false.

Omdat er een DFA is die $B^{\mathcal{R}}$ accepteert, is $B^{\mathcal{R}}$ regulier.

$B$ is regulier

Als laatste stap gebruiken we de sluitingseigenschap uit Mathlib: een taal is regulier dan en slechts dan als zijn omkering regulier is (L.reverse.IsRegular ↔ L.IsRegular). Aangezien we hebben bewezen dat $B^{\mathcal{R}}$ regulier is, volgt daaruit dat $B$ regulier is.

Slotbeschouwingen

We hebben aangetoond dat de taal $B$ regulier is met een bewijs dat door Lean wordt geaccepteerd. Naast het bewijs hebben we een formeel geverifieerde implementatie van een DFA gecreëerd.

Formele bewijzen vereisen veel meer detail dan we normaal gesproken zouden opschrijven. In de echte wereld zijn systemen veel complexer; gedistribueerde systemen vereisen bijvoorbeeld temporele logica.

Tegenwoordig kunnen AI-agenten eenvoudige bewijzen als deze in één keer genereren. Hoewel het verleidelijk is om machine-gegenereerde bewijzen als black-boxes te behandelen, is het cruciaal dat we ze kunnen begrijpen. Een voorbeeld hiervan is onze run-invariant, die een carry-out term introduceerde die in de oorspronkelijke definitie van $B$ niet werd genoemd. Dit was geen bug, maar het legde een verborgen vereiste bloot: alle drie de rijen moeten dezelfde lengte hebben, zodat $B$ sommen uitsluit die zouden overflowen.

De toekomst van software engineering is spannend; formele methoden stellen ons in staat om op een hoger abstractieniveau te werken en maken ons productiever door meer automatisering mogelijk te maken.

***

Voetnoten:

  1. Om verwarring tussen interpretaties van bit-lijsten te voorkomen, had men aparte types voor little- en big-endian kunnen introduceren, maar dit zou veel bestaande stellingen opnieuw vereisen.
  2. Set is in Lean een functie die test of een element in de set zit.
  3. Een beslissingsprocedure is een functie die een propositie evalueert en true of false teruggeeft.
  4. De evaluatie in de type-checker is gegarandeerd terminerend, omdat Lean functies weigert tenzij terminatie is bewezen.
  5. De werkelijke term is ofdecideeq_true (id (Eq.refl true)).
  6. Vereenvoudigde versie van de definitie in Mathlib.
  7. De definitie in Mathlib is uitgebreider; hier is een verkorte versie gebruikt.
  8. De informele argumentatie over de equivalentie van de little-endian interpretatie en de big-endian interpretatie van de omkering is geformaliseerd in het specificatiebestand.
  9. .toNat is weggelaten voor de leesbaarheid.
  10. .toNat is weggelaten voor de leesbaarheid.
  11. Projecten zoals Aeneas vertalen Rust-programma's naar Lean voor verificatie.
  12. Bijvoorbeeld: game-based of simulation-based bewijzen zijn moeilijk te formaliseren.
  13. Zie de blogposts van Leonardo de Moura over Proof Assistants in the Age of AI.