Verifikation von Algorithmen mit Z3 – Teil 3

Im ersten Artikel dieser Reihe hatten wir den SMT-Solver Z3 kennen gelernt und uns allgemeine Gedanken zu Spezifikation und Verifikation gemacht. Im zweiten Artikel haben wir den sog. Bresenham-Algorithmus – eine Berechnungsvorschrift zum Zeichnen von geraden Linien – mit Z3 implementiert und dann auch sichergestellt, dass dieser Algorithmus genau das tut, was wir von ihm erwarten. Die Implementierung des Bresenham-Algorithmus in Z3 ist zwar lauffähige Software, allerdings ist Z3 (bzw. SMT-LIB2) keine Allzweckprogrammiersprache, d.h. wir werden kein umfängliches Softwareprojekt komplett in Z3 schreiben können. War also alles letztlich doch für die Katz?

Natürlich nicht. Wir wissen jetzt, dass der Algorithmus grundsätzlich funktioniert und wir könnten nun die komplexe Berechnunngsvorschrift, die maßgeblich in der Funktion step-4 zum Ausdruck kam, von Hand in eine Allzweckprogrammiersprache wie Haskell überführen. Wenn diese manuelle Übersetzung ohne Fehler ist, dann ist auch das resultierende Haskell-Programm korrekt. Durch externe Maßnahmen wie Code Reviews, Pair-Programming oder die Sicherstellung von ausreichendem Schlaf für die beteiligten Entwickler lassen sich die Fehlerraten bei solchen Aufgaben im Zaum halten. Aber was sollen wir tun, wenn wir nachts statt zu schlafen lieber mit Freunden in einer Bar Darts spielen oder Tischkickern wollen? Glücklicherweise gibt es im Werkzeugkasten der Formalen Methoden auch mindestens ein Werkzeug, das mit diesem Lifestyle kompatibel ist: Mit Liquid Haskell können wir ganz normale Haskell-Programme schreiben und diese Programme mit Annotationen anreichern, sodass der Code automatisch verifiziert werden kann. Das kriegt man auch nach einer durchzechten Nacht hin. Also spitzt die Dart-Pfeile und ölt den Tischkicker – in diesem Artikel wollen wir unseren Bresenham-Algorithmus mit Liquid Haskell formulieren.

This integer is too small

Liquid Haskell bietet ein sog. Refinement Type System. Das Liquid-Haskell-Tutorial erklärt Refinement Types so:

Refinement types allow us to enrich Haskell’s type system with predicates that precisely describe the sets of valid inputs and outputs of functions, values held inside containers, and so on. These predicates are drawn from special logics for which there are fast decision procedures called SMT solvers.

Bei Refinement Types ist der Startpunkt immer ein wohl-typisiertes Programm der zugrundeliegenden Programmiersprache. Darauf aufbauend kann man dann die Typen der Werte und Funktionen veredeln, d.h. mit Prädikaten – Ausdrücken vom Typ Bool – weiter einschränken. Einen Index in eine endliche Liste kann man in herkömmlichen Haskell-Code z.B. zunächst als Int typisieren:

type Idx = Int
i :: Idx
i = 1

Werte des Typs Idx kann man als Argument für den !!-Operator verwenden, um aus einer gegebenen Liste den entsprechenden Wert zu holen:

x = [9, 7, 5] !! i
-- Ergebnis: 7

Leider kann ein solcher Idx auch negativ sein, was keinen Sinn macht und bei Listenzugriffen zum Programmabsturz führt:

j :: Idx
j = -4
y = [9, 7, 5] !! j
-- Ergebnis: Programm stürzt ab

Mit Liquid Haskell können wir den Typ Idx veredeln und ausschließen, dass negative Werte verwendet werden können. Dazu schreiben wir über die Zeile type Idx = Int noch einen speziellen Kommentar:

{-@ type Idx = {v : Int | v >= 0} @-}
type Idx = Int
i :: Idx
i = 1

