add more abstract logic

_CoqProject

@@ -32,6 +32,7 @@ theories/lang/heap.v
 theories/lang/tactics.v
 theories/lang/lifting.v
 theories/lang/stbor/examples/reborrowing.v
+theories/lang/stbor/examples/abstract.v
 # theories/lang/proofmode.v
 # theories/lang/races.v
 # theories/lang/lib/memcpy.v

theories/lang/stbor/examples/abstract.v

+From iris.algebra Require Import lib.excl_auth.
+From iris.bi Require Import fractional.
+From iris.base_logic Require Export lib.own invariants.
+From iris.proofmode Require Export tactics.
+From lrust.lang.stbor Require Export stbor_semantics stbor_ghost.
+From lrust.lang Require Export lang notation lifting heap.
+Set Default Proof Using "Type".
+
+Section defs.
+  Context `{!lrustG Σ}.
+
+  Definition uniq_ref (p : ptr) (gstk : ghost_stack) (v : val) : iProp Σ :=
+    p.1 ↦ v ∗ stbor_stack p.1 1 gstk ∗ stbor_grants_write gstk p.2.
+
+  Definition shr_ref (p : ptr) (q : Qp) (gstk : ghost_stack)  (v : val) : iProp Σ :=
+    ∃ γg gstk', p.1 ↦{q} v ∗ stbor_stack p.1 q gstk ∗ ⌜gstk = GSharedRO γg :: gstk'⌝ ∗ stbor_grants_read gstk p.2.
+
+  Lemma wpabs_alloc E :
+    ↑stborN ⊆ E →
+    {{{ True }}}
+      Alloc (Lit $ LitInt 1) @ E
+    {{{ l tg gstk, RET LitV $ LitLoc (l, tg); †l…1 ∗ uniq_ref (l, tg) gstk #LitPoison }}}.
+  Proof.
+    iIntros (? Φ) "_ HΦ".
+    iApply wp_alloc; [solve_ndisj|done|].
+    iModIntro. iIntros (l tg) "(Hdel & Hl & Hstk)".
+    iApply "HΦ". iFrame "Hdel Hstk".
+    iSplit=>//.
+    rewrite /heap_mapsto_vec big_sepL_singleton.
+    rewrite /shift_loc Z.add_0_r -surjective_pairing.
+    iFrame "Hl".
+  Qed.
+
+  Lemma wpabs_free E l tg gstk v :
+    ↑stborN ⊆ E →
+    {{{ uniq_ref (l, tg) gstk v ∗ †l…1 }}}
+      Free (Lit $ LitInt 1) (Lit $ LitLoc (l, tg)) @ E
+    {{{ RET LitV LitPoison; True }}}.
+  Proof.
+    iIntros (? Φ) "[(Hl & Hstk & #Hgrants) Hdel] HΦ".
+    iApply (wp_free with "Hgrants [Hl $Hstk $Hdel]"); first solve_ndisj.
+    { iModIntro. iDestruct (heap_mapsto_vec_singleton with "Hl") as "Hl".
+      iFrame "Hl". }
+    iApply "HΦ".
+  Qed.
+
+  Lemma wpabs_read_uniq_na E l tg v gstk :
+    ↑stborN ⊆ E →
+    {{{ uniq_ref (l, tg) gstk v }}}
+      Read Na1Ord (Lit $ LitLoc (l, tg)) @ E
+    {{{ RET v; uniq_ref (l, tg) gstk v }}}.
+  Proof.
+    iIntros (? Φ) "Href HΦ".
+    iDestruct "Href" as "(Hl & Hstk & #Hgrants)".
+    iDestruct (stbor_grants_write_to_read with "Hgrants") as "#Hgrants'".
+    iApply (wp_read_na with "Hgrants' [$Hl $Hstk]"); first solve_ndisj.
+    iModIntro. iIntros "[Hl Hstk]".
+    iApply "HΦ".
+    iFrame "Hl Hstk Hgrants".
+  Qed.
+
+  Lemma wpabs_write_uniq_na e v E gstk tg l v' :
+    IntoVal e v →
+    ↑stborN ⊆ E →
+    {{{ uniq_ref (l, tg) gstk v' }}}
+      Write Na1Ord (Lit $ LitLoc (l, tg)) e @ E
+    {{{ RET LitV LitPoison; uniq_ref (l, tg) gstk v }}}.
+  Proof.
+    iIntros (? ? Φ) "(Hl & Hstk & #Hgrants) HΦ".
+    iApply (wp_write_na with "Hgrants [$Hl $Hstk]"); first solve_ndisj.
+    iModIntro. iIntros "[Hl Hstk]".
+    iApply "HΦ".
+    iFrame "Hl Hstk Hgrants".
+  Qed.
+
+  Lemma wpabs_retag_uniq_uniq l tgold gstk v int_mut E :
+    ↑lft_userN ⊆ E →
+    stbor_inv -∗
+    {{{ uniq_ref (l, tgold) gstk v }}}
+      Retag [int_mut] (PkRef Mutable) (Lit $ LitLoc (l, tgold)) @ E
+    {{{ tgnew gstk', RET LitV $ LitLoc (l, tgnew);
+        uniq_ref (l, tgnew) gstk' v ∗
+        (uniq_ref (l, tgnew) gstk' v ={E}=∗ uniq_ref (l, tgold) gstk v)
+    }}}.
+  Proof.
+    iIntros (?) "#BOR !>". iIntros (Φ) "Href HΦ".
+    iDestruct "Href" as "(Hl & Hstk & #Hgrants)".
+    iApply (wp_retag_unique with "Hgrants Hstk"); first solve_ndisj.
+    iIntros "!>" (tgnew) "Hstk'".
+    iApply "HΦ".
+    rewrite /uniq_ref. iFrame "Hl Hstk'".
+    iSplit=>//.
+    iIntros "($ & Hstk & _)". iFrame "Hgrants".
+    iApply (stbor_remove with "BOR Hstk"); first solve_ndisj.
+    by apply suffix_cons_r.
+  Qed.
+
+  (* TODO: Move this *)
+  Lemma stbor_grants_write_to_read_push_sharedro gstk tg γg :
+    stbor_grants_write gstk tg -∗
+    stbor_grants_read (GSharedRO γg :: gstk) tg.
+  Proof.
+    iIntros "#Hgrants".
+    destruct gstk as [|[| | |]]; [done| |done| |done].
+    - iRight. iApply "Hgrants".
+    - iRight. iLeft. iApply "Hgrants".
+  Qed.
+
+  Lemma convert_uniq_to_shr l tg gstk v E :
+    ↑lft_userN ⊆ E →
+    stbor_inv -∗
+    uniq_ref (l, tg) gstk v ={E}=∗
+    ∃ gstk',
+      shr_ref (l, tg) 1 gstk' v ∗
+      (∀ tg', shr_ref (l, tg') 1 gstk' v ={E}=∗ uniq_ref (l, tg) gstk v).
+  Proof.
+    iIntros (?) "#BOR Href".
+    iDestruct "Href" as "(Hl & Hstk & #Hgrants)".
+    iDestruct (stbor_grants_write_to_no_sharedro with "Hgrants") as %Hnoshared.
+    iMod (stbor_push_sharedro with "BOR Hstk") as (γg) "Hstk'"; [solve_ndisj|done|].
+    iModIntro. iExists _. iFrame "Hl Hstk'".
+    iSplit.
+    { iExists _, _. iSplit; first done.
+      by iApply stbor_grants_write_to_read_push_sharedro. }
+    iIntros (tg') "Href".
+    iDestruct "Href" as (γg' gstk') "(Hl & Hstk & _)".
+    iFrame "Hl Hgrants".
+    iApply (stbor_remove with "BOR Hstk"); first solve_ndisj.
+    by apply suffix_cons_r.
+  Qed.
+
+  Lemma wpabs_read_na E l tg q v gstk :
+    ↑stborN ⊆ E →
+    {{{ shr_ref (l, tg) q gstk v }}}
+      Read Na1Ord (Lit $ LitLoc (l, tg)) @ E
+    {{{ RET v; shr_ref (l, tg) q gstk v }}}.
+  Proof.
+    iIntros (? Φ) "Href HΦ".
+    iDestruct "Href" as (γg gstk') "(Hl & Hstk & -> & #Hgrants)".
+    iApply (wp_read_na with "Hgrants [$Hl $Hstk]"); first solve_ndisj.
+    iIntros "!> [Hl Hstk]". iApply "HΦ".
+    iExists _, _. iFrame "Hl Hstk Hgrants". done.
+  Qed.
+
+  Lemma wpabs_retag_shr_shr l tgold q1 q2 gstk v E :
+    ↑lft_userN ⊆ E →
+    stbor_inv -∗
+    {{{ shr_ref (l, tgold) (q1 + q2) gstk v }}}
+      Retag [OutsideUnsafeCell] (PkRef Immutable) (Lit $ LitLoc (l, tgold)) @ E
+    {{{ tgnew, RET LitV $ LitLoc (l, tgnew);
+        shr_ref (l, tgold) q1 gstk v ∗
+        shr_ref (l, tgnew) q2 gstk v
+    }}}.
+  Proof.
+    iIntros (?) "#BOR !>". iIntros (Φ) "Href HΦ".
+    iDestruct "Href" as (γg gstk') "(Hl & Hstk & -> & #Hgrants)".
+    iDestruct "Hl" as "[Hl1 Hl2]".
+    iDestruct "Hstk" as "[Hstk1 Hstk2]".
+    iApply (wp_retag_sharedro_add with "Hgrants Hstk1"); first solve_ndisj.
+    iModIntro. iIntros (tgnew) "[Hstk1 Hnew]".
+    iApply "HΦ".
+    iFrame "Hl1 Hl2 Hstk1 Hstk2 Hgrants Hnew".
+    iSplit; eauto.
+  Qed.
+
+  Lemma shr_combine l tg1 tg2 q1 q2 gstk v :
+    shr_ref (l, tg1) q1 gstk v -∗
+    shr_ref (l, tg2) q2 gstk v -∗
+    shr_ref (l, tg1) (q1 + q2) gstk v.
+  Proof.
+    iIntros "Href1 Href2".
+    iDestruct "Href1" as (γg1 gstk1) "(Hl1 & Hstk1 & -> & #Hgrants1)".
+    iDestruct "Href2" as (γg2 gstk2) "(Hl2 & Hstk2 & Heq2 & #Hgrants2)".
+    iCombine "Hl1 Hl2" as "Hl".
+    iCombine "Hstk1 Hstk2" as "Hstk".
+    iFrame "Hl Hstk Hgrants1". eauto.
+  Qed.
+
+End defs.