From 0ed9c6b0d71570f9caf0d02b36bb52c1d015c90c Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 8 Apr 2026 22:04:25 +0200
Subject: [PATCH 01/10] Scoped lock specs and test proof

---
 rocq-brick-libstdcpp/proof/mutex/inc.hpp      |   6 +
 .../proof/mutex/spec/scoped_lock.v            | 147 ++++++++++++++++++
 2 files changed, 153 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/inc.hpp b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
index ccb7a7c..5f56386 100644
--- a/rocq-brick-libstdcpp/proof/mutex/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
@@ -1,3 +1,9 @@
 #include <mutex>
 
 template class std::lock_guard<std::mutex>;
+template class std::scoped_lock<std::mutex, std::mutex>;
+
+inline void foo() {
+  std::mutex m1, m2;
+  std::scoped_lock lock(m1, m2);
+}
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
new file mode 100644
index 0000000..bb9da6c
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
@@ -0,0 +1,147 @@
+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.
+
+Module scoped_lock.
+  Section with_cpp.
+    Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> list (ptr * gname * Qp * mpred) -> Rep.
+
+    #[only(type_ptr="std::scoped_lock<std::mutex, std::mutex>")] derive R.
+    #[only(cfractional,ascfractional,cfracvalid)] derive R.
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      cpp.spec
+      "std::scoped_lock<...<std::mutex, std::mutex>>::scoped_lock(std::mutex&, std::mutex&)"
+      (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
+      as ctor_spec from source with (
+        \this this
+        \arg{mp1} "" (Vptr mp1)
+        \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
+        \pre mutex.token g1 q1
+        \arg{mp2} "" (Vptr mp2)
+        \pre{g2 q2 P2} mp2 |-> mutex.R g2 q2$m P2
+        \pre mutex.token g2 q2
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)] **
+          P1 ** mutex.locked g1 thr q1 **
+          P2 ** mutex.locked g2 thr q2
+      ).
+
+      cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
+        as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{
+          mp1 mp2
+          g1 q1 P1
+          g2 q2 P2
+        }
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)]
+        \pre |> P1
+        \pre |> P2
+        \pre mutex.locked g1 thr q1
+        \pre mutex.locked g2 thr q2
+        \post
+          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
+          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+      ).
+
+      cpp.spec "foo()" as foo_spec from source with
+      (
+        \persist{thr} current_thread thr
+        \post emp
+      ).
+
+      Lemma foo_ok : verify[source] foo_spec.
+      Proof.
+        verify_spec; go.
+        iExists emp; go.
+        iExists emp; go.
+        Fail solve [ego].
+        ework.
+        ego.
+
+        (**
+        (** Weird failure! *)
+        ego.
+  match args_for <$> as_function (normalize_type ?ty0) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu ?ρ) ?es0)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f0 ?ty0 vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete ?destroyed_type (?Q Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete ?destroyed_type obj_ptr
+  (?Q Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  match args_for <$> as_function (normalize_type ?ty) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu0 ?ρ0) ?es)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f ?ty vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete0 ?destroyed_type0 (?Q0 Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete0 ?destroyed_type0 obj_ptr
+  (?Q0 Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  lock_addr
+  |-> R 1$m
+  [(?p, ?g, ?q,
+  ::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty0)) ?es0)
+  ?destroyed_type));
+  (?p0, ?g0, ?q0,
+  ::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty)) ?es)
+  ?destroyed_type0))] ∗ mutex.locked ?g thr ?q ∗ mutex.locked ?g0 thr ?q0 ∗
+  (?p
+  |-> mutex.R ?g ?q$m
+  (::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty0)) ?es0)
+  ?destroyed_type)) ∗ mutex.token ?g ?q ∗
+  ?p0
+  |-> mutex.R ?g0 ?q0$m
+  (::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty)) ?es)
+  ?destroyed_type0)) ∗ mutex.token ?g0 ?q0 -∗
+  interp source ((1 >*> FreeTemps.delete "std::mutex" m2_addr) >*>
+  FreeTemps.delete "std::mutex" m1_addr)
+  (∀ p : ptr, p |-> primR "void" 1$m Vvoid -∗ ▷ _PostPred_ p))
+        *)
+      Qed.
+    End with_threads.
+  End with_cpp.
+
+End scoped_lock.

