Skip to content

Commit

Permalink
Implementation of TX_INIT and TX_FINL fix (#517)
Browse files Browse the repository at this point in the history
  • Loading branch information
@OlivierBBB
OlivierBBB authored Jan 10, 2025
1 parent b644a39 commit 05aa1c6
Show file tree
Hide file tree
Showing 27 changed files with 670 additions and 281 deletions.
4 changes: 3 additions & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,9 @@ HUB := $(wildcard hub/columns/*lisp) \
$(wildcard hub/constraints/tx_skip/*lisp) \
$(wildcard hub/constraints/tx_prewarm/*lisp) \
$(wildcard hub/constraints/tx_init/*lisp) \
$(wildcard hub/constraints/tx_init/rows/*lisp) \
$(wildcard hub/constraints/tx_finl/*lisp) \
$(wildcard hub/constraints/tx_finl/rows/*lisp) \
$(wildcard hub/constraints/*lisp) \
$(wildcard hub/lookups/*lisp) \
hub/constants.lisp
Expand Down Expand Up @@ -142,7 +144,7 @@ ZKEVM_MODULES := ${ALU} \
${EUC} \
${EXP} \
${GAS} \
${HUB_COLUMNS} \
${HUB} \
${LIBRARY} \
${LOG_DATA} \
${LOG_INFO} \
Expand Down
10 changes: 5 additions & 5 deletions blockdata/columns.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,19 @@
(INST :byte :display :opcode)
(COINBASE_HI :i32)
(COINBASE_LO :i128)
(BLOCK_GAS_LIMIT :i48)
(BASEFEE :i48)
(BLOCK_GAS_LIMIT :i64)
(BASEFEE :i64)
(FIRST_BLOCK_NUMBER :i48)
(REL_BLOCK :i8)
(REL_TX_NUM_MAX :i10)
(REL_BLOCK :i16)
(REL_TX_NUM_MAX :i16)
(DATA_HI :i128)
(DATA_LO :i128)
(ARG_1_HI :i128)
(ARG_1_LO :i128)
(ARG_2_HI :i128)
(ARG_2_LO :i128)
(RES :i128)
(EXO_INST :byte)
(EXO_INST :byte :display :opcode)
(WCP_FLAG :binary@prove)
(EUC_FLAG :binary@prove)
)
Expand Down
2 changes: 1 addition & 1 deletion constants/constants.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@
LINEA_DIFFICULTY 2
LINEA_MAX_NUMBER_OF_TRANSACTIONS_IN_BATCH 200
ETHEREUM_GAS_LIMIT_MINIMUM 5000
ETHEREUM_GAS_LIMIT_MAXIMUM 0xffffffffffffffffffffffffffffffff ;; maxUint64
ETHEREUM_GAS_LIMIT_MAXIMUM 0xffffffffffffffff ;; maxUint64
LINEA_GAS_LIMIT_MINIMUM 61000000
LINEA_GAS_LIMIT_MAXIMUM 2000000000
GAS_LIMIT_ADJUSTMENT_FACTOR 1024
Expand Down
2 changes: 1 addition & 1 deletion hub/columns/stack.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
( STACK_ITEM_STAMP :array [4] :i36) ;; STAMP is :i32 and we consider 8 * STAMP + bla with 0 ≤ bla < 8

;; instruction and instruction decoded flags
( INSTRUCTION :display :opcode)
( INSTRUCTION :byte :display :opcode)
( STATIC_GAS :i32 ) ;; TODO: vastly exagerated, shouldn't carry values greater than 32_000 so :i16 should suffice)
( ACC_FLAG :binary )
( ADD_FLAG :binary )
Expand Down
7 changes: 4 additions & 3 deletions hub/constants.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@

(defconst
MULTIPLIER___STACK_STAMP 8 ;; \hubTau
MULTIPLIER___DOM_SUB_STAMPS 8 ;; \hubLambda
DOM_SUB_STAMP_OFFSET___REVERT 6 ;; \revertEpsilon
DOM_SUB_STAMP_OFFSET___SELFDESTRUCT 7 ;; \selfdestructEpsilon
MULTIPLIER___DOM_SUB_STAMPS 16 ;; \hubLambda
DOM_SUB_STAMP_OFFSET___REVERT 8 ;; \revertEpsilon
DOM_SUB_STAMP_OFFSET___FINALIZATION 9 ;; \finalizationEpsilon
DOM_SUB_STAMP_OFFSET___SELFDESTRUCT 10 ;; \selfdestructEpsilon
)
9 changes: 8 additions & 1 deletion hub/constraints/generalities/revert_data_specific.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (self_revert_trigger) (- (+ XAHOY (* stack/HALT_FLAG [stack/DEC_FLAG 2]))
(* XAHOY stack/HALT_FLAG [stack/DEC_FLAG 2])))
(* XAHOY stack/HALT_FLAG [stack/DEC_FLAG 2]))) ;; ""

(defconstraint recording-self-induced-revert (:perspective stack)
(if-not-zero (force-bool (self_revert_trigger))
Expand Down Expand Up @@ -112,6 +112,13 @@
sub_stamp_offset
))

;; (defun (DOM-SUB-stamps---finalization rel_offset
;; sub_offset)
;; (undoing-dom-sub-stamps rel_offset
;; TX_END_STAMP
;; DOM_SUB_STAMP_OFFSET___FINALIZATION
;; sub_offset))

(defun (selfdestruct-dom-sub-stamps relOffset) (undoing-dom-sub-stamps
relOffset
TX_END_STAMP
Expand Down
10 changes: 9 additions & 1 deletion hub/constraints/heartbeat/hub_stamp.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,15 @@
(will-inc! HUB_STAMP 1))))

(defconstraint heartbeat---hub-stamp---constancy-during-skipping-phase ()
(if-not-zero (+ TX_SKIP TX_INIT TX_FINL)
(if-not-zero TX_SKIP
(will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION))))

(defconstraint heartbeat---hub-stamp---constancy-during-initialization-phase ()
(if-not-zero TX_INIT
(will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_CONTEXT))))

(defconstraint heartbeat---hub-stamp---constancy-during-finalization-phase ()
(if-not-zero TX_FINL
(will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION))))

(defconstraint heartbeat---hub-stamp---jumps-at-transaction-boundaries ()
Expand Down
2 changes: 1 addition & 1 deletion hub/constraints/heartbeat/transaction_phase_flags.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@
(if-not-zero TX_WARM
(eq! (next (+ TX_WARM TX_INIT)) 1))
(if-not-zero TX_INIT
(if-zero PEEK_AT_TRANSACTION
(if-zero PEEK_AT_CONTEXT
(eq! (next TX_INIT) 1)
(eq! (next TX_EXEC) 1)))
(if-not-zero TX_EXEC
Expand Down
105 changes: 69 additions & 36 deletions hub/constraints/instruction-handling/sto.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,14 @@
(defun (storage-instruction---value-to-store-lo) [ stack/STACK_ITEM_VALUE_LO 4 ])
(defun (storage-instruction---OOB-prediction-of-sstorex) (shift [ misc/OOB_DATA 7 ] 2)) ;; ""

(defconstraint storage-instruction---stack-pattern (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---stack-pattern
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(load-store-stack-pattern (storage-instruction---is-SSTORE)))

(defconstraint storage-instruction---valid-exceptions (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---valid-exceptions
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(begin
(if-not-zero (storage-instruction---is-SLOAD)
(eq! XAHOY stack/OOGX))
Expand All @@ -24,7 +28,9 @@
stack/SSTOREX
stack/OOGX)))))

(defconstraint storage-instruction---setting-NSR-and-peeking-flags-STATICX (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-NSR-and-peeking-flags-STATICX
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; static exception
;;;;;;;;;;;;;;;;;;;
(if-not-zero stack/STATICX
Expand All @@ -34,7 +40,9 @@
(+ (shift PEEK_AT_CONTEXT 1)
(shift PEEK_AT_CONTEXT 2))))))

(defconstraint storage-instruction---setting-NSR-and-peeking-flags-SSTOREX (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-NSR-and-peeking-flags-SSTOREX
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; sstore gas exception
;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero stack/SSTOREX
Expand All @@ -45,7 +53,9 @@
(shift PEEK_AT_MISCELLANEOUS 2)
(shift PEEK_AT_CONTEXT 3))))))

(defconstraint storage-instruction---setting-NSR-and-peeking-flags-OOGX (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-NSR-and-peeking-flags-OOGX
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; out of gas exception
;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero stack/OOGX
Expand All @@ -58,7 +68,9 @@
(shift PEEK_AT_STORAGE 4)
(shift PEEK_AT_CONTEXT 5))))))

(defconstraint storage-instruction---setting-NSR-and-peeking-flags-UNEXCEPTIONAL (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-NSR-and-peeking-flags-UNEXCEPTIONAL
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; unexceptional
;;;;;;;;;;;;;;;;
(if-zero XAHOY
Expand All @@ -70,16 +82,22 @@
(shift PEEK_AT_STORAGE 3)
(* CONTEXT_WILL_REVERT (shift PEEK_AT_STORAGE 4)))))))

(defconstraint storage-instruction---first-context-row (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---first-context-row
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(read-context-data 1 ;; row offset
CONTEXT_NUMBER )) ;; context to read

(defconstraint storage-instruction---justifying-STATICX (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---justifying-STATICX
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! stack/STATICX
(* (storage-instruction---is-SSTORE)
(shift context/IS_STATIC 1))))

(defconstraint storage-instruction---setting-MISC-row (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-MISC-row
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (shift PEEK_AT_MISCELLANEOUS 2)
(begin
(eq! (weighted-MISC-flag-sum 2)
Expand All @@ -89,15 +107,20 @@
GAS_ACTUAL )) ;; GAS_ACTUAL
)))

(defconstraint storage-instruction---justifying-SSTOREX (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---justifying-SSTOREX
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (shift PEEK_AT_MISCELLANEOUS 2)
(if-not-zero (storage-instruction---is-SSTORE)
(eq! stack/SSTOREX
(storage-instruction---OOB-prediction-of-sstorex)))))

(defun (oogx-or-no-exception) (+ stack/OOGX (- 1 XAHOY)))
(defun (no-exception) (- 1 XAHOY))
(defun (oogx-or-no-exception) (+ stack/OOGX (no-exception)))

(defconstraint storage-instruction---setting-storage-slot-parameters (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-storage-slot-parameters
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (oogx-or-no-exception)
(begin
(eq! (shift storage/ADDRESS_HI 3) (shift context/ACCOUNT_ADDRESS_HI 1))
Expand All @@ -109,29 +132,37 @@
(DOM-SUB-stamps---standard 3 ;; kappa
0)))) ;; c

(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SLOAD (:guard (storage-instruction---no-stack-exceptions))
(if-not-zero (oogx-or-no-exception)
(if-not-zero (force-bin (storage-instruction---is-SLOAD))
(begin
(storage-reading 3)
(eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3))
(eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3))))))

(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SSTORE (:guard (storage-instruction---no-stack-exceptions))
(if-not-zero (oogx-or-no-exception)
(if-not-zero (force-bin (storage-instruction---is-SSTORE))
(begin
(eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3))
(eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3))))))
(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SLOAD
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (storage-instruction---is-SLOAD)
(begin
(if-not-zero (oogx-or-no-exception)
(storage-reading 3))
(if-not-zero (no-exception)
(begin
(eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3))
(eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3)))))))

(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SSTORE
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (storage-instruction---is-SSTORE)
(if-not-zero (oogx-or-no-exception)
(begin
(eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3))
(eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3))))))

(defconstraint storage-instruction---setting-storage-slot-values---undoing-storage-operation (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-storage-slot-values---undoing-storage-operation
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (oogx-or-no-exception)
(if-not-zero CONTEXT_WILL_REVERT
(begin
(storage-same-slot 4)
(undo-storage-warmth-and-value-update 4)
(DOM-SUB-stamps---revert-with-current 4 ;; kappa
0))))) ;; c
(if-not-zero CONTEXT_WILL_REVERT
(begin
(storage-same-slot 4)
(undo-storage-warmth-and-value-update 4)
(DOM-SUB-stamps---revert-with-current 4 ;; kappa
0))))) ;; c

(defun (orig-is-zero) (shift storage/VALUE_ORIG_IS_ZERO 3))
(defun (curr-is-zero) (shift storage/VALUE_CURR_IS_ZERO 3))
Expand Down Expand Up @@ -190,10 +221,12 @@
(defun (r-dirty-reset) (* (next-not-curr)
(curr-not-orig)
(next-is-orig)
(+ (* (orig-is-zero) (- GAS_CONST_G_SSET GAS_CONST_G_WARM_ACCESS))
(* (orig-not-zero) (- GAS_CONST_G_WARM_ACCESS GAS_CONST_G_SRESET)))))
(+ (* (orig-is-zero) (- GAS_CONST_G_SSET GAS_CONST_G_WARM_ACCESS))
(* (orig-not-zero) (- GAS_CONST_G_SRESET GAS_CONST_G_WARM_ACCESS)))))

(defconstraint storage-instruction---setting-the-refund (:guard (storage-instruction---no-stack-exceptions))
(defconstraint storage-instruction---setting-the-refund
(:guard (storage-instruction---no-stack-exceptions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq!
REFUND_COUNTER_NEW
(+ REFUND_COUNTER
Expand Down
0 hub/constraints/tx_finl/constraints.lisp → hub/constraints/tx_finl/constraints.lispX
View file
File renamed without changes.
17 changes: 17 additions & 0 deletions hub/constraints/tx_finl/peeking.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X TX_FINL phase ;;
;; X.Y Introduction ;;
;; X.Y Setting the peeking flags ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint tx-finl---setting-peeking-flags
(:guard (tx-finl---standard-precondition))
(eq! 3
(+ (shift PEEK_AT_ACCOUNT tx-finl---row-offset---ACC---sender-gas-refund)
(shift PEEK_AT_ACCOUNT tx-finl---row-offset---ACC---coinbase-reward)
(shift PEEK_AT_TRANSACTION tx-finl---row-offset---TXN))))
Loading

0 comments on commit 05aa1c6

Please sign in to comment.