Safely Sliding Windows

Dirk Henkel RVS Group Research Report RVS-RR-97-05a Universität Bielefeld

5 May, 1997 last changed 19 November, 1997

Abstract

A formal TLA proof is given that the sliding window message retransmission mechanism with linear arithmetic implements the safety property of a reliable, lossless, asynchronous FIFO queue. In order to make the verification as routine as possible, the proof is divided into four parts with three additional specifications intermediate between the requirements specification and the sliding window specification.

Introduction

This paper provides the safety part of a verification proof for a sliding-window-style message retransmission mechanism^{1} with linear arithmetic (SWLA). SWLA is the linear arithmetic version of the sliding window message retransmission mechanism with modular arithmetic (SWMA), which is part of the Radio Link Protocol (RLP1), the datalink layer protocol for TDMA mobile cellular radio being analysed by the FCAR project of the Telecommunications Software Group at INRS-Télécommunications in Montréal [Fer96]. The specifications and proofs in this paper contribute to the verification of SWLA using TLA and TLA^{+}.

Documents on the Temporal Logic of Actions (TLA) calculus and the corresponding specification language TLA^{+} can be found at the TLA website of Leslie Lamport [Lam]. A tutorial on TLA verification has been written by Peter Ladkin [Lad97].

TLA provides a clear separation between safety and liveness properties. The following specifications and proofs concern only safety properties. To obtain complete specifications we must add liveness properties, and to obtain a complete verification of SWLA, we ought to prove its liveness properties, too. Liveness properties in TLA specifications have the form of Boolean combinations of fairness properties. The specifications have been designed, so to speak, with these liveness properties in mind, so we don’t believe that adding them will change the general idea of how the five specified systems work. The only sure way to know, however, would be to add them and provide the relevant proofs.

System verification must be performed relative to stated requirements. For SWLA (as well as for RLP1) we require that the protocol implements a reliable, asynchronous first-in first-out message-transfer stream. We specify this by means of a variable buffer which contains the messages that have been sent but not received, in order. Reliability is ensured by the implicit criterion that sent messages do not disappear; asynchrony by the independence of send and receive actions (corresponding to the buffer’s push and pop actions); FIFO by the standard FIFO property of a buffer. The AbstractBuffer (AB) is thus a state machine which embodies exactly the requirements of the communication system. The AB specification in TLA was first formulated and used in [Lad96].

1It has been pointed out by Michael Ferguson that the meaning of the word “protocol” in telecommunications engeneering is far richer than its informal use by specification engineers and network textbook writers. We find the mathematical operation far better described as a “retransmission mechanism”, as Ferguson suggests.

For both SWLA and AB we give formal specifications of their safety properties: the TLA formulas I .Safety and V .Safety. Proving that SWLA-safety implies AB-safety is equivalent to proving that I .Safety logically implies V .Safety. One may try this directly, but it’s easier to do it in several small steps via a hierarchy of specifications. We use three intermediate specifications II .Safety, III .Safety and IV .Safety, which show a continuous development from the simplicity of I .Safety to the details of V .Safety. The whole safety proof is accomplished in four steps of the form “(N + 1).Safety implies N .Safety”. A summary of the five TLA^{+} specifications without the proofs is given in [GHL97].

The approach to the system verification differs from that of Mokkedem, Ferguson and Johnston [MFJ97]. They describe invariants, and prove using the TLA logic that these invariants logically follow from an implementation specified in TLA. We follow the “traditional” TLA format, in which all specifications, including the requirement, have the form of a state machine. In this example, the requirement state machine embodies, as we have argued, exactly the properties of a reliable, asynchronous FIFO channel. It is notable that the required invariant in [MFJ97] does not appear to be logically equivalent to a TLA specification as defined by Lamport [Lam94], thus it is not guaranteed that the TLA logic suffices to prove it (but Mokkedem, Ferguson and Johnston have indeed succeeded in proving it).

The five safety specifications are given in six TLA^{+} modules. The first one is a collection of some common definitions. It is extend’d by each of the five specification modules I to V . Module I , the “requirement”, specifies the safety properties of AB, which is just a sequence with fixed maximum length and the two actions Push and Pop. As we said above, the purpose of any reliable, asynchronous FIFO message-transmission mechanism must be to simulate this precisely. Module II is a translation of AB into set notation. Module III introduces a distinction between sender and receiver sides. In Module IV the message transfer from sender to receiver is split into two seperate actions. Module V specifies the safety properties of SWLA. Besides Push and Pop, it defines four actions that make up the message transfer. Each module is preceeded by some commentary that should give an idea of how the specified system works.

Section 1 introduces the common definitions module. In section 2 the AB-safety requirement is specified by module I . Each of the sections 3 to 6 contains another specification module, a TLA^{+} module stating that this specification implies the previous one, and the corresponding TLA proof.

Acknowledgements

The specifications were developed jointly with Thorsten Gerdsmeier, Prof. Dr. Jean-Charles Grégoire of INRS-Télécommunications à l’Université de Québec in Montréal and Prof. Dr. Peter Ladkin. Petra Korff also contributed to the analysis and verification of some of the former high-level specifications with which we worked. Some of the explanatory commentary to the specifications is based on notes by Prof. Dr. Grégoire.

References

[Fer] Michael J. Ferguson: Selected publications. Available through

http://www.inrs-telecom.uquebec.ca/users/telesoft/

[Fer96] Michael J. Ferguson: Formalization and validation of the Radio Link Protocol (RLP1). To be published in Computer Networks and ISDN Systems, 1996. Available through [Fer].

[GHL97] Thorsten Gerdsmeier, Dirk Henkel, Peter B. Ladkin: Safely sliding windows: the specs. Technical Report RVS-RR-97-05b, RVS Group, Universität Bielefeld, Technische Fakultät, July 1997. Available through [Lad].

[Lad] Peter B. Ladkin: Abstracts of RVS research publications.

Available through http://www.rvs.uni-bielefeld.de

[Lad96] Peter B. Ladkin: Formal but lively buffers in TLA^{+}. Technical Report RVS-RR-96-07, RVS Group, Universität Bielefeld, Technische Fakultät, January 1996. Available through [Lad].

[Lad97] Peter B. Ladkin: Using the Temporal Logic of Actions: A tutorial on TLA verification. Technical Report RVS-RR-97-08, RVS Group, Universität Bielefeld, Technische Fakultät, June 1997. Available through [Lad].

[Lam] Leslie Lamport: TLA – The Temporal Logic of Actions.

http://www.research.digital.com/SRC/tla/

[Lam94] Leslie Lamport: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994. Also available through [Lam].

[MFJ97] Abdelillah Mokkedem, Michael J. Ferguson, and Robert deB. Johnston: A TLA solution to the specification and verification of the RLP1 retransmission protocol. Formal Methods Europe symposium, September 1997. Available through [Fer].

[Gre97] Jean-Charles Gregoire: TLA + PROMELA: conjecture, check, proof – engineering new protocols using methods and formal notations. Formal Methods Europe symposium, September 1997.

1 Common Definitions

Some declarations, assumptions and definitions will be needed in several of the following specifications. They are collected in the module CommonDefinitions.

Messages is the Set of all Objects that can be passed through the buffer we specify. It specifically does not contain the constant ⊥_{Messages}. BufferLength is the maximum number of such objects that can be held in the buffer at any time. We require Bufferlength ≥ 1.

We introduce a simple notation for intervals of natural numbers and some operators on sequences: Len(s) denotes the length of a sequence s; Tail(s) is ”s without its first element”; s ∘ t the concatenation of the sequences s and t.

The last four definitions refer to sets of pairs of the form (index, message) where index is a natural number. MinPair(S) is that pair (or one of those pairs) with the least index in S, MinIndex(S) is this least index. Similarly for Max-functions with the greatest index. These functions are defined only on nonempty sets.

module CommonDefinitions

extends Naturals

constants BufferLength, Messages, ⊥_{Messages} assumption BufferLength > 0 assumption ⊥_{Messages} ∉ Messages

l . . u =^{Δ} {i ∈ Nat : l ≤ i ∧ i ≤ u} Len(s) =^{Δ} choose n : ∧ n ∈ Nat ∧ Domain s = 1 . . n

Tail(s) =^{Δ} [i ∈ 1 . . (Len(s) − 1) ↦ s[i + 1]] s ∘ t =^{Δ} [i ∈ 1 . . (Len(s) + Len(t)) ↦ if i ≤ Len(s) then s[i] else t[i − Len(s)]]

MinPair(S) =^{Δ} choose z : \begin{matrix}∧ z ∈ S \\ ∧ ∀ y ∈ S : z[1] ≤ y[1] \end{matrix}

MaxPair(S) =^{Δ} choose z : \begin{matrix}∧ z ∈ S \\ ∧ ∀ y ∈ S : z[1] ≥ y[1] \end{matrix}

MinIndex(S) =^{Δ} MinPair(S)[1] MaxIndex(S) =^{Δ} MaxPair(S)[1]

2 An Abstract Buffer

Module I contains a straight-forward specification of an abstract buffer. Its only variable is the sequence buffer. At the beginning, buffer is empty. If the buffer is at any time not full (i.e. shorter than BufferLength), a message can be Push’d onto it at the rear end. If the buffer is not empty, its first message can be Pop’d off. Thus the messages are Pop’d in FIFO order.

module I

extends CommonDefinitions

variables buffer

Init =^{Δ} buffer = ⟨ ⟩

Push(a) =^{Δ} ∧ a ∈ Messages ∧ Len(buffer) < BufferLength ∧ buffer′ = buffer ∘ ⟨a ⟩

Pop =^{Δ} ∧ buffer ≠ ⟨ ⟩ ∧ buffer′ = Tail(buffer)

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{buffer}

3 Set Notation

Specification II is a translation of the buffer into set notation. Instead of the sequence buffer we now use the set tSet. Like buffer in specification I , tSet starts empty.

To preserve the FIFO property of the buffer, we must know in which order the messages in the buffer have been Push’d. Thus Push(a) does not simply add the message a to tSet but a pair (index, a) where index is the current number of the Push action. Accordingly, Pop takes the elements out of tSet in ascending order of index.

The current indices for the Push and Pop actions are stored in the counter variables index_{s} and index_{r}. Both start at 0; every Push increments index_{s}; every Pop increments index_{r}. Thus index_{s} is the index of the next element to be Push’d and index_{r} is the index of the next element to be Pop’d.

The difference between index_{s} and index_{r} equals the size of tSet, thus it can be used to specify that the buffer must not be full at the beginning of a Push.

module II

extends CommonDefinitions

variables tSet, index_{r}, index_{s}

Vars =^{Δ} ⟨tSet, index_{s}, index_{r} ⟩ Init =^{Δ} ∧ tSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

Push(a) =^{Δ} ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r}

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s}

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

II.Safety implies I.Safety

module II implies I

extends II

