Sketch of the lockable concept

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

@@ -0,0 +1,64 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+
+(** This file captures the following "named requirements":
+    - [BasicLockable](https://cppreference.com/cpp/named_req/BasicLockable)
+    - [Lockable](https://cppreference.com/cpp/named_req/Lockable)
+
+    It proposes a pattern for capturing these using Rocq typeclasses such
+    that clients can use these to depend on
+ *)
+
+Section with_cpp.
+  Context `{Σ : cpp_logic} {σ : genv}.
+
+  (* NOTE: This is *not* meant to be a statement about the way that
+     things should be packaged (bundled or unbundled), just a demonstration
+     of the way that specifications can be written in a higher-order way.
+   *)
+
+  (** This captures [BasicLockable](https://cppreference.com/cpp/named_req/BasicLockable) *)
+  Class BasicLockable (ty : type) {T : Type} (R : cQp.t -> T -> Rep) : Type :=
+  { do_lock : ptr -> T -> mpred -> mpred
+    (* the WP for <ty::lock()> *)
+  ; do_unlock : ptr -> T -> mpred -> mpred
+    (* the WP for <ty::unlock()> *)
+  }.
+  (** TODO: consider adding a Hint Mode*)
+  (*
+  #[global] Hint Mode BasicLockable ! - ! : typeclass_instances.
+  #[global] Arguments do_lock ty {T} R {BL} _ _ _ : rename.
+  #[global] Arguments do_unlock ty {T} R {BL} _ _ _ : rename.
+  *)
+
+  Section with_BasicLockable.
+    Context (ty : type) {T: Type} (R : cQp.t -> T -> Rep) {BL : BasicLockable ty R}.
+
+    Definition lock_basic_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_lock this m K
+       \post K).
+
+    Definition unlock_basic_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_unlock this m K
+       \post K).
+  End with_BasicLockable.
+
+  (** This captures [Lockable](https://cppreference.com/cpp/named_req/Lockable) *)
+  Class Lockable (ty : type) {T : Type} (R : cQp.t -> T -> Rep) {BASIC_LOCKABLE : BasicLockable ty R} : Type :=
+  { do_try_lock : ptr -> T -> (bool -> mpred) -> mpred }.
+  (* TODO: Hint Mode here too. *)
+
+  Section with_Lockable.
+    Context (ty : type) {T : Type} (R : cQp.t -> T -> Rep) `{LOCKABLE : Lockable (T:=T) ty R}.
+
+    Definition try_lock_lockable : ptr -> WpSpec mpred val val :=
+      (\this this
+       \prepost{q m} this |-> R q m
+       \pre{K} do_try_lock this m K
+       \post{r}[Vbool r] K r).
+  End with_Lockable.
+
+End with_cpp.

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

@@ -1,5 +1,8 @@
-Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
+(* Export all specifications.
+Keep them listed in alphabetical order. *)
+Require Export skylabs.brick.libstdcpp.mutex.spec.defer_lock_t.
 Require Export skylabs.brick.libstdcpp.mutex.spec.lock_guard.
+Require Export skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.recursive_mutex.
 Require Export skylabs.brick.libstdcpp.mutex.spec.scoped_lock.
 Require Export skylabs.brick.libstdcpp.mutex.spec.unique_lock.

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

@@ -0,0 +1,23 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+
+Module defer_lock_t.
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Parameter R : forall {σ : genv}, cQp.t -> Rep.
+  #[only(cfracsplittable, type_ptr="std::defer_lock_t")] derive R.
+
+  cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (
+    \this this
+    \arg{other} "other" (Vptr other)
+    \prepost{q} other |-> R q
+    \post this |-> R 1$m
+  ).
+  cpp.spec "std::defer_lock_t::~defer_lock_t()" as defer_lock_dtor_spec from source with (
+    \this this
+    \pre this |-> R 1$m
+    \post emp
+  ).
+End with_cpp.
+End defer_lock_t.

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

@@ -7,9 +7,11 @@ Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.auto.cpp.weakly_local_with.
 
 Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.auto.cpp.proof.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
 
 Import linearity.
 
@@ -59,6 +61,24 @@ Section with_cpp.
   Context `{MOD : source ⊧ σ}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
+  Definition do_unlock (thr : thread_idT) (lk : gname * Qp * mpred) (Q : mpred) : mpred :=
+      match lk with
+      | (g, q, P) =>
+        locked g thr q ** ▷P **
+        (* TODO readd *)
+        (* ▷ *)
+        (token g q -* Q)
+      end.
+
+  Definition do_lock (thr : thread_idT) (lk : gname * Qp * mpred) (K: mpred) : mpred :=
+      match lk with
+      | (g, q, P) =>
+        token g q **
+        (* TODO readd *)
+        (* ▷ *)
+        (locked g thr q ** ▷P -* K)
+      end.
+
   cpp.spec "std::mutex::mutex()" as ctor_spec with
       (\this this
       \pre{P} ▷P
@@ -75,6 +95,14 @@ Section with_cpp.
       \pre token g q
       \post P ** locked g thr q).
 
+  cpp.spec "std::mutex::lock()" as lock_spec_alt with
+      (\this this
+      \prepost{q P g} this |-> R g q$m P (* part of both pre and post *)
+      \persist{thr} current_thread thr
+      \pre{K} do_lock thr (g, q, P) K
+      \post K
+      ).
+
   cpp.spec "std::mutex::try_lock()" as try_lock_spec with
       (\this this
       \prepost{q P g} this |-> R g q P (* part of both pre and post *)
@@ -90,11 +118,44 @@ Section with_cpp.
       \pre ▷P
       \post token g q).
 
+  cpp.spec "std::mutex::unlock()" as unlock_spec_alt with
+      (\this this
+      \prepost{q P g} this |-> R g q$m P (* part of both pre and post *)
+      \persist{thr} current_thread thr
+      \pre{K} do_unlock thr (g, q, P) K
+      \post K).
+
   cpp.spec "std::mutex::~mutex()" as dtor_spec with
       (\this this
       \pre{g P} this |-> R g 1$m P ** token g 1
       \post P).
 
+  Lemma lock_spec_entails_lock_spec_alt : lock_spec |-- lock_spec_alt.
+  Proof.
+    apply specify_mono.
+    rewrite /do_lock.
+    go. iExists q$m%cQp. go.
+  Qed.
+
+  Lemma unlock_spec_entails_unlock_spec_alt : unlock_spec |-- unlock_spec_alt.
+  Proof.
+    apply specify_mono.
+    rewrite /do_unlock.
+    go. iExists q$m%cQp. go.
+  Qed.
+
+  (* candidate? *)
+  Definition T : Type := gname * mpred.
+
+  #[global,program] Instance mutex_basic_lockable : BasicLockable (T := thread_idT * gname * Qp * mpred) "std::mutex" (λ q '(thr, γ, q', P), R γ q$m P) :=
+  { do_lock := fun this '(thr, γ, q', P) K => do_lock thr (γ, q', P) K
+  ; do_unlock := fun this '(thr, γ, q', P) K => do_unlock thr (γ, q', P) K }.
+
+  (*
+  #[global,program] Instance mutex_basic_lockable : BasicLockable (T := gname * Qp * mpred) "std::mutex" (λ q '(thr, γ, q', P), R γ q$m P) :=
+  { do_lock := fun this '(γ, q', P) K => do_lock thr (γ, q', P) K
+  ; do_unlock := fun this '(γ, q', P) K => do_unlock thr (γ, q', P) K }.
+  *)
 End with_cpp.
 End mutex.
 

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

@@ -4,27 +4,6 @@ Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 
-Module defer_lock_t.
-Section with_cpp.
-  Context `{Σ : cpp_logic, σ : genv}.
-
-  Parameter R : forall {σ : genv}, cQp.t -> Rep.
-  #[only(cfracsplittable, type_ptr="std::defer_lock_t")] derive R.
-
-  cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (
-    \this this
-    \arg{other} "other" (Vptr other)
-    \prepost{q} other |-> R q
-    \post this |-> R 1$m
-  ).
-  cpp.spec "std::defer_lock_t::~defer_lock_t()" as defer_lock_dtor_spec from source with (
-    \this this
-    \pre this |-> R 1$m
-    \post emp
-  ).
-End with_cpp.
-End defer_lock_t.
-
 Module unique_lock.
 Section with_cpp.
   Context `{Σ : cpp_logic}.