# Formal Proof of a Machine Closed Theorem in Coq

Authors: Hai Wan; Anping He; Zhiyang You; Xibin Zhao
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

The paper presents a formal proof of a machine closed theorem of TLA+ in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.


---

## Body

## 1. Introduction

TLA+ [1, 2] is a formal specification language for describing and reasoning about distributed and concurrent systems. It is based on mathematical logic, set theory, and linear time temporal logic TLA [3]. TLA+ is widely used to write precise and formal specifications of discrete systems. The notion of machine closed plays an important role in the system specification. Generally speaking, a specification consists of two parts: one is a safety part and the other is a liveness part. The specification is called machine closed if the liveness part does not constrain the safety part. In [1], it is said that “we seldom want to write a specification that isn’t machine closed. If we do write one, it’s usually by mistake.” Hence, we need to check whether the specification is machine closed. Fortunately, there is a well-known theorem, that is, machine closed theorem [4], stating that all the TLA+ specifications are machine closed. More precisely, a TLA+ specification which consists of a transition system and a possibly countable infinite fairness constraints is machine closed. Hence, in TLA+ there is no need to verify the specification to see whether it is machine closed. In other words, TLA+ specifications are constructed to be machine closed.We are now working on formalizing a subset of TLA+ in the theorem prover Coq. As an important part, we want to have the machine closed theorem in our formalization. There are mainly two ways to embed the theorem: one is to have it as an axiom and the other is to state it as a theorem and prove it. We think the second way is better. The reason is twofold:(i)
it needs to be very careful to introduce an axiom into a proof system, since sometimes the introduction of a new axiom may result in inconsistence;(ii)
it is worthwhile to have a formal proof of the theorem, though it is well-known. The proof will help to understand and check the previous formalizations (i.e., the fundamental definitions needed to state the theorem) and make the whole formalization more solid.In this paper, we present a formal proof of a machine closed theorem in the theorem prover Coq. In order to do so, various fundamental definitions, such as traces, properties, safety property, liveness property, safety closure, and machine closed are given. Based on these definitions, the theorem is formally stated. The proof follows [4]. The key part of the proof is to find a strategy which can generate a trace with some desired properties. We designed a reusable proof pattern to guide this process. Besides this proof, the pattern is also used in proving whether a property is a liveness property; for example, both strong and weak fairness constraints are proved to be liveness properties using this pattern. The whole proof is done in a shallow-embedded manner, which makes the formalization independent of any concrete syntaxes. In other words, this work can be reused in other settings.The rest of the paper is organized as follows. In Section2, some preliminaries and a short introduction of TLA+ are given. Section 3 presents the formalization of the machine closed theorem in Coq. The detailed proof is described in Section 4. Related work and concluding remarks are given in Section 5.


## 2. Preliminaries

### 2.1. TLA+ Specifications

The TLA+ specification is a formula of the form Init∧□[Next]v∧L, where v is a tuple usually containing all state variables in Init, Next, and L [4]. The first conjunct Init describes the possible initial states of the system. The second conjunct of the specification asserts that every step (i.e., every pair of successive states in the system) either satisfies Next or leaves the variables in v unchanged. Allowing such stuttering steps is a key ingredient to obtain compositionality of specifications. However, it also means that executions that stutter infinitely are allowed by the specification. The third conjunct L is a temporal formula stating the liveness constraints of the specification, and particularly it can be used to rule out infinite stuttering. The part Init∧□[Next]v is known to be the safety part of the specification while L to be the liveness part. The machine closed theorem states that (Init∧□[Next]v, L) is machine closed.


### 2.2. Definitions

We fix the set of states asSt. St* denotes the set of finite sequences of states, and Stω is the set of infinite sequences of states. A sequence is also called atrace in this paper. The ith state in trace t is denoted by ti. |t| denotes thelength of t, if t is finite.Aproperty is a set of infinite traces. Given a property P, we use t⊨P, which means trace t satisfies property P, to denote t∈P. Given a finite trace t∈St*, if ∃t′∈Stω.t∘t′⊨P (∘ is the traditional trace concatenation operator), then we say t⊨P. t[⋯n] and t[n⋯] denote the prefix (t0⋯tn) and suffix (tntn+1⋯) of t, respectively. Following [5], a property P is asafety property, if ∀t∈Stω.Pt↔∀i.∃t′∈Stω.t[⋯i]∘t′⊨P. A property P is aliveness property, if ∀t∈St*.∃t′∈Stω.t∘t′⊨P.Anactiona is a predicate over two states. Action a is asubaction of action a′ if ∀ss′.ass′→a′ss′.Following [6], we have the definitions of safety closure and machine closed. Given an arbitrary property P, itssafety closure  C(P) is defined as {t∈Stω∣∀i.t[⋯i]⊨P}. It can be proved that C(P) is the smallest safety property containing P.Definition. A pair of properties (S,L) is said to bemachine closed if C(S∩L)=S and S is a safety property.


## 2.1. TLA+ Specifications

The TLA+ specification is a formula of the form Init∧□[Next]v∧L, where v is a tuple usually containing all state variables in Init, Next, and L [4]. The first conjunct Init describes the possible initial states of the system. The second conjunct of the specification asserts that every step (i.e., every pair of successive states in the system) either satisfies Next or leaves the variables in v unchanged. Allowing such stuttering steps is a key ingredient to obtain compositionality of specifications. However, it also means that executions that stutter infinitely are allowed by the specification. The third conjunct L is a temporal formula stating the liveness constraints of the specification, and particularly it can be used to rule out infinite stuttering. The part Init∧□[Next]v is known to be the safety part of the specification while L to be the liveness part. The machine closed theorem states that (Init∧□[Next]v, L) is machine closed.


## 2.2. Definitions

We fix the set of states asSt. St* denotes the set of finite sequences of states, and Stω is the set of infinite sequences of states. A sequence is also called atrace in this paper. The ith state in trace t is denoted by ti. |t| denotes thelength of t, if t is finite.Aproperty is a set of infinite traces. Given a property P, we use t⊨P, which means trace t satisfies property P, to denote t∈P. Given a finite trace t∈St*, if ∃t′∈Stω.t∘t′⊨P (∘ is the traditional trace concatenation operator), then we say t⊨P. t[⋯n] and t[n⋯] denote the prefix (t0⋯tn) and suffix (tntn+1⋯) of t, respectively. Following [5], a property P is asafety property, if ∀t∈Stω.Pt↔∀i.∃t′∈Stω.t[⋯i]∘t′⊨P. A property P is aliveness property, if ∀t∈St*.∃t′∈Stω.t∘t′⊨P.Anactiona is a predicate over two states. Action a is asubaction of action a′ if ∀ss′.ass′→a′ss′.Following [6], we have the definitions of safety closure and machine closed. Given an arbitrary property P, itssafety closure  C(P) is defined as {t∈Stω∣∀i.t[⋯i]⊨P}. It can be proved that C(P) is the smallest safety property containing P.Definition. A pair of properties (S,L) is said to bemachine closed if C(S∩L)=S and S is a safety property.


## 3. Formalization of Machine Closed Theorem

We work on the semantical level, in other words, we define all the concepts described in Section2.2 in a shallow embedding manner. Throughout this section, we first describe the notions informally then give the corresponding Coq scripts.


### 3.1. Help Definitions

In the following scripts, we first define the set of state asSt. A trace is a function of type nat→St (There are other ways to define traces. E.g., [7] uses coinductive data types to define infinite traces and [8] uses coinductive data types to define both infinite and finite traces. The reasons why we adapt the “function type” one is twofold: (i) the “function type” trace is intuitive; (ii) we only consider infinite traces, and we want to separate the finite traces and infinite traces at the data type level. In the subsequent section, finite traces are defined separately using inductive data type.). So given a trace t and a natural number i, (ti) denotes the ith state of t (count from 0). PredOn1 and PredOn2 are the types of predicates over one state and two states, respectively. PredOn1 is the state predicate type while PredOn2 is the action type. A property is a set of traces, whose type is Trace→Prop. UptoNtt′n means traces t and t′ are identical up to index n. UptoN_et′t means traces t and t′ are identical up to index (n-1). Offsettn returns t[n⋯]. State1toProperty (State2toProperty, resp.) makes a trace predicate(i.e., a property) from a one-state (two-state, resp.) predicate. In order to make the representation more concise, we define three coercions which implicitly changes a one-state or a two-state predicate to properties, respectively.Variable St: Set.Definition Trace  := nat -> St.Definition PredOn1  := St -> Prop.Definition PredOn2  := St -> St -> Prop.Definition Property  := Ensemble Trace.Definition UptoN (t t’: Trace) (n:nat):Prop  :=forall i, i <= n -> t i = t’i.Definition UptoN_e (t t’: Trace)(n:nat): Prop  :=forall i, i < n -> t i = t’i.Definition OffsetN (t:Trace) (n:nat):Trace  :=fun i  => t (n+i).Definition State1toProperty (p:PredOn1): Property  :=fun t  => p (t 0).Definition State2toProperty (p:PredOn2): Property  :=fun t  => p (t 0) (t 1).Definition Actions  := PredOn2.Coercion State1toProperty: PredOn1 >->Property.Coercion State2toProperty: PredOn2 >->Property.Coercion Action2toProperty: Actions >->Property. In the following scripts, we have the traditional definitions of “finally,” “always,” “infinite often,” “finally always,” “enabled,” “strong fairness,” and “weak fairness.” Definition F (p: Property) (t:Trace):=exists n, p (OffsetN t n).Definition G (p: Property) (t:Trace):=forall n, p (OffsetN t n).Definition FG p  := F (G p).Definition GF p  := G (F p).Definition En (p2: PredOn2) (s: St)  :=exists s’, p2 s s’.Definition SF_Action (a: Actions):Property  :=fun t  => GF (En a) t -> GF a t.Definition WF_Action (a: Actions):Property  :=fun t  => FG (En a) t -> GF a t.


