recursive mutex spec: Instantiate ghost state

rocq-brick-libstdcpp/proof/mutex/spec.v

@@ -83,43 +83,133 @@ Section with_cpp.
 End with_cpp.
 End mutex.
 
+
+Require Import iris.algebra.gset.
+
 Module recursive_mutex.
+  (*
+  Inductive locked_ghost :=
+  | Zero (threads : gset thread_idT) : locked_ghost
+  | NonZero (threads : gset thread_idT) (owner : thread_idT) (count : nat) : locked_ghost
+  | Bot.
+
+  NonZero . Zero = NonZero
+
+  *)
+
+  Canonical Structure locked_ghostUR : ucmra :=
+    prodR (gset_disjR thread_idTO) (optionR (exclR (prodO thread_idTO natO))).
+  (* Not prodO thread_idTO natO. *)
+  (* A thread that has zero, locked γ th 0 does not even know which thread has non-0. *)
+  Canonical Structure locked_cmraR := authR locked_ghostUR.
 
   (** <<locked γ th n>> <<th>> owns the mutex <<γ>> <<n>> times. *)
-  #[projections(primitive=no)]
   Class lockedG `{Σ : cpp_logic} := {
+    #[local] has_locked :: HasOwn (iPropI _Σ) locked_cmraR;
+    #[local] has_locked_upd :: HasOwnUpd (iPropI _Σ) locked_cmraR;
+    #[local] has_locked_valid :: HasOwnValid (iPropI _Σ) locked_cmraR
   }.
   #[global] Arguments lockedG {_ _} Σ : assert.
 
-  Parameter locked :
-    ∀ `{Σ : cpp_logic, !lockedG Σ}
-    (γ : gname) (th : thread_idT) (n : nat), mpred.
+  sl.lock
+  Definition locked `{Σ : cpp_logic, !lockedG Σ}
+      (γ : gname) (th : thread_idT) (n : nat) : mpred :=
+      own γ (◯ (GSet {[ th ]},
+        match n with
+        | 0 => None
+        | S n => Excl' (th, n)
+        end)).
 
-  Parameter used_threads :
-    ∀ `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ}
-    (γ : gname) (s : gset thread_idT), mpred.
+  sl.lock
+  Definition used_threads
+    `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ}
+    (γ : gname) (s : gset thread_idT) : mpred :=
+    ∃ n,
+    match n with
+    | 0 => own γ (● (GSet s, None))
+    | S n => ∃ t, own γ (● (GSet s, Excl' (t, n)))
+    end.
 
   #[only(timeless)] derive locked.
   #[only(timeless)] derive used_threads.
 
+  (* XXX upstream *)
+  (* #[only(fwd,bwd(l2r))] derive monPred_at_sep.
+  #[only(fwd,bwd(l2r))] derive monPred_at_embed.
+  #[only(fwd,bwd(l2r))] derive monPred_at_pure.
+  #[only(fwd,bwd(l2r))] derive monPred_at_only_provable. *)
+  (* #[only(fwd,bwd(l2r))] derive monPred_at_exist. *)
+  (* #[only(fwd)] derive monPred_at_exist. *)
+
   Section locked_with_cpp.
     Context `{Σ : cpp_logic}.
     Context `{!lockedG Σ}.
     Context `{!HasStdThreads Σ}.
 
-    Axiom use_thread : ∀ th g s,
+    Lemma use_thread th g s :
       th ∉ s ->
       current_thread th ** used_threads g s |--
       |==> used_threads g (s ∪ {[ th ]}) ** locked g th 0.
+    Proof.
+      rewrite used_threads.unlock locked.unlock => Hni.
+      iIntros "[#CT (% & A)]".
+      destruct n.
+      {
+        iMod (own_update with "A") as "[● ◯]".
+        { apply (auth_update_alloc _ (GSet ({[th]} ∪ s), None) (GSet ({[th]}), None)).
+          apply prod_local_update_1.
+          apply gset_disj_alloc_empty_local_update. set_solver. }
+        iEval (
+          replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO))))
+          ) in "◯".
+        iFrame.
+        iModIntro; iExists 0. rewrite comm_L //.
+      }
+      {
+        iDestruct "A" as "(%t & A)".
+        iMod (own_update with "A") as "[● ◯]".
+        { apply (auth_update_alloc _ (GSet ({[th]} ∪ s), Excl' (t, n)) (GSet {[th]}, None)).
+          apply prod_local_update_1.
+          apply gset_disj_alloc_empty_local_update. set_solver.
+        }
+        iEval (
+          replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO))))
+          ) in "◯".
+        iFrame.
+        iModIntro; iExists (S n). rewrite comm_L //. iFrame.
+      }
+    Qed.
 
