ROM revision --- deeper changes

hub/lookups/into_rom_jump_destination_vetting.tex

@@ -15,7 +15,7 @@
 			\begin{enumerate}
 				\item \cfi{}
 				\item \pc{}
-				\item \ISVALIDJUMPDESTINATION{}
+				\item \opcodeIsJumpDest{}
 			\end{enumerate}
 		\end{multicols}
 \end{description}

mxp/version.md

@@ -1 +1 @@
-previously called `mxp_v2`
+`mxp_v2`

pkg/common.sty

@@ -293,7 +293,7 @@
 \newcommand{\constraints}         {\mathcal{C}}
 \newcommand{\fullConstraints}     {\constraints\zkEvm}
 \newcommand{\true}                {\texttt{\yellow{<true>}}}
-\newcommand{\false}               {\texttt{\gray{<false>}}}
+\newcommand{\false}               {\texttt{\gray{<faux>}}}
 \newcommand{\mTrue}               {\mathtt{true}}
 \newcommand{\mFalse}              {\mathtt{false}}
 

pkg/rom.sty

@@ -3,7 +3,7 @@
 \newcommand{\ct}{\col{CT}}
 \newcommand{\maxCt}{\col{CT\_MAX}}
 
-\newcommand{\CS}{\col{CODESIZE}}
+\newcommand{\CS}{\col{CODE\_SIZE}}
 \newcommand{\cs}{\col{CS}}
 
 % \newcommand{\DCS}{\Delta\col{\_CODESIZE}}
@@ -22,7 +22,7 @@
 \newcommand{\opc}{\col{OPCODE}}
 \newcommand{\pc}{\col{PC}}
 
-\newcommand{\CSR}{\col{CODESIZE\_REACHED}}
+\newcommand{\CSR}{\col{CODE\_SIZE\_REACHED}}
 \newcommand{\csr}{\col{CSR}}
 
 \newcommand{\IBC}{\col{IS\_BYTE\_CODE}}
@@ -64,18 +64,21 @@
 \newcommand{\keyl}{\col{KEY}\low}
 
 % push related
-\newcommand{\PP}{\col{PUSH\_CT\_MAX}}
+\newcommand{\CP}{\col{PUSH\_COUNTER}}
+\newcommand{\cp}{\col{PUSH\_CT}}
+
+\newcommand{\PP}{\col{PUSH\_COUNTER\_MAX}}
 \newcommand{\pp}{\col{PP}}
 
 \newcommand{\PV}{\col{PUSH\_VALUE}}
 \newcommand{\pv}{\col{PV}}
 
-\newcommand{\IP}{\col{IS\_PUSH\_INST}} % TODO IS\_PUSH
+\newcommand{\IP}{\col{OPCODE\_IS\_PUSH}} % TODO IS\_PUSH
 \newcommand{\ip}{\col{IPI}}
 \newcommand{\IRP}{\col{IS\_RAW\_PUSH}} % TODO IS\_PUSH
 \newcommand{\irp}{\col{IRPI}}
 
-\newcommand{\IJD}{\col{IS\_JUMPDEST}} % TODO IS\_PUSH
+\newcommand{\IJD}{\col{OPCODE\_IS\_JUMPDEST}} % TODO IS\_PUSH
 \newcommand{\ijd}{\col{IJD}}
 \newcommand{\IRJD}{\col{IS\_RAW\_JUMPDEST}} % TODO IS\_PUSH
 \newcommand{\irjd}{\col{IRJD}}
@@ -100,12 +103,38 @@
 \newcommand{\isinitcode}{\col{IS\_INITCODE}}
 \newcommand{\deploymentSuccess}{\col{DEPLOYMENT\_SUCCESSFUL}}
 
-\newcommand{\ISVALIDJUMPDESTINATION}{\col{IS\_VALID\_JUMP\_DESTINATION}}
+\newcommand{\opcodeIsJumpDest}{\col{OPCODE\_IS\_JUMPDEST}}
 \newcommand{\isValidJumpDestination}{\col{VJD}}
 
-\newcommand{\CP}{\col{PUSH\_COUNTER}}
-\newcommand{\cp}{\col{PUSH\_CT}}
-
 \newcommand{\ctMax}{\col{CT\_MAX}}
 
 \newcommand{\nBytesAcc}{\col{nBYTES\_ACC}}
+
+\newcommand{\romColumn}[1]                 {\col{#1}}
+\newcommand{\romColumnEmptyCode}           {\romColumn{EMPTY\_CODE}}
+\newcommand{\romColumnNonemptyCode}        {\romColumn{NONEMPTY\_CODE}}
+\newcommand{\romColumnCFI}                 {\romColumn{CODE\_FRAGMENT\_INDEX}}
+\newcommand{\romColumnCFImax}              {\romColumn{CODE\_FRAGMENT\_INDEX\_MAX}}
+\newcommand{\romColumnCfi}                 {\romColumn{CFI}}
+\newcommand{\romColumnCfiMax}              {\romColumn{CFI\_MAX}}
+\newcommand{\romColumnCodeSize}            {\romColumn{CODE\_SIZE}}
+\newcommand{\romColumnPadding}             {\romColumn{PADDING}}
+\newcommand{\romColumnProgramCounter}      {\romColumn{PROGRAM\_COUNTER}}
+\newcommand{\romColumnLimb}                {\romColumn{LIMB}}
+\newcommand{\romColumnLimbByte}            {\romColumn{LIMB\_BYTE}}
+\newcommand{\romColumnLimbAcc}             {\romColumn{LIMB\_ACC}}
+\newcommand{\romColumnLimbByteSize}        {\romColumn{LIMB\_SIZE}}
+\newcommand{\romColumnLimbByteSizeAcc}     {\romColumn{LIMB\_SIZE\_ACC}}
+\newcommand{\romColumnLimbIndex}           {\romColumn{LIMB\_INDEX}}
+\newcommand{\romColumnOpcode}              {\romColumn{OPCODE}}
+\newcommand{\romColumnOpcodeIsPush}        {\romColumn{OPCODE\_IS\_PUSH}}
+\newcommand{\romColumnOpcodeIsJumpDest}    {\romColumn{OPCODE\_IS\_JUMPDEST}}
+\newcommand{\romColumnClaimedByPush}       {\romColumn{CLAIMED\_BY\_PUSH}}
+\newcommand{\romColumnPushCounter}         {\romColumn{PUSH\_COUNTER}}
+\newcommand{\romColumnPushCounterMax}      {\romColumn{PUSH\_COUNTER\_MAX}}
+\newcommand{\romColumnPushValue}           {\romColumn{PUSH\_VALUE}}
+\newcommand{\romColumnPushValueHi}         {\romColumn{PUSH\_VALUE\_HI}}
+\newcommand{\romColumnPushValueLo}         {\romColumn{PUSH\_VALUE\_LO}}
+\newcommand{\romColumnPushValueAcc}        {\romColumn{PUSH\_VALUE\_ACC}}
+\newcommand{\romColumnPushFunnelBit}       {\romColumn{PUSH\_FUNNEL\_BIT}}
+

rlp_txn/version.md

@@ -1 +1 @@
-previously called `rlp_txn_v2`
+`rlp_txn_v2`

rom/_all_rom.tex

@@ -1,4 +1,4 @@
-\documentclass{article}
+\documentclass[fleqn]{article}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{xkeyval}
 \usepackage{fontspec}
@@ -32,6 +32,8 @@
 \usepackage{../pkg/rlp_tx}
 \usepackage{../pkg/rlp_patterns}
 \usepackage{../pkg/log_info}
+\usepackage{../pkg/system}
+\usepackage{../pkg/iomf_done}
 
 \usepackage{../pkg/draculatheme}
 

rom/_inputs.tex

@@ -1,9 +1,10 @@
 \input{_local}
 \section{The \romMod{} module}                                   \label{rom}
 \subsection{Introduction}                                        \label{rom: intro}                        \input{intro}
+\subsection{Byte code}                                           \label{rom: byte code}                    \input{byte_code}
 \subsection{Convention}                                          \label{rom: convention}                   \input{convention}
 \subsection{Column description}                                  \label{rom: columns}                      \input{columns}
 \subsection{Generalities}                                        \label{rom: constraints}                  \input{generalities/_inputs}
-\subsection{Connecting \pbcb{} to \opc{} and related flags}      \label{rom: opcode related constraints}   \input{opcode/_inputs}
+\subsection{Connecting \romColumnLimbByte{} to \romColumnOpcode{} and related flags}      \label{rom: opcode related constraints}   \input{opcode/_inputs}
 \subsection{\inst{PUSH} related constraints}                     \label{rom: push related constraints}     \input{push/_inputs}
 \subsection{Instruction decoding}                                \label{rom: instruction decoding}         \input{lookups/rom_into_instruction_decoder}

rom/_local.tex

@@ -1,5 +1,8 @@
-\def\rOne     {\red{1}}
+\def\rOne     {\yellowm{1}}
 \def\gZero    {\graym{0}}
 \def\gz       {{\color{gray!60}\mathtt{0x\,0}}}
 \def\qmda     {{\color{gray!60}\overset{\displaystyle\vdots}?}} % Question Mark Dots Above
 \def\qmdb     {{\color{gray!60}\underset{\displaystyle\vdots}?}} % Question Mark Dots Bbove
+
+\def\weightedCodeTypeSum {\col{wght\_code\_type\_sum}}
+\def\codeTypeSum         {\col{code\_type\_sum}}

rom/byte_code.tex

@@ -0,0 +1,28 @@
+As already mentioned numerous times,
+the \romMod{}-module only processes \textbf{nonempty} byte code.
+This byte code is systematically right-padded with anywhere from $\evmWordSize$ to $\evmWordSize + \llargeMO$
+zero bytes ($\texttt{0x00}$).
+To be precise, the present module artificially appends $\evmWordSize + r$ many zero bytes to the byte code,
+where $r \in \{ 0, 1, \dots, \llargeMO \}$ is uniquely characterized by
+the requirement that
+\[
+  \romColumnCodeSize + r \equiv 0 \mod \llarge
+\]
+Those extraneous ``padding'' bytes are useful for constructing
+$\romColumnPushValue$'s in a uniform way.
+(I.e. in the same manner whether or not \inst{PUSHX} instructions in the byte code
+are followed by $\col{X}$ bytes belonging to the byte code proper or whether
+$\col{X}$ bytes following that opcode would overflow the bytecode,
+i.e. when the bytecode terminates on a \inst{PUSHX} instruction
+followed by $0 \leq \col{Y} < \col{X}$ bytes in the byte code \emph{per se}.)
+
+\saNote{}
+Those ``padding'' bytes don't pollute the bytecode as stored in the state.
+The binary column \romColumnPadding{} serves as a means to distinguish
+between bytes belonging to the byte code and padding bytes.
+This binary column is in particular used to filter out extraneous zeros
+when the prover proceeds to \inst{KECCAK}-hash the bytecode.
+
+\includepdf[fitpaper=true, pages={1}]{lua/byte_code.pdf}
+\includepdf[fitpaper=true, pages={1}]{lua/padding_zero.pdf}
+\includepdf[fitpaper=true, pages={1}]{lua/padding_nonzero.pdf}

rom/columns.tex

@@ -1,51 +1,66 @@
 The following column is used for book-keeping of different code fragments within the \romMod{} module.
 \begin{enumerate}
-    \item \CFI{}:
+    \item \romColumnEmptyCode{} and \romColumnNonemptyCode{}:
+	code-fragment-index-constant binary columns;
+    \item \romColumnCFI{}:
 	code-fragment-constant column;
 	an unique (block)-identifier of a code fragment;
-	abbreviated to \cfi{};
-    \item $\cfiMax$:
+	abbreviated to \romColumnCfi{};
+    \item $\romColumnCFImax$:
 	conflation-wide maximal code fragment index;
-    \item \CS{}:
+	abbreviated to
+	$\romColumnCfiMax$;
+    \item \romColumnCodeSize{}:
 	a code-fragment-constant column containing the code size of the bytecode currently being loaded into \romMod{} module;
-	abbreviated to \cs{};
-    \item \CSR{}:
-	a binary column that equals $0$ at the onset of a given bytecode and reaches 1 at the point where $\pc_i=\CS_i$;
-	abbreviated to \csr{};
-    \item \pc{}:
+	abbreviated to \romColumnCodeSize{};
+    \item \romColumnPadding{}:
+	a binary column that equals $0$ at the onset of a given bytecode and reaches 1 at the point where $\romColumnProgramCounter _{i} = \romColumnCodeSize _{i}$;
+    \item \romColumnProgramCounter{}:
 	program counter (i.e. index of the byte in the current bytecode);
-    \item \index{}:
-	contains the index of the current \limb{};
-	starts counting at $0$;
+    \item \done{}:
+	binary column marking the final row of a given byte code;
     \item \ct{}:
 	a periodic counter;
 	it counts up from $0$ to \ctMax{} in increments of 1 and resets;
     \item \ctMax{}:
 	a \ct{}-constant colomn, gives the high bound of \ct{};
-    \item \limb{}:
-	contains $\llarge$-byte slices of (right zero padded) bytecode;
-    \item \nBytes{}:
-	number of non-padded bytes of the \limb;
-    \item \nBytesAcc{}:
-	an accumulator for \nBytes{};
-    \item \ACC{}:
-	accumulate the \pbcb{} bytes;
+    \item \romColumnLimbIndex{}:
+	contains the index of the current \romColumnLimb{};
+	starts counting at $0$;
+    \item \romColumnLimb{}:
+	contains $\llarge$-byte slices of (left aligned and right zero padded) bytecode;
+    \item \romColumnLimbAcc{}:
+	accumulate the \romColumnLimbByte{} bytes;
+    \item \romColumnLimbByte{}:
+	raw byte from the \romColumnLimb{};
+	the \romColumnLimbByte{} column lists the bytes from said bytecode one by one as well as some extraneous \texttt{0x00}'s beyond the \romColumnCodeSize{} (padding);
+    \item \romColumnLimbByteSize{}:
+	number of non-padded bytes of the \romColumnLimb;
+    \item \romColumnLimbByteSizeAcc{}:
+	an accumulator for \romColumnLimbByteSize{};
 \end{enumerate}
-The \pbcb{} column gets instruction decoded in the \idMod{} module.
+The \romColumnLimbByte{} column contains the raw bytes that make up byte code.
+The \romColumnOpcode{} column is deduced from that and gets instruction decoded in the \idMod{} module.
 These are the columns that the \romMod{} extracts from it:
 \begin{enumerate}[resume]
-    \item \PBCB{}:
-	raw byte from the \limb{};
-	the \pbcb{} column lists the bytes from said bytecode one by one as well as some extraneous \texttt{0x00}'s beyond the \CS{} (padding);
-	abbreviated to \pbcb{};
-    \item \IRP{}:
-	instruction decoded binary flag;
-	lights up for every \pbcb{} whose numeric value matches that of a \inst{PUSHX} instructions\footnote{that is, is in the range $[\![\, \texttt{0x60} , ~ \texttt{0x7f} \,]\!]$};
-	abbreviated to \irp{};
-    \item \IRJD{}:
-	instruction decoded binary flag;
-	lights up for every \pbcb{} whose numeric value matches that of the \inst{JUMPDEST} instruction\footnote{that is, \texttt{0x5b}};
-	abbreviated to \irjd{};
+    \item \romColumnOpcode{}:
+	the opcode associated to the \romColumnLimbByte{};
+	depends on the the context i.e. on whether the byte is shadowed by a \inst{PUSH} instruction (i.e. \( \romColumnClaimedByPush{} = 1 \)) and whether the \romColumnPadding{} flag is on (at which point we impose $\romColumnLimbByte = \romColumnOpcode = \texttt{0x00}$);
+	in all other circumstances \( \romColumnOpcode{} = \romColumnLimbByte{} \);
+    \item \romColumnOpcodeIsPush{}:
+	lights up precisely when
+	$\romColumnOpcode \equiv \inst{PUSHX}$\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}
+	for some $\inst{X}$;
+	abbreviated to \ip{};
+    \item \romColumnOpcodeIsJumpDest{}:
+	lights up precisely when $\romColumnOpcode \equiv \inst{JUMPDEST}$;
+	abbreviated to \isValidJumpDestination{};
+    \item \romColumnClaimedByPush{}:
+	binary flag;
+	lights up for the $\inst{X}$ rows following a \inst{PUSHX} instruction;
+	selects those bytes from the bytecode that contribute to the \inst{PUSH} instruction's $\romColumnPushValueHi$ or $\romColumnPushValueLo$;
+	also sets the \romColumnOpcode{} of said lines to \inst{INVALID};
+	abbreviated to \romColumnClaimedByPush{};
 \end{enumerate}
 The following columns relate to the processing of \inst{PUSHX} instructions.
 \begin{enumerate}[resume]
@@ -55,41 +70,21 @@
     \item \CP{}:
 	counter which counts from $1$ to \PP{} while processing a \inst{PUSHX} instruction;
 	otherwise its value is $0$;
-    \item \PV\HIGH{} and \PV\LOW{}:
+    \item \romColumnPushValueHi{} and \romColumnPushValueLo{}
 	high and low part of the value that a push instruction pushes on stack;
 	abbreviated to $\pv\high$ and $\pv\low$ respectively;
     \item \PVA:
-	``accumulator'' variables used to construct $\PV\HIGH$ and $\PV\LOW$ byte by byte out of ``data carrying bytes'';
+	``accumulator'' variables used to construct $\romColumnPushValueHi$ and $\romColumnPushValueLo$ byte by byte out of ``data carrying bytes'';
 	abbreviated to $\pva$;
     \item \PFB{}:
-	a binary flag that matters for correctly contructing \PV\HIGH{} and \PV\LOW{};
+	a binary flag that matters for correctly contructing \romColumnPushValueHi{} and \romColumnPushValueLo{};
 	abbreviated to \pfb{};
 \end{enumerate}
-
 The columns below are related to the bytecode itself: the bytes that make it up, how to interpret them (i.e. do they code for instructions or are they data carriers for a \inst{PUSHX} instruction?), how much to pad with \texttt{0x00}'s etc\dots:
-\begin{enumerate}[resume]
-    \item \opc{}:
-	the opcode associated to the \pbcb{};
-	depends on the the context i.e. on whether the byte is shadowed by a \inst{PUSH} instruction (i.e. \( \ipd{}=1 \)) and whether the \CSR{} flag is on (at which point we impose $\pbcb=\opc=\texttt{0x00}$);
-	in all other circumstances \( \opc{} = \PBCB{} \);
-    \item \IP{}:
-	lights up precisely when
-	$\opc \equiv \inst{PUSHX}$\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}
-	for some $\inst{X}$;
-	abbreviated to \ip{};
-    \item \IPD{}:
-	binary flag;
-	lights up for the $\inst{X}$ rows following a \inst{PUSHX} instruction;
-	selects those bytes from the bytecode that contribute to the \inst{PUSH} instruction's $\PV\HIGH$ or $\PV\LOW$;
-	also sets the \opc{} of said lines to \inst{INVALID};
-	abbreviated to \ipd{};
-    \item \ISVALIDJUMPDESTINATION{}:
-	lights up precisely when $\opc \equiv \inst{JUMPDEST}$;
-	abbreviated to \isValidJumpDestination{};
-\end{enumerate}
+
 \saNote{}
