{'fraction_non_alphanumeric': 0.04133738601823708, 'fraction_numerical': 0.006363577572269288, 'mean_word_length': 4.36506835056554, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
TLC: temporal logic of distributed components

Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components.We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.


INTRODUCTION
Distributed systems are the backbone of the modern computing infrastructure. They support the reliable, scalable and responsive execution of Internet services and replicated aviation control systems, and are at the core of crypto-currencies. However, due to their combinatorially large state spaces, and node and network failures, distributed systems are complicated and prone to bugs. Therefore, they repeatedly suffer data and currency loss, and service outage [Guo et al. 2013;Web 2018a,b,c]. Several projects [Dragoi et al. 2016;Hawblitzel et al. 2015;Lesani et al. 2016;Padon et al. 2016;Rahli 2012;Wilcox et al. 2015] have been recently successful in verification of various distributed systems. However, they either do not benefit from a program logic and carry out verification in the semantic domain [Hawblitzel et al. 2015;Lesani et al. 2016;Wilcox et al. 2015], do not consider compositional reasoning [Dragoi et al. 2016;Hawblitzel et al. 2015;Padon et al. 2016;Rahli 2012], or do not verify liveness properties ].
Both operating systems, and and network middleware have been traditionally built in layers [Biagioni et al. 2001;Gu et al. 2016;Peterson and Davie 2003]. Each node hosts a stack of protocol layers and communicates with other nodes by the communication primitives at the bottom layers. This modular approach brings separation of the implementation from the interface. A higher layer only uses the interface and is separate from the implementation of the lower layers. Similarly, modular verification of each layer using only the specification of the lower layers reduces the proof engineering effort and brings scalability to the development of reliable distributed systems. Layers can be verified separately and composed to build verified stacks of distributed systems. Further, a layer remains correct if one of its lower layers is replaced with a new layer with the same specification.
This paper presents a novel framework for compositional specification and verification of distributed system stacks. Protocol designers and practitioners do reason about their distributed systems. We observe that they often state the properties of a protocol as natural language statements on events, assume the properties of the sub-protocols, and argue about correctness using intuitive arguments about the temporal precedence of the events that the protocol and the sub-protocols exchange [Cachin et al. 2011]. They find it more natural to state properties about the past events rather than add ghost state. Similarly, they prove liveness properties by simple reasoning about future events. This observation led us to the following questions: Can we capture the properties in a temporal logic for composable components? Can we capture the use of the specifications of subcomponents as a sound transformation? Can we formalize the principles used in these intuitive proofs as logical inference rules? Program logics have been traditionally developed as extensions of the classical Floyd-Hoare logic [Hoare 1969]. In the past decade, the community has witnessed increasingly complicated Hoare logics for concurrent programs that can be effectively used by experts. This project takes a distinct approach and strives to keep the formal techniques as close as possible to the practitioner language. It presents a new compositional and temporal approach to verification of stacks of distributed protocols.
We present a layered programming model to separately capture functional implementations of distributed components. Layers of components communicate through the interface of request and indication events: request events are input from the higher layer and output to the lower layers while indication events are input from the lower layers and output to the higher layer. We present a temporal assertion language on event traces to specify properties of components. The assertion language can naturally capture both safety and liveness properties of components in terms of their interface: incoming requests and outgoing indications. We present a novel program logic called TLC (Temporal Logic of Components) that features intuitive inference rules to directly reason about implementations of distributed components. We want to compositionally verify each component based on only its own implementation and the specifications of its subcomponents. Thus, we present a novel syntactic transformation to lower the temporal specifications of a component to be used as a subcomponent. We present an operational semantics for stacks of distributed components where events propagate across layers in a node, and nodes communicate via the bottom link layer in partially synchronous networks where nodes may crash. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics. We successfully applied the programming model, the lowering transformation and TLC to compose and verify stacks of fundamental distributed components including stubborn links, perfect links, best-effort broadcast, uniform reliable broadcast, epoch Paxos consensus. Further, we present our progress in proof mechanization towards building certified middleware.
The main contribution of this paper is the novel program logic TLC and the lowering transformation for compositional verification of both safety and liveness properties of distributed components. On the whole, the paper makes the following contributions: (1) a compositional programming (a) (b) (c) model for distributed stacks ( § 2) and its novel semantics ( § 6), (2) a temporal assertion language on event traces to specify safety and liveness properties of components ( § 3), and a sound composable verification technique based on lowering specifications ( § 4), (3) a program logic to reason about components ( § 5) and its soundness with respect to the semantics ( § 7) and (4) verification of stacks of fundamental distributed components (the appendix [Appendix 2020] § 5.2), and the encodings and mechanized proofs in Coq ( § 8). We start with an overview.

