Reintroduce acp_EXISTS / acp_EXISTS_NEW columns for state manager (…

…#97)

hub/consistencies/account/columns.tex

@@ -22,6 +22,8 @@
 		\item $\order{\accCodehashLo\new}$
 		\item $\order{\accCodesize}$
 		\item $\order{\accCodesize\new}$
+		\item $\order{\accExists}$
+		\item $\order{\accExists\new}$
 		\item $\order{\accWarmth}$
 		\item $\order{\accWarmth\new}$
 		\item $\order{\accDeploymentNumber}$
@@ -30,8 +32,6 @@
 		\item $\order{\accDeploymentStatus\new}$
 		\item $\order{\accMarkedForSelfdestruct}$
 		\item $\order{\accMarkedForSelfdestruct\new}$
-		% \item $\order{\accDeploymentNumberFirstInBlock}$
-		% \item $\order{\accDeploymentNumberFinalInBlock}$
 		\item $\order{\accTrmFlag}$
 		\item $\order{\accTrmIsPrecompile}$
 		\item[\vspace{\fill}]
@@ -51,3 +51,12 @@
 		\item $\order{\accDeploymentNumberFinalInBlock}$
 	\end{enumerate}
 \end{multicols}
+\saNote{}
+The row-permuted columns
+$\order{\accExists}$ and
+$\order{\accExists\new}$
+play absolutely no rôle in the sequel.
+They are essentially left unconstrained beyond their definition.
+We include them nonetheless in both specification and implementation as they are used by the wider system in establishing the connection between
+the arithmetization and
+the \textbf{prover's state manager}.

hub/consistencies/account/link.tex

@@ -2,37 +2,38 @@
 \begin{description}
 	\item[\underline{At the conflation level:}]
 		\If $\accAgainInConflation_{i} = 1$
-		% \[
-		% 	\left\{ \begin{array}{lclc}
-		% 		\order{\peekAccount} _{i} & = & 1  & \et \\
-		% 		\accFirstInConflation_{i} & = & 0 \\
-		% 	\end{array} \right.
-		% \]
 		\Then we impose that
 		\[
-			\left\{ \begin{array}{lcl}
-				\order{\accNonce            }_{i} & = & \order{\accNonce               \new }_{i - 1}              \\
-				\order{\accBalance          }_{i} & = & \order{\accBalance             \new }_{i - 1}              \\
-				\order{\accCodesize         }_{i} & = & \order{\accCodesize            \new }_{i - 1}              \\
-				\order{\accCodehashHi       }_{i} & = & \order{\accCodehashHi          \new }_{i - 1}              \\
-				\order{\accCodehashLo       }_{i} & = & \order{\accCodehashLo          \new }_{i - 1}              \\
-				\order{\accDeploymentNumber }_{i} & = & \order{\accDeploymentNumber    \new }_{i - 1}              \\
-				\order{\accDeploymentStatus }_{i} & = & \order{\accDeploymentStatus    \new }_{i - 1} \vspace{2mm} \\
+			\left\{ \begin{array}{lclr}
+				\order{\accNonce            } _{i} & = & \order{\accNonce            \new } _{i - 1}              \\
+				\order{\accBalance          } _{i} & = & \order{\accBalance          \new } _{i - 1}              \\
+				\order{\accCodesize         } _{i} & = & \order{\accCodesize         \new } _{i - 1}              \\
+				\order{\accCodehashHi       } _{i} & = & \order{\accCodehashHi       \new } _{i - 1}              \\
+				\order{\accCodehashLo       } _{i} & = & \order{\accCodehashLo       \new } _{i - 1}              \\
+				\order{\accDeploymentNumber } _{i} & = & \order{\accDeploymentNumber \new } _{i - 1}              \\
+				\order{\accDeploymentStatus } _{i} & = & \order{\accDeploymentStatus \new } _{i - 1} \vspace{2mm} \\
+				\order{\accExists           } _{i} & = & \order{\accExists           \new } _{i - 1}               & (\trash) \\
 			\end{array} \right.
 		\]
+		\saNote{}
+		There really is no need to enforce linking constraints between $\order{\accExists}$ and $\order{\accExists \new}$
+		which is why we label that constraints with $(\trash)$.
+		Indeed, both $\accExists$ and $\accExists \new$ are completely defined in terms of various account columns.
+		Their row-permuted counterparts are therefore also completely defined by (the row-permuted counterparts of) these same account columns,
+		which are already subject to linking constraints.
+
 		We further impose
 		\[
-			\order{\accTrmIsPrecompile}_{i} = \order{\accTrmIsPrecompile}_{i - 1}
+			\left\{ \begin{array}{lclr}
+				\order{\accTrmIsPrecompile}_{i}   & = & \order{\accTrmIsPrecompile} _{i - 1} \\
+			\end{array} \right.
 		\]
-		\saNote{} This last constraint is less of a ``linking'' constraint an more of an ``address-constancy'' condition for \accTrmIsPrecompile{}.
+		\saNote{}
+		The constraint pertaining to $\accTrmIsPrecompile$ is less of a ``linking-constraint''
+		than an ``address-constancy'' constraint.
+
 	\item[\underline{At the block level:}]
 		\If $\accAgainInBlock_{i} = 1$
-		% \[
-		% 	\left\{ \begin{array}{lclc}
-		% 		\order{\peekAccount} _{i} & = & 1  & \et \\
-		% 		\accFirstInBlock     _{i} & = & 0 \\
-		% 	\end{array} \right.
-		% \]
 		\Then we impose that
 		\[
 			\left\{ \begin{array}{lcl}
@@ -42,12 +43,6 @@
 		\]
 	\item[\underline{At the transaction level:}]
 		\If $\accAgainInTransaction_{i} = 1$
-		% \[
-		% 	\left\{ \begin{array}{lclc}
-		% 		\order{\peekAccount}   _{i} & = & 1  & \et \\
-		% 		\accFirstInTransaction _{i} & = & 0 \\
-		% 	\end{array} \right.
-		% \]
 		\Then we impose
 		\begin{enumerate}
 			\item $\order{\accWarmth}_{i}                = \order{\accWarmth\new}_{i                - 1} $