Skip to content

Commit

Permalink
Rationalization of REFUND increments for SSTORE (#22)
Browse files Browse the repository at this point in the history
  • Loading branch information
@OlivierBBB
OlivierBBB authored Dec 5, 2024
1 parent 8cbeaae commit ec3f528
Show file tree
Hide file tree
Showing 2 changed files with 108 additions and 31 deletions.
12 changes: 12 additions & 0 deletions hub/instruction_handling/storage/_local.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,14 @@
\def\locCurrIsOrig {\col{curr\_is\_orig}}
\def\locNextIsOrig {\col{next\_is\_orig}}
\def\locNextIsCurr {\col{next\_is\_curr}}

\def\locOrigNotZero {\col{orig\_not\_zero}}
\def\locCurrNotZero {\col{curr\_not\_zero}}
\def\locNextNotZero {\col{next\_not\_zero}}
\def\locCurrNotOrig {\col{curr\_not\_orig}}
\def\locNextNotOrig {\col{next\_not\_orig}}
\def\locNextNotCurr {\col{next\_not\_curr}}

\def\locFirstCon {\yellowm{1}}
\def\locStaticxSecondCon {\yellowm{2}}
\def\locSstorexMisc {\yellowm{2}}
Expand All @@ -28,3 +36,7 @@
\def\locLoadedValueLo {\col{loaded\_value\_lo}}
\def\locValueToStoreHi {\col{value\_to\_store\_hi}}
\def\locValueToStoreLo {\col{value\_to\_store\_lo}}

\def\locCleanClear {\col{r\_clean\_clear}}
\def\locDirtyClear {\col{r\_dirty\_clear}}
\def\locDirtyReset {\col{r\_dirty\_reset}}
127 changes: 96 additions & 31 deletions hub/instruction_handling/storage/constraints.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,15 @@
\locNextIsOrig & \!\!\! \define \!\!\! & \stoNextValueIsOrig_{i + \locFirstStoRowOffset} \\
\locNextIsCurr & \!\!\! \define \!\!\! & \stoNextValueIsCurr_{i + \locFirstStoRowOffset} \\
\end{array} \right.
\quad\text{and}\quad
\left\{ \begin{array}{lcl}
\locOrigNotZero & \!\!\! \define \!\!\! & 1 - \locOrigIsZero \\
\locCurrNotZero & \!\!\! \define \!\!\! & 1 - \locCurrIsZero \\
\locNextNotZero & \!\!\! \define \!\!\! & 1 - \locNextIsZero \\
\locCurrNotOrig & \!\!\! \define \!\!\! & 1 - \locCurrIsOrig \\
\locNextNotOrig & \!\!\! \define \!\!\! & 1 - \locNextIsOrig \\
\locNextNotCurr & \!\!\! \define \!\!\! & 1 - \locNextIsCurr \\
\end{array} \right.
\]
\begin{description}
\item[\underline{Setting the gas cost:}]
Expand All @@ -207,12 +216,12 @@
\item[\underline{The \inst{SSTORE} case:}]
\If $\locIsSstore = 1$ \Then
\begin{enumerate}
\item \If $\locNextIsCurr = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $
\item \If $\locCurrIsOrig = 0$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $
\item \If \Big($\locNextIsCurr = 0$ \et $\locCurrIsOrig = 1$\Big)
\item \If $\locNextIsCurr = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $
\item \If $\locCurrNotOrig = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $
\item \If \Big($\locNextNotCurr = 1$ \et $\locCurrIsOrig = 1$\Big)
\begin{enumerate}
\item \If $\locOrigIsZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sset} $
\item \If $\locOrigIsZero = 0$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sreset} $
\item \If $\locOrigIsZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sset} $
\item \If $\locOrigNotZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sreset} $
\end{enumerate}
\end{enumerate}
where in the above we have used the following shorthand
Expand All @@ -221,31 +230,87 @@
\]
\end{description}
\item[\underline{Setting the refund:}]
recall that among instructions raising the $\stackDecStoFlag$ only the \inst{SSTORE} instruction may grand refunds.
Futhermore refunds may only be granted in non reverting contexts.
recall that among instructions raising the $\stackDecStoFlag$ only the \inst{SSTORE} instruction ($\locIsSstore \equiv 1$) may grand refunds.
Futhermore refunds may only be granted in non reverting contexts ($\cnWillRev \equiv 0$.)
See section~(\ref{hub: generalities: refunds: refunds}) for more details.

