The permission-selection policy in pinned Miri's NewPermission::new. Rust type/layout facts and interpreter configuration are explicit inputs; this module does not model rustc type queries, pointer checks, or the full retag caller.

inductive Miri.TreeBorrows.RetagPolicy.RetagMode : Type

• None : RetagMode
• Default : RetagMode
• TwoPhase : RetagMode
• FnEntry : RetagMode
• Raw : RetagMode

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqRetagMode : DecidableEq RetagMode

Equations

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

def Miri.TreeBorrows.RetagPolicy.instReprRetagMode.repr : RetagMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprRetagMode : Repr RetagMode

Equations

• Miri.TreeBorrows.RetagPolicy.instReprRetagMode = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprRetagMode.repr }

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instInhabitedRetagMode : Inhabited RetagMode

Equations

• Miri.TreeBorrows.RetagPolicy.instInhabitedRetagMode = { default := Miri.TreeBorrows.RetagPolicy.instInhabitedRetagMode.default }

inductive Miri.TreeBorrows.RetagPolicy.ReferenceKind : Type

• Shared : ReferenceKind
• Mutable : ReferenceKind
• Box : ReferenceKind

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqReferenceKind : DecidableEq ReferenceKind

Equations

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

def Miri.TreeBorrows.RetagPolicy.instReprReferenceKind.repr : ReferenceKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprReferenceKind : Repr ReferenceKind

Equations

• Miri.TreeBorrows.RetagPolicy.instReprReferenceKind = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprReferenceKind.repr }

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instInhabitedReferenceKind : Inhabited ReferenceKind

Equations

• Miri.TreeBorrows.RetagPolicy.instInhabitedReferenceKind = { default := Miri.TreeBorrows.RetagPolicy.instInhabitedReferenceKind.default }

structure Miri.TreeBorrows.RetagPolicy.TypeFacts : Type

• isUnpin : Bool
• isUnsafeUnpin : Bool
• isFreeze : Bool

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqTypeFacts : DecidableEq TypeFacts

Equations

• Miri.TreeBorrows.RetagPolicy.instDecidableEqTypeFacts = Miri.TreeBorrows.RetagPolicy.instDecidableEqTypeFacts.decEq

def Miri.TreeBorrows.RetagPolicy.instDecidableEqTypeFacts.decEq (x✝ x✝¹ : TypeFacts) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.TreeBorrows.RetagPolicy.instReprTypeFacts.repr : TypeFacts → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprTypeFacts : Repr TypeFacts

Equations

• Miri.TreeBorrows.RetagPolicy.instReprTypeFacts = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprTypeFacts.repr }

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instInhabitedTypeFacts : Inhabited TypeFacts

Equations

• Miri.TreeBorrows.RetagPolicy.instInhabitedTypeFacts = { default := Miri.TreeBorrows.RetagPolicy.instInhabitedTypeFacts.default }

structure Miri.TreeBorrows.RetagPolicy.PolicyConfig : Type

• implicitWrites : Bool
• rustcNoWritable : Bool

def Miri.TreeBorrows.RetagPolicy.instDecidableEqPolicyConfig.decEq (x✝ x✝¹ : PolicyConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqPolicyConfig : DecidableEq PolicyConfig

Equations

• Miri.TreeBorrows.RetagPolicy.instDecidableEqPolicyConfig = Miri.TreeBorrows.RetagPolicy.instDecidableEqPolicyConfig.decEq

def Miri.TreeBorrows.RetagPolicy.instReprPolicyConfig.repr : PolicyConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprPolicyConfig : Repr PolicyConfig

Equations

• Miri.TreeBorrows.RetagPolicy.instReprPolicyConfig = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprPolicyConfig.repr }

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instInhabitedPolicyConfig : Inhabited PolicyConfig

Equations

• Miri.TreeBorrows.RetagPolicy.instInhabitedPolicyConfig = { default := Miri.TreeBorrows.RetagPolicy.instInhabitedPolicyConfig.default }

structure Miri.TreeBorrows.RetagPolicy.NewPermission : Type

• freezePermission : Permission
• nonfreezePermission : Permission
• outsidePermission : Permission
• protector : Option ProtectorKind

def Miri.TreeBorrows.RetagPolicy.instDecidableEqNewPermission.decEq (x✝ x✝¹ : NewPermission) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqNewPermission : DecidableEq NewPermission

Equations

