examples/verifythis_2024_challenge0.mlw

   1
   2 (** {1 VerifyThis 2024, challenge 0, The Rope Data Structure}
   3
   4   See https://www.pm.inf.ethz.ch/research/verifythis.html
   5
   6   Team YYY: Jean-Christophe Filliâtre (CNRS)
   7 *)
   8
   9 use int.Int
  10 use seq.Seq
  11 use seq.FreeMonoid
  12
  13 (** abstract type of characters *)
  14 type char
  15
  16 (** strings are sequences of characters *)
  17 type str = seq char
  18
  19 (** Ropes are implemented here as an immutable data strcuture. *)
  20 type rope =
  21   | Leaf str
  22   | Node int rope rope
  23
  24 (** Function `to_str` is a logic function (keyword `function`)
  25     that can be used in programs as well (keyword `let`).  *)
  26 let rec function to_str (r: rope) : str =
  27   match r with
  28   | Leaf s       -> s
  29   | Node _ rl rr -> to_str rl ++ to_str rr
  30   end
  31
  32 (** We introduce a `valid` predicate to express that the weight
  33     stored in `Node` is indeed the length of the left subrope. *)
  34 predicate valid (r: rope) =
  35   match r with
  36   | Leaf _s       -> true
  37   | Node wl rl rr -> wl = length (to_str rl) && valid rl && valid rr
  38   end
  39
  40 (** Length of a rope, descending along the right spine. *)
  41 let rec str_len (r: rope) : int
  42   requires { valid r }
  43   variant  { r }
  44   ensures  { result = length (to_str r) }
  45 = match r with
  46   | Leaf s -> length s
  47   | Node wl _ rr -> wl + str_len rr
  48   end
  49
  50 (** Rope concatenation (see below for the optimized version). *)
  51 let concat (left right: rope) : rope
  52   requires { valid left }
  53   requires { valid right }
  54   ensures  { valid result }
  55   ensures  { to_str result = to_str left ++ to_str right }
  56 = Node (str_len left) left right
  57
  58 (** Splitting a rope at a given position. *)
  59 let rec split (r: rope) (i: int) : (left : rope, right: rope)
  60   requires { valid r }
  61   requires { 0 <= i <= length (to_str r) }
  62   variant  { r }
  63   ensures  { valid left }
  64   ensures  { valid right }
  65   ensures  { to_str r = to_str left ++ to_str right }
  66   ensures  { length (to_str left) = i }
  67 = match r with
  68   | Leaf s ->
  69       (Leaf s[..i], Leaf s[i..])
  70   | Node wl rl rr ->
  71       if i < wl then
  72         let rll, rlr = split rl i in
  73         (rll, concat rlr rr)
  74       else if i > wl then
  75         let rrl, rrr = split rr (i - wl) in
  76         (concat rl rrl, rrr)
  77       else
  78         (rl, rr)
  79   end
  80
  81 (** Deleting characters `i..i+len`. *)
  82 let delete (r: rope) (i len: int) : rope
  83   requires { valid r }
  84   requires { 0 <= i <= length (to_str r) }
  85   requires { 0 <= len <= length (to_str r) - i }
  86   ensures  { valid result }
  87   ensures  { to_str result = (to_str r)[..i] ++ (to_str r)[i+len..] }
  88 = let left, remaining = split r i in
  89   let _, right = split remaining len in
  90   concat left right
  91
  92 (** Predicate `is_short` is left uninterpreted, as required. *)
  93 val predicate is_short (r: str)
  94
  95 (** Optimized concatenation.
  96     Note that the contract of `concat2` is that of `concat`. *)
  97 let concat2 (left right: rope) : rope
  98   requires { valid left }
  99   requires { valid right }
 100   ensures  { valid result }
 101   ensures  { to_str result = to_str left ++ to_str right }
 102 = match right with
 103   | Leaf sr ->
 104      if is_short sr then match left with
 105        | Leaf sl ->
 106           if is_short sl then Leaf (sl ++ sr) else concat left right
 107        | Node wl rl (Leaf sl) ->
 108           if is_short sl then Node wl rl (Leaf (sl ++ sr))
 109           else concat left right
 110        | _ -> concat left right
 111      end else concat left right
 112   | _ -> concat left right
 113   end
 114
 115 (** Inserting a rope at position `i`. *)
 116 let insert (r: rope) (i: int) (to_insert: str) : rope
 117   requires { valid r }
 118   requires { 0 <= i <= length (to_str r) }
 119   ensures  { valid result }
 120   ensures  { to_str result = (to_str r)[..i] ++ to_insert ++ (to_str r)[i..] }
 121 = let left, right = split r i in
 122   concat left (concat (Leaf to_insert) right)
 123
 124 (** The lizard examples *)
 125
 126 val constant char_l: char
 127 val constant char_i: char
 128 val constant char_z: char
 129 val constant char_a: char
 130 val constant char_r: char
 131 val constant char_d: char
 132
 133 let constant str_lizard: str =
 134   cons char_l (cons char_i (cons char_z (
 135   cons char_a (cons char_r (cons char_d empty)))))
 136
 137 let constant str_lard : str =
 138   cons char_l (cons char_a (cons char_r (cons char_d empty)))
 139
 140 let test_delete (r: rope) : rope
 141   requires { valid r }
 142   requires { to_str r = str_lizard }
 143   ensures  { to_str result = str_lard }
 144 = delete r 1 2
 145
 146 let constant str_iz : str =
 147   cons char_i (cons char_z empty)
 148
 149 let test_insert (r: rope) : rope
 150   requires { valid r }
 151   requires { to_str r = str_lard }
 152   ensures  { to_str result == str_lizard }
 153 = insert r 1 str_iz