The allocation-local state layout from Miri's tree_borrows/tree.rs: tag-to-index map, indexed nodes, per-range location data, and ordered roots. The first constructor is the exact Tree::new root state. Diagnostic-only node history is intentionally omitted. Child insertion and access traversal are separate operations.

structure Miri.TreeBorrows.TreeNode : Type

Per-node information consumed by tree traversal and permission defaults. The source's NodeDebugInfo name is retained because miri_pointer_name and miri_print_borrow_state expose it. Access history is diagnostic-only and is not needed to print the current tree.

• tag : Memory.BorTag
• parent : Option UniIndex
• children : Array UniIndex
• defaultInitialPermission : Permission
• defaultInitialSifa : IdempotentForeignAccess
• isExposed : Bool
• debugName : Option String

def Miri.TreeBorrows.instDecidableEqTreeNode.decEq (x✝ x✝¹ : TreeNode) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqTreeNode : DecidableEq TreeNode

Equations

• Miri.TreeBorrows.instDecidableEqTreeNode = Miri.TreeBorrows.instDecidableEqTreeNode.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprTreeNode : Repr TreeNode

Equations

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

def Miri.TreeBorrows.instReprTreeNode.repr : TreeNode → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.TreeNode.defaultLocationState (node : TreeNode) : Tree.LocationState

Equations

• node.defaultLocationState = { permission := node.defaultInitialPermission, accessed := false, idempotentForeignAccess := node.defaultInitialSifa }

structure Miri.TreeBorrows.ExposedCacheNode : Type

Willard-cache counters for one node at one homogeneous byte range. Counters keep the source's u16 width.

• localWrites : UInt16
• localReads : UInt16

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqExposedCacheNode : DecidableEq ExposedCacheNode

Equations

• Miri.TreeBorrows.instDecidableEqExposedCacheNode = Miri.TreeBorrows.instDecidableEqExposedCacheNode.decEq

def Miri.TreeBorrows.instDecidableEqExposedCacheNode.decEq (x✝ x✝¹ : ExposedCacheNode) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.instReprExposedCacheNode.repr : ExposedCacheNode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprExposedCacheNode : Repr ExposedCacheNode

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedExposedCacheNode : Inhabited ExposedCacheNode

Equations

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

inductive Miri.TreeBorrows.WildcardAccessRelatedness : Type

• LocalAccess : WildcardAccessRelatedness
• ForeignAccess : WildcardAccessRelatedness
• EitherAccess : WildcardAccessRelatedness

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqWildcardAccessRelatedness : DecidableEq WildcardAccessRelatedness

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprWildcardAccessRelatedness : Repr WildcardAccessRelatedness

Equations

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

def Miri.TreeBorrows.instReprWildcardAccessRelatedness.repr : WildcardAccessRelatedness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedWildcardAccessRelatedness : Inhabited WildcardAccessRelatedness

Equations

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

structure Miri.TreeBorrows.ExposedCache : Type

Wildcard-relatedness cache for one location range.

• nodes : UniValMap ExposedCacheNode

def Miri.TreeBorrows.instDecidableEqExposedCache.decEq (x✝ x✝¹ : ExposedCache) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqExposedCache : DecidableEq ExposedCache

Equations

• Miri.TreeBorrows.instDecidableEqExposedCache = Miri.TreeBorrows.instDecidableEqExposedCache.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprExposedCache : Repr ExposedCache

Equations

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

def Miri.TreeBorrows.instReprExposedCache.repr : ExposedCache → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedExposedCache : Inhabited ExposedCache

Equations

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

inductive Miri.TreeBorrows.ExposedCacheError : Type

• MissingNode (index : UniIndex) : ExposedCacheError
• InvalidIndex (index : Nat) : ExposedCacheError
• ParentCycle (index : UniIndex) : ExposedCacheError

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqExposedCacheError : DecidableEq ExposedCacheError

Equations

• Miri.TreeBorrows.instDecidableEqExposedCacheError = Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq

def Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (x✝ x✝¹ : ExposedCacheError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.MissingNode index) (Miri.TreeBorrows.ExposedCacheError.InvalidIndex index_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.MissingNode index) (Miri.TreeBorrows.ExposedCacheError.ParentCycle index_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.InvalidIndex index) (Miri.TreeBorrows.ExposedCacheError.MissingNode index_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.InvalidIndex index) (Miri.TreeBorrows.ExposedCacheError.ParentCycle index_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.ParentCycle index) (Miri.TreeBorrows.ExposedCacheError.MissingNode index_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqExposedCacheError.decEq (Miri.TreeBorrows.ExposedCacheError.ParentCycle index) (Miri.TreeBorrows.ExposedCacheError.InvalidIndex index_1) = isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.instReprExposedCacheError : Repr ExposedCacheError

Equations

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

def Miri.TreeBorrows.instReprExposedCacheError.repr : ExposedCacheError → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.ExposedCacheUpdate : Type

• cache : ExposedCache
• outcome : Except ExposedCacheError Unit

def Miri.TreeBorrows.instDecidableEqExposedCacheUpdate.decEq (x✝ x✝¹ : ExposedCacheUpdate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqExposedCacheUpdate : DecidableEq ExposedCacheUpdate

Equations

• Miri.TreeBorrows.instDecidableEqExposedCacheUpdate = Miri.TreeBorrows.instDecidableEqExposedCacheUpdate.decEq

def Miri.TreeBorrows.instReprExposedCacheUpdate.repr : ExposedCacheUpdate → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprExposedCacheUpdate : Repr ExposedCacheUpdate

Equations

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

def Miri.TreeBorrows.ExposedCache.accessRelatedness (cache : ExposedCache) (root id : UniIndex) (kind : AccessKind) (isWildcardTree onlyForeign : Bool) : Option WildcardAccessRelatedness

Equations

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

def Miri.TreeBorrows.ExposedCache.updateExposure (cache : ExposedCache) (nodes : UniValMap TreeNode) (id : UniIndex) (oldLevel newLevel : WildcardAccessLevel) : ExposedCacheUpdate

Source ExposedCache::update_exposure: update the node's counters and propagate the same exposure delta through each ancestor. On malformed node indices/cycles, preserve all earlier counter mutations in the returned cache.

Equations

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

def Miri.TreeBorrows.ExposedCache.remove (cache : ExposedCache) (idx : UniIndex) : ExposedCache

Equations

• cache.remove idx = { nodes := cache.nodes.remove idx }

structure Miri.TreeBorrows.LocationTree : Type

The source's LocationTree: lazily stored permission state and one exposed-node cache per homogeneous range.

• perms : UniValMap Tree.LocationState
• exposedCache : ExposedCache

def Miri.TreeBorrows.instDecidableEqLocationTree.decEq (x✝ x✝¹ : LocationTree) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqLocationTree : DecidableEq LocationTree

Equations

• Miri.TreeBorrows.instDecidableEqLocationTree = Miri.TreeBorrows.instDecidableEqLocationTree.decEq

def Miri.TreeBorrows.instReprLocationTree.repr : LocationTree → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instReprLocationTree : Repr LocationTree

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedLocationTree : Inhabited LocationTree

Equations

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

structure Miri.TreeBorrows.BorrowTree : Type

Allocation-local tree state. roots begins with the allocation's unique root and may later contain ordered wildcard roots.

• tagMapping : UniKeyMap Memory.BorTag
• nodes : UniValMap TreeNode
• locations : DataStructures.DedupRangeMap LocationTree
• roots : Array UniIndex

def Miri.TreeBorrows.instDecidableEqBorrowTree.decEq (x✝ x✝¹ : BorrowTree) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqBorrowTree : DecidableEq BorrowTree

Equations

• Miri.TreeBorrows.instDecidableEqBorrowTree = Miri.TreeBorrows.instDecidableEqBorrowTree.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprBorrowTree : Repr BorrowTree

Equations

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

def Miri.TreeBorrows.instReprBorrowTree.repr : BorrowTree → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.DebugNameError : Type

• missingTag (tag : Memory.BorTag) : DebugNameError
• missingNode (index : UniIndex) : DebugNameError
• missingParent (tag : Memory.BorTag) (distance : Nat) : DebugNameError

def Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (x✝ x✝¹ : DebugNameError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingTag tag) (Miri.TreeBorrows.DebugNameError.missingNode index) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingTag tag) (Miri.TreeBorrows.DebugNameError.missingParent tag_1 distance) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingNode index) (Miri.TreeBorrows.DebugNameError.missingTag tag) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingNode index) (Miri.TreeBorrows.DebugNameError.missingParent tag distance) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingParent tag distance) (Miri.TreeBorrows.DebugNameError.missingTag tag_1) = isFalse ⋯
• Miri.TreeBorrows.instDecidableEqDebugNameError.decEq (Miri.TreeBorrows.DebugNameError.missingParent tag distance) (Miri.TreeBorrows.DebugNameError.missingNode index) = isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqDebugNameError : DecidableEq DebugNameError

