Mechanical Verification of a Schematic Protocol for Byzantine Fault Tolerant Clock Synchronization

Natarajan Shankar Computer Science Laboratory

SRI International 333 Ravenswood

Menlo Park, CA 94025

June 5, 1991

Abstract

Schneider [1] generalizes a number of protocols for Byzantine fault tolerant clock synchronization and presents a uniform proof for their correctness. We present a machine checked proof of this schematic protocol that revises some of the details in Schneider’s original analysis. The verification was carried out with the Ehdm system [2] developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith’s Interactive Convergence Algorithm [3] satisfies the requirements of Schneider’s protocol.

Contents

1 Introduction 1

2 Schneider’s Schema for Clock Synchronization 6 2.1 Defining Clocks . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Clock conditions . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 The Correctness Proof . . . . . . . . . . . . . . . . . . . . . . 14

2.3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.2 The Proof . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.4 ICA as an instance of Schneider’s scheme . . . . . . . . . . . 22

3 The Verification of Schneider’s Protocol using EHDM 25 3.1 The Clock Assumptions . . . . . . . . . . . . . . . . . . . . . 25 3.2 The Proof Highlights . . . . . . . . . . . . . . . . . . . . . . . 30

4 Conclusions 34

Bibliography 37

A Proof Summary 38

B The Complete EHDM Proof 40 Multiplication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Absolutes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Division . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Arith . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Countmod . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Clockassumptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Readbounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 Lemma3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Lemma final . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 Ica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 Ica2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 Ica3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 Ica4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

C Proof Chain Analysis 81 C.1 Proof Chain for Agreement . . . . . . . . . . . . . . . . . . . 81 C.2 Proof Chain for ICA Translation Invariance . . . . . . . . . . 85 C.3 Proof Chain for ICA Precision Enhancement . . . . . . . . . 86 C.4 Proof Chain for ICA Accuracy Preservation . . . . . . . . . . 90

List of Figures

3.1 Declarations from module clockassumptions . . . . . . . . . . 26 3.2 Constants in module clockassumptions . . . . . . . . . . . . . 27 3.3 Physical clock axioms in module clockassumptions . . . . . . 28 3.4 Clock definitions in module clockassumptions . . . . . . . . . 28 3.5 Conditions on Logical Clocks in module clockassumptions . . 29 3.6 Main Theorem in module lemma final . . . . . . . . . . . . . 30 3.7 Skew immediately following resynchronization from module

readbounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.8 Skew up to ith resynchronization from module lemma3 …. 31 3.9 Egocentric mean from module ica . . . . . . . . . . . . . . . . 32 3.10 Properties of egocentric mean from modules ica, ica3, and ica4 33

Chapter 1

Introduction

Synchronizing clocks in the presence of faults is a classic problem in distributed computing. Even the most accurate clocks do drift at significant rates, both with respect to a time standard and relative to each other. In order for independent processors to exhibit cooperative behavior, it is often required that their local clocks be synchronized. Such synchrony is the basis for distributed algorithms that use timeouts, time stamps, and rounds of message passing. Synchronization is also assumed when the same computation is executed on multiple, independent processors in order to mask processor failures. Digital avionics systems constitute a typical example of the need for synchronized clocks. In these systems, the results of multiple redundant processors are voted to ensure a high degree of fault tolerance, and the processor clocks must be synchronized in order to carry this out. Clock synchronization problems led to the scrubbing of the first scheduled launch of the NASA Space Shuttle [4], and to anomalous behavior of the Voyager spacecraft [5]. Butler [6] presents a survey of various clock synchronization protocols.

Synchronizing clocks in the presence of faults is a difficult problem. If synchrony is maintained by periodically broadcasting a global clock value to each of the processors, the failure of the global clock then becomes critical. On the other hand, if each processor has its own local clock and these clocks are initially synchronized, they might slowly drift apart so that with time the system loses its ability to behave synchronously. It is therefore necessary to periodically resynchronize the clocks. We are concerned here with algorithms that perform this resynchronization in a fault tolerant manner. In the cases we consider, the clocks are required to be synchronized only with respect to each other and not with respect to some external standard clock. The primary requirement that any solution must satisfy is that at any instant, the absolute difference, or the skew, between two clock readings should be within some bound δ. The secondary requirement is that there must be a small bound on the correction required to keep clocks in synchrony. The latter requirement prevents trivial solutions that, for example, reset the clocks to zero at each round of synchronization. We restrict our focus to the primary requirement, since the secondary requirement turns out to be a straightforward consequence of one of the assumptions for the operation of the protocol studied here.

To implement synchronized clocks, each processor has a physical clock whose drift rate with respect to a fixed standard time is bounded. We refer to the fixed standard time as real time. In addition to the physical clock, each processor maintains a logical, or virtual, clock that is computed by periodically applying an adjustment to the reading of the physical clock. The adjustment to be applied at the end of each period is determined by means of a synchronization protocol. The application of such an adjustment could be continuous so that the individual clock ticks are either sped up or slowed down, but no clock ticks are dropped or repeated. Alternately, the adjustment could be applied in an instantaneous manner, in which case, some clock ticks might be dropped or repeated. In the latter situation, critical events should not be scheduled during these clock ticks. This report only considers the case of instantaneous clock adjustments. These results are therefore applicable to the class of systems that have a synchronization phase followed by a period of normal operation in each cycle of synchronization. The results here can be extended to the case of continuous clock adjustments. Schneider [1] presents an analysis of continuous adjustments.

To take a somewhat coarse look at clock synchronization, suppose that the various physical clocks start synchronized and drift apart from real time at a rate not exceeding ρ. For example, a clock might gain or lose up to a minute every hour. The processors operate normally for a period R of, say, an hour. The processors then engage in a round of synchronization during which they exchange clock values. Assume for simplicity that the communication between clocks occurs instantaneously. At some mutually agreeable instant, the processors reset their clocks to some mutually agreeable value such as the average of their clock readings. Thus at the end of such a round of synchronization, the skew between clocks vanishes. Clearly, if we want the clocks to be no more than δ apart, the period R between synchronizations should not exceed δ/2ρ. Given that ρ is a minute per hour, and R is an hour, δ can be no less than two minutes.

The above outline obviously makes a great many simplifying assumptions, but it does capture the basic process of clock synchronization. The most significant invalid assumption is that clocks and processors do not fail. Clock synchronization protocols ought to be able to tolerate a certain number of processor failures since they are often used to synchronize multiple processors in fault-tolerant architectures. When processors do fail, they could do so in the worst possible way by exhibiting arbitrarily different behaviors towards different processors, e.g., by “maliciously” communicating different clock values to different processors. Such failures are known as Byzantine failures [7]. Consider the case of three clocks a, b, and c, when a reads 12 noon, b reads 11:59 am, and c has failed. To resynchronize, they exchange clock values and c maliciously communicates its value as 12:01 pm to a and as 11:58 am to b. Suppose each clock is resynchronized by taking the average of all the clock values observed by it, then a resets itself to 12 noon and b resets itself to 11:59 am. The clocks are thus no closer following resynchronization than immediately prior to resynchronization. Thus the clocks can continue to drift even further apart until the next round of synchronization.

The above scenario illustrates one of the earliest clock synchronization protocols capable of tolerating Byzantine processor failures: the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [3]. ICA tolerates up to ⌊(N − 1)/3⌋ failures for N processors. In ICA, a processor p resynchronizes for the i’th time when its clock reads iR. Processor p then reads the difference between the other clock readings and its own clock reading. By ignoring clock differences larger than a certain value Δ, processor p computes the egocentric mean of the acceptable clock differences as the correction required to resynchronize its clock. Rushby and von Henke [8] have subjected Lamport and Melliar-Smith’s proof of correctness to mechanical scrutiny using Ehdm. As is often the case with fault-tolerant distributed protocols, the original proof is both subtle and complex. The mechanical verification was able to identify and correct several minor flaws, and to significantly streamline the proof.

Schneider [1] presents a clock synchronization scheme that generalizes protocols such as ICA. Schneider’s clock synchronization scheme (abbreviated here as SCS) regards each logical clock as being periodically reset to a value computed by a convergence function. The egocentric mean of ICA is an instance of such a convergence function. Schneider places certain natural conditions on the behavior of suitable convergence functions and shows that these conditions are sufficient for bounding the skew between the resulting logical clocks. He also shows that the convergence functions used by a number of existing protocols satisfy these restrictions. Such a schematic presentation of Byzantine clock synchronization provides an elegant framework for understanding various individual protocols, and greatly simplifies the proofs of their correctness.

Since the SCS protocol captures the mathematics behind Byzantine clock synchronization in an abstract and schematic manner, it makes an interesting candidate for verification. The schematic nature of the SCS protocol makes it convenient to subsequently verify a number of specific protocols as instances of the SCS protocol. Also, Schneider’s analysis employs a global “real time” rather than clock time as its frame of reference, i.e., clocks map real time to clock time. Lamport and Melliar-Smith’s analysis [3] of ICA and the verification by Rushby and von Henke [8] were both carried out in terms of clocks that mapped clock time to real time. The use of clock time as a frame of reference makes some of the mathematics is fairly cumbersome and also makes the specification harder to understand. It seems reasonable to assume that to each real time instant, there is a unique clock reading, but not quite as reasonable to insist that there is a unique real time instant corresponding to a clock reading since a failed clock could exhibit the same reading at different real time instants. It is, of course, possible to explain away such objections. The question of what is the best framework for specifying such protocols is, to our knowledge, still open.

The mechanical verification of the SCS protocol was carried out using the Ehdm verification system developed at the Computer Science Laboratory of SRI International. The egocentric mean function of the ICA protocol was also verified as satisfying Schneider’s restrictions. The SCS protocol and its informal proof are presented in Chapter 2. An overview of the mechanically checked proof is presented in Chapter 3. The appendices contain the complete listing of the proof that was presented as input to Ehdm.

The use of Ehdm to check the proof led to the clarification of a number of details from Schneider’s original presentation without tampering unduly with the outline and intent of his argument. Schneider’s proof employs a monotonicity condition on convergence functions that was found to be inessential for the proof. The monotonicity condition actually fails for ICA and other similar convergence functions (see Section 2.4). Schneider’s proof requires certain relations to hold between the convergence behavior of the convergence function, the drift rate of the physical clocks, the error in communicating clock values, and the time between synchronization rounds. The machine proof clears up some minor inaccuracies in Schneider’s derivation of these relations.

Acknowledgements. John Rushby supplied much of the background and guidance for this work. Friedrich von Henke helped me get started with Ehdm. I am also grateful to Fred Schneider and Rick Butler for their encouragement.

Schneider’s Schema for Clock Synchronization

Schneider shows that a number of known algorithms for synchronizing Byzantine clocks can be presented in a uniform manner so that their individual proofs are greatly simplified [1]. The exposition below follows Schneider’s outline quite closely, but revises a number of the details in the description of the protocol as well as the proof. Section 2.1 describes how the logical clock is computed from the physical clock using the convergence function. Section 2.2 describes the conditions on the behavior of clocks and on suitable convergence functions. The proof of correctness of clock synchronization from the conditions of Section 2.2 is outlined in Section 2.3.

2.1 Defining Clocks

The physical and logical clocks are presented as functions from real time (as given by some external standard) to clock readings. This real time thus forms the frame of reference and is often referred to simply as “time.”^{1} The variable t ranges over this real time. Synchronization takes place in rounds. The time at which processor p adjusts its clock following the i’th round of synchronization is represented by t_{p}^{i}. The starting time t_{p}^{0} which is the time from which the system is observed, is taken to be zero.

In our abstraction, both the real time and the clock readings can be interpreted as ranging over the real numbers or the rationals. The ordered field axioms that are used are satisfied by both the real numbers and the rationals. The term P C_{p}(t) is the reading of p’s physical clock at real time t. The adjusted virtual clock reading at time t_{p}^{i} is computed by applying an adjustment adj_{p}^{i} to the physical clock reading P C_{p}(t_{p}^{i}). In its i’th interval of operation, i.e., when t_{p}^{i} ≤ t < t_{p}^{i+1}, the virtual clock reading, V C_{p}(t) is given by P C_{p}(t) + adj_{p}^{i}. At round 0, the adjustment adj_{p}^{0} is taken to be 0 so that for t < t_{p}^{1}, the reading V C_{p}(t) is just P C_{p}(t). In other words, in the first period of operation, each clock takes its physical clock reading as its virtual clock reading. This means that for synchronization over the first period, we need as a condition, a bound on the initial skews between the physical clocks of nonfaulty processors.

1In the original presentation of the interactive convergence algorithm, clocks are represented as functions from clock time to the external standard time [3, 8].

For i > 0, we let Θ_{p}^{i} be an array of clock readings so that Θ_{p}^{i}(q) is p’s reading of q’s clock at time t_{p}^{i}. In the Ehdm formalization, the array of observed clock readings Θ_{p}^{i}, is actually represented as a function from clocks to readings. The corrected value of V C_{p}(t_{p}^{i}) is computed by a convergence function, cfn(p, Θ_{p}^{i}). The adjustment adj_{p}^{i} to be applied to the physical clock is therefore given by the difference cfn(p, Θ_{p}^{i}) − P C_{p}(t_{p}^{i}). Since Θ_{p}^{i} is a function, cfn is a higher-order function.

The above explanation of Θ_{p}^{i}(q) does not specify whether q’s physical or virtual clock is the one that is read by clock p. Note that if t_{q}^{i} preceded t_{p}^{i}, then q’s virtual clock has already been adjusted for the i’th time at time t_{p}^{i}. In Schneider’s model, Θ_{p}^{i}(q) is a reading of q’s virtual clock at time t_{p}^{i} but ignoring the i’th correction that may have already been applied to q’s clock. This value is represented by an abstraction called the interval clock. The interval clock reading IC_{q}^{i}(t) is given by P C_{q}(t) + adj_{q}^{i}. Thus for i > 0, the value Θ_{p}^{i}(q) is p’s reading of IC_{q}^{i−1}(t_{p}^{i}). The rationale for introducing an interval clock is that the observed clock readings in the protocol are based on readings exchanged prior to synchronization. The interval clock is an abstraction that is useful for describing the protocol and it need not actually be implemented. The physical and virtual clocks are of course both implemented.

The above description leads to following definitions where i ranges over the natural numbers and t > 0.

adj_{p}^{i+1} = cfn(p, Θ_{p}^{i+1}) − P C_{p}(t_{p}^{i+1})  (2.1.1)
adj_{p}^{0} = 0  (2.1.2)
IC_{p}^{i}(t) = P C_{p}(t) + adj_{p}^{i}  (2.1.3)
V C_{p}(t) = IC_{p}^{i}(t), for t_{p}^{i} ≤ t < t_{p}^{i+1}  (2.1.4)

It is easy to derive the following from Definitions (2.1.1), (2.1.3), and (2.1.4).

V C_{p}(t_{p}^{i+1}) = IC_{p}^{i+1}(t_{p}^{i+1}) = cfn(p, Θ_{p}^{i+1})  (2.1.5)
IC_{p}^{i+1}(t) = cfn(p, Θ_{p}^{i+1}) + P C_{p}(t) − P C_{p}(t_{p}^{i+1})  (2.1.6)

So far we have merely defined the virtual and interval clock functions in terms of the physical clock function P C_{p}(t), the synchronization times t_{p}^{i}, and the convergence function cfn applied to the clock readings Θ_{p}^{i}. In the next section, we enumerate Schneider’s constraints on these quantities when p is a nonfaulty, or correct, processor. The main result we obtain from these constraints and the above definitions is a bound δ on the skew between the logical clocks of two correct processors p and q.

Theorem 2.1.1 (bounded skew) For any two clocks p and q that are nonfaulty at time t,

|V C_{p}(t) − V C_{q}(t)| ≤ δ  (2.1.7)

The proof of Theorem 2.1.1 is outlined in Section 2.3.1.

2.2 Clock conditions

In formalizing the laws constraining the behavior of individual clocks, we must ensure that no assumptions are made regarding the faulty clocks since we are dealing with Byzantine failures. These laws which are conditions on the behavior of clocks are enumerated as axioms within the boxes below. Individual protocols and clock implementations are expected to satisfy these conditions.

The conditions constraining the behaviour of clocks employ a number of constants represented by lowercase Greek letters. All of these constants are taken to be non-negative.

Section 2.1 above described how the processors go through rounds of synchronization. The proof of Theorem 2.1.7 is by induction on the number of rounds. The main idea of the proof is to show that the virtual clocks are within δ_{S} immediately following a round of synchronization, and the skew between them does not exceed δ in the following period until the next round of synchronization. To start, the following condition asserts that the nonfaulty clocks are synchronized to within the quantity δ_{S} at time 0.

Condition 1 (initial skew) For nonfaulty processors p and q

|P C_{p}(0) − P C_{q}(0)| ≤ δ_{S}  (2.2.8)

The nonfaulty physical clocks must keep good enough time so that they do not drift away from real time by a rate greater than ρ.

Condition 2 (bounded drift) There is a nonnegative constant ρ such that if clock p is nonfaulty at time s, s ≥ t, then

(1 − ρ)(s − t) ≤ P C_{p}(s) − P C_{p}(t) ≤ (1 + ρ)(s − t)  (2.2.9)

A useful corollary to bounded drift is that two physical clocks p and q that are not faulty at time s,^{2} for s ≥ t, can drift further apart over the interval s − t by 2ρ(s − t), since both p and q can drift by ρ(s − t) with respect to real time, but in opposite directions.

|P C_{p}(s) − P C_{q}(s)| ≤ |P C_{p}(t) − P C_{q}(t)| + 2ρ(s − t)  (2.2.10)

Each protocol has some mechanism for triggering the resynchronization of the clocks. Schneider postulates the existence of a global synchronization signal, t_{G}^{i}, which occurs at a period bounded from above and below. One can usually interpret t_{G}^{i} as the real-time instant when the first nonfaulty processor decides to resynchronize for the i’th time. Schneider’s conditions on t_{G}^{i} are stated in terms of positive constants which we name lo, hi, and wid. His first condition is that the period t_{G}^{i+1} − t_{G}^{i} is bounded from below by lo, and from above by hi. The second condition bounds the delay in receiving the trigger so that t_{p}^{i} − t_{G}^{i} ≤ wid, for nonfaulty p.

Our description of the proof uses a slightly different set of parameters in order to dispense with the notion of a global synchronization signal used in Schneider’s formulation. The parameters below seem easier to identify for the various instances of Schneider’s protocol. The different choice of parameters do not affect the proof of correctness in any significant way. For individual synchronization protocols, it should be possible to derive one set of parameters from the other.

2In the description of the machine verification, great pains are taken to indicate the times at which the clocks are required to be nonfaulty. The rest of the informal outline of the proof makes the simplifying assumption that clocks are either faulty or nonfaulty, and disregards the time at which clocks are asserted as being nonfaulty.

Condition 3 (bounded interval) For nonfaulty clock p

0 < r_{min} ≤ t_{p}^{i+1} − t_{p}^{i} ≤ r_{max}  (2.2.11)

Condition 4 (bounded delay) For nonfaulty clocks p and q^{3}

|t_{q}^{i} − t_{p}^{i}| ≤ β  (2.2.12)

Condition 5 (initial synchronization) For nonfaulty clock p

t_{p}^{0} = 0  (2.2.13)

From the conditions of bounded interval and bounded delay above, it follows that if β ≤ r_{min}, then t_{p}^{i} ≤ t_{q}^{i+1} for nonfaulty clocks p and q; i.e., there is no overlap between the i’th and the (i + 1)’th rounds of synchronization. Since we do want the synchronization rounds not to overlap, we state the following as a condition. If the periods were allowed to overlap, then the protocol would be difficult to implement since p could have started its (i + 1)’th clock before another processor q had started its i’th clock.

Condition 6 (nonoverlap)

β ≤ r_{min}  (2.2.14)

Another corollary of the bounded interval and bounded delay conditions is that for any two nonfaulty clocks p and q, we can derive,

0 ≤ t_{p}^{i+1} − t_{q}^{i} ≤ r_{max} + β.  (2.2.15)

For nonfaulty clocks p and q, Θ_{p}^{i+1}(q) represents p’s observation of q’s i’th clock reading at time t_{p}^{i+1}, i.e., it is p’s estimate of IC_{q}^{i}(t_{p}^{i+1}). The error in this reading is assumed to be bounded by Λ.

Condition 7 (reading error) For nonfaulty clocks p and q,

|IC_{q}^{i}(t_{p}^{i+1}) − Θ_{p}^{i+1}(q)| ≤ Λ  (2.2.16)

The above conditions turn out to be sufficient to bound the skew in the period between successive rounds of synchronization in terms of the skew bound δ_{S} immediately following synchronization. The conditions below of bounded faults, translation invariance, and precision enhancement, are needed to derive the skew bound δ_{S}. The condition of accuracy preservation below is needed to bound the skew between virtual clocks when, for instance, q has synchronized for the i’th time but p has not.

The parameter N is the total number of processors, and F is the maximum number of faulty clocks that the algorithm is expected to tolerate. This property of the system is captured by the following condition.

Condition 8 (bounded faults) At any time t, the number processors faulty at time t is at most F.

The conditions below are mathematical constraints placed on the convergence function, e.g., clocks, drifts, and failures, do not play any role in the statements. The isolation of the constraints makes it possible to demonstrate that the egocentric mean function of ICA satisfies the conditions of translation invariance, precision enhancement, and accuracy preservation, in purely mathematical terms. Note that these conditions do not make any distinction between the faulty and the nonfaulty clocks but are instead given in terms of a subset C of clocks satisfying certain mathematical constraints.

Suppose that t_{p}^{i} ≥ t_{q}^{i} for nonfaulty p and q, then in order to compute δ_{S}, we are interested in comparing the clock times for p and q at t_{p}^{i}, the time when clocks p and q have both just been synchronized for the i’th time. Processor q starts its i’th interval clock at t_{q}^{i} with value cfn(q, Θ_{q}), so that its reading at t_{p}^{i} is cfn(q, Θ_{q}) + x, where x = P C_{q}(t_{p}^{i}) − P C_{q}(t_{q}^{i}). The condition of translation invariance indicates that adding x to the value of the convergence function should be the same as adding x to each clock reading instead. Recall that the array of clock readings is represented by a function from clocks to readings so that cfn is a higher-order function.

Condition 9 (translation invariance) For any function θ mapping clocks to clock values,

cfn(p, (λn: θ(n) + x)) = cfn(p, θ) + x  (2.2.17)

As a consequence of translation invariance, we know that at t_{p}^{i}, both p and q have been resynchronized and V C_{q}(t_{p}^{i}) = cfn(q, (λn: Θ_{q}(n) + x)) for some x, and V C_{p}(t_{p}^{i+1}) = cfn(p, Θ_{p}). We clearly need some condition to bound the difference between these two values of the convergence function to within δ_{S}. The condition of precision enhancement allows exactly such a comparison between values of the convergence function based on the range of values of some subset of the clock readings that intuitively correspond to the readings of nonfaulty clocks.

In the statement of precision enhancement, γ and θ are any two arrays (or functions) of clock readings, and C is to be intuitively interpreted as the subset of nonfaulty processors. This interpretation of C is permissible by the bounded faults condition. The reason it is not directly taken to be the set of nonfaulty clocks is because the protocol cannot assume that any individual clock can distinguish the faulty from the nonfaulty clocks. The convergence functions for some protocols can neglect readings of nonfaulty clocks while considering readings of faulty clocks.

Precision enhancement is used to bound the skew between two clocks immediately after both have been resynchronized whereas accuracy preservation is used to bound the skew between a clock that has been resynchronized and one that has yet to be resynchronized in the ith round. The condition of precision enhancement bounds the skew between two clocks as computed by the convergence function, based on the skews between the clock readings that are inputs to the convergence function. We will refer to the clocks in C as C-clocks. Precision enhancement then asserts that if the readings of different C-clocks in γ fall within a range y as do the C-clock readings in θ, and the corresponding readings in γ and in θ of any C-clock differ by no more than x, then cfn(p, γ) and cfn(q, θ) are within π(x, y) of each other.^{4} The parameter y will roughly correspond to the amount by which the clocks have drifted relative to each other and x roughly indicates the message delay in communicating clock values. Typically, the parameter y dominates x. The quantity π(x, y) provides the bound on the skew δ_{S} immediately following resynchronization. For the precision to be truly enhanced, it is crucial for π(x, y) to be smaller than y.

Condition 10 (precision enhancement) Given any subset C of the N clocks with |C| ≥ N − F, and clocks p and q in C, then for any readings γ and θ satisfying the conditions

1. for any l in C, |γ(l) − θ(l)| ≤ x

2. for any l, m in C, |γ(l) − γ(m)| ≤ y

3. for any l, m in C, |θ(l) − θ(m)| ≤ y

there is a bound π(x, y), such that

|cfn(p, γ) − cfn(q, θ)| ≤ π(x, y)  (2.2.18)

The final condition of accuracy preservation bounds the distance between the value of cfn(p, θ) and the nonfaulty entries in θ. If t_{q}^{i} ≤ t_{p}^{i}, then accuracy preservation^{5} can be used to bound the difference between IC_{q}^{i+1}(t_{q}^{i+1}) and IC_{p}^{i}(t_{q}^{i+1}).

4Note that the order of arguments to π are reversed from their order in Schneider’s description [1].

5Footnote 7 in Schneider [1] explains the choice of the terms precision enhancement and accuracy preservation. ‘Precision’ is defined as the closeness with which a measurement can be reproduced, whereas ‘accuracy’ is the proximity of the measurement to the actual value being measured. The virtual clocks represent various measurements of real time.

The condition of precision enhancement characterizes the closeness of these measurements to each other. The condition of accuracy preservation can be seen as bounding the drift rate of the virtual clock with respect to real time.

Condition 11 (accuracy preservation) Given any subset C of the N clocks with |C| ≥ N − F, and clock readings θ such that for any l and m in C, the bound |θ(l) − θ(m)| ≤ x holds, there is a bound α(x) such that for any q in C

