theorem rwlock_writer_lock_none_contract (global : Miri.Concurrency.GlobalState) (threads : Miri.Concurrency.ThreadManager) : have result := { }.writerLock global threads Miri.Concurrency.SyncClockHandler.none; (result.syncState Miri.Concurrency.GlobalState).writer = some threads.activeThread ∧ (result.syncState Miri.Concurrency.GlobalState).readers = [] ∧ result.outcomeIsOk

The WriterLock source operation, with the no-race-handler clock hook, establishes writer ownership for the active thread.

theorem mutex_callback_is_pending (state : Miri.Concurrency.MutexState) (global : Miri.Concurrency.GlobalState) (threads : Miri.Concurrency.ThreadManager) (request : Miri.Concurrency.SyncCallbackRequest) (hcallback : (state.unlock global threads Miri.Concurrency.SyncClockHandler.none).callback Miri.Concurrency.GlobalState = some request) : (state.unlock global threads Miri.Concurrency.SyncClockHandler.none).hasPendingWork = true

The mutex callback bridge is a pending source action until callback completion; a transition with that action cannot satisfy the local completed predicate.