lifting.v 8.05 KB
 Ralf Jung committed Jan 27, 2016 1 ``````Require Import prelude.gmap iris.lifting. `````` Ralf Jung committed Jan 27, 2016 2 ``````Require Export iris.weakestpre barrier.parameter. `````` Ralf Jung committed Jan 26, 2016 3 4 ``````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 `````` (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) `````` Ralf Jung committed Jan 27, 2016 46 47 48 ``````Lemma wp_alloc E σ e v: e2v e = Some v → ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc e) `````` Ralf Jung committed Jan 26, 2016 49 50 `````` (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). Proof. `````` Ralf Jung committed Jan 27, 2016 51 `````` (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *) `````` Ralf Jung committed Jan 27, 2016 52 `````` intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 53 `````` (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None); `````` Ralf Jung committed Jan 26, 2016 54 `````` last first. `````` Ralf Jung committed Jan 26, 2016 55 `````` - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done. `````` Ralf Jung committed Jan 27, 2016 56 `````` rewrite Hv in Hvl. inversion_clear Hvl. `````` Ralf Jung committed Jan 26, 2016 57 `````` eexists; split_ands; done. `````` Ralf Jung committed Jan 27, 2016 58 `````` - set (l := fresh \$ dom (gset loc) σ). `````` Ralf Jung committed Jan 27, 2016 59 `````` exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done. `````` Ralf Jung committed Jan 27, 2016 60 `````` apply (not_elem_of_dom (D := gset loc)). apply is_fresh. `````` Ralf Jung committed Jan 26, 2016 61 62 63 64 65 `````` - 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 66 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 67 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 68 `````` apply const_elim_l. intros [l [-> [-> Hl]]]. `````` Ralf Jung committed Jan 26, 2016 69 70 71 72 `````` 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 73 ``````Qed. `````` Ralf Jung committed Jan 26, 2016 74 75 76 77 78 79 `````` 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 80 81 82 `````` (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}. rewrite Hlookup. case=>->. done. `````` Ralf Jung committed Jan 27, 2016 83 `````` - do 3 eexists. econstructor; eassumption. `````` Ralf Jung committed Jan 26, 2016 84 85 86 87 `````` - 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 88 `````` apply forall_intro=>e2. apply forall_intro=>σ2. `````` Ralf Jung committed Jan 26, 2016 89 `````` apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. `````` Ralf Jung committed Jan 26, 2016 90 `````` apply const_elim_l. intros [-> ->]. `````` Ralf Jung committed Jan 26, 2016 91 92 93 94 95 `````` rewrite -wp_value. apply and_intro. + by apply const_intro. + done. Qed. `````` Ralf Jung committed Jan 27, 2016 96 97 ``````Lemma wp_store E σ l e v v': e2v e = Some v → `````` Ralf Jung committed Jan 26, 2016 98 `````` σ !! l = Some v' → `````` Ralf Jung committed Jan 27, 2016 99 100 `````` ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) e) (λ v', ■(v' = LitUnitV) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). `````` Ralf Jung committed Jan 26, 2016 101 ``````Proof. `````` Ralf Jung committed Jan 27, 2016 102 `````` intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) `````` Ralf Jung committed Jan 26, 2016 103 104 `````` (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first. - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}. `````` Ralf Jung committed Jan 27, 2016 105 106 `````` rewrite Hvl in Hv. inversion_clear Hv. done. - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption. `````` 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 `````` (** Base axioms for core primitives of the language: Stateless reductions *) Lemma wp_fork E e : `````` Ralf Jung committed Jan 27, 2016 122 `````` ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ v, ■(v = LitUnitV)). `````` Ralf Jung committed Jan 26, 2016 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 ``````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. `````` Ralf Jung committed Jan 27, 2016 141 142 `````` rewrite -wp_value'; last reflexivity. by apply const_intro. `````` Ralf Jung committed Jan 26, 2016 143 ``````Qed. `````` 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 `````` 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 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 `````` 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. `````` Ralf Jung committed Jan 27, 2016 191 192 193 194 195 196 197 198 199 200 201 202 203 204 ``````Lemma wp_plus n1 n2 E P Q : P ⊑ Q (LitNatV (n1 + n2)) → ▷P ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q. Proof. intros HP. etransitivity; last eapply wp_lift_pure_step with (φ := λ e', e' = LitNat (n1 + n2)); last first. - intros ? ? ? ? Hstep. inversion_clear Hstep; done. - intros ?. do 3 eexists. econstructor. - reflexivity. - apply later_mono, forall_intro=>e2. apply impl_intro_l. apply const_elim_l=>->. rewrite -wp_value'; last reflexivity; done. Qed.``````