The typed-immediate branch of pinned operand.rs and place.rs. The MemoryOperandLayout is only the TyAndLayout projection consumed here; ABI backend representations and scalar sizing come directly from rustc_abi's runtime-layout port. Pointer resolution, global lookup, and Miri access hooks are delegated to the required AllocationAccess and dynamic-layout hooks.

@[reducible, inline]

abbrev Miri.Interpreter.BackendPrimitive : Type

Equations

• Miri.Interpreter.BackendPrimitive = Miri.ABI.Primitive

structure Miri.Interpreter.MemoryOperandLayout : Type

• size : ABI.Size
• align : ABI.Align
• backendRepr : ABI.BackendRepr
• canonicalType : Option Nat

  Canonical compiler type identity, retained for effectful unsized layout. Byte-level standalone views may omit it; typed machine views never do.

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemoryOperandLayout : DecidableEq MemoryOperandLayout

Equations

• Miri.Interpreter.instDecidableEqMemoryOperandLayout = Miri.Interpreter.instDecidableEqMemoryOperandLayout.decEq

def Miri.Interpreter.instDecidableEqMemoryOperandLayout.decEq (x✝ x✝¹ : MemoryOperandLayout) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprMemoryOperandLayout : Repr MemoryOperandLayout

Equations

• Miri.Interpreter.instReprMemoryOperandLayout = { reprPrec := Miri.Interpreter.instReprMemoryOperandLayout.repr }

def Miri.Interpreter.instReprMemoryOperandLayout.repr : MemoryOperandLayout → Nat → Std.Format

Equations

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

structure Miri.Interpreter.MemoryOperandPlace (Prov : Type) : Type

• mplace : MemPlace Prov
• layout : MemoryOperandLayout

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemoryOperandPlace {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (MemoryOperandPlace Prov✝)

Equations

• Miri.Interpreter.instDecidableEqMemoryOperandPlace = Miri.Interpreter.instDecidableEqMemoryOperandPlace.decEq

def Miri.Interpreter.instDecidableEqMemoryOperandPlace.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : MemoryOperandPlace Prov✝) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.instReprMemoryOperandPlace.repr {Prov✝ : Type} [Repr Prov✝] : MemoryOperandPlace Prov✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprMemoryOperandPlace {Prov✝ : Type} [Repr Prov✝] : Repr (MemoryOperandPlace Prov✝)

Equations

• Miri.Interpreter.instReprMemoryOperandPlace = { reprPrec := Miri.Interpreter.instReprMemoryOperandPlace.repr }

structure Miri.Interpreter.ImmediateValue (Prov : Type) : Type

• value : Immediate Prov
• layout : MemoryOperandLayout

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqImmediateValue {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (ImmediateValue Prov✝)

Equations

• Miri.Interpreter.instDecidableEqImmediateValue = Miri.Interpreter.instDecidableEqImmediateValue.decEq

def Miri.Interpreter.instDecidableEqImmediateValue.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : ImmediateValue Prov✝) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.instReprImmediateValue.repr {Prov✝ : Type} [Repr Prov✝] : ImmediateValue Prov✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprImmediateValue {Prov✝ : Type} [Repr Prov✝] : Repr (ImmediateValue Prov✝)

Equations

• Miri.Interpreter.instReprImmediateValue = { reprPrec := Miri.Interpreter.instReprImmediateValue.repr }

inductive Miri.Interpreter.ImmediateOrPlace (Prov : Type) : Type

