Miri machine validation defaults and scoped validity execution. Source machine.rs ValidationMode/enforce_validity/cached_union_data_range and interpret/memory.rs ghost_run_mut. Actual validation/retag/memory ports are bound here; only compiler/pointer/trait queries remain supplied dictionaries.

inductive Miri.Interpreter.ValidityMachine.ValidationMode : Type

• No : ValidationMode
• Shallow : ValidationMode
• Deep : ValidationMode

@[instance_reducible]

instance Miri.Interpreter.ValidityMachine.instDecidableEqValidationMode : DecidableEq ValidationMode

Equations

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

def Miri.Interpreter.ValidityMachine.instReprValidationMode.repr : ValidationMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityMachine.instReprValidationMode : Repr ValidationMode

Equations

• Miri.Interpreter.ValidityMachine.instReprValidationMode = { reprPrec := Miri.Interpreter.ValidityMachine.instReprValidationMode.repr }

inductive Miri.Interpreter.ValidityMachine.AlignmentCheck : Type

• None : AlignmentCheck
• Symbolic : AlignmentCheck
• Int : AlignmentCheck

@[instance_reducible]

instance Miri.Interpreter.ValidityMachine.instDecidableEqAlignmentCheck : DecidableEq AlignmentCheck

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ValidityMachine.instReprAlignmentCheck : Repr AlignmentCheck

Equations

• Miri.Interpreter.ValidityMachine.instReprAlignmentCheck = { reprPrec := Miri.Interpreter.ValidityMachine.instReprAlignmentCheck.repr }

def Miri.Interpreter.ValidityMachine.instReprAlignmentCheck.repr : AlignmentCheck → Nat → Std.Format

Equations

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

structure Miri.Interpreter.ValidityMachine.Control (User : Type) : Type

Concrete additional fields for the canonical machine's User payload. This extends machine state; it is not a second program representation or value IR.

• payload : User
• validation : ValidationMode
• alignment : AlignmentCheck
• ghost : Bool
• unionDataRanges : Array (MIR.TyId × Memory.Validity.DataRangeSet)

@[reducible, inline]

abbrev Miri.Interpreter.ValidityMachine.UserState (User : Type) : Type

Equations

• Miri.Interpreter.ValidityMachine.UserState User = Miri.Interpreter.PointerMachine.User (Miri.Interpreter.ValidityMachine.Control User)

@[reducible, inline]

abbrev Miri.Interpreter.ValidityMachine.State (K User : Type) : Type

Equations

• Miri.Interpreter.ValidityMachine.State K User = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.ValidityMachine.UserState User)

@[reducible, inline]

abbrev Miri.Interpreter.ValidityMachine.M (K User A : Type) : Type

Equations

• Miri.Interpreter.ValidityMachine.M K User A = Miri.Interpreter.MachineHooks.M K (Miri.Interpreter.ValidityMachine.UserState User) A

@[reducible, inline]

abbrev Miri.Interpreter.ValidityMachine.Access (K User : Type) : Type

Equations

• Miri.Interpreter.ValidityMachine.Access K User = Miri.Interpreter.PlaceMachine.AccessConfig K (Miri.Interpreter.ValidityMachine.UserState User)

@[reducible, inline]

abbrev Miri.Interpreter.ValidityMachine.Compiler (K User C : Type) : Type

Equations

• Miri.Interpreter.ValidityMachine.Compiler K User C = Miri.Interpreter.PlaceMachine.CompilerHooks K (Miri.Interpreter.ValidityMachine.UserState User) C

def Miri.Interpreter.ValidityMachine.enforceValidity {K User : Type} : M K User Bool

Equations

• Miri.Interpreter.ValidityMachine.enforceValidity = do let __do_lift ← get pure (__do_lift.machine.user.payload.validation != Miri.Interpreter.ValidityMachine.ValidationMode.No)

def Miri.Interpreter.ValidityMachine.enforceValidityRecursively {K User : Type} : M K User Bool

