The scalar and primitive validity core from pinned rustc_const_eval::interpret::validity. It preserves the source distinction between invalid integer bits, a possibly-null relative pointer, and a pointer whose absolute address is unknown. Allocation reads and pointer/null checks remain explicit inputs; aggregate and metadata validation return delegation steps rather than being treated as successful values.

structure Miri.Memory.ScalarValidityLayout : Type

• size : ABI.Size
• validRange : ABI.WrappingRange

def Miri.Memory.instDecidableEqScalarValidityLayout.decEq (x✝ x✝¹ : ScalarValidityLayout) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarValidityLayout : DecidableEq ScalarValidityLayout

Equations

• Miri.Memory.instDecidableEqScalarValidityLayout = Miri.Memory.instDecidableEqScalarValidityLayout.decEq

@[instance_reducible]

instance Miri.Memory.instReprScalarValidityLayout : Repr ScalarValidityLayout

Equations

• Miri.Memory.instReprScalarValidityLayout = { reprPrec := Miri.Memory.instReprScalarValidityLayout.repr }

def Miri.Memory.instReprScalarValidityLayout.repr : ScalarValidityLayout → Nat → Std.Format

Equations

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

inductive Miri.Memory.ExpectedValue : Type

• boolean : ExpectedValue
• character : ExpectedValue
• float : ExpectedValue
• integer : ExpectedValue
• functionPointer : ExpectedValue
• rawPointer : ExpectedValue
• reference : ExpectedValue
• box : ExpectedValue
• string : ExpectedValue

@[instance_reducible]

instance Miri.Memory.instDecidableEqExpectedValue : DecidableEq ExpectedValue

Equations

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

def Miri.Memory.instReprExpectedValue.repr : ExpectedValue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprExpectedValue : Repr ExpectedValue

Equations

• Miri.Memory.instReprExpectedValue = { reprPrec := Miri.Memory.instReprExpectedValue.repr }

inductive Miri.Memory.SafePointerKind : Type

• reference (mutable : Bool) : SafePointerKind
• box : SafePointerKind