-    #[global] Declare Instance
+    #[global] Instance
       locked_WeaklyObjective γ thr n :
       WeaklyObjective (PROP := iPropI _) (locked γ thr n).
+    Proof. rewrite locked.unlock. apply _. Qed.
 
-    Axiom locked_excl_same_thread : forall g th n m,
+    Lemma locked_excl_same_thread g th n m :
       locked g th n ** locked g th m |-- False.
-    Axiom locked_excl_different_thread : forall g th th' n m,
+    Proof.
+      rewrite locked.unlock.
+      iIntros "[A B]".
+      iDestruct (own_valid_2 with "A B") as "%".
+      rewrite -auth_frag_op -pair_op auth_frag_valid in H.
+      destruct H.
+      rewrite /= gset_disj_valid_op /= in H.
+      set_solver.
+    Qed.
+
+    Lemma locked_excl_different_thread g th th' n m :
       locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True.
+    Proof.
+      destruct (decide (th = th')) as [->|Hne]. {
+        rewrite locked_excl_same_thread. work.
+      }
+      rewrite locked.unlock.
+      iIntros "[A B]".
+      destruct n, m; try auto.
+      iDestruct (own_valid_2 with "A B") as "%".
+      rewrite -auth_frag_op -pair_op auth_frag_valid in H.
+      destruct H as [_ H]. done.
+    Qed.
 
   End locked_with_cpp.
 
@@ -454,18 +544,30 @@ Section with_cpp.
     ework with br_erefl.
   Qed.
 
+(* Require Import bluerock.auto.cpp.prelude.proof. *)
   Lemma lock_spec_impl_lock_spec' :
     lock_spec |-- lock_spec'.
   Proof using MOD HOV HOU.
     apply specify_mono; work.
+    Import auto_frac.
+    iExists q, q'.
 
-    iExists _, q', (∃ t : acquire_state TT, [| acquire n t |] ∗
-              ▷ acquireable g th t P)%I.
-    work.
+    iExists (∃ t,
+      [| acquire n t |] ∗
+      (* token (lock_gname g) (cQp.scale (1 / 2) q') ∗
+      a |-> R (lock_gname g) (cQp.scale (1 / 2) q) ∗ *)
+      ▷ acquireable g th t P)%I.
 
     wname [bi_wand] "W".
     wfocus (bi_wand _ _) "W".
     { work $usenamed=true. }
+    work.
+    (* wname [token] "T".
+    wname [R] "R".
+    wname [acquireable] "A".
+    (* About atomic_commit . *)
+    wfocus (atomic_commit _ _ _ _ _ _) "T R A". *)
+    (* iStopProof; work. *)
     iAcIntro; rewrite /commit_acc/=.
     rewrite inv_rmutex.unlock acquireable.unlock.
     iInv rmutex_namespace as (??) "(>Hn & Hcases)" "Hclose".
@@ -483,7 +585,7 @@ Section with_cpp.
       iMod (own_update_2 with "Hn Hcase") as "(Hg & Hcase)";
         first apply (excl_auth_update _ _ (1, th)).
       iMod "Hclose'" as "_".
-      wname [locked _ th _] "Hlocked".
+      wname [recursive_mutex.locked _ th _] "Hlocked".
       iMod ("Hclose" with "[$Hg $Hlocked //]") as "_".
       iMod (bi.later_exist_except_0 with "HP") as "(%args & HP)".
       iModIntro.
@@ -496,7 +598,7 @@ Section with_cpp.
       iMod (own_update_2 with "Hn [$]") as "(Hg & Hcase)";
         first apply (excl_auth_update _ _ (S (S n), th)).
       iMod "Hclose'" as "_".
-      wname [locked _ th _] "Hlocked".
+      wname [recursive_mutex.locked _ th _] "Hlocked".
       iMod ("Hclose" with "[$Hg $Hlocked //]") as "_".
       iModIntro.
       iExists (Held (S n) xs). work $usenamed=true.