From a2d9911a0044442ad016097b5e2e2efcead6b5f3 Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Thu, 23 May 2024 06:52:57 +0530 Subject: [PATCH 1/2] feat(shakira): delegate to wcp --- Makefile | 32 +----------- shakiradata/columns.lisp | 4 +- shakiradata/constants.lisp | 7 +-- shakiradata/constraints.lisp | 52 +++++++------------ .../shakira_into_wcp_increasing_id.lisp | 36 +++++++++++++ .../shakira_into_wcp_nonzero_last_nbytes.lisp | 34 ++++++++++++ .../shakira_into_wcp_small_last_nbytes.lisp | 22 ++++++++ 7 files changed, 114 insertions(+), 73 deletions(-) create mode 100644 shakiradata/lookups/shakira_into_wcp_increasing_id.lisp create mode 100644 shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp create mode 100644 shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp diff --git a/Makefile b/Makefile index 222b9758..2ab36a8e 100644 --- a/Makefile +++ b/Makefile @@ -91,7 +91,6 @@ TXN_DATA := txndata WCP := wcp -# TODO: fix issues with the HUB and include it again in the modules ZKEVM_MODULES := ${ALU} \ ${BIN} \ ${BLAKE2f_MODEXP_DATA} \ @@ -112,6 +111,7 @@ ZKEVM_MODULES := ${ALU} \ ${RLP_TXRCPT} \ ${ROM} \ ${ROM_LEX} \ + ${SHAKIRA_DATA} \ ${SHIFT} \ ${STP} \ ${TABLES} \ @@ -121,37 +121,7 @@ ZKEVM_MODULES := ${ALU} \ # TODO: add later # ${GAS} \ -# ${SHAKIRA_DATA} \ - -#ZKEVM_MODULES := ${ALU} \ -# ${BIN} \ -# ${BLAKE2f_MODEXP_DATA} \ -# ${BLOCKDATA} \ -# ${BLOCKHASH} \ -# ${CONSTANTS} \ -# ${EC_DATA} \ -# ${EUC} \ -# ${EXP} \ -# ${GAS} \ # ${HUB} \ -# ${LIBRARY} \ -# ${LOG_DATA} \ -# ${LOG_INFO} \ -# ${MMU} \ -# ${MMIO} \ -# ${MXP} \ -# ${RLP_ADDR} \ -# ${RLP_TXN} \ -# ${RLP_TXRCPT} \ -# ${ROM} \ -# ${ROM_LEX} \ -# ${SHAKIRA_DATA} \ -# ${SHIFT} \ -# ${STP} \ -# ${TABLES} \ -# ${TRM} \ -# ${TXN_DATA} \ -# ${WCP} define.go: ${ZKEVM_MODULES} ${CORSET} wizard-iop -vv -P define -o $@ ${ZKEVM_MODULES} diff --git a/shakiradata/columns.lisp b/shakiradata/columns.lisp index 7b801632..bbca14ea 100644 --- a/shakiradata/columns.lisp +++ b/shakiradata/columns.lisp @@ -6,9 +6,8 @@ (PHASE :byte) (INDEX :i32) (INDEX_MAX :i32) - (DELTA_BYTE :byte@prove) (LIMB :i128) - (nBYTES :byte@prove) + (nBYTES :i8) (nBYTES_ACC :i32) (TOTAL_SIZE :i32) (IS_KECCAK_DATA :binary@prove) @@ -17,7 +16,6 @@ (IS_SHA2_RESULT :binary@prove) (IS_RIPEMD_DATA :binary@prove) (IS_RIPEMD_RESULT :binary@prove) - (IS_EXTRA :binary@prove) (SELECTOR_KECCAK_RES_HI :binary) (SELECTOR_KECCAK_RES_LO :binary)) diff --git a/shakiradata/constants.lisp b/shakiradata/constants.lisp index f658b2f7..66d5355b 100644 --- a/shakiradata/constants.lisp +++ b/shakiradata/constants.lisp @@ -1,11 +1,6 @@ (module shakiradata) (defconst - INDEX_MAX_SHA2_DATA 11 - INDEX_MAX_SHA2_RESULT 1 - INDEX_MAX_RIPEMD_DATA 3 - INDEX_MAX_RIPEMD_RESULT 1 - INDEX_MAX_KECCAK_DATA 0 - INDEX_MAX_KECCAK_RESULT 1) + INDEX_MAX_RESULT 1) diff --git a/shakiradata/constraints.lisp b/shakiradata/constraints.lisp index e97fd80c..bd9e1b7f 100644 --- a/shakiradata/constraints.lisp +++ b/shakiradata/constraints.lisp @@ -72,8 +72,15 @@ ;; IS_EXTRA ))) +(defun (is-first-data-row) + (force-bool (* (is-data) + (- 1 (prev (is-data)))))) + +(defun (is-last-data-row) + (force-bool (* (id-data) (next (is-result))))) + (defun (flag-sum) - (force-bool (+ (is-keccak) (is-sha2) (is-ripemd) IS_EXTRA))) + (force-bool (+ (is-keccak) (is-sha2) (is-ripemd)))) (defun (phase-sum) (+ (* PHASE_KECCAK_DATA IS_KECCAK_DATA) @@ -90,8 +97,7 @@ (defun (index-reset-bit) (force-bool (+ (* (- 1 (is-data)) (next (is-data))) - (* (- 1 (is-result)) (next (is-result))) - (* (- 1 IS_EXTRA) (next IS_EXTRA))))) + (* (- 1 (is-result)) (next (is-result)))))) (defun (legal-transitions-bit) (force-bool (+ (* IS_KECCAK_DATA (next (is-keccak))) @@ -102,9 +108,7 @@ (* IS_SHA2_RESULT (next IS_SHA2_RESULT)) (* IS_RIPEMD_RESULT (next IS_RIPEMD_RESULT)) ;; - (* (is-result) (next IS_EXTRA)) - (* IS_EXTRA - (next (+ IS_EXTRA (is-data))))))) + (* (is-result) (next (is-data)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -136,6 +140,9 @@ (eq! (flag-sum) 1)) (eq! PHASE (phase-sum)))) +(defconstraint set-total-size-for-result (:guard (is-result)) + (eq! TOTAL_SIZE WORD_SIZE)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; X.3.5 Heartbeat ;; @@ -166,34 +173,13 @@ ;; INDEX ≠ INDEX_MAX case (will-eq! INDEX (+ 1 INDEX)))))) -(defconstraint fixed-length-index-max-constraints () - (if (force-bool (+ (is-result) IS_EXTRA)) - (eq! INDEX_MAX (+ IS_KECCAK_RESULT IS_SHA2_RESULT IS_RIPEMD_RESULT IS_EXTRA IS_EXTRA)))) - -(defconstraint small-ID-increments () - (if-not-zero (will-remain-constant! RIPSHA_STAMP) - (will-eq! ID - (+ 1 - ID - (+ (* (^ 256 3) (shift DELTA_BYTE 1)) - (* (^ 256 2) (shift DELTA_BYTE 2)) - (* (^ 256 1) (shift DELTA_BYTE 3)) - (* (^ 256 0) (shift DELTA_BYTE 4))))))) - -(defconstraint smallness-of-last-nBYTES () - (if-zero (prev IS_EXTRA) - (if-not-zero IS_EXTRA - (begin (eq! (shift DELTA_BYTE 1) - (- (shift nBYTES -3) 1)) - (eq! (shift DELTA_BYTE 2) - (- (+ 240 (shift nBYTES -3)) - 1)))))) - -(defconstraint finalization (:domain {-1}) - (if-not-zero RIPSHA_STAMP - (begin (eq! INDEX INDEX_MAX) - (eq! IS_EXTRA 1)))) +(defconstraint fixed-length-index-max-constraints (:guard (is-result)) + (eq! INDEX_MAX INDEX_MAX_RESULT)) +;(defconstraint finalization (:domain {-1}) ;;debug end constraint +; (if-not-zero RIPSHA_STAMP +; (begin (eq! INDEX INDEX_MAX) +; (eq! (is-result) 1)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; X.3.6 nBYTES accumulation ;; diff --git a/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp b/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp new file mode 100644 index 00000000..8e54d129 --- /dev/null +++ b/shakiradata/lookups/shakira_into_wcp_increasing_id.lisp @@ -0,0 +1,36 @@ +;; TODO the selector functiun should be imported from shakira/constraints +(defun (is-data) + (force-bool (+ shakiradata.IS_KECCAK_DATA + ;; IS_KECCAK_RESULT + shakiradata.IS_SHA2_DATA + ;; IS_SHA2_RESULT + shakiradata.IS_RIPEMD_DATA + ;; IS_RIPEMD_RESULT + ))) + +(defun (is-first-data-row) + (force-bool (* (is-data) + (- 1 (prev (is-data)))))) + +(deflookup + shakira-into-wcp-increasing-id + ; target colums (in WCP) + ( + wcp.ARG_1_HI + wcp.ARG_1_LO + wcp.ARG_2_HI + wcp.ARG_2_LO + wcp.RES + wcp.INST + ) + ; source columns + ( + 0 + (* (is-first-data-row) (prev shakiradata.ID)) + 0 + (* (is-first-data-row) shakiradata.ID) + (* (is-first-data-row) 1) + (* (is-first-data-row) EVM_INST_LT) + )) + + diff --git a/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp new file mode 100644 index 00000000..6c0e992e --- /dev/null +++ b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp @@ -0,0 +1,34 @@ +;; TODO the selector functiun should be imported from shakira/constraints +(defun (is-result) + (force-bool (+ ;; shakiradata.IS_KECCAK_DATA + shakiradata.IS_KECCAK_RESULT + ;; shakiradata.IS_SHA2_DATA + shakiradata.IS_SHA2_RESULT + ;; shakiradata.IS_RIPEMD_DATA + shakiradata.IS_RIPEMD_RESULT))) + +(defun (is-final-data-row) + (force-bool (* (is-data) (next (is-result))))) + +(deflookup + shakira-into-wcp-nonzero-last-nbytes + ; target colums (in WCP) + ( + wcp.ARG_1_HI + wcp.ARG_1_LO + wcp.ARG_2_HI + wcp.ARG_2_LO + wcp.RES + wcp.INST + ) + ; source columns + ( + 0 + (* (is-final-data-row) shakiradata.nBYTES) + 0 + 0 + (* (is-first-data-row) 1) + (* (is-first-data-row) EVM_INST_GT) + )) + + diff --git a/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp new file mode 100644 index 00000000..c8594df1 --- /dev/null +++ b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp @@ -0,0 +1,22 @@ +(deflookup + shakira-into-wcp-small-last-nbytes + ; target colums (in WCP) + ( + wcp.ARG_1_HI + wcp.ARG_1_LO + wcp.ARG_2_HI + wcp.ARG_2_LO + wcp.RES + wcp.INST + ) + ; source columns + ( + 0 + (* (is-final-data-row) shakiradata.nBYTES) + 0 + (* (is-final-data-row) LLARGE) + (* (is-first-data-row) 1) + (* (is-first-data-row) WCP_INST_LEQ) + )) + + From 9e726082ca66b2a89ca25a360a1a6cb4245b0447 Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Thu, 23 May 2024 10:11:57 +0530 Subject: [PATCH 2/2] fix: typo --- shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp | 4 ++-- shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp index 6c0e992e..82ac95ab 100644 --- a/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp +++ b/shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp @@ -27,8 +27,8 @@ (* (is-final-data-row) shakiradata.nBYTES) 0 0 - (* (is-first-data-row) 1) - (* (is-first-data-row) EVM_INST_GT) + (* (is-final-data-row) 1) + (* (is-final-data-row) EVM_INST_GT) )) diff --git a/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp index c8594df1..bcca86f0 100644 --- a/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp +++ b/shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp @@ -15,8 +15,8 @@ (* (is-final-data-row) shakiradata.nBYTES) 0 (* (is-final-data-row) LLARGE) - (* (is-first-data-row) 1) - (* (is-first-data-row) WCP_INST_LEQ) + (* (is-final-data-row) 1) + (* (is-final-data-row) WCP_INST_LEQ) ))