Finite-prefix safety for the actual scheduler iteration. These definitions are conditional on the supplied machine operations and permitted choices; they do not assert that an arbitrary hook implementation covers pinned Miri. In particular, excluding UB alone does not discharge unsupported operations.

inductive Miri.Interpreter.RunLoop.Prefix {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) : S → List C → S → Prop

A finite execution prefix, retaining every choice as a witness. Only successful iterations continue; errors are observable outcomes, not steps.

• nil {S C Callback : Type} {hooks : RunLoopHooks S C Callback} {allowed : S → C → Prop} (state : S) : Prefix hooks allowed state [] state
• cons {S C Callback : Type} {hooks : RunLoopHooks S C Callback} {allowed : S → C → Prop} {start middle finish : S} {choice : C} {choices : List C} : allowed start choice → iteration hooks choice start = (middle, Except.ok ()) → Prefix hooks allowed middle choices finish → Prefix hooks allowed start (choice :: choices) finish

def Miri.Interpreter.RunLoop.Reachable {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) (state : S) : Prop

All states reached after a permitted finite prefix, including the initial state. No fuel or termination assumption restricts this relation.

Equations

• Miri.Interpreter.RunLoop.Reachable hooks allowed initial state = ∃ (start : S), ∃ (choices : List C), initial start ∧ Miri.Interpreter.RunLoop.Prefix hooks allowed start choices state

def Miri.Interpreter.RunLoop.ReachesError {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) (error : StepError) : Prop

An error outcome with a complete finite choice witness.

Equations

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

def Miri.Interpreter.RunLoop.UBFreedomFrom {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) : Prop

Exclude UB on every permitted finite prefix. This is a statement about the specified operations and choices, not a coverage certificate for Rust.

Equations

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

def Miri.Interpreter.RunLoop.UBReachable {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) : Prop

Witness of a UB outcome; unlike failed proof search, it establishes a permitted execution ending in UB.

Equations

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

theorem Miri.Interpreter.RunLoop.prefix_preserves {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (invariant : S → Prop) (preserved : ∀ (before after : S) (choice : C), invariant before → allowed before choice → iteration hooks choice before = (after, Except.ok ()) → invariant after) {start finish : S} {choices : List C} (execution : Prefix hooks allowed start choices finish) (atStart : invariant start) : invariant finish

theorem Miri.Interpreter.RunLoop.ubFreedomFrom_of_invariant {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial invariant : S → Prop) (initialized : ∀ (state : S), initial state → invariant state) (preserved : ∀ (before after : S) (choice : C), invariant before → allowed before choice → iteration hooks choice before = (after, Except.ok ()) → invariant after) (excludesUB : ∀ (before after : S) (choice : C) (error : StepError), invariant before → allowed before choice → iteration hooks choice before = (after, Except.error error) → reportsUB error = false) : UBFreedomFrom hooks allowed initial

Optional invariant proof rule. UB freedom itself is defined directly by outcomes above, without requiring an invariant or program termination.

theorem Miri.Interpreter.RunLoop.not_ubFreedomFrom_of_ubReachable {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) (witness : UBReachable hooks allowed initial) : ¬UBFreedomFrom hooks allowed initial

theorem Miri.Interpreter.RunLoop.ubFreedomFrom_iff_not_ubReachable {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (allowed : S → C → Prop) (initial : S → Prop) : UBFreedomFrom hooks allowed initial ↔ ¬UBReachable hooks allowed initial

Outcome exclusion and absence of a permitted UB witness are equivalent. Neither side asserts implementation completeness or resolves unknown errors.