examples/just_join.mlw

   1
   2 (** Just Join for Parallel Ordered Sets
   3
   4   Guy E. Blelloch, Daniel Ferizovic, Yihan Sun
   5   28th ACM Symposium on Parallelism in Algorithms and Architectures, 2016
   6   https://www.cs.cmu.edu/~guyb/papers/BFS16.pdf
   7
   8   In the paper above, the authors implement various kinds of balanced
   9   binary search trees on top of a `join` operation. This includes the
  10   case of AVL trees, for which the authors prove that `join` preserves
  11   the AVL property (Lemma 1 in the paper).
  12
  13   In the proof below, we verify this lemma using Why3 (the AVL
  14   property, not the complexity). The paper skips the details regarding
  15   the AVL property---“The resulting tree satisfies the AVL invariants
  16   since rotations are used to restore the invariant (details left
  17   out)”---but the proof happens to be subtle. See CRITICAL below.
  18
  19   Authors: Jean-Christophe Filliâtre (CNRS)
  20            Paul Patault (Univ Paris-Saclay)
  21 *)
  22
  23 use int.Int
  24 use int.MinMax
  25
  26 (** the type `elt` of elements, ordered with `lt` *)
  27 type elt
  28
  29 val (=) (x y: elt) : bool
  30   ensures { result <-> x=y }
  31
  32 val predicate lt elt elt
  33 clone relations.TotalStrictOrder with
  34   type t = elt, predicate rel = lt, axiom .
  35
  36 (** the type of AVL trees, with the height stored in the first component
  37     so that we get the height in O(1) with function `ht` *)
  38 type tree = E | N int tree elt tree
  39
  40 let function ht (t: tree) : int =
  41   match t with E -> 0 | N h _ _ _ -> h end
  42
  43 let function node (l: tree) (x: elt) (r: tree) : tree =
  44   N (1 + max (ht l) (ht r)) l x r
  45
  46 let rec ghost function height (t: tree) : int
  47   ensures { result >= 0 }
  48 = match t with
  49   | E         -> 0
  50   | N _ l _ r -> 1 + max (height l) (height r)
  51   end
  52
  53 (** trees are well-formed i.e. the height stored in the nodes is correct *)
  54 predicate wf (t: tree) =
  55   match t with
  56   | E         -> true
  57   | N h l x r -> h = height t && wf l && wf r
  58   end
  59
  60 (** AVL are binary search trees *)
  61
  62 predicate mem (y: elt) (t: tree) =
  63   match t with
  64   | E         -> false
  65   | N _ l x r -> mem y l || y=x || mem y r
  66   end
  67
  68 predicate tree_lt (t: tree) (y: elt) =
  69   forall x. mem x t -> lt x y
  70
  71 predicate lt_tree (y: elt) (t: tree) =
  72   forall x. mem x t -> lt y x
  73
  74 predicate bst (t: tree) =
  75   match t with
  76   | E         -> true
  77   | N _ l x r -> bst l && tree_lt l x && bst r && lt_tree x r
  78   end
  79
  80 (** AVL height invariant *)
  81 predicate avl (t: tree) =
  82   match t with
  83   | E         -> true
  84   | N _ l _ r -> avl l && avl r && -1 <= height l - height r <= 1
  85   end
  86
  87 (** Code starts here
  88
  89   Note: It is a pity that the specification for `rotate_left` and `rotate_right` is
  90   longer than the code, but we can't make them logical functions since
  91   they are partial functions. *)
  92
  93 let rotate_left (t: tree) : (r: tree)
  94   requires { wf t  } ensures { wf r  }
  95   requires { bst t } ensures { bst r }
  96   requires { match t with N _ _ _ (N _ _ _ _) -> true | _ -> false end }
  97   ensures  { match t with N _ a x (N _ b y c) ->
  98              match r with N _ (N _ ra rx rb) ry rc ->
  99                ra=a && rx=x && rb=b && ry=y && rc=c
 100              | _ -> false end | _ -> false end }
 101 = match t with
 102   | N _ a x (N _ b y c) -> node (node a x b) y c
 103   | _ -> absurd
 104   end
 105
 106 let rotate_right (t: tree) : (r: tree)
 107   requires { wf t  } ensures { wf r  }
 108   requires { bst t } ensures { bst r }
 109   requires { match t with N _ (N _ _ _ _) _ _ -> true | _ -> false end }
 110   ensures  { match t with N _ (N _ a x b) y c ->
 111              match r with N _ ra rx (N _ rb ry rc) ->
 112                ra=a && rx=x && rb=b && ry=y && rc=c
 113              | _ -> false end | _ -> false end }
 114 = match t with
 115   | N _ (N _ a x b) y c -> node a x (node b y c)
 116   | _ -> absurd
 117   end
 118
 119 let rec join_right (l: tree) (x: elt) (r: tree) : tree
 120   requires { wf l && wf r } ensures { wf result }
 121   requires { bst l && tree_lt l x }
 122   requires { bst r && lt_tree x r } ensures { bst result }
 123   ensures  { forall y. mem y result <-> (mem y l || y=x || mem y r) }
 124   requires { height l >= height r + 2 } variant { height l }
 125   requires { avl l && avl r } ensures { avl result }
 126   (* CRITICAL *)
 127   ensures  { height result = height l ||
 128              height result = height l + 1 && match result with
 129                | N _ rl _ rr ->
 130                    height rl = height l - 1 && height rr = height l
 131                | _ -> false end }
 132 = match l with
 133   | N _ ll lx lr ->
 134       if ht lr <= ht r + 1 then
 135         let t = node lr x r in
 136         if ht t <= ht ll + 1 then node ll lx t
 137         else rotate_left (node ll lx (rotate_right t))
 138       else
 139         let t = join_right lr x r in
 140         let t' = node ll lx t in
 141         if ht t <= ht ll + 1 then t' else rotate_left t'
 142         (*                                ^^^^^^^^^^^^^^
 143            The CRITICAL postcondition is used here
 144            to show that the rotated tree is indeed an AVL. *)
 145   | E -> absurd
 146   end
 147
 148 let rec join_left (l: tree) (x: elt) (r: tree) : tree
 149   requires { wf l && wf r } ensures { wf result }
 150   requires { bst l && tree_lt l x }
 151   requires { bst r && lt_tree x r } ensures { bst result }
 152   ensures  { forall y. mem y result <-> (mem y l || y=x || mem y r) }
 153   requires { height r >= height l + 2 } variant { height r }
 154   requires { avl l && avl r } ensures { avl result }
 155   (* CRITICAL *)
 156   ensures  { height result = height r ||
 157              height result = height r + 1 && match result with
 158                | N _ rl _ rr ->
 159                    height rr = height r - 1 && height rl = height r
 160                | _ -> false end }
 161 = match r with
 162   | N _ rl rx rr ->
 163       if ht rl <= ht l + 1 then
 164         let t = node l x rl in
 165         if ht t <= ht rr + 1 then node t rx rr
 166         else rotate_right (node (rotate_left t) rx rr)
 167       else
 168         let t = join_left l x rl in
 169         let t' = node t rx rr in
 170         if ht t <= ht rr + 1 then t' else rotate_right t'
 171         (*                                ^^^^^^^^^^^^^^^ *)
 172   | E -> absurd
 173   end
 174
 175 let join (l: tree) (x: elt) (r: tree) : tree
 176   requires { wf l && wf r } ensures { wf result }
 177   requires { bst l && tree_lt l x }
 178   requires { bst r && lt_tree x r } ensures { bst result }
 179   ensures  { forall y. mem y result <-> (mem y l || y=x || mem y r) }
 180   requires { avl l && avl r } ensures { avl result }
 181   ensures  { height result <= 1 + max (height l) (height r) }
 182 =      if ht l > ht r + 1 then join_right l x r
 183   else if ht r > ht l + 1 then join_left  l x r
 184   else                         node       l x r
 185
 186 (** The remaining is much simpler. *)
 187
 188 let rec split (t: tree) (y: elt) : (l: tree, b: bool, r: tree)
 189   requires { wf t && bst t && avl t }
 190   variant  { height t }
 191   ensures  { wf l && bst l && avl l } ensures { tree_lt l y }
 192   ensures  { wf r && bst r && avl r } ensures { lt_tree y r }
 193   ensures  { forall x. mem x t <-> (mem x l || mem x r || b && x=y) }
 194 = match t with
 195   | E -> E, false, E
 196   | N _ l x r ->
 197            if y = x then l, true, r
 198       else if lt y x then let ll, b, lr = split l y in ll, b, join lr x r
 199       else                let rl, b, rr = split r y in join l x rl, b, rr
 200   end
 201
 202 let insert (x: elt) (t: tree) : (r: tree)
 203   requires { wf t && bst t && avl t }
 204   ensures  { wf r && bst r && avl r }
 205   ensures  { forall y. mem y r <-> (mem y t || y=x) }
 206 = let l, _, r = split t x in
 207   join l x r
 208
 209 let rec split_last (t: tree) : (r: tree, m: elt)
 210   requires { t <> E }
 211   requires { wf t && bst t && avl t }
 212   variant  { height t }
 213   ensures  { wf r && bst r && avl r }
 214   ensures  { forall x. mem x t <-> (mem x r && lt x m || x=m) }
 215   ensures  { tree_lt r m }
 216 = match t with
 217   | N _ l x E -> l, x
 218   | N _ l x r -> let r', m = split_last r in join l x r', m
 219   | _ -> absurd
 220   end
 221
 222 let join2 (l r: tree) : (t: tree)
 223   requires { wf l && bst l && avl l }
 224   requires { wf r && bst r && avl r }
 225   requires { forall x y. mem x l -> mem y r -> lt x y }
 226   ensures  { wf t && bst t && avl t }
 227   ensures  { forall x. mem x t <-> (mem x l || mem x r) }
 228 = match l with
 229   | E -> r
 230   | _ -> let l, k = split_last l in join l k r
 231   end
 232
 233 let delete (x: elt) (t: tree) : (r: tree)
 234   requires { wf t && bst t && avl t }
 235   ensures  { wf r && bst r && avl r }
 236   ensures  { forall y. mem y r <-> (mem y t && y<>x) }
 237 = let l, _, r = split t x in
 238   join2 l r