From 4e6f40930843e9a70df0de8d335e65abe987c950 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 15 Apr 2026 19:42:55 +0200
Subject: [PATCH 02/10] scoped_lock: add learning hint

---
 .../proof/mutex/spec/scoped_lock.v            | 75 +------------------
 1 file changed, 2 insertions(+), 73 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
index bb9da6c..5f42cc3 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
@@ -19,6 +19,8 @@ Module scoped_lock.
       Context {σ : genv}.
       Context `{HAS_THREADS : !HasStdThreads Σ}.
 
+      #[global] Instance: LearnEqF1 R := ltac:(solve_learnable).
+
       cpp.spec
       "std::scoped_lock<...<std::mutex, std::mutex>>::scoped_lock(std::mutex&, std::mutex&)"
       (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
@@ -67,79 +69,6 @@ Module scoped_lock.
         verify_spec; go.
         iExists emp; go.
         iExists emp; go.
-        Fail solve [ego].
-        ework.
-        ego.
-
-        (**
-        (** Weird failure! *)
-        ego.
-  match args_for <$> as_function (normalize_type ?ty0) with
-  | Some _ =>
-  eval evaluation_order.nd (map (wp_operand ?tu ?ρ) ?es0)
-  (λ (vs : list val) (free : FreeTemps),
-  builtins.wp_builtin ?f0 ?ty0 vs
-  (λ v : val,
-  match v with
-  | Vptr obj_ptr =>
-  if bool_decide (obj_ptr = nullptr)
-  then wp_delete_null ?default_delete ?destroyed_type (?Q Vvoid free)
-  else
-  new_delete.wp_delete_dispatch.body ?default_delete ?destroyed_type obj_ptr
-  (?Q Vvoid free)
-  | _ => False
-  end))
-  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
-  end ∗
-  match args_for <$> as_function (normalize_type ?ty) with
-  | Some _ =>
-  eval evaluation_order.nd (map (wp_operand ?tu0 ?ρ0) ?es)
-  (λ (vs : list val) (free : FreeTemps),
-  builtins.wp_builtin ?f ?ty vs
-  (λ v : val,
-  match v with
-  | Vptr obj_ptr =>
-  if bool_decide (obj_ptr = nullptr)
-  then wp_delete_null ?default_delete0 ?destroyed_type0 (?Q0 Vvoid free)
-  else
-  new_delete.wp_delete_dispatch.body ?default_delete0 ?destroyed_type0 obj_ptr
-  (?Q0 Vvoid free)
-  | _ => False
-  end))
-  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
-  end ∗
-  lock_addr
-  |-> R 1$m
-  [(?p, ?g, ?q,
-  ::wpOperand
-  ?ρ
-  (Edelete false ?default_delete
-  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty0)) ?es0)
-  ?destroyed_type));
-  (?p0, ?g0, ?q0,
-  ::wpOperand
-  ?ρ0
-  (Edelete false ?default_delete0
-  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty)) ?es)
-  ?destroyed_type0))] ∗ mutex.locked ?g thr ?q ∗ mutex.locked ?g0 thr ?q0 ∗
-  (?p
-  |-> mutex.R ?g ?q$m
-  (::wpOperand
-  ?ρ
-  (Edelete false ?default_delete
-  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty0)) ?es0)
-  ?destroyed_type)) ∗ mutex.token ?g ?q ∗
-  ?p0
-  |-> mutex.R ?g0 ?q0$m
-  (::wpOperand
-  ?ρ0
-  (Edelete false ?default_delete0
-  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty)) ?es)
-  ?destroyed_type0)) ∗ mutex.token ?g0 ?q0 -∗
-  interp source ((1 >*> FreeTemps.delete "std::mutex" m2_addr) >*>
-  FreeTemps.delete "std::mutex" m1_addr)
-  (∀ p : ptr, p |-> primR "void" 1$m Vvoid -∗ ▷ _PostPred_ p))
-        *)
       Qed.
     End with_threads.
   End with_cpp.

From c87c6da966cedc1382fee8c74ca280a51368f396 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 8 Apr 2026 22:04:25 +0200
Subject: [PATCH 03/10] Scoped lock specs and test proof (TODO rename)

---
 .../proof/mutex/scoped_lock_spec.v            | 149 ++++++++++++++++++
 1 file changed, 149 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v b/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v
new file mode 100644
index 0000000..6be2e73
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/scoped_lock_spec.v
@@ -0,0 +1,149 @@
+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.
+
+Module scoped_lock.
+  Section with_cpp.
+    Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> list (ptr * gname * Qp * mpred) -> Rep.
+
+    #[only(type_ptr="std::scoped_lock<std::mutex, std::mutex>")] derive R.
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      cpp.spec
+      "std::scoped_lock<...<std::mutex, std::mutex>>::scoped_lock(std::mutex&, std::mutex&)"
+      (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
+      as ctor_spec from source with (
+        \this this
+        \arg{mp1} "" (Vptr mp1)
+        \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
+        \pre mutex.token g1 q1
+        \arg{mp2} "" (Vptr mp2)
+        \pre{g2 q2 P2} mp2 |-> mutex.R g2 q2$m P2
+        \pre mutex.token g2 q2
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)] **
+          P1 ** mutex.locked g1 thr q1 **
+          P2 ** mutex.locked g2 thr q2
+      ).
+
+      cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
+        as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{
+          mp1 mp2
+          g1 q1 P1
+          g2 q2 P2
+        }
+          this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)]
+        \pre |> P1
+        \pre |> P2
+        \pre mutex.locked g1 thr q1
+        \pre mutex.locked g2 thr q2
+        \post
+          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
+          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+      ).
+
+      cpp.spec "foo()" as foo_spec from source with
+      (
+        \persist{thr} current_thread thr
+        \post emp
+      ).
+
+      (* #[only(cfracsplittable)] derive R. *)
+      #[only(cfractional,ascfractional,cfracvalid)] derive R.
+
+      Lemma foo_ok : verify[source] foo_spec.
+      Proof.
+        verify_spec; go.
+        iExists emp; go.
+        iExists emp; go.
+        Fail solve [ego].
+        ework.
+        ego.
+
+        (**
+        (** Weird failure! *)
+        ego.
+  match args_for <$> as_function (normalize_type ?ty0) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu ?ρ) ?es0)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f0 ?ty0 vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete ?destroyed_type (?Q Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete ?destroyed_type obj_ptr
+  (?Q Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  match args_for <$> as_function (normalize_type ?ty) with
+  | Some _ =>
+  eval evaluation_order.nd (map (wp_operand ?tu0 ?ρ0) ?es)
+  (λ (vs : list val) (free : FreeTemps),
+  builtins.wp_builtin ?f ?ty vs
+  (λ v : val,
+  match v with
+  | Vptr obj_ptr =>
+  if bool_decide (obj_ptr = nullptr)
+  then wp_delete_null ?default_delete0 ?destroyed_type0 (?Q0 Vvoid free)
+  else
+  new_delete.wp_delete_dispatch.body ?default_delete0 ?destroyed_type0 obj_ptr
+  (?Q0 Vvoid free)
+  | _ => False
+  end))
+  | None => errors.Errors.ERROR.body "builtin does not have function type"%bs
+  end ∗
+  lock_addr
+  |-> R 1$m
+  [(?p, ?g, ?q,
+  ::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty0)) ?es0)
+  ?destroyed_type));
+  (?p0, ?g0, ?q0,
+  ::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun (Tptr [...])) (Eglobal (Nglobal [...]) ?ty)) ?es)
+  ?destroyed_type0))] ∗ mutex.locked ?g thr ?q ∗ mutex.locked ?g0 thr ?q0 ∗
+  (?p
+  |-> mutex.R ?g ?q$m
+  (::wpOperand
+  ?ρ
+  (Edelete false ?default_delete
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty0)) ?es0)
+  ?destroyed_type)) ∗ mutex.token ?g ?q ∗
+  ?p0
+  |-> mutex.R ?g0 ?q0$m
+  (::wpOperand
+  ?ρ0
+  (Edelete false ?default_delete0
+  (Ecall (Ecast (Cbuiltin2fun ([...])) (Eglobal ([...]) ?ty)) ?es)
+  ?destroyed_type0)) ∗ mutex.token ?g0 ?q0 -∗
+  interp source ((1 >*> FreeTemps.delete "std::mutex" m2_addr) >*>
+  FreeTemps.delete "std::mutex" m1_addr)
+  (∀ p : ptr, p |-> primR "void" 1$m Vvoid -∗ ▷ _PostPred_ p))
+        *)
+      Qed.
+    End with_threads.
+  End with_cpp.
+
+End scoped_lock.

From edcc7b76e774f63e0f8f5f63fe9341424937a585 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 15 Apr 2026 19:07:21 +0200
Subject: [PATCH 04/10] unique_lock spec

---
 rocq-brick-libstdcpp/proof/mutex/inc.hpp      |   1 +
 .../proof/mutex/spec/unique_lock.v            | 134 ++++++++++++++++++
 2 files changed, 135 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v

diff --git a/rocq-brick-libstdcpp/proof/mutex/inc.hpp b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
index 5f56386..0bdd0c2 100644
--- a/rocq-brick-libstdcpp/proof/mutex/inc.hpp
+++ b/rocq-brick-libstdcpp/proof/mutex/inc.hpp
@@ -1,6 +1,7 @@
 #include <mutex>
 
 template class std::lock_guard<std::mutex>;
+template class std::unique_lock<std::mutex>;
 template class std::scoped_lock<std::mutex, std::mutex>;
 
 inline void foo() {
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
new file mode 100644
index 0000000..1d975af
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -0,0 +1,134 @@
+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.
+
+Module unique_lock.
+Section with_cpp.
+  Context `{Σ : cpp_logic}.
+
+    (* Parameter gname : Set. *)
+    Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
+      cQp.t -> option (ptr * gname * Qp * mpred * bool) -> Rep.
+
+    (* #[only(type_ptr="std::unique_lock<std::mutex>")] derive R. *)
+
+    Section with_threads.
+      Context {σ : genv}.
+      Context `{HAS_THREADS : !HasStdThreads Σ}.
+
+      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 from source with (
+        \this this
+        \arg{mp} "" (Vptr mp)
+        \pre{g q P} mp |-> mutex.R g q$m P
+        \pre mutex.token g q
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m (Some (mp, g, q, P, true)) **
+          P ** mutex.locked g thr q
+      ).
+
+      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{g q P} mp |-> mutex.R g q$m P
+        \arg{def_p} "" (Vptr def_p)
+        \post this |-> R 1$m (Some (mp, g, q, P, false))
+      ).
+
+      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
+      ).
+
+      cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{om} this |-> R 1$m om
+        \pre
+          match om with
+          | Some (mp, g, q, P, true) => mutex.locked g thr q ** ▷P
+          | _ => emp
+          end
+        \post
+          match om with
+          | Some (mp, g, q, P, true) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (mp, g, q, P, false) => mp |-> mutex.R g q$m P
+          | None => emp
+          end
+        ).
+
+      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
+          match om1 with
+          | Some (mp, g, q, P, true) => mutex.locked g thr q ** ▷P
+          | _ => emp
+          end
+        \post
+          this |-> R 1$m om2 **
+          other |-> R 1$m None **
+          match om1 with
+          | Some (mp, g, q, P, true) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (mp, g, q, P, false) => mp |-> mutex.R g q$m P
+          | None => emp
+          end
+        ).
+
+      Definition owned (om : option (ptr * gname * Qp * mpred * bool)) : bool :=
+        match om with
+        | Some (mp, g, q, P, own) => own
+        | None => false
+        end.
+
+      Definition mutex (om : option (ptr * gname * Qp * mpred * bool)) : ptr :=
+        match om with
+        | Some (mp, g, q, P, own) => mp
+        | None => nullptr
+        end.
+
+      cpp.spec "std::unique_lock<std::mutex>::owns_lock() const" as owns_lock_spec from source with (
+        \this this
+        \prepost{om q} this |-> R q om
+        \post [Vbool (owned om)] emp).
+
+      cpp.spec "std::unique_lock<std::mutex>::operator bool() const" as operator_bool_spec from source with (
+        \this this
+        \prepost{om q} this |-> R q om
+        \post [Vbool (owned om)] emp).
+
+      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{mp g q P} this |-> R 1$m (Some (mp, g, q, P, false))
+        \pre mutex.token g q
+        \persist{thr} current_thread thr
+        \post
+          this |-> R 1$m (Some (mp, g, q, P, true)) **
+          P ** mutex.locked g thr q).
+    End with_threads.
+End with_cpp.
+End unique_lock.

From 9ca4e4805e85cba2753d669ea62fe5f3213ff4a7 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 15 Apr 2026 19:33:37 +0200
Subject: [PATCH 05/10] Revisions

---
 .../proof/mutex/spec/unique_lock.v            | 93 ++++++++++++++-----
 1 file changed, 70 insertions(+), 23 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index 1d975af..c803d95 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -9,8 +9,23 @@ Section with_cpp.
   Context `{Σ : cpp_logic}.
 
     (* Parameter gname : Set. *)
+    (* 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 {HAS_THREADS : HasStdThreads Σ} {σ : genv},
-      cQp.t -> option (ptr * gname * Qp * mpred * bool) -> Rep.
+      cQp.t -> option (bool * (ptr * gname * Qp * mpred)) -> Rep.
+
+    Definition owned (om : option (bool * (ptr * gname * Qp * mpred))) : bool :=
+      match om with
+      | Some (own, _) => own
+      | None => false
+      end.
+
+    Definition mutex (om : option (bool * (ptr * gname * Qp * mpred))) : ptr :=
+      match om with
+      | Some (_, (mp, g, q, P)) => mp
+      | None => nullptr
+      end.
 
     (* #[only(type_ptr="std::unique_lock<std::mutex>")] derive R. *)
 
@@ -18,12 +33,42 @@ Section with_cpp.
       Context {σ : genv}.
       Context `{HAS_THREADS : !HasStdThreads Σ}.
 
+      (* TODO maybe a class / interface Lockable that exposes do_lock, do_unlock
+         and the rep predicate R, formalizing the C++ lockable concept
+         <https://en.cppreference.com/w/cpp/named_req/Lockable.html>.
+
+         Instantiate with mutex, recursive_mutex, maybe in different styles (AC
+         and invariant styles).
+      *)
+      Definition do_unlock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
+        match lk with
+        | (mp, g, q, P) =>
+          mutex.locked g thr q ** ▷P ** |> (mutex.token g q -* Q)
+        end.
+
+      Definition do_lock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
+        match lk with
+        | (mp, g, q, P) =>
+          mutex.token g q ** |> (mutex.locked g thr q ** ▷P -* Q)
+        end.
+
       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{g q P} mp |-> mutex.R g q$m P
+        \persist{thr} current_thread thr
+        \pre{K} do_lock thr (mp, g, q, P) K
+        \post
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
+          K
+      ).
+
       cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::mutex&)" as mutex_ctor_spec from source with (
         \this this
         \arg{mp} "" (Vptr mp)
@@ -31,7 +76,7 @@ Section with_cpp.
         \pre mutex.token g q
         \persist{thr} current_thread thr
         \post
-          this |-> R 1$m (Some (mp, g, q, P, true)) **
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
           P ** mutex.locked g thr q
       ).
 
@@ -40,7 +85,7 @@ Section with_cpp.
         \arg{mp} "" (Vptr mp)
         \pre{g q P} mp |-> mutex.R g q$m P
         \arg{def_p} "" (Vptr def_p)
-        \post this |-> R 1$m (Some (mp, g, q, P, false))
+        \post this |-> R 1$m (Some (false, (mp, g, q, P)))
       ).
 
       cpp.spec "std::unique_lock<std::mutex>::unique_lock(std::unique_lock<std::mutex> &&)" as move_ctor_spec from source with (
@@ -52,19 +97,33 @@ Section with_cpp.
           other |-> R 1$m None
       ).
 
+      cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec_alt from source with (
+        \this this
+        \persist{thr} current_thread thr
+        \pre{om} this |-> R 1$m om
+        \pre{K}
+          match om with
+          | Some (true, mm) => do_unlock thr mm K
+          | Some (false, (mp, g, q, P)) =>
+            |> (mp |-> mutex.R g q$m P -* K)
+          | _ => K
+          end
+        \post K
+        ).
+
       cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec from source with (
         \this this
         \persist{thr} current_thread thr
         \pre{om} this |-> R 1$m om
         \pre
           match om with
-          | Some (mp, g, q, P, true) => mutex.locked g thr q ** ▷P
+          | Some (true, (mp, g, q, P)) => mutex.locked g thr q ** ▷P
           | _ => emp
           end
         \post
           match om with
-          | Some (mp, g, q, P, true) => mp |-> mutex.R g q$m P ** mutex.token g q
-          | Some (mp, g, q, P, false) => mp |-> mutex.R g q$m P
+          | Some (true, (mp, g, q, P)) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (false, (mp, g, q, P)) => mp |-> mutex.R g q$m P
           | None => emp
           end
         ).
@@ -77,31 +136,19 @@ Section with_cpp.
         \persist{thr} current_thread thr
         \pre
           match om1 with
-          | Some (mp, g, q, P, true) => mutex.locked g thr q ** ▷P
+          | Some (true, (mp, g, q, P)) => mutex.locked g thr q ** ▷P
           | _ => emp
           end
         \post
           this |-> R 1$m om2 **
           other |-> R 1$m None **
           match om1 with
-          | Some (mp, g, q, P, true) => mp |-> mutex.R g q$m P ** mutex.token g q
-          | Some (mp, g, q, P, false) => mp |-> mutex.R g q$m P
+          | Some (true, (mp, g, q, P)) => mp |-> mutex.R g q$m P ** mutex.token g q
+          | Some (false, (mp, g, q, P)) => mp |-> mutex.R g q$m P
           | None => emp
           end
         ).
 
-      Definition owned (om : option (ptr * gname * Qp * mpred * bool)) : bool :=
-        match om with
-        | Some (mp, g, q, P, own) => own
-        | None => false
-        end.
-
-      Definition mutex (om : option (ptr * gname * Qp * mpred * bool)) : ptr :=
-        match om with
-        | Some (mp, g, q, P, own) => mp
-        | None => nullptr
-        end.
-
       cpp.spec "std::unique_lock<std::mutex>::owns_lock() const" as owns_lock_spec from source with (
         \this this
         \prepost{om q} this |-> R q om
@@ -123,11 +170,11 @@ Section with_cpp.
       - 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{mp g q P} this |-> R 1$m (Some (mp, g, q, P, false))
+        \pre{mp g q P} this |-> R 1$m (Some (false, (mp, g, q, P)))
         \pre mutex.token g q
         \persist{thr} current_thread thr
         \post
-          this |-> R 1$m (Some (mp, g, q, P, true)) **
+          this |-> R 1$m (Some (true, (mp, g, q, P))) **
           P ** mutex.locked g thr q).
     End with_threads.
 End with_cpp.

From 57496c7b1308e585a95c0de1d429b189129eda9f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 22 Apr 2026 18:23:22 +0200
Subject: [PATCH 06/10] Reduce duplication between specs

---
 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index c803d95..1bd01c8 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -149,15 +149,16 @@ Section with_cpp.
           end
         ).
 
-      cpp.spec "std::unique_lock<std::mutex>::owns_lock() const" as owns_lock_spec from source with (
+      Notation owns_lock_spec_body := (
         \this this
         \prepost{om q} this |-> R q om
-        \post [Vbool (owned om)] emp).
+        \post [Vbool (owned om)] emp) (only parsing).
 
-      cpp.spec "std::unique_lock<std::mutex>::operator bool() const" as operator_bool_spec from source with (
-        \this this
-        \prepost{om q} this |-> R q om
-        \post [Vbool (owned om)] emp).
+      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

From a0c74db3f0fe76b5d3379090ee5290b78aa547ca Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 22 Apr 2026 18:25:16 +0200
Subject: [PATCH 07/10] Add TODO on refactoring

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

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index 1bd01c8..efd17e7 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -40,6 +40,18 @@ Section with_cpp.
          Instantiate with mutex, recursive_mutex, maybe in different styles (AC
          and invariant styles).
       *)
+
+      (*
+      TODO: could we write something like this?
+      Definition do_unlock_spec_body (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : WpSpec_cpp :=
+        match lk with
+        | (mp, g, q, P) =>
+        \pre mutex.locked g thr q
+        \pre ▷P
+        \post mutex.token g q
+        end.
+        *)
+
       Definition do_unlock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
         match lk with
         | (mp, g, q, P) =>

From f103fc83391ab374efb60bdbda6808eb5c6707f0 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 20 Apr 2026 03:47:13 +0000
Subject: [PATCH 08/10] replace |> with \triangleright

---
 rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index efd17e7..f53a8e6 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -55,13 +55,13 @@ Section with_cpp.
       Definition do_unlock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
         match lk with
         | (mp, g, q, P) =>
-          mutex.locked g thr q ** ▷P ** |> (mutex.token g q -* Q)
+          mutex.locked g thr q ** ▷P ** ▷(mutex.token g q -* Q)
         end.
 
       Definition do_lock (thr : thread_idT) (lk : ptr * gname * Qp * mpred) (Q : mpred) : mpred :=
         match lk with
         | (mp, g, q, P) =>
-          mutex.token g q ** |> (mutex.locked g thr q ** ▷P -* Q)
+          mutex.token g q ** ▷(mutex.locked g thr q ** ▷P -* Q)
         end.
 
       cpp.spec "std::unique_lock<std::mutex>::unique_lock()"
@@ -117,7 +117,7 @@ Section with_cpp.
           match om with
           | Some (true, mm) => do_unlock thr mm K
           | Some (false, (mp, g, q, P)) =>
-            |> (mp |-> mutex.R g q$m P -* K)
+            ▷ (mp |-> mutex.R g q$m P -* K)
           | _ => K
           end
         \post K

From 8443d0ace4e7d284d40aec386e93e131d66e6de6 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 20 Apr 2026 03:55:31 +0000
Subject: [PATCH 09/10] add comments

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

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index f53a8e6..3b74521 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -109,6 +109,8 @@ Section with_cpp.
           other |-> R 1$m None
       ).
 
+      (* spec for dtor written with do_unlock; dtor_spec below should be
+      equivalent to dtor_spec_alt. *)
       cpp.spec "std::unique_lock<std::mutex>::~unique_lock()" as dtor_spec_alt from source with (
         \this this
         \persist{thr} current_thread thr

From d7e2a22f2f8bee440ae2323ca57b3adc82c600e7 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 20 Apr 2026 04:16:51 +0000
Subject: [PATCH 10/10] refactor post condition of dtor and move operator in
 unique_lock

---
 .../proof/mutex/spec/unique_lock.v            | 36 ++++++++++++++-----
 1 file changed, 28 insertions(+), 8 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
index 3b74521..7c86a6f 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v
@@ -109,19 +109,23 @@ Section with_cpp.
           other |-> R 1$m None
       ).
 
-      (* spec for dtor written with do_unlock; dtor_spec below should be
-      equivalent to dtor_spec_alt. *)
+      (* unlock the associated mutex, if any  *)
+      Definition ensure_unlock (thr : thread_idT) (om : option (bool * (ptr * gname * Qp * mpred))) (Q : mpred) : mpred :=
+        match om with
+        | Some (true, mm) => do_unlock thr mm Q
+        | Some (false, (mp, g, q, P)) =>
+          ▷ (mp |-> mutex.R g q$m P -* Q)
+        | _ => (* TODO should this be [bi_later Q]? *) Q
+        end.
+
+      (* 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
         \persist{thr} current_thread thr
         \pre{om} this |-> R 1$m om
         \pre{K}
-          match om with
-          | Some (true, mm) => do_unlock thr mm K
-          | Some (false, (mp, g, q, P)) =>
-            ▷ (mp |-> mutex.R g q$m P -* K)
-          | _ => K
-          end
+          ensure_unlock thr om K
         \post K
         ).
 
@@ -142,6 +146,22 @@ Section with_cpp.
           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
+        \persist{thr} current_thread thr
+        \pre{K}
+          ensure_unlock thr 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)