From 814597b757a11fd51e07ba334c90cecd25167ee9 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Thu, 28 May 2026 19:38:26 +0200
Subject: [PATCH 01/12] mutex/spec: extract do_lock and do_unlock

https://github.com/SkyLabsAI/auto/issues/66 strikes again.
---
 rocq-brick-libstdcpp/proof/mutex/spec/mutex.v | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index a687349..6ba581f 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -7,6 +7,7 @@ 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.
@@ -59,6 +60,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 +94,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 +117,31 @@ 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.
 End with_cpp.
 End mutex.
 

From 106971cdc683d65abe53ef839814b48f3a8a1490 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 14:49:41 +0200
Subject: [PATCH 02/12] Extract defer_lock_t.v

---
 rocq-brick-libstdcpp/proof/mutex/spec.v       |  5 +++-
 .../proof/mutex/spec/defer_lock_t.v           | 23 +++++++++++++++++++
 .../proof/mutex/spec/unique_lock.v            | 21 -----------------
 3 files changed, 27 insertions(+), 22 deletions(-)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v
index 4264c53..c5e4344 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec.v
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v b/rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v
new file mode 100644
index 0000000..e9bbd60
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index 47f86e1..ae2ce6c 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/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}.

From 8bb28276ea47288786fed8e6c1c2fc8d8465c0fa Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@skylabs-ai.com>
Date: Wed, 6 May 2026 22:15:45 -0400
Subject: [PATCH 03/12] Sketch of the lockable concept

