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.

Sign up for GitHub

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(txn-data): implement max nonce comparaison #291

Merged
merged 3 commits into from
Aug 19, 2024
Merged

feat(txn-data): implement max nonce comparaison #291

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ddea238
feat(txn-data): implement max nonce comparaison
letypequividelespoubelles Aug 19, 2024
97b4be3
enable TXN_DATA columns for lookup
letypequividelespoubelles Aug 19, 2024
2db1c54
style: ras
letypequividelespoubelles Aug 19, 2024
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
6 changes: 4 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,8 @@ TABLES := reftables/bin_reftable.lisp \

TRM := trm

TXN_DATA := txndata
# TXN_DATA := txndata
TXN_DATA := txndata/columns.lisp

WCP := wcp

Expand All @@ -114,6 +115,7 @@ ZKEVM_MODULES := ${ALU} \
${CONSTANTS} \
${EC_DATA} \
${EUC} \
${EXP} \
${GAS} \
${LIBRARY} \
${LOG_DATA} \
Expand All @@ -132,12 +134,12 @@ ZKEVM_MODULES := ${ALU} \
${TABLES} \
${TRM} \
${TXN_DATA} \
${EXP} \
${WCP}

# ${HUB} \
# ${STP} \


define.go: ${ZKEVM_MODULES}
${CORSET} wizard-iop -vv -o $@ ${ZKEVM_MODULES}

Expand Down
38 changes: 24 additions & 14 deletions txndata/constants.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,30 @@
(module txndata)

(defconst
NB_ROWS_TYPE_0 7
NB_ROWS_TYPE_1 8
NB_ROWS_TYPE_2 8
NB_ROWS_TYPE_0 8
NB_ROWS_TYPE_1 9
NB_ROWS_TYPE_2 9
;;
COMMON_RLP_TXN_PHASE_NUMBER_0 RLP_TXN_PHASE_RLP_PREFIX
COMMON_RLP_TXN_PHASE_NUMBER_1 RLP_TXN_PHASE_TO
COMMON_RLP_TXN_PHASE_NUMBER_2 RLP_TXN_PHASE_NONCE
COMMON_RLP_TXN_PHASE_NUMBER_3 RLP_TXN_PHASE_VALUE
COMMON_RLP_TXN_PHASE_NUMBER_4 RLP_TXN_PHASE_DATA
COMMON_RLP_TXN_PHASE_NUMBER_5 RLP_TXN_PHASE_GAS_LIMIT
TYPE_0_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_GAS_PRICE
TYPE_1_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_GAS_PRICE
TYPE_1_RLP_TXN_PHASE_NUMBER_7 RLP_TXN_PHASE_ACCESS_LIST
TYPE_2_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_MAX_FEE_PER_GAS
TYPE_2_RLP_TXN_PHASE_NUMBER_7 RLP_TXN_PHASE_ACCESS_LIST)
COMMON_RLP_TXN_PHASE_NUMBER_0 RLP_TXN_PHASE_RLP_PREFIX
COMMON_RLP_TXN_PHASE_NUMBER_1 RLP_TXN_PHASE_TO
COMMON_RLP_TXN_PHASE_NUMBER_2 RLP_TXN_PHASE_NONCE
COMMON_RLP_TXN_PHASE_NUMBER_3 RLP_TXN_PHASE_VALUE
COMMON_RLP_TXN_PHASE_NUMBER_4 RLP_TXN_PHASE_DATA
COMMON_RLP_TXN_PHASE_NUMBER_5 RLP_TXN_PHASE_GAS_LIMIT
TYPE_0_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_GAS_PRICE
TYPE_1_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_GAS_PRICE
TYPE_1_RLP_TXN_PHASE_NUMBER_7 RLP_TXN_PHASE_ACCESS_LIST
TYPE_2_RLP_TXN_PHASE_NUMBER_6 RLP_TXN_PHASE_MAX_FEE_PER_GAS
TYPE_2_RLP_TXN_PHASE_NUMBER_7 RLP_TXN_PHASE_ACCESS_LIST
;;
comparaison---nonce-row-offset 0
comparaison---initial-balance-row-offset 1
comparaison---sufficient-gas-row-offset 2
comparaison---upper-limit-refunds-row-offset 3
comparaison---effective-refund-row-offset 4
comparaison---detecting-empty-call-data-row-offset 5
comparaison---max-fee-and-basefee-row-offset 6
comparaison---maxfee-and-max-priority-fee-row-offset 7
comparaison---computing-effective-gas-price-row-offset 8)


