Library-owned positive representation of source DynSym and dynamic FD objects. TCP protocol states and descriptor tags are distinct constructors. No Any payload, string-based descriptor downcast or client fallback is used.

inductive Miri.Interpreter.SourceOther.Value (Raw Listener Stream Error : Type) : Type

• dynamicSymbol {Raw Listener Stream Error : Type} (name : String) : Value Raw Listener Stream Error
• eventFd {Raw Listener Stream Error : Type} (id : Files.FdId) : Value Raw Listener Stream Error
• epoll {Raw Listener Stream Error : Type} (watcher : Nat) : Value Raw Listener Stream Error
• virtualSocket {Raw Listener Stream Error : Type} (id : Files.FdId) : Value Raw Listener Stream Error
• tcpSocket {Raw Listener Stream Error : Type} (id : Files.FdId) : Value Raw Listener Stream Error
• tcpState {Raw Listener Stream Error : Type} (value : TcpSocket.State Raw Listener Stream Error) : Value Raw Listener Stream Error

structure Miri.Interpreter.SourceOther.TcpStateEmbedding (Other Raw Listener Stream Error : Type) : Type

• inject : TcpSocket.State Raw Listener Stream Error → Other
• project : Other → Option (TcpSocket.State Raw Listener Stream Error)
• projectInject (value : TcpSocket.State Raw Listener Stream Error) : self.project (self.inject value) = some value

def Miri.Interpreter.SourceOther.tcpState {R L T E : Type} : TcpStateEmbedding (Value R L T E) R L T E

Equations

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

def Miri.Interpreter.SourceOther.sockets {R L T E : Type} : SocketMachine.Descriptor (Value R L T E)

Equations

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

def Miri.Interpreter.SourceOther.eventTag {R L T E : Type} (id : Files.FdId) : Value R L T E

Equations

• Miri.Interpreter.SourceOther.eventTag id = Miri.Interpreter.SourceOther.Value.eventFd id

def Miri.Interpreter.SourceOther.eventProject {R L T E : Type} : Value R L T E → Option Files.FdId

Equations

• Miri.Interpreter.SourceOther.eventProject (Miri.Interpreter.SourceOther.Value.eventFd id) = some id
• Miri.Interpreter.SourceOther.eventProject x✝ = none

@[simp]

theorem Miri.Interpreter.SourceOther.event_roundtrip {R L T E : Type} (id : Files.FdId) : eventProject (eventTag id) = some id

def Miri.Interpreter.SourceOther.epoll {R L T E : Type} : PollMachine.DescriptorHooks (Value R L T E)

Equations

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

def Miri.Interpreter.SourceOther.unixSymbol {R L T E : Type} (value : UnixDynamic.Symbol) : Value R L T E

Equations

• Miri.Interpreter.SourceOther.unixSymbol value = Miri.Interpreter.SourceOther.Value.dynamicSymbol value.name

def Miri.Interpreter.SourceOther.windowsSymbol {R L T E : Type} (value : WindowsPlatform.DynamicSymbol) : Value R L T E

Equations

• Miri.Interpreter.SourceOther.windowsSymbol value = Miri.Interpreter.SourceOther.Value.dynamicSymbol value.name

def Miri.Interpreter.SourceOther.dynamicSymbol {R L T E : Type} : Value R L T E → Except StepError UnixDynamic.Symbol

Equations

• Miri.Interpreter.SourceOther.dynamicSymbol (Miri.Interpreter.SourceOther.Value.dynamicSymbol name) = Except.ok { name := name }
• Miri.Interpreter.SourceOther.dynamicSymbol x✝ = Except.error (Miri.Interpreter.StepError.invalidProgram "non-DynSym object in source function allocation")

def Miri.Interpreter.SourceOther.windowsDynamicSymbol {R L T E : Type} : Value R L T E → Except StepError WindowsPlatform.DynamicSymbol

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.SourceOther.windowsDynamicSymbol x✝ = Except.error (Miri.Interpreter.StepError.invalidProgram "non-DynSym object in source function allocation")