Event objects share the actual FD ownership/readiness registry. Tags carry only canonical FD identity; counter/clock/queues have one authoritative store.

@[reducible, inline]

abbrev Miri.Interpreter.EventFdMachine.Ref (H D O : Type) : Type

Equations

• Miri.Interpreter.EventFdMachine.Ref H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

structure Miri.Interpreter.EventFdMachine.Store (U O : Type) : Type

• get : U → Array (Files.FdId × EventFd.Event)
• put : Array (Files.FdId × EventFd.Event) → U → U
• tag : Files.FdId → O
• untag : O → Option Files.FdId

def Miri.Interpreter.EventFdMachine.withDestructor {U O K H D : Type} (store : Store U O) (machine : ReadinessMachine.Hooks K U H D O) (ready : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) : ReadinessMachine.Hooks K U H D O

Install this last-drop action in the shared readiness machine; a plain FileMachine.dropReference would skip source watched-field destruction.

Equations

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

def Miri.Interpreter.EventFdMachine.physical {K U O H D C : Type} [DecidableEq K] (store : Store U O) (machine : ReadinessMachine.Hooks K U H D O) (ready : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) (wakeBudget : Nat) (access : PlaceMachine.AccessConfig K U) (place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (choice : C) (libcI32 : String → MachineHooks.M K U Int32) (u64Layout : MachineHooks.M K U LocalLayout) : EventFd.PhysicalHooks (MachineHooks.State K U) (Ref H D O)

Equations

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

def Miri.Interpreter.EventFdMachine.bind {K U O H D C : Type} [DecidableEq K] (store : Store U O) (machine : ReadinessMachine.Hooks K U H D O) (ready : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) (wakeBudget : Nat) (access : PlaceMachine.AccessConfig K U) (place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (choice : C) (base : EventFd.Hooks (MachineHooks.State K U) (Ref H D O)) : EventFd.Hooks (MachineHooks.State K U) (Ref H D O)

Equations

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

def Miri.Interpreter.EventFdMachine.bindFiles {U O K H D Host Meta : Type} (store : Store U O) (event : EventFd.Hooks (MachineHooks.State K U) (Ref H D O)) (retryBudget : Nat) (errorFromKind : IoError.ErrorKind → MachineHooks.M K U (IoError.Error Host)) (base : Files.Hooks (MachineHooks.State K U) H D O Host Meta) : Files.Hooks (MachineHooks.State K U) H D O Host Meta

Route dynamic FileDescription IO to the source eventfd implementation. ErrorKind conversion is the actual io::Error::from(kind) host constructor.

Equations

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

def Miri.Interpreter.EventFdMachine.bindReadiness {U O K H D : Type} (store : Store U O) (base : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)

Shared readiness callbacks query the same authoritative event counter.

Equations

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

def Miri.Interpreter.EventFdMachine.metadataKind {U O : Type} (store : Store U O) (payload : O) : Option String

The actual source metadata result is synthetic S_IFREG, not host metadata.

Equations

• Miri.Interpreter.EventFdMachine.metadataKind store payload = if (store.untag payload).isSome = true then some "S_IFREG" else none