perf: several wcp perf (#60)

ec_data/columns.lisp

@@ -1,56 +1,47 @@
 (module ec_data)
 
-(defcolumns
-	STAMP
-	INDEX
-	CT_MIN
-	LIMB
+(defcolumns 
+  STAMP
+  INDEX
+  CT_MIN
+  LIMB
+  TYPE
+  (EC_RECOVER :binary)
+  (EC_ADD :binary)
+  (EC_MUL :binary)
+  (EC_PAIRING :binary)
+  TOTAL_PAIRINGS
+  ACC_PAIRINGS
+  (COMPARISONS :binary)
+  (EQUALITIES :binary)
+  (HURDLE :binary)
+  (PRELIMINARY_CHECKS_PASSED :binary)
+  (ALL_CHECKS_PASSED :binary)
+  SQUARE
+  CUBE
+  (BYTE_DELTA :byte)
+  ACC_DELTA
+  WCP_ARG1_HI
+  WCP_ARG1_LO
+  WCP_ARG2_HI
+  WCP_ARG2_LO
+  (WCP_INST :byte :display :opcode)
+  (WCP_RES :binary)
+  EXT_ARG1_HI
+  EXT_ARG1_LO
+  EXT_ARG2_HI
+  EXT_ARG2_LO
+  EXT_ARG3_HI
+  EXT_ARG3_LO
+  EXT_INST
+  EXT_RES_LO
+  EXT_RES_HI
+  (THIS_IS_NOT_ON_G2 :binary)
+  (THIS_IS_NOT_ON_G2_ACC :binary)
+  (SOMETHING_WASNT_ON_G2 :binary))
 
-	TYPE
-	(EC_RECOVER	:binary)
-	(EC_ADD	:binary)
-	(EC_MUL	:binary)
-	(EC_PAIRING	:binary)
-
-	TOTAL_PAIRINGS
-	ACC_PAIRINGS
-
-	(COMPARISONS	:binary)
-	(EQUALITIES	:binary)
-
-	(HURDLE	:binary)
-	(PRELIMINARY_CHECKS_PASSED	:binary)
-	(ALL_CHECKS_PASSED	:binary)
-
-	SQUARE
-	CUBE
-
-	(BYTE_DELTA	:byte)
-	ACC_DELTA
-
-	WCP_ARG1_HI
-	WCP_ARG1_LO
-	WCP_ARG2_HI
-	WCP_ARG2_LO
-	WCP_INST
-	WCP_RES
-
-	EXT_ARG1_HI
-	EXT_ARG1_LO
-	EXT_ARG2_HI
-	EXT_ARG2_LO
-	EXT_ARG3_HI
-	EXT_ARG3_LO
-	EXT_INST
-	EXT_RES_LO
-	EXT_RES_HI
+;; aliases
+(defalias 
+  PCP PRELIMINARY_CHECKS_PASSED)
 
-	(THIS_IS_NOT_ON_G2	:binary)
-	(THIS_IS_NOT_ON_G2_ACC	:binary)
-	(SOMETHING_WASNT_ON_G2	:binary)
-)
 
-;; aliases
-(defalias
-	PCP			PRELIMINARY_CHECKS_PASSED
-)

ec_data/ecdata_into_wcp.lisp

@@ -1,20 +1,22 @@
-(deflookup lookup-ec_data-into-wcp
-    ; target columns
-    (
-        wcp.ARGUMENT_1_HI
-        wcp.ARGUMENT_1_LO
-        wcp.ARGUMENT_2_HI
-        wcp.ARGUMENT_2_LO
-        wcp.INST
-        wcp.RESULT_LO
-    )
-    ; source columns
-    (
-        ec_data.WCP_ARG1_HI
-        ec_data.WCP_ARG1_LO
-        ec_data.WCP_ARG2_HI
-        ec_data.WCP_ARG2_LO
-        ec_data.WCP_INST
-        ec_data.WCP_RES
-    )
-)
+(deflookup 
+  lookup-ec_data-into-wcp
+  ; target columns
+  (
+    wcp.ARGUMENT_1_HI
+    wcp.ARGUMENT_1_LO
+    wcp.ARGUMENT_2_HI
+    wcp.ARGUMENT_2_LO
+    wcp.INST
+    wcp.RESULT
+  )
+  ; source columns
+  (
+    ec_data.WCP_ARG1_HI
+    ec_data.WCP_ARG1_LO
+    ec_data.WCP_ARG2_HI
+    ec_data.WCP_ARG2_LO
+    ec_data.WCP_INST
+    ec_data.WCP_RES
+  ))
+
+

stp/lookups/stp_into_wcp.lisp

@@ -6,8 +6,7 @@
     wcp.ARG_1_LO
     wcp.ARG_2_HI
     wcp.ARG_2_LO
-    wcp.RES_HI
-    wcp.RES_LO
+    wcp.RES
     wcp.INST
   )
   ; source columns (in STP)
