One-location normal-tree access processing from the interaction between Miri's tree visitor and LocationState::perform_transition. This composes the exact local/foreign visit schedule with lazy per-node defaults, SIFA skip and record behavior, permission transitions, and protector errors.

The model assumes aligned node/default/state arrays and a valid finite tree. It covers the normal concrete-provenance tree path at one location. Ranged allocations, wildcard roots/exposed caches, diagnostics, and deallocation checks remain separate.

structure Miri.TreeBorrows.Tree.NormalTreeState : Type

Per-node defaults and protector status for one concrete tree location.

• topology : TraversalTree
• defaultStates : Array LocationState
• protectedNodes : List Nat
• locationStates : Array (Option LocationState)

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqNormalTreeState : DecidableEq NormalTreeState

Equations

• Miri.TreeBorrows.Tree.instDecidableEqNormalTreeState = Miri.TreeBorrows.Tree.instDecidableEqNormalTreeState.decEq

def Miri.TreeBorrows.Tree.instDecidableEqNormalTreeState.decEq (x✝ x✝¹ : NormalTreeState) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.Tree.instReprNormalTreeState.repr : NormalTreeState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprNormalTreeState : Repr NormalTreeState

Equations

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

inductive Miri.TreeBorrows.Tree.NormalAccessStatus : Type

Termination/status from one normal tree access.

• Completed : NormalAccessStatus
• TransitionError (node : Nat) (error : Diagnostics.TransitionError) : NormalAccessStatus
• RecordDebugAssertion (node : Nat) : NormalAccessStatus
• PermissionInvariantFailure (node : Nat) : NormalAccessStatus
• TransitionApplicationInvariantFailure (node : Nat) : NormalAccessStatus
• PossibleInvariantFailure (node : Nat) : NormalAccessStatus
• MissingLocationState (node : Nat) : NormalAccessStatus

def Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus.decEq (x✝ x✝¹ : NormalAccessStatus) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus.decEq Miri.TreeBorrows.Tree.NormalAccessStatus.Completed Miri.TreeBorrows.Tree.NormalAccessStatus.Completed = isTrue ⋯
• Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus.decEq Miri.TreeBorrows.Tree.NormalAccessStatus.Completed (Miri.TreeBorrows.Tree.NormalAccessStatus.RecordDebugAssertion node) = isFalse ⋯
• Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus.decEq Miri.TreeBorrows.Tree.NormalAccessStatus.Completed (Miri.TreeBorrows.Tree.NormalAccessStatus.MissingLocationState node) = isFalse ⋯

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus : DecidableEq NormalAccessStatus

Equations

• Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus = Miri.TreeBorrows.Tree.instDecidableEqNormalAccessStatus.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprNormalAccessStatus : Repr NormalAccessStatus

Equations

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

def Miri.TreeBorrows.Tree.instReprNormalAccessStatus.repr : NormalAccessStatus → Nat → Std.Format

Equations

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

structure Miri.TreeBorrows.Tree.NormalAccessResult : Type

Updated one-location tree, root of the accessed tree, events propagated, and the first source error (if any).

• tree : NormalTreeState
• root : Nat
• visited : List TraversalEvent
• status : NormalAccessStatus

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqNormalAccessResult : DecidableEq NormalAccessResult

Equations

• Miri.TreeBorrows.Tree.instDecidableEqNormalAccessResult = Miri.TreeBorrows.Tree.instDecidableEqNormalAccessResult.decEq

def Miri.TreeBorrows.Tree.instDecidableEqNormalAccessResult.decEq (x✝ x✝¹ : NormalAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.Tree.instReprNormalAccessResult.repr : NormalAccessResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprNormalAccessResult : Repr NormalAccessResult

Equations

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

def Miri.TreeBorrows.Tree.NormalTreeState.stateAt (tree : NormalTreeState) (node : Nat) : Option LocationState

Existing lazy state, or the node's source default state.

Equations

• tree.stateAt node = match tree.locationStates[node]? with | none => none | some (some state) => some state | some none => tree.defaultStates[node]?

def Miri.TreeBorrows.Tree.NormalTreeState.performAccess (tree : NormalTreeState) (start : Nat) (kind : AccessKind) (mode : ChildrenVisitMode) : NormalAccessResult

Apply the normal concrete-tree access at one location. The visit skip set is computed from each node's current-or-default state exactly as Miri's foreign-only continue callback does.

Equations

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

def Miri.TreeBorrows.Tree.NormalTreeState.singletonCell : NormalTreeState

A one-node Cell tree used to establish a complete normal-access contract.

Equations

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

theorem Miri.TreeBorrows.Tree.NormalTreeState.singletonCellAccess_contract (kind : AccessKind) : have result := singletonCell.performAccess 0 kind ChildrenVisitMode.VisitChildrenOfAccessed; result.status = NormalAccessStatus.Completed ∧ result.visited = [{ node := 0, relatedness := AccessRelatedness.LocalAccess }] ∧ result.tree.locationStates = #[some { permission := Permission.Cell, accessed := true, idempotentForeignAccess := IdempotentForeignAccess.None }]

On a singleton tree, a local Cell access completes and materializes the accessed location state exactly as the source helpers require.