HLS =^{Δ} instance I with buffer ← [\begin{matrix}i ∈ 1 . . (index_{s} − index_{r}) \\ ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet] \end{matrix}

f ⊔ g =^{Δ} [x ∈ (Domain f ∪ Domain g) ↦ choose y : y = f [x] ∨ y = g[x]]

theorem Safety ⇒ HLS.Safety

⟨0⟩1. Safety ⇒ HLS.Safety

Proof: ⟨1⟩1. Init ⇒ HLS.Init

Proof:

⟨2⟩1. ∧ tSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

⇒ buffer = ⟨ ⟩

Proof: From index_{s} = 0, index_{r} = 0 and the definition of buffer follows buffer= [i ∈ 1 . . 0 ↦ choose x : ⟨i − 1, x ⟩ ∈ tSet] = [i ∈ ∅ ↦ choose x : ⟨i − 1, x ⟩ ∈ tSet] = ⟨ ⟩.

⟨2⟩2. Q.E.D.

Proof: Direct from the definitions of Init and HLS.Init.

⟨1⟩2. ∧ Init

∧ □[SomeAction]_{Vars}

⇒ □[HLS.SomeAction]_{buffer}

Proof: We use the following invariant: Let: Inv =^{Δ} 1.∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s} 2.∧ |tSet| = index_{s} − index_{r} 3.∧ ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1

We use Inv.1 and Inv.3 to prove that Push simulates HLS.Push. We use Inv.1, Inv.2 and Inv.3 to prove that Pop simulates HLS.Pop. We use Inv.1 to prove the invariance of Inv.2 and Inv.3 under Push.

⟨2⟩1. ∧ Init

∧ □[SomeAction]_{Vars}
⇒ □Inv

Proof: ⟨3⟩1. Init ⇒ Inv

Proof: From index_{s} = 0 and index_{r} = 0 follows index_{s} − index_{r} = 0. Inv.1 follows from tSet = ∅. Inv.2 follows from tSet = ∅ and index_{s} − index_{r} = 0. Inv.3 follows from index_{s} − index_{r} = 0.

⟨3⟩2. ∧ Inv

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof:

⟨4⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ Inv′

Proof:

⟨5⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ unchanged Vars

⇒ Inv′

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : Push(a) ⇒ Inv′

Proof: Let: a : constant

⟨7⟩1. ∧ Inv ; ∧ Push(a)

⇒ Inv′

Proof:

⟨8⟩1. ∧ Inv

∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r} ⇒ Inv′

Proof: ⟨9⟩1.

∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1

⇒ ∨ tSet′ = ∅ ∨ MaxIndex(tSet′) < index′_{s}

Proof: From tSet = ∅ ∨ MaxIndex(tSet) < index_{s} and tSet′ = tSet ∪ {⟨index_{s}, a ⟩} follows MaxIndex(tSet′) = index_{s}. From this and index′_{s} = index_{s} + 1 follows MaxIndex(tSet′) < index′_{s}.

⟨9⟩2.

∧ |tSet| = index_{s} − index_{r}

∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩}

∧ index′_{s} = index_{s} + 1

∧ unchanged index_{r}

⇒ |tSet′| = index′_{s} − index′_{r}

Proof: From tSet = ∅ ∨ MaxIndex(tSet) < index_{s} follows ⟨index_{s}, a ⟩ ∉ tSet. From this and tSet′ = tSet ∪ {⟨index_{s}, a ⟩} follows |tSet′| = |tSet| + 1. From index′_{s} = index_{s} + 1 and unchanged index_{r} follows index′_{s} − index′_{r} = index_{s} − index_{r} + 1. Now we obtain the following equality: |tSet′|\begin{matrix}= |tSet| + 1 \\ = index_{s} − index_{r} + 1 \\ = index′_{s} − index′_{r}. \end{matrix}

⟨9⟩3.

∧ ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 ∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩}

∧ index′_{s} = index_{s} + 1

∧ unchanged index_{r}

⇒ ∀ i ∈ 1 . . (index′_{s} − index′_{r}) : |{p ∈ tSet′ : p[1] = i + index′_{r} − 1}| = 1

Proof: From tSet = ∅ ∨ MaxIndex(tSet) < index_{s} follows |{p ∈ tSet : p[1] = index_{s}}| = 0. From this and tSet′ = tSet ∪ {⟨index_{s}, a ⟩} follows |{p ∈ tSet′ : p[1] = index_{s}}| = 1. From this and index′_{s} = index_{s} + 1 follows |{p ∈ tSet′ : p[1] = index′_{s} − 1}| = 1. For all i ∈ 1 . . (index_{s} − index_{r}) holds i + index_{r} − 1 < index_{s}. From this, tSet′ = tSet ∪ {⟨index_{s}, a ⟩} and ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 follows ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet′ : p[1] = i + index_{r} − 1}| = 1. From this, index′_{s} = index_{s} + 1 and unchanged index_{r} follows ∀ i ∈ 1 . . (index′_{s} − index′_{r} − 1) : |{p ∈ tSet′ : p[1] = i + index′_{r} − 1}| = 1. From this and |{p ∈ tSet′ : p[1] = index′_{s} − 1}| = 1 follows ∀ i ∈ 1 . . (index′_{s} − index′_{r}) : |{p ∈ tSet′ : p[1] = i + index′_{r} − 1}| = 1.

⟨9⟩4. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2 and ⟨9⟩3.

⟨8⟩2. Q.E.D. Proof: Direct from the definition of Push(a).

⟨7⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨6⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ Inv′

Proof: Let: a : constant

⟨8⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ Inv′

Proof: ⟨9⟩1.

∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ unchanged index_{s} ⇒ ∨ tSet′ = ∅ ∨ MaxIndex(tSet′) < index′_{s}

Proof: From tSet = ∅ ∨ MaxIndex(tSet) < index_{s} and ⟨index_{r}, a ⟩ ∈ tSet follows MaxIndex(tSet) < index_{s}. From tSet′ = tSet \{⟨index_{r}, a ⟩} follows tSet′ ⊂ tSet. From this and MaxIndex(tSet) < index_{s} follows tSet′ = ∅ ∨ MaxIndex(tSet′) < index_{s}. From this and unchanged index_{s} follows tSet′ = ∅ ∨ MaxIndex(tSet′) < index′_{s}.

⟨9⟩2.

∧ |tSet| = index_{s} − index_{r} ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ |tSet′| = index′_{s} − index′_{r}

Proof: From ⟨index_{r}, a ⟩ ∈ tSet and tSet′ = tSet \{⟨index_{r}, a ⟩} follows |tSet′| = |tSet| − 1. From index′_{r} = index_{r} + 1 and unchanged index_{s} follows index′_{s} − index′_{r} = index_{s} − index_{r} − 1. Now we obtain the following equality:

|tSet′|\begin{matrix}= |tSet| − 1 \\ = index_{s} − index_{r} − 1 \\ = index′_{s} − index′_{r}. \end{matrix}

⟨9⟩3.

∧ ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ ∀ i ∈ 1 . . (index′_{s} − index′_{r}) : |{p ∈ tSet′ : p[1] = i + index′_{r} − 1}| = 1

Proof: From ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 follows ∀ i ∈ 2 . . (index_{s} −index_{r}) : |{p ∈ tSet : p[1] = i +index_{r} −1}| = 1, and this is equivalent to ∀ i ∈ 1 . . (index_{s} − index_{r}) − 1 : |{p ∈ tSet : p[1] = i + index_{r}}| = 1. From this, index′_{r} = index_{r} + 1 and unchanged index_{s} follows ∀ i ∈ 1 . . (index′_{s} − index′_{r}) : |{p ∈ tSet : p[1] = i + index′_{r} − 1}| = 1. From this and tSet′ = tSet \{⟨index_{r}, a ⟩} follows ∀ i ∈ 1 . . (index′_{s} − index′_{r}) : |{p ∈ tSet′ : p[1] = i + index′_{r} − 1}| = 1.

⟨9⟩4. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2 and ⟨9⟩3.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D.

Proof: Direct from the definition of Pop.

⟨6⟩3. ∧ Inv

∧ unchanged Vars ⇒ Inv′

Proof: Direct from the definitions of Vars and Inv.

⟨6⟩4. Q.E.D.

Proof: Propositional logic from ⟨6⟩1, ⟨6⟩2 and ⟨6⟩3.

⟨5⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨4⟩2. Q.E.D.

Proof: Direct from ⟨4⟩1 using rule INV1.

⟨3⟩3. Q.E.D. Proof: Propositional logic from ⟨3⟩1 and ⟨3⟩2.

⟨2⟩2. ∧ □Inv

∧ □[SomeAction]_{Vars} ⇒ □[HLS.SomeAction]_{buffer}

Proof:

⟨3⟩1. ∧ Inv

∧ [SomeAction]_{Vars}

⇒ [HLS.SomeAction]_{buffer}

Proof:

⟨4⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ unchanged Vars

⇒ ∨ ∃ a : HLS.Push(a) ∨ HLS.Pop ∨ unchanged buffer

Proof: ⟨5⟩1. ∧ Inv ∧ ∃ a : Push(a) ⇒ ∃ a : HLS.Push(a)

Proof: Let: a : constant

⟨6⟩1. ∧ Inv ; ∧ Push(a) ⇒ HLS.Push(a)

Proof:

⟨7⟩1. ∧ Inv

∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r} ⇒ ∧ a ∈ Messages ∧ Len(buffer) < BufferLength ∧ buffer′ = buffer ∘ ⟨a ⟩

Proof: ⟨8⟩1. a ∈ Messages ⇒ a ∈ Messages

Proof: Trivial.

⟨8⟩2. index_{s} − index_{r} < BufferLength ⇒ Len(buffer) < BufferLength

Proof: From the definition of buffer follows Len(buffer) = index_{s} − index_{r}. From this and index_{s} − index_{r} < BufferLength follows Len(buffer) < BufferLength.

⟨8⟩3.

∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 ∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r} ⇒ buffer′ = buffer ∘ ⟨a ⟩

Proof: For all i ∈ 1 . . (index_{s} − index_{r}) holds i + index_{r} − 1 < index_{s}. From this and ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 follows [i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}] = [i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet]. From tSet = ∅ ∨ MaxIndex(tSet) < index_{s} follows choose x : ⟨index_{s}, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩} = a. From the definition of buffer follows Len(buffer) = index_{s} − index_{r} and thus buffer ⊔ [index_{s} − index_{r} + 1 ↦ a] = buffer ∘ ⟨a ⟩. Now we obtain the following equality chain: buffer′ = [i ∈ 1 . . (index′_{s} − index′_{r}) ↦ choose x : ⟨i + index′_{r} − 1, x ⟩ ∈ tSet′] = [i ∈ 1 . . (index_{s} +1−index_{r}) ↦ choose x : ⟨i +index_{r} −1, x ⟩ ∈ tSet ∪{⟨index_{s}, a ⟩}] = [i ∈ 1 . . (index_{s} − index_{r}) ∪ {index_{s} − index_{r} + 1} ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}]

