Skip to content
Snippets Groups Projects
Commit a7a6079a authored by Daniël Louwrink's avatar Daniël Louwrink
Browse files

remove repetition from stbor_ghost

parent 58cb00c9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/lang/stbor/stbor_ghost.v
+ 302
− 205
View file @ a7a6079a
......@@ -676,6 +676,90 @@ Section defs.
by rewrite /do_write /range_update Hlookup1 /= Hstep /=.
Qed.
(* TODO: Move this? *)
Definition stack_set (l : loc) (stk : stack) (stbor : stbor_state) : stbor_state :=
{| stbor_stacks := <[l := stk]> stbor.(stbor_stacks); stbor_pnext := stbor.(stbor_pnext) |}.
Definition stack_lookup (l : loc) (stbor : stbor_state) : option stack :=
stbor.(stbor_stacks) !! l.
Lemma stbor_ctx_lookup stbor l q gstk :
stbor_ctx stbor -∗
stbor_active l q gstk -∗
⌜∃ stk, stack_lookup l stbor = Some stk⌝.
Proof.
iIntros "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro.
apply (elem_of_dom_2 (D := gset loc)) in Hlookup2.
rewrite -Hdom in Hlookup2.
apply elem_of_dom in Hlookup2 as (stk & Hlookup2).
exists stk. apply Hlookup2.
Qed.
Lemma stbor_ctx_insert_acc_1 l stbor stkold q gstk :
stack_lookup l stbor = Some stkold →
stbor_ctx stbor -∗
stbor_active l q gstk -∗
stbor_rel_stack stkold gstk ∗
stbor_active l q gstk ∗
(∀ stknew, stbor_rel_stack stknew gstk -∗ stbor_ctx (stack_set l stknew stbor)).
Proof.
iIntros (Hlookup1) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
rewrite /stbor_rel_stacks big_sepM2_insert_acc; [|done..].
iDestruct "Hrel" as "[Hrel1 Hrel]".
iFrame "Hrel1 Hactive◯".
iIntros (stknew) "Hrel1". iSpecialize ("Hrel" with "Hrel1").
rewrite /stack_lookup in Hlookup2. apply insert_id in Hlookup2 as ->.
iExists _. iFrame "Hactive● Hrel".
Qed.
Lemma stbor_ctx_insert_acc_2 gstk2 l stbor stk1 gstk1 :
stack_lookup l stbor = Some stk1 →
stbor_ctx stbor -∗
stbor_active l 1 gstk1 ==∗
stbor_rel_stack stk1 gstk1 ∗
stbor_active l 1 gstk2 ∗
(∀ stk2, stbor_rel_stack stk2 gstk2 -∗ stbor_ctx (stack_set l stk2 stbor)).
Proof.
iIntros (Hlookup1) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iMod (stbor_active_set l gstk2 with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro.
rewrite /stbor_rel_stacks big_sepM2_insert_acc; [|done..].
iDestruct "Hrel" as "[Hrel1 Hrel]".
iFrame "Hrel1 Hactive◯".
iIntros (stk2) "Hrel1". iSpecialize ("Hrel" with "Hrel1").
iExists _. iFrame "Hactive● Hrel".
Qed.
(* TODO: Move inversion lemmas *)
Lemma write_inv l tg stbor1 stbor2 :
stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
write_single tg stkold = Some stknew ∧
stbor2 = stack_set l stknew stbor1.
Proof.
intros Hstep.
inversion Hstep as [|? ? ? ? Hwrite| | |].
rewrite /do_write /range_update in Hwrite.
apply bind_Some in Hwrite as (stkold & Hlookup & Hwrite).
apply bind_Some in Hwrite as (stknew & Hwrite1 & Hwrite).
exists stkold, stknew. repeat split; [done..|].
inversion Hwrite.
destruct stbor2 as [stks2 pnext2].
destruct stbor1 as [stks1 pnext1].
rewrite /stack_set. f_equal; subst; done.
Qed.
Lemma stbor_write_ctx l tg stbor1 stbor2 gstk q :
stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
ghost_grants_write gstk tg -∗
......@@ -686,25 +770,14 @@ Section defs.
stbor_active l q gstk.
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor1 !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hrel1".
iDestruct (ghost_grants_write_log with "Hgrants Hrel1") as %Hgrantslog.
iFrame "Hactive◯". iExists gstks. iFrame "Hactive●".
inversion Hstep as [|? ? ? ? Hwrite| | |].
rewrite /do_write /range_update Hlookup1 /= in Hwrite.
destruct (write_single tg stkold) as [stknew|] eqn:Hwrite'; inversion Hwrite.
eapply write_single_preserve in Hgrantslog; try done.
iSpecialize ("Hrel" $! stknew gstk).
apply insert_id in Hlookup2. rewrite Hlookup2.
iApply "Hrel".
iExists stklog. iFrame "Hrel1". iPureIntro. apply Hgrantslog.
edestruct write_inv as (stkold & stknew & Hlookup1 & Hwrite1 & Hset); first done.
iDestruct (stbor_ctx_insert_acc_1 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_grants_write_log with "Hgrants Hgstk") as %Hgrantslog.
eapply write_single_preserve in Hgrantslog; [|done..].
iFrame "Hactive◯". rewrite Hset.
iApply "Hback".
iExists _. iFrame "Hgstk". done.
Qed.
Lemma stbor_write l tg stbor1 stbor2 gstk q E :
......@@ -744,6 +817,28 @@ Section defs.
by rewrite /do_dealloc /range_update Hlookup1 /= Hstep.
Qed.
Definition stack_delete (l : loc) (stbor : stbor_state) : stbor_state :=
{| stbor_stacks := delete l stbor.(stbor_stacks); stbor_pnext := stbor.(stbor_pnext) |}.
Lemma dealloc_inv l tg stbor1 stbor2 :
stbor_step stbor1 (StborDeallocEv l tg 1) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
write_single tg stkold = Some stknew ∧
stbor2 = stack_delete l stbor1.
Proof.
intros Hstep.
inversion Hstep as [| | |? ? ? ? Hdealloc|].
rewrite /do_dealloc /range_update in Hdealloc.
apply bind_Some in Hdealloc as (stkold & Hlookup & Hdealloc).
apply bind_Some in Hdealloc as (stknew & Hwrite & Hdelete).
exists stkold, stknew. repeat split; [done..|].
inversion Hdelete.
destruct stbor1 as [stks1 pnext1].
destruct stbor2 as [stks2 pnext2].
rewrite /stack_delete. f_equal; subst; done.
Qed.
Lemma stbor_dealloc_ctx l tg gstk stbor1 stbor2 :
stbor_step stbor1 (StborDeallocEv l tg 1) stbor2 →
ghost_grants_write gstk tg -∗
......@@ -753,23 +848,15 @@ Section defs.
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iMod (stbor_active_dealloc with "Hactive● Hactive◯") as "Hactive●".
iModIntro.
inversion Hstep as [| | |? ? ? ? Hdealloc|].
rewrite /do_dealloc /range_update in Hdealloc.
destruct (stbor_stacks stbor1 !! l) as [stkold|] eqn:Hlookup; last inversion Hdealloc.
simpl in Hdealloc.
destruct (write_single tg stkold) as [stknew|] eqn:Hwrite; last inversion Hdealloc.
iExists _. iFrame "Hactive●".
inversion Hdealloc.
iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
assert (is_Some (gstks !! l)) as Hlookup2.
{ apply (elem_of_dom (D := gset loc)).
rewrite -Hdom.
rewrite elem_of_dom. by eapply mk_is_Some. }
destruct Hlookup2 as [gstk' Hlookup2].
iDestruct (big_sepM2_delete with "Hrel") as "[_ $]"; first done.
apply Hlookup2.
edestruct dealloc_inv as (stkold & stknew & Hlookup1 & Hwrite & Hdelete); first done.
destruct stbor1 as [stks1 pnext1].
destruct stbor2 as [stks2 pnext2].
inversion Hdelete.
iDestruct (big_sepM2_delete with "Hrel") as "[_ $]"; eassumption.
Qed.
Lemma stbor_dealloc l tg gstk stbor1 stbor2 E :
......@@ -807,6 +894,25 @@ Section defs.
by rewrite /do_read /range_update Hlookup1 /= Hstep /=.
Qed.
Lemma read_inv l tg stbor1 stbor2 :
stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
read_single tg stkold = Some stknew ∧
stbor2 = stack_set l stknew stbor1.
Proof.
intros Hstep.
inversion Hstep as [| |? ? ? ? Hread| |].
rewrite /do_read /range_update in Hread.
apply bind_Some in Hread as (stkold & Hlookup & Hread).
apply bind_Some in Hread as (stknew & Hread & Hset).
exists stkold, stknew. repeat split; [done..|].
destruct stbor1 as [stks1 pnext1].
destruct stbor2 as [stks2 pnext2].
inversion Hset.
rewrite /stack_set. f_equal; subst; done.
Qed.
Lemma stbor_read_ctx l tg stbor1 stbor2 gstk q :
stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
ghost_grants_read gstk tg -∗
......@@ -817,25 +923,14 @@ Section defs.
stbor_active l q gstk.
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor1 !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hrel1".
iDestruct (ghost_grants_read_log with "Hgrants Hrel1") as %Hgrantslog.
iFrame "Hactive◯". iExists gstks. iFrame "Hactive●".
inversion Hstep as [| |? ? ? ? Hread| |].
rewrite /do_read /range_update Hlookup1 /= in Hread.
destruct (read_single tg stkold) as [stknew|] eqn:Hread'; inversion Hread.
eapply read_single_preserve in Hgrantslog; try done.
iSpecialize ("Hrel" $! stknew gstk).
apply insert_id in Hlookup2. rewrite Hlookup2.
iApply "Hrel".
iExists stklog. iFrame "Hrel1". iPureIntro. apply Hgrantslog.
edestruct read_inv as (stkold & stknew & Hlookup & Hread & Hset); first done.
iDestruct (stbor_ctx_insert_acc_1 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_grants_read_log with "Hgrants Hgstk") as %Hgrantslog.
eapply read_single_preserve in Hgrantslog; [|done..].
iFrame "Hactive◯". rewrite Hset.
iApply "Hback".
iExists _. iFrame "Hgstk". done.
Qed.
Lemma stbor_read l tg stbor1 stbor2 gstk q E :
......@@ -875,6 +970,31 @@ Section defs.
by rewrite /do_retag /range_interior_update Hlookup1 /= /retag_single /= /retag_unique_single /= Hstep.
Qed.
Definition stack_tick (stbor : stbor_state) : stbor_state :=
{| stbor_stacks := stbor.(stbor_stacks); stbor_pnext := S (stbor.(stbor_pnext)) |}.
Lemma retag_unique_inv l tgold tgnew stbor1 stbor2 int_mut :
stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRef Mutable) RkDefault tgnew) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
retag_unique_single tgold tgnew stkold = Some stknew ∧
stbor2 = stack_tick (stack_set l stknew stbor1).
Proof.
intros Hstep.
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /range_interior_update in Hretag.
apply bind_Some in Hretag as (stksnew' & Hretag & Htag).
apply bind_Some in Hretag as (stkold & Hlookup & Hretag).
apply bind_Some in Hretag as (stknew & Hretag & Hset).
exists stkold, stknew.
rewrite /retag_single /= in Hretag.
inversion Htag.
repeat split; [done..|].
inversion Hset.
destruct stbor1 as [stks1 pnext1]. destruct stbor2 as [stks2 pnext2].
rewrite /stack_set /stack_tick. f_equal; subst; done.
Qed.
Lemma stbor_retag_unique_ctx l tgold tgnew int_mut stbor1 stbor2 gstk :
stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRef Mutable) (RkDefault) tgnew) stbor2 →
ghost_grants_write gstk tgold -∗
......@@ -885,27 +1005,16 @@ Section defs.
stbor_active l 1 (GUnique tgnew :: gstk).
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor1 !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hrel1".
iDestruct (ghost_grants_write_log with "Hgrants Hrel1") as %Hgrantslog.
iMod (stbor_active_set l (GUnique tgnew :: gstk) with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro. iFrame "Hactive◯". iExists _. iFrame "Hactive●".
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /= Hlookup1 /= /retag_single /= in Hretag.
destruct (retag_unique_single tgold (Tagged (stbor_pnext stbor1)) stkold) as [stknew|] eqn:Hretagu; inversion Hretag.
eapply retag_unique_single_preserve in Hgrantslog; try done.
iApply ("Hrel" $! stknew (GUnique (Tagged (stbor_pnext stbor1)) :: gstk)).
rewrite /stbor_rel_stack.
iExists _; iSplit; first (iPureIntro; eassumption).
rewrite /stbor_ghost_stack.
iApply big_sepL2_cons; iSplit; done.
edestruct retag_unique_inv as (stkold & stknew & Hlookup & Hretag & Hset); first done.
iMod (stbor_ctx_insert_acc_2 (GUnique tgnew :: gstk) with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iModIntro.
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_grants_write_log with "Hgrants Hgstk") as %Hgrantslog.
eapply retag_unique_single_preserve in Hgrantslog; [|done..].
iFrame "Hactive◯". rewrite Hset.
iApply "Hback".
iExists _. iSplit; first done.
by iApply (stbor_ghost_stack_cons with "[] Hgstk").
Qed.
Lemma stbor_retag_unique l tgold tgnew int_mut stbor1 stbor2 gstk E :
......@@ -945,6 +1054,26 @@ Section defs.
by rewrite /do_retag /range_interior_update Hlookup1 /= /retag_single /= /retag_sharedro_single /= Hstep.
Qed.
Lemma retag_sharedro_inv l tgold tgnew stbor1 stbor2 :
stbor_step stbor1 (StborRetagEv l tgold [OutsideUnsafeCell] (PkRef Immutable) RkDefault tgnew) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
retag_sharedro_single tgold {[ tgnew ]} stkold = Some stknew ∧
stbor2 = stack_tick (stack_set l stknew stbor1).
Proof.
intros Hstep.
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /range_interior_update in Hretag.
apply bind_Some in Hretag as (stksnew' & Hretag & Htag).
apply bind_Some in Hretag as (stkold & Hlookup & Hretag).
apply bind_Some in Hretag as (stknew & Hretag & Hset).
exists stkold, stknew. inversion Htag.
repeat split; [done..|].
destruct stbor1 as [stks1 pnext1]. destruct stbor2 as [stks2 pnext2].
rewrite /stack_set /stack_tick. inversion Hset.
f_equal; subst; done.
Qed.
Lemma stbor_retag_sharedro_add_ctx l tgold tgnew stbor1 stbor2 q γg gstk :
stbor_step stbor1 (StborRetagEv l tgold [OutsideUnsafeCell] (PkRef Immutable) (RkDefault) tgnew) stbor2 →
ghost_grants_read (GSharedRO γg :: gstk) tgold -∗
......@@ -956,35 +1085,19 @@ Section defs.
stbor_shared γg tgnew.
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor1 !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists (GSharedRO γg :: gstk). }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hrel1".
iDestruct (ghost_grants_read_log with "Hgrants Hrel1") as %Hgrantslog.
iFrame "Hactive◯".
iDestruct (stbor_ghost_stack_cons_inv_r with "Hrel1") as (it stklog' ->) "[Hgit Hgstk]".
iDestruct "Hgit" as (tgs Heq) "Hgit".
iMod (stbor_shared_extend tgnew with "Hgit") as "[Hgit Hshared]".
iFrame "Hshared". iModIntro. iExists _. iFrame "Hactive●".
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /= Hlookup1 /= /retag_single /= in Hretag.
destruct (retag_sharedro_single tgold {[Tagged (stbor_pnext stbor1)]} stkold) as [stknew|] eqn:Hretagu; inversion Hretag.
rewrite Heq in Hgrantslog Hlog.
edestruct retag_sharedro_inv as (stkold & stknew & Hlookup & Hretag & Hset); first done.
iDestruct (stbor_ctx_insert_acc_1 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_grants_read_log with "Hgrants Hgstk") as %Hgrantslog.
iDestruct (stbor_ghost_stack_cons_inv_r with "Hgstk") as (it stklog' ->) "[Hgit Hgstk]".
iDestruct "Hgit" as (tgs ->) "Hgit".
eapply retag_sharedro_single_extend_preserve in Hgrantslog; [|done..].
set (tgsnew := {[ Tagged (stbor_pnext stbor1) ]} : gset tag).
iSpecialize ("Hrel" $! stknew (GSharedRO γg :: gstk)).
apply insert_id in Hlookup2. rewrite Hlookup2.
iApply "Hrel".
rewrite /stbor_rel_stack.
iExists (ItSharedRO (tgsnew ∪ tgs) :: stklog').
iSplit; first done.
iApply big_sepL2_cons. iFrame "Hgstk".
iExists (tgsnew ∪ tgs). by iFrame "Hgit".
iFrame "Hactive◯". rewrite Hset.
iMod (stbor_shared_extend tgnew with "Hgit") as "[Hgit $]".
iModIntro. iApply "Hback".
iExists _. iSplit; first done.
iApply (stbor_ghost_stack_cons with "[Hgit] Hgstk").
iExists _. iFrame "Hgit". done.
Qed.
Lemma stbor_retag_sharedro_add l tgold tgnew stbor1 stbor2 q γg gstk E :
......@@ -1035,6 +1148,17 @@ Section defs.
intros (? & ? & Heq). inversion Heq.
Qed.
Lemma stack_set_id l stbor stk :
stack_lookup l stbor = Some stk →
stack_set l stk stbor = stbor.
Proof.
intros Hlookup.
destruct stbor as [stks pnext].
rewrite /stack_lookup in Hlookup.
apply insert_id in Hlookup.
rewrite /stack_set. f_equal; subst; done.
Qed.
Lemma stbor_push_sharedro_ctx l gstk stbor :
ghost_stack_no_sharedro gstk →
stbor_ctx stbor -∗
......@@ -1045,30 +1169,19 @@ Section defs.
stbor_active l 1 (GSharedRO γg :: gstk).
Proof.
iIntros (Hnoshared) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_ctx_lookup with "Hctx Hactive◯") as %[stk Hlookup].
iMod (stbor_shared_alloc ∅) as (γg) "Hshared●".
iExists γg.
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk. }
iMod (stbor_active_set l (GSharedRO γg :: gstk) with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro. iFrame "Hactive◯". iExists _. iFrame "Hactive●".
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hrel1".
iDestruct (ghost_stack_no_sharedro_rel with "Hrel1") as %Hnoshared'; first assumption.
apply retag_sharedro_single_initial_preserve in Hlog; last done.
(* iDestruct (ghost_stack_no_sharedro_push_sharedro with "Hrel1") as %Hpush; first done. *)
(* rewrite Hpush in Hlog. *)
iSpecialize ("Hrel" $! stkold (GSharedRO γg :: gstk)).
apply insert_id in Hlookup1. rewrite Hlookup1.
iApply "Hrel".
rewrite /stbor_rel_stack.
iExists _; iSplit; first done.
iApply big_sepL2_cons; iSplitR "Hrel1"; last done.
iExists ∅. by iFrame "Hshared●".
iMod (stbor_ctx_insert_acc_2 (GSharedRO γg :: gstk) with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iModIntro. iExists γg. iFrame "Hactive◯".
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_stack_no_sharedro_rel with "Hgstk") as %Hnoshared'; first assumption.
apply retag_sharedro_single_initial_preserve in Hrel; last done.
iSpecialize ("Hback" $! stk).
rewrite stack_set_id; last done.
iApply "Hback".
iExists _. iSplit; first done.
iApply (stbor_ghost_stack_cons with "[Hshared●] Hgstk").
iExists _. by iFrame "Hshared●".
Qed.
Lemma stbor_push_sharedro l gstk E :
......@@ -1119,23 +1232,17 @@ Section defs.
stbor_active l 1 gstk2.
Proof.
iIntros (Hsub) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk1. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hrellog) "Hgstk".
iDestruct (stack_ghost_sublist with "Hgstk") as (stklog' Hsub') "Hgstk'"; first done.
iMod (stbor_active_set l gstk2 with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro. iFrame "Hactive◯". iExists _. iFrame "Hactive●".
iSpecialize ("Hrel" $! stkold gstk2).
apply insert_id in Hlookup1. rewrite Hlookup1.
iApply "Hrel".
iExists _; iSplit; last iFrame "Hgstk'".
iPureIntro. by eapply log_pop_prefix_preserve.
iDestruct (stbor_ctx_lookup with "Hctx Hactive◯") as %[stk Hlookup].
iMod (stbor_ctx_insert_acc_2 gstk2 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iModIntro. iFrame "Hactive◯".
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (stack_ghost_sublist with "Hgstk") as (stklog' Hsub') "Hgstk"; first done.
eapply log_pop_prefix_preserve in Hrel; last done.
iSpecialize ("Hback" $! stk).
rewrite stack_set_id; last done.
iApply "Hback".
iExists _. iSplit; first done.
iFrame "Hgstk".
Qed.
Lemma stbor_remove gstk2 l gstk1 E :
......@@ -1162,23 +1269,17 @@ Section defs.
stbor_active l 1 gstk2.
Proof.
iIntros (Hsub) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by exists gstk1. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hrellog) "Hgstk".
iDestruct (ghost_disable_log with "Hgstk") as (stklog' Hsub') "Hgstk'"; first done.
iMod (stbor_active_set l gstk2 with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro. iFrame "Hactive◯". iExists _. iFrame "Hactive●".
iSpecialize ("Hrel" $! stkold gstk2).
apply insert_id in Hlookup1. rewrite Hlookup1.
iApply "Hrel".
iExists _; iSplit; last iFrame "Hgstk'".
iPureIntro. by eapply log_disable_preserve.
iDestruct (stbor_ctx_lookup with "Hctx Hactive◯") as %[stk Hlookup].
iMod (stbor_ctx_insert_acc_2 gstk2 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iModIntro. iFrame "Hactive◯".
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_disable_log with "Hgstk") as (stklog' Hsub') "Hgstk"; first done.
eapply log_disable_preserve in Hrel; last done.
iSpecialize ("Hback" $! stk).
rewrite stack_set_id; last done.
iApply "Hback".
iExists _. iSplit; first done.
iFrame "Hgstk".
Qed.
Lemma stbor_disable gstk2 gstk1 l E :
......@@ -1206,27 +1307,20 @@ Section defs.
stbor_ctx stbor.
Proof.
iIntros (Hretag) "Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by eexists. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hrellog) "Hgstk".
iDestruct (ghost_retag_sharedrw_initial_log with "Hgstk") as (stklog1 stklog2 Hretaglog) "[Hgstk1 Hgstk2]"; first done.
iDestruct (stbor_ctx_lookup with "Hctx Hactive◯") as %[stk Hlookup].
iMod (stbor_shared_alloc ∅) as (γg) "Hshared●".
iMod (stbor_active_set l (gstk1 ++ GSharedRW γg :: gstk2) with "Hactive● Hactive◯") as "[Hactive● Hactive◯]".
iModIntro. iExists γg. iFrame "Hactive◯". iExists _. iFrame "Hactive●".
iSpecialize ("Hrel" $! stkold (gstk1 ++ GSharedRW γg :: gstk2)).
apply insert_id in Hlookup1. rewrite Hlookup1.
iApply "Hrel".
iExists (stklog1 ++ ItSharedRW ∅ :: stklog2). iSplit.
- iPureIntro. by eapply retag_sharedrw_single_initial.
- iApply (stbor_ghost_stack_app with "[Hgstk1 //] [Hshared● Hgstk2]").
iApply (stbor_ghost_stack_cons with "[Hshared●] [Hgstk2 //]").
iExists ∅. by iFrame "Hshared●".
iMod (stbor_ctx_insert_acc_2 (gstk1 ++ GSharedRW γg :: gstk2) with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iModIntro. iExists γg. iFrame "Hactive◯".
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_retag_sharedrw_initial_log with "Hgstk") as (stklog1 stklog2 Hretaglog) "[Hgstk1 Hgstk2]"; first done.
eapply retag_sharedrw_single_initial in Hrel; last done.
iSpecialize ("Hback" $! stk).
rewrite stack_set_id; last done.
iApply "Hback".
iExists _. iSplit; first done.
iApply (stbor_ghost_stack_app with "Hgstk1 [Hshared● Hgstk2]").
iApply (stbor_ghost_stack_cons with "[Hshared●] Hgstk2").
iExists ∅. by iFrame "Hshared●".
Qed.
Lemma retag_sharedrw_initial_preserve l gstk gstk1 gstk2 E :
......@@ -1244,10 +1338,6 @@ Section defs.
Qed.
(** * Retag (SharedRW) extend *)
(* TODO: Maybe state retag_sharedrw_extend using append instead of an inductive. *)
Lemma retag_sharedrw_extend_skip_app tgold tgsnew stklog1 stklog2 stklog2' :
retag_sharedrw_extend tgold tgsnew stklog2 stklog2' →
retag_sharedrw_extend tgold tgsnew (stklog1 ++ stklog2) (stklog1 ++ stklog2').
......@@ -1328,6 +1418,28 @@ Section defs.
by rewrite /do_retag /range_interior_update Hlookup1 /= /retag_single /= Hstep.
Qed.
Lemma retag_sharedrw_inv l tgold tgnew stbor1 stbor2 :
stbor_step stbor1 (StborRetagEv l tgold [InsideUnsafeCell] (PkRef Immutable) RkDefault tgnew) stbor2 →
∃ stkold stknew,
stack_lookup l stbor1 = Some stkold ∧
retag_sharedrw_single tgold {[ tgnew ]} stkold = Some stknew ∧
stbor2 = stack_tick (stack_set l stknew stbor1).
Proof.
intros Hstep.
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /range_interior_update in Hretag.
apply bind_Some in Hretag as (stksnew' & Hretag & Htag).
apply bind_Some in Hretag as (stkold & Hlookup & Hretag).
apply bind_Some in Hretag as (stknew & Hretag & Hset).
exists stkold, stknew.
rewrite /retag_single /= in Hretag.
inversion Htag.
repeat split; [done..|].
destruct stbor1 as [stks1 pnext1]. destruct stbor2 as [stks2 pnext2].
rewrite /stack_tick /stack_set.
inversion Hset. subst. by f_equal.
Qed.
Lemma stbor_retag_sharedrw_add_ctx l tgold tgnew stbor1 stbor2 q γg gstk :
stbor_step stbor1 (StborRetagEv l tgold [InsideUnsafeCell] (PkRef Immutable) (RkDefault) tgnew) stbor2 →
ghost_grants_retag_sharedrw gstk γg tgold -∗
......@@ -1339,31 +1451,16 @@ Section defs.
stbor_shared γg tgnew.
Proof.
iIntros (Hstep) "#Hgrants Hctx Hactive◯".
iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
iAssert (⌜is_Some (stbor_stacks stbor1 !! l)⌝)%I as %(stkold & Hlookup1).
{ iDestruct (big_sepM2_dom with "Hrel") as %Hdom.
iPureIntro. rewrite -(elem_of_dom (D := gset loc)) Hdom.
rewrite elem_of_dom. by eexists. }
rewrite /stbor_rel_stacks big_sepM2_insert_acc; try done.
iDestruct "Hrel" as "[Hrel1 Hrel]".
iDestruct "Hrel1" as (stklog Hlog) "Hgstk".
edestruct retag_sharedrw_inv as (stkold & stknew & Hlookup & Hretag & Hset); first done.
iDestruct (stbor_ctx_insert_acc_1 with "Hctx Hactive◯") as "(Hrel & Hactive◯ & Hback)"; first done.
iDestruct "Hrel" as (stklog Hrel) "Hgstk".
iDestruct (ghost_grants_retag_sharedrw_log with "Hgrants Hgstk") as %Hgrantslog.
iMod (stbor_ghost_stack_insert_sharedrw with "Hgrants Hgstk") as (stklog2 Hretagrw) "[Hgstk $]".
iFrame "Hactive◯".
iModIntro. iExists _. iFrame "Hactive●".
inversion Hstep as [| | | |? ? ? ? ? ? ? Hretag].
rewrite /do_retag /range_update /= Hlookup1 /= /retag_single /= in Hretag.
destruct (retag_sharedrw_single tgold _ stkold) as [stknew|] eqn:Hretagu; inversion Hretag.
subst. eapply retag_sharedrw_single_extend in Hretagrw; [|done..].
set (tgsnew := {[ Tagged (stbor_pnext stbor1) ]} : gset tag).
iSpecialize ("Hrel" $! stknew gstk).
apply insert_id in Hlookup2. rewrite Hlookup2.
iApply "Hrel".
rewrite /stbor_rel_stack.
iExists stklog2.
iSplit; first done.
iFrame "Hgstk".
iModIntro. iFrame "Hactive◯".
rewrite Hset.
iApply "Hback".
iExists _. iFrame "Hgstk". iPureIntro.
by eapply retag_sharedrw_single_extend.
Qed.
Lemma stbor_retag_sharedrw_add l tgold tgnew stbor1 stbor2 q γg gstk E :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment