Source scalar/memory/pointer intrinsic dispatch from pinned core interpret/intrinsics.rs and Miri intrinsics/{mod,math}.rs. Unhandled names return false for source MIR fallback; recognized missing families fail visibly. No arithmetic branch delegates to a generic name-to-result callback.

structure Miri.Interpreter.IntrinsicHooks (P S C V : Type) : Type

• simdHooks : IntrinsicSimdHooks P S C V
• atomicHooks : IntrinsicAtomicHooks P S C V
• typeIdHooks : IntrinsicTypeIdHooks P S C V
• varArgsHooks : IntrinsicVarArgsHooks P S C V
• varArgsFuel : Nat
• target : ABI.TargetDataLayout
• pointerOffset : ABI.Size

  Scalar::from_target_usize uses pointer_offset; target-sized reads use pointer_size.

• maxSizeOfVal : ABI.Size
• destLayout : V → ABI.TyAndLayout MIR.TyId
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• pointeeType : C → MIR.TyId → RvalueM S MIR.TyId
• integerKind : C → MIR.TyId → RvalueM S MIR.IntegerKind
• usizeLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• isizeLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• evalOperand : C → MIR.Operand → RvalueM S (OpTy P)
• evalOperandAt : C → OperandPath → MIR.Operand → RvalueM S (OpTy P)
• writeImmediate : C → Immediate P → V → RvalueM S Unit
• writePointer : C → Memory.Pointer (Option P) → V → RvalueM S Unit
• copyOp : C → OpTy P → V → RvalueM S Unit
• placeToOp : C → V → RvalueM S (OpTy P)
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• derefPointer : C → OpTy P → RvalueM S V
• immPointerToPlace : C → RvalueImmTy P → RvalueM S (OpTy P)
• dynamicSizeAlign : C → OpTy P → RvalueM S (Option (ABI.Size × ABI.Align))
• scalarOps : ScalarOpsHooks P S C
• floatOps : FloatOpsHooks P S C
• applyFloatNondeterminism : C → RvalueImmTy P → RvalueM S (RvalueImmTy P)
• chooseEqualFloatRight : C → FloatBits → FloatBits → RvalueM S Bool
• fuseMulAdd : C → RvalueM S Bool
• floatFastError : C → RvalueImmTy P → Nat → RvalueM S (RvalueImmTy P)
• checkAlign : C → Memory.Pointer (Option P) → ABI.Align → RvalueM S Unit
• memCopy : C → Memory.Pointer (Option P) → Memory.Pointer (Option P) → ABI.Size → Bool → RvalueM S Unit
• writeBytes : C → Memory.Pointer (Option P) → UInt8 → ABI.Size → RvalueM S Unit
• readBytesStripProvenance : C → Memory.Pointer (Option P) → ABI.Size → RvalueM S (Array UInt8)
• allocateStack : C → ABI.TyAndLayout MIR.TyId → RvalueM S V
• deallocateStack : C → Memory.Pointer (Option P) → RvalueM S Unit
• enforceValidity : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• enforceValidityRecursively : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• validatePlace : C → V → Bool → Bool → RvalueM S Unit
• tryAllocId : C → Memory.Pointer (Option P) → RvalueM S (Except UInt64 (Memory.AllocId × ABI.Size))
• checkSignedAccess : C → Memory.Pointer (Option P) → Int64 → RvalueM S (Except StepError Unit)
• vtableSizeAlign : C → Memory.Pointer (Option P) → Option Nat → RvalueM S (ABI.Size × ABI.Align)
• readDiscriminant : C → OpTy P → RvalueM S MIR.VariantIndex
• discriminantForVariant : C → MIR.TyId → MIR.VariantIndex → RvalueM S (RvalueImmTy P)
• variantLayout : C → ABI.TyAndLayout MIR.TyId → Nat → RvalueM S (ABI.TyAndLayout MIR.TyId)
• ensureMonomorphic : C → MIR.TyId → RvalueM S Unit
• typeNameConstant : C → MIR.TyId → ABI.TyAndLayout MIR.TyId → RvalueM S (OpTy P)
• needsDrop : C → MIR.TyId → RvalueM S Bool
• variantCount : C → MIR.TyId → RvalueM S Nat
• callerLocationConstant : C → ABI.TyAndLayout MIR.TyId → RvalueM S (OpTy P)
• chooseStaticKnown : C → RvalueM S Bool
• catchUnwind : C → OpTy P → OpTy P → OpTy P → V → Option MIR.BasicBlockId → RvalueM S Unit
• returnToBlock : C → Option MIR.BasicBlockId → RvalueM S Unit
• mathHooks : Option (Math.Hooks P S C V)

  Optional source Miri math-family implementation. This is a typed capability, not a name/result oracle; ordinary core operations remain in their existing branches and the math family is consulted only at the unknown-intrinsic fallback point.

