Miri.TreeBorrows.Permissions

source

inductive Miri.TreeBorrows.Permission :

Type

The activation states of a Tree Borrows pointer.

Cell : Permission
A shared reference to interior mutable data.
ReservedFrz (conflicted : Bool) : Permission
A local mutable reference not yet written through.
ReservedIM : Permission
A reservation to interior mutable data.
Unique : Permission
A unique pointer.
Frozen : Permission
A shared, read-only pointer.
Disabled : Permission
A disabled pointer.

Instances For

source

def Miri.TreeBorrows.instDecidableEqPermission.decEq (x✝ x✝¹ : Permission) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqPermission :

DecidableEq Permission

Equations

Miri.TreeBorrows.instDecidableEqPermission = Miri.TreeBorrows.instDecidableEqPermission.decEq

source

def Miri.TreeBorrows.instReprPermission.repr :

Permission → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprPermission :

Repr Permission

Equations

Miri.TreeBorrows.instReprPermission = { reprPrec := Miri.TreeBorrows.instReprPermission.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedPermission :

Inhabited Permission

Equations

Miri.TreeBorrows.instInhabitedPermission = { default := Miri.TreeBorrows.instInhabitedPermission.default }

source

inductive Miri.TreeBorrows.AccessKind :

Type

The access kind used by Miri's borrow tracker.

Read : AccessKind
Write : AccessKind

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqAccessKind :

DecidableEq AccessKind

Equations

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

source

def Miri.TreeBorrows.instReprAccessKind.repr :

AccessKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprAccessKind :

Repr AccessKind

Equations

Miri.TreeBorrows.instReprAccessKind = { reprPrec := Miri.TreeBorrows.instReprAccessKind.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedAccessKind :

Inhabited AccessKind

Equations

Miri.TreeBorrows.instInhabitedAccessKind = { default := Miri.TreeBorrows.instInhabitedAccessKind.default }

source

inductive Miri.TreeBorrows.AccessRelatedness :

Type

Whether an access is through this node or one of its children.

LocalAccess : AccessRelatedness
ForeignAccess : AccessRelatedness

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqAccessRelatedness :

DecidableEq AccessRelatedness

Equations

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

source

def Miri.TreeBorrows.instReprAccessRelatedness.repr :

AccessRelatedness → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprAccessRelatedness :

Repr AccessRelatedness

Equations

Miri.TreeBorrows.instReprAccessRelatedness = { reprPrec := Miri.TreeBorrows.instReprAccessRelatedness.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedAccessRelatedness :

Inhabited AccessRelatedness

Equations

Miri.TreeBorrows.instInhabitedAccessRelatedness = { default := Miri.TreeBorrows.instInhabitedAccessRelatedness.default }

source

def Miri.TreeBorrows.AccessRelatedness.isForeign :

AccessRelatedness → Bool

true exactly for an ancestor, sibling, cousin, or other non-child access.

Equations

Instances For

source

inductive Miri.TreeBorrows.AccessOutcome :

Type

Outcomes of Miri's Option<PermissionPriv> transition function.

UndefinedBehavior corresponds to upstream None for a forbidden child access. ImpossibleProtectedReservedIM preserves the upstream assert!(!protected) branches: those are invariant failures, not ordinary UB outcomes.

Transition (permission : Permission) : AccessOutcome
UndefinedBehavior : AccessOutcome
ImpossibleProtectedReservedIM : AccessOutcome

Instances For

source

def Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq (x✝ x✝¹ : AccessOutcome) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq (Miri.TreeBorrows.AccessOutcome.Transition a) (Miri.TreeBorrows.AccessOutcome.Transition b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq (Miri.TreeBorrows.AccessOutcome.Transition permission) Miri.TreeBorrows.AccessOutcome.UndefinedBehavior = isFalse ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq (Miri.TreeBorrows.AccessOutcome.Transition permission) Miri.TreeBorrows.AccessOutcome.ImpossibleProtectedReservedIM = isFalse ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq Miri.TreeBorrows.AccessOutcome.UndefinedBehavior (Miri.TreeBorrows.AccessOutcome.Transition permission) = isFalse ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq Miri.TreeBorrows.AccessOutcome.UndefinedBehavior Miri.TreeBorrows.AccessOutcome.UndefinedBehavior = isTrue ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq Miri.TreeBorrows.AccessOutcome.ImpossibleProtectedReservedIM (Miri.TreeBorrows.AccessOutcome.Transition permission) = isFalse ⋯
Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq Miri.TreeBorrows.AccessOutcome.ImpossibleProtectedReservedIM Miri.TreeBorrows.AccessOutcome.ImpossibleProtectedReservedIM = isTrue ⋯

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqAccessOutcome :

DecidableEq AccessOutcome

Equations

Miri.TreeBorrows.instDecidableEqAccessOutcome = Miri.TreeBorrows.instDecidableEqAccessOutcome.decEq

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprAccessOutcome :

Repr AccessOutcome

Equations

Miri.TreeBorrows.instReprAccessOutcome = { reprPrec := Miri.TreeBorrows.instReprAccessOutcome.repr }

source

def Miri.TreeBorrows.instReprAccessOutcome.repr :

AccessOutcome → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedAccessOutcome :

Inhabited AccessOutcome

Equations

Miri.TreeBorrows.instInhabitedAccessOutcome = { default := Miri.TreeBorrows.instInhabitedAccessOutcome.default }

source

def Miri.TreeBorrows.performAccess (kind : AccessKind) (relPos : AccessRelatedness) (old : Permission) (isProtected : Bool) :

AccessOutcome

Apply the pinned Miri transition rules to one permission.

The dispatcher is the same four-way match as upstream on (kind, rel_pos.is_foreign()).

Equations

Miri.TreeBorrows.performAccess Miri.TreeBorrows.AccessKind.Write relPos old isProtected = Miri.TreeBorrows.foreignWrite✝ old isProtected
Miri.TreeBorrows.performAccess Miri.TreeBorrows.AccessKind.Read relPos old isProtected = Miri.TreeBorrows.foreignRead✝ old isProtected
Miri.TreeBorrows.performAccess Miri.TreeBorrows.AccessKind.Write relPos old isProtected = Miri.TreeBorrows.childWrite✝ old isProtected
Miri.TreeBorrows.performAccess Miri.TreeBorrows.AccessKind.Read relPos old isProtected = Miri.TreeBorrows.childRead✝ old

Instances For

source

def Miri.TreeBorrows.Permission.isInitial :

Permission → Bool

Whether this permission is one of the upstream initial states.

Equations

Instances For

source

def Miri.TreeBorrows.permissionLE :

Permission → Permission → Bool

Source ordering by reachability of permission transitions.

This captures the PartialOrd relation from PermissionPriv::partial_cmp: Cell is isolated; ReservedIM is incomparable with either ReservedFrz state; all remaining reachable states form the Reserved → Unique → Frozen → Disabled chain, with the conflicted Reserved state above the unconflicted one.

Equations

Instances For

source

inductive Miri.TreeBorrows.PermissionOrdering :

Type

Result corresponding to Rust's Option<Ordering> for the source PermissionPriv::partial_cmp.

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqPermissionOrdering :

DecidableEq PermissionOrdering

Equations

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

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprPermissionOrdering :

Repr PermissionOrdering

Equations

Miri.TreeBorrows.instReprPermissionOrdering = { reprPrec := Miri.TreeBorrows.instReprPermissionOrdering.repr }

source

def Miri.TreeBorrows.instReprPermissionOrdering.repr :

PermissionOrdering → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedPermissionOrdering :

Inhabited PermissionOrdering

Equations

Miri.TreeBorrows.instInhabitedPermissionOrdering = { default := Miri.TreeBorrows.instInhabitedPermissionOrdering.default }

source

def Miri.TreeBorrows.permissionCompare (left right : Permission) :

PermissionOrdering

Equations

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

Instances For

source

inductive Miri.TreeBorrows.WildcardAccessLevel :

Type

Whether a local access to a permission is allowed by the wildcard cache.

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqWildcardAccessLevel :

DecidableEq WildcardAccessLevel

Equations

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

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprWildcardAccessLevel :

Repr WildcardAccessLevel

Equations

Miri.TreeBorrows.instReprWildcardAccessLevel = { reprPrec := Miri.TreeBorrows.instReprWildcardAccessLevel.repr }

source

def Miri.TreeBorrows.instReprWildcardAccessLevel.repr :

WildcardAccessLevel → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedWildcardAccessLevel :

Inhabited WildcardAccessLevel

Equations

Miri.TreeBorrows.instInhabitedWildcardAccessLevel = { default := Miri.TreeBorrows.instInhabitedWildcardAccessLevel.default }

source

inductive Miri.TreeBorrows.IdempotentForeignAccess :

Type

Whether a foreign access can be skipped after a recorded subtree access.

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqIdempotentForeignAccess :

DecidableEq IdempotentForeignAccess

Equations

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

source

def Miri.TreeBorrows.instReprIdempotentForeignAccess.repr :

IdempotentForeignAccess → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprIdempotentForeignAccess :

Repr IdempotentForeignAccess

Equations

Miri.TreeBorrows.instReprIdempotentForeignAccess = { reprPrec := Miri.TreeBorrows.instReprIdempotentForeignAccess.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedIdempotentForeignAccess :

Inhabited IdempotentForeignAccess

Equations

Miri.TreeBorrows.instInhabitedIdempotentForeignAccess = { default := Miri.TreeBorrows.instInhabitedIdempotentForeignAccess.default }

source

def Miri.TreeBorrows.WildcardAccessLevel.rank :

WildcardAccessLevel → Nat

Equations

Instances For

source

def Miri.TreeBorrows.WildcardAccessLevel.allows (level : WildcardAccessLevel) (kind : AccessKind) :

Bool

Whether this cached access level allows the requested access kind.

Equations

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.rank :

IdempotentForeignAccess → Nat

Equations

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.isLocal :

IdempotentForeignAccess → Bool

Equations

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.isForeign (access : IdempotentForeignAccess) :

Bool

Equations

access.isForeign = !access.isLocal

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.le (left right : IdempotentForeignAccess) :

Bool

Source order used by Miri: None < Read < Write.

Equations

left.le right = decide (left.rank ≤ right.rank)

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.max (left right : IdempotentForeignAccess) :

IdempotentForeignAccess

Equations

left.max right = if left.rank ≤ right.rank then right else left

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.fromForeign :

AccessKind → IdempotentForeignAccess

Construct a foreign access from its access kind.

Equations

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.fromAccessAndRelatedness (kind : AccessKind) (relatedness : AccessRelatedness) :

IdempotentForeignAccess

Convert an access and its relation to the cache's recorded-access value.

Equations

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

Instances For

source

inductive Miri.TreeBorrows.IdempotentForeignAccess.SkipCheckResult :

Type

Result of the source skip check, including its debug assertion.

Decision (canSkip : Bool) : SkipCheckResult
DebugAssertion : SkipCheckResult

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.instDecidableEqSkipCheckResult.decEq (x✝ x✝¹ : SkipCheckResult) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.IdempotentForeignAccess.instDecidableEqSkipCheckResult :

DecidableEq SkipCheckResult

Equations

Miri.TreeBorrows.IdempotentForeignAccess.instDecidableEqSkipCheckResult = Miri.TreeBorrows.IdempotentForeignAccess.instDecidableEqSkipCheckResult.decEq

source

def Miri.TreeBorrows.IdempotentForeignAccess.instReprSkipCheckResult.repr :

SkipCheckResult → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.IdempotentForeignAccess.instReprSkipCheckResult :

Repr SkipCheckResult

Equations

Miri.TreeBorrows.IdempotentForeignAccess.instReprSkipCheckResult = { reprPrec := Miri.TreeBorrows.IdempotentForeignAccess.instReprSkipCheckResult.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.IdempotentForeignAccess.instInhabitedSkipCheckResult :

Inhabited SkipCheckResult

Equations

Miri.TreeBorrows.IdempotentForeignAccess.instInhabitedSkipCheckResult = { default := Miri.TreeBorrows.IdempotentForeignAccess.instInhabitedSkipCheckResult.default }

source

def Miri.TreeBorrows.IdempotentForeignAccess.canSkipForeignAccess (recorded happeningNext : IdempotentForeignAccess) :

SkipCheckResult

Whether the recorded access allows skipping the next foreign access.

The source's debug_assert!(happeningNext.is_foreign()) is represented explicitly for calls outside its documented domain.

Equations

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

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.recordNew (recorded justHappened : IdempotentForeignAccess) :

IdempotentForeignAccess

Update a recorded access exactly as the source record_new method does.

Equations

recorded.recordNew justHappened = if justHappened.isLocal = true then Miri.TreeBorrows.IdempotentForeignAccess.None else recorded.max justHappened

Instances For

source

def Miri.TreeBorrows.IdempotentForeignAccess.ensureNoStrongerThan (recorded strongestAllowed : IdempotentForeignAccess) :

IdempotentForeignAccess × Bool

Weaken a cache value when a newly inserted child has a weaker value.

Equations

recorded.ensureNoStrongerThan strongestAllowed = if strongestAllowed.rank < recorded.rank then (strongestAllowed, true ) else (recorded, false )

Instances For

source

def Miri.TreeBorrows.Permission.isDisabled :

Permission → Bool

Equations

Instances For

source

def Miri.TreeBorrows.Permission.isFrozen :

Permission → Bool

Equations

Miri.TreeBorrows.Permission.Frozen.isFrozen = true
x✝.isFrozen = false

Instances For

source

def Miri.TreeBorrows.Permission.isCell :

Permission → Bool

Equations

Miri.TreeBorrows.Permission.Cell.isCell = true
x✝.isCell = false

Instances For

source

def Miri.TreeBorrows.Permission.isUnique :

Permission → Bool

Equations

Miri.TreeBorrows.Permission.Unique.isUnique = true
x✝.isUnique = false

Instances For

source

def Miri.TreeBorrows.Permission.newUnique :

Permission

Equations

Miri.TreeBorrows.Permission.newUnique = Miri.TreeBorrows.Permission.Unique

Instances For

source

def Miri.TreeBorrows.Permission.newReservedFrz :

Permission

Equations

Miri.TreeBorrows.Permission.newReservedFrz = Miri.TreeBorrows.Permission.ReservedFrz false

Instances For

source

def Miri.TreeBorrows.Permission.newReservedIM :

Permission

Equations

Miri.TreeBorrows.Permission.newReservedIM = Miri.TreeBorrows.Permission.ReservedIM

Instances For

source

def Miri.TreeBorrows.Permission.newFrozen :

Permission

Equations

Miri.TreeBorrows.Permission.newFrozen = Miri.TreeBorrows.Permission.Frozen

Instances For

source

def Miri.TreeBorrows.Permission.newDisabled :

Permission

Equations

Miri.TreeBorrows.Permission.newDisabled = Miri.TreeBorrows.Permission.Disabled

Instances For

source

def Miri.TreeBorrows.Permission.newCell :

Permission

Equations

Miri.TreeBorrows.Permission.newCell = Miri.TreeBorrows.Permission.Cell

Instances For

source

def Miri.TreeBorrows.Permission.associatedAccess :

Permission → Option AccessKind

The access Miri associates with this permission when releasing protection or reborrowing.

Equations

Instances For

source

def Miri.TreeBorrows.Permission.canBeReplacedByChild (parent child : Permission) :

Bool

Whether a parent permission can be soundly replaced by the given child during the source's tree compaction. The caller must ensure the parent is not protected, as the source documents.

Equations

Instances For

source

inductive Miri.TreeBorrows.Permission.IdempotentAccessResult :

Type

Strongest foreign action this node survives unchanged.

ImpossibleProtectedReservedIM preserves the upstream unreachable! branch as an invariant failure instead of treating it as an ordinary result.

Access (access : IdempotentForeignAccess) : IdempotentAccessResult
ImpossibleProtectedReservedIM : IdempotentAccessResult

Instances For

source

def Miri.TreeBorrows.Permission.instDecidableEqIdempotentAccessResult.decEq (x✝ x✝¹ : IdempotentAccessResult) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.Permission.instDecidableEqIdempotentAccessResult :

DecidableEq IdempotentAccessResult

Equations

Miri.TreeBorrows.Permission.instDecidableEqIdempotentAccessResult = Miri.TreeBorrows.Permission.instDecidableEqIdempotentAccessResult.decEq

source

@[instance_reducible]

instance Miri.TreeBorrows.Permission.instReprIdempotentAccessResult :

Repr IdempotentAccessResult

Equations

Miri.TreeBorrows.Permission.instReprIdempotentAccessResult = { reprPrec := Miri.TreeBorrows.Permission.instReprIdempotentAccessResult.repr }

source

def Miri.TreeBorrows.Permission.instReprIdempotentAccessResult.repr :

IdempotentAccessResult → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.Permission.instInhabitedIdempotentAccessResult :

Inhabited IdempotentAccessResult

Equations

Miri.TreeBorrows.Permission.instInhabitedIdempotentAccessResult = { default := Miri.TreeBorrows.Permission.instInhabitedIdempotentAccessResult.default }

source

def Miri.TreeBorrows.Permission.strongestIdempotentForeignAccess (permission : Permission) (isProtected : Bool) :

IdempotentAccessResult

Equations

Instances For

source

def Miri.TreeBorrows.Permission.strongestAllowedLocalAccess (permission : Permission) (isProtected : Bool) :

WildcardAccessLevel

Strongest local access that does not cause UB, used by wildcard tracking.

Equations

One or more equations did not get rendered due to their size.
Miri.TreeBorrows.Permission.Disabled.strongestAllowedLocalAccess isProtected = Miri.TreeBorrows.WildcardAccessLevel.None
Miri.TreeBorrows.Permission.Frozen.strongestAllowedLocalAccess isProtected = Miri.TreeBorrows.WildcardAccessLevel.Read
permission.strongestAllowedLocalAccess isProtected = Miri.TreeBorrows.WildcardAccessLevel.Write

Instances For

source

structure Miri.TreeBorrows.PermTransition :

Type

A transition reconstructed by the source diagnostics and permission API.

fromPermission : Permission
toPermission : Permission

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqPermTransition :

DecidableEq PermTransition

Equations

Miri.TreeBorrows.instDecidableEqPermTransition = Miri.TreeBorrows.instDecidableEqPermTransition.decEq

source

def Miri.TreeBorrows.instDecidableEqPermTransition.decEq (x✝ x✝¹ : PermTransition) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

def Miri.TreeBorrows.instReprPermTransition.repr :

PermTransition → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprPermTransition :

Repr PermTransition

Equations

Miri.TreeBorrows.instReprPermTransition = { reprPrec := Miri.TreeBorrows.instReprPermTransition.repr }

source

def Miri.TreeBorrows.PermTransition.isPossible (transition : PermTransition) :

Bool

Equations

transition.isPossible = Miri.TreeBorrows.permissionLE transition.fromPermission transition.toPermission

Instances For

source

def Miri.TreeBorrows.PermTransition.isNoop (transition : PermTransition) :

Bool

Equations

transition.isNoop = (transition.fromPermission == transition.toPermission)

Instances For

source

def Miri.TreeBorrows.PermTransition.applied (transition : PermTransition) (startingPoint : Permission) :

Option Permission

Apply this transition only when the supplied starting permission matches.

Equations

transition.applied startingPoint = if (startingPoint == transition.fromPermission) = true then some transition.toPermission else none

Instances For

source

def Miri.TreeBorrows.PermTransition.producesDisabled (transition : PermTransition) :

Bool

Equations

transition.producesDisabled = transition.toPermission.isDisabled

Instances For

source

def Miri.TreeBorrows.PermTransition.endpoint (transition : PermTransition) :

Permission

Equations

transition.endpoint = transition.toPermission

Instances For

source

inductive Miri.TreeBorrows.PermTransitionOutcome :

Type

Permission-level result of the public source Permission::perform_access wrapper, retaining an explicit label for its invariant panic.

Transition (transition : PermTransition) : PermTransitionOutcome
UndefinedBehavior : PermTransitionOutcome
ImpossibleProtectedReservedIM : PermTransitionOutcome

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instDecidableEqPermTransitionOutcome :

DecidableEq PermTransitionOutcome

Equations

Miri.TreeBorrows.instDecidableEqPermTransitionOutcome = Miri.TreeBorrows.instDecidableEqPermTransitionOutcome.decEq

source

def Miri.TreeBorrows.instDecidableEqPermTransitionOutcome.decEq (x✝ x✝¹ : PermTransitionOutcome) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.TreeBorrows.instDecidableEqPermTransitionOutcome.decEq Miri.TreeBorrows.PermTransitionOutcome.UndefinedBehavior (Miri.TreeBorrows.PermTransitionOutcome.Transition transition) = isFalse ⋯
Miri.TreeBorrows.instDecidableEqPermTransitionOutcome.decEq Miri.TreeBorrows.PermTransitionOutcome.UndefinedBehavior Miri.TreeBorrows.PermTransitionOutcome.UndefinedBehavior = isTrue ⋯

Instances For

source

def Miri.TreeBorrows.instReprPermTransitionOutcome.repr :

PermTransitionOutcome → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.TreeBorrows.instReprPermTransitionOutcome :

Repr PermTransitionOutcome

Equations

Miri.TreeBorrows.instReprPermTransitionOutcome = { reprPrec := Miri.TreeBorrows.instReprPermTransitionOutcome.repr }

source

@[instance_reducible]

instance Miri.TreeBorrows.instInhabitedPermTransitionOutcome :

Inhabited PermTransitionOutcome

Equations

Miri.TreeBorrows.instInhabitedPermTransitionOutcome = { default := Miri.TreeBorrows.instInhabitedPermTransitionOutcome.default }

source

def Miri.TreeBorrows.performAccessTransition (kind : AccessKind) (relPos : AccessRelatedness) (old : Permission) (isProtected : Bool) :

PermTransitionOutcome

Convert the per-node result to the source PermTransition wrapper form.

Equations

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

Instances For

source

theorem Miri.TreeBorrows.reserved_local_write_activates :

performAccessTransition AccessKind.Write AccessRelatedness.LocalAccess (Permission.ReservedFrz false) false = PermTransitionOutcome.Transition { fromPermission := Permission.ReservedFrz false, toPermission := Permission.Unique }

A write activates an unconflicted two-phase reservation.

source

theorem Miri.TreeBorrows.cell_is_unchanged (kind : AccessKind) (relPos : AccessRelatedness) (isProtected : Bool) :

performAccess kind relPos Permission.Cell isProtected = AccessOutcome.Transition Permission.Cell

source

theorem Miri.TreeBorrows.valid_protector_avoids_invariant_failure (kind : AccessKind) (relPos : AccessRelatedness) (state : Permission) (isProtected : Bool) (h : isProtected = false ∨ state ≠ Permission.ReservedIM) :

performAccess kind relPos state isProtected ≠ AccessOutcome.ImpossibleProtectedReservedIM

If the protector invariant holds, the two upstream assertion branches are unreachable. The invariant excludes only protected ReservedIM; Cell may be protected, as in upstream behavior.

source

theorem Miri.TreeBorrows.successful_transition_is_monotone (kind : AccessKind) (relPos : AccessRelatedness) (state next : Permission) (isProtected : Bool) (h : performAccess kind relPos state isProtected = AccessOutcome.Transition next) :

permissionLE state next = true

Every successful per-node transition is nondecreasing in Miri's source permission ordering.

source

theorem Miri.TreeBorrows.can_replace_permission_by_itself (state : Permission) :

state.canBeReplacedByChild state = true

Tree compaction always permits replacing a permission with itself.

source

theorem Miri.TreeBorrows.strongest_local_access_matches_transition (state : Permission) (isProtected : Bool) (kind : AccessKind) :

(state.strongestAllowedLocalAccess isProtected).allows kind = match performAccess kind AccessRelatedness.LocalAccess state isProtected with | AccessOutcome.Transition permission => true | AccessOutcome.UndefinedBehavior => false | AccessOutcome.ImpossibleProtectedReservedIM => false

The strongest-local-access summary agrees with the local read/write transition function: it allows exactly the accesses that are not UB.

source

theorem Miri.TreeBorrows.record_local_access_resets_sifa (recorded : IdempotentForeignAccess) :

recorded.recordNew IdempotentForeignAccess.None = IdempotentForeignAccess.None

A recorded local access resets SIFA regardless of the previous value.

source

theorem Miri.TreeBorrows.transition_applied_at_source (transition : PermTransition) :

transition.applied transition.fromPermission = some transition.toPermission

A successful source transition can be applied only at its recorded source state, and then returns the recorded endpoint.

source

theorem Miri.TreeBorrows.sifa_read_is_stable (state : Permission) (isProtected : Bool) (h : state.strongestIdempotentForeignAccess isProtected = Permission.IdempotentAccessResult.Access IdempotentForeignAccess.Read) :

performAccess AccessKind.Read AccessRelatedness.ForeignAccess state isProtected = AccessOutcome.Transition state

A permission marked idempotent under foreign reads really is unchanged by the source foreign-read transition.

source

theorem Miri.TreeBorrows.sifa_write_is_stable (state : Permission) (isProtected : Bool) (h : state.strongestIdempotentForeignAccess isProtected = Permission.IdempotentAccessResult.Access IdempotentForeignAccess.Write) (kind : AccessKind) :

performAccess kind AccessRelatedness.ForeignAccess state isProtected = AccessOutcome.Transition state

A permission marked idempotent under foreign writes is unchanged by both foreign read and write transitions.