From 8129f5e6c193476754b37210cd34a3189592a9e5 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 31 Aug 2026 18:13:50 +0000
Subject: [PATCH 01/16] [mutex.v]: change token to user; comment out
 with_RepFor section

---
 rocq-brick-libstdcpp/proof/mutex/spec/mutex.v | 59 ++++++++++---------
 1 file changed, 31 insertions(+), 28 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index f013828f..c2254964 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -12,8 +12,10 @@ Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 Require Import skylabs.brick.libstdcpp.mutex.requirements.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 Import linearity.
+Import lock_ghost.
 
 (* TODO UPSTREAM. *)
 #[global] Instance SplitRecord_prod A B : SplitRecord (@prod A B) := {}.
@@ -28,21 +30,14 @@ Section with_cpp.
   #[global] Declare Instance R_learnable : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
       Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R).
 
-  (** Owning [mutex_token γ 1] proves that the mutex is not locked, and
-  therefore can be safely destroyed: the standard specifies that calling
-  [std::mutex::~mutex()] while holding the lock results in undefined behavior.
-  *)
-  Parameter token : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> Qp -> mpred.
-  #[only(fractional,fracvalid,asfractional,timeless)] derive token.
-
-  Section with_RepFor.
+  (* Section with_RepFor.
     Import rep.RepFor.
     Import RepScheme.
 
     #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
       rep.RepFor.C "std::mutex" [ArgType.Constant _; ArgType.CFrac; ArgType.Constant _]
-        (funI γ q P => R γ q P ∗ pureR (token γ q)) := {}.
-  End with_RepFor.
+        (funI γ q P => R γ q P) := {}.
+  End with_RepFor. *)
 
 
   (** A resource enforcing that the thread calling unlock must be the same thread
@@ -65,27 +60,36 @@ Section with_cpp.
     >>
    *)
   Parameter locked : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
-      gname -> thread_idT -> Qp -> mpred.
+      gname -> thread_idT -> mpred.
   #[only(timeless)] derive locked.
 
-  (** locked takes a [Qp] but _cannot_ be split. *)
   #[only(exclusive)] derive locked.
 
+  Context `{!lockG Σ}.
+
+  Abbreviation used_threads γ s :=
+    (lock_ghost.used_threads γ s).
+
+  Abbreviation users γ ths :=
+    (lock_ghost.users γ ths).
+
+  Abbreviation user γ th := (users γ {[ th ]}).
+
   Context `{MOD : source ⊧ σ}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
-  #[global] Instance locked_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin) locked).
+  #[global] Instance locked_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_hints.fin) locked).
   Proof. solve_learnable. Qed.
 
 
   cpp.spec "std::mutex::mutex()" as ctor_spec with (
     \this this
     \pre{P} ▷P
-    \post Exists g, this |-> R g 1$m P ** token g 1).
+    \post Exists g, this |-> R g 1$m P ** used_threads g ∅).
 
   cpp.spec "std::mutex::~mutex()" as dtor_spec with (
     \this this
-    \pre{g P} this |-> R g 1$m P ** token g 1
+    \pre{g P} this |-> R g 1$m P ** used_threads g ∅
     \post P).
 
   (* "Inline" version of these specs. *)
