Safety and liveness predicates over concurrent runs

This file packages the semantic notions of safety and liveness that sit on top of runs and fairness.

The goal is deliberately modest and foundational. Rather than introducing a full temporal-logic syntax, the file defines:

• run predicates and state predicates;
• the basic temporal lifts of a state predicate along a run;
• admissibility, safety, and initiality for ProcessOver.System; and
• what it means for a system to satisfy a run property under a chosen fairness assumption.

The closed-world Process API is recovered as a specialization of these generic definitions.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.Run.Pred {Γ : Spec.Node.Context} (process : ProcessOver Γ) : Type (max u_1 w)

Pred process is the type of semantic properties of whole runs of process.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.Run.StatePred {Γ : Spec.Node.Context} (process : ProcessOver Γ) : Type u_1

StatePred process is the type of predicates on residual process states.

def Interaction.Concurrent.ProcessOver.Run.AlwaysState {Γ : Spec.Node.Context} {process : ProcessOver Γ} (P : StatePred process) (run : process.Run) : Prop

AlwaysState P run means that the state predicate P holds at every state of the run run.

def Interaction.Concurrent.ProcessOver.Run.EventuallyState {Γ : Spec.Node.Context} {process : ProcessOver Γ} (P : StatePred process) (run : process.Run) : Prop

EventuallyState P run means that the run eventually reaches a state satisfying P.

def Interaction.Concurrent.ProcessOver.Run.InfinitelyOftenState {Γ : Spec.Node.Context} {process : ProcessOver Γ} (P : StatePred process) (run : process.Run) : Prop

InfinitelyOftenState P run means that P holds at arbitrarily late states of run.

theorem Interaction.Concurrent.ProcessOver.Run.alwaysState_mono {Γ : Spec.Node.Context} {process : ProcessOver Γ} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : AlwaysState P run → AlwaysState Q run

Monotonicity of AlwaysState.

theorem Interaction.Concurrent.ProcessOver.Run.eventuallyState_mono {Γ : Spec.Node.Context} {process : ProcessOver Γ} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : EventuallyState P run → EventuallyState Q run

Monotonicity of EventuallyState.

theorem Interaction.Concurrent.ProcessOver.Run.infinitelyOftenState_mono {Γ : Spec.Node.Context} {process : ProcessOver Γ} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : InfinitelyOftenState P run → InfinitelyOftenState Q run

Monotonicity of InfinitelyOftenState.

def Interaction.Concurrent.ProcessOver.System.Admissible {Γ : Spec.Node.Context} (system : System Γ) (run : system.Run) : Prop

A run of system is admissible when the ambient assumptions hold at every state along the run.

def Interaction.Concurrent.ProcessOver.System.Safe {Γ : Spec.Node.Context} (system : System Γ) (run : system.Run) : Prop

A run of system is safe when the safety predicate holds at every state along the run.

def Interaction.Concurrent.ProcessOver.System.Initial {Γ : Spec.Node.Context} (system : System Γ) (run : system.Run) : Prop

A run starts from an initial state when its first residual process state satisfies system.init.

def Interaction.Concurrent.ProcessOver.System.Satisfies {Γ : Spec.Node.Context} (system : System Γ) (fairness property : Run.Pred system.toProcess) : Prop

Satisfies system fairness property means: every initial admissible run of system that satisfies the fairness assumption fairness also satisfies the run property property.

theorem Interaction.Concurrent.ProcessOver.System.alwaysState_of_safe {Γ : Spec.Node.Context} (system : System Γ) {P : Run.StatePred system.toProcess} (himp : ∀ (p : system.Proc), system.safe p → P p) {run : system.Run} : system.Safe run → Run.AlwaysState P run

If a run is safe and every safe state satisfies P, then P holds at every state along the run.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.Pred {Party : Type u} (process : Process Party) : Type (max u_1 u_2)

The closed-world specialization of ProcessOver.Run.Pred.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.StatePred {Party : Type u} (process : Process Party) : Type u_1

The closed-world specialization of ProcessOver.Run.StatePred.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.AlwaysState {Party : Type u} {process : Process Party} (P : StatePred process) (run : process.Run) : Prop

AlwaysState for closed-world runs.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.EventuallyState {Party : Type u} {process : Process Party} (P : StatePred process) (run : process.Run) : Prop

EventuallyState for closed-world runs.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.InfinitelyOftenState {Party : Type u} {process : Process Party} (P : StatePred process) (run : process.Run) : Prop

InfinitelyOftenState for closed-world runs.

theorem Interaction.Concurrent.Process.Run.alwaysState_mono {Party : Type u} {process : Process Party} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : AlwaysState P run → AlwaysState Q run

theorem Interaction.Concurrent.Process.Run.eventuallyState_mono {Party : Type u} {process : Process Party} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : EventuallyState P run → EventuallyState Q run

theorem Interaction.Concurrent.Process.Run.infinitelyOftenState_mono {Party : Type u} {process : Process Party} {P Q : StatePred process} (himp : ∀ (p : process.Proc), P p → Q p) {run : process.Run} : InfinitelyOftenState P run → InfinitelyOftenState Q run

@[reducible, inline]

abbrev Interaction.Concurrent.Process.System.Admissible {Party : Type u} (system : System Party) (run : Run system.toProcess) : Prop

The closed-world specialization of run admissibility.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.System.Safe {Party : Type u} (system : System Party) (run : Run system.toProcess) : Prop

The closed-world specialization of run safety.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.System.Initial {Party : Type u} (system : System Party) (run : Run system.toProcess) : Prop

The closed-world specialization of initiality.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.System.Satisfies {Party : Type u} (system : System Party) (fairness property : Run.Pred system.toProcess) : Prop

The closed-world specialization of semantic satisfaction under fairness.

theorem Interaction.Concurrent.Process.System.alwaysState_of_safe {Party : Type u} (system : System Party) {P : Run.StatePred system.toProcess} (himp : ∀ (p : system.Proc), system.safe p → P p) {run : Run system.toProcess} : system.Safe run → Run.AlwaysState P run