Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(shakira): delegate to wcp #201

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 1 addition & 31 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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} \
Expand All @@ -112,6 +111,7 @@ ZKEVM_MODULES := ${ALU} \
${RLP_TXRCPT} \
${ROM} \
${ROM_LEX} \
${SHAKIRA_DATA} \
${SHIFT} \
${STP} \
${TABLES} \
Expand All @@ -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}
Expand Down
4 changes: 1 addition & 3 deletions shakiradata/columns.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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))

Expand Down
7 changes: 1 addition & 6 deletions shakiradata/constants.lisp
Original file line number Diff line number Diff line change
@@ -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)


52 changes: 19 additions & 33 deletions shakiradata/constraints.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)))
Expand All @@ -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))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
Expand Down Expand Up @@ -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 ;;
Expand Down Expand Up @@ -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 ;;
Expand Down
36 changes: 36 additions & 0 deletions shakiradata/lookups/shakira_into_wcp_increasing_id.lisp
Original file line number Diff line number Diff line change
@@ -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)
))


34 changes: 34 additions & 0 deletions shakiradata/lookups/shakira_into_wcp_nonzero_last_nbytes.lisp
Original file line number Diff line number Diff line change
@@ -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-final-data-row) 1)
(* (is-final-data-row) EVM_INST_GT)
))


22 changes: 22 additions & 0 deletions shakiradata/lookups/shakira_into_wcp_small_last_nbytes.lisp
Original file line number Diff line number Diff line change
@@ -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-final-data-row) 1)
(* (is-final-data-row) WCP_INST_LEQ)
))


Loading