Source-ordered tb_retag_ptr_value / tb_retag_place / tb_reborrow core. Rustc type/layout queries, pointer validation/resolution, diagnostics, and data race operations are explicit hook results. The live allocation's actual BorrowTree is stored in MemoryState extra data and updated through the source allocation API. This module does not claim the interpreter hooks are implemented.

structure Miri.TreeBorrows.RetagPipeline.MachineState (MachineKind : Type) : Type

• memory : Memory.MemoryState Memory.Provenance BorrowTree MachineKind
• global : GlobalState
• frame : FrameState

structure Miri.TreeBorrows.RetagPipeline.ResolvedLocation : Type

• allocId : Memory.AllocId
• baseOffset : ABI.Size
• parentProvenance : Memory.ProvenanceExtra

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instDecidableEqResolvedLocation : DecidableEq ResolvedLocation

Equations

• Miri.TreeBorrows.RetagPipeline.instDecidableEqResolvedLocation = Miri.TreeBorrows.RetagPipeline.instDecidableEqResolvedLocation.decEq

def Miri.TreeBorrows.RetagPipeline.instDecidableEqResolvedLocation.decEq (x✝ x✝¹ : ResolvedLocation) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.RetagPipeline.instReprResolvedLocation.repr : ResolvedLocation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instReprResolvedLocation : Repr ResolvedLocation

Equations

• Miri.TreeBorrows.RetagPipeline.instReprResolvedLocation = { reprPrec := Miri.TreeBorrows.RetagPipeline.instReprResolvedLocation.repr }

inductive Miri.TreeBorrows.RetagPipeline.RetagInputKind : Type

The source tb_retag_ptr_value type dispatch. Raw pointers and boxes with custom allocators return before place conversion; only reference types and global boxes construct a NewPermission and call tb_retag_place.

• reference : RetagInputKind
• globalBox : RetagInputKind
• rawPointer : RetagInputKind
• customAllocatorBox : RetagInputKind
• invalidType : RetagInputKind

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagInputKind : DecidableEq RetagInputKind

Equations

• Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagInputKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.TreeBorrows.RetagPipeline.instReprRetagInputKind.repr : RetagInputKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instReprRetagInputKind : Repr RetagInputKind

Equations

• Miri.TreeBorrows.RetagPipeline.instReprRetagInputKind = { reprPrec := Miri.TreeBorrows.RetagPipeline.instReprRetagInputKind.repr }

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instInhabitedRetagInputKind : Inhabited RetagInputKind

Equations

• Miri.TreeBorrows.RetagPipeline.instInhabitedRetagInputKind = { default := Miri.TreeBorrows.RetagPipeline.instInhabitedRetagInputKind.default }

structure Miri.TreeBorrows.RetagPipeline.RetagTypeShape : Type

Predicates supplied by rustc for the source type match. Although Rust's type constructors are disjoint, isGlobalBox is a separate predicate and is tested before TyKind, exactly as in tb_retag_ptr_value. Keeping the predicates explicit lets the Lean caller preserve that guard priority.

• isGlobalBox : Bool
• isReference : Bool
• isRawPointer : Bool
• isBox : Bool

def Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagTypeShape.decEq (x✝ x✝¹ : RetagTypeShape) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagTypeShape : DecidableEq RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagTypeShape = Miri.TreeBorrows.RetagPipeline.instDecidableEqRetagTypeShape.decEq

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instReprRetagTypeShape : Repr RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.instReprRetagTypeShape = { reprPrec := Miri.TreeBorrows.RetagPipeline.instReprRetagTypeShape.repr }

def Miri.TreeBorrows.RetagPipeline.instReprRetagTypeShape.repr : RetagTypeShape → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instInhabitedRetagTypeShape : Inhabited RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.instInhabitedRetagTypeShape = { default := Miri.TreeBorrows.RetagPipeline.instInhabitedRetagTypeShape.default }

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.classify (shape : RetagTypeShape) : RetagInputKind

Equations

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

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.reference : RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.RetagTypeShape.reference = { }

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.globalBox : RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.RetagTypeShape.globalBox = { isGlobalBox := true, isReference := false, isBox := true }

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.rawPointer : RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.RetagTypeShape.rawPointer = { isReference := false, isRawPointer := true }

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.customAllocatorBox : RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.RetagTypeShape.customAllocatorBox = { isReference := false, isBox := true }

def Miri.TreeBorrows.RetagPipeline.RetagTypeShape.invalid : RetagTypeShape

Equations

• Miri.TreeBorrows.RetagPipeline.RetagTypeShape.invalid = { isReference := false }

inductive Miri.TreeBorrows.RetagPipeline.Event : Type

• placeConverted : Event
• reborrowSizeSelected (size : ABI.Size) : Event
• pointerTagAllocated (tag : Memory.BorTag) : Event
• allocationResolution (location : Option Memory.AllocId) : Event
• pointerAccessChecked : Event
• creationLogCalled (tag : Memory.BorTag) (location : Option Memory.AllocId) (tracked : Bool) : Event
• protectorRegistered (tag : Memory.BorTag) (kind : ProtectorKind) : Event
• allocationKindChecked (allocId : Memory.AllocId) (kind : Memory.AllocationKind) : Event
• freezeLayoutVisited : Event
• allocationExtraLoaded (allocId : Memory.AllocId) : Event
• parentTreeAccess (kind : AccessKind) (range : DataStructures.ByteRange) : Event
• dataRaceAccess (kind : AccessKind) (range : DataStructures.ByteRange) : Event
• childInserted (tag : Memory.BorTag) : Event
• reborrowReturned (provenance : Option Memory.Provenance) : Event
• placeProvenanceReplaced (provenance : Option Memory.Provenance) : Event
• retaggedValueReconstructed : Event

