From 8cbeaae7fc3b9040a8c23a7a5a4a68d073fa17a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Olivier=20B=C3=A9gassat?=
 <38285177+OlivierBBB@users.noreply.github.com>
Date: Thu, 28 Nov 2024 18:01:59 +0700
Subject: [PATCH] Only CALL may actually transfer value (#9)

---
 .../generalities/account_rows_first_set.tex   | 43 ++++++++++++++++++-
 1 file changed, 41 insertions(+), 2 deletions(-)

diff --git a/hub/instruction_handling/call/generalities/account_rows_first_set.tex b/hub/instruction_handling/call/generalities/account_rows_first_set.tex
index 149b906..fdb5618 100644
--- a/hub/instruction_handling/call/generalities/account_rows_first_set.tex
+++ b/hub/instruction_handling/call/generalities/account_rows_first_set.tex
@@ -45,10 +45,29 @@
 					{i}{\callFirstCallerAccountRowOffset}
 				\]
 			\item \If $\scenCallBalanceUpdateRequired _{i} = 1$ \Then
+				\begin{enumerate}
+				        \item \If $\locIsCall = 1$ \Then
+						\[
+							\accDecrementBalance
+							{i}{\callFirstCallerAccountRowOffset}{\locValueLo}
+						\]
+					\item \If $\locIsCallcode + \locIsDelegatecall + \locIsStaticcall = 1$ \Then
+						\[
+							\accSameBalance
+							{i}{\callFirstCallerAccountRowOffset}
+						\]
+				\end{enumerate}
+				\saNote{} \label{hub: instruction handling: call: generalities: first account rows: value transfer subtleties}
+				The above may alternatively be implemented without case disjunction as
 				\[
 					\accDecrementBalance
-					{i}{\callFirstCallerAccountRowOffset}{\locValueLo}
+					{i}{\callFirstCallerAccountRowOffset}{\locIsCall \cdot \locValueLo}
 				\]
+				Either way the above reflects that fact that only \inst{CALL} may \emph{actually} transfer value.
+				The \inst{CALL}-type instruction \inst{CALLCODE} also has a ``\locValue'' argument but it doesn't set off a value transfer.
+				This ``\locValue'' becomes the ``call value'' of the child context.
+				It is noteworthy that while no \emph{actual} value transfer takes place,
+				\inst{CALLCODE} may nonetheless incur a value transfer cost.
 		\end{enumerate}
 	\item[\underline{First \calleee{} account-row $n^°(i + \callFirstCalleeAccountRowOffset)$:}] 
 		we impose that
@@ -87,7 +106,27 @@
 		we impose that
 		\begin{enumerate}
 			\item \If $\scenCallBalanceUpdateNotRequired _{i} = 1$ \Then $\accSameBalance      {i}{\callFirstCalleeAccountRowOffset}$
-			\item \If $\scenCallBalanceUpdateRequired _{i}    = 1$ \Then $\accIncrementBalance {i}{\callFirstCalleeAccountRowOffset}{\locValueLo}$
+			\item \If $\scenCallBalanceUpdateRequired    _{i} = 1$ \Then
+				\begin{enumerate}
+				        \item \If $\locIsCall = 1$ \Then
+						\[
+							\accIncrementBalance
+							{i}{\callFirstCalleeAccountRowOffset}{\locValueLo}
+						\]
+					\item \If $\locIsCallcode + \locIsDelegatecall + \locIsStaticcall = 1$ \Then
+						\[
+							\accSameBalance
+							{i}{\callFirstCalleeAccountRowOffset}
+						\]
+				\end{enumerate}
+				\saNote{}
+				Echoing
+				note~(\ref{hub: instruction handling: call: generalities: first account rows: value transfer subtleties}),
+				the above may alternatively be implemented without case disjunction as
+				\[
+					\accIncrementBalance
+					{i}{\callFirstCalleeAccountRowOffset}{\locIsCall \cdot \locValueLo}
+				\]
 		\end{enumerate}
 	\item[\underline{Setting the \calleee{} warmth update on account-row $n^°(i + \callFirstCalleeAccountRowOffset)$:}]
 		we impose that