@@ -93,41 +97,41 @@ Section with_cpp.
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{thr} current_thread thr
-    \pre{q'} token g q'
-    \post P ** locked g thr q').
+    \pre user g thr
+    \post P ** locked g thr).
 
   Definition do_lock (lk : gname * mpred) (K: mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    ∃ q thr, current_thread thr ∗ token g q ∗
+    ∃ thr, current_thread thr ∗ user g thr ∗
     (* TODO readd *)
     (* ▷ *)
-    (locked g thr q ** P -* K).
+    (locked g thr ** P -* K).
   #[global] Arguments do_lock /.
 
   cpp.spec "std::mutex::unlock()" as unlock_spec_alt with (
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{thr} current_thread thr
-    \pre{q'} locked g thr q'
+    \pre locked g thr
     \pre ▷P
-    \post token g q').
+    \post user g thr).
 
   Definition do_unlock (lk : gname * mpred) (Q : mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    Exists q thr, current_thread thr ** locked g thr q ** ▷P **
+    Exists thr, current_thread thr ** locked g thr ** ▷P **
     (* TODO readd *)
     (* ▷ *)
-    (token g q -* Q).
+    (user g thr -* Q).
   #[global] Arguments do_unlock /.
 
   cpp.spec "std::mutex::try_lock()" as try_lock_spec_alt with (
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{th} current_thread th
-    \pre{q'} token g q'
-    \post{b}[Vbool b] if b then P ** locked g th q' else token g q').
+    \pre user g th
+    \post{b}[Vbool b] if b then P ** locked g th else user g th).
 
   (* Obtain same specs from (Basic)Lockable. *)
   (** <<std::mutex>> implements [BasicLockable] *)
@@ -146,9 +150,9 @@ Section with_cpp.
   Definition do_try_lock (lk : gname * mpred) (Q : bool -> mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    ∃ q thr, current_thread thr ∗ token g q ∗
+    ∃ thr, current_thread thr ∗ user g thr ∗
     ∀ b : bool,
-    (if b then P ** locked g thr q else token g q) -∗ Q b.
+    (if b then P ** locked g thr else user g thr) -∗ Q b.
   #[global] Arguments do_try_lock /.
 
   #[global,program] Instance mutex_lockable : Lockable (T:=T) "std::mutex" (λ q γP, R γP.1 q γP.2) :=
@@ -173,4 +177,3 @@ Section with_cpp.
   Qed.
 End with_cpp.
 End mutex.
-

From c14bc58dc9694b30bcaa51951b497b74b10a77ce Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 31 Aug 2026 18:40:05 +0000
Subject: [PATCH 02/16] replace appearance of mutex.token to user

---
 .../proof/mutex/proof/lock_guard.v            |  5 ++---
 .../proof/mutex/proof/unique_lock.v           |  5 +++--
 .../proof/mutex/spec/lock_guard.v             | 11 +++++-----
 .../proof/mutex/spec/scoped_lock.v            | 20 ++++++++++---------
 4 files changed, 22 insertions(+), 19 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v b/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v
index 74de4d0d..a828faae 100644
--- a/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v
+++ b/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v
@@ -3,12 +3,14 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Import skylabs.brick.libstdcpp.mutex.spec.lock_guard.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 Import linearity.
 
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!lock_ghost.lockG Σ}.
 
   Import lock_guard.
 
@@ -17,9 +19,6 @@ Section with_cpp.
       Cbn (Learn (learn_eq ==> learn_eq ==> learn_eq ==> fin_at) mutex.R).
   Proof. solve_learnable. Qed.
 
-  #[global] Instance UNSAFE_token_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_hints.fin) mutex.token).
-  Proof. solve_learnable. Qed.
-
   #[local] Hint Resolve fractional.UNSAFE_read_prim_learn : sl_opacity.
 
   Lemma ctor_ok : verify[source] ctor_spec.
diff --git a/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v b/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
index 45ff3244..dc8a20d7 100644
--- a/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
@@ -6,11 +6,13 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.prelude.
 Require Import skylabs.brick.libstdcpp.mutex.spec.unique_lock.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Import skylabs.brick.libstdcpp.lib.tactics.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 NES.Begin unique_lock.
   Section with_cpp.
     Context `{Σ : cpp_logic} {σ : genv}.
     Context `{HAS_THREADS : !HasStdThreads Σ}.
+    Context `{!lock_ghost.lockG Σ}.
 
     Import R_unfold.
 
@@ -43,10 +45,9 @@ NES.Begin unique_lock.
         "std::unique_lock<std::mutex>::unique_lock(std::mutex&)".
     Proof.
       verify_spec; go.
-      iExists K.
+      iExists K, q.
       (* Time Succeed solve [setoid_rewrite cQp.scale_mut; setoid_rewrite (right_id_L 1%Qp Qp.mul); ego with br_erefl]. *)
 
-      iExists _, q.
       rewrite cQp.scale_mut (right_id_L 1%Qp Qp.mul).
       go with br_erefl.
     Qed.
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v b/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
index 392b5445..c95924eb 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
@@ -3,6 +3,7 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 
 Import linearity.
@@ -47,6 +48,7 @@ Module lock_guard.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!lock_ghost.lockG Σ}.
 
   #[global] Instance R_learn :
     Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) lock_guard.R) :=
@@ -87,20 +89,20 @@ Section with_cpp.
     \arg{mp} "m" (Vptr mp)
     \persist{thr} current_thread thr
     \pre{g q P} mp |-> mutex.R g q$m P
-    \pre mutex.token g q
+    \pre lock_ghost.user g thr
     \post
       this |-> R (mp, g, q) 1$m P **
-      P ** mutex.locked g thr q
+      P ** mutex.locked g thr
     ).
 
   cpp.spec "std::lock_guard<std::mutex>::~lock_guard()" as dtor_spec from source with (
     \this this
     \pre{mp g q P} this |-> R (mp, g, q) 1$m P
     \persist{thr} current_thread thr
-    \pre mutex.locked g thr q
+    \pre mutex.locked g thr
     \pre ▷P
     \post
-      mutex.token g q **
+      lock_ghost.user g thr **
       mp |-> mutex.R g q$m P
   ).
 
@@ -124,4 +126,3 @@ Section with_cpp.
 
 End with_cpp.
 End lock_guard.
-
diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
index 7a734e9f..b8811f8e 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
@@ -3,6 +3,7 @@ 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.lib.lock_ghost.
 
 Module scoped_lock.
   Section with_cpp.
@@ -17,6 +18,7 @@ Module scoped_lock.
     Section with_threads.
       Context {σ : genv}.
       Context `{HAS_THREADS : !HasStdThreads Σ}.
+      Context `{!lock_ghost.lockG Σ}.
 
       #[global] Instance: LearnEqF1 R := ltac:(solve_learnable).
 
@@ -25,17 +27,17 @@ Module scoped_lock.
       (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
       as ctor_spec from source with (
         \this this
+        \persist{thr} current_thread thr
         \arg{mp1} "" (Vptr mp1)
         \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
-        \pre mutex.token g1 q1
+        \pre lock_ghost.user g1 thr
         \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
+        \pre lock_ghost.user g2 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
+          P1 ** mutex.locked g1 thr **
+          P2 ** mutex.locked g2 thr
       ).
 
       cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
@@ -50,11 +52,11 @@ Module scoped_lock.
           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
+        \pre mutex.locked g1 thr
+        \pre mutex.locked g2 thr
         \post
-          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
-          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+          mp1 |-> mutex.R g1 q1$m P1 ** lock_ghost.user g1 thr **
+          mp2 |-> mutex.R g2 q2$m P2 ** lock_ghost.user g2 thr
       ).
     End with_threads.
   End with_cpp.

From 2588395da0816a93b4fcd6e207f03f1894adb01d Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Mon, 31 Aug 2026 23:36:44 +0000
Subject: [PATCH 03/16] check in layout of a custom mutex proof

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 79 +++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
new file mode 100644
index 00000000..70f0b4b1
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -0,0 +1,79 @@
+(** Provisional *)
+
+Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
+Require Import skylabs.brick.libstdcpp.test.mutex.custom_mutex_hpp.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
+Import lock_ghost.
+Require Import skylabs.brick.libstdcpp.atomic.spec.
+
+Module custom_mutex.
+
+  Abbreviation N := "MyMutex"%cpp_name.
+
+
+  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t -> option thread_idT -> Rep.
+
+  Parameter exclusive_token : ∀ `{Σ : cpp_logic}, iprop.gname -> mpred.
+  Parameter owner_token_auth : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
+  Parameter owner_token_frac : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
+
+  Record gname : Set := MkGname
+  { user_gname : iprop.gname
+  ; cinv_gname : iprop.gname
+  ; phys_state_gname : iprop.gname
+  }.
+
+  Definition lock_namespace : namespace := nroot .@@ "MyMutex".
+
+  Definition locked `{Σ : cpp_logic} `{!lockG Σ} (g: gname) (th : thread_idT) : mpred 
+    := owner_token_auth g.(phys_state_gname) (Some th) ** user g.(user_gname) th.
+
+  (* Definition IR `{Σ : cpp_logic, σ : genv, !HasStdThreads Σ, !recursive_mutex.lockedG Σ} (γ : gname) (q : cQp.t) : mpred :=
+    ∃ x, recursive_mutex.owned_count_id_auth γ.(rec_gname) x. *)
+(*
+    Definition rawR `{Σ : cpp_logic, σ : genv} (owner : option thread_idT) (count : nat) : Rep :=
+      structR "std::recursive_mutex" 1$m **
+      _field "MyRecursiveMutex::m_count" |-> ulonglongR 1$m count. *)
+
+  Section with_Σ.
+    Context `{Σ : cpp_logic, σ : genv, !HasStdThreads Σ, !lockG Σ}.
+
+    Definition mutex_content (γ : gname) : Rep :=
+      ∃ o_owner lockedb,
+         _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m lockedb **
+         _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m o_owner.
+
+    Definition mutex_inv (this : ptr) (γ : gname) (P : mpred) : mpred :=
+      ∃ o_owner, this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m o_owner **
+      owner_token_frac γ.(phys_state_gname) o_owner **
+      ∃ b : bool,
+      this ,, _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m b **
+      if b then
+        ∃ owner, [| Some owner = o_owner |]
+      else
+        owner_token_auth γ.(phys_state_gname) o_owner **
+        P.
+
+    Definition IR (γ : gname) (q : cQp.t) (P : mpred) : Rep :=
+      structR N q$m **
+      as_Rep (fun this =>
+        cinv lock_namespace γ.(cinv_gname) (mutex_inv this γ P) **
+        cinv_own γ.(cinv_gname) q
+      ).
+
+    Section proof.
+
+      Context `{MOD : source ⊧ σ}.
+      Context {HAS_THREADS : HasStdThreads Σ}.
+
+      cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
+        \this this
+        \pre{P} ▷P
+        \post Exists g, this |-> IR g 1$m P ** used_threads g.(user_gname) ∅).
+
+    End proof.
+
+  End with_Σ.
+
+End custom_mutex.

From 441bd7d5d4bca15e154550fcb7767bb73ed09a29 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Tue, 1 Sep 2026 04:46:57 +0000
Subject: [PATCH 04/16] [custom_mutex_hpp_proof.v] add do_lock lemma statement

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 60 ++++++++++++++-----
 1 file changed, 46 insertions(+), 14 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 70f0b4b1..2750bcfc 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -12,7 +12,9 @@ Module custom_mutex.
   Abbreviation N := "MyMutex"%cpp_name.
 
 
-  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t -> option thread_idT -> Rep.
+  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t -> 
+    (* None if value is thread::id(), Some otherwise *) 
+    option thread_idT -> Rep.
 
   Parameter exclusive_token : ∀ `{Σ : cpp_logic}, iprop.gname -> mpred.
   Parameter owner_token_auth : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
@@ -45,15 +47,21 @@ Module custom_mutex.
          _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m o_owner.
 
     Definition mutex_inv (this : ptr) (γ : gname) (P : mpred) : mpred :=
-      ∃ o_owner, this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m o_owner **
+      ∃ o_owner,
       owner_token_frac γ.(phys_state_gname) o_owner **
       ∃ b : bool,
       this ,, _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m b **
       if b then
-        ∃ owner, [| Some owner = o_owner |]
+        emp
       else
         owner_token_auth γ.(phys_state_gname) o_owner **
-        P.
+        P **
+        (** m_owner does not concern do_lock() and do_unlock(), the actual
+          implementation of mutex, and does not always equal o_owner.
+          It is just a resource that one can get from the invariant. *)
+        ∃ m_owner : option thread_idT,
+        this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m m_owner
+    .
 
     Definition IR (γ : gname) (q : cQp.t) (P : mpred) : Rep :=
       structR N q$m **
@@ -62,18 +70,42 @@ Module custom_mutex.
         cinv_own γ.(cinv_gname) q
       ).
 
-    Section proof.
 
-      Context `{MOD : source ⊧ σ}.
-      Context {HAS_THREADS : HasStdThreads Σ}.
 
-      cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
-        \this this
-        \pre{P} ▷P
-        \post Exists g, this |-> IR g 1$m P ** used_threads g.(user_gname) ∅).
-
-    End proof.
+    Context `{MOD : source ⊧ σ}.
+    Context {HAS_THREADS : HasStdThreads Σ}.
+
+    cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
+      \this this
+      \pre{P} ▷P
+      \post Exists g, this |-> IR g 1$m P ** used_threads g.(user_gname) ∅).
+
+    cpp.spec "MyMutex::~MyMutex()" as dtor_spec with (
+      \this this
+      \pre{g P} this |-> IR g 1$m P ** used_threads g.(user_gname) ∅
+      \post P).
+
+    cpp.spec "MyMutex::do_lock()" as lock_spec with (
+      \this this
+      \prepost{q P g} this |-> IR g q P
+      \persist{thr} current_thread thr
+      \pre user g.(user_gname) thr
+      \post ▷ P ** locked g thr).
+    
+    cpp.spec "MyMutex::do_unlock()" as unlock_spec with (
+      \this this
+      \prepost{q P g} this |-> IR g q P
+      \persist{thr} current_thread thr
+      \pre locked g thr
+      \pre ▷P
+      \post user g.(user_gname) thr).
+
+    (* Axiom *)
+    cpp.spec "std::this_thread::yield()" as yield_spec with (
+      \post emp).
+    
+    Import std.atomic.
+    Fail Lemma test_do_lock_ok : verify[source] "MyMutex::do_lock()".
 
   End with_Σ.
-
 End custom_mutex.

From 3120853c16832af0f8224256b742a0d2af99c185 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 11:58:22 +0200
Subject: [PATCH 05/16] Tweak spec and client proof

---
 rocq-brick-libstdcpp/proof/mutex/spec/mutex.v    | 6 +++---
 rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
index c2254964..1bea8673 100644
--- a/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+++ b/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
@@ -13,9 +13,9 @@ Require Export skylabs.brick.libstdcpp.runtime.pred.
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 Require Import skylabs.brick.libstdcpp.mutex.requirements.
 Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
+Export skylabs.brick.libstdcpp.lib.lock_ghost(lockG).
 
 Import linearity.
-Import lock_ghost.
 
 (* TODO UPSTREAM. *)
 #[global] Instance SplitRecord_prod A B : SplitRecord (@prod A B) := {}.
@@ -30,14 +30,14 @@ Section with_cpp.
   #[global] Declare Instance R_learnable : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
       Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R).
 
-  (* Section with_RepFor.
+  Section with_RepFor.
     Import rep.RepFor.
     Import RepScheme.
 
     #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
       rep.RepFor.C "std::mutex" [ArgType.Constant _; ArgType.CFrac; ArgType.Constant _]
         (funI γ q P => R γ q P) := {}.
-  End with_RepFor. *)
+  End with_RepFor.
 
 
   (** A resource enforcing that the thread calling unlock must be the same thread
diff --git a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
index 7f263bf2..53c73e3e 100644
--- a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
@@ -6,6 +6,7 @@ Import linearity.
 
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv} {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!lockG Σ}.
 
   cpp.spec "test_mutex()" as test_mutex_spec from source with (\post emp).
 

From 5c0b508ef179927a2f2cf8bec11b82cb3d341931 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 12:03:16 +0200
Subject: [PATCH 06/16] Drop trailing whitespace

---
 .../test/mutex/custom_mutex_hpp_proof.v                | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 2750bcfc..6e218639 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -12,8 +12,8 @@ Module custom_mutex.
   Abbreviation N := "MyMutex"%cpp_name.
 
 
-  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t -> 
-    (* None if value is thread::id(), Some otherwise *) 
+  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t ->
+    (* None if value is thread::id(), Some otherwise *)
     option thread_idT -> Rep.
 
   Parameter exclusive_token : ∀ `{Σ : cpp_logic}, iprop.gname -> mpred.
@@ -28,7 +28,7 @@ Module custom_mutex.
 
   Definition lock_namespace : namespace := nroot .@@ "MyMutex".
 
-  Definition locked `{Σ : cpp_logic} `{!lockG Σ} (g: gname) (th : thread_idT) : mpred 
+  Definition locked `{Σ : cpp_logic} `{!lockG Σ} (g: gname) (th : thread_idT) : mpred
     := owner_token_auth g.(phys_state_gname) (Some th) ** user g.(user_gname) th.
 
   (* Definition IR `{Σ : cpp_logic, σ : genv, !HasStdThreads Σ, !recursive_mutex.lockedG Σ} (γ : gname) (q : cQp.t) : mpred :=
@@ -91,7 +91,7 @@ Module custom_mutex.
       \persist{thr} current_thread thr
       \pre user g.(user_gname) thr
       \post ▷ P ** locked g thr).
-    
+
     cpp.spec "MyMutex::do_unlock()" as unlock_spec with (
       \this this
       \prepost{q P g} this |-> IR g q P
@@ -103,7 +103,7 @@ Module custom_mutex.
     (* Axiom *)
     cpp.spec "std::this_thread::yield()" as yield_spec with (
       \post emp).
-    
+
     Import std.atomic.
     Fail Lemma test_do_lock_ok : verify[source] "MyMutex::do_lock()".
 

From 9f957181811f4f4ee3ac9ead7534db5e7f563cc1 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 12:03:25 +0200
Subject: [PATCH 07/16] cleanups

---
 rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 6e218639..0b6d7068 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -2,11 +2,11 @@
 
 Require Import skylabs.auto.cpp.proof.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
-Require Import skylabs.brick.libstdcpp.test.mutex.custom_mutex_hpp.
 Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
-Import lock_ghost.
 Require Import skylabs.brick.libstdcpp.atomic.spec.
 
+Require Import skylabs.brick.libstdcpp.test.mutex.custom_mutex_hpp.
+
 Module custom_mutex.
 
   Abbreviation N := "MyMutex"%cpp_name.

From 9e6b955a577d1ee774c5c25965bdd4c0b9549248 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 13:14:24 +0200
Subject: [PATCH 08/16] Fix parentheses in Rep

---
 .../test/mutex/custom_mutex_hpp_proof.v          | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 0b6d7068..2b06e63b 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -50,17 +50,17 @@ Module custom_mutex.
       ∃ o_owner,
       owner_token_frac γ.(phys_state_gname) o_owner **
       ∃ b : bool,
-      this ,, _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m b **
-      if b then
+      this ,, _field "MyMutex::m_lock" |-> atomic.R "int" 1$m (if b then 1 else 0)%Z **
+      (if b then
         emp
       else
         owner_token_auth γ.(phys_state_gname) o_owner **
-        P **
-        (** m_owner does not concern do_lock() and do_unlock(), the actual
-          implementation of mutex, and does not always equal o_owner.
-          It is just a resource that one can get from the invariant. *)
-        ∃ m_owner : option thread_idT,
-        this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m m_owner
+        P) **
+      (** m_owner does not concern do_lock() and do_unlock(), the actual
+        implementation of mutex, and does not always equal o_owner.
+        It is just a resource that one can get from the invariant. *)
+      ∃ m_owner : option thread_idT,
+      this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m m_owner
     .
 
     Definition IR (γ : gname) (q : cQp.t) (P : mpred) : Rep :=

From f34aa7c53d8b75197dd26b3156c98a0570bef4d5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 12:02:35 +0200
Subject: [PATCH 09/16] custom_mutex: atomic<bool> -> atomic<int>

---
 rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp b/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
index c5844ede..b5bcbf60 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
@@ -16,13 +16,14 @@ std::mutex protocol:
 - can't be destroyed while held.
 */
 class MyMutex {
-  std::atomic<bool> m_lock{false};
+  // std::atomic<bool> m_lock{false};
+  std::atomic<int> m_lock{0};
 
   std::thread::id m_owner{};
 
   // "Actual locking"
   void do_lock() {
-    while (m_lock.exchange(true)) {
+    while (m_lock.exchange(1)) {
       // Yielding helps scheduling, and makes this loop obviously not UB
       // (under https://eel.is/c++draft/intro.progress#1.2).
       // Calling exchange might qualify under
@@ -32,7 +33,7 @@ class MyMutex {
   }
 
   void do_unlock() {
-    m_lock = false;
+    m_lock = 0;
   }
 public:
 
@@ -60,7 +61,7 @@ class MyMutex {
   }
 
   ~MyMutex() {
-    assert(!m_lock);
+    assert(m_lock == 0);
     assert(m_owner == std::thread::id()); //unowned
   }
 };

From bfc0f314e6f8bde530c345c8c64188bfe158739b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Tue, 1 Sep 2026 13:15:01 +0200
Subject: [PATCH 10/16] Proof sketch

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 96 ++++++++++++++++++-
 1 file changed, 91 insertions(+), 5 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 2b06e63b..add64e88 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -15,6 +15,7 @@ Module custom_mutex.
   Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t ->
     (* None if value is thread::id(), Some otherwise *)
     option thread_idT -> Rep.
+  #[only(timeless)] derive atomic_thread_idT.
 
   Parameter exclusive_token : ∀ `{Σ : cpp_logic}, iprop.gname -> mpred.
   Parameter owner_token_auth : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
@@ -39,7 +40,7 @@ Module custom_mutex.
       _field "MyRecursiveMutex::m_count" |-> ulonglongR 1$m count. *)
 
   Section with_Σ.
-    Context `{Σ : cpp_logic, σ : genv, !HasStdThreads Σ, !lockG Σ}.
+    Context `{Σ : cpp_logic, σ : genv, HAS_THREADS : !HasStdThreads Σ, !lockG Σ}.
 
     Definition mutex_content (γ : gname) : Rep :=
       ∃ o_owner lockedb,
@@ -69,11 +70,12 @@ Module custom_mutex.
         cinv lock_namespace γ.(cinv_gname) (mutex_inv this γ P) **
         cinv_own γ.(cinv_gname) q
       ).
