examples/vstte12_tree_reconstruction.mlw

   1
   2 (* The 2nd Verified Software Competition (VSTTE 2012)
   3    https://sites.google.com/site/vstte2012/compet
   4
   5    Problem 4: Tree Reconstruction
   6    Build a binary tree from a list of leaf depths, if any
   7
   8    This is a purely applicative implementation, using immutable
   9    lists from Why3's standard library.
  10 *)
  11
  12 module Tree
  13
  14   use export int.Int
  15   use export list.List
  16   use export list.Append
  17
  18   type tree = Leaf | Node tree tree
  19
  20   (* the list of leaf depths for tree t, if root is at depth d *)
  21   let rec function depths (d: int) (t: tree) : list int =
  22     match t with
  23     | Leaf -> Cons d Nil
  24     | Node l r -> depths (d+1) l ++ depths (d+1) r
  25     end
  26
  27   (* lemmas on depths *)
  28
  29   lemma depths_head:
  30     forall t: tree, d: int.
  31     match depths d t with Cons x _ -> x >= d | Nil -> false end
  32
  33   let rec lemma depths_unique (t1 t2: tree) (d: int) (s1 s2: list int)
  34     requires { depths d t1 ++ s1 = depths d t2 ++ s2 }
  35     variant { t1 }
  36     ensures { t1 = t2 && s1 = s2 }
  37   = let d' = d+1 in
  38     match t1,t2 with
  39     | Leaf,Leaf -> ()
  40     | Node t11 t12, Node t21 t22 ->
  41       depths_unique t11 t21 d' (depths d' t12 ++ s1) (depths d' t22 ++ s2);
  42       depths_unique t12 t22 d' s1 s2
  43     | Leaf, (Node t _) | (Node t _), Leaf ->
  44       match depths d' t with
  45       | Nil -> absurd
  46       | Cons x _ -> assert { x >= d' }
  47       end
  48     end
  49
  50   lemma depths_prefix:
  51     forall t: tree, d1 d2: int, s1 s2: list int.
  52     depths d1 t ++ s1 = depths d2 t ++ s2 -> d1 = d2
  53
  54   lemma depths_prefix_simple:
  55     forall t: tree, d1 d2: int.
  56     depths d1 t = depths d2 t -> d1 = d2
  57
  58   let rec lemma depths_subtree (t1 t2: tree) (d1 d2:int) (s1:list int)
  59     requires { depths d1 t1 ++ s1 = depths d2 t2 }
  60     variant { t1 }
  61     ensures { d1 >= d2 }
  62   = assert { depths d2 t2 = depths d2 t2 ++ Nil };
  63     match t1 with
  64     | Leaf -> ()
  65     | Node t3 t4 ->
  66         depths_subtree t3 t2 (d1+1) d2 (depths (d1+1) t4 ++ s1)
  67     end
  68
  69   lemma depths_unique2:
  70     forall t1 t2: tree, d1 d2: int.
  71     depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2
  72
  73 end
  74
  75 module TreeReconstruction
  76
  77   use export Tree
  78   use list.Length
  79   use list.HdTlNoOpt
  80
  81   exception Failure
  82     (* used to signal the algorithm's failure i.e. there is no tree *)
  83
  84   let rec build_rec (d: int) (s: list int) : (t: tree, s': list int)
  85     variant { length s, hd s - d }
  86     ensures { s = depths d t ++ s' }
  87     raises  { Failure -> forall t: tree, s' : list int. depths d t ++ s' <> s }
  88   = match s with
  89     | Nil ->
  90         raise Failure
  91     | Cons h t ->
  92         if h < d then raise Failure;
  93         if h = d then
  94           Leaf, t
  95         else
  96           let l, s = build_rec (d+1) s in
  97           let r, s = build_rec (d+1) s in
  98           Node l r, s
  99     end
 100
 101   let build (s: list int) : tree
 102     ensures { depths 0 result = s }
 103     raises  { Failure -> forall t: tree. depths 0 t <> s }
 104   = let t, s = build_rec 0 s in
 105     match s with
 106     | Nil -> t
 107     | _ -> raise Failure
 108     end
 109
 110 end
 111
 112 module Harness
 113
 114   use TreeReconstruction
 115
 116   let harness ()
 117     ensures { result = Node Leaf (Node (Node Leaf Leaf) Leaf) }
 118     raises  { Failure -> false }
 119   = build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil))))
 120
 121   let harness2 () : (_:tree)
 122     ensures { false } raises { Failure -> true }
 123   = build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil))))
 124
 125 end
 126
 127 (*
 128   A variant implementation proposed by Jayadev Misra
 129
 130   Given the input list [x1; x2; ...; xn], we first turn it into the
 131   list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)].  Then,
 132   repeatedly, we scan this list from left to right, looking for two
 133   consecutive pairs (v1, t1) and (v2, t2) with v1 = v2.  Then we
 134   replace them with the pair (v1-1, Node t1 t2) and we start again.
 135   We stop when there is only one pair left (v,t). Then we must have v=0.
 136
 137   The implementation below achieves linear complexity using a zipper
 138   data structure to traverse the list of pairs. The left list contains
 139   the elements already traversed (thus on the left), in reverse order,
 140   and the right list contains the elements yet to be traversed.
 141
 142 *)
 143
 144 (* Proving termination is quite easy and we do it first (though we could,
 145    obviously, do it together with proving correctness) *)
 146
 147 module ZipperBasedTermination
 148
 149   use Tree
 150   use list.Length
 151   use list.Reverse
 152
 153   exception Failure
 154
 155   let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
 156     variant { length left + length right, length right }
 157     raises  { Failure }
 158   = match left, right with
 159     | _, Nil ->
 160         raise Failure
 161     | Nil, Cons (v, t) Nil ->
 162         if v = 0 then t else raise Failure
 163     | Nil, Cons (v, t) right' ->
 164         tc (Cons (v, t) Nil) right'
 165     | Cons (v1, t1) left', Cons (v2, t2) right' ->
 166         if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right')
 167         else tc (Cons (v2, t2) left) right'
 168     end
 169
 170 end
 171
 172 (* Now soundness and completeness *)
 173
 174 module ZipperBased
 175
 176   use Tree
 177   use list.Length
 178   use list.Reverse
 179
 180   (* the following function generalizes function [depths] to a forest, that
 181      is a list of pairs (depth, tree) *)
 182
 183   function forest_depths (f: list (int, tree)) : list int = match f with
 184   | Nil -> Nil
 185   | Cons (d, t) r -> depths d t ++ forest_depths r
 186   end
 187
 188   (* an obvious lemma on [forest_depths] *)
 189
 190   lemma forest_depths_append:
 191     forall f1 f2: list (int, tree).
 192     forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2
 193
 194   (* to prove completeness, one needs an invariant over the list [left].
 195      The main ingredient is predicate [greedy] below, which states that
 196      [d] is distinct from all depths along the left branch of [d1, t1]. *)
 197
 198   predicate greedy (d: int) (d1: int) (t1: tree) =
 199     d <> d1 /\ match t1 with Leaf -> true | Node l1 _ -> greedy d (d1+1) l1 end
 200
 201   (* then we extend it to a list of pairs [(dn,tn); ...; (d2,t2); (d1,t1)]
 202      as follows: [greedy d2 d1 t1], [greedy d3 d2 t2], etc.
 203      this is inductive predicate [g] *)
 204
 205   inductive g (l: list (int, tree)) =
 206     | Gnil: g Nil
 207     | Gone: forall d: int, t: tree. g (Cons (d, t) Nil)
 208     | Gtwo: forall d1 d2: int, t1 t2: tree, l: list (int, tree).
 209         greedy d1 d2 t2 -> g (Cons (d1, t1) l) ->
 210         g (Cons (d2, t2) (Cons (d1, t1) l))
 211
 212   (* an easy lemma on [g] *)
 213
 214   lemma g_append:
 215     forall l1 [@induction] l2: list (int, tree). g (l1 ++ l2) -> g l1
 216
 217   (* key lemma for completeness: whenever we fail because [right] is empty,
 218      we have to prove that there is no solution
 219
 220      Note: the proof first generalizes the statement as follows:
 221        forest_depths ((d1,t1) :: l) <> depths d t + s
 222      whenever d < d1 (see the corresponding Coq file) *)
 223
 224   lemma depths_length: forall t d. length (depths d t) >= 1
 225   lemma forest_depths_length: forall l. length (forest_depths l) >= 0
 226   lemma g_tail: forall l1 l2: list (int, tree). g (l1 ++ l2) -> g l2
 227
 228   lemma key_lemma : forall t l d d1 t1 s. d < d1 ->
 229     1 <= length l -> g (reverse (Cons (d1, t1) l)) ->
 230     not (forest_depths (Cons (d1, t1) l) = (depths d t) ++ s)
 231
 232   lemma right_nil:
 233     forall l: list (int, tree). length l >= 2 -> g l ->
 234     forall t: tree, d: int.
 235     forest_depths (reverse l) <> depths d t
 236
 237   (* key lemma for soundness: preservation of the invariant when we move
 238      a tree from [right] to [left] *)
 239
 240   lemma main_lemma:
 241     forall l: list (int, tree), d1 d2: int, t1 t2: tree. d1 <> d2 ->
 242     g (Cons (d1, t1) l) ->
 243     match t2 with Node l2 _ -> greedy d1 (d2+1) l2 | Leaf -> true end ->
 244     g (Cons (d2, t2) (Cons (d1, t1) l))
 245
 246   (* finally, we need a predicate to state that a forest [l] contains only
 247      leaves *)
 248
 249   predicate only_leaf (l: list (int, tree)) = match l with
 250     | Nil -> true
 251     | Cons (_, t) r -> t = Leaf /\ only_leaf r
 252   end
 253
 254   exception Failure
 255
 256   let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
 257     requires { (* list [left] satisfies the invariant *)
 258       g left /\
 259       (* when [left] has one element, it can't be a solution *)
 260       match left with Cons (d1, _) Nil -> d1 <> 0 \/ right <> Nil
 261                     | _                -> true                    end /\
 262       (* apart (possibly) from its head, all elements in [right] are leaves;
 263          moreover the left branch of [right]'s head already satisfies
 264          invariant [g] when consed to [left] *)
 265       match right with
 266         | Cons (d2, t2) right' -> only_leaf right' /\
 267             match t2 with Node l2 _ -> g (Cons (d2+1, l2) left)
 268                         | Leaf      -> true end
 269         | Nil -> true end }
 270     variant { length left + 2 * length right }
 271     ensures { depths 0 result = forest_depths (reverse left ++ right) }
 272     raises { Failure ->
 273       forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) }
 274   = match left, right with
 275     | _, Nil ->
 276         raise Failure
 277     | Nil, Cons (v, t) Nil ->
 278         if v = 0 then t else raise Failure
 279     | Nil, Cons (v, t) right' ->
 280         tc (Cons (v, t) Nil) right'
 281     | Cons (v1, t1) left', Cons (v2, t2) right' ->
 282         if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right')
 283         else tc (Cons (v2, t2) left) right'
 284     end
 285
 286   (* Getting function [build] from [tc] is easy: from the list
 287      [x1; x2; ...; xn] we simply build the list of pairs
 288      [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)].
 289      Function [map_leaf] below does this. *)
 290
 291   let rec function map_leaf (l: list int) : list (int, tree) =
 292     match l with
 293     | Nil -> Nil
 294     | Cons d r -> Cons (d, Leaf) (map_leaf r)
 295     end
 296
 297   (* two lemmas on [map_leaf] *)
 298
 299   lemma map_leaf_depths:
 300     forall l: list int. forest_depths (map_leaf l) = l
 301
 302   lemma map_leaf_only_leaf:
 303     forall l: list int. only_leaf (map_leaf l)
 304
 305   let build (s: list int)
 306     ensures { depths 0 result = s }
 307     raises  { Failure -> forall t: tree. depths 0 t <> s }
 308   = tc Nil (map_leaf s)
 309
 310 end