Authenticated Adversarial Routing

The aim of this paper is to demonstrate the feasibility of authenticated throughput-efficient routing in an unreliable and dynamically changing synchronous network in which the majority of malicious insiders try to destroy and alter messages or disrupt communication in any way. More specifically, in this paper we seek to answer the following question: Given a network in which the majority of nodes are controlled by a node-controlling adversary and whose topology is changing every round, is it possible to develop a protocol with polynomially bounded memory per processor (with respect to network size) that guarantees throughput-efficient and correct end-to-end communication?

We answer the question affirmatively for extremely general corruption patterns: we only request that the topology of the network and the corruption pattern of the adversary leaves at least one path each round connecting the sender and receiver through honest nodes (though this path may change at every round). Out construction works in the public-key setting and enjoys optimal transfer rate and bounded memory per processor (that is polynomial in the network size and does not depend on the amount of traffic). We stress that our protocol assumes no knowledge of which nodes are corrupted nor which path is reliable at any round, and is also fully distributed with nodes making decisions locally, so that they need not know the topology of the network at any time.

The optimality that we prove for our protocol is very strong. Given any routing protocol, we evaluate its efficiency (rate of message delivery) in the “worst case,” that is with respect to the worst possible graph and against the worst possible (polynomially bounded) adversarial strategy (subject to the above mentioned connectivity constraints). Using this metric, we show that there does not exist any protocol that can be asymptotically superior (in terms of throughput) to ours in this setting.

We remark that the aim of our paper is to demonstrate via explicit example the feasibility of throughput-efficient authenticated adversarial routing. However, we stress that out protocol is not intended to provide a practical solution, as due to its complexity, no attempt thus far has been made to reduce constants and memory requirements.

Our result is related to recent work of Barak et al. (Proc. of Advances in Cryptology—27th EUROCRYPT 2008, LNCS, vol. 4965, pp. 341–360, 2008) who studied fault localization in networks assuming a private-key trusted-setup setting. Our work, in contrast, assumes a public-key PKI setup and aims at not only fault localization, but also transmission optimality. Among other things, our work answers one of the open questions posed in the Barak et al. paper regarding fault localization on multiple paths. The use of a public-key setting to achieve strong error-correction results in networks was inspired by the work of Micali et al. (Proc. of 2nd Theory of Cryptography Conf., LNCS, vol. 3378, pp. 1–16, 2005) who showed that classical error correction against a polynomially bounded adversary can be achieved with surprisingly high precision. Our work is also related to an interactive coding theorem of Rajagopalan and Schulman (Proc. 26th ACM Symp. on Theory of Computing, pp. 790–799, 1994) who showed that in noisy-edge static-topology networks a constant overhead in communication can also be achieved (provided none of the processors are malicious), thus establishing an optimal-rate routing theorem for static-topology networks.

Finally, our work is closely related and builds upon to the problem of End-To-End Communication in distributed networks, studied by Afek and Gafni (Proc. of the 7th ACM Symp. on Principles of Distributed Computing, pp. 131–148, 1988); Awebuch et al. (Proc. of the 30th IEEE Symp. on Foundations of Computer Science, FOCS, 1989); Afek et al. (Proc. of the 11th ACM Symp. on Principles of Distributed Computing, pp. 35–46, 1992); and Afek et al. (J. Algorithms 22:158–186, 1997), though none of these papers consider or ensure correctness in the setting of a node-controlling adversary that may corrupt the majority of the network.

1. For the protocol of Sect. 4, we require that P∈Ω(logn), while the protocol of Sect. 5 requires that P∈Ω(k+logn), where k is the security parameter.

2. The separation into two separate adversaries is artificial: our protocol is secure whether edge-scheduling and corruption of nodes are performed by two separate adversaries that have different capabilities yet can coordinate their actions with each other, or this can be viewed as a single coordinated adversary.

3. A more general definition of an edge-scheduling adversary would be to allow completely arbitrary edge failures (except that in the limit there must be no permanent cut between the sender and receiver). However, this definition (while more general) greatly complicates the evaluation of a protocol’s throughput performance; in particular, our current definition of throughput rate cannot be used to compare routing protocols in this generalized setting.

4. The conforming assumption guarantees that the sender and receiver are incorruptible, and our protocol places the responsibility of identifying and eliminating corrupt nodes on these two nodes.

5. Also known in practical works as “gravitational flow” routing.

6. There are numerous protocols that have been designed to work in specific networks settings, e.g. ad hoc wireless networks, where the networks are susceptible to both corrupt/faulty nodes as well as unreliable links. While research in designing specific (end-to-end) protocols for specific network settings is extensive, no existing protocol has been demonstrated to be provably secure with respect to a formal notion of security (as presented here).

7. By “flood,” we mean that the sender will repeatedly attempt to send the first packet across every adjacent edge for n rounds, and then do the same thing for the second packet for the next n rounds, and so forth. The internal nodes behave similarly, attempting to send whatever packet they are storing (there will be just one) across every adjacent edge. They continue to do this until they have a more recent packet, at which point they repeat this behavior with the new packet (and delete the older packet).

8. An alternative approach would have the sender continue flooding the first packet, and upon receipt, the receiver floods confirmation of receipt. This alternative solution requires sequence numbers to accompany packets/confirmations, and the rule that internal nodes only keep and broadcast the packet and confirmation with largest sequence number. Although this alternative may potentially speed things up, in the worst-case it will still take O(n) rounds for a single packet/confirmation pair to be transmitted.

9. More precisely, for each neighboring node n _i , the sender keeps track of the highest indexed packet p _j(i) it has sent to that neighbor (and gotten confirmation of receipt from the neighbor). Then the next time the sender is able to utilize edge E(S,n _i ), it sends the next indexed packet that has not yet been received by the receiver (e.g. packet p _j+1, if the sender has not already received confirmation of receipt for this packet from the receiver).

10. Consider the following pattern of edge failures/activations by the scheduling adversary: for 1≤i≤n−2 and for any \(m \in\mathbb{N}\), during round mi, the only active edges are E(S,N _i ) and E(R,N _i ). It is straightforward to see that this pattern of activating edges will have this protocol deliver just one distinct packet at the end of each (n−2) rounds, for a throughput rate of Θ(x/n).

11. Since this paper is concerned only with transferring an (arbitrary) polynomial (in n and k) number of inputs, by “arbitrarily large” processor memory, we mean that there does not exist a memory bound C=poly(n,k) for which this protocol is correct and achieves reasonable throughput. To see that correctness and/or throughput become problematic if memory is bounded by something polynomial in n (call it C), consider the following example. Label the internal nodes (S,R,N ₀,N ₁,…,N _n−3), where n≥5 is the size of the network. Suppose that for M:=⌈C(1+5/n)⌉ rounds, the scheduling adversary activates edges as follows: for each 1≤i≤n−3 and for any \(m \in\mathbb{N}\), during round mi, the only active edges are E(S,N _i ), E(N _i ,R), and E(S,N ₀). Notice that at the end of these M rounds, the sender has successfully sent ≈M/(n−3) packets to the receiver (and received confirmation of receipt for these), which means that node N ₀ is storing its capacity C packets (the sender has had the opportunity to send M packets to N ₀, and at most M/(n−3) can be deleted by N ₀ when the sender indicates the packets have already been received by the receiver; so M−M/(n−3)=C(n+4)(n−4)/n(n−3)>C). Then for the next 2C rounds, the scheduling adversary activates edges E(S,N ₁), E(N ₁,N ₂), and E(N ₂,R). Notice that by the end of these 2C rounds, ≈2C packets have gone from sender to receiver through N ₁ and N ₂, and neither N ₁ nor N ₂ will be storing any confirmations of receipt for any of the C packets that N ₀ is storing. At this point, edges E(S,N ₁), E(N ₁,N ₀), E(N ₀,N ₂), E(N ₂,R) are activated every round henceforth. Notice that no progress can be made, since N ₀ cannot accept any more packets until it has freed room, and it cannot delete any of its packets until it receives indication that the receiver already has them (but neither N ₁ nor N ₂ can give N ₀ such confirmation, since they no longer have it). One could try to modify this protocol in various ways (e.g. allow overwriting of packets by packets that have a much higher index number, or have sender/receiver resend old confirmations of receipt); but this example demonstrates the challenge of simultaneously maximizing throughput while demanding correctness, and the fact that naïve protocols do not suffice.

12. We give a definition of the adversary in Sect. 3.2.

13. In this paper we use public-key operations to sign individual packets with control information. Clearly, this is too expensive to do per-packet in practice. There are methods of amortizing the cost of signatures by signing “batches” of packets; using private-key initialization [8, 12], or using a combination of private-key and public-key operations, such as “on-line/off-line” signatures [11, 19]. For the sake of clarity and since the primary focus of our paper is theoretical feasibility, we restrict our attention to the straightforward public-key setting without considering these techniques.

14. We emphasize here the importance that the sender is able to distinguish the case that the jamming is a result of the edge-scheduling adversary’s controlling of edges verses the case that a corrupt node is duplicating packets. After all, in the case of the former, there is no reward for “localizing” the fault to an edge that has failed, as all edges are controlled by the edge-scheduling adversary, and therefore no edge is inherently better than another. But in the case a node is duplicating packets, if the sender can identify the node, it can eliminate it and effectively reduce the node-controlling adversary’s ability to disrupt communication in the future.

15. Although synchronous networks are difficult to realize in practice, we can further relax the model to one in which there is a known upper bound on the amount of time an active edge can take to transfer a packet.

16. The distinction between the two kinds of adversaries is made solely to emphasize the contribution of this paper. Edge-scheduling adversaries (as described above) are commonly used to model edge failures in networks, while the contribution of our paper is in handling the additional presence of a node-controlling adversary, which has the ability to corrupt the nodes of the network.

17. Although the node-controlling adversary is dynamic, he is still constrained by the conforming assumption. Namely, the adversary may not corrupt nodes that have been, or will be, part of any active path connecting sender and receiver.

18. If desired, privacy can be added trivially by encrypting all packets.

19. In this paper, we assume the existence of an error-correcting code with information rate σ and error rate λ.

20. Although the original Slide protocol does not require room to be left in incoming buffers, our technique for proving optimal throughput rate requires this modification: At a high level, the proof regarding throughput will require that a packet never increase in height from the time it is inserted into the network by the sender. Thus, whenever a packet is transferred, the height it assumes in the receiving node’s buffer must be no greater than the height it had in the sending node’s buffer. While this is the guiding principle of Slide, in our network setting and version of the Slide protocol, this property is threatened in the following scenario: Suppose there is a round in which node A’s incoming buffer along E(A,B) has fewer packets than B’s outgoing buffer along that edge; a condition that leads the Slide protocol to transfer a packet p ₀ from B to A. But as this packet is being exchanged, the connecting edge fails before it is delivered. The edge remains down for some time, during which A’s other edges remain active, and A’s buffers fill because it is getting packets from other neighbors (our version of Slide keeps its buffers balanced, so that even A’s incoming buffer along E(A,B) is filling during this time). Then once E(A,B) becomes active again, our protocol must decide what to do with p ₀. If no spot was reserved for p ₀, then either A rejects p ₀, or A accepts p ₀ at a height higher than p ₀ had in B’s buffer (or A must shift other packets up to make room for p ₀). Both these scenarios are problematic for our throughput proof, the former because our proof requires that an active edge is always utilized when it has a packet to transfer, and the latter because it violates the property that packets always decrease in height.

21. Note that because ghost packets do not count towards height, there appears to be a danger that the re-shuffle rules may dictate a packet gets transferred into an incoming buffer, and this packet either has no place to go (because the ghost packet occupies the top slot) or the packet increases in height (which would violate Claim B.13 in Appendix B). However, because only incoming buffers are allowed to re-shuffle packets into other incoming buffers, and the difference in height must be at least two when this happens, neither of these troublesome events can occur.

22. As mentioned, the Slide protocol was developed and analyzed in a series of papers prior to this paper, including [2–6], and [14]. However, none of these papers considered the network setting encountered in the present paper, and as such Theorem 4.3 (and more specifically the fact that the Slide protocol enjoys linear throughput-rate in synchronous networks) has not been proven previously.

23. Note that for the Slide protocol in this section, P∈Ω(logn) to account for the fact that a codeword packet must carry with it Ω(logn) bits of information regarding its position in the codeword. In the next section, we will require that P∈Ω(k+logn), where k is the security parameter, so that each packet can carry a signature.

24. An initial guess that the minimal potential drop equals “2n” for each blocked round is incorrect. Consider the case where the active path consists of all n−2 intermediate nodes with the following current state: the first two nodes’ buffers all have height 2n, the next pair’s buffers all have height 2n−1, and so forth, down to the last pair of internal nodes, whose buffers all have height n+2. Then the drop in the network’s non-duplicated potential is only n+2 for this round.

25. Intuitively, an outgoing buffer has at most one flagged packet since the buffer will continue trying to send this packet until it receives confirmation of receipt from the neighboring node. We restate and prove this fact in terms of the pseudo-code in Claim B.10 in Appendix B.

26. Even if the sending and/or receiving node’s buffer heights have changed since the original communication that prompted the packet transfer, the fact that flagged packets are not re-shuffled or shifted down to fill-gaps ensures that the flagged-packet maintains its original height; while the use of ghost packets ensures that the height assumed by the transferred packet (when it is finally accepted) is exactly one greater than the originally communicated height.

27. Note that our use of error correction allows for the fact that some packets may be in the internal nodes’ buffers, and yet the receiver can still decode: Even if every buffer of each internal node is completely full, the receiver will still be able to decode the codeword if it has received the rest of the codeword packets. Therefore, if the sender has inserted all D of the codeword packets, the receiver should be able to decode, even if many of the packets are stuck in the internal nodes’ buffers.

28. In the case a transmission T fails as in F4, which means the receiver got at least one duplicated packet p, then the testimonies from the nodes includes only the final value (from each of their neighbors) on the number of times p has passed between them. In particular, even though the control packets passed between neighbors have been accumulating information on all of the Θ(n ³) codeword packets, the only value returned to the sender is on the relevant packet p that had been duplicated. This way, a testimony from each node consists of n−1 packets instead of Θ(n ³) packets. Indeed, once a node learns a transmission fails for reason F4 and they know a packet p that has been duplicated (how this knowledge is conveyed is discussed below), they can delete the information corresponding to all of the other Θ(n ³) packets, freeing up this memory.

29. An honest node will never send a packet with faulty information. Therefore, if a node receives a packet with faulty information from a neighbor, the node can be certain its neighbor is corrupt. There are three reasonable candidates for how a protocol should have nodes deal with the knowledge its neighbor is corrupt: (1) Do nothing; (2) Keep the information local, but refuse all future communication with the node; (3) Report the offending node, to alert the network the node is faulty in attempt to have it eliminated. Option (3) introduces the difficulty of a “he said, she said” problem of the sender not being able to pinpoint which of the two nodes is corrupt, and we therefore do not use that approach. Of the other two options, we choose the former, simply because it is more in line with our approach for eliminating corrupt nodes, as opposed to eliminating the links adjacent to corrupt nodes. However, employing strategy (2) can be done without any major modifications to Mal-Slide (although this strategy will not improve the bound for throughput efficiency that is stated in Theorem 5.2 below).

