Lawful embedding of actual address/tape actions into whole interpreter User records, including ThreadStacks.Storage. Actual stack/memory changes are preserved; no synthetic stack or second address/tape state is created.

def Miri.Interpreter.ExecutionAddressBindings.action {Whole Payload K A : Type} (lens : FunctionPointers.AddressLens Whole Payload) (inner : PointerMachine.M K Payload A) : MachineHooks.M K Whole A

Equations

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

def Miri.Interpreter.ExecutionAddressBindings.tape {Whole Payload K : Type} (lens : FunctionPointers.AddressLens Whole Payload) (inner : ExecutionChoices.Access (PointerMachine.User Payload)) : ExecutionChoices.Access (MachineHooks.State K Whole)

The tape remains inside the lawful pointer-user embedding. This lens updates only the actual nested record and preserves the active stack.

Equations

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

def Miri.Interpreter.ExecutionAddressBindings.pointerTape {Payload K : Type} (inner : ExecutionChoices.Access (PointerMachine.User Payload)) : ExecutionChoices.Access (PointerMachine.State K Payload)

Equations

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

def Miri.Interpreter.ExecutionAddressBindings.adjustRootPointer {K U : Type} (access : ExecutionChoices.Access (PointerMachine.State K U)) (h : PointerMachine.Hooks K U) (id : Memory.AllocId) (tag : Memory.BorTag) (offset : ABI.Size) (kind : Memory.AllocAddresses.AddressMemoryKind) : PointerMachine.M K U (Memory.Pointer Memory.Provenance)

Equations

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

def Miri.Interpreter.ExecutionAddressBindings.functionHooks {Whole Payload K Other : Type} (lens : FunctionPointers.AddressLens Whole Payload) (access : ExecutionChoices.Access (PointerMachine.User Payload)) (h : PointerMachine.Hooks K Payload) (base : FunctionPointers.Hooks K Whole Other) : FunctionPointers.Hooks K Whole Other

Source global/function address assignment uses fresh choices only on an uncached managed address. Function salt draws remain independently bound by ExecutionChoiceBindings.functionHooks using the same nested tape.

Equations

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