Commit f9dd92b9 by Asma Tafat

### blocking semantic proof

parent 41e0c512
 ... ... @@ -4,6 +4,7 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.MinMax. Require set.Set. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := ... ... @@ -575,109 +576,32 @@ 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). 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)). 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:(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:(set1 mident)), (assigns sigma a sigma). Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set mident)), (assigns sigma a sigma). Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3). value)) (sigma3:(map mident value)) (a:(set.Set.set 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:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1 sigma') -> (assigns sigma (union s1 s2) sigma'). mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)), (assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma'). Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2 sigma') -> (assigns sigma (union s1 s2) sigma'). mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)), (assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma'). (* Why3 assumption *) Fixpoint stmt_writes(s:stmt) (w:(set1 mident)) {struct s}: Prop := Fixpoint stmt_writes(s:stmt) (w:(set.Set.set mident)) {struct s}: Prop := match s with | (Sskip|(Sassert _)) => True | (Sassign id _) => (mem1 id w) | (Sassign id _) => (set.Set.mem 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) ... ... @@ -720,6 +644,9 @@ Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list Axiom monotonicity : forall (s:stmt) (p:fmla) (q:fmla), (valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (wp s p) (wp s q))). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem distrib_conj : forall (s:stmt), match s with ... ... @@ -738,22 +665,15 @@ Theorem distrib_conj : forall (s:stmt), end. destruct s; auto. simpl. intros H sigma pi p q ((H0 & H1) & (_ & H2)). intros H sigma pi p q (H0 & H1). destruct H0. destruct H1; clear H1. split; auto. apply abstract_effects_monotonic. red; simpl; intuition. with (sigma := sigma) (pi:=pi). simpl. split; apply abstract_effects_generalize in H1; simpl in H1; destruct H1; intros (H5 & _). (* True *) apply H1; auto. (* False *) clear H1. split; auto. apply abstract_effects_generalize in H2; simpl in H2; destruct H2. apply H2; auto. apply abstract_effects_generalize in H3; simpl in H3; destruct H3. Qed.
 ... ... @@ -677,6 +677,4 @@ intros. do 3 eexists. econstructor. eauto. Qed. Qed. \ No newline at end of file
