Direct validity visitor construction from surviving compiler/CTFE queries. Every byte/scalar access, provenance/padding operation, scoped ghost validation, union-range cache and pointer check is the actual canonical implementation. The recursive visitor and freeze-sensitive retag policy are reused unchanged.

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

• classify : C → MIR.TyId → ValidityVisitor.M S ValidityVisitor.TypeKind
• unitLayout : C → ValidityVisitor.M S LocalLayout
• typeName : C → MIR.TyId → ValidityVisitor.M S String
• opsemInhabited : C → MIR.TyId → ValidityVisitor.M S Bool
• isFreeze : C → MIR.TyId → ValidityVisitor.M S Bool
• fieldPath : C → LocalLayout → Nat → MIR.TyId → ValidityVisitor.M S Memory.PathElem
• variantPath : C → LocalLayout → Nat → ValidityVisitor.M S Memory.PathElem
• projectBox : C → RuntimePlace Memory.Provenance → ValidityVisitor.M S (RuntimePlace Memory.Provenance × RuntimePlace Memory.Provenance)
• metadataTail : C → MIR.TyId → ValidityVisitor.M S ValidityVisitor.MetadataTail
• ctfePointerLookup : C → MPlaceTy Memory.Provenance → Memory.Validity.CtfeMode → ValidityVisitor.M S Memory.Validity.PointerAllocLookup

def Miri.Interpreter.ExecutionValidity.Leaves.ofHooks {S C E F A Pad : Type} (h : ValidityVisitor.Hooks Memory.Provenance S C E F A Pad) : Leaves S C

Equations

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

def Miri.Interpreter.ExecutionValidity.hooks {K U C F A : Type} [DecidableEq K] (queries : Leaves (ValidityMachine.State K U) C) (access : ValidityMachine.Access K U) (allocation : PlaceMachine.AllocationConfig K (ValidityMachine.UserState U)) (compiler : ValidityMachine.Compiler K U C) (projection : PlaceProjectionHooks Memory.Provenance (ValidityMachine.State K U) C MachineHooks.FrameExtra) (vtable : VTableHooks Memory.Provenance (ValidityMachine.State K U) C F A) (discriminant : DiscriminantHooks Memory.Provenance (ValidityMachine.State K U) C (RuntimePlace Memory.Provenance)) (retag : TypedRetag.Hooks K (ValidityMachine.UserState U)) (retagBudget : Nat) : ValidityVisitor.Hooks Memory.Provenance (ValidityMachine.State K U) C MachineHooks.FrameExtra F A ValidityMemory.PaddingHandle

Equations

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