Restructured proof; should be complete now

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index b96f391f4179b97e4b457c3338814242a642d969..52ec3f098effc7dfa90b5d6c8d5c04f0985d5626 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -883,9 +883,9 @@ and $\mathsf{Dat_t}$ are exactly the same.
 \end{defn}\r
 \r
 \begin{defn}[Parent]\r
 \end{defn}\r
 \r
 \begin{defn}[Parent]\r

-A parent of a message $\mathsf{t}$ is the message $\mathsf{\mathscr{P}_t}$, \r
+A parent of a message $\mathsf{t}$ is the message $\mathsf{p_t}$, \r

 unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that \r
 unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that \r

-$\mathsf{hmac_p(t) = hmac_c(\mathscr{P}_t)}$.\r
+$\mathsf{hmac_p(t) = hmac_c(p_t)}$.\r

 \end{defn}\r
 \r
 \begin{defn}[Chain]\r
 \end{defn}\r
 \r
 \begin{defn}[Chain]\r


@@ -922,9 +922,7 @@ $\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$.
 Transitive closure set at sequence number $\mathsf{s_n}$ is a set \r
 $\mathsf{\mathscr{S}}$ of clients comprising a connected component of an \r
 undirected graph, where two clients are connected by an edge if they both \r
 Transitive closure set at sequence number $\mathsf{s_n}$ is a set \r
 $\mathsf{\mathscr{S}}$ of clients comprising a connected component of an \r
 undirected graph, where two clients are connected by an edge if they both \r

-received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t < s_n}$.\r
-%TODO: Check with Thomas whether this is $\mathsf{s_t > s_n}$ or it should be\r
-%$\mathsf{s_t < s_n}$\r
+received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > s_n}$.\r

 \end{defn}\r
 \r
 \subsubsection{Lemmas and Proofs}\r
 \end{defn}\r
 \r
 \subsubsection{Lemmas and Proofs}\r


@@ -955,7 +953,7 @@ $\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$.
 \begin{figure}[h]\r
   \centering\r
       \xymatrix{ & & L \\\r
 \begin{figure}[h]\r
   \centering\r
       \xymatrix{ & & L \\\r

-\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & p \ar[r] & \dots \ar[r] & l_n = u \\\r
+\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & m \ar[r] & \dots \ar[r] & l_n = u \\\r

 & & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\\r
 & & R\r
 \save "2,3"."2,8"*+\frm{^\}}\r
 & & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\\r
 & & R\r
 \save "2,3"."2,8"*+\frm{^\}}\r


@@ -963,7 +961,7 @@ $\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$.
 \restore\r
 \restore\r
 }\r
 \restore\r
 \restore\r
 }\r

-\caption{By Lemma 1, receiving $t$ after $u$ is impossible.}\r
+\caption{By Lemma 1, receiving both $t$ and $u$ here is impossible.}\r

 \end{figure}\r
 \r
 \begin{lem} Two messages are received without errors by a client $\mathsf{C}$; \r
 \end{figure}\r
 \r
 \begin{lem} Two messages are received without errors by a client $\mathsf{C}$; \r


@@ -986,41 +984,37 @@ not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message
 $\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist, \r
 since all clients and the server were initialized with the same state. Let \r
 $\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$; \r
 $\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist, \r
 since all clients and the server were initialized with the same state. Let \r
 $\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$; \r

-we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_m = t)}$ be \r
+we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_{|R|} = t)}$ be \r

 the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$ \r
 the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$ \r

-be the distinct portion of the path of $\mathsf{l_n = u}$.\r
+be the distinct portion of the path of $\mathsf{l_{|L|} = u}$.\r

 \r
 Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that \r
 $\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who \r
 \r
 Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that \r
 $\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who \r

-sent $\mathsf{l_1}$.\r
-\r
-We know the following three facts: \r
+sent $\mathsf{l_1}$. Because no client can send two messages with the same sequence number, and \r
+$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$.\r

 \r
 \r

