eval.rs:390–471,641–710: actual immutable argument/argv/root-cell memory and Windows command-line encoding. Compiler array-layout queries retain real TyIds; projected indices execute the existing effectful canonical Place path.

def Miri.Interpreter.EntryArguments.windowsCommandLine (args : Array String) : Except StepError (Array UInt16)

Source initialization panics are explicit invalid-program results, never host exceptions. Empty argv produces exactly one UTF-16 zero.

Equations

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

structure Miri.Interpreter.EntryArguments.Layouts : Type

• isize : LocalLayout
• u8 : LocalLayout
• u16 : LocalLayout
• u8Pointer : LocalLayout
• u8PointerPointer : LocalLayout

structure Miri.Interpreter.EntryArguments.Arguments : Type

• argc : RvalueImmTy Memory.Provenance
• argv : RvalueImmTy Memory.Provenance

structure Miri.Interpreter.EntryArguments.Hooks (K User AddressPayload AllocPayload C : Type) : Type

• addresses : FunctionPointers.AddressLens User AddressPayload
• allocation : PlaceMachine.AllocationConfig K (PointerMachine.User AddressPayload)

  This is the already source-assembled allocation config. Its tail and root-address callback own extras and the persistent choice tape.

• arithmetic : Memory.PointerArithmetic
• access : PlaceMachine.AccessConfig K User
• place : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra
• layouts : Layouts
• arrayLayout : C → MIR.TyId → UInt64 → MachineHooks.M K User LocalLayout

  Ty::new_array(element,count) and layout_of in the actual typing environment.

• entryPointers : User → MachineGCRoots.EntryPointers
• putEntryPointers : User → MachineGCRoots.EntryPointers → User
• windows : Bool
• isNoCore : MachineHooks.M K User Bool
• coreSentinelMirAvailable : MachineHooks.M K User Bool

def Miri.Interpreter.EntryArguments.setup {K User AP EP C : Type} [DecidableEq K] (h : Hooks K User AP EP C) (choice : C) (machineKind : K) (args : Array String) : MachineHooks.M K User Arguments

The exact source initialization order: all strings, argv array, argc cell, argv cell, optional UTF-16 command line, then return typed argc/argv for the captured main callback. Every byte/scalar write invokes real memory policies.

Equations

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

def Miri.Interpreter.EntryArguments.initializeMiri {User AP EP C : Type} (h : Hooks Memory.MiriMemoryKind User AP EP C) (choice : C) (args : Array String) : MachineHooks.M Memory.MiriMemoryKind User Arguments

Actual Miri source kind, without choosing ownership from a layout size.

Equations

• Miri.Interpreter.EntryArguments.initializeMiri h choice args = Miri.Interpreter.EntryArguments.setup h choice Miri.Memory.MiriMemoryKind.machine args