Re-enabling certain lookups + TXN instructions fix (#539)

Consensys · Dec 9, 2024 · 2cf716a · 2cf716a
1 parent de15d81
commit 2cf716a
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 12 deletions.
diff --git a/hub/constraints/generalities/jump_destination_vetting.lisp b/hub/constraints/generalities/jump_destination_vetting.lisp
@@ -6,7 +6,9 @@
 ;;                                          ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defconstraint jump-destination- (:guard PEEK_AT_STACK)
+(defconstraint jump-destination-vetting
+               (:guard PEEK_AT_STACK)
+               ;;;;;;;;;;;;;;;;;;;;;;
                (begin
                  (debug (is-binary stack/JUMP_DESTINATION_VETTING_REQUIRED))
                  (if-zero (force-bin stack/JUMP_FLAG)

diff --git a/hub/constraints/instruction-handling/txn.lisp b/hub/constraints/instruction-handling/txn.lisp
@@ -13,28 +13,35 @@
 
 (defconstraint    txn-instruction---setting-the-stack-pattern
                   (:guard (txn-instruction---standard-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (stack-pattern-0-1))
 
 (defconstraint    txn-instruction---setting-NSR
                   (:guard (txn-instruction---standard-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (eq! NSR (+ 1 CMC)))
 
 (defconstraint    txn-instruction---setting-the-peeking-flags
                   (:guard (txn-instruction---standard-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (eq! NSR
                        (+ (shift     PEEK_AT_TRANSACTION  roff---txn-instruction---transaction-row)
                           (* (shift  PEEK_AT_CONTEXT      roff---txn-instruction---exceptional-context-row) CMC))))
 
 (defconstraint    txn-instruction---setting-the-gas-cost
                   (:guard (txn-instruction---standard-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (eq! GAS_COST stack/STATIC_GAS))
 
 (defconstraint    txn-instruction---setting-the-result
                   (:guard (txn-instruction---standard-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (begin
-                    (if-not-zero    (txn-instruction---is-ORIGIN)
-                                    (begin (eq! (txn-instruction---result-hi) (shift   transaction/FROM_ADDRESS_HI   roff---txn-instruction---transaction-row))
-                                           (eq! (txn-instruction---result-lo) (shift   transaction/FROM_ADDRESS_LO   roff---txn-instruction---transaction-row))))
-                    (if-not-zero    (txn-instruction---is-GASPRICE)
-                                    (begin (eq! (txn-instruction---result-hi) 0)
-                                           (eq! (txn-instruction---result-lo) (shift   transaction/GAS_PRICE         roff---txn-instruction---transaction-row))))))
+                    (if-zero    XAHOY
+                                (begin
+                                  (if-not-zero    (txn-instruction---is-ORIGIN)
+                                                  (begin (eq! (txn-instruction---result-hi) (shift   transaction/FROM_ADDRESS_HI   roff---txn-instruction---transaction-row))
+                                                         (eq! (txn-instruction---result-lo) (shift   transaction/FROM_ADDRESS_LO   roff---txn-instruction---transaction-row))))
+                                  (if-not-zero    (txn-instruction---is-GASPRICE)
+                                                  (begin (eq! (txn-instruction---result-hi) 0)
+                                                         (eq! (txn-instruction---result-lo) (shift   transaction/GAS_PRICE         roff---txn-instruction---transaction-row))))))))
diff --git a/rlptxn/lookups/rlp_txn_into_hub.lispX b/rlptxn/lookups/rlp_txn_into_hub.lispX
@@ -1,10 +1,10 @@
 (defun (rlp-txn-into-hub-src-selector) (* rlptxn.REQUIRES_EVM_EXECUTION rlptxn.IS_PHASE_ACCESS_LIST (- 1 rlptxn.IS_PREFIX)))
 
-;(defun (prewarming-phase-address-hi)       (+ (* hub.PEEK_AT_ACCOUNT hub.account/ADDRESS_HI) (* hub.PEEK_AT_STORAGE hub.storage/ADDRESS_HI)))
-;(defun (prewarming-phase-address-lo)       (+ (* hub.PEEK_AT_ACCOUNT hub.account/ADDRESS_LO) (* hub.PEEK_AT_STORAGE hub.storage/ADDRESS_LO)))
-;(defun (prewarming-phase-storage-key-hi)   (* hub.PEEK_AT_STORAGE hub.storage/STORAGE_KEY_HI))
-;(defun (prewarming-phase-storage-key-lo)   (* hub.PEEK_AT_STORAGE hub.storage/STORAGE_KEY_LO))
-;(defun (rlp-txn-depth-2)                   [rlptxn.DEPTH 2])
+(defun (prewarming-phase-address-hi)       (+ (* hub.PEEK_AT_ACCOUNT hub.account/ADDRESS_HI) (* hub.PEEK_AT_STORAGE hub.storage/ADDRESS_HI)))
+(defun (prewarming-phase-address-lo)       (+ (* hub.PEEK_AT_ACCOUNT hub.account/ADDRESS_LO) (* hub.PEEK_AT_STORAGE hub.storage/ADDRESS_LO)))
+(defun (prewarming-phase-storage-key-hi)   (* hub.PEEK_AT_STORAGE hub.storage/STORAGE_KEY_HI))
+(defun (prewarming-phase-storage-key-lo)   (* hub.PEEK_AT_STORAGE hub.storage/STORAGE_KEY_LO))
+(defun (rlp-txn-depth-2)                   [rlptxn.DEPTH 2]) ;; ""
 
 (deflookup 
   rlptxn-into-hub

diff --git a/txndata/lookups/txndata_into_hub.lispX → txndata/lookups/txndata_into_hub.lisp b/txndata/lookups/txndata_into_hub.lispX → txndata/lookups/txndata_into_hub.lisp