From d490138d7e5fa23d9cdb9c6c383f97245cd1e1f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Sep 2024 16:14:54 +0200 Subject: [PATCH 1/4] fix: priority fee per gas --- txndata/constraints.lisp | 322 +++++++++++++++++++-------------------- 1 file changed, 160 insertions(+), 162 deletions(-) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index e9df170a..126db028 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -1,9 +1,9 @@ (module txndata) (defpurefun (if-not-eq A B then else) - (if-not-zero (- A B) - then - else)) + (if-not-zero (- A B) + then + else)) ;; sum of transaction type flags (defun (tx-type-sum) (force-bool (+ TYPE0 @@ -12,7 +12,7 @@ ;; constraint imposing that STAMP[i + 1] ∈ { STAMP[i], 1 + STAMP[i] } (defpurefun (stamp-progression STAMP) - (vanishes! (any! (will-remain-constant! STAMP) (will-inc! STAMP 1)))) + (vanishes! (any! (will-remain-constant! STAMP) (will-inc! STAMP 1)))) ;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -20,51 +20,51 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint first-row (:domain {0}) ;; "" - (vanishes! ABS)) +(defcontraint first-row (:domain {0}) ;; "" + (vanishes! ABS)) -(defconstraint padding-is-padding () - (if-zero ABS - (begin (debug (vanishes! CT)) - (vanishes! (weight_sum))))) ;;TODO: useless, but in the spec +(defcontraint padding-is-padding () + (if-zero ABS + (begin (debug (vanishes! CT)) + (vanishes! (weight_sum))))) ;;TODO: useless, but in the spec -(defconstraint padding () - (if-zero ABS - (begin (vanishes! CT) - (vanishes! (tx-type-sum))))) +(defcontraint padding () + (if-zero ABS + (begin (vanishes! CT) + (vanishes! (tx-type-sum))))) -(defconstraint abs-tx-num-increments () - (stamp-progression ABS)) +(defcontraint abs-tx-num-increments () + (stamp-progression ABS)) -(defconstraint new-stamp-reboot-ct () - (if-not-zero (will-remain-constant! ABS) - (vanishes! (next CT)))) +(defcontraint new-stamp-reboot-ct () + (if-not-zero (will-remain-constant! ABS) + (vanishes! (next CT)))) -(defconstraint transactions-have-a-single-type (:guard ABS) (eq! (tx-type-sum) 1)) +(defcontraint transactions-have-a-single-type (:guard ABS) (eq! (tx-type-sum) 1)) -(defconstraint counter-column-updates-type-0 (:guard TYPE0) - (if-eq-else CT (+ CT_MAX_TYPE_0 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) +(defcontraint counter-column-updates-type-0 (:guard TYPE0) + (if-eq-else CT (+ CT_MAX_TYPE_0 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) -(defconstraint counter-column-updates-type-1 (:guard TYPE1) - (if-eq-else CT (+ CT_MAX_TYPE_1 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) +(defcontraint counter-column-updates-type-1 (:guard TYPE1) + (if-eq-else CT (+ CT_MAX_TYPE_1 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) -(defconstraint counter-column-updates-type-2 (:guard TYPE2) - (if-eq-else CT (+ CT_MAX_TYPE_2 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) +(defcontraint counter-column-updates-type-2 (:guard TYPE2) + (if-eq-else CT (+ CT_MAX_TYPE_2 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) -(defconstraint final-row (:domain {-1}) ;; "" - (begin - (eq! ABS ABS_MAX) - (eq! REL REL_MAX) - (debug (eq! IS_LAST_TX_OF_BLOCK 1)) - (if-not-zero TYPE0 (eq! CT (+ CT_MAX_TYPE_0 1))) - (if-not-zero TYPE1 (eq! CT (+ CT_MAX_TYPE_1 1))) - (if-not-zero TYPE2 (eq! CT (+ CT_MAX_TYPE_2 1))))) +(defcontraint final-row (:domain {-1}) ;; "" + (begin + (eq! ABS ABS_MAX) + (eq! REL REL_MAX) + (debug (eq! IS_LAST_TX_OF_BLOCK 1)) + (if-not-zero TYPE0 (eq! CT (+ CT_MAX_TYPE_0 1))) + (if-not-zero TYPE1 (eq! CT (+ CT_MAX_TYPE_1 1))) + (if-not-zero TYPE2 (eq! CT (+ CT_MAX_TYPE_2 1))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -84,72 +84,72 @@ (* (^ 2 5) COPY_TXCD) (* (^ 2 6) STATUS_CODE))) ;; "" -(defconstraint constancies () - (begin - (transaction-constant FROM_HI) - (transaction-constant FROM_LO) - (transaction-constant NONCE) - (transaction-constant VALUE) - (transaction-constant GLIM) - (transaction-constant TO_HI) - (transaction-constant TO_LO) - (transaction-constant CALL_DATA_SIZE) - (transaction-constant INIT_CODE_SIZE) - (transaction-constant IGAS) - (transaction-constant PRIORITY_FEE_PER_GAS) - (transaction-constant GAS_PRICE) - (transaction-constant BASEFEE) - (transaction-constant COINBASE_HI) - (transaction-constant COINBASE_LO) - (transaction-constant CUM_GAS) - (transaction-constant CFI) - (transaction-constant GAS_LEFTOVER) - (transaction-constant REF_CNT) - (transaction-constant REFUND_EFFECTIVE) - (transaction-constant IBAL) - (transaction-constant BLK) - (transaction-constant REL) - (transaction-constant (weight_sum)))) +(defcontraint constancies () + (begin + (transaction-constant FROM_HI) + (transaction-constant FROM_LO) + (transaction-constant NONCE) + (transaction-constant VALUE) + (transaction-constant GLIM) + (transaction-constant TO_HI) + (transaction-constant TO_LO) + (transaction-constant CALL_DATA_SIZE) + (transaction-constant INIT_CODE_SIZE) + (transaction-constant IGAS) + (transaction-constant PRIORITY_FEE_PER_GAS) + (transaction-constant GAS_PRICE) + (transaction-constant BASEFEE) + (transaction-constant COINBASE_HI) + (transaction-constant COINBASE_LO) + (transaction-constant CUM_GAS) + (transaction-constant CFI) + (transaction-constant GAS_LEFTOVER) + (transaction-constant REF_CNT) + (transaction-constant REFUND_EFFECTIVE) + (transaction-constant IBAL) + (transaction-constant BLK) + (transaction-constant REL) + (transaction-constant (weight_sum)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 2.4 Batch numbers and transaction number ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint total-number-constancies () - (begin (if-not-zero ABS - (will-remain-constant! ABS_MAX) - ;; (begin (vanishes! ABS_MAX) - ;; (vanishes! BLK_MAX) - ;; (vanishes! REL_MAX) - ;; (vanishes! BLK) - ;; (vanishes! REL)) - ) - (if-not-zero (will-inc! BLK 1) - (will-remain-constant! REL_MAX)))) - -(defconstraint batch-num-increments () - (stamp-progression BLK)) - -(defconstraint batchNum-txNum-lexicographic () - (begin (if-zero ABS - (begin (vanishes! BLK) - (vanishes! REL) - (if-not-zero (will-remain-constant! ABS) - (begin (eq! (next BLK) 1) - (eq! (next REL) 1)))) - (if-not-zero (will-remain-constant! ABS) - (if-not-eq REL_MAX - REL - (begin (will-remain-constant! BLK) - (will-inc! REL 1)) - (begin (will-inc! BLK 1) - (will-eq! REL 1))))))) - -(defconstraint set-last-tx-of-block-flag (:guard ABS_TX_NUM) - (if-eq-else REL_TX_NUM REL_TX_NUM_MAX - (eq! IS_LAST_TX_OF_BLOCK 1) - (vanishes! IS_LAST_TX_OF_BLOCK))) +(defcontraint total-number-constancies () + (begin (if-not-zero ABS + (will-remain-constant! ABS_MAX) + ;; (begin (vanishes! ABS_MAX) + ;; (vanishes! BLK_MAX) + ;; (vanishes! REL_MAX) + ;; (vanishes! BLK) + ;; (vanishes! REL)) + ) + (if-not-zero (will-inc! BLK 1) + (will-remain-constant! REL_MAX)))) + +(defcontraint batch-num-increments () + (stamp-progression BLK)) + +(defcontraint batchNum-txNum-lexicographic () + (begin (if-zero ABS + (begin (vanishes! BLK) + (vanishes! REL) + (if-not-zero (will-remain-constant! ABS) + (begin (eq! (next BLK) 1) + (eq! (next REL) 1)))) + (if-not-zero (will-remain-constant! ABS) + (if-not-eq REL_MAX + REL + (begin (will-remain-constant! BLK) + (will-inc! REL 1)) + (begin (will-inc! BLK 1) + (will-eq! REL 1))))))) + +(defcontraint set-last-tx-of-block-flag (:guard ABS_TX_NUM) + (if-eq-else REL_TX_NUM REL_TX_NUM_MAX + (eq! IS_LAST_TX_OF_BLOCK 1) + (vanishes! IS_LAST_TX_OF_BLOCK))) ;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -216,10 +216,10 @@ (defun (first-row-of-new-transaction) (- ABS (prev ABS))) -(defconstraint verticalization (:guard (first-row-of-new-transaction)) - (begin (setting_phase_numbers) - (data_transfer) - (debug (vanishing_data_cells)))) +(defcontraint verticalization (:guard (first-row-of-new-transaction)) + (begin (setting_phase_numbers) + (data_transfer) + (debug (vanishing_data_cells)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -227,8 +227,8 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint euc-and-wcp-exclusivity () - (vanishes! (* EUC_FLAG WCP_FLAG))) +(defcontraint euc-and-wcp-exclusivity () + (vanishes! (* EUC_FLAG WCP_FLAG))) (defun (small-call-to-LT row arg1 arg2) (begin (eq! (shift WCP_FLAG row) 1) @@ -337,35 +337,33 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint setting-gas-init (:guard (first-row-of-new-transaction)) - (if-not-zero TYPE0 - (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (legacy_upfront_gas_cost))) - (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (access_upfront_gas_cost))))) +(defcontraint setting-gas-initially-available (:guard (first-row-of-new-transaction)) + (if-not-zero TYPE0 + (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (legacy_upfront_gas_cost))) + (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (access_upfront_gas_cost))))) -(defconstraint setting-gas-price (:guard (first-row-of-new-transaction)) - (if-zero TYPE2 - (eq! GAS_PRICE (gas_price)) - (if-not-zero (get_full_tip) - (eq! GAS_PRICE (+ BASEFEE (max_priority_fee))) - (eq! GAS_PRICE (max_fee))))) +(defcontraint setting-gas-price (:guard (first-row-of-new-transaction)) + (if-zero TYPE2 + (eq! GAS_PRICE (gas_price)) + (if-not-zero (get_full_tip) + (eq! GAS_PRICE (+ BASEFEE (max_priority_fee))) + (eq! GAS_PRICE (max_fee))))) -(defconstraint setting-priority-fee-per-gas (:guard (first-row-of-new-transaction)) - (if-zero TYPE2 - (eq! PRIORITY_FEE_PER_GAS (gas_price)) - (eq! PRIORITY_FEE_PER_GAS (- GAS_PRICE BASEFEE)))) +(defcontraint setting-priority-fee-per-gas (:guard (first-row-of-new-transaction)) + (eq! PRIORITY_FEE_PER_GAS (- GAS_PRICE BASEFEE))) -(defconstraint setting-refund-effective (:guard (first-row-of-new-transaction)) - (if-zero (get_full_refund) - (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER (refund_limit))) - (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER REFUND_COUNTER)))) +(defcontraint setting-refund-effective (:guard (first-row-of-new-transaction)) + (if-zero (get_full_refund) + (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER (refund_limit))) + (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER REFUND_COUNTER)))) -(defconstraint partially-setting-requires-evm (:guard (first-row-of-new-transaction)) - (if-not-zero IS_DEP - (eq! REQUIRES_EVM_EXECUTION (nonzero-data-size)))) +(defcontraint partially-setting-requires-evm-execution (:guard (first-row-of-new-transaction)) + (if-not-zero IS_DEP + (eq! REQUIRES_EVM_EXECUTION (nonzero-data-size)))) -(defconstraint setting-copy-txcd (:guard (first-row-of-new-transaction)) - (eq! COPY_TXCD - (* (- 1 IS_DEP) REQUIRES_EVM_EXECUTION (nonzero-data-size)))) +(defcontraint setting-copy-txcd (:guard (first-row-of-new-transaction)) + (eq! COPY_TXCD + (* (- 1 IS_DEP) REQUIRES_EVM_EXECUTION (nonzero-data-size)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -373,14 +371,14 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint verticalisation-rlp-txn-rcpt (:guard (first-row-of-new-transaction)) - (begin - (eq! PHASE_RLP_TXNRCPT RLP_RCPT_SUBPHASE_ID_TYPE) - (eq! OUTGOING_RLP_TXNRCPT (tx_type)) - (eq! (next PHASE_RLP_TXNRCPT) RLP_RCPT_SUBPHASE_ID_STATUS_CODE) - (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE) - (eq! (shift PHASE_RLP_TXNRCPT 2) RLP_RCPT_SUBPHASE_ID_CUMUL_GAS) - (eq! (shift OUTGOING_RLP_TXNRCPT 2) GAS_CUMULATIVE))) +(defcontraint verticalisation-rlp-txn-rcpt (:guard (first-row-of-new-transaction)) + (begin + (eq! PHASE_RLP_TXNRCPT RLP_RCPT_SUBPHASE_ID_TYPE) + (eq! OUTGOING_RLP_TXNRCPT (tx_type)) + (eq! (next PHASE_RLP_TXNRCPT) RLP_RCPT_SUBPHASE_ID_STATUS_CODE) + (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE) + (eq! (shift PHASE_RLP_TXNRCPT 2) RLP_RCPT_SUBPHASE_ID_CUMUL_GAS) + (eq! (shift OUTGOING_RLP_TXNRCPT 2) GAS_CUMULATIVE))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -388,27 +386,27 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint cumulative-gas () - (begin (if-zero ABS - (vanishes! GAS_CUMULATIVE)) - (if-not-zero (will-remain-constant! BLK) - ; BLK[i + 1] != BLK[i] - (eq! (next GAS_CUMULATIVE) - (next (- GAS_LIMIT REFUND_EFFECTIVE)))) - (if-not-zero (and (will-inc! BLK 1) (will-remain-constant! ABS)) - ; BLK[i + 1] != 1 + BLK[i] && ABS[i+1] != ABS[i] i.e. BLK[i + 1] == BLK[i] && ABS[i+1] == ABS[i] +1 - (eq! (next GAS_CUMULATIVE) - (+ GAS_CUMULATIVE - (next (- GAS_LIMIT REFUND_EFFECTIVE))))))) - -(defconstraint cumulative-gas-comparison (:guard IS_LAST_TX_OF_BLOCK) - (if-not-zero (- ABS_TX_NUM (prev ABS_TX_NUM)) - (if-zero TYPE0 - (begin (small-call-to-LEQ NB_ROWS_TYPE_1 - GAS_CUMULATIVE - BLOCK_GAS_LIMIT) - (result-must-be-true NB_ROWS_TYPE_1)) - (begin (small-call-to-LEQ NB_ROWS_TYPE_0 - GAS_CUMULATIVE - BLOCK_GAS_LIMIT) - (result-must-be-true NB_ROWS_TYPE_0))))) +(defcontraint cumulative-gas () + (begin (if-zero ABS + (vanishes! GAS_CUMULATIVE)) + (if-not-zero (will-remain-constant! BLK) + ; BLK[i + 1] != BLK[i] + (eq! (next GAS_CUMULATIVE) + (next (- GAS_LIMIT REFUND_EFFECTIVE)))) + (if-not-zero (and (will-inc! BLK 1) (will-remain-constant! ABS)) + ; BLK[i + 1] != 1 + BLK[i] && ABS[i+1] != ABS[i] i.e. BLK[i + 1] == BLK[i] && ABS[i+1] == ABS[i] +1 + (eq! (next GAS_CUMULATIVE) + (+ GAS_CUMULATIVE + (next (- GAS_LIMIT REFUND_EFFECTIVE))))))) + +(defcontraint cumulative-gas-comparison (:guard IS_LAST_TX_OF_BLOCK) + (if-not-zero (- ABS_TX_NUM (prev ABS_TX_NUM)) + (if-zero TYPE0 + (begin (small-call-to-LEQ NB_ROWS_TYPE_1 + GAS_CUMULATIVE + BLOCK_GAS_LIMIT) + (result-must-be-true NB_ROWS_TYPE_1)) + (begin (small-call-to-LEQ NB_ROWS_TYPE_0 + GAS_CUMULATIVE + BLOCK_GAS_LIMIT) + (result-must-be-true NB_ROWS_TYPE_0))))) From 6783d61e84eb979dde660837dd2cfdbe675b756d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Sep 2024 16:17:43 +0200 Subject: [PATCH 2/4] fix: typo --- txndata/constraints.lisp | 52 ++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index 126db028..a6df7bdf 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -20,44 +20,44 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint first-row (:domain {0}) ;; "" +(defconstraint first-row (:domain {0}) ;; "" (vanishes! ABS)) -(defcontraint padding-is-padding () +(defconstraint padding-is-padding () (if-zero ABS (begin (debug (vanishes! CT)) (vanishes! (weight_sum))))) ;;TODO: useless, but in the spec -(defcontraint padding () +(defconstraint padding () (if-zero ABS (begin (vanishes! CT) (vanishes! (tx-type-sum))))) -(defcontraint abs-tx-num-increments () +(defconstraint abs-tx-num-increments () (stamp-progression ABS)) -(defcontraint new-stamp-reboot-ct () +(defconstraint new-stamp-reboot-ct () (if-not-zero (will-remain-constant! ABS) (vanishes! (next CT)))) -(defcontraint transactions-have-a-single-type (:guard ABS) (eq! (tx-type-sum) 1)) +(defconstraint transactions-have-a-single-type (:guard ABS) (eq! (tx-type-sum) 1)) -(defcontraint counter-column-updates-type-0 (:guard TYPE0) +(defconstraint counter-column-updates-type-0 (:guard TYPE0) (if-eq-else CT (+ CT_MAX_TYPE_0 IS_LAST_TX_OF_BLOCK) (will-inc! ABS 1) (will-inc! CT 1))) -(defcontraint counter-column-updates-type-1 (:guard TYPE1) +(defconstraint counter-column-updates-type-1 (:guard TYPE1) (if-eq-else CT (+ CT_MAX_TYPE_1 IS_LAST_TX_OF_BLOCK) (will-inc! ABS 1) (will-inc! CT 1))) -(defcontraint counter-column-updates-type-2 (:guard TYPE2) +(defconstraint counter-column-updates-type-2 (:guard TYPE2) (if-eq-else CT (+ CT_MAX_TYPE_2 IS_LAST_TX_OF_BLOCK) (will-inc! ABS 1) (will-inc! CT 1))) -(defcontraint final-row (:domain {-1}) ;; "" +(defconstraint final-row (:domain {-1}) ;; "" (begin (eq! ABS ABS_MAX) (eq! REL REL_MAX) @@ -84,7 +84,7 @@ (* (^ 2 5) COPY_TXCD) (* (^ 2 6) STATUS_CODE))) ;; "" -(defcontraint constancies () +(defconstraint constancies () (begin (transaction-constant FROM_HI) (transaction-constant FROM_LO) @@ -116,7 +116,7 @@ ;; 2.4 Batch numbers and transaction number ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint total-number-constancies () +(defconstraint total-number-constancies () (begin (if-not-zero ABS (will-remain-constant! ABS_MAX) ;; (begin (vanishes! ABS_MAX) @@ -128,10 +128,10 @@ (if-not-zero (will-inc! BLK 1) (will-remain-constant! REL_MAX)))) -(defcontraint batch-num-increments () +(defconstraint batch-num-increments () (stamp-progression BLK)) -(defcontraint batchNum-txNum-lexicographic () +(defconstraint batchNum-txNum-lexicographic () (begin (if-zero ABS (begin (vanishes! BLK) (vanishes! REL) @@ -146,7 +146,7 @@ (begin (will-inc! BLK 1) (will-eq! REL 1))))))) -(defcontraint set-last-tx-of-block-flag (:guard ABS_TX_NUM) +(defconstraint set-last-tx-of-block-flag (:guard ABS_TX_NUM) (if-eq-else REL_TX_NUM REL_TX_NUM_MAX (eq! IS_LAST_TX_OF_BLOCK 1) (vanishes! IS_LAST_TX_OF_BLOCK))) @@ -216,7 +216,7 @@ (defun (first-row-of-new-transaction) (- ABS (prev ABS))) -(defcontraint verticalization (:guard (first-row-of-new-transaction)) +(defconstraint verticalization (:guard (first-row-of-new-transaction)) (begin (setting_phase_numbers) (data_transfer) (debug (vanishing_data_cells)))) @@ -227,7 +227,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint euc-and-wcp-exclusivity () +(defconstraint euc-and-wcp-exclusivity () (vanishes! (* EUC_FLAG WCP_FLAG))) (defun (small-call-to-LT row arg1 arg2) @@ -337,31 +337,31 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint setting-gas-initially-available (:guard (first-row-of-new-transaction)) +(defconstraint setting-gas-initially-available (:guard (first-row-of-new-transaction)) (if-not-zero TYPE0 (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (legacy_upfront_gas_cost))) (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (access_upfront_gas_cost))))) -(defcontraint setting-gas-price (:guard (first-row-of-new-transaction)) +(defconstraint setting-gas-price (:guard (first-row-of-new-transaction)) (if-zero TYPE2 (eq! GAS_PRICE (gas_price)) (if-not-zero (get_full_tip) (eq! GAS_PRICE (+ BASEFEE (max_priority_fee))) (eq! GAS_PRICE (max_fee))))) -(defcontraint setting-priority-fee-per-gas (:guard (first-row-of-new-transaction)) +(defconstraint setting-priority-fee-per-gas (:guard (first-row-of-new-transaction)) (eq! PRIORITY_FEE_PER_GAS (- GAS_PRICE BASEFEE))) -(defcontraint setting-refund-effective (:guard (first-row-of-new-transaction)) +(defconstraint setting-refund-effective (:guard (first-row-of-new-transaction)) (if-zero (get_full_refund) (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER (refund_limit))) (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER REFUND_COUNTER)))) -(defcontraint partially-setting-requires-evm-execution (:guard (first-row-of-new-transaction)) +(defconstraint partially-setting-requires-evm-execution (:guard (first-row-of-new-transaction)) (if-not-zero IS_DEP (eq! REQUIRES_EVM_EXECUTION (nonzero-data-size)))) -(defcontraint setting-copy-txcd (:guard (first-row-of-new-transaction)) +(defconstraint setting-copy-txcd (:guard (first-row-of-new-transaction)) (eq! COPY_TXCD (* (- 1 IS_DEP) REQUIRES_EVM_EXECUTION (nonzero-data-size)))) @@ -371,7 +371,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint verticalisation-rlp-txn-rcpt (:guard (first-row-of-new-transaction)) +(defconstraint verticalisation-rlp-txn-rcpt (:guard (first-row-of-new-transaction)) (begin (eq! PHASE_RLP_TXNRCPT RLP_RCPT_SUBPHASE_ID_TYPE) (eq! OUTGOING_RLP_TXNRCPT (tx_type)) @@ -386,7 +386,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defcontraint cumulative-gas () +(defconstraint cumulative-gas () (begin (if-zero ABS (vanishes! GAS_CUMULATIVE)) (if-not-zero (will-remain-constant! BLK) @@ -399,7 +399,7 @@ (+ GAS_CUMULATIVE (next (- GAS_LIMIT REFUND_EFFECTIVE))))))) -(defcontraint cumulative-gas-comparison (:guard IS_LAST_TX_OF_BLOCK) +(defconstraint cumulative-gas-comparison (:guard IS_LAST_TX_OF_BLOCK) (if-not-zero (- ABS_TX_NUM (prev ABS_TX_NUM)) (if-zero TYPE0 (begin (small-call-to-LEQ NB_ROWS_TYPE_1 From b7f7713f1c7e9ad88325b723348f1670c617133e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Sep 2024 16:26:49 +0200 Subject: [PATCH 3/4] renaming of constants --- txndata/constants.lisp | 18 +-- txndata/constraints.lisp | 288 +++++++++++++++++++-------------------- 2 files changed, 153 insertions(+), 153 deletions(-) diff --git a/txndata/constants.lisp b/txndata/constants.lisp index d2a247e6..351522e9 100644 --- a/txndata/constants.lisp +++ b/txndata/constants.lisp @@ -21,14 +21,14 @@ 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 ;; - comparison---nonce-row-offset 0 - comparison---initial-balance-row-offset 1 - comparison---sufficient-gas-row-offset 2 - comparison---upper-limit-refunds-row-offset 3 - comparison---effective-refund-row-offset 4 - comparison---detecting-empty-call-data-row-offset 5 - comparison---max-fee-and-basefee-row-offset 6 - comparison---maxfee-and-max-priority-fee-row-offset 7 - comparison---computing-effective-gas-price-row-offset 8) + row-offset---nonce-comparison 0 + row-offset---initial-balance-comparison 1 + row-offset---sufficient-gas-comparison 2 + row-offset---upper-limit-refunds-comparison 3 + row-offset---effective-refund-comparison 4 + row-offset---detecting-empty-call-data-comparison 5 + row-offset---max-fee-and-basefee-comparison 6 + row-offset---max-fee-and-max-priority-fee-comparison 7 + row-offset---computing-effective-gas-price-comparison 8) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index a6df7bdf..2daef328 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -21,50 +21,50 @@ ;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint first-row (:domain {0}) ;; "" - (vanishes! ABS)) + (vanishes! ABS)) (defconstraint padding-is-padding () - (if-zero ABS - (begin (debug (vanishes! CT)) - (vanishes! (weight_sum))))) ;;TODO: useless, but in the spec + (if-zero ABS + (begin (debug (vanishes! CT)) + (vanishes! (weight_sum))))) ;;TODO: useless, but in the spec (defconstraint padding () - (if-zero ABS - (begin (vanishes! CT) - (vanishes! (tx-type-sum))))) + (if-zero ABS + (begin (vanishes! CT) + (vanishes! (tx-type-sum))))) (defconstraint abs-tx-num-increments () - (stamp-progression ABS)) + (stamp-progression ABS)) (defconstraint new-stamp-reboot-ct () - (if-not-zero (will-remain-constant! ABS) - (vanishes! (next CT)))) + (if-not-zero (will-remain-constant! ABS) + (vanishes! (next CT)))) (defconstraint transactions-have-a-single-type (:guard ABS) (eq! (tx-type-sum) 1)) (defconstraint counter-column-updates-type-0 (:guard TYPE0) - (if-eq-else CT (+ CT_MAX_TYPE_0 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) + (if-eq-else CT (+ CT_MAX_TYPE_0 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) (defconstraint counter-column-updates-type-1 (:guard TYPE1) - (if-eq-else CT (+ CT_MAX_TYPE_1 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) + (if-eq-else CT (+ CT_MAX_TYPE_1 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) (defconstraint counter-column-updates-type-2 (:guard TYPE2) - (if-eq-else CT (+ CT_MAX_TYPE_2 IS_LAST_TX_OF_BLOCK) - (will-inc! ABS 1) - (will-inc! CT 1))) + (if-eq-else CT (+ CT_MAX_TYPE_2 IS_LAST_TX_OF_BLOCK) + (will-inc! ABS 1) + (will-inc! CT 1))) (defconstraint final-row (:domain {-1}) ;; "" - (begin - (eq! ABS ABS_MAX) - (eq! REL REL_MAX) - (debug (eq! IS_LAST_TX_OF_BLOCK 1)) - (if-not-zero TYPE0 (eq! CT (+ CT_MAX_TYPE_0 1))) - (if-not-zero TYPE1 (eq! CT (+ CT_MAX_TYPE_1 1))) - (if-not-zero TYPE2 (eq! CT (+ CT_MAX_TYPE_2 1))))) + (begin + (eq! ABS ABS_MAX) + (eq! REL REL_MAX) + (debug (eq! IS_LAST_TX_OF_BLOCK 1)) + (if-not-zero TYPE0 (eq! CT (+ CT_MAX_TYPE_0 1))) + (if-not-zero TYPE1 (eq! CT (+ CT_MAX_TYPE_1 1))) + (if-not-zero TYPE2 (eq! CT (+ CT_MAX_TYPE_2 1))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -85,31 +85,31 @@ (* (^ 2 6) STATUS_CODE))) ;; "" (defconstraint constancies () - (begin - (transaction-constant FROM_HI) - (transaction-constant FROM_LO) - (transaction-constant NONCE) - (transaction-constant VALUE) - (transaction-constant GLIM) - (transaction-constant TO_HI) - (transaction-constant TO_LO) - (transaction-constant CALL_DATA_SIZE) - (transaction-constant INIT_CODE_SIZE) - (transaction-constant IGAS) - (transaction-constant PRIORITY_FEE_PER_GAS) - (transaction-constant GAS_PRICE) - (transaction-constant BASEFEE) - (transaction-constant COINBASE_HI) - (transaction-constant COINBASE_LO) - (transaction-constant CUM_GAS) - (transaction-constant CFI) - (transaction-constant GAS_LEFTOVER) - (transaction-constant REF_CNT) - (transaction-constant REFUND_EFFECTIVE) - (transaction-constant IBAL) - (transaction-constant BLK) - (transaction-constant REL) - (transaction-constant (weight_sum)))) + (begin + (transaction-constant FROM_HI) + (transaction-constant FROM_LO) + (transaction-constant NONCE) + (transaction-constant VALUE) + (transaction-constant GLIM) + (transaction-constant TO_HI) + (transaction-constant TO_LO) + (transaction-constant CALL_DATA_SIZE) + (transaction-constant INIT_CODE_SIZE) + (transaction-constant IGAS) + (transaction-constant PRIORITY_FEE_PER_GAS) + (transaction-constant GAS_PRICE) + (transaction-constant BASEFEE) + (transaction-constant COINBASE_HI) + (transaction-constant COINBASE_LO) + (transaction-constant CUM_GAS) + (transaction-constant CFI) + (transaction-constant GAS_LEFTOVER) + (transaction-constant REF_CNT) + (transaction-constant REFUND_EFFECTIVE) + (transaction-constant IBAL) + (transaction-constant BLK) + (transaction-constant REL) + (transaction-constant (weight_sum)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -117,39 +117,39 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint total-number-constancies () - (begin (if-not-zero ABS - (will-remain-constant! ABS_MAX) - ;; (begin (vanishes! ABS_MAX) - ;; (vanishes! BLK_MAX) - ;; (vanishes! REL_MAX) - ;; (vanishes! BLK) - ;; (vanishes! REL)) - ) - (if-not-zero (will-inc! BLK 1) - (will-remain-constant! REL_MAX)))) + (begin (if-not-zero ABS + (will-remain-constant! ABS_MAX) + ;; (begin (vanishes! ABS_MAX) + ;; (vanishes! BLK_MAX) + ;; (vanishes! REL_MAX) + ;; (vanishes! BLK) + ;; (vanishes! REL)) + ) + (if-not-zero (will-inc! BLK 1) + (will-remain-constant! REL_MAX)))) (defconstraint batch-num-increments () - (stamp-progression BLK)) + (stamp-progression BLK)) (defconstraint batchNum-txNum-lexicographic () - (begin (if-zero ABS - (begin (vanishes! BLK) - (vanishes! REL) - (if-not-zero (will-remain-constant! ABS) - (begin (eq! (next BLK) 1) - (eq! (next REL) 1)))) - (if-not-zero (will-remain-constant! ABS) - (if-not-eq REL_MAX - REL - (begin (will-remain-constant! BLK) - (will-inc! REL 1)) - (begin (will-inc! BLK 1) - (will-eq! REL 1))))))) + (begin (if-zero ABS + (begin (vanishes! BLK) + (vanishes! REL) + (if-not-zero (will-remain-constant! ABS) + (begin (eq! (next BLK) 1) + (eq! (next REL) 1)))) + (if-not-zero (will-remain-constant! ABS) + (if-not-eq REL_MAX + REL + (begin (will-remain-constant! BLK) + (will-inc! REL 1)) + (begin (will-inc! BLK 1) + (will-eq! REL 1))))))) (defconstraint set-last-tx-of-block-flag (:guard ABS_TX_NUM) - (if-eq-else REL_TX_NUM REL_TX_NUM_MAX - (eq! IS_LAST_TX_OF_BLOCK 1) - (vanishes! IS_LAST_TX_OF_BLOCK))) + (if-eq-else REL_TX_NUM REL_TX_NUM_MAX + (eq! IS_LAST_TX_OF_BLOCK 1) + (vanishes! IS_LAST_TX_OF_BLOCK))) ;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -217,9 +217,9 @@ (- ABS (prev ABS))) (defconstraint verticalization (:guard (first-row-of-new-transaction)) - (begin (setting_phase_numbers) - (data_transfer) - (debug (vanishing_data_cells)))) + (begin (setting_phase_numbers) + (data_transfer) + (debug (vanishing_data_cells)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -228,7 +228,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint euc-and-wcp-exclusivity () - (vanishes! (* EUC_FLAG WCP_FLAG))) + (vanishes! (* EUC_FLAG WCP_FLAG))) (defun (small-call-to-LT row arg1 arg2) (begin (eq! (shift WCP_FLAG row) 1) @@ -264,13 +264,13 @@ (defconstraint comparison---nonce-must-not-exceed-EIP-2681-max-nonce (:guard (first-row-of-new-transaction)) (begin - (small-call-to-LT comparison---nonce-row-offset NONCE EIP2681_MAX_NONCE) - (result-must-be-true comparison---nonce-row-offset))) + (small-call-to-LT row-offset---nonce-comparison NONCE EIP2681_MAX_NONCE) + (result-must-be-true row-offset---nonce-comparison))) (defconstraint comparison---initial-balance-must-cover-value-plus-maximal-gas-cost (:guard (first-row-of-new-transaction)) (begin - (small-call-to-LEQ comparison---initial-balance-row-offset INITIAL_BALANCE (+ (value) (* (max_fee) (gas_limit)))) - (result-must-be-true comparison---initial-balance-row-offset))) + (small-call-to-LEQ row-offset---initial-balance-comparison INITIAL_BALANCE (+ (value) (* (max_fee) (gas_limit)))) + (result-must-be-true row-offset---initial-balance-comparison))) (defun (upfront_gas_cost) (+ (* TYPE0 (legacy_upfront_gas_cost)) @@ -289,30 +289,30 @@ (defconstraint comparison---gas-limit-must-cover-upfront-gas-cost (:guard (first-row-of-new-transaction)) (begin - (small-call-to-LEQ comparison---sufficient-gas-row-offset (upfront_gas_cost) (gas_limit)) - (result-must-be-true comparison---sufficient-gas-row-offset))) + (small-call-to-LEQ row-offset---sufficient-gas-comparison (upfront_gas_cost) (gas_limit)) + (result-must-be-true row-offset---sufficient-gas-comparison))) (defconstraint integer-division---compute-upper-limit-for-refunds (:guard (first-row-of-new-transaction)) (begin - (call-to-EUC comparison---upper-limit-refunds-row-offset (execution_gas_cost) MAX_REFUND_QUOTIENT))) + (call-to-EUC row-offset---upper-limit-refunds-comparison (execution_gas_cost) MAX_REFUND_QUOTIENT))) (defun (execution_gas_cost) (- (gas_limit) GAS_LEFTOVER)) -(defun (refund_limit) (shift RES comparison---upper-limit-refunds-row-offset)) +(defun (refund_limit) (shift RES row-offset---upper-limit-refunds-comparison)) (defconstraint comparison---final-refund-counter-vs-refund-limit (:guard (first-row-of-new-transaction)) - (small-call-to-LT comparison---effective-refund-row-offset REF_CNT (refund_limit))) + (small-call-to-LT row-offset---effective-refund-comparison REF_CNT (refund_limit))) -(defun (get_full_refund) (force-bool (shift RES comparison---effective-refund-row-offset))) +(defun (get_full_refund) (force-bool (shift RES row-offset---effective-refund-comparison))) (defconstraint comparison---detect-empty-data-in-transaction (:guard (first-row-of-new-transaction)) - (small-call-to-ISZERO comparison---detecting-empty-call-data-row-offset (data_size))) + (small-call-to-ISZERO row-offset---detecting-empty-call-data-comparison (data_size))) -(defun (nonzero-data-size) (force-bool (- 1 (shift RES comparison---detecting-empty-call-data-row-offset)))) +(defun (nonzero-data-size) (force-bool (- 1 (shift RES row-offset---detecting-empty-call-data-comparison)))) (defconstraint comparison---comparing-the-maximum-gas-price-against-the-basefee (:guard (first-row-of-new-transaction)) (begin - (small-call-to-LEQ comparison---max-fee-and-basefee-row-offset BASEFEE (maximal_gas_price)) - (result-must-be-true comparison---max-fee-and-basefee-row-offset))) + (small-call-to-LEQ row-offset---max-fee-and-basefee-comparison BASEFEE (maximal_gas_price)) + (result-must-be-true row-offset---max-fee-and-basefee-comparison))) (defun (maximal_gas_price) (+ (* TYPE0 (gas_price)) (* TYPE1 (gas_price)) @@ -323,13 +323,13 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint comparison-for-type-2---comparing-max-fee-and-max-priority-fee (:guard (* (first-row-of-new-transaction) TYPE2)) - (begin (small-call-to-LEQ comparison---maxfee-and-max-priority-fee-row-offset (max_priority_fee) (max_fee)) - (result-must-be-true comparison---maxfee-and-max-priority-fee-row-offset))) + (begin (small-call-to-LEQ row-offset---max-fee-and-max-priority-fee-comparison (max_priority_fee) (max_fee)) + (result-must-be-true row-offset---max-fee-and-max-priority-fee-comparison))) (defconstraint comparison-for-type-2---computing-the-effective-gas-price (:guard (* (first-row-of-new-transaction) TYPE2)) - (small-call-to-LEQ comparison---computing-effective-gas-price-row-offset (+ (max_priority_fee) BASEFEE) (max_fee))) + (small-call-to-LEQ row-offset---computing-effective-gas-price-comparison (+ (max_priority_fee) BASEFEE) (max_fee))) -(defun (get_full_tip) (force-bool (shift RES comparison---computing-effective-gas-price-row-offset))) +(defun (get_full_tip) (force-bool (shift RES row-offset---computing-effective-gas-price-comparison))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -338,32 +338,32 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint setting-gas-initially-available (:guard (first-row-of-new-transaction)) - (if-not-zero TYPE0 - (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (legacy_upfront_gas_cost))) - (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (access_upfront_gas_cost))))) + (if-not-zero TYPE0 + (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (legacy_upfront_gas_cost))) + (eq! GAS_INITIALLY_AVAILABLE (- (gas_limit) (access_upfront_gas_cost))))) (defconstraint setting-gas-price (:guard (first-row-of-new-transaction)) - (if-zero TYPE2 - (eq! GAS_PRICE (gas_price)) - (if-not-zero (get_full_tip) - (eq! GAS_PRICE (+ BASEFEE (max_priority_fee))) - (eq! GAS_PRICE (max_fee))))) + (if-zero TYPE2 + (eq! GAS_PRICE (gas_price)) + (if-not-zero (get_full_tip) + (eq! GAS_PRICE (+ BASEFEE (max_priority_fee))) + (eq! GAS_PRICE (max_fee))))) (defconstraint setting-priority-fee-per-gas (:guard (first-row-of-new-transaction)) - (eq! PRIORITY_FEE_PER_GAS (- GAS_PRICE BASEFEE))) + (eq! PRIORITY_FEE_PER_GAS (- GAS_PRICE BASEFEE))) (defconstraint setting-refund-effective (:guard (first-row-of-new-transaction)) - (if-zero (get_full_refund) - (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER (refund_limit))) - (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER REFUND_COUNTER)))) + (if-zero (get_full_refund) + (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER (refund_limit))) + (eq! REFUND_EFFECTIVE (+ GAS_LEFTOVER REFUND_COUNTER)))) (defconstraint partially-setting-requires-evm-execution (:guard (first-row-of-new-transaction)) - (if-not-zero IS_DEP - (eq! REQUIRES_EVM_EXECUTION (nonzero-data-size)))) + (if-not-zero IS_DEP + (eq! REQUIRES_EVM_EXECUTION (nonzero-data-size)))) (defconstraint setting-copy-txcd (:guard (first-row-of-new-transaction)) - (eq! COPY_TXCD - (* (- 1 IS_DEP) REQUIRES_EVM_EXECUTION (nonzero-data-size)))) + (eq! COPY_TXCD + (* (- 1 IS_DEP) REQUIRES_EVM_EXECUTION (nonzero-data-size)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -372,13 +372,13 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint verticalisation-rlp-txn-rcpt (:guard (first-row-of-new-transaction)) - (begin - (eq! PHASE_RLP_TXNRCPT RLP_RCPT_SUBPHASE_ID_TYPE) - (eq! OUTGOING_RLP_TXNRCPT (tx_type)) - (eq! (next PHASE_RLP_TXNRCPT) RLP_RCPT_SUBPHASE_ID_STATUS_CODE) - (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE) - (eq! (shift PHASE_RLP_TXNRCPT 2) RLP_RCPT_SUBPHASE_ID_CUMUL_GAS) - (eq! (shift OUTGOING_RLP_TXNRCPT 2) GAS_CUMULATIVE))) + (begin + (eq! PHASE_RLP_TXNRCPT RLP_RCPT_SUBPHASE_ID_TYPE) + (eq! OUTGOING_RLP_TXNRCPT (tx_type)) + (eq! (next PHASE_RLP_TXNRCPT) RLP_RCPT_SUBPHASE_ID_STATUS_CODE) + (eq! (next OUTGOING_RLP_TXNRCPT) STATUS_CODE) + (eq! (shift PHASE_RLP_TXNRCPT 2) RLP_RCPT_SUBPHASE_ID_CUMUL_GAS) + (eq! (shift OUTGOING_RLP_TXNRCPT 2) GAS_CUMULATIVE))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -387,26 +387,26 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint cumulative-gas () - (begin (if-zero ABS - (vanishes! GAS_CUMULATIVE)) - (if-not-zero (will-remain-constant! BLK) - ; BLK[i + 1] != BLK[i] - (eq! (next GAS_CUMULATIVE) - (next (- GAS_LIMIT REFUND_EFFECTIVE)))) - (if-not-zero (and (will-inc! BLK 1) (will-remain-constant! ABS)) - ; BLK[i + 1] != 1 + BLK[i] && ABS[i+1] != ABS[i] i.e. BLK[i + 1] == BLK[i] && ABS[i+1] == ABS[i] +1 - (eq! (next GAS_CUMULATIVE) - (+ GAS_CUMULATIVE - (next (- GAS_LIMIT REFUND_EFFECTIVE))))))) + (begin (if-zero ABS + (vanishes! GAS_CUMULATIVE)) + (if-not-zero (will-remain-constant! BLK) + ; BLK[i + 1] != BLK[i] + (eq! (next GAS_CUMULATIVE) + (next (- GAS_LIMIT REFUND_EFFECTIVE)))) + (if-not-zero (and (will-inc! BLK 1) (will-remain-constant! ABS)) + ; BLK[i + 1] != 1 + BLK[i] && ABS[i+1] != ABS[i] i.e. BLK[i + 1] == BLK[i] && ABS[i+1] == ABS[i] +1 + (eq! (next GAS_CUMULATIVE) + (+ GAS_CUMULATIVE + (next (- GAS_LIMIT REFUND_EFFECTIVE))))))) (defconstraint cumulative-gas-comparison (:guard IS_LAST_TX_OF_BLOCK) - (if-not-zero (- ABS_TX_NUM (prev ABS_TX_NUM)) - (if-zero TYPE0 - (begin (small-call-to-LEQ NB_ROWS_TYPE_1 - GAS_CUMULATIVE - BLOCK_GAS_LIMIT) - (result-must-be-true NB_ROWS_TYPE_1)) - (begin (small-call-to-LEQ NB_ROWS_TYPE_0 - GAS_CUMULATIVE - BLOCK_GAS_LIMIT) - (result-must-be-true NB_ROWS_TYPE_0))))) + (if-not-zero (- ABS_TX_NUM (prev ABS_TX_NUM)) + (if-zero TYPE0 + (begin (small-call-to-LEQ NB_ROWS_TYPE_1 + GAS_CUMULATIVE + BLOCK_GAS_LIMIT) + (result-must-be-true NB_ROWS_TYPE_1)) + (begin (small-call-to-LEQ NB_ROWS_TYPE_0 + GAS_CUMULATIVE + BLOCK_GAS_LIMIT) + (result-must-be-true NB_ROWS_TYPE_0))))) From d051fea7939024ee55f1b7b516ec6a3bca4fe1e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Sep 2024 18:17:11 +0200 Subject: [PATCH 4/4] fix(typo) --- txndata/constraints.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index 2daef328..9d315e85 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -269,7 +269,7 @@ (defconstraint comparison---initial-balance-must-cover-value-plus-maximal-gas-cost (:guard (first-row-of-new-transaction)) (begin - (small-call-to-LEQ row-offset---initial-balance-comparison INITIAL_BALANCE (+ (value) (* (max_fee) (gas_limit)))) + (small-call-to-LEQ row-offset---initial-balance-comparison (+ (value) (* (max_fee) (gas_limit))) INITIAL_BALANCE) (result-must-be-true row-offset---initial-balance-comparison))) (defun (upfront_gas_cost)