The actual Unix foreign chain selects typed owned eventfd/poll/epoll IO. Existing FD/socket families keep their source dispatch, while these supported families use the one HostRuntime arena and canonical physical operations.

@[reducible, inline]

abbrev Miri.Input.EvalForeignIoMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalForeignIoMachine.State = Miri.Input.EvalForeignSyncMachine.State

@[reducible, inline]

abbrev Miri.Input.EvalForeignIoMachine.Inner (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalForeignIoMachine.Inner = Miri.Input.EvalOwnedIoMachine.State

@[reducible, inline]

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

Equations

• Miri.Input.EvalForeignIoMachine.FD = Miri.Input.EvalOwnedIoMachine.FD

def Miri.Input.EvalForeignIoMachine.bind {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Place HM Time Kind ReadDir DirEntry Duration AddrIter TZ Timestamp Block Instance : Type} (bound : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (h : Interpreter.UnixForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place H D O Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration Iter AddrIter Instant System TZ Timestamp Block Instance) : Interpreter.UnixForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place H D O Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration Iter AddrIter Instant System TZ Timestamp Block Instance

Equations

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

def Miri.Input.EvalForeignIoMachine.unix {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Place HM Time Kind ReadDir DirEntry Duration AddrIter TZ Timestamp Block Instance : Type} (sync : Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (bound : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (h : Interpreter.UnixForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place H D O Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration Iter AddrIter Instant System TZ Timestamp Block Instance) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place Concurrency.TypedSyncRuntime.Dest (Memory.Pointer (Option Memory.Provenance)) Block Instance) : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Block Instance

Actual terminal Unix foreign dictionary: typed synchronization and owned IO are installed before the source dispatch captures its hooks.

Equations

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

def Miri.Input.EvalForeignIoMachine.invoke {Os R P H D O Aff B Poll Instant System Native Profiler E Iter : Type} (bound : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (other : Nat → Concurrency.UnblockKind → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (token : Nat) (kind : Concurrency.UnblockKind) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Equations

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