Exact eval_windows compiler constants at the TLS callback boundary. The source requests a particular module/name pair only on the Windows callback path. Missing rows and unsupported constants therefore remain demand-time Unknowns, while every successful value is decoded from the canonical named constant table with its exported type/layout checks.

@[reducible, inline]

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

Equations

• Miri.Input.EvalStartupWindows.Outer Os R P H D O Aff B Host = Miri.Input.EvalRuntimeConstruction.EntryOuter Os R P H D O Aff B Host

def Miri.Input.EvalStartupWindows.evalWindows {Os R P H D O Aff B Host : Type} (compiler : CompilerProviders.Prepared) : String → String → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Outer Os R P H D O Aff B Host) (Memory.Scalar Memory.Provenance)

Source-backed eval_windows(lib, name). In the pinned TLS path lib is the exact module component below std::sys::pal::windows; it is not matched by suffix or display name.

Equations

• Miri.Input.EvalStartupWindows.evalWindows compiler module name = Miri.Input.EvalStartupWindows.demand✝ (Miri.Input.CompilerWindowsConstants.scalar compiler.namedConstants module name)

def Miri.Input.EvalStartupWindows.mainFromExecution {Os R P H D O Aff B Host C ClockHost : Type} (compiler : CompilerProviders.Prepared) (execution : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalEntryMachine.InnerUser Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (deallocationError : Memory.MemoryLifecycleError → Interpreter.StepError) (deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalEntryMachine.InnerUser Os R P H D O Aff B Host) Unit) (choice : C) (layout : EvalEntryMachine.Layouts) (spans : Interpreter.AllocationDriver.SpanHooks) (platform : Interpreter.TlsPlatform) (format : Interpreter.ConstructorBinaryFormat) (externStatic : MIR.DefId → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Outer Os R P H D O Aff B Host) (Memory.Pointer Memory.Provenance)) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Outer Os R P H D O Aff B Host)) : Except Interpreter.StepError (Interpreter.MainMachine.Hooks (EvalEntryMachine.Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P)

Main/TLS assembly with the exact compiler-backed Windows constant leaf. All other capabilities remain the ones already derived from the same fixed execution Config and actual machine state.

Equations

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