Pinned helpers.rs::gen_random. Source host getrandom failure is unsupported; isolated random bytes are nondeterministic semantic inputs, never a fixed seed.

@[reducible, inline]

abbrev Miri.Interpreter.RandomMemory.M (σ α : Type) : Type

Equations

• Miri.Interpreter.RandomMemory.M = EStateM Miri.Interpreter.StepError

structure Miri.Interpreter.RandomMemory.Hooks (S : Type) : Type

• communicate : Bool
• hostUsizeBits : Nat
• hostFill : Nat → M S (Except String ByteArray)

  Host getrandom::fill result; retains its actual state/error effects.

• isolatedFill : Nat → M S ByteArray
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit

def Miri.Interpreter.RandomMemory.generate {S : Type} (h : Hooks S) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M S Unit

Equations

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

def Miri.Interpreter.RandomMemory.bind {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K U) (tape : ExecutionChoices.Access (MachineHooks.State K U)) (base : Hooks (MachineHooks.State K U)) : Hooks (MachineHooks.State K U)

Equations

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

def Miri.Interpreter.RandomMemory.machine {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K U) (tape : ExecutionChoices.Access (MachineHooks.State K U)) (communicate : Bool) (hostUsizeBits : Nat) (hostFill : Nat → M (MachineHooks.State K U) (Except String ByteArray)) : Hooks (MachineHooks.State K U)

Construct helpers.rs::gen_random directly from genuine host effects and the current machine's source-choice tape and physical byte writer. This form does not require placeholder random or memory callbacks in a baseline record.

Equations

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