Global pointer-tag and protector bookkeeping from Miri's borrow_tracker::GlobalStateInner, FrameState, and ProtectorKind.

This is the borrow-tracker bookkeeping layer only. Allocation tree mutations, protector-triggered reads on stack pop, and memory accesses live in separate Tree Borrows operations.

inductive Miri.TreeBorrows.ProtectorKind : Type

Miri's two protector strengths.

• WeakProtector : ProtectorKind
• StrongProtector : ProtectorKind

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqProtectorKind : DecidableEq ProtectorKind

Equations

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

def Miri.TreeBorrows.instReprProtectorKind.repr : ProtectorKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprProtectorKind : Repr ProtectorKind

Equations

• Miri.TreeBorrows.instReprProtectorKind = { reprPrec := Miri.TreeBorrows.instReprProtectorKind.repr }

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedProtectorKind : Inhabited ProtectorKind

Equations

• Miri.TreeBorrows.instInhabitedProtectorKind = { default := Miri.TreeBorrows.instInhabitedProtectorKind.default }

structure Miri.TreeBorrows.ProtectedTags : Type

Finite map from source BorTag to ProtectorKind.

The source uses an FxHashMap, whose iteration order is not semantic here. This representation preserves the observable map operations (insert replaces, remove deletes, lookup returns the current kind).

• entries : Array (Memory.BorTag × ProtectorKind)

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqProtectedTags : DecidableEq ProtectedTags

Equations

• Miri.TreeBorrows.instDecidableEqProtectedTags = Miri.TreeBorrows.instDecidableEqProtectedTags.decEq

def Miri.TreeBorrows.instDecidableEqProtectedTags.decEq (x✝ x✝¹ : ProtectedTags) : Decidable (x✝ = x✝¹)

Equations

