Complete raw global/local lookup around memory.rs:1490–1638 memcopy. Cow::Borrowed sources remain detached; only Owned source conversions cache. Destination globals materialize before WriteToReadOnly, preserving that cache on UB. Source snapshots survive destination conversion and overlapping writes.

@[reducible, inline]

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

Equations

• Miri.Interpreter.GlobalMemoryCopyMachine.User = Miri.Interpreter.PointerMachine.User

@[reducible, inline]

abbrev Miri.Interpreter.GlobalMemoryCopyMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.GlobalMemoryCopyMachine.M K U A = Miri.Interpreter.PointerMachine.M K U A

def Miri.Interpreter.GlobalMemoryCopyMachine.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

Two pointer checks precede source probe (even size zero), source lookup, read, destination lookup/mutability, destination before_alloc_access, write, then actual snapshot copy. num_copies=0 still reads a nonzero source.

Equations

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

def Miri.Interpreter.GlobalMemoryCopyMachine.typedCopy {K U C : Type} [DecidableEq K] (config : PlaceMachine.AccessConfig K U) (addresses : U → Memory.AllocAddresses.GlobalAddressState) (arithmetic : Memory.PointerArithmetic) (dynamic : DynamicLayoutHooks Memory.Provenance (MachineHooks.State K U) C) (fuel : Nat) (debugAssertions : Bool) (choice : C) (source dest : MPlaceTy Memory.Provenance) : MachineHooks.M K U Unit

Source typed-copy slow path shared by intrinsic and MIR copies. Dynamic sizes precede physical copying; misalignment is reported only after copying.

Equations

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

def Miri.Interpreter.GlobalMemoryCopyMachine.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) : M K U Unit

Original PointerMachine-shaped API, retaining the same implementation.

Equations

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