lifting.v 5.77 KB
 Ralf Jung committed Jan 27, 2016 1 ``````Require Import prelude.gmap iris.lifting. `````` Ralf Jung committed Jan 26, 2016 2 3 4 ``````Require Export barrier.parameter. Import uPred. `````` Ralf Jung committed Jan 26, 2016 5 6 7 8 9 10 11 12 13 ``````(* TODO RJ: Figure out a way to to always use our Σ. *) (** Bind. *) Lemma wp_bind E e K Q : wp E e (λ v, wp (Σ:=Σ) E (fill K (of_val v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q. Proof. by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx. Qed. `````` Ralf Jung committed Jan 26, 2016 14 15 16 17 18 19 20 21 22 23 24 ``````(** Base axioms for core primitives of the language: Stateful reductions *) Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 : E1 ⊆ E2 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) → pvs E2 E1 (ownP (Σ:=Σ) σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP (Σ:=Σ) σ2) -★ pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q)) ⊑ wp (Σ:=Σ) E2 e1 Q. Proof. intros ? He Hsafe Hstep. `````` Ralf Jung committed Jan 26, 2016 25 `````` (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *) `````` Ralf Jung committed Jan 26, 2016 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` etransitivity; last eapply wp_lift_step with (σ2 := σ1) (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first. - intros e2 σ2 ef Hstep'%prim_ectx_step; last done. by apply Hstep. - destruct Hsafe as (e' & σ' & ? & ?). do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); eassumption. - done. - eassumption. - apply pvs_mono. apply sep_mono; first done. apply later_mono. apply forall_mono=>e2. apply forall_mono=>σ2. apply forall_intro=>ef. apply wand_intro_l. rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ. rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r. apply pvs_mono. rewrite right_id. done. Qed. `````` Ralf Jung committed Jan 26, 2016 43 44 45 `````` (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) `````` Ralf Jung committed Jan 26, 2016 46 47 ``````(* TODO RJ: There is probably a specialized version of the lifting lemma that would be useful here. *) `````` Ralf Jung committed Jan 26, 2016 48 49 50 51 52 53 ``````Lemma wp_alloc E σ v: ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v)) (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). Proof. (* RJ FIXME: rewrite would be nicer... *) etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 54 `````` (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None); `````` Ralf Jung committed Jan 26, 2016 55 `````` last first. `````` Ralf Jung committed Jan 26, 2016 56 `````` - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done. `````` Ralf Jung committed Jan 26, 2016 57 58 `````` rewrite v2v in Hv. inversion_clear Hv. eexists; split_ands; done. `````` Ralf Jung committed Jan 27, 2016 59 60 61 `````` - set (l := fresh \$ dom (gset loc) σ). exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first by rewrite v2v. apply (not_elem_of_dom (D := gset loc)). apply is_fresh. `````` Ralf Jung committed Jan 26, 2016 62 63 64 65 66 `````` - reflexivity. - reflexivity. - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *) rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). apply sep_mono; first done. rewrite -later_intro. `````` Ralf Jung committed Jan 26, 2016 67 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 68 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 69 `````` apply const_elim_l. intros [l [-> [-> Hl]]]. `````` Ralf Jung committed Jan 26, 2016 70 71 72 73 `````` rewrite -wp_value'; last reflexivity. erewrite <-exist_intro with (a := l). apply and_intro. + by apply const_intro. + done. `````` Ralf Jung committed Jan 27, 2016 74 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 75 76 77 78 79 80 `````` Lemma wp_load E σ l v: σ !! l = Some v → ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Load (Loc l)) (λ v', ■(v' = v) ∧ ownP (Σ:=Σ) σ). Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 81 82 83 84 `````` (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}. rewrite Hlookup. case=>->. done. - do 3 eexists. eapply LoadS; eassumption. `````` Ralf Jung committed Jan 26, 2016 85 86 87 88 `````` - reflexivity. - reflexivity. - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). apply sep_mono; first done. rewrite -later_intro. `````` Ralf Jung committed Jan 26, 2016 89 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 90 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 91 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 26, 2016 92 93 94 95 96 97 98 `````` rewrite -wp_value. apply and_intro. + by apply const_intro. + done. Qed. Lemma wp_store E σ l v v': σ !! l = Some v' → `````` Ralf Jung committed Jan 26, 2016 99 100 `````` ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v)) (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). `````` Ralf Jung committed Jan 26, 2016 101 102 ``````Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 103 104 105 106 `````` (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}. rewrite v2v in Hv. inversion_clear Hv. done. - do 3 eexists. eapply StoreS; last (eexists; eassumption). by rewrite v2v. `````` Ralf Jung committed Jan 26, 2016 107 108 109 110 `````` - reflexivity. - reflexivity. - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). apply sep_mono; first done. rewrite -later_intro. `````` Ralf Jung committed Jan 26, 2016 111 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 112 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 113 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 26, 2016 114 115 116 117 `````` rewrite -wp_value'; last reflexivity. apply and_intro. + by apply const_intro. + done. Qed. `````` Ralf Jung committed Jan 26, 2016 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 `````` (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e : ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ _, True). Proof. etransitivity; last eapply wp_lift_pure_step with (φ := λ e' ef, e' = LitUnit ∧ ef = Some e); last first. - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first. { do 3 eexists. eapply ForkS. } inversion_clear Hstep. done. - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); []. eapply ForkS. - reflexivity. - apply later_mono. apply forall_intro=>e2. apply forall_intro=>ef. apply impl_intro_l. apply const_elim_l. intros [-> ->]. (* FIXME RJ This is ridicolous. *) transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I; first by rewrite left_id. apply sep_mono; last reflexivity. rewrite -wp_value'; reflexivity. Qed.``````