• Miri.TreeBorrows.RetagPolicy.instDecidableEqNewPermission = Miri.TreeBorrows.RetagPolicy.instDecidableEqNewPermission.decEq

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprNewPermission : Repr NewPermission

Equations

• Miri.TreeBorrows.RetagPolicy.instReprNewPermission = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprNewPermission.repr }

def Miri.TreeBorrows.RetagPolicy.instReprNewPermission.repr : NewPermission → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqPart : DecidableEq Miri.TreeBorrows.RetagPolicy.Part✝

Equations

• Miri.TreeBorrows.RetagPolicy.instDecidableEqPart x✝ y✝ = if h : Miri.TreeBorrows.RetagPolicy.Part.ctorIdx✝ x✝ = Miri.TreeBorrows.RetagPolicy.Part.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

def Miri.TreeBorrows.RetagPolicy.instReprPart.repr : Miri.TreeBorrows.RetagPolicy.Part✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprPart : Repr Miri.TreeBorrows.RetagPolicy.Part✝

Equations

• Miri.TreeBorrows.RetagPolicy.instReprPart = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprPart.repr }

def Miri.TreeBorrows.RetagPolicy.create (facts : TypeFacts) (kind : ReferenceKind) (mode : RetagMode) (config : PolicyConfig) : Option NewPermission

Source NewPermission::new policy, with the rustc type queries and #[rustc_no_writable] lookup supplied as finite inputs.

None covers both disabled retagging and the source's mutable/Box pinning early return. Other interpreter operations around reborrowing remain outside this policy function.

Equations

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

inductive Miri.TreeBorrows.RetagPolicy.InitialStateError : Type

The source tb_reborrow closure selecting its permission for a frozen or UnsafeCell byte and constructing the matching accessed/future location state. The freeze-sensitive layout visitor that chooses frozen is a separate hook.

• protectedReservedIM : InitialStateError
• invalidLazyPermission (permission : Permission) : InitialStateError
• lazyUnique : InitialStateError

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instDecidableEqInitialStateError : DecidableEq InitialStateError

Equations

• Miri.TreeBorrows.RetagPolicy.instDecidableEqInitialStateError = Miri.TreeBorrows.RetagPolicy.instDecidableEqInitialStateError.decEq

def Miri.TreeBorrows.RetagPolicy.instDecidableEqInitialStateError.decEq (x✝ x✝¹ : InitialStateError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.RetagPolicy.instReprInitialStateError : Repr InitialStateError

Equations

• Miri.TreeBorrows.RetagPolicy.instReprInitialStateError = { reprPrec := Miri.TreeBorrows.RetagPolicy.instReprInitialStateError.repr }

def Miri.TreeBorrows.RetagPolicy.instReprInitialStateError.repr : InitialStateError → Nat → Std.Format

Equations

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

def Miri.TreeBorrows.RetagPolicy.initialLocationState (policy : NewPermission) (frozen : Bool) : Except InitialStateError Tree.LocationState

Equations

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

theorem Miri.TreeBorrows.RetagPolicy.none_mode_never_creates_permission (facts : TypeFacts) (kind : ReferenceKind) (config : PolicyConfig) : create facts kind RetagMode.None config = none

theorem Miri.TreeBorrows.RetagPolicy.pinned_mutable_reference_is_not_retagged (facts : TypeFacts) (config : PolicyConfig) (h : (!(facts.isUnpin && facts.isUnsafeUnpin)) = true) : create facts ReferenceKind.Mutable RetagMode.Default config = none

theorem Miri.TreeBorrows.RetagPolicy.pinned_box_is_not_retagged (facts : TypeFacts) (config : PolicyConfig) (h : (!(facts.isUnpin && facts.isUnsafeUnpin)) = true) : create facts ReferenceKind.Box RetagMode.FnEntry config = none

theorem Miri.TreeBorrows.RetagPolicy.shared_cell_starts_unaccessed : initialLocationState { freezePermission := Permission.Frozen, nonfreezePermission := Permission.Cell, outsidePermission := Permission.Cell, protector := none } false = Except.ok { permission := Permission.Cell, accessed := false, idempotentForeignAccess := IdempotentForeignAccess.Write }

theorem Miri.TreeBorrows.RetagPolicy.unique_reborrow_starts_accessed : initialLocationState { freezePermission := Permission.Unique, nonfreezePermission := Permission.Unique, outsidePermission := Permission.ReservedFrz false, protector := none } true = Except.ok { permission := Permission.Unique, accessed := true, idempotentForeignAccess := IdempotentForeignAccess.None }