+    Hint Opaque IR : sl_opacity typeclass_instances.
+    #[only(type_ptr,cfractional,ascfractional,cfracvalid)] derive IR.
 
 
 
     Context `{MOD : source ⊧ σ}.
-    Context {HAS_THREADS : HasStdThreads Σ}.
 
     cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
       \this this
@@ -90,6 +92,7 @@ Module custom_mutex.
       \prepost{q P g} this |-> IR g q P
       \persist{thr} current_thread thr
       \pre user g.(user_gname) thr
+      \prepost{q'} _global "std::memory_order_seq_cst" |-> primR "enum std::memory_order" q' (memory_order.to_val memory_order.seq_cst)
       \post ▷ P ** locked g thr).
 
     cpp.spec "MyMutex::do_unlock()" as unlock_spec with (
@@ -104,8 +107,91 @@ Module custom_mutex.
     cpp.spec "std::this_thread::yield()" as yield_spec with (
       \post emp).
 
-    Import std.atomic.
-    Fail Lemma test_do_lock_ok : verify[source] "MyMutex::do_lock()".
-
+    Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int>").
+
+    #[only(timeless)] derive exclusive_token.
+    #[only(timeless)] derive owner_token_auth.
+    #[only(timeless)] derive owner_token_frac.
+
+    Definition bi_later_exist_F := [FWD] @bi.later_exist.
+    Definition bi_later_sep_F := [FWD] @bi.later_sep.
+    Definition bi_later_sep_B := [BWD->] @bi.later_sep.
+    Hint Resolve bi_later_exist_F bi_later_sep_F : br_hints.
+    Import linearity.
+
+    #[program]
+    Definition do_exchange_C (p : ptr) :=
+      \cancelx
+      \using denoteModule source
+      \using{thr} current_thread thr
+      \consuming{g q P} p |-> IR g q P
+      \proving{K (_ : IsExistential K)}
+      std.atomic.do_exchange "int" (BASE (p,, o_field σ "MyMutex::m_lock") ) 1%Z K
+      \instantiate K := (fun res => p |-> IR g q P ** [| res = 0 \/ res = 1 |]%Z **
+                          if bool_decide (res = 0) then P ** owner_token_auth g.(phys_state_gname) (Some thr) else emp)
+                          \end@{mpredI}.
+    Next Obligation.
+      intros. iIntros "[#M ?]" (?? ->).
+      iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+      iAuIntro1. rewrite /atomic1_acc.
+      rewrite {1}/IR/mutex_inv/=; work.
+      wname [cinv] "#?".
+      iInv lock_namespace as "?" "Hc"; work.
+      iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; first solve_ndisj.
+      work.
+      1: admit. (* can and should be an AC *)
+      iMod "Y" as "_"; wpose "Hc"; work.
+      wname [cinv] "CI".
+      wname [owner_token_frac] "OG".
+      wname [_ |-> atomic.R _ _ _] "FL".
+      wname [_ |-> atomic_thread_idT _ _] "FO".
+      ren_hyp b bool.
+      destruct b eqn:?; work. {
+        iSplitL "OG FO FL"; first last. {
+          iModIntro. rewrite /IR/mutex_inv. work $usenamed=true.
+          auto.
+        }
+        work $usenamed=true with br_erefl.
+        iExists _, true.
+        ework $usenamed=true with br_erefl.
+      }
+      wname [P] "P".
+      wname [owner_token_auth] "OA".
+      iSplitL "FO OG FL"; first last. {
+        iModIntro. rewrite /IR/mutex_inv. ework $usenamed=true with br_erefl.
+        auto.
+        (* perform ghost update, but earlier *)
+        admit.
+      }
+      work $usenamed=true with br_erefl.
+      iExists _, true.
+      ework $usenamed=true with br_erefl.
+      all: fail.
+
+      (* iSplitL "OG FO I FL"; first last. { *)
+      (*   iModIntro. rewrite /IR/mutex_inv. work $usenamed=true. *)
+      (*   wfocus [| _ |] "". { iPureIntro. destruct b; auto. } *)
+      (*   destruct b eqn:?; work. *)
+      (* } *)
+      (* destruct b eqn:?. { *)
+      (*   work $usenamed=true with br_erefl. *)
+      (*   iExists _, true. *)
+      (*   ework $usenamed=true with br_erefl. *)
+      (* } *)
+      (* work $usenamed=true with br_erefl. *)
+      (* iExists _, true. *)
+      (* ework $usenamed=true with br_erefl. *)
+      (* iApply affine; last iAccu. *)
+    Admitted.
+    Hint Resolve do_exchange_C : sl_opacity.
+    Hint Opaque locked : sl_opacity.
+
+    Lemma test_do_lock_ok : verify[source] "MyMutex::do_lock()".
+    Proof using MOD HAS_THREADS.
+      verify_spec; go.
+      wp_while (fun _ => emp); go; first by ework.
+      wp_if; go.
+      rewrite /locked; go.
+    Qed.
   End with_Σ.
 End custom_mutex.

From 13f1a011822387e3f1a3df9c6d7b638b89f66234 Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Tue, 1 Sep 2026 21:35:39 +0000
Subject: [PATCH 11/16] progress on custom mutex proof

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 81 +++++++++++--------
 1 file changed, 47 insertions(+), 34 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index add64e88..f447712d 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -12,14 +12,15 @@ Module custom_mutex.
   Abbreviation N := "MyMutex"%cpp_name.
 
 
-  Parameter atomic_thread_idT : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t ->
+  Parameter thread_idR : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t ->
     (* None if value is thread::id(), Some otherwise *)
     option thread_idT -> Rep.
-  #[only(timeless)] derive atomic_thread_idT.
+  #[only(timeless)] derive thread_idR.
 
-  Parameter exclusive_token : ∀ `{Σ : cpp_logic}, iprop.gname -> mpred.
   Parameter owner_token_auth : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
   Parameter owner_token_frac : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