= [i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}] ⊔[index_{s} − index_{r} + 1 ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}]

= [i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}] ⊔[index_{s} − index_{r} + 1 ↦ choose x : ⟨index_{s}, x ⟩ ∈ tSet ∪ {⟨index_{s}, a ⟩}]

= [i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet] ⊔[index_{s} − index_{r} + 1 ↦ a]

= buffer ⊔ [index_{s} − index_{r} + 1 ↦ a] = buffer ∘ ⟨a ⟩.

⟨8⟩4. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2 and ⟨8⟩3.

⟨7⟩2. Q.E.D.

Proof: Direct from the definitions of Push(a) and HLS.Push(a).

⟨6⟩2. Q.E.D. Proof: Predicate logic: exist-intro and forall-intro.

⟨5⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ HLS.Pop

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ ∧ buffer ≠ ⟨ ⟩ ∧ buffer′ = Tail(buffer)

Proof: Let: a : constant

⟨7⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ ∧ buffer ≠ ⟨ ⟩ ∧ buffer′ = Tail(buffer)

Proof: ⟨8⟩1.

∧ |tSet| = index_{s} − index_{r}

∧ ⟨index_{r}, a ⟩ ∈ tSet

⇒ buffer ≠ ⟨ ⟩

Proof: From |tSet| = index_{s} − index_{r} and the definition of buffer follows Len(buffer) = |tSet|. From this and ⟨index_{r}, a ⟩ ∈ tSet follows buffer ≠ ⟨ ⟩.

⟨8⟩2.

∧ ∨ tSet = ∅ ∨ MaxIndex(tSet) < index_{s}

∧ |tSet| = index_{s} − index_{r}

∧ ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ buffer′ = Tail(buffer)

Proof: For all i ∈ 2 . . (index_{s} − index_{r}) holds i + index_{r} − 1 > index_{r}. From this and ∀ i ∈ 1 . . (index_{s} − index_{r}) : |{p ∈ tSet : p[1] = i + index_{r} − 1}| = 1 follows [i ∈ 2 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet \{⟨index_{r}, a ⟩}] = [i ∈ 2 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet]. Now we obtain the following equality chain: buffer′ = [i ∈ 1 . . (index′_{s} − index′_{r}) ↦ choose x : ⟨i + index′_{r} − 1, x ⟩ ∈ tSet′] = [i ∈ 1 . . (index_{s} − index_{r}) − 1 ↦ choose x : ⟨i + index_{r}, x ⟩ ∈ tSet \{⟨index_{r}, a ⟩}] = Tail([1 ↦ choose x : ⟨index_{r}, x ⟩ ∈ tSet]⊔ [i ∈ 2 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet \{⟨index_{r}, a ⟩}])

= Tail([1 ↦ choose x : ⟨1 + index_{r} − 1, x ⟩ ∈ tSet]⊔ [i ∈ 2 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet])

= Tail([i ∈ 1 . . (index_{s} − index_{r}) ↦ choose x : ⟨i + index_{r} − 1, x ⟩ ∈ tSet]) = Tail(buffer).

⟨8⟩3. Q.E.D.

Proof: Propositional logic from ⟨8⟩1 and ⟨8⟩2.

⟨7⟩2. Q.E.D.

Proof: Predicate logic: exist-intro and forall-intro.

⟨6⟩2. Q.E.D. Proof: Direct from the definitions of Pop and HLS.Pop.

⟨5⟩3. unchanged Vars ⇒ unchanged buffer

Proof: Direct from the definitions of Vars and buffer. ⟨5⟩4. Q.E.D.

Proof: Propositional logic from ⟨5⟩1, ⟨5⟩2 and ⟨5⟩3. ⟨4⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions. ⟨3⟩2. Q.E.D.

Proof: Proof by STL5 and STL4. ⟨2⟩3. Q.E.D.

Proof: Direct from ⟨2⟩1 and ⟨2⟩2 using propositional logic. ⟨1⟩3. Q.E.D.

Proof: Direct from ⟨1⟩1 and ⟨1⟩2 using propositional logic.

4 Sender and Receiver

In this module, we split tSet into two different variables, rSet and sSet. We are slowly evolving towards a specification with distinct sender and receiver sides. At this stage though, we keep index_{r} and index_{s} as global variables. In particular, the sender action Push uses the information in the receiver variable index_{r}.

The buffer is now the (disjoint) union of rSet and sSet. Its actual size still equals the difference between index_{s} and index_{r}.

The only changes to Push and Pop are that we now Push to sSet but Pop from rSet. A new action Transfer is added to the model, to represent the transfer of information from rSet to sSet. This action picks non-deterministically a pair from sSet and moves it to rSet. Indexing and index_{r} become critical as pairs are Transfer’d in non-deterministic order, but must be Pop’d in FIFO order.

module III

extends CommonDefinitions

variables sSet, rSet, index_{s}, index_{r}

Vars =^{Δ} ⟨sSet, rSet, index_{s}, index_{r} ⟩ Init =^{Δ} ∧ index_{r} = 0 ; ∧ index_{s} = 0 ; ∧ sSet = ∅ ; ∧ rSet = ∅

Push(a) =^{Δ} ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Transfer =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨index_{s}, index_{r} ⟩

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ Transfer

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

III.Safety implies II.Safety

module III implies II

extends III

HLS =^{Δ} instance II with tSet ← sSet ∪ rSet index_{s} ← index_{s} index_{r} ← index_{r}

theorem Safety ⇒ HLS.Safety

⟨0⟩2. Safety ⇒ HLS.Safety

Proof: ⟨1⟩1. Init ⇒ HLS.Init

Proof:

⟨2⟩1. ∧ sSet = ∅ ; ∧ rSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

⇒ ∧ sSet ∪ rSet = ∅ ∧ index_{s} = 0 ∧ index_{r} = 0

Proof: Immediate.

⟨2⟩2. Q.E.D.

Proof: Direct from the definitions of Init and HLS.Init.

⟨1⟩2. ∧ Init

∧ □[SomeAction]_{Vars}

⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof: We use the following invariant: Let: Inv =^{Δ} 1.∧ sSet ∩ rSet = ∅ 2.∧ ∨ sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}

We use Inv.1 to prove that Pop simulates HLS.Pop. We use Inv.2 to prove that Inv.1 is invariant under Push.

⟨2⟩1. ∧ Init

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof:

⟨3⟩1. Init ⇒ Inv

Proof: Inv.1 and Inv.2 follow immediately from sSet = ∅ and rSet = ∅.

⟨3⟩2. ∧ Inv

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof:

⟨4⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ Inv′

Proof:

⟨5⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ Transfer ∨ unchanged Vars

⇒ Inv′

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : Push(a) ⇒ Inv′

Proof: Let: a : constant

⟨7⟩1. ∧ Inv ; ∧ Push(a)

⇒ Inv′

Proof:

⟨8⟩1. ∧ Inv

∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ sSet ∩ rSet = ∅

∧ ∨ sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩}

∧ unchanged rSet

⇒ sSet′ ∩ rSet′ = ∅

Proof: From sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s} follows {⟨index_{s}, a ⟩} ∉ rSet. From this, the other parts of the premise and set theory we obtain

sSet′ ∩ rSet′= (sSet ∪ {⟨index_{s}, a ⟩}) ∩ rSet = (sSet ∩ rSet) ∪ ({⟨index_{s}, a ⟩} ∩ rSet) = ∅ ∪ ∅ = ∅.

⟨9⟩2.

∧ ∨ sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩}

∧ index′_{s} = index_{s} + 1

∧ unchanged rSet

⇒ ∨ sSet′ ∪ rSet′ = ∅ ∨ MaxIndex(sSet′ ∪ rSet′) < index′_{s}

Proof: From sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}, sSet′ = sSet ∪ {⟨index_{s}, a ⟩} and unchanged rSet follows MaxIndex(sSet′ ∪ rSet′) = index_{s}. From this and index′_{s} = index_{s} + 1 follows MaxIndex(sSet′ ∪ rSet′) < index′_{s}.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Direct from the definition of Push(a).

⟨7⟩2. Q.E.D. Proof: Predicate logic: forall-intro.

⟨6⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ Inv′

Proof: Let: a : constant

⟨8⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ Inv′

Proof:

⟨9⟩1.

∧ sSet ∩ rSet = ∅ ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ unchanged sSet ⇒ sSet′ ∩ rSet′ = ∅

Proof: From unchanged sSet and rSet′ = rSet \{⟨index_{r}, a ⟩} follows sSet′ ∩ rSet′ ⊆ sSet ∩ rSet. From this and sSet ∩ rSet = ∅ follows sSet′ ∩ rSet′ = ∅.

⟨9⟩2.

∧ ∨ sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}

∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∨ sSet′ ∪ rSet′ = ∅ ∨ MaxIndex(sSet′ ∪ rSet′) < index′_{s}

Proof: From unchanged sSet and rSet′ = rSet \{⟨index_{r}, a ⟩} follows sSet′ ∩ rSet′ ⊆ sSet ∪ rSet. From this, sSet ∪rSet = ∅∨MaxIndex(sSet ∪rSet) < index_{s} and unchanged index_{s} follows sSet′ ∪ rSet′ = ∅ ∨ MaxIndex(sSet′ ∪ rSet′) < index′_{s}.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of Pop.

⟨6⟩3. ∧ Inv ; ∧ Transfer

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ p : ∧ p ∈ sSet ∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ Inv′

Proof: Let: p ∈ sSet

⟨8⟩1. ∧ Inv

∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ Inv′ Proof: ⟨9⟩1.

∧ sSet ∩ rSet = ∅ ∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ⇒ sSet′ ∩ rSet′ = ∅

Proof: Set theory: sSet′ ∩ rSet′= (sSet \{p}) ∩ (rSet ∪ {p}) = ((sSet \{p}) ∩ rSet) ∪ ((sSet \{p}) ∩ {p}) = ((sSet ∩ rSet) \{p}) ∪ ∅ ⊆ sSet ∩ rSet = ∅.

⟨9⟩2.

∧ ∨ sSet ∪ rSet = ∅ ∨ MaxIndex(sSet ∪ rSet) < index_{s}

∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ∧ unchanged index_{s} ⇒ ∨ sSet′ ∪ rSet′ = ∅ ∨ MaxIndex(sSet′ ∪ rSet′) < index′_{s}

Proof: From sSet′ = sSet \{p} and rSet′ = rSet ∪ {p} follows sSet′ ∪ rSet′ = sSet ∪ rSet ∪ {p}. From this and p ∈ sSet follows sSet′ ∪ rSet′ = sSet ∪ rSet. From this, unchanged index_{s} and sSet ∪rSet = ∅∨MaxIndex(sSet ∪rSet) < index_{s} follows sSet′ ∪ rSet′ = ∅ ∨ MaxIndex(sSet′ ∪ rSet′) < index′_{s}.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D.

