Generic operational safety and partial correctness

This file defines reusable infrastructure for relations that have not yet been given a concrete language semantics. It is not an interpreter or a model of Rust or MIR. A future semantics must supply its own states, transition relation, terminal outcomes, and proofs that its relation is complete.

Terminal outcomes distinguish successful returns from undefined behavior, blocked proof obligations, and unsupported cases. Safe rejects each of the three non-success outcomes and requires every finitely reachable state to have an explicit transition or terminal outcome. This lets infinite executions be safe without treating a missing transition or an unimplemented case as success.

inductive Miri.OperationalSafety.Outcome (Value : Type v) (UB : Type w) (Obligation : Type x) : Type (max v w x)

A terminal result of a semantics supplied by a client.

• returned {Value : Type v} {UB : Type w} {Obligation : Type x} : Value → Outcome Value UB Obligation

  A computation returned a value.

• undefinedBehavior {Value : Type v} {UB : Type w} {Obligation : Type x} : UB → Outcome Value UB Obligation

  The computation reached an undefined-behavior outcome.

• blocked {Value : Type v} {UB : Type w} {Obligation : Type x} : Obligation → Outcome Value UB Obligation

  A required semantic or verification obligation remains blocked.

• unsupported {Value : Type v} {UB : Type w} {Obligation : Type x} : Obligation → Outcome Value UB Obligation

  The computation reached a case not supported by the supplied semantics.

@[instance_reducible]

instance Miri.OperationalSafety.instInhabitedOutcome {a✝ : Type u_1} [Inhabited a✝] {a✝¹ : Type u_2} {a✝² : Type u_3} : Inhabited (Outcome a✝ a✝¹ a✝²)

Equations

• Miri.OperationalSafety.instInhabitedOutcome = { default := Miri.OperationalSafety.instInhabitedOutcome.default }

def Miri.OperationalSafety.Outcome.isReturn {Value : Type u_1} {UB : Type u_2} {Obligation : Type u_3} : Outcome Value UB Obligation → Prop

Whether a terminal result is a successful return.

Equations

• (Miri.OperationalSafety.Outcome.returned a).isReturn = True
• (Miri.OperationalSafety.Outcome.undefinedBehavior a).isReturn = False
• (Miri.OperationalSafety.Outcome.blocked a).isReturn = False
• (Miri.OperationalSafety.Outcome.unsupported a).isReturn = False

structure Miri.OperationalSafety.System (State : Type u) (Value : Type v) (UB : Type w) (Obligation : Type x) : Type (max (max (max u v) w) x)

A small-step transition system with explicit terminal outcomes.

• step : State → State → Prop

  One permitted finite transition. Multiple successors encode nondeterminism.

• terminal : State → Outcome Value UB Obligation → Prop

  A terminal outcome permitted at a state.

inductive Miri.OperationalSafety.System.Reaches {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) : State → State → Prop

Finite reachability, including the zero-step path.

• refl {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} {sys : System State Value UB Obligation} (state : State) : sys.Reaches state state
• step {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} {sys : System State Value UB Obligation} {start middle finish : State} : sys.Reaches start middle → sys.step middle finish → sys.Reaches start finish

def Miri.OperationalSafety.System.ReachesOutcome {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) (outcome : Outcome Value UB Obligation) : Prop

A terminal result reachable after finitely many transitions.

Equations

• sys.ReachesOutcome start outcome = ∃ (final : State), sys.Reaches start final ∧ sys.terminal final outcome

