lifting.v 4.11 KB
Newer Older
 Ralf Jung committed Jan 26, 2016 1 2 3 4 ``````Require Export barrier.parameter. Require Import prelude.gmap iris.lifting. 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 ``````(** Base axioms for core primitives of the language. *) (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) `````` Ralf Jung committed Jan 26, 2016 18 19 ``````(* TODO RJ: There is probably a specialized version of the lifting lemma that would be useful here. *) `````` Ralf Jung committed Jan 26, 2016 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 ``````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 := σ) (φ := λ e' σ' ef, ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None ∧ ef = None); last first. - intros e2 σ2 ef Hstep%prim_ectx_step; last first. { exists ∅. do 3 eexists. eapply AllocS with (l:=0); by rewrite ?v2v. } inversion_clear Hstep. 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. apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. apply const_elim_l. intros [l [-> [-> [Hl ->]]]]. rewrite right_id. 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 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` 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 := σ) (φ := λ e' σ' ef, e' = v2e v ∧ σ' = σ ∧ ef = None); last first. - intros e2 σ2 ef Hstep%prim_ectx_step; last first. { exists σ. do 3 eexists. eapply LoadS; eassumption. } move: Hl. inversion_clear Hstep=>{σ}. rewrite Hlookup. case=>->. done. - do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); []. eapply LoadS; eassumption. - reflexivity. - reflexivity. - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). apply sep_mono; first done. rewrite -later_intro. apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. apply const_elim_l. intros [-> [-> ->]]. rewrite right_id. rewrite -wp_value. apply and_intro. + by apply const_intro. + done. Qed. Lemma wp_store E σ l v v': σ !! l = Some v' → ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v)) (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)). Proof. intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ) (φ := λ e' σ' ef, e' = LitUnit ∧ σ' = <[l:=v]>σ ∧ ef = None); last first. - intros e2 σ2 ef Hstep%prim_ectx_step; last first. { exists σ. do 3 eexists. eapply StoreS; last (eexists; eassumption). by rewrite v2v. } move: Hl. inversion_clear Hstep=>{σ2}. rewrite v2v in Hv. inversion_clear Hv. done. - do 3 eexists. exists EmptyCtx. do 2 eexists. split_ands; try (by rewrite fill_empty); []. eapply StoreS; last (eexists; eassumption). by rewrite v2v. - reflexivity. - reflexivity. - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True). apply sep_mono; first done. rewrite -later_intro. apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. apply const_elim_l. intros [-> [-> ->]]. rewrite right_id. rewrite -wp_value'; last reflexivity. apply and_intro. + by apply const_intro. + done. Qed.``````