lifting.v 7.46 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 ``````(* TODO RJ: Figure out a way to to always use our Σ. *) (** Bind. *) Lemma wp_bind E e K Q : `````` Ralf Jung committed Jan 27, 2016 9 `````` wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q. `````` Ralf Jung committed Jan 26, 2016 10 11 12 13 ``````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 46 47 48 49 `````` (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) Lemma wp_alloc E σ v: ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v)) (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). Proof. `````` Ralf Jung committed Jan 27, 2016 50 `````` (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *) `````` Ralf Jung committed Jan 26, 2016 51 `````` etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 52 `````` (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None); `````` Ralf Jung committed Jan 26, 2016 53 `````` last first. `````` Ralf Jung committed Jan 26, 2016 54 `````` - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done. `````` Ralf Jung committed Jan 26, 2016 55 56 `````` rewrite v2v in Hv. inversion_clear Hv. eexists; split_ands; done. `````` Ralf Jung committed Jan 27, 2016 57 58 59 `````` - 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 60 61 62 63 64 `````` - 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 65 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 66 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 67 `````` apply const_elim_l. intros [l [-> [-> Hl]]]. `````` Ralf Jung committed Jan 26, 2016 68 69 70 71 `````` 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 72 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 73 74 75 76 77 78 `````` 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 79 80 81 82 `````` (φ := λ 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 83 84 85 86 `````` - 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 87 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 88 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 89 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 26, 2016 90 91 92 93 94 95 96 `````` 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 97 98 `````` ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v)) (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). `````` Ralf Jung committed Jan 26, 2016 99 100 ``````Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 101 102 103 104 `````` (φ := λ 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 105 106 107 108 `````` - 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 109 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 110 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 111 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 26, 2016 112 113 114 115 `````` rewrite -wp_value'; last reflexivity. apply and_intro. + by apply const_intro. + done. Qed. `````` Ralf Jung committed Jan 26, 2016 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 `````` (** 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. `````` 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 `````` Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 : to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) → (▷ ∀ e2, ■ φ e2 → wp (Σ:=Σ) E e2 Q) ⊑ wp (Σ:=Σ) E e1 Q. Proof. intros He Hsafe Hstep. (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *) etransitivity; last eapply wp_lift_pure_step with (φ0 := λ e' ef, ef = None ∧ φ e'); last first. - intros σ1 e2 σ2 ef Hstep'%prim_ectx_step; last done. by apply Hstep. - intros σ1. destruct (Hsafe σ1) as (e' & σ' & ? & ?). do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); eassumption. - done. - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef. apply impl_intro_l. apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r. rewrite right_id. done. Qed. `````` Ralf Jung committed Jan 27, 2016 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 `````` Lemma wp_rec' E e v P Q : P ⊑ wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q → ▷P ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q. Proof. intros HP. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = e.[Rec e, v2e v /]); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep. done. - intros ?. do 3 eexists. eapply BetaS. by rewrite v2v. - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. done. Qed. Lemma wp_lam E e v P Q : P ⊑ wp (Σ:=Σ) E (e.[v2e v/]) Q → ▷P ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q. Proof. intros HP. rewrite -wp_rec'; first (intros; apply later_mono; eassumption). (* RJ: This pulls in functional extensionality. If that bothers us, we have to talk to the Autosubst guys. *) by asimpl. Qed. ``````