Physical projection and canonical type/layout queries on the final World. Source: interpret/{projection,operand,place}.rs and eval_context.rs. Pure immediate views are snapshots; indirect/dynamic effects use PlaceDynamic.

@[reducible, inline]

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

Equations

• Miri.Input.EvalProjectionMachine.User = Miri.Input.EvalBackendMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalProjectionMachine.State = Miri.Input.EvalBackendMachine.State

def Miri.Input.EvalProjectionMachine.arrays {Os R P H D O Aff B Host : Type} : RuntimeArrayQueries.Access (State 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.EvalProjectionMachine.packed (runtime : RuntimeMetadata) (ty : MIR.TyId) : Except Interpreter.ProjectionError (Option ABI.Align)

Equations

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

def Miri.Input.EvalProjectionMachine.field (world : RuntimeArrayTypes.World) (layout : Interpreter.LocalLayout) (index : Nat) : Except Interpreter.ProjectionError Interpreter.LocalLayout

Equations

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

def Miri.Input.EvalProjectionMachine.assertAbi (target : ABI.RuntimeTargetDataLayout) (value : Interpreter.Immediate Memory.Provenance) (layout : ABI.LayoutData) : Except Interpreter.ProjectionError Unit

Exact source ABI shape assertion, including provenance restriction on non-pointer scalars. It does not validate initialized scalar values.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalProjectionMachine.assertAbi target value✝ layout = throw (Miri.Interpreter.ProjectionError.invariant "immediate does not match ABI")

def Miri.Input.EvalProjectionMachine.memoryOffset {Os R P H D O Aff B Host : Type} (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (snapshot : State Os R P H D O Aff B Host) (place : Interpreter.MemPlace Memory.Provenance) (offset : ABI.Size) (mode : Interpreter.OffsetMode) (metadata : Interpreter.MemPlaceMeta Memory.Provenance) : Except Interpreter.ProjectionError (Interpreter.MemPlace Memory.Provenance)

The source metadata guard and signed conversion precede resolution. Zero offset and wrapping mode never consult the address/allocation maps.

Equations

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

def Miri.Input.EvalProjectionMachine.context {Os R P H D O Aff B Host : Type} (prepared : CompilerFactAdapters.Prepared) (maxSizeOfVal : ABI.Size) (debug : Bool) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (snapshot : State Os R P H D O Aff B Host) : Interpreter.ProjectionCx Memory.Provenance

Only immediate operations use this pure snapshot. Dynamic indirect fields, MIR dereference/local index and constructor-allocating subslices have actual stateful adapters; trying those effects here is an explicit obligation.

Equations

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

def Miri.Input.EvalProjectionMachine.dynamicKind (prepared : CompilerFactAdapters.Prepared) (ty : MIR.TyId) : Except Interpreter.ProjectionError Interpreter.DynamicTypeKind

Equations

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

def Miri.Input.EvalProjectionMachine.dynamic {Os R P H D O Aff B Host C : Type} (prepared : CompilerFactAdapters.Prepared) (base : Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R P H D O Aff B Host) C) : 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.EvalProjectionMachine.subslice {Os R P H D O Aff B Host : Type} (base : Interpreter.LocalLayout) (count : UInt64) : EStateM Interpreter.StepError (State Os R P H D O Aff B Host) (Interpreter.LocalLayout × Interpreter.MemPlaceMeta Memory.Provenance)

Array constructor effects occur after caller bounds/stride checks. Slice metadata is converted with the actual target pointer width.

Equations

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

def Miri.Input.EvalProjectionMachine.bindCompiler {Os R P H D O Aff B Host C : Type} (prepared : CompilerFactAdapters.Prepared) (maxSizeOfVal : ABI.Size) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (base : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C) : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User 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.EvalProjectionMachine.bindProjection {Os R P H D O Aff B Host C : Type} (prepared : CompilerFactAdapters.Prepared) (base : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra

Equations

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