Executable callback binding for pinned concurrency/sync.rs. Canonical Sync transitions own lock/clock/queue rules; this layer runs real typed closures, scalar stores and ThreadManager callbacks rather than accepting token completion.

@[reducible, inline]

abbrev Miri.Concurrency.SyncRuntime.M (σ α : Type) : Type

Equations

• Miri.Concurrency.SyncRuntime.M = EStateM Miri.Interpreter.StepError

@[reducible, inline]

abbrev Miri.Concurrency.SyncRuntime.Callback (S : Type) : Type

Equations

• Miri.Concurrency.SyncRuntime.Callback S = (Miri.Concurrency.UnblockKind → Miri.Concurrency.SyncRuntime.M S Unit)

structure Miri.Concurrency.SyncRuntime.Registry (S : Type) : Type

• next : Nat
• entries : Array (Nat × Callback S)
• disposers : Array (Nat × M S Unit)

  Explicit semantic Drop actions for owned captures. Plain callbacks use lexical cleanup (for example Files.withDrop) or contain non-owning IDs.

def Miri.Concurrency.SyncRuntime.Registry.register {S : Type} (registry : Registry S) (callback : Callback S) : Registry S × Nat

Equations

• registry.register callback = ({ next := registry.next + 1, entries := registry.entries.push (registry.next, callback), disposers := registry.disposers }, registry.next)

def Miri.Concurrency.SyncRuntime.Registry.registerOwned {S : Type} (registry : Registry S) (callback : Callback S) (dropCaptures : M S Unit) : Registry S × Nat

Owned captures require an actual stateful drop, never a GC-root promise.

Equations

• One or more equations did not get rendered due to their size.

structure Miri.Concurrency.SyncRuntime.TakenCallback (S : Type) : Type

• body : Callback S
• dispose : Option (M S Unit)

def Miri.Concurrency.SyncRuntime.Registry.take {S : Type} (registry : Registry S) (token : Nat) : Except Interpreter.StepError (Registry S × TakenCallback S)

Source MachineCallback.call consumes Box<Self> before running its body. Duplicate tokens are representation failures, never an arbitrary first match.

Equations

• One or more equations did not get rendered due to their size.

inductive Miri.Concurrency.SyncRuntime.UserCapture (R D : Type) : Type

Data-only captures of source OS callbacks.

• pthreadSemaphore {R D : Type} (timed : Bool) (dest : D) : UserCapture R D
• futexErrno {R D : Type} (dest : D) : UserCapture R D
• windowsAddress {R D : Type} (dest : D) : UserCapture R D
• windowsInitOnce {R D : Type} (ref : R) (pending dest : D) : UserCapture R D
• macAddress {R D : Type} (ref : R) (dest : D) : UserCapture R D
• macSemaphore {R D : Type} (dest : D) : UserCapture R D
• sleep {R D : Type} : UserCapture R D

inductive Miri.Concurrency.SyncRuntime.Capture (R V D : Type) : Type

• mutex {R V D : Type} (ref : R) (result : Option (V × D)) : Capture R V D
• reader {R V D : Type} (ref : R) (value : V) (dest : D) : Capture R V D
• writer {R V D : Type} (ref : R) (value : V) (dest : D) : Capture R V D
• condvar {R V D : Type} (ref mutex : R) (success timeout : V) (dest : D) : Capture R V D
• futex {R V D : Type} (ref : R) (user : UserCapture R D) : Capture R V D
• semaphore {R V D : Type} (ref : R) (deadline : Option ThreadDeadline) (user : UserCapture R D) : Capture R V D
• user {R V D : Type} (value : UserCapture R D) : Capture R V D

inductive Miri.Concurrency.SyncRuntime.CallbackBackend (S R V D : Type) : Type

Production stores typed captures. Only the explicit fixture branch carries an arbitrary function registry; a production constructor never supplies one.

• legacy {S R V D : Type} (get : M S (Registry S)) (put : Registry S → M S Unit) : CallbackBackend S R V D
• typed {S R V D : Type} (register : Capture R V D → M S Nat) (run : Nat → UnblockKind → M S Unit) (cancel : Nat → M S Unit) (owns : Nat → M S Bool) : CallbackBackend S R V D

structure Miri.Concurrency.SyncRuntime.Hooks (S R V D : Type) : Type

