From 568e6777dcd749303b97c1edb630964a4afee483 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Thu, 12 Dec 2024 12:58:54 +1100 Subject: [PATCH 1/7] Add 3SF concepts --- reports/3sf.tex | 77 +++++++++++++++++++++++++++++++++++++++++++ reports/preambule.tex | 8 +++++ reports/report.tex | 2 ++ 3 files changed, 87 insertions(+) create mode 100644 reports/3sf.tex diff --git a/reports/3sf.tex b/reports/3sf.tex new file mode 100644 index 0000000..df33838 --- /dev/null +++ b/reports/3sf.tex @@ -0,0 +1,77 @@ +%! TeX root = report.tex + +\section{Basic 3SF concepts}\label{sec:3sf} + +In this section, we summarize the basic concepts of the 3SF protocol that this project depends on. +We refer the reader to the 3SF paper~\cite{d20243} for a more comprehensive explanation or any concepts that this project depends on which we might have missed listing here. + +\paragraph*{Validators.} Participants of the protocol are referred to as \emph{validators} with $n$ being their total number. +Every validator is identified by a unique cryptographic identity and the public keys are common knowledge. +Each validator has a \emph{stake} but for the purpose of this project each validator's stake is set to 1. +% If a validator $v_i$ misbehaves and a proof of this misbehavior is given, it loses a part of its stake ($v_i$ gets \emph{slashed}). + +\paragraph*{Slots.} Time is divided into \emph{slots}. +In ideal condition a new block (see below) is expected to be proposed at the beginning of each slot. + +\paragraph{Blocks and Chains.} +A \emph{block} is a pair of elements, denoted as \( B = (b,p) \). Here, \( b \) represents the \emph{block body} -- essentially, the main content of the block which contains a batch of transactions grouped together. +Each block body contains a reference pointing to its \emph{parent} block. +The second element of the pair, \( p \geq 0 \), indicates the \emph{slot} where the block \( B \) is proposed. +By definition, if $B_p$ is the parent of $B$, then $B_p.p < B.p$. +The \emph{genesis block} is the only block that does not have a parent {and has a negative slot}. +Given the definition above, each different block $B$ implicitly identifies a different finite \emph{chain} of blocks starting from block $B$, down to the genesis block, by recursively moving from a block to its parent. +Hence, there is no real distinction between a block and the chain that it identifies. +So, by chain $\chain$, we mean the chain identified by the block $\chain$. +We write $\chain_1 \preceq \chain_2$ to mean that $\chain_1$ is a non-strict prefix of $\chain_2$. +We say that $\chain_1$ \emph{conflicts} with $\chain_2$ if and only if neither $\chain_1 \preceq \chain_2$ nor $\chain_2 \preceq \chain_1$ holds. + +\paragraph{Checkpoints.} +In the protocol described in~\cite{d20243}, a \emph{checkpoint} is a tuple $(\chain, c)$, where \(\chain \) is a chain and \( c \) is a slot signifying where \( \chain \) is proposed for justification (this concept is introduced and explained below). +However, for efficiency reasons, in the specification targeted by this project, a \emph{valid} checkpoint $\C$ is a triple $(H, c, p)$ where $H$ is the hash of a chain $\chain$, $c$ is as per the definition above and $p = \chain.p$. +The total pre-order among checkpoints is defined: +$\C \leq \C'$ if and only if either \(\C.c < \C'.c\) or, in the case where \(\C.c = \C'.c\), then \(\C.p \leq \C'.p\). +Also, $\C < \C'$ means $\C \leq \C' \land \C \neq \C'$. + + +\paragraph*{FFG Votes.} +Validators cast two main types of votes: \textsc{ffg-vote}s and \textsc{vote}s. +Each \textsc{vote} includes an \textsc{ffg-vote}. +The specification targeted by this project only deals with \textsc{ffg-vote}s as the extra information included in \textsc{vote}s has no impact on AccountableSafety. +An \textsc{ffg-vote} is represented as a tuple \([\textsc{ffg-vote}, \C_1, \C_2, v_i]\), where {$v_i$ is the validator sending the \textsc{ffg-vote}\footnote{Digital signature are employed to ensure that $v_i$ is the actual sender and it is assumed that such digital signatures are unforgeable.}, while} \(\C_1\) and \(\C_2\) are checkpoints. +These checkpoints are respectively referred to as the \emph{source} (\(\C_1\)) and the \emph{target} (\(\C_2\)) of the \textsc{ffg-vote}. +Such an \textsc{ffg-vote} is \emph{valid} +%(i.e., $\mathrm{valid}(\C_1 \to \C_2$)) +if and only if both checkpoints are valid, +\(\C_1.c < \C_2.c\) and \(\C_1.\chain \preceq \C_2.\chain\). +\textsc{ffg-vote}s effectively act as \emph{links} connecting the source and target checkpoints. Sometimes the whole \textsc{ffg-vote} is simply denoted as \(\C_1 \to \C_2\). + +\paragraph*{Justification.} +A set of \textsc{ffg-vote}s is a \emph{supermajority set} if it contains valid \textsc{ffg-vote}s from at least \(\frac{2}{3}n\) distinct validators. +A checkpoint \(\C\) is considered \emph{justified} if it either corresponds to the genesis block, i.e., \(\C = (B_\text{genesis}, 0)\), or if there exists a supermajority set of links \(\{\C_i \to \C_j\}\) satisfying the following conditions. First, for each link $\C_i \to \C_j$ in the set, {\(\C_i \to \C_j\) is valid and} \(\C_i.\chain \preceq \C.\chain \preceq \C_j.\chain\). Moreover, all source checkpoints \(\C_i\) in these links need to be already justified, and the checkpoint slot of \(\C_j\) needs to be the same as that of \(\C\) (\(\C_j.c=\C.c\)), for every \(j\). It is important to note that the source and target chain may vary across different votes. +% This justification rule is formalized by the binary function $\mathsf{J}(\V,\C)$ in Algorithm~\ref{alg:justification-finalization} which outputs \textsc{true} if and only if checkpoint $\C$ is justified according to the set of messages $\V$. +% Lastly, we say that a {chain \(\chain\)} \emph{is justified} if and only if there exists a justified checkpoint \(\C\) for which {\(\C.\chain = \chain\)}. + +% \paragraph*{Greatest justified checkpoint and chain.} +% A checkpoint is considered justified in a view \(\V\) if \(\V\) contains a supermajority set of links justifying it. A \emph{justified} checkpoint which is maximal in \(\V\) with respect to the previously defined lexicographic ordering is referred to as the \emph{greatest justified checkpoint} in \(\V\), denoted as \(\GJ(\V)\). In the event of ties, they are broken arbitrarily. Chain \(\GJ(\V).\chain\) is referred to as the \emph{greatest justified chain}. + +\paragraph*{Finality.} +A checkpoint \(\C\) is \emph{finalized} if it is justified and there exists a supermajority link with source \(\C\) and potentially different targets \(\C_i\) where \(\C_i.c = \C.c + 1\). A chain \(\chain\) is finalized if there exists a finalized checkpoint \(\C\) with \(\chain = \C.\chain\). The checkpoint \(\C = (B_\text{genesis}, 0)\) is finalized by definition. +% This finalization rule is formalized by the binary function $\mathsf{F}(\V,\C)$ in Algorithm~\ref{alg:justification-finalization} which outputs \textsc{true} if and only if checkpoint $\C$ is finalized according to the set of messages $\V$. +% {Given a view $\V$, a finalized checkpoint which is maximal in \(\V\) with respect to the previously defined lexicographic ordering is referred to as the \emph{greatest finalized checkpoint} in \(\V\), denoted as \(\GF(\V)\). +% In the event of ties, they are broken arbitrarily. +% % We say that a chain +% We say that a chain $\chain$ is finalized according to a view $\V$ if and only if $\chain \preceq \GF(\V).\chain$. + + +\paragraph*{Slashing.} +A validator \(v_i\) is subject to slashing for sending two \emph{distinct} \textsc{ffg-vote}s \(\C_1 \to \C_2\) and \(\C_3 \to \C_4\) if either of the following conditions holds: {\(\mathbf{E_1}\) (Double voting)} if \(\C_2.c = \C_4.c\), implying that a validator must not cast distinct \textsc{ffg-vote}s for the same checkpoint slot; or {\(\mathbf{E_2}\) (Surround voting)} if \(\C_3 < \C_1\) + and \(\C_2.c < \C_4.c\), indicating that a validator must not vote using a lower checkpoint as source and must avoid voting within the span of its other votes. + + + \begin{definition}[AccountableSafety] + \label{def:acc-safety} + AccountableSafety holds if and only if, upon two conflicting chains being finalized, + {by having access to all messages sent,} it is possible to slash at least $\frac{n}{3}$ of the validators. + % Finally, we also say that a chain is $f$-\emph{accountable} if the protocol outputting it has Accountable Safety with resilience $f$. + % If a protocol $\Pi$ comprises $k$ subprotocols, $\Pi_i$, each of which outputs a chain, $\Chain_i$, we say that $\Chain_i$ is $f$-accountable if $\Pi_i$ is $f$-accountable. +\end{definition} \ No newline at end of file diff --git a/reports/preambule.tex b/reports/preambule.tex index 7ff3fbe..5e7a13d 100644 --- a/reports/preambule.tex +++ b/reports/preambule.tex @@ -82,6 +82,7 @@ \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} +\newtheorem{definition}{Definition} \newcommand{\iteDef}[4]{ #1 \coloneqq \left\{ @@ -128,6 +129,13 @@ \newcommand{\Push}{\mathrm{Push}} \newcommand{\At}{\mathrm{At}} \newcommand{\Indices}{\mathrm{Indices}} +\newcommand{\chain}[0]{\mathsf{ch}} +\newcommand{\C}[0]{\mathcal{C}} +\newcommand{\V}[0]{\mathcal{V}} +\newcommand{\GF}[0]{\mathcal{GF}} +\newcommand{\GJ}[0]{\mathcal{GJ}} + + % \newcommand{\UNION}{\mathrm{UNION}} % \newcommand{\CHOOSE}{\mathrm{CHOOSE}} % \newcommand{\TRUE}{\mathrm{TRUE}} diff --git a/reports/report.tex b/reports/report.tex index 00ee571..d869d3d 100644 --- a/reports/report.tex +++ b/reports/report.tex @@ -65,6 +65,8 @@ \input{intro} +\input{3sf} + % Milestone 1 - Spec 1 \input{spec1} From ccf873ad11c732f8d0e2ff7257dc2ab24acc276b Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Sat, 14 Dec 2024 09:43:41 +1100 Subject: [PATCH 2/7] Update reports/3sf.tex Co-authored-by: Kukovec --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index df33838..cb6291a 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -3,7 +3,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} In this section, we summarize the basic concepts of the 3SF protocol that this project depends on. -We refer the reader to the 3SF paper~\cite{d20243} for a more comprehensive explanation or any concepts that this project depends on which we might have missed listing here. +We refer the reader to the 3SF paper~\cite{d20243} for a more comprehensive explanation. \paragraph*{Validators.} Participants of the protocol are referred to as \emph{validators} with $n$ being their total number. Every validator is identified by a unique cryptographic identity and the public keys are common knowledge. From dd7cbf67b524cd2b78d18adf2bf6bc6648949af1 Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Sat, 14 Dec 2024 09:44:14 +1100 Subject: [PATCH 3/7] Update reports/3sf.tex Co-authored-by: Kukovec --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index cb6291a..7cd57be 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -37,7 +37,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} Validators cast two main types of votes: \textsc{ffg-vote}s and \textsc{vote}s. Each \textsc{vote} includes an \textsc{ffg-vote}. The specification targeted by this project only deals with \textsc{ffg-vote}s as the extra information included in \textsc{vote}s has no impact on AccountableSafety. -An \textsc{ffg-vote} is represented as a tuple \([\textsc{ffg-vote}, \C_1, \C_2, v_i]\), where {$v_i$ is the validator sending the \textsc{ffg-vote}\footnote{Digital signature are employed to ensure that $v_i$ is the actual sender and it is assumed that such digital signatures are unforgeable.}, while} \(\C_1\) and \(\C_2\) are checkpoints. +An \textsc{ffg-vote} is represented as a tuple \([\textsc{ffg-vote}, \C_1, \C_2, v_i]\), where {$v_i$ is the validator sending the \textsc{ffg-vote}\footnote{Digital signatures are employed to ensure that $v_i$ is the actual sender and it is assumed that such digital signatures are unforgeable.}, while} \(\C_1\) and \(\C_2\) are checkpoints. These checkpoints are respectively referred to as the \emph{source} (\(\C_1\)) and the \emph{target} (\(\C_2\)) of the \textsc{ffg-vote}. Such an \textsc{ffg-vote} is \emph{valid} %(i.e., $\mathrm{valid}(\C_1 \to \C_2$)) From 78cd478f01fdd1d78bf573c7ebc3304fbb11ef0c Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Sat, 14 Dec 2024 09:44:42 +1100 Subject: [PATCH 4/7] Update reports/3sf.tex Co-authored-by: Kukovec --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index 7cd57be..1305dda 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -55,7 +55,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} % A checkpoint is considered justified in a view \(\V\) if \(\V\) contains a supermajority set of links justifying it. A \emph{justified} checkpoint which is maximal in \(\V\) with respect to the previously defined lexicographic ordering is referred to as the \emph{greatest justified checkpoint} in \(\V\), denoted as \(\GJ(\V)\). In the event of ties, they are broken arbitrarily. Chain \(\GJ(\V).\chain\) is referred to as the \emph{greatest justified chain}. \paragraph*{Finality.} -A checkpoint \(\C\) is \emph{finalized} if it is justified and there exists a supermajority link with source \(\C\) and potentially different targets \(\C_i\) where \(\C_i.c = \C.c + 1\). A chain \(\chain\) is finalized if there exists a finalized checkpoint \(\C\) with \(\chain = \C.\chain\). The checkpoint \(\C = (B_\text{genesis}, 0)\) is finalized by definition. +A checkpoint \(\C\) is \emph{finalized} if it is justified and there exists a supermajority link with source \(\C\) and potentially different targets \(\C_j\) where \(\C_j.c = \C.c + 1\). A chain \(\chain\) is finalized if there exists a finalized checkpoint \(\C\) with \(\chain = \C.\chain\). The checkpoint \(\C = (B_\text{genesis}, 0)\) is finalized by definition. % This finalization rule is formalized by the binary function $\mathsf{F}(\V,\C)$ in Algorithm~\ref{alg:justification-finalization} which outputs \textsc{true} if and only if checkpoint $\C$ is finalized according to the set of messages $\V$. % {Given a view $\V$, a finalized checkpoint which is maximal in \(\V\) with respect to the previously defined lexicographic ordering is referred to as the \emph{greatest finalized checkpoint} in \(\V\), denoted as \(\GF(\V)\). % In the event of ties, they are broken arbitrarily. From d92d0e6b9d70e858ba142fdf499cf6a5039a75f8 Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Sat, 14 Dec 2024 09:45:45 +1100 Subject: [PATCH 5/7] Update reports/3sf.tex Co-authored-by: Kukovec --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index 1305dda..77178a4 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -11,7 +11,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} % If a validator $v_i$ misbehaves and a proof of this misbehavior is given, it loses a part of its stake ($v_i$ gets \emph{slashed}). \paragraph*{Slots.} Time is divided into \emph{slots}. -In ideal condition a new block (see below) is expected to be proposed at the beginning of each slot. +In ideal conditions a new block (see below) is expected to be proposed at the beginning of each slot. \paragraph{Blocks and Chains.} A \emph{block} is a pair of elements, denoted as \( B = (b,p) \). Here, \( b \) represents the \emph{block body} -- essentially, the main content of the block which contains a batch of transactions grouped together. From 86d657f6b1a948f07e0fc0c8b2193b54a68cd6e2 Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Tue, 17 Dec 2024 13:02:14 +1100 Subject: [PATCH 6/7] Update reports/3sf.tex Co-authored-by: Thomas Pani --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index 77178a4..0ef41f9 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -18,7 +18,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} Each block body contains a reference pointing to its \emph{parent} block. The second element of the pair, \( p \geq 0 \), indicates the \emph{slot} where the block \( B \) is proposed. By definition, if $B_p$ is the parent of $B$, then $B_p.p < B.p$. -The \emph{genesis block} is the only block that does not have a parent {and has a negative slot}. +The \emph{genesis block} is the only block that does not have a parent. Its slot is \( p = 0 \). Given the definition above, each different block $B$ implicitly identifies a different finite \emph{chain} of blocks starting from block $B$, down to the genesis block, by recursively moving from a block to its parent. Hence, there is no real distinction between a block and the chain that it identifies. So, by chain $\chain$, we mean the chain identified by the block $\chain$. From 49d422347ed6ef23b1844690187481984212d4dd Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Tue, 17 Dec 2024 13:04:39 +1100 Subject: [PATCH 7/7] Small fix --- reports/3sf.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/3sf.tex b/reports/3sf.tex index 0ef41f9..0e755ad 100644 --- a/reports/3sf.tex +++ b/reports/3sf.tex @@ -27,7 +27,7 @@ \section{Basic 3SF concepts}\label{sec:3sf} \paragraph{Checkpoints.} In the protocol described in~\cite{d20243}, a \emph{checkpoint} is a tuple $(\chain, c)$, where \(\chain \) is a chain and \( c \) is a slot signifying where \( \chain \) is proposed for justification (this concept is introduced and explained below). -However, for efficiency reasons, in the specification targeted by this project, a \emph{valid} checkpoint $\C$ is a triple $(H, c, p)$ where $H$ is the hash of a chain $\chain$, $c$ is as per the definition above and $p = \chain.p$. +However, for efficiency reasons, in the specification targeted by this project, a \emph{valid} checkpoint $\C$ is a triple $(H, c, p)$ where $H$ is the hash of a chain $\chain$, $c$ is the slot at which chain $\chain$ is proposed for justification, as per the definition above, and $p = \chain.p$. The total pre-order among checkpoints is defined: $\C \leq \C'$ if and only if either \(\C.c < \C'.c\) or, in the case where \(\C.c = \C'.c\), then \(\C.p \leq \C'.p\). Also, $\C < \C'$ means $\C \leq \C' \land \C \neq \C'$.