Finite tree-visitor schedule from pinned Miri tree_borrows/tree_visitor.rs. This models the normal-tree visitation order and the precise local/foreign relation used at each node. A tree is assumed to be a valid finite rooted tree, as it is at Miri's visitor call sites. Allocation ranges, wildcard subtrees, exposed caches, and diagnostics are outside this traversal schedule.

inductive Miri.TreeBorrows.Tree.ChildrenVisitMode : Type

Whether to visit the accessed node's direct children.

• VisitChildrenOfAccessed : ChildrenVisitMode
• SkipChildrenOfAccessed : ChildrenVisitMode

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqChildrenVisitMode : DecidableEq ChildrenVisitMode

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprChildrenVisitMode : Repr ChildrenVisitMode

Equations

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

def Miri.TreeBorrows.Tree.instReprChildrenVisitMode.repr : ChildrenVisitMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instInhabitedChildrenVisitMode : Inhabited ChildrenVisitMode

Equations

• Miri.TreeBorrows.Tree.instInhabitedChildrenVisitMode = { default := Miri.TreeBorrows.Tree.instInhabitedChildrenVisitMode.default }

structure Miri.TreeBorrows.Tree.TraversalNode : Type

Ordered parent/child links used by Miri's normal tree visitor.

• parent : Option Nat
• children : List Nat

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqTraversalNode : DecidableEq TraversalNode

Equations

• Miri.TreeBorrows.Tree.instDecidableEqTraversalNode = Miri.TreeBorrows.Tree.instDecidableEqTraversalNode.decEq

def Miri.TreeBorrows.Tree.instDecidableEqTraversalNode.decEq (x✝ x✝¹ : TraversalNode) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.Tree.instReprTraversalNode.repr : TraversalNode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprTraversalNode : Repr TraversalNode

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instInhabitedTraversalNode : Inhabited TraversalNode

Equations

• Miri.TreeBorrows.Tree.instInhabitedTraversalNode = { default := Miri.TreeBorrows.Tree.instInhabitedTraversalNode.default }

structure Miri.TreeBorrows.Tree.TraversalTree : Type

A finite tree indexed by its node positions.

• nodes : Array TraversalNode

def Miri.TreeBorrows.Tree.instDecidableEqTraversalTree.decEq (x✝ x✝¹ : TraversalTree) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqTraversalTree : DecidableEq TraversalTree

Equations

• Miri.TreeBorrows.Tree.instDecidableEqTraversalTree = Miri.TreeBorrows.Tree.instDecidableEqTraversalTree.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprTraversalTree : Repr TraversalTree

Equations

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

def Miri.TreeBorrows.Tree.instReprTraversalTree.repr : TraversalTree → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instInhabitedTraversalTree : Inhabited TraversalTree

Equations

• Miri.TreeBorrows.Tree.instInhabitedTraversalTree = { default := Miri.TreeBorrows.Tree.instInhabitedTraversalTree.default }

structure Miri.TreeBorrows.Tree.TraversalEvent : Type

One node visit and the access relation passed to the location transition.

• node : Nat
• relatedness : AccessRelatedness

def Miri.TreeBorrows.Tree.instDecidableEqTraversalEvent.decEq (x✝ x✝¹ : TraversalEvent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqTraversalEvent : DecidableEq TraversalEvent

Equations

• Miri.TreeBorrows.Tree.instDecidableEqTraversalEvent = Miri.TreeBorrows.Tree.instDecidableEqTraversalEvent.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprTraversalEvent : Repr TraversalEvent

Equations

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

def Miri.TreeBorrows.Tree.instReprTraversalEvent.repr : TraversalEvent → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.Tree.TraversalTree.ancestorPath (tree : TraversalTree) (start : Nat) : List Nat

Equations

• tree.ancestorPath start = Miri.TreeBorrows.Tree.TraversalTree.ancestorPathAux✝ tree tree.nodes.size start

theorem Miri.TreeBorrows.Tree.TraversalTree.ancestorPath_head (tree : TraversalTree) (start : Nat) : (tree.ancestorPath start).head? = some start

def Miri.TreeBorrows.Tree.TraversalTree.traverse (tree : TraversalTree) (start : Nat) (mode : ChildrenVisitMode) (skipNodes : List Nat) : Nat × List TraversalEvent

Schedule a normal access: access the start and its ancestors first, then visit deferred cousin/child subtrees bottom-up. skipNodes models the source's foreign-only continue callback.

Equations

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

theorem Miri.TreeBorrows.Tree.TraversalTree.traverse_starts_at_accessed_node (tree : TraversalTree) (start : Nat) (mode : ChildrenVisitMode) (skipNodes : List Nat) : (tree.traverse start mode skipNodes).snd.head? = some { node := start, relatedness := AccessRelatedness.LocalAccess }

The source visitor always propagates at the accessed node first.