Physical LLVM architecture dispatch on the same canonical execution state. Pinned sources: intrinsics/mod.rs, intrinsics/x86/mod.rs and helpers.rs expect_target_feature_for_intrinsic. Target identity and features are compiler facts; host architecture and target-triple parsing are never substitutes.

def Miri.Input.EvalArchitectureMachine.targetArch (prepared : CompilerIntrinsicFacts.Prepared) : Except String String

Exact compiler session target.arch, added independently of target triple.

Equations

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

def Miri.Input.EvalArchitectureMachine.expectFeature {S : Type} (prepared : CompilerIntrinsicFacts.Prepared) (intrinsic feature : String) : EStateM Interpreter.StepError S Unit

helpers.rs:940–952: absent enabled ISA feature is UB, whereas absent compiler evidence is an unresolved input obligation.

Equations

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

def Miri.Input.EvalArchitectureMachine.dispatcher {K U C : Type} [DecidableEq K] (prepared : CompilerIntrinsicFacts.Prepared) (access : Interpreter.PlaceMachine.AccessConfig K (Interpreter.ValidityMachine.UserState U)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C Interpreter.MachineHooks.FrameExtra) (pointers : Interpreter.PointerMachine.Hooks K (Interpreter.ValidityMachine.Control U)) (choices : Interpreter.ExecutionChoices.Access (Interpreter.ValidityMachine.State K U)) (simd : Interpreter.IntrinsicSimdHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C (Interpreter.RuntimePlace Memory.Provenance)) (u128Layout : Interpreter.LocalLayout) (x86 : Interpreter.IntrinsicX86.Hooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C (Interpreter.RuntimePlace Memory.Provenance)) (base : Interpreter.IntrinsicArchitecture.DispatchHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C (Interpreter.RuntimePlace Memory.Provenance)) : Except String (Interpreter.IntrinsicArchitecture.DispatchHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C (Interpreter.RuntimePlace Memory.Provenance))

Install concrete SIMD projection/transmutes, all x86 families and shared choice-tape float perturbations. Only compiler type construction, signature checks, host sqrt and source numerical settings remain in the x86 leaf record. The scheduler yield updates the canonical ThreadManager directly.

Equations

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

def Miri.Input.EvalArchitectureMachine.bind {Os R P H D O Aff B Host C X ClockHost : Type} (prepared : CompilerIntrinsicFacts.Prepared) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host))) (u128Layout : Interpreter.LocalLayout) (x86 : Interpreter.IntrinsicX86.Hooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (base : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B Host) C O X ClockHost) : Except String (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B Host) C O X ClockHost)

Apply after EvalCoreMachine.config, so LLVM operations share its physical SIMD, access, projection, and scalar dictionaries. This does not reconstruct or capture an older fallback call chain. Existing core files need no modification.

Equations

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

def Miri.Input.EvalArchitectureMachine.compilerDispatcher {Os R P H D O Aff B Host C : Type} (context : CompilerFacts.Context) (prepared : CompilerIntrinsicFacts.Prepared) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host))) (checkSymbolClash : String → Interpreter.RvalueM (EvalCoreMachine.State Os R P H D O Aff B Host) Unit) (math : Interpreter.Math.Hooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B Host)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (simdBase : Interpreter.IntrinsicSimdHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (unsupportedForeignItem : String → String → Interpreter.StepError) : Except String (Interpreter.IntrinsicArchitecture.DispatchHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance))

Compiler-closed production entry: no caller-provided x86 implementation or layout-constructor callbacks. Signature symbol-clash and host math are the same source policies used by the enclosing foreign/intrinsic factory.

Equations

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

def Miri.Input.EvalArchitectureMachine.bindCompiler {Os R P H D O Aff B Host C X ClockHost : Type} (context : CompilerFacts.Context) (prepared : CompilerIntrinsicFacts.Prepared) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host))) (checkSymbolClash : String → Interpreter.RvalueM (EvalCoreMachine.State Os R P H D O Aff B Host) Unit) (math : Interpreter.Math.Hooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (base : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B Host) C O X ClockHost) : Except String (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B Host) C O X ClockHost)

Install the same direct constructor in an already assembled configuration.

Equations

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