Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit 03640fbb authored by MARCHE Claude's avatar MARCHE Claude

update some obsolete sessions

parent 5facf99b
......@@ -12,116 +12,120 @@ Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom set : forall (a:Type) {a_WT:WhyType a}, Type.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> Prop.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(@set a a_WT)) (s2:(@set
a a_WT)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)), (infix_eqeq s1 s2) -> (s1 = s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a} (s1:(@set a a_WT)) (s2:(@set
a a_WT)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
a a_WT)), (subset s s).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)) (s3:(@set a a_WT)), (subset s1 s2) -> ((subset
s2 s3) -> (subset s1 s3)).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(@set a a_WT)): Prop :=
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(@set
a a_WT))).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty :(@set a a_WT))).
(empty : (set a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> (@set
a a_WT).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(@set a a_WT)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT)
-> (@set a a_WT).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(@set a a_WT)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (mem x s) -> ((add x (remove x s)) = s).
Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), ((remove x (add x s)) = (remove x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(@set
a a_WT)), (subset (remove x s) s).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
a a_WT) -> (@set a a_WT).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/
(mem x s2)).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
a a_WT) -> (@set a a_WT).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\
(mem x s2)).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> (@set
a a_WT) -> (@set a a_WT).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set a a_WT))
(s2:(@set a a_WT)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x
s2)).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)), (subset (diff s1 s2) s1).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> a.
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
a a_WT)), (~ (is_empty s)) -> (mem (choose s) s).
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (@set a a_WT) -> Z.
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
a a_WT)), (0%Z <= (cardinal s))%Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set
a a_WT)), ((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(@set a a_WT)), (~ (mem x s)) -> ((cardinal (add x
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(@set a a_WT)), (mem x s) ->
((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(@set
a a_WT)) (s2:(@set a a_WT)), (subset s1 s2) ->
((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(@set a a_WT)),
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter vertices: (@set vertex vertex_WhyType).
Parameter vertices: (set vertex).
Parameter edges: (@set (vertex* vertex)%type _).
Parameter edges: (set (vertex* vertex)%type).
(* Why3 assumption *)
Definition edge (x:vertex) (y:vertex): Prop := (mem (x, y) edges).
......@@ -136,111 +140,118 @@ Axiom s_in_graph : (mem s vertices).
Axiom vertices_cardinal_pos : (0%Z < (cardinal vertices))%Z.
(* Why3 assumption *)
Inductive path : vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x nil x)
Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(edge x y) -> ((path y l z) -> (path x (cons x l) z)).
(edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).
Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
(List.app l (cons y nil)) z)).
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).
Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
(path x l z) -> (((x = z) /\ (l = nil)) \/ exists y:vertex,
(path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
exists l':(list vertex), (path x l' y) /\ ((edge y z) /\
(l = (List.app l' (cons y nil))))).
(l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))).
Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
(l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
(List.app l1 l2) z)).
(Init.Datatypes.app l1 l2) z)).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x nil y) -> (x = y).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
y) -> (x = y).
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)), (path x (List.app l1 (cons y l2))
z) -> ((path x l1 y) /\ (path y (cons y l2) z)).
(l1:(list vertex)) (l2:(list vertex)), (path x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
(path y (Init.Datatypes.cons y l2) z)).
Parameter weight: vertex -> vertex -> Z.
(* Why3 assumption *)
Fixpoint path_weight (l:(list vertex)) (dst:vertex) {struct l}: Z :=
match l with
| nil => 0%Z
| (cons x nil) => (weight x dst)
| (cons x ((cons y _) as r)) => ((weight x y) + (path_weight r dst))%Z
| Init.Datatypes.nil => 0%Z
| (Init.Datatypes.cons x Init.Datatypes.nil) => (weight x dst)
| (Init.Datatypes.cons x ((Init.Datatypes.cons y _) as r)) => ((weight x
y) + (path_weight r dst))%Z
end.
Axiom path_weight_right_extension : forall (x:vertex) (y:vertex)
(l:(list vertex)), ((path_weight (List.app l (cons x nil))
(l:(list vertex)),
((path_weight (Init.Datatypes.app l (Init.Datatypes.cons x Init.Datatypes.nil))
y) = ((path_weight l x) + (weight x y))%Z).
Axiom path_weight_decomposition : forall (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)),
((path_weight (List.app l1 (cons y l2)) z) = ((path_weight l1
y) + (path_weight (cons y l2) z))%Z).
((path_weight (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))
z) = ((path_weight l1 y) + (path_weight (Init.Datatypes.cons y l2) z))%Z).
Axiom path_in_vertices : forall (v1:vertex) (v2:vertex) (l:(list vertex)),
(mem v1 vertices) -> ((path v1 l v2) -> (mem v2 vertices)).
(* Why3 assumption *)
Definition pigeon_set (s1:(@set vertex vertex_WhyType)): Prop :=
forall (l:(list vertex)), (forall (e:vertex), (list.Mem.mem e l) -> (mem e
s1)) -> (((cardinal s1) < (list.Length.length l))%Z -> exists e:vertex,
Definition pigeon_set (s1:(set vertex)): Prop := forall (l:(list vertex)),
(forall (e:vertex), (list.Mem.mem e l) -> (mem e s1)) ->
(((cardinal s1) < (list.Length.length l))%Z -> exists e:vertex,
exists l1:(list vertex), exists l2:(list vertex), exists l3:(list vertex),
(l = (List.app l1 (cons e (List.app l2 (cons e l3)))))).
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons e (Init.Datatypes.app l2 (Init.Datatypes.cons e l3)))))).
Axiom Induction : (forall (s1:(@set vertex vertex_WhyType)), (is_empty s1) ->
(pigeon_set s1)) -> ((forall (s1:(@set vertex vertex_WhyType)), (pigeon_set
s1) -> forall (t:vertex), (~ (mem t s1)) -> (pigeon_set (add t s1))) ->
forall (s1:(@set vertex vertex_WhyType)), (pigeon_set s1)).
Axiom Induction : (forall (s1:(set vertex)), (is_empty s1) -> (pigeon_set
s1)) -> ((forall (s1:(set vertex)), (pigeon_set s1) -> forall (t:vertex),
(~ (mem t s1)) -> (pigeon_set (add t s1))) -> forall (s1:(set vertex)),
(pigeon_set s1)).
Axiom corner : forall (s1:(@set vertex vertex_WhyType)) (l:(list vertex)),
Axiom corner : forall (s1:(set vertex)) (l:(list vertex)),
((list.Length.length l) = (cardinal s1)) -> ((forall (e:vertex),
(list.Mem.mem e l) -> (mem e s1)) -> ((exists e:vertex,
(exists l1:(list vertex), (exists l2:(list vertex),
(exists l3:(list vertex),
(l = (List.app l1 (cons e (List.app l2 (cons e l3))))))))) \/
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons e (Init.Datatypes.app l2 (Init.Datatypes.cons e l3))))))))) \/
forall (e:vertex), (mem e s1) -> (list.Mem.mem e l))).
Axiom pigeon_0 : (pigeon_set (empty :(@set vertex vertex_WhyType))).
Axiom pigeon_0 : (pigeon_set (empty : (set vertex))).
Axiom pigeon_1 : forall (s1:(@set vertex vertex_WhyType)), (pigeon_set s1) ->
Axiom pigeon_1 : forall (s1:(set vertex)), (pigeon_set s1) ->
forall (t:vertex), (pigeon_set (add t s1)).
Axiom pigeon_2 : forall (s1:(@set vertex vertex_WhyType)), (pigeon_set s1).
Axiom pigeon_2 : forall (s1:(set vertex)), (pigeon_set s1).
Axiom pigeonhole : forall (s1:(@set vertex vertex_WhyType))
(l:(list vertex)), (forall (e:vertex), (list.Mem.mem e l) -> (mem e s1)) ->
Axiom pigeonhole : forall (s1:(set vertex)) (l:(list vertex)),
(forall (e:vertex), (list.Mem.mem e l) -> (mem e s1)) ->
(((cardinal s1) < (list.Length.length l))%Z -> exists e:vertex,
exists l1:(list vertex), exists l2:(list vertex), exists l3:(list vertex),
(l = (List.app l1 (cons e (List.app l2 (cons e l3)))))).
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons e (Init.Datatypes.app l2 (Init.Datatypes.cons e l3)))))).
Axiom long_path_decomposition_pigeon1 : forall (l:(list vertex)) (v:vertex),
(path s l v) -> ((~ (l = nil)) -> forall (v1:vertex), (list.Mem.mem v1
(cons v l)) -> (mem v1 vertices)).
(path s l v) -> ((~ (l = Init.Datatypes.nil)) -> forall (v1:vertex),
(list.Mem.mem v1 (Init.Datatypes.cons v l)) -> (mem v1 vertices)).
Axiom long_path_decomposition_pigeon2 : forall (l:(list vertex)) (v:vertex),
(forall (v1:vertex), (list.Mem.mem v1 (cons v l)) -> (mem v1 vertices)) ->
(((cardinal vertices) < (list.Length.length (cons v l)))%Z ->
(forall (v1:vertex), (list.Mem.mem v1 (Init.Datatypes.cons v l)) -> (mem v1
vertices)) ->
(((cardinal vertices) < (list.Length.length (Init.Datatypes.cons v l)))%Z ->
exists e:vertex, exists l1:(list vertex), exists l2:(list vertex),
exists l3:(list vertex),
((cons v l) = (List.app l1 (cons e (List.app l2 (cons e l3)))))).
((Init.Datatypes.cons v l) = (Init.Datatypes.app l1 (Init.Datatypes.cons e (Init.Datatypes.app l2 (Init.Datatypes.cons e l3)))))).
Axiom long_path_decomposition_pigeon3 : forall (l:(list vertex)) (v:vertex),
(exists e:vertex, (exists l1:(list vertex), (exists l2:(list vertex),
(exists l3:(list vertex),
((cons v l) = (List.app l1 (cons e (List.app l2 (cons e l3))))))))) ->
((Init.Datatypes.cons v l) = (Init.Datatypes.app l1 (Init.Datatypes.cons e (Init.Datatypes.app l2 (Init.Datatypes.cons e l3))))))))) ->
((exists l1:(list vertex), (exists l2:(list vertex),
(l = (List.app l1 (cons v l2))))) \/ exists n:vertex,
exists l1:(list vertex), exists l2:(list vertex), exists l3:(list vertex),
(l = (List.app l1 (cons n (List.app l2 (cons n l3)))))).
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons v l2))))) \/
exists n:vertex, exists l1:(list vertex), exists l2:(list vertex),
exists l3:(list vertex),
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons n (Init.Datatypes.app l2 (Init.Datatypes.cons n l3)))))).
Axiom long_path_decomposition : forall (l:(list vertex)) (v:vertex), (path s
l v) -> (((cardinal vertices) <= (list.Length.length l))%Z ->
((exists l1:(list vertex), (exists l2:(list vertex),
(l = (List.app l1 (cons v l2))))) \/ exists n:vertex,
exists l1:(list vertex), exists l2:(list vertex), exists l3:(list vertex),
(l = (List.app l1 (cons n (List.app l2 (cons n l3))))))).
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons v l2))))) \/
exists n:vertex, exists l1:(list vertex), exists l2:(list vertex),
exists l3:(list vertex),
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons n (Init.Datatypes.app l2 (Init.Datatypes.cons n l3))))))).
Axiom simple_path : forall (v:vertex) (l:(list vertex)), (path s l v) ->
exists l':(list vertex), (path s l' v) /\
......@@ -297,29 +308,28 @@ Axiom Antisymm : forall (x:t) (y:t), (le x y) -> ((le y x) -> (x = y)).
Axiom Total : forall (x:t) (y:t), (le x y) \/ (le y x).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Definition t1 (a:Type) {a_WT:WhyType a} := (@ref (@set a a_WT) (@set_WhyType
a a_WT)).
Definition t1 (a:Type) := (ref (set a)).
(* Why3 assumption *)
Definition distmap := (@map.Map.map vertex vertex_WhyType t t_WhyType).
Definition distmap := (map.Map.map vertex t).
(* Why3 assumption *)
Definition inv1 (m:(@map.Map.map vertex vertex_WhyType t t_WhyType)) (pass:Z)
(via:(@set (vertex* vertex)%type _)): Prop := forall (v:vertex), (mem v
vertices) -> match (map.Map.get m
Definition inv1 (m:(map.Map.map vertex t)) (pass:Z) (via:(set (vertex*
vertex)%type)): Prop := forall (v:vertex), (mem v vertices) ->
match (map.Map.get m
v) with
| (Finite n) => (exists l:(list vertex), (path s l v) /\ ((path_weight l
v) = n)) /\ ((forall (l:(list vertex)), (path s l v) ->
......@@ -334,22 +344,20 @@ Definition inv1 (m:(@map.Map.map vertex vertex_WhyType t t_WhyType)) (pass:Z)
end.
(* Why3 assumption *)
Definition inv2 (m:(@map.Map.map vertex vertex_WhyType t t_WhyType))
(via:(@set (vertex* vertex)%type _)): Prop := forall (u:vertex) (v:vertex),
(mem (u, v) via) -> (le (map.Map.get m v) (add1 (map.Map.get m u)
(Finite (weight u v)))).
Definition inv2 (m:(map.Map.map vertex t)) (via:(set (vertex*
vertex)%type)): Prop := forall (u:vertex) (v:vertex), (mem (u, v) via) ->
(le (map.Map.get m v) (add1 (map.Map.get m u) (Finite (weight u v)))).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 30.
Ltac ae := why3 "alt-ergo" timelimit 60.
Ltac Z3 := why3 "z3" timelimit 10.
Require Import list.Length.
(* Why3 goal *)
Theorem key_lemma_2 : forall (m:(@map.Map.map vertex vertex_WhyType
t t_WhyType)), (inv1 m (cardinal vertices) (empty :(@set (vertex*
vertex)%type _))) -> ((inv2 m edges) -> forall (v:vertex),
~ (negative_cycle v)).
Theorem key_lemma_2 : forall (m:(map.Map.map vertex t)), (inv1 m
(cardinal vertices) (empty : (set (vertex* vertex)%type))) -> ((inv2 m
edges) -> forall (v:vertex), ~ (negative_cycle v)).
(* Why3 intros m h1 h2 v. *)
intros m hinv1. unfold inv2. intros hinv2.
intros v (hv, ((l1, h1), (l2, (h2a, h2b)))).
......@@ -393,4 +401,3 @@ absurd (Map.get m v = Infinite); auto.
ae.
Qed.
......@@ -39,7 +39,7 @@
</theory>
<theory name="BellmanFord" sum="3edf366e70f2e60d675074f0e8f934af" expanded="true">
<goal name="key_lemma_2" expanded="true">
<proof prover="0" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="20.40"/></proof>
<proof prover="0" edited="bf_WP_BellmanFord_key_lemma_2_1.v"><result status="valid" time="19.51"/></proof>
</goal>
<goal name="WP_parameter relax" expl="VC for relax" expanded="true">
<transf name="split_goal_wp" expanded="true">
......
This diff is collapsed.
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="ae38e28d7adb31fc270172c0537012eb">
<theory name="Compiler_logic" sum="9e3a5974823767e3433defed638e833e">
<goal name="seq_wp_lemma">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../specs.mlw" expanded="true">
<theory name="VM_instr_spec" sum="7a644b37a9d4e75706a1354367239885" expanded="true">
<theory name="VM_instr_spec" sum="fe73772d4d0aefd456a2417e8dd9699e" expanded="true">
<goal name="WP_parameter ifunf" expl="VC for ifunf">
<transf name="split_goal_wp">
<goal name="WP_parameter ifunf.1" expl="1. assertion">
......@@ -217,7 +217,7 @@
<goal name="WP_parameter isetvarf.1.1" expl="1.">
<transf name="compute_specified">
<goal name="WP_parameter isetvarf.1.1.1" expl="1.">
<proof prover="1"><result status="valid" time="2.47"/></proof>
<proof prover="1"><result status="valid" time="3.13"/></proof>
</goal>
</transf>
</goal>
......
......@@ -20,7 +20,7 @@
</transf>
</goal>
</theory>
<theory name="Vm" sum="8a39716eae7f444c42b1f9cce9c81614">
<theory name="Vm" sum="60241979209704f3c99a003fd588279c">
<goal name="codeseq_at_app_right">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
......
This diff is collapsed.
......@@ -2,203 +2,198 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="10" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="4000"/>
<prover id="8" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="10" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="4000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="71145ad2d10f0f843d8e9c004fc8a374" expanded="true">
<theory name="EuclideanAlgorithm" sum="7a432e31947f2a4bd6100c41353b8564" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. postcondition">
<proof prover="2" timelimit="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="2" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>