Concrete scalar, pointer and destination effects shared by source entropy wrappers. Both families draw through the one actual machine choice tape.
def
Miri.Interpreter.RandomDispatchMachine.unix
{K U C D B I : Type}
[DecidableEq K]
(access : PlaceMachine.AccessConfig K U)
(tape : ExecutionChoices.Access (MachineHooks.State K U))
(place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra)
(choice : C)
(base : UnixRandomDispatch.Hooks (MachineHooks.State K U) D B I)
:
UnixRandomDispatch.Hooks (MachineHooks.State K U) D B I
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.RandomDispatchMachine.windows
{K U C D B I : Type}
[DecidableEq K]
(access : PlaceMachine.AccessConfig K U)
(tape : ExecutionChoices.Access (MachineHooks.State K U))
(place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra)
(choice : C)
(base : WindowsRandomDispatch.Hooks (MachineHooks.State K U) D B I)
:
WindowsRandomDispatch.Hooks (MachineHooks.State K U) D B I
Equations
- One or more equations did not get rendered due to their size.