+  #[only(timeless, exclusive)] derive owner_token_auth.
+  #[only(timeless, exclusive)] derive owner_token_frac.
 
   Record gname : Set := MkGname
   { user_gname : iprop.gname
@@ -29,8 +30,10 @@ Module custom_mutex.
 
   Definition lock_namespace : namespace := nroot .@@ "MyMutex".
 
-  Definition locked `{Σ : cpp_logic} `{!lockG Σ} (g: gname) (th : thread_idT) : mpred
-    := owner_token_auth g.(phys_state_gname) (Some th) ** user g.(user_gname) th.
+  Definition locked `{Σ : cpp_logic} `{!lockG Σ} `{σ : genv}
+      (γ: gname) (o_thr : option thread_idT) : Rep :=
+    _field "MyMutex::m_owner" |-> thread_idR 1$m o_thr ** pureR (owner_token_frac γ.(phys_state_gname) o_thr).
+  #[only(timeless, exclusive)] derive locked.
 
   (* Definition IR `{Σ : cpp_logic, σ : genv, !HasStdThreads Σ, !recursive_mutex.lockedG Σ} (γ : gname) (q : cQp.t) : mpred :=
     ∃ x, recursive_mutex.owned_count_id_auth γ.(rec_gname) x. *)
@@ -45,23 +48,23 @@ Module custom_mutex.
     Definition mutex_content (γ : gname) : Rep :=
       ∃ o_owner lockedb,
          _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m lockedb **
-         _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m o_owner.
+         _field "MyMutex::m_owner" |-> thread_idR 1$m o_owner.
 
     Definition mutex_inv (this : ptr) (γ : gname) (P : mpred) : mpred :=
-      ∃ o_owner,
-      owner_token_frac γ.(phys_state_gname) o_owner **
       ∃ b : bool,
       this ,, _field "MyMutex::m_lock" |-> atomic.R "int" 1$m (if b then 1 else 0)%Z **
+      ∃ o_owner : option thread_idT,
+      owner_token_auth γ.(phys_state_gname) o_owner **
       (if b then
-        emp
+        ∃ th, user γ.(user_gname) th ** [| o_owner = Some th |]
       else
-        owner_token_auth γ.(phys_state_gname) o_owner **
-        P) **
-      (** m_owner does not concern do_lock() and do_unlock(), the actual
-        implementation of mutex, and does not always equal o_owner.
-        It is just a resource that one can get from the invariant. *)
-      ∃ m_owner : option thread_idT,
-      this ,, _field "MyMutex::m_owner" |-> atomic_thread_idT 1$m m_owner
+        (* owner_token γ.(phys_state_gname) o_owner ** *)
+        P **
+        (** m_owner does not concern do_lock() and do_unlock(), the actual
+          implementation of mutex, and does not always equal o_owner.
+          It is just a resource that one can get from the invariant. *)
+        this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None **
+        owner_token_frac γ.(phys_state_gname) o_owner)
     .
 
     Definition IR (γ : gname) (q : cQp.t) (P : mpred) : Rep :=
@@ -73,8 +76,6 @@ Module custom_mutex.
     Hint Opaque IR : sl_opacity typeclass_instances.
     #[only(type_ptr,cfractional,ascfractional,cfracvalid)] derive IR.
 
