Source-point choice dictionaries. Each callback consumes from the same persistent tape, not a context-wide value reused at every callback invocation. Compiler, physical memory, host operations retain their dictionaries.

def Miri.Interpreter.ExecutionChoiceBindings.nanChoice {S : Type} (access : ExecutionChoices.Access S) (candidates : List FloatBits) : RvalueM S Nat

Source IteratorRandom::choose then independent random sign flip. The existing NaN relation enumerates [candidate,-candidate] pairs in source order; these two events map to that relation without merging duplicate payloads.

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.floatHooks {S P C : Type} (access : ExecutionChoices.Access S) (base : FloatOpsHooks P S C) : FloatOpsHooks P S C

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.successRate (failure : UInt64) : Except StepError UInt64

Source success_rate = 1.0 - failure_rate is a rounded binary64 subtraction, not an exact rational complement. Preserve this distinction at endpoint rates.

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.atomicHooks {S P C V : Type} (access : ExecutionChoices.Access S) (failureRate : UInt64) (base : IntrinsicAtomicHooks P S C V) : IntrinsicAtomicHooks P S C V

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.simdHooks {S P C V : Type} (access : ExecutionChoices.Access S) (base : IntrinsicSimdHooks P S C V) : IntrinsicSimdHooks P S C V

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.intrinsicHooks {S P C V : Type} (access : ExecutionChoices.Access S) (failureRate : UInt64) (base : IntrinsicHooks P S C V) : IntrinsicHooks P S C V

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.vtableHooks {S P C F A : Type} (access : ExecutionChoices.Access S) (base : VTableHooks P S C F A) : VTableHooks P S C F A

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.mathHooks {S P C V : Type} (access : ExecutionChoices.Access S) (base : Math.Hooks P S C V) : Math.Hooks P S C V

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.x86Hooks {S P C V : Type} (access : ExecutionChoices.Access S) (base : IntrinsicX86.Hooks P S C V) : IntrinsicX86.Hooks P S C V

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.functionHooks {K U Other : Type} (access : ExecutionChoices.Access (MachineHooks.State K U)) (base : FunctionPointers.Hooks K U Other) : FunctionPointers.Hooks K U Other

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.schedulerChoice {S : Type} (access : ExecutionChoices.Access S) (candidates : List Concurrency.ThreadId) : RvalueM S (Option Concurrency.ThreadId)

Source scheduling never samples an empty iterator. Fixed scheduling skips this callback in ThreadStacks.scheduleLocal; every enabled candidate is admitted.

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.schedulerHooks {K U : Type} (access : ExecutionChoices.Access (ThreadStacks.State K U)) (base : ThreadStacks.LocalSchedulerHooks K U) : ThreadStacks.LocalSchedulerHooks K U

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.threadClockReuse {K U C O X F A Aff : Type} (access : ExecutionChoices.Access (ThreadMachine.State K U)) (base : ThreadMachine.Hooks K U C O X F A Aff) : ThreadMachine.Hooks K U C O X F A Aff

Source thread creation may reuse a vector clock only from the exact safe candidate set supplied by ThreadMachine. Consume one execution-tape index at that point; empty support is never sampled, and out-of-range tape inputs fail closed. The impossible post-index lookup remains a defensive invalid-program error. Explicit reuse overrides are handled by ThreadMachine before this hook is called.

Equations

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

def Miri.Interpreter.ExecutionChoiceBindings.beforeTerminator {K U Host : Type} [DecidableEq K] (access : ExecutionChoices.Access (MachineHooks.State K U)) (h : TerminatorMachine.Hooks K U Host) : MachineHooks.M K U Unit

The tape request runs at the source post-GC preemption point, and only outside fixed scheduling. Clock tick remains after the decision.

Equations

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