30. Corrupt nodes cannot be prevented from transferring packets to/from blacklisted nodes. However, such a strategy will not help them to cause transmissions to fail without their guilt being discovered, as if they employ this strategy to force a transmission T′ to fail, then either: (1) They return the accurate control information for T′ (in which case the sender sees they transferred codeword packets with blacklisted nodes and are therefore necessarily corrupt); (2) They return the control information to the sender, but do not include with this the parts that indicate they transferred packets with blacklisted nodes (in which case there will be discrepancies in the testimony that they return); (3) They do not return any control information, and are consequently blacklisted (and not able to affect future transmissions) until they return enough control information to fall under case (1) or (2) and become permanently eliminated.

31. Because our protocol is only valid for an input stream of packets of size polynomial in n, timestamps can be achieved using Θ(logn) bits.

32. Even though the receiver cannot be corrupted, he nevertheless can (and will) be placed on the blacklist at the end of each failed transmission. After all, the blacklist is not just a list of potential nodes that may be corrupt; rather, it is a list of nodes who participated in a given failed transmission and it emphasizes that the sender has yet to receive those nodes’ testimonies for the transmission. So the receiver gets placed on the blacklist to emphasize to intermediate nodes the need to relay the receiver’s testimony back to the sender.

33. We explain in the proof of Theorem D.34 how to account for the “off-by-one” error discussed above, so that the equality in (6) is precise.

34. In [14], it was shown how to modify the Slide protocol so that it only requires O(nlogn) memory per internal node. We did not explore in this paper if and/or how their techniques could be applied to our protocol to similarly reduce it by a factor of n.

35. If we are given an a priori bound that a path-length of any conforming path is at most L, the O(n ⁴logn) can be somewhat reduced to O(Ln ³logn). Similarly, if we are given a bound that the maximum degree (number of edges) for all nodes is bounded by δ, then the memory bound can be further reduced to O(Lδn ²logn).

36. The sender’s outgoing buffers are filled with (distinct) packets from \(\mathcal{M}\) at the outset of each transmission (A.4.70) and during re-shuffling (A.5.96). Since S never receives packets (A.3.08), once a packet p has left the sender, it will never again be in any of the sender’s (outgoing) buffers. Consequently, whenever \(\tilde{p}\) is set as on (A.4.38) after round t′, \(\tilde{p}\) can never be set to p, and hence on line (A.4.38), it will never be the case (after round t′) that OUT[H _FP ]=p.

37. The Claim remains valid even if t′ is a round in a different transmission than t.

38. Failing the condition on (A.3.30) technically means RR<FR or FR=⊥; but in light of Statement 3 of this claim, FR=t′ for all rounds between t′ and the time B gets confirmation of receipt for p.

39. Or through the end of the transmission, whichever occurs first.

40. Since a packet was necessarily transferred in t by definition of t, and since we already noted sb _OUT =0 at the start of t, the fact that a packet was sent means that (A.3.16) was satisfied, and thus H _OUT >H _IN . Since the values cannot change between (A.3.15) and (A.3.16), we have that line (A.4.37) was necessarily satisfied in round t.

41. By Statement 3 of Claim B.9, the packet flagged in t ₀ is the only packet \(O_{N_{1},R}\) can send to R between t ₀+1 and the time R receives this flagged packet. Since we know R has still not accepted this flagged packet by the outset of t, this means that between t ₀ and t−1, RR cannot be changed as on (A.4.53). Since RR begins each transmission equal to −1 ((A.1.31) and (A.4.64)) and can only be changed after this on (A.4.53), necessarily RR<t ₀ through the start of t.

42. This drop was not already accounted for when we invoked the induction hypothesis, because the definition of ϕ does not count the re-shuffling in the chain’s first node (however, since N ₂ is actually the second node in the chain \(\mathcal{C}\) being considered, it is valid to count its contributions to ϕ based on re-shuffling packets into \(O_{N_{2}, N_{3}}\)).

43. For the argument in the Base Case, we used the fact that the receiver’s incoming buffer had height zero in order to conclude H _OUT >H _IN (and thus a packet would be sent). Here, we use instead (B.5) to come to the same conclusion.

44. The (n−1) comes from the fact that there are no testimonies for the sender.

45. We assume that the signature buffer information for two directed edges E(A,B) and E(B,A) are combined into one testimony parcel.

46. Since for all transmissions, lines (C.6.166) and (C.7.171) cannot be reached after line (C.7.188), we see that if (N,T′) is removed from the blacklist as on (C.6.166) or (C.7.171) of transmission T, then necessarily T>T′, since (N,T′) can only be added to BL at the very end of transmission T′ (C.7.188).

47. The sender already received enough information to eliminate a node. Even though it is possible that other nodes acted maliciously and caused one of the failed transmissions, it is also possible that the node just eliminated caused all of the failed transmissions. Therefore, the protocol does not spend further resources attempting to detect another corrupt node, but rather starts anew with a reduced network (the eliminated node no longer legally participates), and will address future failed transmissions as they arise.

48. If A=R, then re-shuffling of packets also does not occur until R receives the full SOT broadcast. See lines (A.5.97–102), which were necessarily reached at the end of the previous transmission.

49. SIG ^A[3] along outgoing edges measures the decrease in potential as a positive quantity. Thus, a positive value for SIG ^A[3] along an outgoing edge corresponds to a decrease in non-duplicated potential.

50. Notice that (D.8) is the only statement of the Lemma that involves quantities in the neighbors’ signature buffers (in addition to A’s buffers). Since there is no assumption made about the honesty of the neighbor’s of A, this may seem problematic. However, we show in the proof that regardless of the honesty of A’s neighbors B∈G, (D.8) will be satisfied if A in honest.

51. A given packet p may have multiple stays in A during a single transmission, one for each time A sees p.

52. The notation Δ _p is meant to denote the fact that we are considering the affect of p’s stay on each of the variables listed in the equation.

53. If p was a flagged packet that was deleted as on (C.7.206), then let m denote the height p had just before it was deleted, i.e. the value of H _FP when (C.7.206) is reached.

54. Since A is honest, it will never send/receive packets from any node not in \(\mathcal{P}\) by Lemma D.20.

55. Note that necessarily p is a packet corresponding to the current codeword, since packets corresponding to old codewords do not increment SIG[1], see comments on (C.4.59–60) and (C.3.11). Therefore, there are only two cases to consider.

56. Note that necessarily p is a packet corresponding to the current codeword, since packets corresponding to old codewords do not increment SIG[p], see comments on (C.4.59–60) and (C.3.11). Therefore, there are only two cases to consider.

57. We are only interested in packets p corresponding to the current codeword, and all signatures that A provides for SIG ^B[p] _A,B include the transmission index, so A’s honesty plus the inforgibility of the signature scheme imply that all of B’s signatures from A from old transmissions will not be valid.

58. As long as the adversary does not break the signature scheme, which will happen with all but negligible probability, the sender will never falsely identify an honest node.

59. The values of the quantities SIG ^B and SIG ^A all correspond to a common transmission T and refer to values the sender has received in the form of testimonies for T as on (C.6.161).

60. The values of the quantities SIG ^A correspond to some transmission T and refer to values the sender has received in the form of testimonies for T as on (C.6.161).

61. If the packet accepted corresponds to an old codeword, then SIG ^B[1] _A,B =SIG ^A[1] _A,B and SIG ^B[p] _A,B =SIG ^A[1] _A,B =⊥.

62. On a technical point, since our protocol calls for internal nodes to keep old codeword packets in their buffers from one transmission to the next, packets being transferred during some transmission may correspond to old codewords. We emphasize that the quantities in SIG _A,A , SIG[2], and SIG[3] include old codeword packets, while SIG[1] and SIG[p] do not count old codeword packets (see (C.3.11) and (C.4.59–60)).

63. This includes, but is not limited to: (1) The node has returned a (value, signature) pair, where the value is not in an appropriate domain; (2) The node has returned non-zero values indicating interaction with blacklisted or eliminated nodes; (3)The node has reported values for SIG ^A[3] _S,A that are inconsistent with the sender’s quantity SIG ^S[2] _S,A ; or (4) The node has returned outdated information in their testimony. By “outdated” information, we mean that as part of its testimony, A returned a (value, signature) pair using a signature he received in round t from one of A’s neighbors N, but in N’s testimony, N provided a (value, signature) pair from A indicating they communicated after round t and that A was necessarily using an outdated signature from N.

64. More precisely, F3 states that the sender knowingly inserted at least D packets and the receiver did not receive any packet (from the current codeword) more than once. By Fact 1′, since we are not in case S1, the receiver got fewer than D−6n ³ distinct packets corresponding to the current codeword.

65. Intuitively, A must be corrupt since the sum on the RHS of (D.39) represents the net number of packets A input minus the number of packets A output. Since this difference is larger than the capacity of A’s internal buffers, A must have deleted at least one packet and is necessarily corrupt.

66. This was proven in Observations 2–3 of Lemma B.15 for the edge-scheduling protocol. However, the proofs of these observations remain valid in the (node-controlling+edge-scheduling) model because the sender is honest (by the conforming adversary assumption).

67. Intuitively, A is corrupt since (D.43) says that it has output p more times than it input p.

Authors and Affiliations

1. Department of Computer Science, Johns Hopkins University, Baltimore, MD, USA

   Yair Amir

2. Google, Mountain View, CA, USA

   Paul Bunn

3. UCLA Departments of Computer Science and Department of Mathematics, Los Angeles, CA, USA

   Rafail Ostrovsky

Corresponding author

Correspondence to Rafail Ostrovsky.

Communicated by Oded Goldreich

A preliminary version of this paper appeared in the 6th IACR Theory of Cryptography Conference, pp. 163–182, 2009.

Part of Y. Amir’s work was done while visiting IPAM and supported in part by NSF grant 0430254.

P. Bunn’s work was supported in part by NSF grants 0430254, 0716835, 0716389 and 0830803.

Part of R. Ostrovsky’s work was done while visiting IPAM and supported in part by NSF grants CNS-0430254; CNS-0716835; CNS-0716389; CNS-0830803; CCF-0916574; IIS-1065276; CCF-1016540; CNS-1118126; CNS-1136174; US-Israel BSF grant 2008411, OKAWA Foundation Research Award, IBM Faculty Research Award, Xerox Faculty Research Award, B. John Garrick Foundation Award, Teradata Research Award, and Lockheed-Martin Corporation Research Award. This material is also based upon work supported by the Defense Advanced Research Projects Agency through the U.S. Office of Naval Research under Contract N00014-11-1-0392. The views expressed are those of the author and do not reflect the official policy or position of the Department of Defense or the U.S. Government.

Appendix A. Pseudo-Code for the Edge-Scheduling Adversarial Protocol

In this section we present pseudo-code for the Slide protocol, which will be evaluated in the next section with respect to networks operating in the edge-scheduling adversary model of Sect. 3.1. As mentioned, the Slide protocol was developed in a series of works: [2, 3, 6], and [14]. The version presented here varies slightly from these other versions, but no significant changes have been made.

In what follows, let [a..b] denote the integers between a and b (inclusive); i.e. \([a..b] = [a,b] \cap\mathbb{Z}\).

Pseudo-code for internal nodes’ setup for the edge-scheduling adversarial model.

Full size image

Additional code for sender and receiver setup.

Full size image

Routing rules for edge-scheduling adversarial model.

Full size image

Routing rules for edge-scheduling adversarial model (continued).

Full size image

Re-shuffle rules for both edge-scheduling and (node-controlling + edge-scheduling) protocols.

Full size image

Appendix B. Edge-Scheduling Protocol: Pseudo-Code Intensive Claims and Proofs

In this section we prove that our pseudo-code is consistent with the claimed properties that the Slide protocol of Sect. 4 enjoys.

The following lemma begins to link the pseudo-code with the high-level description of what the Slide protocol is doing. Recall that a buffer is in normal (respectively problem) status whenever its status bit sb is zero (respectively one). Also, an outgoing buffer is said to have a flagged packet if H _FP ≠⊥, and the flagged packet is the packet in the outgoing buffer at height H _FP . Notice that because the pseudo-code is written sequentially, things that conceptually happen simultaneously appear in the pseudo-code as occurring consecutively. In particular, when packets are moved between buffers, updating the buffers’ contents and updating the height variables does not happen simultaneously in the code, which explains the wording of the first sentence in the following lemma.

Lemma B.1

At all times (i.e. all lines of code in Figs. A.3, A.4, and A.5) EXCEPT when packets travel between buffers ((A.3.32–33), (A.4.52–53), and (A.5.89–90)), along any (directed) edge E(A,B) for any pair of internal nodes (A,B), we have

1. 1.

   If H _GP >H _IN or H _GP =⊥, then H _GP =H _IN +1 or H _GP =⊥ and \(\mathsf{IN}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{IN}}]\) and \(\mathsf{IN}[i] = \bot\thickspace\forall i \in [H_{\mathit{IN}}+1..2n]\).

2. 2.

   If ⊥≠H _GP ≤H _IN , then \(\mathsf{IN}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{GP}}-1]\) and ∀i∈[H _GP +1..H _IN +1], and \(\mathsf{IN}[i] = \bot\thickspace\forall i \in[H_{\mathit{IN}}+2..2n]\) and IN[H _GP ]=⊥.

3. 3.

   If ⊥≠H _FP >H _OUT , then sb=1 and \(\mathsf{OUT}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{OUT}}-1]\) and OUT[H _FP ]≠⊥.

4. 4.

   If H _FP =⊥ or H _FP ≤H _OUT , then \(\mathsf {OUT}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{OUT}}]\).

5. 5.

   The height of IN, as defined by the number of packets in IN (i.e. non-⊥ entries of IN), is equal to the value of H _IN .

6. 6.

   The height of OUT, as defined by the number of packets in OUT (i.e. non-null entries of OUT), is equal to the value of H _OUT .

7. 7.

   Whenever (A.4.53) is reached, H _GP ∈[1..2n] and H _IN ∈[0..2n−1].

8. 8.

   Whenever (A.3.32) is reached, H _FP ≠⊥ and H _OUT ∈[1..2n].

9. 9.

   At all times (even those listed in the hypothesis above), H _IN ,H _OUT ∈[0..2n] and H _GP ,H _FP ∈(⊥∪[1..2n]) (so the domains of these variables are correct).

Additionally, during any call to Re-Shuffle:

1. 10.

   Whenever the conditional statement on line (A.5.74) is satisfied, one packet will pass between buffers. In particular, there will be a buffer that was storing the packet before the call to Re-Shuffle that will not be storing (that instance of) the packet after the re-shuffle. Similarly, there will be another buffer that has filled a vacant slot with (an instance of) the packet in question.

2. 11.

   Flagged packets do not move. More precisely, if H _FP ≠⊥ just before any call to Re-Shuffle, then H _FP and OUT[H _FP ] will not change during that call to Re-Shuffle.

3. 12.

   Either H _GP does not change during re-shuffling or H _GP has decreased to equal H _IN +1. Also, if H _GP ≠⊥, then IN[H _GP ] does not get filled at any point during re-shuffling.

4. 13.

   If H _IN <2n before Re-Shuffling, then H _IN <2n after Re-Shuffling.

Proof of Lemma B.1

We prove each Statement of the Lemma above simultaneously by using induction on the round and line number as follows. We first prove the Lemma holds at the outset of the protocol (base case). We then notice that the above variables only change their value in the lines mentioned in the hypothesis of the Lemma and lines (A.3.28), (A.3.35), (A.4.38), (A.4.46), (A.4.50), (A.4.55), (A.4.57), (A.4.61–62), (A.4.64), and (A.5.91–94). In particular, we use the induction hypothesis to argue that as long as the statement of the Lemma is true going into each of these lines, then it will remain true when the protocol leaves each of these lines. Using this technique, we now prove each Statement listed above.

