EIP-3855: PUSH0

constants/constants.lisp

@@ -75,6 +75,7 @@
   EVM_INST_GAS                              0x5A
   EVM_INST_JUMPDEST                         0x5B
   ;; Push Operations
+  EVM_INST_PUSH0                            0x5F
   EVM_INST_PUSH1                            0x60
   EVM_INST_PUSH2                            0x61
   EVM_INST_PUSH3                            0x62

hub/constraints/instruction-handling/push_pop.lisp

@@ -4,7 +4,8 @@
 (defun    (push-pop-instruction---result-hi)             [ stack/STACK_ITEM_VALUE_HI  4 ])
 (defun    (push-pop-instruction---result-lo)             [ stack/STACK_ITEM_VALUE_LO  4 ])
 (defun    (push-pop-instruction---is-POP)                [ stack/DEC_FLAG             1 ])
-(defun    (push-pop-instruction---is-PUSH)               [ stack/DEC_FLAG             2 ]) ;; ""
+(defun    (push-pop-instruction---is-PUSH)               [ stack/DEC_FLAG             2 ])
+(defun    (push-pop-instruction---is-PUSH-ZERO)          [ stack/DEC_FLAG             3 ]) ;; ""
 
 (defconstraint    push-pop-instruction---setting-the-stack-pattern---POP-case
                   (:guard (push-pop-instruction---standard-hypothesis))
@@ -13,7 +14,7 @@
 
 (defconstraint    push-pop-instruction---setting-the-stack-pattern---PUSH-case
                   (:guard (push-pop-instruction---standard-hypothesis))
-                  (if-not-zero (push-pop-instruction---is-PUSH)
+                  (if-not-zero (+ (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO) )
                                (stack-pattern-0-1)))
 
 (defconstraint    push-pop-instruction---setting-NSR
@@ -36,6 +37,12 @@
                                (begin (eq! (push-pop-instruction---result-hi) stack/PUSH_VALUE_HI)
                                       (eq! (push-pop-instruction---result-lo) stack/PUSH_VALUE_LO))))
 
+(defconstraint    push-pop-instruction---setting-stack-values---PUSH0-case
+                  (:guard (push-pop-instruction---standard-hypothesis))
+                  (if-not-zero (push-pop-instruction---is-PUSH-ZERO)
+                               (begin (vanishes! (push-pop-instruction---result-hi))
+                                      (vanishes! (push-pop-instruction---result-lo)))))
+
 (defconstraint    push-pop-instruction---setting-PC_NEW---POP-case
                   (:guard (push-pop-instruction---standard-hypothesis))
                   (if-not-zero (push-pop-instruction---is-POP)