From 648230dd94e6e57f9a3de600f67fa630e2ff4ebb Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Thu, 26 Sep 2024 10:26:54 +0530 Subject: [PATCH 1/4] fix(rlpTxn): constraint ADDR during AccessList tuple Signed-off-by: Francois Bojarski --- rlptxn/constraints.lisp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index c7b1b0c5..155e1a36 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -690,11 +690,11 @@ (eq! (next DATA_GAS_COST) (shift DATA_GAS_COST 2))) (vanishes! (next LC_CORRECTION)))))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; ;; 4.5 Phase 10 : AccessList ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defconstraint phaseAccessList-stillphase-noend (:guard IS_PHASE_ACCESS_LIST) (if-not-zero PHASE_SIZE (vanishes! PHASE_END))) @@ -829,10 +829,9 @@ ;; 4.5.2.15 (defconstraint phaseAccessList-updateAddrLookUp (:guard IS_PHASE_ACCESS_LIST) - (if-zero (+ [DEPTH 2] - (- (prev nADDR) nADDR)) - (begin (remained-constant! ADDR_HI) - (remained-constant! ADDR_LO)))) + (if-not-zero (* [DEPTH 1] (- nADDR (- (prev nADDR) 1))) + (begin (remained-constant! ADDR_HI) + (remained-constant! ADDR_LO)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; From 92e53664b93fa400236ad78347ca2d60ba978017 Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Fri, 27 Sep 2024 10:19:04 +0530 Subject: [PATCH 2/4] add chainId constraint Signed-off-by: Francois Bojarski --- rlptxn/constants.lisp | 9 +++++++++ rlptxn/constraints.lisp | 19 ++++++++++++++----- 2 files changed, 23 insertions(+), 5 deletions(-) create mode 100644 rlptxn/constants.lisp diff --git a/rlptxn/constants.lisp b/rlptxn/constants.lisp new file mode 100644 index 00000000..5e39c1ec --- /dev/null +++ b/rlptxn/constants.lisp @@ -0,0 +1,9 @@ +(module rlptxn) + +(defconst + UNPROTECTED_V 27 + UNPROTECTED_V_PO (+ UNPROTECTED_V 1) + PROTECTED_BASE_V 35 + PROTECTED_BASE_V_PO (+ PROTECTED_BASE_V 1)) + + diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index 155e1a36..54633fdc 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -829,9 +829,11 @@ ;; 4.5.2.15 (defconstraint phaseAccessList-updateAddrLookUp (:guard IS_PHASE_ACCESS_LIST) - (if-not-zero (* [DEPTH 1] (- nADDR (- (prev nADDR) 1))) - (begin (remained-constant! ADDR_HI) - (remained-constant! ADDR_LO)))) + (if-not-zero (* [DEPTH 1] + (- nADDR + (- (prev nADDR) 1))) + (begin (remained-constant! ADDR_HI) + (remained-constant! ADDR_LO)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; @@ -844,7 +846,12 @@ (eq! nSTEP 8)))) (defun (w-minus-two-seven) - (- [INPUT 1] 27)) + (- [INPUT 1] PROTECTED_BASE_V)) + +(defun (w-minus-two-beta-minus-protected-base-V) + (- [INPUT 1] + (+ (* 2 (next [INPUT 1])) + PROTECTED_BASE_V))) (defconstraint phaseBeta-rlp-w (:guard IS_PHASE_BETA) (if-not-zero (* LT (- 1 LX)) @@ -857,7 +864,9 @@ (begin (vanishes! (+ PHASE_END (next LT) (- 1 (next LX)) - (- 1 (next IS_PREFIX))))))))))) + (- 1 (next IS_PREFIX)))) + (eq! (^ (w-minus-two-beta-minus-protected-base-V) 2) + (w-minus-two-beta-minus-protected-base-V))))))))) (defconstraint phaseBeta-rlp-beta (:guard IS_PHASE_BETA) (if-not-zero (* LX IS_PREFIX) From 85c30fe7995554768586e5bcfe8d3128ec29508e Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Fri, 27 Sep 2024 12:08:38 +0530 Subject: [PATCH 3/4] fix typo Signed-off-by: Francois Bojarski --- rlptxn/constraints.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index 54633fdc..6fd7d61a 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -846,7 +846,7 @@ (eq! nSTEP 8)))) (defun (w-minus-two-seven) - (- [INPUT 1] PROTECTED_BASE_V)) + (- [INPUT 1] UNPROTECTED_V)) (defun (w-minus-two-beta-minus-protected-base-V) (- [INPUT 1] From 50be4837b0a80002044f1441b002fe8665fb438f Mon Sep 17 00:00:00 2001 From: Francois Bojarski Date: Fri, 27 Sep 2024 12:32:50 +0530 Subject: [PATCH 4/4] style Signed-off-by: Francois Bojarski --- rlptxn/constraints.lisp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/rlptxn/constraints.lisp b/rlptxn/constraints.lisp index 6fd7d61a..7e39c531 100644 --- a/rlptxn/constraints.lisp +++ b/rlptxn/constraints.lisp @@ -865,8 +865,7 @@ (next LT) (- 1 (next LX)) (- 1 (next IS_PREFIX)))) - (eq! (^ (w-minus-two-beta-minus-protected-base-V) 2) - (w-minus-two-beta-minus-protected-base-V))))))))) + (is-binary (w-minus-two-beta-minus-protected-base-V))))))))) (defconstraint phaseBeta-rlp-beta (:guard IS_PHASE_BETA) (if-not-zero (* LX IS_PREFIX)