verifythis_fm2012_LRS.mlw 14 KB
Newer Older
1
(**
2

3 4 5 6 7 8 9 10 11 12 13
{1 VerifyThis@fm2012 competition, Challenge 1: Longest Repeated Substring}

{h
The following is the original description of the verification task,
reproduced verbatim. A <a
href="http://fm2012.verifythis.org/challenges">reference
implementation in Java</a> (based on code by Robert Sedgewick and
Kevin Wayne) was also given. The Why3 implementation below follows the
Java implementation as faithfully as possible.

<pre>
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
Longest Common Prefix (LCP) - 45 minutes

VERIFICATION TASK
-----------------

Longest Common Prefix (LCP) is an algorithm used for text querying. In
the following, we model text as an integer array. You may use other
representations (e.g., Java Strings), if your system supports them.

LCP can be implemented with the pseudocode given below. Formalize and
verify the following informal specification for LCP.

Input:  an integer array a, and two indices x and y into this array
Output: length of the longest common prefix of the subarrays of a
        starting at x and y respectively.

Pseudocode:

    int lcp(int[] a, int x, int y) {
        int l = 0;
34
        while (x+l&lt;a.length && y+l&lt;a.length && a[x+l]==a[y+l]) {
35 36 37 38 39 40
            l++;
        }
        return l;
    }


MARCHE Claude's avatar
MARCHE Claude committed
41
ADVANCED
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
========

BACKGROUND
----------

Together with a suffix array, LCP can be used to solve interesting text
problems, such as finding the longest repeated substring (LRS) in a text.

A suffix array (for a given text) is an array of all suffixes of the
text. For the text [7,8,8,6], the suffix array is
[[7,8,8,6],
   [8,8,6],
     [8,6],
       [6]]

Typically, the suffixes are not stored explicitly as above but
represented as pointers into the original text. The suffixes in a suffix
array  are sorted in lexicographical order. This way, occurrences of
repeated substrings in the original text are neighbors in the suffix
MARCHE Claude's avatar
MARCHE Claude committed
61
array.
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76

For the above, example (assuming pointers are 0-based integers), the
sorted suffix array is:

[3,0,2,1]

VERIFICATION TASK
-----------------

The attached Java code contains an implementation of a suffix array
(SuffixArray.java), consisting essentially of a lexicographical
comparison on arrays, a sorting routine, and LCP.

The client code (LRS.java) uses these to solve the LRS problem. Verify
that it does so correctly.
77
</pre>}
MARCHE Claude's avatar
MARCHE Claude committed
78

79 80
*)

MARCHE Claude's avatar
MARCHE Claude committed
81 82


83
(** {2 First module: longest common prefix}
84

85
    it corresponds to the basic part of the challenge
86

87
*)
88

89
module LCP
90

MARCHE Claude's avatar
MARCHE Claude committed
91
use export int.Int
92
use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
93

94 95 96
(** [is_common_prefix a x y l] is true when the prefixes of length [l]
    at respective positions [x] and [y] in array [a] are identical. In
    other words, the array parts a[x..x+l-1] and a[y..y+l-1] are equal
97
    *)
98 99
predicate is_common_prefix (a:array int) (x y l:int) =
  0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
MARCHE Claude's avatar
MARCHE Claude committed
100 101
  (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])

102 103 104
(** This lemma helps for the proof of [lcp] (but is not mandatory) and
    is needed later (for [le_trans]) *)
lemma not_common_prefix_if_last_char_are_different:
MARCHE Claude's avatar
MARCHE Claude committed
105 106 107 108
  forall a:array int, x y:int, l:int.
    0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
      not is_common_prefix a x y (l+1)

109 110
(** [is_longest_common_prefix a x y l] is true when [l] is the maximal
    length such that prefixes at positions [x] and [y] in array [a]
111 112 113
    are identical. *)
predicate is_longest_common_prefix (a:array int) (x y l:int) =
  is_common_prefix a x y l /\