|cfn(p, θ) − θ(q)| ≤ α(x)  (2.2.19)

In addition to the conditions enumerated above, Schneider presents a condition called monotonicity that is actually not satisfied by several clock synchronization protocols. Fortunately, this condition turns out to be unnecessary in the derivation. The monotonicity condition asserts that if for each processor l, θ(l) ≥ γ(l), then cfn(p, θ) ≥ cfn(p, γ). The failure of the monotonicity condition for ICA is demonstrated in Section 2.4.

2.3 The Correctness Proof

The proof described below closely follows Schneider’s outline. A few of the details are different, mainly reflecting corrections or perceived improvements. These seemingly small revisions do, however, lead to drastic changes in the statements of many of the theorems. The details of the correctness proof are both conceptually and notationally complicated. The formal arguments are extremely delicate to carry out carefully and correctly due to the additional consideration of processor failure. The true difficulty of constructing watertight proofs may not be apparent in the descriptions below since they only capture the end result of a mechanical verification and not the tenuous intermediate steps. It would be extremely difficult for even the most diligent mathematician to correctly capture all the details of such proofs without machine assistance. One difficulty is the care that is needed to ensure that no assumptions are made regarding failed clocks. Schneider [1], for instance, asserts, “We make no assumptions about the behavior of clocks at faulty processors — not even that they can be modeled by functions.” The present formulation does not go as far as to avoid the use of functions to model the behavior of failed clocks but no constraints are placed on the values of these functions when a processor has failed. The use of functions does not seem to contradict any intuitive understanding of the physical behavior of failed clocks. The possibility of processor failure adds significantly to the complexity of the formalization as well as the proof.

The proof described in this section is itself a somewhat simplified rendering of the mechanically verified proof. The main difference is that in the mechanical proof, the faultiness of a processor is itself a time-varying property, i.e., processors can fail at any time. A brief overview is given below to provide an outline of the detailed proof. The words processor and clock are used interchangeably.

2.3.1 Overview

To establish the main result, Theorem 2.1.1, we must show that the skew, or absolute difference, between the readings of any two nonfaulty clocks p and q at time t, given by |V C_{p}(t) − V C_{q}(t)|, is bounded by a quantity δ. By the definition of V C in (2.1.4), this reduces to the following two cases:

1. When both clocks have been resynchronized for the i’th time but not for the (i + 1)’th time, i.e., if max(t_{p}^{i}, t_{q}^{i}) ≤ t < min(t_{p}^{i+1}, t_{q}^{i+1}), then the skew between IC_{p}^{i}(t) and IC_{q}^{i}(t) is bounded by δ, and

2. When only one clock, say q, has been resynchronized for the (i + 1)’th time, i.e., if t_{q}^{i+1} ≤ t < t_{p}^{i+1}, then the skew between IC_{p}^{i}(t) and IC_{q}^{i+1}(t) is bounded by δ.

For two nonfaulty clocks p and q, the time immediately following their i’th round of synchronization is max(t_{p}^{i}, t_{q}^{i}). The main step in the argument is to show that the skew between the readings IC_{p}^{i}(t) and IC_{q}^{i}(t) at time t = max(t_{p}^{i}, t_{q}^{i}), is bounded by a quantity δ_{S}. This is shown by induction on i, and employs the conditions of initial skew, translation invariance, and precision enhancement.

We now know that the clocks IC_{p}^{i} and IC_{q}^{i} start off no more than δ_{S} apart at max(t_{p}^{i}, t_{q}^{i}). By bounded interval and bounded drift, the skew between IC_{p}^{i}(t) and IC_{q}^{i}(t) does not increase by more than 2ρr_{max} in the interval max(t_{p}^{i}, t_{q}^{i}) ≤ t < min(t_{p}^{i}, t_{q}^{i}). Assuming that t_{q}^{i+1} ≤ t_{p}^{i+1}, then the restriction of accuracy preservation on the convergence function is used to bound the skew between IC_{p}^{i}(t_{q}^{i+1}) and IC_{q}^{i+1}(t_{q}^{i+1}). By bounded delay and bounded drift, the additional skew between the readings IC_{p}^{i}(t) and IC_{q}^{i+1}(t) over the interval t_{q}^{i+1} ≤ t < t_{p}^{i+1} is no more than 2ρβ. To obtain the final result, we need to constrain the quantities ρ, δ_{S}, r_{min}, r_{max}, and β so that the skew bounds derived over the various intervals are within δ. Schneider also shows that the restrictions of translation invariance, precision enhancement, and accuracy preservation, are satisfied by many of the known Byzantine fault tolerant convergence functions [1].

2.3.2 The Proof

The details of the proof of bounded skew are presented below. Let t_{p,q}^{i+1} denote max(t_{p}^{i}, t_{q}^{i}). The first major step in Schneider’s proof is to prove:

Theorem 2.3.1 There is a bound δ_{S} such that for synchronization round i and any two nonfaulty processors p and q

|IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ δ_{S}.  (2.3.20)

Proof. The proof of Theorem 2.3.1 is by induction on the round number i.

Base case: When i = 0, by (2.2.13) we have t_{p}^{0} = t_{q}^{0} = 0. Then by Definitions (2.1.3) and (2.1.1), IC_{p}^{0}(t_{p}^{0}) = P C_{p}(0) and IC_{q}^{0}(t_{p}^{0}) = P C_{q}(0). The condition of initial skew asserts |P C_{p}(0) − P C_{q}(0)| ≤ δ_{S}. Hence, |IC_{p}^{0}(0) − IC_{q}^{0}(0)| is also bounded by δ_{S}.

Induction case: The induction hypothesis asserts that for every pair of nonfaulty processors, l and m

|IC_{l}^{i}(t_{l,m}^{i}) − IC_{m}^{i}(t_{l,m}^{i})| ≤ δ_{S}.  (2.3.21)

The goal is to establish for any pair of nonfaulty processors p and q, that

|IC_{p}^{i+1}(t_{p,q}^{i+1}) − IC_{q}^{i+1}(t_{p,q}^{i+1})| ≤ δ_{S}.  (2.3.22)

Without loss of generality, assume that t_{q}^{i+1} precedes t_{p}^{i+1} so that t_{p,q}^{i+1} = t_{p}^{i+1}. Then Equation (2.1.6) yields

IC_{q}(t_{p}^{i+1}) = cfn(q, Θ_{q}^{i+1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}).  (2.3.23)

By Equation (2.1.5), we have

IC_{p}^{i+1}(t_{p}^{i+1}) = cfn(p, Θ_{p}^{i+1}).  (2.3.24)

The condition of translation invariance provides an estimate of IC_{q}^{i+1}(t_{p}^{i+1}) in terms of the convergence function cfn. With Θ_{q}^{i+1} for θ in Equation (2.2.17), we get

cfn(q, Θ_{q}^{i+1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})
= cfn(q, (λn: Θ_{q}^{i+1}(n) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}))). (2.3.25)

By (2.3.24) and (2.3.25), the bound on the initial skews can be rewritten as follows:

|IC_{q}^{i+1}(t_{p}^{i+1}) − IC_{p}^{i+1}(t_{p}^{i+1})|
= |cfn(q, (λn: Θ_{q}^{i+1}(n) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})))
−cfn(p, Θ_{p}^{i+1})|.  (2.3.26)

The right-hand side of (2.3.26) can be bounded by π(x, y) for some x and y using precision enhancement with (λn: Θ_{q}^{i+1}(n) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) for γ and Θ_{p}^{i+1} for θ. The set C in precision enhancement is taken to be the subset of nonfaulty clocks as permitted by bounded faults. The next few steps demonstrate that the remaining hypotheses of precision enhancement can be satisfied with these substitutions. To satisfy Hypothesis 1, we need to find an x such that for any nonfaulty l we can derive

|(Θ_{q}^{i+1}(l) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) − Θ_{p}^{i+1}(l)| ≤ x.

As shown below, the value 2ρβ + 2Λ can be substituted for x. By Equation (2.2.16), we easily get

|IC_{l}^{i}(t_{q}^{i+1}) − Θ_{q}^{i+1}(l)| ≤ Λ, and  (2.3.27)
|IC_{l}^{i}(t_{p}^{i+1}) − Θ_{p}^{i+1}(l)| ≤ Λ.  (2.3.28)

Note that t_{p}^{i+1} −t_{q}^{i+1} ≤ β by (2.2.12). So from Equation (2.1.3) and bounded drift, we have

|(IC_{l}^{i}(t_{q}^{i+1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) − IC_{l}^{i}(t_{p}^{i+1})|
= |(P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) − (IC_{l}^{i}(t_{p}^{i+1}) − IC_{l}^{i}(t_{q}^{i+1}))|
= |(P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) − (P C_{l}(t_{p}^{i+1}) − P C_{l}(t_{q}^{i+1}))|
≤ |(1 + ρ)(t_{p}^{i+1} − t_{q}^{i+1}) − (1 − ρ)(t_{p}^{i+1} − t_{q}^{i+1})|
= |2ρ(t_{p}^{i+1} − t_{q}^{i+1})|
≤ 2ρβ.  (2.3.29)

Putting together Equations (2.3.27), (2.3.28), and (2.3.29), we get the required inequality

|Θ_{q}^{i+1}(l) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}) − Θ_{p}^{i+1}(l)| ≤ 2ρβ + 2Λ.  (2.3.30)

The substitution 2ρβ + 2Λ for x thus satisfies Hypothesis 1 of precision enhancement.

The next step is to satisfy Hypotheses 2 and 3 of precision enhancement for the specified substitutions. For these, we need a y such that for any nonfaulty processors l and m, the following inequalities hold.

|(Θ_{q}^{i+1}(l) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) −
(Θ_{q}^{i+1}(m) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}))| ≤ y  (2.3.31)
|Θ_{p}^{i+1}(l) − Θ_{p}^{i+1}(m)| ≤ y  (2.3.32)

Since (2.3.31) can be simplified by cancellation, both (2.3.31) and (2.3.32) can derived by deriving a bound y such that for all nonfaulty clocks k, l, and m, we get

|Θ_{k}^{i+1}(l) − Θ_{k}^{i+1}(m)| ≤ y  (2.3.33)

First note that

|Θ_{k}^{i+1}(l) − Θ_{k}^{i+1}(m)|
≤ |Θ_{k}^{i+1}(l) − IC_{l}^{i}(t_{k}^{i+1})| + |IC_{l}^{i}(t_{k}^{i+1}) − IC_{m}^{i}(t_{k}^{i+1})| +
|Θ_{k}^{i+1}(m) − IC_{m}^{i}(t_{k}^{i+1})|  (2.3.34)

In (2.3.34), we know by Equation (2.2.16) that

|Θ_{k}^{i+1}(l) − IC_{l}^{i}(t_{k}^{i+1})| ≤ Λ and  (2.3.35)
|Θ_{k}^{i+1}(m) − IC_{m}^{i}(t_{k}^{i+1})| ≤ Λ  (2.3.36)

By the induction hypothesis (2.3.21), we get

|IC_{l}^{i}(t_{l,m}^{i}) − IC_{m}^{i}(t_{l,m}^{i})| ≤ δ_{S}.  (2.3.37)

We know by (2.2.15) that, t_{k}^{i+1} − t_{l,m}^{i} ≤ r_{max} + β. Then by (2.1.3), (2.2.10), and (2.3.37), we get

|IC_{l}^{i}(t_{k}^{i+1}) − IC_{m}^{i}(t_{k}^{i+1})| ≤ δ_{S} + 2ρ(r_{max} + β).  (2.3.38)

Combining Equations (2.3.34), (2.3.35), (2.3.36), and (2.3.38), we get

|Θ_{k}^{i+1}(l) − Θ_{k}^{i+1}(m)| ≤ δ_{S} + 2ρ(r_{max} + β) + 2Λ.  (2.3.39)

So the expression δ_{S} + 2ρ(r_{max} + β) + 2Λ is the required bound y satisfying both Hypotheses 2 and 3 of precision enhancement.

If we now choose δ_{S} so that

π(2Λ + 2βρ, δ_{S} + 2ρ(r_{max} + β) + 2Λ) ≤ δ_{S},  (2.3.40)

then the conclusion of precision enhancement along with Equation (2.1.6) ensures that

|IC_{p}^{i+1}(t_{p}^{i+1}) − IC_{q}^{i+1}(t_{p}^{i+1})| ≤ δ_{S}

to complete the proof of Theorem 2.3.1.

We have now shown that for any pair of nonfaulty processors p and q, the skew between their clock readings at t_{p,q}^{i}, given by |IC_{p}^{i}(t_{p,q}^{i})−IC_{q}^{i}(t_{p,q}^{i})|, does not exceed δ_{S}. The next step is to show that for any i, the clock skew between t_{p,q}^{i} and t_{p,q}^{i+1}, is bounded.

Theorem 2.3.2 For any two nonfaulty clocks p, q, and t_{p,q}^{i} ≤ t < t_{p,q}^{i+1},

|V C_{p}(t) − V C_{q}(t)| ≤ δ.  (2.3.41)

Proof. Assume without loss of generality that t_{q}^{i+1} ≤ t_{p}^{i+1}. The proof has two cases according to whether t_{p,q}^{i} ≤ t < t_{q}^{i+1} or t_{q}^{i+1} ≤ t < t_{p}^{i+1}.

Case 1: Assuming t_{p,q}^{i} ≤ t < t_{q}^{i+1}, from bounded interval we get t−t_{p,q}^{i} ≤ r_{max}. By Equation (2.1.4), it is clear that for t in this interval V C_{p}(t) = IC_{p}^{i}(t) and V C_{q}(t) = IC_{q}^{i}(t). Then by (2.2.10) and (2.1.3), it follows that

|V C_{p}(t) − V C_{q}(t)| ≤ |V C_{p}(t_{p,q}^{i}) − V C_{q}(t_{p,q}^{i})| + 2ρr_{max}.  (2.3.42)

Recall that Theorem 2.3.1 yields

|V C_{p}(t_{p,q}^{i}) − V C_{q}(t_{p,q}^{i})| ≤ δ_{S}.  (2.3.43)

Combining Equations (2.3.42) and (2.3.43), we have

|V C_{p}(t) − V C_{q}(t)| ≤ δ_{S} + 2ρr_{max}.  (2.3.44)

The bound δ should therefore be chosen so that

δ_{S} + 2ρr_{max} ≤ δ.  (2.3.45)

Case 2: Assuming t_{q}^{i+1} < t < t_{p,q}^{i+1}. In this interval, V C_{q}(t) = IC_{q}^{i+1}(t), whereas V C_{p}(t) = IC_{p}^{i}(t). The strategy here is to bound the skew at t_{q}^{i+1} and then compute the additional quantity by which the clocks can drift apart in the given interval. By Equations (2.1.5) and (2.1.4), we have

|V C_{p}(t_{q}^{i+1}) − V C_{q}(t_{q}^{i+1})| = |IC_{p}^{i}(t_{q}^{i+1}) − cfn(q, Θ_{q}^{i+1})|.  (2.3.46)

We now need to use the condition of accuracy preservation with C as the subset of nonfaulty processors as allowed by bounded faults. To satisfy the hypothesis of accuracy preservation, we need a bound x such that, for any pair of nonfaulty clocks l and m,

|Θ_{q}^{i+1}(l) − Θ_{q}^{i+1}(m)| ≤ x.  (2.3.47)

The next few steps are similar to those required to establish Hypotheses 2 and 3 of precision enhancement. By Equation (2.2.16), we have

|Θ_{q}^{i+1}(l) − IC_{l}^{i}(t_{q}^{i+1})| ≤ Λ  (2.3.48)
|Θ_{q}^{i+1}(m) − IC_{m}^{i}(t_{q}^{i+1})| ≤ Λ.  (2.3.49)

By Equation (2.2.15), t_{q}^{i+1} − t_{l,m}^{i} ≤ r_{max} + β holds. Theorem 2.3.1 and (2.2.10) can now be applied to get

|IC_{l}^{i}(t_{q}^{i+1}) − IC_{m}^{i}(t_{q}^{i+1})| ≤ δ_{S} + 2ρ(r_{max} + β).  (2.3.50)

Letting x be δ_{S} + 2ρ(r_{max} + β) + 2Λ, and substituting p for q and q for p in accuracy preservation, we can combine Equations (2.3.48), (2.3.49), and (2.3.50), to get

|cfn(q, Θ_{q}^{i+1}) − Θ_{q}^{i+1}(p)| ≤ α(δ_{S} + 2ρ(r_{max} + β) + 2Λ).  (2.3.51)

Since Equation (2.2.16) yields |Θ_{q}^{i+1}(p) − IC_{p}^{i}(t_{q}^{i+1})| ≤ Λ, it follows from Equations (2.3.51) and (2.3.46), that

|V C_{p}(t_{q}^{i+1}) − V C_{q}(t_{q}^{i+1})|
= |IC_{p}^{i}(t_{q}^{i+1}) − cfn(q, Θ_{q}^{i+1})|
≤ α(δ_{S} + 2ρ(r_{max} + β) + 2Λ) + Λ.  (2.3.52)

Having bounded the skew at t_{q}^{i+1}, we can bound the skew over the interval t_{q}^{i+1} ≤ t < t_{p}^{i+1}, by observing that t_{p}^{i+1} − t_{q}^{i+1} ≤ β by (2.2.12), and applying Equation (2.2.10) to derive the inequality,

|V C_{p}(t) − V C_{q}(t)| ≤ α(δ_{S} + 2ρ(r_{max} + β) + 2Λ) + Λ + 2ρβ. (2.3.53)

Therefore δ has to be chosen to satisfy

α(δ_{S} + 2ρ(r_{max} + β) + 2Λ) + Λ + 2ρβ ≤ δ.  (2.3.54)

This completes both cases of the proof of Theorem 2.3.2.

Theorem 2.3.2 forms the induction step in the proof of the following theorem.

Theorem 2.3.3 For any two nonfaulty clocks p, q, and t < t_{p,q}^{i}

|V C_{p}(t) − V C_{q}(t)| ≤ δ  (2.3.55)

Proof. The proof is by straightforward induction over i. When i = 0, the antecedent fails since t_{p,q}^{i} = 0. The induction hypothesis asserts that for t < t_{p,q}^{i}, the quantity |V C_{p}(t) − V C_{q}(t)| does not exceed δ. The induction conclusion requires showing that δ bounds |V C_{p}(t) − V C_{q}(t)| even when t < t_{p,q}^{i+1}. We observe that either t < t_{p,q}^{i}, in which case the conclusion follows from the induction hypothesis, or, t_{p,q}^{i} ≤ t < t_{p,q}^{i+1}, and the conclusion easily follows from Theorem 2.3.2.

One small step remains in the proof of bounded skew from Theorem 2.3.3.

Theorem 2.3.4 For any t > 0 and nonfaulty processors p and q, there is an i such that

t < t_{p,q}^{i}.

Proof. By bounded interval, 0 < r_{min} ≤ t_{p}^{j+1} − t_{p}^{j}. Thus, t_{p}^{j+1} > jr_{min}. If we let i be ⌈t/r_{min}⌉ + 1, then t_{p}^{i} > t.

The main result, Theorem 2.1.1, easily follows from the Theorems 2.3.3 and 2.3.4.

We take note of the various conditions on δ and δ_{S}^{6}:

1. π(2Λ + 2βρ, δ_{S} + 2ρ(r_{max} + β) + 2Λ) ≤ δ_{S}, by 2.3.40.

2. δ_{S} + 2ρr_{max} ≤ δ, by 2.3.45

3. α(δ_{S} + 2ρ(r_{max} + β) + 2Λ) + Λ + 2ρβ ≤ δ, by 2.3.54

This concludes the informal presentation of the proof.

6Note that these conditions are significantly different from those derived by Schneider [1] due to various inaccuracies that have been corrected in the mechanical proof.

2.4 ICA as an instance of Schneider’s scheme

The egocentric mean function which is used as a convergence function in the Interactive Convergence Algorithm of Lamport and Melliar-Smith [3] can be shown to satisfy Schneider’s conditions of translation invariance, precision enhancement, and accuracy preservation.

With the interactive convergence algorithm, the convergence function cfn_{I} takes the egocentric mean of p’s estimate of the readings of the N clocks numbered from 0 to N − 1, i.e., any readings that are more than Δ away from p’s own reading are replaced by p’s own reading. This yields the definition

cfn_{I}(p, θ) = \frac{∑_{l=0}^{N−1} fix_{p}(θ(l))}{N}  (2.4.56)

where

