diff --git a/barrier/proof.v b/barrier/proof.v index c0392b89a7d784ce1346d2ab5c31f228ea060e9c..ac18c35cfd4b9995395887708313a245a9de408b 100644 --- a/barrier/proof.v +++ b/barrier/proof.v @@ -10,10 +10,10 @@ Import uPred. (* Not bundling heapG, as it may be shared with other users. *) Class barrierG Σ := BarrierG { barrier_stsG :> stsG heap_lang Σ sts; - barrier_savedPropG :> savedPropG heap_lang Σ (laterCF idCF); + barrier_savedPropG :> savedPropG heap_lang Σ idCF; }. (** The Functors we need. *) -Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF (laterCF idCF)]. +Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF]. (* Show and register that they match. *) Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ. Proof. destruct H as (?&?&?). split; apply _. Qed. @@ -26,7 +26,7 @@ Local Notation iProp := (iPropG heap_lang Σ). Definition ress (P : iProp) (I : gset gname) : iProp := (∃ Ψ : gname → iProp, - ▷ (P -★ Π★{set I} Ψ) ★ Π★{set I} (λ i, saved_prop_own i (Next (Ψ i))))%I. + ▷ (P -★ Π★{set I} Ψ) ★ Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I. Coercion state_to_val (s : state) : val := match s with State Low _ => #0 | State High _ => #1 end. @@ -48,7 +48,7 @@ Definition send (l : loc) (P : iProp) : iProp := Definition recv (l : loc) (R : iProp) : iProp := (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★ - saved_prop_own i (Next Q) ★ ▷ (Q -★ R))%I. + saved_prop_own i Q ★ ▷ (Q -★ R))%I. Global Instance barrier_ctx_always_stable (γ : gname) (l : loc) (P : iProp) : AlwaysStable (barrier_ctx γ l P). @@ -79,8 +79,8 @@ Proof. solve_proper. Qed. (** Helper lemmas *) Lemma ress_split i i1 i2 Q R1 R2 P I : i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 → - (saved_prop_own i2 (Next R2) ★ - saved_prop_own i1 (Next R1) ★ saved_prop_own i (Next Q) ★ + (saved_prop_own i2 R2 ★ + saved_prop_own i1 R1 ★ saved_prop_own i Q ★ (Q -★ R1 ★ R2) ★ ress P I) ⊑ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))). Proof. @@ -89,9 +89,9 @@ Proof. rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //. do 4 (rewrite big_sepS_insert; last set_solver). rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert. - set savedQ := _ i _. set savedΨ := _ i _. + set savedQ := _ i Q. set savedΨ := _ i (Ψ _). sep_split left: [savedQ; savedΨ; Q -★ _; ▷ (_ -★ Π★{set I} _)]%I. - - rewrite !assoc saved_prop_agree later_equivI /=. strip_later. + - rewrite !assoc saved_prop_agree /=. strip_later. apply wand_intro_l. to_front [P; P -★ _]%I. rewrite wand_elim_r. rewrite (big_sepS_delete _ I i) //. sep_split right: [Π★{set _} _]%I. @@ -119,13 +119,13 @@ Proof. apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l. rewrite !assoc. apply pvs_wand_r. (* The core of this proof: Allocating the STS and the saved prop. *) - eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF idCF) _ (Next P)). + eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ P). rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l. apply exist_elim=>i. trans (pvs ⊤ ⊤ (heap_ctx heapN ★ - ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i (Next P))). + ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i P)). - rewrite -pvs_intro. cancel [heap_ctx heapN]. - rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)]. + rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i P]. rewrite /barrier_inv /ress -later_intro. cancel [l ↦ #0]%I. rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I). by rewrite !big_sepS_singleton /= wand_diag -later_intro. @@ -217,8 +217,8 @@ Proof. rewrite !sep_exist_r. apply exist_mono=>Ψ. rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep. ecancel [▷ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I. - apply wand_intro_l. set savedΨ := _ i _. set savedQ := _ i _. - to_front [savedΨ; savedQ]. rewrite saved_prop_agree later_equivI /=. + apply wand_intro_l. set savedΨ := _ i (Ψ _). set savedQ := _ i Q. + to_front [savedΨ; savedQ]. rewrite saved_prop_agree /=. wp_op; [|done]=> _. wp_if. rewrite !assoc. eapply wand_apply_r'; first done. eapply wand_apply_r'; first done. apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I. @@ -240,11 +240,11 @@ Proof. apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc. apply const_elim_sep_l=>Hs. rewrite /pvs_fsa. eapply sep_elim_True_l. - { eapply saved_prop_alloc_strong with (x := Next R1) (G := I). } + { eapply saved_prop_alloc_strong with (x := R1) (G := I). } rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r. apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc. apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l. - { eapply saved_prop_alloc_strong with (x := Next R2) (G := I ∪ {[ i1 ]}). } + { eapply saved_prop_alloc_strong with (x := R2) (G := I ∪ {[ i1 ]}). } rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r. apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc. apply const_elim_sep_l=>Hi2. diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v index e0543d70ea5dfb76b603bbd2f38379a8170c5c46..51fd60d86c3e985c32cb601e8057a30d1cc008d4 100644 --- a/program_logic/saved_prop.v +++ b/program_logic/saved_prop.v @@ -4,18 +4,18 @@ Import uPred. Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) := SavedPropG { - saved_prop_F_contractive :> cFunctorContractive F; - saved_prop_inG :> inG Λ Σ (agreeR (F (iPreProp Λ (globalF Σ)))); + saved_prop_F_contractive :> cFunctorNe F; + saved_prop_inG :> inG Λ Σ (agreeR \$ laterC (F (iPreProp Λ (globalF Σ)))); }. -Definition savedPropGF (F : cFunctor) `{cFunctorContractive F} : - gFunctor := GFunctor (agreeRF F). -Instance inGF_savedPropG `{cFunctorContractive F} +Definition savedPropGF (F : cFunctor) `{cFunctorNe F} : + gFunctor := GFunctor (agreeRF \$ laterCF F). +Instance inGF_savedPropG `{cFunctorNe F} `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F. Proof. split; try apply _; apply: inGF_inG. Qed. Definition saved_prop_own `{savedPropG Λ Σ F} (γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ := - own γ (to_agree (cFunctor_map F (iProp_fold, iProp_unfold) x)). + own γ (to_agree \$ Next (cFunctor_map F (iProp_fold, iProp_unfold) x)). Typeclasses Opaque saved_prop_own. Instance: Params (@saved_prop_own) 4. @@ -36,16 +36,16 @@ Section saved_prop. Proof. by apply own_alloc. Qed. Lemma saved_prop_agree γ x y : - (saved_prop_own γ x ★ saved_prop_own γ y) ⊑ (x ≡ y). + (saved_prop_own γ x ★ saved_prop_own γ y) ⊑ ▷(x ≡ y). Proof. - rewrite -own_op own_valid agree_validI agree_equivI. + rewrite -own_op own_valid agree_validI agree_equivI later_equivI. set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)). set (G2 := cFunctor_map F (@iProp_unfold Λ (globalF Σ), @iProp_fold Λ (globalF Σ))). assert (∀ z, G2 (G1 z) ≡ z) as help. { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id. apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. } - rewrite -{2}[x]help -{2}[y]help. + rewrite -{2}[x]help -{2}[y]help. apply later_mono. apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I; first solve_proper; auto with I. Qed. diff --git a/program_logic/tests.v b/program_logic/tests.v index 4f39e8b27171bccc6637b5cafe1ffbcd82c9d396..ceb9e9dff0ba0a0de48177d87f7c64d6caecd286 100644 --- a/program_logic/tests.v +++ b/program_logic/tests.v @@ -9,14 +9,14 @@ End ModelTest. Module SavedPropTest. (* Test if we can really go "crazy higher order" *) Section sec. - Definition F := laterCF (cofe_morCF idCF idCF). + Definition F := (cofe_morCF idCF idCF). Definition Σ : gFunctors := #[ savedPropGF F ]. Context {Λ : language}. Notation iProp := (iPropG Λ Σ). Local Instance : savedPropG Λ Σ F := _. - Definition own_pred γ (φ : laterC (iProp -n> iProp)) : iProp := + Definition own_pred γ (φ : iProp -n> iProp) : iProp := saved_prop_own γ φ. End sec. End SavedPropTest.