Source-shaped operand evaluation. Compiler normalization, projection, and machine policy are mandatory contracts, never default successful operations.

@[reducible, inline]

abbrev Miri.Interpreter.TypedOperand (Prov : Type) : Type

Equations

• Miri.Interpreter.TypedOperand = Miri.Interpreter.OpTy

def Miri.Interpreter.localMemoryLayout (layout : LocalLayout) : MemoryOperandLayout

One-way projection for byte/ABI memory operations; canonical operands retain full compiler type identity and layout.

Equations

• Miri.Interpreter.localMemoryLayout layout = { size := layout.layout.size, align := layout.layout.align.abi, backendRepr := layout.layout.backendRepr, canonicalType := some layout.ty }

inductive Miri.Interpreter.LocalAccessError : Type

• stack (error : StackError) : LocalAccessError
• memory (error : MemoryOperandError) : LocalAccessError
• projection (error : ProjectionError) : LocalAccessError
• unsizedImmediate : LocalAccessError
• resolver (message : String) : LocalAccessError

def Miri.Interpreter.instDecidableEqLocalAccessError.decEq (x✝ x✝¹ : LocalAccessError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.stack a) (Miri.Interpreter.LocalAccessError.stack b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.stack error) (Miri.Interpreter.LocalAccessError.memory error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.stack error) (Miri.Interpreter.LocalAccessError.projection error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.stack error) Miri.Interpreter.LocalAccessError.unsizedImmediate = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.stack error) (Miri.Interpreter.LocalAccessError.resolver message) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.memory error) (Miri.Interpreter.LocalAccessError.stack error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.memory a) (Miri.Interpreter.LocalAccessError.memory b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.memory error) (Miri.Interpreter.LocalAccessError.projection error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.memory error) Miri.Interpreter.LocalAccessError.unsizedImmediate = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.memory error) (Miri.Interpreter.LocalAccessError.resolver message) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.projection error) (Miri.Interpreter.LocalAccessError.stack error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.projection error) (Miri.Interpreter.LocalAccessError.memory error_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.projection error) Miri.Interpreter.LocalAccessError.unsizedImmediate = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.projection error) (Miri.Interpreter.LocalAccessError.resolver message) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq Miri.Interpreter.LocalAccessError.unsizedImmediate (Miri.Interpreter.LocalAccessError.stack error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq Miri.Interpreter.LocalAccessError.unsizedImmediate (Miri.Interpreter.LocalAccessError.memory error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq Miri.Interpreter.LocalAccessError.unsizedImmediate (Miri.Interpreter.LocalAccessError.projection error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq Miri.Interpreter.LocalAccessError.unsizedImmediate Miri.Interpreter.LocalAccessError.unsizedImmediate = isTrue ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq Miri.Interpreter.LocalAccessError.unsizedImmediate (Miri.Interpreter.LocalAccessError.resolver message) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.resolver message) (Miri.Interpreter.LocalAccessError.stack error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.resolver message) (Miri.Interpreter.LocalAccessError.memory error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.resolver message) (Miri.Interpreter.LocalAccessError.projection error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalAccessError.decEq (Miri.Interpreter.LocalAccessError.resolver message) Miri.Interpreter.LocalAccessError.unsizedImmediate = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqLocalAccessError : DecidableEq LocalAccessError

Equations

• Miri.Interpreter.instDecidableEqLocalAccessError = Miri.Interpreter.instDecidableEqLocalAccessError.decEq

def Miri.Interpreter.instReprLocalAccessError.repr : LocalAccessError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprLocalAccessError : Repr LocalAccessError

Equations

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

structure Miri.Interpreter.LocalAccessResult (Prov Extra State α : Type) : Type

• frame : Frame Prov LocalLayout Extra
• state : State
• outcome : Except LocalAccessError α

structure Miri.Interpreter.LocalAccessHooks (Prov Extra State : Type) : Type

layout implements from_known_layout, normalization and layout lookup. project implements rustc Projectable including provenance and metadata. checkPlaceType performs the debug-mode normalized MIR type sanity check when that mode is enabled, and must explicitly implement the disabled-mode policy. Constant evaluation includes instantiation, normalization and failure handling.

• layout : Frame Prov LocalLayout Extra → State → MIR.LocalId → Option LocalLayout → LocalAccessResult Prov Extra State LocalLayout
• validationInProgress : State → Bool
• afterLocalRead : Frame Prov LocalLayout Extra → State → MIR.LocalId → LocalAccessResult Prov Extra State Unit
• project : Frame Prov LocalLayout Extra → State → TypedOperand Prov → MIR.ProjectionElem → LocalAccessResult Prov Extra State (TypedOperand Prov)
• checkPlaceType : Frame Prov LocalLayout Extra → State → MIR.Place → TypedOperand Prov → LocalAccessResult Prov Extra State Unit
• runtimeChecks : Frame Prov LocalLayout Extra → State → MIR.RuntimeChecks → LocalAccessResult Prov Extra State (TypedOperand Prov)
• constant : Frame Prov LocalLayout Extra → State → MIR.ConstOperand → Option LocalLayout → LocalAccessResult Prov Extra State (TypedOperand Prov)

def Miri.Interpreter.localProjectionHook {Prov Extra State : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (frame : Frame Prov LocalLayout Extra) (state : State) (op : TypedOperand Prov) (elem : MIR.ProjectionElem) : LocalAccessResult Prov Extra State (TypedOperand Prov)

Use the executable canonical projector rather than a second projection IR.

Equations

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

def Miri.Interpreter.localToOp {Prov Extra State : Type} (hooks : LocalAccessHooks Prov Extra State) (frame : Frame Prov LocalLayout Extra) (state : State) (localId : MIR.LocalId) (known : Option LocalLayout) : LocalAccessResult Prov Extra State (TypedOperand Prov)

Pinned operand.rs local_to_op: layout cache precedes dead-localId checking; only immediate reads outside validation invoke the machine read hook.

Equations

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

def Miri.Interpreter.evalPlaceToOp {Prov Extra State : Type} (hooks : LocalAccessHooks Prov Extra State) (frame : Frame Prov LocalLayout Extra) (state : State) (place : MIR.Place) (known : Option LocalLayout) : LocalAccessResult Prov Extra State (TypedOperand Prov)

Equations

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

def Miri.Interpreter.evalOperand {Prov Extra State : Type} (hooks : LocalAccessHooks Prov Extra State) (frame : Frame Prov LocalLayout Extra) (state : State) (operand : MIR.Operand) (known : Option LocalLayout) : LocalAccessResult Prov Extra State (TypedOperand Prov)

Copy and Move deliberately share the source branch. Pinned rustc's FIXME leaves move invalidation unimplemented; this port does not invent it.

Equations

• Miri.Interpreter.evalOperand hooks frame state (Miri.MIR.Operand.Copy place) known = Miri.Interpreter.evalPlaceToOp hooks frame state place known
• Miri.Interpreter.evalOperand hooks frame state (Miri.MIR.Operand.Move place) known = Miri.Interpreter.evalPlaceToOp hooks frame state place known
• Miri.Interpreter.evalOperand hooks frame state (Miri.MIR.Operand.RuntimeChecks check) known = hooks.runtimeChecks frame state check
• Miri.Interpreter.evalOperand hooks frame state (Miri.MIR.Operand.Constant constant) known = hooks.constant frame state constant known

structure Miri.Interpreter.LocalReadContext (Prov MemExtra Kind HookState ProvExtra : Type) : Type

Connected immediate-read context. Allocation/global/access hooks are the existing memory port's required inputs.

• runtime : ABI.RuntimeTargetDataLayout
• ghostMode : Bool
• globalKind : Option Kind
• globalHooks : Memory.GlobalAllocationHooks Prov MemExtra Kind HookState
• accessHooks : Memory.AllocationAccessHooks Prov MemExtra Kind HookState ProvExtra
• dynamicLayout : DynamicLayoutResolver Prov MemExtra Kind HookState

def Miri.Interpreter.readTypedImmediate {Kind Prov MemExtra HookState ProvExtra : Type} [DecidableEq Kind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (context : LocalReadContext Prov MemExtra Kind HookState ProvExtra) (memory : Memory.MemoryState Prov MemExtra Kind) (state : HookState) (op : TypedOperand Prov) : MemoryOperandResult Prov MemExtra Kind HookState (ImmediateValue Prov)

The actual MemoryOperand.readImmediate path, retaining memory, hook state, and touched allocation even if decoding or access fails.

Equations

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

structure Miri.Interpreter.LocalReadState (Prov MemExtra Kind HookState : Type) : Type

• memory : Memory.MemoryState Prov MemExtra Kind
• hooks : HookState
• touched : Option (Memory.AllocationAccessRef Prov MemExtra)

def Miri.Interpreter.evalOperandImmediate {Kind Prov MemExtra HookState ProvExtra Extra : Type} [DecidableEq Kind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (context : LocalReadContext Prov MemExtra Kind HookState ProvExtra) (hooks : LocalAccessHooks Prov Extra (LocalReadState Prov MemExtra Kind HookState)) (frame : Frame Prov LocalLayout Extra) (state : LocalReadState Prov MemExtra Kind HookState) (operand : MIR.Operand) (known : Option LocalLayout) : LocalAccessResult Prov Extra (LocalReadState Prov MemExtra Kind HookState) (ImmediateValue Prov)

Evaluate MIR syntax and read its immediate using the existing allocation semantics. Local hooks operate on this same memory and machine state.

Equations

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

def Miri.Interpreter.readLocalImmediate {Kind Prov MemExtra HookState ProvExtra Extra : Type} [DecidableEq Kind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (context : LocalReadContext Prov MemExtra Kind HookState ProvExtra) (hooks : LocalAccessHooks Prov Extra (LocalReadState Prov MemExtra Kind HookState)) (frame : Frame Prov LocalLayout Extra) (state : LocalReadState Prov MemExtra Kind HookState) (localId : MIR.LocalId) : LocalAccessResult Prov Extra (LocalReadState Prov MemExtra Kind HookState) (ImmediateValue Prov)

Equations

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

structure Miri.Interpreter.LocalWriteHooks (Prov Extra State : Type) : Type

Required post-write machine and ABI-debug policy, with no silent policy.

• validationInProgress : State → Bool
• afterLocalWrite : Frame Prov LocalLayout Extra → State → MIR.LocalId → LocalAccessResult Prov Extra State Unit
• checkImmediateAbi : Frame Prov LocalLayout Extra → State → Immediate Prov → LocalLayout → LocalAccessResult Prov Extra State Unit

def Miri.Interpreter.writeImmediateLocalBranch {Prov Extra State : Type} (hooks : LocalWriteHooks Prov Extra State) (frame : Frame Prov LocalLayout Extra) (state : State) (localId : MIR.LocalId) (layout : LocalLayout) (value : Immediate Prov) : LocalAccessResult Prov Extra State Unit

Immediate-only whole-local branch, reusable without inventing an allocation context. Callers must have selected an immediate-backed destination.

Equations

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

def Miri.Interpreter.writeLocalImmediateNoValidate {Kind Prov MemExtra HookState ProvExtra Extra : Type} [DecidableEq Kind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (context : LocalReadContext Prov MemExtra Kind HookState ProvExtra) (willLaterValidate : MemoryOperandLayout → Bool) (hooks : LocalWriteHooks Prov Extra (LocalReadState Prov MemExtra Kind HookState)) (frame : Frame Prov LocalLayout Extra) (state : LocalReadState Prov MemExtra Kind HookState) (localId : MIR.LocalId) (layout : LocalLayout) (value : Immediate Prov) : LocalAccessResult Prov Extra (LocalReadState Prov MemExtra Kind HookState) Unit

Whole-local immediate write branch from place.rs. The replacement precedes both the machine hook and debug ABI check, so failures retain the new value. Indirect locals use the existing memory writer, preserving metadata.

Equations

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

def Miri.Interpreter.localCopyReadRaw {Kind Prov MemExtra HookState ProvExtra Extra : Type} [DecidableEq Kind] [DecidableEq Prov] [Memory.PointerProvenance Prov] (context : LocalReadContext Prov MemExtra Kind HookState ProvExtra) (frame : Frame Prov LocalLayout Extra) (state : LocalReadState Prov MemExtra Kind HookState) (source : TypedOperand Prov) : LocalAccessResult Prov Extra (LocalReadState Prov MemExtra Kind HookState) (ImmediateOrPlace Prov)

Concrete raw-reader adapter for the copy pipeline's fast-path probe.

Equations

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

structure Miri.Interpreter.LocalCopyHooks (Prov Extra State Dest : Type) : Type

Required source-copy dependencies. hasPadding includes the wide-pointer special case and scalar-size queries. copyMemory must perform nonoverlapping mem_copy before source then destination alignment checks, retaining effects. validate performs the source/destination typed passes, provenance/padding reset and recursive-validity policy from copy_op_inner.

• destinationLayout : Dest → LocalLayout
• compatible : LocalLayout → LocalLayout → Except LocalAccessError Bool
• hasPadding : LocalLayout → Except LocalAccessError Bool
• readRaw : Frame Prov LocalLayout Extra → State → TypedOperand Prov → LocalAccessResult Prov Extra State (ImmediateOrPlace Prov)
• writeImmediate : Frame Prov LocalLayout Extra → State → Dest → Immediate Prov → LocalAccessResult Prov Extra State Unit
• forceDestination : Frame Prov LocalLayout Extra → State → Dest → LocalAccessResult Prov Extra State (MemoryOperandPlace Prov)
• writeTransmuted : Frame Prov LocalLayout Extra → State → MemoryOperandPlace Prov → LocalLayout → Immediate Prov → LocalAccessResult Prov Extra State Unit
• copyMemory : Frame Prov LocalLayout Extra → State → MemoryOperandPlace Prov → MemoryOperandPlace Prov → LocalAccessResult Prov Extra State Unit
• validate : Frame Prov LocalLayout Extra → State → LocalLayout → Dest → LocalAccessResult Prov Extra State Unit

def Miri.Interpreter.copyOperandNoValidate {Prov Extra State Dest : Type} (hooks : LocalCopyHooks Prov Extra State Dest) (frame : Frame Prov LocalLayout Extra) (state : State) (source : TypedOperand Prov) (dest : Dest) (allowTransmute : Bool) : LocalAccessResult Prov Extra State Unit

Pinned place.rs copy_op_no_validate decision pipeline. Every slow-path operation has an explicit contract; no missing memory operation succeeds.

Equations

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

def Miri.Interpreter.copyOperand {Prov Extra State Dest : Type} (hooks : LocalCopyHooks Prov Extra State Dest) (frame : Frame Prov LocalLayout Extra) (state : State) (source : TypedOperand Prov) (dest : Dest) (allowTransmute : Bool) : LocalAccessResult Prov Extra State Unit

Equations

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

theorem Miri.Interpreter.copy_move_same {Prov Extra State : Type} (hooks : LocalAccessHooks Prov Extra State) (frame : Frame Prov LocalLayout Extra) (state : State) (place : MIR.Place) (known : Option LocalLayout) : evalOperand hooks frame state (MIR.Operand.Copy place) known = evalOperand hooks frame state (MIR.Operand.Move place) known