diff --git a/theories/examples/generative.v b/theories/examples/generative.v index 42dbc5a7672dd0ebe2d9c5c972c5d05f6493e5f4..3ddf3751be5f849b252d7642dd27ecd19d7c8edc 100644 --- a/theories/examples/generative.v +++ b/theories/examples/generative.v @@ -163,20 +163,22 @@ Qed. Hint Resolve cell1_typed : typeable. Definition cell2 : val := - Λ: let: "l" := newlock #() in - Pack ( λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in - release "l";; "v" - , λ: "r", acquire "l";; - let: "v" := - if: !(Fst (Fst "r")) - then !(Snd "r") - else !(Snd (Fst "r")) in - release "l";; - "v" - , λ: "r" "x", acquire "l";; - (if: !(Fst (Fst "r")) - then (Snd (Fst "r")) <- "x";; (Fst (Fst "r")) <- #false - else (Snd "r") <- "x";; (Fst (Fst "r")) <- #true);; + Λ: Pack ( λ: "x", (ref #false, ref "x", ref "x", newlock #()) + , λ: "r", let: "l" := (Snd "r") in + acquire "l";; + let: "v" := + if: !(Fst (Fst (Fst "r"))) + then !(Snd (Fst "r")) + else !(Snd (Fst (Fst "r"))) in + release "l";; + "v" + , λ: "r" "x", let: "l" := (Snd "r") in + acquire "l";; + (if: !(Fst (Fst (Fst "r"))) + then (Snd (Fst (Fst "r"))) <- "x";; + (Fst (Fst (Fst "r"))) <- #false + else (Snd (Fst "r")) <- "x";; + (Fst (Fst (Fst "r"))) <- #true);; release "l"). Lemma cell2_typed Γ : typed Γ cell2 cellτ. @@ -184,125 +186,58 @@ Proof. unfold cellτ. unlock cell2. solve_typed. econstructor. - econstructor. 2: solve_typed. - econstructor. - eapply TPack with (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))). + eapply TPack with (TProd (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))) (Tref TBool)). asimpl. econstructor; solve_typed. econstructor; solve_typed. + econstructor; solve_typed. + econstructor; solve_typed. + econstructor; solve_typed. + econstructor; solve_typed. Qed. Hint Resolve cell2_typed : typeable. -Definition refPool := gset ((loc * loc * loc) * loc). -Definition refPoolR := gsetUR ((loc * loc * loc) * loc). - -Class refPoolG Σ := RefPoolG -{ refPool_inG :> authG Σ refPoolR }. - Section cell_refinement. - Context `{logrelG Σ, lockG Σ, refPoolG Σ}. + Context `{logrelG Σ, lockG Σ}. Notation D := (prodC valC valC -n> iProp Σ). - Definition cellInt (R : D) (r1 r2 r3 r : loc) : iProp Σ := + Definition lockR (R : D) (r1 r2 r3 r : loc) : iProp Σ := (∃ (a b c : val), r ↦ₛ a ∗ r2 ↦ᵢ b ∗ r3 ↦ᵢ c ∗ - ( (r1 ↦ᵢ #true ∗ R (c, a)) - ∨ (r1 ↦ᵢ #false ∗ R (b, a))))%I. - - Definition cellRegInv (P : refPool) (R : D) : iProp Σ := - ([∗ set] rs ∈ P, match rs with - | ((r1, r2, r3), r) => cellInt R r1 r2 r3 r - end)%I. + ( (r1 ↦ᵢ #true ∗ R (c, a)) + ∨ (r1 ↦ᵢ #false ∗ R (b, a))))%I. - Definition cellInv γ R : iProp Σ := - (∃ (P : refPool), own γ (● P) ∗ cellRegInv P R)%I. + Definition cellInt (R : D) (r1 r2 r3 l r : loc) : iProp Σ := + (∃ γ N, is_lock N γ #l (lockR R r1 r2 r3 r))%I. - Program Definition cellR (γ : gname) : D := λne vv, - (∃ r1 r2 r3 r : loc, ⌜vv.1 = (#r1, #r2, #r3)%V⌝ ∗ ⌜vv.2 = #r⌝ - ∗ own γ (◯ {[(r1, r2, r3), r]}))%I. + Program Definition cellR (R : D) : D := λne vv, + (∃ r1 r2 r3 l r : loc, ⌜vv.1 = (#r1, #r2, #r3, #l)%V⌝ ∗ ⌜vv.2 = #r⌝ + ∗ cellInt R r1 r2 r3 l r)%I. Next Obligation. solve_proper. Qed. - Instance cellR_persistent γ ww : PersistentP (cellR γ ww). + Instance cellR_persistent R ww : PersistentP (cellR R ww). Proof. apply _. Qed. - Lemma cellRegInv_excl (P : refPool) R (r1 r2 r3 r : loc) (v : val) : - cellRegInv P R -∗ r1 ↦ᵢ v -∗ ⌜(r1, r2, r3, r) ∉ P⌝. - Proof. - rewrite /cellRegInv. - iIntros "HP Hr1". - iAssert (⌜(r1, r2, r3, r) ∈ P⌝ → False)%I as %Hbaz. - { - iIntros (HP). - rewrite (big_sepS_elem_of _ P _ HP). - iDestruct "HP" as (a b c) "(Hr & Hr2 & Hr3 & Hrs)". - iDestruct "Hrs" as "[[Hr1' ?]|[Hr1' ?]]"; - iDestruct (mapsto_valid_2 r1 with "Hr1' Hr1") as %Hfoo; - compute in Hfoo; contradiction. - } - iPureIntro. eauto. - Qed. - - Lemma cellRegInv_open (P : refPool) R (r1 r2 r3 r : loc) : - (r1, r2, r3, r) ∈ P → - cellRegInv P R -∗ - (cellInt R r1 r2 r3 r) ∗ (cellInt R r1 r2 r3 r -∗ cellRegInv P R). - Proof. - iIntros (Hrin) "Hreg". - rewrite /cellRegInv. - iDestruct (big_sepS_elem_of_acc _ P (r1, r2, r3, r) with "Hreg") as "[Hrs Hreg]"; first assumption. - by iFrame. - Qed. - - Lemma refPool_alloc γ (P : refPool) (r1 r2 r3 r : loc) : - (r1, r2, r3, r) ∉ P → - own γ (● P) - ==∗ own γ (● ({[(r1, r2, r3, r)]} ∪ P)) - ∗ own γ (◯ ({[(r1, r2, r3, r)]})). - Proof. - iIntros (Hin) "HP". - iMod (own_update with "HP") as "[HP Hfrag]". - { eapply auth_update_alloc. - eapply (gset_local_update _ _ ({[(r1, r2, r3, r)]} ∪ P)). - apply union_subseteq_r. } - iFrame. - rewrite -gset_op_union auth_frag_op. - by iDestruct "Hfrag" as "[\$ _]". - Qed. - - Lemma refPool_lookup γ (P : refPool) (r1 r2 r3 r : loc) : - own γ (● P) -∗ - own γ (◯ {[(r1, r2), r3, r]}) -∗ - ⌜(r1, r2, r3, r) ∈ P⌝. - Proof. - iIntros "Ho Hrs". - iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo. - iPureIntro. - apply auth_valid_discrete in Hfoo. - simpl in Hfoo. destruct Hfoo as [Hfoo _]. - revert Hfoo. rewrite left_id. - by rewrite gset_included elem_of_subseteq_singleton. - Qed. - Lemma cell2_cell1_refinement Γ : Γ ⊨ cell2 ≤log≤ cell1 : cellτ. Proof. iIntros (Δ). unlock cell2 cell1 cellτ. - pose (N:=logrelN.@"locked"). - assert (Closed (dom _ Γ) (let: "l" := newlock #() in - Pack - (λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in - release "l";; "v", + assert (Closed (dom _ Γ) (Pack + (λ: "x", (ref #false, ref "x", ref "x", newlock #()), λ: "r", + let: "l" := Snd "r" in acquire "l" ;; - let: "v" := if: ! (Fst (Fst "r")) then - ! (Snd "r") else ! (Snd (Fst "r")) in + let: "v" := if: ! (Fst (Fst (Fst "r"))) then + ! (Snd (Fst "r")) else ! (Snd (Fst (Fst "r"))) in release "l" ;; "v", λ: "r" "x", + let: "l" := Snd "r" in acquire "l" ;; - (if: ! (Fst (Fst "r")) - then Snd (Fst "r") <- "x" ;; Fst (Fst "r") <- #false - else Snd "r" <- "x" ;; - Fst (Fst "r") <- #true) ;; release "l"))). + (if: ! (Fst (Fst (Fst "r"))) + then Snd (Fst (Fst "r")) <- "x" ;; + Fst (Fst (Fst "r")) <- #false + else Snd (Fst "r") <- "x" ;; Fst (Fst (Fst "r")) <- #true) ;; + release "l"))%E). { apply Closed_mono with ∅; eauto. set_solver. } assert (Closed (dom _ Γ) (Pack (λ: "x", ref "x", λ: "r", ! "r", λ: "r" "x", "r" <- "x"))). @@ -310,86 +245,68 @@ Section cell_refinement. set_solver. } iApply bin_log_related_tlam; auto. iIntros (R HR) "!#". - iApply fupd_logrel'. - iMod (own_alloc (● (∅ : refPoolR))) as (γ) "Ho"; first done. - iModIntro. - rel_apply_l (bin_log_related_newlock_l N (cellInv γ R)%I with "[Ho]"). - { iExists _. iFrame. unfold cellRegInv. - by rewrite big_sepS_empty. } - iIntros (lk γl) "#Hlk". - rel_let_l. - iApply (bin_log_related_pack _ (cellR γ)). + iApply (bin_log_related_pack _ (cellR R)). repeat iApply bin_log_related_pair. - (* New cell *) iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/= #Hv". rel_let_l. rel_let_r. - rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. - iIntros "Hl". - iDestruct 1 as (P) "[Ho HP]". - rel_let_l. + rel_alloc_r as r "Hr". rel_alloc_l as r1 "Hr1". rel_alloc_l as r2 "Hr2". rel_alloc_l as r3 "Hr3". - rel_alloc_r as r "Hr". - rel_let_l. - iDestruct (cellRegInv_excl with "HP Hr1") as %Hrs. - iApply fupd_logrel'. - iMod (refPool_alloc γ P r1 r2 r3 r with "Ho") as "[Ho #Hrs]"; first apply Hrs. - iModIntro. - rel_apply_l (bin_log_related_release_l with "Hlk Hl [-Hrs]"); first auto. - { iExists _; iFrame. rewrite {2}/cellRegInv. - rewrite big_sepS_insert; last assumption. - iFrame. iExists _,_,_. iFrame. iRight; by iFrame. } - rel_let_l. - rel_vals. iModIntro. iAlways. iExists _,_,_,_. eauto. + pose (N:=logrelN.@(r1,r)). + rel_apply_l (bin_log_related_newlock_l N (lockR R r1 r2 r3 r)%I with "[-]"). + { iExists _,_,_. iFrame. + iRight. by iFrame. } + iIntros (lk γl) "#Hlk". + rel_vals. iModIntro. iAlways. + iExists _,_,_,_,_. repeat iSplit; eauto. + iExists _,_. by iFrame. - (* Read cell *) iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/=". - iDestruct 1 as (r1 r2 r3 r) "[% [% #Hrs]]". simplify_eq. + iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq. + rel_let_l. rel_proj_l. rel_let_l. + rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk". + rel_apply_l (bin_log_related_acquire_l with "Hlk"); first auto. + iIntros "Htok". + rewrite /lockR. iDestruct 1 as (a b c) "(Hr & Hr2 & Hr3 & Hr1)". rel_let_l. - rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. - iIntros "Hl". - iDestruct 1 as (P) "[Ho HP]". - rel_let_l. repeat rel_proj_l. - iDestruct (refPool_lookup with "Ho Hrs") as %Hrin. - iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin. - iDestruct "Hr" as (a b c) "(Hr & Hr2 & Hr3 & [[Hr1 #HR] | [Hr1 #HR]])"; - rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l; - rel_let_r; rel_load_r. - + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. - { iExists _; iFrame. iApply "HclP". - iExists _,_,_; iFrame. iLeft; by iFrame. } + repeat rel_proj_l. + rel_let_r. rel_load_r. + iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]"; + rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l. + + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. + { iExists _,_,_; iFrame. iLeft; by iFrame. } rel_let_l. rel_vals; eauto. - + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. - { iExists _; iFrame. iApply "HclP". - iExists _,_,_; iFrame. iRight; by iFrame. } + + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. + { iExists _,_,_; iFrame. iRight; by iFrame. } rel_let_l. rel_vals; eauto. - (* Insert cell *) iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/=". - iDestruct 1 as (r1 r2 r3 r) "[% [% #Hrs]]". simplify_eq. + iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq. rel_let_l. rel_let_r. iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/= #Hv". - rel_let_l. rel_let_r. - rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. - iIntros "Hl". - iDestruct 1 as (P) "[Ho HP]". - rel_let_l. repeat rel_proj_l. - iDestruct (refPool_lookup with "Ho Hrs") as %Hrin. - iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin. - iDestruct "Hr" as (a b c) "(Hr & Hr2 & Hr3 & [[Hr1 #HR] | [Hr1 #HR]])"; - rel_load_l; rel_if_l; repeat rel_proj_l; - rel_store_l; rel_let_l; repeat rel_proj_l; - rel_store_l; rel_store_r; rel_let_l. - + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. - { iExists _; iFrame. iApply "HclP". - iExists _,_,_; iFrame. iRight; by iFrame. } + rel_let_l. rel_proj_l. rel_let_l. rel_let_r. + rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk". + rel_apply_l (bin_log_related_acquire_l with "Hlk"); first auto. + iIntros "Htok". + rewrite /lockR. iDestruct 1 as (a b c) "(Hr & Hr2 & Hr3 & Hr1)". + rel_let_l. + repeat rel_proj_l. + rel_store_r. + iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]"; + rel_load_l; rel_if_l; + repeat rel_proj_l; rel_store_l; rel_seq_l; + repeat rel_proj_l; rel_store_l; rel_seq_l. + + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. + { iExists _,_,_; iFrame. iRight; by iFrame. } iApply bin_log_related_unit. - + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. - { iExists _; iFrame. iApply "HclP". - iExists _,_,_; iFrame. iLeft; by iFrame. } + + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. + { iExists _,_,_; iFrame. iLeft; by iFrame. } iApply bin_log_related_unit. Qed. End cell_refinement.