Conversation
Signed-off-by: F Bojarski <[email protected]>
Signed-off-by: F Bojarski <[email protected]>
Signed-off-by: F Bojarski <[email protected]>
Signed-off-by: F Bojarski <[email protected]>
| \begin{enumerate} | ||
| \item \If $\locAuthorizationPrefix _{i} = 1$ \Then | ||
| \ob{We require a constraint that connects \rlpTxnCommonColumnNumberOfAuthorization{} | ||
| to an eponymous column in the $\isTxn{}$-perspective.} |
There was a problem hiding this comment.
Required constraint explicitly marked as missing TODO
High Severity
Constraint item 1 contains a red TODO marker (\ob{}) stating "We require a constraint that connects \rlpTxnCommonColumnNumberOfAuthorization to an eponymous column in the \isTxn{}-perspective." This explicitly documents a missing constraint that is required but not specified. Without this linkage, the number of authorizations from transaction data won't be properly available during authorization list processing.
There was a problem hiding this comment.
@OlivierBBB we can discard thos no ? \rlpTxnCommonColumnNumberOfAuthorization is a common colun, so no need to duplicate it in the txn perpective ?
| \left\{ \begin{array}{lclr} | ||
| \locAuthorizationIndex _{i - 1} & = & 0 & (\sanityCheck) \\ | ||
| \locAuthorizationIndex _{i} & = & 0 \\ | ||
| \locAuthorizationIndex _{i + 1} & = & 1 \vspace{2mm} \\ |
There was a problem hiding this comment.
Empty authorization list causes unsatisfiable constraints
High Severity
The specification cannot handle type-4 transactions with empty authorization lists. Line 45 unconditionally sets \locAuthorizationIndex _{i + 1} = 1 when entering the phase, but line 97 requires \locAuthorizationIndex = \rlpTxnCommonColumnNumberOfAuthorizations to exit. Combined with the monotonicity constraint (line 62) that only allows the index to increase, if NumberOfAuthorizations is 0, the index becomes 1 and can never return to 0, making the exit condition unsatisfiable.
Additional Locations (1)
There was a problem hiding this comment.
that's the aim, yes.
OlivierBBB
left a comment
There was a problem hiding this comment.
Several comments, also made some changes to the counter of authorization tuples.
pkg/rlp_txn_v2.sty
Outdated
|
|
||
| \newcommand{\rlpTxnCommonColumnReplayProtection} {\col{REPLAY\_PROTECTION}} | ||
| \newcommand{\rlpTxnCommonColumnYparity} {\col{Y\_PARITY}} | ||
| \newcommand{\rlpTxnCommonColumnNumberOfAuthorization} {\col{NUMBER\_OF\_AUTHORIZATION}} |
There was a problem hiding this comment.
Is that the number of an authorization tuple in the authorization list ? If so the name we use in the HUB and the RLP_TXN module is TUPLE_INDEX.
Edit. Since this column is constant the above doesn't apply. The only comment I would make is spelling, it has to be pural
\newcommand{\rlpTxnCommonColumnNumberOfAuthorizations} {\col{NUMBER\_OF\_AUTHORIZATIONS}}
There was a problem hiding this comment.
+1 for "s"
rlp_txn/columns/shared.tex
Outdated
| \markAsJustifiedHere{} | ||
| \rlpTxnCommonColumnNumberOfAuthorization{}: | ||
| the number of authorization in the authorization list; | ||
| \end{enumerate} No newline at end of file |
There was a problem hiding this comment.
BTW we also (currently) count the number of auth tuples in the HUB: as it stands the HUB counts, for every type 4 transaction
- the number of authorization tuples
- the number of valid authorization tuples with
sender == authority
Counting the valid ones with address collision in the HUB makes sense. I will remove the generic counting from the HUB as counting it in RLP_TXN makes more sense.
There was a problem hiding this comment.
Is this column constant for the transaction ? Is it a countdown ? I ask this question in light of my
\rlpTxntransactionColumnLengthOfAuthorizationList
comment
There was a problem hiding this comment.
yes, \rlpTxnCommonColumnNumberOfAuthorization{}: is transaction constant (and must be 0 for non-7702 txs)
rlp_txn/generalities/constancies.tex
Outdated
| \item \CFI | ||
| \item \rlpTxnCommonColumnReplayProtection | ||
| \item \rlpTxnCommonColumnYparity | ||
| \item \rlpTxnCommonColumnNumberOfAuthorization |
There was a problem hiding this comment.
So \rlpTxnCommonColumnNumberOfAuthorization isn't a countdown given it's tx-constant.
| } | ||
| \end{center} | ||
|
|
||
| We constrain \locAuthorizationIndex to increase by at most one: |
There was a problem hiding this comment.
Missing braces to separate the macro from "to"
... \locAuthorizationIndex{} to ...
| \end{array} \right. | ||
| \] | ||
|
|
||
| \saNote{} We don't require any counter constancy for those columns. No newline at end of file |
There was a problem hiding this comment.
Do we have a constraint imposing that authorization lists are nonempty ? Likely something à la
If
TYPE_4[i] = true
is_first_row_of_phase_y[i] = true
Then
PHASE_AUTHORIZATION[i - 1] = trueShould do.
There was a problem hiding this comment.
yes, the "listCantBeEmpty" bit of the rlpization of the prefix of the authorization list
There was a problem hiding this comment.
Cursor comment is right (Spurious text appended to section description)
There was a problem hiding this comment.
Is there no constraint imposing that \locAuthorizationIndex _{i} should start at the value 1 for the first authorization tuple ?
Should we not impose e.g.
If AUTHORIZATION_PHASE[i - 1] = faux and AUTHORIZATION_PHASE[i] = true Then auth_index[i] = 1
If AUTHORIZATION_PHASE[i - 1] = true and AUTHORIZATION_PHASE[i] = true Then auth_index[i] is one of { auth_index[i - 1], 1 + auth_index[i - 1] }
Or do we know for sure that auth_index[i - 1] = 0 if i is the row where you compute the RLP prefix for the entire auth list ? If that is the case we should state it. Currently I'm not sure we couldn't start at the value auth_index = 13 for instance.
| \phaseAuthorizationList _{i + 1} & = & 1 \\ | ||
| \phaseAuthorizationList _{i + 10} & = & 1 \\ | ||
| \phaseAuthorizationList _{i + \locAuthorizationNumberOfRows} & = & 1 \\ | ||
| \end{array} \right. |
There was a problem hiding this comment.
Authorization list constraints unsatisfiable for empty lists
High Severity
The authorization list constraints are unsatisfiable when rlpTxnCommonColumnNumberOfAuthorizations is 0 (empty list). Constraint 2 unconditionally sets locAuthorizationIndex[i+1] = 1 and forces the phase to last at least locAuthorizationNumberOfRows (19) rows. However, constraint 5 requires locAuthorizationIndex = numberOfAuthorizations when exiting the phase. For an empty list (count=0), these constraints contradict each other - the index is forced to 1 but must equal 0 to exit. No constraint forbids empty authorization lists for type-4 transactions.
Additional Locations (1)
|
|
||
| \ob{TODO: We require a constraint that connects \rlpTxnCommonColumnNumberOfAuthorizations{} | ||
| to an eponymous column in the $\isTxn{}$-perspective.} | ||
| \end{enumerate} |
There was a problem hiding this comment.
Missing constraint connecting authorization count to transaction data
High Severity
The code contains an explicit TODO (lines 11-12) marking a required but missing constraint: "We require a constraint that connects \rlpTxnCommonColumnNumberOfAuthorizations to an eponymous column in the \isTxn-perspective." Without this constraint, the authorization count column is never actually set from transaction data for type-4 transactions, yet this value is used to control when authorization tuple processing terminates.
a2bf987 to
a9d5cbb
Compare
|
|
||
| \ob{TODO: We require a constraint that connects \rlpTxnCommonColumnNumberOfAuthorizations{} | ||
| to an eponymous column in the $\isTxn{}$-perspective.} | ||
| \end{enumerate} |
There was a problem hiding this comment.
Missing constraint leaves NumberOfAuthorizations unvalidated for type-4 transactions
High Severity
The constraint at lines 8-13 has an empty body after \If $\locAuthorizationPrefix _{i} = 1$ \Then - only a TODO comment exists where the actual constraint should be. This means \rlpTxnCommonColumnNumberOfAuthorizations is never connected to actual transaction data for type-4 transactions. While non-type-4 transactions force this to 0, type-4 transactions allow any prover-supplied positive value. This is a soundness issue where the count of authorization tuples processed may not match the actual transaction.
| \If $\locAuthorizationPrefix _{i} = 1$ \Then | ||
| \[ | ||
| \left\{ \begin{array}{lclr} | ||
| \locAuthorizationIndex _{i - 1} & = & 0 \\ |
There was a problem hiding this comment.
? the previous row is a TXN row tuple_index is a CMP row. This has to be deleted imho.
| \locAuthorizationIndex _{i + 1} & = & 1 \vspace{2mm} \\ | ||
| \isCmp _{i + 1} & = & 1 \vspace{2mm} \\ | ||
| \phaseAuthorizationList _{i + 1} & = & 1 \\ | ||
| \phaseAuthorizationList _{i + 10} & = & 1 \\ |
There was a problem hiding this comment.
what is this +10 about ?
There was a problem hiding this comment.
The above is a precaution to have checkpoints that are 100% reachable in any trace from the current vantage point to prevent early exits from the current phase. It's related to how constraints with large offsets get ignored if the trace runs out of rows such as how certain CALL constraints get clipped due to the presence of large MODEXP related shifts.
There are 1 + 3 rows per follow-up phase where integer rlp-utils calls are done on y, r, s. Three such phases are expected and must follow the current phase, so we are guaranteed that 12 rows must follow after the first CMP row of the AUTHORIZATION_LIST phase. The constraint with offset 10 falls squarely in that range and forces there to be at least 10 + 12 rows past the current vantage point.
The 3rd checkpoint isn't strictly speaking necessary due to this and will already be covered by the constraint saying that if tuple_index ≠ NUMBER_OF_AUTHORIZATIONS then IS_AUTHORIZATION[i + 19] = 1.
E.g. implemented as follows
(defconst
AUTHORIZATION_PHASE___1ST_CHECKPOINT_OFFSET 1
AUTHORIZATION_PHASE___2ND_CHECKPOINT_OFFSET 10
AUTHORIZATION_PHASE___3RD_CHECKPOINT_OFFSET 19
)
(defconstraint authority-list-phase---ensuring-minimum-phase-length (:guard ...)
(begin
(eq! (shift IS_AUTHORIZATION_LIST AUTHORIZATION_PHASE___1ST_CHECKPOINT_OFFSET ) 1)
(eq! (shift IS_AUTHORIZATION_LIST AUTHORIZATION_PHASE___2ND_CHECKPOINT_OFFSET ) 1)
(eq! (shift IS_AUTHORIZATION_LIST AUTHORIZATION_PHASE___3RD_CHECKPOINT_OFFSET ) 1)
))| \locAuthorizationIndex _{i - 1} & = & 0 \\ | ||
| \locAuthorizationIndex _{i} & = & 0 \\ | ||
| \locAuthorizationIndex _{i + 1} & = & 1 \vspace{2mm} \\ | ||
| \isCmp _{i + 1} & = & 1 \vspace{2mm} \\ |
There was a problem hiding this comment.
We can keep only of the two folowing: we have general constrains that a phase change <=> TXN row.
| where $\ell$ is the length of the \texttt{authorization\_list} in the | ||
| current ``set code transaction'' i.e. $\ell \equiv \rlpTxnCommonColumnNumberOfAuthorizations$. | ||
| \item\label{rlp txn: phase constraints: authorization list: constraints: monotonicity of tuple index} | ||
| \If $\phaseAuthorizationList _{i - 1} = \true$ \Then $\locAuthorizationIndex _{i} \in \{ \locAuthorizationIndex _{i - 1}, 1 + \locAuthorizationIndex _{i - 1} \}$ |
There was a problem hiding this comment.
why not using shorthand again_CMP_row_of_auth_phase ? We have already the constraint for the two first rows: 0 and then 1.
| \Then | ||
| \[ | ||
| \left\{ \begin{array}{lcl} | ||
| \phaseAuthorizationList _{i + 1} & = & 1 \\ |
There was a problem hiding this comment.
one of the two is enough
There was a problem hiding this comment.
I mean one of the CMP or IS_AUTH_LIST, but the two offset are ok.
| \locAuthorizationLengthCountdown _{i} & \define & \rlpTxnComputationColumnAuxiliaryData {1} _{i} \\ | ||
| \locAuthorizationItemCountdown _{i} & \define & \rlpTxnComputationColumnAuxiliaryData {2} _{i} \\ | ||
| \locAuthorizationIndex _{i} & \define & \rlpTxnComputationColumnCounterConstantAuxiliaryData {1} _{i} \\ | ||
| \locAuthorizationChainId _{i} & \define & \rlpTxnComputationColumnCounterConstantAuxiliaryData {2} _{i} \\ |
| We enforce that authorization lists must be nonempty | ||
| \begin{enumerate}[resume] | ||
| \item\label{rlp txn: phase constraints: authorization list: constraints: authorization lists must be nonempty} | ||
| $\rlpTxnCommonColumnNumberOfAuthorizations _{i} \neq 0$ |
| \rlpProcessInteger { | ||
| anchorRow = i , | ||
| relOffset = \yellowm{1} , | ||
| integerHi = 0 , |
There was a problem hiding this comment.
chainId Hi as well ?
| \end{enumerate} | ||
| And a finalization constraint: | ||
| \begin{enumerate}[resume] | ||
| \item \If $\phaseEnd _{i} = 1$ \Then $\locAuthorizationLengthCountdown _{i} = 0$ |



Note
Medium Risk
Medium risk because it extends core
rlp_txnconstraint/spec logic with a new transaction type, new phase transitions, and new counters/columns; some of the new authorization-list constraints still contain TODO/incomplete pieces that could leave behavior underspecified.Overview
Adds support for 7702 transactions by enabling
typeFourTxand introducing a new\phaseAuthorizationListphase (plusNUMBER_OF_AUTHORIZATIONS) across therlp_txncolumn definitions and general constraints.Updates phase flag sums, binarity/constancy requirements, LT/LX participation, and transaction-type-specific phase-transition/RLP-component constraints to account for the new phase, and documents that 7702 txs cannot be deployment transactions.
Introduces a new
phase_constraints/authorization_list/*section defining shorthands and RLP-ization/tuple-index/countdown constraints for authorization lists, adjusts auxiliary data column counts accordingly, and removes obsoleteaccess_list/constraints.texplus a staleversion.md.Written by Cursor Bugbot for commit a9d5cbb. This will update automatically on new commits. Configure here.