-
Notifications
You must be signed in to change notification settings - Fork 134
/
deposit-spec.ini
825 lines (767 loc) · 50.7 KB
/
deposit-spec.ini
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
; contract: https://github.com/ethereum/eth2.0-specs/blob/v0.10.0/deposit_contract/contracts/validator_registration.vy
; vyper: https://github.com/vyperlang/vyper/tree/1761-HOTFIX-v0.1.0-beta.13
[root]
k: #execute
; default
pc: 0 => _
word_stack: .WordStack => _
local_mem: .Map => _
gas: #symGas(G, 0 => {GAS_COST_MIN}, 0 => {GAS_COST_MAX}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
memory_used: #symMem({PRE_MEM_COST} => {MEM_COST}, .Set)
; no changes
call_data: _
log: _
refund: _
storage: _
orig_storage: _
balance: INIT_BALANCE
nonce: INIT_NONCE
code: {RUNTIME_CODE}
; ignore (potential) changes
output: _ => _
status_code: _ => _
; variables
comment:
schedule: ISTANBUL
this: THIS
msg_sender: MSG_SENDER
call_value: CALL_VALUE
call_depth: CALL_DEPTH
active_accounts:
accounts:
requires:
// conditions
andBool #range(0 <= CALL_DEPTH < 1024)
andBool #regularAddress({SCHEDULE}, THIS)
// types
andBool #rangeAddress(THIS)
andBool #rangeAddress(MSG_SENDER)
andBool #rangeUInt(256, CALL_VALUE)
andBool #rangeUInt(256, INIT_BALANCE)
andBool #rangeUInt(256, INIT_NONCE)
andBool #rangeUInt(256, EXTRA_CALL_DATA_SIZE)
andBool isInitGas(G)
ensures:
attribute:
GAS_COST_MIN: {GAS_COST}
GAS_COST_MAX: {GAS_COST}
PRE_MEM_COST: 0
VYPER_GENERATED_BOUNDS:
; bounds - vyper generated
[ 32 := #buf(32, 1461501637330902918203684832716283019655932542976) ]
[ 64 := #buf(32, 170141183460469231731687303715884105727) ]
[ 96 := #buf(32, 115792089237316195423570985008687907853099843482180094807725896704197245534208) ]
[ 128 := #buf(32, 1701411834604692317316873037158841057270000000000) ]
[ 160 := #buf(32, 115792089237316195423570985006986496018665292348323691002298742950633129639936) ]
ENSURES_VYPER_GENERATED_BOUNDS:
andBool #range(NEW_MEM, 32, 32) ==K #buf(32, 1461501637330902918203684832716283019655932542976)
andBool #range(NEW_MEM, 64, 32) ==K #buf(32, 170141183460469231731687303715884105727)
andBool #range(NEW_MEM, 96, 32) ==K #buf(32, 115792089237316195423570985008687907853099843482180094807725896704197245534208)
andBool #range(NEW_MEM, 128, 32) ==K #buf(32, 1701411834604692317316873037158841057270000000000)
andBool #range(NEW_MEM, 160, 32) ==K #buf(32, 115792089237316195423570985006986496018665292348323691002298742950633129639936)
LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT:
// let-bindings
andBool X1 ==Int DEPOSIT_COUNT /Int 256
andBool X2 ==Int X1 /Int 256
andBool X3 ==Int X2 /Int 256
andBool X4 ==Int X3 /Int 256
andBool X5 ==Int X4 /Int 256
andBool X6 ==Int X5 /Int 256
andBool X7 ==Int X6 /Int 256
andBool X8 ==Int X7 /Int 256
//
andBool Y1 ==Int DEPOSIT_COUNT &Int 255
andBool Y2 ==Int (Y1 *Int 256) +Int (X1 &Int 255)
andBool Y3 ==Int (Y2 *Int 256) +Int (X2 &Int 255)
andBool Y4 ==Int (Y3 *Int 256) +Int (X3 &Int 255)
andBool Y5 ==Int (Y4 *Int 256) +Int (X4 &Int 255)
andBool Y6 ==Int (Y5 *Int 256) +Int (X5 &Int 255)
andBool Y7 ==Int (Y6 *Int 256) +Int (X6 &Int 255)
andBool Y8 ==Int (Y7 *Int 256) +Int (X7 &Int 255)
LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_AMOUNT:
// let-bindings
andBool XX1 ==Int {DEPOSIT_AMOUNT} /Int 256
andBool XX2 ==Int XX1 /Int 256
andBool XX3 ==Int XX2 /Int 256
andBool XX4 ==Int XX3 /Int 256
andBool XX5 ==Int XX4 /Int 256
andBool XX6 ==Int XX5 /Int 256
andBool XX7 ==Int XX6 /Int 256
andBool XX8 ==Int XX7 /Int 256
//
andBool YY1 ==Int {DEPOSIT_AMOUNT} &Int 255
andBool YY2 ==Int (YY1 *Int 256) +Int (XX1 &Int 255)
andBool YY3 ==Int (YY2 *Int 256) +Int (XX2 &Int 255)
andBool YY4 ==Int (YY3 *Int 256) +Int (XX3 &Int 255)
andBool YY5 ==Int (YY4 *Int 256) +Int (XX4 &Int 255)
andBool YY6 ==Int (YY5 *Int 256) +Int (XX5 &Int 255)
andBool YY7 ==Int (YY6 *Int 256) +Int (XX6 &Int 255)
andBool YY8 ==Int (YY7 *Int 256) +Int (XX7 &Int 255)
;
; __init__
;
[init]
; for create
code: {INIT_CODE}
call_data: #buf(CALL_DATA_SIZE, CALL_DATA) /* The expected call_data is empty, but we want to ensure that any accidental or malicious garbage doesn't break the logic. */
storage: .Map
orig_storage: .Map
[init-success]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: 0 => 4684
output: _ => #parseByteStack({RUNTIME_CODE})
storage: .Map => .Map
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 1) <- ZERO_HASHES_01 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 2) <- ZERO_HASHES_02 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 3) <- ZERO_HASHES_03 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 4) <- ZERO_HASHES_04 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 5) <- ZERO_HASHES_05 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 6) <- ZERO_HASHES_06 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 7) <- ZERO_HASHES_07 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 8) <- ZERO_HASHES_08 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 9) <- ZERO_HASHES_09 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 10) <- ZERO_HASHES_10 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 11) <- ZERO_HASHES_11 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 12) <- ZERO_HASHES_12 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 13) <- ZERO_HASHES_13 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 14) <- ZERO_HASHES_14 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 15) <- ZERO_HASHES_15 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 16) <- ZERO_HASHES_16 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 17) <- ZERO_HASHES_17 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 18) <- ZERO_HASHES_18 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 19) <- ZERO_HASHES_19 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 20) <- ZERO_HASHES_20 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 21) <- ZERO_HASHES_21 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 22) <- ZERO_HASHES_22 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 23) <- ZERO_HASHES_23 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 24) <- ZERO_HASHES_24 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 25) <- ZERO_HASHES_25 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 26) <- ZERO_HASHES_26 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 27) <- ZERO_HASHES_27 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 28) <- ZERO_HASHES_28 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 29) <- ZERO_HASHES_29 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 30) <- ZERO_HASHES_30 ]
[ #hashedLocation({COMPILER}, {ZERO_HASHES}, 31) <- ZERO_HASHES_31 ]
+ensures:
andBool ZERO_HASHES_01 ==Int 111109925611824843164212799849330761292948257037696933205019304127221294824267
andBool ZERO_HASHES_02 ==Int 99208582119974435635122834636860944394611999454454139265101248405002450066801
andBool ZERO_HASHES_03 ==Int 90236482254272784387420235795439987838046297224132114184911355661882633139004
andBool ZERO_HASHES_04 ==Int 37735605373063189145609870960383397519157271673603325697615186821228299686460
andBool ZERO_HASHES_05 ==Int 71913990603354163933828411608472620759041242276514156984220416916786598645040
andBool ZERO_HASHES_06 ==Int 97950246258348409692531222476457095756697573854283095464293321272902400876449
andBool ZERO_HASHES_07 ==Int 61477539263323159367083172935543284935396148729545980766185719446310214598444
andBool ZERO_HASHES_08 ==Int 17421805441306662828813938682339723858550903736451371212309658526853237682579
andBool ZERO_HASHES_09 ==Int 36378541427962263534507524415416206454520492712868881526514165827410968138209
andBool ZERO_HASHES_10 ==Int 115790397228362049466744952478840932980575707644826095658658722282297806219563
andBool ZERO_HASHES_11 ==Int 49274280630555601797897865132281002146293805070798126028158380560236737348128
andBool ZERO_HASHES_12 ==Int 83141414795720293663742362646790664571283415314047445910275483835985445429087
andBool ZERO_HASHES_13 ==Int 101054748575760473813564301333136859612099677302306750615986031729334544803934
andBool ZERO_HASHES_14 ==Int 82118745295487409076436877854822273376925616082029112448942904331137821783940
andBool ZERO_HASHES_15 ==Int 96163225932810885736266036029917445088819617531019675867068430475668935471803
andBool ZERO_HASHES_16 ==Int 65088336600655240038095685796880324455992690470134814168105519136673920265195
andBool ZERO_HASHES_17 ==Int 63799769208876827738003032821893022143097474293424873737753651534389224801195
andBool ZERO_HASHES_18 ==Int 67816509212607392382740074792956495608635882665724233434230291854030732195236
andBool ZERO_HASHES_19 ==Int 112434921305070287559384313443636314384702132445424344431569901673819370811775
andBool ZERO_HASHES_20 ==Int 93112230953615344385943808306254931967020084209711158834711445534019305401258
andBool ZERO_HASHES_21 ==Int 62669181200805966564192421757819261985029837393920877947563891644048741760924
andBool ZERO_HASHES_22 ==Int 115205076510789746548603599597779790746302978279183356048242913992201050263911
andBool ZERO_HASHES_23 ==Int 104539113834876204786309677268196632426672930326563741131169818132455910346967
andBool ZERO_HASHES_24 ==Int 22220639310854829338009213075933187018531271127936675242871245915956321995712
andBool ZERO_HASHES_25 ==Int 15020270542076658589520891983882988038238976963402869888887748183344883676484
andBool ZERO_HASHES_26 ==Int 44153847389689082926726920587762841378344527039658864594464812861203077687141
andBool ZERO_HASHES_27 ==Int 56477553013929602061607210630309819251225478284985718139011950762099695862212
andBool ZERO_HASHES_28 ==Int 59947690453143216863404114195220773987146401062580150977299285593826340359137
andBool ZERO_HASHES_29 ==Int 61701827484336113174235061579227602710411934053193562355142130200675961312822
andBool ZERO_HASHES_30 ==Int 82317687062382453000908156613654683080667757725396933779730835823850574461532
andBool ZERO_HASHES_31 ==Int 68918648562210843738065282119278105929739692988049575047112145589597483221239
// cross-check
andBool ZERO_HASHES_01 ==Int #sha256(#buf(32, 0) ++ #buf(32, 0))
andBool ZERO_HASHES_02 ==Int #sha256(#buf(32, ZERO_HASHES_01) ++ #buf(32, ZERO_HASHES_01))
andBool ZERO_HASHES_03 ==Int #sha256(#buf(32, ZERO_HASHES_02) ++ #buf(32, ZERO_HASHES_02))
andBool ZERO_HASHES_04 ==Int #sha256(#buf(32, ZERO_HASHES_03) ++ #buf(32, ZERO_HASHES_03))
andBool ZERO_HASHES_05 ==Int #sha256(#buf(32, ZERO_HASHES_04) ++ #buf(32, ZERO_HASHES_04))
andBool ZERO_HASHES_06 ==Int #sha256(#buf(32, ZERO_HASHES_05) ++ #buf(32, ZERO_HASHES_05))
andBool ZERO_HASHES_07 ==Int #sha256(#buf(32, ZERO_HASHES_06) ++ #buf(32, ZERO_HASHES_06))
andBool ZERO_HASHES_08 ==Int #sha256(#buf(32, ZERO_HASHES_07) ++ #buf(32, ZERO_HASHES_07))
andBool ZERO_HASHES_09 ==Int #sha256(#buf(32, ZERO_HASHES_08) ++ #buf(32, ZERO_HASHES_08))
andBool ZERO_HASHES_10 ==Int #sha256(#buf(32, ZERO_HASHES_09) ++ #buf(32, ZERO_HASHES_09))
andBool ZERO_HASHES_11 ==Int #sha256(#buf(32, ZERO_HASHES_10) ++ #buf(32, ZERO_HASHES_10))
andBool ZERO_HASHES_12 ==Int #sha256(#buf(32, ZERO_HASHES_11) ++ #buf(32, ZERO_HASHES_11))
andBool ZERO_HASHES_13 ==Int #sha256(#buf(32, ZERO_HASHES_12) ++ #buf(32, ZERO_HASHES_12))
andBool ZERO_HASHES_14 ==Int #sha256(#buf(32, ZERO_HASHES_13) ++ #buf(32, ZERO_HASHES_13))
andBool ZERO_HASHES_15 ==Int #sha256(#buf(32, ZERO_HASHES_14) ++ #buf(32, ZERO_HASHES_14))
andBool ZERO_HASHES_16 ==Int #sha256(#buf(32, ZERO_HASHES_15) ++ #buf(32, ZERO_HASHES_15))
andBool ZERO_HASHES_17 ==Int #sha256(#buf(32, ZERO_HASHES_16) ++ #buf(32, ZERO_HASHES_16))
andBool ZERO_HASHES_18 ==Int #sha256(#buf(32, ZERO_HASHES_17) ++ #buf(32, ZERO_HASHES_17))
andBool ZERO_HASHES_19 ==Int #sha256(#buf(32, ZERO_HASHES_18) ++ #buf(32, ZERO_HASHES_18))
andBool ZERO_HASHES_20 ==Int #sha256(#buf(32, ZERO_HASHES_19) ++ #buf(32, ZERO_HASHES_19))
andBool ZERO_HASHES_21 ==Int #sha256(#buf(32, ZERO_HASHES_20) ++ #buf(32, ZERO_HASHES_20))
andBool ZERO_HASHES_22 ==Int #sha256(#buf(32, ZERO_HASHES_21) ++ #buf(32, ZERO_HASHES_21))
andBool ZERO_HASHES_23 ==Int #sha256(#buf(32, ZERO_HASHES_22) ++ #buf(32, ZERO_HASHES_22))
andBool ZERO_HASHES_24 ==Int #sha256(#buf(32, ZERO_HASHES_23) ++ #buf(32, ZERO_HASHES_23))
andBool ZERO_HASHES_25 ==Int #sha256(#buf(32, ZERO_HASHES_24) ++ #buf(32, ZERO_HASHES_24))
andBool ZERO_HASHES_26 ==Int #sha256(#buf(32, ZERO_HASHES_25) ++ #buf(32, ZERO_HASHES_25))
andBool ZERO_HASHES_27 ==Int #sha256(#buf(32, ZERO_HASHES_26) ++ #buf(32, ZERO_HASHES_26))
andBool ZERO_HASHES_28 ==Int #sha256(#buf(32, ZERO_HASHES_27) ++ #buf(32, ZERO_HASHES_27))
andBool ZERO_HASHES_29 ==Int #sha256(#buf(32, ZERO_HASHES_28) ++ #buf(32, ZERO_HASHES_28))
andBool ZERO_HASHES_30 ==Int #sha256(#buf(32, ZERO_HASHES_29) ++ #buf(32, ZERO_HASHES_29))
andBool ZERO_HASHES_31 ==Int #sha256(#buf(32, ZERO_HASHES_30) ++ #buf(32, ZERO_HASHES_30))
refund: _ => _
+requires:
// conditions
andBool CALL_VALUE ==Int 0
GAS_COST: 672893
MEM_COST: 4278
[init-revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
pc: 0 => 151
+requires:
// conditions
andBool CALL_VALUE =/=Int 0
GAS_COST: 69
MEM_COST: 192
;
; get_deposit_root
;
[get_deposit_root]
; The term `#buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)` models certain extra call-data added accidently or intentionally.
; This ensures that the function works correctly even in such a case.
call_data: #abiCallData("get_deposit_root", .TypedArgs) ++ #buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)
[get_deposit_root-success]
storage: M
+requires:
// conditions
andBool CALL_VALUE ==Int 0
// types
andBool #rangeUInt(256, DEPOSIT_COUNT)
andBool isStorage(M)
// let-bindings
andBool DEPOSIT_COUNT ==Int select(M, #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList))
PC_LOOPHEAD: 968
PC_END: 1291
WORD_STACK_LOOP: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
LOOP_BOUND: 32
LOOP_INDEX_ADDR: 416
[get_deposit_root-success-init]
pc: 0 => {PC_LOOPHEAD}
word_stack: .WordStack => 1 : {WORD_STACK_LOOP}
local_mem: .Map => NEW_MEM
+ensures:
{ENSURES_VYPER_GENERATED_BOUNDS}
andBool #range(NEW_MEM, 320, 32) ==K #buf(32, 0)
andBool #range(NEW_MEM, 352, 32) ==K #buf(32, {NODE_1})
andBool #range(NEW_MEM, 384, 32) ==K #buf(32, DEPOSIT_COUNT /Int 2)
andBool #range(NEW_MEM, 416, 32) ==K #buf(32, 1)
[get_deposit_root-success-init-then]
NODE_1: #sha256(#buf(32, {BRANCH_0}) ++ #buf(32, 0))
BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
+requires:
// conditions
andBool DEPOSIT_COUNT &Int 1 ==Int 1
GAS_COST: 1728
MEM_COST: 672
[get_deposit_root-success-init-else]
NODE_1: #sha256(#buf(32, 0) ++ #buf(32, {ZERO_HASHES_0}))
ZERO_HASHES_0: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, 0))
+requires:
// conditions
andBool DEPOSIT_COUNT &Int 1 =/=Int 1
GAS_COST: 1718
MEM_COST: 544
[get_deposit_root-success-loop]
LOCAL_MEM_LOOPHEAD: MEM
{VYPER_GENERATED_BOUNDS}
; locals - invariants
[ 320 /* = 320 + 32 * 0 */ := #buf(32, 0) ] /* zero_bytes32: bytes32 = 0x0 */
[ 352 /* = 320 + 32 * 1 */ := #buf(32, NODE) ] /* node: bytes32 */
[ 384 /* = 320 + 32 * 2 */ := #buf(32, SIZE) ] /* size: uint256 */
[ 416 /* = 320 + 32 * 3 */ := #buf(32, HEIGHT) ] /* height */
+requires:
// conditions - invariants
andBool HEIGHT <=Int 32
// types
andBool #rangeUInt(256, NODE)
andBool #rangeUInt(256, SIZE)
andBool #rangeUInt(256, HEIGHT)
PRE_MEM_COST: 672
[get_deposit_root-success-loop-enter]
pc: {PC_LOOPHEAD}
word_stack: (HEIGHT => HEIGHT +Int 1) : {WORD_STACK_LOOP}
local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
+ensures:
{ENSURES_VYPER_GENERATED_BOUNDS}
andBool #range(NEW_MEM, 320, 32) ==K #buf(32, 0)
andBool #range(NEW_MEM, 352, 32) ==K #buf(32, {NODE_NEW})
andBool #range(NEW_MEM, 384, 32) ==K #buf(32, SIZE /Int 2)
andBool #range(NEW_MEM, 416, 32) ==K #buf(32, HEIGHT +Int 1)
+requires:
// conditions
andBool HEIGHT =/=Int 32
[get_deposit_root-success-loop-enter-then]
NODE_NEW: #sha256(#buf(32, {BRANCH_HEIGHT}) ++ #buf(32, NODE))
BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
+requires:
// conditions
andBool SIZE &Int 1 ==Int 1
GAS_COST: 1350
MEM_COST: 672
[get_deposit_root-success-loop-enter-else]
NODE_NEW: #sha256(#buf(32, NODE) ++ #buf(32, {ZERO_HASHES_HEIGHT}))
ZERO_HASHES_HEIGHT: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, HEIGHT))
+requires:
// conditions
andBool SIZE &Int 1 =/=Int 1
GAS_COST: 1340
MEM_COST: 672
[get_deposit_root-success-loop-exit]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: {PC_LOOPHEAD} => {PC_END}
output: _ => #buf(32, {RETURN_VAL})
RETURN_VAL: #sha256(#buf(32, NODE) ++ #bufSeg(#buf(32, Y8), 24, 8) ++ #buf(24, 0))
word_stack: HEIGHT : {WORD_STACK_LOOP} => .WordStack
local_mem: {LOCAL_MEM_LOOPHEAD} => _
+requires:
// conditions
andBool HEIGHT ==Int 32
{LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT}
GAS_COST: 11385
MEM_COST: 1216
[get_deposit_root-revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
pc: 0 => 663
+requires:
// conditions
andBool CALL_VALUE =/=Int 0
GAS_COST: 154
MEM_COST: 192
;
; get_deposit_count
;
[get_deposit_count]
; The term `#buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)` models certain extra call-data added accidently or intentionally.
; This ensures that the function works correctly even in such a case.
call_data: #abiCallData("get_deposit_count", .TypedArgs) ++ #buf(EXTRA_CALL_DATA_SIZE, EXTRA_CALL_DATA)
[get_deposit_count-success]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: 0 => 1561
output: _ => #encodeArgs(#bytes(#bufSeg(#buf(32, Y8), 24, 8))) /* #buf(32, 32) ++ #buf(32, 8) ++ #bufSeg(#buf(32, Y8), 24, 8) ++ #buf(24, 0) */
storage: M /* constant function; no storage update */
word_stack: .WordStack
local_mem: .Map => _
+requires:
// conditions
andBool CALL_VALUE ==Int 0
// types
andBool #rangeUInt(256, DEPOSIT_COUNT)
andBool isStorage(M)
// let-bindings
andBool DEPOSIT_COUNT ==Int select(M, #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList))
{LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT}
GAS_COST: 11424
MEM_COST: 832
[get_deposit_count-revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
pc: 0 => 1318
+requires:
// conditions
andBool CALL_VALUE =/=Int 0
GAS_COST: 183
MEM_COST: 192
;
; deposit
;
[deposit]
; #buf(32, 96) ++ #buf(32, 192) ++ #buf(32, 256) // header
; ++ #buf(32, 48) ++ #buf(48, PUBKEY) ++ #buf(16, 0) // pubkey + zero-padding
; ++ #buf(32, 32) ++ #buf(32, WITHDRAWAL_CREDENTIALS) // withdrawal_credentials
; ++ #buf(32, 96) ++ #buf(96, SIGNATURE) // signature
call_data: #abiCallData("deposit", (
#bytes(#buf({PUBKEY_LENGTH}, PUBKEY)),
#bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, WITHDRAWAL_CREDENTIALS)),
#bytes(#buf({SIGNATURE_LENGTH}, SIGNATURE)),
#bytes32(DEPOSIT_DATA_ROOT) ))
storage: M
+requires:
// ranges
andBool #range(0 <= PUBKEY < 2 ^Int ({PUBKEY_LENGTH} *Int 8))
andBool #range(0 <= WITHDRAWAL_CREDENTIALS < 2 ^Int ({WITHDRAWAL_CREDENTIALS_LENGTH} *Int 8))
andBool #range(0 <= SIGNATURE < 2 ^Int ({SIGNATURE_LENGTH} *Int 8))
andBool #rangeUInt(256, DEPOSIT_DATA_ROOT)
// types
andBool #rangeUInt(256, DEPOSIT_COUNT)
andBool isStorage(M)
// let-bindings
andBool DEPOSIT_COUNT ==Int select(M, #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList))
{LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT}
{LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_AMOUNT}
PUBKEY_LENGTH: 48
WITHDRAWAL_CREDENTIALS_LENGTH: 32
SIGNATURE_LENGTH: 96
MAX_DEPOSIT_COUNT: 4294967295
GWEI_IN_WEI: 1000000000
MIN_DEPOSIT_AMOUNT: 1000000000
DEPOSIT_AMOUNT: (CALL_VALUE /Int {GWEI_IN_WEI})
PUBKEY_ROOT: #sha256(#buf(48, PUBKEY) ++ #buf(16, 0))
TMP1: #sha256(#bufSeg(#buf(96, SIGNATURE), 0, 64))
TMP2: #sha256(#bufSeg(#buf(96, SIGNATURE), 64, 32) ++ #buf(32, 0))
SIGNATURE_ROOT: #sha256(#buf(32, {TMP1}) ++ #buf(32, {TMP2}))
TMP3: #sha256(#buf(32, {PUBKEY_ROOT}) ++ #buf(32, WITHDRAWAL_CREDENTIALS))
TMP4: #sha256(#bufSeg(#buf(32, YY8), 24, 8) ++ #buf(24, 0) ++ #buf(32, {SIGNATURE_ROOT}))
NODE: #sha256(#buf(32, {TMP3}) ++ #buf(32, {TMP4}))
PC_SUBCALL_1: 1792
PC_ADD_BEGIN: 4020
PC_ADD_LOOPHEAD: 4260
PC_ADD_END: 4270
MU_INIT: 768
MU_DATA: 3296
MU_ADD_ODD: 3392
MU_ADD_EVEN: 3488
; #### `DepositData`
;
; ```python
; class DepositData(Container):
; pubkey: BLSPubkey
; withdrawal_credentials: Hash
; amount: Gwei
; signature: BLSSignature
; ```
; ___________________________ node _________________________
; / \
; __________ tmp3 ___________________ ______________ tmp4 _______________
; / \ / \
; pubkey_root withdrawal_credentials amount _____ signature_root __________
; / \ / \
; pubkey[0:32] pubkey[32:48]++zero[0:16] tmp1 tmp2
; / \ / \
; signature[0:32] signature[32:64] signature[64:96] zero[0:32]
[deposit-success]
+requires:
// conditions
andBool DEPOSIT_COUNT <Int {MAX_DEPOSIT_COUNT}
andBool CALL_VALUE /Int {GWEI_IN_WEI} >=Int {MIN_DEPOSIT_AMOUNT}
andBool {NODE} ==Int DEPOSIT_DATA_ROOT
[deposit-success-data]
pc: 0 => {PC_ADD_BEGIN}
word_stack: .WordStack
local_mem: .Map => NEW_MEM
+ensures:
{ENSURES_VYPER_GENERATED_BOUNDS}
andBool #range(NEW_MEM, 2784, 32) ==K #buf(32, {NODE})
log: _:List ( .List => ListItem(#abiEventLog(THIS, "DepositEvent",
#bytes(#buf({PUBKEY_LENGTH}, PUBKEY)),
#bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, WITHDRAWAL_CREDENTIALS)),
#bytes(#bufSeg(#buf(32, YY8), 24, 8)),
#bytes(#buf({SIGNATURE_LENGTH}, SIGNATURE)),
#bytes(#bufSeg(#buf(32, Y8), 24, 8)) )))
GAS_COST: 55443
MEM_COST: {MU_DATA}
[deposit-success-insert]
WORD_STACK_INIT: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
LOOP_BOUND: 32
LOOP_INDEX_ADDR: 3360
[deposit-success-insert-init]
LOCAL_MEM_DATA: MEM
{VYPER_GENERATED_BOUNDS}
; locals
[ 2784 := #buf(32, {NODE}) ] /* node */
PRE_MEM_COST: {MU_DATA}
[deposit-success-insert-init-then]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: {PC_ADD_BEGIN} => {PC_ADD_END}
output: _ => .WordStack
word_stack: .WordStack
local_mem: {LOCAL_MEM_DATA} => _
storage: M => M
[ #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList) <- DEPOSIT_COUNT +Int 1 ]
[ #hashedLocation({COMPILER}, {BRANCH}, 0) <- {NODE} ]
refund: _ => _
+requires:
// conditions
andBool (DEPOSIT_COUNT +Int 1) &Int 1 ==Int 1
GAS_COST_MIN: 11019
GAS_COST_MAX: 41019
MEM_COST: {MU_ADD_ODD}
[deposit-success-insert-init-else]
pc: {PC_ADD_BEGIN} => {PC_ADD_LOOPHEAD}
word_stack: .WordStack => 1 : {WORD_STACK_INIT}
local_mem: {LOCAL_MEM_DATA} => NEW_MEM
+ensures:
{ENSURES_VYPER_GENERATED_BOUNDS}
andBool #range(NEW_MEM, 2784, 32) ==K #buf(32, {NODE_1})
andBool #range(NEW_MEM, 3328, 32) ==K #buf(32, (DEPOSIT_COUNT +Int 1) /Int 2)
andBool #range(NEW_MEM, 3360, 32) ==K #buf(32, 1)
NODE_1: #sha256(#buf(32, {BRANCH_0}) ++ #buf(32, {NODE}))
BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
storage: M => M
[ #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList) <- DEPOSIT_COUNT +Int 1 ]
refund: _ => _
+requires:
// conditions
andBool (DEPOSIT_COUNT +Int 1) &Int 1 =/=Int 1
GAS_COST_MIN: 7196
GAS_COST_MAX: 22196
MEM_COST: {MU_ADD_EVEN}
[deposit-success-insert-loop]
LOCAL_MEM_LOOPHEAD: MEM
{VYPER_GENERATED_BOUNDS}
; locals - invariants
[ 2784 := #buf(32, NODE) ] /* node */
[ 3328 := #buf(32, SIZE) ] /* size */
[ 3360 := #buf(32, HEIGHT) ] /* height */
+requires:
// conditions - invariants
andBool HEIGHT <=Int 32
// types
andBool #rangeUInt(256, NODE)
andBool #rangeUInt(256, SIZE)
andBool #rangeUInt(256, HEIGHT)
PRE_MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
[deposit-success-insert-loop-enter]
+requires:
// conditions
andBool HEIGHT =/=Int 32
[deposit-success-insert-loop-enter-then]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: {PC_ADD_LOOPHEAD} => {PC_ADD_END}
output: _ => .WordStack
word_stack: HEIGHT : {WORD_STACK_INIT} => .WordStack
local_mem: {LOCAL_MEM_LOOPHEAD} => _
storage: M => M
[ #hashedLocation({COMPILER}, {BRANCH}, HEIGHT) <- NODE ]
refund: _ => _
+requires:
// conditions
andBool SIZE &Int 1 ==Int 1
GAS_COST_MIN: 5162
GAS_COST_MAX: 20162
MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
[deposit-success-insert-loop-enter-else]
pc: {PC_ADD_LOOPHEAD}
word_stack: (HEIGHT => HEIGHT +Int 1) : {WORD_STACK_INIT}
local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
+ensures:
{ENSURES_VYPER_GENERATED_BOUNDS}
andBool #range(NEW_MEM, 2784, 32) ==K #buf(32, {NODE_NEW})
andBool #range(NEW_MEM, 3328, 32) ==K #buf(32, SIZE /Int 2)
andBool #range(NEW_MEM, 3360, 32) ==K #buf(32, HEIGHT +Int 1)
NODE_NEW: #sha256(#buf(32, {BRANCH_HEIGHT}) ++ #buf(32, NODE))
BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
+requires:
// conditions
andBool SIZE &Int 1 =/=Int 1
GAS_COST: 1339
MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
[deposit-success-insert-loop-exit]
k: #execute => #halt
status_code: _ => EVMC_SUCCESS
pc: {PC_ADD_LOOPHEAD} => {PC_ADD_END}
output: _ => .WordStack
word_stack: HEIGHT : {WORD_STACK_INIT} => .WordStack
local_mem: {LOCAL_MEM_LOOPHEAD}
+requires:
// conditions
andBool HEIGHT ==Int 32
GAS_COST: 27
MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
[deposit-revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
word_stack: .WordStack => _
local_mem: .Map => _
log: _ => _
[deposit-revert-1]
pc: 0 => 1691
+requires:
// conditions
andBool DEPOSIT_COUNT >=Int {MAX_DEPOSIT_COUNT}
GAS_COST: 620
MEM_COST: 672
[deposit-revert-2]
pc: 0 => 1743
+requires:
// conditions
andBool DEPOSIT_COUNT <Int {MAX_DEPOSIT_COUNT}
andBool CALL_VALUE /Int {GWEI_IN_WEI} <Int {MIN_DEPOSIT_AMOUNT}
GAS_COST: 697
MEM_COST: 768
[deposit-revert-3]
pc: 0 => 4018
+requires:
// conditions
andBool DEPOSIT_COUNT <Int {MAX_DEPOSIT_COUNT}
andBool CALL_VALUE /Int {GWEI_IN_WEI} >=Int {MIN_DEPOSIT_AMOUNT}
andBool {NODE} =/=Int DEPOSIT_DATA_ROOT
GAS_COST: 769 +Int 10925 +Int 12354 +Int 17029 +Int 14371
MEM_COST: {MU_DATA}
[deposit-calldata-decoding]
; arbitrary calldata including ill-formed one
call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
+requires:
// conditions
andBool {FUNCTION_SELECTOR} ==Int 579424536 /* 0x22895118 deposit */
andBool CALL_DATA_SIZE >=Int 4
// conditions
andBool DEPOSIT_COUNT <Int {MAX_DEPOSIT_COUNT}
andBool CALL_VALUE /Int {GWEI_IN_WEI} >=Int {MIN_DEPOSIT_AMOUNT}
;
CALLDATALOAD_0: #take(32, {CALL_DATA})
FUNCTION_SELECTOR: #asWord(#take(4, {CALLDATALOAD_0}))
;
PUBKEY_OFFSET: (4 +Word #asWord({CALL_DATA}[ 4 .. 32 ]))
WITHDRAWAL_CREDENTIALS_OFFSET: (4 +Word #asWord({CALL_DATA}[ 36 .. 32 ]))
SIGNATURE_OFFSET: (4 +Word #asWord({CALL_DATA}[ 68 .. 32 ]))
;
PUBKEY_ARRAY: ({CALL_DATA}[ {PUBKEY_OFFSET} .. (32 +Int {PUBKEY_LENGTH} ) ])
WITHDRAWAL_CREDENTIALS_ARRAY: ({CALL_DATA}[ {WITHDRAWAL_CREDENTIALS_OFFSET} .. (32 +Int {WITHDRAWAL_CREDENTIALS_LENGTH}) ])
SIGNATURE_ARRAY: ({CALL_DATA}[ {SIGNATURE_OFFSET} .. (32 +Int {SIGNATURE_LENGTH} ) ])
;
PUBKEY_ARRAY_SIZE: #asWord(#take(32, {PUBKEY_ARRAY}))
WITHDRAWAL_CREDENTIALS_ARRAY_SIZE: #asWord(#take(32, {WITHDRAWAL_CREDENTIALS_ARRAY}))
SIGNATURE_ARRAY_SIZE: #asWord(#take(32, {SIGNATURE_ARRAY}))
[deposit-calldata-decoding-success]
; until the length check
pc: 0 => {PC_SUBCALL_1}
word_stack: .WordStack
local_mem: .Map => .Map
; function hash
[ 28 := {CALLDATALOAD_0} ]
{VYPER_GENERATED_BOUNDS}
; load calldata
[ 320 := {PUBKEY_ARRAY} ]
[ 448 := {WITHDRAWAL_CREDENTIALS_ARRAY} ]
[ 544 := {SIGNATURE_ARRAY} ]
[ 736 := #buf(32, {GWEI_IN_WEI}) ] /* 1 gwei = 10^9 wei */
[ 704 := #buf(32, {DEPOSIT_AMOUNT}) ] /* deposit_amount: uint256 = msg.value / as_wei_value(1, "gwei") */
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} ==Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} ==Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} ==Int {SIGNATURE_LENGTH}
GAS_COST: 769
MEM_COST: {MU_INIT}
[deposit-calldata-decoding-revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
word_stack: .WordStack => _
local_mem: .Map => _
[deposit-calldata-decoding-revert-1]
pc: 0 => 1609
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} >Int {PUBKEY_LENGTH}
GAS_COST: 261
MEM_COST: 400
[deposit-calldata-decoding-revert-2]
pc: 0 => 1641
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} <=Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} >Int {WITHDRAWAL_CREDENTIALS_LENGTH}
GAS_COST: 326
MEM_COST: 512
[deposit-calldata-decoding-revert-3]
pc: 0 => 1673
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} <=Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} <=Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} >Int {SIGNATURE_LENGTH}
GAS_COST: 397
MEM_COST: 672
[deposit-calldata-decoding-revert-4]
pc: 0 => 1759
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} <=Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} <=Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} <=Int {SIGNATURE_LENGTH}
andBool {PUBKEY_ARRAY_SIZE} =/=Int {PUBKEY_LENGTH}
GAS_COST: 723
MEM_COST: 768
[deposit-calldata-decoding-revert-5]
pc: 0 => 1775
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} <=Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} <=Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} <=Int {SIGNATURE_LENGTH}
andBool {PUBKEY_ARRAY_SIZE} ==Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} =/=Int {WITHDRAWAL_CREDENTIALS_LENGTH}
GAS_COST: 749
MEM_COST: 768
[deposit-calldata-decoding-revert-6]
pc: 0 => 1791
+requires:
// conditions
andBool {PUBKEY_ARRAY_SIZE} <=Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} <=Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} <=Int {SIGNATURE_LENGTH}
andBool {PUBKEY_ARRAY_SIZE} ==Int {PUBKEY_LENGTH}
andBool {WITHDRAWAL_CREDENTIALS_ARRAY_SIZE} ==Int {WITHDRAWAL_CREDENTIALS_LENGTH}
andBool {SIGNATURE_ARRAY_SIZE} =/=Int {SIGNATURE_LENGTH}
GAS_COST: 775
MEM_COST: 768
;
; revert cases
;
[revert]
k: #execute => #halt
status_code: _ => EVMC_REVERT
; Revert if the first four bytes are invalid (or not fully provided).
[revert-invalid_function_identifier]
call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
pc: 0 => 4277
[revert-invalid_function_identifier-lt_4]
+requires:
// conditions
andBool #range(0 <= CALL_DATA_SIZE < 4)
GAS_COST: 42
MEM_COST: 0
[revert-invalid_function_identifier-ge_4]
+requires:
// conditions
andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 3321006383 /* 0xc5f2892f get_deposit_root */
andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 1646252336 /* 0x621fd130 get_deposit_count */
andBool #asWord(#bufSeg(#buf(CALL_DATA_SIZE, CALL_DATA), 0, 4)) =/=Int 579424536 /* 0x22895118 deposit */
GAS_COST: 196
MEM_COST: 192
[revert-invalid_function_identifier-ge_4-lt_32]
+requires:
// conditions
andBool #range(4 <= CALL_DATA_SIZE < 32)
[revert-invalid_function_identifier-ge_4-ge_32]
+requires:
// conditions
andBool CALL_DATA_SIZE >=Int 32
;
; globals
;
[pgm]
COMPILER: "Array"
; Storage variables:
; branch: bytes32[DEPOSIT_CONTRACT_TREE_DEPTH]
; deposit_count: uint256
; zero_hashes: bytes32[DEPOSIT_CONTRACT_TREE_DEPTH]
BRANCH: 0
DEPOSIT_COUNT: 1
ZERO_HASHES: 2
; Constants:
; MIN_DEPOSIT_AMOUNT: constant(uint256) = 1000000000 # Gwei
; DEPOSIT_CONTRACT_TREE_DEPTH: constant(uint256) = 32
; MAX_DEPOSIT_COUNT: constant(uint256) = 4294967295 # 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1
; PUBKEY_LENGTH: constant(uint256) = 48 # bytes
; WITHDRAWAL_CREDENTIALS_LENGTH: constant(uint256) = 32 # bytes
; AMOUNT_LENGTH: constant(uint256) = 8 # bytes
; SIGNATURE_LENGTH: constant(uint256) = 96 # bytes
DEPOSIT_CONTRACT_TREE_DEPTH: 32
; bytecode
RUNTIME_CODE: "0x600436101561000d576110b0565b600035601c52740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a05260001561027f575b6101605261014052600061018052610140516101a0526101c060006008818352015b61018051600860008112156100e8578060000360020a82046100ef565b8060020a82025b905090506101805260ff6101a051166101e052610180516101e0516101805101101561011a57600080fd5b6101e0516101805101610180526101a0517ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff86000811215610163578060000360020a820461016a565b8060020a82025b905090506101a0525b81516001018083528114156100cb575b5050601860086020820661020001602082840111156101a157600080fd5b60208061022082610180600060045af15050818152809050905090508051602001806102c08284600060045af16101d757600080fd5b50506102c05160206001820306601f82010390506103206102c0516020818352015b826103205110151561020a57610226565b6000610320516102e001535b81516001018083528114156101f9575b50505060206102a05260406102c0510160206001820306601f8201039050610280525b60006102805111151561025b57610277565b602061028051036102a001516020610280510361028052610249565b610160515650005b63c5f2892f600051141561050e57341561029857600080fd5b6000610140526101405161016052600154610180526101a060006020818352015b600160016101805116141561033a5760006101a051602081106102db57600080fd5b600060c052602060c02001546020826102400101526020810190506101605160208261024001015260208101905080610240526102409050602060c0825160208401600060025af161032c57600080fd5b60c0519050610160526103a8565b6000610160516020826101c00101526020810190506101a0516020811061036057600080fd5b600260c052602060c02001546020826101c0010152602081019050806101c0526101c09050602060c0825160208401600060025af161039e57600080fd5b60c0519050610160525b61018060026103b657600080fd5b60028151048152505b81516001018083528114156102b9575b505060006101605160208261046001015260208101905061014051610160516101805163806732896102e0526001546103005261030051600658016100a9565b506103605260006103c0525b6103605160206001820306601f82010390506103c05110151561043d57610456565b6103c05161038001526103c0516020016103c05261041b565b61018052610160526101405261036060088060208461046001018260208501600060045af150508051820191505060006018602082066103e001602082840111156104a057600080fd5b60208061040082610140600060045af150508181528090509050905060188060208461046001018260208501600060045af150508051820191505080610460526104609050602060c0825160208401600060025af16104fe57600080fd5b60c051905060005260206000f350005b63621fd130600051141561061c57341561052757600080fd5b6380673289610140526001546101605261016051600658016100a9565b506101c0526000610220525b6101c05160206001820306601f8201039050610220511015156105725761058b565b610220516101e001526102205160200161022052610550565b6101c08051602001806102808284600060045af16105a857600080fd5b50506102805160206001820306601f82010390506102e0610280516020818352015b826102e0511015156105db576105f7565b60006102e0516102a001535b81516001018083528114156105ca575b5050506020610260526040610280510160206001820306601f8201039050610260f350005b632289511860005114156110af57605060043560040161014037603060043560040135111561064a57600080fd5b60406024356004016101c037602060243560040135111561066a57600080fd5b608060443560040161022037606060443560040135111561068a57600080fd5b63ffffffff6001541061069c57600080fd5b633b9aca006102e0526102e0516106b257600080fd5b6102e05134046102c052633b9aca006102c05110156106d057600080fd5b603061014051146106e057600080fd5b60206101c051146106f057600080fd5b6060610220511461070057600080fd5b610140610360525b6103605151602061036051016103605261036061036051101561072a57610708565b6380673289610380526102c0516103a0526103a051600658016100a9565b50610400526000610460525b6104005160206001820306601f8201039050610460511015156107765761078f565b6104605161042001526104605160200161046052610754565b610340610360525b61036051526020610360510361036052610140610360511015156107ba57610797565b6104008051602001806103008284600060045af16107d757600080fd5b5050610140610480525b61048051516020610480510161048052610480610480511015610803576107e1565b63806732896104a0526001546104c0526104c051600658016100a9565b50610520526000610580525b6105205160206001820306601f82010390506105805110151561084e57610867565b610580516105400152610580516020016105805261082c565b610460610480525b61048051526020610480510361048052610140610480511015156108925761086f565b6105208051602001806105a08284600060045af16108af57600080fd5b505060a061062052610620516106605261014080516020018061062051610660018284600060045af16108e157600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516040818352015b826106005110151561091e5761093f565b600061060051610620516106800101535b815160010180835281141561090d575b505050602061062051610660015160206001820306601f82010390506106205101016106205261062051610680526101c080516020018061062051610660018284600060045af161098f57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b82610600511015156109cc576109ed565b600061060051610620516106800101535b81516001018083528114156109bb575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106a05261030080516020018061062051610660018284600060045af1610a3d57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b8261060051101515610a7a57610a9b565b600061060051610620516106800101535b8151600101808352811415610a69575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106c05261022080516020018061062051610660018284600060045af1610aeb57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516060818352015b8261060051101515610b2857610b49565b600061060051610620516106800101535b8151600101808352811415610b17575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106e0526105a080516020018061062051610660018284600060045af1610b9957600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b8261060051101515610bd657610bf7565b600061060051610620516106800101535b8151600101808352811415610bc5575b505050602061062051610660015160206001820306601f8201039050610620510101610620527f649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c561062051610660a160006107005260006101406030806020846107c001018260208501600060045af150508051820191505060006010602082066107400160208284011115610c8c57600080fd5b60208061076082610700600060045af15050818152809050905090506010806020846107c001018260208501600060045af1505080518201915050806107c0526107c09050602060c0825160208401600060025af1610cea57600080fd5b60c0519050610720526000600060406020820661086001610220518284011115610d1357600080fd5b6060806108808260206020880688030161022001600060045af1505081815280905090509050602060c0825160208401600060025af1610d5257600080fd5b60c0519050602082610a600101526020810190506000604060206020820661092001610220518284011115610d8657600080fd5b6060806109408260206020880688030161022001600060045af15050818152809050905090506020806020846109e001018260208501600060045af1505080518201915050610700516020826109e0010152602081019050806109e0526109e09050602060c0825160208401600060025af1610e0157600080fd5b60c0519050602082610a6001015260208101905080610a6052610a609050602060c0825160208401600060025af1610e3857600080fd5b60c0519050610840526000600061072051602082610b000101526020810190506101c0602080602084610b0001018260208501600060045af150508051820191505080610b0052610b009050602060c0825160208401600060025af1610e9d57600080fd5b60c0519050602082610c800101526020810190506000610300600880602084610c0001018260208501600060045af15050805182019150506000601860208206610b800160208284011115610ef157600080fd5b602080610ba082610700600060045af1505081815280905090509050601880602084610c0001018260208501600060045af150508051820191505061084051602082610c0001015260208101905080610c0052610c009050602060c0825160208401600060025af1610f6257600080fd5b60c0519050602082610c8001015260208101905080610c8052610c809050602060c0825160208401600060025af1610f9957600080fd5b60c0519050610ae052606435610ae05114610fb357600080fd5b6001805460018254011015610fc757600080fd5b6001815401815550600154610d0052610d2060006020818352015b60016001610d005116141561101757610ae051610d20516020811061100657600080fd5b600060c052602060c02001556110ab565b6000610d20516020811061102a57600080fd5b600060c052602060c0200154602082610d40010152602081019050610ae051602082610d4001015260208101905080610d4052610d409050602060c0825160208401600060025af161107b57600080fd5b60c0519050610ae052610d00600261109257600080fd5b60028151048152505b8151600101808352811415610fe2575b5050005b5b60006000fd"
INIT_CODE: "0x740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a052341561009857600080fd5b6101406000601f818352015b600061014051602081106100b757600080fd5b600260c052602060c020015460208261016001015260208101905061014051602081106100e357600080fd5b600260c052602060c020015460208261016001015260208101905080610160526101609050602060c0825160208401600060025af161012157600080fd5b60c0519050606051600161014051018060405190131561014057600080fd5b809190121561014e57600080fd5b6020811061015b57600080fd5b600260c052602060c02001555b81516001018083528114156100a4575b505061123556600436101561000d576110b0565b600035601c52740100000000000000000000000000000000000000006020526f7fffffffffffffffffffffffffffffff6040527fffffffffffffffffffffffffffffffff8000000000000000000000000000000060605274012a05f1fffffffffffffffffffffffffdabf41c006080527ffffffffffffffffffffffffed5fa0e000000000000000000000000000000000060a05260001561027f575b6101605261014052600061018052610140516101a0526101c060006008818352015b61018051600860008112156100e8578060000360020a82046100ef565b8060020a82025b905090506101805260ff6101a051166101e052610180516101e0516101805101101561011a57600080fd5b6101e0516101805101610180526101a0517ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff86000811215610163578060000360020a820461016a565b8060020a82025b905090506101a0525b81516001018083528114156100cb575b5050601860086020820661020001602082840111156101a157600080fd5b60208061022082610180600060045af15050818152809050905090508051602001806102c08284600060045af16101d757600080fd5b50506102c05160206001820306601f82010390506103206102c0516020818352015b826103205110151561020a57610226565b6000610320516102e001535b81516001018083528114156101f9575b50505060206102a05260406102c0510160206001820306601f8201039050610280525b60006102805111151561025b57610277565b602061028051036102a001516020610280510361028052610249565b610160515650005b63c5f2892f600051141561050e57341561029857600080fd5b6000610140526101405161016052600154610180526101a060006020818352015b600160016101805116141561033a5760006101a051602081106102db57600080fd5b600060c052602060c02001546020826102400101526020810190506101605160208261024001015260208101905080610240526102409050602060c0825160208401600060025af161032c57600080fd5b60c0519050610160526103a8565b6000610160516020826101c00101526020810190506101a0516020811061036057600080fd5b600260c052602060c02001546020826101c0010152602081019050806101c0526101c09050602060c0825160208401600060025af161039e57600080fd5b60c0519050610160525b61018060026103b657600080fd5b60028151048152505b81516001018083528114156102b9575b505060006101605160208261046001015260208101905061014051610160516101805163806732896102e0526001546103005261030051600658016100a9565b506103605260006103c0525b6103605160206001820306601f82010390506103c05110151561043d57610456565b6103c05161038001526103c0516020016103c05261041b565b61018052610160526101405261036060088060208461046001018260208501600060045af150508051820191505060006018602082066103e001602082840111156104a057600080fd5b60208061040082610140600060045af150508181528090509050905060188060208461046001018260208501600060045af150508051820191505080610460526104609050602060c0825160208401600060025af16104fe57600080fd5b60c051905060005260206000f350005b63621fd130600051141561061c57341561052757600080fd5b6380673289610140526001546101605261016051600658016100a9565b506101c0526000610220525b6101c05160206001820306601f8201039050610220511015156105725761058b565b610220516101e001526102205160200161022052610550565b6101c08051602001806102808284600060045af16105a857600080fd5b50506102805160206001820306601f82010390506102e0610280516020818352015b826102e0511015156105db576105f7565b60006102e0516102a001535b81516001018083528114156105ca575b5050506020610260526040610280510160206001820306601f8201039050610260f350005b632289511860005114156110af57605060043560040161014037603060043560040135111561064a57600080fd5b60406024356004016101c037602060243560040135111561066a57600080fd5b608060443560040161022037606060443560040135111561068a57600080fd5b63ffffffff6001541061069c57600080fd5b633b9aca006102e0526102e0516106b257600080fd5b6102e05134046102c052633b9aca006102c05110156106d057600080fd5b603061014051146106e057600080fd5b60206101c051146106f057600080fd5b6060610220511461070057600080fd5b610140610360525b6103605151602061036051016103605261036061036051101561072a57610708565b6380673289610380526102c0516103a0526103a051600658016100a9565b50610400526000610460525b6104005160206001820306601f8201039050610460511015156107765761078f565b6104605161042001526104605160200161046052610754565b610340610360525b61036051526020610360510361036052610140610360511015156107ba57610797565b6104008051602001806103008284600060045af16107d757600080fd5b5050610140610480525b61048051516020610480510161048052610480610480511015610803576107e1565b63806732896104a0526001546104c0526104c051600658016100a9565b50610520526000610580525b6105205160206001820306601f82010390506105805110151561084e57610867565b610580516105400152610580516020016105805261082c565b610460610480525b61048051526020610480510361048052610140610480511015156108925761086f565b6105208051602001806105a08284600060045af16108af57600080fd5b505060a061062052610620516106605261014080516020018061062051610660018284600060045af16108e157600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516040818352015b826106005110151561091e5761093f565b600061060051610620516106800101535b815160010180835281141561090d575b505050602061062051610660015160206001820306601f82010390506106205101016106205261062051610680526101c080516020018061062051610660018284600060045af161098f57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b82610600511015156109cc576109ed565b600061060051610620516106800101535b81516001018083528114156109bb575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106a05261030080516020018061062051610660018284600060045af1610a3d57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b8261060051101515610a7a57610a9b565b600061060051610620516106800101535b8151600101808352811415610a69575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106c05261022080516020018061062051610660018284600060045af1610aeb57600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516060818352015b8261060051101515610b2857610b49565b600061060051610620516106800101535b8151600101808352811415610b17575b505050602061062051610660015160206001820306601f820103905061062051010161062052610620516106e0526105a080516020018061062051610660018284600060045af1610b9957600080fd5b505061062051610660015160206001820306601f82010390506106006106205161066001516020818352015b8261060051101515610bd657610bf7565b600061060051610620516106800101535b8151600101808352811415610bc5575b505050602061062051610660015160206001820306601f8201039050610620510101610620527f649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c561062051610660a160006107005260006101406030806020846107c001018260208501600060045af150508051820191505060006010602082066107400160208284011115610c8c57600080fd5b60208061076082610700600060045af15050818152809050905090506010806020846107c001018260208501600060045af1505080518201915050806107c0526107c09050602060c0825160208401600060025af1610cea57600080fd5b60c0519050610720526000600060406020820661086001610220518284011115610d1357600080fd5b6060806108808260206020880688030161022001600060045af1505081815280905090509050602060c0825160208401600060025af1610d5257600080fd5b60c0519050602082610a600101526020810190506000604060206020820661092001610220518284011115610d8657600080fd5b6060806109408260206020880688030161022001600060045af15050818152809050905090506020806020846109e001018260208501600060045af1505080518201915050610700516020826109e0010152602081019050806109e0526109e09050602060c0825160208401600060025af1610e0157600080fd5b60c0519050602082610a6001015260208101905080610a6052610a609050602060c0825160208401600060025af1610e3857600080fd5b60c0519050610840526000600061072051602082610b000101526020810190506101c0602080602084610b0001018260208501600060045af150508051820191505080610b0052610b009050602060c0825160208401600060025af1610e9d57600080fd5b60c0519050602082610c800101526020810190506000610300600880602084610c0001018260208501600060045af15050805182019150506000601860208206610b800160208284011115610ef157600080fd5b602080610ba082610700600060045af1505081815280905090509050601880602084610c0001018260208501600060045af150508051820191505061084051602082610c0001015260208101905080610c0052610c009050602060c0825160208401600060025af1610f6257600080fd5b60c0519050602082610c8001015260208101905080610c8052610c809050602060c0825160208401600060025af1610f9957600080fd5b60c0519050610ae052606435610ae05114610fb357600080fd5b6001805460018254011015610fc757600080fd5b6001815401815550600154610d0052610d2060006020818352015b60016001610d005116141561101757610ae051610d20516020811061100657600080fd5b600060c052602060c02001556110ab565b6000610d20516020811061102a57600080fd5b600060c052602060c0200154602082610d40010152602081019050610ae051602082610d4001015260208101905080610d4052610d409050602060c0825160208401600060025af161107b57600080fd5b60c0519050610ae052610d00600261109257600080fd5b60028151048152505b8151600101808352811415610fe2575b5050005b5b60006000fd5b61017f6112350361017f60003961017f611235036000f3"