Equations

• Miri.TreeBorrows.instDecidableEqDebugNameError = Miri.TreeBorrows.instDecidableEqDebugNameError.decEq

@[instance_reducible]

instance Miri.TreeBorrows.instReprDebugNameError : Repr DebugNameError

Equations

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

def Miri.TreeBorrows.instReprDebugNameError.repr : DebugNameError → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.BorrowTree.nthParent (tree : BorrowTree) (tag : Memory.BorTag) (distance : Nat) : Except DebugNameError Memory.BorTag

Source Tree::nth_parent, with malformed/exhausted ancestry retained as a checked machine error by diagnostic callers instead of an unchecked unwrap.

Equations

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

def Miri.TreeBorrows.BorrowTree.addDebugName (tree : BorrowTree) (tag : Memory.BorTag) (name : String) : Except DebugNameError BorrowTree

Source NodeDebugInfo::add_name: several names for one tag are joined with ", " in their insertion order.

Equations

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

def Miri.TreeBorrows.BorrowTree.givePointerDebugName (tree : BorrowTree) (tag : Memory.BorTag) (distance : Nat) (name : String) : Except DebugNameError BorrowTree

Source Tree::give_pointer_debug_name, including ancestor selection.

Equations

• tree.givePointerDebugName tag distance name = do let ancestor ← tree.nthParent tag distance tree.addDebugName ancestor name

def Miri.TreeBorrows.BorrowTree.new (rootTag : Memory.BorTag) (size : ABI.Size) : BorrowTree

Source Tree::new: disabled default at out-of-bounds/uninitialized locations, one non-exposed root, and an accessed Unique permission throughout the allocation's in-bounds bytes.

Equations

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

def Miri.TreeBorrows.BorrowTree.indexOfTag (tree : BorrowTree) (tag : Memory.BorTag) : Option UniIndex

Equations

• tree.indexOfTag tag = tree.tagMapping.get tag

def Miri.TreeBorrows.BorrowTree.nodeAt (tree : BorrowTree) (idx : UniIndex) : Option TreeNode

Equations

• tree.nodeAt idx = tree.nodes.get idx

def Miri.TreeBorrows.BorrowTree.locationStateAt (tree : BorrowTree) (location : LocationTree) (idx : UniIndex) : Option Tree.LocationState

Current or lazily initialized per-location state for a node.

Equations

• tree.locationStateAt location idx = do let node ← tree.nodeAt idx pure ((location.perms.get idx).getD node.defaultLocationState)

structure Miri.TreeBorrows.BorrowTree.NormalLocationAccessResult : Type

• location : LocationTree
• access : Tree.NormalAccessResult
• outcome : Except ExposedCacheError Unit

