Pinned place.rs local_to_place/eval_place/force_allocation and mutable-local selection. Canonical layouts retain type identity across frame and memory forms. Memory and machine leaves are mandatory stateful operations.

@[reducible, inline]

abbrev Miri.Interpreter.PlaceM (S A : Type) : Type

Equations

• Miri.Interpreter.PlaceM S A = EStateM Miri.Interpreter.StepError S A

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

• getFrame : PlaceM S (Frame P LocalLayout E)
• setFrame : Frame P LocalLayout E → PlaceM S Unit
• debugAssertions : Bool
• frameIndex : PlaceM S Nat
• resolveLayout : C → MIR.LocalId → PlaceM S LocalLayout
• localToOp : C → MIR.LocalId → PlaceM S (OpTy P)

  Must invoke canonical immediate-local read hooks outside validation.

• projection : C → PlaceM S (ProjectionCx P)
• deref : C → RuntimePlace P → Bool → PlaceM S (RuntimePlace P)

  Normal deref performs pointer validity; simple deref bypass uses readImmediate followed by imm_ptr_to_mplace, precisely the skip flag's source distinction.

• checkPlaceType : C → MIR.Place → RuntimePlace P → PlaceM S Unit
• allocateStack : C → LocalLayout → PlaceM S (MPlaceTy P)
• writeMemoryNoValidate : C → Immediate P → MPlaceTy P → PlaceM S Unit
• afterLocalMovedToMemory : C → MIR.LocalId → MPlaceTy P → PlaceM S Unit

  Required machine hook: transfer vector clocks and declaration span to fresh allocation extras, preserving provenance/borrow state.

• memoryOffset : C → MemPlace P → ABI.Size → OffsetMode → MemPlaceMeta P → PlaceM S (MemPlace P)
• writeLocalImmediate : C → MIR.LocalId → LocalLayout → Immediate P → PlaceM S Unit
• enforceValidity : C → LocalLayout → PlaceM S Bool
• validate : C → RuntimePlace P → PlaceM S Unit

@[simp]

theorem Miri.Interpreter.placeLift_ok {A S : Type} (value : A) : Miri.Interpreter.placeLift✝ (Except.ok value) = pure value

Successful physical/compiler results lift without state effects.

@[simp]

theorem Miri.Interpreter.stackLift_ok {A S : Type} (value : A) : Miri.Interpreter.stackLift✝ (Except.ok value) = pure value

Successful stack results lift without changing interpreter state.

