feat: shanghai hard fork

.github/workflows/check.yml

@@ -15,7 +15,7 @@ jobs:
 
     - name: Install Go Corset
       shell: bash
-      run: go install github.com/consensys/go-corset/cmd/[email protected].1
+      run: go install github.com/consensys/go-corset/cmd/[email protected].7
 
     - name: Build Constraints
       run: make -B zkevm.bin

Makefile

@@ -11,11 +11,17 @@ BIN := bin
 BLAKE2f_MODEXP_DATA := blake2fmodexpdata
 
 # constraints used in prod for LINEA, with linea block gas limit
-BLOCKDATA := $(wildcard blockdata/*.lisp) \
-	       $(wildcard blockdata/processing/*.lisp) \
-	       $(wildcard blockdata/processing/gaslimit/common.lisp) \
-	       $(wildcard blockdata/processing/gaslimit/linea.lisp) \
-	       $(wildcard blockdata/lookups/*.lisp)
+BLOCKDATALON := $(wildcard blockdata/blockdatalon/*.lisp) \
+	       $(wildcard blockdata/blockdatalon/processing/*.lisp) \
+	       $(wildcard blockdata/blockdatalon/processing/gaslimit/common.lisp) \
+	       $(wildcard blockdata/blockdatalon/processing/gaslimit/linea.lisp) \
+	       $(wildcard blockdata/blockdatalon/lookups/*.lisp)
+
+BLOCKDATASHAN := $(wildcard blockdata/blockdatashan/*.lisp) \
+	   $(wildcard blockdata/blockdatashan/processing/*.lisp) \
+	   $(wildcard blockdata/blockdatashan/processing/gaslimit/common.lisp) \
+	   $(wildcard blockdata/blockdatashan/processing/gaslimit/linea.lisp) \
+	   $(wildcard blockdata/blockdatashan/lookups/*.lisp)
 
 BLOCKHASH := blockhash
 
@@ -74,7 +80,8 @@ ZKEVM_MODULES := ${CONSTANTS} \
 		 ${ALU} \
 		 ${BIN} \
 		 ${BLAKE2f_MODEXP_DATA} \
-		 ${BLOCKDATA} \
+		 ${BLOCKDATALON} \
+		 ${BLOCKDATASHAN} \
 		 ${BLOCKHASH} \
 		 ${EC_DATA} \
 		 ${EUC} \

blockdata/columns.lisp → blockdata/blockdatalon/columns.lisp

@@ -1,4 +1,4 @@
-(module blockdata)
+(module blockdata (< EVM_FORK EVM_SHANGHAI))
 
 (defcolumns
  (IOMF                :binary@prove)

blockdata/blockdatashan/columns.lisp

@@ -0,0 +1,42 @@
+(module blockdatashan (>= EVM_FORK EVM_SHANGHAI))
+
+(defcolumns
+ (IOMF                :binary@prove)
+ (CT_MAX              :i3)
+ (CT                  :i3)
+ (IS_COINBASE         :binary@prove)
+ (IS_TIMESTAMP        :binary@prove)
+ (IS_NUMBER           :binary@prove)
+ (IS_DIFFICULTY       :binary@prove)
+ (IS_GASLIMIT         :binary@prove)
+ (IS_CHAINID          :binary@prove)
+ (IS_BASEFEE          :binary@prove)
+ (INST                :byte :display :opcode)
+ (COINBASE_HI         :i32)
+ (COINBASE_LO         :i128)
+ (BLOCK_GAS_LIMIT     :i64) ;;i32 is enough for Linea, not for reference tests
+ (BASEFEE             :i64)
+ (FIRST_BLOCK_NUMBER  :i48)
+ (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 :display :opcode)
+ (WCP_FLAG            :binary@prove)
+ (EUC_FLAG            :binary@prove)
+ )
+
+ (defalias 
+  IS_CB   IS_COINBASE
+  IS_TS   IS_TIMESTAMP
+  IS_NB   IS_NUMBER
+  IS_DF   IS_DIFFICULTY
+  IS_GL   IS_GASLIMIT
+  IS_ID   IS_CHAINID
+  IS_BF   IS_BASEFEE
+  )

blockdata/blockdatashan/constants.lisp

@@ -0,0 +1,16 @@
+(module blockdatashan)
+
+(defconst
+  ;;
+  ;; CT MAX FOR BLOCKDATA COLUMNS
+  ;;
+  nROWS_CB       1
+  nROWS_TS       2
+  nROWS_NB       2
+  nROWS_DF       1
+  nROWS_GL       5
+  nROWS_ID       1
+  nROWS_BF       1
+  nROWS_DEPTH    (+ nROWS_CB nROWS_TS nROWS_NB nROWS_DF nROWS_GL nROWS_ID nROWS_BF)
+)
+

blockdata/blockdatashan/constraints.lisp

@@ -0,0 +1,87 @@
+(module blockdatashan)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                ;;
+;;    2.2 Binary constraints      ;;
+;;                                ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; done with binary@prove in columns.lisp
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                 ;;
+;;  2.3 Unconditional constraints  ;;
+;;                                 ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defconstraint   unconditional-constraints ()
+                 (begin
+                   (eq! IOMF   (flag-sum))
+                   (eq! CT_MAX (ct-max-sum))
+                   (eq! INST   (inst-sum))))
+
+;;;;;;;;;;;;;;;;;;;;;;
+;;                  ;;
+;;  2.4 Contancies  ;;
+;;                  ;;
+;;;;;;;;;;;;;;;;;;;;;;
+
+(defconstraint   counter-constancies ()
+                 (begin (counter-constancy CT DATA_HI)
+                        (counter-constancy CT DATA_LO)
+                        (counter-constancy CT COINBASE_HI)
+                        (counter-constancy CT COINBASE_LO)
+                        (counter-constancy CT REL_TX_NUM_MAX)
+                        (counter-constancy CT BLOCK_GAS_LIMIT)
+                        (counter-constancy CT (wght-sum))))
+
+(defconstraint   first-block-number-is-conflation-constant ()
+                 (if-not-zero IOMF
+                              (will-remain-constant! FIRST_BLOCK_NUMBER)))
+
+;;;;;;;;;;;;;;;;;;;;;
+;;                 ;;
+;;  2.5 Heartbeat  ;;
+;;                 ;;
+;;;;;;;;;;;;;;;;;;;;;
+
+(defconstraint   heartbeat---iomf-initially-vanishes (:domain {0}) ;; ""
+                 (vanishes! IOMF))
+
+(defconstraint   heartbeat---iomf-is-non-decreasing ()
+                 (if-not-zero    IOMF
+                                 (eq!    (next    IOMF)    1)))
+
+(defconstraint   heartbeat---padding-vanishing ()
+                 (if-zero IOMF
+                          (begin (vanishes! CT)
+                                 (vanishes! (next CT)))))
+
+(defconstraint   heartbeat---first-instruction-is-coinbase ()
+                 (if-not    (will-remain-constant!    IOMF)
+                            (will-eq!                 IS_CB 1)))
+
+(defconstraint   heartbeat---counter-reset-at-phase-entry ()
+                 (if-not-zero (phase-entry)
+                              (vanishes! (next CT))))
+
+(defconstraint   heartbeat---counter-increase-or-instruction-transition ()
+                 (if-not-zero IOMF
+                              (if-not-zero (- CT CT_MAX)
+                                           (will-inc!  CT  1)
+                                           (eq!        (allowable-transitions) 1))))
+
+(defconstraint   heartbeat---first-row-rel-block (:domain {0}) ;; ""
+                 (vanishes! REL_BLOCK))
+
+(defconstraint   heartbeat---rel-block-increments-by-0-or-1 ()
+                 (or!  (will-inc!  REL_BLOCK  0)
+                       (will-inc!  REL_BLOCK  1)))
+
+(defconstraint   heartbeat---rel-block-exact-increments ()
+                 (eq!    (next REL_BLOCK)
+                         (+ REL_BLOCK (* (-  1  IS_CB) (next IS_CB)))))
+
+(defconstraint   heartbeat---finalization-constraints (:domain {-1}) ;; ""
+                 (begin
+                   (eq!  IS_BF  1)
+                   (eq!  CT     CT_MAX)))

blockdata/blockdatashan/lookups/blockdata_into_euc.lisp

@@ -0,0 +1,19 @@
+(defun (blockdata-into-euc-selector-shan) blockdatashan.EUC_FLAG)
+
+(deflookup 
+  blockdata-into-euc
+  ;; target columns
+  (
+    euc.IOMF
+    euc.DIVIDEND
+    euc.DIVISOR
+    euc.QUOTIENT
+  )
+  ;; source columns
+  (
+    (* 1                  (blockdata-into-euc-selector-shan))
+    (* blockdatashan.ARG_1_LO (blockdata-into-euc-selector-shan))
+    (* blockdatashan.ARG_2_LO (blockdata-into-euc-selector-shan))
+    (* blockdatashan.RES      (blockdata-into-euc-selector-shan))
+  ))
+

blockdata/blockdatashan/lookups/blockdata_into_txndata.lisp

@@ -0,0 +1,12 @@
+(deflookup
+  blockdata-into-txndata
+  ; target columns
+  (
+    txndatashan.REL_BLOCK
+  )
+  ; source columns
+  (
+    blockdatashan.REL_BLOCK
+  ))
+
+

blockdata/blockdatashan/lookups/blockdata_into_wcp.lisp

@@ -0,0 +1,24 @@
+(defun (blockdata-into-wcp-selector-shan)
+  blockdatashan.WCP_FLAG)
+
+(deflookup 
+  blockdata-into-wcp
+  ;; target columns
+  (
+    wcp.ARGUMENT_1_HI
+    wcp.ARGUMENT_1_LO
+    wcp.ARGUMENT_2_HI
+    wcp.ARGUMENT_2_LO
+    wcp.RESULT
+    wcp.INST
+  )
+  ;; source columns
+  (
+    (* blockdatashan.ARG_1_HI (blockdata-into-wcp-selector-shan))
+    (* blockdatashan.ARG_1_LO (blockdata-into-wcp-selector-shan))
+    (* blockdatashan.ARG_2_HI (blockdata-into-wcp-selector-shan))
+    (* blockdatashan.ARG_2_LO (blockdata-into-wcp-selector-shan))
+    (* blockdatashan.RES      (blockdata-into-wcp-selector-shan))
+    (* blockdatashan.EXO_INST (blockdata-into-wcp-selector-shan))
+  ))
+

blockdata/blockdatashan/macros.lisp

@@ -0,0 +1,77 @@
+(module blockdatashan)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                          ;;
+;;  1.3 Module call macros  ;;
+;;                          ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun (wcp-call-to-LT    offset
+                          a_hi
+                          a_lo
+                          b_hi
+                          b_lo)
+  (begin (eq! (shift WCP_FLAG offset) 1)
+         (eq! (shift EXO_INST offset) EVM_INST_LT)
+         (eq! (shift ARG_1_HI offset) a_hi)
+         (eq! (shift ARG_1_LO offset) a_lo)
+         (eq! (shift ARG_2_HI offset) b_hi)
+         (eq! (shift ARG_2_LO offset) b_lo)
+         (eq! (shift RES      offset) 1)))
+
+(defun (wcp-call-to-GT    offset
+                          a_hi
+                          a_lo
+                          b_hi
+                          b_lo)
+  (begin (eq! (shift WCP_FLAG offset) 1)
+         (eq! (shift EXO_INST offset) EVM_INST_GT)
+         (eq! (shift ARG_1_HI offset) a_hi)
+         (eq! (shift ARG_1_LO offset) a_lo)
+         (eq! (shift ARG_2_HI offset) b_hi)
+         (eq! (shift ARG_2_LO offset) b_lo)
+         (eq! (shift RES      offset) 1)))
+
+(defun (wcp-call-to-LEQ   offset
+                          a_hi
+                          a_lo
+                          b_hi
+                          b_lo)
+  (begin
+    (eq! (shift WCP_FLAG offset) 1)
+    (eq! (shift EXO_INST offset) WCP_INST_LEQ)
+    (eq! (shift ARG_1_HI offset) a_hi)
+    (eq! (shift ARG_1_LO offset) a_lo)
+    (eq! (shift ARG_2_HI offset) b_hi)
+    (eq! (shift ARG_2_LO offset) b_lo)
+    (eq! (shift RES      offset) 1)))
+
+(defun (wcp-call-to-GEQ   offset
+                          a_hi
+                          a_lo
+                          b_hi
+                          b_lo)
+  (begin (eq! (shift WCP_FLAG offset) 1)
+         (eq! (shift EXO_INST offset) WCP_INST_GEQ)
+         (eq! (shift ARG_1_HI offset) a_hi)
+         (eq! (shift ARG_1_LO offset) a_lo)
+         (eq! (shift ARG_2_HI offset) b_hi)
+         (eq! (shift ARG_2_LO offset) b_lo)
+         (eq! (shift RES      offset) 1)))
+
+(defun (wcp-call-to-ISZERO    offset
+                              a_hi
+                              a_lo)
+  (begin (eq! (shift WCP_FLAG offset) 1)
+         (eq! (shift EXO_INST offset) EVM_INST_ISZERO)
+         (eq! (shift ARG_1_HI offset) a_hi)
+         (eq! (shift ARG_1_LO offset) a_lo)
+         (eq! (shift ARG_2_HI offset) 0)
+         (eq! (shift ARG_2_LO offset) 0)))
+
+(defun (euc-call    offset
+                    a
+                    b)
+  (begin (eq! (shift EUC_FLAG offset) 1)
+         (eq! (shift ARG_1_LO offset) a)
+         (eq! (shift ARG_2_LO offset) b)))

blockdata/blockdatashan/processing/basefee.lisp

@@ -0,0 +1,27 @@
+(module blockdatashan)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                             ;;
+;;  3 Computations and checks  ;;
+;;  3.X For BASEFEE            ;;
+;;                             ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun (basefee-precondition) (* (- 1 (prev IS_BF)) IS_BF))
+(defun (curr-BASEFEE-hi)      (curr-data-hi))
+(defun (curr-BASEFEE-lo)      (curr-data-lo))
+
+(defconstraint   basefee---horizontalization
+                 (:guard (basefee-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (begin (eq!  (curr-BASEFEE-hi)  0)
+                        (eq!  (curr-BASEFEE-lo)  BASEFEE)))
+
+(defconstraint   basefee---size-constraint
+                 (:guard (basefee-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (wcp-call-to-GEQ   0
+                                    (curr-BASEFEE-hi)
+                                    (curr-BASEFEE-lo)
+                                    0
+                                    0))

blockdata/blockdatashan/processing/chainid.lisp

@@ -0,0 +1,22 @@
+(module blockdatashan)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                             ;;
+;;  3 Computations and checks  ;;
+;;  3.X For CHAINID            ;;
+;;                             ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun (chainid-precondition) (* (- 1 (prev IS_ID)) IS_ID))
+
+(defconstraint   chainid-permanence
+                 (:guard (chainid-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (if-not-zero   (isnt-first-block-in-conflation)
+                                (begin (eq! DATA_HI (shift DATA_HI (* nROWS_DEPTH -1)))
+                                       (eq! DATA_LO (shift DATA_LO (* nROWS_DEPTH -1))))))
+
+(defconstraint   chainid-bound
+                 (:guard (chainid-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (wcp-call-to-GEQ 0 DATA_HI DATA_LO 0 0))