Canonical Unix descriptor/file operation construction. Host file handles and true host IO stay typed effects; descriptor identity, ownership, guest buffer reads/writes, and scalar accesses are bound to the current EvalWorld.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixIoConstruction.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.EvalUnixIoConstruction.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.EvalUnixIoConstruction.FD (H D O : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixIoConstruction.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.EvalUnixIoConstruction.HostFileEffects (S H D O E Meta : Type) : Type

Genuine host resource operations only. Guest byte access, descriptor ownership, and FileDescription policy are supplied by the source constructor. The other* callbacks are the already source-built event/socket operation family and remain separate from the host file boundary.

• hostRead : Interpreter.Files.Description H D O → ByteArray → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) (Nat × ByteArray))
• hostWrite : Interpreter.Files.Description H D O → ByteArray → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Nat)
• flushStdout : EStateM Interpreter.StepError S Unit
• hostSeek : H → Interpreter.Files.SeekFrom → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) UInt64)
• hostMetadata : Interpreter.Files.Description H D O → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Meta)
• hostIsTerminal : Interpreter.Files.Description H D O → EStateM Interpreter.StepError S Bool
• permissionDenied : EStateM Interpreter.StepError S (Interpreter.IoError.HostError E)

structure Miri.Input.EvalUnixIoConstruction.OtherFileEffects (S H D O E : Type) : Type

• read : FD H D O → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S E → EStateM Interpreter.StepError S Unit
• write : FD H D O → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S E → EStateM Interpreter.StepError S Unit
• shortOperations : O → Bool
• readiness : O → EStateM Interpreter.StepError S (Option Interpreter.Files.Readiness)
• hasReadinessWatched : O → Bool
• isTerminal : O → Bool → EStateM Interpreter.StepError S Bool

structure Miri.Input.EvalUnixIoConstruction.FileLockEffects (S H E : Type) : Type

• tryLock : H → Bool → EStateM Interpreter.StepError S (Except (Interpreter.UnixFileOperations.TryLockError E) Unit)
• unlock : H → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Unit)

structure Miri.Input.EvalUnixIoConstruction.FileResourceEffects (S H D O : Type) : Type

Resource finalization at the FileMachine last-owner boundary. Host file and directory handles have separate cleanup effects; source-owned descriptors retain their own typed cleanup route. The four standard descriptors need no external resource release.

• dropFile : H → EStateM Interpreter.StepError S Unit
• dropDirectory : D → EStateM Interpreter.StepError S Unit
• dropOther : O → EStateM Interpreter.StepError S Unit

def Miri.Input.EvalUnixIoConstruction.filesFromSourceFor {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler Metadata : Type} (family : Interpreter.ForeignItems.Family) (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored 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)))) (host : 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 Metadata) (other : 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) : Except Interpreter.StepError (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 Metadata)

Construct FileDescription behavior from the selected compiler target and canonical physical guest memory. other is an operation bundle from the source-owned EventFd/Socket adapters, not a replaceable Files hook record.

Equations

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

def Miri.Input.EvalUnixIoConstruction.filesFromSource {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler Metadata : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored 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)))) (host : 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 Metadata) (other : 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) : Except Interpreter.StepError (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 Metadata)

Preserve the historical Unix-only constructor and target validation.

Equations

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

def Miri.Input.EvalUnixIoConstruction.fileRegistry {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (hostUsizeBits referenceBudget : Nat) (effects : FileResourceEffects (Interpreter.MachineHooks.State 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)) : Interpreter.FileMachine.Hooks Memory.MiriMemoryKind (EvalSocketStorage.User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (EvalSocketStorage.Other Raw Listener TcpStream Error)

The descriptor registry is the one in EvalWorld runtime state. This helper keeps table, Rc ownership, and destructor callbacks on the FileMachine path.

Equations

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

def Miri.Input.EvalUnixIoConstruction.fileOperationsFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (p : CompilerProviders.Prepared) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (effects : FileLockEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) : Except Interpreter.StepError (Interpreter.UnixFileOperations.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error)

Equations

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

def Miri.Input.EvalUnixIoConstruction.unixFdFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Metadata C : Type} (p : CompilerProviders.Prepared) (communicate shortFdOperations : Bool) (hostIsizeBits : Nat) (registry : 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)) (readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (fileHooks : 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 Metadata) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (randomShort : EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) 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) (otherPositionalRead otherPositionalWrite : FD H D (Other Raw Listener TcpStream Error) → UInt64 → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) : Except Interpreter.StepError (Interpreter.UnixFd.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 Metadata)

Bind exact guest access and compiler target limits to source UnixFd policy. Random short-read selection remains a source RNG effect, and non-Unix positional descriptions remain explicit unsupported operations.

Equations

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

structure Miri.Input.EvalUnixIoConstruction.ControlSourceEffects (S : Type) : Type

• fullSync : Int32 → EStateM Interpreter.StepError S (Memory.Scalar Memory.Provenance)

def Miri.Input.EvalUnixIoConstruction.controlFromSource {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C Metadata ShimBody I Host : Type} (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (isolatedOp : EvalUnixConstruction.IsolatedOp) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (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) (fd : Interpreter.UnixFd.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 Metadata) (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) (typeBudget : Nat) (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) (fileEffects : FileLockEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) (effects : ControlSourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) : Except Interpreter.StepError (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 Metadata MIR.Place ShimBody I)

Assemble fcntl/ioctl dispatch from exact compiler ABI/constants and canonical access. Only the shared general shim-signature provider and genuine source policy/resource effects remain inputs.

Equations

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

def Miri.Input.EvalUnixIoConstruction.vectoredFromFieldsWithLifecycle {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C Metadata : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (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) (projection : 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) (choice : C) (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored 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)))) (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)) (fd : Interpreter.UnixFd.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 Metadata) (hostUsizeBits : Nat) (checkedSum : Bool) : Interpreter.UnixVectored.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 Metadata

Full source vectored field construction. The temporary iovec buffer uses the compiler's exact element layout, EvalWorld allocation lifecycle, actual pointer arithmetic, and provenance-preserving copy. checkedSum and host usize width are native build properties, supplied as explicit host facts.

Equations

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

def Miri.Input.EvalUnixIoConstruction.vectoredFromFields {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C Metadata : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (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) (projection : 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) (choice : C) (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored 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)))) (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) (fd : Interpreter.UnixFd.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 Metadata) (hostUsizeBits : Nat) (checkedSum : Bool) : Interpreter.UnixVectored.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 Metadata

Compatibility wrapper for callers which still package the genuine diagnostic and native-drop leaves in an AllocationMachine record. The source lifecycle itself remains constructed at the actual operation point.

Equations

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

def Miri.Input.EvalUnixIoConstruction.vectoredFromSource {Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C ClockHost Metadata : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored 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))) (config : ExecConfig Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C ClockHost) (choice : C) (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored 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)))) (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) (fd : Interpreter.UnixFd.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 Metadata) (hostUsizeBits : Nat) (checkedSum : Bool) : Interpreter.UnixVectored.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 Metadata

Compatibility wrapper for callers that already own a complete execution configuration. The production source constructor uses vectoredFromFields so Core can build the foreign component without a configuration cycle.

Equations

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