Base Case

At the outset of the protocol, H _GP and H _FP =⊥, H _IN and H _OUT =0, and all entries of IN and OUT are ⊥ (A.1.29–31) and (A.1.33–35) so Statements 1–6 and 9 are true (Statements 7, 8, and 10–13 are specific to certain lines of the pseudo-code, and there is nothing to prove for these in the base case).

Induction Step

We now prove that each of the above statements hold after leaving lines (A.3.28), (A.3.32–33), (A.3.35), (A.4.38), (A.4.46), (A.4.50), (A.4.52–53), (A.4.55), (A.4.57), (A.4.61–62), (A.4.64), (A.5.89–90), and (A.5.91–94), provided they held upon entering these lines.

Lines (A.3.28)

Statement 3 is the only relevant statement, since only sb is changed on line (A.3.28). However, since sb is set to one on this line, there is no chance that Statement 3 becomes false upon leaving (A.3.28) if it was true upon enter this line. In other words, if Statement 3 were to be false, it would not be because of line (A.3.28).

Lines (A.3.32–33)

The variables in Statements 1, 2, 5, and 7 do not change in these lines, and Statements 10–13 are not relevant here, and hence these statements remain valid by the induction hypothesis. Statement 3 is vacuously true, since H _FP is set to ⊥ at the end of line (A.3.33). Also, Statement 9 will remain valid as long as Statement 8 does, as H _FP is set to ⊥ on line (A.3.33), and H _OUT ∈[0..2n] would follow from Statement 8 since upon entering these lines, H _OUT ∈[1..2n] (Statement 8), and so subtracting 1 from H on line (A.3.33) ensures that H _OUT will remain in [0..2n−1]⊆[0..2n]. The first part of Statement 8, that H _FP ≠⊥ when (A.3.32) is reached, follows immediately from Claim B.6 below together with the fact that (A.3.30) must have been satisfied to reach (A.3.32). The second part of Statement 8 is proved below.

We next prove Statement 6. Anytime lines (A.3.32–33) are reached, the decrease of one by H _OUT on (A.3.33) represents the fact that OUT should be deleting a packet on these lines. Since the induction hypothesis (applied to Statement 6) guarantees that H _OUT matches the number of packets (non-bottom entries) of OUT before lines (A.3.32–33), the changes to H _OUT and the height of OUT on these lines will exactly match/cancel provided OUT does actually decrease in height by 1 (i.e. provided OUT[H _FP ]≠⊥). Since H _FP is changed (A.3.33) after deleting a packet (A.3.32), we may apply the induction hypothesis to Statements 3 and 4 to argue that OUT[H _FP ]≠⊥ as long as the value of H _FP was not ⊥ when line (A.3.32) was reached. This was proven above for the first part of Statement 8.

Statement 4 follows from the argument above as follows. Upon leaving line (A.3.33), H _FP =⊥, so we must show \(\mathsf{OUT}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{OUT}}]\). As was argued above, H _FP ≠⊥ when (A.3.32) is reached. If H _FP >H _OUT when (A.3.32) is reached, then by the induction hypothesis applied to Statement 3, on that same line \(\mathsf{OUT}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{OUT}}-1]\). Then when H _OUT is reduced by one on (A.3.33), we will have that \(\mathsf{OUT}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{OUT}}]\), as required.

If on the other hand H _FP ≤H _OUT when (A.3.32) is reached, then by the induction hypothesis applied to Statement 4, on that same line \(\mathsf{OUT}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{OUT}}]\). The packet at height H _FP will be deleted on (A.3.32) and the packets on top of it shifted down one if necessary, so that after (A.3.32) but before (A.3.33), we will have that \(\mathsf{OUT}[i] \neq\bot\thickspace\forall i \in [1..H_{\mathit{OUT}}-1]\). Then when H _OUT is reduced by one on (A.3.33), we will have that \(\mathsf{OUT}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{OUT}}]\), as required.

The second part of Statement 8 also follows from the arguments above as follows. First, it was shown in the proof of Statement 6 that OUT[H _FP ]≠⊥ when (A.3.32) is reached. In particular, the height of OUT is at least one going into (A.3.32), and then the induction hypothesis applied to Statement 6 implies that H _OUT ≥1 when (A.3.32) is reached, and the induction hypothesis applied to Statement 9 implies that H _OUT ≤2n when (A.3.32) is reached.

Line (A.3.35)

Since only H _FP and OUT are modified on (A.3.35), we need only verify Statements 3, 4, 6, and 9 remain true after leaving (A.3.35). Since H _FP is gets the value max(H _OUT ,H _FP ) on (A.3.35), Statement 9 will be true by the induction hypothesis (applied to Statement 9). Also, the height of OUT does not change, as (A.3.35) only swaps the location of two packets already in OUT, so Statement 6 will remain true.

Statement 3 is only relevant if H _FP >H _OUT before reaching (A.3.35), since otherwise H _FP =H _OUT upon leaving (A.3.35), and Statement 3 will be vacuously true. On the other hand, if H _FP >H _OUT , then line (A.3.35) is not reached since (A.3.34) will be false.

In order to reach (A.3.35), H _FP ≠⊥ on (A.3.34), and so both H _OUT and H _FP are not equal to ⊥ when (A.3.35) is entered (Claim B.6), and hence H _FP ≠⊥ upon leaving (A.3.35). Also, since (A.3.35) is only reached if H _FP <H _OUT (A.3.34), we use the induction hypothesis (applied to Statement 4) to argue that before reaching (A.3.35), we had that \(\mathsf{OUT}[i] \neq\bot\thickspace \forall i \in[1..H_{\mathit{OUT}}]\). In particular, both OUT[H _FP ] and OUT[H _OUT ] are storing a packet, and the call to Elevate Flagged Packet simply swaps these packets, so that after the swap, it is still the case that \(\mathsf{OUT}[i] \neq\bot\thickspace \forall i \in[1..H_{\mathit{OUT}}]\). Since in this case H _FP =H _OUT after line (A.3.35), Statement 4 will remain true.

Line (A.4.38)

H _FP is the only relevant value changed on (A.4.38), so it remains to prove the relevant parts of Statements 3, 4, and 9. We will show that whenever (A.4.38) is reached, H _OUT ∈[1..2n] and OUT[H _OUT ]≠⊥. If we can show these two things, we will be done, since when H _FP is set to H _OUT on (A.4.38), Statement 9 will be true, Statement 4 will follow from the induction hypothesis applied to either Statement 3 or 4, and Statement 3 will not be relevant. By the induction hypothesis (applied to Statement 9), H _OUT ∈[0..2n] when (A.4.38) is reached. The fact that (A.4.38) was reached means that the conditional statement on the line before (A.4.37) was satisfied, and thus OUT is in normal status (sb=0) and H _OUT ∈[1..2n] (the latter is true by the induction hypothesis applied to Statement 9 with respect to H _IN and H _OUT ). By the induction hypothesis (applied to Statement 3), the fact that sb=0 going into (A.4.37) implies that H _FP =⊥ or H _FP ≤H _OUT going into (A.4.37), and then the induction hypothesis (applied to Statement 4) says that OUT[H _OUT ]≠⊥ when (A.4.38) is entered.

Lines (A.4.46) and (A.4.50)

The parts of Statements 1, 2, and 9 that involve changes to H _GP are the only statements that are affected by these lines. If the conditional statement on these lines are not satisfied, then no values change, and there is nothing to prove. We therefore consider the case that the conditional statement is satisfied. Then H _GP is set to H _IN +1 on these lines, and hence Statement 2 is vacuously satisfied. Since we are assuming H _GP changes value on (A.4.46) or (A.4.50), the conditional statement says that H _GP =⊥ or H _GP >H _IN going into (A.4.46) (respectively (A.4.50)). By the induction hypothesis (applied to Statement 1), IN[i]≠⊥ for all 1≤i≤H _IN , and IN[i]=⊥ for all i>H _IN . Therefore, since IN and H _IN do not change on (A.4.46) or (A.4.50), Statement 1 will remain true upon leaving these lines. Finally, for Statement 9, we need only show H _GP ∈[1..2n] upon leaving line (A.4.46) (respectively line (A.4.50)). If H _GP >H _IN going into line (A.4.46) (respectively line (A.4.50)), then the change to H _GP is non-positive, and so the induction hypothesis applied to Statements 1 and 9 guarantee H _GP will be in [1..2n] upon leaving these lines. On the other hand, if H _GP =⊥ going into either of these lines, then H _IN <2n, and the induction hypothesis applied to Statement 9 indicates that H _IN ∈[0..2n−1] going into these lines, and hence H _GP ∈[1..2n] upon leaving either line.

Lines (A.4.52–53)

Statements 1, 2, 5, 7, and 9 are the only statements that are affected by these lines. Notice that H _GP necessarily equals ⊥ when leaving (A.4.53), so Statement 2 is vacuously satisfied.

We prove Statement 1 first. Recall that the height of an incoming buffer refers to the number of (non-ghost) packets the buffer currently holds. Since H _GP will necessarily equal ⊥ when leaving line (A.4.53), we must show that \(\mathsf{IN}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{IN}}]\) and \(\mathsf{IN}[i] = \bot\thickspace\forall i \in[H_{\mathit{IN}}+1..2n]\) upon leaving line (A.4.53). Both of these follow immediately from the induction hypothesis applied to Statements 1 and 2, as follows. By the induction hypothesis applied to Statements 1, 2, and 9, either H _GP =⊥, 1≤H _GP ≤H _IN , or H _GP =H _IN +1≤2n when line (A.4.52) is reached. We consider each case:

• If H _GP =H _IN +1 when we reach line (A.4.52), then by the induction hypothesis (applied to Statement 1) it will also be true that \(\mathsf{IN}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{IN}}]\) and \(\mathsf{IN}[i] = \bot \thickspace\forall i \in[H_{\mathit{IN}}+1..2n]\) when this line is reached. While on line (A.4.53), first IN[H _GP ]=IN[H _IN +1] is filled with a packet, and then H _IN is increased by one, and so Statement 1 will remain true by the end of line (A.4.53).

• If 1≤H _GP ≤H _IN when the protocol reaches (A.4.52), then also when this line is reached we have that (by the induction hypothesis applied to Statement 2) \(\mathsf {IN}[i] \neq\bot\thickspace\forall i \in[1..H_{\mathit{GP}}-1]\) and ∀i∈[H _GP +1..H _IN +1], and \(\mathsf{IN}[i] = \bot\thickspace \forall i \in[H_{\mathit{IN}}+2..2n]\) and IN[H _GP ]=⊥. When a packet is inserted into slot H _GP and H _IN is increased by one on line (A.4.53), we will therefore have that all slots between 1 and (the new value of) H _IN will have a packet, and all other slots will be ⊥, and thus Statement 1 will hold.

• If H _GP =⊥ going into line (A.4.52), then H _GP will be set to H _IN +1 on this line, and then we can repeat the argument of the top bullet point, provided H _IN +1≤2n. If sb _OUT =1, then Statement 4 of Lemma B.12 states that H _GP ≠⊥ when (A.4.52) is reached, contradicting the fact we are in the case H _GP =⊥. So we may assume sb _OUT =0, and then the fact that (A.4.52) was reached means that (A.4.47) must have been satisfied because H _OUT >H _IN . Since both of these variables live in [0..2n] by the induction hypothesis applied to Statement 9, we conclude H _IN <2n on (A.4.47), and it cannot change value between then and (A.4.52).

The first part of Statement 7 is proven in the above three bullet points. For the second part, if sb _OUT =0 when (A.4.47) was evaluated earlier in the round, then the fact that (A.4.53) was reached means H _OUT >H _IN , and then the second part of Statement 7 follows from the induction hypothesis applied to Statement 9. If on the other hand sb _OUT =1 when (A.4.47) was evaluated, then the second part of Statement 7 follows from Statement 5 of Lemma B.12.

We now prove Statement 5. There are two relevant changes made on line (A.4.53) that affect Statement 5: a packet is added to IN[H _GP ] and H _IN is increased by one. The argument in the preceding paragraph showed that when (A.4.53) is reached, H _GP ∈[1..2n] and IN[H _GP ]=⊥, and therefore the net effect of (A.4.53) is to increase the number of packets stored in IN by one and to increase H _IN by one. Therefore, since Statement 5 was true going into line (A.4.53) by the induction hypothesis, it will remain true upon leaving (A.4.53).

It remains to prove the parts of Statement 9 not yet proven, namely that at all times H _IN ∈[0..2n] and H _GP ∈⊥∪[1..2n]. As was proven in the third bullet point above, if (A.4.52) is satisfied, then H _IN <2n, and hence the change there does not threaten the domain of H _GP . Also, (A.4.53) sets H _GP to ⊥, which is again in the valid domain. Meanwhile, on (A.4.53) H _IN is changed to H _IN +1≤2n, where the inequality follows from the induction hypothesis applied to Statement 7.

Line (A.4.55), (A.4.57), and (A.4.64)

Since IN and H _GP are the only relevant quantities that change value on these lines, only the relevant parts of Statements 1, 2, and 9 must be proven. Since H _GP is set to ⊥ on these lines, Statement 9 is immediate and Statement 2 is vacuously true. It remains to prove Statement 1. If H _GP =⊥ going into (A.4.55), (A.4.57), or (A.4.64), then H _GP and IN will not change, and the inductive hypothesis (applied to Statement 1) will ensure that Statement 1 will continue to be true upon exiting any of these lines. If 1≤H _GP ≤H _IN when (A.4.55), (A.4.57), or (A.4.64) is entered, then we may apply the induction hypothesis to Statement 2 to conclude that \(\mathsf{IN}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{GP}}-1]\) and ∀i∈[H _GP +1..H _IN +1], and \(\mathsf{IN}[i] = \bot\thickspace\forall i \in[H_{\mathit{IN}}+2..2n]\) and IN[H _GP ]=⊥. In particular, there is a gap in IN where a “ghost packet” is being stored, and this gap will be filled when Fill Gap is called on (A.4.55), (A.4.57) or (A.4.64). Namely, this will shift all the packets from height H _GP +1 through H _IN +1 down one spot, so that after Fill Gap is called, \(\mathsf{IN}[i] \neq\bot \thickspace\forall i \in[1..H_{\mathit{IN}}]\) and \(\mathsf{IN}[i] = \bot \thickspace\forall i \in[H_{\mathit{IN}}+1..2n]\), which is Statement 1. Finally, if H _GP >H _IN when (A.4.55), (A.4.57) or (A.4.64) is entered, then Fill Gap will not do anything, and so IN will not change. Since Statement 1 was true going into these lines (by our induction hypothesis), it will remain true upon exiting these lines.

Line (A.4.61–62)

The only relevant variables to change values on these lines are sb _OUT , H _OUT , H _FP , and OUT, so we need only verify that Statements 3, 4, 6, and 9 remain true after leaving (A.4.61–62). First note that H _FP ≠⊥ upon reaching (A.4.61) (since (A.4.60) must be satisfied to reach (A.4.61–62)), so the induction hypothesis (applied to Statements 3 and 4) implies that OUT[H _FP ]≠⊥ when (A.4.61) is reached. Therefore, by the induction hypothesis applied to Statement 6, H _OUT ≥1 when (A.4.61) is reached, and hence H _OUT ∈[1..2n] upon reaching (A.4.61) by the induction hypothesis (applied to Statement 9). In particular, when H _OUT is reduced by one on (A.4.62), we will have that H _OUT ∈[0..2n−1] upon leaving (A.4.62), as required. Also, H _FP will be set to ⊥ upon leaving (A.4.62), so Statement 9 remains true.

