Source place.rs pointer→place construction and deref_pointer, on the canonical Miri address/alignment/validity state. Construction merely caches misalignment; only typed safe-pointer dereference checks dereferenceability.

@[reducible, inline]

abbrev Miri.Interpreter.PointerPlaceMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.PointerPlaceMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.PointerPlaceMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.PointerPlaceMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

inductive Miri.Interpreter.PointerPlaceMachine.Kind : Type

• reference : Kind
• box : Kind
• raw : Kind
• other : Kind

@[instance_reducible]

instance Miri.Interpreter.PointerPlaceMachine.instDecidableEqKind : DecidableEq Kind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PointerPlaceMachine.instReprKind : Repr Kind

Equations

• Miri.Interpreter.PointerPlaceMachine.instReprKind = { reprPrec := Miri.Interpreter.PointerPlaceMachine.instReprKind.repr }

def Miri.Interpreter.PointerPlaceMachine.instReprKind.repr : Kind → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.PointerPlaceMachine.UnsizedTail : Type

• dynamic (expectedTrait : Nat) : UnsizedTail
• slice : UnsizedTail
• str : UnsizedTail
• foreign : UnsizedTail
• other : UnsizedTail

@[instance_reducible]

instance Miri.Interpreter.PointerPlaceMachine.instReprUnsizedTail : Repr UnsizedTail

Equations

• Miri.Interpreter.PointerPlaceMachine.instReprUnsizedTail = { reprPrec := Miri.Interpreter.PointerPlaceMachine.instReprUnsizedTail.repr }

def Miri.Interpreter.PointerPlaceMachine.instReprUnsizedTail.repr : UnsizedTail → Nat → Std.Format

Equations

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

structure Miri.Interpreter.PointerPlaceMachine.Compiler (K U C : Type) : Type

• kind : C → MIR.TyId → M K U Kind
• builtinDeref : C → MIR.TyId → M K U (Option MIR.TyId)
• layoutOf : C → MIR.TyId → M K U LocalLayout
• structTail : C → MIR.TyId → M K U UnsizedTail

structure Miri.Interpreter.PointerPlaceMachine.AlignmentContext (User : Type) : Type

Representation access to the actual alignment policy and shared pointer promises. These are data projections, not an operation-result oracle.

• policy : User → ValidityMachine.AlignmentCheck
• promises : User → Array (Memory.AllocId × ABI.Size × ABI.Align)

def Miri.Interpreter.PointerPlaceMachine.controlledAlignment {U : Type} : AlignmentContext (ValidityMachine.UserState U)

Equations

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

def Miri.Interpreter.PointerPlaceMachine.misalignmentWith {K User : Type} (access : PlaceMachine.AccessConfig K User) (context : AlignmentContext User) (ptr : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : MachineHooks.M K User (Option Memory.Misalignment)

Source is_ptr_misaligned, including the no-resolve disabled/one-byte path, allocation symbolic policy, and integer-address fallback.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.misalignment {K U : Type} (access : ValidityMachine.Access K U) (ptr : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : M K U (Option Memory.Misalignment)

Existing concrete control/pointer-state API uses the same generic rule.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.withMetadata {K U : Type} (access : ValidityMachine.Access K U) (ptr : Memory.Pointer (Option Memory.Provenance)) (metadata : MemPlaceMeta Memory.Provenance) (layout : LocalLayout) (unaligned : Bool) : M K U (MPlaceTy Memory.Provenance)

Equations

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

def Miri.Interpreter.PointerPlaceMachine.fromPointer {K U : Type} (access : ValidityMachine.Access K U) (ptr : Memory.Pointer (Option Memory.Provenance)) (layout : LocalLayout) (unaligned : Bool) : M K U (MPlaceTy Memory.Provenance)

Equations

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

def Miri.Interpreter.PointerPlaceMachine.fromImmediate {K U C : Type} (access : ValidityMachine.Access K U) (compiler : Compiler K U C) (choice : C) (value : RvalueImmTy Memory.Provenance) : M K U (MPlaceTy Memory.Provenance)

Source builtin_deref/layout query precedes scalar/metadata extraction. No dynamic-layout or pointer validity check occurs in this constructor.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.dereference {K U C F A : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (compiler : Compiler K U C) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (fuel : Nat) (choice : C) (source : OpTy Memory.Provenance) : M K U (MPlaceTy Memory.Provenance)

Full source typed dereference: kind check, read, place construction, conditional validity, safe-pointer null/layout/access/alignment; raw-pointer unsized dynamic tails validate only their vtable identity/type.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.bindCompiler {K U C F A : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (allocation : PlaceMachine.AllocationConfig K (ValidityMachine.UserState U)) (compiler : Compiler K U C) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (fuel : Nat) (base : PlaceMachine.CompilerHooks K (ValidityMachine.UserState U) C) : PlaceMachine.CompilerHooks K (ValidityMachine.UserState U) C

Close ordinary and simple-deref PlaceHooks with the same source driver. Simple deref skips kind/validity checks and performs only read+construction.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.bindScalarOps {K U C F A : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (compiler : Compiler K U C) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (fuel : Nat) (base : ScalarOpsHooks Memory.Provenance (State K U) C) : ScalarOpsHooks Memory.Provenance (State K U) C

Unary PtrMetadata's source validity event executes before extracting the metadata scalar. Immediates remain typed and do not gain spurious memory reads.

Equations

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

def Miri.Interpreter.PointerPlaceMachine.bindCast {K U C F A V : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (compiler : Compiler K U C) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (fuel : Nat) (base : CastHooks Memory.Provenance (State K U) C V) : CastHooks Memory.Provenance (State K U) C V

Equations

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

def Miri.Interpreter.PointerPlaceMachine.bindIntrinsics {K U C F A : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (compiler : Compiler K U C) (dynamic : DynamicLayoutHooks Memory.Provenance (State K U) C) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (fuel : Nat) (base : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Close the common pointer-conversion/dereference leaves of core intrinsics and atomic access, reusing precisely the same validity driver as ordinary MIR.

Equations

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