Merge branch 'master' into 516-implementation-of-initialization-and-f…

…inalization-phase-fix
Consensys · Dec 5, 2024 · d9d41d3 · d9d41d3
2 parents c2d3c88 + ba3e726
commit d9d41d3
Show file tree

Hide file tree

Showing 160 changed files with 406 additions and 356 deletions.
diff --git a/alu/add/columns.lisp b/alu/add/columns.lisp
@@ -1,6 +1,6 @@
 (module add)
 
-(defcolumns 
+(defcolumns
   (STAMP :i32)
   (CT_MAX :byte)
   (CT :byte)

diff --git a/alu/add/constraints.lisp b/alu/add/constraints.lisp
@@ -1,6 +1,6 @@
 (module add)
 
-(defconst 
+(defconst
   THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16
 
 (defconstraint stamp-constancies ()

diff --git a/alu/ext/columns.lisp b/alu/ext/columns.lisp
@@ -19,7 +19,7 @@
     (OF_I   :binary@prove)
     (OF_J   :binary@prove)
     (OF_H   :binary@prove)
-    (OF_RES :binary@prove) 
+    (OF_RES :binary@prove)
     ;
     (BIT_1 :binary@prove)
     (BIT_2 :binary@prove)

diff --git a/alu/ext/constraints.lisp b/alu/ext/constraints.lisp
@@ -1,6 +1,6 @@
 (module ext)
 
-(defconst 
+(defconst
   THETA  18446744073709551616                     ;18446744073709551616 = 256^8
   THETA2 340282366920938463463374607431768211456) ;340282366920938463463374607431768211456 = 256^16
 
@@ -141,7 +141,7 @@
 (defconstraint bit-3-constraints ()
                (if-not-zero STAMP
                             (begin
-                              (if-not-zero   ARG_3_HI                 
+                              (if-not-zero   ARG_3_HI
                                              ;; ARG_3_HI ≠ 0
                                              (vanishes! BIT_3)
                                              ;; ARG_3_HI = 0

diff --git a/alu/mod/columns.lisp b/alu/mod/columns.lisp
@@ -1,6 +1,6 @@
 (module mod)
 
-(defcolumns 
+(defcolumns
   (STAMP   :i32)
   (OLI     :binary@prove)
   (MLI     :binary@prove)

diff --git a/alu/mod/constants.lisp b/alu/mod/constants.lisp
@@ -1,6 +1,6 @@
 (module mod)
 
-(defconst 
+(defconst
   THETA                  18446744073709551616                     ;18446744073709551616 = 256^8
   THETA2                 340282366920938463463374607431768211456  ;340282366920938463463374607431768211456 = 256^16
   THETA_SQUARED_OVER_TWO 170141183460469231731687303715884105728) ;170141183460469231731687303715884105728 = (1/2)*THETA2

diff --git a/alu/mul/constraints.lisp b/alu/mul/constraints.lisp
@@ -1,6 +1,6 @@
 (module mul)
 
-(defconst 
+(defconst
   ONETWOEIGHT 128
   ONETWOSEVEN 127
   THETA       18446744073709551616                     ;18446744073709551616 = 256^8

diff --git a/bin/columns.lisp b/bin/columns.lisp
@@ -1,6 +1,6 @@
 (module bin)
 
-(defcolumns 
+(defcolumns
   (STAMP :i32)
   (CT_MAX :byte)
   (COUNTER :byte)
@@ -41,7 +41,7 @@
   (XXX_BYTE_LO :byte))
 
 ;; aliases
-(defalias 
+(defalias
   CT       COUNTER
   ARG_1_HI ARGUMENT_1_HI
   ARG_1_LO ARGUMENT_1_LO

diff --git a/bin/constraints.lisp b/bin/constraints.lisp
@@ -71,7 +71,7 @@
          (counter-constancy CT NEG)
          (counter-constancy CT SMALL)))
 
-;;    2.6 byte decompositions   
+;;    2.6 byte decompositions
 (defconstraint byte_decompositions ()
   (begin (byte-decomposition CT ACC_1 BYTE_1)
          (byte-decomposition CT ACC_2 BYTE_2)
@@ -80,7 +80,7 @@
          (byte-decomposition CT ACC_5 BYTE_5)
          (byte-decomposition CT ACC_6 BYTE_6)))
 
-;;    2.7 target constraints   
+;;    2.7 target constraints
 (defun (requires-byte-decomposition)
   (+ IS_AND
      IS_OR
@@ -148,7 +148,7 @@
                      (eq! SMALL 1)
                      (vanishes! SMALL))))
 
-;;    2.9 pivot constraints    
+;;    2.9 pivot constraints
 (defconstraint pivot (:guard CT_MAX)
   (begin (if-eq IS_BYTE 1
                 (if-zero LOW_4

diff --git a/bin/lookups/bin_into_binreftable.lisp b/bin/lookups/bin_into_binreftable.lisp
@@ -1,7 +1,7 @@
 (defpurefun (selector-bin-to-binreftable)
   (+ bin.IS_AND bin.IS_OR bin.IS_XOR bin.IS_NOT))
 
-(deflookup 
+(deflookup
   bin-into-binreftable-high
   ;reference columns
   (
@@ -10,15 +10,15 @@
     binreftable.INPUT_BYTE_1
     binreftable.INPUT_BYTE_2
   )
-  ;source columns 
+  ;source columns
   (
     (* bin.INST (selector-bin-to-binreftable))
     (* bin.XXX_BYTE_HI (selector-bin-to-binreftable))
     (* bin.BYTE_1 (selector-bin-to-binreftable))
     (* bin.BYTE_3 (selector-bin-to-binreftable))
   ))
 
-(deflookup 
+(deflookup
   bin-into-binreftable-low
   ;reference columns
   (
@@ -27,7 +27,7 @@
     binreftable.INPUT_BYTE_1
     binreftable.INPUT_BYTE_2
   )
-  ;source columns 
+  ;source columns
   (
     (* bin.INST (selector-bin-to-binreftable))
     (* bin.XXX_BYTE_LO (selector-bin-to-binreftable))

diff --git a/blake2fmodexpdata/columns.lisp b/blake2fmodexpdata/columns.lisp
@@ -1,6 +1,6 @@
 (module blake2fmodexpdata)
 
-(defcolumns 
+(defcolumns
   (STAMP                :i10)
   (ID                   :i32)
   (PHASE                :byte)

diff --git a/blake2fmodexpdata/constants.lisp b/blake2fmodexpdata/constants.lisp
@@ -1,6 +1,6 @@
 (module blake2fmodexpdata)
 
-(defconst 
+(defconst
   INDEX_MAX_MODEXP          31
   INDEX_MAX_MODEXP_BASE     INDEX_MAX_MODEXP
   INDEX_MAX_MODEXP_EXPONENT INDEX_MAX_MODEXP

diff --git a/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp b/blake2fmodexpdata/lookups/blakemodexp_into_wcp.lisp
@@ -2,7 +2,7 @@
   (force-bool (* (~ blake2fmodexpdata.STAMP)
                  (- blake2fmodexpdata.STAMP (prev blake2fmodexpdata.STAMP)))))
 
-(deflookup 
+(deflookup
   blake2fmodexpdata-into-wcp
   ; target colums (in WCP)
   (

diff --git a/blockdata/columns.lisp b/blockdata/columns.lisp
@@ -1,6 +1,6 @@
 (module blockdata)
 
-(defcolumns 
+(defcolumns
   (FIRST_BLOCK_NUMBER :i48)
   (CT :i4)
   (REL_BLOCK           :i10)

diff --git a/blockdata/constants.lisp b/blockdata/constants.lisp
@@ -1,6 +1,6 @@
 (module blockdata)
 
-(defconst 
+(defconst
   CT_MAX_FOR_BLOCKDATA    6 ;;need to update the lookup into wcp if changed
   ROW_SHIFT_COINBASE      0
   ROW_SHIFT_TIMESTAMP     1

diff --git a/blockdata/constraints.lisp b/blockdata/constraints.lisp
@@ -69,7 +69,7 @@
 (defun    (blockdata---first-row-of-new-block)   (-   REL_BLOCK   (prev REL_BLOCK)))
 
 (defconstraint value-constraints---COINBASE (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq! (shift INST     ROW_SHIFT_COINBASE) EVM_INST_COINBASE)
                  (eq! (shift DATA_HI  ROW_SHIFT_COINBASE) COINBASE_HI)
                  (eq! (shift DATA_LO  ROW_SHIFT_COINBASE) COINBASE_LO)
@@ -87,7 +87,7 @@
                                (* (^ 256 (- LLARGEMO   11)) (shift [BYTE_HI   11]   ROW_SHIFT_COINBASE))))))
 
 (defconstraint value-constraints---TIMESTAMP (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST     ROW_SHIFT_TIMESTAMP) EVM_INST_TIMESTAMP)
                  (vanishes! (shift DATA_HI  ROW_SHIFT_TIMESTAMP))
                  (vanishes! (+ (* (^ 256 (- LLARGEMO   0)) (shift [BYTE_LO   0]   ROW_SHIFT_TIMESTAMP))
@@ -104,7 +104,7 @@
                               (eq! (shift WCP_FLAG ROW_SHIFT_TIMESTAMP) 1))))
 
 (defconstraint value-constraints---NUMBER (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST      ROW_SHIFT_NUMBER) EVM_INST_NUMBER)
                  (vanishes! (shift DATA_HI   ROW_SHIFT_NUMBER))
                  (eq!       (shift DATA_LO   ROW_SHIFT_NUMBER) (+ FIRST_BLOCK_NUMBER (- REL_BLOCK 1)))
@@ -120,27 +120,27 @@
                                (* (^ 256 (- LLARGEMO   9)) (shift [BYTE_LO   9]   ROW_SHIFT_NUMBER))))))
 
 (defconstraint value-constraints---DIFFICULTY (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST      ROW_SHIFT_DIFFICULTY) EVM_INST_DIFFICULTY)
                  (vanishes! (shift DATA_HI   ROW_SHIFT_DIFFICULTY))
                  (eq!       (shift DATA_LO   ROW_SHIFT_DIFFICULTY) LINEA_DIFFICULTY)))
 
 (defconstraint value-constraints---GASLIMIT (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST      ROW_SHIFT_GASLIMIT) EVM_INST_GASLIMIT)
                  (vanishes! (shift DATA_HI   ROW_SHIFT_GASLIMIT))
                  (eq!       (shift DATA_LO   ROW_SHIFT_GASLIMIT) LINEA_BLOCK_GAS_LIMIT)
                  (eq!       (shift DATA_LO   ROW_SHIFT_GASLIMIT) BLOCK_GAS_LIMIT)))
 
 (defconstraint value-constraints---CHAINID (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST      ROW_SHIFT_CHAINID) EVM_INST_CHAINID)
                  (vanishes! (shift DATA_HI   ROW_SHIFT_CHAINID))
                  ;(eq!      (shift DATA_LO   ROW_SHIFT_CHAINID) LINEA_CHAIN_ID) ;; TODO: this needs some fixing
                  ))
 
 (defconstraint value-constraints---BASEFEE (:guard (blockdata---first-row-of-new-block))
-               (begin  
+               (begin
                  (eq!       (shift INST      ROW_SHIFT_BASEFEE) EVM_INST_BASEFEE)
                  (vanishes! (shift DATA_HI   ROW_SHIFT_BASEFEE))
                  (eq!       (shift DATA_LO   ROW_SHIFT_BASEFEE) LINEA_BASE_FEE)

diff --git a/blockdata/lookups/blockdata_into_txndata.lisp b/blockdata/lookups/blockdata_into_txndata.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockdata-into-txndata
   ; target columns
   (

diff --git a/blockdata/lookups/blockdata_into_wcp.lisp b/blockdata/lookups/blockdata_into_wcp.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockdata-into-wcp
   ; target columns
   (

diff --git a/blockhash/columns.lisp b/blockhash/columns.lisp
@@ -1,6 +1,6 @@
 (module blockhash)
 
-(defcolumns 
+(defcolumns
   (IOMF :binary)
   (BLOCK_NUMBER_HI :i128)
   (BLOCK_NUMBER_LO :i128)

diff --git a/blockhash/lookups/blockhash_into_blockdata.lisp b/blockhash/lookups/blockhash_into_blockdata.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockhash-into-blockdata
   ; target columns
   (

diff --git a/blockhash/lookups/blockhash_into_wcp_lex.lisp b/blockhash/lookups/blockhash_into_wcp_lex.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockhash-into-wcp-lex
   ; target columns
   (

diff --git a/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp b/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockhash-into-wcp-lower-bound
   ; target columns
   (

diff --git a/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp b/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   blockhash-into-wcp-upper-bound
   ; target columns
   (

diff --git a/constants/constants.lisp b/constants/constants.lisp
@@ -1,4 +1,4 @@
-(defconst 
+(defconst
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;                  ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM INSTRUCTIONS ;;
@@ -419,7 +419,7 @@
   RLP_RCPT_SUBPHASE_ID_DATA_SIZE            83
   RLP_RCPT_SUBPHASE_ID_TOPIC_DELTA          96
   ;;
-  ;; RLP_ADDR 
+  ;; RLP_ADDR
   ;;
   RLP_ADDR_RECIPE_1                         1                                  ;; for RlpAddr, used to discriminate between recipe for create
   RLP_ADDR_RECIPE_2                         2                                  ;; for RlpAddr, used to discriminate between recipe for create

diff --git a/ecdata/columns.lisp b/ecdata/columns.lisp
@@ -1,6 +1,6 @@
 (module ecdata)
 
-(defcolumns 
+(defcolumns
   (STAMP        :i32)
   (ID           :i32)
   (INDEX        :i16)
@@ -62,7 +62,7 @@
   (EXT_INST     :byte :display :opcode))
 
 ;; aliases
-(defalias 
+(defalias
   ICP              INTERNAL_CHECKS_PASSED
   TRIVIAL_PAIRING  OVERALL_TRIVIAL_PAIRING
   G2MTR            G2_MEMBERSHIP_TEST_REQUIRED

diff --git a/ecdata/constants.lisp b/ecdata/constants.lisp
@@ -1,6 +1,6 @@
 (module ecdata)
 
-(defconst 
+(defconst
   P_BN_HI                       0x30644e72e131a029b85045b68181585d
   P_BN_LO                       0x97816a916871ca8d3c208c16d87cfd47
   SECP256K1N_HI                 0xffffffffffffffffffffffffffffffff

diff --git a/ecdata/constraints.lisp b/ecdata/constraints.lisp
@@ -286,7 +286,7 @@
                   (vanishes! ID))))
 
 (defconstraint stamp-increment-sanity-check ()
-  (begin 
+  (begin
     (debug (any! (will-remain-constant! STAMP) (will-inc! STAMP 1))))) ;; implied by the constraint below
 
 (defconstraint stamp-increment ()

diff --git a/ecdata/lookups/ecdata_into_ext.lisp b/ecdata/lookups/ecdata_into_ext.lisp
@@ -1,7 +1,7 @@
 (defun (ec_data-into-ext-activation-flag)
   ecdata.EXT_FLAG)
 
-(deflookup 
+(deflookup
   ecdata-into-ext
   ; target columns
   (

diff --git a/ecdata/lookups/ecdata_into_wcp.lisp b/ecdata/lookups/ecdata_into_wcp.lisp
@@ -1,7 +1,7 @@
 (defun (ec_data-into-wcp-activation-flag)
   ecdata.WCP_FLAG)
 
-(deflookup 
+(deflookup
   ecdata-into-wcp
   ; target columns
   (

diff --git a/euc/columns.lisp b/euc/columns.lisp
@@ -1,6 +1,6 @@
 (module euc)
 
-(defcolumns 
+(defcolumns
   (IOMF :binary@prove)
   (CT :i8)
   (CT_MAX :i8)

diff --git a/euc/constraints.lisp b/euc/constraints.lisp
@@ -1,6 +1,6 @@
 (module euc)
 
-(defconst 
+(defconst
   MAX_INPUT_LENGTH MMEDIUM)
 
 (defconstraint first-row (:domain {0})

diff --git a/euc/lookups/euc_into_wcp.lisp b/euc/lookups/euc_into_wcp.lisp
@@ -1,4 +1,4 @@
-(deflookup 
+(deflookup
   euc-into-wcp
   ;reference columns
   (

diff --git a/exp/columns.lisp b/exp/columns.lisp
@@ -1,6 +1,6 @@
 (module exp)
 
-(defcolumns 
+(defcolumns
   (CMPTN         :binary@prove)
   (MACRO         :binary@prove)
   (PRPRC         :binary@prove)

diff --git a/exp/constants.lisp b/exp/constants.lisp
@@ -1,6 +1,6 @@
 (module exp)
 
-(defconst 
+(defconst
   CT_MAX_CMPTN_EXP_LOG    15
   CT_MAX_MACRO_EXP_LOG    0
   CT_MAX_PRPRC_EXP_LOG    0