fix_{p}(x) = \{ \begin{matrix}x & if |x − θ(p)| ≤ Δ \\ θ(p) & otherwise. \end{matrix}

Translation invariance follows from the observation that

fix_{p}((λl: θ(l) + t)(q)) = fix_{p}(θ(q)) + t  (2.4.57)

and

\frac{∑_{l=0}^{N−1}(θ(l) + t)}{N} = \frac{∑_{l=0}^{N−1}(θ(l))}{N} + t  (2.4.58)

To demonstrate precision enhancement, we start with a set of processors C of cardinality |C| greater than N − F. Let f be N − |C|. The hypotheses for precision enhancement are that for any l and m in C,

|γ(l) − θ(l)| ≤ x  (2.4.59)
|γ(l) − γ(m)| ≤ y  (2.4.60)
|θ(l) − θ(m)| ≤ y.  (2.4.61)

We need to determine π(x, y) so that for any p and q in C, we get

|cfn_{I}(p, γ) − cfn_{I}(q, θ)| ≤ π(x, y).  (2.4.62)

This difference can be rewritten as

|\frac{∑_{l=0}^{N−1} fix_{p}(γ(l))}{N} − \frac{∑_{l=0}^{N−1} fix_{q}(θ(l))}{N}|

which is no greater than

\frac{∑_{l=0}^{N−1} |fix_{p}(γ(l)) − fix_{q}(θ(l))|}{N}.

This in turn can be rewritten as

\frac{∑_{l∈C} |fix_{p}(γ(l)) − fix_{q}(θ(l))|}{N} + \frac{∑_{l∉C} |fix_{p}(γ(l)) − fix_{q}(θ(l))|}{N}.

Assuming y ≤ Δ and l ∈ C, we get fix_{p}(γ(l)) to be γ(l) and fix_{q}(θ(l)) to be θ(l), so that

|fix_{p}(γ(l)) − fix_{q}(θ(l))| ≤ x

and hence,

\frac{∑_{l∈C} |fix_{p}(γ(l)) − fix_{q}(θ(l))|}{N} ≤ \frac{(N − f)x}{N}.

For l ∉ C, the difference

|fix_{p}(γ(l)) − fix_{q}(θ(l))| ≤ 2Δ + |γ(p) − θ(q)| ≤ 2Δ + x + y

and hence

\frac{∑_{l∉C} |fix_{p}(γ(l)) − fix_{q}(θ(l))|}{N} ≤ \frac{2fΔ + fx + fy}{N} .

We thus get, when y ≤ Δ, that

π(x, y) = \frac{(N − f)x}{N} + \frac{2fΔ + fx + fy}{N} .  (2.4.63)

In the typical situation when the egocentric mean is computed, the quantity x representing the reading error is negligible, and y representing the clock skew is bounded by Δ. Since the skew following synchronization should be smaller than Δ, we can see that in Equation (2.4.63), the number of failed processors f should be below N/3. Though the derivation of π(x, y) for the case when y > Δ is carried out in the machine proof, it is not essential since in practice, y will not exceed Δ

To show that cfn_{I} satisfies accuracy preservation, it is sufficient to observe that if all the nonfaulty clocks are within x of each other, then the nonfaulty clocks can cause the egocentric mean to be at most (N − f)x/N away from any nonfaulty clock. The faulty clocks can cause the egocentric mean to be up to f × (x + Δ)/N away from a good clock. The total thus yields

α(x) = x + \frac{fΔ}{N}.

The final step is to demonstrate the failure of the monotonicity condition for ICA. The monotonicity condition mentioned at the end of Section 2.2 asserts that if for each processor l, θ(l) ≥ γ(l), then cfn(p, θ) ≥ cfn(p, γ). The key reason for the failure of the monotonicity condition is that if some readings in γ were ignored because they were more than Δ below γ(p) but were increased in θ so that they were no longer ignored, then cfn(p, θ) could effectively be smaller than cfn(p, γ) even though for every l, θ(l) ≥ γ(l). More specifically, let θ(p) = γ(p). Observe now that if there is some l such that θ(l) + Δ < θ(p), but with γ(p) > γ(l) ≥ γ(p) − Δ, then fix_{p}(θ(l)) > fix_{p}(γ(l)) holds. So, it is possible to have fix_{p}(θ(l)) > fix_{p}(γ(l)), even though we have θ(l) < γ(l).

For the mechanical verification of ICA as an instance of Schneider’s protocol, we have verified the constraints, i.e., translation invariance, precision enhancement, and accuracy preservation, hold for the egocentric mean taken as a convergence function. We have not yet instantiated the quantities r_{min}, r_{max} and β, nor verified the conditions of bounded interval, bounded delay and nonoverlap, since these depend on specific implementation choices. It would also be useful to mechanically verify various other Byzantine fault tolerant clock synchronization algorithms to be instances of Schneider’s scheme.

The Verification of Schneider’s Protocol using

EHDM

The outline in Chapter 2 was adapted from Schneider’s description but differs from his presentation in many of the details. The mechanized formalization using Ehdm follows the informal description in Chapter 2 fairly closely. We illustrate the highlights of the machine proof below and indicate the correspondence to the informal description. Details regarding the language and capabilities of Ehdm are contained in the Ehdm tutorial document [2].

3.1 The Clock Assumptions

This section contains the Ehdm formalization of the conditions axiomatizing the behavior of clocks. These axioms are contained in a module labeled clockassumptions that is listed in Appendix B starting from page 47. Figure 3.1 contains the type declarations for some of the variables and constants

used in clockassumptions. The clockassumptions module makes use of

the module arith, which contains the basic arithmetic facts, and countmod, which introduces a counting function. Nonfaultiness is expressed by the predicate correct.

The first few axioms express various minor constraints on the constants as shown in Figure 3.2.

The axioms constraining the physical behavior of the clock appear in Figure 3.3. Since we require the initial skew bound μ to not exceed δ_{S},

clockassumptions: Module

Using arith, countmod

Exporting all with countmod, arith

Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time X, Y, Z, R, S, T: Var Clocktime γ, θ: Var function[process → Clocktime] δ, μ, ρ, r_{min}, r_{max}, β, Λ: number P C_{⋆1}(⋆2), V C_{⋆1}(⋆2): function[process, time → Clocktime] t_{⋆1}^{⋆2}: function[process, event → time] Θ_{⋆1}^{⋆2}: function[process, event → function[process → Clocktime]] IC_{⋆1}^{⋆2}(⋆3): function[process, event, time → Clocktime] correct: function[process, time → bool] cfn: function[process, function[process → Clocktime] → Clocktime] π: function[Clocktime, Clocktime → Clocktime] α: function[Clocktime → Clocktime]

Figure 3.1: Declarations from module clockassumptions

delta 0: Axiom δ ≥ 0

mu 0: Axiom μ ≥ 0

rho 0: Axiom ρ ≥ 0

rho 1: Axiom ρ < 1

rmin 0: Axiom r_{min} > 0

rmax 0: Axiom r_{max} > 0

beta 0: Axiom β ≥ 0

lamb 0: Axiom Λ ≥ 0

Figure 3.2: Constants in module clockassumptions

axiom init essentially corresponds to initial skew. Axiom correct closed asserts that a failed processor never recovers. Axioms rate 1 and rate 2 together express the bounded drift condition. The axioms rts0 and rts1 capture the bounded interval condition. These axioms look strange because the variable t, needed to properly capture the correctness condition, appears in them but not in bounded interval. Most of the obvious ways of stating these axioms are either too restrictive or wrong. The axiom rts2 captures bounded delay, and synctime 0 is just initial synchronization. The condition of nonoverlap appears as an antecedent to the concluding theorem rather than as an axiom. In the LaTEX format below, multiplication is represented by ∗ as well as ⋆. These are synonymous, but the latter represents the uninterpreted form of multiplication whereas the former is interpreted by the linear arithmetic decision procedures of Ehdm.

The definitions of the virtual clock and the interval clock in terms of the physical clock appear in Figure 3.4. These correspond to (2.1.1), (2.1.4), and (2.1.3), respectively.

The conditions on the convergence function appear in Figure 3.5. The axiom Readerror corresponds to the condition reading error. The axiom correct count corresponds to bounded faults. The remaining correspondences should be self-evident.

Some of the definitions and lemmas from the module clockassumptions have been omitted from this discussion.

init: Axiom correct(p, 0) ⊃ P C_{p}(0) ≥ 0 ∧ P C_{p}(0) ≤ μ correct closed: Axiom s ≥ t ∧ correct(p, s) ⊃ correct(p, t) rate 1: Axiom correct(p, s) ∧ s ≥ t ⊃ P C_{p}(s) − P C_{p}(t) ≤ (s − t) ⋆ (1 + ρ) rate 2: Axiom correct(p, s) ∧ s ≥ t ⊃ P C_{p}(s) − P C_{p}(t) ≥ (s − t) ⋆ (1 − ρ) rts0: Axiom correct(p, t) ∧ t ≤ t_{p}^{i+1} ⊃ t − t_{p}^{i} ≤ r_{max} rts1: Axiom correct(p, t) ∧ t ≥ t_{p}^{i+1} ⊃ t − t_{p}^{i} ≥ r_{min} rts 0: Lemma correct(p, t_{p}^{i+1}) ⊃ t_{p}^{i+1} − t_{p}^{i} ≤ r_{max} rts 1: Lemma correct(p, t_{p}^{i+1}) ⊃ t_{p}^{i+1} − t_{p}^{i} ≥ r_{min} rts2: Axiom correct(p, t) ∧ t ≥ t_{q}^{i} + β ∧ correct(q, t) ⊃ t ≥ t_{p}^{i} rts 2: Axiom correct(p, t_{p}^{i}) ∧ correct(q, t_{q}^{i}) ⊃ t_{p}^{i} − t_{q}^{i} ≤ β synctime 0: Axiom t_{p}^{0} = 0

Figure 3.3: Physical clock axioms in module clockassumptions

VClock defn: Axiom

correct(p, t) ∧ t ≥ t_{p}^{i} ∧ t < t_{p}^{i+1} ⊃ V C_{p}(t) = IC_{p}^{i}(t) Adj: function[process, event → Clocktime] =

( λ p, i: ( if i > 0 then cfn(p, Θ_{p}^{i}) − P C_{p}(t_{p}^{i}) else 0 end if)) IClock defn: Axiom correct(p, t) ⊃ IC_{p}^{i}(t) = P C_{p}(t) + Adj(p, i)

Figure 3.4: Clock definitions in module clockassumptions

Readerror: Axiom correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ |Θ_{p}^{i+1}(q) − IC_{q}^{i}(t_{p}^{i+1})| ≤ Λ

translation invariance: Axiom X ≥ 0 ⊃ cfn(p, ( λ p_{1} → Clocktime: γ(p_{1}) + X)) = cfn(p, γ) + X

ppred: Var function[process → bool] maxfaults: process okay Readpred: function[function[process → Clocktime], Clocktime,

function[process → bool] → bool] =

( λ γ, Y, ppred: ( ∀ l, m: ppred(l) ∧ ppred(m) ⊃ |γ(l) − γ(m)| ≤ Y)) okay pairs: function[function[process → Clocktime],

function[process → Clocktime], Clocktime, function[process → bool] → bool] =

( λ γ, θ, X, ppred: ( ∀ p_{3}: ppred(p_{3}) ⊃ |γ(p_{3}) − θ(p_{3})| ≤ X)) N: process

N 0: Axiom N > 0

N maxfaults: Axiom maxfaults ≤ N

precision enhancement ax: Axiom

count(ppred, N) ≥ N − maxfaults

∧ okay Readpred(γ, Y, ppred) ∧ okay Readpred(θ, Y, ppred)

∧ okay pairs(γ, θ, X, ppred) ∧ ppred(p) ∧ ppred(q) ⊃ |cfn(p, γ) − cfn(q, θ)| ≤ π(X, Y)

correct count: Axiom count(( λ p: correct(p, t)), N) ≥ N − maxfaults

accuracy preservation ax: Axiom

okay Readpred(γ, X, ppred)

∧ count(ppred, N) ≥ N − maxfaults ∧ ppred(p) ∧ ppred(q) ⊃ |cfn(p, γ) − γ(q)| ≤ α(X)

Figure 3.5: Conditions on Logical Clocks in module clockassumptions

agreement: Lemma β ≤ r_{min}

∧ μ ≤ δ_{S} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}

∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ

∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ

∧ t ≥ 0 ∧ correct(p, t) ∧ correct(q, t)
⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ

Figure 3.6: Main Theorem in module lemma final

okaymaxsync: function[nat, Clocktime → bool] =

( λ i, X: ( ∀ p, q:

correct(p, t_{p,q}^{i}) ∧ correct(q, t_{p,q}^{i})
⊃ |IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ X))

lemma 2: Lemma β ≤ r_{min}

∧ μ ≤ X ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ⊃ okaymaxsync(i, X)

Figure 3.7: Skew immediately following resynchronization from module readbounds

3.2 The Proof Highlights

The conclusion corresponding to Theorem 2.1.1 is the theorem agreement that appears in the module lemma final listed at page 63 of Appendix B. This theorem is displayed in Figure 3.6. It should be compared to the statement of Theorem 2.1.1 (page 8) and to the conditions at the end of Section 2.3.2 (page 21). The axioms, definitions, and lemmas used, whether in a direct or indirect manner, in the proof of agreement are analyzed in Appendix C.1 to ensure that all proof obligations have been discharged. Both the process and the result of checking these dependencies are part of what is termed the proof chain analysis.

The verified version of Theorem 2.3.1 is given in Figure 3.7 extracted from the module readbounds listed at page 55 of Appendix B.

The verified version of Theorem 2.3.2 appears in Figure 3.8 which is taken from the module lemma3 listed at page B of Appendix B. The expression t_{(p⇑q)[i]}^{i} is an alternative notation for t_{p,q}^{i} since (p ⇑ q)[i] represents p if t_{p}^{i} ≥ t_{q}^{i},

okayClocks: function[process, process, nat → bool] =

( λ p, q, i: ( ∀ t:

t ≥ 0 ∧ t < t_{(p⇑q)[i]}^{i} ∧ correct(p, t) ∧ correct(q, t)
⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ))

lemma3 3: Lemma β ≤ r_{min}

∧ μ ≤ δ_{S} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}

∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ

⊃ okayClocks(p, q, i)

Figure 3.8: Skew up to ith resynchronization from module lemma3

and q otherwise.

The Ehdm definition of the egocentric mean function is given by icalg in Figure 3.9.

The verification of the translation invariance, precision enhancement, and accuracy preservation properties of the egocentric mean function is presented in Figure 3.10. The proof chain analyses for these theorems appear in Appendices C.2, C.3, and C.4.

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time X, Y, Z, R, S, T: Var Clocktime fun, γ, θ: Var function[process → Clocktime] ppred, ppred1, ppred2: Var function[process → bool] sigma size: function[function[process → Clocktime], process → process] =

( λ fun, i: i) sigma: function[function[process → Clocktime], process → Clocktime] =

( λ fun, i: ( if i > 0 then fun(i − 1) + sigma(fun, i − 1) else 0 end if)) by sigma size

fix: function[Clocktime, Clocktime, Clocktime → Clocktime] =

( λ X, Y, Z: ( if |Y − Z| ≤ X then Y else Z end if)) iconv: function[process, function[process → Clocktime], Clocktime

→ Clocktime] =

( λ p, fun, Y: sigma(( λ q: fix(Y, fun(q), fun(p))), N)) icalg: function[process, function[process → Clocktime], Clocktime

→ Clocktime] = ( λ p, fun, Y: iconv(p, fun, Y)/N)

Figure 3.9: Egocentric mean from module ica

ica translation invariance: Lemma N > 0 ⊃ icalg(p, ( λ q: fun(q) + X), Y) = icalg(p, fun, Y) + X

icalg precision enhancement: Lemma

ppred(p) ∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay pairs(fun1, fun2, X, ppred)

∧ okay Readpred(fun1, Z, ppred) ∧ okay Readpred(fun2, Z, ppred) ⊃ icalg(p, fun1, Δ) − icalg(q, fun2, Δ) ≤ icalg Pi(X, Z)

icalg accuracy preservation: Lemma

ppred(p) ∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay Readpred(fun, X, ppred) ⊃ |icalg(p, fun, Δ) − fun(q)|

≤ ((N − maxfaults) ⋆ X + maxfaults ⋆ (X + Δ))/N

Figure 3.10: Properties of egocentric mean from modules ica, ica3, and ica4

Conclusions

Rigorously proving the correctness of distributed protocols is an extremely difficult task, with or without mechanical assistance. Fault-tolerant clock synchronization is an excellent example of a problem where the algorithms, though often simple, are not at all easily verified. In such cases, it is extremely important to have certain organizing principles which capture the common features of the various protocols with convincing generality. Schneider’s schema for Byzantine clock synchronization provides such principles to unify the presentation and proofs of a number of different protocols. Schneider starts with certain axioms constraining the behaviors of clocks, the selection of synchronization times, and the convergence functions. He uses these constraints to derive a bound on the skew between any two nonfaulty clocks. It is worth noting for the discussion below that Schneider’s work is described in an unpublished technical report that has not had the benefit of widespread examination.

The formalization here revises a few details from Schneider’s presentation. Schneider’s notion of a global signal to trigger resynchronization has been dropped because such a notion is difficult to instantiate for many protocols. Though the quantities r_{max} and r_{min} have a different meaning from Schneider’s, these differences ought not to matter in any of the bounds derived. For instance, r_{max} here bounds t_{p}^{i+1} − t_{p}^{i}, but Schneider’s bound on this quantity would be r_{max} + β. However, the significant quantity in the proof is the difference t_{p}^{i+1} − t_{q}^{i} and the bound on this quantity is r_{max} + β in either formalization. In other words, Schneider’s bounds on δ and δ_{S} ought to have been the same as those derived in Section 2.3.2, but there were certain minor errors of algebra in his proofs and some latitude in his argument. The derivation we present is extremely tight, given the structure of the proof. Schneider’s monotonicity condition is avoided in the proofs here. This condition is used heavily by Schneider in his arguments, but it actually turns out to be false for many protocols. The statement of accuracy preservation is also slightly different here from that of Schneider. Schneider also presents the proof for the case of continuous resynchronization which is not handled here.

The initial proof using Ehdm took about a month. The proof has been considerably revised and improved since that first effort. Verifying that the egocentric mean function of ICA satisfied the conditions of translation invariance, accuracy preservation, and precision enhancement, took about two weeks. The Ehdm modules are listed in Appendix B. The proof involves 182 theorems or lemmas. A rerun of the entire proof on a SUN 3/470 takes 3227 CPU seconds (see Appendix A).

An early difficulty in the verification attempt was in arriving at a satisfactory formalization that suitably revised the one from Schneider. The proper treatment of failure proved to be a pervasive and important difficulty. Unlike other similar informal and machine-verified proofs, our formalization was careful to permit processors to fail at any time. Rushby and von Henke [8], for example, regard processors as nonfaulty in an interval between synchronizations only if they have been nonfaulty for the entire interval. This is an adequate model for most practical purposes but it is less general because it does not distinguish between processors that may have failed at the beginning of the interval and those that failed at the very end of an interval. An even coarser model, and the one unwittingly used in most informal presentations of clock synchronization, is one where the only correct processors are those that never fail. In some sense, this is acceptable since often the only significant requirement is that a sufficient number of processors be nonfaulty at any given time. However, such a formalization allows no conclusion to be drawn regarding a processor which has yet to fail but does eventually fail, since it is regarded as always having been faulty.

To illustrate the circularity lurking in the formalization of time and failure, consider the following seemingly natural formalization of nonfaultiness in an interval. Suppose that a processor is described as nonfaulty for an interval if it functions normally through the end of the interval. Let the end of the interval be the time at which the nonfaulty clocks indicate a certain reading or have performed a certain operation such as resetting their readings. Suppose, for example, that the end of the interval is given by the time t when the slowest of the “nonfaulty” clocks p reads T. Now suppose that p fails exactly at t. Then clearly the end of the interval is earlier than t, but at any point earlier than t, processor p is nonfaulty and has yet to read T. This “natural” definition of the end of an interval thus yields a contradiction. Many similar problem arose frequently in attempting to set down the clock axioms. The most natural statement of these axioms often turned out to be either wrong or too restrictive. It is also important to observe that these problems would never have been noticed in most informal presentations since these details, though important, would have been largely ignored.

The most useful features of Ehdm for this verification were the decision procedures for linear integer and real inequalities and equalities. The informal proof is of course replete with long chains of inequality reasoning, and the decision procedures handled those steps in a fairly mechanical manner. The higher-order features of the language were also used to formalize the conditions of translation invariance, precision enhancement, and accuracy preservation, but these were not essential. These could have also been formalized in terms of lists or finite arrays. The language of Ehdm underwent a number of improvements during this project, and not all of these improvements have been exploited in this proof. The use of predicate subtypes would have permitted the introduction of types corresponding to the non-negative and the positive numbers.

Fault-tolerant distributed protocols are sufficiently delicate to warrant careful, formal, mechanized analysis. Schneider’s presentation of Byzantine fault-tolerant clock synchronization protocols provides a valuable mathematical framework for such an analysis. The machine-checked proof of Schneider’s protocol led to a more precise formulation of the protocol and a more closely reasoned proof. It is inconceivable that the same degree of logical rigor and accuracy could be achieved without computational assistance.

Bibliography

[1] Schneider, Fred B.: Understanding Protocols for Byzantine Clock Synchronization. Department of Computer Science, Cornell University, Technical Report 87-859, Ithaca, NY, August 1987.

[2] Rushby, John; von Henke, Friedrich; and Owre, Sam: An Introduction to Formal Specification and Verification Using Ehdm. Computer Science Laboratory, SRI International, Technical Report SRI-CSL-91-2, Menlo Park, CA, Feb. 1991.

[3] Lamport, L.; and Melliar-Smith, P.M.: Synchronizing Clocks in the Presence of Faults. Journal of the ACM, vol. 32, no. 1, January 1985, pp. 52–78.

[4] Garman, J. R.: The “Bug” Heard ’Round The World. ACM SIGSOFT Software Engineering Notes, vol. 6, no. 5, October 1981, pp. 3–10.

[5] Anonymous: Reprogramming Capability Proves Key to Extending Voyager 2’s Journey. Aviation Week and Space Technology, August 7, 1989, pp. 72.

[6] Butler, Ricky W.: A Survey of Provably Correct Fault-Tolerant Clock Synchronization Techniques. NASA TM-100553, February 1988.

[7] Lamport, Leslie; Shostak, Robert; and Pease, Marshall: The Byzantine Generals Problem. ACM TOPLAS, vol. 4, no. 3, July 1982, pp. 382–401.

[8] Rushby, John; and von Henke, Friedrich: Formal Verification of a Fault Tolerant Clock Synchronization Algorithm. NASA CR-4239, June 1989.

Appendix A

Proof Summary

The proof summary is the result of executing a command to attempt to prove all the proof declarations in the context. The only failures are in the automatically generated proof declarations for the type correctness conditions (tcc). The time given below is the running time on a SUN 3/470.

Proof summaries for modules on using chain of module top
Proof summaries for modules on using chain of module top
Module division_tcc:      7 successful proofs,  0 failures,  0 errors
Module tcc_proofs_tcc:    2 successful proofs,  1 failure,   0 errors
Module ica3_tcc:          0 successful proofs,  3 failures,  0 errors
Module ica4_tcc:          0 successful proofs,  2 failures,  0 errors
Module ica_tcc:           1 successful proof,   2 failures,  0 errors
Module lemma_final_tcc:   0 successful proofs,  5 failures,  0 errors
Module countmod_tcc:      3 successful proofs,  2 failures,  0 errors
Module tcc_proofs:       14 successful proofs,  0 failures,  0 errors
Module ica3:              8 successful proofs,  0 failures,  0 errors
Module ica2:             20 successful proofs,  0 failures,  0 errors
Module ica:               6 successful proofs,  0 failures,  0 errors
Module ica4:              8 successful proofs,  0 failures,  0 errors
Module basics:           25 successful proofs,  0 failures,  0 errors
Module readbounds:       12 successful proofs,  0 failures,  0 errors
Module lemma3:           24 successful proofs,  0 failures,  0 errors
Module countmod:         no proofs
Module clockassumptions:  9 successful proofs,  0 failures,  0 errors
Module lemma_final:       5 successful proofs,  0 failures,  0 errors
Module absmod:           15 successful proofs,  0 failures,  0 errors
Module division:         11 successful proofs,  0 failures,  0 errors

Module multiplication:   11 successful proofs,  0 failures,  0 errors
Module arith:            no proofs
Module top:               1 successful proof,   0 failures,  0 errors
Totals:                  182 successful proofs,  15 failures,   0 errors

Total time: 3227 seconds.

Appendix B

The Complete EHDM Proof

Note that the modules ending with tcc are automatically generated during type checking. The proofs declared in these modules may not succeed, but all the automatically generated theorems have been proved as illustrated by the completeness of the proof chain analyses in Appendix C.

multiplication: Module

Exporting all Theory

x, y, z, x_{1}, y_{1}, z_{1}, x_{2}, y_{2}, z_{2}: Var number ⋆1 ⋆ ⋆2: function[number, number → number] = ( λ x, y: (x ∗ y)) mult ldistrib: Lemma x ⋆ (y + z) = x ⋆ y + x ⋆ z mult ldistrib minus: Lemma x ⋆ (y − z) = x ⋆ y − x ⋆ z mult rident: Lemma x ⋆ 1 = x mult lident: Lemma 1 ⋆ x = x distrib: Lemma (x + y) ⋆ z = x ⋆ z + y ⋆ z distrib minus: Lemma (x − y) ⋆ z = x ⋆ z − y ⋆ z mult non neg: Axiom ((x ≥ 0 ∧ y ≥ 0) ∨ (x ≤ 0 ∧ y ≤ 0)) ⇔ x ⋆ y ≥ 0 mult pos: Axiom ((x > 0 ∧ y > 0) ∨ (x < 0 ∧ y < 0)) ⇔ x ⋆ y > 0 mult com: Lemma x ⋆ y = y ⋆ x pos product: Lemma x ≥ 0 ∧ y ≥ 0 ⊃ x ⋆ y ≥ 0 mult leq: Lemma z ≥ 0 ∧ x ≥ y ⊃ x ⋆ z ≥ y ⋆ z mult leq 2: Lemma z ≥ 0 ∧ x ≥ y ⊃ z ⋆ x ≥ z ⋆ y mult l0: Axiom 0 ⋆ x = 0 mult gt: Lemma z > 0 ∧ x > y ⊃ x ⋆ z > y ⋆ z

Proof

mult gt pr: Prove mult gt from

mult pos {x ← x − y, y ← z}, distrib minus distrib minus pr: Prove distrib minus from

mult ldistrib minus {x ← z, y ← x, z ← y}, mult com {x ← x − y, y ← z}, mult com {y ← z}, mult com {x ← y, y ← z} mult leq 2 pr: Prove mult leq 2 from

mult ldistrib minus {x ← z, y ← x, z ← y},

mult non neg {x ← z, y ← x − y} mult leq pr: Prove mult leq from

distrib minus, mult non neg {x ← x − y, y ← z} mult com pr: Prove mult com from ⋆1 ⋆ ⋆2 , ⋆1 ⋆ ⋆2 {x ← y, y ← x} pos product pr: Prove pos product from mult non neg mult rident proof: Prove mult rident from ⋆1 ⋆ ⋆2 {y ← 1} mult lident proof: Prove mult lident from ⋆1 ⋆ ⋆2 {x ← 1, y ← x} distrib proof: Prove distrib from ⋆1 ⋆ ⋆2 {x ← x + y, y ← z}, ⋆1 ⋆ ⋆2 {y ← z}, ⋆1 ⋆ ⋆2 {x ← y, y ← z}

mult ldistrib proof: Prove mult ldistrib from

⋆1 ⋆ ⋆2 {y ← y + z, x ← x}, ⋆1 ⋆ ⋆2 , ⋆1 ⋆ ⋆2 {y ← z} mult ldistrib minus proof: Prove mult ldistrib minus from ⋆1 ⋆ ⋆2 {y ← y − z, x ← x}, ⋆1 ⋆ ⋆2 , ⋆1 ⋆ ⋆2 {y ← z}

End multiplication absmod: Module

Using multiplication Exporting all Theory

x, y, z, x_{1}, y_{1}, z_{1}, x_{2}, y_{2}, z_{2}: Var number | ⋆ 1|: Definition function[number → number] =

( λ x: ( if x < 0 then − x else x end if)) abs main: Lemma |x| < z ⊃ (x < z ∨ −x < z) abs leq 0: Lemma |x − y| ≤ z ⊃ (x − y) ≤ z abs diff: Lemma |x − y| < z ⊃ ((x − y) < z ∨ (y − x) < z) abs leq: Lemma |x| ≤ z ⊃ (x ≤ z ∨ −x ≤ z) abs bnd: Lemma 0 ≤ z ∧ 0 ≤ x ∧ x ≤ z ∧ 0 ≤ y ∧ y ≤ z ⊃ |x − y| ≤ z abs 1 bnd: Lemma |x − y| ≤ z ⊃ x ≤ y + z abs 2 bnd: Lemma |x − y| ≤ z ⊃ x ≥ y − z abs 3 bnd: Lemma x ≤ y + z ∧ x ≥ y − z ⊃ |x − y| ≤ z abs drift: Lemma |x − y| ≤ z ∧ |x_{1} − x| ≤ z_{1} ⊃ |x_{1} − y| ≤ z + z_{1} abs com: Lemma |x − y| = |y − x| abs drift 2: Lemma

|x − y| ≤ z ∧ |x_{1} − x| ≤ z_{1} ∧ |y_{1} − y| ≤ z_{2} ⊃ |x_{1} − y_{1}| ≤ z + z_{1} + z_{2} abs geq: Lemma x ≥ y ∧ y ≥ 0 ⊃ |x| ≥ |y| abs ge0: Lemma x ≥ 0 ⊃ |x| = x abs plus: Lemma |x + y| ≤ |x| + |y|

abs diff 3: Lemma x − y ≤ z ∧ y − x ≤ z ⊃ |x − y| ≤ z

Proof

abs plus pr: Prove abs plus from | ⋆ 1| {x ← x + y}, | ⋆ 1| , | ⋆ 1| {x ← y} abs diff 3 pr: Prove abs diff 3 from | ⋆ 1| {x ← x − y} abs ge0 proof: Prove abs ge0 from | ⋆ 1| abs geq proof: Prove abs geq from | ⋆ 1| , | ⋆ 1| {x ← y} abs drift 2 proof: Prove abs drift 2 from

abs drift,

abs drift {x ← y, y ← y_{1}, z ← z_{2}, z_{1} ← z + z_{1}}, abs com {x ← y_{1}}

abs com proof: Prove abs com from |⋆1| {x ← (x−y)}, |⋆1| {x ← (y−x)} abs drift proof: Prove abs drift from

abs 1 bnd,

abs 1 bnd {x ← x_{1}, y ← x, z ← z_{1}},

abs 2 bnd,

abs 2 bnd {x ← x_{1}, y ← x, z ← z_{1}}, abs 3 bnd {x ← x_{1}, z ← z + z_{1}}

abs 3 bnd proof: Prove abs 3 bnd from | ⋆ 1| {x ← (x − y)}

abs main proof: Prove abs main from | ⋆ 1|

