Direct place/compiler construction from pinned interpret/{place,operand, projection,eval_context}.rs. No complete fallback compiler or projection record is accepted. Validation is the actual visitor supplied by the final assembly; the debug type assertion is a genuine compiler query, not an execution oracle.

@[reducible, inline]

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

Equations

• Miri.Input.EvalPlaceConstruction.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalPlaceConstruction.State = Miri.Input.EvalCoreMachine.State

structure Miri.Input.EvalPlaceConstruction.Options : Type

• debugAssertions : Bool
• maxSizeOfVal : ABI.Size
• dynamicFuel : Nat
• validation : Interpreter.ValidityMachine.ValidationMode

def Miri.Input.EvalPlaceConstruction.localLayout {K U : Type} (p : CompilerProviders.Prepared) (id : LocalId) : Interpreter.MachineHooks.M K U Interpreter.LocalLayout

Same cache/read sequence as layout_of_local: cached layouts do not query normalization again; a failed query cannot install a layout.

Equations

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

def Miri.Input.EvalPlaceConstruction.dynamic {Os R P H D O Aff B Host C F A : Type} (p : CompilerProviders.Prepared) (options : Options) (vtable : Interpreter.VTableHooks Memory.Provenance (State Os R P H D O Aff B Host) C F A) : Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R P H D O Aff B Host) C

Equations

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

def Miri.Input.EvalPlaceConstruction.compiler {Os R P H D O Aff B Host C F A : Type} (p : CompilerProviders.Prepared) (options : Options) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored Os R P H D O Aff B Host)) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host))) (vtable : Interpreter.VTableHooks Memory.Provenance (State Os R P H D O Aff B Host) C F A) (checkPlaceType : C → MIR.Place → Interpreter.RuntimePlace Memory.Provenance → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (validate : C → Interpreter.RuntimePlace Memory.Provenance → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C

The configured validation mode is the source Machine option. Final state construction must install that same mode; actual enforce/ghost checks sample the live state. Production place writes use scoped ValidityMachine.placeHooks.

Equations

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

def Miri.Input.EvalPlaceConstruction.projection {Os R P H D O Aff B Host C F A : Type} (p : CompilerProviders.Prepared) (options : Options) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored Os R P H D O Aff B Host)) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C) (vtable : Interpreter.VTableHooks Memory.Provenance (State Os R P H D O Aff B Host) C F A) : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra

Complete projection dictionary, including stateful runtime array interning, physical vtable alignment and actual optimized-local reads.

Equations

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