Source-owned Windows configuration construction. Reuse the fixed MIR engine while deriving its foreign factory from compiler facts, the actual world and raw host leaves. No completed foreign dictionary is an input. The context retains the same live assembly factory for startup and later connection to Main/callbacks.

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.Other (Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalWindowsConfigurationCore.Other = Miri.Input.EvalWindowsCallDispatchConstruction.Other

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.Host (Poll Instant System H D Raw Listener TcpStream Error Native Profiler : Type) : Type

Equations

• Miri.Input.EvalWindowsConfigurationCore.Host = Miri.Input.EvalWindowsCallDispatchConstruction.Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.State (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalWindowsConfigurationCore.State = Miri.Input.EvalWindowsCallDispatchConstruction.State

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.CoreState (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalWindowsConfigurationCore.CoreState = Miri.Input.EvalWindowsCallDispatchConstruction.CoreState

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.Assembly (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp : Type) : Type

Equations

• Miri.Input.EvalWindowsConfigurationCore.Assembly = Miri.Input.EvalWindowsCallDispatchConstruction.Assembly

@[reducible, inline]

abbrev Miri.Input.EvalWindowsConfigurationCore.Context (Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error Meta Path Zone Timestamp : Type) : Type 1

Equations

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

def Miri.Input.EvalWindowsConfigurationCore.makeWithSourceConnection {Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error ErrorHost Meta Path AddrIter Zone Timestamp : Type} [DecidableEq Os] [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncPayload.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance AddrIter) (windowsHost : EvalWindowsEnvironmentConstruction.HostEffects (State Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error) (choice : C) (capacity : Nat) (connection : Option (Context Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error Meta Path Zone Timestamp → Assembly Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp → EStateM Interpreter.StepError (CoreState Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Assembly Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp))) (portableConnection : Option (Context Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error Meta Path Zone Timestamp → Interpreter.ForeignItems.Hooks Memory.Provenance (CoreState Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance → EStateM Interpreter.StepError (CoreState Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.ForeignItems.Hooks Memory.Provenance (CoreState Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance)) := none) : Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalConfigurationCore.SourceUser Os R EvalSyncPayload.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Other Raw Listener TcpStream Error) ABI.ExternAbi Instant × EvalConfigurationCore.ForeignContext Os R EvalSyncPayload.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C Instant (Assembly Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp))

Equations

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

def Miri.Input.EvalWindowsConfigurationCore.makeFromSourcePackage {Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error ErrorHost Meta Path AddrIter Zone Timestamp : Type} [DecidableEq Os] [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncPayload.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance AddrIter) (windowsHost : EvalWindowsEnvironmentConstruction.HostEffects (State Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error) (choice : C) (capacity : Nat) : Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalConfigurationCore.SourceUser Os R EvalSyncPayload.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Other Raw Listener TcpStream Error) ABI.ExternAbi Instant × Context Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error Meta Path Zone Timestamp)

Equations

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