EIP 7702 --- HUB side
#354
Conversation
we do this in preparation of future changes where the relative block number will be anbandoned in favour of using the absolute block number everywhere
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
| \] | ||
| \end{enumerate} | ||
| \end{enumerate} | ||
| % \[ |
There was a problem hiding this comment.
Missing txAuth in finalization phase transition constraint
High Severity
The transition constraint for the txFinl phase adds txAuth to the sum in constraint (a) at line 49, and the transition graph shows a valid finl -> auth edge, but constraint (b) at lines 52-57 only sums txSkip + txWarm + txInit = peekContext without including txAuth. This means when peekContext = 1 (indicating a new transaction should start), txAuth must be 0 by constraint (a), making it impossible to start a new transaction with the authorization phase even though this transition is explicitly shown in the graph and intended by design.
Additional Locations (1)
| \item \If $\txSkip _{i} = 1$ \Then | ||
| \begin{enumerate} | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txInit _{i + 1} = 1$ | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txAuth _{i + 1} + \txInit _{i + 1} = 1$ |
There was a problem hiding this comment.
Inconsistent sanity check missing txAuth in skip transition
Medium Severity
The main constraint for txSkip transitions at line 5 was updated to include txAuth in the sum (txSkip + txWarm + txAuth + txInit = 1), but the sanity check at line 7 was not updated and still only sums txSkip + txWarm + txInit = 1. The note claims this sanity check is derivable from the main constraint and hubStamp properties, but adding txAuth to the main constraint invalidates this derivation since the hubStamp increment formula for SKIP doesn't involve txAuth. Either txAuth shouldn't be in the main constraint (consistent with the graph not showing skip->auth), or the sanity check derivation needs revision.
| \node[main, color = orange!70] (finl) [below of=warm] {$\txFinl$}; | ||
| \node[main, color = orange!70] (skip) [above left of=warm] {$\txSkip$}; | ||
| \draw[-latex] (warm) -- (auth); | ||
| \draw[-latex] (auth) -- (init); |
There was a problem hiding this comment.
Graph missing direct warm->init transition edge
Medium Severity
The diff shows the old warm -> init edge was replaced by warm -> auth at line 9. However, the constraint in transition.tex specifies txInit_{i+1} = peekTransaction_{i+1}, meaning when peekTransaction = 1 and peekAuthorization = 0, a direct transition from txWarm to txInit occurs (for transactions with access lists but no delegation lists). The graph now only shows warm -> auth -> init path, incorrectly implying all warm-phase transactions must go through authorization before initialization.
| \item \If $\txSkip _{i} = 1$ \Then | ||
| \begin{enumerate} | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txInit _{i + 1} = 1$ | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txAuth _{i + 1} + \txInit _{i + 1} = 1$ |
There was a problem hiding this comment.
Sanity check constraint may be missing txAuth
Medium Severity
The sanity check on line 7 states that when peekContext=1 in txSkip phase, the next state satisfies txSkip + txWarm + txInit = 1. However, the main constraint on line 5 includes txAuth, and the userTransactionStart formula in shorthands_start.tex line 10 explicitly accounts for transactions starting with txAuth when coming from non-txWarm/non-txAuth rows (including txSkip). Either the sanity check derivation is incomplete or txAuth should be added to the sanity check.
| \item \If $\txAuth _{i} = 1$ \Then | ||
| \begin{enumerate} | ||
| \item $\txAuth _{i + 1} + \txSkip _{i + 1} + \txInit _{i + 1} = 1$ | ||
| \item $\txSkip _{i + 1} + \txInit _{i + 1} = \peekTransaction _{i + 1}$ |
There was a problem hiding this comment.
AUTH transition missing txAuth-peekAuthorization linkage constraint
High Severity
The AUTH phase transition constraints are missing the linkage txAuth_{i+1} = peekAuthorization_{i+1} that the WARM transition includes at line 18. This means when staying in AUTH phase (AUTH→AUTH transitions), peekAuthorization is not constrained to equal txAuth. Since the hubStamp increment formula in increments.tex uses peekAuthorization_{i+1}, a prover could set peekAuthorization to arbitrary values within AUTH rows, potentially manipulating the hubStamp calculation. The AUTH transition should include a constraint analogous to line 18 to maintain consistency.
| \item \label{hub: system: hub stamp: increments: WARM case} \If $\txWarm _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + 1$ | ||
| \item \label{hub: system: hub stamp: increments: INIT case} \If $\txInit _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekContext _{i}$ | ||
| \item \label{hub: system: hub stamp: increments: FINL case} \If $\txFinl _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekContext _{i}$ | ||
| \item \label{hub: system: hub stamp: increments: AUTH case} \If $\txAuth _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekAuthorization _{i + 1} + \txInit _{i + 1}$ |
There was a problem hiding this comment.
AUTH hubStamp formula missing txSkip term for AUTH-to-SKIP
High Severity
The hubStamp increment formula for the AUTH phase uses peekAuthorization_{i+1} + txInit_{i+1}, but per transition.tex line 24, exiting AUTH can go to either INIT or SKIP via txSkip_{i+1} + txInit_{i+1} = peekTransaction_{i+1}. For AUTH→SKIP transitions (non-EVM-execution transactions with authorization), the formula evaluates to 0 since both peekAuthorization and txInit are 0. However, formal.tex line 4 expects hubStamp to increment by peekTransaction when entering SKIP phase. The formula should use peekTransaction_{i+1} instead of just txInit_{i+1} to handle both AUTH→INIT and AUTH→SKIP transitions.
| \end{enumerate} | ||
| \end{enumerate} | ||
| % \[ | ||
| % \left\{ \begin{array}{cccccccccc} |
There was a problem hiding this comment.
Missing txAuth in FINL phase transition constraint
High Severity
The "furthermore" constraint for txFinl transitions (lines 52-57) specifies txSkip + txWarm + txInit = peekContext, which excludes txAuth. However, line 49 includes txAuth in the valid transitions, and the transition graph explicitly shows a dashed edge from FINL to AUTH. The userTransactionStart shorthand also expects FINL → AUTH transitions for type 4 transactions without access lists. When peekContext = 1, the current constraint forces txAuth = 0, preventing valid transitions to authorization phase when starting a new type 4 transaction.
🔬 Verification Test
Why verification test was not possible: This is a LaTeX specification document defining ZK-EVM constraints, not executable code. The inconsistency is evident by comparing the transition constraint (lines 51-58), which omits txAuth, with the transition graph in transition_graph.tex line 14 (\draw[-latex, dashed, color = solarized-blue] (finl) -- (auth);) which explicitly shows FINL → AUTH as a valid transition.
| \item \If $\txSkip _{i} = 1$ \Then | ||
| \begin{enumerate} | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txInit _{i + 1} = 1$ | ||
| \item $\txSkip _{i + 1} + \txWarm _{i + 1} + \txAuth _{i + 1} + \txInit _{i + 1} = 1$ |
There was a problem hiding this comment.
SKIP transition sanity check missing txAuth flag
Medium Severity
The SKIP phase sanity check on line 7 specifies txSkip_{i+1} + txWarm_{i+1} + txInit_{i+1} = 1 when peekContext = 1, but the main constraint on line 5 includes txAuth in the valid transitions. This prevents SKIP → AUTH transitions at transaction boundaries, which contradicts the userTransactionStart formula in shorthands_start.tex that expects type 4 transactions without access lists to start with AUTH after a SKIP phase (e.g., following a SYSI transaction). The sanity check is missing + txAuth_{i+1}.
🔬 Verification Test
Why verification test was not possible: This is a LaTeX specification document. The inconsistency is evident by comparing line 5 (txSkip + txWarm + txAuth + txInit = 1) which allows AUTH, with line 7's sanity check (txSkip + txWarm + txInit = 1) which omits AUTH. The shorthands_start.tex line 10 expects [1 - txWarm_{i-1} - txAuth_{i-1}] * txAuth_i to detect transaction starts from SKIP → AUTH transitions.
| \item \label{hub: system: hub stamp: increments: WARM case} \If $\txWarm _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + 1$ | ||
| \item \label{hub: system: hub stamp: increments: INIT case} \If $\txInit _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekContext _{i}$ | ||
| \item \label{hub: system: hub stamp: increments: FINL case} \If $\txFinl _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekContext _{i}$ | ||
| \item \label{hub: system: hub stamp: increments: AUTH case} \If $\txAuth _{i} = 1$ \Then $\hubStamp _{i + 1} = \hubStamp _{i} + \peekAuthorization _{i + 1} + \txInit _{i + 1}$ |
There was a problem hiding this comment.
AUTH hub stamp increment missing txSkip transition term
High Severity
The AUTH phase hub stamp increment rule specifies hubStamp_{i+1} = hubStamp_i + peekAuthorization_{i+1} + txInit_{i+1}, but this doesn't account for the AUTH → SKIP transition. When transitioning from AUTH to SKIP (for type 4 transactions without EVM execution), peekAuthorization_{i+1} = 0 and txInit_{i+1} = 0, resulting in no increment. However, the transition constraint in transition.tex establishes that txSkip_{i+1} + txInit_{i+1} = peekTransaction_{i+1}, and formal.tex expects SKIP rows to satisfy hubStamp_i = hubStamp_{i-1} + peekTransaction_i. The increment rule is missing + txSkip_{i+1} to maintain consistency with the AUTH → SKIP transition.
🔬 Verification Test
Why verification test was not possible: This is a LaTeX specification document defining ZK-EVM constraints. The inconsistency is demonstrated by tracing the AUTH → SKIP transition: according to transition.tex lines 23-24, when txAuth_i = 1 and transitioning to SKIP, we have txSkip_{i+1} + txInit_{i+1} = peekTransaction_{i+1}, so peekTransaction_{i+1} = 1. The formal.tex SKIP entry (line 4) expects hubStamp_i = hubStamp_{i-1} + peekTransaction_i = hubStamp_{i-1} + 1, but the AUTH increment rule gives hubStamp_i = hubStamp_{i-1} + 0 + 0 = hubStamp_{i-1}.
Note
Implements EIP‑7702 authorization/delegation in the HUB spec and wires it into transaction flow.
txAuthphase: Addstx_authorization/(intro, generalities, constraints) to process authorization tuples viapeekAuthorization→peekAccount, gated byauthEcrecoverSuccess.auth*address/nonce/code-hash/delegation flags) and account rows (accDelegationAddress{Hi,Lo},accDelegationAddressNew{Hi,Lo},accIsDelegated{,New}).txAuth; delegated accounts have code size\delegatedAccountCodeSize. Addsxkeyvalmacros:accSetDelegationAddress,accSameDelegationAddress.TXAUTH/txAuth; updates phase binarities, legality, transitions, start shorthands, and transition graph; adjustshubStampincrement rules fortxAuth.sysi._all_hub.texand_inputs.tex; extendsenv.sty/common.stywith symbols and constants.Written by Cursor Bugbot for commit 328e293. This will update automatically on new commits. Configure here.