-The \opc{} and \pbcb{} columns differ in that bytes that are ``obscured'' by a previous \inst{PUSHX} opcode
-will appear unaltered in the \pbcb{} column, but altered to \inst{INVALID} in the \opc{} column, see section~(\ref{rom: opcode: opcode from padded byte code byte}).
+The \romColumnOpcode{} and \romColumnLimbByte{} columns differ in that bytes that are ``obscured'' by a previous \inst{PUSHX} opcode
+will appear unaltered in the \romColumnLimbByte{} column, but altered to \inst{INVALID} in the \romColumnOpcode{} column, see section~(\ref{rom: opcode: opcode from padded byte code byte}).
 As such the above precisely recognizes valid jump destinations as specified in the \cite{EYP-London}.
 
 \saNote{}
@@ -98,13 +93,13 @@
 doesn't deal with the \inst{PUSH0} instruction of \cite{EIP-3855} as it does with
 \inst{PUSHX} instructions\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}.
 For one, it doesn't construct a ``push value'' for \inst{PUSH0} instructions.
-As a consequence, the \inst{PUSH0} opcode \textbf{does not raise} the \IP{} flag while the other \inst{PUSHX} instructions do,
+As a consequence, the \inst{PUSH0} opcode \textbf{does not raise} the \romColumnOpcodeIsPush{} flag while the other \inst{PUSHX} instructions do,
 see diagram~(\ref{rom: instruction decoding: relevant portion of ID module}).
 
 \saNote{}
 \label{rom: columns: push values for PUSH0 vs PUSHX in the HUB}
 Given that the ``push value'' of a \inst{PUSH0} instruction is zero by definition,
 the \hubMod{} module knows to push \inst{0x\,00} to the stack for that opcode,
 see section~(\ref{hub: instruction handling: push pop: setting result to zero for PUSH0}).
-For \inst{PUSHX} instructions the \hubMod{} module is reliant on the $\PV$ constructed in the present module,
+For \inst{PUSHX} instructions the \hubMod{} module is reliant on the $\romColumnPushValue$ constructed in the present module,
 see section~(\ref{hub: instruction handling: push pop: setting result to push value for PUSHX}).

rom/convention.tex

@@ -1,5 +1,6 @@
 \label{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0}
-Throughout the specification of the \romMod{} module, whenever we write
-``\inst{PUSHX}'' we will \textbf{always} be talking about the case where $\inst{X} \neq \inst{0}$, i.e. with $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$.
+Throughout the specification of the \romMod{} module, whenever we write ``\inst{PUSHX}''
+we will \textbf{always} be talking about the case where $\inst{X} \neq \inst{0}$,
+i.e. with $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \evmWordSize \}$.
 The \inst{PUSH0} instruction of \cite{EIP-3855} is dealt with differently than the other \inst{PUSHX} instructions,
 see section~(\ref{rom: columns: IS_PUSH_FLAG does not light up for PUSH0}) for more details.