Fix/ref tests colum resize

Makefile

@@ -73,7 +73,9 @@ RLP_ADDR := rlpaddr
 RLP_TXN_LONDON := rlptxn/london
 RLP_TXN_CANCUN := rlptxn/cancun
 RLP_TXN_PRAGUE := rlptxn/cancun
+RLP_TXN_OSAKA  := rlptxn/osaka
 # TODO: update for Prague v2 + add RLP_AUTH
+# only difference between cancun and prague is the size of GAS_LIMIT (i25 vs i32)
 
 RLP_TXN_RCPT := rlptxrcpt
 
@@ -214,7 +216,7 @@ ZKEVM_MODULES_OSAKA := ${ZKEVM_MODULES_COMMON} \
 		 ${MMU_OSAKA} \
 		 ${MXP_CANCUN} \
 		 ${OOB_OSAKA} \
-		 ${RLP_TXN_PRAGUE} \
+		 ${RLP_TXN_OSAKA} \
 		 ${RLP_UTILS_CANCUN} \
 		 ${TRM_OSAKA} \
 		 ${TXN_DATA_OSAKA}

hub/prague/columns/transaction.lisp

@@ -23,8 +23,8 @@
                 ( IS_TYPE2                     :binary )
 
                 ;; gas related
-                ( GAS_LIMIT                    :i25 )
-                ( GAS_INITIALLY_AVAILABLE      :i25 )
+                ( GAS_LIMIT                    :i64 )
+                ( GAS_INITIALLY_AVAILABLE      :i64 )
                 ( GAS_PRICE                    :i64 )
                 ( PRIORITY_FEE_PER_GAS         :i64 )
                 ( BASEFEE                      :i64 ) ;; in Linea London this is hard-coded to 7 ... but in the reference tests this may be much larger
@@ -35,9 +35,9 @@
 
                 ;; end of transaction predictions
                 ( STATUS_CODE                  :binary )
-                ( GAS_LEFTOVER                 :i25    )
-                ( REFUND_COUNTER_INFINITY      :i25    )
-                ( REFUND_EFFECTIVE             :i25    )
+                ( GAS_LEFTOVER                 :i64    )
+                ( REFUND_COUNTER_INFINITY      :i64    )
+                ( REFUND_EFFECTIVE             :i64    )
 
                 ;; coinbase related
                 ( COINBASE_ADDRESS_HI          :i32  )

rlptxn/cancun/columns/transaction.lisp

@@ -10,7 +10,7 @@
                  ( GAS_PRICE                        :i64  )
                  ( MAX_PRIORITY_FEE_PER_GAS         :i64  )
                  ( MAX_FEE_PER_GAS                  :i64  )
-                 ( GAS_LIMIT                        :i25  )
+                 ( GAS_LIMIT                        :i64  )
                  ( TO_HI                            :i32  )
                  ( TO_LO                            :i128 )
                  ( VALUE                            :i96  )

rlptxn/osaka/columns/computation.lisp

@@ -0,0 +1,27 @@
+(module rlptxn)
+
+(defperspective cmp
+                ;; selector
+                CMP
+                (
+                 ( LIMB          :i128   )
+                 ( LIMB_SIZE     :i8     )
+                 ( TRM_FLAG      :binary )
+                 ( RLPUTILS_FLAG :binary )
+                 ( RLPUTILS_INST :i8     )
+                 ( EXO_DATA_1    :i128   )
+                 ( EXO_DATA_2    :i128   )
+                 ( EXO_DATA_3    :binary )
+                 ( EXO_DATA_4    :binary )
+                 ( EXO_DATA_5    :binary )
+                 ( EXO_DATA_6    :i128   )
+                 ( EXO_DATA_7    :i128   )
+                 ( EXO_DATA_8    :i8     )
+                 ( AUX_CCC_1     :i16    )
+                 ( AUX_CCC_2     :i16    )
+                 ( AUX_CCC_3     :i16    )
+                 ( AUX_CCC_4     :i32    )
+                 ( AUX_CCC_5     :i128   )
+                 ( AUX_1         :i24    )
+                 ( AUX_2         :i24    )
+                 ))

rlptxn/osaka/columns/shared.lisp

