From 5a3aaf6c92779fef2566d12708fad92fdfb90b7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 11:54:34 +0100 Subject: [PATCH 1/3] fix: added unpermuted account columns and made it compile --- Makefile | 6 +-- .../consistency/account/columns.lisp | 41 ++++++++++++++++--- hub/lookups/hub_into_rlp_txn.lisp | 2 +- 3 files changed, 39 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index f5a2f78c..84bb3e2b 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,6 @@ HUB := $(wildcard hub/columns/*lisp) \ $(wildcard hub/constraints/consistency/account/*lisp) \ $(wildcard hub/constraints/consistency/context/*lisp) \ $(wildcard hub/constraints/consistency/execution_environment/*lisp) \ - $(wildcard hub/constraints/consistency/stack/*lisp) \ $(wildcard hub/constraints/consistency/storage/*lisp) \ $(wildcard hub/constraints/context-rows/*lisp) \ $(wildcard hub/constraints/generalities/*lisp) \ @@ -40,7 +39,8 @@ HUB := $(wildcard hub/columns/*lisp) \ hub/constants.lisp - # Missing from the above +# Missing from the above +# $(wildcard hub/constraints/consistency/stack/*lisp) \ ALU := $(wildcard alu/add/*.lisp) \ $(wildcard alu/ext/*.lisp) \ @@ -135,7 +135,7 @@ ZKEVM_MODULES := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB_COLUMNS} \ + ${HUB} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ diff --git a/hub/constraints/consistency/account/columns.lisp b/hub/constraints/consistency/account/columns.lisp index 6fdcf5e4..f59c8a89 100644 --- a/hub/constraints/consistency/account/columns.lisp +++ b/hub/constraints/consistency/account/columns.lisp @@ -1,12 +1,13 @@ (module hub) (defcolumns - ;; account consistency permutation related - ( acp_FIRST_IN_CNF :binary@prove ) ( acp_FIRST_IN_BLK :binary@prove ) ( acp_FIRST_IN_TXN :binary@prove ) - ( acp_AGAIN_IN_CNF :binary@prove ) ( acp_AGAIN_IN_BLK :binary@prove ) ( acp_AGAIN_IN_TXN :binary@prove ) - ( acp_FINAL_IN_CNF :binary@prove ) ( acp_FINAL_IN_BLK :binary@prove ) ( acp_FINAL_IN_TXN :binary@prove ) - ( acp_DEPLOYMENT_NUMBER_FIRST_IN_BLOCK :i16) - ( acp_DEPLOYMENT_NUMBER_FINAL_IN_BLOCK :i16) + + ;; the unpermuted versions of those columns + ( FIRST_IN_CNF :binary@prove ) ( FIRST_IN_BLK :binary@prove ) ( FIRST_IN_TXN :binary@prove ) + ( AGAIN_IN_CNF :binary@prove ) ( AGAIN_IN_BLK :binary@prove ) ( AGAIN_IN_TXN :binary@prove ) + ( FINAL_IN_CNF :binary@prove ) ( FINAL_IN_BLK :binary@prove ) ( FINAL_IN_TXN :binary@prove ) + ( DEPLOYMENT_NUMBER_FIRST_IN_BLOCK :i16) + ( DEPLOYMENT_NUMBER_FINAL_IN_BLOCK :i16) ) ;; acp_ ⇔ account consistency permutation @@ -44,6 +45,18 @@ acp_MARKED_FOR_SELFDESTRUCT_NEW acp_TRM_FLAG acp_IS_PRECOMPILE + ;; permuted versions + acp_FIRST_IN_CNF + acp_FIRST_IN_BLK + acp_FIRST_IN_TXN + acp_AGAIN_IN_CNF + acp_AGAIN_IN_BLK + acp_AGAIN_IN_TXN + acp_FINAL_IN_CNF + acp_FINAL_IN_BLK + acp_FINAL_IN_TXN + acp_DEPLOYMENT_NUMBER_FIRST_IN_BLOCK + acp_DEPLOYMENT_NUMBER_FINAL_IN_BLOCK ) ;; original columns ;;;;;;;;;;;;;;;;;;; @@ -77,5 +90,21 @@ account/MARKED_FOR_SELFDESTRUCT_NEW account/TRM_FLAG account/IS_PRECOMPILE + ;; un permuted versions + FIRST_IN_CNF + FIRST_IN_BLK + FIRST_IN_TXN + AGAIN_IN_CNF + AGAIN_IN_BLK + AGAIN_IN_TXN + FINAL_IN_CNF + FINAL_IN_BLK + FINAL_IN_TXN + DEPLOYMENT_NUMBER_FIRST_IN_BLOCK + DEPLOYMENT_NUMBER_FINAL_IN_BLOCK ) ) + + + + diff --git a/hub/lookups/hub_into_rlp_txn.lisp b/hub/lookups/hub_into_rlp_txn.lisp index 63f9b500..36f20d38 100644 --- a/hub/lookups/hub_into_rlp_txn.lisp +++ b/hub/lookups/hub_into_rlp_txn.lisp @@ -37,7 +37,7 @@ (* rlptxn.ADDR_HI (hub-into-rlp-txn-tgt-selector)) (* rlptxn.ADDR_LO (hub-into-rlp-txn-tgt-selector)) (* [rlptxn.INPUT 1] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector)) - (* [rlptxn.INPUT 2] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector))) + (* [rlptxn.INPUT 2] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector)) ) ;; source columns ( From 6578e105d377404402d5ff49f60c919c1f33e25c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 11:58:20 +0100 Subject: [PATCH 2/3] fix: added these columns to the account/ perspective --- hub/columns/account.lisp | 10 +++++- .../consistency/account/columns.lisp | 31 +++++++------------ 2 files changed, 20 insertions(+), 21 deletions(-) diff --git a/hub/columns/account.lisp b/hub/columns/account.lisp index bef10181..de0b9d72 100644 --- a/hub/columns/account.lisp +++ b/hub/columns/account.lisp @@ -54,6 +54,14 @@ (RLPADDR_SALT_HI :i128) (RLPADDR_SALT_LO :i128) (RLPADDR_KEC_HI :i128) - (RLPADDR_KEC_LO :i128))) + (RLPADDR_KEC_LO :i128) + + ;; the unpermuted versions of those columns + ( FIRST_IN_CNF :binary@prove ) ( FIRST_IN_BLK :binary@prove ) ( FIRST_IN_TXN :binary@prove ) + ( AGAIN_IN_CNF :binary@prove ) ( AGAIN_IN_BLK :binary@prove ) ( AGAIN_IN_TXN :binary@prove ) + ( FINAL_IN_CNF :binary@prove ) ( FINAL_IN_BLK :binary@prove ) ( FINAL_IN_TXN :binary@prove ) + ( DEPLOYMENT_NUMBER_FIRST_IN_BLOCK :i16) + ( DEPLOYMENT_NUMBER_FINAL_IN_BLOCK :i16) + )) diff --git a/hub/constraints/consistency/account/columns.lisp b/hub/constraints/consistency/account/columns.lisp index f59c8a89..d081412a 100644 --- a/hub/constraints/consistency/account/columns.lisp +++ b/hub/constraints/consistency/account/columns.lisp @@ -1,14 +1,5 @@ (module hub) -(defcolumns - - ;; the unpermuted versions of those columns - ( FIRST_IN_CNF :binary@prove ) ( FIRST_IN_BLK :binary@prove ) ( FIRST_IN_TXN :binary@prove ) - ( AGAIN_IN_CNF :binary@prove ) ( AGAIN_IN_BLK :binary@prove ) ( AGAIN_IN_TXN :binary@prove ) - ( FINAL_IN_CNF :binary@prove ) ( FINAL_IN_BLK :binary@prove ) ( FINAL_IN_TXN :binary@prove ) - ( DEPLOYMENT_NUMBER_FIRST_IN_BLOCK :i16) - ( DEPLOYMENT_NUMBER_FINAL_IN_BLOCK :i16) - ) ;; acp_ ⇔ account consistency permutation (defpermutation @@ -91,17 +82,17 @@ account/TRM_FLAG account/IS_PRECOMPILE ;; un permuted versions - FIRST_IN_CNF - FIRST_IN_BLK - FIRST_IN_TXN - AGAIN_IN_CNF - AGAIN_IN_BLK - AGAIN_IN_TXN - FINAL_IN_CNF - FINAL_IN_BLK - FINAL_IN_TXN - DEPLOYMENT_NUMBER_FIRST_IN_BLOCK - DEPLOYMENT_NUMBER_FINAL_IN_BLOCK + account/FIRST_IN_CNF + account/FIRST_IN_BLK + account/FIRST_IN_TXN + account/AGAIN_IN_CNF + account/AGAIN_IN_BLK + account/AGAIN_IN_TXN + account/FINAL_IN_CNF + account/FINAL_IN_BLK + account/FINAL_IN_TXN + account/DEPLOYMENT_NUMBER_FIRST_IN_BLOCK + account/DEPLOYMENT_NUMBER_FINAL_IN_BLOCK ) ) From 03036a434f1996b758cc1e49604193cd7a0a38a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 12:00:23 +0100 Subject: [PATCH 3/3] ras --- hub/columns/account.lisp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/hub/columns/account.lisp b/hub/columns/account.lisp index de0b9d72..3df7b589 100644 --- a/hub/columns/account.lisp +++ b/hub/columns/account.lisp @@ -34,19 +34,23 @@ (DEPLOYMENT_STATUS :binary@prove) ;; TODO: demote to debug constraint (DEPLOYMENT_STATUS_NEW :binary@prove) ;; TODO: demote to debug constraint (DEPLOYMENT_STATUS_INFTY :binary@prove) ;; TODO: demote to debug constraint + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; TRM module lookup columns ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (TRM_FLAG :binary@prove) (IS_PRECOMPILE :binary@prove) ;; TODO: demote to debug constraint (TRM_RAW_ADDRESS_HI :i128) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; RLPADDR module lookup columns ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (RLPADDR_FLAG :binary@prove) (RLPADDR_RECIPE :i8) (RLPADDR_DEP_ADDR_HI :i32) @@ -56,7 +60,13 @@ (RLPADDR_KEC_HI :i128) (RLPADDR_KEC_LO :i128) - ;; the unpermuted versions of those columns + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; ;; + ;; ACCOUNT consistency temporal columns ;; + ;; ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + ;; the unpermuted columns whose permuted counter-parts will be used in account-consistency-arguments ( FIRST_IN_CNF :binary@prove ) ( FIRST_IN_BLK :binary@prove ) ( FIRST_IN_TXN :binary@prove ) ( AGAIN_IN_CNF :binary@prove ) ( AGAIN_IN_BLK :binary@prove ) ( AGAIN_IN_TXN :binary@prove ) ( FINAL_IN_CNF :binary@prove ) ( FINAL_IN_BLK :binary@prove ) ( FINAL_IN_TXN :binary@prove )