structure Miri.Interpreter.MemoryIntrinsicHooks (P S C : Type) : Type

Shared memory operations need no function instance, generic-constant queries, SIMD/atomic dispatcher, return destination or fallback dictionary.

• target : ABI.TargetDataLayout
• maxSizeOfVal : ABI.Size
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• pointeeType : C → MIR.TyId → RvalueM S MIR.TyId
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• checkAlign : C → Memory.Pointer (Option P) → ABI.Align → RvalueM S Unit
• memCopy : C → Memory.Pointer (Option P) → Memory.Pointer (Option P) → ABI.Size → Bool → RvalueM S Unit

def Miri.Interpreter.IntrinsicHooks.memory {P S C V : Type} (h : IntrinsicHooks P S C V) : MemoryIntrinsicHooks P S C

Equations

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

def Miri.Interpreter.Intrinsics.copyWith {P S C : Type} [Memory.PointerProvenance P] (h : MemoryIntrinsicHooks P S C) (choice : C) (source dest count : OpTy P) (nonoverlapping : Bool) : RvalueM S Unit

Source count read precedes pointee layout and multiplication; pointer reads and alignment checks follow, including for zero-length copies.

Equations

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

def Miri.Interpreter.Intrinsics.copy {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (source dest count : OpTy P) (nonoverlapping : Bool) : RvalueM S Unit

Equations

• Miri.Interpreter.Intrinsics.copy h choice source dest count nonoverlapping = Miri.Interpreter.Intrinsics.copyWith h.memory choice source dest count nonoverlapping

def Miri.Interpreter.Intrinsics.writeBytes {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (dest byte count : OpTy P) : RvalueM S Unit

Equations

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

def Miri.Interpreter.Intrinsics.compareBytes {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (left right count : OpTy P) : RvalueM S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.Intrinsics.rawEq {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (left right : OpTy P) : RvalueM S Bool

Equations

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

def Miri.Interpreter.Intrinsics.typedSwap {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (left right : OpTy P) : RvalueM S Unit

Equations

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

def Miri.Interpreter.Intrinsics.pointerOffsetFrom {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (a b : OpTy P) (pointee : MIR.TyId) (unsigned : Bool) (dest : V) : RvalueM S Unit

Core ptr_offset_from computes addresses only for address provenance, or common-allocation offsets otherwise; both directed ranges must be valid.

Equations

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

def Miri.Interpreter.Intrinsics.floatIntrinsic {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (name : String) (args : Array (OpTy P)) (dest : V) : RvalueM S Bool

Portable suffixed float intrinsic families, including genuinely fused FMA. Only the machine's choice of fusion/equal operand/NaN remains effectful.

Equations

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

def Miri.Interpreter.Intrinsics.eval {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (name : String) (types : Array MIR.TyId) (args : Array (OpTy P)) (dest : V) (ret : Option MIR.BasicBlockId) : RvalueM S Bool

Source handled-result distinction: false permits the compiler's intrinsic MIR fallback. This never manufactures a successful result for an unknown name.

def Miri.Interpreter.Intrinsics.arithmetic {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (op : MIR.BinOp) (left right : OpTy P) (dest : V) : RvalueM S Unit

MIR fallback arithmetic uses the existing concrete scalar engine; intrinsic names that the pinned dispatcher does not intercept must enter that fallback rather than acquiring invented dispatcher behavior.

Equations

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

def Miri.Interpreter.Intrinsics.memoryCopyAdapter {K P E H PE : Type} {C : Sort u_1} [DecidableEq K] (target : ABI.TargetDataLayout) (hooks : Memory.MemoryCopyHooks P E K H PE) (classifyError : Memory.MemoryLifecycleError → StepError) (choice : C) (source dest : Memory.Pointer (Option P)) (size : ABI.Size) (nonoverlapping : Bool) : RvalueM (Memory.MemoryState P E K × H) Unit

Actual memory-copy primitive adapter, preserving updated memory and machine state even on failure. Error classification is an explicit required boundary.

Equations

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

def Miri.Interpreter.Intrinsics.evalNondivergingWith {P S C : Type} [Memory.PointerProvenance P] (h : MemoryIntrinsicHooks P S C) (evalOperandAt : C → OperandPath → MIR.Operand → RvalueM S (OpTy P)) (choice : C) (intrinsic : MIR.NonDivergingIntrinsic) : RvalueM S Unit

Source statement intrinsics preserve operand evaluation order and UB.

Equations

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

def Miri.Interpreter.Intrinsics.evalNondiverging {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicHooks P S C V) (choice : C) (intrinsic : MIR.NonDivergingIntrinsic) : RvalueM S Unit

Equations

• Miri.Interpreter.Intrinsics.evalNondiverging h choice intrinsic = Miri.Interpreter.Intrinsics.evalNondivergingWith h.memory h.evalOperandAt choice intrinsic