OVERVIEW
In this section, we present compositional verification of a small property of a simple component that uses a subcomponent. We summarize the future sections of the paper including the necessary parts of the assertion language and selected inference rules. We present the specification of the properties of the component and the subcomponent, lower the specification of the subcomponent and then apply TLC to verify a property of the component. We present a small intuitive proof in the natural language in one paragraph and then illustrate how each step of this proof is directly supported by TLC. Component Composition. We define the type of components Comp as a parametric record that is represented in Fig. 2. A component is parametric for the type of the events at the top and the bottom of the component as depicted in Fig. 1.(a). The events at the top are the interface of the component. They are the input requests of type IR and the output indications of type OI . A component may have multiple subcomponents. The events at the bottom are the output requests of types OR to and the input indications of types II from the subcomponents. We use the overline notation to denote multiple instances; for example, we use OR to denote multiple output request types, one per subcomponent. A component defines the State type and its initial value per node as the function init. It also defines three handler functions, request, indication and periodic, that are called in response to input request, input indication and periodic events. Periodic events are automatically issued regularly on correct nodes. Nodes may have crash-stop failures. A node is correct if it does not crash. The periodic handlers usually react to certain conditions; for example, when enough acknowledgements are received, an output indication is issued. Each of the three functions get the current node identifier (of type N) and the pre-state of the component (of type State) as parameters. As the next parameter, the request function gets the input request from the higher component and the indication function gets the input indication from one of the subcomponents. The handler functions return the post-state, a list of output requests (to subcomponents) and a list of output indications (to the parent component). . Σ and Π are parametric sum and product types. A component is defined as record of its State type, initialization function init and the three handler functions, request, indication and periodic, that are executed in response to input request, indication and periodic events. A stack is inductively constructed as either a component and its matching substacks, or a bottom link.
As Fig. 2 presents, we define the stack of components Stack as an inductive type that is parametrized on the interface of the stack. The interface of a stack is the top events IR and OI of its top component. A stack is inductively constructed as either a component and its matching substacks (as the inductive case) or a bottom link (as the base case). Basic links are the weakest components at the leaves of a stack. They accept requests send l (n,m) of type Req l to send message m to node n and issue indications deliver l (n,m) of type Ind l to deliver message m from node n. The semantics of a link can drop messages. However, it does not unfairly drop a particular message that is repeatedly sent. If a sender keeps resending a message and the receiver has not failed, the message is eventually delivered.
As Fig. 1.(b) and (c) show, increasingly stronger components can be built on top of basic links: stubborn links, perfect links, besteffort broadcast, uniform reliable broadcast, epoch consensus, epoch change, and Paxos (uniform) consensus. We have spent extensive effort to write proofs of correctness for these components. The implementation, properties and detailed proofs of all these components are available in the appendix [Appendix 2020] § 4 and 5.3. Fig. 1.(b) shows the stack of the uniform reliable broadcast. Two identical stacks are drawn to show replication at two different nodes. The bottom horizontal lines show the low-level message passing by the basic link. Fig. 1.(c) shows the Paxos consensus [Lamport 1998]  The stubborn link repeatedly resends messages by the basic link so that they are eventually delivered. However, retransmission results in multiple deliveries that may not be desired by the higher-level components. Thus, the perfect link component is built on top of the stubborn link to eliminate duplicate messages. It keeps track of delivered messages and ignores duplicates. Fig. 3.(a) presents the perfect link component, PLC. (We will visit the parts (b) and (c) of Fig. 3 later in this section.) PLC provides the perfect link interface and uses a substack with the stubborn link interface. The state of each node stores the number of messages sent by the current node, counter, initialized to zero and the set of received message identifiers, received, initialized to empty (at L 2 -L 4 ). The counter is used to assign unique numbers to messages that the node sends. Each message can be uniquely identified by the pair of the sender node identifier and the number of the message in that node. Upon a request to send a message (at L 6 -L 9 ), the counter is incremented (at L 10 ) and the PLC∶ Component Req pl Ind pl (Req sl ,Ind sl ) L 1 let slc ∶= 0 in L 2 ∐︀State ∶= ∐︀counter∶ Nat, let or ∶= (slc,send sl (n ′ ,∐︀c ′ ,m̃︀)) in L 12 ∐︀∐︀c ′ ,r̃︀,(︀or ⌋︀,(︀⌋︀̃︀, ∐︀∐︀c,r ′̃︀ ,(︀⌋︀,(︀oi⌋︀̃︀ L 25 end L 26 L 27 periodic ∶= λ n,s. ∐︀s,(︀⌋︀,(︀⌋︀̃︀̃︀ (a) SL 1 (Stubborn delivery): n ∈ Correct ∧ n ′ ∈ Correct → (n • ⊺ ↓ send sl (n ′ ,m)) ⇒ □◇(n ′ • ⊺ ↑ deliver sl (n,m)) If a correct node n sends a message m to a correct node n ′ , then n ′ delivers m infinitely often.
SL 2 (No-forge): (n • ⊺ ↑ deliver sl (n ′ ,m)) (n ′ • ⊺ ↓ send sl (n,m)) If a node n delivers a message m with sender n ′ , then n ′ previously sent m to n. (b) ) If a correct node n sends a message m to a correct node n ′ , then n ′ will eventually deliver m.
⌋︀ If a message is sent at most once, it will be delivered at most once.
PL 3 (No-forge): (n • ⊺ ↑ deliver pl (n ′ ,m)) (n ′ • ⊺ ↓ send pl (n,m)) If a node n delivers a message m with sender n ′ , then n ′ previously sent m to n. (c) The assertion (n • ⊺ ↓ send sl (n ′ ,m)) describes an event at node n at the top level interface ⊺ for the request ↓ to send the message m to the node n ′ , i.e., send sl (n ′ ,m). The assertion (n • ⊺ ↑ deliver sl (n ′ ,m)) describes an event at node n at the top level interface ⊺ for the indication ↑ to deliver the message m from the node n ′ , i.e., deliver sl (n ′ ,m). Correct is the set of nodes that have not crashed. message is sent together with the new counter value using the stubborn link subcomponent (at L 11 -L 12 ). Upon a delivery indication of a message from the stubborn link subcomponent (at L 15 -L 18 ), if the message is already received, it is ignored (at L 19 -L 20 ). Otherwise, the message identifier is added to the received set and a delivery indication event is issued (at L 21 -L 24 ). (In component descriptions, we write a sum term constructed from a term t of the i-th type parameter as (i,t) for brevity.) Finally, PLC does not need a periodic handler (at L 27 ). Semantics. In § 6, we define the operational semantics of distributed components. It models the propagation of events across the stack, message passing across nodes in partially synchronous networks and node failures. Here, we illustrate the structure of a stack and a fragment of a round of a trace in Fig. 4. Components are represented as boxes and the orientation o of request, periodic and indication events are shown as ↓, ⇝ and ↑ respectively. Incoming events are executed on the component itself and outgoing events are issued to be executed on other components. The distinct location identifier d of a component in the tree of a distributed stack is the reverse list of branch indices from the top component to that component. Going down and up the tree simply corresponds to adding and removing a subcomponent index at the head of this list. For example, the identifier d for the top component C 1 is (︀⌋︀, for its left child C 2 is (︀0⌋︀ and for its right grandchild C 5 is (︀1,0⌋︀. The interface of each component is the events immediately above it and they share its identifier. For example, the identifier d of the right child C 3 and its interface events are both (︀1⌋︀. Similarly, the location identifier of a substack is the location identifier of its top component. For example, the left substack rooted at C 2 is at location (︀0⌋︀. A simple trace is shown on the right of Fig. 4 where the lines show a sequence of events from left to right at different interface levels. The execution of an event at a component updates the state of the component and may issue other request and indication events. The issued events are subsequently executed. The trace starts with e 1 , a request ↓ at the top (︀⌋︀ from the client. When e 1 is processed in the top component C 1 at (︀⌋︀, e 2 , a request ↓ on the left child component C 2 at (︀0⌋︀ is issued. When e 2 is processed in C 2 , in turn, e 3 , a request ↓ to its right child C 5 at (︀1,0⌋︀, is issued. Processing of e 3 on C 5 issues e 4 , an indication ↑ event at (︀1,0⌋︀. When e 4 is processed in the parent component C 2 at (︀0⌋︀, e 5 that is an indication ↑ at (︀0⌋︀, is issued. (We note that C 2 could instead issue another request like e 3 to one of its children.) When e 5 is executed at the parent component C 1 at (︀⌋︀, finally, e 6 that is an indication ↑ at the top level (︀⌋︀, is issued (that is executed in the client). An (infinite) sequence of event labels is an execution trace. Given a stack, the semantics defines its set of execution traces. Assertion Language. To represent the specifications of distributed component stacks, we define a temporal assertion language that can describe traces of events across the stack. It features specific variables for the properties of the handler calls and a location variable to distinguish the unique places of the composed components in the stack. It can concisely capture safety and liveness properties of distributed components. In § 3, we will describe the assertion language and here, briefly describe the parts that we use in the overview. The always assertion □ states that the assertion holds at every event in the future including the current event. The always in the past assertion ⊟ states that holds at every event in the past including the current event. The eventually assertion ◇ states that holds at some future event. The eventually in the past assertion states that holds at some past event. The strict versions□,⊟,◇ andˆ exclude the current event. The strong implication ⇒ ′ is syntactic sugar for □( → ′ ) where → is the logical implication. The leads-to assertion ⇝ ′ is syntactic sugar for □( → ◇ ′ ). Similarly, the preceded-by assertion ′ is syntactic sugar for □( → ′ ). An assertion is non-temporal if it does not include any temporal operators. The user events are the event objects that the protocol handlers take as argument and issue, for example send pl (n,m). A trace event represents the execution of a user event by a handler. The assertion language can describe event traces across the stack. Variables are partitioned into rigid and flexible variables. A rigid variable has the same value in all events of an execution, while a flexible variable may assume different values in different events. We represent the flexible variables with the bold face. The flexible variables for an event are the identifier n of the node that executes the event, the round number r that executes the event, location identifier d that the event is executed at, the orientation o of the event, the user event e that is processed, the output requests ors and output indications ois that the event issues, the pre-state s of the event, and the post-state s ′ of the event. The pre and the post-state represent functions from node identifiers to the state of the component at the nodes. We call the top component self as it is the top component that is verified assuming the correctness of the subcomponents. We use the syntactic sugar assertion self to describe events that are applied to the top component. A self event is either a request or periodic event at the top or an indication event from a subcomponent at the second level. The constants Correct represents the set of identifiers of correct node, i.e., the nodes that have not crashed.
The syntactic sugar assertion n • (where • is used as a separator) is sugar for n = n ∧ ; it describes an event that is executed at node n and satisfies . The syntactic sugar assertion ⊺ o e stands for d = (︀⌋︀ ∧ o = o ∧ e = e; it describes an event that is at the top (⊺) level interface (︀⌋︀, its orientation is o (either the constant ↓ for requests, ⇝ for periodics or ↑ for indications) and its user event is e. For example, the assertion (n • ⊺ ↓ send sl (n ′ ,m)) describes an event at node n at the top level interface (︀⌋︀ where the request (↓) event send sl (n ′ ,m) is executed. As the periodic handler is not called with a user event, we use the constant per to represent periodic user events. Similarly, the syntactic sugar assertion i o e stands for d = (︀i⌋︀ ∧ o = o ∧ e = e; it describes an event that is at the interface of the i-th subcomponent at location (︀i⌋︀, its orientation is o and its user event is e. For example, the assertion (n • 1 ↑ deliver sl (n ′ ,m)) describes an event at node n at the interface location (︀1⌋︀ where the indication (↑) event deliver sl (n ′ ,m) is executed. It is notable that as a pleasant result of compositional reasoning, we only need to refer to the events at the top and events at the second level. Therefore, we defined syntactic sugar for only the first two levels.
Specifications. Fig. 3.(b) and (c) shows the specification of stubborn links and perfect links that are written almost verbatim from their natural language descriptions. A stubborn link stubbornly retransmits messages. The stubborn delivery property SL 1 states that once a message is sent, it is delivered infinitely often. The no-forge property SL 2 states that a stubborn link never forges a message. The properties SL 1 and SL 2 are liveness and safety properties respectively. Intuitively, a safety property states that a bad state never happens and a liveness property states that a good state eventually happens. The reliable delivery property PL 1 states that perfect links can reliably transmit messages between correct nodes. The no-duplication property PL 2 states that perfect links do not redundantly deliver messages. (It is notable that (p ⇒⊟¬p) → (p ⇒□¬p); hence the□ conjunct is omitted in the no-duplication property.) The no-forge property PL 3 states that perfect links do not forge messages. The property PL 1 is a liveness and the properties PL 2 and PL 3 are safety properties.
The specification of a component is simply written when it is the main component at the top of the stack in terms of its interface: its incoming requests and outgoing indications. It can then be lowered to any subcomponent location. We note that as the location is always the top ⊺ in specifications, it can be elided in specifications for brevity. Further, if we add the convention that the event names such as send and deliver are used for only either requests or indications, the orientation arrows ↓ for request and ↑ for indication can be removed from the specifications as well; they can be derived from the event. For example, send is a always a request and deliver is always an indication. Then, for example, the no-forge property of stubborn links SL 2 in Fig. 3 can be summarized as the following assertion: (n • deliver sl (n ′ ,m)) (n ′ • send sl (n,m)). If a node n delivers a message m with sender n ′ , then n ′ previously sent m to n. This specification seem to be the bare minimum to match the corresponding natural language statement. To keep the uniformity of assertions, we make the location and orientation explicit in the specifications.
Lowering Specifications. We now showcase lowering specifications and the program logic inference rules with the short proof of the no-forge property of the perfect link component PLC.
PLC uses the stubborn link interface and relies on its properties. The specification of the stubborn link in subcomponent. When a component is used as a subcomponent, its events are at lower locations and are also interleaved with the events of the parent and sibling components. Given the top-level specification of the stubborn link, how can we transform it to be used as the specification of a subcomponent for the perfect link? Not every assertion can be lowered. In § 4, we present an invariant assertion language that is restrictive enough to be lowered by a syntactic transformation and expressive enough to capture component specifications.  (b)). Consider that we have a stack with the component c at the top and the substacks i , i.e., = stack(c, i ). We want to verify that satisfies its specification (Fig. 5.(c)). What can we assume for each subcomponents i ? We define the translation function lower on invariants and show that to prove the validity of for , it is sound to assume lower(i,ℐ (︀⌋︀ i ) and derive in TLC, i.e., lower(i,ℐ The SL 2 assertion is in the invariant sub-language. Applying the lower transformation to SL 2 to use it as the 0-th subcomponent results in the following: We will see the transformation details later in § 4, but notice here that top ⊺ is changed to 0. The lowering transformation can be similarly applied to SL 1 to result in SL ′ 1 . The judgements of the logic are of the form Γ ⊢ c that states that under assumptions Γ, the assertion holds for the component c. We assume the two lowered assertions; thus, we have Γ = SL ′ 1 ,SL ′ 2 . Program Logic. We now showcase the program logic using a simple example. The no-forge property of perfect links states that a perfect link delivery event is preceded by a corresponding perfect link send event. We want to apply TLC to prove the following judgement that states that assuming Γ, the no-forge property is valid for PLC. Γ ⊢ PLC (n • ⊺ ↑ deliver pl (n ′ ,m)) (n ′ • ⊺ ↓ send pl (n,m)) At a high-level level, the proof shows a precedence sequence that transitively imply the desired precedence. The proof steps are illustrated in Fig. 7. Step 1: A perfect link delivery event is executed; hence, the event should have been previously issued.
Step 2: By the component implementation Fig. 6. Three Selected TLC Inference Rules and Two Basic Temporal Logic Lemmas Fig. 7. Illustration of the Proof Steps. The trace is a sequence of events from left to right. Each rectangle represents an event. In a sequence of steps, the proof shows that a perfect link deliver event deliver pl is preceded by a perfect link send event send pl . Fig. 3.(a)), a perfect link delivery event is issued by only the indication handler function. Thus, the issuing event is a stubborn link delivery event.

(in
Step 3: By the no-forge property of stubborn links, a stubborn link delivery is preceded by a stubborn link send.
Step 4: A stubborn link send event is executed before; thus, it should have been previously issued.
Step 5: By the component implementation (in Fig. 3.(a)), a stubborn link send event is issued by only the request handler function. Thus, the issuing event is a perfect link send event. By the transitivity of precedence, it is concluded form the above steps that A perfect link delivery is preceded by a perfect link send.
The rules and lemmas that we use for this proof are presented in Fig. 6. We will look at the rules closely in § 5. Here, we use two basic rules: rule OR ′ and rule OI ′ , one derived rule: rule InvL and two basic temporal logic lemmas Trans and Trans . Intuitively, the two rules OR ′ and OI ′ state that if an event is executed, it should have been previously issued. The rule OR ′ states that if at a node n and the subcomponent i, a request ↓ event e is processed, then in the past, at the same node n, the request (i,e) is issued by a self event. Similarly, the rule OI ′ states that if at a node n and at the top level ⊺, an output indication ↑ event e is processed, then in the past, at the same node n, the indication e is issued by a self event. The rule InvL states that if a non-temporal assertion holds for all the three handler functions of the component, request, periodic and indication, then the assertion holds in every self event. It is notable that InvL reduces a temporal global assertion to non-temporal local proof obligations: each premise of this rule is a non-temporal assertion about a single handler function. Thus, the functional implementation of the component can be directly used to infer its properties. The two temporal logic lemmas Trans and Trans state basic temporal transitivity properties. By rule OI ′ , we have Step 1: Γ ⊢ PLC (n • ⊺ ↑ deliver pl (n ′ ,m)) ⇒ (n • deliver pl (n ′ ,m) ∈ ois ∧ self) that states that if a perfect link indication is executed, it is previously issued by a self event. We now prove that it is issued only when a stubborn link delivery is executed. We use rule InvL with = n • deliver pl (n ′ ,m) ∈ ois → ∃c. (n • 0 ↑ deliver sl (n ′ ,∐︀c,m̃︀)) Considering the implementation in Fig. 3.(a), the two cases for request and periodic are straightforward as ois = (︀⌋︀ in both and the premise is refuted. The other case is for indication where the stubborn link indication is executed. Thus, by rule InvL (and then reducing two implications to one), we have: Step 2: By Lemma Trans on Eq. 2 and Eq. 4, and existential elimination for c, we have that states that the perfect link delivery event is preceded by a stubborn link delivery event.

ASSERTION LANGUAGE
We now present the assertion language of TLC in Fig. 8. It is a temporal language on event traces of stacks composed of distributed components. It can concisely capture both safety and liveness properties. We have already seen parts of the language in § 2; we consider the rest here.
The constants N and Correct are the set of participating and correct node identifiers respectively. Similar to classical first-order logic, a term t can be a variable, a constant or an application of a function f to other terms. As the pre-state s and post-state s ′ variables have function values, a term can be constructed by applying a variable to terms as well.
An atomic assertion is an application of a predicate p to terms. All propositional and quantified formula can be constructed as syntactic sugar to conjunction, negation and universal quantification.
Assertion for the stack at location d: ⋃︀ t ∈ Correct and ◯ and Ⓢ are not used. Invariant for the stack at location d: ℐ ∶= □ such that ◯ and Ⓢ are not used. Syntactic Sugar:

Fig. 8. Assertion Language
Similarly, the grammar only shows the strict versions of the temporal operators as the non-strict versions can be defined as syntactic sugar. The temporal operators that we did not introduce in § 2 are ◯ and Ⓢ . The next operator ◯ states that its operand assertion holds in the immediate next event. The self subtrace is the sequence of events executed on the top component. The self operator Ⓢ allows stating assertions about the self subtrace. The assertion Ⓢ asserts on the self subtrace. The self operator is usually used as the outermost operator. We use ℐ d to represent invariant assertions for the substack at location d. The specification of a component is written when it is at the top (︀⌋︀ as a top-level invariant ℐ (︀⌋︀ . An invariant ℐ d is of the form □ d . To support lowering, the atomic assertions used in an assertion d are constrained to have the form The location variable d is explicitly equal to an extension d ′ of d, i.e., the event is executed under the substack at location d. For example, the event at location (︀2,1,0⌋︀ is executed under the 0-th child of the top component, i.e., (︀2,1,0⌋︀ ⊇ (︀0⌋︀. The assertion also includes explicit equalities for the executing node n, the orientation o and the user-level event e. Further, invariant assertions do not use the next ◯ or self Ⓢ operators.

SPECIFICATION LOWERING
The presented programming model allows a component to be programmed using subcomponents. The goal of compositional verification is to verify the component using only the specifications (and not the implementations) of the subcomponents. The specification of each component is written when it is the main component at the top of the stack; however, it should be later used as the specification of a subcomponent. A fundamental question is how the specification of a component should be lowered to be used as a subcomponent. The lowered specifications of the subcomponents are used as assumptions to verify the specification of the new parent component (that is programmed on top of the subcomponents). In this section, we define the lowering transformation on specification assertions and prove its soundness. Lowering is not possible for every assertion. We observed that lowering specifications requires certain information, such as the location of events, to be present and certain operators, such as next, to be absent from the specification. We identify a subset of the assertion language that is both restrictive enough to allow the definition of the lowering transformation and expressive enough to represent specifications. As we saw in Fig. 5, the specification of each stack i is given as an invariant ℐ (︀⌋︀ i (Fig. 5.(a) and (b)). We have a stack with the component c at the top and the substacks i , i.e., = stack(c, i ). We want to verify that satisfies its specification (Fig. 5.(c)). We define the translation function lower on invariants and show that to prove the validity of for , it is sufficient to assume lower(i,ℐ (︀⌋︀ i ) and derive in TLC. Fig. 9 represents the the function lower on the invariant sub-language ℐ (︀⌋︀ . It first pushes and then restricts the assertion. We visit each in turn.
Pushing. For the component at the top, the semantics of stacks models the most general client that may issue any request. However, when the component is used as a subcomponent, the parent component may only issue a subset of the possible requests. Therefore, if a stack is pushed from the top to a lower layer, its set of subtraces can only become smaller (or stay the same). Thus, the specification of a stack at the top level can serve as a starting point for its specification as the substack i. However, the stack is now used at a deeper level. The location of every event of the stack is now under branch i. For example, the location of its highest events is (︀⌋︀ when it is at the top and is (︀i⌋︀ when it is at the i-th substack. Similarly, an event at location (︀1⌋︀ is pushed to location (︀1,i⌋︀. Therefore, the first transformation is to push the locations under branch i. The function push is defined in Fig. 9. As we saw in the definition of the invariant sub-language ℐ d ∶= □ d , the location values d ′ ⊇ d are explicit in assertions d . Given a top-level assertion (︀⌋︀ and a branch index i, the function push translates the location value from d ′ to i ∶∶∶ d ′ . Appending i to d ′ effectively pushes the events to branch i. lower(0,(n • ⊺ ↑ deliver sl (n ′ ,m)) (n ′ • ⊺ ↓ send sl (n,m))) = (11) Restricting. When a stack is at the top, all events belong to that stack. However, when it is pushed to a substack, its events are interleaved with events from the top component and the sibling substacks. Therefore, the second transformation is to restrict the specification to remain valid on traces that are extended with interleaving events. Consider a specification □ for a stack. After pushing the assertion to the i-th substack, the resulting assertion □push(i, ) does not necessarily remain valid because although the assertion push(i, ) is valid on events under branch i, it may simply not be valid on events of the top component and the sibling substacks. Thus, the restricting condition of being under branch i should be added and the assertion □push(i, ) is translated to □(d ⊇ (︀i⌋︀ → push(i, )). (The assertion push(i, ) should be recursively translated as well.) As the definition of the function restrict in Fig. 9 shows, the other variants of the always operator are translated similarly. On the other hand, an eventually assertion ◇ remains the same. If an event will happen in the future, it will still happen if other events are interleaved before it. Similarly, the other variants of the eventually operator remain the same.
As an example, Fig. 10 elaborates lowering of SL 2 that we saw in Eq. 1. The property SL 2 is in the invariant language ℐ (︀⌋︀ and can be easily lowered by the syntactic transformation. The steps follow the definition in Fig. 9. We only explain a couple of subtleties. In Eq. 12 -Eq. 13, the push function translates d = (︀⌋︀ to d = (︀0⌋︀. Thus, in the syntactic sugar, ⊺ is translated to 0. In Eq. 14, the syntactic sugar (n • 0 ↑ deliver sl (n ′ ,m)) includes the conjunct d = (︀0⌋︀. From basic propositional logic, for any and ′ , we have that We note that if the location was not explicit in the assertion, the assertion could not be pushed and would remain too general. For example, consider the assertion e = send(n,m) ⇒ m > 0 for a stack components. However, they are useful for intermediate verification steps. For example, the basic inference rule PostPre that we will see in the next section uses both of these operators.
Soundness. The following theorem states the soundness of the lowering transformation for compositional reasoning. If a top-level invariant ℐ

TLC INFERENCE RULES
In this section, we present the basic and derived inference rules of TLC. The basic inference rules are intuitive and fit in half a page. Yet, they provide the basis for verification of full stacks such as Fig. 1.(b) and (c). During the verification of the use-case protocols, we incrementally captured the fundamental reasoning steps as the basic rules. Further, we captured the higher-level reasoning steps as derived rules. The sequent judgements are of the form Γ ⊢ c where c is the component, Γ is a set of assumed assertions and is the deduced assertion. The inference rules axiomatize the properties of the semantics and the low-level communication primitive. More importantly, they allow deducing assertions about execution traces from the functional definition of the component. Fig. 11 presents the basic inference rules of TLC. (We elide the standard rules of sequent logic to the appendix [Appendix 2020] § 1.1). Further, we present a few derived rules in Fig. 12. A full list of derived rules are available in the appendix [Appendix 2020] § 1.3. The first three rules IR, II and Pe state that when an event is executed on the top component, the corresponding handler function of the component is applied. These rules take the reasoning to the functional definition of the component. (Rule IR): The rule IR (for input request) states that if at the top level ⊺, a request ↓ event e is executed then the request c handler function is called at that step. The request c function of the component c represents a relation between its inputs: the stepping node n, the pre-state s(n) of n, and the user event e, and its outputs: the post-state s ′ (n), the issued output requests ors and the issued output indications ois. The rules II (for input indication) and Pe (for periodic) are similar. (Rule II): The rule II states that if an indication ↑ event e from the i-th subcomponent is executed then the indication c handler function is called. (An indication event e from a subcomponent i is passed to the indication c function as the sum term (i,e).) (Rule Pe): The rule Pe states that if at the top ⊺, a periodic ⇝ event per is executed then the periodic c handler function is called.
The next four rules axiomatize the relation of issued and executed events. The rules OR and OI state that an event that is issued for a component is eventually executed on the component, and the rules OR ′ and OI ′ state that executed events are previously issued. These rules let the reasoning follow a chain of steps. (Rule OR): An output request from the top component is an IR ⊢c ⊺ ↓ e ⇒ (s ′ (n),ors,ois) = request c (n,s(n),e) II ⊢c i ↑ e ⇒ (s ′ (n),ors,ois) = indicationc (n,s(n),(i,e)) Pe ⊢c ⊺ ⇝ per ⇒ (s ′ (n),ors,ois) = periodic c (n,s(n)) OR ⊢c n • (i,e) ∈ ors ∧ self ⇒◇(n event e to a subcomponent i that is issued as the sum term (i,e). The rule OR (for output request) states that if at a node n, an output request (i,e) is issued by a self event, then eventually at n and the subcomponent i, the request ↓ event e is executed. (Rule OI): Similarly, the rule OI (for output indication) states that if at a node n, an output indication e is issued by a self event, then eventually at n and the top level ⊺, the indication ↑ event e is executed. The rules OR ′ and OI ′ state the relation of issued and executed events in the opposite direction of the rules OR and OI. (Rule OR ′ ): The rule OR ′ states that if at a node n and a subcomponent i, a request ↓ event e is executed, then in the past, at that node n, the request event for that subcomponent (i,e) is issued by a self event.
(Rule OI ′ ): Similarly, the rule OI ′ states that if at a node n and the top level ⊺, an output indication ↑ event e is executed, then in the past, at that node n, that indication event e is issued by a self event.
(Rule APer): The rule APer (for always periodic) states that if a node is correct, it infinitely often executes the periodic event.
(Rule ASelf): The self subtrace is the sequence of events executed on the top component. The rule ASelf (for always self) states that every event in the self subtrace is a self event. (Rule SInv): The rule SInv (for self invariant) states that an invariant for the self subtrace can be transformed to an invariant for the whole trace and vice versa using the restrict function that we saw earlier in Fig. 9. An invariant ℐ holds in the self subtrace if and only if the restriction of the assertion restrict(self,ℐ) holds in the whole trace. As the invariant continues to hold in the self events of the whole trace, the restriction condition is the self assertion. The rules ASelf and SInv lead to the derived rule InvLSe (in Fig. 12). (Rule InvLSe): The rule InvLSe states that if a non-temporal assertion holds for all the three handler functions, request, indication and periodic, then the assertion holds in every self event. We note that this rule reduces a global temporal assertion down to local non-temporal proof obligations about the handler functions. Let us see how the the rule InvLSe is derived. First, the self assertion in the rule ASelf is expanded to the disjunction of three request, indication or periodic events: Then, for the three cases, the rule SInv is applied to the assertions that the rules IR, II and Pe state (for the whole trace) to derive the same assertions under the self operator (for the self subtrace). For example, after basic logical rewriting, the assertion of the rule IR can be restated as ⊢ c □(︀self → (⊺ ↓ e → (s ′ (n),ors,ois) = request c (n,s(n),e))⌋︀ that is equivalent to the following assertion. (We remember that ⇒ ′ is defined as □( → ′ ).) ⊢ c restrict(self, ⊺ ↓ e ⇒ (s ′ (n),ors,ois) = request c (n,s(n),e)) Then, the result of applying the rule SInv is which is the same assertion as the rule IR but for the self subtrace. Then, by the classical temporal logic, the three non-temporal implications in the assumptions of the rule InvLSe can be generalized to strong implications. For example, the first assumption of the rule InvLSe can be generalized to ⊢ c Ⓢ (⊺ ↓ e ∧ request c (n,s(n),e) = (s ′ (n),ois,ors)) ⇒ From Eq. 20 and Eq. 21, we immediately have Therefore, the request event ⊺ ↓ e in Eq. 17 can be rewritten to . The other disjuncts can be similarly rewritten. The result is Ⓢ □ that is the conclusion of the rule InvLSe. Similarly, the rule InvL that we saw in the overview section (in Fig. 6) is in fact derived by applying the rule SInv to the rule InvLSe (in Fig. 12).
(Rule Init): The rule Init states that at the beginning of the execution, the state s of every node n is the state defined by the init c function of the implementation. (Rule PostPre): The rule PostPre states that in the self subtrace, the post-state s ′ of every event is the pre-state s of the next event. We note that this assertion does not hold on the whole trace as the events of different components are interleaved. (Rule SEq): The rule SEq (for state equality) states that if the stepping node n is not a node n, then the state of n stays unchanged ie. its pre-state s(n) and post-state s ′ (n) are equal.
The above four rules derive inductive inference rules for the state of the top component. Let us consider the derived rule InvSSe ′ in Fig. 12. (Rule InvSSe ′ ): The rule InvSSe ′ states that if a state predicate S holds in the initial state and all the three handler functions, request, indication and periodic preserve S, then S always holds in the self events. This rule is used to prove state invariants. Similar to the rule InvLSe, this rule reduces a global temporal assertion to local non-temporal assertions about the handler functions. To derive this rule, the rule Init is used in the base case. For the inductive case, the rule PostPre brings the invariant S on the post-state of an event to the pre-state of the next event. To show that each step preserves the invariant, there are two cases. If the node is not stepping, the rule SEq is used. If it is, expanding self in the rule ASelf leads to a case-analysis for the handler functions that directly proved by the assumptions of the rule InvSSe ′ .
(Rule RSeq): The rule RSeq (for round sequence) states that the round numbers are non-decreasing. Messages are transmitted using basic links at the leaves of the stack. A basic link is a weak communication primitive; it can drop, reorder and duplicate messages. The next three rules, GST, FDup and NForge, state the properties of basic links. Stronger communication primitives can be programmed based on these properties. (Rule GST): The rule GST states that after the round r GST InvLSe ∀e. ⊺ ↓ e ∧ request c (n,s(n),e) = (s ′ (n),ois,ors) → ∀e,i. i ↑ e ∧ indicationc (n,s(n),(i,e)) = (s ′ (n),ois,ors) → ⊺ ⇝ per ∧ periodic c (n,s(n)) = (s ′ (n),ois,ors) → non-temporal (Global Stabilization Time) if a message is sent to a correct node, it is delivered in the same round. It axiomatizes the partial synchrony of the network and is used to prove liveness properties. (We will consider the semantics of partially synchronous networks and GST in the next section.) In particular, the rule GST is used to show that the eventual failure detector component eventually suspects no correct node. The rule GST also derives the rule FLoss (in Fig. 12). (Rule FLoss): The rule FLoss (for fair-loss) states that links are fair in dropping messages in the sense that they do not systematically drop any particular message. If a node sends a message infinitely often and the receiver is correct, then the message is delivered to the receiver infinitely often. The rule FLoss is used to verify stubborn links that are implemented on top of basic links. (Rule FDup): The rule FDup (for finite duplication) states that basic links duplicate a message only a finite number of times. If the same message is delivered to a node infinitely often, then it is sent infinitely often. (Rule NForge): The rule NForge (for no-forge) states that links do not forge messages. If a message is delivered, it is previously sent.
(Rule UniOR): The rule UniOR (for unique output request) states that if a request is issued at most once, then it is executed at most once. If an output request e is issued at most once at the current event and it is not issued at any other event, then if e is executed at an event, it is never executed before or after that event. The rule UniOI (unique output indication) states a similar fact for indications and is elided.
(Rule Node): The rule Node states that the current node n is always in the set of executing nodes N. This rule is used to reason about the subsets of nodes such as quorums. (Rule Quorum): The derived rule Quorum states that assuming that the number of correct nodes is more than t 1 , if the size of a subset N of nodes (called a quorum) is more than t 2 and the sum of t 1 and t 2 is more than the total number of nodes, then there is at least one correct node in N . Usually t 1 and t 2 are both half the number of nodes N. Intuitively, this rule holds because the two sets are large enough to have at least one common element. Quorums are the basis of many distributed protocols and the Quorum rule presents an intuitive reasoning principle for them. We illustrate the use of the quorum rules in verification of the uniform reliable broadcast in the appendix [Appendix 2020] § 2.

DISTRIBUTED STACK SEMANTICS
In this section, we present the semantics of distributed components. It is a novel operational semantics that models the interaction of composed components in partially synchronous networks. The transitions are labeled with traces of events. Thus, the operational semantics leads to a trace semantics for composed components. TLC is proved sound with respect to this semantics in § 7. Given a stack of components, the semantics defines the transitions that nodes deploying take. It models propagation and processing of downward request and periodic events, and upward indication events across layers of components. It also models the crash-stop failure of nodes, and propagation, loss and duplication of messages. After a node crashes, it does not take any steps; a node is called correct if it does not crash.
The semantics models partially synchronous networks. In synchronous networks, a fixed upper bound on message delivery time is known. In contrast, no such bound exists for asynchronous networks and many distributed computing abstractions including consensus are impossible in this model [Fischer et al. 1985]. However, most practical networks including the Internet fall in the partially synchronous model. In these networks, either a bound holds but is not known a priori, or a bound eventually holds. Partial synchrony [Dwork et al. 1988] presented the basic round model for partially synchronous networks. Our semantics follows the basic round model. In this model, each round consists of sending, delivering and processing messages. In each round, only a subset of sent messages may be delivered; the rest are lost. However, after a round r GST called the Global Stabilization Time (GST), every message that is sent to a correct node is delivered in the same round. After this round, the network stabilizes and protocols can rely on its synchrony. In practice, the network will eventually remain stable long enough for the protocol to achieve its goal.

Fig. 13. Operational Semantics Variables
The variables used in the operational semantics are defined in Fig. 13. We denote the set of node identifiers n by N. As mentioned before, we uniquely identify each component in a stack by the (reverse) list of branch numbers in the path from the top to that component. With the reverse list, moving up and down the tree corresponds to adding and removing an index at the head of the list. We call this sequence the distinct location d ∈ of the component. The substack at location d of a stack is denoted by (d). The definition of each component declares the component state type State c . The state of a distributed component s ∈ S is a mapping from N to State c . The state of a distributed stack σ ∈ Σ is a heterogeneous map from to S types. A message is a tuple of the sender node, the receiver node, the location of the receiver component and the message payload m. We use ms ∈ ℳ to denote a multi-set of messages. The state of the transition system w ∈ (for world) is a tuple (σ ,ms, f ,r ) where σ is the state of the distributed stack, ms is the multi-set (or bag) of in-transit messages, f is the set of failed nodes and r is the round number. Given a stack , the initial state w 0 ( ) maps the state of every node and location to the state that the init function of the component at that location returns, sets the initial bag of messages ms and failed nodes f to the empty set, and sets the round to the initial round r 0 . We use e to denote user-level events such as send l (n,m). The orientation o of an event is either ↓ for request, ↑ for indication or ⇝ for periodic events. An event label ℓ is a record (n,r ,d,o,fe,σ ,σ ′ ,or ,oi) where n is the stepping node, r is the round and d is the location where the event is executed, o is the orientation of the event, fe is either fail or an executed user event e, σ and σ ′ are the stack pre-state and post-state, or is the issued request event and oi is the issued indication event. (To access the fields of a label, we use functions with the same names as fields.) An output request event or is a tuple (i,e) of the target subcomponent number i and the user event e. (We note that to present a core semantics, the request, indication and periodic handler functions of the components return one rather than a list of request and indication events. A list of events can be similarly processed in sequence. We also elide the complication that o, or and oi are option values.) A trace τ is a sequence of label events. The i-th event of a trace τ is denoted by τ (i). The trace τ i ..j denotes the sub-trace of τ from and including location i to and excluding location j, and the trace τ i .. denotes the sub-trace of τ from and including location i onward. Given a predicate p on event labels, the sub-trace τ ⋃︀ p is the projection of τ for events that satisfy p. We use the overline notation to denote multiple instances; for example, we use τ i to denote multiple traces τ i one for each index i in the context. The trace τ ⋅ τ ′ denotes the concatenation of the traces τ and τ ′ , and ⋅ τ i denotes the concatenation of the traces τ i .
Given a stack of components , Fig. 14 presents the operational semantics for . The semantics is parametric in the round r GST (Global Stabilization Time). We start with an overview. A round → comprises two parts. (1) The first part In the rules, we use _ as a placeholder for variables that are not used in the context. The two rules Reqest and Fail make top-level transitions → t . The rule Reqest uses the helper transition → r eq . The transition → r eq processes request events; it is taken by the two rules Req and Req ′ . The rule Req uses the helper transition → ind . The transition → ind processes indication events; it is taken by the two rules Ind and Ind ′ . The rule Ind, in turn, uses the helper transition → r eq . The transitions → r eq and → ind are interdependent; the rule Req that makes the transition → r eq uses the transition → ind and the rule Ind that makes the transition → ind uses the transition → r eq . The rule Periodic makes periodic transitions → p . It uses the helper transitions → msд and → per . The transition → msд that processes messages is taken by the rule Msg. The transition → per that executes the periodic functions is taken by the rules Per and Per ′ . Next, we take a closer look at each rule.
The rule Fail makes a top-level transition with a fail event for a node that has not already failed, and adds it to the set of failed nodes f . Similarly, the other rules require that the executing node has not already failed.
The rule Reqest executes a top-level request. It makes a transition → t , if a request transition → r eq can be taken with a trace starting with a top-level (request) event. The top-level request, in turn, may result in a sequence of requests and indications. The rule Req makes transitions → r eq for request events on the internal (non-leaf) components. We take a close look at the rule Req and the other rules are similar to it. The first event of the trace represents that at a node n and a component at location d, a request ↓ event e is executed that takes the pre-state of the stack σ to the post-state σ ′ , issues the request event e 1 to the i-th subcomponent and issues the indication event e 2 . Let c be the top component of the stack at location d. The state s for the component c is obtained from the stack state σ . The request function request c is called with the node identifier n, the pre-state for the node s(n) and the request event e, and results in the post-state s ′ n for n, the request event (i,e 1 ), i.e., the request e 1 for the i-th subcomponent, and the indication event e 2 . The state s of the component is updated to s ′ with the new state s ′ n for the node n, and the state of the stack σ is updated to σ ′ with the new state s ′ at location d. The issued request event (i,e 1 ) inductively results in a transition → r eq at the i-th substack whose location is i ∶∶ d. Similarly the issued indication event e 2 inductively results in a transition → ind at location d on the parent component. The trace for the whole transition is the original request event concatenated with the two subsequent transition traces for the issued request and indication events.
Basic links are used as the leaves of a stack. the rule Req ′ makes a transition for a send request on a leaf component. The rule adds tuples to the in-transit messages that contain the sender and the receiver node identifiers, the component location and the message payload. A message can be duplicated in the network. Therefore, the overline notation indicates a finite number of duplicate message. Further, we note that messages are added to an unordered multi-set of messages. Therefore, messages can be arbitrarily reordered.
The rule Ind makes a transition → ind for indication events from components except the topmost. (We note that the location of the first event in the trace label of this rule is i ∶∶ d to exclude the top.) The rule is similar to the rule Req in structure but executes an indication instead of a request event. The indication event is executed at the parent component that is at location d. The rule Ind ′ makes a transition → ind for indication events from the topmost component. In this case, there is no explicit parent component; thus, the rule simply records the issued indication in its label.
The rule Periodic delivers messages and executes periodic functions. It drops messages sent to failed nodes f (using the drop function). In addition, before the round r GST , it may drop some other messages and retain a subset of messages ms ′ . The set of remained messages are delivered by the message transition → msд , and calls to the periodic handlers are started at the top level by the period transition → per . The rule Msg that makes the transition → msд delivers all the messages in its pre-state. For every message, it issues a delivery indication event at the recipient node and component location. The trace of the transition is the concatenation of the traces of the indication transitions for all the messages. The rule Per executes the periodic function of a component at a (non-leaf) location d and recursively for every subcomponent i at location i ∶∶ d. The rule Per is similar to the rule Req in structure but in addition to calling the periodic function on the component, it propagates the periodic calls to lower-level components as well. At the leaf layers, the rule Per ′ makes trivial periodic transitions.

SOUNDNESS OF TLC
In this section, we define the semantics of assertions on execution traces and prove the soundness of TLC with respect to distributed stack semantics (that we saw in § 6). We note that TLC is independent of the distributed stack semantics and its soundness can be studied for other semantics.
We define a model m as a tuple (τ ,i,I ) of a trace τ , a position i in the trace and an interpretation I . A trace τ is the sequence of event labels of an execution. To evaluate temporal operators, the model includes a position i in the trace. The model also includes an interpretation I that maps free rigid variables, and interpreted functions and predicates to concrete values, functions and predicates. We define the set of models M( ) of a stack as the set of tuples (τ ,0,I 0 ) where τ is a trace of , 0 is the first position and I 0 is an initial interpretation that includes mappings for r,(︀⌋︀, ,fail,σ ,σ , , ) →t (σ ,ms ′ , f ∪ {n},r ) Periodic r,(︀⌋︀,↑,e,σ ,σ , , ) → ind (σ ,ms) ,σ ,σ , , ) →per (σ ,ms) commonly used integer, list and set functions and predicates. The traces of a stack is the set of traces of the executions of (for any r GST ). In Fig. 15, we define the models relation, m ⊧ , that is read as the model m models or satisfies the assertion . We also use the models relation for terms, m ⊧ t∶v, that is read as the model m evaluates the term t to the value v. We remember from the classical temporal logic [Manna and Pnueli 1992] that a rigid variable has the same value in all elements of a trace, while a flexible variable may assume distinct values in different elements. The rule VarM evaluates a rigid variable x using the interpretation I . On the other hand, separate rules evaluate the flexible variables n, r, d, o, e, s, s ′ , ois and ors based on τ (i), the event at the i-th position in the trace τ . For instance, the rule NM evaluates the flexible variable n for the current node to the first element n of τ (i). Let us take a closer look at the rule SM that evaluates the flexible variable s (pre-state). We remember from the distributed stack semantics that if an event at location d is a request or periodic event, then it is applied to the component at location d, but if it is an indication event, it is applied to the parent component at location tail(d). Therefore, if the event at location d has a downward orientation, i.e., ↓ or ⇝ then the location d is applied to the stack state σ to obtain the component state. However, if it has an upward orientation, i.e., ↑ then the location tail(d) is applied to σ . The rule SM ′ for the post-state s ′ is similar. The rule CM evaluates constants except Correct by the interpretation I . The rule CSM evaluates the constant Correct to the set of nodes in N that do not have a fail transition in the trace. As the pre-state s and post-state s ′ variables take function values, not only a function but also a variable can be applied to terms. The two applications are evaluated in FunM and FunM ′ respectively.
The rule PredM evaluates predicates using the interpretation I . The definition of the models relation for conjunction, negation and quantification is standard. The strict always operator□ requires the assertion to hold in every future position starting from the position after the current. The strict always in the past operator⊟ requires a similar condition in the past. The strict eventual operator◇ requires the assertion to hold in at least one future position starting from the position after the current. The strict eventual in the past operatorˆ requires a similar condition in the past. As we defined the non-strict temporal operators as syntactic sugar for strict ones, their semantics are derived from the above semantics. The next operator ◯ requires the assertion to hold in the position after the current. As defined at the bottom of Fig. 15, we say that an event label ℓ is on the self component mself(ℓ), if it is a request (↓) or periodic ( ⇝ ) at the top location ((︀⌋︀) or is an indication (↑) at the second level (at location (︀i⌋︀ for some i). The self operator Ⓢ requires the assertion to hold on the self subtrace, i.e., the projection of the trace over mself. More precisely, the self operator requires the assertion to hold on the first self position after the current position.
We are now ready to state the soundness of TLC. An assertion is valid for a stack , written as ⊧ , if and only if every model of satisfies .
Definition 4 (Valid Assertion). For all and , ⊧ iff for all m ∈ M( ), m ⊧ . We say that a set of assertions Γ entail an assertion if and only if every model m of that models Γ also models .
The following theorem states the soundness of TLC. If assuming assertions Γ, TLC derives an assertion then Γ entails .
Theorem 2 (Soundness). For all Γ, , c, ′ , , such that = stack(c, ′ ), if Γ ⊢ c , then Γ ⊧ . The detailed proofs are available in the appendix [Appendix 2020] § 5.1. The following corollary is immediately derived. It states that if assuming valid assertions, TLC derives an assertion then that assertion is valid as well. In other words, TLC derives only valid assertions from valid assertions.

MECHANIZATION
The ultimate goal of this project is mechanized distributed middleware. This goal is a huge undertaking and fully achieving it may take multiple years. The main topic of this paper is TLC, its compositionality and applicability. We have finished all the proofs of the components in the appendix to ensure that TLC is comprehensive. Nonetheless, we have been mechanizing the proofs in Coq. The TLC Coq framework provides a deep embedding of an enriched lambda calculus for defining functional components, an evaluation engine for embedded terms, an inductive definition of TLC, and a set of tactics for constructing TLC proof terms. We have used this library to successfully mechanize the verification of the stubborn link and the perfect link components and we are extending mechanization to the other components. Embedding Approaches. We tried different approaches for encoding TLC in Coq. The earliest attempts were shallow embeddings of TLC. The intent was to utilize Coq's Gallina functional programming language to capture component definitions and its Ltac proof language to construct proof terms. These approaches proved unsuccessful due to the syntactic nature of proofs in TLC.
The syntactic rules of TLC require recursive analysis of the syntax of terms, which cannot be done directly on Gallina terms. We define a deep embedding of a minimal functional programming language to program component terms. This embedding is an untyped lambda calculus enriched with pattern matching terms, externally defined functions, value literals, value constructors, and locally nameless parameters. Similarly, we define a deep embedding of the syntax of TLC as well.
Embedding. The syntax of terms is defined as the inductive type presented in Fig. 16.(a). The TParameter, TAbstraction, and TApplication terms come directly from untyped lambda calculus. We adopted the locally nameless representation [Charguéraud 2012] to separately define parameters and variables. We chose this encoding instead of implementing capture-avoiding substitution of arbitrarily named variables. Coq requires all recursive functions to be structurally decreasing. Algorithms for capture-avoiding substitution are not strictly decreasing and are rejected by Coq. Bound variables, represented by the TParameter constructor, are referenced using deBruijn indices. Free variables, represented by the TVariable constructor, are named strings.
The TConstructor term represents a constructor of an inductive type. The TLiteral term represents a literal value of a Coq type, such as the natural numbers. The TFunction term represents a function that is not defined explicitly in the term language, such as recursively defined functions. These terms are lifted into Coq, evaluated, and the result is lowered into the embedded term type. The TMatch constructor represents a pattern matching expression. The TFailure term is the empty term, produced when an ill-formed term is evaluated.
To simplify the definition of terms, we have defined a library of Coq notations for the term language. The library allows for the relatively direct translation of the implementation of the components into embedded terms. Similarly, Coq notations are provided for the assertion language and the sequent judgements. These notations allow writing judgements in the commonly used form. The context of a sequent is the set of variable names that are universally quantified along with the list of assumed assertions. As an example, Fig. 16.(b) shows the statement of the stubborn delivery property: if a message is sent, it is infinitely often delivered. The context declares the list of free variable n, n' and m and no assumed assertions [::]. The conclusion is read as follows: if two nodes n and n' are correct and n at the top level [] sends a request event -> to send the message m to n', then infinitely often at n', at the top level [], the indication event <-that delivers the message m from n is executed.
Logic. The basic rules and axioms of TLC are encoded as an inductive type. Fig. 16.(c) shows three constructors that are representative of the encoding of the rules and axioms of TLC. The rules are extended with rules specific to the implementation of the extended term language. The first constructor, DAEvaluateP, states that if the terms within the first premise can be simplified then proving the conclusion assuming the premise can be reduced to proving the conclusion assuming the simplified premise. The [[A Ap]] notation represents assertion evaluation, which replaces all computational terms within an assertion with the terms produced by their evaluation. Terms are evaluated recursively inside of a monad, which produces a failure case when a failure term is evaluated. The second constructor, DSCut, is a sequent logic rule that can be used to introduce an assertion as a premise. The third constructor, DPIR, is an axiom of the TLC program logic, the rule IR that we saw in § 5.
The framework provides tactics to facilitate applying TLC. For example, it provides a set of tactics that mirror a subset of Coq's Ltac tactics for producing Gallina proof terms, as well as a library of lemmas. These tactics allow proofs to be written in a more natural, Coq-like style. These are tactics such as d_left (d refers to the derives relation), d_right, d_splitp (p for premise), and d_splitc (c for conclusion), which mirror the primitive Coq tactics left, right, destruct (on conjunctive hypotheses), and split. In addition to these basic tactics, there are tactics that automate some multi-step common tasks. For example, the d_evalc imitates the Coq simpl tactic, functional implementation of protocols that can be directly executed. Further, in contrast to TLA, TLC defines an operational semantics to support the soundness of the logic.
I/O Automata [Lynch and Tuttle 1989] models specifications and protocols as transition systems and provides simulation proof techniques [Lynch and W. Vaandrager 1995] between automata. In contrast, TLC captures component implementations as functional programs and specifications as descriptive temporal assertions, and provides a program logic and a compositional proof technique to derive the specification for the implementation.
Both I/O Automata [Lynch and Tuttle 1989] and Reactive Modules [Alur and Henzinger 1999] model protocols as transition systems. They capture specifications in the semantic domain as either transitions systems or properties of execution traces. In contrast, TLC captures component implementations as functional programs and specifications as temporal assertions. I/O Automata provides simulation proof techniques [Lynch and W. Vaandrager 1995] between automata. The simulation proofs are written in the semantic domain. In contrast, TLC provides a program logic to derive the specification for the implementation. Both I/O Automata and and Reactive Modules support composition of interacting modules with matching input and outputs. They support assume-guarantee reasoning where each module can be verified based on the specification of the other module. TLC models distributed systems as structured stacks of components where each component composes with its subcomponents below and its parent component above. Similar to the assume-guarantee reasoning, it supports compositional verification of each component based on the specification of its subcomponents. However, no assumptions for the parent component is needed. The specification of each component is for the most general parent. A verified component can serve as the subcomponent of any parent component.
EventML [Rahli 2012] is a functional domain-specific language for distributed protocols. Protocols written in EventML can be translated to Nuprl [Constable et al. 1986] and then interactively verified. It has been used to verify monolithic replicated services [Rahli et al. 2018;Schiper et al. 2014]; however, it does not address compositional verification.
IronFleet [Hawblitzel et al. 2015] models a distributed system as a hierarchy of state transition systems at multiple levels of abstraction from the high-level specification to the low-level implementation. It proves a refinement [He et al. 1986;Lynch and W. Vaandrager 1995] between a layer and the layer immediately above it. However, it only considers monolithic protocols without subcomponents and the verification is carried out using refinement in contrast to a program logic.
Similarly, network refinement [Koh et al. 2019] presents specifications for a swap server that can be both tested and verified using observational refinement. The server is well-integrated with several other verified systems. To contrast, TLC is a temporal logic and can verify liveness in addition to safety properties. Further, TLC focuses on composition of distributed protocols and builds component stacks on basic links that are much weaker than TCP.
Verdi [Wilcox et al. 2015;Woos et al. 2016] models several network semantics and provides transformations from correct protocols in one semantics to another. It has been applied to verification of state machine replication. Similar to TLC, Verdi provides a form of vertical composition. However, its proofs are based on simulation [He et al. 1986;Lynch and W. Vaandrager 1995] in the semantic domain rather than a program logic.
Chapar [Lesani et al. 2016] presents an operational semantics and a proof technique for verification of causally consistent distributed stores. Similar to TLC, Chapar considers the interface between clients and store implementations; however, only for causal consistency. Further, verification is based on simulation rather than program logic.
PSync [Dragoi et al. 2016] is a DSL for distributed protocols based on the heard-of round-based model [Charron-Bost and Schiper 2009]. This lockstep model enables proof automation that has been successfully applied to verification of consensus variants. However, PSync left composition as future work.
Ivy [Padon et al. 2016] is an interactive tool that assists in finding inductive invariants. It has been applied to verification of a few distributed protocols. A follow-up work [Taube et al. 2018] lets the user split a protocol into logical modules with explicit invariants. Modules facilitate an assume-guarantee reasoning such that verification of each falls in a separate decidable theory. While the main focus of Ivy is automatic verification of separate parts of monolithic protocols, TLC's focus is compositional verification of stacks of protocols. Further, in contrast to Ivy, TLC supports verification of liveness properties.
Disel ] is a program logic for distributed protocols that provides Floyd-Hoare-style specification [Floyd 1967;Hoare 1969;Reynolds 2002] and proof rules for horizontal composition. In Disel, the specification of a component is written in terms of its state and the message pool. On the other hand, in TLC, the temporal specification is written in terms of the interface events almost verbatim from the natural language description. Disel and Hoare-style reasoning require definition of stable invariants and sometimes ghost variables. However, TLC does not require additional annotations on the components. Disel can state and prove safety properties while TLC can state and prove both safety and liveness properties. A follow-up work [García-Pérez et al. 2018] similarly applies the rely-guarantee reasoning to verification of a decomposition of Paxos [Boichat et al. 2003]. However, it does not consider the leader election subcomponent. This paper considers leader election and epoch change as well.
Also related is recent work by Merten et al. [Merten et al. 2018] on Cage, a system for verifying the complexity and optimality of distributed systems in domains like routing and load balancing. Rather than verifying such systems using a program logic, as in TLC, Cage builds protocols and associated implementations that are correct by construction by recasting distributed systems as games with close-to-optimal equilibria, which it then executed using a distributed implementation of no-regret dynamics.

CONCLUSION
TLC is a temporal program logic for compositional verification of stacks of distributed components. Its assertion language can capture both safety and liveness properties. Using a transformation function that lowers the specification of components to be used as subcomponents, TLC supports compositional verification of components based on only the specification of their subcomponents. It features intuitive inference rules and induction principles that can deduce assertions about a component based on its functional implementation. TLC and the lowering transformation are proved sound with respect to the operational semantics of distributed stacks in partially synchronous networks. TLC has been successfully applied to verify a stack of fundamental distributed components as the first steps towards certified distributed system stacks.
We hope that the design of TLC motivates further exploration for compositional verification methods in the rich space beyond the traditional structure of the Floyd-Hoare logic. In particular, concurrent and distributed programs logics that directly support reasoning about the execution order of events seem to capture intuitive proofs.