Lawful existing full-state reassociation for final foreign calls. Only interpreter actions move; source object/callback identities stay unchanged.

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncTransport.Inner (K U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncTransport.Inner K U = Miri.Interpreter.TypedSyncMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncTransport.Outer (K U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncTransport.Outer K U = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.ExecutionStateTransport.Outer U)

def Miri.Interpreter.TypedSyncTransport.metadata {K U A : Type} (h : Concurrency.SyncObject.MetadataHooks (Inner K U) A) : Concurrency.SyncObject.MetadataHooks (Outer K U) A

Equations

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

def Miri.Interpreter.TypedSyncTransport.full {K U A : Type} (h : Concurrency.SyncObject.Hooks (Inner K U) A) : Concurrency.SyncObject.Hooks (Outer K U) A

Equations

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

def Miri.Interpreter.TypedSyncTransport.bytes {K U : Type} (h : TypedSyncObjectMachine.Bytes (Inner K U)) : TypedSyncObjectMachine.Bytes (Outer K U)

Equations

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

def Miri.Interpreter.TypedSyncTransport.runtime {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (Inner K U)) : Concurrency.SyncRuntime.Hooks (Outer K U) Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest

Construct the outer production backend directly from the source typed factory. No legacy registry is transported or fabricated.

Equations

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

def Miri.Interpreter.TypedSyncTransport.once {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (Inner K U)) : Concurrency.InitOnce.Hooks (Outer K U) Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest

Equations

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

def Miri.Interpreter.TypedSyncTransport.pthread {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (Inner K U)) (h : PthreadObjects.Hooks (Inner K U) Concurrency.TypedSyncRuntime.Ref) : PthreadObjects.Hooks (Outer K U) Concurrency.TypedSyncRuntime.Ref

Equations

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