(* Projet Coq - WP - MPRI 2.7.1 *) (***** Partie 1 : definition de While ****************************************) Require Import ZArith.BinInt. Require Import Omega. Import Z. Definition Var := nat. Definition Mem := Var -> Z. Definition Expr:= Mem -> Z. Inductive Instr : Type := | skip: Instr | abort: Instr | assign: Var -> Expr -> Instr | seq: Instr -> Instr -> Instr | ifelse: Expr -> Instr -> Instr -> Instr | while: Expr -> Instr -> Instr. Definition ifonly (exp: Expr) (inst: Instr) : Instr := ifelse exp inst skip. (***** CPO *******************************************************************) Fixpoint nat_eq x y := match x, y with | 0, 0 => true | 0, S _ => false | S _, 0 => false | S x0, S y0 => nat_eq x0 y0 end. Definition Sequence (S: Type) := nat -> S. Inductive cpo (T: Type): Type := | CpoError: (cpo T) | CpoElem: T -> (cpo T). Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop := fun T x y => match x, y with | CpoError _, _ => True | CpoElem _ x0, CpoElem _ y0 => x0 = y0 | _, _ => False end. Arguments cpo_leq {T} _ _. Infix "cpo<=" := cpo_leq (at level 100). Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop := fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)). Arguments is_chain {T} _. Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop := fun T chain elt => forall (n: nat), (chain n) cpo<= elt. Arguments is_lub_of {T} _ _. Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T. Arguments find_lub {T} _. Axiom find_lub_correct: forall (T: Type), forall (chain: Sequence (cpo T)), is_chain chain -> is_lub_of chain (find_lub chain). Arguments find_lub_correct {T} {chain} _. (***** Interpretation ********************************************************) Definition subst: Mem -> Var -> Z -> Mem := fun (m: Mem) (v: Var) (z: Z) (v2: Var) => if nat_eq v v2 then z else m v2. Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity). Definition MemCpo := cpo Mem. Definition MemError := CpoError Mem. Definition MemElem := CpoElem Mem. Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo := match mem with | CpoError _ => MemError | CpoElem _ mem0 => match inst with | skip => MemElem mem0 | abort => MemError | assign v e => (MemElem (mem0 [v <- (e mem0)])) | seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0)) | ifelse guard instrIf instrElse => if ((guard mem0) =? 0) % Z then interp instrElse mem else interp instrIf mem | while guard body => let fix while_chain (mem: MemCpo) (n: nat): MemCpo := match n with | 0 => mem | S m => match while_chain (MemElem mem0) m with | CpoError _ => MemError | CpoElem _ submem => if ((guard submem) =? 0) % Z then interp body (MemElem submem) else mem end end in find_lub (fun n => match while_chain (MemElem mem0) n with | CpoError _ => MemError | CpoElem _ submem => if ((guard submem) =? 0) % Z then MemError else MemElem submem end) end end. Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr := match n with | 0 => skip | S m => seq (nth_iterate instr m) instr end. Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with | CpoError _ => False | CpoElem _ mem0 => (expr mem0 <> 0) % Z end. Infix "|=e" := satisfies_expr (at level 32). Definition expr_neg (expr: Expr) : Expr := fun mem => match expr mem with | 0%Z => 1%Z | _ => 0%Z end. Lemma certain_termination_exists body guard mem : interp (while guard body) mem <> MemError -> exists n: nat, interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard. Proof. intros noError. Admitted. Lemma certain_termination_exists_minimal body guard mem : interp (while guard body) mem <> MemError -> exists n: nat, (forall p: nat, p < n -> interp (nth_iterate (ifonly guard body) p) mem |=e guard) /\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard. Proof. intros not_error. Admitted. Lemma certain_termination body guard mem : interp (while guard body) mem <> MemError -> exists n: nat, (interp (nth_iterate body n) mem) |=e (expr_neg guard) /\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard) /\ interp (while guard body) mem = interp (nth_iterate body n) mem. Proof. intros notError. elim (certain_termination_exists_minimal body guard mem). intros n. intros [notBeforeN atN]. exists n. split. Admitted. (***** Validite, prouvabilite pour Hoare *************************************) Definition Assert := Mem -> Prop. Delimit Scope assert with assert. Definition assertTop : Assert := fun _ => True. Definition assertBot : Assert := fun _ => False. Definition assertNot : Assert -> Assert := fun orig mem => ~ (orig mem). Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert. Definition assertAnd : Assert -> Assert -> Assert := fun x1 x2 mem => (x1 mem) /\ (x2 mem). Infix "/\" := assertAnd : assert. Definition assertOr : Assert -> Assert -> Assert := fun x1 x2 mem => (x1 mem) \/ (x2 mem). Infix "\/" := assertOr : assert. Definition assertImpl : Assert -> Assert -> Assert := fun x1 x2 => (~x1 \/ x2) % assert. Infix "->" := assertImpl : assert. Definition assertForall : Var -> Assert -> Assert := fun ident asser mem => forall (z: Z), asser (mem [ident <- z]). Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert. Definition existsForall : Var -> Assert -> Assert := fun ident asser mem => exists (z: Z), asser (mem [ident <- z]). Notation "'exists' x" := (existsForall x) (at level 87, no associativity): assert. Definition assertMemForall : Assert -> Assert := fun asser mem => forall (mem: Mem), asser mem. Notation "'\-/m' x" := (assertMemForall x) (at level 90, no associativity): assert. Definition existsMemForall : Assert -> Assert := fun asser mem => exists (mem: Mem), asser mem. Notation "'exists_m' x" := (existsMemForall x) (at level 87, no associativity): assert. Definition substAssert : Assert -> Var -> Z -> Assert := fun asser ident val mem => asser (mem [ident <- val]). Notation "a [[ x <- z ]]" := (substAssert a x z) (at level 50, left associativity). Definition substAssertExpr : Assert -> Var -> Expr -> Assert := fun asser ident expr mem => asser (mem [ident <- (expr mem)]). Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z) (at level 50, left associativity). Definition assertOfExpr : Expr -> Assert := fun expr mem => (expr mem <> 0)%Z. Definition assertImplLogical (a1 a2: Assert): Prop := forall (m: Mem), (a1 m) -> (a2 m). (***** Hoare provability *****************************************************) Reserved Notation "|- [| x |] y [| z |]" (at level 30). Inductive hoare_provability : Assert -> Instr -> Assert -> Prop := | H_skip: forall pre, hoare_provability pre skip pre | H_abort: forall pre, forall post, hoare_provability pre abort post | H_assign: forall post, forall (x: Var), forall (e: Expr), (|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert | H_conseq: forall pre, forall post, forall pre', forall post', forall s, (|- [| pre' |] s [| post' |]) % assert -> (assertImplLogical pre pre') -> (assertImplLogical post' post) -> (|- [| pre |] s [| post |]) % assert | H_seq: forall pre, forall mid, forall post, forall s1, forall s2, (|- [|pre|] s1 [|mid|]) % assert -> (|- [|mid|] s2 [|post|]) % assert -> (|- [|pre|] (seq s1 s2) [|post|]) % assert | H_if: forall pre, forall post, forall expr, forall sIf, forall sElse, (|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert -> (|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert -> (|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert | H_while: forall inv, forall expr, forall sBody, (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert -> (|- [| inv |] (while expr sBody) [| inv /\ ~ (assertOfExpr expr) |]) % assert where "|- [| pre |] instr [| post |]" := (hoare_provability pre instr post) : assert. (***** Hoare: provability implies consequence ********************************) Definition conseq_or_bottom (y: Assert) (m: MemCpo) := match m with | CpoError _ => True | CpoElem _ m0 => y m0 end. Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) := forall mem: Mem, (pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))). Notation "|= [| pre |] instr [| post |]" := (hoare_consequence pre instr post) (at level 30): assert. Lemma weaken_in_conseq: forall a1, forall a2, forall m, assertImplLogical a1 a2 -> conseq_or_bottom a1 m -> conseq_or_bottom a2 m. Proof. intros a1 a2 m impl conseq. destruct m. - apply conseq. - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq. Qed. Lemma interp_of_error (s: Instr): interp s (MemError) = MemError. Proof. unfold MemError. destruct s; cbv; trivial. Qed. Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) : conseq_or_bottom y (MemElem m) -> y m. Proof. intros src; unfold conseq_or_bottom; simpl; trivial. Qed. Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat): interp (nth_iterate s (S n)) (MemElem m) = interp s (interp (nth_iterate s n) (MemElem m)). Proof. simpl; congruence. Qed. Lemma error_leads_to_no_success s: forall m, interp s MemError <> MemElem m. Proof. intros mem. unfold interp; destruct s; simpl ; unfold MemElem; unfold MemError; congruence. Qed. Lemma expr_neg_consistency (expr: Expr): forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem. Proof. intros mem. intros src. unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel. + congruence. + elimtype False. unfold expr_neg in src; rewrite exprRel in src. apply src. congruence. + elimtype False. unfold expr_neg in src; rewrite exprRel in src. apply src. congruence. Qed. Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem): interp (nth_iterate s (S n)) (MemElem sMem) = MemElem m -> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0 /\ interp s (MemElem m0) = MemElem m. Proof. intro HSn. destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel. - rewrite (unfold_one_iter s sMem n) in HSn. rewrite nRel in HSn. apply error_leads_to_no_success in HSn. elimtype False. apply HSn. - exists m0; unfold MemElem. split. * trivial. * rewrite <- nRel; simpl. apply HSn. Qed. Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem): n1 < n2 -> interp (nth_iterate s n2) (MemElem sMem) = MemElem m -> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0. Proof. intros nRel eventuallySound. assert (forall nDecr, nDecr <= n2 - n1 -> exists m0, interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0). * intros mDecr mDecrRel. induction mDecr. + exists m. assert (n2 = n2 - 0). { unfold Nat.sub. destruct n2; trivial. } { rewrite <- H. assumption. } + assert (mDecr <= n2 - n1). { omega. } { elim (IHmDecr H). intros memNext memNextRel. elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext). intros memNow [memNowRel memNowInterp]. exists memNow. apply memNowRel. assert (S (n2 - S mDecr) = n2 - mDecr). omega. rewrite H0. apply memNextRel. } * assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0). intros memRes memResRel. exists memRes. assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel. assumption. Qed. Lemma unwrap_CpoElem (T: Type) : forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2. Proof. intros m1 m2 cpoEq. congruence. Qed. Theorem hoare_provability_implies_consequence : forall (pre: Assert), forall (s: Instr), forall (post: Assert), ( |- [| pre |] s [| post |] ) % assert -> ( |= [| pre |] s [| post |] ) % assert. Proof. intros pre instr post. intros deduction. induction deduction; intros mem preInMem. - exact preInMem. - simpl; trivial. - exact preInMem. - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0). apply IHdeduction. apply H. exact preInMem. - simpl; destruct (interp s1 (MemElem mem)) eqn:mRel. * fold MemError. rewrite (interp_of_error s2); simpl; trivial. * apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1. specialize IHdeduction1 with mem as IH1_mem. rewrite mRel in IH1_mem. apply IH1_mem. assumption. - simpl; destruct (expr mem =? 0)%Z eqn:branchEqn. * apply (IHdeduction2 mem). unfold assertOfExpr. unfold assertAnd. split. + assumption. + unfold assertNot. rewrite <- Z.eqb_eq. congruence. * apply (IHdeduction1 mem). unfold assertOfExpr. unfold assertAnd. split. + assumption. + rewrite <- Z.eqb_eq. congruence. - unfold conseq_or_bottom. destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel. * trivial. * elim (certain_termination sBody expr (MemElem mem)). intros n [lastIter [notLastIter isWhile] ]. rewrite isWhile in interpRel. destruct n. { simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel. unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split. { rewrite interpRel in preInMem; assumption. } { apply expr_neg_consistency; rewrite <- interpRel; assumption. } } unfold assertAnd; split. + apply conseq_or_bottom_is_conseq. unfold MemElem. rewrite <- interpRel. assert (forall n1, n1 <= (S n) -> conseq_or_bottom inv (interp (nth_iterate sBody n1) (MemElem mem))). { induction n1. { intros obvious. simpl. assumption. } { intros order; simpl. unfold hoare_consequence in IHdeduction. assert (n1 < S n) as nOrder. omega. elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel). intros memN relMemN. specialize (IHdeduction memN) as IHmem. rewrite relMemN. apply IHmem. unfold assertAnd; split. { rewrite relMemN in IHn1; unfold MemElem in IHn1. apply IHn1. omega. } { unfold assertOfExpr. specialize (notLastIter n1). rewrite relMemN in notLastIter. unfold satisfies_expr in notLastIter; simpl in notLastIter. apply notLastIter. assumption. } } } { apply H. omega. } + unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter. unfold satisfies_expr in lastIter. unfold expr_neg in lastIter. destruct (expr m); simpl; congruence. + rewrite interpRel; unfold MemError; congruence. Qed. (***** Weakest precondition **************************************************) Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with | skip => cond | abort => assertTop | assign x expr => (cond [[ x <- expr expr ]]) | seq s1 s2 => wp s1 (wp s2 cond) | ifelse guard sIf sElse => ((assertOfExpr guard -> wp sIf cond) /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert | while guard body => assertBot end. Lemma assertImplElim {a b: Assert} : forall (m: Mem), (assertImpl a b) m -> a m -> b m. Proof. intros mem impl pa. unfold assertImpl in impl; unfold assertOr in impl. destruct impl. * elimtype False. unfold assertNot in H. apply (H pa). * assumption. Qed. Lemma assertImplSelf (a: Assert) : assertImplLogical a a. Proof. unfold assertImplLogical. intros mem x. assumption. Qed. Lemma preBottomIsCorrect {instr post}: (|= [|assertBot|] instr [|post|]) % assert. Proof. unfold hoare_consequence. intros mem. unfold assertBot. intros F; exfalso; exact F. Qed. Theorem wp_correctness (instr: Instr): forall post, ( |= [| wp instr post |] instr [| post |] ) % assert. Proof. induction instr; intros post. * apply hoare_provability_implies_consequence. apply (H_skip post). * apply hoare_provability_implies_consequence. apply (H_abort assertTop post). * apply hoare_provability_implies_consequence. apply (H_assign post v e). * apply hoare_provability_implies_consequence. remember (wp instr2 (Some post)) as mid eqn:midRel. remember (wp instr1 mid) as pre eqn:preRel. simpl; rewrite <- midRel; rewrite <- preRel. specialize IHinstr2 with (Some post0) as IHpost. specialize IHinstr1 with mid as IHmid. rewrite <- midRel in IHpost; rewrite <- preRel in IHmid. destruct mid as [mid0 | ] eqn:mid0Rel. destruct pre as [pre0 | ] eqn: pre0Rel. apply (H_seq pre0 mid0 post0). apply IHmid. apply IHpost. + unfold whatever_or_none; trivial. + destruct pre. - unfold provable_or_none in IHmid; unfold whatever_or_none in IHmid. exfalso. apply IHmid. - unfold whatever_or_none; trivial. * apply hoare_provability_implies_consequence. specialize IHinstr1 with (Some post0); specialize IHinstr2 with (Some post0). destruct (wp instr1 (Some post0)) as [preIf | ] eqn:preIfRel; destruct (wp instr2 (Some post0)) as [preElse | ] eqn:preElseRel. remember ((assertOfExpr e -> preIf) /\ (~ assertOfExpr e -> preElse)) % assert as pre0 eqn:pre0Rel. assert (wp (ifelse e instr1 instr2) (Some post0) = (Some pre0)). { rewrite pre0Rel; simpl; rewrite preIfRel; rewrite preElseRel; congruence. } { rewrite H. apply (H_if pre0 post0 e instr1 instr2). - apply (H_conseq (pre0 /\ assertOfExpr e)%assert post0 preIf post0 instr1 IHinstr1). + rewrite pre0Rel. unfold assertImplLogical. intros mem [ [disjunctIf disjunctElse] isIf]. apply (assertImplElim mem disjunctIf isIf). + apply (assertImplSelf post0). - apply (H_conseq (pre0 /\ ~ assertOfExpr e)%assert post0 preElse post0 instr2 IHinstr2). + rewrite pre0Rel. unfold assertImplLogical. intros mem [ [disjunctIf disjunctElse] isElse]. apply (assertImplElim mem disjunctElse isElse). + apply (assertImplSelf post0). } - unfold provable_or_none; simpl; rewrite preElseRel; rewrite preIfRel; trivial. - unfold provable_or_none; simpl; rewrite preElseRel; rewrite preIfRel; trivial. - unfold provable_or_none; simpl; rewrite preElseRel; rewrite preIfRel; trivial. * unfold wp. apply preBottomIsCorrect. Qed. Lemma provable_opt_implies_provable {pre instr post} : (|-opt [|Some pre|] instr [|Some post|])%assert -> (|- [|pre|] instr [|post|])%assert. Proof. intros prf. unfold provable_or_none in prf; unfold whatever_or_none in prf. assumption. Qed. Theorem wp_correctness (instr: Instr) : forall post, ( |=opt [| wp instr post |] instr [| post |] ) % assert. Proof. intros post. destruct post as [post0 | ] eqn:post0Rel. remember (wp instr (Some post0)) as pre eqn:preRel. destruct pre as [ pre0 | ] eqn:pre0Rel. - unfold consequence_or_none; unfold whatever_or_none. apply hoare_provability_implies_consequence. apply provable_opt_implies_provable. rewrite preRel. apply wp_correctness_provable. - unfold consequence_or_none; unfold whatever_or_none; trivial. - unfold wp. destruct instr; unfold consequence_or_none; unfold whatever_or_none; trivial. Qed. (* vim: ts=2 sw=2 *)