121 lines
6.2 KiB
TeX
121 lines
6.2 KiB
TeX
\begin{theorem}[Integrity]
|
|
If a message $m$ is delivered by any process, then it was previously broadcast by some process via the \texttt{AB-broadcast} primitive.
|
|
\end{theorem}
|
|
|
|
\begin{proof}
|
|
Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs.
|
|
|
|
\begin{align*}
|
|
&\text{AB-deliver}_j(m) & \text{(line 24)} \\
|
|
\Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\
|
|
\Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\
|
|
\Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\
|
|
\Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\
|
|
\Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\
|
|
&\textbf{else if } m_1 \neq m: \\
|
|
&\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\
|
|
&\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\
|
|
&\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)}
|
|
\end{align*}
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}[No Duplication]
|
|
No message is delivered more than once by any process.
|
|
\end{theorem}
|
|
|
|
\begin{proof}
|
|
Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$.
|
|
|
|
\begin{align*}
|
|
&\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\
|
|
\Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\
|
|
\Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\
|
|
\Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\
|
|
&\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)}
|
|
\end{align*}
|
|
|
|
We now distinguish two cases:
|
|
|
|
\vspace{0.5em}
|
|
\noindent\textbf{Case 1:} $r_0 = r_1$:
|
|
\begin{itemize}
|
|
\item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$.
|
|
\item If $j_0 = j_1$:
|
|
\begin{align*}
|
|
\Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\
|
|
\Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\
|
|
\Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\
|
|
\Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\
|
|
&\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\
|
|
&\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\
|
|
&\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\
|
|
\end{align*}
|
|
\end{itemize}
|
|
|
|
% \vspace{0.5em}
|
|
\noindent\textbf{Case 2:} $r_0 \ne r_1$:
|
|
\begin{itemize}
|
|
\item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds.
|
|
\item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds.
|
|
\end{itemize}
|
|
|
|
In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$
|
|
\end{proof}
|
|
|
|
% \subsubsection{No Duplication}
|
|
|
|
% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$
|
|
% \\
|
|
% Proof \\
|
|
% \begin{align*}
|
|
% &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\
|
|
% &\exists r_0,\ m_0 \in M^{r_0} \\
|
|
% &\exists r_1,\ m_1 \in M^{r_1} \\
|
|
% &\text{if } r_0 = r_1 \\
|
|
% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
|
|
% &\quad \text{if} j_0 \neq j_1 \\
|
|
% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
|
|
% &\quad \text{if } j_0 = j_1 \\
|
|
% &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\
|
|
% &\quad\quad \text{Impossible si } j_0 \text{ correct} \\
|
|
% &\text{else} \\
|
|
% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
|
|
% &\quad \text{if } j_0 \neq j_1 \\
|
|
% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
|
|
% &\quad \text{if } j_0 = j_1 \\
|
|
% &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\
|
|
% &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques}
|
|
% \end{align*}
|
|
|
|
\subsubsection{Broadcast Validity}
|
|
$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\
|
|
|
|
Proof:
|
|
\begin{align*}
|
|
&\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\
|
|
&\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\
|
|
&\exists receieved : m_0 \in receieved_{j_1} \\
|
|
&\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\
|
|
&\exists prop: \text{prop}[r_0][j_0] = m_0 \\
|
|
&\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\
|
|
&\quad r_0 += 1 \\
|
|
&\quad \text{jump to LOOP} \\
|
|
&\text{else} \\
|
|
&\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\
|
|
&\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\
|
|
&\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0)
|
|
\end{align*}
|
|
|
|
\subsubsection*{AB receive width}
|
|
\[
|
|
\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1}
|
|
\]
|
|
|
|
Proof:
|
|
\begin{align*}
|
|
&\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\
|
|
&\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0)
|
|
\end{align*} |