Stored operands and the low-level LocalState operations from pinned operand.rs, place.rs, and stack.rs. Memory access and machine hooks are required at higher-level accesses; the ghost accessor below never substitutes for a Rust read.

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

• ptr : Memory.Pointer (Option Prov)
• metadata : MemPlaceMeta Prov
• misaligned : Option Memory.Misalignment

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemPlace {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (MemPlace Prov✝)

Equations

• Miri.Interpreter.instDecidableEqMemPlace = Miri.Interpreter.instDecidableEqMemPlace.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprMemPlace {Prov✝ : Type} [Repr Prov✝] : Repr (MemPlace Prov✝)

Equations

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

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

Equations

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

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

• immediate {Prov : Type} (value : Immediate Prov) : Operand Prov
• indirect {Prov : Type} (place : MemPlace Prov) : Operand Prov

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

Equations

• Miri.Interpreter.instDecidableEqOperand.decEq (Miri.Interpreter.Operand.immediate a) (Miri.Interpreter.Operand.immediate b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqOperand.decEq (Miri.Interpreter.Operand.immediate value) (Miri.Interpreter.Operand.indirect place) = isFalse ⋯
• Miri.Interpreter.instDecidableEqOperand.decEq (Miri.Interpreter.Operand.indirect place) (Miri.Interpreter.Operand.immediate value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqOperand.decEq (Miri.Interpreter.Operand.indirect a) (Miri.Interpreter.Operand.indirect b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqOperand {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (Operand Prov✝)

Equations

• Miri.Interpreter.instDecidableEqOperand = Miri.Interpreter.instDecidableEqOperand.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprOperand {Prov✝ : Type} [Repr Prov✝] : Repr (Operand Prov✝)

Equations

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

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

Equations

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

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

• dead {Prov : Type} : LocalValue Prov
• live {Prov : Type} (value : Operand Prov) : LocalValue Prov

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

Equations

• Miri.Interpreter.instDecidableEqLocalValue.decEq Miri.Interpreter.LocalValue.dead Miri.Interpreter.LocalValue.dead = isTrue ⋯
• Miri.Interpreter.instDecidableEqLocalValue.decEq Miri.Interpreter.LocalValue.dead (Miri.Interpreter.LocalValue.live value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalValue.decEq (Miri.Interpreter.LocalValue.live value) Miri.Interpreter.LocalValue.dead = isFalse ⋯
• Miri.Interpreter.instDecidableEqLocalValue.decEq (Miri.Interpreter.LocalValue.live a) (Miri.Interpreter.LocalValue.live b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqLocalValue {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (LocalValue Prov✝)

Equations

• Miri.Interpreter.instDecidableEqLocalValue = Miri.Interpreter.instDecidableEqLocalValue.decEq

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprLocalValue {Prov✝ : Type} [Repr Prov✝] : Repr (LocalValue Prov✝)

Equations

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

structure Miri.Interpreter.LocalState (Prov Layout : Type) : Type

Layout will be the canonical imported TyAndLayout representation at the integrated interpreter boundary. Its cached value is retained unchanged by the selected source operations.

• value : LocalValue Prov
• layout : Option Layout

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

Equations

• Miri.Interpreter.instDecidableEqLocalState.decEq { value := a, layout := a_1 } { value := 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.instDecidableEqLocalState {Prov✝ Layout✝ : Type} [DecidableEq Prov✝] [DecidableEq Layout✝] : DecidableEq (LocalState Prov✝ Layout✝)

Equations

• Miri.Interpreter.instDecidableEqLocalState = Miri.Interpreter.instDecidableEqLocalState.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprLocalState {Prov✝ Layout✝ : Type} [Repr Prov✝] [Repr Layout✝] : Repr (LocalState Prov✝ Layout✝)

Equations

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

def Miri.Interpreter.instReprLocalState.repr {Prov✝ Layout✝ : Type} [Repr Prov✝] [Repr Layout✝] : LocalState Prov✝ Layout✝ → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.LocalStateError : Type

• deadLocal : LocalStateError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqLocalStateError : DecidableEq LocalStateError

Equations

• Miri.Interpreter.instDecidableEqLocalStateError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprLocalStateError : Repr LocalStateError

Equations

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

def Miri.Interpreter.instReprLocalStateError.repr : LocalStateError → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.OffsetMode : Type

• inbounds : OffsetMode
• wrapping : OffsetMode

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqOffsetMode : DecidableEq OffsetMode

Equations

• Miri.Interpreter.instDecidableEqOffsetMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.instReprOffsetMode.repr : OffsetMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprOffsetMode : Repr OffsetMode

Equations

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

inductive Miri.Interpreter.MemPlaceOffsetError : Type

• addedMetadataToThinPlace : MemPlaceOffsetError
• offsetDoesNotFitI64 (offset : ABI.Size) : MemPlaceOffsetError
• inbounds (reason : PointerOffsetError) : MemPlaceOffsetError
• pointer (reason : Memory.PointerError) : MemPlaceOffsetError

def Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (x✝ x✝¹ : MemPlaceOffsetError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace = isTrue ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace (Miri.Interpreter.MemPlaceOffsetError.inbounds reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace (Miri.Interpreter.MemPlaceOffsetError.pointer reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.offsetDoesNotFitI64 offset) (Miri.Interpreter.MemPlaceOffsetError.pointer reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.inbounds reason) Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.inbounds reason) (Miri.Interpreter.MemPlaceOffsetError.offsetDoesNotFitI64 offset) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.inbounds reason) (Miri.Interpreter.MemPlaceOffsetError.pointer reason_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.pointer reason) Miri.Interpreter.MemPlaceOffsetError.addedMetadataToThinPlace = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.pointer reason) (Miri.Interpreter.MemPlaceOffsetError.offsetDoesNotFitI64 offset) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq (Miri.Interpreter.MemPlaceOffsetError.pointer reason) (Miri.Interpreter.MemPlaceOffsetError.inbounds reason_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemPlaceOffsetError : DecidableEq MemPlaceOffsetError

Equations

• Miri.Interpreter.instDecidableEqMemPlaceOffsetError = Miri.Interpreter.instDecidableEqMemPlaceOffsetError.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprMemPlaceOffsetError : Repr MemPlaceOffsetError

Equations

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

def Miri.Interpreter.instReprMemPlaceOffsetError.repr : MemPlaceOffsetError → Nat → Std.Format

Equations

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

def Miri.Interpreter.MemPlace.mapProvenance {Prov : Type} (self : MemPlace Prov) (f : Prov → Prov) : MemPlace Prov

Equations

• self.mapProvenance f = { ptr := self.ptr.mapProvenance (Option.map f), metadata := self.metadata, misaligned := self.misaligned }

def Miri.Interpreter.MemPlace.toRef {Prov : Type} (self : MemPlace Prov) (layout : ABI.TargetDataLayout) : Except ImmediateError (Immediate Prov)

Equations

• self.toRef layout = Miri.Interpreter.Immediate.newPointerWithMeta self.ptr self.metadata layout

def Miri.Interpreter.MemPlace.offsetWithMeta {Prov ProvExtra : Type} (self : MemPlace Prov) (offset : ABI.Size) (mode : OffsetMode) (metadata : MemPlaceMeta Prov) (target : Memory.PointerArithmetic) (resolve : Memory.PointerResolver Prov ProvExtra) (lookup : Memory.LiveAllocationLookup) : Except MemPlaceOffsetError (MemPlace Prov)

Source MemPlace::offset_with_meta_: metadata cannot be added to a thin place; inbounds mode checks the signed conversion and allocation bounds, while wrapping mode uses the target-width pointer operation directly.

Equations

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

theorem Miri.Interpreter.MemPlace.mapProvenance_metadata {Prov : Type} (self : MemPlace Prov) (f : Prov → Prov) : (self.mapProvenance f).metadata = self.metadata

def Miri.Interpreter.LocalState.makeLiveUninit {Prov Layout : Type} (self : LocalState Prov Layout) : LocalState Prov Layout

Equations

• self.makeLiveUninit = { value := Miri.Interpreter.LocalValue.live (Miri.Interpreter.Operand.immediate Miri.Interpreter.Immediate.uninit), layout := self.layout }

def Miri.Interpreter.LocalState.asMplaceOrImmGhost {Prov Layout : Type} (self : LocalState Prov Layout) : Option (Memory.Pointer (Option Prov) × MemPlaceMeta Prov ⊕ Immediate Prov)

Source ghost read for provenance visiting. It does not count as a read in the abstract machine and performs no borrow/race hooks.

Equations

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

def Miri.Interpreter.LocalState.access {Prov Layout : Type} (self : LocalState Prov Layout) : Except LocalStateError (Operand Prov)

Equations

• self.access = match self.value with | Miri.Interpreter.LocalValue.dead => Except.error Miri.Interpreter.LocalStateError.deadLocal | Miri.Interpreter.LocalValue.live value => Except.ok value

def Miri.Interpreter.LocalState.modify {Prov Layout : Type} (self : LocalState Prov Layout) (f : Operand Prov → Operand Prov) : Except LocalStateError (LocalState Prov Layout)

Functional form of source access_mut: only a live operand is exposed for mutation. It is still the caller's job to perform the machine access hook.

Equations

• self.modify f = do let value ← self.access pure { value := Miri.Interpreter.LocalValue.live (f value), layout := self.layout }

theorem Miri.Interpreter.LocalState.dead_access {Layout Prov : Type} (layout : Option Layout) : { value := LocalValue.dead, layout := layout }.access = Except.error LocalStateError.deadLocal

theorem Miri.Interpreter.LocalState.access_success {Prov Layout : Type} (self : LocalState Prov Layout) (operand : Operand Prov) (success : self.access = Except.ok operand) : self.value = LocalValue.live operand

theorem Miri.Interpreter.LocalState.makeLiveUninit_preserves_layout {Prov Layout : Type} (self : LocalState Prov Layout) : self.makeLiveUninit.layout = self.layout

theorem Miri.Interpreter.LocalState.makeLiveUninit_access {Prov Layout : Type} (self : LocalState Prov Layout) : self.makeLiveUninit.access = Except.ok (Operand.immediate Immediate.uninit)

theorem Miri.Interpreter.LocalState.dead_modify {Layout Prov : Type} (layout : Option Layout) (f : Operand Prov → Operand Prov) : { value := LocalValue.dead, layout := layout }.modify f = Except.error LocalStateError.deadLocal