Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 6d673d20 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

LCP: use a ghost variable

parent d56caa8b
......@@ -86,10 +86,11 @@ predicate map_permutation (m:Map.map int int) (u : int) =
MapInjection.range m u /\
MapInjection.injective m u
(*
lemma map_permut_permutation :
forall m1 m2:Map.map int int, u:int [MapPermut.permut_sub m1 m2 0 u].
MapPermut.permut_sub m1 m2 0 u -> map_permutation m1 u -> map_permutation m2 u
*)
use import array.Array
use import array.ArrayPermut
......@@ -97,10 +98,11 @@ use import array.ArrayPermut
predicate permutation (a:array int) =
map_permutation a.elts a.length
(**)
lemma permut_permutation :
forall a1 a2:array int.
permut a1 a2 -> permutation a1 -> permutation a2
(**)
......@@ -129,6 +131,24 @@ axiom lcp_spec:
(l = longest_common_prefix a x y <->
is_common_prefix a x y l /\ not is_common_prefix a x y (l+1))
use import ref.Refint
let lcp (a:array int) (x y:int) : int
requires { 0 <= x <= a.length }
requires { 0 <= y <= a.length }
ensures { result = longest_common_prefix a x y }
= 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;
assert { is_common_prefix a x y !l };
assert { x + !l < n /\ y + !l < n -> a[x + !l] <> a[y + !l] };
assert { not is_common_prefix a x y (!l+1) };
!l
lemma lcp_is_cp :
forall a:array int, x y:int.
0 <= x <= a.length /\ 0 <= y <= a.length ->
......@@ -150,24 +170,6 @@ lemma lcp_sym :
0 <= x <= a.length /\ 0 <= y <= a.length ->
longest_common_prefix a x y = longest_common_prefix a y x
use import ref.Refint
let lcp (a:array int) (x y:int) : int
requires { 0 <= x <= a.length }
requires { 0 <= y <= a.length }
ensures { result = longest_common_prefix a x y }
= 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;
assert { is_common_prefix a x y !l };
assert { x + !l < n /\ y + !l < n -> a[x + !l] <> a[y + !l] };
assert { not is_common_prefix a x y (!l+1) };
!l
let test1 () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
......@@ -434,14 +436,14 @@ module LRS "longest repeated substring"
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 { exists y:int.
0 <= y <= a.length /\ !solStart <> y /\
!solLength = LCP.longest_common_prefix a !solStart y }
ensures { 0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
!solLength = LCP.longest_common_prefix a !solStart !solStart2 }
ensures { forall x y:int.
0 <= x < y < a.length ->
!solLength >= LCP.longest_common_prefix a x y }
......@@ -450,12 +452,13 @@ module LRS "longest repeated substring"
assert { LCP.permutation sa.SuffixArray.suffixes };
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 { exists y:int.
0 <= y <= a.length /\ !solStart <> y /\
!solLength = LCP.longest_common_prefix a !solStart y }
invariant {
0 <= !solStart2 <= a.length /\ !solStart <> !solStart2 /\
!solLength = LCP.longest_common_prefix a !solStart !solStart2 }
invariant { forall j k:int.
0 <= j < k < i ->
!solLength >= LCP.longest_common_prefix a
......@@ -475,6 +478,7 @@ module LRS "longest repeated substring"
sa.SuffixArray.suffixes[k] };
if l > !solLength then begin
solStart := SuffixArray.select sa i;
solStart2 := SuffixArray.select sa (i-1);
solLength := l
end
done;
......
......@@ -3,6 +3,9 @@
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
......@@ -20,40 +23,15 @@ Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
| (mk_ref x) => x
end.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map Z a) -> array a.
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) :=
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
......@@ -65,80 +43,81 @@ Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
end.
(* Why3 assumption *)
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
(get (elts a1) i).
Definition get {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (set (elts a1) i v)).
Definition set {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
(mk_array n (const v:(map Z a))).
(mk_array n (map.Map.const v:(map.Map.map Z a))).
(* Why3 assumption *)
Definition injective(a:(map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
Definition injective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) ->
((~ (i = j)) -> ~ ((get a i) = (get a j)))).
((~ (i = j)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))).
(* Why3 assumption *)
Definition surjective(a:(map Z Z)) (n:Z): Prop := forall (i:Z),
Definition surjective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\
((get a j) = i).
((map.Map.get a j) = i).
(* Why3 assumption *)
Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z).
Definition range(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\
((map.Map.get a i) < n)%Z).
Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) ->
((range a n) -> (surjective a n)).
Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Definition permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\
(injective (elts a) (length a)).
Definition map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\
(injective m u).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
(l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
(i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1
j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2
k))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)),
forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1
k) = (map.Map.get a2 k))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
j).
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z
-> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z
a)) (a2:(map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\
(l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) ->
(permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
(a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
(a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\
((get a2 i) = (get a1 j)).
Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a)
-> (map.Map.map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a1 l u)
| permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a))
(a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1
a2 l u))).
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z)
(l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) ->
((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z
a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
i) = (map.Map.get a1 i)).
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a},
forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2
i) = (map.Map.get a1 j)).
(* Why3 assumption *)
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
......@@ -165,6 +144,11 @@ Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
(a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
(permut a1 a3)).
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
......@@ -181,14 +165,18 @@ Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).
Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), ((permut a1
a2) /\ (permutation a1)) -> (permutation a2).
(* Why3 assumption *)
Definition permutation(a:(array Z)): Prop := (map_permutation (elts a)
(length a)).
Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1
a2) -> ((permutation a1) -> (permutation a2)).
(* Why3 assumption *)
Definition is_common_prefix(a:(array Z)) (x:Z) (y:Z) (l:Z): Prop :=
(0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\
(((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < l)%Z) -> ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)))).
(i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))).
Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z).
......@@ -199,7 +187,7 @@ Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z)
(l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\
(((y + l)%Z < (length a))%Z /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a
(((y + l)%Z < (length a))%Z /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a
(y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l).
Parameter longest_common_prefix: (array Z) -> Z -> Z -> Z.
......@@ -216,7 +204,7 @@ Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
(x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) ->
forall (i:Z), ((0%Z <= i)%Z /\ (i < (longest_common_prefix a x y))%Z) ->
((get1 a (x + i)%Z) = (get1 a (y + i)%Z)).
((get a (x + i)%Z) = (get a (y + i)%Z)).
Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> ((longest_common_prefix a x
......@@ -230,7 +218,7 @@ Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
Definition le(a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in
(((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ let l :=
(longest_common_prefix a x y) in (((x + l)%Z = n) \/ (((x + l)%Z < n)%Z /\
(((y + l)%Z < n)%Z /\ ((get1 a (x + l)%Z) <= (get1 a (y + l)%Z))%Z))))).
(((y + l)%Z < n)%Z /\ ((get a (x + l)%Z) <= (get a (y + l)%Z))%Z))))).
Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\
(x <= (length a))%Z) -> (le a x x).
......@@ -247,41 +235,45 @@ Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\
(* Why3 assumption *)
Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop :=
forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) ->
(le a (get1 data i1) (get1 data i2)).
(le a (get data i1) (get data i2)).
Axiom sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
(x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x
(get1 data l)))) -> (le a x (get1 data i)).
(get data l)))) -> (le a x (get data i)).
Axiom sorted_ge : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z)
(x:Z), ((sorted_sub a data l u) /\ ((le a (get1 data (u - 1%Z)%Z) x) /\
((l <= i)%Z /\ (i < u)%Z))) -> (le a (get1 data i) x).
(x:Z), ((sorted_sub a data l u) /\ ((le a (get data (u - 1%Z)%Z) x) /\
((l <= i)%Z /\ (i < u)%Z))) -> (le a (get data i) x).
Axiom sorted_sub_sub : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(l':Z) (u':Z), ((l <= l')%Z /\ (u' <= u)%Z) -> ((sorted_sub a data l u) ->
(sorted_sub a data l' u')).
Axiom sorted_sub_add : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z),
((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get1 data l) (get1 data
((sorted_sub a data (l + 1%Z)%Z u) /\ (le a (get data l) (get data
(l + 1%Z)%Z))) -> (sorted_sub a data l u).
Axiom sorted_sub_concat : forall (a:(array Z)) (data:(array Z)) (l:Z) (m:Z)
(u:Z), (((l <= m)%Z /\ (m <= u)%Z) /\ ((sorted_sub a data l m) /\
((sorted_sub a data m u) /\ (le a (get1 data (m - 1%Z)%Z) (get1 data
((sorted_sub a data m u) /\ (le a (get data (m - 1%Z)%Z) (get data
m))))) -> (sorted_sub a data l u).
Axiom sorted_sub_set : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
(set1 data i v) l u).
(set data i v) l u).
Axiom sorted_sub_set2 : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z)
(i:Z) (v:Z), ((sorted_sub a data l u) /\ (u <= i)%Z) -> (sorted_sub a
(mk_array (length a) (set (elts data) i v)) l u).
(mk_array (length a) (map.Map.set (elts data) i v)) l u).
(* Why3 assumption *)
Definition sorted(a:(array Z)) (data:(array Z)): Prop := (sorted_sub a data
0%Z (length data)).
Axiom lcp_le_le_min : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\
(le a y z)) -> ((longest_common_prefix a x
z) = (Zmin (longest_common_prefix a x y) (longest_common_prefix a y z))).
Axiom lcp_le_le : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), ((le a x y) /\
(le a y z)) -> ((longest_common_prefix a x z) <= (longest_common_prefix a y
z))%Z.
......@@ -307,42 +299,39 @@ Definition values(v:suffixArray): (array Z) :=
(* Why3 assumption *)
Definition inv(s:suffixArray): Prop :=
((length (values s)) = (length (suffixes s))) /\
(permutation (suffixes s)).
((permutation (suffixes s)) /\ (sorted (values s) (suffixes s))).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map Z Z)), let a2 :=
(mk_array a a1) in ((0%Z < a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z) (sa1:(map
Z Z)) (sa2:Z) (sa3:(map Z Z)), (((sa = a) /\ (sa1 = a1)) /\
(inv (mk_suffixArray (mk_array sa sa1) (mk_array sa2 sa3)))) ->
((permutation (mk_array sa2 sa3)) -> forall (solStart:Z),
Theorem WP_parameter_lrs : forall (a:Z), forall (a1:(map.Map.map Z Z)),
let a2 := (mk_array a a1) in ((0%Z < a)%Z -> ((0%Z <= a)%Z -> forall (sa:Z)
(sa1:(map.Map.map Z Z)) (sa2:Z) (sa3:(map.Map.map Z Z)), (((sa = a) /\
(sa1 = a1)) /\ (inv (mk_suffixArray (mk_array sa sa1) (mk_array sa2
sa3)))) -> ((map_permutation sa3 sa2) -> forall (solStart:Z),
(solStart = 0%Z) -> forall (solLength:Z), (solLength = 0%Z) ->
((1%Z <= (a - 1%Z)%Z)%Z -> forall (solLength1:Z) (solStart1:Z),
forall (solStart2:Z), (solStart2 = a) -> ((1%Z <= (a - 1%Z)%Z)%Z ->
forall (solStart21:Z) (solLength1:Z) (solStart1:Z),
(((((0%Z <= solLength1)%Z /\ (solLength1 <= a)%Z) /\
((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ exists y:Z,
((0%Z <= y)%Z /\ (y <= a)%Z) /\ ((~ (solStart1 = y)) /\
(solLength1 = (longest_common_prefix a2 solStart1 y)))) /\ forall (j:Z)
(k:Z), (((0%Z <= j)%Z /\ (j < k)%Z) /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) ->
((longest_common_prefix a2 (get sa3 j) (get sa3 k)) <= solLength1)%Z) ->
((0%Z <= solStart1)%Z /\ (solStart1 <= a)%Z)) /\ (((0%Z <= solStart21)%Z /\
(solStart21 <= a)%Z) /\ ((~ (solStart1 = solStart21)) /\
(solLength1 = (longest_common_prefix a2 solStart1 solStart21))))) /\
forall (j:Z) (k:Z), (((0%Z <= j)%Z /\ (j < k)%Z) /\
(k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) -> ((longest_common_prefix a2
(map.Map.get sa3 j) (map.Map.get sa3 k)) <= solLength1)%Z) ->
((surjective sa3 sa2) -> ((forall (j:Z) (k:Z), (((0%Z <= j)%Z /\
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ~ (j = k))) ->
((longest_common_prefix a2 (get sa3 j) (get sa3 k)) <= solLength1)%Z) ->
((forall (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x < y)%Z) /\ (y < a)%Z) ->
exists j:Z, exists k:Z, ((0%Z <= j)%Z /\ (j < a)%Z) /\ (((0%Z <= k)%Z /\
(k < a)%Z) /\ ((~ (j = k)) /\ ((x = (get sa3 j)) /\ (y = (get sa3
k)))))) -> forall (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x < y)%Z) /\
(y < a)%Z) -> ((longest_common_prefix a2 x y) <= solLength1)%Z))))))).
intros a a1 a2 h1 h2 sa sa1 sa2 sa3 ((h3,h4),h5) h6 solStart h7 solLength h8
h9 solLength1 solStart1
((((h10,h11),(h12,h13)),(y,((h14,h15),(h16,h17)))),h18) h19 h20 h21 x y0
h22.
elim (h21 _ _ h22).
intros i (j & H1 & H2 & H3 & H4 & H5).
subst x y0.
apply h20.
omega.
((longest_common_prefix a2 (map.Map.get sa3 j) (map.Map.get sa3
k)) <= solLength1)%Z) -> ((forall (x:Z) (y:Z), (((0%Z <= x)%Z /\
(x < y)%Z) /\ (y < a)%Z) -> exists j:Z, exists k:Z, ((0%Z <= j)%Z /\
(j < a)%Z) /\ (((0%Z <= k)%Z /\ (k < a)%Z) /\ ((~ (j = k)) /\
((x = (map.Map.get sa3 j)) /\ (y = (map.Map.get sa3 k)))))) -> forall (x:Z)
(y:Z), (((0%Z <= x)%Z /\ (x < y)%Z) /\ (y < a)%Z) ->
((longest_common_prefix a2 x y) <= solLength1)%Z))))))).
intros.
elim (H10 _ _ H11).
ae.
Qed.
......@@ -3,6 +3,9 @@
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require map.Map.
Require map.MapPermut.
(* Why3 assumption *)
Definition unit := unit.
......@@ -20,40 +23,15 @@ Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
| (mk_ref x) => x
end.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).