Canonical typed runtime places shared by frame storage, call dispatch and place execution. Byte-level MemoryOperandLayout is only a one-way memory API projection; saved places always retain their original TyAndLayout.

@[reducible, inline]

abbrev Miri.Interpreter.LocalLayout : Type

Equations

• Miri.Interpreter.LocalLayout = Miri.ABI.TyAndLayout Miri.MIR.TyId

structure Miri.Interpreter.MPlaceTy (P : Type) : Type

• mplace : MemPlace P
• layout : LocalLayout

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMPlaceTy {P✝ : Type} [DecidableEq P✝] : DecidableEq (MPlaceTy P✝)

Equations

• Miri.Interpreter.instDecidableEqMPlaceTy = Miri.Interpreter.instDecidableEqMPlaceTy.decEq

def Miri.Interpreter.instDecidableEqMPlaceTy.decEq {P✝ : Type} [DecidableEq P✝] (x✝ x✝¹ : MPlaceTy P✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqMPlaceTy.decEq { mplace := a, layout := a_1 } { mplace := b, layout := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprMPlaceTy {P✝ : Type} [Repr P✝] : Repr (MPlaceTy P✝)

Equations

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

def Miri.Interpreter.instReprMPlaceTy.repr {P✝ : Type} [Repr P✝] : MPlaceTy P✝ → Nat → Std.Format

Equations

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

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

• local {P : Type} (frameIndex localId : Nat) (offset : Option ABI.Size) (localsIdentity : LocalsIdentity) : RuntimePlaceRef P
• memory {P : Type} (place : MemPlace P) : RuntimePlaceRef P

def Miri.Interpreter.instDecidableEqRuntimePlaceRef.decEq {P✝ : Type} [DecidableEq P✝] (x✝ x✝¹ : RuntimePlaceRef P✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqRuntimePlaceRef.decEq (Miri.Interpreter.RuntimePlaceRef.memory a) (Miri.Interpreter.RuntimePlaceRef.memory b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqRuntimePlaceRef {P✝ : Type} [DecidableEq P✝] : DecidableEq (RuntimePlaceRef P✝)

Equations

• Miri.Interpreter.instDecidableEqRuntimePlaceRef = Miri.Interpreter.instDecidableEqRuntimePlaceRef.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprRuntimePlaceRef {P✝ : Type} [Repr P✝] : Repr (RuntimePlaceRef P✝)

Equations

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

def Miri.Interpreter.instReprRuntimePlaceRef.repr {P✝ : Type} [Repr P✝] : RuntimePlaceRef P✝ → Nat → Std.Format

Equations

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

structure Miri.Interpreter.RuntimePlace (P : Type) : Type

• ref : RuntimePlaceRef P
• layout : LocalLayout

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqRuntimePlace {P✝ : Type} [DecidableEq P✝] : DecidableEq (RuntimePlace P✝)

Equations

• Miri.Interpreter.instDecidableEqRuntimePlace = Miri.Interpreter.instDecidableEqRuntimePlace.decEq

def Miri.Interpreter.instDecidableEqRuntimePlace.decEq {P✝ : Type} [DecidableEq P✝] (x✝ x✝¹ : RuntimePlace P✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqRuntimePlace.decEq { ref := a, layout := a_1 } { ref := b, layout := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprRuntimePlace {P✝ : Type} [Repr P✝] : Repr (RuntimePlace P✝)

Equations

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

def Miri.Interpreter.instReprRuntimePlace.repr {P✝ : Type} [Repr P✝] : RuntimePlace P✝ → Nat → Std.Format

Equations

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

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

Saved evaluated call/return destination. Both variants retain canonical compiler type identity, including projected local destinations.

• memory {P : Type} (place : MPlaceTy P) : RuntimeStackPlace P
• frameLocal {P : Type} (frameIndex localId : Nat) (offset : Option ABI.Size) (layout : LocalLayout) (localsIdentity : LocalsIdentity) : RuntimeStackPlace P

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqRuntimeStackPlace {P✝ : Type} [DecidableEq P✝] : DecidableEq (RuntimeStackPlace P✝)

Equations

• Miri.Interpreter.instDecidableEqRuntimeStackPlace = Miri.Interpreter.instDecidableEqRuntimeStackPlace.decEq

def Miri.Interpreter.instDecidableEqRuntimeStackPlace.decEq {P✝ : Type} [DecidableEq P✝] (x✝ x✝¹ : RuntimeStackPlace P✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprRuntimeStackPlace {P✝ : Type} [Repr P✝] : Repr (RuntimeStackPlace P✝)

Equations

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

def Miri.Interpreter.instReprRuntimeStackPlace.repr {P✝ : Type} [Repr P✝] : RuntimeStackPlace P✝ → Nat → Std.Format

Equations

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

def Miri.Interpreter.RuntimeStackPlace.toRuntimePlace {P : Type} : RuntimeStackPlace P → RuntimePlace P

Equations

• (Miri.Interpreter.RuntimeStackPlace.memory a).toRuntimePlace = { ref := Miri.Interpreter.RuntimePlaceRef.memory a.mplace, layout := a.layout }
• (Miri.Interpreter.RuntimeStackPlace.frameLocal a a_1 a_2 a_3 a_4).toRuntimePlace = { ref := Miri.Interpreter.RuntimePlaceRef.local a a_1 a_2 a_4, layout := a_3 }

def Miri.Interpreter.RuntimeStackPlace.layout {P : Type} : RuntimeStackPlace P → LocalLayout

Equations

• (Miri.Interpreter.RuntimeStackPlace.memory a).layout = a.layout
• (Miri.Interpreter.RuntimeStackPlace.frameLocal a a_1 a_2 a_3 a_4).layout = a_3

def Miri.Interpreter.RuntimePlace.stackView {P : Type} (place : RuntimePlace P) : RuntimeStackPlace P

Equations

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

@[simp]

theorem Miri.Interpreter.RuntimePlace.stackView_toRuntimePlace {P : Type} (place : RuntimePlace P) : place.stackView.toRuntimePlace = place

@[simp]

theorem Miri.Interpreter.RuntimeStackPlace.toRuntimePlace_stackView {P : Type} (place : RuntimeStackPlace P) : place.toRuntimePlace.stackView = place