New ghost state for mutex spec & implementation; give up `user` ghost state. by dkxb · Pull Request #173 · SkyLabsAI/brick-libcpp

dkxb · 2026-09-09T22:11:04Z

Conflicts with #167; maybe easiest to cherry pick from #167 and then close #167 at this point.

Currently, only rocq-brick-libstdcpp/proof/mutex/spec/mutex.v and rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp_proof.v compile.

There are so many commits, and it might be easier to review the diff of the two branches instead of reading the commits.

The changes mostly include these aspects:

A MUTEX_PREDS interface, which includes predicates that mutex specs need and some of their rules. The proof that the mutex custom implementation meets the spec cannot solely depend on the interface; e.g., the instantiation of not_locked includes points-to of m_owner, and it needs to be exposed during verification.
The instantiation of MUTEX_PREDS include 3 ghost state modules (defined in lock_ghost2.v, see comments in the file for how these modules work):
- MUTEX_TOKENS defines token/given_token. This is for making sure no thread is holding the lock when destructor is called.
- MUTEX_SETS defines my_mutexes for making sure a thread only gets resource once from a mutex invariant before it unlocks.
- OWNER_TID for remembering the owner thread ID of the mutex.

--
Fix #153, #174, #154.

skylabs-ai-ci · 2026-09-09T22:23:18Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	ke/mutex_impl	72b7dde	e4cbb0f	main	be863c8	#173

Passive Repos

Repo	Job Branch	Job Commit
./	main	db1581e
fmdeps/BRiCk/	main	e819c36
fmdeps/auto/	main	bc4c71e
fmdeps/auto-docs/	main	6490c5f
bluerock/NOVA/	skylabs-proof	f3533d2
bluerock/bhv/	skylabs-main	e37df58
fmdeps/ci/	main	e1ec839
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	227bb83
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	5c3d0ab
vendored/vsrocq/	skylabs-main	ee79e7a

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	${\color{red}7}$	0	7
Warnings	91	${\color{red}2}$	${\color{green}2}$	91

Performance

Relative	Master	MR	Change	Filename
+0.96%	198198.0	200098.2	+1900.2	total
-0.52%	1048.1	-	-1048.1	├ disappeared files (13)
+1.46%	-	2936.7	+2936.7	├ newly appeared files (10)
+0.01%	197149.8	197161.5	+11.7	└ common files
-0.00%	53108.6	53108.4	-0.2	├ translation units
+0.01%	144041.3	144053.2	+11.9	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
+41.01%	31.2	44.0	+12.8	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v

+0.96%	198198.0	200098.2	+1900.2	total
-0.52%	1048.1	-	-1048.1	├ disappeared files (13)
+1.46%	-	2936.7	+2936.7	├ newly appeared files (10)
+0.01%	197149.8	197161.5	+11.7	└ common files
-0.00%	53108.6	53108.4	-0.2	├ translation units
+0.01%	144041.3	144053.2	+11.9	└ proofs and tests

pgiarrusso-sl · 2026-09-10T16:11:18Z

+      (mp : ptr * mutex.gname * Qp * Qp) (q : cQp.t) (P : mpred) : Rep :=
    structR "std::lock_guard<std::mutex>" q **
-    let '(mp, g, q') := mp in
+    let '(mp, g, q', _) := mp in


Why are we adding a fraction that we're throwing away.

It is a mistake and I'll delete it.

skylabs-ai-ci · 2026-09-10T16:22:33Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	ke/mutex_impl	7f96c5d	250308e	main	be863c8	#173

Passive Repos

Repo	Job Branch	Job Commit
./	main	db1581e
fmdeps/BRiCk/	main	e819c36
fmdeps/auto/	main	0d2d68d
fmdeps/auto-docs/	main	6490c5f
bluerock/NOVA/	skylabs-proof	f3533d2
bluerock/bhv/	skylabs-main	e37df58
fmdeps/ci/	main	e1ec839
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	227bb83
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	5c3d0ab
vendored/vsrocq/	skylabs-main	ee79e7a

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	${\color{red}7}$	0	7
Warnings	91	${\color{red}2}$	${\color{green}2}$	91

Performance

