Concrete validity byte/provenance/padding operations. Allocation access is explicitly ghost, as validate_place_internal requires; retagging remains a separate actual machine effect in ValidityVisitor. All memory, hook-state and touched-extra effects are committed before propagating failures.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.ValidityMemory.Environment (P Extra Kind H ProvExtra S : Type) : Type

• context : LocalReadContext P Extra Kind H ProvExtra
• memory : S → Memory.MemoryState P Extra Kind
• hooks : S → H
• putMemoryHooks : S → Memory.MemoryState P Extra Kind → H → S
• putTouched : S → Option (Memory.AllocationAccessRef P Extra) → S
• memoryError : H → MemoryOperandError → StepError
• pointerError : H → Memory.PtrAllocationError → StepError
• allocationError : Memory.AllocError → StepError

def Miri.Interpreter.ValidityMemory.readImmediate {K P E H X S : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (env : Environment P E K H X S) (operand : OpTy P) (expected : Memory.ExpectedValue) : M S (RvalueImmTy P)

Actual primitive scalar/scalar-pair decoding, retaining full type identity. Known initialization/provenance failures are mapped to validity categories.

Equations

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

def Miri.Interpreter.ValidityMemory.readBytes {K P E H X S : Type} [DecidableEq K] [Memory.PointerProvenance P] (env : Environment P E K H X S) (place : MPlaceTy P) (size : ABI.Size) (expected : Memory.ExpectedValue) : M S Unit

Numeric arrays and str validate initialized bytes while stripping pointer provenance according to the actual provenance representation. No extra alignment check is introduced: source uses get_ptr_alloc, not place access.

Equations

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

structure Miri.Interpreter.ValidityMemory.PaddingHandle : Type

A padding handle names the one mutable allocation reference obtained by reset_padding. Later gap writes re-read its current allocation, preserving all earlier gap writes and partial mutations on error.

• allocId : Memory.AllocId
• range : Memory.AllocRange

@[instance_reducible]

instance Miri.Interpreter.ValidityMemory.instDecidableEqPaddingHandle : DecidableEq PaddingHandle

Equations

• Miri.Interpreter.ValidityMemory.instDecidableEqPaddingHandle = Miri.Interpreter.ValidityMemory.instDecidableEqPaddingHandle.decEq

def Miri.Interpreter.ValidityMemory.instDecidableEqPaddingHandle.decEq (x✝ x✝¹ : PaddingHandle) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityMemory.instReprPaddingHandle : Repr PaddingHandle

Equations

• Miri.Interpreter.ValidityMemory.instReprPaddingHandle = { reprPrec := Miri.Interpreter.ValidityMemory.instReprPaddingHandle.repr }

def Miri.Interpreter.ValidityMemory.instReprPaddingHandle.repr : PaddingHandle → Nat → Std.Format

Equations

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

def Miri.Interpreter.ValidityMemory.beginPadding {K P E H X S : Type} [DecidableEq K] (env : Environment P E K H X S) (place : MPlaceTy P) (size : ABI.Size) : M S (Option PaddingHandle)

Equations

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

theorem Miri.Interpreter.ValidityMemory.beginPadding_zero {K P E H X S : Type} [DecidableEq K] (env : Environment P E K H X S) (place : MPlaceTy P) (state : S) (identity : env.putTouched (env.putMemoryHooks state (env.memory state) (env.hooks state)) none = state) : beginPadding env place ABI.Size.ZERO state = EStateM.Result.ok none state

A zero-sized padding region obtains no allocation reference. The lens identity states that committing the unchanged view has no effect.

def Miri.Interpreter.ValidityMemory.writePadding {K P E H X S : Type} [DecidableEq K] (env : Environment P E K H X S) (handle : PaddingHandle) (relative : Memory.AllocRange) : M S Unit

Equations

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

def Miri.Interpreter.ValidityMemory.clearBytesProvenance {K P E H X S : Type} [DecidableEq K] (env : Environment P E K H X S) (place : MPlaceTy P) (size : ABI.Size) : M S Unit

Equations

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

def Miri.Interpreter.ValidityMemory.clearPlaceProvenance {K P E H X S C Extra : Type} [DecidableEq K] [Memory.PointerProvenance P] (env : Environment P E K H X S) (placeHooks : PlaceHooks P S C Extra) (choice : C) (validationInProgress : M S Bool) (afterLocalWrite : MIR.LocalId → Bool → M S Unit) (place : RuntimePlace P) : M S Unit

Source place.rs clear_provenance, including the no-provenance immediate fast path and partial ScalarPair conversion. Under validation the local write hook is suppressed; outside that scope its actual callback remains required.

Equations

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

def Miri.Interpreter.ValidityMemory.writeNoValidate {K P E H X S C Extra : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (env : Environment P E K H X S) (placeHooks : PlaceHooks P S C Extra) (choice : C) (willValidate : MemoryOperandLayout → Bool) (value : Immediate P) (place : RuntimePlace P) : M S Unit

Typed writes performed by provenance resetting explicitly use ghost allocation access; optimized-local handling remains source's mutable-local selection and scoped local-write policy.

Equations

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

def Miri.Interpreter.ValidityMemory.bind {K P S C Extra F A E H X : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (base : ValidityVisitor.Hooks P S C Extra F A PaddingHandle) (env : Environment P E K H X S) (validationInProgress : M S Bool) (afterLocalWrite : MIR.LocalId → Bool → M S Unit) (willValidate : MemoryOperandLayout → Bool) : ValidityVisitor.Hooks P S C Extra F A PaddingHandle

Install the concrete allocation operations without replacing compiler, reference, vtable or machine-retag queries with successful stubs.

Equations

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