diff --git a/Makefile b/Makefile index 28d29255..045e4b26 100644 --- a/Makefile +++ b/Makefile @@ -32,6 +32,7 @@ mxp: view-mxp oob: view-oob prc: view-prc rlp_addr: view-rlp_addr +rlp_auth: view-rlp_auth rlp_patterns: view-rlp_patterns rlp_txn: view-rlp_txn rlp_txnrcpt: view-rlp_txnrcpt @@ -70,6 +71,7 @@ rmxp: recompile-mxp roob: recompile-oob rprc: recompile-prc rrlp_addr: recompile-rlp_addr +rrlp_auth: recompile-rlp_auth rrlp_patterns: recompile-rlp_patterns rrlp_txn: recompile-rlp_txn rrlp_txnrcpt: recompile-rlp_txnrcpt diff --git a/gas/lookups/into_wcp.tex b/gas/lookups/into_wcp.tex index 4c721511..b7b3234c 100644 --- a/gas/lookups/into_wcp.tex +++ b/gas/lookups/into_wcp.tex @@ -4,23 +4,23 @@ \item[Source columns:] we use the following: \begin{multicols}{3} \begin{enumerate} + \item $\wcpInst _{i}$ \item $0$ \item $\wcpArgOneLo _{i}$ \item $0$ \item $\wcpArgTwoLo _{i}$ \item $\wcpRes _{i}$ - \item $\wcpInst _{i}$ \end{enumerate} \end{multicols} \item[Target columns:] we use the following: \begin{multicols}{3} \begin{enumerate} + \item $\INST _{j}$ \item $\argOneHi _{j}$ \item $\argOneLo _{j}$ \item $\argTwoHi _{j}$ \item $\argTwoLo _{j}$ - \item $\resLo _{j}$ - \item $\INST _{j}$ + \item $\res _{j}$ \end{enumerate} \end{multicols} \end{description} diff --git a/mxp/lua/decision_tree.lua.tex b/mxp/lua/decision_tree.lua.tex index 093a9ce4..dd15f6f2 100644 --- a/mxp/lua/decision_tree.lua.tex +++ b/mxp/lua/decision_tree.lua.tex @@ -11,7 +11,7 @@ \usepackage{../../pkg/flags_stamps_selectors} \usetikzlibrary{arrows.meta} \begin{document} -\input{mxp_v3/_local} +\input{mxp/_local} \input{hub/instruction_handling/create/_local} \begin{tikzpicture} \def\BAS {-3} diff --git a/pkg/column_generator.py b/pkg/column_generator.py index 58d5eb3d..a73d62da 100644 --- a/pkg/column_generator.py +++ b/pkg/column_generator.py @@ -66,6 +66,7 @@ "invalid": "invalid", # rlp modules "rlpAddr": "address Rlp", + "rlpAuth": "authorization Rlp", "rlpTxn": "transaction Rlp", "rlpTxnRcpt": "transaction Receipt Rlp", "rlpUtils": "rlp Utils", diff --git a/pkg/flags_stamps_selectors.sty b/pkg/flags_stamps_selectors.sty index 1fb7a58c..227cc8fc 100644 --- a/pkg/flags_stamps_selectors.sty +++ b/pkg/flags_stamps_selectors.sty @@ -1575,6 +1575,31 @@ \newcommand{\iRlpAddrSelect}{\imported{\rlpAddrSelect}} \newcommand{\stackDecRlpAddrFlag}{\stackInstructionDecodedColumn{\rlpAddrFlag}} +% authorization rlp columns: +%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\rlpAuthMod}{\col{RLPAUTH}} + +\newcommand{\rlpAuthSTAMP}{\col{AUTHORIZATION\_RLP\_STAMP}} +\newcommand{\rlpAuthStamp}{\col{RLPAUTH}\stamp} +\newcommand{\iRlpAuthSTAMP}{\imported{\rlpAuthSTAMP}} +\newcommand{\iRlpAuthStamp}{\imported{\rlpAuthStamp}} +\newcommand{\rlpAuthRevStamp}{\col{RLPAUTH}\stamp\,\col{REV}} +\newcommand{\iRlpAuthRevStamp}{\imported{\rlpAuthRevStamp}} + +\newcommand{\rlpAuthFLAG}{\col{AUTHORIZATION\_RLP\_FLAG}} +\newcommand{\rlpAuthFlag}{\col{RLPAUTH}\flag} +\newcommand{\decRlpAuthFLAG}{\decoded{\rlpAuthFLAG}} +\newcommand{\decRlpAuthFlag}{\decoded{\rlpAuthFlag}} +\newcommand{\idecRlpAuthFLAG}{\imported{\decRlpAuthFLAG}} +\newcommand{\idecRlpAuthFlag}{\imported{\decRlpAuthFlag}} + +\newcommand{\rlpAuthSELECT}{\col{AUTHORIZATION\_RLP\_SELECTOR}} +\newcommand{\rlpAuthSelect}{\col{RLPAUTH}\select} +\newcommand{\iRlpAuthSELECT}{\imported{\rlpAuthSELECT}} +\newcommand{\iRlpAuthSelect}{\imported{\rlpAuthSelect}} +\newcommand{\stackDecRlpAuthFlag}{\stackInstructionDecodedColumn{\rlpAuthFlag}} + % transaction rlp columns: %%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/pkg/rlp_auth.sty b/pkg/rlp_auth.sty new file mode 100644 index 00000000..5992857e --- /dev/null +++ b/pkg/rlp_auth.sty @@ -0,0 +1,104 @@ +\newcommand{\computation} {\col{CMPTN}} +\newcommand{\computationPerspectivePrefix} {\col{computation}} +\newcommand{\macro} {\col{MACRO}} +\newcommand{\macroPerspectivePrefix} {\col{macro}} +\newcommand{\extern} {\col{XTERN}} +\newcommand{\externPerspectivePrefix} {\col{xtern}} +\newcommand{\utils} {\col{UTILS}} +\newcommand{\utilsPerspectivePrefix} {\col{utils}} +\newcommand{\authority} {\col{AUTHORITY}} +\newcommand{\address} {\col{ADDRESS}} +\newcommand{\signature} {\col{SIGNATURE}} +\newcommand{\signatureY} {\col{\signature\_Y}} +\newcommand{\signatureR} {\col{\signature\_R}} +\newcommand{\signatureS} {\col{\signature\_S}} +\newcommand{\transactionFromAddress} {\col{TXN\_FROM\_}\address} +\newcommand{\authorityTupleIndex} {\col{TUPLE\_INDEX}} +\newcommand{\tuple} {TUPLE} +\newcommand{\isValidTupleName} {\authority\col{\_\tuple\_IS\_VALID}} +\newcommand{\authorityEcrecoverAttempt} {\authority\col{\_ECRECOVER\_ATTEMPT}} +\newcommand{\authorityEcrecoverSuccess} {\authority\col{\_ECRECOVER\_SUCCESS}} +\newcommand{\senderIsAuthority} {\col{SENDER\_IS\_}\authority} +\newcommand{\addressIsZeroAddress} {\col{ADDRESS\_IS\_ZERO\_ADDRESS}} +\newcommand{\transactionTypeWithAuthorityLists} {\col{TXN\_WITH\_AUTHORITY\_LIST}} +\newcommand{\transactionTypeSansAuthorityLists} {\col{TXN\_SANS\_AUTHORITY\_LIST}} +\newcommand{\authorityIsSenderAcc} {\col{AUTHORITY\_IS\_SENDER\_ACC}} +\newcommand{\authorityIsSenderTot} {\col{AUTHORITY\_IS\_SENDER\_TOT}} + + +\newcommand{\chainIdHiName} {\chainId\_HI} +\newcommand{\chainIdLoName} {\chainId\_LO} +\newcommand{\addressHiName} {\address\_HI} +\newcommand{\addressLoName} {\address\_LO} +\newcommand{\yparityName} {\signatureY} +\newcommand{\rhiName} {\signatureR\_HI} +\newcommand{\rloName} {\signatureR\_LO} +\newcommand{\shiName} {\signatureS\_HI} +\newcommand{\sloName} {\signatureS\_LO} +\newcommand{\authorityHiName} {\authority\_HI} +\newcommand{\authorityLoName} {\authority\_LO} +\newcommand{\transactionFromAddressHi} {\transactionFromAddress\_HI} +\newcommand{\transactionFromAddressLo} {\transactionFromAddress\_LO} +\newcommand{\authorityNonce} {\authority\_NONCE} +\newcommand{\authorizationTupleNonce} {\tuple\_NONCE} +\newcommand{\networkChainId} {NETWORK\_\chainId} +\newcommand{\networkChainIdHi} {\networkChainId\_HI} +\newcommand{\networkChainIdLo} {\networkChainId\_LO} + + +\newcommand{\rlpAuthMacroColumn}[1] {\macroPerspectivePrefix\separator\col{#1}} +\newcommand{\rlpAuthMacroChainIdHi} {\rlpAuthMacroColumn{\tuple\_\chainIdHiName}} +\newcommand{\rlpAuthMacroChainIdLo} {\rlpAuthMacroColumn{\tuple\_\chainIdLoName}} +\newcommand{\rlpAuthMacroAddressHi} {\rlpAuthMacroColumn{\tuple\_\addressHiName}} +\newcommand{\rlpAuthMacroAddressLo} {\rlpAuthMacroColumn{\tuple\_\addressLoName}} +\newcommand{\rlpAuthMacroNonce} {\rlpAuthMacroColumn{\authorizationTupleNonce}} +\newcommand{\rlpAuthMacroSignatureYparity} {\rlpAuthMacroColumn{\tuple\_\yparityName}} +\newcommand{\rlpAuthMacroSignatureRhi} {\rlpAuthMacroColumn{\tuple\_\rhiName}} +\newcommand{\rlpAuthMacroSignatureRlo} {\rlpAuthMacroColumn{\tuple\_\rloName}} +\newcommand{\rlpAuthMacroSignatureShi} {\rlpAuthMacroColumn{\tuple\_\shiName}} +\newcommand{\rlpAuthMacroSignatureSlo} {\rlpAuthMacroColumn{\tuple\_\sloName}} +\newcommand{\rlpAuthMacroAuthorityTupleIndex} {\rlpAuthMacroColumn{\authorityTupleIndex}} + + +\newcommand{\rlpAuthExternColumn}[1] {\externPerspectivePrefix\separator\col{#1}} +\newcommand{\rlpAuthExternAuthorityEcrecoverAttempt} {\rlpAuthExternColumn{\authorityEcrecoverAttempt}} +\newcommand{\rlpAuthExternAuthorityRecoverySuccess} {\rlpAuthExternColumn{\authorityEcrecoverSuccess}} +\newcommand{\rlpAuthExternAuthorityTupleIsValid} {\rlpAuthExternColumn{\isValidTupleName}} +\newcommand{\rlpAuthExternTupleAddressHi} {\rlpAuthExternColumn{\addressHiName}} +\newcommand{\rlpAuthExternTupleAddressLo} {\rlpAuthExternColumn{\addressLoName}} +\newcommand{\rlpAuthExternAuthorityAddressHi} {\rlpAuthExternColumn{\authorityHiName}} +\newcommand{\rlpAuthExternAuthorityAddressLo} {\rlpAuthExternColumn{\authorityLoName}} +\newcommand{\rlpAuthExternTransactionFromAddressHi} {\rlpAuthExternColumn{\transactionFromAddressHi}} +\newcommand{\rlpAuthExternTransactionFromAddressLo} {\rlpAuthExternColumn{\transactionFromAddressLo}} +\newcommand{\rlpAuthExternSenderIsAuthority} {\rlpAuthExternColumn{\senderIsAuthority}} +\newcommand{\rlpAuthExternAddressIsZeroAddress} {\rlpAuthExternColumn{\addressIsZeroAddress}} +\newcommand{\rlpAuthExternAuthorityNonce} {\rlpAuthExternColumn{\authorityNonce}} +\newcommand{\rlpAuthExternNetworkChainIdHi} {\rlpAuthExternColumn{\networkChainIdHi}} +\newcommand{\rlpAuthExternNetworkChainIdLo} {\rlpAuthExternColumn{\networkChainIdLo}} +\newcommand{\rlpAuthExternPotentialNewCodeHashHi} {\rlpAuthExternColumn{\codeHash}\col{\_HI}} +\newcommand{\rlpAuthExternPotentialNewCodeHashLo} {\rlpAuthExternColumn{\codeHash}\col{\_LO}} + + + +\newcommand{\rlpAuthUtilsColumn}[1] {\utilsPerspectivePrefix\separator\col{#1}} +\newcommand{\rlpAuthUtilsColumnIsMagic} {\rlpAuthUtilsColumn{IS\_MAGIC}} +\newcommand{\rlpAuthUtilsColumnIsPrefix} {\rlpAuthUtilsColumn{IS\_PREFIX}} +\newcommand{\rlpAuthUtilsColumnIsChainId} {\rlpAuthUtilsColumn{IS\_CHAIN\_ID}} +\newcommand{\rlpAuthUtilsColumnIsAddress} {\rlpAuthUtilsColumn{IS\_ADDRESS}} +\newcommand{\rlpAuthUtilsColumnIsNonce} {\rlpAuthUtilsColumn{IS\_NONCE}} +\newcommand{\rlpAuthUtilsColumnLimbBit} {\rlpAuthUtilsColumn{LIMB\_BIT}} +\newcommand{\rlpAuthUtilsColumnLimb} {\rlpAuthUtilsColumn{LIMB}} +\newcommand{\rlpAuthUtilsColumnLimbSize} {\rlpAuthUtilsColumn{LIMB\_SIZE}} +\newcommand{\rlpAuthUtilsColumnExoDataColumn}[1] {\rlpAuthUtilsColumn{DATA\_#1}} +\newcommand{\rlpAuthUtilsColumnRlpUtilsFlag} {\rlpAuthUtilsColumn{\rlpUtilsMod\_FLAG}} +\newcommand{\rlpAuthUtilsColumnRlpUtilsInstruction} {\rlpAuthUtilsColumn{\rlpUtilsMod\_INST}} +\newcommand{\rlpAuthUtilsColumnSizeCountdown} {\rlpAuthUtilsColumn{BYTE\_SIZE\_COUNTDOWN}} + + +\newcommand{\rlpAuthComputationColumn}[1] {\computationPerspectivePrefix\separator\col{#1}} +\newcommand{\rlpAuthComputationInst} {\rlpAuthComputationColumn{INST}} +\newcommand{\rlpAuthComputationArgOneHi} {\rlpAuthComputationColumn{ARG\_1\_HI}} +\newcommand{\rlpAuthComputationArgOneLo} {\rlpAuthComputationColumn{ARG\_1\_LO}} +\newcommand{\rlpAuthComputationArgTwoHi} {\rlpAuthComputationColumn{ARG\_2\_HI}} +\newcommand{\rlpAuthComputationArgTwoLo} {\rlpAuthComputationColumn{ARG\_2\_LO}} +\newcommand{\rlpAuthComputationRes} {\rlpAuthComputationColumn{RES}} diff --git a/pkg/rlp_tx.sty b/pkg/rlp_tx.sty index 50e2c106..75eef67b 100644 --- a/pkg/rlp_tx.sty +++ b/pkg/rlp_tx.sty @@ -21,8 +21,8 @@ \newcommand{\indexx} {\col{INDEX\_LX}} \newcommand{\rlptsize} {\col{RLP\_LT\_BYTESIZE}} \newcommand{\rlpxsize} {\col{RLP\_LX\_BYTESIZE}} -\newcommand{\ltByteSizeCountDown} {\col{LT\_BYTE\_SIZE\_COUNTDOWN}} -\newcommand{\lxByteSizeCountDown} {\col{LX\_BYTE\_SIZE\_COUNTDOWN}} +\newcommand{\ltByteSizeCountdown} {\col{LT\_BYTE\_SIZE\_COUNTDOWN}} +\newcommand{\lxByteSizeCountdown} {\col{LX\_BYTE\_SIZE\_COUNTDOWN}} \newcommand{\accsize} {\col{ACC\_BYTESIZE}} \newcommand{\indexData} {\col{INDEX\_DATA}} \newcommand{\dataGasCost} {\col{DATA\_GAS\_COST}} diff --git a/rlp_auth/_all_rlp_auth.tex b/rlp_auth/_all_rlp_auth.tex new file mode 100644 index 00000000..9ca1222d --- /dev/null +++ b/rlp_auth/_all_rlp_auth.tex @@ -0,0 +1,68 @@ +\documentclass[fleqn]{article} +\usepackage[dvipsnames]{xcolor} +\usepackage{xkeyval} +\usepackage{../pkg/xkeyval_macros/context} +\usepackage{../pkg/xkeyval_macros/transient} +% \usepackage{../pkg/xkeyval_macros/dom_sub_stamps} +% \usepackage{../pkg/xkeyval_macros/mmu_instructions} +% \usepackage{../pkg/xkeyval_macros/mxp_instructions} +% \usepackage{../pkg/xkeyval_macros/oob_instructions} +% \usepackage{../pkg/xkeyval_macros/stp_instructions} +% \usepackage{../pkg/xkeyval_macros/misc_flag_sums} +\usepackage{../pkg/xkeyval_macros/wcp_calls} +% \usepackage{../pkg/xkeyval_macros/ext_calls} +% \usepackage{../pkg/xkeyval_macros/euc_calls} +% \usepackage{../pkg/xkeyval_macros/prc_calls} +\usepackage{../pkg/common} +\usepackage{../pkg/std} +\usepackage{../pkg/env} +\usepackage{../pkg/flags_stamps_selectors} +\usepackage{../pkg/instruction_flags} +\usepackage{../pkg/system} +\usepackage{../pkg/call_stack} +\usepackage{../pkg/IEEEtrantools} +\usepackage{../pkg/access} +\usepackage{../pkg/trm} +\usepackage{../pkg/alu_old} +\usepackage{../pkg/bin} +\usepackage{../pkg/call_stack} +\usepackage{../pkg/comparisons} +\usepackage{../pkg/exceptions} +\usepackage{../pkg/expansion} +\usepackage{../pkg/exponent} +\usepackage{../pkg/gas} +\usepackage{../pkg/offset_processor} +\usepackage{../pkg/oob} +\usepackage{../pkg/public} +\usepackage{../pkg/ram} +\usepackage{../pkg/rom} +\usepackage{../pkg/scenario} +\usepackage{../pkg/storage} +\usepackage{../pkg/warm} +\usepackage{../pkg/wc3} +\usepackage{../pkg/shifting} +\usepackage{../pkg/precompiles} +\usepackage{../pkg/rlp_auth} +\usepackage{../pkg/rlp_tx} +\usepackage{../pkg/rlp_txn_v2} +\usepackage{../pkg/rlp_log} +\usepackage{../pkg/rlp_patterns} +\usepackage{../pkg/txn_data} +\usepackage{../pkg/rlp_utils} +\usepackage{../pkg/block_data} +\usepackage{../pkg/subsubsubsection} +\usepackage{../pkg/iomf_done} + +\usepackage{../pkg/draculatheme} + +\title{Transaction \rlpAuthMod{} module} +\author{\arithmetizationTeam{}} +\date{September 2025} + +\begin{document} + +\maketitle +\tableofcontents +\input{_inputs} + +\end{document} diff --git a/rlp_auth/_design_notes/keccak.md b/rlp_auth/_design_notes/keccak.md new file mode 100644 index 00000000..449840a0 --- /dev/null +++ b/rlp_auth/_design_notes/keccak.md @@ -0,0 +1,127 @@ +We may want to perform the KECCAK independently. In this case we may want to select the following columns + +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| USER_TXN_NUMBER | TUPLE_INDEX | IS_RESULT | KECCAK_HI | KECCAK_LO | IS_DATA | LIMB_INDEX | LIMB | nBYTES | LIMB_CONSTRUCTED | notes | RLP_UTILS instruction | +|:---------------:|:-----------:|:---------:|:---------:|:---------:|:-------:|:----------:|:----:|:------:|:----------------:|----------------|----------------------:| +| n | a | | msg_hi | msg_lo | | | | | | | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| n | a | | | | 1 | 0 | | 1 | | magic | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| n | a | | | | 1 | 1 | | 1/2 | | rlp prefix | BYTE_STRING_PREFIX | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| n | a | | | | 1 | 2 | | 1/0 | ? | chain id | INTEGER | +| n | a | | | | 1 | 3 | | ? | ? | 1 / 2 / 3 rows | | +| n | a | | | | 1 | 4 | | ? | ? | | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| n | a | | | | 1 | 5 | | 1 | | address | ADDRESS | +| n | a | | | | 1 | 6 | | 4 | | 3 rows | | +| n | a | | | | 1 | 7 | | 16 | | | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| +| n | a | | | | 1 | 8 | | 1/0 | ? | nonce | INTEGER | +| n | a | | | | 1 | 9 | | 0 | | 1 / 2 rows | | +| n | a | | | | 1 | 10 | | ? | ? | | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|------|--------|------------------|----------------|-----------------------| + +For a total of +- at least 6 limbs of data +- and up to 10 limbs of data + +The selector would likely be something à la +- ATTEMPT_ECRECOVER ∙ [MACRO + UTILS] (yet to be defined binary column, that is AUTHORITY_TUPLE constant, and set on the MACRO row) +- for IS_RESULT we would take `MACRO` +- for IS_DATA we would take `UTILS ∙ utils/LIMB_CONSTRUCTED` + +So a typical operation may look like so + +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| USER_TXN_NUMBER | TUPLE_INDEX | IS_RESULT | KECCAK_HI | KECCAK_LO | IS_DATA | LIMB_INDEX | LIMB | nBYTES | LIMB_CONSTRUCTED | notes | RLP_UTILS instruction | +|:---------------:|:-----------:|:---------:|:---------:|:---------:|:-------:|:----------:|:---------------------------------------------------|:------:|:----------------:|-----------------|----------------------:| +| n | a | 1 | 0xff..ff | 0xff..ff | | | | | | | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| n | a | | | | 1 | 0 | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | magic | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| n | a | | | | 1 | 1 | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | rlp prefix | BYTE_STRING_PREFIX | +| | | | | | | | | | | 0x9d ≡ 128 + 29 | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| n | a | | | | 1 | 2 | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | chain id | INTEGER | +| n | a | | | | 1 | | | | | 2 rows | | +| n | a | | | | 1 | 3 | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | 1 | 0x83 ≡ 128 + 3 | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| n | a | | | | 1 | 4 | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | address | ADDRESS | +| n | a | | | | 1 | 5 | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | 1 | 3 rows | | +| n | a | | | | 1 | 6 | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | 1 | 0x94 ≡ 128 + 20 | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| +| n | a | | | | 1 | 7 | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | nonce | INTEGER | +| n | a | | | | 1 | | | | | 2 rows | | +| n | a | | | | 1 | 8 | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | 1 | 0x82 ≡ 128 + 2 | | +|-----------------|-------------|-----------|-----------|-----------|---------|------------|----------------------------------------------------|--------|------------------|-----------------|-----------------------| + +Note: as per usual empty cells either don't matter or contain 0's + +And translate, after filtering (`XXX → φ_XXX`) to + +|-------------------|---------------|---------|---------------------|------------------|------------------|------------------|------------------|--------------------------------------|------------------------|------------------------|---------------|--------------|----------------------------------------------------|----------|--------------------| +| φ_USER_TXN_NUMBER | φ_TUPLE_INDEX | φ_MACRO | φ_macro/SIGNATURE_Y | φ_SIGNATURE_R_HI | φ_SIGNATURE_R_LO | φ_SIGNATURE_S_HI | φ_SIGNATURE_S_LO | φ_extern/AUTHORITY_ECRECOVER_SUCCESS | φ_AUTHORITY_ADDRESS_HI | φ_AUTHORITY_ADDRESS_LO | φ_IS_DATA (?) | φ_LIMB_INDEX | φ_LIMB | φ_nBYTES | φ_LIMB_CONSTRUCTED | +|:-----------------:|:-------------:|--------:|:-------------------:|:----------------:|:----------------:|:----------------:|:----------------:|:------------------------------------:|:----------------------:|:----------------------:|:-------------:|:------------:|:---------------------------------------------------|:--------:|:------------------:| +| n | a | | | | | | | | | | | | | | | +| n | a | | | | | | | | | | | | | | | +| n | a | | | | | | | | | | | 0 | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 1 | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 2 | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 3 | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | | +| n | a | | | | | | | | | | | 4 | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 5 | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | | +| n | a | | | | | | | | | | | 6 | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | | +| n | a | | | | | | | | | | | 7 | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 8 | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | | +|-------------------|---------------|---------|---------------------|------------------|------------------|------------------|------------------|--------------------------------------|------------------------|------------------------|---------------|--------------|----------------------------------------------------|----------|--------------------| + +Where + + = 0xaabbccdd (no padding, trimmed) ≡ address[:4] + = 0xaabbccdd (no padding, trimmed) ≡ address[4:] + +You would be ok with + +| signature data | result | limbs | limb_size | index | +|----------------|---------------|----------------------------------------------------|:---------:|:-----:| +| | | | | | +| | | | | | +| | | | | | +| | | | | | +| | | | | | +| | | | | | +| | | | | | +| | | | | | +| | | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 0 | +| | | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | +| | | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 2 | +| | | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | 3 | +| | | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 4 | +| | | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | 5 | +| | | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | 6 | +| | | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 7 | +| | | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | 8 | + + +| is_signature_data | is_result | is_result | limbs | limb_size | index | +|-------------------|-----------|-----------|----------------------------------------------------|:---------:|:-----:| +| | | | | | 0 | +| | | | | | 1 | +| | | | | | 2 | +| | | | | | 3 | +| | | | | | 4 | +|-------------------|-----------|-----------|----------------------------------------------------|-----------|-------| +| | | | | | 0 | +| | | | | | 1 | +| | | | | | 2 | +|-------------------|-----------|-----------|----------------------------------------------------|-----------|-------| +| | | | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 0 | +| | | | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | +| | | | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 2 | +| | | | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | 3 | +| | | | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 4 | +| | | | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | 5 | +| | | | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | 6 | +| | | | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 7 | +| | | | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | 8 | diff --git a/rlp_auth/_design_notes/todo.md b/rlp_auth/_design_notes/todo.md new file mode 100644 index 00000000..bbb9b77f --- /dev/null +++ b/rlp_auth/_design_notes/todo.md @@ -0,0 +1,304 @@ +# Module structure + +A likely good structure for the module is + +|-----------|--------|-----------|--------------------------------| +| | | CT_MAX | notes | +|-----------|--------|:---------:|--------------------------------| +| WCP | rows * | | | +| | | | This comprises both | +| | | | . MANDATORY PRECONDITIONS | +| | | | . VALIDITY CHECK COMPARISONS | +|-----------|--------|:---------:|--------------------------------| +| MACRO | row | 0 | +|-----------|--------|:---------:|--------------------------------| +| RLP_UTILS | rows * | | | +| | | | processing phase columns: | +| | | | . IS_MAGIC | +| | | | . IS_GLOBAL_PREFIX | +| | | | . IS_CHAIN_ID | +| | | | . IS_ADDRESS | +|-----------|--------|-----------|--------------------------------|-------------------------| +| ∅ | ∅ | ∅ | | Not part of the message | +| | | | | | +| | | | | | +|-----------|--------|-----------|--------------------------------|-------------------------| + +The idea is to carry out all steps of the above +- we do the MANDATORY PRECONDITIONS WCP CHECKS +- we do the VALIDITY WCP CHECKS + +we then define + + valid_chain_id ≡ chain_id_is_0 ∨ chain_id_is_β + call_ec_recover ≡ valid_chain_id ∧ valid_nonce_bound + call_keccak_on_rlp ≡ call_ec_recover + +we impose + + If call_ec_recover ≡ Then AUTHORITY_RECOVERY_SUCCESS ≡ false + If call_ec_recover ≡ Then AUTHORITY_RECOVERY_SUCCESS ≡ + +at this point all constraints will be written assuming "If AUTHORITY_RECOVERY_SUCCESS ≡ " +also the fields + + macro/AUTHORITY_NONCE + macro/AUTHORITY_HAS_CODE + macro/AUTHORITY_IS_DELEGATED + +must be meaningful. +This could be done directly through a lookup `RLP_AUTH → HUB.account/`. +We may want to impose a sanity check constraints setting them to 0 otherwise, histoire de fixer les idées. + +|---------------------------------------------|-------|------------------------------------------------------|--------------|-------------------------------------------------------| +| `RLP_AUTH` columns | notes | `HUB` columns | notes | | +|---------------------------------------------|:-----:|------------------------------------------------------|:------------:|-------------------------------------------------------| +| 1 | | hub.DELEGATION | | | +| rlp_auth.USER_TXN_NUMBER | ✓ | hub.USER_TXN_NUMBER | | | +| rlp_auth.macro/AUTHORITY_TUPLE_INDEX | ✓ | hub.delegation/AUTHORITY_TUPLE_INDEX | | | +| rlp_auth.macro/AUTHORITY_RECOVERY_SUCCESS | ✓ | hub.delegation/AUTHORITY_RECOVERY_SUCCESS | | defines whether to load account next or not | +|---------------------------------------------|:-----:|------------------------------------------------------|:------------:|-------------------------------------------------------| +| rlp_auth.macro/AUTHORITY_HI | ✓ | hub.delegation/AUTHORITY_HI | | | +| rlp_auth.macro/AUTHORITY_LO | ✓ | hub.delegation/AUTHORITY_LO | | | +| rlp_auth.macro/ADDRESS_HI | ✓ | hub.delegation/POTENTIALLY_NEW_DELEGATION_ADDRESS_HI | | hub.account/DELEGATION_ADDRESS_HI_NEW will also exist | +| rlp_auth.macro/ADDRESS_LO | ✓ | hub.delegation/POTENTIALLY_NEW_DELEGATION_ADDRESS_LO | | hub.account/DELEGATION_ADDRESS_LO_NEW | +| rlp_auth.macro/ADDRESS_IS_ZERO_ADDRESS | ✓ | hub.delegation/POTENTIALLY_RESET_DELEGATION | | | +| rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_HI | ✓ | hub.delegation/POTENTIALLY_NEW_CODE_HASH_HI | | new columns: place where to write potential updated | +| rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_LO | ✓ | hub.delegation/POTENTIALLY_NEW_CODE_HASH_LO | | code hash | +|---------------------------------------------|:-----:|------------------------------------------------------|--------------|-------------------------------------------------------| +| rlp_auth.macro/AUTHORITY_NONCE | ⟦ π ⟧ | hub.delegation/AUTHORITY_NONCE | justif. here | read off (potential) upcoming account/ row | +| rlp_auth.macro/AUTHORITY_HAS_CODE | ⟦ π ⟧ | hub.delegation/AUTHORITY_HAS_CODE | justif. here | | +| rlp_auth.macro/AUTHORITY_IS_DELEGATED | ⟦ π ⟧ | hub.delegation/AUTHORITY_IS_DELEGATED | justif. here | | +|---------------------------------------------|:-----:|------------------------------------------------------|--------------|-------------------------------------------------------| +| rlp_auth.macro/PROCEED_WITH_DELEGATION | mixed | hub.delegation/PROCEED_WITH_DELEGATION | | used to decide whether to do something or not | +|---------------------------------------------|-------|------------------------------------------------------|--------------|-------------------------------------------------------| + +One way to do it in the HUB is as follows: + +| perspective | AUTHORITY_RECOVERY_SUCCESS | notes | +|-------------|:--------------------------:|----------------------------| +| DELEGATION | | no address, no account row | +|-------------|----------------------------|----------------------------| +| DELEGATION | | | +| ACCOUNT | | load account | +|-------------|----------------------------|----------------------------| +| DELEGATION | | | +| ACCOUNT | | load account | +|-------------|----------------------------|----------------------------| +| DELEGATION | | | +|-------------|----------------------------|----------------------------| +| DELEGATION | | | +|-------------|----------------------------|----------------------------| +| DELEGATION | | | +| ACCOUNT | | load account | +|-------------|----------------------------|----------------------------| + +This way we don't have to create this effective index (AUTHORITY_RECOVERY_SUCCESS_ACCUMULATOR). + +Now that we have the currently true nonce and other information such as whether the account is delegated or not we proceed: + + authority_code_is_empty_or_already_delegated ≡ (1 - macro/AUTHORITY_HAS_CODE) ∨ macro/AUTHORITY_IS_DELEGATED + proceed_with_delegation ≡ authority_code_is_empty_or_already_delegated ∧ nonce_agreement + + rlp_auth.macro/PROCEED_WITH_DELEGATION ≡ proceed_with_delegation + +# Lookups + +## Lookup to WCP + +We need comparisons (ali ≡ authority list item) to verify MANDATORY PRECONDITIONS + +|-----------------|--------------|----------|-----|-----------------------| +| WCP instruction | arg1 | arg2 | res | note | +|-----------------|--------------|----------|-----|-----------------------| +| GEQ | ali.chain_id | 0 | | result must be | +| LT | ali.nonce | 1 << 64 | | result must be | +| LT | ali.address | 1 << 20 | | result must be | +| LT | ali.y_parity | 1 << 8 | | result must be | +| LT | ali.r | 1 << 256 | | result must be | +| LT | ali.s | 1 << 256 | | result must be | +|-----------------|--------------|----------|-----|-----------------------| + + +We also need comparisons that are VALIDITY CHECK COMPARISONS (that are ALLOWED TO FAIL) + +|-----------------|---------------|------------------|-------------------------|--------------------------------------------------------------------| +| WCP instruction | arg1 | arg2 | res | note | +|-----------------|---------------|------------------|-------------------------|--------------------------------------------------------------------| +| ISZERO | ali.chain_id | | chain_id_is_0 | | +| EQ | ali.chain_id | β | chain_id_is_β | | +| LT | ali.nonce | (2 << 64) - 1 | valid_nonce_bound | | +| LT | ali.s | secp256k1 / 2 | valid_s_bound | | +| EQ | ali.nonce | hub.acc/NONCE | nonce_agreement | potentially compare ali.nonce with acc/nonce + SENDER_IS_AUTHORITY | +| EQ | ali.authority | txndata.hub/FROM | sender_is_authority | | +| ISZERO | ali.address | | address_is_zero_address | | +|-----------------|---------------|------------------|-------------------------|--------------------------------------------------------------------| + + +## RLP-ization of authority list tuples + +We need to RLP-ize the authority list. Recall that these are of the form + +authority_list ≡ [ authority_item, authority_item...] +authority_item ≡ [ chain_id, address, nonce, y_parity, r, s ] + +With +- chain_id ≡ integer, 32B at most, rlp-ization: 1B to 33B +- address ≡ address, 20B exactly, rlp-ization: 21B +- nonce ≡ integer, 8B at most, rlp-ization: 1B to 9B +- y_parity ≡ integer, 1B at most, rlp-ization: 1B or 2B +- r ≡ integer, 32B at most, rlp-ization: 1B to 33B +- s ≡ integer, 32B at most, rlp-ization: 1B to 33B + +so that + +ζ ≡ RLP( chain_id ) ∙ RLP( address ) ∙ RLP( nonce ) ∙ RLP( y_parity ) ∙ RLP( r ) ∙ RLP( s ) ∈ B_k + +where k ∈ {25, ..., 122}. So that + +RLP( authority_item ) ≡ RLP( ζ ) +≡ ∙ ζ + +and so we must call `RLP_UTILS` for + +|-----------------------|---------------|-------| +| RLP_UTILS instruction | argument | notes | +|-----------------------|---------------|-------| +| BYTESTRING | global prefix | | +| INTEGER | chain_id | | +| ADDRESS | address | | +| INTEGER | nonce | | +| INTEGER | y_parity | | +| INTEGER | r | | +| INTEGER | s | | +|-----------------------|---------------|-------| + +and for the whole list + +RLP( authority_list ) ≡ ∙ RLP( item_1 ) ∙ RLP( item_2 ) ∙ ⋯ ∙ RLP( item_n ) + +## Lookup to BLOCK_DATA + +We need to justify the network chain id β. + +## Lookup to TXN_DATA + +The goals of this lookup are to +- justify the transaction FROM address +- this is required so that we can justify `SENDER_IS_AUTHORITY` + +- selector: `rlp_auth.MACRO` +- correspondence: + +|-----------------------------|------------------------------| +| `RLP_AUTH` columns | `TXN_DATA` columns | +|-----------------------------|------------------------------| +| 1 | txn_data.HUB | +| 1 | txn_data.rlp/TYPE_4[-1] | +| rlp_auth.USER_TXN_NUMBER | txn_data.USER_TXN_NUMBER | +| rlp_auth.macro/AUTHORITY_HI | rlp_data.hub/FROM_ADDRESS_HI | +| rlp_auth.macro/AUTHORITY_LO | rlp_data.hub/FROM_ADDRESS_LO | +|-----------------------------|------------------------------| + +## Lookup RLP_AUTH → RLP_TXN + +This lookup ensures that the `RLP_AUTH` module does not deal with more authorization list tuples than required. +Unclear at the moment whether this is necessary. + +- selector: `rlp_auth.MACRO` +- correspondence: + +|--------------------------------|-------------------------------| +| `RLP_AUTH` columns | `RLP_TXN` columns | +|--------------------------------|-------------------------------| +| 1 | rlp_txn.AUTH | +| rlp_auth.USER_TXN_NUMBER | rlp_txn.USER_TXN_NUMBER | +| rlp_auth.AUTHORITY_TUPLE_INDEX | rlp_txn.AUTHORITY_TUPLE_INDEX | +|--------------------------------|-------------------------------| + +## Lookup RLP_TXN → RLP_AUTH + +This lookup provides the `RLP_AUTH` with its instructions. + +- selector: `rlp_txn.AUTH`, the AUTH "subperspective" is yet to be specified +- correspondence: + +|-------------------------------------------|---------------------------------------------|------------------------------| +| `RLP_TXN` columns | `RLP_AUTH` columns | notes | +|-------------------------------------------|---------------------------------------------|------------------------------| +| 1 | rlp_auth.MACRO | | +| rlp_txn.USER_TXN_NUMBER | rlp_auth.USER_TXN_NUMBER | | +| rlp_txn.auth/AUTHORITY_TUPLE_INDEX | rlp_auth.AUTHORITY_TUPLE_INDEX | | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/CHAIN_ID_HI | rlp_auth.macro/CHAIN_ID_HI | raw data from the | +| rlp_txn.auth/CHAIN_ID_LO | rlp_auth.macro/CHAIN_ID_LO | authorization list | +| rlp_txn.auth/ADDRESS_HI | rlp_auth.macro/ADDRESS_HI | | +| rlp_txn.auth/ADDRESS_LO | rlp_auth.macro/ADDRESS_LO | | +| rlp_txn.auth/ACCESS_TUPLE_NONCE | rlp_auth.macro/ACCESS_TUPLE_NONCE | | +| rlp_txn.auth/SIGNATURE_Y | rlp_auth.macro/SIGNATURE_Y | | +| rlp_txn.auth/SIGNATURE_R_HI | rlp_auth.macro/SIGNATURE_R_HI | | +| rlp_txn.auth/SIGNATURE_R_LO | rlp_auth.macro/SIGNATURE_R_LO | | +| rlp_txn.auth/SIGNATURE_S_HI | rlp_auth.macro/SIGNATURE_S_HI | | +| rlp_txn.auth/SIGNATURE_S_LO | rlp_auth.macro/SIGNATURE_S_LO | | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/PROCEED_WITH_DELEGATION | rlp_auth.macro/PROCEED_WITH_DELEGATION | | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/AUTHORITY_RECOVERY_SUCCESS | rlp_auth.macro/AUTHORITY_RECOVERY_SUCCESS | | +| rlp_txn.auth/AUTHORITY_HI | rlp_auth.macro/AUTHORITY_HI | | +| rlp_txn.auth/AUTHORITY_LO | rlp_auth.macro/AUTHORITY_LO | | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/SENDER_IS_AUTHORITY | rlp_auth.macro/SENDER_IS_AUTHORITY | | +| rlp_txn.auth/ADDRESS_IS_ZERO_ADDRESS | rlp_auth.macro/ADDRESS_IS_ZERO_ADDRESS | | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/AUTHORITY_NONCE | rlp_auth.macro/AUTHORITY_NONCE | read from the HUB | +| rlp_txn.auth/AUTHORITY_HAS_CODE | rlp_auth.macro/AUTHORITY_HAS_CODE | read from the HUB | +| rlp_txn.auth/AUTHORITY_IS_DELEGATED | rlp_auth.macro/AUTHORITY_IS_DELEGATED | read from the HUB | +|-------------------------------------------|---------------------------------------------|------------------------------| +| rlp_txn.auth/POTENTIALLY_NEW_CODE_HASH_HI | rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_HI | either empty code hash | +| rlp_txn.auth/POTENTIALLY_NEW_CODE_HASH_LO | rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_LO | or KEC( ef0100 ∙
) | +|-------------------------------------------|---------------------------------------------|------------------------------| + +## Lookup RLP_AUTH -> HUB + +To transmit to transmit the access list tuple to the HUB. It also +The `HUB` should operate under the same order as the transaction has its stuff RLP-ized: +1. access list +2. authorization list + +- selector: `sel ≡ rlp_txn.AUTH ∙ rlp_txn.auth/AUTHORITY_RECOVERY_SUCCESS` +- correspondence: + +|---------------------------------------------|------------------------------------------------------|-------------------------------------------------------| +| RLP_AUTH columns | HUB columns | notes | +|---------------------------------------------|------------------------------------------------------|-------------------------------------------------------| +| 1 | hub.auth | | +| rlp_auth.USER_TXN_NUMBER | hub.USER_TXN_NUMBER | | +| rlp_auth.macro/AUTHORITY_TUPLE_INDEX | hub.delegation/AUTHORITY_TUPLE_INDEX | | +| rlp_auth.macro/PROCEED_WITH_DELEGATION | hub.delegation/PROCEED_WITH_DELEGATION | used to decide whether to do something or not | +| rlp_auth.macro/ADDRESS_HI | hub.delegation/POTENTIALLY_NEW_DELEGATION_ADDRESS_HI | hub.account/DELEGATION_ADDRESS_HI_NEW will also exist | +| rlp_auth.macro/ADDRESS_LO | hub.delegation/POTENTIALLY_NEW_DELEGATION_ADDRESS_LO | hub.account/DELEGATION_ADDRESS_LO_NEW | +| rlp_auth.macro/ADDRESS_IS_ZERO_ADDRESS | hub.delegation/POTENTIALLY_RESET_DELEGATION | | +| rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_HI | hub.delegation/POTENTIALLY_NEW_CODE_HASH_HI | new columns: place where to write potential updated | +| rlp_auth.macro/POTENTIALLY_NEW_CODE_HASH_LO | hub.delegation/POTENTIALLY_NEW_CODE_HASH_LO | code hash | +|---------------------------------------------|------------------------------------------------------|-------------------------------------------------------| +| rlp_auth.macro/AUTHORITY_HI | hub.delegation/ADDRESS_HI | | +| rlp_auth.macro/AUTHORITY_LO | hub.delegation/ADDRESS_LO | | +| rlp_auth.macro/AUTHORITY_NONCE | hub.delegation/NONCE | | +| rlp_auth.macro/AUTHORITY_HAS_CODE | hub.delegation/HAS_CODE | | +| rlp_auth.macro/AUTHORITY_IS_DELEGATED | hub.delegation/IS_DELEGATED | hub.account/IS_DELEGATED_NEW will also exist | +|---------------------------------------------|------------------------------------------------------|-------------------------------------------------------| + +## Counting [SENDER ≡ AUTHORITY] + +We should have the standard couple +- SENDER_IS_AUTHORITY_BIT → lives in a single rlp_auth.macro/ row, must be something like `rlp_auth.MACRO ∙ rlp_auth.macro/PROCEED_WITH_DELEGATION ∙ sender_is_authority` +- SENDER_IS_AUTHORITY_ACC → as follows + - initialized at 0 (when `rlp_auth.USER_TRANSACTION_NUMBER` just changed) + - is `AUTHORITY_LIST_ITEM`-constant + - gets updated by the BIT otherwise +- SENDER_IS_AUTHORITY_TOT + +## Unique sorting of transactions + +We could either prove monotonicity of `rlp_auth.USER_TRANSACTION_NUMBER` (don't like it) +We could alternatively have two regimes: `rlp_auth.TXN_SUPPORTS_AUTHORITY_LIST` vs `rlp_auth.TXN_DOESNT_SUPPORT_AUTHORITY_LIST` and deal with all transaction in the present module diff --git a/rlp_auth/_inputs.tex b/rlp_auth/_inputs.tex new file mode 100644 index 00000000..d9dd5aaf --- /dev/null +++ b/rlp_auth/_inputs.tex @@ -0,0 +1,10 @@ +\input{_local} +\section{Introduction} \label{rlp auth: intro} \input{intro} +\section{Column descriptions} \label{rlp auth: column descriptions} \input{columns/_inputs} +\section{Generalities} \label{rlp auth: generalities} \input{generalities/_inputs} +\section{Specialized constraints} \label{rlp auth: specialized constraints} \input{specialized/_inputs} +\section{Graphical representation} \label{rlp auth: graphical representation} \input{lua/_inputs} +\section{Comparisons} \label{rlp auth: comparisons} \input{comparisons/_inputs} +\section{\rlpUtilsMod{} constraints} \label{rlp auth: rlp utils} \input{utils/_inputs} +\section{Specialized constraints} \label{rlp auth: specialized} \input{specialized/_inputs} +\section{Lookups} \label{rlp auth: lookups} \input{lookups/_inputs} diff --git a/rlp_auth/_local.tex b/rlp_auth/_local.tex new file mode 100644 index 00000000..e3a3dc5d --- /dev/null +++ b/rlp_auth/_local.tex @@ -0,0 +1,184 @@ +\def\locUtilsFlagSum {\loc{utils\_flag\_sum}} + +% mandatory checks +\def\roffCompMandatoryChainId {\roffConstYellow{(-13)}} +\def\roffCompMandatoryNonce {\roffConstYellow{(-12)}} +\def\roffCompMandatoryAddress {\roffConstYellow{(-11)}} +\def\roffCompMandatoryYparity {\roffConstYellow{(-10)}} +\def\roffCompMandatorySignatureRwellformed {\roffConstYellow{(-9)}} +\def\roffCompMandatorySignatureSwellformed {\roffConstYellow{(-8)}} +% validity checks +\def\roffCompValidityChainIdIszero {\roffConstYellow{(-7)}} +\def\roffCompValidityChainIdVsNetworkChainId {\roffConstYellow{(-6)}} +\def\roffCompValidityNonceEipBound {\roffConstYellow{(-5)}} +\def\roffCompValiditySignatureSnonMalleabilityBound {\roffConstYellow{(-4)}} +\def\roffCompValidityNonceVsAccountNonce {\roffConstYellow{(-3)}} +\def\roffCompValidityAuthorityVsSender {\roffConstYellow{(-2)}} +\def\roffCompValidityAddressIszero {\roffConstYellow{(-1)}} +% macro instruction +\def\roffCompMacroRow {\roffConstYellow{0}} +% extern row +\def\roffCompExternRow {\roffConstYellow{1}} +% RLP_UTILS calls +\def\roffRlpUtilsMagic {\roffConstYellow{2}} +\def\roffRlpUtilsPrefix {\roffConstYellow{3}} +\def\roffRlpUtilsChainId {\roffConstYellow{4}} +\def\roffRlpUtilsAddress {\roffConstYellow{7}} +\def\roffRlpUtilsNonce {\roffConstYellow{10}} + +\def\locMagicByte {\numConst{MAGIC}} +\def\locMagicByteValue {\numConst{0x05}} +\def\locAthorizationCodePrefixValue {\numConst{0xef0001}} +\def\locAthorizationCodePrefix {\numConst{code\_prefix}} + + +\def\locHi {\loc{\_hi}} +\def\locLo {\loc{\_lo}} +\def\locChainId {\loc{chain\_id}} +\def\locChainIdHi {\locChainId\locHi} +\def\locChainIdLo {\locChainId\locLo} +\def\locNetworkChainId {\loc{network\_}\locChainId} +\def\locNetworkChainIdHi {\locNetworkChainId\locHi} +\def\locNetworkChainIdLo {\locNetworkChainId\locLo} +\def\locAddress {\loc{address}} +\def\locAddressHi {\locAddress\locHi} +\def\locAddressLo {\locAddress\locLo} +\def\locSignature {\loc{sig\_}} +\def\locSignatureR {\locSignature\loc{r}} +\def\locSignatureS {\locSignature\loc{s}} +\def\locSignatureY {\locSignature\loc{y\_parity}} +\def\locSignatureRhi {\locSignatureR\locHi} +\def\locSignatureRlo {\locSignatureR\locLo} +\def\locSignatureShi {\locSignatureS\locHi} +\def\locSignatureSlo {\locSignatureS\locLo} +\def\locAuthority {\loc{authority}} +\def\locAuthorityAddress {\locAuthority\loc{\_}\locAddress} +\def\locAuthorityAddressHi {\locAuthorityAddress\locHi} +\def\locAuthorityAddressLo {\locAuthorityAddress\locLo} +\def\locNonce {\loc{nonce}} +\def\locAuthorityNonce {\locAuthority\loc{\_}\locNonce} +\def\locSenderAddress {\loc{sender\_address}} +\def\locMagic {\loc{MAGIC}} +\def\locSecpPrime {\loc{secpk1n\_prime}} +\def\locSecpPrimeOverTwo {\locSecpPrime\loc{\_over\_2}} +\def\locSecpPrimeOverTwoHi {\locSecpPrimeOverTwo\locHi} +\def\locSecpPrimeOverTwoLo {\locSecpPrimeOverTwo\locLo} +\def\locNonceEqualsAuthorityNonce {\locNonce\loc{\_equals\_}\locAuthority\loc{\_}\locNonce} +\def\locFromAddress {\loc{from\_address}} +\def\locFromAddressHi {\locFromAddress\locHi} +\def\locFromAddressLo {\locFromAddress\locLo} +\def\locAddressIsZero {\locAddress\loc{\_is\_zero}} +\def\locAuthorityIsSender {\locAuthority\loc{\_is\_sender}} +\def\locAuthorityTupleIsValidExpression {\locAuthority\loc{\_tuple\_is\_valid}} +\def\locCtMaxSum {\loc{ct\_max\_sum}} +\def\locWeightedPerspectiveSum {\loc{wght\_persp\_sum}} + + +\def\locChainIdIszero {\locChainId\loc{\_is\_zero}} +\def\locChainIdIsNetworkChainId {\locChainId\loc{\_is\_beta}} +\def\locChainIdIsZeroOrBeta {\locChainId\loc{\_is\_zero\_or\_beta}} +\def\locNonceSatisfiesEipBound {\locNonce\loc{\_satisfies\_EIP-2681\_bound}} +\def\locSignatureSisNonMalleable {\locSignatureS\loc{\_is\_non\_malleable}} +\def\locCallEcrecoverExpression {\loc{call\_ecrecover\_expression}} + +\def\mandatoryComparisonsStandingHypothesis { + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\chainIdIsZeroStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\chainIdIsNetworkChainIdStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\nonceEipCheckStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\stringentSignatureSCheckStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\nonceAgreementStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\authorityIsSenderStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\addressIsZeroStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + +\def\shorthandsStandingHypothesis{ + \begin{center} + \boxed{\text{The shorthands defined below require } + \macro _{i + \roffCompMacroRow} = 1 + } + \end{center} +} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +\def\magicRlpPrefixStandingHypothesis{ + \begin{center} + \boxed{\text{The constraints below assume that } + \left\{ \begin{array}{lcl} + \macro _{i + \roffCompMacroRow} & = & \true \\ + \rlpAuthExternAuthorityEcrecoverAttempt _{i + \roffCompMacroRow} & = & \true \\ + \end{array} \right. + } + \end{center} +} +\def\rlpPrefixStandingHypothesis {\magicRlpPrefixStandingHypothesis} +\def\tupleChainIdStandingHypothesis {\magicRlpPrefixStandingHypothesis} +\def\tupleAddressStandingHypothesis {\magicRlpPrefixStandingHypothesis} +\def\tupleNonceStandingHypothesis {\magicRlpPrefixStandingHypothesis} + + + +\def\rlpAuthCtmaxComputation {\numConst{ct\_max\_computation}} \def\rlpAuthNrowsComputationValue {\numConst{13}} \def\rlpAuthCtmaxComputationValue {\rlpAuthNrowsComputationValue - 1} +\def\rlpAuthCtmaxMacro {\numConst{ct\_max\_macro}} \def\rlpAuthNrowsMacroValue {\numConst{1}} \def\rlpAuthCtmaxMacroValue {\rlpAuthNrowsMacroValue - 1} +\def\rlpAuthCtmaxExtern {\numConst{ct\_max\_extern}} \def\rlpAuthNrowsExternValue {\numConst{1}} \def\rlpAuthCtmaxExternValue {\rlpAuthNrowsExternValue - 1} +\def\rlpAuthCtmaxUtils {\numConst{ct\_max\_utils}} \def\rlpAuthNrowsUtilsValue {\numConst{12}} \def\rlpAuthCtmaxUtilsValue {\rlpAuthNrowsUtilsValue - 1} +\def\rlpAuthCtmaxNoop {\numConst{ct\_max\_noop}} \def\rlpAuthNrowsNoopValue {\numConst{1}} \def\rlpAuthCtmaxNoopValue {\rlpAuthNrowsNoopValue - 1} diff --git a/rlp_auth/columns/_inputs.tex b/rlp_auth/columns/_inputs.tex new file mode 100644 index 00000000..b2604193 --- /dev/null +++ b/rlp_auth/columns/_inputs.tex @@ -0,0 +1,5 @@ +\subsection{Common columns \lispTodo{}} \input{columns/common} +\subsection{\computation{}-columns \lispTodo{}} \input{columns/computation} +\subsection{\macro{}-columns \lispTodo{}} \input{columns/macro} +\subsection{\extern{}-columns \lispTodo{}} \input{columns/extern} +\subsection{\utils{}-columns \lispTodo{}} \input{columns/utils} diff --git a/rlp_auth/columns/common.tex b/rlp_auth/columns/common.tex new file mode 100644 index 00000000..272e0d08 --- /dev/null +++ b/rlp_auth/columns/common.tex @@ -0,0 +1,61 @@ +\begin{enumerate} + \item \iomf{}: + binary column; + separates \textbf{padding-rows} (characterized by $\iomf \equiv \false$) + from \textbf{non-padding-rows} (characterized by $\iomf \equiv \true$); + \item \blockNumber{}: + block number; + \item \userTransactionNumber{}: + user transaction number; + \item \authorityTupleIndex{}: + index of authorization tuple + in authorization list; + \item \ct{} and \maxCt{}: + usual counter columns; +\end{enumerate} +The following columns distinguish between (\user) transactions +whose underlying transaction type allow for +\textbf{authority lists} +and those that don't. +\begin{enumerate}[resume] + \item \transactionTypeWithAuthorityLists{}: + binary column; + \item \transactionTypeSansAuthorityLists{}: + binary column; +\end{enumerate} +The following columns define the perspectives of the present module. +\begin{enumerate}[resume] + \item \computation{}: + binary column defining the + \computationPerspectivePrefix{}-perspective; + \item \macro{}: + binary column defining the + \macroPerspectivePrefix{}-perspective; + \item \extern{}: + binary column defining the + \externPerspectivePrefix{}-perspective; + \item \utils{}: + binary column defining the + \utilsPerspectivePrefix{}-perspective; +\end{enumerate} +The following columns are used for book-keeping related to +authority tuples that \macroEcrecover{} the (transaction's) sender address. +\begin{enumerate}[resume] + \item + \authorityIsSenderAcc{}: + accumulates, within a given transaction, + the number of \textbf{valid} authority tuples + whose \authority{} address is the transaction's + sender address; + \item + \authorityIsSenderTot{}: + \textbf{transaction-constant} column + containing the total number of \textbf{valid} + authority tuples in a transaction's authority list + whose \authority{} address is the transaction's + sender address; +\end{enumerate} +\saNote{} +We provide more details on the difficulties that arise from authority tuples whose +\authority{} is the (transaction's) sender address +in note~(\ref{rlp auth: comparisons: validity: nonce vs account nonce: when authority is sender}). diff --git a/rlp_auth/columns/computation.tex b/rlp_auth/columns/computation.tex new file mode 100644 index 00000000..298fa8f1 --- /dev/null +++ b/rlp_auth/columns/computation.tex @@ -0,0 +1,12 @@ +The following colunms in the \computation{}-perspective require no further comment. +\begin{enumerate} + \item \rlpAuthComputationInst{} + \item \rlpAuthComputationArgOneHi{} + \item \rlpAuthComputationArgOneLo{} + \item \rlpAuthComputationArgTwoHi{} + \item \rlpAuthComputationArgTwoLo{} + \item \rlpAuthComputationRes{} +\end{enumerate} +\saNote{} +The \rlpAuthMod{} module serves these columns exclusively to the \wcpMod{} module, +see section~(\ref{rlp auth: lookup: into wcp}). diff --git a/rlp_auth/columns/extern.tex b/rlp_auth/columns/extern.tex new file mode 100644 index 00000000..383e9355 --- /dev/null +++ b/rlp_auth/columns/extern.tex @@ -0,0 +1,57 @@ +\begin{enumerate} + \item + $\rlpAuthExternAuthorityEcrecoverAttempt$: + binary column which is \true{} + \emph{iff} the module makes an attempt + at \macroEcrecover{}'ing the \authority{} address; + \item + $\rlpAuthExternAuthorityRecoverySuccess$: + binary column which is \true{} + \emph{iff} \macroEcrecover{} + returns an \authority{} address + rather than $\varnothing$; + \item + $\rlpAuthExternAuthorityTupleIsValid$: + binary column which is \true{} + \emph{iff} the authorization tuple is valid; + \item + $\rlpAuthExternTupleAddressHi$ and + $\rlpAuthExternTupleAddressLo$: + hi and lo parts of + the \authority{} address (potentially) extracted + from an authorization tuple; + \item + $\rlpAuthExternAuthorityAddressHi$ and + $\rlpAuthExternAuthorityAddressLo$: + hi and lo parts of + the \authority{} address (potentially) extracted + from an authorization tuple; + \item + $\rlpAuthExternTransactionFromAddressHi$ and + $\rlpAuthExternTransactionFromAddressLo$: + hi and lo parts of the + \transactionFromAddress{} + \item + $\rlpAuthExternSenderIsAuthority$: + binary column which is \true{} + \emph{iff} the authorization tuple is valid and + the transaction's sender coincides with the + \authority{} of the authorization tuple; + \item + $\rlpAuthExternAddressIsZeroAddress$: + binary column which is \true{} + \emph{iff} the authorization tuple is valid and + the \address{} of the authorization tuple + is the zero address $\texttt{0x\,00\,..\,00} \in \mathbb{B} _{\addressSize}$; + \item + $\rlpAuthExternAuthorityNonce$: + \emph{may} contain the \authority{} account's nonce; + \item + $\rlpAuthExternNetworkChainIdHi$ and + $\rlpAuthExternNetworkChainIdLo$: + contain respectively the hi/lo part of the network chain id $\beta$; + \item + $\rlpAuthExternPotentialNewCodeHashHi$ and + $\rlpAuthExternPotentialNewCodeHashLo$: + contain respectively the hi/lo part of the potentially new code hash of the delegated authority; +\end{enumerate} diff --git a/rlp_auth/columns/macro.tex b/rlp_auth/columns/macro.tex new file mode 100644 index 00000000..5e2e930b --- /dev/null +++ b/rlp_auth/columns/macro.tex @@ -0,0 +1,15 @@ +The following columns belong to the \macro-perspective. +Their contents are extracted from the \rlpTxnMod{} module. +As such their contents are labeled as ``\godGiven{}''. +\begin{enumerate} + \item \godGiven{}: $\rlpAuthMacroChainIdHi$ + \item \godGiven{}: $\rlpAuthMacroChainIdLo$ + \item \godGiven{}: $\rlpAuthMacroAddressHi$ + \item \godGiven{}: $\rlpAuthMacroAddressLo$ + \item \godGiven{}: $\rlpAuthMacroNonce$ + \item \godGiven{}: $\rlpAuthMacroSignatureYparity$ + \item \godGiven{}: $\rlpAuthMacroSignatureRhi$ + \item \godGiven{}: $\rlpAuthMacroSignatureRlo$ + \item \godGiven{}: $\rlpAuthMacroSignatureShi$ + \item \godGiven{}: $\rlpAuthMacroSignatureSlo$ +\end{enumerate} diff --git a/rlp_auth/columns/utils.tex b/rlp_auth/columns/utils.tex new file mode 100644 index 00000000..620b94fd --- /dev/null +++ b/rlp_auth/columns/utils.tex @@ -0,0 +1,36 @@ +The following colunms in the \utils{}-perspective require no further comment. +The \rlpAuthMod{} module serves these columns exclusively to the \rlpUtilsMod{} module, +see section~(\ref{rlp auth: lookup: into utils}). +\begin{enumerate} + \item \rlpAuthUtilsColumnLimbBit: + binary column; + turns on along \utils{}-rows containing a (nontrivial, finished) \limb{}; + \item \rlpAuthUtilsColumnLimb: + contains limbs; + \item \rlpAuthUtilsColumnLimbSize: + contains the number of significant bytes of \rlpAuthUtilsColumnLimb{}; + \item \rlpAuthUtilsColumnExoDataColumn{k}, for $k = 1, \dots, \numberOfRlpUtilsDataColumns$: + \item \rlpAuthUtilsColumnRlpUtilsFlag: + binary flag indicating when to trigger the lookup to the \rlpUtilsMod{} module; + \item \rlpAuthUtilsColumnRlpUtilsInstruction: + contains \rlpUtilsMod{}-module instructions; + \item \rlpAuthUtilsColumnSizeCountdown: + column that performs a countdown of the number of remaining bytes + to \rlp{}-ize; +\end{enumerate} +\saNote{} +As per usual, \limb{}'s are \textbf{left aligned on the $\llarge$-th byte}. + +\saNote{} +The purpose of the $(\rlpAuthUtilsColumnLimbBit, \rlpAuthUtilsColumnLimb, \rlpAuthUtilsColumnLimbSize)$ +tuples is that, +whenever $\rlpAuthUtilsColumnLimbBit = \true$, +$\rlpAuthUtilsColumnLimb$ contain a ``nonempty'' data limb left aligned (on the $\llarge$-th byte) +with $\rlpAuthUtilsColumnLimbSize$ many significant bytes (counting from the $\llarge$-th byte) +which, if concatenated together, make up the \rlp{}-string +\[ + \rlp\Big( \locChainId \Big) \cdot + \rlp\Big( \locAddress \Big) \cdot + \rlp\Big( \locNonce \Big) +\] + diff --git a/rlp_auth/comparisons/_inputs.tex b/rlp_auth/comparisons/_inputs.tex new file mode 100644 index 00000000..95e04e54 --- /dev/null +++ b/rlp_auth/comparisons/_inputs.tex @@ -0,0 +1,5 @@ +\subsection{Introduction \lispTodo{}} \label{rlp auth: comparisons: intro} \input{comparisons/intro} +\subsection{Shorthands \lispTodo{}} \label{rlp auth: comparisons: shorthands} \input{comparisons/shorthands} +\subsection{Mandatory autorization list tuple checks \lispTodo{}} \label{rlp auth: comparisons: mandatory checks} \input{comparisons/mandatory/_inputs} +\subsection{Authorization list tuple validity checks \lispTodo{}} \label{rlp auth: comparisons: validity checks} \input{comparisons/validity/_inputs} +\subsection{Justifying \externPerspectivePrefix-values \lispTodo{}} \label{rlp auth: comparisons: justifying extern values} \input{comparisons/setting} diff --git a/rlp_auth/comparisons/intro.tex b/rlp_auth/comparisons/intro.tex new file mode 100644 index 00000000..0ac4bea0 --- /dev/null +++ b/rlp_auth/comparisons/intro.tex @@ -0,0 +1,7 @@ +The first portion of processing an authorization list item is to perform various checks. +These checks fall into two categories: +\textbf{mandatory checks} that express that the +authorization list tuple is \textbf{well-formed}. +These checks are characterized by the requirement that they all pass (\resultMustBeTrueName). +\textbf{Validity checks} determine whether the authorization tuple is acted upon during transaction pre-processing. +Contrary to the first batch the required comparisons may or may not hold. diff --git a/rlp_auth/comparisons/mandatory/__01__chain_id_well_formed.tex b/rlp_auth/comparisons/mandatory/__01__chain_id_well_formed.tex new file mode 100644 index 00000000..1636fc1a --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__01__chain_id_well_formed.tex @@ -0,0 +1,26 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToGeq { + anchorRow = i , + relOffset = \roffCompMandatoryChainId , + argOneHi = \locChainIdHi , + argOneLo = \locChainIdLo , + argTwoHi = 0 , + argTwoLo = 0 , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatoryChainId , + } + \end{array} \right. +\] +\saNote{} +The above ensures the authorization tuple +\locChainId{}, +as given by its hi / lo decomposition +\locChainIdHi{} / \locChainIdLo{}, +is well-formed as an integer $\in\mathbb{N}_{256}$. diff --git a/rlp_auth/comparisons/mandatory/__02__nonce_8B_bound.tex b/rlp_auth/comparisons/mandatory/__02__nonce_8B_bound.tex new file mode 100644 index 00000000..bf8134a8 --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__02__nonce_8B_bound.tex @@ -0,0 +1,24 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \roffCompMandatoryNonce , + argOneHi = 0 , + argOneLo = \locNonce , + argTwoHi = 0 , + argTwoLo = 2^{64} , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatoryNonce , + } + \end{array} \right. +\] +\saNote{} +The above ensures that the authorization tuple +\locNonce{} +is well formed as an 8-byte integer. diff --git a/rlp_auth/comparisons/mandatory/__03__address_20B_bound.tex b/rlp_auth/comparisons/mandatory/__03__address_20B_bound.tex new file mode 100644 index 00000000..c02fcdf5 --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__03__address_20B_bound.tex @@ -0,0 +1,26 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \roffCompMandatoryAddress , + argOneHi = \locAddressHi , + argOneLo = \locAddressLo , + argTwoHi = 256^4 , + argTwoLo = 0 , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatoryAddress , + } + \end{array} \right. +\] +\saNote{} +The above ensures that the authorization tuple +\locAddress{}, +as given by its hi / lo decomposition +\locAddressHi{} / \locAddressLo{}, +is well formed as an address $\in \mathbb{B} _{\addressSize}$. diff --git a/rlp_auth/comparisons/mandatory/__04__y_parity_1B_bound.tex b/rlp_auth/comparisons/mandatory/__04__y_parity_1B_bound.tex new file mode 100644 index 00000000..2e625aee --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__04__y_parity_1B_bound.tex @@ -0,0 +1,24 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \roffCompMandatoryYparity , + argOneHi = 0 , + argOneLo = \locSignatureY , + argTwoHi = 0 , + argTwoLo = 2^8 , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatoryYparity , + } + \end{array} \right. +\] +\saNote{} +The above ensures that the authorization tuple's +\locSignatureY{} +is well formed as a 1-byte integer. diff --git a/rlp_auth/comparisons/mandatory/__05__signature_r_well_formed.tex b/rlp_auth/comparisons/mandatory/__05__signature_r_well_formed.tex new file mode 100644 index 00000000..2453d0ed --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__05__signature_r_well_formed.tex @@ -0,0 +1,27 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToGeq { + anchorRow = i , + relOffset = \roffCompMandatorySignatureRwellformed , + argOneHi = \locSignatureRhi , + argOneLo = \locSignatureRlo , + argTwoHi = 0 , + argTwoLo = 0 , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatorySignatureRwellformed , + } + \end{array} \right. +\] +\saNote{} +The above ensures that the authorization tuple's +\locSignatureR{}, +as given by its hi / lo decomposition +\locSignatureRhi{} / \locSignatureRlo{} +is well-formed as an integer $\in\mathbb{N}_{256}$. + diff --git a/rlp_auth/comparisons/mandatory/__06__signature_s_well_formed.tex b/rlp_auth/comparisons/mandatory/__06__signature_s_well_formed.tex new file mode 100644 index 00000000..0c53aa83 --- /dev/null +++ b/rlp_auth/comparisons/mandatory/__06__signature_s_well_formed.tex @@ -0,0 +1,27 @@ +\mandatoryComparisonsStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToGeq { + anchorRow = i , + relOffset = \roffCompMandatorySignatureSwellformed , + argOneHi = \locSignatureShi , + argOneLo = \locSignatureSlo , + argTwoHi = 0 , + argTwoLo = 0 , + } + \vspace{2mm} + \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \roffCompMandatorySignatureSwellformed , + } + \end{array} \right. +\] +\saNote{} +The above ensures that the authorization tuple's +\locSignatureS{}, +as given by its hi / lo decomposition +\locSignatureShi{} / \locSignatureSlo{}, +is well-formed as an integer $\in\mathbb{N}_{256}$. + diff --git a/rlp_auth/comparisons/mandatory/_inputs.tex b/rlp_auth/comparisons/mandatory/_inputs.tex new file mode 100644 index 00000000..9961d4cd --- /dev/null +++ b/rlp_auth/comparisons/mandatory/_inputs.tex @@ -0,0 +1,7 @@ +\subsubsection{Introduction \lispTodo{}} \label{rlp auth: comparisons: mandatory:intro} \input{comparisons/mandatory/intro} +\subsubsection{\locChainId{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: chain id well formed} \input{comparisons/mandatory/__01__chain_id_well_formed} +\subsubsection{\locNonce{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: nonce bound} \input{comparisons/mandatory/__02__nonce_8B_bound} +\subsubsection{\locAddress{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: address bound} \input{comparisons/mandatory/__03__address_20B_bound} +\subsubsection{\locSignatureY{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: y parity bound} \input{comparisons/mandatory/__04__y_parity_1B_bound} +\subsubsection{\locSignatureR{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: signature r well formed} \input{comparisons/mandatory/__05__signature_r_well_formed} +\subsubsection{\locSignatureS{} bound check \lispTodo{}} \label{rlp auth: comparisons: mandatory: signature s well formed} \input{comparisons/mandatory/__06__signature_s_well_formed} diff --git a/rlp_auth/comparisons/mandatory/intro.tex b/rlp_auth/comparisons/mandatory/intro.tex new file mode 100644 index 00000000..45936971 --- /dev/null +++ b/rlp_auth/comparisons/mandatory/intro.tex @@ -0,0 +1,4 @@ +In the present section we perform the following checks that are \textbf{required} to pass. +We refer the reader to \cite{EIP-7702}'s +\href{https://eips.ethereum.org/EIPS/eip-7702#set-code-transaction}{Set code transaction} +section. diff --git a/rlp_auth/comparisons/setting.tex b/rlp_auth/comparisons/setting.tex new file mode 100644 index 00000000..d39025ad --- /dev/null +++ b/rlp_auth/comparisons/setting.tex @@ -0,0 +1,8 @@ +Having carried out the aforementioned comparisons, we are in a position to +justify various fields from the \macroPerspectivePrefix-perspective. +\[ + \left\{ \begin{array}{lcl} + \rlpAuthExternAuthorityEcrecoverAttempt _{i + \roffCompMacroRow} & = & \locCallEcrecoverExpression \\ + \rlpAuthExternAuthorityTupleIsValid _{i + \roffCompMacroRow} & = & \locAuthorityTupleIsValidExpression \\ + \end{array} \right. +\] diff --git a/rlp_auth/comparisons/shorthands.tex b/rlp_auth/comparisons/shorthands.tex new file mode 100644 index 00000000..05af0949 --- /dev/null +++ b/rlp_auth/comparisons/shorthands.tex @@ -0,0 +1,32 @@ +\shorthandsStandingHypothesis{} +We define shorthands. +The first volley of shorthands represent +data associated with and authority tuple. +\[ + \left\{ \begin{array}{lcl} + \locChainIdHi & \define & \rlpAuthMacroChainIdHi _{i + \roffCompMacroRow} \\ + \locChainIdLo & \define & \rlpAuthMacroChainIdLo _{i + \roffCompMacroRow} \\ + \locNonce & \define & \rlpAuthMacroNonce _{i + \roffCompMacroRow} \\ + \locAddressHi & \define & \rlpAuthMacroAddressHi _{i + \roffCompMacroRow} \\ + \locAddressLo & \define & \rlpAuthMacroAddressLo _{i + \roffCompMacroRow} \\ + \locSignatureY & \define & \rlpAuthMacroSignatureYparity _{i + \roffCompMacroRow} \\ + \locSignatureRhi & \define & \rlpAuthMacroSignatureRhi _{i + \roffCompMacroRow} \\ + \locSignatureRlo & \define & \rlpAuthMacroSignatureRlo _{i + \roffCompMacroRow} \\ + \locSignatureShi & \define & \rlpAuthMacroSignatureShi _{i + \roffCompMacroRow} \\ + \locSignatureSlo & \define & \rlpAuthMacroSignatureSlo _{i + \roffCompMacroRow} \\ + % \loc & \define & \\ + \end{array} \right. +\] +The following shorthands +\[ + \left\{ \begin{array}{lcl} + \locNetworkChainIdHi & \define & \rlpAuthExternNetworkChainIdHi _{i + \roffCompExternRow} \\ + \locNetworkChainIdLo & \define & \rlpAuthExternNetworkChainIdLo _{i + \roffCompExternRow} \\ + \locAuthorityAddressHi & \define & \rlpAuthExternAuthorityAddressHi _{i + \roffCompExternRow} \\ + \locAuthorityAddressLo & \define & \rlpAuthExternAuthorityAddressLo _{i + \roffCompExternRow} \\ + \locAuthorityNonce & \define & \rlpAuthExternAuthorityNonce _{i + \roffCompExternRow} \\ + \locFromAddressHi & \define & \rlpAuthExternTransactionFromAddressHi _{i + \roffCompExternRow} \\ + \locFromAddressLo & \define & \rlpAuthExternTransactionFromAddressLo _{i + \roffCompExternRow} \\ + \end{array} \right. +\] + diff --git a/rlp_auth/comparisons/validity/__01__chain_id_iszero.tex b/rlp_auth/comparisons/validity/__01__chain_id_iszero.tex new file mode 100644 index 00000000..e9238b38 --- /dev/null +++ b/rlp_auth/comparisons/validity/__01__chain_id_iszero.tex @@ -0,0 +1,17 @@ +\chainIdIsZeroStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToIszero { + anchorRow = i , + relOffset = \roffCompValidityChainIdIszero , + argOneHi = \locChainIdHi , + argOneLo = \locChainIdLo , + } + \vspace{2mm} + \\ + \locChainIdIszero \define \rlpAuthComputationRes _{i + \roffCompValidityChainIdIszero} + \end{array} \right. +\] +\saNote{} +Thus \( \locChainIdIszero = \true ~\iff~ \locChainId = 0 \). diff --git a/rlp_auth/comparisons/validity/__02__chain_id_vs_network_chain_id.tex b/rlp_auth/comparisons/validity/__02__chain_id_vs_network_chain_id.tex new file mode 100644 index 00000000..0980685a --- /dev/null +++ b/rlp_auth/comparisons/validity/__02__chain_id_vs_network_chain_id.tex @@ -0,0 +1,20 @@ +\chainIdIsNetworkChainIdStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToEq { + anchorRow = i , + relOffset = \roffCompValidityChainIdVsNetworkChainId , + argOneHi = \locChainIdHi , + argOneLo = \locChainIdLo , + argTwoHi = \locNetworkChainIdHi , + argTwoLo = \locNetworkChainIdLo , + } + \vspace{2mm} + \\ + \locChainIdIsNetworkChainId \define \rlpAuthComputationRes _{i + \roffCompValidityChainIdVsNetworkChainId} + \end{array} \right. +\] +\saNote{} +Thus \( \locChainIdIsNetworkChainId = \true ~\iff~ \locChainId = \beta \) +where $\beta$ stands for the \textbf{network chain id}. diff --git a/rlp_auth/comparisons/validity/__03__nonce_EIP_2681_bound.tex b/rlp_auth/comparisons/validity/__03__nonce_EIP_2681_bound.tex new file mode 100644 index 00000000..354b92d9 --- /dev/null +++ b/rlp_auth/comparisons/validity/__03__nonce_EIP_2681_bound.tex @@ -0,0 +1,19 @@ +\nonceEipCheckStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \roffCompValidityNonceEipBound , + argOneHi = 0 , + argOneLo = \locNonce , + argTwoHi = 0 , + argTwoLo = \maxNonce , + } + \vspace{2mm} + \\ + \locNonceSatisfiesEipBound \define \rlpAuthComputationRes _{i + \roffCompValidityNonceEipBound} + \end{array} \right. +\] +\saNote{} +Thus \( \locNonceSatisfiesEipBound = \true ~\iff~ \locNonce < \maxNonce = \maxNonceValue \). diff --git a/rlp_auth/comparisons/validity/__04__signature_s_non_malleability_bound.tex b/rlp_auth/comparisons/validity/__04__signature_s_non_malleability_bound.tex new file mode 100644 index 00000000..51056070 --- /dev/null +++ b/rlp_auth/comparisons/validity/__04__signature_s_non_malleability_bound.tex @@ -0,0 +1,19 @@ +\stringentSignatureSCheckStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \roffCompValiditySignatureSnonMalleabilityBound , + argOneHi = \locSignatureShi , + argOneLo = \locSignatureSlo , + argTwoHi = \locSecpPrimeOverTwoHi , + argTwoLo = \locSecpPrimeOverTwoLo , + } + \vspace{2mm} + \\ + \locSignatureSisNonMalleable \define \rlpAuthComputationRes _{i + \roffCompValiditySignatureSnonMalleabilityBound} + \end{array} \right. +\] +\saNote{} +Thus $\locSignatureSisNonMalleable = \true ~\iff~ \locSignatureS < \locSecpPrimeOverTwo$. diff --git a/rlp_auth/comparisons/validity/__05__nonce_vs_account_nonce.tex b/rlp_auth/comparisons/validity/__05__nonce_vs_account_nonce.tex new file mode 100644 index 00000000..bb012028 --- /dev/null +++ b/rlp_auth/comparisons/validity/__05__nonce_vs_account_nonce.tex @@ -0,0 +1,36 @@ +\nonceAgreementStandingHypothesis{} + +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToEq { + anchorRow = i , + relOffset = \roffCompValidityNonceVsAccountNonce , + argOneHi = 0 , + argOneLo = \locNonce , + argTwoHi = 0 , + argTwoLo = \locAuthorityNonce + \locAuthorityIsSender , + } + \vspace{2mm} + \\ + \locNonceEqualsAuthorityNonce \define \rlpAuthComputationRes _{i + \roffCompValidityNonceVsAccountNonce} + \end{array} \right. +\] +\saNote{}\label{rlp auth: comparisons: validity: nonce vs account nonce: when authority is sender} +Thus we have +\begin{enumerate} + \item \If $\locAuthorityIsSender = \false$ \Then \[ \locNonceEqualsAuthorityNonce = \true ~\iff~ \locNonce = \locAuthorityNonce \] + \item \If $\locAuthorityIsSender = \true$ \Then \[ \locNonceEqualsAuthorityNonce = \true ~\iff~ \locNonce = \locAuthorityNonce + 1 \] +\end{enumerate} +We provide some background for this particular constraint. +We first point out that our processing of authority lists in the \hubMod{} module happens \textbf{before} the transaction induced +incrementation of the sender nonce. +We next recall that, as per \cite{EIP-7702}, +the processing the authority list should happen \textbf{after} the transaction induced sender nonce update. +This poses a difficulty if the authority-list transaction includes authority tuples signed by the transaction's sender. +For such a tuple to be valid it is necessary that the (tuple's) nonce be greater by one +than the nonce in the sender's account at the time of processing of said tuple \textbf{in the \hubMod{} module}. +We note furthermore that the sender's nonce continuously updates in the \hubMod{} with every valid +authority tuple (for which the sender is the \authority{}). +Therefore the sender's nonce will only every lag behind by $1$ in the processing of valid authority tuples +(for which the sender is the \authority{}). diff --git a/rlp_auth/comparisons/validity/__06__authority_vs_sender.tex b/rlp_auth/comparisons/validity/__06__authority_vs_sender.tex new file mode 100644 index 00000000..280230a9 --- /dev/null +++ b/rlp_auth/comparisons/validity/__06__authority_vs_sender.tex @@ -0,0 +1,20 @@ +\authorityIsSenderStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToEq { + anchorRow = i , + relOffset = \roffCompValidityAuthorityVsSender , + argOneHi = \locAuthorityAddressHi , + argOneLo = \locAuthorityAddressLo , + argTwoHi = \locFromAddressHi , + argTwoLo = \locFromAddressLo , + } + \vspace{2mm} + \\ + \locAuthorityIsSender \define \rlpAuthComputationRes _{i + \roffCompValidityAuthorityVsSender} + \end{array} \right. +\] +\saNote{} +Thus \( \locAuthorityIsSender = \true ~\iff~ \locAuthorityAddress = \locFromAddress \). + diff --git a/rlp_auth/comparisons/validity/__07__address_iszero.tex b/rlp_auth/comparisons/validity/__07__address_iszero.tex new file mode 100644 index 00000000..d6f84596 --- /dev/null +++ b/rlp_auth/comparisons/validity/__07__address_iszero.tex @@ -0,0 +1,17 @@ +\addressIsZeroStandingHypothesis{} +We impose that +\[ + \left\{ \begin{array}{lcl} + \wcpCallToIszero { + anchorRow = i , + relOffset = \roffCompValidityAddressIszero , + argOneHi = \locAddressHi , + argOneLo = \locAddressLo , + } + \vspace{2mm} + \\ + \locAddressIsZero \define \rlpAuthComputationRes _{i + \roffCompValidityAddressIszero} + \end{array} \right. +\] +\saNote{} +Thus \( \locAddressIsZero = \true ~\iff~ \locAddress = \texttt{0x\,00\,\dots\,00} \in \mathbb{B}_{\addressSize} \). diff --git a/rlp_auth/comparisons/validity/_inputs.tex b/rlp_auth/comparisons/validity/_inputs.tex new file mode 100644 index 00000000..89f4d450 --- /dev/null +++ b/rlp_auth/comparisons/validity/_inputs.tex @@ -0,0 +1,12 @@ +\subsubsection{Introduction \lispTodo{}} \label{rlp auth: comparisons: validity: intro} \input{comparisons/validity/intro} +\subsubsection{\locChainId{} vs zero \lispTodo{}} \label{rlp auth: comparisons: validity: chain id iszero} \input{comparisons/validity/__01__chain_id_iszero} +\subsubsection{\locChainId{} vs the network chain id $\beta$ \lispTodo{}} \label{rlp auth: comparisons: validity: chain id vs network chain id} \input{comparisons/validity/__02__chain_id_vs_network_chain_id} +\subsubsection{\locChainIdIsZeroOrBeta{} definition \lispTodo{}} \label{rlp auth: comparisons: validity: defining chain id is 0 or beta} \input{comparisons/validity/chain_id_is_0_or_beta} +\subsubsection{\locNonce{} vs \maxNonce{} \lispTodo{}} \label{rlp auth: comparisons: validity: nonce EIP 2681 bound} \input{comparisons/validity/__03__nonce_EIP_2681_bound} +\subsubsection{\locSignatureS{} non-malleability bound \lispTodo{}} \label{rlp auth: comparisons: validity: signature s non malleability} \input{comparisons/validity/__04__signature_s_non_malleability_bound} +\subsubsection{\locCallEcrecoverExpression{} definition \lispTodo{}} \label{rlp auth: comparisons: validity: defining call ecrecover expression} \input{comparisons/validity/call_ecrecover_bit} +\subsubsection{Authority recovery success \lispTodo{}} \label{rlp auth: comparisons: validity: authority recovery success} \input{comparisons/validity/tests_requiring_successful_recovery} +\subsubsection{\locNonce{} vs \locAuthorityNonce{} \lispTodo{}} \label{rlp auth: comparisons: validity: nonce vs account nonce} \input{comparisons/validity/__05__nonce_vs_account_nonce} +\subsubsection{\locAuthorityAddress{} vs \locSenderAddress{} \lispTodo{}} \label{rlp auth: comparisons: validity: authority vs sender address} \input{comparisons/validity/__06__authority_vs_sender} +\subsubsection{\locAddress{} vs zero address \lispTodo{}} \label{rlp auth: comparisons: validity: address vs zero address} \input{comparisons/validity/__07__address_iszero} +\subsubsection{\locAuthorityTupleIsValidExpression{} definition \lispTodo{}} \label{rlp auth: comparisons: validity: authority tuple is valid} \input{comparisons/validity/tuple_is_valid} diff --git a/rlp_auth/comparisons/validity/call_ecrecover_bit.tex b/rlp_auth/comparisons/validity/call_ecrecover_bit.tex new file mode 100644 index 00000000..81f07635 --- /dev/null +++ b/rlp_auth/comparisons/validity/call_ecrecover_bit.tex @@ -0,0 +1,20 @@ +We now define the \locCallEcrecoverExpression{} shorthand: +\[ + \locCallEcrecoverExpression \define + \left[ \begin{array}{cl} + \cdot & \locChainIdIsZeroOrBeta \\ + \cdot & \locNonceSatisfiesEipBound \\ + \cdot & \locSignatureSisNonMalleable \\ + \end{array} \right] +\] +\saNote{} +Thus by definition +\[ + \locCallEcrecoverExpression = \true + \quad \iff \quad + \left\{ \begin{array}{l} + \locChainIdIsZeroOrBeta = \true \\ + \quad \wedge ~ \locNonceSatisfiesEipBound = \true \\ + \quad \quad \wedge ~ \locSignatureSisNonMalleable = \true \\ + \end{array} \right. +\] diff --git a/rlp_auth/comparisons/validity/chain_id_is_0_or_beta.tex b/rlp_auth/comparisons/validity/chain_id_is_0_or_beta.tex new file mode 100644 index 00000000..642a6af5 --- /dev/null +++ b/rlp_auth/comparisons/validity/chain_id_is_0_or_beta.tex @@ -0,0 +1,18 @@ +We now define the \locChainIdIsZeroOrBeta{} shorthand +\[ + \locChainIdIsZeroOrBeta \define + \left[ \begin{array}{cl} + + & \locChainIdIszero \\ + + & \locChainIdIsNetworkChainId \\ + - & \locChainIdIszero \cdot \locChainIdIsNetworkChainId \\ + \end{array} \right] +\] +\saNote{} +Thus by definition +\[ + \locChainIdIsZeroOrBeta = \true \quad \iff \quad + \left\{ \begin{array}{l} + \locChainIdIszero = \true \\ + \quad \vee ~ \locChainIdIsNetworkChainId = \true \\ + \end{array} \right. +\] diff --git a/rlp_auth/comparisons/validity/intro.tex b/rlp_auth/comparisons/validity/intro.tex new file mode 100644 index 00000000..4c35a621 --- /dev/null +++ b/rlp_auth/comparisons/validity/intro.tex @@ -0,0 +1,3 @@ +The present section performs the checks that determine the validity of an authority list tuple. +These checks aren't required to pass: if they don't the authority tuple is invalid and has no +effect on the authority account (if the authority address is extractable in the first place). diff --git a/rlp_auth/comparisons/validity/tests_requiring_successful_recovery.tex b/rlp_auth/comparisons/validity/tests_requiring_successful_recovery.tex new file mode 100644 index 00000000..88361771 --- /dev/null +++ b/rlp_auth/comparisons/validity/tests_requiring_successful_recovery.tex @@ -0,0 +1,7 @@ +The following tests are only meaningful if $\rlpAuthExternAuthorityRecoverySuccess _{i + \roffCompMacroRow} = \true$. +Indeed, the \textbf{authority account parameters}, +specifically the \locAuthorityAddress{} and the \locAuthorityNonce{} parameters +are only meaningful in case of \macroEcrecover{} success. +However, the \rlpAuthMod{} module carries these tests out regardless of recovery success. +There is no harm in setting \locAuthorityAddress{} and \locAuthorityNonce{} to zero in that case. +The resulting ``result bits'' are similarly meaningless and will not be used in what follows. diff --git a/rlp_auth/comparisons/validity/tuple_is_valid.tex b/rlp_auth/comparisons/validity/tuple_is_valid.tex new file mode 100644 index 00000000..be386771 --- /dev/null +++ b/rlp_auth/comparisons/validity/tuple_is_valid.tex @@ -0,0 +1,10 @@ +We define the following shorthand +\[ + \locAuthorityTupleIsValidExpression + \define + \left[ \begin{array}{cl} + \cdot & \rlpAuthExternAuthorityEcrecoverAttempt _{i + \roffCompMacroRow} \\ + \cdot & \rlpAuthExternAuthorityRecoverySuccess _{i + \roffCompMacroRow} \\ + \cdot & \locNonceEqualsAuthorityNonce \\ + \end{array} \right] +\] diff --git a/rlp_auth/generalities/_inputs.tex b/rlp_auth/generalities/_inputs.tex new file mode 100644 index 00000000..f3d999cf --- /dev/null +++ b/rlp_auth/generalities/_inputs.tex @@ -0,0 +1,16 @@ +\subsection{Binarities \lispTodo{}} \label{rlp auth: generalities: binarities} \input{generalities/binarities} +\subsection{Constancies \lispTodo{}} \label{rlp auth: generalities: constancies} \input{generalities/constancies} +\subsection{\iomf{} constraints \lispTodo{}} \label{rlp auth: generalities: iomf} \input{generalities/iomf} +\subsection{\userTransactionNumber{} constraints \lispTodo{}} \label{rlp auth: generalities: user transaction number} \input{generalities/user_transaction_number} +\subsection{\rlpAuthMacroAuthorityTupleIndex{} constraints \lispTodo{}} \label{rlp auth: generalities: authority tuple index} \input{generalities/tuple_index} +\subsection{\transactionTypeWithAuthorityLists{} and \transactionTypeWithAuthorityLists{} constraints \lispTodo{}} \label{rlp auth: generalities: transactions with or sans authority list} \input{generalities/with_vs_sans_authority_list} +\subsection{Perspective constraints \lispTodo{}} \label{rlp auth: generalities: perspectives} \input{generalities/perspectives} +\subsection{\ct{} and \maxCt{} constraints \lispTodo{}} \label{rlp auth: generalities: ct and ct_max} \input{generalities/ct_and_ct_max} +\subsection{\rlpAuthUtilsColumnSizeCountdown{} constraints \lispTodo{}} \label{rlp auth: generalities: byte size countdown constraints} \input{generalities/byte_size_countdown} +\subsection{\authorityIsSenderAcc{} constraints \lispTodo{}} \label{rlp auth: generalities: sender is authority acc} \input{generalities/authority_is_sender_acc} +\subsection{\authorityIsSenderTot{} constraints \lispTodo{}} \label{rlp auth: generalities: sender is authority tot} \input{generalities/authority_is_sender_tot} +\subsection{Authority \macroEcrecover{} and validity related bits \lispTodo{}} \label{rlp auth: generalities: authority validity and recovery bits} \input{generalities/recovery_bits} +\subsection{Finalization constraints \lispTodo{}} \label{rlp auth: generalities: finalization} \input{generalities/finalization} + + + diff --git a/rlp_auth/generalities/authority_is_sender_acc.tex b/rlp_auth/generalities/authority_is_sender_acc.tex new file mode 100644 index 00000000..5e31f5de --- /dev/null +++ b/rlp_auth/generalities/authority_is_sender_acc.tex @@ -0,0 +1,34 @@ +We constrain the \authorityIsSenderAcc{} column. +We impose +\begin{enumerate} + \item + \If $\iomf _{i} = 0$ + \Then $\authorityIsSenderAcc _{i} = 0$ + \item + \If $\userTransactionNumber _{i} \neq \userTransactionNumber _{i - 1}$ + \Then $\authorityIsSenderAcc _{i} = 0$ + \item + \If $\userTransactionNumber _{i} \neq 1 + \userTransactionNumber _{i - 1}$ + \[ + \authorityIsSenderAcc _{i} = \authorityIsSenderAcc _{i - 1} + + + \left[ \begin{array}{cl} + \cdot & \macro _{i + \roffCompMacroRow} \\ + \cdot & \extern _{i + \roffCompExternRow} \\ + \cdot & \rlpAuthExternAuthorityTupleIsValid _{i + \roffCompExternRow} \\ + \cdot & \locAuthorityIsSender \\ + \end{array} \right] + \] +\end{enumerate} +\saNote{} +We refer the reader to +section~(\ref{rlp auth: comparisons: shorthands}) +for the definition of \locAuthorityIsSender{}. +We have pegged the above ``increment constraint'' to +$\macro _{i + \roffCompMacroRow} \equiv \true$ +in order to be able to use said shorthand. + +\saNote{} +We don't strictly require the inclusion of the +$\macro _{i + \roffCompMacroRow}$ in the increment. +We include it here for clarity. diff --git a/rlp_auth/generalities/authority_is_sender_tot.tex b/rlp_auth/generalities/authority_is_sender_tot.tex new file mode 100644 index 00000000..70023340 --- /dev/null +++ b/rlp_auth/generalities/authority_is_sender_tot.tex @@ -0,0 +1,27 @@ +We constrain the \authorityIsSenderTot{} column. +We impose +\begin{enumerate} + \item + \If $\iomf _{i} = 0$ + \Then $\authorityIsSenderTot _{i} = 0$ + (\sanityCheck) + \item + \If $\userTransactionNumber _{i} \neq 1 + \userTransactionNumber _{i - 1}$ + \Then + \[ \authorityIsSenderTot _{i} = \authorityIsSenderTot _{i - 1} \] + \item + \If $\userTransactionNumber _{i} \neq \userTransactionNumber _{i - 1}$ + \Then + \[ \authorityIsSenderTot _{i - 1} = \authorityIsSenderAcc _{i - 1} \] + \item + $\authorityIsSenderTot _{N} = \authorityIsSenderAcc _{N}$ +\end{enumerate} +\saNote{} +We refer the reader to +section~(\ref{rlp auth: comparisons: shorthands}) +for the definition of \locAuthorityIsSender{}. + +\saNote{} +We don't strictly require the inclusion of the +$\macro _{i + \roffCompMacroRow}$ in the increment. +We include it here for clarity. diff --git a/rlp_auth/generalities/binarities.tex b/rlp_auth/generalities/binarities.tex new file mode 100644 index 00000000..a7ac0b22 --- /dev/null +++ b/rlp_auth/generalities/binarities.tex @@ -0,0 +1,26 @@ +We require the following columns to be binary: +\begin{multicols}{3} + \begin{enumerate} + \item \iomf{} + \item \transactionTypeWithAuthorityLists{} + \item \transactionTypeSansAuthorityLists{} + \item[\vspace{\fill}] + % \item[\vspace{\fill}] + \item \computation{} + \item \macro{} + \item \extern{} + \item \utils{} + % \item[\vspace{\fill}] + % \item[\vspace{\fill}] + % \item \rlpAuthUtilsColumnIsMagic{} + % \item \rlpAuthUtilsColumnIsPrefix{} + % \item \rlpAuthUtilsColumnIsChainId{} + % \item \rlpAuthUtilsColumnIsAddress{} + % \item \rlpAuthUtilsColumnIsNonce{} + \item \rlpAuthUtilsColumnLimbBit{} + \item \rlpAuthExternAuthorityEcrecoverAttempt{} + \item \rlpAuthExternAuthorityRecoverySuccess{} + \item \rlpAuthExternAuthorityTupleIsValid{} + % \item[\vspace{\fill}] + \end{enumerate} +\end{multicols} diff --git a/rlp_auth/generalities/byte_size_countdown.tex b/rlp_auth/generalities/byte_size_countdown.tex new file mode 100644 index 00000000..7fa4a800 --- /dev/null +++ b/rlp_auth/generalities/byte_size_countdown.tex @@ -0,0 +1,28 @@ +The above describes the behaviour of the \rlpAuthUtilsColumnSizeCountdown{} column. +This column, which belongs to the \utils{} perspetive is initialized, on the first +row of any \utils{}-row block, to some value. +Then, with every completed limb ($\rlpAuthUtilsColumnLimbBit \equiv \true$) +it decrements by \rlpAuthUtilsColumnLimbSize{}. +At the end of any \utils{}-row block it must reach the value of zero. +\begin{enumerate} + \item \If $\utils _{i - 1} = \true$ \et $\utils _{i} = \true$ \Then we impose + \[ + \rlpAuthUtilsColumnSizeCountdown _{i} + = + \rlpAuthUtilsColumnSizeCountdown _{i - 1} + - + \left[ \begin{array}{cl} + \cdot & \rlpAuthUtilsColumnLimbBit _{i} \\ + \cdot & \rlpAuthUtilsColumnLimbSize _{i} \\ + \end{array} \right] + \] + \item \If $\utils _{i} = \true$ \et $\utils _{i + 1} = \false$ \Then $\rlpAuthUtilsColumnSizeCountdown _{i} = 0$ + \item \If $\utils _{N} = \true$ \Then we impose $\rlpAuthUtilsColumnSizeCountdown _{N} = 0$ +\end{enumerate} +\saNote{} +The first value it takes on any \utils{}-row block is the length of +\[ + \rlp\Big( \locChainId \Big) \cdot + \rlp\Big( \locAddress \Big) \cdot + \rlp\Big( \locNonce \Big) +\] diff --git a/rlp_auth/generalities/constancies.tex b/rlp_auth/generalities/constancies.tex new file mode 100644 index 00000000..6b35b920 --- /dev/null +++ b/rlp_auth/generalities/constancies.tex @@ -0,0 +1,21 @@ +We define the usual constancy conditions. +A column \col{X} is +\textbf{transaction-constant} if it satisfies +\[ + \If \userTransactionNumber _{i} \neq 1 + \userTransactionNumber _{i - 1} ~ + \Then \col{X} _{i} = \col{X} _{i - 1} +\] +\textbf{authority-list-item-constant} if it satisfies +\[ + \If + \begin{cases} + \userTransactionNumber _{i} \neq 1 + \userTransactionNumber _{i - 1} \\ + \authorityTupleIndex _{i} = \authorityTupleIndex _{i - 1} \\ + \end{cases} + \Then \col{X} _{i} = \col{X} _{i - 1} +\] +\textbf{counter-constant} if it satisfies +\[ + \If \ct _{i} \neq 0 ~ + \Then \col{X} _{i} = \col{X} _{i - 1} +\] diff --git a/rlp_auth/generalities/ct_and_ct_max.tex b/rlp_auth/generalities/ct_and_ct_max.tex new file mode 100644 index 00000000..85e964ab --- /dev/null +++ b/rlp_auth/generalities/ct_and_ct_max.tex @@ -0,0 +1,41 @@ +We impose standard constraints for the \ct{} and \maxCt{} columns: +\begin{enumerate} + \item $\maxCt$ is \textbf{counter-constant} (\sanityCheck) + \item $\maxCt _{i} = \locCtMaxSum _{i}$ + \item \If $\transactionTypeWithAuthorityLists _{i} = 0$ \Then + \[ + \left\{ \begin{array}{lclr} + \ct _{i} & = & 0 \\ + \maxCt _{i} & = & 0 & (\sanityCheck) \\ + \end{array} \right. + \] + \item \If $\ct _{i} \neq \maxCt _{i}$ \Then $\ct _{i + 1} = 1 + \ct _{i}$ + \item \If $\ct _{i} = \maxCt _{i}$ \Then $\ct _{i + 1} = 0$ +\end{enumerate} +Where we introduce the following shorthand +\[ + \begin{array}{lcl} + \locCtMaxSum _{i} & \define & + \left[ \begin{array}{clcl} + + & \rlpAuthCtmaxComputation & \cdot & \computation _{i} \\ + + & \rlpAuthCtmaxMacro & \cdot & \macro _{i} \\ + + & \rlpAuthCtmaxExtern & \cdot & \extern _{i} \\ + + & \rlpAuthCtmaxUtils & \cdot & \utils _{i} \\ + \end{array} \right] + \cdot \transactionTypeWithAuthorityLists _{i} + \vspace{2mm} + \\ + && + \rlpAuthCtmaxNoop \cdot \computation _{i} \cdot \transactionTypeSansAuthorityLists _{i} \\ + \end{array} +\] +and +\[ + \left\{ \begin{array}{lcl} + \rlpAuthCtmaxComputation & \define & \rlpAuthCtmaxComputationValue \\ + \rlpAuthCtmaxMacro & \define & \rlpAuthCtmaxMacroValue \\ + \rlpAuthCtmaxExtern & \define & \rlpAuthCtmaxExternValue \\ + \rlpAuthCtmaxUtils & \define & \rlpAuthCtmaxUtilsValue \\ + \rlpAuthCtmaxNoop & \define & \rlpAuthCtmaxNoopValue \\ + \end{array} \right. +\] + diff --git a/rlp_auth/generalities/finalization.tex b/rlp_auth/generalities/finalization.tex new file mode 100644 index 00000000..9e994967 --- /dev/null +++ b/rlp_auth/generalities/finalization.tex @@ -0,0 +1,13 @@ +We impose that +\begin{enumerate} + \item \If $\transactionTypeSansAuthorityLists _{N} = \true$ \Then no further constraints required + \[ + \computation _{N} = \true \quad (\sanityCheck) + \] + \item \If $\transactionTypeWithAuthorityLists _{N} = \true$ \Then + \begin{enumerate} + \item $\extern _{N} + \utils _{N} = \true$ + \item \If $\extern _{N} = \true$ \Then $\rlpAuthExternAuthorityEcrecoverAttempt _{N} = \false$ + \item \If $\utils _{N} = \true$ \Then $\ct _{N} = \maxCt _{N}$ + \end{enumerate} +\end{enumerate} diff --git a/rlp_auth/generalities/iomf.tex b/rlp_auth/generalities/iomf.tex new file mode 100644 index 00000000..d728d426 --- /dev/null +++ b/rlp_auth/generalities/iomf.tex @@ -0,0 +1,6 @@ +We impose that +\begin{enumerate} + \item \iomf{} is binary (\sanityCheck) + \item $\iomf _{0} = \false$ + \item \If $\iomf _{i} = \true$ \Then $\iomf _{i + 1} = \true$ +\end{enumerate} diff --git a/rlp_auth/generalities/perspectives.tex b/rlp_auth/generalities/perspectives.tex new file mode 100644 index 00000000..5bd236e3 --- /dev/null +++ b/rlp_auth/generalities/perspectives.tex @@ -0,0 +1,74 @@ +We impose that +\begin{enumerate} + \item \computation{}, \macro{}, \extern{} and \utils{} are binary (\sanityCheck) + \item \computation{}, \macro{}, \extern{} and \utils{} are counter-constant + \item $\iomf _{i} = \computation _{i} + \macro _{i} + \extern _{i} + \utils _{i}$ + \item \If $\userTransactionNumber _{i + 1} \neq \userTransactionNumber _{i}$ \Then $\computation _{i + 1} = 1$ + \item \If $\authorityTupleIndex _{i + 1} \neq \authorityTupleIndex _{i}$ \Then $\computation _{i + 1} = 1$ + \item + we impose certain transitions + \[ + \left[ \begin{array}{llllllllllll} + + \!\!\!& \computation _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& + \!\!\!& \macro _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& & \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \macro _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& \!\!\!& \!\!\!& + \!\!\!& \extern _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \extern _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& + \!\!\!& \utils _{i + 1} \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \utils _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& + \!\!\!& \utils _{i + 1} \!\!\!& \!\!\! \Big] \\ + \end{array} \right] + = \iomf _{i} + \] + \item + \If $\transactionTypeWithAuthorityLists _{i} = 1$ \et $\ct _{i} = \maxCt _{i}$ \Then + \[ + \left[ \begin{array}{llllllllllll} + + \!\!\!& \computation _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& + \!\!\!& \macro _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& & \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \macro _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& \!\!\!& \!\!\!& + \!\!\!& \extern _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \extern _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& + \!\!\!& \utils _{i + 1} \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \utils _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \\ + \end{array} \right] + = 1 + \] + \item + \If $\transactionTypeWithAuthorityLists _{i} = 1$ \et $\ct _{i} \neq \maxCt _{i}$ \Then + \[ + \left[ \begin{array}{llllllllllll} + + \!\!\!& \computation _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \computation _{i + 1} \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \macro _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& \!\!\!& 0 \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \extern _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& 0 \!\!\!& \!\!\!& \!\!\!& \!\!\! \Big] \vspace{2mm} \\ + + \!\!\!& \utils _{i} \!\!\!& \cdot \!\!& \Big[ \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \!\!\!& \utils _{i + 1} \!\!\!& \!\!\! \Big] \\ + \end{array} \right] + = 1 + \quad (\sanityCheck) + \] + \item + \If $\transactionTypeSansAuthorityLists _{i} = 1$ + \[ + \left[ \begin{array}{llllllllllll} + + & \computation _{i} & \!\!\!\cdot \!\!& \computation _{i + 1} \vspace{2mm} \\ + \end{array} \right] + = 1 + \quad (\sanityCheck) + \] +\end{enumerate} +We make the above more precise in what follows +\begin{enumerate}[resume] + \item \If $\extern _{i} = \true$ \Then $\utils _{i + 1} = \rlpAuthExternAuthorityEcrecoverAttempt _{i}$ +\end{enumerate} +\saNote{} +The above imposes binary exclusivity on +\computation{}, \macro{} and \utils{}. + +\saNote{} +The counter-constancy of +\computation{}, \macro{}, \extern{} and \utils{} +may be implemented as the counter-constancy of the following weighted sum +\[ + \locWeightedPerspectiveSum _{i} + \define + \left[ \begin{array}{lcl} + 2 ^ {0} & \cdot & \computation _{i} \\ + 2 ^ {1} & \cdot & \macro _{i} \\ + 2 ^ {2} & \cdot & \extern _{i} \\ + 2 ^ {3} & \cdot & \utils _{i} \\ + \end{array} \right] +\] +be \textbf{counter-constant}. diff --git a/rlp_auth/generalities/recovery_bits.tex b/rlp_auth/generalities/recovery_bits.tex new file mode 100644 index 00000000..a8812152 --- /dev/null +++ b/rlp_auth/generalities/recovery_bits.tex @@ -0,0 +1,33 @@ +We impose the following general constraints: +\begin{enumerate} + \item + we impose binarity constraints the following columns + \begin{enumerate} + \item \rlpAuthExternAuthorityEcrecoverAttempt{} (\sanityCheck) + \item \rlpAuthExternAuthorityRecoverySuccess{} (\sanityCheck) + \item \rlpAuthExternAuthorityTupleIsValid{} (\sanityCheck) + \end{enumerate} + \item + \If $\extern _{i} = \true$ + \Then we impose + \begin{enumerate} + \item + \If $\rlpAuthExternAuthorityEcrecoverAttempt _{i} = \false$ + \Then + \[ + \left\{ \begin{array}{lcl} + \rlpAuthExternAuthorityRecoverySuccess _{i} & = & \false \\ + \rlpAuthExternAuthorityTupleIsValid _{i} & = & \false \\ + \end{array} \right. + \] + \item + \If $\rlpAuthExternAuthorityRecoverySuccess _{i} = \false$ + \Then + \[ + \rlpAuthExternAuthorityTupleIsValid _{i} = \false + \] + \end{enumerate} +\end{enumerate} +\saNote{} +Explicit values for these columns are set in +section~(\ref{rlp auth: comparisons: justifying extern values}). diff --git a/rlp_auth/generalities/tuple_index.tex b/rlp_auth/generalities/tuple_index.tex new file mode 100644 index 00000000..13c7135c --- /dev/null +++ b/rlp_auth/generalities/tuple_index.tex @@ -0,0 +1,24 @@ +We impose that +\begin{enumerate} + \item + \If $\iomf _{i} = 0$ + \Then $\authorityTupleIndex _{i} = 0$ (\trash) + \item + $\authorityTupleIndex _{i + 1} \in \{ \authorityTupleIndex _{i}, 1 + \authorityTupleIndex _{i}, 0 \}$ + \item + \If $\userTransactionNumber _{i + 1} \neq \userTransactionNumber _{i}$ + \Then $\authorityTupleIndex _{i} = 0$ + \item + \If $\userTransactionNumber _{i + 1} \neq 1 + \userTransactionNumber _{i}$ + \Then $\authorityTupleIndex _{i + 1} = \authorityTupleIndex _{i} + \utils _{i} \cdot \computation _{i + 1}$ + \item + \If $\authorityTupleIndex _{i + 1} \neq \authorityTupleIndex _{i}$ + \Then + \[ + \left\{ \begin{array}{lclr} + \utils _{i} & = & \true \\ + \rlpAuthUtilsColumnIsNonce _{i} & = & \true \\ + \ct _{i} & = & \maxCt _{i} \\ + \end{array} \right. + \] +\end{enumerate} diff --git a/rlp_auth/generalities/user_transaction_number.tex b/rlp_auth/generalities/user_transaction_number.tex new file mode 100644 index 00000000..b8abc52f --- /dev/null +++ b/rlp_auth/generalities/user_transaction_number.tex @@ -0,0 +1,28 @@ +We impose the following constraints +\begin{enumerate} + \item $\userTransactionNumber _{0} = 0$ + \item \If $\userTransactionNumber _{i} = 0$ \et $\iomf _{i} = 0$ + \item \If $\userTransactionNumber _{i} \neq 0$ \et $\iomf _{i} = 1$ + \item $\userTransactionNumber _{i} \in \{ \userTransactionNumber _{i - 1}, 1 + \userTransactionNumber _{i - 1} \}$ \quad (\sanityCheck) +\end{enumerate} +We cannot completely characterize when the \userTransactionNumber{} increments, but we impose the following +\begin{enumerate}[resume] + \item + \If $\transactionTypeSansAuthorityLists _{i} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \userTransactionNumber _{i} & = & 1 + \userTransactionNumber _{i - 1} \\ + \userTransactionNumber _{i + 1} & = & 1 + \userTransactionNumber _{i} \\ + \end{array} \right. + \] + \item + \If $\transactionTypeWithAuthorityLists _{i} = 1$ \et $\userTransactionNumber _{i} \neq \userTransactionNumber _{i + 1}$ + \Then + \[ + \left\{ \begin{array}{lcl} + \utils _{i} & = & \true \\ + \rlpAuthUtilsColumnIsNonce _{i} & = & \true \\ + \ct _{i} & = & \maxCt _{i} \\ + \end{array} \right. + \] +\end{enumerate} diff --git a/rlp_auth/generalities/with_vs_sans_authority_list.tex b/rlp_auth/generalities/with_vs_sans_authority_list.tex new file mode 100644 index 00000000..fb4c873d --- /dev/null +++ b/rlp_auth/generalities/with_vs_sans_authority_list.tex @@ -0,0 +1,21 @@ +We impose that +\begin{enumerate} + \item both \transactionTypeWithAuthorityLists{} and \transactionTypeWithAuthorityLists{} are binary (\sanityCheck) + \item both \transactionTypeWithAuthorityLists{} and \transactionTypeWithAuthorityLists{} are \textbf{transaction-constant} + \item we peg them to \iomf{}: + \[ + \iomf _{i} + = + \left[ \begin{array}{cl} + + & \transactionTypeWithAuthorityLists _{i} \\ + + & \transactionTypeSansAuthorityLists _{i} \\ + \end{array} \right] + \] + \item we impose that +\end{enumerate} +\saNote{} \label{rlp auth: generalities: transactions with or sans authority list: exclusivity} +The above entails that +\transactionTypeWithAuthorityLists{} +\transactionTypeSansAuthorityLists{} +are binary exclusive. + diff --git a/rlp_auth/intro.tex b/rlp_auth/intro.tex new file mode 100644 index 00000000..6f79a0a2 --- /dev/null +++ b/rlp_auth/intro.tex @@ -0,0 +1,93 @@ +The \rlpAuthMod{} module carries out the analysis of individual +\textbf{authorization tuples} of \textbf{set code transactions} +(i.e. $\typeFourTx$ transactions) +as specified in \cite{EIP-7702} +and as required by the \rlpTxnMod{} module. + +The present module parses \textbf{all} \user{}-transactions regardless of their (transaction) type. +Transactions whose underlying type doesn't support \textbf{authorization lists} +($\transactionTypeSansAuthorityLists{} \equiv 1$) +have ``trivial'' processing, +while those that do +($\transactionTypeWithAuthorityLists{} \equiv 1$) +have more involved processing. + +We deal with authorization lists by +dealing with their authorization tuples sequentially, +and the processing of any one authorization tuple +takes place over a block of contiguous, perspectivized rows. +The ``authority tuple data'' is read off of a single \macro{}-row. +Processing involves various \textbf{mandatory} comparisons, which mustn't fail, +as well as other \textbf{validity} checks, which may or may not hold. +The ultimate goal of processing as a whole is to determine +\rlpAuthExternAuthorityTupleIsValid{} +which is the determining factor as to whether or not +an authority tuple leads to a state change in the +\locAuthority{} account. +Whenever $\rlpAuthExternAuthorityTupleIsValid \equiv \true$, the +\hubMod{} module will carry out the relevant account changes. + +The precise sequence of events goes as follows: +\begin{description} + \item[\underline{\underline{Determining \rlpAuthExternAuthorityEcrecoverAttempt{}:}}] + several of the \textbf{validity} checks, taken together, determine the + \rlpAuthExternAuthorityEcrecoverAttempt{} bit. + This bit, as the name suggests, dictates whether an attempt is made + at \macroEcrecover{}'ing the \locAuthorityAddress{}. + It is therfore the main trigger for the lookup of + section~(\ref{rlp auth: lookup: extraction for ecrecover}). + \item[\underline{\underline{Attempting \macroEcrecover{}:}}] + whenever $\rlpAuthExternAuthorityEcrecoverAttempt \equiv \true$ + the module attempts to \macroEcrecover{} the \locAuthorityAddress{}; + this requires computing the following byte string + \[ + \begin{array}{lcl} + \texttt{msg} & \equiv & + \locMagicByte + ~ \cdot ~ + \rlp\Big( \big[ \locChainId, \locAddress, \locNonce \big] \Big) \vspace{2mm} \\ + & \equiv & + \locMagicByte + ~ \cdot ~ + \rlp\Big( + \rlp\big( \locChainId \big) \, \cdot \, + \rlp\big( \locAddress \big) \, \cdot \, + \rlp\big( \locNonce \big) + \Big) + \\ + \end{array} + \] + which is supposedly signed in the authority tuple. + This \rlp{}-ization of those data, + which are available on the \macro{}-row, takes place + along \utils{}-rows. + + The success (or failure) of this attempt is recorded in + \rlpAuthExternAuthorityRecoverySuccess{}. + If address recovery failed, the shorthand \locAuthorityAddress{} carries no meaningful value. + \item[\underline{\underline{Extracting \hubMod{} information:}}] + whenever $\rlpAuthExternAuthorityRecoverySuccess \equiv \true$, the + \locAuthorityAddress{} is meaningful and the present module queries the \hubMod{} + to extract the associated \locAuthorityNonce{}. + At this point the module can check the validity of the authority tuple \locNonce{} + and thus compute \rlpAuthExternAuthorityTupleIsValid{}. + State changes will be enacted in the \hubMod{} module accordingly. + + Special care has to be taken in case the \loc{sender\_address} and \locAuthorityAddress{} + coincide, specifically with respect to comparing the \locNonce{} and \locAuthorityNonce{}, + see note~(\ref{rlp auth: comparisons: validity: nonce vs account nonce: when authority is sender}). + \item[\underline{\underline{Computing the new ``\codeHash{}'':}}] + if $\rlpAuthExternAuthorityTupleIsValid \equiv \true$ then the \locAuthority{}'s + ``code'' and \codeHash{} must be updated as well as its code hash. + This requires computing + \[ + \left\{ \begin{array}{lcl} + \texttt{KECCAK}(\loc{code}) \vspace{2mm} \\ + \loc{code} \define \locAthorizationCodePrefix ~ \cdot ~ \locAddress \\ + + \end{array} \right. + \] + and is the reason for the lookup in + section~(\ref{rlp auth: lookup: extraction for keccak}). +\end{description} + diff --git a/rlp_auth/lookups/_inputs.tex b/rlp_auth/lookups/_inputs.tex new file mode 100644 index 00000000..03c15c8e --- /dev/null +++ b/rlp_auth/lookups/_inputs.tex @@ -0,0 +1,7 @@ +\subsection{Into \wcpMod{} \lispTodo{}} \label{rlp auth: lookup: into wcp} \input{lookups/rlp_auth_into_wcp} +\subsection{Into \rlpUtilsMod{} \lispTodo{}} \label{rlp auth: lookup: into rlp utils} \input{lookups/rlp_auth_into_rlp_utils} +\subsection{Into \userTxnDataMod{} \lispTodo{}} \label{rlp auth: lookup: into txn data} \input{lookups/rlp_auth_into_txn_data} +\subsection{Into \btcMod{} \lispTodo{}} \label{rlp auth: lookup: into block data} \input{lookups/rlp_auth_into_block_data} +\subsection{Into \hubMod{} \lispTodo{}} \label{rlp auth: lookup: into hub} \input{lookups/rlp_auth_into_hub} +\subsection{Data extraction for \macroEcrecover{} \lispTodo{}} \label{rlp auth: lookup: extraction for ecrecover} \input{lookups/extraction_for_ecrecover} +\subsection{Data extraction for \inst{KECCAK} \lispTodo{}} \label{rlp auth: lookup: extraction for keccak} \input{lookups/extraction_for_keccak} diff --git a/rlp_auth/lookups/extraction_for_ecrecover.tex b/rlp_auth/lookups/extraction_for_ecrecover.tex new file mode 100644 index 00000000..d4404f5b --- /dev/null +++ b/rlp_auth/lookups/extraction_for_ecrecover.tex @@ -0,0 +1,3 @@ +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_ecrecover___pre_verticalization.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_ecrecover___verticalized.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_ecrecover___prover_columns.pdf} diff --git a/rlp_auth/lookups/extraction_for_keccak.tex b/rlp_auth/lookups/extraction_for_keccak.tex new file mode 100644 index 00000000..7fc324da --- /dev/null +++ b/rlp_auth/lookups/extraction_for_keccak.tex @@ -0,0 +1,59 @@ +The present section describes how to extract the message to hash defining the ``delegation'' code hash. +Recall that this is defined as the \texttt{KECCAK} hash of +\[ + \underbrace{\locAthorizationCodePrefix}_{\in \mathbb{B} _{3}} ~ \cdot ~ \underbrace{\locAddress}_{\in \mathbb{B} _{\addressSize}} \in \mathbb{B} _{23} +\] +where $\locAthorizationCodePrefix \define \locAthorizationCodePrefixValue$ +and for the purposes of the arithmetization it is broken up into three chunks +\[ + \underbrace{\locAthorizationCodePrefix}_{\in \mathbb{B} _{3}} + ~ \cdot ~ \underbrace{\locAddress\loc{[:4]}}_{\in \mathbb{B} _{4}} + ~ \cdot ~ \underbrace{\locAddress\loc{[4:]}}_{\in \mathbb{B} _{\llarge}} + \in \mathbb{B} _{23} +\] +\begin{description} + \item[\underline{Selector:}] + we use + \[ + \loc{code\_hash\_selector} _{i} + \define + \left[ \begin{array}{cl} + \cdot & \extern _{i} \\ + \cdot & \rlpAuthExternAuthorityTupleIsValid _{i} \\ + \end{array} \right] + \] + \item[\underline{Columns:}] + we use the following expressions + \begin{enumerate} + \item $1$ + \item $\userTransactionNumber _{i}$ + \item $\authorityTupleIndex _{i}$ + \item $\locAthorizationCodePrefix \cdot 256 ^ \numConst{13}$ + \item $\rlpAuthExternTupleAddressHi _{i} \cdot 256 ^ \numConst{12}$ + \item $\rlpAuthExternTupleAddressLo _{i} \cdot 256 ^ \numConst{0}$ + \item $\rlpAuthExternPotentialNewCodeHashHi _{i}$ + \item $\rlpAuthExternPotentialNewCodeHashLo _{i}$ + \end{enumerate} +\end{description} +Where +\[ + \left\{ \begin{array}{l} + \locAthorizationCodePrefixValue \in \mathbb{B} _{3} \\ + \rlpAuthExternTupleAddressHi _{i} \in \mathbb{B} _{4} \\ + \rlpAuthExternTupleAddressLo _{i} \in \mathbb{B} _{\llarge} \\ + \end{array} \right. + \quad\text{and}\quad + \left\{ \begin{array}{lcl} + \numConst{13} & \equiv & \llarge - 3 \vspace{2mm} \\ + \numConst{12} & \equiv & \llarge - 4 \\ + \numConst{0} & \equiv & \llarge - \llarge \\ + \end{array} \right. +\] +\saNote{} +We do not provide byte sizes for the three (left aligned) limbs making up the message to hash +as they are known to be $3$, $4$ and $\llarge$. + +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_keccak___pre_verticalization.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_keccak___verticalized.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/extraction_for_keccak___prover_columns.pdf} + diff --git a/rlp_auth/lookups/rlp_auth_into_block_data.tex b/rlp_auth/lookups/rlp_auth_into_block_data.tex new file mode 100644 index 00000000..eb3981e2 --- /dev/null +++ b/rlp_auth/lookups/rlp_auth_into_block_data.tex @@ -0,0 +1,20 @@ +The purpose of the present lookup is to extract the \textbf{network chain id} $\beta$. +\begin{description} + \item[\underline{Selector:}] + we use + \[ + \col{block\_data\_selector} _{i} \define \extern _{i} + \] + \item[\underline{Column correspondence:}] + \[ + \renewcommand{\arraystretch}{1.5} + \begin{array}{|l|c|l|} + \hline + \text{\rlpAuthMod{}-columns} & & \text{\btcMod{}-columns} \\ \hline\hline + \blockNumber _{i} & \rightsquigarrow & \relBlock _{j} \\ \hline + 1 & \rightsquigarrow & \isChainid _{j} \\ \hline + \rlpAuthExternNetworkChainIdHi _{i} & \rightsquigarrow & \blockDataHi _{j} \\ \hline + \rlpAuthExternNetworkChainIdLo _{i} & \rightsquigarrow & \blockDataLo _{j} \\ \hline + \end{array} + \] +\end{description} diff --git a/rlp_auth/lookups/rlp_auth_into_hub.tex b/rlp_auth/lookups/rlp_auth_into_hub.tex new file mode 100644 index 00000000..d57e1e73 --- /dev/null +++ b/rlp_auth/lookups/rlp_auth_into_hub.tex @@ -0,0 +1,42 @@ +The purpose of the $\rlpAuthMod \hookrightarrow \hubMod$ lookup is to extract the $\rlpAuthExternAuthorityNonce$. +Furthermore, this lookup is the means by which the \hubMod{} learns about authority tuples, whether valid or invalid. +% TODO: @OLIVIER: we need an inverse lookup from HUB to RLP_AUTH to make sure we don't add extra delegations +% TODO: @OLIVIER: we need a new transaction execution phase in the HUB, which we should name TXN_AUTH (like TXN_WARM) to deal with authorization tuples +% TODO: @OLIVIER: we need an indexing mechanism for tuples for which ecrecovery was successful to prevent "double authorizations" or what not (likely impossible but ok) in the HUB +\begin{description} + \item[\underline{Selector:}] + we use + \[ + \col{hub\_selector} _{i} + \define + \extern _{i} \cdot \rlpAuthExternAuthorityRecoverySuccess _{i} + \] + \item[\underline{Source columns:}] --- + \item[\underline{Column correspondence:}] + \[ + \renewcommand{\arraystretch}{1.5} + \begin{array}{|l|c|l|} + \hline + \text{\rlpAuthMod{}-columns} & & \text{\hubMod{}-columns} \\ \hline\hline + 1 & \rightsquigarrow & ``\col{TX\_AUTH}" \\ \hline + 1 & \rightsquigarrow & ``\col{PEEK\_AT\_AUTH}" \\ \hline + \rlpAuthExternAuthorityAddressHi _{i} & \rightsquigarrow & \\ \hline + \rlpAuthExternAuthorityAddressLo _{i} & \rightsquigarrow & \\ \hline + \rlpAuthMacroAddressHi _{i - 1} & \rightsquigarrow & \\ \hline + \rlpAuthMacroAddressLo _{i - 1} & \rightsquigarrow & \\ \hline \hline + \rlpAuthExternAddressIsZeroAddress _{i} & \rightsquigarrow & \\ \hline + \rlpAuthExternAuthorityNonce _{i} & \rightsquigarrow & \\ \hline + \rlpAuthExternSenderIsAuthority _{i} & \rightsquigarrow & \\ \hline + \rlpAuthExternPotentialNewCodeHashHi _{i} & \rightsquigarrow & \\ \hline + \rlpAuthExternPotentialNewCodeHashLo _{i} & \rightsquigarrow & \\ \hline + \end{array} + \] + \item[\underline{Target columns:}] --- + \begin{multicols}{2} + \begin{enumerate} + \item "\col{TX\_AUTH}" % \txAuth % transaction processing phase + \item "\col{PEEK\_AT\_AUTH}" % \peekAuth % perspective + \item various \col{authorization/XXX} columns of the "\col{PEEK\_AT\_AUTH}" perspective + \end{enumerate} + \end{multicols} +\end{description} diff --git a/rlp_auth/lookups/rlp_auth_into_rlp_utils.tex b/rlp_auth/lookups/rlp_auth_into_rlp_utils.tex new file mode 100644 index 00000000..e5e880d8 --- /dev/null +++ b/rlp_auth/lookups/rlp_auth_into_rlp_utils.tex @@ -0,0 +1 @@ +\red{@Olivier: TODO!} diff --git a/rlp_auth/lookups/rlp_auth_into_txn_data.tex b/rlp_auth/lookups/rlp_auth_into_txn_data.tex new file mode 100644 index 00000000..e8c8ad4b --- /dev/null +++ b/rlp_auth/lookups/rlp_auth_into_txn_data.tex @@ -0,0 +1,29 @@ +The purpose of the present lookup is to justify the +\transactionFromAddress{}. +\begin{description} + \item[\underline{Selector:}] + we use + \[ + \col{txn\_data\_selector} _{i} \define + \left[ \begin{array}{cl} + \cdot & \macro _{i} \\ + \cdot & \rlpAuthExternAuthorityRecoverySuccess _{i} \\ + \end{array} \right] + \] + \item[\underline{Column correspondence:}] + \[ + \renewcommand{\arraystretch}{1.5} + \begin{array}{|l|c|l|} + \hline + \text{\rlpAuthMod{}-columns} & & \text{\txnDataMod{}-columns} \\ \hline\hline + \blockNumber _{i} & \rightsquigarrow & \blockNumber _{j} \\ \hline + \userTransactionNumber _{i} & \rightsquigarrow & \userTransactionNumber _{j} \\ \hline + 1 & \rightsquigarrow & \user _{j} \\ \hline + 1 & \rightsquigarrow & \isUserTxnHubView _{j} \\ \hline + 1 & \rightsquigarrow & \txnDataRlpIsAccountDelegationTransaction _{j - \yellowm{1}} \\ \hline + \rlpAuthExternTransactionFromAddressHi _{i} & \rightsquigarrow & \txnDataHubFromHi _{j} \\ \hline + \rlpAuthExternTransactionFromAddressLo _{i} & \rightsquigarrow & \txnDataHubFromLo _{j} \\ \hline + \authorityIsSenderTot _{i} & \rightsquigarrow & \red{@Olivier: TODO !} \\ \hline + \end{array} + \] +\end{description} diff --git a/rlp_auth/lookups/rlp_auth_into_wcp.tex b/rlp_auth/lookups/rlp_auth_into_wcp.tex new file mode 100644 index 00000000..5a384c3c --- /dev/null +++ b/rlp_auth/lookups/rlp_auth_into_wcp.tex @@ -0,0 +1,30 @@ +The purpose of the present lookup is to justify the +computations claimed in the \computation{}-perspective. +\begin{description} + \item[\underline{Selector:}] + we use + \[ + \col{txn\_data\_selector} _{i} \define \computation _{i} + \] + \item[\underline{Column correspondence:}] + \[ + \renewcommand{\arraystretch}{1.5} + \begin{array}{|l|c|l|} + \hline + \text{\rlpAuthMod{}-columns} & & \text{\wcpMod{}-columns} \\ \hline\hline + \rlpAuthComputationInst{} _{i} & \rightsquigarrow & \INST _{j} \\ \hline + \rlpAuthComputationArgOneHi{} _{i} & \rightsquigarrow & \argOneHi _{j} \\ \hline + \rlpAuthComputationArgOneLo{} _{i} & \rightsquigarrow & \argOneLo _{j} \\ \hline + \rlpAuthComputationArgTwoHi{} _{i} & \rightsquigarrow & \argTwoHi _{j} \\ \hline + \rlpAuthComputationArgTwoLo{} _{i} & \rightsquigarrow & \argTwoLo _{j} \\ \hline + \rlpAuthComputationRes{} _{i} & \rightsquigarrow & \res _{j} \\ \hline + \end{array} + \] +\end{description} + + + + + + + diff --git a/rlp_auth/lua/_inputs.tex b/rlp_auth/lua/_inputs.tex new file mode 100644 index 00000000..a3e25143 --- /dev/null +++ b/rlp_auth/lua/_inputs.tex @@ -0,0 +1,4 @@ +\includepdf[fitpaper=true, pages={1}]{lua/computations.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/ecrecover_no_attempt.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/ecrecover_failure.pdf} +\includepdf[fitpaper=true, pages={1}]{lua/ecrecover_success.pdf} diff --git a/rlp_auth/lua/computations.lua.tex b/rlp_auth/lua/computations.lua.tex new file mode 100644 index 00000000..30f1ec20 --- /dev/null +++ b/rlp_auth/lua/computations.lua.tex @@ -0,0 +1,84 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + + + + ██████\ ██\ ██\ ██\ +██ __██\ ██ | ██ | \__| +██ / \__| ██████\ ██████\████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ██████\ ███████\ ███████\ +██ | ██ __██\ ██ _██ _██\ ██ __██\ ██ | ██ |\_██ _| \____██\\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ | ██ / ██ |██ / ██ / ██ |██ / ██ |██ | ██ | ██ | ███████ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██\ ██ | ██ |██ | ██ | ██ |██ | ██ |██ | ██ | ██ |██\ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\██████ |\██████ |██ | ██ | ██ |███████ |\██████ | \████ |\███████ | \████ |██ |\██████ |██ | ██ |███████ | + \______/ \______/ \__| \__| \__|██ ____/ \______/ \____/ \_______| \____/ \__| \______/ \__| \__|\_______/ + ██ | + ██ | + \__| + + +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+-----------------------| +| CMPTN | MACRO | XTERN | UTILS | row | computation | mandatory | result | derived | god given | +|:-----:+:-----:+:-----:+:-----:+:-------+------------------------------------+:---------:+------------------------------------+:------------------------------------------+-----------------------| +| CMPTN | | | | i - 13 | tuple.chain_id ∈ ℕ_256 | ✓ | | | +| CMPTN | | | | i - 12 | tuple.nonce ∈ ℕ_64 | ✓ | | | +| CMPTN | | | | i - 11 | tuple.address ∈ 𝔹_20 | ✓ | (all required to succeed) | | +| CMPTN | | | | i - 10 | tuple.sig_y ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 9 | tuple.sig_r ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 8 | tuple.sig_s ∈ ℕ_8 | ✓ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 7 | tuple.chain_id == 0 | | ✨ chain_id_is_0 | +| CMPTN | | | | i - 6 | tuple.chain_id == network_chain_id | | ✨ chain_id_is_β | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | | | | | | | | ✨ chain_id_is_0_or_β ≡ | +| | | | | | | | | . chain_id_is_0 | +| | | | | | | | | . ∨ chain_id_is_β | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 5 | tuple.nonce < EIP_2681_MAX_NONCE | | ✨ nonce_satisfies_EIP_2681_bound | +| CMPTN | | | | i - 4 | tuple.sig_s < secpk1_256n / 2 | | ✨ sig_s_is_non_malleable | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | | | | | | | | ✨ ecrecover_attempt_expression ≡ | +| | | | | | | | | . chain_id_is_0_or_β | +| | | | | | | | | . ∧ nonce_satisfies_EIP_2681_bound | +| | | | | | | | | . ∧ sig_s_is_non_malleable | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 3 | tuple.nonce == authority.nonce | | ✨ nonce_equals_authority_nonce | MEANINGFUL IFF ecrecover_attempt ≡ | +| CMPTN | | | | i - 2 | tuple.address == from_address | | ✨ authority_is_sender | MEANINGFUL IFF ecrecover_attempt ≡ | +| CMPTN | | | | i - 1 | tuple.address == Address.ZERO | | ✨ address_is_zero | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | MACRO | | | i | ∅ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+-----------------------| +| | | | | | | | | | ✅ tuple.chain_id | +| | | | | | | | | | ✅ tuple.nonce | +| | | | | | | | | | ✅ tuple.address | +| | | | | | | | | | ✅ tuple.sig_y | +| | | | | | | | | | ✅ tuple.sig_r | +| | | | | | | | | | ✅ tuple.sig_s | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+-----------------------| +| | | XTERN | | i + 1 | ∅ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+-----------------------| +| | | | | | | | | | ✅ network_chain_id | +| | | | | | | | | | ✅ from_address | +| | | | | | | | | | | +| | | | | | | | | ✨ ecrecover_attempt | | +| | | | | | | | | . ← ecrecover_attempt_expression | | +| | | | | | | | | | | +| | | | | | | | | | ✅ ecrecover_success | +| | | | | | | | | | | +| | | | | | | | | ecrecover_success triggers HUB lookup | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+-----------------------| +| ??? | | | ??? | i + 2 | +|-------+-------+-------+-------+--------| + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/ecrecover_failure.lua.tex b/rlp_auth/lua/ecrecover_failure.lua.tex new file mode 100644 index 00000000..a89d9bd6 --- /dev/null +++ b/rlp_auth/lua/ecrecover_failure.lua.tex @@ -0,0 +1,124 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + + ██████\ ██\ ██\ ██\ +██ __██\ ██ | ██ | \__| +██ / \__| ██████\ ██████\████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ██████\ ███████\ ███████\ +██ | ██ __██\ ██ _██ _██\ ██ __██\ ██ | ██ |\_██ _| \____██\\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ | ██ / ██ |██ / ██ / ██ |██ / ██ |██ | ██ | ██ | ███████ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██\ ██ | ██ |██ | ██ | ██ |██ | ██ |██ | ██ | ██ |██\ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\██████ |\██████ |██ | ██ | ██ |███████ |\██████ | \████ |\███████ | \████ |██ |\██████ |██ | ██ |███████ | + \______/ \______/ \__| \__| \__|██ ____/ \______/ \____/ \_______| \____/ \__| \______/ \__| \__|\_______/ + ██ | + ██ | + \__| + + + _____ ____ ____ _____ ____ _____ _______ ____ + | ____/ ___| _ \| ____/ ___/ _ \ \ / / ____| _ \ + | _|| | | |_) | _|| | | | | \ \ / /| _| | |_) | + | |__| |___| _ <| |__| |__| |_| |\ V / | |___| _ < + |_____\____|_| \_\_____\____\___/ \_/ |_____|_| \_\ + __ _ + _ _ _ __ ___ _ _ ___ ___ ___ ___ ___ / _|_ _| | + | | | | '_ \/ __| | | |/ __/ __/ _ \/ __/ __| |_| | | | | + | |_| | | | \__ \ |_| | (_| (_| __/\__ \__ \ _| |_| | | + \__,_|_| |_|___/\__,_|\___\___\___||___/___/_| \__,_|_| + _ _ _ + __ _| |_| |_ ___ _ __ ___ _ __ | |_ + / _` | __| __/ _ \ '_ ` _ \| '_ \| __| + | (_| | |_| || __/ | | | | | |_) | |_ + \__,_|\__|\__\___|_| |_| |_| .__/ \__| + |_| + + + +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| CMPTN | MACRO | XTERN | UTILS | row | computation | mandatory | result | Derived | God Given | +|:-----:+:-----:+:-----:+:-----:+:-------+------------------------------------+:---------:+------------------------------------+:---------------------------------------+------------------------| +| CMPTN | | | | i - 13 | tuple.chain_id ∈ ℕ_256 | ✓ | | | +| CMPTN | | | | i - 12 | tuple.nonce ∈ ℕ_64 | ✓ | | | +| CMPTN | | | | i - 11 | tuple.address ∈ 𝔹_20 | ✓ | | | +| CMPTN | | | | i - 10 | tuple.sig_y ∈ ℕ_8 | ✓ | (all required to succeed) | | +| CMPTN | | | | i - 9 | tuple.sig_r ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 8 | tuple.sig_s ∈ ℕ_8 | ✓ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 7 | tuple.chain_id == 0 | | ✨ chain_id_is_0 | | +| CMPTN | | | | i - 6 | tuple.chain_id == network_chain_id | | ✨ chain_id_is_β | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| ✓ | | | | | | | | ✨ chain_id_is_0_or_β ≡ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 5 | tuple.nonce < EIP_2681_MAX_NONCE | | ✨ nonce_satisfies_EIP_2681_bound | | +| CMPTN | | | | i - 4 | tuple.sig_s < secpk1_256n / 2 | | ✨ sig_s_is_non_malleable | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| ✓ | | | | | | | | ✨ ecrecover_attempt_expression ≡ | +| ✓ | | | | | | | | . chain_id_is_0_or_β | +| ✓ | | | | | | | | . ∧ nonce_satisfies_EIP_2681_bound | +| ✓ | | | | | | | | . ∧ sig_s_is_non_malleable | +| ✓ | | | | | | | | . ≡ ✅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 3 | tuple.nonce == authority.nonce | | ❌ nonce_equals_authority_nonce | | +| CMPTN | | | | i - 2 | tuple.address == from_address | | ❌ authority_is_sender | | +| CMPTN | | | | i - 1 | tuple.address == Address.ZERO | | ✨ address_is_zero | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | MACRO | | | i | ∅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| | ✓ | | | | | | | | ✅ tuple.chain_id | +| | ✓ | | | | | | | | ✅ tuple.nonce | +| | ✓ | | | | | | | | ✅ tuple.address | +| | ✓ | | | | | | | | ✅ tuple.sig_y | +| | ✓ | | | | | | | | ✅ tuple.sig_r | +| | ✓ | | | | | | | | ✅ tuple.sig_s | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| | | XTERN | | i + 1 | ∅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| | | ✓ | | | | | | | ✅ network_chain_id | +| | | ✓ | | | | | | | ✅ from_address | +| | | ✓ | | | | | | ✨ ecrecover_attempt | | +| | | ✓ | | | | | | . ← ecrecover_attempt_expression | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| | | ✓ | | | | | | ecrecover_attempt ≡ ✅ | | +| | | ✓ | | | | | | | ecrecover_success ≡ ❌ | +| | | ✓ | | | | | | call the hub ≡ ❌ | | +| | | ✓ | | | | | | authority_tuple_is_valid ≡ ❌ | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+------------------------| +| | | | UTILS | i + 2 | | | | Magic | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 3 | | | | ⟦RLP_UTILS_byte_string_prefix⟧ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 4 | | | | ⟦RLP_UTILS_integer⟧ | +| | | | UTILS | i + 5 | | | | | +| | | | UTILS | i + 6 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 7 | | | | ⟦RLP_UTILS_address⟧ | +| | | | UTILS | i + 8 | | | | | +| | | | UTILS | i + 9 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 10 | | | | ⟦RLP_UTILS_nonce⟧ | +| | | | UTILS | i + 11 | | | | | +| | | | UTILS | i + 12 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +|-------+-------+-------+-------+--------| +| CMPTN | | | | i + 13 | +|-------+-------+-------+-------+--------| + +Notes. +- ecrecover_attempt_expression ≡ ✅ dictates that an attempt is made at ECRECOVER-ing the authority address +- ecrecover_success ≡ ❌ means that that attempt is unsuccessful + - no HUB call is made + - no KECCAK call is made for the new code hash + +\end{verbatim} +\end{document} + diff --git a/rlp_auth/lua/ecrecover_no_attempt.lua.tex b/rlp_auth/lua/ecrecover_no_attempt.lua.tex new file mode 100644 index 00000000..e330926f --- /dev/null +++ b/rlp_auth/lua/ecrecover_no_attempt.lua.tex @@ -0,0 +1,99 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + + + + ██████\ ██\ ██\ ██\ +██ __██\ ██ | ██ | \__| +██ / \__| ██████\ ██████\████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ██████\ ███████\ ███████\ +██ | ██ __██\ ██ _██ _██\ ██ __██\ ██ | ██ |\_██ _| \____██\\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ | ██ / ██ |██ / ██ / ██ |██ / ██ |██ | ██ | ██ | ███████ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██\ ██ | ██ |██ | ██ | ██ |██ | ██ |██ | ██ | ██ |██\ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\██████ |\██████ |██ | ██ | ██ |███████ |\██████ | \████ |\███████ | \████ |██ |\██████ |██ | ██ |███████ | + \______/ \______/ \__| \__| \__|██ ____/ \______/ \____/ \_______| \____/ \__| \______/ \__| \__|\_______/ + ██ | + ██ | + \__| + + + _____ ____ ____ _____ ____ _____ _______ ____ + _ __ ___ | ____/ ___| _ \| ____/ ___/ _ \ \ / / ____| _ \ + | '_ \ / _ \ | _|| | | |_) | _|| | | | | \ \ / /| _| | |_) | + | | | | (_) | | |__| |___| _ <| |__| |__| |_| |\ V / | |___| _ < + |_| |_|\___/ |_____\____|_| \_\_____\____\___/ \_/ |_____|_| \_\ + + _ _ _ _ + __ _| |_| |_ ___ _ __ ___ _ __ | |_ _ __ ___ __ _ __| | ___ + / _` | __| __/ _ \ '_ ` _ \| '_ \| __| | '_ ` _ \ / _` |/ _` |/ _ \ + | (_| | |_| || __/ | | | | | |_) | |_ | | | | | | (_| | (_| | __/ + \__,_|\__|\__\___|_| |_| |_| .__/ \__| |_| |_| |_|\__,_|\__,_|\___| + |_| + +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+----------------------| +| CMPTN | MACRO | XTERN | UTILS | row | computation | mandatory | result | derived | god given | +|:-----:+:-----:+:-----:+:-----:+:-------+------------------------------------+:---------:+------------------------------------+:------------------------------------------+----------------------| +| CMPTN | | | | i - 13 | tuple.chain_id ∈ ℕ_256 | ✓ | | | +| CMPTN | | | | i - 12 | tuple.nonce ∈ ℕ_64 | ✓ | | | +| CMPTN | | | | i - 11 | tuple.address ∈ 𝔹_20 | ✓ | (all required to succeed) | | +| CMPTN | | | | i - 10 | tuple.sig_y ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 9 | tuple.sig_r ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 8 | tuple.sig_s ∈ ℕ_8 | ✓ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 7 | tuple.chain_id == 0 | | ✨ chain_id_is_0 | +| CMPTN | | | | i - 6 | tuple.chain_id == network_chain_id | | ✨ chain_id_is_β | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | | | | | | | | ✨ chain_id_is_0_or_β ≡ | +| | | | | | | | | . chain_id_is_0 | +| | | | | | | | | . ∨ chain_id_is_β | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 5 | tuple.nonce < EIP_2681_MAX_NONCE | | ✨ nonce_satisfies_EIP_2681_bound | +| CMPTN | | | | i - 4 | tuple.sig_s < secpk1_256n / 2 | | ✨ sig_s_is_non_malleable | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | | | | | | | | ✨ ecrecover_attempt_expression ≡ | +| | | | | | | | | . chain_id_is_0_or_β | +| | | | | | | | | . ∧ nonce_satisfies_EIP_2681_bound | +| | | | | | | | | . ∧ sig_s_is_non_malleable | +| ✓ | | | | | | | | . ≡ ❌ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| CMPTN | | | | i - 3 | tuple.nonce == authority.nonce | | ✨ nonce_equals_authority_nonce | MEANINGFUL IFF ecrecover_attempt ≡ | +| CMPTN | | | | i - 2 | tuple.address == from_address | | ✨ authority_is_sender | MEANINGFUL IFF ecrecover_attempt ≡ | +| CMPTN | | | | i - 1 | tuple.address == Address.ZERO | | ✨ address_is_zero | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------| +| | MACRO | | | i | ∅ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+----------------------| +| | | | | | | | | | ✅ tuple.chain_id | +| | | | | | | | | | ✅ tuple.nonce | +| | | | | | | | | | ✅ tuple.address | +| | | | | | | | | | ✅ tuple.sig_y | +| | | | | | | | | | ✅ tuple.sig_r | +| | | | | | | | | | ✅ tuple.sig_s | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+----------------------| +| | | XTERN | | i + 1 | ∅ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+----------------------| +| | | | | | | | | | ✅ network_chain_id | +| | | | | | | | | | ✅ from_address | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+-------------------------------------------+----------------------| +|-------+-------+-------+-------+--------| +| CMPTN | | | | i + 2 | +|-------+-------+-------+-------+--------| + + +Notes. +- ecrecover_attempt_expression ≡ ❌ dictates that no attempt is made at ECRECOVER-ing the authority address +- ecrecover_success ≡ ❌ follows automatically + - no HUB call is made + - no KECCAK call is made for the new code hash + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/ecrecover_success.lua.tex b/rlp_auth/lua/ecrecover_success.lua.tex new file mode 100644 index 00000000..34d28651 --- /dev/null +++ b/rlp_auth/lua/ecrecover_success.lua.tex @@ -0,0 +1,132 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + + + ██████\ ██\ ██\ ██\ +██ __██\ ██ | ██ | \__| +██ / \__| ██████\ ██████\████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ██████\ ███████\ ███████\ +██ | ██ __██\ ██ _██ _██\ ██ __██\ ██ | ██ |\_██ _| \____██\\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ | ██ / ██ |██ / ██ / ██ |██ / ██ |██ | ██ | ██ | ███████ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██\ ██ | ██ |██ | ██ | ██ |██ | ██ |██ | ██ | ██ |██\ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\██████ |\██████ |██ | ██ | ██ |███████ |\██████ | \████ |\███████ | \████ |██ |\██████ |██ | ██ |███████ | + \______/ \______/ \__| \__| \__|██ ____/ \______/ \____/ \_______| \____/ \__| \______/ \__| \__|\_______/ + ██ | + ██ | + \__| + + + _____ ____ ____ _____ ____ _____ _______ ____ + | ____/ ___| _ \| ____/ ___/ _ \ \ / / ____| _ \ + | _|| | | |_) | _|| | | | | \ \ / /| _| | |_) | + | |__| |___| _ <| |__| |__| |_| |\ V / | |___| _ < + |_____\____|_| \_\_____\____\___/ \_/ |_____|_| \_\ + __ _ + ___ _ _ ___ ___ ___ ___ ___ / _|_ _| | + / __| | | |/ __/ __/ _ \/ __/ __| |_| | | | | + \__ \ |_| | (_| (_| __/\__ \__ \ _| |_| | | + |___/\__,_|\___\___\___||___/___/_| \__,_|_| + _ _ _ + __ _| |_| |_ ___ _ __ ___ _ __ | |_ + / _` | __| __/ _ \ '_ ` _ \| '_ \| __| + | (_| | |_| || __/ | | | | | |_) | |_ + \__,_|\__|\__\___|_| |_| |_| .__/ \__| + |_| + + + +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| CMPTN | MACRO | XTERN | UTILS | row | computation | mandatory | result | Derived | God Given | +|:-----:+:-----:+:-----:+:-----:+:-------+------------------------------------+:---------:+------------------------------------+:---------------------------------------+----------------------| +| CMPTN | | | | i - 13 | tuple.chain_id ∈ ℕ_256 | ✓ | | | +| CMPTN | | | | i - 12 | tuple.nonce ∈ ℕ_64 | ✓ | | | +| CMPTN | | | | i - 11 | tuple.address ∈ 𝔹_20 | ✓ | | | +| CMPTN | | | | i - 10 | tuple.sig_y ∈ ℕ_8 | ✓ | (all required to succeed) | | +| CMPTN | | | | i - 9 | tuple.sig_r ∈ ℕ_8 | ✓ | | | +| CMPTN | | | | i - 8 | tuple.sig_s ∈ ℕ_8 | ✓ | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 7 | tuple.chain_id == 0 | | ✨ chain_id_is_0 | | +| CMPTN | | | | i - 6 | tuple.chain_id == network_chain_id | | ✨ chain_id_is_β | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| ✓ | | | | | | | | ✨ chain_id_is_0_or_β ≡ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 5 | tuple.nonce < EIP_2681_MAX_NONCE | | ✨ nonce_satisfies_EIP_2681_bound | | +| CMPTN | | | | i - 4 | tuple.sig_s < secpk1_256n / 2 | | ✨ sig_s_is_non_malleable | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| ✓ | | | | | | | | ✨ ecrecover_attempt_expression ≡ | +| ✓ | | | | | | | | . chain_id_is_0_or_β | +| ✓ | | | | | | | | . ∧ nonce_satisfies_EIP_2681_bound | +| ✓ | | | | | | | | . ∧ sig_s_is_non_malleable | +| ✓ | | | | | | | | . ≡ ✅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| CMPTN | | | | i - 3 | tuple.nonce == authority.nonce | | ✨ nonce_equals_authority_nonce | | +| CMPTN | | | | i - 2 | tuple.address == from_address | | ✨ authority_is_sender | | +| CMPTN | | | | i - 1 | tuple.address == Address.ZERO | | ✨ address_is_zero | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | MACRO | | | i | ∅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| | ✓ | | | | | | | | ✅ tuple.chain_id | +| | ✓ | | | | | | | | ✅ tuple.nonce | +| | ✓ | | | | | | | | ✅ tuple.address | +| | ✓ | | | | | | | | ✅ tuple.sig_y | +| | ✓ | | | | | | | | ✅ tuple.sig_r | +| | ✓ | | | | | | | | ✅ tuple.sig_s | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| | | XTERN | | i + 1 | ∅ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| | | ✓ | | | | | | | ✅ network_chain_id | +| | | ✓ | | | | | | | ✅ from_address | +| | | ✓ | | | | | | ✨ ecrecover_attempt | | +| | | ✓ | | | | | | . ← ecrecover_attempt_expression | | +| | | ✓ | | | | | | | ✅ authority.nonce | +| | | ✓ | | | | | | | ✅ from_address | +| | | ✓ | | | | | | ✨ potential_new_code_hash | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| | | ✓ | | | | | | ecrecover_attempt ≡ ✅ | | +| | | ✓ | | | | | | | ✅ ecrecover_success | +| | | ✓ | | | | | | call the hub ≡ ✅ | | +| | | ✓ | | | | | | authority_tuple_is_valid ≡ ❓ | | +| | | ✓ | | | | | | | ✅ ecrecover_success | +| | | ✓ | | | | | | | ✅ code_hash | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------+----------------------| +| | | | UTILS | i + 2 | | | | Magic | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 3 | | | | ⟦RLP_UTILS_byte_string_prefix⟧ | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 4 | | | | ⟦RLP_UTILS_integer⟧ | +| | | | UTILS | i + 5 | | | | | +| | | | UTILS | i + 6 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 7 | | | | ⟦RLP_UTILS_address⟧ | +| | | | UTILS | i + 8 | | | | | +| | | | UTILS | i + 9 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +| | | | UTILS | i + 10 | | | | ⟦RLP_UTILS_nonce⟧ | +| | | | UTILS | i + 11 | | | | | +| | | | UTILS | i + 12 | | | | | +|-------+-------+-------+-------+--------+------------------------------------+-----------+------------------------------------+----------------------------------------| +|-------+-------+-------+-------+--------| +| CMPTN | | | | i + 13 | +|-------+-------+-------+-------+--------| + +Notes. +- ecrecover_attempt_expression ≡ ✅ dictates that an attempt is made at ECRECOVER-ing the authority address +- ecrecover_success ≡ ✅ means that that attempt is successful +- a HUB call is made ≡ ✅ and the following comparisons become MEANINGFUL + - tuple.nonce == authority.nonce + - tuple.address == from_address + +- a KECCAK call is made for the new code hash + +\end{verbatim} +\end{document} + diff --git a/rlp_auth/lua/extraction_for_ecrecover___pre_verticalization.lua.tex b/rlp_auth/lua/extraction_for_ecrecover___pre_verticalization.lua.tex new file mode 100644 index 00000000..e3325d79 --- /dev/null +++ b/rlp_auth/lua/extraction_for_ecrecover___pre_verticalization.lua.tex @@ -0,0 +1,57 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +████████\ ██████\ ███████\ ████████\ ██████\ ██████\ ██\ ██\ ████████\ ███████\ ██\ ██\ +██ _____|██ __██\ ██ __██\ ██ _____|██ __██\ ██ __██\ ██ | ██ |██ _____|██ __██\ ██ | ██ | +██ | ██ / \__|██ | ██ |██ | ██ / \__|██ / ██ |██ | ██ |██ | ██ | ██ | ███████ | ██████\ ██████\ ██████\ +█████\ ██ | ███████ |█████\ ██ | ██ | ██ |\██\ ██ |█████\ ███████ | ██ __██ | \____██\\_██ _| \____██\ +██ __| ██ | ██ __██< ██ __| ██ | ██ | ██ | \██\██ / ██ __| ██ __██< ██ / ██ | ███████ | ██ | ███████ | +██ | ██ | ██\ ██ | ██ |██ | ██ | ██\ ██ | ██ | \███ / ██ | ██ | ██ | ██ | ██ |██ __██ | ██ |██\ ██ __██ | +████████\ \██████ |██ | ██ |████████\ \██████ | ██████ | \█ / ████████\ ██ | ██ | \███████ |\███████ | \████ |\███████ | +\________| \______/ \__| \__|\________| \______/ \______/ \_/ \________|\__| \__| \_______| \_______| \____/ \_______| + + + + ██\ ██\ ██\ ██\ ██\ ██\ + ██ | \__| ██ |\__| ██ | \__| + ██████\ ██████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ██████\ ██\ ██████\ ███████\ +██ __██\ ██ __██\ ██ __██\ ██████\\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |\____██\\_██ _| ██ |██ __██\ ██ __██\ +██ / ██ |██ | \__|████████ |\______|\██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ███████ | ██ | ██ |██ / ██ |██ | ██ | +██ | ██ |██ | ██ ____| \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | +███████ |██ | \███████\ \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\\███████ | \████ |██ |\██████ |██ | ██ | +██ ____/ \__| \_______| \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________|\_______| \____/ \__| \______/ \__| \__| +██ | +██ | +\__| + + + + +|-------------------|---------------|---------|---------------------|------------------|------------------|------------------|------------------|--------------------------------------|------------------------|------------------------|---------------|--------------|----------------------------------------------------|----------|--------------------| +| φ_USER_TXN_NUMBER | φ_TUPLE_INDEX | φ_MACRO | φ_macro/SIGNATURE_Y | φ_SIGNATURE_R_HI | φ_SIGNATURE_R_LO | φ_SIGNATURE_S_HI | φ_SIGNATURE_S_LO | φ_extern/AUTHORITY_ECRECOVER_SUCCESS | φ_AUTHORITY_ADDRESS_HI | φ_AUTHORITY_ADDRESS_LO | φ_IS_DATA (?) | φ_LIMB_INDEX | φ_LIMB | φ_nBYTES | φ_LIMB_CONSTRUCTED | +|:-----------------:|:-------------:|--------:|:-------------------:|:----------------:|:----------------:|:----------------:|:----------------:|:------------------------------------:|:----------------------:|:----------------------:|:-------------:|:------------:|:---------------------------------------------------|:--------:|:------------------:| +| n | a | | | | | | | | | | | | | | | +| n | a | | | | | | | | | | | | | | | +| n | a | | | | | | | | | | | 0 | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 1 | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 2 | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 3 | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | | +| n | a | | | | | | | | | | | 4 | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 5 | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | | +| n | a | | | | | | | | | | | 6 | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | | +| n | a | | | | | | | | | | | 7 | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | | +| n | a | | | | | | | | | | | 8 | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | | +|-------------------|---------------|---------|---------------------|------------------|------------------|------------------|------------------|--------------------------------------|------------------------|------------------------|---------------|--------------|----------------------------------------------------|----------|--------------------| + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/extraction_for_ecrecover___prover_columns.lua.tex b/rlp_auth/lua/extraction_for_ecrecover___prover_columns.lua.tex new file mode 100644 index 00000000..28ff98a0 --- /dev/null +++ b/rlp_auth/lua/extraction_for_ecrecover___prover_columns.lua.tex @@ -0,0 +1,172 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +██\ ██\ ██\ ██\ ██\ ██\ ██\ +██ | ██ | ██ | \__| ██ |\__| ██ | +██ | ██ | ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ███████ | +\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |██ __██\ ██ __██ | + \██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ████████ |██ / ██ | + \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ ____|██ | ██ | + \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\ \███████\ \███████ | + \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________| \_______| \_______| + + + +████████\ ██████\ ███████\ ████████\ ██████\ ██████\ ██\ ██\ ████████\ ███████\ +██ _____|██ __██\ ██ __██\ ██ _____|██ __██\ ██ __██\ ██ | ██ |██ _____|██ __██\ +██ | ██ / \__|██ | ██ |██ | ██ / \__|██ / ██ |██ | ██ |██ | ██ | ██ | +█████\ ██ | ███████ |█████\ ██ | ██ | ██ |\██\ ██ |█████\ ███████ | +██ __| ██ | ██ __██< ██ __| ██ | ██ | ██ | \██\██ / ██ __| ██ __██< +██ | ██ | ██\ ██ | ██ |██ | ██ | ██\ ██ | ██ | \███ / ██ | ██ | ██ | +████████\ \██████ |██ | ██ |████████\ \██████ | ██████ | \█ / ████████\ ██ | ██ | +\________| \______/ \__| \__|\________| \______/ \______/ \_/ \________|\__| \__| + + + + ██\ + ██ | + ███████\ ██████\ ██ |██\ ██\ ██████\████\ ███████\ +██ _____|██ __██\ ██ |██ | ██ |██ _██ _██\ ██ __██\ +██ / ██ / ██ |██ |██ | ██ |██ / ██ / ██ |██ | ██ | +██ | ██ | ██ |██ |██ | ██ |██ | ██ | ██ |██ | ██ | +\███████\ \██████ |██ |\██████ |██ | ██ | ██ |██ | ██ | + \_______| \______/ \__| \______/ \__| \__| \__|\__| \__| + + + + ██\ ██████\ ██\ ██\ ██\ ██\ + ██ | ██ __██\ \__| \__| ██ | \__| + ███████ | ██████\ ██ / \__|██\ ███████\ ██\ ██████\ ██\ ██████\ ███████\ ███████\ +██ __██ |██ __██\ ████\ ██ |██ __██\ ██ |\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ / ██ |████████ |██ _| ██ |██ | ██ |██ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██ |██ ____|██ | ██ |██ | ██ |██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\███████ |\███████\ ██ | ██ |██ | ██ |██ | \████ |██ |\██████ |██ | ██ |███████ | + \_______| \_______|\__| \__|\__| \__|\__| \____/ \__| \______/ \__| \__|\_______/ + + + + +########################################################################################## + +NOTE. The following defines columns in the arithmetization which extract the data required +by the prover to handle the ECRECOVER attempts associated with a particular authority list +tuple. Such attempts are made whenever + + xtern/AUTHORITY_ECRECOVER_ATTEMPT ≡ + +########################################################################################## + + + +(module rlpauth) + +(defun (rlpauth-ecrecover-trigger) (* XTERN xtern/AUTHORITY_ECRECOVER_ATTEMPT)) + +(defconst + ROFF___Y 7 + ROFF___R_HI 6 + ROFF___R_LO 5 + ROFF___S_HI 4 + ROFF___S_LO 3 + ROFF___ADDR_HI 2 + ROFF___ADDR_LO 1 + ROFF___SUC_BIT 0 + ) + +(defun (macro-selector---y-parity) (shift (rlpauth-ecrecover-trigger) ROFF___Y )) +(defun (macro-selector---r-hi) (shift (rlpauth-ecrecover-trigger) ROFF___R_HI )) +(defun (macro-selector---r-lo) (shift (rlpauth-ecrecover-trigger) ROFF___R_LO )) +(defun (macro-selector---s-hi) (shift (rlpauth-ecrecover-trigger) ROFF___S_HI )) +(defun (macro-selector---s-lo) (shift (rlpauth-ecrecover-trigger) ROFF___S_LO )) +(defun (xtern-selector---address-hi) (shift (rlpauth-ecrecover-trigger) ROFF___ADDR_HI )) +(defun (xtern-selector---address-lo) (shift (rlpauth-ecrecover-trigger) ROFF___ADDR_LO )) +(defun (xtern-selector---success-bit) (shift (rlpauth-ecrecover-trigger) ROFF___SUC_BIT )) +(defun (message-selector) (* UTILS utils/LIMB_BIT)) + + +(defun (ecrecover-limb---y-parity) (shift macro/Y_PARITY (- ROFF___Y 1) )) +(defun (ecrecover-limb---r-hi) (shift macro/SIG_R_HI (- ROFF___R_HI 1) )) +(defun (ecrecover-limb---r-lo) (shift macro/SIG_R_LO (- ROFF___R_LO 1) )) +(defun (ecrecover-limb---s-hi) (shift macro/SIG_S_HI (- ROFF___S_HI 1) )) +(defun (ecrecover-limb---s-lo) (shift macro/SIG_S_LO (- ROFF___S_LO 1) )) +(defun (ecrecover-limb---address-hi) (shift xtern/ADDRESS_HI ROFF___ADDR_HI )) +(defun (ecrecover-limb---address-lo) (shift xtern/ADDRESS_LO ROFF___ADDR_LO )) +(defun (ecrecover-limb---success-bit) (shift xtern/AUTHORITY_RECOVERY_SUCCESS ROFF___SUC_BIT )) + + +(defcomputed (ecrecover-extraction---IS_SIGNATURE) + (+ (macro-selector---y-parity) + (macro-selector---r-hi) + (macro-selector---r-lo) + (macro-selector---s-hi) + (macro-selector---s-lo) + )) + +(defcomputed (ecrecover-extraction---IS_RESULT) + (+ (xtern-selector---address-hi) + (xtern-selector---address-lo) + (xtern-selector---success-bit) + )) + +(defcomputed (ecrecover-extraction---IS_MESSAGE) + (message-selector) + ) + +(defcomputed (ecrecover-extraction---USER_TXN_NUMBER) + (* (+ (ecrecover-extraction---IS_SIGNATURE) + (ecrecover-extraction---IS_RESULT) + (ecrecover-extraction---IS_MESSAGE)) + USER_TXN_NUMBER + )) + +(defcomputed (ecrecover-extraction---TUPLE_INDEX) + (* (+ (ecrecover-extraction---IS_SIGNATURE) + (ecrecover-extraction---IS_RESULT) + (ecrecover-extraction---IS_MESSAGE)) + TUPLE_INDEX + )) + +(defcomputed (ecrecover-extraction---LIMB) + (+ (* (macro-selector---y-parity) (ecrecover-limb---y-parity) ) + (* (macro-selector---r-hi) (ecrecover-limb---r-hi) ) + (* (macro-selector---r-lo) (ecrecover-limb---r-lo) ) + (* (macro-selector---s-hi) (ecrecover-limb---s-hi) ) + (* (macro-selector---s-lo) (ecrecover-limb---s-lo) ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (xtern-selector---address-hi) (ecrecover-limb---address-hi) ) + (* (xtern-selector---address-lo) (ecrecover-limb---address-lo) ) + (* (xtern-selector---success-bit) (ecrecover-limb---success-bit) ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (ecrecover-extraction---IS_MESSAGE) utils/LIMB_INDEX ) + )) + +(defcomputed (ecrecover-extraction---LIMB_SIZE) + (* (ecrecover-extraction---IS_MESSAGE) utils/LIMB_SIZE) + ) + +(defcomputed (ecrecover-extraction---LIMB_INDEX) + (+ (* (macro-selector---y-parity) 0 ) + (* (macro-selector---r-hi) 1 ) + (* (macro-selector---r-lo) 2 ) + (* (macro-selector---s-hi) 3 ) + (* (macro-selector---s-lo) 4 ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (xtern-selector---address-hi) 0 ) + (* (xtern-selector---address-lo) 1 ) + (* (xtern-selector---success-bit) 2 ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (ecrecover-extraction---IS_MESSAGE) utils/LIMB_INDEX ) + )) + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/extraction_for_ecrecover___verticalized.lua.tex b/rlp_auth/lua/extraction_for_ecrecover___verticalized.lua.tex new file mode 100644 index 00000000..e54a5894 --- /dev/null +++ b/rlp_auth/lua/extraction_for_ecrecover___verticalized.lua.tex @@ -0,0 +1,86 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +██\ ██\ ██\ ██\ ██\ ██\ ██\ +██ | ██ | ██ | \__| ██ |\__| ██ | +██ | ██ | ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ███████ | +\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |██ __██\ ██ __██ | + \██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ████████ |██ / ██ | + \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ ____|██ | ██ | + \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\ \███████\ \███████ | + \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________| \_______| \_______| + + + +████████\ ██████\ ███████\ ████████\ ██████\ ██████\ ██\ ██\ ████████\ ███████\ ██\ ██\ +██ _____|██ __██\ ██ __██\ ██ _____|██ __██\ ██ __██\ ██ | ██ |██ _____|██ __██\ ██ | ██ | +██ | ██ / \__|██ | ██ |██ | ██ / \__|██ / ██ |██ | ██ |██ | ██ | ██ | ███████ | ██████\ ██████\ ██████\ +█████\ ██ | ███████ |█████\ ██ | ██ | ██ |\██\ ██ |█████\ ███████ | ██ __██ | \____██\\_██ _| \____██\ +██ __| ██ | ██ __██< ██ __| ██ | ██ | ██ | \██\██ / ██ __| ██ __██< ██ / ██ | ███████ | ██ | ███████ | +██ | ██ | ██\ ██ | ██ |██ | ██ | ██\ ██ | ██ | \███ / ██ | ██ | ██ | ██ | ██ |██ __██ | ██ |██\ ██ __██ | +████████\ \██████ |██ | ██ |████████\ \██████ | ██████ | \█ / ████████\ ██ | ██ | \███████ |\███████ | \████ |\███████ | +\________| \______/ \__| \__|\________| \______/ \______/ \_/ \________|\__| \__| \_______| \_______| \____/ \_______| + + + + +|-----------------+-------------+--------------+-----------+------------+----------------------------------------------------+-----------+-------| +| USER_TXN_NUMBER | TUPLE_INDEX | is_signature | is_result | is_message | limb | limb_size | index | +|:---------------:+:-----------:+:------------:+:---------:+:----------:+----------------------------------------------------+:---------:+:-----:| +| n | a | | | | | | 0 | +| n | a | | | | | | 1 | +| n | a | | | | | | 2 | +| n | a | | | | | | 3 | +| n | a | | | | | | 4 | +|-----------------+-------------+--------------+-----------+------------+----------------------------------------------------+-----------+-------| +| n | a | | | | | | 0 | +| n | a | | | | | | 1 | +| n | a | | | | | | 2 | +|-----------------+-------------+--------------+-----------+------------+----------------------------------------------------+-----------+-------| +| n | a | | | | 0x 05 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 0 | +| n | a | | | | 0x 9d .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 1 | +| n | a | | | | 0x 83 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 2 | +| n | a | | | | 0x ff ff ff .. .. .. .. .. .. .. .. .. .. .. .. .. | 3 | 3 | +| n | a | | | | 0x 94 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 4 | +| n | a | | | | 0x ad dr es s0 .. .. .. .. .. .. .. .. .. .. .. .. | 4 | 5 | +| n | a | | | | 0x ff ff ff ad dr es s0 ad dr es s0 11 11 11 11 11 | 16 | 6 | +| n | a | | | | 0x 82 .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 1 | 7 | +| n | a | | | | 0x 13 37 .. .. .. .. .. .. .. .. .. .. .. .. .. .. | 2 | 8 | +|-----------------+-------------+--------------+-----------+------------+----------------------------------------------------+-----------+-------| +| ∅ | +| ⋮ | +| ∅ | +|:---------------:+:-----------:+--------------+-----------+------------+----------------------------------------------------+:---------:+:-----:| +| m | b | | | | | | 0 | +| ⋮ | | | | | | | | + + +NOTE. The column names are different in the implementation: + + +|-----------------+---+----------------------------------------| +| name in diagram | | column name in implementation | +|-----------------+---+----------------------------------------| +| USER_TXN_NUMBER | ⇒ | ecrecover-extraction---USER_TXN_NUMBER | +| TUPLE_INDEX | ⇒ | ecrecover-extraction---TUPLE_INDEX | +| is_signature | ⇒ | ecrecover-extraction---IS_SIGNATURE | +| is_result | ⇒ | ecrecover-extraction---IS_RESULT | +| is_message | ⇒ | ecrecover-extraction---IS_MESSAGE | +| limb | ⇒ | ecrecover-extraction---LIMB | +| limb_size | ⇒ | ecrecover-extraction---LIMB_SIZE | +| index | ⇒ | ecrecover-extraction---LIMB_INDEX | +|-----------------+---+----------------------------------------| + + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/extraction_for_keccak___pre_verticalization.lua.tex b/rlp_auth/lua/extraction_for_keccak___pre_verticalization.lua.tex new file mode 100644 index 00000000..c896cc8c --- /dev/null +++ b/rlp_auth/lua/extraction_for_keccak___pre_verticalization.lua.tex @@ -0,0 +1,94 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +██\ ██\ ████████\ ██████\ ██████\ ██████\ ██\ ██\ ██\ ██\ +██ | ██ |██ _____|██ __██\ ██ __██\ ██ __██\ ██ | ██ | ██ | ██ | +██ |██ / ██ | ██ / \__|██ / \__|██ / ██ |██ |██ / ███████ | ██████\ ██████\ ██████\ +█████ / █████\ ██ | ██ | ████████ |█████ / ██ __██ | \____██\\_██ _| \____██\ +██ ██< ██ __| ██ | ██ | ██ __██ |██ ██< ██ / ██ | ███████ | ██ | ███████ | +██ |\██\ ██ | ██ | ██\ ██ | ██\ ██ | ██ |██ |\██\ ██ | ██ |██ __██ | ██ |██\ ██ __██ | +██ | \██\ ████████\ \██████ |\██████ |██ | ██ |██ | \██\ \███████ |\███████ | \████ |\███████ | +\__| \__|\________| \______/ \______/ \__| \__|\__| \__| \_______| \_______| \____/ \_______| + + + + ██\ ██\ ██\ ██\ ██\ ██\ + ██ | \__| ██ |\__| ██ | \__| + ██████\ ██████\ ██████\ ██\ ██\ ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ██████\ ██\ ██████\ ███████\ +██ __██\ ██ __██\ ██ __██\ ██████\\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |\____██\\_██ _| ██ |██ __██\ ██ __██\ +██ / ██ |██ | \__|████████ |\______|\██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ███████ | ██ | ██ |██ / ██ |██ | ██ | +██ | ██ |██ | ██ ____| \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ __██ | ██ |██\ ██ |██ | ██ |██ | ██ | +███████ |██ | \███████\ \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\\███████ | \████ |██ |\██████ |██ | ██ | +██ ____/ \__| \_______| \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________|\_______| \____/ \__| \______/ \__| \__| +██ | +██ | +\__| + + + + +| φ_SEL | φ_USER_TXN_NUMBER | φ_TUPLE_INDEX | φ_shifted_code_prefix | φ_shifted_xtern/ADDRESS_HI | φ_shifted_xtern/ADDRESS_LO | φ_xtern/CODE_HASH_HI | φ_xtern/CODE_HASH_LO | +|:-----:+:-----------------:+:-------------:+:----------------------------+------------------------------+----------------------------+----------------------+----------------------| +| ⋮ | | | | | | | | +| 0 | | | | | | | | +| 1 | 13 | 0 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 13 | 1 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 13 | 7 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 13 | 8 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 13 | 39 | 0x ef0001.................. | 0x ................ | 0x | | | +|-------+-------------------+---------------+-----------------------------+------------------------------+----------------------------+----------------------+----------------------| +| 1 | 66 | 0 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 1 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 2 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 3 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 4 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 5 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 66 | 6 | 0x ef0001.................. | 0x ................ | 0x | | | +|-------+-------------------+---------------+-----------------------------+------------------------------+----------------------------+----------------------+----------------------| +| 1 | 198 | 21 | 0x ef0001.................. | 0x ................ | 0x | | | +| 1 | 198 | 22 | 0x ef0001.................. | 0x ................ | 0x | | | +|-------+-------------------+---------------+-----------------------------+------------------------------+----------------------------+----------------------+----------------------| +| 0 | | | | | | | | +| ⋮ | | | | | | | | + +NOTE. We write φ_XXX for the appropriately selector-filtered column XXX, i.e. φ_XXX ≡ sel ∙ XXX +NOTE. As per usual, '.' in a limb stands for 0. All 'limbs' are thus left aligned on the 16-th byte. +NOTE. When nontrivial, + +* φ_shifted_code_prefix ≡ 3 data bytes (always 0xef0001, left aligned on the 16th byte) +* φ_shifted_xtern/ADDRESS_HI ≡ 4 data bytes +* φ_shifted_xtern/ADDRESS_LO ≡ 16 data bytes + +NOTE. When nontrivial, "φ_xtern/CODE_HASH" should contain the following (split into hi/lo parts) + + code ≡ 0xef0001 ∙ address + KECCAK( code ) + +where ∙ stands for byte concatenation, and the 'code' is thus always a 23 byte string. + +NOTE. Between any rows that are "nontrivial" there will be several (at least 13, but potentially unboundedly many) "trivial rows" + +| φ_SEL | | | | | | | | +|-------+---+---+---+---+---+---+---| +| 1 | X | X | X | X | X | X | X | ← "nontrivial row" +| 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | ← "trivial row" +| ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | +| 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +| 1 | Y | Y | Y | Y | Y | Y | Y | ← other "nontrivial row" + +NOTE. There are at least 13 + 1 + 1 + (1 + 1 + 3 + 3 + 3) between any two "nontrivial rows" + +NOTE. The prefix can be added by the prover circuit. + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/extraction_for_keccak___prover_columns.lua.tex b/rlp_auth/lua/extraction_for_keccak___prover_columns.lua.tex new file mode 100644 index 00000000..a00195aa --- /dev/null +++ b/rlp_auth/lua/extraction_for_keccak___prover_columns.lua.tex @@ -0,0 +1,157 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +██\ ██\ ██\ ██\ ██\ ██\ ██\ +██ | ██ | ██ | \__| ██ |\__| ██ | +██ | ██ | ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ███████ | +\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |██ __██\ ██ __██ | + \██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ████████ |██ / ██ | + \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ ____|██ | ██ | + \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\ \███████\ \███████ | + \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________| \_______| \_______| + + + +██\ ██\ ████████\ ██████\ ██████\ ██████\ ██\ ██\ +██ | ██ |██ _____|██ __██\ ██ __██\ ██ __██\ ██ | ██ | +██ |██ / ██ | ██ / \__|██ / \__|██ / ██ |██ |██ / +█████ / █████\ ██ | ██ | ████████ |█████ / +██ ██< ██ __| ██ | ██ | ██ __██ |██ ██< +██ |\██\ ██ | ██ | ██\ ██ | ██\ ██ | ██ |██ |\██\ +██ | \██\ ████████\ \██████ |\██████ |██ | ██ |██ | \██\ +\__| \__|\________| \______/ \______/ \__| \__|\__| \__| + + + + ██\ + ██ | + ███████\ ██████\ ██ |██\ ██\ ██████\████\ ███████\ +██ _____|██ __██\ ██ |██ | ██ |██ _██ _██\ ██ __██\ +██ / ██ / ██ |██ |██ | ██ |██ / ██ / ██ |██ | ██ | +██ | ██ | ██ |██ |██ | ██ |██ | ██ | ██ |██ | ██ | +\███████\ \██████ |██ |\██████ |██ | ██ | ██ |██ | ██ | + \_______| \______/ \__| \______/ \__| \__| \__|\__| \__| + + + + ██\ ██████\ ██\ ██\ ██\ ██\ + ██ | ██ __██\ \__| \__| ██ | \__| + ███████ | ██████\ ██ / \__|██\ ███████\ ██\ ██████\ ██\ ██████\ ███████\ ███████\ +██ __██ |██ __██\ ████\ ██ |██ __██\ ██ |\_██ _| ██ |██ __██\ ██ __██\ ██ _____| +██ / ██ |████████ |██ _| ██ |██ | ██ |██ | ██ | ██ |██ / ██ |██ | ██ |\██████\ +██ | ██ |██ ____|██ | ██ |██ | ██ |██ | ██ |██\ ██ |██ | ██ |██ | ██ | \____██\ +\███████ |\███████\ ██ | ██ |██ | ██ |██ | \████ |██ |\██████ |██ | ██ |███████ | + \_______| \_______|\__| \__|\__| \__|\__| \____/ \__| \______/ \__| \__|\_______/ + + + + +########################################################################################## + +NOTE. The following defines columns in the arithmetization which extract the data required +by the prover to handle the KECCAK calls associated with a particular authority list tuple. +Such attempts are made whenever + + xtern/AUTHORITY_RECOVERY_SUCCESS ≡ + +########################################################################################## + + + +(module rlpauth) + +(defun (rlpauth-keccak-trigger) (* XTERN xtern/AUTHORITY_ECRECOVER_SUCCESS)) + +(defconst + + DELEGATION_PREFIX 0xef0100 + + ROFF___PREFIX 4 + ROFF___ADDRESS_HI 3 + ROFF___ADDRESS_LO 2 + ROFF___KECCAK_HI 1 + ROFF___KECCAK_LO 0 + + LIMB_SIZE___DELEGATION_PREFIX 3 + LIMB_SIZE___ADDRESS_HI 4 + LIMB_SIZE___ADDRESS_LO 16 + + SHIFT_FACTOR___PREFIX (^ 256 (- 16 LIMB_SIZE___DELEGATION_PREFIX )) + SHIFT_FACTOR___ADDRESS_HI (^ 256 (- 16 LIMB_SIZE___ADDRESS_HI )) + SHIFT_FACTOR___ADDRESS_LO (^ 256 (- 16 LIMB_SIZE___ADDRESS_LO )) + ) + +(defun (prefix-selector) (shift (rlpauth-keccak-trigger) ROFF___PREFIX )) +(defun (macro-selector---address-hi) (shift (rlpauth-keccak-trigger) ROFF___ADDRESS_HI )) +(defun (macro-selector---address-lo) (shift (rlpauth-keccak-trigger) ROFF___ADDRESS_LO )) +(defun (xtern-selector---keccak-hi) (shift (rlpauth-keccak-trigger) ROFF___KECCAK_HI )) +(defun (xtern-selector---keccak-lo) (shift (rlpauth-keccak-trigger) ROFF___KECCAK_LO )) + + +(defun (keccak-limb---input---left-shifted-prefix) (* DELEGATION_PREFIX SHIFT_FACTOR___DELEGATION_PREFIX ) ) +(defun (keccak-limb---input---left-shifted-address-hi) (* (shift macro/ADDRESS_HI ROFF___ADDRESS_HI ) SHIFT_FACTOR___ADDRESS_HI ) ) +(defun (keccak-limb---input---left-shifted-address-lo) (* (shift macro/ADDRESS_LO ROFF___ADDRESS_LO ) SHIFT_FACTOR___ADDRESS_LO ) ) +(defun (keccak-limb---rsult---keccak-hi) (shift xtern/AUTHORITY_RECOVERY_SUCCESS ROFF___KECCAK_HI ) ) +(defun (keccak-limb---rsult---keccak-lo) (shift xtern/AUTHORITY_RECOVERY_SUCCESS ROFF___KECCAK_LO ) ) + + +(defcomputed (keccak-extraction---IS_DATA) + (+ (prefix-selector) + (macro-selector---address-hi) + (macro-selector---address-lo) + )) + +(defcomputed (keccak-extraction---IS_RESULT) + (+ (xtern-selector---keccak-hi) + (xtern-selector---keccak-lo) + )) + +(defcomputed (keccak-extraction---USER_TXN_NUMBER) + (* (+ (keccak-extraction---IS_DATA) + (keccak-extraction---IS_RESULT)) + USER_TXN_NUMBER + )) + +(defcomputed (keccak-extraction---TUPLE_INDEX) + (* (+ (keccak-extraction---IS_DATA) + (keccak-extraction---IS_RESULT)) + TUPLE_INDEX + )) + +(defcomputed (keccak-extraction---LIMB) + (+ (* (prefix-selector) (keccak-limb---input---left-shifted-prefix) ) + (* (macro-selector---address-hi) (keccak-limb---input---left-shifted-address-hi) ) + (* (macro-selector---address-lo) (keccak-limb---input---left-shifted-address-lo) ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (xtern-selector---keccak-hi) (keccak-limb---rsult---keccak-hi) ) + (* (xtern-selector---keccak-lo) (keccak-limb---rsult---keccak-lo) ) + )) + +(defcomputed (keccak-extraction---LIMB_SIZE) + (+ (* (prefix-selector) LIMB_SIZE___DELEGATION_PREFIX ) + (* (macro-selector---address-hi) LIMB_SIZE___ADDRESS_HI ) + (* (macro-selector---address-lo) LIMB_SIZE___ADDRESS_LO ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + )) + +(defcomputed (keccak-extraction---LIMB_INDEX) + (+ (* (prefix-selector) 0 ) + (* (macro-selector---address-hi) 1 ) + (* (macro-selector---address-lo) 2 ) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (* (xtern-selector---keccak-hi) 0 ) + (* (xtern-selector---keccak-lo) 1 ) + )) + +\end{verbatim} +\end{document} diff --git a/rlp_auth/lua/extraction_for_keccak___verticalized.lua.tex b/rlp_auth/lua/extraction_for_keccak___verticalized.lua.tex new file mode 100644 index 00000000..d5491776 --- /dev/null +++ b/rlp_auth/lua/extraction_for_keccak___verticalized.lua.tex @@ -0,0 +1,77 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback ("emojifallback", { "NotoColorEmoji:mode=harf;" })} + +\setmonofont{JetBrains Mono NL Regular}[RawFeature={fallback=emojifallback}] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +██\ ██\ ██\ ██\ ██\ ██\ ██\ +██ | ██ | ██ | \__| ██ |\__| ██ | +██ | ██ | ██████\ ██████\ ██████\ ██\ ███████\ ██████\ ██ |██\ ████████\ ██████\ ███████ | +\██\ ██ |██ __██\ ██ __██\\_██ _| ██ |██ _____|\____██\ ██ |██ |\____██ |██ __██\ ██ __██ | + \██\██ / ████████ |██ | \__| ██ | ██ |██ / ███████ |██ |██ | ████ _/ ████████ |██ / ██ | + \███ / ██ ____|██ | ██ |██\ ██ |██ | ██ __██ |██ |██ | ██ _/ ██ ____|██ | ██ | + \█ / \███████\ ██ | \████ |██ |\███████\\███████ |██ |██ |████████\ \███████\ \███████ | + \_/ \_______|\__| \____/ \__| \_______|\_______|\__|\__|\________| \_______| \_______| + + + +██\ ██\ ████████\ ██████\ ██████\ ██████\ ██\ ██\ ██\ ██\ +██ | ██ |██ _____|██ __██\ ██ __██\ ██ __██\ ██ | ██ | ██ | ██ | +██ |██ / ██ | ██ / \__|██ / \__|██ / ██ |██ |██ / ███████ | ██████\ ██████\ ██████\ +█████ / █████\ ██ | ██ | ████████ |█████ / ██ __██ | \____██\\_██ _| \____██\ +██ ██< ██ __| ██ | ██ | ██ __██ |██ ██< ██ / ██ | ███████ | ██ | ███████ | +██ |\██\ ██ | ██ | ██\ ██ | ██\ ██ | ██ |██ |\██\ ██ | ██ |██ __██ | ██ |██\ ██ __██ | +██ | \██\ ████████\ \██████ |\██████ |██ | ██ |██ | \██\ \███████ |\███████ | \████ |\███████ | +\__| \__|\________| \______/ \______/ \__| \__|\__| \__| \_______| \_______| \____/ \_______| + + + +|-----------------+-------------+----------------------------+-----------+-------+---------+-----------| +| USER_TXN_NUMBER | TUPLE_INDEX | limbs | limb_size | index | is_data | is_result | +|-----------------+-------------+----------------------------+-----------+-------+:-------:+:---------:| +| n | a | | 3 | 0 | | +| n | a | | 4 | 1 | | +| n | a | | 16 | 2 | | +|-----------------+-------------+----------------------------+-----------+-------+---------+-----------| +| n | a | | | 0 | | | +| n | a | | | 1 | | | +|-----------------+-------------+----------------------------+-----------+-------+---------+-----------| +| ∅ | +| ⋮ | +| ∅ | +|-----------------+-------------+----------------------------+-----------+-------+---------| +| n | b | ' | 3 | 0 | | +| n | b | ' | 4 | 1 | | +| n | b | ' | 16 | 2 | | +|-----------------+-------------+----------------------------+-----------+-------+---------+-----------| +| n | b | ' | | 0 | | | +| n | b | ' | | 1 | | | +|-----------------+-------------+----------------------------+-----------+-------+---------+-----------| + +NOTE. Results on a line would also be ok. + + +NOTE. The column names are different in the implementation: + + +|-----------------+---+-------------------------------------| +| name in diagram | | column name in implementation | +|-----------------+---+-------------------------------------| +| USER_TXN_NUMBER | ⇒ | keccak-extraction---USER_TXN_NUMBER | +| TUPLE_INDEX | ⇒ | keccak-extraction---TUPLE_INDEX | +| is_data | ⇒ | keccak-extraction---IS_DATA | +| is_result | ⇒ | keccak-extraction---IS_RESULT | +| limb | ⇒ | keccak-extraction---LIMB | +| limb_size | ⇒ | keccak-extraction---LIMB_SIZE | +| index | ⇒ | keccak-extraction---LIMB_INDEX | +|-----------------+---+-------------------------------------| + +\end{verbatim} +\end{document} diff --git a/rlp_auth/specialized/_conditionally_set_limb.tex b/rlp_auth/specialized/_conditionally_set_limb.tex new file mode 100644 index 00000000..07217b66 --- /dev/null +++ b/rlp_auth/specialized/_conditionally_set_limb.tex @@ -0,0 +1,13 @@ +We define +\[ + \conditionallySetLimb { + anchorRow = i , + relOffset = \relof , + condition = \loc{condition\_bit} , + limb = \loc{limb} , + nBytes = \loc{number\_of\_bytes} , + } +\] +precisely as in +section~(\ref{rlp txn: specialized: limb setting: potentially set limb}) +using the column replacements from diff --git a/rlp_auth/specialized/_inputs.tex b/rlp_auth/specialized/_inputs.tex new file mode 100644 index 00000000..864e9fc0 --- /dev/null +++ b/rlp_auth/specialized/_inputs.tex @@ -0,0 +1 @@ +\subsection{Column replacements \lispTodo{}} \label{rlp auth: specialized: intro} \input{specialized/column_replacements} diff --git a/rlp_auth/specialized/column_replacements.tex b/rlp_auth/specialized/column_replacements.tex new file mode 100644 index 00000000..e44a7a1b --- /dev/null +++ b/rlp_auth/specialized/column_replacements.tex @@ -0,0 +1,74 @@ +We will use constraint systems defined originally in +the \rlpTxnMod{} module, specifically +in section~(\ref{rlptxn: specialized}). +In order to do so we have to do various columns replacements. +\[ + \renewcommand{\arraystretch}{1.3} + \begin{array}{|l|l|} + \hline + \text{\rlpTxnMod{}-columns} & \text{\rlpAuthMod{}-columns} \\ \hline\hline + \maxCt & \maxCt \\ \hline + \lc & \rlpAuthUtilsColumnLimbBit \\ \hline + \rlpTxnComputationColumnLimb & \rlpAuthUtilsColumnLimb \\ \hline + \rlpTxnComputationColumnLimbSize & \rlpAuthUtilsColumnLimbSize \\ \hline + \rlpTxnComputationColumnExoDataColumn{1} & \rlpAuthUtilsColumnExoDataColumn{1} \\ \hline + \rlpTxnComputationColumnExoDataColumn{2} & \rlpAuthUtilsColumnExoDataColumn{2} \\ \hline + \rlpTxnComputationColumnExoDataColumn{3} & \rlpAuthUtilsColumnExoDataColumn{3} \\ \hline + \rlpTxnComputationColumnExoDataColumn{4} & \rlpAuthUtilsColumnExoDataColumn{4} \\ \hline + \rlpTxnComputationColumnExoDataColumn{5} & \rlpAuthUtilsColumnExoDataColumn{5} \\ \hline + \rlpTxnComputationColumnExoDataColumn{6} & \rlpAuthUtilsColumnExoDataColumn{6} \\ \hline + \rlpTxnComputationColumnExoDataColumn{7} & \rlpAuthUtilsColumnExoDataColumn{7} \\ \hline + \rlpTxnComputationColumnExoDataColumn{8} & \rlpAuthUtilsColumnExoDataColumn{8} \\ \hline + \rlpTxnComputationColumnRlpUtilsFlag & \rlpAuthUtilsColumnRlpUtilsFlag \\ \hline + \rlpTxnComputationColumnRlpUtilsInstruction & \rlpAuthUtilsColumnRlpUtilsInstruction \\ \hline + \end{array} +\] +With the following caveats: +\begin{enumerate} + \item + we remove the \rlpTxnComputationColumnTrmFlag{} constraint from \rlpProcessAddressName{}; + well-formedness of the \address{} is a given considering + section~(\ref{rlp auth: comparisons: mandatory: address bound}); + \item + we remove any and all constraints involving the \rlpTxnMod{}-column \phaseEnd{}; + \item + we remove any and all constraints setting \maxCt{}; +\end{enumerate} +In what follows we freely re-use the following constraint systems, +switching the column names as indicated above, +and dropping constraints as explained above if necessary. +\begin{description} + \item[\underline{Limb setting constraints:}] + \begin{enumerate} + \item + \setLimbName{}, + see section~(\ref{rlp txn: specialized: limb setting: potentially set limb}) + \item + \conditionallySetLimbName{}, + see section~(\ref{rlp txn: specialized: limb setting: finalize limb}) + \item + \discardLimbName{}, + see section~(\ref{rlp txn: specialized: limb setting: dismiss limb}) + \end{enumerate} + \item[\underline{\rlpUtilsMod{}-calls:}] + \begin{enumerate} + \item + \rlpUtilsInstCallByteStringPrefixName{}, + see section~(\ref{rlp txn: specialized: utils calls: integer}) + \item + \rlpUtilsInstCallIntegerName{}, + see section~(\ref{rlp txn: specialized: utils calls: byte string prefix}) + \end{enumerate} + \item[\underline{Processing constraints:}] + \begin{enumerate} + \item + \rlpProcessIntegerName{}, + see section~(\ref{rlp txn: specialized: processing: integer}) + \item + \rlpProcessByteStringName{}, + see section~(\ref{rlp txn: specialized: processing: byte string prefix}) + \item + \rlpProcessAddressName{}, + see section~(\ref{rlp txn: specialized: processing: address}) + \end{enumerate} +\end{description} diff --git a/rlp_auth/utils/_inputs.tex b/rlp_auth/utils/_inputs.tex new file mode 100644 index 00000000..ec2386aa --- /dev/null +++ b/rlp_auth/utils/_inputs.tex @@ -0,0 +1,6 @@ +\subsection{Introduction \lispTodo{}} \label{rlp auth: rlp utils calls: intro} \input{utils/intro} +\subsection{``\locMagicByte'' prefix \lispTodo{}} \label{rlp auth: rlp utils calls: magic} \input{utils/calls/__01__magic} +\subsection{\rlp{}-prefix \lispTodo{}} \label{rlp auth: rlp utils calls: prefix} \input{utils/calls/__02__prefix} +\subsection{\rlp{}-ization of \locChainId{} \lispTodo{}} \label{rlp auth: rlp utils calls: chain id} \input{utils/calls/__03__chain_id} +\subsection{\rlp{}-ization of \locAddress{} \lispTodo{}} \label{rlp auth: rlp utils calls: address} \input{utils/calls/__04__address} +\subsection{\rlp{}-ization of \locNonce{} \lispTodo{}} \label{rlp auth: rlp utils calls: nonce} \input{utils/calls/__05__nonce} diff --git a/rlp_auth/utils/calls/__01__magic.tex b/rlp_auth/utils/calls/__01__magic.tex new file mode 100644 index 00000000..30c1e248 --- /dev/null +++ b/rlp_auth/utils/calls/__01__magic.tex @@ -0,0 +1,17 @@ +\magicRlpPrefixStandingHypothesis{} +The present subsection deals with the \col{MAGIC} prefix to the message to hash. +As such we impose +\[ + \setLimb{ + anchorRow = i , + relOffset = \roffRlpUtilsMagic , + limb = \locMagicByte \cdot 256 ^ {\llargeMO} , + nBytes = 1 , + } +\] +where +\[ + \locMagicByte + \define + \locMagicByteValue +\] diff --git a/rlp_auth/utils/calls/__02__prefix.tex b/rlp_auth/utils/calls/__02__prefix.tex new file mode 100644 index 00000000..de2f5e09 --- /dev/null +++ b/rlp_auth/utils/calls/__02__prefix.tex @@ -0,0 +1,33 @@ +\rlpPrefixStandingHypothesis{} +We impose +\[ + \rlpProcessByteString { + anchorRow = i , + relOffset = \roffRlpUtilsPrefix , + byteStringLength = \rlpAuthUtilsColumnSizeCountdown _{i} , + firstByte = \nothing , + isList = \true , + mustBeNontrivial = \true , + } +\] +\saNote{} +The byte string whose \rlp{} prefix the above is tasked with computing contains +at least $1 + (1 + \addressSize) + 1 = 23$ bytes +and at most $(1 + \evmWordSize) + (1 + \addressSize) + (1 + 8) = 63$ bytes. +\[ + \underbrace{ + \overbrace{\rlp\Big( \locChainId \Big)} ^ {\text{1 to }(1 + \evmWordSize)\text{ bytes}} \cdot + \overbrace{\rlp\Big( \locAddress \Big)} ^ {(1 + \addressSize) \text{ bytes}} \cdot + \overbrace{\rlp\Big( \locNonce \Big)} ^ {\text{1 to }(1 + 8)\text{ bytes}} + }_\text{23 to 63 bytes} + \in + \mathbb{B} ^ * +\] +Its leading byte (which only matters if the byte string has length 1) +is therefore irrelevant in computing its prefix and we can not explicitly set it ($\nothing$). + +\saNote{} +The value of $\rlpAuthUtilsColumnSizeCountdown _{i}$ +is the right one as it has already been decremented +by the current $\rlpAuthUtilsColumnLimbSize _{i}$, +which is the size of the byte prefix of the above byte string. diff --git a/rlp_auth/utils/calls/__03__chain_id.tex b/rlp_auth/utils/calls/__03__chain_id.tex new file mode 100644 index 00000000..b02316c2 --- /dev/null +++ b/rlp_auth/utils/calls/__03__chain_id.tex @@ -0,0 +1,11 @@ +\tupleChainIdStandingHypothesis +We impose +\[ + \rlpProcessInteger { + anchorRow = i , + relOffset = \roffRlpUtilsChainId , + integerHi = \locChainIdHi , + integerLo = \locChainIdLo , + endOfPhase = \nothing , + } +\] diff --git a/rlp_auth/utils/calls/__04__address.tex b/rlp_auth/utils/calls/__04__address.tex new file mode 100644 index 00000000..81bb9604 --- /dev/null +++ b/rlp_auth/utils/calls/__04__address.tex @@ -0,0 +1,10 @@ +\tupleAddressStandingHypothesis +We impose +\[ + \rlpProcessAddress { + anchorRow = i , + relOffset = \roffRlpUtilsAddress , + addressHi = \locAddressHi , + addressLo = \locAddressLo , + } +\] diff --git a/rlp_auth/utils/calls/__05__nonce.tex b/rlp_auth/utils/calls/__05__nonce.tex new file mode 100644 index 00000000..7b99b854 --- /dev/null +++ b/rlp_auth/utils/calls/__05__nonce.tex @@ -0,0 +1,11 @@ +\tupleNonceStandingHypothesis{} +We impose +\[ + \rlpProcessInteger { + anchorRow = i , + relOffset = \roffRlpUtilsNonce , + integerHi = 0 , + integerLo = \locNonce , + endOfPhase = \nothing , + } +\] diff --git a/rlp_auth/utils/intro.tex b/rlp_auth/utils/intro.tex new file mode 100644 index 00000000..9b5410f9 --- /dev/null +++ b/rlp_auth/utils/intro.tex @@ -0,0 +1,4 @@ +The present section describes the process of constructing the following string +\[ + \locMagic \cdot \rlp\Big(\big[\,\locChainId, \, \locAddress, \, \locNonce \,]\Big) +\] diff --git a/rlp_txn/columns/shared.tex b/rlp_txn/columns/shared.tex index 712270e8..6bf5c028 100644 --- a/rlp_txn/columns/shared.tex +++ b/rlp_txn/columns/shared.tex @@ -19,14 +19,14 @@ \item $\indexx$: index of the current limb within the current string of $\locLxTilde(\locTransaction)$; starts at $0$ when starting a new transaction and increments by 1 when $\lc$ and $\lx$ are one; - \item $\ltByteSizeCountDown$: + \item $\ltByteSizeCountdown$: number of bytes of $L_{\mathrm{T}}(\locTransaction)$ of the current transaction ($\locTransaction$) \emph{minus} a certain number of bytes, - see section~(\ref{rlp txn v2: phase constraints: rlp prefix}); + see section~(\ref{rlp txn: phase constraints: rlp prefix}); used in \phaseRlpPrefix{} to compute the global \rlp{} prefix of $L_{\mathrm{T}}(\locTransaction)$; in futher phases this column simply decreases by $\rlpTxnComputationColumnLimbSize$ when $\lc$ and $\lt$ are one; constrained to vanish at the end of the transaction; - \item $\lxByteSizeCountDown$: - same interpretation as \ltByteSizeCountDown{} but for $L_{\mathrm{X}}(\locTransaction)$ + \item $\lxByteSizeCountdown$: + same interpretation as \ltByteSizeCountdown{} but for $L_{\mathrm{X}}(\locTransaction)$ (and with $\lt$ swapped for $\lx$); \item \toHashByProver{}: binary column; equals $\lc \cdot \lx$; is a selector to extract data for the prover; @@ -101,7 +101,7 @@ turns on precisely for deployment transactions; \end{enumerate} The following are \textbf{counter-constant}, \textbf{binary} columns used in particular in the \rlp{}-ization of \textbf{access lists}, -see section~(\ref{rlp txn v2: phase constraints: access list: approach}). +see section~(\ref{rlp txn: phase constraints: access list: approach}). \begin{multicols}{2} \begin{enumerate}[resume] \setcounter{enumi}{33} diff --git a/rlp_txn/columns/transaction.tex b/rlp_txn/columns/transaction.tex index 58872b6b..bc9c32fa 100644 --- a/rlp_txn/columns/transaction.tex +++ b/rlp_txn/columns/transaction.tex @@ -59,7 +59,7 @@ the number of nonzero bytes in the transaction's payload \textbf{p}; \end{enumerate} We recall the definition of the payload \textbf{p} of a transaction $T$ -in section~(\ref{rlp txn v2: phase constraints: payload: payload size analysis: definition of payload in terms of transaction fields}). +in section~(\ref{rlp txn: phase constraints: payload: payload size analysis: definition of payload in terms of transaction fields}). \begin{enumerate}[resume] \item \markAsJustifiedHere{} diff --git a/rlp_txn/generalities/_inputs.tex b/rlp_txn/generalities/_inputs.tex index 29ecb6a8..603b774d 100644 --- a/rlp_txn/generalities/_inputs.tex +++ b/rlp_txn/generalities/_inputs.tex @@ -1,18 +1,18 @@ -\subsection{Binarities} \label{rlp txn v2: generalities: binarities} \input{generalities/binarities} -\subsection{Constancies} \label{rlp txn v2: generalities: constancies} \input{generalities/constancies} -\subsection{\userTransactionNumber{} constraints} \label{rlp txn v2: generalities: user transaction number} \input{generalities/user_transaction_number} -\subsection{\locPhaseFlagSum{} constraints} \label{rlp txn v2: generalities: phase flag sum} \input{generalities/phase_flag_sum} -\subsection{\locPerspFlagSum{} and perspectives} \label{rlp txn v2: generalities: perspectives} \input{generalities/perspectives} -\subsection{\phaseEnd{} constraints} \label{rlp txn v2: generalities: PHASE_END constraints} \input{generalities/phase_end} -\subsection{\ct{} and \maxCt{} constraints} \label{rlp txn v2: generalities: ct and ct_max} \input{generalities/ct_and_ct_max} -\subsection{\typeSomethingTx{k} constraints} \label{rlp txn v2: generalities: transaction decoding} \input{generalities/transaction_decoding} -\subsection{Transaction type \rlp{} components} \label{rlp txn v2: generalities: transaction type rlp components} \input{generalities/transaction_type_rlp_components} -\subsection{Transaction type phase transitions} \label{rlp txn v2: generalities: admissible rlp component flags} \input{generalities/transaction_type_phase_transitions} -\subsection{\lc{}, \lx{} and \lt{} constraints} \label{rlp txn v2: generalities: lc lt and lx constraints} \input{generalities/lt_lx_lc_bits} -\subsection{\indext{} and \indexx{} constraints} \label{rlp txn v2: generalities: indices and limb constructed} \input{generalities/indices_and_limb_constructed} -\subsection{\ltByteSizeCountDown{} and \lxByteSizeCountDown{} constraints} \label{rlp txn v2: generalities: rlp lt and lx byte size constraints} \input{generalities/lt_lx_byte_size_countdown} -\subsection{Finalization constraints} \label{rlp txn v2: generalities: finalization} \input{generalities/finalization} -\subsection{Constraints for miscellaneous transaction columns} \label{rlp txn v2: generalities: miscellaneous txn columns} \input{generalities/miscellaneous_transaction_columns} -\subsection{\rlpTxnComputationColumnCounterConstantAuxiliaryData{k} constraints} \label{rlp txn v2: generalities: TMP k column generalities} \input{generalities/aux_k} -\subsection{\rlpTxnSharedColumnRequiresEvmExecution{} constraints} \label{rlp txn v2: generalities: requires evm execution column} \input{generalities/requires_evm_execution} +\subsection{Binarities} \label{rlp txn: generalities: binarities} \input{generalities/binarities} +\subsection{Constancies} \label{rlp txn: generalities: constancies} \input{generalities/constancies} +\subsection{\userTransactionNumber{} constraints} \label{rlp txn: generalities: user transaction number} \input{generalities/user_transaction_number} +\subsection{\locPhaseFlagSum{} constraints} \label{rlp txn: generalities: phase flag sum} \input{generalities/phase_flag_sum} +\subsection{\locPerspFlagSum{} and perspectives} \label{rlp txn: generalities: perspectives} \input{generalities/perspectives} +\subsection{\phaseEnd{} constraints} \label{rlp txn: generalities: PHASE_END constraints} \input{generalities/phase_end} +\subsection{\ct{} and \maxCt{} constraints} \label{rlp txn: generalities: ct and ct_max} \input{generalities/ct_and_ct_max} +\subsection{\typeSomethingTx{k} constraints} \label{rlp txn: generalities: transaction decoding} \input{generalities/transaction_decoding} +\subsection{Transaction type \rlp{} components} \label{rlp txn: generalities: transaction type rlp components} \input{generalities/transaction_type_rlp_components} +\subsection{Transaction type phase transitions} \label{rlp txn: generalities: admissible rlp component flags} \input{generalities/transaction_type_phase_transitions} +\subsection{\lc{}, \lx{} and \lt{} constraints} \label{rlp txn: generalities: lc lt and lx constraints} \input{generalities/lt_lx_lc_bits} +\subsection{\indext{} and \indexx{} constraints} \label{rlp txn: generalities: indices and limb constructed} \input{generalities/indices_and_limb_constructed} +\subsection{\ltByteSizeCountdown{} and \lxByteSizeCountdown{} constraints} \label{rlp txn: generalities: rlp lt and lx byte size constraints} \input{generalities/lt_lx_byte_size_countdown} +\subsection{Finalization constraints} \label{rlp txn: generalities: finalization} \input{generalities/finalization} +\subsection{Constraints for miscellaneous transaction columns} \label{rlp txn: generalities: miscellaneous txn columns} \input{generalities/miscellaneous_transaction_columns} +\subsection{\rlpTxnComputationColumnCounterConstantAuxiliaryData{k} constraints} \label{rlp txn: generalities: TMP k column generalities} \input{generalities/aux_k} +\subsection{\rlpTxnSharedColumnRequiresEvmExecution{} constraints} \label{rlp txn: generalities: requires evm execution column} \input{generalities/requires_evm_execution} diff --git a/rlp_txn/generalities/lt_lx_byte_size_countdown.tex b/rlp_txn/generalities/lt_lx_byte_size_countdown.tex index f3cfaf3b..b8aa24e6 100644 --- a/rlp_txn/generalities/lt_lx_byte_size_countdown.tex +++ b/rlp_txn/generalities/lt_lx_byte_size_countdown.tex @@ -1,18 +1,18 @@ We impose \begin{description} \item[\underline{\underline{Initialization:}}] - both \ltByteSizeCountDown{} and \lxByteSizeCountDown{} are \textbf{implicitly} initialized, - see section~(\ref{rlp txn v2: phase constraints: rlp prefix}), + both \ltByteSizeCountdown{} and \lxByteSizeCountdown{} are \textbf{implicitly} initialized, + see section~(\ref{rlp txn: phase constraints: rlp prefix}), during the ``$\phaseRlpPrefix _{i} = \true$'' rows. \item[\underline{\underline{Updates:}}] \If $\phaseRlpPrefix _{i} = \false$ \Then \begin{enumerate} - \item $\ltByteSizeCountDown _{i} = \ltByteSizeCountDown _{i - 1} - \lc _{i} \cdot \lt _{i} \cdot \rlpTxnComputationColumnLimbSize _{i}$ - \item $\lxByteSizeCountDown _{i} = \lxByteSizeCountDown _{i - 1} - \lc _{i} \cdot \lx _{i} \cdot \rlpTxnComputationColumnLimbSize _{i}$ + \item $\ltByteSizeCountdown _{i} = \ltByteSizeCountdown _{i - 1} - \lc _{i} \cdot \lt _{i} \cdot \rlpTxnComputationColumnLimbSize _{i}$ + \item $\lxByteSizeCountdown _{i} = \lxByteSizeCountdown _{i - 1} - \lc _{i} \cdot \lx _{i} \cdot \rlpTxnComputationColumnLimbSize _{i}$ \end{enumerate} \saNote{} Recall that by - constraint~(\ref{rlp txn v2: generalities: lc lt and lx constraints: lc vanishes outside of computation rows}), + constraint~(\ref{rlp txn: generalities: lc lt and lx constraints: lc vanishes outside of computation rows}), $\lc$ vanishes outside of \textbf{computation-rows}. This enforces that the above ``update constraints'' only apply along \textbf{computation-rows}, @@ -22,8 +22,8 @@ \item[\underline{\underline{Finalization:}}] \If $\phaseS _{i} = \true$ \et $\phaseEnd _{i} = \true$ \Then \begin{enumerate} - \item $\ltByteSizeCountDown _{i} = 0$ - \item $\lxByteSizeCountDown _{i} = 0$ + \item $\ltByteSizeCountdown _{i} = 0$ + \item $\lxByteSizeCountdown _{i} = 0$ \end{enumerate} \item[\underline{\underline{\toHashByProver{} definition:}}] $\toHashByProver _{i} = \lc _{i} \cdot \lx _{i}$ diff --git a/rlp_txn/generalities/lt_lx_lc_bits.tex b/rlp_txn/generalities/lt_lx_lc_bits.tex index 13ca7097..a8bf69d5 100644 --- a/rlp_txn/generalities/lt_lx_lc_bits.tex +++ b/rlp_txn/generalities/lt_lx_lc_bits.tex @@ -3,7 +3,7 @@ \item most phase flags explicitly dictate whether to set \lt{} (resp. \lx{}) or not; some don't, and setting \lt{} (resp. \lx{}) is a more refined process; - see section~(\ref{rlp txn v2: phase constraints: definitions: table}) + see section~(\ref{rlp txn: phase constraints: definitions: table}) for more details; counter-constancy perpetuates this initial choice for the appropriate duration; \item @@ -66,7 +66,7 @@ \] \saNote{} Clearly the first constraint could be replaced with ``$\lt _{i} = \true$''. - \item \label{rlp txn v2: generalities: lc lt and lx constraints: lc vanishes outside of computation rows} + \item \label{rlp txn: generalities: lc lt and lx constraints: lc vanishes outside of computation rows} \If $\isCmp _{i} = 0$ \Then $\lc _{i} = 0$ \item \If $\locPhaseFlagSum _{i} = 0$ \Then \[ @@ -80,6 +80,6 @@ Special constraints apply to the \phaseRlpPrefix{} and \phaseBeta{} phases, -see section~(\ref{rlp txn v2: phase constraints: rlp prefix}) -and section~(\ref{rlp txn v2: phase constraints: beta}) +see section~(\ref{rlp txn: phase constraints: rlp prefix}) +and section~(\ref{rlp txn: phase constraints: beta}) respectively. diff --git a/rlp_txn/generalities/miscellaneous_transaction_columns.tex b/rlp_txn/generalities/miscellaneous_transaction_columns.tex index 07983215..b9b4cac2 100644 --- a/rlp_txn/generalities/miscellaneous_transaction_columns.tex +++ b/rlp_txn/generalities/miscellaneous_transaction_columns.tex @@ -7,5 +7,5 @@ \item \If $\isTxn _{i} = 1$ \et $\rlpTxnTransactionColumnChainId _{i} = 0$ \Then $\rlpTxnCommonColumnReplayProtection _{i} = 0$ \item \If $\isTxn _{i} = 1$ \et $\typeZeroTx _{i} = 0$ \Then $\rlpTxnCommonColumnReplayProtection _{i} = 1$ \end{enumerate} -\saNote{} \label{rlp txn v2: generalities: transaction decoding: non legacy transaction can't be chainless} +\saNote{} \label{rlp txn: generalities: transaction decoding: non legacy transaction can't be chainless} The above imposes that only legacy transactions can be chainless. diff --git a/rlp_txn/generalities/perspectives.tex b/rlp_txn/generalities/perspectives.tex index 42647726..a5b66595 100644 --- a/rlp_txn/generalities/perspectives.tex +++ b/rlp_txn/generalities/perspectives.tex @@ -31,20 +31,20 @@ \begin{enumerate} \item $\locPerspFlagSum _{i} = \locPhaseFlagSum _{i}$ \item $\locAboutToEnterNewPhase _{i} = \isTxn _{i + 1}$ - \item \label{rlp txn v2: generalities: perspectives: every transaction row is followed by a computation row} \If $\isTxn _{i} = 1$ \Then $\isCmp _{i + 1} = 1$ + \item \label{rlp txn: generalities: perspectives: every transaction row is followed by a computation row} \If $\isTxn _{i} = 1$ \Then $\isCmp _{i + 1} = 1$ \item \If $\locPhaseFlagSum _{i} = 1$ \Then \[ \locAboutToEnterNewPhase _{i} = \locAboutToExitPhase _{i} \quad (\sanityCheck) \] \end{enumerate} -\saNote{} \label{rlp txn v2: generalities: heartbeat: the perspective flags are binary exclusive} +\saNote{} \label{rlp txn: generalities: heartbeat: the perspective flags are binary exclusive} Given the \emph{empirical binarity} of \locPhaseFlagSum{}, -see note~(\ref{rlp txn v2: generalities: phase flag sum: phase flag sum is binary}), +see note~(\ref{rlp txn: generalities: phase flag sum: phase flag sum is binary}), the above implies that $\isTxn$ and $\isCmp$ are (binary) exclusive. -\saNote{} \label{rlp txn v2: generalities: perspectives: perspective columns are fully constrained and every transaction row is followed by at least one computation row} +\saNote{} \label{rlp txn: generalities: perspectives: perspective columns are fully constrained and every transaction row is followed by at least one computation row} The above constraints \emph{completely} constrain both $\isTxn$ and $\isCmp$. -Furthermore, constraint (\ref{rlp txn v2: generalities: perspectives: every transaction row is followed by a computation row}) +Furthermore, constraint (\ref{rlp txn: generalities: perspectives: every transaction row is followed by a computation row}) imposes that \emph{each and every} phase starts with a \textbf{single} $\isTxn$-row followed by at least one $\isCmp$-row. diff --git a/rlp_txn/generalities/phase_end.tex b/rlp_txn/generalities/phase_end.tex index 6ec138d8..70ec5366 100644 --- a/rlp_txn/generalities/phase_end.tex +++ b/rlp_txn/generalities/phase_end.tex @@ -26,11 +26,11 @@ \begin{enumerate} \item $\locAboutToExitPhase _{i}$ is binary \quad (\sanityCheck) - \item \label{rlp txn v2: generalities: PHASE_END constraints} + \item \label{rlp txn: generalities: PHASE_END constraints} $\phaseEnd_{i} = \locAboutToExitPhase _{i}$ \end{enumerate} \saNote{} -The above constraint~(\ref{rlp txn v2: generalities: PHASE_END constraints}) +The above constraint~(\ref{rlp txn: generalities: PHASE_END constraints}) must be understood as follows: rather than \textbf{constraining} \phaseEnd{}, the constraints will often times \textbf{set} the value of \phaseEnd{} and thereby force a phase transition upon the module. diff --git a/rlp_txn/generalities/phase_flag_sum.tex b/rlp_txn/generalities/phase_flag_sum.tex index d6890154..9f6fbd32 100644 --- a/rlp_txn/generalities/phase_flag_sum.tex +++ b/rlp_txn/generalities/phase_flag_sum.tex @@ -24,13 +24,13 @@ \item \If $\userTransactionNumber _{i} = 0$ \Then $\locPhaseFlagSum _{i} = 0$ \item \If $\userTransactionNumber _{i} \neq 0$ \Then $\locPhaseFlagSum _{i} = 1$ \end{enumerate} -\saNote{} \label{rlp txn v2: generalities: phase flag sum: phase flag sum is binary} +\saNote{} \label{rlp txn: generalities: phase flag sum: phase flag sum is binary} The above makes \locPhaseFlagSum{} \emph{empirically} binary. -\saNote{} \label{rlp txn v2: generalities: phase flag sum: flag sums are binary exclusive} +\saNote{} \label{rlp txn: generalities: phase flag sum: flag sums are binary exclusive} The above implies that the various ``phase flags'' are (binary) exclusive. -\saNote{} \label{rlp txn v2: generalities: phase flag sum: padding rows and non padding rows} +\saNote{} \label{rlp txn: generalities: phase flag sum: padding rows and non padding rows} As per usual we label rows (with row index $i$) as \textbf{padding-rows} if they satisfy $\locPhaseFlagSum _{i} \equiv 1$ and as \textbf{non-padding-rows} if they satisfy $\locPhaseFlagSum _{i} \equiv 0$. diff --git a/rlp_txn/generalities/transaction_decoding.tex b/rlp_txn/generalities/transaction_decoding.tex index e048a9b8..365032a6 100644 --- a/rlp_txn/generalities/transaction_decoding.tex +++ b/rlp_txn/generalities/transaction_decoding.tex @@ -38,6 +38,6 @@ % \item $\lc _{i} = 0$ (\sanityCheck) % \end{enumerate} \end{enumerate} -\saNote{} \label{rlp txn v2: generalities: transaction decoding: flag exclusivity} +\saNote{} \label{rlp txn: generalities: transaction decoding: flag exclusivity} The above implicitly imposes flag exclusivity on the ``transaction type flags.'' It further imposes that every transaction raises precisely one of the ``transaction type flags.'' diff --git a/rlp_txn/generalities/transaction_type_rlp_components.tex b/rlp_txn/generalities/transaction_type_rlp_components.tex index def89d70..04397e07 100644 --- a/rlp_txn/generalities/transaction_type_rlp_components.tex +++ b/rlp_txn/generalities/transaction_type_rlp_components.tex @@ -56,6 +56,6 @@ \item \If $\typeOneTx _{i} = 1$ \Then $\locRlpComponentsTypeOne _{i} = 1$ \quad (\sanityCheck) \item \If $\typeTwoTx _{i} = 1$ \Then $\locRlpComponentsTypeTwo _{i} = 1$ \quad (\sanityCheck) \end{enumerate} -\saNote{} \label{rlp txn v2: generalities: transaction type rlp components: refinement of flag sum} +\saNote{} \label{rlp txn: generalities: transaction type rlp components: refinement of flag sum} The above refines -constraint~(\ref{rlp txn v2: generalities: phase flag sum}). +constraint~(\ref{rlp txn: generalities: phase flag sum}). diff --git a/rlp_txn/lookups/rlptxn_into_hub.tex b/rlp_txn/lookups/rlptxn_into_hub.tex index 47bad1b4..cfbd4326 100644 --- a/rlp_txn/lookups/rlptxn_into_hub.tex +++ b/rlp_txn/lookups/rlptxn_into_hub.tex @@ -35,7 +35,7 @@ \end{multicols} \saNote{} The above uses shorthands introduced - in section~(\ref{rlp txn v2: phase constraints: access list: countdowns: shorthands}). + in section~(\ref{rlp txn: phase constraints: access list: countdowns: shorthands}). \item[Target columns:] --- \begin{multicols}{2} \begin{enumerate} diff --git a/rlp_txn/phase_constraints/_inputs.tex b/rlp_txn/phase_constraints/_inputs.tex index 133974ce..1d16d008 100644 --- a/rlp_txn/phase_constraints/_inputs.tex +++ b/rlp_txn/phase_constraints/_inputs.tex @@ -1,9 +1,9 @@ \def\localSectionTitle {\rlp{}-ization of the integers \texttt{chainId}, \texttt{nonce}, \texttt{gasPrice}, \texttt{maxProrityFeePerGas}, \texttt{maxFeePerGas}, \texttt{gasLimit}, \texttt{value}, \texttt{yParity}, \texttt{r} and \texttt{s} } -\subsection{Phase definitions} \label{rlp txn v2: phase constraints: definitions} \input{phase_constraints/definition} -\subsection{Global \rlp{} prefix (\phaseRlpPrefix)} \label{rlp txn v2: phase constraints: rlp prefix} \input{phase_constraints/rlp_prefix} -\subsection{\localSectionTitle{} (\phaseChainId{}, \dots, \phaseY{}, \phaseR{} and \phaseS{})} \label{rlp txn v2: phase constraints: integers} \input{phase_constraints/int} -\subsection{\rlp{}-ization of \texttt{to} (\phaseTo)} \label{rlp txn v2: phase constraints: to address} \input{phase_constraints/to_address} -\subsection{\rlp{}-ization of \texttt{data} (\phaseData)} \label{rlp txn v2: phase constraints: payload} \input{phase_constraints/data/_inputs} -\subsection{\rlp{}-ization of \texttt{access list} (\phaseAccessList)} \label{rlp txn v2: phase constraints: access list} \input{phase_constraints/access_list/_inputs} -\subsection{\rlp{}-ization of \texttt{beta} (\phaseBeta)} \label{rlp txn v2: phase constraints: beta} \input{phase_constraints/beta} +\subsection{Phase definitions} \label{rlp txn: phase constraints: definitions} \input{phase_constraints/definition} +\subsection{Global \rlp{} prefix (\phaseRlpPrefix)} \label{rlp txn: phase constraints: rlp prefix} \input{phase_constraints/rlp_prefix} +\subsection{\localSectionTitle{} (\phaseChainId{}, \dots, \phaseY{}, \phaseR{} and \phaseS{})} \label{rlp txn: phase constraints: integers} \input{phase_constraints/int} +\subsection{\rlp{}-ization of \texttt{to} (\phaseTo)} \label{rlp txn: phase constraints: to address} \input{phase_constraints/to_address} +\subsection{\rlp{}-ization of \texttt{data} (\phaseData)} \label{rlp txn: phase constraints: payload} \input{phase_constraints/data/_inputs} +\subsection{\rlp{}-ization of \texttt{access list} (\phaseAccessList)} \label{rlp txn: phase constraints: access list} \input{phase_constraints/access_list/_inputs} +\subsection{\rlp{}-ization of \texttt{beta} (\phaseBeta)} \label{rlp txn: phase constraints: beta} \input{phase_constraints/beta} diff --git a/rlp_txn/phase_constraints/access_list/_inputs.tex b/rlp_txn/phase_constraints/access_list/_inputs.tex index 03d476c9..07d3ad9b 100644 --- a/rlp_txn/phase_constraints/access_list/_inputs.tex +++ b/rlp_txn/phase_constraints/access_list/_inputs.tex @@ -1,7 +1,7 @@ -\subsubsection{Approach } \label{rlp txn v2: phase constraints: access list: approach} \input{phase_constraints/access_list/approach} -\subsubsection{Shorthands } \label{rlp txn v2: phase constraints: access list: shorthands} \input{phase_constraints/access_list/shorthands} -\subsubsection{Access list bits } \label{rlp txn v2: phase constraints: access list: access list bits} \input{phase_constraints/access_list/access_list_bits} -\subsubsection{Legal bit transitions } \label{rlp txn v2: phase constraints: access list: legal transitions} \input{phase_constraints/access_list/legal_transitions} -\subsubsection{Countdown constraints } \label{rlp txn v2: phase constraints: access list: countdowns} \input{phase_constraints/access_list/countdowns/_inputs} -\subsubsection{Subphases of processing } \label{rlp txn v2: phase constraints: access list: access list prefix} \input{phase_constraints/access_list/subphases/_inputs} -% \subsubsection{Constraints } \label{rlp txn v2: phase constraints: access list: constraints} \input{phase_constraints/access_list/constraints} +\subsubsection{Approach } \label{rlp txn: phase constraints: access list: approach} \input{phase_constraints/access_list/approach} +\subsubsection{Shorthands } \label{rlp txn: phase constraints: access list: shorthands} \input{phase_constraints/access_list/shorthands} +\subsubsection{Access list bits } \label{rlp txn: phase constraints: access list: access list bits} \input{phase_constraints/access_list/access_list_bits} +\subsubsection{Legal bit transitions } \label{rlp txn: phase constraints: access list: legal transitions} \input{phase_constraints/access_list/legal_transitions} +\subsubsection{Countdown constraints } \label{rlp txn: phase constraints: access list: countdowns} \input{phase_constraints/access_list/countdowns/_inputs} +\subsubsection{Subphases of processing } \label{rlp txn: phase constraints: access list: access list prefix} \input{phase_constraints/access_list/subphases/_inputs} +% \subsubsection{Constraints } \label{rlp txn: phase constraints: access list: constraints} \input{phase_constraints/access_list/constraints} diff --git a/rlp_txn/phase_constraints/access_list/access_list_bits.tex b/rlp_txn/phase_constraints/access_list/access_list_bits.tex index 7dbc8af9..0fe0572e 100644 --- a/rlp_txn/phase_constraints/access_list/access_list_bits.tex +++ b/rlp_txn/phase_constraints/access_list/access_list_bits.tex @@ -14,7 +14,7 @@ \end{enumerate} \end{multicols} are required to be \textbf{binary} (\sanityCheck), - see section~(\ref{rlp txn v2: generalities: binarities}), + see section~(\ref{rlp txn: generalities: binarities}), and \textbf{counter-constant}. \item[\underline{Flag exclusivities:}] we impose diff --git a/rlp_txn/phase_constraints/access_list/approach.tex b/rlp_txn/phase_constraints/access_list/approach.tex index 495fa2f7..10ee721b 100644 --- a/rlp_txn/phase_constraints/access_list/approach.tex +++ b/rlp_txn/phase_constraints/access_list/approach.tex @@ -1,6 +1,6 @@ The present section deals with the \rlp{}-ization of access lists. The transaction types which feature access lists can be read off of -table~(\ref{rlp txn v2: phase constraints: definitions: table}). +table~(\ref{rlp txn: phase constraints: definitions: table}). Recall that, if applicable, the access list $T_\textbf{A}$ of a transaction $T$ is a tuple \[ \left\{ \begin{array}{lcl} diff --git a/rlp_txn/phase_constraints/access_list/countdowns/_inputs.tex b/rlp_txn/phase_constraints/access_list/countdowns/_inputs.tex index 84ed6fb8..ca40ad4b 100644 --- a/rlp_txn/phase_constraints/access_list/countdowns/_inputs.tex +++ b/rlp_txn/phase_constraints/access_list/countdowns/_inputs.tex @@ -1,7 +1,7 @@ -\subsubsubsection{Shorthands } \label{rlp txn v2: phase constraints: access list: countdowns: shorthands} \input{phase_constraints/access_list/countdowns/shorthands} -\subsubsubsection{\loc{address} constancy conditions } \label{rlp txn v2: phase constraints: access list: countdowns: address constancy conditions} \input{phase_constraints/access_list/countdowns/address_constancy} -\subsubsubsection{\locAccessListItemCountdown {} constraints } \label{rlp txn v2: phase constraints: access list: countdowns: addresses} \input{phase_constraints/access_list/countdowns/addresses} -\subsubsubsection{\locStoragePrewarmingCountdown {} constraints } \label{rlp txn v2: phase constraints: access list: countdowns: storage keys} \input{phase_constraints/access_list/countdowns/storage_keys} -\subsubsubsection{\locStorageKeyListCountdown {} constraints } \label{rlp txn v2: phase constraints: access list: countdowns: storage key list} \input{phase_constraints/access_list/countdowns/storage_key_list} -\subsubsubsection{\locAccessListLengthCountdown {} constraints } \label{rlp txn v2: phase constraints: access list: countdowns: access list RLP length} \input{phase_constraints/access_list/countdowns/access_list_RLP_length} -\subsubsubsection{\locAccessListItemRlpLengthCountdown {} constraints } \label{rlp txn v2: phase constraints: access list: countdowns: access list item RLP length} \input{phase_constraints/access_list/countdowns/access_list_item_RLP_length} +\subsubsubsection{Shorthands } \label{rlp txn: phase constraints: access list: countdowns: shorthands} \input{phase_constraints/access_list/countdowns/shorthands} +\subsubsubsection{\loc{address} constancy conditions } \label{rlp txn: phase constraints: access list: countdowns: address constancy conditions} \input{phase_constraints/access_list/countdowns/address_constancy} +\subsubsubsection{\locAccessListItemCountdown {} constraints } \label{rlp txn: phase constraints: access list: countdowns: addresses} \input{phase_constraints/access_list/countdowns/addresses} +\subsubsubsection{\locStoragePrewarmingCountdown {} constraints } \label{rlp txn: phase constraints: access list: countdowns: storage keys} \input{phase_constraints/access_list/countdowns/storage_keys} +\subsubsubsection{\locStorageKeyListCountdown {} constraints } \label{rlp txn: phase constraints: access list: countdowns: storage key list} \input{phase_constraints/access_list/countdowns/storage_key_list} +\subsubsubsection{\locAccessListLengthCountdown {} constraints } \label{rlp txn: phase constraints: access list: countdowns: access list RLP length} \input{phase_constraints/access_list/countdowns/access_list_RLP_length} +\subsubsubsection{\locAccessListItemRlpLengthCountdown {} constraints } \label{rlp txn: phase constraints: access list: countdowns: access list item RLP length} \input{phase_constraints/access_list/countdowns/access_list_item_RLP_length} diff --git a/rlp_txn/phase_constraints/access_list/countdowns/access_list_RLP_length.tex b/rlp_txn/phase_constraints/access_list/countdowns/access_list_RLP_length.tex index 70500093..d167cb0c 100644 --- a/rlp_txn/phase_constraints/access_list/countdowns/access_list_RLP_length.tex +++ b/rlp_txn/phase_constraints/access_list/countdowns/access_list_RLP_length.tex @@ -34,7 +34,7 @@ \locAccessListLengthCountdown _{i} = \locAccessListLengthCountdown _{i - 1} - \lc _{i} \cdot \rlpTxnComputationColumnLimbSize _{i} \] \end{description} -\saNote{} \label{rlp txn v2: phase constraints: access list: countdowns: non counter constancy of access list RLP length} +\saNote{} \label{rlp txn: phase constraints: access list: countdowns: non counter constancy of access list RLP length} The \locAccessListLengthCountdown{} and \locAccessListItemRlpLengthCountdown{} updates may happen mid-counter-cycle. diff --git a/rlp_txn/phase_constraints/access_list/countdowns/access_list_item_RLP_length.tex b/rlp_txn/phase_constraints/access_list/countdowns/access_list_item_RLP_length.tex index 45e81666..c318c0ef 100644 --- a/rlp_txn/phase_constraints/access_list/countdowns/access_list_item_RLP_length.tex +++ b/rlp_txn/phase_constraints/access_list/countdowns/access_list_item_RLP_length.tex @@ -36,7 +36,7 @@ ~ \Then \locAccessListItemRlpLengthCountdown _{i} = 0 \] \end{description} -\saNote{} \label{rlp txn v2: phase constraints: access list: countdowns: non counter constancy of access list item RLP length} +\saNote{} \label{rlp txn: phase constraints: access list: countdowns: non counter constancy of access list item RLP length} The \locAccessListLengthCountdown{} and \locAccessListItemRlpLengthCountdown{} updates may happen mid-counter-cycle. diff --git a/rlp_txn/phase_constraints/access_list/countdowns/addresses.tex b/rlp_txn/phase_constraints/access_list/countdowns/addresses.tex index d6683110..cc985003 100644 --- a/rlp_txn/phase_constraints/access_list/countdowns/addresses.tex +++ b/rlp_txn/phase_constraints/access_list/countdowns/addresses.tex @@ -17,8 +17,8 @@ is counter-constant (\sanityCheck) by virtue of its definition, - see section~(\ref{rlp txn v2: phase constraints: access list: countdowns: shorthands}), - and section~(\ref{rlp txn v2: generalities: TMP k column generalities}) + see section~(\ref{rlp txn: phase constraints: access list: countdowns: shorthands}), + and section~(\ref{rlp txn: generalities: TMP k column generalities}) \item[\underline{\underline{Initialization:}}] \If $\locAccessListPrefix _{i} = \true$ \Then we impose diff --git a/rlp_txn/phase_constraints/access_list/countdowns/shorthands.tex b/rlp_txn/phase_constraints/access_list/countdowns/shorthands.tex index 6ed4efd7..74c53f34 100644 --- a/rlp_txn/phase_constraints/access_list/countdowns/shorthands.tex +++ b/rlp_txn/phase_constraints/access_list/countdowns/shorthands.tex @@ -20,8 +20,8 @@ \locAccessListItemRlpLengthCountdown{}. Indeed we may at times update either more than once per counter-cycle, -see section~(\ref{rlp txn v2: phase constraints: access list: subphases: countdown}) and -note~(\ref{rlp txn v2: phase constraints: access list: subphases: countdown: non counter constancy}). +see section~(\ref{rlp txn: phase constraints: access list: subphases: countdown}) and +note~(\ref{rlp txn: phase constraints: access list: subphases: countdown: non counter constancy}). We further the following shorthands, all of which are \textbf{bits} \[ diff --git a/rlp_txn/phase_constraints/access_list/legal_transitions.tex b/rlp_txn/phase_constraints/access_list/legal_transitions.tex index 0336a88a..6d79d6c4 100644 --- a/rlp_txn/phase_constraints/access_list/legal_transitions.tex +++ b/rlp_txn/phase_constraints/access_list/legal_transitions.tex @@ -5,7 +5,7 @@ % \end{center} We impose that \begin{enumerate} - \item \label{rlp txn v2: phase constraints: access list: legal transitions: start with access list item prefix} + \item \label{rlp txn: phase constraints: access list: legal transitions: start with access list item prefix} \If $\locAccessListPrefix _{i} = \true$ \Then \[ \rlpTxnSharedColumnIsPrefixOfAccessListItem _{i + 1} = \phaseAccessList _{i + 1} @@ -83,7 +83,7 @@ \] \end{enumerate} \saNote{} -By counter-constancy transitions may only take place when $\ct \equiv \maxCt$ i.e. when $\done \equiv 1$, see (\ref{rlp txn v2: generalities: ct and ct_max}). +By counter-constancy transitions may only take place when $\ct \equiv \maxCt$ i.e. when $\done \equiv 1$, see (\ref{rlp txn: generalities: ct and ct_max}). The constraint adorned with (\sanityCheck) follows from that. The other constraints linking sub-sums to \done{} enforce the fact that \begin{itemize} diff --git a/rlp_txn/phase_constraints/access_list/subphases/_inputs.tex b/rlp_txn/phase_constraints/access_list/subphases/_inputs.tex index ad3b10a0..1592090a 100644 --- a/rlp_txn/phase_constraints/access_list/subphases/_inputs.tex +++ b/rlp_txn/phase_constraints/access_list/subphases/_inputs.tex @@ -1,6 +1,6 @@ -\subsubsubsection{\rlp{}-prefix of the full access list } \label{rlp txn v2: phase constraints: access list: subphases: full access list prefix} \input{phase_constraints/access_list/subphases/prefix_of_full_access_list} -\subsubsubsection{\rlp{}-prefix of access list items } \label{rlp txn v2: phase constraints: access list: subphases: access item prefix} \input{phase_constraints/access_list/subphases/prefix_of_access_list_item} -\subsubsubsection{\rlp{}-ization of addresses } \label{rlp txn v2: phase constraints: access list: subphases: address} \input{phase_constraints/access_list/subphases/address} -\subsubsubsection{\rlp{}-prefix of storage key lists } \label{rlp txn v2: phase constraints: access list: subphases: storage key list prefix} \input{phase_constraints/access_list/subphases/prefix_of_storage_key_list} -\subsubsubsection{\rlp{}-ization of storage keys } \label{rlp txn v2: phase constraints: access list: subphases: storage key} \input{phase_constraints/access_list/subphases/storage_key} -\subsubsubsection{Finalization constraints } \label{rlp txn v2: phase constraints: access list: subphases: finalization constraints} \input{phase_constraints/access_list/subphases/finalization} +\subsubsubsection{\rlp{}-prefix of the full access list } \label{rlp txn: phase constraints: access list: subphases: full access list prefix} \input{phase_constraints/access_list/subphases/prefix_of_full_access_list} +\subsubsubsection{\rlp{}-prefix of access list items } \label{rlp txn: phase constraints: access list: subphases: access item prefix} \input{phase_constraints/access_list/subphases/prefix_of_access_list_item} +\subsubsubsection{\rlp{}-ization of addresses } \label{rlp txn: phase constraints: access list: subphases: address} \input{phase_constraints/access_list/subphases/address} +\subsubsubsection{\rlp{}-prefix of storage key lists } \label{rlp txn: phase constraints: access list: subphases: storage key list prefix} \input{phase_constraints/access_list/subphases/prefix_of_storage_key_list} +\subsubsubsection{\rlp{}-ization of storage keys } \label{rlp txn: phase constraints: access list: subphases: storage key} \input{phase_constraints/access_list/subphases/storage_key} +\subsubsubsection{Finalization constraints } \label{rlp txn: phase constraints: access list: subphases: finalization constraints} \input{phase_constraints/access_list/subphases/finalization} diff --git a/rlp_txn/phase_constraints/access_list/subphases/prefix_of_full_access_list.tex b/rlp_txn/phase_constraints/access_list/subphases/prefix_of_full_access_list.tex index daabbd11..e79af686 100644 --- a/rlp_txn/phase_constraints/access_list/subphases/prefix_of_full_access_list.tex +++ b/rlp_txn/phase_constraints/access_list/subphases/prefix_of_full_access_list.tex @@ -9,7 +9,7 @@ we impose \[ \left\{ \begin{array}{lcll} - \rlpTxnSharedColumnIsPrefixOfAccessListItem _{i} & = & \false & (\sanityCheck), \text{ see section~(\ref{rlp txn v2: phase constraints: access list: access list bits})} \\ + \rlpTxnSharedColumnIsPrefixOfAccessListItem _{i} & = & \false & (\sanityCheck), \text{ see section~(\ref{rlp txn: phase constraints: access list: access list bits})} \\ \rlpTxnSharedColumnIsAccessListAddress _{i} & = & \false & (\sanityCheck), \text{ idem} \\ \rlpTxnSharedColumnIsPrefixOfStorageKeyList _{i} & = & \false & (\sanityCheck), \text{ idem} \\ \rlpTxnSharedColumnIsAccessListStorageKey _{i} & = & \false & (\sanityCheck), \text{ idem} \\ @@ -51,7 +51,7 @@ \] \saNote{} The (\sanityCheck) constraints follow from - section~(\ref{rlp txn v2: phase constraints: access list: access list bits}) and - constraint~(\ref{rlp txn v2: phase constraints: access list: legal transitions: start with access list item prefix}). + section~(\ref{rlp txn: phase constraints: access list: access list bits}) and + constraint~(\ref{rlp txn: phase constraints: access list: legal transitions: start with access list item prefix}). \end{enumerate} diff --git a/rlp_txn/phase_constraints/data/_inputs.tex b/rlp_txn/phase_constraints/data/_inputs.tex index 1aaabf44..eda82b49 100644 --- a/rlp_txn/phase_constraints/data/_inputs.tex +++ b/rlp_txn/phase_constraints/data/_inputs.tex @@ -1,3 +1,3 @@ -\subsubsection{Shorthands } \label{rlp txn v2: phase constraints: payload: shorthands} \input{phase_constraints/data/shorthands} -\subsubsection{\rlp{}-prefix of payload } \label{rlp txn v2: phase constraints: payload: payload size analysis} \input{phase_constraints/data/payload_size_analysis} -\subsubsection{\rlp{}-izing the payload limbs } \label{rlp txn v2: phase constraints: payload: limb content analysis} \input{phase_constraints/data/limb_content_analysis} +\subsubsection{Shorthands } \label{rlp txn: phase constraints: payload: shorthands} \input{phase_constraints/data/shorthands} +\subsubsection{\rlp{}-prefix of payload } \label{rlp txn: phase constraints: payload: payload size analysis} \input{phase_constraints/data/payload_size_analysis} +\subsubsection{\rlp{}-izing the payload limbs } \label{rlp txn: phase constraints: payload: limb content analysis} \input{phase_constraints/data/limb_content_analysis} diff --git a/rlp_txn/phase_constraints/data/limb_content_analysis.tex b/rlp_txn/phase_constraints/data/limb_content_analysis.tex index 2d379aa9..c89ff7a6 100644 --- a/rlp_txn/phase_constraints/data/limb_content_analysis.tex +++ b/rlp_txn/phase_constraints/data/limb_content_analysis.tex @@ -58,7 +58,7 @@ \end{enumerate} \saNote{} The above constraining of \phaseEnd{}, -along with section~(\ref{rlp txn v2: generalities: ct and ct_max}), +along with section~(\ref{rlp txn: generalities: ct and ct_max}), implicitly constrain $\maxCt$ to be \[ \left\lceil \frac{\left\| \textbf{p} \right\|}{\llarge} \right\rceil diff --git a/rlp_txn/phase_constraints/data/payload_size_analysis.tex b/rlp_txn/phase_constraints/data/payload_size_analysis.tex index 50a0509f..3fb68997 100644 --- a/rlp_txn/phase_constraints/data/payload_size_analysis.tex +++ b/rlp_txn/phase_constraints/data/payload_size_analysis.tex @@ -6,7 +6,7 @@ The present section performs an analysis of the transaction's payload size. This is required to justify the \rlp{}-prefix associated with \rlp{}-izing the payload $\textbf{p} \in \mathbb{B}$: -\label{rlp txn v2: phase constraints: payload: payload size analysis: definition of payload in terms of transaction fields} +\label{rlp txn: phase constraints: payload: payload size analysis: definition of payload in terms of transaction fields} \[ \textbf{p} \equiv \begin{cases} diff --git a/rlp_txn/phase_constraints/data/shorthands.tex b/rlp_txn/phase_constraints/data/shorthands.tex index 982f9887..dd0b6e7b 100644 --- a/rlp_txn/phase_constraints/data/shorthands.tex +++ b/rlp_txn/phase_constraints/data/shorthands.tex @@ -15,12 +15,12 @@ \locIsLimbContentAnalysisRow _{i} & \define & \isCmp _{i - 1} & \cdot & \isCmp _{i} & \cdot & \phaseData _{i} \\ \end{array} \right. \] -\saNote{} \label{rlp txn v2: phase constraints: payload: asymmetry between row nature bits} +\saNote{} \label{rlp txn: phase constraints: payload: asymmetry between row nature bits} There is (seemingly) an asymmetry between the definitions of \locIsPayloadSizeAnalysisRow{} and \locIsLimbContentAnalysisRow{}. However, in light of -constraint~(\ref{rlp txn v2: generalities: perspectives: perspective columns are fully constrained and every transaction row is followed by at least one computation row}), +constraint~(\ref{rlp txn: generalities: perspectives: perspective columns are fully constrained and every transaction row is followed by at least one computation row}), we have \[ \isTxn _{i - 1} \equiv 1 diff --git a/rlp_txn/phase_constraints/definition.tex b/rlp_txn/phase_constraints/definition.tex index 93fca28b..ac08433d 100644 --- a/rlp_txn/phase_constraints/definition.tex +++ b/rlp_txn/phase_constraints/definition.tex @@ -2,7 +2,7 @@ \phaseRlpPrefix{} is the phase where the $\transactionType$ of transaction, concatanated with the \rlp{} prefix of the total list is computed. Not all phases are accessible to any transaction type, -see section~(\ref{rlp txn v2: generalities: PHASE_END constraints}). +see section~(\ref{rlp txn: generalities: PHASE_END constraints}). However, the actions performed during a given phase are independent of the underlying transaction type. Most phases have $\lx \equiv 1$ \emph{and} $\lt \equiv 1$, @@ -17,7 +17,7 @@ The phases \phaseY{}, \phaseR{} and \phaseS{} correspond to the \rlp{}-ization of components of the signature. They therefore only contribute to limbs belonging to $\locLtTilde$. -The table~(\ref{rlp txn v2: phase constraints: definitions: table}) shows the phase which \textbf{will be executed} depending on the \transactionType. +The table~(\ref{rlp txn: phase constraints: definitions: table}) shows the phase which \textbf{will be executed} depending on the \transactionType. \begin{table}[h] \def\gCheckMark {\text{~{\color{solarized-green}\faCheck}~}} \def\rCross {\text{~{\color{gray}\faClose}~}} @@ -45,6 +45,6 @@ $\phaseS$ & \texttt{s} & \gCM & \gCM & \gCM & \true & \false \\ \hline \end{tabular} \caption{Phase definition} - \label{rlp txn v2: phase constraints: definitions: table} + \label{rlp txn: phase constraints: definitions: table} \end{table} diff --git a/rlp_txn/phase_constraints/int.tex b/rlp_txn/phase_constraints/int.tex index cbcfdced..b311425a 100644 --- a/rlp_txn/phase_constraints/int.tex +++ b/rlp_txn/phase_constraints/int.tex @@ -69,8 +69,8 @@ \end{enumerate} \saNote{} Given the constraints from -section~(\ref{rlp txn v2: specialized: processing: integer}) and -section~(\ref{rlp txn v2: specialized: utils calls: integer}), +section~(\ref{rlp txn: specialized: processing: integer}) and +section~(\ref{rlp txn: specialized: utils calls: integer}), the shorthand definitions of \locPhaseAppropriateIntegerHi{} and \locPhaseAppropriateIntegerLo{} diff --git a/rlp_txn/phase_constraints/rlp_prefix.tex b/rlp_txn/phase_constraints/rlp_prefix.tex index e4df0117..914875b3 100644 --- a/rlp_txn/phase_constraints/rlp_prefix.tex +++ b/rlp_txn/phase_constraints/rlp_prefix.tex @@ -4,12 +4,12 @@ We unconditionally impose that \begin{enumerate} - \item $\ltByteSizeCountDown _{i} = \ltByteSizeCountDown _{i + 1}$ - \item $\lxByteSizeCountDown _{i} = \lxByteSizeCountDown _{i + 1}$ + \item $\ltByteSizeCountdown _{i} = \ltByteSizeCountdown _{i + 1}$ + \item $\lxByteSizeCountdown _{i} = \lxByteSizeCountdown _{i + 1}$ \item $\maxCt _{i} = 0$ \quad (\sanityCheck) \end{enumerate} \saNote{} -The initial value of \ltByteSizeCountDown{} +The initial value of \ltByteSizeCountdown{} is the length of the \rlp{}-ization of the whole transaction \emph{minus} the number of bytes of the global \rlp{} prefix itself and, if applicable, the first byte encoding the transaction type. @@ -70,7 +70,7 @@ \rlpProcessByteString { anchorRow = i , relOffset = \locRowOffset , - byteStringLength = \ltByteSizeCountDown _{i} , + byteStringLength = \ltByteSizeCountdown _{i} , firstByte = \nothing , isList = \true , mustBeNontrivial = \true , @@ -99,7 +99,7 @@ \rlpProcessByteString { anchorRow = i , relOffset = \locRowOffset , - byteStringLength = \lxByteSizeCountDown _{i} , + byteStringLength = \lxByteSizeCountdown _{i} , firstByte = \nothing , isList = \true , mustBeNontrivial = \true , diff --git a/rlp_txn/specialized/_inputs.tex b/rlp_txn/specialized/_inputs.tex index 12085859..e7b79406 100644 --- a/rlp_txn/specialized/_inputs.tex +++ b/rlp_txn/specialized/_inputs.tex @@ -1,5 +1,5 @@ -\subsection{Introdution } \label{rlp txn v2: specialized: intro} \input{specialized/intro} -\subsection{Limb setting constraints } \label{rlp txn v2: specialized: limb setting} \input{specialized/limb_setting/_inputs} -\subsection{Limb membership constraints } \label{rlp txn v2: specialized: limb membership} \input{specialized/limbs_of_lt_lx} -\subsection{\rlpUtilsMod{} call constraints } \label{rlp txn v2: specialized: utils calls} \input{specialized/utils_calls/_inputs} -\subsection{Data processing compound constraints } \label{rlp txn v2: specialized: processing} \input{specialized/processing/_inputs} +\subsection{Introdution } \label{rlp txn: specialized: intro} \input{specialized/intro} +\subsection{Limb setting constraints } \label{rlp txn: specialized: limb setting} \input{specialized/limb_setting/_inputs} +\subsection{Limb membership constraints } \label{rlp txn: specialized: limb membership} \input{specialized/limbs_of_lt_lx} +\subsection{\rlpUtilsMod{} call constraints } \label{rlp txn: specialized: utils calls} \input{specialized/utils_calls/_inputs} +\subsection{Data processing compound constraints } \label{rlp txn: specialized: processing} \input{specialized/processing/_inputs} diff --git a/rlp_txn/specialized/limb_setting/_inputs.tex b/rlp_txn/specialized/limb_setting/_inputs.tex index b09b7099..74fae5b9 100644 --- a/rlp_txn/specialized/limb_setting/_inputs.tex +++ b/rlp_txn/specialized/limb_setting/_inputs.tex @@ -1,4 +1,4 @@ -\subsubsection{\conditionallySetLimbName{} constraint } \label{rlp txn v2: specialized: limb setting: potentially set limb} \input{specialized/limb_setting/potentially_set_limb} -\subsubsection{\setLimbName{} constraint } \label{rlp txn v2: specialized: limb setting: finalize limb} \input{specialized/limb_setting/set_limb} -\subsubsection{\discardLimbName{} constraint } \label{rlp txn v2: specialized: limb setting: dismiss limb} \input{specialized/limb_setting/discard_limb} +\subsubsection{\conditionallySetLimbName{} constraint } \label{rlp txn: specialized: limb setting: potentially set limb} \input{specialized/limb_setting/conditionally_set_limb} +\subsubsection{\setLimbName{} constraint } \label{rlp txn: specialized: limb setting: finalize limb} \input{specialized/limb_setting/set_limb} +\subsubsection{\discardLimbName{} constraint } \label{rlp txn: specialized: limb setting: dismiss limb} \input{specialized/limb_setting/discard_limb} diff --git a/rlp_txn/specialized/limb_setting/conditionally_set_limb.tex b/rlp_txn/specialized/limb_setting/conditionally_set_limb.tex new file mode 100644 index 00000000..49ae027e --- /dev/null +++ b/rlp_txn/specialized/limb_setting/conditionally_set_limb.tex @@ -0,0 +1,19 @@ +We define \conditionallySetLimbName{} as follows: +\[ + \begin{array}{l} + \conditionallySetLimb { + anchorRow = i , + relOffset = \relof , + condition = \loc{condition\_bit} , + limb = \loc{limb} , + nBytes = \loc{number\_of\_bytes} , + } + \vspace{2mm} \\ + \qquad \define + \left\{ \begin{array}{lcl} + \lc _{i + \relof} & = & \loc{condition\_bit} \\ + \rlpTxnComputationColumnLimb _{i + \relof} & = & \loc{condition\_bit} \cdot \loc{limb} \\ + \rlpTxnComputationColumnLimbSize _{i + \relof} & = & \loc{condition\_bit} \cdot \loc{number\_of\_bytes} \\ + \end{array} \right. + \end{array} +\] diff --git a/rlp_txn/specialized/limb_setting/potentially_set_limb.tex b/rlp_txn/specialized/limb_setting/potentially_set_limb.tex index e74d1dd7..49ae027e 100644 --- a/rlp_txn/specialized/limb_setting/potentially_set_limb.tex +++ b/rlp_txn/specialized/limb_setting/potentially_set_limb.tex @@ -11,7 +11,7 @@ \vspace{2mm} \\ \qquad \define \left\{ \begin{array}{lcl} - \lc _{i + \relof} & = & \loc{condition\_bit} \\ + \lc _{i + \relof} & = & \loc{condition\_bit} \\ \rlpTxnComputationColumnLimb _{i + \relof} & = & \loc{condition\_bit} \cdot \loc{limb} \\ \rlpTxnComputationColumnLimbSize _{i + \relof} & = & \loc{condition\_bit} \cdot \loc{number\_of\_bytes} \\ \end{array} \right. diff --git a/rlp_txn/specialized/limb_setting/set_limb.tex b/rlp_txn/specialized/limb_setting/set_limb.tex index 7f832cc2..c8ac829c 100644 --- a/rlp_txn/specialized/limb_setting/set_limb.tex +++ b/rlp_txn/specialized/limb_setting/set_limb.tex @@ -10,7 +10,7 @@ \vspace{2mm} \\ \qquad \define \left\{ \begin{array}{lcl} - \lc _{i + \relof} & = & \true \\ + \lc _{i + \relof} & = & \true \\ \rlpTxnComputationColumnLimb _{i + \relof} & = & \loc{limb} \\ \rlpTxnComputationColumnLimbSize _{i + \relof} & = & \loc{number\_of\_bytes} \\ \end{array} \right. diff --git a/rlp_txn/specialized/processing/_inputs.tex b/rlp_txn/specialized/processing/_inputs.tex index d3e7111c..d754b56a 100644 --- a/rlp_txn/specialized/processing/_inputs.tex +++ b/rlp_txn/specialized/processing/_inputs.tex @@ -1,4 +1,4 @@ -\subsubsection{\rlpProcessIntegerName {} constraints } \label{rlp txn v2: specialized: processing: integer} \input{specialized/processing/integer} -\subsubsection{\rlpProcessByteStringName {} constraints } \label{rlp txn v2: specialized: processing: byte string prefix} \input{specialized/processing/byte_string_prefix} -\subsubsection{\rlpProcessBytesThirtyTwoName {} constraints } \label{rlp txn v2: specialized: processing: bytes 32} \input{specialized/processing/bytes_32} -\subsubsection{\rlpProcessAddressName {} constraints } \label{rlp txn v2: specialized: processing: address} \input{specialized/processing/address} +\subsubsection{\rlpProcessIntegerName {} constraints } \label{rlp txn: specialized: processing: integer} \input{specialized/processing/integer} +\subsubsection{\rlpProcessByteStringName {} constraints } \label{rlp txn: specialized: processing: byte string prefix} \input{specialized/processing/byte_string_prefix} +\subsubsection{\rlpProcessBytesThirtyTwoName {} constraints } \label{rlp txn: specialized: processing: bytes 32} \input{specialized/processing/bytes_32} +\subsubsection{\rlpProcessAddressName {} constraints } \label{rlp txn: specialized: processing: address} \input{specialized/processing/address} diff --git a/rlp_txn/specialized/processing/integer.tex b/rlp_txn/specialized/processing/integer.tex index c24134d6..680c639d 100644 --- a/rlp_txn/specialized/processing/integer.tex +++ b/rlp_txn/specialized/processing/integer.tex @@ -93,7 +93,7 @@ relOffset = \relof + 2 , condition = \locOutputInputIntegerIsNonzero , limb = \locLastLimb , - nBytes = \locLastLimbByteSize , + nBytes = \locLastLimbByteSize , } \] \end{description} diff --git a/rlp_txn/specialized/utils_calls/_inputs.tex b/rlp_txn/specialized/utils_calls/_inputs.tex index 78fd50b4..fdc8ace0 100644 --- a/rlp_txn/specialized/utils_calls/_inputs.tex +++ b/rlp_txn/specialized/utils_calls/_inputs.tex @@ -1,5 +1,5 @@ -\subsubsection{\rlpUtilsInstCallIntegerName {} constraints } \label{rlp txn v2: specialized: utils calls: integer} \input{specialized/utils_calls/integer} -\subsubsection{\rlpUtilsInstCallByteStringPrefixName {} constraints } \label{rlp txn v2: specialized: utils calls: byte string prefix} \input{specialized/utils_calls/byte_string_prefix} -\subsubsection{\rlpUtilsInstCallBytesThirtyTwoName {} constraints } \label{rlp txn v2: specialized: utils calls: bytes 32} \input{specialized/utils_calls/bytes_32} -\subsubsection{\rlpUtilsInstCallDataPricingName {} constraints } \label{rlp txn v2: specialized: utils calls: data pricing} \input{specialized/utils_calls/data_pricing} +\subsubsection{\rlpUtilsInstCallIntegerName {} constraints } \label{rlp txn: specialized: utils calls: integer} \input{specialized/utils_calls/integer} +\subsubsection{\rlpUtilsInstCallByteStringPrefixName {} constraints } \label{rlp txn: specialized: utils calls: byte string prefix} \input{specialized/utils_calls/byte_string_prefix} +\subsubsection{\rlpUtilsInstCallBytesThirtyTwoName {} constraints } \label{rlp txn: specialized: utils calls: bytes 32} \input{specialized/utils_calls/bytes_32} +\subsubsection{\rlpUtilsInstCallDataPricingName {} constraints } \label{rlp txn: specialized: utils calls: data pricing} \input{specialized/utils_calls/data_pricing} diff --git a/rlp_txn/specialized/utils_calls/byte_string_prefix.tex b/rlp_txn/specialized/utils_calls/byte_string_prefix.tex index e60548a3..fd97110f 100644 --- a/rlp_txn/specialized/utils_calls/byte_string_prefix.tex +++ b/rlp_txn/specialized/utils_calls/byte_string_prefix.tex @@ -12,11 +12,11 @@ \\ \qquad \define \left\{ \begin{array}{lcl} - \rlpTxnComputationColumnRlpUtilsFlag _{i + \relof} & = & \rOne \\ - \rlpTxnComputationColumnRlpUtilsInstruction _{i + \relof} & = & \rlpUtilsInstByteStringPrefix \\ - \rlpTxnComputationColumnExoDataColumn{1} _{i + \relof} & = & \loc{length} \\ - \rlpTxnComputationColumnExoDataColumn{2} _{i + \relof} & = & \loc{first\_byte} \\ - \rlpTxnComputationColumnExoDataColumn{3} _{i + \relof} & = & \loc{is\_list} \\ + \rlpTxnComputationColumnRlpUtilsFlag _{i + \relof} & = & \rOne \\ + \rlpTxnComputationColumnRlpUtilsInstruction _{i + \relof} & = & \rlpUtilsInstByteStringPrefix \\ + \rlpTxnComputationColumnExoDataColumn{1} _{i + \relof} & = & \loc{length} \\ + \rlpTxnComputationColumnExoDataColumn{2} _{i + \relof} & = & \loc{first\_byte} \\ + \rlpTxnComputationColumnExoDataColumn{3} _{i + \relof} & = & \loc{is\_list} \\ \end{array} \right. \end{array} \right. \] diff --git a/rlp_txn/specialized/utils_calls/data_pricing.tex b/rlp_txn/specialized/utils_calls/data_pricing.tex index 5802b320..5814a5d8 100644 --- a/rlp_txn/specialized/utils_calls/data_pricing.tex +++ b/rlp_txn/specialized/utils_calls/data_pricing.tex @@ -11,10 +11,10 @@ \\ \qquad \define \left\{ \begin{array}{lcl} - \rlpTxnComputationColumnRlpUtilsFlag _{i + \relof} & = & \rOne \\ - \rlpTxnComputationColumnRlpUtilsInstruction _{i + \relof} & = & \rlpUtilsInstDataPricing \\ - \rlpTxnComputationColumnExoDataColumn{1} _{i + \relof} & = & \loc{limb} \\ - \rlpTxnComputationColumnExoDataColumn{2} _{i + \relof} & = & \loc{n\_bytes} \\ + \rlpTxnComputationColumnRlpUtilsFlag _{i + \relof} & = & \rOne \\ + \rlpTxnComputationColumnRlpUtilsInstruction _{i + \relof} & = & \rlpUtilsInstDataPricing \\ + \rlpTxnComputationColumnExoDataColumn{1} _{i + \relof} & = & \loc{limb} \\ + \rlpTxnComputationColumnExoDataColumn{2} _{i + \relof} & = & \loc{n\_bytes} \\ \end{array} \right. \end{array} \right. \]