• handler : SyncClockHandler
• usizeBits : Nat
• communicate : Bool
• global : M S (Option GlobalState)
• putGlobal : Option GlobalState → M S Unit
• threads : M S ThreadManager
• putThreads : ThreadManager → M S Unit
• callbackBackend : CallbackBackend S R V D
• mutex : R → M S MutexState
• putMutex : R → MutexState → M S Unit
• rwlock : R → M S RwLockState
• putRwlock : R → RwLockState → M S Unit
• condvar : R → M S CondvarState
• putCondvar : R → CondvarState → M S Unit
• futex : R → M S FutexState
• putFutex : R → FutexState → M S Unit
• semaphore : R → M S SemaphoreState
• putSemaphore : R → SemaphoreState → M S Unit
• writeScalar : V → D → M S Unit
• error : SyncError → Interpreter.StepError

def Miri.Concurrency.SyncRuntime.Hooks.callbacks {S R V D : Type} (h : Hooks S R V D) : M S (Registry S)

Legacy-only compatibility accessors. Production typed backends expose no function registry; an unported caller remains an explicit callback obligation.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.Hooks.putCallbacks {S R V D : Type} (h : Hooks S R V D) (registry : Registry S) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.register {S R V D : Type} (h : Hooks S R V D) (capture : Option (Capture R V D)) (callback : Callback S) : M S Nat

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.ownsCallback {S R V D : Type} (h : Hooks S R V D) (token : Nat) : M S Bool

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.takeCallback {S R V D : Type} (h : Hooks S R V D) (token : Nat) : M S (TakenCallback S)

This operation is only available on the explicit legacy fixture backend.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.runCallback {S R V D : Type} (h : Hooks S R V D) (token : Nat) (kind : UnblockKind) : M S Unit

No thread switch/restore: deadline and readiness wrappers already own it.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.cancelCallback {S R V D : Type} (h : Hooks S R V D) (token : Nat) : M S Unit

Cancel an unowned registration, consuming source FnOnce captures once.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.discardIfUnowned {S R V D : Type} (h : Hooks S R V D) (token : Nat) : M S Unit

Source drops a newly built callback when blocking fails before ownership moves into ThreadState::Blocked. Keep entries already owned by any thread.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.runUnblockCallback {S R V D : Type} (h : Hooks S R V D) (obligation : UnblockCallbackObligation) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.mutexLock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.mutexUnlock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S MutexUnlockResult

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.mutexEnqueue {S R V D : Type} (h : Hooks S R V D) (ref : R) (retval : Option (V × D)) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.readerLock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.writerLock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.readerUnlock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Bool

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.writerUnlock {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Bool

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.enqueueReader {S R V D : Type} (h : Hooks S R V D) (ref : R) (value : V) (dest : D) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.enqueueWriter {S R V D : Type} (h : Hooks S R V D) (ref : R) (value : V) (dest : D) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.reacquireMutex {S R V D : Type} (h : Hooks S R V D) (ref : R) (value : V) (dest : D) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.condvarWait {S R V D : Type} (h : Hooks S R V D) (ref mutex : R) (deadline : Option ThreadDeadline) (success timeout : V) (dest : D) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.condvarSignal {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Bool

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.futexWait {S R V D : Type} (h : Hooks S R V D) (ref : R) (bitset : UInt32) (deadline : Option ThreadDeadline) (callback : Callback S) (capture : Option (UserCapture R D) := none) : M S Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.futexWake {S R V D : Type} (h : Hooks S R V D) (ref : R) (bitset : UInt32) (count : Nat) : M S Nat

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.semaphoreDecrement {S R V D : Type} (budget : Nat) (h : Hooks S R V D) (ref : R) (deadline : Option ThreadDeadline) (callback : Callback S) (capture : Option (UserCapture R D) := none) : M S Unit

Production retries are interpreted from data and need no recursive runner budget. The legacy fixture path retains its explicit resource bound.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.semaphoreIncrement {S R V D : Type} (h : Hooks S R V D) (ref : R) : M S Bool

Equations

• One or more equations did not get rendered due to their size.

def Miri.Concurrency.SyncRuntime.bindMachine {K U R V D : Type} (base : Hooks (Interpreter.MachineHooks.State K U) R V D) : Hooks (Interpreter.MachineHooks.State K U) R V D

Equations

• One or more equations did not get rendered due to their size.