examples/verifythis_2024_challenge1.mlw

   1
   2 (** {1 VerifyThis 2024, challenge 1, Smart Array Copy by Shuffled Subsegments}
   3
   4   See https://www.pm.inf.ethz.ch/research/verifythis.html
   5
   6   Team YYY: Jean-Christophe Filliâtre (CNRS)
   7
   8   Summary:
   9   - Smart Array Copy version 0 implemented and verified
  10   - Smart Array Copy version 1 implemented and verified
  11   - Smart Array Copy version 2 not implemented
  12 *)
  13
  14 use int.Int
  15 use int.EuclideanDivision
  16 use array.Array
  17
  18 (** Permutations
  19
  20   Two key ideas here:
  21   - A permutation is contained in a *prefix* of length `l`
  22     of some array `p`.
  23   - Function `permute` also returns the inverse permutation,
  24     as a ghost output.
  25  *)
  26
  27 predicate permutation (l: int) (p: array int) =
  28   0 <= l <= length p &&
  29   (forall i. 0 <= i < l -> 0 <= p[i] < l) &&
  30   (forall i j. 0 <= i < l -> 0 <= j < l -> i <> j -> p[i] <> p[j])
  31
  32 predicate permutation_pair (l: int) (p invp: array int) =
  33   permutation l p && permutation l invp &&
  34   (forall i. 0 <= i < l -> p[invp[i]] = i) &&
  35   (forall i. 0 <= i < l -> invp[p[i]] = i)
  36
  37 val permute (l: int) : (p: array int, ghost invp: array int)
  38   requires { l > 0 }
  39   ensures  { length p = length invp = l }
  40   ensures  { permutation_pair l p invp }
  41
  42 val function identity (l: int) : array int
  43   requires { l > 0 }
  44   ensures  { length result = l }
  45   ensures  { forall i. 0 <= i < l -> result[i] = i }
  46   ensures  { permutation_pair l result result }
  47
  48 (** The array elements belong to some uninterpreted type.
  49     (In particular, they won't be confused with array indices.) *)
  50 type elt
  51
  52 (** Shortcut predicates *)
  53 predicate valid_chunk (a: array elt) (ofs len: int) =
  54   0 <= ofs <= ofs+len <= length a
  55
  56 predicate copy (src dst: array elt) (ofs len: int) =
  57   valid_chunk src ofs len && length src = length dst &&
  58   forall i. ofs <= i < ofs+len -> dst[i] = src[i]
  59
  60 (** Helper lemma function: when all subsegments are copied,
  61     the whole segment is copied *)
  62 let lemma all_subsegments (start k l: int) (src dst: array elt)
  63   (sigma invsigma: array int)
  64   requires { k > 0 && l > 0 }
  65   requires { valid_chunk src start (k*l) }
  66   requires { length dst = length src }
  67   requires { forall j. 0 <= j < l ->
  68                copy src dst (start + sigma[j]*k) k }
  69   requires { permutation_pair l sigma invsigma }
  70   ensures  { copy src dst start (k*l) }
  71 = let m = k*l in
  72   assert { forall i. start <= i < start + m ->
  73     dst[i] = src[i]
  74     (* key idea here: Euclidean division + permutation inverse *)
  75     by let q = div (i - start) k in
  76        let r = mod (i - start) k in
  77        let j = invsigma[q] in
  78        i = start + q*k + r
  79     so i = start + sigma[j]*k + r
  80   }
  81
  82 (** Smart Array Copy version 0 *)
  83
  84 let smart_array_copy_0 (n k l q r: int) (src dst: array elt) : unit
  85   requires { length src = length dst = n > 0 }
  86   requires { k > 0 && l > 0 && q >= 0 && 0 <= r < k*l }
  87   requires { n = q * k*l + r }
  88   writes   { dst }
  89   ensures  { copy src dst 0 n }
  90 = let m = k*l in
  91   for s = 0 to q - 1 do
  92     invariant { copy src dst 0 (s*m) }
  93     let start = s*m in
  94     let sigma, invsigma = permute l in
  95     for j = 0 to l - 1 do
  96       invariant { copy src dst 0 (s*m) }
  97       invariant {
  98         forall j'. 0 <= j' < j -> copy src dst (start + sigma[j']*k) k }
  99       let startj = start + sigma[j]*k in
 100       for i = 0 to k - 1 do
 101         invariant { copy src dst 0 (s*m) }
 102         invariant {
 103           forall j'. 0 <= j' < j -> copy src dst (start + sigma[j']*k) k }
 104         invariant { copy src dst startj i }
 105         dst[startj + i] <- src[startj + i]
 106       done
 107     done;
 108     all_subsegments start k l src dst sigma invsigma
 109   done;
 110   let last = q*m in
 111   for i = 0 to r - 1 do
 112     invariant { copy src dst 0 (q*m) }
 113     invariant { copy src dst last i }
 114     dst[last + i] <- src[last + i]
 115   done
 116
 117 (** Smart Array Copy version 0, variant
 118
 119   This time we introduce a function `copy_chunk` that copies a chunk
 120   from `src` to `dst`, possibly at different offsets. Will be reused
 121   later in version 1. *)
 122
 123 predicate copy_to (src dst: array elt) (ofss ofsd len: int) =
 124   valid_chunk src ofss len && valid_chunk dst ofsd len && length src = length dst &&
 125   (forall i. 0 <= i < len -> dst[ofsd + i] = src[ofss + i]) &&
 126   (forall i. ofsd <= i < ofsd+len -> dst[i] = src[i + (ofss - ofsd)])
 127
 128 let copy_chunk (src dst: array elt) (ofss ofsd len: int) : unit
 129   requires { length src = length dst }
 130   requires { valid_chunk src ofss len }
 131   requires { valid_chunk dst ofsd len }
 132   writes   { dst }
 133   ensures  { copy_to src dst ofss ofsd len }
 134   (* frame *)
 135   ensures  { forall i. 0 <= i < ofsd -> dst[i] = (old dst)[i] }
 136   ensures  { forall i. ofsd+len <= i < length dst -> dst[i] = (old dst)[i] }
 137 = for i = 0 to len - 1 do
 138     invariant { copy_to src dst ofss ofsd i }
 139     invariant { forall i. 0 <= i < ofsd -> dst[i] = (old dst)[i] }
 140     invariant { forall i. ofsd+len <= i < length dst -> dst[i] = (old dst)[i] }
 141     dst[ofsd + i] <- src[ofss + i]
 142   done
 143
 144 (** Re-implementation of Smart Array Copy version 0 using `copy_chunk` *)
 145 let smart_array_copy_0b (n k l q r: int) (src dst: array elt) : unit
 146   requires { length src = length dst = n > 0 }
 147   requires { k > 0 && l > 0 && q >= 0 && 0 <= r < k*l }
 148   requires { n = q * k*l + r }
 149   writes   { dst }
 150   ensures  { copy src dst 0 n }
 151 = let m = k*l in
 152   for s = 0 to q - 1 do
 153     invariant { copy src dst 0 (s*m) }
 154     let start = s*m in
 155     let sigma, invsigma = permute l in
 156     for j = 0 to l - 1 do
 157       invariant { copy src dst 0 (s*m) }
 158       invariant {
 159         forall j'. 0 <= j' < j -> copy src dst (start + sigma[j']*k) k }
 160       let startj = start + sigma[j]*k in
 161       copy_chunk src dst startj startj k
 162     done;
 163     all_subsegments start k l src dst sigma invsigma
 164   done;
 165   let last = q*m in
 166   copy_chunk src dst last last r
 167
 168 (** Smart Array Copy version 1
 169
 170     The situation is as follows. We have already copied `s` segments,
 171     each of length `m = kl`, and we are currently copying the `l`
 172     subsegments of the next segment from `src` to `dst`.
 173
 174                        <------------segment s-------------->
 175                         sm   sigma[j]                      (s+1)m
 176     +------------------+-----------------------------------+-----------------+
 177 src |  already copied  |  ?  | ... |  ?  | done|  ?  | done|                 |
 178     +------------------+-----------------------------------+-----------------+
 179          ^   |                  |
 180         p|   |invp              +-----------------+
 181          |   V                                    V
 182     +------------------+-----------------------------------+-----------------+
 183 dst |  already copied  |     |     |     |     | ... |     |                 |
 184     +------------------+-----------------------------------+-----------------+
 185                                             tau[sigma[j]]
 186
 187     The arrays `p` and `invp` maintain the permutations between `src`
 188     and `dst` (`p` maps indices from `dst` to `src`, and `invp` in the
 189     other way back).  These permutations are only defined for the
 190     segments and subsegments already copied.
 191
 192 *)
 193
 194 (** We have copied `src[..size]` into `dst[..size]`,
 195     according to a permutation given by `p`/`invp`. *)
 196 predicate copy_perm (src dst: array elt) (size: int) (p invp: array int) =
 197   valid_chunk src 0 size && length src = length dst &&
 198   permutation_pair size p invp &&
 199   (forall i. 0 <= i < size -> 0 <=    p[i] < size) &&
 200   (forall i. 0 <= i < size -> 0 <= invp[i] < size) &&
 201   (forall i. 0 <= i < size -> dst[i] = src[p[i]]) &&
 202   (forall i. 0 <= i < size -> src[i] = dst[invp[i]])
 203
 204 (** We have copied subsegment `sigma[j]` to `tau[sigma[j]]`,
 205     and `p`/`invp` are set accordingly. *)
 206 predicate copy_subsegment (src dst: array elt) (s k l j: int)
 207     (sigma tau p invp: array int) =
 208   (* k > 0 && 0 <= j < l && s >= 0 && *)
 209   let start  = s*(k*l) in
 210   let starts = start + sigma[j]*k in
 211   let startd = start + tau[sigma[j]]*k in
 212   copy_to src dst starts startd k &&
 213   (forall i. 0 <= i < k -> p[startd+i] = starts+i) &&
 214   (forall i. 0 <= i < k -> invp[starts+i] = startd+i)
 215
 216 (** Distinct subsegments are indeed distinct, in both source
 217     (`sigma`) and destination (`sigma` then `tau`). *)
 218 let lemma distinct_subsegments (s k l j1 j2: int) (sigma tau: array int)
 219   requires { k > 0 && l > 0 && s >= 0 }
 220   requires { 0 <= j1 < l && 0 <= j2 < l && j1 <> j2 }
 221   requires { permutation l sigma }
 222   requires { permutation l tau }
 223   ensures  {
 224     let start  = s*(k*l) in
 225     let starts1 = start + sigma[j1]*k in
 226     let startd1 = start + tau[sigma[j1]]*k in
 227     let starts2 = start + sigma[j2]*k in
 228     let startd2 = start + tau[sigma[j2]]*k in
 229     forall i. 0 <= i < k -> starts1+i <> starts2+i && startd1+i <> startd2+i }
 230 = ()
 231
 232 (** Framing lemmas *)
 233
 234 predicate frame (a1 a2: array 'a) (ofs len: int) =
 235   length a2 = length a1 &&
 236   (forall i. 0 <= i < ofs -> a2[i] = a1[i]) &&
 237   (forall i. ofs+len <= i < length a2 -> a2[i] = a1[i])
 238
 239 let lemma frame_permutation_pair (start start1 start2 k: int) (op p oinvp invp: array int)
 240   requires { length op = length p = length oinvp = length invp }
 241   requires { 0 <= start <= start1 <= start1 + k <= length p }
 242   requires { 0 <= start <= start2 <= start2 + k <= length p }
 243   requires { permutation_pair start op oinvp }
 244   requires { frame op    p    start1 k }
 245   requires { frame oinvp invp start2 k }
 246   ensures  { permutation_pair start p  invp }
 247 = ()
 248
 249 let lemma frame_subsegment (src odst dst: array elt) (s k l j1 j2: int)
 250      (sigma tau op p oinvp invp: array int)
 251   requires { k > 0 && l > 0 && s >= 0 }
 252   requires { 0 <= j1 < l && 0 <= j2 < l && j1 <> j2 }
 253   requires { length op = length p = length oinvp = length invp >= (s+1)*(k*l) }
 254   requires { permutation l sigma }
 255   requires { permutation l tau }
 256   requires { copy_subsegment src odst s k l j1 sigma tau op oinvp }
 257   requires { frame odst  dst  (s*(k*l) + tau[sigma[j2]]*k) k }
 258   requires { frame op    p    (s*(k*l) + tau[sigma[j2]]*k) k }
 259   requires { frame oinvp invp (s*(k*l) +     sigma[j2] *k) k }
 260   ensures  { copy_subsegment src dst s k l j1 sigma tau p invp }
 261 = ()
 262
 263 (** Find the subsegment in `src` contains `i`. *)
 264 let lemma decompose_sigma (s k l: int) (sigma invsigma: array int) (i: int) :
 265   (j: int, r: int)
 266   requires { k > 0 && l > 0 && s >= 0 }
 267   requires { permutation_pair l sigma invsigma }
 268   requires { s*(k*l) <= i < (s+1)*(k*l) }
 269   ensures  { 0 <= j < l && 0 <= r < k }
 270   ensures  { i = s*(k*l) + sigma[j]*k + r }
 271 = let m = k*l in
 272   let start = s*m in
 273   let q = div (i - start) k in
 274   let r = mod (i - start) k in
 275   let j = invsigma[q] in
 276   assert { 0 <= j < l && 0 <= r < k };
 277   assert { i = start + q*k + r };
 278   assert { i = start + sigma[j]*k + r };
 279   (j, r)
 280
 281 (** Find the subsegment in `dst` contains `i`. *)
 282 let lemma decompose_tau_sigma (s k l: int) (sigma invsigma tau invtau: array int) (i: int) :
 283   (j: int, r: int)
 284   requires { k > 0 && l > 0 && s >= 0 }
 285   requires { permutation_pair l sigma invsigma }
 286   requires { permutation_pair l tau   invtau   }
 287   requires { s*(k*l) <= i < (s+1)*(k*l) }
 288   ensures  { 0 <= j < l && 0 <= r < k }
 289   ensures  { i = s*(k*l) + tau[sigma[j]]*k + r }
 290 = let (j, r) = decompose_sigma s k l tau invtau i in
 291   (invsigma[j], r)
 292
 293 (** And now for the most difficult part: once all subsegments are copied,
 294     we have copied the the whole segment. This is similar to `all_subsegments`
 295     above, but much harder, for we have permutations to be taken into
 296     account now. *)
 297 let lemma all_subsegments_perm (src dst: array elt)
 298     (s k l: int) (sigma invsigma tau invtau p invp: array int)
 299   requires { k > 0 && l > 0 && s >= 0 }
 300   requires { length src = length dst = length p = length invp >= (s+1)*(k*l) }
 301   requires { permutation_pair l sigma invsigma }
 302   requires { permutation_pair l tau   invtau   }
 303   requires { copy_perm src dst (s*(k*l)) p invp }
 304   requires { permutation_pair (s*(k*l)) p invp }
 305   requires { forall j. 0 <= j < l ->
 306                copy_subsegment src dst s k l j sigma tau p invp }
 307   ensures  { permutation_pair ((s+1)*(k*l)) p invp }
 308   ensures  { copy_perm src dst ((s+1)*(k*l)) p invp }
 309 = let m = k*l in
 310   let start = s*m in
 311   assert { start = (s*l) * k };
 312   let lemma mulk (j1 j2: int) requires { j1 < j2 } ensures { j1*k <= j2*k - k }
 313   = () in
 314   let lemma decompose1 (i: int) : (j: int, r: int) requires { start <= i < start+m }
 315     ensures { 0 <= j < l && 0 <= r < k && i = start + sigma[j]*k + r }
 316   = decompose_sigma s k l sigma invsigma i in
 317   let lemma decompose2 (i: int) : (j: int, r: int) requires { start <= i < start+m }
 318     ensures { 0 <= j < l && 0 <= r < k && i = start + tau[sigma[j]]*k + r }
 319   = decompose_tau_sigma s k l sigma invsigma tau invtau i in
 320   let lemma pi_good (i: int) requires { start <= i < start+m }
 321     ensures { start <= p[i] < start+m }
 322   = let j, r = decompose2 i in
 323     assert { copy_subsegment src dst s k l j sigma tau p invp };
 324     assert { p[i] = start + sigma[j]*k + r } in
 325   let lemma invpi_good (i: int) requires { start <= i < start+m }
 326     ensures { start <= invp[i] < start+m by
 327               mod 0 1 = 0  (* to keep div/mod in the context *) }
 328   = let j, r = decompose1 i in
 329     assert { copy_subsegment src dst s k l j sigma tau p invp };
 330     assert { invp[i] = start + tau[sigma[j]]*k + r } in
 331   let lemma p_injective (i1 i2: int) requires { start <= i1 < start+m }
 332     requires { start <= i2 < start+m } requires { i1 <> i2 }
 333     ensures { p[i1] <> p[i2] }
 334   = let j1, r1 = decompose2 i1 in
 335     assert { copy_subsegment src dst s k l j1 sigma tau p invp };
 336     assert { p[i1] = start + sigma[j1]*k + r1 };
 337     let j2, r2 = decompose2 i2 in
 338     assert { copy_subsegment src dst s k l j2 sigma tau p invp };
 339     assert { p[i2] = start + sigma[j2]*k + r2 };
 340     if sigma[j1] < sigma[j2] then (
 341       mulk sigma[j1] sigma[j2]
 342     ) else if sigma[j1] > sigma[j2] then (
 343       mulk sigma[j2] sigma[j1]
 344     ) else (
 345       assert { r1 <> r2 }
 346     ) in
 347   let lemma invp_injective (i1 i2: int) requires { start <= i1 < start+m }
 348     requires { start <= i2 < start+m } requires { i1 <> i2 }
 349     ensures { invp[i1] <> invp[i2] }
 350   = let j1, r1 = decompose1 i1 in
 351     assert { copy_subsegment src dst s k l j1 sigma tau p invp };
 352     assert { invp[i1] = start + tau[sigma[j1]]*k + r1 };
 353     let j2, r2 = decompose1 i2 in
 354     assert { copy_subsegment src dst s k l j2 sigma tau p invp };
 355     assert { invp[i2] = start + tau[sigma[j2]]*k + r2 };
 356     if tau[sigma[j1]] < tau[sigma[j2]] then (
 357       mulk tau[sigma[j1]] tau[sigma[j2]]
 358     ) else if tau[sigma[j1]] > tau[sigma[j2]] then (
 359       mulk tau[sigma[j2]] tau[sigma[j1]]
 360     ) else (
 361       assert { r1 <> r2 }
 362     ) in
 363   let lemma pinvp (i: int) requires { start <= i < start+m }
 364     ensures { p[invp[i]] = i }
 365   = let j, _r = decompose1 i in
 366     assert { copy_subsegment src dst s k l j sigma tau p invp }
 367   in
 368   let lemma copy_i (i: int) requires { start <= i < start+m }
 369     ensures { dst[i] = src[p[i]] }
 370   = let j, _r = decompose2 i in
 371     assert { copy_subsegment src dst s k l j sigma tau p invp };
 372     pi_good i
 373   in
 374   ()
 375
 376 let smart_array_copy_1 (n k l q r: int) (src dst: array elt) :
 377   (ghost p: array int, ghost invp: array int)
 378   requires { length src = length dst = n > 0 }
 379   requires { k > 0 && l > 0 && q >= 0 && 0 <= r < k*l }
 380   requires { n = q * k*l + r }
 381   writes   { dst }
 382   ensures  { copy_perm src dst n p invp }
 383 = let ghost p    = identity n in
 384   let ghost invp = identity n in
 385   let m = k*l in
 386   for s = 0 to q - 1 do
 387     invariant { permutation_pair (s*m) p invp }
 388     invariant { copy_perm src dst (s*m) p invp }
 389     let start = s*m in
 390     assert { start+m <= n };
 391     let sigma, invsigma = permute l in
 392     let tau,   invtau   = permute l in
 393     for j = 0 to l - 1 do
 394       invariant { permutation_pair (s*m) p invp }
 395       invariant { copy_perm src dst (s*m) p invp }
 396       invariant { forall j'. 0 <= j' < j ->
 397                   copy_subsegment src dst s k l j' sigma tau p invp }
 398       let startsrc = start +     sigma[j] *k in
 399       assert { startsrc + k <= start + m };
 400       let startdst = start + tau[sigma[j]]*k in
 401       assert { startdst + k <= start + m };
 402       label L in
 403       for i = 0 to k - 1 do
 404         invariant { frame (dst  at L) dst  startdst k }
 405         invariant { frame (p    at L) p    startdst k }
 406         invariant { frame (invp at L) invp startsrc k }
 407         invariant { permutation_pair (s*m) p invp }
 408         invariant { copy_perm src dst (s*m) p invp }
 409         invariant { copy_to src dst startsrc startdst i }
 410         invariant { forall i'. 0 <= i' < i -> p[startdst+i'] = startsrc+i' }
 411         invariant { forall i'. 0 <= i' < i -> invp[startsrc+i'] = startdst+i' }
 412         invariant { forall j'. 0 <= j' < j ->
 413                     copy_subsegment src dst s k l j' sigma tau p invp }
 414         dst[startdst + i] <- src[startsrc + i];
 415         p  [startdst + i] <-     startsrc + i;
 416         invp[startsrc + i] <- startdst + i
 417       done
 418     done;
 419     all_subsegments_perm src dst s k l sigma invsigma tau invtau p invp
 420   done;
 421   let last = q*m in
 422   for i = 0 to r - 1 do
 423     invariant { permutation_pair (last+i) p invp }
 424     invariant { copy_perm src dst (last+i) p invp }
 425     dst[last + i] <- src[last + i];
 426     p[last + i] <- last + i;
 427     invp[last + i] <- last + i
 428   done;
 429   (p, invp)