From 4ba562110e1687cd2f376302d87a91d002e2b1fa Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Wed, 30 Oct 2024 13:06:05 +0100 Subject: [PATCH 01/30] add HUB constraints Signed-off-by: F Bojarski --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index f5a2f78c..fff85832 100644 --- a/Makefile +++ b/Makefile @@ -135,7 +135,7 @@ ZKEVM_MODULES := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB_COLUMNS} \ + ${HUB} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ @@ -176,12 +176,12 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB_COLUMNS} \ + ${HUB} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ ${MMU} \ - ${MMIO_COLUMNS} \ + ${MMIO_COLUMNS} ${MXP} \ ${OOB} \ ${RLP_ADDR} \ From 8bd3f9409f8c587b1eb6a88ae795bd5b88568066 Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Wed, 30 Oct 2024 14:24:11 +0100 Subject: [PATCH 02/30] typo Signed-off-by: F Bojarski --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index fff85832..89c831ba 100644 --- a/Makefile +++ b/Makefile @@ -181,7 +181,7 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ ${LOG_DATA} \ ${LOG_INFO} \ ${MMU} \ - ${MMIO_COLUMNS} + ${MMIO_COLUMNS} \ ${MXP} \ ${OOB} \ ${RLP_ADDR} \ From a2234f670fc959123c942da6138009be84336016 Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Wed, 30 Oct 2024 14:47:16 +0100 Subject: [PATCH 03/30] typo Signed-off-by: F Bojarski --- Makefile | 2 +- hub/lookups/hub_into_rlp_txn.lisp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 89c831ba..33649725 100644 --- a/Makefile +++ b/Makefile @@ -181,7 +181,7 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ ${LOG_DATA} \ ${LOG_INFO} \ ${MMU} \ - ${MMIO_COLUMNS} \ + ${MMIO_COLUMNS} \ ${MXP} \ ${OOB} \ ${RLP_ADDR} \ diff --git a/hub/lookups/hub_into_rlp_txn.lisp b/hub/lookups/hub_into_rlp_txn.lisp index 63f9b500..36f20d38 100644 --- a/hub/lookups/hub_into_rlp_txn.lisp +++ b/hub/lookups/hub_into_rlp_txn.lisp @@ -37,7 +37,7 @@ (* rlptxn.ADDR_HI (hub-into-rlp-txn-tgt-selector)) (* rlptxn.ADDR_LO (hub-into-rlp-txn-tgt-selector)) (* [rlptxn.INPUT 1] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector)) - (* [rlptxn.INPUT 2] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector))) + (* [rlptxn.INPUT 2] (rlp-txn-depth-2) (hub-into-rlp-txn-tgt-selector)) ) ;; source columns ( From 837f08ef35d1205d4ba9cadaf2b656eaaecb9a4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 14:54:48 +0100 Subject: [PATCH 04/30] fix: removed stack consistency constraints --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 33649725..4bcd96a9 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,6 @@ HUB := $(wildcard hub/columns/*lisp) \ $(wildcard hub/constraints/consistency/account/*lisp) \ $(wildcard hub/constraints/consistency/context/*lisp) \ $(wildcard hub/constraints/consistency/execution_environment/*lisp) \ - $(wildcard hub/constraints/consistency/stack/*lisp) \ $(wildcard hub/constraints/consistency/storage/*lisp) \ $(wildcard hub/constraints/context-rows/*lisp) \ $(wildcard hub/constraints/generalities/*lisp) \ @@ -40,7 +39,8 @@ HUB := $(wildcard hub/columns/*lisp) \ hub/constants.lisp - # Missing from the above +# Missing from the above +# $(wildcard hub/constraints/consistency/stack/*lisp) \ ALU := $(wildcard alu/add/*.lisp) \ $(wildcard alu/ext/*.lisp) \ From 16d3740ee6d5a07df39b2c7c3d588a5cf899dbe7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 14:58:07 +0100 Subject: [PATCH 05/30] fix: make the constraints compile - removed consistency arguemnts - removed internal lookup HUB -> HUB --- Makefile | 10 +++++----- hub/lookups/{hub_into_hub.lisp => hub_into_hub.lispX} | 0 2 files changed, 5 insertions(+), 5 deletions(-) rename hub/lookups/{hub_into_hub.lisp => hub_into_hub.lispX} (100%) diff --git a/Makefile b/Makefile index 4bcd96a9..c91b4a86 100644 --- a/Makefile +++ b/Makefile @@ -4,11 +4,6 @@ HUB_COLUMNS := $(wildcard hub/columns/*lisp) HUB := $(wildcard hub/columns/*lisp) \ $(wildcard hub/constraints/account-rows/*lisp) \ - $(wildcard hub/constraints/consistency/*lisp) \ - $(wildcard hub/constraints/consistency/account/*lisp) \ - $(wildcard hub/constraints/consistency/context/*lisp) \ - $(wildcard hub/constraints/consistency/execution_environment/*lisp) \ - $(wildcard hub/constraints/consistency/storage/*lisp) \ $(wildcard hub/constraints/context-rows/*lisp) \ $(wildcard hub/constraints/generalities/*lisp) \ $(wildcard hub/constraints/heartbeat/*lisp) \ @@ -41,6 +36,11 @@ HUB := $(wildcard hub/columns/*lisp) \ # Missing from the above # $(wildcard hub/constraints/consistency/stack/*lisp) \ +# $(wildcard hub/constraints/consistency/*lisp) \ +# $(wildcard hub/constraints/consistency/account/*lisp) \ +# $(wildcard hub/constraints/consistency/context/*lisp) \ +# $(wildcard hub/constraints/consistency/execution_environment/*lisp) \ +# $(wildcard hub/constraints/consistency/storage/*lisp) \ ALU := $(wildcard alu/add/*.lisp) \ $(wildcard alu/ext/*.lisp) \ diff --git a/hub/lookups/hub_into_hub.lisp b/hub/lookups/hub_into_hub.lispX similarity index 100% rename from hub/lookups/hub_into_hub.lisp rename to hub/lookups/hub_into_hub.lispX From 182ad138448bb78338eaa9b482e0046ea42676d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 23:54:31 +0100 Subject: [PATCH 06/30] fix: context consistency constraints --- .../consistency/context/constraints.lisp | 52 ++++++++++--------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/hub/constraints/consistency/context/constraints.lisp b/hub/constraints/consistency/context/constraints.lisp index 63118268..b0ea86e9 100644 --- a/hub/constraints/consistency/context/constraints.lisp +++ b/hub/constraints/consistency/context/constraints.lisp @@ -21,31 +21,33 @@ (defconstraint context-consistency---context-data-immutability () (if-not-zero (next con_AGAIN) - (begin - ( will-remain-constant! ccp_CALL_STACK_DEPTH ) - ( will-remain-constant! ccp_IS_ROOT ) - ( will-remain-constant! ccp_IS_STATIC ) - ( will-remain-constant! ccp_ACCOUNT_ADDRESS_HI ) - ( will-remain-constant! ccp_ACCOUNT_ADDRESS_LO ) - ( will-remain-constant! ccp_ACCOUNT_DEPLOYMENT_NUMBER ) - ( will-remain-constant! ccp_BYTE_CODE_ADDRESS_HI ) - ( will-remain-constant! ccp_BYTE_CODE_ADDRESS_LO ) - ( will-remain-constant! ccp_BYTE_CODE_DEPLOYMENT_NUMBER ) - ( will-remain-constant! ccp_BYTE_CODE_DEPLOYMENT_STATUS ) - ( will-remain-constant! ccp_BYTE_CODE_CODE_FRAGMENT_INDEX ) - ( will-remain-constant! ccp_CALLER_ADDRESS_HI ) - ( will-remain-constant! ccp_CALLER_ADDRESS_LO ) - ( will-remain-constant! ccp_CALL_VALUE ) - ( will-remain-constant! ccp_CALL_DATA_CONTEXT_NUMBER ) - ( will-remain-constant! ccp_CALL_DATA_OFFSET ) - ( will-remain-constant! ccp_CALL_DATA_SIZE ) - ( will-remain-constant! ccp_RETURN_AT_OFFSET ) - ( will-remain-constant! ccp_RETURN_AT_CAPACITY )))) + (if-not-zero (next ccp_CONTEXT_NUMBER) + (begin + ( will-remain-constant! ccp_CALL_STACK_DEPTH ) + ( will-remain-constant! ccp_IS_ROOT ) + ( will-remain-constant! ccp_IS_STATIC ) + ( will-remain-constant! ccp_ACCOUNT_ADDRESS_HI ) + ( will-remain-constant! ccp_ACCOUNT_ADDRESS_LO ) + ( will-remain-constant! ccp_ACCOUNT_DEPLOYMENT_NUMBER ) + ( will-remain-constant! ccp_BYTE_CODE_ADDRESS_HI ) + ( will-remain-constant! ccp_BYTE_CODE_ADDRESS_LO ) + ( will-remain-constant! ccp_BYTE_CODE_DEPLOYMENT_NUMBER ) + ( will-remain-constant! ccp_BYTE_CODE_DEPLOYMENT_STATUS ) + ( will-remain-constant! ccp_BYTE_CODE_CODE_FRAGMENT_INDEX ) + ( will-remain-constant! ccp_CALLER_ADDRESS_HI ) + ( will-remain-constant! ccp_CALLER_ADDRESS_LO ) + ( will-remain-constant! ccp_CALL_VALUE ) + ( will-remain-constant! ccp_CALL_DATA_CONTEXT_NUMBER ) + ( will-remain-constant! ccp_CALL_DATA_OFFSET ) + ( will-remain-constant! ccp_CALL_DATA_SIZE ) + ( will-remain-constant! ccp_RETURN_AT_OFFSET ) + ( will-remain-constant! ccp_RETURN_AT_CAPACITY ))))) (defconstraint context-consistency---context-data-return-data-constancy () (if-not-zero (next con_AGAIN) - (if-zero (force-bool (next ccp_UPDATE)) - (begin - ( will-remain-constant! ccp_RETURN_DATA_CONTEXT_NUMBER ) - ( will-remain-constant! ccp_RETURN_DATA_OFFSET ) - ( will-remain-constant! ccp_RETURN_DATA_SIZE ))))) + (if-not-zero (next ccp_CONTEXT_NUMBER) + (if-zero (force-bool (next ccp_UPDATE)) + (begin + ( will-remain-constant! ccp_RETURN_DATA_CONTEXT_NUMBER ) + ( will-remain-constant! ccp_RETURN_DATA_OFFSET ) + ( will-remain-constant! ccp_RETURN_DATA_SIZE )))))) From 7e018d120b9e4e52414bbee0b49755a91bad18ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 23:58:57 +0100 Subject: [PATCH 07/30] fix: unexceptional RETURN's from message calls now always provide return data (even in the root) --- .../instruction-handling/halting/return.lisp | 20 ++++++------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/hub/constraints/instruction-handling/halting/return.lisp b/hub/constraints/instruction-handling/halting/return.lisp index e5ae9a4c..e23220e7 100644 --- a/hub/constraints/instruction-handling/halting/return.lisp +++ b/hub/constraints/instruction-handling/halting/return.lisp @@ -358,20 +358,12 @@ (defun (return-instruction---message-call-scenario) (* PEEK_AT_SCENARIO (scenario-shorthand---RETURN---message-call))) (defconstraint return-instruction---setting-the-callers-new-return-data-message-call-case (:guard (return-instruction---message-call-scenario)) - (if-not-zero (force-bin (return-instruction---is-root)) - ;; IS_ROOT = 1 - (read-context-data - ROFF_RETURN___CALLER_CONTEXT___MESSAGE_CALL ;; row offset - CONTEXT_NUMBER ;; context number - ) - ;; IS_ROOT = 0 - (provide-return-data - ROFF_RETURN___CALLER_CONTEXT___MESSAGE_CALL ;; row offset - CALLER_CONTEXT_NUMBER ;; receiver context - CONTEXT_NUMBER ;; provider context - (return-instruction---type-safe-return-data-offset) ;; (type safe) rdo - (return-instruction---type-safe-return-data-size) ;; (type safe) rds - ))) + (provide-return-data ROFF_RETURN___CALLER_CONTEXT___MESSAGE_CALL ;; row offset + CALLER_CONTEXT_NUMBER ;; receiver context + CONTEXT_NUMBER ;; provider context + (return-instruction---type-safe-return-data-offset) ;; (type safe) rdo + (return-instruction---type-safe-return-data-size) ;; (type safe) rds + )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; From b639c86a7a645475316d60e50d523f5cf954c034 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 30 Oct 2024 23:59:21 +0100 Subject: [PATCH 08/30] fix: unexceptional REVERT's now always provide return data, even in the root --- .../instruction-handling/halting/revert.lisp | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/hub/constraints/instruction-handling/halting/revert.lisp b/hub/constraints/instruction-handling/halting/revert.lisp index ca57c35a..a6bb7ecc 100644 --- a/hub/constraints/instruction-handling/halting/revert.lisp +++ b/hub/constraints/instruction-handling/halting/revert.lisp @@ -86,17 +86,12 @@ (begin (read-context-data ROFF_REVERT___NO_XAHOY_CURRENT_CONTEXT_ROW (revert-instruction---current-context)) - (if-not-zero (force-bin (revert-instruction---current-context-is-root)) - ;; current context IS root - (read-context-data ROFF_REVERT___NO_XAHOY_CALLER_CONTEXT_ROW - (revert-instruction---caller-context)) - ;; current context ISN'T root - (provide-return-data ROFF_REVERT___NO_XAHOY_CALLER_CONTEXT_ROW ;; row offset - (revert-instruction---caller-context) ;; receiver context - (revert-instruction---current-context) ;; provider context - (revert-instruction---type-safe-return-data-offset) ;; type safe rdo - (revert-instruction---type-safe-return-data-size) ;; type safe rds - ))))) + (provide-return-data ROFF_REVERT___NO_XAHOY_CALLER_CONTEXT_ROW ;; row offset + (revert-instruction---caller-context) ;; receiver context + (revert-instruction---current-context) ;; provider context + (revert-instruction---type-safe-return-data-offset) ;; type safe rdo + (revert-instruction---type-safe-return-data-size) ;; type safe rds + )))) (defun (revert-instruction---trigger_MMU) (* (- 1 XAHOY) (- 1 (revert-instruction---current-context-is-root)) From d04e219b2ec9f8ed0b6b01042efa3ec5b952c719 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 10:43:54 +0100 Subject: [PATCH 09/30] fix: splitting the "REVERT setting context" constraint in two - exceptional version - unexceptional version --- hub/constraints/instruction-handling/halting/revert.lisp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/hub/constraints/instruction-handling/halting/revert.lisp b/hub/constraints/instruction-handling/halting/revert.lisp index a6bb7ecc..a24d7088 100644 --- a/hub/constraints/instruction-handling/halting/revert.lisp +++ b/hub/constraints/instruction-handling/halting/revert.lisp @@ -78,11 +78,12 @@ (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 (:guard (revert-instruction---standard-precondition)) +(defconstraint revert-instruction---setting-the-context-rows---exceptional (:guard (revert-instruction---standard-precondition)) (if-not-zero XAHOY - ;; XAHOY ≡ 1 - (execution-provides-empty-return-data ROFF_REVERT___XAHOY_CALLER_CONTEXT_ROW) - ;; XAHOY ≡ 0 + (execution-provides-empty-return-data ROFF_REVERT___XAHOY_CALLER_CONTEXT_ROW))) + +(defconstraint revert-instruction---setting-the-context-rows---unexceptional (:guard (revert-instruction---standard-precondition)) + (if-zero XAHOY (begin (read-context-data ROFF_REVERT___NO_XAHOY_CURRENT_CONTEXT_ROW (revert-instruction---current-context)) From eb6bfecbbb1b4294db737d060202d056894dad87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 11:13:47 +0100 Subject: [PATCH 10/30] fix: simplified GAS_COST for CALLDATACOPY + split the constraint --- .../instruction-handling/copy/calldatacopy.lisp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/hub/constraints/instruction-handling/copy/calldatacopy.lisp b/hub/constraints/instruction-handling/copy/calldatacopy.lisp index 64af41aa..bcf46178 100644 --- a/hub/constraints/instruction-handling/copy/calldatacopy.lisp +++ b/hub/constraints/instruction-handling/copy/calldatacopy.lisp @@ -6,13 +6,14 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint copy-instruction---CALLDATACOPY---setting-the-gas-cost (:guard (copy-instruction---standard-CALLDATACOPY)) - (begin (if-not-zero stack/MXPX - (vanishes! GAS_COST)) - (if-not-zero stack/OOGX - (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))) - (if-zero XAHOY - (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))))) +(defconstraint copy-instruction---CALLDATACOPY---setting-the-gas-cost---MXPX-case (:guard (copy-instruction---standard-CALLDATACOPY)) + (if-not-zero stack/MXPX + (vanishes! GAS_COST))) + +(defconstraint copy-instruction---CALLDATACOPY---setting-the-gas-cost---no-MXPX-case (:guard (copy-instruction---standard-CALLDATACOPY)) + (if-zero stack/MXPX + (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))) + (defconstraint copy-instruction---CALLDATACOPY---setting-context-row---exceptional-case (:guard (copy-instruction---standard-CALLDATACOPY)) (if-not-zero XAHOY From b3790cf8f4c146ad719619428c0730b3fd54013f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 11:16:04 +0100 Subject: [PATCH 11/30] fix: split GAS_COST for RETURNDATACOPY into SANS/WITH_COMPUTATION cases --- .../instruction-handling/copy/returndatacopy.lisp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/hub/constraints/instruction-handling/copy/returndatacopy.lisp b/hub/constraints/instruction-handling/copy/returndatacopy.lisp index b720eae2..de12c52b 100644 --- a/hub/constraints/instruction-handling/copy/returndatacopy.lisp +++ b/hub/constraints/instruction-handling/copy/returndatacopy.lisp @@ -6,10 +6,13 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint copy-instruction---RETURNDATACOPY---setting-the-gas-cost (:guard (copy-instruction---standard-RETURNDATACOPY)) +(defconstraint copy-instruction---RETURNDATACOPY---setting-the-gas-cost---sans-computation (:guard (copy-instruction---standard-RETURNDATACOPY)) (begin (if-not-zero stack/RDCX (vanishes! GAS_COST)) - (if-not-zero stack/MXPX (vanishes! GAS_COST)) + (if-not-zero stack/MXPX (vanishes! GAS_COST)))) + +(defconstraint copy-instruction---RETURNDATACOPY---setting-the-gas-cost---with-computation (:guard (copy-instruction---standard-RETURNDATACOPY)) + (begin (if-not-zero stack/OOGX (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))) (if-zero XAHOY (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))))) From e3d7047b478e017fc71854229d0d289f41779bfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 11:53:05 +0100 Subject: [PATCH 12/30] fix: splitting GAS_COST for CODECOPY --- .../instruction-handling/copy/codecopy.lisp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/hub/constraints/instruction-handling/copy/codecopy.lisp b/hub/constraints/instruction-handling/copy/codecopy.lisp index 5529b274..755451c7 100644 --- a/hub/constraints/instruction-handling/copy/codecopy.lisp +++ b/hub/constraints/instruction-handling/copy/codecopy.lisp @@ -6,14 +6,13 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint copy-instruction---CODECOPY---setting-the-gas-cost +(defconstraint copy-instruction---CODECOPY---setting-the-gas-cost---MXPX-case (:guard (copy-instruction---standard-CODECOPY)) - (begin (if-not-zero stack/MXPX - (vanishes! GAS_COST)) - (if-not-zero stack/OOGX - (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))) - (if-zero XAHOY - (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas)))))) + (if-not-zero stack/MXPX (vanishes! GAS_COST))) + +(defconstraint copy-instruction---CODECOPY---setting-the-gas-cost---no-MXPX-case + (:guard (copy-instruction---standard-CODECOPY)) + (if-zero stack/MXPX (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas))))) (defconstraint copy-instruction---CODECOPY---setting-the-context-row---exceptional-case (:guard (copy-instruction---standard-CODECOPY)) From 0f5f5525009fb0dec60b6e7c6e85d9f6ac698355 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 11:53:22 +0100 Subject: [PATCH 13/30] fix: spliting GAS_COST for EXTCODECOPY --- .../instruction-handling/copy/extcodecopy.lisp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/hub/constraints/instruction-handling/copy/extcodecopy.lisp b/hub/constraints/instruction-handling/copy/extcodecopy.lisp index 8fc53d7d..61ddff87 100644 --- a/hub/constraints/instruction-handling/copy/extcodecopy.lisp +++ b/hub/constraints/instruction-handling/copy/extcodecopy.lisp @@ -6,11 +6,12 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint copy-instruction---EXTCODECOPY---setting-the-gas-cost (:guard (copy-instruction---standard-EXTCODECOPY)) +(defconstraint copy-instruction---EXTCODECOPY---setting-the-gas-cost---MXPX-case (:guard (copy-instruction---standard-EXTCODECOPY)) (if-not-zero stack/MXPX - ;; MXPX ≡ 1 - (vanishes! GAS_COST) - ;; MXPX ≡ 0 + (vanishes! GAS_COST))) + +(defconstraint copy-instruction---EXTCODECOPY---setting-the-gas-cost---no-MXPX-case (:guard (copy-instruction---standard-EXTCODECOPY)) + (if-zero stack/MXPX (eq! GAS_COST (+ stack/STATIC_GAS (copy-instruction---MXP-memory-expansion-gas) From 1eb747f79efbeef16832d62c5958a2dabf21ec6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 13:51:39 +0100 Subject: [PATCH 14/30] fix: debug constraint had issue --- hub/constraints/generalities/auxiliary_stamps.lisp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/hub/constraints/generalities/auxiliary_stamps.lisp b/hub/constraints/generalities/auxiliary_stamps.lisp index 33918bd4..06ed7e8e 100644 --- a/hub/constraints/generalities/auxiliary_stamps.lisp +++ b/hub/constraints/generalities/auxiliary_stamps.lisp @@ -43,9 +43,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint generalities---auxiliary-stamps---LOG_INFO_STAMP-increments () - (begin (debug (any! (remained-constant! LOG_INFO_STAMP) (did-inc! LOG_INFO_STAMP))) - (if-not-zero (remained-constant! HUB_STAMP) - (did-inc! LOG_INFO_STAMP (* PEEK_AT_STACK stack/LOG_INFO_FLAG))))) + (begin + (debug (any! (remained-constant! LOG_INFO_STAMP) (did-inc! LOG_INFO_STAMP 1))) + (if-not-zero (remained-constant! HUB_STAMP) + (did-inc! LOG_INFO_STAMP (* PEEK_AT_STACK stack/LOG_INFO_FLAG))))) (defconstraint generalities---auxiliary-stamps---necessary-conditions-for-LOG_INFO_FLAG-to-be-on (:perspective stack) (begin (debug (is-binary LOG_INFO_FLAG)) From 96f7c562fe14ebca39370d5ecac66695083dce59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 15:32:49 +0100 Subject: [PATCH 15/30] fix: TXN instruction family now uses is_ORIGIN and is_GASPRICE flags --- hub/constraints/instruction-handling/txn.lisp | 52 ++++++++++++------- 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/hub/constraints/instruction-handling/txn.lisp b/hub/constraints/instruction-handling/txn.lisp index bac5b3ed..efdfd5ea 100644 --- a/hub/constraints/instruction-handling/txn.lisp +++ b/hub/constraints/instruction-handling/txn.lisp @@ -1,26 +1,40 @@ (module hub) -(defun (txn-no-stack-exceptions) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (* PEEK_AT_STACK stack/TXN_FLAG (- 1 stack/SUX stack/SOX))) +(defun (txn-instruction---standard-precondition) (* PEEK_AT_STACK stack/TXN_FLAG (- 1 stack/SUX stack/SOX))) +(defun (txn-instruction---is-ORIGIN) [ stack/DEC_FLAG 1 ]) +(defun (txn-instruction---is-GASPRICE) [ stack/DEC_FLAG 2 ]) +(defun (txn-instruction---result-hi) [ stack/STACK_ITEM_VALUE_HI 4 ]) +(defun (txn-instruction---result-lo) [ stack/STACK_ITEM_VALUE_LO 4 ]) ;; "" -(defconstraint txn-stack-pattern (:guard (txn-no-stack-exceptions)) - (stack-pattern-0-1)) +(defconst + roff---txn-instruction---transaction-row 1 + roff---txn-instruction---exceptional-context-row 2 + ) -(defconstraint txn-setting-NSR (:guard (txn-no-stack-exceptions)) - (eq! NSR (+ 1 CMC))) +(defconstraint txn-instruction---setting-the-stack-pattern + (:guard (txn-instruction---standard-precondition)) + (stack-pattern-0-1)) -(defconstraint txn-setting-peeking-flags (:guard (txn-no-stack-exceptions)) - (eq! (+ (shift PEEK_AT_TRANSACTION 1) - (* (shift PEEK_AT_CONTEXT 2) CMC)) - NSR)) +(defconstraint txn-instruction---setting-NSR + (:guard (txn-instruction---standard-precondition)) + (eq! NSR (+ 1 CMC))) -(defconstraint txn-setting-gas-cost (:guard (txn-no-stack-exceptions)) - (eq! GAS_COST stack/STATIC_GAS)) +(defconstraint txn-instruction---setting-the-peeking-flags + (:guard (txn-instruction---standard-precondition)) + (eq! NSR + (+ (shift PEEK_AT_TRANSACTION roff---txn-instruction---transaction-row) + (* (shift PEEK_AT_CONTEXT roff---txn-instruction---exceptional-context-row) CMC)))) -(defconstraint txn-setting-stack-values (:guard (txn-no-stack-exceptions)) - (if-zero (force-bin [stack/DEC_FLAG 1]) - (begin (eq! [stack/STACK_ITEM_VALUE_HI 4] (next transaction/FROM_ADDRESS_HI)) - (eq! [stack/STACK_ITEM_VALUE_LO 4] (next transaction/FROM_ADDRESS_LO))) - (begin (vanishes! [stack/STACK_ITEM_VALUE_HI 4]) - (eq! [stack/STACK_ITEM_VALUE_LO 4] (next transaction/GAS_PRICE))))) +(defconstraint txn-instruction---setting-the-gas-cost + (:guard (txn-instruction---standard-precondition)) + (eq! GAS_COST stack/STATIC_GAS)) + +(defconstraint txn-instruction---setting-the-result + (:guard (txn-instruction---standard-precondition)) + (begin + (if-not-zero (txn-instruction---is-ORIGIN) + (begin (eq! (txn-instruction---result-hi) (shift transaction/FROM_ADDRESS_HI roff---txn-instruction---transaction-row)) + (eq! (txn-instruction---result-lo) (shift transaction/FROM_ADDRESS_LO roff---txn-instruction---transaction-row)))) + (if-not-zero (txn-instruction---is-GASPRICE) + (begin (eq! (txn-instruction---result-hi) 0) + (eq! (txn-instruction---result-lo) (shift transaction/GAS_PRICE roff---txn-instruction---transaction-row)))))) From b6464f6258a9cdfdfcd2cd6e3f10a6ea7098ce41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 16:15:58 +0100 Subject: [PATCH 16/30] ras --- hub/constraints/instruction-handling/txn.lisp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hub/constraints/instruction-handling/txn.lisp b/hub/constraints/instruction-handling/txn.lisp index efdfd5ea..7342c740 100644 --- a/hub/constraints/instruction-handling/txn.lisp +++ b/hub/constraints/instruction-handling/txn.lisp @@ -22,8 +22,8 @@ (defconstraint txn-instruction---setting-the-peeking-flags (:guard (txn-instruction---standard-precondition)) (eq! NSR - (+ (shift PEEK_AT_TRANSACTION roff---txn-instruction---transaction-row) - (* (shift PEEK_AT_CONTEXT roff---txn-instruction---exceptional-context-row) CMC)))) + (+ (shift PEEK_AT_TRANSACTION roff---txn-instruction---transaction-row) + (* (shift PEEK_AT_CONTEXT roff---txn-instruction---exceptional-context-row) CMC)))) (defconstraint txn-instruction---setting-the-gas-cost (:guard (txn-instruction---standard-precondition)) From dc16d76370aa93aa804b68c1a8b471da6852302b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 16:50:25 +0100 Subject: [PATCH 17/30] fix: mix up in SLOAD/SSTORE flags fixed storage-instruction---setting-storage-slot-values --- hub/constraints/instruction-handling/sto.lisp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hub/constraints/instruction-handling/sto.lisp b/hub/constraints/instruction-handling/sto.lisp index 401d72e7..ab4b2021 100644 --- a/hub/constraints/instruction-handling/sto.lisp +++ b/hub/constraints/instruction-handling/sto.lisp @@ -113,12 +113,12 @@ (defconstraint storage-instruction---setting-storage-slot-values (:guard (storage-instruction---no-stack-exceptions)) (if-not-zero (oogx-or-no-exception) (begin - (if-not-zero (force-bin (storage-instruction---is-SSTORE)) + (if-not-zero (force-bin (storage-instruction---is-SLOAD)) (begin (storage-reading 3) (eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3)) (eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3)))) - (if-not-zero (force-bin (storage-instruction---is-SLOAD)) + (if-not-zero (force-bin (storage-instruction---is-SSTORE)) (begin (eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3)) (eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3)))) From 13996250a6e3fcc3ffe0a094aa4625af9d88a894 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 16:57:38 +0100 Subject: [PATCH 18/30] ras: splitting up the storage-instruction's "setting-values" into 3 - for SSTORE - for SLOAD - undoing row for either --- hub/constraints/instruction-handling/sto.lisp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/hub/constraints/instruction-handling/sto.lisp b/hub/constraints/instruction-handling/sto.lisp index ab4b2021..1667e823 100644 --- a/hub/constraints/instruction-handling/sto.lisp +++ b/hub/constraints/instruction-handling/sto.lisp @@ -110,24 +110,29 @@ (DOM-SUB-stamps---standard 3 ;; kappa 0)))) ;; c -(defconstraint storage-instruction---setting-storage-slot-values (:guard (storage-instruction---no-stack-exceptions)) +(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SLOAD (:guard (storage-instruction---no-stack-exceptions)) (if-not-zero (oogx-or-no-exception) - (begin (if-not-zero (force-bin (storage-instruction---is-SLOAD)) (begin (storage-reading 3) (eq! (storage-instruction---loaded-value-hi) (shift storage/VALUE_CURR_HI 3)) - (eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3)))) + (eq! (storage-instruction---loaded-value-lo) (shift storage/VALUE_CURR_LO 3)))))) + +(defconstraint storage-instruction---setting-storage-slot-values---doing-for-SSTORE (:guard (storage-instruction---no-stack-exceptions)) + (if-not-zero (oogx-or-no-exception) (if-not-zero (force-bin (storage-instruction---is-SSTORE)) (begin (eq! (storage-instruction---value-to-store-hi) (shift storage/VALUE_NEXT_HI 3)) - (eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3)))) + (eq! (storage-instruction---value-to-store-lo) (shift storage/VALUE_NEXT_LO 3)))))) + +(defconstraint storage-instruction---setting-storage-slot-values---undoing-storage-operation (:guard (storage-instruction---no-stack-exceptions)) + (if-not-zero (oogx-or-no-exception) (if-not-zero CONTEXT_WILL_REVERT (begin (storage-same-slot 4) (undo-storage-warmth-and-value-update 4) - (DOM-SUB-stamps---revert-with-current 4 ;; kappa - 0)))))) ;; c + (DOM-SUB-stamps---revert-with-current 4 ;; kappa + 0))))) ;; c (defun (orig-is-zero) (shift storage/VALUE_ORIG_IS_ZERO 3)) (defun (curr-is-zero) (shift storage/VALUE_CURR_IS_ZERO 3)) From b58578ef7d51008fe3bbad1a616d1236f08264f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 31 Oct 2024 19:38:44 +0100 Subject: [PATCH 19/30] ras: formatting + removed empty file --- hub/columns/account.lisp | 70 ++++++++++++++++++------------------ hub/columns/consistency.lisp | 7 ---- hub/columns/storage.lisp | 4 --- 3 files changed, 35 insertions(+), 46 deletions(-) delete mode 100644 hub/columns/consistency.lisp diff --git a/hub/columns/account.lisp b/hub/columns/account.lisp index 3df7b589..cd1e0a14 100644 --- a/hub/columns/account.lisp +++ b/hub/columns/account.lisp @@ -6,34 +6,34 @@ PEEK_AT_ACCOUNT ;; account-row columns - ((ADDRESS_HI :i32) ;; 4 bytes - (ADDRESS_LO :i128) - (NONCE :i64) - (NONCE_NEW :i64) - (BALANCE :i128) - (BALANCE_NEW :i128) - (CODE_SIZE :i32) - (CODE_SIZE_NEW :i32) - (CODE_HASH_HI :i128) - (CODE_HASH_LO :i128) - (CODE_HASH_HI_NEW :i128) - (CODE_HASH_LO_NEW :i128) - (HAS_CODE :binary@prove) ;; TODO: demote to debug constraint - (HAS_CODE_NEW :binary@prove) ;; TODO: demote to debug constraint - (CODE_FRAGMENT_INDEX :i32) - (ROMLEX_FLAG :binary@prove) - (EXISTS :binary@prove) ;; TODO: demote to debug constraint, already fully constrained - (EXISTS_NEW :binary@prove) ;; TODO: demote to debug constraint, already fully constrained - (WARMTH :binary@prove) ;; TODO: demote to debug constraint - (WARMTH_NEW :binary@prove) ;; TODO: demote to debug constraint - (MARKED_FOR_SELFDESTRUCT :binary@prove) ;; TODO: demote to debug constraint + ((ADDRESS_HI :i32) ;; 4 bytes + (ADDRESS_LO :i128) + (NONCE :i64 :display :dec) + (NONCE_NEW :i64 :display :dec) + (BALANCE :i128 :display :dec) + (BALANCE_NEW :i128 :display :dec) + (CODE_SIZE :i32 :display :dec) + (CODE_SIZE_NEW :i32 :display :dec) + (CODE_HASH_HI :i128) + (CODE_HASH_LO :i128) + (CODE_HASH_HI_NEW :i128) + (CODE_HASH_LO_NEW :i128) + (HAS_CODE :binary@prove) ;; TODO: demote to debug constraint + (HAS_CODE_NEW :binary@prove) ;; TODO: demote to debug constraint + (CODE_FRAGMENT_INDEX :i32 :display :dec) + (ROMLEX_FLAG :binary@prove) + (EXISTS :binary@prove) ;; TODO: demote to debug constraint, already fully constrained + (EXISTS_NEW :binary@prove) ;; TODO: demote to debug constraint, already fully constrained + (WARMTH :binary@prove) ;; TODO: demote to debug constraint + (WARMTH_NEW :binary@prove) ;; TODO: demote to debug constraint + (MARKED_FOR_SELFDESTRUCT :binary@prove) ;; TODO: demote to debug constraint (MARKED_FOR_SELFDESTRUCT_NEW :binary@prove) ;; TODO: demote to debug constraint - (DEPLOYMENT_NUMBER :i32) - (DEPLOYMENT_NUMBER_NEW :i32) - (DEPLOYMENT_NUMBER_INFTY :i32) - (DEPLOYMENT_STATUS :binary@prove) ;; TODO: demote to debug constraint - (DEPLOYMENT_STATUS_NEW :binary@prove) ;; TODO: demote to debug constraint - (DEPLOYMENT_STATUS_INFTY :binary@prove) ;; TODO: demote to debug constraint + (DEPLOYMENT_NUMBER :i32 :display :dec) + (DEPLOYMENT_NUMBER_NEW :i32 :display :dec) + (DEPLOYMENT_NUMBER_INFTY :i32 :display :dec) + (DEPLOYMENT_STATUS :binary@prove) ;; TODO: demote to debug constraint + (DEPLOYMENT_STATUS_NEW :binary@prove) ;; TODO: demote to debug constraint + (DEPLOYMENT_STATUS_INFTY :binary@prove) ;; TODO: demote to debug constraint ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -41,8 +41,8 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (TRM_FLAG :binary@prove) - (IS_PRECOMPILE :binary@prove) ;; TODO: demote to debug constraint + (TRM_FLAG :binary@prove) + (IS_PRECOMPILE :binary@prove) ;; TODO: demote to debug constraint (TRM_RAW_ADDRESS_HI :i128) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -51,14 +51,14 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (RLPADDR_FLAG :binary@prove) - (RLPADDR_RECIPE :i8) + (RLPADDR_FLAG :binary@prove) + (RLPADDR_RECIPE :i8) (RLPADDR_DEP_ADDR_HI :i32) (RLPADDR_DEP_ADDR_LO :i128) - (RLPADDR_SALT_HI :i128) - (RLPADDR_SALT_LO :i128) - (RLPADDR_KEC_HI :i128) - (RLPADDR_KEC_LO :i128) + (RLPADDR_SALT_HI :i128) + (RLPADDR_SALT_LO :i128) + (RLPADDR_KEC_HI :i128) + (RLPADDR_KEC_LO :i128) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; diff --git a/hub/columns/consistency.lisp b/hub/columns/consistency.lisp deleted file mode 100644 index 48e14390..00000000 --- a/hub/columns/consistency.lisp +++ /dev/null @@ -1,7 +0,0 @@ -(module hub) - -;; extra columns can be found in the relevant consistency//columns.lisp file -;; -;; columns for account, context and storage perspectives consistency -;; arguments will be merged into a single se of 9 columns in a future -;; update (perspective aware lexicographic ordering arguments PR.) diff --git a/hub/columns/storage.lisp b/hub/columns/storage.lisp index 15b3af81..f6ed29d8 100644 --- a/hub/columns/storage.lisp +++ b/hub/columns/storage.lisp @@ -31,10 +31,6 @@ ( VALUE_NEXT_IS_ORIG :binary ) ( VALUE_CURR_CHANGES :binary ) - ;; not yet in the spec - ( UNCONSTRAINED_FIRST :binary ) - ( UNCONSTRAINED_FINAL :binary ) - ;; storage consistency permutation related ( FIRST_IN_CNF :binary@prove ) ( FIRST_IN_BLK :binary@prove ) ( FIRST_IN_TXN :binary@prove ) ( AGAIN_IN_CNF :binary@prove ) ( AGAIN_IN_BLK :binary@prove ) ( AGAIN_IN_TXN :binary@prove ) From 409aa9871371db1d86a76e0d00fd170a1c167df2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 15:21:46 +0100 Subject: [PATCH 20/30] ras splitting of hub/generalities constraint split generalities---setting-CMC-and-XAHOY into 3 --- hub/constraints/generalities/context.lisp | 24 +++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/hub/constraints/generalities/context.lisp b/hub/constraints/generalities/context.lisp index 88c4a61a..9458b15f 100644 --- a/hub/constraints/generalities/context.lisp +++ b/hub/constraints/generalities/context.lisp @@ -32,14 +32,22 @@ stack/CREATE_FLAG stack/HALT_FLAG)) -(defconstraint generalities---setting-CMC-and-XAHOY () - (begin (hub-stamp-constancy (cmc_and_xahoy_weighted_sum)) ;; this settles hub-stamp-constancy for CMC and XAHOY simultaneously - (if-zero TX_EXEC (vanishes! (cmc_and_xahoy_weighted_sum))) ;; this forces the vanishing of CMC and XAHOY outside of execution rows - (if-not-zero PEEK_AT_STACK - (begin (eq! (exception_flag_sum) XAHOY) - (if-zero (cmc_sum) - (eq! CMC 0) - (eq! CMC 1)))))) +(defconstraint generalities---setting-CMC-and-XAHOY---stamp-constancies () + ;; this settles hub-stamp-constancy for CMC and XAHOY simultaneously + (hub-stamp-constancy (cmc_and_xahoy_weighted_sum))) + +(defconstraint generalities---setting-CMC-and-XAHOY---automatic-vanishing () + ;; this forces the vanishing of CMC and XAHOY outside of execution rows + (if-zero TX_EXEC + (vanishes! (cmc_and_xahoy_weighted_sum)))) + +(defconstraint generalities---setting-CMC-and-XAHOY---nontrivial-values () + ;; nontrivial values for CMC and XAHOY + (if-not-zero PEEK_AT_STACK + (begin (eq! (exception_flag_sum) XAHOY) + (if-zero (cmc_sum) + (eq! CMC 0) + (eq! CMC 1))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; From 91b79e9b66a7e4fe2d67d0e01e1098bcda684921 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 15:22:06 +0100 Subject: [PATCH 21/30] fix: some renaming of jump instruction constriants --- .../instruction-handling/jump.lisp | 29 ++++++++++--------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/hub/constraints/instruction-handling/jump.lisp b/hub/constraints/instruction-handling/jump.lisp index bbfc10ec..0f3968da 100644 --- a/hub/constraints/instruction-handling/jump.lisp +++ b/hub/constraints/instruction-handling/jump.lisp @@ -36,8 +36,8 @@ (defun (jump-instruction---new-pc-lo) [ stack/STACK_ITEM_VALUE_LO 1 ]) (defun (jump-instruction---jump-condition-hi) [ stack/STACK_ITEM_VALUE_HI 2 ]) (defun (jump-instruction---jump-condition-lo) [ stack/STACK_ITEM_VALUE_LO 2 ]) -(defun (jump-instruction---is-jump) [ stack/DEC_FLAG 1 ]) -(defun (jump-instruction---is-jumpi) [ stack/DEC_FLAG 2 ]) +(defun (jump-instruction---is-JUMP) [ stack/DEC_FLAG 1 ]) +(defun (jump-instruction---is-JUMPI) [ stack/DEC_FLAG 2 ]) ;; (defun (jump-instruction---code-address-hi) (shift context/BYTE_CODE_ADDRESS_HI ROW_OFFSET_FOR_JUMP_NO_OOGX_CURRENT_CONTEXT_ROW)) (defun (jump-instruction---code-address-lo) (shift context/BYTE_CODE_ADDRESS_LO ROW_OFFSET_FOR_JUMP_NO_OOGX_CURRENT_CONTEXT_ROW)) @@ -49,12 +49,12 @@ ;; (defun (jump-instruction---JUMPI-jump-not-attempted) (shift [ misc/OOB_DATA 6 ] ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW)) (defun (jump-instruction---JUMPI-guaranteed-exception) (shift [ misc/OOB_DATA 7 ] ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW)) -(defun (jump-instruction---JUMPI-must-be-attempted) (shift [ misc/OOB_DATA 8 ] ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW)) +(defun (jump-instruction---JUMPI-must-be-attempted) (shift [ misc/OOB_DATA 8 ] ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW)) ;; "" (defconstraint jump-instruction---setting-the-stack-pattern (:guard (jump-instruction---no-stack-exception)) (begin - (if-not-zero (jump-instruction---is-jump) (stack-pattern-1-0)) - (if-not-zero (jump-instruction---is-jumpi) (stack-pattern-2-0)))) + (if-not-zero (jump-instruction---is-JUMP) (stack-pattern-1-0)) + (if-not-zero (jump-instruction---is-JUMPI) (stack-pattern-2-0)))) ;; TODO: allow for debug only constraints ;; TODO: remove ugly hack @@ -109,27 +109,28 @@ (DOM-SUB-stamps---standard ROW_OFFSET_FOR_JUMP_NO_OOGX_ADDRESS_ROW 0))) -(defconstraint jump-instruction---the-miscellaneous-row-flags (:guard (jump-instruction---no-stack-exception-and-no-oogx)) +(defconstraint jump-instruction---miscellaneous-row---setting-the-module-flags (:guard (jump-instruction---no-stack-exception-and-no-oogx)) (eq! (weighted-MISC-flag-sum ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW) MISC_WEIGHT_OOB)) -(defconstraint jump-instruction---the-miscellaneous-row-OOB-instruction (:guard (jump-instruction---no-stack-exception-and-no-oogx)) - (begin - (if-not-zero (jump-instruction---is-jump) +(defconstraint jump-instruction---miscellaneous-row---setting-the-OOB-instruction---JUMP-case (:guard (jump-instruction---no-stack-exception-and-no-oogx)) + (if-not-zero (jump-instruction---is-JUMP) (set-OOB-instruction---jump ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW (jump-instruction---new-pc-hi) (jump-instruction---new-pc-lo) - (jump-instruction---code-size))) - (if-not-zero (jump-instruction---is-jumpi) + (jump-instruction---code-size)))) + +(defconstraint jump-instruction---miscellaneous-row---setting-the-OOB-instruction---JUMPI-case (:guard (jump-instruction---no-stack-exception-and-no-oogx)) + (if-not-zero (jump-instruction---is-JUMPI) (set-OOB-instruction---jumpi ROW_OFFSET_FOR_JUMP_NO_OOGX_MISC_ROW (jump-instruction---new-pc-hi) (jump-instruction---new-pc-lo) (jump-instruction---jump-condition-hi) (jump-instruction---jump-condition-lo) - (jump-instruction---code-size))))) + (jump-instruction---code-size)))) (defconstraint jump-instruction---setting-PC_NEW-and-JUMP_DESTINATION_VETTING-for-JUMP (:guard (jump-instruction---no-stack-exception-and-no-oogx)) - (if-not-zero (jump-instruction---is-jump) + (if-not-zero (jump-instruction---is-JUMP) (begin (if-not-zero (jump-instruction---JUMP-guaranteed-exception) (begin (eq! stack/JUMP_DESTINATION_VETTING_REQUIRED 0) @@ -140,7 +141,7 @@ (defconstraint jump-instruction---setting-PC_NEW-and-JUMP_DESTINATION_VETTING-for-JUMPI (:guard (jump-instruction---no-stack-exception-and-no-oogx)) - (if-not-zero (jump-instruction---is-jumpi) + (if-not-zero (jump-instruction---is-JUMPI) (begin (if-not-zero (jump-instruction---JUMPI-jump-not-attempted) (begin (eq! stack/JUMP_DESTINATION_VETTING_REQUIRED 0) From 74d9408783d9b57eaff7c5ee2265af85b86de2ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 17:03:28 +0100 Subject: [PATCH 22/30] fix: splitting the MACHINE_STATE's "setting-stack-value" constraint in 3 --- .../instruction-handling/machine_state.lisp | 29 ++++++++++++++----- 1 file changed, 22 insertions(+), 7 deletions(-) diff --git a/hub/constraints/instruction-handling/machine_state.lisp b/hub/constraints/instruction-handling/machine_state.lisp index efd74686..190eb0ec 100644 --- a/hub/constraints/instruction-handling/machine_state.lisp +++ b/hub/constraints/instruction-handling/machine_state.lisp @@ -68,13 +68,28 @@ (eq! (weighted-MISC-flag-sum ROFF_MACHINESTATE___MSIZE___MISC_ROW) MISC_WEIGHT_MXP) (set-MXP-instruction-type-1 ROFF_MACHINESTATE___MSIZE___MISC_ROW)))) -(defconstraint machine-state-instruction---setting-gas-cost (:guard (machine-state-instruction---no-stack-exception)) +(defconstraint machine-state-instruction---setting-gas-cost + (:guard (machine-state-instruction---no-stack-exception)) (eq! GAS_COST stack/STATIC_GAS)) -(defconstraint machine-state-instruction---setting-stack-value (:guard (machine-state-instruction---no-stack-exception)) +(defconstraint machine-state-instruction---all-instructions-produce-zero-high-part + (:guard (machine-state-instruction---no-stack-exception)) + (vanishes! (machine-state-instruction---result-hi))) + +(defconstraint machine-state-instruction---setting-stack-value---PC-case + (:guard (machine-state-instruction---no-stack-exception)) + (if-zero XAHOY + (if-not-zero (machine-state-instruction---is-PC) + (eq! (machine-state-instruction---result-lo) PROGRAM_COUNTER)))) + +(defconstraint machine-state-instruction---setting-stack-value---MSIZE-case + (:guard (machine-state-instruction---no-stack-exception)) + (if-zero XAHOY + (if-not-zero (machine-state-instruction---is-MSIZE) + (eq! (machine-state-instruction---result-lo) (shift misc/MXP_WORDS ROFF_MACHINESTATE___MSIZE___MISC_ROW))))) + +(defconstraint machine-state-instruction---setting-stack-value---GAS-case + (:guard (machine-state-instruction---no-stack-exception)) (if-zero XAHOY - (begin - (vanishes! (machine-state-instruction---result-hi)) - (if-not-zero (machine-state-instruction---is-PC) (eq! (machine-state-instruction---result-lo) PROGRAM_COUNTER)) - (if-not-zero (machine-state-instruction---is-MSIZE) (eq! (machine-state-instruction---result-lo) (shift misc/MXP_WORDS ROFF_MACHINESTATE___MSIZE___MISC_ROW))) - (if-not-zero (machine-state-instruction---is-GAS) (eq! (machine-state-instruction---result-lo) GAS_NEXT))))) + (if-not-zero (machine-state-instruction---is-GAS) + (eq! (machine-state-instruction---result-lo) GAS_NEXT)))) From 171c6446513c05a722a52b3582a0786245e4c95d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 17:07:16 +0100 Subject: [PATCH 23/30] fix: remain faithful to spec the spec only requires the high part to vanish if the instruction is unexceptional (though it doesn't really matter.) --- hub/constraints/instruction-handling/machine_state.lisp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/hub/constraints/instruction-handling/machine_state.lisp b/hub/constraints/instruction-handling/machine_state.lisp index 190eb0ec..860b6fa1 100644 --- a/hub/constraints/instruction-handling/machine_state.lisp +++ b/hub/constraints/instruction-handling/machine_state.lisp @@ -74,7 +74,8 @@ (defconstraint machine-state-instruction---all-instructions-produce-zero-high-part (:guard (machine-state-instruction---no-stack-exception)) - (vanishes! (machine-state-instruction---result-hi))) + (if-zero XAHOY + (vanishes! (machine-state-instruction---result-hi)))) (defconstraint machine-state-instruction---setting-stack-value---PC-case (:guard (machine-state-instruction---no-stack-exception)) From 4ee0ff85ee6380f96ee55548779ccb18e5008828 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 17:31:21 +0100 Subject: [PATCH 24/30] fix: implemented the correct formula for MSIZE --- hub/constraints/instruction-handling/machine_state.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hub/constraints/instruction-handling/machine_state.lisp b/hub/constraints/instruction-handling/machine_state.lisp index 860b6fa1..2075c44f 100644 --- a/hub/constraints/instruction-handling/machine_state.lisp +++ b/hub/constraints/instruction-handling/machine_state.lisp @@ -87,7 +87,7 @@ (:guard (machine-state-instruction---no-stack-exception)) (if-zero XAHOY (if-not-zero (machine-state-instruction---is-MSIZE) - (eq! (machine-state-instruction---result-lo) (shift misc/MXP_WORDS ROFF_MACHINESTATE___MSIZE___MISC_ROW))))) + (eq! (machine-state-instruction---result-lo) (shift (* misc/MXP_WORDS WORD_SIZE) ROFF_MACHINESTATE___MSIZE___MISC_ROW))))) (defconstraint machine-state-instruction---setting-stack-value---GAS-case (:guard (machine-state-instruction---no-stack-exception)) From fb233c7ddf90167e49d2fa6e4e9efab5259e468b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 1 Nov 2024 20:00:29 +0100 Subject: [PATCH 25/30] fix: create stack pattern STACK_STAMP typo for CREATE2's + renaming renaming: MULTIPLIER___STACK_HEIGHT -> MULTIPLIER___STACK_STAMP which correctly reflects its purpose --- hub/constants.lisp | 2 +- hub/constraints/stack_patterns.lisp | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/hub/constants.lisp b/hub/constants.lisp index f131c5d2..abde5ff9 100644 --- a/hub/constants.lisp +++ b/hub/constants.lisp @@ -1,7 +1,7 @@ (module hub) (defconst - MULTIPLIER___STACK_HEIGHT 8 ;; \hubTau + MULTIPLIER___STACK_STAMP 8 ;; \hubTau MULTIPLIER___DOM_SUB_STAMPS 8 ;; \hubLambda DOM_SUB_STAMP_OFFSET___REVERT 6 ;; \revertEpsilon DOM_SUB_STAMP_OFFSET___SELFDESTRUCT 7 ;; \selfdestructEpsilon diff --git a/hub/constraints/stack_patterns.lisp b/hub/constraints/stack_patterns.lisp index 66d74a4f..2bfa89eb 100644 --- a/hub/constraints/stack_patterns.lisp +++ b/hub/constraints/stack_patterns.lisp @@ -33,14 +33,14 @@ (vanishes! [ stack/STACK_ITEM_STAMP k ]))) ;; current row -(defun (set-frst-row-stack-item-stamp k offset ) (= [ stack/STACK_ITEM_STAMP k ] (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) offset) )) +(defun (set-frst-row-stack-item-stamp k offset ) (= [ stack/STACK_ITEM_STAMP k ] (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) offset) )) (defun (pop-frst-row-stack-item k ) (= [ stack/STACK_ITEM_POP k ] 1 )) (defun (push-frst-row-stack-item k ) (= [ stack/STACK_ITEM_POP k ] 0 )) (defun (inc-frst-row-stack-item-X-height-by-Y k increment) (= [ stack/STACK_ITEM_HEIGHT k ] (+ HEIGHT increment) )) (defun (dec-frst-row-stack-item-X-height-by-Y k decrement) (= [ stack/STACK_ITEM_HEIGHT k ] (- HEIGHT decrement) )) ;; next row -(defun (set-scnd-row-stack-item-stamp k offset ) (= (next [ stack/STACK_ITEM_STAMP k ]) (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) offset) )) +(defun (set-scnd-row-stack-item-stamp k offset ) (= (next [ stack/STACK_ITEM_STAMP k ]) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) offset) )) (defun (pop-scnd-row-stack-item k ) (= (next [ stack/STACK_ITEM_POP k ]) 1 )) (defun (push-scnd-row-stack-item k ) (= (next [ stack/STACK_ITEM_POP k ]) 0 )) (defun (inc-scnd-row-stack-item-X-height-by-Y k increment) (= (next [ stack/STACK_ITEM_HEIGHT k ]) (+ HEIGHT increment) )) @@ -318,19 +318,19 @@ ;; stack item 5: (will-eq! [ stack/STACK_ITEM_HEIGHT 1 ] (* (b-sum-1) (- HEIGHT 2))) (will-eq! [ stack/STACK_ITEM_POP 1 ] (b-sum-1)) - (will-eq! [ stack/STACK_ITEM_STAMP 1 ] (* (b-sum-1) (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) 2))) + (will-eq! [ stack/STACK_ITEM_STAMP 1 ] (* (b-sum-1) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 2))) ;; stack item 6: (will-eq! [ stack/STACK_ITEM_HEIGHT 2 ] (* (b-sum-2) (- HEIGHT 3))) (will-eq! [ stack/STACK_ITEM_POP 2 ] (b-sum-2)) - (will-eq! [ stack/STACK_ITEM_STAMP 2 ] (* (b-sum-2) (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) 3))) + (will-eq! [ stack/STACK_ITEM_STAMP 2 ] (* (b-sum-2) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 3))) ;; stack item 7: (will-eq! [ stack/STACK_ITEM_HEIGHT 3 ] (* (b-sum-3) (- HEIGHT 4))) (will-eq! [ stack/STACK_ITEM_POP 3 ] (b-sum-3)) - (will-eq! [ stack/STACK_ITEM_STAMP 3 ] (* (b-sum-3) (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) 4))) + (will-eq! [ stack/STACK_ITEM_STAMP 3 ] (* (b-sum-3) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 4))) ;; stack item 8: (will-eq! [ stack/STACK_ITEM_HEIGHT 4 ] (* (b-sum-4) (- HEIGHT 5))) (will-eq! [ stack/STACK_ITEM_POP 4 ] (b-sum-4)) - (will-eq! [ stack/STACK_ITEM_STAMP 4 ] (* (b-sum-4) (+ (* MULTIPLIER___STACK_HEIGHT HUB_STAMP) 5))))) + (will-eq! [ stack/STACK_ITEM_STAMP 4 ] (* (b-sum-4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 5))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -355,7 +355,7 @@ ;; stack item 4: (= [ stack/STACK_ITEM_HEIGHT 4 ] (* b HEIGHT)) (= [ stack/STACK_ITEM_POP 4 ] b) - (= [ stack/STACK_ITEM_STAMP 4 ] (* b MULTIPLIER___STACK_HEIGHT HUB_STAMP)) + (= [ stack/STACK_ITEM_STAMP 4 ] (* b MULTIPLIER___STACK_STAMP HUB_STAMP)) ;; height update; (debug (= HEIGHT_NEW (- HEIGHT 3 b))) )) @@ -397,7 +397,7 @@ ;; 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_HEIGHT HUB_STAMP) 2))) + (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) @@ -434,7 +434,7 @@ ;; 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_HEIGHT HEIGHT) 3))) + (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) From 8a442493e9f0587ffdb82c4b692774f1bd80f32e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 4 Nov 2024 21:02:18 +0100 Subject: [PATCH 26/30] ras: renaming --- hub/constraints/generalities/context.lisp | 4 +- hub/constraints/generalities/exceptions.lisp | 70 +++++++++---------- .../generalities/program_counter.lisp | 24 +++---- 3 files changed, 48 insertions(+), 50 deletions(-) diff --git a/hub/constraints/generalities/context.lisp b/hub/constraints/generalities/context.lisp index 9458b15f..43e2e174 100644 --- a/hub/constraints/generalities/context.lisp +++ b/hub/constraints/generalities/context.lisp @@ -14,9 +14,9 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; (defconstraint setting-the-context-may-change-flag () +;; (defconstraint generalitie---setting-the-CONTEXT_MAY_CHANGE-flag () ;; (begin -;; (is-binary CMC) +;; (is-binary CMC) ;; column already declared :binary@prove ;; (hub-stamp-constancy CMC) ;; (if-zero TX_EXEC (vanishes! CMC)) ;; (if-not-zero PEEK_AT_STACK diff --git a/hub/constraints/generalities/exceptions.lisp b/hub/constraints/generalities/exceptions.lisp index 7c46792d..6ddd81d5 100644 --- a/hub/constraints/generalities/exceptions.lisp +++ b/hub/constraints/generalities/exceptions.lisp @@ -42,28 +42,29 @@ -(defconstraint exception-flags-are-binary (:perspective stack) - (begin - (is-binary SUX ) - (is-binary SOX ) - (is-binary MXPX ) - (is-binary OOGX ) - (is-binary RDCX ) - (is-binary JUMPX ) - (is-binary STATICX ) - (is-binary SSTOREX ) - (is-binary ICPX ) - (is-binary MAXCSX ) - (is-binary OPCX ) - )) +;; ;; These columns are already marked binary@prove in their respective definitions +;; (defconstraint generalities---exceptions---stack-exception-flags-are-binary (:perspective stack) +;; (begin +;; (is-binary SUX ) +;; (is-binary SOX ) +;; (is-binary MXPX ) +;; (is-binary OOGX ) +;; (is-binary RDCX ) +;; (is-binary JUMPX ) +;; (is-binary STATICX ) +;; (is-binary SSTOREX ) +;; (is-binary ICPX ) +;; (is-binary MAXCSX ) +;; (is-binary OPCX ) +;; )) -(defconstraint exception-flags-are-exclusive (:perspective stack) - (is-binary (exception_flag_sum))) +(defconstraint generalities---exceptions---stack-exception-flags-are-exclusive (:perspective stack) + (is-binary (exception_flag_sum))) -(defconstraint exception-flags-are-stack-constant (:perspective stack) - (stack-row-constancy (weighted_exception_flag_sum))) +(defconstraint generalities---exceptions---exception-flags-are-stack-constant (:perspective stack) + (stack-row-constancy (weighted_exception_flag_sum))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -73,15 +74,15 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint automatic-exception-flag-vanishing (:perspective stack) - (begin - (eq! INVALID_FLAG OPCX) - (if-zero MXP_FLAG (vanishes! MXPX)) - (if-zero JUMP_FLAG (vanishes! JUMPX)) - (if-zero STATIC_FLAG (vanishes! STATICX)) - (if-not-zero (- INSTRUCTION EVM_INST_RETURNDATACOPY) (vanishes! RDCX)) - (if-not-zero (- INSTRUCTION EVM_INST_SSTORE) (vanishes! SSTOREX)) - (if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! (+ ICPX MAXCSX))))) +(defconstraint generalities---exceptions---automatic-stack-exception-flag-vanishing (:perspective stack) + (begin + (eq! INVALID_FLAG OPCX) + (if-zero MXP_FLAG (vanishes! MXPX)) + (if-zero JUMP_FLAG (vanishes! JUMPX)) + (if-zero STATIC_FLAG (vanishes! STATICX)) + (if-not-zero (- INSTRUCTION EVM_INST_RETURNDATACOPY) (vanishes! RDCX)) + (if-not-zero (- INSTRUCTION EVM_INST_SSTORE) (vanishes! SSTOREX)) + (if-not-zero (- INSTRUCTION EVM_INST_RETURN) (vanishes! (+ ICPX MAXCSX))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -90,12 +91,9 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; we deal with those constraints in context.lisp along side CMC - -;; (defconstraint exception_ahoy () -;; (begin -;; (is-binary XAHOY) -;; (hub-stamp-constancy XAHOY) -;; (if-zero TX_EXEC (vanishes! XAHOY)) -;; (if-not-zero PEEK_AT_STACK -;; (eq! (exception_flag_sum) XAHOY)))) +;; (defconstraint generalities---exceptions---setting-the-EXCEPTIONS_AHOY-flag () +;; (begin +;; (is-binary XAHOY) ;; column already declared :binary@prove +;; (hub-stamp-constancy XAHOY) +;; (if-zero TX_EXEC (eq! XAHOY 0)) +;; (if-not-zero PEEK_AT_STACK (eq! XAHOY (exception_flag_sum))))) diff --git a/hub/constraints/generalities/program_counter.lisp b/hub/constraints/generalities/program_counter.lisp index d75b3676..a5b21e9c 100644 --- a/hub/constraints/generalities/program_counter.lisp +++ b/hub/constraints/generalities/program_counter.lisp @@ -1,16 +1,16 @@ (module hub) -(defconstraint PC-stamp-constancy () - (begin - (hub-stamp-constancy PC) - (hub-stamp-constancy PC_NEW))) +(defconstraint generalities---program-counter---stamp-constancy () + (begin + (hub-stamp-constancy PC) + (hub-stamp-constancy PC_NEW))) -(defconstraint PC-automatic-vanishing-outside-of-EXEC-phase () - (if-zero TX_EXEC - (begin - (vanishes! PC) - (vanishes! PC_NEW)))) +(defconstraint generalities---program-counter---automatic-vanishing-outside-of-EXEC-phase () + (if-zero TX_EXEC + (begin + (vanishes! PC) + (vanishes! PC_NEW)))) -(defconstraint PC-automatic-update (:guard PEEK_AT_STACK) - (if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG)) - (eq! PC_NEW (+ 1 PC)))) +(defconstraint generalities---program-counter---automatic-update (:guard PEEK_AT_STACK) + (if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG)) + (eq! PC_NEW (+ 1 PC)))) From 5e8250838fb3f782a6e4eacfa1bc1b016035241c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 4 Nov 2024 21:03:53 +0100 Subject: [PATCH 27/30] fix: using HUB_COLUMNS to merge stuff into arith-dev --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c91b4a86..d25d80a0 100644 --- a/Makefile +++ b/Makefile @@ -135,7 +135,7 @@ ZKEVM_MODULES := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB} \ + ${HUB_COLUMNS} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ From ae831edbbdd7ff627a4c068a5a6dc90dd88e591f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Tue, 5 Nov 2024 15:08:31 +0100 Subject: [PATCH 28/30] ras MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com> --- hub/constraints/generalities/exceptions.lisp | 1 + 1 file changed, 1 insertion(+) diff --git a/hub/constraints/generalities/exceptions.lisp b/hub/constraints/generalities/exceptions.lisp index 6ddd81d5..7823f7ee 100644 --- a/hub/constraints/generalities/exceptions.lisp +++ b/hub/constraints/generalities/exceptions.lisp @@ -91,6 +91,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; we deal with those constraints in context.lisp along side CMC ;; (defconstraint generalities---exceptions---setting-the-EXCEPTIONS_AHOY-flag () ;; (begin ;; (is-binary XAHOY) ;; column already declared :binary@prove From 1ede9f5fda6ec2c7c0db7a07704eee2ab6dda3c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Tue, 5 Nov 2024 15:11:25 +0100 Subject: [PATCH 29/30] ras MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com> --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index d25d80a0..2045d1c4 100644 --- a/Makefile +++ b/Makefile @@ -176,7 +176,7 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ ${EUC} \ ${EXP} \ ${GAS} \ - ${HUB} \ + ${HUB_COLUMNS} \ ${LIBRARY} \ ${LOG_DATA} \ ${LOG_INFO} \ From bbc95873fdc2b5ec96ca056bc162205e15abe3d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Tue, 5 Nov 2024 15:15:55 +0100 Subject: [PATCH 30/30] typo MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com> --- hub/constraints/generalities/context.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hub/constraints/generalities/context.lisp b/hub/constraints/generalities/context.lisp index 43e2e174..2ada5763 100644 --- a/hub/constraints/generalities/context.lisp +++ b/hub/constraints/generalities/context.lisp @@ -14,7 +14,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; (defconstraint generalitie---setting-the-CONTEXT_MAY_CHANGE-flag () +;; (defconstraint generalities---setting-the-CONTEXT_MAY_CHANGE-flag () ;; (begin ;; (is-binary CMC) ;; column already declared :binary@prove ;; (hub-stamp-constancy CMC)