Source construction for the native Unix file-descriptor dispatch family. Only actual host filesystem/path/resource effects, random choices, and source socket/event operations remain inputs. ABI checks, path reads, descriptor ownership/readiness, control dispatch, and vectored memory behavior use the canonical compiler and EvalWorld components.

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixNativeFdConstruction.Other Raw Listener TcpStream Error = Miri.Input.EvalSocketStorage.Other Raw Listener TcpStream Error

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixNativeFdConstruction.FD (H D O : Type) : Type

Equations

• Miri.Input.EvalUnixNativeFdConstruction.FD H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

@[reducible, inline]

abbrev Miri.Input.EvalUnixNativeFdConstruction.M (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error A : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixNativeFdConstruction.ExecConfig (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C ClockHost : Type) : Type 1

Equations

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

structure Miri.Input.EvalUnixNativeFdConstruction.OpenHostEffects (S H D E Meta Path Os : Type) : Type

• pathFromOs : Os → Path

  Conversion from the host OsString representation to this host's Path.

• isAbsolute : Path → Bool
• isEmpty : Path → Bool
• isDot : Path → Bool
• emptyPath : Path
• procAbsolute : Path → EStateM Interpreter.StepError S Bool

  Exact host path::absolute(...).is_ok_and(starts_with("/proc")).

• diagnoseProc : EStateM Interpreter.StepError S Unit
• hostCustomFlag : Interpreter.UnixOpen.Flag → EStateM Interpreter.StepError S UInt32
• openFile : Option D → Path → Interpreter.UnixOpen.Options → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) H)
• openDirectoryAsFile : Option D → Path → Interpreter.UnixOpen.Options → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) H)
• metadata : H → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Interpreter.UnixOpen.Metadata)
• asDirectory : H → EStateM Interpreter.StepError S D

structure Miri.Input.EvalUnixNativeFdConstruction.OtherPositionalEffects (S H D O E : Type) : Type

• read : FD H D O → UInt64 → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S E → EStateM Interpreter.StepError S Unit
• write : FD H D O → UInt64 → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S E → EStateM Interpreter.StepError S Unit

structure Miri.Input.EvalUnixNativeFdConstruction.Components (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I : Type) (ShimBody : Type := B) : Type

• files : Interpreter.Files.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta
• registry : Interpreter.FileMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)
• readiness : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)
• fd : Interpreter.UnixFdDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta Path
• control : Interpreter.UnixFdControlDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta Place ShimBody I
• vector : Interpreter.UnixVectoredDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta Place ShimBody I

def Miri.Input.EvalUnixNativeFdConstruction.fromSourceWithLifecycle {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C Payload ShimBody I Host ClockHost : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (compatibilityBudget typeBudget : Nat) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (openHost : OpenHostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D Error Meta Path Os) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Payload) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error Interpreter.EnvVars.Kind) (resources : EvalUnixIoConstruction.FileResourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta) (otherFiles : EvalUnixIoConstruction.OtherFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (positional : OtherPositionalEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (fileLocks : EvalUnixIoConstruction.FileLockEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) (controlEffects : EvalUnixIoConstruction.ControlSourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (signatures : Interpreter.ShimSignatures.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ShimBody I) (readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (watcherReferenceBudget fileReferenceBudget hostUsizeBits : Nat) (shortFdOperations : Bool) (hostIsizeBits : Nat) (randomShort : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Bool) (communicate : Bool) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (isolatedOp : EvalUnixConstruction.IsolatedOp) (pollAndUnblockZero : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Unit) (descriptor : Interpreter.SocketMachine.Descriptor (Other Raw Listener TcpStream Error)) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Host) (checkedSum : Bool) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) (compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) C) (projectionHooks : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (spans : Interpreter.AllocationDriver.SpanHooks) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) P) (diagnostic : Memory.AllocId → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) Unit) (nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) Unit)) : Except Interpreter.StepError (Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I ShimBody)

Complete descriptor component construction over the selected compiler, canonical EvalWorld memory and existing Files/readiness/runtime policies. Host path/file operations, random short-I/O draws, source socket/event positional operations, host file locks, and full-sync remain explicit typed effects.

Equations

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

def Miri.Input.EvalUnixNativeFdConstruction.fromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C Payload ShimBody I Host ClockHost : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (compatibilityBudget typeBudget : Nat) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (openHost : OpenHostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D Error Meta Path Os) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Payload) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error Interpreter.EnvVars.Kind) (resources : EvalUnixIoConstruction.FileResourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta) (otherFiles : EvalUnixIoConstruction.OtherFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (positional : OtherPositionalEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (fileLocks : EvalUnixIoConstruction.FileLockEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) (controlEffects : EvalUnixIoConstruction.ControlSourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (signatures : Interpreter.ShimSignatures.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ShimBody I) (readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (watcherReferenceBudget fileReferenceBudget hostUsizeBits : Nat) (shortFdOperations : Bool) (hostIsizeBits : Nat) (randomShort : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Bool) (communicate : Bool) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (isolatedOp : EvalUnixConstruction.IsolatedOp) (pollAndUnblockZero : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Unit) (descriptor : Interpreter.SocketMachine.Descriptor (Other Raw Listener TcpStream Error)) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Host) (checkedSum : Bool) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) (compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) C) (projectionHooks : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (spans : Interpreter.AllocationDriver.SpanHooks) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) P) (deallocation : Interpreter.AllocationMachine.DeallocationHooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)) P) : Except Interpreter.StepError (Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I ShimBody)

Compatibility entry point for callers which already carry a full deallocation hook record. New source assembly should pass the genuine diagnostic/native-drop leaves to fromSourceWithLifecycle directly.

Equations

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