Canonical source construction for Windows thread/TLS shims. Thread starts, joins, TLS keys and destructor identities all reuse the initialized Main hooks and their existing ThreadManager/TLS arena. The file-handle view is expected to come from the same source Windows file construction.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsThreadConstruction.State Os R P H D O Aff B Host = Miri.Interpreter.MainMachine.State (Miri.Input.EvalWindowsThreadConstruction.Payload Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalWindowsThreadConstruction.FileRef (H D O : Type) : Type

Equations

• Miri.Input.EvalWindowsThreadConstruction.FileRef H D O = Miri.Interpreter.WindowsFileMachine.Ref H D O

def Miri.Input.EvalWindowsThreadConstruction.fromSource [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host C Error : Type} (p : CompilerProviders.Prepared) (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (environment : Interpreter.WindowsEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind) (handles : Interpreter.WindowsHandles.Hooks (State Os R P H D O Aff B Host) (FileRef H D O)) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (compatibilityBudget : Nat) : Except Interpreter.StepError (Interpreter.WindowsThreadDispatch.Hooks (State Os R P H D O Aff B Host) (FileRef H D O))

Equations

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