\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*}