Statement 6 also follows from the fact that OUT[H _FP ]≠⊥ when (A.4.61) is reached, as follows. Since (by induction) Statement 6 was true upon reaching (A.4.61), the packet deleted from OUT on (A.4.61) is accounted for by the drop in H _OUT on (A.4.62).

Statement 3 is vacuously true upon leaving (A.4.62), so it remains to prove Statement 4. This argument is identical to the one used to prove Statement 4 in lines (A.3.32–33) above.

Lines (A.5.89–94)

We first prove Statements 10–13, and then address Statements 1–9. We first prove that before Shuffle Packet is called on (A.5.77), we have that B _F [M]≠⊥ and B _T [m+1]=⊥, from which Statement 10 follows.

• If B _F is an outgoing buffer and H _FP =⊥ or \(H_{\mathit{FP}} < H_{B_{F}}\), then \(M = H_{B_{F}}\) (the conditional statement on lines (A.5.80) and (A.5.82) will fail), and then B _F [M]≠⊥ by the induction hypothesis applied to Statement 4.

• If B _F is an outgoing buffer and \(H_{\mathit{FP}} \geq H_{B_{F}}\), then \(M = H_{B_{F}}-1\) (the conditional statement on line (A.5.80) will pass), and then B _F [M]≠⊥ by the induction hypothesis applied to Statement 3 or 4 (that \(M = H_{B_{F}}-1\) is greater than zero follows from the fact that \(H_{B_{F}} \geq2\) in order for (A.5.74) to be true, since m≥0 by the induction hypothesis applied to Statement 9, and then the comment on (A.5.74), together with the fact that B _F is an outgoing buffer, means that \(H_{B_{F}} \geq2\)).

• If B _F is an incoming buffer and B _F [M+1]≠⊥, then (A.5.82) is satisfied and M is set to M+1 on line (A.5.83), and thus for the new value of M, B _F [M]≠⊥ after line (A.5.83).

• Suppose B _F is an incoming buffer and B _F [M+1]=⊥. Notice that the induction hypothesis applied to Statement 2 and the fact that B _F [M+1]=⊥ imply that H _GP =⊥ or H _GP >H _IN =M. Therefore, the induction hypothesis applied to Statement 1 implies that B _F [M]≠⊥.

• If B _T is an outgoing buffer and B _T [m]=⊥, then the conditional statement on line (A.5.84) will be satisfied, and hence m is set to m−1. Thus after line (A.5.85), B _T [m+1]=⊥.

• If B _T is an outgoing buffer and B _T [m]≠⊥, then the induction hypothesis applied to Statements 3, 4, and 6 imply that B _T [m+1]=⊥.

• If B _T is an incoming buffer and H _GP =⊥, then the value of m is not changed on line (A.5.86), and so m+1=H _IN +1. The induction hypothesis applied to Statement 1 then implies that B _T [m+1]=⊥.

• If B _T is an incoming buffer and H _GP ≠⊥, then B _T [H _IN +2]=⊥ by the induction hypothesis applied to Statement 2, and thus after m is changed to m+1 on (A.5.87), we have that B _T [m+1]=B _T [H _IN +2]=⊥, as required.

For Statements 11–13, we need to change notation slightly, since Re-Shuffling can occur between two buffers of any types (except outgoing to incoming). To prove these statements, we therefore treat four cases: (1) B _F is an outgoing buffer, (2) B _F is an incoming buffer, (3) B _T is an outgoing buffer, (4) B _T is an incoming buffer. We then prove the necessary statements in each case.

Case 1. :

The value of B _F [M]=OUT[M] is changed on line (A.5.90), and hence Statement 11 will hold provided M≠H _FP . The top two bullet points above guarantee that this is indeed the case. Statements 12 and 13 are not relevant unless B _T is an incoming buffer, which will be handled in case 4 below.

Case 2. :

For Statement 13, the only relevant change to H _IN is on line (A.5.92), where H _IN decreases in value, and hence Statement 13 will remain true. For the first part of Statement 12, the only place H _GP can change is line (A.5.94). But if H _GP does change value here, then the conditional statement on the previous line guarantees that H _GP decreases to H _IN +1. Statement 11 and the second part of Statement 12 are not relevant to this case.

Case 3. :

The value of B _T [m+1]=OUT[m+1] is changed on line (A.5.89), and hence Statement 11 will hold provided m+1≠H _FP . But we have already shown Statement 10 remains true, and in particular the slot that is filled on line (A.5.89) was vacant. If H _FP ≠⊥, then by the induction hypothesis applied to Statements 3 and 4, OUT[H _FP ]≠⊥, and hence OUT[m+1]=⊥ implies that m+1≠H _FP . Statements 12 and 13 are not relevant to this case.

Case 4. :

Since B _T is an incoming buffer, the condition on line (A.5.74) implies that the value of m (which is the height of B _T ) on line (A.5.73) must be at most 2n−2 (M−m>1 and M,m∈[0..2n] by induction hypothesis applied to Statement 9). Therefore, when the height of B _T is increased by one on line (A.5.91), it will be at most 2n−1, and so Statement 13 will remain true. For the second part of Statement 12, we must show that the value of m+1 on line (A.5.89) is not equal to H _GP . In the case that H _GP ≠⊥ on line (A.5.86), the value of m will change to H _IN +1 on line (A.5.87), and then the induction hypothesis applied to Statement 1 implies that H _GP ≤H _IN +1=m and so H _GP ≠m+1 on line (A.5.89). Statement 11 and the first part of Statement 12 are not relevant for this case.

It remains to verify Statements 1–9. There are two parts to proving Statements 1 and 2: we must show they hold when B _F is an incoming buffer and also when B _T is an incoming buffer. For the latter part, Statements 1 and 2 will be true if we can show that anytime an incoming buffer’s slot is filled as on line (A.5.89), the slot was either slot H _IN +1 (in the case that H _GP =⊥) or H _IN +2 (in the case that H _GP ≠⊥). These facts follow immediately from the definition of m on line (A.5.73) and lines (A.5.86–87) and (A.5.89). For the former part, Statements 1 and 2 will remain true provided the packet taken from B _F on line (A.5.89) is the top-most packet in B _F . Looking at the conditional statement on line (A.5.82), if IN[H _IN +1]≠⊥, then by the induction hypothesis applied to Statements 1 and 2, we must have that IN[H _IN +1] is the top-most non-null packet, which is the packet that will be taken from B _F on line (A.5.89) (since in this case M=H _IN is changed to H _IN +1 on line (A.5.83)). On the other hand, if IN[H _IN +1]=⊥ on line (A.5.82), then the induction hypothesis applied to Statements 1 and 2 imply that IN[H _IN ] is the top-most non-null packet, which is exactly the packet taken on line (A.5.89) (since the conditional statement on line (A.5.82) will not be satisfied, and hence the value of M will not be changed on line (A.5.83)).

Similarly, there are two parts to proving Statements 3 and 4: we must show they hold when B _F is an outgoing buffer and also when B _T is an outgoing buffer. The former part will be true provided the packet taken from B _F on line (A.5.89) is the top-most non-flagged packet. If H _FP =⊥, then there is no flagged packet, and hence the packet taken from B _F will be the top packet, i.e. the packet in index B _F [H _OUT ] (see lines (A.5.72), (A.5.80–81), and (A.5.89)). If H _FP ≠⊥ and H _FP <H _OUT , then investigating those same lines also shows the top packet will be taken from B _F (which is not flagged since H _FP <H _OUT by assumption). If H _FP ≥H _OUT , then line (A.5.80) will be satisfied, shifting the value of M to H _OUT −1 on line (A.5.81). By the induction hypothesis applied to Statement 3, this new value of M corresponds to the top-most non-flagged packet of B _F .

When B _T is an outgoing buffer, Statements 3 and 4 will be true provided the packet given to B _T takes the first free slot in B _T (in particular, the packet will not over-write a flagged packet’s spot). If B _T [H _OUT ]≠⊥ on line (A.5.84), then the induction hypothesis applied to Statements 3, 4, and 6 imply that all slots of B _T between [1..H _OUT ] are non-⊥, and all spots above H _OUT are ⊥. Therefore, (since in this case the conditional statement on line (A.5.84) fails and hence the value of m does not change on the next line) the definition of m on line (A.5.73) and line (A.5.89) show that the first free slot of B _T will be filled. On the other hand, if B _T [H _OUT ]=⊥ on line (A.5.84), then by the induction hypothesis, we must have that B _T [H _OUT ] is the first free slot of B _T , and by investigating lines (A.5.73), (A.5.84–85), and (A.5.89), this is exactly the spot that is filled.

Statements 5 and 6 remain true by the fact that Statement 10 was proven true and lines (A.5.91) and (A.5.92). To satisfy the condition on line (A.5.74), it must be that \(H_{B_{F}} = M \geq1\) and \(H_{B_{T}} = m <2n\), and hence the changes made to \(H_{B_{F}}\) and \(H_{B_{T}}\) on lines (A.5.91) and (A.5.92) will guarantee the parts of Statement 9 regarding H _OUT and H _IN remain true. Also, H _GP remains in the appropriate domain by induction applied to Statements 9, 12, and 13. Statements 7, 8, are not relevant.  □

Lemma B.2

The domains of all of the variables in Figs. A.1 and A.2 are appropriate. In other words, the protocol never calls for more information to be stored in a node’s variable (buffer, packet, etc.) than the variable has room for.

Proof

Below we fix a node N∈G and track changes to each of its variables.

Outgoing Buffers OUT (A.1.08).:

Each entry of OUT is initialized to ⊥ on (A.1.33). After this point, Statement 6 of Lemma B.1 above guarantees OUT will need to hold at most H _OUT packets, and since H _OUT is always between 0 and 2n (by Statement 9 of Lemma B.1) and packets have size P, the domain for OUT is as indicated.

Copy of Packet to be Sent \(\tilde{p}\) (A.1.09).:

This is initialized to ⊥ on (A.1.34), and is only modified afterwards on (A.4.38), (A.3.33), and (A.4.62). By Statements 3, 4, and 9 of Lemma B.1, OUT[H]≠⊥ when \(\tilde{p}\) is set on (A.4.38) (since sb=0 must have been true on (A.4.37) in order to reach (A.4.38)), and the changes on (A.3.33) and (A.4.62) reset \(\tilde {p}\) to ⊥. Therefore, the domain of \(\tilde{p}\) is as indicated.

Outgoing Status Bit sb (A.1.10).:

This is initialized to 0 on (A.1.35), and is only modified afterwards on lines (A.3.33), (A.3.28), and (A.4.62), all of which change sb to 0 or 1, as required.

Packet Sent Bit d (A.1.11).:

This is initialized to 0 on (A.1.35), and is only modified afterwards on lines (A.3.26), (A.4.40), and (A.4.62), each of which change d to 0 or 1, as required.

Flagged Round Index FR (A.1.12).:

This is initialized to ⊥ on (A.1.34), and is only modified afterwards on lines (A.4.38), (A.3.33), and (A.4.62). The latter two lines reset FR to ⊥, while (A.4.38) sets FR to the index of the current stage and round t, and since there are 3D rounds per transmission and 2 stages per round (A.3.02), so when FR is set to t on (A.4.38), it will be in [0..6D], as required.

Height of Outgoing Buffer H (A.1.13).:

This is initialized to 0 on (A.1.35). After this point, Statement 9 of Lemma B.1 above guarantees H∈[0..2n], as required.

Height of Flagged Packet H _FP (A.1.14).:

Statement 9 of Lemma B.1 guarantees that H _FP will lie in the appropriate domain at all times.

Round Adjacent Node Last Received a Packet RR (A.1.15).:

This is initialized to ⊥ on (A.1.34), and is only modified afterwards when it is received on (A.3.06), where it is either set to the received value or ⊥ if nothing was received. As discussed below, the incoming buffer’s value for RR always lies in the appropriate domain, and hence so will the value received on (A.3.06).

Outgoing Buffer’s Value for Adjacent Node’s Incoming Buffer Height H _IN (A.1.16).:

This is initialized to 0 on (A.1.35), and is only modified afterwards on line (A.3.06), where it is set to the value sent on (A.3.09) by the adjacent node, or ⊥ in case no value was received. Since the value sent on (A.3.09) will always be between 0 and 2n (by Statement 9 of Lemma B.1), H _IN has the required domain.

Incoming Buffers IN (A.1.18).:

Each entry of IN is initialized to ⊥ on (A.1.29). After this point, Statement 5 of Lemma B.1 above guarantees IN will need to hold at most H _IN packets, and since H _IN is always between 0 and 2n (by Statement 9 of Lemma B.1) and packets have size P, the domain for IN is as indicated.

Packet Just Received p (A.1.19).:

This is initialized to ⊥ on (A.1.30), and is only modified afterwards on (A.4.43), where it either is set to the value sent on (A.4.41) or ⊥ in the case no value was received. Since the value sent on (A.4.41) has the appropriate domain (i.e. the size of a packet, P), in either case p has the appropriate domain.

Incoming Status Bit sb (A.1.20).:

This is initialized to 0 on (A.1.31), and is only modified afterwards on lines (A.4.45), (A.4.49), (A.4.53), (A.4.55), (A.4.57), and (A.4.64), all of which change sb to 0 or 1 as required.

Round Received Index RR (A.1.21).:

This is initialized to −1 on (A.1.31), and is only modified afterwards on lines (A.4.53) and (A.4.64). The former sets RR to the index of the current stage and round t, and since there are 3D rounds per transmission and 2 stages per round (A.3.02), setting RR=t as on (A.4.53) will put RR in [0..6D] as required. Meanwhile, (A.4.64) resets RR to −1. Thus, at all times, RR is in the appropriate domain.

Height of Incoming Buffer H (A.1.22).:

This is initialized to 0 on (A.1.31). After this point, Statement 9 of Lemma B.1 above guarantees H∈[0..2n], as required.

Height of Ghost Packet H _GP (A.1.23).:

Statement 9 of Lemma B.1 guarantees that H _GP will lie in the appropriate domain at all times.

Incoming  Buffer’s  Value  for  Adjacent  Node’s  Outgoing  Buffer  Height   H _OUT  (A.1.24).:

This is initialized to 0 on (A.1.31), and is only modified afterwards on line (A.3.11), where it is set to be one of the values sent on (A.3.05) by the adjacent node, or ⊥ in case no value was received. Since the value sent on (A.3.05) (either H _OUT or H _FP ) will always be ⊥ or a number between 1 and 2n (see domain argument above for an outgoing buffer’s height of flagged packet variable H _FP ), H _OUT has the required domain.

Incoming Buffer’s Value for Adjacent Node’s Status Bit sb _OUT (A.1.25).:

This is initialized to 0 on (A.1.31), and is only modified afterwards on lines (A.3.10) and (A.3.11). Both changes assign sb _OUT to ‘0’ or ‘1’, as required.

Incoming Buffer’s Value for Adjacent Node’s Flagged Round Index FR (A.1.26).:

