Effectful Projectable rules for canonical places. Dynamic field alignment can execute vtable/compiler/machine queries; those effects are threaded through the same interpreter state rather than converted into pure ProjectionCx fields. Source: projection.rs project_field/index/subslice/downcast; place.rs Projectable.

structure Miri.Interpreter.PlaceProjectionHooks (P S C E : Type) : Type

• place : PlaceHooks P S C E
• target : ABI.TargetDataLayout
• maxSizeOfVal : ABI.Size
• dynamic : DynamicLayoutHooks P S C
• dynamicFuel : Nat
• isSliceOrStr : C → MIR.TyId → PlaceM S Bool
• field : C → LocalLayout → Nat → PlaceM S LocalLayout
• variant : C → LocalLayout → Nat → PlaceM S LocalLayout
• packedAlign : C → MIR.TyId → PlaceM S (Option ABI.Align)
• subsliceLayout : C → LocalLayout → UInt64 → PlaceM S (LocalLayout × MemPlaceMeta P)
• layoutOf : C → MIR.TyId → PlaceM S LocalLayout
• localIndex : C → MIR.LocalId → PlaceM S UInt64

def Miri.Interpreter.PlaceDynamic.offsetWithMeta {P S C E : Type} (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (amount : ABI.Size) (mode : OffsetMode) (metaValue : MemPlaceMeta P) (layout : LocalLayout) : PlaceM S (RuntimePlace P)

Source PlaceTy::offset_with_meta, with actual effectful memory offset and checked local offset. Local places cannot carry metadata or unsized layouts.

Equations

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

def Miri.Interpreter.PlaceDynamic.length {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) : PlaceM S UInt64

Equations

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

def Miri.Interpreter.PlaceDynamic.field {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (index : Nat) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.downcast {P S C E : Type} (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (variant : Nat) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.index {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (index : UInt64) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.constantIndex {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (offset minLength : UInt64) (fromEnd : Bool) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.subslice {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (fromIndex to : UInt64) (fromEnd : Bool) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.project {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (base : RuntimePlace P) (elem : MIR.ProjectionElem) : PlaceM S (RuntimePlace P)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.PlaceDynamic.project h choice base (Miri.MIR.ProjectionElem.Field i ty) = Miri.Interpreter.PlaceDynamic.field h choice base i
• Miri.Interpreter.PlaceDynamic.project h choice base (Miri.MIR.ProjectionElem.Downcast name variant) = Miri.Interpreter.PlaceDynamic.downcast h choice base variant
• Miri.Interpreter.PlaceDynamic.project h choice base Miri.MIR.ProjectionElem.Deref = h.place.deref choice base false
• Miri.Interpreter.PlaceDynamic.project h choice base (Miri.MIR.ProjectionElem.OpaqueCast ty) = throw (Miri.Interpreter.StepError.invalidProgram "OpaqueCast after borrowck")
• Miri.Interpreter.PlaceDynamic.project h choice base Miri.MIR.ProjectionElem.PhantomDeref = throw (Miri.Interpreter.StepError.invalidProgram "PhantomDeref after borrowck")

def Miri.Interpreter.PlaceDynamic.evalPlace {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceProjectionHooks P S C E) (choice : C) (mirPlace : MIR.Place) (skipValidityForSimpleDeref : Bool) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.PlaceDynamic.memoryCopy {Kind P S C Extra HookState ProvExtra : Type} [DecidableEq Kind] [Memory.PointerProvenance P] (dynamic : DynamicLayoutHooks P S C) (choice : C) (fuel : Nat) (debugAssertions : Bool) (pointerSize : ABI.Size) (hooks : Memory.MemoryCopyHooks P Extra Kind HookState ProvExtra) (getMemory : S → Memory.MemoryState P Extra Kind) (getHooks : S → HookState) (putMemoryHooks : S → Memory.MemoryState P Extra Kind → HookState → S) (source dest : MPlaceTy P) : PlaceM S Unit

Whole-state dynamic layout adapter for the concrete Place slow-copy path.

Equations

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

def Miri.Interpreter.PlaceDynamic.mutableAccess {Kind P S C Extra HookState ProvExtra : Type} [DecidableEq Kind] [DecidableEq P] [Memory.PointerProvenance P] (dynamic : DynamicLayoutHooks P S C) (choice : C) (fuel : Nat) (context : LocalReadContext P Extra Kind HookState ProvExtra) (getMemory : S → Memory.MemoryState P Extra Kind) (getHooks : S → HookState) (putMemoryHooks : S → Memory.MemoryState P Extra Kind → HookState → S) (putTouched : S → Option (Memory.AllocationAccessRef P Extra) → S) (place : MPlaceTy P) : PlaceM S Unit

Dynamic mutable-place access runs effectful metadata layout first, then uses the resolved size as an operational ABI view for existing allocation access. Full type identity remains in the input; Foreign uses the source's fixed-size fallback. The canonical state and touched snapshots are committed before any allocation/access error is propagated.

Equations

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

def Miri.Interpreter.PlaceDynamic.withVTable {P S C F A : Type} (dynamic : DynamicLayoutHooks P S C) (vtable : VTableHooks P S C F A) : DynamicLayoutHooks P S C

Bind symbolic vtable checking and compiler layout lookup to dynamic trait size/alignment queries; predicate and global-resolution effects stay in S.

Equations

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