The source synchronization metadata sum is shared by ordinary MIR memory extras and callback futex construction. Keep this payload/embedding layer below EvalConfigurationCore so both source assemblers can depend on it without an import cycle.

inductive Miri.Input.EvalSyncPayload.Payload : Type

• typed (value : Interpreter.TypedSyncMetadata.Payload) : Payload
• linuxFutex (ref : Concurrency.FutexRuntime.Ref) : Payload

def Miri.Input.EvalSyncPayload.typedEmbedding : Interpreter.TypedSyncObjectMachine.Payload Payload

Equations

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

def Miri.Input.EvalSyncPayload.linuxFutexEmbedding : Interpreter.LinuxFutexMachine.Payload Payload

Equations

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