Pinned Miri machine hooks for frame-local clocks, retag scopes and protector lifecycle. Compiler/memory leaves remain explicit effects.

structure Miri.Interpreter.MachineHooks.CatchUnwindData : Type

• catchFn : Memory.Pointer (Option Memory.Provenance)
• data : RvalueImmTy Memory.Provenance
• dest : MPlaceTy Memory.Provenance
• ret : Option MIR.BasicBlockId

structure Miri.Interpreter.MachineHooks.FrameExtra : Type

Semantic FrameExtra fields; profiling-only timing is omitted.

• borrowTracker : Option TreeBorrows.FrameState
• catchUnwind : Option CatchUnwindData
• userRelevance : UInt8
• dataRace : Option Concurrency.LocalRace.FrameState

structure Miri.Interpreter.MachineHooks.BorrowState : Type

• global : TreeBorrows.GlobalState
• retagMode : TreeBorrows.RetagPolicy.RetagMode

structure Miri.Interpreter.MachineHooks.MachineState (K User : Type) : Type

Allocation race extras are keyed by the same canonical AllocId as live memory; this external index composes with the existing BorrowTree extra type. Allocation lifecycle adapters must install/remove entries with their allocation.

• memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K
• borrowTracker : Option BorrowState
• dataRace : Option Concurrency.GlobalState
• threads : Concurrency.ThreadManager
• raceAllocations : Array (Memory.AllocId × Concurrency.VClockAlloc)
• allocationSpans : Array (Memory.AllocId × MIR.SpanRef × Option MIR.SpanRef)
• user : User

@[reducible, inline]