Proof: Direct from the definition of Transfer.

⟨6⟩4. ∧ Inv

∧ unchanged Vars ⇒ Inv′

Proof: Direct from the definitions of Vars and Inv.

⟨6⟩5. Q.E.D.

Proof: Propositional logic from ⟨6⟩1, ⟨6⟩2, ⟨6⟩3 and ⟨6⟩4.

⟨5⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨4⟩2. Q.E.D. Proof: Direct from ⟨4⟩1 using rule INV1.

⟨3⟩3. Q.E.D. Proof: Propositional logic from ⟨3⟩1 and ⟨3⟩2.

⟨2⟩2. ∧ □Inv

∧ □[SomeAction]_{Vars} ⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof:

⟨3⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ [HLS.SomeAction]_{HLS.Vars}

Proof:

⟨4⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ Transfer ∨ unchanged Vars

⇒ ∨ ∃ a : HLS.Push(a) ∨ HLS.Pop ∨ unchanged HLS.Vars

Proof: ⟨5⟩1. ∃ a : Push(a) ⇒ ∃ a : HLS.Push(a)

Proof: Let: a : constant

⟨6⟩1. Push(a) ⇒ HLS.Push(a)

Proof: ⟨7⟩1.

∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ sSet′ ∪ rSet′ = sSet ∪ rSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r}

Proof: ⟨8⟩1. a ∈ Messages ⇒ a ∈ Messages

Proof: Trivial.

⟨8⟩2. index_{s} − index_{r} < BufferLength ⇒ index_{s} − index_{r} < BufferLength

Proof: Trivial.

⟨8⟩3.

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩}

∧ unchanged rSet

⇒ sSet′ ∪ rSet′ = sSet ∪ rSet ∪ {⟨index_{s}, a ⟩}

Proof: Simple set theory.

⟨8⟩4. index′_{s} = index_{s} + 1 ⇒ index′_{s} = index_{s} + 1

Proof: Trivial.

⟨8⟩5. unchanged index_{r} ⇒ unchanged index_{r}

Proof: Trivial.

⟨8⟩6. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3, ⟨8⟩4 and ⟨8⟩5.

⟨7⟩2. Q.E.D.

Proof: Direct from the definitions of Push(a) and HLS.Push(a).

⟨6⟩2. Q.E.D. Proof: Predicate logic: exist-intro and forall-intro.

⟨5⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ HLS.Pop

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ sSet ∪ rSet ∧ sSet′ ∪ rSet′ = (sSet ∪ rSet) \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s}

Proof: Let: a : constant

⟨7⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet

∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∧ ⟨index_{r}, a ⟩ ∈ sSet ∪ rSet ∧ sSet′ ∪ rSet′ = (sSet ∪ rSet) \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s}

Proof:

⟨8⟩1. ⟨index_{r}, a ⟩ ∈ rSet ⇒ ⟨index_{r}, a ⟩ ∈ sSet ∪ rSet

Proof: Simple set theory. ⟨8⟩2.

∧ sSet ∩ rSet = ∅

∧ ⟨index_{r}, a ⟩ ∈ rSet

∧ rSet′ = rSet \{⟨index_{r}, a ⟩}unchanged sSet ⇒ sSet′ ∪ rSet′ = (sSet ∪ rSet) \{⟨index_{r}, a ⟩}

Proof: From sSet ∩ rSet = ∅ and ⟨index_{r}, a ⟩ ∈ rSet follows ⟨index_{r}, a ⟩ ∉ sSet and thus sSet = sSet \{⟨index_{r}, a ⟩}. Using this, rSet′ = rSet \{⟨index_{r}, a ⟩}, unchanged sSet and some set theory we obtain sSet′ ∪ rSet′= sSet ∪ (rSet \{⟨index_{r}, a ⟩}) = (sSet \{⟨index_{r}, a ⟩}) ∪ (rSet \{⟨index_{r}, a ⟩}) = (sSet ∪ rSet) \{⟨index_{r}, a ⟩}.

⟨8⟩3. index′_{r} = index_{r} + 1 ⇒ index′_{r} = index_{r} + 1

Proof: Trivial. ⟨8⟩4. unchanged index_{s} ⇒ unchanged index_{s}

Proof: Trivial. ⟨8⟩5. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3 and ⟨8⟩4. ⟨7⟩2. Q.E.D.

Proof: Predicate logic: exist-intro and forall-intro. ⟨6⟩2. Q.E.D.

Proof: Direct from the definitions of Pop and HLS.Pop. ⟨5⟩3. Transfer ⇒ unchanged HLS.Vars

Proof: ⟨6⟩1.

∧ ∃ p : ∧ p ∈ sSet ∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ unchanged HLS.Vars

Proof: Let: p ∈ sSet ⟨7⟩1.

∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ unchanged HLS.Vars

Proof: From sSet′ = sSet \{p} and rSet′ = rSet ∪ {p} follows sSet′ ∪ rSet′ = sSet ∪ rSet ∪ {p}. From this and p ∈ sSet follows sSet′ ∪ rSet′ = sSet ∪ rSet. From this, unchanged ⟨index_{s}, index_{r} ⟩ and the definition of HLS.Vars follows unchanged HLS.Vars.

⟨7⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨6⟩2. Q.E.D.

Proof: Direct from the definition of Transfer.

⟨5⟩4. unchanged Vars ⇒ unchanged HLS.Vars

Proof: Direct from the definitions of Vars and HLS.Vars.

⟨5⟩5. Q.E.D.

Proof: Propositional logic from ⟨5⟩1, ⟨5⟩2, ⟨5⟩3 and ⟨5⟩4.

⟨4⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨3⟩2. Q.E.D.

Proof: Proof by STL5 and STL4.

⟨2⟩3. Q.E.D.

Proof: Direct from ⟨2⟩1 and ⟨2⟩2 using propositional logic.

⟨1⟩3. Q.E.D. Proof: Direct from ⟨1⟩1 and ⟨1⟩2 using propositional logic.

5 Copy and Purge

Specification IV introduces a first degree of asynchronism between both sides of communication. An index-message pair is no longer Transfer’d but rather Copy’d from sSet to rSet and later Purge’d from sSet, when it has been Pop’d for certain. As a consequence rSet is not disjoint from, but rather a subset of sSet. This asynchronism is a first step towards handling loss of data between sender and receiver: the sender became careful, she keeps a sent message until she knows it has been Pop’d.

In the Specifications II and III , the difference index_{s} − index_{r} was controlled to ensure that the buffer didn’t exceed the maximum length. Here, we use the term index_{s} − MinIndex(sSet) instead, since MinIndex(sSet) can linger below index_{r}. The size control is now completely local to the sender side.

This is the only change to Push. Pop has not changed at all. In contrast to III .Transfer, Copy allows multiple copying of the same pair to rSet. Since we are dealing with sets, such multiple copies are idempotent. Purge can handle several messages at once: it non-deterministically picks an already-Pop’d message in sSet and deletes this and all older messages.

The sender and the receiver side are not yet completely separated. Copy is a common action using both sSet and rSet. Purge could be regarded as a sender action, but it still uses the receiver information in index_{r}, thus index_{r} remains a global variable.

module IV

extends CommonDefinitions

variables sSet, rSet, index_{r}, index_{s}

Vars =^{Δ} ⟨sSet, rSet, index_{r}, index_{s} ⟩ Init =^{Δ} ∧ index_{r} = 0 ; ∧ index_{s} = 0 ; ∧ sSet = ∅ ; ∧ rSet = ∅

Push(a) =^{Δ} ∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Copy =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩

Purge =^{Δ} ∧ ∃ p ∈ sSet : ∧ p[1] < index_{r} ∧ sSet′ = sSet \ {pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{r}, index_{s} ⟩ SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ Copy ∨ Purge Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

IV.Safety implies III.Safety

module IV implies III

extends IV

UpperSet(set, index) =^{Δ} {p ∈ set : p[1] ≥ index} HLSsSet =^{Δ} UpperSet(sSet, index_{r}) \rSet HLS =^{Δ} instance III with sSet ← HLSsSet rSet ← rSet index_{s} ← index_{s} index_{r} ← index_{r}

Indices =^{Δ} {i ∈ Nat : index_{r} ≤ i < index_{s}}

theorem Safety ⇒ HLS.Safety

⟨0⟩3. Safety ⇒ HLS.Safety

Proof: ⟨1⟩1. Init ⇒ HLS.Init

Proof:

⟨2⟩1. ∧ sSet = ∅ ; ∧ rSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

⇒ ∧ HLSsSet = ∅ ∧ rSet = ∅ ∧ index_{s} = 0 ∧ index_{r} = 0

Proof: Direct from the definition of HLSsSet.

⟨2⟩2. Q.E.D.

Proof: Direct from the definitions of Init and HLS.Init.

⟨1⟩2. ∧ Init

∧ □[SomeAction]_{Vars}

⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof: We use the following invariant:

Let: Inv =^{Δ} 1.∧ rSet ⊆ UpperSet(sSet, index_{r}) 2.∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s} 3.∧ index_{r} ≤ index_{s} 4.∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1

We use Inv.1, Inv.2, Inv.3 and Inv.4 to prove that Push simulates HLS.Push. We use Inv.1 and Inv.4 to prove that Pop simulates HLS.Pop.

Instead of Inv.1 one might use the weaker rSet ⊆ sSet, but that can’t be proven to be invariant without additional Inv-parts.

⟨2⟩1. ∧ Init

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof: ⟨3⟩1. Init ⇒ Inv

Proof: Inv.1 follows from sSet = ∅ and rSet = ∅. Inv.2 follows from sSet = ∅. Inv.3 follows from index_{s} = 0 and index_{r} = 0. Inv.4 follows from Indices = ∅, which follows from index_{s} = 0 and index_{r} = 0.

⟨3⟩2. ∧ Inv

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof:

⟨4⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ Inv′

Proof:

⟨5⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ Copy ∨ Purge ∨ unchanged Vars

⇒ Inv′

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : Push(a) ⇒ Inv′

Proof:

Let: a : constant

⟨7⟩1. ∧ Inv ; ∧ Push(a)

⇒ Inv′

Proof:

⟨8⟩1. ∧ Inv

∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ rSet ⊆ UpperSet(sSet, index_{r}) ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ rSet′ ⊆ UpperSet(sSet′, index′_{r})

Proof: Follows from rSet′ = rSet ⊆ UpperSet(sSet, index_{r}) ⊆ UpperSet(sSet′, index′_{r}).

⟨9⟩2.

∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ⇒ ∨ sSet′ = ∅ ∨ MaxIndex(sSet′) < index′_{s}

Proof: From sSet = ∅ ∨ MaxIndex(sSet) < index_{s} and sSet′ = sSet ∪ {⟨index_{s}, a ⟩} follows MaxIndex(sSet′) = index_{s}. From this and index′_{s} = index_{s} + 1 follows MaxIndex(sSet′) < index′_{s}.