Equations

• Miri.Interpreter.ValidityMachine.enforceValidityRecursively = do let __do_lift ← get pure (__do_lift.machine.user.payload.validation == Miri.Interpreter.ValidityMachine.ValidationMode.Deep)

def Miri.Interpreter.ValidityMachine.validationInProgress {K User : Type} : M K User Bool

Equations

• Miri.Interpreter.ValidityMachine.validationInProgress = do let __do_lift ← get pure __do_lift.machine.user.payload.ghost

def Miri.Interpreter.ValidityMachine.withGhostValidation {K User A : Type} (action : M K User A) : M K User A

Exact non-nesting ghost scope. Ordinary allocation/local read/write hooks observe this flag and are suppressed; borrow/race trackers remain installed because source retagging during validity still executes their actual reborrow operations. Both normal and error results restore the flag while retaining all memory, clocks, borrow state, payload and cache mutations.

Equations

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

def Miri.Interpreter.ValidityMachine.cachedUnionRanges {K User : Type} (layout : LocalLayout) (compute : M K User Memory.Validity.DataRangeSet) : M K User Memory.Validity.DataRangeSet

Source machine.rs caches union data ranges by canonical compiler type ID. The computation runs only on a miss and inserts only after success; queries and partial effects of a failing computation are retained without a cache hit.

Equations

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

def Miri.Interpreter.ValidityMachine.scopedAccess {K User : Type} (access : Access K User) : M K User (Access K User)

Capture the actual current ghost flag at each memory operation, rather than when an interpreter hook dictionary is created.

Equations

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

def Miri.Interpreter.ValidityMachine.readImmediate {K User : Type} [DecidableEq K] (access : Access K User) (value : OpTy Memory.Provenance) : M K User (RvalueImmTy Memory.Provenance)

Equations

• Miri.Interpreter.ValidityMachine.readImmediate access value = do let __do_lift ← Miri.Interpreter.ValidityMachine.scopedAccess access Miri.Interpreter.PlaceMachine.readImmediate __do_lift value

def Miri.Interpreter.ValidityMachine.compilerPolicy {K User C : Type} (compiler : Compiler K User C) : Compiler K User C

Equations

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

def Miri.Interpreter.ValidityMachine.placeHooks {K User C : Type} [DecidableEq K] (access : Access K User) (allocation : PlaceMachine.AllocationConfig K (UserState User)) (compiler : Compiler K User C) : PlaceHooks Memory.Provenance (State K User) C MachineHooks.FrameExtra

Scoped optimized-local hooks and memory writes share the same canonical state flag. The write's enforce-validity decision is sampled at its source call, including padding-clearing policy inside the memory writer.

Equations

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

def Miri.Interpreter.ValidityMachine.memoryEnvironment {K User : Type} (access : Access K User) : ValidityMemory.Environment Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (UserState User)) Memory.ProvenanceExtra (State K User)

Actual byte/provenance/padding environment. Typed machine errors pass through the legacy allocation access boundary without being flattened into an unclassified string, and touched borrowed-global extras remain retained.

Equations

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

def Miri.Interpreter.ValidityMachine.checkPointerAccessResult {K User : Type} (access : Access K User) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) : M K User (Except Memory.AccessError Unit)

Typed form used by validity.rs, which remaps pointer access errors into path-qualified validation failures. Zero-sized validity retains the source no-resolve fast path.

Equations

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

def Miri.Interpreter.ValidityMachine.checkPointerAccess {K User : Type} (access : Access K User) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : ABI.Size) : M K User Unit

General machine users retain the ordinary typed access-error mapping; validity alone consumes checkPointerAccessResult to add its path context.

Equations

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