@@ -16,7 +15,6 @@
     (* stp.ARG_1_LO stp.WCP_FLAG)
     0
     (* stp.ARG_2_LO stp.WCP_FLAG)
-    0
     (* stp.RES_LO stp.WCP_FLAG)
     (* stp.EXO_INST stp.WCP_FLAG)
   ))

txn_data/columns.lisp

@@ -41,7 +41,7 @@
   OUTGOING_RLP_TXNRCPT
   WCP_ARG_ONE_LO
   WCP_ARG_TWO_LO
-  (WCP_RES_LO :binary)
+  (WCP_RES :binary)
   (WCP_INST :byte :display :opcode))
 
 (defalias 

txn_data/constraints.lisp

@@ -284,7 +284,7 @@
          (= WCP_ARG_TWO_LO
             (+ (value) (* (max_fee) (gas_limit))))
          (= WCP_INST LT)
-         (vanishes! WCP_RES_LO)))
+         (vanishes! WCP_RES)))
 
 (defun (upfront_gas_cost_of_transaction)
   (if-not-zero TYPE0
@@ -302,7 +302,7 @@
   (begin (= (shift WCP_ARG_ONE_LO 1) (gas_limit))
          (= (shift WCP_ARG_TWO_LO 1) (upfront_gas_cost_of_transaction))
          (= (shift WCP_INST 1) LT)
-         (vanishes! (shift WCP_RES_LO 1))))
+         (vanishes! (shift WCP_RES 1))))
 
 ;; epsilon is the remainder in the euclidean division of [T_g - g'] by 2
 (defun (epsilon)
@@ -315,15 +315,15 @@
   (begin (= (shift WCP_ARG_ONE_LO 2) (- (gas_limit) LEFTOVER_GAS))
          ;;  (= (shift WCP_ARG_TWO_LO 2) ???) ;; unknown
          (= (shift WCP_INST 2) LT)
-         (vanishes! (shift WCP_RES_LO 2))
+         (vanishes! (shift WCP_RES 2))
          (is-binary (epsilon))))
 
 ;; row i + 3
 (defun (effective_refund)
   (begin (= (shift WCP_ARG_ONE_LO 3) REF_CNT)
          (= (shift WCP_ARG_TWO_LO 3) (shift WCP_ARG_TWO_LO 2))
          (= (shift WCP_INST 3) LT)
-         ;;  (= (shift WCP_RES_LO     3) ???) ;; unknown
+         ;;  (= (shift WCP_RES     3) ???) ;; unknown
          ))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -334,21 +334,21 @@
   (begin (= (shift WCP_ARG_ONE_LO 4) (max_fee))
          (= (shift WCP_ARG_TWO_LO 4) BASEFEE)
          (= (shift WCP_INST 4) LT)
-         (= (shift WCP_RES_LO 4) 0)))
+         (= (shift WCP_RES 4) 0)))
 
 ;; row i + 5
 (defun (type_2_comparing_max_fee_and_max_priority_fee)
   (begin (= (shift WCP_ARG_ONE_LO 5) (max_fee))
          (= (shift WCP_ARG_TWO_LO 5) (max_priority_fee))
          (= (shift WCP_INST 5) LT)
-         (= (shift WCP_RES_LO 5) 0)))
+         (= (shift WCP_RES 5) 0)))
 
 ;; row i + 6
 (defun (type_2_computing_the_effective_gas_price)
   (begin (= (shift WCP_ARG_ONE_LO 6) (max_fee))
          (= (shift WCP_ARG_TWO_LO 6) (+ (max_priority_fee) BASEFEE))
          (= (shift WCP_INST 6) LT)
-         ;;  (= (shift WCP_RES_LO     6) ???) ;; unknown
+         ;;  (= (shift WCP_RES     6) ???) ;; unknown
          ))
 
 (defconstraint comparisons (:guard (first-row-trigger))
@@ -371,14 +371,14 @@
          (= IGAS
             (- (gas_limit) (shift WCP_ARG_TWO_LO 1)))
          ;; constraining REFUND_AMOUNT
-         (if-zero (shift WCP_RES_LO 3)
+         (if-zero (shift WCP_RES 3)
                   (= REF_AMT
                      (+ LEFTOVER_GAS (shift WCP_ARG_TWO_LO 2)))
                   (= REF_AMT (+ LEFTOVER_GAS REF_CNT)))
          ;; constraining GAS_PRICE
          (if-zero TYPE2
                   (= GAS_PRICE (gas_price))
-                  (if-zero (shift WCP_RES_LO 6)
+                  (if-zero (shift WCP_RES 6)
                            (= GAS_PRICE (+ (max_priority_fee) BASEFEE))
                            (= GAS_PRICE (max_fee))))))
 

txn_data/lookups/into_wcp.lisp

@@ -6,8 +6,7 @@
     wcp.ARGUMENT_1_LO
     wcp.ARGUMENT_2_HI
     wcp.ARGUMENT_2_LO
-    wcp.RESULT_HI
-    wcp.RESULT_LO
+    wcp.RESULT
     wcp.INST
   )
   ; source columns
