Whole-state operand.rs local/operand evaluation. Immediate locals remain immediate; dynamic indirect projections use the stateful place projector.

structure Miri.Interpreter.OperandMachine.Hooks (K User C : Type) : Type

• compiler : PlaceMachine.CompilerHooks K User C
• projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra
• layoutCompatible : LocalLayout → LocalLayout → Except StepError Bool
• checkPlaceType : C → MIR.Place → OpTy Memory.Provenance → MachineHooks.M K User Unit
• dereference : C → OpTy Memory.Provenance → MachineHooks.M K User (MPlaceTy Memory.Provenance)
• runtimeChecks : C → MIR.RuntimeChecks → MachineHooks.M K User Bool
• boolLayout : C → MachineHooks.M K User LocalLayout
• constant : C → MIR.ConstOperand → Option LocalLayout → MachineHooks.M K User (OpTy Memory.Provenance)
• constantAt : C → OperandPath → MIR.ConstOperand → Option LocalLayout → MachineHooks.M K User (OpTy Memory.Provenance)

def Miri.Interpreter.OperandMachine.localToOp {K User C : Type} (h : Hooks K User C) (c : C) (id : MIR.LocalId) (known : Option LocalLayout) : MachineHooks.M K User (OpTy Memory.Provenance)

Equations

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

def Miri.Interpreter.OperandMachine.field {K User C : Type} (h : Hooks K User C) (c : C) (base : OpTy Memory.Provenance) (index : Nat) : MachineHooks.M K User (OpTy Memory.Provenance)

Equations

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

def Miri.Interpreter.OperandMachine.project {K User C : Type} (h : Hooks K User C) (c : C) (base : OpTy Memory.Provenance) (elem : MIR.ProjectionElem) : MachineHooks.M K User (OpTy Memory.Provenance)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OperandMachine.project h c base (Miri.MIR.ProjectionElem.Field index ty) = Miri.Interpreter.OperandMachine.field h c base index

def Miri.Interpreter.OperandMachine.evalPlaceToOp {K User C : Type} (h : Hooks K User C) (c : C) (place : MIR.Place) (known : Option LocalLayout) : MachineHooks.M K User (OpTy Memory.Provenance)

Equations

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

def Miri.Interpreter.OperandMachine.evalOperand {K User C : Type} (h : Hooks K User C) (c : C) (operand : MIR.Operand) (known : Option LocalLayout) : MachineHooks.M K User (OpTy Memory.Provenance)

Copy and Move share source behavior; no invented move invalidation.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OperandMachine.evalOperand h c (Miri.MIR.Operand.Copy place) known = Miri.Interpreter.OperandMachine.evalPlaceToOp h c place known
• Miri.Interpreter.OperandMachine.evalOperand h c (Miri.MIR.Operand.Move place) known = Miri.Interpreter.OperandMachine.evalPlaceToOp h c place known
• Miri.Interpreter.OperandMachine.evalOperand h c (Miri.MIR.Operand.Constant value) known = h.constant c value known

def Miri.Interpreter.OperandMachine.evalOperandAt {K User C : Type} (h : Hooks K User C) (c : C) (path : OperandPath) (operand : MIR.Operand) (known : Option LocalLayout) : MachineHooks.M K User (OpTy Memory.Provenance)

The path is carried by the structural caller, not recovered from the operand.

Equations

• Miri.Interpreter.OperandMachine.evalOperandAt h c path (Miri.MIR.Operand.Constant value) known = h.constantAt c (Array.push path (Miri.Interpreter.OperandPathElement.field "constant")) value known
• Miri.Interpreter.OperandMachine.evalOperandAt h c path operand known = Miri.Interpreter.OperandMachine.evalOperand h c operand known