def Miri.Interpreter.placeLayoutOfLocal {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (localId : MIR.LocalId) : PlaceM S LocalLayout

Equations

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

theorem Miri.Interpreter.requireCurrent_eq {P S C E : Type} (h : PlaceHooks P S C E) (frame : Nat) : Miri.Interpreter.requireCurrent✝ h frame = do let __do_lift ← h.frameIndex if (__do_lift != frame) = true then throw (StepError.invalidProgram "place refers to another frame") else pure ()

Public source equation for the structural current-frame guard.

@[simp]

theorem Miri.Interpreter.checkLocalIdentity_debugOff {P S C E : Type} (h : PlaceHooks P S C E) (identity : LocalsIdentity) (off : h.debugAssertions = false) : Miri.Interpreter.checkLocalIdentity✝ h identity = pure ()

Debug-disabled local identity assertions are query-free.

def Miri.Interpreter.localToPlace {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (localId : MIR.LocalId) : PlaceM S (RuntimePlace P)

Equations

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

def Miri.Interpreter.projectRuntimePlace {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceHooks P S C E) (choice : C) (place : RuntimePlace P) (elem : MIR.ProjectionElem) : PlaceM S (RuntimePlace P)

Project local places without allocating or reading their values. Reuse the canonical projector with a local-offset carrier; its memoryOffset is replaced by source PlaceTy's checked Size addition, never a fabricated memory access.

Equations

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

def Miri.Interpreter.evalPlace {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceHooks 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.forceAllocation {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (place : RuntimePlace P) : PlaceM S (MPlaceTy P)

Allocation and old-value write precede machine migration, and only then is local storage replaced. Hook failures retain allocation/write effects, with the old local still immediate. Replacement fetches the current frame, preserving machine hook changes to race clocks and borrow metadata.

Equations

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

inductive Miri.Interpreter.MutablePlace (P : Type) : Type

• memory {P : Type} (place : MPlaceTy P) : MutablePlace P
• immediateLocal {P : Type} (localId : MIR.LocalId) (layout : LocalLayout) : MutablePlace P

def Miri.Interpreter.asMplaceOrMutableLocal {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (place : RuntimePlace P) : PlaceM S (MutablePlace P)

Equations

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

def Miri.Interpreter.writePlaceImmediateNoValidate {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (value : Immediate P) (dest : RuntimePlace P) : PlaceM S Unit

Equations

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

def Miri.Interpreter.writePlaceImmediate {P S C E : Type} (h : PlaceHooks P S C E) (choice : C) (value : Immediate P) (dest : RuntimePlace P) : PlaceM S Unit

Equations

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

def Miri.Interpreter.placeToOpCore {P S E : Type} {C : Sort u_1} [Memory.PointerProvenance P] (getFrame : PlaceM S (Frame P LocalLayout E)) (debugAssertions : Bool) (frameIndex : PlaceM S Nat) (localToOp : C → MIR.LocalId → PlaceM S (OpTy P)) (projection : C → PlaceM S (ProjectionCx P)) (choice : C) (place : RuntimePlace P) : PlaceM S (OpTy P)

Read-only capability slice of place-to-operand conversion. Keeping this slice explicit avoids recursive construction of a complete place dictionary.

Equations

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

def Miri.Interpreter.placeToOp {P S C E : Type} [Memory.PointerProvenance P] (h : PlaceHooks P S C E) (choice : C) (place : RuntimePlace P) : PlaceM S (OpTy P)

Equations

• Miri.Interpreter.placeToOp h choice place = Miri.Interpreter.placeToOpCore h.getFrame h.debugAssertions h.frameIndex h.localToOp h.projection choice place

def Miri.Interpreter.placeMemoryOffset {P ProvExtra S : Type} (target : Memory.PointerArithmetic) (resolve : Memory.PointerResolver P ProvExtra) (lookup : Memory.LiveAllocationLookup) (place : MemPlace P) (offset : ABI.Size) (mode : OffsetMode) (metadata : MemPlaceMeta P) : PlaceM S (MemPlace P)

Actual memory-place offset operation with target arithmetic and required live-allocation/provenance resolution, preserving cached misalignment.

Equations

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

def Miri.Interpreter.placeWriteLocalImmediate {S P E : Type} (getFrame : PlaceM S (Frame P LocalLayout E)) (setFrame : Frame P LocalLayout E → PlaceM S Unit) (validationInProgress : PlaceM S Bool) (afterLocalWrite : MIR.LocalId → Bool → PlaceM S Unit) (debugAbiCheck : Immediate P → LocalLayout → PlaceM S Unit) (localId : MIR.LocalId) (layout : LocalLayout) (value : Immediate P) : PlaceM S Unit

Whole-state optimized-local writer. The current frame is replaced before machine effects; subsequent hooks operate on that state directly, so canonical race clocks and borrow metadata are never overwritten by an old frame copy.

Equations

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

def Miri.Interpreter.placeAllocateStack {Kind P Extra HookState S : Type} [DecidableEq Kind] (maximumObjectSize : ABI.Size) (zeroedStorage : ABI.Size → ABI.Align → Option (Array UInt8)) (synchronizeMemory : Memory.MemoryState P Extra Kind → HookState → HookState) (initExtra : Memory.MemoryState P Extra Kind → HookState → Memory.AllocId → Memory.MemoryKind Kind → ABI.Size → ABI.Align → Memory.MemoryStateHookResult P Extra Kind HookState Extra) (adjustRoot : Memory.MemoryState P Extra Kind → HookState → Memory.AllocId → Memory.MemoryKind Kind → Memory.MemoryStateHookResult P Extra Kind HookState (Memory.Pointer P)) (getMemory : S → Memory.MemoryState P Extra Kind) (getHooks : S → HookState) (putMemoryHooks : S → Memory.MemoryState P Extra Kind → HookState → S) (layout : LocalLayout) : PlaceM S (MPlaceTy P)

Concrete stack materialization allocator. Root adjustment and allocation extras must install the canonical provenance, borrow tree and race clocks.

Equations

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

def Miri.Interpreter.placeMemoryWrite {Kind P Extra HookState ProvExtra S : Type} [DecidableEq Kind] [DecidableEq P] [Memory.PointerProvenance P] (context : LocalReadContext P Extra Kind HookState ProvExtra) (willValidate : MemoryOperandLayout → Bool) (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) (value : Immediate P) (place : MPlaceTy P) : PlaceM S Unit

Concrete bridge to the existing memory writer. Memory/hooks are committed before propagating errors; callers select canonical machine allocation hooks.

Equations

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

def Miri.Interpreter.placeReadRaw {Kind P Extra HookState ProvExtra S : Type} [DecidableEq Kind] [DecidableEq P] [Memory.PointerProvenance P] (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) (source : OpTy P) : PlaceM S (ImmediateOrPlace P)

Equations

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

def Miri.Interpreter.placeMemoryCopy {Kind P S Extra HookState ProvExtra : Type} [DecidableEq Kind] (debugAssertions : Bool) (pointerSize : ABI.Size) (sizeAndAlign : MPlaceTy P → PlaceM S (Option (ABI.Size × ABI.Align))) (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

Source slow-copy path: destination dynamic size, debug source size (or fixed-part approximation), nonoverlapping memory copy, then cached alignment checks in source/destination order. Memory hooks and partial writes survive UB.

Equations

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

structure Miri.Interpreter.PlaceCopyHooks (P S C : Type) : Type

• compatible : LocalLayout → LocalLayout → Except StepError Bool
• hasPadding : LocalLayout → Except StepError Bool
• readRaw : C → OpTy P → PlaceM S (ImmediateOrPlace P)
• memoryCopy : C → MPlaceTy P → MPlaceTy P → PlaceM S Unit

  Resolve dynamic sizes; require sizes compatible; mem_copy nonoverlapping true; check source then destination misalignment only after memory copy.

• validateSource : C → LocalLayout → RuntimePlace P → PlaceM S Unit

  Source-layout validation pass includes transmute, recursive policy and reset of provenance/padding. Destination validation is done by PlaceHooks.

def Miri.Interpreter.copyRuntimePlaceNoValidate {P S C E : Type} (h : PlaceHooks P S C E) (copy : PlaceCopyHooks P S C) (choice : C) (source : OpTy P) (dest : RuntimePlace P) (allowTransmute : Bool) : PlaceM S Unit

Connected copy_op_no_validate, with materialization through forceAllocation. All type identity stays canonical; the memory read result supplies only bytes.

Equations

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

def Miri.Interpreter.copyRuntimePlace {P S C E : Type} (h : PlaceHooks P S C E) (copy : PlaceCopyHooks P S C) (choice : C) (source : OpTy P) (dest : RuntimePlace P) (allowTransmute : Bool) : PlaceM S Unit

Equations

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