Allocation-range iteration for the normal one-root Tree Borrows slice. Each deduplicated range stores the lazily materialized per-node states for one location, and each selected range gets the normal-tree visitor transition. Wildcard roots, exposed-pointer state, diagnostics, and protector lifecycle remain outside this model.

structure Miri.TreeBorrows.Tree.RangedNormalTreeState : Type

Normal-tree state partitioned over allocation byte ranges. Each range's payload contains one optional state per tree node, matching lazy LocationTree.perms initialization at that location.

• topology : TraversalTree
• defaultStates : Array LocationState
• protectedNodes : List Nat
• locations : DataStructures.DedupRangeMap (Array (Option LocationState))

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqRangedNormalTreeState : DecidableEq RangedNormalTreeState

Equations

• Miri.TreeBorrows.Tree.instDecidableEqRangedNormalTreeState = Miri.TreeBorrows.Tree.instDecidableEqRangedNormalTreeState.decEq

def Miri.TreeBorrows.Tree.instDecidableEqRangedNormalTreeState.decEq (x✝ x✝¹ : RangedNormalTreeState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprRangedNormalTreeState : Repr RangedNormalTreeState

Equations

• Miri.TreeBorrows.Tree.instReprRangedNormalTreeState = { reprPrec := Miri.TreeBorrows.Tree.instReprRangedNormalTreeState.repr }

def Miri.TreeBorrows.Tree.instReprRangedNormalTreeState.repr : RangedNormalTreeState → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.Tree.RangedNormalTreeState.new (size : ABI.Size) (topology : TraversalTree) (defaultStates : Array LocationState) (protectedNodes : List Nat) (initialStates : Array (Option LocationState)) : RangedNormalTreeState

Equations

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

def Miri.TreeBorrows.Tree.RangedNormalTreeState.singletonCell : RangedNormalTreeState

One-byte, one-node Cell state used for a small end-to-end ranged access contract.

Equations

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

structure Miri.TreeBorrows.Tree.RangedLocationResult : Type

One tree access result for one deduplicated location interval.

• range : DataStructures.ByteRange
• result : NormalAccessResult

def Miri.TreeBorrows.Tree.instDecidableEqRangedLocationResult.decEq (x✝ x✝¹ : RangedLocationResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqRangedLocationResult : DecidableEq RangedLocationResult

Equations

• Miri.TreeBorrows.Tree.instDecidableEqRangedLocationResult = Miri.TreeBorrows.Tree.instDecidableEqRangedLocationResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprRangedLocationResult : Repr RangedLocationResult

Equations

• Miri.TreeBorrows.Tree.instReprRangedLocationResult = { reprPrec := Miri.TreeBorrows.Tree.instReprRangedLocationResult.repr }

def Miri.TreeBorrows.Tree.instReprRangedLocationResult.repr : RangedLocationResult → Nat → Std.Format

Equations

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

inductive Miri.TreeBorrows.Tree.RangedAccessStatus : Type

Status from mutating the selected range partition and applying each per-location tree transition in source order.

• Completed : RangedAccessStatus
• RangeMapFailure (error : DataStructures.DedupRangeMapError) : RangedAccessStatus
• LocationMapFailure (range : DataStructures.ByteRange) (error : DataStructures.DedupRangeMapError) : RangedAccessStatus
• AccessFailure (range : DataStructures.ByteRange) (status : NormalAccessStatus) : RangedAccessStatus

def Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus.decEq (x✝ x✝¹ : RangedAccessStatus) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus.decEq Miri.TreeBorrows.Tree.RangedAccessStatus.Completed Miri.TreeBorrows.Tree.RangedAccessStatus.Completed = isTrue ⋯
• Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus.decEq Miri.TreeBorrows.Tree.RangedAccessStatus.Completed (Miri.TreeBorrows.Tree.RangedAccessStatus.RangeMapFailure error) = isFalse ⋯
• Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus.decEq (Miri.TreeBorrows.Tree.RangedAccessStatus.RangeMapFailure error) Miri.TreeBorrows.Tree.RangedAccessStatus.Completed = isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus : DecidableEq RangedAccessStatus

Equations

• Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus = Miri.TreeBorrows.Tree.instDecidableEqRangedAccessStatus.decEq

def Miri.TreeBorrows.Tree.instReprRangedAccessStatus.repr : RangedAccessStatus → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprRangedAccessStatus : Repr RangedAccessStatus

Equations

• Miri.TreeBorrows.Tree.instReprRangedAccessStatus = { reprPrec := Miri.TreeBorrows.Tree.instReprRangedAccessStatus.repr }

structure Miri.TreeBorrows.Tree.RangedAccessResult : Type

Updated partition, visited location intervals (including a failing one), and first failure.

• state : RangedNormalTreeState
• locations : Array RangedLocationResult
• status : RangedAccessStatus

def Miri.TreeBorrows.Tree.instDecidableEqRangedAccessResult.decEq (x✝ x✝¹ : RangedAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqRangedAccessResult : DecidableEq RangedAccessResult

Equations

• Miri.TreeBorrows.Tree.instDecidableEqRangedAccessResult = Miri.TreeBorrows.Tree.instDecidableEqRangedAccessResult.decEq

def Miri.TreeBorrows.Tree.instReprRangedAccessResult.repr : RangedAccessResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprRangedAccessResult : Repr RangedAccessResult

Equations

• Miri.TreeBorrows.Tree.instReprRangedAccessResult = { reprPrec := Miri.TreeBorrows.Tree.instReprRangedAccessResult.repr }

def Miri.TreeBorrows.Tree.RangedNormalTreeState.performAccessRange (state : RangedNormalTreeState) (offset length : ABI.Size) (start : Nat) (kind : AccessKind) (mode : ChildrenVisitMode) : RangedAccessResult

Apply one normal-tree access to every deduplicated range in the requested byte interval. The range map performs its eager split/merge preparation first; then each selected payload is updated in order. A per-location error retains that interval's partial tree changes and stops the remaining range loop.

Equations

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