@@ -16,8 +15,7 @@
     txnData.WCP_ARG_ONE_LO
     0
     txnData.WCP_ARG_TWO_LO
-    0
-    txnData.WCP_RES_LO
+    txnData.WCP_RES
     txnData.WCP_INST
   ))
 

wcp/columns.lisp

@@ -2,15 +2,24 @@
 
 (defcolumns 
   WORD_COMPARISON_STAMP
-  (ONE_LINE_INSTRUCTION :binary)
-  COUNTER
-  (INST :display :opcode)
+  (COUNTER :byte)
+  (CT_MAX :byte)
+  (INST :byte :display :opcode)
   ARGUMENT_1_HI
   ARGUMENT_1_LO
   ARGUMENT_2_HI
   ARGUMENT_2_LO
-  RESULT_HI
-  RESULT_LO
+  (RESULT :binary)
+  (IS_LT :binary)
+  (IS_GT :binary)
+  (IS_SLT :binary)
+  (IS_SGT :binary)
+  (IS_EQ :binary)
+  (IS_ISZERO :binary)
+  (IS_GEQ :binary)
+  (IS_LEQ :binary)
+  (ONE_LINE_INSTRUCTION :binary)
+  (VARIABLE_LENGTH_INSTRUCTION :binary)
   (BITS :binary)
   (NEG_1 :binary)
   (NEG_2 :binary)
@@ -35,12 +44,12 @@
 (defalias 
   STAMP    WORD_COMPARISON_STAMP
   OLI      ONE_LINE_INSTRUCTION
+  VLI      VARIABLE_LENGTH_INSTRUCTION
   CT       COUNTER
   ARG_1_HI ARGUMENT_1_HI
   ARG_1_LO ARGUMENT_1_LO
   ARG_2_HI ARGUMENT_2_HI
   ARG_2_LO ARGUMENT_2_LO
-  RES_HI   RESULT_HI
-  RES_LO   RESULT_LO)
+  RES      RESULT)