diff --git a/Makefile b/Makefile index 2dcfa87f..4c400597 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,5 @@ CORSET ?= corset +GO_CORSET ?= go-corset HUB_COLUMNS := $(wildcard hub/columns/*lisp) @@ -61,13 +62,15 @@ BLOCKDATA_FOR_REFERENCE_TESTS := $(wildcard blockdata/*.lisp) \ $(wildcard blockdata/lookups/*.lisp) # with gaslimit for linea file -BLOCKDATA := $(wildcard blockdata/*.lisp) \ - $(wildcard blockdata/processing/*.lisp) \ - $(wildcard blockdata/processing/gaslimit/common.lisp) \ - $(wildcard blockdata/processing/gaslimit/linea.lisp) \ - $(wildcard blockdata/lookups/*.lisp) +BLOCKDATA_FOR_LINEA := $(wildcard blockdata/*.lisp) \ + $(wildcard blockdata/processing/*.lisp) \ + $(wildcard blockdata/processing/gaslimit/common.lisp) \ + $(wildcard blockdata/processing/gaslimit/linea.lisp) \ + $(wildcard blockdata/lookups/*.lisp) -BLOCKHASH := blockhash +BLOCKHASH := $(wildcard blockhash/columns/*.lisp) \ + $(wildcard blockhash/lookups/*.lisp) \ + $(wildcard blockhash/*.lisp) CONSTANTS := constants/constants.lisp @@ -137,7 +140,7 @@ WCP := wcp ZKEVM_MODULES := ${ALU} \ ${BIN} \ ${BLAKE2f_MODEXP_DATA} \ - ${BLOCKDATA} \ + ${BLOCKDATA_FOR_LINEA} \ ${BLOCKHASH} \ ${CONSTANTS} \ ${EC_DATA} \ @@ -173,6 +176,9 @@ define.go: ${ZKEVM_MODULES} zkevm.bin: ${ZKEVM_MODULES} ${CORSET} compile -vv -o $@ ${ZKEVM_MODULES} +zkevm.go.bin: ${ZKEVM_MODULES} + ${GO_CORSET} compile -o $@ ${ZKEVM_MODULES} + ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ ${BIN} \ @@ -211,5 +217,8 @@ ZKEVM_MODULES_FOR_REFERENCE_TESTS := ${ALU} \ zkevm_for_reference_tests.bin: ${ZKEVM_MODULES_FOR_REFERENCE_TESTS} ${CORSET} compile -vv -o $@ ${ZKEVM_MODULES_FOR_REFERENCE_TESTS} +zkevm_for_reference_tests.go.bin: ${ZKEVM_MODULES_FOR_REFERENCE_TESTS} + ${GO_CORSET} compile -o $@ ${ZKEVM_MODULES_FOR_REFERENCE_TESTS} + diff --git a/bin/lookups/bin_into_binreftable.lisp b/bin/lookups/bin_into_binreftable.lisp index 5db4de47..cf8fa832 100644 --- a/bin/lookups/bin_into_binreftable.lisp +++ b/bin/lookups/bin_into_binreftable.lisp @@ -1,4 +1,4 @@ -(defpurefun (selector-bin-to-binreftable) +(defun (selector-bin-to-binreftable) (+ bin.IS_AND bin.IS_OR bin.IS_XOR bin.IS_NOT)) (deflookup diff --git a/blockdata/processing/gaslimit/common.lisp b/blockdata/processing/gaslimit/common.lisp index 7dd3f06e..8fc1c91a 100644 --- a/blockdata/processing/gaslimit/common.lisp +++ b/blockdata/processing/gaslimit/common.lisp @@ -8,7 +8,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (gaslimit-precondition) (* (- 1 (prev IS_GL)) IS_GL)) -(defun (prev-gas-limit) (shift BLOCK_GAS_LIMIT (* nROWS_DEPTH -1))) +(defun (prev-gas-limit) (shift BLOCK_GAS_LIMIT (- 0 nROWS_DEPTH))) (defun (curr-GASLIMIT-hi) (curr-data-hi)) (defun (curr-GASLIMIT-lo) (curr-data-lo)) (defun (prev-GASLIMIT-hi) (prev-data-hi)) diff --git a/blockdata/processing/gaslimit/ethereum.lisp b/blockdata/processing/gaslimit/ethereum.lisp index d3fd5a5a..b12b032b 100644 --- a/blockdata/processing/gaslimit/ethereum.lisp +++ b/blockdata/processing/gaslimit/ethereum.lisp @@ -1,5 +1,9 @@ (module blockdata) +;; TODO add reference to global constants +(defconst GAS_LIMIT_MINIMUM 5000) +(defconst GAS_LIMIT_MAXIMUM 0xffffffffffffffff) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 3 Computations and checks ;; @@ -14,7 +18,7 @@ (curr-GASLIMIT-hi) (curr-GASLIMIT-lo) 0 - ETHEREUM_GAS_LIMIT_MINIMUM)) + GAS_LIMIT_MINIMUM)) (defconstraint gaslimit---upper-bound---ETHEREUM (:guard (gaslimit-precondition)) @@ -23,4 +27,4 @@ (curr-GASLIMIT-hi) (curr-GASLIMIT-lo) 0 - ETHEREUM_GAS_LIMIT_MAXIMUM)) + GAS_LIMIT_MAXIMUM)) diff --git a/blockdata/processing/gaslimit/linea.lisp b/blockdata/processing/gaslimit/linea.lisp index 4cc9938b..76141104 100644 --- a/blockdata/processing/gaslimit/linea.lisp +++ b/blockdata/processing/gaslimit/linea.lisp @@ -1,5 +1,9 @@ (module blockdata) +;; TODO add reference to global constants +(defconst GAS_LIMIT_MINIMUM 61000000) +(defconst GAS_LIMIT_MAXIMUM 2000000000) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 3 Computations and checks ;; @@ -14,7 +18,7 @@ (curr-GASLIMIT-hi) (curr-GASLIMIT-lo) 0 - LINEA_GAS_LIMIT_MINIMUM)) + GAS_LIMIT_MINIMUM)) (defconstraint gaslimit---upper-bound---LINEA (:guard (gaslimit-precondition)) @@ -23,4 +27,4 @@ (curr-GASLIMIT-hi) (curr-GASLIMIT-lo) 0 - LINEA_GAS_LIMIT_MAXIMUM)) + GAS_LIMIT_MAXIMUM)) diff --git a/blockhash/columns.lisp b/blockhash/columns.lisp index dfa19a97..f71bb259 100644 --- a/blockhash/columns.lisp +++ b/blockhash/columns.lisp @@ -1,17 +1,39 @@ (module blockhash) (defcolumns - (IOMF :binary) - (BLOCK_NUMBER_HI :i128) - (BLOCK_NUMBER_LO :i128) - (RES_HI :i128) - (RES_LO :i128) - (REL_BLOCK :i8) - (ABS_BLOCK :i48) - (LOWER_BOUND_CHECK :binary) - (UPPER_BOUND_CHECK :binary) - (IN_RANGE :binary) - (BLOCK_HASH_HI :i128) - (BLOCK_HASH_LO :i128) - (BYTE_HI :array [0:15] :byte@prove) - (BYTE_LO :array [0:15] :byte@prove)) + (IOMF :binary@prove) + (MACRO :binary@prove) + (PRPRC :binary@prove) + (CT :i8) + (CT_MAX :i8)) + +(defperspective macro + ;; selector + MACRO + ;; macro-instruction fields + ( + (REL_BLOCK :i16) + (ABS_BLOCK :i48) + (BLOCKHASH_VAL_HI :i128) + (BLOCKHASH_VAL_LO :i128) + (BLOCKHASH_ARG_HI :i128) + (BLOCKHASH_ARG_LO :i128) + (BLOCKHASH_RES_HI :i128) + (BLOCKHASH_RES_LO :i128) + ) + ) + +(defperspective preprocessing + ;; selector + PRPRC + ;; instruction pre-processing fields + ( + (EXO_ARG_1_HI :i128) + (EXO_ARG_1_LO :i128) + (EXO_ARG_2_HI :i128) + (EXO_ARG_2_LO :i128) + (EXO_INST :i8) + (EXO_RES :binary@prove) + ) + ) + diff --git a/blockhash/constants.lisp b/blockhash/constants.lisp new file mode 100644 index 00000000..bdce9cb3 --- /dev/null +++ b/blockhash/constants.lisp @@ -0,0 +1,13 @@ +(module blockhash) + +(defconst + nROWS_MACRO 1 + nROWS_PRPRC 5 + BLOCKHASH_DEPTH (+ nROWS_MACRO nROWS_PRPRC) + NEGATIVE_OF_BLOCKHASH_DEPTH (- 0 BLOCKHASH_DEPTH) + ROFF___BLOCKHASH_arguments___monotony 1 + ROFF___BLOCKHASH_arguments___equality_test 2 + ROFF___ABS___comparison_to_256 3 + ROFF___curr_BLOCKHASH_argument___comparison_to_max 4 + ROFF___curr_BLOCKHASH_argument___comparison_to_min 5 + ) diff --git a/blockhash/constraints.lisp b/blockhash/constraints.lisp index 8e977962..64bd40ce 100644 --- a/blockhash/constraints.lisp +++ b/blockhash/constraints.lisp @@ -1,90 +1,253 @@ (module blockhash) -(defconstraint first-row (:domain {0}) - (vanishes! IOMF)) - -(defconstraint heartbeat () - (if-zero IOMF - (begin (vanishes! IN_RANGE) - (vanishes! BLOCK_NUMBER_HI) - (vanishes! BLOCK_NUMBER_LO)) - (begin (eq! IOMF 1) - (eq! (next IOMF) IOMF)))) - -(defconstraint horizontal-byte-dec () - (begin (eq! BLOCK_HASH_HI - (+ (* (^ 256 (- LLARGEMO 0)) - [BYTE_HI 0]) - (* (^ 256 (- LLARGEMO 1)) - [BYTE_HI 1]) - (* (^ 256 (- LLARGEMO 2)) - [BYTE_HI 2]) - (* (^ 256 (- LLARGEMO 3)) - [BYTE_HI 3]) - (* (^ 256 (- LLARGEMO 4)) - [BYTE_HI 4]) - (* (^ 256 (- LLARGEMO 5)) - [BYTE_HI 5]) - (* (^ 256 (- LLARGEMO 6)) - [BYTE_HI 6]) - (* (^ 256 (- LLARGEMO 7)) - [BYTE_HI 7]) - (* (^ 256 (- LLARGEMO 8)) - [BYTE_HI 8]) - (* (^ 256 (- LLARGEMO 9)) - [BYTE_HI 9]) - (* (^ 256 (- LLARGEMO 10)) - [BYTE_HI 10]) - (* (^ 256 (- LLARGEMO 11)) - [BYTE_HI 11]) - (* (^ 256 (- LLARGEMO 12)) - [BYTE_HI 12]) - (* (^ 256 (- LLARGEMO 13)) - [BYTE_HI 13]) - (* (^ 256 (- LLARGEMO 14)) - [BYTE_HI 14]) - (* (^ 256 (- LLARGEMO 15)) - [BYTE_HI 15]))) - (eq! BLOCK_HASH_LO - (+ (* (^ 256 (- LLARGEMO 0)) - [BYTE_LO 0]) - (* (^ 256 (- LLARGEMO 1)) - [BYTE_LO 1]) - (* (^ 256 (- LLARGEMO 2)) - [BYTE_LO 2]) - (* (^ 256 (- LLARGEMO 3)) - [BYTE_LO 3]) - (* (^ 256 (- LLARGEMO 4)) - [BYTE_LO 4]) - (* (^ 256 (- LLARGEMO 5)) - [BYTE_LO 5]) - (* (^ 256 (- LLARGEMO 6)) - [BYTE_LO 6]) - (* (^ 256 (- LLARGEMO 7)) - [BYTE_LO 7]) - (* (^ 256 (- LLARGEMO 8)) - [BYTE_LO 8]) - (* (^ 256 (- LLARGEMO 9)) - [BYTE_LO 9]) - (* (^ 256 (- LLARGEMO 10)) - [BYTE_LO 10]) - (* (^ 256 (- LLARGEMO 11)) - [BYTE_LO 11]) - (* (^ 256 (- LLARGEMO 12)) - [BYTE_LO 12]) - (* (^ 256 (- LLARGEMO 13)) - [BYTE_LO 13]) - (* (^ 256 (- LLARGEMO 14)) - [BYTE_LO 14]) - (* (^ 256 (- LLARGEMO 15)) - [BYTE_LO 15]))))) - -(defconstraint constency () - (begin (eq! IN_RANGE (* LOWER_BOUND_CHECK UPPER_BOUND_CHECK)) - (eq! RES_HI (* IN_RANGE BLOCK_HASH_HI)) - (eq! RES_LO (* IN_RANGE BLOCK_HASH_LO)) - (if-zero (remained-constant! BLOCK_NUMBER_LO) - (begin (remained-constant! BLOCK_HASH_HI) - (remained-constant! BLOCK_HASH_LO))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; X. Generalities ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.1 Shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; +(defun (flag-sum) (+ MACRO PRPRC)) +(defun (wght-sum) (+ (* 1 MACRO) + (* 2 PRPRC))) +(defun (transition-bit) (+ (* (- 1 MACRO) (next MACRO)) + (* (- 1 PRPRC) (next PRPRC)))) +(defun (ct-max-sum) (+ (* (- nROWS_MACRO 1) MACRO) + (* (- nROWS_PRPRC 1) PRPRC))) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.2 Binarities ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +;; ok via :binary@prove + +;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.3 Constancies ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint constancies () + (counter-constancy CT (wght-sum))) + +;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; X.4 Heartbeat ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;; + + +(defconstraint heartbeat---IOMF---unconditional-setting () + (eq! IOMF (flag-sum))) + +(defconstraint heartbeat---IOMF---initial-vanishing (:domain {0}) ;; "" + (vanishes! IOMF)) + +(defconstraint heartbeat---IOMF---consequences-of-it-vanishing () + (if-zero IOMF + (begin + (vanishes! CT) + (vanishes! (next PRPRC)) + (vanishes! (next CT)) + (debug (vanishes! macro/BLOCKHASH_ARG_HI)) + (debug (vanishes! macro/BLOCKHASH_ARG_LO)) + (debug (vanishes! macro/BLOCKHASH_VAL_HI)) + (debug (vanishes! macro/BLOCKHASH_VAL_LO)) + (debug (vanishes! macro/BLOCKHASH_RES_HI)) + (debug (vanishes! macro/BLOCKHASH_RES_LO))))) + +(defconstraint heartbeat---IOMF---nondecreasing () + (if-not-zero IOMF + (will-eq! IOMF 1))) + +(defconstraint heartbeat---CT_MAX---unconditional-setting () + (eq! CT_MAX (ct-max-sum))) + +(defconstraint heartbeat---CT---transitions () + (if-not-zero IOMF + (if-eq-else CT CT_MAX + ;; CT == CT_MAX case + (eq! (transition-bit) 1) + ;; CT != CT_MAX case + (will-inc! CT 1)))) + +(defconstraint heartbeat---CT---reset () + (if-not-zero (transition-bit) + (vanishes! (next CT)))) + +(defconstraint heartbeat---finalization (:domain {-1}) ;; "" + (if-not-zero IOMF + (begin + (eq! CT CT_MAX) + (eq! PRPRC 1)))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; Y. Processing ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Y.1 Shorthands ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (not-first) (shift IOMF NEGATIVE_OF_BLOCKHASH_DEPTH)) +(defun (prev-BH-arg-hi) (* (not-first) (shift macro/BLOCKHASH_ARG_HI NEGATIVE_OF_BLOCKHASH_DEPTH))) +(defun (prev-BH-arg-lo) (* (not-first) (shift macro/BLOCKHASH_ARG_LO NEGATIVE_OF_BLOCKHASH_DEPTH))) +(defun (curr-BH-arg-hi) macro/BLOCKHASH_ARG_HI ) +(defun (curr-BH-arg-lo) macro/BLOCKHASH_ARG_LO ) ;; "" + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Y.4 Module calls ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (wcp-call-to-LT relof + arg_1_hi + arg_1_lo + arg_2_hi + arg_2_lo) + (begin + (eq! (shift preprocessing/EXO_ARG_1_HI relof) arg_1_hi ) + (eq! (shift preprocessing/EXO_ARG_1_LO relof) arg_1_lo ) + (eq! (shift preprocessing/EXO_ARG_2_HI relof) arg_2_hi ) + (eq! (shift preprocessing/EXO_ARG_2_LO relof) arg_2_lo ) + (eq! (shift preprocessing/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 preprocessing/EXO_ARG_1_HI relof) arg_1_hi ) + (eq! (shift preprocessing/EXO_ARG_1_LO relof) arg_1_lo ) + (eq! (shift preprocessing/EXO_ARG_2_HI relof) arg_2_hi ) + (eq! (shift preprocessing/EXO_ARG_2_LO relof) arg_2_lo ) + (eq! (shift preprocessing/EXO_INST relof) WCP_INST_LEQ ))) + +(defun (wcp-call-to-EQ relof + arg_1_hi + arg_1_lo + arg_2_hi + arg_2_lo) + (begin + (eq! (shift preprocessing/EXO_ARG_1_HI relof) arg_1_hi ) + (eq! (shift preprocessing/EXO_ARG_1_LO relof) arg_1_lo ) + (eq! (shift preprocessing/EXO_ARG_2_HI relof) arg_2_hi ) + (eq! (shift preprocessing/EXO_ARG_2_LO relof) arg_2_lo ) + (eq! (shift preprocessing/EXO_INST relof) EVM_INST_EQ ))) + + + +(defun (result-must-be-true relof) (eq! (shift preprocessing/EXO_RES relof) 1)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Y.5 Processing constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint processing---row-1---blockhash-argument-monontony + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (begin + (wcp-call-to-LEQ ROFF___BLOCKHASH_arguments___monotony + (prev-BH-arg-hi) + (prev-BH-arg-lo) + (curr-BH-arg-hi) + (curr-BH-arg-lo)) + (result-must-be-true ROFF___BLOCKHASH_arguments___monotony))) + +(defconstraint processing---row-2---blockhash-argument-equality-test + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (wcp-call-to-EQ ROFF___BLOCKHASH_arguments___equality_test + (prev-BH-arg-hi) + (prev-BH-arg-lo) + (curr-BH-arg-hi) + (curr-BH-arg-lo))) + +(defun (same-argument) (shift preprocessing/EXO_RES ROFF___BLOCKHASH_arguments___equality_test)) + +(defconstraint processing---row-3---ABS-vs-256 + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (wcp-call-to-LEQ ROFF___ABS___comparison_to_256 + 0 + 256 + 0 + macro/ABS_BLOCK)) + +(defun (minimal-reachable) (* (shift preprocessing/EXO_RES ROFF___ABS___comparison_to_256) + (- macro/ABS_BLOCK 256))) + +(defconstraint processing---row-4---blockhash-argument-vs-max + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (wcp-call-to-LT ROFF___curr_BLOCKHASH_argument___comparison_to_max + (curr-BH-arg-hi) + (curr-BH-arg-lo) + 0 + macro/ABS_BLOCK)) + +(defun (upper-bound-ok) (shift preprocessing/EXO_RES ROFF___curr_BLOCKHASH_argument___comparison_to_max)) + +(defconstraint processing---row-5---blockhash-argument-vs-min + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (wcp-call-to-LEQ ROFF___curr_BLOCKHASH_argument___comparison_to_min + 0 + (minimal-reachable) + (curr-BH-arg-hi) + (curr-BH-arg-lo) + )) + +(defun (lower-bound-ok) (shift preprocessing/EXO_RES ROFF___curr_BLOCKHASH_argument___comparison_to_min)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Y.6 Result constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint setting-the-result + (:guard MACRO) + ;;;;;;;;;;;;;;;;; + (begin + (eq! macro/BLOCKHASH_RES_HI (* (arg-in-bounds) macro/BLOCKHASH_VAL_HI)) + (eq! macro/BLOCKHASH_RES_LO (* (arg-in-bounds) macro/BLOCKHASH_VAL_LO)))) + +(defun (arg-in-bounds) (* (lower-bound-ok) + (upper-bound-ok))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; ;;;; +;;;; Z. Consistency ;;;; +;;;; ;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint consistency () + (if-not-zero MACRO + (if-not-zero (not-first) + (if-not-zero (same-argument) + (begin + (eq! macro/BLOCKHASH_VAL_HI (shift macro/BLOCKHASH_VAL_HI NEGATIVE_OF_BLOCKHASH_DEPTH)) + (eq! macro/BLOCKHASH_VAL_LO (shift macro/BLOCKHASH_VAL_LO NEGATIVE_OF_BLOCKHASH_DEPTH))))))) diff --git a/blockhash/lookups/blockhash_into_blockdata.lisp b/blockhash/lookups/blockhash_into_blockdata.lisp index 6400f2bb..26f91473 100644 --- a/blockhash/lookups/blockhash_into_blockdata.lisp +++ b/blockhash/lookups/blockhash_into_blockdata.lisp @@ -1,16 +1,17 @@ +(defun (blockhash-into-blockdata-selector) blockhash.MACRO) ;; "" + (deflookup blockhash-into-blockdata ; target columns ( - blockdata.REL_BLOCK - blockdata.DATA_LO - blockdata.INST - ) + blockdata.REL_BLOCK + blockdata.DATA_LO + blockdata.INST + ) ; source columns ( - blockhash.REL_BLOCK - blockhash.ABS_BLOCK - (* blockhash.IOMF EVM_INST_NUMBER) - )) - - + (* (blockhash-into-blockdata-selector) blockhash.macro/REL_BLOCK) + (* (blockhash-into-blockdata-selector) blockhash.macro/ABS_BLOCK) + (* (blockhash-into-blockdata-selector) EVM_INST_NUMBER) + ) + ) diff --git a/blockhash/lookups/blockhash_into_wcp.lisp b/blockhash/lookups/blockhash_into_wcp.lisp new file mode 100644 index 00000000..6740f75b --- /dev/null +++ b/blockhash/lookups/blockhash_into_wcp.lisp @@ -0,0 +1,25 @@ +(defun (blockhash-into-wcp-selector) blockhash.PRPRC) ;; "" + +(deflookup + blockhash-into-wcp-lex + ; target columns + ( + wcp.ARGUMENT_1_HI + wcp.ARGUMENT_1_LO + wcp.ARGUMENT_2_HI + wcp.ARGUMENT_2_LO + wcp.INST + wcp.RESULT + ) + ; source columns + ( + (* blockhash.preprocessing/EXO_ARG_1_HI (blockhash-into-wcp-selector)) + (* blockhash.preprocessing/EXO_ARG_1_LO (blockhash-into-wcp-selector)) + (* blockhash.preprocessing/EXO_ARG_2_HI (blockhash-into-wcp-selector)) + (* blockhash.preprocessing/EXO_ARG_2_LO (blockhash-into-wcp-selector)) + (* blockhash.preprocessing/EXO_INST (blockhash-into-wcp-selector)) + (* blockhash.preprocessing/EXO_RES (blockhash-into-wcp-selector)) + ) + ) + + diff --git a/blockhash/lookups/blockhash_into_wcp_lex.lisp b/blockhash/lookups/blockhash_into_wcp_lex.lisp deleted file mode 100644 index 13d6de3b..00000000 --- a/blockhash/lookups/blockhash_into_wcp_lex.lisp +++ /dev/null @@ -1,22 +0,0 @@ -(deflookup - blockhash-into-wcp-lex - ; target columns - ( - wcp.ARGUMENT_1_HI - wcp.ARGUMENT_1_LO - wcp.ARGUMENT_2_HI - wcp.ARGUMENT_2_LO - wcp.RESULT - wcp.INST - ) - ; source columns - ( - (* blockhash.BLOCK_NUMBER_HI blockhash.IOMF) - (* blockhash.BLOCK_NUMBER_LO blockhash.IOMF) - (* (prev blockhash.BLOCK_NUMBER_HI) blockhash.IOMF) - (* (prev blockhash.BLOCK_NUMBER_LO) blockhash.IOMF) - blockhash.IOMF - (* WCP_INST_GEQ blockhash.IOMF) - )) - - diff --git a/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp b/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp deleted file mode 100644 index 781c566f..00000000 --- a/blockhash/lookups/blockhash_into_wcp_lower_bound.lisp +++ /dev/null @@ -1,22 +0,0 @@ -(deflookup - blockhash-into-wcp-lower-bound - ; target columns - ( - wcp.ARGUMENT_1_HI - wcp.ARGUMENT_1_LO - wcp.ARGUMENT_2_HI - wcp.ARGUMENT_2_LO - wcp.RESULT - wcp.INST - ) - ; source columns - ( - (* blockhash.BLOCK_NUMBER_HI blockhash.IOMF) - (* blockhash.BLOCK_NUMBER_LO blockhash.IOMF) - 0 - (* (- blockhash.ABS_BLOCK 256) blockhash.IOMF) - (* blockhash.LOWER_BOUND_CHECK blockhash.IOMF) - (* WCP_INST_GEQ blockhash.IOMF) - )) - - diff --git a/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp b/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp deleted file mode 100644 index a35122ba..00000000 --- a/blockhash/lookups/blockhash_into_wcp_upper_bound.lisp +++ /dev/null @@ -1,22 +0,0 @@ -(deflookup - blockhash-into-wcp-upper-bound - ; target columns - ( - wcp.ARGUMENT_1_HI - wcp.ARGUMENT_1_LO - wcp.ARGUMENT_2_HI - wcp.ARGUMENT_2_LO - wcp.RESULT - wcp.INST - ) - ; source columns - ( - (* blockhash.BLOCK_NUMBER_HI blockhash.IOMF) - (* blockhash.BLOCK_NUMBER_LO blockhash.IOMF) - 0 - (* blockhash.ABS_BLOCK blockhash.IOMF) - (* blockhash.UPPER_BOUND_CHECK blockhash.IOMF) - (* EVM_INST_LT blockhash.IOMF) - )) - - diff --git a/hub/columns/stack.lisp b/hub/columns/stack.lisp index 66034a0d..3aeaef0a 100644 --- a/hub/columns/stack.lisp +++ b/hub/columns/stack.lisp @@ -74,10 +74,5 @@ ( HASH_INFO_KECCAK_LO :i128 ) ;; log info related - (LOG_INFO_FLAG :binary@prove) - ) - - (defalias - INST INSTRUCTION - )) + (LOG_INFO_FLAG :binary@prove))) diff --git a/hub/constraints/account.lisp b/hub/constraints/account.lisp index 917ddd54..8aa6d1c7 100644 --- a/hub/constraints/account.lisp +++ b/hub/constraints/account.lisp @@ -9,58 +9,58 @@ ;; Nonce constraintes (defun (same_nonce_h) - (eq! NONCE NONCE_NEW)) + (eq! account/NONCE account/NONCE_NEW)) (defun (increment_nonce_h) - (eq! NONCE_NEW (+ NONCE 1))) + (eq! account/NONCE_NEW (+ account/NONCE 1))) (defun (decrement_nonce_h) - (eq! NONCE_NEW (- NONCE 1))) + (eq! account/NONCE_NEW (- account/NONCE 1))) (defun (undo_account_nonce_update_v) (begin - (eq! NONCE (- (prev NONCE_NEW) 1)) - (eq! NONCE_NEW (prev NONCE)))) + (eq! account/NONCE (- (prev account/NONCE_NEW) 1)) + (eq! account/NONCE_NEW (prev account/NONCE)))) (defun (undo_previous_account_nonce_update_v) (begin - (eq! NONCE (- (shift NONCE_NEW -2) 1)) - (eq! NONCE_NEW (shift NONCE -2)))) + (eq! account/NONCE (- (shift account/NONCE_NEW -2) 1)) + (eq! account/NONCE_NEW (shift account/NONCE -2)))) ;; Balance constraints (defun (same_balance_h) - (eq! BALANCE_NEW BALANCE)) + (eq! account/BALANCE_NEW account/BALANCE)) (defun (undo_account_balance_update_v) (begin - (eq! BALANCE (prev BALANCE_NEW)) - (eq! BALANCE_NEW (prev BALANCE)))) + (eq! account/BALANCE (prev account/BALANCE_NEW)) + (eq! account/BALANCE_NEW (prev account/BALANCE)))) (defun (undo_previous_account_balance_update_v) (begin - (eq! BALANCE (shift BALANCE_NEW -2)) - (eq! BALANCE_NEW (shift BALANCE -2)))) + (eq! account/BALANCE (shift account/BALANCE_NEW -2)) + (eq! account/BALANCE_NEW (shift account/BALANCE -2)))) ;; Warmth constraints (defun (same_account_warmth_h) - (eq! WARMTH_NEW WARMTH)) + (eq! account/WARMTH_NEW account/WARMTH)) (defun (turn_on_account_warmth_h) - (eq! WARMTH_NEW 1)) + (eq! account/WARMTH_NEW 1)) (defun (undo_account_warmth_update_v) (begin - (eq! WARMTH (prev WARMTH_NEW)) - (eq! WARMTH_NEW (prev WARMTH)))) + (eq! account/WARMTH (prev account/WARMTH_NEW)) + (eq! account/WARMTH_NEW (prev account/WARMTH)))) ;; Code constraints (defun (same_code_size_h) - (eq! CODE_SIZE_NEW CODE_SIZE)) + (eq! account/CODE_SIZE_NEW account/CODE_SIZE)) (defun (same_code_hash_h) (begin - (eq! CODE_HASH_HI_NEW CODE_HASH_HI) - (eq! CODE_HASH_LO_NEW CODE_HASH_LO))) + (eq! account/CODE_HASH_HI_NEW account/CODE_HASH_HI) + (eq! account/CODE_HASH_LO_NEW account/CODE_HASH_LO))) (defun (same_code_h) (begin @@ -69,22 +69,22 @@ (defun (undo_code_size_update_v) (begin - (eq! CODE_SIZE (prev CODE_SIZE_NEW)) - (eq! CODE_SIZE_NEW (prev CODE_SIZE)))) + (eq! account/CODE_SIZE (prev account/CODE_SIZE_NEW)) + (eq! account/CODE_SIZE_NEW (prev account/CODE_SIZE)))) (defun (undo_code_hash_update_v) (begin - (eq! CODE_HASH_HI (prev CODE_HASH_HI_NEW)) - (eq! CODE_HASH_HI_NEW (prev CODE_HASH_HI)) - (eq! CODE_HASH_LO (prev CODE_HASH_LO_NEW)) - (eq! CODE_HASH_LO_NEW (prev CODE_HASH_LO)))) + (eq! account/CODE_HASH_HI (prev account/CODE_HASH_HI_NEW)) + (eq! account/CODE_HASH_HI_NEW (prev account/CODE_HASH_HI)) + (eq! account/CODE_HASH_LO (prev account/CODE_HASH_LO_NEW)) + (eq! account/CODE_HASH_LO_NEW (prev account/CODE_HASH_LO)))) ;; Deployment status constraints (defun (same_dep_number_h) - (eq! DEPLOYMENT_NUMBER_NEW DEPLOYMENT_NUMBER)) + (eq! account/DEPLOYMENT_NUMBER_NEW account/DEPLOYMENT_NUMBER)) (defun (same_dep_status_h) - (eq! DEPLOYMENT_STATUS_NEW DEPLOYMENT_STATUS)) + (eq! account/DEPLOYMENT_STATUS_NEW account/DEPLOYMENT_STATUS)) (defun (same_dep_num_and_status_h) (begin @@ -93,13 +93,13 @@ (defun (undo_dep_number_update_v) (begin - (eq! DEPLOYMENT_NUMBER (prev DEPLOYMENT_NUMBER_NEW)) - (eq! DEPLOYMENT_NUMBER_NEW (prev DEPLOYMENT_NUMBER)))) + (eq! account/DEPLOYMENT_NUMBER (prev account/DEPLOYMENT_NUMBER_NEW)) + (eq! account/DEPLOYMENT_NUMBER_NEW (prev account/DEPLOYMENT_NUMBER)))) (defun (undo_dep_status_update_v) (begin - (eq! DEPLOYMENT_STATUS (prev DEPLOYMENT_STATUS_NEW)) - (eq! DEPLOYMENT_STATUS_NEW (prev DEPLOYMENT_STATUS)))) + (eq! account/DEPLOYMENT_STATUS (prev account/DEPLOYMENT_STATUS_NEW)) + (eq! account/DEPLOYMENT_STATUS_NEW (prev account/DEPLOYMENT_STATUS)))) (defun (undo_dep_status_and_number_update_v) (begin @@ -107,34 +107,34 @@ (undo_dep_status_update_v))) (defun (increment_dep_number_h) - (eq! DEPLOYMENT_NUMBER_NEW (+ DEPLOYMENT_NUMBER 1))) + (eq! account/DEPLOYMENT_NUMBER_NEW (+ account/DEPLOYMENT_NUMBER 1))) (defun (fresh_new_dep_num_and_status_h) (begin - (vanishes! NONCE_NEW) - (vanishes CODE_SIZE_NEW) - (vanishes! HAS_CODE_NEW) - (debug (eq! CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) - (debug (eq! CODE_HASH_LO_NEW EMPTY_KECCAK_LO)) + (vanishes! account/NONCE_NEW) + (vanishes! account/CODE_SIZE_NEW) + (vanishes! account/HAS_CODE_NEW) + (debug (eq! account/CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) + (debug (eq! account/CODE_HASH_LO_NEW EMPTY_KECCAK_LO)) (increment_dep_number_h) - (vanishes! DEPLOYMENT_STATUS_NEW))) + (vanishes! account/DEPLOYMENT_STATUS_NEW))) (defun (dep_num_and_status_update_for_deployment_with_code_h) (begin (increment_dep_number_h) - (eq! DEPLOYMENT_STATUS_NEW 1) - (vanishes! HAS_CODE_NEW) - (debug (eq! CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) - (debug (eq! CODE_HASH_LO_NEW EMPTY_KECCAK_LO)))) + (eq! account/DEPLOYMENT_STATUS_NEW 1) + (vanishes! account/HAS_CODE_NEW) + (debug (eq! account/CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) + (debug (eq! account/CODE_HASH_LO_NEW EMPTY_KECCAK_LO)))) (defun (dep_num_and_status_update_for_deployment_without_code_h) (begin (increment_dep_number_h) - (vanishes! DEPLOYMENT_STATUS_NEW) - (vanishes! CODE_SIZE_NEW) - (vanishes HAS_CODE_NEW) - (debug (eq! CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) - (debug (eq! CODE_HASH_LO_NEW EMPTY_KECCAK_LO)))) + (vanishes! account/DEPLOYMENT_STATUS_NEW) + (vanishes! account/CODE_SIZE_NEW) + (vanishes! account/HAS_CODE_NEW) + (debug (eq! account/CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) + (debug (eq! account/CODE_HASH_LO_NEW EMPTY_KECCAK_LO)))) ;; Account inspection (defun (account_opening_h) @@ -150,40 +150,40 @@ (defun (account_deletion_h) (begin - (vanishes! NONCE_NEW) - (vanishes! BALANCE_NEW) - (vanishes! CODE_SIZE_NEW) - (vanishes! HAS_CODE_NEW) - (debug (eq! CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) - (debug (eq! CODE_HASH_LO_NEW EMPTY_KECCAK_LO)) - fresh_new_dep_num_and_status_h)) + (vanishes! account/NONCE_NEW) + (vanishes! account/BALANCE_NEW) + (vanishes! account/CODE_SIZE_NEW) + (vanishes! account/HAS_CODE_NEW) + (debug (eq! account/CODE_HASH_HI_NEW EMPTY_KECCAK_HI)) + (debug (eq! account/CODE_HASH_LO_NEW EMPTY_KECCAK_LO)) + (fresh_new_dep_num_and_status_h))) (defun (same_addr_as_previously_v) (begin - (remained-constant! ADDRESS_HI) - (remained-constant! ADDRESS_LO))) + (remained-constant! account/ADDRESS_HI) + (remained-constant! account/ADDRESS_LO))) (defun (same_addr_and_dep_num_as_previously_v) (begin (same_addr_as_previously_v) - (eq! DEPLOYMENT_NUMBER (prev DEPLOYMENT_NUMBER_NEW)))) + (eq! account/DEPLOYMENT_NUMBER (prev account/DEPLOYMENT_NUMBER_NEW)))) (defun (same_addr_and_dep_num_and_dep_stage_as_previously_v) (begin (same_addr_and_dep_num_as_previously_v) - (eq! DEPLOYMENT_STATUS (prev DEPLOYMENT_STATUS_NEW)))) + (eq! account/DEPLOYMENT_STATUS (prev account/DEPLOYMENT_STATUS_NEW)))) -(defun (deploy_empty_bytecode_h) - (begin - (eq! ADDRESS_HI CODE_ADDRESS_HI) - (eq! ADDRESS_LO CODE_ADDRESS_LO) - (eq! DEPLOYMENT_NUMBER CODE_DEPLOYMENT_NUMBER) - (debug (eq! DEPLOYMENT_STATUS 1)) - (debug (vanishes! DEPLOYMENT_STATUS_NEW)) - (eq! DEPLOYMENT_STATUS_NEW (- DEPLOYMENT_STATUS 1)) - (vanishes! CODE_SIZE_NEW) - (vanishes! HAS_CODE_NEW) - (debug same_code_hash_h))) +;; (defun (deploy_empty_bytecode_h) +;; (begin +;; (eq! account/ADDRESS_HI CODE_ADDRESS_HI) +;; (eq! account/ADDRESS_LO CODE_ADDRESS_LO) +;; (eq! account/DEPLOYMENT_NUMBER CODE_DEPLOYMENT_NUMBER) +;; (debug (eq! account/DEPLOYMENT_STATUS 1)) +;; (debug (vanishes! account/DEPLOYMENT_STATUS_NEW)) +;; (eq! account/DEPLOYMENT_STATUS_NEW (- account/DEPLOYMENT_STATUS 1)) +;; (vanishes! account/CODE_SIZE_NEW) +;; (vanishes! account/HAS_CODE_NEW) +;; (debug same_code_hash_h))) ;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -193,18 +193,18 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint hascode_emptyness (:perspective account) - (if-eq-else CODE_HASH_HI EMPTY_KECCAK_HI - (if-eq-else CODE_HASH_LO EMPTY_KECCAK_LO - (vanishes! HAS_CODE) - (eq! HAS_CODE 1)) - (eq! HAS_CODE 1))) + (if-eq-else account/CODE_HASH_HI EMPTY_KECCAK_HI + (if-eq-else account/CODE_HASH_LO EMPTY_KECCAK_LO + (vanishes! account/HAS_CODE) + (eq! account/HAS_CODE 1)) + (eq! account/HAS_CODE 1))) (defconstraint hascode_new_emptyness (:perspective account) - (if-eq-else CODE_HASH_HI_NEW EMPTY_KECCAK_HI - (if-eq-else CODE_HASH_LO_NEW EMPTY_KECCAK_LO - (eq! HAS_CODE_NEW 0) - (eq! HAS_CODE_NEW 1)) - (eq! HAS_CODE_NEW 1))) + (if-eq-else account/CODE_HASH_HI_NEW EMPTY_KECCAK_HI + (if-eq-else account/CODE_HASH_LO_NEW EMPTY_KECCAK_LO + (eq! account/HAS_CODE_NEW 0) + (eq! account/HAS_CODE_NEW 1)) + (eq! account/HAS_CODE_NEW 1))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -216,15 +216,15 @@ ;; TODO DEBUG Only (defconstraint exist_is_binary (:perspective account) (begin - (is-binary EXISTS) - (is-binary EXISTS_NEW))) + (is-binary account/EXISTS) + (is-binary account/EXISTS_NEW))) (defconstraint exists_is_on (:perspective account) - (if-zero (+ (~ NONCE) (~ BALANCE) (~ HAS_CODE)) - (vanishes! EXISTS) - (eq! EXISTS 1))) + (if-zero (+ (~ account/NONCE) (~ account/BALANCE) (~ account/HAS_CODE)) + (vanishes! account/EXISTS) + (eq! account/EXISTS 1))) (defconstraint exists_new_is_on (:perspective account) - (if-zero (+ (~ NONCE_NEW) (~ BALANCE_NEW) (~ HAS_CODE_NEW)) - (vanishes! EXISTS_NEW) - (eq! EXISTS_NEW 1))) + (if-zero (+ (~ account/NONCE_NEW) (~ account/BALANCE_NEW) (~ account/HAS_CODE_NEW)) + (vanishes! account/EXISTS_NEW) + (eq! account/EXISTS_NEW 1))) diff --git a/hub/constraints/instruction-handling/call/generalities/universal.lisp b/hub/constraints/instruction-handling/call/generalities/universal.lisp index 28cf4a5a..1877acc2 100644 --- a/hub/constraints/instruction-handling/call/generalities/universal.lisp +++ b/hub/constraints/instruction-handling/call/generalities/universal.lisp @@ -149,7 +149,7 @@ (eq! (+ scenario/CALL_SMC_FAILURE_CALLER_WILL_REVERT scenario/CALL_SMC_SUCCESS_CALLER_WILL_REVERT) (call-instruction---caller-will-revert)) (debug (eq! (+ scenario/CALL_SMC_FAILURE_CALLER_WONT_REVERT scenario/CALL_SMC_SUCCESS_CALLER_WONT_REVERT) - (- 1 call-instruction---caller-will-revert))) + (- 1 (call-instruction---caller-will-revert)))) (eq! (scenario-shorthand---CALL---smc-failure) (call-instruction---callee-self-reverts)) (eq! (scenario-shorthand---CALL---smc-success) (- 1 (call-instruction---callee-self-reverts))))))) diff --git a/hub/constraints/instruction-handling/call/triggers.lisp b/hub/constraints/instruction-handling/call/triggers.lisp index 0d50053d..a4b4f848 100644 --- a/hub/constraints/instruction-handling/call/triggers.lisp +++ b/hub/constraints/instruction-handling/call/triggers.lisp @@ -30,7 +30,7 @@ (defun (call-instruction---trigger_ROMLEX) (+ (scenario-shorthand---CALL---smart-contract))) -(defun (call-instruction---call-requires-callee-account) (+ (shift misc/STP_FLAG CALL_misc___row_offset))) +;; (defun (call-instruction---call-requires-callee-account) (+ (shift misc/STP_FLAG CALL_misc___row_offset))) (defun (call-instruction---call-requires-caller-account) (+ (scenario-shorthand---CALL---unexceptional))) diff --git a/hub/constraints/instruction-handling/halting/selfdestruct.lisp b/hub/constraints/instruction-handling/halting/selfdestruct.lisp index f1a55a09..edd2a392 100644 --- a/hub/constraints/instruction-handling/halting/selfdestruct.lisp +++ b/hub/constraints/instruction-handling/halting/selfdestruct.lisp @@ -280,7 +280,7 @@ (if-eq-else (selfdestruct-instruction---account-address) (selfdestruct-instruction---recipient-address) ;; self destructing account address = recipient address (begin - (debug (vanishes! account/BALANCE ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW)) + ;;(debug (vanishes! account/BALANCE ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW)) (account-same-balance ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW)) ;; self destructing account address ≠ recipient address (account-increment-balance-by ROFF_SELFDESTRUCT___ACCOUNT___2ND_DOING_ROW (selfdestruct-instruction---balance))))))) diff --git a/hub/constraints/stack_patterns.lisp b/hub/constraints/stack_patterns.lisp index 82f52917..24dc47ab 100644 --- a/hub/constraints/stack_patterns.lisp +++ b/hub/constraints/stack_patterns.lisp @@ -292,10 +292,10 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (b-sum-1) (+ b1 b2 b3 b4)) -(defun (b-sum-2) (+ b2 b3 b4)) -(defun (b-sum-3) (+ b3 b4)) -(defun (b-sum-4) 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 @@ -314,21 +314,21 @@ ;; height update; (debug (= HEIGHT_NEW (- HEIGHT param 2))) ;; 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_STAMP HUB_STAMP) 2))) + (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) (- HEIGHT 3))) - (will-eq! [ stack/STACK_ITEM_POP 2 ] (b-sum-2)) - (will-eq! [ stack/STACK_ITEM_STAMP 2 ] (* (b-sum-2) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 3))) + (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) (- HEIGHT 4))) - (will-eq! [ stack/STACK_ITEM_POP 3 ] (b-sum-3)) - (will-eq! [ stack/STACK_ITEM_STAMP 3 ] (* (b-sum-3) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 4))) + (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) (- HEIGHT 5))) - (will-eq! [ stack/STACK_ITEM_POP 4 ] (b-sum-4)) - (will-eq! [ stack/STACK_ITEM_STAMP 4 ] (* (b-sum-4) (+ (* MULTIPLIER___STACK_STAMP HUB_STAMP) 5))))) + (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/lookups/hub_into_block_hash.lisp b/hub/lookups/hub_into_block_hash.lisp index 32790f76..55e754e3 100644 --- a/hub/lookups/hub_into_block_hash.lisp +++ b/hub/lookups/hub_into_block_hash.lisp @@ -5,11 +5,11 @@ hub-into-blockhash ;; target columns ( - blockhash.REL_BLOCK - blockhash.BLOCK_NUMBER_HI - blockhash.BLOCK_NUMBER_LO - blockhash.RES_HI - blockhash.RES_LO + blockhash.macro/REL_BLOCK + blockhash.macro/BLOCKHASH_ARG_HI + blockhash.macro/BLOCKHASH_ARG_LO + blockhash.macro/BLOCKHASH_RES_HI + blockhash.macro/BLOCKHASH_RES_LO ) ;; source columns ( diff --git a/hub/lookups/hub_into_rom_instruction_fetching.lisp b/hub/lookups/hub_into_rom_instruction_fetching.lisp index 6d0c8d15..5a8fa566 100644 --- a/hub/lookups/hub_into_rom_instruction_fetching.lisp +++ b/hub/lookups/hub_into_rom_instruction_fetching.lisp @@ -1,4 +1,4 @@ -(defpurefun (hub-into-rom-instruction-fetching-trigger) hub.PEEK_AT_STACK) +(defun (hub-into-rom-instruction-fetching-trigger) hub.PEEK_AT_STACK) (deflookup hub-into-rom-instruction-fetching ;; target columns diff --git a/logdata/lookups/logdata-to-rlprcpt.lisp b/logdata/lookups/logdata-to-rlprcpt.lisp index 557eaf11..d9f3adab 100644 --- a/logdata/lookups/logdata-to-rlprcpt.lisp +++ b/logdata/lookups/logdata-to-rlprcpt.lisp @@ -1,4 +1,4 @@ -(defpurefun (sel-logdata-to-rlptxnrcpt) +(defun (sel-logdata-to-rlptxnrcpt) logdata.LOGS_DATA) (deflookup diff --git a/loginfo/lookups/loginfo-into-logdata.lisp b/loginfo/lookups/loginfo-into-logdata.lisp index d4fa5654..d6571b2f 100644 --- a/loginfo/lookups/loginfo-into-logdata.lisp +++ b/loginfo/lookups/loginfo-into-logdata.lisp @@ -1,4 +1,4 @@ -(defpurefun (sel-loginfo-to-logdata) +(defun (sel-loginfo-to-logdata) loginfo.TXN_EMITS_LOGS) (deflookup diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index c90f58f5..0f217cbb 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -253,13 +253,13 @@ (if-eq IS_PHASE_VALUE 1 (eq! (next IS_PHASE_DATA) 1)) (if-eq IS_PHASE_DATA 1 - (begin (debug (vanishes! RLP_TXN_PHASE_SIZE)) + (begin ;;(debug (vanishes! RLP_TXN_PHASE_SIZE)) (vanishes! DATA_GAS_COST) (if-zero TYPE (eq! (next IS_PHASE_BETA) 1) (eq! (next IS_PHASE_ACCESS_LIST) 1)))) (if-eq IS_PHASE_ACCESS_LIST 1 - (begin (debug (vanishes! RLP_TXN_PHASE_SIZE)) + (begin ;;(debug (vanishes! RLP_TXN_PHASE_SIZE)) (vanishes! nADDR) (vanishes! nKEYS) (vanishes! nKEYS_PER_ADDR) diff --git a/rom/constraints.lisp b/rom/constraints.lisp index 6c78aef9..5d0c5572 100644 --- a/rom/constraints.lisp +++ b/rom/constraints.lisp @@ -60,7 +60,7 @@ (debug (vanishes! COUNTER_PUSH)) (debug (vanishes! PUSH_PARAMETER)) (debug (vanishes! PROGRAM_COUNTER))) - (begin (debug (or! (eq! COUNTER_MAX LLARGEMO) (eq! COUNTER_MAX EVMWORDMO))) + (begin (debug (or! (eq! COUNTER_MAX LLARGEMO) (eq! COUNTER_MAX WORD_SIZE_MO))) (if-eq COUNTER_MAX LLARGEMO (will-remain-constant! CFI)) (if-not-eq COUNTER COUNTER_MAX (will-remain-constant! CFI)) (if-eq CT WORD_SIZE_MO (will-inc! CFI 1))))) diff --git a/shf/constraints.lisp b/shf/constraints.lisp index 32a66d5f..1ba3d81d 100644 --- a/shf/constraints.lisp +++ b/shf/constraints.lisp @@ -191,7 +191,7 @@ ;; 2.5 shifting constraints ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (left-shift-by k ct bit_b bit_n B1_init B2_init B1_shft B2_shft) +(defun (left-shift-by k ct bit_b (bit_n :binary) B1_init B2_init B1_shft B2_shft) (begin (plateau-constraint ct bit_n (- LLARGE k)) (if-zero bit_b (begin (= B1_shft B1_init) @@ -203,7 +203,7 @@ (shift B2_init (- k LLARGE))) (vanishes! B2_shft)))))) -(defun (right-shift-by k ct neg inst bit_b bit_n B1_init B2_init B1_shft B2_shft) +(defun (right-shift-by k ct neg inst bit_b (bit_n :binary) B1_init B2_init B1_shft B2_shft) (begin (plateau-constraint ct bit_n k) (if-zero bit_b (begin (= B1_shft B1_init) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index 47b4b7ad..8cf48db8 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -131,7 +131,7 @@ (begin (if-zero ABS (begin (vanishes! BLK) (vanishes! REL) - (debug (vanishes! BLK_MAX)) + ;;(debug (vanishes! BLK_MAX)) (debug (vanishes! REL_MAX)) (if-not-zero (will-remain-constant! ABS) (begin (eq! (next BLK) 1)