⟨9⟩3.

∧ index_{r} ≤ index_{s} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r} ⇒ index′_{r} ≤ index′_{s}

Proof: Follows from index′_{r} = index_{r} ≤ index_{s} < index′_{s}.

⟨9⟩4.

∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r} ⇒ ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1

Proof: From sSet′ = sSet ∪ {⟨index_{s}, a ⟩} follows for all i ≠ index_{s}: |{p ∈ sSet : p[1] = i}| = |{p ∈ sSet′ : p[1] = i}|. Thus for all i ∈ Indices: |{p ∈ sSet′ : p[1] = i}| = |{p ∈ sSet : p[1] = i}| = 1. From sSet = ∅ ∨ MaxIndex(sSet) < index_{s} follows |{p ∈ sSet : p[1] = index_{s}}| = 0. From this and sSet′ = sSet ∪ {⟨index_{s}, a ⟩} follows |{p ∈ sSet′ : p[1] = index_{s}}| = 1. From index′_{s} = index_{s} + 1, unchanged index_{r} and the definition of Indices follows Indices′ = Indices ∪ {index_{s}}. Now from this, ∀ i ∈ Indices : |{p ∈ sSet′ : p[1] = i}| = 1 and |{p ∈ sSet′ : p[1] = index_{s}}| = 1 we obtain ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1.

⟨9⟩5. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 and ⟨9⟩4.

⟨8⟩2. Q.E.D.

Proof: Direct from the definition of Push(a).

⟨7⟩2. Q.E.D. Proof: Predicate logic: forall-intro.

⟨6⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ Inv′

Proof: Let: a : constant

⟨8⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ rSet ⊆ UpperSet(sSet, index_{r})

∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged sSet ⇒ rSet′ ⊆ UpperSet(sSet′, index′_{r})

Proof: From rSet ⊆ UpperSet(sSet, index_{r}) follows rSet = UpperSet(rSet, index_{r}). From rSet ⊆ UpperSet(sSet, index_{r}) and ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 follows |{p ∈ rSet : p[1] = index_{r}}| = 1. From |{p ∈ rSet : p[1] = index_{r}}| = 1 and ⟨index_{r}, a ⟩ ∈ rSet follows {p ∈ rSet : p[1] = index_{r}} = ⟨index_{r}, a ⟩.

Thus rSet \{⟨index_{r}, a ⟩} = UpperSet(rSet, index_{r} + 1). Now we obtain rSet′= rSet \{⟨index_{r}, a ⟩} = UpperSet(rSet, index_{r} + 1) ⊆ UpperSet(sSet, index_{r} + 1) = UpperSet(sSet′, index′_{r}).

⟨9⟩2.

∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∨ sSet′ = ∅ ∨ MaxIndex(sSet′) < index′_{s}

Proof: Trivial.

⟨9⟩3.

∧ rSet ⊆ UpperSet(sSet, index_{r}) ∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ index_{r} ≤ index_{s} ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s} ⇒ index′_{r} ≤ index′_{s}

Proof: From ⟨index_{r}, a ⟩ ∈ rSet and rSet ⊆ UpperSet(sSet, index_{r}) follows index_{r} ∈ sSet. From index_{r} ∈ sSet and sSet = ∅ ∨ MaxIndex(sSet) < index_{s} follows index_{r} < index_{s} and thus index_{r} + 1 ≤ index_{s}. Now we obtain index′_{r} = index_{r} + 1 ≤ index_{s} = index′_{s}.

⟨9⟩4.

∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1

Proof: From index′_{r} = index_{r}+1 and unchanged index_{s} follows Indices′ ⊆ Indices. ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1 follows from Indices′ ⊆ Indices and unchanged sSet.

⟨9⟩5. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 and ⟨9⟩4.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of Pop.

⟨6⟩3. \begin{matrix}∧ Inv \\ ∧ Copy \end{matrix}

⇒ Inv′ Proof:

⟨7⟩1. ∧ Inv

∧ ∃ p : ∧ p ∈ sSet ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ Inv′

Proof: Let: p ∈ sSet

⟨8⟩1. ∧ Inv

∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ rSet ⊆ UpperSet(sSet, index_{r}) ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{r} ⟩ ⇒ rSet′ ⊆ UpperSet(sSet′, index′_{r})

Proof: From p ∈ sSet and p[1] ≥ index_{r} follows p ∈ UpperSet(sSet, index_{r}). Thus rSet′ = rSet ∪ {p} ⊆ UpperSet(sSet, index_{r}) = UpperSet(sSet′, index′_{r}).

⟨9⟩2.

∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∨ sSet′ = ∅ ∨ MaxIndex(sSet′) < index′_{s}

Proof: Trivial.

⟨9⟩3.

∧ index_{r} ≤ index_{s} ∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ index′_{r} ≤ index′_{s}

Proof: Trivial.

⟨9⟩4.

∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1

Proof: Direct from the definition of Indices.

⟨9⟩5. Q.E.D. Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 and ⟨9⟩4.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of Copy.

⟨6⟩4. ∧ Inv ; ∧ Purge

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ p : ∧ p ∈ sSet ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]}

∧ unchanged ⟨rSet, index_{s}, index_{r} ⟩ ⇒ Inv′

Proof: Let: p ∈ sSet

⟨8⟩1. ∧ Inv

∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{s}, index_{r} ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ rSet ⊆ UpperSet(sSet, index_{r}) ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ rSet′ ⊆ UpperSet(sSet′, index′_{r})

Proof: From p[1] < index_{r} follows UpperSet(sSet, index_{r}) ∩ {pair ∈ sSet : pair[1] ≤ p[1]} = ∅. Now we obtain rSet′= rSet ⊆ UpperSet(sSet, index_{r}) = UpperSet(sSet, index_{r}) \{pair ∈ sSet : pair[1] ≤ p[1]} = UpperSet(sSet \{pair ∈ sSet : pair[1] ≤ p[1]}, index_{r}) = UpperSet(sSet′, index′_{r}).

⟨9⟩2.

∧ ∨ sSet = ∅ ∨ MaxIndex(sSet) < index_{s}

∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged index_{s} ⇒ ∨ sSet′ = ∅ ∨ MaxIndex(sSet′) < index′_{s}

Proof: From sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} follows sSet′ ⊆ sSet. From sSet′ ⊆ sSet follows sSet′ = ∅ or MaxIndex(sSet′) ≤ MaxIndex(sSet) < index_{s} = index′_{s}.

⟨9⟩3.

∧ index_{r} ≤ index_{s}

∧ unchanged ⟨index_{s}, index_{r} ⟩

⇒ index′_{r} ≤ index′_{s}

Proof: Trivial.

⟨9⟩4.

∧ ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨index_{s}, index_{r} ⟩ ⇒ ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1

Proof: Let: SSubset = {p ∈ sSet : p[1] ∈ Indices}

From p[1] < index_{r} and the definition of Indices follows SSubset ∩ {pair ∈ sSet : pair[1] ≤ p[1]} = ∅. From this, the definition of Indices, sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} and unchanged ⟨index_{s}, index_{r} ⟩ follows SSubset′ = SSubset. From unchanged ⟨index_{s}, index_{r} ⟩ follows Indices′ = Indices. Using this, SSubset′ = SSubset and the definition of Indices we get the following equivalence: ∀ i ∈ Indices : |{p ∈ sSet : p[1] = i}| = 1 ⇔ ∀ i ∈ Indices : |{p ∈ SSubset : p[1] = i}| = 1 ⇔ ∀ i ∈ Indices′ : |{p ∈ SSubset′ : p[1] = i}| = 1 ⇔ ∀ i ∈ Indices′ : |{p ∈ sSet′ : p[1] = i}| = 1.

⟨9⟩5. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 and ⟨9⟩4.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D.

Proof: Direct from the definition of Purge.

⟨6⟩5. ∧ Inv

∧ unchanged Vars ⇒ Inv′

Proof: Direct from the definitions of Vars and Inv.

⟨6⟩6. Q.E.D.

Proof: Propositional logic from ⟨6⟩1, ⟨6⟩2, ⟨6⟩3, ⟨6⟩4 and ⟨6⟩5.

⟨5⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨4⟩2. Q.E.D. Proof: Direct from ⟨4⟩1 using rule INV1.

⟨3⟩3. Q.E.D.

Proof: Propositional logic from ⟨3⟩1 and ⟨3⟩2.

⟨2⟩2. ∧ □Inv

∧ □[SomeAction]_{Vars} ⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof:

⟨3⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ [HLS.SomeAction]_{HLS.Vars}

Proof:

⟨4⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ Copy ∨ Purge ∨ unchanged Vars

⇒ ∨ ∃ a : HLS.Push(a) ∨ HLS.Pop ∨ HLS.Transfer ∨ unchanged HLS.Vars

Proof:

⟨5⟩1. ∧ Inv

∧ ∃ a : Push(a) ⇒ ∃ a : HLS.Push(a)

Proof: Let: a : constant

⟨6⟩1. ∧ Inv ; ∧ Push(a)

⇒ HLS.Push(a)

Proof:

⟨7⟩1. ∧ Inv

∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ HLSsSet′ = HLSsSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Proof: ⟨8⟩1. a ∈ Messages ⇒ a ∈ Messages

Proof: Trivial.

⟨8⟩2. ∧ Inv

∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength

⇒ index_{s} − index_{r} < BufferLength

Proof:

⟨9⟩1. \begin{matrix}∧ Inv \\ ∧ sSet = ∅ \end{matrix}

⇒ Indices = ∅

Proof: From sSet = ∅ follows ∀ i : |{p ∈ sSet : p[1] = i}| = 0.

From this and Inv.4 follows Indices = ∅.

⟨9⟩2. Indices = ∅ ⇒ index_{s} − index_{r} < BufferLength

Proof: From Indices = ∅ follows index_{s} ≤ index_{r}.

Using this and the refinement mapping we obtain

index_{s} − index_{r} ≤ 0 < BufferLength.

⟨9⟩3. ∧ Indices ≠ ∅

∧ Inv

∧ index_{s} − MinIndex(sSet) < BufferLength ⇒ index_{s} − index_{r} < BufferLength

Proof: From Indices ≠ ∅ and Inv.4 follows |{p ∈ sSet : p[1] = index_{r}}| = 1. Then MinIndex(sSet) ≤ index_{r}, and we obtain index_{s} − index_{r} ≤ index_{s} − MinIndex(sSet) < BufferLength.

⟨9⟩4. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2 and ⟨9⟩3.

⟨8⟩3. ∧ Inv

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩}

∧ unchanged ⟨rSet, index_{r} ⟩

⇒ HLSsSet′ = HLSsSet ∪ {⟨index_{s}, a ⟩}

