Portable intrinsic memory and helper dictionaries on canonical machine state. Arithmetic dispatch stays in Intrinsics; physical memory callbacks are closed with the actual allocation, TB, race, weak-memory and sync pipelines.

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicMachine.User (User : Type) : Type

Equations

• Miri.Interpreter.IntrinsicMachine.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

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

Equations

• Miri.Interpreter.IntrinsicMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

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

Equations

• Miri.Interpreter.IntrinsicMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

def Miri.Interpreter.IntrinsicMachine.copyMemory {K U C : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (fuel : Nat) (debugAssertions : Bool) (choice : C) (source dest : MPlaceTy Memory.Provenance) : M K U Unit

Full typed-copy memory arm, preserving destination dynamic query before optional source query, real global materialization, and delayed misalignment.

Equations

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

def Miri.Interpreter.IntrinsicMachine.bind {K U C SyncPayload F A Padding : Type} [DecidableEq K] (base : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K (User U)) (allocation : PlaceMachine.AllocationConfig K (User U)) (deallocation : AllocationMachine.DeallocationHooks K (User U) SyncPayload) (compiler : PlaceMachine.CompilerHooks K (User U) C) (copy : PlaceCopyHooks Memory.Provenance (State K U) C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (dynamicFuel : Nat) (validity : ValidityVisitor.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra F A Padding) (validationFuel : Nat) : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Bind concrete physical helper operations. AllocationConfig and deallocation hooks must be the owner's already composed lifecycle dictionaries, including MemoryExtras initialization and cleanup; this never installs them twice. Compiler type/layout/dereference queries remain the existing source ports.

Equations

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