abs leq 0 proof: Prove abs leq 0 from | ⋆ 1| {x ← x − y} abs diff proof: Prove abs diff from | ⋆ 1| {x ← (x − y)} abs leq proof: Prove abs leq from | ⋆ 1| abs bnd proof: Prove abs bnd from | ⋆ 1| {x ← (x − y)} abs 1 bnd proof: Prove abs 1 bnd from | ⋆ 1| {x ← (x − y)}

abs 2 bnd proof: Prove abs 2 bnd from | ⋆ 1| {x ← (x − y)} End absmod division: Module

Using multiplication, absmod Exporting all Theory

x, y, z, x_{1}, y_{1}, z_{1}, x_{2}, y_{2}, z_{2}: Var number ⌈⋆1⌉: function[number → int] ceil defn: Axiom ⌈x⌉ ≥ x ∧ ⌈x⌉ − 1 < x mult div 1: Axiom z ≠ 0 ⊃ x ⋆ y/z = x ⋆ (y/z) mult div 2: Axiom z ≠ 0 ⊃ x ⋆ y/z = (x/z) ⋆ y mult div 3: Axiom z ≠ 0 ⊃ (z/z) = 1 mult div: Lemma y ≠ 0 ⊃ (x/y) ⋆ y = x div cancel: Lemma x ≠ 0 ⊃ x ⋆ y/x = y div distrib: Lemma z ≠ 0 ⊃ ((x + y)/z) = (x/z) + (y/z) ceil mult div: Lemma y > 0 ⊃ ⌈x/y⌉ ⋆ y ≥ x ceil plus mult div: Lemma y > 0 ⊃ ⌈x/y⌉ + 1 ⋆ y > x div nonnegative: Lemma x ≥ 0 ∧ y > 0 ⊃ (x/y) ≥ 0 div minus distrib: Lemma z ≠ 0 ⊃ (x − y)/z = (x/z) − (y/z) div ineq: Lemma z > 0 ∧ x ≤ y ⊃ (x/z) ≤ (y/z) abs div: Lemma y > 0 ⊃ |x/y| = |x|/y mult minus: Lemma y ≠ 0 ⊃ −(x/y) = (−x/y) div minus 1: Lemma y > 0 ∧ x < 0 ⊃ (x/y) < 0

Proof

div nonnegative pr: Prove div nonnegative from mult non neg {x ← ( if y ≠ 0 then (x/y) else 0 end if)}, mult div

div distrib pr: Prove div distrib from mult div 1 {x ← x + y, y ← 1, z ← z}, mult rident {x ← x + y}, mult div 1 {x ← x, y ← 1, z ← z}, mult rident, mult div 1 {x ← y, y ← 1, z ← z}, mult rident {x ← y}, distrib {z ← ( if z ≠ 0 then (1/z) else 0 end if)}

div cancel pr: Prove div cancel from mult div 2 {z ← x}, mult div 3 {z ← x}, mult lident {x ← y}

mult div pr: Prove mult div from mult div 2 {z ← y}, mult div 1 {z ← y}, mult div 3 {z ← y}, mult rident

abs div pr: Prove abs div from | ⋆ 1| {x ← ( if y ≠ 0 then (x/y) else 0 end if)}, | ⋆ 1| , div nonnegative, div minus 1, mult minus

mult minus pr: Prove mult minus from mult div 1 {x ← −1, y ← x, z ← y}, ⋆1 ⋆ ⋆2 {x ← −1, y ← x}, ⋆1 ⋆ ⋆2 {x ← −1, y ← ( if y ≠ 0 then (x/y) else 1 end if)}

div minus 1 pr: Prove div minus 1 from mult div, pos product {x ← ( if y ≠ 0 then (x/y) else 0 end if), y ← y}

div minus distrib pr: Prove div minus distrib from div distrib {y ← −y}, mult minus {x ← y, y ← z} div ineq pr: Prove div ineq from

mult div {y ← z},

mult div {x ← y, y ← z},

mult gt {x ← ( if z ≠ 0 then (x/z) else 0 end if), y ← ( if z ≠ 0 then (y/z) else 0 end if)}

ceil plus mult div proof: Prove ceil plus mult div from ceil mult div, distrib

{x ← ⌈( if y ≠ 0 then (x/y) else 0 end if)⌉, y ← 1, z ← y},

mult lident {x ← y}

ceil mult div proof: Prove ceil mult div from mult div, mult leq

{x ← ⌈( if y ≠ 0 then (x/y) else 0 end if)⌉, y ← ( if y ≠ 0 then (x/y) else 0 end if), z ← y},

ceil defn {x ← ( if y ≠ 0 then (x/y) else 0 end if)}

End division division tcc: Module

Using division Exporting all with division Theory

x: Var number y: Var number z: Var number mult div 1 TCC1: Formula (z ≠ 0) ⊃ (z ≠ 0) mult div TCC1: Formula (y ≠ 0) ⊃ (y ≠ 0) div cancel TCC1: Formula (x ≠ 0) ⊃ (x ≠ 0) ceil mult div TCC1: Formula (y > 0) ⊃ (y ≠ 0) div nonnegative TCC1: Formula (x ≥ 0 ∧ y > 0) ⊃ (y ≠ 0) div ineq TCC1: Formula (z > 0 ∧ x ≤ y) ⊃ (z ≠ 0) div minus 1 TCC1: Formula (y > 0 ∧ x < 0) ⊃ (y ≠ 0)

Proof

mult div 1 TCC1 PROOF: Prove mult div 1 TCC1 mult div TCC1 PROOF: Prove mult div TCC1 div cancel TCC1 PROOF: Prove div cancel TCC1 ceil mult div TCC1 PROOF: Prove ceil mult div TCC1 div nonnegative TCC1 PROOF: Prove div nonnegative TCC1 div ineq TCC1 PROOF: Prove div ineq TCC1 div minus 1 TCC1 PROOF: Prove div minus 1 TCC1 End division tcc

arith: Module

Using multiplication, division, absmod

Exporting all with multiplication, division, absmod

End arith countmod: Module

Exporting all

Theory

l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var nat i, j, k: Var nat x, y, z, r, s, t: Var number X, Y, Z: Var number ppred, ppred1, ppred2: Var function[nat → bool] fun, fun1, fun2: Var function[nat → number] countsize: function[function[nat → bool], nat → nat] = ( λ ppred, i: i) count: Recursive function[function[nat → bool], nat → nat] =

( λ ppred, i: ( if i > 0

then ( if ppred(i − 1) then 1 + (count(ppred, i − 1)) else count(ppred, i − 1) end if)

else 0

end if)) by countsize

End countmod countmod tcc: Module

Using countmod Exporting all with countmod Theory

i: Var naturalnumber ppred: Var function[naturalnumber → boolean] count TCC1: Formula (i > 0) ⊃ (i − 1 ≥ 0) count TCC2: Formula (ppred(i − 1)) ∧ (i > 0) ⊃ (i − 1 ≥ 0) count TCC3: Formula (¬(ppred(i − 1))) ∧ (i > 0) ⊃ (i − 1 ≥ 0) count TCC4: Formula

(ppred(i − 1)) ∧ (i > 0) ⊃ countsize(ppred, i) > countsize(ppred, i − 1) count TCC5: Formula

(¬(ppred(i − 1))) ∧ (i > 0) ⊃ countsize(ppred, i) > countsize(ppred, i − 1)

Proof

count TCC1 PROOF: Prove count TCC1 count TCC2 PROOF: Prove count TCC2 count TCC3 PROOF: Prove count TCC3 count TCC4 PROOF: Prove count TCC4 count TCC5 PROOF: Prove count TCC5

End countmod tcc clockassumptions: Module

Using arith, countmod Exporting all with countmod, arith Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time X, Y, Z, R, S, T: Var Clocktime γ, θ: Var function[process → Clocktime] δ, μ, ρ, r_{min}, r_{max}, β, Λ: number P C_{⋆1}(⋆2), V C_{⋆1}(⋆2): function[process, time → Clocktime] t_{⋆1}^{⋆2}: function[process, event → time] Θ_{⋆1}^{⋆2}: function[process, event → function[process → Clocktime]] IC_{⋆1}^{⋆2}(⋆3): function[process, event, time → Clocktime] correct: function[process, time → bool] cfn: function[process, function[process → Clocktime] → Clocktime] π: function[Clocktime, Clocktime → Clocktime] α: function[Clocktime → Clocktime] delta 0: Axiom δ ≥ 0 mu 0: Axiom μ ≥ 0 rho 0: Axiom ρ ≥ 0 rho 1: Axiom ρ < 1 rmin 0: Axiom r_{min} > 0 rmax 0: Axiom r_{max} > 0 beta 0: Axiom β ≥ 0

lamb 0: Axiom Λ ≥ 0

init: Axiom correct(p, 0) ⊃ P C_{p}(0) ≥ 0 ∧ P C_{p}(0) ≤ μ

correct closed: Axiom s ≥ t ∧ correct(p, s) ⊃ correct(p, t)

rate 1: Axiom correct(p, s) ∧ s ≥ t ⊃ P C_{p}(s) − P C_{p}(t) ≤ (s − t) ⋆ (1 + ρ)

rate 2: Axiom correct(p, s) ∧ s ≥ t ⊃ P C_{p}(s) − P C_{p}(t) ≥ (s − t) ⋆ (1 − ρ)

rts0: Axiom correct(p, t) ∧ t ≤ t_{p}^{i+1} ⊃ t − t_{p}^{i} ≤ r_{max}

rts1: Axiom correct(p, t) ∧ t ≥ t_{p}^{i+1} ⊃ t − t_{p}^{i} ≥ r_{min}

rts 0: Lemma correct(p, t_{p}^{i+1}) ⊃ t_{p}^{i+1} − t_{p}^{i} ≤ r_{max}

rts 1: Lemma correct(p, t_{p}^{i+1}) ⊃ t_{p}^{i+1} − t_{p}^{i} ≥ r_{min}

rts2: Axiom correct(p, t) ∧ t ≥ t_{q}^{i} + β ∧ correct(q, t) ⊃ t ≥ t_{p}^{i}

rts 2: Axiom correct(p, t_{p}^{i}) ∧ correct(q, t_{q}^{i}) ⊃ t_{p}^{i} − t_{q}^{i} ≤ β

synctime 0: Axiom t_{p}^{0} = 0

VClock defn: Axiom correct(p, t) ∧ t ≥ t_{p}^{i} ∧ t < t_{p}^{i+1} ⊃ V C_{p}(t) = IC_{p}^{i}(t)

Adj: function[process, event → Clocktime] = ( λ p, i: ( if i > 0 then cfn(p, Θ_{p}^{i}) − P C_{p}(t_{p}^{i}) else 0 end if))

IClock defn: Axiom correct(p, t) ⊃ IC_{p}^{i}(t) = P C_{p}(t) + Adj(p, i)

Readerror: Axiom correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ |Θ_{p}^{i+1}q) − IC_{q}^{i}(t_{p}^{i+1})| ≤ Λ

translation invariance: Axiom X ≥ 0 ⊃ cfn(p, ( λ p_{1} → Clocktime: γ(p_{1}) + X)) = cfn(p, γ) + X ppred: Var function[process → bool] maxfaults: process okay Readpred: function[function[process → Clocktime], Clocktime,

function[process → bool] → bool] =

( λ γ, Y, ppred: ( ∀ l, m: ppred(l) ∧ ppred(m) ⊃ |γ(l) − γ(m)| ≤ Y)) okay pairs: function[function[process → Clocktime],

function[process → Clocktime], Clocktime, function[process → bool] → bool] =

( λ γ, θ, X, ppred: ( ∀ p_{3}: ppred(p_{3}) ⊃ |γ(p_{3}) − θ(p_{3})| ≤ X)) N: process

N 0: Axiom N > 0

N maxfaults: Axiom maxfaults ≤ N

precision enhancement ax: Axiom count(ppred, N) ≥ N − maxfaults

∧ okay Readpred(γ, Y, ppred) ∧ okay Readpred(θ, Y, ppred)

∧ okay pairs(γ, θ, X, ppred) ∧ ppred(p) ∧ ppred(q) ⊃ |cfn(p, γ) − cfn(q, θ)| ≤ π(X, Y)

correct count: Axiom count(( λ p: correct(p, t)), N) ≥ N − maxfaults

okay Reading: function[function[process → Clocktime], Clocktime, time → bool] =

( λ γ, Y, t: ( ∀ p_{1}, q_{1}:

correct(p_{1}, t) ∧ correct(q_{1}, t) ⊃ |γ(p_{1}) − γ(q_{1})| ≤ Y))

okay Readvars: function[function[process → Clocktime], function[process → Clocktime], Clocktime, Clocktime → bool] = ( λ γ, θ, X, t: ( ∀ p_{3}: correct(p_{3}, t) ⊃ |γ(p_{3}) − θ(p_{3})| ≤ X))

okay Readpred Reading: Lemma okay Reading(γ, Y, t) ⊃ okay Readpred(γ, Y, ( λ p: correct(p, t)))

okay pairs Readvars: Lemma okay Readvars(γ, θ, X, t) ⊃ okay pairs(γ, θ, X, ( λ p: correct(p, t))) precision enhancement: Lemma

okay Reading(γ, Y, t_{p}^{i+1})

∧ okay Reading(θ, Y, t_{p}^{i+1})

∧ okay Readvars(γ, θ, X, t_{p}^{i+1})
∧ correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ |cfn(p, γ) − cfn(q, θ)| ≤ π(X, Y)

okay Reading defn lr: Lemma

okay Reading(γ, Y, t)

⊃ ( ∀ p_{1}, q_{1}: correct(p_{1}, t) ∧ correct(q_{1}, t) ⊃ |γ(p_{1}) − γ(q_{1})| ≤ Y)

okay Reading defn rl: Lemma

( ∀ p_{1}, q_{1}: correct(p_{1}, t) ∧ correct(q_{1}, t) ⊃ |γ(p_{1}) − γ(q_{1})| ≤ Y)

⊃ okay Reading(γ, Y, t)

okay Readvars defn lr: Lemma okay Readvars(γ, θ, X, t) ⊃ ( ∀ p_{3}: correct(p_{3}, t) ⊃ |γ(p_{3}) − θ(p_{3})| ≤ X)

okay Readvars defn rl: Lemma ( ∀ p_{3}: correct(p_{3}, t) ⊃ |γ(p_{3}) − θ(p_{3})| ≤ X) ⊃ okay Readvars(γ, θ, X, t)

accuracy preservation ax: Axiom

okay Readpred(γ, X, ppred)

∧ count(ppred, N) ≥ N − maxfaults ∧ ppred(p) ∧ ppred(q) ⊃ |cfn(p, γ) − γ(q)| ≤ α(X)

Proof

okay Reading defn rl pr: Prove okay Reading defn rl {p_{1} ← p_{1}@P1S, q_{1} ← q_{1}@P1S} from okay Reading

okay Reading defn lr pr: Prove okay Reading defn lr from okay Reading {p_{1} ← p_{1}@CS, q_{1} ← q_{1}@CS}

okay Readvars defn rl pr: Prove okay Readvars defn rl {p_{3} ← p_{3}@P1S} from

okay Readvars okay Readvars defn lr pr: Prove okay Readvars defn lr from

okay Readvars {p_{3} ← p_{3}@CS}

precision enhancement pr: Prove precision enhancement from precision enhancement ax {ppred ← ( λ q: correct(q, t_{p}^{i+1}))}, okay Readpred Reading {t ← t_{p}^{i+1}}, okay Readpred Reading {t ← t_{p}^{i+1}, γ ← θ}, okay pairs Readvars {t ← t_{p}^{i+1}}, correct count {t ← t_{p}^{i+1}}

okay Readpred Reading pr: Prove okay Readpred Reading from okay Readpred {ppred ← ( λ p: correct(p, t))}, okay Reading {p_{1} ← l@P 1S, q_{1} ← m@P 1S}

okay pairs Readvars pr: Prove okay pairs Readvars from okay pairs {ppred ← ( λ p: correct(p, t))}, okay Readvars {p_{3} ← p_{3}@P1S}

rts 0 proof: Prove rts 0 from rts0 {t ← t_{p}^{i+1}}

rts 1 proof: Prove rts 1 from rts1 {t ← t_{p}^{i+1}}

End clockassumptions basics: Module

Using clockassumptions, arith

Exporting all with clockassumptions

Theory

p, q, p_{1}, p_{2}, q_{1}, q_{2}, l, m, n: Var process i, j, k: Var event x, y, z: Var number r, s, t, t_{1}, t_{2}: Var time X, Y, Z, R, S, T, T_{1}, T_{2}: Var Clocktime γ, θ: Var function[process → time] (⋆1 ⇑ ⋆2)[⋆3]: Definition function[process, process, event → process] =

( λ p, q, i: ( if t_{p}^{i} ≥ t_{q}^{i} then p else q end if))

maxsync correct: Lemma correct(p, s)∧correct(q, s) ⊃ correct((p ⇑ q)[i], s)

minsync: Definition function[process, process, event → process] = ( λ p, q, i: ( if t_{p}^{i} ≥ t_{q}^{i} then q else p end if))

minsync correct: Lemma correct(p, s) ∧ correct(q, s) ⊃ correct((p ⇓ q)[i], s)

minsync maxsync: Lemma t_{(p⇓q)[i]}^{i} ≤ t_{(p⇑q)[i]}^{i}

t_{⋆1,⋆2}^{⋆3}: Definition function[process, process, event → time] = ( λ p, q, i: t_{(p⇑q)[i]}^{i})

lemma 1: Lemma correct(p, t_{p}^{i}) ∧ correct(q, t_{q}^{i+1}) ∧ β ≤ r_{min} ⊃ t_{p}^{i} ≤ t_{q}^{i+1}

lemma 1 1: Lemma correct(p, t_{q}^{i+1}) ∧ correct(q, t_{q}^{i+1}) ∧ β ≤ r_{min} ⊃ t_{p}^{i} ≤ t_{q}^{i+1}

lemma 1 2: Lemma correct(p, t_{p}^{i+1}) ∧ correct(q, t_{q}^{i})

⊃ t_{p}^{i+1} ≤ t_{q}^{i} + r_{max} + β lemma 2 0: Lemma correct(p, 0) ∧ correct(q, 0) ⊃ |IC_{p}^{0}(0) − IC_{q}^{0}(0)| ≤ μ

lemma 2 1: Lemma correct(q, t_{q}^{i+1})

⊃ IC_{q}^{i+1}(t_{q}^{i+1}) = cfn(q, Θ_{q}^{i+1})

lemma 2 2a: Lemma correct(q, s) ∧ s ≥ t ⊃ IC_{q}^{i}(s) ≤ IC_{q}^{i}(t) + (s − t) ⋆ (1 + ρ)

lemma 2 2b: Lemma correct(q, s) ∧ s ≥ t ⊃ IC_{q}^{i}(s) ≥ IC_{q}^{i}(t) + (s − t) ⋆ (1 − ρ)

abs shift: Lemma |r − s| ≤ x

∧ t_{1} ≤ r + y + z ∧ t_{1} ≥ r + y − z ∧ t_{2} ≤ s + y + z ∧ t_{2} ≥ s + y − z

⊃ |t_{1} − t_{2}| ≤ x + 2 ∗ z

ReadClock bnd1: Lemma

correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ Θ_{p}^{i+1}q) ≤ IC_{q}^{i}(t_{p}^{i+1}) + Λ

ReadClock bnd2: Lemma

correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ Θ_{p}^{i+1}q) ≥ IC_{q}^{i}(t_{p}^{i+1}) − Λ

ReadClock bnd11: Lemma

correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1}) ∧ correct(p_{1}, t_{p_{1}}^{i}) ∧ β ≤ r_{min} ⊃ Θ_{p}^{i+1}q) ≤ IC_{q}^{i}(t_{p_{1}}^{i}) + (t_{p}^{i+1} − t_{p_{1}}^{i}) + (r_{max} + β) ⋆ ρ + Λ

ReadClock bnd12: Lemma

correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1}) ∧ correct(p_{1}, t_{p_{1}}^{i}) ∧ β ≤ r_{min} ⊃ Θ_{p}^{i+1}q) ≥ IC_{q}^{i}(t_{p_{1}}^{i}) + (t_{p}^{i+1} − t_{p_{1}}^{i}) − (r_{max} + β) ⋆ ρ − Λ

ReadClock bnd: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1})
∧ correct(q_{1}, t_{p}^{i+1})
∧ |IC_{q}^{i}(t_{q,q_{1}}^{i}) − IC_{q_{1}}^{i}(t_{q,q_{1}}^{i})| ≤ X ∧ β ≤ r_{min}
⊃ |Θ_{p}^{i+1}q) − Θ_{p}^{i+1}q_{1})| ≤ X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)

okay Reading shift1: Lemma

correct(p_{1}, s) ∧ s ≥ t_{p_{1}}^{i+1}

∧ β ≤ r_{min}

∧ ( ∀ p, q:
correct(p, t_{p,q}^{i}) ∧ correct(q, t_{p,q}^{i})
⊃ |IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ X)

⊃ okay Reading(Θ_{p_{1}}^{i+1}, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ), s)

okay Readvars shift step: Lemma

s ≥ t_{1} − y ∧ s ≤ t_{1} + y

∧ t ≥ t_{2} − y ∧ t ≤ t_{2} + y ∧ 0 ≤ t_{2} − t_{1} ∧ t_{2} − t_{1} ≤ x ⊃ |s + x − t| ≤ 2 ∗ y + x

okay Readvars shift stepb: Lemma

s ≥ t_{1} − y ∧ s ≤ t_{1} + y

∧ t ≥ t_{2} − y ∧ t ≤ t_{2} + y ∧ 0 ≤ t_{2} − t_{1} ∧ t_{2} − t_{1} ≤ x ⊃ |s − t| ≤ 2 ∗ y + x

okay Readvars shift step1: Lemma

|s − t_{1}| ≤ y ∧ |t − t_{2}| ≤ y ∧ 0 ≤ t_{2} − t_{1} ∧ t_{2} − t_{1} ≤ x ⊃ |s + x − t| ≤ 2 ∗ y + x

okay Readvars shift step2: Lemma

|s − t_{1}| ≤ y ∧ |t − t_{2}| ≤ y ∧ 0 ≤ t_{2} − t_{1} ∧ t_{2} − t_{1} ≤ x ⊃ |s − t| ≤ 2 ∗ y + x

okay Readvars shift11: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1}) ∧ correct(p_{1}, t_{p}^{i+1}) ∧ t_{p}^{i+1} ≥ t_{q}^{i+1} ⊃ Θ_{q}^{i+1}p_{1}) + (P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})) − Θ_{p}^{i+1}p_{1})

≤ 2 ∗ Λ + 2 ∗ β ⋆ ρ

okay Readvars shift12: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1}) ∧ correct(p_{1}, t_{p}^{i+1}) ∧ t_{p}^{i+1} ≥ t_{q}^{i+1} ⊃ Θ_{p}^{i+1}p_{1}) − (Θ_{q}^{i+1}p_{1}) + (P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})))

≤ 2 ∗ Λ + 2 ∗ β ⋆ ρ

okay Readvars shift1: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1}) ∧ correct(p_{1}, t_{p}^{i+1}) ∧ t_{p}^{i+1} ≥ t_{q}^{i+1}
⊃ |Θ_{p}^{i+1}p_{1}) − (Θ_{q}^{i+1}p_{1}) + (P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})))|
≤ 2 ∗ Λ + 2 ∗ β ⋆ ρ

okay Readvars shift2: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1}) ∧ t ≥ t_{p}^{i+1} ∧ t_{p}^{i+1} ≥ t_{q}^{i+1}
⊃ okay Readvars(Θ_{p}^{i+1}, Θ_{q}^{i+1}, 2 ∗ Λ + 2 ∗ β ⋆ ρ, t)

okay Readvars shift: Lemma

t ≥ t_{p}^{i+1} ∧ correct(p, t) ∧ correct(q, t) ∧ t_{p}^{i+1} ≥ t_{q}^{i+1}

⊃ okay Readvars(Θ_{p}^{i+1},
( λ p_{1} → time:
Θ_{q}^{i+1}p_{1}) + (P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}))),
2 ∗ Λ + 2 ∗ β ⋆ ρ,
t)

Proof

maxsync correct pr: Prove maxsync correct from (⋆1 ⇑ ⋆2)[⋆3]

minsync correct pr: Prove minsync correct from minsync

minsync maxsync pr: Prove minsync maxsync from minsync, (⋆1 ⇑ ⋆2)[⋆3] okay Reading shift1 proof: Prove

okay Reading shift1 {p ← p_{1}@P1S, q ← q_{1}@P1S} from okay Reading defn rl

{γ ← Θ_{p_{1}}^{i+1}, Y ← X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ), t ← s},

ReadClock bnd {p ← p_{1}, q ← p_{1}@P1S, q_{1} ← q_{1}@P1S}, t_{⋆1,⋆2}^{⋆3} {p ← p_{1}@P1S, q ← q_{1}@P1S}, maxsync correct {p ← p_{1}@P1S, q ← q_{1}@P1S, s ← t_{p_{1}}^{i+1}}, correct closed {p ← p_{1}@P1S, t ← t_{p_{1}}^{i+1}}, correct closed {p ← q_{1}@P1S, t ← t_{p_{1}}^{i+1}}, correct closed {p ← p_{1}@P1S, t ← t_{p,q}^{i}, s ← t_{p_{1}}^{i+1}}, correct closed {p ← q_{1}@P1S, t ← t_{p,q}^{i}, s ← t_{p_{1}}^{i+1}}, correct closed {p ← p_{1}, t ← t_{p_{1}}^{i+1}}, lemma 1 1 {q ← p_{1}, p ← (p ⇑ q)[i]} ReadClock bnd proof: Prove ReadClock bnd from

ReadClock bnd11 {p_{1} ← (q ⇑ q_{1})[i]}, ReadClock bnd12 {p_{1} ← (q ⇑ q_{1})[i]}, ReadClock bnd11 {q ← q_{1}, p_{1} ← (q ⇑ q_{1})[i]}, ReadClock bnd12 {q ← q_{1}, p_{1} ← (q ⇑ q_{1})[i]}, lemma 1 1 {p ← (q ⇑ q_{1})[i], q ← p}, correct closed

