Data environments of source IO finish callbacks. A Finish value is a transient call parameter; only its data capture may enter HostRuntime storage. Function coercions retain fixture compatibility without decoding functions.

@[reducible, inline]

abbrev Miri.Interpreter.IoCompletionData.Dest : Type

Equations

• Miri.Interpreter.IoCompletionData.Dest = Miri.Interpreter.MPlaceTy Miri.Memory.Provenance

@[reducible, inline]

abbrev Miri.Interpreter.IoCompletionData.Buffer : Type

Equations

• Miri.Interpreter.IoCompletionData.Buffer = (Miri.Memory.Pointer (Option Miri.Memory.Provenance) × UInt64)

inductive Miri.Interpreter.IoCompletionData.Capture : Type

• unixScalar (count : Nat) (dest : Dest) : Capture
• unixVectored (write : Bool) (temporary : Memory.Pointer (Option Memory.Provenance)) (buffers : Array Buffer) (dest : Dest) : Capture
• windowsNt (count : UInt32) (status information dest : Dest) : Capture

structure Miri.Interpreter.IoCompletionData.Finish (S Error : Type) : Type

• body : Except Error Nat → EStateM StepError S Unit
• capture : Option Capture

@[instance_reducible]

instance Miri.Interpreter.IoCompletionData.instCoeForallExceptNatEStateMStepErrorUnitFinish {Error S : Type} : Coe (Except Error Nat → EStateM StepError S Unit) (Finish S Error)

Equations

• Miri.Interpreter.IoCompletionData.instCoeForallExceptNatEStateMStepErrorUnitFinish = { coe := fun (body : Except Error Nat → EStateM Miri.Interpreter.StepError S Unit) => { body := body } }

@[instance_reducible]

instance Miri.Interpreter.IoCompletionData.instCoeFunFinishForallExceptNatEStateMStepErrorUnit {S Error : Type} : CoeFun (Finish S Error) fun (x : Finish S Error) => Except Error Nat → EStateM StepError S Unit

Equations

• Miri.Interpreter.IoCompletionData.instCoeFunFinishForallExceptNatEStateMStepErrorUnit = { coe := Miri.Interpreter.IoCompletionData.Finish.body }

def Miri.Interpreter.IoCompletionData.Finish.source {Error S : Type} (capture : Capture) (body : Except Error Nat → EStateM StepError S Unit) : Finish S Error

Equations

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