Production-shaped typed retag bindings. No precomputed RetagPipeline request is constructed: all leaves execute inside TypedRetag's source driver.

def Miri.Interpreter.TypedMachineBindings.retagHooks {K User : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (queries : TypedRetag.Hooks K User) : TypedRetag.Hooks K User

Install actual machine writes and source reference reconstruction. The remaining required dictionary contains genuine compiler/pointer queries.

Equations

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

def Miri.Interpreter.TypedMachineBindings.bindValidity {K User C F A Padding : Type} [DecidableEq K] (base : ValidityVisitor.Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra F A Padding) (retag : TypedRetag.Hooks K User) (budget : Nat) : ValidityVisitor.Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra F A Padding

Copies retag through the actual validity visitor only when its source resetProvenanceAndPadding policy requests it. FnEntry/None/Default modes are read here at the source event, rather than captured while constructing hooks.

Equations

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

def Miri.Interpreter.TypedMachineBindings.bindValidation {K User C F A Padding : Type} [DecidableEq K] (compiler : PlaceMachine.CompilerHooks K User C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (visitor : ValidityVisitor.Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra F A Padding) (retag : TypedRetag.Hooks K User) (retagBudget validationBudget : Nat) (recursive : C → LocalLayout → MachineHooks.M K User Bool) : PlaceMachine.CompilerHooks K User C × PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C

place.rs write_immediate/copy_op_inner validation policies: destination reset is true; a transmute validates at the source layout first, including a wrapping zero-offset projection, then the destination's validation pass. The recursive machine policy remains an explicit source query.

Equations

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

def Miri.Interpreter.TypedMachineBindings.bindRvalue {K User C : Type} [DecidableEq K] (base : RvalueHooks Memory.Provenance (MachineHooks.State K User) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K User) (allocation : PlaceMachine.AllocationConfig K User) (compiler : PlaceMachine.CompilerHooks K User C) (queries : TypedRetag.Hooks K User) (budget : Nat) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (evaluatePlace : C → MIR.Place → Bool → MachineHooks.M K User (RuntimePlace Memory.Provenance)) : RvalueHooks Memory.Provenance (MachineHooks.State K User) C (RuntimePlace Memory.Provenance)

Bind typed places and source retag events to rvalue execution. The compiler validation dictionary must use bindValidity so copy/reset paths share this same stateful retag driver. Raw pointer and integer copies gain no extra retag.

Equations

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

def Miri.Interpreter.TypedMachineBindings.popRaw {K User : Type} [DecidableEq K] (retag : TypedRetag.Hooks K User) : MachineHooks.M K User (Frame Memory.Provenance LocalLayout MachineHooks.FrameExtra)

Source pop_stack_frame_raw: release protectors while the frame remains current, before removing it and before return-value copying.

Equations

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

def Miri.Interpreter.TypedMachineBindings.bindCall {K User C Other Extern FnABI ArgABI : Type} [DecidableEq K] (base : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) (access : PlaceMachine.AccessConfig K User) (allocation : PlaceMachine.AllocationConfig K User) (compiler : PlaceMachine.CompilerHooks K User C) (storage : MachineHooks.StorageHooks K User) (queries : TypedRetag.Hooks K User) (budget : Nat) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (evaluatePlace : C → MIR.Place → Bool → MachineHooks.M K User (RuntimePlace Memory.Provenance)) : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI

Call argument and return-slot copies use the canonical place copy path; FnEntry scope comes from Call.initStackFrame, not from dictionary construction. In-place protection is performed after each source copy.

Equations

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

def Miri.Interpreter.TypedMachineBindings.bindControl {K User C : Type} [DecidableEq K] (base : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C (OpTy Memory.Provenance)) (access : PlaceMachine.AccessConfig K User) (allocation : PlaceMachine.AllocationConfig K User) (compiler : PlaceMachine.CompilerHooks K User C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (queries : TypedRetag.Hooks K User) : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C (OpTy Memory.Provenance)

Return reads local zero before pop, copies after protector release/pop, and invokes the same transmute-copy/validity path as argument passing. Cleanup and unwind policy stay the required source lifecycle dictionary fields.

Equations

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