{p ← (q ⇑ q_{1})[i], s ← t_{p}^{i+1}, t ← t_{(q⇑q_{1})[i]}^{i}},

abs shift {r ← IC_{q}^{i}(t_{q,q_{1}}^{i}), s ← IC_{q_{1}}^{i}(t_{q,q_{1}}^{i}), t_{1} ← Θ_{p}^{i+1}q), t_{2} ← Θ_{p}^{i+1}q_{1}), y ← (t_{p}^{i+1} − t_{q,q_{1}}^{i}), z ← (r_{max} + β) ⋆ ρ + Λ, x ← X},

t_{⋆1,⋆2}^{⋆3} {p ← q, q ← q_{1}}, maxsync correct {p ← q, q ← q_{1}, s ← t_{p}^{i+1}}

ReadClock bnd11 proof: Prove ReadClock bnd11 from ReadClock bnd1, lemma 2 2a {s ← t_{p}^{i+1}, t ← t_{p_{1}}^{i}}, lemma 1 2 {q ← p_{1}}, lemma 1 {q ← p, p ← p_{1}}, mult ldistrib {x ← t_{p}^{i+1} − t_{p_{1}}^{i}, y ← 1, z ← ρ}, mult leq {x ← r_{max} + β, y ← t_{p}^{i+1} − t_{p_{1}}^{i}, z ← ρ}, mult rident {x ← t_{p}^{i+1} − t_{p_{1}}^{i}}, rho 0 ReadClock bnd12 proof: Prove ReadClock bnd12 from

ReadClock bnd2, lemma 2 2b {s ← t_{p}^{i+1}, t ← t_{p_{1}}^{i}}, lemma 1 2 {q ← p_{1}}, lemma 1 {q ← p, p ← p_{1}}, mult ldistrib minus {x ← t_{p}^{i+1} − t_{p_{1}}^{i}, y ← 1, z ← ρ}, mult leq {x ← r_{max} + β, y ← t_{p}^{i+1} − t_{p_{1}}^{i}, z ← ρ}, mult rident {x ← t_{p}^{i+1} − t_{p_{1}}^{i}}, rho 0

ReadClock bnd1 proof: Prove ReadClock bnd1 from Readerror, | ⋆ 1| {x ← Θ_{p}^{i+1}q) − IC_{q}^{i}(t_{p}^{i+1})}

ReadClock bnd2 proof: Prove ReadClock bnd2 from Readerror, | ⋆ 1| {x ← Θ_{p}^{i+1}q) − IC_{q}^{i}(t_{p}^{i+1})}

okay Readvars shift step1 proof: Prove okay Readvars shift step1 from okay Readvars shift step, | ⋆ 1| {x ← s − t_{1}}, | ⋆ 1| {x ← t − t_{2}}

okay Readvars shift step2 proof: Prove okay Readvars shift step2 from okay Readvars shift stepb, | ⋆ 1| {x ← s − t_{1}}, | ⋆ 1| {x ← t − t_{2}}

okay Readvars shift11 proof: Prove okay Readvars shift11 from ReadClock bnd2 {q ← p_{1}}, ReadClock bnd1 {p ← q, q ← p_{1}}, correct closed {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← p_{1}}, correct closed {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← q}, lemma 2 2b {q ← p_{1}, s ← t_{p}^{i+1}, t ← t_{q}^{i+1}}, rate 1 {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← q}, mult ldistrib minus {x ← t_{p}^{i+1} − t_{q}^{i+1}, y ← 1, z ← ρ}, mult ldistrib {x ← t_{p}^{i+1} − t_{q}^{i+1}, y ← 1, z ← ρ}, mult leq {x ← β, y ← t_{p}^{i+1} − t_{q}^{i+1}, z ← ρ}, rts 2 {i ← i + 1}, rho 0 okay Readvars shift12 proof: Prove okay Readvars shift12 from

ReadClock bnd1 {q ← p_{1}},

ReadClock bnd2 {p ← q, q ← p_{1}},

correct closed {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← p_{1}}, correct closed {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← q}, lemma 2 2a {q ← p_{1}, s ← t_{p}^{i+1}, t ← t_{q}^{i+1}}, rate 2 {s ← t_{p}^{i+1}, t ← t_{q}^{i+1}, p ← q}, mult ldistrib minus {x ← t_{p}^{i+1} − t_{q}^{i+1}, y ← 1, z ← ρ}, mult ldistrib {x ← t_{p}^{i+1} − t_{q}^{i+1}, y ← 1, z ← ρ}, mult leq {x ← β, y ← t_{p}^{i+1} − t_{q}^{i+1}, z ← ρ}, rts 2 {i ← i + 1}, rho 0

okay Readvars shift1 proof: Prove okay Readvars shift1 from okay Readvars shift11, okay Readvars shift12, abs diff 3

{y ← Θ_{q}^{i+1}p_{1}) + (P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})),

x ← Θ_{p}^{i+1}p_{1}),

z ← 2 ∗ Λ + 2 ∗ β ⋆ ρ}

okay Readvars shift step proof: Prove okay Readvars shift step from | ⋆ 1| {x ← s + x − t}

okay Readvars shift stepb proof: Prove okay Readvars shift stepb from | ⋆ 1| {x ← s − t}, | ⋆ 1| {x ← t_{2} − t_{1}}

okay Readvars shift proof: Prove okay Readvars shift from okay Readvars shift1 {p_{1} ← p_{3}@P2S}, okay Readvars defn rl

{θ ← ( λ p_{1} → time: Θ_{q}^{i+1}p_{1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})), γ ← Θ_{p}^{i+1}, X ← 2 ∗ Λ + 2 ∗ β ⋆ ρ}, correct closed {s ← t, t ← t_{p}^{i+1}}, correct closed {p ← q, s ← t, t ← t_{p}^{i+1}}, correct closed {p ← p_{3}@P2S, s ← t, t ← t_{p}^{i+1}} lemma 1 proof: Prove lemma 1 from

rts 1 {p ← q}, rts 2, rmin 0, correct closed {p ← q, s ← t_{q}^{i+1}, t ← t_{q}^{i}}

lemma 1 2 proof: Prove lemma 1 2 from rts 0, rts 1, rts 2, rmin 0, correct closed {s ← t_{p}^{i+1}, t ← t_{p}^{i}}

lemma 2 0 proof: Prove lemma 2 0 from synctime 0, synctime 0 {p ← q}, IClock defn {p ← q, i ← 0, t ← 0}, IClock defn {i ← 0, t ← 0}, Adj {i ← 0, p ← q}, Adj {i ← 0}, init {p ← q}, init, rts 1 {p ← q, i ← 0}, rts 1 {i ← 0}, rmin 0, mu 0, abs bnd {x ← IC_{p}^{0}(t_{p}^{0}), y ← IC_{q}^{0}(t_{p}^{0}), z ← μ}

lemma 2 1 proof: Prove lemma 2 1 from IClock defn {p ← q, i ← i + 1, t ← t_{q}^{i+1}}, Adj {i ← i + 1, p ← q}

lemma 2 2a proof: Prove lemma 2 2a from IClock defn {p ← q, t ← s}, IClock defn {p ← q}, rate 1 {p ← q}, correct closed {p ← q} lemma 2 2b proof: Prove lemma 2 2b from

IClock defn {p ← q, t ← s},

IClock defn {p ← q},

rate 2 {p ← q},

correct closed {p ← q}

abs shift proof: Prove abs shift from | ⋆ 1| {x ← r − s}, | ⋆ 1| {x ← t_{1} − t_{2}}

lemma 1 1 proof: Prove lemma 1 1 from rts 1 {p ← q}, rts2 {t ← t_{q}^{i+1}}, beta 0, rmin 0, correct closed {p ← q, s ← t_{q}^{i+1}, t ← t_{q}^{i}}

End basics readbounds: Module

Using basics, clockassumptions, arith

Exporting all with basics

Theory

p, q, p_{1}, p_{2}, q_{1}, q_{2}, l, m, n: Var process i, j, k: Var event X, Y, Z, R, S, T, T_{1}, T_{2}: Var Clocktime x, y, z, r, s, t, t_{1}, t_{2}: Var number γ, θ: Var function[process → Clocktime] prop: Var function[nat → bool] okaymaxsync: function[nat, Clocktime → bool] =

( λ i, X: ( ∀ p, q:

correct(p, t_{p,q}^{i}) ∧ correct(q, t_{p,q}^{i})

⊃ |IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ X))

okaymaxsync defn lr: Lemma

okaymaxsync(i, X)

⊃ ( ∀ p, q:

correct(p, t_{p,q}^{i}) ∧ correct(q, t_{p,q}^{i})
⊃ |IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ X)

okaymaxsync defn rl: Lemma

( ∀ p, q: correct(p, t_{p,q}^{i}) ∧ correct(q, t_{p,q}^{i})

⊃ |IC_{p}^{i}(t_{p,q}^{i}) − IC_{q}^{i}(t_{p,q}^{i})| ≤ X) ⊃ okaymaxsync(i, X)

lemma 2 base: Lemma μ ≤ X ⊃ okaymaxsync(0, X)

okay Reading shift2: Lemma

correct(p_{1}, s) ∧ s ≥ t_{p_{1}}^{i+1} ∧ β ≤ r_{min} ∧ okaymaxsync(i, X) ⊃ okay Reading(Θ_{p_{1}}^{i+1}, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ), s)

Cfn IClock1: Lemma

correct(q, t_{p}^{i+1}) ∧ correct(p, t_{p}^{i+1}) ∧ t_{p}^{i+1} ≥ t_{q}^{i+1}

⊃ IC_{q}^{i+1}(t_{p}^{i+1})

= cfn(q, ( λ p_{1} → time: Θ_{q}^{i+1}p_{1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})))

okay Reading plus: Lemma okay Reading(γ, Y, t) ⊃ okay Reading(( λ p_{1} → time: γ(p_{1}) + X), Y, t)

lemma 2 ind1: Lemma

β ≤ r_{min} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X

∧ okaymaxsync(i, X)

∧ t_{p}^{i+1} ≥ t_{q}^{i+1} ∧ correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ |cfn(p, Θ_{p}^{i+1})
− cfn(q,
( λ p_{1} → time:
Θ_{q}^{i+1}p_{1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})))|

≤ X

lemma2 abs fact: Lemma t_{1} ≤ t ∧ t ≤ t_{2} ∧ |s − t_{1}| ≤ X ∧ |s − t_{2}| ≤ X ⊃ |s − t| ≤ X

lemma 2 ind3: Lemma

β ≤ r_{min} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X

∧ okaymaxsync(i, X)

∧ t_{p}^{i+1} ≥ t_{q}^{i+1} ∧ correct(p, t_{p}^{i+1}) ∧ correct(q, t_{p}^{i+1})

⊃ |IC_{p}^{i+1}(t_{p}^{i+1}) − IC_{q}^{i+1}(t_{p}^{i+1})| ≤ X

lemma 2 ind step: Lemma |IC_{(p⇑q)[i]}^{i}(t) − IC_{(p⇓q)[i]}^{i}(t)| ≤ X ⊃ |IC_{p}^{i}(t) − IC_{q}^{i}(t)| ≤ X

lemma 2 ind: Lemma

β ≤ r_{min} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X

∧ okaymaxsync(i, X) ⊃ okaymaxsync(i + 1, X) lemma 2: Lemma β ≤ r_{min}

∧ μ ≤ X ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ⊃ okaymaxsync(i, X)

induction: Axiom prop(0) ∧ ( ∀ j: prop(j) ⊃ prop(j + 1)) ⊃ prop(i)

Proof

okaymaxsync defn lr pr: Prove okaymaxsync defn lr from okaymaxsync {p ← p@CS, q ← q@CS}

okaymaxsync defn rl pr: Prove okaymaxsync defn rl {p ← p@P 1S, q ← q@P 1S} from okaymaxsync

lemma 2 base proof: Prove lemma 2 base from t_{⋆1,⋆2}^{⋆3} {i ← 0, p ← p@P 4S, q ← q@P 4S}, synctime 0 {p ← (p@P 4S ⇑ q@P 4S)[0]}, lemma 2 0 {p ← p@P 4S, q ← q@P 4S}, okaymaxsync defn rl {i ← 0}

okay Reading shift2 proof: Prove okay Reading shift2 from okay Reading shift1, okaymaxsync defn lr {p ← p@P 1S, q ← q@P 1S}

Cfn IClock1 proof: Prove Cfn IClock1 from IClock defn {p ← q, t ← t_{p}^{i+1}, i ← i + 1}, Adj {p ← q, i ← i + 1}, translation invariance

{p ← q, γ ← Θ_{q}^{i+1}, X ← P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})},

rate 2 {p ← q, s ← t_{p}^{i+1}, t ← t_{q}^{i+1}}, rho 1, pos product {x ← t_{p}^{i+1} − t_{q}^{i+1}, y ← 1 − ρ}

okay Reading plus proof: Prove okay Reading plus from okay Reading defn lr {p_{1} ← p_{1}@P2S, q_{1} ← q_{1}@P2S}, okay Reading defn rl {γ ← ( λ p_{1} → time: γ(p_{1}) + X)} lemma 2 ind1 proof: Prove lemma 2 ind1 from

precision enhancement {θ ← ( λ p_{1} → time: Θ_{q}^{i+1}p_{1}) + P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1})), γ ← Θ_{p}^{i+1}, X ← 2 ∗ Λ + 2 ∗ β ⋆ ρ, Y ← X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)},

okay Readvars shift {t ← t_{p}^{i+1}},

okay Reading shift2 {p_{1} ← p, s ← t_{p}^{i+1}}, okay Reading shift2 {p_{1} ← q, s ← t_{p}^{i+1}}, okay Reading plus {γ ← Θ_{q}^{i+1}, t ← t_{p}^{i+1}, X ← P C_{q}(t_{p}^{i+1}) − P C_{q}(t_{q}^{i+1}), Y ← X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)}, correct closed {p ← q, s ← t_{p}^{i+1}, t ← t_{q}^{i+1}}

lemma2 abs fact proof: Prove lemma2 abs fact from | ⋆ 1| {x ← s − t_{1}}, | ⋆ 1| {x ← s − t_{2}}, | ⋆ 1| {x ← s − t}

lemma 2 ind3 proof: Prove lemma 2 ind3 from lemma 2 ind1, lemma2 abs fact

{s ← IC_{p}^{i+1}(t_{p}^{i+1}), t ← IC_{q}^{i+1}(t_{p}^{i+1}), t_{1} ← cfn(q, Θ_{q}^{i+1}), t_{2} ← cfn(q, ( λ p_{1} → time: Θ_{q}^{i+1}p_{1}) + β ⋆ (1 + ρ))), X ← X}, lemma 2 1 {q ← p}, Cfn IClock1

lemma 2 ind step proof: Prove lemma 2 ind step from (⋆1 ⇑ ⋆2)[⋆3] , minsync, abs com {x ← IC_{p}^{i}(t), y ← IC_{q}^{i}(t)} lemma 2 ind proof: Prove lemma 2 ind from

lemma 2 ind3 {p ← (p@P 2S ⇑ q@P 2S)[i+1], q ← (p@P 2S ⇓ q@P 2S)[i+ 1]},

okaymaxsync defn rl {i ← i + 1}, lemma 2 ind step

{i ← i + 1, p ← p@P 2S, q ← q@P 2S, t ← t_{p@P 2S,q@P 2S}^{i+1}},

t_{⋆1,⋆2}^{⋆3} {i ← i + 1, p ← p@P 2S, q ← q@P 2S}, minsync maxsync {i ← i + 1, p ← p@P 2S, q ← q@P 2S}, maxsync correct

{s ← t_{p,q}^{i+1}, i ← i + 1, p ← p@P 2S, q ← q@P 2S},

minsync correct {s ← t_{p,q}^{i+1}, i ← i + 1, p ← p@P 2S, q ← q@P 2S}

lemma 2 proof: Prove lemma 2 from

readbounds.induction

{prop ← ( λ i → bool:

β ≤ r_{min} ∧ μ ≤ X

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ⊃ okaymaxsync(i, X))},

lemma 2 ind {i ← j@P 1S}, lemma 2 base, mu 0

End readbounds lemma3: Module

Using readbounds, basics, clockassumptions, arith

Exporting all with readbounds

Theory

prop: Var function[nat → bool] l, m, n, p_{0}, q_{0}, p, q, p_{1}, p_{2}, q_{1}, q_{2}: Var process i, j, k: Var event x, y, z, r, s, t, t_{1}, t_{2}, x_{1}, x_{2}, y_{1}, y_{2}: Var time X, Y, Z, R, S, T, T_{1}, T_{2}, X_{1}, X_{2}, Y_{1}, Y_{2}: Var Clocktime γ, θ: Var function[process → Clocktime] abs IClock diff: function[nat, Clocktime → bool] IClock Reading: function[nat, time → function[process → Clocktime]] δ_{S}: time

maxmax gap: Lemma

correct(p, s) ∧ correct(q, s)

∧ s ≥ t ∧ s ≤ t_{(p⇑q)[i+1]}^{i+1} ∧ t ≥ t_{(p⇑q)[i]}^{i} ⊃ s − t ≤ r_{max}

minmax gap: Lemma

correct(p, s) ∧ correct(q, s)

∧ s ≥ t ∧ s ≤ t_{(p⇓q)[i+1]}^{i+1} ∧ t ≥ t_{(p⇑q)[i]}^{i} ⊃ s − t ≤ r_{max}

drift bnd: Lemma t ≤ s

∧ correct(p, s) ∧ correct(q, s) ∧ |IC_{p}^{i}(t) − IC_{q}^{j}(t)| ≤ Y

⊃ |IC_{p}^{i}(s) − IC_{q}^{j}(s)| ≤ Y + 2 ∗ (s − t) ⋆ ρ

maxsync max: Lemma t_{(p⇑q)[i]}^{i} ≥ t_{p}^{i} ∧ t_{(p⇑q)[i]}^{i} ≥ t_{q}^{i}

minsync min: Lemma t_{(p⇓q)[i]}^{i} ≤ t_{p}^{i} ∧ t_{(p⇓q)[i]}^{i} ≤ t_{q}^{i} accuracy preservation: Lemma

correct(p, t_{p}^{i+1})

∧ correct(q, t_{p}^{i+1})

∧ ( ∀ l, m:

correct(l, t_{p}^{i+1}) ∧ correct(m, t_{p}^{i+1})

⊃ |IC_{l}^{i}(t_{p}^{i+1}) − IC_{m}^{i}(t_{p}^{i+1})| ≤ X)

⊃ |IC_{p}^{i+1}(t_{p}^{i+1}) − IC_{q}^{i}(t_{p}^{i+1})| ≤ α(X + 2 ∗ Λ) + Λ

accuracy pres step0: Lemma |s − t_{1}| ≤ y ∧ |t − t_{2}| ≤ y ∧ |t_{1} − t_{2}| ≤ x ⊃ |s − t| ≤ 2 ∗ y + x

accuracy pres step1: Lemma

correct(p, t_{p}^{i+1}) ∧ correct(l, t_{p}^{i+1}) ∧ correct(m, t_{p}^{i+1})

⊃ |Θ_{p}^{i+1}l) − Θ_{p}^{i+1}m)| ≤ |IC_{l}^{i}(t_{p}^{i+1}) − IC_{m}^{i}(t_{p}^{i+1})| + 2 ∗ Λ

lemma3 1 1: Lemma

correct(p, t) ∧ correct(q, t)

∧ β ≤ r_{min}

∧ μ ≤ X

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X

∧ t ≥ t_{(p⇑q)[i]}^{i}

⊃ |IC_{p}^{i}(t) − IC_{q}^{i}(t)| ≤ X + 2 ∗ (t − t_{(p⇑q)[i]}^{i}) ⋆ ρ

lemma3 1: Lemma correct(p, t)

∧ correct(q, t)

∧ β ≤ r_{min}

∧ μ ≤ X

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X

∧ t ≥ t_{(p⇑q)[i]}^{i} ∧ t < t_{(p⇓q)[i+1]}^{i+1}

⊃ |V C_{p}(t) − V C_{q}(t)| ≤ X + 2 ∗ r_{max} ⋆ ρ lemma3 2 0: Lemma

correct(p, t_{(p⇓q)[i+1]}^{i+1})

∧ correct(q, t_{(p⇓q)[i+1]}^{i+1})

∧ β ≤ r_{min}

∧ μ ≤ X ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ⊃ |IC_{(p⇓q)[i+1]}^{i+1}(t_{(p⇓q)[i+1]}^{i+1})

− IC_{(p⇑q)[i+1]}^{i}(t_{(p⇓q)[i+1]}^{i+1})|
≤ α(X + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ

lemma3 2 1: Lemma

correct(p, t) ∧ correct(q, t)

∧ β ≤ r_{min}

∧ μ ≤ X

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ∧ α(X + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ

∧ t ≥ t_{(p⇓q)[i+1]}^{i+1} ∧ t < t_{(p⇑q)[i+1]}^{i+1}

⊃ |IC_{(p⇓q)[i+1]}^{i+1}(t) − IC_{(p⇑q)[i+1]}^{i}(t)| ≤ δ

lemma3 2 step: Lemma

correct(p, t) ∧ correct(q, t) ∧ β ≤ r_{min} ∧ t ≥ t_{(p⇓q)[i]}^{i} ∧ t < t_{(p⇑q)[i]}^{i} ⊃ t < t_{(p⇓q)[i]}^{i+1}

lemma3 2 step1: Lemma

correct(p, t) ∧ correct(q, t) ∧ β ≤ r_{min} ∧ t ≥ t_{(p⇓q)[i+1]}^{i+1} ⊃ t ≥ t_{(p⇑q)[i+1]}^{i}

lemma3 2 step2: Lemma

correct(p, t) ∧ correct(q, t)

∧ β ≤ r_{min} ∧ t ≥ t_{(p⇓q)[i+1]}^{i+1} ∧ t < t_{(p⇑q)[i+1]}^{i+1} ⊃ |IC_{(p⇓q)[i+1]}^{i+1}(t) − IC_{(p⇑q)[i+1]}^{i}(t)|

= |V C_{(p⇓q)[i+1]}(t) − V C_{(p⇑q)[i+1]}(t)|

lemma3 2 step3: Lemma |V C_{(p⇓q)[i+1]}(t) − V C_{(p⇑q)[i+1]}(t)| = |V C_{p}(t) − V C_{q}(t)| lemma3 2: Lemma correct(p, t)

∧ correct(q, t)

∧ β ≤ r_{min}
∧ μ ≤ X

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, X + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ X ∧ α(X + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ

∧ X + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ t ≥ t_{(p⇑q)[i]}^{i} ∧ t < t_{(p⇑q)[i+1]}^{i+1}
⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ

okayClocks: function[process, process, nat → bool] =

( λ p, q, i: ( ∀ t:

t ≥ 0 ∧ t < t_{(p⇑q)[i]}^{i} ∧ correct(p, t) ∧ correct(q, t)

⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ))

okayClocks defn lr: Lemma

okayClocks(p, q, i)

⊃ ( ∀ t: t ≥ 0 ∧ t < t_{(p⇑q)[i]}^{i} ∧ correct(p, t) ∧ correct(q, t)

⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ)

okayClocks defn rl: Lemma

( ∀ t: t ≥ 0 ∧ t < t_{(p⇑q)[i]}^{i} ∧ correct(p, t) ∧ correct(q, t)

⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ) ⊃ okayClocks(p, q, i)

lemma3 3 0: Lemma μ ≤ δ ⊃ okayClocks(p, q, 0)

lemma3 3 ind: Lemma

β ≤ r_{min} ∧ μ ≤ δ_{S}

∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}

∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ
∧ okayClocks(p, q, i)

⊃ okayClocks(p, q, i + 1) lemma3 3: Lemma β ≤ r_{min}

∧ μ ≤ δ_{S} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}
∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ
⊃ okayClocks(p, q, i)

Proof

okayClocks defn lr pr: Prove okayClocks defn lr from okayClocks {t ← t@CS}

okayClocks defn rl pr: Prove okayClocks defn rl {t ← t@P 1S} from okay-Clocks

accuracy pres step2: Lemma z ≥ 0 ∧ y_{1} − z ≤ y ∧ y_{1} + z ≥ y ⊃ |x − y| ≤ |x − y_{1}| + z

accuracy pres step2 pr: Prove accuracy pres step2 from | ⋆ 1| {x ← x − y}, | ⋆ 1| {x ← x − y_{1}} accuracy preservation pr: Prove

accuracy preservation {l ← l@P 2S, m ← m@P 2S} from accuracy preservation ax

{ppred ← ( λ q: correct(q, t_{p}^{i+1})), γ ← Θ_{p}^{i+1}, X ← X + 2 ∗ Λ},

okay Readpred {Y ← X + 2 ∗ Λ, ppred ← ( λ q: correct(q, t_{p}^{i+1})), γ ← Θ_{p}^{i+1}},

accuracy pres step1 {l ← l@P 2S, m ← m@P 2S}, accuracy pres step2

{z ← Λ,

y_{1} ← Θ_{p}^{i+1}q),

y ← IC_{q}^{i}(t_{p}^{i+1}),

x ← IC_{p}^{i+1}(t_{p}^{i+1})}, ReadClock bnd1, ReadClock bnd2, correct count {t ← t_{p}^{i+1}}, IClock defn {i ← i + 1, t ← t_{p}^{i+1}}, Adj {i ← i + 1}

abs diff 2: Lemma |x − y| ≤ z ⊃ x − y ≤ z ∧ y − x ≤ z

abs diff 2 pr: Prove abs diff 2 from | ⋆ 1| {x ← x − y}

accuracy pres step0 pr: Prove accuracy pres step0 from okay Readvars shift step2, okay Readvars shift step2

{t_{1} ← t_{2},

t_{2} ← t_{1},

s ← t,

t ← s}, abs diff 2 {x ← t_{1}, y ← t_{2}, z ← x}, abs com {x ← s, y ← t} accuracy pres step1 pr: Prove accuracy pres step1 from