def Miri.OperationalSafety.System.CanProgress {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (state : State) : Prop

A state can make progress when it can step or has an explicit terminal result.

Equations

• sys.CanProgress state = ((∃ (next : State), sys.step state next) ∨ ∃ (outcome : Miri.OperationalSafety.Outcome Value UB Obligation), sys.terminal state outcome)

def Miri.OperationalSafety.System.CompleteFrom {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) : Prop

Progress holds at every state reachable by a finite path from start.

This premise rules out unclassified dead ends. Divergent states satisfy it by having at least one successor, even if no terminal result is ever produced.

Equations

• sys.CompleteFrom start = ∀ (state : State), sys.Reaches start state → sys.CanProgress state

def Miri.OperationalSafety.System.NoUndefinedBehavior {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) : Prop

UB freedom excludes UB outcomes after every permitted finite execution. This property alone does not certify semantic coverage or resolve unsupported cases.

Equations

• sys.NoUndefinedBehavior start = ∀ (reason : UB), ¬sys.ReachesOutcome start (Miri.OperationalSafety.Outcome.undefinedBehavior reason)

def Miri.OperationalSafety.System.Safe {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) : Prop

Safety over all finite paths and all terminal outcomes.

Safe requires explicit progress at every reachable state and permits only successful terminal returns. Because quantification is over every successor and every terminal outcome, this definition is demonic with respect to nondeterminism. It does not require termination.

Equations

• sys.Safe start = (sys.CompleteFrom start ∧ ∀ (outcome : Miri.OperationalSafety.Outcome Value UB Obligation), sys.ReachesOutcome start outcome → outcome.isReturn)

def Miri.OperationalSafety.System.PartialCorrect {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) (post : Value → Prop) : Prop

Partial correctness: every reachable successful return satisfies post.

This assertion is conditional on return; it does not claim that a return is reachable.

Equations

• sys.PartialCorrect start post = ∀ (value : Value), sys.ReachesOutcome start (Miri.OperationalSafety.Outcome.returned value) → post value

theorem Miri.OperationalSafety.System.invariant_of_step_preserved {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (invariant : State → Prop) (initial : invariant start) (preserved : ∀ {before after : State}, invariant before → sys.step before after → invariant after) {state : State} (reachable : sys.Reaches start state) : invariant state

Every finite reachable state satisfies an invariant preserved by each step.

theorem Miri.OperationalSafety.System.partialCorrect_of_terminal_spec {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (post : Value → Prop) (spec : ∀ {final : State} {value : Value}, sys.Reaches start final → sys.terminal final (Outcome.returned value) → post value) : sys.PartialCorrect start post

A local property of all reachable successful terminal states proves partial correctness.

theorem Miri.OperationalSafety.System.noUndefinedBehavior_of_safe {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (safe : sys.Safe start) : sys.NoUndefinedBehavior start

Certified safety implies UB freedom; its progress/coverage requirements are additional requirements for accepting a Safe result.

theorem Miri.OperationalSafety.System.no_reachable_ub {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (safe : sys.Safe start) (reason : UB) (reachable : sys.ReachesOutcome start (Outcome.undefinedBehavior reason)) : False

A safe system cannot reach an undefined-behavior outcome.

theorem Miri.OperationalSafety.System.no_reachable_blocked {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (safe : sys.Safe start) (goal : Obligation) (reachable : sys.ReachesOutcome start (Outcome.blocked goal)) : False

A safe system cannot reach a blocked obligation.

theorem Miri.OperationalSafety.System.no_reachable_unsupported {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (safe : sys.Safe start) (goal : Obligation) (reachable : sys.ReachesOutcome start (Outcome.unsupported goal)) : False

A safe system cannot reach an unsupported case.

def Miri.OperationalSafety.InfiniteRun {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) (start : State) : Prop

An infinite run, represented by a state at each natural-number time.

Equations

• Miri.OperationalSafety.InfiniteRun sys start = ∃ (run : Nat → State), run 0 = start ∧ ∀ (n : Nat), sys.step (run n) (run (n + 1))

theorem Miri.OperationalSafety.System.safe_of_invariant {State : Type u} {Value : Type v} {UB : Type w} {Obligation : Type x} (sys : System State Value UB Obligation) {start : State} (invariant : State → Prop) (initial : invariant start) (progress : ∀ {state : State}, sys.Reaches start state → sys.CanProgress state) (preserved : ∀ {before after : State}, invariant before → sys.step before after → invariant after) (terminalSuccess : ∀ {state : State} {outcome : Outcome Value UB Obligation}, invariant state → sys.terminal state outcome → outcome.isReturn) : sys.Safe start

Invariants are an optional proof method for operational safety. Each permitted transition must preserve the invariant; progress excludes unclassified dead ends and terminalSuccess excludes unresolved outcomes.