Ordinary scalar/typed-pointer providers from exact imported rustc facts. Type identity comes from canonical input IDs and source query evidence, never layout size, pointer bytes or diagnostic type spelling.

@[reducible, inline]

abbrev Miri.Interpreter.CompilerExecutionProviders.Result (α : Type u_1) : Type u_1

Equations

• Miri.Interpreter.CompilerExecutionProviders.Result = Except Miri.Interpreter.StepError

def Miri.Interpreter.CompilerExecutionProviders.integerKind (facts : Input.CompilerFacts.Context) (ty : MIR.TyId) : Result MIR.IntegerKind

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.format (facts : Input.CompilerFacts.Context) (ty : MIR.TyId) : Result FloatFormat

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.scalarClass (facts : Input.CompilerFacts.Context) (ty : MIR.TyId) : Result ScalarTypeClass

Source is_any_ptr includes function pointers, while unary PtrMetadata does not. The separate category prevents the provider from admitting extra MIR.

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.metadataLayout (facts : Input.CompilerFacts.Context) (pointer : MIR.TyId) : Result LocalLayout

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.floatHooks {P S C : Type} (facts : Input.CompilerFacts.Context) (base : FloatOpsHooks P S C) : FloatOpsHooks P S C

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.scalarHooks {P S C : Type} [Memory.PointerProvenance P] (facts : Input.CompilerFacts.Context) (floats : FloatOpsHooks P S C) (base : ScalarOpsHooks P S C) : ScalarOpsHooks P S C

The exact Ordering language-item type is a required readonly compiler query, supplied by CompilerPrimitiveFacts; it cannot be inferred from an enum name or its three discriminants. All other scalar compiler leaves are closed.

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.pointerCompiler {K U C : Type} (prepared : Input.CompilerFactAdapters.Prepared) : PointerPlaceMachine.Compiler K U C

Compiler classification for pointer→place construction/dereference. The Box test uses source is_global_box rather than scalar ABI shape.

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.projectBox {K U C : Type} (facts : Input.CompilerFacts.Context) (runtime : Input.CompilerRuntimeQueries.Prepared) (projection : PlaceProjectionHooks Memory.Provenance (ValidityMachine.State K U) C MachineHooks.FrameExtra) (choice : C) (source : RuntimePlace Memory.Provenance) : ValidityMachine.M K U (RuntimePlace Memory.Provenance × RuntimePlace Memory.Provenance)

Source project_to_ptr_in_box: both field projections precede boxed_ty, mutable raw-pointer type construction and wrapping transmute.

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.machineScalarHooks {K U C F A : Type} [DecidableEq K] (prepared : Input.CompilerFactAdapters.Prepared) (access : ValidityMachine.Access K U) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (dynamic : DynamicLayoutHooks Memory.Provenance (ValidityMachine.State K U) C) (vtable : VTableHooks Memory.Provenance (ValidityMachine.State K U) C F A) (fuel : Nat) (floats : FloatOpsHooks Memory.Provenance (ValidityMachine.State K U) C) (base : ScalarOpsHooks Memory.Provenance (ValidityMachine.State K U) C) : ScalarOpsHooks Memory.Provenance (ValidityMachine.State K U) C

Complete scalar arithmetic dictionary on the canonical machine: compiler class/result types, exact FloatOps, real Miri pointers and pointer validity.

Equations

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

def Miri.Interpreter.CompilerExecutionProviders.rvalueHooks {K U C V : Type} (scalar : ScalarOpsHooks Memory.Provenance (ValidityMachine.State K U) C) (base : RvalueHooks Memory.Provenance (ValidityMachine.State K U) C V) : RvalueHooks Memory.Provenance (ValidityMachine.State K U) C V

Install exactly that dictionary at the MIR evaluation boundary. Choice, operand evaluation and source result-layout assertions stay in Rvalue.

Equations

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