Physical vectored IO: real typed reads/projections, raw Stack allocation, in-bounds pointer offsets and provenance-preserving nonoverlapping copies. Only canonical compiler queries and the actual deallocation driver survive.

@[reducible, inline]

abbrev Miri.Interpreter.UnixVectoredMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.UnixVectoredMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.UnixVectoredMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.UnixVectoredMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

def Miri.Interpreter.UnixVectoredMachine.bind {K U C H D O E Meta : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (allocation : PlaceMachine.AllocationConfig K (ValidityMachine.UserState U)) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (place : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (choice : C) (unitLayout : M K U LocalLayout) (iovecArrayLayout : UInt64 → M K U LocalLayout) (fieldIndex : LocalLayout → String → M K U Nat) (deallocateStack : Memory.Pointer (Option Memory.Provenance) → M K U Unit) (base : UnixVectored.Hooks (State K U) H D O E Meta) : UnixVectored.Hooks (State K U) H D O E Meta

Equations

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