This is initialized to ⊥ on (A.1.30), and is only modified afterwards on lines (A.3.10–11) and (A.4.43). Each of these times, FR is either set to the value sent by the adjacent node, or ⊥ in the case nothing was received. Since the values sent on (A.3.05) and (A.4.41) live in [0..6D]∪⊥ (see argument above for an outgoing buffer’s variable FR living in the appropriate domain), so does FR.

Sender’s Count of Packets Inserted κ (A.2.37).:

We want to argue that at all times, κ corresponds to the number of packets (corresponding to the current codeword) that the sender has knowingly inserted. Lines (A.2.39) and (A.4.69) guarantee that κ=0 at the outset of any transmission. The only other place κ is modified is (A.3.31) where it is incremented by one, so we must argue that (A.3.31) is reached exactly once for every packet the sender knowingly inserts. By “knowingly” inserting a packet, we mean that the sender has received verification that the adjacent node has received and stored the packet, and hence the sender can delete the packet.

Suppose that in some round t, the sender sends a packet p as on (A.4.41). By Claim B.9 below, the sender will not to try and send any other packet besides p to its neighbor until he receives confirmation of receipt for p. There are two things to show: (1) If the sender does not receive confirmation of receipt, then κ is never incremented as on (A.3.31), and (2) If the sender does receive confirmation of receipt, then κ is incremented exactly once. By “receiving confirmation of receipt,” we mean that line (A.3.30) is satisfied in some round t′ when the sender’s value for \(\tilde{p}\) equals the packet p sent in round t (see Definition B.8 below). Clearly, (1) will be true since (A.3.31) will never be reached if (A.3.30) is never satisfied. For (2), suppose that in some later round t′>t the sender gets confirmation of receipt for p. Clearly line (A.3.31) is reached this round, and κ is incremented by one there. We must show κ will not be incremented due to p ever again. To see this, p will be deleted on line (A.3.32–33) of round t′, and therefore this packet can cause the sender to reach (A.3.31) at most once.^{Footnote 36} Thus, at all times κ corresponds to the number of packets (corresponding to the current codeword) that the sender has knowingly inserted, as desired. Since each codeword has D packets, the domain for κ is as required.

Receiver’s Storage Buffer I _R (A.2.40).:

Each entry of I _R is initialized to ⊥ on (A.2.43), after which it is only modified on lines (A.5.101) and (A.4.67). The latter resets I _R , while the former sets entry κ of I _R to the packet in IN[1]. We show below that κ will always accurately represent the number of current codeword packets the receiver has received, and hence will be a value between 0 and D. It remains to show that IN[1] will always hold a packet when (A.5.101) is reached. We use Claim B.5 below which states that for the receiver, anytime H _IN >0, H _GP =⊥. Therefore, whenever (A.5.99) is satisfied, Statement 1 of Lemma B.1 (together with the argument that IN has the appropriate domain) state that IN[1] will hold a packet, as required.

Receiver’s Number of Packets Received κ (A.2.41).:

We want to show that κ always equals the number of packets corresponding to the current codeword the receiver has received so far. Lines (A.2.42) and (A.4.67) guarantee that κ=0 at the outset of any transmission. The only other place κ is modified is (A.5.101) where it is incremented by one, so we must argue that (A.5.101) is reached exactly once for every packet (corresponding to the current codeword) that the receiver receives. By Statement 1 of Lemma B.1 and Claim B.5 below, anytime (A.5.101) is reached, IN[1] necessarily stores a packet. This packet is added to I _R on (A.5.101) and then is promptly deleted from IN on (A.5.102). By Claim B.15, the receiver will never enter (A.5.100) twice due to the same packet, and hence (A.5.101) is reached exactly once for every distinct packet corresponding to the current codeword (see comments on (A.5.100) and (A.5.104)). Therefore, κ always equals the number of packets corresponding to the current codeword the receiver has received so far, as desired. Since there are D packets per codeword, κ∈[0..D], as required.  □

Claim B.3

After re-shuffling, (and hence at the very end/beginning of each round), all of the buffers of each node are balanced. In particular, there are no incoming buffers that have height strictly bigger than any outgoing buffers, and the difference in height between any two buffers is at most one.

Proof

We prove this using induction (on the round index), noting that all buffers are balanced at the outset of the protocol (lines (A.1.29) and (A.1.33)). Consider any node N in the network, and assume that its buffers are all balanced at the end of some round t. We need to show the buffers of N will remain balanced at the end of the next round t+1. Let B ₁ and B ₂ denote any two buffers of N, and let h ₁ be the variable denoting the height of B ₁ and h ₂ the height of B ₂. Suppose for the sake of contradiction that h ₁≥h ₂+2 at the end of round t+1 (after re-shuffling). Let H denote the height of the maximum buffer in N at the end of t+1, so H≥h ₁≥h ₂+2. Also let h denote the height of the minimum buffer in N at the end of t+1, so h≤h ₂≤H−2. But then the Re-Shuffle Rules dictate that N should have kept re-shuffling (A.5.72–74), a contradiction.

Similarly, assume for contradiction that there exists an incoming buffer whose height h ₂ is bigger than that of some outgoing buffer that has height h ₁. Let H and h be as defined above, so we have that h≤h ₁<h ₂≤H. In the case that h ₂=H, Re-Shuffle Rules (A.5.72) guarantee that an incoming buffer will be selected to take a packet from. Also, if h=h ₁, then Re-Shuffle Rules (A.5.73) guarantee that an outgoing buffer will be chosen to give a packet to. Therefore, in this case a packet should have been re-shuffled (A.5.74), and hence we have contradicted the fact that we are at the end of the Re-Shuffle phase of round t. On the other hand, if h≠h ₁ or H≠h ₂, then H−h≥2, and again Re-Shuffling should not have terminated (A.5.74). □

Lemma B.4

Every change in network potential comes from one of the following three events:

1. 1.

   S inserts a packet into the network.

2. 2.

   R receives a packet.

3. 3.

   A packet that was sent from one internal node to another is accepted; the verification of packet receipt is received by the sending node; a packet is shuffled between buffers of the same node; or a packet is moved within a buffer.

Furthermore, changes in network potential due to item (1) are strictly non-negative and changes due to item (2) are strictly non-positive. Also, changes in network non-duplicated potential due to item (3) are strictly non-positive. Finally, at all times, network packet duplication potential is bounded between zero and 2n ³−8n ²+8n.

Proof

Since network potential counts the heights of the internal nodes’ buffers, it only changes when these heights change, which in turn happens exclusively when there is packet movement. By reviewing the pseudo-code, we see that this happens only on lines (A.4.32), (A.4.35), (A.4.53), (A.4.55), (A.4.57), (A.4.61), (A.4.64), and (A.5.89–90). Each of these falls under one of the three items listed in the Lemma, thus proving the first statement in the Lemma. That network potential changes due to packet insertion by S are strictly non-negative is obvious (either the receiving node’s potential increases by the height the packet assumed, as on (A.4.53), or the receiving node is R and the packet does not contribute to potential). Similarly, that potential change upon packet receipt by R is strictly non-positive is clear, since packets at R do not count towards potential (see Definition 4.7). Also, since only flagged packets (but not necessarily all of them) contribute to network packet duplication potential, the biggest it can be is the maximal number of flagged packets that can exist in the network at any given time, times the maximum height each flagged packet can have. By Claim B.14, there are at most (n−2)² flagged packets in the network at any given time, and each one has maximal height 2n (Lemma B.1, part 9), so network packet duplication potential is bounded by 2n ³−8n ²+8n.

It remains to prove that changes in network non-duplicated potential due to item (3) are strictly non-positive. To do this, we look at all lines on which there is packet movement, and argue each will result in a non-positive change to non-duplicated potential. Clearly potential changes on lines (A.4.32), (A.4.55), (A.4.57), (A.4.61), and (A.4.64) are non-positive. Also, if (A.4.35) is reached, if R has already accepted the packet, then that packet’s potential will count towards duplicated potential within the outgoing buffer, and so the change in potential as on (A.4.35) will not affect non-duplicated potential. If on the other hand R has not already accepted the packet, then the flagged packet still counts towards non-duplication potential in the outgoing buffer. Since the result of (A.4.35) is simply to swap the flagged packet with the top packet in the buffer, the net change in non-duplication potential is zero. That changes in potential due to re-shuffling packets (A.5.89–90) are strictly non-positive follows from Claim B.13 below. It remains to check the cases that a packet that was transferred between two internal nodes is accepted (A.4.53). Notice that upon receipt there are two changes to network non-duplicated potential: it increases by the height the packet assumes in the incoming buffer it arrived at (A.4.53), and it decreases by the height the packet had in the corresponding outgoing buffer (this decrease is because the flagged packet in the outgoing buffer will count towards packet duplication potential instead of non-duplicated potential the instant the packet is accepted). The decrease outweighs the increase since the packet’s height in the incoming buffer is less than or equal to the height it had in the corresponding outgoing buffer (Claim B.13). □

Claim B.5

For any of the receiver’s buffers IN, H _IN =0 at the start of every round. Also, anytime H _IN >0, H _GP =⊥.

Proof

H=H _IN is set to 0 at the outset of the protocol (A.1.31). The first statement follows immediately from line (A.5.102), where each of the receiver’s incoming buffers IN have H _IN reset to zero during the re-shuffle phase of every round. For the second statement, we will show that whenever H changes value from 0 in any round t, that H _GP will be set to ⊥ at the same time, and neither will change value until the end of the round when H will be reset to zero during re-shuffling. In particular, the only place H can change from zero is on (A.4.53). Suppose (A.4.53) is reached in some round t, changing H from zero to 1, and also changing H _GP to ⊥. Looking at the pseudo-code, neither H nor H _GP can change value until line (A.5.102), where H is reset to zero. Therefore, H can only be non-zero between lines (A.4.53) and (A.3.21) (when Receiver Re-Shuffle is called) of a given round, and at these times H _GP is always equal to ⊥. □

Claim B.6

Let OUT be any outgoing buffer, and H _FP , FR, and sb denote the height of it flagged packet, round the packet was flagged, and status bit, respectively (see (A.1.10), (A.1.12), (A.1.14)). Then H _FP =⊥⇔FR=⊥. Also, anytime OUT has no flagged packets (i.e. H _FP =⊥), OUT has normal status (i.e. sb=0).

Proof

The first statement is true at the outset of the protocol (A.1.34), so it will be enough to make sure that anytime H _FP or FR changes value from ⊥ to non-⊥ (or vice versa), the other one also changes. Examining the pseudo-code, these changes occur only on lines (A.3.33), (A.4.38), and (A.4.62), where it is clear H _FP takes on a non-⊥ (respectively ⊥) value if and only if FR does.

The second statement is true at the outset of the protocol (A.1.34–35). So it is enough to show: (1) anytime H _FP is set to ⊥, sb is equal to zero, and (2) anytime sb changes to one, H _FP ≠⊥. The former is true since anytime H _FP changes to ⊥, sb is set to zero on the same line ((A.3.33) and (A.4.62)), while the latter is true since sb only changes to one on (A.3.28), which can only be reached if FR≠⊥ (A.3.27), which by the first statement of this claim implies H _FP ≠⊥. □

Claim B.7

The following two statements are true:

1. 1.

   Anytime sb _OUT is equal to 1 when Create Flagged Packet is called on line (A.3.15), H _FP ≠⊥.

2. 2.

   Anytime Send Packet is called on line (A.3.17), the flagged packet has height at least one (i.e. H _FP is at least one anytime Send Packet is called).

Proof

We prove the second statement by separating the proof into the following two cases.

Case 1: sb _OUT =0 at the start of Stage 2.:

Since Send Packet is called, the conditional statement on line (A.3.16) was satisfied. Therefore, since we are in the case sb _OUT =0 on that line (sb _OUT cannot change values between (A.3.12) and (A.3.16)), then H _OUT >H _IN . Tracing H _IN backwards, it was received on line (A.3.06) and represents the value of H _IN that was sent on line (A.3.09). Using Statement 9 of Lemma B.1, H _IN ≥0 and hence the value of H _OUT on (A.3.16) must be at least one. Since H _OUT and H _IN cannot change between lines (A.3.15) and (A.3.16) of any round, when Create Flagged Packet was called, it was still true that sb _OUT =0 and H _OUT >H _IN ≥0. Therefore, line (A.4.37) will be satisfied and (A.4.38) will set H _FP =H _OUT ≥1 as required.

Case 2: sb _OUT =1 at the start of Stage 2.:

Let t denote some round where sb _OUT =1 at the start of Stage 2. Our strategy will be to find the most recent round that sb _OUT switched from 0 to 1, and argue that the value that H _FP acquired in that round has not changed. So let \(\mathtt{t_{0}}+1\) denote the most recent round that sb _OUT had the value 0 at any stage of the round. We argue that sb _OUT =1 by the end of t ₀+1, and sb _OUT =0 at the start of Stage 2 of round t ₀ (the round before t ₀+1) as follows:

• If sb _OUT equals 0 by the end of round \(\mathtt{t_{0}}+1\), then it will at the start of round \(\mathtt{t_{0}}+2\), contradicting the choice of \(\mathtt{t_{0}}+1\).

• If sb _OUT =1 at the start of Stage 2 of round t ₀, then sb _OUT must have changed its value to 0 sometime between Stage 2 of round t ₀ and the end of round t ₀+1 (since sb _OUT =0 at some point of round t ₀+1 by definition). This can only happen on line (A.3.33) inside the Reset Outgoing Variables function of round t ₀+1 (this is the only place that sb _OUT can be set to zero). However, since sb _OUT cannot change between the time that Reset Outgoing Variables is called on line (A.3.07) and the end of the round, it must be that sb _OUT was equal to zero at the start of round t ₀+2, contradicting the choice of t ₀+1.

Now since sb _OUT =0 at the start of round \(\mathtt{t_{0}}+1\) (it cannot change between Stage 2 of t ₀ and the start of t ₀+1), and sb _OUT =1 by the end of t ₀+1, it must have changed on line (A.3.28) of round t ₀+1 (this is the only line that sets sb _OUT to 1). In particular, the conditional statements on lines (A.3.25) and (A.3.27) must have been satisfied, and so d was equal to 1 on line (A.3.25) of round t ₀+1. Since d is reset to zero during Stage 1 of every round (A.3.26), it must be that d was switched from 0 to 1 on line (A.4.40) of round t ₀ (this is the only place d is set to one). Thus, we have that Send Packet was called on line (A.3.17) of round t ₀. We are now back in Case 1 above (but for round t ₀ instead of t), and thus H _FP was set to a value of at least 1 on line (A.4.38) of round t ₀. It remains to argue that H _FP does not decrease in value between round t ₀ and line (A.3.17) of round t. But H _FP can only change value on lines (A.3.33), (A.3.35), and (A.4.38). For round t ₀, the former two of these lines have both passed when the latter is called (setting H _FP ≥1 as in Case 1). Meanwhile, between t ₀+1 and t, we know that (A.3.33) and (A.4.38) cannot be reached, as this would imply the value of sb _OUT is zero sometime after t ₀+1, contradicting the choice of t ₀+1. The only other place H _FP can change is (A.3.35), which can only increase H _FP . Thus in any case, ⊥≠H _FP ≥1 when Send Packet is called on (A.3.17) of round t.

The proof of the first statement follows from the proof given in Case 2 above. □

Definition B.8

