Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SELFDESTRUCT typo fix #542

Merged
merged 3 commits into from
Dec 9, 2024
Merged

SELFDESTRUCT typo fix #542

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6186da8
ras: formatting
OlivierBBB Dec 9, 2024
ab0e7b1
fix: guard fix
OlivierBBB Dec 9, 2024
3ca3ba5
fix: using the right row offsets
OlivierBBB Dec 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 36 additions & 24 deletions hub/constraints/instruction-handling/halting/selfdestruct.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,9 @@
0)
))))

(defconstraint selfdestruct-instruction---setting-code-and-deployment-for-the-first-account-row (:guard (selfdestruct-instruction---scenario-precondition))
(defconstraint selfdestruct-instruction---setting-code-and-deployment-for-the-first-account-row
(:guard (selfdestruct-instruction---scenario-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-zero (selfdestruct-instruction---STATICX)
(begin
(if-not-zero XAHOY
Expand All @@ -232,7 +234,9 @@
(eq! (shift account/DEPLOYMENT_STATUS_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW) 0)
(account-same-deployment-number ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW)))))))

(defconstraint selfdestruct-instruction---setting-balance-and-marked-for-SELFDESTRUCT-for-first-account-row (:guard (selfdestruct-instruction---scenario-precondition))
(defconstraint selfdestruct-instruction---setting-balance-and-marked-for-SELFDESTRUCT-for-first-account-row
(:guard (selfdestruct-instruction---scenario-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-zero (selfdestruct-instruction---STATICX)
(begin
(if-not-zero (selfdestruct-instruction---OOGX)
Expand All @@ -244,7 +248,9 @@
(if-not-zero scenario/SELFDESTRUCT_WONT_REVERT_ALREADY_MARKED (account-same-marked-for-selfdestruct ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW))
(if-not-zero scenario/SELFDESTRUCT_WONT_REVERT_NOT_YET_MARKED (account-mark-account-for-selfdestruct ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW)))))

(defconstraint selfdestruct-instruction---generalities-for-the-second-account-row (:guard (selfdestruct-instruction---scenario-precondition))
(defconstraint selfdestruct-instruction---generalities-for-the-second-account-row
(:guard (selfdestruct-instruction---scenario-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(begin
(if-zero (selfdestruct-instruction---STATICX)
(begin
Expand All @@ -260,7 +266,9 @@
(account-same-marked-for-selfdestruct ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW)
(DOM-SUB-stamps---standard ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW 1 )))))

(defconstraint selfdestruct-instruction---balance-and-warmth-for-second-account-row (:guard (selfdestruct-instruction---scenario-precondition))
(defconstraint selfdestruct-instruction---balance-and-warmth-for-second-account-row
(:guard (selfdestruct-instruction---scenario-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(begin
(if-not-zero (selfdestruct-instruction---OOGX)
(begin
Expand Down Expand Up @@ -297,10 +305,11 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (selfdestruct-instruction---scenario-WILL_REVERT-precondition) (* PEEK_AT_SCENARIO
scenario/SELFDESTRUCT_WILL_REVERT))
(defun (selfdestruct-instruction---scenario-WILL_REVERT-precondition) (* PEEK_AT_SCENARIO scenario/SELFDESTRUCT_WILL_REVERT))

(defconstraint selfdestruct-instruction---first-undoing-row-for-WILL_REVERT-scenario (:guard (selfdestruct-instruction---scenario-WILL_REVERT-precondition))
(defconstraint selfdestruct-instruction---first-undoing-row-for-WILL_REVERT-scenario
(:guard (selfdestruct-instruction---scenario-WILL_REVERT-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(begin
(debug (eq! (shift account/ROMLEX_FLAG ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0))
(debug (eq! (shift account/TRM_FLAG ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0))
Expand All @@ -313,7 +322,9 @@
(account-same-marked-for-selfdestruct ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)
(DOM-SUB-stamps---revert-with-current ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW 2)))

(defconstraint selfdestruct-instruction---second-undoing-row-for-WILL_REVERT-scenario (:guard (selfdestruct-instruction---scenario-WILL_REVERT-precondition))
(defconstraint selfdestruct-instruction---second-undoing-row-for-WILL_REVERT-scenario
(:guard (selfdestruct-instruction---scenario-WILL_REVERT-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(begin
(debug (eq! (shift account/ROMLEX_FLAG ROFF_SELFDESTRUCT___ACCOUNT___2ND_UNDOING_ROW) 0))
(debug (eq! (shift account/TRM_FLAG ROFF_SELFDESTRUCT___ACCOUNT___2ND_UNDOING_ROW) 0))
Expand All @@ -332,21 +343,22 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition) (* PEEK_AT_SCENARIO
(scenario/SELFDESTRUCT_WONT_REVERT_NOT_YET_MARKED)))
(defun (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition) (* PEEK_AT_SCENARIO scenario/SELFDESTRUCT_WONT_REVERT_NOT_YET_MARKED))

(defconstraint selfdestruct-instruction---first-undoing-row-for-WONT_REVERT_NOT_YET_MARKED-scenario (:guard (selfdestruct-instruction---scenario-WILL_REVERT-precondition))
(defconstraint selfdestruct-instruction---account-deletion-row
(:guard (selfdestruct-instruction---scenario-WONT_REVERT_NOT_YET_MARKED-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we

  • rename constraint to account-deletion-row
  • we use the correct guard

(begin
(debug (eq! (shift account/ROMLEX_FLAG ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0))
(debug (eq! (shift account/TRM_FLAG ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0))
(account-same-address-as ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW ROFF_SELFDESTRUCT___ACCOUNT___1ST_DOING_ROW)
(eq! (shift account/BALANCE_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0)
(eq! (shift account/NONCE_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0)
(account-same-warmth ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)
(eq! (shift account/CODE_SIZE_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) 0)
(eq! (shift account/CODE_HASH_HI_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) EMPTY_KECCAK_HI)
(eq! (shift account/CODE_HASH_LO_NEW ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW) EMPTY_KECCAK_LO)
(shift (eq! account/DEPLOYMENT_NUMBER_NEW (+ 1 account/DEPLOYMENT_NUMBER)) ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)
(shift (eq! account/DEPLOYMENT_STATUS_NEW 0 ) ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)
(account-same-marked-for-selfdestruct ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)
(selfdestruct-dom-sub-stamps ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW)))
(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)
(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)
(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)))
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we use the right row offset (numerically the two are equal)

old: ROFF_SELFDESTRUCT___ACCOUNT___1ST_UNDOING_ROW
new: ROFF_SELFDESTRUCT___ACCOUNT_DELETION_ROW

Loading