Typed dyn SyncObj payloads inhabit the canonical allocation-local extras, not an independent address registry. Resolution/materialization is shared with the physical Linux futex binding. Metadata contains source host identities only.

structure Miri.Interpreter.TypedSyncObjectMachine.Payload (P : Type) : Type

• inject : TypedSyncMetadata.Payload → P
• project : P → Option TypedSyncMetadata.Payload
• projectInject (value : TypedSyncMetadata.Payload) : self.project (self.inject value) = some value

def Miri.Interpreter.TypedSyncObjectMachine.extras {U P K : Type} (v : TypedSyncMachine.Views U) (embedding : Payload P) (base : MemoryExtras.Hooks K (LinuxFutexMachine.User U) P) : MemoryExtras.Hooks K (LinuxFutexMachine.User U) P

Source access checks run directly in the physical allocation hook state, with no fabricated frame or duplicated callback roots. Unrelated source payloads remain owned by the other actual metadata family.

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.bindMemory {U P K C O B H Y Z T E : Type} (v : TypedSyncMachine.Views U) (embedding : Payload P) (h : LinuxFutexMachine.Hooks K U C P O B H Y Z T E) : LinuxFutexMachine.Hooks K U C P O B H Y Z T E

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.bindObjectMemory {U P K C O B : Type} (v : TypedSyncMachine.Views U) (embedding : Payload P) (h : LinuxFutexMachine.ObjectHooks K U C P O B) : LinuxFutexMachine.ObjectHooks K U C P O B

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.metadataFromObjectHooks {K U C P O B : Type} [DecidableEq K] (h : LinuxFutexMachine.ObjectHooks K U C P O B) (embedding : Payload P) (typed : Concurrency.TypedSyncRuntime.Hooks (LinuxFutexMachine.State K U)) : Concurrency.SyncObject.MetadataHooks (LinuxFutexMachine.State K U) TypedSyncMetadata.Payload

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.metadata {K U C P O B H Y Z T E : Type} [DecidableEq K] (h : LinuxFutexMachine.Hooks K U C P O B H Y Z T E) (embedding : Payload P) (typed : Concurrency.TypedSyncRuntime.Hooks (LinuxFutexMachine.State K U)) : Concurrency.SyncObject.MetadataHooks (LinuxFutexMachine.State K U) TypedSyncMetadata.Payload

Equations

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

structure Miri.Interpreter.TypedSyncObjectMachine.Downcast (A : Type) : Type

Exact dyn downcast view. A mismatch is absence and the canonical source getOrInitMetadata then replaces that allocation-local entry.

• inject : A → TypedSyncMetadata.Payload
• project : TypedSyncMetadata.Payload → Option A
• projectInject (value : A) : self.project (self.inject value) = some value

def Miri.Interpreter.TypedSyncObjectMachine.narrow {S A : Type} (base : Concurrency.SyncObject.MetadataHooks S TypedSyncMetadata.Payload) (cast : Downcast A) : Concurrency.SyncObject.MetadataHooks S A

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.pthread : Downcast (PthreadObjects.Payload Concurrency.TypedSyncRuntime.Ref)

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.windows : Downcast (WindowsSync.Payload Concurrency.TypedSyncRuntime.Ref)

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.macLock : Downcast (MacOsSync.Unfair Concurrency.TypedSyncRuntime.Ref)

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.macSemaphore : Downcast (MacOsSync.Semaphore Concurrency.TypedSyncRuntime.Ref)

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.macFutex : Downcast Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.TypedSyncObjectMachine.freeBsdFutex : Downcast Concurrency.TypedSyncRuntime.Ref

Equations

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

structure Miri.Interpreter.TypedSyncObjectMachine.Bytes (S : Type) : Type

Byte access operations are separated from typed metadata ownership. They must be supplied by the actual allocation/atomic machine, never by an arena.

• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → EStateM StepError S Unit
• offset : MPlaceTy Memory.Provenance → ABI.Size → EStateM StepError S (MPlaceTy Memory.Provenance)
• compareExchangeByteRelaxed : MPlaceTy Memory.Provenance → UInt8 → UInt8 → EStateM StepError S (UInt8 × Bool)
• writeZeros : Memory.Pointer (Option Memory.Provenance) → ABI.Size → EStateM StepError S Unit
• writeByte : MPlaceTy Memory.Provenance → UInt8 → EStateM StepError S Unit

def Miri.Interpreter.TypedSyncObjectMachine.full {S A : Type} (base : Concurrency.SyncObject.MetadataHooks S TypedSyncMetadata.Payload) (bytes : Bytes S) (cast : Downcast A) : Concurrency.SyncObject.Hooks S A

Equations

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