### 3.2.  Safety, Liveness, and Machine Closed

In the definitions of safety property, liveness property and safety closure, the notions of “finite trace” and “concatenation of a finite trace and an infinite trace” are used. Since we choose the function type to present traces, it is not very convenient to express finite traces. In order to avoid the notions of “finite trace” and “concatenation,” we should change the definitions to their equivalent counterparts which only involve infinite traces.Safety Property. We change “∀t∈Sω.Pt↔∀i.∃t′∈Sω.t[⋯i]∘t′⊨P” to its equivalent formula “∀t∈Sω.Pt↔∀i.∃t′∈Sω.(UptoNtt′i)∧t′⊨P.”Definition IsSafetyProperty (p:Property)  :=forall t, p t <-> (forall i, existst’, UptoN t t’i/∖ p t’).Liveness Property. We change “∀t∈S*.∃t′∈Sω.t∘t′⊨P” to “∀t∈Sω.∀i.∃t′∈Sω.UptoN_ett′i∧t′⊨P” and have the following definition:Definition IsLivenessProperty (p:Property)  :=forall t i, exists t’, UptoN_e t t’i/∖ p t’.Safety Closure. “{t∈Sω∣∀i.t[⋯i]⊨P}” is changed to “{t∈Sω∣∀i.∃t′.UptoNtt′i∧t′⊨P}”.Definition SafetyClosure (p: Property):Property  :=fun t  => forall i, exists t’, UptoN tt’i/∖ p t’.We use the notation mechanism of Coq to make the representations more succinct.p[/∖]q denotes that the intersection of properties p and q. p[<=]q expresses the fact that property p is a subset of property q. p[=]q describes the fact that property p is equal to property q. [C]p is the safety closure of p. [S?] is a shorthand of predicate IsSafetyProperty while [L?] is a shorthand of predicate IsLivenessProperty.Machine Closed. It is defined asDefinition MachineClosed (sp:Property): Prop  :=[C] (s [/∖] p) [=] s  /∖ [S?] s.


### 3.3.  Transition System

As described in Section2.1, the specification of a system is of form Init∧□[Next]v∧L. Guided by this form, a transition system is parameterized by(1)
the setSt of states,Variable St: Set.(2)
predicatesInit of type PredOn1St and Next of type PredOn2St characterizing the initial states and next-state relation, respectively, where we require that (Parameter is a synonym of Variable in Coq.): every state has a successor according to Next; in other words, Next is total.Parameter Init: PredOn1 St.Parameter Next: PredOn2 St.Hypothesis next_input_enabled: foralls, exists s’, Next s s’.(3)
two sets of indexes:I and J. I∪J is finite or countable infinite and each k∈I∪J, action ak is a subaction of Next. Each i∈I (j∈J, resp.), action ai (aj, resp.) is associated with a strong (weak, resp.) fairness constraint.Parameter Acts_S: nat -> Actions St.Parameter Acts_W: nat -> Actions St.Definition Acts_SF  := fun n  =>SF_Action _ (Acts_S n).Definition Acts_WF  := fun n  =>WF_Action _ (Acts_W n).Hypothesis Acts_subaction_of_Next_SF:forall i s s’, (Acts_S i) s s’->Next s s’.Hypothesis Acts_subaction_of_Next_WF:forall i s s’, (Acts_W i) s s’->Next s s’.In the scripts, we use a function of typenat→ActionsSt to represent the set of actions. Note that the cases where the set of actions is finite or countable infinite are covered by the definitions of Acts_S and Acts_W. The essential point is that both Acts_S and Acts_W are of type nat→ActionsSt. Suppose the set of I is finite, say its cardinality is N, we can build Acts_S as follows: for each i<N, map Acts_Si to the (i+1)th action in I; for each i≥N, map Acts_Si to (funss′⇒False). If the set of I is countable infinite, then for each i∈ℕ, map Acts_Si to the (i+1)th action.Based on the above definitions, we can build the safety partsp and the liveness part lp for the transition system:(i)
sp: all traces allowed by Init and Next.Definition sp  :=fun (t:Trace _)  => Init (t 0)/∖forall n, Next (t n)(t (S n)).(ii)
lp: all traces allowed by the set of fairness constraints.Definition lp: Property _  :=fun t  => forall n, Acts_SF n t/∖Acts_WF n t.Finally, we get the theorem to proveTheorem machine_closed:MachineClosed _ sp lp.


## 3.1. Help Definitions

In the following scripts, we first define the set of state asSt. A trace is a function of type nat→St (There are other ways to define traces. E.g., [7] uses coinductive data types to define infinite traces and [8] uses coinductive data types to define both infinite and finite traces. The reasons why we adapt the “function type” one is twofold: (i) the “function type” trace is intuitive; (ii) we only consider infinite traces, and we want to separate the finite traces and infinite traces at the data type level. In the subsequent section, finite traces are defined separately using inductive data type.). So given a trace t and a natural number i, (ti) denotes the ith state of t (count from 0). PredOn1 and PredOn2 are the types of predicates over one state and two states, respectively. PredOn1 is the state predicate type while PredOn2 is the action type. A property is a set of traces, whose type is Trace→Prop. UptoNtt′n means traces t and t′ are identical up to index n. UptoN_et′t means traces t and t′ are identical up to index (n-1). Offsettn returns t[n⋯]. State1toProperty (State2toProperty, resp.) makes a trace predicate(i.e., a property) from a one-state (two-state, resp.) predicate. In order to make the representation more concise, we define three coercions which implicitly changes a one-state or a two-state predicate to properties, respectively.Variable St: Set.Definition Trace  := nat -> St.Definition PredOn1  := St -> Prop.Definition PredOn2  := St -> St -> Prop.Definition Property  := Ensemble Trace.Definition UptoN (t t’: Trace) (n:nat):Prop  :=forall i, i <= n -> t i = t’i.Definition UptoN_e (t t’: Trace)(n:nat): Prop  :=forall i, i < n -> t i = t’i.Definition OffsetN (t:Trace) (n:nat):Trace  :=fun i  => t (n+i).Definition State1toProperty (p:PredOn1): Property  :=fun t  => p (t 0).Definition State2toProperty (p:PredOn2): Property  :=fun t  => p (t 0) (t 1).Definition Actions  := PredOn2.Coercion State1toProperty: PredOn1 >->Property.Coercion State2toProperty: PredOn2 >->Property.Coercion Action2toProperty: Actions >->Property. In the following scripts, we have the traditional definitions of “finally,” “always,” “infinite often,” “finally always,” “enabled,” “strong fairness,” and “weak fairness.” Definition F (p: Property) (t:Trace):=exists n, p (OffsetN t n).Definition G (p: Property) (t:Trace):=forall n, p (OffsetN t n).Definition FG p  := F (G p).Definition GF p  := G (F p).Definition En (p2: PredOn2) (s: St)  :=exists s’, p2 s s’.Definition SF_Action (a: Actions):Property  :=fun t  => GF (En a) t -> GF a t.Definition WF_Action (a: Actions):Property  :=fun t  => FG (En a) t -> GF a t.


## 3.2.  Safety, Liveness, and Machine Closed

In the definitions of safety property, liveness property and safety closure, the notions of “finite trace” and “concatenation of a finite trace and an infinite trace” are used. Since we choose the function type to present traces, it is not very convenient to express finite traces. In order to avoid the notions of “finite trace” and “concatenation,” we should change the definitions to their equivalent counterparts which only involve infinite traces.Safety Property. We change “∀t∈Sω.Pt↔∀i.∃t′∈Sω.t[⋯i]∘t′⊨P” to its equivalent formula “∀t∈Sω.Pt↔∀i.∃t′∈Sω.(UptoNtt′i)∧t′⊨P.”Definition IsSafetyProperty (p:Property)  :=forall t, p t <-> (forall i, existst’, UptoN t t’i/∖ p t’).Liveness Property. We change “∀t∈S*.∃t′∈Sω.t∘t′⊨P” to “∀t∈Sω.∀i.∃t′∈Sω.UptoN_ett′i∧t′⊨P” and have the following definition:Definition IsLivenessProperty (p:Property)  :=forall t i, exists t’, UptoN_e t t’i/∖ p t’.Safety Closure. “{t∈Sω∣∀i.t[⋯i]⊨P}” is changed to “{t∈Sω∣∀i.∃t′.UptoNtt′i∧t′⊨P}”.Definition SafetyClosure (p: Property):Property  :=fun t  => forall i, exists t’, UptoN tt’i/∖ p t’.We use the notation mechanism of Coq to make the representations more succinct.p[/∖]q denotes that the intersection of properties p and q. p[<=]q expresses the fact that property p is a subset of property q. p[=]q describes the fact that property p is equal to property q. [C]p is the safety closure of p. [S?] is a shorthand of predicate IsSafetyProperty while [L?] is a shorthand of predicate IsLivenessProperty.Machine Closed. It is defined asDefinition MachineClosed (sp:Property): Prop  :=[C] (s [/∖] p) [=] s  /∖ [S?] s.


