Connected compiler and machine providers for runtime typed validity and Tree Borrows. Existing actual vtable/discriminant/global compiler dictionaries remain shared; no new representation of values, heaps, or type IDs is added.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def Miri.Interpreter.TypedValidityProviders.resolveAllocation {K U : Type} (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (ptr : Memory.Pointer (Option Memory.Provenance)) : M K U (Option TreeBorrows.RetagPipeline.ResolvedLocation)

Source ptr_try_get_alloc_id(ptr,0) supplies the actual offset and parent TB provenance, including wildcard provenance. No physical read/access hooks run.

Equations

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

def Miri.Interpreter.TypedValidityProviders.retagHooks {K U C F A : Type} [DecidableEq K] (prepared : Input.CompilerFactAdapters.Prepared) (runtime : Input.CompilerRuntimeQueries.Prepared) (access : ValidityMachine.Access K U) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (vtable : VTableHooks Memory.Provenance (State K U) C F A) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (choice : C) (base : TypedRetag.Hooks K (User U)) : TypedRetag.Hooks K (User U)

Close compiler queries, pointer conversion/resolution, dynamic layout and actual freeze projections. Source diagnostic policy, rustc_no_writable and configuration flags remain typed inputs, not successful placeholder defaults.

Equations

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

def Miri.Interpreter.TypedValidityProviders.visitor {K U C F A : Type} [DecidableEq K] (prepared : Input.CompilerFactAdapters.Prepared) (runtime : Input.CompilerRuntimeQueries.Prepared) (access : ValidityMachine.Access K U) (allocation : PlaceMachine.AllocationConfig K (User U)) (compiler : ValidityMachine.Compiler K U C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (retag : TypedRetag.Hooks K (User U)) (retagFuel : Nat) (base : ValidityVisitor.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra F A ValidityMemory.PaddingHandle) : ValidityVisitor.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra F A ValidityMemory.PaddingHandle

Compose compiler type/path evidence, real Box projection, actual immediate pointer construction and existing canonical memory/ghost/retag visitor. The remaining base CTFE lookup and vtable/discriminant records are genuine compiler allocation/type pipelines, not a guessed result from payload bytes.

Equations

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