Compiler- and execution-state construction for the Unix descriptor/poll family. Descriptor and readiness registries are projections of the actual EvalWorld; target policy and the poll ABI come from rustc metadata. Only the last-drop resource actions and the already-source-built physical epoll/poll operations remain inputs.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

structure Miri.Input.EvalUnixFdConstruction.SourceFacts : Type

• target : CompilerExternStatic.TargetFacts
• pollAbi : Except String (ABI.FnAbi MIR.TyId)

  Demand-time query results: missing libc names or named ABI rows leave only poll unsupported while ordinary FD and filesystem shims remain usable.

def Miri.Input.EvalUnixFdConstruction.sourceFacts (p : CompilerProviders.Prepared) : Except Interpreter.StepError SourceFacts

Equations

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

def Miri.Input.EvalUnixFdConstruction.files {H D Raw Listener TcpStream Error Os R P Aff B Poll Instant System Native Profiler : Type} (hostUsizeBits referenceBudget : Nat) (onLastDrop : Interpreter.Files.Description H D (Other Raw Listener TcpStream Error) → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) : 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 canonical descriptor table and Rc registry already contain the three source stdio descriptors from InitialMachine/HostRuntime construction. This builder only supplies their state projections and destructor effects; it never reinitializes or duplicates the table.

Equations

• Miri.Input.EvalUnixFdConstruction.files hostUsizeBits referenceBudget onLastDrop = Miri.Input.EvalSocketStorage.files hostUsizeBits referenceBudget onLastDrop

def Miri.Input.EvalUnixFdConstruction.readiness {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (fileHooks : 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)) (watcherReferenceBudget : Nat) (onLastDrop : FD H D (Other Raw Listener TcpStream Error) → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) : Interpreter.ReadinessMachine.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)

Readiness shares the same descriptor ownership registry. Its last-drop callback performs watched-metadata cleanup and then the true resource drop.

Equations

• Miri.Input.EvalUnixFdConstruction.readiness fileHooks watcherReferenceBudget onLastDrop = Miri.Input.EvalSocketStorage.readiness fileHooks watcherReferenceBudget onLastDrop

def Miri.Input.EvalUnixFdConstruction.bindReadiness {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (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)) (physical : Interpreter.Readiness.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))) : Interpreter.Readiness.Hooks (Interpreter.MachineHooks.State Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (Interpreter.Files.Ref (Interpreter.Files.Description H D (Other Raw Listener TcpStream Error)))

Install the real registry/weak-liveness semantics underneath a physical readiness dictionary. The physical access and wake operations remain the existing canonical source leaves.

Equations

• Miri.Input.EvalUnixFdConstruction.bindReadiness registry physical = Miri.Interpreter.ReadinessMachine.bind registry physical

def Miri.Input.EvalUnixFdConstruction.bindUnixFd {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta : Type} (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)) (physicalReadiness : Interpreter.Readiness.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))) (base : 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 Meta) : Interpreter.UnixFd.Hooks (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) Error Meta

Bind FD operations to the actual descriptor and ownership arena, including the source ReadinessWatched creation/drop hooks. The supplied UnixFd methods are the physical/source operation leaves; their table and Rc behavior cannot be substituted by caller-owned state.

Equations

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

def Miri.Input.EvalUnixFdConstruction.bindPoll {C Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Iter : Type} (p : CompilerProviders.Prepared) (compatibilityBudget : Nat) (choice : C) (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)) (place : Interpreter.PlaceHooks Memory.Provenance (EvalCoreMachine.State 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 Interpreter.MachineHooks.FrameExtra) (base : Interpreter.PollDispatch.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)) Iter) : Except Interpreter.StepError (Interpreter.PollDispatch.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)) Iter)

Construct the real poll foreign-item hooks around the existing source poll/epoll implementation. Compiler ABI, C ABI compatibility, symbol-clash checks, and operand transmutation are rebound here; a missing exact poll query remains an Unsupported result at the source poll call.

Equations

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

structure Miri.Input.EvalUnixFdConstruction.ArrayCursor : Type

• iterator : Interpreter.ArrayProjection.Iterator
• next : Nat

structure Miri.Input.EvalUnixFdConstruction.ReadinessRoute (S : Type) : Type

The only readiness leaves that need to cross the startup constructor boundary: typed callback/runtime routing and the source wake operation. Descriptor policy and current readiness are taken from Files descriptions.

• runtime : Concurrency.SyncRuntime.Hooks S Nat Int32 (Interpreter.MPlaceTy Memory.Provenance)
• debugAssertions : Bool
• unblock : Concurrency.ThreadId → Concurrency.BlockReason → EStateM Interpreter.StepError S Unit