This is just a sketch.
---
 .../proof/mutex/requirements.v                |  57 +++++
 .../proof/mutex/spec/unique_lock_generic.v    | 201 ++++++++++++++++++
 2 files changed, 258 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/requirements.v
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/requirements.v b/rocq-brick-libstdcpp/proof/mutex/requirements.v
new file mode 100644
index 0000000..b970c24
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/requirements.v
@@ -0,0 +1,57 @@
+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()> *)
+  ; cfrac :> CFracSplittable_1 R }.
+
+  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 }.
+
+  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.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
new file mode 100644
index 0000000..6a9708a
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -0,0 +1,201 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+
+Require Export skylabs.brick.libstdcpp.runtime.pred.
+Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
+
+
+Module unique_lock.
+Section with_cpp.
+  Context `{Σ : cpp_logic}.
+
+  Record M {T : Type} : Type :=
+  { is_held : bool
+  ; mutex_ptr : ptr
+  ; mutex_q : Qp
+  ; mutex_m : T }.
+  Arguments M _ : clear implicits.
+  #[only(lens)] derive M.
+
+  (* a unique_lock may have an associated mutex, if so it holds
+      (Some (b * mutex_state)) where b indicates whether the unique_lock
+      has acquired the associated mutex. *)
+  Parameter R : forall {σ : genv},
+      forall ty {T} mutexR {BL : BasicLockable ty (T:=T) mutexR},
+                        cQp.t -> option (M T) -> Rep.
+
+  Definition owned {T} (om : option (M T)) : bool :=
+    match om with
+    | Some m => m.(is_held)
+    | None => false
+    end.
+
+  Definition mutex {T} (om : option (M T)) : ptr :=
+    match om with
+    | Some m => m.(mutex_ptr)
+    | None => nullptr
+    end.
+
+  #[only(cfracsplittable,type_ptr="std::unique_lock<std::mutex>")] derive R.
+
+  Section with_threads.
+    Context {σ : genv}.
+    Context `{HAS_THREADS : !HasStdThreads Σ}.
+    Context {ty : type} {mutexT : Type} (mutexR : cQp.t -> mutexT -> Rep) {BL : BasicLockable ty mutexR}.
+
+    #[global] Instance: LearnEqF1 (R ty mutexR) := ltac:(solve_learnable).
+    #[local] Notation R := (R ty (T:=mutexT) mutexR).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock()"
+      as default_ctor_spec from source with (
+      \this this
+      \post this |-> R 1$m None
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&)" as mutex_ctor_spec_alt from source with (
+      \this this
+      \arg{mp} "" (Vptr mp)
+      \pre{q m} mp |-> mutexR q$m m
+      \pre{K} do_lock mp m K
+      \post
+        this |-> R 1$m (Some {| is_held := true ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |}) **
+        K
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&, std::defer_lock_t)" as mutex_defer_ctor_spec from source with (
+      \this this
+      \arg{mp} "" (Vptr mp)
+      \pre{q m} mp |-> mutexR q$m m
+      \arg{def_p} "" (Vptr def_p)
+      \post this |-> R 1$m (Some {| is_held := false ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |})
+    ).
+
+    cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::unique_lock<std::mutex> &&)" as move_ctor_spec from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om} other |-> R 1$m om
+      \post
+        this |-> R 1$m om **
+        other |-> R 1$m None
+    ).
+
+    (** Ensures the associated mutex is unlocked and released. *)
+    Definition ensure_unlock (om : option (M mutexT)) (Q : mpred) : mpred :=
+      match om with
+      | Some {| is_held := is_held ; mutex_ptr := mp ; mutex_q := q ; mutex_m := m |} =>
+        if is_held then
+          letI* := do_unlock mp m in
+          mp |-> mutexR q$m m -* Q
+        else
+          ▷ (mp |-> mutexR q$m m -* Q)
+      | _ =>
+      (* TODO should this be [bi_later Q]? *)
+        Q
+      end%I.
+
+    (* spec for dtor written with do_unlock.
+    Should be equivalent to dtor_spec. *)
+    cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec_alt from source with (
+      \this this
+      \pre{om} this |-> R 1$m om
+      \pre{K} ensure_unlock om K
+      \post K
+      ).
+
+    cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec from source with (
+      \this this
+      \pre{om} this |-> R 1$m om
+      \pre{K}
+        match om with
+        | Some m =>
+            if m.(is_held) then do_unlock m.(mutex_ptr) m.(mutex_m) K
+            else K
+        | _ => K
+        end
+      \post K **
+        match om with
+        | Some m => m.(mutex_ptr) |-> mutexR m.(mutex_q)$m m.(mutex_m)
+        | None => emp
+        end
+      ).
+
+    (* unlock the associated mutex, if any, and set input as the associated mutex.
+    Should be equivalent to move_assign_spec. *)
+    cpp.spec "std::unique_lock<std::mutex>::operator=(std::unique_lock<std::mutex> &&)" as move_assign_spec_alt from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om1} this |-> R 1$m om1
+      \pre{om2} other |-> R 1$m om2
+      \pre{K} ensure_unlock om1 K
+      \post
+        this |-> R 1$m om2 **
+        other |-> R 1$m None **
+        K
+      ).
+
+    cpp.spec "std::unique_lock<std::mutex>::operator=(std::unique_lock<std::mutex> &&)" as move_assign_spec from source with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{om1} this |-> R 1$m om1
+      \pre{om2} other |-> R 1$m om2
+      \persist{thr} current_thread thr
+      \pre{K}
+        match om1 with
+        | Some m =>
+            if m.(is_held) then do_unlock m.(mutex_ptr) m.(mutex_m) K
+            else K
+        | _ => K
+        end
+      \post
+        this |-> R 1$m om2 **
+        other |-> R 1$m None **
+        K **
+        match om1 with
+        | Some m => m.(mutex_ptr) |-> mutexR m.(mutex_q)$m m.(mutex_m)
+        | None => emp
+        end
+      ).
+
+    Notation owns_lock_spec_body := (
+      \this this
+      \prepost{om q} this |-> R q om
+      \post [Vbool (owned om)] emp) (only parsing).
+
+    cpp.spec "std::unique_lock<std::mutex>::owns_lock() const" as owns_lock_spec
+      from source with (owns_lock_spec_body).
+
+    cpp.spec "std::unique_lock<std::mutex>::operator bool() const" as operator_bool_spec
+      from source with (owns_lock_spec_body).
+
+    cpp.spec "std::unique_lock<std::mutex>::mutex() const" as mutex_spec from source with (
+      \this this
+      \prepost{om q} this |-> R q om
+      \post[Vptr (mutex om)] emp
+    ).
+
+    (* these preconditions statically rule out cases that throw exceptions, such as:
+    - If there is no associated mutex, std::system_error with an error code of std::errc::operation_not_permitted.
+    - If the mutex is already locked by this unique_lock (in other words, owns_lock() is true), std::system_error with an error code of std::errc::resource_deadlock_would_occur. *)
+    cpp.spec "std::unique_lock<std::mutex>::lock()" as lock_spec from source with (
+      \this this
+      \pre{mm} this |-> R 1$m (Some mm)
+      \require ~~ mm.(is_held)
+      \pre{K} do_lock mm.(mutex_ptr) mm.(mutex_m) K
+      \post
+        this |-> R 1$m (Some (mm &: _is_held .= true)%lens) **
+        K).
+
+    cpp.spec "std::unique_lock<std::mutex>::unlock()" as unlock_spec from source with (
+      \this this
+      \pre{mm} this |-> R 1$m (Some mm)
+      \require mm.(is_held)
+      \pre{K} do_unlock mm.(mutex_ptr) mm.(mutex_m) K
+      \post
+        this |-> R 1$m (Some (mm &: _is_held .= false)%lens) **
+        K
+    ).
+
+  End with_threads.
+End with_cpp.
+End unique_lock.

