Pinned machine.rs::before_terminator and thread.rs::maybe_preempt_active_thread. Progress-report formatting is omitted. Random Bernoulli draws use the exact rand 0.10.3 64-bit threshold support; choices below that threshold are impossible even when the probability is positive. Full UB freedom must quantify over every admitted choice, not just one executable invocation.

structure Miri.Interpreter.TerminatorMachine.Control (Host : Type) : Type

• basicBlockCount : UInt64
• sinceGc : UInt32
• gcInterval : UInt32
• monotonic : Clock.Monotonic Host
• preemptionRateBits : UInt64
• checkedArithmetic : Bool

structure Miri.Interpreter.TerminatorMachine.Hooks (K User Host : Type) : Type

• getControl : User → Control Host
• setControl : Control Host → User → User
• provenance : ProvenanceGC.Hooks K User
• blockingIoGc : MachineHooks.M K User Unit

  Actual blocking_io::run_gc (weak readiness/source-description cleanup). This required leaf must not be replaced with success if I/O is in use.

def Miri.Interpreter.TerminatorMachine.permitsPreemption (rate : UInt64) (choice : Bool) : Except StepError Bool

Decoded binary64 from source MiriConfig, retaining signed zero. rand 0.10.3 Bernoulli::new converts p to floor(p * 2^64), then samples a u64 v and returns v < threshold. Use its exact rational form so tiny probabilities retain the source's empty-success support. Invalid probabilities trigger the source random_bool invariant only if queried.

Equations

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

def Miri.Interpreter.TerminatorMachine.maybePreemptWithChoice {K User Host : Type} (h : Hooks K User Host) (draw : MachineHooks.M K User Bool) : MachineHooks.M K User Unit

A choice outside the configured support is unresolved input, never Rust UB or a successful skipped preemption. Fixed scheduling never queries it.

Equations

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

def Miri.Interpreter.TerminatorMachine.beforeTerminatorWithChoice {K User Host : Type} [DecidableEq K] (h : Hooks K User Host) (preempt : MachineHooks.M K User Bool) : MachineHooks.M K User Unit

Equations

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

def Miri.Interpreter.TerminatorMachine.maybePreempt {K User Host : Type} (h : Hooks K User Host) (choice : Bool) : MachineHooks.M K User Unit

Retain the explicit-value APIs as source-equivalent deterministic wrappers.

Equations

• Miri.Interpreter.TerminatorMachine.maybePreempt h choice = Miri.Interpreter.TerminatorMachine.maybePreemptWithChoice h (pure choice)

def Miri.Interpreter.TerminatorMachine.beforeTerminator {K User Host : Type} [DecidableEq K] (h : Hooks K User Host) (preempt : Bool) : MachineHooks.M K User Unit

Equations

• Miri.Interpreter.TerminatorMachine.beforeTerminator h preempt = Miri.Interpreter.TerminatorMachine.beforeTerminatorWithChoice h (pure preempt)

def Miri.Interpreter.TerminatorMachine.bindStep {K User C V Host : Type} [DecidableEq K] (base : StepHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C V) (h : Hooks K User Host) (preemptionChoice : C → Bool) : StepHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C V

Install this source implementation into the same small-step driver.

Equations

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

theorem Miri.Interpreter.TerminatorMachine.updateControl_eq {K User Host : Type} (h : Hooks K User Host) (f : Control Host → Control Host) (state : MachineHooks.State K User) : Miri.Interpreter.TerminatorMachine.updateControl✝ h f state = EStateM.Result.ok () { stack := state.stack, machine := have __src := state.machine; { memory := __src.memory, borrowTracker := __src.borrowTracker, dataRace := __src.dataRace, threads := __src.threads, raceAllocations := __src.raceAllocations, allocationSpans := __src.allocationSpans, user := h.setControl (f (h.getControl state.machine.user)) state.machine.user } }