def Miri.Memory.instDecidableEqSafePointerKind.decEq (x✝ x✝¹ : SafePointerKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqSafePointerKind.decEq (Miri.Memory.SafePointerKind.reference a) (Miri.Memory.SafePointerKind.reference b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqSafePointerKind.decEq (Miri.Memory.SafePointerKind.reference mutable) Miri.Memory.SafePointerKind.box = isFalse ⋯
• Miri.Memory.instDecidableEqSafePointerKind.decEq Miri.Memory.SafePointerKind.box (Miri.Memory.SafePointerKind.reference mutable) = isFalse ⋯
• Miri.Memory.instDecidableEqSafePointerKind.decEq Miri.Memory.SafePointerKind.box Miri.Memory.SafePointerKind.box = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqSafePointerKind : DecidableEq SafePointerKind

Equations

• Miri.Memory.instDecidableEqSafePointerKind = Miri.Memory.instDecidableEqSafePointerKind.decEq

@[instance_reducible]

instance Miri.Memory.instReprSafePointerKind : Repr SafePointerKind

Equations

• Miri.Memory.instReprSafePointerKind = { reprPrec := Miri.Memory.instReprSafePointerKind.repr }

def Miri.Memory.instReprSafePointerKind.repr : SafePointerKind → Nat → Std.Format

Equations

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

inductive Miri.Memory.PathElem : Type

• field (name : String) : PathElem
• variant (name : String) : PathElem
• coroutineState (index : Nat) : PathElem
• capturedVar (name : String) : PathElem
• arrayElem (index : Nat) : PathElem
• tupleElem (index : Nat) : PathElem
• deref : PathElem
• enumTag : PathElem
• coroutineTag : PathElem
• dynDowncast (typeName : String) : PathElem
• vtable : PathElem

def Miri.Memory.instDecidableEqPathElem.decEq (x✝ x✝¹ : PathElem) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqPathElem : DecidableEq PathElem

Equations

• Miri.Memory.instDecidableEqPathElem = Miri.Memory.instDecidableEqPathElem.decEq

@[instance_reducible]

instance Miri.Memory.instReprPathElem : Repr PathElem

Equations

• Miri.Memory.instReprPathElem = { reprPrec := Miri.Memory.instReprPathElem.repr }

def Miri.Memory.instReprPathElem.repr : PathElem → Nat → Std.Format

Equations

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

structure Miri.Memory.ValidationPath : Type

• originalType : String
• projections : Array PathElem

@[instance_reducible]

instance Miri.Memory.instDecidableEqValidationPath : DecidableEq ValidationPath

Equations

• Miri.Memory.instDecidableEqValidationPath = Miri.Memory.instDecidableEqValidationPath.decEq

def Miri.Memory.instDecidableEqValidationPath.decEq (x✝ x✝¹ : ValidationPath) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.instReprValidationPath.repr : ValidationPath → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprValidationPath : Repr ValidationPath

Equations

• Miri.Memory.instReprValidationPath = { reprPrec := Miri.Memory.instReprValidationPath.repr }

def Miri.Memory.ValidationPath.push (path : ValidationPath) (projection : PathElem) : ValidationPath

Equations

• path.push projection = { originalType := path.originalType, projections := path.projections.push projection }

def Miri.Memory.ValidationPath.withElem {α : Type} (path : ValidationPath) (projection : PathElem) (visit : ValidationPath → α) : α

Equations

• path.withElem projection visit = visit (path.push projection)

def Miri.Memory.PathElem.render : PathElem → String

Equations

• (Miri.Memory.PathElem.field a).render = toString "." ++ toString a
• (Miri.Memory.PathElem.variant a).render = toString ".<enum-variant(" ++ toString a ++ toString ")>"
• (Miri.Memory.PathElem.coroutineState a).render = toString ".<coroutine-state(" ++ toString a ++ toString ")>"
• (Miri.Memory.PathElem.capturedVar a).render = toString ".<captured-var(" ++ toString a ++ toString ")>"
• (Miri.Memory.PathElem.arrayElem a).render = toString "[" ++ toString a ++ toString "]"
• (Miri.Memory.PathElem.tupleElem a).render = toString "." ++ toString a
• Miri.Memory.PathElem.deref.render = ".<deref>"
• Miri.Memory.PathElem.enumTag.render = ".<enum-tag>"
• Miri.Memory.PathElem.coroutineTag.render = ".<coroutine-tag>"
• (Miri.Memory.PathElem.dynDowncast a).render = toString ".<dyn-downcast(" ++ toString a ++ toString ")>"
• Miri.Memory.PathElem.vtable.render = ".<vtable>"

def Miri.Memory.ValidationPath.render (path : ValidationPath) : String

Render projections with the same spelling and order as validity.rs's write_path; originalType is kept separately, as in the source Path.

Equations

• path.render = String.join (List.map Miri.Memory.PathElem.render path.projections.toList)

inductive Miri.Memory.RangeSetError : Type

• memory (reason : MemoryError) : RangeSetError
• malformedRangeSet : RangeSetError

@[instance_reducible]

instance Miri.Memory.instDecidableEqRangeSetError : DecidableEq RangeSetError

Equations

• Miri.Memory.instDecidableEqRangeSetError = Miri.Memory.instDecidableEqRangeSetError.decEq

def Miri.Memory.instDecidableEqRangeSetError.decEq (x✝ x✝¹ : RangeSetError) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqRangeSetError.decEq (Miri.Memory.RangeSetError.memory a) (Miri.Memory.RangeSetError.memory b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqRangeSetError.decEq (Miri.Memory.RangeSetError.memory reason) Miri.Memory.RangeSetError.malformedRangeSet = isFalse ⋯
• Miri.Memory.instDecidableEqRangeSetError.decEq Miri.Memory.RangeSetError.malformedRangeSet (Miri.Memory.RangeSetError.memory reason) = isFalse ⋯
• Miri.Memory.instDecidableEqRangeSetError.decEq Miri.Memory.RangeSetError.malformedRangeSet Miri.Memory.RangeSetError.malformedRangeSet = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.instReprRangeSetError : Repr RangeSetError

Equations

• Miri.Memory.instReprRangeSetError = { reprPrec := Miri.Memory.instReprRangeSetError.repr }

def Miri.Memory.instReprRangeSetError.repr : RangeSetError → Nat → Std.Format

Equations

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

inductive Miri.Memory.PaddingPlanError : Type

• memory (reason : MemoryError) : PaddingPlanError
• invalidDataRangeOrder (previousEnd nextStart : ABI.Size) : PaddingPlanError
• finalCoverageMismatch (expectedEnd actualEnd : ABI.Size) : PaddingPlanError

@[instance_reducible]

instance Miri.Memory.instDecidableEqPaddingPlanError : DecidableEq PaddingPlanError

Equations

• Miri.Memory.instDecidableEqPaddingPlanError = Miri.Memory.instDecidableEqPaddingPlanError.decEq

def Miri.Memory.instDecidableEqPaddingPlanError.decEq (x✝ x✝¹ : PaddingPlanError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqPaddingPlanError.decEq (Miri.Memory.PaddingPlanError.memory a) (Miri.Memory.PaddingPlanError.memory b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqPaddingPlanError.decEq (Miri.Memory.PaddingPlanError.memory reason) (Miri.Memory.PaddingPlanError.invalidDataRangeOrder previousEnd nextStart) = isFalse ⋯
• Miri.Memory.instDecidableEqPaddingPlanError.decEq (Miri.Memory.PaddingPlanError.memory reason) (Miri.Memory.PaddingPlanError.finalCoverageMismatch expectedEnd actualEnd) = isFalse ⋯
• Miri.Memory.instDecidableEqPaddingPlanError.decEq (Miri.Memory.PaddingPlanError.invalidDataRangeOrder previousEnd nextStart) (Miri.Memory.PaddingPlanError.memory reason) = isFalse ⋯
• Miri.Memory.instDecidableEqPaddingPlanError.decEq (Miri.Memory.PaddingPlanError.finalCoverageMismatch expectedEnd actualEnd) (Miri.Memory.PaddingPlanError.memory reason) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprPaddingPlanError : Repr PaddingPlanError

Equations

• Miri.Memory.instReprPaddingPlanError = { reprPrec := Miri.Memory.instReprPaddingPlanError.repr }

def Miri.Memory.instReprPaddingPlanError.repr : PaddingPlanError → Nat → Std.Format

Equations

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

inductive Miri.Memory.AggregatePathError : Type

• multipleTagOnNonVariantType (typeName : String) : AggregatePathError
• emptyEnumField : AggregatePathError
• multipleEnumFieldWithoutActiveVariant : AggregatePathError
• missingFieldName (typeName : String) (field : Nat) : AggregatePathError
• missingVariantName (typeName : String) (variant : Nat) : AggregatePathError
• dynamicFieldIndex (field : Nat) : AggregatePathError
• unexpectedVariantType (typeName : String) : AggregatePathError
• unsupportedAggregate (typeName : String) : AggregatePathError

@[instance_reducible]

instance Miri.Memory.instDecidableEqAggregatePathError : DecidableEq AggregatePathError

Equations

• Miri.Memory.instDecidableEqAggregatePathError = Miri.Memory.instDecidableEqAggregatePathError.decEq

def Miri.Memory.instDecidableEqAggregatePathError.decEq (x✝ x✝¹ : AggregatePathError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.multipleTagOnNonVariantType typeName) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.multipleTagOnNonVariantType typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField Miri.Memory.AggregatePathError.emptyEnumField = isTrue ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.missingFieldName typeName field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.missingVariantName typeName variant) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.dynamicFieldIndex field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.unexpectedVariantType typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.emptyEnumField (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq Miri.Memory.AggregatePathError.multipleEnumFieldWithoutActiveVariant (Miri.Memory.AggregatePathError.dynamicFieldIndex field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.missingFieldName typeName field) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.missingFieldName typeName field) (Miri.Memory.AggregatePathError.dynamicFieldIndex field_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.missingFieldName typeName field) (Miri.Memory.AggregatePathError.unsupportedAggregate typeName_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.missingVariantName typeName variant) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.missingVariantName typeName variant) (Miri.Memory.AggregatePathError.dynamicFieldIndex field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) (Miri.Memory.AggregatePathError.multipleTagOnNonVariantType typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) Miri.Memory.AggregatePathError.multipleEnumFieldWithoutActiveVariant = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) (Miri.Memory.AggregatePathError.missingFieldName typeName field_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) (Miri.Memory.AggregatePathError.missingVariantName typeName variant) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) (Miri.Memory.AggregatePathError.unexpectedVariantType typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.dynamicFieldIndex field) (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unexpectedVariantType typeName) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unexpectedVariantType typeName) (Miri.Memory.AggregatePathError.dynamicFieldIndex field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unexpectedVariantType typeName) (Miri.Memory.AggregatePathError.unsupportedAggregate typeName_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) Miri.Memory.AggregatePathError.emptyEnumField = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) (Miri.Memory.AggregatePathError.missingFieldName typeName_1 field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) (Miri.Memory.AggregatePathError.dynamicFieldIndex field) = isFalse ⋯
• Miri.Memory.instDecidableEqAggregatePathError.decEq (Miri.Memory.AggregatePathError.unsupportedAggregate typeName) (Miri.Memory.AggregatePathError.unexpectedVariantType typeName_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprAggregatePathError : Repr AggregatePathError

Equations

• Miri.Memory.instReprAggregatePathError = { reprPrec := Miri.Memory.instReprAggregatePathError.repr }

def Miri.Memory.instReprAggregatePathError.repr : AggregatePathError → Nat → Std.Format

Equations

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

inductive Miri.Memory.UnionDataRangeError : Type

• invalidNodeIndex (index available : Nat) : UnionDataRangeError
• recursiveLayout (node : Nat) : UnionDataRangeError
• malformedFieldOffsets (children offsets : Nat) : UnionDataRangeError
• memory (reason : MemoryError) : UnionDataRangeError
• rangeSet (reason : RangeSetError) : UnionDataRangeError

def Miri.Memory.instDecidableEqUnionDataRangeError.decEq (x✝ x✝¹ : UnionDataRangeError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) (Miri.Memory.UnionDataRangeError.recursiveLayout node) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) (Miri.Memory.UnionDataRangeError.memory reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) (Miri.Memory.UnionDataRangeError.rangeSet reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.recursiveLayout node) (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.recursiveLayout node) (Miri.Memory.UnionDataRangeError.malformedFieldOffsets children offsets) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.recursiveLayout node) (Miri.Memory.UnionDataRangeError.memory reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.recursiveLayout node) (Miri.Memory.UnionDataRangeError.rangeSet reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.malformedFieldOffsets children offsets) (Miri.Memory.UnionDataRangeError.memory reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.malformedFieldOffsets children offsets) (Miri.Memory.UnionDataRangeError.rangeSet reason) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.memory reason) (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.memory reason) (Miri.Memory.UnionDataRangeError.recursiveLayout node) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.memory reason) (Miri.Memory.UnionDataRangeError.malformedFieldOffsets children offsets) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.memory a) (Miri.Memory.UnionDataRangeError.memory b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.memory reason) (Miri.Memory.UnionDataRangeError.rangeSet reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.rangeSet reason) (Miri.Memory.UnionDataRangeError.invalidNodeIndex index available) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.rangeSet reason) (Miri.Memory.UnionDataRangeError.recursiveLayout node) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.rangeSet reason) (Miri.Memory.UnionDataRangeError.malformedFieldOffsets children offsets) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.rangeSet reason) (Miri.Memory.UnionDataRangeError.memory reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqUnionDataRangeError.decEq (Miri.Memory.UnionDataRangeError.rangeSet a) (Miri.Memory.UnionDataRangeError.rangeSet b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqUnionDataRangeError : DecidableEq UnionDataRangeError

Equations

• Miri.Memory.instDecidableEqUnionDataRangeError = Miri.Memory.instDecidableEqUnionDataRangeError.decEq

def Miri.Memory.instReprUnionDataRangeError.repr : UnionDataRangeError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprUnionDataRangeError : Repr UnionDataRangeError

Equations

• Miri.Memory.instReprUnionDataRangeError = { reprPrec := Miri.Memory.instReprUnionDataRangeError.repr }

inductive Miri.Memory.ValidityFailure : Type

• uninitialized (expected : ExpectedValue) (info : Option BadBytesAccess) : ValidityFailure
• pointerAsInt (expected : ExpectedValue) (info : Option BadBytesAccess) : ValidityFailure
• partialPointer (offset : ABI.Size) : ValidityFailure
• invalidBool (value : UInt8) : ValidityFailure
• invalidChar (value : UInt32) : ValidityFailure
• invalidScalarBits (bits : ABI.U128) (layout : ScalarValidityLayout) : ValidityFailure
• maybeNullPointer : ValidityFailure
• unknownAbsoluteAddress (layout : ScalarValidityLayout) : ValidityFailure
• nullSafePointer (kind : SafePointerKind) (maybe : Bool) : ValidityFailure
• uninhabitedPointee (kind : SafePointerKind) : ValidityFailure
• addressTooClose (kind : SafePointerKind) (size : ABI.Size) : ValidityFailure
• readOnlyPointer (kind : SafePointerKind) : ValidityFailure
• unsafeCellInReadOnlyMemory : ValidityFailure
• nullFunctionPointer (maybe : Bool) : ValidityFailure
• danglingSafePointer (kind : SafePointerKind) : ValidityFailure
• mutablePointerToReadOnly (kind : SafePointerKind) : ValidityFailure
• neverValue : ValidityFailure

def Miri.Memory.instDecidableEqValidityFailure.decEq (x✝ x✝¹ : ValidityFailure) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqValidityFailure : DecidableEq ValidityFailure

Equations

• Miri.Memory.instDecidableEqValidityFailure = Miri.Memory.instDecidableEqValidityFailure.decEq

@[instance_reducible]

instance Miri.Memory.instReprValidityFailure : Repr ValidityFailure

Equations

• Miri.Memory.instReprValidityFailure = { reprPrec := Miri.Memory.instReprValidityFailure.repr }

def Miri.Memory.instReprValidityFailure.repr : ValidityFailure → Nat → Std.Format

Equations

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

inductive Miri.Memory.ValidityError (MachineError : Type) : Type

• failure {MachineError : Type} (reason : ValidityFailure) : ValidityError MachineError
• pathFailure {MachineError : Type} (path : ValidationPath) (reason : ValidityFailure) : ValidityError MachineError
• scalar {MachineError : Type} (reason : ScalarError) : ValidityError MachineError
• range {MachineError : Type} (reason : ABI.WrappingRangeError) : ValidityError MachineError
• rangeSet {MachineError : Type} (reason : RangeSetError) : ValidityError MachineError
• padding {MachineError : Type} (reason : PaddingPlanError) : ValidityError MachineError
• pathInvariant {MachineError : Type} (reason : AggregatePathError) : ValidityError MachineError
• unionRange {MachineError : Type} (reason : UnionDataRangeError) : ValidityError MachineError
• walkInvariant {MachineError : Type} (reason : String) : ValidityError MachineError
• rangeInvariant {MachineError : Type} (reason : String) : ValidityError MachineError
• machine {MachineError : Type} (reason : MachineError) : ValidityError MachineError

@[instance_reducible]

instance Miri.Memory.instDecidableEqValidityError {MachineError✝ : Type} [DecidableEq MachineError✝] : DecidableEq (ValidityError MachineError✝)

Equations

• Miri.Memory.instDecidableEqValidityError = Miri.Memory.instDecidableEqValidityError.decEq

def Miri.Memory.instDecidableEqValidityError.decEq {MachineError✝ : Type} [DecidableEq MachineError✝] (x✝ x✝¹ : ValidityError MachineError✝) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.instReprValidityError.repr {MachineError✝ : Type} [Repr MachineError✝] : ValidityError MachineError✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprValidityError {MachineError✝ : Type} [Repr MachineError✝] : Repr (ValidityError MachineError✝)

Equations

• Miri.Memory.instReprValidityError = { reprPrec := Miri.Memory.instReprValidityError.repr }

inductive Miri.Memory.PrimitiveKind : Type

• boolean : PrimitiveKind
• character : PrimitiveKind
• scalar : PrimitiveKind
• never : PrimitiveKind
• foreign : PrimitiveKind
• functionDefinition : PrimitiveKind
• rawPointer (pointeeSized : Bool) : PrimitiveKind
• safeReference : PrimitiveKind
• box : PrimitiveKind
• functionPointer : PrimitiveKind
• aggregate : PrimitiveKind

def Miri.Memory.instDecidableEqPrimitiveKind.decEq (x✝ x✝¹ : PrimitiveKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqPrimitiveKind : DecidableEq PrimitiveKind

Equations

• Miri.Memory.instDecidableEqPrimitiveKind = Miri.Memory.instDecidableEqPrimitiveKind.decEq

@[instance_reducible]

instance Miri.Memory.instReprPrimitiveKind : Repr PrimitiveKind

Equations

• Miri.Memory.instReprPrimitiveKind = { reprPrec := Miri.Memory.instReprPrimitiveKind.repr }

def Miri.Memory.instReprPrimitiveKind.repr : PrimitiveKind → Nat → Std.Format

Equations

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

inductive Miri.Memory.PrimitiveStep : Type

Non-scalar work is returned to the caller as a required validation step. The caller must supply the matching recursive, metadata, or pointer hooks.

• valid : PrimitiveStep
• recurse : PrimitiveStep
• rawPointerMetadata : PrimitiveStep
• safePointer : PrimitiveStep
• boxPointer : PrimitiveStep
• functionPointer : PrimitiveStep

@[instance_reducible]

instance Miri.Memory.instDecidableEqPrimitiveStep : DecidableEq PrimitiveStep

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprPrimitiveStep : Repr PrimitiveStep

Equations

• Miri.Memory.instReprPrimitiveStep = { reprPrec := Miri.Memory.instReprPrimitiveStep.repr }

def Miri.Memory.instReprPrimitiveStep.repr : PrimitiveStep → Nat → Std.Format

Equations

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

structure Miri.Memory.Validity.DataRangeSet : Type

Sorted, disjoint, non-adjacent set of data-byte ranges used by the source visitor's padding reset. Its constructor is private so malformed interval arrays cannot enter the visitor through this API.

• ranges : Array Miri.Memory.AllocRange

def Miri.Memory.Validity.instDecidableEqDataRangeSet.decEq (x✝ x✝¹ : DataRangeSet) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.Validity.instDecidableEqDataRangeSet.decEq { ranges := a } { ranges := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqDataRangeSet : DecidableEq DataRangeSet

Equations

• Miri.Memory.Validity.instDecidableEqDataRangeSet = Miri.Memory.Validity.instDecidableEqDataRangeSet.decEq

def Miri.Memory.Validity.instReprDataRangeSet.repr : DataRangeSet → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprDataRangeSet : Repr DataRangeSet

Equations

• Miri.Memory.Validity.instReprDataRangeSet = { reprPrec := Miri.Memory.Validity.instReprDataRangeSet.repr }

def Miri.Memory.Validity.DataRangeSet.empty : DataRangeSet

Equations

• Miri.Memory.Validity.DataRangeSet.empty = { ranges := #[] }

def Miri.Memory.Validity.DataRangeSet.toArray (ranges : DataRangeSet) : Array AllocRange

Equations

• ranges.toArray = Miri.Memory.Validity.DataRangeSet.ranges✝ ranges

def Miri.Memory.Validity.DataRangeSet.addRange (ranges : DataRangeSet) (offset size : ABI.Size) : Except RangeSetError DataRangeSet

Source RangeSet::add_range: zero-sized ranges are ignored; overlapping and adjacent ranges coalesce, preserving sorted disjoint storage.

Equations

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

def Miri.Memory.Validity.DataRangeSet.containsRange (ranges : DataRangeSet) (range : AllocRange) : Bool

Equations

• ranges.containsRange range = (Miri.Memory.Validity.DataRangeSet.ranges✝ ranges).any fun (x : Miri.Memory.AllocRange) => x == range

inductive Miri.Memory.Validity.UnionFieldsShape : Type

• primitive : UnionFieldsShape
• unionFields (children : Array Nat) : UnionFieldsShape
• array (element : Nat) (stride : ABI.Size) (count : UInt64) (elementIsScalar : Bool) : UnionFieldsShape
• arbitrary (children : Array Nat) (offsets : Array ABI.Size) : UnionFieldsShape

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqUnionFieldsShape : DecidableEq UnionFieldsShape

Equations

• Miri.Memory.Validity.instDecidableEqUnionFieldsShape = Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq

def Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq (x✝ x✝¹ : UnionFieldsShape) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq Miri.Memory.Validity.UnionFieldsShape.primitive Miri.Memory.Validity.UnionFieldsShape.primitive = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq Miri.Memory.Validity.UnionFieldsShape.primitive (Miri.Memory.Validity.UnionFieldsShape.unionFields children) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq Miri.Memory.Validity.UnionFieldsShape.primitive (Miri.Memory.Validity.UnionFieldsShape.arbitrary children offsets) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq (Miri.Memory.Validity.UnionFieldsShape.unionFields children) Miri.Memory.Validity.UnionFieldsShape.primitive = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionFieldsShape.decEq (Miri.Memory.Validity.UnionFieldsShape.arbitrary children offsets) Miri.Memory.Validity.UnionFieldsShape.primitive = isFalse ⋯

def Miri.Memory.Validity.instReprUnionFieldsShape.repr : UnionFieldsShape → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprUnionFieldsShape : Repr UnionFieldsShape

Equations

• Miri.Memory.Validity.instReprUnionFieldsShape = { reprPrec := Miri.Memory.Validity.instReprUnionFieldsShape.repr }

inductive Miri.Memory.Validity.UnionVariantsShape : Type

• single : UnionVariantsShape
• empty : UnionVariantsShape
• multiple (variants : Array Nat) : UnionVariantsShape

def Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq (x✝ x✝¹ : UnionVariantsShape) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq Miri.Memory.Validity.UnionVariantsShape.single Miri.Memory.Validity.UnionVariantsShape.single = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq Miri.Memory.Validity.UnionVariantsShape.single (Miri.Memory.Validity.UnionVariantsShape.multiple variants) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq Miri.Memory.Validity.UnionVariantsShape.empty Miri.Memory.Validity.UnionVariantsShape.empty = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq Miri.Memory.Validity.UnionVariantsShape.empty (Miri.Memory.Validity.UnionVariantsShape.multiple variants) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq (Miri.Memory.Validity.UnionVariantsShape.multiple variants) Miri.Memory.Validity.UnionVariantsShape.single = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq (Miri.Memory.Validity.UnionVariantsShape.multiple variants) Miri.Memory.Validity.UnionVariantsShape.empty = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqUnionVariantsShape : DecidableEq UnionVariantsShape

Equations

• Miri.Memory.Validity.instDecidableEqUnionVariantsShape = Miri.Memory.Validity.instDecidableEqUnionVariantsShape.decEq

def Miri.Memory.Validity.instReprUnionVariantsShape.repr : UnionVariantsShape → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprUnionVariantsShape : Repr UnionVariantsShape

Equations

• Miri.Memory.Validity.instReprUnionVariantsShape = { reprPrec := Miri.Memory.Validity.instReprUnionVariantsShape.repr }

structure Miri.Memory.Validity.UnionLayoutNode : Type

A finite, indexed description of one TyAndLayout node for the pure union_data_range_uncached traversal. Child indices deliberately remain checked at runtime: malformed synthetic layouts cannot be mistaken for an empty union. elementIsScalar is the upstream backend-representation fast-path fact for array elements.

• size : ABI.Size
• fields : UnionFieldsShape
• variants : UnionVariantsShape

def Miri.Memory.Validity.instDecidableEqUnionLayoutNode.decEq (x✝ x✝¹ : UnionLayoutNode) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqUnionLayoutNode : DecidableEq UnionLayoutNode

Equations

• Miri.Memory.Validity.instDecidableEqUnionLayoutNode = Miri.Memory.Validity.instDecidableEqUnionLayoutNode.decEq

@[instance_reducible]

instance Miri.Memory.Validity.instReprUnionLayoutNode : Repr UnionLayoutNode

Equations

• Miri.Memory.Validity.instReprUnionLayoutNode = { reprPrec := Miri.Memory.Validity.instReprUnionLayoutNode.repr }

def Miri.Memory.Validity.instReprUnionLayoutNode.repr : UnionLayoutNode → Nat → Std.Format

Equations

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

structure Miri.Memory.Validity.UnionLayoutGraph : Type

• root : Nat
• nodes : Array UnionLayoutNode

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqUnionLayoutGraph : DecidableEq UnionLayoutGraph

Equations

• Miri.Memory.Validity.instDecidableEqUnionLayoutGraph = Miri.Memory.Validity.instDecidableEqUnionLayoutGraph.decEq

def Miri.Memory.Validity.instDecidableEqUnionLayoutGraph.decEq (x✝ x✝¹ : UnionLayoutGraph) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprUnionLayoutGraph : Repr UnionLayoutGraph

Equations

• Miri.Memory.Validity.instReprUnionLayoutGraph = { reprPrec := Miri.Memory.Validity.instReprUnionLayoutGraph.repr }

def Miri.Memory.Validity.instReprUnionLayoutGraph.repr : UnionLayoutGraph → Nat → Std.Format

Equations

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

def Miri.Memory.Validity.unionDataRange (graph : UnionLayoutGraph) : Except UnionDataRangeError DataRangeSet

Exact recursive layout walk from ValidityVisitor::union_data_range. The work stack implements its depth-first recursion while detecting malformed cycles and checking each source Size operation.

Equations

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

inductive Miri.Memory.Validity.CtfeMode : Type

• static (mutable : Bool) : CtfeMode
• promoted : CtfeMode
• constant (allowImmutableUnsafeCell : Bool) : CtfeMode

def Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (x✝ x✝¹ : CtfeMode) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.static a) (Miri.Memory.Validity.CtfeMode.static b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.static mutable) Miri.Memory.Validity.CtfeMode.promoted = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.static mutable) (Miri.Memory.Validity.CtfeMode.constant allowImmutableUnsafeCell) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq Miri.Memory.Validity.CtfeMode.promoted (Miri.Memory.Validity.CtfeMode.static mutable) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq Miri.Memory.Validity.CtfeMode.promoted Miri.Memory.Validity.CtfeMode.promoted = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq Miri.Memory.Validity.CtfeMode.promoted (Miri.Memory.Validity.CtfeMode.constant allowImmutableUnsafeCell) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.constant allowImmutableUnsafeCell) (Miri.Memory.Validity.CtfeMode.static mutable) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.constant allowImmutableUnsafeCell) Miri.Memory.Validity.CtfeMode.promoted = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqCtfeMode.decEq (Miri.Memory.Validity.CtfeMode.constant a) (Miri.Memory.Validity.CtfeMode.constant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqCtfeMode : DecidableEq CtfeMode

Equations

• Miri.Memory.Validity.instDecidableEqCtfeMode = Miri.Memory.Validity.instDecidableEqCtfeMode.decEq

def Miri.Memory.Validity.instReprCtfeMode.repr : CtfeMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprCtfeMode : Repr CtfeMode

Equations

• Miri.Memory.Validity.instReprCtfeMode = { reprPrec := Miri.Memory.Validity.instReprCtfeMode.repr }

def Miri.Memory.Validity.allowsImmutableUnsafeCell : CtfeMode → Bool

Equations

• Miri.Memory.Validity.allowsImmutableUnsafeCell (Miri.Memory.Validity.CtfeMode.constant allow) = allow
• Miri.Memory.Validity.allowsImmutableUnsafeCell (Miri.Memory.Validity.CtfeMode.static mutable) = false
• Miri.Memory.Validity.allowsImmutableUnsafeCell Miri.Memory.Validity.CtfeMode.promoted = false

def Miri.Memory.Validity.checkUnsafeCell {MachineError HookState : Type} (mode : Option CtfeMode) (isZeroSized isUnsafeCell : Bool) (path : ValidationPath) (isMutableMemory : HookState → EStateM.Result (ValidityError MachineError) HookState Bool) : EStateM (ValidityError MachineError) HookState Unit

Source visit_value's UnsafeCell check for the current ADT node. The memory mutability query is required only after CTFE policy, dynamic ZST, and the type predicate establish that it matters.

Equations

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

structure Miri.Memory.Validity.UnionVisitHooks (MachineError HookState : Type) : Type

• dynamicSize : HookState → EStateM.Result (ValidityError MachineError) HookState (Option ABI.Size)
• isFreeze : HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• isMutableMemory : HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• dataRangeOffset : HookState → EStateM.Result (ValidityError MachineError) HookState ABI.Size

def Miri.Memory.Validity.visitUnion {MachineError HookState : Type} (hooks : UnionVisitHooks MachineError HookState) (mode : Option CtfeMode) (path : ValidationPath) (resetProvenanceAndPadding : Bool) (dataBytes : Option DataRangeSet) (layout : UnionLayoutGraph) : EStateM (ValidityError MachineError) HookState (Option DataRangeSet)

Source ValueVisitor::visit_union: CTFE checks !Freeze before data range collection, and only tracked typed copies query the containing offset. Union layout/range failures remain distinct from validation UB and machine lookup failures.

Equations

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

inductive Miri.Memory.Validity.AggregateTypeKind : Type

• closure : AggregateTypeKind
• coroutine : AggregateTypeKind
• coroutineClosure : AggregateTypeKind
• tuple : AggregateTypeKind
• enum : AggregateTypeKind
• struct : AggregateTypeKind
• array : AggregateTypeKind
• slice : AggregateTypeKind
• dynamic : AggregateTypeKind
• other (typeName : String) : AggregateTypeKind

def Miri.Memory.Validity.instDecidableEqAggregateTypeKind.decEq (x✝ x✝¹ : AggregateTypeKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqAggregateTypeKind : DecidableEq AggregateTypeKind

Equations

• Miri.Memory.Validity.instDecidableEqAggregateTypeKind = Miri.Memory.Validity.instDecidableEqAggregateTypeKind.decEq

def Miri.Memory.Validity.instReprAggregateTypeKind.repr : AggregateTypeKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprAggregateTypeKind : Repr AggregateTypeKind

Equations

• Miri.Memory.Validity.instReprAggregateTypeKind = { reprPrec := Miri.Memory.Validity.instReprAggregateTypeKind.repr }

inductive Miri.Memory.Validity.VariantLayoutKind : Type

• multiple (tagField : Nat) : VariantLayoutKind
• single : VariantLayoutKind
• empty : VariantLayoutKind

def Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq (x✝ x✝¹ : VariantLayoutKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq (Miri.Memory.Validity.VariantLayoutKind.multiple tagField) Miri.Memory.Validity.VariantLayoutKind.single = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq (Miri.Memory.Validity.VariantLayoutKind.multiple tagField) Miri.Memory.Validity.VariantLayoutKind.empty = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq Miri.Memory.Validity.VariantLayoutKind.single (Miri.Memory.Validity.VariantLayoutKind.multiple tagField) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq Miri.Memory.Validity.VariantLayoutKind.single Miri.Memory.Validity.VariantLayoutKind.single = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq Miri.Memory.Validity.VariantLayoutKind.empty (Miri.Memory.Validity.VariantLayoutKind.multiple tagField) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq Miri.Memory.Validity.VariantLayoutKind.empty Miri.Memory.Validity.VariantLayoutKind.empty = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqVariantLayoutKind : DecidableEq VariantLayoutKind

Equations

• Miri.Memory.Validity.instDecidableEqVariantLayoutKind = Miri.Memory.Validity.instDecidableEqVariantLayoutKind.decEq

def Miri.Memory.Validity.instReprVariantLayoutKind.repr : VariantLayoutKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprVariantLayoutKind : Repr VariantLayoutKind

Equations

• Miri.Memory.Validity.instReprVariantLayoutKind = { reprPrec := Miri.Memory.Validity.instReprVariantLayoutKind.repr }

structure Miri.Memory.Validity.AggregatePathInfo : Type

• typeName : String
• kind : AggregateTypeKind
• variants : VariantLayoutKind
• field : Nat
• fieldName : Option String
• capturedVariableName : Option String
• fieldTypeName : String

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqAggregatePathInfo : DecidableEq AggregatePathInfo

Equations

• Miri.Memory.Validity.instDecidableEqAggregatePathInfo = Miri.Memory.Validity.instDecidableEqAggregatePathInfo.decEq

def Miri.Memory.Validity.instDecidableEqAggregatePathInfo.decEq (x✝ x✝¹ : AggregatePathInfo) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.Validity.instReprAggregatePathInfo.repr : AggregatePathInfo → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprAggregatePathInfo : Repr AggregatePathInfo

Equations

• Miri.Memory.Validity.instReprAggregatePathInfo = { reprPrec := Miri.Memory.Validity.instReprAggregatePathInfo.repr }

def Miri.Memory.Validity.aggregateFieldPathElem (info : AggregatePathInfo) : Except AggregatePathError PathElem

Port of aggregate_field_path_elem. Layout and HIR lookup facts are explicit inputs; closure captures fall back to the source's numeric symbol.

Equations

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

def Miri.Memory.Validity.visitAggregateField {MachineError HookState α : Type} (path : ValidationPath) (info : AggregatePathInfo) (visit : ValidationPath → EStateM (ValidityError MachineError) HookState α) : EStateM (ValidityError MachineError) HookState α

Source visit_field path scoping. The projection lookup is evaluated before the child visitor, and only that child sees the extended path.

Equations

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

def Miri.Memory.Validity.variantPathElem (typeName : String) (kind : AggregateTypeKind) (variant : Nat) (name : Option String) : Except AggregatePathError PathElem

Source visit_variant path selection for ADTs and coroutines.

Equations

• Miri.Memory.Validity.variantPathElem typeName Miri.Memory.Validity.AggregateTypeKind.enum variant (some name_1) = pure (Miri.Memory.PathElem.variant name_1)
• Miri.Memory.Validity.variantPathElem typeName Miri.Memory.Validity.AggregateTypeKind.enum variant none = throw (Miri.Memory.AggregatePathError.missingVariantName typeName variant)
• Miri.Memory.Validity.variantPathElem typeName Miri.Memory.Validity.AggregateTypeKind.coroutine variant name = pure (Miri.Memory.PathElem.coroutineState variant)
• Miri.Memory.Validity.variantPathElem typeName kind variant name = throw (Miri.Memory.AggregatePathError.unexpectedVariantType typeName)

def Miri.Memory.Validity.visitAggregateVariant {MachineError HookState α : Type} (path : ValidationPath) (typeName : String) (kind : AggregateTypeKind) (variant : Nat) (name : Option String) (visit : ValidationPath → EStateM (ValidityError MachineError) HookState α) : EStateM (ValidityError MachineError) HookState α

Equations

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

def Miri.Memory.Validity.paddingWrites (data : DataRangeSet) (start size : ABI.Size) : Except PaddingPlanError (Array AllocRange)

Compute source reset_padding writes. The final zero-length sentinel closes the last gap; malformed/out-of-object ranges return explicit invariant failures instead of relying on rustc assertions or Size panics.

Equations

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

def Miri.Memory.Validity.resetPadding {MachineError HookState : Type} (data : Option DataRangeSet) (allocationRange : HookState → EStateM.Result (ValidityError MachineError) HookState (Option (ABI.Size × ABI.Size))) (writeUninit : AllocRange → HookState → EStateM.Result (ValidityError MachineError) HookState Unit) : EStateM (ValidityError MachineError) HookState Unit

Execute the planned padding writes in source order. The allocation lookup and byte-mask mutations stay on explicit machine callbacks; a failed write retains all earlier callback state. none data tracking and ZST places are source no-ops.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.resetPadding data allocationRange writeUninit initialState = (pure (EStateM.Result.ok () initialState)).run

inductive Miri.Memory.Validity.MetadataKind : Type

• sized : MetadataKind
• dynamic : MetadataKind
• slice : MetadataKind
• string : MetadataKind
• foreign : MetadataKind
• unexpected (description : String) : MetadataKind

def Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (x✝ x✝¹ : MetadataKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.sized Miri.Memory.Validity.MetadataKind.sized = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.sized (Miri.Memory.Validity.MetadataKind.unexpected description) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.dynamic Miri.Memory.Validity.MetadataKind.dynamic = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.dynamic (Miri.Memory.Validity.MetadataKind.unexpected description) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.slice Miri.Memory.Validity.MetadataKind.slice = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.slice (Miri.Memory.Validity.MetadataKind.unexpected description) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.string Miri.Memory.Validity.MetadataKind.string = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.string (Miri.Memory.Validity.MetadataKind.unexpected description) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.foreign Miri.Memory.Validity.MetadataKind.foreign = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq Miri.Memory.Validity.MetadataKind.foreign (Miri.Memory.Validity.MetadataKind.unexpected description) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (Miri.Memory.Validity.MetadataKind.unexpected description) Miri.Memory.Validity.MetadataKind.sized = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (Miri.Memory.Validity.MetadataKind.unexpected description) Miri.Memory.Validity.MetadataKind.dynamic = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (Miri.Memory.Validity.MetadataKind.unexpected description) Miri.Memory.Validity.MetadataKind.slice = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (Miri.Memory.Validity.MetadataKind.unexpected description) Miri.Memory.Validity.MetadataKind.string = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqMetadataKind.decEq (Miri.Memory.Validity.MetadataKind.unexpected description) Miri.Memory.Validity.MetadataKind.foreign = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqMetadataKind : DecidableEq MetadataKind

Equations

• Miri.Memory.Validity.instDecidableEqMetadataKind = Miri.Memory.Validity.instDecidableEqMetadataKind.decEq

@[instance_reducible]

instance Miri.Memory.Validity.instReprMetadataKind : Repr MetadataKind

Equations

• Miri.Memory.Validity.instReprMetadataKind = { reprPrec := Miri.Memory.Validity.instReprMetadataKind.repr }

def Miri.Memory.Validity.instReprMetadataKind.repr : MetadataKind → Nat → Std.Format

Equations

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

inductive Miri.Memory.Validity.GlobalAllocationKind : Type

• static (nested foreignItem : Bool) : GlobalAllocationKind
• other : GlobalAllocationKind

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqGlobalAllocationKind : DecidableEq GlobalAllocationKind

Equations

• Miri.Memory.Validity.instDecidableEqGlobalAllocationKind = Miri.Memory.Validity.instDecidableEqGlobalAllocationKind.decEq

def Miri.Memory.Validity.instDecidableEqGlobalAllocationKind.decEq (x✝ x✝¹ : GlobalAllocationKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqGlobalAllocationKind.decEq Miri.Memory.Validity.GlobalAllocationKind.other (Miri.Memory.Validity.GlobalAllocationKind.static nested foreignItem) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqGlobalAllocationKind.decEq Miri.Memory.Validity.GlobalAllocationKind.other Miri.Memory.Validity.GlobalAllocationKind.other = isTrue ⋯

def Miri.Memory.Validity.instReprGlobalAllocationKind.repr : GlobalAllocationKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprGlobalAllocationKind : Repr GlobalAllocationKind

Equations

• Miri.Memory.Validity.instReprGlobalAllocationKind = { reprPrec := Miri.Memory.Validity.instReprGlobalAllocationKind.repr }

inductive Miri.Memory.Validity.PointerAllocLookup : Type

Machine lookup facts needed by the source CTFE recursion policy. The allocation identity/global query itself belongs to the interpreter callback; the policy decisions are performed here.

• noAllocationId : PointerAllocLookup
• missingGlobal (stillInMemory : Bool) : PointerAllocLookup
• global (size : ABI.Size) (mutability : Mutability) (kind : GlobalAllocationKind) : PointerAllocLookup

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqPointerAllocLookup : DecidableEq PointerAllocLookup

Equations

• Miri.Memory.Validity.instDecidableEqPointerAllocLookup = Miri.Memory.Validity.instDecidableEqPointerAllocLookup.decEq

def Miri.Memory.Validity.instDecidableEqPointerAllocLookup.decEq (x✝ x✝¹ : PointerAllocLookup) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqPointerAllocLookup.decEq Miri.Memory.Validity.PointerAllocLookup.noAllocationId Miri.Memory.Validity.PointerAllocLookup.noAllocationId = isTrue ⋯

def Miri.Memory.Validity.instReprPointerAllocLookup.repr : PointerAllocLookup → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprPointerAllocLookup : Repr PointerAllocLookup

Equations

• Miri.Memory.Validity.instReprPointerAllocLookup = { reprPrec := Miri.Memory.Validity.instReprPointerAllocLookup.repr }

def Miri.Memory.Validity.ctfeRecursionDecision (mode : CtfeMode) (kind : SafePointerKind) (lookup : PointerAllocLookup) : Except ValidityFailure Bool

Source CTFE-only allocation and mutability checks performed before adding a safe pointer to the recursive worklist. The true result means skip the descent (including the source's delayed-bug/missing-interning early return).

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.ctfeRecursionDecision mode kind Miri.Memory.Validity.PointerAllocLookup.noAllocationId = pure false
• Miri.Memory.Validity.ctfeRecursionDecision mode kind (Miri.Memory.Validity.PointerAllocLookup.missingGlobal true) = pure true
• Miri.Memory.Validity.ctfeRecursionDecision mode kind (Miri.Memory.Validity.PointerAllocLookup.missingGlobal false) = throw (Miri.Memory.ValidityFailure.danglingSafePointer kind)

structure Miri.Memory.Validity.VisitorFlags : Type

Persistent visitor flags. withMaybeDangling scopes the source's may_dangle |= is_like_maybe_dangling() update and restores the old value on successful return. Errors unwind the visitor just as the source macro does.

• resetProvenanceAndPadding : Bool
• mayDangle : Bool

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqVisitorFlags : DecidableEq VisitorFlags

Equations

• Miri.Memory.Validity.instDecidableEqVisitorFlags = Miri.Memory.Validity.instDecidableEqVisitorFlags.decEq

def Miri.Memory.Validity.instDecidableEqVisitorFlags.decEq (x✝ x✝¹ : VisitorFlags) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.Validity.instReprVisitorFlags.repr : VisitorFlags → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprVisitorFlags : Repr VisitorFlags

Equations

• Miri.Memory.Validity.instReprVisitorFlags = { reprPrec := Miri.Memory.Validity.instReprVisitorFlags.repr }

def Miri.Memory.Validity.withMaybeDangling {Error HookState α : Type} (flags : VisitorFlags) (isLikeMaybeDangling : Bool) (visit : VisitorFlags → EStateM Error HookState α) : EStateM Error HookState (α × VisitorFlags)

Equations

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

structure Miri.Memory.Validity.PrimitiveHooks (Prov MachineError HookState : Type) : Type

Mutation and machine-resolution boundary used by ValidityVisitor::try_visit_primitive.

• clearProvenance : HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• resetPointerProvenance : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• addDataRange : HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• checkRawPointerMetadata : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• checkFunctionPointer : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Unit

structure Miri.Memory.Validity.SafePointerTarget (Prov Key : Type) : Type

Facts returned by the machine's imm_ptr_to_mplace boundary. Dynamic size/alignment and pointer access remain separate callbacks so their ordering matches the pinned visitor.

• original : Scalar Prov
• pointer : Scalar Prov
• metadataKind : MetadataKind
• layoutSize : ABI.Size
• layoutAlign : ABI.Align
• absoluteAddress : Option UInt64
• key : Key

structure Miri.Memory.Validity.RefTracking (Key Path : Type) : Type

A small, explicit recursive-reference worklist matching rustc's RefTracking: seen persists after an item is popped, and todo is LIFO.

• seen : Array Key
• todo : Array (Key × Path)

@[instance_reducible]

instance Miri.Memory.Validity.instReprRefTracking {Key✝ Path✝ : Type} [Repr Key✝] [Repr Path✝] : Repr (RefTracking Key✝ Path✝)

Equations

• Miri.Memory.Validity.instReprRefTracking = { reprPrec := Miri.Memory.Validity.instReprRefTracking.repr }

def Miri.Memory.Validity.instReprRefTracking.repr {Key✝ Path✝ : Type} [Repr Key✝] [Repr Path✝] : RefTracking Key✝ Path✝ → Nat → Std.Format

Equations

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

def Miri.Memory.Validity.RefTracking.empty {Key Path : Type} : RefTracking Key Path

Equations

• Miri.Memory.Validity.RefTracking.empty = { }

def Miri.Memory.Validity.RefTracking.start {Key Path : Type} (key : Key) (path : Path) : RefTracking Key Path

Equations

• Miri.Memory.Validity.RefTracking.start key path = { seen := #[key], todo := #[(key, path)] }

def Miri.Memory.Validity.RefTracking.next {Key Path : Type} (tracking : RefTracking Key Path) : Option ((Key × Path) × RefTracking Key Path)

Equations

• tracking.next = do let item ← tracking.todo.back? pure (item, { seen := tracking.seen, todo := tracking.todo.pop })

def Miri.Memory.Validity.RefTracking.track {Key Path : Type} (tracking : RefTracking Key Path) (key : Key) (makePath : Unit → Path) [DecidableEq Key] : RefTracking Key Path

Duplicate references are ignored; makePath is only evaluated on the first visit, matching the source's lazy path construction.

Equations

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

inductive Miri.Memory.Validity.ValueWalkFields : Type

• primitive : ValueWalkFields
• union (fieldCount : Nat) : ValueWalkFields
• arbitrary (inMemoryOrder fields : Array Nat) : ValueWalkFields
• array (elements : Array Nat) : ValueWalkFields

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqValueWalkFields : DecidableEq ValueWalkFields

Equations

• Miri.Memory.Validity.instDecidableEqValueWalkFields = Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq

def Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (x✝ x✝¹ : ValueWalkFields) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq Miri.Memory.Validity.ValueWalkFields.primitive Miri.Memory.Validity.ValueWalkFields.primitive = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq Miri.Memory.Validity.ValueWalkFields.primitive (Miri.Memory.Validity.ValueWalkFields.union fieldCount) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq Miri.Memory.Validity.ValueWalkFields.primitive (Miri.Memory.Validity.ValueWalkFields.arbitrary inMemoryOrder fields) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq Miri.Memory.Validity.ValueWalkFields.primitive (Miri.Memory.Validity.ValueWalkFields.array elements) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.union fieldCount) Miri.Memory.Validity.ValueWalkFields.primitive = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.union fieldCount) (Miri.Memory.Validity.ValueWalkFields.array elements) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.arbitrary inMemoryOrder fields) Miri.Memory.Validity.ValueWalkFields.primitive = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.array elements) Miri.Memory.Validity.ValueWalkFields.primitive = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.array elements) (Miri.Memory.Validity.ValueWalkFields.union fieldCount) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkFields.decEq (Miri.Memory.Validity.ValueWalkFields.array elements) (Miri.Memory.Validity.ValueWalkFields.arbitrary inMemoryOrder fields) = isFalse ⋯

def Miri.Memory.Validity.instReprValueWalkFields.repr : ValueWalkFields → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprValueWalkFields : Repr ValueWalkFields

Equations

• Miri.Memory.Validity.instReprValueWalkFields = { reprPrec := Miri.Memory.Validity.instReprValueWalkFields.repr }

inductive Miri.Memory.Validity.ValueWalkVariants : Type

• single : ValueWalkVariants
• empty : ValueWalkVariants
• multiple (variants : Array Nat) : ValueWalkVariants

def Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq (x✝ x✝¹ : ValueWalkVariants) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq Miri.Memory.Validity.ValueWalkVariants.single Miri.Memory.Validity.ValueWalkVariants.single = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq Miri.Memory.Validity.ValueWalkVariants.single (Miri.Memory.Validity.ValueWalkVariants.multiple variants) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq Miri.Memory.Validity.ValueWalkVariants.empty Miri.Memory.Validity.ValueWalkVariants.empty = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq Miri.Memory.Validity.ValueWalkVariants.empty (Miri.Memory.Validity.ValueWalkVariants.multiple variants) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq (Miri.Memory.Validity.ValueWalkVariants.multiple variants) Miri.Memory.Validity.ValueWalkVariants.single = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq (Miri.Memory.Validity.ValueWalkVariants.multiple variants) Miri.Memory.Validity.ValueWalkVariants.empty = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqValueWalkVariants : DecidableEq ValueWalkVariants

Equations

• Miri.Memory.Validity.instDecidableEqValueWalkVariants = Miri.Memory.Validity.instDecidableEqValueWalkVariants.decEq

@[instance_reducible]

instance Miri.Memory.Validity.instReprValueWalkVariants : Repr ValueWalkVariants

Equations

• Miri.Memory.Validity.instReprValueWalkVariants = { reprPrec := Miri.Memory.Validity.instReprValueWalkVariants.repr }

def Miri.Memory.Validity.instReprValueWalkVariants.repr : ValueWalkVariants → Nat → Std.Format

Equations

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

inductive Miri.Memory.Validity.ValueWalkSpecial : Type

• none : ValueWalkSpecial
• dynamic (inner : Nat) : ValueWalkSpecial
• box (pointer allocator : Nat) : ValueWalkSpecial

def Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq (x✝ x✝¹ : ValueWalkSpecial) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq Miri.Memory.Validity.ValueWalkSpecial.none Miri.Memory.Validity.ValueWalkSpecial.none = isTrue ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq Miri.Memory.Validity.ValueWalkSpecial.none (Miri.Memory.Validity.ValueWalkSpecial.dynamic inner) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq Miri.Memory.Validity.ValueWalkSpecial.none (Miri.Memory.Validity.ValueWalkSpecial.box pointer allocator) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq (Miri.Memory.Validity.ValueWalkSpecial.dynamic inner) Miri.Memory.Validity.ValueWalkSpecial.none = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq (Miri.Memory.Validity.ValueWalkSpecial.dynamic inner) (Miri.Memory.Validity.ValueWalkSpecial.box pointer allocator) = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq (Miri.Memory.Validity.ValueWalkSpecial.box pointer allocator) Miri.Memory.Validity.ValueWalkSpecial.none = isFalse ⋯
• Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq (Miri.Memory.Validity.ValueWalkSpecial.box pointer allocator) (Miri.Memory.Validity.ValueWalkSpecial.dynamic inner) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqValueWalkSpecial : DecidableEq ValueWalkSpecial

Equations

• Miri.Memory.Validity.instDecidableEqValueWalkSpecial = Miri.Memory.Validity.instDecidableEqValueWalkSpecial.decEq

def Miri.Memory.Validity.instReprValueWalkSpecial.repr : ValueWalkSpecial → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprValueWalkSpecial : Repr ValueWalkSpecial

Equations

• Miri.Memory.Validity.instReprValueWalkSpecial = { reprPrec := Miri.Memory.Validity.instReprValueWalkSpecial.repr }

structure Miri.Memory.Validity.ValueWalkNode : Type

Resolved projection facts for the generic ValueVisitor::walk_value engine. The machine/layout adapter supplies child handles in source projection order; each index and field/variant lookup is validated before traversal.

• typeName : String
• pathInfo : AggregatePathInfo
• fields : ValueWalkFields
• variants : ValueWalkVariants
• special : ValueWalkSpecial
• fieldNames : Array (Option String)
• capturedNames : Array (Option String)
• variantNames : Array (Option String)
• isLikeMaybeDangling : Bool

def Miri.Memory.Validity.instDecidableEqValueWalkNode.decEq (x✝ x✝¹ : ValueWalkNode) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqValueWalkNode : DecidableEq ValueWalkNode

Equations

• Miri.Memory.Validity.instDecidableEqValueWalkNode = Miri.Memory.Validity.instDecidableEqValueWalkNode.decEq

def Miri.Memory.Validity.instReprValueWalkNode.repr : ValueWalkNode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instReprValueWalkNode : Repr ValueWalkNode

Equations

• Miri.Memory.Validity.instReprValueWalkNode = { reprPrec := Miri.Memory.Validity.instReprValueWalkNode.repr }

structure Miri.Memory.Validity.ValueWalkGraph : Type

• root : Nat
• nodes : Array ValueWalkNode

def Miri.Memory.Validity.instDecidableEqValueWalkGraph.decEq (x✝ x✝¹ : ValueWalkGraph) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.Validity.instDecidableEqValueWalkGraph : DecidableEq ValueWalkGraph

Equations

• Miri.Memory.Validity.instDecidableEqValueWalkGraph = Miri.Memory.Validity.instDecidableEqValueWalkGraph.decEq

@[instance_reducible]

instance Miri.Memory.Validity.instReprValueWalkGraph : Repr ValueWalkGraph

Equations

• Miri.Memory.Validity.instReprValueWalkGraph = { reprPrec := Miri.Memory.Validity.instReprValueWalkGraph.repr }

def Miri.Memory.Validity.instReprValueWalkGraph.repr : ValueWalkGraph → Nat → Std.Format

Equations

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

structure Miri.Memory.Validity.ValueWalkHooks (MachineError HookState : Type) : Type

• tryVisitPrimitive : Nat → ValidationPath → VisitorFlags → HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• checkUnsafeCell : Nat → ValidationPath → VisitorFlags → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• tryVisitSpecialCase : Nat → ValidationPath → VisitorFlags → HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• visitUnion : Nat → Nat → ValidationPath → VisitorFlags → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• visitBox : Nat → Nat → ValidationPath → VisitorFlags → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• readDiscriminant : Nat → HookState → EStateM.Result (ValidityError MachineError) HookState Nat
• visitVariantless : Nat → ValidationPath → HookState → EStateM.Result (ValidityError MachineError) HookState Unit

def Miri.Memory.Validity.walkValue {MachineError HookState : Type} (hooks : ValueWalkHooks MachineError HookState) (graph : ValueWalkGraph) (rootPath : ValidationPath) (flags : VisitorFlags) : EStateM (ValidityError MachineError) HookState Unit

Source ValueVisitor::walk_value traversal order, composed with the validity-specific primitive, UnsafeCell, optimized-case, union, and Box hooks. The finite graph contains layout projections supplied by the interpreter; missing projection or machine operations remain explicit failures.

Equations

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

structure Miri.Memory.Validity.ValidationSession (Key : Type) : Type

Per-invocation state passed through the source visit_value traversal. The path is a value so child scopes can push a projection and restore it on return; data tracking and recursive-reference discovery are returned by the visitor rather than hidden in a default-success operation.

• path : ValidationPath
• flags : VisitorFlags
• ctfeMode : Option CtfeMode
• refTracking : Option (RefTracking Key ValidationPath)
• dataBytes : Option DataRangeSet

structure Miri.Memory.Validity.ValidatePlaceHooks (Place Key MachineError HookState : Type) : Type

• isStoredInMemory : Place → HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• visitValue : Place → ValidationSession Key → HookState → EStateM.Result (ValidityError MachineError) HookState (ValidationSession Key)
• allocationRange : Place → HookState → EStateM.Result (ValidityError MachineError) HookState (Option (ABI.Size × ABI.Size))
• writeUninit : Place → AllocRange → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• trackedPlace : Key → HookState → EStateM.Result (ValidityError MachineError) HookState Place

def Miri.Memory.Validity.validatePlace {Place Key MachineError HookState : Type} [DecidableEq Key] (hooks : ValidatePlaceHooks Place Key MachineError HookState) (root : Place) (originalType : String) (resetProvenanceAndPadding : Bool) (ctfeMode : Option CtfeMode) (initialTracking : Option (RefTracking Key ValidationPath)) (drainTracking : Bool) : EStateM (ValidityError MachineError) HookState Unit

The pinned validate_place_internal orchestration. The actual MIR place projection and recursive type walk are an explicit callback because they depend on rustc's PlaceTy/layout engine; this driver preserves the source setup, mutation order, padding finalizer, and recursive RefTracking drain. Each tracked pointee is visited without provenance reset, with no further tracking, and under may_dangle, as in validate_place.

Equations

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

structure Miri.Memory.Validity.SafePointerHooks (Prov Key MachineError HookState : Type) : Type

Required operations for the source check_safe_pointer path. Each callback stands at a real machine/layout boundary; absent semantics cannot be silently interpreted as success. Callbacks return a ValidityError when the source maps an underlying UB category to a validation failure.

• readImmediate : HookState → EStateM.Result (ValidityError MachineError) HookState (Scalar Prov)
• resolvePlace : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState (SafePointerTarget Prov Key)
• checkWideMetadata : SafePointerTarget Prov Key → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• sizeAndAlign : SafePointerTarget Prov Key → HookState → EStateM.Result (ValidityError MachineError) HookState (Option (ABI.Size × ABI.Align))
• checkAccess : Scalar Prov → ABI.Size → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• retagPointer : Scalar Prov → SafePointerKind → HookState → EStateM.Result (ValidityError MachineError) HookState (Option (Scalar Prov))
• writeAdjustedPointer : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• resetPointerProvenance : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• markPointerData : HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• scalarMayBeNull : Scalar Prov → HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• checkInhabited : SafePointerTarget Prov Key → HookState → EStateM.Result (ValidityError MachineError) HookState Bool
• checkAlignment : Scalar Prov → ABI.Align → HookState → EStateM.Result (ValidityError MachineError) HookState Unit
• ctfePointerAllocLookup : SafePointerTarget Prov Key → CtfeMode → HookState → EStateM.Result (ValidityError MachineError) HookState PointerAllocLookup

def Miri.Memory.Validity.checkSafePointer {Prov MachineError HookState Key Path : Type} [PointerProvenance Prov] [DecidableEq Key] (hooks : SafePointerHooks Prov Key MachineError HookState) (kind : SafePointerKind) (resetProvenanceAndPadding mayDangle : Bool) (ctfeMode : Option CtfeMode) (targetUsizeMax : UInt64) (tracking : Option (RefTracking Key Path × Path)) (makeDerefPath : Path → Path) (invalidMetadataTail : String → ValidityError MachineError) : EStateM (ValidityError MachineError) HookState (Option (RefTracking Key Path))

Run source-ordered safe-reference/Box validation. The optional tracker, CTFE policy, and reset/may-dangle flags are explicit visitor state. A source machine error or validation failure preserves callback state at the exact failing step. targetUsizeMax is the machine target's maximum address.

Equations

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

def Miri.Memory.Validity.formatRange (range : ABI.WrappingRange) (maxHi : ABI.U128) : Except String String

Port of validity.rs::fmt_range, retaining its invariant failures as explicit errors instead of Lean/Rust panics.

Equations

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

def Miri.Memory.Validity.formatFailure (failure : ValidityFailure) : Except String String

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.formatFailure (Miri.Memory.ValidityFailure.uninitialized a a_1) = pure (toString "encountered uninitialized memory, but " ++ toString (reprStr a))
• Miri.Memory.Validity.formatFailure (Miri.Memory.ValidityFailure.pointerAsInt a a_1) = pure (toString "encountered a pointer, but " ++ toString (reprStr a))
• Miri.Memory.Validity.formatFailure (Miri.Memory.ValidityFailure.partialPointer a) = pure "encountered a partial pointer or a mix of pointers"
• Miri.Memory.Validity.formatFailure (Miri.Memory.ValidityFailure.invalidBool a) = pure (toString "invalid boolean byte " ++ toString a.toNat)
• Miri.Memory.Validity.formatFailure (Miri.Memory.ValidityFailure.invalidChar a) = pure (toString "encountered " ++ toString a.toNat ++ toString ", but expected a valid Unicode scalar value")
• Miri.Memory.Validity.formatFailure Miri.Memory.ValidityFailure.maybeNullPointer = pure "encountered a maybe-null pointer, but expected something that is definitely non-zero"
• Miri.Memory.Validity.formatFailure Miri.Memory.ValidityFailure.unsafeCellInReadOnlyMemory = pure "encountered `UnsafeCell` in read-only memory"
• Miri.Memory.Validity.formatFailure Miri.Memory.ValidityFailure.neverValue = pure "encountered a value of the never type `!`"

def Miri.Memory.Validity.classifyReadError (expected : ExpectedValue) (error : AllocError) : Option ValidityFailure

Equations

• Miri.Memory.Validity.classifyReadError expected (Miri.Memory.AllocError.invalidUninitBytes info) = some (Miri.Memory.ValidityFailure.uninitialized expected info)
• Miri.Memory.Validity.classifyReadError expected (Miri.Memory.AllocError.readPointerAsInt info) = some (Miri.Memory.ValidityFailure.pointerAsInt expected info)
• Miri.Memory.Validity.classifyReadError expected (Miri.Memory.AllocError.readPartialPointer offset) = some (Miri.Memory.ValidityFailure.partialPointer offset)
• Miri.Memory.Validity.classifyReadError expected error = none

def Miri.Memory.Validity.checkScalar {Prov : Type} [PointerProvenance Prov] {MachineError HookState : Type} (layout : ScalarValidityLayout) (scalar : Scalar Prov) (scalarMayBeNull : Scalar Prov → HookState → EStateM.Result MachineError HookState Bool) : EStateM (ValidityError MachineError) HookState Unit

Source ValidityVisitor::visit_scalar, with scalar_may_be_null as a required machine callback. Callback errors pass through unchanged, while the result state is retained on callback failure.

Equations

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

def Miri.Memory.Validity.checkPrimitive {Prov : Type} [PointerProvenance Prov] {MachineError HookState : Type} (kind : PrimitiveKind) (_layout : ScalarValidityLayout) (scalar : Scalar Prov) (_scalarMayBeNull : Scalar Prov → HookState → EStateM.Result MachineError HookState Bool) : EStateM (ValidityError MachineError) HookState PrimitiveStep

Source primitive classification after the memory read. The integer/float case only requires initialized scalar bytes here; valid-range checking is the separate visitScalar operation used by the higher-level visitor when needed. Pointer-specific operations remain explicit delegation steps.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.scalar _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.valid state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.foreign _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.valid state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.functionDefinition _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.valid state)).run
• Miri.Memory.Validity.checkPrimitive (Miri.Memory.PrimitiveKind.rawPointer true) _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.valid state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.safeReference _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.safePointer state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.box _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.boxPointer state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.functionPointer _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.functionPointer state)).run
• Miri.Memory.Validity.checkPrimitive Miri.Memory.PrimitiveKind.aggregate _layout scalar _scalarMayBeNull state = (pure (EStateM.Result.ok Miri.Memory.PrimitiveStep.recurse state)).run

