Source-owned construction for the one EvalWorld. These constructors accept actual compiler/host capabilities, never a baseline ExecutionMachine.Config or placeholder operational records. The remaining top-level assembly is built on these same persistent registry, address, frame and source-choice stores.

@[reducible, inline]

abbrev Miri.Input.EvalConfiguration.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalConfiguration.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

abbrev Miri.Input.EvalConfiguration.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalConfiguration.State = Miri.Input.EvalCoreMachine.State

@[reducible, inline]

abbrev Miri.Input.EvalConfiguration.Stored (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalConfiguration.Stored = Miri.Input.EvalCoreMachine.Stored

def Miri.Input.EvalConfiguration.functions {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (crossCrateInlineAlways : Bool) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O

Exact source machine option; Always short-circuits inline_never just as FunctionPointers.globalSalt does. No inline classification is inferred.

Equations

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

def Miri.Input.EvalConfiguration.symbols {Os R P H D O Aff B Host : Type} : Interpreter.IntrinsicSymbolsMachine.Access (User Os R P H D O Aff B Host)

Real symbolic memory maps, distinct from function/vtable registries. Empty initial maps are rustc Memory::new; neither map adds provenance GC roots.

Equations

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

def Miri.Input.EvalConfiguration.identity {Os R P H D O Aff B Host : Type} : Interpreter.ExecutionCallLeaves.IdentityAccess (User Os R P H D O Aff B Host)

Equations

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

def Miri.Input.EvalConfiguration.allocation {Os R P H D O Aff B Host : Type} (maximumObjectSize : ABI.Size) (storage : ABI.Size → ABI.Align → Option (Array UInt8)) (diagnostic : Memory.AllocId → ABI.Size → ABI.Align → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)

Host byte storage and allocation diagnostics are explicit. Root address selection, weak-memory extras and actual backend inspection are source code, not caller supplied successful allocation hooks.

Equations

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