lifting.v 5.65 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 59 60 61 62 63 64 `````` rewrite v2v in Hv. inversion_clear Hv. eexists; split_ands; done. - (* RJ FIXME: Need to find a fresh location. *) admit. - 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 72 `````` rewrite -wp_value'; last reflexivity. erewrite <-exist_intro with (a := l). apply and_intro. + by apply const_intro. + done. Abort. `````` 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.``````