The state and per-location update layer from pinned Miri tree_borrows/tree.rs. This is below the allocation-wide range map and tree visitor: it keeps the initialization/accessed bit, permission, SIFA cache, and the exact permission/protector error ordering for one tree node at one location.

inductive Miri.TreeBorrows.Diagnostics.TransitionError : Type

Transition errors emitted by the per-location layer. ProtectedDealloc belongs to the later tree-wide deallocation check.

• ChildAccessForbidden (permission : Permission) : TransitionError
• ProtectedDisabled (permission : Permission) : TransitionError
• ProtectedDealloc : TransitionError

def Miri.TreeBorrows.Diagnostics.instDecidableEqTransitionError.decEq (x✝ x✝¹ : TransitionError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Diagnostics.instDecidableEqTransitionError : DecidableEq TransitionError

Equations

• Miri.TreeBorrows.Diagnostics.instDecidableEqTransitionError = Miri.TreeBorrows.Diagnostics.instDecidableEqTransitionError.decEq

def Miri.TreeBorrows.Diagnostics.instReprTransitionError.repr : TransitionError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Diagnostics.instReprTransitionError : Repr TransitionError

Equations

• Miri.TreeBorrows.Diagnostics.instReprTransitionError = { reprPrec := Miri.TreeBorrows.Diagnostics.instReprTransitionError.repr }

@[instance_reducible]

instance Miri.TreeBorrows.Diagnostics.instInhabitedTransitionError : Inhabited TransitionError

Equations

• Miri.TreeBorrows.Diagnostics.instInhabitedTransitionError = { default := Miri.TreeBorrows.Diagnostics.instInhabitedTransitionError.default }

inductive Miri.TreeBorrows.Tree.ContinueTraversal : Type

The two continuation results used by Miri's tree visitor.

• Recurse : ContinueTraversal
• SkipSelfAndChildren : ContinueTraversal

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqContinueTraversal : DecidableEq ContinueTraversal

Equations

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

def Miri.TreeBorrows.Tree.instReprContinueTraversal.repr : ContinueTraversal → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprContinueTraversal : Repr ContinueTraversal

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instInhabitedContinueTraversal : Inhabited ContinueTraversal

Equations

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

structure Miri.TreeBorrows.Tree.LocationState : Type

Per-node state at one allocation location. A false accessed bit stores the future initial permission for a location that has not yet been reached by a child pointer.

• permission : Permission
• accessed : Bool
• idempotentForeignAccess : IdempotentForeignAccess

def Miri.TreeBorrows.Tree.instDecidableEqLocationState.decEq (x✝ x✝¹ : LocationState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instDecidableEqLocationState : DecidableEq LocationState

Equations

• Miri.TreeBorrows.Tree.instDecidableEqLocationState = Miri.TreeBorrows.Tree.instDecidableEqLocationState.decEq

def Miri.TreeBorrows.Tree.instReprLocationState.repr : LocationState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.instReprLocationState : Repr LocationState

Equations

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

inductive Miri.TreeBorrows.Tree.LocationState.ConstructionResult : Type

Construction failures corresponding to the source assert!s.

• Constructed (state : LocationState) : ConstructionResult
• PermissionNotInitialOrDisabled : ConstructionResult
• UniquePermissionNotAccessed : ConstructionResult

def Miri.TreeBorrows.Tree.LocationState.instDecidableEqConstructionResult.decEq (x✝ x✝¹ : ConstructionResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instDecidableEqConstructionResult : DecidableEq ConstructionResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instDecidableEqConstructionResult = Miri.TreeBorrows.Tree.LocationState.instDecidableEqConstructionResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instReprConstructionResult : Repr ConstructionResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instReprConstructionResult = { reprPrec := Miri.TreeBorrows.Tree.LocationState.instReprConstructionResult.repr }

def Miri.TreeBorrows.Tree.LocationState.instReprConstructionResult.repr : ConstructionResult → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.Tree.LocationState.newNonAccessed (permission : Permission) (sifa : IdempotentForeignAccess) : ConstructionResult

Source new_non_accessed, with its assertions retained as explicit outcomes.

Equations

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

def Miri.TreeBorrows.Tree.LocationState.newAccessed (permission : Permission) (sifa : IdempotentForeignAccess) : LocationState

Source new_accessed has no validity assertions.

Equations

• Miri.TreeBorrows.Tree.LocationState.newAccessed permission sifa = { permission := permission, accessed := true, idempotentForeignAccess := sifa }

def Miri.TreeBorrows.Tree.LocationState.possible (state : LocationState) : Bool

A lazy Unique state is unreachable; every other permission is possible regardless of whether its location has been accessed.

Equations

• state.possible = (state.accessed || !state.permission.isUnique)

def Miri.TreeBorrows.Tree.LocationState.isAccessed (state : LocationState) : Bool

Check whether any child pointer has accessed this location.

Equations

• state.isAccessed = state.accessed

def Miri.TreeBorrows.Tree.LocationState.currentPermission (state : LocationState) : Permission

Current permission or future initial permission.

Equations

• state.currentPermission = state.permission

def Miri.TreeBorrows.Tree.LocationState.skipIfKnownNoop (state : LocationState) (accessKind : AccessKind) (relatedness : AccessRelatedness) : ContinueTraversal

Result of the tree traversal's per-node skip predicate.

Equations

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

inductive Miri.TreeBorrows.Tree.LocationState.RecordAccessResult : Type

SIFA update with the source debug-assert precondition represented as a separate result.

• Recorded (state : LocationState) : RecordAccessResult
• DebugAssertion : RecordAccessResult

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instDecidableEqRecordAccessResult : DecidableEq RecordAccessResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instDecidableEqRecordAccessResult = Miri.TreeBorrows.Tree.LocationState.instDecidableEqRecordAccessResult.decEq

def Miri.TreeBorrows.Tree.LocationState.instDecidableEqRecordAccessResult.decEq (x✝ x✝¹ : RecordAccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instReprRecordAccessResult : Repr RecordAccessResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instReprRecordAccessResult = { reprPrec := Miri.TreeBorrows.Tree.LocationState.instReprRecordAccessResult.repr }

def Miri.TreeBorrows.Tree.LocationState.instReprRecordAccessResult.repr : RecordAccessResult → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.Tree.LocationState.recordNewAccess (state : LocationState) (accessKind : AccessKind) (relatedness : AccessRelatedness) : RecordAccessResult

Source record_new_access; callers must only record accesses whose skip-check result is Recurse.

Equations

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

inductive Miri.TreeBorrows.Tree.LocationState.AccessResult : Type

Result of applying one access to one location, including the resulting state on source Err results. Miri mutates the state before returning a ProtectedDisabled error.

• Success (state : LocationState) (transition : PermTransition) : AccessResult
• Error (state : LocationState) (error : Diagnostics.TransitionError) : AccessResult
• PermissionInvariantFailure (state : LocationState) : AccessResult
• TransitionApplicationInvariantFailure (state : LocationState) : AccessResult
• PossibleInvariantFailure (state : LocationState) : AccessResult

def Miri.TreeBorrows.Tree.LocationState.instDecidableEqAccessResult.decEq (x✝ x✝¹ : AccessResult) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instDecidableEqAccessResult : DecidableEq AccessResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instDecidableEqAccessResult = Miri.TreeBorrows.Tree.LocationState.instDecidableEqAccessResult.decEq

@[instance_reducible]

instance Miri.TreeBorrows.Tree.LocationState.instReprAccessResult : Repr AccessResult

Equations

• Miri.TreeBorrows.Tree.LocationState.instReprAccessResult = { reprPrec := Miri.TreeBorrows.Tree.LocationState.instReprAccessResult.repr }

def Miri.TreeBorrows.Tree.LocationState.instReprAccessResult.repr : AccessResult → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.Tree.LocationState.AccessResult.resultingState : AccessResult → LocationState

The location state after a call, including state retained on source errors.

Equations

• (Miri.TreeBorrows.Tree.LocationState.AccessResult.Success a a_1).resultingState = a
• (Miri.TreeBorrows.Tree.LocationState.AccessResult.Error a a_1).resultingState = a
• (Miri.TreeBorrows.Tree.LocationState.AccessResult.PermissionInvariantFailure a).resultingState = a
• (Miri.TreeBorrows.Tree.LocationState.AccessResult.TransitionApplicationInvariantFailure a).resultingState = a
• (Miri.TreeBorrows.Tree.LocationState.AccessResult.PossibleInvariantFailure a).resultingState = a

def Miri.TreeBorrows.Tree.LocationState.performAccess (state : LocationState) (accessKind : AccessKind) (relatedness : AccessRelatedness) (isProtected : Bool) : AccessResult

Apply LocationState::perform_access in source order.

Permission failure leaves the old location untouched. Otherwise the access bit and permission are updated before the protector check; thus a protected transition to Disabled is an error only if the location is now accessed.

Equations

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

theorem Miri.TreeBorrows.Tree.LocationState.performAccess_child_forbidden_unchanged (state : LocationState) (accessKind : AccessKind) (isProtected : Bool) (h : performAccessTransition accessKind AccessRelatedness.LocalAccess state.permission isProtected = PermTransitionOutcome.UndefinedBehavior) : state.performAccess accessKind AccessRelatedness.LocalAccess isProtected = AccessResult.Error state (Diagnostics.TransitionError.ChildAccessForbidden state.permission)

A forbidden child access leaves every part of the location state intact.