prove write progress lemma

theories/lang/stbor/stbor_ghost.v

@@ -736,6 +736,13 @@ Section defs.
   Qed.
 
   (* Allocation/initialization *)
+  Lemma stbor_alloc_1 stbor1 l :
+    ∃ stbor2, stbor_step stbor1 (StborAllocEv l 1 (Tagged (stbor_pnext stbor1))) stbor2.
+  Proof.
+    exists (MkStborState (<[l := [ItUnique (Tagged (stbor_pnext stbor1))]]> (stbor_stacks stbor1)) (S (stbor_pnext stbor1))).
+    rewrite /stbor_step. apply StborStepAlloc.
+  Qed.
+
   Lemma stbor_alloc l tgnew stbor1 stbor2 :
     stbor_step stbor1 (StborAllocEv l 1 tgnew) stbor2 →
     stbor1.(stbor_stacks) !! l = None →
@@ -760,6 +767,92 @@ Section defs.
   Qed.
 
   (* Writing *)
+  Lemma stbor_parse_tail_submseteq stk :
+    stbor_parse_tail stk ⊆+ stk.
+  Proof.
+    destruct stk as [|[| |] stk]; try done.
+    by apply submseteq_cons.
+  Qed.
+
+  Lemma stbor_rel_grants_write tg gstk stkold :
+    ghost_grants_write gstk tg →
+    stbor_rel_stack stkold gstk -∗
+    ⌜∃ it, it ∈ stkold ∧ item_grants_write it tg⌝.
+  Proof.
+    iIntros (Hgrants) "Hrel".
+    inversion Hgrants.
+    - iDestruct "Hrel" as "[Hrel _]". iDestruct "Hrel" as %Hrel.
+      iPureIntro. exists (ItUnique tg); split; last done.
+      destruct Hrel as (gtail & Hsub & Hconv).
+      apply sublist_submseteq in Hsub.
+      assert (GUnique tg ∈ gstk_tail gstk) as Helem1.
+      { subst. apply elem_of_list_here. }
+      assert (GUnique tg ∈ gtail) as Helem2.
+      { subst. by eapply elem_of_submseteq. }
+      apply (elem_of_list_fmap_1 stbor_convert_item) in Helem2.
+      rewrite /stbor_convert_tail in Hconv. rewrite Hconv in Helem2.
+      eapply elem_of_submseteq.
+      { apply Helem2. }
+      { apply stbor_parse_tail_submseteq. }
+    - iDestruct "Hrel" as "[Hrel _]". iDestruct "Hrel" as %Hrel.
+      iPureIntro. exists ItSharedRW; split; last done.
+      destruct Hrel as (gtail & Hsub & Hconv).
+      apply sublist_submseteq in Hsub.
+      assert (GSharedRW ∈ gstk_tail gstk) as Helem1.
+      { subst. apply elem_of_list_here. }
+      assert (GSharedRW ∈ gtail) as Helem2.
+      { subst. by eapply elem_of_submseteq. }
+      apply (elem_of_list_fmap_1 stbor_convert_item) in Helem2.
+      rewrite /stbor_convert_tail in Hconv. rewrite Hconv in Helem2.
+      eapply elem_of_submseteq.
+      { apply Helem2. }
+      { apply stbor_parse_tail_submseteq. }
+  Qed.
+
+  Lemma write_single_Some_elem_grants itg stkold tg :
+    itg ∈ stkold →
+    item_grants_write itg tg →
+    ∃ stknew, write_single tg stkold = Some stknew.
+  Proof.
+    intros Helem Hgrants.
+    destruct (write_single tg stkold) as [stknew|] eqn:Hwrite; first (by exists stknew).
+    exfalso.
+    induction stkold as [|it stkold IH]; first inversion Helem.
+    apply elem_of_cons in Helem as [Helem|Helem].
+    - rewrite /write_single in Hwrite.
+      rewrite decide_True in Hwrite. inversion Hwrite.
+      rewrite -Helem. apply Hgrants.
+    - apply IH; first done.
+      rewrite /write_single in Hwrite; case_decide; first inversion Hwrite.
+      apply Hwrite.
+  Qed.
+
+  Lemma stbor_write_single_1 gstk tg stkold :
+    ghost_grants_write gstk tg →
+    stbor_rel_stack stkold gstk -∗
+    ⌜∃ stknew, write_single tg stkold = Some stknew⌝.
+  Proof.
+    iIntros (Hgrants) "Hrel".
+    iDestruct (stbor_rel_grants_write with "Hrel") as %(itg & Helem & Hgrantsit); first done.
+    iPureIntro. by eapply write_single_Some_elem_grants.
+  Qed.
+
+  Lemma stbor_write_1 gstk stbor1 q l tg :
+    ghost_grants_write gstk tg →
+    stbor_ctx stbor1 -∗
+    stbor_active l q gstk -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborWriteEv l tg 1) stbor2⌝.
+  Proof.
+    iIntros (Hgrants) "Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_write_single_1 with "Hrel") as %[stknew Hsingle]; first done.
+    iPureIntro. exists (MkStborState (<[l:=stknew]> (stbor_stacks stbor1)) (stbor_pnext stbor1)).
+    apply StborStepWrite.
+    by rewrite /do_write /range_update Hlookup1 /= Hsingle /=.
+  Qed.
+
   Lemma stbor_write l tg stbor1 stbor2 gstk q :
     stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
     ghost_grants_write gstk tg →
