Pinned interpret/discriminant.rs pipelines. Field access, compiler queries and CTFE pointer-nullability remain explicit effectful dependencies.

structure Miri.Interpreter.DiscriminantHooks (Prov S C V : Type) : Type

• runtimeTarget : ABI.RuntimeTargetDataLayout
• discriminantLayout : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• tagLayout : C → ABI.Scalar → RvalueM S (ABI.TyAndLayout MIR.TyId)
• 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
• projectRead : C → OpTy Prov → Nat → RvalueM S (OpTy Prov)
• readImmediate : C → OpTy Prov → RvalueM S (RvalueImmTy Prov)
• destLayout : V → ABI.TyAndLayout MIR.TyId
• projectWrite : C → V → Nat → RvalueM S V
• writeScalar : C → Memory.Scalar Prov → V → RvalueM S Unit
• toOp : C → V → RvalueM S (OpTy Prov)
• scalarMayBeNull : C → Memory.Scalar Prov → RvalueM S Bool

def Miri.Interpreter.Discriminant.discriminantForVariant {P S C V : Type} (h : DiscriminantHooks P S C V) (choice : C) (ty : MIR.TyId) (variant : Nat) : RvalueM S (RvalueImmTy P)

User-visible discriminants differ from both tag bits and declaration indices. Types without compiler discriminants have only discriminant/index zero.

Equations

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

def Miri.Interpreter.Discriminant.tagForVariant {P S C V : Type} [Memory.PointerProvenance P] (h : DiscriminantHooks P S C V) (choice : C) (layout : ABI.TyAndLayout MIR.TyId) (variant : Nat) : RvalueM S (Option (Memory.ScalarInt × Nat))

Source tag_for_variant: uninhabited variants fail before all tag queries.

Equations

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

def Miri.Interpreter.Discriminant.readDiscriminant {P S C V : Type} [Memory.PointerProvenance P] (h : DiscriminantHooks P S C V) (choice : C) (op : OpTy P) : RvalueM S Nat

Read the discriminant without assuming that an enum's wrapping range is a complete set of declared tags. Pointer niches retain the CTFE nullability hook.

Equations

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

def Miri.Interpreter.Discriminant.writeDiscriminant {P S C V : Type} [Memory.PointerProvenance P] (h : DiscriminantHooks P S C V) (choice : C) (variant : Nat) (dest : V) : RvalueM S Unit

Equations

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