-\begin{enumerate}\r
+We also know the following three facts: \r

 \r
 \r

-\item Because no client can send two messages with the same sequence number, and \r
-$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$.\r
+\begin{prop} No client sends both a message in \r
+$\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. \end{prop}\r

 \r
 \r

-\item To send a message $\mathsf{p}$ that is the parent of some other \r
+\begin{proof}\r
+To send a message $\mathsf{p}$ that is the parent of some other \r

 message, one must have received the parent of $\mathsf{p}$. Since \r
 $\mathsf{u}$ is the message with smallest sequence number received by any \r
 message, one must have received the parent of $\mathsf{p}$. Since \r
 $\mathsf{u}$ is the message with smallest sequence number received by any \r

-client that violates this lemma, no client receives both a message in $\mathsf{r}$ \r
-and a message in $\mathsf{l}$; therefore, no client sends both a message in \r
-$\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$.\r
+client that violates Lemma 1, no client receives both a message in $\mathsf{r}$ \r
+and a message in $\mathsf{l}$. \end{proof}\r

 \r
 \r

-\item Since $\mathsf{u}$ is the message with the greatest- and least- sequence \r
-number that violates this lemma, $\mathsf{C}$ does not receive any message with \r
-sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. Because the \r
-$\mathsf{s_{last}}$ that $\mathsf{C}$ stores increases at every message receipt \r
-event, $\mathsf{C}$ also does not receive any message after $\mathsf{t}$ and before \r
-$\mathsf{u}$ in real time.\r
+\begin{prop} $\mathsf{C}$ does not receive any message with \r
+sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. \end{prop}\r
+\r
+\begin{proof} If there were such a message with sequence number smaller than $\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the message with least sequence number that violates Lemma 1. \end{proof}\r

 \r
 \r

-\end{enumerate}\r

 There are two cases:\r
 \begin{itemize}\r
 There are two cases:\r
 \begin{itemize}\r

-\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then \r
-%$\mathsf{v_J(t) > v_J(q) = v_J(u)}$.\r
-$\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.\r
+\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$ \r
+is the greatest sequence number of the messages that client $\mathsf{J}$ sent in \r
+the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.\r

 \begin{itemize}\r
 \item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ \r
 between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if \r
 \begin{itemize}\r
 \item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ \r
 between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if \r


@@ -1035,57 +1029,49 @@ throws an error in the $\mathsf{CheckLastSeqN}$ subroutine.
 \end{itemize}\r
 \r
 \item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the \r
 \end{itemize}\r
 \r
 \item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the \r

-first one $\mathsf{p}$. We know that $\mathsf{s_p > s_{r_1}}$, since \r
-$\mathsf{J \neq K}$ and $\mathsf{p \neq l_1}$. Message $\mathsf{r_1}$ must be sent \r
-either before or after $\mathsf{p}$.\r
+first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since \r
+$\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent \r
+either before or after $\mathsf{m}$.\r

 \begin{itemize}\r
 \begin{itemize}\r

-\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{p}$, and then $\mathsf{r_1}$. \r
-Before sending $\mathsf{p}$, the greatest sequence number of a message that \r
+\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$. \r
+Before sending $\mathsf{m}$, the greatest sequence number of a message that \r

 $\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to \r
 $\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to \r