• Miri.TreeBorrows.instDecidableEqProtectedTags.decEq { entries := a } { entries := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.instReprProtectedTags : Repr ProtectedTags

Equations

• Miri.TreeBorrows.instReprProtectedTags = { reprPrec := Miri.TreeBorrows.instReprProtectedTags.repr }

def Miri.TreeBorrows.instReprProtectedTags.repr : ProtectedTags → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedProtectedTags : Inhabited ProtectedTags

Equations

• Miri.TreeBorrows.instInhabitedProtectedTags = { default := Miri.TreeBorrows.instInhabitedProtectedTags.default }

def Miri.TreeBorrows.ProtectedTags.get (map : ProtectedTags) (tag : Memory.BorTag) : Option ProtectorKind

Equations

• map.get tag = Option.map Prod.snd (Array.find? (fun (entry : Miri.Memory.BorTag × Miri.TreeBorrows.ProtectorKind) => entry.fst == tag) map.entries)

def Miri.TreeBorrows.ProtectedTags.contains (map : ProtectedTags) (tag : Memory.BorTag) : Bool

Equations

• map.contains tag = (map.get tag).isSome

def Miri.TreeBorrows.ProtectedTags.insert (map : ProtectedTags) (tag : Memory.BorTag) (kind : ProtectorKind) : ProtectedTags

Equations

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

def Miri.TreeBorrows.ProtectedTags.remove (map : ProtectedTags) (tag : Memory.BorTag) : ProtectedTags

Equations

• map.remove tag = { entries := Array.filter (fun (entry : Miri.Memory.BorTag × Miri.TreeBorrows.ProtectorKind) => entry.fst != tag) map.entries }

def Miri.TreeBorrows.ProtectedTags.size (map : ProtectedTags) : Nat

Equations

• map.size = map.entries.size

@[simp]

theorem Miri.TreeBorrows.ProtectedTags.get_insert_same (map : ProtectedTags) (tag : Memory.BorTag) (kind : ProtectorKind) : (map.insert tag kind).get tag = some kind

@[simp]

theorem Miri.TreeBorrows.ProtectedTags.get_remove_same (map : ProtectedTags) (tag : Memory.BorTag) : (map.remove tag).get tag = none

structure Miri.TreeBorrows.FrameState : Type

Tags protected by one call frame, paired with the allocation whose Tree Borrows state must receive its release operation before the frame ends.

• protectedTags : Array (Memory.AllocId × Memory.BorTag)

def Miri.TreeBorrows.instDecidableEqFrameState.decEq (x✝ x✝¹ : FrameState) : Decidable (x✝ = x✝¹)

Equations

• Miri.TreeBorrows.instDecidableEqFrameState.decEq { protectedTags := a } { protectedTags := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqFrameState : DecidableEq FrameState

Equations

• Miri.TreeBorrows.instDecidableEqFrameState = Miri.TreeBorrows.instDecidableEqFrameState.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprFrameState : Repr FrameState

Equations

• Miri.TreeBorrows.instReprFrameState = { reprPrec := Miri.TreeBorrows.instReprFrameState.repr }

def Miri.TreeBorrows.instReprFrameState.repr : FrameState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedFrameState : Inhabited FrameState

Equations

• Miri.TreeBorrows.instInhabitedFrameState = { default := Miri.TreeBorrows.instInhabitedFrameState.default }

def Miri.TreeBorrows.FrameState.addProtector (frame : FrameState) (allocId : Memory.AllocId) (tag : Memory.BorTag) : FrameState

Equations

• frame.addProtector allocId tag = { protectedTags := frame.protectedTags.push (allocId, tag) }

def Miri.TreeBorrows.FrameState.liveBorrowTags (frame : FrameState) : Array (Memory.AllocId × Memory.BorTag)

Provenance pairs visited by the source VisitProvenance implementation. The global protected-tag table is intentionally not separately traced.

Equations

• frame.liveBorrowTags = frame.protectedTags

inductive Miri.TreeBorrows.GlobalStateError : Type

• pointerTagOverflow (tag : Memory.BorTag) : GlobalStateError

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqGlobalStateError : DecidableEq GlobalStateError

Equations

• Miri.TreeBorrows.instDecidableEqGlobalStateError = Miri.TreeBorrows.instDecidableEqGlobalStateError.decEq

def Miri.TreeBorrows.instDecidableEqGlobalStateError.decEq (x✝ x✝¹ : GlobalStateError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.instReprGlobalStateError.repr : GlobalStateError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprGlobalStateError : Repr GlobalStateError

Equations

• Miri.TreeBorrows.instReprGlobalStateError = { reprPrec := Miri.TreeBorrows.instReprGlobalStateError.repr }

structure Miri.TreeBorrows.GlobalState : Type

The semantic fields from Miri's GlobalStateInner that govern pointer tag allocation and protector bookkeeping. Root allocation IDs and tracked tag IDs use arrays as finite maps/sets; their insertion and lookup behavior matches the source's map/set API.

• nextPointerTag : Memory.BorTag
• rootPointerTags : Array (Memory.AllocId × Memory.BorTag)
• protectedTags : ProtectedTags
• trackedPointerTags : Array Memory.BorTag

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqGlobalState : DecidableEq GlobalState

Equations

• Miri.TreeBorrows.instDecidableEqGlobalState = Miri.TreeBorrows.instDecidableEqGlobalState.decEq

def Miri.TreeBorrows.instDecidableEqGlobalState.decEq (x✝ x✝¹ : GlobalState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprGlobalState : Repr GlobalState

Equations

• Miri.TreeBorrows.instReprGlobalState = { reprPrec := Miri.TreeBorrows.instReprGlobalState.repr }

def Miri.TreeBorrows.instReprGlobalState.repr : GlobalState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedGlobalState : Inhabited GlobalState

Equations

• Miri.TreeBorrows.instInhabitedGlobalState = { default := Miri.TreeBorrows.instInhabitedGlobalState.default }

def Miri.TreeBorrows.GlobalState.new (trackedPointerTags : Array Memory.BorTag := #[]) : GlobalState

Equations

• Miri.TreeBorrows.GlobalState.new trackedPointerTags = { trackedPointerTags := trackedPointerTags }

def Miri.TreeBorrows.GlobalState.isTrackedPointerTag (state : GlobalState) (tag : Memory.BorTag) : Bool

Equations

• state.isTrackedPointerTag tag = state.trackedPointerTags.contains tag

def Miri.TreeBorrows.GlobalState.rootTag? (state : GlobalState) (allocId : Memory.AllocId) : Option Memory.BorTag

Equations

• state.rootTag? allocId = Option.map Prod.snd (Array.find? (fun (entry : Miri.Memory.AllocId × Miri.Memory.BorTag) => entry.fst == allocId) state.rootPointerTags)

def Miri.TreeBorrows.GlobalState.newPointerTag (state : GlobalState) : Except GlobalStateError (GlobalState × Memory.BorTag)

Source GlobalStateInner::new_ptr: return the current tag and advance the counter with checked BorTag::succ. Miri unwraps overflow; this port retains it as an explicit error.

Equations

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

def Miri.TreeBorrows.GlobalState.rootPointerTag (state : GlobalState) (allocId : Memory.AllocId) : Except GlobalStateError (GlobalState × Memory.BorTag)

Source root_ptr_tag: return the stable per-allocation root tag, creating one with new_ptr when absent.

Equations

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

def Miri.TreeBorrows.GlobalState.removeUnreachableAllocs (state : GlobalState) (liveAllocIds : Array Memory.AllocId) : GlobalState

Source remove_unreachable_allocs, where liveAllocIds is the set passed by the allocation collector.

Equations

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

def Miri.TreeBorrows.GlobalState.addProtector (state : GlobalState) (frame : FrameState) (allocId : Memory.AllocId) (tag : Memory.BorTag) (kind : ProtectorKind) : GlobalState × FrameState

Add the two source-side records created when a reborrow installs a protector: one frame-owned (allocation, tag) pair and one global tag-to-kind entry used by access transitions.

Equations

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

def Miri.TreeBorrows.GlobalState.endCall (state : GlobalState) (frame : FrameState) : GlobalState

Source end_call: remove every tag listed by the frame from the global protected-tag map. Tree Borrows' release operation is performed before this bookkeeping step by on_stack_pop.

Equations

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

def Miri.TreeBorrows.GlobalState.liveBorrowTags (frames : Array FrameState) : Array (Memory.AllocId × Memory.BorTag)

The global map is only a lookup index; protected tags remain live through their frame-owned provenance records.

Equations

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

@[simp]

theorem Miri.TreeBorrows.GlobalState.newPointerTag_returns_one : new.newPointerTag = Except.ok (have __src := new; { nextPointerTag := { value := 2, nonzero := ⋯ }, rootPointerTags := __src.rootPointerTags, protectedTags := __src.protectedTags, trackedPointerTags := __src.trackedPointerTags }, Memory.BorTag.one)

@[simp]

theorem Miri.TreeBorrows.GlobalState.rootPointerTag_existing (state : GlobalState) (allocId : Memory.AllocId) (tag : Memory.BorTag) (h : state.rootTag? allocId = some tag) : state.rootPointerTag allocId = Except.ok (state, tag)

@[simp]

theorem Miri.TreeBorrows.GlobalState.endCall_empty (state : GlobalState) : state.endCall { } = state

@[simp]

theorem Miri.TreeBorrows.GlobalState.addProtector_global_lookup (state : GlobalState) (frame : FrameState) (allocId : Memory.AllocId) (tag : Memory.BorTag) (kind : ProtectorKind) : (state.addProtector frame allocId tag kind).fst.protectedTags.get tag = some kind