Canonical eval.rs main/constructors/exit callback execution. Existing GlobalConstructors and callMain source policy is reused through transient typed views; all calls, return memory, TLS, termination and scheduler actions use actual full machine state and retain failed prefixes.

@[reducible, inline]

abbrev Miri.Interpreter.MainMachine.State (U : Type) : Type

Equations

• Miri.Interpreter.MainMachine.State = Miri.Interpreter.ThreadTlsMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.MainMachine.M (U A : Type) : Type

Equations

• Miri.Interpreter.MainMachine.M = Miri.Interpreter.ThreadTlsMachine.M

@[reducible, inline]

abbrev Miri.Interpreter.MainMachine.MainView (U : Type) : Type

Equations

• Miri.Interpreter.MainMachine.MainView U = Miri.Interpreter.MainThreadState Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree (Miri.Interpreter.MainMachine.State U)

structure Miri.Interpreter.MainMachine.Data : Type

• token : Nat
• stage : MainThreadStage Memory.Provenance
• constructors : GlobalCtorStage Memory.Provenance
• tls : TlsDtorsStage Memory.Provenance

structure Miri.Interpreter.MainMachine.Hooks (U C O X F A Aff Payload : Type) : Type 1

• termination : ThreadTerminationMachine.Hooks U C O X F A Aff Payload
• functions : FunctionPointers.Hooks Memory.MiriMemoryKind (ThreadStacks.Storage U) O
• access : PlaceMachine.AccessConfig Memory.MiriMemoryKind (ThreadStacks.Storage U)
• layouts : EntryArguments.Layouts
• data : U → Option Data
• putData : U → Option Data → U
• entry : U → MachineGCRoots.EntryPointers
• putEntry : U → MachineGCRoots.EntryPointers → U
• format : ConstructorBinaryFormat
• cNoUnwind : X
• lookupLinkSection : (String → Bool) → M U (Array (TlsImmediate Memory.Provenance × MIR.SpanRef))
• genericParameters : MIR.DefId → M U (Array MainGenericParameter)
• entrySignature : MIR.DefId → M U MainSignature
• startLangItem : M U (Option MIR.DefId)
• resolveInstance : MIR.DefId → Array MIR.GenericArg → M U (Option CallInstance)
• layoutOf : MIR.TyId → M U LocalLayout

def Miri.Interpreter.MainMachine.withTerminationPayload {U C O X F A Aff P Q : Type} (h : Hooks U C O X F A Aff P) : Hooks U C O X F A Aff Q

Reassociate the unused termination-payload type parameter. The actual world payload, TLS/thread hooks, entry roots and every machine action remain the original ones; no synchronization metadata is converted.

Equations

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

def Miri.Interpreter.MainMachine.mainQueries {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (choice : C) (token : Nat) : MainThreadQueries Memory.Provenance TreeBorrows.BorrowTree (State U) StepError

Equations

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

def Miri.Interpreter.MainMachine.constructors {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (choice : C) : GlobalCtorQueries Memory.Provenance TreeBorrows.BorrowTree (State U) StepError

Equations

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

def Miri.Interpreter.MainMachine.invoke {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (choice : C) : M U StackEmptyPoll

One source main callback invocation, excluding scheduler take/restore. Existing source ctor/callMain policies execute; exit uses the canonical ThreadTerminationMachine so TLS/free/join callbacks do not pass through stale memory-only legacy lifecycle hooks.

Equations

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

inductive Miri.Interpreter.MainMachine.Callback : Type

• main (token : Nat) : Callback
• tls (callback : ThreadLoops.TakenTls) : Callback

def Miri.Interpreter.MainMachine.take {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) : M U Callback

Main and ordinary TLS closures share one actual scheduler callback path. Each callback is taken once; program-stop/error leaves it consumed.

Equations

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

def Miri.Interpreter.MainMachine.restore {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) : Callback → M U Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.MainMachine.restore h (Miri.Interpreter.MainMachine.Callback.tls callback) = Miri.Interpreter.ThreadLoops.restore h.termination.tls callback

def Miri.Interpreter.MainMachine.bindLoop {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (base : RunLoopHooks (State U) C Callback) (scheduler : C → ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) : RunLoopHooks (State U) C Callback

Equations

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

def Miri.Interpreter.MainMachine.install {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (entry : MIR.DefId) (entryType : MainEntryType) (args : EntryArguments.Arguments) (windows : Bool) : M U Unit

The final late_init thread step installs the actual captured main stage. EnvVars and extern-static initialization must precede this source operation.

Equations

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