examples/verifythis_2021_lexicographic_permutations_2.mlw

   1
   2 (**
   3 {1 VerifyThis @ ETAPS 2021 competition
   4    Challenge 1: Lexicographic Permutations}
   5    See https://www.pm.inf.ethz.ch/research/verifythis.html
   6
   7    Authors:
   8    - Quentin Garchery (Université Paris-Saclay)
   9    - Xavier Denis (Université Paris-Saclay)
  10 *)
  11
  12
  13 module ArrayListConversions
  14    use int.Int
  15    use array.Array
  16    use export array.ArrayEq
  17    use list.List as L
  18    use list.Nth
  19    use list.Length as L
  20    use option.Option
  21
  22
  23 let rec function to_list_from (i : int) (a : array int) : L.list int
  24     variant { length a - i }
  25     requires { 0 <= i <= length a }
  26     ensures { L.length result = length a - i }
  27     ensures { forall k. 0 <= k < length a - i -> nth k result = Some a[k+i] }
  28     =
  29     if i = length a then L.Nil else L.Cons a[i] (to_list_from (i+1) a)
  30
  31 let function to_list a = to_list_from 0 a
  32
  33 let lemma to_list_array_eq (a1 a2 : array int) : unit
  34     requires { array_eq a1 a2 }
  35     ensures { to_list a1 = to_list a2 }
  36     =
  37     let rec lemma to_list_array_eq_from (a1 a2 : array int) (i : int) : unit
  38         variant { length a1 - i }
  39         requires { 0 <= i <= length a1}
  40         requires { array_eq a1 a2 }
  41         ensures { to_list_from i a1 = to_list_from i a2 }
  42         =
  43         if i < length a1 then to_list_array_eq_from a1 a2 (i+1) in
  44     to_list_array_eq_from a1 a2 0
  45
  46 let function of_list (l : L.list int) : array int
  47     ensures { length result = L.length l }
  48     ensures { forall k. 0 <= k < L.length l -> nth k l = Some result[k] }
  49     =
  50     let a = make (L.length l) 0 in
  51     let rec update_from l' i
  52         variant { l' }
  53         writes { a }
  54         requires { 0 <= i }
  55         requires { L.length l' = L.length l - i }
  56         requires { forall k. 0 <= k < L.length l' -> nth (k+i) l = nth k l' }
  57         ensures { forall k. i <= k < L.length l -> nth k l = Some a[k] }
  58         ensures { forall k. 0 <= k < i -> a[k] = old a[k] }
  59         =
  60         match l' with
  61         | L.Nil -> ()
  62         | L.Cons v t ->
  63           a[i] <- v;
  64           assert { forall k. 0 < k < L.length t ->
  65                    nth (k+i+1) l = nth k t
  66                    by nth ((k+1)+i) l = nth (k+1) l' };
  67           update_from t (i+1)
  68         end in
  69     update_from l 0;
  70     a
  71
  72 let rec lemma eq_nth (l1 l2 : L.list 'a)
  73     requires { L.length l1 = L.length l2 }
  74     requires { forall k. 0 <= k < L.length l1 -> nth k l1 = nth k l2 }
  75     ensures { l1 = l2 }
  76     =
  77     match l1, l2 with
  78     | L.Cons a1 t1, L.Cons a2 t2 ->
  79       assert { a1 = a2 && L.length t1 = L.length t2 };
  80       assert { forall k. 0 <= k < L.length t1 ->
  81                nth k t1 = nth k t2
  82                by nth (k+1) l1 = nth (k+1) l2 };
  83       eq_nth t1 t2
  84     | L.Nil, L.Nil -> ()
  85     | _ -> assert {false}; ()
  86     end
  87
  88
  89 lemma of_to_list : forall a. array_eq (of_list (to_list a)) a
  90
  91 lemma to_of_list : forall l. to_list (of_list l) = l
  92
  93 meta remove_prop axiom eq_nth
  94
  95 end
  96
  97 module BoxedIntArrays
  98 use int.Int
  99 use int.Abs
 100 use int.MinMax
 101 use int.Power
 102 use array.Array
 103 use array.ArrayPermut
 104
 105 predicate boxed (u : int) (a : array int) =
 106    forall i. 0 <= i < length a -> 2 * abs a[i] < u
 107
 108 lemma boxed_permut : forall a a' u.
 109       boxed u a ->
 110       permut_all a a' ->
 111       boxed u a'
 112
 113 let function greater a
 114     ensures { result >= 0 }
 115     ensures { forall i. 0 <= i < length a -> 2 * abs a[i] < result }
 116     =
 117     let rec function great a l
 118         variant { length a - l }
 119         requires { 0 <= l <= length a }
 120         ensures { result >= 0 }
 121         ensures { forall i. l <= i < length a -> 2 * abs a[i] < result }
 122         =
 123         if l = length a then 0
 124         else let r = great a (l+1) in
 125              max r (2 * abs a[l] + 1) in
 126     great a 0
 127
 128 lemma boxed_greater : forall a.
 129       boxed (greater a) a
 130
 131 let function maxi base (a : array int)
 132     requires { boxed base a }
 133     =
 134     power base (length a)
 135
 136 end
 137
 138 module Permut
 139
 140 use int.Int
 141 use array.Array
 142 use array.ArrayPermut
 143 use array.ArrayExchange
 144 use array.ArrayEq
 145
 146 use array.IntArraySorted
 147 clone array.Sorted as Decr with type elt = int, predicate le = (>=)
 148
 149 predicate le (a1 a2 : array int) =
 150    length a1 = length a2 &&
 151    exists i. 0 <= i <= length a1 &&
 152    (forall j. 0 <= j < i -> a1[j] = a2[j])
 153    && (i < length a1 -> a1[i] < a2[i])
 154
 155 predicate lt (a1 a2 : array int) =
 156    le a1 a2 && not array_eq a1 a2
 157
 158 let rec function find_eq (a1 a2 : array int) (i : int) : int
 159     variant { length a1 - i }
 160     requires { length a1 = length a2 }
 161     requires { 0 <= i <= length a1 }
 162     requires { array_eq_sub a1 a2 0 i }
 163     ensures { 0 <= result <= length a1 }
 164     ensures { array_eq_sub a1 a2 0 result }
 165     ensures { result < length a1 -> a1[result] <> a2[result] }
 166     =
 167     if i = length a1 || a1[i] <> a2[i] then i
 168     else find_eq a1 a2 (i+1)
 169
 170 lemma lt_trans : forall a1 a2 a3 : array int.
 171       lt a1 a2 -> lt a2 a3 -> lt a1 a3
 172       by let i = find_eq a1 a2 0 in
 173          let j = find_eq a2 a3 0 in
 174          i < length a1 && j < length a1
 175          so i <= j -> array_eq_sub a1 a3 0 i && a1[i] < a3[i]
 176          so j < i -> array_eq_sub a1 a3 0 j && a1[j] < a3[j]
 177
 178 let function find_le a1 a2
 179     ensures { result <-> le a1 a2 }
 180     =
 181     length a1 = length a2 &&
 182     let i = find_eq a1 a2 0 in
 183     i = length a1 || a1[i] < a2[i]
 184
 185 lemma eq_le_compat : forall a1 a2 b1 b2 : array int.
 186       array_eq a1 b1 -> array_eq a2 b2 ->
 187       le a1 a2 -> le b1 b2
 188       by let i = find_eq a1 a2 0 in
 189          array_eq_sub b1 b2 0 i &&
 190          i < length a1 ->
 191          b1[i] <= b2[i]
 192
 193 lemma eq_lt_compat : forall a1 a2 b1 b2 : array int.
 194       array_eq a1 b1 -> array_eq a2 b2 ->
 195       lt a1 a2 -> lt b1 b2
 196
 197 lemma le_or_lt : forall a1 a2 : array int.
 198       length a1 = length a2 ->
 199       le a1 a2 \/ lt a2 a1
 200       by not le a1 a2 ->
 201          let i = find_eq a1 a2 0 in
 202          i < length a1 && a1[i] > a2[i]
 203          && array_eq_sub a1 a2 0 i
 204
 205 lemma lt_not_le : forall a1 a2 : array int.
 206       lt a1 a2 -> not le a2 a1
 207       by let i = find_eq a1 a2 0 in
 208          i < length a1 && a1[i] < a2[i]
 209          && array_eq_sub a1 a2 0 i
 210
 211 let lemma eq_sub_permut (a1 a2 : array int) (u : int)
 212     requires { permut_all a1 a2 }
 213     requires { array_eq_sub a1 a2 0 u }
 214     ensures { permut_sub a1 a2 u (length a1) }
 215     =
 216     let rec lemma eq_sub_permut_ind (a1 a2 : array int) (i1 i2 i3 : int)
 217         variant { i2 - i1 }
 218         requires { i1 <= i2 <= i3 }
 219         requires { permut_sub a1 a2 i1 i3 }
 220         requires { array_eq_sub a1 a2 i1 i2 }
 221         ensures { permut_sub a1 a2 i2 i3 }
 222         =
 223         if i1 < i2 then
 224         eq_sub_permut_ind a1 a2 (i1+1) i2 i3 in
 225     eq_sub_permut_ind a1 a2 0 u (length a1)
 226
 227
 228 lemma le_permut_sorted : forall a1 a2 i.
 229       length a1 = length a2 ->
 230       permut_sub a1 a2 i (length a1) ->
 231       sorted_sub a1 i (length a1) ->
 232       le a1 a2
 233       by let i' = find_eq a1 a2 0 in
 234          i' >= i
 235          so i' < length a1 -> permut_sub a1 a2 i' (length a1)
 236          so a1[i'] <= a2[i']
 237
 238 lemma le_permut_decr_sorted : forall a1 a2 i.
 239       length a1 = length a2 ->
 240       permut_sub a1 a2 i (length a1) ->
 241       Decr.sorted_sub a1 i (length a1) ->
 242       le a2 a1
 243       by let i' = find_eq a1 a2 0 in
 244          i' >= i
 245          so i' < length a1 -> permut_sub a1 a2 i' (length a1)
 246          so a1[i'] >= a2[i']
 247
 248 let next (a : array int)
 249     writes { a }
 250     ensures { permut_all a (old a) }
 251     ensures { not result -> a = old a &&
 252               forall a'. permut_all a a' -> le a a' -> array_eq a a'
 253               by Decr.sorted a }
 254     ensures { result ->
 255               lt (old a) a &&
 256               forall a'. permut_all (old a) a' ->
 257               lt (old a) a' -> le a a' }
 258     =
 259     let ref i = length a - 1 in
 260     while (i > 0 && a[i-1] >= a[i]) do
 261           variant { i }
 262           invariant { i <= length a - 1}
 263           invariant { Decr.sorted_sub a i (length a) }
 264           i <- i-1
 265     done;
 266     if i <= 0 then false else
 267     begin
 268     let ref j = length a - 1 in
 269     while (a[j] <= a[i-1]) do
 270           variant { j }
 271           invariant { i <= j <= length a - 1 }
 272           invariant { forall k. j < k < length a -> a[k] <= a[i-1] }
 273           j <- j-1
 274     done;
 275
 276     assert { a[j] > a[i-1] };
 277     assert { forall k. i <= k < length a -> a[k] > a[i-1] -> a[k] >= a[j] };
 278     let ghost i0 = i in
 279
 280     let ref temp = a[i-1] in
 281     a[i-1] <- a[j];
 282     a[j] <- temp;
 283     assert { exchange a (old a) (i-1) j };
 284     j <- length a - 1;
 285
 286     label L in
 287     while (i<j) do
 288           variant { j-i }
 289           invariant { i0 <= i < length a }
 290           invariant { i0 <= j < length a }
 291           invariant { permut_all a (a at L) }
 292           invariant { array_eq_sub a (a at L) 0 i0 }
 293           invariant { forall k1 k2. i0 <= k1 < k2 < i -> a[k1] <= a[k2] }
 294           invariant { forall k1 k2. i <= k1 < k2 < j+1 -> a[k1] >= a[k2] }
 295           invariant { forall k1 k2. j+1 <= k1 < k2 < length a -> a[k1] <= a[k2] }
 296           invariant { forall k1 k2. i0 <= k1 < i -> i <= k2 <= j ->
 297                       a[k1] <= a[k2] }
 298           invariant { forall k1 k2. i <= k1 <=j -> j < k2 < length a ->
 299                       a[k1] <= a[k2] }
 300           invariant { forall k1 k2. i0 <= k1 < i -> j < k2 < length a ->
 301                       a[k1] <= a[k2] }
 302           label StartLoop in
 303           temp <- a[i];
 304           a[i] <- a[j];
 305           a[j] <- temp;
 306           assert { exchange a (a at StartLoop) i j };
 307           i <- i+1;
 308           j <- j-1
 309     done;
 310     assert { sorted_sub a i0 (length a) };
 311     assert { forall a'. permut_all (old a) a' ->
 312               lt (old a) a' -> le a a'
 313               by let i = find_eq (old a) a' 0 in
 314                  if i = length a
 315                  then array_eq (old a) a' so le a a'
 316                  else if i < i0-1
 317                  then a'[i] > (old a)[i] so le a a'
 318                  else if i > i0-1
 319                  then a'[i0-1] = (old a)[i0-1] < a[i0-1] so false
 320                  else i = i0-1
 321                  so if a'[i0-1] <> a[i0-1]
 322                     then (old a)[i0-1] < a'[i0-1]
 323                          so permut_sub (old a) a' (i0 -1) (length a)
 324                          so a[i0-1] <= a'[i0-1]
 325                          so le a a'
 326                     else array_eq_sub a a' 0 (i0-1)
 327                          so array_eq_sub a a' 0 i0
 328                          so permut_sub a a' i0 (length a)
 329                          so le a a' };
 330     true
 331     end
 332
 333 use queue.Queue as Queue
 334 use list.List as L
 335 use int.Abs
 336 use int.Power
 337
 338 use BoxedIntArrays
 339
 340 val sort (a : array int) : unit
 341     writes { a }
 342     ensures { permut_all a (old a) }
 343     ensures { sorted a }
 344
 345 let rec function as_num base a i
 346     variant { length a - i }
 347     requires { boxed base a }
 348     requires { 0 <= i <= length a }
 349     ensures { 2 * abs result < power base (length a - i) }
 350     =
 351     if i = length a then 0
 352     else begin
 353     let rest = as_num base a (i+1) in
 354     assert { 2 * abs (a[i] * power base (length a - 1 - i) + rest) <=
 355              2 * abs a[i] * power base (length a - 1 - i) + 2 * abs rest <
 356              (2 * abs a[i] + 1) * power base (length a - 1 - i) <=
 357              base * power base (length a - 1 - i) <=
 358              power base (length a - i)
 359              by (forall x y : int. x >= 0 -> y >= 0 -> x * y >= 0)
 360              so forall x y z : int. x <= y -> z >= 0 -> x * z <= y * z
 361                 by (y - x) * z >= 0 };
 362     a[i] * power base (length a - 1 - i) + rest end
 363
 364 let function as_number base a
 365     requires { boxed base a }
 366     ensures { abs result <= maxi base a }
 367     =
 368     as_num base a 0
 369
 370 let rec lemma as_number_ind (a a' : array int) (base i j : int)
 371     variant { j - i }
 372     requires { 0 <= i <= j < length a }
 373     requires { boxed base a }
 374     requires { boxed base a' }
 375     requires { array_eq_sub a a' 0 j }
 376     requires { a[j] < a'[j] }
 377     ensures { as_num base a i < as_num base a' i }
 378     =
 379     if i < j then (assert { a[i] = a'[i] }; as_number_ind a a' base (i+1) j) else
 380     assert { as_num base a i = a[i] * power base (length a - 1 - i) +
 381                                as_num base a (i+1) /\
 382              as_num base a' i = a'[i] * power base (length a - 1 - i) +
 383                                 as_num base a' (i+1) /\
 384              2 * (as_num base a (i+1) - as_num base a' (i+1)) <=
 385              2 * abs (as_num base a (i+1)) + 2 * abs (as_num base a' (i+1)) <
 386              2 * power base (length a - 1 - i) <=
 387              2 * (a'[i] - a[i]) * power base (length a - 1 - i) }
 388
 389 let lemma as_number_strict a a' base
 390     requires { length a = length a'}
 391     requires { boxed base a }
 392     requires { boxed base a' }
 393     requires { lt a a' }
 394     ensures { as_number base a < as_number base a' }
 395     =
 396     let n = length a in
 397     for i = 0 to n - 1 do
 398         invariant { array_eq_sub a a' 0 i }
 399         if a[i] <> a'[i] then (as_number_ind a a' base 0 i; return)
 400     done
 401
 402 use seq.Seq
 403 use seq.Mem
 404 use ArrayListConversions
 405
 406 lemma seq_snoc_mem : forall s : seq 'a, x y.
 407       mem x (snoc s y) <-> mem x s \/ x = y
 408
 409 let permut (a : Array.array int) : Queue.t (L.list int)
 410     ensures { forall i1 i2. 0 <= i1 < i2 < length result ->
 411               lt (of_list result[i1]) (of_list result[i2]) }
 412     ensures { forall a'. permut_all a a' -> mem (to_list a') result }
 413     =
 414     let ghost base = greater a in
 415     let res = Queue.create () in
 416     if length a = 0 then
 417     begin Queue.push L.Nil res;
 418           assert { forall a'. permut_all a a' -> mem (to_list a') res };
 419           res end
 420     else begin
 421     sort a;
 422     let ref cont = true in
 423     let ghost ref cont_int = 1 in
 424     assert { forall a'. permut_all a' a -> lt a' a -> false
 425              by permut_sub a a' 0 (Array.length a) };
 426     while cont do
 427           invariant { permut_all a (old a) }
 428           invariant { boxed base a }
 429           invariant { cont_int = 1 <-> cont }
 430           invariant { cont -> forall a'. permut_all a' a -> lt a' a ->
 431                       mem (to_list a') res }
 432           invariant { not cont -> forall a'. permut_all a' a -> le a' a ->
 433                       mem (to_list a') res}
 434           invariant { cont -> forall a'. mem (to_list a') res -> lt a' a }
 435           invariant { not cont -> forall a'. permut_all a a' -> le a a' ->
 436                       array_eq a a' }
 437           invariant { forall i1 i2. 0 <= i1 < i2 < length res ->
 438                       lt (of_list res[i1]) (of_list res[i2]) }
 439           variant { cont_int, maxi base a - as_number base a }
 440           label SL in
 441           Queue.push (to_list a) res;
 442           cont <- next a;
 443           if cont then begin
 444           assert { forall a'. permut_all a' a -> lt a' a ->
 445                    mem (to_list a') res
 446                    by not le a a'
 447                    so le a' (a at SL) };
 448           assert { forall a'. mem (to_list a') res -> lt a' a
 449                    by le a a' -> lt (a at SL) a'
 450                       so not mem (to_list a') (res at SL)
 451                       so to_list a' = to_list (a at SL)
 452                       so lt a' a };
 453           () end
 454           else cont_int <- 0;
 455           assert { boxed base a };
 456           assert { forall i1 i2. 0 <= i1 < i2 < length res ->
 457                       lt (of_list res[i1]) (of_list res[i2])
 458                       by i2 = length res - 1 ->
 459                          array_eq (of_list res[i2]) (a at SL)
 460                          && lt (of_list res[i1]) (a at SL)};
 461
 462     done;
 463     res
 464     end
 465
 466 end