From b26bf642c14c2f12bac0ed9cf631628df8801619 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Wed, 27 Nov 2024 23:12:52 +1100 Subject: [PATCH 1/6] Add minor comments --- reports/discussion.tex | 2 +- reports/report.tex | 1 + reports/spec1.tex | 2 +- reports/spec2.tex | 1 + reports/spec3-alloy.tex | 3 ++- reports/spec4b.tex | 4 ++-- 6 files changed, 8 insertions(+), 5 deletions(-) diff --git a/reports/discussion.tex b/reports/discussion.tex index 284a2d5..fa6a7ab 100644 --- a/reports/discussion.tex +++ b/reports/discussion.tex @@ -4,7 +4,7 @@ various perspectives. Initially, we developed a direct translation of the protocol's Python specification into \tlap{}, but this approach proved unsatisfactory due to the reliance on recursion. To address this, we modified -the specification to use folds in place of recursion, theoretically enabling +the specification to use folds\rs{if possible, quickly explain what folds are or provide a reference} in place of recursion, theoretically enabling model-checking with Apalache. However, this approach also proved impractical due to the high computational complexity involved. Subsequently, we applied a series of abstractions to improve the model-checking efficiency. diff --git a/reports/report.tex b/reports/report.tex index 00ee571..2dacf94 100644 --- a/reports/report.tex +++ b/reports/report.tex @@ -11,6 +11,7 @@ \newcommand{\tth}[1]{\footnote{\textcolor{blue}{#1}}} \newcommand{\tbh}[1]{\textsc{\textbf{#1}}} +\newcommand{\rs}[1]{\footnote{\textcolor{purple}{#1}}} \title{Technical Report:\\ Exploring Automatic Model-Checking of the Ethereum specification\footnote{% diff --git a/reports/spec1.tex b/reports/spec1.tex index 563eb50..0f820aa 100644 --- a/reports/spec1.tex +++ b/reports/spec1.tex @@ -33,7 +33,7 @@ \subsection{Shape of the Python Specification} \paragraph{Functions.} The function definitions are mostly pure functions that take some input and return some output -- side-effects are rare and limited to -auxiliary state when computing the function output. Some functions are +auxiliary state when computing the function output.\rs{Not sure this is correct as all functions should be side-effect free.} Some functions are (mutually) recursive, as can be seen in Figure~\ref{fig:callgraph}. \paragraph{Similarities between Python and \tlap{}.} Despite being a programming diff --git a/reports/spec2.tex b/reports/spec2.tex index ee4ae96..021f03a 100644 --- a/reports/spec2.tex +++ b/reports/spec2.tex @@ -148,6 +148,7 @@ \subsection{Checking the Specification} forest. The graphs in Figures~\ref{fig:tricky1}--\ref{fig:tricky2} do not represent chains. The graph~\texttt{I1} is a direct-acyclic graph but not a forest. The graph~\texttt{I2} has a loop. +\rs{Perhaps this was something that we failed to make clear, but there is no need to consider graphs that are not trees. Or perhaps I don't fully understand the point that we are making above. Let's discuss.} \begin{figure} \input{block-graphs} diff --git a/reports/spec3-alloy.tex b/reports/spec3-alloy.tex index b0c8cf6..2e5ce9d 100644 --- a/reports/spec3-alloy.tex +++ b/reports/spec3-alloy.tex @@ -14,6 +14,7 @@ \section{\SpecThreeB{} in Alloy}\label{sec:alloy} restrict the number of checkpoints and votes to 5 and 12, respectively. Although we introduced similar restrictions with Apalache, Alloy has even finer level of parameter tuning. + \rs{Is there some inherent limitation of Apalache that we should discuss?} \item Alloy translates the model checking problem to a Boolean satisfiability problem (SAT), in constrast to Apalache, which translates it to satisfiability-modulo-theory (SMT). This @@ -50,7 +51,7 @@ \subsection{From \tlap{} to Alloy} \end{lstlisting} In contrast to~\SpecThree{}, our Alloy specification does not describe a -state machine, but it specifies an arbitrary single state of the protocol. As +state machine, but it specifies an arbitrary single state of the protocol.\rs{Like the SMT spec, right? if so, perhaps we should say so} As in~\SpecThree{}, we compute the set of justified checkpoints as a fixpoint: \begin{lstlisting}[language=alloy,columns=fullflexible] diff --git a/reports/spec4b.tex b/reports/spec4b.tex index ef4729e..cac79c5 100644 --- a/reports/spec4b.tex +++ b/reports/spec4b.tex @@ -37,7 +37,7 @@ \subsection{Constraints over set cardinalities} \cdot T + 1$ set elements to show that Equation~(\ref{eq:card-comparison2}) holds true. This gives us a linear number of constraints, instead of a quadratic one. For example, when $T=1$ and the set may contain up to~$n$ -elements, the model checker produces $3 \cdot O(n)$ constraints to check +elements, the model checker produces $3 \cdot O(n)$\rs{Why write $3\cdot O(n)$ rather than just $O(n)$ given that $3 \cdot O(n) \in O(n)$.} constraints to check Equation~(\ref{eq:card-comparison2}). A similar optimization is used in the specification of Tendermint~\cite{TendermintSpec2020}. @@ -45,7 +45,7 @@ \subsection{Quorum sets} To further optimize the constraints over set cardinalities, we have applied the well-known pattern of replacing cardinality tests with quorum sets. For -example, this approach is used in the specification of Paxos\footnote{% +example, this approach is used in the specification of Paxos\rs{Why use footnote here rather than a citation?}\footnote{% \tlap{} specification of Paxos: \url{https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla}.} From 6625f4ab27b2192166d9dabf66a534730b469eec Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 16 Dec 2024 15:21:56 +0100 Subject: [PATCH 2/6] Address some of the comments --- reports/discussion.tex | 2 +- reports/spec1.tex | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/reports/discussion.tex b/reports/discussion.tex index fa6a7ab..284a2d5 100644 --- a/reports/discussion.tex +++ b/reports/discussion.tex @@ -4,7 +4,7 @@ various perspectives. Initially, we developed a direct translation of the protocol's Python specification into \tlap{}, but this approach proved unsatisfactory due to the reliance on recursion. To address this, we modified -the specification to use folds\rs{if possible, quickly explain what folds are or provide a reference} in place of recursion, theoretically enabling +the specification to use folds in place of recursion, theoretically enabling model-checking with Apalache. However, this approach also proved impractical due to the high computational complexity involved. Subsequently, we applied a series of abstractions to improve the model-checking efficiency. diff --git a/reports/spec1.tex b/reports/spec1.tex index 0f820aa..c0bc5db 100644 --- a/reports/spec1.tex +++ b/reports/spec1.tex @@ -31,9 +31,9 @@ \subsection{Shape of the Python Specification} code. Composite types are defined using the \texttt{pyrsistent} library, which provides immutable data structures such as sets and maps. -\paragraph{Functions.} The function definitions are mostly pure functions that +\paragraph{Functions.} The function definitions are pure functions that take some input and return some output -- side-effects are rare and limited to -auxiliary state when computing the function output.\rs{Not sure this is correct as all functions should be side-effect free.} Some functions are +local state. Some functions are (mutually) recursive, as can be seen in Figure~\ref{fig:callgraph}. \paragraph{Similarities between Python and \tlap{}.} Despite being a programming From 85998298604caa1d258c0faaf064099436fe14ae Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 16 Dec 2024 15:44:45 +0100 Subject: [PATCH 3/6] Address some of the comments --- reports/spec3-alloy.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/spec3-alloy.tex b/reports/spec3-alloy.tex index 2e5ce9d..c30fd8a 100644 --- a/reports/spec3-alloy.tex +++ b/reports/spec3-alloy.tex @@ -51,7 +51,7 @@ \subsection{From \tlap{} to Alloy} \end{lstlisting} In contrast to~\SpecThree{}, our Alloy specification does not describe a -state machine, but it specifies an arbitrary single state of the protocol.\rs{Like the SMT spec, right? if so, perhaps we should say so} As +state machine, but it specifies an arbitrary single state of the protocol. As in~\SpecThree{}, we compute the set of justified checkpoints as a fixpoint: \begin{lstlisting}[language=alloy,columns=fullflexible] From f2f9e7a0fb205296c50765e87c9e9ff658b8b561 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Tue, 17 Dec 2024 14:11:51 +1100 Subject: [PATCH 4/6] Explain why we also consider forests --- reports/spec2.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/reports/spec2.tex b/reports/spec2.tex index 021f03a..e1f7bb4 100644 --- a/reports/spec2.tex +++ b/reports/spec2.tex @@ -134,7 +134,7 @@ \subsection{Checking the Specification} on top of these graphs. -To further evaluate \SpecTwo{}, we fix the block graph --- this way the solver +To further evaluate \SpecTwo{}, we fix the block graph\footnote{We consider forests, rather than just trees, because the specification allows for that. Specifically, forests can occur when only some of the blocks of a given chain are received by a node. In the specification, the set of blocks received corresponds the map \texttt{CommonNodeState.view\_blocks}.} --- this way the solver only has to reason about voting. We encode three example block graphs: a single, linear chain (\texttt{SingleChain}), a minimal forked chain of three blocks (\texttt{ShortFork}), and a forest of disconnected chains @@ -148,7 +148,6 @@ \subsection{Checking the Specification} forest. The graphs in Figures~\ref{fig:tricky1}--\ref{fig:tricky2} do not represent chains. The graph~\texttt{I1} is a direct-acyclic graph but not a forest. The graph~\texttt{I2} has a loop. -\rs{Perhaps this was something that we failed to make clear, but there is no need to consider graphs that are not trees. Or perhaps I don't fully understand the point that we are making above. Let's discuss.} \begin{figure} \input{block-graphs} From acbecd28afc356282c1ad70bf242d78ec660e636 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Wed, 18 Dec 2024 15:34:32 +1100 Subject: [PATCH 5/6] Remove comment --- reports/spec3-alloy.tex | 1 - 1 file changed, 1 deletion(-) diff --git a/reports/spec3-alloy.tex b/reports/spec3-alloy.tex index 6690a7d..f73d78b 100644 --- a/reports/spec3-alloy.tex +++ b/reports/spec3-alloy.tex @@ -14,7 +14,6 @@ \section{\SpecThreeC{} in Alloy}\label{sec:alloy} restrict the number of checkpoints and votes to 5 and 12, respectively. Although we introduced similar restrictions with Apalache, Alloy has even finer level of parameter tuning. - \rs{Is there some inherent limitation of Apalache that we should discuss?} \item Alloy translates the model checking problem to a Boolean satisfiability problem (SAT), in contrast to Apalache, which translates it to satisfiability-modulo-theory (SMT). This From 08584bb1227c26c3d1c546ce2ef5e66a83294822 Mon Sep 17 00:00:00 2001 From: Roberto Saltini <38655434+saltiniroberto@users.noreply.github.com> Date: Wed, 18 Dec 2024 23:01:35 +1100 Subject: [PATCH 6/6] Update reports/spec2.tex Co-authored-by: Thomas Pani --- reports/spec2.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reports/spec2.tex b/reports/spec2.tex index 2fccd1b..52b5ca1 100644 --- a/reports/spec2.tex +++ b/reports/spec2.tex @@ -134,7 +134,7 @@ \subsection{Checking the Specification} on top of these graphs. -To further evaluate \SpecTwo{}, we fix the block graph\footnote{We consider forests, rather than just trees, because the specification allows for that. Specifically, forests can occur when only some of the blocks of a given chain are received by a node. In the specification, the set of blocks received corresponds the map \texttt{CommonNodeState.view\_blocks}.} --- this way the solver +To further evaluate \SpecTwo{}, we fix the block graph\footnote{We consider forests, rather than just trees, because the specification allows for that. Specifically, forests can occur when only some of the blocks of a given chain are received by a node. In the specification, the set of blocks received corresponds to the map \texttt{CommonNodeState.view\_blocks}.} --- this way the solver only has to reason about voting. We encode three example block graphs: a single, linear chain (\texttt{SingleChain}), a minimal forked chain of three blocks (\texttt{ShortFork}), and a forest of disconnected chains