Pinned Miri helpers.rs visit_freeze_sensitive / UnsafeCellVisitor, using rustc interpret/visitor.rs walk_value order. This visitor never reads a local discriminant or follows a pointer into its pointee. Compiler predicates, layout projection, dyn-vtable resolution and DST sizes are required leaves.

@[reducible, inline]

abbrev Miri.TreeBorrows.FreezeVisitor.M (S A : Type) : Type

Equations

• Miri.TreeBorrows.FreezeVisitor.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.TreeBorrows.FreezeVisitor.Hooks (P S : Type) : Type

The Boolean queries correspond to exact source type-kind tests; missing metadata must fail. projectBox implements project_to_ptr_in_box and returns its raw pointer field and allocator field, retaining layout/provenance.

• target : Memory.PointerArithmetic
• debugAssertions : Bool
• isUnsafeCell : MIR.TyId → M S Bool
• typeIsFreeze : MIR.TyId → M S Bool
• isDynamic : MIR.TyId → M S Bool
• isBox : MIR.TyId → M S Bool
• isTooGeneric : MIR.TyId → M S Bool
• sizeAndAlign : Interpreter.MPlaceTy P → M S (Option (ABI.Size × ABI.Align))
• unpackDynTrait : Interpreter.MPlaceTy P → M S (Interpreter.MPlaceTy P)
• projectBox : Interpreter.MPlaceTy P → M S (Interpreter.MPlaceTy P × Interpreter.MPlaceTy P)
• projectField : Interpreter.MPlaceTy P → Nat → M S (Interpreter.MPlaceTy P)
• arrayLength : Interpreter.MPlaceTy P → M S UInt64
• projectIndex : Interpreter.MPlaceTy P → UInt64 → M S (Interpreter.MPlaceTy P)

def Miri.TreeBorrows.FreezeVisitor.visitFreezeSensitive {P S : Type} (h : Hooks P S) (budget : Nat) (place : Interpreter.MPlaceTy P) (size : ABI.Size) (action : Memory.AllocRange → Bool → M S Unit) : M S Unit

Source helper including its debug size assertion and final zero-sized UnsafeCell at the wrapping end pointer, which flushes trailing frozen bytes.

Equations

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