examples/verifythis_2019_cartesian_trees.mlw

   1 (** {1 VerifyThis @ ETAPS 2019 competition Challenge 2: Cartesian Trees }
   2
   3 Author: Quentin Garchery (LRI, Université Paris Sud)
   4 *)
   5
   6 use int.Int
   7 use list.ListRich
   8 use array.Array
   9 use exn.Exn
  10
  11
  12 (** {2 PART A : All nearest smaller value} *)
  13
  14 clone list.Sorted as Decr with type t = int, predicate le = (>=)
  15
  16 (** Implement the stack with a list *)
  17
  18 let function destruct l
  19   requires { not is_nil l }
  20 =
  21   match l with
  22   | Cons h t -> h, t end
  23
  24 let function peek l
  25   requires { not is_nil l }
  26   ensures { mem result l }
  27 =
  28   let h, _ = destruct l in
  29   h
  30
  31 let function tail l
  32   requires { not is_nil l }
  33 =
  34   let _, t = destruct l in
  35   t
  36
  37 lemma destruct_peek_tail :
  38   forall l : list 'a. not is_nil l -> l = Cons (peek l) (tail l)
  39
  40 (** Compute the sequence of left neighbors *)
  41
  42 let smaller_left (s : array int) : array int
  43   (* Task 1 : left neighbor has smaller index *)
  44   ensures { forall y. 0 <= y < s.length -> result[y] < y }
  45   (* Task 2 : left neighbor has smaller value *)
  46   ensures { forall y. 0 <= y < s.length -> 0 <= result[y] ->
  47                       s[result[y]] < s[y] }
  48   (* Task 3 : no smaller value between an element and its left neighbor *)
  49   ensures { forall x z. 0 <= x < s.length ->
  50                         result[x] < z < x -> s[z] >= s[x] }
  51 ensures { result.length = s.length }
  52 =
  53   let n = s.length in
  54   let left = make n (-1) in
  55   let ref my_stack = Nil in
  56   for x = 0 to s.length - 1 do
  57       (* To show that the access are correct *)
  58       invariant { forall z. mem z my_stack -> 0 <= z < x }
  59       (* Good formation of the stack *)
  60       invariant { is_nil my_stack -> x = 0 }
  61       invariant { not is_nil my_stack -> peek my_stack = x-1 }
  62       invariant { Decr.sorted my_stack }
  63       (* Task 1 *)
  64       invariant { forall y. 0 <= y < x -> left[y] < y }
  65       (* Task 2 *)
  66       invariant { forall y. 0 <= y < x -> 0 <= left[y] ->
  67                             s[left[y]] < s[y] }
  68       (* Show that we only need to look in the stack to find the nearest smaller value *)
  69       invariant { forall z. 0 <= z < x ->
  70                   exists y. z <= y < x /\ mem y my_stack /\ s[y] <= s[z] }
  71       (* Task 3 *)
  72       invariant { forall y z. 0 <= y < x -> left[y] < z < y ->
  73                                s[z] >= s[y] }
  74       label BeforeLoop in
  75       while not is_nil my_stack && s[peek my_stack] >= s[x] do
  76             (* Good formation of the stack *)
  77             invariant { forall z. mem z my_stack -> 0 <= z < x }
  78             invariant { Decr.sorted my_stack }
  79             (* Remember that what was removed from the stack was too big *)
  80             invariant { forall z. mem z (my_stack at BeforeLoop) ->
  81                                   s[z] >= s[x] \/ mem z my_stack }
  82             (* Make sure that stack elements at the right of the current top of the stack
  83                were previously removed *)
  84             invariant { forall z. not is_nil my_stack ->
  85                                   mem z my_stack -> z <= peek my_stack }
  86             (* Task 3 *)
  87             invariant { forall z. not is_nil my_stack ->
  88                                   peek my_stack < z < x -> s[z] >= s[x] }
  89             invariant { forall z. is_nil my_stack -> 0 <= z < x ->
  90                                   s[z] >= s[x] }
  91             variant { Length.length my_stack }
  92             my_stack <- tail my_stack
  93       done;
  94       assert { not is_nil my_stack -> s[peek my_stack] < s[x] };
  95       if is_nil my_stack
  96       then left[x] <- -1
  97       else left[x] <- peek my_stack;
  98       assert { 0 <= left[x] -> s[left[x]] < s[x] };
  99       my_stack <- Cons x my_stack
 100   done;
 101   left
 102
 103 (** Same thing but for closest smaller right value :
 104  when there is no such value, return an integer greater than the length *)
 105
 106 val smaller_right (s : array int) : array int
 107   (* Task 1 : right neighbor has greater index *)
 108   ensures { forall y. 0 <= y < s.length -> result[y] > y }
 109   (* Task 2 : right neighbor has smaller value *)
 110   ensures { forall y. 0 <= y < s.length -> result[y] < s.length ->
 111                       s[result[y]] < s[y] }
 112   (* Task 3 : no smaller value between an element and its right neighbor *)
 113   ensures { forall x z. 0 <= x < s.length ->
 114                         x < z < result[x] -> s[z] >= s[x] }
 115   ensures { result.length = s.length }
 116
 117
 118 (** {2 PART B : Construction of a Cartesian Tree} *)
 119
 120
 121 use option.Option
 122
 123 type dir = { left : option int;
 124            right : option int }
 125
 126 type dirs = array dir
 127
 128 predicate parent (t : dirs) (p s : int) =
 129  t[p].left = Some s \/ t[p].right = Some s
 130
 131 inductive descendant dirs int int =
 132  | Self : forall t p s. p = s -> descendant t p s
 133  | Son_left  : forall t p s1 s2. descendant t p s1 -> t[s1].left  = Some s2 ->
 134                descendant t p s2
 135  | Son_right : forall t p s1 s2. descendant t p s1 -> t[s1].right = Some s2 ->
 136                descendant t p s2
 137
 138 predicate is_smallest (a : array int) (i : int) =
 139  0 <= i < a.length /\
 140  forall j. 0 <= j < a.length -> a[i] <= a[j]
 141
 142 (** Construct an array storing the eventual sons of a node *)
 143
 144 let construct_dirs (a : array int) : dirs
 145   requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] }
 146   ensures { result.length = a.length }
 147   (* Task 2 ++, heap property :
 148      left and right sons have greater value than the parent
 149      left son is on the left in the array, right son is on the right
 150      between indices of parent and son there is no smaller value *)
 151   ensures { forall j v. 0 <= j < a.length ->
 152                   (result[j].left = Some v ->
 153                   a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\
 154                   (result[j].right = Some v ->
 155                   a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) }
 156   ensures { forall p s. 0 <= p < a.length -> descendant result p s ->
 157             0 <= s < a.length /\ a[s] >= a[p] }
 158   (* Task3, in-order traversal :
 159      every "left-descendant" is located on the left in the array
 160      every "right-descendant" is located on the right in the array *)
 161   ensures { forall p1 p2 s. 0 <= p1 < a.length -> descendant result p2 s ->
 162             (result[p1].left  = Some p2 -> s < p1) /\
 163             (result[p1].right = Some p2 -> s > p1) }
 164   (* Task 1, well-formedness *)
 165   (* Every non-minimal element has a parent *)
 166   ensures { forall i k. 0 <= i < a.length -> 0 <= k < a.length -> a[k] < a[i] ->
 167             exists sm. 0 <= sm < a.length /\ parent result sm i }
 168   ensures { forall i. 0 <= i < a.length ->
 169             (is_smallest a i \/
 170             (exists sm. 0 <= sm < a.length /\ parent result sm i)) }
 171   (* Every element has at most one parent *)
 172   ensures { forall p1 p2 s. 0 <= p1 < a.length -> 0 <= p2 < a.length -> 0 <= s < a.length ->
 173             parent result p1 s -> parent result p2 s -> p1 = p2 }
 174   (* No cycles *)
 175   ensures { forall p1 p2 s. 0 <= p1 < a.length -> 0 <= p2 < a.length -> 0 <= s < a.length ->
 176             parent result p1 p2 -> descendant result p2 s -> p1 <> s }
 177 =
 178   let n = a.length in
 179   let s_left = smaller_left a in
 180   let s_right = smaller_right a in
 181   let dirs = Array.make n {left = None; right = None} in
 182   for i = 0 to n-1 do
 183       (* Task 2 ++ *)
 184       invariant { forall j v. 0 <= j < a.length ->
 185                   (dirs[j].left = Some v ->
 186                   a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] >= a[j]) /\
 187                   (dirs[j].right = Some v ->
 188                   a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] >= a[j]) }
 189       (* Show that once a parent is set-up in <dirs>, it does not change *)
 190       invariant { forall j. 0 <= j < i ->
 191                   if s_left[j] >= 0 && s_right[j] >= n
 192                   then dirs[s_left[j]].right = Some j
 193                   else if s_left[j] < 0 && s_right[j] < n
 194                   then dirs[s_right[j]].left = Some j
 195                   else if s_left[j] >= 0 && s_right[j] < n
 196                   then if a[s_left[j]] > a[s_right[j]]
 197                        then dirs[s_left[j]].right = Some j
 198                        else dirs[s_right[j]].left = Some j
 199                   else true
 200                  }
 201       invariant { forall j p. 0 <= j < a.length -> 0 <= p < a.length ->
 202                   (dirs[p].right = Some j -> p = s_left[j] /\
 203                   (s_right[j] < n -> a[s_left[j]] > a[s_right[j]]) ) /\
 204                   (dirs[p].left  = Some j -> p = s_right[j] /\
 205                   (s_left[j] >= 0 -> a[s_left[j]] <= a[s_right[j]])) }
 206       let li = s_left[i] in
 207       let ri = s_right[i] in
 208       if li >= 0
 209       then if ri < n
 210            then if a[li] > a[ri]
 211                 then dirs[li] <- { dirs[li] with right = Some i }
 212                 else dirs[ri] <- { dirs[ri] with left  = Some i }
 213            else dirs[li] <- { dirs[li] with right = Some i }
 214       else if ri < n
 215            then dirs[ri] <- { dirs[ri] with left  = Some i }
 216   done;
 217   dirs
 218
 219
 220 (** The function <par> finds the parent of a node and is used to define <all_descendant_root>.
 221 This last lemma function is useful to show that every node is reachable from the root *)
 222
 223 let par (a : array int) (dirs : array dir) (j : int)
 224   requires { exists sm. 0 <= sm < a.length /\ parent dirs sm j }
 225   requires { a.length = dirs.length }
 226   requires { forall j v. 0 <= j < a.length ->
 227                   (dirs[j].left = Some v ->
 228                   a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\
 229                   (dirs[j].right = Some v ->
 230                   a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) }
 231   ensures { 0 <= result < a.length }
 232   ensures { parent dirs result j }
 233 =
 234   assert { not a.length = 0 };
 235   let ref res = 0 in
 236   for i = 0 to a.length - 1 do
 237       invariant { 0 <= res < a.length }
 238       invariant { parent dirs res j \/ exists sm. i <= sm < a.length /\ parent dirs sm j }
 239       match dirs[i].left with
 240       | Some jl -> if jl = j then res <- i
 241       | None -> ()
 242       end;
 243       match dirs[i].right with
 244       | Some jr -> if jr = j then res <- i
 245       | None -> ()
 246       end
 247   done;
 248   res
 249
 250
 251 let rec lemma all_descendant_root a dirs root j
 252   variant { a[j] - a[root] }
 253   requires { a.length = dirs.length }
 254   requires { forall j v. 0 <= j < a.length ->
 255                   (dirs[j].left = Some v ->
 256                   a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\
 257                   (dirs[j].right = Some v ->
 258                   a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) }
 259   requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] }
 260   requires { 0 <= j < a.length /\ 0 <= root < a.length }
 261   requires { is_smallest a root }
 262   requires { forall i. 0 <= i < a.length ->
 263             (is_smallest a i \/
 264             (exists sm. 0 <= sm < a.length /\ parent dirs sm i)) }
 265   ensures { descendant dirs root j }
 266 =
 267   if a[j] <> a[root]
 268   then all_descendant_root a dirs root (par a dirs j)
 269
 270 (** Finds the root of the direction tree : it's the smallest element in the array *)
 271
 272 let find_smaller a =
 273   ensures { match result with
 274             | Some mv -> is_smallest a mv
 275             | None -> a.length = 0
 276             end }
 277   let ref m = None in
 278   for i = 0 to a.length - 1 do
 279       invariant { match m with
 280             | Some mv -> 0 <= mv < a.length /\ forall j. 0 <= j < i -> a[mv] <= a[j]
 281             | None -> i = 0
 282             end }
 283       match m with
 284       | Some mv -> if a[mv] > a[i] then m <- Some i
 285       | _ -> m <- Some i
 286       end
 287   done;
 288   m
 289
 290 (** The other way to define descendant. Useful here because it follows the definition of
 291  <traversal> *)
 292
 293 lemma other_descendant :
 294  forall t p1 p2 s. parent t p1 p2 -> descendant t p2 s ->
 295                    descendant t p1 s
 296
 297 lemma inv_other_descendant :
 298  forall t p1 s. descendant t p1 s ->
 299  p1 = s \/
 300  exists p2. parent t p1 p2 /\ descendant t p2 s
 301
 302 clone list.Sorted as StrictIncr with type t = int, predicate le = (<)
 303
 304 (** In-order traversal, we store the indices we traversed *)
 305
 306 let rec traversal (a : array int) dirs top (ghost s : int) (ghost e)
 307   variant { e - s }
 308   requires { dirs.length = a.length }
 309   requires { 0 <= s <= e <= a.length }
 310   requires { forall p1 p2 s. 0 <= p1 < a.length -> descendant dirs p2 s ->
 311              (dirs[p1].left  = Some p2 -> s < p1) /\
 312              (dirs[p1].right = Some p2 -> s > p1) }
 313   requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] }
 314   requires { match top with
 315              | Some top -> forall son. descendant dirs top son <-> s <= son < e
 316              | None -> s = e end }
 317   ensures { forall x. mem x result <-> s <= x < e }
 318   ensures { StrictIncr.sorted result }
 319 =
 320   match top with
 321   | None -> Nil
 322   | Some top ->
 323          assert { s <= top < e by descendant dirs top top };
 324          let dir = dirs[top] in
 325          traversal a dirs dir.left s top ++
 326          Cons top (
 327          traversal a dirs dir.right (top+1) e)
 328   end
 329
 330 (** We traverse the tree <construct_dirs a> in-order from the root <find_smaller a>,
 331  and we collect the indices. Last 2 arguments of <traversal> are ghost.
 332
 333  We show that the result is the list [0..(a.length-1)], the in-order traversal of
 334  the tree traverses elements from 0 to (a.length-1)
 335 *)
 336
 337 let in_order a
 338   requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] }
 339   ensures { forall x. mem x result <-> 0 <= x < a.length }
 340   ensures { StrictIncr.sorted result }
 341 =
 342   traversal a (construct_dirs a) (find_smaller a) 0 a.length