ras: splitting SELFDESTRUCT's account deletion row constraint

Consensys · Feb 4, 2025 · d97f818 · d97f818
1 parent 0651561
commit d97f818
Showing 1 changed file with 47 additions and 10 deletions.
diff --git a/hub/constraints/instruction-handling/halting/selfdestruct.lisp b/hub/constraints/instruction-handling/halting/selfdestruct.lisp
@@ -345,20 +345,57 @@
 
 (defun    (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition)    (*    PEEK_AT_SCENARIO    scenario/SELFDESTRUCT_WONT_REVERT_NOT_YET_MARKED))
 
-(defconstraint    selfdestruct-instruction---account-deletion-row
+
+
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---flags
                   (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
                   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                   (begin
                     (debug (eq! (shift account/ROMLEX_FLAG           ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0))
-                    (debug (eq! (shift account/TRM_FLAG              ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0))
-                    (account-same-address-as                         ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW      ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW)
-                    (eq!        (shift account/BALANCE_NEW           ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0)
-                    (eq!        (shift account/NONCE_NEW             ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0)
-                    (account-same-warmth                             ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)
+                    (debug (eq! (shift account/TRM_FLAG              ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0))))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---address-duplication
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (account-same-address-as                         ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW      ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---balance-squashing
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (eq!        (shift account/BALANCE_NEW           ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---nonce-squashing
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (eq!        (shift account/NONCE_NEW             ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---no-change-in-warmth
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (account-same-warmth                             ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---code-squashing
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (begin
                     (eq!        (shift account/CODE_SIZE_NEW         ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) 0)
                     (eq!        (shift account/CODE_HASH_HI_NEW      ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) EMPTY_KECCAK_HI)
-                    (eq!        (shift account/CODE_HASH_LO_NEW      ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) EMPTY_KECCAK_LO)
+                    (eq!        (shift account/CODE_HASH_LO_NEW      ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW) EMPTY_KECCAK_LO)))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---fresh-new-deployment
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (begin
                     (shift      (eq!   account/DEPLOYMENT_NUMBER_NEW (+ 1 account/DEPLOYMENT_NUMBER))                   ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)
-                    (shift      (eq!   account/DEPLOYMENT_STATUS_NEW 0                              )                   ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)
-                    (account-same-marked-for-selfdestruct            ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)
-                    (selfdestruct-dom-sub-stamps                     ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)))
+                    (shift      (eq!   account/DEPLOYMENT_STATUS_NEW 0                              )                   ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW)))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---no-change-in-MARKED_FOR_SELFDESTRUCT
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (account-same-marked-for-selfdestruct            ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW))
+
+(defconstraint    selfdestruct-instruction---account-deletion-row---DOM_SUB-stamps
+                  (:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
+                  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                  (selfdestruct-dom-sub-stamps                     ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW))