Complete pinned linux_like/epoll.rs syscall policy. Epoll descriptor creation and downcast are required actual FileDescription operations, not integer aliases.

@[reducible, inline]

abbrev Miri.Interpreter.EpollShims.M (σ α : Type) : Type

Equations

• Miri.Interpreter.EpollShims.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.EpollShims.DeferredBackend (S F : Type) : Type

• legacy {S F : Type} : DeferredBackend S F
• typed {S F : Type} (block : F → MPlaceTy Memory.Provenance → MPlaceTy Memory.Provenance → Option Concurrency.ThreadDeadline → M S Unit) : DeferredBackend S F

structure Miri.Interpreter.EpollShims.Hooks (S F Iter : Type) : Type

• deferred : DeferredBackend S F
• poll : PollShims.Hooks S F Iter
• libcI32 : String → M S Int32
• libcU32 : String → M S UInt32
• readImmediate : OpTy Memory.Provenance → M S (OpTy Memory.Provenance)
• derefEvent : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• indexedField : MPlaceTy Memory.Provenance → Nat → M S (MPlaceTy Memory.Provenance)
• readU32 : MPlaceTy Memory.Provenance → M S UInt32
• readU64 : MPlaceTy Memory.Provenance → M S UInt64
• arrayLength : MPlaceTy Memory.Provenance → M S Nat
• writeEvent : MPlaceTy Memory.Provenance → UInt32 → UInt64 → M S Unit

  Actual write_int_fields_named, preserving field projection/write order.

• writeI32 : Int32 → MPlaceTy Memory.Provenance → M S Unit
• setErrno : String → M S Unit
• insertEpoll : Nat → M S Int32

  Creates an Epoll description owning this watcher, inserts it in actual FD table. Source metadata is Unix S_IFREG; default unsupported operations remain unsupported.

• asEpoll : F → M S (Option Nat)

def Miri.Interpreter.EpollShims.create {S F I : Type} (h : Hooks S F I) (flags : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.EpollShims.fromFlags {S F I : Type} (h : Hooks S F I) (flags : UInt32) : M S Files.Readiness

Equations

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

def Miri.Interpreter.EpollShims.toFlags {S F I : Type} (h : Hooks S F I) (ready : Files.Readiness) : M S UInt32

Equations

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

def Miri.Interpreter.EpollShims.control {S F I : Type} (budget : Nat) (h : Hooks S F I) (epfd op fd event : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.EpollShims.returnReady {S F I : Type} (budget : Nat) (h : Hooks S F I) (watcher : Nat) (dest events : MPlaceTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.EpollShims.wait {S F I : Type} (budget : Nat) (h : Hooks S F I) (epfd events maxevents timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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