Add minor comments

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{%

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. 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

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}

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]

reports/spec4b.tex

@@ -37,15 +37,15 @@ \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}.
 
 \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}.}