(* CS3234, Martin Henz and Aquinas Hobor *) (* Homework on Hoare logic soundness in Coq *) (* Some useful tactics *) Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). Ltac remembertac2 x a := let x := fresh x in let H := fresh "Heq" x in (set (x:=a) in *; assert (H: a=x) by reflexivity; clearbody x). Tactic Notation "cases" constr(a) := let x := fresh in (remembertac2 x a; destruct x). Require ClassicalFacts. (* no axioms in this line *) Require Export Coq.Logic.ClassicalChoice. (* Axioms dependent_unique_choice, relational_choice *) Tactic Notation "LEM" constr(a) := destruct (classic a). Axiom dep_extensionality: forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g. Implicit Arguments dep_extensionality. Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. Require Import ZArith. Open Local Scope Z_scope. (* You may want to look at the notes on Hoare logic and the lecture slides for help understanding this file. *) (* Total 100 poins, plus 40 points extra credit *) Definition var : Type := nat. Inductive nexp : Type := | neInt : Z -> nexp | neVar : var -> nexp | nePlus : nexp -> nexp -> nexp | neMinus : nexp -> nexp -> nexp | neTimes : nexp -> nexp -> nexp. Inductive bexp : Type := | beLE : nexp -> nexp -> bexp | beOr : bexp -> bexp -> bexp | beNot : bexp -> bexp. Definition beTrue : bexp := beLE (neInt 0) (neInt 0). Definition beFalse : bexp := beNot beTrue. Definition beAnd (b1 b2 : bexp) : bexp := beNot (beOr (beNot b1) (beNot b2)). Definition beEq (n1 n2 : nexp) : bexp := beAnd (beLE n1 n2) (beLE n2 n1). Definition beNeq (n1 n2 : nexp) : bexp := beNot (beEq n1 n2). Definition beLT (n1 n2 : nexp) : bexp := beAnd (beLE n1 n2) (beNeq n1 n2). Definition context : Type := var -> Z. Fixpoint neval (rho : context) (ne : nexp) : Z := match ne with | neInt z => z | neVar x => rho x | nePlus ne1 ne2 => (neval rho ne1) + (neval rho ne2) | neMinus ne1 ne2 => (neval rho ne1) - (neval rho ne2) | neTimes ne1 ne2 => (neval rho ne1) * (neval rho ne2) end. Fixpoint beval (rho : context) (be : bexp) : Prop := match be with | beLE n1 n2 => (neval rho n1) <= (neval rho n2) | beOr b1 b2 => (beval rho b1) \/ (beval rho b2) | beNot b => ~(beval rho b) end. Inductive Command : Type := | Skip : Command | Assign : var -> nexp -> Command | Seq : Command -> Command -> Command | If : bexp -> Command -> Command -> Command | While : bexp -> Command -> Command. Definition assert : Type := context -> Prop. Definition Top : assert := fun _ => True. Definition Bot : assert := fun _ => False. Definition And (P1 P2 : assert) : assert := fun rho => (P1 rho) /\ (P2 rho). Definition Or (P1 P2 : assert) : assert := fun rho => (P1 rho) \/ (P2 rho). Definition Impl (P1 P2 : assert) : assert := fun rho => (P1 rho) -> (P2 rho). Definition Not (P : assert) : assert := Impl P Bot. Definition Univ (A : Type) (P : A -> assert) : assert := fun rho => forall a, P a rho. Definition Exis (A : Type) (P : A -> assert) : assert := fun rho => exists a, P a rho. Definition Lift (P : Prop) : assert := fun rho => P. Definition NEval (ne : nexp) (z : Z) : assert := fun rho => neval rho ne = z. Definition BEval (be : bexp) : assert := fun rho => beval rho be. Definition relation : Type := context -> context -> Prop. Definition Box (R : relation) (P : assert) : assert := fun rho => forall rho', R rho rho' -> P rho'. Definition Diam (R : relation) (P : assert) : assert := fun rho => exists rho', R rho rho' /\ P rho'. Definition upd_ctx (rho : context) (x : var) (z : Z) : context := fun x' => if eq_nat_dec x x' then z else rho x'. Definition U (x : var) (z : Z) : relation := fun rho rho' => rho' = upd_ctx rho x z. Definition UBox (x : var) (z : Z) : assert -> assert := Box (U x z). Definition UEBox (x : var) (ne : nexp) (P : assert) : assert := fun rho => UBox x (neval rho ne) P rho. Inductive BStep : Command -> context -> context -> Prop := | bSkip : forall rho, BStep Skip rho rho | bAssign : forall x ne rho, BStep (Assign x ne) rho (upd_ctx rho x (neval rho ne)) | bSeq : forall rho rho' rho'' c1 c2, BStep c1 rho rho' -> BStep c2 rho' rho'' -> BStep (Seq c1 c2) rho rho'' | bIf1 : forall rho rho' b c1 c2, beval rho b -> BStep c1 rho rho' -> BStep (If b c1 c2) rho rho' | bIf2 : forall rho rho' b c1 c2, ~beval rho b -> BStep c2 rho rho' -> BStep (If b c1 c2) rho rho' | bWhile1 : forall rho rho' rho'' b c, beval rho b -> BStep c rho rho' -> BStep (While b c) rho' rho'' -> BStep (While b c) rho rho'' | bWhile2 : forall rho b c, ~beval rho b -> BStep (While b c) rho rho. Lemma BStep_det: forall rho c rho' rho'', BStep rho c rho' -> BStep rho c rho'' -> rho' = rho''. Proof. intros. revert rho'' H0. induction H; intros. inversion H0. trivial. inversion H0. trivial. inversion H1; subst. generalize (IHBStep1 rho'0 H4); intro. subst rho'0. generalize (IHBStep2 _ H7); intro. subst rho''0. trivial. inversion H1; subst. apply IHBStep in H8. trivial. contradiction. inversion H1; subst. contradiction. apply IHBStep in H8. trivial. inversion H2; subst. apply IHBStep1 in H6. subst rho'0. apply IHBStep2 in H9. trivial. contradiction. inversion H0; subst. contradiction. trivial. Qed. Definition SBox (c : Command) : assert -> assert := Box (BStep c). Definition SDiam (c : Command) : assert -> assert := Diam (BStep c). Definition HTriple (P : assert) (c : Command) (Q : assert) : Prop := forall rho, (Impl P (SBox c Q)) rho. Definition THTriple (P : assert) (c : Command) (Q : assert) : Prop := forall rho, (Impl P (SDiam c Q)) rho. Lemma THTriple_HTriple: forall P c Q, THTriple P c Q -> HTriple P c Q. Proof. repeat intro. generalize (H rho H0). intro. destruct H2 as [rho'' [? ?]]. replace rho' with rho''; trivial. eapply BStep_det; eauto. Qed. (* 10 marks *) Lemma HT_Skip: forall P, HTriple P Skip P. Proof. admit. Qed. (* 10 marks *) Lemma HT_Assign: forall x e P, HTriple (UEBox x e P) (Assign x e) P. Proof. admit. Qed. (* 10 marks *) Lemma HT_Seq: forall P Q R c1 c2, HTriple P c1 Q -> HTriple Q c2 R -> HTriple P (Seq c1 c2) R. Proof. admit. Qed. (* 10 marks *) Lemma HT_Cons: forall P c Q P' Q', HTriple P' c Q' -> (forall rho, (Impl P P') rho) -> (forall rho, (Impl Q' Q) rho) -> HTriple P c Q. Proof. admit. Qed. (* 10 marks *) Lemma HT_If : forall P Q b c1 c2, HTriple (And P (BEval b)) c1 Q -> HTriple (And P (Not (BEval b))) c2 Q -> HTriple P (If b c1 c2) Q. Proof. admit. Qed. (* 10 marks *) Lemma THT_Skip: forall P, THTriple P Skip P. Proof. admit. Qed. (* 10 marks *) Lemma THT_Assign: forall x e P, THTriple (UEBox x e P) (Assign x e) P. Proof. admit. Qed. (* 10 marks *) Lemma THT_Seq: forall P Q R c1 c2, THTriple P c1 Q -> THTriple Q c2 R -> THTriple P (Seq c1 c2) R. Proof. admit. Qed. (* 10 marks *) Lemma THT_Cons: forall P c Q P' Q', THTriple P' c Q' -> (forall rho, (Impl P P') rho) -> (forall rho, (Impl Q' Q) rho) -> THTriple P c Q. Proof. admit. Qed. (* 10 marks *) Lemma THT_If : forall P Q b c1 c2, THTriple (And P (BEval b)) c1 Q -> THTriple (And P (Not (BEval b))) c2 Q -> THTriple P (If b c1 c2) Q. Proof. admit. Qed. (* 20 extra credit marks *) (* Do everything else first *) Lemma HT_While : forall P b c, HTriple (And P (BEval b)) c P -> HTriple P (While b c) (And P (Not (BEval b))). Proof. admit. Qed. (* Prove that we can use the HT_While rule to verify this infinite loop *) Goal HTriple Top (While beTrue Skip) Bot. Proof. replace Bot with (And Top (Not (BEval beTrue))). apply HT_While. eapply HT_Cons. apply HT_Skip. instantiate (1 := Top). repeat intro. red. trivial. repeat intro. red. trivial. apply dep_extensionality. intro. apply prop_ext. split; intro. destruct H. red. apply H0. red. simpl. omega. inversion H. Qed. Definition term_meas : Type := context -> nat. Definition TM_prop (tm : term_meas) (J : nat -> Prop) : assert := fun ctx => J(tm ctx). Open Local Scope nat_scope. (* 20 extra credit marks *) (* Do everything else first *) Lemma THT_While : forall P b c tm, (forall n, THTriple (And P (And (BEval b) (TM_prop tm (fun n' => n' = n)))) c (And P (TM_prop tm (fun n' => n' < n)))) -> THTriple P (While b c) (And P (Not (BEval b))). Proof. admit. Qed.