Construct target OS-string operations from the canonical machine memory and allocation engines. Only host OsStr representation/conversion remains a host capability; target byte/UTF-16 access and array allocation use Miri state.

@[reducible, inline]

abbrev Miri.Input.EvalHostRuntimeConstruction.RuntimeState (U : Type) : Type

Equations

• Miri.Input.EvalHostRuntimeConstruction.RuntimeState U = Miri.Interpreter.MachineHooks.State Miri.Memory.MiriMemoryKind (Miri.Interpreter.PointerMachine.User U)

@[reducible, inline]

abbrev Miri.Input.EvalHostRuntimeConstruction.RuntimeM (U A : Type) : Type

Equations

• Miri.Input.EvalHostRuntimeConstruction.RuntimeM U A = Miri.Interpreter.MachineHooks.M Miri.Memory.MiriMemoryKind (Miri.Interpreter.PointerMachine.User U) A

These operations are properties of the actual host OsStr implementation. They are intentionally separate from target memory operations below.

structure Miri.Input.EvalHostRuntimeConstruction.OsHostEffects (Os : Type) : Type

• hostWindows : Bool
• hostUnix : Bool
• targetWindows : Bool
• fromUnixBytes : ByteArray → Os
• fromUtf8 : ByteArray → Except Interpreter.StepError Os
• fromWide : Array UInt16 → Except Interpreter.StepError Os
• toWide : Os → Except Interpreter.StepError (Array UInt16)
• encodedBytes : Os → ByteArray
• encodedLength : Os → Nat
• decodeUnixBytes : ByteArray → Except Interpreter.StepError Os
• empty : Os
• concat : Os → Os → Os
• ascii : String → Os
• isEmpty : Os → Bool
• containsEquals : Os → Bool

structure Miri.Input.EvalHostRuntimeConstruction.EnvironmentLens (U Os : Type) : Type

• get : Interpreter.PointerMachine.User U → Interpreter.EnvVars.State (Option Memory.Provenance) Os
• set : Interpreter.PointerMachine.User U → Interpreter.EnvVars.State (Option Memory.Provenance) Os → Interpreter.PointerMachine.User U

structure Miri.Input.EvalHostRuntimeConstruction.ExternStaticLens (U : Type) : Type

• get : Interpreter.PointerMachine.User U → Interpreter.ExternStatic.State
• set : Interpreter.PointerMachine.User U → Interpreter.ExternStatic.State → Interpreter.PointerMachine.User U

structure Miri.Input.EvalHostRuntimeConstruction.ExternStaticTarget : Type

• os : String
• env : String
• families : Array String

def Miri.Input.EvalHostRuntimeConstruction.ExternStaticTarget.fromCompiler (facts : CompilerExternStatic.TargetFacts) : ExternStaticTarget

Equations

• Miri.Input.EvalHostRuntimeConstruction.ExternStaticTarget.fromCompiler facts = { os := facts.os, env := facts.env, families := facts.families }

structure Miri.Input.EvalHostRuntimeConstruction.EnvironmentHostEffects (U : Type) : Type

• invalidArgument : RuntimeM U Int32
• envVarNotFound : RuntimeM U Unit

structure Miri.Input.EvalHostRuntimeConstruction.EnvironmentMemory (U C Payload : Type) : Type

• access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)
• allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)
• deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → RuntimeM U Unit

  Operation-local source deallocation. This runs in the real MachineHooks state so current span, free allocation identity, address reuse, and all partial effects observe the active frame instead of a captured startup state.

• pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind U
• projection : Interpreter.PlaceProjectionHooks Memory.Provenance (RuntimeState U) C Interpreter.MachineHooks.FrameExtra
• arrays : RuntimeArrayQueries.Access (RuntimeState U)
• symbolicAlignment : Bool
• enforceAlignment : Bool
• stringScanBudget : Nat
• choice : C
• pointerTy : MIR.TyId
• pointerLayout : Interpreter.LocalLayout

def Miri.Input.EvalHostRuntimeConstruction.osStrings {Os U : Type} [DecidableEq Memory.MiriMemoryKind] (host : OsHostEffects Os) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind U) (arrays : RuntimeArrayQueries.Access (RuntimeState U)) (symbolicAlignment enforceAlignment : Bool) (budget : Nat) : Interpreter.OsStrings.Hooks Memory.Provenance (RuntimeState U) Os Interpreter.EnvVars.Kind

Build OsStrings.Hooks with the source access and allocation records. The array type identity is interned in the same persistent runtime-type world used by EntryArguments; byte-size coincidence never substitutes for Ty::new_array.

Equations

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

def Miri.Input.EvalHostRuntimeConstruction.osStringsFromMemory {Os U C Payload : Type} (host : OsHostEffects Os) (memory : EnvironmentMemory U C Payload) : Interpreter.OsStrings.Hooks Memory.Provenance (RuntimeState U) Os Interpreter.EnvVars.Kind

Equations

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

def Miri.Input.EvalHostRuntimeConstruction.envVars {Os U C : Type} [DecidableEq Memory.MiriMemoryKind] (host : OsHostEffects Os) (hostEffects : EnvironmentHostEffects U) (lens : EnvironmentLens U Os) (family : Interpreter.ForeignItems.Family) (strings : Interpreter.OsStrings.Hooks Memory.Provenance (RuntimeState U) Os Interpreter.EnvVars.Kind) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)) (deallocate : Memory.Pointer (Option Memory.Provenance) → Interpreter.EnvVars.Kind → RuntimeM U Unit) (machinePointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind U) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (RuntimeState U) C Interpreter.MachineHooks.FrameExtra) (arrays : RuntimeArrayQueries.Access (RuntimeState U)) (choice : C) (pointerTy : MIR.TyId) (pointerLayout : Interpreter.LocalLayout) : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (RuntimeState U)

Source environment allocation and pointer-cell operations built from the same canonical access, allocation and projection engines as MIR. State access is only a lens into MachineGCRoots.Storage; no parallel environment map is created. Host errno/Win32-not-found effects remain explicit.

Equations

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

def Miri.Input.EvalHostRuntimeConstruction.envVarsFromSource {Os U C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (host : OsHostEffects Os) (hostEffects : EnvironmentHostEffects U) (lens : EnvironmentLens U Os) (family : Interpreter.ForeignItems.Family) (memory : EnvironmentMemory U C Payload) : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (RuntimeState U)

Equations

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

def Miri.Input.EvalHostRuntimeConstruction.externStaticsFromSource {U Os C Payload Other : Type} [DecidableEq Memory.MiriMemoryKind] (target : ExternStaticTarget) (environment : EnvironmentLens U Os) (externStatics : ExternStaticLens U) (memory : EnvironmentMemory U C Payload) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (Interpreter.PointerMachine.User U) Other) (dynamicValue : String → Other) (u8Layout usizeLayout : Interpreter.LocalLayout) : Interpreter.ExternStatic.InitHooks (RuntimeState U)

Construct init_extern_statics from real allocation, typed scalar writes, the actual environment root, exact source dynamic-symbol allowlists and the canonical FunctionPointers registry. dynamicValue only embeds the source DynSym value into the caller's concrete Other representation.

Equations

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