Skip to content

Commit cbc6bcb

Browse files
DavePearceDavePearce
authored
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).
1 parent e35f354 commit cbc6bcb

File tree

10 files changed

+34
-43
lines changed

10 files changed

+34
-43
lines changed

‎.github/workflows/check.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ jobs:
1515

1616
- name: Install Go Corset
1717
shell: bash
18-
run: go install github.com/consensys/go-corset/cmd/go-corset@v1.0.7
18+
run: go install github.com/consensys/go-corset/cmd/go-corset@v1.1.1
1919

2020
- name: Build Constraints
2121
run: make -B zkevm.bin

‎bin/constraints.lisp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
(module bin)
22

3-
(defpurefun (if-eq-else A B THEN ELSE)
4-
(if-zero (- A B)
5-
THEN
6-
ELSE))
7-
83
;; 2.2 Shorthands
94
(defun (flag-sum)
105
(+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND))

‎hub/constraints/instruction-handling/halting/revert.lisp

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -91,15 +91,18 @@
9191
(revert-instruction---type-safe-return-data-size) ;; type safe rds
9292
)))
9393

94-
(defun (revert-instruction---trigger_MMU) (* (- 1 XAHOY)
95-
(- 1 (revert-instruction---current-context-is-root))
96-
(is-not-zero (* (revert-instruction---size-lo)
97-
(revert-instruction---r@c)))))
98-
9994
(defconstraint revert-instruction---setting-the-miscellaneous-row-module-flags (:guard (revert-instruction---standard-precondition))
100-
(eq! (weighted-MISC-flag-sum ROFF_REVERT___MISC_ROW)
101-
(+ MISC_WEIGHT_MXP
102-
(* MISC_WEIGHT_MMU (revert-instruction---trigger_MMU)))))
95+
(let ((FLAG (weighted-MISC-flag-sum ROFF_REVERT___MISC_ROW)))
96+
;;
97+
(if (or!
98+
(eq! XAHOY 1)
99+
(eq! (revert-instruction---current-context-is-root) 1)
100+
(eq! (revert-instruction---size-lo) 0)
101+
(eq! (revert-instruction---r@c) 0))
102+
;; trigger_MMU == 0
103+
(eq! FLAG MISC_WEIGHT_MXP)
104+
;; trigger_MMU == 1
105+
(eq! FLAG (+ MISC_WEIGHT_MXP MISC_WEIGHT_MMU)))))
103106

104107
(defconstraint revert-instruction---setting-the-MXP-data (:guard (revert-instruction---standard-precondition))
105108
(set-MXP-instruction-type-4 ROFF_REVERT___MISC_ROW ;; row offset kappa

‎loginfo/constraints.lisp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,5 @@
11
(module loginfo)
22

3-
(defun (if-not-eq A B then)
4-
(if-not-zero (- A B)
5-
then))
6-
73
;;;;;;;;;;;;;;;;;;;;;;;;;
84
;; ;;
95
;; 2.1 Heartbeat ;;

‎mxp/constraints.lisp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -90,10 +90,13 @@
9090
(begin (if-not-zero (+ [MXP_TYPE 1] [MXP_TYPE 2] [MXP_TYPE 3])
9191
(eq! NOOP [MXP_TYPE 1]))
9292
(if-eq [MXP_TYPE 4] 1
93-
(eq! NOOP (is-zero SIZE_1_LO)))
93+
(if (eq! SIZE_1_LO 0)
94+
(eq! NOOP 1)
95+
(eq! NOOP 0)))
9496
(if-eq [MXP_TYPE 5] 1
95-
(eq! NOOP
96-
(* (is-zero SIZE_1_LO) (is-zero SIZE_2_LO)))))))
97+
(if (and! (eq! SIZE_1_LO 0) (eq! SIZE_2_LO 0))
98+
(eq! NOOP 1)
99+
(eq! NOOP 0))))))
97100