Proof: From Inv.1 and Inv.2 follows index_{s} ∉ rSet. Using this, Inv.3 and the refinement mapping we obtain HLSsSet′= UpperSet(sSet′, index′_{r}) \rSet′ = UpperSet(sSet ∪ {⟨index_{s}, a ⟩}, index_{r}) \rSet = (UpperSet(sSet, index_{r}) \rSet) ∪ {⟨index_{s}, a ⟩} = HLSsSet ∪ {⟨index_{s}, a ⟩}.

⟨8⟩4. index′_{s} = index_{s} + 1 ⇒ index′_{s} = index_{s} + 1

Proof: Trivial.

⟨8⟩5. unchanged ⟨rSet, index_{r} ⟩ ⇒ unchanged ⟨rSet, index_{r} ⟩

Proof: Trivial.

⟨8⟩6. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3, ⟨8⟩4 and ⟨8⟩5.

⟨7⟩2. Q.E.D.

Proof: Direct from the definitions of Push(a) and HLS.Push(a).

⟨6⟩2. Q.E.D. Proof: Predicate logic: exist-intro and forall-intro.

⟨5⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ HLS.Pop

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩ ⇒ ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨HLSsSet, index_{s} ⟩

Proof: Let: a : constant

⟨7⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet

∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1

∧ unchanged ⟨sSet, index_{s} ⟩

⇒ ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨HLSsSet, index_{s} ⟩

Proof: ⟨8⟩1. ⟨index_{r}, a ⟩ ∈ rSet ⇒ ⟨index_{r}, a ⟩ ∈ rSet

Proof: Trivial.

⟨8⟩2. rSet′ = rSet \{⟨index_{r}, a ⟩} ⇒ rSet′ = rSet \{⟨index_{r}, a ⟩}

Proof: Trivial.

⟨8⟩3. index′_{r} = index_{r} + 1 ⇒ index′_{r} = index_{r} + 1

Proof: Trivial.

⟨8⟩4. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet

∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged sSet ⇒ unchanged HLSsSet

Proof: From ⟨index_{r}, a ⟩ ∈ rSet, Inv.1 and Inv.4 follows {p ∈ sSet : p[1] = index_{r}} = {⟨index_{r}, a ⟩}. Using this and the refinement mapping we obtain HLSsSet′ = UpperSet(sSet′, index′_{r}) \rSet′ = UpperSet(sSet, index_{r} + 1) \(rSet \{⟨index_{r}, a ⟩}) = (UpperSet(sSet, index_{r}) \{p ∈ sSet : p[1] = index_{r}}) \(rSet \{⟨index_{r}, a ⟩}) = (UpperSet(sSet, index_{r}) \{⟨index_{r}, a ⟩}) \(rSet \{⟨index_{r}, a ⟩}) = UpperSet(sSet, index_{r}) \rSet = HLSsSet.

⟨8⟩5. unchanged index_{s} ⇒ unchanged index_{s}

Proof: Trivial.

⟨8⟩6. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3, ⟨8⟩4 and ⟨8⟩5.

⟨7⟩2. Q.E.D.

Proof: Predicate logic: exist-intro and forall-intro.

⟨6⟩2. Q.E.D. Proof: Direct from the definitions of Pop and HLS.Pop.

⟨5⟩3. Copy ⇒ ∨ HLS.Transfer ∨ unchanged HLS.Vars

Proof: ⟨6⟩1.

∧ ∃ p : ∧ p ∈ sSet ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ ∨ HLS.Transfer ∨ unchanged HLS.Vars

Proof: Let: p ∈ sSet

⟨7⟩1. ∧ p[1] ≥ index_{r}

∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ ∨ HLS.Transfer ∨ unchanged HLS.Vars Proof:

⟨8⟩1. ∧ p[1] ≥ index_{r}

∧ p ∉ rSet ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ HLS.Transfer

Proof:

⟨9⟩1. ∧ p[1] ≥ index_{r}

∧ p ∉ rSet

∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨sSet, index_{r} ⟩ ⇒ ∃ p : ∧ p ∈ HLSsSet ∧ HLSsSet′ = HLSsSet \{p} ∧ rSet′ = rSet ∪ {p}

Proof:

⟨10⟩1. ∧ p[1] ≥ index_{r}

∧ p ∉ rSet

∧ rSet′ = rSet ∪ {p}

∧ unchanged ⟨sSet, index_{r} ⟩ ⇒ ∧ p ∈ HLSsSet ∧ HLSsSet′ = HLSsSet \{p} ∧ rSet′ = rSet ∪ {p}

Proof: p ∈ HLSsSet follows from p ∈ sSet, p[1] ≥ index_{r}, p ∉ rSet and the definition of HLSsSet. Using the refinement mapping we obtain HLSsSet′= UpperSet(sSet′, index′_{r}) \rSet′ = UpperSet(sSet, index_{r}) \(rSet ∪ {p}) = UpperSet(sSet, index_{r}) \rSet \{p} = HLSsSet \{p}.

rSet′ = rSet ∪ {p} follows trivially from rSet′ = rSet ∪ {p}.

⟨10⟩2. Q.E.D.

Proof: Predicate logic: exist-intro.

⟨9⟩2. unchanged ⟨index_{s}, index_{r} ⟩ ⇒ unchanged ⟨index_{s}, index_{r} ⟩

Proof: Trivial.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. ∧ p ∈ rSet

∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ unchanged HLS.Vars

Proof: From p ∈ rSet and rSet′ = rSet ∪ {p} follows unchanged rSet. unchanged HLS.Vars follows directly from unchanged ⟨sSet, rSet, index_{s}, index_{r} ⟩

and the definition of HLS.Vars.

⟨8⟩3. Q.E.D.

Proof: Propositional logic from ⟨8⟩1 and ⟨8⟩2.

⟨7⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨6⟩2. Q.E.D. Proof: Direct from the definition of Copy.

⟨5⟩4. Purge ⇒ unchanged HLS.Vars

Proof: ⟨6⟩1.

∧ ∃ p : ∧ p ∈ sSet ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]}

∧ unchanged ⟨rSet, index_{s}, index_{r} ⟩ ⇒ unchanged ⟨HLSsSet, rSet, index_{s}, index_{r} ⟩

Proof: ⟨7⟩1.

∧ ∃ p : ∧ p ∈ sSet ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]}

∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ unchanged HLSsSet

Proof: Let: p ∈ sSet

⟨8⟩1. ∧ p[1] < index_{r}

∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{r} ⟩ ⇒ unchanged HLSsSet

Proof: From p[1] < index_{r} follows UpperSet(sSet, index_{r}) ∩ {pair ∈ sSet : pair[1] ≤ p[1]} = ∅. Using this and the refinement mapping we obtain HLSsSet′= UpperSet(sSet′, index′_{r}) \rSet′ = UpperSet(sSet \{pair ∈ sSet : pair[1] ≤ p[1]}, index_{r}) \rSet = UpperSet(sSet, index_{r}) \{pair ∈ sSet : pair[1] ≤ p[1]} \rSet = UpperSet(sSet, index_{r}) \rSet = HLSsSet.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. unchanged ⟨rSet, index_{s}, index_{r} ⟩ ⇒ unchanged ⟨rSet, index_{s}, index_{r} ⟩

Proof: Trivial.

⟨7⟩3. Q.E.D.

Proof: Propositional logic from ⟨7⟩1 and ⟨7⟩2. ⟨6⟩2. Q.E.D.

Proof: Direct from the definitions of Purge and HLS.Vars. ⟨5⟩5. unchanged Vars ⇒ unchanged HLS.Vars

Proof: Direct from the definitions of Vars and HLS.Vars. ⟨5⟩6. Q.E.D.

Proof: Propositional logic from ⟨5⟩1, ⟨5⟩2, ⟨5⟩3, ⟨5⟩4 and ⟨5⟩5. ⟨4⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions. ⟨3⟩2. Q.E.D.

Proof: Proof by STL5 and STL4. ⟨2⟩3. Q.E.D.

Proof: Direct from ⟨2⟩1 and ⟨2⟩2 using propositional logic. ⟨1⟩3. Q.E.D.

Proof: Direct from ⟨1⟩1 and ⟨1⟩2 using propositional logic.

6 Sliding Window with Linear Arithmetic

Module V specifies the sliding-window-style message retransmission mechanism with linear arithmetic. We introduce full decoupling between sender and receiver by modeling communications as two one-way communication channels: a forward channel fBuffer for the messages and a backward channel bBuffer for acknowledgements. These are the only common variables of the sender and the receiver sides.

The communication channels are handled as if they might lose data: sender and receiver can send messages rsp. acknowledgements repeatedly; the sender keeps the sent messages until they have been acknowledged, and the receiver acknowledges only what he has already Pop’d.

Rather than Copying a pair from one side to the other, the pair is put into fBuffer with SendMsg, and read from there by ReadMsg. fBuffer contains either one index-message pair or the zero element ⟨0, ⊥_{Messages} ⟩ which indicates ”no message”. SendMsg copies an arbitrary message from sSet into fBuffer, no matter if this overwrites an unread earlier message. Reading a message deletes it from fBuffer and puts it into rSet.

SendAck and ReadAck replace IV .Purge: SendAck copies index_{r} into bBuffer. Thus bBuffer contains the index of the oldest message, that might not yet be Pop’d. It can be understood as meaning ”precisely those messages older than this index are guaranteed to be Pop’d”. ReadAck removes all messages from sSet with an index older (i.e. smaller) than that in bBuffer. In contrast to fBuffer, bBuffer is never reset to 0.

module V

extends CommonDefinitions

variables sSet, rSet, index_{r}, index_{s}, fBuffer, bBuffer

Vars =^{Δ} ⟨sSet, rSet, index_{r}, index_{s}, fBuffer, bBuffer ⟩ Init =^{Δ} ∧ index_{r} = 0 ∧ index_{s} = 0 ∧ sSet = ∅ ∧ rSet = ∅ ∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ bBuffer = 0

Push(a) =^{Δ} ∧ a ∈ Messages ∧ (sSet = ∅) ∨ (index_{s} − MinIndex(sSet) < BufferLength) ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r}, fBuffer, bBuffer ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩

SendMsg =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ fBuffer′ = p ∧ unchanged ⟨index_{s}, index_{r}, sSet, rSet, bBuffer ⟩ ReadMsg =^{Δ} ∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩ ∧ fBuffer[1] < index_{r} + BufferLength ∧ fBuffer[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {fBuffer} ∧ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged ⟨index_{s}, index_{r}, sSet, bBuffer ⟩ SendAck =^{Δ} ∧ bBuffer′ = index_{r} ∧ unchanged ⟨index_{s}, index_{r}, sSet, rSet, fBuffer ⟩ ReadAck =^{Δ} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] < bBuffer} ∧ unchanged ⟨index_{s}, index_{r}, rSet, fBuffer, bBuffer ⟩ SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ SendMsg ∨ ReadMsg ∨ SendAck ∨ ReadAck Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

V.Safety implies IV.Safety

module V implies IV

extends V

