Commit c4ec91d6 by Dan Frumin

### A more reasonable reference cell refinement example

parent a7ff7a8d
 ... @@ -163,20 +163,22 @@ Qed. ... @@ -163,20 +163,22 @@ Qed. Hint Resolve cell1_typed : typeable. Hint Resolve cell1_typed : typeable. Definition cell2 : val := Definition cell2 : val := Λ: let: "l" := newlock #() in Λ: Pack ( λ: "x", (ref #false, ref "x", ref "x", newlock #()) Pack ( λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in , λ: "r", let: "l" := (Snd "r") in release "l";; "v" acquire "l";; , λ: "r", acquire "l";; let: "v" := let: "v" := if: !(Fst (Fst (Fst "r"))) if: !(Fst (Fst "r")) then !(Snd (Fst "r")) then !(Snd "r") else !(Snd (Fst (Fst "r"))) in else !(Snd (Fst "r")) in release "l";; release "l";; "v" "v" , λ: "r" "x", let: "l" := (Snd "r") in , λ: "r" "x", acquire "l";; acquire "l";; (if: !(Fst (Fst "r")) (if: !(Fst (Fst (Fst "r"))) then (Snd (Fst "r")) <- "x";; (Fst (Fst "r")) <- #false then (Snd (Fst (Fst "r"))) <- "x";; else (Snd "r") <- "x";; (Fst (Fst "r")) <- #true);; (Fst (Fst (Fst "r"))) <- #false else (Snd (Fst "r")) <- "x";; (Fst (Fst (Fst "r"))) <- #true);; release "l"). release "l"). Lemma cell2_typed Γ : Lemma cell2_typed Γ : typed Γ cell2 cellτ. typed Γ cell2 cellτ. ... @@ -184,125 +186,58 @@ Proof. ... @@ -184,125 +186,58 @@ Proof. unfold cellτ. unlock cell2. unfold cellτ. unlock cell2. solve_typed. solve_typed. econstructor. econstructor. econstructor. 2: solve_typed. eapply TPack with (TProd (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))) (Tref TBool)). econstructor. eapply TPack with (TProd (TProd (Tref TBool) (Tref (TVar 0))) (Tref (TVar 0))). asimpl. asimpl. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. econstructor; solve_typed. Qed. Qed. Hint Resolve cell2_typed : typeable. 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. Section cell_refinement. Context `{logrelG Σ, lockG Σ, refPoolG Σ}. Context `{logrelG Σ, lockG Σ}. Notation D := (prodC valC valC -n> iProp Σ). 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 ∗ (∃ (a b c : val), r ↦ₛ a ∗ r2 ↦ᵢ b ∗ r3 ↦ᵢ c ∗ ( (r1 ↦ᵢ #true ∗ R (c, a)) ( (r1 ↦ᵢ #true ∗ R (c, a)) ∨ (r1 ↦ᵢ #false ∗ R (b, a))))%I. ∨ (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. Definition cellInv γ R : iProp Σ := Definition cellInt (R : D) (r1 r2 r3 l r : loc) : iProp Σ := (∃ (P : refPool), own γ (● P) ∗ cellRegInv P R)%I. (∃ γ N, is_lock N γ #l (lockR R r1 r2 r3 r))%I. Program Definition cellR (γ : gname) : D := λne vv, Program Definition cellR (R : D) : D := λne vv, (∃ r1 r2 r3 r : loc, ⌜vv.1 = (#r1, #r2, #r3)%V⌝ ∗ ⌜vv.2 = #r⌝ (∃ r1 r2 r3 l r : loc, ⌜vv.1 = (#r1, #r2, #r3, #l)%V⌝ ∗ ⌜vv.2 = #r⌝ ∗ own γ (◯ {[(r1, r2, r3), r]}))%I. ∗ cellInt R r1 r2 r3 l r)%I. Next Obligation. solve_proper. Qed. Next Obligation. solve_proper. Qed. Instance cellR_persistent γ ww : PersistentP (cellR γ ww). Instance cellR_persistent R ww : PersistentP (cellR R ww). Proof. apply _. Qed. 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 Γ : Lemma cell2_cell1_refinement Γ : Γ ⊨ cell2 ≤log≤ cell1 : cellτ. Γ ⊨ cell2 ≤log≤ cell1 : cellτ. Proof. Proof. iIntros (Δ). iIntros (Δ). unlock cell2 cell1 cellτ. unlock cell2 cell1 cellτ. pose (N:=logrelN.@"locked"). assert (Closed (dom _ Γ) (Pack assert (Closed (dom _ Γ) (let: "l" := newlock #() in (λ: "x", (ref #false, ref "x", ref "x", newlock #()), Pack (λ: "x", acquire "l";; let: "v" := (ref #false, ref "x", ref "x") in release "l";; "v", λ: "r", λ: "r", let: "l" := Snd "r" in acquire "l" ;; acquire "l" ;; let: "v" := if: ! (Fst (Fst "r")) then let: "v" := if: ! (Fst (Fst (Fst "r"))) then ! (Snd "r") else ! (Snd (Fst "r")) in ! (Snd (Fst "r")) else ! (Snd (Fst (Fst "r"))) in release "l" ;; "v", release "l" ;; "v", λ: "r" "x", λ: "r" "x", let: "l" := Snd "r" in acquire "l" ;; acquire "l" ;; (if: ! (Fst (Fst "r")) (if: ! (Fst (Fst (Fst "r"))) then Snd (Fst "r") <- "x" ;; Fst (Fst "r") <- #false then Snd (Fst (Fst "r")) <- "x" ;; else Snd "r" <- "x" ;; Fst (Fst (Fst "r")) <- #false Fst (Fst "r") <- #true) ;; release "l"))). else Snd (Fst "r") <- "x" ;; Fst (Fst (Fst "r")) <- #true) ;; release "l"))%E). { apply Closed_mono with ∅; eauto. { apply Closed_mono with ∅; eauto. set_solver. } set_solver. } assert (Closed (dom _ Γ) (Pack (λ: "x", ref "x", λ: "r", ! "r", λ: "r" "x", "r" <- "x"))). assert (Closed (dom _ Γ) (Pack (λ: "x", ref "x", λ: "r", ! "r", λ: "r" "x", "r" <- "x"))). ... @@ -310,86 +245,68 @@ Section cell_refinement. ... @@ -310,86 +245,68 @@ Section cell_refinement. set_solver. } set_solver. } iApply bin_log_related_tlam; auto. iApply bin_log_related_tlam; auto. iIntros (R HR) "!#". iIntros (R HR) "!#". iApply fupd_logrel'. iApply (bin_log_related_pack _ (cellR R)). 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 γ)). repeat iApply bin_log_related_pair. repeat iApply bin_log_related_pair. - (* New cell *) - (* New cell *) iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/= #Hv". iAlways. iIntros (v1 v2) "/= #Hv". rel_let_l. rel_let_r. rel_let_l. rel_let_r. rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. rel_alloc_r as r "Hr". iIntros "Hl". iDestruct 1 as (P) "[Ho HP]". rel_let_l. rel_alloc_l as r1 "Hr1". rel_alloc_l as r1 "Hr1". rel_alloc_l as r2 "Hr2". rel_alloc_l as r2 "Hr2". rel_alloc_l as r3 "Hr3". rel_alloc_l as r3 "Hr3". rel_alloc_r as r "Hr". pose (N:=logrelN.@(r1,r)). rel_let_l. rel_apply_l (bin_log_related_newlock_l N (lockR R r1 r2 r3 r)%I with "[-]"). iDestruct (cellRegInv_excl with "HP Hr1") as %Hrs. { iExists _,_,_. iFrame. iApply fupd_logrel'. iRight. by iFrame. } iMod (refPool_alloc γ P r1 r2 r3 r with "Ho") as "[Ho #Hrs]"; first apply Hrs. iIntros (lk γl) "#Hlk". iModIntro. rel_vals. iModIntro. iAlways. rel_apply_l (bin_log_related_release_l with "Hlk Hl [-Hrs]"); first auto. iExists _,_,_,_,_. repeat iSplit; eauto. { iExists _; iFrame. rewrite {2}/cellRegInv. iExists _,_. by iFrame. rewrite big_sepS_insert; last assumption. iFrame. iExists _,_,_. iFrame. iRight; by iFrame. } rel_let_l. rel_vals. iModIntro. iAlways. iExists _,_,_,_. eauto. - (* Read cell *) - (* Read cell *) iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/=". 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_let_l. rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. repeat rel_proj_l. iIntros "Hl". rel_let_r. rel_load_r. iDestruct 1 as (P) "[Ho HP]". iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]"; rel_let_l. repeat rel_proj_l. rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l. iDestruct (refPool_lookup with "Ho Hrs") as %Hrin. + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin. { iExists _,_,_; iFrame. iLeft; by iFrame. } 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. } rel_let_l. rel_vals; eauto. rel_let_l. rel_vals; eauto. + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. { iExists _; iFrame. iApply "HclP". { iExists _,_,_; iFrame. iRight; by iFrame. } iExists _,_,_; iFrame. iRight; by iFrame. } rel_let_l. rel_vals; eauto. rel_let_l. rel_vals; eauto. - (* Insert cell *) - (* Insert cell *) iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/=". 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. rel_let_l. rel_let_r. iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (v1 v2) "/= #Hv". iAlways. iIntros (v1 v2) "/= #Hv". rel_let_l. rel_let_r. rel_let_l. rel_proj_l. rel_let_l. rel_let_r. rel_apply_l (bin_log_related_acquire_l N _ lk with "Hlk"); first auto. rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk". iIntros "Hl". rel_apply_l (bin_log_related_acquire_l with "Hlk"); first auto. iDestruct 1 as (P) "[Ho HP]". iIntros "Htok". rel_let_l. repeat rel_proj_l. rewrite /lockR. iDestruct 1 as (a b c) "(Hr & Hr2 & Hr3 & Hr1)". iDestruct (refPool_lookup with "Ho Hrs") as %Hrin. rel_let_l. iDestruct (cellRegInv_open with "HP") as "[Hr HclP]"; first apply Hrin. repeat rel_proj_l. iDestruct "Hr" as (a b c) "(Hr & Hr2 & Hr3 & [[Hr1 #HR] | [Hr1 #HR]])"; rel_store_r. rel_load_l; rel_if_l; repeat rel_proj_l; iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]"; rel_store_l; rel_let_l; repeat rel_proj_l; rel_load_l; rel_if_l; rel_store_l; rel_store_r; rel_let_l. repeat rel_proj_l; rel_store_l; rel_seq_l; + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. repeat rel_proj_l; rel_store_l; rel_seq_l. { iExists _; iFrame. iApply "HclP". + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. iExists _,_,_; iFrame. iRight; by iFrame. } { iExists _,_,_; iFrame. iRight; by iFrame. } iApply bin_log_related_unit. iApply bin_log_related_unit. + rel_apply_l (bin_log_related_release_l with "Hlk Hl [-]"); auto. + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. { iExists _; iFrame. iApply "HclP". { iExists _,_,_; iFrame. iLeft; by iFrame. } iExists _,_,_; iFrame. iLeft; by iFrame. } iApply bin_log_related_unit. iApply bin_log_related_unit. Qed. Qed. End cell_refinement. End cell_refinement.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment