Canonical typed runtime visitor from pinned validity.rs and visitor.rs. Traversal consumes actual RuntimePlace/TyAndLayout, not a pre-resolved value graph. Compiler facts and machine accesses remain required effectful leaves.

inductive Miri.Interpreter.ValidityVisitor.TypeKind : Type

• boolean : TypeKind
• character : TypeKind
• integer : TypeKind
• float : TypeKind
• functionPointer : TypeKind
• never : TypeKind
• foreign : TypeKind
• functionDefinition : TypeKind
• rawPointer (pointee : MIR.TyId) (pointeeSized : Bool) : TypeKind
• reference (mutable : Bool) : TypeKind
• string : TypeKind
• sequence (element : MIR.TyId) : TypeKind
• dynamic (expectedTrait : Nat) : TypeKind
• box : TypeKind
• pattern (base : MIR.TyId) : TypeKind
• aggregate (maybeDangling unsafeCell isEnum : Bool) : TypeKind
• unsafeBinder : TypeKind
• invalid : TypeKind

def Miri.Interpreter.ValidityVisitor.instDecidableEqTypeKind.decEq (x✝ x✝¹ : TypeKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instDecidableEqTypeKind : DecidableEq TypeKind

Equations

• Miri.Interpreter.ValidityVisitor.instDecidableEqTypeKind = Miri.Interpreter.ValidityVisitor.instDecidableEqTypeKind.decEq

def Miri.Interpreter.ValidityVisitor.instReprTypeKind.repr : TypeKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instReprTypeKind : Repr TypeKind

Equations

• Miri.Interpreter.ValidityVisitor.instReprTypeKind = { reprPrec := Miri.Interpreter.ValidityVisitor.instReprTypeKind.repr }

inductive Miri.Interpreter.ValidityVisitor.MetadataTail : Type

• dynamic (expectedTrait : Nat) : MetadataTail
• sliceOrStr : MetadataTail
• foreign : MetadataTail

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail : DecidableEq MetadataTail

Equations

• Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail = Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail.decEq

def Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail.decEq (x✝ x✝¹ : MetadataTail) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail.decEq Miri.Interpreter.ValidityVisitor.MetadataTail.sliceOrStr Miri.Interpreter.ValidityVisitor.MetadataTail.sliceOrStr = isTrue ⋯
• Miri.Interpreter.ValidityVisitor.instDecidableEqMetadataTail.decEq Miri.Interpreter.ValidityVisitor.MetadataTail.foreign Miri.Interpreter.ValidityVisitor.MetadataTail.foreign = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instReprMetadataTail : Repr MetadataTail

Equations

• Miri.Interpreter.ValidityVisitor.instReprMetadataTail = { reprPrec := Miri.Interpreter.ValidityVisitor.instReprMetadataTail.repr }

def Miri.Interpreter.ValidityVisitor.instReprMetadataTail.repr : MetadataTail → Nat → Std.Format

Equations

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

structure Miri.Interpreter.ValidityVisitor.Key (P : Type) : Type

• mplace : MemPlace P
• layout : LocalLayout

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instDecidableEqKey {P✝ : Type} [DecidableEq P✝] : DecidableEq (Key P✝)

Equations

• Miri.Interpreter.ValidityVisitor.instDecidableEqKey = Miri.Interpreter.ValidityVisitor.instDecidableEqKey.decEq

@[instance_reducible]

instance Miri.Interpreter.ValidityVisitor.instReprKey {P✝ : Type} [Repr P✝] : Repr (Key P✝)

Equations

• Miri.Interpreter.ValidityVisitor.instReprKey = { reprPrec := Miri.Interpreter.ValidityVisitor.instReprKey.repr }

def Miri.Interpreter.ValidityVisitor.instReprKey.repr {P✝ : Type} [Repr P✝] : Key P✝ → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.ValidityVisitor.Session (P : Type) : Type

Equations

• Miri.Interpreter.ValidityVisitor.Session P = Miri.Memory.Validity.ValidationSession (Miri.Interpreter.ValidityVisitor.Key P)

@[reducible, inline]

abbrev Miri.Interpreter.ValidityVisitor.M (S A : Type) : Type

Equations

• Miri.Interpreter.ValidityVisitor.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Interpreter.ValidityVisitor.Hooks (P S C E Fn ABI Padding : Type) : Type 1

Memory operations here run under withGhostValidation, including provenance writes. Retagging is the source exception: its actual machine reborrow effects must still execute. readBytes strips provenance and checks initialization; it must not validate UTF-8 (source str validity only checks bytes). beginPadding obtains mutable allocation access once, followed by writePadding per gap.

• target : Miri.ABI.RuntimeTargetDataLayout
• projection : PlaceProjectionHooks P S C E
• vtable : VTableHooks P S C Fn ABI
• discriminant : DiscriminantHooks P S C (RuntimePlace P)
• debugAssertions : Bool
• classify : C → MIR.TyId → M S TypeKind
• unitLayout : C → M S LocalLayout
• typeName : C → MIR.TyId → M S String
• opsemInhabited : C → MIR.TyId → M S Bool
• isFreeze : C → MIR.TyId → M S Bool
• fieldPath : C → LocalLayout → Nat → MIR.TyId → M S Memory.PathElem
• variantPath : C → LocalLayout → Nat → M S Memory.PathElem
• projectBox : C → RuntimePlace P → M S (RuntimePlace P × RuntimePlace P)
• toOp : C → RuntimePlace P → M S (OpTy P)
• readImmediate : C → RuntimePlace P → Memory.ExpectedValue → M S (RvalueImmTy P)
• clearProvenance : C → RuntimePlace P → M S Unit
• writeNoValidate : C → Immediate P → RuntimePlace P → M S Unit
• sizeAndAlign : C → MPlaceTy P → M S (Option (Miri.ABI.Size × Miri.ABI.Align))
• ptrToPlace : C → RvalueImmTy P → M S (MPlaceTy P)
• metadataTail : C → MIR.TyId → M S MetadataTail
• checkPointerAccess : C → Memory.Pointer (Option P) → Miri.ABI.Size → M S (Except Memory.AccessError Unit)
• checkPointerAlign : C → Memory.Pointer (Option P) → Miri.ABI.Align → M S Unit
• checkPointerAlignResult : C → Memory.Pointer (Option P) → Miri.ABI.Align → M S (Except Memory.Misalignment Unit)

  Typed result for validity's source-specific AlignmentCheckFailed mapping. Other consumers keep the ordinary machine alignment error behavior.

• scalarMayBeNull : C → Memory.Scalar P → M S Bool
• retagPointer : C → RvalueImmTy P → MIR.TyId → M S (Option (RvalueImmTy P))
• ctfePointerLookup : C → MPlaceTy P → Memory.Validity.CtfeMode → M S Memory.Validity.PointerAllocLookup
• inMutableMemory : C → RuntimePlace P → M S Bool
• readBytes : C → MPlaceTy P → Miri.ABI.Size → Memory.ExpectedValue → M S Unit
• clearBytesProvenance : C → MPlaceTy P → Miri.ABI.Size → M S Unit
• beginPadding : C → MPlaceTy P → Miri.ABI.Size → M S (Option Padding)
• writePadding : C → Padding → Memory.AllocRange → M S Unit
• cachedUnionRanges : C → LocalLayout → M S Memory.Validity.DataRangeSet → M S Memory.Validity.DataRangeSet
• withGhostValidation {A : Type} : M S A → M S A

def Miri.Interpreter.ValidityVisitor.classifyRetagError (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (error : StepError) : StepError

validity.rs::check_safe_pointer gives retag failures two pieces of source-specific treatment. A mutable reborrow of immutable memory is reported as a validity failure at the current path, while an aliasing-model machine stop carries the path as diagnostic context. This runner keeps the callback's successor state in either case, including when it fails after changing the borrow tree.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ValidityVisitor.classifyRetagError path kind error = error

def Miri.Interpreter.ValidityVisitor.classifyPointerAlignmentError (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (misalignment : Memory.Misalignment) : StepError

Equations

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

def Miri.Interpreter.ValidityVisitor.mapPointerAlignmentOutcome {S : Type} (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (check : M S (Except Memory.Misalignment Unit)) : M S Unit

Keep the source check_ptr_align successor state when turning its one source-remapped failure into a validation UB. Other machine failures retain their original classification and successor state.

Equations

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

def Miri.Interpreter.ValidityVisitor.classifyPointerAccessError (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (error : Memory.AccessError) : StepError

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ValidityVisitor.classifyPointerAccessError path kind error = Miri.Interpreter.MemoryErrors.access error

def Miri.Interpreter.ValidityVisitor.mapRetagOutcome {S A : Type} (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (retag : M S A) : M S A

Equations

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

def Miri.Interpreter.ValidityVisitor.retagSafePointer {C : Sort u_1} {P S : Type} (path : Memory.ValidationPath) (kind : Memory.SafePointerKind) (retag : C → RvalueImmTy P → MIR.TyId → M S (Option (RvalueImmTy P))) (c : C) (pointer : RvalueImmTy P) (ty : MIR.TyId) : M S (Option (RvalueImmTy P))

Equations

• Miri.Interpreter.ValidityVisitor.retagSafePointer path kind retag c pointer ty = Miri.Interpreter.ValidityVisitor.mapRetagOutcome path kind (retag c pointer ty)

def Miri.Interpreter.ValidityVisitor.unionRanges {P S C E F A Pad : Type} (h : Hooks P S C E F A Pad) (c : C) : Nat → LocalLayout → ABI.Size → Memory.Validity.DataRangeSet → M S Memory.Validity.DataRangeSet

Data-byte union layout walk. It traverses compiler layouts, never reads an active union field, and preserves the source scalar-array fast path.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ValidityVisitor.unionRanges h c 0 x✝² x✝¹ x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "union layout traversal fuel")

def Miri.Interpreter.ValidityVisitor.visit {P S C E F A Pad : Type} [Memory.PointerProvenance P] [DecidableEq P] (h : Hooks P S C E F A Pad) (c : C) : Nat → Session P → RuntimePlace P → M S (Session P)

Recursive ValueVisitor plus validity-specific primitive/array/union rules. Fuel exhaustion is visible resource failure; it never validates an unexplored subvalue. Fields follow in-memory order; enum tag precedes active variant.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ValidityVisitor.visit h c 0 x✝¹ x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "validity traversal fuel")

theorem Miri.Interpreter.ValidityVisitor.visit_fieldless {P S C E F A Pad : Type} [Memory.PointerProvenance P] [DecidableEq P] (h : Hooks P S C E F A Pad) (c : C) (fuel : Nat) (session : Session P) (place : RuntimePlace P) (state : S) (variant : Nat) (classify : h.classify c place.layout.ty state = EStateM.Result.ok (TypeKind.aggregate false false false) state) (inhabited : h.opsemInhabited c place.layout.ty state = EStateM.Result.ok true state) (fields : place.layout.layout.fields = ABI.FieldsShape.Arbitrary #[] #[]) (variants : place.layout.layout.variants = ABI.Variants.Single variant) (runtime : session.ctfeMode = none) (debugOff : h.debugAssertions = false) : visit h c (fuel + 1) session place state = EStateM.Result.ok session state

A fieldless inhabited aggregate has no value bytes or child accesses. The premises expose compiler queries at this state, rather than assuming a validation-operation outcome.

@[simp]

theorem Miri.Interpreter.ValidityVisitor.resetPadding_no_ranges {P S C E F A Pad : Type} (h : Hooks P S C E F A Pad) (c : C) (session : Session P) (place : RuntimePlace P) (empty : session.dataBytes = none) : Miri.Interpreter.ValidityVisitor.resetPadding✝ h c session place = pure ()

No padding allocation is needed for a local-only validation session.

theorem Miri.Interpreter.ValidityVisitor.resetPadding_memory_zero {P S C E F A Pad : Type} [Memory.PointerProvenance P] (h : Hooks P S C E F A Pad) (c : C) (session : Session P) (place : MPlaceTy P) (state : S) (ranges : session.dataBytes = some Memory.Validity.DataRangeSet.empty) (size : place.layout.layout.size = ABI.Size.ZERO) (dynamic : h.sizeAndAlign c place state = EStateM.Result.ok (some (ABI.Size.ZERO, place.layout.layout.align.abi)) state) (padding : h.beginPadding c place ABI.Size.ZERO state = EStateM.Result.ok none state) : Miri.Interpreter.ValidityVisitor.resetPadding✝ h c session { ref := RuntimePlaceRef.memory place.mplace, layout := place.layout } state = EStateM.Result.ok () state

Unit memory validation has no padding bytes. Its zero-size mutable-access query produces no handle, so reset performs no writes or allocation.

def Miri.Interpreter.ValidityVisitor.validatePlace {P S C E F A Pad : Type} [Memory.PointerProvenance P] [DecidableEq P] (h : Hooks P S C E F A Pad) (c : C) (fuel : Nat) (place : RuntimePlace P) (recursive reset : Bool) : M S Unit

Runtime validation: root may retag/reset; tracked pointees are checked in LIFO order without reset, without further tracking, and under may_dangle.

Equations

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

def Miri.Interpreter.ValidityVisitor.constValidatePlace {P S C E F A Pad : Type} [Memory.PointerProvenance P] [DecidableEq P] (h : Hooks P S C E F A Pad) (c : C) (fuel : Nat) (place : RuntimePlace P) (path : Memory.ValidationPath) (tracking : Memory.Validity.RefTracking (Key P) Memory.ValidationPath) (mode : Memory.Validity.CtfeMode) : M S (Memory.Validity.RefTracking (Key P) Memory.ValidationPath)

Const validation exposes the updated worklist to its outer interning loop; CTFE restrictions are distinct from ordinary recursive runtime checks.

Equations

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

theorem Miri.Interpreter.ValidityVisitor.resetPadding_forced_zero {P S C E F A Pad : Type} [Memory.PointerProvenance P] (h : Hooks P S C E F A Pad) (c : C) (session : Session P) (original : RuntimePlace P) (place : MPlaceTy P) (state : S) (ranges : session.dataBytes = some Memory.Validity.DataRangeSet.empty) (forced : forceAllocation h.projection.place c original state = EStateM.Result.ok place state) (size : place.layout.layout.size = ABI.Size.ZERO) (dynamic : h.sizeAndAlign c place state = EStateM.Result.ok (some (ABI.Size.ZERO, place.layout.layout.align.abi)) state) (padding : h.beginPadding c place ABI.Size.ZERO state = EStateM.Result.ok none state) : Miri.Interpreter.ValidityVisitor.resetPadding✝ h c session original state = EStateM.Result.ok () state

Internal zero-padding composition after the original local place has been proved to denote its existing backing.