feat: TXN instructions write the result only if unexceptional

Consensys · Dec 8, 2024 · ec0aca8 · ec0aca8
1 parent 92c2432
commit ec0aca8
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 7 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))))))))