Source construction for the three Windows entropy entry points in pinned shims/windows/foreign_items.rs. Memory and isolated choices belong to the same Main state; host entropy is the only optional external operation.

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRandomConstruction.Payload (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsRandomConstruction.Payload Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalCoreMachine.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRandomConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsRandomConstruction.State Os R P H D O Aff B Host = Miri.Interpreter.MainMachine.State (Miri.Input.EvalWindowsRandomConstruction.Payload Os R P H D O Aff B Host)

def Miri.Input.EvalWindowsRandomConstruction.fromAccess [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host C Destination Body Instance : Type} (p : CompilerProviders.Prepared) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (Payload Os R P H D O Aff B Host))) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Body Instance) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (tape : Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)) (choice : C) (communicate : Bool) (hostUsizeBits : Nat) (hostFill : Option (Nat → EStateM Interpreter.StepError (State Os R P H D O Aff B Host) (Except String ByteArray))) : Except Interpreter.StepError (Interpreter.WindowsRandomDispatch.Hooks (State Os R P H D O Aff B Host) Destination Body Instance)

Equations

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

def Miri.Input.EvalWindowsRandomConstruction.fromSource [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host C Destination Body Instance : Type} (p : CompilerProviders.Prepared) (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Body Instance) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (tape : Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)) (choice : C) (communicate : Bool) (hostUsizeBits : Nat) (hostFill : Option (Nat → EStateM Interpreter.StepError (State Os R P H D O Aff B Host) (Except String ByteArray))) : Except Interpreter.StepError (Interpreter.WindowsRandomDispatch.Hooks (State Os R P H D O Aff B Host) Destination Body Instance)

Equations

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