def Miri.TreeBorrows.BorrowTree.instDecidableEqNormalLocationAccessResult.decEq (x✝ x✝¹ : NormalLocationAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqNormalLocationAccessResult : DecidableEq NormalLocationAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqNormalLocationAccessResult = Miri.TreeBorrows.BorrowTree.instDecidableEqNormalLocationAccessResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprNormalLocationAccessResult : Repr NormalLocationAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprNormalLocationAccessResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprNormalLocationAccessResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprNormalLocationAccessResult.repr : NormalLocationAccessResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.BorrowTree.TreeMutationError : Type

• MissingTag (tag : Memory.BorTag) : TreeMutationError
• MissingNode (index : UniIndex) : TreeMutationError
• ExposedCache (error : ExposedCacheError) : TreeMutationError
• RangeMap (error : DataStructures.DedupRangeMapError) : TreeMutationError

def Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationError.decEq (x✝ x✝¹ : TreeMutationError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationError : DecidableEq TreeMutationError

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationError = Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationError.decEq

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprTreeMutationError : Repr TreeMutationError

Equations

• Miri.TreeBorrows.BorrowTree.instReprTreeMutationError = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprTreeMutationError.repr }

def Miri.TreeBorrows.BorrowTree.instReprTreeMutationError.repr : TreeMutationError → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.BorrowTree.TreeMutationResult : Type

• tree : BorrowTree
• outcome : Except TreeMutationError Unit

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationResult : DecidableEq TreeMutationResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationResult = Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationResult.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqTreeMutationResult.decEq (x✝ x✝¹ : TreeMutationResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprTreeMutationResult : Repr TreeMutationResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprTreeMutationResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprTreeMutationResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprTreeMutationResult.repr : TreeMutationResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.BorrowTree.ChildInsertError : Type

• DuplicateTag (tag : Memory.BorTag) : ChildInsertError
• TagIndexExhausted (active : Nat) : ChildInsertError
• MissingParentTag (tag : Memory.BorTag) : ChildInsertError
• OutsidePermissionNotInitial (permission : Permission) : ChildInsertError
• OutsideUniquePermission : ChildInsertError
• ProtectedReservedIM : ChildInsertError
• InsidePermissionNotInitial (permission : Permission) : ChildInsertError
• InsideSifaMismatch (permission : Permission) : ChildInsertError
• InsidePermissionInvariant (permission : Permission) : ChildInsertError
• SizeError (error : ABI.SizeError) : ChildInsertError
• RangeMapError (error : DataStructures.DedupRangeMapError) : ChildInsertError
• MissingNode (index : UniIndex) : ChildInsertError
• ParentCycle (index : UniIndex) : ChildInsertError

def Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertError.decEq (x✝ x✝¹ : ChildInsertError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertError : DecidableEq ChildInsertError

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertError = Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertError.decEq

def Miri.TreeBorrows.BorrowTree.instReprChildInsertError.repr : ChildInsertError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprChildInsertError : Repr ChildInsertError

Equations

• Miri.TreeBorrows.BorrowTree.instReprChildInsertError = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprChildInsertError.repr }

structure Miri.TreeBorrows.BorrowTree.ChildInsertResult : Type

• tree : BorrowTree
• outcome : Except ChildInsertError Unit

def Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertResult.decEq (x✝ x✝¹ : ChildInsertResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertResult : DecidableEq ChildInsertResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertResult = Miri.TreeBorrows.BorrowTree.instDecidableEqChildInsertResult.decEq

def Miri.TreeBorrows.BorrowTree.instReprChildInsertResult.repr : ChildInsertResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprChildInsertResult : Repr ChildInsertResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprChildInsertResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprChildInsertResult.repr }

inductive Miri.TreeBorrows.BorrowTree.TreeGcError : Type

• MissingNode (index : UniIndex) : TreeGcError
• MissingChildPosition (parent : UniIndex) (position : Nat) : TreeGcError
• MissingReplacementChild (index : UniIndex) : TreeGcError
• EmptyTraversalStack (root : UniIndex) : TreeGcError
• ParentCycle (root : UniIndex) : TreeGcError
• RangeMerge (error : DataStructures.DedupRangeMapError) : TreeGcError

def Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (x✝ x✝¹ : TreeGcError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.MissingNode index) (Miri.TreeBorrows.BorrowTree.TreeGcError.ParentCycle root) = isFalse ⋯
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.MissingNode index) (Miri.TreeBorrows.BorrowTree.TreeGcError.RangeMerge error) = isFalse ⋯
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.ParentCycle root) (Miri.TreeBorrows.BorrowTree.TreeGcError.MissingNode index) = isFalse ⋯
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.ParentCycle root) (Miri.TreeBorrows.BorrowTree.TreeGcError.RangeMerge error) = isFalse ⋯
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.RangeMerge error) (Miri.TreeBorrows.BorrowTree.TreeGcError.MissingNode index) = isFalse ⋯
• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq (Miri.TreeBorrows.BorrowTree.TreeGcError.RangeMerge error) (Miri.TreeBorrows.BorrowTree.TreeGcError.ParentCycle root) = isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError : DecidableEq TreeGcError

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError = Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcError.decEq

def Miri.TreeBorrows.BorrowTree.instReprTreeGcError.repr : TreeGcError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprTreeGcError : Repr TreeGcError

Equations

• Miri.TreeBorrows.BorrowTree.instReprTreeGcError = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprTreeGcError.repr }

structure Miri.TreeBorrows.BorrowTree.TreeGcResult : Type

• tree : BorrowTree
• outcome : Except TreeGcError Unit

def Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcResult.decEq (x✝ x✝¹ : TreeGcResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcResult : DecidableEq TreeGcResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcResult = Miri.TreeBorrows.BorrowTree.instDecidableEqTreeGcResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprTreeGcResult : Repr TreeGcResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprTreeGcResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprTreeGcResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprTreeGcResult.repr : TreeGcResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.BorrowTree.WildcardAccessStatus : Type

• Completed : WildcardAccessStatus
• EmptyTraversalStack (root : UniIndex) : WildcardAccessStatus
• NoValidExposedReferences (root : UniIndex) (node : Option UniIndex) : WildcardAccessStatus
• MissingNode (index : UniIndex) : WildcardAccessStatus
• RecordDebugAssertion (index : UniIndex) : WildcardAccessStatus
• TransitionError (index : UniIndex) (error : Diagnostics.TransitionError) : WildcardAccessStatus
• CacheFailure (error : ExposedCacheError) : WildcardAccessStatus
• PermissionInvariantFailure (index : UniIndex) : WildcardAccessStatus
• TransitionApplicationInvariantFailure (index : UniIndex) : WildcardAccessStatus
• PossibleInvariantFailure (index : UniIndex) : WildcardAccessStatus
• ParentCycle (root : UniIndex) : WildcardAccessStatus

def Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardAccessStatus.decEq (x✝ x✝¹ : WildcardAccessStatus) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardAccessStatus : DecidableEq WildcardAccessStatus

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardAccessStatus = Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardAccessStatus.decEq

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprWildcardAccessStatus : Repr WildcardAccessStatus

Equations

• Miri.TreeBorrows.BorrowTree.instReprWildcardAccessStatus = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprWildcardAccessStatus.repr }

def Miri.TreeBorrows.BorrowTree.instReprWildcardAccessStatus.repr : WildcardAccessStatus → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.BorrowTree.WildcardLocationAccessResult : Type