114 115
  forall m:int. l < m -> not (is_common_prefix a x y m)

116 117 118 119
(** This lemma helps to proving [lcp] (but again is not mandatory),
    and is needed for proving [lcp_sym] and [le_trans] lemmas, and
    the post-condition of [compare] function in the "absurd" case *)

MARCHE Claude's avatar
MARCHE Claude committed
120
lemma longest_common_prefix_succ:
121 122 123
  forall a:array int, x y l:int.
    is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) ->
    is_longest_common_prefix a x y l
MARCHE Claude's avatar
MARCHE Claude committed
124

MARCHE Claude's avatar
MARCHE Claude committed
125
use export ref.Refint
MARCHE Claude's avatar
MARCHE Claude committed
126

127
(** the first function, that computes the longest common prefix *)
MARCHE Claude's avatar
MARCHE Claude committed
128 129 130
let lcp (a:array int) (x y:int) : int
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
131
  ensures { is_longest_common_prefix a x y result }
MARCHE Claude's avatar
MARCHE Claude committed
132 133 134 135 136 137 138 139
  = let n = a.length in
    let l = ref 0 in
    while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
      invariant { is_common_prefix a x y !l }
      incr l
    done;
    !l

140 141 142 143
end

module LCP_test

144
(** test harness for lcp *)
145 146 147 148

use import array.Array
use import LCP

MARCHE Claude's avatar
MARCHE Claude committed
149
(*
MARCHE Claude's avatar
MARCHE Claude committed
150
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let x = lcp arr 1 2 in
MARCHE Claude's avatar
MARCHE Claude committed
154
  assert { is_common_prefix arr 1 2 1};
155
  assert { not is_common_prefix arr 1 2 2};
156
  check { x = 1 };
MARCHE Claude's avatar
MARCHE Claude committed
157 158 159 160
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let x = lcp brr 1 2 in
MARCHE Claude's avatar
MARCHE Claude committed
161
  assert { is_common_prefix brr 1 2 0};
162
  assert { not is_common_prefix brr 1 2 1};
163
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let x = lcp crr 2 3 in
MARCHE Claude's avatar
MARCHE Claude committed
168
  assert { is_common_prefix crr 2 3 0};
169
  assert { not is_common_prefix crr 2 3 1};
170
  check { x = 0 };
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173 174
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let x = lcp drr 2 3 in
MARCHE Claude's avatar
MARCHE Claude committed
175
  assert { is_common_prefix drr 2 3 1};
176
  assert { not is_common_prefix drr 2 3 2};
177
  check {x = 1}
MARCHE Claude's avatar
MARCHE Claude committed
178
*)
179

MARCHE Claude's avatar
MARCHE Claude committed
180 181 182 183 184
let bench () =
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let x = lcp arr 1 2 in
  if x <> 1 then absurd
MARCHE Claude's avatar
MARCHE Claude committed
185

MARCHE Claude's avatar
MARCHE Claude committed
186
end
MARCHE Claude's avatar
MARCHE Claude committed
187

MARCHE Claude's avatar
MARCHE Claude committed
188

189 190
(** {2 Second module: sorting suffixes } *)
module SuffixSort
MARCHE Claude's avatar
MARCHE Claude committed
191

MARCHE Claude's avatar
MARCHE Claude committed
192 193
  use import int.Int
  use import ref.Refint
MARCHE Claude's avatar
MARCHE Claude committed
194
  use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
195
  use LCP
MARCHE Claude's avatar
MARCHE Claude committed
196 197

  (** order by prefix *)
198
  predicate lt (a : array int) (x y:int) =
MARCHE Claude's avatar
MARCHE Claude committed
199
     let n = a.length in
200
     0 <= x <= n /\ 0 <= y <= n /\
MARCHE Claude's avatar
MARCHE Claude committed
201
     exists l:int. LCP.is_common_prefix a x y l /\