98101
(defconstraint noop-consequences (:guard NOOP)
99102
(begin (vanishes! QUAD_COST)
@@ -273,8 +276,8 @@
273276
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
274277

275278
(defun (offsets-are-in-bounds)
276-
(* (is-zero (- CT CT_MAX_NON_TRIVIAL))
277-
(- 1 MXPX)))
279+
(if (eq! CT CT_MAX_NON_TRIVIAL)
280+
(- 1 MXPX) 0))
278281

279282
(defconstraint size-in-evm-words (:guard (* (standing-hypothesis) (offsets-are-in-bounds)))
280283
(if-eq [MXP_TYPE 4] 1

‎rlpaddr/constraints.lisp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -132,10 +132,9 @@
132132
(begin (vanishes! (shift INDEX -7))
133133
(eq! ACC NONCE)
134134
(eq! BIT_ACC BYTE1)
135-
(if-zero (+ (~ (eq! ACC_BYTESIZE 1))
136-
(shift BIT1 -7))
137-
(eq! 1 TINY_NON_ZERO_NONCE)
138-
(vanishes! TINY_NON_ZERO_NONCE))
135+
(if (and! (eq! ACC_BYTESIZE 1) (eq! (shift BIT1 -7) 0))
136+
(eq! 1 TINY_NON_ZERO_NONCE)
137+
(vanishes! TINY_NON_ZERO_NONCE))
139138
(eq! (+ (shift LC -4) (shift LC -3))
140139
1)
141140
(eq! (shift LIMB -3)

‎rlptxn/constraints.lisp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -147,9 +147,11 @@
147147

148148
;; 2.3.2.4
149149
(defconstraint ABS_TX_NUM-evolution ()
150-
(eq! ABS_TX_NUM
151-
(+ (prev ABS_TX_NUM)
152-
(* IS_PHASE_RLP_PREFIX (remained-constant! IS_PHASE_RLP_PREFIX)))))
150+
(if (or! (eq! IS_PHASE_RLP_PREFIX 0) (remained-constant! IS_PHASE_RLP_PREFIX))
151+
;; no change
152+
(remained-constant! ABS_TX_NUM)
153+
;; increment
154+
(did-inc! ABS_TX_NUM 1)))
153155

154156
(defconstraint set-to-hash-by-prover-flag ()
155157
(eq! TO_HASH_BY_PROVER (* LC LX)))

‎rlptxrcpt/constraints.lisp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,5 @@
11
(module rlptxrcpt)
22

3-
(defpurefun (if-not-eq x y then)
4-
(if-not-zero (- x y)
5-
then))
6-
73
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
84
;; ;;
95
;; 4.1 Global Constraints ;;
@@ -96,9 +92,11 @@
9692
(reduce + (for i [5] [PHASE i])))))
9793

9894
(defconstraint ABS_TX_NUM-evolution ()
99-
(eq! ABS_TX_NUM
100-
(+ (prev ABS_TX_NUM)
101-
(* [PHASE 1] (remained-constant! [PHASE 1])))))
95+
(if (or! (eq! [PHASE 1] 0) (remained-constant! [PHASE 1]))
96+
;; no change
97+
(remained-constant! ABS_TX_NUM)
98+
;; increment
99+
(did-inc! ABS_TX_NUM 1)))
102100

103101
(defconstraint ABS_LOG_NUM-evolution ()
104102
(if-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT)

‎stp/constraints.lisp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@
192192
;; ;;
193193
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
194194

195-
(defun (call---first-row-common) (* (remained-constant! STAMP) (is_call)))
195+
(defun (call---first-row-common) (* (remained-constant STAMP) (is_call)))
196196
(defun (call---first-row-unexceptional) (* (call---first-row-common) (- 1 OOGX)))
197197

198198

‎txndata/constraints.lisp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
(module txndata)
22

3-
(defpurefun (if-not-eq A B then else)
4-
(if-not-zero (- A B)
5-
then
6-
else))
7-
83
;; sum of transaction type flags
94
(defun (tx-type-sum) (force-bin (+ TYPE0
105
TYPE1

0 commit comments

Comments
 (0)