examples/verifythis_2021_shearsort_modified.mlw

   1
   2 (**
   3 {1 VerifyThis @ ETAPS 2021 competition
   4    Challenge 3: Shearsort}
   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    - sequential code only (no parallelism in Why3)
  14
  15    - termination verified under some assumptions over the number of
  16      inversions in functions `sort_row` and `sort_column`
  17
  18    - *CHANGE IN CODE*
  19
  20      We were not able to show that ceil(log(n))+1 steps suffices.
  21
  22      Therefore, we replaced the `repeat` loop infinite loop from which
  23      we exit as soon as none of the calls to `sort_column` makes a
  24      change to the matrix.
  25
  26      We argue that this does not increase the complexity. Indeed, it can be
  27      proved, independently, that the loops will never execute more than
  28      ceil(log(n))+1 steps. Actually, our change even *improves* the
  29      performance of the code, as we may perform fewer steps in some cases
  30      (e.g. when the matrix is already snake-sorted).
  31
  32 *)
  33
  34 use int.Int
  35 use int.ComputerDivision
  36 use matrix.Matrix
  37 use map.Occ
  38 use int.NumOf
  39 use int.Sum
  40
  41 meta coercion function elts
  42
  43 (*** SPECIFICATION STARTS HERE ********************************************)
  44
  45 function mocc (x: int) (m: matrix int) : int =
  46   sum (fun i -> occ x (m i) 0 m.columns) 0 m.rows
  47
  48 predicate lt (i j k l: int)
  49 = i < k \/
  50   i = k /\ if mod i 2 = 0 then j < l else l < j
  51
  52 predicate snake_order (m: matrix int)
  53 = let rw = m.rows in
  54   let cl = m.columns in
  55   forall i j k l.
  56   0 <= i < rw -> 0 <= j < cl ->
  57   0 <= k < rw -> 0 <= l < cl ->
  58   lt i j k l -> m i j <= m k l
  59
  60 function inversions (m: matrix int) : int
  61 = sum (fun i ->
  62     sum (fun j ->
  63       sum (fun k ->
  64            numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns)
  65         0 m.rows)
  66       0 m.columns)
  67     0 m.rows
  68
  69 (*** SPECIFICATION STOPS HERE **********************************************)
  70 (*** beyond this point, the only thing you need to read are the contracts
  71      for functions `sort_row`, `sort_column`, `shearsort` below *)
  72
  73 let lemma inv_nonneg (m: matrix int)
  74   ensures { 0 <= inversions m }
  75 = let zero = pure { fun (_:int) -> 0 } in
  76   assert { forall i j k.
  77     zero k <= numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns };
  78   assert { forall i j.
  79     zero j <= sum (fun k ->
  80            numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns)
  81         0 m.rows };
  82   assert { forall i.
  83     zero i <= sum (fun j -> sum (fun k ->
  84            numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns)
  85         0 m.rows)
  86       0 m.columns };
  87   assert { 0 = sum zero 0 m.rows <= inversions m };
  88   ()
  89
  90 predicate sorted_row (m: matrix int) (row: int) (ascending: bool) =
  91   0 <= row < m.rows /\
  92   if ascending then
  93                forall j l. 0 <= j <= l < m.columns -> m row j <= m row l
  94              else
  95                forall j l. 0 <= j <= l < m.columns -> m row j >= m row l
  96
  97 val sort_row (m: matrix int) (row: int) (ascending: bool) : unit
  98   requires { 0 <= row < m.rows }
  99   writes   { m }
 100   ensures  { (* frame *)
 101              forall i j. 0 <= i < m.rows ->  0 <= j < m.columns ->
 102                i <> row -> m i j = old m i j }
 103   ensures  { forall x. mocc x m = mocc x (old m) }
 104   ensures  { sorted_row m row ascending }
 105   ensures  { inversions m <= old inversions m }
 106
 107 predicate sorted_column (m: matrix int) (column: int) =
 108   0 <= column < m.columns /\
 109   forall i k. 0 <= i <= k < m.rows -> m i column <= m k column
 110
 111 val sort_column (m: matrix int) (column: int) : (nochange: bool)
 112   requires { 0 <= column < m.columns }
 113   writes   { m }
 114   ensures  { (* frame *)
 115              forall i j. 0 <= i < m.rows -> 0 <= j < m.columns ->
 116                j <> column -> m i j = old m i j }
 117   ensures  { forall x. mocc x m = mocc x (old m) }
 118   ensures  { nochange -> forall i. 0 <= i < m.rows ->
 119                m i column = old m i column }
 120   ensures  { sorted_column m column }
 121   ensures  { inversions m <= old inversions m }
 122   ensures  { not nochange -> inversions m < old inversions m }
 123
 124 let shearsort (n: int) (m: matrix int) : unit
 125   requires { m.rows = m.columns = n }
 126   writes   { m }
 127   (* TASK 3 *)
 128   ensures  { snake_order m }
 129   (* TASK 2 *)
 130   ensures  { forall x. mocc x m = mocc x (old m) }
 131 = label Init in
 132   while true do (* <-- CHANGE instead of ceil(log(n))+1 steps *)
 133     invariant  { forall x. mocc x m = mocc x (old m) }
 134     variant    { inversions m }
 135     label L1 in
 136     for i = 0 to n - 1 do
 137       invariant  { forall k. 0 <= k < i -> sorted_row m k (mod k 2 = 0) }
 138       invariant  { forall x. mocc x m = mocc x (old m) }
 139       invariant  { inversions m <= (inversions m at L1) }
 140       sort_row m i (mod i 2 = 0)
 141     done;
 142     label L2 in
 143     let ref nochange = true in
 144     for j = 0 to n - 1 do
 145       invariant  { nochange ->
 146                    forall i j. 0 <= i < m.rows -> 0 <= j < m.columns ->
 147                      m i j = (m i j at L2) }
 148       invariant  { forall l. 0 <= l < j -> sorted_column m l }
 149       invariant  { forall x. mocc x m = mocc x (old m) }
 150       invariant  { inversions m <= (inversions m at L2) }
 151       invariant  { not nochange -> inversions m < (inversions m at L2) }
 152       let nch = sort_column m j in
 153       if not nch then nochange <- false
 154     done;
 155     if nochange then break
 156   done;
 157   let lemma ordered (i j k l: int)
 158     requires { 0 <= i < n } requires { 0 <= j < n }
 159     requires { 0 <= k < n } requires { 0 <= l < n }
 160     requires { lt i j k l } ensures  { m i j <= m k l }
 161   = if i = k then return;
 162     assert { sorted_column m j };
 163     assert { sorted_column m l };
 164     if j <= l then (
 165       if mod i 2 = 0 then
 166         assert { m i j <= m i l <= m k l }
 167       else (
 168         assert { mod (i+1) 2 = 0 };
 169         assert { sorted_row m (i+1) true };
 170         assert { m i j <= m (i+1) j <= m (i+1) l <= m k l }
 171       )
 172     )
 173   in
 174   ()
 175
 176 (* Notes
 177
 178 The verification tasks for shearsort are:
 179
 180 1. Verify that shearsort terminates, and is memory safe.
 181    PARTIAL: memory safety DONE (enforced by Why3)
 182             termination using hypotheses over number of inversions
 183
 184 2. Verify that shearsort permutes the input matrix.
 185    DONE
 186
 187 3. Verify that shearsort sorts the matrix in a snake-like manner.
 188    DONE
 189
 190 4. Verify that (parallel) shearsort satisfies the same specification
 191    as sequenti al shearsort, in which all parallel for-loops are replaced
 192    by sequential ones.
 193
 194 5. Verify that shearsort and alternative-shearsort satisfy the same
 195    specification.
 196
 197 6. Extra: give implementations to sort-row, sort-column and transpose,
 198    and verify these as well.
 199
 200 *)