@@ -791,6 +884,22 @@ Section defs.
   Qed.
 
   (* Deallocation *)
+  Lemma stbor_dealloc_1 l gstk stbor1 tg :
+    ghost_grants_write gstk tg →
+    stbor_ctx stbor1 -∗
+    stbor_active l 1 gstk -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborDeallocEv l tg 1) stbor2⌝.
+  Proof.
+    iIntros (Hgrants) "Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_write_single_1 with "Hrel") as %[stknew Hsingle]; first done.
+    iPureIntro. exists (MkStborState (delete l (stbor_stacks stbor1)) (stbor_pnext stbor1)).
+    apply StborStepDealloc.
+    by rewrite /do_dealloc /range_update Hlookup1 /= Hsingle /=.
+  Qed.
+
   Lemma stbor_dealloc l tg gstk stbor1 stbor2 :
     stbor_step stbor1 (StborDeallocEv l tg 1) stbor2 →
     ghost_grants_write gstk tg →
@@ -888,6 +997,27 @@ Section defs.
   Qed.
 
   (* Reading *)
+  Lemma stbor_read_single_1 gstk tg stkold :
+    ghost_grants_read gstk tg -∗
+    stbor_rel_stack stkold gstk -∗
+    ⌜∃ stknew, read_single tg stkold = Some stknew⌝.
+  Proof. Admitted.
+
+  Lemma stbor_read_1 l gstk q stbor1 tg :
+    ghost_grants_read gstk tg -∗
+    stbor_ctx stbor1 -∗
+    stbor_active l q gstk -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborReadEv l tg 1) stbor2⌝.
+  Proof.
+    iIntros "#Hgrants Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_read_single_1 with "Hgrants Hrel") as %[stknew Hsingle].
+    iPureIntro. exists (MkStborState (<[l:=stknew]> (stbor_stacks stbor1)) (stbor_pnext stbor1)).
+    apply StborStepRead.
+    by rewrite /do_read /range_update Hlookup1 /= Hsingle /=.
+  Qed.
 
   Lemma stbor_read l tg stbor1 stbor2 gstk q :
     stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
@@ -918,6 +1048,29 @@ Section defs.
   Qed.
 
   (* Retagging (SharedRO) *)
+  Lemma stbor_retag_sharedro_single_add_1 tgnew gstk tgold stkold :
+    ghost_grants_read gstk tgold -∗
+    stbor_rel_stack stkold gstk -∗
+    ⌜∃ stknew, retag_sharedro_single tgold {[ tgnew ]} stkold = Some stknew⌝.
+  Proof. Admitted.
+
+  Lemma stbor_retag_sharedro_add_1 l tgold stbor1 q γg gstk :
+    gstk.(gstk_sharedro) = Some γg →
+    ghost_grants_read gstk tgold -∗
+    stbor_ctx stbor1 -∗
+    stbor_active l q gstk -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborRetagEv l tgold [OutsideUnsafeCell] (PkRef Immutable) (RkDefault) (Tagged (stbor_pnext stbor1))) stbor2⌝.
+  Proof.
+    iIntros (Hgroup) "#Hgrants Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_retag_sharedro_single_add_1 (Tagged (stbor_pnext stbor1)) with "Hgrants Hrel") as %[stknew Hsingle].
+    iPureIntro. exists (MkStborState (<[l:=stknew]> (stbor_stacks stbor1)) (S (stbor_pnext stbor1))).
+    apply StborStepRetag.
+    by rewrite /do_retag /range_update /range_interior_update Hlookup1 /= /retag_single /= Hsingle.
+  Qed.
+
   Lemma stbor_retag_sharedro_add l tgold tgnew stbor1 stbor2 q γg gstk :
     stbor_step stbor1 (StborRetagEv l tgold [OutsideUnsafeCell] (PkRef Immutable) (RkDefault) tgnew) stbor2 →
     gstk.(gstk_sharedro) = Some γg →