• location : LocationTree
• status : WildcardAccessStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardLocationAccessResult : DecidableEq WildcardLocationAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardLocationAccessResult = Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardLocationAccessResult.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqWildcardLocationAccessResult.decEq (x✝ x✝¹ : WildcardLocationAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprWildcardLocationAccessResult : Repr WildcardLocationAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprWildcardLocationAccessResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprWildcardLocationAccessResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprWildcardLocationAccessResult.repr : WildcardLocationAccessResult → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.BorrowTree.performWildcardAccessAt (tree : BorrowTree) (initialLocation : LocationTree) (root : UniIndex) (maxLocalTag : Option Memory.BorTag) (kind : AccessKind) (protectedTags : ProtectedTags) (isWildcardTree : Bool) : WildcardLocationAccessResult

Source LocationTree::perform_wildcard_access. The stack implements the source visitor's child-first, postorder traversal. Relatedness and SIFA skip decisions are recomputed against the cache as child transitions change it.

Equations

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

def Miri.TreeBorrows.BorrowTree.performNormalAccessAt (tree : BorrowTree) (location : LocationTree) (start : UniIndex) (kind : AccessKind) (protectedTags : ProtectedTags) (mode : Tree.ChildrenVisitMode) : NormalLocationAccessResult

Perform the source normal-tree component at one actual tree location. Permission transitions are delegated to NormalTreeState; this operation projects the source UniValMap topology and lazy defaults, writes state back to the real maps, and applies exposed-cache deltas in visit order. Additional wildcard roots are handled by the separate wildcard-access component.

Equations

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

def Miri.TreeBorrows.BorrowTree.exposeTag (tree : BorrowTree) (protectedTags : ProtectedTags) (tag : Memory.BorTag) : TreeMutationResult

Source Tree::expose_tag, including the per-range Willard-cache update. The global protected-tag table determines which local accesses remain valid through this exposed tag.

Equations

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

def Miri.TreeBorrows.BorrowTree.updateExposureForProtectorRelease (tree : BorrowTree) (tag : Memory.BorTag) : TreeMutationResult

Source update_exposure_for_protector_release: exposed nodes retain their exposure, while the cache counters change from protected to unprotected local permission strength.

Equations

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

def Miri.TreeBorrows.BorrowTree.newChild (tree : BorrowTree) (baseOffset : ABI.Size) (parentProvenance : Memory.ProvenanceExtra) (newTag : Memory.BorTag) (insidePermissions : DataStructures.DedupRangeMap Tree.LocationState) (outsidePermission : Permission) (isProtected : Bool) : ChildInsertResult

Source Tree::new_child: allocate the tag index, attach a concrete child or ordered wildcard root, store lazy defaults, materialize inside-range permissions, and weaken ancestor SIFAs until the retag invariant is restored. Mutation and invariant failures retain earlier source-ordered state changes.

Equations

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

def Miri.TreeBorrows.BorrowTree.provenanceTags (tree : BorrowTree) : Array Memory.BorTag

Tags reported by source VisitProvenance for Tree: all roots and every exposed node whose provenance may still permit an access.

Equations

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

def Miri.TreeBorrows.BorrowTree.removeUnreachableTags (tree : BorrowTree) (liveTags : Array Memory.BorTag) : TreeGcResult

Source Tree::remove_unreachable_tags: process each ordered root with postorder leaf removal and safe single-child collapse, then thoroughly merge adjacent equal location ranges.

Equations

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

structure Miri.TreeBorrows.BorrowTree.BorrowTreeLocationResult : Type

• range : DataStructures.ByteRange
• normalAccess : Option Tree.NormalAccessResult

def Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeLocationResult.decEq (x✝ x✝¹ : BorrowTreeLocationResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeLocationResult : DecidableEq BorrowTreeLocationResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeLocationResult = Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeLocationResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprBorrowTreeLocationResult : Repr BorrowTreeLocationResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprBorrowTreeLocationResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprBorrowTreeLocationResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprBorrowTreeLocationResult.repr : BorrowTreeLocationResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.BorrowTree.BorrowTreeAccessStatus : Type

• Completed : BorrowTreeAccessStatus
• MissingTag (tag : Memory.BorTag) : BorrowTreeAccessStatus
• MultipleRoots (count : Nat) : BorrowTreeAccessStatus
• RangeMapFailure (error : DataStructures.DedupRangeMapError) : BorrowTreeAccessStatus
• LocationMapFailure (range : DataStructures.ByteRange) (error : DataStructures.DedupRangeMapError) : BorrowTreeAccessStatus
• CacheFailure (range : DataStructures.ByteRange) (error : ExposedCacheError) : BorrowTreeAccessStatus
• AccessFailure (range : DataStructures.ByteRange) (status : Tree.NormalAccessStatus) : BorrowTreeAccessStatus
• WildcardFailure (range : DataStructures.ByteRange) (status : WildcardAccessStatus) : BorrowTreeAccessStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessStatus : DecidableEq BorrowTreeAccessStatus

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessStatus = Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessStatus.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessStatus.decEq (x✝ x✝¹ : BorrowTreeAccessStatus) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessStatus.repr : BorrowTreeAccessStatus → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessStatus : Repr BorrowTreeAccessStatus

Equations

• Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessStatus = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessStatus.repr }

structure Miri.TreeBorrows.BorrowTree.BorrowTreeAccessResult : Type

• tree : BorrowTree
• locations : Array BorrowTreeLocationResult
• status : BorrowTreeAccessStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessResult : DecidableEq BorrowTreeAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessResult = Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessResult.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeAccessResult.decEq (x✝ x✝¹ : BorrowTreeAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessResult : Repr BorrowTreeAccessResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprBorrowTreeAccessResult.repr : BorrowTreeAccessResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.BorrowTree.BorrowTreeDeallocStatus : Type

• Deallocated : BorrowTreeDeallocStatus
• AccessFailure (status : BorrowTreeAccessStatus) : BorrowTreeDeallocStatus
• MultipleRoots (count : Nat) : BorrowTreeDeallocStatus
• MissingTag (tag : Memory.BorTag) : BorrowTreeDeallocStatus
• RangeMapFailure (error : DataStructures.DedupRangeMapError) : BorrowTreeDeallocStatus
• ProtectedDealloc (range : DataStructures.ByteRange) (node : UniIndex) : BorrowTreeDeallocStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocStatus : DecidableEq BorrowTreeDeallocStatus

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocStatus = Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocStatus.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocStatus.decEq (x✝ x✝¹ : BorrowTreeDeallocStatus) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocStatus : Repr BorrowTreeDeallocStatus

Equations

• Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocStatus = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocStatus.repr }

def Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocStatus.repr : BorrowTreeDeallocStatus → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.BorrowTree.BorrowTreeDeallocResult : Type

• tree : BorrowTree
• status : BorrowTreeDeallocStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocResult : DecidableEq BorrowTreeDeallocResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocResult = Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocResult.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqBorrowTreeDeallocResult.decEq (x✝ x✝¹ : BorrowTreeDeallocResult) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocResult.repr : BorrowTreeDeallocResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocResult : Repr BorrowTreeDeallocResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprBorrowTreeDeallocResult.repr }

