From 4ae55518dce794de3c84e1f16798cc92435d62bf Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 26 Jan 2016 19:01:54 +0100 Subject: [PATCH] simplify stateful lifting lemmas; prove fork lemma --- barrier/heap_lang.v | 40 +++++++++-------- barrier/lifting.v | 102 +++++++++++++++++++++++++++++++------------- modures/logic.v | 12 ++++++ 3 files changed, 104 insertions(+), 50 deletions(-) diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v index be15073c..8ee263c4 100644 --- a/barrier/heap_lang.v +++ b/barrier/heap_lang.v @@ -280,22 +280,20 @@ Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop := prim_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None . -Definition reducible e: Prop := - exists σ e' σ' ef, prim_step e σ e' σ' ef. +Definition reducible e σ : Prop := + ∃ e' σ' ef, prim_step e σ e' σ' ef. -Lemma reducible_not_value e: - reducible e -> e2v e = None. +Lemma reducible_not_value e σ : + reducible e σ → e2v e = None. Proof. - intros (σ' & e'' & σ'' & ef & Hstep). destruct Hstep; simpl in *; reflexivity. + intros (e' & σ' & ef & Hstep). destruct Hstep; simpl in *; reflexivity. Qed. -Definition stuck (e : expr) : Prop := - forall K e', - e = fill K e' -> - ~reducible e'. +Definition stuck (e : expr) σ : Prop := + ∀ K e', e = fill K e' → ~reducible e' σ. -Lemma values_stuck v : - stuck (v2e v). +Lemma values_stuck v σ : + stuck (v2e v) σ. Proof. intros ?? Heq. edestruct (fill_value K) as [v' Hv']. @@ -309,9 +307,9 @@ Section step_by_value. expression has a non-value e in the hole, then K is a left sub-context of K' - in other words, e also contains the reducible expression *) -Lemma step_by_value {K K' e e'} : +Lemma step_by_value {K K' e e' σ} : fill K e = fill K' e' -> - reducible e' -> + reducible e' σ -> e2v e = None -> exists K'', K' = comp_ctx K K''. Proof. @@ -324,7 +322,7 @@ Proof. by erewrite ?v2v). Ltac bad_red Hfill e' Hred := exfalso; destruct e'; try discriminate Hfill; []; - case: Hfill; intros; subst; destruct Hred as (σ' & e'' & σ'' & ef & Hstep); + case: Hfill; intros; subst; destruct Hred as (e'' & σ'' & ef & Hstep); inversion Hstep; done || (clear Hstep; subst; eapply fill_not_value2; last ( try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl; @@ -451,14 +449,14 @@ Section Language. |}. Next Obligation. intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2. - eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption. + eapply fill_not_value. eapply reducible_not_value. do 3 eexists; eassumption. Qed. Next Obligation. intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep). subst. move: (Hatomic). rewrite (atomic_fill e1' K). - rewrite !fill_empty. eauto using atomic_step. - assumption. - - clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption. + - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption. Qed. (** We can have bind with arbitrary evaluation contexts **) @@ -470,8 +468,8 @@ Section Language. exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2. split; last split; reflexivity || assumption. - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep). - destruct (step_by_value Heq1) as [K' HeqK]. - + do 4 eexists. eassumption. + destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK]. + + do 3 eexists. eassumption. + assumption. + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1. subst e1'. exists (fill K' e2''). split; first by rewrite -fill_comp. @@ -479,15 +477,15 @@ Section Language. Qed. Lemma prim_ectx_step e1 σ1 e2 σ2 ef : - reducible e1 → + reducible e1 σ1 → ectx_step e1 σ1 e2 σ2 ef → prim_step e1 σ1 e2 σ2 ef. Proof. intros Hred (K' & e1' & e2' & Heq1 & Heq2 & Hstep). - destruct (@step_by_value K' EmptyCtx e1' e1) as [K'' [HK' HK'']%comp_empty]. + destruct (@step_by_value K' EmptyCtx e1' e1 σ1) as [K'' [HK' HK'']%comp_empty]. - by rewrite fill_empty. - done. - - apply reducible_not_value. do 4 eexists; eassumption. + - eapply reducible_not_value. do 3 eexists; eassumption. - subst K' K'' e1 e2. by rewrite !fill_empty. Qed. diff --git a/barrier/lifting.v b/barrier/lifting.v index fbe2509d..d8e14c7c 100644 --- a/barrier/lifting.v +++ b/barrier/lifting.v @@ -1,5 +1,5 @@ Require Export barrier.parameter. -Require Import prelude.gmap iris.lifting. +Require Import prelude.gmap iris.lifting barrier.heap_lang. Import uPred. (* TODO RJ: Figure out a way to to always use our Σ. *) @@ -11,7 +11,35 @@ Proof. by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx. Qed. -(** Base axioms for core primitives of the language. *) +(** 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. + (* RJ FIXME WTF the bound names of wp_lift_step *changed*?!?? *) + intros ? He Hsafe Hstep. + 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. (* TODO RJ: Figure out some better way to make the postcondition a predicate over a *location* *) @@ -23,11 +51,9 @@ Lemma wp_alloc E σ 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); + (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = 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. + - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done. rewrite v2v in Hv. inversion_clear Hv. eexists; split_ands; done. - (* RJ FIXME: Need to find a fresh location. *) admit. @@ -36,9 +62,9 @@ Proof. - (* 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 forall_intro=>e2. apply forall_intro=>σ2. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. - apply const_elim_l. intros [l [-> [-> [Hl ->]]]]. rewrite right_id. + apply const_elim_l. intros [l [-> [-> Hl]]]. rewrite -wp_value'; last reflexivity. erewrite <-exist_intro with (a := l). apply and_intro. + by apply const_intro. @@ -50,21 +76,17 @@ Lemma wp_load E σ l 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. + (φ := λ 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. - 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 forall_intro=>e2. apply forall_intro=>σ2. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. - apply const_elim_l. intros [-> [-> ->]]. rewrite right_id. + apply const_elim_l. intros [-> ->]. rewrite -wp_value. apply and_intro. + by apply const_intro. + done. @@ -72,25 +94,47 @@ 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]>σ)). + 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. + (φ := λ 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. - 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 forall_intro=>e2. apply forall_intro=>σ2. apply wand_intro_l. rewrite right_id. rewrite -pvs_intro. - apply const_elim_l. intros [-> [-> ->]]. rewrite right_id. + apply const_elim_l. intros [-> ->]. rewrite -wp_value'; last reflexivity. apply and_intro. + by apply const_intro. + done. Qed. + +(** 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. diff --git a/modures/logic.v b/modures/logic.v index c8a8666c..3f31b923 100644 --- a/modures/logic.v +++ b/modures/logic.v @@ -454,6 +454,18 @@ Proof. intros H; apply impl_intro_l. by rewrite -H and_elim_l. Qed. +Lemma const_intro_l φ Q R : + φ → (■φ ∧ Q) ⊑ R → Q ⊑ R. +Proof. + intros ? <-. apply and_intro; last done. + by apply const_intro. +Qed. +Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R. +Proof. + (* FIXME RJ: Why does this not work? rewrite (commutative uPred_and Q (■φ)%I). *) + intros ? <-. apply and_intro; first done. + by apply const_intro. +Qed. Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R. Proof. intros; apply const_elim with φ; eauto. Qed. Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R. -- GitLab