huge rearangement + new algo. TODO proof on it

Recherche/BFT-ARBover/2_Primitives/index.tex

@@ -7,16 +7,28 @@
   \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
 \end{itemize}
 
-\subsection{Group Election Object}
+\subsection{DenyList Object}
 
-We consider a Groupe Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.
-
-There are three operations: $\CANDIDATE(r), \CLOSE(r)$ and $\READGE(r)$ such that:
-\begin{itemize}
-  \item \textbf{Termination.} A $\CANDIDATE(r), \CLOSE(r)$ or $\READGE(r)$ operation invoked by a correct process always returns.
-  \item \textbf{Election.} If there exists at least one $\CLOSE(r)$ operation and let $\CLOSE(r)^\star$ denote the first $\CLOSE(r)$ in the linearization order. If some correct process $p$ invokes $\CANDIDATE(r)$ and the invocation of $\CANDIDATE(r)$ appears before $\CLOSE(r)^\star$ in the linearization order, then $\Winners_r \neq \emptyset$.
-  \item \textbf{Prefix Inclusion.} If $\CLOSE(r)^\star$ exists, then there exists a set $\Winners_r \subseteq \Pi$ such that, for any process $p_j$: $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ operation is linearized before $\CLOSE(r)^\star$.
-  \item \textbf{Stability.} If $\CLOSE(r)^\star$ exists, then every $\READGE(r)$ operation linearized after
-  $\CLOSE(r)^\star$ returns exactly $\Winners_r$.
-  \item \textbf{READ Validity.} The invocation of $op = \READGE(r)$ by a process $p$ returns the list of valid invocations of $\CANDIDATE(r)$ that appears before $op$ in the linearization order along with the names of the processes that invoked each operation.
-\end{itemize}
+ We assume a synchronous DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.
+  
+    The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
+    \begin{itemize}
+      \item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
+      \item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
+      \begin{itemize}
+        \item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
+        \item $x \in S$, where $S$ is a predefined set. 
+      \end{itemize} 
+      Otherwise, the operation is invalid.
+      \item \textbf{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then:  
+      \begin{itemize}
+        \item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
+        \item A valid $\APPEND(x)$ appears before $op$ in $\Seq$. 
+      \end{itemize}
+      Otherwise, the operation is valid.
+      \item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
+      \item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation. 
+      item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
+    \end{itemize}
+  
+    We assume that $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).