papers/lux-consensus/sections/03-system-model.tex

\section{System Model}

\label{sec:model}

\subsection{Network Model}

We model the network as a directed communication graph $G = (V, E)$ where $V$ is the set
of $n$ validators and $E$ represents point-to-point authenticated communication channels.
We assume the network is \emph{partially synchronous}~\cite{dwork1988consensus}: there
exists a known bound $\Delta$ on message delivery time after a global stabilization time
(GST) that is unknown a priori. Before GST, messages may be arbitrarily delayed.

\begin{definition}[Validator Set]
Let $V = H \cup B$ where $H$ is the set of honest validators, $|H| \geq \lceil 2n/3 \rceil + 1$,
and $B$ is the set of Byzantine validators, $|B| \leq \lfloor n/3 \rfloor - 1$. Byzantine
validators may deviate arbitrarily from the protocol but cannot forge cryptographic signatures.
\end{definition}

\begin{definition}[Stake-Weighted Validator Set]
Each validator $v \in V$ holds stake weight $w_v > 0$ with $\sum_{v \in V} w_v = W$.
The Byzantine stake constraint is $\sum_{v \in B} w_v < W/3$.
A \emph{weighted sample} of size $k$ selects validators with probability proportional
to their stake weight.
\end{definition}

\subsection{Adversary Model}

We consider a computationally bounded adversary $\mathcal{A}$ that:
\begin{itemize}
\item Controls up to $f < n/3$ validators (or equivalently, less than $W/3$ stake),
which may behave arbitrarily (Byzantine)
\item Can observe all messages in the network (rushing adversary)
\item Can delay, reorder, and selectively drop messages up to the synchrony bound $\Delta$
\item Cannot break cryptographic primitives (hash functions, digital signatures, VRFs) in
polynomial time
\item Cannot observe honest nodes' internal random coin flips before they are committed
\item Is \emph{static}: cannot corrupt new validators during protocol execution
\end{itemize}

\subsection{Conflict and Preference Model}

\begin{definition}[Transaction DAG]
The transaction set $T$ forms a directed acyclic graph where each transaction $t \in T$
has a set of parents $\text{parents}(t) \subseteq T$ representing the transactions it
extends. A transaction is \emph{valid} if all its ancestors are valid and it satisfies
application-specific validity predicates.
\end{definition}

\begin{definition}[Conflict Set]
Two transactions $t_i, t_j \in T$ \emph{conflict} if they attempt to consume the same
input. The conflict set $\mathcal{C}(t)$ of transaction $t$ is the set of all transactions
that conflict with $t$: $\mathcal{C}(t) = \{t' \in T \mid t' \neq t \text{ and } t' \text{ conflicts with } t\}$.
\end{definition}

\begin{definition}[Preference and Strong Preference]
Node $v$'s preference $\text{pref}(v, t) \in \{0, 1\}$ indicates whether $v$ currently
prefers transaction $t$ over its conflicting alternatives. Transaction $t$ is \emph{strongly
preferred} by $v$ if $\text{pref}(v, t') = 1$ for every ancestor $t'$ in the DAG ancestry
$\mathcal{A}(t) \cup \{t\}$.
\end{definition}

\subsection{Correctness Properties}

We require the following standard properties:

\begin{definition}[Safety]
No two honest validators finalize conflicting transactions. If honest validator $v$ accepts
$t$ and honest validator $u$ accepts $t'$, then $t \notin \mathcal{C}(t')$.
\end{definition}

\begin{definition}[Liveness]
If a valid transaction $t$ is submitted and all honest validators eventually learn of $t$,
then $t$ (or a non-conflicting alternative) is eventually accepted by all honest validators.
\end{definition}

%% -----------------------------------------------------------------------
%%  4. THE LUX PROTOCOL
%% -----------------------------------------------------------------------