Reduced cast leaves and direct physical CastHooks construction. Compiler, vtable and provenance policies survive; canonical memory/copy/projection, function-pointer resolution and recursive validation never enter as a dummy base dictionary. The Cast.cast source policy is reused unchanged.

structure Miri.Interpreter.ExecutionCast.Leaves (S C : Type) : Type

• typeInfo : C → MIR.TyId → RvalueM S CastTypeInfo
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• exposeProvenance : C → Memory.Provenance → RvalueM S Unit
• pointerFromExposedAddress : C → UInt64 → RvalueM S (Memory.Pointer (Option Memory.Provenance))
• usizeLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• ensureMonomorphic : C → MIR.TyId → RvalueM S Unit
• requireNoBoundVars : C → Array MIR.GenericArg → RvalueM S Unit
• resolveFunction : C → MIR.DefId → Array MIR.GenericArg → RvalueM S (Option CallInstance)
• resolveClosureFnOnce : C → MIR.DefId → Array MIR.GenericArg → RvalueM S CallInstance
• builtinDeref : C → MIR.TyId → Bool → RvalueM S (Option MIR.TyId)
• boxLayout : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• validateImmediateABI : Immediate Memory.Provenance → ABI.LayoutData → Except StepError Unit
• fieldLayout : C → ABI.TyAndLayout MIR.TyId → Nat → RvalueM S (ABI.TyAndLayout MIR.TyId)
• lockstepTails : C → MIR.TyId → MIR.TyId → RvalueM S (MIR.TyId × MIR.TyId)
• vtableType : C → Memory.Pointer (Option Memory.Provenance) → Option Nat → RvalueM S MIR.TyId
• vtablePointer : C → MIR.TyId → Nat → RvalueM S (Memory.Pointer (Option Memory.Provenance))
• principal : C → Nat → RvalueM S (Option Nat)
• vtableEntries : C → Option Nat → MIR.TyId → RvalueM S (Array (VTableEntry CallInstance))
• supertraitSlot : C → MIR.TyId → MIR.TyId → RvalueM S (Option Nat)
• eraseSelfTraitRef : C → Nat → RvalueM S Nat
• normalizePrincipal : C → Nat → RvalueM S (Option Nat)

def Miri.Interpreter.ExecutionCast.Leaves.ofHooks {S C V : Type} (h : CastHooks Memory.Provenance S C V) : Leaves S C

Equations

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

def Miri.Interpreter.ExecutionCast.hooks {K U C O Pad : Type} [DecidableEq K] (queries : Leaves (MachineHooks.State K U) C) (access : PlaceMachine.AccessConfig K U) (allocation : PlaceMachine.AllocationConfig K U) (compiler : PlaceMachine.CompilerHooks K U C) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K U) C) (retag : TypedRetag.Hooks K U) (validity : ValidityVisitor.Hooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra (FnVal O) (ABI.FnAbi MIR.TyId) Pad) (functions : FunctionPointers.Hooks K U O) (floats : FloatOpsHooks Memory.Provenance (MachineHooks.State K U) C) (dereference : C → OpTy Memory.Provenance → MachineHooks.M K U (MPlaceTy Memory.Provenance)) (projectRead : C → OpTy Memory.Provenance → Nat → MachineHooks.M K U (OpTy Memory.Provenance)) (validationRecursive : C → LocalLayout → MachineHooks.M K U Bool) (retagBudget validationBudget : Nat) : CastHooks Memory.Provenance (MachineHooks.State K U) C (RuntimePlace Memory.Provenance)

Equations

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