From a67cb26f8f9e28ab8c87131533a5cbf6ce64e078 Mon Sep 17 00:00:00 2001 From: rinshankaihou Date: Mon, 31 Aug 2026 18:13:50 +0000 Subject: [PATCH 1/4] [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. *) (** <> 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 3d49757e873ff4e199082248462b45f2eaf004b6 Mon Sep 17 00:00:00 2001 From: rinshankaihou Date: Mon, 31 Aug 2026 18:40:05 +0000 Subject: [PATCH 2/4] 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::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::~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::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<...>::~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 10d5ee259062367b1a00d85b04aea57a97629a50 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 1 Sep 2026 11:58:22 +0200 Subject: [PATCH 3/4] 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 1770be11be7dfefb533fd4575e3cda40fa267980 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 4 Sep 2026 13:46:17 +0200 Subject: [PATCH 4/4] WIP on porting mutex client --- .../test/mutex/test_cpp_proof.v | 91 +++++++++++++++++-- 1 file changed, 81 insertions(+), 10 deletions(-) diff --git a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v index 53c73e3e..3406e906 100644 --- a/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v @@ -8,12 +8,48 @@ 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). + cpp.spec "test_mutex()" as test_mutex_spec from source with ( + \post emp). + + (* #[program] *) + (* Definition login_C E (th : thread_idT) (g : gname) (s : gset thread_idT) := *) + (* \cancelx *) + (* \masks MatchFUpd E E => NoConfig *) + (* \consuming lock_ghost.used_threads g s *) + (* \preserving current_thread th *) + (* (* \require th ∉ s *) *) + (* \using [| th ∉ s |] *) + (* \deduce lock_ghost.users g {[th]} *) + (* \deduce lock_ghost.used_threads g (s ∪ {[th]}) *) + (* \end. *) + (* Next Obligation. *) + (* intros; work. *) + (* wapply (lock_ghost.login th g s); first set_solver; work. *) + (* iModIntro; work. *) + (* Qed. *) + + Import wp_notations.Verbose. Theorem test_mutex_ok : verify[source] "test_mutex()". Proof. verify_spec; go. - iExists emp. go. + iExists emp. + wuntil Emember_call go. + + ren_hyp g gname. + wapply current_thread_always_exists; work. + wapply (lock_ghost.login t g ∅); first set_solver. + + (* Depends on fewer details, but more awkward. *) + Succeed + solve [ + wuntil (FreeTemps.delete "std::mutex") go; run1; iApply fupd_wp_destroy_named; + wapply (lock_ghost.logout t g ∅); first set_solver; work; iModIntro; go]. + + (* Easier, but more fragile: [Kfree] might disappear. *) + wuntil Kfree go. + wapply (lock_ghost.logout t g ∅); first set_solver. + go. Qed. cpp.spec "test_lock_guard()" as test_lock_guard_spec from source with (\post emp). @@ -21,7 +57,17 @@ Section with_cpp. Lemma test_lock_guard_ok : verify[source] "test_lock_guard()". Proof. verify_spec; go. - iExists emp; go. + iExists emp. + wuntil Econstructor go. + + ren_hyp g gname. + wapply current_thread_always_exists; work. + wapply (lock_ghost.login t g ∅); first set_solver. + wuntil Kfree go; run1; wuntil Kfree go. + + wapply (lock_ghost.logout t g ∅); first set_solver. + + go. Qed. cpp.spec "test_scoped_lock()" as test_scoped_lock_spec from source with (\post emp). @@ -30,19 +76,36 @@ Section with_cpp. Proof. verify_spec; go. iExists emp; go. - iExists emp; go. + iExists emp. + wuntil Econstructor go. + wapply current_thread_always_exists; work. + wapply (lock_ghost.login t _ ∅); last work with br_erefl; first set_solver. + wapply (lock_ghost.login t _ ∅); last work with br_erefl; first set_solver. + wuntil Kfree go. run1. + wuntil interp go. + wapply (lock_ghost.logout t _ ∅); first set_solver. + step with br_erefl. + wapply (lock_ghost.logout t _ ∅); first set_solver. + go with br_erefl. Qed. cpp.spec "test_unique_lock()" as test_unique_lock_spec from source with (\post emp). Lemma test_unique_lock_ok : verify[source] "test_unique_lock()". Proof. - verify_spec; go. - - iExists emp; go. + verify_spec. + go. + iExists emp. + wuntil Econstructor go. + + ren_hyp g gname. + wapply current_thread_always_exists; work. + wapply (lock_ghost.login t g ∅); first set_solver. + wuntil Kfree go; run1; wuntil Kfree go. + wapply (lock_ghost.logout t g ∅); first set_solver. + go. Qed. - cpp.spec "test_unique_lock_defer()" as test_unique_lock_defer_spec from source with ( \prepost{q} _global "std::defer_lock" |-> defer_lock_t.R q \post emp). @@ -60,7 +123,15 @@ Section with_cpp. Lemma test_unique_lock_move_ok : verify[source] "test_unique_lock_move()". Proof. - verify_spec; go. - iExists emp; go. + verify_spec; go. iExists emp. + wuntil Econstructor go. + + ren_hyp g gname. + wapply current_thread_always_exists; work. + wapply (lock_ghost.login t g ∅); first set_solver. + + wuntil Kfree go. + wapply (lock_ghost.logout t g ∅); first set_solver. + go. Qed. End with_cpp.