Der Teil hinter der Pipe | ist das Prädikat. Die Formulierungen dieser Prädikate beziehen sich implizit auf eine Umgebung in der die freien Variablen gebunden sind. Hier wird der Name v vor der Pipe gebunden und steht dann hinter der Pipe zur Verwendung bereit.

Mit dieser Einschränkung erlaubt Liquid Haskell für Idx dann nur solche Int-Werte, die auch größer oder gleich 0 sind. Unser Code ist dabei weiterhin ganz normaler Haskell-Code. GHC selbst interessiert sich noch nicht für unsere speziellen Kommentare {-@ ... @-}. Folgendes ist ein valides Haskell-Programm und so lange wir Liquid-Haskell nicht anschalten, wird das einfach ganz gewöhnlich kompiliert:

j :: Idx
j = -4

Sobald wir Liquid-Haskell anschalten …

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

… bekommen wir vom entsprechendem GHC-Plugin einen „Liquid Type Mismatch“:

**** LIQUID: UNSAFE ************************************************************
src/Bresenham.hs:16:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == (-(4 : int))}
    .
    is not a subtype of the required type
      VV : {VV##590 : GHC.Types.Int | VV##590 >= 0}
    .
    Constraint id 1
   |
16 | j = -4
   | ^^^^^^

Hier erhalten wir einen ersten Einblick in die Funktionsweise von Liquid Haskell. Den in der Fehlermeldung genannten, geforderten Typ für j („required type“) haben wir im Code selbst bestimmt, indem wir gesagt haben, dass j vom Typ Idx und Idx der veredelte Typ {v : Int | v >= 0} sein soll. Liquid Haskell hat sich die Freiheit genommen, unser schönes v in ein VV##590 umzubenennen, aber ansonsten steht dort in der Fehlermeldung genau das, was wir persönlich in den Code geschrieben haben. Für Werte, an die wir selbst keine Typen geklebt haben, macht Liquid Haskell Typinferenz, indem es Constraints aufsammelt. Im Fall des Literals -4 hat Liquid Haskell den Typ {v : GHC.Types.Int | v == (-(4 : int))} inferiert, also der Typ aller Ganzzahlen, die genau -4 sind. Liquid Haskell ist genau dann mit unserem Code zufrieden, wenn die inferierten, verwendeten Typen zu den geforderten Typen passen und das bedeutet in diesem Typsystem, dass die verwendeten Typen Subtypen der geforderten Typen sind. Da ein Liquid Type im Wesentlichen eine Menge von Werten ist, ist die Subtyp-Relation einfach eine Teilmengen-Relation. Wir fragen uns also konkret: Ist die Menge der Ganzzahlen, die durch {v : GHC.Types.Int | v == (-(4 : int))} beschrieben ist, eine Teilmenge der Ganzzahlen, die durch {VV##590 : GHC.Types.Int | VV##590 >= 0} beschrieben ist?

Diese Teilmengen-Frage beantwortet das Liquid-Haskell-Plugin nicht direkt selbst, sondern es bastelt sich daraus ein SMT-Programm und fragt dann bei Z3 nach. In unserem Beispiel könnte dieses SMT-Programm in erster Näherung so aussehen:

(declare-const v Int)

(assert (not
         (=> (= v (- 4))
             (>= v 0))))

Dieses Programm prüft – wie im ersten Artikel ausgeführt – die Allgemeingültigkeit der Implikation (=> (= v (- 4)) (>= v 0)) dadurch, dass die Aussage verneint wird und dann auf Erfüllbarkeit geprüft wird. Wenn das Programm erfüllbar ist, dann ist die Implikation nicht allgemeingültig. Und das Programm ist natürlich erfüllbar, denn wenn wir v gleich -4 setzen, dann ist die Bedingung der Implikation wahr, die Folgerung (>= v 0) jedoch falsch und damit ist die Implikation falsch und damit wiederum ist die Verneinung der Implikation wahr. Dieses Ergebnis meldet Z3 an Liquid-Haskell zurück und dieses schreibt uns dann die obige Fehlermeldung ins Terminal.

Durch die zusätzliche Annotation für Idx können wir also statisch ausschließen, dass Werte dieses Typs negativ sein können.

This integer is too big

Doch leider kann ein solcher Idx immer noch eine Zahl sein, die zu groß für die Liste ist, auf die wir zugreifen wollen. Auch das hat einen Programmabsturz zur Folge:

j :: Idx
j = 5
y = [9, 7, 5] !! j
-- Ergebnis: Programm stürzt schon wieder ab

Wir hätten für die Listenindizes gern einen Typ, der für eine gegebene Liste nur genau die Werte beschreibt, die gültige Indizes sind. Die obere Grenze für die gültigen Indizes hängt ab von der Länge der Liste, auf die wir zugreifen möchten: Für eine Liste der Länge n sind die gültigen Indizes genau die Ganzzahlen von 0 bis n - 1. Falls die Liste leer ist, ist auch die Menge der gültigen Indizes leer.

This integer is just right

Wenn ein Typ von einem Wert abhängt, dann handelt es sich um einen sog. abhängigen Typ („dependent type“).¹ Die Menge der gültigen Indizes hängt ab von der Liste selbst (und nicht vom Typ [Int]). Solche abhängigen Typen kann man in Haskell so direkt nicht ausdrücken. Mit Liquid Haskell geht‘s aber:

{-@ type Idx xs = {i:Int | 0 <= i && i < len xs} @-}

Typ-Aliase mit type gibt‘s auch in herkömmlichem Haskell und in Liquid-Haskell kann man solche Aliase zusätzlich mit Parametern ausstatten. Idx wirkt dann wie ein Macro, d.h. immer, wenn wir irgendwo Idx ... hinschreiben, wird die Stelle syntaktisch durch {i:Int | 0 <= i && i < len ...} ersetzt. Der resultierende Typ ist dann abhängig von dem Wert, den wir für ... eingesetzt haben.

Mithilfe dieses vollendet veredelten Spitzentyps können wir versuchen, eine Variante des Listenzugriffsoperators !! zu definieren, der bereits zur Compilezeit und nicht erst zur Laufzeit fehlschlägt, falls wir mit ihm unlautere Dinge anstellen.

{-@ at :: xs:[a] -> Idx xs -> a @-}
at :: [a] -> Int -> a
at (x:_)  0 = x
at (_:xs) i = at xs (i - 1)
at []     _ = error "impossible"

Dieser Code geht sowohl durch den normalen Haskell-Typchecker als auch durch den Liquid-Haskell-Typchecker. Wir sollten trotzdem skeptisch bleiben, ob denn der Laufzeitfehler wirklich nicht mehr auftreten kann; immerhin steht dort doch noch die Erzeugung der Laufzeitausnahme mit error "impossible". Wer ausgeschlafen ist, kann konzentriert auf den Code schauen und sich davon überzeugen, dass dieser Codepfad tatsächlich impossible zu erreichen ist: Idx xs ist in diesem Fall gleich Idx [] und das ist äquivalent zum Refinement Type {i:Int | 0 <= i && i < 0}. Dieser Typ beschreibt die leere Menge, denn die Bedingung gilt für keine einzige Ganzzahl. Wir bekommen in diesem Fall also einen Wert, der Teil einer leeren Menge ist, übergeben – ein Widerspruch, den wir produktiv machen können.

Liquid Haskell erlaubt uns nicht nur die Veredelung unseres eigenen Codes; auch bestehende Typen und Funktionen bspw. aus Prelude wurden bereits mit Refinements angereichert. So hat auch die Funktion error einen veredelten Typ bekommen, der dazu führt, dass error nur an unerreichbaren Code-Stellen verwendet werden kann. Das kriegen wir spätestens dann zu spüren, wenn wir versuchen, error an eine Stelle zu schreiben, die eben doch erreichbar ist:

produziereLaufzeitfehler :: String -> a
produziereLaufzeitfehler = error "ups"

Die Fehlermeldung sagt:

   |
63 | produziereLaufzeitfehler = error "ups"
   |                                  ^^^^^

Liquid Type Mismatch
.
The inferred type
  VV : {v : [GHC.Types.Char] | v == ?t
                               && GHC.Types_LHAssumptions.len v == strLen "ups"
                               && GHC.Types_LHAssumptions.len v >= 0
                               && v ~~ "ups"}
.
is not a subtype of the required type
  VV : {VV##3792 : [GHC.Types.Char] | false}
.

Die veredelte Version von error braucht nicht einfach nur einen String als Argument, sondern einen String, den es gar nicht geben kann. Der verlangte Typ {VV##3792 : [GHC.Types.Char] | false} beschreibt alle Strings (Listen von Char), die das Prädikat false erfüllen. Wo kriegen wir einen solchen widersprüchlichen String her?

Tatsächlich geht in die Voraussetzung der Implikation, die die Subtyprelation prüft auch implizit ein sog. Environment ein. In widersprüchlichen Situationen enthält das Environment diese Widersprüche und damit können wir – ex falso quodlibet – alles mögliche folgern. Da wir uns oben im vierten Fall der Definition von at in einer Umgebung befinden, die genau einen solchen Widerspruch enthält und zwar in der Form von Idx [], können wir solche widersprüchlichen Strings ganz easy übergeben. error kann in Liquid Haskell also wirklich nur an Stellen auftauchen, die beweisbar unerreichbar sind.

Doch das Measure sieht man nicht

In der Definition von Idx haben wir das Prädikat 0 <= i && i < len xs aufgeschrieben. Das sieht zwar syntaktisch aus wie Haskell, ist aber eine eigene Logiksprache. Operatoren wie <= oder && funktionieren, wie man das erwarten würde. Augenscheinlich rufen wir in diesem Prädikat mit len xs auch eine Funktion auf. len ist ein sog. Measure. Measures können wir auch selbst definieren. Um die Verwirrung zu vollenden, definiert man Measures als Haskell-Funktion, allerdings müssen diese Funktionsdefinitionen einem sehr engen Korsett entsprechen.

A measure is a total Haskell function,

1. With a single equation per data constructor, and
2. Guaranteed to terminate, typically via structural recursion.

Das Measure len könnte man so aufschreiben:

{-@ measure len @-}
len :: [a] -> Int
len [] = 0
len (x:xs) = 1 + (len xs)

Bresenham

Bevor wir unser Z3-Programm in Liquid Haskell übersetzen, müssen wir uns noch um eine kleine Formalität kümmern. Aus Gründen, die sich mir noch nicht erschlossen haben, kann Liquid Haskell nicht mit Division umgehen. Folgendes Programm beschreibt ein Theorem, das eigentlich eine Trivialität ausdrückt, nämlich, dass wir eine beliebige reelle Zahl² durch 3 teilen und danach wieder mit 3 multiplizieren können und heraus kommt dieselbe Zahl:

{-@ foo :: x:Double -> {v:() | x == (x / 3) * 3 } @-}
foo :: Double -> ()
foo x = ()

Für z3 wäre dieses Theorem kein Problem; Liquid Haskell gibt allerdings direkt auf. Eine Division tritt in unserer Bresenham-Formulierung auf, wenn wir über die ideale Geradesteigung m = dy/dx sprechen. Wir können fürs Liquid Haskell diese Geradensteigung m einfach zusätzlich zu dy und dx in unseren Algorithmenzustand aufnehmen und dann einen weiteren Constraint hinzufügen, der den Zusammenhang als Multiplikation ausdrückt: m * dx == dy. Damit kommt Liquid Haskell besser klar.

Jetzt können wir die finale Formulierung des Bresenham-Algorithmus aus dem vorhergehenden Artikel von SMT-LIB2 in Liquid Haskell übersetzen. Wir beginnen mit einem Datentyp für den Zustand des Algorithmus.

{-@
data State = State {
  state_m :: Double,
  state_dx :: {dx':Int | 0 < dx'},
  state_dy :: {dy':Int | 0 <= dy' && dy' <= state_dx && state_m * state_dx == dy'},
  state_x :: {x':Int | x' >= 0},
  state_y :: Int,
  state_d :: Int,
}
@-}
data State = State {
  state_m :: Double,
  state_dx :: Int,
  state_dy :: Int,
  state_x :: Int,
  state_y :: Int,
  state_d :: Int
  }

In der Liquid-Haskell-Version dieses Datentyps haben wir bereits manche der Constraints aus state-4-valid abgeräumt: Die Steigung m muss kleiner 1 sein, dx größer 0 und x läuft nur nach rechts.

Den Zusammenhang von d, dy, dx, x und y können wir als Measure ausdrücken:

{-@ measure state_d_correct @-}
state_d_correct :: State -> Bool
state_d_correct (State _ dx dy x y d) = d == 2 * dy * (x + 1) - (2 * y * dx) - dx

Dann fehlt noch das Korrektheitskriterium für y. Die Ganzzahl y soll die gerundete Version des y-Achsenabschnitts der Ideallinie sein. In z3 hatten wir das mit Rekurs auf eine Rundungsfunktion formuliert:

(= y (round-to-nearest (* m (to_real x))))

Dieses round-to-nearest haben wir in Liquid Haskell nicht zur Verfügung, aber wir können dasselbe Kriterium mit einer oberen und einer unteren Schranke formulieren:

{-@ measure state_y_correct @-}
state_y_correct :: State -> Bool
state_y_correct (State m _ _ x y _) = (fromIntegral y) - 0.5 <= m * (fromIntegral x) && (fromIntegral y) + 0.5 > m * (fromIntegral x)

Das ganzzahlige y soll sich sozusagen in einem engen Korridor um die Ideallinie herum bewegen.

Die beiden Measures können wir verwenden, um einen neuen Datentypen ValidState zu definieren:

{-@ type ValidState = {st:State | state_y_correct st && state_d_correct st} @-}

Unser step-4 können wir dann 1-zu-1 übersetzen:

{-@ step :: st:ValidState -> {st':ValidState | state_x st' == state_x st + 1} @-}
step :: State -> State
step (State m dx dy x y d) =
  if d >= 0
  then
    (State m dx dy (x + 1) (y + 1) (d + ((2 * dy) - (2 * dx))))
  else
    (State m dx dy (x + 1) y (d + (2 * dy)))

Liquid Haskell ist damit einverstanden. Wir haben den Bresenham-Algorithmus also mal wieder korrekt implementiert.³

Um in die Welt der validen States einzutreten, schreiben wir uns noch eine kleine Hilfsfunktion:

{-@ init_state :: m:Double -> {dx:Int | dx > 0} -> {dy:Int | dy < dx && dy > 0 && m * dx == dy} -> ValidState @-}
init_state :: Double -> Int -> Int -> State
init_state m dx dy = State m dx dy x y d
  where
    x = 0
    y = 0
    d = 2 * dy * (x + 1) - (2 * y * dx) - dx

Diese Funktion hat noch den Ergonomie-Nachteil, dass wir ein passendes m übergeben müssen, welches ein Computer doch eigentlich für uns ausrechnen könnte. Wir schreiben deshalb noch eine weitere Hilfsfunktion, bei der wir die Division knallhart durchführen und mit assume gegenüber Liquid Haskell beteuern, dass wir uns sicher sind, dass die Rechnung ihre Spezifikation auch einhält.

{-@ data Frac = Frac { rate :: Double, numer :: Int, denom :: Int } @-}
data Frac = Frac { rate :: Double, numer :: Int, denom :: Int }

{-@ init_state' :: {dx:Int | dx > 0} -> {dy:Int | dy < dx && dy > 0} -> ValidState @-}
init_state' :: Int -> Int -> ValidState
init_state' dx dy = init_state (rate frac) (numer frac) (denom frac)
  where
    {-@ assume frac :: {v:Frac | (rate v) * (numer v) == (denom v) && (numer v) > 0 && (denom v) < (numer v) && (denom v) > 0} @-}
    frac :: Frac
    frac = Frac ((fromIntegral dy) / (fromIntegral dx)) dx dy