From 292479e9c7a81fc5c2c95e48aa4588112ece7701 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 4 Feb 2026 19:39:56 +0100 Subject: [PATCH 1/8] One experiment instantiating instances --- rocq-brick-libstdcpp/proof/mutex/spec.v | 94 +++++++++++++++++++++---- 1 file changed, 82 insertions(+), 12 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 667765e..2cf67fe 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -1,3 +1,4 @@ +Require Import iris.base_logic.lib.ghost_map. Require Import skylabs.bi.tls_modalities. Require Import skylabs.bi.tls_modalities_rep. Require Import skylabs.bi.weakly_objective. @@ -83,44 +84,113 @@ Section with_cpp. End with_cpp. End mutex. + +#[export] Hint Opaque ghost_map_auth ghost_map_elem : sl_opacity. + Module recursive_mutex. (** <> <> owns the mutex <<γ>> <> times. *) - #[projections(primitive=no)] Class lockedG `{Σ : cpp_logic} := { + #[local] has_locked :: ghost_mapG _Σ thread_idT nat }. #[global] Arguments lockedG {_ _} Σ : assert. - Parameter locked : - ∀ `{Σ : cpp_logic, !lockedG Σ} - (γ : gname) (th : thread_idT) (n : nat), mpred. + sl.lock + Definition locked `{Σ : cpp_logic, !lockedG Σ} + (γ : gname) (th : thread_idT) (n : nat) : mpred := + ⎡ ghost_map_elem γ th (DfracOwn 1) n ⎤. - Parameter used_threads : - ∀ `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ} - (γ : gname) (s : gset thread_idT), mpred. + sl.lock + Definition used_threads + `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ} + (γ : gname) (s : gset thread_idT) : mpred := + ∃ m : gmap thread_idT nat, [| dom m = s |] ∗ ⎡ ghost_map_auth γ 1 m ⎤. #[only(timeless)] derive locked. #[only(timeless)] derive used_threads. + (* XXX upstream *) + #[only(fwd,bwd(l2r))] derive monPred_at_sep. + #[only(fwd,bwd(l2r))] derive monPred_at_embed. + #[only(fwd,bwd(l2r))] derive monPred_at_pure. + #[only(fwd,bwd(l2r))] derive monPred_at_only_provable. + (* #[only(fwd,bwd(l2r))] derive monPred_at_exist. *) + (* #[only(fwd)] derive monPred_at_exist. *) + Section locked_with_cpp. Context `{Σ : cpp_logic}. Context `{!lockedG Σ}. Context `{!HasStdThreads Σ}. - Axiom use_thread : ∀ th g s, + Lemma use_thread th g s : th ∉ s -> current_thread th ** used_threads g s |-- |==> used_threads g (s ∪ {[ th ]}) ** locked g th 0. + Proof. + rewrite used_threads.unlock locked.unlock => Hni. + constructor => i. + rewrite !(monPred_at_sep, monPred_at_embed, monPred_at_only_provable, monPred_at_exist, monPred_at_bupd). + iIntros "[#CT (%m & %Hdom & A)]". + set m' := <[ th := 0 ]> m. + iMod (ghost_map_insert th 0 with "[$]") as "[? $]". + { apply /not_elem_of_dom. by rewrite Hdom. } + iExists m'; subst m'. iModIntro. iFrame. + iIntros "!%". + by rewrite dom_insert_L Hdom comm_L. + Qed. - #[global] Declare Instance + Section with_ghost_map_inG. + #[local] Existing Instance ghost_map_inG. + + (* TODO: necessary? useful? *) + #[local] + Lemma locked_unseal γ th n : + locked γ th n ⊣⊢ + own γ (gmap_view.gmap_view_frag (V:=agreeR $ natO) th (DfracOwn 1) (to_agree n)). + Import iprop_own. + Proof. + rewrite locked.unlock ghost_map.ghost_map_elem_unseal /ghost_map.ghost_map_elem_def. + rewrite /own /=. + by rewrite has_own_monpred_eq /has_own_monpred_def has_own_iprop_eq /has_own_iprop_def /=. + Qed. + End with_ghost_map_inG. + + #[global] Instance locked_WeaklyObjective γ thr n : WeaklyObjective (PROP := iPropI _) (locked γ thr n). + Proof. rewrite locked.unlock. apply _. Qed. - Axiom locked_excl_same_thread : forall g th n m, + Lemma locked_excl_same_thread g th n m : locked g th n ** locked g th m |-- False. - Axiom locked_excl_different_thread : forall g th th' n m, - locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True. + Proof. + rewrite locked.unlock. + (* constructor => i. work. iStopProof. *) + iIntros "[A B]". iCombine "A B" gives %[HQV _]. + by exfalso. + Qed. + (* work. + cbv in HQV. + work. + constructor => i. + (* work. + Import monpred. *) + rewrite monPred_at_sep !monPred_at_embed monPred_at_pure. + by exfalso. + Qed. *) + + Lemma locked_excl_different_thread g th th' n m : + locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True. + Proof. + destruct (decide (th = th')) as [->|Hne]. { + rewrite locked_excl_same_thread. work. + } + rewrite locked.unlock. + constructor => i. + iIntros "[A B]". + work. + (* missing a restriction *) + Admitted. End locked_with_cpp. (* the mask of recursive_mutex *) From 4ab7768fb798d0abd2574da8bdec104a559d9d99 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 9 Jan 2026 01:47:00 +0100 Subject: [PATCH 2/8] (Unrelated) Automation WIP --- rocq-brick-libstdcpp/proof/mutex/spec.v | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 2cf67fe..f8bd320 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -524,18 +524,30 @@ Section with_cpp. ework with br_erefl. Qed. +(* Require Import bluerock.auto.cpp.prelude.proof. *) Lemma lock_spec_impl_lock_spec' : lock_spec |-- lock_spec'. Proof using MOD HOV HOU. apply specify_mono; work. + Import auto_frac. + iExists q, q'. - iExists _, q', (∃ t : acquire_state TT, [| acquire n t |] ∗ - ▷ acquireable g th t P)%I. - work. + iExists (∃ t, + [| acquire n t |] ∗ + (* token (lock_gname g) (cQp.scale (1 / 2) q') ∗ + a |-> R (lock_gname g) (cQp.scale (1 / 2) q) ∗ *) + ▷ acquireable g th t P)%I. wname [bi_wand] "W". wfocus (bi_wand _ _) "W". { work $usenamed=true. } + work. + (* wname [token] "T". + wname [R] "R". + wname [acquireable] "A". + (* About atomic_commit . *) + wfocus (atomic_commit _ _ _ _ _ _) "T R A". *) + (* iStopProof; work. *) iAcIntro; rewrite /commit_acc/=. rewrite inv_rmutex.unlock acquireable.unlock. iInv rmutex_namespace as (??) "(>Hn & Hcases)" "Hclose". @@ -553,7 +565,7 @@ Section with_cpp. iMod (own_update_2 with "Hn Hcase") as "(Hg & Hcase)"; first apply (excl_auth_update _ _ (1, th)). iMod "Hclose'" as "_". - wname [locked _ th _] "Hlocked". + wname [recursive_mutex.locked _ th _] "Hlocked". iMod ("Hclose" with "[$Hg $Hlocked //]") as "_". iMod (bi.later_exist_except_0 with "HP") as "(%args & HP)". iModIntro. @@ -566,7 +578,7 @@ Section with_cpp. iMod (own_update_2 with "Hn [$]") as "(Hg & Hcase)"; first apply (excl_auth_update _ _ (S (S n), th)). iMod "Hclose'" as "_". - wname [locked _ th _] "Hlocked". + wname [recursive_mutex.locked _ th _] "Hlocked". iMod ("Hclose" with "[$Hg $Hlocked //]") as "_". iModIntro. iExists (Held (S n) xs). work $usenamed=true. From 5dee1fe73333981e14f1255b8ca7a6318f8d199a Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 4 Feb 2026 19:10:16 +0100 Subject: [PATCH 3/8] Version 2: custom inductive --- rocq-brick-libstdcpp/proof/mutex/spec.v | 97 ++++++++++++++++++++++--- 1 file changed, 87 insertions(+), 10 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index f8bd320..72b7680 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -1,4 +1,3 @@ -Require Import iris.base_logic.lib.ghost_map. Require Import skylabs.bi.tls_modalities. Require Import skylabs.bi.tls_modalities_rep. Require Import skylabs.bi.weakly_objective. @@ -85,35 +84,97 @@ End with_cpp. End mutex. -#[export] Hint Opaque ghost_map_auth ghost_map_elem : sl_opacity. +Require Import iris.algebra.gset. +(* Alternative: prodO (gsetR thread_idT) (optionR (exclO (prodO thread_idTO natO)) *) +Canonical Structure cmraAltR := + prodR (gsetR thread_idTO) (optionR (exclR (prodO thread_idTO natO))). + +(* +Inductive locked_ghost := +| Zero (threads : gset thread_idT) : locked_ghost +| NonZero (threads : gset thread_idT) (owner : thread_idT) (count : nat) : locked_ghost +| Bot. + +NonZero . Zero = NonZero + +*) Module recursive_mutex. + Section build_camera. + (* #[global] Instance : Equiv locked_ghost := (=). + Instance : LeibnizEquiv locked_ghost. *) + (* Equiv A, PCore A, Op A, Valid A} := { *) + Canonical Structure locked_ghostO := leibnizO locked_ghost. + #[local] Instance locked_ghost_pcore : PCore locked_ghostO := λ a, + match a with + | Bot => Some Bot + | _ => Some (Zero ∅) + end. + + #[local] Instance locked_ghost_op : Op locked_ghostO := λ a b, + match a, b with + | Bot, _ => Bot + | _, Bot => Bot + | Zero s1, Zero s2 => Zero (s1 ∪ s2) + | Zero s1, NonZero s2 o c => NonZero (s1 ∪ s2) o c + | NonZero s1 o c, Zero s2 => NonZero (s1 ∪ s2) o c + | NonZero s1 o1 c1, NonZero s2 o2 c2 => + Bot + end. + + #[local] Instance locked_ghost_valid : Valid locked_ghostO := λ a, + match a with + | Bot => False + | Zero _ => True + | NonZero s o c => o ∈ s /\ c > 0 + (** TODO: is this right? *) + end. + + Lemma locked_ghost_mixin : RAMixin locked_ghostO. + Proof. + apply ra_total_mixin. + Admitted. + #[local] Instance locked_ghost_unit : Unit locked_ghostO := Zero ∅. + Lemma locked_ghost_ucmra_mixin : UcmraMixin locked_ghostO. + Admitted. + End build_camera. + (* Canonical Structure locked_ghostRA : ra := cmraR *) + Canonical Structure locked_ghostR : cmra := discreteR locked_ghost locked_ghost_mixin. + Canonical Structure locked_ghostUR : ucmra := Ucmra locked_ghost locked_ghost_ucmra_mixin. + + (* Not prodO thread_idTO natO. *) + (* A thread that has zero, locked γ th 0 does not even know which thread has non-0. *) + Canonical Structure cmraR := authR locked_ghostUR. (** <> <> owns the mutex <<γ>> <> times. *) Class lockedG `{Σ : cpp_logic} := { - #[local] has_locked :: ghost_mapG _Σ thread_idT nat + #[local] has_locked :: HasOwn mpredI cmraR }. #[global] Arguments lockedG {_ _} Σ : assert. sl.lock Definition locked `{Σ : cpp_logic, !lockedG Σ} (γ : gname) (th : thread_idT) (n : nat) : mpred := - ⎡ ghost_map_elem γ th (DfracOwn 1) n ⎤. + match n with + | 0 => own γ (◯ (Zero {[ th ]})) + | S n => own γ (◯ (NonZero {[ th ]} th n)) + end. + (* ⎡ ghost_map_elem γ th (DfracOwn 1) n ⎤. *) sl.lock Definition used_threads `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ} (γ : gname) (s : gset thread_idT) : mpred := - ∃ m : gmap thread_idT nat, [| dom m = s |] ∗ ⎡ ghost_map_auth γ 1 m ⎤. + ∃ t n, own γ (● (NonZero s t n)). #[only(timeless)] derive locked. #[only(timeless)] derive used_threads. (* XXX upstream *) - #[only(fwd,bwd(l2r))] derive monPred_at_sep. + (* #[only(fwd,bwd(l2r))] derive monPred_at_sep. #[only(fwd,bwd(l2r))] derive monPred_at_embed. #[only(fwd,bwd(l2r))] derive monPred_at_pure. - #[only(fwd,bwd(l2r))] derive monPred_at_only_provable. + #[only(fwd,bwd(l2r))] derive monPred_at_only_provable. *) (* #[only(fwd,bwd(l2r))] derive monPred_at_exist. *) (* #[only(fwd)] derive monPred_at_exist. *) @@ -128,9 +189,25 @@ Module recursive_mutex. |==> used_threads g (s ∪ {[ th ]}) ** locked g th 0. Proof. rewrite used_threads.unlock locked.unlock => Hni. - constructor => i. - rewrite !(monPred_at_sep, monPred_at_embed, monPred_at_only_provable, monPred_at_exist, monPred_at_bupd). - iIntros "[#CT (%m & %Hdom & A)]". + iIntros "[#CT (% & % & A)]". + iMod (own_update with "A") as "?". + About own_update. + { + apply (auth_update_alloc (NonZero (s ∪ {[ th ]}) th 0)). +(* own_update : +∀ {PROP : bi} {BiBUpd0 : BiBUpd PROP} {A : cmra} {HasOwn0 : HasOwn PROP A}, +HasOwnUpd PROP A → ∀ (γ : gname) (a a' : A), a ~~> a' → own γ a ⊢ |==> own γ a' *) + + as "(? & ?)"; + first ( + apply auth_update; + destruct n0; simpl; + try (apply (auth_update_alloc (NonZero (s ∪ {[ th ]}) th 0)); + [apply singleton_subseteq_l|]); + apply (auth_update_local_update _ (Zero (s ∪ {[ th ]}))); + simpl; constructor; split; [set_solver|lia] + ). + (* iIntros "[#CT (%th & %n & A)]". *) set m' := <[ th := 0 ]> m. iMod (ghost_map_insert th 0 with "[$]") as "[? $]". { apply /not_elem_of_dom. by rewrite Hdom. } From 8ded098cdcb90fc31890424df59eb0e9c5550721 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 4 Feb 2026 19:16:04 +0100 Subject: [PATCH 4/8] Body of version 3 --- rocq-brick-libstdcpp/proof/mutex/spec.v | 75 ++++++------------------- 1 file changed, 18 insertions(+), 57 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 72b7680..df54fcc 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -85,63 +85,20 @@ End mutex. Require Import iris.algebra.gset. -(* Alternative: prodO (gsetR thread_idT) (optionR (exclO (prodO thread_idTO natO)) *) -Canonical Structure cmraAltR := - prodR (gsetR thread_idTO) (optionR (exclR (prodO thread_idTO natO))). -(* -Inductive locked_ghost := -| Zero (threads : gset thread_idT) : locked_ghost -| NonZero (threads : gset thread_idT) (owner : thread_idT) (count : nat) : locked_ghost -| Bot. - -NonZero . Zero = NonZero +Module recursive_mutex. + (* + Inductive locked_ghost := + | Zero (threads : gset thread_idT) : locked_ghost + | NonZero (threads : gset thread_idT) (owner : thread_idT) (count : nat) : locked_ghost + | Bot. -*) + NonZero . Zero = NonZero -Module recursive_mutex. - Section build_camera. - (* #[global] Instance : Equiv locked_ghost := (=). - Instance : LeibnizEquiv locked_ghost. *) - (* Equiv A, PCore A, Op A, Valid A} := { *) - Canonical Structure locked_ghostO := leibnizO locked_ghost. - #[local] Instance locked_ghost_pcore : PCore locked_ghostO := λ a, - match a with - | Bot => Some Bot - | _ => Some (Zero ∅) - end. - - #[local] Instance locked_ghost_op : Op locked_ghostO := λ a b, - match a, b with - | Bot, _ => Bot - | _, Bot => Bot - | Zero s1, Zero s2 => Zero (s1 ∪ s2) - | Zero s1, NonZero s2 o c => NonZero (s1 ∪ s2) o c - | NonZero s1 o c, Zero s2 => NonZero (s1 ∪ s2) o c - | NonZero s1 o1 c1, NonZero s2 o2 c2 => - Bot - end. - - #[local] Instance locked_ghost_valid : Valid locked_ghostO := λ a, - match a with - | Bot => False - | Zero _ => True - | NonZero s o c => o ∈ s /\ c > 0 - (** TODO: is this right? *) - end. - - Lemma locked_ghost_mixin : RAMixin locked_ghostO. - Proof. - apply ra_total_mixin. - Admitted. - #[local] Instance locked_ghost_unit : Unit locked_ghostO := Zero ∅. - Lemma locked_ghost_ucmra_mixin : UcmraMixin locked_ghostO. - Admitted. - End build_camera. - (* Canonical Structure locked_ghostRA : ra := cmraR *) - Canonical Structure locked_ghostR : cmra := discreteR locked_ghost locked_ghost_mixin. - Canonical Structure locked_ghostUR : ucmra := Ucmra locked_ghost locked_ghost_ucmra_mixin. + *) + Canonical Structure locked_ghostUR : ucmra := + prodR (gsetR thread_idTO) (optionR (exclR (prodO thread_idTO natO))). (* Not prodO thread_idTO natO. *) (* A thread that has zero, locked γ th 0 does not even know which thread has non-0. *) Canonical Structure cmraR := authR locked_ghostUR. @@ -156,16 +113,20 @@ Module recursive_mutex. Definition locked `{Σ : cpp_logic, !lockedG Σ} (γ : gname) (th : thread_idT) (n : nat) : mpred := match n with - | 0 => own γ (◯ (Zero {[ th ]})) - | S n => own γ (◯ (NonZero {[ th ]} th n)) + | 0 => own γ (◯ ({[ th ]}, None)) + | S n => own γ (◯ ({[ th ]}, Excl' (th, n))) end. - (* ⎡ ghost_map_elem γ th (DfracOwn 1) n ⎤. *) sl.lock Definition used_threads `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ} (γ : gname) (s : gset thread_idT) : mpred := - ∃ t n, own γ (● (NonZero s t n)). + ∃ n, + match n with + | 0 => own γ (● (s, None)) + | S n => ∃ t, own γ (● (s, Excl' (t, n))) + end. + (* own γ (● (s, (NonZero s t n)). *) #[only(timeless)] derive locked. #[only(timeless)] derive used_threads. From fc03ca2984ec439307238c36c541e9b2f0ca9cc1 Mon Sep 17 00:00:00 2001 From: rinshankaihou Date: Wed, 11 Feb 2026 09:32:30 +0000 Subject: [PATCH 5/8] fix use_thread --- rocq-brick-libstdcpp/proof/mutex/spec.v | 57 ++++++++++++++----------- 1 file changed, 33 insertions(+), 24 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index df54fcc..d52010a 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -144,37 +144,46 @@ Module recursive_mutex. Context `{!lockedG Σ}. Context `{!HasStdThreads Σ}. + Instance HOU : HasOwnUpd mpredI cmraR. + Admitted. + Lemma use_thread th g s : th ∉ s -> current_thread th ** used_threads g s |-- |==> used_threads g (s ∪ {[ th ]}) ** locked g th 0. Proof. rewrite used_threads.unlock locked.unlock => Hni. - iIntros "[#CT (% & % & A)]". - iMod (own_update with "A") as "?". - About own_update. + iIntros "[#CT (% & A)]". + destruct n. { - apply (auth_update_alloc (NonZero (s ∪ {[ th ]}) th 0)). -(* own_update : -∀ {PROP : bi} {BiBUpd0 : BiBUpd PROP} {A : cmra} {HasOwn0 : HasOwn PROP A}, -HasOwnUpd PROP A → ∀ (γ : gname) (a a' : A), a ~~> a' → own γ a ⊢ |==> own γ a' *) - - as "(? & ?)"; - first ( - apply auth_update; - destruct n0; simpl; - try (apply (auth_update_alloc (NonZero (s ∪ {[ th ]}) th 0)); - [apply singleton_subseteq_l|]); - apply (auth_update_local_update _ (Zero (s ∪ {[ th ]}))); - simpl; constructor; split; [set_solver|lia] - ). - (* iIntros "[#CT (%th & %n & A)]". *) - set m' := <[ th := 0 ]> m. - iMod (ghost_map_insert th 0 with "[$]") as "[? $]". - { apply /not_elem_of_dom. by rewrite Hdom. } - iExists m'; subst m'. iModIntro. iFrame. - iIntros "!%". - by rewrite dom_insert_L Hdom comm_L. + iMod (own_update with "A") as "H". + { apply (auth_update_alloc _ (s ∪ {[th]}, None) (s ∪ {[th]}, None)). + apply prod_local_update_1. + apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. } + iDestruct "H" as "[● ◯]". + iEval ( + replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) + ) in "◯". + iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". + iDestruct (own_op with "◯") as "[Hs $]". + iModIntro; iExists 0. iFrame. + } + { + iDestruct "A" as "(%t & A)". + iMod (own_update with "A") as "H". + { apply (auth_update_alloc _ (s ∪ {[th]}, Excl' (t, n)) (s ∪ {[th]}, None)). + apply prod_local_update_1. + apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. + } + iDestruct "H" as "[● ◯]". + iEval ( + replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) + ) in "◯". + iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". + iDestruct (own_op with "◯") as "[Hs $]". + iModIntro; iExists (S n). + iFrame. + } Qed. Section with_ghost_map_inG. From a133c62f88a3586069f70a7022362fa7ee75f838 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 11 Feb 2026 18:02:03 +0100 Subject: [PATCH 6/8] Fix lockedG assumptions --- rocq-brick-libstdcpp/proof/mutex/spec.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index d52010a..95b5d9b 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -105,7 +105,8 @@ Module recursive_mutex. (** <> <> owns the mutex <<γ>> <> times. *) Class lockedG `{Σ : cpp_logic} := { - #[local] has_locked :: HasOwn mpredI cmraR + #[local] has_locked :: HasOwn (iPropI _Σ) cmraR; + #[local] has_locked_upd :: HasOwnUpd (iPropI _Σ) cmraR }. #[global] Arguments lockedG {_ _} Σ : assert. @@ -144,9 +145,6 @@ Module recursive_mutex. Context `{!lockedG Σ}. Context `{!HasStdThreads Σ}. - Instance HOU : HasOwnUpd mpredI cmraR. - Admitted. - Lemma use_thread th g s : th ∉ s -> current_thread th ** used_threads g s |-- From 2cb4fb42515126f90e41630c4f54ae8df7979f6c Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 11 Feb 2026 18:02:22 +0100 Subject: [PATCH 7/8] Small proof tweaks --- rocq-brick-libstdcpp/proof/mutex/spec.v | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 95b5d9b..1794870 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -154,33 +154,31 @@ Module recursive_mutex. iIntros "[#CT (% & A)]". destruct n. { - iMod (own_update with "A") as "H". + iMod (own_update with "A") as "[● ◯]". { apply (auth_update_alloc _ (s ∪ {[th]}, None) (s ∪ {[th]}, None)). apply prod_local_update_1. apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. } - iDestruct "H" as "[● ◯]". iEval ( replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) ) in "◯". iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". - iDestruct (own_op with "◯") as "[Hs $]". - iModIntro; iExists 0. iFrame. + iDestruct "◯" as "[Hs $]". + iModIntro; iExists 0. iFrame. } { - iDestruct "A" as "(%t & A)". - iMod (own_update with "A") as "H". + iDestruct "A" as "(%t & A)". + iMod (own_update with "A") as "[● ◯]". { apply (auth_update_alloc _ (s ∪ {[th]}, Excl' (t, n)) (s ∪ {[th]}, None)). apply prod_local_update_1. apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. - } - iDestruct "H" as "[● ◯]". + } iEval ( replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) ) in "◯". iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". - iDestruct (own_op with "◯") as "[Hs $]". + iDestruct "◯" as "[Hs $]". iModIntro; iExists (S n). - iFrame. + iFrame. } Qed. From ee95cb7dc031df38a77576dfcf006b1f3e6dcaa5 Mon Sep 17 00:00:00 2001 From: rinshankaihou Date: Wed, 18 Feb 2026 17:58:54 +0000 Subject: [PATCH 8/8] fill in the recursive mutex ghost state --- rocq-brick-libstdcpp/proof/mutex/spec.v | 85 +++++++++---------------- 1 file changed, 31 insertions(+), 54 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 1794870..79fcf89 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -98,25 +98,27 @@ Module recursive_mutex. *) Canonical Structure locked_ghostUR : ucmra := - prodR (gsetR thread_idTO) (optionR (exclR (prodO thread_idTO natO))). + prodR (gset_disjR thread_idTO) (optionR (exclR (prodO thread_idTO natO))). (* Not prodO thread_idTO natO. *) (* A thread that has zero, locked γ th 0 does not even know which thread has non-0. *) - Canonical Structure cmraR := authR locked_ghostUR. + Canonical Structure locked_cmraR := authR locked_ghostUR. (** <> <> owns the mutex <<γ>> <> times. *) Class lockedG `{Σ : cpp_logic} := { - #[local] has_locked :: HasOwn (iPropI _Σ) cmraR; - #[local] has_locked_upd :: HasOwnUpd (iPropI _Σ) cmraR + #[local] has_locked :: HasOwn (iPropI _Σ) locked_cmraR; + #[local] has_locked_upd :: HasOwnUpd (iPropI _Σ) locked_cmraR; + #[local] has_locked_valid :: HasOwnValid (iPropI _Σ) locked_cmraR }. #[global] Arguments lockedG {_ _} Σ : assert. sl.lock Definition locked `{Σ : cpp_logic, !lockedG Σ} (γ : gname) (th : thread_idT) (n : nat) : mpred := - match n with - | 0 => own γ (◯ ({[ th ]}, None)) - | S n => own γ (◯ ({[ th ]}, Excl' (th, n))) - end. + own γ (◯ (GSet {[ th ]}, + match n with + | 0 => None + | S n => Excl' (th, n) + end)). sl.lock Definition used_threads @@ -124,10 +126,9 @@ Module recursive_mutex. (γ : gname) (s : gset thread_idT) : mpred := ∃ n, match n with - | 0 => own γ (● (s, None)) - | S n => ∃ t, own γ (● (s, Excl' (t, n))) + | 0 => own γ (● (GSet s, None)) + | S n => ∃ t, own γ (● (GSet s, Excl' (t, n))) end. - (* own γ (● (s, (NonZero s t n)). *) #[only(timeless)] derive locked. #[only(timeless)] derive used_threads. @@ -155,49 +156,30 @@ Module recursive_mutex. destruct n. { iMod (own_update with "A") as "[● ◯]". - { apply (auth_update_alloc _ (s ∪ {[th]}, None) (s ∪ {[th]}, None)). + { apply (auth_update_alloc _ (GSet ({[th]} ∪ s), None) (GSet ({[th]}), None)). apply prod_local_update_1. - apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. } + apply gset_disj_alloc_empty_local_update. set_solver. } iEval ( replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) ) in "◯". - iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". - iDestruct "◯" as "[Hs $]". - iModIntro; iExists 0. iFrame. + iFrame. + iModIntro; iExists 0. rewrite comm_L //. } { iDestruct "A" as "(%t & A)". iMod (own_update with "A") as "[● ◯]". - { apply (auth_update_alloc _ (s ∪ {[th]}, Excl' (t, n)) (s ∪ {[th]}, None)). + { apply (auth_update_alloc _ (GSet ({[th]} ∪ s), Excl' (t, n)) (GSet {[th]}, None)). apply prod_local_update_1. - apply (gset_local_update _ _ (s ∪ {[th]})). set_solver. + apply gset_disj_alloc_empty_local_update. set_solver. } iEval ( replace None with (None ⋅ None:(optionR (exclR (prodO thread_idTO natO)))) ) in "◯". - iEval (rewrite -gset_op pair_op auth_frag_op) in "◯". - iDestruct "◯" as "[Hs $]". - iModIntro; iExists (S n). iFrame. + iModIntro; iExists (S n). rewrite comm_L //. iFrame. } Qed. - Section with_ghost_map_inG. - #[local] Existing Instance ghost_map_inG. - - (* TODO: necessary? useful? *) - #[local] - Lemma locked_unseal γ th n : - locked γ th n ⊣⊢ - own γ (gmap_view.gmap_view_frag (V:=agreeR $ natO) th (DfracOwn 1) (to_agree n)). - Import iprop_own. - Proof. - rewrite locked.unlock ghost_map.ghost_map_elem_unseal /ghost_map.ghost_map_elem_def. - rewrite /own /=. - by rewrite has_own_monpred_eq /has_own_monpred_def has_own_iprop_eq /has_own_iprop_def /=. - Qed. - End with_ghost_map_inG. - #[global] Instance locked_WeaklyObjective γ thr n : WeaklyObjective (PROP := iPropI _) (locked γ thr n). @@ -207,21 +189,14 @@ Module recursive_mutex. locked g th n ** locked g th m |-- False. Proof. rewrite locked.unlock. - (* constructor => i. work. iStopProof. *) - iIntros "[A B]". iCombine "A B" gives %[HQV _]. - by exfalso. + iIntros "[A B]". + iDestruct (own_valid_2 with "A B") as "%". + rewrite -auth_frag_op -pair_op auth_frag_valid in H. + destruct H. + rewrite /= gset_disj_valid_op /= in H. + set_solver. Qed. - (* work. - cbv in HQV. - work. - constructor => i. - (* work. - Import monpred. *) - rewrite monPred_at_sep !monPred_at_embed monPred_at_pure. - by exfalso. - Qed. *) - Lemma locked_excl_different_thread g th th' n m : locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True. Proof. @@ -229,11 +204,13 @@ Module recursive_mutex. rewrite locked_excl_same_thread. work. } rewrite locked.unlock. - constructor => i. iIntros "[A B]". - work. - (* missing a restriction *) - Admitted. + destruct n, m; try auto. + iDestruct (own_valid_2 with "A B") as "%". + rewrite -auth_frag_op -pair_op auth_frag_valid in H. + destruct H as [_ H]. done. + Qed. + End locked_with_cpp. (* the mask of recursive_mutex *)