@@ -0,0 +1,54 @@
+(module rlptxn)
+
+(defcolumns
+  ;; ( USER_TXN_NUMBER                  :i24 ) ;; defcomputed column
+  ( TXN                           :binary@prove )
+  ( CMP                           :binary@prove )
+  ( LIMB_CONSTRUCTED              :binary@prove )
+  ( LT                            :binary@prove )
+  ( LX                            :binary@prove )
+  ;; ( INDEX_LT                      :i32 ) ;; defcomputed column
+  ;; ( INDEX_LX                      :i32 ) ;; defcomputed column
+  ( LT_BYTE_SIZE_COUNTDOWN        :i32          )
+  ( LX_BYTE_SIZE_COUNTDOWN        :i32          )
+  ;; ( TO_HASH_BY_PROVER             :binary ) ;; defcomputed column
+  ( CODE_FRAGMENT_INDEX           :i24          )
+  ( TYPE_0                        :binary@prove )
+  ( TYPE_1                        :binary@prove )
+  ( TYPE_2                        :binary@prove )
+  ;; ( TYPE_3                        :binary@prove )
+  ;; ( TYPE_4                        :binary@prove )
+  ( IS_RLP_PREFIX                 :binary@prove )
+  ( IS_CHAIN_ID                   :binary@prove )
+  ( IS_NONCE                      :binary@prove )
+  ( IS_GAS_PRICE                  :binary@prove )
+  ( IS_GAS_LIMIT                  :binary@prove )
+  ( IS_TO                         :binary@prove )
+  ( IS_VALUE                      :binary@prove )
+  ( IS_DATA                       :binary@prove )
+  ( IS_ACCESS_LIST                :binary@prove )
+  ( IS_BETA                       :binary@prove )
+  ( IS_MAX_PRIORITY_FEE_PER_GAS   :binary@prove )
+  ( IS_MAX_FEE_PER_GAS            :binary@prove )
+  ( IS_Y                          :binary@prove )
+  ( IS_R                          :binary@prove )
+  ( IS_S                          :binary@prove )
+  ;; ( PHASE_END                     :binary ) ;; defcomputed column
+  ( CT                            :i32          ) ;; Linea call data is capped at 120kB < 2**17 limbs = 2**13 bytes
+  ( CT_MAX                        :i32          ) ;; i16 is not enough for ref tests
+  ;; ( DONE                          :binary ) ;; defcomputed column
+  ( REPLAY_PROTECTION             :binary@prove )
+  ( Y_PARITY                      :binary@prove )
+  ( REQUIRES_EVM_EXECUTION        :binary       )
+  ( IS_DEPLOYMENT                 :binary       )
+  ( IS_PREFIX_OF_ACCESS_LIST_ITEM :binary@prove )
+  ( IS_PREFIX_OF_STORAGE_KEY_LIST :binary@prove )
+  ( IS_ACCESS_LIST_ADDRESS        :binary@prove )
+  ( IS_ACCESS_LIST_STORAGE_KEY    :binary@prove )
+  )
+
+;; aliases
+(defalias
+  LC  LIMB_CONSTRUCTED
+  CFI CODE_FRAGMENT_INDEX
+  )

rlptxn/osaka/columns/transaction.lisp

@@ -0,0 +1,21 @@
+(module rlptxn)
+
+(defperspective txn
+                ;; selector
+                TXN
+                (
+                 ( TX_TYPE                          :i8   )
+                 ( CHAIN_ID                         :i64  )
+                 ( NONCE                            :i64  )
+                 ( GAS_PRICE                        :i64  )
+                 ( MAX_PRIORITY_FEE_PER_GAS         :i64  )
+                 ( MAX_FEE_PER_GAS                  :i64  )
+                 ( GAS_LIMIT                        :i25  )
+                 ( TO_HI                            :i32  )
+                 ( TO_LO                            :i128 )
+                 ( VALUE                            :i96  )
+                 ( NUMBER_OF_ZERO_BYTES             :i32  )
+                 ( NUMBER_OF_NONZERO_BYTES          :i32  )
+                 ( NUMBER_OF_PREWARMED_ADDRESSES    :i24  )
+                 ( NUMBER_OF_PREWARMED_STORAGE_KEYS :i24  )
+                 ))

rlptxn/osaka/constants.lisp

@@ -0,0 +1,7 @@
+(module rlptxn)
+
+(defconst 
+RLP_TXN_CT_MAX_INTEGER          2
+RLP_TXN_CT_MAX_BYTES32          2
+RLP_TXN_CT_MAX_ADDRESS          2
+)

rlptxn/osaka/constraints/generalities/aux_ccc_k.lisp

@@ -0,0 +1,15 @@
+(module rlptxn)
+
+(defconstraint counter-constancies-for-the-AUX_CCC_k-columns ()
+    (begin
+    (counter-constant   cmp/AUX_CCC_1   CT)
+    (counter-constant   cmp/AUX_CCC_2   CT)
+    (counter-constant   cmp/AUX_CCC_3   CT)
+    (counter-constant   cmp/AUX_CCC_4   CT)
+    (counter-constant   cmp/AUX_CCC_5   CT)))
+
+
+
+
+
+