def Miri.Memory.Validity.visitPrimitive {Prov : Type} [PointerProvenance Prov] {MachineError HookState : Type} (hooks : PrimitiveHooks Prov MachineError HookState) (kind : PrimitiveKind) (layout : ScalarValidityLayout) (scalar : Scalar Prov) (resetProvenanceAndPadding recursiveTracking : Bool) (scalarMayBeNull : Scalar Prov → HookState → EStateM.Result MachineError HookState Bool) : EStateM (ValidityError MachineError) HookState PrimitiveStep

Execute the stateful portion of try_visit_primitive. The caller has already read the scalar/immediate at the expected type. This preserves the source order for pointer reset, data-byte tracking, wide-pointer metadata, and function-pointer validation. Safe references and Box delegate to checkSafePointer through distinct explicit steps.

Equations

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

theorem Miri.Memory.Validity.zero_is_outside_byte_nonzero_niche : { start := 1#128, «end» := 255#128 }.contains 0 = false

The standard one-byte nonzero niche excludes the null representation.

theorem Miri.Memory.Validity.byte_nonzero_niche_accepts (value : UInt8) (h : (value.toNat != 0) = true) : { start := 1#128, «end» := 255#128 }.contains (BitVec.ofNat 128 value.toNat) = true

Any one-byte value from 1 through 255 satisfies the nonzero niche.