Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit e9fb4453 authored by MARCHE Claude's avatar MARCHE Claude

final lemme for blocking sematnics

parent ad1b6642
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -555,6 +554,14 @@ Axiom many_steps_seq : forall (sigma1:(map mident value)) (sigma3:(map mident
pi2 Sskip n1) /\ ((many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2) /\
(n = ((1%Z + n1)%Z + n2)%Z)).
Axiom type_preservation : forall (s1:stmt) (s2:stmt) (sigma1:(map mident
value)) (sigma2:(map mident value)) (pi1:(list (ident* value)%type))
(pi2:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list
(ident* datatype)%type)), ((type_stmt sigmat pit s1) /\
((compatible_env sigma1 sigmat pi1 pit) /\ (one_step sigma1 pi1 s1 sigma2
pi2 s2))) -> ((type_stmt sigmat pit s2) /\ (compatible_env sigma2 sigmat
pi2 pit)).
(* Why3 assumption *)
Definition valid_triple(p:fmla) (s:stmt) (q:fmla): Prop := forall (sigma:(map
mident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
......@@ -568,32 +575,109 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint stmt_writes(s:stmt) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint stmt_writes(s:stmt) (w:(set1 mident)) {struct s}: Prop :=
match s with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (set.Set.mem id w)
| (Sassign id _) => (mem1 id w)
| (Sseq s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Sif t s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ body) => (stmt_writes body w)
......@@ -683,27 +767,21 @@ generalize Hnpos.
pattern n; apply Z_lt_induction; auto.
intros x Hind Hxpos.
intros.
assert (h: (x = 0 \/ 0 < x)%Z) by omega.
destruct h.
(* cas x = 0 *)
clear Hind; subst x.
inversion h1; subst; clear h1.
(* cas zero etapes *)
destruct (decide_is_skip s').
subst s'.
split; auto.
contradiction h2.
contradiction h2; clear h2.
apply progress2 with (q:=q) (1:=Hcomp); auto.
generalize (steps_non_neg _ _ _ _ _ _ _ H7).
intros; elimtype False; omega.
(* cas x > 0 *)
inversion h1; subst; clear h1.
elimtype False; omega.
apply Hind with (y:=n0) (sigmat:=sigmat) (pit:=pit) (5:=H1);
auto with zarith.
admit. (* TODO: compatible_env preserved by reduction *)
admit. (* TODO: type preserved by reduction *)
apply wp_reduction with (1:=H0).
auto.
(* cas au moins une etape *)
generalize (steps_non_neg _ _ _ _ _ _ _ H0).
intro.
generalize (type_preservation s s2 sigma sigma2 pi pi2 sigmat pit).
intros h.
apply Hind with (y:=n0) (sigmat:=sigmat) (pit:=pit) (5:=H0);
intuition.
apply wp_reduction with (1:=H); auto.
Qed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment