Skip to content

Commit 19f9411

Browse files
letypequividelespoubellesletypequividelespoubelles
committed
eip-7642: rm bloom filter from tx receipt
Signed-off-by: F Bojarski <[email protected]>
1 parent 3666fb4 commit 19f9411

File tree

4 files changed

+78
-102
lines changed

4 files changed

+78
-102
lines changed

‎rlptxrcpt/london/columns.lisp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@
3030
(IS_TOPIC :binary@prove)
3131
(IS_DATA :binary@prove)
3232
(LOG_ENTRY_SIZE :i32)
33-
(LOCAL_SIZE :i32)
34-
(PHASE_ID :i16))
33+
(LOCAL_SIZE :i32))
34+
;; (PHASE_ID :i16) defcomputedcolumn
3535

3636
;; aliases
3737
(defalias

‎rlptxrcpt/london/constraints.lisp‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -71,15 +71,18 @@
7171
(phase-constancy [PHASE 1] TXRCPT_SIZE))
7272

7373
;; 4.1.2 Global Phase Constraints ;;
74-
(defconstraint impose-phase-id ()
75-
(eq! PHASE_ID
76-
(+ (reduce +
77-
(for k [1 : 5] (* k [PHASE k])))
74+
(defcomputedcolumn (PHASE_ID :i16)
75+
(+
76+
(* 1 [PHASE 1])
77+
(* 2 [PHASE 2])
78+
(* 3 [PHASE 3])
79+
(* 4 [PHASE 4])
80+
(* 5 [PHASE 5])
7881
(* SUBPHASE_ID_WEIGHT_IS_PREFIX IS_PREFIX)
7982
(* SUBPHASE_ID_WEIGHT_IS_OT IS_TOPIC)
8083
(* SUBPHASE_ID_WEIGHT_IS_OD IS_DATA)
8184
(* SUBPHASE_ID_WEIGHT_DEPTH DEPTH_1)
82-
(* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL))))
85+
(* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL)))
8386

8487
(defconstraint initial-stamp (:domain {0})
8588
(begin (vanishes! ABS_TX_NUM)

‎rlptxrcpt/osaka/columns.lisp‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,10 @@
1010
(LIMB_CONSTRUCTED :binary@prove)
1111
(INDEX :i24)
1212
(INDEX_LOCAL :i24)
13-
(PHASE :binary@prove :array [5])
13+
(PHASE_1 :binary@prove )
14+
(PHASE_2 :binary@prove )
15+
(PHASE_3 :binary@prove )
16+
(PHASE_5 :binary@prove )
1417
(PHASE_END :binary@prove)
1518
(COUNTER :i32)
1619
(nSTEP :i32)
@@ -30,8 +33,8 @@
3033
(IS_TOPIC :binary@prove)
3134
(IS_DATA :binary@prove)
3235
(LOG_ENTRY_SIZE :i32)
33-
(LOCAL_SIZE :i32)
34-
(PHASE_ID :i16))
36+
(LOCAL_SIZE :i32))
37+
;; (PHASE_ID :i16) defcomputedcolumn
3538

3639
;; aliases
3740
(defalias

‎rlptxrcpt/osaka/constraints.lisp‎

Lines changed: 62 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -50,56 +50,56 @@
5050
(counter-constant IS_DATA)))
5151

5252
(defconstraint special-ct-constancy ()
53-
(if-not-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) IS_PREFIX (- 1 IS_DATA))
53+
(if-not-zero (+ (- 1 PHASE_5) (- 1 DEPTH_1) IS_PREFIX (- 1 IS_DATA))
5454
(counter-constant [INPUT 1])))
5555

56-
(defconstraint ct-incrementings ()
56+
(defconstraint ct-incrementing ()
5757
(begin (if-zero (* IS_DATA IS_PREFIX)
5858
(counter-incrementing LC))
5959
(counter-incrementing LC_CORRECTION)))
6060

61-
(defconstraint phase4-decrementing ()
62-
(phase-decrementing [PHASE 4] IS_PREFIX))
63-
6461
(defconstraint phase5-incrementing ()
65-
(phase-incrementing [PHASE 5] DEPTH_1))
62+
(phase-incrementing PHASE_5 DEPTH_1))
6663

67-
(defconstraint istopic-incrementing ()
64+
(defconstraint is-topic-incrementing ()
6865
(phase-incrementing IS_TOPIC INDEX_LOCAL))
6966

7067
(defconstraint phase1-constant ()
71-
(phase-constancy [PHASE 1] TXRCPT_SIZE))
68+
(phase-constancy PHASE_1 TXRCPT_SIZE))
7269

7370
;; 4.1.2 Global Phase Constraints ;;
74-
(defconstraint impose-phase-id ()
75-
(eq! PHASE_ID
76-
(+ (reduce +
77-
(for k [1 : 5] (* k [PHASE k])))
71+
(defcomputedcolumn (PHASE_ID :i16)
72+
(+
73+
(* 1 PHASE_1)
74+
(* 2 PHASE_2)
75+
(* 3 PHASE_3)
76+
(* 5 PHASE_5)
7877
(* SUBPHASE_ID_WEIGHT_IS_PREFIX IS_PREFIX)
7978
(* SUBPHASE_ID_WEIGHT_IS_OT IS_TOPIC)
8079
(* SUBPHASE_ID_WEIGHT_IS_OD IS_DATA)
8180
(* SUBPHASE_ID_WEIGHT_DEPTH DEPTH_1)
82-
(* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL))))
81+
(* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL)))
8382

8483
(defconstraint initial-stamp (:domain {0})
8584
(begin (vanishes! ABS_TX_NUM)
8685
(vanishes! ABS_LOG_NUM)))
8786

87+
(defun (phase-sum) (+ PHASE_1 PHASE_2 PHASE_3 PHASE_5))
88+
8889
(defconstraint phase-exclusion ()
8990
(if-zero ABS_TX_NUM
90-
(vanishes! (reduce + (for i [5] [PHASE i])))
91-
(eq! 1
92-
(reduce + (for i [5] [PHASE i])))))
91+
(vanishes! (phase-sum))
92+
(eq! 1 (phase-sum))))
9393

9494
(defconstraint ABS_TX_NUM-evolution ()
95-
(if (or! (eq! [PHASE 1] 0) (remained-constant! [PHASE 1]))
95+
(if (or! (eq! PHASE_1 0) (remained-constant! PHASE_1))
9696
;; no change
9797
(remained-constant! ABS_TX_NUM)
9898
;; increment
9999
(did-inc! ABS_TX_NUM 1)))
100100

101101
(defconstraint ABS_LOG_NUM-evolution ()
102-
(if-zero (+ (- 1 [PHASE 5]) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT)
102+
(if-zero (+ (- 1 PHASE_5) (- 1 DEPTH_1) (- 1 IS_PREFIX) IS_TOPIC IS_DATA CT)
103103
(did-inc! ABS_LOG_NUM 1)
104104
(remained-constant! ABS_LOG_NUM)))
105105

@@ -111,24 +111,27 @@
111111
(if-not-zero PHASE_SIZE
112112
(vanishes! PHASE_END)))
113113

114-
(defconstraint no-end-no-changephase (:guard ABS_TX_NUM)
114+
(defun (phase-wght-sum) (+ PHASE_1
115+
(* 2 PHASE_2)
116+
(* 3 PHASE_3)
117+
(* 5 PHASE_5)))
118+
119+
(defconstraint no-end-no-change-phase (:guard ABS_TX_NUM)
115120
(if-zero PHASE_END
116-
(eq! (reduce +
117-
(for i [5] (* i [PHASE i])))
118-
(reduce +
119-
(for i
120-
[5]
121-
(* i (next [PHASE i])))))))
121+
(eq! (phase-wght-sum)
122+
(+ (next PHASE_1)
123+
(* 2 (next PHASE_2))
124+
(* 3 (next PHASE_3))
125+
(* 5 (next PHASE_5))))))
122126

123127
(defconstraint phase-transition ()
124128
(if-eq PHASE_END 1
125129
(begin (eq! 1
126-
(+ (* [PHASE 1] (next [PHASE 2]))
127-
(* [PHASE 2] (next [PHASE 3]))
128-
(* [PHASE 3] (next [PHASE 4]))
129-
(* [PHASE 4] (next [PHASE 5]))
130-
(* [PHASE 5] (next [PHASE 1]))))
131-
(if-eq [PHASE 5] 1 (vanishes! TXRCPT_SIZE)))))
130+
(+ (* PHASE_1 (next PHASE_2))
131+
(* PHASE_2 (next PHASE_3))
132+
(* PHASE_3 (next PHASE_5))
133+
(* PHASE_5 (next PHASE_1))))
134+
(if-eq PHASE_5 1 (vanishes! TXRCPT_SIZE)))))
132135

133136
;; 4.1.3 Byte decomposition's loop heartbeat ;;
134137
(defconstraint ct-imply-done (:guard ABS_TX_NUM)
@@ -163,26 +166,25 @@
163166

164167
;; 4.1.6 Byte size updates ;;
165168
(defconstraint globalsize-update ()
166-
(if-zero [PHASE 1]
169+
(if-zero PHASE_1
167170
(eq! TXRCPT_SIZE
168171
(- (prev TXRCPT_SIZE) (* LC nBYTES)))))
169172

170-
(defconstraint phasesize-update ()
171-
(if-eq 1 (+ (* [PHASE 4] (- 1 IS_PREFIX))
172-
(* [PHASE 5] DEPTH_1))
173+
(defconstraint phase-size-update ()
174+
(if-eq 1 (* PHASE_5 DEPTH_1)
173175
(eq! PHASE_SIZE
174176
(- (prev PHASE_SIZE) (* LC nBYTES)))))
175177

176178
;; LC correction nullity ;;
177-
(defconstraint lccorrection-nullity ()
178-
(if-zero (+ [PHASE 1] (* [PHASE 5] IS_DATA))
179+
(defconstraint lc-correction-nullity ()
180+
(if-zero (+ PHASE_1 (* PHASE_5 IS_DATA))
179181
(vanishes! LC_CORRECTION)))
180182

181-
;; 4.1.8 Finalisation Constraints ;;
182-
(defconstraint finalisation (:domain {-1})
183+
;; 4.1.8 Finalization Constraints ;;
184+
(defconstraint finalization (:domain {-1})
183185
(if-not-zero ABS_TX_NUM
184186
(begin (eq! PHASE_END 1)
185-
(eq! [PHASE 5] 1)
187+
(eq! PHASE_5 1)
186188
(eq! ABS_TX_NUM ABS_TX_NUM_MAX)
187189
(eq! ABS_LOG_NUM ABS_LOG_NUM_MAX))))
188190

@@ -192,8 +194,8 @@
192194
;; ;;
193195
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
194196
;; 4.2.1 Phase 1 : RLP prefix ;;
195-
(defconstraint phase1-init (:guard [PHASE 1]);; 4.1.1
196-
(if-zero (prev [PHASE 1])
197+
(defconstraint phase1-init (:guard PHASE_1);; 4.1.1
198+
(if-zero (prev PHASE_1)
197199
(begin (vanishes! (+ (- 1 IS_PREFIX) PHASE_END (next IS_PREFIX)))
198200
(eq! nSTEP 1)
199201
(if-zero [INPUT 1]
@@ -203,17 +205,17 @@
203205
(* [INPUT 1] (^ 256 LLARGEMO)))
204206
(eq! nBYTES 1))))))
205207

206-
(defconstraint phase1-rlprefix (:guard [PHASE 1])
208+
(defconstraint phase1-rlprefix (:guard PHASE_1)
207209
(if-zero IS_PREFIX
208210
(begin (eq! nSTEP 8)
209211
(vanishes! LC_CORRECTION)
210212
(eq! [INPUT 1] TXRCPT_SIZE)
211-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 1] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
213+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_1 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
212214
(if-eq DONE 1 (eq! PHASE_END 1)))))
213215

214216
;; 4.2.2 Phase 2 : status code Rz ;;
215217
(defconstraint phase2 ()
216-
(if-eq [PHASE 2] 1
218+
(if-eq PHASE_2 1
217219
(begin (eq! nSTEP 1)
218220
(if-zero [INPUT 1]
219221
(eq! LIMB
@@ -225,51 +227,19 @@
225227

226228
;; 4.2.3 Phase 3 : cumulative gas Ru ;;
227229
(defconstraint phase3 ()
228-
(if-eq [PHASE 3] 1
230+
(if-eq PHASE_3 1
229231
(begin (eq! nSTEP 8)
230232
(rlpPrefixInt [INPUT 1] CT nSTEP DONE [BYTE 1] [ACC 1] ACC_SIZE POWER BIT BIT_ACC LIMB LC nBYTES)
231233
(if-eq DONE 1
232234
(begin (limbShifting [INPUT 1] POWER ACC_SIZE LIMB nBYTES)
233235
(eq! PHASE_END 1))))))
234236

235-
;; Phase 4: bloom filter Rb ;;
236-
(defconstraint phase4-prefix (:guard [PHASE 4])
237-
(if-zero (prev [PHASE 4])
238-
(begin (vanishes! (+ (- 1 IS_PREFIX) PHASE_END (next IS_PREFIX)))
239-
(eq! PHASE_SIZE 256)
240-
(eq! nSTEP 1)
241-
(eq! LIMB
242-
(+ (* (+ RLP_PREFIX_INT_LONG 2) (^ 256 LLARGEMO))
243-
(* PHASE_SIZE (^ 256 13))))
244-
(eq! nBYTES 3)
245-
(vanishes! INDEX_LOCAL))))
246-
247-
(defconstraint phase4-bloom-concatenation (:guard [PHASE 4])
248-
(if-zero IS_PREFIX
249-
(begin (eq! nSTEP LLARGE)
250-
(if-eq DONE 1
251-
(begin (for k
252-
[1 : 4]
253-
(begin (eq! [ACC k] [INPUT k])
254-
(eq! [INPUT k]
255-
(shift LIMB (- k 4)))
256-
(eq! (shift nBYTES (- k 4))
257-
LLARGE)))
258-
(eq! (+ (shift LC -4) (shift LC -3))
259-
1)
260-
(if-zero PHASE_SIZE
261-
(eq! PHASE_END 1))))
262-
(eq! INDEX_LOCAL
263-
(+ (prev INDEX_LOCAL)
264-
(* (prev LC)
265-
(- 1 (prev IS_PREFIX))))))))
266-
267237
;; Phase 5: log series Rl ;;
268-
(defconstraint phase5-init (:guard [PHASE 5])
269-
(if-zero (prev [PHASE 5])
238+
(defconstraint phase5-init (:guard PHASE_5)
239+
(if-zero (prev PHASE_5)
270240
(vanishes! (+ DEPTH_1 (- 1 IS_PREFIX) IS_TOPIC IS_DATA))))
271241

272-
(defconstraint phase5-phaseRlpPrefix (:guard [PHASE 5])
242+
(defconstraint phase5-phaseRlpPrefix (:guard PHASE_5)
273243
(if-zero DEPTH_1
274244
(begin (eq! [INPUT 1] PHASE_SIZE)
275245
(if-zero [INPUT 1]
@@ -279,22 +249,22 @@
279249
(eq! nBYTES 1)
280250
(eq! PHASE_END 1))
281251
(begin (eq! nSTEP 8)
282-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 5] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
252+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_5 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
283253
(if-eq DONE 1
284254
(vanishes! (+ (- 1 (next DEPTH_1))
285255
(- 1 (next IS_PREFIX))
286256
(next IS_TOPIC)
287257
(next IS_DATA)))))))))
288258

289-
(defconstraint phase5-logentryRlpPrefix (:guard [PHASE 5])
259+
(defconstraint phase5-logentryRlpPrefix (:guard PHASE_5)
290260
(if-eq 1 (* DEPTH_1 IS_PREFIX (- 1 IS_TOPIC) (- 1 IS_DATA))
291261
(begin (eq! [INPUT 1] LOG_ENTRY_SIZE)
292262
(eq! nSTEP 8)
293-
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE [PHASE 5] ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
263+
(rlpPrefixOfByteString [INPUT 1] CT nSTEP DONE PHASE_5 ACC_SIZE POWER BIT [ACC 1] [ACC 2] LC LIMB nBYTES)
294264
(if-eq DONE 1
295265
(vanishes! (+ (next IS_PREFIX) (next IS_TOPIC) (next IS_DATA)))))))
296266

297-
(defconstraint phase5-rlpAddress (:guard [PHASE 5])
267+
(defconstraint phase5-rlpAddress (:guard PHASE_5)
298268
(if-zero (+ IS_PREFIX IS_TOPIC IS_DATA)
299269
(begin (eq! nSTEP 3)
300270
(eq! LC 1)
@@ -311,7 +281,7 @@
311281
(- 1 (next IS_TOPIC))
312282
(next IS_DATA))))))))
313283

314-
(defconstraint phase5-topic-prefix (:guard [PHASE 5])
284+
(defconstraint phase5-topic-prefix (:guard PHASE_5)
315285
(if-eq (* IS_PREFIX IS_TOPIC) 1
316286
(begin (vanishes! INDEX_LOCAL)
317287
(eq! nSTEP 1)
@@ -336,7 +306,7 @@
336306
(- 1 (next IS_TOPIC))
337307
(next IS_DATA))))))))
338308

339-
(defconstraint phase5-topic (:guard [PHASE 5])
309+
(defconstraint phase5-topic (:guard PHASE_5)
340310
(if-zero (+ IS_PREFIX (- 1 IS_TOPIC))
341311
(begin (eq! nSTEP 3)
342312
(eq! LC 1)
@@ -360,7 +330,7 @@
360330
(- 1 (next IS_TOPIC))
361331
(next IS_DATA)))))))))
362332

363-
(defconstraint phase5-dataprefix (:guard [PHASE 5])
333+
(defconstraint phase5-dataprefix (:guard PHASE_5)
364334
(if-eq (* IS_PREFIX IS_DATA) 1
365335
(begin (eq! [INPUT 1] LOCAL_SIZE)
366336
(if-zero LOCAL_SIZE
@@ -402,7 +372,7 @@
402372
CT
403373
nSTEP
404374
DONE
405-
[PHASE 1]
375+
PHASE_1
406376
ACC_SIZE
407377
POWER
408378
BIT
@@ -416,7 +386,7 @@
416386
(next IS_TOPIC)
417387
(- 1 (next IS_DATA))))))))))
418388

419-
(defconstraint phase5-data (:guard [PHASE 5])
389+
(defconstraint phase5-data (:guard PHASE_5)
420390
(if-zero (+ IS_PREFIX (- 1 IS_DATA))
421391
(begin (eq! INDEX_LOCAL CT)
422392
(eq! LC 1)
@@ -431,13 +401,13 @@
431401
(next IS_TOPIC)
432402
(next IS_DATA)))))))))
433403

434-
(defconstraint phase5-logEntrySize-update (:guard [PHASE 5])
404+
(defconstraint phase5-logEntrySize-update (:guard PHASE_5)
435405
(if-zero (+ (- 1 DEPTH_1)
436406
(* IS_PREFIX (- 1 IS_TOPIC) (- 1 IS_DATA)))
437407
(eq! LOG_ENTRY_SIZE
438408
(- (prev LOG_ENTRY_SIZE) (* LC nBYTES)))))
439409

440-
(defconstraint phase5-localsize-update (:guard [PHASE 5])
410+
(defconstraint phase5-localsize-update (:guard PHASE_5)
441411
(if-zero (+ IS_PREFIX
442412
(- 1 (+ IS_TOPIC IS_DATA)))
443413
(eq! LOCAL_SIZE

0 commit comments

Comments
 (0)