64 changes: 39 additions & 25 deletions txndata/constraints.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,14 +286,21 @@
;; 2.9 Comparisons ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; row i
;; row i + comparaison---nonce-row-offset
(defun (nonce-check)
(begin (small-call-to-LT comparaison---nonce-row-offset
INITIAL_BALANCE
(+ (value) (* (max_fee) (gas_limit))))
(result-must-be-true nonce-row-offset)))

;; row i + comparaison---sufficient-gas-row-offset
(defun (sufficient_balance)
(begin (small-call-to-LT 0
(begin (small-call-to-LT comparaison---initial-balance-row-offset
INITIAL_BALANCE
(+ (value) (* (max_fee) (gas_limit))))
(result-must-be-false 0)))
(result-must-be-false comparaison---initial-balance-row-offset)))

;; row i + 1
;; row i + comparaison---sufficient-gas-row-offset
(defun (upfront_gas_cost_of_transaction)
(if-not-zero TYPE0
;; TYPE0 = 1
Expand All @@ -312,56 +319,63 @@
(* (num_keys) GAS_CONST_G_ACCESS_LIST_STORAGE)))

(defun (sufficient_gas_limit)
(begin (small-call-to-LT 1 (gas_limit) (upfront_gas_cost_of_transaction))
(result-must-be-false 1)))
(begin (small-call-to-LT comparaison---sufficient-gas-row-offset
(gas_limit)
(upfront_gas_cost_of_transaction))
(result-must-be-false comparaison---sufficient-gas-row-offset)))

;; row i + 2
;; row i + comparaison---upper-limit-refunds-row-offset
;; epsilon is the remainder in the euclidean division of [T_g - g'] by 2
(defun (execution-gas-cost)
(- (gas_limit) GAS_LEFTOVER))

(defun (upper_limit_for_refunds)
(begin (call-to-EUC 2 (execution-gas-cost) MAX_REFUND_QUOTIENT)))
(begin (call-to-EUC comparaison---upper-limit-refunds-row-offset (execution-gas-cost) MAX_REFUND_QUOTIENT)))

(defun (refund_limit)
(shift RES 2))
(shift RES comparaison---upper-limit-refunds-row-offset))

;; row i + 3
;; row i + comparaison---effective-refund-row-offset
(defun (effective_refund)
(small-call-to-LT 3 REF_CNT (refund_limit)))
(small-call-to-LT comparaison---effective-refund-row-offset REF_CNT (refund_limit)))

(defun (get_full_refund)
(force-bool (shift RES 3)))
(force-bool (shift RES comparaison---effective-refund-row-offset)))

;; row i + 4
;; row i + comparaison---detecting-empty-call-data-row-offset
(defun (is-zero-call-data)
(small-call-to-ISZERO 4 (data_size)))
(small-call-to-ISZERO comparaison---detecting-empty-call-data-row-offset (data_size)))

(defun (nonzero_data_size)
(force-bool (- 1 (shift RES 4))))
(force-bool (- 1 (shift RES comparaison---detecting-empty-call-data-row-offset))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; applicable only to type 2 transactions ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; row i + 5
;; row i + comparaison---max-fee-and-basefee-row-offset
(defun (type_2_comparing_max_fee_and_basefee)
(begin (small-call-to-LT 5 (max_fee) BASEFEE)
(result-must-be-false 5)))
(begin (small-call-to-LT comparaison---max-fee-and-basefee-row-offset (max_fee) BASEFEE)
(result-must-be-false comparaison---max-fee-and-basefee-row-offset)))

;; row i + 6
;; row i + comparaison---maxfee-and-max-priority-fee-row-offset
(defun (type_2_comparing_max_fee_and_max_priority_fee)
(begin (small-call-to-LT 6 (max_fee) (max_priority_fee))
(result-must-be-false 6)))
(begin (small-call-to-LT comparaison---maxfee-and-max-priority-fee-row-offset
(max_fee)
(max_priority_fee))
(result-must-be-false comparaison---maxfee-and-max-priority-fee-row-offset)))

;; row i + 7
;; row i + comparaison---computing-effective-gas-price-row-offset
(defun (type_2_computing_the_effective_gas_price)
(small-call-to-LT 7 (max_fee) (+ (max_priority_fee) BASEFEE)))
(small-call-to-LT comparaison---computing-effective-gas-price-row-offset
(max_fee)
(+ (max_priority_fee) BASEFEE)))

(defun (get_full_tip)
(force-bool (- 1 (shift RES 7))))
(force-bool (- 1 (shift RES comparaison---computing-effective-gas-price-row-offset))))

(defconstraint comparisons (:guard (first-row-trigger))
(begin (sufficient_balance)
(begin (nonce-check)
(sufficient_balance)
(sufficient_gas_limit)
(upper_limit_for_refunds)
(effective_refund)
Expand Down
Loading