Skip to content

feat: shanghai hard fork #647

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

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
Draft

feat: shanghai hard fork #647

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
cdef343
EIP-3651: warm coinbase (#635)
letypequividelespoubelles Apr 11, 2025
8b5cce3
Merge branch 'master' into shanghai-hard-fork
letypequividelespoubelles Apr 29, 2025
f5ae0b3
EIP-3855: PUSH0 (#640)
letypequividelespoubelles Apr 29, 2025
3947b53
PUSH0 constraint is after SHANGHAI
letypequividelespoubelles Apr 29, 2025
62b0dd6
PUSH0 shorthand
letypequividelespoubelles Apr 29, 2025
28df989
EIP-3860: Limit and meter initcode (#644)
OlivierBBB Apr 29, 2025
fa6fed9
ras: resize of inst columns
letypequividelespoubelles May 5, 2025
4fdb02c
fix typo
letypequividelespoubelles May 7, 2025
c9cc670
fix typo
letypequividelespoubelles May 7, 2025
060f54f
delete duplicate file
letypequividelespoubelles May 8, 2025
39a2dfc
fix typo
letypequividelespoubelles May 8, 2025
a56a35e
add shanghai et london txn data constant
letypequividelespoubelles May 13, 2025
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
12 changes: 12 additions & 0 deletions constants/constants.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,16 @@
(defconst
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM Forks ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
EVM_LONDON 14
EVM_PARIS (+ 1 EVM_LONDON)
EVM_SHANGHAI (+ 2 EVM_LONDON)
EVM_CANCUN (+ 3 EVM_LONDON)
EVM_PRAGUE (+ 4 EVM_LONDON)
;; Default fork
(EVM_FORK :i8 :extern) EVM_LONDON
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM INSTRUCTIONS ;;
Expand Down
Binary file added debug.bin
View file
Open in desktop
Binary file not shown.
6 changes: 3 additions & 3 deletions hub/columns/miscellaneous.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,11 @@
( STP_FLAG :binary@prove )

;; EXP columns (DONE)
( EXP_INST :i32 )
( EXP_INST :i16 )
( EXP_DATA :array [5] :i128 )

;; MMU columns (DONE)
( MMU_INST :i32 :display :hex)
( MMU_INST :i16 :display :hex)
( MMU_SRC_ID :i32 )
( MMU_TGT_ID :i32 )
( MMU_AUX_ID :i32 )
Expand All @@ -34,7 +34,7 @@
( MMU_EXO_SUM :i32 )

;; MXP colummns
( MXP_INST :i32 )
( MXP_INST :byte )
( MXP_MXPX :binary )
( MXP_DEPLOYS :binary )
( MXP_OFFSET_1_HI :i128 )
Expand Down
24 changes: 6 additions & 18 deletions hub/constraints/generalities/exceptions.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,23 +42,6 @@



;; ;; These columns are already marked binary@prove in their respective definitions
;; (defconstraint generalities---exceptions---stack-exception-flags-are-binary (:perspective stack)
;; (begin
;; (is-binary SUX )
;; (is-binary SOX )
;; (is-binary MXPX )
;; (is-binary OOGX )
;; (is-binary RDCX )
;; (is-binary JUMPX )
;; (is-binary STATICX )
;; (is-binary SSTOREX )
;; (is-binary ICPX )
;; (is-binary MAXCSX )
;; (is-binary OPCX )
;; ))


(defconstraint generalities---exceptions---stack-exception-flags-are-exclusive (:perspective stack)
(is-binary (exception_flag_sum)))

Expand All @@ -82,7 +65,12 @@
(if-zero STATIC_FLAG (vanishes! STATICX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURNDATACOPY) (vanishes! RDCX))
(if-not-zero (- INSTRUCTION EVM_INST_SSTORE) (vanishes! SSTOREX))
(if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! (+ ICPX MAXCSX)))))
(if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! ICPX))
(if-not-zero (* (- INSTRUCTION EVM_INST_RETURN)
(- 1 CREATE_FLAG))
(vanishes! MAXCSX))
)
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down
4 changes: 2 additions & 2 deletions hub/constraints/instruction-handling/create/constants.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,10 @@
;; Empty initialization code (will or won't revert)
CREATE_empty_init_code_will_revert_current_context_row___row_offset 7
CREATE_empty_init_code_wont_revert_current_context_row___row_offset 5
;; Nonmpty initialization code failure (will or won't revert)
;; Nonempty initialization code failure (will or won't revert)
CREATE_nonempty_init_code_failure_will_revert_new_context_row___row_offset 9
CREATE_nonempty_init_code_failure_wont_revert_new_context_row___row_offset 7
;; Nonmpty initialization code success (will or won't revert)
;; Nonempty initialization code success (will or won't revert)
CREATE_nonempty_init_code_success_will_revert_new_context_row___row_offset 7
CREATE_nonempty_init_code_success_wont_revert_new_context_row___row_offset 5
)
Expand Down
14 changes: 12 additions & 2 deletions hub/constraints/instruction-handling/create/constraints/generalities.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,19 @@
(create-instruction---STP-oogx))
))

(defconstraint create-instruction---setting-the-OOB-instruction
(defconstraint create-instruction---setting-the-OOB-instruction---exceptional-case
(:guard (create-instruction---generic-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (shift misc/OOB_FLAG CREATE_miscellaneous_row___row_offset)
(if-not-zero (create-instruction---trigger_OOB_X)
(set-OOB-instruction---xcreate CREATE_miscellaneous_row___row_offset ;; offset
(create-instruction---STACK-size-hi) ;; init code size (high part)
(create-instruction---STACK-size-lo) ;; init code size (low part, stack argument of CREATE-type instruction)
)))

(defconstraint create-instruction---setting-the-OOB-instruction---unexceptional-case
(:guard (create-instruction---generic-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (create-instruction---trigger_OOB_U)
(set-OOB-instruction---create CREATE_miscellaneous_row___row_offset ;; offset
(create-instruction---STACK-value-hi) ;; value (high part)
(create-instruction---STACK-value-lo) ;; value (low part, stack argument of CALL-type instruction)
Expand All @@ -97,6 +106,7 @@
(create-instruction---createe-has-code) ;; callee's HAS_CODE
(create-instruction---current-context-csd) ;; current call stack depth
(create-instruction---creator-nonce) ;; creator account nonce
(create-instruction---init-code-size) ;; init code size
)))

(defun (create-instruction---createe-nonce) (* (scenario-shorthand---CREATE---load-createe-account) (shift account/NONCE CREATE_first_createe_account_row___row_offset)))
Expand Down
3 changes: 2 additions & 1 deletion hub/constraints/instruction-handling/create/non_stack_rows.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@
(defconstraint create-instruction---setting-the-peeking-flags (:guard (create-instruction---standard-precondition))
(eq! (shift NON_STACK_ROWS CREATE_first_stack_row___row_offset)
(+ (* (create-instruction---flag-sum-staticx) (create-instruction---STACK-staticx) )
(+ (* (create-instruction---flag-sum-maxcsx) (create-instruction---STACK-maxcsx) )
(* (create-instruction---flag-sum-mxpx) (create-instruction---STACK-mxpx) )
(* (create-instruction---flag-sum-oogx) (create-instruction---STACK-oogx) )
(* (create-instruction---flag-sum-abort) scenario/CREATE_ABORT )
Expand All @@ -46,4 +47,4 @@
(* (create-instruction---flag-sum-nonempty-init-success-wont-revert) scenario/CREATE_NONEMPTY_INIT_CODE_SUCCESS_WONT_REVERT )
)
)
)
))
4 changes: 4 additions & 0 deletions hub/constraints/instruction-handling/create/peeking_flags_shorthands.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,10 @@
(shift PEEK_AT_CONTEXT CREATE_exception_caller_context_row___row_offset)
))

(defun (create-instruction---flag-sum-maxcsx) (+ (create-instruction---std-prefix)
(shift PEEK_AT_CONTEXT CREATE_exception_caller_context_row___row_offset)
))

(defun (create-instruction---flag-sum-mxpx) (+ (create-instruction---std-prefix)
(shift PEEK_AT_CONTEXT CREATE_exception_caller_context_row___row_offset)
))
Expand Down
1 change: 1 addition & 0 deletions hub/constraints/instruction-handling/create/shorthands.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
(defun (create-instruction---is-CREATE) (shift [stack/DEC_FLAG 1] CREATE_first_stack_row___row_offset))
(defun (create-instruction---is-CREATE2) (shift [stack/DEC_FLAG 2] CREATE_first_stack_row___row_offset))
(defun (create-instruction---STACK-staticx) (shift stack/STATICX CREATE_first_stack_row___row_offset))
(defun (create-instruction---STACK-maxcsx) (shift stack/MAXCSX CREATE_first_stack_row___row_offset))
(defun (create-instruction---STACK-mxpx) (shift stack/MXPX CREATE_first_stack_row___row_offset))
(defun (create-instruction---STACK-oogx) (shift stack/OOGX CREATE_first_stack_row___row_offset))
(defun (create-instruction---STACK-offset-hi) (shift [stack/STACK_ITEM_VALUE_HI 1] CREATE_first_stack_row___row_offset))
Expand Down
5 changes: 4 additions & 1 deletion hub/constraints/instruction-handling/create/triggers.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,10 @@
(defun (create-instruction---trigger_STP) (+ (create-instruction---STACK-oogx)
(scenario-shorthand---CREATE---unexceptional)))

(defun (create-instruction---trigger_OOB) (+ (scenario-shorthand---CREATE---unexceptional)))
(defun (create-instruction---trigger_OOB_X) (+ (create-instruction---STACK-maxcsx) ))
(defun (create-instruction---trigger_OOB_U) (+ (scenario-shorthand---CREATE---unexceptional) ))
(defun (create-instruction---trigger_OOB) (+ (create-instruction---trigger_OOB_X)
(create-instruction---trigger_OOB_U) ))

(defun (create-instruction---trigger_MMU) (+ (create-instruction---hash-init-code)
(create-instruction---hash-init-code-and-send-to-ROM)
Expand Down
21 changes: 16 additions & 5 deletions hub/constraints/instruction-handling/push_pop.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,14 @@
(module hub)

(defun (push-pop-instruction---standard-hypothesis) (* PEEK_AT_STACK stack/PUSHPOP_FLAG (- 1 stack/SUX stack/SOX)))
(defun (push-pop-instruction---standard-hypothesis) (force-bin (* PEEK_AT_STACK stack/PUSHPOP_FLAG (- 1 stack/SUX stack/SOX))))
(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)
(if (>= EVM_FORK EVM_SHANGHAI)
[ stack/DEC_FLAG 3 ]
0)) ;; ""

(defconstraint push-pop-instruction---setting-the-stack-pattern---POP-case
(:guard (push-pop-instruction---standard-hypothesis))
Expand All @@ -13,7 +17,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 (force-bin (+ (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO)))
(stack-pattern-0-1)))

(defconstraint push-pop-instruction---setting-NSR
Expand All @@ -36,12 +40,19 @@
(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 (>= EVM_FORK EVM_SHANGHAI)
(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)
(eq! PC_NEW (+ 1 PC))))

(defconstraint push-pop-instruction---setting-PC_NEW---PUSH-case
(:guard (push-pop-instruction---standard-hypothesis))
(if-not-zero (push-pop-instruction---is-PUSH)
(eq! PC_NEW (+ 1 PC 1 (- stack/INSTRUCTION EVM_INST_PUSH1)))))
(if-not-zero (force-bin (+ (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO)))
(eq! PC_NEW (+ 1 PC (- stack/INSTRUCTION EVM_INST_PUSH0)))))
5 changes: 2 additions & 3 deletions hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_create.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
has_code ;; callee's HAS_CODE
call_stack_depth ;; current call stack depth
creator_nonce ;; creator account nonce
;; init_code_size ;; init code size (it's necessarily small at this point, so only low part required)
init_code_size ;; init code size (it's necessarily small at this point, so only low part required)
) (begin
(eq! (shift misc/OOB_INST kappa) OOB_INST_CREATE )
(eq! (shift (misc_oob_data_1) kappa) value_hi )
Expand All @@ -21,6 +21,5 @@
;; (eq! (shift (misc_oob_data_7) kappa) ) ;; value_is_nonzero
;; (eq! (shift (misc_oob_data_8) kappa) ) ;; aborting condition
(eq! (shift (misc_oob_data_9) kappa) creator_nonce )
;; (eq! (shift (misc_oob_data_10) kappa) init_code_size ) ;; XXXXXX
(eq! (shift (misc_oob_data_10) kappa) init_code_size )
))

3 changes: 0 additions & 3 deletions ...s-rows/oob/opcodes/oob_inst_xcreate.lispX → ...us-rows/oob/opcodes/oob_inst_xcreate.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
(module hub)


;; XXXXXX has to be uncommented (lispX -> lisp)


(defun (set-OOB-instruction---xcreate kappa ;; offset
init_code_size_hi ;; high part of initialization code size argument of CREATE(2)
init_code_size_lo ;; low part of initialization code size argument of CREATE(2)
Expand Down
2 changes: 1 addition & 1 deletion hub/constraints/miscellaneous-rows/oob/shorthands.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,4 +9,4 @@
(defun (misc_oob_data_7) [ misc/OOB_DATA 7 ])
(defun (misc_oob_data_8) [ misc/OOB_DATA 8 ])
(defun (misc_oob_data_9) [ misc/OOB_DATA 9 ])
;; (defun (misc_oob_data_10) [ misc/OOB_DATA 10 ]) ;; XXXXXX
(defun (misc_oob_data_10) [ misc/OOB_DATA 10 ])
11 changes: 7 additions & 4 deletions hub/constraints/tx_init/peeking.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,34 +11,37 @@
(:guard (tx-init---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC)
(shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN))
2))
(shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN)
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---coinbase-warming))
3))

(defconstraint tx-init---setting-peeking-flags---transaction-failure
(:guard (tx-init---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (tx-init---transaction-failure-prediction)
(eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC )
(shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---coinbase-warming)
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-pay-for-gas )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer---undoing )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception---undoing )
(shift PEEK_AT_CONTEXT tx-init---row-offset---CON---context-initialization-row---failure))
8)))
9)))

(defconstraint tx-init---setting-peeking-flags---transaction-success
(:guard (tx-init---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (tx-init---transaction-success-prediction)
(eq! (+ (shift PEEK_AT_MISCELLANEOUS tx-init---row-offset---MISC )
(shift PEEK_AT_TRANSACTION tx-init---row-offset---TXN )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---coinbase-warming)
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-pay-for-gas )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---sender-value-transfer )
(shift PEEK_AT_ACCOUNT tx-init---row-offset---ACC---recipient-value-reception )
(shift PEEK_AT_CONTEXT tx-init---row-offset---CON---context-initialization-row---success))
6)))
7)))

(defconstraint tx-init---justifying-predictions---transaction-failure
(:guard (tx-init---standard-precondition))
Expand Down
Loading
Loading