feat: enable build for zkevm.go.bin (#559)

Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com>
Co-authored-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com>

Makefile

@@ -1,4 +1,5 @@
 CORSET ?= corset
+GO_CORSET ?= go-corset
 
 HUB_COLUMNS :=  $(wildcard hub/columns/*lisp)
 
@@ -175,6 +176,9 @@ define.go: ${ZKEVM_MODULES}
 zkevm.bin: ${ZKEVM_MODULES}
 	${CORSET} compile -vv -o $@ ${ZKEVM_MODULES}
 
+zkevm.go.bin: ${ZKEVM_MODULES}
+	${GO_CORSET} compile -o $@ ${ZKEVM_MODULES}
+
 
 ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \
 				     ${BIN} \
@@ -213,5 +217,8 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \
 zkevm_for_reference_tests.bin: ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
 	${CORSET} compile -vv -o $@ ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
 
+zkevm_for_reference_tests.go.bin: ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
+	${GO_CORSET} compile -o $@ ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
+
 
 

bin/lookups/bin_into_binreftable.lisp

@@ -1,4 +1,4 @@
-(defpurefun (selector-bin-to-binreftable)
+(defun (selector-bin-to-binreftable)
   (+ bin.IS_AND bin.IS_OR bin.IS_XOR bin.IS_NOT))
 
 (deflookup

blockdata/processing/gaslimit/ethereum.lisp

@@ -1,5 +1,9 @@
 (module blockdata)
 
+;; TODO add reference to global constants
+(defconst GAS_LIMIT_MINIMUM 5000)
+(defconst GAS_LIMIT_MAXIMUM 0xffffffffffffffff)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;                                 ;;
 ;;  3 Computations and checks      ;;

blockdata/processing/gaslimit/linea.lisp

@@ -1,5 +1,9 @@
 (module blockdata)
 
+;; TODO add reference to global constants
+(defconst GAS_LIMIT_MINIMUM 61000000)
+(defconst GAS_LIMIT_MAXIMUM 2000000000)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;                              ;;
 ;;  3 Computations and checks   ;;

ecdata/constraints.lisp

@@ -453,8 +453,8 @@
                                      P_x_lo
                                      P_y_hi
                                      P_y_lo
-                                     P_x_square_hi
-                                     P_x_square_lo
+                                     P_y_square_hi
+                                     P_y_square_lo
                                      P_x_cube_plus_three_hi
                                      P_x_cube_plus_three_lo)
               (callToC1MembershipEXT k
@@ -481,8 +481,8 @@
                               P_x_lo
                               P_y_hi
                               P_y_lo
-                              P_x_square_hi
-                              P_x_square_lo
+                              P_y_square_hi
+                              P_y_square_lo
                               P_x_cube_plus_three_hi
                               P_x_cube_plus_three_lo)
   (begin (callToLT k P_x_hi P_x_lo P_BN_HI P_BN_LO)

hub/columns/stack.lisp

@@ -74,10 +74,5 @@
    ( HASH_INFO_KECCAK_LO     :i128 )
 
    ;; log info related
-   (LOG_INFO_FLAG :binary@prove)
-   )
-
-  (defalias
-   INST    INSTRUCTION
-   ))
+   (LOG_INFO_FLAG :binary@prove)))
 

hub/constraints/account.lisp

@@ -9,58 +9,58 @@
 ;; Nonce constraintes
 
 (defun (same_nonce_h)
- (eq! NONCE NONCE_NEW))
+ (eq! account/NONCE account/NONCE_NEW))
 
 (defun (increment_nonce_h)
- (eq! NONCE_NEW (+ NONCE 1)))
+ (eq! account/NONCE_NEW (+ account/NONCE 1)))
 
 (defun (decrement_nonce_h)
- (eq! NONCE_NEW (- NONCE 1)))
+ (eq! account/NONCE_NEW (- account/NONCE 1)))
 
 (defun (undo_account_nonce_update_v)
  (begin
-  (eq! NONCE (- (prev NONCE_NEW) 1))
-  (eq! NONCE_NEW (prev NONCE))))
+  (eq! account/NONCE  (- (prev account/NONCE_NEW) 1))
+  (eq! account/NONCE_NEW (prev account/NONCE))))
 
 (defun (undo_previous_account_nonce_update_v)
  (begin
-  (eq! NONCE (- (shift NONCE_NEW -2) 1))
-  (eq! NONCE_NEW (shift NONCE -2))))
+  (eq! account/NONCE  (- (shift account/NONCE_NEW -2) 1))
+  (eq! account/NONCE_NEW (shift account/NONCE     -2))))
 
 ;; Balance constraints
 (defun (same_balance_h)
- (eq! BALANCE_NEW BALANCE))
+ (eq! account/BALANCE_NEW account/BALANCE))
 
 (defun (undo_account_balance_update_v)
  (begin
-  (eq! BALANCE (prev BALANCE_NEW))
-  (eq! BALANCE_NEW (prev BALANCE))))
+  (eq! account/BALANCE (prev account/BALANCE_NEW))
+  (eq! account/BALANCE_NEW (prev account/BALANCE))))
 
 (defun (undo_previous_account_balance_update_v)
  (begin
-  (eq! BALANCE (shift BALANCE_NEW -2))
-  (eq! BALANCE_NEW (shift BALANCE -2))))
+  (eq! account/BALANCE     (shift account/BALANCE_NEW -2))
+  (eq! account/BALANCE_NEW (shift account/BALANCE     -2))))
 
 ;; Warmth constraints
 (defun (same_account_warmth_h)
- (eq! WARMTH_NEW WARMTH))
+ (eq! account/WARMTH_NEW account/WARMTH))
 
 (defun (turn_on_account_warmth_h)
- (eq! WARMTH_NEW 1))
+ (eq! account/WARMTH_NEW 1))
 
 (defun (undo_account_warmth_update_v)
  (begin
-  (eq! WARMTH (prev WARMTH_NEW))
-  (eq! WARMTH_NEW (prev WARMTH))))
+  (eq! account/WARMTH     (prev account/WARMTH_NEW))
+  (eq! account/WARMTH_NEW (prev account/WARMTH))))
 
 ;; Code constraints
 (defun (same_code_size_h)
- (eq! CODE_SIZE_NEW CODE_SIZE))
+ (eq! account/CODE_SIZE_NEW account/CODE_SIZE))
 
 (defun (same_code_hash_h)
  (begin
-  (eq! CODE_HASH_HI_NEW CODE_HASH_HI)
-  (eq! CODE_HASH_LO_NEW CODE_HASH_LO)))
+  (eq! account/CODE_HASH_HI_NEW account/CODE_HASH_HI)
+  (eq! account/CODE_HASH_LO_NEW account/CODE_HASH_LO)))
 
 (defun (same_code_h)
  (begin
@@ -69,22 +69,22 @@
 
 (defun (undo_code_size_update_v)
  (begin
-  (eq! CODE_SIZE (prev CODE_SIZE_NEW))
-  (eq! CODE_SIZE_NEW (prev CODE_SIZE))))
+  (eq! account/CODE_SIZE     (prev account/CODE_SIZE_NEW))
+  (eq! account/CODE_SIZE_NEW (prev account/CODE_SIZE))))
 
 (defun (undo_code_hash_update_v)
  (begin
-  (eq! CODE_HASH_HI (prev CODE_HASH_HI_NEW))
-  (eq! CODE_HASH_HI_NEW (prev CODE_HASH_HI))
-  (eq! CODE_HASH_LO (prev CODE_HASH_LO_NEW))
-  (eq! CODE_HASH_LO_NEW (prev CODE_HASH_LO))))
+  (eq! account/CODE_HASH_HI     (prev account/CODE_HASH_HI_NEW))
+  (eq! account/CODE_HASH_HI_NEW (prev account/CODE_HASH_HI))
+  (eq! account/CODE_HASH_LO     (prev account/CODE_HASH_LO_NEW))
+  (eq! account/CODE_HASH_LO_NEW (prev account/CODE_HASH_LO))))
 
 ;; Deployment status constraints
 (defun (same_dep_number_h)
- (eq! DEPLOYMENT_NUMBER_NEW DEPLOYMENT_NUMBER))
+ (eq! account/DEPLOYMENT_NUMBER_NEW account/DEPLOYMENT_NUMBER))
 
 (defun (same_dep_status_h)
- (eq! DEPLOYMENT_STATUS_NEW DEPLOYMENT_STATUS))
+ (eq! account/DEPLOYMENT_STATUS_NEW account/DEPLOYMENT_STATUS))
 
 (defun (same_dep_num_and_status_h)
  (begin
@@ -93,48 +93,48 @@
 
 (defun (undo_dep_number_update_v)
  (begin
-  (eq! DEPLOYMENT_NUMBER (prev DEPLOYMENT_NUMBER_NEW))
-  (eq! DEPLOYMENT_NUMBER_NEW (prev DEPLOYMENT_NUMBER))))
+  (eq! account/DEPLOYMENT_NUMBER     (prev account/DEPLOYMENT_NUMBER_NEW))
+  (eq! account/DEPLOYMENT_NUMBER_NEW (prev account/DEPLOYMENT_NUMBER))))
 
 (defun (undo_dep_status_update_v)
  (begin
-  (eq! DEPLOYMENT_STATUS (prev DEPLOYMENT_STATUS_NEW))
-  (eq! DEPLOYMENT_STATUS_NEW (prev DEPLOYMENT_STATUS))))
+  (eq! account/DEPLOYMENT_STATUS     (prev account/DEPLOYMENT_STATUS_NEW))
+  (eq! account/DEPLOYMENT_STATUS_NEW (prev account/DEPLOYMENT_STATUS))))
 
 (defun (undo_dep_status_and_number_update_v)
  (begin
   (undo_dep_number_update_v)
   (undo_dep_status_update_v)))
 
 (defun (increment_dep_number_h)
- (eq! DEPLOYMENT_NUMBER_NEW (+ DEPLOYMENT_NUMBER 1)))
+ (eq! account/DEPLOYMENT_NUMBER_NEW (+ account/DEPLOYMENT_NUMBER 1)))
 
 (defun (fresh_new_dep_num_and_status_h)
  (begin
-  (vanishes! NONCE_NEW)
-  (vanishes CODE_SIZE_NEW)
-  (vanishes! HAS_CODE_NEW)
-  (debug (eq! CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
-  (debug (eq! CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))
+  (vanishes! account/NONCE_NEW)
+  (vanishes! account/CODE_SIZE_NEW)
+  (vanishes! account/HAS_CODE_NEW)
+  (debug (eq! account/CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
+  (debug (eq! account/CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))
   (increment_dep_number_h)
-  (vanishes! DEPLOYMENT_STATUS_NEW)))
+  (vanishes! account/DEPLOYMENT_STATUS_NEW)))
 
 (defun (dep_num_and_status_update_for_deployment_with_code_h)
  (begin
   (increment_dep_number_h)
-  (eq! DEPLOYMENT_STATUS_NEW 1)
-  (vanishes! HAS_CODE_NEW)
-  (debug (eq! CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
-  (debug (eq! CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))))
+  (eq! account/DEPLOYMENT_STATUS_NEW 1)
+  (vanishes! account/HAS_CODE_NEW)
+  (debug (eq! account/CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
+  (debug (eq! account/CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))))
 
 (defun (dep_num_and_status_update_for_deployment_without_code_h)
  (begin
   (increment_dep_number_h)
-  (vanishes! DEPLOYMENT_STATUS_NEW)
-  (vanishes! CODE_SIZE_NEW)
-  (vanishes HAS_CODE_NEW)
-  (debug (eq! CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
-  (debug (eq! CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))))
+  (vanishes! account/DEPLOYMENT_STATUS_NEW)
+  (vanishes! account/CODE_SIZE_NEW)
+  (vanishes! account/HAS_CODE_NEW)
+  (debug (eq! account/CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
+  (debug (eq! account/CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))))
 
 ;; Account inspection
 (defun (account_opening_h)
@@ -150,40 +150,40 @@
 
 (defun (account_deletion_h)
  (begin
-  (vanishes! NONCE_NEW)
-  (vanishes! BALANCE_NEW)
-  (vanishes! CODE_SIZE_NEW)
-  (vanishes! HAS_CODE_NEW)
-  (debug (eq! CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
-  (debug (eq! CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))
-  fresh_new_dep_num_and_status_h))
+  (vanishes! account/NONCE_NEW)
+  (vanishes! account/BALANCE_NEW)
+  (vanishes! account/CODE_SIZE_NEW)
+  (vanishes! account/HAS_CODE_NEW)
+  (debug (eq! account/CODE_HASH_HI_NEW    EMPTY_KECCAK_HI))
+  (debug (eq! account/CODE_HASH_LO_NEW    EMPTY_KECCAK_LO))
+  (fresh_new_dep_num_and_status_h)))
 
 (defun (same_addr_as_previously_v)
  (begin
-  (remained-constant! ADDRESS_HI)
-  (remained-constant! ADDRESS_LO)))
+  (remained-constant! account/ADDRESS_HI)
+  (remained-constant! account/ADDRESS_LO)))
 
 (defun (same_addr_and_dep_num_as_previously_v)
  (begin
   (same_addr_as_previously_v)
-  (eq! DEPLOYMENT_NUMBER (prev DEPLOYMENT_NUMBER_NEW))))
+  (eq! account/DEPLOYMENT_NUMBER (prev account/DEPLOYMENT_NUMBER_NEW))))
 
 (defun (same_addr_and_dep_num_and_dep_stage_as_previously_v)
  (begin
   (same_addr_and_dep_num_as_previously_v)
-  (eq! DEPLOYMENT_STATUS (prev DEPLOYMENT_STATUS_NEW))))
+  (eq! account/DEPLOYMENT_STATUS (prev account/DEPLOYMENT_STATUS_NEW))))
 
-(defun (deploy_empty_bytecode_h)
- (begin
-  (eq! ADDRESS_HI CODE_ADDRESS_HI)
-  (eq! ADDRESS_LO CODE_ADDRESS_LO)
-  (eq! DEPLOYMENT_NUMBER CODE_DEPLOYMENT_NUMBER)
-  (debug (eq! DEPLOYMENT_STATUS 1))
-  (debug (vanishes! DEPLOYMENT_STATUS_NEW))
-  (eq! DEPLOYMENT_STATUS_NEW (- DEPLOYMENT_STATUS 1))
-  (vanishes! CODE_SIZE_NEW)
-  (vanishes! HAS_CODE_NEW)
-  (debug same_code_hash_h)))
+;; (defun (deploy_empty_bytecode_h)
+;;  (begin
+;;   (eq! account/ADDRESS_HI CODE_ADDRESS_HI)
+;;   (eq! account/ADDRESS_LO CODE_ADDRESS_LO)
+;;   (eq! account/DEPLOYMENT_NUMBER CODE_DEPLOYMENT_NUMBER)
+;;   (debug (eq! account/DEPLOYMENT_STATUS 1))
+;;   (debug (vanishes! account/DEPLOYMENT_STATUS_NEW))
+;;   (eq! account/DEPLOYMENT_STATUS_NEW (- account/DEPLOYMENT_STATUS 1))
+;;   (vanishes! account/CODE_SIZE_NEW)
+;;   (vanishes! account/HAS_CODE_NEW)
+;;   (debug same_code_hash_h)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -193,18 +193,18 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defconstraint hascode_emptyness (:perspective account)
- (if-eq-else CODE_HASH_HI EMPTY_KECCAK_HI
-    (if-eq-else CODE_HASH_LO EMPTY_KECCAK_LO
-        (vanishes! HAS_CODE)
-        (eq! HAS_CODE 1))
-    (eq! HAS_CODE 1)))
+ (if-eq-else account/CODE_HASH_HI EMPTY_KECCAK_HI
+    (if-eq-else account/CODE_HASH_LO EMPTY_KECCAK_LO
+        (vanishes! account/HAS_CODE)
+        (eq!       account/HAS_CODE 1))
+    (eq! account/HAS_CODE 1)))
 
 (defconstraint hascode_new_emptyness (:perspective account)
-               (if-eq-else    CODE_HASH_HI_NEW    EMPTY_KECCAK_HI
-                              (if-eq-else    CODE_HASH_LO_NEW    EMPTY_KECCAK_LO
-                                             (eq!    HAS_CODE_NEW 0)
-                                             (eq!    HAS_CODE_NEW 1))
-                              (eq!    HAS_CODE_NEW    1)))
+               (if-eq-else    account/CODE_HASH_HI_NEW    EMPTY_KECCAK_HI
+                              (if-eq-else    account/CODE_HASH_LO_NEW    EMPTY_KECCAK_LO
+                                             (eq!    account/HAS_CODE_NEW 0)
+                                             (eq!    account/HAS_CODE_NEW 1))
+                              (eq!    account/HAS_CODE_NEW    1)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -216,15 +216,15 @@
 ;; TODO DEBUG Only
 (defconstraint exist_is_binary (:perspective account)
  (begin
-  (is-binary EXISTS)
-  (is-binary EXISTS_NEW)))
+  (is-binary account/EXISTS)
+  (is-binary account/EXISTS_NEW)))
 
 (defconstraint exists_is_on (:perspective account)
- (if-zero (+ (~ NONCE) (~ BALANCE) (~ HAS_CODE))
-    (vanishes! EXISTS)
-    (eq! EXISTS 1)))
+ (if-zero (+ (~ account/NONCE) (~ account/BALANCE) (~ account/HAS_CODE))
+    (vanishes! account/EXISTS)
+    (eq!       account/EXISTS 1)))
 
 (defconstraint exists_new_is_on (:perspective account)
- (if-zero (+ (~ NONCE_NEW) (~ BALANCE_NEW) (~ HAS_CODE_NEW))
-    (vanishes! EXISTS_NEW)
-    (eq! EXISTS_NEW 1)))
+ (if-zero (+ (~ account/NONCE_NEW) (~ account/BALANCE_NEW) (~ account/HAS_CODE_NEW))
+    (vanishes! account/EXISTS_NEW)
+    (eq!       account/EXISTS_NEW 1)))