Reassociate the complete foreign primitive dictionary between the actual Core and Main thread-stack states. Each action transports its result and its partially updated error state; no guest operation is reconstructed.

def Miri.Interpreter.ExecutionForeignTransport.core {P K U D MD Ptr B I : Type} (h : ForeignItems.Core P (MachineHooks.State K (ExecutionStateTransport.Inner U)) D MD Ptr B I) : ForeignItems.Core P (MachineHooks.State K (ExecutionStateTransport.Outer U)) D MD Ptr B I

Equations

• Miri.Interpreter.ExecutionForeignTransport.core h = Miri.Interpreter.ExecutionForeignTransport.mapCore✝ (fun {A : Type} => Miri.Interpreter.ExecutionStateTransport.action) h

def Miri.Interpreter.ExecutionForeignTransport.reverseCore {P K U D MD Ptr B I : Type} (h : ForeignItems.Core P (MachineHooks.State K (ExecutionStateTransport.Outer U)) D MD Ptr B I) : ForeignItems.Core P (MachineHooks.State K (ExecutionStateTransport.Inner U)) D MD Ptr B I

Equations

• Miri.Interpreter.ExecutionForeignTransport.reverseCore h = Miri.Interpreter.ExecutionForeignTransport.mapCore✝ (fun {A : Type} => Miri.Interpreter.ExecutionStateTransport.reverseAction) h

def Miri.Interpreter.ExecutionForeignTransport.hooks {P K U D MD Ptr B I : Type} (h : ForeignItems.Hooks P (MachineHooks.State K (ExecutionStateTransport.Inner U)) D MD Ptr B I) : ForeignItems.Hooks P (MachineHooks.State K (ExecutionStateTransport.Outer U)) D MD Ptr B I

Equations

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

def Miri.Interpreter.ExecutionForeignTransport.reverseHooks {P K U D MD Ptr B I : Type} (h : ForeignItems.Hooks P (MachineHooks.State K (ExecutionStateTransport.Outer U)) D MD Ptr B I) : ForeignItems.Hooks P (MachineHooks.State K (ExecutionStateTransport.Inner U)) D MD Ptr B I

Equations

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

def Miri.Interpreter.ExecutionForeignTransport.unwind {K U C O : Type} (h : Unwind.Hooks K (ExecutionStateTransport.Inner U) C O) : Unwind.Hooks K (ExecutionStateTransport.Outer U) C O

Equations

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