Concrete mem_copy_repeatedly access adapter. Actual Allocation copying retains initialization and partial provenance; PlaceMachine supplies ordered race/weak/TB/sync callbacks, including partial failed tree mutation.

@[reducible, inline]

abbrev Miri.Interpreter.MemoryCopyMachine.User (U : Type) : Type

Equations

• Miri.Interpreter.MemoryCopyMachine.User = Miri.Interpreter.PointerMachine.User

@[reducible, inline]

abbrev Miri.Interpreter.MemoryCopyMachine.GenericState (K U : Type) : Type

Equations

• Miri.Interpreter.MemoryCopyMachine.GenericState K U = Miri.Interpreter.PlaceMachine.AccessState K U

@[reducible, inline]

abbrev Miri.Interpreter.MemoryCopyMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.MemoryCopyMachine.State K U = Miri.Interpreter.MemoryCopyMachine.GenericState K (Miri.Interpreter.MemoryCopyMachine.User U)

def Miri.Interpreter.MemoryCopyMachine.genericHooks {K U : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K U) (addresses : U → Memory.AllocAddresses.GlobalAddressState) (arithmetic : Memory.PointerArithmetic) : Memory.MemoryCopyHooks Memory.Provenance TreeBorrows.BorrowTree K (GenericState K U) Memory.ProvenanceExtra

Equations

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

def Miri.Interpreter.MemoryCopyMachine.genericCopy {K U : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K U) (addresses : U → Memory.AllocAddresses.GlobalAddressState) (arithmetic : Memory.PointerArithmetic) (source dest : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) (repeatCount : UInt64) (nonoverlapping : Bool) : MachineHooks.M K U Unit

Real bytes, init-mask, provenance, and overlapping-copy operation. Both machine effects and allocation-tree mutations commit before any failure.

Equations

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

def Miri.Interpreter.MemoryCopyMachine.hooks {K U : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K (User U)) (arithmetic : Memory.PointerArithmetic) : Memory.MemoryCopyHooks Memory.Provenance TreeBorrows.BorrowTree K (State K U) Memory.ProvenanceExtra

Compatibility adapter for the original PointerMachine user record.

Equations

• Miri.Interpreter.MemoryCopyMachine.hooks config arithmetic = Miri.Interpreter.MemoryCopyMachine.genericHooks config Miri.Interpreter.PointerMachine.User.addresses arithmetic

def Miri.Interpreter.MemoryCopyMachine.copy {K U : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K (User U)) (arithmetic : Memory.PointerArithmetic) (source dest : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) (repeatCount : UInt64) (nonoverlapping : Bool) : MachineHooks.M K (User U) Unit

Equations

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