switch lock spec to be accessor-based

_CoqProject

@@ -53,6 +53,7 @@ theories/typing/lib/fake_shared_box.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/rc.v
+theories/typing/lib/mutex.v
 theories/typing/lib/refcell/refcell.v
 theories/typing/lib/refcell/ref.v
 theories/typing/lib/refcell/refmut.v

theories/lang/lib/lock.v

@@ -22,110 +22,88 @@ Proof. solve_inG. Qed.
 Section proof.
   Context `{!lrustG Σ, !lockG Σ} (N : namespace).
 
-  Definition lockname := (gname * gname)%type.
-
-  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
+  Definition lock_proto (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
 
-  Definition is_lock (γ : lockname) (l : loc) (R : iProp Σ) : iProp Σ :=
-    cinv N (γ.1) (lock_inv (γ.2) l R).
-
-  Definition own_lock (γ : lockname) : frac → iProp Σ :=
-    cinv_own (γ.1).
+  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
-  Definition locked (γ : lockname): iProp Σ := own (γ.2) (Excl ()).
-
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
+  Global Instance lock_inv_ne γ l : NonExpansive (lock_proto γ l).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
-  Proof. solve_contractive. Qed.
-  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
-  Proof. exact: contractive_ne. Qed.
 
-  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
-  Proof. apply _. Qed.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γ : lockname) : locked γ -∗ locked γ -∗ False.
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
 
-  Lemma is_lock_iff γ l R R' :
-    □ ▷ (R ↔ R') -∗ is_lock γ l R -∗ is_lock γ l R'.
+  Lemma lock_proto_iff γ l R R' :
+    □ (R ↔ R') -∗ lock_proto γ l R -∗ lock_proto γ l R'.
   Proof.
-    iIntros "#HRR' Hlck". iApply cinv_iff; last done. iNext. iAlways.
-    iSplit; iIntros "Hinv"; iDestruct "Hinv" as (b) "[Hl HR]"; iExists b;
-      iFrame "Hl"; (destruct b; first done); iDestruct "HR" as "[$ HR]";
-      by iApply "HRR'".
+    iIntros "#HRR' Hlck". iDestruct "Hlck" as (b) "[Hl HR]". iExists b.
+    iFrame "Hl". destruct b; first done. iDestruct "HR" as "[$ HR]".
+    by iApply "HRR'".
   Qed.
 
   (** The main proofs. *)
-  Lemma newlock_inplace (E : coPset) (R : iProp Σ) l (b : bool) :
-    l ↦ #b -∗ (if b then True else ▷ R) ={E}=∗ ∃ γ, is_lock γ l R ∗ own_lock γ 1%Qp.
+  Lemma lock_proto_create (E : coPset) (R : iProp Σ) l (b : bool) :
+    l ↦ #b -∗ (if b then True else R) ={E}=∗ ∃ γ, lock_proto γ l R.
   Proof.
     iIntros "Hl HR".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iMod (cinv_alloc _ N (lock_inv γ l R) with "[-]") as (γ') "Hlock".
-    { iExists b. destruct b; by iFrame. }
-    iModIntro. iExists (_, _). eauto.
-  Qed.
-
-  Lemma newlock_spec (R : iProp Σ) :
-    {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; is_lock γ l R ∗ own_lock γ 1%Qp }}}.
-  Proof.
-    iIntros (Φ) "HR HΦ". iApply wp_fupd.
-    wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
-    rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
-    wp_let. wp_write. iMod (newlock_inplace with "Hl HR") as (γ) "?".
-    by iApply "HΦ".
+    iExists _, _. iFrame "Hl". destruct b; first done. by iFrame.
   Qed.
 
-  Lemma destroy_lock E γ l R :
+  Lemma lock_proto_destroy E γ l R :
     ↑N ⊆ E → 
-    is_lock γ l R -∗ own_lock γ 1%Qp ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷ R.
+    lock_proto γ l R ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
   Proof.
-    iIntros (?) "#Hinv Hown".
-    iMod (cinv_cancel with "Hinv Hown") as (b) "[>Hl HR]"; first done.
-    iExists b. destruct b; first by eauto.
+    iIntros (?) "Hlck". iDestruct "Hlck" as (b) "[Hl HR]".
+    iExists b. iFrame "Hl". destruct b; first done.
     iDestruct "HR" as "[_ $]". done.
   Qed.
 
-  Lemma try_acquire_spec γ l R q :
-    {{{ is_lock γ l R ∗ own_lock γ q }}} try_acquire [ #l ]
-    {{{ b, RET #b; (if b is true then locked γ ∗ R else True) ∗ own_lock γ q }}}.
+  (* At this point, it'd be really nice to have some sugar for symmetric
+     accessors. *)
+  Lemma try_acquire_spec E γ l R P :
+    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} try_acquire [ #l ] @ E
+    {{{ b, RET #b; (if b is true then locked γ ∗ R else True) ∗ P }}}.
   Proof.
-    iIntros (Φ) "[Hinv Hown] HΦ".
-    wp_rec. iMod (cinv_open with "Hinv Hown") as "(Hinv & Hown & Hclose)"; first done.
+    iIntros "#Hproto !# * HP HΦ".
+    wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
     iDestruct "Hinv" as ([]) "[Hl HR]".
     - wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
-      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iMod ("Hclose" with "[Hl]"); first (iExists true; by eauto).
       iModIntro. iApply ("HΦ" $! false). auto.
     - wp_apply (wp_cas_int_suc with "Hl"); [done..|]. iIntros "Hl".
       iDestruct "HR" as "[Hγ HR]".
-      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. rewrite /locked. iApply ("HΦ" $! true with "[$Hγ $HR $Hown]").
+      iMod ("Hclose" with "[Hl]") as "HP"; first (iExists true; by eauto).
+      iModIntro. rewrite /locked. iApply ("HΦ" $! true with "[$Hγ $HR $HP]").
   Qed.
 
-  Lemma acquire_spec γ l R q :
-    {{{ is_lock γ l R ∗ own_lock γ q }}} acquire [ #l ]
-    {{{ RET #(); locked γ ∗ R ∗ own_lock γ q }}}.
+  Lemma acquire_spec E γ l R P :
+    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); locked γ ∗ R ∗ P }}}.
   Proof.
-    iIntros (Φ) "[#Hinv Hown] HΦ". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "[$Hinv $Hown]"). iIntros ([]).
+    iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
+    iPoseProof (try_acquire_spec with "[Hproto] * HP") as "Hacq".
+    { iFrame "Hproto". (* FIXME: Just saying "Hproto" in the pattern above should work. *) }
+    wp_apply "Hacq". (* FIXME: Using `(try_acquire_spec with "[Hproto] * HP")` to avoid the
+                        iPoseProof should work. *)
+    iIntros ([]).
     - iIntros "[[Hlked HR] Hown]". wp_if. iApply "HΦ"; iFrame.
     - iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown [HΦ]"). auto.
   Qed.
 
-  Lemma release_spec γ l R q :
-    {{{ is_lock γ l R ∗ locked γ ∗ R ∗ own_lock γ q }}} release [ #l ]
-    {{{ RET #(); own_lock γ q }}}.
+  Lemma release_spec E γ l R P :
+    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
+    {{{ locked γ ∗ R ∗ P }}} release [ #l ] @ E {{{ RET #(); P }}}.
   Proof.
-    iIntros (Φ) "(Hinv & Hlocked & HR & Hown) HΦ".
-    rewrite /release /=. wp_let.
-    iMod (cinv_open with "Hinv Hown") as "(Hinv & Hown & Hclose)"; first done.
-    iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ". iFrame "Hown".
-    iApply "Hclose". iNext. iExists false. by iFrame.
+    iIntros "#Hproto !# * (Hlocked & HR & HP) HΦ". wp_let.
+    iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
+    iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
+    iApply "Hclose". iExists false. by iFrame.
   Qed.
 End proof.
 
-Typeclasses Opaque is_lock locked.
+Typeclasses Opaque lock_proto locked.

theories/lifetime/lifetime.v

@@ -55,6 +55,12 @@ Proof.
   iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
 
+Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
+Proof.
+  iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
+  iNext. iAlways. iSplit; iIntros "?"; iApply "HP"; done.
+Qed.
+
 Lemma bor_later E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.