Commit 2491d164 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

made masks in view shifts general

parent 25207539
......@@ -111,7 +111,6 @@ Section to_gc_map.
Qed.
End to_gc_map.
Section gc.
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
......@@ -127,9 +126,9 @@ Section gc.
Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
Proof. rewrite /gc_inv_P. apply _. Qed.
Lemma make_gc l v: gc_inv - l v ={gcN}= gc_mapsto l v.
Lemma make_gc l v E: gcN E gc_inv - l v ={E}= gc_mapsto l v.
Proof.
iIntros "#Hinv Hl".
iIntros (HN) "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iDestruct "P" as (gcm) "[H● HsepM]".
destruct (gcm !! l) as [v' | ] eqn: Hlookup.
......@@ -181,12 +180,12 @@ Section gc.
by apply gc_map_singleton_included.
Qed.
Lemma gc_access l v:
gc_inv - gc_mapsto l v ={gcN, }= (l v ( w, l w ={, gcN}= gc_mapsto l w)).
Lemma gc_access l v E:
gcN E gc_inv - gc_mapsto l v ={E, E gcN}= (l v ( w, l w ={E gcN, E}= gc_mapsto l w)).
Proof.
iIntros "#Hinv Hgc_l".
iIntros (HN) "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
rewrite difference_diag_L. iModIntro.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//.
......@@ -203,11 +202,11 @@ Section gc.
iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
Qed.
Lemma is_gc_access l: gc_inv - is_gc_loc l ={gcN, }= v, l v (l v ={, gcN}= True).
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}= v, l v (l v ={E gcN, E}= True).
Proof.
iIntros "#Hinv Hgc_l".
iIntros (HN) "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
rewrite difference_diag_L. iModIntro.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
destruct Hsome as [v Hsome].
......
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