Skip to content

Commit

Permalink
RETURNDATACOPY must always load the current execution context (#449)
Browse files Browse the repository at this point in the history
  • Loading branch information
@OlivierBBB
OlivierBBB authored Oct 14, 2024
1 parent 7c4b705 commit 9c78cc9
Show file tree
Hide file tree
Showing 9 changed files with 399 additions and 428 deletions.
17 changes: 9 additions & 8 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,11 +79,10 @@ MMU := $(wildcard mmu/*.lisp) \
$(wildcard mmu/instructions/*.lisp) \
$(wildcard mmu/instructions/any_to_ram_with_padding/*.lisp)

MMIO := mmio/columns.lisp
MMIO_COLUMNS := mmio/columns.lisp

# TODO enable the MMIO constraint and lookup
# $(wildcard mmio/*lisp) \
# $(wildcard mmio/lookups/*lisp) \
MMIO := $(wildcard mmio/*lisp) \
$(wildcard mmio/lookups/*lisp) \

MXP := mxp

Expand Down Expand Up @@ -140,7 +139,7 @@ ZKEVM_MODULES := ${ALU} \
${LOG_DATA} \
${LOG_INFO} \
${MMU} \
${MMIO} \
${MMIO_COLUMNS} \
${MXP} \
${OOB} \
${RLP_ADDR} \
Expand All @@ -156,8 +155,9 @@ ZKEVM_MODULES := ${ALU} \
${TXN_DATA} \
${WCP}

# ${HUB} \
# ${GAS} \
# ${HUB} \
# ${MMIO} \
define.go: ${ZKEVM_MODULES}
${CORSET} wizard-iop -vv -o $@ ${ZKEVM_MODULES}
Expand All @@ -180,7 +180,7 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \
${LOG_DATA} \
${LOG_INFO} \
${MMU} \
${MMIO} \
${MMIO_COLUMNS} \
${MXP} \
${OOB} \
${RLP_ADDR} \
Expand All @@ -197,8 +197,9 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \
${WCP}

# ${BLOCKDATA} \
# ${HUB} \
# ${GAS} \
# ${HUB} \
# ${MMIO} \
zkevm_for_reference_tests.bin: ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
${CORSET} compile -vv -o $@ ${ZKEVM_MODULES_FOR_REFERENCE_TESTS}
2 changes: 1 addition & 1 deletion gas/columns.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
(FIRST :binary@prove)
(CT :i3)
(CT_MAX :i3)
(GAS_ACTUAL :i32)
(GAS_ACTUAL :i64)
(GAS_COST :i64)
(EXCEPTIONS_AHOY :binary@prove)
(OUT_OF_GAS_EXCEPTION :binary@prove)
Expand Down
417 changes: 0 additions & 417 deletions hub/constraints/instruction-handling/copy.lisp
View file

This file was deleted.

21 changes: 21 additions & 0 deletions hub/constraints/instruction-handling/copy/calldatacopy.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.4 Specifics for CALLDATACOPY ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint copy-instruction---CALLDATACOPY---setting-the-gas-cost (:guard (copy-instruction---standard-CALLDATACOPY))
(begin (if-not-zero stack/MXPX
(vanishes! GAS_COST))
(if-not-zero stack/OOGX
(eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))
(if-zero XAHOY
(eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))))

(defconstraint copy-instruction---CALLDATACOPY---setting-context-row---exceptional-case (:guard (copy-instruction---standard-CALLDATACOPY))
(if-not-zero XAHOY
(execution-provides-empty-return-data ROW_OFFSET_CALLDATACOPY_CONTEXT_ROW)
(read-context-data ROW_OFFSET_CALLDATACOPY_CONTEXT_ROW CONTEXT_NUMBER)))

39 changes: 39 additions & 0 deletions hub/constraints/instruction-handling/copy/codecopy.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.6 Specifics for CODECOPY ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint copy-instruction---CODECOPY---setting-the-gas-cost (:guard (copy-instruction---standard-CODECOPY))
(begin (if-not-zero stack/MXPX
(vanishes! GAS_COST))
(if-not-zero stack/OOGX
(eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))
(if-zero XAHOY
(eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))))

(defconstraint copy-instruction---CODECOPY---setting-the-context-row---exceptional-case (:guard (copy-instruction---standard-CODECOPY))
(if-not-zero XAHOY
(execution-provides-empty-return-data ROW_OFFSET_CODECOPY_XAHOY_CONTEXT_ROW)))

(defconstraint copy-instruction---CODECOPY---setting-the-context-row-unexceptional-case (:guard (copy-instruction---standard-CODECOPY))
(if-zero XAHOY
(read-context-data ROW_OFFSET_CODECOPY_XAHOY_CONTEXT_ROW CONTEXT_NUMBER)))

(defconstraint copy-instruction---CODECOPY---setting-the-account-row---unexceptional-case (:guard (copy-instruction---standard-CODECOPY))
(if-zero XAHOY
(begin (eq! (shift account/ADDRESS_HI ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW) (shift context/BYTE_CODE_ADDRESS_HI ROW_OFFSET_CODECOPY_NO_XAHOY_CONTEXT_ROW))
(eq! (shift account/ADDRESS_LO ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW) (shift context/BYTE_CODE_ADDRESS_LO ROW_OFFSET_CODECOPY_NO_XAHOY_CONTEXT_ROW))
(eq! (shift account/DEPLOYMENT_NUMBER ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW) (shift context/BYTE_CODE_CODE_FRAGMENT_INDEX ROW_OFFSET_CODECOPY_NO_XAHOY_CONTEXT_ROW))
(eq! (shift account/CODE_FRAGMENT_INDEX ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW) CODE_FRAGMENT_INDEX)
(eq! (shift account/ROMLEX_FLAG ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW) 1)
(account-same-balance ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(account-same-nonce ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(account-same-code ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(account-same-deployment-number-and-status ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(account-same-warmth ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(account-same-marked-for-selfdestruct ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW)
(DOM-SUB-stamps---standard ROW_OFFSET_CODECOPY_NO_XAHOY_ACCOUNT_ROW 0))))

79 changes: 79 additions & 0 deletions hub/constraints/instruction-handling/copy/extcodecopy.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.7 Specifics for EXTCODECOPY ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint copy-instruction---EXTCODECOPY---setting-the-gas-cost (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero stack/MXPX
;; MXPX ≡ 1
(vanishes! GAS_COST)
;; MXPX ≡ 0
(eq! GAS_COST
(+ stack/STATIC_GAS
(copy-instruction---MXP-memory-expansion-gas)
(* (copy-instruction---exo-address-warmth) GAS_CONST_G_WARM_ACCESS)
(* (- 1 (copy-instruction---exo-address-warmth)) GAS_CONST_G_COLD_ACCOUNT_ACCESS)))))

(defconstraint copy-instruction---EXTCODECOPY---the-MXPX-case (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero stack/MXPX
(execution-provides-empty-return-data ROW_OFFSET_EXTCODECOPY_MXPX_CONTEXT_ROW)))

(defconstraint copy-instruction---EXTCODECOPY---the-OOGX-case (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero stack/OOGX
;; account-row i + 2
(begin (account-trim-address ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW (copy-instruction---raw-address-hi) (copy-instruction---raw-address-lo))
(vanishes! (shift account/ROMLEX_FLAG ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW))
(account-same-balance ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(account-same-nonce ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(account-same-code ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(account-same-deployment-number-and-status ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(account-same-warmth ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(account-same-marked-for-selfdestruct ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW)
(DOM-SUB-stamps---standard ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW 0))
;; context-row i + 3
(execution-provides-empty-return-data ROW_OFFSET_EXTCODECOPY_OOGX_CONTEXT_ROW)))

(defun (copy-instruction---trigger-CFI)
(* (copy-instruction---is-EXTCODECOPY)
(copy-instruction---trigger_MMU)
(copy-instruction---exo-address-has-code)))

(defconstraint copy-instruction---unexceptional-reverted-EXTCODECOPY---doing-account-row (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero (* (- 1 XAHOY) CONTEXT_WILL_REVERT)
(begin (account-trim-address ROW_OFFSET_EXTCODECOPY_OOGX_ACCOUNT_ROW (copy-instruction---raw-address-hi) (copy-instruction---raw-address-lo))
(eq! (shift account/ROMLEX_FLAG ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW) (copy-instruction---trigger-CFI))
(account-same-balance ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-same-nonce ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-same-code ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-same-deployment-number-and-status ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-turn-on-warmth ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-same-marked-for-selfdestruct ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(DOM-SUB-stamps---standard ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW 0))))

(defconstraint copy-instruction---unexceptional-reverted-EXTCODECOPY---undoing-account-row (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero (* (- 1 XAHOY) CONTEXT_WILL_REVERT)
(begin (account-same-address-as ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(debug (vanishes! (shift account/ROMLEX_FLAG ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW)))
(account-undo-balance-update ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-undo-nonce-update ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-undo-code-update ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-undo-deployment-status-update ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-undo-warmth-update ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_DOING_ROW)
(account-same-marked-for-selfdestruct ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW)
(DOM-SUB-stamps---revert-with-current ROW_OFFSET_EXTCODECOPY_NO_XAHOY_REVERT_ACCOUNT_UNDOING_ROW 1))))

(defconstraint copy-instruction---unexceptional-unreverted-EXTCODECOPY-account-row (:guard (copy-instruction---standard-EXTCODECOPY))
(if-not-zero (* (- 1 XAHOY) (- 1 CONTEXT_WILL_REVERT))
(begin (account-trim-address ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW (copy-instruction---raw-address-hi) (copy-instruction---raw-address-lo))
(eq! (shift account/ROMLEX_FLAG ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW) (copy-instruction---trigger-CFI))
(account-same-balance ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(account-same-nonce ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(account-same-code ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(account-same-deployment-number-and-status ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(account-turn-on-warmth ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(account-same-marked-for-selfdestruct ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW)
(DOM-SUB-stamps---standard ROW_OFFSET_EXTCODECOPY_NO_XAHOY_NO_REVERT_ACCOUNT_ROW 0))))

Loading

0 comments on commit 9c78cc9

Please sign in to comment.