def Miri.TreeBorrows.BorrowTree.performBorrowAccessRange (tree : BorrowTree) (provenance : Memory.ProvenanceExtra) (offset length : ABI.Size) (kind : AccessKind) (protectedTags : ProtectedTags) (mode : Tree.ChildrenVisitMode) : BorrowTreeAccessResult

Ranged access for concrete or wildcard provenance. Tree state and Willard-cache updates are threaded across homogeneous range segments and all ordered roots.

Equations

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

def Miri.TreeBorrows.BorrowTree.performNormalAccessRange (tree : BorrowTree) (tag : Memory.BorTag) (offset length : ABI.Size) (kind : AccessKind) (protectedTags : ProtectedTags) (mode : Tree.ChildrenVisitMode) : BorrowTreeAccessResult

Concrete-tag convenience wrapper over the full source-root access path.

Equations

• tree.performNormalAccessRange tag offset length kind protectedTags mode = tree.performBorrowAccessRange (Miri.Memory.ProvenanceExtra.concrete tag) offset length kind protectedTags mode

inductive Miri.TreeBorrows.BorrowTree.ProtectorReleaseStatus : Type

• Released : ProtectorReleaseStatus
• MissingTag (tag : Memory.BorTag) : ProtectorReleaseStatus
• RangeMapFailure (error : DataStructures.DedupRangeMapError) : ProtectorReleaseStatus
• LocationMapFailure (error : DataStructures.DedupRangeMapError) : ProtectorReleaseStatus
• AccessFailure (range : DataStructures.ByteRange) (status : BorrowTreeAccessStatus) : ProtectorReleaseStatus
• ExposureUpdateFailure (error : TreeMutationError) : ProtectorReleaseStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseStatus : DecidableEq ProtectorReleaseStatus

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseStatus = Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseStatus.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseStatus.decEq (x✝ x✝¹ : ProtectorReleaseStatus) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseStatus : Repr ProtectorReleaseStatus

Equations

• Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseStatus = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseStatus.repr }

def Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseStatus.repr : ProtectorReleaseStatus → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.BorrowTree.ProtectorReleaseResult : Type

• tree : BorrowTree
• status : ProtectorReleaseStatus

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseResult : DecidableEq ProtectorReleaseResult

Equations

• Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseResult = Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseResult.decEq