rlptxn/osaka/constraints/generalities/byte_size_countdown.lisp

@@ -0,0 +1,19 @@
+(module rlptxn)
+
+(defconstraint byte-size-countdown-update-constraints ()
+    (if-zero IS_RLP_PREFIX
+        (begin
+        (eq! LT_BYTE_SIZE_COUNTDOWN 
+             (- (prev LT_BYTE_SIZE_COUNTDOWN)
+                (* LC LT cmp/LIMB_SIZE)))
+        (eq! LX_BYTE_SIZE_COUNTDOWN 
+             (- (prev LX_BYTE_SIZE_COUNTDOWN)
+                (* LC LX cmp/LIMB_SIZE))))))
+
+(defconstraint byte-size-countdown-finalization-constraints ()
+    (if-not-zero (* IS_S PHASE_END)
+        (begin
+        (vanishes! LT_BYTE_SIZE_COUNTDOWN)
+        (vanishes! LX_BYTE_SIZE_COUNTDOWN))))
+
+(defcomputedcolumn (TO_HASH_BY_PROVER :binary) (* LC LX))

rlptxn/osaka/constraints/generalities/constancies.lisp

@@ -0,0 +1,12 @@
+(module rlptxn)
+
+(defun (transaction-constant col) 
+  (if-not (== USER_TXN_NUMBER (+ 1 (prev USER_TXN_NUMBER)))
+          (remained-constant! col)))
+
+(defconstraint transaction-constancies ()
+               (begin
+                 (transaction-constant CFI)
+                 (transaction-constant REPLAY_PROTECTION)
+                 (transaction-constant Y_PARITY)
+                 ))

rlptxn/osaka/constraints/generalities/counter.lisp

@@ -0,0 +1,19 @@
+(module rlptxn)
+
+(defconstraint counter-constancy-of-ct-max () (counter-constant CT_MAX CT))
+
+(defconstraint automatic-vanishing-of-counters-outside-of-computation-rows ()
+    (if-zero CMP 
+        (begin 
+        (vanishes! CT)
+        (vanishes! CT_MAX))))
+
+(defconstraint ct-loop ()
+    (if (== CT CT_MAX)
+        (vanishes! (next CT))
+        (will-inc! CT 1)))
+
+(defcomputedcolumn (DONE :binary)
+    (if (== CT CT_MAX)
+        (phase-flag-sum)
+        0))

rlptxn/osaka/constraints/generalities/finalization.lisp

@@ -0,0 +1,7 @@
+(module rlptxn)
+
+(defconstraint finalization (:domain {-1})
+    (if-not-zero USER_TXN_NUMBER
+        (begin 
+        (eq! PHASE_END 1)
+        (eq! IS_S      1))))

rlptxn/osaka/constraints/generalities/indexes.lisp

@@ -0,0 +1,19 @@
+(module rlptxn)
+
+;;note: :i16 is not enough for ref tests
+
+(defcomputedcolumn (INDEX_LT :i32 :fwd) 
+    (if-not-zero (is-first-row-of-transaction)
+        ;; initialization
+        0
+        ;; update
+        (+ (prev INDEX_LT) (* (prev LC) (prev LT)))
+        ))
+
+(defcomputedcolumn (INDEX_LX :i32 :fwd) 
+    (if-not-zero (is-first-row-of-transaction)
+        ;; initialization
+        0
+        ;; update
+        (+ (prev INDEX_LX) (* (prev LC) (prev LX)))
+        ))

rlptxn/osaka/constraints/generalities/lc_lt_lx.lisp