Relative	Master	MR	Change	Filename
+0.96%	198220.5	200120.6	+1900.1	total
-0.52%	1048.2	-	-1048.2	├ disappeared files (13)
+1.46%	-	2936.7	+2936.7	├ newly appeared files (10)
+0.01%	197172.3	197183.9	+11.7	└ common files
-0.00%	53108.6	53108.4	-0.2	├ translation units
+0.01%	144063.7	144075.6	+11.9	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-1.95%	51.3	50.3	-1.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v
+41.01%	31.2	44.0	+12.8	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v

+0.96%	198220.5	200120.6	+1900.1	total
-0.52%	1048.2	-	-1048.2	├ disappeared files (13)
+1.46%	-	2936.7	+2936.7	├ newly appeared files (10)
+0.01%	197172.3	197183.9	+11.7	└ common files
-0.00%	53108.6	53108.4	-0.2	├ translation units
+0.01%	144063.7	144075.6	+11.9	└ proofs and tests

pgiarrusso-sl · 2026-09-17T08:24:42Z

+(** Specialize the reusable specs to the standard mutex representation and
+    bind them to their C++ names. *)
+Module StdMutex (Preds : MUTEX_PREDS with Definition cpp_ty := "std::mutex"%cpp_type).
+  Include Preds.


Worth a closer look.

The idea with MUTEX_PREDS is that, since multiple mutex specs depend on the same locked/not_locked etc, by wrapping them up in a module, we enforce the specs use the same locked .

So the mutex_spec module plus the MUTEX_PREDS module type is the complete mutex interface, and programs that use mutexes only need to import them (specs in mutex_spec and rules in MUTEX_PREDS).

A mutex implementation (i.e., custom_mutex_hpp_proof.v) is then a proof that the program meets specs in mutex_spec, with a specific MUTEX_PREDS instance.

pgiarrusso-sl · 2026-09-17T08:24:46Z

+  Include Preds.
+  #[global] Hint Opaque token not_locked locked R : sl_opacity.
+
+  Module Spec := mutex_spec Preds.


Worth a closer look.

pgiarrusso-sl · 2026-09-17T08:27:58Z

+      try_lock_lockable cpp_ty (fun q gP => R gP.1 q gP.2).
+
+    Lemma try_lock_spec_equiv_try_lock_spec_alt
+        (Htry_lock : requirements.do_try_lock cpp_ty = do_try_lock) this xs K :


Htry_lock seems odd — this should just be unfolding mutex_lockable?

pgiarrusso-sl · 2026-09-17T16:11:03Z

+  #[global] Declare Instance wp_fptr_objective (f : ptr) (Q : mpred)
+      `{!WeaklyObjective Q} :
+    ObjectiveWith threadTI
+      (wp_fptr (σ.(genv_tu).(types)) entry_type f [] (fun _ => Q)).


pgiarrusso-sl · 2026-09-17T16:36:28Z

+  Definition entry_type : type := Tfunction (FunctionType Tvoid []).
+
+  #[global] Declare Instance wp_fptr_objective (f : ptr) (Q : mpred)
+      `{!WeaklyObjective Q} :


I'd guess nothing consumes this, or I'm curious where.

Also figure out the mix of WeaklyObjective and ObjectiveWith.

pgiarrusso-sl · 2026-09-17T18:24:24Z

