More comments/fixes

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.

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

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

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

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]

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}
 

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}

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