We will say that an outgoing buffer gets confirmation of receipt for a packet p that it sent across its adjacent edge whenever line (A.3.30) (alternatively line (C.4.46) for the Mal-Slide protocol of Sect. 5) is reached and satisfied and the packet subsequently deleted (via “OUT[H _FP ]=⊥ on (A.3.32)) (respectively (C.4.50)) is (a copy of) p.

Claim B.9

Let B, p, and t denote either:

• B is the sender, p is any packet the sender is currently storing, and t=0 is the outset of a transmission, OR

• B is an internal node and p is (an instance of) a packet that is accepted by node B in round t (using the definition of “accepted” from Definition 4.4)

Then:

1. 1.

   Let t′ be the first round after ^{Footnote 37} t in which B attempts to send (a copy of) this packet across any outgoing edge. Then the corresponding outgoing buffer OUT of B will necessarily have normal status at the start of Stage 2 of t′.

2. 2.

   If B fails to get confirmation of receipt for the packet in round t+1 (i.e. either RR is not received on (A.3.06) of round t′+1, or it is received but RR<t′^{Footnote 38}), then OUT enters problem status as on (A.3.28) of round t′+1. OUT will remain in problem status until the end of the transmission or until the round in which it gets confirmation of receipt (i.e. until RR is received as on (A.3.06) with RR≥t′).

3. 3.

   From the time p is first flagged as on (A.4.38) of round t′ through the time B does get confirmation of receipt (or through the end of the transmission, whichever comes first), OUT will not have any other flagged packets, i.e. \(\tilde{p}=\mathsf{OUT}[H_{\mathit{FP}}] = p\) and FR=t′.

Proof