@@ -950,6 +1103,28 @@ Section defs.
   Qed.
 
   (* Retagging (Unique) *)
+  Lemma stbor_retag_unique_single_1 tgnew tgold stkold gstk :
+    ghost_grants_write gstk tgold →
+    stbor_rel_stack stkold gstk -∗
+    ⌜∃ stknew, retag_unique_single tgold tgnew stkold = Some stknew⌝.
+  Proof. Admitted.
+
+  Lemma stbor_retag_unique_1 l tgold int_mut stbor1 gtail :
+    ghost_grants_write (MkGhostStack None gtail) tgold →
+    stbor_ctx stbor1 -∗
+    stbor_active l 1 (MkGhostStack None gtail) -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRef Mutable) (RkDefault) (Tagged (stbor_pnext stbor1))) stbor2⌝.
+  Proof.
+    iIntros (Hgrants) "Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_retag_unique_single_1 (Tagged (stbor_pnext stbor1)) with "Hrel") as %[stknew Hsingle]; first done.
+    iPureIntro. exists (MkStborState (<[l:=stknew]> (stbor_stacks stbor1)) (S (stbor_pnext stbor1))).
+    apply StborStepRetag.
+    by rewrite /do_retag /range_update /range_interior_update Hlookup1 /= /retag_single /= Hsingle /=.
+  Qed.
+
   Lemma stbor_retag_unique l tgold tgnew int_mut stbor1 stbor2 gtail :
     stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRef Mutable) (RkDefault) tgnew) stbor2 →
     ghost_grants_write (MkGhostStack None gtail) tgold →
@@ -978,6 +1153,27 @@ Section defs.
   Qed.
 
   (* Retagging (SharedRW) *)
+  Lemma stbor_retag_sharedrw_single_1 stkold gtail tgold gshared :
+    ghost_grants_retag_sharedrw_tail gtail tgold →
+    stbor_rel_stack stkold (MkGhostStack gshared gtail) -∗
+    ⌜∃ stknew, retag_sharedrw_single tgold stkold = Some stknew⌝.
+  Proof. Admitted.
+
+  Lemma stbor_retag_sharedrw_1 stbor1 gtail tgold gshared l int_mut :
+    ghost_grants_retag_sharedrw_tail gtail tgold →
+    stbor_ctx stbor1 -∗
+    stbor_active l 1 (MkGhostStack gshared gtail) -∗
+    ⌜∃ stbor2, stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRaw Mutable) RkRaw Untagged) stbor2⌝.
+  Proof.
+    iIntros (Hgrants) "Hctx Hactive◯".
+    iDestruct "Hctx" as (gstks) "[Hrel Hactive●]".
+    iDestruct (stbor_active_lookup with "Hactive● Hactive◯") as %Hlookup2.
+    iDestruct (big_sepM2_lookup_2 with "Hrel") as (stkold Hlookup1) "Hrel"; first done.
+    iDestruct (stbor_retag_sharedrw_single_1 with "Hrel") as %[stknew Hsingle]; first done.
+    iPureIntro. exists (MkStborState (<[l:=stknew]> (stbor_stacks stbor1)) (S (stbor_pnext stbor1))).
+    apply StborStepRetag.
+    by rewrite /do_retag /range_update /range_interior_update Hlookup1 /= /retag_single /= Hsingle /=.
+  Qed.
 
   Lemma stbor_retag_sharedrw l tgold tgnew int_mut stbor1 stbor2 gshared gtail :
     stbor_step stbor1 (StborRetagEv l tgold [int_mut] (PkRaw Mutable) RkRaw tgnew) stbor2 →