abbrev Miri.Interpreter.MachineHooks.State (K User : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.MachineHooks.M (K User A : Type) : Type

Equations

• Miri.Interpreter.MachineHooks.M K User A = EStateM Miri.Interpreter.StepError (Miri.Interpreter.MachineHooks.State K User) A

def Miri.Interpreter.MachineHooks.currentFrame {K User : Type} : M K User (Frame Memory.Provenance LocalLayout FrameExtra)

Equations

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

def Miri.Interpreter.MachineHooks.setCurrentFrame {K User : Type} (frame : Frame Memory.Provenance LocalLayout FrameExtra) : M K User Unit

Equations

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

def Miri.Interpreter.MachineHooks.afterLocalRead {K User : Type} (localId : MIR.LocalId) : M K User Unit

Source machine after_local_read. LocalAccess already skips this hook for indirect operands and while validation is in progress.

Equations

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

def Miri.Interpreter.MachineHooks.afterLocalWrite {K User : Type} (localId : MIR.LocalId) (storageLive : Bool) : M K User Unit

Source machine after_local_write. The storage-live bit changes the clock transition; it is never treated as an ordinary overwrite.

Equations

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

def Miri.Interpreter.MachineHooks.localAccessAfterRead {K User : Type} (frame : Frame Memory.Provenance LocalLayout FrameExtra) (machine : MachineState K User) (localId : MIR.LocalId) : LocalAccessResult Memory.Provenance FrameExtra (MachineState K User) Unit

LocalAccess's frame/state callback boundary, preserving the canonical frame-local clock map instead of copying it into an unrelated side state.

Equations

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

structure Miri.Interpreter.MachineHooks.StorageHooks (K User : Type) : Type

Required layout and stack-memory leaves. Whole-state storage operations below preserve FrameExtra changes made by afterLocalWrite and allocation.

• veryTriviallySized : MIR.TyId → Except StepError Bool
• layout : MIR.LocalId → M K User LocalLayout
• allocateDyn : LocalLayout → MemPlaceMeta Memory.Provenance → M K User (MemPlace Memory.Provenance)
• deallocateStack : Memory.Pointer (Option Memory.Provenance) → M K User Unit

@[simp]

theorem Miri.Interpreter.MachineHooks.storageResult_ok {A K User : Type} (value : A) : Miri.Interpreter.MachineHooks.fromStack✝ (Except.ok value) = pure value

A successful stack result introduces no machine effect. This public rule lets client proofs use the storage driver without naming its private adapter.

@[simp]

theorem Miri.Interpreter.MachineHooks.deallocateLocal_dead {K User : Type} (hooks : StorageHooks K User) : Miri.Interpreter.MachineHooks.deallocateLocal✝ hooks LocalValue.dead = pure ()

Dead local storage owns no allocation to deallocate.

def Miri.Interpreter.MachineHooks.storageLiveDyn {K User : Type} (hooks : StorageHooks K User) (localId : MIR.LocalId) (metadata : MemPlaceMeta Memory.Provenance) : M K User Unit

Canonical whole-state source storage_live_dyn. The generic Frame operation cannot itself install FrameExtra mutations made by a machine hook; this binding uses current Frame methods after each hook so local-race/protector state survives.

Equations

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

def Miri.Interpreter.MachineHooks.storageDead {K User : Type} (hooks : StorageHooks K User) (localId : MIR.LocalId) : M K User Unit

Equations

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

def Miri.Interpreter.MachineHooks.initFrame {K User : Type} (relevance : Frame Memory.Provenance LocalLayout Unit → M K User UInt8) (frame : Frame Memory.Provenance LocalLayout Unit) : M K User (Frame Memory.Provenance LocalLayout FrameExtra)

Source init_frame semantic fields. New frames have empty protected-tag and local-clock sets exactly when their corresponding machine backend is enabled.

Equations

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

def Miri.Interpreter.MachineHooks.afterLocalMovedToMemory {K User : Type} (localId : MIR.LocalId) (place : MPlaceTy Memory.Provenance) (localSpan : MIR.Body → MIR.LocalId → M K User MIR.SpanRef) : M K User Unit

Source after_local_moved_to_memory records declaration span before fetching allocation extras, then transfers local timestamps to every byte.

Equations

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

def Miri.Interpreter.MachineHooks.memoryRaceAccess {K User : Type} (machine : MachineState K User) (allocId : Memory.AllocId) (range : Memory.AllocRange) (writeType : Option Concurrency.NaWriteType) (readType : Concurrency.NaReadType) : MachineState K User × Except StepError Unit

Allocation-level vector-clock read/write binding. The outer machine memory hook must still perform weak-memory invalidation (writes), Tree Borrows and sync-object access in source order; this function is the data-race stage only.

Equations

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

def Miri.Interpreter.MachineHooks.memoryRaceRead {K User : Type} (allocId : Memory.AllocId) (range : Memory.AllocRange) (readType : Concurrency.NaReadType) : M K User Unit

Equations

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

def Miri.Interpreter.MachineHooks.memoryRaceWrite {K User : Type} (allocId : Memory.AllocId) (range : Memory.AllocRange) (writeType : Concurrency.NaWriteType) : M K User Unit

Equations

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

def Miri.Interpreter.MachineHooks.withRetagMode {K User A : Type} (mode : TreeBorrows.RetagPolicy.RetagMode) (action : M K User A) : M K User A

Source with_retag_mode restores the old mode after both success and error. A disabled borrow tracker runs the body directly, as in machine.rs.

Equations

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

structure Miri.Interpreter.MachineHooks.Hooks (K User : Type) : Type

Required typed pointer queries and memory effects around the existing Tree Borrows core. prepare* returns all explicit RetagPipeline leaf results; no successful request is generated for missing compiler or pointer facts.

• preparePointerRetag : RvalueImmTy Memory.Provenance → MIR.TyId → TreeBorrows.RetagPolicy.RetagMode → M K User TreeBorrows.RetagPipeline.Request
• reconstructImmediate : RvalueImmTy Memory.Provenance → Option Memory.Provenance → M K User (RvalueImmTy Memory.Provenance)
• preparePlaceProtection : MPlaceTy Memory.Provenance → M K User TreeBorrows.RetagPipeline.Request
• writeUninit : MPlaceTy Memory.Provenance → M K User Unit
• ensureTreeExtra : Memory.AllocId → M K User Unit

  Source get_alloc_extra may materialize a compiler global or fail (extern static).

def Miri.Interpreter.MachineHooks.retagPtrValue {K User : Type} [DecidableEq K] (hooks : Hooks K User) (value : RvalueImmTy Memory.Provenance) (ty : MIR.TyId) : M K User (Option (RvalueImmTy Memory.Provenance))

Equations

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

def Miri.Interpreter.MachineHooks.protectionPolicy : TreeBorrows.RetagPolicy.NewPermission

This policy is exactly tb_protect_place's explicit NewPermission.

Equations

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

theorem Miri.Interpreter.MachineHooks.protectionPolicy_eq : TreeBorrows.RetagPolicy.create { isUnpin := true, isUnsafeUnpin := true, isFreeze := true } TreeBorrows.RetagPolicy.ReferenceKind.Mutable TreeBorrows.RetagPolicy.RetagMode.FnEntry { implicitWrites := false, rustcNoWritable := false } = some protectionPolicy

Reuse the existing reborrow core with a policy whose equality to the source explicit protector policy is kernel checked below.

def Miri.Interpreter.MachineHooks.protectInPlaceFunctionArgument {K User : Type} [DecidableEq K] (hooks : Hooks K User) (place : MPlaceTy Memory.Provenance) : M K User Unit

Source protect-place retags first, then writes uninit through the newly protected tag. Errors retain allocated tags, tree effects and write effects.

Equations

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

def Miri.Interpreter.MachineHooks.beforeStackPopWithEnsure {K User : Type} [DecidableEq K] (ensureTreeExtra : Memory.AllocId → M K User Unit) : M K User Unit

Source on_stack_pop releases each live allocation's protector while all protectors remain registered, commits partial tree mutations on failure, and only removes global protectors once every release succeeds.

Equations

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

def Miri.Interpreter.MachineHooks.beforeStackPop {K User : Type} [DecidableEq K] (hooks : Hooks K User) : M K User Unit

Compatibility entrypoint for legacy request-based fixture dictionaries.

Equations

• Miri.Interpreter.MachineHooks.beforeStackPop hooks = Miri.Interpreter.MachineHooks.beforeStackPopWithEnsure hooks.ensureTreeExtra

def Miri.Interpreter.MachineHooks.run {K User A : Type} (action : M K User A) (state : State K User) : StepResult (State K User) A

Direct adapters for the Call/Rvalue hooks use these EStateM functions. This runner retains error-state effects in the canonical StepResult format.

Equations

• Miri.Interpreter.MachineHooks.run action state = Miri.Interpreter.Call.run action state