Executable projection rules from pinned rustc interpret/projection.rs. Compiler queries and machine-owned operations are required fallible callbacks. No projection reads memory, validates a discriminant, or erases provenance.

structure Miri.Interpreter.OpTy (Prov : Type) : Type

• op : Operand Prov
• layout : ABI.TyAndLayout MIR.TyId

@[instance_reducible]

instance Miri.Interpreter.instReprOpTy {Prov✝ : Type} [Repr Prov✝] : Repr (OpTy Prov✝)

Equations

• Miri.Interpreter.instReprOpTy = { reprPrec := Miri.Interpreter.instReprOpTy.repr }

def Miri.Interpreter.instReprOpTy.repr {Prov✝ : Type} [Repr Prov✝] : OpTy Prov✝ → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ProjectionError : Type

• machineError (error : StepError) : ProjectionError
• obligation (operation : String) : ProjectionError
• invariant (message : String) : ProjectionError
• bounds (len index : UInt64) : ProjectionError
• pointerArithOverflow : ProjectionError
• layout (reason : ABI.LayoutError) : ProjectionError
• size (reason : ABI.SizeError) : ProjectionError
• align (reason : ABI.AlignError) : ProjectionError
• offset (reason : MemPlaceOffsetError) : ProjectionError
• immediate (reason : ImmediateError) : ProjectionError
• scalar (reason : Memory.ScalarError) : ProjectionError

