Exact socket.rs finish environments and result-specific source bodies. File-description IO and socket send/recv use distinct source result encodings.

@[reducible, inline]

abbrev Miri.Interpreter.OwnedSocketCompletion.Dest : Type

Equations

• Miri.Interpreter.OwnedSocketCompletion.Dest = Miri.Interpreter.IoCompletionData.Dest

inductive Miri.Interpreter.OwnedSocketCompletion.Bytes : Type

• file (capture : IoCompletionData.Capture) : Bytes
• socket (dest : Dest) : Bytes

structure Miri.Interpreter.OwnedSocketCompletion.Accept : Type

• address : Memory.Pointer (Option Memory.Provenance)
• length : Memory.Pointer (Option Memory.Provenance)
• dest : Dest

structure Miri.Interpreter.OwnedSocketCompletion.Connect : Type

• dest : Dest

structure Miri.Interpreter.OwnedSocketCompletion.Peer : Type

• address : Memory.Pointer (Option Memory.Provenance)
• length : Memory.Pointer (Option Memory.Provenance)
• dest : Dest

inductive Miri.Interpreter.OwnedSocketCompletion.Data : Type → Type

• bytes (value : Bytes) : Data Nat
• accept (value : Accept) : Data (Int32 × SocketAddress.Address)
• connect (value : Connect) : Data Unit
• peer (value : Peer) : Data SocketAddress.Address

structure Miri.Interpreter.OwnedSocketCompletion.Finish (S E A : Type) : Type

• body : Files.Result E A → EStateM StepError S Unit
• capture : Option (Data A)

@[instance_reducible]

instance Miri.Interpreter.OwnedSocketCompletion.instCoeForallResultEStateMStepErrorUnitFinish {E A S : Type} : Coe (Files.Result E A → EStateM StepError S Unit) (Finish S E A)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.OwnedSocketCompletion.instCoeFunFinishForallResultEStateMStepErrorUnit {S E A : Type} : CoeFun (Finish S E A) fun (x : Finish S E A) => Files.Result E A → EStateM StepError S Unit

Equations

• Miri.Interpreter.OwnedSocketCompletion.instCoeFunFinishForallResultEStateMStepErrorUnit = { coe := Miri.Interpreter.OwnedSocketCompletion.Finish.body }

def Miri.Interpreter.OwnedSocketCompletion.Finish.source {A E S : Type} (capture : Data A) (body : Files.Result E A → EStateM StepError S Unit) : Finish S E A

Equations

• Miri.Interpreter.OwnedSocketCompletion.Finish.source capture body = { body := body, capture := some capture }

structure Miri.Interpreter.OwnedSocketCompletion.Hooks (S E Iter : Type) : Type

• file : IoCompletion.Hooks S E
• address : SocketAddress.Hooks S E Iter
• pointerSize : ABI.Size

def Miri.Interpreter.OwnedSocketCompletion.bytes {S E I : Type} (h : Hooks S E I) (capture : Bytes) (result : Files.Result E Nat) : EStateM StepError S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OwnedSocketCompletion.bytes h (Miri.Interpreter.OwnedSocketCompletion.Bytes.file capture_2) result = Miri.Interpreter.IoCompletion.invoke h.file capture_2 result

def Miri.Interpreter.OwnedSocketCompletion.accept {S E I : Type} (h : Hooks S E I) (capture : Accept) (result : Files.Result E (Int32 × SocketAddress.Address)) : EStateM StepError S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OwnedSocketCompletion.accept h capture (Except.error error) = Miri.Interpreter.IoError.setErrnoAndReturnNeg1 h.address.errors error capture.dest

def Miri.Interpreter.OwnedSocketCompletion.connect {S E I : Type} (h : Hooks S E I) (capture : Connect) (result : Files.Result E Unit) : EStateM StepError S Unit

Equations

• Miri.Interpreter.OwnedSocketCompletion.connect h capture (Except.ok PUnit.unit) = h.address.writeInt 0 capture.dest
• Miri.Interpreter.OwnedSocketCompletion.connect h capture (Except.error error) = Miri.Interpreter.IoError.setErrnoAndReturnNeg1 h.address.errors error capture.dest

def Miri.Interpreter.OwnedSocketCompletion.peer {S E I : Type} (h : Hooks S E I) (capture : Peer) (result : Files.Result E SocketAddress.Address) : EStateM StepError S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OwnedSocketCompletion.peer h capture (Except.error error) = Miri.Interpreter.IoError.setErrnoAndReturnNeg1 h.address.errors error capture.dest