def Miri.TreeBorrows.RetagPipeline.instDecidableEqEvent.decEq (x✝ x✝¹ : Event) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instDecidableEqEvent : DecidableEq Event

Equations

• Miri.TreeBorrows.RetagPipeline.instDecidableEqEvent = Miri.TreeBorrows.RetagPipeline.instDecidableEqEvent.decEq

def Miri.TreeBorrows.RetagPipeline.instReprEvent.repr : Event → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instReprEvent : Repr Event

Equations

• Miri.TreeBorrows.RetagPipeline.instReprEvent = { reprPrec := Miri.TreeBorrows.RetagPipeline.instReprEvent.repr }

inductive Miri.TreeBorrows.RetagPipeline.Error : Type

• placeConversion (message : String) : Error
• rawPointerWrongMode : Error
• invalidType : Error
• sizeQuery (message : String) : Error
• pointerTagOverflow (tag : Memory.BorTag) : Error
• pointerAccess (message : String) : Error
• creationLog (message : String) : Error
• nonzeroSizeWithoutAllocation (size : ABI.Size) : Error
• allocationLookup (error : Memory.AllocationLookupError) : Error
• nonLiveAllocationHasBytes (kind : Memory.AllocationKind) (size : ABI.Size) : Error
• freezeVisitor (message : String) : Error
• initialState (error : RetagPolicy.InitialStateError) : Error
• layoutRangeMap (error : DataStructures.DedupRangeMapError) : Error
• allocationExtra (message : String) : Error
• treeExtraUnavailable (allocId : Memory.AllocId) : Error
• writeToReadOnly (allocId : Memory.AllocId) : Error
• offsetOverflow (baseOffset : ABI.Size) (relativeOffset : UInt64) : Error
• rangeEndOverflow (start length : ABI.Size) : Error
• treeAccess (range : DataStructures.ByteRange) (status : BorrowTree.BorrowTreeAccessStatus) : Error
• missingDataRaceResult (index : Nat) : Error
• dataRace (message : String) : Error
• childInsert (error : BorrowTree.ChildInsertError) : Error
• memoryUpdate (error : Memory.AllocationLookupError) : Error

def Miri.TreeBorrows.RetagPipeline.instDecidableEqError.decEq (x✝ x✝¹ : Error) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instDecidableEqError : DecidableEq Error

Equations

• Miri.TreeBorrows.RetagPipeline.instDecidableEqError = Miri.TreeBorrows.RetagPipeline.instDecidableEqError.decEq

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instReprError : Repr Error

Equations

• Miri.TreeBorrows.RetagPipeline.instReprError = { reprPrec := Miri.TreeBorrows.RetagPipeline.instReprError.repr }

def Miri.TreeBorrows.RetagPipeline.instReprError.repr : Error → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.RetagPipeline.Result (MachineKind : Type) : Type

• state : MachineState MachineKind
• outcome : Except Error (Option Memory.Provenance)
• events : Array Event

structure Miri.TreeBorrows.RetagPipeline.Hooks : Type

Inputs supplied by the rustc/Miri layer around tb_reborrow. A failed hook is kept at the point where the pinned source calls it. freezeVisitor is consulted only when precise interior mutability is enabled; dataRace is none when the allocation has no vector-clock model.

• placeConversion : Except String Unit
• sizeAndAlignOfValue : Except String (Option ABI.Size)
• pointerAccess : Except String Unit
• allocationResolution : Option ResolvedLocation

  Result of ptr_try_get_alloc_id(place.ptr(), 0), consulted only after check_ptr_access succeeds. An absent result takes Miri's zero-size path.

• creationLog : Except String Unit
• freezeVisitor : Except String (DataStructures.DedupRangeMap Bool)
• allocationExtra : Except String Unit
• dataRace : Option (Array (Except String Unit))

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instInhabitedHooks : Inhabited Hooks

Equations

• Miri.TreeBorrows.RetagPipeline.instInhabitedHooks = { default := Miri.TreeBorrows.RetagPipeline.instInhabitedHooks.default }

structure Miri.TreeBorrows.RetagPipeline.Request : Type

• typeShape : RetagTypeShape
• typeFacts : RetagPolicy.TypeFacts
• referenceKind : RetagPolicy.ReferenceKind
• mode : RetagPolicy.RetagMode
• config : RetagPolicy.PolicyConfig
• layoutSize : ABI.Size
• originalProvenance : Option Memory.Provenance
• pointeeIsFreeze : Bool
• preciseInteriorMut : Bool
• hooks : Hooks

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.instInhabitedRequest : Inhabited Request

Equations

• Miri.TreeBorrows.RetagPipeline.instInhabitedRequest = { default := Miri.TreeBorrows.RetagPipeline.instInhabitedRequest.default }

def Miri.TreeBorrows.RetagPipeline.retagPointerValue {MachineKind : Type} [DecidableEq MachineKind] (state : MachineState MachineKind) (request : Request) : Result MachineKind

Source tb_retag_ptr_value followed by tb_retag_place and the allocation-local portion of tb_reborrow. Policy selection precedes place conversion; the dynamic-size query precedes new_ptr; pointer validation follows tag allocation. Hook failures return the state accumulated up to that source point, including installed protectors and earlier parent accesses.

Equations

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