Direct source intrinsic capability construction. Surviving compiler, choice, math and policy leaves are explicit; no base physical hook dictionary is accepted. Canonical operations match AtomicMachine.bind (data_race.rs:749–875), IntrinsicVectorMachine.bindSimd (intrinsics/simd.rs::emulate_simd_intrinsic), and IntrinsicMachine.bind (intrinsics/mod.rs::emulate_intrinsic_by_name). Only dictionary construction changes; source event order and partial-state behavior stay in those same operations.

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionIntrinsic.User (User : Type) : Type

Equations

• Miri.Interpreter.ExecutionIntrinsic.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionIntrinsic.State (K U : Type) : Type

Equations

• Miri.Interpreter.ExecutionIntrinsic.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionIntrinsic.M (K U A : Type) : Type

Equations

• Miri.Interpreter.ExecutionIntrinsic.M K U = Miri.Interpreter.ValidityMachine.M K U

structure Miri.Interpreter.ExecutionIntrinsic.Atomic.AccessLeaves (P S C V : Type) : Type

• loadChoiceRank : C → Nat → RvalueM S Nat
• weakPolicy : WeakCasPolicy
• weakSuccessChoice : C → RvalueM S Bool
• diagnostic : C → Concurrency.WeakMemoryDiagnostic → RvalueM S Unit
• classifyDispatchError : Concurrency.AtomicDispatchError → StepError
• classifyGlobalError : Concurrency.GlobalStateError → StepError

structure Miri.Interpreter.ExecutionIntrinsic.Atomic.Leaves (P S C V : Type) extends Miri.Interpreter.ExecutionIntrinsic.Atomic.AccessLeaves P S C V : Type

• loadChoiceRank : C → Nat → RvalueM S Nat
• weakPolicy : WeakCasPolicy
• weakSuccessChoice : C → RvalueM S Bool
• diagnostic : C → Concurrency.WeakMemoryDiagnostic → RvalueM S Unit
• classifyDispatchError : Concurrency.AtomicDispatchError → StepError
• classifyGlobalError : Concurrency.GlobalStateError → StepError
• orderingConst : C → Nat → RvalueM S Concurrency.AtomicOrdering
• volatileConst : C → Nat → RvalueM S Unit

def Miri.Interpreter.ExecutionIntrinsic.Atomic.access {K U C Payload : Type} [DecidableEq K] (leaves : AccessLeaves Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (scalarOps : ScalarOpsHooks Memory.Provenance (State K U) C) (access : PlaceMachine.AccessConfig K (User U)) (places : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (extras : MemoryExtras.Hooks K (User U) Payload) : AtomicAccessHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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

def Miri.Interpreter.ExecutionIntrinsic.Atomic.dispatcher {K U C : Type} [DecidableEq K] (physical : AtomicAccessHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (ordering : C → Nat → M K U Concurrency.AtomicOrdering) (volatile : C → Nat → M K U Unit) (deref : C → OpTy Memory.Provenance → M K U (RuntimePlace Memory.Provenance)) (accessConfig : PlaceMachine.AccessConfig K (User U)) (places : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (returnToBlock : C → Option MIR.BasicBlockId → M K U Unit) : IntrinsicAtomicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Dispatch adds only the actual full-callee constant queries and source MIR operand/continuation operations to the shared physical atomic engine.

Equations

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

def Miri.Interpreter.ExecutionIntrinsic.Atomic.make {K U C Payload : Type} [DecidableEq K] (leaves : Leaves Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (derefPointer : C → OpTy Memory.Provenance → M K U (RuntimePlace Memory.Provenance)) (scalarOps : ScalarOpsHooks Memory.Provenance (State K U) C) (returnToBlock : C → Option MIR.BasicBlockId → M K U Unit) (accessConfig : PlaceMachine.AccessConfig K (User U)) (places : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (extras : MemoryExtras.Hooks K (User U) Payload) : IntrinsicAtomicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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

structure Miri.Interpreter.ExecutionIntrinsic.Simd.Leaves (P S C V : Type) : Type

• boolTy : MIR.TyId
• u8Ty : MIR.TyId
• isSimd : C → MIR.TyId → RvalueM S Bool
• simdSizeAndType : C → MIR.TyId → RvalueM S (UInt64 × MIR.TyId)
• shuffleConst : C → Nat → RvalueM S (Array UInt32)
• alignmentConst : C → Nat → RvalueM S Memory.SimdAlignment
• chooseEqualFloatRight : C → FloatBits → FloatBits → RvalueM S Bool
• fuseMulAdd : C → RvalueM S Bool
• mathLane : C → SimdMathOp → OpTy P → V → RvalueM S Unit

def Miri.Interpreter.ExecutionIntrinsic.Simd.make {K U C : Type} [DecidableEq K] (leaves : Leaves Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (scalarOps : ScalarOpsHooks Memory.Provenance (State K U) C) (floatOps : FloatOpsHooks Memory.Provenance (State K U) C) (castHooks : CastHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (returnToBlock : C → Option MIR.BasicBlockId → RvalueM (State K U) Unit) (access : PlaceMachine.AccessConfig K (User U)) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (copy : PlaceCopyHooks Memory.Provenance (State K U) C) (pointerCompiler : PointerPlaceMachine.Compiler K U C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) : IntrinsicSimdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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

structure Miri.Interpreter.ExecutionIntrinsic.Core.Leaves (P S C V : Type) : Type

• varArgsFuel : Nat
• maxSizeOfVal : ABI.Size
• 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)
• 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)
• 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

def Miri.Interpreter.ExecutionIntrinsic.Core.make {K U C SyncPayload F A Padding : Type} [DecidableEq K] (leaves : Leaves Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (simdHooks : IntrinsicSimdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (atomicHooks : IntrinsicAtomicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (typeIdHooks : IntrinsicTypeIdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (varArgsHooks : IntrinsicVarArgsHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (evalOperand : C → MIR.Operand → RvalueM (State K U) (OpTy Memory.Provenance)) (evalOperandAt : C → OperandPath → MIR.Operand → RvalueM (State K U) (OpTy Memory.Provenance)) (derefPointer : C → OpTy Memory.Provenance → RvalueM (State K U) (RuntimePlace Memory.Provenance)) (immPointerToPlace : C → RvalueImmTy Memory.Provenance → RvalueM (State K U) (OpTy Memory.Provenance)) (scalarOps : ScalarOpsHooks Memory.Provenance (State K U) C) (floatOps : FloatOpsHooks Memory.Provenance (State K U) C) (readDiscriminant : C → OpTy Memory.Provenance → RvalueM (State K U) MIR.VariantIndex) (discriminantForVariant : C → MIR.TyId → MIR.VariantIndex → RvalueM (State K U) (RvalueImmTy Memory.Provenance)) (catchUnwind : C → OpTy Memory.Provenance → OpTy Memory.Provenance → OpTy Memory.Provenance → RuntimePlace Memory.Provenance → Option MIR.BasicBlockId → RvalueM (State K U) Unit) (returnToBlock : C → Option MIR.BasicBlockId → RvalueM (State K U) Unit) (access : PlaceMachine.AccessConfig K (User U)) (allocation : PlaceMachine.AllocationConfig K (User U)) (extras : MemoryExtras.Hooks K (User U) SyncPayload) (deallocateStack : Memory.Pointer (Option Memory.Provenance) → M K U Unit) (compiler : PlaceMachine.CompilerHooks K (User U) C) (places : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (copy : PlaceCopyHooks Memory.Provenance (State K U) C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (dynamicFuel : Nat) (validity : ValidityVisitor.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra F A Padding) (validationFuel : Nat) : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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