add ghost disabling

theories/lang/stbor/stbor_ghost.v

@@ -308,6 +308,13 @@ Section defs.
   Definition ghost_stack_no_sharedro (gstk : ghost_stack) : Prop :=
     ¬ ∃ γg gstk', gstk = GSharedRO γg :: gstk'.
 
+  Inductive ghost_disable_item : ghost_item → ghost_item → Prop :=
+  | ghost_disable_item_keep git : ghost_disable_item git git
+  | ghost_disable_item_disable tg : ghost_disable_item (GUnique tg) GDisabled.
+
+  Definition ghost_disable (gstk1 : ghost_stack) (gstk2 : ghost_stack) : Prop :=
+    Forall2 ghost_disable_item gstk1 gstk2.
+
   Global Instance ghost_grants_write_pers gstk tg : Persistent (ghost_grants_write gstk tg).
   Proof. destruct gstk as [|[| | |]]; apply _. Qed.
 
@@ -399,6 +406,35 @@ Section defs.
         apply Hgrantslog.
   Qed.
 
+  Lemma ghost_disable_log gstk1 gstk2 stklog1 :
+    ghost_disable gstk1 gstk2 →
+    stbor_ghost_stack stklog1 gstk1 -∗
+    ∃ stklog2, ⌜log_disable stklog1 stklog2⌝ ∗ stbor_ghost_stack stklog2 gstk2.
+  Proof.
+    iIntros (Hdis) "Hgstk".
+    iInduction Hdis as [|? ? ? ? Hdisit] "IH" forall (stklog1).
+    - rewrite /stbor_ghost_stack.
+      iDestruct (big_sepL2_length with "Hgstk") as %Hlen.
+      apply nil_length_inv in Hlen. rewrite Hlen.
+      iExists []. iSplit; first (iPureIntro; constructor).
+      by rewrite big_sepL2_nil.
+    - iDestruct (big_sepL2_cons_inv_r with "Hgstk") as (itlog stklog' ->) "[Hgit Hgstk]".
+      iDestruct ("IH" with "Hgstk") as (stklog2') "[Hdis2 Hgstk]".
+      iDestruct "Hdis2" as %Hdis2.
+      inversion Hdisit; subst.
+      + iExists _; iSplit.
+        * iPureIntro. constructor; first apply log_disable_item_keep.
+          apply Hdis2.
+        * rewrite /stbor_ghost_stack.
+          iApply big_sepL2_cons. iFrame "Hgit Hgstk".
+      + iDestruct "Hgit" as %->.
+        iExists _; iSplit.
+        * iPureIntro. constructor; first apply log_disable_item_disable.
+          apply Hdis2.
+        * rewrite /stbor_ghost_stack.
+          iApply big_sepL2_cons. by iFrame "Hgstk".
+  Qed.
+
   (** Allocation *)
 
   (* Allocation never fails, since we do not check if the location has already
@@ -949,7 +985,47 @@ Section defs.
     iApply ("Hclose" with "Hopen").
   Qed.
 
-  (* TODO: Ghost disabling *)
+  Lemma stbor_disable_ctx gstk2 l gstk1 stbor :
+    ghost_disable gstk1 gstk2 →
+    stbor_ctx stbor -∗
+    stbor_active l 1 gstk1 ==∗
+    stbor_ctx stbor ∗
+    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.
+  Qed.
+
+  Lemma stbor_disable gstk2 gstk1 l E :
+    ↑stborN ⊆ E →
+    ghost_disable gstk1 gstk2 →
+    stbor_inv -∗
+    stbor_active l 1 gstk1 ={E}=∗
+    stbor_active l 1 gstk2.
+  Proof.
+    iIntros (? Hdis) "#BOR Hactive◯".
+    iMod (stbor_inv_acc with "BOR") as (stbor) "[Hopen Hclose]"; first done.
+    iMod (stbor_disable_ctx with "Hopen Hactive◯") as "[Hopen Hactive◯]"; first done.
+    iFrame "Hactive◯".
+    iApply ("Hclose" with "Hopen").
+  Qed.
+
   (* TODO: Retag SharedRW *)
 
 End defs.