Genuine surviving execution inputs. Operational callbacks replaced by canonical assembly are deliberately absent, rather than accepted and ignored.

structure Miri.Interpreter.ExecutionLeaves.Rvalue (S C : Type) : Type

• threadLocalPointer : C → MIR.DefId → RvalueM S (Memory.Pointer (Option Memory.Provenance))
• normalize : C → MIR.TyId → RvalueM S MIR.TyId

structure Miri.Interpreter.ExecutionLeaves.Discriminant (S C : Type) : Type

• discriminantLayout : C → MIR.TyId → RvalueM S LocalLayout
• tagLayout : C → ABI.Scalar → RvalueM S LocalLayout
• discriminantValue : C → MIR.TyId → Nat → RvalueM S (Option (MIR.TyId × ABI.U128))
• variantForDiscriminant : C → MIR.TyId → ABI.U128 → RvalueM S (Option Nat)
• adtVariantCount : C → MIR.TyId → RvalueM S Nat
• scalarMayBeNull : C → Memory.Scalar Memory.Provenance → RvalueM S Bool

def Miri.Interpreter.ExecutionLeaves.Discriminant.ofHooks {S C V : Type} (h : DiscriminantHooks Memory.Provenance S C V) : Discriminant S C

Equations

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

structure Miri.Interpreter.ExecutionLeaves.Operand (S C : Type) : Type

• checkPlaceType : C → MIR.Place → OpTy Memory.Provenance → RvalueM S Unit
• dereference : C → OpTy Memory.Provenance → RvalueM S (MPlaceTy Memory.Provenance)
• runtimeChecks : C → MIR.RuntimeChecks → RvalueM S Bool
• boolLayout : C → RvalueM S LocalLayout
• constantAt : C → OperandPath → MIR.ConstOperand → Option LocalLayout → RvalueM S (OpTy Memory.Provenance)

structure Miri.Interpreter.ExecutionLeaves.Control (P L E : Type) : Type

• bodySpan : Frame P L E → Except StepError MIR.SpanRef