mutex should not be able to lock twice

[dkxb]

The requirement that dtor is called when no threads hold the lock can be enforced by the token/given_token and is orthogonal. We are experimenting with two approaches:

1. The mutex constructor returns used_threads \empty, the ablility to allocate an exclusive user th ghost state for each thread (with

   brick-libcpp/rocq-brick-libstdcpp/proof/lib/lock_ghost.v

   Lines 80 to 83 in be863c8

   	Lemma login th g s :
   	th ∉ s ->
   	used_threads g s |--
   	(|==> used_threads g (s ∪ {[ th ]}) ** user g th).

   ). This is bad with a mutex client: consider the main thread initializing some mutex, and then spawns some threads t2, t3 (which may also spawn threads dynamically and try to grab the mutex). Since used_threads is exclusive, how the threads login becomes a problem -- 2 problems, actually: a). how to distribute used_threads, and b). When a thread th log in, how does it know that th is not logged in yet? I sketch 3 attempts here; each is flawed:
   1. The main thread allocates all user tokens and then distributes them; there must exist a way to distribute them, but for the main thread to distribute a set of user to t2, it must know the set of threads that t2 will allocate in the future.
   2. We put user in some invariant user_inv ; then the set of threads already allocated is existentially quantified, and we need some other way to know what user has not been allocated. This might be mitigated by including user_inv in the thread constructor spec and using the fact that thread spawn always gets a fresh thread ID, but there the mutex can be created after threads are spawned. So the postcondition for thread ctor should probably include the ability to acquire a mutex later, even when the mutex is not created yet (which will be approach 2).
   3. We make login depend only on a version of used_threads where used_threads can be fragmented and distributed to threads, but I don't know if such a model exists while user th is still exclusive. If we have used_threads (q1+q2) \empty |-- used_threads q1 \empty ** used_threads q2 \empty then thread th can allocate user twice, which is probably not what we want.

2. Don't use user, and a thread keeps track of invariant gnames that it has locked so far (the MUTEX_SET module). Thread constructor returns my_mutexes th sa sf where sa, sf : gset gnames :=\empty for thread th, and sa is the auth piece that th keeps, sf is the frag that is used like user (traded into inv for resource); to get resources from mutex_inv := inv \gamma P, th first does my_mutexes th sa sf |-- |==> my_mutexes th (sa \union {[\gamma]} (sf \union {[\gamma]}), then split the token my_mutexes th (sa \union {[\gamma]} (sf \union {[\gamma]}) |-- |==> my_mutexes th (sa \union {[\gamma]} sf ** my_mutexes_frag th {[ \gamma ]}, and puts the singleton my_mutexes_frag in inv.

With 2, it does not have the problems that user has, but it does have a new one: since inv gnames are introduced under an \exists, we need a way to know that the gname is not in sa in my_mutexes th sa sf. Can we do this with namespaces/non_atomic invaraints?