From 82c27ac18f718d841dc0579d678f1eb9475ccc33 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:10:59 +0200
Subject: [PATCH 04/12] Unbundle CFracSplittable

---
 rocq-brick-libstdcpp/proof/mutex/requirements.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/requirements.v b/rocq-brick-libstdcpp/proof/mutex/requirements.v
index b970c24..9ae4c79 100644
--- a/rocq-brick-libstdcpp/proof/mutex/requirements.v
+++ b/rocq-brick-libstdcpp/proof/mutex/requirements.v
@@ -22,7 +22,7 @@ Section with_cpp.
     (* the WP for <ty::lock()> *)
   ; do_unlock : ptr -> T -> mpred -> mpred
     (* the WP for <ty::unlock()> *)
-  ; cfrac :> CFracSplittable_1 R }.
+  }.
 
   Section with_BasicLockable.
     Context (ty : type) {T: Type} (R : cQp.t -> T -> Rep) {BL : BasicLockable ty R}.

From 0368ecb33360f0fdd372d5c4c628733cc728be0e Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:21:51 +0200
Subject: [PATCH 05/12] Tweak type signatures

---
 .../proof/mutex/spec/unique_lock_generic.v                 | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
index 6a9708a..c503424 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -21,9 +21,8 @@ Section with_cpp.
   (* a unique_lock may have an associated mutex, if so it holds
       (Some (b * mutex_state)) where b indicates whether the unique_lock
       has acquired the associated mutex. *)
-  Parameter R : forall {σ : genv},
-      forall ty {T} mutexR {BL : BasicLockable ty (T:=T) mutexR},
-                        cQp.t -> option (M T) -> Rep.
+  Parameter R : forall {σ : genv} ty {T} mutexR `{!BasicLockable ty (T:=T) mutexR},
+    cQp.t -> option (M T) -> Rep.
 
   Definition owned {T} (om : option (M T)) : bool :=
     match om with
@@ -42,7 +41,7 @@ Section with_cpp.
   Section with_threads.
     Context {σ : genv}.
     Context `{HAS_THREADS : !HasStdThreads Σ}.
-    Context {ty : type} {mutexT : Type} (mutexR : cQp.t -> mutexT -> Rep) {BL : BasicLockable ty mutexR}.
+    Context ty {mutexT} mutexR `{!BasicLockable ty (T:=mutexT) mutexR}.
 
     #[global] Instance: LearnEqF1 (R ty mutexR) := ltac:(solve_learnable).
     #[local] Notation R := (R ty (T:=mutexT) mutexR).

From 821b6266216832319600bcb7e5de3ab39cd61e8d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:11:16 +0200
Subject: [PATCH 06/12] Generic unique_lock.R: fix Typed instance

---
 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
index c503424..d6d60b9 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -36,7 +36,10 @@ Section with_cpp.
     | None => nullptr
     end.
 
-  #[only(cfracsplittable,type_ptr="std::unique_lock<std::mutex>")] derive R.
+  #[only(cfracsplittable)] derive R.
+
+  #[global] Declare Instance R_type_ptr {σ : genv} `{!BasicLockable ty (T:=T) mutexR} q om :
+    Typed ("std::unique_lock" .<< Atype ty >>) (R ty mutexR q om).
 
   Section with_threads.
     Context {σ : genv}.

From d039f74de9eeadfcc634e0768aa12107acde1c77 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:22:04 +0200
Subject: [PATCH 07/12] Add TODOs

---
 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
index d6d60b9..5e33d68 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -49,6 +49,8 @@ Section with_cpp.
     #[global] Instance: LearnEqF1 (R ty mutexR) := ltac:(solve_learnable).
     #[local] Notation R := (R ty (T:=mutexT) mutexR).
 
+    (* TODO: all the following specs should be generalized over the lock type, except for [lock_spec] and [unlock_spec]. *)
+
     cpp.spec "std::unique_lock<std::mutex>::unique_lock()"
       as default_ctor_spec from source with (
       \this this
@@ -176,6 +178,8 @@ Section with_cpp.
       \post[Vptr (mutex om)] emp
     ).
 