This diff is collapsed.
 ... ... @@ -434,7 +434,6 @@ end (** {2 Problématique des variables fraîches} *) theory FreshVariables use import SemOp ... ... @@ -518,7 +517,7 @@ lemma subst_fresh_term : (* lemma subst_fresh : forall f:fmla, x:ident, v:ident. fresh_in_fmla x f -> subst f x v = f fresh_in_fmla x f -> subst f x v = f *) (* Needed for monotonicity and wp_reduction *) ... ... @@ -540,29 +539,12 @@ id1 <> id2 -> (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t = eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t) (* lemma eval_swap_term_2: forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t = eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t) *) lemma eval_swap: forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <-> eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f) (* lemma eval_swap_2: forall f:fmla, id1 id2:ident, v1 v2:value. id1 <> id2 -> forall sigma:env, pi:stack. (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <-> eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f) *) lemma eval_term_change_free : forall t:term, sigma:env, pi:stack, id:ident, v:value. fresh_in_term id t -> ... ... @@ -580,14 +562,6 @@ lemma eval_change_free : end (** {2 Hoare logic} *) theory HoareLogic ... ... @@ -723,6 +697,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) = end *) function fresh_from (f:fmla) : ident (* Need it for monotonicity*) ... ...
 ... ... @@ -351,6 +351,9 @@ Axiom eval_term_change_free : forall (t:term) (sigma:(map mident value)) (pi:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_term id t) -> ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem eval_change_free : forall (f:fmla), match f with ... ... @@ -366,7 +369,18 @@ Theorem eval_change_free : forall (f:fmla), (Cons (id, v) pi) f) -> (eval_fmla sigma pi f) | (Fforall i d f1) => True end. destruct f; auto. simpl. intros. destruct H0 as (h1 & h2 & h3). rewrite eval_term_change_free in H1; auto. assert (eval_fmla sigma (infix_plpl (Nil : (list (ident*value))) (Cons (i, eval_term sigma pi t) (Cons (id, v) pi))) f = eval_fmla sigma (Cons (i, eval_term sigma pi t) (Cons (id, v) pi)) f); auto. rewrite <- H0 in H1; clear H0. apply eval_swap in H1; auto. apply H in H1; auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Inductive datatype := | TYunit : datatype | TYint : datatype | TYbool : datatype . Axiom datatype_WhyType : WhyType datatype. Existing Instance datatype_WhyType. (* Why3 assumption *) Inductive value := | Vvoid : value | Vint : Z -> value | Vbool : bool -> value . Axiom value_WhyType : WhyType value. Existing Instance value_WhyType. (* Why3 assumption *) Inductive operator := | Oplus : operator | Ominus : operator | Omult : operator | Ole : operator . Axiom operator_WhyType : WhyType operator. Existing Instance operator_WhyType. Axiom mident : Type. Parameter mident_WhyType : WhyType mident. Existing Instance mident_WhyType. Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/ ~ (m1 = m2). Axiom ident : Type. Parameter ident_WhyType : WhyType ident. Existing Instance ident_WhyType. Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2). (* Why3 assumption *) Inductive term := | Tvalue : value -> term | Tvar : ident -> term | Tderef : mident -> term | Tbin : term -> operator -> term -> term . Axiom term_WhyType : WhyType term. Existing Instance term_WhyType. (* Why3 assumption *) Inductive fmla := | Fterm : term -> fmla | Fand : fmla -> fmla -> fmla | Fnot : fmla -> fmla | Fimplies : fmla -> fmla -> fmla | Flet : ident -> term -> fmla -> fmla | Fforall : ident -> datatype -> fmla -> fmla . Axiom fmla_WhyType : WhyType fmla. Existing Instance fmla_WhyType. (* Why3 assumption *) Inductive stmt := | Sskip : stmt | Sassign : mident -> term -> stmt | Sseq : stmt -> stmt -> stmt | Sif : term -> stmt -> stmt -> stmt | Sassert : fmla -> stmt | Swhile : term -> fmla -> stmt -> stmt . Axiom stmt_WhyType : WhyType stmt. Existing Instance stmt_WhyType. Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip). 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 list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Definition env := (map mident value). (* Why3 assumption *) Definition stack := (list (ident* value)%type). Parameter get_stack: ident -> (list (ident* value)%type) -> value. Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)), match pi with | Nil => ((get_stack i pi) = Vvoid) | (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) -> ((get_stack i pi) = (get_stack i r))) end. Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident* value)%type)), ((get_stack x (Cons (x, v) r)) = v). Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident* value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i r)). Parameter eval_bin: value -> operator -> value -> value. Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x, y) with | ((Vint x1), (Vint y1)) => match op with | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z)) | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z)) | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z)) | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\ ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false))) end | (_, _) => ((eval_bin x op y) = Vvoid) end. (* Why3 assumption *) Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type)) (t:term) {struct t}: value := match t with | (Tvalue v) => v | (Tvar id) => (get_stack id pi) | (Tderef id) => (get sigma id) | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)) end. (* Why3 assumption *) Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type)) (f:fmla) {struct f}: Prop := match f with | (Fterm t) => ((eval_term sigma pi t) = (Vbool true)) | (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2) | (Fnot f1) => ~ (eval_fmla sigma pi f1) | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2) | (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi) f1) | (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x, (Vint n)) pi) f1) | (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x, (Vbool b)) pi) f1) | (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1) end. (* Why3 assumption *) Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p). (* Why3 assumption *) Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt -> (map mident value) -> (list (ident* value)%type) -> stmt -> Prop := | one_step_assign : forall (sigma:(map mident value)) (sigma':(map mident value)) (pi:(list (ident* value)%type)) (x:mident) (t:term), (sigma' = (set sigma x (eval_term sigma pi t))) -> (one_step sigma pi (Sassign x t) sigma' pi Sskip) | one_step_seq_noskip : forall (sigma:(map mident value)) (sigma':(map mident value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type)) (s1:stmt) (s1':stmt) (s2:stmt), (one_step sigma pi s1 sigma' pi' s1') -> (one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1' s2)) | one_step_seq_skip : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (s:stmt), (one_step sigma pi (Sseq Sskip s) sigma pi s) | one_step_if_true : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (t:term) (s1:stmt) (s2:stmt), ((eval_term sigma pi t) = (Vbool true)) -> (one_step sigma pi (Sif t s1 s2) sigma pi s1) | one_step_if_false : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (t:term) (s1:stmt) (s2:stmt), ((eval_term sigma pi t) = (Vbool false)) -> (one_step sigma pi (Sif t s1 s2) sigma pi s2) | one_step_assert : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi (Sassert f) sigma pi Sskip) | one_step_while_true : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))) | one_step_while_false : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi inv) -> (((eval_term sigma pi cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body) sigma pi Sskip)). (* Why3 assumption *) Inductive many_steps : (map mident value) -> (list (ident* value)%type) -> stmt -> (map mident value) -> (list (ident* value)%type) -> stmt -> Z -> Prop := | many_steps_refl : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (s:stmt), (many_steps sigma pi s sigma pi s 0%Z) | many_steps_trans : forall (sigma1:(map mident value)) (sigma2:(map mident value)) (sigma3:(map mident value)) (pi1:(list (ident* value)%type)) (pi2:(list (ident* value)%type)) (pi3:(list (ident* value)%type)) (s1:stmt) (s2:stmt) (s3:stmt) (n:Z), (one_step sigma1 pi1 s1 sigma2 pi2 s2) -> ((many_steps sigma2 pi2 s2 sigma3 pi3 s3 n) -> (many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n + 1%Z)%Z)). Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident value)) (pi1:(list (ident* value)%type)) (pi2:(list (ident* value)%type)) (s1:stmt) (s2:stmt) (n:Z), (many_steps sigma1 pi1 s1 sigma2 pi2 s2 n) -> (0%Z <= n)%Z. (* Why3 assumption *) Definition reducible(sigma:(map mident value)) (pi:(list (ident* value)%type)) (s:stmt): Prop := exists sigma':(map mident value), exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s sigma' pi' s'). (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))