def Miri.Input.EvalUnixFdConstruction.readinessFromFiles {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error HostError Metadata : Type} (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)) (fileSemantics : 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) HostError Metadata) (route : ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) : Interpreter.Readiness.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))

Construct the physical readiness view from the actual source File hooks. The registry binder below replaces every ownership/state operation; this view provides only source description classification, callback routing and wakeup.

Equations

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

def Miri.Input.EvalUnixFdConstruction.pollWithDeadlineMillis {C Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler HostError Metadata : Type} (p : CompilerProviders.Prepared) (choice : C) (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))) (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) (unitLayout : Interpreter.LocalLayout) (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)) (fileSemantics : 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) HostError Metadata) (readinessRoute : ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (deadlineMillis : UInt32 → Interpreter.PollShims.M (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Concurrency.ThreadDeadline) (iterationBudget : Nat) : Except Interpreter.StepError (Interpreter.PollShims.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)) ArrayCursor)

Build all PollShims operations from exact libc/compiler queries and canonical physical place/memory operations. physicalReadiness supplies only thread/callback waking; the readiness registry, descriptor lookups, watcher creation, layout projections, memory reads/writes, and compiler constants are installed here. The deferred hook is only a construction intermediate: EvalOwnedIoMachine.prepare replaces it with its typed completion route.

Equations

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

def Miri.Input.EvalUnixFdConstruction.poll {C Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler HostError Metadata : Type} (p : CompilerProviders.Prepared) (choice : C) (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))) (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) (unitLayout : Interpreter.LocalLayout) (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)) (fileSemantics : 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) HostError Metadata) (readinessRoute : ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Instant System) (iterationBudget : Nat) : Except Interpreter.StepError (Interpreter.PollShims.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)) ArrayCursor)

Compatibility wrapper retaining the full deadline interface for existing source constructors. Poll itself only needs monotonic deadline creation, so new call sites can use pollWithDeadlineMillis with the actual narrow action and avoid constructing scheduler callback capabilities prematurely.

Equations

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

def Miri.Input.EvalUnixFdConstruction.epoll {C Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler HostError : Type} (p : CompilerProviders.Prepared) (choice : C) (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))) (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) (pollHooks : Interpreter.PollShims.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)) ArrayCursor) (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)) (descriptor : Interpreter.PollMachine.DescriptorHooks (Other Raw Listener TcpStream Error)) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) HostError) : Interpreter.EpollShims.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)) ArrayCursor

Build the Linux/Android epoll hook set from the canonical poll hooks, compiler event layout/constants, actual guest memory, and the same descriptor registry. EvalOwnedIoMachine.prepare replaces the legacy construction marker with its source typed deferred completion.

Equations

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

def Miri.Input.EvalUnixFdConstruction.dispatch {C Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler HostEffect : Type} (p : CompilerProviders.Prepared) (compatibilityBudget : Nat) (choice : C) (place : Interpreter.PlaceHooks Memory.Provenance (EvalCoreMachine.State 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 Interpreter.MachineHooks.FrameExtra) (epollHooks : Interpreter.EpollShims.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)) ArrayCursor) (communicate : Bool) (entryPollBudget : Nat) (io : Interpreter.BlockingIo.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)) Poll HostEffect) : Except Interpreter.StepError (Interpreter.PollDispatch.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)) ArrayCursor)

Assemble the final Unix poll/epoll foreign dispatcher rather than asking an outer constructor to hand in a completed PollDispatch dictionary. The sole physical scheduling leaf is the real zero-timeout mio poll operation.

Equations

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

def Miri.Input.EvalUnixFdConstruction.pollDispatch {C Os R P H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler HostError Metadata HostEffect : Type} (p : CompilerProviders.Prepared) (compatibilityBudget : Nat) (choice : C) (place : Interpreter.PlaceHooks Memory.Provenance (EvalCoreMachine.State 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 Interpreter.MachineHooks.FrameExtra) (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) (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))) (unitLayout : Interpreter.LocalLayout) (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)) (fileSemantics : 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) HostError Metadata) (readinessRoute : ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Instant System) (descriptor : Interpreter.PollMachine.DescriptorHooks (Other Raw Listener TcpStream Error)) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) HostError) (communicate : Bool) (entryPollBudget iterationBudget : Nat) (io : Interpreter.BlockingIo.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)) Poll HostEffect) : Except Interpreter.StepError (Interpreter.PollDispatch.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)) ArrayCursor)

Complete source constructor for Unix poll and Linux/Android epoll. It connects compiler queries, guest memory, descriptor/watcher ownership, callback routing, deadlines and the real blocking scheduler into one PollDispatch value, with no caller-selected poll/epoll implementation.

Equations

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