## 3.3.  Transition System

As described in Section2.1, the specification of a system is of form Init∧□[Next]v∧L. Guided by this form, a transition system is parameterized by(1)
the setSt of states,Variable St: Set.(2)
predicatesInit of type PredOn1St and Next of type PredOn2St characterizing the initial states and next-state relation, respectively, where we require that (Parameter is a synonym of Variable in Coq.): every state has a successor according to Next; in other words, Next is total.Parameter Init: PredOn1 St.Parameter Next: PredOn2 St.Hypothesis next_input_enabled: foralls, exists s’, Next s s’.(3)
two sets of indexes:I and J. I∪J is finite or countable infinite and each k∈I∪J, action ak is a subaction of Next. Each i∈I (j∈J, resp.), action ai (aj, resp.) is associated with a strong (weak, resp.) fairness constraint.Parameter Acts_S: nat -> Actions St.Parameter Acts_W: nat -> Actions St.Definition Acts_SF  := fun n  =>SF_Action _ (Acts_S n).Definition Acts_WF  := fun n  =>WF_Action _ (Acts_W n).Hypothesis Acts_subaction_of_Next_SF:forall i s s’, (Acts_S i) s s’->Next s s’.Hypothesis Acts_subaction_of_Next_WF:forall i s s’, (Acts_W i) s s’->Next s s’.In the scripts, we use a function of typenat→ActionsSt to represent the set of actions. Note that the cases where the set of actions is finite or countable infinite are covered by the definitions of Acts_S and Acts_W. The essential point is that both Acts_S and Acts_W are of type nat→ActionsSt. Suppose the set of I is finite, say its cardinality is N, we can build Acts_S as follows: for each i<N, map Acts_Si to the (i+1)th action in I; for each i≥N, map Acts_Si to (funss′⇒False). If the set of I is countable infinite, then for each i∈ℕ, map Acts_Si to the (i+1)th action.Based on the above definitions, we can build the safety partsp and the liveness part lp for the transition system:(i)
sp: all traces allowed by Init and Next.Definition sp  :=fun (t:Trace _)  => Init (t 0)/∖forall n, Next (t n)(t (S n)).(ii)
lp: all traces allowed by the set of fairness constraints.Definition lp: Property _  :=fun t  => forall n, Acts_SF n t/∖Acts_WF n t.Finally, we get the theorem to proveTheorem machine_closed:MachineClosed _ sp lp.


## 4. Proof of Machine Closed Theorem

The proof follows the proof of Proposition  4 in [4].Given a specification of a transition system,Init∧□Next∧L where L=∀i∈I.WF(ai)∧∀j∈J.SF(aj), ∀i∈I.ai is a subaction of Next, ∀j∈J.aj is a subaction of Next and I∪J is finite or countable infinite, we need to prove that (Init∧□Next,L) is machine closed. Based on the discussion in Section 3.3, here we prove a more general case where both I and J are countable infinite. Hence, we can take I and J to be ℕ.The whole proof is divided into two steps. First, we prove that a stronger version of the specification, in which all the weak fairness constraints are changed to their strong fairness counterparts, is machine closed. Second, we prove the original specification is machine closed.


### 4.1. The Stronger Specification

To build a stronger specification, first we need a mappingf:nat→ActionsSt, which has the property that ran(Acts_S)∪ran(Acts_W)=ran(f), where ran• is the range of function •. Informally speaking, through f we can get all the actions used in the original specification. In the following scripts, even_odd_dec is deployed to test whether a natural number is even and div2n returns  n/2.Definition f (n:nat): Actions St  :=match (even_odd_dec n) with| left _  => Acts_S (div2 n)| right _  => Acts_W (div2 n)end. Then we can build the stronger specification that is equivalent to the original one except for(i)
the fairness constraintlp is replaced by lp_stronger. As we can see in the following scripts, each action is associated with a strong fairness constraint. It differs from the original one in which some actions are associated with weak fairness constraints, while the other with strong fairness constraints.Definition lp_stronger  := fun t  =>forall n, SF_Action _ (f n) t.(ii)
Based on assumptionsActs_subaction_of_Next_SF and Acts_subaction_of_Next_WF, the following theorem is proved:Theorem Acts_subaction_of_Next:forall i s s’, (f i) s s’->Next s s’.Since all the actions are indexed by a natural number and accessible through the number using f, in the sequel, we will use a natural number to represent the action: phrase “action i” is equivalent to “action f(i).”The intermediate theorem about the stronger specification isTheorem sp_lp_stronger_machine_closed:MachineClosed _ sp lp_stronger.Following the definition of machine closed, we need to prove(1)
sp is a safety property;(2)
C(sp∩lp_stronger)=sp. There are two directions:
(1.1)
C(sp∩lp_stronger)⊆sp;(2.2)
sp⊆C(sp∩lp_stronger).The set of all runs of the transition system is a safety property.Init∧□[Next], which is equal to sp, defines a transition system. Hence, condition (1) is proved. Condition (2.1) can be proved from the fact that sp∩lp_stronger⊆sp and the following theorem:Theorem SafetyClosureSmallest:forall p p’, p[<=]p’-> [S?] p’->([C] p) [<=] p’. In order to prove condition (2.2), based on the definition of safety closure, it is sufficient to prove that for each t∈sp and n∈ℕ, t[⋯n] can be extended to an infinite trace t′ such that t′∈sp∧t′∈lp_stronger. As described in [4], given t[⋯n] we need to construct a trace-generate strategy g which can generate a trace t′ and t′ have properties: t′[⋯n]=t[⋯n]∧t′∈sp∧t′∈lp_stronger.


#### 4.1.1. Trace-Generate Strategy

Roughly speaking, a trace-generate strategy is of typeS*→S, which takes a finite trace as input and returns a state. In other words, a trace-generate strategy defines a scheduling policy which returns a next state based on the state sequence the system already produced. We first define the finite trace data type FiniteTrace (list is a predefined type in Coq: Inductive list (A: Type): Type  := nil: list A—cons: A → list A → list A. The concatenation of an element a of type A and a list l of type listA is denoted by a::l.).Definition FiniteTrace  := list St. There are two ways to obtain a strategy function: (1) define it as a function of type FiniteTrace→St directly; (2) first define a relation of type FiniteTrace→St→Prop and then derive a function of type FiniteTrace→St from the relation using the classical choice axiom. In our case, we choose the second way, since we only care about the relation. And furthermore defining a relation is easier than defining a function: a function is difficult to define if the computation is complex. In our case, we essentially defined a scheduling policy, which is complex.In order to use the classic choice axiom, the relationg should be total; that is, for each finite trace t there exists a state s such that gts. We only consider this kind of strategy relations. The set of all valid strategy relations is captured by VGenStrategy.Definition GenStrategy  := FiniteTrace-> St -> Prop.Definition GenStrategyF  := FiniteTrace-> St.Definition VGenStrategy  :={g:GenStrategy∣ (forall f, existss:St, g f s)
}
. A trace t can be derived based on a valid strategy relation vsr. The main derivation steps are as follows: (1)
a strategy functionf is derived from vsr using the choice axiom;(2)
given a strategy functionf and a natural number n, prefix t[⋯n] is calculated recursively by GSF_to_FiniteTrace;Fixpoint GSF_to_FiniteTrace(sf:GenStrategyF)(n:nat){struct n
}: FiniteTrace  :=match n with| 0  => sf nil  :: nil| S n’=> let t’:= GSF_to_FiniteTracesf n’insf t’ :: t’end.(3)
the prefix is always not nil, which means we can always get the last statetn that is the nth state in t. (myhead of type ∀l:FiniteTrace.l≠nil→St returns the head of a finite trace. It requires a proof that the input finite trace is not nil. This fact is provided by theorem GSF_to_FiniteTrace_notnil.)Definition GSF_to_Trace (g:GenStrategyF): Trace  :=fun n  => myhead (GSF_to_FiniteTraceg n)(GSF_to_FiniteTrace_notnil g n). Finally we get theorem GenStrategy_to_Trace, through which we can derive a trace t based on a valid strategy g and t fulfils our constraints that (nil,t0) and (t[⋯i],ti+1) (for all i∈ℕ) satisfies the strategy relation. GetG is used to get the GenStrategy part from a VGenStrategy and GetPrefixN is used to get the first n states from a Trace. Theorem GenStrategy_to_Trace:forall g: VGenStrategy, existst:Trace,forall n, (GetG g) (GetPrefixN t n)(t n).


#### 4.1.2.  Design a Trace-Generate Strategy