def Miri.TreeBorrows.BorrowTree.instDecidableEqProtectorReleaseResult.decEq (x✝ x✝¹ : ProtectorReleaseResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseResult : Repr ProtectorReleaseResult

Equations

• Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseResult = { reprPrec := Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseResult.repr }

def Miri.TreeBorrows.BorrowTree.instReprProtectorReleaseResult.repr : ProtectorReleaseResult → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.BorrowTree.releaseProtector (tree : BorrowTree) (tag : Memory.BorTag) (protectedTags : ProtectedTags) : ProtectorReleaseResult

Source Tree::perform_protector_end_access followed by update_exposure_for_protector_release. The tag remains protected during its implicit accessed-location read/write, and the caller removes the global protector only after this operation succeeds.

Equations

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

def Miri.TreeBorrows.BorrowTree.deallocateBorrowRange (tree : BorrowTree) (provenance : Memory.ProvenanceExtra) (offset length : ABI.Size) (protectedTags : ProtectedTags) : BorrowTreeDeallocResult

Source Tree::dealloc for a single concrete root: first perform the write through the supplied tag, then inspect visited nodes in source tree-visitor order for accessed strong protectors. Cell permissions are exempt. Weak protectors are handled by the initial write transition itself.

Equations

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

def Miri.TreeBorrows.BorrowTree.deallocateRange (tree : BorrowTree) (tag : Memory.BorTag) (offset length : ABI.Size) (protectedTags : ProtectedTags) : BorrowTreeDeallocResult

Concrete-tag convenience wrapper for source Tree::dealloc.

Equations

• tree.deallocateRange tag offset length protectedTags = tree.deallocateBorrowRange (Miri.Memory.ProvenanceExtra.concrete tag) offset length protectedTags

@[simp]

theorem Miri.TreeBorrows.BorrowTree.new_root_node (rootTag : Memory.BorTag) (size : ABI.Size) : (new rootTag size).nodes.get { idx := 0 } = some { tag := rootTag, parent := none, defaultInitialPermission := Permission.newDisabled, defaultInitialSifa := IdempotentForeignAccess.None }

@[simp]

theorem Miri.TreeBorrows.BorrowTree.new_root_is_only_tree_root (rootTag : Memory.BorTag) (size : ABI.Size) : (new rootTag size).roots = #[{ idx := 0 }]

theorem Miri.TreeBorrows.BorrowTree.new_one_byte_root_is_accessed_unique : Option.map (fun (segment : DataStructures.RangeMapSegment LocationTree) => segment.data.perms.get { idx := 0 }) (new Memory.BorTag.one (ABI.Size.ofBytes 1)).locations.iterAll[0]? = some (some { permission := Permission.Unique, accessed := true, idempotentForeignAccess := IdempotentForeignAccess.None })

Zero-byte protected child construction from finite graph and allocator invariants. These proof-only declarations do not change the interpreter. The rank and loop lemmas are adapted from PR35/38 generic Tree Borrows proofs.

def Miri.TreeBorrows.BorrowTree.ZeroProtection.tacticName_ancestor_loop : Lean.ParserDescr

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.loop_invariant {β : Type} (scan : Unit → β → Id (ForInStep β)) (measure : β → Nat) (property : β → Prop) (step : ∀ (state : β), property state → (∃ (final : β), scan () state = ForInStep.done final ∧ property final) ∨ ∃ (next : β), scan () state = ForInStep.yield next ∧ property next ∧ measure next < measure state) (initial : β) (valid : property initial) : property ({ }.forIn initial scan)

A source while-loop invariant with a well-founded data measure.

structure Miri.TreeBorrows.BorrowTree.ZeroProtection.ParentDepth (nodes : UniValMap TreeNode) : Type

• depth : UniIndex → Nat
• bounded (index : UniIndex) (node : TreeNode) : nodes.get index = some node → self.depth index ≤ nodes.size
• parent (index : UniIndex) (node : TreeNode) : nodes.get index = some node → ∀ (before : UniIndex), node.parent = some before → ∃ (earlier : TreeNode), nodes.get before = some earlier ∧ self.depth before < self.depth index

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.index_injective (left right : UniIndex) (same : left.toNat = right.toNat) : left = right

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.lookup_valid {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (present : nodes.get index = some value) : index.toNat < nodes.data.size

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.insert_existing {α : Type} (nodes : UniValMap α) (index : UniIndex) (old next : α) (present : nodes.get index = some old) : (nodes.insert index next).data = nodes.data.set index.toNat (some next) ⋯

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.insert_existing_get_same {α : Type} (nodes : UniValMap α) (index : UniIndex) (old next : α) (present : nodes.get index = some old) : (nodes.insert index next).get index = some next

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.insert_existing_get_other {α : Type} (nodes : UniValMap α) (index query : UniIndex) (old next : α) (present : nodes.get index = some old) (different : query ≠ index) : (nodes.insert index next).get query = nodes.get query

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.insert_existing_size {α : Type} (nodes : UniValMap α) (index : UniIndex) (old next : α) (present : nodes.get index = some old) : (nodes.insert index next).size = nodes.size

def Miri.TreeBorrows.BorrowTree.ZeroProtection.update_depth (nodes : UniValMap TreeNode) (depth : ParentDepth nodes) (index : UniIndex) (old next : TreeNode) (present : nodes.get index = some old) (sameParent : next.parent = old.parent) : ParentDepth (nodes.insert index next)

Changing non-parent node metadata preserves the real exposed-cache ancestor certificate and its depth function.

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.update_depth nodes depth index old next present sameParent = { depth := depth.depth, bounded := ⋯, parent := ⋯ }

@[reducible, inline]

abbrev Miri.TreeBorrows.BorrowTree.ZeroProtection.LoopState : Type

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.weakened (tree : BorrowTree) (index : UniIndex) (node : TreeNode) (strongest : IdempotentForeignAccess) : BorrowTree

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.changed (tree : BorrowTree) (index : UniIndex) (node : TreeNode) (strongest : IdempotentForeignAccess) : Bool

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Good (depth : UniIndex → Nat) (state : LoopState) : Prop

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Measure (depth : UniIndex → Nat) (state : LoopState) : Nat

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.succeeds (tree : BorrowTree) (depth : ParentDepth tree.nodes) (start : UniIndex) (node : TreeNode) (present : tree.nodes.get start = some node) (strict : depth.depth start < tree.nodes.size) (strongest : IdempotentForeignAccess) : (Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ tree start strongest).snd = Except.ok ()

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.insert_append {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (atEnd : index.toNat = nodes.data.size) : (nodes.insert index value).data = nodes.data.push (some value)

The append-index branch of the actual newChild node insertion. Existing node data and parent depth are arbitrary; free-index reuse is a separate case.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.append_size {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (atEnd : index.toNat = nodes.data.size) : (nodes.insert index value).size = nodes.size + 1

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.append_get_same {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (atEnd : index.toNat = nodes.data.size) : (nodes.insert index value).get index = some value

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.append_get_other {α : Type} (nodes : UniValMap α) (index query : UniIndex) (value : α) (atEnd : index.toNat = nodes.data.size) (different : query ≠ index) : (nodes.insert index value).get query = nodes.get query

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.append_depth (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (atEnd : index.toNat = nodes.data.size) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) : ParentDepth (nodes.insert index newNode)

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.attachedNodes (nodes : UniValMap TreeNode) (index parent : UniIndex) (parentNode newNode : TreeNode) : UniValMap TreeNode

The second source-ordered node insertion in newChild attaches the new index to its parent's children, without changing either node's parent link.

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.parent_not_fresh (nodes : UniValMap TreeNode) (index parent : UniIndex) (parentNode : TreeNode) (atEnd : index.toNat = nodes.data.size) (parentPresent : nodes.get parent = some parentNode) : parent ≠ index

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.attached_depth (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (atEnd : index.toNat = nodes.data.size) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) : ParentDepth (attachedNodes nodes index parent parentNode newNode)

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.attached_parent_strict (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (atEnd : index.toNat = nodes.data.size) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) : (attached_depth nodes before index parent parentNode newNode atEnd parentPresent childParent).depth parent < (attachedNodes nodes index parent parentNode newNode).size

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Append.sifa_after_attach (tree : BorrowTree) (before : ParentDepth tree.nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (atEnd : index.toNat = tree.nodes.data.size) (parentPresent : tree.nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) (strongest : IdempotentForeignAccess) : (Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ { tagMapping := tree.tagMapping, nodes := attachedNodes tree.nodes index parent parentNode newNode, locations := tree.locations, roots := tree.roots } parent strongest).snd = Except.ok ()

The real ancestor-SIFA stage invoked by newChild succeeds after its two actual node insertions. The new index and original parent's presence are data conditions; no successful child insertion or SIFA update is a premise.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Sparse.extend_get {α : Type} (map : UniValMap α) (length : Nat) (index : UniIndex) : { data := UniValMap.extendTo map.data length }.get index = map.get index

Extending a sparse location map with absent entries preserves every lookup, including queries beyond both its old and new extents.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Sparse.get_same {α : Type} (map : UniValMap α) (index : UniIndex) (value : α) : (map.insert index value).get index = some value

The actual sparse-map insertion stores the new child's materialized state.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Sparse.get_other {α : Type} (map : UniValMap α) (index query : UniIndex) (value : α) (different : query ≠ index) : (map.insert index value).get query = map.get query

Inserting the new child state preserves every other node's state even when the per-location sparse array has a different length from the node table.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.insert_bounded {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (valid : index.toNat < nodes.data.size) : (nodes.insert index value).data = nodes.data.set index.toNat (some value) valid

Insertion at a bounded sparse slot retains the table length. Vacancy is a separate caller condition: this operation itself also permits overwriting.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.bounded_size {α : Type} (nodes : UniValMap α) (index : UniIndex) (value : α) (valid : index.toNat < nodes.data.size) : (nodes.insert index value).size = nodes.size

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.parent_not_vacant (nodes : UniValMap TreeNode) (index parent : UniIndex) (parentNode : TreeNode) (vacant : nodes.get index = none) (parentPresent : nodes.get parent = some parentNode) : parent ≠ index

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.vacant_depth (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (valid : index.toNat < nodes.data.size) (vacant : nodes.get index = none) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) (parentSlack : before.depth parent < nodes.size) : ParentDepth (nodes.insert index newNode)

A bounded vacant slot can hold a fresh child. The explicit rank slack ensures the child's parent-rank-plus-one fits without enlarging the table. Every old parent edge remains valid; none can point to the vacant slot.

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.attached_depth (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (valid : index.toNat < nodes.data.size) (vacant : nodes.get index = none) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) (parentSlack : before.depth parent < nodes.size) : ParentDepth (Append.attachedNodes nodes index parent parentNode newNode)

Both source node insertions preserve the depth certificate on a reusable slot. No absence of per-location permissions is inferred from node vacancy.

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.attached_parent_strict (nodes : UniValMap TreeNode) (before : ParentDepth nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (valid : index.toNat < nodes.data.size) (vacant : nodes.get index = none) (parentPresent : nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) (parentSlack : before.depth parent < nodes.size) : (attached_depth nodes before index parent parentNode newNode valid vacant parentPresent childParent parentSlack).depth parent < (Append.attachedNodes nodes index parent parentNode newNode).size

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Reuse.sifa_after_attach (tree : BorrowTree) (before : ParentDepth tree.nodes) (index parent : UniIndex) (parentNode newNode : TreeNode) (valid : index.toNat < tree.nodes.data.size) (vacant : tree.nodes.get index = none) (parentPresent : tree.nodes.get parent = some parentNode) (childParent : newNode.parent = some parent) (parentSlack : before.depth parent < tree.nodes.size) (strongest : IdempotentForeignAccess) : (Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ { tagMapping := tree.tagMapping, nodes := Append.attachedNodes tree.nodes index parent parentNode newNode, locations := tree.locations, roots := tree.roots } parent strongest).snd = Except.ok ()

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.concrete_child (tree : BorrowTree) (depth : ParentDepth tree.nodes) (parentTag tag : Memory.BorTag) (parent : UniIndex) (parentNode : TreeNode) (tagged : tree.tagMapping.get parentTag = some parent) (present : tree.nodes.get parent = some parentNode) (fresh : tree.tagMapping.get tag = none) (room : tree.tagMapping.mapping.size ≤ 4294967295) (appendAligned : tree.tagMapping.deassigned.back? = none → tree.tagMapping.mapping.size = tree.nodes.size) (reuseValid : ∀ (index : UniIndex), tree.tagMapping.deassigned.back? = some index → index.toNat < tree.nodes.size ∧ tree.nodes.get index = none) (rank : depth.depth parent < tree.nodes.size) (offset : ABI.Size) (initial : Tree.LocationState) : ∃ (after : BorrowTree), tree.newChild offset (Memory.ProvenanceExtra.concrete parentTag) tag (DataStructures.DedupRangeMap.new ABI.Size.ZERO initial) (Permission.ReservedFrz false) true = { tree := after, outcome := Except.ok () }

Both concrete allocation branches of a zero-byte protected child complete from raw parent, allocator and acyclic-graph facts.

@[reducible, inline]

abbrev Miri.TreeBorrows.BorrowTree.ZeroProtection.View.StateShape : Type

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.StateShape = (Miri.TreeBorrows.Permission × Bool)

@[reducible, inline]

abbrev Miri.TreeBorrows.BorrowTree.ZeroProtection.View.NodeShape : Type

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.NodeShape = (Miri.Memory.BorTag × Option Miri.TreeBorrows.UniIndex × Array Miri.TreeBorrows.UniIndex × Miri.TreeBorrows.Permission × Bool)

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.stateShape (state : Tree.LocationState) : StateShape

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.stateShape state = (state.permission, state.accessed)

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.nodeShape (node : TreeNode) : NodeShape

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.nodeShape node = (node.tag, node.parent, node.children, node.defaultInitialPermission, node.isExposed)

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.locationShape (location : LocationTree) : Array (Option StateShape)

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.locationShape location = Array.map (Option.map Miri.TreeBorrows.BorrowTree.ZeroProtection.View.stateShape) location.perms.data

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.treeShape (tree : BorrowTree) : UniKeyMap Memory.BorTag × Array (Option NodeShape) × Array (DataStructures.ByteRange × Array (Option StateShape)) × Array UniIndex

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.insert_existing_shape {α β : Type} (shape : α → β) (nodes : UniValMap α) (index : UniIndex) (old next : α) (present : nodes.get index = some old) (same : shape next = shape old) : Array.map (Option.map shape) (nodes.insert index next).data = Array.map (Option.map shape) nodes.data

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.weakenLocation (location : LocationTree) (index : UniIndex) (strongest : IdempotentForeignAccess) : LocationTree

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.weaken_location_shape (location : LocationTree) (index : UniIndex) (strongest : IdempotentForeignAccess) : locationShape (weakenLocation location index strongest) = locationShape location

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.weakened_tree_shape (tree : BorrowTree) (index : UniIndex) (node : TreeNode) (present : tree.nodes.get index = some node) (strongest : IdempotentForeignAccess) : treeShape (weakened tree index node strongest) = treeShape tree

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.Preserves (before : BorrowTree) (state : LoopState) : Prop

Equations

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

def Miri.TreeBorrows.BorrowTree.ZeroProtection.View.Measure (state : LoopState) : Nat

Equations

• Miri.TreeBorrows.BorrowTree.ZeroProtection.View.Measure state = if state.snd.snd.snd.snd = true then state.snd.fst.nodes.size + 1 - state.snd.snd.snd.fst + 1 else 0

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.preserves (tree : BorrowTree) (start : UniIndex) (strongest : IdempotentForeignAccess) : treeShape (Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ tree start strongest).fst = treeShape tree

Even an error result changes no tag/topology/permission/accessed data in this SIFA-only stage. This metadata fact is not an assertion of safe execution.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.mapped_lookup {A B : Type} (shape : A → B) (nodes : UniValMap A) (index : UniIndex) : (Array.map (Option.map shape) nodes.data)[index.toNat]?.getD none = Option.map shape (nodes.get index)

Sparse lookup commutes with the observable metadata projection.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.node_fields (before after : BorrowTree) (same : treeShape after = treeShape before) (index : UniIndex) (node : TreeNode) (present : before.nodes.get index = some node) : ∃ (result : TreeNode), after.nodes.get index = some result ∧ result.tag = node.tag ∧ result.isExposed = node.isExposed

In particular, SIFA weakening preserves any fresh node's tag and exposure.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.View.absent_permissions (before after : BorrowTree) (same : treeShape after = treeShape before) (index : UniIndex) (absent : ∀ (position : Nat) (valid : position < before.locations.entries.size), before.locations.entries[position].data.perms.get index = none) (position : Nat) (valid : position < after.locations.entries.size) : after.locations.entries[position].data.perms.get index = none

An index absent from every location remains absent after SIFA weakening; we do not assume that physical node vacancy alone implies permission vacancy.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.index_exact {A : Type} (map : DataStructures.DedupRangeMap A) (position : Nat) (valid : position < map.entries.size) : map.index position = Except.ok map.entries[position]

An in-range raw range-map index always supplies its actual stored segment.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.list_tail {α β : Type} (items : List α) (scan : α → β → Id (ForInStep β)) (property : List α → β → Prop) (initial : β) (good : property items initial) (distinct : items.Nodup) (step : ∀ (item : α) (rest : List α), ¬item ∈ rest → ∀ (state : β), property (item :: rest) state → ∃ (next : β), scan item state = ForInStep.yield next ∧ property rest next) : property [] (forIn items initial scan)

def Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.tacticName_fresh_release_scan : Lean.ParserDescr

Equations

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

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.release (tree : BorrowTree) (tag : Memory.BorTag) (index : UniIndex) (node : TreeNode) (tagged : tree.indexOfTag tag = some index) (present : tree.nodeAt index = some node) (unexposed : node.isExposed = false) (absent : ∀ (position : Nat) (valid : position < tree.locations.entries.size), tree.locations.entries[position].data.perms.get index = none) (protections : ProtectedTags) : tree.releaseProtector tag protections = { tree := tree, status := ProtectorReleaseStatus.Released }

Releasing an unexposed zero-sized reservation with no materialized states really scans all allocation locations, skips each absent permission, and returns Released. Existing roots, ranges and exposure caches are preserved.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.after_sifa (tree : BorrowTree) (tag : Memory.BorTag) (index start : UniIndex) (node : TreeNode) (strongest : IdempotentForeignAccess) (tagged : tree.indexOfTag tag = some index) (present : tree.nodes.get index = some node) (unexposed : node.isExposed = false) (absent : ∀ (position : Nat) (valid : position < tree.locations.entries.size), tree.locations.entries[position].data.perms.get index = none) (protections : ProtectedTags) : have after := (Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ tree start strongest).fst; after.releaseProtector tag protections = { tree := after, status := ProtectorReleaseStatus.Released }

The ancestor SIFA stage preserves the exact facts needed to release a fresh, lazy, unexposed child, including on every existing byte partition.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.concrete_zero_eq (tree : BorrowTree) (parentTag tag : Memory.BorTag) (index parent : UniIndex) (parentNode : TreeNode) (mapping : UniKeyMap Memory.BorTag) (inserted : tree.tagMapping.insert tag = UniKeyMapInsertResult.Inserted mapping index) (tagged : tree.tagMapping.get parentTag = some parent) (present : tree.nodes.get parent = some parentNode) (vacant : tree.nodes.get index = none) (offset : ABI.Size) (initial : Tree.LocationState) : have node := { tag := tag, parent := some parent, defaultInitialPermission := Permission.ReservedFrz false, defaultInitialSifa := IdempotentForeignAccess.None }; have staged := { tagMapping := mapping, nodes := Append.attachedNodes tree.nodes index parent parentNode node, locations := tree.locations, roots := tree.roots }; have result := Miri.TreeBorrows.BorrowTree.updateSifaAfterRetag✝ staged parent IdempotentForeignAccess.None; tree.newChild offset (Memory.ProvenanceExtra.concrete parentTag) tag (DataStructures.DedupRangeMap.new ABI.Size.ZERO initial) (Permission.ReservedFrz false) true = { tree := result.fst, outcome := result.snd }

Implementation-facing source equation for a concrete zero child. The insertion equation is discharged from raw freshness/pool data by clients.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.concrete_zero_release (tree : BorrowTree) (parentTag tag : Memory.BorTag) (index parent : UniIndex) (parentNode : TreeNode) (mapping : UniKeyMap Memory.BorTag) (inserted : tree.tagMapping.insert tag = UniKeyMapInsertResult.Inserted mapping index) (tagged : tree.tagMapping.get parentTag = some parent) (present : tree.nodes.get parent = some parentNode) (vacant : tree.nodes.get index = none) (newTag : mapping.get tag = some index) (absent : ∀ (position : Nat) (valid : position < tree.locations.entries.size), tree.locations.entries[position].data.perms.get index = none) (offset : ABI.Size) (initial : Tree.LocationState) (protections : ProtectedTags) : have after := (tree.newChild offset (Memory.ProvenanceExtra.concrete parentTag) tag (DataStructures.DedupRangeMap.new ABI.Size.ZERO initial) (Permission.ReservedFrz false) true).tree; after.releaseProtector tag protections = { tree := after, status := ProtectorReleaseStatus.Released }

The freshly inserted concrete zero child can be released without changing its post-constructor tree. Initial node vacancy and permission vacancy are separate facts; no release or byte-access success is assumed.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.wildcard_zero_eq (tree : BorrowTree) (tag : Memory.BorTag) (index : UniIndex) (mapping : UniKeyMap Memory.BorTag) (inserted : tree.tagMapping.insert tag = UniKeyMapInsertResult.Inserted mapping index) (offset : ABI.Size) (initial : Tree.LocationState) : tree.newChild offset Memory.ProvenanceExtra.wildcard tag (DataStructures.DedupRangeMap.new ABI.Size.ZERO initial) (Permission.ReservedFrz false) true = { tree := { tagMapping := mapping, nodes := tree.nodes.insert index { tag := tag, parent := none, defaultInitialPermission := Permission.ReservedFrz false, defaultInitialSifa := IdempotentForeignAccess.None }, locations := tree.locations, roots := tree.roots.push index }, outcome := Except.ok () }

Exact lazy-root result for the wildcard zero-size source constructor.

theorem Miri.TreeBorrows.BorrowTree.ZeroProtection.Release.wildcard_zero_release (tree : BorrowTree) (tag : Memory.BorTag) (index : UniIndex) (mapping : UniKeyMap Memory.BorTag) (inserted : tree.tagMapping.insert tag = UniKeyMapInsertResult.Inserted mapping index) (newTag : mapping.get tag = some index) (absent : ∀ (position : Nat) (valid : position < tree.locations.entries.size), tree.locations.entries[position].data.perms.get index = none) (offset : ABI.Size) (initial : Tree.LocationState) (protections : ProtectedTags) : have after := (tree.newChild offset Memory.ProvenanceExtra.wildcard tag (DataStructures.DedupRangeMap.new ABI.Size.ZERO initial) (Permission.ReservedFrz false) true).tree; after.releaseProtector tag protections = { tree := after, status := ProtectorReleaseStatus.Released }

Ending the fresh wildcard-root protector leaves its zero-size constructor result unchanged. Node vacancy and permission vacancy are kept independent.

theorem Miri.TreeBorrows.BorrowTree.fresh_root_full_write (tag : Memory.BorTag) (size : ABI.Size) (protectedTags : ProtectedTags) : have result := (new tag size).performBorrowAccessRange (Memory.ProvenanceExtra.concrete tag) ABI.Size.ZERO size AccessKind.Write protectedTags Tree.ChildrenVisitMode.VisitChildrenOfAccessed; result.status = BorrowTreeAccessStatus.Completed ∧ result.tree = new tag size

The actual first full-range write on fresh allocation-owned provenance. The existing global protector map is arbitrary.