HLS =^{Δ} instance IV with sSet ← sSet rSet ← rSet index_{s} ← index_{s} index_{r} ← index_{r}

PurgeSet =^{Δ} {pair ∈ sSet : pair[1] < bBuffer}

theorem Safety ⇒ HLS.Safety

⟨0⟩4. Safety ⇒ HLS.Safety

Proof: ⟨1⟩1. Init ⇒ HLS.Init

Proof:

⟨2⟩1. ∧ sSet = ∅

∧ rSet = ∅ ∧ index_{s} = 0 ∧ index_{r} = 0 ∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ bBuffer = 0 ⇒ ∧ sSet = ∅ ; ∧ rSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

Proof: Immediate.

⟨2⟩2. Q.E.D.

Proof: Direct from the definitions of Init and HLS.Init.

⟨1⟩2. ∧ Init

∧ □[SomeAction]_{Vars}

⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof: We use the following invariant:

Let: Inv =^{Δ} 1.∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet 2.∧ bBuffer ≤ index_{r}

We use Inv.1 to prove that ReadMsg simulates HLS.Copy.

We use Inv.2 to prove that ReadAck simulates HLS.Purge or unchanged HLS.Vars, and to prove that Inv.1 is invariant under ReadAck.

⟨2⟩1. ∧ Init

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof: ⟨3⟩1. Init ⇒ Inv

Proof: Inv.1 follows from fBuffer = ⟨0, ⊥_{Messages} ⟩. Inv.2 follows from bBuffer = 0 and index_{r} = 0.

⟨3⟩2. ∧ Inv

∧ □[SomeAction]_{Vars} ⇒ □Inv

Proof:

⟨4⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ Inv′

Proof:

⟨5⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ SendMsg ∨ ReadMsg ∨ SendAck ∨ ReadAck ∨ unchanged Vars

⇒ Inv′

Proof:

⟨6⟩1. ∧ Inv

∧ ∃ a : Push(a) ⇒ Inv′

Proof:

Let: a : constant

⟨7⟩1. ∧ Inv ; ∧ Push(a)

⇒ Inv′

Proof:

⟨8⟩1. ∧ Inv

∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r}, fBuffer, bBuffer ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet

∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ unchanged ⟨index_{r}, fBuffer ⟩ ⇒ ∨ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer′[1] < index′_{r} ∨ fBuffer′ ∈ sSet′

Proof: ⟨10⟩1.

∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged fBuffer ⇒ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

Proof: Trivial.

⟨10⟩2.

∧ fBuffer[1] < index_{r} ∧ unchanged ⟨index_{r}, fBuffer ⟩ ⇒ fBuffer′[1] < index′_{r}

Proof: Trivial.

⟨10⟩3.

∧ fBuffer ∈ sSet ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ unchanged fBuffer ⇒ fBuffer′ ∈ sSet′

Proof: From sSet′ = sSet ∪ {⟨index_{s}, a ⟩} follows sSet ⊆ sSet′. Now fBuffer′ = fBuffer ∈ sSet ⊆ sSet′.

⟨10⟩4. Q.E.D.

Proof: Propositional logic from ⟨10⟩1, ⟨10⟩2 and ⟨10⟩3.

⟨9⟩2.

∧ bBuffer ≤ index_{r} ∧ unchanged ⟨index_{r}, bBuffer ⟩ ⇒ bBuffer′ ≤ index′_{r}

Proof: Trivial.

⟨9⟩3. Q.E.D. Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Direct from the definition of Push(a).

⟨7⟩2. Q.E.D. Proof: Predicate logic: forall-intro.

⟨6⟩2. \begin{matrix}∧ Inv \\ ∧ Pop \end{matrix}

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩ ⇒ Inv′

Proof: Let: a : constant

⟨8⟩1. ∧ Inv

∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet

∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, fBuffer ⟩ ⇒ ∨ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer′[1] < index′_{r} ∨ fBuffer′ ∈ sSet′

Proof: ⟨10⟩1.

∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged fBuffer ⇒ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

Proof: Trivial.

⟨10⟩2.

∧ fBuffer[1] < index_{r} ∧ index′_{r} = index_{r} + 1 ∧ unchanged fBuffer ⇒ fBuffer′[1] < index′_{r}

Proof: From index′_{r} = index_{r} + 1 follows index_{r} ≤ index′_{r}.

Now fBuffer′[1] = fBuffer[1] < index_{r} ≤ index′_{r}.

⟨10⟩3.

∧ fBuffer ∈ sSet

∧ unchanged ⟨sSet, fBuffer ⟩ ⇒ fBuffer′ ∈ sSet′

Proof: Trivial.

⟨10⟩4. Q.E.D.

Proof: Propositional logic from ⟨10⟩1, ⟨10⟩2 and ⟨10⟩3.

⟨9⟩2.

∧ bBuffer ≤ index_{r} ∧ index′_{r} = index_{r} + 1 ∧ unchanged bBuffer ⇒ bBuffer′ ≤ index′_{r}

Proof: From index′_{r} = index_{r} + 1 follows index_{r} ≤ index′_{r}. Now bBuffer′ = bBuffer ≤ index_{r} ≤ index′_{r}.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of Pop.

⟨6⟩3. ∧ Inv ; ∧ SendMsg

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ ∃ p : ∧ p ∈ sSet ∧ fBuffer′ = p

∧ unchanged ⟨sSet, rSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ Inv′

Proof: Let: p ∈ sSet

⟨8⟩1. ∧ Inv

∧ fBuffer′ = p ∧ unchanged ⟨sSet, rSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ Inv′

Proof: ⟨9⟩1.

∧ fBuffer′ = p ∧ unchanged sSet ⇒ fBuffer′ ∈ sSet′ Proof: From fBuffer′ = p and p ∈ sSet follows fBuffer′ ∈ sSet. From this and unchanged sSet follows fBuffer′ ∈ sSet′.

⟨9⟩2.

∧ bBuffer ≤ index_{r}

∧ unchanged ⟨index_{r}, bBuffer ⟩ ⇒ bBuffer′ ≤ index′_{r}

Proof: Trivial.

⟨9⟩3. Q.E.D.

Proof: Propositional logic from ⟨9⟩1 and ⟨9⟩2.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: forall-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of SendMsg.

⟨6⟩4. ∧ Inv ; ∧ ReadMsg

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩

∧ fBuffer[1] < index_{r} + BufferLength

∧ fBuffer[1] ≥ index_{r}

∧ rSet′ = rSet ∪ {fBuffer}

∧ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

∧ unchanged ⟨sSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ Inv′

Proof: ⟨8⟩1. fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ⇒ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

Proof: Trivial.

⟨8⟩2.

∧ bBuffer ≤ index_{r}

∧ unchanged ⟨index_{r}, bBuffer ⟩ ⇒ bBuffer′ ≤ index′_{r}

Proof: Trivial.

⟨8⟩3. Q.E.D.

Proof: Propositional logic from ⟨8⟩1 and ⟨8⟩2.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of ReadMsg.

⟨6⟩5. ∧ Inv ; ∧ SendAck

⇒ Inv′ Proof:

⟨7⟩1. ∧ Inv

∧ bBuffer′ = index_{r} ∧ unchanged ⟨sSet, rSet, index_{s}, index_{r}, fBuffer ⟩ ⇒ Inv′

Proof: ⟨8⟩1.

∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet

∧ unchanged ⟨sSet, index_{r}, fBuffer ⟩ ⇒ ∨ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer′[1] < index′_{r} ∨ fBuffer′ ∈ sSet′

Proof: Trivial.

⟨8⟩2.

∧ bBuffer′ = index_{r} ∧ unchanged index_{r} ⇒ bBuffer′ ≤ index′_{r}

Proof: Trivial.

⟨8⟩3. Q.E.D.

Proof: Propositional logic from ⟨8⟩1 and ⟨8⟩2.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of SendAck.

⟨6⟩6. ∧ Inv ; ∧ ReadAck

⇒ Inv′

Proof:

⟨7⟩1. ∧ Inv

∧ sSet′ = sSet \PurgeSet ∧ unchanged ⟨rSet, index_{s}, index_{r}, fBuffer, bBuffer ⟩ ⇒ Inv′

Proof: ⟨8⟩1.

∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet

∧ bBuffer ≤ index_{r} ∧ sSet′ = sSet \PurgeSet ∧ unchanged ⟨index_{r}, fBuffer ⟩ ⇒ ∨ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer′[1] < index′_{r} ∨ fBuffer′ ∈ sSet′

Proof:

⟨9⟩1.

∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged fBuffer ⇒ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

Proof: Trivial.

⟨9⟩2.

∧ fBuffer[1] < index_{r} ∧ unchanged ⟨index_{r}, fBuffer ⟩ ⇒ fBuffer′[1] < index′_{r}

Proof: Trivial.

⟨9⟩3.

∧ fBuffer[1] ≥ index_{r} ∧ fBuffer ∈ sSet ∧ bBuffer ≤ index_{r} ∧ sSet′ = sSet \PurgeSet ∧ unchanged fBuffer ⇒ fBuffer′ ∈ sSet′

Proof: From fBuffer[1] ≥ index_{r} and fBuffer ∈ sSet follows fBuffer ∈ {p ∈ sSet : p[1] ≥ index_{r}}. From bBuffer ≤ index_{r} follows {p ∈ sSet : p[1] ≥ index_{r}} ⊆ {p ∈ sSet : p[1] ≥ bBuffer}. From sSet′ = sSet \PurgeSet follows {p ∈ sSet : p[1] ≥ bBuffer} = {p ∈ sSet′ : p[1] ≥ bBuffer}. Using these conclusions and unchanged fBuffer we obtain fBuffer′= fBuffer ∈ {p ∈ sSet : p[1] ≥ index_{r}} ⊆ {p ∈ sSet : p[1] ≥ bBuffer} = {p ∈ sSet′ : p[1] ≥ bBuffer} ⊆ sSet′.

⟨9⟩4. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2 and ⟨9⟩3.

⟨8⟩2.

∧ bBuffer ≤ index_{r} ∧ unchanged ⟨index_{r}, bBuffer ⟩ ⇒ bBuffer′ ≤ index′_{r}

Proof: Trivial.

⟨8⟩3. Q.E.D.

Proof: Propositional logic from ⟨8⟩1 and ⟨8⟩2.

⟨7⟩2. Q.E.D. Proof: Direct from the definition of ReadAck.

⟨6⟩7. ∧ Inv

∧ unchanged Vars ⇒ Inv′

Proof: Direct from the definitions of Vars and Inv.

⟨6⟩8. Q.E.D.

Proof: Propositional logic from ⟨6⟩1, ⟨6⟩2, ⟨6⟩3, ⟨6⟩4, ⟨6⟩5, ⟨6⟩6 and ⟨6⟩7.

⟨5⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨4⟩2. Q.E.D.

Proof: Direct from ⟨4⟩1 using rule INV1.

