The self-contained value representation and pointer metadata from the pinned interpreter's operand.rs and place.rs. Layout/ABI validation is a separate caller obligation; an immediate alone is not a typed Rust value.

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

• metadata {Prov : Type} (value : Memory.Scalar Prov) : MemPlaceMeta Prov
• none {Prov : Type} : MemPlaceMeta Prov

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

Equations

• Miri.Interpreter.instDecidableEqMemPlaceMeta.decEq (Miri.Interpreter.MemPlaceMeta.metadata a) (Miri.Interpreter.MemPlaceMeta.metadata b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceMeta.decEq (Miri.Interpreter.MemPlaceMeta.metadata value) Miri.Interpreter.MemPlaceMeta.none = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceMeta.decEq Miri.Interpreter.MemPlaceMeta.none (Miri.Interpreter.MemPlaceMeta.metadata value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqMemPlaceMeta.decEq Miri.Interpreter.MemPlaceMeta.none Miri.Interpreter.MemPlaceMeta.none = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqMemPlaceMeta {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (MemPlaceMeta Prov✝)

Equations

• Miri.Interpreter.instDecidableEqMemPlaceMeta = Miri.Interpreter.instDecidableEqMemPlaceMeta.decEq

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprMemPlaceMeta {Prov✝ : Type} [Repr Prov✝] : Repr (MemPlaceMeta Prov✝)

Equations

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

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

• scalar {Prov : Type} (value : Memory.Scalar Prov) : Immediate Prov
• scalarPair {Prov : Type} (first second : Memory.Scalar Prov) : Immediate Prov
• uninit {Prov : Type} : Immediate Prov

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqImmediate {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (Immediate Prov✝)

Equations

• Miri.Interpreter.instDecidableEqImmediate = Miri.Interpreter.instDecidableEqImmediate.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqImmediate.decEq (Miri.Interpreter.Immediate.scalar a) (Miri.Interpreter.Immediate.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq (Miri.Interpreter.Immediate.scalar value) (Miri.Interpreter.Immediate.scalarPair first second) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq (Miri.Interpreter.Immediate.scalar value) Miri.Interpreter.Immediate.uninit = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq (Miri.Interpreter.Immediate.scalarPair first second) (Miri.Interpreter.Immediate.scalar value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq (Miri.Interpreter.Immediate.scalarPair first second) Miri.Interpreter.Immediate.uninit = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq Miri.Interpreter.Immediate.uninit (Miri.Interpreter.Immediate.scalar value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq Miri.Interpreter.Immediate.uninit (Miri.Interpreter.Immediate.scalarPair first second) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediate.decEq Miri.Interpreter.Immediate.uninit Miri.Interpreter.Immediate.uninit = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprImmediate {Prov✝ : Type} [Repr Prov✝] : Repr (Immediate Prov✝)

Equations

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

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

Equations

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

inductive Miri.Interpreter.ImmediateError : Type

• scalar (reason : Memory.ScalarError) : ImmediateError
• expectedScalar : ImmediateError
• expectedScalarPair : ImmediateError
• unexpectedUninit : ImmediateError
• expectedInteger : ImmediateError
• expectedMetadata : ImmediateError

def Miri.Interpreter.instDecidableEqImmediateError.decEq (x✝ x✝¹ : ImmediateError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar a) (Miri.Interpreter.ImmediateError.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar reason) Miri.Interpreter.ImmediateError.expectedScalar = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar reason) Miri.Interpreter.ImmediateError.expectedScalarPair = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar reason) Miri.Interpreter.ImmediateError.unexpectedUninit = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar reason) Miri.Interpreter.ImmediateError.expectedInteger = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq (Miri.Interpreter.ImmediateError.scalar reason) Miri.Interpreter.ImmediateError.expectedMetadata = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedScalar (Miri.Interpreter.ImmediateError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedScalar Miri.Interpreter.ImmediateError.expectedScalar = isTrue ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedScalarPair (Miri.Interpreter.ImmediateError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedScalarPair Miri.Interpreter.ImmediateError.expectedScalarPair = isTrue ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.unexpectedUninit (Miri.Interpreter.ImmediateError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.unexpectedUninit Miri.Interpreter.ImmediateError.unexpectedUninit = isTrue ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedInteger (Miri.Interpreter.ImmediateError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedInteger Miri.Interpreter.ImmediateError.expectedInteger = isTrue ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedMetadata (Miri.Interpreter.ImmediateError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqImmediateError.decEq Miri.Interpreter.ImmediateError.expectedMetadata Miri.Interpreter.ImmediateError.expectedMetadata = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqImmediateError : DecidableEq ImmediateError

Equations

• Miri.Interpreter.instDecidableEqImmediateError = Miri.Interpreter.instDecidableEqImmediateError.decEq

def Miri.Interpreter.instReprImmediateError.repr : ImmediateError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprImmediateError : Repr ImmediateError

Equations

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

def Miri.Interpreter.MemPlaceMeta.unwrapMeta {Prov : Type} : MemPlaceMeta Prov → Except ImmediateError (Memory.Scalar Prov)

Equations

• (Miri.Interpreter.MemPlaceMeta.metadata a).unwrapMeta = Except.ok a
• Miri.Interpreter.MemPlaceMeta.none.unwrapMeta = Except.error Miri.Interpreter.ImmediateError.expectedMetadata

def Miri.Interpreter.MemPlaceMeta.hasMeta {Prov : Type} : MemPlaceMeta Prov → Bool

Equations

• (Miri.Interpreter.MemPlaceMeta.metadata a).hasMeta = true
• Miri.Interpreter.MemPlaceMeta.none.hasMeta = false

def Miri.Interpreter.Immediate.newPointerWithMeta {Prov : Type} (pointer : Memory.Pointer (Option Prov)) (metadata : MemPlaceMeta Prov) (layout : ABI.TargetDataLayout) : Except ImmediateError (Immediate Prov)

Equations

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

def Miri.Interpreter.Immediate.newSlice {Prov : Type} (pointer : Memory.Pointer (Option Prov)) (length : UInt64) (layout : ABI.TargetDataLayout) : Except ImmediateError (Immediate Prov)

Equations

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

def Miri.Interpreter.Immediate.newDynTrait {Prov : Type} (pointer vtable : Memory.Pointer (Option Prov)) (layout : ABI.TargetDataLayout) : Except ImmediateError (Immediate Prov)

Equations

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

def Miri.Interpreter.Immediate.toScalar {Prov : Type} : Immediate Prov → Except ImmediateError (Memory.Scalar Prov)

Equations

• (Miri.Interpreter.Immediate.scalar a).toScalar = Except.ok a
• (Miri.Interpreter.Immediate.scalarPair a a_1).toScalar = Except.error Miri.Interpreter.ImmediateError.expectedScalar
• Miri.Interpreter.Immediate.uninit.toScalar = Except.error Miri.Interpreter.ImmediateError.unexpectedUninit

def Miri.Interpreter.Immediate.toScalarInt {Prov : Type} [Memory.PointerProvenance Prov] (self : Immediate Prov) : Except ImmediateError Memory.ScalarInt

Equations

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

def Miri.Interpreter.Immediate.toScalarPair {Prov : Type} : Immediate Prov → Except ImmediateError (Memory.Scalar Prov × Memory.Scalar Prov)

Equations

• (Miri.Interpreter.Immediate.scalarPair first second).toScalarPair = Except.ok (first, second)
• (Miri.Interpreter.Immediate.scalar value).toScalarPair = Except.error Miri.Interpreter.ImmediateError.expectedScalarPair
• Miri.Interpreter.Immediate.uninit.toScalarPair = Except.error Miri.Interpreter.ImmediateError.unexpectedUninit

def Miri.Interpreter.Immediate.toScalarAndMeta {Prov : Type} : Immediate Prov → Except ImmediateError (Memory.Scalar Prov × MemPlaceMeta Prov)

Equations

• (Miri.Interpreter.Immediate.scalarPair first second).toScalarAndMeta = Except.ok (first, Miri.Interpreter.MemPlaceMeta.metadata second)
• (Miri.Interpreter.Immediate.scalar value).toScalarAndMeta = Except.ok (value, Miri.Interpreter.MemPlaceMeta.none)
• Miri.Interpreter.Immediate.uninit.toScalarAndMeta = Except.error Miri.Interpreter.ImmediateError.unexpectedUninit

def Miri.Interpreter.Immediate.hasProvenance {Prov : Type} : Immediate Prov → Bool

Equations

• (Miri.Interpreter.Immediate.scalar a).hasProvenance = a.isPointer
• (Miri.Interpreter.Immediate.scalarPair a a_1).hasProvenance = (a.isPointer || a_1.isPointer)
• Miri.Interpreter.Immediate.uninit.hasProvenance = false

def Miri.Interpreter.Immediate.clearProvenance {Prov : Type} [Memory.PointerProvenance Prov] : EStateM Memory.ScalarError (Immediate Prov) Unit

Preserve source in-place sequencing: if the second component fails to clear its provenance, the first component remains converted.

Equations

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

theorem Miri.Interpreter.Immediate.scalar_to_scalar {Prov : Type} (value : Memory.Scalar Prov) : (scalar value).toScalar = Except.ok value

theorem Miri.Interpreter.Immediate.uninit_has_no_provenance {Prov : Type} : uninit.hasProvenance = false