diff --git a/reports/discussion.tex b/reports/discussion.tex index fb5745e..36fadb2 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{We should explain what folds are} 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. @@ -24,7 +24,7 @@ in \tlap{}, Alloy, and SMT (CVC5), representing both a direct translation and different levels of abstraction of the protocol. The largest instances we exhaustively verified to satisfy \textit{AccountableSafety} include up to 7 -checkpoints and 24 validator votes (see Table~\ref{tab:alloy-mc} in +checkpoints\rs{Roberto/Thanh-Hai to perhaps add a short description of the 3SF protocol explaining the basic concepts} and 24 validator votes (see Table~\ref{tab:alloy-mc} in Section~\ref{sec:alloy-results}). This comprehensive verification gives us absolute confidence that the modeled protocol satisfies \textit{AccountableSafety} for systems up to this size. diff --git a/reports/future.tex b/reports/future.tex index 966d0ed..343e341 100644 --- a/reports/future.tex +++ b/reports/future.tex @@ -2,6 +2,8 @@ \begin{enumerate} + \item \emph{Prove other properties.}\rs{Roberto to add.} + \item \emph{Generating inputs to the Python specification.} As we have noted, the power of our~\tlap{} specifications is the ability to generate examples with Apalache. This would help the authors of the Python specification to diff --git a/reports/intro.tex b/reports/intro.tex index e09677e..c34fe93 100644 --- a/reports/intro.tex +++ b/reports/intro.tex @@ -63,7 +63,7 @@ \section{Introduction} \paragraph{Complexity of (model-checking) the protocol.} The 3SF protocol is intricate, with a high degree of combinatorial complexity, making it challenging -to reason about. We have observed multiple layers of complexity\rs{We should point out that the following points make automatic model checking complex, not other formal verification techniques, such as theorem proving. Perhaps add a section on the diff between automatic model checking and theorem proving.} in the protocol: +for automatic model checking. We have observed multiple layers of complexity in the protocol: \begin{itemize} \item The Python specification considers all possible graphs over all proposed blocks. From graph theory~\cite{cayley1878theorem}, we know that the number 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/spec3-alloy.tex b/reports/spec3-alloy.tex index e4c9853..3d65a31 100644 --- a/reports/spec3-alloy.tex +++ b/reports/spec3-alloy.tex @@ -3,7 +3,7 @@ \section{\SpecThreeB{} in Alloy}\label{sec:alloy} Once we saw that our specifications~\SpecThree{} and~\SpecFour{} -were too challenging for the \tlap{} tools, we have decided\rs{we decided (without ``have'')} to employ +were too challenging for the \tlap{} tools, we decided to employ Alloy~\cite{jackson2012software,alloytools}, as an alternative to our tooling. Alloy has two features that are attractive for our project: @@ -17,8 +17,7 @@ \section{\SpecThreeB{} in Alloy}\label{sec:alloy} \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).\rs{It may good to explain SMT vs SAT} This - allows us to run the latest off-the-shelf solvers such as Kissat, the + problem (SAT), in contrast to Apalache, which translates it to satisfiability-modulo-theory (SMT). This allows us to run the latest off-the-shelf solvers such as Kissat, the winner of the SAT Competition 2024~\cite{SAT-Competition-2024-solvers}. \end{itemize} @@ -51,7 +50,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{this is similar to the SMT spec} 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/spec3.tex b/reports/spec3.tex index ec7c74a..26d665a 100644 --- a/reports/spec3.tex +++ b/reports/spec3.tex @@ -83,7 +83,7 @@ \subsection{Introducing a state machine} \subsection{Model checking experiments} We have conducted model checking experiments with this specification. They are -summarized in Table~\ref{tab:abstract-ffg-mc}.\rs{What does ``N'' mean in the last row of the table?} Two things to notice: +summarized in Table~\ref{tab:abstract-ffg-mc}. Two things to notice: \begin{itemize} diff --git a/reports/spec4.tex b/reports/spec4.tex index e73f9dd..8d6f40d 100644 --- a/reports/spec4.tex +++ b/reports/spec4.tex @@ -25,7 +25,7 @@ \subsection{Inductive Invariant}\label{sec:spec4-indinv} The challenge, typically, is that inductive invariants are more difficult to write, compared to state invariants. They are usually composed of several lemmas, i.e. properties that we are less interested in on their own, but which are crucial in establishing property (2.). -As we explain below, the inductive invariant introduced in \SpecFour{} mainly contains of two sets of lemmas, one for characterizing the chain-fork scenarios, and a second one for characterizing justified checkpoints, shown in Figure~\ref{figFork} and Figure~\ref{figJC} respectively. +As we explain below, the inductive invariant introduced in \SpecFour{} mainly consists of two sets of lemmas, one for characterizing the chain-fork scenarios, and a second one for characterizing justified checkpoints, shown in Figure~\ref{figFork} and Figure~\ref{figJC} respectively. \begin{figure} \includegraphics[width=\textwidth]{images/chain-and-fork-inv.pdf} diff --git a/reports/spec4b.tex b/reports/spec4b.tex index 455e057..0d50b50 100644 --- a/reports/spec4b.tex +++ b/reports/spec4b.tex @@ -9,7 +9,6 @@ \section{\SpecFourB{}: Decomposition \& abstractions}\label{sec:spec4b} find these abstractions quite important for further research on model checking of algorithms similar to 3SF\@. -\textcolor{purple}{RS: Done till here} \subsection{Constraints over set cardinalities} @@ -22,7 +21,7 @@ \subsection{Constraints over set cardinalities} In the general case, the symbolic model checker has to encode constraints for the cardinality computation in Equation~(\ref{eq:card-comparison}). If a set -$S$ contains up to $n$~elements, Apalache produces $O(n^2)$~constraints\rs{it may be good to provide an intuition for why $O(n^2)$.} for +$S$ contains up to $n$~elements, Apalache produces $O(n^2)$~constraints for $\textit{Cardinality(S)}$. To partially remediate the above issue in~\SpecFour{}, we introduce a