def Miri.Interpreter.instDecidableEqProjectionError.decEq (x✝ x✝¹ : ProjectionError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqProjectionError : DecidableEq ProjectionError

Equations

• Miri.Interpreter.instDecidableEqProjectionError = Miri.Interpreter.instDecidableEqProjectionError.decEq

def Miri.Interpreter.instReprProjectionError.repr : ProjectionError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprProjectionError : Repr ProjectionError

Equations

• Miri.Interpreter.instReprProjectionError = { reprPrec := Miri.Interpreter.instReprProjectionError.repr }

structure Miri.Interpreter.ProjectionCx (Prov : Type) : Type

Compiler/machine dependencies are explicit, including ABI checking of immediates and dynamic alignment computation (which may execute custom DST code). subsliceLayout must construct the array type or retain the slice type and run layout_of; sliceMetadata must use the target usize representation.

• target : ABI.TargetDataLayout
• maxSizeOfVal : ABI.Size
• isSliceOrStr : MIR.TyId → Except ProjectionError Bool
• field : ABI.TyAndLayout MIR.TyId → Nat → Except ProjectionError (ABI.TyAndLayout MIR.TyId)
• variant : ABI.TyAndLayout MIR.TyId → Nat → Except ProjectionError (ABI.TyAndLayout MIR.TyId)
• dynamicAlign : MemPlaceMeta Prov → ABI.TyAndLayout MIR.TyId → Except ProjectionError (Option ABI.Align)
• packedAlign : MIR.TyId → Except ProjectionError (Option ABI.Align)
• immediateOffset : Immediate Prov → ABI.TyAndLayout MIR.TyId → ABI.Size → ABI.TyAndLayout MIR.TyId → Except ProjectionError (Immediate Prov)
• memoryOffset : MemPlace Prov → ABI.Size → OffsetMode → MemPlaceMeta Prov → Except ProjectionError (MemPlace Prov)
• subsliceLayout : ABI.TyAndLayout MIR.TyId → UInt64 → Except ProjectionError (ABI.TyAndLayout MIR.TyId × MemPlaceMeta Prov)
• layoutOf : MIR.TyId → Except ProjectionError (ABI.TyAndLayout MIR.TyId)
• deref : OpTy Prov → Except ProjectionError (OpTy Prov)
• localIndex : MIR.LocalId → Except ProjectionError UInt64

def Miri.Interpreter.projectionMemoryOffset {Prov ProvExtra : Type} (target : Memory.PointerArithmetic) (resolve : Memory.PointerResolver Prov ProvExtra) (lookup : Memory.LiveAllocationLookup) (place : MemPlace Prov) (offset : ABI.Size) (mode : OffsetMode) (metadata : MemPlaceMeta Prov) : Except ProjectionError (MemPlace Prov)

The actual memory adapter delegates to the existing pointer arithmetic semantics, retaining allocation identity, provenance and misalignment.

Equations

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

def Miri.Interpreter.projectionImmediateOffset {Prov : Type} (validate : Immediate Prov → ABI.LayoutData → Except ProjectionError Unit) (value : Immediate Prov) (source : ABI.TyAndLayout MIR.TyId) (offset : ABI.Size) (target : ABI.TyAndLayout MIR.TyId) (debugAssertions : Bool := true) : Except ProjectionError (Immediate Prov)

Source ImmTy::offset_. ABI validation is required before extraction and on the resulting immediate, even for uninitialized/uninhabited/ZST values.

Equations

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

def Miri.Interpreter.OpTy.metadata {Prov : Type} (self : OpTy Prov) : MemPlaceMeta Prov

Equations

• self.metadata = match self.op with | Miri.Interpreter.Operand.indirect place => place.metadata | Miri.Interpreter.Operand.immediate value => Miri.Interpreter.MemPlaceMeta.none

def Miri.Interpreter.OpTy.offsetWithMeta {Prov : Type} (cx : ProjectionCx Prov) (base : OpTy Prov) (offset : ABI.Size) (mode : OffsetMode) (metadata : MemPlaceMeta Prov) (layout : ABI.TyAndLayout MIR.TyId) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.OpTy.offset {Prov : Type} (cx : ProjectionCx Prov) (base : OpTy Prov) (offset : ABI.Size) (layout : ABI.TyAndLayout MIR.TyId) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.OpTy.transmute {Prov : Type} (cx : ProjectionCx Prov) (base : OpTy Prov) (layout : ABI.TyAndLayout MIR.TyId) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.OpTy.len {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) : Except ProjectionError UInt64

Equations

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

def Miri.Interpreter.projectField {Prov : Type} (cx : ProjectionCx Prov) (base : OpTy Prov) (field : Nat) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.projectDowncast {Prov : Type} (cx : ProjectionCx Prov) (base : OpTy Prov) (variant : Nat) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.projectIndex {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (index : UInt64) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.projectConstantIndex {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (offset minLength : UInt64) (fromEnd : Bool) : Except ProjectionError (OpTy Prov)

Equations

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

def Miri.Interpreter.prepareSubslice {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (fromIndex to : UInt64) (fromEnd : Bool) : Except ProjectionError (ABI.Size × UInt64)

Equations

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

def Miri.Interpreter.projectSubslice {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (fromIndex to : UInt64) (fromEnd : Bool) : Except ProjectionError (OpTy Prov)

Equations

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

structure Miri.Interpreter.ProjectionArrayIterator (Prov : Type) : Type

Iterator range state is advanced before projecting the element, even when that projection fails, matching Range::next followed by fallible offset.

• base : OpTy Prov
• nextIndex : UInt64
• endIndex : UInt64
• stride : ABI.Size
• fieldLayout : ABI.TyAndLayout MIR.TyId

def Miri.Interpreter.projectArrayFields {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (unitLayout : ABI.TyAndLayout MIR.TyId) : Except ProjectionError (ProjectionArrayIterator Prov)

Equations

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

def Miri.Interpreter.ProjectionArrayIterator.next {Prov : Type} (cx : ProjectionCx Prov) : EStateM ProjectionError (ProjectionArrayIterator Prov) (Option (UInt64 × OpTy Prov))

Equations

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

def Miri.Interpreter.project {Prov : Type} [Memory.PointerProvenance Prov] (cx : ProjectionCx Prov) (base : OpTy Prov) (elem : MIR.ProjectionElem) : Except ProjectionError (OpTy Prov)

Consume the existing source MIR projection syntax; oversized imported Nat indices fail explicitly rather than silently truncating to upstream u64.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.project cx base (Miri.MIR.ProjectionElem.Field field ty) = Miri.Interpreter.projectField cx base field
• Miri.Interpreter.project cx base (Miri.MIR.ProjectionElem.Downcast name variant) = Miri.Interpreter.projectDowncast cx base variant
• Miri.Interpreter.project cx base Miri.MIR.ProjectionElem.Deref = cx.deref base
• Miri.Interpreter.project cx base (Miri.MIR.ProjectionElem.Index localId) = do let __do_lift ← cx.localIndex localId Miri.Interpreter.projectIndex cx base __do_lift
• Miri.Interpreter.project cx base (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = do let __do_lift ← cx.layoutOf ty Miri.Interpreter.OpTy.transmute cx base __do_lift
• Miri.Interpreter.project cx base (Miri.MIR.ProjectionElem.OpaqueCast ty) = throw (Miri.Interpreter.ProjectionError.invariant "OpaqueCast after borrowck")
• Miri.Interpreter.project cx base Miri.MIR.ProjectionElem.PhantomDeref = throw (Miri.Interpreter.ProjectionError.invariant "PhantomDeref after borrowck")