Pinned core intrinsics/simd.rs and Miri intrinsics/simd.rs dispatch. Every lane retains its canonical compiler type and full pointer provenance; projection, memory and compiler dependencies remain required typed effects.

inductive Miri.Interpreter.SimdMathOp : Type

• sqrt : SimdMathOp
• sin : SimdMathOp
• cos : SimdMathOp
• exp : SimdMathOp
• exp2 : SimdMathOp
• log : SimdMathOp
• log2 : SimdMathOp
• log10 : SimdMathOp

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqSimdMathOp : DecidableEq SimdMathOp

Equations

• Miri.Interpreter.instDecidableEqSimdMathOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.instReprSimdMathOp.repr : SimdMathOp → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprSimdMathOp : Repr SimdMathOp

Equations

• Miri.Interpreter.instReprSimdMathOp = { reprPrec := Miri.Interpreter.instReprSimdMathOp.repr }

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

• target : ABI.TargetDataLayout
• boolTy : MIR.TyId
• u8Ty : MIR.TyId
• isSimd : C → MIR.TyId → RvalueM S Bool
• simdSizeAndType : C → MIR.TyId → RvalueM S (UInt64 × MIR.TyId)
• forceAllocation : C → V → RvalueM S V
• placeLayout : V → ABI.TyAndLayout MIR.TyId
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• fieldRead : C → OpTy P → Nat → RvalueM S (OpTy P)
• fieldWrite : C → V → Nat → RvalueM S V
• fieldLayout : C → ABI.TyAndLayout MIR.TyId → Nat → RvalueM S (ABI.TyAndLayout MIR.TyId)
• indexRead : C → OpTy P → UInt64 → RvalueM S (OpTy P)
• indexWrite : C → V → UInt64 → RvalueM S V
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• writeImmediate : C → Immediate P → V → RvalueM S Unit
• copyOp : C → OpTy P → V → RvalueM S Unit
• derefImmediate : C → RvalueImmTy P → RvalueM S V
• readPlaceImmediate : C → V → RvalueM S (RvalueImmTy P)
• unalignedPlace : C → Memory.Pointer (Option P) → ABI.TyAndLayout MIR.TyId → RvalueM S V
• checkAlign : C → Memory.Pointer (Option P) → ABI.Align → RvalueM S Unit
• readBytes : C → Memory.Pointer (Option P) → ABI.Size → RvalueM S (Array UInt8)
• writeBytes : C → Memory.Pointer (Option P) → Array UInt8 → RvalueM S Unit
• shuffleConst : C → Nat → RvalueM S (Array UInt32)
• alignmentConst : C → Nat → RvalueM S Memory.SimdAlignment
• scalarOps : ScalarOpsHooks P S C
• floatOps : FloatOpsHooks P S C
• castHooks : CastHooks P S C V
• chooseEqualFloatRight : C → FloatBits → FloatBits → RvalueM S Bool
• fuseMulAdd : C → RvalueM S Bool
• mathLane : C → SimdMathOp → OpTy P → V → RvalueM S Unit
• returnToBlock : C → Option MIR.BasicBlockId → RvalueM S Unit

def Miri.Interpreter.IntrinsicSimd.elementToBool {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicSimdHooks P S C V) (choice : C) (value : RvalueImmTy P) : RvalueM S Bool

Equations

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

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

Core always forces the destination before dispatch; lane effects occur in source order and remain committed when a later lane fails.