⟨3⟩3. Q.E.D. Proof: Propositional logic from ⟨3⟩1 and ⟨3⟩2.

⟨2⟩2. ∧ □Inv

∧ □[SomeAction]_{Vars} ⇒ □[HLS.SomeAction]_{HLS.Vars}

Proof:

⟨3⟩1. ∧ Inv

∧ [SomeAction]_{Vars} ⇒ [HLS.SomeAction]_{HLS.Vars}

Proof:

⟨4⟩1. ∧ Inv

∧ ∨ ∃ a : Push(a) ∨ Pop ∨ SendMsg ∨ ReadMsg ∨ SendAck ∨ ReadAck ∨ unchanged Vars

⇒ ∨ ∃ a : HLS.Push(a) ∨ HLS.Pop ∨ HLS.Copy ∨ HLS.Purge ∨ unchanged HLS.Vars

Proof: ⟨5⟩1. ∃ a : Push(a) ⇒ ∃ a : HLS.Push(a)

Proof: Let: a : constant

⟨6⟩1. Push(a) ⇒ HLS.Push(a)

Proof:

⟨7⟩1.

∧ a ∈ Messages

∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r}, fBuffer, bBuffer ⟩ ⇒ ∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Proof: ⟨8⟩1. a ∈ Messages ⇒ a ∈ Messages

Proof: Trivial.

⟨8⟩2. ∨ sSet = ∅

∨ index_{s} − MinIndex(sSet) < BufferLength ⇒ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength

Proof: Trivial. ⟨8⟩3. sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ⇒ sSet′ = sSet ∪ {⟨index_{s}, a ⟩}

Proof: Trivial. ⟨8⟩4. index′_{s} = index_{s} + 1 ⇒ index′_{s} = index_{s} + 1

Proof: Trivial. ⟨8⟩5. unchanged ⟨rSet, index_{r} ⟩ ⇒ unchanged ⟨rSet, index_{r} ⟩

Proof: Trivial. ⟨8⟩6. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3, ⟨8⟩4 and ⟨8⟩5. ⟨7⟩2. Q.E.D.

Proof: Direct from the definitions of Push(a) and HLS.Push(a). ⟨6⟩2. Q.E.D.

Proof: Predicate logic: exist-intro and forall-intro. ⟨5⟩2. Pop ⇒ HLS.Pop

Proof:

⟨6⟩1.

∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩ ⇒ ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Proof: Let: a : constant ⟨7⟩1.

∧ ⟨index_{r}, a ⟩ ∈ rSet

∧ rSet′ = rSet \{⟨index_{r}, a ⟩}

∧ index′_{r} = index_{r} + 1

∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩ ⇒ ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Proof: ⟨8⟩1. ⟨index_{r}, a ⟩ ∈ rSet ⇒ ⟨index_{r}, a ⟩ ∈ rSet

Proof: Trivial. ⟨8⟩2. rSet′ = rSet \{⟨index_{r}, a ⟩} ⇒ rSet′ = rSet \{⟨index_{r}, a ⟩}

Proof: Trivial. ⟨8⟩3. index′_{r} = index_{r} + 1 ⇒ index′_{r} = index_{r} + 1

Proof: Trivial. ⟨8⟩4. unchanged ⟨sSet, index_{s} ⟩ ⇒ unchanged ⟨sSet, index_{s} ⟩

Proof: Trivial. ⟨8⟩5. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3 and ⟨8⟩4. ⟨7⟩2. Q.E.D.

Proof: Predicate logic: exist-intro and forall-intro. ⟨6⟩2. Q.E.D.

Proof: Direct from the definitions of Pop and HLS.Pop. ⟨5⟩3. SendMsg ⇒ unchanged HLS.Vars

Proof:

⟨6⟩1.

∧ ∃ p : ∧ p ∈ sSet ∧ fBuffer′ = p

∧ unchanged ⟨sSet, rSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ unchanged ⟨sSet, rSet, index_{s}, index_{r} ⟩

Proof: Immediate.

⟨6⟩2. Q.E.D. Proof: Direct from the definitions of SendMsg and HLS.Vars.

⟨5⟩4. ∧ Inv ; ∧ ReadMsg

⇒ HLS.Copy

Proof:

⟨6⟩1. ∧ Inv

∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩ ∧ fBuffer[1] < index_{r} + BufferLength ∧ fBuffer[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {fBuffer} ∧ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged ⟨sSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ ∧ ∃ p : ∧ p ∈ sSet ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩

Proof:

⟨7⟩1. ∧ Inv

∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩

∧ fBuffer[1] < index_{r} + BufferLength

∧ fBuffer[1] ≥ index_{r}

∧ rSet′ = rSet ∪ {fBuffer}

∧ fBuffer′ = ⟨0, ⊥_{Messages} ⟩

∧ unchanged ⟨sSet, index_{s}, index_{r}, bBuffer ⟩ ⇒ ∧ fBuffer ∈ sSet ∧ fBuffer[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {fBuffer} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩

Proof: ⟨8⟩1.

∧ ∨ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∨ fBuffer[1] < index_{r} ∨ fBuffer ∈ sSet

∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩ ∧ fBuffer[1] ≥ index_{r} ⇒ fBuffer ∈ sSet

Proof: Simple propositional logic.

⟨8⟩2. fBuffer[1] ≥ index_{r} ⇒ fBuffer[1] ≥ index_{r}

Proof: Trivial.

⟨8⟩3. rSet′ = rSet ∪ {fBuffer} ⇒ rSet′ = rSet ∪ {fBuffer}

Proof: Trivial.

⟨8⟩4. unchanged ⟨sSet, index_{s}, index_{r} ⟩ ⇒ unchanged ⟨sSet, index_{s}, index_{r} ⟩

Proof: Trivial.

⟨8⟩5. Q.E.D.

Proof: Propositional logic from ⟨8⟩1, ⟨8⟩2, ⟨8⟩3 and ⟨8⟩4.

⟨7⟩2. Q.E.D.

Proof: Predicate logic: exist-intro.

⟨6⟩2. Q.E.D. Proof: Direct from the definitions of ReadMsg and HLS.Copy.

⟨5⟩5. SendAck ⇒ unchanged HLS.Vars

Proof: ⟨6⟩1.

∧ bBuffer′ = index_{r} ∧ unchanged ⟨sSet, rSet, index_{s}, index_{r}, fBuffer ⟩ ⇒ unchanged ⟨sSet, rSet, index_{s}, index_{r} ⟩

Proof: Immediate.

⟨6⟩2. Q.E.D. Proof: Direct from the definitions of SendAck and HLS.Vars.

⟨5⟩6. ∧ Inv ; ∧ ReadAck

⇒ ∨ HLS.Purge ∨ unchanged HLS.Vars

Proof:

⟨6⟩1. ∧ Inv

∧ PurgeSet ≠ ∅ ∧ ReadAck ⇒ HLS.Transfer

Proof:

⟨7⟩1. ∧ Inv

∧ PurgeSet ≠ ∅

∧ sSet′ = sSet \PurgeSet

∧ unchanged ⟨rSet, index_{s}, index_{r}, fBuffer, bBuffer ⟩ ⇒ ∧ ∃ p : ∧ p ∈ sSet ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{s}, index_{r} ⟩ Proof: Let: p =^{Δ} MaxPair(PurgeSet)

⟨8⟩1. ∧ Inv

∧ PurgeSet ≠ ∅ ∧ sSet′ = sSet \PurgeSet ∧ unchanged ⟨rSet, index_{s}, index_{r}, fBuffer, bBuffer ⟩ ⇒ ∧ p ∈ sSet ∧ p[1] < index_{r} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{s}, index_{r} ⟩

Proof: ⟨9⟩1. PurgeSet ≠ ∅ ⇒ p ∈ sSet

Proof: From PurgeSet ≠ ∅ follows that p is well defined. From the definitions of p and PurgeSet follows p ∈ PurgeSet and PurgeSet ⊆ sSet, and thus p ∈ sSet.

⟨9⟩2.

∧ bBuffer ≤ index_{r}

∧ PurgeSet ≠ ∅

⇒ p[1] < index_{r}

Proof: From PurgeSet ≠ ∅ follows that p is well defined. From the definitions of p and PurgeSet follows p[1] < bBuffer. From this and bBuffer ≤ index_{r} follows p[1] < index_{r}.

⟨9⟩3.

∧ PurgeSet ≠ ∅

∧ sSet′ = sSet \PurgeSet

⇒ sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]}

Proof: From PurgeSet ≠ ∅ follows that p is well defined. From the definitions of p and PurgeSet follows {pair ∈ sSet : pair[1] ≤ p[1]} = PurgeSet. From this and sSet′ = sSet \PurgeSet follows sSet′ = sSet \{pair ∈ sSet : pair[1] ≤ p[1]}.

⟨9⟩4. unchanged ⟨rSet, index_{s}, index_{r} ⟩ ⇒ unchanged ⟨rSet, index_{s}, index_{r} ⟩

Proof: Trivial.

⟨9⟩5. Q.E.D.

Proof: Propositional logic from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 and ⟨9⟩4.

⟨8⟩2. Q.E.D.

Proof: Predicate logic: exist-intro.

⟨7⟩2. Q.E.D. Proof: Direct from the definitions of ReadAck and HLS.Transfer.

⟨6⟩2.

∧ PurgeSet = ∅ ∧ ReadAck

⇒ unchanged HLS.Vars

Proof: ⟨7⟩1.

∧ PurgeSet = ∅

∧ sSet′ = sSet \PurgeSet

∧ unchanged ⟨rSet, index_{s}, index_{r}, fBuffer, bBuffer ⟩ ⇒ unchanged ⟨sSet, rSet, index_{s}, index_{r} ⟩

Proof: unchanged ⟨rSet, index_{s}, index_{r} ⟩ follows immediately.

unchanged sSet follows from PurgeSet = ∅ and sSet′ = sSet \PurgeSet.

⟨7⟩2. Q.E.D.

Proof: Direct from the definitions of ReadAck and HLS.Vars.

⟨6⟩3. Q.E.D.

Proof: Propositional logic from ⟨6⟩1 and ⟨6⟩2.

⟨5⟩7. unchanged Vars ⇒ unchanged HLS.Vars

Proof: Direct from the definitions of Vars and HLS.Vars.

⟨5⟩8. Q.E.D.

Proof: Propositional logic from ⟨5⟩1, ⟨5⟩2, ⟨5⟩3, ⟨5⟩4, ⟨5⟩5, ⟨5⟩6 and ⟨5⟩7.

⟨4⟩2. Q.E.D.

Proof: Propositional logic from TLA^{+} definitions.

⟨3⟩2. Q.E.D.

Proof: Proof by STL5 and STL4.

⟨2⟩3. Q.E.D.

Proof: Direct from ⟨2⟩1 and ⟨2⟩2 using propositional logic.

⟨1⟩3. Q.E.D. Proof: Direct from ⟨1⟩1 and ⟨1⟩2 using propositional logic.