We prove Statement 1 by contradiction. Let t′ denote the first round after t in which B attempts to send (a copy of) p across an edge E(B,C), i.e. t′ is the first round after t that Send Packet is called by B’s outgoing buffer OUT such that the \(\tilde{p}\) that appears on line (A.4.38) of that round corresponds to p. For the sake of contradiction, assume that sb _OUT =1 at the start of Stage 2 of round t′. Since sb _OUT cannot change between the start of Stage 2 and the time that Create Flagged Packet is called on line (A.3.15), we must have that sb _OUT =1 on line (A.4.37) of round t′, and hence (A.4.38) is not reached that round. In particular, when Send Packet is called on line (A.3.17) (as it must be by the fact that p was sent during round t′), the packet \(\tilde{p}\) that is sent (which is p) was set in some previous round. Let \(\widetilde{\mathtt{t}}\) denote the most recent round for which \(\tilde{p}\) was set to p as on (A.4.38) (this is the only line which sets \(\tilde{p}\)). Then by assumption \(\widetilde{\mathtt{t}} < \mathtt {t}'\), and OUT had normal status at the start of Stage 2 of round \(\widetilde{\mathtt{t}}\) (in order for (A.4.38) to be reached). Since OUT had normal status at the start of Stage 2 of round \(\widetilde{\mathtt{t}}\), but by assumption OUT had problem status at the start of Stage 2 of round t′, let \(\widehat{\mathtt{t}}\) denote the first round such that \(\widetilde{\mathtt{t}} < \widehat{\mathtt{t}} \leq \mathtt{t}'\) and such that OUT had problem status at the start of Stage 2 of \(\widehat{\mathtt{t}}\). Since the only place OUT switches status from normal to problem is on (A.3.28), this line must have been reached in round \(\widehat{\mathtt{t}}\). In particular, this implies that (A.3.25) was satisfied in round \(\widehat{\mathtt{t}}\), which in turn implies that Send Packet was called in round \(\widehat{\mathtt{t}}-1\) (since d is reset to zero at the end of Stage 1 of every round as on (A.3.26)). But this is a contradiction, since \(\widetilde{\mathtt{t}} \leq\widehat {\mathtt{t}}-1 < \mathtt{t}'\), and so \(p=\tilde{p}\) was sent in a round before t′, contradicting the choice of t′.

For Statement 2, since B sent p in round t′ and OUT had normal status at the start of Stage 2 of this round, we have that H _OUT >H _IN on line (A.3.16) of round t′ (so that Send Packet could be called). Since sb _OUT ,H _OUT , and H _IN cannot change between (A.3.15) and (A.3.17) of any round, (A.4.37) will be true, and thus FR is set to t′ on (A.4.38) of round t′. Also, d=1 after the call to Send Packet of round t′ (A.4.40). Notice that neither FR nor d can change value between the call to Create Flagged Packet in round t′ and the call to Reset Outgoing Variables in the following round. Therefore, if B does not receive RR or if RR<FR=t′ when Reset Outgoing Variables is called in round t′+1, then (A.3.25) and (A.3.27) will be satisfied, and hence OUT will enter problem status on (A.3.28) of round t′+1. That OUT remains in problem status until the end of the transmission or until the round in which RR is received on (A.3.06) with RR≥t′ now follows from the following subclaim. (Warning: the following subclaim switches notation. In particular, to apply the subclaim here, replace (t,t ₀) of the subclaim with (t′+1,t′).)

Subclaim.   Suppose that at the start of Stage 2 of some round t, an outgoing buffer OUT has problem status and ⊥≠FR=t ₀. Then OUT will remain in problem status until the end of the transmission or until the round in which RR is received on (A.3.06) with RR≥t ₀.

Proof.  OUT will certainly return to normal status by the end of the transmission (A.4.62), in which case there is nothing to show. So suppose that t′>t is such that OUT first returns to normal status (in the same transmission as t) as on (A.3.33) of round t′. In particular, lines (A.3.29) and (A.3.30) were both satisfied, so OUT must have received RR on (A.3.06) earlier in round t′, with RR≥FR. If the value of FR on line (A.3.30) equals t ₀, then the proof is complete. We show by contradiction that this must be the case.

Assume for the sake of contradiction that FR≠t ₀ on line (A.3.30) of round t′. Since FR was equal to t ₀ at the start of Stage 2 of round t by hypothesis, FR must have changed at some point between Stage 2 of round t and round t′. Notice that between these rounds, FR can only change values on lines (A.3.33) and (A.4.38). Let t″ denote the first round between t and t′ such that one of these two lines is reached. Note that t″>t, since (A.3.33) already passed by the start of Stage 2 (which is when the subclaim asserts FR=t ₀), and (A.4.38) cannot be reached in round t since OUT has problem status when (A.4.37) of round t is reached (by hypothesis).

• Suppose FR is first changed from FR=t ₀ on (A.3.33) of round t″. First note that because (A.3.33) is the first time FR changes its value from t ₀, it must be the case that FR was still equal to t ₀ on (A.3.30) earlier in round t″. Also, since (A.3.33) is reached in round t″, OUT returns to normal status. Since t′ was defined to be the first round after t for which this happens, we must have that t″≥t′. But by construction t″≤t′, so we must have that t″=t′. However, this is a contradiction, because our assumption is that FR≠t ₀ on line (A.3.30) of round t′=t″, but as noted in the second sentence of this paragraph, we are in the case that FR=t ₀ on line (A.3.30) of round t″.

• Suppose FR is first changed from FR=t ₀ on (A.4.38) of round t″. Then (A.4.37) must have been satisfied, and thus OUT had normal status when Create Flagged Packet was called in round t″. Since OUT had problem status at the start of Stage 2 of round t (by hypothesis), the status must have switched to normal at some point between t and t″, which can only happen on (A.3.33). But if (A.3.33) is reached, then FR will be set to ⊥ on this line, which contradicts the fact that FR was first changed from FR=t ₀ on (A.4.38) of round t″.

This completes the proof of the subclaim. □

For the third Statement, first note that OUT[H _FP ]=p as of line (A.4.38) of round t′. This is the case since sb _OUT =0 on line (A.3.12) (by Statement 1 of this claim), and then the fact that Send Packet is called in round t′ means H _OUT >H _IN on (A.3.16), and therefore since none of these values change between (A.3.12) and (A.3.16), (A.4.37) will be satisfied in round t′. Therefore, we will track all changes to OUT and H _FP from Stage 2 of round t′ through the time p is deleted from OUT as on (A.3.32–33) of some later round,^{Footnote 39} and show that none of these changes will alter the fact that OUT[H _FP ]=p. Notice that (before the end of the transmission) H _FP only changes value on lines (A.3.33), (A.3.35), and (A.4.38); while OUT only changes values on lines (A.3.32), (A.3.35), and (A.5.89–90). Clearly the changes to each value on (A.3.35) will preserve OUT[H _FP ]=p, so it is enough to check the other changes. Notice that (A.3.32) is reached if and only if (A.3.33) is reached, which by Statement 2 of this claim does not happen until OUT gets confirmation of receipt that p was successfully received by B’s neighbor, and therefore these changes also do not threaten the validity of Statement 3. The change to H _FP as on (A.4.38) can only occur if (A.4.37) is satisfied, i.e. only if OUT has normal status, and thus again Statement 2 of this claim says this cannot happen until OUT gets confirmation of receipt that p was successfully received by B’s neighbor. Finally, lines (A.5.89–90) will preserve OUT[H _FP ]=p by Statement 11 of Lemma B.1.

That FR=t′ from (A.4.38) of t′ through the time B gets confirmation of receipt for p was proven in the subclaim above. Also, \(\tilde{p}\) can only change on (A.3.33) or (A.4.38), which we already proved (in the proof of the subclaim above) are not reached. □

Claim B.10

At any time, an outgoing buffer has at most one flagged packet.

Proof

This follows immediately from Statement 3 of Claim B.9. □

Claim B.11

For any outgoing buffer OUT, if at any time its Flagged Round value FR is equal to t, then OUT necessarily called Send Packet on line (A.3.17) of round t.

Proof

Suppose that at some point in time, FR is set to t. Notice that the only place FR assumes non-⊥ values is on (A.4.38), and therefore line (A.4.37) must have been satisfied in round t. Since the values for sb _OUT ,H _OUT , and H _IN cannot change between lines (A.3.15) and (A.3.16), the statement on (A.3.16) will also be satisfied in round t, and consequently Send Packet will be reached in t. □

Lemma B.12

Suppose that sb _OUT =1 when line (A.4.47) is reached in round t on an edge linking buffers OUT and IN. Further suppose that IN does receive the communication (p,FR) from OUT on line (A.4.43) of t. Let t ₀ denote the round described by FR, let h denote the number of packets in OUT in round t ₀, and let h′ denote the height of IN at the start of round t ₀. Then the following are true:

1. 1.

   t ₀ is well-defined (i.e. t ₀≠⊥ and t ₀≤t).

2. 2.

   h>h′.

3. 3.

   OUT sent p to IN on line (A.4.41) of round t ₀. Furthermore, the height of p in OUT when it is sent on line (A.4.41) of round t is greater than or equal to h.

4. 4.

   If the condition statement on line (A.4.51) of round t is satisfied, then the value of H _GP when this line is entered, which corresponds to the height in IN that p assumes when it is inserted on (A.4.53), satisfies ⊥≠H _GP ≤h′+1≤2n.

5. 5.

   If the condition statement on line (A.4.51) of round t is satisfied, then H _IN was less than 2n at the start of all rounds between t ₀ and t.

Proof of Lemma B.12

We make a series of subclaims to prove the five statements of the lemma.

Subclaim 1

The value of FR that is sent on (A.4.41) of round t is not ⊥.

Proof

Since (A.4.41) is reached, Send Packet was called on (A.3.17). By Statement 2 of Claim B.7, we have that H _FP ≥1 when Send Packet is called, and in particular H _FP ≠⊥ on line (A.3.17). Since H _FP cannot change between (A.3.17) and (A.4.41), we have that H _FP ≠⊥ on (A.4.41), and hence FR≠⊥ on this line (Claim B.6). □

Subclaim 2

t ₀ is well-defined (i.e. ⊥≠t ₀≤t).

Proof

By the definition of t ₀ and Subclaim 1, t ₀≠⊥. Also, by looking at the three places that FR changes values ((A.3.33), (A.4.38), and (A.4.62)), it is clear that when FR≠⊥, FR will always be less than or equal to the current round index. □

Subclaim 3

t>t ₀.

Proof

By Subclaim 2, we only have to show t≠t ₀. For the sake of contradiction, suppose t=t ₀. By hypothesis, sb _OUT =1 when line (A.4.47) of round t=t ₀ is reached. Notice that sb _OUT had been reset to 0 on (A.3.10) of round t=t ₀, so the only way it can be ‘1’ on (A.4.47) later that round is if it is set to one on (A.3.11). This can only happen if H _OUT =⊥ or FR>RR. Since (A.4.47) is reached, (A.4.44) must have failed, and since H _OUT does not change values between the time it is received on (A.3.11) and (A.4.44), we have that H _OUT ≠⊥ on (A.3.11). Therefore, we must have that FR>RR on (A.3.11) of round t=t ₀.

Notice the value for FR here comes from the value sent by OUT on (A.3.05), and this happens before line (A.4.38) has been reached in round t=t ₀. Therefore, the value of FR received on (A.3.11) obeys FR<t=t ₀ (as noted above, FR can never attain a value bigger than the current round). Since RR<FR, line (A.3.30) cannot have been satisfied since the time FR was set to its current value (within a transmission, the values RR assumes are strictly increasing, see (A.4.53)). Therefore, we may apply Claim B.11 and Statement 2 of Claim B.9 to argue that FR will not be changed on (A.4.38) of round t=t ₀ (since OUT will have problem status), and consequently FR will still be strictly smaller than t=t ₀ when line (A.4.41) is reached of round t ₀. This contradicts the definition of t ₀ as the value received on line (A.4.43) of round t. □

Subclaim 4

OUT had normal status at the start of Stage 2 of round t ₀. For every round between Stage 2 of t ₀+1 through t−1, OUT had problem status and FR=t ₀.

Proof

By definition of t ₀, it equals the value of FR that was received in round t on line (A.4.43), which in turn corresponds to the value of FR that was sent on line (A.4.41). Tracing the values of FR backwards, we see that the only time/place FR is set to a non-⊥ value (as we know it has by Subclaim 1) is on line (A.4.38), and this must have happened in round t ₀ since FR=t ₀ by definition of t ₀. Therefore, in round t ₀, line (A.4.38) must have been reached when Create Flagged Packet was called on line (A.3.15); so in particular sb _OUT must have been zero on line (A.4.37) to have entered the conditional statement. Since sb _OUT cannot change between the start of Stage 2 and line (A.3.15) (where Create Flagged Packet is called), it must have been zero at the start of Stage 2. This proves the first part of the subclaim. Now suppose there is a round t′ between Stage 2 of t ₀+1 and t−1 such that sb _OUT =0 at any time in that round (without loss of generality, let t′ be the first such round). Since sb _OUT can only switch to zero on (A.3.33) inside the call to Reset Outgoing Variables, it must be that this line is reached in t′, and hence FR is also set to ⊥ on this line. Since FR is only assigned non-⊥ values on (A.4.38), FR can only assume values at least t′>t ₀ after this point. Thus, FR will not ever be able to return to the value of t ₀, contradicting the fact that FR=t ₀ during round t. Finally, if FR were to change values at any point during rounds t ₀+1 and t−1, then we again would have that FR can only assume values at least t′>t ₀ after this point, and thus FR will not ever be able to return to the value of t ₀, contradicting the fact that FR=t ₀ during round t. □

Subclaim 5

OUT attempted to send p in round t ₀.

Proof

By definition, t ₀ denotes the value of FR during round t. Since FR can only be set to t ₀ on (A.4.38) of round t ₀, this line must have been reached in t ₀. In particular, line (A.4.37) was satisfied during the call to Create Flagged Packet of round t ₀, and hence sb=0 and H>H _IN at that time. Therefore, (A.3.16) will be satisfied when it is reached in round t ₀, which implies Send Packet will be called on the following line. The fact that it was the same packet p that was sent in t ₀ as in t follows from Statement 3 of Claim B.9. □

Subclaim 6

The height of p in OUT when it is sent in round t is greater than or equal to h.

Proof

Subclaim 5 stated that OUT attempted to send p in round t ₀, and Subclaim 4 stated that OUT had normal status at the start of t ₀. Therefore, the packet which was sent in round t ₀ (which is p) was initialized inside the call to Create Flagged Packet on line (A.4.38). By observing the code there, we see that p is set to OUT[H], i.e. p has height H in round t ₀, and H _FP is set to equal H on this same line. By Statement 3 of Claim B.9, \(p = \tilde{p}\) will remain the flagged packet through the start of round t, and OUT[H _FP ]=p. By Statement 11 of Lemma B.1, H _FP will not change during any call to re-shuffle. Indeed, since Subclaim 4 ensures that line (A.4.38) is never reached from t ₀+1 through the start of t, the only place H _FP can change value is on (A.3.33) or (A.3.35). We know the former cannot happen between t ₀+1 and the start of t, since this would imply sb _OUT is reset to zero on (A.3.33) of that round, contradicting Subclaim 4. Therefore, H _FP can only change values between t ₀+1 and the start of t as on (A.3.35), which can only increase H _FP . Hence, from the time H _FP is set to equal the height of OUT in round t ₀ as on (A.4.38) (which by definition is h), H _FP can only increase through the start of round t. □

Subclaim 7

h>h′.

Proof

This follows immediately from Subclaims 4 and 5 as follows. Because OUT tried to send the packet in round t ₀ (Subclaim 5) and because OUT had normal status in this round (Subclaim 4), it must be that the conditional statement on line (A.3.16) of round t ₀ was satisfied, and in particular that the expression H>H _IN was true. Since h is defined to be the value of H as of line (A.4.38) of round t ₀ (Statement 6 of Lemma B.1), this subclaim will follow if h′ equals the value of H _IN as of line (A.4.38) of round t ₀. But this is true by Statement 5 of Lemma B.1, since the value of H _IN on line (A.3.16) comes from the value received on line (A.3.06), which in turn corresponds to the value of H _IN sent on line (A.3.09). □

Subclaim 8

If the conditional statement on line (A.4.51) is satisfied in round t, then OUT ’s attempt to send p in round t ₀ failed (i.e. IN did not store p in t ₀), and furthermore IN did not store p in any round between t ₀ and t.

Proof

We prove this by contradiction. Suppose there is some round \(\widetilde{\mathtt{t}} \in[\mathtt{t}_{0}, \mathtt{t}-1]\) in which IN stored p. This would mean that line (A.4.51) was satisfied in round \(\widetilde{\mathtt{t}}\), and in particular RR is set to \(\widetilde{\mathtt{t}} \geq\mathtt {t}_{0}\) on (A.4.53). But as already noted in the proof of Subclaim 2, for the remainder of the transmission, FR can never assume the value of a round before t ₀. Similarly, once RR changes to \(\widetilde{\mathtt{t}} \geq\mathtt {t}_{0}\) on (A.4.53) of round \(\widetilde{\mathtt {t}}\), it can never assume a smaller (non-⊥) value for the rest of the transmission (RR can only change to a non-⊥ value on line (A.4.53)). But this contradicts the fact that RR<FR on (A.4.51) of round t, since by definition of t ₀, FR=t ₀ on (A.4.51) of round t. □

Subclaim 9

If the conditional statement on line (A.4.51) is satisfied in round t, then RR<t ₀ between the start of t ₀ through line (A.4.51) of round t. In particular, lines (A.4.47) and (A.4.51) will be satisfied for any round between t ₀ and t for which they are reached.

Proof

RR is set to −1 at the start of any transmission ((A.1.31) and (A.4.64)). Since the only other place RR changes value is (A.4.53), it is always the case that the value of RR is less than or equal to the index of the current round. Thus, RR can only assume a value greater than (or equal to) t ₀ in a round after (or during) t ₀. But this would mean there was some round between t ₀ and t−1 (inclusive) such that (A.4.53) was reached, which contradicts Subclaim 8. The fact that (A.4.51) will be satisfied whenever it is reached now follows immediately from Subclaim 4, since in order to reach (A.4.51), line (A.4.48) must have failed, which means the communication on line (A.4.43) was received. The fact that (A.4.47) will be satisfied whenever it is reached follows from the fact that sb _OUT will always be set to one on (A.3.11) of each round between t ₀ and t (the first part of this subclaim says RR<t ₀, and Subclaim 4 says that if FR is received on (A.3.11), then FR=t ₀). □

Subclaim 10

If the conditional statement on line (A.4.51) is satisfied in round t, then there was no round between t ₀+1 and t−1 (inclusive) in which IN received both H _OUT and p.

Proof

Suppose for the sake of contradiction that there is such a round, \(\widetilde{\mathtt{t}}\). Notice that line (A.4.51) of round \(\widetilde{\mathtt{t}}\) will necessarily be reached (since the conditional statement of line (A.4.44) will fail by assumption, (A.4.47) will be satisfied by Subclaim 9, and (A.4.48) will fail by assumption). However, line (A.4.53) cannot be reached in round \(\widetilde{\mathtt {t}}\) (Subclaim 8 above), and therefore the conditional statement on line (A.4.51) must fail. This contradicts Subclaim 9. □

Subclaim 11

If the conditional statement on line (A.4.51) is satisfied in round t, then IN was in problem status at the end of round t ₀, and remained in problem status until (at least) line (A.4.53) of round t.

Proof

We first show that sb _IN will be set to one on line (A.4.45) or (A.4.49) of round t ₀. To see this, we note that if (A.4.44) fails in round t ₀, then necessarily (A.4.47) and (A.4.48) will both be satisfied. After all, (A.4.47) is satisfied (Subclaim 9), and then (A.4.48) must be true (by Subclaim 10, since we are assuming (A.4.49) failed). Thus, sb _IN will be set to one on line (A.4.45) or (A.4.49) of round t ₀, as claimed. Now for every round between t ₀+1 and t, Subclaims 9 and 10 imply that either the conditional statement on line (A.4.44) will be satisfied, or the conditional statements on lines (A.4.47) and (A.4.48) will both be satisfied, and hence sb _IN can never be reset to zero since lines (A.4.53), (A.4.55), and (A.4.57) will never be reached. □

Subclaim 12

If the conditional statement on line (A.4.51) is satisfied in round t, then between the end of round t ₀ and the time Receive Packet is called in round t, we have that H _GP ≠⊥ and H _GP ≤h′+1≤2n.

Proof

As in the proof of Subclaim 11, either line (A.4.46) or (A.4.50) will be reached in round t ₀ (since either line (A.4.45) or (A.4.49) is reached). The value of H _IN at the start of round t ₀ is h′ by definition. Since h′<h≤2n (the first inequality is Subclaim 7, the second is Statements 6 and 9 of Lemma B.1), and since H _IN cannot change value between the start of t ₀ and the time Receive Packet is called later in t ₀, we have that the value of H _IN <2n when either line (A.4.46) or (A.4.50) is reached. Therefore, these lines guarantee that ⊥≠H _GP ≤h′+1≤2n after these lines (either because H _GP satisfied this before these lines, or it was set to H _IN +1 on these lines). After this, there are five places H _GP can change its value: (A.4.46), (A.4.50), (A.4.53), (A.4.55), and (A.4.57). As in the proof of Subclaim 11, lines (A.4.53), (A.4.55), and (A.4.57) will not be reached at any point between t ₀ and t. The other two lines that change H _GP can only decrease it (but they cannot set H _GP to ⊥). □

Subclaim 13

If the condition statement on line (A.4.51) of round t is satisfied, then the value of H _GP when this line is entered, which corresponds to the height in IN that p assumes when it is inserted on (A.4.53), satisfies H _GP ≠⊥ and H _GP ≤h′+1≤2n.

Proof

This follows immediately from Subclaim 12 since p is inserted into IN at height H _GP (A.4.53). □

Subclaim 14

If the condition statement on line (A.4.51) of round t is satisfied, then H _IN was less than 2n at the start of all rounds between t ₀ and t.

Proof

Subclaim 12 implies that h′<2n (so H _IN had height strictly smaller than 2n at the start of round t ₀). Searching through the pseudo-code, we see that H _IN is only modified on lines (A.4.53), and during Re-Shuffling (A.5.91–92). Between rounds t ₀ and t−1, line (A.4.53) is never reached (Subclaim 8), and hence all changes to H _IN must come from Re-Shuffling. But because H _IN was less than 2n when it entered the Re-Shuffle phase in round t ₀, Statement 13 of Lemma B.1 guarantees that H _IN will still be less than 2n at the start of round t. □

All statements of the lemma have now been proven.  □

Claim B.13

Every packet is inserted into one of the sender’s outgoing buffers at some initial height. When (a copy of) the packet goes between any two buffers B ₁≠B ₂ (either across an edge or locally during re-shuffling), its height in B ₂ is less than or equal to the height it had in B ₁. If B ₁=B ₂, the statement remains true EXCEPT for on line (A.3.35).

Proof

We separate the proof into cases, based on the nature of the packet movement. The only times packets are accepted by a new buffer or re-shuffled within the same buffer are lines (A.3.32), (A.3.35), (A.4.53), (A.4.55), (A.4.57), (A.4.61), (A.4.64), (A.5.89–90), and (A.5.101–102). Of these, (A.3.35) is excluded from the claim, and the packet movement on lines (A.3.32), (A.4.55), (A.4.57), (A.4.61), (A.4.64), and (A.5.101–102) are all clearly strictly downwards. It remains to consider lines (A.4.53) and (A.5.89–90).

Case 1: The packet moved during Re-Shuffling as on (A.5.89–90).:

By investigating the code on these lines, we must show that m+1≤M. This was certainly true as of line (A.5.74), but we need to make sure this did not change when Adjust Heights was called. The changes made to M and m on (A.5.83) and (A.5.85) will only serve to help the inequality m+1≤M, so we need only argue the cases for when (A.5.81) and/or (A.5.87) is reached. Notice that if either line is reached, by (A.5.74) we must have (before adjusting M and m) that M−m≥2, and therefore modifying only M=M−1 or m=m+1 will not threaten the inequality m+1≤M. It remains to argue that both (A.5.81) and (A.5.87) cannot happen simultaneously (i.e. cannot both happen within the same call to Re-Shuffle). If both of these were to happen, then it must be that during this call to Re-Shuffle, there was an outgoing buffer B ₁ that had height 2 or more higher than an incoming buffer B ₂ (see lines (A.5.72–74) and (A.5.80) and (A.5.86)). We argue that this cannot ever happen. By Claim B.3, at the end of the previous round, we had that the height of B ₁ was at most one bigger than the height of B ₂. During routing, B ₂ can only get bigger (it is an incoming buffer) and B ₁ can only get smaller (it is an outgoing buffer) ((A.4.53) and (A.3.33) are the only places these heights change). Therefore, after Routing but before any Re-Shuffling, we have again that the height of B ₁ was at most one bigger than the height of B ₂. Therefore, in order for B ₁ to get at least 2 bigger than B ₂, either a packet must be shuffled into B ₁, or a packet must be shuffled out of B ₂, and this must happen when B ₁ is already one bigger than B ₂. But analyzing (A.5.72) and (A.5.73) shows that this can never happen.

Case 2: The packet moved during Routing as on (A.4.53).:

In order to reach (A.4.53), the conditional statements on lines (A.4.47) and (A.4.51) must be satisfied and the statement on (A.4.48) must fail; so p≠⊥, RR<FR, and either sb _OUT =1 or H _OUT >H (or both). We investigate each case separately:

Case A: sb _OUT =1 on line (A.4.47).:

Then Statements 2–4 of Lemma B.12 imply that the height of the packet in B ₁ is greater than or equal to the height it will be stored into in B ₂, as desired.

Case B: sb _OUT =0 and H _OUT >H _IN on line (A.4.47).:

For notational convenience, denote the current round (when the hypotheses of Case B hold) by t. First note that Statements 1 and 2 of Lemma B.1 imply that the height the packet assumes in B ₂ (H _GP ) is less than or equal to H _IN +1. Meanwhile, since sb _OUT =0 (it is set on (A.3.11) of round t), the value received for H _OUT on (A.3.11) is not ⊥, and the value for FR received on (A.3.11) is either ⊥ or satisfies FR≤RR. Notice that the case FR≤RR is not possible, since then (A.4.53) would not be reached ((A.4.51) would fail). Therefore, FR=⊥ but H _OUT ≠⊥, and so B ₂ received the communication sent by B ₁ on (A.3.05) of round t, which had the first of the two possible forms. In particular, H _FP =⊥ at the outset of t, and since H _FP cannot change between the start of a round and line (A.4.38) of the previous round, we must have that (A.4.37) failed in round t−1. By this fact and Claim B.6, B ₁ had normal status when (A.3.16) was reached in round t−1, and this will not be able to change in the call to Reset Outgoing Variables of round t because d=0 (A.3.25) (since d is reset to zero every round on (A.3.26), it can only have non-zero values between line (A.4.40) of one round and line (A.3.26) of the following round IF a packet was sent the earlier round. However, as already noted this did not happen, as the fact that OUT had normal status and yet (A.4.37) failed in round t−1 implies that (A.3.16) will also fail in round t−1). Therefore, B ₁ has normal status when Create Flagged Packet is called in round t, and in particular, H _FP is set to H _OUT on (A.4.38), i.e. the flagged packet to be transferred during t has height H _OUT in B ₁.^{Footnote 40} Putting this all together, the packet has height H _OUT in B ₁ and assumes height H _GP in B ₂. But as argued above, H _OUT ≥H _IN +1≥H _GP , as desired.  □

Claim B.14

Before End of Transmission Adjustments is called in any transmission  T (A.4.58–61), any packet that was inserted into the network during transmission T is either in some buffer (perhaps as a flagged packet) or has been received by R.

Proof

As packets travel between nodes, the sending node maintains a copy of the packet until it has obtained verification from the receiving node that the packet was accepted. This way, packets that are lost due to edge failure are backed-up. This is the high-level idea of why the claim is true, we now go through the details.

First notice that the statement only concerns packets corresponding to the current codeword transmission, and hence packets deleted as on (A.4.61) do not threaten the validity of the claim. We consider a specific packet p that has been inserted into the network and show that p is never removed from a buffer B until another buffer B′ has taken p from B. We do this by considering every line of code that a buffer could possible remove p, and argue that whenever this happens, p has necessarily been accepted from B by some other buffer B′. Notice that the only lines that a buffer could possibly remove p (before line (A.4.61) of T is reached) are: (A.3.32), (A.4.53), and (A.5.89–90).

Line (A.4.53)

This line is handled by Lemma B.1, Statements 1 and 2 (see also (A.4.52)), which say that whenever a slot of an incoming buffer is filled as on line (A.4.53), it fills an empty slot, and therefore cannot correspond to removing (overwriting) p.

Lines (A.5.89–90)

These lines are handled by Lemma B.1, Statement 10.

Line (A.3.32)

This is the interesting case, where p is removed from an outgoing buffer after a packet transfer. We must show that any time p is removed here, it has been accepted by some incoming buffer B′. For notation, we will let t denote the round that p is deleted from B (i.e. when line (A.3.32) is reached), and t ₀ denote the round that B first tried to send the packet to B′ as on (A.4.41). By Statement 3 of Claim B.9, t ₀ is the round that \(\tilde{p}\) was most recently set to p as on line (A.4.38) (note that t ₀≤t). Since line (A.3.32) was reached in round t, the conditional statements on lines (A.3.29) and (A.3.30) were satisfied, and so ⊥≠RR≥FR≠⊥ when those lines were reached. By Statement 3 of Claim B.9, FR will equal t ₀ when (A.3.30) is satisfied. Since in any round t′, the only non-⊥ value that RR can ever be set to is t′ (A.4.53), and since RR≥t ₀=FR (A.3.30), it must be that (A.4.53) was reached in some round t′∈[t ₀,t]. In particular, B′ stored a packet as on (A.4.53) of round t′, which by Statement 3 of Claim B.9 was necessarily p.  □

Claim B.15

Not counting flagged packets, there is at most one copy of any packet in the network at any time (not including packets in the sender or receiver’s buffers). Looking at all copies (flagged and un-flagged) of any given packet present in the network at any time, at most one copy of that packet will ever be accepted (as in Definition 4.4) by another node.

Proof

For any packet p, let # _p denote the copies of p (both flagged and not) present in the network (in an internal node’s buffer) at a given time. We begin the proof via a sequence of observations:

Observation 1

The only time # _p can ever increase is on line (A.4.53).

Proof

The only way for # _p to increase is if (a copy of) p is stored by a new buffer. Looking at the pseudo-code, the only place a buffer slot can be assigned a new copy of p is on lines (A.3.32), (A.3.35), (A.4.53), (A.4.55), (A.4.57), (A.4.61), (A.4.64), and (A.5.89). Of these, only (A.4.53) and (A.5.89) could possibly increase # _p , as the others simply shift packets within a buffer and/or delete packets. In the latter case, # _p does not change by Statement 10 of Lemma B.1. □

Observation 2

Suppose A (including A=S) first sends a (copy of a) packet p to B as on (A.4.41) of round t ₀. Then:

1. (a)

   The copy of p in A’s outgoing buffer along E(A,B) (for which there was a copy made and sent on (A.4.41) of round t ₀) will never be transferred to any of A’s other buffers.

2. (b)

   The copy of p will remain in A’s outgoing buffer along E(A,B) as a flagged packet until it is deleted either when A gets confirmation of receipt (see Definition B.8) in some round t≥t ₀ (A.3.32), or at the end of the transmission as on (A.4.61). In the latter case, define t:=3D (the last round of the transmission) for Statement (c) below.

3. (c)

   Between t ₀ and line (A.3.07) of round t, B will accept (a copy of) p from A as on (A.4.53) at most once. Furthermore, the copy of p in A’s buffer cannot move to any other buffer or generate any other copies other than the one (possibly) received by B as on (A.4.53).

Proof

Statement (a) follows from Statement 3 of Claim B.9 and Statement 11 of Lemma B.1, together with the fact that lines (A.3.32) and (A.4.61) imply that the relevant copy of A will be deleted when it does get confirmation of receipt as in Definition B.8 (or the end of the transmission). By Statement 3 of Claim B.9, this copy of p will be (the unique) flagged packet in A’s outgoing buffer to B until confirmation of receipt (or the end of the transmission), which proves Statement (b). For Statement (c), suppose that B accepts a copy of p as on (A.4.53) during some round t′∈[t ₀,t]. Then RR will be set to t′ on (A.4.53) of round t′, and RR cannot obtain a smaller index until the next transmission (A.4.53). By Statement 3 of Claim B.9, FR will remain equal to t ₀ from line (A.4.38) of round t ₀ through the time (A.3.33) of round t is reached. Therefore, between t′≥t ₀ and line (A.3.33) of round t, we have that FR=t ₀≤t′≤RR, and hence line (A.4.51) can never be satisfied during these times, which implies (A.4.53) can never be reached again after t′. This proves the first part of Statement (c). The second part follows by looking at all possible places (copies of) packets can move or be created: (A.3.32), (A.3.35), (A.4.53), (A.4.55), (A.4.57), (A.4.61), (A.4.64), and (A.5.89–90). Of these, only (A.4.53) and (A.5.89–90) threaten to move p or create a new copy of p. However, the first part of Observation 2(c) says that (A.4.53) can happen at most once (and is accounted for), while Statement 11 of Lemma B.1 rules out the case that the packet is re-shuffled as on (A.5.89–90). □

Observation 3

No packet will ever be inserted (see Definition 4.5) into the network more than once. In particular, for any packet p, # _p =0 until the sender inserts it (i.e. some node accepts the packet from the sender as on (A.4.53)), at which point # _p =1. After this point, the only way # _p can become larger than one is if (A.4.53) is reached, where neither the sending node nor the receiving node is S or R.

Proof

Since the packets of S are distributed to his outgoing buffers before being inserted into the network (A.2.38), (A.4.66), and (A.4.68–70), and since S never receives a packet he has already inserted (S has no incoming edges (A.3.18) nor shuffles packets between buffers ((A.3.22) and (A.5.95–96)), a given packet p can only be inserted along a single edge adjacent to the sender. The fact the sender can insert at most one (copy of a) packet p along an adjacent edge now follows from Observation 2 above for A=S. This proves the first part of Observation 3.

By Observation 1, the only place # _p can increase is on (A.4.53). Whenever this line is reached, the copy stored comes from the one received on (A.4.43), which in turn was sent by another node on (A.4.41). The copy sent on (A.4.41) in turn can only be set on (A.4.38) (perhaps in an earlier round), so in particular a copy of the packet must have already existed in an outgoing buffer of the sending node. This proves that when # _p goes from zero to one, it can only happen when a packet is inserted for the first time by the sender. The rest of Observation 3 now follows from Observation 1, the first part of Observation 3, the fact that copies reaching R do not increase # _p (by definition of # _p ), and the fact R never sends a copy of a packet (A.3.13) and S never accepts packets (A.3.18). □

Define a copy of a packet p in the network to be dead if that copy will never leave the buffer it is currently in, nor will it ever generate any new copies. A copy of a packet that is not dead will be alive.

Observation 4

If a (copy of a) packet is ever flagged and dead, it will forever remain both flagged and dead, until it is deleted.

Proof

By definition of being “dead,” once a (copy of a) packet becomes dead it can never become alive again. Also, copies of a packet that are flagged remain flagged until they are deleted by Observation 2(b). □

Claim B.15 now follows immediately from the following subclaim:

Subclaim

Fix any packet p that is ever inserted into the network. Then at any time, there is at most one alive copy of p in the network at any time. Also at any time, if there is one alive copy of p, then all dead copies of p are flagged packets. If there are no alive copies, then there is at most one dead copy of p that is not a flagged packet.

Proof

Before p is inserted into the network, # _p =0, and there is nothing to show. Suppose p is inserted into the network in round t ₀, so that # _p =1 by the end of t ₀ (Observation 3). Since # _p =1, the validity of the subclaim is not threatened. Also, if this packet is dead, then the proof is complete, as by Observation 3 and the definition of deadness, no other (copies) of p will ever be created, and hence the subclaim will forever be true for p. So suppose p is alive when it is inserted. We will show that a (copy of an) alive packet can create at most one new (copy of a) packet, and the instant it does so, the original copy is necessarily both flagged and dead (the new copy may be either alive or dead), from which the subclaim follows from Observation 4. So suppose an alive copy of p creates a new copy (increasing # _p ) of itself in round t. Notice that the only time new copies of any packet can be created is on (A.4.53) (see e.g. proof of Observation 2). Fix notation, so that the alive copy of p was in node A’s outgoing buffer to node B, and hence it was B’s corresponding buffer that entered (A.4.53) in round t. The fact that the alive copy of p in A’s outgoing buffer is flagged and dead the instant B accepts it on (A.4.53) of round t follows immediately from Observation 2. □

 □

Lemma B.16

Suppose that in round t, B accepts (as in Definition 4.4) a packet from A. Let O _A,B denote A’s outgoing buffer along E(A,B), and let O denote the height the packet had in O _A,B when Send Packet was called in round t (A.3.17). Also let I _B,A denote B’s incoming buffer along E(A,B), and let I denote the height of I _B,A at the start of t. Then the change in non-duplicated potential caused by this packet transfer is less than or equal to:

Furthermore, after the packet transfer but before re-shuffling, I _B,A will have height I+1.

Proof

By definition, B accepts the packet in round t means that (A.4.53) was reached by B’s incoming buffer along E(A,B) in round t. Since the packet is stored at height H _GP (A.4.53), B’s non-duplicated potential will increase by H _GP due to this packet transfer (if B=R, then by definition of non-duplicated potential, packets in R do not contribute anything, so there will be no change). By Statements 1 and 2 of Lemma B.1, H _GP ≤I+1, and hence B’s increase in non-duplicated potential caused by the packet transfer is at most I+1 (or zero in the case B=R). Also, since B had height I at the start of the round, and B accepts a packet on (A.4.53) of round t, B will have I+1 packets in I when the re-shuffling phase of round t begins, which is the second statement of the lemma (since the height of I _B,A does not change from the start of t through the start of Re-Shuffling, except when I _B,A receives the packet on (A.4.53)).

Meanwhile, the packet transferred along E(A,B) in round t still has a copy in O _A,B (until A receives confirmation of receipt from B, see Definition B.8), but by definition of non-duplicated potential (see Definition 4.7), this (flagged) packet will no longer count towards non-duplicated potential the instant B accepts it as on (A.4.53) of round t. Therefore, A’s non-duplicated potential will drop by the value H _FP has when B accepts the packet on (A.4.53) (Statement 3 of Claim B.9), which equals O since H _FP cannot change between the time Send Packet is called on (A.3.17) and the time the packet is accepted on (A.4.53). Therefore, counting only changes in non-duplicated potential due to the packet transfer, the change in potential is: −O+H _GP ≤−O+I+1 (or −O in the case B=R), as desired. □

Lemma B.17

Let \(\mathcal{C} = N_{1} N_{2} \cdots N_{l}\) be a path consisting of l nodes, such that R=N _l and \(S \notin\mathcal {C}\). Suppose that in round t, all edges E(N _i ,N _i+1), 1≤i<l are active for the entire round. Let ϕ denote the change in the network’s non-duplicated potential caused by

1. 1.

   For 1≤i<l: Packet transfers across E(N _i ,N _i+1) in round  t,

2. 2.

   For 1<i<l: Re-shuffling packets into N _i ’s outgoing buffers during t

Then if \(O_{N_{1}, N_{2}}\) denotes N ₁ ’s outgoing buffer along E(N ₁,N ₂) and O denotes its height at the start of t, we have:

• If \(O_{N_{1}, N_{2}}\) has a flagged packet that has already been accepted by N ₂ before round t, then:

  $$ \phi\leq-O + l-1. $$

  (B.2)

• Otherwise,

  $$ \phi\leq-O + l-2. $$

  (B.3)

Proof

(Induction on l).

Base Case: l=2

So \(\mathcal{C} = N_{1} R\).

Case 1: \(O_{N_{1},R}\) had a flagged packet at the start of t that had already been accepted by N ₂.:

Our aim for this case is to prove (B.2) for l=2. If O<2, then −O+l−1≥−1+2−1=0, and then (B.2) will be true by Lemma 4.11. So assume O≥2. Since E(N ₁,R) is active during t and R had already accepted the packet in some previous round \(\tilde{\mathtt{t}} < \mathtt{t}\), we see that \(\mathit{RR} \geq\tilde {\mathtt{t}}\) (A.4.53), and N ₁ will receive this value for RR in R’s stage one communication (A.3.06), (A.3.09). By Statement 3 of Claim B.9, \(\mathit{FR} \leq\tilde{\mathtt{t}} \leq \mathit{RR}\), and thus lines (A.3.29–30) will be satisfied in round t, so the flagged packet is deleted on (A.3.32–33), O gets the value O−1, and sb is set to ‘0’. When Create Flagged Packet is called on (A.3.15), a new packet will be flagged since sb=0 and H _OUT =O−1≥1>H _IN =0, with H _FP =H _OUT =O−1 and FR=t (since O≥2, there will be at least one packet left in \(O_{N_{1},R}\) of height O−1>0 by Lemma B.1). Letting I denote the height of the receiver’s incoming buffer along E(N ₁,R), we see that I=0 (Claim B.5). Therefore, H _OUT >H _IN , and so the flagged packet will be sent as on (A.3.17). Since R will receive and store this packet (since the edge is active and RR<t=FR, lines (A.4.44) and (A.4.48) will fail, while lines (A.4.47) and (A.4.51) will be satisfied), we apply Lemma B.16 to argue there will be a change in non-duplication potential that is less than or equal to −(O−1), which is (B.2) (for l=2).

Case 2: Either \(O_{N_{1},R}\) has no flagged packet at the start of t, or if so, it has not yet been accepted by R.:

Our aim for this case is to prove (B.3) for l=2. If O=0, then −O+l−2=0, and (B.3) is true by Lemma 4.11. So assume O≥1. Then necessarily a packet will be sent during round t ((A.3.16) is necessarily satisfied since by assumption E(N ₁,R) is active during t, H _OUT ≥1 by Lemma B.1 and H _IN =0 by Claim B.5). We first show that the height of the packet in \(O_{N_{1}, R}\) that will be transferred in round t (which will be the value held by H _FP when Send Packet is called in round t) is greater than or equal to O (whether or not it was flagged before round t):

• If \(O_{N_{1},R}\) did not have any flagged packets at the outset of t, then H _FP =⊥ at the start of t, and so sb=0 and FR=⊥ at the start of t by Claim B.6. Since H _FP cannot change between the call to Send Packet in the previous round and the call to Reset Outgoing Variables in the current round, Statement 2 of Claim B.7 implies no packet was sent the previous round, and hence d=0 at the start of t (d was necessarily zero as of (A.3.26) of round t−1, and as argued did not change to ‘1’ on (A.4.40) later that round). Consequently, sb will remain zero from the start of t through the time Create Flagged Packet is called in round t, and because H _OUT =O>0=I=H _IN , (A.4.38) will be reached in round t, setting H _FP to O.

• Alternatively, if \(O_{N_{1},R}\) does have a flagged packet at the outset of t, we argue that it will have height at least O when Send Packet is called in round t as follows. Let t ₀<t denote the round \(O_{N_{1},R}\) first sent (a copy of) the packet to R. We first show that N ₁ will not get confirmation of receipt from R (as in Definition B.8) for the packet at any point between rounds t ₀ and t−1 (inclusive). To see this, note that since we are Case 2, R has not accepted the flagged packet by the start of t. This means that at all times between t ₀ and the start of t, RR<t ₀.^{Footnote 41} Meanwhile, by Statement 3 of Claim B.9, FR=t ₀ and H _FP ≠⊥ at the start of t. Since these do not change values between the start of t and the time Reset Outgoing Variables is called in round t, line (A.3.34) guarantees that if H _FP <O, then line (A.3.35) will be reached, and thus in either case H _FP ≥O after the call to Reset Outgoing Variables.

Therefore, since R will necessarily receive and accept the flagged packet sent (by the same argument used in Case 1), we may apply Lemma B.16 to argue that ϕ≤−O, which is (B.3) (for l=2).