diff --git a/hub/instruction_handling/_inputs.tex b/hub/instruction_handling/_inputs.tex index a44377e..da0f3ee 100644 --- a/hub/instruction_handling/_inputs.tex +++ b/hub/instruction_handling/_inputs.tex @@ -16,7 +16,7 @@ \subsection{Instructions raising the $\stackDecKecFlag$ \lispDone{}} \subsection{Instructions raising the $\stackDecConFlag$ \lispDone{}} \label{hub: instruction handling: con} \input{instruction_handling/context/_inputs} \subsection{Instructions raising the $\stackDecAccFlag$ \lispDone{}} \label{hub: instruction handling: acc} \input{instruction_handling/account/_inputs} \subsection{Instructions raising the $\stackDecCopyFlag$ \lispDone{}} \label{hub: instruction handling: copy} \input{instruction_handling/copy/_inputs} -\subsection{Instructions raising the $\stackDecTxnFlag$ \lispDone{}} \label{hub: instruction handling: txn} \input{instruction_handling/txn} +\subsection{Instructions raising the $\stackDecTxnFlag$ \lispDone{}} \label{hub: instruction handling: txn} \input{instruction_handling/txn/_inputs} \subsection{Instructions raising the $\stackDecBtcFlag$ \lispDone{}} \label{hub: instruction handling: btc} \input{instruction_handling/btc} \subsection{Instructions raising the $\stackDecStackRamFlag$ \lispDone{}} \label{hub: instruction handling: stackRam} \input{instruction_handling/stack_ram/_inputs} \subsection{Instructions raising the $\stackDecStoFlag$ \lispDone{}} \label{hub: instruction handling: sto} \input{instruction_handling/storage/_inputs} diff --git a/hub/instruction_handling/txn.tex b/hub/instruction_handling/txn.tex deleted file mode 100644 index f902520..0000000 --- a/hub/instruction_handling/txn.tex +++ /dev/null @@ -1,62 +0,0 @@ -\subsubsection{Supported instructions and flags} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -\[ -\begin{array}{|l||c||c|c|} - \hline - \INST & \tli & \stackDecTxnFlag & \decFlag{1} \\ \hline\hline - \inst{ORIGIN} & \zero & \oneCell & \zero \\ \hline - \inst{GASPRICE} & \zero & \oneCell & \oneCell \\ \hline -\end{array} -\] -\saNote{} $\decFlag{1}$ distinguishes between the two instructions raising the $\stackDecTxnFlag$ flag. - - - -\subsubsection{Constraints} -%%%%%%%%%%%%%%%%%%%%%%%%%%% -\def\locTxnRow{\yellowm{1}} -\def\locConRow{\orangem{2}} -\begin{center} - \boxed{% - \text{The stack constraints presented below assume } - \begin{cases} - \peekStack_{i} = 1 \\ - \stackDecTxnFlag_{i} = 1 \\ - \stackSux_{i} + \stackSox_{i} = 0 \\ - \end{cases}} -\end{center} -We impose the following constraints: -\begin{description} - \item[\underline{Setting the stack pattern:}] we impose $\zeroOneSP_{i}$; - \item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = 1 + \cmc_{i}$; - \item[\underline{Setting the peeking flags:}] we impose - \[ - \left[ \begin{array}{lrcl} - + & \peekTransaction _{i + \locTxnRow} \\ - + & \peekContext _{i + \locConRow} & \!\!\!\cdot\!\!\! & \cmc_{i} \\ - \end{array} \right] - = - \nonStackRows_{i} - \] - \item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$; - \item[\underline{Value constraints:}] --- %\If $\cmc_{i} = 0$ \Then - \begin{enumerate} - \item \If $\decFlag{1}_{i} = 0$\footnote{i.e. $\INST_{i} = \inst{ORIGIN}$} \Then - \[ - \left\{ \begin{array}{lcl} - \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & \txFrom\high_{i + \locTxnRow} \\ - \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txFrom\low_{i + \locTxnRow} \\ - \end{array} \right. - \] - \item \If $\decFlag{1}_{i} = 1$\footnote{i.e. $\INST_{i} = \inst{GASPRICE}$} \Then - \[ - \left\{ \begin{array}{lcl} - \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & 0 \\ - \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txGasPrice_{i + \locTxnRow} \\ - \end{array} \right. - \] - \end{enumerate} -\end{description} -\saNote{} For instructions raising the $\stackDecTxnFlag$ one has $\cmc = \xAhoy$. diff --git a/hub/instruction_handling/txn/_inputs.tex b/hub/instruction_handling/txn/_inputs.tex new file mode 100644 index 0000000..9e1736f --- /dev/null +++ b/hub/instruction_handling/txn/_inputs.tex @@ -0,0 +1,5 @@ +\input{instruction_handling/txn/_local} +\subsubsection{Supported instructions and flags} \label{hub: instruction handling: txn: instructions} \input{instruction_handling/txn/instructions} +\subsubsection{Shorthands \lispDone{}} \label{hub: instruction handling: txn: shorthands} \input{instruction_handling/txn/shorthands} +\subsubsection{Constraints \lispDone{}} \label{hub: instruction handling: txn: constraints} \input{instruction_handling/txn/constraints} + diff --git a/hub/instruction_handling/txn/_local.tex b/hub/instruction_handling/txn/_local.tex new file mode 100644 index 0000000..0b40b80 --- /dev/null +++ b/hub/instruction_handling/txn/_local.tex @@ -0,0 +1,4 @@ +\def\locTxnRow {\yellowm{1}} +\def\locConRow {\orangem{2}} +\def\locIsOrigin {\col{is\_ORIGIN}} +\def\locIsGasPrice {\col{is\_GASPRICE}} diff --git a/hub/instruction_handling/txn/constraints.tex b/hub/instruction_handling/txn/constraints.tex new file mode 100644 index 0000000..77a6757 --- /dev/null +++ b/hub/instruction_handling/txn/constraints.tex @@ -0,0 +1,44 @@ +\begin{center} + \boxed{% + \text{The stack constraints presented below assume } + \begin{cases} + \peekStack _{i} = 1 \\ + \stackDecTxnFlag _{i} = 1 \\ + \stackSux _{i} + \stackSox _{i} = 0 \\ + \end{cases}} +\end{center} +We impose the following constraints: +\begin{description} + \item[\underline{Setting the stack pattern:}] we impose $\zeroOneSP_{i}$; + \item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = 1 + \cmc_{i}$; + \item[\underline{Setting the peeking flags:}] we impose + \[ + \left[ \begin{array}{lrcl} + + & \peekTransaction _{i + \locTxnRow} \\ + + & \peekContext _{i + \locConRow} & \!\!\!\cdot\!\!\! & \cmc_{i} \\ + \end{array} \right] + = + \nonStackRows_{i} + \] + \item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$; + \item[\underline{Value constraints:}] + \If $\xAhoy _{i} = 0$ \Then we impose that + \begin{enumerate} + \item \If $\locIsOrigin = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & \txFrom\high_{i + \locTxnRow} \\ + \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txFrom\low_{i + \locTxnRow} \\ + \end{array} \right. + \] + \item \If $\locIsGasPrice = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & 0 \\ + \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txGasPrice_{i + \locTxnRow} \\ + \end{array} \right. + \] + \end{enumerate} +\end{description} +\saNote{} +For instructions raising the $\stackDecTxnFlag$ one has $\cmc = \xAhoy$. diff --git a/hub/instruction_handling/txn/instructions.tex b/hub/instruction_handling/txn/instructions.tex new file mode 100644 index 0000000..4ee588f --- /dev/null +++ b/hub/instruction_handling/txn/instructions.tex @@ -0,0 +1,9 @@ +\[ + \begin{array}{|l||c||c|c|c|} + \hline + \INST & \tli & \stackDecTxnFlag & \decFlag{1} & \decFlag{2} \\ \hline\hline + \inst{ORIGIN} & \zero & \oneCell & \oneCell & \zero \\ \hline + \inst{GASPRICE} & \zero & \oneCell & \zero & \oneCell \\ \hline + \end{array} +\] + diff --git a/hub/instruction_handling/txn/shorthands.tex b/hub/instruction_handling/txn/shorthands.tex new file mode 100644 index 0000000..304abca --- /dev/null +++ b/hub/instruction_handling/txn/shorthands.tex @@ -0,0 +1,7 @@ +We further introduce the following shorthands +\[ + \left\{ \begin{array}{lcl} + \locIsOrigin & \define & \decFlag {1} _{i} \\ + \locIsGasPrice & \define & \decFlag {2} _{i} \\ + \end{array} \right. +\]