Typed owned IO callbacks on the actual final World. Counters/queues, pending captures, readiness watchers and callback tokens each have one authoritative source store. Compiler layouts/host effects reuse their existing dictionaries.

@[reducible, inline]

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

Equations

• Miri.Input.EvalOwnedIoMachine.World = Miri.Input.EvalTypedSyncMachine.World

@[reducible, inline]

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

Equations

• Miri.Input.EvalOwnedIoMachine.State = Miri.Input.EvalTypedSyncMachine.State

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def Miri.Input.EvalOwnedIoMachine.views {Os R P H D O Aff B Poll Instant System Native Profiler : Type} : Interpreter.OwnedIoMachine.Views (World Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)

Equations

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

def Miri.Input.EvalOwnedIoMachine.eventStore {O Os R P H D Aff B Poll Instant System Native Profiler : Type} (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) : Interpreter.EventFdMachine.Store (User Os R P H D O Aff B Poll Instant System Native Profiler) O

Equations

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

def Miri.Input.EvalOwnedIoMachine.physicalEvent {O Os R P H D Aff B Poll Instant System Native Profiler C : Type} (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (machine : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) H D O) (ready : Interpreter.Readiness.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)) (wakeBudget : Nat) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler)) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.MachineHooks.FrameExtra) (choice : C) (libcI32 : String → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Int32) (u64Layout : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Interpreter.LocalLayout) : Interpreter.EventFd.PhysicalHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)

Equations

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

def Miri.Input.EvalOwnedIoMachine.completion {S H D O E Meta : Type} (h : Interpreter.UnixVectored.Hooks S H D O E Meta) : Interpreter.IoCompletion.Hooks S E

Equations

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

structure Miri.Input.EvalOwnedIoMachine.Bindings (S F E Iter : Type) : Type

• effects : Interpreter.TypedSyncMachine.Effects S
• operations : Interpreter.OwnedIoMachine.Operations S F E
• event : Interpreter.EventFd.Hooks S F
• poll : Interpreter.PollShims.Hooks S F Iter
• epoll : Interpreter.EpollShims.Hooks S F Iter

def Miri.Input.EvalOwnedIoMachine.prepare {Os R P H D O Aff B Poll Instant System Native Profiler Iter E Meta : Type} (e : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (event : Interpreter.EventFd.PhysicalHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)) (poll : Interpreter.PollShims.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Iter) (epoll : Interpreter.EpollShims.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Iter) (vector : Interpreter.UnixVectored.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) H D O E Meta) (wakeBudget : Nat) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Bindings (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter)

Equations

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

def Miri.Input.EvalOwnedIoMachine.files {Os R P H D O Aff B Poll Instant System Native Profiler E Iter Meta : Type} (store : Interpreter.EventFdMachine.Store (User Os R P H D O Aff B Poll Instant System Native Profiler) O) (bound : Bindings (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter) (base : Interpreter.Files.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) H D O E Meta) : Interpreter.Files.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler)) H D O E Meta

Equations

• Miri.Input.EvalOwnedIoMachine.files store bound base = Miri.Interpreter.EventFdMachine.bindFiles store bound.event 0 bound.operations.errorFromKind base

def Miri.Input.EvalOwnedIoMachine.invoke {Os R P H D O Aff B Poll Instant System Native Profiler E Iter : Type} (bound : Bindings (State 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.

def Miri.Input.EvalOwnedIoMachine.socketViews {Os R P H D O Aff B Poll Instant System Native Profiler : Type} : Interpreter.OwnedSocketMachine.Views (World Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)

Socket callbacks share the exact arena and ThreadMachine token supply used by eventfd/poll/epoll and synchronization callbacks.

Equations

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

structure Miri.Input.EvalOwnedIoMachine.SocketBindings (S F E R L T P H I : Type) : Type

• virtual : Interpreter.OwnedVirtualSocket.Hooks S F E I
• tcp : Interpreter.OwnedTcpSocket.Hooks S F R L T E P H I
• socket : Interpreter.Socket.Hooks S F E I

def Miri.Input.EvalOwnedIoMachine.prepareSockets {Os R P H D O Aff B Poll Instant System Native Profiler Raw Listener TcpStream E Host I : Type} (effects : Interpreter.TypedSyncMachine.Effects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (machine : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) H D O) (descriptor : Interpreter.SocketMachine.Descriptor O) (store : Interpreter.SocketMachine.Store (User Os R P H D O Aff B Poll Instant System Native Profiler) Raw Listener TcpStream E) (blocking : Interpreter.ReadinessMachine.BlockingStore (User Os R P H D O Aff B Poll Instant System Native Profiler) Poll) (asUnix : FD H D O → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Raw Listener TcpStream E Poll Host) (options : Interpreter.SocketOptions.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E I) (socket : Interpreter.Socket.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E I) (finish : Interpreter.OwnedSocketCompletion.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) E I) (resource : Nat) : SocketBindings (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host I

Equations

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

def Miri.Input.EvalOwnedIoMachine.socketFiles {O Os R P H D Aff B Poll Instant System Native Profiler E Raw Listener TcpStream Host I Meta : Type} (descriptor : Interpreter.SocketMachine.Descriptor O) (bound : SocketBindings (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host I) (resource : Nat) (base : Interpreter.Files.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) H D O E Meta) : Interpreter.Files.Hooks (Interpreter.OwnedSocketOperations.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R P H D O Aff B Poll Instant System Native Profiler)) H D O E Meta

Equations

• Miri.Input.EvalOwnedIoMachine.socketFiles descriptor bound resource base = Miri.Interpreter.OwnedSocketOperations.files descriptor bound.virtual bound.tcp resource base

def Miri.Input.EvalOwnedIoMachine.invokeSocket {Os R P H D O Aff B Poll Instant System Native Profiler E Raw Listener TcpStream Host I : Type} (bound : SocketBindings (State Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host I) (resource token : Nat) (kind : Concurrency.UnblockKind) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Bool

Equations

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