• place {Prov : Type} (value : MemoryOperandPlace Prov) : ImmediateOrPlace Prov
• immediate {Prov : Type} (value : ImmediateValue Prov) : ImmediateOrPlace Prov

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqImmediateOrPlace {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (ImmediateOrPlace Prov✝)

Equations

• Miri.Interpreter.instDecidableEqImmediateOrPlace = Miri.Interpreter.instDecidableEqImmediateOrPlace.decEq

def Miri.Interpreter.instDecidableEqImmediateOrPlace.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : ImmediateOrPlace Prov✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqImmediateOrPlace.decEq (Miri.Interpreter.ImmediateOrPlace.place a) (Miri.Interpreter.ImmediateOrPlace.place b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateOrPlace.decEq (Miri.Interpreter.ImmediateOrPlace.place value) (Miri.Interpreter.ImmediateOrPlace.immediate value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateOrPlace.decEq (Miri.Interpreter.ImmediateOrPlace.immediate value) (Miri.Interpreter.ImmediateOrPlace.place value_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprImmediateOrPlace {Prov✝ : Type} [Repr Prov✝] : Repr (ImmediateOrPlace Prov✝)

Equations

• Miri.Interpreter.instReprImmediateOrPlace = { reprPrec := Miri.Interpreter.instReprImmediateOrPlace.repr }

def Miri.Interpreter.instReprImmediateOrPlace.repr {Prov✝ : Type} [Repr Prov✝] : ImmediateOrPlace Prov✝ → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.MemoryOperandError : Type

• runtimeLayout (error : ABI.RuntimeLayoutError) : MemoryOperandError
• scalarLayout (error : ABI.ScalarLayoutError) : MemoryOperandError
• pointerAccess (error : Memory.PtrAllocationError) : MemoryOperandError
• dynamicLayoutFailure (message : String) : MemoryOperandError
• allocation (error : Memory.AllocError) : MemoryOperandError
• memoryRange (error : Memory.MemoryError) : MemoryOperandError
• sourceInvariant (message : String) : MemoryOperandError
• immediate (error : ImmediateError) : MemoryOperandError
• invalidPrimitiveRead : MemoryOperandError
• rawReadReturnedPlace : MemoryOperandError
• invalidUninitBytes : MemoryOperandError
• unsizedImmediateWrite : MemoryOperandError
• immediateAbiMismatch : MemoryOperandError
• immediateSizeMismatch (expected actual : ABI.Size) : MemoryOperandError
• immediateCarriesNonPointerProvenance : MemoryOperandError
• memoryUpdate (error : Memory.AllocationLookupError) : MemoryOperandError

def Miri.Interpreter.instDecidableEqMemoryOperandError.decEq (x✝ x✝¹ : MemoryOperandError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemoryOperandError : DecidableEq MemoryOperandError

Equations

• Miri.Interpreter.instDecidableEqMemoryOperandError = Miri.Interpreter.instDecidableEqMemoryOperandError.decEq

def Miri.Interpreter.instReprMemoryOperandError.repr : MemoryOperandError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprMemoryOperandError : Repr MemoryOperandError

Equations

• Miri.Interpreter.instReprMemoryOperandError = { reprPrec := Miri.Interpreter.instReprMemoryOperandError.repr }

structure Miri.Interpreter.MemoryOperandResult (Prov Extra MachineKind HookState α : Type) : Type

• memory : Memory.MemoryState Prov Extra MachineKind
• hooks : HookState
• touched : Option (Memory.AllocationAccessRef Prov Extra)

  Updated allocation extras from access hooks, including on hook failure.

• outcome : Except MemoryOperandError α

structure Miri.Interpreter.DynamicLayoutResult (Prov Extra MachineKind HookState : Type) : Type

• memory : Memory.MemoryState Prov Extra MachineKind
• hooks : HookState
• outcome : Except String (Option (ABI.Size × ABI.Align))

@[reducible, inline]

abbrev Miri.Interpreter.DynamicLayoutResolver (Prov Extra MachineKind HookState : Type) : Type

Equations

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

These two functions preserve the get_place_alloc and get_place_alloc_mut order: dynamic layout first; pointer access and hooks next; the cached misalignment check last, with pointer/mutability errors taking precedence.

def Miri.Interpreter.getPlaceAlloc {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (place : MemoryOperandPlace Prov) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (Option (Memory.AllocationAccessRef Prov Extra))

Equations

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

def Miri.Interpreter.getPlaceAllocMut {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (place : MemoryOperandPlace Prov) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (Option (Memory.AllocationAccessRef Prov Extra))

Equations

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

Source read_immediate_from_mplace_raw. In particular, an unsized layout returns before touching memory; a zero-sized access with no allocation becomes Uninit; all layouts that are not fully initialized scalar/scalar-pair ABIs remain in memory.

def Miri.Interpreter.readImmediateFromMplaceRaw {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (place : MemoryOperandPlace Prov) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (Option (ImmediateValue Prov))

Equations

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

Raw operand reads retain the source's memory fallback. The caller supplies the layout cached on the source OpTy; a local-to-place projection that must materialize a local remains an explicit higher-level operation.

def Miri.Interpreter.readImmediateRaw {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (operand : Operand Prov) (layout : MemoryOperandLayout) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (ImmediateOrPlace Prov)

Equations

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

Source read_immediate, with the source span-bug and UB branches made explicit. Unavailable pointer/machine semantics are retained by the wrapped allocation-access error and are never interpreted as a valid value.

def Miri.Interpreter.readImmediate {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (operand : Operand Prov) (layout : MemoryOperandLayout) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (ImmediateValue Prov)

Equations

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

def Miri.Interpreter.readScalar {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (operand : Operand Prov) (layout : MemoryOperandLayout) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) : MemoryOperandResult Prov Extra MachineKind HookState (Memory.Scalar Prov)

Equations

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

Source write_immediate_to_mplace_no_validate. The ABI assertion precedes pointer access; the scalar-pair offset assertion follows mutable place access; padding is cleared before either component write; and each allocation update is committed before the next operation so later failures retain partial state. Machine validity policy is an explicit input, matching M::enforce_validity.

def Miri.Interpreter.writeImmediateToMplaceNoValidate {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (value : Immediate Prov) (place : MemoryOperandPlace Prov) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) (willLaterValidate : MemoryOperandLayout → Bool) : MemoryOperandResult Prov Extra MachineKind HookState Unit

Equations

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

theorem Miri.Interpreter.unsized_raw_read_does_not_call_dynamic_access {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (memory : Memory.MemoryState Prov Extra MachineKind) (hooks : HookState) (place : MemoryOperandPlace Prov) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : Memory.GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : Memory.AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) (dynamicLayout : DynamicLayoutResolver Prov Extra MachineKind HookState) (h : place.layout.backendRepr.isUnsized = true) : (readImmediateFromMplaceRaw memory hooks place runtime ghostMode globalKind globalHooks accessHooks dynamicLayout).memory = memory

theorem Miri.Interpreter.zero_uninit_write {P E K H X : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (memory : Memory.MemoryState P E K) (hooks : H) (pointer : Memory.Pointer (Option P)) (runtime : ABI.RuntimeTargetDataLayout) (pointerSize : ABI.Size) (pointerMetadata : runtime.pointerSizeIn runtime.defaultAddressSpace = Except.ok pointerSize) (ghost : Bool) (kind : Option K) (globals : Memory.GlobalAllocationHooks P E K H) (access : Memory.AllocationAccessHooks P E K H X) (dynamic : DynamicLayoutResolver P E K H) (later : MemoryOperandLayout → Bool) (ty : Option Nat) : writeImmediateToMplaceNoValidate memory hooks Immediate.uninit { mplace := { ptr := pointer, metadata := MemPlaceMeta.none, misaligned := none }, layout := { size := ABI.Size.ZERO, align := ABI.Align.ONE, backendRepr := ABI.BackendRepr.Memory, canonicalType := ty } } runtime ghost kind globals access dynamic later = { memory := memory, hooks := hooks, touched := none, outcome := Except.ok () }

Unit storage has no byte write, for any aligned pointer and arbitrary memory/access hooks. Only the target pointer-size query is a metadata premise.

theorem Miri.Interpreter.getPlaceAllocMut_sized_of_access {P E K H X : Type} [DecidableEq K] (memory : Memory.MemoryState P E K) (hooks : H) (place : MemoryOperandPlace P) (runtime : ABI.RuntimeTargetDataLayout) (pointerSize : ABI.Size) (kind : Option K) (global : Memory.GlobalAllocationHooks P E K H) (access : Memory.AllocationAccessHooks P E K H X) (dynamic : DynamicLayoutResolver P E K H) (reference : Memory.AllocationAccessRef P E) (sized : place.layout.backendRepr.isUnsized = false) (aligned : place.mplace.misaligned = none) (pointer : runtime.pointerSizeIn runtime.defaultAddressSpace = Except.ok pointerSize) (actual : Memory.AllocationAccess.getPtrAllocMut memory hooks { pointerSize := pointerSize } place.mplace.ptr place.layout.size false kind global access = { memory := memory, hooks := hooks, touched := some reference, outcome := Except.ok (some reference) }) : getPlaceAllocMut memory hooks place runtime false kind global access dynamic = { memory := memory, hooks := hooks, touched := some reference, outcome := Except.ok (some reference) }

Internal positive-access composition after raw source resolution.

theorem Miri.Interpreter.writeImmediate_scalar_of_access {P E K H X : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (memory afterMemory : Memory.MemoryState P E K) (hooks : H) (place : MemoryOperandPlace P) (runtime : ABI.RuntimeTargetDataLayout) (kind : Option K) (global : Memory.GlobalAllocationHooks P E K H) (access : Memory.AllocationAccessHooks P E K H X) (dynamic : DynamicLayoutResolver P E K H) (later : MemoryOperandLayout → Bool) (value : Memory.Scalar P) (abi : ABI.Scalar) (id : Memory.AllocId) (allocation after : Memory.Allocation P E) (backend : place.layout.backendRepr = ABI.BackendRepr.Scalar abi) (width : abi.primitive.size runtime = Except.ok value.size) (category : match abi.primitive with | ABI.Primitive.Pointer addressSpace => True | x => value.isPointer = false) (bound : value.size.bytes ≤ place.layout.size.bytes) (actual : getPlaceAllocMut memory hooks place runtime false kind global access dynamic = { memory := memory, hooks := hooks, touched := some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := allocation }, outcome := Except.ok (some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := allocation }) }) (written : Memory.Allocation.writeScalar runtime.base (Memory.allocRange ABI.Size.ZERO value.size) value allocation = EStateM.Result.ok () after) (committed : memory.setLiveAllocation id after = Except.ok afterMemory) : writeImmediateToMplaceNoValidate memory hooks (Immediate.scalar value) place runtime false kind global access dynamic later = { memory := afterMemory, hooks := hooks, touched := some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := after }, outcome := Except.ok () }

The actual scalar immediate writer, composed with its derived mutable access and pure allocation mutation. These are internal operation edges.

theorem Miri.Interpreter.writeImmediate_pair_of_access {P E K H X : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (memory middleMemory afterMemory : Memory.MemoryState P E K) (hooks : H) (place : MemoryOperandPlace P) (runtime : ABI.RuntimeTargetDataLayout) (kind : Option K) (global : Memory.GlobalAllocationHooks P E K H) (access : Memory.AllocationAccessHooks P E K H X) (dynamic : DynamicLayoutResolver P E K H) (first second : Memory.Scalar P) (abiA abiB : ABI.Scalar) (offset : ABI.Size) (id : Memory.AllocId) (allocation middle after : Memory.Allocation P E) (backend : place.layout.backendRepr = ABI.BackendRepr.ScalarPair) (widthA : abiA.primitive.size runtime = Except.ok first.size) (widthB : abiB.primitive.size runtime = Except.ok second.size) (categoryA : match abiA.primitive with | ABI.Primitive.Pointer addressSpace => True | x => first.isPointer = false) (categoryB : match abiB.primitive with | ABI.Primitive.Pointer addressSpace => True | x => second.isPointer = false) (offsetPositive : offset.bytes ≠ 0) (firstEnd : first.size.bytes ≤ offset.bytes) (bound : offset.bytes.toNat + second.size.bytes.toNat ≤ place.layout.size.bytes.toNat) (actual : getPlaceAllocMut memory hooks place runtime false kind global access dynamic = { memory := memory, hooks := hooks, touched := some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := allocation }, outcome := Except.ok (some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := allocation }) }) (writtenA : Memory.Allocation.writeScalar runtime.base (Memory.allocRange ABI.Size.ZERO first.size) first allocation = EStateM.Result.ok () middle) (cacheA : memory.setLiveAllocation id middle = Except.ok middleMemory) (writtenB : Memory.Allocation.writeScalar runtime.base (Memory.allocRange offset second.size) second middle = EStateM.Result.ok () after) (cacheB : middleMemory.setLiveAllocation id after = Except.ok afterMemory) : (writeImmediateToMplaceNoValidate memory hooks (Immediate.scalarPair first second) place runtime false kind global access dynamic fun (x : MemoryOperandLayout) => true) = { memory := afterMemory, hooks := hooks, touched := some { allocId := id, range := Memory.allocRange ABI.Size.ZERO place.layout.size, allocation := after }, outcome := Except.ok () }

ScalarPair's real source branch under the caller's current shallow validation policy; the two writes and intermediate cache update are retained.