Named constructors for source execution choice tapes.

The strict finite tape remains the default input mode. diagnosticTape is an explicit, bounded way to obtain one concrete, domain-valid diagnostic trace; it is not an exploration of all source outcomes and makes no safety or verification claim about other choices. Supplied inputs are always consumed and validated as supplied, without falling back to generated choices.

def Miri.Input.ExecutionChoicePolicy.strictTape (inputs : Array Interpreter.ExecutionChoices.Input := #[]) : Interpreter.ExecutionChoices.Tape

A strict finite tape. Exhaustion retains the source runner's existing unknown-choice behavior.

Equations

• Miri.Input.ExecutionChoicePolicy.strictTape inputs = { inputs := inputs }

def Miri.Input.ExecutionChoicePolicy.diagnosticTape (maxGeneratedChoices maxByteLength : Nat) (inputs : Array Interpreter.ExecutionChoices.Input := #[]) : Interpreter.ExecutionChoices.Tape

Explicit bounded diagnostic source choices. maxGeneratedChoices bounds the number of choices generated after the supplied prefix, and maxByteLength bounds each generated random-byte vector before allocation.

Equations

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

def Miri.Input.ExecutionChoicePolicy.seededDiagnosticTape (maxGeneratedChoices maxByteLength : Nat) (seed : UInt64) (inputs : Array Interpreter.ExecutionChoices.Input := #[]) : Interpreter.ExecutionChoices.Tape

Explicit bounded diagnostic source choices selected by a deterministic seeded stream. Generated values are appended to inputs, so the resulting consumed tape is replayable. The seed chooses one trace only and does not establish rand/Miri PRNG equivalence, uniformity, or safety for other traces.

Equations

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