+    (* TODO: these specs seem mutex-specific. unlock_spec doesn't seem good for recursive mutexes. *)
+
     (* these preconditions statically rule out cases that throw exceptions, such as:
     - If there is no associated mutex, std::system_error with an error code of std::errc::operation_not_permitted.
     - If the mutex is already locked by this unique_lock (in other words, owns_lock() is true), std::system_error with an error code of std::errc::resource_deadlock_would_occur. *)

From 6322dc7ed7d067488e831bf24c17cc29b98ae25a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:20:31 +0200
Subject: [PATCH 08/12] BasicLockable: Add TODO on Hint Mode

---
 rocq-brick-libstdcpp/proof/mutex/requirements.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/mutex/requirements.v b/rocq-brick-libstdcpp/proof/mutex/requirements.v
index 9ae4c79..4e0427a 100644
--- a/rocq-brick-libstdcpp/proof/mutex/requirements.v
+++ b/rocq-brick-libstdcpp/proof/mutex/requirements.v
@@ -23,6 +23,12 @@ Section with_cpp.
   ; 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}.
@@ -43,6 +49,7 @@ Section with_cpp.
   (** 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}.

From a18a8e3409173c9565f4bdfa5c19131a4009f266 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 15:28:33 +0200
Subject: [PATCH 09/12] Make Arguments #{global]

---
 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
index 5e33d68..4e57b01 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -15,7 +15,7 @@ Section with_cpp.
   ; mutex_ptr : ptr
   ; mutex_q : Qp
   ; mutex_m : T }.
-  Arguments M _ : clear implicits.
+  #[global] Arguments M _ : clear implicits.
   #[only(lens)] derive M.
 
   (* a unique_lock may have an associated mutex, if so it holds

From 485d4257dafb865481378dc5e4fde6359ad97967 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 19:25:10 +0200
Subject: [PATCH 10/12] unique_lock_generic: add side conditions to
 cfracsplittable

---
 .../proof/mutex/spec/unique_lock_generic.v      | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
index 4e57b01..c168700 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock_generic.v
@@ -36,13 +36,28 @@ Section with_cpp.
     | None => nullptr
     end.
 
-  #[only(cfracsplittable)] derive R.
+  #[global] Declare Instance R_cfrac {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFractional1 mutexR ->
+    CFractional1 (R ty mutexR).
+
+  #[global] Instance R_as_cfrac {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFractional1 mutexR ->
+    AsCFractional1 (R ty mutexR).
+  Proof. solve_as_cfrac. Qed.
+
+  (* #[global] Declare Instance R_timeless {σ : genv} `{!BasicLockable ty (T:=T) mutexR} : *)
+  (*   Timeless2 mutexR -> *)
+  (*   Timeless2 (R ty mutexR). *)
+
+  #[global] Declare Instance R_cfrac_valid {σ : genv} `{!BasicLockable ty (T:=T) mutexR} :
+    CFracValid1 (R ty mutexR).
 
   #[global] Declare Instance R_type_ptr {σ : genv} `{!BasicLockable ty (T:=T) mutexR} q om :
     Typed ("std::unique_lock" .<< Atype ty >>) (R ty mutexR q om).
 
   Section with_threads.
     Context {σ : genv}.
+
     Context `{HAS_THREADS : !HasStdThreads Σ}.
     Context ty {mutexT} mutexR `{!BasicLockable ty (T:=mutexT) mutexR}.
 

From c37a947cdf240f781dcf876648f287a8864b0baa Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Thu, 28 May 2026 19:45:11 +0200
Subject: [PATCH 11/12] attempt on instantiating BasicLockable interface for
 mutex (doesn't build)

---
 rocq-brick-libstdcpp/proof/mutex/spec/mutex.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index 6ba581f..f393683 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -11,6 +11,7 @@ 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.
 
@@ -142,6 +143,13 @@ Section with_cpp.
     rewrite /do_unlock.
     go. iExists q$m%cQp. go.
   Qed.
+
+  #[global] Instance mutex_basic_lockable ptr : BasicLockable _ _ :=
+  { do_lock := fun _ t K => let '(thr, lk, K) := t in do_lock thr lk K;
+    do_unlock := fun _ t K => let '(thr, lk, K) := t in do_unlock thr lk K }.
+        
+
+
 End with_cpp.
 End mutex.
 

From 792280bcde14a0cb8f2ff3abecea1a74ace28b32 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Thu, 28 May 2026 19:25:55 +0200
Subject: [PATCH 12/12] Candidate BasicLockable instance with problems

Fixed build in meeting, but we're still unhappy.
---
 rocq-brick-libstdcpp/proof/mutex/spec/mutex.v | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index f393683..7600867 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -144,12 +144,18 @@ Section with_cpp.
     go. iExists q$m%cQp. go.
   Qed.
 
-  #[global] Instance mutex_basic_lockable ptr : BasicLockable _ _ :=
-  { do_lock := fun _ t K => let '(thr, lk, K) := t in do_lock thr lk K;
-    do_unlock := fun _ t K => let '(thr, lk, K) := t in do_unlock thr lk K }.
-        
+  (* 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.