examples/verifythis_2021_lexicographic_permutations_1.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    - Jean-Christophe Filliâtre (CNRS)
   9    - Andrei Paskevich (Univ. Paris-Saclay)
  10
  11    Summary:
  12
  13    - all tasks verified
  14
  15    - only one change in the code, due to the absence of do/while loop in Why3
  16
  17    - main idea for proving termination: show that the set of all permutations
  18      is finite, by building a finite over-approximation of that set
  19      (see function `all_permutations` below)
  20
  21 *)
  22
  23 use int.Int
  24 use import array.Array as A
  25 use import seq.Seq as S
  26 use int.NumOf as N
  27
  28 (*** SPECIFICATION STARTS HERE ********************************************)
  29
  30 type elt = int
  31
  32 type permutation = seq elt
  33
  34 (* lexicographic order on permutations *)
  35 predicate lt (p q: permutation) =
  36   length p = length q > 0 /\
  37   exists i. 0 <= i < length p /\
  38     (forall j. 0 <= j < i -> p[j] = q[j]) /\
  39     p[i] < q[i]
  40
  41 (* lt is a total order *)
  42
  43 let lemma lt_trans (p q r: permutation)
  44   requires { lt p q } requires { lt q r } ensures { lt p r }
  45 = ()
  46
  47 let lemma lt_asym (p q: permutation)
  48   requires { lt p q } requires { lt q p } ensures { false }
  49 = ()
  50
  51 let lemma lt_total (p q: permutation) : bool
  52   requires { length p = length q }
  53   ensures  { if result then lt p q else p = q \/ lt q p }
  54 = let n = length p in
  55   for i = 0 to n-1 do
  56     invariant { forall j. 0 <= j < i -> p[j] = q[j] }
  57     if p[i] < q[i] then return true;
  58     if p[i] > q[i] then return false;
  59   done;
  60   return false
  61
  62 (* number of occurrences in a (sub-)sequence *)
  63
  64 function iseq (x: 'a) (s: seq 'a) : int->bool =
  65   fun i -> s[i] = x
  66
  67 function occ (x: 'a) (s: seq 'a) (l u: int) : int =
  68   N.numof (iseq x s) l u
  69
  70 function occ_all (x: 'a) (s: seq 'a) : int =
  71   occ x s 0 (length s)
  72
  73 predicate is_permutation_of (p a: seq elt) =
  74   length p = length a /\
  75   forall x. occ_all x p = occ_all x a
  76
  77 (*** SPECIFICATION STOPS HERE **********************************************)
  78 (*** beyond this point, the only thing you need to read are the contracts
  79      for functions `next` and `permut` *)
  80
  81 predicate descending (s: seq elt) (lo hi: int)
  82 = 0 <= lo <= hi <= length s /\
  83   forall i j. lo <= i <= j < hi -> s[i] >= s[j]
  84
  85 predicate ascending (s: seq elt) (lo hi: int)
  86 = 0 <= lo <= hi <= length s /\
  87   forall i j. lo <= i <= j < hi -> s[i] <= s[j]
  88
  89 let function to_seq (a: array elt) : (s: seq elt)
  90   ensures { length s = A.length a }
  91   ensures { forall i. 0 <= i < length s -> s[i] = A.(a[i]) }
  92 = let ref s = empty in
  93   for k = 0 to A.length a - 1 do
  94     invariant { length s = k }
  95     invariant { forall i. 0 <= i < k -> s[i] = A.(a[i]) }
  96     s <- snoc s A.(a[k])
  97   done;
  98   return s
  99
 100 lemma is_permutation_of_refl:
 101   forall p. is_permutation_of p p
 102 lemma is_permutation_of_sym :
 103   forall p q. is_permutation_of p q -> is_permutation_of q p
 104 lemma is_permutation_of_tran:
 105   forall p q r. is_permutation_of p q -> is_permutation_of q r ->
 106                 is_permutation_of p r
 107
 108 let lemma occ_id (s1 s2: seq elt) (l u: int)
 109   requires { 0 <= l <= u <= length s1 = length s2 }
 110   requires { forall i. l <= i < u -> s1[i] = s2[i] }
 111   ensures  { forall x. occ x s1 l u = occ x s2 l u }
 112 = ()
 113
 114 let lemma occ_split (s: seq elt) (l mid u: int)
 115   requires { 0 <= l <= mid <= u <= length s }
 116   ensures  { forall x. occ x s l u = occ x s l mid + occ x s mid u }
 117 = ()
 118
 119 let lemma occ_at (s: seq elt) (l i u: int)
 120   requires { 0 <= l <= i < u <= length s }
 121   ensures  { forall x. occ x s l u =
 122                occ x s l i + (if x = s[i] then 1 else 0) + occ x s (i+1) u }
 123 = occ_split s l i u;
 124   occ_split s i (i+1) u
 125
 126 let lemma occ_none (v: elt) (s: seq elt) (l u: int)
 127   requires { 0 <= l <= u <= length s }
 128   requires { forall k. l <= k < u -> s[k] <> v }
 129   ensures  { occ v s l u = 0 }
 130 = ()
 131
 132 let lemma descending_is_last (s p: seq elt)
 133   requires { descending s 0 (length s) }
 134   requires { is_permutation_of p s }
 135   ensures  { not (lt s p) }
 136 = let n = length s in
 137   for i = 0 to n-1 do
 138     invariant { forall j. 0 <= j < i -> s[j] = p[j] }
 139     if s[i] > p[i] then return;
 140     if s[i] < p[i] then (
 141       let y = p[i] in
 142       occ_at s 0 i n;
 143       occ_at p 0 i n;
 144       assert { occ y s (i+1) n > 0 };
 145       assert { exists k. i < k < n /\ s[k] = y };
 146       return
 147     );
 148   done
 149
 150 let lemma ascending_is_first (s p: seq elt)
 151   requires { ascending s 0 (length s) }
 152   requires { is_permutation_of p s }
 153   ensures  { not (lt p s) }
 154 = let n = length s in
 155   for i = 0 to n-1 do
 156     invariant { forall j. 0 <= j < i -> s[j] = p[j] }
 157     if s[i] < p[i] then return;
 158     if s[i] > p[i] then (
 159       let y = p[i] in
 160       occ_at s 0 i n;
 161       occ_at p 0 i n;
 162       assert { occ y s (i+1) n > 0 };
 163       assert { exists k. i < k < n /\ s[k] = y };
 164       return
 165     );
 166   done
 167
 168 let swap (a: array elt) (i j: int)
 169   requires  { 0 <= i < A.length a }
 170   requires  { 0 <= j < A.length a }
 171   ensures   { A.(a[i] = old a[j]) }
 172   ensures   { A.(a[j] = old a[i]) }
 173   ensures   { forall k. 0 <= k < A.length a ->
 174                 k <> i -> k <> j -> A.(a[k] = old a[k]) }
 175   ensures   { is_permutation_of (to_seq a) (to_seq (old a)) }
 176 = A.(
 177   let temp = a[i] in
 178   a[i] <- a[j];
 179   a[j] <- temp
 180   );
 181   let ghost s1 = pure { to_seq (old a) } in
 182   let ghost s2 = pure { to_seq      a  } in
 183   let ghost n = A.length a in
 184   if i <= j then
 185     if i = j then ()
 186     else (occ_id s1 s2 0 i;
 187           occ_at s1 0 i n; occ_at s2 0 i n;
 188           occ_at s1 (i+1) j n; occ_at s2 (i+1) j n;
 189           occ_id s1 s2 (i+1) j;
 190           occ_id s1 s2 (j+1) n)
 191   else (occ_id s1 s2 0 j;
 192           occ_at s1 0 j n; occ_at s2 0 j n;
 193           occ_at s1 (j+1) i n; occ_at s2 (j+1) i n;
 194           occ_id s1 s2 (j+1) i;
 195           occ_id s1 s2 (i+1) n);
 196   ()
 197
 198 let next (ghost a0: seq elt) (a: array elt) : bool
 199   (* TASK 1 enforced by Why3 *)
 200   (* TASK 2 ensured by absence of `diverges` clause *)
 201   requires { A.length a = length a0 }
 202   requires { is_permutation_of (to_seq a) a0 }
 203   (* TASK 3 *)
 204   ensures  { is_permutation_of (to_seq a) a0 }
 205   (* TASK 4 *)
 206   ensures  { not result -> forall i. 0 <= i < A.length a -> A.(a[i] = old a[i]) }
 207   ensures  { not result -> forall p. is_permutation_of p a0 ->
 208                             not (lt (to_seq a) p) }
 209   (* TASK 5 *)
 210   ensures  { result -> lt (to_seq (old a)) (to_seq a) }
 211   ensures  { result -> forall p. is_permutation_of p a0 ->
 212                          not (lt (to_seq (old a)) p /\ lt p (to_seq a)) }
 213 = label Init in
 214   let n = A.length a in
 215   let ref i = n - 1 in
 216   while i > 0 && A.(a[i-1] >= a[i]) do
 217     invariant { -1 <= i < n } variant { i }
 218     invariant { i = -1 /\ n = 0 \/ i >= 0 /\ descending (to_seq a) i n }
 219     i <- i - 1
 220   done;
 221   if i <= 0 then return false;
 222   let ghost i0 = i - 1 in
 223   let ghost x = A.(a[i0]) in
 224   let ref j = n - 1 in
 225   while A.(a[j] <= a[i-1]) do
 226     invariant { i <= j < n } variant { j }
 227     invariant { forall k. j < k < n -> A.(a[k]) <= x }
 228     j <- j - 1
 229   done;
 230   let ghost z = A.(a[j]) in
 231   swap a (i-1) j;
 232   assert { is_permutation_of (to_seq a) a0 };
 233   assert { lt (to_seq (old a)) (to_seq a) };
 234   j <- n - 1;
 235   label L in
 236   while i < j do
 237     invariant { i0 < i && i0 < j < n } variant { j - i }
 238     invariant { is_permutation_of (to_seq a) a0 }
 239     invariant { forall k. 0 <= k < i0 -> A.(a[k] = a[k] at Init) }
 240     invariant { A.(a[i0] = z) }
 241     invariant { i - i0 = n - j }
 242     invariant { forall k. i <= k <= j -> A.(a[k] = a[k] at L) }
 243     invariant { forall k. 0 < k < i-i0 -> A.(a[i0+k] = a[n-k] at L)
 244                                         /\ A.(a[n-k] = a[i0+k] at L) }
 245     swap a i j;
 246     i <- i + 1;
 247     j <- j - 1
 248   done;
 249   assert { forall k. i0 < k < n -> A.(a[k] = a[n - (k - i0)] at L) };
 250   assert { ascending (to_seq a) (i0+1) n };
 251   let lemma is_next (p: permutation)
 252     requires { is_permutation_of p a0 }
 253     requires { lt (to_seq (a at Init)) p }
 254     requires { lt p (to_seq a) }
 255     ensures  { false }
 256   = assert { forall k. 0 <= k < i0 -> p[k] = A.(a[k] at Init) };
 257     assert { x <= p[i0] <= z };
 258     let a1 = pure { to_seq (a at Init) } in
 259     let v = p[i0] in
 260     if v = x then (
 261       for l = i0+1 to n - 1 do
 262         invariant { forall k. i0+1 <= k < l -> p[k] = a1[k] }
 263         if p[l] <> a1[l] then (
 264           assert { a1[l] < p[l] };
 265           occ_id a1 p 0 l; occ_split a1 0 l n; occ_split p 0 l n;
 266           occ_at a1 0 l n; occ_at p 0 l n;
 267           assert { occ p[l] a1 l n = occ p[l] p l n > 0 };
 268           return;
 269         )
 270       done
 271     ) else if v = z then (
 272       let a2 = to_seq a in
 273       for l = i0+1 to n - 1 do
 274         invariant { forall k. i0+1 <= k < l -> p[k] = a2[k] }
 275         if p[l] <> a2[l] then (
 276           assert { is_permutation_of p a2 };
 277           assert { a2[l] > p[l] };
 278           occ_id a2 p 0 l; occ_split a2 0 l n; occ_split p 0 l n;
 279           occ_at a2 0 l n; occ_at p 0 l n;
 280           (* if l <= j0 then (occ_split a2 l j0 n; occ_split p 0 j0 n); *)
 281           assert { occ p[l] a2 l n = occ p[l] p l n };
 282           assert { occ p[l] p l n > 0 };
 283           assert { occ p[l] a2 (l+1) n > 0 };
 284           occ_none p[l] a2 (l+1) n;
 285           return;
 286         )
 287       done
 288     )
 289     else (
 290       occ_split p  0 i0 n;
 291       occ_split a1 0 i0 n;
 292       occ_id p a1 0 i0;
 293       assert { occ v p i0 n = occ v a1 i0 n > 0 };
 294       occ_none v a1 i0 n;
 295     )
 296   in
 297   return true
 298
 299 val sort (a: array elt) : unit
 300   writes  { a }
 301   ensures { forall i j. 0 <= i <= j < A.length a -> A.(a[i] <= a[j]) }
 302   ensures { is_permutation_of (to_seq a) (to_seq (old a)) }
 303 (* NOTE we could provide an implementation here,
 304         but this was not part of the tasks *)
 305
 306 use import set.Fset as FS
 307
 308 (* this is actually an over-approximation of the sets of all permutations
 309    of s, namely the set of all sequences of length |s| made with elements
 310    of s *)
 311 let ghost function
 312   all_permutations (s: permutation) : (all: fset permutation)
 313   ensures { forall p. is_permutation_of p s -> mem p all }
 314 = let n = length s in
 315   let rec enum (k: int) : fset permutation
 316     requires { 0 <= k <= n }
 317     ensures  { forall p.
 318                  length p = k /\ (forall i. 0 <= i < k -> occ_all p[i] s > 0)
 319                  -> mem p result }
 320     variant  { k }
 321   =
 322     if k = 0 then return FS.singleton empty;
 323     let now = enum (k - 1) in
 324     let ref acc = FS.empty in
 325     for j = 0 to n - 1 do
 326       invariant { forall p.
 327                  length p = k /\ (forall i. 0 <= i < k -> occ_all p[i] s > 0)
 328                  /\ occ p[0] s 0 j > 0
 329                  -> mem p acc }
 330       acc <- FS.union acc (FS.map (cons s[j]) now)
 331     done;
 332     return acc
 333   in
 334   let all = enum n in
 335   let lemma final (p: permutation) : unit
 336     requires { is_permutation_of p s } ensures { mem p all }
 337   = assert { forall i. 0 <= i < n -> occ_all p[i] s > 0
 338       by occ_all p[i] p = occ p[i] p 0 i + 1 + occ p[i] p (i+1) n > 0 };
 339     ()
 340   in
 341   return all
 342
 343 let permut (a: array elt) : seq permutation
 344   (* TASK 6 enforced by Why3 *)
 345   (* TASK 7 ensured by absence of `diverges` clause *)
 346   (* TASKS 8,9,10 *)
 347   ensures { (* result only contains permutation of a *)
 348             forall i. 0 <= i < length result ->
 349               is_permutation_of result[i] (to_seq (old a)) }
 350   ensures { (* result is sorted in strict ascending order *)
 351             forall i j. 0 <= i < j < length result -> lt result[i] result[j] }
 352   ensures { (* result contains any permutation of a *)
 353             forall p. is_permutation_of p (to_seq (old a)) ->
 354               exists i. 0 <= i < length result /\ result[i] = p }
 355 = let ghost a0 = to_seq a in
 356   let ghost all = all_permutations a0 in
 357   let ref result = empty in
 358   sort a;
 359   (* CHANGE: no do/while loop => unroll once *)
 360   result <- snoc result (to_seq a);
 361   let ghost ref last = to_seq a in
 362   let ghost ref sresult = FS.singleton (to_seq a) in
 363   while next a0 a do
 364     invariant { length result > 0 }
 365     invariant { is_permutation_of (to_seq a) a0 }
 366     invariant { forall i. 0 <= i < length result ->
 367                   is_permutation_of result[i] a0 }
 368     invariant { last = result[length result - 1] = to_seq a }
 369     invariant { is_permutation_of last a0 }
 370     invariant { forall i j. 0 <= i < j < length result ->
 371                   lt result[i] result[j] }
 372     invariant { forall p. is_permutation_of p a0 -> lt p last ->
 373                   exists i. 0 <= i < length result - 1 /\ result[i] = p }
 374     invariant { forall p. mem p sresult <->
 375                   exists i. 0 <= i < length result /\ result[i] = p }
 376     invariant { subset sresult all }
 377     variant   { cardinal all - cardinal sresult }
 378     result <- snoc result (to_seq a);
 379     last <- to_seq a;
 380     sresult <- FS.add (to_seq a) sresult
 381   done;
 382   return result
 383