-
-
     Context `{MOD : source ⊧ σ}.
 
     cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
@@ -93,14 +94,16 @@ Module custom_mutex.
       \persist{thr} current_thread thr
       \pre user g.(user_gname) thr
       \prepost{q'} _global "std::memory_order_seq_cst" |-> primR "enum std::memory_order" q' (memory_order.to_val memory_order.seq_cst)
-      \post ▷ P ** locked g thr).
+      \post (▷ P **
+            this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None) **
+            owner_token_frac g.(phys_state_gname) (Some thr)).
 
     cpp.spec "MyMutex::do_unlock()" as unlock_spec with (
       \this this
       \prepost{q P g} this |-> IR g q P
       \persist{thr} current_thread thr
-      \pre locked g thr
       \pre ▷P
+      \pre this |-> locked g (Some thr)
       \post user g.(user_gname) thr).
 
     (* Axiom *)
@@ -109,10 +112,6 @@ Module custom_mutex.
 
     Abbreviation BASE p := (p ,, _base "std::atomic<int>" "std::__atomic_base<int>").
 
-    #[only(timeless)] derive exclusive_token.
-    #[only(timeless)] derive owner_token_auth.
-    #[only(timeless)] derive owner_token_frac.
-
     Definition bi_later_exist_F := [FWD] @bi.later_exist.
     Definition bi_later_sep_F := [FWD] @bi.later_sep.
     Definition bi_later_sep_B := [BWD->] @bi.later_sep.
@@ -125,10 +124,13 @@ Module custom_mutex.
       \using denoteModule source
       \using{thr} current_thread thr
       \consuming{g q P} p |-> IR g q P
+      \consuming user g.(user_gname) thr
       \proving{K (_ : IsExistential K)}
       std.atomic.do_exchange "int" (BASE (p,, o_field σ "MyMutex::m_lock") ) 1%Z K
       \instantiate K := (fun res => p |-> IR g q P ** [| res = 0 \/ res = 1 |]%Z **
-                          if bool_decide (res = 0) then P ** owner_token_auth g.(phys_state_gname) (Some thr) else emp)
+                          if bool_decide (res = 0) then P ** owner_token_frac g.(phys_state_gname) (Some thr) **
+                            p ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None
+                          else user g.(user_gname) thr)
                           \end@{mpredI}.
     Next Obligation.
       intros. iIntros "[#M ?]" (?? ->).
@@ -142,30 +144,32 @@ Module custom_mutex.
       1: admit. (* can and should be an AC *)
       iMod "Y" as "_"; wpose "Hc"; work.
       wname [cinv] "CI".
-      wname [owner_token_frac] "OG".
+      wname [owner_token_auth] "OA".
       wname [_ |-> atomic.R _ _ _] "FL".
-      wname [_ |-> atomic_thread_idT _ _] "FO".
+      wname [_ |-> thread_idR _ _] "PF".
+      wname [user _ _] "U".
       ren_hyp b bool.
       destruct b eqn:?; work. {
-        iSplitL "OG FO FL"; first last. {
+        iSplitL "OA FL PF"; first last. {
           iModIntro. rewrite /IR/mutex_inv. work $usenamed=true.
           auto.
         }
         work $usenamed=true with br_erefl.
-        iExists _, true.
+        iExists true, _.
         ework $usenamed=true with br_erefl.
       }
-      wname [P] "P".
-      wname [owner_token_auth] "OA".
-      iSplitL "FO OG FL"; first last. {
+      iDestruct "PF" as "(P & ? & OF)".
+      iSplitL "FL OA U"; first last. {
         iModIntro. rewrite /IR/mutex_inv. ework $usenamed=true with br_erefl.
         auto.
         (* perform ghost update, but earlier *)
         admit.
       }
       work $usenamed=true with br_erefl.
-      iExists _, true.
+      iExists true, _.
       ework $usenamed=true with br_erefl.
+      (* should be proved by the previously mentioned ghost update *)
+      admit. 
       all: fail.
 
       (* iSplitL "OG FO I FL"; first last. { *)
@@ -191,7 +195,16 @@ Module custom_mutex.
       verify_spec; go.
       wp_while (fun _ => emp); go; first by ework.
       wp_if; go.
-      rewrite /locked; go.
     Qed.
+
+    Lemma test_do_unlock_ok : verify[source] "MyMutex::do_unlock()".
+    Proof using MOD HAS_THREADS.
+      verify_spec; go.
+      iExists (user g.(user_gname) thr).
+      rewrite /locked.
+      work.
+    Admitted.
+
+
   End with_Σ.
 End custom_mutex.

From e7f35d7bc9393fe1f6174e14a2359f87f267dd1a Mon Sep 17 00:00:00 2001
From: rinshankaihou <madoka@umich.edu>
Date: Wed, 2 Sep 2026 07:36:34 +0000
Subject: [PATCH 12/16] custom mutex proof mostly done

Fix invariant.
Add specs for all functions in MyMutex.
Not sure if we need do_store_C or do_load_C.
---
 rocq-brick-libstdcpp/proof/atomic/pred.v      |   3 +
 .../test/mutex/custom_mutex.hpp               |   2 +
 .../test/mutex/custom_mutex_hpp_proof.v       | 415 +++++++++++++++---
 3 files changed, 363 insertions(+), 57 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/atomic/pred.v b/rocq-brick-libstdcpp/proof/atomic/pred.v
index 995d3dc0..435de841 100644
--- a/rocq-brick-libstdcpp/proof/atomic/pred.v
+++ b/rocq-brick-libstdcpp/proof/atomic/pred.v
@@ -5,6 +5,7 @@
  * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
  *)
 Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.cpp.spec.concepts.
 Require skylabs.brick.libstdcpp.atomic.inc_int_cpp.
 
@@ -45,6 +46,8 @@ Module Type ATOMIC_PREDS.
     #[global] Declare Instance R_frac_valid : CFracValid1 R.
     #[global] Declare Instance R_agree : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R).
     #[global] Declare Instance R_type : Typed2 (class_name ty) R.
+    #[global] Declare Instance R_weakly_objective q x p :
+      WeaklyObjective (R q x p).
   End R_props.
 
 End ATOMIC_PREDS.
diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp b/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
index b5bcbf60..54865952 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp
@@ -37,6 +37,8 @@ class MyMutex {
   }
 public:
 
+  MyMutex() {}
+
   void lock() {
     std::thread::id this_id{std::this_thread::get_id()};
 
diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index f447712d..4e62bd24 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -1,27 +1,122 @@
 (** Provisional *)
 
+Require Import iris.algebra.lib.excl_auth.
+Require Import iris.algebra.gset.
+
 Require Import skylabs.auto.cpp.proof.
+Require Import skylabs.auto.cpp.hints.base_derived.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
+Require Import skylabs.brick.libstdcpp.mutex.requirements.
 Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 Require Import skylabs.brick.libstdcpp.atomic.spec.
+Require Import skylabs.brick.libstdcpp.cassert.spec.
 
 Require Import skylabs.brick.libstdcpp.test.mutex.custom_mutex_hpp.
 
 Module custom_mutex.
 
-  Abbreviation N := "MyMutex"%cpp_name.
+  #[local] Existing Instance lock_ghost.has_lock.
+  #[local] Existing Instance lock_ghost.has_lock_upd.
+  #[local] Existing Instance lock_ghost.has_lock_valid.
 
+  Abbreviation N := "MyMutex"%cpp_name.
 
+  (* FIXME maybe don't need to split it? *)
   Parameter thread_idR : ∀ `{Σ : cpp_logic, σ : genv}, cQp.t ->
     (* None if value is thread::id(), Some otherwise *)
     option thread_idT -> Rep.