+     \pre{Q : mpred} [| WeaklyObjective Q |]
+     \pre
+       (∀ child,
+          (MutexSets.my_mutexes γ child (coPset.CoPset ⊤) -*


Here we bundle a specific ghost update, but we agreed we could abstract over a fancy update of the right shape instead.

pgiarrusso-sl · 2026-09-24T09:58:41Z


- *)
+(** FIXME don't need StdAtomicSpecs *)
+Module StdAtomicSpecs := RecursiveMutexAtomicSpecs StdRecursiveMutexName.


Nit: StdAtomicSpecs should be the name for std::atomic specs

dkxb · 2026-09-29T04:21:11Z

Updated recursive_mutex specs to use my_mutexes as well.
Spec interface change: recursive_mutex now mainly exposes these predicates:

brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v

Lines 101 to 128 in 150e85a

    
             (** Ghost name of the ghost state that keeps track of a pool of gnames for each thread. *) 
        
             Parameter pool_name : gname -> iprop.gname. 
        
             Parameter rmutex_inv_namespace : gname -> namespace. 
        
             #[global] Declare Instance sets_G `{Σ : cpp_logic, !G Σ} : MutexSets.G Σ. 
        
             Parameter token : forall `{Σ : cpp_logic, !G Σ}, gname -> cQp.t -> mpred. 
        
             #[global] Declare Instance token_fractional 
        
                 `{Σ : cpp_logic, !G Σ} g : CFractional (token g). 
        
             #[global] Declare Instance token_timeless 
        
                 `{Σ : cpp_logic, !G Σ} g qt : Timeless (token g qt). 
        
             Parameter given_token : forall `{Σ : cpp_logic, !G Σ}, 
        
               gname -> cQp.t -> thread_idT -> nat -> mpred. 
        
             Definition acquireable `{Σ : cpp_logic, !G Σ} 
        
                 {HAS_THREADS : HasStdThreads Σ} (g : gname) (qt : cQp.t) (th : thread_idT) 
        
                 {TT : tele} (s : acquire_state TT) (P : TT -t> mpred) : mpred := 
        
               current_thread th ** 
        
               match s with 
        
               | NotHeld => token g qt ** MutexSets.my_mutexes (pool_name g) th 
        
                   (CoPset $ ↑rmutex_inv_namespace g) 
        
               | Held n xs => given_token g qt th n ** tele_app P xs 
        
               end. 
        
             (* abstract predicate of owership of a recursive mutex that protects some 
        
                resource [P], e.g. in the form of [inv _ P]. Note that it only represents 
        
                the mutex data structure, not the ownership of [P]. *) 
        
             Parameter R : forall `{Σ : cpp_logic, !G Σ} 
        
               {HAS_THREADS : HasStdThreads Σ} {σ : genv}, 
        
               gname -> cQp.t -> mpred -> Rep.

R g 1 is the rep predicate for the recursive_mutex (notice it is not tied to any thread); token/given_token for preventing destruction while holding the lock. A thread can get the acqurieable handle with a fraction of R and token, plus my_mutexes _ th N: https://github.com/SkyLabsAI/brick-libcpp/blob/150e85ae6aa155edba33f5ffe756283432f09356/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v#L141-148

The specs are now:

brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v

Lines 171 to 195 in 150e85a

    
           Definition ctor_spec : ptr -> WpSpec mpred val val := 
        
             (\this this 
        
              \pre{pool N TT P xs} |> tele_app (TT := TT) P xs 
        
              \require ∀ xs, Objective (tele_app P xs) 
        
              \post Exists g, 
        
                [| pool_name g = pool /\ rmutex_inv_namespace g = N |] ** 
        
                this |-> R g 1$m (∃ xs, tele_app P xs) ** token g 1$m). 
        
           Definition dtor_spec : ptr -> WpSpec mpred val val := 
        
             (\this this 
        
              \pre{g TT P} this |-> R g 1 (∃ xs, tele_app (TT := TT) P xs) 
        
              \pre token g 1$m 
        
              \post |> (Exists xs, tele_app (TT := TT) P xs)). 
        
           Definition lock_spec : ptr -> WpSpec mpred val val := 
        
             (\this this 
        
              \prepost{g TT P q} this |-> R g q (∃ xs, tele_app (TT := TT) P xs) 
        
              \pre{qt th n} acquireable g qt th n P 
        
              \post Exists n', [| acquire n n' |] ** ▷ acquireable g qt th n' P). 
        
           Definition unlock_spec : ptr -> WpSpec mpred val val := 
        
             (\this this 
        
              \prepost{g TT P q} this |-> R g q (∃ xs, tele_app (TT := TT) P xs) 
        
              \pre{qt th n args} acquireable g qt th (Held n args) P 
        
              \post acquireable g qt th (release $ Held n args) P).

dkxb · 2026-09-29T04:29:52Z

Added a client of mutexes and its proof which is supposed to show that my_mutexes gives a data structure containing a mutex in its implementation a good abstraction.

Similar to the recursive mutex, the register rule

brick-libcpp/rocq-brick-libstdcpp/test/mutex/transfer_with_mutex_cpp_proof.v

Lines 121 to 124 in 150e85a

    
           Lemma account_register_thread (this : ptr) gpool N q th : 
        
             current_thread th ** this |-> accountR gpool N q ** 
        
             MutexSets.my_mutexes gpool th (coPset.CoPset (↑N)) ⊣⊢ 
        
             this |-> account_acquireableR gpool N q th.

allows a thread to turn a fraction of the data structure rep accountR and its my_mutexes to some user handle account_acquireableR, which can then be used with C::call(). (see spec)

…d transfer_with_mutex.cpp

…n that we need

… an instance mutex_set_G, following the invariant_name pattern in wsat.v in iris

…proof; require mutex namespace to not be [nroot]

…ow use the same ghost state to track the owner thread and how much [token] it deposits

… the module

…racR

…x/libcpp_tests

skylabs-ai-ci · 2026-10-29T17:01:29Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	ke/mutex_impl	661ab5f	19ace83	main	dc3d407	#173

Passive Repos

Repo	Job Branch	Job Commit
./	main	9537067
fmdeps/BRiCk/	main	072037a
fmdeps/auto/	main	a2ac8f7
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	02f6828
bluerock/bhv/	skylabs-main	b5a9d07
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	53fde9a
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	285745a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	ba29dba
fmdeps/skylabs-fm/	main	d2bc589
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	${\color{red}4}$	0	4
Warnings	75	${\color{red}1}$	${\color{green}2}$	74

Performance

Relative	Master	MR	Change	Filename
+0.49%	198895.8	199868.9	+973.2	total
-0.60%	1202.7	-	-1202.7	├ disappeared files (10)
+1.08%	-	2161.8	+2161.8	├ newly appeared files (10)
+0.01%	197693.0	197707.1	+14.1	└ common files
+0.01%	49587.4	49590.0	+2.6	├ translation units
+0.01%	148105.6	148117.1	+11.5	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-15.18%	16.9	14.3	-2.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
-14.72%	26.4	22.5	-3.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
-0.22%	601.2	599.9	-1.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_recursive_mutex_hpp.v
+1.80%	169.2	172.2	+3.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp.v
+1.86%	143.5	146.1	+2.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp_templates.v
+2.27%	48.2	49.3	+1.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
+8.48%	31.2	33.9	+2.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/shared_mutex/shared_mutex.v
+15.16%	29.0	33.4	+4.4	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+30.98%	22.5	29.5	+7.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/shared_mutex/test_cpp_proof.v

+0.49%	198895.8	199868.9	+973.2	total
-0.60%	1202.7	-	-1202.7	├ disappeared files (10)
+1.08%	-	2161.8	+2161.8	├ newly appeared files (10)
+0.01%	197693.0	197707.1	+14.1	└ common files
+0.01%	49587.4	49590.0	+2.6	├ translation units
+0.01%	148105.6	148117.1	+11.5	└ proofs and tests

skylabs-ai-ci · 2026-10-29T17:19:30Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	ke/mutex_impl	a41fe72	6f962c9	main	dc3d407	#173

Passive Repos

Repo	Job Branch	Job Commit
./	main	9537067
fmdeps/BRiCk/	main	072037a
fmdeps/auto/	main	a2ac8f7
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	02f6828
bluerock/bhv/	skylabs-main	b5a9d07
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	53fde9a
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	285745a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	ba29dba
fmdeps/skylabs-fm/	main	d2bc589
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	75	${\color{red}5}$	${\color{green}1}$	79

Performance

Relative	Master	MR	Change	Filename
+1.54%	198895.7	201963.4	+3067.7	total
+1.35%	-	2733.8	+2733.8	├ newly appeared files (14)
+0.17%	198895.7	199229.6	+333.9	└ common files
+0.01%	49587.4	49590.0	+2.6	├ translation units
+0.22%	149308.3	149639.6	+331.3	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-49.42%	64.0	32.4	-31.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v
-15.18%	16.9	14.3	-2.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
-14.72%	26.4	22.5	-3.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
-0.22%	601.2	599.9	-1.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_recursive_mutex_hpp.v
+1.80%	169.2	172.2	+3.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp.v
+1.86%	143.5	146.1	+2.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp_templates.v
+2.27%	48.2	49.3	+1.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
+3.05%	62.4	64.3	+1.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v
+7.63%	145.9	157.0	+11.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
+8.48%	31.2	33.9	+2.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/shared_mutex/shared_mutex.v
+15.16%	29.0	33.4	+4.4	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+30.98%	22.5	29.5	+7.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/shared_mutex/test_cpp_proof.v
+690.41%	23.7	187.7	+163.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v
+1464.79%	11.9	185.5	+173.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_recursive_mutex_hpp_proof.v

+1.54%	198895.7	201963.4	+3067.7	total
+1.35%	-	2733.8	+2733.8	├ newly appeared files (14)
+0.17%	198895.7	199229.6	+333.9	└ common files
+0.01%	49587.4	49590.0	+2.6	├ translation units
+0.22%	149308.3	149639.6	+331.3	└ proofs and tests

Written by Codex. Add prominent per-file adaptation notices while preserving the upstream LLVM license headers and source provenance.

Written by Codex. Make id_hash a C++17 inline variable and guard the entire header. Add a Dune runtest regression that includes the header twice, links two translation units, checks the shared sentinel address, and exercises recursive locking.

Written by Codex. Document that the standard Hash requirements allow collisions and that owner discrimination requires a target-specific injectivity argument, including the default thread ID, or a collision-free identity.

Written by Codex. Check the existing generic constructor contract with distinct lock and try_lock effects, and specialize its false-flag premises to the incorrect both-true postcondition. Add a native libstdc++ CountingMutex witness under Dune runtest and document the diagnostic scope and unresolved contract issue.

skylabs-ai-ci · 2026-10-29T20:31:38Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	ke/mutex_impl	61ae683	57bce7f	main	dc3d407	#173

Passive Repos

Repo	Job Branch	Job Commit
./	main	9537067
fmdeps/BRiCk/	main	f98bd89
fmdeps/auto/	main	c46a785
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	b6f875a
bluerock/bhv/	skylabs-main	8c30fef
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	53fde9a
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	285745a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	ba29dba
fmdeps/skylabs-fm/	main	d2bc589
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	75	${\color{red}5}$	${\color{green}1}$	79

Performance

Relative	Master	MR	Change	Filename
+1.56%	198049.8	201134.7	+3085.0	total
+1.37%	-	2758.0	+2758.0	├ newly appeared files (15)
+0.17%	198049.8	198376.7	+326.9	└ common files
+0.01%	49585.7	49588.6	+2.8	├ translation units
+0.22%	148464.0	148788.1	+324.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-49.07%	63.3	32.2	-31.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v
-14.49%	16.7	14.3	-2.4	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/scoped_lock.v
-12.45%	25.7	22.5	-3.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v
-0.21%	601.1	599.9	-1.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_recursive_mutex_hpp.v
+0.17%	591.1	592.1	+1.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_mutex_hpp.v
+1.82%	169.1	172.2	+3.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp.v
+1.88%	143.4	146.1	+2.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/inc_hpp_templates.v
+2.19%	47.5	48.5	+1.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v
+3.12%	62.0	63.9	+1.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v
+7.64%	145.8	157.0	+11.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
+9.58%	30.6	33.5	+2.9	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/shared_mutex/shared_mutex.v
+16.38%	28.3	32.9	+4.6	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/mutex.v
+31.01%	22.5	29.5	+7.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/shared_mutex/test_cpp_proof.v
+653.51%	23.7	178.9	+155.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/lock_guard.v
+1460.82%	11.9	185.1	+173.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/custom_recursive_mutex_hpp_proof.v

+1.56%	198049.8	201134.7	+3085.0	total
+1.37%	-	2758.0	+2758.0	├ newly appeared files (15)
+0.17%	198049.8	198376.7	+326.9	└ common files
+0.01%	49585.7	49588.6	+2.8	├ translation units
+0.22%	148464.0	148788.1	+324.1	└ proofs and tests

pgiarrusso-sl force-pushed the ke/mutex_impl branch from e4cbb0f to 250308e Compare September 10, 2026 16:07

pgiarrusso-sl reviewed Sep 10, 2026

View reviewed changes

pgiarrusso-sl reviewed Sep 17, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/mutex/spec/mutex.v Resolved

pgiarrusso-sl reviewed Sep 17, 2026

View reviewed changes

simon-skylabs reviewed Sep 17, 2026

View reviewed changes

Comment thread rocq-brick-libstdcpp/proof/thread/spec.v Resolved

pgiarrusso-sl reviewed Sep 24, 2026

View reviewed changes

dkxb force-pushed the ke/mutex_impl branch from 8372447 to 49f0438 Compare October 6, 2026 06:30

pgiarrusso-sl mentioned this pull request Oct 9, 2026

spec for thread creation with pthread.h #186

Open

dkxb force-pushed the ke/mutex_impl branch from 821fe0f to 50cbb59 Compare October 14, 2026 19:15

dkxb linked an issue Oct 28, 2026 that may be closed by this pull request

mutex should not be able to lock twice #174

Open

dkxb removed a link to an issue Oct 28, 2026

mutex should not be able to lock twice #174

Open

pgiarrusso-sl and others added 11 commits October 29, 2026 16:24

WIP on thread_id proofs

c0e72f3

[mutex.v]: change token to user; comment out with_RepFor section

4f2111b

replace appearance of mutex.token to user

9c3b48c

check in layout of a custom mutex proof

39c9682

[custom_mutex_hpp_proof.v] add do_lock lemma statement

0789521

Tweak spec and client proof

5b1bdda

Drop trailing whitespace

0aa1a82

cleanups

4e0677c

Fix parentheses in Rep

6981a1a

custom_mutex: atomic<bool> -> atomic<int>

f78f655

Proof sketch

bf2b4da

dkxb added 21 commits October 29, 2026 16:25

update dune.inc to include the rocq ast of custom_shared_mutex.hpp an…

303d82e

…d transfer_with_mutex.cpp

[recursive_mutex.v] move current_thread out of acquireable

956e8f1

remove the MUTEX_SET module type, as it has exactly one implementatio…

72aa916

…n that we need

fix custom_mutex_hpp_proof.v

7c0c5e8

gpool, the ghost name for my_mutexes and mutex_set_map, is moved into…

6af57fd

… an instance mutex_set_G, following the invariant_name pattern in wsat.v in iris

generic [lock_guard.v] spec

0a1b844

fix files that depend on lock_guard

26964a8

fix comments

0db3eef

plausible generic [scoped_lock.v] specs

14561bd

remove the second, extraneous [my_mutexes] from mutex implementation …

5c4c5c6

…proof; require mutex namespace to not be [nroot]

[custom_mutex_hpp_proof.v] and [custom_recursive_mutex_hpp_proof.v] n…

66a7d9b

…ow use the same ghost state to track the owner thread and how much [token] it deposits

[custom_mutex_hpp_proof.v] lift owner_tid_auth out of the match in state

82c4685

[custom_recursive_mutex_hpp_proof.v] inline an unnecessary definition

b275f82

[lock_ghost2.v] remove the unnecessary MUTEX_TOKENS module type, keep…

3816527

… the module

simplify the token module: do not need given_token, token is just a f…

bb267d2

…racR

[mutex/proof/lock_guard.v] now verifies the lock_guard template code

cab2b7c

add <try_lock> and <try_lock_shared> for all 3 kinds of mutexes

a3a1674

add libcpp_tests for custom_mutex implementation

5f603a0

let dune-gen.sh ignore C++ files under rocq-brick-libstdcpp/test/mute…

ac85203

…x/libcpp_tests

make custom_mutex_hpp_proof.v more compact

1a2b17a

template spec and proof for lock_guard dtor

6f962c9

pgiarrusso-sl force-pushed the ke/mutex_impl branch from 25cd4f6 to 19ace83 Compare October 29, 2026 16:45

pgiarrusso-sl force-pushed the ke/mutex_impl branch from 19ace83 to 6f962c9 Compare October 29, 2026 17:05

pgiarrusso-sl added 4 commits October 29, 2026 19:46

[Codex] Mark adapted LLVM mutex test sources as modified

ee7f4de

Written by Codex. Add prominent per-file adaptation notices while preserving the upstream LLVM license headers and source provenance.

[Codex] Track the thread-ID hash injectivity proof obligation

be3b47a

Written by Codex. Document that the standard Hash requirements allow collisions and that owner discrimination requires a target-specific injectivity argument, including the default thread ID, or a collision-free identity.

Conversation

dkxb commented Sep 9, 2026 • edited by pgiarrusso-sl Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented Sep 9, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

skylabs-ai-ci Bot commented Sep 10, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dkxb Sep 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dkxb commented Sep 29, 2026

Uh oh!

dkxb commented Sep 29, 2026

Uh oh!

skylabs-ai-ci Bot commented Oct 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

skylabs-ai-ci Bot commented Oct 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

skylabs-ai-ci Bot commented Oct 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

dkxb commented Sep 9, 2026 •

edited by pgiarrusso-sl

Loading

dkxb Sep 18, 2026 •

edited

Loading