Canonical typed-memory provider closure: address resolution retains source TB tag/wildcard extras, and discriminant execution consumes actual compiler facts plus real typed field reads/writes. No synthetic stack is constructed.

@[reducible, inline]

abbrev Miri.Interpreter.TypedMemoryProviders.User (User : Type) : Type

Equations

• Miri.Interpreter.TypedMemoryProviders.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.TypedMemoryProviders.Machine (K U : Type) : Type

Equations

• Miri.Interpreter.TypedMemoryProviders.Machine K U = Miri.Interpreter.MachineHooks.MachineState K (Miri.Interpreter.TypedMemoryProviders.User U)

@[reducible, inline]

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

Equations

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

def Miri.Interpreter.TypedMemoryProviders.resolvePointer {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : Int) : PlaceMachine.MachineM K (User U) (Except UInt64 (Memory.ResolvedPointer Memory.ProvenanceExtra))

Source ptr_try_get_alloc_id performs address lookup without ordinary access hooks. Parent provenance is reduced only to its source tag/wildcard extra; allocation identity stays in ResolvedPointer.allocId and the address cache.

Equations

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

def Miri.Interpreter.TypedMemoryProviders.bindAccess {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (base : ValidityMachine.Access K U) : ValidityMachine.Access K U

Equations

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

def Miri.Interpreter.TypedMemoryProviders.lifecycleResolver {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K → PlaceMachine.AccessState K (User U) → Memory.Pointer (Option Memory.Provenance) → Int → Memory.PointerResolutionResult Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (User U)) Memory.ProvenanceExtra

Lifecycle's older resolver boundary has no typed error variant; preserve that error in AccessState.pendingError, which AllocationMachine propagates before classifying its legacy pointer failure. Resolution failure commits no allocation removal or byte effects.

Equations

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

def Miri.Interpreter.TypedMemoryProviders.bindLifecycle {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (base : Memory.MemoryLifecycleHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (User U)) Memory.ProvenanceExtra) : Memory.MemoryLifecycleHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (User U)) Memory.ProvenanceExtra

Equations

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

def Miri.Interpreter.TypedMemoryProviders.discriminant {K U C : Type} [DecidableEq K] (facts : Input.CompilerFacts.Context) (access : ValidityMachine.Access K U) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (base : DiscriminantHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) : DiscriminantHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

All five discriminant compiler queries come from actual exporter evidence. Read/write field operations are canonical source projections and typed memory; source invalid-tag/niche/order logic remains the existing Discriminant driver.

Equations

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

def Miri.Interpreter.TypedMemoryProviders.bindRvalue {K U C : Type} (discr : DiscriminantHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (base : RvalueHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) : RvalueHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Rvalue and Aggregate run exactly the same discriminant record, so direct, niche and uninhabited checks cannot diverge between reads and tag writes.

Equations

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

def Miri.Interpreter.TypedMemoryProviders.bindAggregate {K U C : Type} (discr : DiscriminantHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (base : AggregateHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) : AggregateHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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

def Miri.Interpreter.TypedMemoryProviders.bindIntrinsics {K U C : Type} (discr : DiscriminantHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (base : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) : IntrinsicHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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