-  #[only(timeless)] derive thread_idR.
+  #[only(cfracsplittable, type_ptr="std::thread::id")] derive thread_idR.
+  #[global] Axiom thread_idR_WeaklyObjective :
+    ∀ `{Σ : cpp_logic, σ : genv} (q : cQp.t)
+      (o : option thread_idT) (p : ptr),
+      WeaklyObjective (thread_idR q o p).
+  #[global] Existing Instance thread_idR_WeaklyObjective.
+
+  #[local] Instance at_WeaklyObjective `{Σ : cpp_logic}
+      (p : ptr) (R : Rep) `{!WeaklyObjective (R p)} :
+    WeaklyObjective (p |-> R).
+  Proof. rewrite INTERNAL._at_eq. apply _. Qed.
+
+  Canonical Structure owner_stateO := optionO thread_idTO.
+  Canonical Structure owner_tokenR := excl_authR owner_stateO.
 
-  Parameter owner_token_auth : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
-  Parameter owner_token_frac : ∀ `{Σ : cpp_logic}, iprop.gname -> option thread_idT -> mpred.
+  Class ownerG `{Σ : cpp_logic} := {
+    #[local] has_owner_token :: HasOwn (iPropI _Σ) owner_tokenR;
+    #[local] has_owner_token_upd :: HasOwnUpd (iPropI _Σ) owner_tokenR;
+    #[local] has_owner_token_valid :: HasOwnValid (iPropI _Σ) owner_tokenR;
+  }.
+  #[global] Arguments ownerG {_ _} Σ : assert.
+
+  sl.lock
+  Definition owner_token_auth `{Σ : cpp_logic, !ownerG Σ}
+      (γ : iprop.gname) (o_thr : option thread_idT) : mpred :=
+    own γ (●E o_thr).
+  sl.lock
+  Definition owner_token_frac `{Σ : cpp_logic, !ownerG Σ}
+      (γ : iprop.gname) (o_thr : option thread_idT) : mpred :=
+    own γ (◯E o_thr).
   #[only(timeless, exclusive)] derive owner_token_auth.
   #[only(timeless, exclusive)] derive owner_token_frac.
 
+  #[global] Instance owner_token_auth_WeaklyObjective
+      `{Σ : cpp_logic, !ownerG Σ} γ o_thr :
+    WeaklyObjective (PROP := iPropI _) (owner_token_auth γ o_thr).
+  Proof. rewrite owner_token_auth.unlock. apply _. Qed.
+
+  #[global] Instance owner_token_frac_WeaklyObjective
+      `{Σ : cpp_logic, !ownerG Σ} γ o_thr :
+    WeaklyObjective (PROP := iPropI _) (owner_token_frac γ o_thr).
+  Proof. rewrite owner_token_frac.unlock. apply _. Qed.
+
+  Lemma owner_token_agree `{Σ : cpp_logic, !ownerG Σ}
+      γ (o1 o2 : option thread_idT) :
+    owner_token_auth γ o1 ** owner_token_frac γ o2 |-- [| o1 = o2 |].
+  Proof.
+    rewrite owner_token_auth.unlock owner_token_frac.unlock.
+    iIntros "[A F]".
+    iDestruct (own_valid_2 with "A F") as %HV.
+    iPureIntro.
+    apply leibniz_equiv, excl_auth_agree, HV.
+  Qed.
+
+  #[global] Instance owner_token_agree_observe
+      `{Σ : cpp_logic, !ownerG Σ} γ (o1 o2 : option thread_idT) :
+    Observe2 [| o1 = o2 |]
+      (owner_token_auth γ o1) (owner_token_frac γ o2).
+  Proof.
+    apply observe_2_intro_only_provable.
+    rewrite owner_token_auth.unlock owner_token_frac.unlock.
+    iIntros "A F".
+    iDestruct (own_valid_2 with "A F") as %HV.
+    iPureIntro.
+    apply leibniz_equiv, excl_auth_agree, HV.
+  Qed.
+
+  #[global] Instance owner_token_agree_observe_sep
+      `{Σ : cpp_logic, !ownerG Σ} γ (o1 o2 : option thread_idT) :
+    Observe [| o1 = o2 |]
+      (owner_token_auth γ o1 ** owner_token_frac γ o2).
+  Proof.
+    apply observe_intro_only_provable.
+    rewrite owner_token_auth.unlock owner_token_frac.unlock.
+    iIntros "[A F]".
+    iDestruct (own_valid_2 with "A F") as %HV.
+    iPureIntro.
+    apply leibniz_equiv, excl_auth_agree, HV.
+  Qed.
+
+  Lemma owner_token_update `{Σ : cpp_logic, !ownerG Σ}
+      γ (oa ofrag o' : option thread_idT) :
+    owner_token_auth γ oa ** owner_token_frac γ ofrag |--
+      (|==> owner_token_auth γ o' ** owner_token_frac γ o').
+  Proof.
+    rewrite owner_token_auth.unlock owner_token_frac.unlock.
+    iIntros "[A F]".
+    iMod (own_update_2 with "A F") as "[$ $]";
+      first apply (excl_auth_update _ _ o').
+    done.
+  Qed.
+
   Record gname : Set := MkGname
   { user_gname : iprop.gname
   ; cinv_gname : iprop.gname
@@ -30,7 +125,8 @@ Module custom_mutex.
 
   Definition lock_namespace : namespace := nroot .@@ "MyMutex".
 
-  Definition locked `{Σ : cpp_logic} `{!lockG Σ} `{σ : genv}
+  sl.lock
+  Definition locked `{Σ : cpp_logic} `{!lockG Σ, !ownerG Σ} `{σ : genv}
       (γ: gname) (o_thr : option thread_idT) : Rep :=
     _field "MyMutex::m_owner" |-> thread_idR 1$m o_thr ** pureR (owner_token_frac γ.(phys_state_gname) o_thr).
   #[only(timeless, exclusive)] derive locked.
@@ -43,7 +139,11 @@ Module custom_mutex.
       _field "MyRecursiveMutex::m_count" |-> ulonglongR 1$m count. *)
 
   Section with_Σ.
-    Context `{Σ : cpp_logic, σ : genv, HAS_THREADS : !HasStdThreads Σ, !lockG Σ}.
+    Context `{Σ : cpp_logic, σ : genv, HAS_THREADS : !HasStdThreads Σ,
+      !lockG Σ, !ownerG Σ}.
+
+    (* Abbreviation BASE p :=
+      (p ,, _base "std::atomic<int>" "std::__atomic_base<int>"). *)
 
     Definition mutex_content (γ : gname) : Rep :=
       ∃ o_owner lockedb,
@@ -52,7 +152,8 @@ Module custom_mutex.
 
     Definition mutex_inv (this : ptr) (γ : gname) (P : mpred) : mpred :=
       ∃ b : bool,
-      this ,, _field "MyMutex::m_lock" |-> atomic.R "int" 1$m (if b then 1 else 0)%Z **
+      this ,, _field "MyMutex::m_lock" |->
+        atomic.R "int" 1$m (if b then 1 else 0)%Z **
       ∃ o_owner : option thread_idT,
       owner_token_auth γ.(phys_state_gname) o_owner **
       (if b then
@@ -78,35 +179,117 @@ Module custom_mutex.
 
     Context `{MOD : source ⊧ σ}.
 
+    Abbreviation GLOBALS q :=
+      (_global "std::memory_order_seq_cst" |->
+        primR "enum std::memory_order" q
+          (memory_order.to_val memory_order.seq_cst)).
+
+    cpp.spec (default_ctor "std::thread::id") as thread_id_ctor_spec with (
+      \this this
+      \post this |-> thread_idR 1$m None).
+
+    cpp.spec (const_copy_ctor "std::thread::id") as thread_id_copy_ctor_spec with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \prepost{q o} other |-> thread_idR q o
+      \post this |-> thread_idR 1$m o).
+
+    cpp.spec (dtor "std::thread::id") as thread_id_dtor_spec with (
+      \this this
+      \pre{o} this |-> thread_idR 1$m o
+      \post emp).
+
+    cpp.spec "std::thread::id::operator=(const std::thread::id&)"
+        as thread_id_copy_assign_spec with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{old} this |-> thread_idR 1$m old
+      \prepost{q o} other |-> thread_idR q o
+      \post[Vref this] this |-> thread_idR 1$m o).
+
+    cpp.spec "std::thread::id::operator=(std::thread::id&&)"
+        as thread_id_move_assign_spec with (
+      \this this
+      \arg{other} "" (Vptr other)
+      \pre{old} this |-> thread_idR 1$m old
+      \prepost{o} other |-> thread_idR 1$m o
+      \post[Vref this] this |-> thread_idR 1$m o).
+
+    cpp.spec "std::operator==(std::thread::id, std::thread::id)"
+        as thread_id_eq_spec with (
+      \arg{lhs} "" (Vptr lhs)
+      \arg{rhs} "" (Vptr rhs)
+      \prepost{q1 o1} lhs |-> thread_idR q1 o1
+      \prepost{q2 o2} rhs |-> thread_idR q2 o2
+      \post[Vbool (bool_decide (o1 = o2))] emp).
+
+    cpp.spec "std::this_thread::get_id()" as get_id_spec with (
+      \persist{thr} current_thread thr
+      \post{result}[Vptr result]
+        result |-> thread_idR 1$m (Some thr)).
+
     cpp.spec "MyMutex::MyMutex()" as ctor_spec with (
       \this this
       \pre{P} ▷P
-      \post Exists g, this |-> IR g 1$m P ** used_threads g.(user_gname) ∅).
+      \require WeaklyObjective P
+      \post (|={⊤}=> Exists g,
+        this |-> IR g 1$m P ** used_threads g.(user_gname) ∅)).
 
     cpp.spec "MyMutex::~MyMutex()" as dtor_spec with (
       \this this
       \pre{g P} this |-> IR g 1$m P ** used_threads g.(user_gname) ∅
       \post P).
 