-$\mathsf{s_p - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, \r
+$\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, \r

 client $\mathsf{J}$ cannot then send a message with sequence number \r
 $\mathsf{s_{r_1}}$, a contradiction.\r
 client $\mathsf{J}$ cannot then send a message with sequence number \r
 $\mathsf{s_{r_1}}$, a contradiction.\r

-\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{p}$. \r
-Let $\mathsf{X = (r_1, \dots )}$ be the list of messages $\mathsf{J}$ sends \r
-starting before $\mathsf{r_1}$ and ending before $p$.\r
+\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$. \r
+Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends \r
+starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence number $\mathsf{s_p = s_q + 1}$.\r

 \begin{itemize}\r
 \begin{itemize}\r

-\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Let $\mathsf{s_{w_J}}$ \r
-be the greatest sequence number of the messages that client $\mathsf{J}$ sent in \r
-the path of message $\mathsf{w}$. In this case, before sending $\mathsf{p}$, \r
+\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$, \r

 $\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would \r
 be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with \r
 contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and \r
 $\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would \r
 be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with \r
 contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and \r

-$\mathsf{p}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, \r
-when preparing to send $\mathsf{p}$, $\mathsf{J}$ would have received an update of its \r
+$\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, \r
+when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its \r

 own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before \r
 sending $\mathsf{p}$, because its own latest sequence number decreases.\r
 own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before \r
 sending $\mathsf{p}$, because its own latest sequence number decreases.\r

-\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{p}$ \r
-the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$. Note that \r
-$\mathsf{u}$ is the message with least sequence number that violates this lemma, and \r
-therefore the first one that $\mathsf{C}$ receives after $\mathsf{t}$. Therefore, \r
+\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$ \r
+the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$.\r
+\r
+We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$ must have at least $\mathsf{{max_g}_C} >= 2$ messages for $\mathsf{r_1}$ to fall off the end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$. $\mathsf{H \neq J}$ by Proposition 3 and the existence of $\mathsf{m}$. Since $\mathsf{H \neq J}$, then by Proposition 3 it could not also have sent a message in $\mathsf{(l_2,..., u}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$, so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a last sequence number similar to Case 1, a contradiction.\r
+\r
+Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$ immediately after $\mathsf{t}$ by Proposition 4. Therefore, \r

 $\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less \r
 $\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less \r

-than $\mathsf{s_p}$. In the $\mathsf{PutDataEntries}$ subroutine, $\mathsf{J}$ adds every \r
-%TODO: Check with Thomas about this part\r
-%rejected message to $\mathsf{CR(p)}$; so for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, \r
-%the $\mathsf{s}$-th element of $\mathsf{X}$ will be recorded in the rejected message list\r
-%$\mathsf{CR}$ of all further elements of $\mathsf{X}$; and every element of \r
-%$\mathsf{X}$ will be recorded in $\mathsf{CR_C(p)}$. Since every rejected message in \r
-%$\mathsf{CR(p)}$ will be in $\mathsf{CR_C(u)}$, ${r_1}$ will be recorded in \r
-%$\mathsf{CR_C(p)}$. When $\mathsf{C}$ receives $\mathsf{u}$, $\mathsf{C}$ will throw \r
-%an error from the match $\mathsf{\tuple{s_q+1, id_J}}$ in $\mathsf{CR_C(p)}$.\r
+than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries}$ subroutine, $\mathsf{J}$ adds every \r

 $\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID \r
 $\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID \r

-$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{p}$ into \r
+$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into \r

 $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely\r
 $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely\r

-those which not all clients have seen. Hence, for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, \r
-the collision winner that has collided with $\mathsf{s}$-th element of $\mathsf{X}$ \r
-will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record \r
-the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ \r
-is received, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
-collision against ${r_1}$. When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
-has seen the $\mathsf{cr}$ entry that records the collision, it will already throw \r
+those which not all clients have seen. Hence, for every $\mathsf{i}$, $\mathsf{1 \leq i < |X|}$, \r
+the collision winner that has collided with $\mathsf{x_i}$ will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ \r
+is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
+collision against ${r_1}$.\r
+\r
+When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
+has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will throw \r

 an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with \r
 $\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.\r
 an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with \r
 $\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.\r

-\item Case 2.2.2.1: \r
+\r

 \end{itemize}\r
 \end{itemize}\r
 \r
 \end{itemize}\r
 \end{itemize}\r
 \r