Recall that we need to prove condition (2.2) in the previous subsection: given a tracet∈sp and a position n, a trace t′ should be constructed such that three properties (a) t′[⋯n]=t[⋯n], (b) t′∈sp and (c) t′∈lp_stronger are hold. To achieve the goal, firstly, we need to design a trace-generate strategy relation (the relation is designed with the three properties under consideration); secondly, we need to prove the relation is valid; at last, we need to prove the generated trace conforms to the properties. We fix t, n, ft, and s in the sequel.Define the Relation. The design principles of the relation are as follows:(1)
at any point, the set of schedulable actions should be finite and all actions in the set is enabled;(2)
at any point, if the schedulable action set is not empty, the action that has not been executed for the longest time is scheduled to execute. In event of ties, the action with minimal index is chosen. Principle 1 is the key to this principle, since if the schedulable action set is infinite, there may exist an action which is infinitely enabled but not infinitely executed;(3)
at any point, if the schedulable actions set is empty, then pickNext to execute since Next is total;(4)
t[⋯n] should be a prefix of the generated trace.The strategy is defined as:Definition MC_strategy (t:Trace _)(n:nat)  :=fun (ft:FiniteTrace St)(s:St)  =>match ft with| nil  => s = t 0| cons s’tl  =>(0<length ft<=n/∖t (length ft)=s)∖/(n<length ft/∖ (forall i,~MC_Enabled ft s’i)/∖Next s’s)∖/(n<length ft  /∖exists i,MC_Enabled ft s’i/∖MC_theMin ft s’i/∖ (Acts i) s’s)end.Intuitively “(MC_strategytn)fts” has the following implicit meanings:(i)
ft is the finite trace that the system has already produced;(ii)
if(MC_strategytn)fts holds, then s is the next state the system will generate. Depend on the length of ft, there are 4 cases of how the strategy generates a next state: (a) ft is nil; (b) |ft|≤n; (c) |ft|>n and all the actions are not enabled; (d) |ft|>n and there is an enabled action.M
C
_
t
h
e
M
i
n
f
t
s
′
i denotes that the action i has the properties mentioned in the second principle. In order to define MC_theMin, there are several concepts that need to be represented: (a) given a finite trace and an action, the number of steps that the action continuously has not been executed up to now (nsteps); (b) notion of the largest number of nonexecuted steps (MC_theLongestEnabled); (c) the smallest index with the largest nonexecuted number MC_theMin. Given a finite trace ft, a nat i, and an action predicate a, NoExeOfActionUpToftia returns the number of executable actions of ft.Fixpoint nsteps (ft:FiniteTrace St)(i:nat)(a: Actions St)
{
struct ft
}
: nat  :=if lt_le_dec i (length ft) thenmatch ft with| nil  => 0| hd  :: nil  => 0| hd  :: (hd’ :: _) as tail  =>if action_dec a hd’hd then 0else S (NoExeOfActionUpTo taili a)endelse 0.Definition MC_theLongestEnabled (ft:FiniteTrace _) s idx  :=MC_Enabled s idx/∖(forall idx’, MC_Enabled s idx’->nsteps ft idx’(f idx’)<=nsteps ftidx(f idx).Definition MC_theMin (ft: FiniteTrace_) s idx  :=MC_theLongestEnabled ft s idx/∖(forall idx’, MC_theLongestEnabledft s idx’->idx <= idx’).n
s
t
e
p
s needs more descriptions. For its arguments, ft is the finite trace, i is the index of the action and a is the action. lt_le_dec returns true if and only if its first argument is less than the second argument. The first if-statement is the key to make the schedulable action set finite, but it does so in an implicit way, which will be explained in section “Prove the Properties.” action_decahd′hd returns true if and only if ahdhd′ holds.Useful Theorems. In the sequent proofs, we want to choose an element with a specific property from a set, for example, the minimal or the maximal element from a set according to some order. We use theorems to do so and these theorems are of a similar pattern: given a set, if the set is not empty, then there exists an element in the set with some specific properties.(i)
Get the Minimal Element. The following theorem states that given a set P, if P is not empty and R is a well-founded order, then there exists a minimal element in P according to order R.Theorem ExistTheMin_general:forall (A:Set)(R: A -> A -> Prop)(P: Ensemble A),well_founded R ->(~ Empty_set _ P)->(exists n, In _ P n/∖ (forall i,In _ P i ->~ R i n)).(ii)
Get the Maximal Element. The following theorem expresses that given a set P of natural numbers, if there exists a natural number max which is larger than all the elements in P, then there exists a maximal element in P.Theorem ExistTheMax_nat:(~ Empty_set _ P) ->(exists max, (forall n, In _ Pn -> n <= max)) ->exists m, In _ P m/∖ forall n,In _ P n -> n <= m.These theorems can be thought as a kind of element choosers, which can be used to pick up a specific element from a set. Combining these choosers with proper initializations of the set predicates (i.e.,P in the theorem), we can obtain some useful complex choosers, such as the one choosing the smallest index among the indexes whose associated actions have not been executed for the longest time.(iii)
The following theorem represents that givenP, a finite set of natural numbers, and F, a relation over two natural numbers, if F is total on P (i.e., for each element in P there exists a number F-related to it), and F is transitive over the second parameter (i.e., for each element in P, if a number is F-related to the element then any number larger than the number is also F-related to the element) then there exists an m such that m is F-related to each element in P.Theorem PFiniteExistsAMax:forall (P: Ensemble nat)(F: nat->nat->Prop),Finite _ P->(forall i, In _ P i ->exists xi, F i xi) ->(forall i xi xi’, In _ P i->F ixi->xi<=xi’->F i xi’) ->exists m, forall i, In _ P i ->F i m.Prove the Validity. The validity of MC_strategy is demonstrated by the following theorem:Theorem MC_strategy_Valid:forall t n f, exists s:St, MC_strategyt n f s. The theorem is proved by case analysis, which corresponds to the four cases of MC_strategy. For the first 3 cases, they are not hard to prove. For the last case, we need to prove the following theorem: Theorem MC_theMin_Valid:forall ft s, (exists i, MC_Enabledft s i) ->exists idx, MC_theMin ft s idx. This theorem is proved based on the theorems described in the previous subsection.Prove the Properties. At this point, we have a valid trace-generate relation, based on which we obtain a generated trace. We need to prove that the generated trace conforms to the three properties.Recall thatt′ is the generated trace. Property (a) (i.e., t′[⋯n]=t[⋯n]) is ensured by the first and second cases of MC_strategy: if ft is nil, then the next state is t0; else if |ft|≤n, then the next state is t|ft|. Property (b) is proved based on the facts that: (1) t∈sp; (2) case 3 generates a next state based on Next; (3) case 4 generates a state based on an action which is a subaction of Next. The last property (c) expresses that for each action if it is infinitely enabled in trace t′, then it is also infinitely executed. We prove this by contradiction:(1)
if there is an action that is infinitely enabled but finitely executed, then there is a set of actions that are infinitely enabled but only finitely executed;(2)
properly pick an actiona from the set and a position n such that a is not executed in the suffix t′[n⋯];(3)
pick a positionm>n such that at m the next action chosen to execute by the scheduler is a, which conflicts with step 2.In order to make a concise representation, we have the following definitions:Definition NotAfter t a n  :=forall i, n<=i ->~a t[i] t[S i].Definition InfEn t a  :=GF (En a) t.For the second step, corresponding toMC_strategy, we choose action idx and n such that (n,idx) is the smallest element in {(n,idx)∣idx<=n+1∧InfEnt′(fi)∧NotAftert′(fi)n}  (the order between two pairs p1=(a1,b1) and p2=(a2,b2) is the classical lexicographic order: p1<p2≜a1<a2∨(a1=a2∧b1<b2)), that is, the smallest idx with the smallest n. The first conjunct is used to ensure that we only consider the actions whose indexes are less than the length of ft. This constraint corresponds to the first if-statement in nsteps. The second conjunct guarantees that there always is an arbitrary large position at which the action is enabled. It can be proved that the set is not empty based on the assumption in step 1. Again, there is a chooser theorem for this operation.Intuitively there is some point aftern where action idx is the next action to execute, because it has not been executed since n and its index is the smallest. Now we need to find such a point m at which:(1)
for each actionidx′≤n, one of the following cases holds:
(a)
ifidx′ is infinitely enabled and infinitely executed, then nstepst[⋯m]idx′<nstepst[⋯m]idx;(b)
ifidx′ is infinitely enabled but finitely executed, then
(i)
if actionidx′ is executed at least once after n, then nstepst[⋯m]idx'<nstepst[⋯m]idx;(ii)
if actionidx′ is not executed after n, then nstepst[⋯m]idx′≤nstepst[⋯m]idx;(c)
ifidx′ is finitely enabled, then idx′ is not enabled at m;(2)
for each actionidx′>n, nstepst[⋯m]idx′≤nstepst[⋯m]idx and idx<idx′;Suppose we findm satisfying both conditions. The theorem PropertyOfM (we omit the preconditions, since they are too many) states that idx is the smallest index with the longest nonexecute steps (i.e., MC_theMint′[⋯m]t′[m]idx), hence only the fourth case of MC_strategy can be true. Based on the uniqueness of MC_theMin, we can infer that action idx is the action the scheduler chooses to execute at m.Lemma PropertyOfM:⋯ ->MC_theMin t’[⋯m] t’[m] idx.Theorem MC_theMin_Unique:forall ft s i i’, MC_theMin fts i -> MC_theMin ft s i’->i=i’.In order to obtain suchm, we first construct that m′ s.t. condition (1) holds and then construct that m s.t. both conditions hold. We use theorem PFiniteExistsAMax to get m′. In the theorem P is the set of indexes less than (n+1) and F is defined asDefinition F  := fun i xi  =>let inf_en  := (GF St (En St (Acts i))t’) inlet inf_exe  := (GF St (Acts i) t’) inlet tp  := (GetPrefixN St t’(S xi)) inlet a  := Acts idx inlet a’:= Acts i inn <= xi/∖((inf_en/∖ inf_exe  /∖ nstep tp i a’<nstep tp idx a)∖/(inf_en/∖~ inf_exe  /∖(((exists n, min_n <= n/∖ a’(t’n)(t’(S n)))/∖nstep tp i a’< nstep tp idx a)∖/((forall n, min_n <= n ->~a’(t’n)(t’(S n)))/∖nstep tp i a’<= nstep tp idx a)))∖/(~ inf_en  /∖ (forall k, xi <= k ->  ~En St a’(t’k)))). The second conjunct consists of four disjuncts, each of which corresponds to a sub condition in condition (1). The total and transitive properties of F are proved by case analysis. By PFiniteExistsAMax we obtain the m′ which is F-related to all the actions whose indexes are less than (n+1). For each index i>n, by using theorem greater_less we know nstept[⋯m]i(fi)≤(m+1-i), and by theorem less_greater, we know m-n≤nstept[⋯m]idx(fidx); hence, we know m also holds for condition (2). Thus m is the position we want—property (c) holds on trace t′. Lemma greater_less:forall ft i a, nstep ft i a <= lengthft - i.Lemma less_greater:forall t idx a n, idx <=S n ->(forall j, n<=j ->~a (t j)(t (S j))) ->forall k, n < k -> k-n<=nstep(GetPrefixN St t (S k)) idx a.Finally, we prove that the stronger specification is machine closed.


### 4.2.  The Original Specification

Based on theoremsp_lp_stronger_machine_closed, we need to prove theorem machine_closed. According to the definition of machine closed, the proof is sketched as(1)
provesp is a safety property;(2)
proveC(sp∩lp)=sp. There are two directions:
(a)
C(sp∩lp)⊆sp. The proof is similar to the proof of condition (2.1) in Section 4.1;(b)
sp⊆C(sp∩lp). Given t and i, by theorem sp_lp_stronger_machine_closed we can get an extended trace t0 of t[⋯i] such that t0∈sp∧t0∈lp_stronger. Hence, the only subgoal needed to solve is to prove that t0 is also in lp. It is sufficient to prove that
(i)
for eachi∈I, t0 satisfies the strong fairness constraint of action ai—this holds, since t0 satisfies the strong fairness constraint of action af(2*i) which is equal to ai.(ii)
for eachi∈J, t0 satisfies the weak fairness constraint of action aj—this holds, since t0 satisfies the strong fairness constraint of action af(2*j+1) which is equal to aj and the following theorem which expresses that if a trace satisfies the strong fairness constraint of an action it also satisfies the weak fairness constraint of that action:Theorem SF_imp_WF:forall (a:Actions), SF_Actiona [->] WF_Action a.


## 4.1. The Stronger Specification

To build a stronger specification, first we need a mappingf:nat→ActionsSt, which has the property that ran(Acts_S)∪ran(Acts_W)=ran(f), where ran• is the range of function •. Informally speaking, through f we can get all the actions used in the original specification. In the following scripts, even_odd_dec is deployed to test whether a natural number is even and div2n returns  n/2.Definition f (n:nat): Actions St  :=match (even_odd_dec n) with| left _  => Acts_S (div2 n)| right _  => Acts_W (div2 n)end. Then we can build the stronger specification that is equivalent to the original one except for(i)
the fairness constraintlp is replaced by lp_stronger. As we can see in the following scripts, each action is associated with a strong fairness constraint. It differs from the original one in which some actions are associated with weak fairness constraints, while the other with strong fairness constraints.Definition lp_stronger  := fun t  =>forall n, SF_Action _ (f n) t.(ii)
Based on assumptionsActs_subaction_of_Next_SF and Acts_subaction_of_Next_WF, the following theorem is proved:Theorem Acts_subaction_of_Next:forall i s s’, (f i) s s’->Next s s’.Since all the actions are indexed by a natural number and accessible through the number using f, in the sequel, we will use a natural number to represent the action: phrase “action i” is equivalent to “action f(i).”The intermediate theorem about the stronger specification isTheorem sp_lp_stronger_machine_closed:MachineClosed _ sp lp_stronger.Following the definition of machine closed, we need to prove(1)
sp is a safety property;(2)
C(sp∩lp_stronger)=sp. There are two directions:
(1.1)
C(sp∩lp_stronger)⊆sp;(2.2)
sp⊆C(sp∩lp_stronger).The set of all runs of the transition system is a safety property.Init∧□[Next], which is equal to sp, defines a transition system. Hence, condition (1) is proved. Condition (2.1) can be proved from the fact that sp∩lp_stronger⊆sp and the following theorem:Theorem SafetyClosureSmallest:forall p p’, p[<=]p’-> [S?] p’->([C] p) [<=] p’. In order to prove condition (2.2), based on the definition of safety closure, it is sufficient to prove that for each t∈sp and n∈ℕ, t[⋯n] can be extended to an infinite trace t′ such that t′∈sp∧t′∈lp_stronger. As described in [4], given t[⋯n] we need to construct a trace-generate strategy g which can generate a trace t′ and t′ have properties: t′[⋯n]=t[⋯n]∧t′∈sp∧t′∈lp_stronger.


### 4.1.1. Trace-Generate Strategy

Roughly speaking, a trace-generate strategy is of typeS*→S, which takes a finite trace as input and returns a state. In other words, a trace-generate strategy defines a scheduling policy which returns a next state based on the state sequence the system already produced. We first define the finite trace data type FiniteTrace (list is a predefined type in Coq: Inductive list (A: Type): Type  := nil: list A—cons: A → list A → list A. The concatenation of an element a of type A and a list l of type listA is denoted by a::l.).Definition FiniteTrace  := list St. There are two ways to obtain a strategy function: (1) define it as a function of type FiniteTrace→St directly; (2) first define a relation of type FiniteTrace→St→Prop and then derive a function of type FiniteTrace→St from the relation using the classical choice axiom. In our case, we choose the second way, since we only care about the relation. And furthermore defining a relation is easier than defining a function: a function is difficult to define if the computation is complex. In our case, we essentially defined a scheduling policy, which is complex.In order to use the classic choice axiom, the relationg should be total; that is, for each finite trace t there exists a state s such that gts. We only consider this kind of strategy relations. The set of all valid strategy relations is captured by VGenStrategy.Definition GenStrategy  := FiniteTrace-> St -> Prop.Definition GenStrategyF  := FiniteTrace-> St.Definition VGenStrategy  :={g:GenStrategy∣ (forall f, existss:St, g f s)
}
. A trace t can be derived based on a valid strategy relation vsr. The main derivation steps are as follows: (1)
a strategy functionf is derived from vsr using the choice axiom;(2)
given a strategy functionf and a natural number n, prefix t[⋯n] is calculated recursively by GSF_to_FiniteTrace;Fixpoint GSF_to_FiniteTrace(sf:GenStrategyF)(n:nat){struct n
}: FiniteTrace  :=match n with| 0  => sf nil  :: nil| S n’=> let t’:= GSF_to_FiniteTracesf n’insf t’ :: t’end.(3)
the prefix is always not nil, which means we can always get the last statetn that is the nth state in t. (myhead of type ∀l:FiniteTrace.l≠nil→St returns the head of a finite trace. It requires a proof that the input finite trace is not nil. This fact is provided by theorem GSF_to_FiniteTrace_notnil.)Definition GSF_to_Trace (g:GenStrategyF): Trace  :=fun n  => myhead (GSF_to_FiniteTraceg n)(GSF_to_FiniteTrace_notnil g n). Finally we get theorem GenStrategy_to_Trace, through which we can derive a trace t based on a valid strategy g and t fulfils our constraints that (nil,t0) and (t[⋯i],ti+1) (for all i∈ℕ) satisfies the strategy relation. GetG is used to get the GenStrategy part from a VGenStrategy and GetPrefixN is used to get the first n states from a Trace. Theorem GenStrategy_to_Trace:forall g: VGenStrategy, existst:Trace,forall n, (GetG g) (GetPrefixN t n)(t n).


### 4.1.2.  Design a Trace-Generate Strategy

Recall that we need to prove condition (2.2) in the previous subsection: given a tracet∈sp and a position n, a trace t′ should be constructed such that three properties (a) t′[⋯n]=t[⋯n], (b) t′∈sp and (c) t′∈lp_stronger are hold. To achieve the goal, firstly, we need to design a trace-generate strategy relation (the relation is designed with the three properties under consideration); secondly, we need to prove the relation is valid; at last, we need to prove the generated trace conforms to the properties. We fix t, n, ft, and s in the sequel.Define the Relation. The design principles of the relation are as follows:(1)
at any point, the set of schedulable actions should be finite and all actions in the set is enabled;(2)
at any point, if the schedulable action set is not empty, the action that has not been executed for the longest time is scheduled to execute. In event of ties, the action with minimal index is chosen. Principle 1 is the key to this principle, since if the schedulable action set is infinite, there may exist an action which is infinitely enabled but not infinitely executed;(3)
at any point, if the schedulable actions set is empty, then pickNext to execute since Next is total;(4)
t[⋯n] should be a prefix of the generated trace.The strategy is defined as:Definition MC_strategy (t:Trace _)(n:nat)  :=fun (ft:FiniteTrace St)(s:St)  =>match ft with| nil  => s = t 0| cons s’tl  =>(0<length ft<=n/∖t (length ft)=s)∖/(n<length ft/∖ (forall i,~MC_Enabled ft s’i)/∖Next s’s)∖/(n<length ft  /∖exists i,MC_Enabled ft s’i/∖MC_theMin ft s’i/∖ (Acts i) s’s)end.Intuitively “(MC_strategytn)fts” has the following implicit meanings:(i)
ft is the finite trace that the system has already produced;(ii)
if(MC_strategytn)fts holds, then s is the next state the system will generate. Depend on the length of ft, there are 4 cases of how the strategy generates a next state: (a) ft is nil; (b) |ft|≤n; (c) |ft|>n and all the actions are not enabled; (d) |ft|>n and there is an enabled action.M
C
_
t
h
e
M
i
n
f
t
s
′
i denotes that the action i has the properties mentioned in the second principle. In order to define MC_theMin, there are several concepts that need to be represented: (a) given a finite trace and an action, the number of steps that the action continuously has not been executed up to now (nsteps); (b) notion of the largest number of nonexecuted steps (MC_theLongestEnabled); (c) the smallest index with the largest nonexecuted number MC_theMin. Given a finite trace ft, a nat i, and an action predicate a, NoExeOfActionUpToftia returns the number of executable actions of ft.Fixpoint nsteps (ft:FiniteTrace St)(i:nat)(a: Actions St)
{
struct ft
}
: nat  :=if lt_le_dec i (length ft) thenmatch ft with| nil  => 0| hd  :: nil  => 0| hd  :: (hd’ :: _) as tail  =>if action_dec a hd’hd then 0else S (NoExeOfActionUpTo taili a)endelse 0.Definition MC_theLongestEnabled (ft:FiniteTrace _) s idx  :=MC_Enabled s idx/∖(forall idx’, MC_Enabled s idx’->nsteps ft idx’(f idx’)<=nsteps ftidx(f idx).Definition MC_theMin (ft: FiniteTrace_) s idx  :=MC_theLongestEnabled ft s idx/∖(forall idx’, MC_theLongestEnabledft s idx’->idx <= idx’).n
s
t
e
p
s needs more descriptions. For its arguments, ft is the finite trace, i is the index of the action and a is the action. lt_le_dec returns true if and only if its first argument is less than the second argument. The first if-statement is the key to make the schedulable action set finite, but it does so in an implicit way, which will be explained in section “Prove the Properties.” action_decahd′hd returns true if and only if ahdhd′ holds.Useful Theorems. In the sequent proofs, we want to choose an element with a specific property from a set, for example, the minimal or the maximal element from a set according to some order. We use theorems to do so and these theorems are of a similar pattern: given a set, if the set is not empty, then there exists an element in the set with some specific properties.(i)
Get the Minimal Element. The following theorem states that given a set P, if P is not empty and R is a well-founded order, then there exists a minimal element in P according to order R.Theorem ExistTheMin_general:forall (A:Set)(R: A -> A -> Prop)(P: Ensemble A),well_founded R ->(~ Empty_set _ P)->(exists n, In _ P n/∖ (forall i,In _ P i ->~ R i n)).(ii)
Get the Maximal Element. The following theorem expresses that given a set P of natural numbers, if there exists a natural number max which is larger than all the elements in P, then there exists a maximal element in P.Theorem ExistTheMax_nat:(~ Empty_set _ P) ->(exists max, (forall n, In _ Pn -> n <= max)) ->exists m, In _ P m/∖ forall n,In _ P n -> n <= m.These theorems can be thought as a kind of element choosers, which can be used to pick up a specific element from a set. Combining these choosers with proper initializations of the set predicates (i.e.,P in the theorem), we can obtain some useful complex choosers, such as the one choosing the smallest index among the indexes whose associated actions have not been executed for the longest time.(iii)
The following theorem represents that givenP, a finite set of natural numbers, and F, a relation over two natural numbers, if F is total on P (i.e., for each element in P there exists a number F-related to it), and F is transitive over the second parameter (i.e., for each element in P, if a number is F-related to the element then any number larger than the number is also F-related to the element) then there exists an m such that m is F-related to each element in P.Theorem PFiniteExistsAMax:forall (P: Ensemble nat)(F: nat->nat->Prop),Finite _ P->(forall i, In _ P i ->exists xi, F i xi) ->(forall i xi xi’, In _ P i->F ixi->xi<=xi’->F i xi’) ->exists m, forall i, In _ P i ->F i m.Prove the Validity. The validity of MC_strategy is demonstrated by the following theorem:Theorem MC_strategy_Valid:forall t n f, exists s:St, MC_strategyt n f s. The theorem is proved by case analysis, which corresponds to the four cases of MC_strategy. For the first 3 cases, they are not hard to prove. For the last case, we need to prove the following theorem: Theorem MC_theMin_Valid:forall ft s, (exists i, MC_Enabledft s i) ->exists idx, MC_theMin ft s idx. This theorem is proved based on the theorems described in the previous subsection.Prove the Properties. At this point, we have a valid trace-generate relation, based on which we obtain a generated trace. We need to prove that the generated trace conforms to the three properties.Recall thatt′ is the generated trace. Property (a) (i.e., t′[⋯n]=t[⋯n]) is ensured by the first and second cases of MC_strategy: if ft is nil, then the next state is t0; else if |ft|≤n, then the next state is t|ft|. Property (b) is proved based on the facts that: (1) t∈sp; (2) case 3 generates a next state based on Next; (3) case 4 generates a state based on an action which is a subaction of Next. The last property (c) expresses that for each action if it is infinitely enabled in trace t′, then it is also infinitely executed. We prove this by contradiction:(1)
if there is an action that is infinitely enabled but finitely executed, then there is a set of actions that are infinitely enabled but only finitely executed;(2)
properly pick an actiona from the set and a position n such that a is not executed in the suffix t′[n⋯];(3)
pick a positionm>n such that at m the next action chosen to execute by the scheduler is a, which conflicts with step 2.In order to make a concise representation, we have the following definitions:Definition NotAfter t a n  :=forall i, n<=i ->~a t[i] t[S i].Definition InfEn t a  :=GF (En a) t.For the second step, corresponding toMC_strategy, we choose action idx and n such that (n,idx) is the smallest element in {(n,idx)∣idx<=n+1∧InfEnt′(fi)∧NotAftert′(fi)n}  (the order between two pairs p1=(a1,b1) and p2=(a2,b2) is the classical lexicographic order: p1<p2≜a1<a2∨(a1=a2∧b1<b2)), that is, the smallest idx with the smallest n. The first conjunct is used to ensure that we only consider the actions whose indexes are less than the length of ft. This constraint corresponds to the first if-statement in nsteps. The second conjunct guarantees that there always is an arbitrary large position at which the action is enabled. It can be proved that the set is not empty based on the assumption in step 1. Again, there is a chooser theorem for this operation.Intuitively there is some point aftern where action idx is the next action to execute, because it has not been executed since n and its index is the smallest. Now we need to find such a point m at which:(1)
for each actionidx′≤n, one of the following cases holds:
(a)
ifidx′ is infinitely enabled and infinitely executed, then nstepst[⋯m]idx′<nstepst[⋯m]idx;(b)
ifidx′ is infinitely enabled but finitely executed, then
(i)
if actionidx′ is executed at least once after n, then nstepst[⋯m]idx'<nstepst[⋯m]idx;(ii)
if actionidx′ is not executed after n, then nstepst[⋯m]idx′≤nstepst[⋯m]idx;(c)
ifidx′ is finitely enabled, then idx′ is not enabled at m;(2)
for each actionidx′>n, nstepst[⋯m]idx′≤nstepst[⋯m]idx and idx<idx′;Suppose we findm satisfying both conditions. The theorem PropertyOfM (we omit the preconditions, since they are too many) states that idx is the smallest index with the longest nonexecute steps (i.e., MC_theMint′[⋯m]t′[m]idx), hence only the fourth case of MC_strategy can be true. Based on the uniqueness of MC_theMin, we can infer that action idx is the action the scheduler chooses to execute at m.Lemma PropertyOfM:⋯ ->MC_theMin t’[⋯m] t’[m] idx.Theorem MC_theMin_Unique:forall ft s i i’, MC_theMin fts i -> MC_theMin ft s i’->i=i’.In order to obtain suchm, we first construct that m′ s.t. condition (1) holds and then construct that m s.t. both conditions hold. We use theorem PFiniteExistsAMax to get m′. In the theorem P is the set of indexes less than (n+1) and F is defined asDefinition F  := fun i xi  =>let inf_en  := (GF St (En St (Acts i))t’) inlet inf_exe  := (GF St (Acts i) t’) inlet tp  := (GetPrefixN St t’(S xi)) inlet a  := Acts idx inlet a’:= Acts i inn <= xi/∖((inf_en/∖ inf_exe  /∖ nstep tp i a’<nstep tp idx a)∖/(inf_en/∖~ inf_exe  /∖(((exists n, min_n <= n/∖ a’(t’n)(t’(S n)))/∖nstep tp i a’< nstep tp idx a)∖/((forall n, min_n <= n ->~a’(t’n)(t’(S n)))/∖nstep tp i a’<= nstep tp idx a)))∖/(~ inf_en  /∖ (forall k, xi <= k ->  ~En St a’(t’k)))). The second conjunct consists of four disjuncts, each of which corresponds to a sub condition in condition (1). The total and transitive properties of F are proved by case analysis. By PFiniteExistsAMax we obtain the m′ which is F-related to all the actions whose indexes are less than (n+1). For each index i>n, by using theorem greater_less we know nstept[⋯m]i(fi)≤(m+1-i), and by theorem less_greater, we know m-n≤nstept[⋯m]idx(fidx); hence, we know m also holds for condition (2). Thus m is the position we want—property (c) holds on trace t′. Lemma greater_less:forall ft i a, nstep ft i a <= lengthft - i.Lemma less_greater:forall t idx a n, idx <=S n ->(forall j, n<=j ->~a (t j)(t (S j))) ->forall k, n < k -> k-n<=nstep(GetPrefixN St t (S k)) idx a.Finally, we prove that the stronger specification is machine closed.


## 4.1.1. Trace-Generate Strategy

Roughly speaking, a trace-generate strategy is of typeS*→S, which takes a finite trace as input and returns a state. In other words, a trace-generate strategy defines a scheduling policy which returns a next state based on the state sequence the system already produced. We first define the finite trace data type FiniteTrace (list is a predefined type in Coq: Inductive list (A: Type): Type  := nil: list A—cons: A → list A → list A. The concatenation of an element a of type A and a list l of type listA is denoted by a::l.).Definition FiniteTrace  := list St. There are two ways to obtain a strategy function: (1) define it as a function of type FiniteTrace→St directly; (2) first define a relation of type FiniteTrace→St→Prop and then derive a function of type FiniteTrace→St from the relation using the classical choice axiom. In our case, we choose the second way, since we only care about the relation. And furthermore defining a relation is easier than defining a function: a function is difficult to define if the computation is complex. In our case, we essentially defined a scheduling policy, which is complex.In order to use the classic choice axiom, the relationg should be total; that is, for each finite trace t there exists a state s such that gts. We only consider this kind of strategy relations. The set of all valid strategy relations is captured by VGenStrategy.Definition GenStrategy  := FiniteTrace-> St -> Prop.Definition GenStrategyF  := FiniteTrace-> St.Definition VGenStrategy  :={g:GenStrategy∣ (forall f, existss:St, g f s)
}
. A trace t can be derived based on a valid strategy relation vsr. The main derivation steps are as follows: (1)
a strategy functionf is derived from vsr using the choice axiom;(2)
given a strategy functionf and a natural number n, prefix t[⋯n] is calculated recursively by GSF_to_FiniteTrace;Fixpoint GSF_to_FiniteTrace(sf:GenStrategyF)(n:nat){struct n
}: FiniteTrace  :=match n with| 0  => sf nil  :: nil| S n’=> let t’:= GSF_to_FiniteTracesf n’insf t’ :: t’end.(3)
the prefix is always not nil, which means we can always get the last statetn that is the nth state in t. (myhead of type ∀l:FiniteTrace.l≠nil→St returns the head of a finite trace. It requires a proof that the input finite trace is not nil. This fact is provided by theorem GSF_to_FiniteTrace_notnil.)Definition GSF_to_Trace (g:GenStrategyF): Trace  :=fun n  => myhead (GSF_to_FiniteTraceg n)(GSF_to_FiniteTrace_notnil g n). Finally we get theorem GenStrategy_to_Trace, through which we can derive a trace t based on a valid strategy g and t fulfils our constraints that (nil,t0) and (t[⋯i],ti+1) (for all i∈ℕ) satisfies the strategy relation. GetG is used to get the GenStrategy part from a VGenStrategy and GetPrefixN is used to get the first n states from a Trace. Theorem GenStrategy_to_Trace:forall g: VGenStrategy, existst:Trace,forall n, (GetG g) (GetPrefixN t n)(t n).


## 4.1.2.  Design a Trace-Generate Strategy

Recall that we need to prove condition (2.2) in the previous subsection: given a tracet∈sp and a position n, a trace t′ should be constructed such that three properties (a) t′[⋯n]=t[⋯n], (b) t′∈sp and (c) t′∈lp_stronger are hold. To achieve the goal, firstly, we need to design a trace-generate strategy relation (the relation is designed with the three properties under consideration); secondly, we need to prove the relation is valid; at last, we need to prove the generated trace conforms to the properties. We fix t, n, ft, and s in the sequel.Define the Relation. The design principles of the relation are as follows:(1)
at any point, the set of schedulable actions should be finite and all actions in the set is enabled;(2)
at any point, if the schedulable action set is not empty, the action that has not been executed for the longest time is scheduled to execute. In event of ties, the action with minimal index is chosen. Principle 1 is the key to this principle, since if the schedulable action set is infinite, there may exist an action which is infinitely enabled but not infinitely executed;(3)
at any point, if the schedulable actions set is empty, then pickNext to execute since Next is total;(4)
t[⋯n] should be a prefix of the generated trace.The strategy is defined as:Definition MC_strategy (t:Trace _)(n:nat)  :=fun (ft:FiniteTrace St)(s:St)  =>match ft with| nil  => s = t 0| cons s’tl  =>(0<length ft<=n/∖t (length ft)=s)∖/(n<length ft/∖ (forall i,~MC_Enabled ft s’i)/∖Next s’s)∖/(n<length ft  /∖exists i,MC_Enabled ft s’i/∖MC_theMin ft s’i/∖ (Acts i) s’s)end.Intuitively “(MC_strategytn)fts” has the following implicit meanings:(i)
ft is the finite trace that the system has already produced;(ii)
if(MC_strategytn)fts holds, then s is the next state the system will generate. Depend on the length of ft, there are 4 cases of how the strategy generates a next state: (a) ft is nil; (b) |ft|≤n; (c) |ft|>n and all the actions are not enabled; (d) |ft|>n and there is an enabled action.M
C
_
t
h
e
M
i
n
f
t
s
′
i denotes that the action i has the properties mentioned in the second principle. In order to define MC_theMin, there are several concepts that need to be represented: (a) given a finite trace and an action, the number of steps that the action continuously has not been executed up to now (nsteps); (b) notion of the largest number of nonexecuted steps (MC_theLongestEnabled); (c) the smallest index with the largest nonexecuted number MC_theMin. Given a finite trace ft, a nat i, and an action predicate a, NoExeOfActionUpToftia returns the number of executable actions of ft.Fixpoint nsteps (ft:FiniteTrace St)(i:nat)(a: Actions St)
{
struct ft
}
: nat  :=if lt_le_dec i (length ft) thenmatch ft with| nil  => 0| hd  :: nil  => 0| hd  :: (hd’ :: _) as tail  =>if action_dec a hd’hd then 0else S (NoExeOfActionUpTo taili a)endelse 0.Definition MC_theLongestEnabled (ft:FiniteTrace _) s idx  :=MC_Enabled s idx/∖(forall idx’, MC_Enabled s idx’->nsteps ft idx’(f idx’)<=nsteps ftidx(f idx).Definition MC_theMin (ft: FiniteTrace_) s idx  :=MC_theLongestEnabled ft s idx/∖(forall idx’, MC_theLongestEnabledft s idx’->idx <= idx’).n
s
t
e
p
s needs more descriptions. For its arguments, ft is the finite trace, i is the index of the action and a is the action. lt_le_dec returns true if and only if its first argument is less than the second argument. The first if-statement is the key to make the schedulable action set finite, but it does so in an implicit way, which will be explained in section “Prove the Properties.” action_decahd′hd returns true if and only if ahdhd′ holds.Useful Theorems. In the sequent proofs, we want to choose an element with a specific property from a set, for example, the minimal or the maximal element from a set according to some order. We use theorems to do so and these theorems are of a similar pattern: given a set, if the set is not empty, then there exists an element in the set with some specific properties.(i)
Get the Minimal Element. The following theorem states that given a set P, if P is not empty and R is a well-founded order, then there exists a minimal element in P according to order R.Theorem ExistTheMin_general:forall (A:Set)(R: A -> A -> Prop)(P: Ensemble A),well_founded R ->(~ Empty_set _ P)->(exists n, In _ P n/∖ (forall i,In _ P i ->~ R i n)).(ii)
Get the Maximal Element. The following theorem expresses that given a set P of natural numbers, if there exists a natural number max which is larger than all the elements in P, then there exists a maximal element in P.Theorem ExistTheMax_nat:(~ Empty_set _ P) ->(exists max, (forall n, In _ Pn -> n <= max)) ->exists m, In _ P m/∖ forall n,In _ P n -> n <= m.These theorems can be thought as a kind of element choosers, which can be used to pick up a specific element from a set. Combining these choosers with proper initializations of the set predicates (i.e.,P in the theorem), we can obtain some useful complex choosers, such as the one choosing the smallest index among the indexes whose associated actions have not been executed for the longest time.(iii)
The following theorem represents that givenP, a finite set of natural numbers, and F, a relation over two natural numbers, if F is total on P (i.e., for each element in P there exists a number F-related to it), and F is transitive over the second parameter (i.e., for each element in P, if a number is F-related to the element then any number larger than the number is also F-related to the element) then there exists an m such that m is F-related to each element in P.Theorem PFiniteExistsAMax:forall (P: Ensemble nat)(F: nat->nat->Prop),Finite _ P->(forall i, In _ P i ->exists xi, F i xi) ->(forall i xi xi’, In _ P i->F ixi->xi<=xi’->F i xi’) ->exists m, forall i, In _ P i ->F i m.Prove the Validity. The validity of MC_strategy is demonstrated by the following theorem:Theorem MC_strategy_Valid:forall t n f, exists s:St, MC_strategyt n f s. The theorem is proved by case analysis, which corresponds to the four cases of MC_strategy. For the first 3 cases, they are not hard to prove. For the last case, we need to prove the following theorem: Theorem MC_theMin_Valid:forall ft s, (exists i, MC_Enabledft s i) ->exists idx, MC_theMin ft s idx. This theorem is proved based on the theorems described in the previous subsection.Prove the Properties. At this point, we have a valid trace-generate relation, based on which we obtain a generated trace. We need to prove that the generated trace conforms to the three properties.Recall thatt′ is the generated trace. Property (a) (i.e., t′[⋯n]=t[⋯n]) is ensured by the first and second cases of MC_strategy: if ft is nil, then the next state is t0; else if |ft|≤n, then the next state is t|ft|. Property (b) is proved based on the facts that: (1) t∈sp; (2) case 3 generates a next state based on Next; (3) case 4 generates a state based on an action which is a subaction of Next. The last property (c) expresses that for each action if it is infinitely enabled in trace t′, then it is also infinitely executed. We prove this by contradiction:(1)
if there is an action that is infinitely enabled but finitely executed, then there is a set of actions that are infinitely enabled but only finitely executed;(2)
properly pick an actiona from the set and a position n such that a is not executed in the suffix t′[n⋯];(3)
pick a positionm>n such that at m the next action chosen to execute by the scheduler is a, which conflicts with step 2.In order to make a concise representation, we have the following definitions:Definition NotAfter t a n  :=forall i, n<=i ->~a t[i] t[S i].Definition InfEn t a  :=GF (En a) t.For the second step, corresponding toMC_strategy, we choose action idx and n such that (n,idx) is the smallest element in {(n,idx)∣idx<=n+1∧InfEnt′(fi)∧NotAftert′(fi)n}  (the order between two pairs p1=(a1,b1) and p2=(a2,b2) is the classical lexicographic order: p1<p2≜a1<a2∨(a1=a2∧b1<b2)), that is, the smallest idx with the smallest n. The first conjunct is used to ensure that we only consider the actions whose indexes are less than the length of ft. This constraint corresponds to the first if-statement in nsteps. The second conjunct guarantees that there always is an arbitrary large position at which the action is enabled. It can be proved that the set is not empty based on the assumption in step 1. Again, there is a chooser theorem for this operation.Intuitively there is some point aftern where action idx is the next action to execute, because it has not been executed since n and its index is the smallest. Now we need to find such a point m at which:(1)
for each actionidx′≤n, one of the following cases holds:
(a)
ifidx′ is infinitely enabled and infinitely executed, then nstepst[⋯m]idx′<nstepst[⋯m]idx;(b)
ifidx′ is infinitely enabled but finitely executed, then
(i)
if actionidx′ is executed at least once after n, then nstepst[⋯m]idx'<nstepst[⋯m]idx;(ii)
if actionidx′ is not executed after n, then nstepst[⋯m]idx′≤nstepst[⋯m]idx;(c)
ifidx′ is finitely enabled, then idx′ is not enabled at m;(2)
for each actionidx′>n, nstepst[⋯m]idx′≤nstepst[⋯m]idx and idx<idx′;Suppose we findm satisfying both conditions. The theorem PropertyOfM (we omit the preconditions, since they are too many) states that idx is the smallest index with the longest nonexecute steps (i.e., MC_theMint′[⋯m]t′[m]idx), hence only the fourth case of MC_strategy can be true. Based on the uniqueness of MC_theMin, we can infer that action idx is the action the scheduler chooses to execute at m.Lemma PropertyOfM:⋯ ->MC_theMin t’[⋯m] t’[m] idx.Theorem MC_theMin_Unique:forall ft s i i’, MC_theMin fts i -> MC_theMin ft s i’->i=i’.In order to obtain suchm, we first construct that m′ s.t. condition (1) holds and then construct that m s.t. both conditions hold. We use theorem PFiniteExistsAMax to get m′. In the theorem P is the set of indexes less than (n+1) and F is defined asDefinition F  := fun i xi  =>let inf_en  := (GF St (En St (Acts i))t’) inlet inf_exe  := (GF St (Acts i) t’) inlet tp  := (GetPrefixN St t’(S xi)) inlet a  := Acts idx inlet a’:= Acts i inn <= xi/∖((inf_en/∖ inf_exe  /∖ nstep tp i a’<nstep tp idx a)∖/(inf_en/∖~ inf_exe  /∖(((exists n, min_n <= n/∖ a’(t’n)(t’(S n)))/∖nstep tp i a’< nstep tp idx a)∖/((forall n, min_n <= n ->~a’(t’n)(t’(S n)))/∖nstep tp i a’<= nstep tp idx a)))∖/(~ inf_en  /∖ (forall k, xi <= k ->  ~En St a’(t’k)))). The second conjunct consists of four disjuncts, each of which corresponds to a sub condition in condition (1). The total and transitive properties of F are proved by case analysis. By PFiniteExistsAMax we obtain the m′ which is F-related to all the actions whose indexes are less than (n+1). For each index i>n, by using theorem greater_less we know nstept[⋯m]i(fi)≤(m+1-i), and by theorem less_greater, we know m-n≤nstept[⋯m]idx(fidx); hence, we know m also holds for condition (2). Thus m is the position we want—property (c) holds on trace t′. Lemma greater_less:forall ft i a, nstep ft i a <= lengthft - i.Lemma less_greater:forall t idx a n, idx <=S n ->(forall j, n<=j ->~a (t j)(t (S j))) ->forall k, n < k -> k-n<=nstep(GetPrefixN St t (S k)) idx a.Finally, we prove that the stronger specification is machine closed.


## 4.2.  The Original Specification

Based on theoremsp_lp_stronger_machine_closed, we need to prove theorem machine_closed. According to the definition of machine closed, the proof is sketched as(1)
provesp is a safety property;(2)
proveC(sp∩lp)=sp. There are two directions:
(a)
C(sp∩lp)⊆sp. The proof is similar to the proof of condition (2.1) in Section 4.1;(b)
sp⊆C(sp∩lp). Given t and i, by theorem sp_lp_stronger_machine_closed we can get an extended trace t0 of t[⋯i] such that t0∈sp∧t0∈lp_stronger. Hence, the only subgoal needed to solve is to prove that t0 is also in lp. It is sufficient to prove that
(i)
for eachi∈I, t0 satisfies the strong fairness constraint of action ai—this holds, since t0 satisfies the strong fairness constraint of action af(2*i) which is equal to ai.(ii)
for eachi∈J, t0 satisfies the weak fairness constraint of action aj—this holds, since t0 satisfies the strong fairness constraint of action af(2*j+1) which is equal to aj and the following theorem which expresses that if a trace satisfies the strong fairness constraint of an action it also satisfies the weak fairness constraint of that action:Theorem SF_imp_WF:forall (a:Actions), SF_Actiona [->] WF_Action a.


## 5. Related Works and Concluding Remarks

The machine closed theorem is first proved in [4]. There is already some work that embeds TLAi n a theorem prover [9], but to our best knowledge, this is the first time that the theorem is formally proved in a theorem prover. There are several other works that concern the definitions of properties. These works can be discussed in two steps. The first step is how traces are represented. In [10], a function of type nat→St is chosen, which is the same as our solution. In other works, inductive and/or coinductive types are used [7, 8, 11]. In [12], the authors propose a more general solution, in which they do not commit to a particular formalization of traces; instead, they exploit the module system of Coq and only list the interface of traces. The second step is how the safety and liveness properties are defined. In [7], the safety property is defined as a state invariant of a transition system and the liveness property is not defined formally.In this paper, we present a formal proof of the the machine closed theorem in theorem prover Coq. Various fundamental definitions, such as traces, properties, safety property, liveness property, safety closure and machine closed, are given. Based on these definitions, the theorem is formally stated and proved. The main proof of machine closed theorem is done using the section mechanism of Coq. This mechanism makes our formalization adaptable. It can be encapsulated into a module or a record. In our case study, we used the module type. The result module is general, since it is at the semantics level (because we do the proof in a shallow embedding manner) and thus is independent of any concrete syntax. This work also results in several reusable Coq libraries. The Coq scripts can be provided upon request.



---

*Source: 892832-2014-03-30.xml*