accuracy pres step0 {y ← Λ, x ← |IC_{l}^{i}(t_{p}^{i+1}) − IC_{m}^{i}(t_{p}^{i+1})|, s ← Θ_{p}^{i+1}l), t_{1} ← IC_{l}^{i}(t_{p}^{i+1}), t ← Θ_{p}^{i+1}m), t_{2} ← IC_{m}^{i}(t_{p}^{i+1})}, Readerror {q ← l}, Readerror {q ← m}, abs com {x ← IC_{l}^{i}(t_{p}^{i+1}), y ← Θ_{p}^{i+1}l)}, abs com {x ← IC_{m}^{i}(t_{p}^{i+1}), y ← Θ_{p}^{i+1}m)}

lemma3 3 proof: Prove lemma3 3 from lemma3 3 ind {i ← j@P 2S}, readbounds.induction {prop ← ( λ i → bool:

β ≤ r_{min} ∧ μ ≤ δ_{S}
∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}
∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ
⊃ okayClocks(p, q, i))},

lemma3 3 0,

pos product {x ← r_{max}, y ← ρ},

rmax 0, rho 0

lemma3 3 ind proof: Prove lemma3 3 ind from lemma3 2 {t ← t@P 3S, X ← δ_{S}}, okayClocks defn lr {t ← t@P 3S}, okayClocks defn rl {i ← i + 1} lemma3 3 0 proof: Prove lemma3 3 0 from

okayClocks defn rl {i ← 0}, synctime 0 {p ← (p ⇑ q)[0]}, synctime 0, synctime 0 {p ← q}, VClock defn {t ← t@P 1S, i ← 0}, VClock defn {p ← q, t ← t@P 1S, i ← 0}, lemma 2 0, rts1 {t ← t@P 1S, i ← 0}, rts1 {p ← q, t ← t@P 1S, i ← 0}, rmin 0

lemma3 1 1proof: Prove lemma3 1 1 from lemma 2, okaymaxsync defn lr {p ← p, q ← q}, t_{⋆1,⋆2}^{⋆3} , drift bnd {s ← t, t ← t_{(p⇑q)[i]}^{i}, Y ← X, j ← i}, rho 0, correct closed {s ← t, t ← t_{(p⇑q)[i]}^{i}}, correct closed {s ← t, t ← t_{(p⇑q)[i]}^{i}, p ← q}, mult leq {z ← ρ, y ← t − t_{(p⇑q)[i]}^{i}, x ← r_{max}}, maxsync max, minsync min {i ← i + 1}, minmax gap {s ← t, t ← t_{p,q}^{i}}

lemma3 1 proof: Prove lemma3 1 from lemma3 1 1, VClock defn, VClock defn {p ← q}, rts0, mult leq {z ← ρ, y ← t − t_{(p⇑q)[i]}^{i}, x ← r_{max}}, maxsync max, minsync min {i ← i + 1}, rho 0 lemma3 2 0 proof: Prove lemma3 2 0 from

lemma3 1 1 {p ← l@P 2S, q ← m@P 2S, t ← t_{(p⇓q)[i+1]}^{i+1}}, accuracy preservation {p ← (p ⇓ q)[i + 1], q ← (p ⇑ q)[i + 1], X ← X + 2 ∗ (r_{max} + β) ⋆ ρ},

lemma 1 2 {p ← (p ⇓ q)[i + 1], q ← (l@P 2S ⇑ m@P 2S)[i]}, mult leq

{x ← r_{max} + β,

y ← t_{(p⇓q)[i+1]}^{i+1} − t_{(l@P 2S⇑m@P 2S)[i]}^{i}, z ← ρ},

lemma 1 1 {q ← (p ⇓ q)[i + 1], p ← (l@P 2S ⇑ m@P 2S)[i]}, rho 0, minsync correct {i ← i + 1, s ← t_{(p⇓q)[i+1]}^{i+1}}, maxsync correct {i ← i + 1, s ← t_{(p⇓q)[i+1]}^{i+1}}, maxsync correct {p ← l@P 2S, q ← m@P 2S, s ← t_{(p⇓q)[i+1]}^{i+1}},

correct closed {s ← t_{(p⇓q)[i+1]}^{i+1}, t ← t_{(l@P 2S⇑m@P 2S)[i]}^{i}, p ← (l@P 2S ⇑ m@P 2S)[i]} lemma3 2 1 proof: Prove lemma3 2 1 from

lemma3 2 0, VClock defn {p ← (p ⇓ q)[i + 1], i ← i + 1}, VClock defn {p ← (p ⇑ q)[i + 1]}, drift bnd

{s ← t, t ← t_{(p⇓q)[i+1]}^{i+1}, q ← (p ⇑ q)[i + 1], p ← (p ⇓ q)[i + 1], i ← i + 1, j ← i, Y ← α(X + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ},

rho 0, maxsync correct {s ← t, i ← i + 1}, minsync correct {s ← t, i ← i + 1}, correct closed

{p ← (p ⇑ q)[i + 1], s ← t, t ← t_{(p⇓q)[i+1]}^{i+1}},

correct closed {p ← (p ⇓ q)[i + 1], s ← t, t ← t_{(p⇓q)[i+1]}^{i+1}},

correct closed {s ← t, t ← t_{(p⇓q)[i+1]}^{i+1}}, correct closed {p ← q, s ← t, t ← t_{(p⇓q)[i+1]}^{i+1}}, rts1 {i ← i + 1, p ← (p ⇓ q)[i + 1]}, mult leq {z ← ρ, y ← t − t_{(p⇓q)[i+1]}^{i+1}, x ← β}, rts2 {i ← i + 1, p ← (p ⇑ q)[i + 1], q ← (p ⇓ q)[i + 1]}

lemma3 2 proof: Prove lemma3 2 from lemma3 2 1, lemma3 1, lemma3 2 step2, lemma3 2 step3 lemma3 2 step proof: Prove lemma3 2 step from

rts2 {p ← (p ⇑ q)[i], q ← (p ⇓ q)[i]}, rts1 {p ← (p ⇓ q)[i]}, minsync correct {s ← t}, maxsync correct {s ← t}, minsync min, correct closed {p ← (p ⇓ q)[i], s ← t, t ← t_{(p⇓q)[i]}^{i}}

lemma3 2 step1 proof: Prove lemma3 2 step1 from rts2 {p ← (p ⇑ q)[i + 1], q ← (p ⇓ q)[i + 1]}, rts1 {p ← (p ⇓ q)[i + 1]}, minsync correct {s ← t, i ← i + 1}, maxsync correct {s ← t, i ← i + 1}

lemma3 2 step2 proof: Prove lemma3 2 step2 from lemma3 2 step {i ← i + 1}, lemma3 2 step1, VClock defn {p ← (p ⇓ q)[i + 1], i ← i + 1}, VClock defn {p ← (p ⇑ q)[i + 1]}, minsync correct {s ← t, i ← i + 1}, maxsync correct {s ← t, i ← i + 1}

lemma3 2 step3 proof: Prove lemma3 2 step3 from abs com {x ← V C_{p}(t), y ← V C_{q}(t)}, minsync {p ← p, q ← q, i ← i + 1}, (⋆1 ⇑ ⋆2)[⋆3] {p ← p, q ← q, i ← i + 1}

maxmax gap proof: Prove maxmax gap from (⋆1 ⇑ ⋆2)[⋆3] {i ← i+1}, (⋆1 ⇑ ⋆2)[⋆3] , rts0 {t ← s}, rts0 {t ← s, p ← q}

minmax gap proof: Prove minmax gap from minsync maxsync {i ← i + 1}, maxmax gap drift bnd proof: Prove drift bnd from

lemma 2 2a {i ← j}, lemma 2 2a {q ← p}, lemma 2 2b {i ← j}, lemma 2 2b {q ← p}, mult ldistrib minus {x ← s − t, y ← 1, z ← ρ}, mult ldistrib {x ← s − t, y ← 1, z ← ρ}, abs shift

{r ← IC_{p}^{i}(t), s ← IC_{q}^{j}(t), t_{1} ← IC_{p}^{i}(s), t_{2} ← IC_{q}^{j}(s), y ← (s − t) ⋆ 1, z ← (s − t) ⋆ ρ, x ← Y }

maxsync max proof: Prove maxsync max from (⋆1 ⇑ ⋆2)[⋆3]

minsync min proof: Prove minsync min from minsync

End lemma3 lemma final: Module

Using clockassumptions, lemma3, arith, basics

Exporting all with clockassumptions, lemma3

Theory

p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}, i, j, k: Var nat l, m, n: Var int x, y, z: Var number posnumber: Type from number with ( λ x: x ≥ 0) r, s, t: Var posnumber

correct synctime: Lemma correct(p, t) ∧ t < t_{p}^{i} + r_{min} ⊃ t < t_{p}^{i+1}

synctime multiples: Lemma correct(p, t) ∧ t ≥ 0 ∧ t < i ⋆ r_{min} ⊃ t_{p}^{i} > t

synctime multiples bnd: Lemma correct(p, t) ∧ t ≥ 0 ⊃ t < t_{p}^{⌈t/r_{min}⌉+1}

agreement: Lemma β ≤ r_{min}

∧ μ ≤ δ_{S} ∧ π(2 ∗ Λ + 2 ∗ β ⋆ ρ, δ_{S} + 2 ∗ ((r_{max} + β) ⋆ ρ + Λ)) ≤ δ_{S}

∧ δ_{S} + 2 ∗ r_{max} ⋆ ρ ≤ δ
∧ α(δ_{S} + 2 ∗ (r_{max} + β) ⋆ ρ + 2 ∗ Λ) + Λ + 2 ∗ β ⋆ ρ ≤ δ
∧ t ≥ 0 ∧ correct(p, t) ∧ correct(q, t)
⊃ |V C_{p}(t) − V C_{q}(t)| ≤ δ

Proof

agreement proof: Prove agreement from lemma3 3 {i ← ⌈t/r_{min}⌉ + 1}, okayClocks defn lr {i ← ⌈t/r_{min}⌉ + 1, t ← t@CS}, maxsync correct {s ← t, i ← ⌈t/r_{min}⌉ + 1}, synctime multiples bnd {p ← (p ⇑ q)[⌈t/r_{min}⌉ + 1]}, rmin 0, div nonnegative {x ← t, y ← r_{min}}, ceil defn {x ← (t/r_{min})} synctime multiples bnd proof: Prove synctime multiples bnd from

ceil plus mult div {x ← t, y ← r_{min}}, synctime multiples {i ← ⌈t/r_{min}⌉ + 1}, rmin 0, div nonnegative {x ← t, y ← r_{min}}, ceil defn {x ← (t/r_{min})}

correct synctime proof: Prove correct synctime from rts1 {t ← t@CS}

synctime multiples pred: function[nat, nat, posnumber → bool] == ( λ i, p, t: correct(p, t) ∧ t ≥ 0 ∧ t < i ∗ r_{min} ⊃ t_{p}^{i} > t)

synctime multiples step: Lemma correct(p, t) ∧ t ≥ t_{p}^{i} ∧ t ≥ 0 ⊃ t_{p}^{i} ≥ i ⋆ r_{min}

synctime multiples proof: Prove synctime multiples from synctime multiples step

synctime multiples step pred: function[nat, nat, posnumber → bool] == ( λ i, p, t: correct(p, t) ∧ t_{p}^{i} ≤ t ∧ t ≥ 0 ⊃ t_{p}^{i} ≥ i ⋆ r_{min})

synctime multiples step proof: Prove synctime multiples step from

readbounds.induction

{prop ← ( λ i: synctime multiples step pred(i, p, t))}, mult l0 {x ← r_{min}}, synctime 0, rts 1 {i ← j@P 1}, rmin 0, correct closed {s ← t, t ← t_{p}^{j@P 1+1}}, distrib {x ← j@P 1, y ← 1, z ← r_{min}}, mult lident {x ← r_{min}}

End lemma final lemma final tcc: Module

Using lemma final

Exporting all with lemma final

Theory

p: Var naturalnumber

x: Var number

j: Var naturalnumber t: Var posnumber

posnumber TCC1: Formula ( ∃ x: x ≥ 0)

synctime multiples bnd TCC1: Formula (correct(p, t) ∧ t ≥ 0) ⊃ (r_{min} ≠ 0)

synctime multiples bnd TCC2: Formula (correct(p, t) ∧ t ≥ 0) ⊃ (⌈t/r_{min}⌉ + 1 ≥ 0)

agreement proof TCC1: Formula (r_{min} ≠ 0)

agreement proof TCC2: Formula (⌈t/r_{min}⌉ + 1 ≥ 0)

Proof

posnumber TCC1 PROOF: Prove posnumber TCC1

synctime multiples bnd TCC1 PROOF: Prove synctime multiples bnd TCC1

synctime multiples bnd TCC2 PROOF: Prove synctime multiples bnd TCC2

agreement proof TCC1 PROOF: Prove agreement proof TCC1

agreement proof TCC2 PROOF: Prove agreement proof TCC2

End lemma final tcc

ica: Module

Using arith, countmod, clockassumptions, readbounds

Exporting all with clockassumptions

Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time X, Y, Z, R, S, T: Var Clocktime fun, γ, θ: Var function[process → Clocktime] ppred, ppred1, ppred2: Var function[process → bool] sigma size: function[function[process → Clocktime], process → process] =

( λ fun, i: i) sigma: function[function[process → Clocktime], process → Clocktime] =

( λ fun, i: ( if i > 0 then fun(i − 1) + sigma(fun, i − 1) else 0 end if)) by sigma size

fix: function[Clocktime, Clocktime, Clocktime → Clocktime] =

( λ X, Y, Z: ( if |Y − Z| ≤ X then Y else Z end if)) iconv: function[process, function[process → Clocktime], Clocktime

→ Clocktime] =

( λ p, fun, Y: sigma(( λ q: fix(Y, fun(q), fun(p))), N)) icalg: function[process, function[process → Clocktime], Clocktime

→ Clocktime] = ( λ p, fun, Y: iconv(p, fun, Y)/N)

ica translation invariance1: Lemma iconv(p, ( λ q: fun(q) + X), Y) = iconv(p, fun, Y) + N ⋆ X

ica translation invariance: Lemma N > 0 ⊃ icalg(p, ( λ q: fun(q) + X), Y) = icalg(p, fun, Y) + X

extensionality: Axiom ( ∀ l: ppred1(l) = ppred2(l)) ⊃ ppred1 = ppred2 fun1, fun2: Var function[process → time]

fun extensionality: Axiom ( ∀ l: fun1(l) = fun2(l)) ⊃ fun1 = fun2

sigma trans inv: Lemma sigma(( λ q_{1}: fun(q_{1}) + X), n) = sigma(fun, n) + n ⋆ X

Proof

fix trans: Lemma ( λ q:

fix(Y, (( λ q_{1}: fun(q_{1}) + X)q), (( λ q_{1}: fun(q_{1}) + X)p)))

= ( λ q: fix(Y, fun(q), fun(p)) + X)

fix trans pr: Prove fix trans from

fun extensionality {fun1 ← ( λ q: fix(Y, (( λ q_{1}: fun(q_{1}) + X)q), (( λ q_{1}: fun(q_{1}) + X)p))), fun2 ← ( λ q: fix(Y, fun(q), fun(p)) + X)},

fix {X ← Y, Y ← (( λ q_{1}: fun(q_{1}) + X)l@P 1S), Z ← (( λ q_{1}: fun(q_{1}) + X)p)},

fix {X ← Y, Y ← fun(l@P 1S), Z ← fun(p)}

sigma trans inv base: Lemma sigma(( λq_{1}: fun(q_{1})+X), 0) = sigma(fun, 0)

sigma trans inv base pr: Prove sigma trans inv base from sigma {i ← 0}, sigma {fun ← ( λ q_{1}: fun(q_{1}) + X), i ← 0}

sigma trans inv ind: Lemma

sigma(( λ q_{1}: fun(q_{1}) + X), j) = sigma(fun, j) + j ⋆ X ⊃ sigma(( λ q_{1}: fun(q_{1}) + X), j + 1) = sigma(fun, j + 1) + (j + 1) ⋆ X

sigma trans inv ind pr: Prove sigma trans inv ind from sigma {fun ← ( λ q_{1}: fun(q_{1}) + X), i ← j + 1}, sigma {i ← j + 1}, distrib {x ← j, y ← 1, z ← X}, mult lident {x ← X} sigma trans inv pr: Prove sigma trans inv from

induction {prop ← ( λ n: sigma(( λ q_{1}: fun(q_{1}) + X), n) = sigma(fun, n) + n ⋆ X), i ← n},

sigma trans inv base, sigma trans inv ind {j ← j@P 1}, mult l0 {x ← X}

ica translation invariance1 pr: Prove ica translation invariance1 from iconv, iconv {fun ← ( λ q: fun(q) + X)}, fix trans, sigma trans inv {fun ← ( λ q: fix(Y, fun(q), fun(p))), n ← N}

ica translation invariance pr: Prove ica translation invariance from ica translation invariance1, icalg, icalg {fun ← ( λ q: fun(q) + X)}, div distrib {x ← iconv(p, fun, Y), y ← N ⋆ X, z ← N}, div cancel {x ← N, y ← X}

End ica ica2: Module

Using arith, countmod, clockassumptions, readbounds, ica

Exporting all with ica

Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time D, X, Y, Z, R, S, T: Var Clocktime fun, fun1, fun2, γ, θ: Var function[process → Clocktime] ppred, ppred1, ppred2: Var function[process → bool]

sigma split: Lemma

sigma(fun, i) = sigma(( λ q: ( if ppred(q) then fun(q) else 0 end if)), i) + sigma(( λ q: ( if ¬ppred(q) then fun(q) else 0 end if)), i)

sigma pos: Lemma okay pairs(fun1, fun2, X, ppred)

⊃ sigma(( λq: ( if ppred(q) then (fun1(q)−fun2(q)) else 0 end if)), i) ≤ count(ppred, i) ⋆ X

okay pairs fix: Lemma Z ≥ 0 ∧ ppred(p)

∧ ppred(q) ∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ okay pairs(( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p))), ( λ q_{1}: fix(Y, fun2(q_{1}), fun2(q))), ( if Z ≤ Y then X else X + Z end if), ppred) sigma diff: Lemma

sigma(fun1, i) − sigma(fun2, i) = sigma(( λ q: fun1(q) − fun2(q)), i)

sigma neg: Lemma Y ≥ 0 ∧ fun1(p) − fun2(q) ≤ z

⊃ sigma(( λ q_{1}:

( if ¬ppred(q_{1})

then (fix(Y, fun1(q_{1}), fun1(p))−fix(Y, fun2(q_{1}), fun2(q))) else 0 end if)),

i) ≤ count(( λ q_{1}: ¬ppred(q_{1})), i) ⋆ (z + 2 ∗ Y)

sigma pos neg: Lemma

Y ≥ 0 ∧ Z ≥ 0 ∧ ppred(p)

∧ ppred(q)

∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ sigma(( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p)) − fix(Y, fun2(q_{1}), fun2(q))), i)

≤ count(ppred, i) ⋆ ( if Z ≤ Y then X else X + Z end if) + count(( λ q_{1}: ¬ppred(q_{1})), i) ⋆ (X + Z + 2 ∗ Y)

iconv sigma diff: Lemma

Y ≥ 0 ∧ Z ≥ 0 ∧ ppred(p)

∧ ppred(q)

∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ iconv(p, fun1, Y) − iconv(q, fun2, Y)

≤ count(ppred, N) ⋆ ( if Z ≤ Y then X else X + Z end if) + count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Y)

okay Readpred pairs: Lemma

ppred(p) ∧ ppred(q)

∧ okay pairs(fun1, fun2, X, ppred) ∧ okay Readpred(fun1, Z, ppred) ⊃ fun1(p) − fun2(q) ≤ X + Z

okay Readpred lr: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun1, Z, ppred)

⊃ |fun1(p) − fun1(q)| ≤ Z okay pairs lr: Lemma

ppred(p) ∧ okay pairs(fun1, fun2, X, ppred) ⊃ |fun1(p) − fun2(p)| ≤ X

Proof

okay Readpred pairs pr: Prove okay Readpred pairs from okay pairs {γ ← fun1, θ ← fun2, p_{3} ← q}, abs leq 0 {x ← fun1(q), y ← fun2(q), z ← X}, okay Readpred {γ ← fun1, Y ← Z, l ← p, m ← q}, abs leq 0 {x ← fun1(p), y ← fun1(q), z ← Z}

iconv sigma diff pr: Prove iconv sigma diff from sigma pos neg {i ← N}, sigma diff

{fun1 ← ( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p))),

fun2 ← ( λ q_{1}: fix(Y, fun2(q_{1}), fun2(q))),

i ← N}, iconv {fun ← fun1}, iconv {p ← q, fun ← fun2}

sigma pos neg pr: Prove sigma pos neg from

sigma pos {fun1 ← ( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p))), fun2 ← ( λ q_{1}: fix(Y, fun2(q_{1}), fun2(q))), X ← ( if Z ≤ Y then X else X + Z end if)},

sigma neg {z ← X + Z}, okay pairs fix, okay Readpred pairs, sigma split

{fun ← ( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p)) − fix(Y, fun2(q_{1}), fun2(q)))}

fix diff1: Lemma Z ≥ 0 ∧ |fun1(p_{3}) − fun2(p_{3})| ≤ X

∧ |fun1(p_{3}) − fun1(p)| ≤ Z ⊃ |fix(Y, fun1(p_{3}), fun1(p)) − fun2(p_{3})|

≤ ( if Z ≤ Y then X else X + Z end if) fix diff1 pr: Prove fix diff1 from

fix {X ← Y, Y ← fun1(p_{3}), Z ← fun1(p)}, abs drift

{x_{1} ← fun1(p), y ← fun2(p_{3}), x ← fun1(p_{3}), z ← X, z_{1} ← Z},

abs com {x ← fun1(p), y ← fun1(p_{3})}

fix diff2: Lemma |fun1(p_{3}) − fun2(p_{3})| ≤ X ∧ |fun2(p_{3}) − fun2(q)| ≤ Z ⊃ |fun1(p_{3}) − fun2(q)| ≤ X + Z

fix diff2 pr: Prove fix diff2 from

abs drift {x_{1} ← fun1(p_{3}), y ← fun2(q), x ← fun2(p_{3}), z_{1} ← X, z ← Z}

fix diff3: Lemma |fun1(q) − fun2(q)| ≤ X ∧ |fun1(p) − fun1(q)| ≤ Z ⊃ |fun1(p) − fun2(q)| ≤ X + Z

fix diff3 pr: Prove fix diff3 from

abs drift {x_{1} ← fun1(p), y ← fun2(q), x ← fun1(q), z_{1} ← Z, z ← X} fix diff: Lemma Z ≥ 0

∧ |fun1(p_{3}) − fun2(p_{3})| ≤ X

∧ |fun1(q) − fun2(q)| ≤ X
∧ |fun1(p_{3}) − fun1(p)| ≤ Z

∧ |fun2(p_{3}) − fun2(q)| ≤ Z ∧ |fun1(p) − fun1(q)| ≤ Z ⊃ |fix(Y, fun1(p_{3}), fun1(p)) − fix(Y, fun2(p_{3}), fun2(q))|

≤ ( if Z ≤ Y then X else X + Z end if)

fix diff pr: Prove fix diff from fix {X ← Y, Y ← fun1(p_{3}), Z ← fun1(p)}, fix {X ← Y, Y ← fun2(p_{3}), Z ← fun2(q)}, fix diff1, fix diff2, fix diff3

okay pairs lr pr: Prove okay pairs lr from okay pairs {γ ← fun1, θ ← fun2, p_{3} ← p}

okay Readpred lr pr: Prove okay Readpred lr from okay Readpred {γ ← fun1, Y ← Z, l ← p, m ← q}

fix diff corr: Lemma

Z ≥ 0 ∧ ppred(p)

∧ ppred(q)

∧ ppred(p_{3})

∧ okay pairs(fun1, fun2, X, ppred)

∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ |fix(Y, fun1(p_{3}), fun1(p)) − fix(Y, fun2(p_{3}), fun2(q))| ≤ ( if Z ≤ Y then X else X + Z end if)

fix diff corr pr: Prove fix diff corr from fix diff, okay pairs lr {p ← p_{3}}, okay pairs lr {p ← q}, okay Readpred lr {p ← p_{3}, q ← p}, okay Readpred lr {fun1 ← fun2, p ← p_{3}}, okay Readpred lr okay pairs fix pr: Prove okay pairs fix from

okay pairs {γ ← ( λ q_{1}: fix(Y, fun1(q_{1}), fun1(p))), θ ← ( λ q_{1}: fix(Y, fun2(q_{1}), fun2(q))), X ← ( if Z ≤ Y then X else X + Z end if)},

fix diff corr {p_{3} ← p_{3}@P1S}

sigma neg ind step: Lemma

Y ≥ 0 ∧ fun1(p) − fun2(q) ≤ z ⊃ fix(Y, fun1(i), fun1(p)) − fix(Y, fun2(i), fun2(q)) ≤ z + 2 ∗ Y

sigma neg ind step pr: Prove sigma neg ind step from fix {X ← Y, Y ← fun1(i), Z ← fun1(p)}, fix {X ← Y, Y ← fun2(i), Z ← fun2(q)}, abs leq 0 {x ← fun1(i), y ← fun1(p), z ← Y }, abs com {x ← fun2(i), y ← fun2(q)}, abs leq 0 {x ← fun2(q), y ← fun2(i), z ← Y }

sigma neg ind: Lemma

Y ≥ 0 ∧ fun1(p) − fun2(q) ≤ z

∧ sigma(( λ q_{1}:

( if ¬ppred(q_{1})

then fix(Y, fun1(q_{1}), fun1(p)) − fix(Y, fun2(q_{1}), fun2(q))

else 0 end if)),

i) ≤ count(( λ q_{1}: ¬ppred(q_{1})), i) ⋆ (z + 2 ∗ Y)

