Direct cast query construction. Unexported generic/trait transformations remain named mandatory compiler queries, rather than a baseline CastHooks record containing physical operations that will subsequently be overwritten.

structure Miri.Input.CompilerCastLeaves.Required (S C : Type) : Type

• requireNoBoundVars : C → Array MIR.GenericArg → Interpreter.RvalueM S Unit
• resolveFunction : C → MIR.DefId → Array MIR.GenericArg → Interpreter.RvalueM S (Option Interpreter.CallInstance)
• resolveClosureFnOnce : C → MIR.DefId → Array MIR.GenericArg → Interpreter.RvalueM S Interpreter.CallInstance
• lockstepTails : C → MIR.TyId → MIR.TyId → Interpreter.RvalueM S (MIR.TyId × MIR.TyId)
• boxLayout : C → MIR.TyId → Interpreter.RvalueM S (ABI.TyAndLayout MIR.TyId)
• principal : C → Nat → Interpreter.RvalueM S (Option Nat)
• supertraitSlot : C → MIR.TyId → MIR.TyId → Interpreter.RvalueM S (Option Nat)
• eraseSelfTraitRef : C → Nat → Interpreter.RvalueM S Nat
• normalizePrincipal : C → Nat → Interpreter.RvalueM S (Option Nat)

def Miri.Input.CompilerCastLeaves.make {S C : Type} (p : CompilerProviders.Prepared) (required : Required S C) (vtable : Interpreter.VTableHooks Memory.Provenance S C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) (expose : C → Memory.Provenance → Interpreter.RvalueM S Unit) (fromExposed : C → UInt64 → Interpreter.RvalueM S (Memory.Pointer (Option Memory.Provenance))) (validateABI : Interpreter.Immediate Memory.Provenance → ABI.LayoutData → Except Interpreter.StepError Unit) : Interpreter.ExecutionCast.Leaves S C

Equations

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