\If \Big($\cnWillRev_{i} = 0$ \et $\locIsSstore = 1$\Big) \Then we thus impose that
\begin{enumerate}
\item \If $\locNextIsCurr = 1$ \Then $\refund\new_{i} = \refund_{i}$
\item \If $\locNextIsCurr = 0$ \Then
\begin{enumerate}
\item \If $\locCurrIsOrig = 0$ \Then
\[
\refund\new_{i} = \refund_{i}
+
\left[ \begin{array}{crcccl}
+ & (1 - \locOrigIsZero) & \cdot & (\locNextIsZero - \locCurrIsZero) & \cdot & R_\text{sclear} \\
+ & \locNextIsOrig & \cdot & \locOrigIsZero & \cdot & \big(G_\text{sset} - G_\text{warmaccess}\big) \\
+ & \locNextIsOrig & \cdot & (1 -\locOrigIsZero) & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\
\end{array} \right]
\]
\item \If $\locCurrIsOrig = 1$ \Then
\begin{enumerate}
\item \If $\locNextIsZero = 0$ \Then $\refund\new_{i} = \refund_{i}$
\item \If $\locNextIsZero = 1$ \Then $\refund\new_{i} = \refund_{i} + R_\text{sclear}$
\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{description}

We therefore unconditionally impose
\[
\refund\new _{i} = \refund_{i} + (1 - \cnWillRev_{i}) \cdot \locIsSstore \cdot
\left[ \begin{array}{cr}
+ & \locCleanClear \\
+ & \locDirtyClear \\
+ & \locDirtyReset \\
\end{array} \right]
\]
where $\locCleanClear$, $\locDirtyClear$, $\locDirtyReset$ are shorthands which we define below.

\saNote{}
In the explanations provided below we use notations from the \cite{EYP} whereby
$v_0$ stands for the value originally in storage,
$v$ for the value currently in storage,
$v'$ for the value we are attempting to store:
\begin{description}
\item[\underline{Defining \locCleanClear{}:}]
we set
\[
\locCleanClear \define
\left[ \begin{array}{cr}
\cdot & \locNextNotCurr \\
\cdot & \locCurrIsOrig \\
\cdot & \locNextIsZero \\
\end{array} \right]
\cdot R_\text{sclear}
\]
which corresponds to
\begin{itemize}
\item $R_\text{sclear}$ whenever $[v \neq v'] \wedge [v = v_{0}] \wedge [v' = 0]$
\item and $0$ otherwise
\end{itemize}
\item[\underline{Defining \locDirtyClear{}:}]
we set
\[
\locDirtyClear \define
\left[ \begin{array}{cr}
\cdot & \locNextNotCurr \\
\cdot & \locCurrNotOrig \\
\end{array} \right]
\cdot
\locOrigNotZero
\cdot
\left[ \begin{array}{cr}
- & \locCurrIsZero \\
+ & \locNextIsZero \\
\end{array} \right]
\cdot R_\text{sclear}
\]
which corresponds to
\begin{itemize}
\item $- R_\text{sclear}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} \neq 0] \wedge [v = 0]$,
\item $+ R_\text{sclear}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} \neq 0] \wedge [v' = 0]$,
\item and $0$ otherwise.
\end{itemize}
\item[\underline{Defining \locDirtyReset{}:}]
we set
\[
\locDirtyReset \define
\left[ \begin{array}{cr}
\cdot & \locNextNotCurr \\
\cdot & \locCurrNotOrig \\
\end{array} \right]
\cdot
\locNextIsOrig
\cdot
\left[ \begin{array}{crcl}
+ & \locOrigIsZero & \cdot & \big(G_\text{sset} - G_\text{warmaccess}\big) \\
+ & \locOrigNotZero & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\
\end{array} \right]
\]
which corresponds to
\begin{itemize}
\item $G_\text{sset} - G_\text{warmaccess}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} = v'] \wedge [v_{0} = 0]$,
\item $G_\text{sreset} - G_\text{warmaccess}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} = v'] \wedge [v_{0} \neq 0]$,
\item and $0$ otherwise.
\end{itemize}
\end{description}
\end{description}

0 comments on commit ec3f528

Please sign in to comment.