ras

Author: OlivierBBB

rom/generalities/binarities.tex

@@ -4,13 +4,16 @@
 	\item \romColumnPadding{}
 	\item \romColumnClaimedByPush{}
 	\item \PFB{}
-	\item \romColumnOpcodeIsPush{} \quad (\trash)
-	\item \romColumnOpcodeIsJumpDest{} \quad (\trash)
-	\item[\vspace{\fill}]
 	\item \romColumnEmptyCode    {}
 	\item \romColumnNonemptyCode {}
 	\item \done                  {}
+	\item \romColumnOpcodeIsPush{}     (\trash)
+	\item \romColumnOpcodeIsJumpDest{} (\trash)
+	\item[\vspace{\fill}]
     \end{enumerate}
 \end{multicols}
 \saNote{}
-both \romColumnOpcodeIsPush{} and \romColumnOpcodeIsJumpDest{} are instruction decoded, see section~(\ref{rom: instruction decoding}); their ``binary-ness'' is thus a given.
+both \romColumnOpcodeIsPush{} and \romColumnOpcodeIsJumpDest{} are instruction decoded,
+see section~(\ref{rom: instruction decoding});
+their ``binary-ness'' is thus a given,
+whence the (\trash).

rom/generalities/cfi.tex

@@ -1,14 +1,21 @@
 We impose
 \begin{enumerate}
 	\item $\romColumnCfi _{0} = 0$ (\sanityCheck)
-	\item $\romColumnCfi _{i + 1} \in \{ \romColumnCfi _{i}, 1 + \romColumnCfi _{i} \}$ (\sanityCheck)
+	\item\label{rom: generalities: cfi constraints: 0/1 increments} $\romColumnCfi _{i + 1} \in \{ \romColumnCfi _{i}, 1 + \romColumnCfi _{i} \}$
 	\item \If $\romColumnCfi _{i} =    0$ \Then $\flagSum _{i} = 0$
 	\item \If $\romColumnCfi _{i} \neq 0$ \Then $\flagSum _{i} = 1$
-	\item \If $\romColumnCfi _{i} \neq 0$ \Then $\romColumnCfi _{i + 1} = \romColumnCfi _{i} + \done _{i}$
+	\item\label{rom: generalities: cfi constraints: exact increments} \If $\romColumnCfi _{i} \neq 0$ \Then $\romColumnCfi _{i + 1} = \romColumnCfi _{i} + \done _{i}$
 \end{enumerate}
 \saNote{}
 It follows from the above and
 section~(\ref{rom: generalities: flag sum constraints})
 that $\romColumnCfi \equiv 0 \iff \flagSum \equiv 0$
 and once $\romColumnCfi$ is nonzero it is required to remain so until the end of the trace,
-allowing for $0/1$ increments only.
+allowing for $0/1$ increments only,
+(\ref{rom: generalities: cfi constraints: exact increments}).
+
+\saNote{}
+Constraint~(\ref{rom: generalities: cfi constraints: 0/1 increments})
+doesn't follow from
+constraint~(\ref{rom: generalities: cfi constraints: exact increments})
+since that constraint applies to non-padding-rows.

rom/generalities/wght_sum.tex

@@ -8,9 +8,9 @@
 \]
 We impose
 \begin{enumerate}
-    \item \weightedFlagSum{} is \textbf{code-fragment-context-constant}
+    \item \weightedFlagSum{} is \textbf{\cfi{}-constant}
 \end{enumerate}
 \saNote{}
 It follows that both
 \romColumnEmptyCode{} and \romColumnNonemptyCode{} are
-\textbf{code-fragment-context-constant}.
+\textbf{\cfi{}-constant}.