202
     (y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
MARCHE Claude's avatar
MARCHE Claude committed
203

204 205


MARCHE Claude's avatar
MARCHE Claude committed
206
(** comparison function, that decides the order of prefixes *)
MARCHE Claude's avatar
MARCHE Claude committed
207
let compare (a:array int) (x y:int) : int
208 209
  requires { 0 <= x <= a.length }
  requires { 0 <= y <= a.length }
210
  ensures { result = 0 -> x = y }
211 212
  ensures { result < 0 -> lt a x y }
  ensures { result > 0 -> lt a y x }
MARCHE Claude's avatar
MARCHE Claude committed
213
  =
214
  if x = y then 0 else
MARCHE Claude's avatar
MARCHE Claude committed
215
  let n = a.length in
MARCHE Claude's avatar
MARCHE Claude committed
216
  let l = LCP.lcp a x y in
MARCHE Claude's avatar
MARCHE Claude committed
217 218 219 220
  if x + l = n then -1 else
  if y + l = n then 1 else
  if a[x + l] < a[y + l] then -1 else
  if a[x + l] > a[y + l] then 1 else
221 222
  absurd

MARCHE Claude's avatar
MARCHE Claude committed
223

224
  use map.MapInjection
225 226 227
  (** [range a] is true when for each [i], [a[i]] is between [0] at
      [a.length-1] *)
  predicate range (a:array int) = MapInjection.range a.elts a.length
228 229 230 231

  (** for the [permut] predicate (permutation of elements) *)
  use array.ArrayPermut

MARCHE Claude's avatar
MARCHE Claude committed
232
  predicate le (a : array int) (x y:int) = x = y \/ lt a x y
233

MARCHE Claude's avatar
MARCHE Claude committed
234 235 236
  (* needed for le_trans (for cases x = y /\ le y z and le x y /\ y = z) *)
  lemma lcp_same_index :
    forall a:array int, x:int.
MARCHE Claude's avatar
MARCHE Claude committed
237
      0 <= x <= a.length -> LCP.is_longest_common_prefix a x x (a.length - x)
MARCHE Claude's avatar
MARCHE Claude committed
238

239 240
  lemma le_trans : forall a:array int, x y z:int.
    le a x y /\ le a y z -> le a x z
MARCHE Claude's avatar
MARCHE Claude committed
241

MARCHE Claude's avatar
MARCHE Claude committed
242 243
  (** spec of sorted in increasing prefix order *)
  use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
244

245 246 247
  predicate sorted_sub (a:array int) (data:Map.map int int) (l u:int) =
    forall i1 i2 : int. l <= i1 <= i2 < u ->
      le a (Map.get data i1) (Map.get data i2)
MARCHE Claude's avatar
MARCHE Claude committed
248

249
  predicate sorted (a : array int) (data:array int) =
250
    sorted_sub a data.elts 0 data.length
MARCHE Claude's avatar
MARCHE Claude committed
251

252
let sort (a:array int) (data : array int)
253
  requires { data.length = a.length }
254
  requires { range data }
255
  ensures { sorted a data }
256
  ensures { ArrayPermut.permut (old data) data }
MARCHE Claude's avatar
MARCHE Claude committed
257 258
  =
   'Init:
MARCHE Claude's avatar
MARCHE Claude committed
259
   for i = 0 to data.length - 1 do
260
     invariant { ArrayPermut.permut (at data 'Init) data   }
261
     invariant { sorted_sub a data.elts 0 i  }
262
     invariant { range data }
MARCHE Claude's avatar
MARCHE Claude committed
263 264 265
     let j = ref i in
     while !j > 0 && compare a data[!j-1] data[!j] > 0 do
       invariant { 0 <= !j <= i }
266
       invariant { range data }
267
       invariant { ArrayPermut.permut (at data 'Init) data   }
268 269
       invariant { sorted_sub a data.elts 0 !j }
       invariant { sorted_sub a data.elts !j (i+1) }
270 271
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                     le a data[k1] data[k2] }
MARCHE Claude's avatar
MARCHE Claude committed
272 273 274 275 276
       'L:
       let b = !j - 1 in
       let t = data[!j] in
       data[!j] <- data[b];
       data[b] <- t;
277
       assert { ArrayPermut.exchange (at data 'L) data (!j-1) !j };
MARCHE Claude's avatar
MARCHE Claude committed
278
       decr j
279 280 281
     done;
     (* needed to prove the invariant [sorted_sub a data.elts 0 i] *)
     assert { !j > 0 -> le a data[!j-1] data[!j] }
282
   done
MARCHE Claude's avatar
MARCHE Claude committed
283

MARCHE Claude's avatar
MARCHE Claude committed
284 285
end

MARCHE Claude's avatar
MARCHE Claude committed
286 287 288 289 290





291
(** {2 Third module: Suffix Array Data Structure } *)
MARCHE Claude's avatar
MARCHE Claude committed
292

MARCHE Claude's avatar
MARCHE Claude committed
293

MARCHE Claude's avatar
MARCHE Claude committed
294 295
module SuffixArray

MARCHE Claude's avatar
MARCHE Claude committed
296
use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
297
use import array.Array
MARCHE Claude's avatar
MARCHE Claude committed
298 299 300
use LCP
use SuffixSort
use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
301
use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
302

MARCHE Claude's avatar
MARCHE Claude committed
303 304
predicate permutation (m:Map.map int int) (u : int) =
  MapInjection.range m u /\ MapInjection.injective m u
MARCHE Claude's avatar
MARCHE Claude committed
305

MARCHE Claude's avatar
MARCHE Claude committed
306 307 308 309
type suffixArray = {
    values : array int;
    suffixes : array int;
}
MARCHE Claude's avatar
MARCHE Claude committed
310 311
invariant { self.values.length = self.suffixes.length /\
  permutation self.suffixes.elts self.suffixes.length /\
MARCHE Claude's avatar
MARCHE Claude committed
312
  SuffixSort.sorted self.values self.suffixes }
313

MARCHE Claude's avatar
MARCHE Claude committed
314
let select (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
315
  requires { 0 <= i < s.values.length }
MARCHE Claude's avatar
MARCHE Claude committed
316 317 318
  ensures { result = s.suffixes[i] }
  = s.suffixes[i]

319
use array.ArrayPermut
MARCHE Claude's avatar
MARCHE Claude committed
320

MARCHE Claude's avatar
MARCHE Claude committed
321
(** needed to establish invariant in function [create] *)
322
lemma permut_permutation : forall a1 a2:array int.
323
  ArrayPermut.permut a1 a2 /\ permutation a1.elts a1.length ->
324
    permutation a2.elts a2.length
MARCHE Claude's avatar
MARCHE Claude committed
325

MARCHE Claude's avatar
MARCHE Claude committed
326
(** constructor of suffixArray structure *)
MARCHE Claude's avatar
MARCHE Claude committed
327
let create (a:array int) : suffixArray
MARCHE Claude's avatar
MARCHE Claude committed
328
  ensures { result.values = a }
329 330 331 332 333 334 335
= let n = a.length in
  let suf = Array.make n 0 in
  for i = 0 to n-1 do
    invariant { forall j:int. 0 <= j < i -> suf[j] = j }
    suf[i] <- i done;
  SuffixSort.sort a suf;
  { values = a; suffixes = suf }
336

MARCHE Claude's avatar
MARCHE Claude committed
337
let lcp (s:suffixArray) (i:int) : int
MARCHE Claude's avatar
MARCHE Claude committed
338
  requires { 0 < i < s.values.length }
339
  ensures { LCP.is_longest_common_prefix s.values
MARCHE Claude's avatar
MARCHE Claude committed
340
              s.suffixes[i-1] s.suffixes[i] result }
341
= LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
MARCHE Claude's avatar
MARCHE Claude committed
342

343 344
end

345 346 347



348 349 350 351 352
module SuffixArray_test

use import array.Array
use import SuffixArray

MARCHE Claude's avatar
MARCHE Claude committed
353
(*
MARCHE Claude's avatar
MARCHE Claude committed
354
let test () =
MARCHE Claude's avatar
MARCHE Claude committed
355 356 357
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
358 359 360 361
  assert { sa.suffixes[0] = 0 };
  assert { sa.suffixes[1] = 1 };
  assert { sa.suffixes[2] = 2 };
  assert { sa.suffixes[3] = 3 };
MARCHE Claude's avatar
MARCHE Claude committed
362
  let x = lcp sa 1 in
363
  check {x = 0};
MARCHE Claude's avatar
MARCHE Claude committed
364 365 366 367
  (* int[] brr = {1,2,3,5}; *)
  let brr = Array.make 4 0 in
  brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
  let sa = create brr in
MARCHE Claude's avatar
MARCHE Claude committed
368
  let x = lcp sa 1 in
369
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
370 371 372 373
  (* int[] crr = {1,2,3,5}; *)
  let crr = Array.make 4 0 in
  crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
  let sa = create crr in
MARCHE Claude's avatar
MARCHE Claude committed
374
  let x = lcp sa 2 in
375
  check {x = 0 (* TODO *)};
MARCHE Claude's avatar
MARCHE Claude committed
376 377 378 379
  (* int[] drr = {1,2,3,3}; *)
  let drr = Array.make 4 0 in
  drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
  let sa = create drr in
MARCHE Claude's avatar
MARCHE Claude committed
380
  let x = lcp sa 2 in
381
  check {x = 0 (* TODO *)}
MARCHE Claude's avatar
MARCHE Claude committed
382
*)
383

MARCHE Claude's avatar
MARCHE Claude committed
384 385 386 387 388 389 390 391 392
let bench () =
  let arr = Array.make 4 0 in
  arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
  let sa = create arr in
  if sa.suffixes[0] <> 0 then absurd;
  if sa.suffixes[1] <> 1 then absurd;
  if sa.suffixes[2] <> 2 then absurd;
  if sa.suffixes[3] <> 3 then absurd

393
end
MARCHE Claude's avatar
MARCHE Claude committed
394 395


396
(** {2 Fourth module: Longest Repeated Substring} *)
MARCHE Claude's avatar
MARCHE Claude committed
397

398
module LRS
MARCHE Claude's avatar
MARCHE Claude committed
399

MARCHE Claude's avatar
MARCHE Claude committed
400 401 402
  use import int.Int
  use import ref.Ref
  use import array.Array
403
  use map.MapInjection
MARCHE Claude's avatar
MARCHE Claude committed
404
  use LCP
405
  use SuffixSort
MARCHE Claude's avatar
MARCHE Claude committed
406
  use SuffixArray
MARCHE Claude's avatar
MARCHE Claude committed
407 408


MARCHE Claude's avatar
MARCHE Claude committed
409
(** additional properties relating [le] and [longest_common_prefix] *)
MARCHE Claude's avatar
MARCHE Claude committed
410

MARCHE Claude's avatar
MARCHE Claude committed
411
(* needed for [lrs] function, last before last assert *)
MARCHE Claude's avatar
MARCHE Claude committed
412 413 414
lemma lcp_sym :
  forall a:array int, x y l:int.
     0 <= x <= a.length /\ 0 <= y <= a.length ->
415
       LCP.is_longest_common_prefix a x y l ->
MARCHE Claude's avatar
MARCHE Claude committed
416
       LCP.is_longest_common_prefix a y x l
MARCHE Claude's avatar
MARCHE Claude committed
417 418


MARCHE Claude's avatar
MARCHE Claude committed
419 420
(** allows CVC to prove the next lemma *)
lemma le_le_common_prefix:
MARCHE Claude's avatar
MARCHE Claude committed
421
    forall a:array int, x y z l:int.
MARCHE Claude's avatar
MARCHE Claude committed
422 423
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
     LCP.is_common_prefix a x z l -> LCP.is_common_prefix a y z l
MARCHE Claude's avatar
MARCHE Claude committed
424

MARCHE Claude's avatar
MARCHE Claude committed
425
(** proved by Alt-Ergo and CVC. But only by Alt-Ergo if previous lemma is removed *)
MARCHE Claude's avatar
MARCHE Claude committed
426 427
  lemma le_le_longest_common_prefix:
    forall a:array int, x y z l m :int.
MARCHE Claude's avatar
MARCHE Claude committed
428
     SuffixSort.le a x y /\ SuffixSort.le a y z ->
429
     LCP.is_longest_common_prefix a x z l /\
MARCHE Claude's avatar
MARCHE Claude committed
430 431
     LCP.is_longest_common_prefix a y z m
       -> l <= m
MARCHE Claude's avatar
MARCHE Claude committed
432

MARCHE Claude's avatar
MARCHE Claude committed
433

MARCHE Claude's avatar
MARCHE Claude committed
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
  val solStart : ref int
  val solLength : ref int
  val ghost solStart2 : ref int

  let lrs (a:array int) : unit
    requires { a.length > 0 }
    ensures { 0 <= !solLength <= a.length }
    ensures { 0 <= !solStart <= a.length }
    ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
              LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
    ensures { forall x y l:int.
                0 <= x < y < a.length /\
                LCP.is_longest_common_prefix a x y l ->
                !solLength >= l }
  =
    let sa = SuffixArray.create a in
    solStart := 0;
    solLength := 0;
    solStart2 := a.length;
    for i=1 to a.length - 1 do
      invariant { 0 <= !solLength <= a.length }
      invariant { 0 <= !solStart <= a.length }
      invariant {
           0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
           LCP.is_longest_common_prefix a !solStart !solStart2 !solLength }
      invariant { forall j k l:int.
460 461 462 463
                  0 <= j < k < i /\
                  LCP.is_longest_common_prefix a
                    sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
                  !solLength >= l }
MARCHE Claude's avatar
MARCHE Claude committed
464 465 466 467 468 469 470 471 472 473
      let l = SuffixArray.lcp sa i in
      if l > !solLength then begin
         solStart := SuffixArray.select sa i;
         solStart2 := SuffixArray.select sa (i-1);
         solLength := l
      end
    done;
    (** the following assert needs [lcp_sym] lemma *)
    assert { forall j k l:int.
                0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
474
                 LCP.is_longest_common_prefix a
MARCHE Claude's avatar
MARCHE Claude committed
475 476
                 sa.SuffixArray.suffixes[j] sa.SuffixArray.suffixes[k] l ->
              !solLength >= l};
MARCHE Claude's avatar
MARCHE Claude committed
477
    (* we state explicitly that sa.suffixes is surjective *)
MARCHE Claude's avatar
MARCHE Claude committed
478 479 480
    assert { forall x y:int.
                0 <= x < y < a.length ->
                exists j k : int.
481 482
                  0 <= j < a.length /\ 0 <= k < a.length /\ j <> k /\
                  x = sa.SuffixArray.suffixes[j] /\
483
                  y = sa.SuffixArray.suffixes[k] };
MARCHE Claude's avatar
MARCHE Claude committed
484
    ()
485

486 487 488
end


MARCHE Claude's avatar
MARCHE Claude committed
489
(*
490 491 492 493 494 495
module LRS_test

use import array.Array
use import ref.Ref
use import LRS

496
 let test () =
MARCHE Claude's avatar
MARCHE Claude committed
497 498 499
    let arr = Array.make 4 0 in
    arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
    lrs arr;
500
    check { !solStart = 1 /\ !solLength = 1 }
501 502

end
MARCHE Claude's avatar
MARCHE Claude committed
503
*)