diff --git a/hub/lookups/into_rom_jump_destination_vetting.tex b/hub/lookups/into_rom_jump_destination_vetting.tex index 96b6d5b1..9e6569a6 100644 --- a/hub/lookups/into_rom_jump_destination_vetting.tex +++ b/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} diff --git a/mxp/version.md b/mxp/version.md index 3b0b14f9..60c2fadf 100644 --- a/mxp/version.md +++ b/mxp/version.md @@ -1 +1 @@ -previously called `mxp_v2` +`mxp_v2` diff --git a/pkg/common.sty b/pkg/common.sty index 4d229485..e6cd32c6 100644 --- a/pkg/common.sty +++ b/pkg/common.sty @@ -293,7 +293,7 @@ \newcommand{\constraints} {\mathcal{C}} \newcommand{\fullConstraints} {\constraints\zkEvm} \newcommand{\true} {\texttt{\yellow{}}} -\newcommand{\false} {\texttt{\gray{}}} +\newcommand{\false} {\texttt{\gray{}}} \newcommand{\mTrue} {\mathtt{true}} \newcommand{\mFalse} {\mathtt{false}} diff --git a/pkg/rom.sty b/pkg/rom.sty index f50d1d91..d4b05edd 100644 --- a/pkg/rom.sty +++ b/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}} + diff --git a/rlp_txn/version.md b/rlp_txn/version.md index 2b375734..a4ee985f 100644 --- a/rlp_txn/version.md +++ b/rlp_txn/version.md @@ -1 +1 @@ -previously called `rlp_txn_v2` +`rlp_txn_v2` diff --git a/rom/_all_rom.tex b/rom/_all_rom.tex index 8eaf6cf7..5e37b0d6 100644 --- a/rom/_all_rom.tex +++ b/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} diff --git a/rom/_inputs.tex b/rom/_inputs.tex index c9e5a42c..d5a602dd 100644 --- a/rom/_inputs.tex +++ b/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} diff --git a/rom/_local.tex b/rom/_local.tex index 4818770e..064b3ca6 100644 --- a/rom/_local.tex +++ b/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}} diff --git a/rom/byte_code.tex b/rom/byte_code.tex new file mode 100644 index 00000000..7739a47a --- /dev/null +++ b/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} diff --git a/rom/columns.tex b/rom/columns.tex index 42cfcce3..bdb76dd0 100644 --- a/rom/columns.tex +++ b/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,7 +93,7 @@ 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{} @@ -106,5 +101,5 @@ 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}). diff --git a/rom/convention.tex b/rom/convention.tex index 50e147ec..edc3d09a 100644 --- a/rom/convention.tex +++ b/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. diff --git a/rom/generalities/_inputs.tex b/rom/generalities/_inputs.tex index 295259da..a549f1b4 100644 --- a/rom/generalities/_inputs.tex +++ b/rom/generalities/_inputs.tex @@ -1,9 +1,19 @@ -\subsubsection{Binarity constraints} \label{rom: generalities: binarities} \input{generalities/binarities} -\subsubsection{Bytehood} \label{rom: generalities: bytehood} \input{generalities/bytehood} -\subsubsection{Constancy constraints} \label{rom: generalities: constancies} \input{generalities/constancies} -\subsubsection{Heartbeat} \label{rom: generalities: heartbeat} \input{generalities/heartbeat} -\subsubsection{\PC{} constraints} \label{rom: generalities: program counter} \input{generalities/program_counter} -\subsubsection{\CSR{} constraints} \label{rom: generalities: code size reached} \input{generalities/codesize_reached} -\subsubsection{\nBytes{} constraints} \label{rom: generalities: nBytes} \input{generalities/nBytes} -\subsubsection{\index{} constraints} \label{rom: generalities: index} \input{generalities/index} -\subsubsection{End of the \cfi{}} \label{rom: generalities: end of cfi} \input{generalities/end_of_cfi} +\subsubsection{Constancy constraints} \label{rom: generalities: constancies} \input{generalities/constancies} +\subsubsection{Binarity constraints} \label{rom: generalities: binarities} \input{generalities/binarities} +\subsubsection{Bytehood constraints} \label{rom: generalities: bytehood} \input{generalities/bytehood} +\subsubsection{\flagSum{} constraints} \label{rom: generalities: flag sum constraints} \input{generalities/flag_sum} +\subsubsection{\weightedFlagSum{} constraints} \label{rom: generalities: weighted flag sum constraints} \input{generalities/wght_sum} +\subsubsection{\romColumnCfiMax{} constraints} \label{rom: generalities: cfi max constraints} \input{generalities/cfi_max} +\subsubsection{\romColumnCfi{} constraints} \label{rom: generalities: cfi constraints} \input{generalities/cfi} +\subsubsection{\done{} constraints} \label{rom: generalities: done constraints} \input{generalities/done} +\subsubsection{\romColumnEmptyCode{} and \romColumnNonemptyCode{} constraints} \label{rom: generalities: empty and nonempty code} \input{generalities/empty_vs_nonempty} +\subsubsection{\ct{} and \maxCt{} constraints} \label{rom: generalities: ct and ct max constraints} \input{generalities/ct_and_ct_max} +\subsubsection{Heartbeat} \label{rom: generalities: heartbeat} \input{generalities/heartbeat} +\subsubsection{\romColumnLimb{}, \romColumnLimbAcc{} and \romColumnLimbByte{} constraints} \label{rom: generalities: limb byte accumulation} \input{generalities/limb_byte_accumulation} +\subsubsection{\romColumnLimbByteSize{} and \romColumnLimbByteSizeAcc{} constraints} \label{rom: generalities: limb byte size and acc} \input{generalities/limb_size_accumulation} +\subsubsection{\romColumnProgramCounter{} constraints} \label{rom: generalities: program counter} \input{generalities/program_counter} +\subsubsection{\romColumnPadding{} constraints} \label{rom: generalities: padding constraints} \input{generalities/padding} +\subsubsection{\romColumnLimbIndex{} constraints} \label{rom: generalities: index} \input{generalities/limb_index} +\subsubsection{End of the \romColumnCfi{}} \label{rom: generalities: end of cfi} \input{generalities/end_of_cfi} +\subsubsection{Vanishing in trace padding constraints} \label{rom: generalities: vanishing in trace padding} \input{generalities/vanishing} + diff --git a/rom/generalities/binarities.tex b/rom/generalities/binarities.tex index 1e37b29c..703dbcb8 100644 --- a/rom/generalities/binarities.tex +++ b/rom/generalities/binarities.tex @@ -1,13 +1,19 @@ The following columns are binary columns: -\begin{multicols}{2} +\begin{multicols}{3} \begin{enumerate} - \item \CSR{} - \item \IPD{} + \item \romColumnPadding{} + \item \romColumnClaimedByPush{} \item \PFB{} - \item \IP{} \quad (\trash) - \item \ISVALIDJUMPDESTINATION{} \quad (\trash) + \item \romColumnEmptyCode {} + \item \romColumnNonemptyCode {} + \item \done {} + \item \romColumnOpcodeIsPush{} (\trash) + \item \romColumnOpcodeIsJumpDest{} (\trash) \item[\vspace{\fill}] \end{enumerate} \end{multicols} \saNote{} -both \IP{} and \ISVALIDJUMPDESTINATION{} 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). diff --git a/rom/generalities/bytehood.tex b/rom/generalities/bytehood.tex index 3865cdd5..57cac948 100644 --- a/rom/generalities/bytehood.tex +++ b/rom/generalities/bytehood.tex @@ -1,12 +1,12 @@ The following columns contain bytes: \begin{multicols}{2} \begin{enumerate} - \item \PBCB{} \quad (\trash) - \item \opc{} \quad (\trash) + \item \romColumnLimbByte {} \quad (\trash) + \item \romColumnOpcode {} \quad (\trash) \end{enumerate} \end{multicols} \saNote{} The bytehood of these columns follows implicitly from the lookup $\romMod \hookrightarrow \idMod$ from section~(\ref{rom: instruction decoding}) -and the derivation of \opc{} from \pbcb{}, see section~(\ref). (\ob{todo: add section reference}) +and the derivation of \romColumnOpcode{} from \romColumnLimbByte{}, see section~(\ref{rom: instruction decoding}). diff --git a/rom/generalities/cfi.tex b/rom/generalities/cfi.tex new file mode 100644 index 00000000..a0447646 --- /dev/null +++ b/rom/generalities/cfi.tex @@ -0,0 +1,21 @@ +We impose +\begin{enumerate} + \item $\romColumnCfi _{0} = 0$ (\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\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, +(\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. diff --git a/rom/generalities/cfi_max.tex b/rom/generalities/cfi_max.tex new file mode 100644 index 00000000..2573b5e4 --- /dev/null +++ b/rom/generalities/cfi_max.tex @@ -0,0 +1,10 @@ +We impose the following constraints on \romColumnCfiMax{}. +\begin{enumerate} + \item \If $\flagSum _{i} = 0$ \Then $\romColumnCfiMax _{i} = 0$ + \item \If $\flagSum _{i} = 1$ \Then $\romColumnCfiMax _{i + 1} = \romColumnCfiMax _{i}$ + % \item \If $\flagSum _{N} = 1$ \Then $\romColumnCfiMax _{N} = \romColumnCfi _{N}$ + \item $\romColumnCfiMax _{N} = \romColumnCfi _{N}$ +\end{enumerate} +\saNote{} +In other words, \romColumnCfiMax{} is unchanging along non-padding-rows +and must coincide with \romColumnCfi{} on the final row of any trace. diff --git a/rom/generalities/code_type.tex b/rom/generalities/code_type.tex new file mode 100644 index 00000000..ab11cc19 --- /dev/null +++ b/rom/generalities/code_type.tex @@ -0,0 +1,6 @@ +\begin{enumerate} +\end{enumerate} +\saNote{} +In the implementation one may replace the two \romColumnCfi{}-constancy conditions with +the single \romColumnCfi{}-constancy condition for \weightedCodeTypeSum{}. + diff --git a/rom/generalities/codesize_reached.tex b/rom/generalities/codesize_reached.tex deleted file mode 100644 index 5f451184..00000000 --- a/rom/generalities/codesize_reached.tex +++ /dev/null @@ -1,20 +0,0 @@ -We impose that \CSR{} equals $0$ while the \pc{} hasn't reached \CS{}. -Once it does, we impose that \csr{} increment to $1$ and stay there until the end of the current \cfi{}. -\begin{enumerate} - \item we impose that \CSR{} be binary (\sanityCheck{}, see section~(\ref{rom: constraints: binarities}); - \item we impose that \CSR{} be \cfi-incrementing; - \item \If $\pc_{i} = \cs_{i} - 1$ \Then $\csr_{i} + \csr_{i + 1}=1$ -\end{enumerate} - -Before \CSR{} switches to one, -we are given with \limb{} -of $\llarge$ bytes, -therefore a $\llarge$ long \ct{}-loop. -After the \CSR{} switches to one, we want at least $\evmWordSize$ padded bytes after, in case the last opcode is a \inst{PUSH32}. -\begin{enumerate}[resume] - \item \If $\cfi_{i} \neq 0$ \et $\ct_{i}=0$ \Then: - \begin{enumerate} - \item \If $\CSR_{i}=0$ \Then $\ctMax_{i} = \llargeMO$ - \item \If $\CSR_{i}=1$ \Then $\ctMax_{i} = \evmWordSizeMO$ - \end{enumerate} -\end{enumerate} diff --git a/rom/generalities/constancies.tex b/rom/generalities/constancies.tex index d30d8892..7ba32300 100644 --- a/rom/generalities/constancies.tex +++ b/rom/generalities/constancies.tex @@ -1,51 +1,51 @@ -A column $\col{X}$ is \textbf{\cfi-constant}\label{def: CFI constant} if it satisfies +A column $\col{X}$ is \textbf{\romColumnCfi{}-constant}\label{def: romColumnCFI constant} if it satisfies \[ - \If ~ \Big(\cfi_i \ne \cfi_{i-1} +1 \Big) ~ \Then \col{X}_{i} = \col{X}_{i-1} + \If ~ \Big(\romColumnCfi _i \neq \romColumnCfi _{i - 1} +1 \Big) ~ \Then \col{X} _{i} = \col{X} _{i - 1} \] -\noindent A column $\col{X}$ is \textbf{\cfi-incrementing}\label{def: CFI incrementing} if it satisfies +\noindent A column $\col{X}$ is \textbf{\romColumnCfi{}-incrementing}\label{def: romColumnCFI incrementing} if it satisfies \[ - \If ~ \Big(\cfi_i \ne \cfi_{i-1} + 1 \Big) ~ \Then \col{X}_{i} \in \{ \col{X}_{i-1} , 1 + \col{X}_{i-1}\} + \If ~ \Big(\romColumnCfi _i \neq \romColumnCfi _{i - 1} + 1 \Big) ~ \Then \col{X} _{i} \in \{ \col{X} _{i - 1} , 1 + \col{X} _{i - 1}\} \] \noindent A column $\col{X}$ is \textbf{counter-constant}\label{def: counter constant} if it satisfies \[ - \If ~ \ct_i \neq \ctMax_{i} ~ \Then \col{X}_{i+1} = \col{X}_{i} + \If ~ \ct _i \neq \ctMax _{i} ~ \Then \col{X} _{i+1} = \col{X} _{i} \] \noindent A column $\col{X}$ is \textbf{push-constant}\label{def: push constant} if it satisfies \[ - \If ~ \CP_i \neq 0 ~ \Then \col{X}_{i} = \col{X}_{i-1} + \If ~ \CP _i \neq 0 ~ \Then \col{X} _{i} = \col{X} _{i - 1} \] \noindent A column $\col{X}$ is \textbf{push-incrementing}\label{def: push incrementing} if it satisfies \[ - \If ~ \CP_i \neq 0 ~ \Then \col{X}_{i} \in \{ \col{X}_{i-1} , 1 + \col{X}_{i-1}\} + \If ~ \CP _i \neq 0 ~ \Then \col{X} _{i} \in \{ \col{X} _{i - 1} , 1 + \col{X} _{i - 1}\} \] -\noindent We require the following columns to be \cfi-constant: +\noindent We require the following columns to be \romColumnCfi{}-constant: \begin{enumerate} - \item \CS{} + \item \romColumnCodeSize{} \end{enumerate} -\noindent We require the following columns to be \cfi-incrementing: +\noindent We require the following columns to be \romColumnCfi{}-incrementing: \begin{enumerate} - \item \pc{} (\ob{done}) - \item \CSR{} (\ob{done}) + \item \romColumnProgramCounter{} (\ob{done}) + \item \romColumnPadding{} (\ob{done}) \end{enumerate} \noindent We require the following columns to be counter-constant: \begin{enumerate} - \item \limb - \item \nBytes + \item \romColumnLimb + \item \romColumnLimbByteSize \item \ctMax \end{enumerate} \noindent We require the following columns to be push-constant: \begin{enumerate} \item \PP{} - \item \PV\HIGH{} - \item \PV\LOW{} + \item \romColumnPushValueHi{} + \item \romColumnPushValueLo{} \end{enumerate} \noindent We require the following columns to be push-incrementing: diff --git a/rom/generalities/ct_and_ct_max.tex b/rom/generalities/ct_and_ct_max.tex new file mode 100644 index 00000000..cab90f72 --- /dev/null +++ b/rom/generalities/ct_and_ct_max.tex @@ -0,0 +1,26 @@ +We impose +\begin{enumerate} + \item \ctMax{} is \textbf{counter-constant} + \item \If $\ct _{i} \neq \maxCt _{i}$ \Then $\ct _{i + 1} = 1 + \ct _{i}$ + \item \If $\ct _{i} = \maxCt _{i}$ \Then $\ct _{i + 1} = 0$ + \item \If $\flagSum _{i} = 0$ \Then + \[ + \left\{ \begin{array}{lcl} + \ct _{i} & = & 0 \\ + \maxCt _{i} & = & 0 \\ + \end{array} \right. + \] + \item \If $\flagSum _{i} = 1$ \Then + \begin{enumerate} + \item $\maxCt _{i} \in \{ \llargeMO, \evmWordSizeMO \}$ (\sanityCheck) + \item \If $\ct _{i} = 0$ \et $\romColumnPadding _{i} = 0$ \Then $\maxCt _{i} = \llargeMO$ + \item \If $\ct _{i} = 0$ \et $\romColumnPadding _{i} = 1$ \Then $\maxCt _{i} = \evmWordSizeMO$ + \end{enumerate} + \item \If $\flagSum _{N} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \ct _{N} & = & \maxCt _{N} \\ + \maxCt _{N} & = & \evmWordSizeMO \\ + \end{array} \right. + \] +\end{enumerate} diff --git a/rom/generalities/done.tex b/rom/generalities/done.tex new file mode 100644 index 00000000..bc8ebd2b --- /dev/null +++ b/rom/generalities/done.tex @@ -0,0 +1,19 @@ +We characterize the \done{} column. We impose +\begin{enumerate} + \item \done{} is binary (\sanityCheck) + \item \If $\flagSum _{i} = 0$ \Then $\done _{i} = 0$ (\sanityCheck) + \item \If $\romColumnEmptyCode _{i} = 1$ \Then $\done _{i} = 1$ + \item \If $\romColumnNonemptyCode _{i} = 1$ \Then + \begin{enumerate} + \item + \If $\ct _{i} \neq \maxCt _{i}$ + \Then $\done _{i} = 0$ + \item + \If $\romColumnPadding _{i} = 0$ + \Then $\done _{i} = 0$ + \item + \If $\ct _{i} = \maxCt _{i}$ + \et $\romColumnPadding _{i} = 1$ + \Then $\done _{i} = 1$ + \end{enumerate} +\end{enumerate} diff --git a/rom/generalities/empty_vs_nonempty.tex b/rom/generalities/empty_vs_nonempty.tex new file mode 100644 index 00000000..8b47a00a --- /dev/null +++ b/rom/generalities/empty_vs_nonempty.tex @@ -0,0 +1,13 @@ +We impose +\begin{enumerate} + \item \romColumnEmptyCode{} and \romColumnNonemptyCode{} are binary (\sanityCheck{}) + \item we impose + \begin{enumerate} + \item \If $\romColumnCodeSize _{i} = 0$ \Then $\romColumnNonemptyCode _{i} = \false $ + \item \If $\romColumnCodeSize _{i} \neq 0$ \Then $\romColumnNonemptyCode _{i} = \true $ + \end{enumerate} +\end{enumerate} +The current iteration of the \romMod{} module only allows for \textbf{nonempty byte code}: +\begin{enumerate}[resume] + \item\label{rom: generalities: code type stuff: empty code is disallowed} we impose $\romColumnEmptyCode _{i} = 0$ +\end{enumerate} diff --git a/rom/generalities/end_of_cfi.tex b/rom/generalities/end_of_cfi.tex index 60c49484..fc193cc8 100644 --- a/rom/generalities/end_of_cfi.tex +++ b/rom/generalities/end_of_cfi.tex @@ -1,9 +1,9 @@ -The constraints below impose that within the padding bytes\footnote{of which there are at least $\evmWordSize{}$ and at most $\evmWordSize + \llargeMO$} the \PBCB's are all zero. This is compatible with the final instruction of a code fragment being some \inst{PUSHX} instruction. +The constraints below impose that within the padding bytes\footnote{of which there are at least $\evmWordSize{}$ and at most $\evmWordSize + \llargeMO$} the \romColumnLimbByte's are all zero. This is compatible with the final instruction of a code fragment being some \inst{PUSHX} instruction. \begin{enumerate} - \item \If $\CSR_{i} = 1$ \Then: + \item \If $\romColumnPadding _{i} = 1$ \Then: \begin{enumerate} - \item $\PBCB_{i}=0$ - \item $\IP_{i}=0$ \quad (\trash) + \item $\romColumnLimbByte _{i} = 0$ + \item $\IP _{i} = 0$ \quad (\trash) \end{enumerate} \end{enumerate} diff --git a/rom/generalities/flag_sum.tex b/rom/generalities/flag_sum.tex new file mode 100644 index 00000000..23f07036 --- /dev/null +++ b/rom/generalities/flag_sum.tex @@ -0,0 +1,27 @@ +We define +\[ + \flagSum _{i} \define + \left[ \begin{array}{cr} + + & \romColumnEmptyCode _{i} \\ + + & \romColumnNonemptyCode _{i} \\ + \end{array} \right] +\] +and we impose +\begin{enumerate} + \item\label{rom: generalities: code type stuff: flag exclusivity} \flagSum{} is \textbf{binary} + \item $\flagSum _{0} = 0$ + \item \If $\flagSum _{i} = 1$ \Then $\flagSum _{i + 1} = 1$ +\end{enumerate} +\saNote{} +Constraint~(\ref{rom: generalities: code type stuff: flag exclusivity}) +means that +\romColumnEmptyCode {} and +\romColumnNonemptyCode {} +are \textbf{binary exclusive}. + +\saNote{} +\flagSum{} is thus \textbf{nondecreasing binary}. + +\saNote{} +We completely characterize \romColumnNonemptyCode{} +in section~(\ref{rom: generalities: empty and nonempty code}). diff --git a/rom/generalities/heartbeat.tex b/rom/generalities/heartbeat.tex index a66383ac..a882d291 100644 --- a/rom/generalities/heartbeat.tex +++ b/rom/generalities/heartbeat.tex @@ -1,56 +1,56 @@ -The $\CFI{}$ acts as a "stamp" of the module: +The $\romColumnCFI{}$ acts as a ``stamp'' of the module: \begin{enumerate} - \item $\cfi_{0}=0$ - \item $\cfi_{i + 1} \in \{ \cfi_{i}, 1 + \cfi_{i} \}$ - \item \If $\cfi_{i}=0$ \Then + \item $\romColumnCfi _{0} = 0$ + \item $\romColumnCfi _{i + 1} \in \{ \romColumnCfi _{i}, 1 + \romColumnCfi _{i} \}$ + \item \If $\romColumnCfi _{i} = 0$ \Then \[ \left\{ \begin{array}{lclr} - \ct_{i} & = & 0 \\ - \ctMax_{i} & = & 0 \\ - \pbcb_{i} & = & 0 \\ - \pc_{i} & = & 0 & (\trash) \\ - \IP_{i} & = & 0 & (\trash) \\ - \IPD_{i} & = & 0 & (\trash) \\ - \CP & = & 0 & (\trash) \\ - \PP & = & 0 & (\trash) \\ - \PC & = & 0 & (\trash) \\ + \ct _{i} & = & 0 \\ + \ctMax _{i} & = & 0 \\ + \romColumnLimbByte _{i} & = & 0 \\ + \romColumnProgramCounter _{i} & = & 0 & (\trash) \\ + \romColumnOpcodeIsPush _{i} & = & 0 & (\trash) \\ + \romColumnClaimedByPush _{i} & = & 0 & (\trash) \\ + \CP _{i} & = & 0 & (\trash) \\ + \PP _{i} & = & 0 & (\trash) \\ + \romColumnProgramCounter _{i} & = & 0 & (\trash) \\ \end{array} \right. \] - \item \If $\cfi_{i} \neq 0$ \Then + \item \If $\romColumnCfi _{i} \neq 0$ \Then \begin{enumerate} - \item $\ctMax_{i} \in \{ \llargeMO, \evmWordSizeMO \}$ (\trash) - \item \If $\ctMax_{i} = \llargeMO$ \Then $\cfi_{i + 1}=\cfi_{i}$ - \item \If $\ct_{i} \ne \ctMax_{i}$ \Then $\cfi_{i + 1}=\cfi_{i}$ - \item \If ($\ctMax_{i} = \evmWordSizeMO$ \et $\ct_{i} = \ctMax_{i}$) \Then $\cfi_{i + 1} = \cfi_{i}+1$ + \item $\ctMax _{i} \in \{ \llargeMO, \evmWordSizeMO \}$ (\trash) + \item \If $\ctMax _{i} = \llargeMO$ \Then $\romColumnCfi _{i + 1} = \romColumnCfi _{i}$ + \item \If $\ct _{i} \neq \ctMax _{i}$ \Then $\romColumnCfi _{i + 1} = \romColumnCfi _{i}$ + \item \If ($\ctMax _{i} = \evmWordSizeMO$ \et $\ct _{i} = \ctMax _{i}$) \Then $\romColumnCfi _{i + 1} = \romColumnCfi _{i}+1$ \end{enumerate} \end{enumerate} -\noindent The \CT{} column imposes cycles of \ctMax{} rows inside each \cfi{}. +\noindent The \CT{} column imposes cycles of \ctMax{} rows inside each \romColumnCfi{}. \begin{enumerate}[resume] - % \item \If $\cfi_{i} \ne 0$ \Then + % \item \If $\romColumnCfi _{i} \neq 0$ \Then % \begin{enumerate} - \item \If $\ct_{i} \neq \ctMax_{i}$ \Then $\ct_{i + 1} = \ct_{i} + 1$, - \item \If $\ct_{i} = \ctMax_{i}$ \Then $\ct_{i + 1} = 0$, + \item \If $\ct _{i} \neq \ctMax _{i}$ \Then $\ct _{i + 1} = \ct _{i} + 1$, + \item \If $\ct _{i} = \ctMax _{i}$ \Then $\ct _{i + 1} = 0$, % \end{enumerate} \end{enumerate} We impose the following constraint on the \textbf{last row}: \begin{enumerate}[resume] - \item \If $\cfi_{N} \neq 0$ \Then - \begin{enumerate} - \item $\ct _{N} = \ctMax_{N}$ - \item $\ctMax_{N} = \evmWordSizeMO$ - \item $\cfi _{N} = \cfiMax_{N}$ - \item $\cp _{N} = \PP_{N}$ - \end{enumerate} + \item \If $\romColumnCfi _{N} \neq 0$ \Then + \begin{enumerate} + \item $\ct _{N} = \ctMax _{N}$ + \item $\ctMax _{N} = \evmWordSizeMO$ + \item $\romColumnCfi _{N} = \romColumnCfiMax _{N}$ + \item $\cp _{N} = \PP _{N}$ + \end{enumerate} \end{enumerate} -And we impose $\cfiMax$ to be constant all along the trace, except during the padding rows: +And we impose $\romColumnCfiMax$ to be constant all along the trace, except during the padding rows: \begin{enumerate}[resume] - \item \If $\cfi_{i} = 0$ \Then $\cfiMax_{i} = 0$ - \item \If $\cfi_{i} \ne 0$ \Then $\cfiMax_{i} =\cfiMax_{i + 1}$ + \item \If $\romColumnCfi _{i} = 0$ \Then $\romColumnCfiMax _{i} = 0$ + \item \If $\romColumnCfi _{i} \neq 0$ \Then $\romColumnCfiMax _{i} = \romColumnCfiMax _{i + 1}$ \end{enumerate} We build an accumulator: \begin{enumerate}[resume] - \item \If $\ct_{i}=0$ \Then $\ACC_{i} = \pbcb_{i}$ - \item \If $\ct_{i} \ne 0$ \Then $\ACC_{i} = 256 \cdot \ACC_{i - 1} + \pbcb_{i}$ - \item \If $\ct_{i} = \ctMax_{i} $ \Then $\ACC_{i} = \limb_{i}$ + \item \If $\ct _{i} = 0$ \Then $\romColumnLimbAcc _{i} = \romColumnLimbByte _{i}$ + \item \If $\ct _{i} \neq 0$ \Then $\romColumnLimbAcc _{i} = 256 \cdot \romColumnLimbAcc _{i - 1} + \romColumnLimbByte _{i}$ + \item \If $\ct _{i} = \ctMax _{i}$ \Then $\romColumnLimbAcc _{i} = \romColumnLimb _{i}$ \end{enumerate} diff --git a/rom/generalities/index.tex b/rom/generalities/index.tex deleted file mode 100644 index 15f2afbd..00000000 --- a/rom/generalities/index.tex +++ /dev/null @@ -1,15 +0,0 @@ - -\begin{enumerate} - \item \If $\cfi_{i} = 0$ \Then $\index_{i}= 0$ - \item \If $\cfi_{i} \neq \cfi_{i-1}$ \Then $\index_{i}= 0$ - \item \If \Big($\cfi_{i} \neq 0$ \et $\cfi_{i} \neq \cfi_{i-1} + 1$ \et $\ct_{i} = 0$\Big) \Then: - \[ \index_{i} = \index_{i-1}+1 \] - \item \If $\ct_{i} = \llarge$ \Then $\index_{i} = \index_{i-1}+1$ - \item \If ($\ct_{i} \ne 0$ \et $\ct_{i} \ne \llarge$) \Then $\index_{i} = \index_{i-1}$ -\end{enumerate} -\saNote{} The condition ``$\ct_{i} = \llarge$'' is only triggered in the zero-padding of bytecode that happens at the end of every code fragment tracing. This constraint imposes that the index grow by one at the expected row. - -\saNote{} The requirement to add two full zero limbs at the end of the code fragment stems from two different reasons: -(\emph{a}) allowing for simple push value construction -(\emph{b}) making the lookup $\rlpTxnMod \hookrightarrow \romMod$ work seamlessly. -The former module indeed appends two padding limbs to the end of initialization code. diff --git a/rom/generalities/limb_byte_accumulation.tex b/rom/generalities/limb_byte_accumulation.tex new file mode 100644 index 00000000..2a1ec38c --- /dev/null +++ b/rom/generalities/limb_byte_accumulation.tex @@ -0,0 +1,15 @@ +We impose +\begin{enumerate} + \item \If $\romColumnNonemptyCode _{i} = 0$ \Then + \[ + \left\{ \begin{array}{lcl} + \romColumnLimb _{i} & = & 0 \\ + \romColumnLimbAcc _{i} & = & 0 \\ + \romColumnLimbByte _{i} & = & 0 \\ + \end{array} \right. + \] + \item \If $\ct _{i} = 0$ \Then $\romColumnLimbAcc _{i} = \romColumnLimbByte _{i}$ + \item \If $\ct _{i} \neq 0$ \Then $\romColumnLimbAcc _{i} = 256 \cdot \romColumnLimbAcc _{i - 1} + \romColumnLimbByte _{i}$ + \item \If $\ct _{i} = \ctMax _{i}$ \Then $\romColumnLimbAcc _{i} = \romColumnLimb _{i}$ +\end{enumerate} + diff --git a/rom/generalities/limb_index.tex b/rom/generalities/limb_index.tex new file mode 100644 index 00000000..5f4ca43e --- /dev/null +++ b/rom/generalities/limb_index.tex @@ -0,0 +1,28 @@ +We impose that +\begin{enumerate} + \item \If $\romColumnNonemptyCode _{i} = \false $ \Then $\romColumnLimbIndex _{i} = 0$ + \item \If $\romColumnNonemptyCode _{i} = \true $ \Then + \begin{enumerate} + \item \If $\romColumnCfi _{i} \neq \romColumnCfi _{i - 1}$ \Then $\romColumnLimbIndex _{i} = 0$ + \item \If $\romColumnCfi _{i} = \romColumnCfi _{i - 1}$ \Then + \begin{enumerate} + \item \If $\ct _{i} = 0$ \Then $\romColumnLimbIndex _{i} = \romColumnLimbIndex _{i - 1} + 1$ + \item \If $\ct _{i} = \llarge$ \Then $\romColumnLimbIndex _{i} = \romColumnLimbIndex _{i - 1} + 1$ + \item \If ($\ct _{i} \neq 0$ \et $\ct _{i} \neq \llarge$) \Then $\romColumnLimbIndex _{i} = \romColumnLimbIndex _{i - 1}$ + \end{enumerate} + \end{enumerate} +\end{enumerate} +\saNote{} +\romColumnLimbIndex{} isn't quite \textbf{counter-constant}. +During the long counter-cycle which concludes a \romColumnNonemptyCode{}-segment +\romColumnLimbIndex{} increments at the $\ct = \llarge$ mark. + +\saNote{} +The condition ``$\ct _{i} = \llarge$'' is only triggered in the zero-padding of bytecode that happens at the end of every code fragment tracing. +This constraint imposes that the index grow by one at the expected row. + +\saNote{} +The requirement to add two full zero limbs at the end of the code fragment stems from two different reasons: +(\emph{a}) allowing for simple push value construction +(\emph{b}) making the lookup $\rlpTxnMod \hookrightarrow \romMod$ work seamlessly. +The former module indeed appends two padding limbs to the end of initialization code. diff --git a/rom/generalities/limb_size_accumulation.tex b/rom/generalities/limb_size_accumulation.tex new file mode 100644 index 00000000..88f95bf0 --- /dev/null +++ b/rom/generalities/limb_size_accumulation.tex @@ -0,0 +1,29 @@ +We impose the following +\begin{enumerate} + \item \romColumnLimbByteSize{} is \textbf{counter-constant} + \item \If $\romColumnNonemptyCode _{i} = \false$ \Then + \[ + \left\{ \begin{array}{lclr} + \romColumnLimbByteSize _{i} & = & 0 & (\trash) \\ + \romColumnLimbByteSizeAcc _{i} & = & 0 & (\trash) \\ + \end{array} \right. + \] + \item \If $\romColumnNonemptyCode _{i} = \true$ \Then: + \begin{enumerate} + \item \If $\ct _{i} = 0$ \Then: + \begin{enumerate} + \item \If $\romColumnPadding _{i} = 0$ \Then $\romColumnLimbByteSizeAcc _{i} = 1$ + \item \If $\romColumnPadding _{i} = 1$ \Then $\romColumnLimbByteSizeAcc _{i} = 0$ + \end{enumerate} + \item \If $\ct _{i} \neq 0$ \Then: + \begin{enumerate} + \item \If $\romColumnPadding _{i} = 0$ \Then $\romColumnLimbByteSizeAcc _{i} = \romColumnLimbByteSizeAcc _{i - 1}+1$ + \item \If $\romColumnPadding _{i} = 1$ \Then $\romColumnLimbByteSizeAcc _{i} = \romColumnLimbByteSizeAcc _{i - 1}$ + \end{enumerate} + \end{enumerate} + \item \If $\ct _{i} = \ctMax _{i}$ \Then $\romColumnLimbByteSizeAcc _{i} = \romColumnLimbByteSize _{i}$ +\end{enumerate} +\saNote{} By construction: +\begin{enumerate}[resume] + \item \romColumnLimbByteSizeAcc{} is \ct-incrementing \quad (\sanityCheck) +\end{enumerate} diff --git a/rom/generalities/nBytes.tex b/rom/generalities/nBytes.tex deleted file mode 100644 index 4709d3ec..00000000 --- a/rom/generalities/nBytes.tex +++ /dev/null @@ -1,21 +0,0 @@ -\begin{enumerate} - \item \If $\cfi_{i} \ne 0$ \Then: - \begin{enumerate} - \item \If $\ct_{i}=0$ \Then: - \begin{enumerate} - \item \If $\CSR_{i}=0$ \Then $\nBytesAcc_{i}=1$ - \item \If $\CSR_{i}=1$ \Then $\nBytesAcc_{i}=0$ - \end{enumerate} - \item \If $\ct_{i} \neq 0$ \Then: - \begin{enumerate} - \item \If $\CSR_{i}=0$ \Then $\nBytesAcc_{i}=\nBytesAcc_{i-1}+1$ - \item \If $\CSR_{i}=1$ \Then $\nBytesAcc_{i}=\nBytesAcc_{i-1}$ - \end{enumerate} - \end{enumerate} - \item \If $\ct_{i}=\ctMax_{i}$ \Then $\nBytesAcc_{i}=\nBytes_{i}$ -\end{enumerate} - -\saNote{} By construction: -\begin{enumerate}[resume] - \item \nBytesAcc{} is CT-incrementing \quad (\trash) -\end{enumerate} diff --git a/rom/generalities/padding.tex b/rom/generalities/padding.tex new file mode 100644 index 00000000..0351baba --- /dev/null +++ b/rom/generalities/padding.tex @@ -0,0 +1,31 @@ +We impose that \romColumnPadding{} equals $0$ while the \romColumnProgramCounter{} hasn't reached \romColumnCodeSize{}. +Once it does, we impose that \romColumnPadding{} increment to $1$ and stay there until the end of the current \romColumnCfi{}. +This (byte code) padding phase can take anywhere from $\evmWordSize$ to $\evmWordSize + \llargeMO$ rows. +\begin{enumerate} + \item we impose that \romColumnPadding{} be binary (\sanityCheck{}) + \item we impose that \romColumnPadding{} be \romColumnCfi{}-incrementing; + \item \If $\flagSum _{i} = 0$ \Then $\romColumnPadding _{i} = 0$; + \item \If $\romColumnCfi _{i} \neq \romColumnCfi _{i - 1}$ \Then $\romColumnPadding _{i} = \romColumnEmptyCode _{i}$ + \item \If $\romColumnNonemptyCode _{i} = 1$ \et $\romColumnProgramCounter _{i} = \romColumnCodeSize _{i} - 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \romColumnPadding _{i} & = & 0 \\ + \romColumnPadding _{i + 1} & = & 1 \\ + \end{array} \right. + \] +\end{enumerate} +\saNote{} +One may compress the two constraints about ``turning on'' the \romColumnPadding{}-bit into the following alternative one: +\[ + \romColumnPadding _{i} + \romColumnPadding _{i + 1} = 1 \quad (\sanityCheck) +\] +The purpose of these constraints is to have $\romColumnPadding \equiv 0$ while ``within the byte code'' +and $\romColumnPadding \equiv 1$ as soon as the ``byte code runs out'' and one enters (byte code) padding territory. + +\saNote{} +Recall that according to +section~(\ref{rom: generalities: ct and ct max constraints}), +for byte code that is \romColumnNonemptyCode{}, +\romColumnLimb{} are initially $\llarge$ bytes long, giving rise to a \ct{}-loops of length $\llarge$. +After the \romColumnPadding{} switches to one the final \ct{}-loop has length $\evmWordSizeMO$. + diff --git a/rom/generalities/program_counter.tex b/rom/generalities/program_counter.tex index 8050ea6e..6ae55dda 100644 --- a/rom/generalities/program_counter.tex +++ b/rom/generalities/program_counter.tex @@ -1,10 +1,13 @@ -The program counter \pc{} is local to a code fragment index. +The program counter \romColumnProgramCounter{} is local to a code fragment index. It starts at $0$ and increases by $1$ with every byte in the code fragment (i.e. padded bytecode). This includes the padding bytes, which are all $\texttt{0x\,}\utt{00}$, that follow the actual byte code. \begin{enumerate} - \item \If $\cfi_{i} = 0$ \Then $\pc_{i} = 0$; - \item \If $\cfi_{i + 1} \neq \cfi_{i}$ \Then $\pc_{i + 1} = 0$ - \item \If \Big($\cfi_{i} \neq 0$ \et $\cfi_{i + 1} \neq 1 + \cfi_{i}$\Big) \Then $\pc_{i + 1} = 1 + \pc_{i}$; + \item \If $\romColumnNonemptyCode _{i} = \false$ \Then $\romColumnProgramCounter _{i} = 0$; + \item \If $\romColumnNonemptyCode _{i} = \true$ \Then + \begin{enumerate} + \item \If $\romColumnCfi _{i} \neq \romColumnCfi _{i - 1}$ \Then $\romColumnProgramCounter _{i + 1} = 0$ + \item \If $\romColumnCfi _{i} = \romColumnCfi _{i - 1}$ \Then $\romColumnProgramCounter _{i + 1} = 1 + \romColumnProgramCounter _{i}$ + \end{enumerate} \end{enumerate} \saNote{} -\pc{} is \emph{de facto} \cfi-incrementing. +\romColumnProgramCounter{} is \emph{de facto} \romColumnCfi{}-incrementing. diff --git a/rom/generalities/vanishing.tex b/rom/generalities/vanishing.tex new file mode 100644 index 00000000..7d0bea7b --- /dev/null +++ b/rom/generalities/vanishing.tex @@ -0,0 +1,25 @@ +We impose the following vanishing conditions: +\begin{enumerate} + \item + \If $\romColumnNonemptyCode _{i} = \false$ \Then + \[ + \left\{ \begin{array}{lclr} + \ct _{i} & = & 0 \\ + \ctMax _{i} & = & 0 \\ + \done _{i} & = & 0 \\ + \romColumnLimb _{i} & = & 0 \\ + \romColumnPadding _{i} & = & \romColumnEmptyCode _{i} \\ + \romColumnLimbByte _{i} & = & 0 & (\trash) \\ + \romColumnOpcode _{i} & = & \inst{STOP} & (\trash) \\ + \romColumnLimbIndex _{i} & = & 0 & (\trash) \\ + \romColumnProgramCounter _{i} & = & 0 & (\trash) \\ + \romColumnOpcodeIsPush _{i} & = & 0 & (\trash) \\ + \romColumnClaimedByPush _{i} & = & 0 & (\trash) \\ + \CP _{i} & = & 0 & (\trash) \\ + \PP _{i} & = & 0 & (\trash) \\ + \romColumnProgramCounter _{i} & = & 0 & (\trash) \\ + \end{array} \right. + \] +\end{enumerate} +\saNote{} +Recall the byte value of the \inst{STOP} opcode: \texttt{0x00}. diff --git a/rom/generalities/wght_sum.tex b/rom/generalities/wght_sum.tex new file mode 100644 index 00000000..4664481f --- /dev/null +++ b/rom/generalities/wght_sum.tex @@ -0,0 +1,16 @@ +We define +\[ + \weightedFlagSum _{i} \define + \left[ \begin{array}{crcr} + + & 2^{0} & \cdot & \romColumnEmptyCode _{i} \\ + + & 2^{1} & \cdot & \romColumnNonemptyCode _{i} \\ + \end{array} \right] +\] +We impose +\begin{enumerate} + \item \weightedFlagSum{} is \textbf{\cfi{}-constant} +\end{enumerate} +\saNote{} +It follows that both +\romColumnEmptyCode{} and \romColumnNonemptyCode{} are +\textbf{\cfi{}-constant}. diff --git a/rom/intro.tex b/rom/intro.tex index 89db2bff..d2a3b01f 100644 --- a/rom/intro.tex +++ b/rom/intro.tex @@ -1,16 +1,34 @@ -The \romMod{} module compiles the \textbf{nonempty} bytecodes, initialization codes and deployed byte codes alike, used during the execution of a conflation of blocks. -Its main role in the overall design is to provide the \hubMod{} module with the correct sequence of instructions. -It furthermore assembles the \inst{PUSH}-values from the bytes following a \inst{PUSHX} instruction, $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$. -It also tags (in)valid jump destinations as such, as is required by \textsc{jump destination analysis}. +The \romMod{} module exposes and processes all pieces of (\textbf{nonempty}) byte code, +initialization codes and deployed byte codes alike, +required by the processing of a conflation of blocks. +Its main role in the overall design is to provide the \hubMod{} module with the correct sequence of instructions, +as well as related pieces of data. +In more detail, the present module +\textbf{performs jump destination analysis} and +\textbf{assembles \inst{PUSH}-values} from the bytes following a \inst{PUSHX} opcode, +for $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \evmWordSize \}$. +Note that \inst{PUSH0}, introduced in \cite{EYP-Shanghai} with \cite{EIP-3855}, is excluded from that list. Most of the arithmetization below focuses on building the \romMod{} module as a seqence of padded byte codes and of extracting the correct push values from it (i.e. the $\inst{X}$-byte long arguments of actual \inst{PUSHX} instructions). -There are three kinds of accesses to bytecode that the \romMod{} module deals with, with contract deployment being subdivided into 1 or 2 phases (since deployments may fail): +What follows is a complete list of events that trigger the \romMod{} module to incorporate byte code into its trace: \begin{enumerate} - \item loading the full bytecode of an already deployed smart contract to \inst{CALL}, \inst{CALLCODE}, \inst{STATICCALL} or \inst{DELEGATECALL} into it; - \item loading the full bytecode of an already deployed smart contract to \inst{EXTCODECOPY} from it; - \item deploying a smart contract through a deployment transaction or an (unexceptional, unaborted and no failure condition raising) \inst{CREATE(2)} instruction: - \begin{enumerate} - \item loading the initialization code into the \romMod{} module; - \item and for (temporarily) successful deployments loading the bytecode that will be (temporarily) deployed at the relevant address into the \romMod{} module. - \end{enumerate} + \item + \user{}-transaction processing whose $\loc{addr} \equiv \col{tx.toAddress()} \neq \varnothing$ has nonempty byte code; + the \romMod{} module loads the byte code $\mathbf{b}$ from the state, + where $\texttt{KECCAK}(\mathbf{b}) = \bm{\sigma}\big[ \loc{addr} \big]_c$; + \item + similarly for unexceptional \inst{CALL}'s, \inst{CALLCODE}'s, \inst{STATICCALL}'s and \inst{DELEGATECALL}'s into accounts with nonempty byte code; + \item + \user{}-transaction processing with $\loc{tx.toAddress()} = \varnothing$ and nonempty \loc{tx.payload()}; + the \romMod{} loads the initialization code $T_\mathbf{i} \equiv \loc{tx.payload()}$ from the \rlpTxnMod{} module; + \item + similarly when initiating deployments through (unexceptional, unaborted and no failure condition raising) \inst{CREATE(2)} instructions; + the \romMod{} module similarly loads the initialization code from \textsc{ram}, i.e. from the \mmioMod{} module; + \item + for \emph{temporarily} successful deployments of + nonempty byte code, the byte code is loaded into the \romMod{} from \textsc{ram}, i.e. from the \mmioMod{} module; + \item + for nontrivial and unexceptional \inst{EXTCODECOPY} operations targeting an account with nonempty byte code; \end{enumerate} +\saNote{} +We add the qualifier \emph{temporarily} to deployments since successful deployments may get reverted later on in the same transaction. diff --git a/rom/lookups/rom_into_instruction_decoder.tex b/rom/lookups/rom_into_instruction_decoder.tex index 8e2d4e1f..fcb282ea 100644 --- a/rom/lookups/rom_into_instruction_decoder.tex +++ b/rom/lookups/rom_into_instruction_decoder.tex @@ -8,9 +8,9 @@ from the \romMod{} module: \begin{multicols}{3} \begin{enumerate} - \item $\pbcb _{i}$ - \item $\IRP _{i}$ - \item $\IRJD _{i}$ + \item $\romColumnOpcode _{i}$ + \item $\romColumnOpcodeIsPush _{i}$ + \item $\IJD _{i}$ % \item[\vspace{\fill}] \end{enumerate} \end{multicols} @@ -18,8 +18,8 @@ from the \idMod{} module: \begin{multicols}{3} \begin{enumerate} - \item $\opc _{j}$ - \item $\IP _{j}$ + \item $\romColumnOpcode _{j}$ + \item $\romColumnOpcodeIsPush _{j}$ \item $\IJD _{j}$ % \item[\vspace{\fill}] \end{enumerate} @@ -31,7 +31,7 @@ \[ \renewcommand{\arraystretch}{1.3} \begin{array}{|l|c|c|} \hline - \opc & \idMod\separator\IP & \idMod\separator\IJD \\ \hline \hline + \romColumnOpcode & \idMod\separator\romColumnOpcodeIsPush & \idMod\separator\IJD \\ \hline \hline \inst{PUSH0} & \gZero & \gZero \\ \hline \inst{PUSHX} & \rOne & \gZero \\ \hline \inst{JUMPDEST} & \gZero & \rOne \\ \hline @@ -40,7 +40,7 @@ \] \caption{% Relevant portion of the \idMod{} module. - In the above $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$} + In the above $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \evmWordSize \}$} \label{rom: instruction decoding: relevant portion of ID module} \end{figure} diff --git a/rom/lua/byte_code.lua.tex b/rom/lua/byte_code.lua.tex new file mode 100644 index 00000000..820d4725 --- /dev/null +++ b/rom/lua/byte_code.lua.tex @@ -0,0 +1,53 @@ +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback + ("emojifallback", + { + "NotoColorEmoji:mode=harf;" + } + )} + +\setmonofont{JetBrains Mono NL Regular}[ + RawFeature={fallback=emojifallback} +] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + +When the byte code contains X bytes following a PUSHX instruction: + + PUSH11 + ↓ +... ?? ?? 6a 11 22 33 44 55 66 77 88 99 aa bb ?? ?? + │ │ + ├──────────────────────────────────────────┘ + │ PUSH bytes + │ + └─────────────────────────────────────────────────── ∙∙∙ + bytes belonging to the byte code proper + + + +When the byte code contains fewer than X bytes following a PUSHX instruction: + + PUSH20 final byte of byte code + ↓ ↓ +... ?? ?? 73 11 22 33 44 55 66 77 88 99 aa bb cc .. .. .. .. .. .. .. .. .. + │ │ │ + ├──────────────────────────────────────────────┘ │ + │ bytes belonging to the byte code proper │ + │ │ + └──────────────────────────────────────────────────────────────────────────────┘ + PUSH bytes (".." stand for 00) + + +NOTE. What we call "PUSH bytes" are the bytes use to build the PUSH_VALUE, i.e. + the X bytes of the (zero padded) byte code following a PUSHX instruction. + +\end{verbatim} +\end{document} + diff --git a/rom/lua/padding_nonzero.lua.tex b/rom/lua/padding_nonzero.lua.tex new file mode 100644 index 00000000..bc3e57ce --- /dev/null +++ b/rom/lua/padding_nonzero.lua.tex @@ -0,0 +1,80 @@ +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback + ("emojifallback", + { + "NotoColorEmoji:mode=harf;" + } + )} + +\setmonofont{JetBrains Mono NL Regular}[ + RawFeature={fallback=emojifallback} +] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + ██████\ ██████\ ███████\ ████████\ ██████\ ██████\ ████████\ ████████\ ██\ ██████\ ██\ ██\ ██████\ +██ __██\ ██ __██\ ██ __██\ ██ _____| ██ __██\ \_██ _|\____██ |██ _____| ██ | ███ __██\ ██ | ████ | ██ __██\ +██ / \__|██ / ██ |██ | ██ |██ | ██ / \__| ██ | ██ / ██ | ██ |████\ ████\ ██ | ██████\████\ ██████\ ███████ | \_██ | ██ / \__| +██ | ██ | ██ |██ | ██ |█████\ \██████\ ██ | ██ / █████\ ██ |\____| ██\██\██ | ██ _██ _██\ ██ __██\ ██ __██ | ██ | ███████\ +██ | ██ | ██ |██ | ██ |██ __| \____██\ ██ | ██ / ██ __| \__|████\ ██ \████ | ██ / ██ / ██ |██ / ██ |██ / ██ | ██ | ██ __██\ +██ | ██\ ██ | ██ |██ | ██ |██ | ██\ ██ | ██ | ██ / ██ | \____| ██ |\███ | ██ | ██ | ██ |██ | ██ |██ | ██ | ██ | ██ / ██ | +\██████ | ██████ |███████ |████████\ \██████ |██████\ ████████\ ████████\ ██\ \██████ / ██ | ██ | ██ |\██████ |\███████ | ██████\ ██████ | + \______/ \______/ \_______/ \________|██████\\______/ \______|\________|\________| \__| \______/ \__| \__| \__| \______/ \_______| \______|\______/ + \______| + + +Padding when CODE_SIZE + r ≡ 0 mod 16, r ∈ { 0, 1 ..., 15 } +Here CODE_SIZE = 16 * n + 3 so that r = 12 +There are thus 32 + r = 44 byte code PADDING-rows (where PADDING ≡ 1 i.e. PADDING ≡ ) + +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +| LIMB_SIZE | LIMB_SIZE_ACC | CODE_SIZE | PADDING | LIMB | LIMB_BYTE | CFI | CT | CT_MAX | +|:---------:+:-------------:+:---------:+:-------:+:----------------------------:+:---------:+:-----:+:---:+:------:| +| | ... | | ... | ... | | ... | | | +| | | | | | | | | | +| | cs - 16 | cs | 0 | 0x ?? ?? ... ?? ?? ?? | | c | 15 | 15 | +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | 00 | c | 0 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | 11 | c | 1 | 15 | ← +| | | | | | | | | | ← +| ... | ... | | ... | ... | ... | ... | ... | ... | ← 16 rows +| | | | | | | | | | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | dd | c | 13 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | ee | c | 14 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | ff | c | 15 | 15 | ← +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +| 3 | cs | cs | 0 | 0x 11 22 33 .. .. ... .. | 11 | c | 0 | 15 | ← +| 3 | cs | cs | 0 | 0x 11 22 33 .. .. ... .. | 22 | c | 1 | 15 | ← +| 3 | cs | cs | 0 | 0x 11 22 33 .. .. ... .. | 33 | c | 2 | 15 | ← +| 3 | cs | cs | | 0x 11 22 33 .. .. ... .. | 00 | c | 3 | 15 | ← PADDING starts here +| 3 | cs | cs | | 0x 11 22 33 .. .. ... .. | 00 | c | 4 | 15 | ← +| | | | | | | | | | ← +| ... | ... | | ... | ... | ... | ... | ... | ... | ← 16 rows (total) +| | | | | | | | | | ← +| 3 | cs | cs | | 0x 11 22 33 .. .. ... .. | 00 | c | 14 | 15 | ← +| 3 | cs | cs | | 0x 11 22 33 .. .. ... .. | 00 | c | 15 | 15 | ← +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +| | | | | | 00 | c | 0 | 31 | ← +| | | | | | 00 | c | 1 | 31 | ← +| | | | | | | | | | ← +| ... | ... | | ... | ... | ... | ... | ... | ... | ← 32 rows +| | | | | | | | | | ← +| | | | | | 00 | c | 30 | 31 | ← +| | | | | | 00 | c | 31 | 31 | ← +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +|-----------+---------------+-----------+---------+------------------------------+-----------+-------+-----+--------| +| ls' | ls' | cs' | 0 | 0x ?? ?? ... ?? ?? ?? | ?? | c + 1 | 0 | 15 | +| | | | | | | | | | +| ... | ... | | ... | ... | ... | ... | ... | ... | + + +NOTE. As per usual, one must interpret ".." as "00" and "..." as "and so on". +NOTE. In the above there are +\end{verbatim} +\end{document} + diff --git a/rom/lua/padding_zero.lua.tex b/rom/lua/padding_zero.lua.tex new file mode 100644 index 00000000..31823d0e --- /dev/null +++ b/rom/lua/padding_zero.lua.tex @@ -0,0 +1,70 @@ +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback + ("emojifallback", + { + "NotoColorEmoji:mode=harf;" + } + )} + +\setmonofont{JetBrains Mono NL Regular}[ + RawFeature={fallback=emojifallback} +] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + ██████\ ██████\ ███████\ ████████\ ██████\ ██████\ ████████\ ████████\ ██████\ ██\ ██\ ██████\ +██ __██\ ██ __██\ ██ __██\ ██ _____| ██ __██\ \_██ _|\____██ |██ _____| ███ __██\ ██ | ████ | ██ __██\ +██ / \__|██ / ██ |██ | ██ |██ | ██ / \__| ██ | ██ / ██ | ████\ ████\ ████\ ██ | ██████\████\ ██████\ ███████ | \_██ | ██ / \__| +██ | ██ | ██ |██ | ██ |█████\ \██████\ ██ | ██ / █████\ \____|\____| ██\██\██ | ██ _██ _██\ ██ __██\ ██ __██ | ██ | ███████\ +██ | ██ | ██ |██ | ██ |██ __| \____██\ ██ | ██ / ██ __| ████\ ████\ ██ \████ | ██ / ██ / ██ |██ / ██ |██ / ██ | ██ | ██ __██\ +██ | ██\ ██ | ██ |██ | ██ |██ | ██\ ██ | ██ | ██ / ██ | \____|\____| ██ |\███ | ██ | ██ | ██ |██ | ██ |██ | ██ | ██ | ██ / ██ | +\██████ | ██████ |███████ |████████\ \██████ |██████\ ████████\ ████████\ \██████ / ██ | ██ | ██ |\██████ |\███████ | ██████\ ██████ | + \______/ \______/ \_______/ \________|██████\\______/ \______|\________|\________| \______/ \__| \__| \__| \______/ \_______| \______|\______/ + \______| + + + +Padding when CODE_SIZE ≡ 0 mod 16 so that +CODE_SIZE + r ≡ 0 mod 16, r ∈ { 0, 1 ..., 15 }, has r = 0. +There are thus 32 + r = 32 byte code PADDING-rows (where PADDING ≡ 1 i.e. PADDING ≡ ) + +|-----------+---------------+-----------+---------+---------------------------+-----------+-------+-----+--------| +| LIMB_SIZE | LIMB_SIZE_ACC | CODE_SIZE | PADDING | LIMB | LIMB_BYTE | CFI | CT | CT_MAX | +|:---------:+:-------------:+:---------:+:-------:+:-------------------------:+:---------:+:-----:+:---:+:------:| +| | ... | | ... | ... | | ... | | | +| | | | | | | | | | +| | cs - 16 | cs | 0 | 0x ?? ?? ... ?? ?? ?? | | c | 15 | 15 | +|-----------+---------------+-----------+---------+---------------------------+-----------+-------+-----+--------| +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | 00 | c | 0 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | 11 | c | 1 | 15 | ← +| | | | | | | | | | ← +| ... | ... | | ... | ... | ... | ... | ... | ... | ← 16 rows +| | | | | | | | | | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | dd | c | 13 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | ee | c | 14 | 15 | ← +| 16 | cs | cs | 0 | 0x 00 11 ... dd ee ff | ff | c | 15 | 15 | ← +|-----------+---------------+-----------+---------+---------------------------+-----------+-------+-----+--------| +| | | | | | 00 | c | 0 | 31 | ← PADDING starts here +| | | | | | 00 | c | 1 | 31 | ← +| | | | | | | | | | ← +| ... | ... | | ... | ... | ... | ... | ... | ... | ← 32 rows +| | | | | | | | | | ← +| | | | | | 00 | c | 30 | 31 | ← +| | | | | | 00 | c | 31 | 31 | ← +|-----------+---------------+-----------+---------+---------------------------+-----------+-------+-----+--------| +|-----------+---------------+-----------+---------+---------------------------+-----------+-------+-----+--------| +| ls' | ls' | cs' | 0 | 0x ?? ?? ... ?? ?? ?? | ?? | c + 1 | 0 | 15 | +| | | | | | | | | | +| ... | ... | | ... | ... | ... | ... | ... | ... | + + +NOTE. As per usual, one must interpret ".." as "00" and "..." as "and so on". +NOTE. In the above there are +\end{verbatim} +\end{document} + diff --git a/rom/opcode/_inputs.tex b/rom/opcode/_inputs.tex index 3318e38f..7ed64b72 100644 --- a/rom/opcode/_inputs.tex +++ b/rom/opcode/_inputs.tex @@ -1,3 +1,3 @@ -\subsubsection{Deducing \opc{} from \pbcb{}} \label{rom: opcode: opcode from padded byte code byte} \input{opcode/opcode_vs_raw_byte} -\subsubsection{Connecting \IP{} to \IRP{}} \label{rom: opcode: is push from decoded} \input{opcode/is_push_from_decoded} -\subsubsection{Connecting \ISVALIDJUMPDESTINATION{} to \IRJD{}} \label{rom: opcode: is jumpdest from decoded} \input{opcode/is_jumpdest_from_decoded} +\subsubsection{Deducing \romColumnOpcode{} from \romColumnLimbByte{}} \label{rom: opcode: opcode from padded byte code byte} \input{opcode/opcode_vs_raw_byte} +% \subsubsection{Connecting \romColumnOpcodeIsPush{} to \IRP{}} \label{rom: opcode: is push from decoded} \input{opcode/is_push_from_decoded} +% \subsubsection{Connecting \romColumnOpcodeIsJumpDest{} to \IRJD{}} \label{rom: opcode: is jumpdest from decoded} \input{opcode/is_jumpdest_from_decoded} diff --git a/rom/opcode/is_jumpdest_from_decoded.tex b/rom/opcode/is_jumpdest_from_decoded.tex index fde05e53..7ebba9f6 100644 --- a/rom/opcode/is_jumpdest_from_decoded.tex +++ b/rom/opcode/is_jumpdest_from_decoded.tex @@ -1,10 +1,10 @@ -We now connect \ISVALIDJUMPDESTINATION{} to \IRJD{}: +We now connect \romColumnOpcodeIsJumpDest{} to \IRJD{}: \begin{enumerate} - \item \If $\IRJD _{i} = 0$ \Then $\ISVALIDJUMPDESTINATION _{i} = 0$ + \item \If $\IRJD _{i} = 0$ \Then $\romColumnOpcodeIsJumpDest _{i} = 0$ \item \If $\IRJD _{i} = 1$ \Then \begin{enumerate} - \item \If $\IPD _{i} = 0$ \Then $\ISVALIDJUMPDESTINATION _{i} = 1$ - \item \If $\IPD _{i} = 1$ \Then $\ISVALIDJUMPDESTINATION _{i} = 0$ + \item \If $\romColumnClaimedByPush _{i} = 0$ \Then $\romColumnOpcodeIsJumpDest _{i} = 1$ + \item \If $\romColumnClaimedByPush _{i} = 1$ \Then $\romColumnOpcodeIsJumpDest _{i} = 0$ \end{enumerate} \end{enumerate} diff --git a/rom/opcode/is_push_from_decoded.tex b/rom/opcode/is_push_from_decoded.tex index a2166858..fe796cfe 100644 --- a/rom/opcode/is_push_from_decoded.tex +++ b/rom/opcode/is_push_from_decoded.tex @@ -1,9 +1,9 @@ -We further connect \IP{} to \IRP{}: +We further connect \romColumnOpcodeIsPush{} to \IRP{}: \begin{enumerate} - \item \If $\IRP _{i} = 0$ \Then $\IP _{i} = 0$ + \item \If $\IRP _{i} = 0$ \Then $\romColumnOpcodeIsPush _{i} = 0$ \item \If $\IRP _{i} = 1$ \Then \begin{enumerate} - \item \If $\IPD _{i} = 0$ \Then $\IP _{i} = 1$ - \item \If $\IPD _{i} = 1$ \Then $\IP _{i} = 0$ + \item \If $\romColumnClaimedByPush _{i} = 0$ \Then $\romColumnOpcodeIsPush _{i} = 1$ + \item \If $\romColumnClaimedByPush _{i} = 1$ \Then $\romColumnOpcodeIsPush _{i} = 0$ \end{enumerate} \end{enumerate} diff --git a/rom/opcode/opcode_vs_raw_byte.tex b/rom/opcode/opcode_vs_raw_byte.tex index a4b58c57..4623ad7e 100644 --- a/rom/opcode/opcode_vs_raw_byte.tex +++ b/rom/opcode/opcode_vs_raw_byte.tex @@ -1,5 +1,5 @@ We impose the following unconditionally: \begin{enumerate} - \item \If $\IPD_{i} = 0$ \Then $\opc_{i} = \pbcb_{i}$ - \item \If $\IPD_{i} = 1$ \Then $\opc_{i} = \inst{INVALID}$ + \item \If $\romColumnClaimedByPush _{i} = 0$ \Then $\romColumnOpcode _{i} = \romColumnLimbByte _{i}$ + \item \If $\romColumnClaimedByPush _{i} = 1$ \Then $\romColumnOpcode _{i} = \inst{INVALID}$ \end{enumerate} diff --git a/rom/push/bits.tex b/rom/push/bits.tex index 4575392d..4387f940 100644 --- a/rom/push/bits.tex +++ b/rom/push/bits.tex @@ -1,6 +1,6 @@ We unconditionally impose the following \begin{enumerate} - \item $\IP_{i} \cdot \IPD_{i} = 0$ - \item \If $\IP_{i} = 1$ \Then $\IPD_{i + 1} = 1$ - \item \If $\IPD_{i} = 1$ \Then $\Big(\IPD_{i - 1} + \IP_{i - 1} = 1\Big)$ + \item $\IP _{i} \cdot \romColumnClaimedByPush _{i} = 0$ + \item \If $\IP _{i} = 1$ \Then $\romColumnClaimedByPush _{i + 1} = 1$ + \item \If $\romColumnClaimedByPush _{i} = 1$ \Then $\Big(\romColumnClaimedByPush _{i - 1} + \IP _{i - 1} = 1\Big)$ \end{enumerate} diff --git a/rom/push/counter.tex b/rom/push/counter.tex index 6507b003..4b52580d 100644 --- a/rom/push/counter.tex +++ b/rom/push/counter.tex @@ -1,36 +1,36 @@ -We connect $(\PP, \cp)$ to $(\IP, \IPD)$: +We connect $(\PP, \cp)$ to $(\romColumnOpcodeIsPush, \romColumnClaimedByPush)$: \begin{enumerate} \item - \If $\IP_{i} + \IPD_{i} = 0$ \Then + \If $\romColumnOpcodeIsPush _{i} + \romColumnClaimedByPush _{i} = 0$ \Then \[ \left\{ \begin{array}{lcl} - \PP_{i} & = & 0 \\ - \cp_{i} & = & 0 \\ + \PP _{i} & = & 0 \\ + \cp _{i} & = & 0 \\ \end{array} \right. \] \item \label{rom: push: counter: setting nontrivial PUSH_CT_MAX values} - \If $\IP _{i} = 1$ \Then + \If $\romColumnOpcodeIsPush _{i} = 1$ \Then \[ \left\{ \begin{array}{lcl} - \PP_{i} & = & \opc_{i} - \inst{PUSH1} + 1 \\ - \cp_{i} & = & 0 \\ + \PP _{i} & = & \romColumnOpcode _{i} - \inst{PUSH0} \\ + \cp _{i} & = & 0 \\ \end{array} \right. \] \item - \If $\IPD _{i} = 1$ \Then + \If $\romColumnClaimedByPush _{i} = 1$ \Then \[ \left\{ \begin{array}{lcl} - \PP_{i} & = & \PP_{i - 1} \\ - \cp_{i} & = & 1 + \cp _{i - 1} \\ + \PP _{i} & = & \PP _{i - 1} \\ + \cp _{i} & = & 1 + \cp _{i - 1} \\ \end{array} \right. \] \item \label{rom: push: counter: no early resets for IS_PUSH_BYTE} - \If $\cp_{i} \neq \PP_{i}$ \Then $\IPD _{i + 1} = 1$ + \If $\cp _{i} \neq \PP _{i}$ \Then $\romColumnClaimedByPush _{i + 1} = 1$ \item \label{rom: push: counter: IS_PUSH_BYTE resets when CT reaches MAX} - \If $\cp_{i} = \PP_{i}$ \Then $\IPD _{i + 1} = 0$ + \If $\cp _{i} = \PP _{i}$ \Then $\romColumnClaimedByPush _{i + 1} = 0$ \end{enumerate} \saNote{} It follows from @@ -44,7 +44,7 @@ \saNote{} The purpose of -constraint~(\ref{rom: push: counter: no early resets for IS_PUSH_BYTE}) is to prevent $\IPD$ from ``resetting early.'' +constraint~(\ref{rom: push: counter: no early resets for IS_PUSH_BYTE}) is to prevent $\romColumnClaimedByPush$ from ``resetting early.'' On the other hand the purpose of -constraint~(\ref{rom: push: counter: IS_PUSH_BYTE resets when CT reaches MAX}) is to force $\IPD$ to ``reset'' at the appropriate time, +constraint~(\ref{rom: push: counter: IS_PUSH_BYTE resets when CT reaches MAX}) is to force $\romColumnClaimedByPush$ to ``reset'' at the appropriate time, i.e. when $\cp$ catches up with $\PP$. diff --git a/rom/push/values.tex b/rom/push/values.tex index 9c0ffae0..825eee57 100644 --- a/rom/push/values.tex +++ b/rom/push/values.tex @@ -1,36 +1,36 @@ -The constraints below construct (the high and low parts of) the \PV{} for \inst{PUSH} instructions. We start by describing the ``non push data'' case: +The constraints below construct (the high and low parts of) the \romColumnPushValue{} for \inst{PUSH} instructions. We start by describing the ``non push data'' case: We now deal with the ``push data'' case. Constraints when not in a \inst{PUSH} instruction: Initialisation of a \inst{PUSH} instruction: We unconditionally impose the following \begin{enumerate} - \item $(1 - \IP_{i}) \cdot (1 - \PFB_{i}) = 0$ \quad (\trash) + \item $(1 - \IP _{i}) \cdot (1 - \PFB _{i}) = 0$ \quad (\trash) \end{enumerate} -We now deal with the construction \emph{per se} of (the high and low parts of) the \PV{}: +We now deal with the construction \emph{per se} of (the high and low parts of) the \romColumnPushValue{}: \begin{enumerate}[resume] - \item \If $\IP_{i} = 1$ \Then: + \item \If $\IP _{i} = 1$ \Then: \begin{enumerate} - \item $\PVA_{i} = 0$ - \item $\pfb_{i} + \pfb_{i + 1} = 0$ + \item $\PVA _{i} = 0$ + \item $\pfb _{i} + \pfb _{i + 1} = 0$ \end{enumerate} - \item \If $\IPD_{i} = 1$ \Then + \item \If $\romColumnClaimedByPush _{i} = 1$ \Then \begin{enumerate} - \item \If $\CP_{i} + \llarge \ne \PP_{i}$ \Then: + \item \If $\CP _{i} + \llarge \neq \PP _{i}$ \Then: \begin{enumerate} - \item \If $\IPD_{i + 1} = 1$ \Then $\pfb_{i + 1}=\pfb_{i}$ + \item \If $\romColumnClaimedByPush _{i + 1} = 1$ \Then $\pfb _{i + 1} = \pfb _{i}$ \end{enumerate} - \item \If $\CP_{i} + \llarge = \PP_{i}$ \Then: + \item \If $\CP _{i} + \llarge = \PP _{i}$ \Then: \begin{enumerate} - \item $\pfb_{i + 1} = 1 + \pfb_{i}$\footnote{i.e., since \pfb{} is push-incrementing, $\pfb_{i} = 0$ \et $\pfb_{i + 1}=1$ or alternatively $\pfb_{i} + \pfb_{i + 1} = 1$} - \item $\PVA_{i}=\PV\high_{i}$ + \item $\pfb _{i + 1} = 1 + \pfb _{i}$\footnote{i.e., since \pfb{} is push-incrementing, $\pfb _{i} = 0$ \et $\pfb _{i + 1} = 1$ or alternatively $\pfb _{i} + \pfb _{i + 1} = 1$} + \item $\PVA _{i} = \romColumnPushValue\high _{i}$ \end{enumerate} - \item \If ($\pfb_{i} = \pfb_{i - 1}$) \Then $\pva_{i} = 256 \cdot \pva_{i - 1} + \pbcb_{i}$ - \item \If ($\pfb_{i} \neq \pfb_{i - 1}$) \Then $\pva_{i} = \pbcb_{i}$ - \item \If $\CP_{i} = \PP_{i}$ \Then: + \item \If ($\pfb _{i} = \pfb _{i - 1}$) \Then $\pva _{i} = 256 \cdot \pva _{i - 1} + \romColumnLimbByte _{i}$ + \item \If ($\pfb _{i} \neq \pfb _{i - 1}$) \Then $\pva _{i} = \romColumnLimbByte _{i}$ + \item \If $\CP _{i} = \PP _{i}$ \Then: \begin{enumerate} - \item \If $\PFB_{i} = 0$ \Then $\PV\high_{i} = 0$ - \item $\PVA_{i} = \PV\low_{i}$ + \item \If $\PFB _{i} = 0$ \Then $\romColumnPushValue\high _{i} = 0$ + \item $\PVA _{i} = \romColumnPushValue\low _{i}$ \end{enumerate} \end{enumerate} \end{enumerate} @@ -39,28 +39,28 @@ \[ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline - \opc & \ip{} & \pp{} & \ipd{} & \cp{} & \pbcb{} & \pfb{} & \pva & \pv\high{} & \pv\low{} \\\hline - \inst{PUSH4} & 1 & 4 & 0 & 0 & \mathtt{0x\,63} & 0 & 0 & 0 & \mathtt{0x\,abcd} \\\hline - \inst{INVALID} & 0 & 4 & 1 & 1 & \mathtt{0x\,a} & 0 & \mathtt{0x\,a} & 0 & \mathtt{0x\,abcd} \\\hline - \inst{INVALID} & 0 & 4 & 1 & 2 & \mathtt{0x\,b} & 0 & \mathtt{0x\,ab} & 0 & \mathtt{0x\,abcd} \\\hline - \inst{INVALID} & 0 & 4 & 1 & 3 & \mathtt{0x\,c} & 0 & \mathtt{0x\,abc} & 0 & \mathtt{0x\,abcd} \\\hline - \inst{INVALID} & 0 & 4 & 1 & 4 & \mathtt{0x\,d} & 0 & \mathtt{0x\,abcd} & 0 & \mathtt{0x\,abcd} \\\hline + \romColumnOpcode & \ip{} & \pp{} & \romColumnClaimedByPush{} & \cp{} & \romColumnLimbByte{} & \pfb{} & \pva & \pv\high{} & \pv\low{} \\ \hline + \inst{PUSH4} & 1 & 4 & 0 & 0 & \mathtt{0x\,63} & 0 & 0 & 0 & \mathtt{0x\,abcd} \\ \hline + \inst{INVALID} & 0 & 4 & 1 & 1 & \mathtt{0x\,a} & 0 & \mathtt{0x\,a} & 0 & \mathtt{0x\,abcd} \\ \hline + \inst{INVALID} & 0 & 4 & 1 & 2 & \mathtt{0x\,b} & 0 & \mathtt{0x\,ab} & 0 & \mathtt{0x\,abcd} \\ \hline + \inst{INVALID} & 0 & 4 & 1 & 3 & \mathtt{0x\,c} & 0 & \mathtt{0x\,abc} & 0 & \mathtt{0x\,abcd} \\ \hline + \inst{INVALID} & 0 & 4 & 1 & 4 & \mathtt{0x\,d} & 0 & \mathtt{0x\,abcd} & 0 & \mathtt{0x\,abcd} \\ \hline \end{array} \] \[ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline - \opc & \ip{} & \pp{} & \ipd{} & \cp{} & \pbcb{} & \pfb{} & \pva & \pv\high{} & \pv\low{} \\ \hline - \inst{PUSH20} & 1 & 20 & 0 & 0 & \mathtt{0x\,73} & 0 & 0 & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 1 & \mathtt{0x\,a} & 0 & \mathtt{0x\,a} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 2 & \mathtt{0x\,b} & 0 & \mathtt{0x\,ab} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 3 & \mathtt{0x\,c} & 0 & \mathtt{0x\,abc} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 4 & \mathtt{0x\,d} & 0 & {\cellcolor{\romCol}\mathtt{0x\,abcd}} & {\cellcolor{\romCol}\mathtt{0x\,abcd}} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 5 & \mathtt{0x\,e} & 1 & \mathtt{0x\,e} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 6 & \mathtt{0x\,f} & 1 & \mathtt{0x\,ef} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \vdots & \vdots & 20 & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 19 & \mathtt{0x\,s} & 1 & \mathtt{0x\,efghijklmnopqrs} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline - \inst{INVALID} & 0 & 20 & 1 & 20 & \mathtt{0x\,t} & 1 & {\cellcolor{\romCol}\mathtt{0x\,efghijklmnopqrst}} & \mathtt{0x\,abcd} & {\cellcolor{\romCol}\mathtt{0x\,efghijklmnopqrst}} \\ \hline + \romColumnOpcode & \ip{} & \pp{} & \romColumnClaimedByPush{} & \cp{} & \romColumnLimbByte{} & \pfb{} & \pva & \pv\high{} & \pv\low{} \\ \hline + \inst{PUSH20} & 1 & 20 & 0 & 0 & \mathtt{0x\,73} & 0 & 0 & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 1 & \mathtt{0x\,a} & 0 & \mathtt{0x\,a} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 2 & \mathtt{0x\,b} & 0 & \mathtt{0x\,ab} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 3 & \mathtt{0x\,c} & 0 & \mathtt{0x\,abc} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 4 & \mathtt{0x\,d} & 0 & {\cellcolor{\romCol}\mathtt{0x\,abcd}} & {\cellcolor{\romCol}\mathtt{0x\,abcd}} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 5 & \mathtt{0x\,e} & 1 & \mathtt{0x\,e} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 6 & \mathtt{0x\,f} & 1 & \mathtt{0x\,ef} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \vdots & \vdots & 20 & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 19 & \mathtt{0x\,s} & 1 & \mathtt{0x\,efghijklmnopqrs} & \mathtt{0x\,abcd} & \mathtt{0x\,efghijklmnopqrst} \\ \hline + \inst{INVALID} & 0 & 20 & 1 & 20 & \mathtt{0x\,t} & 1 & {\cellcolor{\romCol}\mathtt{0x\,efghijklmnopqrst}} & \mathtt{0x\,abcd} & {\cellcolor{\romCol}\mathtt{0x\,efghijklmnopqrst}} \\ \hline \end{array} \] diff --git a/rom/version.md b/rom/version.md index b2a5e64c..c07485f3 100644 --- a/rom/version.md +++ b/rom/version.md @@ -1 +1 @@ -previously called `rom_v3` +`rom_v3`