Source foreign_items.rs::exit and Windows ExitProcess share the actual ProgramExitHandler::ExitCalled state machine. Its FnMut capture is stored in World, separate from main/TLS and FnOnce unblock environments.

@[reducible, inline]

abbrev Miri.Input.EvalForeignExit.World (Os R Payload H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalForeignExit.World = Miri.Input.EvalWorld.World

@[reducible, inline]

abbrev Miri.Input.EvalForeignExit.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalForeignExit.User Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalForeignExit.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalForeignExit.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalForeignExit.State Os R P H D O Aff B Host = Miri.Interpreter.ThreadStacks.State Miri.Memory.MiriMemoryKind (Miri.Input.EvalForeignExit.User Os R P H D O Aff B Host)

def Miri.Input.EvalForeignExit.startSource {Os R P H D O Aff B Host : Type} (spans : Interpreter.AllocationDriver.SpanHooks) (code : Int32) : EStateM Interpreter.StepError (State Os R P H D O Aff B Host) Unit

Source replace_active_thread_stack needs only current-user span metadata; all callback/entry/runtime fields are read from their canonical World owners.

Equations

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

def Miri.Input.EvalForeignExit.startInnerSource {Os R P H D O Aff B Host : Type} (spans : Interpreter.AllocationDriver.SpanHooks) (code : Int32) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Inner (World Os R P H D O Aff B Host)) Unit

Equations

• Miri.Input.EvalForeignExit.startInnerSource spans code = Miri.Interpreter.ExecutionStateTransport.reverseAction (Miri.Input.EvalForeignExit.startSource spans code)

def Miri.Input.EvalForeignExit.hooks {Os R P H D O Aff B Host C X F A Payload : Type} (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Host) C O X F A Aff Payload) : Interpreter.WindowsExitMachine.Hooks (User Os R P H D O Aff B Host) C O X F A Aff Payload

Equations

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

def Miri.Input.EvalForeignExit.start {Os R P H D O Aff B Host C X F A Payload : Type} (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Host) C O X F A Aff Payload) (code : Int32) : EStateM Interpreter.StepError (State Os R P H D O Aff B Host) Unit

Equations

• Miri.Input.EvalForeignExit.start main code = Miri.Interpreter.WindowsExitMachine.start (Miri.Input.EvalForeignExit.hooks main) code

def Miri.Input.EvalForeignExit.startInner {Os R P H D O Aff B Host C X F A Payload : Type} (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Host) C O X F A Aff Payload) (code : Int32) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Inner (World Os R P H D O Aff B Host)) Unit

Equations

• Miri.Input.EvalForeignExit.startInner main code = Miri.Interpreter.ExecutionStateTransport.reverseAction (Miri.Input.EvalForeignExit.start main code)

def Miri.Input.EvalForeignExit.loop {Os R P H D O Aff B Host C X F A Payload : Type} (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Host) C O X F A Aff Payload) (base : Interpreter.RunLoopHooks (State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) : Interpreter.RunLoopHooks (Interpreter.WindowsExitMachine.State (User Os R P H D O Aff B Host)) C Interpreter.WindowsExitMachine.Callback

Equations

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