⊃ sigma(( λ q_{1}:

( if ¬ppred(q_{1}) then fix(Y, fun1(q_{1}), fun1(p))−fix(Y, fun2(q_{1}), fun2(q)) else 0 end if)),

i + 1)
≤ count(( λ q_{1}: ¬ppred(q_{1})), i + 1) ⋆ (z + 2 ∗ Y)

sigma neg ind pr: Prove sigma neg ind from

sigma

{fun ← ( λ q_{1}:

( if ¬ppred(q_{1})

then fix(Y, fun1(q_{1}), fun1(p)) − fix(Y, fun2(q_{1}), fun2(q)) else 0 end if)),

i ← i + 1}, count {ppred ← ( λ q_{1}: ¬ppred(q_{1})), i ← i + 1}, sigma neg ind step, distrib

{x ← 1,

y ← count(( λ q_{1}: ¬ppred(q_{1})), i), z ← z + 2 ∗ Y },

mult lident {x ← z + 2 ∗ Y } sigma neg pr: Prove sigma neg from

induction

{prop ← ( λ i:

Y ≥ 0 ∧ fun1(p) − fun2(q) ≤ z

⊃ sigma(( λ q_{1}:

if ¬ppred(q_{1})

then (fix(Y, fun1(q_{1}), fun1(p))

− fix(Y, fun2(q_{1}), fun2(q))) else 0 end if),

i) ≤ count(( λ q_{1}: ¬ppred(q_{1})), i) ⋆ (z + 2 ∗ Y))},

sigma

{fun ← ( λ q_{1}:

( if ¬ppred(q_{1})

then fix(Y, fun1(q_{1}), fun1(p)) − fix(Y, fun2(q_{1}), fun2(q)) else 0 end if)),

i ← 0}, count {i ← 0, ppred ← ( λ q_{1}: ¬ppred(q_{1}))}, mult l0 {x ← z + 2 ∗ Y }, sigma neg ind {i ← j@P 1S}

sigma diff ind: Lemma

sigma(fun1, i) − sigma(fun2, i) = sigma(( λ q: fun1(q) − fun2(q)), i)

⊃ sigma(fun1, i + 1) − sigma(fun2, i + 1) = sigma(( λ q: fun1(q) − fun2(q)), i + 1)

sigma diff ind pr: Prove sigma diff ind from sigma {fun ← fun1, i ← i + 1}, sigma {fun ← fun2, i ← i + 1}, sigma {fun ← ( λ q: fun1(q) − fun2(q)), i ← i + 1} sigma diff pr: Prove sigma diff from

induction

{prop ← ( λ i:

sigma(fun1, i) − sigma(fun2, i)

= sigma(( λ q: fun1(q) − fun2(q)), i))},

sigma {fun ← fun1, i ← 0}, sigma {fun ← fun2, i ← 0}, sigma {fun ← ( λ q: fun1(q) − fun2(q)), i ← 0}, sigma diff ind {i ← j@P 1S}

sigma pos ind: Lemma

okay pairs(fun1, fun2, X, ppred)

∧sigma(( λq: ( if ppred(q) then (fun1(q)−fun2(q)) else 0 end if)), i)

≤ count(ppred, i) ⋆ X ⊃ sigma(( λ q: ( if ppred(q) then (fun1(q) − fun2(q)) else 0 end if)),

i + 1) ≤ count(ppred, i + 1) ⋆ X

sigma pos ind pr: Prove sigma pos ind from

sigma {fun ← ( λ q: ( if ppred(q) then (fun1(q) − fun2(q)) else 0 end if)), i ← i + 1},

okay pairs {γ ← fun1, θ ← fun2, p_{3} ← i}, count {i ← i + 1}, distrib {x ← 1, y ← count(ppred, i), z ← X}, mult lident {x ← X}, abs leq 0 {x ← fun1(i), y ← fun2(i), z ← X} sigma pos pr: Prove sigma pos from

induction

{prop ← ( λ i:

okay pairs(fun1, fun2, X, ppred)

⊃ sigma(( λ q:

( if ppred(q)

then (fun1(q) − fun2(q)) else 0

end if)),

i) ≤ count(ppred, i) ⋆ X)},

sigma {fun ← ( λ q: ( if ppred(q) then (fun1(q) − fun2(q)) else 0 end if)), i ← 0},

count {i ← 0}, mult l0 {x ← X}, sigma pos ind {i ← j@P 1S}

sigma split ind: Lemma

sigma(fun, i) = sigma(( λ q: ( if ppred(q) then fun(q) else 0 end if)), i)

+ sigma(( λ q: ( if ¬ppred(q) then fun(q) else 0 end if)), i) ⊃ sigma(fun, i + 1)

= sigma(( λ q: ( if ppred(q) then fun(q) else 0 end if)), i + 1) + sigma(( λ q: ( if ¬ppred(q) then fun(q) else 0 end if)), i + 1)

sigma split ind pr: Prove sigma split ind from sigma {i ← i + 1}, sigma

{fun ← ( λ q: ( if ppred(q) then fun(q) else 0 end if)),

i ← i + 1}, sigma

{fun ← ( λ q: ( if ¬ppred(q) then fun(q) else 0 end if)),

i ← i + 1} sigma split pr: Prove sigma split from

induction

{prop ← ( λ i:

sigma(fun, i) = sigma(( λ q: ( if ppred(q) then fun(q) else 0 end if)), i) +sigma(( λq: ( if ¬ppred(q) then fun(q) else 0 end if)), i))},

sigma {i ← 0},

sigma {fun ← ( λ q: ( if ppred(q) then fun(q) else 0 end if)), i ← 0},

sigma {fun ← ( λ q: ( if ¬ppred(q) then fun(q) else 0 end if)), i ← 0},

sigma split ind {i ← j@P 1S}

End ica2

ica3: Module

Using arith, countmod, clockassumptions, readbounds, ica, ica2

Exporting all with clockassumptions, ica2

Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time D, X, Y, Z, R, S, T: Var Clocktime fun, fun1, fun2, γ, θ: Var function[process → Clocktime] ppred, ppred1, ppred2: Var function[process → bool] Δ: Clocktime

Delta 0: Axiom Δ ≥ 0

mult sum ineq: Lemma m + n = p + q ∧ n ≤ q ∧ x ≤ y ⊃ m ⋆ x + n ⋆ y ≤ p ⋆ x + q ⋆ y

count complement: Lemma count(( λq: ¬ppred(q)), n) = n−count(ppred, n)

prec enh step3: Lemma

count(ppred, N) ≥ N − maxfaults ∧ X ≥ 0 ∧ Y ≥ 0 ∧ Z ≥ 0

⊃ count(ppred, N) ⋆ ( if Z ≤ Y then X else X + Z end if) + count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Y)

≤ N − maxfaults ⋆ ( if Z ≤ Y then X else X + Z end if) + maxfaults ⋆ (X + Z + 2 ∗ Y)

icalg Pi: function[Clocktime, Clocktime → Clocktime] =

( λ X, Z: (N − maxfaults ⋆ ( if Z ≤ Δ then X else X + Z end if)

+ maxfaults ⋆ (X + Z + 2 ∗ Δ)) /N) prec enh step: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun1, Z, ppred) ⊃ Z ≥ 0

prec enh step2: Lemma ppred(p)∧okay pairs(fun1, fun2, X, ppred) ⊃ X ≥ 0

icalg precision enhancement step: Lemma

ppred(p) ∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ icalg(p, fun1, Δ) − icalg(q, fun2, Δ)

≤ (count(ppred, N) ⋆ ( if Z ≤ Δ then X else X + Z end if)

+ count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Δ)) /N

icalg Mu: function[Clocktime, Clocktime, function[process → bool] → Clocktime] =

( λ X, Z, ppred:

(count(ppred, N) ⋆ ( if Z ≤ Δ then X else X + Z end if) + count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Δ))

/N)

icalg precision enhancement: Lemma

ppred(p) ∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ icalg(p, fun1, Δ) − icalg(q, fun2, Δ) ≤ icalg Pi(X, Z)

Proof

prec enh step4: Lemma

N > 0 ∧ ppred(p)

∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay pairs(fun1, fun2, X, ppred) ∧okay Readpred(fun1, Z, ppred)∧okay Readpred(fun2, Z, ppred)

⊃ icalg Mu(X, Z, ppred) ≤ icalg Pi(X, Z)

prec enh step4 pr: Prove prec enh step4 from prec enh step, prec enh step2, prec enh step3 {Y ← Δ}, Delta 0, icalg Pi, icalg Mu, div ineq

{x ← count(ppred, N) ⋆ ( if Z ≤ Δ then X else X + Z end if)

+ count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Δ), y ← (N − maxfaults) ⋆ ( if Z ≤ Δ then X else X + Z end if)

+ maxfaults ⋆ (X + Z + 2 ∗ Δ), z ← N}

icalg precision enhancement pr: Prove icalg precision enhancement from prec enh step4, N 0, icalg precision enhancement step, icalg Mu icalg precision enhancement step pr: Prove icalg precision enhancement step

from prec enh step, prec enh step2, iconv sigma diff {Y ← Δ}, N 0, icalg {fun ← fun1, Y ← Δ}, icalg {p ← q, fun ← fun2, Y ← Δ}, div minus distrib

{x ← iconv(p, fun1, Δ),

y ← iconv(q, fun2, Δ),

z ← N}, Delta 0, div ineq

{x ← iconv(p, fun1, Δ) − iconv(q, fun2, Δ), y ← count(ppred, N) ⋆ ( if Z ≤ Δ then X else X + Z end if)

+ count(( λ q_{1}: ¬ppred(q_{1})), N) ⋆ (X + Z + 2 ∗ Δ), z ← N}

prec enh step3 pr: Prove prec enh step3 from count complement {n ← N}, mult sum ineq

{m ← count(ppred, N),

n ← count(( λ q: ¬ppred(q)), N),

p ← N − maxfaults,

q ← maxfaults,

x ← ( if Z ≤ Y then X else X + Z end if),

y ← X + Z + 2 ∗ Y }

prec enh step2 pr: Prove prec enh step2 from okay pairs lr, | ⋆ 1| {x ← fun1(p) − fun2(p)} count complement pr: Prove count complement from

induction {prop ← ( λ n: count(( λ q: ¬ppred(q)), n) = n − count(ppred, n)), i ← n},

count {ppred ← ( λ q: ¬ppred(q)), i ← 0}, count {i ← 0}, count {ppred ← ( λ q: ¬ppred(q)), i ← j@P 1S + 1}, count {i ← j@P 1S + 1}

mult sum ineq pr: Prove mult sum ineq from distrib {x ← n, y ← q − n, z ← y}, distrib {x ← p, y ← m − p, z ← x}, mult leq 2 {z ← q − n, x ← y, y ← x}

prec enh step pr: Prove prec enh step from okay Readpred lr, | ⋆ 1| {x ← fun1(p) − fun1(q)}

End ica3

ica4: Module

Using arith, countmod, clockassumptions, readbounds, ica, ica2, ica3

Exporting all with clockassumptions, ica3

Theory

process: Type is nat event: Type is nat time: Type is number Clocktime: Type is number l, m, n, p, q, p_{1}, p_{2}, q_{1}, q_{2}, p_{3}, q_{3}: Var process i, j, k: Var event x, y, z, r, s, t: Var time D, X, Y, Z, R, S, T: Var Clocktime fun, fun1, fun2, γ, θ: Var function[process → Clocktime] ppred, ppred1, ppred2: Var function[process → bool]

sigma duplicate: Lemma sigma(( λ i: x), i) = i ⋆ x

okay Readpred fix diff: Lemma

ppred(p) ∧ ppred(q) ∧ ppred(p_{1}) ∧ okay Readpred(fun, X, ppred) ⊃ |fix(Y, fun(p_{1}), fun(p)) − fun(q)| ≤ X

okay Readpred fix diff2: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun, X, ppred) ∧ Y ≥ 0 ⊃ |fix(Y, fun(p_{1}), fun(p)) − fun(q)| ≤ X + Y

acc pres sigma pos: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun, X, ppred)

⊃ sigma(( λ p_{1}:

( if ppred(p_{1})

then |fix(Y, fun(p_{1}), fun(p)) − fun(q)| else 0 end if)),

N) ≤ count(ppred, N) ⋆ X

acc pres sigma neg: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun, X, ppred) ∧ Y ≥ 0

⊃ sigma(( λ p_{1}:

( if ¬ppred(p_{1}) then |fix(Y, fun(p_{1}), fun(p)) − fun(q)| else 0 end if)),

N) ≤ count(( λ p_{1}: ¬ppred(p_{1})), N) ⋆ (X + Y)

sigma abs: Lemma |sigma(fun, i)| ≤ sigma(( λ p: |fun(p)|), i)

acc pres step: Lemma

ppred(p) ∧ ppred(q) ∧ okay Readpred(fun, X, ppred)

⊃ |iconv(p, fun, Δ) − N ⋆ fun(q)| ≤ count(ppred, N) ⋆ X + count(( λ p: ¬ppred(p)), N) ⋆ (X + Δ)

icalg accuracy preservation: Lemma

ppred(p) ∧ ppred(q)

∧count(ppred, N) ≥ N −maxfaults∧okay Readpred(fun, X, ppred) ⊃ |icalg(p, fun, Δ) − fun(q)|

≤ ((N − maxfaults) ⋆ X + maxfaults ⋆ (X + Δ))/N

Proof

icalg accuracy preservation pr: Prove icalg accuracy preservation from acc pres step, N 0, abs div {x ← iconv(p, fun, Δ) − N ⋆ fun(q), y ← N}, icalg {Y ← Δ}, div cancel {x ← N, y ← fun(q)}, mult sum ineq

{m ← count(ppred, N),

n ← count(( λ p: ¬ppred(p)), N),

p ← N − maxfaults,

q ← maxfaults,

x ← X,

y ← X + Δ}, Delta 0, count complement {n ← N}, div minus distrib {z ← N, x ← iconv(p, fun, Δ), y ← N ⋆ fun(q)}, div ineq

{z ← N,

x ← |iconv(p, fun, Δ) − N ⋆ fun(q)|,

y ← (N − maxfaults) ⋆ X + maxfaults ⋆ (X + Δ)}

acc pres step pr: Prove acc pres step from

sigma split {fun ← ( λ p_{1}: |fix(Δ, fun(p_{1}), fun(p)) − fun(q)|), i ← N},

sigma abs {fun ← ( λ p_{1}: fix(Δ, fun(p_{1}), fun(p)) − fun(q)), i ← N}, sigma diff

{fun1 ← ( λ p_{1}: fix(Δ, fun(p_{1}), fun(p))),

fun2 ← ( λ p_{1}: fun(q)),

i ← N}, acc pres sigma neg {Y ← Δ}, acc pres sigma pos {Y ← Δ}, iconv {Y ← Δ}, sigma duplicate {x ← fun(q), i ← N}, Delta 0 sigma abs pr: Prove sigma abs from

induction {prop ← ( λ i: |sigma(fun, i)| ≤ sigma(( λ p: |fun(p)|), i))}, sigma {i ← 0}, | ⋆ 1| {x ← 0}, sigma {i ← 0, fun ← ( λ p: |fun(p)|)}, sigma {i ← j@P 1S + 1}, sigma {i ← j@P 1S + 1, fun ← ( λ p: |fun(p)|)}, abs plus {x ← sigma(fun, j@P 1S), y ← fun(j@P 1S)}

acc pres sigma neg pr: Prove acc pres sigma neg from

sigma pos {i ← N, fun1 ← ( λ p_{1}: |fix(Y, fun(p_{1}), fun(p)) − fun(q)|), fun2 ← ( λ p_{1} → number: 0), ppred ← ( λ p_{1}: ¬ppred(p_{1})), X ← X + Y },

okay pairs {γ ← ( λ p_{1}: |fix(Y, fun(p_{1}), fun(p)) − fun(q)|), θ ← ( λ p_{1} → number: 0), X ← X + Y, ppred ← ( λ p_{1}: ¬ppred(p_{1}))},

okay Readpred fix diff2 {p_{1} ← p_{3}@P2S}, | ⋆ 1| {x ← |fix(Y, fun(p_{3}@P2S), fun(p)) − fun(q)|}, | ⋆ 1| {x ← fix(Y, fun(p_{3}@P2S), fun(p)) − fun(q)}

acc pres sigma pos pr: Prove acc pres sigma pos from

sigma pos {i ← N, fun1 ← ( λ p_{1}: |fix(Y, fun(p_{1}), fun(p)) − fun(q)|), fun2 ← ( λ p_{1} → number: 0)},

okay pairs {γ ← ( λ p_{1}: |fix(Y, fun(p_{1}), fun(p)) − fun(q)|), θ ← ( λ p_{1} → number: 0)},

okay Readpred fix diff {p_{1} ← p_{3}@P2S}, | ⋆ 1| {x ← |fix(Y, fun(p_{3}@P2S), fun(p)) − fun(q)|}, | ⋆ 1| {x ← fix(Y, fun(p_{3}@P2S), fun(p)) − fun(q)} okay Readpred fix diff2 pr: Prove okay Readpred fix diff2 from

okay Readpred lr {fun1 ← fun, Z ← X}, fix {X ← Y, Y ← fun(p_{1}), Z ← fun(p)}, abs drift

{x_{1} ← fun(p_{1}), y ← fun(q), x ← fun(p), z ← X, z_{1} ← Y }

okay Readpred fix diff pr: Prove okay Readpred fix diff from okay Readpred lr {fun1 ← fun, Z ← X}, okay Readpred lr {fun1 ← fun, p ← p_{1}, Z ← X}, fix {X ← Y, Y ← fun(p_{1}), Z ← fun(p)}

sigma duplicate pr: Prove sigma duplicate from induction {prop ← ( λ i: sigma(( λ i: x), i) = i ⋆ x)}, sigma {i ← 0, fun ← ( λ i: x)}, ⋆1 ⋆ ⋆2 {x ← 0, y ← x}, sigma {i ← j@P 1S, fun ← ( λ i: x)}, sigma {i ← j@P 1S + 1, fun ← ( λ i: x)}, distrib {x ← j@P 1S, y ← 1, z ← x}, ⋆1 ⋆ ⋆2 {x ← 1, y ← x}

End ica4 ica tcc: Module

Using ica Exporting all with ica Theory

i: Var naturalnumber fun: Var function[naturalnumber → number] j: Var naturalnumber l: Var naturalnumber sigma TCC1: Formula (i > 0) ⊃ (i − 1 ≥ 0) sigma TCC2: Formula (i > 0)

⊃ sigma size(fun, i) > sigma size(fun, i − 1)

icalg TCC1: Formula (N ≠ 0)

Proof

sigma TCC1 PROOF: Prove sigma TCC1 sigma TCC2 PROOF: Prove sigma TCC2 icalg TCC1 PROOF: Prove icalg TCC1

End ica tcc ica4 tcc: Module

Using ica4 Exporting all with ica4 Theory

p: Var naturalnumber q: Var naturalnumber X: Var number fun: Var function[naturalnumber → number] ppred: Var function[naturalnumber → boolean] p_{3}: Var naturalnumber j: Var naturalnumber icalg accuracy preservation TCC1: Formula

(ppred(p) ∧ ppred(q)

∧count(ppred, N) ≥ N−maxfaults∧okay Readpred(fun, X, ppred)) ⊃ (N ≠ 0)

icalg accuracy preservation pr TCC1: Formula (N − maxfaults ≥ 0)

Proof

icalg accuracy preservation TCC1 PROOF: Prove

icalg accuracy preservation TCC1 icalg accuracy preservation pr TCC1 PROOF: Prove

icalg accuracy preservation pr TCC1 End ica4 tcc ica3 tcc: Module

Using ica3

Exporting all with ica3

Theory

p: Var naturalnumber q: Var naturalnumber X: Var number Z: Var number fun1: Var function[naturalnumber → number] fun2: Var function[naturalnumber → number] ppred: Var function[naturalnumber → boolean] j: Var naturalnumber

icalg Pi TCC1: Formula (N ≠ 0)

icalg precision enhancement step TCC1: Formula

(ppred(p) ∧ ppred(q)

∧ count(ppred, N) ≥ N − maxfaults ∧ okay pairs(fun1, fun2, X, ppred) ∧ okay Readpred(fun1, Z, ppred) ∧ okay Readpred(fun2, Z, ppred))

⊃ (N ≠ 0)

prec enh step3 pr TCC1: Formula (N − maxfaults ≥ 0)

Proof

icalg Pi TCC1 PROOF: Prove icalg Pi TCC1

icalg precision enhancement step TCC1 PROOF: Prove icalg precision enhancement step TCC1

prec enh step3 pr TCC1 PROOF: Prove prec enh step3 pr TCC1

End ica3 tcc tcc proofs: Module

Using countmod tcc, lemma final tcc, division, clockassumptions, ica tcc,

ica4 tcc, ica3 tcc

Exporting all

with countmod tcc, lemma final tcc, division, clockassumptions, ica tcc, ica4 tcc, ica3 tcc

Proof

countmod TCC4 pr: Prove count TCC4 from countsize, countsize {i ← ( if i > 0 then i − 1 else i end if)}

countmod TCC5 pr: Prove count TCC5 from countsize, countsize {i ← ( if i > 0 then i − 1 else i end if)}

posnumber TCC1 PROOF: Prove posnumber TCC1 {x ← 0}

synctime multiples bnd TCC1 PROOF: Prove synctime multiples bnd TCC1 from

rmin 0

synctime multiples bnd TCC2 PROOF: Prove synctime multiples bnd TCC2 from

div nonnegative {x ← t, y ← r_{min}}, rmin 0, ceil defn {x ← t/r_{min}}

agreement proof TCC1 PROOF: Prove agreement proof TCC1 from rmin 0

agreement proof TCC2 PROOF: Prove agreement proof TCC2 from div nonnegative {x ← t, y ← r_{min}}, rmin 0, ceil defn {x ← t/r_{min}}

sigma TCC2 PROOF: Prove sigma TCC2 from sigma size, sigma size {i ← ( if i > 0 then i − 1 else 0 end if)}

icalg TCC1 PROOF: Prove icalg TCC1 from N 0

icalg Pi TCC1 PROOF:

Prove icalg Pi TCC1 from N 0 icalg precision enhancement step TCC1 PROOF: Prove

icalg precision enhancement step TCC1 from N 0 prec enh step3 pr TCC1 PROOF: Prove

prec enh step3 pr TCC1 from N maxfaults icalg accuracy preservation TCC1 PROOF: Prove

icalg accuracy preservation TCC1 from N 0 icalg accuracy preservation pr TCC1 PROOF: Prove

icalg accuracy preservation pr TCC1 from N maxfaults End tcc proofs tcc proofs tcc: Module

Using tcc proofs Exporting all with tcc proofs Theory

t: Var lemma final.posnumber i: Var naturalnumber countmod TCC4 pr TCC1: Formula (( if i > 0 then i−1 else i end if) ≥

0)

synctime multiples bnd TCC2 PROOF TCC1: Formula (r_{min} ≠ 0) sigma TCC2 PROOF TCC1: Formula (( if i > 0 then i−1 else 0 end if) ≥

0)

Proof

countmod TCC4 pr TCC1 PROOF: Prove countmod TCC4 pr TCC1 synctime multiples bnd TCC2 PROOF TCC1 PROOF: Prove

synctime multiples bnd TCC2 PROOF TCC1 sigma TCC2 PROOF TCC1 PROOF: Prove sigma TCC2 PROOF TCC1

End tcc proofs tcc

top: Module Using arith, lemma final, ica4, tcc proofs, tcc proofs tcc, division tcc Theory Proof

synctime multiples bnd TCC2 PROOF TCC1: Prove

synctime multiples bnd TCC2 PROOF TCC1 from rmin 0

End top

Appendix C

Proof Chain Analysis

The dependency analysis automatically establishes that there are no unproved statements in the proof that are not axioms or definitions.

C.1 Proof Chain for Agreement

Terse proof chain for proof agreement_proof in module
lemma_final
Use of the formula
lemma_final.synctime_multiples_bnd
requires the following TCCs to be proven
lemma_final_tcc.posnumber_TCC1
lemma_final_tcc.synctime_multiples_bnd_TCC1
lemma_final_tcc.synctime_multiples_bnd_TCC2
lemma_final_tcc.agreement_proof_TCC1
lemma_final_tcc.agreement_proof_TCC2
Use of the formula
division.div_nonnegative
requires the following TCCs to be proven
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1

division_tcc.div_cancel_TCC1
division_tcc.ceil_mult_div_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
 ================== SUMMARY ==================
The proof chain is complete
The axioms and assumptions at the base are:
clockassumptions.IClock_defn
clockassumptions.Readerror
clockassumptions.VClock_defn
clockassumptions.accuracy_preservation_ax
clockassumptions.beta_0
clockassumptions.correct_closed
clockassumptions.correct_count
clockassumptions.init
clockassumptions.mu_0
clockassumptions.precision_enhancement_ax
clockassumptions.rate_1
clockassumptions.rate_2

clockassumptions.rho_0
clockassumptions.rho_1
clockassumptions.rmax_0
clockassumptions.rmin_0
clockassumptions.rts0
clockassumptions.rts1
clockassumptions.rts2
clockassumptions.rts_2
clockassumptions.synctime_0
clockassumptions.translation_invariance
division.ceil_defn
division.mult_div_1
division.mult_div_2
division.mult_div_3
multiplication.mult_l0
multiplication.mult_non_neg
readbounds.induction
Total: 29
The definitions and type-constraints are:
absmod.abs
basics.maxsync
basics.maxsynctime
basics.minsync
clockassumptions.Adj
clockassumptions.okay_Reading
clockassumptions.okay_Readpred
clockassumptions.okay_Readvars
clockassumptions.okay_pairs
lemma3.okayClocks
multiplication.mult
readbounds.okaymaxsync
Total: 12
The formulae used are:
absmod.abs_bnd