-    cpp.spec "MyMutex::do_lock()" as lock_spec with (
+    cpp.spec "MyMutex::do_lock()" as do_lock_spec with (
       \this this
       \prepost{q P g} this |-> IR g q P
       \persist{thr} current_thread thr
       \pre user g.(user_gname) thr
-      \prepost{q'} _global "std::memory_order_seq_cst" |-> primR "enum std::memory_order" q' (memory_order.to_val memory_order.seq_cst)
-      \post (▷ P **
+      \prepost{q'} GLOBALS q'
+      \post (P **
             this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None) **
             owner_token_frac g.(phys_state_gname) (Some thr)).
 
-    cpp.spec "MyMutex::do_unlock()" as unlock_spec with (
+    cpp.spec "MyMutex::do_unlock()" as do_unlock_spec with (
       \this this
       \prepost{q P g} this |-> IR g q P
       \persist{thr} current_thread thr
-      \pre ▷P
-      \pre this |-> locked g (Some thr)
+      \pre (▷P **
+            this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None) **
+            owner_token_frac g.(phys_state_gname) (Some thr)
       \post user g.(user_gname) thr).
 
-    (* Axiom *)
+    Definition T : Type := gname * mpred.
+
+    (* FIXME should GLOBALS be in lock specs, instead of do_lock? *)
+    Definition do_lock (this : ptr) (lk : T) (K : mpred) : mpred :=
+      let g := lk.1 in
+      let P := lk.2 in
+      ∃ thr q', current_thread thr ** user g.(user_gname) thr ** GLOBALS q' **
+        (GLOBALS q' ** P ** this |-> locked g (Some thr) -* K).
+    #[global] Arguments do_lock /.
+
+    Definition do_unlock (this : ptr) (lk : T) (K : mpred) : mpred :=
+      let g := lk.1 in
+      let P := lk.2 in
+      ∃ thr, current_thread thr ** this |-> locked g (Some thr) ** ▷P **
+        (user g.(user_gname) thr -* K).
+    #[global] Arguments do_unlock /.
+
+    #[global] Instance custom_mutex_basic_lockable :
+        BasicLockable (T := T) (Tnamed N)
+          (fun q gP => IR gP.1 q gP.2) :=
+      { do_lock := do_lock
+      ; do_unlock := do_unlock }.
+
+    cpp.spec "MyMutex::lock()" as lock_spec with
+      (\exact Reduce
+        (lock_basic_lockable (Tnamed N) (fun q gP => IR gP.1 q gP.2))).
+
+    cpp.spec "MyMutex::unlock()" as unlock_spec with
+      (\exact Reduce
+        (unlock_basic_lockable (Tnamed N) (fun q gP => IR gP.1 q gP.2))).
+
     cpp.spec "std::this_thread::yield()" as yield_spec with (
       \post emp).
 
@@ -142,68 +325,186 @@ Module custom_mutex.
       iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; first solve_ndisj.
       work.
       1: admit. (* can and should be an AC *)
-      iMod "Y" as "_"; wpose "Hc"; work.
       wname [cinv] "CI".
       wname [owner_token_auth] "OA".
       wname [_ |-> atomic.R _ _ _] "FL".
       wname [_ |-> thread_idR _ _] "PF".
       wname [user _ _] "U".
       ren_hyp b bool.
-      destruct b eqn:?; work. {
-        iSplitL "OA FL PF"; first last. {
-          iModIntro. rewrite /IR/mutex_inv. work $usenamed=true.
-          auto.
-        }
-        work $usenamed=true with br_erefl.
-        iExists true, _.
-        ework $usenamed=true with br_erefl.
-      }
-      iDestruct "PF" as "(P & ? & OF)".
-      iSplitL "FL OA U"; first last. {
-        iModIntro. rewrite /IR/mutex_inv. ework $usenamed=true with br_erefl.
+      destruct b eqn:Hb.
+      - iMod "Y" as "_".
+        iMod ("Hc" with "[FL OA PF]") as "_".
+        { iNext. iExists true. iFrame. }
+        iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
+        auto.
+      - iDestruct "PF" as "(P & FO & OF)".
+        iMod (owner_token_update g.(phys_state_gname) _ _ (Some thr)
+          with "[$OA $OF]") as "(OA & OF)".
+        iMod "Y" as "_".
+        iMod ("Hc" with "[FL OA U]") as "_".
+        { iNext. iExists true. iFrame. done. }
+        iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
         auto.
-        (* perform ghost update, but earlier *)
-        admit.
-      }
-      work $usenamed=true with br_erefl.
-      iExists true, _.
-      ework $usenamed=true with br_erefl.
-      (* should be proved by the previously mentioned ghost update *)
-      admit. 
-      all: fail.
-
-      (* iSplitL "OG FO I FL"; first last. { *)
-      (*   iModIntro. rewrite /IR/mutex_inv. work $usenamed=true. *)
-      (*   wfocus [| _ |] "". { iPureIntro. destruct b; auto. } *)
-      (*   destruct b eqn:?; work. *)
-      (* } *)
-      (* destruct b eqn:?. { *)
-      (*   work $usenamed=true with br_erefl. *)
-      (*   iExists _, true. *)
-      (*   ework $usenamed=true with br_erefl. *)
-      (* } *)
-      (* work $usenamed=true with br_erefl. *)
-      (* iExists _, true. *)
-      (* ework $usenamed=true with br_erefl. *)
-      (* iApply affine; last iAccu. *)
     Admitted.
     Hint Resolve do_exchange_C : sl_opacity.
+
+    #[program]
+    Definition do_store_C (p : ptr) :=
+      \cancelx
+      \using denoteModule source
+      \using{thr} current_thread thr
+      \consuming{g q P} p |-> IR g q P
+      \consuming P
+      \consuming p ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None
+      \consuming owner_token_frac g.(phys_state_gname) (Some thr)
+      \proving{K (_ : IsExistential K)}
+        std.atomic.do_store "int" (BASE (p ,, o_field σ "MyMutex::m_lock")) 0%Z K
+      \instantiate K := (p |-> IR g q P ** user g.(user_gname) thr)
+      \end@{mpredI}.
+    Next Obligation.
+      intros. iIntros "[#M ?]" (?? ->).
+      iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+      rewrite /std.atomic.do_store.
+      iAcIntro. rewrite /commit_acc /=.
+      rewrite {1}/IR/mutex_inv /=; work.
+      wname [cinv] "#?".
+      iInv lock_namespace as "?" "Hc"; work.
+      ren_hyp b bool.
+      iExists (if b then 1%Z else 0%Z). iFrame.
+      iApply fupd_mask_intro; first solve_ndisj.
+      iIntros "Y". iNext. iIntros "FL".
+      iMod "Y" as "_".
+      wname [P] "P".
+      wname [_ |-> thread_idR _ _] "FO".
+      wname [owner_token_frac] "OF".
+      wname [owner_token_auth] "OA".
+      iRename "P" into "CI".
+      wname [P] "RP".
+      wname [_ |-> thread_idR _ _] "OwnerField".
+      destruct b eqn:Hb.
+      - iDestruct "FO" as (owner) "(U & ->)".
+        iDestruct (observe [| Some owner = Some thr |]
+          (owner_token_auth g.(phys_state_gname) (Some owner) **
+           owner_token_frac g.(phys_state_gname) (Some thr))
+          with "[$OA $OF]")
+          as %Hagree.
+        inversion Hagree; subst owner.
+        iEval (rewrite _at_offsetR) in "FL".
+        iMod ("Hc" with "[FL OA RP OwnerField OF]") as "_".
+        { iNext. iExists false.
+          work $usenamed=true with br_erefl.
+          iExists (Some thr). iFrame. }
+        iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
+      - iDestruct "FO" as "(RP2 & OwnerField2 & OF2)".
+        iEval (rewrite owner_token_frac.unlock) in "OF".
+        iEval (rewrite owner_token_frac.unlock) in "OF2".
+        iDestruct (own_valid_2 with "OF OF2") as %Hvalid.
+        rewrite excl_auth_frag_op_valid in Hvalid.
+        done.
+    Qed.
+    Hint Resolve do_store_C : sl_opacity.
+
+    #[program]
+    Definition do_load_C (p : ptr) :=
+      \cancelx
+      \using denoteModule source
+      \consuming{q (n : Z)} p |-> atomic.R "int" q n
+      \proving{(K : Z -> mpred) (_ : IsExistential K)}
+        std.atomic.do_load "int" (BASE p) K
+      \instantiate K :=
+        (fun x : Z => p |-> atomic.R "int" q n ** [| x = n |])
+      \end@{mpredI}.
+    Next Obligation.
+      intros. iIntros "[#M ?]" (?? ->).
+      iDestruct (observe [| _ ⊧ _ |] with "M") as "%".
+      rewrite /std.atomic.do_load.
+      iAcIntro. rewrite /commit_acc.
+      iDestruct (fupd_mask_subseteq) as ">Y"; [ | iModIntro ]; eauto.
+      work. iExists q. work.
+      iMod "Y". iModIntro.
+      work.
+    Qed.
+    Hint Resolve do_load_C : sl_opacity.
+
     Hint Opaque locked : sl_opacity.
 
-    Lemma test_do_lock_ok : verify[source] "MyMutex::do_lock()".
+    Lemma mymutex_do_lock_proof : verify[source] "MyMutex::do_lock()".
     Proof using MOD HAS_THREADS.
       verify_spec; go.
       wp_while (fun _ => emp); go; first by ework.
       wp_if; go.
     Qed.
 
-    Lemma test_do_unlock_ok : verify[source] "MyMutex::do_unlock()".
+    Lemma mymutex_do_unlock_proof : verify[source] "MyMutex::do_unlock()".
     Proof using MOD HAS_THREADS.
       verify_spec; go.
-      iExists (user g.(user_gname) thr).
-      rewrite /locked.
+    Qed.
+
+    Lemma mymutex_ctor_proof : verify[source] "MyMutex::MyMutex()".
+    Proof using MOD HAS_THREADS.
+      verify_spec; go.
+      wname [structR] "S".
+      iMod (own_alloc (● (GSet ∅ : lock_ghostUR))) as (gu) "UT".
+      { apply auth_auth_valid. done. }
+      iMod (own_alloc (●E None ⋅ ◯E None)) as (gp) "O".
+      { apply excl_auth_valid. }
+      iDestruct (own_op with "O") as "(OA & OF)".
+      iMod (cinv_alloc ⊤ lock_namespace
+        (mutex_inv this (MkGname gu gu gp) P) with "[-S UT]")
+        as (gi) "(#CI & CO)"; last first.
+      - iExists (MkGname gu gi gp).
+        rewrite /IR used_threads.unlock /=.
+        iModIntro. go $usenamed=true with br_erefl.
+      - rewrite /mutex_inv owner_token_auth.unlock
+          owner_token_frac.unlock /=.
+        iNext. iExists false. iFrame.
+    Qed.
+
+    Lemma mymutex_dtor_proof : verify[source] "MyMutex::~MyMutex()".
+    Proof using MOD HAS_THREADS.
+      verify_spec.
+      rewrite /IR /mutex_inv.
       work.
-    Admitted.
+      wname [cinv] "#CI".
+      wname [cinv_own] "CO".
+      iMod (cinv_cancel with "CI CO")
+        as "Inv"; [done..|].
+      go.
+      iDestruct "Inv" as (b) "(Lock & % & OA & State)".
+      destruct b eqn:Hb.
+      - iDestruct "State" as (th) "(U & %Eq)".
+        iDestruct (used_threads_empty_no_not_locked with "[$]") as %[].
+      - iDestruct "State" as "(P & Owner & OF)".
+        ego $usenamed=true with br_erefl.
+        wname [used_threads] "UT".
+        iApply (affine with "[OA OF UT]"); last iAccu. apply mpred_BiAffine.
+  Qed.
+
+    Lemma mymutex_lock_proof : verify[source] "MyMutex::lock()".
+    Proof using MOD HAS_THREADS.
+      verify_spec.
+      rewrite locked.unlock.
+      ego.
+    Qed.
+
+    Lemma mymutex_unlock_proof : verify[source] "MyMutex::unlock()".
+    Proof using MOD HAS_THREADS.
+      verify_spec.
+      rewrite locked.unlock.
+      go.
+      iExists _, _.
+      go.
+      iExists _, _, _, _.
+      go.
+      iExists _, _.
+      go.
+      iExists _, _.
+      go.
+      iExists _.
+      go.
+      iExists q, m.2, m.1.
+      go.
+    Qed.
 
 
   End with_Σ.

From 7b078ec1e8209207c58b2d447c28aa8d246f1133 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 2 Sep 2026 13:18:18 +0200
Subject: [PATCH 13/16] Import linearity, drop unused lemmas

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 26 +++----------------
 1 file changed, 3 insertions(+), 23 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 4e62bd24..5d66d8a0 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -11,6 +11,7 @@ Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 Require Import skylabs.brick.libstdcpp.atomic.spec.
 Require Import skylabs.brick.libstdcpp.cassert.spec.
 
+Import linearity.
 Require Import skylabs.brick.libstdcpp.test.mutex.custom_mutex_hpp.
 
 Module custom_mutex.
@@ -68,16 +69,6 @@ Module custom_mutex.
     WeaklyObjective (PROP := iPropI _) (owner_token_frac γ o_thr).
   Proof. rewrite owner_token_frac.unlock. apply _. Qed.
 
-  Lemma owner_token_agree `{Σ : cpp_logic, !ownerG Σ}
-      γ (o1 o2 : option thread_idT) :
-    owner_token_auth γ o1 ** owner_token_frac γ o2 |-- [| o1 = o2 |].
-  Proof.
-    rewrite owner_token_auth.unlock owner_token_frac.unlock.
-    iIntros "[A F]".
-    iDestruct (own_valid_2 with "A F") as %HV.
-    iPureIntro.
-    apply leibniz_equiv, excl_auth_agree, HV.
-  Qed.
 
   #[global] Instance owner_token_agree_observe
       `{Σ : cpp_logic, !ownerG Σ} γ (o1 o2 : option thread_idT) :
@@ -92,19 +83,6 @@ Module custom_mutex.
     apply leibniz_equiv, excl_auth_agree, HV.
   Qed.
 
-  #[global] Instance owner_token_agree_observe_sep
-      `{Σ : cpp_logic, !ownerG Σ} γ (o1 o2 : option thread_idT) :
-    Observe [| o1 = o2 |]
-      (owner_token_auth γ o1 ** owner_token_frac γ o2).
-  Proof.
-    apply observe_intro_only_provable.
-    rewrite owner_token_auth.unlock owner_token_frac.unlock.
-    iIntros "[A F]".
-    iDestruct (own_valid_2 with "A F") as %HV.
-    iPureIntro.
-    apply leibniz_equiv, excl_auth_agree, HV.
-  Qed.
-
   Lemma owner_token_update `{Σ : cpp_logic, !ownerG Σ}
       γ (oa ofrag o' : option thread_idT) :
     owner_token_auth γ oa ** owner_token_frac γ ofrag |--
@@ -145,10 +123,12 @@ Module custom_mutex.
     (* Abbreviation BASE p :=
       (p ,, _base "std::atomic<int>" "std::__atomic_base<int>"). *)
 
+    (*
     Definition mutex_content (γ : gname) : Rep :=
       ∃ o_owner lockedb,
          _field "MyMutex::m_lock" |-> atomic.R "bool" 1$m lockedb **
          _field "MyMutex::m_owner" |-> thread_idR 1$m o_owner.
+    *)
 
     Definition mutex_inv (this : ptr) (γ : gname) (P : mpred) : mpred :=
       ∃ b : bool,

From 3ffdfb3a5d49ebe90c9766517180a13a2ee754d4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 2 Sep 2026 13:44:34 +0200
Subject: [PATCH 14/16] Proof tweaks

---
 .../test/mutex/custom_mutex_hpp_proof.v       | 40 +++++++++++--------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 5d66d8a0..5821cb0c 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -311,23 +311,33 @@ Module custom_mutex.
       wname [_ |-> thread_idR _ _] "PF".
       wname [user _ _] "U".
       ren_hyp b bool.
+      iMod "Y" as "_".
       destruct b eqn:Hb.
-      - iMod "Y" as "_".
-        iMod ("Hc" with "[FL OA PF]") as "_".
-        { iNext. iExists true. iFrame. }
+      - iMod ("Hc" with "[FL OA PF]") as "_".
+        { iExists true. ework $usenamed=true with br_erefl. }
         iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
         auto.
       - iDestruct "PF" as "(P & FO & OF)".
         iMod (owner_token_update g.(phys_state_gname) _ _ (Some thr)
           with "[$OA $OF]") as "(OA & OF)".
-        iMod "Y" as "_".
         iMod ("Hc" with "[FL OA U]") as "_".
-        { iNext. iExists true. iFrame. done. }
+        { iExists true. ework $usenamed=true with br_erefl. }
         iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
         auto.
     Admitted.
     Hint Resolve do_exchange_C : sl_opacity.
 
+    #[global] Instance owner_token_frac_excl g :
+      Exclusive1 (owner_token_frac g).
+    Proof.
+      intros; rewrite observe_2_pure owner_token_frac.unlock.
+      apply /observe_2_derive_only_provable.
+      by rewrite excl_auth_frag_op_valid.
+    Qed.
+    Import observe2_fwd.
+    Definition owner_token_frac_excl_F := ltac:(mk_obs2_fwd owner_token_frac_excl).
+    Hint Resolve owner_token_frac_excl_F : sl_opacity.
+
     #[program]
     Definition do_store_C (p : ptr) :=
       \cancelx
@@ -363,24 +373,20 @@ Module custom_mutex.
       wname [_ |-> thread_idR _ _] "OwnerField".
       destruct b eqn:Hb.
       - iDestruct "FO" as (owner) "(U & ->)".
-        iDestruct (observe [| Some owner = Some thr |]
-          (owner_token_auth g.(phys_state_gname) (Some owner) **
-           owner_token_frac g.(phys_state_gname) (Some thr))
-          with "[$OA $OF]")
-          as %Hagree.
-        inversion Hagree; subst owner.
+        iDestruct (observe_2 [| Some owner = Some thr |] with "OA OF")
+          as %->%(inj _).
         iEval (rewrite _at_offsetR) in "FL".
         iMod ("Hc" with "[FL OA RP OwnerField OF]") as "_".
         { iNext. iExists false.
           work $usenamed=true with br_erefl.
           iExists (Some thr). iFrame. }
         iModIntro. rewrite /IR. work $usenamed=true with br_erefl.
-      - iDestruct "FO" as "(RP2 & OwnerField2 & OF2)".
-        iEval (rewrite owner_token_frac.unlock) in "OF".
-        iEval (rewrite owner_token_frac.unlock) in "OF2".
-        iDestruct (own_valid_2 with "OF OF2") as %Hvalid.
-        rewrite excl_auth_frag_op_valid in Hvalid.
-        done.
+      -
+        (* TODO AUTO *)
+        Fail by work $usenamed=true.
+        Succeed by iStopProof; work.
+        iDestruct "FO" as "?"; iDestruct "OF" as "?";
+          work using owner_token_frac_excl_F.
     Qed.
     Hint Resolve do_store_C : sl_opacity.
 

From c5aec847c2c4a6aab56ad9dd245f364f8334c326 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Wed, 2 Sep 2026 14:17:41 +0200
Subject: [PATCH 15/16] More proof tweaks

---
 .../test/mutex/custom_mutex_hpp_proof.v          | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 5821cb0c..0a4ba63a 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -477,19 +477,9 @@ Module custom_mutex.
     Proof using MOD HAS_THREADS.
       verify_spec.
       rewrite locked.unlock.
-      go.
-      iExists _, _.
-      go.
-      iExists _, _, _, _.
-      go.
-      iExists _, _.
-      go.
-      iExists _, _.
-      go.
-      iExists _.
-      go.
-      iExists q, m.2, m.1.
-      go.
+      (* TODO AUTO *)
+      Fail by ego.
+      repeat (go; ework).
     Qed.
 
 

From 6a75fb62afc4c751bf0c8001ba20edde35dce3e1 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 4 Sep 2026 12:39:06 +0200
Subject: [PATCH 16/16] Spec tweaks

---
 .../test/mutex/custom_mutex_hpp_proof.v                | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
index 0a4ba63a..e6da730c 100644
--- a/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
+++ b/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v
@@ -226,17 +226,17 @@ Module custom_mutex.
       \persist{thr} current_thread thr
       \pre user g.(user_gname) thr
       \prepost{q'} GLOBALS q'
-      \post (P **
-            this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None) **
+      \post P **
+            this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None **
             owner_token_frac g.(phys_state_gname) (Some thr)).
 
     cpp.spec "MyMutex::do_unlock()" as do_unlock_spec with (
       \this this
       \prepost{q P g} this |-> IR g q P
       \persist{thr} current_thread thr
-      \pre (▷P **
-            this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None) **
-            owner_token_frac g.(phys_state_gname) (Some thr)
+      \pre ▷P
+      \pre this ,, _field "MyMutex::m_owner" |-> thread_idR 1$m None
+      \pre owner_token_frac g.(phys_state_gname) (Some thr)
       \post user g.(user_gname) thr).
 
     Definition T : Type := gname * mpred.