Commit 9d06622c authored by Hai Dang's avatar Hai Dang
Browse files

Add agreement lemmas for readonly ptsto

parent e8362cd4
......@@ -68,6 +68,87 @@ Proof. rewrite ROSeen_eq. by apply _. Qed.
#[global] Instance ROSeen_timeless l γ v : Timeless (l ro{γ} v).
Proof. rewrite ROSeen_eq. by apply _. Qed.
Lemma ROSeen_agree' l γ v v' V V' :
@{V} l ro{γ} v - @{V'} l ro{γ} v' - v' = v .
Proof.
rewrite ROSeen_eq.
iDestruct 1 as (??) "[_ O1]". iDestruct 1 as (??) "[_ O2]".
rewrite !view_at_objective_iff.
iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
iPureIntro. by simplify_eq.
Qed.
Lemma ROSeen_agree_l l γ v v' V :
@{V} l ro{γ} v - l ro{γ} v' - v' = v .
Proof.
iIntros "O1 O2". iDestruct (view_at_intro with "O2") as (V') "[_ O2]".
iApply (ROSeen_agree' with "O1 O2").
Qed.
Lemma ROSeen_agree_r l γ v v' V' :
l ro{γ} v - @{V'} l ro{γ} v' - v' = v .
Proof.
iIntros "O1". iDestruct (view_at_intro with "O1") as (V) "[_ O1]".
iApply (ROSeen_agree' with "O1").
Qed.
Lemma ROSeen_agree l γ v v' :
l ro{γ} v - l ro{γ} v' - v' = v .
Proof.
iIntros "O1". iDestruct (view_at_intro with "O1") as (V) "[_ O1]".
iApply (ROSeen_agree_l with "O1").
Qed.
Lemma ROPtsTo_ROSeen_agree' l γ v v' V V' :
@{V} l ro{γ} v - @{V'} l ro{γ} v' - v' = v .
Proof.
rewrite ROPtsTo_eq ROSeen_eq.
iDestruct 1 as (???????) "(_&_&_&O1)". iDestruct 1 as (??) "[_ O2]".
rewrite !view_at_objective_iff.
iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
iPureIntro. by simplify_eq.
Qed.
Lemma ROPtsTo_ROSeen_agree_l l γ v v' V :
@{V} l ro{γ} v - l ro{γ} v' - v' = v .
Proof.
iIntros "O1 O2". iDestruct (view_at_intro with "O2") as (V') "[_ O2]".
iApply (ROPtsTo_ROSeen_agree' with "O1 O2").
Qed.
Lemma ROPtsTo_ROSeen_agree_r l γ v v' V' :
l ro{γ} v - @{V'} l ro{γ} v' - v' = v .
Proof.
iIntros "O1". iDestruct (view_at_intro with "O1") as (V) "[_ O1]".
iApply (ROPtsTo_ROSeen_agree' with "O1").
Qed.
Lemma ROPtsTo_ROSeen_agree l γ v v' :
l ro{γ} v - l ro{γ} v' - v' = v .
Proof.
iIntros "O1". iDestruct (view_at_intro with "O1") as (V) "[_ O1]".
iApply (ROPtsTo_ROSeen_agree_l with "O1").
Qed.
Lemma ROPtsTo_from_na l v :
l v == γ, l ro{γ} v.
Proof.
rewrite own_loc_na_eq ROPtsTo_eq /ROPtsTo_def /own_loc_na_def.
iDestruct 1 as (t m) "(Own & %VAL & #sVm)".
iDestruct "Own" as (rsa rsn ws GH) "(AL & ARL & AWL & [%Va NAL] & HC & AW)".
set C := {[t := m]}.
iDestruct (view_at_intro_incl with "AWL sVm") as (Vna) "(sVna & %LeVna & AWL)".
iMod (own_alloc (to_agree ((t,v,Vna) : leibnizO _))) as (γ) "#A"; [done|].
iIntros "!>". iExists γ, t, m, rsa, rsn, ws, Vna. iSplit; [by iPureIntro|].
iFrame "ARL AWL HC AW A". iSplitR "NAL"; [|by eauto].
rewrite seen_time_AllocLocal_singleton_inv seen_view_seen_time. by iFrame.
Qed.
Lemma ROPtsTo_ROSeen l γ v :
l ro{γ} v l ro{γ} v.
Proof.
rewrite ROPtsTo_eq ROSeen_eq.
iDestruct 1 as (t m rsa rns ws Va (GH & Eqv' & LeVa))
"((sV & ARL & AWL & [%Vna NA]) & HC & As & AR)".
iExists t, Va. by iFrame.
Qed.
(* TODO: generalize with the next lemma *)
Lemma ROSeen_read_atomic l γ v v' o tid V Vb E :
Relaxed o histN E
......@@ -184,26 +265,4 @@ Proof.
eauto.
Qed.
Lemma ROPtsTo_from_na l v :
l v == γ, l ro{γ} v.
Proof.
rewrite own_loc_na_eq ROPtsTo_eq /ROPtsTo_def /own_loc_na_def.
iDestruct 1 as (t m) "(Own & %VAL & #sVm)".
iDestruct "Own" as (rsa rsn ws GH) "(AL & ARL & AWL & [%Va NAL] & HC & AW)".
set C := {[t := m]}.
iDestruct (view_at_intro_incl with "AWL sVm") as (Vna) "(sVna & %LeVna & AWL)".
iMod (own_alloc (to_agree ((t,v,Vna) : leibnizO _))) as (γ) "#A"; [done|].
iIntros "!>". iExists γ, t, m, rsa, rsn, ws, Vna. iSplit; [by iPureIntro|].
iFrame "ARL AWL HC AW A". iSplitR "NAL"; [|by eauto].
rewrite seen_time_AllocLocal_singleton_inv seen_view_seen_time. by iFrame.
Qed.
Lemma ROPtsTo_ROSeen l γ v :
l ro{γ} v l ro{γ} v.
Proof.
rewrite ROPtsTo_eq ROSeen_eq.
iDestruct 1 as (t m rsa rns ws Va (GH & Eqv' & LeVa))
"((sV & ARL & AWL & [%Vna NA]) & HC & As & AR)".
iExists t, Va. by iFrame.
Qed.
End ops_rules.
Supports Markdown
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