@@ -0,0 +1,56 @@
+(module rlptxn)
+
+(defun (limb-unconditionally-partakes-in-LX)
+  (force-bin (+
+               ;; IS_RLP_PREFIX
+               IS_CHAIN_ID
+               IS_NONCE
+               IS_GAS_PRICE
+               IS_MAX_PRIORITY_FEE_PER_GAS
+               IS_MAX_FEE_PER_GAS
+               IS_GAS_LIMIT
+               IS_TO
+               IS_VALUE
+               IS_DATA
+               IS_ACCESS_LIST
+               ;; IS_BETA
+               ;; IS_Y
+               ;; IS_R
+               ;; IS_S
+               )))
+
+(defun (limb-unconditionally-partakes-in-LT)
+(force-bin (+
+        (limb-unconditionally-partakes-in-LX)
+        IS_Y
+        IS_R
+        IS_S
+    )))
+
+;; ;; I've added them to the :binary@prove columns
+;; (defproperty lc-lt-lx-binaries
+;;     (begin
+;;     (is-binary LC)
+;;     (is-binary LX)
+;;     (is-binary LT)))
+
+(defconstraint counter-constancies-for-LT-and-LX ()
+    (begin
+    (counter-constant  LT  CT)
+    (counter-constant  LX  CT)
+    ))
+
+(defconstraint setting-LT-and-LX-for-most-phases ()
+    (if-not-zero (limb-unconditionally-partakes-in-LT)
+        (begin
+        (eq! LT (limb-unconditionally-partakes-in-LT))
+        (eq! LX (limb-unconditionally-partakes-in-LX)))))
+
+(defconstraint LC-may-only-turn-on-along-computation-rows ()
+    (if-zero CMP (vanishes! LC)))
+
+(defproperty LT-and-LX-automatically-vanish-on-padding-rows
+    (if-zero (phase-flag-sum)
+        (begin
+        (vanishes! LT)
+        (vanishes! LX))))

rlptxn/osaka/constraints/generalities/miscellanous.lisp

@@ -0,0 +1,15 @@
+(module rlptxn)
+
+;; binarity is taken care of via :binary@prove
+
+;; transaction-constancy is taken care of in eponymous section
+
+(defconstraint replay-protection-means-no-chain-id ()
+    (if-not-zero TXN
+        (if-not-zero txn/CHAIN_ID 
+            (eq!  REPLAY_PROTECTION 1)
+            (eq!  REPLAY_PROTECTION 0))))
+
+(defconstraint only-frontier-tx-are-not-replay-protection ()
+    (if-not-zero TXN
+        (if-zero TYPE_0 (eq! REPLAY_PROTECTION 1))))

rlptxn/osaka/constraints/generalities/perspective_flag_sum.lisp

@@ -0,0 +1,43 @@
+(module rlptxn)
+
+(defun (persp-flag-sum) (force-bin (+ TXN CMP)))
+
+(defun (about-to-enter-new-phase)
+    (force-bin (+
+        (* (- 1 IS_RLP_PREFIX               )     (next IS_RLP_PREFIX               ))
+        (* (- 1 IS_CHAIN_ID                 )     (next IS_CHAIN_ID                 ))
+        (* (- 1 IS_NONCE                    )     (next IS_NONCE                    ))
+        (* (- 1 IS_GAS_PRICE                )     (next IS_GAS_PRICE                ))
+        (* (- 1 IS_MAX_PRIORITY_FEE_PER_GAS )     (next IS_MAX_PRIORITY_FEE_PER_GAS ))
+        (* (- 1 IS_MAX_FEE_PER_GAS          )     (next IS_MAX_FEE_PER_GAS          ))
+        (* (- 1 IS_GAS_LIMIT                )     (next IS_GAS_LIMIT                ))
+        (* (- 1 IS_TO                       )     (next IS_TO                       ))
+        (* (- 1 IS_VALUE                    )     (next IS_VALUE                    ))
+        (* (- 1 IS_DATA                     )     (next IS_DATA                     ))
+        (* (- 1 IS_ACCESS_LIST              )     (next IS_ACCESS_LIST              ))
+        (* (- 1 IS_BETA                     )     (next IS_BETA                     ))
+        (* (- 1 IS_Y                        )     (next IS_Y                        ))
+        (* (- 1 IS_R                        )     (next IS_R                        ))
+        (* (- 1 IS_S                        )     (next IS_S                        ))
+    )))
+
+(defconstraint persp-flag-is-phase-flag () (eq! (persp-flag-sum) (phase-flag-sum)))
+
+(defconstraint every-phase-starts-with-a-transaction-row () (eq! (about-to-enter-new-phase) (next TXN)))
+
+(defconstraint computation-follows-transaction-row () (if-not-zero TXN (will-eq! CMP 1)))
+
+
+(defproperty outside-of-padding-rows-entering-a-new-phase-coincides-with-exiting-the-current-one 
+    (if-not-zero (phase-flag-sum) 
+        (eq! (about-to-enter-new-phase) (about-to-exit-current-phase))))
+
+;; This constraint isn't in the spec AFAICT
+;; indeed the spec doesn't contain the
+;;
+;;    upcoming_phase_transition
+;;
+;; shorthand.
+(defproperty prop-outside-of-padding-rows-entering-a-new-phase-coincides-with-exiting-the-current-one 
+    (if-not-zero (phase-flag-sum) 
+        (eq! (about-to-enter-new-phase) (upcoming-phase-transition))))