Pinned eval.rs::MainThreadState::on_main_stack_empty (309-360), call_main (481-558), ty/instance.rs::Instance::mono (527-538), rustc_session/config/ sigpipe.rs::DEFAULT. Compiler queries, actual allocation/read/call operations remain required stateful leaves; source ordering and checks execute here.

inductive Miri.Interpreter.MainEntryType : Type

• miriStart : MainEntryType
• rustcMain (declaredSigpipe : UInt8) : MainEntryType

inductive Miri.Interpreter.MainGenericParameter : Type

• lifetime : MainGenericParameter
• typeParameter : MainGenericParameter
• constParameter : MainGenericParameter

structure Miri.Interpreter.MainSignature : Type

• hasBoundVariables : Bool
• outputHasBoundVariables : Bool
• returnType : MIR.TyId
• fnPointerType : MIR.TyId

  Compiler Ty::new_fn_ptr from the same entry signature.

inductive Miri.Interpreter.MainThreadStage (P : Type) : Type

• globalConstructors {P : Type} (entry : MIR.DefId) (entryType : MainEntryType) (argc argv : TlsImmediate P) : MainThreadStage P
• running {P : Type} : MainThreadStage P
• exiting {P : Type} (stage : ProgramExitStage) (exitCode : Int32) : MainThreadStage P

structure Miri.Interpreter.MainThreadState (P E H : Type) : Type

• constructors : GlobalCtorState P E H
• stage : MainThreadStage P
• mainReturnPlace : Option (MPlaceTy P)

inductive Miri.Interpreter.MainThreadError (Error : Type) : Type

• constructor {Error : Type} (error : TlsExecutionError Error) : MainThreadError Error
• programExit {Error : Type} (error : ProgramExitError Error) : MainThreadError Error
• scalar {Error : Type} (error : Memory.ScalarError) : MainThreadError Error
• leaf {Error : Type} (error : Error) : MainThreadError Error
• sourceInvariant {Error : Type} (message : String) : MainThreadError Error
• missingStartLangItem {Error : Type} : MainThreadError Error
• unresolvedStartInstance {Error : Type} : MainThreadError Error
• missingMainReturnPlace {Error : Type} : MainThreadError Error
• undefinedBehaviorExitCodeOutOfRange {Error : Type} (exitCode : Int64) : MainThreadError Error

@[instance_reducible]

instance Miri.Interpreter.instReprMainThreadError {Error✝ : Type} [Repr Error✝] : Repr (MainThreadError Error✝)

Equations

• Miri.Interpreter.instReprMainThreadError = { reprPrec := Miri.Interpreter.instReprMainThreadError.repr }

def Miri.Interpreter.instReprMainThreadError.repr {Error✝ : Type} [Repr Error✝] : MainThreadError Error✝ → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.MainThreadM (P E H Error A : Type) : Type

Equations

• Miri.Interpreter.MainThreadM P E H Error A = EStateM (Miri.Interpreter.MainThreadError Error) (Miri.Interpreter.MainThreadState P E H) A

structure Miri.Interpreter.MainThreadQueries (P E H Error : Type) : Type

• isizeLayout : ABI.TyAndLayout MIR.TyId
• u8Layout : ABI.TyAndLayout MIR.TyId
• genericParameters : MIR.DefId → MainThreadM P E H Error (Array MainGenericParameter)

  Includes parent parameters, in compiler GenericArgs::for_item order.

• allocate : ABI.TyAndLayout MIR.TyId → Memory.MemoryKind Memory.MiriMemoryKind → MainThreadM P E H Error (MPlaceTy P)

  Actual allocate(layout, MiriMemoryKind::Machine), including hooks.

• entrySignature : MIR.DefId → MainThreadM P E H Error MainSignature
• startLangItem : MainThreadM P E H Error (Option MIR.DefId)
• resolveInstance : MIR.DefId → Array MIR.GenericArg → MainThreadM P E H Error (Option CallInstance)

  Instance::try_resolve in the actual interpreter typing environment.

• fnPointer : CallInstance → MainThreadM P E H Error (Memory.Pointer P)
• layoutOf : MIR.TyId → MainThreadM P E H Error (ABI.TyAndLayout MIR.TyId)
• callFunction : CallInstance → Array (OpTy P) → MPlaceTy P → MainThreadM P E H Error Unit

  Actual call_function with Rust ABI and Stop{cleanup:true}.

• readTargetIsize : MPlaceTy P → MainThreadM P E H Error Int64

  Actual target-isize memory read, with pointer/initialization/borrow/race checks. An arbitrary precomputed integer does not satisfy this leaf.

def Miri.Interpreter.callMain {P E H Error : Type} (target : ABI.RuntimeTargetDataLayout) (queries : MainThreadQueries P E H Error) (entry : MIR.DefId) (entryType : MainEntryType) (argc argv : TlsImmediate P) : MainThreadM P E H Error Unit

Equations

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

def Miri.Interpreter.mainThreadOnStackEmpty {P E H Error ProvExtra : Type} [Memory.PointerProvenance P] (format : ConstructorBinaryFormat) (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (constructors : GlobalCtorQueries P E H Error) (main : MainThreadQueries P E H Error) (destructors : TlsDestructorQueries P E H Error) (termination : ThreadExitQueries P E H ProvExtra Error) : MainThreadM P E H Error ProgramExitPoll

Global ctor callbacks run before main is scheduled. Main's actual return memory is read only once its stack empties; signed i32 narrowing failure is UB. ProgramExit's machine-stop outcome propagates without reporting callback Ready.

Equations

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