From 24d159f084189513b3dce7d04f39e6799f8eb2ae Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Thu, 3 Apr 2025 12:23:44 +0200 Subject: [PATCH 01/11] EIP-3855: PUSH0 Signed-off-by: F Bojarski --- hub/constraints/instruction-handling/push_pop.lisp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/hub/constraints/instruction-handling/push_pop.lisp b/hub/constraints/instruction-handling/push_pop.lisp index 55061afc..97db8e9e 100644 --- a/hub/constraints/instruction-handling/push_pop.lisp +++ b/hub/constraints/instruction-handling/push_pop.lisp @@ -4,7 +4,8 @@ (defun (push-pop-instruction---result-hi) [ stack/STACK_ITEM_VALUE_HI 4 ]) (defun (push-pop-instruction---result-lo) [ stack/STACK_ITEM_VALUE_LO 4 ]) (defun (push-pop-instruction---is-POP) [ stack/DEC_FLAG 1 ]) -(defun (push-pop-instruction---is-PUSH) [ stack/DEC_FLAG 2 ]) ;; "" +(defun (push-pop-instruction---is-PUSH) [ stack/DEC_FLAG 2 ]) +(defun (push-pop-instruction---is-PUSH-ZERO) [ stack/DEC_FLAG 3 ]) ;; "" (defconstraint push-pop-instruction---setting-the-stack-pattern---POP-case (:guard (push-pop-instruction---standard-hypothesis)) @@ -13,7 +14,7 @@ (defconstraint push-pop-instruction---setting-the-stack-pattern---PUSH-case (:guard (push-pop-instruction---standard-hypothesis)) - (if-not-zero (push-pop-instruction---is-PUSH) + (if-not-zero (+ (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO) ) (stack-pattern-0-1))) (defconstraint push-pop-instruction---setting-NSR @@ -36,6 +37,12 @@ (begin (eq! (push-pop-instruction---result-hi) stack/PUSH_VALUE_HI) (eq! (push-pop-instruction---result-lo) stack/PUSH_VALUE_LO)))) +(defconstraint push-pop-instruction---setting-stack-values---PUSH0-case + (:guard (push-pop-instruction---standard-hypothesis)) + (if-not-zero (push-pop-instruction---is-PUSH-ZERO) + (begin (vanishes! (push-pop-instruction---result-hi)) + (vanishes! (push-pop-instruction---result-lo))))) + (defconstraint push-pop-instruction---setting-PC_NEW---POP-case (:guard (push-pop-instruction---standard-hypothesis)) (if-not-zero (push-pop-instruction---is-POP) From c8dacbec57362fbf70151879d0f3c067f6c74384 Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Thu, 3 Apr 2025 12:29:02 +0200 Subject: [PATCH 02/11] add constant Signed-off-by: F Bojarski --- constants/constants.lisp | 1 + 1 file changed, 1 insertion(+) diff --git a/constants/constants.lisp b/constants/constants.lisp index c7e8d426..80570907 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -75,6 +75,7 @@ EVM_INST_GAS 0x5A EVM_INST_JUMPDEST 0x5B ;; Push Operations + EVM_INST_PUSH0 0x5F EVM_INST_PUSH1 0x60 EVM_INST_PUSH2 0x61 EVM_INST_PUSH3 0x62 From 567d165f43d7357abce0332f4d40ae78c60cba22 Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Fri, 11 Apr 2025 08:43:00 +0200 Subject: [PATCH 03/11] fix: forgoten PUSH 0 in pC new update Signed-off-by: F Bojarski --- hub/constraints/instruction-handling/push_pop.lisp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hub/constraints/instruction-handling/push_pop.lisp b/hub/constraints/instruction-handling/push_pop.lisp index 97db8e9e..0e784a7e 100644 --- a/hub/constraints/instruction-handling/push_pop.lisp +++ b/hub/constraints/instruction-handling/push_pop.lisp @@ -50,5 +50,5 @@ (defconstraint push-pop-instruction---setting-PC_NEW---PUSH-case (:guard (push-pop-instruction---standard-hypothesis)) - (if-not-zero (push-pop-instruction---is-PUSH) - (eq! PC_NEW (+ 1 PC 1 (- stack/INSTRUCTION EVM_INST_PUSH1))))) + (if-not-zero (+ (force-bin (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO))) + (eq! PC_NEW (+ 1 PC (- stack/INSTRUCTION EVM_INST_PUSH0))))) From 8fd05add4bdb9d20d6b158ce97ed9ef147c6bbca Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Fri, 11 Apr 2025 08:48:47 +0200 Subject: [PATCH 04/11] typo Signed-off-by: F Bojarski --- hub/constraints/instruction-handling/push_pop.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hub/constraints/instruction-handling/push_pop.lisp b/hub/constraints/instruction-handling/push_pop.lisp index 0e784a7e..61184e83 100644 --- a/hub/constraints/instruction-handling/push_pop.lisp +++ b/hub/constraints/instruction-handling/push_pop.lisp @@ -50,5 +50,5 @@ (defconstraint push-pop-instruction---setting-PC_NEW---PUSH-case (:guard (push-pop-instruction---standard-hypothesis)) - (if-not-zero (+ (force-bin (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO))) + (if-not-zero (force-bin (+ (push-pop-instruction---is-PUSH) (push-pop-instruction---is-PUSH-ZERO))) (eq! PC_NEW (+ 1 PC (- stack/INSTRUCTION EVM_INST_PUSH0))))) From 5e95606598c9f8c5a18e2c425c6ccc0bf0eab22f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Sat, 12 Apr 2025 14:45:11 +0200 Subject: [PATCH 05/11] Splitting of `oob/constraints.lisp` (#646) --- oob/binarities.lisp | 13 + oob/columns.lisp | 3 +- oob/constancies.lisp | 14 + oob/constraints.lisp | 909 ------------------ oob/decoding.lisp | 19 + oob/heartbeat.lisp | 34 + oob/opcodes/call.lisp | 35 + oob/opcodes/cdl.lisp | 23 + oob/opcodes/create.lisp | 46 + oob/opcodes/deployment.lisp | 22 + oob/opcodes/jump.lisp | 26 + oob/opcodes/jumpi.lisp | 40 + oob/opcodes/rdc.lisp | 44 + oob/opcodes/sstore.lisp | 19 + oob/opcodes/xcall.lisp | 23 + oob/opcodes/xcreate.lisp | 9 + oob/precompiles/blake2f/cds.lisp | 22 + oob/precompiles/blake2f/params.lisp | 32 + .../common/common_constraints.lisp | 33 + oob/precompiles/common/ecpairing.lisp | 42 + .../common/ecrecover_ecadd_ecmul.lisp | 22 + .../common/sha2_ripemd_identity.lisp | 31 + oob/precompiles/modexp/cds.lisp | 28 + oob/precompiles/modexp/extract.lisp | 41 + oob/precompiles/modexp/lead.lisp | 54 ++ oob/precompiles/modexp/pricing.lisp | 53 + oob/precompiles/modexp/xbs.lisp | 41 + oob/shorthands.lisp | 116 +++ oob/specialized.lisp | 56 ++ 29 files changed, 940 insertions(+), 910 deletions(-) create mode 100644 oob/binarities.lisp create mode 100644 oob/constancies.lisp delete mode 100644 oob/constraints.lisp create mode 100644 oob/decoding.lisp create mode 100644 oob/heartbeat.lisp create mode 100644 oob/opcodes/call.lisp create mode 100644 oob/opcodes/cdl.lisp create mode 100644 oob/opcodes/create.lisp create mode 100644 oob/opcodes/deployment.lisp create mode 100644 oob/opcodes/jump.lisp create mode 100644 oob/opcodes/jumpi.lisp create mode 100644 oob/opcodes/rdc.lisp create mode 100644 oob/opcodes/sstore.lisp create mode 100644 oob/opcodes/xcall.lisp create mode 100644 oob/opcodes/xcreate.lisp create mode 100644 oob/precompiles/blake2f/cds.lisp create mode 100644 oob/precompiles/blake2f/params.lisp create mode 100644 oob/precompiles/common/common_constraints.lisp create mode 100644 oob/precompiles/common/ecpairing.lisp create mode 100644 oob/precompiles/common/ecrecover_ecadd_ecmul.lisp create mode 100644 oob/precompiles/common/sha2_ripemd_identity.lisp create mode 100644 oob/precompiles/modexp/cds.lisp create mode 100644 oob/precompiles/modexp/extract.lisp create mode 100644 oob/precompiles/modexp/lead.lisp create mode 100644 oob/precompiles/modexp/pricing.lisp create mode 100644 oob/precompiles/modexp/xbs.lisp create mode 100644 oob/shorthands.lisp create mode 100644 oob/specialized.lisp diff --git a/oob/binarities.lisp b/oob/binarities.lisp new file mode 100644 index 00000000..c4fd244b --- /dev/null +++ b/oob/binarities.lisp @@ -0,0 +1,13 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.2 binary constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint wcp-add-mod-are-exclusive () + (is-binary (lookup-sum 0))) + +;; others are done with binary@prove in columns.lisp diff --git a/oob/columns.lisp b/oob/columns.lisp index 497414dc..88e554e6 100644 --- a/oob/columns.lisp +++ b/oob/columns.lisp @@ -4,7 +4,7 @@ (STAMP :i32) (CT :i3) (CT_MAX :i3) - (DATA :i128 :array [9]) + (DATA :i128 :array [9]) ;; XXXXXX 9 -> 10 (OOB_INST :i16) (IS_JUMP :binary@prove) (IS_JUMPI :binary@prove) @@ -12,6 +12,7 @@ (IS_CDL :binary@prove) (IS_XCALL :binary@prove) (IS_CALL :binary@prove) + ;; (IS_XCREATE :binary@prove) ;; XXXXXX (IS_CREATE :binary@prove) (IS_SSTORE :binary@prove) (IS_DEPLOYMENT :binary@prove) diff --git a/oob/constancies.lisp b/oob/constancies.lisp new file mode 100644 index 00000000..e4f6e3a1 --- /dev/null +++ b/oob/constancies.lisp @@ -0,0 +1,14 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Constancy constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint counter-constancy () + (begin (counter-constancy CT STAMP) + (debug (counter-constancy CT CT_MAX)) + (for i [9] (counter-constancy CT [DATA i])) ;; XXXXXX 9 -> 10 + (counter-constancy CT OOB_INST))) diff --git a/oob/constraints.lisp b/oob/constraints.lisp deleted file mode 100644 index 39241c08..00000000 --- a/oob/constraints.lisp +++ /dev/null @@ -1,909 +0,0 @@ -(module oob) - -;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2 Constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.1 shorthands and ;; -;; constants ;; -;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (flag-sum-inst) (+ IS_JUMP IS_JUMPI - IS_RDC - IS_CDL - IS_XCALL - IS_CALL - IS_CREATE - IS_SSTORE - IS_DEPLOYMENT)) - -(defun (flag-sum-prc-common) (+ IS_ECRECOVER - IS_SHA2 - IS_RIPEMD - IS_IDENTITY - IS_ECADD - IS_ECMUL - IS_ECPAIRING)) - -(defun (flag-sum-prc-blake) (+ IS_BLAKE2F_CDS - IS_BLAKE2F_PARAMS)) - -(defun (flag-sum-prc-modexp) (+ IS_MODEXP_CDS - IS_MODEXP_XBS - IS_MODEXP_LEAD - IS_MODEXP_PRICING - IS_MODEXP_EXTRACT)) - -(defun (flag-sum-prc) (+ (flag-sum-prc-common) - (flag-sum-prc-blake) - (flag-sum-prc-modexp))) - -(defun (flag-sum) (+ (flag-sum-inst) - (flag-sum-prc))) - -(defun (wght-sum-inst) (+ (* OOB_INST_JUMP IS_JUMP) - (* OOB_INST_JUMPI IS_JUMPI) - (* OOB_INST_RDC IS_RDC) - (* OOB_INST_CDL IS_CDL) - (* OOB_INST_XCALL IS_XCALL) - (* OOB_INST_CALL IS_CALL) - (* OOB_INST_CREATE IS_CREATE) - (* OOB_INST_SSTORE IS_SSTORE) - (* OOB_INST_DEPLOYMENT IS_DEPLOYMENT))) - -(defun (wght-sum-prc-common) (+ (* OOB_INST_ECRECOVER IS_ECRECOVER) - (* OOB_INST_SHA2 IS_SHA2) - (* OOB_INST_RIPEMD IS_RIPEMD) - (* OOB_INST_IDENTITY IS_IDENTITY) - (* OOB_INST_ECADD IS_ECADD) - (* OOB_INST_ECMUL IS_ECMUL) - (* OOB_INST_ECPAIRING IS_ECPAIRING))) - -(defun (wght-sum-prc-blake) (+ (* OOB_INST_BLAKE_CDS IS_BLAKE2F_CDS) - (* OOB_INST_BLAKE_PARAMS IS_BLAKE2F_PARAMS))) - -(defun (wght-sum-prc-modexp) (+ (* OOB_INST_MODEXP_CDS IS_MODEXP_CDS) - (* OOB_INST_MODEXP_XBS IS_MODEXP_XBS) - (* OOB_INST_MODEXP_LEAD IS_MODEXP_LEAD) - (* OOB_INST_MODEXP_PRICING IS_MODEXP_PRICING) - (* OOB_INST_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) - -(defun (wght-sum-prc) (+ (wght-sum-prc-common) - (wght-sum-prc-blake) - (wght-sum-prc-modexp))) - -(defun (wght-sum) (+ (wght-sum-inst) - (wght-sum-prc))) - -(defun (maxct-sum-inst) (+ (* CT_MAX_JUMP IS_JUMP) - (* CT_MAX_JUMPI IS_JUMPI) - (* CT_MAX_RDC IS_RDC) - (* CT_MAX_CDL IS_CDL) - (* CT_MAX_XCALL IS_XCALL) - (* CT_MAX_CALL IS_CALL) - (* CT_MAX_CREATE IS_CREATE) - (* CT_MAX_SSTORE IS_SSTORE) - (* CT_MAX_DEPLOYMENT IS_DEPLOYMENT))) - -(defun (maxct-sum-prc-common) (+ (* CT_MAX_ECRECOVER IS_ECRECOVER) - (* CT_MAX_SHA2 IS_SHA2) - (* CT_MAX_RIPEMD IS_RIPEMD) - (* CT_MAX_IDENTITY IS_IDENTITY) - (* CT_MAX_ECADD IS_ECADD) - (* CT_MAX_ECMUL IS_ECMUL) - (* CT_MAX_ECPAIRING IS_ECPAIRING))) - -(defun (maxct-sum-prc-blake) (+ (* CT_MAX_BLAKE2F_CDS IS_BLAKE2F_CDS) - (* CT_MAX_BLAKE2F_PARAMS IS_BLAKE2F_PARAMS))) - -(defun (maxct-sum-prc-modexp) (+ (* CT_MAX_MODEXP_CDS IS_MODEXP_CDS) - (* CT_MAX_MODEXP_XBS IS_MODEXP_XBS) - (* CT_MAX_MODEXP_LEAD IS_MODEXP_LEAD) - (* CT_MAX_MODEXP_PRICING IS_MODEXP_PRICING) - (* CT_MAX_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) - -(defun (maxct-sum-prc) (+ (maxct-sum-prc-common) - (maxct-sum-prc-blake) - (maxct-sum-prc-modexp))) - -(defun (maxct-sum) (+ (maxct-sum-inst) - (maxct-sum-prc))) - -(defun (lookup-sum k) (+ (shift ADD_FLAG k) - (shift MOD_FLAG k) - (shift WCP_FLAG k))) - -(defun (wght-lookup-sum k) (+ (* 1 (shift ADD_FLAG k)) - (* 2 (shift MOD_FLAG k)) - (* 3 (shift WCP_FLAG k)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.2 binary constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconstraint wcp-add-mod-are-exclusive () - (is-binary (lookup-sum 0))) - -;; others are done with binary@prove in columns.lisp - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.3 instruction decoding ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconstraint flag-sum-vanishes () - (if-zero STAMP - (vanishes! (flag-sum)))) - -(defconstraint flag-sum-equal-one () - (if-not-zero STAMP - (eq! (flag-sum) 1))) - -(defconstraint decoding () - (eq! OOB_INST (wght-sum))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.4 Constancy ;; -;; constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconstraint counter-constancy () - (begin (counter-constancy CT STAMP) - (debug (counter-constancy CT CT_MAX)) - (for i [9] (counter-constancy CT [DATA i])) - (counter-constancy CT OOB_INST))) - -;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.5 heartbeat ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconstraint first-row (:domain {0}) - (vanishes! STAMP)) - -(defconstraint padding-vanishing () - (if-zero STAMP - (begin (vanishes! CT) - (vanishes! (+ (lookup-sum 0) (flag-sum)))))) - -(defconstraint stamp-increments () - (or! (remained-constant! STAMP) (did-inc! STAMP 1))) - -(defconstraint counter-reset () - (if-not (remained-constant! STAMP) - (vanishes! CT))) - -(defconstraint ct-max () - (eq! CT_MAX (maxct-sum))) - -(defconstraint non-trivial-instruction-counter-cycle () - (if-not-zero STAMP - (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1)))) - -(defconstraint final-row (:domain {-1}) - (if-not-zero STAMP - (eq! CT CT_MAX))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.6 Constraint systems ;; -;; for populating lookups ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; support function to improve to reduce code duplication in the functions below -(defun (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (shift [OUTGOING_DATA 1] k) arg_1_hi) - (eq! (shift [OUTGOING_DATA 2] k) arg_1_lo) - (eq! (shift [OUTGOING_DATA 3] k) arg_2_hi) - (eq! (shift [OUTGOING_DATA 4] k) arg_2_lo))) - -(defun (call-to-ADD k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 1) - (eq! (shift OUTGOING_INST k) EVM_INST_ADD) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-DIV k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 2) - (eq! (shift OUTGOING_INST k) EVM_INST_DIV) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-MOD k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 2) - (eq! (shift OUTGOING_INST k) EVM_INST_MOD) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-LT k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 3) - (eq! (shift OUTGOING_INST k) EVM_INST_LT) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-GT k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 3) - (eq! (shift OUTGOING_INST k) EVM_INST_GT) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-EQ k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) - (begin (eq! (wght-lookup-sum k) 3) - (eq! (shift OUTGOING_INST k) EVM_INST_EQ) - (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) - -(defun (call-to-ISZERO k arg_1_hi arg_1_lo) - (begin (eq! (wght-lookup-sum k) 3) - (eq! (shift OUTGOING_INST k) EVM_INST_ISZERO) - (eq! (shift [OUTGOING_DATA 1] k) arg_1_hi) - (eq! (shift [OUTGOING_DATA 2] k) arg_1_lo) - (debug (vanishes! (shift [OUTGOING_DATA 3] k))) - (debug (vanishes! (shift [OUTGOING_DATA 4] k))))) - -(defun (noCall k) - (begin (eq! (wght-lookup-sum k) 0))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3 Populating opcodes ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (assumption---fresh-new-stamp) (- STAMP (prev STAMP))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.3 For JUMP ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (jump---standard-precondition) IS_JUMP) -(defun (jump---pc-new-hi) [DATA 1]) -(defun (jump---pc-new-lo) [DATA 2]) -(defun (jump---code-size) [DATA 5]) -(defun (jump---guaranteed-exception) [DATA 7]) -(defun (jump---jump-must-be-attempted) [DATA 8]) -(defun (jump---valid-pc-new) OUTGOING_RES_LO) - -(defconstraint jump---compare-pc-new-against-code-size (:guard (* (assumption---fresh-new-stamp) (jump---standard-precondition))) - (call-to-LT 0 (jump---pc-new-hi) (jump---pc-new-lo) 0 (jump---code-size))) - -(defconstraint jump---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (jump---standard-precondition))) - (begin (eq! (jump---guaranteed-exception) (- 1 (jump---valid-pc-new))) - (eq! (jump---jump-must-be-attempted) (jump---valid-pc-new)) - (debug (is-binary (jump---guaranteed-exception))) - (debug (is-binary (jump---jump-must-be-attempted))) - (debug (eq! (+ (jump---guaranteed-exception) (jump---jump-must-be-attempted)) 1)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.4 For JUMPI ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (jumpi---standard-precondition) IS_JUMPI) -(defun (jumpi---pc-new-hi) [DATA 1]) -(defun (jumpi---pc-new-lo) [DATA 2]) -(defun (jumpi---jump-cond-hi) [DATA 3]) -(defun (jumpi---jump-cond-lo) [DATA 4]) -(defun (jumpi---code-size) [DATA 5]) -(defun (jumpi---jump-not-attempted) [DATA 6]) -(defun (jumpi---guaranteed-exception) [DATA 7]) -(defun (jumpi---jump-must-be-attempted) [DATA 8]) -(defun (jumpi---valid-pc-new) OUTGOING_RES_LO) -(defun (jumpi---jump-cond-is-zero) (next OUTGOING_RES_LO)) - -(defconstraint jumpi---compare-pc-new-against-code-size (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) - (call-to-LT 0 (jumpi---pc-new-hi) (jumpi---pc-new-lo) 0 (jumpi---code-size))) - -(defconstraint jumpi---check-jump-cond-is-zero (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) - (call-to-ISZERO 1 (jumpi---jump-cond-hi) (jumpi---jump-cond-lo))) - -(defconstraint jumpi---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) - (begin (eq! (jumpi---jump-not-attempted) (jumpi---jump-cond-is-zero)) - (eq! (jumpi---guaranteed-exception) - (* (- 1 (jumpi---jump-cond-is-zero)) (- 1 (jumpi---valid-pc-new)))) - (eq! (jumpi---jump-must-be-attempted) - (* (- 1 (jumpi---jump-cond-is-zero)) (jumpi---valid-pc-new))) - (debug (is-binary (jumpi---jump-not-attempted))) - (debug (is-binary (jumpi---guaranteed-exception))) - (debug (is-binary (jumpi---jump-must-be-attempted))) - (debug (eq! (+ (jumpi---guaranteed-exception) - (jumpi---jump-must-be-attempted) - (jumpi---jump-not-attempted)) - 1)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.5 For ;; -;; RETURNDATACOPY ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Note. We use rdc as a shorthand for RETURNDATACOPY - -(defun (rdc---standard-precondition) IS_RDC) -(defun (rdc---offset-hi) [DATA 1]) -(defun (rdc---offset-lo) [DATA 2]) -(defun (rdc---size-hi) [DATA 3]) -(defun (rdc---size-lo) [DATA 4]) -(defun (rdc---rds) [DATA 5]) -(defun (rdc---rdcx) [DATA 7]) -(defun (rdc---rdc-roob) (- 1 OUTGOING_RES_LO)) -(defun (rdc---rdc-soob) (shift OUTGOING_RES_LO 2)) - -(defconstraint rdc---check-offset-is-zero (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) - (call-to-ISZERO 0 (rdc---offset-hi) (rdc---size-hi))) - -(defconstraint rdc---add-offset-and-size (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) - (if-zero (rdc---rdc-roob) - (call-to-ADD 1 0 (rdc---offset-lo) 0 (rdc---size-lo)) - (noCall 1))) - -(defconstraint rdc---compare-offset-plus-size-against-rds (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) - (if-zero (rdc---rdc-roob) - (begin (vanishes! (shift ADD_FLAG 2)) - (vanishes! (shift MOD_FLAG 2)) - (eq! (shift WCP_FLAG 2) 1) - (eq! (shift OUTGOING_INST 2) EVM_INST_GT) - (vanishes! (shift [OUTGOING_DATA 3] 2)) - (eq! (shift [OUTGOING_DATA 4] 2) (rdc---rds))) - (noCall 2))) - -(defconstraint rdc---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) - (eq! (rdc---rdcx) - (+ (rdc---rdc-roob) - (* (- 1 (rdc---rdc-roob)) (rdc---rdc-soob))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.6 For ;; -;; CALLDATALOAD ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Note. We use cdl as a shorthand for CALLDATALOAD - -(defun (cdl---standard-precondition) IS_CDL) -(defun (cdl---offset-hi) [DATA 1]) -(defun (cdl---offset-lo) [DATA 2]) -(defun (cdl---cds) [DATA 5]) -(defun (cdl---cdl-out-of-bounds) [DATA 7]) -(defun (cdl---touches-ram) OUTGOING_RES_LO) - -(defconstraint cdl---compare-offset-against-cds (:guard (* (assumption---fresh-new-stamp) (cdl---standard-precondition))) - (call-to-LT 0 (cdl---offset-hi) (cdl---offset-lo) 0 (cdl---cds))) - -(defconstraint cdl---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (cdl---standard-precondition))) - (eq! (cdl---cdl-out-of-bounds) (- 1 (cdl---touches-ram)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.7 For ;; -;; SSTORE ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (sstore---standard-precondition) IS_SSTORE) -(defun (sstore---gas) [DATA 5]) -(defun (sstore---sstorex) [DATA 7]) -(defun (sstore---sufficient-gas) OUTGOING_RES_LO) - -(defconstraint sstore---compare-g-call-stipend-against-gas (:guard (* (assumption---fresh-new-stamp) (sstore---standard-precondition))) - (call-to-LT 0 0 GAS_CONST_G_CALL_STIPEND 0 (sstore---gas))) - -(defconstraint sstore---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (sstore---standard-precondition))) - (eq! (sstore---sstorex) (- 1 (sstore---sufficient-gas)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.8 For ;; -;; DEPLOYMENT ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Note. Here "DEPLOYMENT" refers to the execution of the RETURN opcode in a deployment context - -(defun (deployment---standard-precondition) IS_DEPLOYMENT) -(defun (deployment---code-size-hi) [DATA 1]) -(defun (deployment---code-size-lo) [DATA 2]) -(defun (deployment---max-code-size-exception) [DATA 7]) -(defun (deployment---exceeds-max-code-size) OUTGOING_RES_LO) - -(defconstraint deployment---compare-max-code-size-against-code-size (:guard (* (assumption---fresh-new-stamp) (deployment---standard-precondition))) - (call-to-LT 0 0 MAX_CODE_SIZE (deployment---code-size-hi) (deployment---code-size-lo))) - -(defconstraint deployment---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (deployment---standard-precondition))) - (eq! (deployment---max-code-size-exception) (deployment---exceeds-max-code-size))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.9 For XCALL's ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Note. We use XCALL as a shorthand for "eXceptional CALL-type instruction" - -(defun (xcall---standard-precondition) IS_XCALL) -(defun (xcall---value-hi) [DATA 1]) -(defun (xcall---value-lo) [DATA 2]) -(defun (xcall---value-is-nonzero) [DATA 7]) -(defun (xcall---value-is-zero) [DATA 8]) - -(defconstraint xcall---check-value-is-zero (:guard (* (assumption---fresh-new-stamp) (xcall---standard-precondition))) - (call-to-ISZERO 0 (xcall---value-hi) (xcall---value-lo))) - -(defconstraint xcall---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (xcall---standard-precondition))) - (begin (eq! (xcall---value-is-nonzero) (- 1 OUTGOING_RES_LO)) - (eq! (xcall---value-is-zero) OUTGOING_RES_LO))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.10 For CALL's ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (call---standard-precondition) IS_CALL) -(defun (call---value-hi) [DATA 1]) -(defun (call---value-lo) [DATA 2]) -(defun (call---balance) [DATA 3]) -(defun (call---call-stack-depth) [DATA 6]) -(defun (call---value-is-nonzero) [DATA 7]) -(defun (call---aborting-condition) [DATA 8]) -(defun (call---insufficient-balance-abort) OUTGOING_RES_LO) -(defun (call---call-stack-depth-abort) (- 1 (next OUTGOING_RES_LO))) -(defun (call---value-is-zero) (shift OUTGOING_RES_LO 2)) - -(defconstraint call---compare-balance-against-value (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) - (call-to-LT 0 0 (call---balance) (call---value-hi) (call---value-lo))) - -(defconstraint call---compare-call-stack-depth-against-1024 (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) - (call-to-LT 1 0 (call---call-stack-depth) 0 1024)) - -(defconstraint call---check-value-is-zero (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) - (call-to-ISZERO 2 (call---value-hi) (call---value-lo))) - -(defconstraint call---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) - (begin (eq! (call---value-is-nonzero) (- 1 (call---value-is-zero))) - (eq! (call---aborting-condition) - (+ (call---insufficient-balance-abort) - (* (- 1 (call---insufficient-balance-abort)) (call---call-stack-depth-abort)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 3.11 For ;; -;; CREATE's ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (create---standard-precondition) IS_CREATE) -(defun (create---value-hi) [DATA 1]) -(defun (create---value-lo) [DATA 2]) -(defun (create---balance) [DATA 3]) -(defun (create---nonce) [DATA 4]) -(defun (create---has-code) [DATA 5]) -(defun (create---call-stack-depth) [DATA 6]) -(defun (create---aborting-condition) [DATA 7]) -(defun (create---failure-condition) [DATA 8]) -(defun (create---creator-nonce) [DATA 9]) -(defun (create---insufficient-balance-abort) OUTGOING_RES_LO) -(defun (create---stack-depth-abort) (- 1 (next OUTGOING_RES_LO))) -(defun (create---nonzero-nonce) (- 1 (shift OUTGOING_RES_LO 2))) -(defun (create---creator-nonce-abort) (- 1 (shift OUTGOING_RES_LO 3))) -(defun (create---aborting-conditions-sum) (+ (create---insufficient-balance-abort) (create---stack-depth-abort) (create---creator-nonce-abort))) - -(defconstraint create---compare-balance-against-value (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) - (call-to-LT 0 0 (create---balance) (create---value-hi) (create---value-lo))) - -(defconstraint create---compare-call-stack-depth-against-1024 (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) - (call-to-LT 1 0 (create---call-stack-depth) 0 1024)) - -(defconstraint create---check-nonce-is-zero (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) - (call-to-ISZERO 2 0 (create---nonce))) - -(defconstraint create---compare-creator-nonce-against-max-nonce (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) - (call-to-LT 3 0 (create---creator-nonce) 0 EIP2681_MAX_NONCE)) - -(defconstraint create---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) - (begin (if-zero (create---aborting-conditions-sum) - (vanishes! (create---aborting-condition)) - (eq! (create---aborting-condition) 1)) - (eq! (create---failure-condition) - (* (- 1 (create---aborting-condition)) - (+ (create---has-code) - (* (- 1 (create---has-code)) (create---nonzero-nonce))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 5 Populating common ;; -;; precompiles ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 5.1 Common ;; -;; constraints for ;; -;; precompiles ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-common---standard-precondition) (flag-sum-prc-common)) -(defun (prc---callee-gas) [DATA 1]) -(defun (prc---cds) [DATA 2]) -(defun (prc---r@c) [DATA 3]) -(defun (prc---hub-success) [DATA 4]) -(defun (prc---ram-success) [DATA 4]) -(defun (prc---return-gas) [DATA 5]) -(defun (prc---extract-call-data) [DATA 6]) -(defun (prc---empty-call-data) [DATA 7]) -(defun (prc---r@c-nonzero) [DATA 8]) -(defun (prc---cds-is-zero) OUTGOING_RES_LO) -(defun (prc---r@c-is-zero) (next OUTGOING_RES_LO)) - -(defconstraint prc---check-cds-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) - (call-to-ISZERO 0 0 (prc---cds))) - -(defconstraint prc---check-r@c-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) - (call-to-ISZERO 1 0 (prc---r@c))) - -(defconstraint prc---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) - (begin (eq! (prc---extract-call-data) - (* (prc---hub-success) (- 1 (prc---cds-is-zero)))) - (eq! (prc---empty-call-data) (* (prc---hub-success) (prc---cds-is-zero))) - (eq! (prc---r@c-nonzero) (- 1 (prc---r@c-is-zero))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 5.2 For ECRECOVER, ;; -;; ECADD, ECMUL ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition) (+ IS_ECRECOVER IS_ECADD IS_ECMUL)) -(defun (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost) (+ (* GAS_CONST_ECRECOVER IS_ECRECOVER) (* GAS_CONST_ECADD IS_ECADD) (* GAS_CONST_ECMUL IS_ECMUL))) -(defun (prc-ecrecover-prc-ecadd-prc-ecmul---insufficient-gas) (shift OUTGOING_RES_LO 2)) - -(defconstraint prc-ecrecover-prc-ecadd-prc-ecmul---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition))) - (call-to-LT 2 0 (prc---callee-gas) 0 (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost))) - -(defconstraint prc-ecrecover-prc-ecadd-prc-ecmul---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition))) - (begin (eq! (prc---hub-success) (- 1 (prc-ecrecover-prc-ecadd-prc-ecmul---insufficient-gas))) - (if-zero (prc---hub-success) - (vanishes! (prc---return-gas)) - (eq! (prc---return-gas) - (- (prc---callee-gas) (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 5.3 For SHA2-256, ;; -;; RIPEMD-160, IDENTITY ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-sha2-prc-ripemd-prc-identity---standard-precondition) (+ IS_SHA2 IS_RIPEMD IS_IDENTITY)) -(defun (prc-sha2-prc-ripemd-prc-identity---ceil) (shift OUTGOING_RES_LO 2)) -(defun (prc-sha2-prc-ripemd-prc-identity---insufficient-gas) (shift OUTGOING_RES_LO 3)) -(defun (prc-sha2-prc-ripemd-prc-identity---sha2-cost) (+ GAS_CONST_SHA2 (* GAS_CONST_SHA2_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) -(defun (prc-sha2-prc-ripemd-prc-identity---ripemd-cost) (+ GAS_CONST_RIPEMD (* GAS_CONST_RIPEMD_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) -(defun (prc-sha2-prc-ripemd-prc-identity---identity-cost) (+ GAS_CONST_IDENTITY (* GAS_CONST_IDENTITY_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) -(defun (prc-sha2-prc-ripemd-prc-identity---precompile-cost) (+ (* (prc-sha2-prc-ripemd-prc-identity---sha2-cost) IS_SHA2 ) - (* (prc-sha2-prc-ripemd-prc-identity---ripemd-cost) IS_RIPEMD ) - (* (prc-sha2-prc-ripemd-prc-identity---identity-cost) IS_IDENTITY))) - -(defconstraint prc-sha2-prc-ripemd-prc-identity---div-cds-plus-31-by-32 (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) - (call-to-DIV 2 0 (+ (prc---cds) 31) 0 32)) - -(defconstraint prc-sha2-prc-ripemd-prc-identity---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) - (call-to-LT 3 0 (prc---callee-gas) 0 (prc-sha2-prc-ripemd-prc-identity---precompile-cost))) - -(defconstraint prc-sha2-prc-ripemd-prc-identity---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) - (begin (eq! (prc---hub-success) (- 1 (prc-sha2-prc-ripemd-prc-identity---insufficient-gas))) - (if-zero (prc---hub-success) - (vanishes! (prc---return-gas)) - (eq! (prc---return-gas) - (- (prc---callee-gas) (prc-sha2-prc-ripemd-prc-identity---precompile-cost)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 4.4 For ECPAIRING ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-ecpairing---standard-precondition) IS_ECPAIRING) -(defun (prc-ecpairing---remainder) (shift OUTGOING_RES_LO 2)) -(defun (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) (shift OUTGOING_RES_LO 3)) -(defun (prc-ecpairing---insufficient-gas) (shift OUTGOING_RES_LO 4)) -(defun (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE) (* (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) - (+ (* GAS_CONST_ECPAIRING PRC_ECPAIRING_SIZE) (* GAS_CONST_ECPAIRING_PAIR (prc---cds))))) - -(defconstraint prc-ecpairing---mod-cds-by-PRC_ECPAIRING_SIZE (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) - (call-to-MOD 2 0 (prc---cds) 0 PRC_ECPAIRING_SIZE)) - -(defconstraint prc-ecpairing---check-remainder-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) - (call-to-ISZERO 3 0 (prc-ecpairing---remainder))) - -(defconstraint prc-ecpairing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) - (if-zero (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) - (noCall 4) - (begin (vanishes! (shift ADD_FLAG 4)) - (vanishes! (shift MOD_FLAG 4)) - (eq! (shift WCP_FLAG 4) 1) - (eq! (shift OUTGOING_INST 4) EVM_INST_LT) - (vanishes! (shift [OUTGOING_DATA 1] 4)) - (eq! (shift [OUTGOING_DATA 2] 4) (prc---callee-gas)) - (vanishes! (shift [OUTGOING_DATA 3] 4)) - (eq! (* (shift [OUTGOING_DATA 4] 4) PRC_ECPAIRING_SIZE) - (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE))))) - -(defconstraint prc-ecpairing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) - (begin (eq! (prc---hub-success) - (* (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) (- 1 (prc-ecpairing---insufficient-gas)))) - (if-zero (prc---hub-success) - (vanishes! (prc---return-gas)) - (eq! (* (prc---return-gas) PRC_ECPAIRING_SIZE) - (- (* (prc---callee-gas) PRC_ECPAIRING_SIZE) (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6 Populating MODEXP ;; -;; precompiles ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6.1 For MODEXP - cds ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-modexp-cds---standard-precondition) IS_MODEXP_CDS) -(defun (prc-modexp-cds---extract-bbs) [DATA 3]) -(defun (prc-modexp-cds---extract-ebs) [DATA 4]) -(defun (prc-modexp-cds---extract-mbs) [DATA 5]) - -(defconstraint prc-modexp-cds---compare-0-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) - (call-to-LT 0 0 0 0 (prc---cds))) - -(defconstraint prc-modexp-cds---compare-32-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) - (call-to-LT 1 0 32 0 (prc---cds))) - -(defconstraint prc-modexp-cds---compare-64-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) - (call-to-LT 2 0 64 0 (prc---cds))) - -(defconstraint prc-modexp-cds---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) - (begin (eq! (prc-modexp-cds---extract-bbs) OUTGOING_RES_LO) - (eq! (prc-modexp-cds---extract-ebs) (next OUTGOING_RES_LO)) - (eq! (prc-modexp-cds---extract-mbs) (shift OUTGOING_RES_LO 2)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6.2 For MODEXP - xbs ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) -(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) -(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) -(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) -(defun (prc-modexp-xbs---compute-max) [DATA 4]) -(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) -(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) -(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) - -(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 0 (prc-modexp-xbs---xbs-hi) (prc-modexp-xbs---xbs-lo) 0 513)) - -(defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) - -(defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) - -(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) - (eq! (prc-modexp-xbs---compo-to_512) 1))) - -(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) - (if-zero (prc-modexp-xbs---compute-max) - (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) - (vanishes! (prc-modexp-xbs---xbs-nonzero))) - (begin (eq! (prc-modexp-xbs---xbs-nonzero) - (- 1 (shift OUTGOING_RES_LO 2))) - (if-zero (prc-modexp-xbs---comp) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo)) - (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6.3 For MODEXP ;; -;; - lead ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-modexp-lead---standard-precondition) IS_MODEXP_LEAD) -(defun (prc-modexp-lead---bbs) [DATA 1]) -(defun (prc-modexp-lead---ebs) [DATA 3]) -(defun (prc-modexp-lead---load-lead) [DATA 4]) -(defun (prc-modexp-lead---cds-cutoff) [DATA 6]) -(defun (prc-modexp-lead---ebs-cutoff) [DATA 7]) -(defun (prc-modexp-lead---sub-ebs_32) [DATA 8]) -(defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO) -(defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO)) -(defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2)) -(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3)) - -(defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (call-to-ISZERO 0 0 (prc-modexp-lead---ebs))) - -(defconstraint prc-modexp-lead---compare-ebs-against-32 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (call-to-LT 1 0 (prc-modexp-lead---ebs) 0 32)) - -(defconstraint prc-modexp-lead---compare-ebs-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (call-to-LT 2 0 (+ 96 (prc-modexp-lead---bbs)) 0 (prc---cds))) - -(defconstraint prc-modexp-lead---compare-cds-minus-96-plus-bbs-against-32 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (if-not-zero (prc-modexp-lead---call-data-contains-exponent-bytes) - (call-to-LT 3 - 0 - (- (prc---cds) (+ 96 (prc-modexp-lead---bbs))) - 0 - 32))) - -(defconstraint prc-modexp-lead---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) - (begin (eq! (prc-modexp-lead---load-lead) - (* (prc-modexp-lead---call-data-contains-exponent-bytes) - (- 1 (prc-modexp-lead---ebs-is-zero)))) - (if-zero (prc-modexp-lead---call-data-contains-exponent-bytes) - (vanishes! (prc-modexp-lead---cds-cutoff)) - (if-zero (prc-modexp-lead---comp) - (eq! (prc-modexp-lead---cds-cutoff) 32) - (eq! (prc-modexp-lead---cds-cutoff) - (- (prc---cds) (+ 96 (prc-modexp-lead---bbs)))))) - (if-zero (prc-modexp-lead---ebs-less-than_32) - (eq! (prc-modexp-lead---ebs-cutoff) 32) - (eq! (prc-modexp-lead---ebs-cutoff) (prc-modexp-lead---ebs))) - (if-zero (prc-modexp-lead---ebs-less-than_32) - (eq! (prc-modexp-lead---sub-ebs_32) (- (prc-modexp-lead---ebs) 32)) - (vanishes! (prc-modexp-lead---sub-ebs_32))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6.4 For MODEXP ;; -;; - pricing ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING) -(defun (prc-modexp-pricing---exponent-log) [DATA 6]) -(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7]) -(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO)) -(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2))) -(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3)) -(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4)) -(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero) - (* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log)) - (prc-modexp-pricing---f-of-max))) -(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) - (prc-modexp-pricing---big-quotient) - GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 0 0 (prc---r@c))) - -(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log))) - -(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 2 - 0 - (+ (prc-modexp-pricing---max-xbs-ybs) 7) - 0 - 8)) - -(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR)) - -(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP)) - -(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost))) - -(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) - (begin (eq! (prc---ram-success) - (- 1 (shift OUTGOING_RES_LO 5))) - (if-zero (prc---ram-success) - (vanishes! (prc---return-gas)) - (eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost)))) - (eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 6.5 For MODEXP ;; -;; - extract ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-modexp-extract---standard-precondition) IS_MODEXP_EXTRACT) -(defun (prc-modexp-extract---bbs) [DATA 3]) -(defun (prc-modexp-extract---ebs) [DATA 4]) -(defun (prc-modexp-extract---mbs) [DATA 5]) -(defun (prc-modexp-extract---extract-base) [DATA 6]) -(defun (prc-modexp-extract---extract-exponent) [DATA 7]) -(defun (prc-modexp-extract---extract-modulus) [DATA 8]) -(defun (prc-modexp-extract---bbs-is-zero) OUTGOING_RES_LO) -(defun (prc-modexp-extract---ebs-is-zero) (next OUTGOING_RES_LO)) -(defun (prc-modexp-extract---mbs-is-zero) (shift OUTGOING_RES_LO 2)) -(defun (prc-modexp-extract---call-data-extends-beyond-exponent) (shift OUTGOING_RES_LO 3)) - -(defconstraint prc-modexp-extract---check-bbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) - (call-to-ISZERO 0 0 (prc-modexp-extract---bbs))) - -(defconstraint prc-modexp-extract---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) - (call-to-ISZERO 1 0 (prc-modexp-extract---ebs))) - -(defconstraint prc-modexp-extract---check-mbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) - (call-to-ISZERO 2 0 (prc-modexp-extract---mbs))) - -(defconstraint prc-modexp-extract---compare-96-plus-bbs-plus-ebs-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) - (call-to-LT 3 0 (+ 96 (prc-modexp-extract---bbs) (prc-modexp-extract---ebs)) 0 (prc---cds))) - -(defconstraint prc-modexp-extract---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) - (begin (eq! (prc-modexp-extract---extract-modulus) - (* (prc-modexp-extract---call-data-extends-beyond-exponent) - (- 1 (prc-modexp-extract---mbs-is-zero)))) - (eq! (prc-modexp-extract---extract-base) - (* (prc-modexp-extract---extract-modulus) (- 1 (prc-modexp-extract---bbs-is-zero)))) - (eq! (prc-modexp-extract---extract-exponent) - (* (prc-modexp-extract---extract-modulus) (- 1 (prc-modexp-extract---ebs-is-zero)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 7 Populating BLAKE2F ;; -;; precompiles ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 7.1 For BLAKE2F_cds ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-blake-cds---standard-precondition) IS_BLAKE2F_CDS) -(defun (prc-blake-cds---valid-cds) OUTGOING_RES_LO) -(defun (prc-blake-cds---r@c-is-zero) (next OUTGOING_RES_LO)) - -(defconstraint prc-blake-cds---compare-cds-against-PRC_BLAKE2F_SIZE (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) - (call-to-EQ 0 0 (prc---cds) 0 PRC_BLAKE2F_SIZE)) - -(defconstraint prc-blake-cds---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) - (call-to-ISZERO 1 0 (prc---r@c))) - -(defconstraint blake2f-a---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) - (begin (eq! (prc---hub-success) (prc-blake-cds---valid-cds)) - (eq! (prc---r@c-nonzero) (- 1 (prc-blake-cds---r@c-is-zero))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;::;; -;; ;; -;; 7.2 For BLAKE2F_params ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun (prc-blake-params---standard-precondition) IS_BLAKE2F_PARAMS) -(defun (prc-blake-params---blake-r) [DATA 6]) -(defun (prc-blake-params---blake-f) [DATA 7]) -(defun (prc-blake-params---sufficient-gas) (- 1 OUTGOING_RES_LO)) -(defun (prc-blake-params---f-is-a-bit) (next OUTGOING_RES_LO)) - - -(defconstraint prc-blake-params---compare-call-gas-against-blake-r (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) - (call-to-LT 0 0 (prc---callee-gas) 0 (* GAS_CONST_BLAKE2_PER_ROUND (prc-blake-params---blake-r)))) - -(defconstraint prc-blake-params---compare-blake-f-against-blake-f-square (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) - (call-to-EQ 1 - 0 - (prc-blake-params---blake-f) - 0 - (* (prc-blake-params---blake-f) (prc-blake-params---blake-f)))) - -(defconstraint prc-blake-params---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) - (begin (eq! (prc---ram-success) - (* (prc-blake-params---sufficient-gas) (prc-blake-params---f-is-a-bit))) - (if-not-zero (prc---ram-success) - (eq! (prc---return-gas) (- (prc---callee-gas) (prc-blake-params---blake-r))) - (vanishes! (prc---return-gas))))) - - diff --git a/oob/decoding.lisp b/oob/decoding.lisp new file mode 100644 index 00000000..f9012368 --- /dev/null +++ b/oob/decoding.lisp @@ -0,0 +1,19 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.3 instruction decoding ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint flag-sum-vanishes () + (if-zero STAMP + (vanishes! (flag-sum)))) + +(defconstraint flag-sum-equal-one () + (if-not-zero STAMP + (eq! (flag-sum) 1))) + +(defconstraint decoding () + (eq! OOB_INST (wght-sum))) diff --git a/oob/heartbeat.lisp b/oob/heartbeat.lisp new file mode 100644 index 00000000..585d60b3 --- /dev/null +++ b/oob/heartbeat.lisp @@ -0,0 +1,34 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.5 heartbeat ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint padding-vanishing () + (if-zero STAMP + (begin (vanishes! CT) + (vanishes! (+ (lookup-sum 0) (flag-sum)))))) + +(defconstraint stamp-increments () + (or! (remained-constant! STAMP) (did-inc! STAMP 1))) + +(defconstraint counter-reset () + (if-not (remained-constant! STAMP) + (vanishes! CT))) + +(defconstraint ct-max () + (eq! CT_MAX (maxct-sum))) + +(defconstraint non-trivial-instruction-counter-cycle () + (if-not-zero STAMP + (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1)))) + +(defconstraint final-row (:domain {-1}) + (if-not-zero STAMP + (eq! CT CT_MAX))) diff --git a/oob/opcodes/call.lisp b/oob/opcodes/call.lisp new file mode 100644 index 00000000..dca166b6 --- /dev/null +++ b/oob/opcodes/call.lisp @@ -0,0 +1,35 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_CALL ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;; + +(defun (call---standard-precondition) IS_CALL) +(defun (call---value-hi) [DATA 1]) +(defun (call---value-lo) [DATA 2]) +(defun (call---balance) [DATA 3]) +(defun (call---call-stack-depth) [DATA 6]) +(defun (call---value-is-nonzero) [DATA 7]) +(defun (call---aborting-condition) [DATA 8]) +(defun (call---insufficient-balance-abort) OUTGOING_RES_LO) +(defun (call---call-stack-depth-abort) (- 1 (next OUTGOING_RES_LO))) +(defun (call---value-is-zero) (shift OUTGOING_RES_LO 2)) + +(defconstraint call---compare-balance-against-value (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) + (call-to-LT 0 0 (call---balance) (call---value-hi) (call---value-lo))) + +(defconstraint call---compare-call-stack-depth-against-1024 (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) + (call-to-LT 1 0 (call---call-stack-depth) 0 1024)) + +(defconstraint call---check-value-is-zero (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) + (call-to-ISZERO 2 (call---value-hi) (call---value-lo))) + +(defconstraint call---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (call---standard-precondition))) + (begin (eq! (call---value-is-nonzero) (- 1 (call---value-is-zero))) + (eq! (call---aborting-condition) + (+ (call---insufficient-balance-abort) + (* (- 1 (call---insufficient-balance-abort)) (call---call-stack-depth-abort)))))) + diff --git a/oob/opcodes/cdl.lisp b/oob/opcodes/cdl.lisp new file mode 100644 index 00000000..4323b5a7 --- /dev/null +++ b/oob/opcodes/cdl.lisp @@ -0,0 +1,23 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_CDL ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;; + +;; Note. We use cdl as a shorthand for CALLDATALOAD + +(defun (cdl---standard-precondition) IS_CDL) +(defun (cdl---offset-hi) [DATA 1]) +(defun (cdl---offset-lo) [DATA 2]) +(defun (cdl---cds) [DATA 5]) +(defun (cdl---cdl-out-of-bounds) [DATA 7]) +(defun (cdl---touches-ram) OUTGOING_RES_LO) + +(defconstraint cdl---compare-offset-against-cds (:guard (* (assumption---fresh-new-stamp) (cdl---standard-precondition))) + (call-to-LT 0 (cdl---offset-hi) (cdl---offset-lo) 0 (cdl---cds))) + +(defconstraint cdl---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (cdl---standard-precondition))) + (eq! (cdl---cdl-out-of-bounds) (- 1 (cdl---touches-ram)))) diff --git a/oob/opcodes/create.lisp b/oob/opcodes/create.lisp new file mode 100644 index 00000000..1d20cf8a --- /dev/null +++ b/oob/opcodes/create.lisp @@ -0,0 +1,46 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_CREATE ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (create---standard-precondition) IS_CREATE) +(defun (create---value-hi) [DATA 1]) +(defun (create---value-lo) [DATA 2]) +(defun (create---balance) [DATA 3]) +(defun (create---nonce) [DATA 4]) +(defun (create---has-code) [DATA 5]) +(defun (create---call-stack-depth) [DATA 6]) +(defun (create---aborting-condition) [DATA 7]) +(defun (create---failure-condition) [DATA 8]) +(defun (create---creator-nonce) [DATA 9]) +;; (defun (create---init-code-size) [DATA 10]) ;; XXXXXX +(defun (create---insufficient-balance-abort) OUTGOING_RES_LO) +(defun (create---stack-depth-abort) (- 1 (next OUTGOING_RES_LO))) +(defun (create---nonzero-nonce) (- 1 (shift OUTGOING_RES_LO 2))) +(defun (create---creator-nonce-abort) (- 1 (shift OUTGOING_RES_LO 3))) +(defun (create---aborting-conditions-sum) (+ (create---insufficient-balance-abort) (create---stack-depth-abort) (create---creator-nonce-abort))) + +(defconstraint create---compare-balance-against-value (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) + (call-to-LT 0 0 (create---balance) (create---value-hi) (create---value-lo))) + +(defconstraint create---compare-call-stack-depth-against-1024 (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) + (call-to-LT 1 0 (create---call-stack-depth) 0 1024)) + +(defconstraint create---check-nonce-is-zero (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) + (call-to-ISZERO 2 0 (create---nonce))) + +(defconstraint create---compare-creator-nonce-against-max-nonce (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) + (call-to-LT 3 0 (create---creator-nonce) 0 EIP2681_MAX_NONCE)) + +(defconstraint create---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (create---standard-precondition))) + (begin (if-zero (create---aborting-conditions-sum) + (vanishes! (create---aborting-condition)) + (eq! (create---aborting-condition) 1)) + (eq! (create---failure-condition) + (* (- 1 (create---aborting-condition)) + (+ (create---has-code) + (* (- 1 (create---has-code)) (create---nonzero-nonce))))))) diff --git a/oob/opcodes/deployment.lisp b/oob/opcodes/deployment.lisp new file mode 100644 index 00000000..7ce08101 --- /dev/null +++ b/oob/opcodes/deployment.lisp @@ -0,0 +1,22 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_DEPLOYMENT ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Note. Here "DEPLOYMENT" refers to the execution of the RETURN opcode in a deployment context + +(defun (deployment---standard-precondition) IS_DEPLOYMENT) +(defun (deployment---code-size-hi) [DATA 1]) +(defun (deployment---code-size-lo) [DATA 2]) +(defun (deployment---max-code-size-exception) [DATA 7]) +(defun (deployment---exceeds-max-code-size) OUTGOING_RES_LO) + +(defconstraint deployment---compare-max-code-size-against-code-size (:guard (* (assumption---fresh-new-stamp) (deployment---standard-precondition))) + (call-to-LT 0 0 MAX_CODE_SIZE (deployment---code-size-hi) (deployment---code-size-lo))) + +(defconstraint deployment---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (deployment---standard-precondition))) + (eq! (deployment---max-code-size-exception) (deployment---exceeds-max-code-size))) diff --git a/oob/opcodes/jump.lisp b/oob/opcodes/jump.lisp new file mode 100644 index 00000000..cc2f0d30 --- /dev/null +++ b/oob/opcodes/jump.lisp @@ -0,0 +1,26 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_JUMP ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;; + +(defun (jump---standard-precondition) IS_JUMP) +(defun (jump---pc-new-hi) [DATA 1]) +(defun (jump---pc-new-lo) [DATA 2]) +(defun (jump---code-size) [DATA 5]) +(defun (jump---guaranteed-exception) [DATA 7]) +(defun (jump---jump-must-be-attempted) [DATA 8]) +(defun (jump---valid-pc-new) OUTGOING_RES_LO) + +(defconstraint jump---compare-pc-new-against-code-size (:guard (* (assumption---fresh-new-stamp) (jump---standard-precondition))) + (call-to-LT 0 (jump---pc-new-hi) (jump---pc-new-lo) 0 (jump---code-size))) + +(defconstraint jump---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (jump---standard-precondition))) + (begin (eq! (jump---guaranteed-exception) (- 1 (jump---valid-pc-new))) + (eq! (jump---jump-must-be-attempted) (jump---valid-pc-new)) + (debug (is-binary (jump---guaranteed-exception))) + (debug (is-binary (jump---jump-must-be-attempted))) + (debug (eq! (+ (jump---guaranteed-exception) (jump---jump-must-be-attempted)) 1)))) diff --git a/oob/opcodes/jumpi.lisp b/oob/opcodes/jumpi.lisp new file mode 100644 index 00000000..6ea0688b --- /dev/null +++ b/oob/opcodes/jumpi.lisp @@ -0,0 +1,40 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_JUMPI ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (jumpi---standard-precondition) IS_JUMPI) +(defun (jumpi---pc-new-hi) [DATA 1]) +(defun (jumpi---pc-new-lo) [DATA 2]) +(defun (jumpi---jump-cond-hi) [DATA 3]) +(defun (jumpi---jump-cond-lo) [DATA 4]) +(defun (jumpi---code-size) [DATA 5]) +(defun (jumpi---jump-not-attempted) [DATA 6]) +(defun (jumpi---guaranteed-exception) [DATA 7]) +(defun (jumpi---jump-must-be-attempted) [DATA 8]) +(defun (jumpi---valid-pc-new) OUTGOING_RES_LO) +(defun (jumpi---jump-cond-is-zero) (next OUTGOING_RES_LO)) + +(defconstraint jumpi---compare-pc-new-against-code-size (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) + (call-to-LT 0 (jumpi---pc-new-hi) (jumpi---pc-new-lo) 0 (jumpi---code-size))) + +(defconstraint jumpi---check-jump-cond-is-zero (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) + (call-to-ISZERO 1 (jumpi---jump-cond-hi) (jumpi---jump-cond-lo))) + +(defconstraint jumpi---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (jumpi---standard-precondition))) + (begin (eq! (jumpi---jump-not-attempted) (jumpi---jump-cond-is-zero)) + (eq! (jumpi---guaranteed-exception) + (* (- 1 (jumpi---jump-cond-is-zero)) (- 1 (jumpi---valid-pc-new)))) + (eq! (jumpi---jump-must-be-attempted) + (* (- 1 (jumpi---jump-cond-is-zero)) (jumpi---valid-pc-new))) + (debug (is-binary (jumpi---jump-not-attempted))) + (debug (is-binary (jumpi---guaranteed-exception))) + (debug (is-binary (jumpi---jump-must-be-attempted))) + (debug (eq! (+ (jumpi---guaranteed-exception) + (jumpi---jump-must-be-attempted) + (jumpi---jump-not-attempted)) + 1)))) diff --git a/oob/opcodes/rdc.lisp b/oob/opcodes/rdc.lisp new file mode 100644 index 00000000..74dec0dc --- /dev/null +++ b/oob/opcodes/rdc.lisp @@ -0,0 +1,44 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_RDC ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;; + +;; Note. We use rdc as a shorthand for RETURNDATACOPY + +(defun (rdc---standard-precondition) IS_RDC) +(defun (rdc---offset-hi) [DATA 1]) +(defun (rdc---offset-lo) [DATA 2]) +(defun (rdc---size-hi) [DATA 3]) +(defun (rdc---size-lo) [DATA 4]) +(defun (rdc---rds) [DATA 5]) +(defun (rdc---rdcx) [DATA 7]) +(defun (rdc---rdc-roob) (- 1 OUTGOING_RES_LO)) +(defun (rdc---rdc-soob) (shift OUTGOING_RES_LO 2)) + +(defconstraint rdc---check-offset-is-zero (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) + (call-to-ISZERO 0 (rdc---offset-hi) (rdc---size-hi))) + +(defconstraint rdc---add-offset-and-size (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) + (if-zero (rdc---rdc-roob) + (call-to-ADD 1 0 (rdc---offset-lo) 0 (rdc---size-lo)) + (noCall 1))) + +(defconstraint rdc---compare-offset-plus-size-against-rds (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) + (if-zero (rdc---rdc-roob) + (begin (vanishes! (shift ADD_FLAG 2)) + (vanishes! (shift MOD_FLAG 2)) + (eq! (shift WCP_FLAG 2) 1) + (eq! (shift OUTGOING_INST 2) EVM_INST_GT) + (vanishes! (shift [OUTGOING_DATA 3] 2)) + (eq! (shift [OUTGOING_DATA 4] 2) (rdc---rds))) + (noCall 2))) + +(defconstraint rdc---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (rdc---standard-precondition))) + (eq! (rdc---rdcx) + (+ (rdc---rdc-roob) + (* (- 1 (rdc---rdc-roob)) (rdc---rdc-soob))))) + diff --git a/oob/opcodes/sstore.lisp b/oob/opcodes/sstore.lisp new file mode 100644 index 00000000..51427fca --- /dev/null +++ b/oob/opcodes/sstore.lisp @@ -0,0 +1,19 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_SSTORE ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (sstore---standard-precondition) IS_SSTORE) +(defun (sstore---gas) [DATA 5]) +(defun (sstore---sstorex) [DATA 7]) +(defun (sstore---sufficient-gas) OUTGOING_RES_LO) + +(defconstraint sstore---compare-g-call-stipend-against-gas (:guard (* (assumption---fresh-new-stamp) (sstore---standard-precondition))) + (call-to-LT 0 0 GAS_CONST_G_CALL_STIPEND 0 (sstore---gas))) + +(defconstraint sstore---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (sstore---standard-precondition))) + (eq! (sstore---sstorex) (- 1 (sstore---sufficient-gas)))) diff --git a/oob/opcodes/xcall.lisp b/oob/opcodes/xcall.lisp new file mode 100644 index 00000000..163f6e84 --- /dev/null +++ b/oob/opcodes/xcall.lisp @@ -0,0 +1,23 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_XCALL ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;; + +;; Note. We use XCALL as a shorthand for "eXceptional CALL-type instruction" + +(defun (xcall---standard-precondition) IS_XCALL) +(defun (xcall---value-hi) [DATA 1]) +(defun (xcall---value-lo) [DATA 2]) +(defun (xcall---value-is-nonzero) [DATA 7]) +(defun (xcall---value-is-zero) [DATA 8]) + +(defconstraint xcall---check-value-is-zero (:guard (* (assumption---fresh-new-stamp) (xcall---standard-precondition))) + (call-to-ISZERO 0 (xcall---value-hi) (xcall---value-lo))) + +(defconstraint xcall---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (xcall---standard-precondition))) + (begin (eq! (xcall---value-is-nonzero) (- 1 OUTGOING_RES_LO)) + (eq! (xcall---value-is-zero) OUTGOING_RES_LO))) diff --git a/oob/opcodes/xcreate.lisp b/oob/opcodes/xcreate.lisp new file mode 100644 index 00000000..34e6b312 --- /dev/null +++ b/oob/opcodes/xcreate.lisp @@ -0,0 +1,9 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_XCREATE ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;; + diff --git a/oob/precompiles/blake2f/cds.lisp b/oob/precompiles/blake2f/cds.lisp new file mode 100644 index 00000000..7b50b21e --- /dev/null +++ b/oob/precompiles/blake2f/cds.lisp @@ -0,0 +1,22 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; BLAKE2F_cds ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-blake-cds---standard-precondition) IS_BLAKE2F_CDS) +(defun (prc-blake-cds---valid-cds) OUTGOING_RES_LO) +(defun (prc-blake-cds---r@c-is-zero) (next OUTGOING_RES_LO)) + +(defconstraint prc-blake-cds---compare-cds-against-PRC_BLAKE2F_SIZE (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) + (call-to-EQ 0 0 (prc---cds) 0 PRC_BLAKE2F_SIZE)) + +(defconstraint prc-blake-cds---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) + (call-to-ISZERO 1 0 (prc---r@c))) + +(defconstraint blake2f-a---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-blake-cds---standard-precondition))) + (begin (eq! (prc---hub-success) (prc-blake-cds---valid-cds)) + (eq! (prc---r@c-nonzero) (- 1 (prc-blake-cds---r@c-is-zero))))) diff --git a/oob/precompiles/blake2f/params.lisp b/oob/precompiles/blake2f/params.lisp new file mode 100644 index 00000000..9b21d131 --- /dev/null +++ b/oob/precompiles/blake2f/params.lisp @@ -0,0 +1,32 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;::;; +;; ;; +;; BLAKE2F_params ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-blake-params---standard-precondition) IS_BLAKE2F_PARAMS) +(defun (prc-blake-params---blake-r) [DATA 6]) +(defun (prc-blake-params---blake-f) [DATA 7]) +(defun (prc-blake-params---sufficient-gas) (- 1 OUTGOING_RES_LO)) +(defun (prc-blake-params---f-is-a-bit) (next OUTGOING_RES_LO)) + + +(defconstraint prc-blake-params---compare-call-gas-against-blake-r (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) + (call-to-LT 0 0 (prc---callee-gas) 0 (* GAS_CONST_BLAKE2_PER_ROUND (prc-blake-params---blake-r)))) + +(defconstraint prc-blake-params---compare-blake-f-against-blake-f-square (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) + (call-to-EQ 1 + 0 + (prc-blake-params---blake-f) + 0 + (* (prc-blake-params---blake-f) (prc-blake-params---blake-f)))) + +(defconstraint prc-blake-params---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-blake-params---standard-precondition))) + (begin (eq! (prc---ram-success) + (* (prc-blake-params---sufficient-gas) (prc-blake-params---f-is-a-bit))) + (if-not-zero (prc---ram-success) + (eq! (prc---return-gas) (- (prc---callee-gas) (prc-blake-params---blake-r))) + (vanishes! (prc---return-gas))))) diff --git a/oob/precompiles/common/common_constraints.lisp b/oob/precompiles/common/common_constraints.lisp new file mode 100644 index 00000000..b778e0c9 --- /dev/null +++ b/oob/precompiles/common/common_constraints.lisp @@ -0,0 +1,33 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_prc_common ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-common---standard-precondition) (flag-sum-prc-common)) +(defun (prc---callee-gas) [DATA 1]) +(defun (prc---cds) [DATA 2]) +(defun (prc---r@c) [DATA 3]) +(defun (prc---hub-success) [DATA 4]) +(defun (prc---ram-success) [DATA 4]) +(defun (prc---return-gas) [DATA 5]) +(defun (prc---extract-call-data) [DATA 6]) +(defun (prc---empty-call-data) [DATA 7]) +(defun (prc---r@c-nonzero) [DATA 8]) +(defun (prc---cds-is-zero) OUTGOING_RES_LO) +(defun (prc---r@c-is-zero) (next OUTGOING_RES_LO)) + +(defconstraint prc---check-cds-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) + (call-to-ISZERO 0 0 (prc---cds))) + +(defconstraint prc---check-r@c-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) + (call-to-ISZERO 1 0 (prc---r@c))) + +(defconstraint prc---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-common---standard-precondition))) + (begin (eq! (prc---extract-call-data) + (* (prc---hub-success) (- 1 (prc---cds-is-zero)))) + (eq! (prc---empty-call-data) (* (prc---hub-success) (prc---cds-is-zero))) + (eq! (prc---r@c-nonzero) (- 1 (prc---r@c-is-zero))))) diff --git a/oob/precompiles/common/ecpairing.lisp b/oob/precompiles/common/ecpairing.lisp new file mode 100644 index 00000000..56ea88a6 --- /dev/null +++ b/oob/precompiles/common/ecpairing.lisp @@ -0,0 +1,42 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 4.4 For ECPAIRING ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-ecpairing---standard-precondition) IS_ECPAIRING) +(defun (prc-ecpairing---remainder) (shift OUTGOING_RES_LO 2)) +(defun (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) (shift OUTGOING_RES_LO 3)) +(defun (prc-ecpairing---insufficient-gas) (shift OUTGOING_RES_LO 4)) +(defun (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE) (* (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) + (+ (* GAS_CONST_ECPAIRING PRC_ECPAIRING_SIZE) (* GAS_CONST_ECPAIRING_PAIR (prc---cds))))) + +(defconstraint prc-ecpairing---mod-cds-by-PRC_ECPAIRING_SIZE (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) + (call-to-MOD 2 0 (prc---cds) 0 PRC_ECPAIRING_SIZE)) + +(defconstraint prc-ecpairing---check-remainder-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) + (call-to-ISZERO 3 0 (prc-ecpairing---remainder))) + +(defconstraint prc-ecpairing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) + (if-zero (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) + (noCall 4) + (begin (vanishes! (shift ADD_FLAG 4)) + (vanishes! (shift MOD_FLAG 4)) + (eq! (shift WCP_FLAG 4) 1) + (eq! (shift OUTGOING_INST 4) EVM_INST_LT) + (vanishes! (shift [OUTGOING_DATA 1] 4)) + (eq! (shift [OUTGOING_DATA 2] 4) (prc---callee-gas)) + (vanishes! (shift [OUTGOING_DATA 3] 4)) + (eq! (* (shift [OUTGOING_DATA 4] 4) PRC_ECPAIRING_SIZE) + (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE))))) + +(defconstraint prc-ecpairing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-ecpairing---standard-precondition))) + (begin (eq! (prc---hub-success) + (* (prc-ecpairing---is-multiple_PRC_ECPAIRING_SIZE) (- 1 (prc-ecpairing---insufficient-gas)))) + (if-zero (prc---hub-success) + (vanishes! (prc---return-gas)) + (eq! (* (prc---return-gas) PRC_ECPAIRING_SIZE) + (- (* (prc---callee-gas) PRC_ECPAIRING_SIZE) (prc-ecpairing---precompile-cost_PRC_ECPAIRING_SIZE)))))) diff --git a/oob/precompiles/common/ecrecover_ecadd_ecmul.lisp b/oob/precompiles/common/ecrecover_ecadd_ecmul.lisp new file mode 100644 index 00000000..72706a80 --- /dev/null +++ b/oob/precompiles/common/ecrecover_ecadd_ecmul.lisp @@ -0,0 +1,22 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; For ECRECOVER, ECADD, ECMUL ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition) (+ IS_ECRECOVER IS_ECADD IS_ECMUL)) +(defun (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost) (+ (* GAS_CONST_ECRECOVER IS_ECRECOVER) (* GAS_CONST_ECADD IS_ECADD) (* GAS_CONST_ECMUL IS_ECMUL))) +(defun (prc-ecrecover-prc-ecadd-prc-ecmul---insufficient-gas) (shift OUTGOING_RES_LO 2)) + +(defconstraint prc-ecrecover-prc-ecadd-prc-ecmul---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition))) + (call-to-LT 2 0 (prc---callee-gas) 0 (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost))) + +(defconstraint prc-ecrecover-prc-ecadd-prc-ecmul---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-ecrecover-prc-ecadd-prc-ecmul---standard-precondition))) + (begin (eq! (prc---hub-success) (- 1 (prc-ecrecover-prc-ecadd-prc-ecmul---insufficient-gas))) + (if-zero (prc---hub-success) + (vanishes! (prc---return-gas)) + (eq! (prc---return-gas) + (- (prc---callee-gas) (prc-ecrecover-prc-ecadd-prc-ecmul---precompile-cost)))))) diff --git a/oob/precompiles/common/sha2_ripemd_identity.lisp b/oob/precompiles/common/sha2_ripemd_identity.lisp new file mode 100644 index 00000000..b546709e --- /dev/null +++ b/oob/precompiles/common/sha2_ripemd_identity.lisp @@ -0,0 +1,31 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; For SHA2-256, RIPEMD-160, IDENTITY ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-sha2-prc-ripemd-prc-identity---standard-precondition) (+ IS_SHA2 IS_RIPEMD IS_IDENTITY)) +(defun (prc-sha2-prc-ripemd-prc-identity---ceil) (shift OUTGOING_RES_LO 2)) +(defun (prc-sha2-prc-ripemd-prc-identity---insufficient-gas) (shift OUTGOING_RES_LO 3)) +(defun (prc-sha2-prc-ripemd-prc-identity---sha2-cost) (+ GAS_CONST_SHA2 (* GAS_CONST_SHA2_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) +(defun (prc-sha2-prc-ripemd-prc-identity---ripemd-cost) (+ GAS_CONST_RIPEMD (* GAS_CONST_RIPEMD_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) +(defun (prc-sha2-prc-ripemd-prc-identity---identity-cost) (+ GAS_CONST_IDENTITY (* GAS_CONST_IDENTITY_WORD (prc-sha2-prc-ripemd-prc-identity---ceil)))) +(defun (prc-sha2-prc-ripemd-prc-identity---precompile-cost) (+ (* (prc-sha2-prc-ripemd-prc-identity---sha2-cost) IS_SHA2 ) + (* (prc-sha2-prc-ripemd-prc-identity---ripemd-cost) IS_RIPEMD ) + (* (prc-sha2-prc-ripemd-prc-identity---identity-cost) IS_IDENTITY))) + +(defconstraint prc-sha2-prc-ripemd-prc-identity---div-cds-plus-31-by-32 (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) + (call-to-DIV 2 0 (+ (prc---cds) 31) 0 32)) + +(defconstraint prc-sha2-prc-ripemd-prc-identity---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) + (call-to-LT 3 0 (prc---callee-gas) 0 (prc-sha2-prc-ripemd-prc-identity---precompile-cost))) + +(defconstraint prc-sha2-prc-ripemd-prc-identity---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-sha2-prc-ripemd-prc-identity---standard-precondition))) + (begin (eq! (prc---hub-success) (- 1 (prc-sha2-prc-ripemd-prc-identity---insufficient-gas))) + (if-zero (prc---hub-success) + (vanishes! (prc---return-gas)) + (eq! (prc---return-gas) + (- (prc---callee-gas) (prc-sha2-prc-ripemd-prc-identity---precompile-cost)))))) diff --git a/oob/precompiles/modexp/cds.lisp b/oob/precompiles/modexp/cds.lisp new file mode 100644 index 00000000..77900cae --- /dev/null +++ b/oob/precompiles/modexp/cds.lisp @@ -0,0 +1,28 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_MODEXP_cds ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-modexp-cds---standard-precondition) IS_MODEXP_CDS) +(defun (prc-modexp-cds---extract-bbs) [DATA 3]) +(defun (prc-modexp-cds---extract-ebs) [DATA 4]) +(defun (prc-modexp-cds---extract-mbs) [DATA 5]) + +(defconstraint prc-modexp-cds---compare-0-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) + (call-to-LT 0 0 0 0 (prc---cds))) + +(defconstraint prc-modexp-cds---compare-32-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) + (call-to-LT 1 0 32 0 (prc---cds))) + +(defconstraint prc-modexp-cds---compare-64-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) + (call-to-LT 2 0 64 0 (prc---cds))) + +(defconstraint prc-modexp-cds---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-cds---standard-precondition))) + (begin (eq! (prc-modexp-cds---extract-bbs) OUTGOING_RES_LO) + (eq! (prc-modexp-cds---extract-ebs) (next OUTGOING_RES_LO)) + (eq! (prc-modexp-cds---extract-mbs) (shift OUTGOING_RES_LO 2)))) + diff --git a/oob/precompiles/modexp/extract.lisp b/oob/precompiles/modexp/extract.lisp new file mode 100644 index 00000000..2fef0cf6 --- /dev/null +++ b/oob/precompiles/modexp/extract.lisp @@ -0,0 +1,41 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_MODEXP_extract ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-modexp-extract---standard-precondition) IS_MODEXP_EXTRACT) +(defun (prc-modexp-extract---bbs) [DATA 3]) +(defun (prc-modexp-extract---ebs) [DATA 4]) +(defun (prc-modexp-extract---mbs) [DATA 5]) +(defun (prc-modexp-extract---extract-base) [DATA 6]) +(defun (prc-modexp-extract---extract-exponent) [DATA 7]) +(defun (prc-modexp-extract---extract-modulus) [DATA 8]) +(defun (prc-modexp-extract---bbs-is-zero) OUTGOING_RES_LO) +(defun (prc-modexp-extract---ebs-is-zero) (next OUTGOING_RES_LO)) +(defun (prc-modexp-extract---mbs-is-zero) (shift OUTGOING_RES_LO 2)) +(defun (prc-modexp-extract---call-data-extends-beyond-exponent) (shift OUTGOING_RES_LO 3)) + +(defconstraint prc-modexp-extract---check-bbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) + (call-to-ISZERO 0 0 (prc-modexp-extract---bbs))) + +(defconstraint prc-modexp-extract---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) + (call-to-ISZERO 1 0 (prc-modexp-extract---ebs))) + +(defconstraint prc-modexp-extract---check-mbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) + (call-to-ISZERO 2 0 (prc-modexp-extract---mbs))) + +(defconstraint prc-modexp-extract---compare-96-plus-bbs-plus-ebs-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) + (call-to-LT 3 0 (+ 96 (prc-modexp-extract---bbs) (prc-modexp-extract---ebs)) 0 (prc---cds))) + +(defconstraint prc-modexp-extract---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-extract---standard-precondition))) + (begin (eq! (prc-modexp-extract---extract-modulus) + (* (prc-modexp-extract---call-data-extends-beyond-exponent) + (- 1 (prc-modexp-extract---mbs-is-zero)))) + (eq! (prc-modexp-extract---extract-base) + (* (prc-modexp-extract---extract-modulus) (- 1 (prc-modexp-extract---bbs-is-zero)))) + (eq! (prc-modexp-extract---extract-exponent) + (* (prc-modexp-extract---extract-modulus) (- 1 (prc-modexp-extract---ebs-is-zero)))))) diff --git a/oob/precompiles/modexp/lead.lisp b/oob/precompiles/modexp/lead.lisp new file mode 100644 index 00000000..d02040e0 --- /dev/null +++ b/oob/precompiles/modexp/lead.lisp @@ -0,0 +1,54 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_MODEXP_lead ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-modexp-lead---standard-precondition) IS_MODEXP_LEAD) +(defun (prc-modexp-lead---bbs) [DATA 1]) +(defun (prc-modexp-lead---ebs) [DATA 3]) +(defun (prc-modexp-lead---load-lead) [DATA 4]) +(defun (prc-modexp-lead---cds-cutoff) [DATA 6]) +(defun (prc-modexp-lead---ebs-cutoff) [DATA 7]) +(defun (prc-modexp-lead---sub-ebs_32) [DATA 8]) +(defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO) +(defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO)) +(defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2)) +(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3)) + +(defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) + (call-to-ISZERO 0 0 (prc-modexp-lead---ebs))) + +(defconstraint prc-modexp-lead---compare-ebs-against-32 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) + (call-to-LT 1 0 (prc-modexp-lead---ebs) 0 32)) + +(defconstraint prc-modexp-lead---compare-ebs-against-cds (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) + (call-to-LT 2 0 (+ 96 (prc-modexp-lead---bbs)) 0 (prc---cds))) + +(defconstraint prc-modexp-lead---compare-cds-minus-96-plus-bbs-against-32 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) + (if-not-zero (prc-modexp-lead---call-data-contains-exponent-bytes) + (call-to-LT 3 + 0 + (- (prc---cds) (+ 96 (prc-modexp-lead---bbs))) + 0 + 32))) + +(defconstraint prc-modexp-lead---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition))) + (begin (eq! (prc-modexp-lead---load-lead) + (* (prc-modexp-lead---call-data-contains-exponent-bytes) + (- 1 (prc-modexp-lead---ebs-is-zero)))) + (if-zero (prc-modexp-lead---call-data-contains-exponent-bytes) + (vanishes! (prc-modexp-lead---cds-cutoff)) + (if-zero (prc-modexp-lead---comp) + (eq! (prc-modexp-lead---cds-cutoff) 32) + (eq! (prc-modexp-lead---cds-cutoff) + (- (prc---cds) (+ 96 (prc-modexp-lead---bbs)))))) + (if-zero (prc-modexp-lead---ebs-less-than_32) + (eq! (prc-modexp-lead---ebs-cutoff) 32) + (eq! (prc-modexp-lead---ebs-cutoff) (prc-modexp-lead---ebs))) + (if-zero (prc-modexp-lead---ebs-less-than_32) + (eq! (prc-modexp-lead---sub-ebs_32) (- (prc-modexp-lead---ebs) 32)) + (vanishes! (prc-modexp-lead---sub-ebs_32))))) diff --git a/oob/precompiles/modexp/pricing.lisp b/oob/precompiles/modexp/pricing.lisp new file mode 100644 index 00000000..6efc2556 --- /dev/null +++ b/oob/precompiles/modexp/pricing.lisp @@ -0,0 +1,53 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_MODEXP_pricing ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING) +(defun (prc-modexp-pricing---exponent-log) [DATA 6]) +(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7]) +(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO)) +(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2))) +(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3)) +(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4)) +(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero) + (* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log)) + (prc-modexp-pricing---f-of-max))) +(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) + (prc-modexp-pricing---big-quotient) + GAS_CONST_MODEXP)) + +(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-ISZERO 0 0 (prc---r@c))) + +(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log))) + +(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-DIV 2 + 0 + (+ (prc-modexp-pricing---max-xbs-ybs) 7) + 0 + 8)) + +(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR)) + +(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP)) + +(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost))) + +(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition))) + (begin (eq! (prc---ram-success) + (- 1 (shift OUTGOING_RES_LO 5))) + (if-zero (prc---ram-success) + (vanishes! (prc---return-gas)) + (eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost)))) + (eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO)))) + diff --git a/oob/precompiles/modexp/xbs.lisp b/oob/precompiles/modexp/xbs.lisp new file mode 100644 index 00000000..fbaaf481 --- /dev/null +++ b/oob/precompiles/modexp/xbs.lisp @@ -0,0 +1,41 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; OOB_INST_MODEXP_xbs ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS) +(defun (prc-modexp-xbs---xbs-hi) [DATA 1]) +(defun (prc-modexp-xbs---xbs-lo) [DATA 2]) +(defun (prc-modexp-xbs---ybs-lo) [DATA 3]) +(defun (prc-modexp-xbs---compute-max) [DATA 4]) +(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7]) +(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8]) +(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO) +(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO)) + +(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (call-to-LT 0 (prc-modexp-xbs---xbs-hi) (prc-modexp-xbs---xbs-lo) 0 513)) + +(defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo))) + +(defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo))) + +(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max))) + (eq! (prc-modexp-xbs---compo-to_512) 1))) + +(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition))) + (if-zero (prc-modexp-xbs---compute-max) + (begin (vanishes! (prc-modexp-xbs---max-xbs-ybs)) + (vanishes! (prc-modexp-xbs---xbs-nonzero))) + (begin (eq! (prc-modexp-xbs---xbs-nonzero) + (- 1 (shift OUTGOING_RES_LO 2))) + (if-zero (prc-modexp-xbs---comp) + (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo)) + (eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo)))))) diff --git a/oob/shorthands.lisp b/oob/shorthands.lisp new file mode 100644 index 00000000..06e58c87 --- /dev/null +++ b/oob/shorthands.lisp @@ -0,0 +1,116 @@ +(module oob) + + +(defun (flag-sum-inst) (+ IS_JUMP IS_JUMPI + IS_RDC + IS_CDL + IS_XCALL + IS_CALL + ;; IS_XCREATE ;; XXXXXX + IS_CREATE + IS_SSTORE + IS_DEPLOYMENT)) + +(defun (flag-sum-prc-common) (+ IS_ECRECOVER + IS_SHA2 + IS_RIPEMD + IS_IDENTITY + IS_ECADD + IS_ECMUL + IS_ECPAIRING)) + +(defun (flag-sum-prc-blake) (+ IS_BLAKE2F_CDS + IS_BLAKE2F_PARAMS)) + +(defun (flag-sum-prc-modexp) (+ IS_MODEXP_CDS + IS_MODEXP_XBS + IS_MODEXP_LEAD + IS_MODEXP_PRICING + IS_MODEXP_EXTRACT)) + +(defun (flag-sum-prc) (+ (flag-sum-prc-common) + (flag-sum-prc-blake) + (flag-sum-prc-modexp))) + +(defun (flag-sum) (+ (flag-sum-inst) + (flag-sum-prc))) + +(defun (wght-sum-inst) (+ (* OOB_INST_JUMP IS_JUMP) + (* OOB_INST_JUMPI IS_JUMPI) + (* OOB_INST_RDC IS_RDC) + (* OOB_INST_CDL IS_CDL) + (* OOB_INST_XCALL IS_XCALL) + (* OOB_INST_CALL IS_CALL) + ;; (* OOB_INST_XCREATE IS_XCREATE) ;; XXXXXX + (* OOB_INST_CREATE IS_CREATE) + (* OOB_INST_SSTORE IS_SSTORE) + (* OOB_INST_DEPLOYMENT IS_DEPLOYMENT))) + +(defun (wght-sum-prc-common) (+ (* OOB_INST_ECRECOVER IS_ECRECOVER) + (* OOB_INST_SHA2 IS_SHA2) + (* OOB_INST_RIPEMD IS_RIPEMD) + (* OOB_INST_IDENTITY IS_IDENTITY) + (* OOB_INST_ECADD IS_ECADD) + (* OOB_INST_ECMUL IS_ECMUL) + (* OOB_INST_ECPAIRING IS_ECPAIRING))) + +(defun (wght-sum-prc-blake) (+ (* OOB_INST_BLAKE_CDS IS_BLAKE2F_CDS) + (* OOB_INST_BLAKE_PARAMS IS_BLAKE2F_PARAMS))) + +(defun (wght-sum-prc-modexp) (+ (* OOB_INST_MODEXP_CDS IS_MODEXP_CDS) + (* OOB_INST_MODEXP_XBS IS_MODEXP_XBS) + (* OOB_INST_MODEXP_LEAD IS_MODEXP_LEAD) + (* OOB_INST_MODEXP_PRICING IS_MODEXP_PRICING) + (* OOB_INST_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) + +(defun (wght-sum-prc) (+ (wght-sum-prc-common) + (wght-sum-prc-blake) + (wght-sum-prc-modexp))) + +(defun (wght-sum) (+ (wght-sum-inst) + (wght-sum-prc))) + +(defun (maxct-sum-inst) (+ (* CT_MAX_JUMP IS_JUMP) + (* CT_MAX_JUMPI IS_JUMPI) + (* CT_MAX_RDC IS_RDC) + (* CT_MAX_CDL IS_CDL) + (* CT_MAX_XCALL IS_XCALL) + (* CT_MAX_CALL IS_CALL) + ;; (* CT_MAX_XCREATE IS_XCREATE) ;; XXXXXX + (* CT_MAX_CREATE IS_CREATE) + (* CT_MAX_SSTORE IS_SSTORE) + (* CT_MAX_DEPLOYMENT IS_DEPLOYMENT))) + +(defun (maxct-sum-prc-common) (+ (* CT_MAX_ECRECOVER IS_ECRECOVER) + (* CT_MAX_SHA2 IS_SHA2) + (* CT_MAX_RIPEMD IS_RIPEMD) + (* CT_MAX_IDENTITY IS_IDENTITY) + (* CT_MAX_ECADD IS_ECADD) + (* CT_MAX_ECMUL IS_ECMUL) + (* CT_MAX_ECPAIRING IS_ECPAIRING))) + +(defun (maxct-sum-prc-blake) (+ (* CT_MAX_BLAKE2F_CDS IS_BLAKE2F_CDS) + (* CT_MAX_BLAKE2F_PARAMS IS_BLAKE2F_PARAMS))) + +(defun (maxct-sum-prc-modexp) (+ (* CT_MAX_MODEXP_CDS IS_MODEXP_CDS) + (* CT_MAX_MODEXP_XBS IS_MODEXP_XBS) + (* CT_MAX_MODEXP_LEAD IS_MODEXP_LEAD) + (* CT_MAX_MODEXP_PRICING IS_MODEXP_PRICING) + (* CT_MAX_MODEXP_EXTRACT IS_MODEXP_EXTRACT))) + +(defun (maxct-sum-prc) (+ (maxct-sum-prc-common) + (maxct-sum-prc-blake) + (maxct-sum-prc-modexp))) + +(defun (maxct-sum) (+ (maxct-sum-inst) + (maxct-sum-prc))) + +(defun (lookup-sum k) (+ (shift ADD_FLAG k) + (shift MOD_FLAG k) + (shift WCP_FLAG k))) + +(defun (wght-lookup-sum k) (+ (* 1 (shift ADD_FLAG k)) + (* 2 (shift MOD_FLAG k)) + (* 3 (shift WCP_FLAG k)))) + +(defun (assumption---fresh-new-stamp) (- STAMP (prev STAMP))) diff --git a/oob/specialized.lisp b/oob/specialized.lisp new file mode 100644 index 00000000..c55ae503 --- /dev/null +++ b/oob/specialized.lisp @@ -0,0 +1,56 @@ +(module oob) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.6 Constraint systems ;; +;; for populating lookups ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; support function to improve to reduce code duplication in the functions below +(defun (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (shift [OUTGOING_DATA 1] k) arg_1_hi) + (eq! (shift [OUTGOING_DATA 2] k) arg_1_lo) + (eq! (shift [OUTGOING_DATA 3] k) arg_2_hi) + (eq! (shift [OUTGOING_DATA 4] k) arg_2_lo))) + +(defun (call-to-ADD k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 1) + (eq! (shift OUTGOING_INST k) EVM_INST_ADD) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-DIV k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 2) + (eq! (shift OUTGOING_INST k) EVM_INST_DIV) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-MOD k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 2) + (eq! (shift OUTGOING_INST k) EVM_INST_MOD) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-LT k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 3) + (eq! (shift OUTGOING_INST k) EVM_INST_LT) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-GT k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 3) + (eq! (shift OUTGOING_INST k) EVM_INST_GT) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-EQ k arg_1_hi arg_1_lo arg_2_hi arg_2_lo) + (begin (eq! (wght-lookup-sum k) 3) + (eq! (shift OUTGOING_INST k) EVM_INST_EQ) + (set-args k arg_1_hi arg_1_lo arg_2_hi arg_2_lo))) + +(defun (call-to-ISZERO k arg_1_hi arg_1_lo) + (begin (eq! (wght-lookup-sum k) 3) + (eq! (shift OUTGOING_INST k) EVM_INST_ISZERO) + (eq! (shift [OUTGOING_DATA 1] k) arg_1_hi) + (eq! (shift [OUTGOING_DATA 2] k) arg_1_lo) + (debug (vanishes! (shift [OUTGOING_DATA 3] k))) + (debug (vanishes! (shift [OUTGOING_DATA 4] k))))) + +(defun (noCall k) + (begin (eq! (wght-lookup-sum k) 0))) From bab8d16354841c0e738d41bb220c3fb6bf823132 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Sat, 12 Apr 2025 14:47:08 +0200 Subject: [PATCH 06/11] Splitting of `hub/misc/oob.lisp` (#645) --- hub/columns/miscellaneous.lisp | 2 +- hub/constraints/miscellaneous-rows/oob.lisp | 336 ------------------ .../oob/opcodes/oob_inst_call.lisp | 21 ++ .../oob/opcodes/oob_inst_cdl.lisp | 21 ++ .../oob/opcodes/oob_inst_create.lisp | 26 ++ .../oob/opcodes/oob_inst_deployment.lisp | 19 + .../oob/opcodes/oob_inst_jump.lisp | 20 ++ .../oob/opcodes/oob_inst_jumpi.lisp | 22 ++ .../oob/opcodes/oob_inst_rdc.lisp | 22 ++ .../oob/opcodes/oob_inst_sstore.lisp | 18 + .../oob/opcodes/oob_inst_xcall.lisp | 19 + .../oob/opcodes/oob_inst_xcreate.lispX | 22 ++ .../precompiles/blake/oob_inst_blake_cds.lisp | 19 + .../blake/oob_inst_blake_params.lisp | 20 ++ .../oob/precompiles/common/common.lisp | 22 ++ .../modexp/oob_inst_modexp_cds.lisp | 18 + .../modexp/oob_inst_modexp_extract.lisp | 21 ++ .../modexp/oob_inst_modexp_lead.lisp | 20 ++ .../modexp/oob_inst_modexp_pricing.lisp | 21 ++ .../modexp/oob_inst_modexp_xbs.lisp | 21 ++ .../miscellaneous-rows/oob/shorthands.lisp | 12 + 21 files changed, 385 insertions(+), 337 deletions(-) delete mode 100644 hub/constraints/miscellaneous-rows/oob.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_call.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_cdl.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_create.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_deployment.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jump.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jumpi.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_rdc.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_sstore.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcall.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcreate.lispX create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_cds.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_params.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/common/common.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_cds.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_extract.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_lead.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_pricing.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_xbs.lisp create mode 100644 hub/constraints/miscellaneous-rows/oob/shorthands.lisp diff --git a/hub/columns/miscellaneous.lisp b/hub/columns/miscellaneous.lisp index b04b507c..89de38a8 100644 --- a/hub/columns/miscellaneous.lisp +++ b/hub/columns/miscellaneous.lisp @@ -53,7 +53,7 @@ ;; OOB columns (OOB_INST :i16 ) - (OOB_DATA :array[1:9] :i128 ) + (OOB_DATA :array[1:9] :i128 ) ;; XXXXXX 9 -> 10 ;; STP columns ( STP_INSTRUCTION :byte ) diff --git a/hub/constraints/miscellaneous-rows/oob.lisp b/hub/constraints/miscellaneous-rows/oob.lisp deleted file mode 100644 index 50464c00..00000000 --- a/hub/constraints/miscellaneous-rows/oob.lisp +++ /dev/null @@ -1,336 +0,0 @@ -(module hub) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 9.4 MISC/OOB constraints: opcodes ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defun (set-OOB-instruction---jump kappa ;; offset - pc_new_hi ;; high part of proposed new program counter - pc_new_lo ;; low part of proposed new program counter - code_size ;; code size of byte code currently executing - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_JUMP ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) pc_new_hi) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) pc_new_lo) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) code_size) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - -(defun (set-OOB-instruction---jumpi kappa ;; offset - pc_new_hi ;; high part of proposed new program counter - pc_new_lo ;; low part of proposed new program counter - jump_condition_hi ;; high part of jump condition - jump_condition_lo ;; low part of jump condition - code_size ;; code size of byte code currently executing - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_JUMPI) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) pc_new_hi) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) pc_new_lo) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) jump_condition_hi) - (eq! (shift [ misc/OOB_DATA 4 ] kappa) jump_condition_lo) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) code_size) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - -(defun (set-OOB-instruction---sstore kappa ;; offset - gas_actual ;; GAS_ACTUAL - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_SSTORE ) - ;; (eq! (shift [ misc/OOB_DATA 1 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 2 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) gas_actual) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - -(defun (set-OOB-instruction---cdl kappa ;; row offset - offset_hi ;; offset within call data, high part - offset_lo ;; offset within call data, low part - call_data_size ;; call data size - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_CDL ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) offset_hi) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) offset_lo) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) call_data_size) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - -(defun (set-OOB-instruction---rdc kappa ;; row offset - source_offset_hi ;; offset within call data, high part - source_offset_lo ;; offset within call data, low part - size_hi ;; size of data to copy, high part - size_lo ;; size of data to copy, low part - return_data_size ;; return data size - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_RDC) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) source_offset_hi) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) source_offset_lo) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) size_hi) - (eq! (shift [ misc/OOB_DATA 4 ] kappa) size_lo) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) return_data_size) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - -(defun (set-OOB-instruction---deployment kappa ;; offset - code_size_hi ;; code size hi - code_size_lo ;; code size lo - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_DEPLOYMENT ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) code_size_hi) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) code_size_lo) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) ;; max code size exception - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---xcall kappa ;; offset - value_hi ;; value (high part) - value_lo ;; value (low part, stack argument of CALL-type instruction) - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_XCALL ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) value_hi ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) value_lo ) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) ;; value_is_nonzero - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) ;; value_is_zero ... I don't remember why I ask for both ... - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---call kappa ;; offset - value_hi ;; value (high part) - value_lo ;; value (low part, stack argument of CALL-type instruction) - balance ;; balance (from caller account) - call_stack_depth ;; call stack depth - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_CALL ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) value_hi ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) value_lo ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) balance ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 6 ] kappa) call_stack_depth) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) ;; value_is_nonzero - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) ;; aborting condition - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---create kappa ;; offset - value_hi ;; value (high part) - value_lo ;; value (low part, stack argument of CALL-type instruction) - balance ;; balance (from caller account) - nonce ;; callee's nonce - has_code ;; callee's HAS_CODE - call_stack_depth ;; current call stack depth - creator_nonce ;; creator account nonce - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_CREATE ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) value_hi ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) value_lo ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) balance ) - (eq! (shift [ misc/OOB_DATA 4 ] kappa) nonce ) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) has_code ) - (eq! (shift [ misc/OOB_DATA 6 ] kappa) call_stack_depth ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) ;; value_is_nonzero - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) ;; aborting condition - (eq! (shift [ misc/OOB_DATA 9 ] kappa) creator_nonce ) - )) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 9.4 MISC/OOB constraints: precompiles ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defun (set-OOB-instruction---common kappa ;; offset - common_precompile_oob_inst ;; relevant OOB instruction - call_gas ;; call gas i.e. gas provided to the precompile - cds ;; call data size - r@c ;; return at capacity - ) (begin - (eq! (shift misc/OOB_INST kappa) common_precompile_oob_inst ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) call_gas ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) cds ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) r@c ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---modexp-cds kappa ;; offset - cds ;; call data size - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_CDS ) - ;; (eq! (shift [ misc/OOB_DATA 1 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) cds ) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---modexp-xbs kappa ;; offset - xbs_hi ;; high part of some {b,e,m}bs - xbs_lo ;; low part of some {b,e,m}bs - ybs_lo ;; low part of some {b,e,m}bs - compute_max ;; bit indicating whether to compute max(xbs, ybs) or not - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_XBS ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) xbs_hi ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) xbs_lo ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) ybs_lo ) - (eq! (shift [ misc/OOB_DATA 4 ] kappa) compute_max ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---modexp-lead kappa ;; offset - bbs_lo ;; low part of bbs (base byte size) - cds ;; call data size - ebs_lo ;; low part of ebs (exponent byte size) - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_LEAD ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) bbs_lo ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) cds ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) ebs_lo ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---modexp-pricing kappa ;; offset - call_gas ;; call gas i.e. gas provided to the precompile - r@c ;; return at capacity - exponent_log ;; leading (≤) word log of exponent - max_mbs_bbs ;; call data size - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_PRICING ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) call_gas ) - ;; (eq! (shift [ misc/OOB_DATA 2 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) r@c ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 6 ] kappa) exponent_log ) - (eq! (shift [ misc/OOB_DATA 7 ] kappa) max_mbs_bbs ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---modexp-extract kappa ;; offset - cds ;; call data size - bbs_lo ;; low part of bbs (base byte size) - ebs_lo ;; low part of ebs (exponent byte size) - mbs_lo ;; low part of mbs (modulus byte size) - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_EXTRACT ) - ;; (eq! (shift [ misc/OOB_DATA 1 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) cds ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) bbs_lo ) - (eq! (shift [ misc/OOB_DATA 4 ] kappa) ebs_lo ) - (eq! (shift [ misc/OOB_DATA 5 ] kappa) mbs_lo ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---blake-cds kappa ;; offset - cds ;; call data size - r@c ;; return at capacity - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_BLAKE_CDS ) - ;; (eq! (shift [ misc/OOB_DATA 1 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 2 ] kappa) cds ) - (eq! (shift [ misc/OOB_DATA 3 ] kappa) r@c ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - -(defun (set-OOB-instruction---blake-params kappa ;; offset - call_gas ;; call gas i.e. gas provided to the precompile - blake_r ;; rounds parameter of the call data of BLAKE2f - blake_f ;; f parameter of the call data of BLAKE2f ("final block indicator") - ) (begin - (eq! (shift misc/OOB_INST kappa) OOB_INST_BLAKE_PARAMS ) - (eq! (shift [ misc/OOB_DATA 1 ] kappa) call_gas ) - ;; (eq! (shift [ misc/OOB_DATA 2 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) - (eq! (shift [ misc/OOB_DATA 6 ] kappa) blake_r ) - (eq! (shift [ misc/OOB_DATA 7 ] kappa) blake_f ) - ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) - ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) - )) - - - -;; (defun (set-OOB-instruction---Z kappa ;; offset -;; ) (begin -;; (eq! (shift misc/OOB_INST kappa) OOB_INST_ ) -;; ;; (eq! (shift [ misc/OOB_DATA 1 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 2 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 3 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 4 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 5 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 6 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 7 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 8 ] kappa) ) -;; ;; (eq! (shift [ misc/OOB_DATA 9 ] kappa) ) -;; )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_call.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_call.lisp new file mode 100644 index 00000000..a16638f6 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_call.lisp @@ -0,0 +1,21 @@ +(module hub) + + +(defun (set-OOB-instruction---call kappa ;; offset + value_hi ;; value (high part) + value_lo ;; value (low part, stack argument of CALL-type instruction) + balance ;; balance (from caller account) + call_stack_depth ;; call stack depth + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_CALL ) + (eq! (shift (misc_oob_data_1) kappa) value_hi ) + (eq! (shift (misc_oob_data_2) kappa) value_lo ) + (eq! (shift (misc_oob_data_3) kappa) balance ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + (eq! (shift (misc_oob_data_6) kappa) call_stack_depth) + ;; (eq! (shift (misc_oob_data_7) kappa) ) ;; value_is_nonzero + ;; (eq! (shift (misc_oob_data_8) kappa) ) ;; aborting condition + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_cdl.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_cdl.lisp new file mode 100644 index 00000000..ed3bcd5b --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_cdl.lisp @@ -0,0 +1,21 @@ +(module hub) + + +(defun (set-OOB-instruction---cdl kappa ;; row offset + offset_hi ;; offset within call data, high part + offset_lo ;; offset within call data, low part + call_data_size ;; call data size + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_CDL ) + (eq! (shift (misc_oob_data_1) kappa) offset_hi) + (eq! (shift (misc_oob_data_2) kappa) offset_lo) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + (eq! (shift (misc_oob_data_5) kappa) call_data_size) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) + diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_create.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_create.lisp new file mode 100644 index 00000000..db337c67 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_create.lisp @@ -0,0 +1,26 @@ +(module hub) + + +(defun (set-OOB-instruction---create kappa ;; offset + value_hi ;; value (high part) + value_lo ;; value (low part, stack argument of CALL-type instruction) + balance ;; balance (from caller account) + nonce ;; callee's nonce + has_code ;; callee's HAS_CODE + call_stack_depth ;; current call stack depth + creator_nonce ;; creator account nonce + ;; init_code_size ;; init code size (it's necessarily small at this point, so only low part required) + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_CREATE ) + (eq! (shift (misc_oob_data_1) kappa) value_hi ) + (eq! (shift (misc_oob_data_2) kappa) value_lo ) + (eq! (shift (misc_oob_data_3) kappa) balance ) + (eq! (shift (misc_oob_data_4) kappa) nonce ) + (eq! (shift (misc_oob_data_5) kappa) has_code ) + (eq! (shift (misc_oob_data_6) kappa) call_stack_depth ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) ;; value_is_nonzero + ;; (eq! (shift (misc_oob_data_8) kappa) ) ;; aborting condition + (eq! (shift (misc_oob_data_9) kappa) creator_nonce ) + ;; (eq! (shift (misc_oob_data_10) kappa) init_code_size ) ;; XXXXXX + )) + diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_deployment.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_deployment.lisp new file mode 100644 index 00000000..ce7c72a2 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_deployment.lisp @@ -0,0 +1,19 @@ +(module hub) + + +(defun (set-OOB-instruction---deployment kappa ;; offset + code_size_hi ;; code size hi + code_size_lo ;; code size lo + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_DEPLOYMENT ) + (eq! (shift (misc_oob_data_1) kappa) code_size_hi) + (eq! (shift (misc_oob_data_2) kappa) code_size_lo) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) ;; max code size exception + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jump.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jump.lisp new file mode 100644 index 00000000..069717f7 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jump.lisp @@ -0,0 +1,20 @@ +(module hub) + + +(defun (set-OOB-instruction---jump kappa ;; offset + pc_new_hi ;; high part of proposed new program counter + pc_new_lo ;; low part of proposed new program counter + code_size ;; code size of byte code currently executing + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_JUMP ) + (eq! (shift (misc_oob_data_1) kappa) pc_new_hi) + (eq! (shift (misc_oob_data_2) kappa) pc_new_lo) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + (eq! (shift (misc_oob_data_5) kappa) code_size) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jumpi.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jumpi.lisp new file mode 100644 index 00000000..598b7cbe --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_jumpi.lisp @@ -0,0 +1,22 @@ +(module hub) + + +(defun (set-OOB-instruction---jumpi kappa ;; offset + pc_new_hi ;; high part of proposed new program counter + pc_new_lo ;; low part of proposed new program counter + jump_condition_hi ;; high part of jump condition + jump_condition_lo ;; low part of jump condition + code_size ;; code size of byte code currently executing + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_JUMPI) + (eq! (shift (misc_oob_data_1) kappa) pc_new_hi) + (eq! (shift (misc_oob_data_2) kappa) pc_new_lo) + (eq! (shift (misc_oob_data_3) kappa) jump_condition_hi) + (eq! (shift (misc_oob_data_4) kappa) jump_condition_lo) + (eq! (shift (misc_oob_data_5) kappa) code_size) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_rdc.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_rdc.lisp new file mode 100644 index 00000000..5480ea7d --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_rdc.lisp @@ -0,0 +1,22 @@ +(module hub) + + +(defun (set-OOB-instruction---rdc kappa ;; row offset + source_offset_hi ;; offset within call data, high part + source_offset_lo ;; offset within call data, low part + size_hi ;; size of data to copy, high part + size_lo ;; size of data to copy, low part + return_data_size ;; return data size + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_RDC) + (eq! (shift (misc_oob_data_1) kappa) source_offset_hi) + (eq! (shift (misc_oob_data_2) kappa) source_offset_lo) + (eq! (shift (misc_oob_data_3) kappa) size_hi) + (eq! (shift (misc_oob_data_4) kappa) size_lo) + (eq! (shift (misc_oob_data_5) kappa) return_data_size) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_sstore.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_sstore.lisp new file mode 100644 index 00000000..63c9167b --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_sstore.lisp @@ -0,0 +1,18 @@ +(module hub) + + +(defun (set-OOB-instruction---sstore kappa ;; offset + gas_actual ;; GAS_ACTUAL + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_SSTORE ) + ;; (eq! (shift (misc_oob_data_1) kappa) ) + ;; (eq! (shift (misc_oob_data_2) kappa) ) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + (eq! (shift (misc_oob_data_5) kappa) gas_actual) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcall.lisp b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcall.lisp new file mode 100644 index 00000000..7789b037 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcall.lisp @@ -0,0 +1,19 @@ +(module hub) + + +(defun (set-OOB-instruction---xcall kappa ;; offset + value_hi ;; value (high part) + value_lo ;; value (low part, stack argument of CALL-type instruction) + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_XCALL ) + (eq! (shift (misc_oob_data_1) kappa) value_hi ) + (eq! (shift (misc_oob_data_2) kappa) value_lo ) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) ;; value_is_nonzero + ;; (eq! (shift (misc_oob_data_8) kappa) ) ;; value_is_zero ... I don't remember why I ask for both ... + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcreate.lispX b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcreate.lispX new file mode 100644 index 00000000..4b68440d --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/opcodes/oob_inst_xcreate.lispX @@ -0,0 +1,22 @@ +(module hub) + + +;; XXXXXX has to be uncommented (lispX -> lisp) + + +(defun (set-OOB-instruction---xcreate kappa ;; offset + init_code_size_hi ;; high part of initialization code size argument of CREATE(2) + init_code_size_lo ;; low part of initialization code size argument of CREATE(2) + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_XCREATE ) + (eq! (shift (misc_oob_data_1) kappa) init_code_size_hi ) + (eq! (shift (misc_oob_data_2) kappa) init_code_size_lo ) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) ;; value_is_nonzero + ;; (eq! (shift (misc_oob_data_8) kappa) ) ;; value_is_zero ... I don't remember why I ask for both ... + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_cds.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_cds.lisp new file mode 100644 index 00000000..d14763fd --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_cds.lisp @@ -0,0 +1,19 @@ +(module hub) + + +(defun (set-OOB-instruction---blake-cds kappa ;; offset + cds ;; call data size + r@c ;; return at capacity + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_BLAKE_CDS ) + ;; (eq! (shift (misc_oob_data_1) kappa) ) + (eq! (shift (misc_oob_data_2) kappa) cds ) + (eq! (shift (misc_oob_data_3) kappa) r@c ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_params.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_params.lisp new file mode 100644 index 00000000..0f8d5f17 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/blake/oob_inst_blake_params.lisp @@ -0,0 +1,20 @@ +(module hub) + + +(defun (set-OOB-instruction---blake-params kappa ;; offset + call_gas ;; call gas i.e. gas provided to the precompile + blake_r ;; rounds parameter of the call data of BLAKE2f + blake_f ;; f parameter of the call data of BLAKE2f ("final block indicator") + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_BLAKE_PARAMS ) + (eq! (shift (misc_oob_data_1) kappa) call_gas ) + ;; (eq! (shift (misc_oob_data_2) kappa) ) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + (eq! (shift (misc_oob_data_6) kappa) blake_r ) + (eq! (shift (misc_oob_data_7) kappa) blake_f ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/common/common.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/common/common.lisp new file mode 100644 index 00000000..ef650d51 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/common/common.lisp @@ -0,0 +1,22 @@ +(module hub) + + +;; note that the instruction is part of the interface ! +(defun (set-OOB-instruction---common kappa ;; offset + common_precompile_oob_inst ;; relevant OOB instruction + call_gas ;; call gas i.e. gas provided to the precompile + cds ;; call data size + r@c ;; return at capacity + ) (begin + (eq! (shift misc/OOB_INST kappa) common_precompile_oob_inst ) + (eq! (shift (misc_oob_data_1) kappa) call_gas ) + (eq! (shift (misc_oob_data_2) kappa) cds ) + (eq! (shift (misc_oob_data_3) kappa) r@c ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_cds.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_cds.lisp new file mode 100644 index 00000000..92de3895 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_cds.lisp @@ -0,0 +1,18 @@ +(module hub) + + +(defun (set-OOB-instruction---modexp-cds kappa ;; offset + cds ;; call data size + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_CDS ) + ;; (eq! (shift (misc_oob_data_1) kappa) ) + (eq! (shift (misc_oob_data_2) kappa) cds ) + ;; (eq! (shift (misc_oob_data_3) kappa) ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_extract.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_extract.lisp new file mode 100644 index 00000000..b50442ca --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_extract.lisp @@ -0,0 +1,21 @@ +(module hub) + + +(defun (set-OOB-instruction---modexp-extract kappa ;; offset + cds ;; call data size + bbs_lo ;; low part of bbs (base byte size) + ebs_lo ;; low part of ebs (exponent byte size) + mbs_lo ;; low part of mbs (modulus byte size) + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_EXTRACT ) + ;; (eq! (shift (misc_oob_data_1) kappa) ) + (eq! (shift (misc_oob_data_2) kappa) cds ) + (eq! (shift (misc_oob_data_3) kappa) bbs_lo ) + (eq! (shift (misc_oob_data_4) kappa) ebs_lo ) + (eq! (shift (misc_oob_data_5) kappa) mbs_lo ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_lead.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_lead.lisp new file mode 100644 index 00000000..53c0222a --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_lead.lisp @@ -0,0 +1,20 @@ +(module hub) + + +(defun (set-OOB-instruction---modexp-lead kappa ;; offset + bbs_lo ;; low part of bbs (base byte size) + cds ;; call data size + ebs_lo ;; low part of ebs (exponent byte size) + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_LEAD ) + (eq! (shift (misc_oob_data_1) kappa) bbs_lo ) + (eq! (shift (misc_oob_data_2) kappa) cds ) + (eq! (shift (misc_oob_data_3) kappa) ebs_lo ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_pricing.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_pricing.lisp new file mode 100644 index 00000000..58b6ab81 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_pricing.lisp @@ -0,0 +1,21 @@ +(module hub) + + +(defun (set-OOB-instruction---modexp-pricing kappa ;; offset + call_gas ;; call gas i.e. gas provided to the precompile + r@c ;; return at capacity + exponent_log ;; leading (≤) word log of exponent + max_mbs_bbs ;; call data size + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_PRICING ) + (eq! (shift (misc_oob_data_1) kappa) call_gas ) + ;; (eq! (shift (misc_oob_data_2) kappa) ) + (eq! (shift (misc_oob_data_3) kappa) r@c ) + ;; (eq! (shift (misc_oob_data_4) kappa) ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + (eq! (shift (misc_oob_data_6) kappa) exponent_log ) + (eq! (shift (misc_oob_data_7) kappa) max_mbs_bbs ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_xbs.lisp b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_xbs.lisp new file mode 100644 index 00000000..57fcb723 --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/precompiles/modexp/oob_inst_modexp_xbs.lisp @@ -0,0 +1,21 @@ +(module hub) + + +(defun (set-OOB-instruction---modexp-xbs kappa ;; offset + xbs_hi ;; high part of some {b,e,m}bs + xbs_lo ;; low part of some {b,e,m}bs + ybs_lo ;; low part of some {b,e,m}bs + compute_max ;; bit indicating whether to compute max(xbs, ybs) or not + ) (begin + (eq! (shift misc/OOB_INST kappa) OOB_INST_MODEXP_XBS ) + (eq! (shift (misc_oob_data_1) kappa) xbs_hi ) + (eq! (shift (misc_oob_data_2) kappa) xbs_lo ) + (eq! (shift (misc_oob_data_3) kappa) ybs_lo ) + (eq! (shift (misc_oob_data_4) kappa) compute_max ) + ;; (eq! (shift (misc_oob_data_5) kappa) ) + ;; (eq! (shift (misc_oob_data_6) kappa) ) + ;; (eq! (shift (misc_oob_data_7) kappa) ) + ;; (eq! (shift (misc_oob_data_8) kappa) ) + ;; (eq! (shift (misc_oob_data_9) kappa) ) + ;; (eq! (shift (misc_oob_data_10) kappa) ) + )) diff --git a/hub/constraints/miscellaneous-rows/oob/shorthands.lisp b/hub/constraints/miscellaneous-rows/oob/shorthands.lisp new file mode 100644 index 00000000..7751702e --- /dev/null +++ b/hub/constraints/miscellaneous-rows/oob/shorthands.lisp @@ -0,0 +1,12 @@ +(module hub) + +(defun (misc_oob_data_1) [ misc/OOB_DATA 1 ]) +(defun (misc_oob_data_2) [ misc/OOB_DATA 2 ]) +(defun (misc_oob_data_3) [ misc/OOB_DATA 3 ]) +(defun (misc_oob_data_4) [ misc/OOB_DATA 4 ]) +(defun (misc_oob_data_5) [ misc/OOB_DATA 5 ]) +(defun (misc_oob_data_6) [ misc/OOB_DATA 6 ]) +(defun (misc_oob_data_7) [ misc/OOB_DATA 7 ]) +(defun (misc_oob_data_8) [ misc/OOB_DATA 8 ]) +(defun (misc_oob_data_9) [ misc/OOB_DATA 9 ]) +;; (defun (misc_oob_data_10) [ misc/OOB_DATA 10 ]) ;; XXXXXX From ccf8a8749f7abf7fd276b02568a6c10d42f72ce5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bojarski?= <54240434+letypequividelespoubelles@users.noreply.github.com> Date: Mon, 14 Apr 2025 10:35:56 +0200 Subject: [PATCH 07/11] add PUSH0 constant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: François Bojarski <54240434+letypequividelespoubelles@users.noreply.github.com> --- constants/constants.lisp | 1 + 1 file changed, 1 insertion(+) diff --git a/constants/constants.lisp b/constants/constants.lisp index c7e8d426..07bb57c9 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -75,6 +75,7 @@ EVM_INST_GAS 0x5A EVM_INST_JUMPDEST 0x5B ;; Push Operations + EVM_INST_PUSH0 0x5F ;; post Shanghai EVM_INST_PUSH1 0x60 EVM_INST_PUSH2 0x61 EVM_INST_PUSH3 0x62 From 445209f0ad75d5b29b7e6924508dd2579a42508a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bojarski?= <54240434+letypequividelespoubelles@users.noreply.github.com> Date: Mon, 14 Apr 2025 10:48:13 +0200 Subject: [PATCH 08/11] add EIP-3860 constants MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: François Bojarski <54240434+letypequividelespoubelles@users.noreply.github.com> --- constants/constants.lisp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/constants/constants.lisp b/constants/constants.lisp index 07bb57c9..f214efd8 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -212,12 +212,14 @@ GAS_CONST_ECPAIRING 45000 GAS_CONST_ECPAIRING_PAIR 34000 GAS_CONST_BLAKE2_PER_ROUND 1 + GAS_CONST_INIT_CODE_WORD 2 ;; post Shanghai EIP-3860 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM MISC ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; MAX_CODE_SIZE 24576 + MAX_INIT_CODE_SIZE (* MAX_CODE_SIZE 2) EIP_3541_MARKER 0xEF BLOCKHASH_MAX_HISTORY 256 MAX_REFUND_QUOTIENT 5 @@ -399,6 +401,7 @@ OOB_INST_CDL 0x35 OOB_INST_XCALL 0xCC OOB_INST_CALL 0xCA + OOB_INST_XCREATE 0xCD OOB_INST_CREATE 0xCE OOB_INST_SSTORE 0x55 OOB_INST_DEPLOYMENT 0xF3 From e35f3542b8280aae54cd1395084bcd3e0949ce3e Mon Sep 17 00:00:00 2001 From: F Bojarski Date: Thu, 24 Apr 2025 21:35:53 +0200 Subject: [PATCH 09/11] feat: columns and constant of SHANGHAI Signed-off-by: F Bojarski --- hub/columns/miscellaneous.lisp | 2 +- oob/columns.lisp | 4 ++-- oob/constants.lisp | 5 ++++- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/hub/columns/miscellaneous.lisp b/hub/columns/miscellaneous.lisp index 89de38a8..fe13a950 100644 --- a/hub/columns/miscellaneous.lisp +++ b/hub/columns/miscellaneous.lisp @@ -53,7 +53,7 @@ ;; OOB columns (OOB_INST :i16 ) - (OOB_DATA :array[1:9] :i128 ) ;; XXXXXX 9 -> 10 + (OOB_DATA :array[1:10] :i128 ) ;; TODO: only 9 for LONDON ;; STP columns ( STP_INSTRUCTION :byte ) diff --git a/oob/columns.lisp b/oob/columns.lisp index 88e554e6..f612790a 100644 --- a/oob/columns.lisp +++ b/oob/columns.lisp @@ -4,7 +4,7 @@ (STAMP :i32) (CT :i3) (CT_MAX :i3) - (DATA :i128 :array [9]) ;; XXXXXX 9 -> 10 + (DATA :i128 :array [10]) ;; TODO: only 9 for LONDON (OOB_INST :i16) (IS_JUMP :binary@prove) (IS_JUMPI :binary@prove) @@ -12,7 +12,7 @@ (IS_CDL :binary@prove) (IS_XCALL :binary@prove) (IS_CALL :binary@prove) - ;; (IS_XCREATE :binary@prove) ;; XXXXXX + (IS_XCREATE :binary@prove) ;; TODO: not in LONDON (IS_CREATE :binary@prove) (IS_SSTORE :binary@prove) (IS_DEPLOYMENT :binary@prove) diff --git a/oob/constants.lisp b/oob/constants.lisp index 06e82624..b0b47806 100644 --- a/oob/constants.lisp +++ b/oob/constants.lisp @@ -7,7 +7,10 @@ CT_MAX_CDL 0 CT_MAX_XCALL 0 CT_MAX_CALL 2 - CT_MAX_CREATE 3 + CT_MAX_XCREATE 0 + CT_MAX_CREATE_LONDON 3 + CT_MAX_CREATE_SHANGHAI 4 + CT_MAX_CREATE 3 ;;TODO fix me CT_MAX_SSTORE 0 CT_MAX_DEPLOYMENT 0 CT_MAX_ECRECOVER 2 From cbc6bcb139a499d1828422d1841566e32dfb9c1b Mon Sep 17 00:00:00 2001 From: David Pearce Date: Mon, 28 Apr 2025 20:06:32 +1200 Subject: [PATCH 10/11] feat: upgrade go corset to v11 (#636) This updates `go-corset` to the latest release which removes the notion of loobean, and replaces it with a clear distinction between logical conditions and integer values. In particular, this adds the operators `==` and `!=` along with true notions of logical or and logical and. This also includes relational operators (e.g. `<` and `<=`) which can be used in constrant expresions (only). --- .github/workflows/check.yml | 2 +- bin/constraints.lisp | 5 ----- .../instruction-handling/halting/revert.lisp | 19 +++++++++++-------- loginfo/constraints.lisp | 4 ---- mxp/constraints.lisp | 13 ++++++++----- rlpaddr/constraints.lisp | 7 +++---- rlptxn/constraints.lisp | 8 +++++--- rlptxrcpt/constraints.lisp | 12 +++++------- stp/constraints.lisp | 2 +- txndata/constraints.lisp | 5 ----- 10 files changed, 34 insertions(+), 43 deletions(-) diff --git a/.github/workflows/check.yml b/.github/workflows/check.yml index 8db71476..5bcdc0ac 100644 --- a/.github/workflows/check.yml +++ b/.github/workflows/check.yml @@ -15,7 +15,7 @@ jobs: - name: Install Go Corset shell: bash - run: go install github.com/consensys/go-corset/cmd/go-corset@v1.0.7 + run: go install github.com/consensys/go-corset/cmd/go-corset@v1.1.1 - name: Build Constraints run: make -B zkevm.bin diff --git a/bin/constraints.lisp b/bin/constraints.lisp index 6c1eaf08..6ab07f7f 100644 --- a/bin/constraints.lisp +++ b/bin/constraints.lisp @@ -1,10 +1,5 @@ (module bin) -(defpurefun (if-eq-else A B THEN ELSE) - (if-zero (- A B) - THEN - ELSE)) - ;; 2.2 Shorthands (defun (flag-sum) (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND)) diff --git a/hub/constraints/instruction-handling/halting/revert.lisp b/hub/constraints/instruction-handling/halting/revert.lisp index 180b0d38..bca41995 100644 --- a/hub/constraints/instruction-handling/halting/revert.lisp +++ b/hub/constraints/instruction-handling/halting/revert.lisp @@ -91,15 +91,18 @@ (revert-instruction---type-safe-return-data-size) ;; type safe rds ))) -(defun (revert-instruction---trigger_MMU) (* (- 1 XAHOY) - (- 1 (revert-instruction---current-context-is-root)) - (is-not-zero (* (revert-instruction---size-lo) - (revert-instruction---r@c))))) - (defconstraint revert-instruction---setting-the-miscellaneous-row-module-flags (:guard (revert-instruction---standard-precondition)) - (eq! (weighted-MISC-flag-sum ROFF_REVERT___MISC_ROW) - (+ MISC_WEIGHT_MXP - (* MISC_WEIGHT_MMU (revert-instruction---trigger_MMU))))) + (let ((FLAG (weighted-MISC-flag-sum ROFF_REVERT___MISC_ROW))) + ;; + (if (or! + (eq! XAHOY 1) + (eq! (revert-instruction---current-context-is-root) 1) + (eq! (revert-instruction---size-lo) 0) + (eq! (revert-instruction---r@c) 0)) + ;; trigger_MMU == 0 + (eq! FLAG MISC_WEIGHT_MXP) + ;; trigger_MMU == 1 + (eq! FLAG (+ MISC_WEIGHT_MXP MISC_WEIGHT_MMU))))) (defconstraint revert-instruction---setting-the-MXP-data (:guard (revert-instruction---standard-precondition)) (set-MXP-instruction-type-4 ROFF_REVERT___MISC_ROW ;; row offset kappa diff --git a/loginfo/constraints.lisp b/loginfo/constraints.lisp index ef409257..d6df220c 100644 --- a/loginfo/constraints.lisp +++ b/loginfo/constraints.lisp @@ -1,9 +1,5 @@ (module loginfo) -(defun (if-not-eq A B then) - (if-not-zero (- A B) - then)) - ;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 2.1 Heartbeat ;; diff --git a/mxp/constraints.lisp b/mxp/constraints.lisp index 68c2791a..d729521c 100644 --- a/mxp/constraints.lisp +++ b/mxp/constraints.lisp @@ -90,10 +90,13 @@ (begin (if-not-zero (+ [MXP_TYPE 1] [MXP_TYPE 2] [MXP_TYPE 3]) (eq! NOOP [MXP_TYPE 1])) (if-eq [MXP_TYPE 4] 1 - (eq! NOOP (is-zero SIZE_1_LO))) + (if (eq! SIZE_1_LO 0) + (eq! NOOP 1) + (eq! NOOP 0))) (if-eq [MXP_TYPE 5] 1 - (eq! NOOP - (* (is-zero SIZE_1_LO) (is-zero SIZE_2_LO))))))) + (if (and! (eq! SIZE_1_LO 0) (eq! SIZE_2_LO 0)) + (eq! NOOP 1) + (eq! NOOP 0)))))) (defconstraint noop-consequences (:guard NOOP) (begin (vanishes! QUAD_COST) @@ -273,8 +276,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun (offsets-are-in-bounds) - (* (is-zero (- CT CT_MAX_NON_TRIVIAL)) - (- 1 MXPX))) + (if (eq! CT CT_MAX_NON_TRIVIAL) + (- 1 MXPX) 0)) (defconstraint size-in-evm-words (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) (if-eq [MXP_TYPE 4] 1 diff --git a/rlpaddr/constraints.lisp b/rlpaddr/constraints.lisp index 422ef8f7..c1fa3002 100644 --- a/rlpaddr/constraints.lisp +++ b/rlpaddr/constraints.lisp @@ -132,10 +132,9 @@ (begin (vanishes! (shift INDEX -7)) (eq! ACC NONCE) (eq! BIT_ACC BYTE1) - (if-zero (+ (~ (eq! ACC_BYTESIZE 1)) - (shift BIT1 -7)) - (eq! 1 TINY_NON_ZERO_NONCE) - (vanishes! TINY_NON_ZERO_NONCE)) + (if (and! (eq! ACC_BYTESIZE 1) (eq! (shift BIT1 -7) 0)) + (eq! 1 TINY_NON_ZERO_NONCE) + (vanishes! TINY_NON_ZERO_NONCE)) (eq! (+ (shift LC -4) (shift LC -3)) 1) (eq! (shift LIMB -3) diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index 330b3926..1e756e9a 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -147,9 +147,11 @@ ;; 2.3.2.4 (defconstraint ABS_TX_NUM-evolution () - (eq! ABS_TX_NUM - (+ (prev ABS_TX_NUM) - (* IS_PHASE_RLP_PREFIX (remained-constant! IS_PHASE_RLP_PREFIX))))) + (if (or! (eq! IS_PHASE_RLP_PREFIX 0) (remained-constant! IS_PHASE_RLP_PREFIX)) + ;; no change + (remained-constant! ABS_TX_NUM) + ;; increment + (did-inc! ABS_TX_NUM 1))) (defconstraint set-to-hash-by-prover-flag () (eq! TO_HASH_BY_PROVER (* LC LX))) diff --git a/rlptxrcpt/constraints.lisp b/rlptxrcpt/constraints.lisp index 3308fe77..23ab2dec 100644 --- a/rlptxrcpt/constraints.lisp +++ b/rlptxrcpt/constraints.lisp @@ -1,9 +1,5 @@ (module rlptxrcpt) -(defpurefun (if-not-eq x y then) - (if-not-zero (- x y) - then)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 4.1 Global Constraints ;; @@ -96,9 +92,11 @@ (reduce + (for i [5] [PHASE i]))))) (defconstraint ABS_TX_NUM-evolution () - (eq! ABS_TX_NUM - (+ (prev ABS_TX_NUM) - (* [PHASE 1] (remained-constant! [PHASE 1]))))) + (if (or! (eq! [PHASE 1] 0) (remained-constant! [PHASE 1])) + ;; no change + (remained-constant! ABS_TX_NUM) + ;; increment + (did-inc! ABS_TX_NUM 1))) (defconstraint ABS_LOG_NUM-evolution () (if-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT) diff --git a/stp/constraints.lisp b/stp/constraints.lisp index be3e08ad..59d446a6 100644 --- a/stp/constraints.lisp +++ b/stp/constraints.lisp @@ -192,7 +192,7 @@ ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun (call---first-row-common) (* (remained-constant! STAMP) (is_call))) +(defun (call---first-row-common) (* (remained-constant STAMP) (is_call))) (defun (call---first-row-unexceptional) (* (call---first-row-common) (- 1 OOGX))) diff --git a/txndata/constraints.lisp b/txndata/constraints.lisp index 225a9e9a..e71fcb94 100644 --- a/txndata/constraints.lisp +++ b/txndata/constraints.lisp @@ -1,10 +1,5 @@ (module txndata) -(defpurefun (if-not-eq A B then else) - (if-not-zero (- A B) - then - else)) - ;; sum of transaction type flags (defun (tx-type-sum) (force-bin (+ TYPE0 TYPE1 From 6680744a6ff95cb0790b2708ab1933181535bf9a Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 29 Apr 2025 09:36:08 +1200 Subject: [PATCH 11/11] add notion of EVM fork This adds the concept of an EVM fork to the set of available constants, such that it can be used subsequently to allow fork-dependent constraints, etc. --- constants/constants.lisp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/constants/constants.lisp b/constants/constants.lisp index f214efd8..7ec3562e 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -1,4 +1,15 @@ (defconst + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM Forks ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + EVM_LONDON_FORK 14 + EVM_PARIS (+ 2 EVM_LONDON_FORK) + EVM_SHANGHAI (+ 2 EVM_LONDON_FORK) + EVM_CANCUN (+ 3 EVM_LONDON_FORK) + ;; Default fork + (EVM_FORK :i8 :extern) EVM_LONDON_FORK ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EVM INSTRUCTIONS ;;