absmod.abs_com
absmod.abs_diff_3
basics.ReadClock_bnd
basics.ReadClock_bnd1
basics.ReadClock_bnd11
basics.ReadClock_bnd12
basics.ReadClock_bnd2
basics.abs_shift
basics.lemma_1
basics.lemma_1_1
basics.lemma_1_2
basics.lemma_2_0
basics.lemma_2_1
basics.lemma_2_2a
basics.lemma_2_2b
basics.maxsync_correct
basics.minsync_correct
basics.minsync_maxsync
basics.okay_Reading_shift1
basics.okay_Readvars_shift
basics.okay_Readvars_shift1
basics.okay_Readvars_shift11
basics.okay_Readvars_shift12
basics.okay_Readvars_shift_step2
basics.okay_Readvars_shift_stepb
clockassumptions.okay_Reading_defn_lr
clockassumptions.okay_Reading_defn_rl
clockassumptions.okay_Readpred_Reading
clockassumptions.okay_Readvars_defn_rl
clockassumptions.okay_pairs_Readvars
clockassumptions.precision_enhancement
clockassumptions.rts_0
clockassumptions.rts_1
division.ceil_mult_div
division.ceil_plus_mult_div
division.div_nonnegative

division.mult_div
division_tcc.ceil_mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
lemma3.abs_diff_2
lemma3.accuracy_pres_step0
lemma3.accuracy_pres_step1
lemma3.accuracy_pres_step2
lemma3.accuracy_preservation
lemma3.drift_bnd
lemma3.lemma3_1
lemma3.lemma3_1_1
lemma3.lemma3_2
lemma3.lemma3_2_0
lemma3.lemma3_2_1
lemma3.lemma3_2_step
lemma3.lemma3_2_step1
lemma3.lemma3_2_step2
lemma3.lemma3_2_step3
lemma3.lemma3_3
lemma3.lemma3_3_0
lemma3.lemma3_3_ind
lemma3.maxmax_gap
lemma3.maxsync_max
lemma3.minmax_gap
lemma3.minsync_min
lemma3.okayClocks_defn_lr
lemma3.okayClocks_defn_rl
lemma_final.synctime_multiples
lemma_final.synctime_multiples_bnd
lemma_final.synctime_multiples_step
lemma_final_tcc.agreement_proof_TCC1

                                                                  lemma_final_tcc.agreement_proof_TCC2
                                                                  lemma_final_tcc.posnumber_TCC1
                                                                  lemma_final_tcc.synctime_multiples_bnd_TCC1
                                                                  lemma_final_tcc.synctime_multiples_bnd_TCC2
                                                                  multiplication.distrib
                                                                  multiplication.distrib_minus
                                                                  multiplication.mult_com
                                                                  multiplication.mult_ldistrib
                                                                  multiplication.mult_ldistrib_minus
                                                                  multiplication.mult_leq
                                                                  multiplication.mult_lident
                                                                  multiplication.mult_rident
                                                                  multiplication.pos_product
                                                                  readbounds.Cfn_IClock1
                                                                  readbounds.lemma2_abs_fact
                                                                  readbounds.lemma_2
                                                                  readbounds.lemma_2_base
                                                                  readbounds.lemma_2_ind
                                                                  readbounds.lemma_2_ind1
                                                                  readbounds.lemma_2_ind3
                                                                  readbounds.lemma_2_ind_step
                                                                  readbounds.okay_Reading_plus
                                                                  readbounds.okay_Reading_shift2
                                                                  readbounds.okaymaxsync_defn_lr
                                                                  readbounds.okaymaxsync_defn_rl
                                                                Total: 98
                                                                The completed proofs are:
                                                                  absmod.abs_bnd_proof
                                                                  absmod.abs_com_proof
                                                                  absmod.abs_diff_3_pr
                                                                  basics.ReadClock_bnd11_proof
                                                                  basics.ReadClock_bnd12_proof
                                                                  basics.ReadClock_bnd1_proof
                                                                  basics.ReadClock_bnd2_proof
                                                                  basics.ReadClock_bnd_proof

basics.abs_shift_proof
basics.lemma_1_1_proof
basics.lemma_1_2_proof
basics.lemma_1_proof
basics.lemma_2_0_proof
basics.lemma_2_1_proof
basics.lemma_2_2a_proof
basics.lemma_2_2b_proof
basics.maxsync_correct_pr
basics.minsync_correct_pr
basics.minsync_maxsync_pr
basics.okay_Reading_shift1_proof
basics.okay_Readvars_shift11_proof
basics.okay_Readvars_shift12_proof
basics.okay_Readvars_shift1_proof
basics.okay_Readvars_shift_proof
basics.okay_Readvars_shift_step2_proof
basics.okay_Readvars_shift_stepb_proof
clockassumptions.okay_Reading_defn_lr_pr
clockassumptions.okay_Reading_defn_rl_pr
clockassumptions.okay_Readpred_Reading_pr
clockassumptions.okay_Readvars_defn_rl_pr
clockassumptions.okay_pairs_Readvars_pr
clockassumptions.precision_enhancement_pr
clockassumptions.rts_0_proof
clockassumptions.rts_1_proof
division.ceil_mult_div_proof
division.ceil_plus_mult_div_proof
division.div_nonnegative_pr
division.mult_div_pr
division_tcc.ceil_mult_div_TCC1_PROOF
division_tcc.div_cancel_TCC1_PROOF
division_tcc.div_ineq_TCC1_PROOF
division_tcc.div_minus_1_TCC1_PROOF
division_tcc.div_nonnegative_TCC1_PROOF
division_tcc.mult_div_1_TCC1_PROOF

                                                                  division_tcc.mult_div_TCC1_PROOF
                                                                  lemma3.abs_diff_2_pr
                                                                  lemma3.accuracy_pres_step0_pr
                                                                  lemma3.accuracy_pres_step1_pr
                                                                  lemma3.accuracy_pres_step2_pr
                                                                  lemma3.accuracy_preservation_pr
                                                                  lemma3.drift_bnd_proof
                                                                  lemma3.lemma3_1_1proof
                                                                  lemma3.lemma3_1_proof
                                                                  lemma3.lemma3_2_0_proof
                                                                  lemma3.lemma3_2_1_proof
                                                                  lemma3.lemma3_2_proof
                                                                  lemma3.lemma3_2_step1_proof
                                                                  lemma3.lemma3_2_step2_proof
                                                                  lemma3.lemma3_2_step3_proof
                                                                  lemma3.lemma3_2_step_proof
                                                                  lemma3.lemma3_3_0_proof
                                                                  lemma3.lemma3_3_ind_proof
                                                                  lemma3.lemma3_3_proof
                                                                  lemma3.maxmax_gap_proof
                                                                  lemma3.maxsync_max_proof
                                                                  lemma3.minmax_gap_proof
                                                                  lemma3.minsync_min_proof
                                                                  lemma3.okayClocks_defn_lr_pr
                                                                  lemma3.okayClocks_defn_rl_pr
                                                                  lemma_final.agreement_proof
                                                                  lemma_final.synctime_multiples_bnd_proof
                                                                  lemma_final.synctime_multiples_proof
                                                                  lemma_final.synctime_multiples_step_proof
                                                                  multiplication.distrib_minus_pr
                                                                  multiplication.distrib_proof
                                                                  multiplication.mult_com_pr
                                                                  multiplication.mult_ldistrib_minus_proof
                                                                  multiplication.mult_ldistrib_proof
                                                                  multiplication.mult_leq_pr
                                                                  multiplication.mult_lident_proof

multiplication.mult_rident_proof
multiplication.pos_product_pr
readbounds.Cfn_IClock1_proof
readbounds.lemma2_abs_fact_proof
readbounds.lemma_2_base_proof
readbounds.lemma_2_ind1_proof
readbounds.lemma_2_ind3_proof
readbounds.lemma_2_ind_proof
readbounds.lemma_2_ind_step_proof
readbounds.lemma_2_proof
readbounds.okay_Reading_plus_proof
readbounds.okay_Reading_shift2_proof
readbounds.okaymaxsync_defn_lr_pr
readbounds.okaymaxsync_defn_rl_pr
tcc_proofs.agreement_proof_TCC1_PROOF
tcc_proofs.agreement_proof_TCC2_PROOF
tcc_proofs.posnumber_TCC1_PROOF
tcc_proofs.synctime_multiples_bnd_TCC1_PROOF
tcc_proofs.synctime_multiples_bnd_TCC2_PROOF
Total: 99

C.2 Proof Chain for ICA Translation Invariance

Terse proof chain for proof ica_translation_invariance_pr in
module ica
Use of the formula
ica.ica_translation_invariance1
requires the following TCCs to be proven
ica_tcc.sigma_TCC1
ica_tcc.sigma_TCC2
ica_tcc.icalg_TCC1

                                                                Formula ica_tcc.sigma_TCC2 is a termination TCC for ica.sigma
                                                                Proof of
                                                                  ica_tcc.sigma_TCC2
                                                                must not use
                                                                  ica.sigma
                                                                Use of the formula
                                                                  division.div_distrib
                                                                requires the following TCCs to be proven
                                                                  division_tcc.mult_div_1_TCC1
                                                                  division_tcc.mult_div_TCC1
                                                                  division_tcc.div_cancel_TCC1
                                                                  division_tcc.ceil_mult_div_TCC1
                                                                  division_tcc.div_nonnegative_TCC1
                                                                  division_tcc.div_ineq_TCC1
                                                                  division_tcc.div_minus_1_TCC1
                                                                   ================== SUMMARY ==================
                                                                The proof chain is complete
                                                                The axioms and assumptions at the base are:
                                                                  clockassumptions.N_0
                                                                  division.mult_div_1
                                                                  division.mult_div_2
                                                                  division.mult_div_3
                                                                  ica.fun_extensionality
                                                                  multiplication.mult_l0
                                                                  readbounds.induction
                                                                Total: 7
                                                                The definitions and type-constraints are:
                                                                  ica.fix
                                                                  ica.icalg
                                                                  ica.iconv

ica.sigma
ica.sigma_size
multiplication.mult
Total: 6
The formulae used are:
division.div_cancel
division.div_distrib
division_tcc.ceil_mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
ica.fix_trans
ica.ica_translation_invariance1
ica.sigma_trans_inv
ica.sigma_trans_inv_base
ica.sigma_trans_inv_ind
ica_tcc.icalg_TCC1
ica_tcc.sigma_TCC1
ica_tcc.sigma_TCC2
multiplication.distrib
multiplication.mult_lident
multiplication.mult_rident
Total: 20
The completed proofs are:
division.div_cancel_pr
division.div_distrib_pr
division_tcc.ceil_mult_div_TCC1_PROOF
division_tcc.div_cancel_TCC1_PROOF
division_tcc.div_ineq_TCC1_PROOF
division_tcc.div_minus_1_TCC1_PROOF
division_tcc.div_nonnegative_TCC1_PROOF

                                                                  division_tcc.mult_div_1_TCC1_PROOF
                                                                  division_tcc.mult_div_TCC1_PROOF
                                                                  ica.fix_trans_pr
                                                                  ica.ica_translation_invariance1_pr
                                                                  ica.ica_translation_invariance_pr
                                                                  ica.sigma_trans_inv_base_pr
                                                                  ica.sigma_trans_inv_ind_pr
                                                                  ica.sigma_trans_inv_pr
                                                                  ica_tcc.sigma_TCC1_PROOF
                                                                  multiplication.distrib_proof
                                                                  multiplication.mult_lident_proof
                                                                  multiplication.mult_rident_proof
                                                                  tcc_proofs.icalg_TCC1_PROOF
                                                                  tcc_proofs.sigma_TCC2_PROOF
                                                                Total: 21

C.3 Proof Chain for ICA Precision Enhancement

                                                                Terse proof chain for proof icalg_precision_enhancement_pr in
                                                                module ica3
                                                                Use of the formula
                                                                  ica3.prec_enh_step4
                                                                requires the following TCCs to be proven
                                                                  ica3_tcc.icalg_Pi_TCC1
                                                                  ica3_tcc.icalg_precision_enhancement_step_TCC1
                                                                  ica3_tcc.prec_enh_step3_pr_TCC1
                                                                Use of the formula
                                                                  countmod.count
                                                                requires the following TCCs to be proven
                                                                  countmod_tcc.count_TCC1

countmod_tcc.count_TCC2
countmod_tcc.count_TCC3
countmod_tcc.count_TCC4
countmod_tcc.count_TCC5
Formula countmod_tcc.count_TCC4 is a termination TCC for
countmod.count
Proof of
countmod_tcc.count_TCC4
must not use
countmod.count
Formula countmod_tcc.count_TCC5 is a termination TCC for
countmod.count
Proof of
countmod_tcc.count_TCC5
must not use
countmod.count
Use of the formula
division.div_ineq
requires the following TCCs to be proven
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.ceil_mult_div_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
Use of the formula
ica.sigma
requires the following TCCs to be proven
ica_tcc.sigma_TCC1
ica_tcc.sigma_TCC2
ica_tcc.icalg_TCC1

Formula ica_tcc.sigma_TCC2 is a termination TCC for ica.sigma
Proof of
ica_tcc.sigma_TCC2
must not use
ica.sigma
 ================== SUMMARY ==================
The proof chain is complete
The axioms and assumptions at the base are:
clockassumptions.N_0
clockassumptions.N_maxfaults
division.mult_div_1
division.mult_div_2
division.mult_div_3
ica3.Delta_0
multiplication.mult_l0
multiplication.mult_non_neg
multiplication.mult_pos
readbounds.induction
Total: 10
The definitions and type-constraints are:
absmod.abs
clockassumptions.okay_Readpred
clockassumptions.okay_pairs
countmod.count
countmod.countsize
ica.fix
ica.icalg
ica.iconv
ica.sigma
ica.sigma_size
ica3.icalg_Mu

ica3.icalg_Pi
multiplication.mult
Total: 13
The formulae used are:
absmod.abs_1_bnd
absmod.abs_2_bnd
absmod.abs_3_bnd
absmod.abs_com
absmod.abs_drift
absmod.abs_leq_0
countmod_tcc.count_TCC1
countmod_tcc.count_TCC2
countmod_tcc.count_TCC3
countmod_tcc.count_TCC4
countmod_tcc.count_TCC5
division.div_distrib
division.div_ineq
division.div_minus_distrib
division.mult_div
division.mult_minus
division_tcc.ceil_mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
ica2.fix_diff
ica2.fix_diff1
ica2.fix_diff2
ica2.fix_diff3
ica2.fix_diff_corr
ica2.iconv_sigma_diff
ica2.okay_Readpred_lr
ica2.okay_Readpred_pairs

                                                                  ica2.okay_pairs_fix
                                                                  ica2.okay_pairs_lr
                                                                  ica2.sigma_diff
                                                                  ica2.sigma_diff_ind
                                                                  ica2.sigma_neg
                                                                  ica2.sigma_neg_ind
                                                                  ica2.sigma_neg_ind_step
                                                                  ica2.sigma_pos
                                                                  ica2.sigma_pos_ind
                                                                  ica2.sigma_pos_neg
                                                                  ica2.sigma_split
                                                                  ica2.sigma_split_ind
                                                                  ica3.count_complement
                                                                  ica3.icalg_precision_enhancement_step
                                                                  ica3.mult_sum_ineq
                                                                  ica3.prec_enh_step
                                                                  ica3.prec_enh_step2
                                                                  ica3.prec_enh_step3
                                                                  ica3.prec_enh_step4
                                                                  ica3_tcc.icalg_Pi_TCC1
                                                                  ica3_tcc.icalg_precision_enhancement_step_TCC1
                                                                  ica3_tcc.prec_enh_step3_pr_TCC1
                                                                  ica_tcc.icalg_TCC1
                                                                  ica_tcc.sigma_TCC1
                                                                  ica_tcc.sigma_TCC2
                                                                  multiplication.distrib
                                                                  multiplication.distrib_minus
                                                                  multiplication.mult_com
                                                                  multiplication.mult_gt
                                                                  multiplication.mult_ldistrib_minus
                                                                  multiplication.mult_leq_2
                                                                  multiplication.mult_lident
                                                                  multiplication.mult_rident
                                                                Total: 64
                                                                The completed proofs are:

absmod.abs_1_bnd_proof
absmod.abs_2_bnd_proof
absmod.abs_3_bnd_proof
absmod.abs_com_proof
absmod.abs_drift_proof
absmod.abs_leq_0_proof
countmod_tcc.count_TCC1_PROOF
countmod_tcc.count_TCC2_PROOF
countmod_tcc.count_TCC3_PROOF
division.div_distrib_pr
division.div_ineq_pr
division.div_minus_distrib_pr
division.mult_div_pr
division.mult_minus_pr
division_tcc.ceil_mult_div_TCC1_PROOF
division_tcc.div_cancel_TCC1_PROOF
division_tcc.div_ineq_TCC1_PROOF
division_tcc.div_minus_1_TCC1_PROOF
division_tcc.div_nonnegative_TCC1_PROOF
division_tcc.mult_div_1_TCC1_PROOF
division_tcc.mult_div_TCC1_PROOF
ica2.fix_diff1_pr
ica2.fix_diff2_pr
ica2.fix_diff3_pr
ica2.fix_diff_corr_pr
ica2.fix_diff_pr
ica2.iconv_sigma_diff_pr
ica2.okay_Readpred_lr_pr
ica2.okay_Readpred_pairs_pr
ica2.okay_pairs_fix_pr
ica2.okay_pairs_lr_pr
ica2.sigma_diff_ind_pr
ica2.sigma_diff_pr
ica2.sigma_neg_ind_pr
ica2.sigma_neg_ind_step_pr
ica2.sigma_neg_pr

                                                                  ica2.sigma_pos_ind_pr
                                                                  ica2.sigma_pos_neg_pr
                                                                  ica2.sigma_pos_pr
                                                                  ica2.sigma_split_ind_pr
                                                                  ica2.sigma_split_pr
                                                                  ica3.count_complement_pr
                                                                  ica3.icalg_precision_enhancement_pr
                                                                  ica3.icalg_precision_enhancement_step_pr
                                                                  ica3.mult_sum_ineq_pr
                                                                  ica3.prec_enh_step2_pr
                                                                  ica3.prec_enh_step3_pr
                                                                  ica3.prec_enh_step4_pr
                                                                  ica3.prec_enh_step_pr
                                                                  ica_tcc.sigma_TCC1_PROOF
                                                                  multiplication.distrib_minus_pr
                                                                  multiplication.distrib_proof
                                                                  multiplication.mult_com_pr
                                                                  multiplication.mult_gt_pr
                                                                  multiplication.mult_ldistrib_minus_proof
                                                                  multiplication.mult_leq_2_pr
                                                                  multiplication.mult_lident_proof
                                                                  multiplication.mult_rident_proof
                                                                  tcc_proofs.countmod_TCC4_pr
                                                                  tcc_proofs.countmod_TCC5_pr
                                                                  tcc_proofs.icalg_Pi_TCC1_PROOF
                                                                  tcc_proofs.icalg_TCC1_PROOF
                                                                  tcc_proofs.icalg_precision_enhancement_step_TCC1_PROOF
                                                                  tcc_proofs.prec_enh_step3_pr_TCC1_PROOF
                                                                  tcc_proofs.sigma_TCC2_PROOF
                                                                Total: 65

C.4 Proof Chain for ICA Accuracy Preservation

Terse proof chain for proof icalg_accuracy_preservation_pr in
module ica4
Use of the formula
ica4.acc_pres_step
requires the following TCCs to be proven
ica4_tcc.icalg_accuracy_preservation_TCC1
ica4_tcc.icalg_accuracy_preservation_pr_TCC1
Use of the formula
ica.sigma
requires the following TCCs to be proven
ica_tcc.sigma_TCC1
ica_tcc.sigma_TCC2
ica_tcc.icalg_TCC1
Formula ica_tcc.sigma_TCC2 is a termination TCC for ica.sigma
Proof of
ica_tcc.sigma_TCC2
must not use
ica.sigma
Use of the formula
countmod.count
requires the following TCCs to be proven
countmod_tcc.count_TCC1
countmod_tcc.count_TCC2
countmod_tcc.count_TCC3
countmod_tcc.count_TCC4
countmod_tcc.count_TCC5
Formula countmod_tcc.count_TCC4 is a termination TCC for
countmod.count

Proof of
countmod_tcc.count_TCC4
must not use
countmod.count
Formula countmod_tcc.count_TCC5 is a termination TCC for
countmod.count
Proof of
countmod_tcc.count_TCC5
must not use
countmod.count
Use of the formula
ica3.Delta_0
requires the following TCCs to be proven
ica3_tcc.icalg_Pi_TCC1
ica3_tcc.icalg_precision_enhancement_step_TCC1
ica3_tcc.prec_enh_step3_pr_TCC1
Use of the formula
division.abs_div
requires the following TCCs to be proven
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.ceil_mult_div_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
 ================== SUMMARY ==================
The proof chain is complete
The axioms and assumptions at the base are:
clockassumptions.N_0

clockassumptions.N_maxfaults
division.mult_div_1
division.mult_div_2
division.mult_div_3
ica3.Delta_0
multiplication.mult_l0
multiplication.mult_non_neg
multiplication.mult_pos
readbounds.induction
Total: 10
The definitions and type-constraints are:
absmod.abs
clockassumptions.okay_Readpred
clockassumptions.okay_pairs
countmod.count
countmod.countsize
ica.fix
ica.icalg
ica.iconv
ica.sigma
ica.sigma_size
multiplication.mult
Total: 11
The formulae used are:
absmod.abs_1_bnd
absmod.abs_2_bnd
absmod.abs_3_bnd
absmod.abs_drift
absmod.abs_leq_0
absmod.abs_plus
countmod_tcc.count_TCC1
countmod_tcc.count_TCC2
countmod_tcc.count_TCC3
countmod_tcc.count_TCC4

countmod_tcc.count_TCC5
division.abs_div
division.div_cancel
division.div_distrib
division.div_ineq
division.div_minus_1
division.div_minus_distrib
division.div_nonnegative
division.mult_div
division.mult_minus
division_tcc.ceil_mult_div_TCC1
division_tcc.div_cancel_TCC1
division_tcc.div_ineq_TCC1
division_tcc.div_minus_1_TCC1
division_tcc.div_nonnegative_TCC1
division_tcc.mult_div_1_TCC1
division_tcc.mult_div_TCC1
ica2.okay_Readpred_lr
ica2.sigma_diff
ica2.sigma_diff_ind
ica2.sigma_pos
ica2.sigma_pos_ind
ica2.sigma_split
ica2.sigma_split_ind
ica3.count_complement
ica3.mult_sum_ineq
ica3_tcc.icalg_Pi_TCC1
ica3_tcc.icalg_precision_enhancement_step_TCC1
ica3_tcc.prec_enh_step3_pr_TCC1
ica4.acc_pres_sigma_neg
ica4.acc_pres_sigma_pos
ica4.acc_pres_step
ica4.okay_Readpred_fix_diff
ica4.okay_Readpred_fix_diff2
ica4.sigma_abs
ica4.sigma_duplicate

ica4_tcc.icalg_accuracy_preservation_TCC1
ica4_tcc.icalg_accuracy_preservation_pr_TCC1
ica_tcc.icalg_TCC1
ica_tcc.sigma_TCC1
ica_tcc.sigma_TCC2
multiplication.distrib
multiplication.distrib_minus
multiplication.mult_com
multiplication.mult_gt
multiplication.mult_ldistrib_minus
multiplication.mult_leq_2
multiplication.mult_lident
multiplication.mult_rident
multiplication.pos_product
Total: 60
The completed proofs are:
absmod.abs_1_bnd_proof
absmod.abs_2_bnd_proof
absmod.abs_3_bnd_proof
absmod.abs_drift_proof
absmod.abs_leq_0_proof
absmod.abs_plus_pr
countmod_tcc.count_TCC1_PROOF
countmod_tcc.count_TCC2_PROOF
countmod_tcc.count_TCC3_PROOF
division.abs_div_pr
division.div_cancel_pr
division.div_distrib_pr
division.div_ineq_pr
division.div_minus_1_pr
division.div_minus_distrib_pr
division.div_nonnegative_pr
division.mult_div_pr
division.mult_minus_pr
division_tcc.ceil_mult_div_TCC1_PROOF

division_tcc.div_cancel_TCC1_PROOF
division_tcc.div_ineq_TCC1_PROOF
division_tcc.div_minus_1_TCC1_PROOF
division_tcc.div_nonnegative_TCC1_PROOF
division_tcc.mult_div_1_TCC1_PROOF
division_tcc.mult_div_TCC1_PROOF
ica2.okay_Readpred_lr_pr
ica2.sigma_diff_ind_pr
ica2.sigma_diff_pr
ica2.sigma_pos_ind_pr
ica2.sigma_pos_pr
ica2.sigma_split_ind_pr
ica2.sigma_split_pr
ica3.count_complement_pr
ica3.mult_sum_ineq_pr
ica4.acc_pres_sigma_neg_pr
ica4.acc_pres_sigma_pos_pr
ica4.acc_pres_step_pr
ica4.icalg_accuracy_preservation_pr
ica4.okay_Readpred_fix_diff2_pr
ica4.okay_Readpred_fix_diff_pr
ica4.sigma_abs_pr
ica4.sigma_duplicate_pr
ica_tcc.sigma_TCC1_PROOF
multiplication.distrib_minus_pr
multiplication.distrib_proof
multiplication.mult_com_pr
multiplication.mult_gt_pr
multiplication.mult_ldistrib_minus_proof
multiplication.mult_leq_2_pr
multiplication.mult_lident_proof
multiplication.mult_rident_proof
multiplication.pos_product_pr
tcc_proofs.countmod_TCC4_pr
tcc_proofs.countmod_TCC5_pr
tcc_proofs.icalg_Pi_TCC1_PROOF

tcc_proofs.icalg_TCC1_PROOF
tcc_proofs.icalg_accuracy_preservation_TCC1_PROOF
tcc_proofs.icalg_accuracy_preservation_pr_TCC1_PROOF
tcc_proofs.icalg_precision_enhancement_step_TCC1_PROOF
tcc_proofs.prec_enh_step3_pr_TCC1_PROOF
tcc_proofs.sigma_TCC2_PROOF
Total: 61