Common use of Proof of the algorithm Clause in Contracts

Proof of the algorithm. The proof considers the system model BAMPn,t[t < n/(m + 1), LRC], the algorithmic safety and liveness constraints on W , namely, W (k + 1) > n and n − t ≥ (W − 1)k + 1, and the non-triviality condition (k < m) ∧ (k ≤ t). Preliminary remark 1 The proof considers the semantic of the messages DECIDE() described pre- viously. This is equivalent to consider that, after it has decided, a correct process continues executing while skipping line 8. Notation Given a round r, let EST [r] be the set of estimate values of the correct processes when they start round r, and AUX [r] be the set including the values of the auxi variables of the correct processes at the end of the first phase of round r (i.e., just after line 5). let us notice that AUX [r] can contain ⊥. Preliminary remark 2 The proof of the MV-Obligation property requires that at most m different val- ues are MV-broadcast. Hence, this requirement extends to the invocations SMV broadcastPHASE[r, x](), where x ∈ {1, 2}. By assumption, this requirement is initially satisfied, namely, |EST [1]| ≤ m. We will see in the proof that (i) AUX [r] contains at most k values proposed by correct processes plus pos- sibly ⊥, (ii) viewi[r, 2] is a subset of AUX [r], and (iii) mv validi[1, 1] contains only values proposed by correct processes. From the previous observations we conclude that at most m different values are SMV-broadcast at line 4 and line 6 of Algorithm 4. Lemma 1. If a correct process decides a value, this value was proposed by a correct process.

Proof of the algorithm. The proof considers the system model BAMPn,t[t < n/(m + 1), LRC], the algorithmic safety and liveness constraints on W , namely, W (k + 1) > n and n − t ≥ (W − 1)k + 1, and the non-triviality condition (k < m) ∧ (k ≤ t). Preliminary remark 1 The proof considers the semantic of the messages DECIDE() described pre- viously. This is equivalent to consider that, after it has decided, a correct process continues executing while skipping line 8. Notation Given a round r, let EST [r] be the set of estimate values of the correct processes when they start round r, and AUX [r] be the set including the values of the auxi variables of the correct processes at the end of the first phase of round r (i.e., just after line 5). let us notice that AUX [r] can contain ⊥. Preliminary remark 2 The proof of the MV-Obligation property requires that at most m different val- ues are MV-broadcast. Hence, this requirement extends to the invocations SMV broadcastPHASE[r, x](), where x ∈ {1, 2}. By assumption, this requirement is initially satisfied, namely, |EST [1]| ≤ m. We will see in the proof that (i) AUX [r] contains at most k values proposed by correct processes plus pos- sibly ⊥, (ii) viewi[r, 2] is a subset of AUX [r], and (iii) mv validi[1, 1] contains only values proposed by correct processes. From the previous observations we conclude that at most m different values are SMV-broadcast at line 4 and line 6 of Algorithm 4. Lemma 1. If a correct process decides a value, this value was proposed by a correct process. Lemma 2. AUX [r] contains at most k non-⊥ values, plus possibly the default value ⊥. Proof Let us assume that AUX [r] contains (k + 1) non-⊥ values. If a value belongs to this set, it is the value of the local variable auxi of a correct process pi, which appears at least W times in the multiset viewi[r, 1] (line 5). Moreover, due to SMV-No-duplicity property, a process (correct or Byzantine) contribute to at most one of these values. It follows from these observations that, if AUX [r] contains (k+1) non-⊥ values, (k+1)W distinct processes have contributed to AUX [r], i.e., have SMV-broadcast PHASE[r, 1]() messages. As (k + 1)W > n, this is impossible. ✷Lemma 2 Lemma 3. If |EST [r]| ≤ k, any correct process that starts round r decides during r a value of EST [r]. Proof As by assumption the correct processes have at most k different estimate values at the beginning of round r, it follows from the SMV-Contribution property of the SMV-broadcast of line 4 that at least (n − t) different processes contributed to the multiset viewi[r, 1]. As n − t ≥ (W − 1)k + 1 (algoritmic liveness), it follows that the multiset viewi[r, 1] of any correct process pi contains at least W copies of a value of EST [r]. Hence, auxi ∈ EST [r] at each correct process. Consequently AUX [r] ⊆ EST [r]. it then follows that the predicate of line 7 is satisfied at any correct process pi, which decides accordingly a value of viewi[r, 2] ⊆ AUX [r] ⊆ EST [r], which concludes the proof of the lemma. ✷Lemma 3 Lemma 4. Let pi and pj be two correct processes. At any round r, the predicates ⊥ ∈/ viewi[r, 2] and viewj[r, 2] = {⊥} are mutually exclusive. Proof let us assume by contradiction that pi is a correct process such that the predicate ⊥ ∈/ viewi[r, 2] is satisfied (line 7), and pj a correct process such that the predicate viewj[r, 2] = {⊥} is satisfied (line 10). It follows from the SMV-Contribution property of the SMV-broadcast issued byi and j at line 6 that viewi[r, 2] contains values contributed by at least (n − t) processes, and similarly for the set viewj[r, 2] of pj. As n > 3t, the intersection of any two sets of (n − t) processes contains at least (t + 1) processes, i.e., one correct process. It then follows that there is a correct process that contributed to both viewi[r, 2] and viewj[r, 2], from which we conclude that either viewi[r, 2] contains ⊥, or viewj[r, 2] contains a non-⊥ estimate value. ✷Lemma 4 Lemma 5. No more than k different values are decided by the correct processes. Proof Let r be the first round during which correct processes decide. They decide at line 8. Due to Lemma 2, the set AUX [r] contains at most k non-⊥ values. Moreover, due to the SMV-broadcast issued by the correct processes at line 6 that we have viewi[r, 2] ⊆ AUX [r] at each correct process pi. Hence, due to line 7, a process that decides during round r can only decide a value of AUX [r]. Let us now consider a correct process pj that proceeds to round (r + 1). Let pi be a process that decides at round r. It follows from Lemma 4 that the predicates ⊥ ∈/ viewi[r, 2] and viewj[r, 2] = {⊥} are mutually exclusive. Consequently, pj executes line 9 before progressing to the next round. Hence, pj updated estj to a non-⊥ value of viewj[r, 2] ⊆ AUX [r] before progressing to the next round. It follows that the estimates of the correct processes progressing to the next round are non-⊥ values of AUX [r]. Hence, EST [r + 1] ⊆ AUX [r] \ {⊥}. It then follows from Lemma 3 that at most k values are decided.