def Miri.Interpreter.ValidityMachine.checkPointerAlignResult {K User : Type} (access : Access K User) (pointer : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : M K User (Except Memory.Misalignment Unit)

Run the canonical alignment check while keeping its typed failure for validity.rs to classify with the active validation path. Resolution failures still use the ordinary machine error channel, and retain their state prefix.

Equations

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

def Miri.Interpreter.ValidityMachine.checkPointerAlign {K User : Type} (access : Access K User) (pointer : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : M K User Unit

General machine users retain the ordinary alignment error mapping. The validity visitor consumes checkPointerAlignResult to apply validity.rs's path-qualified error message without changing the underlying UB category.

Equations

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

def Miri.Interpreter.ValidityMachine.scalarMayBeNull {K User : Type} (scalar : Memory.Scalar Memory.Provenance) : M K User Bool

Miri provenance has absolute addresses, so scalar_may_be_null uses exactly ScalarInt::is_null without CTFE allocation guesses. Malformed scalar widths remain an explicit error.

Equations

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

def Miri.Interpreter.ValidityMachine.inMutableMemory {K User : Type} (place : RuntimePlace Memory.Provenance) : M K User Bool

Source CTFE mutability check: locals are mutable, memory must be interned, and any local cache of that global must agree with compiler mutability.

Equations

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

def Miri.Interpreter.ValidityMachine.visitor {K User C F A : Type} [DecidableEq K] (base : ValidityVisitor.Hooks Memory.Provenance (State K User) C MachineHooks.FrameExtra F A ValidityMemory.PaddingHandle) (access : Access K User) (allocation : PlaceMachine.AllocationConfig K (UserState User)) (compiler : Compiler K User C) (retag : TypedRetag.Hooks K (UserState User)) (retagBudget : Nat) : ValidityVisitor.Hooks Memory.Provenance (State K User) C MachineHooks.FrameExtra F A ValidityMemory.PaddingHandle

Close portable validity leaves with concrete typed places, scalar/byte memory operations, dynamic layout/vtable drivers, local index reads, source union cache and real scoped TypedRetag. Pointer dereference/access/alignment, compiler classification/path/layout facts and CTFE allocation-kind queries remain explicit in the supplied base dictionary.

Equations

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

def Miri.Interpreter.ValidityMachine.validateRuntime {K User C F A Pad : Type} [DecidableEq K] (h : ValidityVisitor.Hooks Memory.Provenance (State K User) C MachineHooks.FrameExtra F A Pad) (choice : C) (budget : Nat) (place : RuntimePlace Memory.Provenance) (reset : Bool) : M K User Unit

Ordinary write/copy validation defaults: reset=true; recursive iff Deep. Mode No is handled by enforceValidity at the source caller. Explicit direct validatePlace requests still validate, as the interpreter source does.

Equations

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

def Miri.Interpreter.ValidityMachine.bindValidation {K User C F A Pad : Type} [DecidableEq K] (compiler : Compiler K User C) (copy : PlaceCopyHooks Memory.Provenance (State K User) C) (h : ValidityVisitor.Hooks Memory.Provenance (State K User) C MachineHooks.FrameExtra F A Pad) (budget : Nat) : Compiler K User C × PlaceCopyHooks Memory.Provenance (State K User) C

Equations

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

def Miri.Interpreter.ValidityMachine.bindRvalue {K User C F A Pad : Type} [DecidableEq K] (base : RvalueHooks Memory.Provenance (State K User) C (RuntimePlace Memory.Provenance)) (access : Access K User) (allocation : PlaceMachine.AllocationConfig K (UserState User)) (compiler : Compiler K User C) (copy : PlaceCopyHooks Memory.Provenance (State K User) C) (h : ValidityVisitor.Hooks Memory.Provenance (State K User) C MachineHooks.FrameExtra F A Pad) : RvalueHooks Memory.Provenance (State K User) C (RuntimePlace Memory.Provenance)

Stateful default rvalue binding. Every place memory write samples the current ghost/validation flags; reference/raw-pointer retag triggers and modes remain exactly those chosen by the existing Rvalue dispatcher. Arithmetic, casts, constants and operand evaluation remain in the supplied base driver.

Equations

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