diff --git a/.gitignore b/.gitignore index f9617934d..edc43359b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +debug.bin zkevm.bin zkevm.go.bin zkevm_for_reference_tests.bin diff --git a/Makefile b/Makefile index b3ae0ac41..10f1c3509 100644 --- a/Makefile +++ b/Makefile @@ -43,6 +43,20 @@ MMIO := mmio MXP := mxp +# mxp cancun version, while waiting for forks feat +# MXPCAN := $(wildcard mxp/mxpcan/columns/*.lisp) \ + $(wildcard mxp/mxpcan/columns/computation/*.lisp) \ + $(wildcard mxp/mxpcan/columns/scenario/*.lisp) \ + $(wildcard mxp/mxpcan/computations/*.lisp) \ + $(wildcard mxp/mxpcan/consistency/*.lisp) \ + $(wildcard mxp/mxpcan/generalities/*.lisp) \ + $(wildcard mxp/mxpcan/generalities/perspectives/*.lisp) \ + $(wildcard mxp/mxpcan/lookups/*.lisp) \ + +# mxp london version, while waiting for forks feat +# MXPLON := $(wildcard mxp/mxplon/*.lisp) \ + $(wildcard mxp/mxplon/lookups/*.lisp) \ + OOB := oob RLP_ADDR := rlpaddr @@ -103,3 +117,10 @@ ZKEVM_MODULES := ${CONSTANTS} \ zkevm.bin: ${ZKEVM_MODULES} ${GO_CORSET_COMPILE} -o $@ ${ZKEVM_MODULES} + +# for debugging purposes + +DEBUGGING := ${CONSTANTS} ${WCP} ${EUC} ${TABLES} + +debug.bin: ${DEBUGGING} + ${GO_CORSET_COMPILE} -o $@ ${DEBUGGING} diff --git a/constants/constants.lisp b/constants/constants.lisp index f214efd85..b564e71ae 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -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 ;; @@ -74,6 +86,7 @@ EVM_INST_MSIZE 0x59 EVM_INST_GAS 0x5A EVM_INST_JUMPDEST 0x5B + EVM_INST_MCOPY 0x5E ;; Push Operations EVM_INST_PUSH0 0x5F ;; post Shanghai EVM_INST_PUSH1 0x60 @@ -486,6 +499,4 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; WCP_INST_GEQ 0x0E - WCP_INST_LEQ 0x0F) - - + WCP_INST_LEQ 0x0F) \ No newline at end of file diff --git a/hub/columns/miscellaneous.lisp b/hub/columns/miscellaneous.lisp index fe13a950c..b57f6e7af 100644 --- a/hub/columns/miscellaneous.lisp +++ b/hub/columns/miscellaneous.lisp @@ -47,7 +47,6 @@ ( MXP_SIZE_2_LO :i128 ) ( MXP_WORDS :i128 ) ( MXP_GAS_MXP :i128 ) - ( MXP_MTNTOP :binary@prove ) ( MXP_SIZE_1_NONZERO_NO_MXPX :binary@prove ) ( MXP_SIZE_2_NONZERO_NO_MXPX :binary@prove ) diff --git a/hub/columns/stack.lisp b/hub/columns/stack.lisp index 4f2c51f27..ae35279a0 100644 --- a/hub/columns/stack.lisp +++ b/hub/columns/stack.lisp @@ -22,6 +22,7 @@ ( CALL_FLAG :binary ) ( CON_FLAG :binary ) ( COPY_FLAG :binary ) + ( MCOPY_FLAG :binary ) ( CREATE_FLAG :binary ) ( DUP_FLAG :binary ) ( EXT_FLAG :binary ) diff --git a/hub/constraints/instruction-handling/call/generalities/universal.lisp b/hub/constraints/instruction-handling/call/generalities/universal.lisp index 1ff627aed..4f90dac55 100644 --- a/hub/constraints/instruction-handling/call/generalities/universal.lisp +++ b/hub/constraints/instruction-handling/call/generalities/universal.lisp @@ -82,17 +82,17 @@ (defconstraint call-instruction---setting-MXP-instruction-parameters (:guard (call-instruction---standard-precondition)) (if-not-zero (shift misc/MXP_FLAG CALL_misc_row___row_offset) - (set-MXP-instruction-type-5 CALL_misc_row___row_offset ;; row offset kappa - (call-instruction---STACK-instruction) ;; instruction - (call-instruction---STACK-cdo-hi) ;; call data offset high - (call-instruction---STACK-cdo-lo) ;; call data offset low - (call-instruction---STACK-cds-hi) ;; call data size high - (call-instruction---STACK-cds-lo) ;; call data size low - (call-instruction---STACK-r@o-hi) ;; return at offset high - (call-instruction---STACK-r@o-lo) ;; return at offset low - (call-instruction---STACK-r@c-hi) ;; return at capacity high - (call-instruction---STACK-r@c-lo) ;; return at capacity low - ) + (set-MXP-instruction---for-CALL-type CALL_misc_row___row_offset ;; row offset kappa + (call-instruction---STACK-instruction) ;; instruction + (call-instruction---STACK-cdo-hi) ;; call data offset high + (call-instruction---STACK-cdo-lo) ;; call data offset low + (call-instruction---STACK-cds-hi) ;; call data size high + (call-instruction---STACK-cds-lo) ;; call data size low + (call-instruction---STACK-r@o-hi) ;; return at offset high + (call-instruction---STACK-r@o-lo) ;; return at offset low + (call-instruction---STACK-r@c-hi) ;; return at capacity high + (call-instruction---STACK-r@c-lo) ;; return at capacity low + ) )) (defconstraint call-instruction---justifying-mxpx (:guard (call-instruction---standard-precondition)) diff --git a/hub/constraints/instruction-handling/copy/generalities.lisp b/hub/constraints/instruction-handling/copy/generalities.lisp index f4ff0c310..0afdf9858 100644 --- a/hub/constraints/instruction-handling/copy/generalities.lisp +++ b/hub/constraints/instruction-handling/copy/generalities.lisp @@ -157,7 +157,7 @@ (defun (copy-instruction---trigger_OOB) (copy-instruction---is-RETURNDATACOPY)) (defun (copy-instruction---trigger_MXP) (- 1 stack/RDCX)) -(defun (copy-instruction---trigger_MMU) (* (- 1 XAHOY) (shift misc/MXP_MTNTOP ROFF_COPY_INST_MISCELLANEOUS_ROW))) +(defun (copy-instruction---trigger_MMU) (* (- 1 XAHOY) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_COPY_INST_MISCELLANEOUS_ROW))) (defconstraint copy-instruction---misc-row---setting-OOB-instruction (:guard (copy-instruction---standard-precondition)) (if-not-zero (shift misc/OOB_FLAG ROFF_COPY_INST_MISCELLANEOUS_ROW) @@ -178,13 +178,13 @@ (defconstraint copy-instruction---misc-row---setting-MXP-instruction (:guard (copy-instruction---standard-precondition)) (if-not-zero (shift misc/MXP_FLAG ROFF_COPY_INST_MISCELLANEOUS_ROW) - (set-MXP-instruction-type-4 ROFF_COPY_INST_MISCELLANEOUS_ROW ;; row offset kappa - stack/INSTRUCTION ;; instruction - 0 ;; deploys (bit modifying the behaviour of RETURN pricing) - (copy-instruction---target-offset-hi) ;; offset high - (copy-instruction---target-offset-lo) ;; offset low - (copy-instruction---size-hi) ;; size high - (copy-instruction---size-lo)))) ;; size low + (set-MXP-instruction---single-mxp-offset-instructions ROFF_COPY_INST_MISCELLANEOUS_ROW ;; row offset kappa + stack/INSTRUCTION ;; instruction + 0 ;; deploys (bit modifying the behaviour of RETURN pricing) + (copy-instruction---target-offset-hi) ;; offset high + (copy-instruction---target-offset-lo) ;; offset low + (copy-instruction---size-hi) ;; size high + (copy-instruction---size-lo)))) ;; size low (defconstraint copy-instruction---misc-row---setting-MXPX (:guard (copy-instruction---standard-precondition)) (if-zero (shift misc/MXP_FLAG ROFF_COPY_INST_MISCELLANEOUS_ROW) diff --git a/hub/constraints/instruction-handling/create/constraints/generalities.lisp b/hub/constraints/instruction-handling/create/constraints/generalities.lisp index 90dacd9d6..335f34e52 100644 --- a/hub/constraints/instruction-handling/create/constraints/generalities.lisp +++ b/hub/constraints/instruction-handling/create/constraints/generalities.lisp @@ -47,13 +47,13 @@ (defconstraint create-instruction---setting-the-MXP-instruction (:guard (create-instruction---generic-precondition)) (if-not-zero (shift misc/MXP_FLAG CREATE_miscellaneous_row___row_offset) - (set-MXP-instruction-type-4 CREATE_miscellaneous_row___row_offset ;; row offset kappa - (create-instruction---instruction) ;; instruction - 0 ;; bit modifying the behaviour of RETURN pricing - (create-instruction---STACK-offset-hi) ;; offset high - (create-instruction---STACK-offset-lo) ;; offset low - (create-instruction---STACK-size-hi) ;; size high - (create-instruction---STACK-size-lo)) ;; size low + (set-MXP-instruction---single-mxp-offset-instructions CREATE_miscellaneous_row___row_offset ;; row offset kappa + (create-instruction---instruction) ;; instruction + 0 ;; bit modifying the behaviour of RETURN pricing + (create-instruction---STACK-offset-hi) ;; offset high + (create-instruction---STACK-offset-lo) ;; offset low + (create-instruction---STACK-size-hi) ;; size high + (create-instruction---STACK-size-lo)) ;; size low )) (defconstraint create-instruction---setting-the-memory-expansion-exception (:guard (create-instruction---generic-precondition)) @@ -126,7 +126,7 @@ (:guard (create-instruction---generic-precondition)) (if-not-zero (scenario-shorthand---CREATE---not-rebuffed) (eq! (scenario-shorthand---CREATE---not-rebuffed-nonempty-init-code) - (create-instruction---MXP-mtntop)))) + (create-instruction---MXP-s1nznomxpx)))) (defconstraint create-instruction---setting-the-CREATE-scenario---not-rebuffed-nonempty-init-code (:guard (create-instruction---generic-precondition)) diff --git a/hub/constraints/instruction-handling/create/shorthands.lisp b/hub/constraints/instruction-handling/create/shorthands.lisp index 9ac31b9f7..57b019437 100644 --- a/hub/constraints/instruction-handling/create/shorthands.lisp +++ b/hub/constraints/instruction-handling/create/shorthands.lisp @@ -45,7 +45,7 @@ (defun (create-instruction---OOB-failure-condition) (shift [misc/OOB_DATA 8] CREATE_miscellaneous_row___row_offset)) (defun (create-instruction---MXP-mxpx) (shift misc/MXP_MXPX CREATE_miscellaneous_row___row_offset)) (defun (create-instruction---MXP-gas) (shift misc/MXP_GAS_MXP CREATE_miscellaneous_row___row_offset)) -(defun (create-instruction---MXP-mtntop) (shift misc/MXP_MTNTOP CREATE_miscellaneous_row___row_offset)) +(defun (create-instruction---MXP-s1nznomxpx) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX CREATE_miscellaneous_row___row_offset)) (defun (create-instruction---STP-gas-paid-out-of-pocket) (shift misc/STP_GAS_PAID_OUT_OF_POCKET CREATE_miscellaneous_row___row_offset)) (defun (create-instruction---STP-oogx) (shift misc/STP_OOGX CREATE_miscellaneous_row___row_offset)) (defun (create-instruction---compute-createe-address) (shift account/RLPADDR_FLAG CREATE_first_creator_account_row___row_offset)) diff --git a/hub/constraints/instruction-handling/create/triggers.lisp b/hub/constraints/instruction-handling/create/triggers.lisp index 9dd326691..443aa1aab 100644 --- a/hub/constraints/instruction-handling/create/triggers.lisp +++ b/hub/constraints/instruction-handling/create/triggers.lisp @@ -30,7 +30,7 @@ (defun (create-instruction---trigger_HASHINFO) (* (create-instruction---is-CREATE2) (+ (* (scenario-shorthand---CREATE---failure-condition) - (create-instruction---MXP-mtntop)) + (create-instruction---MXP-s1nznomxpx)) (scenario-shorthand---CREATE---not-rebuffed-nonempty-init-code)))) (defun (create-instruction---trigger_RLPADDR) (scenario-shorthand---CREATE---compute-deployment-address)) @@ -39,7 +39,7 @@ ;; auxiliary shorthands required for (create-instruction---trigger_MMU) (defun (create-instruction---hash-init-code) (* (scenario-shorthand---CREATE---failure-condition) - (create-instruction---MXP-mtntop) + (create-instruction---MXP-s1nznomxpx) (create-instruction---is-CREATE2))) (defun (create-instruction---hash-init-code-and-send-to-ROM) (* (scenario-shorthand---CREATE---not-rebuffed-nonempty-init-code) diff --git a/hub/constraints/instruction-handling/halting/return.lisp b/hub/constraints/instruction-handling/halting/return.lisp index 7779c74f5..bbf747266 100644 --- a/hub/constraints/instruction-handling/halting/return.lisp +++ b/hub/constraints/instruction-handling/halting/return.lisp @@ -84,13 +84,12 @@ (defun (return-instruction---return-at-capacity) (shift context/RETURN_AT_CAPACITY ROFF_RETURN___CURRENT_CONTEXT_ROW)) (defun (return-instruction---MXP-memory-expansion-gas) (shift misc/MXP_GAS_MXP ROFF_RETURN___1ST_MISC_ROW)) (defun (return-instruction---MXP-memory-expansion-exception) (shift misc/MXP_MXPX ROFF_RETURN___1ST_MISC_ROW)) -(defun (return-instruction---MXP-may-trigger-non-trivial-operation) (shift misc/MXP_MTNTOP ROFF_RETURN___1ST_MISC_ROW)) -(defun (return-instruction---MXP-size-1-is-nonzero-and-no-mxpx) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_RETURN___1ST_MISC_ROW)) +(defun (return-instruction---MXP-s1nznomxpx) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_RETURN___1ST_MISC_ROW)) (defun (return-instruction---MMU-success-bit) (shift misc/MMU_SUCCESS_BIT ROFF_RETURN___1ST_MISC_ROW)) (defun (return-instruction---OOB-max-code-size-exception) (shift [ misc/OOB_DATA 7 ] ROFF_RETURN___1ST_MISC_ROW)) ;; "" (defun (return-instruction---deployment-code-fragment-index) (shift account/CODE_FRAGMENT_INDEX ROFF_RETURN___NONEMPTY_DEPLOYMENT___1ST_ACCOUNT_ROW)) -(defun (return-instruction---type-safe-return-data-offset) (* (return-instruction---offset-lo) (return-instruction---MXP-size-1-is-nonzero-and-no-mxpx))) +(defun (return-instruction---type-safe-return-data-offset) (* (return-instruction---offset-lo) (return-instruction---MXP-s1nznomxpx))) (defun (return-instruction---type-safe-return-data-size) (return-instruction---size-lo)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -207,7 +206,7 @@ (if-not-zero (scenario-shorthand---RETURN---deployment) (begin (eq! (scenario-shorthand---RETURN---deployment-will-revert) CONTEXT_WILL_REVERT) - (eq! (scenario-shorthand---RETURN---nonempty-deployment) (return-instruction---MXP-may-trigger-non-trivial-operation)))) + (eq! (scenario-shorthand---RETURN---nonempty-deployment) (return-instruction---MXP-s1nznomxpx)))) (if-not-zero (scenario-shorthand---RETURN---message-call) (if-zero (return-touch-ram-expression) ;; touch_ram_expression = 0 @@ -217,7 +216,7 @@ )))) (defun (return-touch-ram-expression) (* (- 1 (return-instruction---is-root)) - (return-instruction---MXP-may-trigger-non-trivial-operation) + (return-instruction---MXP-s1nznomxpx) (return-instruction---return-at-capacity) )) @@ -243,15 +242,15 @@ (defconstraint return-instruction---setting-MXP-data (:guard (return-instruction---standard-scenario-row)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (if-not-zero (shift misc/MXP_FLAG ROFF_RETURN___1ST_MISC_ROW) - (set-MXP-instruction-type-4 ROFF_RETURN___1ST_MISC_ROW ;; row offset kappa - (return-instruction---instruction) ;; instruction - (return-instruction---is-deployment) ;; bit modifying the behaviour of RETURN pricing - (return-instruction---offset-hi) ;; offset high - (return-instruction---offset-lo) ;; offset low - (return-instruction---size-hi) ;; size high - (return-instruction---size-lo) ;; size low - ))) + (if-not-zero (shift misc/MXP_FLAG ROFF_RETURN___1ST_MISC_ROW) + (set-MXP-instruction---single-mxp-offset-instructions ROFF_RETURN___1ST_MISC_ROW ;; row offset kappa + (return-instruction---instruction) ;; instruction + (return-instruction---is-deployment) ;; bit modifying the behaviour of RETURN pricing + (return-instruction---offset-hi) ;; offset high + (return-instruction---offset-lo) ;; offset low + (return-instruction---size-hi) ;; size high + (return-instruction---size-lo) ;; size low + ))) (defconstraint return-instruction---setting-OOB-data (:guard (return-instruction---standard-scenario-row)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/hub/constraints/instruction-handling/halting/revert.lisp b/hub/constraints/instruction-handling/halting/revert.lisp index bca419954..bfc3289f8 100644 --- a/hub/constraints/instruction-handling/halting/revert.lisp +++ b/hub/constraints/instruction-handling/halting/revert.lisp @@ -54,19 +54,23 @@ (halting-instruction---is-REVERT) (- 1 stack/SUX stack/SOX ))) -(defconstraint revert-instruction---setting-the-stack-pattern (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-stack-pattern + (:guard (revert-instruction---standard-precondition)) (stack-pattern-2-0)) -(defconstraint revert-instruction---allowable-exceptions (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---allowable-exceptions + (:guard (revert-instruction---standard-precondition)) (eq! XAHOY (+ stack/MXPX stack/OOGX))) -(defconstraint revert-instruction---setting-NSR (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-NSR + (:guard (revert-instruction---standard-precondition)) (eq! NSR (- 3 XAHOY))) -(defconstraint revert-instruction---setting-the-peeking-flags (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-peeking-flags + (:guard (revert-instruction---standard-precondition)) (if-not-zero XAHOY ;; XAHOY ≡ 1 (eq! NSR @@ -78,11 +82,13 @@ (shift PEEK_AT_CONTEXT ROFF_REVERT___NO_XAHOY_CURRENT_CONTEXT_ROW) (shift PEEK_AT_CONTEXT ROFF_REVERT___NO_XAHOY_CALLER_CONTEXT_ROW ))))) -(defconstraint revert-instruction---setting-the-context-rows---exceptional (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-context-rows---exceptional + (:guard (revert-instruction---standard-precondition)) (if-not-zero XAHOY (execution-provides-empty-return-data ROFF_REVERT___XAHOY_CALLER_CONTEXT_ROW))) -(defconstraint revert-instruction---setting-the-context-rows---unexceptional (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-context-rows---unexceptional + (:guard (revert-instruction---standard-precondition)) (if-zero XAHOY (provide-return-data ROFF_REVERT___NO_XAHOY_CALLER_CONTEXT_ROW ;; row offset (revert-instruction---caller-context) ;; receiver context @@ -91,7 +97,8 @@ (revert-instruction---type-safe-return-data-size) ;; type safe rds ))) -(defconstraint revert-instruction---setting-the-miscellaneous-row-module-flags (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-miscellaneous-row-module-flags + (:guard (revert-instruction---standard-precondition)) (let ((FLAG (weighted-MISC-flag-sum ROFF_REVERT___MISC_ROW))) ;; (if (or! @@ -104,19 +111,22 @@ ;; trigger_MMU == 1 (eq! FLAG (+ MISC_WEIGHT_MXP MISC_WEIGHT_MMU))))) -(defconstraint revert-instruction---setting-the-MXP-data (:guard (revert-instruction---standard-precondition)) - (set-MXP-instruction-type-4 ROFF_REVERT___MISC_ROW ;; row offset kappa - (revert-instruction---instruction) ;; instruction - 0 ;; bit modifying the behaviour of RETURN pricing - (revert-instruction---offset-hi) ;; offset high - (revert-instruction---offset-lo) ;; offset low - (revert-instruction---size-hi) ;; size high - (revert-instruction---size-lo))) ;; size low - -(defconstraint revert-instruction---setting-the-MXPX (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-MXP-instruction + (:guard (revert-instruction---standard-precondition)) + (set-MXP-instruction---single-mxp-offset-instructions ROFF_REVERT___MISC_ROW ;; row offset kappa + (revert-instruction---instruction) ;; instruction + 0 ;; bit modifying the behaviour of RETURN pricing + (revert-instruction---offset-hi) ;; offset high + (revert-instruction---offset-lo) ;; offset low + (revert-instruction---size-hi) ;; size high + (revert-instruction---size-lo))) ;; size low + +(defconstraint revert-instruction---setting-the-MXPX + (:guard (revert-instruction---standard-precondition)) (eq! stack/MXPX (shift misc/MXP_MXPX ROFF_REVERT___MISC_ROW))) -(defconstraint revert-instruction---setting-the-MMU-data (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-MMU-data + (:guard (revert-instruction---standard-precondition)) (if-not-zero (shift misc/MMU_FLAG ROFF_REVERT___MISC_ROW) (set-MMU-instruction---ram-to-ram-sans-padding ROFF_REVERT___MISC_ROW ;; row offset (revert-instruction---current-context) ;; source ID @@ -135,7 +145,8 @@ ;; phase ;; phase ))) -(defconstraint revert-instruction---setting-the-gas-cost (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-gas-cost + (:guard (revert-instruction---standard-precondition)) (if-not-zero stack/MXPX (vanishes! GAS_COST) (eq! GAS_COST diff --git a/hub/constraints/instruction-handling/keccak.lisp b/hub/constraints/instruction-handling/keccak.lisp index 04bc1d1c4..82ec196ff 100644 --- a/hub/constraints/instruction-handling/keccak.lisp +++ b/hub/constraints/instruction-handling/keccak.lisp @@ -26,10 +26,10 @@ (defun (keccak-instruction---size-lo) [ stack/STACK_ITEM_VALUE_LO 2 ]) (defun (keccak-instruction---result-hi) [ stack/STACK_ITEM_VALUE_HI 4 ]) (defun (keccak-instruction---result-lo) [ stack/STACK_ITEM_VALUE_LO 4 ]) ;; "" -(defun (keccak-instruction---mxpx) (shift misc/MXP_MXPX ROFF___KEC___MISCELLANEOUS_ROW)) -(defun (keccak-instruction---mxp-gas) (shift misc/MXP_GAS_MXP ROFF___KEC___MISCELLANEOUS_ROW)) -(defun (keccak-instruction---mxp-MTNTOP) (shift misc/MXP_MTNTOP ROFF___KEC___MISCELLANEOUS_ROW)) -(defun (keccak-instruction---trigger_MMU) (* (- 1 XAHOY) (keccak-instruction---mxp-MTNTOP))) +(defun (keccak-instruction---MXP-mxpx) (shift misc/MXP_MXPX ROFF___KEC___MISCELLANEOUS_ROW)) +(defun (keccak-instruction---MXP-gas-mxp) (shift misc/MXP_GAS_MXP ROFF___KEC___MISCELLANEOUS_ROW)) +(defun (keccak-instruction---MXP-s1nznomxpx) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF___KEC___MISCELLANEOUS_ROW)) +(defun (keccak-instruction---trigger_MMU) (* (- 1 XAHOY) (keccak-instruction---MXP-s1nznomxpx))) (defun (keccak-instruction---no-stack-exceptions) (* PEEK_AT_STACK stack/KEC_FLAG (- 1 stack/SUX stack/SOX))) (defconstraint keccak-instruction---setting-stack-pattern (:guard (keccak-instruction---no-stack-exceptions)) @@ -52,14 +52,14 @@ (* MISC_WEIGHT_MMU (keccak-instruction---trigger_MMU))))) (defconstraint keccak-instruction---setting-MXP-parameters (:guard (keccak-instruction---no-stack-exceptions)) - (set-MXP-instruction-type-4 1 ;; row offset kappa - EVM_INST_SHA3 ;; instruction - 0 ;; deploys (bit modifying the behaviour of RETURN pricing) - (keccak-instruction---offset-hi) ;; source offset high - (keccak-instruction---offset-lo) ;; source offset low - (keccak-instruction---size-hi) ;; source size high - (keccak-instruction---size-lo) ;; source size low - )) + (set-MXP-instruction---single-mxp-offset-instructions 1 ;; row offset kappa + EVM_INST_SHA3 ;; instruction + 0 ;; deploys (bit modifying the behaviour of RETURN pricing) + (keccak-instruction---offset-hi) ;; source offset high + (keccak-instruction---offset-lo) ;; source offset low + (keccak-instruction---size-hi) ;; source size high + (keccak-instruction---size-lo) ;; source size low + )) (defconstraint keccak-instruction---setting-MMU-parameters (:guard (keccak-instruction---no-stack-exceptions)) (if-not-zero misc/MMU_FLAG @@ -82,13 +82,13 @@ (defconstraint keccak-instruction---transferring-MXPX-to-stack (:guard (keccak-instruction---no-stack-exceptions)) - (eq! stack/MXPX (keccak-instruction---mxpx))) + (eq! stack/MXPX (keccak-instruction---MXP-mxpx))) (defconstraint keccak-instruction---setting-gas-cost (:guard (keccak-instruction---no-stack-exceptions)) - ;; (if-zero (force-bin (keccak-instruction---mxpx)) - (if-zero (keccak-instruction---mxpx) - (eq! GAS_COST (+ stack/STATIC_GAS (keccak-instruction---mxp-gas))) + ;; (if-zero (force-bin (keccak-instruction---MXP-mxpx)) + (if-zero (keccak-instruction---MXP-mxpx) + (eq! GAS_COST (+ stack/STATIC_GAS (keccak-instruction---MXP-gas-mxp))) (vanishes! GAS_COST))) (defconstraint keccak-instruction---setting-setting-HASH_INFO_FLAG diff --git a/hub/constraints/instruction-handling/log.lisp b/hub/constraints/instruction-handling/log.lisp index c81323006..1012af94c 100644 --- a/hub/constraints/instruction-handling/log.lisp +++ b/hub/constraints/instruction-handling/log.lisp @@ -101,16 +101,16 @@ (defconstraint log-instruction---MISC-row-setting-MXP-data (:guard (log-instruction---standard-hypothesis)) (if-zero stack/STATICX - (set-MXP-instruction-type-4 ROFF_LOG___MISCELLANEOUS_ROW ;; row offset kappa - (log-instruction---instruction) ;; instruction - 0 ;; bit modifying the behaviour of RETURN pricing - (log-instruction---offset-hi) ;; offset high - (log-instruction---offset-lo) ;; offset low - (log-instruction---size-hi) ;; size high - (log-instruction---size-lo)))) ;; size low + (set-MXP-instruction---single-mxp-offset-instructions ROFF_LOG___MISCELLANEOUS_ROW ;; row offset kappa + (log-instruction---instruction) ;; instruction + 0 ;; bit modifying the behaviour of RETURN pricing + (log-instruction---offset-hi) ;; offset high + (log-instruction---offset-lo) ;; offset low + (log-instruction---size-hi) ;; size high + (log-instruction---size-lo)))) ;; size low (defun (trigger_MMU) (* (- 1 CONTEXT_WILL_REVERT) - (shift misc/MXP_MTNTOP ROFF_LOG___MISCELLANEOUS_ROW))) + (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX ROFF_LOG___MISCELLANEOUS_ROW))) (defconstraint log-instruction---MISC-row-setting-MMU-data (:guard (log-instruction---standard-hypothesis)) (if-zero (force-bin stack/STATICX) diff --git a/hub/constraints/instruction-handling/machine_state.lisp b/hub/constraints/instruction-handling/machine_state.lisp index f68c8071b..aa03d3bc9 100644 --- a/hub/constraints/instruction-handling/machine_state.lisp +++ b/hub/constraints/instruction-handling/machine_state.lisp @@ -62,8 +62,8 @@ (defconstraint machine-state-instruction---setting-miscellaneous-row (:guard (machine-state-instruction---no-stack-exception)) (if-not-zero (machine-state-instruction---is-MSIZE) (begin - (eq! (weighted-MISC-flag-sum ROFF_MACHINESTATE___MSIZE___MISC_ROW) MISC_WEIGHT_MXP) - (set-MXP-instruction-type-1 ROFF_MACHINESTATE___MSIZE___MISC_ROW)))) + (eq! (weighted-MISC-flag-sum ROFF_MACHINESTATE___MSIZE___MISC_ROW) MISC_WEIGHT_MXP) + (set-MXP-instruction---for-MSIZE ROFF_MACHINESTATE___MSIZE___MISC_ROW)))) (defconstraint machine-state-instruction---setting-gas-cost (:guard (machine-state-instruction---no-stack-exception)) diff --git a/hub/constraints/instruction-handling/mcopy/constraints.lisp b/hub/constraints/instruction-handling/mcopy/constraints.lisp new file mode 100644 index 000000000..da985ee59 --- /dev/null +++ b/hub/constraints/instruction-handling/mcopy/constraints.lisp @@ -0,0 +1,143 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.5 Instruction handling ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z MCOPY instruction ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint mcopy-instruction---setting-the-stack-pattern + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (stack-pattern-3-0)) + +(defconstraint mcopy-instruction---the-first-row-must-be-misc-and-we-call-MXP + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (begin + (eq! (shift PEEK_AT_MISCELLANEOUS MCOPY_ROFF___1ST_MISC_ROW) 1) + (eq! (shift misc/MXP_FLAG MCOPY_ROFF___1ST_MISC_ROW) 1) + )) + +(defconstraint mcopy-instruction---defining-the-MXP-instruction + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (set-MXP-instruction---for-MCOPY MCOPY_ROFF___1ST_MISC_ROW ;; row offset kappa + (mcopy-instruction---target-offset-hi) ;; target offset hi + (mcopy-instruction---target-offset-lo) ;; target offset lo + (mcopy-instruction---source-offset-hi) ;; source offset hi + (mcopy-instruction---source-offset-lo) ;; source offset lo + (mcopy-instruction---size-hi) ;; size hi + (mcopy-instruction---size-lo) ;; size lo + )) + +(defun (mcopy-instruction---trigger_MXP) 1) +(defun (mcopy-instruction---trigger_MMU) (* (- 1 XAHOY) + (mcopy-instruction---MXP-s1nznomxpx))) ;; "" + +(defconstraint mcopy-instruction---setting-NSR + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero XAHOY + ;; XAHOY ≡ true + (eq! NSR 2) + ;; XAHOY ≡ false + (eq! NSR (+ 1 (mcopy-instruction---trigger_MMU)))) + ) + +(defconstraint mcopy-instruction---setting-the-peeking-flags + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero XAHOY + ;; XAHOY ≡ true + (eq! NSR + (+ (shift PEEK_AT_MISCELLANEOUS MCOPY_ROFF___1ST_MISC_ROW ) + (shift PEEK_AT_CONTEXT MCOPY_ROFF___XCON_ROW ))) + ;; XAHOY ≡ false + (eq! NSR + (+ (shift PEEK_AT_MISCELLANEOUS MCOPY_ROFF___1ST_MISC_ROW ) + (* (mcopy-instruction---trigger_MMU) (shift PEEK_AT_MISCELLANEOUS MCOPY_ROFF___2ND_MISC_ROW )))) + )) + +(defconstraint mcopy-instruction---justifying-the-stacks-MXPX-flag + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! stack/MXPX + (mcopy-instruction---MXP-mxpx) + )) + +(defconstraint mcopy-instruction---setting-the-gas-cost + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-zero stack/MXPX + ;; MXPX ≡ false + (eq! GAS_COST (+ stack/STATIC_GAS (mcopy-instruction---MXP-gas-mxp))) + ;; MXPX ≡ true + (eq! GAS_COST 0 ) + )) + +(defconstraint mcopy-instruction---1st-MISC-row---setting-the-flags + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (eq! (weighted-MISC-flag-sum MCOPY_ROFF___1ST_MISC_ROW) + (+ (* MISC_WEIGHT_MXP (mcopy-instruction---trigger_MXP)) + (* MISC_WEIGHT_MMU (mcopy-instruction---trigger_MMU)) + ))) + +(defconstraint mcopy-instruction---2nd-MISC-row---setting-the-flags + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (mcopy-instruction---trigger_MMU) + (eq! (weighted-MISC-flag-sum MCOPY_ROFF___2ND_MISC_ROW) + MISC_WEIGHT_MMU))) + +(defconstraint mcopy-instruction---1st-MISC-row---setting-the-MMU-call + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (mcopy-instruction---trigger_MMU) + (set-MMU-instruction---ram-to-ram-sans-padding MCOPY_ROFF___1ST_MISC_ROW ;; offset + CONTEXT_NUMBER ;; source ID + (+ 1 HUB_STAMP) ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + (mcopy-instruction---source-offset-lo) ;; source offset low + ;; tgt_offset_lo ;; target offset low + (mcopy-instruction---size-lo) ;; size + 0 ;; reference offset + (mcopy-instruction---size-lo) ;; reference size + ;; success_bit ;; success bit + ;; limb_1 ;; limb 1 + ;; limb_2 ;; limb 2 + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) + +(defconstraint mcopy-instruction---2nd-MISC-row---setting-the-MMU-call + (:guard (mcopy-instruction---standard-precondition)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-not-zero (mcopy-instruction---trigger_MMU) + (set-MMU-instruction---ram-to-ram-sans-padding MCOPY_ROFF___2ND_MISC_ROW ;; offset + (+ 1 HUB_STAMP) ;; source ID + CONTEXT_NUMBER ;; target ID + ;; aux_id ;; auxiliary ID + ;; src_offset_hi ;; source offset high + 0 ;; source offset low + ;; tgt_offset_lo ;; target offset low + (mcopy-instruction---size-lo) ;; size + (mcopy-instruction---target-offset-lo) ;; reference offset + (mcopy-instruction---size-lo) ;; reference size + ;; success_bit ;; success bit + ;; limb_1 ;; limb 1 + ;; limb_2 ;; limb 2 + ;; exo_sum ;; weighted exogenous module flag sum + ;; phase ;; phase + ))) diff --git a/hub/constraints/instruction-handling/mcopy/shorthands.lisp b/hub/constraints/instruction-handling/mcopy/shorthands.lisp new file mode 100644 index 000000000..1ef5e00e9 --- /dev/null +++ b/hub/constraints/instruction-handling/mcopy/shorthands.lisp @@ -0,0 +1,38 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X.5 Instruction handling ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y.Z MCOPY instruction ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (mcopy-instruction---target-offset-hi) [ stack/STACK_ITEM_VALUE_HI 1 ] ) +(defun (mcopy-instruction---target-offset-lo) [ stack/STACK_ITEM_VALUE_HI 1 ] ) +(defun (mcopy-instruction---source-offset-hi) [ stack/STACK_ITEM_VALUE_HI 2 ] ) +(defun (mcopy-instruction---source-offset-lo) [ stack/STACK_ITEM_VALUE_HI 2 ] ) +(defun (mcopy-instruction---size-hi) [ stack/STACK_ITEM_VALUE_HI 3 ] ) +(defun (mcopy-instruction---size-lo) [ stack/STACK_ITEM_VALUE_HI 3 ] ) ;; "" + +(defun (mcopy-instruction---MXP-mxpx) (shift misc/MXP_MXPX MCOPY_ROFF___1ST_MISC_ROW )) +(defun (mcopy-instruction---MXP-gas-mxp) (shift misc/MXP_GAS_MXP MCOPY_ROFF___1ST_MISC_ROW )) +(defun (mcopy-instruction---MXP-s1nznomxpx) (shift misc/MXP_SIZE_1_NONZERO_NO_MXPX MCOPY_ROFF___1ST_MISC_ROW )) + +(defun (mcopy-instruction---standard-precondition) (* PEEK_AT_STACK + stack/MCOPY_FLAG + (- 1 + stack/SUX + stack/SOX))) + +(defconst + MCOPY_ROFF___1ST_MISC_ROW 1 + MCOPY_ROFF___2ND_MISC_ROW 2 + MCOPY_ROFF___XCON_ROW 2 + ) diff --git a/hub/constraints/instruction-handling/stack_ram.lisp b/hub/constraints/instruction-handling/stack_ram.lisp index a47037fbc..f9e333c94 100644 --- a/hub/constraints/instruction-handling/stack_ram.lisp +++ b/hub/constraints/instruction-handling/stack_ram.lisp @@ -42,6 +42,10 @@ (defun (stack-ram---call-data-size) (shift context/CALL_DATA_SIZE ROFF_STACK_RAM___CONTEXT_ROW)) (defun (stack-ram---call-data-offset) (shift context/CALL_DATA_OFFSET ROFF_STACK_RAM___CONTEXT_ROW)) (defun (stack-ram---call-data-context-number) (shift context/CALL_DATA_CONTEXT_NUMBER ROFF_STACK_RAM___CONTEXT_ROW)) +(defun (stack-ram---fixed-size) (+ (* WORD_SIZE (stack-ram---is-MLOAD) ) + (* WORD_SIZE (stack-ram---is-MSTORE) ) + (* 1 (stack-ram---is-MSTORE8) ))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -134,25 +138,17 @@ (vanishes! (stack-ram---value-hi)) (vanishes! (stack-ram---value-lo)))))) -(defconstraint stack-ram---setting-MXP-instruction---MLOAD-MSTORE-case - (:guard (stack-ram---std-hyp)) - (if-not-zero (stack-ram---misc-MXP-flag) - (if-not-zero (+ (stack-ram---is-MLOAD) (stack-ram---is-MSTORE)) - (set-MXP-instruction-type-2 ROFF_STACK_RAM___MISC_ROW ;; row offset - (stack-ram---instruction) ;; instruction - (stack-ram---offset-hi) ;; source offset high - (stack-ram---offset-lo) ;; source offset low - )))) - -(defconstraint stack-ram---setting-MXP-instruction---MSTORE8-case +(defconstraint stack-ram---setting-MXP-instruction (:guard (stack-ram---std-hyp)) (if-not-zero (stack-ram---misc-MXP-flag) - (if-not-zero (stack-ram---is-MSTORE8) - (set-MXP-instruction-type-3 ROFF_STACK_RAM___MISC_ROW ;; row offset - (stack-ram---offset-hi) ;; source offset high - (stack-ram---offset-lo) ;; source offset low - )))) - + (set-MXP-instruction---single-mxp-offset-instructions ROFF_STACK_RAM___MISC_ROW ;; row offset + (stack-ram---instruction) ;; instruction + 0 ;; deploys + (stack-ram---offset-hi) ;; source offset high + (stack-ram---offset-lo) ;; source offset low + 0 ;; size high + (stack-ram---fixed-size) ;; size low + ))) (defconstraint stack-ram---setting-MMU-instruction---CALLDATALOAD-case (:guard (stack-ram---std-hyp)) diff --git a/hub/constraints/miscellaneous-rows/mxp.lisp b/hub/constraints/miscellaneous-rows/mxp.lisp deleted file mode 100644 index a43633a38..000000000 --- a/hub/constraints/miscellaneous-rows/mxp.lisp +++ /dev/null @@ -1,63 +0,0 @@ -(module hub) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 9.2 MISC/MXP constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (set-MXP-instruction-type-1 kappa) - (eq! (shift misc/MXP_INST kappa) EVM_INST_MSIZE)) - -(defun (set-MXP-instruction-type-2 kappa ;; row offset kappa - instruction ;; instruction - offset_hi ;; source offset high - offset_lo ;; source offset low - ) - (begin (eq! (shift misc/MXP_INST kappa) instruction) - (eq! (shift misc/MXP_OFFSET_1_HI kappa) offset_hi) - (eq! (shift misc/MXP_OFFSET_1_LO kappa) offset_lo))) - -(defun (set-MXP-instruction-type-3 kappa ;; row offset kappa - offset_hi ;; source offset high - offset_lo ;; source offset low - ) - (begin (eq! (shift misc/MXP_INST kappa) EVM_INST_MSTORE8) - (eq! (shift misc/MXP_OFFSET_1_HI kappa) offset_hi) - (eq! (shift misc/MXP_OFFSET_1_LO kappa) offset_lo))) - -(defun (set-MXP-instruction-type-4 kappa ;; row offset kappa - instruction ;; instruction - deploys ;; bit modifying the behaviour of RETURN pricing - offset_hi ;; offset high - offset_lo ;; offset low - size_hi ;; size high - size_lo ;; size low - ) - (begin (eq! (shift misc/MXP_INST kappa) instruction) - (eq! (shift misc/MXP_DEPLOYS kappa) deploys) - (eq! (shift misc/MXP_OFFSET_1_HI kappa) offset_hi) - (eq! (shift misc/MXP_OFFSET_1_LO kappa) offset_lo) - (eq! (shift misc/MXP_SIZE_1_HI kappa) size_hi) - (eq! (shift misc/MXP_SIZE_1_LO kappa) size_lo))) - -(defun (set-MXP-instruction-type-5 kappa ;; row offset kappa - instruction ;; instruction - cdo_hi ;; call data offset high - cdo_lo ;; call data offset low - cds_hi ;; call data size high - cds_lo ;; call data size low - r@o_hi ;; return at offset high - r@o_lo ;; return at offset low - r@c_hi ;; return at capacity high - r@c_lo ;; return at capacity low - ) - (begin (eq! (shift misc/MXP_INST kappa) instruction) - (eq! (shift misc/MXP_OFFSET_1_HI kappa) cdo_hi) - (eq! (shift misc/MXP_OFFSET_1_LO kappa) cdo_lo) - (eq! (shift misc/MXP_SIZE_1_HI kappa) cds_hi) - (eq! (shift misc/MXP_SIZE_1_LO kappa) cds_lo) - (eq! (shift misc/MXP_OFFSET_2_HI kappa) r@o_hi) - (eq! (shift misc/MXP_OFFSET_2_LO kappa) r@o_lo) - (eq! (shift misc/MXP_SIZE_2_HI kappa) r@c_hi) - (eq! (shift misc/MXP_SIZE_2_LO kappa) r@c_lo))) - diff --git a/hub/constraints/miscellaneous-rows/mxp/calls.lisp b/hub/constraints/miscellaneous-rows/mxp/calls.lisp new file mode 100644 index 000000000..e5e993172 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/mxp/calls.lisp @@ -0,0 +1,31 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y MISC/MXP CALL-type instructions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (set-MXP-instruction---for-CALL-type kappa ;; row offset kappa + instruction ;; instruction + cdo_hi ;; call data offset high + cdo_lo ;; call data offset low + cds_hi ;; call data size high + cds_lo ;; call data size low + r@o_hi ;; return at offset high + r@o_lo ;; return at offset low + r@c_hi ;; return at capacity high + r@c_lo ;; return at capacity low + ) + (begin + (eq! (shift misc/MXP_INST kappa) instruction ) + (eq! (shift misc/MXP_OFFSET_1_HI kappa) cdo_hi ) + (eq! (shift misc/MXP_OFFSET_1_LO kappa) cdo_lo ) + (eq! (shift misc/MXP_SIZE_1_HI kappa) cds_hi ) + (eq! (shift misc/MXP_SIZE_1_LO kappa) cds_lo ) + (eq! (shift misc/MXP_OFFSET_2_HI kappa) r@o_hi ) + (eq! (shift misc/MXP_OFFSET_2_LO kappa) r@o_lo ) + (eq! (shift misc/MXP_SIZE_2_HI kappa) r@c_hi ) + (eq! (shift misc/MXP_SIZE_2_LO kappa) r@c_lo ) + )) diff --git a/hub/constraints/miscellaneous-rows/mxp/mcopy.lisp b/hub/constraints/miscellaneous-rows/mxp/mcopy.lisp new file mode 100644 index 000000000..4383b0cd8 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/mxp/mcopy.lisp @@ -0,0 +1,27 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y MISC/MXP constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (set-MXP-instruction---for-MCOPY kappa ;; row offset kappa + target_offset_hi ;; target offset hi + target_offset_lo ;; target offset lo + source_offset_hi ;; source offset hi + source_offset_lo ;; source offset lo + size_hi ;; size hi + size_lo ;; size lo + ) + (begin + (eq! (shift misc/MXP_INST kappa) EVM_INST_MCOPY ) + (eq! (shift misc/MXP_OFFSET_1_HI kappa) target_offset_hi ) + (eq! (shift misc/MXP_OFFSET_1_LO kappa) target_offset_lo ) + (eq! (shift misc/MXP_SIZE_1_HI kappa) size_hi ) + (eq! (shift misc/MXP_SIZE_1_LO kappa) size_lo ) + (eq! (shift misc/MXP_OFFSET_2_HI kappa) source_offset_hi ) + (eq! (shift misc/MXP_OFFSET_2_LO kappa) source_offset_lo ) + (eq! (shift misc/MXP_SIZE_2_HI kappa) size_hi ) + (eq! (shift misc/MXP_SIZE_2_LO kappa) size_lo ))) + diff --git a/hub/constraints/miscellaneous-rows/mxp/msize.lisp b/hub/constraints/miscellaneous-rows/mxp/msize.lisp new file mode 100644 index 000000000..ee80e4908 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/mxp/msize.lisp @@ -0,0 +1,11 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 9.2 MISC/MXP instruction for MSIZE ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (set-MXP-instruction---for-MSIZE kappa) + (eq! + (shift misc/MXP_INST kappa) EVM_INST_MSIZE)) diff --git a/hub/constraints/miscellaneous-rows/mxp/single_offset.lisp b/hub/constraints/miscellaneous-rows/mxp/single_offset.lisp new file mode 100644 index 000000000..04e226b72 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/mxp/single_offset.lisp @@ -0,0 +1,25 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.Y MISC/MXP CALL-type instructions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (set-MXP-instruction---single-mxp-offset-instructions kappa ;; row offset kappa + instruction ;; instruction + deploys ;; bit modifying the behaviour of RETURN pricing + offset_hi ;; offset high + offset_lo ;; offset low + size_hi ;; size high + size_lo ;; size low + ) + (begin + (eq! (shift misc/MXP_INST kappa) instruction ) + (eq! (shift misc/MXP_DEPLOYS kappa) deploys ) + (eq! (shift misc/MXP_OFFSET_1_HI kappa) offset_hi ) + (eq! (shift misc/MXP_OFFSET_1_LO kappa) offset_lo ) + (eq! (shift misc/MXP_SIZE_1_HI kappa) size_hi ) + (eq! (shift misc/MXP_SIZE_1_LO kappa) size_lo ) + )) diff --git a/hub/constraints/stack-patterns/0-0-stack-pattern.lisp b/hub/constraints/stack-patterns/0-0-stack-pattern.lisp new file mode 100644 index 000000000..6e1302c8a --- /dev/null +++ b/hub/constraints/stack-patterns/0-0-stack-pattern.lisp @@ -0,0 +1,22 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.5 (0,0)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-0-0) + (begin + (empty-stack-pattern) + (debug (eq! HEIGHT_NEW HEIGHT)))) + diff --git a/hub/constraints/stack-patterns/0-1-stack-pattern.lisp b/hub/constraints/stack-patterns/0-1-stack-pattern.lisp new file mode 100644 index 000000000..b81ca7f34 --- /dev/null +++ b/hub/constraints/stack-patterns/0-1-stack-pattern.lisp @@ -0,0 +1,32 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.8 (0,1)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-0-1) + (begin + ;; stack item 1: + (empty-stack-item 1) + ;; stack item 2: + (empty-stack-item 2) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (inc-frst-row-stack-item-X-height-by-Y 4 1) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 0) + ;; height update; + (debug (eq! HEIGHT_NEW (+ HEIGHT 1))))) + diff --git a/hub/constraints/stack-patterns/1-0-stack-pattern.lisp b/hub/constraints/stack-patterns/1-0-stack-pattern.lisp new file mode 100644 index 000000000..496b31b37 --- /dev/null +++ b/hub/constraints/stack-patterns/1-0-stack-pattern.lisp @@ -0,0 +1,32 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.6 (1,0)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-1-0) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (empty-stack-item 2) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (empty-stack-item 4) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 1))))) + diff --git a/hub/constraints/stack-patterns/1-1-stack-pattern.lisp b/hub/constraints/stack-patterns/1-1-stack-pattern.lisp new file mode 100644 index 000000000..38b9b87e6 --- /dev/null +++ b/hub/constraints/stack-patterns/1-1-stack-pattern.lisp @@ -0,0 +1,34 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.9 (1,1)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-1-1) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (empty-stack-item 2) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (inc-frst-row-stack-item-X-height-by-Y 4 0) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 1) + ;; height update; + (debug (eq! HEIGHT_NEW HEIGHT)))) + diff --git a/hub/constraints/stack-patterns/2-0-stack-pattern.lisp b/hub/constraints/stack-patterns/2-0-stack-pattern.lisp new file mode 100644 index 000000000..0d6aab471 --- /dev/null +++ b/hub/constraints/stack-patterns/2-0-stack-pattern.lisp @@ -0,0 +1,34 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.7 (2,0)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-2-0) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 1) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (empty-stack-item 4) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 2))))) + diff --git a/hub/constraints/stack-patterns/2-1-stack-pattern.lisp b/hub/constraints/stack-patterns/2-1-stack-pattern.lisp new file mode 100644 index 000000000..1b18155fb --- /dev/null +++ b/hub/constraints/stack-patterns/2-1-stack-pattern.lisp @@ -0,0 +1,36 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.10 (2,1)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-2-1) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 1) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (dec-frst-row-stack-item-X-height-by-Y 4 1) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 2) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 1))))) + diff --git a/hub/constraints/stack-patterns/3-0-stack-pattern.lisp b/hub/constraints/stack-patterns/3-0-stack-pattern.lisp new file mode 100644 index 000000000..d4b9a2ab2 --- /dev/null +++ b/hub/constraints/stack-patterns/3-0-stack-pattern.lisp @@ -0,0 +1,35 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.X (3,0)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-3-0) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 1) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (dec-frst-row-stack-item-X-height-by-Y 3 2) + (pop-frst-row-stack-item 3) + (set-frst-row-stack-item-stamp 3 2) + ;; stack item 4: + (empty-stack-item 4) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 2))))) diff --git a/hub/constraints/stack-patterns/3-1-stack-pattern.lisp b/hub/constraints/stack-patterns/3-1-stack-pattern.lisp new file mode 100644 index 000000000..9edacff6d --- /dev/null +++ b/hub/constraints/stack-patterns/3-1-stack-pattern.lisp @@ -0,0 +1,38 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.11 (3,1)-StackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (stack-pattern-3-1) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 1) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (dec-frst-row-stack-item-X-height-by-Y 3 2) + (pop-frst-row-stack-item 3) + (set-frst-row-stack-item-stamp 3 2) + ;; stack item 4: + (dec-frst-row-stack-item-X-height-by-Y 4 2) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 3) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 2))))) + diff --git a/hub/constraints/stack-patterns/_helpers.lisp b/hub/constraints/stack-patterns/_helpers.lisp new file mode 100644 index 000000000..d6f7d24d6 --- /dev/null +++ b/hub/constraints/stack-patterns/_helpers.lisp @@ -0,0 +1,39 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.3 emptyStackItem_k ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (empty-stack-item k) + (begin + (vanishes! [ stack/STACK_ITEM_HEIGHT k ]) + (vanishes! [ stack/STACK_ITEM_POP k ]) + (debug (vanishes! [ stack/STACK_ITEM_VALUE_HI k ])) + (debug (vanishes! [ stack/STACK_ITEM_VALUE_LO k ])) + (vanishes! [ stack/STACK_ITEM_STAMP k ]) + )) + +;; current row +(defun (set-frst-row-stack-item-stamp k offset ) (eq! [ stack/STACK_ITEM_STAMP k ] (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) offset) )) +(defun (pop-frst-row-stack-item k ) (eq! [ stack/STACK_ITEM_POP k ] 1 )) +(defun (push-frst-row-stack-item k ) (eq! [ stack/STACK_ITEM_POP k ] 0 )) +(defun (inc-frst-row-stack-item-X-height-by-Y k increment) (eq! [ stack/STACK_ITEM_HEIGHT k ] (+ HEIGHT increment) )) +(defun (dec-frst-row-stack-item-X-height-by-Y k decrement) (eq! [ stack/STACK_ITEM_HEIGHT k ] (- HEIGHT decrement) )) ;; "" + +;; next row +(defun (set-scnd-row-stack-item-stamp k offset ) (eq! (next [ stack/STACK_ITEM_STAMP k ]) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) offset) )) +(defun (pop-scnd-row-stack-item k ) (eq! (next [ stack/STACK_ITEM_POP k ]) 1 )) +(defun (push-scnd-row-stack-item k ) (eq! (next [ stack/STACK_ITEM_POP k ]) 0 )) +(defun (inc-scnd-row-stack-item-X-height-by-Y k increment) (eq! (next [ stack/STACK_ITEM_HEIGHT k ]) (+ HEIGHT increment) )) +(defun (dec-scnd-row-stack-item-X-height-by-Y k decrement) (eq! (next [ stack/STACK_ITEM_HEIGHT k ]) (- HEIGHT decrement) )) ;; "" + diff --git a/hub/constraints/stack_patterns.lisp b/hub/constraints/stack-patterns/_stack_patterns.lispX similarity index 100% rename from hub/constraints/stack_patterns.lisp rename to hub/constraints/stack-patterns/_stack_patterns.lispX diff --git a/hub/constraints/stack-patterns/call-stack-pattern.lisp b/hub/constraints/stack-patterns/call-stack-pattern.lisp new file mode 100644 index 000000000..942468d4f --- /dev/null +++ b/hub/constraints/stack-patterns/call-stack-pattern.lisp @@ -0,0 +1,57 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.17 callStackPattern[b] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (call-stack-pattern (b :binary)) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 (+ 2 b)) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 3) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 (+ 3 b)) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 4) + ;; stack item 3: + (dec-frst-row-stack-item-X-height-by-Y 3 (+ 4 b)) + (pop-frst-row-stack-item 3) + (set-frst-row-stack-item-stamp 3 5) + ;; stack item 4: + (dec-frst-row-stack-item-X-height-by-Y 4 (+ 5 b)) + (pop-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 6) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 5 b))) + ;; stack item 5; + (dec-scnd-row-stack-item-X-height-by-Y 1 0) + (pop-scnd-row-stack-item 1) + (set-scnd-row-stack-item-stamp 1 0) + ;; stack item 6; + (dec-scnd-row-stack-item-X-height-by-Y 2 1) + (pop-scnd-row-stack-item 2) + (set-scnd-row-stack-item-stamp 2 1) + ;; stack item 7; + (will-eq! [ stack/STACK_ITEM_HEIGHT 3 ] (* b (- HEIGHT 2))) + (will-eq! [ stack/STACK_ITEM_POP 3 ] b ) + (will-eq! [ stack/STACK_ITEM_STAMP 3 ] (* b (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 2))) + ;; stack item 8; + (dec-scnd-row-stack-item-X-height-by-Y 4 (+ 5 b)) + (push-scnd-row-stack-item 4) + (set-scnd-row-stack-item-stamp 4 7) + (vanishes! (next [ stack/STACK_ITEM_VALUE_HI 4 ])) + (is-binary (next [ stack/STACK_ITEM_VALUE_LO 4 ])) + ) + ) diff --git a/hub/constraints/stack-patterns/copy-stack-pattern.lisp b/hub/constraints/stack-patterns/copy-stack-pattern.lisp new file mode 100644 index 000000000..2611b9812 --- /dev/null +++ b/hub/constraints/stack-patterns/copy-stack-pattern.lisp @@ -0,0 +1,39 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.16 copyStackPattern[b] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (copy-stack-pattern (b :binary)) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 b) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 1) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 (+ 2 b)) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 2) + ;; stack item 3: + (dec-frst-row-stack-item-X-height-by-Y 3 (+ 1 b)) + (pop-frst-row-stack-item 3) + (set-frst-row-stack-item-stamp 3 3) + ;; stack item 4: + (eq! [ stack/STACK_ITEM_HEIGHT 4 ] (* b HEIGHT)) + (eq! [ stack/STACK_ITEM_POP 4 ] b) + (eq! [ stack/STACK_ITEM_STAMP 4 ] (* b MULTIPLIER___STACK_STAMP HUB_STAMP)) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 3 b))) + )) + diff --git a/hub/constraints/stack-patterns/create-stack-pattern.lisp b/hub/constraints/stack-patterns/create-stack-pattern.lisp new file mode 100644 index 000000000..1ebceb8a4 --- /dev/null +++ b/hub/constraints/stack-patterns/create-stack-pattern.lisp @@ -0,0 +1,49 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.18 createStackPattern[b] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (create-stack-pattern (b :binary)) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 1) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 1) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 2) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 2) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (empty-stack-item 4) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT 2 b))) + ;; stack item 5; + (next (empty-stack-item 1)) + ;; stack item 6; + (will-eq! [ stack/STACK_ITEM_HEIGHT 2 ] (* b (- HEIGHT 3))) + (will-eq! [ stack/STACK_ITEM_POP 2 ] b) + (will-eq! [ stack/STACK_ITEM_STAMP 2 ] (* b (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 3))) + ;; stack item 7; + (dec-scnd-row-stack-item-X-height-by-Y 3 0) + (pop-scnd-row-stack-item 3) + (set-scnd-row-stack-item-stamp 3 0) + ;; stack item 8; + (dec-scnd-row-stack-item-X-height-by-Y 4 (+ 2 b)) + (push-scnd-row-stack-item 4) + (set-scnd-row-stack-item-stamp 4 4) + )) + diff --git a/hub/constraints/stack-patterns/dup-stack-pattern.lisp b/hub/constraints/stack-patterns/dup-stack-pattern.lisp new file mode 100644 index 000000000..6ecf6a5d5 --- /dev/null +++ b/hub/constraints/stack-patterns/dup-stack-pattern.lisp @@ -0,0 +1,40 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.13 dupStackPattern[param] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (dup-stack-pattern param) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 param) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 param) + (push-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + (eq! [ stack/STACK_ITEM_VALUE_HI 2 ] [ stack/STACK_ITEM_VALUE_HI 1 ]) + (eq! [ stack/STACK_ITEM_VALUE_LO 2 ] [ stack/STACK_ITEM_VALUE_LO 1 ]) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (inc-frst-row-stack-item-X-height-by-Y 4 1) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 2) + (eq! [ stack/STACK_ITEM_VALUE_HI 4 ] [ stack/STACK_ITEM_VALUE_HI 1 ]) + (eq! [ stack/STACK_ITEM_VALUE_LO 4 ] [ stack/STACK_ITEM_VALUE_LO 1 ]) + ;; height update; + (debug (eq! HEIGHT_NEW (+ HEIGHT 1))))) + diff --git a/hub/constraints/stack-patterns/empty-stack-pattern.lisp b/hub/constraints/stack-patterns/empty-stack-pattern.lisp new file mode 100644 index 000000000..d8ddf2564 --- /dev/null +++ b/hub/constraints/stack-patterns/empty-stack-pattern.lisp @@ -0,0 +1,18 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.4 emptyStackPattern ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (empty-stack-pattern) (for k [4] (empty-stack-item k))) ;; "" diff --git a/hub/constraints/stack-patterns/load-store-stack-pattern.lisp b/hub/constraints/stack-patterns/load-store-stack-pattern.lisp new file mode 100644 index 000000000..489330c13 --- /dev/null +++ b/hub/constraints/stack-patterns/load-store-stack-pattern.lisp @@ -0,0 +1,34 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.12 loadStoreStackPattern[b] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (load-store-stack-pattern (b :binary)) + (begin + ;; stack item 1: + (inc-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (empty-stack-item 2) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (dec-frst-row-stack-item-X-height-by-Y 4 b) + (eq! [ stack/STACK_ITEM_POP 4 ] b) + (set-frst-row-stack-item-stamp 4 1) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT b b))))) + diff --git a/hub/constraints/stack-patterns/log-stack-pattern.lisp b/hub/constraints/stack-patterns/log-stack-pattern.lisp new file mode 100644 index 000000000..560a0d05a --- /dev/null +++ b/hub/constraints/stack-patterns/log-stack-pattern.lisp @@ -0,0 +1,54 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.15 logStackPattern[param, b1, b2, b3, b4] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (b-sum-1 b1 b2 b3 b4) (+ b1 b2 b3 b4)) +(defun (b-sum-2 b2 b3 b4) (+ b2 b3 b4)) +(defun (b-sum-3 b3 b4) (+ b3 b4)) +(defun (b-sum-4 b4) b4 ) + +(defun (log-stack-pattern param (b1 :binary) (b2 :binary) (b3 :binary) (b4 :binary)) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 0) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (dec-frst-row-stack-item-X-height-by-Y 2 1) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (empty-stack-item 3) + ;; stack item 4: + (empty-stack-item 4) + ;; height update; + (debug (eq! HEIGHT_NEW (- HEIGHT param 2))) + ;; stack item 5: + (will-eq! [ stack/STACK_ITEM_HEIGHT 1 ] (* (b-sum-1 b1 b2 b3 b4) (- HEIGHT 2))) + (will-eq! [ stack/STACK_ITEM_POP 1 ] (b-sum-1 b1 b2 b3 b4)) + (will-eq! [ stack/STACK_ITEM_STAMP 1 ] (* (b-sum-1 b1 b2 b3 b4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 2))) + ;; stack item 6: + (will-eq! [ stack/STACK_ITEM_HEIGHT 2 ] (* (b-sum-2 b2 b3 b4) (- HEIGHT 3))) + (will-eq! [ stack/STACK_ITEM_POP 2 ] (b-sum-2 b2 b3 b4)) + (will-eq! [ stack/STACK_ITEM_STAMP 2 ] (* (b-sum-2 b2 b3 b4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 3))) + ;; stack item 7: + (will-eq! [ stack/STACK_ITEM_HEIGHT 3 ] (* (b-sum-3 b3 b4) (- HEIGHT 4))) + (will-eq! [ stack/STACK_ITEM_POP 3 ] (b-sum-3 b3 b4)) + (will-eq! [ stack/STACK_ITEM_STAMP 3 ] (* (b-sum-3 b3 b4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 4))) + ;; stack item 8: + (will-eq! [ stack/STACK_ITEM_HEIGHT 4 ] (* (b-sum-4 b4) (- HEIGHT 5))) + (will-eq! [ stack/STACK_ITEM_POP 4 ] (b-sum-4 b4)) + (will-eq! [ stack/STACK_ITEM_STAMP 4 ] (* (b-sum-4 b4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 5))))) diff --git a/hub/constraints/stack-patterns/request-hash.lisp b/hub/constraints/stack-patterns/request-hash.lisp new file mode 100644 index 000000000..ed4682b9e --- /dev/null +++ b/hub/constraints/stack-patterns/request-hash.lisp @@ -0,0 +1,22 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5. requestHash and maybeRequestHash ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (maybe-request-hash relative_offset bit) (eq! (shift stack/HASH_INFO_FLAG relative_offset) + bit)) + +(defun (request-hash relative_offset) (maybe-request-hash relative_offset 1)) diff --git a/hub/constraints/stack-patterns/swap-stack-pattern.lisp b/hub/constraints/stack-patterns/swap-stack-pattern.lisp new file mode 100644 index 000000000..f61cf21db --- /dev/null +++ b/hub/constraints/stack-patterns/swap-stack-pattern.lisp @@ -0,0 +1,42 @@ +(module hub) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; 5 Stack patterns ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 5.14 swapStackPattern[param] ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (swap-stack-pattern param) + (begin + ;; stack item 1: + (dec-frst-row-stack-item-X-height-by-Y 1 param) + (pop-frst-row-stack-item 1) + (set-frst-row-stack-item-stamp 1 0) + ;; stack item 2: + (inc-frst-row-stack-item-X-height-by-Y 2 0) + (pop-frst-row-stack-item 2) + (set-frst-row-stack-item-stamp 2 1) + ;; stack item 3: + (dec-frst-row-stack-item-X-height-by-Y 3 param) + (push-frst-row-stack-item 3) + (set-frst-row-stack-item-stamp 3 2) + (eq! [ stack/STACK_ITEM_VALUE_HI 3 ] [ stack/STACK_ITEM_VALUE_HI 2 ]) + (eq! [ stack/STACK_ITEM_VALUE_LO 3 ] [ stack/STACK_ITEM_VALUE_LO 2 ]) + ;; stack item 4: + (inc-frst-row-stack-item-X-height-by-Y 4 0) + (push-frst-row-stack-item 4) + (set-frst-row-stack-item-stamp 4 3) + (eq! [ stack/STACK_ITEM_VALUE_HI 4 ] [ stack/STACK_ITEM_VALUE_HI 1 ]) + (eq! [ stack/STACK_ITEM_VALUE_LO 4 ] [ stack/STACK_ITEM_VALUE_LO 1 ]) + ;; height update; + (debug (eq! HEIGHT_NEW HEIGHT)))) + diff --git a/hub/lookups/hub_into_instruction_decoder_cancun.lispX b/hub/lookups/hub_into_instruction_decoder_cancun.lispX new file mode 100644 index 000000000..21bb6d4e9 --- /dev/null +++ b/hub/lookups/hub_into_instruction_decoder_cancun.lispX @@ -0,0 +1,89 @@ +(defun (hub-into-instruction-decoder-trigger) hub.PEEK_AT_STACK) + +(deflookup hub-into-instdecoder + ;; target columns + ( + instdecoder_cancun.OPCODE + instdecoder_cancun.STATIC_GAS + instdecoder_cancun.TWO_LINE_INSTRUCTION + instdecoder_cancun.FLAG_1 + instdecoder_cancun.FLAG_2 + instdecoder_cancun.FLAG_3 + instdecoder_cancun.FLAG_4 + instdecoder_cancun.MXP_FLAG + instdecoder_cancun.STATIC_FLAG + instdecoder_cancun.ALPHA + instdecoder_cancun.DELTA + ;; + instdecoder_cancun.FAMILY_ACCOUNT + instdecoder_cancun.FAMILY_ADD + instdecoder_cancun.FAMILY_BIN + instdecoder_cancun.FAMILY_BATCH + instdecoder_cancun.FAMILY_CALL + instdecoder_cancun.FAMILY_CONTEXT + instdecoder_cancun.FAMILY_COPY + instdecoder_cancun.FAMILY_MCOPY + instdecoder_cancun.FAMILY_CREATE + instdecoder_cancun.FAMILY_DUP + instdecoder_cancun.FAMILY_EXT + instdecoder_cancun.FAMILY_HALT + instdecoder_cancun.FAMILY_INVALID + instdecoder_cancun.FAMILY_JUMP + instdecoder_cancun.FAMILY_KEC + instdecoder_cancun.FAMILY_LOG + instdecoder_cancun.FAMILY_MACHINE_STATE + instdecoder_cancun.FAMILY_MOD + instdecoder_cancun.FAMILY_MUL + instdecoder_cancun.FAMILY_PUSH_POP + instdecoder_cancun.FAMILY_SHF + instdecoder_cancun.FAMILY_STACK_RAM + instdecoder_cancun.FAMILY_STORAGE + instdecoder_cancun.FAMILY_SWAP + instdecoder_cancun.FAMILY_TRANSACTION + instdecoder_cancun.FAMILY_WCP + ;; + ) + + ;; source columns + ( + (* hub.stack/INSTRUCTION (hub-into-instruction-decoder-trigger)) + (* hub.stack/STATIC_GAS (hub-into-instruction-decoder-trigger)) + (* hub.TWO_LINE_INSTRUCTION (hub-into-instruction-decoder-trigger)) + (* [hub.stack/DEC_FLAG 1] (hub-into-instruction-decoder-trigger)) + (* [hub.stack/DEC_FLAG 2] (hub-into-instruction-decoder-trigger)) + (* [hub.stack/DEC_FLAG 3] (hub-into-instruction-decoder-trigger)) + (* [hub.stack/DEC_FLAG 4] (hub-into-instruction-decoder-trigger)) + (* hub.stack/MXP_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/STATIC_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/ALPHA (hub-into-instruction-decoder-trigger)) + (* hub.stack/DELTA (hub-into-instruction-decoder-trigger)) + ;; + (* hub.stack/ACC_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/ADD_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/BIN_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/BTC_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/CALL_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/CON_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/COPY_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/MCOPY_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/CREATE_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/DUP_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/EXT_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/HALT_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/INVALID_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/JUMP_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/KEC_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/LOG_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/MACHINE_STATE_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/MOD_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/MUL_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/PUSHPOP_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/SHF_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/STACKRAM_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/STO_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/SWAP_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/TXN_FLAG (hub-into-instruction-decoder-trigger)) + (* hub.stack/WCP_FLAG (hub-into-instruction-decoder-trigger)) + ;; + ) +) diff --git a/hub/lookups/hub_into_instruction_decoder.lisp b/hub/lookups/hub_into_instruction_decoder_london.lisp similarity index 100% rename from hub/lookups/hub_into_instruction_decoder.lisp rename to hub/lookups/hub_into_instruction_decoder_london.lisp diff --git a/hub/lookups/hub_into_mxp_cancun.lisp b/hub/lookups/hub_into_mxp_cancun.lisp new file mode 100644 index 000000000..488b2cbe7 --- /dev/null +++ b/hub/lookups/hub_into_mxp_cancun.lisp @@ -0,0 +1,45 @@ +(defun (hub-into-mxp-trigger) + (* hub.PEEK_AT_MISCELLANEOUS hub.misc/MXP_FLAG)) + +(deflookup + hub-into-mxp + ;; target columns + ( + mxplon.STAMP + mxplon.CN + mxplon.INST + mxplon.MXPX + mxplon.DEPLOYS + mxplon.OFFSET_1_HI + mxplon.OFFSET_1_LO + mxplon.OFFSET_2_HI + mxplon.OFFSET_2_LO + mxplon.SIZE_1_HI + mxplon.SIZE_1_LO + mxplon.SIZE_2_HI + mxplon.SIZE_2_LO + mxplon.WORDS + mxplon.GAS_MXP + mxplon.SIZE_1_NONZERO_NO_MXPX + mxplon.SIZE_2_NONZERO_NO_MXPX + ) + ;; source columns + ( + (* hub.MXP_STAMP (hub-into-mxp-trigger)) + (* hub.CONTEXT_NUMBER (hub-into-mxp-trigger)) + (* hub.misc/MXP_INST (hub-into-mxp-trigger)) + (* hub.misc/MXP_MXPX (hub-into-mxp-trigger)) + (* hub.misc/MXP_DEPLOYS (hub-into-mxp-trigger)) + (* hub.misc/MXP_OFFSET_1_HI (hub-into-mxp-trigger)) + (* hub.misc/MXP_OFFSET_1_LO (hub-into-mxp-trigger)) + (* hub.misc/MXP_OFFSET_2_HI (hub-into-mxp-trigger)) + (* hub.misc/MXP_OFFSET_2_LO (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_1_HI (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_1_LO (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_2_HI (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_2_LO (hub-into-mxp-trigger)) + (* hub.misc/MXP_WORDS (hub-into-mxp-trigger)) + (* hub.misc/MXP_GAS_MXP (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_1_NONZERO_NO_MXPX (hub-into-mxp-trigger)) + (* hub.misc/MXP_SIZE_2_NONZERO_NO_MXPX (hub-into-mxp-trigger)) + )) diff --git a/hub/lookups/hub_into_mxp.lisp b/hub/lookups/hub_into_mxp_london.lispX similarity index 78% rename from hub/lookups/hub_into_mxp.lisp rename to hub/lookups/hub_into_mxp_london.lispX index 36465ca7c..4d87d6f43 100644 --- a/hub/lookups/hub_into_mxp.lisp +++ b/hub/lookups/hub_into_mxp_london.lispX @@ -5,24 +5,24 @@ hub-into-mxp ;; target columns ( - mxp.STAMP - mxp.CN - mxp.INST - mxp.MXPX - mxp.DEPLOYS - mxp.OFFSET_1_HI - mxp.OFFSET_1_LO - mxp.OFFSET_2_HI - mxp.OFFSET_2_LO - mxp.SIZE_1_HI - mxp.SIZE_1_LO - mxp.SIZE_2_HI - mxp.SIZE_2_LO - mxp.WORDS - mxp.GAS_MXP - mxp.MTNTOP - mxp.SIZE_1_NONZERO_NO_MXPX - mxp.SIZE_2_NONZERO_NO_MXPX + mxplon.STAMP + mxplon.CN + mxplon.INST + mxplon.MXPX + mxplon.DEPLOYS + mxplon.OFFSET_1_HI + mxplon.OFFSET_1_LO + mxplon.OFFSET_2_HI + mxplon.OFFSET_2_LO + mxplon.SIZE_1_HI + mxplon.SIZE_1_LO + mxplon.SIZE_2_HI + mxplon.SIZE_2_LO + mxplon.WORDS + mxplon.GAS_MXP + mxplon.MTNTOP + mxplon.SIZE_1_NONZERO_NO_MXPX + mxplon.SIZE_2_NONZERO_NO_MXPX ) ;; source columns ( diff --git a/mxp/mxpcan/columns/common.lisp b/mxp/mxpcan/columns/common.lisp new file mode 100644 index 000000000..62a005457 --- /dev/null +++ b/mxp/mxpcan/columns/common.lisp @@ -0,0 +1,19 @@ +(module mxpcan (>= EVM_FORK EVM_CANCUN)) +;; mdule will be used from Cancun fork and on + +(defcolumns + ( MXP_STAMP :i16 ) + ( CN :i16 ) + ( DECODER :binary@prove ) + ( MACRO :binary@prove ) + ( SCENARIO :binary@prove ) + ( COMPUTATION :binary@prove ) + ( CT :i4 ) + ( CT_MAX :i4 ) + ) + +(defalias + DECDR DECODER + SCNRI SCENARIO + CMPTN COMPUTATION + ) diff --git a/mxp/mxpcan/columns/computation/calls.lisp b/mxp/mxpcan/columns/computation/calls.lisp new file mode 100644 index 000000000..dc0689e63 --- /dev/null +++ b/mxp/mxpcan/columns/computation/calls.lisp @@ -0,0 +1,49 @@ +(module mxpcan) + +(defun (euc-call relof + a + b) + (begin + (eq! (shift computation/EUC_FLAG relof) 1) + (eq! (shift computation/ARG_1_LO relof) a) + (eq! (shift computation/ARG_2_LO relof) b))) + + +(defun (wcp-call-to-LT relof + arg_1_hi + arg_1_lo + arg_2_hi + arg_2_lo) + (begin + (eq! (shift computation/WCP_FLAG relof) 1 ) + (eq! (shift computation/ARG_1_HI relof) arg_1_hi ) + (eq! (shift computation/ARG_1_LO relof) arg_1_lo ) + (eq! (shift computation/ARG_2_HI relof) arg_2_hi ) + (eq! (shift computation/ARG_2_LO relof) arg_2_lo ) + (eq! (shift computation/EXO_INST relof) EVM_INST_LT ))) + + +(defun (wcp-call-to-LEQ relof + arg_1_hi + arg_1_lo + arg_2_hi + arg_2_lo) + (begin + (eq! (shift computation/WCP_FLAG relof) 1 ) + (eq! (shift computation/ARG_1_HI relof) arg_1_hi ) + (eq! (shift computation/ARG_1_LO relof) arg_1_lo ) + (eq! (shift computation/ARG_2_HI relof) arg_2_hi ) + (eq! (shift computation/ARG_2_LO relof) arg_2_lo ) + (eq! (shift computation/EXO_INST relof) WCP_INST_LEQ ))) + + +(defun (wcp-call-to-ISZERO relof + arg_1_hi + arg_1_lo) + (begin + (eq! (shift computation/WCP_FLAG relof) 1 ) + (eq! (shift computation/ARG_1_HI relof) arg_1_hi ) + (eq! (shift computation/ARG_1_LO relof) arg_1_lo ) + (eq! (shift computation/ARG_2_HI relof) 0 ) + (eq! (shift computation/ARG_2_LO relof) 0 ) + (eq! (shift computation/EXO_INST relof) EVM_INST_ISZERO ))) diff --git a/mxp/mxpcan/columns/computation/columns.lisp b/mxp/mxpcan/columns/computation/columns.lisp new file mode 100644 index 000000000..70cae62be --- /dev/null +++ b/mxp/mxpcan/columns/computation/columns.lisp @@ -0,0 +1,19 @@ +(module mxpcan) + + +(defperspective computation + ;; selector + COMPUTATION + ;; computation columns + ( + ( WCP_FLAG :binary@prove ) + ( EUC_FLAG :binary@prove ) + ( EXO_INST :byte ) + ( ARG_1_HI :i128 ) + ( ARG_1_LO :i128 ) + ( ARG_2_HI :i128 ) + ( ARG_2_LO :i128 ) + ( RES_A :i32 ) + ( RES_B :i32 ) + ) + ) diff --git a/mxp/mxpcan/columns/decoder.lisp b/mxp/mxpcan/columns/decoder.lisp new file mode 100644 index 000000000..a747cf761 --- /dev/null +++ b/mxp/mxpcan/columns/decoder.lisp @@ -0,0 +1,21 @@ +(module mxpcan) + +(defperspective decoder + ;; selector + DECODER + ;; instruction decoded columns + ( + ( INST :byte ) + ( IS_MSIZE :binary ) + ( IS_RETURN :binary ) + ( IS_MCOPY :binary ) + ( IS_FIXED_SIZE_32 :binary ) + ( IS_FIXED_SIZE_1 :binary ) + ( IS_SINGLE_MAX_OFFSET :binary ) + ( IS_DOUBLE_MAX_OFFSET :binary ) + ( IS_WORD_PRICING :binary ) + ( IS_BYTE_PRICING :binary ) + ( G_WORD :byte ) + ( G_BYTE :byte ) + ) + ) diff --git a/mxp/mxpcan/columns/macro.lisp b/mxp/mxpcan/columns/macro.lisp new file mode 100644 index 000000000..ffb180a4a --- /dev/null +++ b/mxp/mxpcan/columns/macro.lisp @@ -0,0 +1,25 @@ +(module mxpcan) + +(defperspective macro + ;; selector + MACRO + ;; macro-instruction fields + ( + ( INST :byte ) + ( DEPLOYING :binary ) + ( OFFSET_1_HI :i128 ) + ( OFFSET_1_LO :i128 ) + ( SIZE_1_HI :i128 ) + ( SIZE_1_LO :i128 ) + ( OFFSET_2_HI :i128 ) + ( OFFSET_2_LO :i128 ) + ( SIZE_2_HI :i128 ) + ( SIZE_2_LO :i128 ) + ( RES :i32 ) + ( MXPX :binary ) + ( GAS_MXP :i64 ) + ( MAY_TRIGGER_MMU :binary ) + ( S1NZNOMXPX :binary ) + ( S2NZNOMXPX :binary ) + ) + ) diff --git a/mxp/mxpcan/columns/scenario/columns.lisp b/mxp/mxpcan/columns/scenario/columns.lisp new file mode 100644 index 000000000..57cd74a9e --- /dev/null +++ b/mxp/mxpcan/columns/scenario/columns.lisp @@ -0,0 +1,20 @@ +(module mxpcan) + +(defperspective scenario + ;; selector + SCENARIO + ;; scenario columns + ( + ;; scenario flags + ( MSIZE :binary@prove ) + ( TRIVIAL :binary@prove ) + ( MXPX :binary@prove ) + ( STATE_UPDATE_WORD_PRICING :binary@prove ) + ( STATE_UPDATE_BYTE_PRICING :binary@prove ) + ;; state columns + ( WORDS :i33 ) ;; i32 + i32 = i33 ... + ( WORDS_NEW :i33 ) ;; i32 + i32 = i33 ... + ( C_MEM :i64 ) + ( C_MEM_NEW :i64 ) + ) + ) diff --git a/mxp/mxpcan/columns/scenario/shorthands.lisp b/mxp/mxpcan/columns/scenario/shorthands.lisp new file mode 100644 index 000000000..ffa0db0ce --- /dev/null +++ b/mxp/mxpcan/columns/scenario/shorthands.lisp @@ -0,0 +1,33 @@ +(module mxpcan) + + +(defun (mxp-scenario-shorthand---scenario-sum) + (+ (mxp-scenario-shorthand---no-state-update) + (mxp-scenario-shorthand---state-update) + )) + +(defun (mxp-scenario-shorthand---no-state-update) + (+ scenario/MSIZE + scenario/TRIVIAL + scenario/MXPX + ;; scenario/STATE_UPDATE_WORD_PRICING + ;; scenario/STATE_UPDATE_BYTE_PRICING + )) + +(defun (mxp-scenario-shorthand---state-update) + (+ ;; scenario/MSIZE + ;; scenario/TRIVIAL + ;; scenario/MXPX + scenario/STATE_UPDATE_WORD_PRICING + scenario/STATE_UPDATE_BYTE_PRICING + )) + +(defun (mxp-scenario-shorthand---not-msize-nor-trivial) + (+ (mxp-scenario-shorthand---state-update) + scenario/MXPX + )) + +(defun (mxp-scenario-shorthand---not-msize) + (+ (mxp-scenario-shorthand---not-msize-nor-trivial) + scenario/TRIVIAL + )) diff --git a/mxp/mxpcan/computations/_constants_and_shorthands.lisp b/mxp/mxpcan/computations/_constants_and_shorthands.lisp new file mode 100644 index 000000000..a6d1591d6 --- /dev/null +++ b/mxp/mxpcan/computations/_constants_and_shorthands.lisp @@ -0,0 +1,95 @@ +(module mxpcan) + +;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Row offsets ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;; + +(defconst + ROW_OFFSET___1ST_SIZE___ZERONESS_TEST 1 + ROW_OFFSET___2ND_SIZE___ZERONESS_TEST 2 + ROW_OFFSET___1ST_SIZE___SMALLNESS_TEST 3 + ROW_OFFSET___2ND_SIZE___SMALLNESS_TEST 4 + ROW_OFFSET___1ST_OFFSET___SMALLNESS_TEST 5 + ROW_OFFSET___2ND_OFFSET___SMALLNESS_TEST 6 + ROW_OFFSET___COMPARISON_OF_MAX_OFFSETS 7 + ROW_OFFSET___FLOOR_OF_MAX_OFFSET_OVER_32 8 + ROW_OFFSET___FLOOR_OF_SQUARE_OVER_512 9 + ROW_OFFSET___COMPARISON_OF_WORDS_AND_EYP_A 10 + ROW_OFFSET___CEILING_OF_SIZE_OVER_32 11 + ) + + +;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constants ;; +;; ;; +;;;;;;;;;;;;;;;;;;; + + +(defconst + MXPX_THRESHOLD 0xffffffff ;; 256 ** 4 - 1 + ) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Scenario guards ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; scenario guards +(defun (mxp-guard---msize) (* SCENARIO scenario/MSIZE )) +(defun (mxp-guard---trivial) (* SCENARIO scenario/TRIVIAL )) +(defun (mxp-guard---mxpx) (* SCENARIO scenario/MXPX )) +(defun (mxp-guard---state-update-word-pricing) (* SCENARIO scenario/STATE_UPDATE_WORD_PRICING )) +(defun (mxp-guard---state-update-byte-pricing) (* SCENARIO scenario/STATE_UPDATE_BYTE_PRICING )) + +;; umbrella scenario shorthands +(defun (mxp-guard---not-msize) (* SCENARIO (mxp-scenario-shorthand---not-msize))) +(defun (mxp-guard---not-msize-not-trivial) (* SCENARIO (mxp-scenario-shorthand---not-msize-nor-trivial))) +(defun (mxp-guard---state-update) (* SCENARIO (mxp-scenario-shorthand---state-update))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Macro-row parameter shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (mxp-shorthand---offset-1-hi) (shift macro/OFFSET_1_HI NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---offset-1-lo) (shift macro/OFFSET_1_LO NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---size-1-hi) (shift macro/SIZE_1_HI NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---size-1-lo) (shift macro/SIZE_1_LO NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---offset-2-hi) (shift macro/OFFSET_2_HI NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---offset-2-lo) (shift macro/OFFSET_2_LO NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---size-2-hi) (shift macro/SIZE_2_HI NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) +(defun (mxp-shorthand---size-2-lo) (shift macro/SIZE_2_LO NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Instruction-decoder-row parameter shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun (mxp-shorthand---single-offset-instruction) (shift decoder/IS_SINGLE_MAX_OFFSET NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) +(defun (mxp-shorthand---double-offset-instruction) (shift decoder/IS_DOUBLE_MAX_OFFSET NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) +(defun (mxp-shorthand---word-pricing-instruction) (shift decoder/IS_WORD_PRICING NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) +(defun (mxp-shorthand---byte-pricing-instruction) (shift decoder/IS_BYTE_PRICING NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) + + +;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; ;; +;; ;; Scenario-row shorthands ;; +;; ;; ;; +;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; +;; (defun (mxp-shorthand---words) scenario/WORDS ) +;; (defun (mxp-shorthand---words-new) scenario/WORDS_NEW ) +;; (defun (mxp-shorthand---c_mem) scenario/C_MEM ) +;; (defun (mxp-shorthand---c_mem-new) scenario/C_MEM_NEW ) diff --git a/mxp/mxpcan/computations/generalities.lisp b/mxp/mxpcan/computations/generalities.lisp new file mode 100644 index 000000000..c7ca99768 --- /dev/null +++ b/mxp/mxpcan/computations/generalities.lisp @@ -0,0 +1,31 @@ +(module mxpcan) + +(defconstraint computations---generalities---precisely-one-scenario-is-active + (:guard SCENARIO) + (eq! (mxp-scenario-shorthand---scenario-sum) + 1)) + +(defconstraint computations---generalities---setting-MSIZE-scenario-flag + (:guard SCENARIO) + (eq! scenario/MSIZE + (shift decoder/IS_MSIZE NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR))) + + +(defconstraint computations---generalities---setting-MXPX-scenario-flag + (:guard SCENARIO) + (eq! scenario/MXPX + (shift macro/MXPX NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO))) + +(defconstraint computations---generalities---no-state-update-scenario-enforces-no-state-update + (:guard SCENARIO) + (if-not-zero (mxp-scenario-shorthand---no-state-update) + (begin + (eq! scenario/WORDS_NEW scenario/WORDS) + (eq! scenario/C_MEM_NEW scenario/C_MEM) + ))) + +(defconstraint computations---generalities---no-state-update-scenario-enforces-zero-GAS_MXP + (:guard SCENARIO) + (if-not-zero (mxp-scenario-shorthand---no-state-update) + (vanishes! (shift macro/GAS_MXP NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) + )) diff --git a/mxp/mxpcan/computations/msize.lisp b/mxp/mxpcan/computations/msize.lisp new file mode 100644 index 000000000..abfc751cd --- /dev/null +++ b/mxp/mxpcan/computations/msize.lisp @@ -0,0 +1,14 @@ +(module mxpcan) + + +(defconstraint computation---MSIZE-scenario---setting-macro-RES + (:guard (mxp-guard---msize)) + (begin + (eq! (shift macro/RES NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) scenario/WORDS) + (vanishes! (shift macro/MXPX NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO)) + )) + +(defconstraint computation---MSIZE-scenario---both-module-lookup-flags-are-off + (:guard (mxp-guard---msize)) + (debug + (vanishes! (shift (+ computation/WCP_FLAG computation/EUC_FLAG) 1)))) diff --git a/mxp/mxpcan/computations/mxpx.lisp b/mxp/mxpcan/computations/mxpx.lisp new file mode 100644 index 000000000..f2fd95b4f --- /dev/null +++ b/mxp/mxpcan/computations/mxpx.lisp @@ -0,0 +1,3 @@ +(module mxpcan) + +;; we're done diff --git a/mxp/mxpcan/computations/non_msize.lisp b/mxp/mxpcan/computations/non_msize.lisp new file mode 100644 index 000000000..1c31ddc3d --- /dev/null +++ b/mxp/mxpcan/computations/non_msize.lisp @@ -0,0 +1,35 @@ +(module mxpcan) + + +(defconstraint computations---non-msize---ISZERO-test-for-SIZE_1 + (:guard (mxp-guard---not-msize)) + (wcp-call-to-ISZERO ROW_OFFSET___1ST_SIZE___ZERONESS_TEST + (mxp-shorthand---size-1-hi) + (mxp-shorthand---size-1-lo) + )) + +(defconstraint computations---non-msize---ISZERO-test-for-SIZE_2 + (:guard (mxp-guard---not-msize)) + (wcp-call-to-ISZERO ROW_OFFSET___2ND_SIZE___ZERONESS_TEST + (mxp-shorthand---size-2-hi) + (mxp-shorthand---size-2-lo) + )) + +(defun (mxp-shorthand---size-1-is-zero) (shift computation/RES_A ROW_OFFSET___1ST_SIZE___ZERONESS_TEST)) +(defun (mxp-shorthand---size-2-is-zero) (shift computation/RES_A ROW_OFFSET___2ND_SIZE___ZERONESS_TEST)) +(defun (mxp-shorthand---size-1-is-nonzero) (- 1 (mxp-shorthand---size-1-is-zero))) +(defun (mxp-shorthand---size-2-is-nonzero) (- 1 (mxp-shorthand---size-2-is-zero))) + +(defconstraint computations---non-msize---setting-the-TRIVIAL-scenario-flag + (:guard (mxp-guard---not-msize)) + (eq! scenario/TRIVIAL (* (mxp-shorthand---size-1-is-zero) + (mxp-shorthand---size-2-is-zero)))) + +(defconstraint computations---non-msize---justifying-HUB-predictions---S1NZNOMXPX-and-S2NZNOMXPX + (:guard (mxp-guard---not-msize)) + (begin + (eq! (shift macro/MAY_TRIGGER_MMU NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) (* (mxp-shorthand---size-1-is-nonzero) (- 1 scenario/MXPX))) + (eq! (shift macro/S1NZNOMXPX NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) (* (mxp-shorthand---size-1-is-nonzero) (- 1 scenario/MXPX))) + (eq! (shift macro/S2NZNOMXPX NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) (* (mxp-shorthand---size-2-is-nonzero) (- 1 scenario/MXPX))) + )) + diff --git a/mxp/mxpcan/computations/non_msize_non_trivial.lisp b/mxp/mxpcan/computations/non_msize_non_trivial.lisp new file mode 100644 index 000000000..a1cfa9682 --- /dev/null +++ b/mxp/mxpcan/computations/non_msize_non_trivial.lisp @@ -0,0 +1,90 @@ +(module mxpcan) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; SIZE_1/2 smallness checks ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint computations---non-msize-non-trivial---smallness-test-for-SIZE_1 + (:guard (mxp-guard---not-msize-not-trivial)) + (wcp-call-to-LEQ ROW_OFFSET___1ST_SIZE___SMALLNESS_TEST + (mxp-shorthand---size-1-hi) + (mxp-shorthand---size-1-lo) + 0 + MXPX_THRESHOLD + )) + +(defconstraint computations---non-msize-non-trivial---smallness-test-for-SIZE_2 + (:guard (mxp-guard---not-msize-not-trivial)) + (wcp-call-to-LEQ ROW_OFFSET___2ND_SIZE___SMALLNESS_TEST + (mxp-shorthand---size-2-hi) + (mxp-shorthand---size-2-lo) + 0 + MXPX_THRESHOLD + )) + + +(defun (mxp-shorthand---size-1-is-small) (shift computation/RES_A ROW_OFFSET___1ST_SIZE___SMALLNESS_TEST)) +(defun (mxp-shorthand---size-2-is-small) (shift computation/RES_A ROW_OFFSET___2ND_SIZE___SMALLNESS_TEST)) +(defun (mxp-shorthand---size-1-is-large) (- 1 (mxp-shorthand---size-1-is-small))) +(defun (mxp-shorthand---size-2-is-large) (- 1 (mxp-shorthand---size-2-is-small))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OFFSET_1/2 smallness checks ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint computations---non-msize-non-trivial---smallness-test-for-OFFSET_1 + (:guard (mxp-guard---not-msize-not-trivial)) + (wcp-call-to-LEQ ROW_OFFSET___1ST_OFFSET___SMALLNESS_TEST + (mxp-shorthand---offset-1-hi) + (mxp-shorthand---offset-1-lo) + 0 + MXPX_THRESHOLD + )) + +(defconstraint computations---non-msize-non-trivial---smallness-test-for-OFFSET_2 + (:guard (mxp-guard---not-msize-not-trivial)) + (wcp-call-to-LEQ ROW_OFFSET___2ND_OFFSET___SMALLNESS_TEST + (mxp-shorthand---offset-2-hi) + (mxp-shorthand---offset-2-lo) + 0 + MXPX_THRESHOLD + )) + + +(defun (mxp-shorthand---offset-1-is-small) (shift computation/RES_A ROW_OFFSET___1ST_OFFSET___SMALLNESS_TEST)) +(defun (mxp-shorthand---offset-2-is-small) (shift computation/RES_A ROW_OFFSET___2ND_OFFSET___SMALLNESS_TEST)) +(defun (mxp-shorthand---offset-1-is-large) (- 1 (mxp-shorthand---offset-1-is-small))) +(defun (mxp-shorthand---offset-2-is-large) (- 1 (mxp-shorthand---offset-2-is-small))) + + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Scenario guards ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (mxp-shorthand---mxpx-expression-1) (+ (mxp-shorthand---size-1-is-large) + (* (mxp-shorthand---size-1-is-nonzero) + (mxp-shorthand---offset-1-is-large)))) + +(defun (mxp-shorthand---mxpx-expression-2) (+ (mxp-shorthand---size-2-is-large) + (* (mxp-shorthand---size-2-is-nonzero) + (mxp-shorthand---offset-2-is-large)))) + +(defun (mxp-shorthand---mxpx-expression) (+ (mxp-shorthand---mxpx-expression-1) + (mxp-shorthand---mxpx-expression-2))) + +(defconstraint computations---non-msize-non-trivial---justifying-the-MXPX-scenario-flag + (:guard (mxp-guard---not-msize-not-trivial)) + (if-zero (mxp-shorthand---mxpx-expression) + ;; zero case + (eq! scenario/MXPX 0) + ;; nonzero case + (eq! scenario/MXPX 1) + )) diff --git a/mxp/mxpcan/computations/state_update.lisp b/mxp/mxpcan/computations/state_update.lisp new file mode 100644 index 000000000..e8163823a --- /dev/null +++ b/mxp/mxpcan/computations/state_update.lisp @@ -0,0 +1,74 @@ +(module mxpcan) + +(defconstraint computations---state-update---justifying-state-update-scenario-WORD-vs-BYTE + (:guard (mxp-guard---state-update)) + (begin + (eq! scenario/STATE_UPDATE_WORD_PRICING (mxp-shorthand---word-pricing-instruction)) + (eq! scenario/STATE_UPDATE_BYTE_PRICING (mxp-shorthand---byte-pricing-instruction)) + )) + +(defconstraint computations---state-update---comparing-max-offsets + (:guard (mxp-guard---state-update)) + (wcp-call-to-LT ROW_OFFSET___COMPARISON_OF_MAX_OFFSETS + 0 + (* (mxp-shorthand---double-offset-instruction) (mxp-shorthand---max-1)) + 0 + (* (mxp-shorthand---double-offset-instruction) (mxp-shorthand---max-2)) + )) + +(defun (mxp-shorthand---use-parameter-set-2) (shift computation/RES_A ROW_OFFSET___COMPARISON_OF_MAX_OFFSETS)) +(defun (mxp-shorthand---use-parameter-set-1) (- 1 (mxp-shorthand---use-parameter-set-2))) + +(defun (mxp-shorthand---max-1) (+ (mxp-shorthand---offset-1-lo) (mxp-shorthand---size-1-lo))) +(defun (mxp-shorthand---max-2) (+ (mxp-shorthand---offset-2-lo) (mxp-shorthand---size-2-lo))) +(defun (mxp-shorthand---max-offset-1) (- (mxp-shorthand---max-1) 1)) +(defun (mxp-shorthand---max-offset-2) (- (mxp-shorthand---max-2) 1)) +(defun (mxp-shorthand---max-offset) (+ (* (mxp-shorthand---use-parameter-set-1) (mxp-shorthand---max-offset-1)) + (* (mxp-shorthand---use-parameter-set-2) (mxp-shorthand---max-offset-2)))) + +(defconstraint computations---state-update---computing-EYP_A-as-division-of-max-offset-by-32 + (:guard (mxp-guard---state-update)) + (euc-call ROW_OFFSET___FLOOR_OF_MAX_OFFSET_OVER_32 + (mxp-shorthand---max-offset) + WORD_SIZE)) + +(defun (mxp-shorthand---floor) (shift computation/RES_A ROW_OFFSET___FLOOR_OF_MAX_OFFSET_OVER_32)) +(defun (mxp-shorthand---EYP_a) (+ (mxp-shorthand---floor) 1)) + +(defconstraint computations---state-update---computing-quadratic-part-of-C_MEM-as-division-of-EYP_A-squared-over-512 + (:guard (mxp-guard---state-update)) + (euc-call ROW_OFFSET___FLOOR_OF_SQUARE_OVER_512 + (* (mxp-shorthand---EYP_a) (mxp-shorthand---EYP_a)) + 512)) + +(defun (mxp-shorthand---C_MEM-quad-part) (shift computation/RES_A ROW_OFFSET___FLOOR_OF_SQUARE_OVER_512)) +(defun (mxp-shorthand---C_MEM-linr-part) (* GAS_CONST_G_MEMORY (mxp-shorthand---EYP_a))) + +(defconstraint computations---state-update---comparing-EYP_A-to-current-WORDS + (:guard (mxp-guard---state-update)) + (wcp-call-to-LT ROW_OFFSET___COMPARISON_OF_WORDS_AND_EYP_A + 0 + (mxp-shorthand---words) + 0 + (mxp-shorthand---EYP_a))) + +(defun (mxp-shorthand---words) scenario/WORDS ) ;; "" +(defun (mxp-shorthand---words-new) scenario/WORDS_NEW ) ;; "" +(defun (mxp-shorthand---c_mem) scenario/C_MEM ) ;; "" +(defun (mxp-shorthand---c_mem-new) scenario/C_MEM_NEW ) ;; "" +(defun (mxp-shorthand---update-internal-state) (shift computation/RES_A ROW_OFFSET___COMPARISON_OF_WORDS_AND_EYP_A)) + +(defconstraint computations---state-update---updating-the-state---no-state-update + (:guard (mxp-guard---state-update)) + (if-zero (force-bin (mxp-shorthand---update-internal-state)) + (eq! (mxp-shorthand---words-new) (mxp-shorthand---words)) + (eq! (mxp-shorthand---c_mem-new) (mxp-shorthand---c_mem)) + )) + +(defconstraint computations---state-update---updating-the-state---state-update + (:guard (mxp-guard---state-update)) + (if-not-zero (force-bin (mxp-shorthand---update-internal-state)) + (eq! (mxp-shorthand---words-new) (mxp-shorthand---EYP_a)) + (eq! (mxp-shorthand---c_mem-new) (+ (mxp-shorthand---C_MEM-quad-part) + (mxp-shorthand---C_MEM-linr-part))) + )) diff --git a/mxp/mxpcan/computations/state_update_byte_pricing.lisp b/mxp/mxpcan/computations/state_update_byte_pricing.lisp new file mode 100644 index 000000000..0f72d3156 --- /dev/null +++ b/mxp/mxpcan/computations/state_update_byte_pricing.lisp @@ -0,0 +1,23 @@ +(module mxpcan) + + +(defun (mxp-shorthand---is-deploying) (force-bin (shift macro/DEPLOYING NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO))) +(defun (mxp-shorthand---is-RETURN) (force-bin (shift decoder/IS_RETURN NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR))) +(defun (mxp-shorthand---byte-price) (shift decoder/G_BYTE NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) +(defun (mxp-shorthand---real-byte-price) (if-zero (mxp-shorthand---is-RETURN) + ;; IS_RETURN ≡ false i.e. macro/INST ≠ RETURN + (mxp-shorthand---byte-price) + ;; IS_RETURN ≡ true i.e. macro/INST = RETURN + (* (mxp-shorthand---is-deploying) + (mxp-shorthand---byte-price)) + )) +(defun (mxp-shorthand---number-of-bytes) (mxp-shorthand---size-1-lo)) +(defun (mxp-shorthand---extra-byte-cost) (* (mxp-shorthand---size-1-lo) + (mxp-shorthand---real-byte-price))) + + +(defconstraint computations---state-update---byte-pricing---justifying-the-memory-expansion-gas + (:guard (mxp-guard---state-update-word-pricing)) + (eq! (shift macro/GAS_MXP NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) + (+ (- scenario/C_MEM_NEW scenario/C_MEM) + (mxp-shorthand---extra-byte-cost)))) diff --git a/mxp/mxpcan/computations/state_update_word_pricing.lisp b/mxp/mxpcan/computations/state_update_word_pricing.lisp new file mode 100644 index 000000000..77df31973 --- /dev/null +++ b/mxp/mxpcan/computations/state_update_word_pricing.lisp @@ -0,0 +1,19 @@ +(module mxpcan) + + +(defconstraint computations---state-update---word-pricing---computing-the-number-of-input-words + (:guard (mxp-guard---state-update-word-pricing)) + (euc-call ROW_OFFSET___CEILING_OF_SIZE_OVER_32 + (mxp-shorthand---size-1-lo) + WORD_SIZE)) + +(defun (mxp-shorthand---number-of-words) (shift computation/RES_B ROW_OFFSET___CEILING_OF_SIZE_OVER_32)) +(defun (mxp-shorthand---word-price) (shift decoder/G_WORD NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR)) +(defun (mxp-shorthand---extra-word-cost) (* (mxp-shorthand---word-price) + (mxp-shorthand---number-of-words))) + +(defconstraint computations---state-update---word-pricing---justifying-the-memory-expansion-gas + (:guard (mxp-guard---state-update-word-pricing)) + (eq! (shift macro/GAS_MXP NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO) + (+ (- scenario/C_MEM_NEW scenario/C_MEM) + (mxp-shorthand---extra-word-cost)))) diff --git a/mxp/mxpcan/computations/trivial.lisp b/mxp/mxpcan/computations/trivial.lisp new file mode 100644 index 000000000..f2fd95b4f --- /dev/null +++ b/mxp/mxpcan/computations/trivial.lisp @@ -0,0 +1,3 @@ +(module mxpcan) + +;; we're done diff --git a/mxp/mxpcan/consistency/columns.lisp b/mxp/mxpcan/consistency/columns.lisp new file mode 100644 index 000000000..a6f088115 --- /dev/null +++ b/mxp/mxpcan/consistency/columns.lisp @@ -0,0 +1,26 @@ +(module mxpcan) + +(defpermutation + ;; permuted columns + ;; mscp ≡ MXP state consistency permutation + ( + mscp_SCENARIO + mscp_CN + mscp_MXP_STAMP + mscp_C_MEM + mscp_C_MEM_NEW + mscp_WORDS + mscp_WORDS_NEW + ) + ;; + ;; inputs + ( + (+ SCENARIO) + (+ CN) + (+ MXP_STAMP) + scenario/C_MEM + scenario/C_MEM_NEW + scenario/WORDS + scenario/WORDS_NEW + ) + ) diff --git a/mxp/mxpcan/consistency/constraints.lisp b/mxp/mxpcan/consistency/constraints.lisp new file mode 100644 index 000000000..277f499d8 --- /dev/null +++ b/mxp/mxpcan/consistency/constraints.lisp @@ -0,0 +1,37 @@ +(module mxpcan) + +;; mscp_SCENARIO +;; mscp_CN +;; mscp_STAMP +;; mscp_C_MEM +;; mscp_C_MEM_NEW +;; mscp_WORDS +;; mscp_WORDS_NEW + +(defconstraint consistency---initialization---first-scenario-row () + (if-zero (prev mscp_SCENARIO) + (if-not-zero mscp_SCENARIO + (begin + (vanishes! mscp_WORDS) + (vanishes! mscp_C_MEM) + )))) + + +(defconstraint consistency---initialization---first-encounter-with-context () + (if-not-zero (prev mscp_SCENARIO) + (if-not-zero mscp_SCENARIO + (if-not (remained-constant! mscp_CN) + (begin + (vanishes! mscp_WORDS) + (vanishes! mscp_C_MEM) + ))))) + + +(defconstraint consistency---linking-constraints () + (if-not-zero (prev mscp_SCENARIO) + (if-not-zero mscp_SCENARIO + (if (remained-constant! mscp_CN) + (begin + (eq! mscp_WORDS (prev mscp_WORDS_NEW)) + (eq! mscp_C_MEM (prev mscp_C_MEM_NEW)) + ))))) diff --git a/mxp/mxpcan/generalities/_constants_and_shorthands.lisp b/mxp/mxpcan/generalities/_constants_and_shorthands.lisp new file mode 100644 index 000000000..4b2234b23 --- /dev/null +++ b/mxp/mxpcan/generalities/_constants_and_shorthands.lisp @@ -0,0 +1,16 @@ +(module mxpcan) + + +(defconst + ROW_OFFSET___DECDR_TO_MACRO 1 + ROW_OFFSET___DECDR_TO_SCNRI 2 + ROW_OFFSET___MACRO_TO_SCNRI 1 + ;; + ROW_OFFSET___MACRO_TO_DECDR ROW_OFFSET___DECDR_TO_MACRO + ROW_OFFSET___SCNRI_TO_DECDR ROW_OFFSET___DECDR_TO_SCNRI + ROW_OFFSET___SCNRI_TO_MACRO ROW_OFFSET___MACRO_TO_SCNRI + ;; + NEGATIVE_ROW_OFFSET___SCNRI_TO_DECDR (- 0 ROW_OFFSET___SCNRI_TO_DECDR) + NEGATIVE_ROW_OFFSET___SCNRI_TO_MACRO (- 0 ROW_OFFSET___SCNRI_TO_MACRO) + ) + diff --git a/mxp/mxpcan/generalities/binarities.lisp b/mxp/mxpcan/generalities/binarities.lisp new file mode 100644 index 000000000..b4fd6dfba --- /dev/null +++ b/mxp/mxpcan/generalities/binarities.lisp @@ -0,0 +1,3 @@ +(module mxpcan) + +;; taken care of with binary@prove constraints diff --git a/mxp/mxpcan/generalities/constancies.lisp b/mxp/mxpcan/generalities/constancies.lisp new file mode 100644 index 000000000..c1284eccb --- /dev/null +++ b/mxp/mxpcan/generalities/constancies.lisp @@ -0,0 +1,7 @@ +(module mxpcan) + +(defconstraint counter-constancies () + (begin + (counter-constancy CT CT_MAX ) + (counter-constancy CT (mxp-perspective-wght-sum) ) + )) diff --git a/mxp/mxpcan/generalities/heartbeat.lisp b/mxp/mxpcan/generalities/heartbeat.lisp new file mode 100644 index 000000000..52d17bb6e --- /dev/null +++ b/mxp/mxpcan/generalities/heartbeat.lisp @@ -0,0 +1,87 @@ +(module mxpcan) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Heartbeat constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint generalities---heartbeat---perspective-sum-is-binary () + (is-binary (mxp-perspective-sum))) + +(defconstraint generalities---heartbeat---perspective-sum-initially-vanishes (:domain {0}) ;; "" + (vanishes! (mxp-perspective-sum))) + +(defconstraint generalities---heartbeat---perspective-sum-next-value () + (if-zero (force-bin (mxp-perspective-sum)) + ;; mxp-perspective-sum ≡ 0 + (eq! (next (mxp-perspective-sum)) + (next DECODER)) + ;; mxp-perspective-sum ≡ 1 + (eq! (next (mxp-perspective-sum)) + 1))) + +(defconstraint generalities---heartbeat---MXP-stamp-initially-vanishes (:domain {0}) ;; "" + (vanishes! MXP_STAMP)) + +(defun (mxp-stamp-increment) (* (- 1 DECODER) (next DECODER))) + +(defconstraint generalities---heartbeat---MXP-stamp-increments () + (will-inc! MXP_STAMP (mxp-stamp-increment))) + +(defconstraint generalities---heartbeat---automatic-vanishing-during-padding () + (if-zero (force-bin (mxp-perspective-sum)) + (begin + (vanishes! CT_MAX) + (vanishes! CT) + (vanishes! (next CT)) + ))) + +(defconstraint generalities---heartbeat---CT_MAX-vanishes-in-all-phases-except-COMPUTATION () + (if-not-zero (+ DECDR MACRO SCNRI) + (vanishes! CT_MAX))) + +(defconstraint generalities---heartbeat---setting-CT_MAX-during-COMPUTATION () + (if-not-zero SCNRI + (eq! (next CT_MAX) + (next (mxp-ct-max-sum))) + )) + +(defconstraint generalities---heartbeat---illegal-perspective-transitions () + (vanishes! (+ (* DECDR (next (+ DECDR SCNRI CMPTN))) + (* MACRO (next (+ DECDR MACRO CMPTN))) + (* SCNRI (next (+ DECDR MACRO SCNRI ))) + (* CMPTN (next (+ MACRO SCNRI ))) + ))) + +(defconstraint generalities---heartbeat---legal-perspective-transitions (:guard MXP_STAMP) + (if-not-zero (- CT_MAX CT) + ;; CT ≠ CT_MAX case + (eq! (+ (* DECDR (next DECDR)) + (* MACRO (next MACRO)) + (* SCNRI (next SCNRI)) + (* CMPTN (next CMPTN))) + 1) + ;; CT = CT_MAX case + (eq! (+ (* DECDR (next MACRO)) + (* MACRO (next SCNRI)) + (* SCNRI (next CMPTN)) + (* CMPTN (next DECDR))) + 1) + )) + +(defconstraint generalities---heartbeat---CT-updates () + (if-not-zero (- CT_MAX CT) + ;; CT ≠ CT_MAX case + (will-inc! CT 1) + ;; CT = CT_MAX case + (vanishes! (next CT)) + )) + +(defconstraint generalities---heartbeat---finalization-constraints (:domain {-1}) ;; "" + (if-not-zero MXP_STAMP + (begin + ( eq! CMPTN 1 ) + ( eq! CT CT_MAX ) + ))) diff --git a/mxp/mxpcan/generalities/perspectives/computations.lisp b/mxp/mxpcan/generalities/perspectives/computations.lisp new file mode 100644 index 000000000..dfd00b0f8 --- /dev/null +++ b/mxp/mxpcan/generalities/perspectives/computations.lisp @@ -0,0 +1,4 @@ +(module mxpcan) + +(defconstraint generalies---perspectives---computation---lookup-flag-exclusivity (:guard COMPUTATION) + (vanishes! (* computation/WCP_FLAG computation/EUC_FLAG))) diff --git a/mxp/mxpcan/generalities/perspectives/decoder.lisp b/mxp/mxpcan/generalities/perspectives/decoder.lisp new file mode 100644 index 000000000..8823d33c4 --- /dev/null +++ b/mxp/mxpcan/generalities/perspectives/decoder.lisp @@ -0,0 +1,60 @@ +(module mxpcan) + +(defconstraint generalies---perspectives---decoder---MSIZE-vanishings + (:guard DECODER) + (if-not-zero decoder/IS_MSIZE + (begin + (vanishes! (shift macro/OFFSET_1_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/OFFSET_1_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_1_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_1_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/S1NZNOMXPX ROW_OFFSET___DECDR_TO_MACRO)) ;; end of 1st parameter set + (vanishes! (shift macro/OFFSET_2_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/OFFSET_2_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_2_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_2_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/S2NZNOMXPX ROW_OFFSET___DECDR_TO_MACRO)) ;; end of 2nd parameter set + (vanishes! (shift macro/MXPX ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/GAS_MXP ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/MAY_TRIGGER_MMU ROW_OFFSET___DECDR_TO_MACRO)) + ))) + +(defconstraint generalies---perspectives---decoder---RES-is-zero-if-not-MSIZE + (:guard DECODER) + (if-zero decoder/IS_MSIZE + (vanishes! (shift macro/RES ROW_OFFSET___DECDR_TO_MACRO)))) + +(defconstraint generalies---perspectives---decoder---imposing-SIZE_1-for-is-fixed-size-instructions + (:guard DECODER) + (begin + (if-not-zero decoder/IS_FIXED_SIZE_32 + (begin + (eq! (shift macro/SIZE_1_HI ROW_OFFSET___DECDR_TO_MACRO) 0) + (eq! (shift macro/SIZE_1_LO ROW_OFFSET___DECDR_TO_MACRO) 32))) + (if-not-zero decoder/IS_FIXED_SIZE_1 + (begin + (eq! (shift macro/SIZE_1_HI ROW_OFFSET___DECDR_TO_MACRO) 0) + (eq! (shift macro/SIZE_1_LO ROW_OFFSET___DECDR_TO_MACRO) 1))) + )) + + +(defconstraint generalies---perspectives---decoder---2nd-parameters-vanish-for-single-parameter-set-instructions + (:guard DECODER) + (if-zero decoder/IS_DOUBLE_MAX_OFFSET + (begin + (vanishes! (shift macro/OFFSET_2_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/OFFSET_2_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_2_HI ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/SIZE_2_LO ROW_OFFSET___DECDR_TO_MACRO)) + (vanishes! (shift macro/S2NZNOMXPX ROW_OFFSET___DECDR_TO_MACRO)) ;; end of 2nd parameter set + ))) + +(defconstraint generalies---perspectives---decoder---MCOPY-expects-equal-first-and-second-size-parameters + (:guard DECODER) + (if-not-zero decoder/IS_MCOPY + (begin + (eq! (shift macro/SIZE_1_HI ROW_OFFSET___DECDR_TO_MACRO) + (shift macro/SIZE_2_HI ROW_OFFSET___DECDR_TO_MACRO)) + (eq! (shift macro/SIZE_1_LO ROW_OFFSET___DECDR_TO_MACRO) + (shift macro/SIZE_2_LO ROW_OFFSET___DECDR_TO_MACRO)) + ))) diff --git a/mxp/mxpcan/generalities/shorthands.lisp b/mxp/mxpcan/generalities/shorthands.lisp new file mode 100644 index 000000000..3e71b63c4 --- /dev/null +++ b/mxp/mxpcan/generalities/shorthands.lisp @@ -0,0 +1,36 @@ +(module mxpcan) + +(defun (mxp-perspective-sum) + (+ DECDR + MACRO + SCNRI + CMPTN)) + +(defun (mxp-perspective-wght-sum) + (+ (* 1 DECDR ) + (* 2 MACRO ) + (* 3 SCNRI ) + (* 4 CMPTN ))) + +(defun (mxp-ct-max-sum) + (+ (* CT_MAX_MSIZE scenario/MSIZE ) + (* CT_MAX_TRIV scenario/TRIVIAL ) + (* CT_MAX_MXPX scenario/MXPX ) + (* CT_MAX_UPDT_W scenario/STATE_UPDATE_WORD_PRICING ) + (* CT_MAX_UPDT_B scenario/STATE_UPDATE_BYTE_PRICING ) + )) + + +(defconst + nROWS_MSIZE 1 + nROWS_TRIV 2 + nROWS_MXPX 6 + nROWS_UPDT_W 10 + nROWS_UPDT_B 11 + + CT_MAX_MSIZE (- nROWS_MSIZE 1) + CT_MAX_TRIV (- nROWS_TRIV 1) + CT_MAX_MXPX (- nROWS_MXPX 1) + CT_MAX_UPDT_W (- nROWS_UPDT_W 1) + CT_MAX_UPDT_B (- nROWS_UPDT_B 1) + ) \ No newline at end of file diff --git a/mxp/mxpcan/lookups/mxp_into_euc.lisp b/mxp/mxpcan/lookups/mxp_into_euc.lisp new file mode 100644 index 000000000..47ec2b759 --- /dev/null +++ b/mxp/mxpcan/lookups/mxp_into_euc.lisp @@ -0,0 +1,23 @@ +(defun + (mxp-to-euc-selector) + (* mxpcan.COMPUTATION mxpcan.computation/EUC_FLAG) + ) + +(deflookup + mxp-into-euc + ;reference columns + ( + euc.DIVIDEND + euc.DIVISOR + euc.QUOTIENT + euc.CEIL + euc.DONE + ) + ;source columns + ( + (* mxpcan.computation/ARG_1_LO (mxp-to-euc-selector)) + (* mxpcan.computation/ARG_2_LO (mxp-to-euc-selector)) + (* mxpcan.computation/RES_A (mxp-to-euc-selector)) + (* mxpcan.computation/RES_B (mxp-to-euc-selector)) + (mxp-to-euc-selector) + )) diff --git a/mxp/mxpcan/lookups/mxp_into_instruction_decoder.lisp b/mxp/mxpcan/lookups/mxp_into_instruction_decoder.lisp new file mode 100644 index 000000000..dc9a6ff3c --- /dev/null +++ b/mxp/mxpcan/lookups/mxp_into_instruction_decoder.lisp @@ -0,0 +1,41 @@ +(defun (mxp-into-instruction-decoder-selector) mxpcan.DECODER) ;; "" + +(deflookup hub-into-instdecoder + ;; + ;; target columns + ;; + ( + instdecoder_cancun.MXP_FLAG + instdecoder_cancun.OPCODE + instdecoder_cancun.IS_MSIZE + instdecoder_cancun.IS_RETURN + instdecoder_cancun.IS_MCOPY + instdecoder_cancun.IS_FIXED_SIZE_32 + instdecoder_cancun.IS_FIXED_SIZE_1 + instdecoder_cancun.IS_SINGLE_MAX_OFFSET + instdecoder_cancun.IS_DOUBLE_MAX_OFFSET + instdecoder_cancun.IS_WORD_PRICING + instdecoder_cancun.IS_BYTE_PRICING + instdecoder_cancun.BILLING_PER_WORD + instdecoder_cancun.BILLING_PER_BYTE + ) + ;; + ;; source columns + ;; + ( + (* 1 (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/INST (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_MSIZE (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_RETURN (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_MCOPY (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_FIXED_SIZE_32 (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_FIXED_SIZE_1 (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_SINGLE_MAX_OFFSET (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_DOUBLE_MAX_OFFSET (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_WORD_PRICING (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/IS_BYTE_PRICING (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/G_WORD (mxp-into-instruction-decoder-selector)) + (* mxpcan.decoder/G_BYTE (mxp-into-instruction-decoder-selector)) + ;; + ) +) diff --git a/mxp/mxpcan/lookups/mxp_into_wcp.lisp b/mxp/mxpcan/lookups/mxp_into_wcp.lisp new file mode 100644 index 000000000..3663aefb3 --- /dev/null +++ b/mxp/mxpcan/lookups/mxp_into_wcp.lisp @@ -0,0 +1,25 @@ +(defun + (mxp-to-wcp-selector) + (* mxpcan.COMPUTATION mxpcan.computation/WCP_FLAG) + ) + +(deflookup + mxp-into-wcp + ;reference columns + ( + wcp.INST + wcp.ARGUMENT_1_HI + wcp.ARGUMENT_1_LO + wcp.ARGUMENT_2_HI + wcp.ARGUMENT_2_LO + wcp.RESULT + ) + ;source columns + ( + (* mxpcan.computation/EXO_INST (mxp-to-wcp-selector)) + (* mxpcan.computation/ARG_1_HI (mxp-to-wcp-selector)) + (* mxpcan.computation/ARG_1_LO (mxp-to-wcp-selector)) + (* mxpcan.computation/ARG_2_HI (mxp-to-wcp-selector)) + (* mxpcan.computation/ARG_2_LO (mxp-to-wcp-selector)) + (* mxpcan.computation/RES_A (mxp-to-wcp-selector)) + )) diff --git a/mxp/columns.lisp b/mxp/mxplon/columns.lisp similarity index 91% rename from mxp/columns.lisp rename to mxp/mxplon/columns.lisp index 68307634c..2c100b749 100644 --- a/mxp/columns.lisp +++ b/mxp/mxplon/columns.lisp @@ -1,4 +1,5 @@ -(module mxp) +(module mxplon (< EVM_FORK EVM_CANCUN)) +;; module will be used until Shanghai and then switch to mxpcan (defcolumns (STAMP :i32) diff --git a/mxp/constants.lisp b/mxp/mxplon/constants.lisp similarity index 90% rename from mxp/constants.lisp rename to mxp/mxplon/constants.lisp index c0fde3025..8702b4cfd 100644 --- a/mxp/constants.lisp +++ b/mxp/mxplon/constants.lisp @@ -1,4 +1,4 @@ -(module mxp) +(module mxplon) (defconst CT_MAX_TRIVIAL 0 diff --git a/mxp/constraints.lisp b/mxp/mxplon/constraints.lisp similarity index 99% rename from mxp/constraints.lisp rename to mxp/mxplon/constraints.lisp index d729521c2..a7cd19ea3 100644 --- a/mxp/constraints.lisp +++ b/mxp/mxplon/constraints.lisp @@ -1,4 +1,4 @@ -(module mxp) +(module mxplon) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; diff --git a/mxp/lookups/mxp_into_instdecoder.lisp b/mxp/mxplon/lookups/mxp_into_instdecoder.lisp similarity index 63% rename from mxp/lookups/mxp_into_instdecoder.lisp rename to mxp/mxplon/lookups/mxp_into_instdecoder.lisp index 03bba01cb..f004e86e8 100644 --- a/mxp/lookups/mxp_into_instdecoder.lisp +++ b/mxp/mxplon/lookups/mxp_into_instdecoder.lisp @@ -12,13 +12,13 @@ ) ;target columns ( - mxp.INST - mxp.GWORD - mxp.GBYTE - [mxp.MXP_TYPE 1] ;; TYPE_1 in the specs - [mxp.MXP_TYPE 2] ;; TYPE_2 in the specs - [mxp.MXP_TYPE 3] ;; TYPE_3 in the specs - [mxp.MXP_TYPE 4] ;; TYPE_4 in the specs - [mxp.MXP_TYPE 5] ;; TYPE_5 in the specs + mxplon.INST + mxplon.GWORD + mxplon.GBYTE + [mxplon.MXP_TYPE 1] ;; TYPE_1 in the specs + [mxplon.MXP_TYPE 2] ;; TYPE_2 in the specs + [mxplon.MXP_TYPE 3] ;; TYPE_3 in the specs + [mxplon.MXP_TYPE 4] ;; TYPE_4 in the specs + [mxplon.MXP_TYPE 5] ;; TYPE_5 in the specs ) ) diff --git a/reftables/inst_decoder_cancun.lisp b/reftables/inst_decoder_cancun.lisp new file mode 100644 index 000000000..d369f5939 --- /dev/null +++ b/reftables/inst_decoder_cancun.lisp @@ -0,0 +1,67 @@ +(module instdecoder_cancun + (>= EVM_FORK EVM_CANCUN)) + +(defcolumns + (OPCODE :byte :display :opcode) + + ;; + ;; Family flags + ;; + (FAMILY_ADD :binary) + (FAMILY_MOD :binary) + (FAMILY_MUL :binary) + (FAMILY_EXT :binary) + (FAMILY_WCP :binary) + (FAMILY_BIN :binary) + (FAMILY_SHF :binary) + (FAMILY_KEC :binary) + (FAMILY_CONTEXT :binary) + (FAMILY_ACCOUNT :binary) + (FAMILY_COPY :binary) + (FAMILY_MCOPY :binary) + (FAMILY_TRANSACTION :binary) + (FAMILY_BATCH :binary) + (FAMILY_STACK_RAM :binary) + (FAMILY_STORAGE :binary) + (FAMILY_JUMP :binary) + (FAMILY_MACHINE_STATE :binary) + (FAMILY_PUSH_POP :binary) + (FAMILY_DUP :binary) + (FAMILY_SWAP :binary) + (FAMILY_LOG :binary) + (FAMILY_CREATE :binary) + (FAMILY_CALL :binary) + (FAMILY_HALT :binary) + (FAMILY_INVALID :binary) + (TWO_LINE_INSTRUCTION :binary) + (STATIC_FLAG :binary) + (MXP_FLAG :binary) + (FLAG_1 :binary) + (FLAG_2 :binary) + (FLAG_3 :binary) + (FLAG_4 :binary) + (ALPHA :byte) + (DELTA :byte) + (STATIC_GAS :i32) + + ;; + ;; Billing settings + ;; + (BILLING_PER_WORD :byte) + (BILLING_PER_BYTE :byte) + (IS_MSIZE :binary) + (IS_RETURN :binary) + (IS_MCOPY :binary) + (IS_FIXED_SIZE_1 :binary) + (IS_FIXED_SIZE_32 :binary) + (IS_SINGLE_MAX_OFFSET :binary) + (IS_DOUBLE_MAX_OFFSET :binary) + (IS_WORD_PRICING :binary) + (IS_BYTE_PRICING :binary) + + ;; + ;; ROM columns + ;; + (IS_PUSH :binary) + (IS_JUMPDEST :binary) + ) diff --git a/reftables/inst_decoder.lisp b/reftables/inst_decoder_lon.lisp similarity index 97% rename from reftables/inst_decoder.lisp rename to reftables/inst_decoder_lon.lisp index d5c893445..d4d8e3c1e 100644 --- a/reftables/inst_decoder.lisp +++ b/reftables/inst_decoder_lon.lisp @@ -1,4 +1,5 @@ -(module instdecoder) +(module instdecoder + (< EVM_FORK EVM_CANCUN)) (defcolumns (OPCODE :byte :display :opcode)