Lawful canonical state reassociation for memory/allocation capabilities. All byte/tree/clock/global-materialization effects and failed touched prefixes stay in the same machine. No replacement memory operations are introduced.

def Miri.Interpreter.ExecutionMemoryTransport.machineIn {K U : Type} (s : PlaceMachine.Machine K (ExecutionStateTransport.Outer U)) : PlaceMachine.Machine K (ExecutionStateTransport.Inner U)

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.machineOut {K U : Type} (s : PlaceMachine.Machine K (ExecutionStateTransport.Inner U)) : PlaceMachine.Machine K (ExecutionStateTransport.Outer U)

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.machineAction {K U A : Type} (a : PlaceMachine.MachineM K (ExecutionStateTransport.Inner U) A) : PlaceMachine.MachineM K (ExecutionStateTransport.Outer U) A

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.accessIn {K U : Type} (s : PlaceMachine.AccessState K (ExecutionStateTransport.Outer U)) : PlaceMachine.AccessState K (ExecutionStateTransport.Inner U)

Equations

• Miri.Interpreter.ExecutionMemoryTransport.accessIn s = { machine := Miri.Interpreter.ExecutionMemoryTransport.machineIn s.machine, pendingError := s.pendingError }

def Miri.Interpreter.ExecutionMemoryTransport.accessOut {K U : Type} (s : PlaceMachine.AccessState K (ExecutionStateTransport.Inner U)) : PlaceMachine.AccessState K (ExecutionStateTransport.Outer U)

Equations

• Miri.Interpreter.ExecutionMemoryTransport.accessOut s = { machine := Miri.Interpreter.ExecutionMemoryTransport.machineOut s.machine, pendingError := s.pendingError }

def Miri.Interpreter.ExecutionMemoryTransport.access {K U : Type} (h : PlaceMachine.AccessConfig K (ExecutionStateTransport.Inner U)) : PlaceMachine.AccessConfig K (ExecutionStateTransport.Outer U)

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.allocation {K U : Type} (h : PlaceMachine.AllocationConfig K (ExecutionStateTransport.Inner U)) : PlaceMachine.AllocationConfig K (ExecutionStateTransport.Outer U)

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.extras {K U P : Type} (h : MemoryExtras.Hooks K (ExecutionStateTransport.Inner U) P) : MemoryExtras.Hooks K (ExecutionStateTransport.Outer U) P

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.lifecycle {K U : Type} (h : Memory.MemoryLifecycleHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (ExecutionStateTransport.Inner U)) Memory.ProvenanceExtra) : Memory.MemoryLifecycleHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (ExecutionStateTransport.Outer U)) Memory.ProvenanceExtra

Equations

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

def Miri.Interpreter.ExecutionMemoryTransport.deallocation {K U P : Type} (h : AllocationMachine.DeallocationHooks K (ExecutionStateTransport.Inner U) P) : AllocationMachine.DeallocationHooks K (ExecutionStateTransport.Outer U) P

Equations

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