Implementation of TX_INIT and TX_FINL fix

Makefile

@@ -28,7 +28,9 @@ HUB :=  $(wildcard hub/columns/*lisp) \
 	$(wildcard hub/constraints/tx_skip/*lisp) \
 	$(wildcard hub/constraints/tx_prewarm/*lisp) \
 	$(wildcard hub/constraints/tx_init/*lisp) \
+	$(wildcard hub/constraints/tx_init/rows/*lisp) \
 	$(wildcard hub/constraints/tx_finl/*lisp) \
+	$(wildcard hub/constraints/tx_finl/rows/*lisp) \
 	$(wildcard hub/constraints/*lisp) \
 	$(wildcard hub/lookups/*lisp) \
 	hub/constants.lisp

blockdata/columns.lisp

@@ -14,11 +14,11 @@
  (INST                :byte :display :opcode)
  (COINBASE_HI         :i32)
  (COINBASE_LO         :i128)
- (BLOCK_GAS_LIMIT     :i48)
- (BASEFEE             :i48)
+ (BLOCK_GAS_LIMIT     :i64)
+ (BASEFEE             :i64)
  (FIRST_BLOCK_NUMBER  :i48)
- (REL_BLOCK           :i8)
- (REL_TX_NUM_MAX      :i10)
+ (REL_BLOCK           :i16)
+ (REL_TX_NUM_MAX      :i16)
  (DATA_HI             :i128)
  (DATA_LO             :i128)
  (ARG_1_HI            :i128)

constants/constants.lisp

@@ -222,7 +222,7 @@
   LINEA_DIFFICULTY                          2
   LINEA_MAX_NUMBER_OF_TRANSACTIONS_IN_BATCH 200
   ETHEREUM_GAS_LIMIT_MINIMUM                5000
-  ETHEREUM_GAS_LIMIT_MAXIMUM                0xffffffffffffffffffffffffffffffff ;; maxUint64
+  ETHEREUM_GAS_LIMIT_MAXIMUM                0xffffffffffffffff ;; maxUint64
   LINEA_GAS_LIMIT_MINIMUM                   61000000
   LINEA_GAS_LIMIT_MAXIMUM                   2000000000
   GAS_LIMIT_ADJUSTMENT_FACTOR               1024

hub/constants.lisp

@@ -2,7 +2,8 @@
 
 (defconst
   MULTIPLIER___STACK_STAMP                 8      ;; \hubTau
-  MULTIPLIER___DOM_SUB_STAMPS              8      ;; \hubLambda
-  DOM_SUB_STAMP_OFFSET___REVERT            6      ;; \revertEpsilon
-  DOM_SUB_STAMP_OFFSET___SELFDESTRUCT      7      ;; \selfdestructEpsilon
+  MULTIPLIER___DOM_SUB_STAMPS             16      ;; \hubLambda
+  DOM_SUB_STAMP_OFFSET___REVERT            8      ;; \revertEpsilon
+  DOM_SUB_STAMP_OFFSET___FINALIZATION      9      ;; \finalizationEpsilon
+  DOM_SUB_STAMP_OFFSET___SELFDESTRUCT     10      ;; \selfdestructEpsilon
   )

hub/constraints/generalities/revert_data_specific.lisp

@@ -39,7 +39,7 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun (self_revert_trigger) (- (+ XAHOY (* stack/HALT_FLAG [stack/DEC_FLAG 2]))
-                                (* XAHOY    stack/HALT_FLAG [stack/DEC_FLAG 2])))
+                                (* XAHOY    stack/HALT_FLAG [stack/DEC_FLAG 2]))) ;; ""
 
 (defconstraint recording-self-induced-revert (:perspective stack)
                (if-not-zero (force-bool (self_revert_trigger))
@@ -112,6 +112,13 @@
                              sub_stamp_offset
                              ))
 
+;; (defun (DOM-SUB-stamps---finalization    rel_offset
+;;                                          sub_offset)
+;;   (undoing-dom-sub-stamps   rel_offset
+;;                             TX_END_STAMP
+;;                             DOM_SUB_STAMP_OFFSET___FINALIZATION
+;;                             sub_offset))
+
 (defun (selfdestruct-dom-sub-stamps relOffset) (undoing-dom-sub-stamps
                                                  relOffset
                                                  TX_END_STAMP

hub/constraints/heartbeat/hub_stamp.lisp

@@ -25,7 +25,15 @@
                                 (will-inc! HUB_STAMP 1))))
 
 (defconstraint   heartbeat---hub-stamp---constancy-during-skipping-phase ()
-                 (if-not-zero (+ TX_SKIP TX_INIT TX_FINL)
+                 (if-not-zero TX_SKIP
+                              (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION))))
+
+(defconstraint   heartbeat---hub-stamp---constancy-during-initialization-phase ()
+                 (if-not-zero TX_INIT
+                              (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_CONTEXT))))
+
+(defconstraint   heartbeat---hub-stamp---constancy-during-finalization-phase ()
+                 (if-not-zero TX_FINL
                               (will-eq! HUB_STAMP (+ HUB_STAMP PEEK_AT_TRANSACTION))))
 
 (defconstraint   heartbeat---hub-stamp---jumps-at-transaction-boundaries ()

hub/constraints/heartbeat/transaction_phase_flags.lisp

@@ -47,7 +47,7 @@
                  (if-not-zero TX_WARM
                               (eq! (next (+ TX_WARM TX_INIT)) 1))
                  (if-not-zero TX_INIT
-                              (if-zero PEEK_AT_TRANSACTION
+                              (if-zero PEEK_AT_CONTEXT
                                        (eq! (next TX_INIT) 1)
                                        (eq! (next TX_EXEC) 1)))
                  (if-not-zero TX_EXEC

hub/constraints/instruction-handling/sto.lisp

@@ -190,8 +190,8 @@
 (defun    (r-dirty-reset)    (*    (next-not-curr)
                                    (curr-not-orig)
                                    (next-is-orig)
-                                   (+    (*    (orig-is-zero)     (-   GAS_CONST_G_SSET           GAS_CONST_G_WARM_ACCESS))
-                                         (*    (orig-not-zero)    (-   GAS_CONST_G_WARM_ACCESS    GAS_CONST_G_SRESET)))))
+                                   (+    (*    (orig-is-zero)     (-   GAS_CONST_G_SSET     GAS_CONST_G_WARM_ACCESS))
+                                         (*    (orig-not-zero)    (-   GAS_CONST_G_SRESET   GAS_CONST_G_WARM_ACCESS)))))
 
 (defconstraint   storage-instruction---setting-the-refund (:guard (storage-instruction---no-stack-exceptions))
                  (eq!

hub/constraints/tx_finl/peeking.lisp

@@ -0,0 +1,17 @@
+(module hub)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                   ;;
+;;   X   TX_FINL phase               ;;
+;;   X.Y Introduction                ;;
+;;   X.Y Setting the peeking flags   ;;
+;;                                   ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(defconstraint    tx-finl---setting-peeking-flags
+                  (:guard    (tx-finl---standard-precondition))
+                  (eq!   3
+                         (+ (shift   PEEK_AT_ACCOUNT       tx-finl---row-offset---ACC---sender-gas-refund)
+                            (shift   PEEK_AT_ACCOUNT       tx-finl---row-offset---ACC---coinbase-reward)
+                            (shift   PEEK_AT_TRANSACTION   tx-finl---row-offset---TXN))))

hub/constraints/tx_finl/rows/acc_coinbase_reward.lisp

@@ -0,0 +1,28 @@
+(module hub)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                              ;;
+;;   X     TX_FINL phase        ;;
+;;   X.Y   Common constraints   ;;
+;;   X.Y.Z Coinbase reward      ;;
+;;                              ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(defconstraint   tx-finl---account-row---coinbase-reward
+                 (:guard (tx-finl---standard-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (begin
+                   (account-trim-address   tx-finl---row-offset---ACC---coinbase-reward   ;; row offset
+                                           (tx-finl---coinbase-address-hi)                ;; high part of raw, potentially untrimmed address
+                                           (tx-finl---coinbase-address-lo))               ;; low  part of raw, potentially untrimmed address
+                   ;; (eq!     (shift account/ADDRESS_HI             tx-finl---row-offset---ACC---coinbase-reward)     (tx-finl---coinbase-address-hi))
+                   ;; (eq!     (shift account/ADDRESS_LO             tx-finl---row-offset---ACC---coinbase-reward)     (tx-finl---coinbase-address-lo))
+                   (account-increment-balance-by                  tx-finl---row-offset---ACC---coinbase-reward      (tx-finl---coinbase-reward))
+                   (account-same-nonce                            tx-finl---row-offset---ACC---coinbase-reward)
+                   (account-same-code                             tx-finl---row-offset---ACC---coinbase-reward)
+                   (account-same-deployment-number-and-status     tx-finl---row-offset---ACC---coinbase-reward)
+                   (account-same-warmth                           tx-finl---row-offset---ACC---coinbase-reward)
+                   (account-same-marked-for-selfdestruct          tx-finl---row-offset---ACC---coinbase-reward)
+                   (DOM-SUB-stamps---standard                     tx-finl---row-offset---ACC---coinbase-reward
+                                                                  1)))

hub/constraints/tx_finl/rows/acc_sender_gas_refund.lisp

@@ -0,0 +1,25 @@
+(module hub)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                              ;;
+;;   X     TX_FINL phase        ;;
+;;   X.Y   Common constraints   ;;
+;;   X.Y.Z Sender gas refund    ;;
+;;                              ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(defconstraint   tx-finl---account-row---sender-gas-refund
+                 (:guard (tx-finl---standard-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (begin
+                   (eq!     (shift account/ADDRESS_HI             tx-finl---row-offset---ACC---sender-gas-refund)     (tx-finl---sender-address-hi))
+                   (eq!     (shift account/ADDRESS_LO             tx-finl---row-offset---ACC---sender-gas-refund)     (tx-finl---sender-address-lo))
+                   (account-increment-balance-by                  tx-finl---row-offset---ACC---sender-gas-refund      (tx-finl---sender-gas-refund))
+                   (account-same-nonce                            tx-finl---row-offset---ACC---sender-gas-refund)
+                   (account-same-code                             tx-finl---row-offset---ACC---sender-gas-refund)
+                   (account-same-deployment-number-and-status     tx-finl---row-offset---ACC---sender-gas-refund)
+                   (account-same-warmth                           tx-finl---row-offset---ACC---sender-gas-refund)
+                   (account-same-marked-for-selfdestruct          tx-finl---row-offset---ACC---sender-gas-refund)
+                   (DOM-SUB-stamps---standard                     tx-finl---row-offset---ACC---sender-gas-refund
+                                                                  0)))

hub/constraints/tx_finl/rows/transaction.lisp

@@ -0,0 +1,17 @@
+(module hub)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                              ;;
+;;   X     TX_FINL phase        ;;
+;;   X.Y   Common constraints   ;;
+;;   X.Y.Z Transaction row      ;;
+;;                              ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defconstraint    tx-finl---transaction-row---justifying-TXN_DATA-predictions
+                 (:guard (tx-finl---standard-precondition))
+                 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                 (begin
+                   (eq!   (shift   transaction/STATUS_CODE               tx-finl---row-offset---TXN)   (tx-finl---transaction-success))
+                   (eq!   (shift   transaction/REFUND_COUNTER_INFINITY   tx-finl---row-offset---TXN)   (shift   REFUND_COUNTER_NEW    tx-finl---row-offset---row-preceding-the-finl-phase))
+                   (eq!   (shift   transaction/GAS_LEFTOVER              tx-finl---row-offset---TXN)   (shift   GAS_NEXT              tx-finl---row-offset---row-preceding-the-finl-phase))))

hub/constraints/tx_finl/shorthands.lisp

@@ -0,0 +1,34 @@
+(module hub)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                       ;;
+;;   X   TX_FINL phase   ;;
+;;   X.Y Introduction    ;;
+;;   X.Y Shorthands      ;;
+;;                       ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defconst
+  tx-finl---row-offset---row-preceding-the-finl-phase   -1
+  tx-finl---row-offset---ACC---sender-gas-refund         0
+  tx-finl---row-offset---ACC---coinbase-reward           1
+  tx-finl---row-offset---TXN                             2
+  )
+
+
+
+(defun    (tx-finl---standard-precondition)   (*       (shift   TX_EXEC               tx-finl---row-offset---row-preceding-the-finl-phase)   TX_FINL))
+(defun    (tx-finl---transaction-success)     (-   1   (shift   CONTEXT_WILL_REVERT   tx-finl---row-offset---row-preceding-the-finl-phase)))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defun    (tx-finl---sender-address-hi)       (shift    transaction/FROM_ADDRESS_HI        tx-finl---row-offset---TXN))
+(defun    (tx-finl---sender-address-lo)       (shift    transaction/FROM_ADDRESS_LO        tx-finl---row-offset---TXN))
+(defun    (tx-finl---coinbase-address-hi)     (shift    transaction/COINBASE_ADDRESS_HI    tx-finl---row-offset---TXN))
+(defun    (tx-finl---coinbase-address-lo)     (shift    transaction/COINBASE_ADDRESS_LO    tx-finl---row-offset---TXN))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defun    (tx-finl---effective-gas-price)     (shift    transaction/GAS_PRICE              tx-finl---row-offset---TXN))
+(defun    (tx-finl---effective-gas-refund)    (shift    transaction/REFUND_EFFECTIVE       tx-finl---row-offset---TXN))
+(defun    (tx-finl---sender-gas-refund)       (*        (tx-finl---effective-gas-price)    (tx-finl---effective-gas-refund)))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defun    (tx-finl---priority-fee-per-gas)    (shift    transaction/PRIORITY_FEE_PER_GAS   tx-finl---row-offset---TXN))
+(defun    (tx-finl---gas-limit)               (shift    transaction/GAS_LIMIT              tx-finl---row-offset---TXN))
+(defun    (tx-finl---coinbase-reward)         (*        (-   (tx-finl---gas-limit)   (tx-finl---effective-gas-refund))    (tx-finl---priority-fee-per-gas)))