Concrete machine bindings for the Miri-only extern driver. The user-state lens must target the same static/tracked allocation lists as machine exit. Pointers, symbolic alignment, payloads, threads and GC use their canonical state.

@[reducible, inline]

abbrev Miri.Interpreter.MiriShimMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.MiriShimMachine.State = Miri.Interpreter.PointerMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.MiriShimMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.MiriShimMachine.M = Miri.Interpreter.PointerMachine.M

structure Miri.Interpreter.MiriShimMachine.Bookkeeping : Type

• trackedAllocations : Array Memory.AllocId
• staticRoots : Array Memory.AllocId

structure Miri.Interpreter.MiriShimMachine.Hooks (K U C E Other : Type) : Type

• access : PlaceMachine.AccessConfig K (PointerMachine.User U)
• pointer : PointerMachine.Hooks K U
• place : PlaceHooks Memory.Provenance (State K U) C E
• bookkeeping : U → Bookkeeping
• setBookkeeping : Bookkeeping → U → U
• cAllocation : Memory.MemoryKind K → Bool
• u64Layout : C → M K U LocalLayout
• boolLayout : C → M K U LocalLayout
• usizeLayout : C → M K U LocalLayout
• unwind : Unwind.Hooks K (PointerMachine.User U) C Other
• gc : ProvenanceGC.Hooks K (PointerMachine.User U)

def Miri.Interpreter.MiriShimMachine.allocation {K U C E Other : Type} (h : Hooks K U C E Other) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K U (Except StepError (Memory.AllocId × ABI.Size))

Source failed ptr_get_alloc_id is a value until the calling arm applies its error policy. This conversion retains all effects from pointer resolution.

Equations

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

def Miri.Interpreter.MiriShimMachine.symbolicPromise {K U C E Other : Type} (h : Hooks K U C E Other) (pointer : Memory.Pointer (Option Memory.Provenance)) (alignment : ABI.Align) : M K U Unit

No allocation/liveness check is imposed here: source promises are recorded for any resolved provenance, including dead allocations, using actual offset.

Equations

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

def Miri.Interpreter.MiriShimMachine.core {K U C E Other D B I HostPath : Type} [DecidableEq K] (h : Hooks K U C E Other) (choice : C) (base : MiriShims.CoreHooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I HostPath) : MiriShims.CoreHooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I HostPath

Construct the source Miri operations over the canonical machine while keeping host paths, diagnostics, output, and other source effects explicit. This constructor accepts the nonrecursive CoreHooks projection, so callers do not need to manufacture a complete ForeignItems dispatch record just to bind the physical memory/provenance/thread effects.

Equations

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

def Miri.Interpreter.MiriShimMachine.bind {K U C E Other D B I HostPath : Type} [DecidableEq K] (h : Hooks K U C E Other) (choice : C) (base : MiriShims.Hooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I HostPath) : MiriShims.Hooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I HostPath

ABI, host paths, actual thread creation/join and diagnostic ancestry remain required until their source dictionaries are installed. No success defaults.

Equations

• Miri.Interpreter.MiriShimMachine.bind h choice base = { toOperations := (Miri.Interpreter.MiriShimMachine.core h choice base.core).toOperations, foreign := base.foreign }