Source-owned Windows environment component construction. Guest environment storage, wide-string memory and scalar access use the existing EvalWorld and compiler providers. Only the host path/process operations remain raw leaves.

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsEnvironmentConstruction.Payload Os R P H D O Aff B Host = Miri.Input.EvalExecutable.U Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsEnvironmentConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalStartupAssembly.State Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsEnvironmentConstruction.InnerControl Os R P H D O Aff B Host = Miri.Input.EvalStartupAssembly.InnerControl Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsEnvironmentConstruction.Memory (Os R P H D O Aff B Host C : Type) : Type

Equations

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

structure Miri.Input.EvalWindowsEnvironmentConstruction.HostEffects (S Os E : Type) : Type

• communicate : Bool
• isolatedOp : EvalUnixConstruction.IsolatedOp
• hostPid : EStateM Interpreter.StepError S UInt32
• currentDirectory : EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Os)
• setCurrentDirectory : Os → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Unit)
• userHomeDirectory : EStateM Interpreter.StepError S (Option Os)
• temporaryDirectory : EStateM Interpreter.StepError S Os

def Miri.Input.EvalWindowsEnvironmentConstruction.fromSource {Os R P H D O Aff B Host C Error : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (InnerControl Os R P H D O Aff B Host)) (memory : Memory Os R P H D O Aff B Host C) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (errors : Interpreter.IoError.Hooks (State Os R P H D O Aff B Host) Error) (hostConfig : HostEffects (State Os R P H D O Aff B Host) Os Error) : Except Interpreter.StepError (Interpreter.WindowsEnvironment.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind)

Assemble the exact Windows environment hooks for the already initialized source world. Construction does not create another environment map or process identity; guest variables live in the canonical EnvVars root.

Equations

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