miden-stdlib 0.19.1

Miden VM standard library
Documentation
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
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
use.std::math::ecgfp5::base_field

#! Given an encoded elliptic curve point `w` s.t. it's expressed using
#! an element ∈ GF(p^5) | p = 2^64 - 2^32 + 1, this routine verifies whether
#! given point can be successfully decoded or not
#!
#! Expected stack state
#!
#! [w0, w1, w2, w3, w4, ...]
#!
#! Final stack state
#!
#! [flg, ...]
#!
#! If w can be decoded, flg = 1
#! Else flg = 0
#!
#! Note, if w = (0, 0, 0, 0, 0), it can be successfully decoded to point
#! at infinity i.e. flg = 1, in that case.
#!
#! See https://github.com/pornin/ecgfp5/blob/ce059c6/python/ecGFp5.py#L1043-L1052
#! for reference implementation
export.validate
    repeat.5
        dup.4
    end

    exec.base_field::square
    sub.2 # = e

    exec.base_field::square
    swap
    sub.1052
    swap # = delta

    exec.base_field::legendre
    eq.1
    movdn.5

    push.1
    repeat.5
        swap
        eq.0
        and
    end

    or
end

#! Given an encoded elliptic curve point `w` s.t. it's expressed using
#! an element ∈ GF(p^5) | p = 2^64 - 2^32 + 1, this routine attempts to decode
#! it into x, y coordinates, along with boolean field element denoting whether it's
#! point-at-infinity or not.
#!
#! Expected stack state
#!
#! [w0, w1, w2, w3, w4, ...]
#!
#! Final state state
#!
#! [x0, x1, x2, x3, x4, y0, y1, y2, y3, y4, inf, flg, ...]
#!
#! If `w` has be decoded, flg = 1
#! Else flg = 0 and x, y = (0, 0)
#!
#! Note, when w = (0, 0, 0, 0, 0), it will be successfully decoded to
#! point-at-infinity i.e. x, y = (0, 0) and flg = 1
#!
#! See https://github.com/pornin/ecgfp5/blob/ce059c6/python/ecGFp5.py#L1022-L1041
#! for reference implementation
export.decode
    repeat.5
        dup.4
    end

    exec.base_field::square
    sub.2 # = e

    repeat.5
        dup.4
    end

    exec.base_field::square
    swap
    sub.1052
    swap # = delta

    exec.base_field::sqrt # = (r, c)

    repeat.5
        dup.10
    end

    repeat.5
        dup.9
    end

    exec.base_field::add
    push.0.0.0.0.9223372034707292161
    exec.base_field::mul # = x1

    repeat.5
        movup.9
    end

    repeat.5
        movup.15
    end

    exec.base_field::sub
    push.0.0.0.0.9223372034707292161
    exec.base_field::mul # = x2

    repeat.5
        movup.9
    end

    repeat.5
        dup.4
    end

    exec.base_field::legendre
    eq.1

    if.true
        repeat.5
            movup.5
            drop
        end
    else
        repeat.5
            drop
        end
    end # = x

    repeat.5
        dup.10
    end

    repeat.5
        dup.9
    end

    exec.base_field::mul
    repeat.5
        movup.4
        neg
    end # = y

    dup.10
    not # = inf

    push.1
    repeat.5
        movup.13
        eq.0
        and
    end

    movup.12
    or # = c

    swap

    repeat.5
        movup.6
    end

    repeat.5
        movup.11
    end

    add.6148914689804861441 # = x
end

#! Given an elliptic curve point as Weierstraß coordinates (X, Y) along with
#! boolean field element `inf`, denoting whether this is point-at-infinity or not,
#! this routine encodes it to a single element ∈ GF(p^5) | p = 2^64 - 2^32 + 1
#!
#! Expected stack state
#!
#! [x0, x1, x2, x3, x4, y0, y1, y2, y3, y4, inf, ...]
#!
#! Final stack state
#!
#! [w0, w1, w2, w3, w4, ...]
#!
#! Note, when inf = 1, encoded point w = (0, 0, 0, 0, 0)
#!
#! See https://github.com/pornin/ecgfp5/blob/ce059c6/python/ecGFp5.py#L1214-L1216
#! for reference implementation.
export.encode
    push.0.0.0.0.6148914689804861441 # = a/ 3

    exec.base_field::sub # = (a/ 3) - x

    repeat.5
        movup.9
    end

    exec.base_field::div # = w = y/ ((a/ 3) - x)

    movup.5
    if.true
        repeat.5
            drop
        end

        push.0.0.0.0.0
    end
end

#! Given two elliptic curve points ( say a, b ) as Weierstraß coordinates (X, Y) on stack,
#! this routine computes elliptic curve point c, resulting from a + b.
#!
#! Following point addition formula is complete and it works when two points are
#! same/ different or input operands are point-at-infinity.
#!
#! Expected stack state
#!
#! [x1_0, x1_1, x1_2, x1_3, x1_4, y1_0, y1_1, y1_2, y1_3, y1_4, inf1, x2_0, x2_1, x2_2, x2_3, x2_4, y2_0, y2_1, y2_2, y2_3, y2_4, inf2, ...]
#!
#! s.t. x1_{0..5} -> x1, y1_{0..5} -> y1 |> a = (x1, y1, inf1)
#!      x2_{0..5} -> x2, y2_{0..5} -> y2 |> b = (x2, y2, inf2)
#!
#! Final stack state
#!
#! [x3_0, x3_1, x3_2, x3_3, x3_4, y3_0, y3_1, y3_2, y3_3, y3_4, inf3, ...]
#!
#! Read point addition section ( on page 8 ) of https://ia.cr/2022/274
#! For reference implementation see https://github.com/pornin/ecgfp5/blob/ce059c6/python/ecGFp5.py#L1228-L1255
export.add.40
    loc_storew_be.0
    dropw
    loc_store.4 # cached x1

    loc_storew_be.8
    dropw
    loc_store.12 # cached y1

    loc_store.16 # cached inf1

    loc_storew_be.20
    dropw
    loc_store.24 # cached x2

    loc_storew_be.28
    dropw
    loc_store.32 # cached y2

    loc_store.36 # cached inf2

    loc_load.24
    push.0.0.0.0
    loc_loadw_be.20 # bring x2

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x1

    exec.base_field::eq
    dup

    if.true
        loc_load.4
        push.0.0.0.0
        loc_loadw_be.0 # bring x1

        exec.base_field::square

        repeat.5
            movup.4
            mul.3
        end

        add.6148914689804861439
        swap
        add.263
        swap
    else
        loc_load.12
        push.0.0.0.0
        loc_loadw_be.8 # bring y1

        loc_load.32
        push.0.0.0.0
        loc_loadw_be.28 # bring y2

        exec.base_field::sub
    end # = λ0

    dup.5

    if.true
        loc_load.12
        push.0.0.0.0
        loc_loadw_be.8 # bring y1

        repeat.5
            movup.4
            mul.2
        end
    else
        loc_load.4
        push.0.0.0.0
        loc_loadw_be.0 # bring x1

        loc_load.24
        push.0.0.0.0
        loc_loadw_be.20 # bring x2

        exec.base_field::sub
    end # = λ1

    repeat.5
        movup.9
    end

    exec.base_field::div # = λ

    repeat.5
        dup.4
    end

    exec.base_field::square # = λ^2

    loc_load.24
    push.0.0.0.0
    loc_loadw_be.20 # bring x2

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x1

    exec.base_field::add

    repeat.5
        movup.9
    end

    exec.base_field::sub # compute x3

    repeat.5
        dup.4
    end

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x1

    exec.base_field::sub

    repeat.5
        movup.14
    end

    exec.base_field::mul

    loc_load.12
    push.0.0.0.0
    loc_loadw_be.8 # bring y1

    repeat.5
        movup.9
    end

    exec.base_field::sub # compute y3

    movup.10

    loc_load.12
    push.0.0.0.0
    loc_loadw_be.8 # bring y1

    loc_load.32
    push.0.0.0.0
    loc_loadw_be.28 # bring y2

    exec.base_field::neq

    and # compute inf3

    movdn.5

    # finalize selection of y3

    loc_load.32
    push.0.0.0.0
    loc_loadw_be.28 # bring y2

    loc_load.16 # bring inf1

    if.true
        repeat.5
            movup.5
            drop
        end
    else
        repeat.5
            drop
        end
    end

    loc_load.12
    push.0.0.0.0
    loc_loadw_be.8 # bring y1

    loc_load.36 # bring inf2

    if.true
        repeat.5
            movup.5
            drop
        end
    else
        repeat.5
            drop
        end
    end

    # finalize selection of x3

    repeat.5
        movup.10
    end

    loc_load.24
    push.0.0.0.0
    loc_loadw_be.20 # bring x2

    loc_load.16 # bring inf1

    if.true
        repeat.5
            movup.5
            drop
        end
    else
        repeat.5
            drop
        end
    end

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x1

    loc_load.36 # bring inf2

    if.true
        repeat.5
            movup.5
            drop
        end
    else
        repeat.5
            drop
        end
    end

    # finalize selection of inf3

    movup.10
    loc_load.36 # bring inf2
    loc_load.16 # bring inf1
    cdrop

    loc_load.16 # bring inf1
    loc_load.36 # bring inf2
    cdrop

    movdn.10
end

#! Given one elliptic curve point ( say a ) as Weierstraß coordinates (X, Y) on stack,
#! this routine computes elliptic curve point b s.t. b = 2 * a.
#!
#! Following point doubling formula is complete and it works only when input operand is
#! a non-infinity point, then resulting point b should also be non-infinity.
#!
#! Note, result of add(a, b) = double(a) | a = b
#!
#! Expected stack state
#!
#! [x0, x1, x2, x3, x4, y0, y1, y2, y3, y4, inf, ...]
#!
#! s.t. x{0..5} -> x, y{0..5} -> y |> a = (x, y, inf)
#!
#! Final stack state
#!
#! [x'0, x'1, x'2, x'3, x'4, y'0, y'1, y'2, y'3, y'4, inf, ...]
#!
#! Read point addition section ( on page 8 ) of https://ia.cr/2022/274
#! For reference implementation see https://github.com/pornin/ecgfp5/blob/ce059c6/python/ecGFp5.py#L1270-L1280
export.double.20
    loc_storew_be.0
    dropw
    loc_store.4 # cached x

    loc_storew_be.8
    dropw
    loc_store.12 # cached y

    loc_store.16 # cached inf

    loc_load.12
    push.0.0.0.0
    loc_loadw_be.8 # bring y

    repeat.5
        movup.4
        mul.2
    end # compute λ1

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x

    exec.base_field::square

    repeat.5
        movup.4
        mul.3
    end

    add.6148914689804861439
    swap
    add.263
    swap # compute λ0

    exec.base_field::div # compute λ

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x

    repeat.5
        movup.4
        mul.2
    end

    repeat.5
        dup.9
    end

    exec.base_field::square
    exec.base_field::sub # compute x'

    repeat.5
        dup.4
    end

    loc_load.4
    push.0.0.0.0
    loc_loadw_be.0 # bring x

    exec.base_field::sub

    repeat.5
        movup.14
    end

    exec.base_field::mul

    loc_load.12
    push.0.0.0.0
    loc_loadw_be.8 # bring y

    repeat.5
        movup.9
    end

    exec.base_field::sub # compute y'

    repeat.5
        movup.9
    end

    loc_load.16
    movdn.10
end

#! Given an elliptic curve point ( say a ) as Weierstraß coordinates (X, Y) and a 319 -bit scalar ( say e )
#! on stack, this routine computes elliptic curve point b s.t. b =  e * a, using double-and-add technique.
#!
#! Scalar e should be lesser than 1067993516717146951041484916571792702745057740581727230159139685185762082554198619328292418486241 ( prime number ).
#! Note, scalar e should be provided as 10 limbs on stack, each of 32 -bit, representing it in radix-2^32 form.
#!
#! Given a scalar e ( as arbitrary width big integer ), following python code snippet should convert it to desired input form
#!
#! [(a >> (32*i)) & 0xffff_ffff for i in range(10)]
#!
#! Expected stack state
#!
#! [x0, x1, x2, x3, x4, y0, y1, y2, y3, y4, inf, e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, ...]
#!
#! Point a = (x, y, inf)
#! Scalar e = (e0, e1, e2, e3, e4, e5, e6, e7, e8, e9)
#!
#! Final stack state
#!
#! [x'0, x'1, x'2, x'3, x'4, y'0, y'1, y'2, y'3, y'4, inf, ...]
#!
#! Point b = (x', y' inf') | b = e * a
#!
#! See https://github.com/itzmeanjan/secp256k1/blob/cbbe199/point.py#L174-L186 for source of inpiration.
export.mul.40
    loc_storew_be.0
    dropw
    loc_store.4 # cached base_x

    loc_storew_be.8
    dropw
    loc_store.12 # cached base_y

    loc_store.16 # cached base_inf

    push.0.0.0.0
    loc_storew_be.20
    dropw
    push.0
    loc_store.24 # initialize and cache res_x

    push.0.0.0.0
    loc_storew_be.28
    dropw
    push.0
    loc_store.32 # initialize and cache res_y

    push.1
    loc_store.36 # initialize and cache res_inf

    repeat.10
        repeat.32
            dup
            push.1
            u32and

            if.true
                # bring base
                loc_load.16

                loc_load.12
                push.0.0.0.0
                loc_loadw_be.8

                loc_load.4
                push.0.0.0.0
                loc_loadw_be.0

                # bring res
                loc_load.36

                loc_load.32
                push.0.0.0.0
                loc_loadw_be.28

                loc_load.24
                push.0.0.0.0
                loc_loadw_be.20

                exec.add

                # write back res
                loc_storew_be.20
                dropw
                loc_store.24

                loc_storew_be.28
                dropw
                loc_store.32

                loc_store.36
            end

            # bring base
            loc_load.16

            loc_load.12
            push.0.0.0.0
            loc_loadw_be.8

            loc_load.4
            push.0.0.0.0
            loc_loadw_be.0

            exec.double

            # write back base
            loc_storew_be.0
            dropw
            loc_store.4

            loc_storew_be.8
            dropw
            loc_store.12

            loc_store.16

            u32shr.1
        end

        drop
    end

    # bring res
    loc_load.36

    loc_load.32
    push.0.0.0.0
    loc_loadw_be.28

    loc_load.24
    push.0.0.0.0
    loc_loadw_be.20
end

#! Given a 319 -bit scalar ( say e ) on stack, this routine computes elliptic curve point
#! b s.t. b =  e * G, using double-and-add technique | G = conventional group generator point.
#!
#! Group generator point https://github.com/pornin/ecgfp5/blob/ce059c6/rust/src/curve.rs#L67-L83
#!
#! Scalar e should be lesser than N ( = 1067993516717146951041484916571792702745057740581727230159139685185762082554198619328292418486241 ).
#! Note, scalar e should be provided as 10 limbs on stack, each of 32 -bit, representing it in radix-2^32 form.
#!
#! Given a 319 -bit scalar e, following python code snippet should convert it to
#! desired input form i.e. radix-2^32 representation, having ten 32 -bit limbs
#!
#! [(e >> (32*i)) & 0xffff_ffff for i in range(10)]
#!
#! Expected stack state
#!
#! [e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, ...]
#!
#! Scalar e = (e0, e1, e2, e3, e4, e5, e6, e7, e8, e9)
#!
#! Final stack state
#!
#! [x0, x1, x2, x3, x4, y0, y1, y2, y3, y4, inf, ...]
#!
#! Point b = (x, y, inf) | b = e * G
#!
#! See https://github.com/itzmeanjan/secp256k1/blob/cbbe199/point.py#L174-L186 for source of inpiration.
export.gen_mul.32
    loc_storew_be.0
    dropw
    loc_storew_be.4
    dropw
    push.0.0
    movup.3
    movup.3
    loc_storew_be.8
    dropw # cache 319 -bit scalar, having 10 limbs, each of 32 -bit width

    push.0.0.0.0.0
    loc_storew_be.12
    dropw
    loc_store.16 # initialize and cache res_x

    push.0.0.0.0.0
    loc_storew_be.20
    dropw
    loc_store.24 # initialize and cache res_y

    push.1
    loc_store.28 # initialize and cache res_inf

    push.0.8623373087021137817.12280941316336150722.16498106075800537106.17561351883262171669.14191612778916076371.18286383079848041790.5863339128417000744.11451759428629996034.14179124258460441178.4768624678334228939
    push.0.16248535820734672314.12843058077554438509.14604603115652880441.1861370543582612103.12413761366396265525.4176022593458990041.3883454194479152564.14208568149880154517.30496475895846659.10372352552633189742
    push.0.2877809984845595236.8124729848406989261.2903444924486455483.6139401771336820486.11258486910517561409.11269995078679563195.4075713964805364983.11272694349658053421.17286345916541825175.5239921069304273244
    push.0.17641185070824107975.14889445785061292430.7405791732550181507.4195033912468829473.5893024420900179836.9198199668142261635.13255077950461830861.3315714462260585145.5358622364758307393.721593612819002908
    push.0.17218153792253988554.398898134320123335.14691321837712781231.14813642725547346961.7022468048599869463.13425501193148363047.8102520424076163562.4818391030611537206.3117791970810252983.3664867151911665097
    push.0.9768740144997694838.18337438909916942052.13287690569608682189.1749912136742008160.16874873892224416289.13753848043314362441.4990704782108972448.15940429530085642075.10014152261700797213.8271724616203496328
    push.0.15137575290038364568.834448034475692680.17725871744982540755.17720761966581073520.15617784849739721933.13143846705867213452.6387719880838102748.15637132133232092065.17395668299430845447.4976508673457147220
    push.0.14448869278120871938.2440192432902894712.9065627619858283302.7476463190805008531.12433592364249876790.7326369368968030334.10492708378186270656.8590652592090351714.11478014260122655233.5102808632757846047
    push.0.9652768576975789451.2169826252445647515.8515692953826676326.12790755226033428483.10499532484372206399.1752808319082265622.1461287152438866664.16156917747677348345.1913114203733512691.4220966228724218121
    push.0.15678769274395291067.3644569546435216629.8279510540289007754.14347910311032351181.11017801090920149683.17092277456226211965.16027019793415245260.6242090196981371796.13195765456550520156.18329307820651300136
    push.0.15660277884414351657.4747038350935563407.16563445468461400225.9202649824211012050.16989226289451019470.16269357368883802812.14601257932273902054.11922650544629087011.3837671014910122842.10542030917794106031
    push.0.16679682878508344885.4260113432582040236.6657572838446037989.17057619578187970416.9557888942099085229.16766876175803959905.8797349954628290450.9735674650584728206.16707168790898826743.2957163603751591175
    push.0.12731950592067067806.15132000389362928180.2301212109204980010.11858193693385253107.2787225233368024015.15608358023222707950.5664305148663915403.14236763768002019539.11718445275434263967.10887359501593613247
    push.0.12906063996958603900.1561861388017124445.9769071188656310541.9108206805299149795.828335823705130147.11630764285144089035.13798633568618668074.10120521355198906717.78547975849802565.9032713792450238388
    push.0.2932017870248423748.12862241115656865401.5691212362156829751.10513473720672864882.5811042078412067511.458337204753456641.13679640590869584883.3442439947769535104.10679288079271307010.16403385062095364376
    push.0.2960040779968781381.13743098123458581162.16796911018466257282.3963340258774352059.9493732769165536890.17565729304514950270.14558776703731825254.16603544858443598146.1290832334148046531.7196562104405968541
    push.0.12121575497725661883.16189154896554038370.713702076670502983.2511512527285855394.13074864091280271682.11226573117410114168.4334454122606443001.7823766160466615569.18258517404340224673.12260059464719152256
    push.0.6346101384116280016.17164907193019931643.6403805942282737631.2083047126212086181.15943828273518998540.14240418992504638979.959753680948073425.8797147096983019241.7835785575038815398.15427624465125434692
    push.0.289487472969449713.7875160791236525843.12277145790039167649.18340877018641812993.6669569099586313850.14033385862453802.1174914055793702087.17415867199848812284.12669785880287947992.17495080701629382991
    push.0.8312474118415594556.17907937811574560916.10199001911441156238.11406737362222088800.2978515999920985364.14117192075707323389.10658282210448969656.16696421864516574633.622946243598315577.6442977565493598461
    push.0.18351472755182604550.16873674670332592583.1563426283613098292.16756748498537513640.14150263400191053032.1341383961252998455.12682656025562029354.5988476299461316127.5003803280331938898.16040296516099617960
    push.0.17061741124372913585.1685517822595566267.11099523891222411303.17250161943873998632.92945368961976693.13734055188975953503.10599373628724574420.6688494610312667763.13395241382485607827.13188962304379802595
    push.0.14219042473548823122.16216446370123013057.16028324452314988099.8714729969909028741.17027248534572731013.14534640172031385920.7362562012151593348.12208216257811606410.4252893734082308717.1703418601781259457
    push.0.4327014058376986430.1989617576454441185.1762425062520246326.8465008486473703298.16612594338393994722.9346295873342903705.1650163609981138955.7064315547374207309.3647735235091486966.18050653732501273022
    push.0.549796731310882534.1603781472524072864.12322717272381784961.9791339617885668528.13609270885807643295.13973128232255143098.3075309866542652504.11287711595069922922.14906898503114723002.9018422534148817683
    push.0.5544292075173465445.17952569876806069683.18294583522852322863.7812549498388434524.12594732407823086256.14289194414874100732.8930653582416781286.8702229830945709567.3138314885098236703.5920543334908822938
    push.0.3153500519832367508.14077036784943875784.1776933306225717452.14704425337845754335.8267614728378424246.10769687165686737547.7751523064157770335.6966945298287528097.12931704222567970796.3025181988566097704
    push.0.8104254083834326172.13133237861876174994.2623380753280966679.3440846558577007338.1726232218948619174.14866452736934728304.12516807123009820976.15728197516974733460.16273434968704813505.11037870722440096277
    push.0.11785794741732599626.4205023480681749416.17927651849010052824.9733182900520580654.288031737419838077.4448206481663199216.11999152469828680564.8857433406265399786.16516818218126789744.4342958020584848363
    push.0.14183479619639204891.3799429333187611668.8435429517592671714.13727522106192075677.5822420820081854242.14547233627061294881.5209670832297188306.5630140225745987591.6622781811127690246.1918824110042959015
    push.0.1880749288582535681.16683745163638810921.12466587786369253147.16848428482855375174.3518953767950107533.17983405729116057463.17814892798307066676.2535272740463466201.8230480698157677872.14499162082108138760
    push.0.1916302979603865898.8260178889288550478.26646499599159667.6301450493669887243.4704592818468457027.3908448918630378442.2951407287916727020.11110183886947753091.3154854593170713809.13522061651280905730
    push.0.6820196283502870734.3102708866067456318.14778661640140328917.6265925189214458721.16407809039032430325.1914874522575114695.12764338970584691378.9964703541572957027.7417854382688285327.9382699433915759531
    push.0.5207156023373438265.14525260509106062772.2395711405008193548.6757621780178838077.7776513170818222902.15947526148356376380.16320951159783047591.4292695067569121966.16989995385967173035.14895669740211022315
    push.0.3034843963505367168.15748334406182774163.10636103071641746522.7559527801201479644.1336696995896848644.2803777364610216952.11659714261208125526.10724770875183045787.1151636585516581471.980859215138311481
    push.0.6994941312268035704.9326390209521544125.17336061273178647280.3800870326302256646.7040543825404887332.7069570915343180630.6985436220721015207.12147826232218837916.13682579057609061169.6618927541321669398
    push.0.7674047066975310392.11745500564166725297.14239795158384188795.1109900790367587584.12958018188197419155.1105226328883174692.6524601168505888420.5441569368394681953.9164878155370920623.7008085420962510538
    push.0.2116240205222119208.4132494280964061046.10566452964453765979.14718912460442558579.17895661828495012361.3006752838959182529.1563635887478339898.3172906114470478033.8457374857381075473.9573138949215834317
    push.0.1777901355560571674.15484159105854270055.4322932561529929438.17389794408720062982.1453783255286718728.13027554420484109216.3163291214762220480.9426585630876691901.13149967474174422201.17143238045603604738
    push.0.14842369368400952095.5594425049957081026.4099876751120331350.3717091369923218982.6341504085412945173.1853700149737187990.8993054326145994007.2880463172512751664.4753630321563495430.13270949913435983441
    push.0.16204456898925842008.5846225804553797588.6184652680650514723.16514259334983647945.2807234452792575310.9007264949946770250.5970314025673271025.14767380303471766234.9399511478604347748.7240581324325727548
    push.0.5365532108078092399.4070402222445080228.4762161636688829274.14649623839739289223.17730175834272366684.9283164942351662865.15396259723834670159.2998986461438619571.1910997305341578338.8961068786538229066
    push.0.16830594442029272420.17007264367241594774.13669797300675341979.16752619073253964628.15051063530774587454.11829397261836275125.13388527883555236101.8867219320543040298.13566813824467398970.8466629556190611459
    push.0.2602501967972161937.12956297625288419503.18360142510524723204.11958650038094058686.4331521167782021331.13921902713280222119.9366067068646323294.10927538651588755968.4401325816477107324.13877291572704606701
    push.0.14312342536720426878.16553978068613505651.7697816367239869083.14822161739542361433.7091599647992578987.13471134284483298763.5546332864008572725.16680216382163035843.10209552952070929244.9296380371946157400
    push.0.7199561464575133267.15449469308208155120.9194765034989642025.13410197275085031149.15008815876859135796.13980111533373461410.8329610055703754770.12986892296980890878.17645569698755705018.1181100179577337215
    push.0.10155054019107599816.16733659636596192903.2621229934446330831.8525035289358994385.8451610076766980884.9928702109477485051.12095665962312051674.13014712311104361297.7659271111427188593.5146878047480880458
    push.0.6915402648374048147.12276899907003326372.6289097321522030997.17637876808641763581.3731888671536403186.10403189753574433861.6321431857529302270.13783122757754573802.16510330094976538564.1029062274666544732
    push.0.446215880238809892.13418743295470133351.17424814751766953420.2554564428222572536.9357644946272497412.6241290578564189612.3206882602600504835.14263035729306999708.4404887894073740692.12316756531571250769
    push.0.14780813414078509992.4613996668217155506.9418637878841760218.2800874710741755385.3981426910247946499.3210930749687018473.14372033969657849859.2735971631724284297.8382684062484726808.8382922580497680325
    push.0.3735065785651103422.5153151263639090036.2205863849659907776.2507946390277531534.7295884208888424399.8449604438174063156.2951128037525969339.3166997246587756846.12453705449246557231.11289245604025589015
    push.0.7163506788744553577.1084689658218688251.9705010875399713243.12124131089068182483.5936282441292470683.4670552159934665280.11450458053711546458.407991913637981927.3253210476864404691.645355982171299379
    push.0.3975462909302174663.11319895787666197534.13172176445060108556.3448556529618468089.9837373678418518725.3966876404499849186.5582278950688677188.4090044165787854330.7632682287906095101.2951837761149979578
    push.0.17832518137156248705.17271762195686719631.1466874487663653565.7859413511065748598.4198525493402513890.13939279566380357500.8200569233065986520.9261584397501736834.1076630052153858994.10482682189291916348
    push.0.1055202447895535396.6871073439966489814.4071386580913169518.10452053329819275871.8084495740066252711.3338169956159075928.18333422669047954983.3803418521638619679.15342728983220632863.14736109294328553018
    push.0.7053894182319911393.14350351568522930929.3691110284147723548.14818326401645709094.3706684531439801077.9018767292645886192.16854393170040077930.8767080969925945772.13012977868840415019.16138127786411552130
    push.0.13603080078276802778.2073870094503106295.10951905584177811874.6609072585231462545.6111843640602831102.10004909000352279036.7982504805585321752.13784101012056709491.1024128681725142599.2220613336143883007
    push.0.6710868299518986068.5059355470359170905.18359917278576214252.2557050988546763892.257587370099324000.10836419781925917224.5782281283865350257.3889191117581855742.9317273032303771299.15881740228345739343
    push.0.6364575427116363760.15056105111964953633.10765049144647158714.17985516575032678109.6842427459511438599.3032613742252210134.7619658745129466175.2855857447770502825.1812197165673934299.13911377515429790039
    push.0.8291067736877961619.17347813990897393080.16397321914387724150.2128714162813568524.3993962610068771871.11190983782951783270.4818112912573070526.12503276646510374940.13382923484424189602.8931195577431453869
    push.0.9937389371329833620.13835224339560748676.18311615975123522868.16708602834462084849.9730862800531893240.17364794774109791026.847712426821955072.3276988278200794255.13205142538501185492.10101001140518462526
    push.0.7844197526987222963.17054038385524448266.1156866964957747433.1744181540690067539.4580929592087452731.10649948930145335377.4908813253376294352.10937725200846733781.3510417386309629749.12676239105355221694
    push.0.17124278047710462875.17517567301590527930.9776181882907325601.4207881000577279171.3643978404375644796.6931054894243813366.3106579547577515197.10477849002928174819.1089608442008264634.16328217478605142692
    push.0.1872461744213851309.10348515659615722497.6366580883415589660.3804694559559544141.17811617840688612997.1533109784082713702.17214217739370605980.12828519738305838169.4379462821113127097.16004917732997841063
    push.0.2175173890928735240.8717903446860366768.5637698489416316728.9995698539570583822.5946251956910414853.12995564948373720279.6185216267166559296.6185281230214323651.17026786316929767063.1371630483632623878
    push.0.28522828752240475.9020095465365963989.696110244542650776.17808303157925074864.2642933138133635011.14100132503446025476.17254942585268328420.13397850058426954824.3380539953642696190.3245688829062064379
    push.0.7023138577641819816.888345491465316423.8719148953441624948.17604375298244647404.16562415296882891660.3097629840128645387.6278269791723884368.9743443022943636703.11185571096611486236.15324190241561885824
    push.0.13166230462119390648.7342658688803837346.10751660059632203650.5885359440542923590.4764666061396998565.5070335574397526980.9361951871242657879.409438116996803171.10656825790081120918.2590354176152798544
    push.0.7580641285730189731.12330212076176972521.5166742114339976819.14006092395990518036.16621745047641285521.13159945556018213787.10338825164631772927.13279242153104064738.12123670740570701053.8761983782205094742
    push.0.17543285495725138084.9872491276761801414.3658454209275600265.18277186466531977242.16340625786835156387.6171815447250627794.550416669127513254.16851300882700849066.14257394483971529062.12583004994163822651
    push.0.1414293506728927908.9004966360274905642.6896661678183966487.14266349170502350861.16875562879043359046.16473567055130227177.14374363935711134538.8915106327463969540.4765882820835407657.5407618324791684876
    push.0.16471303590063968975.173312896226433985.9970637043238388190.1828897179863032777.4538931360527895917.13673798921358906731.425544021821533468.8694751753793047609.13072114973478284578.8705358394832845055
    push.0.4237569370655625831.14020567720406698617.16194647074147212680.4850353431918160787.14031756813467392600.5778771245940739211.15920569416681773939.11678088351642186708.4195611118274314519.1865644902568462301
    push.0.1123069889374592178.6056549486347812084.15589388237583220257.11744738116536007179.5074110962365860521.13952662415818778087.7627835810324755770.9533301953155313059.17286205586063449478.11919644626994444449
    push.0.12372000625934083877.12143341280803343756.2846569977243270401.15048500484270158888.6627897955087554211.5792854865609893835.4991338559329831035.3818346663668360521.16907270522653961656.2439533921453181919
    push.0.16101133347627312841.852576287419289720.12336363281713933739.12300896546812666449.18301786571711453195.5515751600539564371.5901638259323232543.7765239397589205739.7823912354530999982.18361949074379275431
    push.0.12105443055109120233.18110484563848106687.11506310428539646509.673779925032488483.8204880988345460619.836951088570344837.1075285822137828965.14710023197641964836.422354990056445986.7614271314051579805
    push.0.4183695638773628221.7910378495738524506.4277464108711396613.1325006583995656421.15468874827017473386.13508431587294104665.15043749830765968014.12404606660146432475.4409258292515244516.16760440675132247549
    push.0.9168438830020046531.16701207333426937718.14630022822632078805.15337484073220659076.16122480251740171388.13394349907407890145.9633895769621914249.16763131972204586850.12838693375414042765.5657345620607428677
    push.0.7483766642608705849.17575831321178111592.10922110391895894893.13618445835347695302.12660960189363197478.1513824258494792168.11146459958544064175.5501070881570194339.4561299457612050388.5031306693773430618
    push.0.13025824763330938911.17278335658212945993.15903667348396459265.10878934593107010656.17443435249456992997.7002797793688983288.2886374583644832891.15361213388445807694.15363614983066629844.1172966641330652356
    push.0.15327686659590080362.12387516141859821404.15301416543020696493.17122328692136403813.15393241407877279886.2839306432593906080.6127232541758738655.16811328201521619452.7304161085290406808.16059664413569107386
    push.0.15193288858795586089.16942653435177375787.3946777778618416532.10509938536765652656.4258063417005156289.17126952009068992022.13243274935223657470.1538532140762430691.11276649317009219525.10927775226172444168
    push.0.17166582430590834885.14921589376264087561.2211063265267269364.11878167538083073978.17490233184156582473.7480716327692133153.17411042824873869795.11084280256321048253.16304235288453447793.10154214189279171174
    push.0.12228941788280660244.545030794554682878.17472013240673331170.12608315576332025170.13443608452980805633.14361575489855071425.2950538992881294387.8321809168639039456.11522521372541721766.14445359893834839972
    push.0.6417032702073914228.7673189027747100244.13429568302596747917.5929339274420884079.10077134679879295167.8410393660543614860.164700640858785903.4490155106496461814.16091902986992120664.757052228671257414
    push.0.12002610632857334515.17372621283291295846.3087898834680363116.9859593464971846348.11737747662391064518.11578784419061685187.5510673849302653937.4180211662815016344.13717027428287158967.12277595419054637096
    push.0.13955588401470570783.12428792939601769829.16661356168189696313.2453725177240705742.2470137452346381877.5569027796564643504.9230392926322836315.17564350929569013609.15192505889072366369.5778622402863190377
    push.0.10924582045216368782.10985887081618036706.14277624669581035225.9663886922232621490.16445921197471846235.14865350183623627144.13405470139238906730.15570630090580664896.13692425879641516839.7280947376465525978
    push.0.8939007276725339488.6029495302165671516.9587626112872864216.6666544784600078361.8037836396575798356.9400115942535189462.6397948936046594805.17438801332531556627.4051466633633471358.13412940551443830405
    push.0.9726200466832458596.8454819643603998462.14482265481499311212.4807282970050412723.4620484624730270861.11317136657715345997.14805054008201796602.17984995814481736906.15807437546612609202.14972924340887445827
    push.0.158317477095448614.7410709909438062509.3887573309448035252.7549259693469514655.5858497437179716741.14248945486343544572.16893841513717955812.4728051327748720935.18020443763203611501.5609439585527798993
    push.0.824175477191863091.14871131581706773623.14592665980334661450.5529897590835459543.8883066108193358813.2728757386129751077.3768691493733489698.12316610818206056903.3028608498697516755.18063477007151738356
    push.0.14731684819714083179.15804204922309626320.15388356002233071073.2855631338589039122.5557047415480486221.1588419554152240645.5525075525596826123.9743215033665424030.8592790465890016265.4764455726403268093
    push.0.6660554529113065529.9511694757268021844.17593042121539303348.9354206873113284441.6202479560500110101.504174952074953392.15125147795013119242.3253885161242968397.11394545756706675921.18239331478755793701
    push.0.4304709109395089268.2708029204928604414.5584420400820589631.8694174516731483102.7450976167265769757.4949457334495711847.3609175339952579510.1825912328437510471.15302423779978715324.7648622408544723061
    push.0.4495520083664693175.2791819568282078919.7003764834025018125.11540253964727014859.6605696417676531613.2106525802802002672.4124160134130671785.569194858678678215.13664743961797527656.14762746267306435752
    push.0.8280474143476238730.1919848678171145328.16407656950980740038.14257488881399543116.11490366629693386058.3953818751749721866.11017082766134756318.8430156326303789334.7204622020808514675.8508872652284654942
    push.0.16683107714492203965.11743674675942799027.14143612703011616047.16361032999605861080.7817648820725953422.14912872776756700973.7786184258831618692.9912182426640181869.11635657469159728043.10776716804938334848
    push.0.623723221048208673.191296230899221810.14685642580379240042.3946383780385805023.5215719559663096649.10418126058572328975.1071874223142751764.5898849537391253881.18400077661251513672.1234528122171540343
    push.0.7940218880091725084.4320993525044036283.14944245410662854899.8204190156440427877.12552653480738740913.11785919875738060416.6852228991733226575.124798157649162588.17010324681323276559.12072163677607811892
    push.0.4075498240676775232.6040713059956170983.2371632428094185735.16691314905468719989.5130679054769544670.866882132546299237.6127403848498784079.11755540293845475189.3410414023309792227.13099755687156924976
    push.0.14276538015910161333.7303817813751046816.12027239745042466260.18103511144450198284.408676560416750124.11097921196531959700.11169564756768544308.13988260114438839243.15958289271037701155.9770880522049927344
    push.0.13749200848399075266.10113055196859370861.1967670285274278694.2146140730043121011.4738449257805060689.11108924199477352483.2013754745878077515.17494861868851847446.6834318209766351365.9202073492552367099
    push.0.6351056919450132061.10089837279505052924.16720271628491808162.913156090095349904.17120617038735485634.14165274137302177116.12510313028889854881.13423409706190478499.2053632328217108022.13110353050246186710
    push.0.2311189585673992046.14124503645152152784.3962656406692193661.9138739675302372830.10712242386728362824.12784958706995345538.14036462812789447906.10569078594939433329.15481305829028555659.17170805497166247867
    push.0.7382805002410860285.10425497696823678744.3357023867951979595.16673034685993474808.8654974446201648674.4811758450585807248.15377762796426158735.16344516389989001666.12030900188642328050.2309861954096334736
    push.0.4302110927140925139.3763464244996315777.2267844304250591536.6307593609451179499.13325445255253725822.16264101543875793742.3841628175430884958.1120185707165585687.9679241579112852490.6438183655684960768
    push.0.15753165968619784829.6835924711691435088.11974827463878048507.13099776651335896081.7225694031460975169.2933863038061303999.9727292747216375981.1698576514417572810.11217981559056178640.15502310972354171735
    push.0.14122651033732052289.10783878409764755096.12853078943671985231.10792674114917427940.14836273315500385471.7520823733379797703.13439099918573744978.3771172863386826010.3890202627310917300.4884541341369749914
    push.0.8430599691284500177.2651822023806122872.11757011185223465691.1515149208247354119.15348470345398104373.5979585420100655222.16285568924557534527.7502156542606336965.16258789090162161923.1793449152275716337
    push.0.2491610338268952346.5714252895240213109.6559908301508772273.5552530161811114556.5830855184859204723.8027616693135594077.15910598519913652665.16406176841335786898.1031086314239084663.8855817408961525547
    push.0.8596729228698193409.8864179579061204992.11698190689028505216.14198894912776784563.4709358045964127167.2305110928095954164.12204182677332424699.9045185264480748370.17613513306847504687.8686900268830621514
    push.0.4970622647550807669.12514456193549219784.1616763814832203145.17626624953229365913.17393420686289912624.10802464322884410917.7116144333945686165.5129302917912935144.9533234438497897156.9371077435246523787
    push.0.10281279984019872662.9096588346499033681.14226447885626098766.11244310704014493042.5176892136710413051.12627590750960605676.13006672782084210036.17498624449938772701.6133160107896884522.6823051581141583227
    push.0.11131872286639508561.2241501460237635041.17497383974290177102.245491008932781659.9853343211989462730.12202729594961185840.10985210228967640810.390320048451404543.5414386984560384713.83776732450326190
    push.0.9828460136280132418.888742373754671681.2553959232594855134.3096257643894027884.2696095000837724818.10531562260335243883.6105043415923263360.9600672996181889354.16037136665793458987.17787574561281551279
    push.0.2190385427552588678.6498484188303216839.4220806226227241034.10541529303897672513.16960532073692483652.13651832003242514428.15873049036692924426.14007795535919730513.17448001006954567937.9953665901679335613
    push.0.9141539949155179068.17185638940848689536.15893269962113726241.4067388702746894565.3630774955482779850.4970607181255154121.20881024342241584.4468094496392282288.7367484213681306464.14801641458320632152
    push.0.9103027861711331626.7279122471982574016.2291957030020603917.6147380083580926977.15512027357257351813.12977328788343115129.17796902738793801365.9913657261843538292.16123977544062621814.2955362922110809864
    push.0.12801706811921039502.7038939822466521824.15774567371226472290.1526580968317234769.12724523554399270466.11377459858263587849.15180125847195586487.5776427043363141489.1536426067849107784.11156933118367558643
    push.0.15384986247725595147.12142855345141702589.15571596848990593282.15473373756304758085.1176213461489905195.6710001656277225749.15006067401844941585.10119561301426961985.6979872257013584728.11655124160102592513
    push.0.1115406689693900582.2482915670795906367.5492335239713293505.5753046212965847853.5440517158211954606.11278897814976215594.7970987824283006628.11271737963702627799.14232931855835259490.2795707215453828919
    push.0.16654397233482981746.5081135121636570367.9053390909155887261.7316257892715476197.6497435458121193770.11579350150456429131.9802052630950799068.16513106090380415381.657389080727375995.9016225280851762219
    push.0.4298592085155304002.8050810089933870234.2310917219791400112.7810821814369636703.11021700782455959686.3247576297820168457.8905723331950217549.55474927821882808.3114500972516708814.1594807159035061702
    push.0.15560217475575558326.15809671754661493365.12884757125510842010.16815727341853264090.1200550041852058473.12049365827271928391.5581170566140582043.7146500688633217385.4446048536316989978.6258668264811656460
    push.0.2497433976944530394.5977502754264628035.13615748940796128925.10115215700052647441.8784220976294297780.4829372024150484688.14007804516783233714.4286340101776228304.7122651649546376075.15015445356348972635
    push.0.15508922913034158340.26461223218494037.8702029733833201466.711060472040396805.8738398656660733707.873076441777215299.16837709251049450949.11361528993003697005.7277557575787572399.7277346577212786754
    push.0.9641041245481077085.9787714475350771104.2948163818156388371.12294916747423685548.11934319105870065896.10964255642276390342.10894306897540525170.16449052245954674864.15435364781074160557.6421660605367459197
    push.0.13740045553385029320.15256123749217190088.6885673792654550606.5427037126353639046.10209776197438086513.7506060566464143051.9766368561813301985.13159447106550181052.8550255195849473852.3486585291149055851
    push.0.9358614769916182114.8255341788033083355.18043895994093838377.17974553120495181762.3970988414359464950.3327504897201910116.1387757479478143578.13553844840588798425.16010420118535505990.3886215859143924312
    push.0.6446898901406636847.15396234993010907448.3198664862417582674.4203712646314273908.17470133987255352257.7996079023219719847.12859018855711955961.17444173045544893434.13245968089613490994.4390980794505425276
    push.0.4837848661116208530.17602819925796284126.9424270682075089792.3366984236884197075.1314457190791492589.8290195589560512657.4065079838738467379.9297025722018529384.1382300748371561577.17423066867322053551
    push.0.6283609622846131035.9612744868757218847.4242545221751144843.10680399596331764210.10381696972305035156.8020644390106378237.11967758018928953802.8232746018896416239.9278131207788127531.4544285496504940435
    push.0.1148954428038209326.10525799565069998598.1059327062881680503.6362167351546473601.9735410768135333336.13546017616921733237.10409578692189072412.9944412781394740479.4236917714245670409.17770070878214737629
    push.0.4169222400887868353.17939894680084073300.16485135361107928433.3486249577630881324.3419131797858981402.17549325107126464532.693015865936579291.4219305397784863298.4731657353462407597.15342714087983032724
    push.0.15931588755353407887.11383376479199396215.10517774750874442033.16353044699536670820.8204736195208105180.8388863355162758707.5378422843971012565.3555752594992642842.5470219114264147538.14005839906994641367
    push.0.14216598920812787371.16498557549813552415.6363208736348918957.673926596230556003.6736126745605384610.7416379150749046722.827418512829564100.4925617983182389738.4954158690075268390.466597748269673899
    push.0.8521574870149789749.16415504352734187065.7327278210531933790.1908988212582936821.4774257653249163579.5370075241082699165.15251484677895602310.7376082261276058528.14358941369003516771.2619638799001314394
    push.0.9365052849849901326.9300555160038224137.9564303728569766648.5257012138019098848.2890387558742926075.5167198306218454630.9101073561404921995.15332696951013317643.7112821550352156292.17918928649621094549
    push.0.18032591614140817247.6532248670988191307.3114611775067215455.18334562370325653721.18228423419933940082.9983865914683803699.12094240391769255993.17247049855964645005.801454064495698976.11786317346579651692
    push.0.13426752911266583822.4084682640416866590.3422083866875084422.6841324504374644350.12755681197559202931.11711190340590079901.14985901274990172838.11007443644650249849.984204421798463368.6680244339311231665
    push.0.6101406834590398680.14081835033936656105.15173504147001126871.8578724464616006011.15868568395837067189.11049089028445903601.6966928495393620308.13026806083133981671.8530051046192879765.16352441666214779132
    push.0.17331157932522532598.1339445229962061732.11850377123494467539.3113596804796278422.17560290831407737995.6962268502874192563.2724487464825661942.1209764310735997575.13363877762986171784.3191119747914339063
    push.0.3309447997161430717.8869983840655821175.15326786304351209380.5603924847068872777.5044694955957267667.3449998642712376745.3316565648770011571.1679669727460307885.18052606616305888524.17196644158681855264
    push.0.3994688580165412230.16463864216633978220.6727894424813456401.17099717058927683067.10370234882016509005.10677019069087909122.2172593184960030523.11919851707931929529.11198230098435403592.8558873892866644754
    push.0.10810603884216506747.4696588852196246047.17736831237326032110.31118056387237020.8146033559930958148.15766548507345577395.5495122917433531395.17346293731244369131.12929910830787734380.13351458655589108589
    push.0.11947569704323663541.17611741529024552656.8751047386069081199.5201144267223104085.12688894049703230700.11899139776861104936.9032500516256410500.11194443546267868477.1667252157171595421.10051231962664638787
    push.0.3972906484029025329.14367710259877376868.11789429132769460994.10486912986715313972.4881650562074114718.11070508761149139664.17453138617063394024.4720415580778452318.13514895520862913088.13770644962837160627
    push.0.4021260568399077166.15551736846229516036.15817615106905268916.3612229159358315460.1351052758445090145.2071490380610054254.4452126859487119337.11508984974197470897.13817381505339062377.14417094237758117449
    push.0.3820142213452287046.4069783268710437611.527032033487753870.3346278437424619136.13566821418054124788.13899495515423506542.6597923568523281866.2067136664626475488.9514569256236519734.6457306709612799828
    push.0.13124628848592904930.14620240994128082675.8063742023810200810.10418112196364605603.3851828405796837309.1031250365053539788.12152678021685649977.3420386301659335642.2872602825217722063.1503553759207888184
    push.0.6068009808758569187.2767457687700542542.11765018871571042045.8409876700024270774.17279210634038157973.7928711640272991685.5287528051647133139.14564454458002438283.5059818220981546090.18392998275950911012
    push.0.159536269612631886.11519395500769954910.2038307652735060789.14105555840518194395.5144912456969352772.12331912666765198123.10055159792173869162.16512674051076335849.13286450073573255591.9734963357212357784
    push.0.7450766146561682348.9416867693267739148.16387773885962376180.14248007030905710132.3297783051856080229.17927255240663177504.3627047584179094923.14636890533306205592.1409723263942946493.5594661877433753100
    push.0.700485491381726231.12492859186299992549.16065891523077676822.1194308062186706438.6306211036939890363.14714833638536236639.6823828886233523953.5793011656494497657.4865092103585717321.8631067780560806944
    push.0.8243248618739674740.2783063428654770724.18174886507777151256.3077542479822390510.91662880523081310.11004584958406819986.10887527349670297886.8090159128280209571.18067621335267655041.3867146354436520430
    push.0.11601720817395362759.18374056254602395419.10453732348213307133.17447996167247104127.9927970242160525307.8350103217316486948.8174000421399426237.10442871299741796216.4711743597573821855.2657415319591826931
    push.0.15968269585949519536.12658221413249996304.4809571376209590291.4209126471218013268.4545230948492021136.15532877936618395207.10835011059085318676.12692335229476624590.11780582010671406253.1708841571113533260
    push.0.4988123399804465387.14436522095586791617.8965735877833484495.16170899461753826952.4137813987497617446.2769747241105789068.9347477110429787356.5640600662304332481.5372563567703415368.15689991353375194123
    push.0.195000311153576937.3948831406012839174.12436027792022609923.10513668095629610547.11114701217578615360.17846615214915205392.16689859222749549836.4135204277706197402.1737906116959518301.2312012940111542045
    push.0.14307651450438567390.5262141835395179045.660673752557835066.15759674352049354821.7003747132469790787.2653446820828520614.12460098993050657362.15192944227277273757.5412422564585010443.13225353270586876948
    push.0.13553594376047365226.2604830409598072699.14104881552020010458.16105355317840231913.12087906784758958322.3331684578271556265.6071995119765542912.793507997896500129.7303528109246578762.16332665227518599141
    push.0.4707919360104465474.4433307821241148811.11459386135677761880.16304685245754544279.3870757596326094334.160974453324942408.36835312700192775.14122444440219142081.3521185321771988418.9773282985444992272
    push.0.9956768691939093.7140658126031746166.1784543017903074436.13400539521599245122.13666803261787663542.16164341954297192569.17454788850562113794.3586380274162258273.9637657059530112570.4203024692279645647
    push.0.4112952375983443392.3542158702654035616.12366887649089280452.8400681711004849073.97151830351649115.17268023732630670499.18055751474448962088.13023674294647657926.11907191203628746871.17168703922877302264
    push.0.5974702239942993415.7984809121917713316.4082460036695972513.14882216879402627222.10789515582974873072.9668437894351413500.14057444527116662055.1926264173047794251.6824781724453850475.16311493344998091253
    push.0.12069073925104462764.9253810276366086500.5601567640259519336.487393504573828569.10705666398341323915.17873058110587519786.6025826469601566925.17996480026666439153.11451208317154808219.544939384348322058
    push.0.13756973684308756153.10981386417020107784.6370444056874558453.3865367130033756248.5578850732377888964.10290482121034245938.1988305123448886627.13353497645008190615.13042953743178586814.9029863969640692537
    push.0.9710501985961874856.3007524742247541270.3872802967304824530.15238949529453298225.2725552331276566722.11708312666615680541.14945647982992804420.1202697318632007538.8196242577529089920.17617583223152241759
    push.0.17835465394277005274.300906558712104403.1125942085164071216.16331119452705336870.15064531150924828178.4739647874629224584.10715931481836632121.12630537312252227923.9032923822760205120.8710112703661906023
    push.0.3927153214028123414.11039666666049528409.3410118792380914924.10360434153811576931.15801816623805232189.15111049098744863115.8396912947637512679.652391629175350602.4739045604868023607.7787044182164728905
    push.0.6708978467688981024.11249797973369721263.13140142171534305864.9576153962908464293.18044966798962085680.4306567098987319159.12352090074854873348.3421622557684603954.14631753661894993614.18355653890597704297
    push.0.4959137158379509192.34173088587565570.8017337047528812408.12870625097971401607.13236111020340205465.6889562471122548307.16298851121339787917.6573333943497860526.4229473793954494859.5530384476483035265
    push.0.3472516037401460720.11184387108733508855.1811047973429658119.1993055780124636133.3317079210735605812.7622248349064273599.6612201218808918928.9167723498799623756.12903406864200927670.14101994049808788840
    push.0.7068224161338127050.5324105912042277558.7863977562539507444.10823639863413957835.848286687683713004.14219389202345150605.13077701645598265316.11051945651740703285.10327743429690337743.6767704040450771282
    push.0.12420981969517990237.13684330607010127863.1504566715531257405.2956789252335739338.2089640185104924971.6334959133140201604.12004049420424447148.9070482989695652297.18227033839034044517.14376702274577995463
    push.0.9864973854720435630.316234715928419640.13298893418738015479.9040470837200533223.9069303394826891359.7412762282765032627.13430948130830170730.2572069764782413777.4771486475593232609.17534286692961505830
    push.0.4295009133824571413.6575211268419854818.12616956373069017894.18280448366088888999.13375653537112985355.11043780014944999142.3460904895572658828.13114945528359552477.13010271460647896186.9208396573943064438
    push.0.18357225189490611060.4389926893276179425.16554220463473735637.6243747206841848358.4470000861562165396.4989817760230567187.3582501880821492375.10216479999596983629.15711138557548957667.3962478702513626928
    push.0.1422119537533375073.3481687641087749059.656792742263079952.13796774689470033421.4595332274178485092.2983580926637587101.9500319307918459038.12288521403276037275.12747067890920294446.7833979869776306069
    push.0.7657479050919090740.3315172887061860357.3341209948746042875.16131386396416237332.16701793491313847768.1651625596078874643.17384959430610786120.18146859149509500508.3139114416603243381.5531746286777855908
    push.0.6670682362884234903.4071722202909040552.13406248124926088747.2923956262256066944.4700838397136001201.17634388881188740290.3755767837021767169.315247410347918636.8622061640433295379.11823016643964747700
    push.0.14638426214578530497.4586102116099901391.9766562364025913814.13923508611367401974.14004611194094219779.14741382475354873228.17248415896537159072.14784843259162407209.13824436459746858811.731856166050687514
    push.0.1752405051108924622.17266567713817979531.10011510271852552387.12139335607944601436.5391634306072651690.1183040322316857140.9356792130881179542.11577964137153041524.12347466341429558007.6325322956900669097
    push.0.14351931166160876571.3983160857466317511.14954034489836155292.3229773739342228314.2255059371314541703.379805978719379573.16451478661716612758.8755859218918575724.5988415312208316567.13914728441019302811
    push.0.9123122794064927609.10637790740931674946.10906270111977751925.8546466703937539800.14033022593493632916.6036976331586501373.5288731394026227210.9168965069533089200.2432754472441944059.10700513258966732913
    push.0.11480857158770836567.10962393049554143503.13962988235857823536.13343013196067088362.16795608682219543692.7305890693719611788.5451346016863558380.2445908487089025663.5184276092299205650.12141467362426733885
    push.0.8389132908584439468.9007430269479995002.12619548253199983119.12242005286108351258.10941548695737955060.17173154947425087097.2360061522590504693.5706522330344313299.13721589664662915763.357126168798781063
    push.0.7020961401331214148.12527644163488054907.2286871031752457296.3013695387746523144.10145224322734592729.14399189236335120422.17945327910604608181.13022809972913951912.1806186261749490523.8369653168515872962
    push.0.4293349106521080664.2326299407610076447.9796298292955461487.7673398111725669874.5390614369402805131.5130655726061393795.6972829772910017432.5320660084731385723.17950759752956992456.9104996427174912603
    push.0.1378917962780597573.12975353420330630884.1538830521655017773.2992741237293306114.8676710802752906377.18257453317262408993.6057118382716298688.6997936110584050110.14969916962041978009.12430988980247236465
    push.0.9960107701698887317.6940792932835049198.13338682836991050991.8083788206957020588.3264417972568878291.2334040249590171293.13115191427126436783.830654163039309748.1025128034826871268.3439222543591367138
    push.0.9998959022906985973.9114229193935201438.4207049044401260900.3758759185801957711.13471909793788845473.8864894119890611513.16836037023553312463.2137737277727377919.12465936042722972374.12895046098158115864
    push.0.12371805497391969808.4441982796202435324.9488116415227662314.2888529128920020749.13817445438191348996.12881493939349309780.16654589788642498200.14319880742851820372.5602948402592119569.11650942195321098769
    push.0.8198727677858695895.9382142222479101818.13287397104249964281.9507499559836388034.8077812162015851729.3475650789565178637.7228028147909131586.7930324450083550207.13273244095486572279.8341725518056258908
    push.0.3386719103508878848.14198775675826874791.17193107942766900640.18370066205910944269.5477789981134060887.5783435724950307643.15861009377854093833.16819928205887300794.2107539545944455255.14546316741640053763
    push.0.6633089477779977472.3423641620740270310.17881304536388707169.12789178531450727978.11298915649135394813.508089241968695491.2773496875145584647.10542966837160744987.14519646431551023101.15471179828256001136
    push.0.15763549945510479254.4788290233584385081.7020911030900328603.7184715913465383733.3537853663414759751.3347541109202596456.814205815388405691.16323163232015215375.13703280570788267720.2864897652811447871
    push.0.13019758583891654603.14618025127516126767.8547994340406959262.17278095783729336767.11496729431425156398.16746392982290723137.9861724341679649349.7841326993219476724.444584399320298833.1493746822349907820
    push.0.1943167798592332652.13680614073334347525.16291982080936744196.3373222487070365834.3735764156189951313.13698697695325642332.9471752408575782861.3870095919918018817.6925358864596018058.2449678685916712114
    push.0.10839087414177878343.14186451781009931382.4659384907645919448.3920722869826463196.2871189237921719458.15183953241428071011.10246773306743064737.13414793532276540554.6084527074671144805.13439691260981064015
    push.0.17229723863328998344.11566688201868880620.14393801982767722637.14642836228761702837.16277674535077750024.15188115562114981297.17099914621529896472.961977865143942826.9447722099270575971.5005944956793387309
    push.0.5565641133026402761.13736644072097157127.11880654275420987394.8322112590442502004.205213271562838500.194993516982959817.13606273579732437126.18065695436814431384.6875131831471744351.4744502611632119075
    push.0.11936157351600811805.10286286521109539524.10382226719228709370.7918706200512990775.7036338757022549519.1580992081219874229.3739002416504085100.8744114579854678733.378246066085719869.8602040124896250302
    push.0.575997173079378443.1152046346784442833.12067443275758147903.15426364550326501794.8868350418144464272.17877511127546579241.12167191484658628348.3203807055432711858.3279992804237062794.8802871366418620255
    push.0.12655511383675631455.1147749443217294784.2395480000741162648.16585408051648126700.8874356453941458197.7360006916076955283.13419291618246934387.7822085153895591248.2587418862418523890.293780325501310820
    push.0.3047889853650402185.6473051126989749014.5718763409937508666.9203151910371543389.14769912082574212739.17433836195871247927.1201004918123254474.15503251879383548676.7095523157135573455.14452321154400640554
    push.0.3801979310058691453.17317890632287738931.7232633923934796985.15870686481932377401.1163948806100564466.698611546166408154.8267654782340622235.8701196005729210797.7479388608858399769.17803039250503176354
    push.0.3527062450660976769.8430252251308455781.11724928499386077297.4400901330276946767.16249167058349577107.3031795984543653250.6862323408101745950.12610931346506525050.14947524721749863007.2708868111395815662
    push.0.1234408073548381954.7878912397113536199.7751952581346691706.507851249418349388.12706803596755976938.6762278742775747047.6561092671999184033.2448900790740605368.6401111612097282627.13997959826320163301
    push.0.12715165219226200133.8400325587216676080.4860235593561380945.8117205348760405919.695332656745767003.6612751438642241310.7920575239028736954.14068295508944678641.6721543325914411015.1137470965573222742
    push.0.5647565850132340816.9694197456730888496.16240394212023652626.8427964663021248700.15076376587168941077.1734346033731036639.1738982527826571322.17207204909812846258.449135304100399591.16319007335216189451
    push.0.15917692224535887680.10122521342399994155.2904103147388099067.13234107563281867259.11791546580822272750.2476788434421279146.6043606661423243031.16444162642645386630.7847564056905388295.13922966133253466015
    push.0.16048382560041578356.6584144664608776215.8684694808840360732.8860359830135910736.15399023700544797073.11441845919143079765.10518114671727375693.2819434418895500549.14942972273943240404.1776102980537651754
    push.0.155044906716120293.12164521489776462640.5780419666876264266.12456055068174222712.12579661127581598099.1300735872451337276.961395267638772674.9735504112002988430.17254047780886825599.3517618530860668106
    push.0.6290380505674493959.17594327111158602366.5286420827140395586.15128333045306538974.10722316659210072564.5216879888401569694.3988077491200707325.8937729159703073112.6315666784461119430.8330526316437737865
    push.0.3047897179784883741.11037478880306743386.2928733848257726445.17151711925822035198.5418387648498594777.8100887189231499975.3853857838276054138.16058783431431055474.8120584694367194464.1105753478535302860
    push.0.17039827270062004340.11355534571052631643.8410908536118643716.11222661633911344888.14659766355173332404.7932744161554421249.1513238091023431508.857188257334735303.16212191762849581109.3760093435827892958
    push.0.11516878815943602842.12762901255701379819.17119334281402511380.9261536973978504863.4832631521119931297.792543918750592841.2525305427329622523.9110643649366849101.12508728423483458282.853215630578494988
    push.0.7595925395827979828.16769043341712098271.6103448836275520924.9857982259682330465.10671310883545631013.1602264498371532197.16504304932602739887.9934039834133779918.15022078508097892392.1190536093440243891
    push.0.14328188688812839393.12110384246321756991.16565833656747264513.1920372783432121465.6332485001188627236.16875485858113074895.9376810511293541022.277437059972288341.17652876362489823138.13288474738481401202
    push.0.7390165800949531859.2652599178606575317.6901011084924941890.1325373443710234480.4284311731416815315.6154010421915934530.10082526841960039344.480009155286456712.16989890923319563756.14867297264640426715
    push.0.16920903680816436660.7793087954999539002.1866109908144315247.1621079132172775266.3381480181649619313.4390916096509411113.7353780922571631437.172251875493820266.4399639099301776477.9582421195822948987
    push.0.1600254831899144289.7443055075787272711.16003422851698589134.9205033310468198355.2524847923099012271.4218130601493258622.6276810541485477356.14337242972438033296.10333068817986357683.12765328104492800948
    push.0.42309518305866493.11962651113387289864.2723139672214190352.14432958596418389216.14957864198143969623.15331692057126212480.651951996788978969.7618405090631068176.12847196060762822137.15380649149591784833
    push.0.17153554975526151819.16522683785886509299.2005599005930068053.5649706527429558732.11115602527920018290.13534286611951423209.10461332831245202829.8700050517131655262.13273601122297582104.5485578783565791789
    push.0.12776415343345291354.6799747137049602813.1492730995955733522.14173795430637744503.14352318233821673246.1126782012357811795.4815317899937652328.2245039210726533859.11943267908538688635.3542075301545807328
    push.0.10639724145771564345.9452242702849381793.9949235047646473695.117550646449162097.9707644132657894020.9687022429836277262.1238146073822648532.5816425562067660173.15993830621634487051.6989667419860960126
    push.0.17587367380699808429.13923853428092038394.11005651689013068143.8744421866041893661.10544017694294261564.17613781908041531549.6324906339187439288.9437942214159762636.15969793156771940025.10246820100402701176
    push.0.16307146396319771386.2143754732363734788.2915025587773567420.14256712344960901010.7909871102255523477.15321014795126694477.5037104821344186706.3574178341707484871.10759085267555155962.2445639778136578976
    push.0.7039216863811417518.17358725385846436454.9840115965080515722.15400053725430128891.6551607374583230818.12532093286182237754.3491206606384436542.9586719305470001431.17713939711942248039.1412506329070387509
    push.0.16743593844092088802.11859167260268673904.6532372727156046481.18404135961617822018.10415048933630811185.11070569371672657541.2967895563096405690.6837343561789295444.3502798255968745031.5102605182540364497
    push.0.14035054724163072268.16958779792959978632.5852501559234032286.11480231090033974684.14506891949178275891.13992850304093599984.17644079724665988418.16641251165734094412.7101622622678895370.8156819670003713739
    push.0.307046440178557609.10723649169958533757.10909968799311945910.12661321382078406620.4307378259383112464.2667202549066513600.11893114548691711367.5553480976329710515.3929635663765370628.15040096737676217427
    push.0.17573793226018345512.16521725481265611191.5603672799676822007.4248031020197200372.14003642884119465560.1597163154697051622.8572038570411814550.13876143370464982591.17904496301912881851.13293131919200007486
    push.0.14003762591247567108.5815100444866389198.15549053560754175467.17748430877237855514.10544097613712789544.12294788392166950053.11438937733692179569.16178551278219797216.1890020298897216298.8225497123709013871
    push.0.12551907793815746791.13293230031884837320.8689027324076638675.4522964536650764568.4447528971533033050.16124069736695489625.5705195766890653601.17307269918872818016.5786742312360890151.1343790092694885743
    push.0.6792665828678765426.3077284494747568727.12452997074422143968.15418061190873789440.11585328585085515027.1732757925482683991.6476416590326179484.12896477256192984389.2434869908257709189.16240133290078401194
    push.0.3622597937239787646.15999519620501152225.10941300141017376260.10182117791784073773.4356523201434004492.13074605988010734483.2652952804264845171.12437478792519202370.1100503447950758423.10797883953061534046
    push.0.8989752260682389611.5579834347053175808.2488829792252722322.10081025573084113030.3081862992847074809.3853675895610726424.12159613892972991937.13316519971863552184.5043779250904161443.12716241730984158438
    push.0.17965436481677549571.6602062080149074412.6837014225695137409.17243821645237897118.5972973985403088575.347368148907539650.2833261417829097560.11336384368877610109.587128010331058874.3896609368828147989
    push.0.15026387477228310316.16521777283464882105.11177790882985705.1873445613525519356.7408104426874608889.11053601381904708982.10572529416546285622.9954033857731192021.13651666545084399183.7100898203392690233
    push.0.15019458743279455631.5257502399171122867.13423955601036387925.13667290384294805584.18382542218505254368.12237828951836963571.13348332730638457161.5312934980934038337.2107984271719021841.13457922997983099635
    push.0.17948208099639232094.4171836269144256272.4289572733488551886.11352282063943892287.10322878737921242472.1124820926444096914.11679195088951065004.6498518230883626986.8002740890700657550.198333258857444479
    push.0.13312825865086786083.3678689359650145551.15207436484493672230.3582867433260511279.10013646971655287710.17014775581773931398.968167509995572746.17405969977694440021.1127852040069429111.7035731336907668762
    push.0.16478332020679438916.11621317637237925319.4629738183152534315.18124884581489307451.2370305827570334461.9907298401904609032.16500830544775116388.11119543323213994862.13210169201742589469.2638692458982870518
    push.0.7403330660719449843.4469238428754110248.4167471722288233847.678737228921875467.4041737125538536852.12841291938810282299.17837501770865873404.8334963824810827952.15795099993289713833.17068067833313176380
    push.0.11790743988215885541.2445839507146971408.10353410103591819391.5232291501929751910.7185020798831905492.11877485516652035054.5753458386672891838.1226517821109131070.10494619630397123364.15455668345278798017
    push.0.15207610859017864399.16967273774621686198.5268565949209861935.2430994687306532974.12295850867877575322.10454724928980767595.16003353757771562476.4422173633615636521.17036638695215118606.14651193037445545925
    push.0.3223304351169692687.6129550318251218178.16719364374154368884.5269651252683706877.8899305390678319129.17708383129052415665.10704391492959612333.12684262692686767668.7859836628585177529.2983215027239992688
    push.0.2282170706365775587.12778753674784642680.9405996892779872270.13827101339237118706.12087115347372951681.566679189205891799.13831222965518707787.5207598892246514602.8676940830856812828.15504715064613624729
    push.0.15851837725083705623.18199586172795049251.2771067958809096013.16557469110138923752.17168034738414210457.9050079476297830440.1011011392107091591.18279769422213352114.8109309512848154857.6618320749384678092
    push.0.18223751826369053749.820137058656363627.18266955884197080823.15758534735620349226.1067843884672669580.13939784668719488816.4878961528779666518.7191884423213510122.16190146530400277568.746995092066214501
    push.0.124400429347425382.17397027725422536703.16616557497190236360.6371825849949938634.12712520774422249170.7229091671185227486.17889959384211770020.4813388171385087915.9438778592131888330.7644505172296750397
    push.0.4778362448168145840.10711092423523441932.3978830118791326973.16590543508296386430.10453916978401173471.12251465514397591868.6508635108226059520.2202764051514769261.976667518673874381.7246101153004898668
    push.0.16806354342444739351.4156975339115783574.14576277126427123490.17756768430222234794.18114036666583487985.4895373317031852628.12538472114550406009.18038167530045347555.16437622177499696466.8841113644792011438
    push.0.12630048209889558695.14008573147513520063.1607603243486775782.13605500811642679342.16678673576494703890.5090666926354741444.4188793477745850989.4227404774898786267.10815441932682385906.3438589904450139585
    push.0.8445097509394044517.16911616603131347023.11940702690924140405.16484166965142121586.10815806099337330707.1396179571591587595.1196057629377175336.3598078591492147347.14828419338253975965.6800030631960746223
    push.0.7604197915034635383.7826962516459832022.4723326813715842265.9160560369334302182.6363494421735162682.15235286255247834233.16853226279527529795.17876046919284835919.9418285952813059832.13047242839344546364
    push.0.12264235005998596237.1061976413581577609.7033214137694063977.18033224665649311218.18243486613747353899.3561247325196799511.16952491481374185391.11481791809705596603.12814085900699512956.17302321040867683019
    push.0.13745726807410668126.9623195265506456617.7465132459024384097.2251369236120399713.6448908484857918863.5099209810094831230.16212884988821190582.18249024762942812442.10688576654212525746.2231508770774915774
    push.0.3659117274757008157.1543192225857881242.18091331260842263096.9574283627610600597.2731767768751191762.11939771934778553534.11392031782150504604.12073684583747438794.6218166897950407936.5067091780869611297
    push.0.17925963073248208614.2420946697258233975.11590258730636715813.16523620421634855676.8090216466740999776.17076533921678987043.11965667210002932874.3703367931172804195.12218855078111536768.854559844467021161
    push.0.10925300850341269202.10413539874204153764.755872134421813580.9283859998879598761.14567590826741910310.15124452005028870205.13940298287036915175.5217101844427995810.6650996839180198324.10522540653602325280
    push.0.5310302679481018691.13002025835949697052.2657376563488972149.17381731082172145664.1988126946544963033.2569883524458680244.17683003090357813592.12835066093285340912.13724552189986070228.7720516663411876862
    push.0.2098954033913097307.2309477348657567165.9792068612095866719.4601919217223470864.209921127464729715.6864747001511208513.3127473742451022966.2095200909052865079.18285644234190705718.12250035273126351135
    push.0.13951827729340705833.14459570299428695304.8834792967118611579.6725813942155569814.11965961266590367121.6752821262462087255.7951529531519773407.13672715535238790890.5356461814158222661.11171072278422198668
    push.0.9475785037879277218.5799814000282413370.12050830618586740088.8318640489922411688.9525782450604333995.6528037067924106012.16619671930806928674.4541731202869057967.3376724773249963293.11615326846494295278
    push.0.482060036600150933.11467119070324730444.772782162370783688.2501605016746329496.13806966740796260753.17395111393851356405.496464070251151417.1163438811892759016.15822076317946554275.12116709547954866691
    push.0.16707389452026649361.16545077215746158984.6284549563105707361.17757608406609173277.9717337822647338211.7662836746913173697.1461453339433232094.3329907353566863894.15133164783446026669.16642661777515982141
    push.0.8740647503568834490.13860852194429510438.3084858846738769525.15244187677213710925.15883709939992049928.1664791628761154801.1001185545593491436.13383494911538359160.4227630525992527269.6200811315064218380
    push.0.3889897788799916147.7080006522627305997.12266798847982790133.4946438751805155985.12617355440493757493.2735807930768448622.9378244653857640135.5675647406953729336.5824055259058228203.9515177899200163281
    push.0.18247135586114942223.930651823751758961.9500980659160065980.6485617698547175492.8218585563975291657.390024465910129004.17080631933542322820.5579052016695440242.7879394206853648717.1761518289134831424
    push.0.4694008238210670962.15952621857965476881.17667717351796224117.6653338727111345230.16995268220155094050.6797173572371213042.16323631078576652770.15787482331396513797.12877534033819042684.988157889575088861
    push.0.1674279547847240439.1435250924888937950.9851276995492170208.9723464670014174269.2092404336422623431.7639881936754925671.1872787524744087839.5430707549711613380.8851507321606133317.16030720196980190149
    push.0.13711212967123806710.15887088256130239404.2595220097008836517.5434347759356035971.372507686096187853.6754565966913018025.1704948599447223686.10068099957244076131.4700179668342543246.779670486882791267
    push.0.2753690086438313400.17142726706751588691.9166290808720836249.6837075886864032051.12139062188611094961.18424172922597002877.3815588670109870781.8627004478936062349.17467033892888397947.5819352812585293358
    push.0.7416522198391969992.14935402090602061790.1164986419839116884.6465521407540412363.7434722558205009845.2038607148449964149.13395313493587162410.11294625583991123993.11059674469150803575.5562958095923747324
    push.0.17402734188517749578.9384909748912482961.12855309661145981139.14263359241149924626.989962272224838369.5993197802171893482.6088156318341592744.17718668168744577187.9212037435887500044.12226201445178564337
    push.0.14897024924357300153.1562476568264884437.3813679152622795675.16362797855001162531.8020672103091949348.11706793147252591339.11597327592744820141.5083990786098826838.1921517212048378446.8750838787107306140
    push.0.1445574475072043880.10739681696848516183.120197019389350304.9446766851661664000.5775386547429124152.827592948198427800.2038862546380392830.12673305441285055900.7591074197096643670.17954994351062516576
    push.0.11010613906728937753.15553739783799103380.18150279541907649276.6387659152810227687.475481362812111140.8510441759530193606.18361326491204467094.2051455984030252586.8636547702225299950.10874202386808292284
    push.0.3875814288044348177.13092410556407346344.11065596013157431778.8072585606113875869.14318692686394367220.14404632169279001489.3383856697668094061.8076721514358960292.8674333929769836934.2731679121642781444
    push.0.16814692975230914520.16901376341036136156.15558911850440836212.9556969753824379796.17445897859889023632.3642552123027051325.14817832106293132630.7664689618974147.11143638953589585330.564008936211520181
    push.0.7196603818767322618.1488537267120623150.6289002217221443332.10471398971568836530.3814158004880465012.5805069186034217881.16954189837129692855.6635834519287936661.16208647209383972720.5567731481585226298
    push.0.239259762544439417.17953781866894335075.4021873334623628700.693202588949276323.15713322409359518713.17238612229881455283.18264781200522947303.12451877540055120439.12967173555236168284.17144253759028946930
    push.0.9488066036193099190.7609307285726135346.15226476525890048429.951304918487237802.15215392690904991936.15728608918936056959.4413556859245318083.18382872221591897999.9431831293476061340.17308851420472240739
    push.0.16393420190434607441.7890575564847357140.15844012039949319321.9167034864858780068.967808157273756999.17867660461107567165.11021458037217286944.13698883855872432508.4015355417032258970.145762164142465173
    push.0.9603207458773176713.3730210125248525647.3286050544489391768.12648487516030367398.13592382833584220040.2901819371313846190.5104122707251530947.7725653442890343249.15238275104185998806.4090742016138453223
    push.0.210810417517734354.10280349760407809225.12467085246253491605.16087577135698544654.4216440044330110668.16382801033853947897.8526431679621302417.13089399225509984819.4889615900468145206.1832691135572047571
    push.0.8581518189142391170.13276657327096485270.14854627013954501930.648842038179234143.5397141448825112686.12649380431713118113.2661995322126287624.1570139004210291306.3340671711284293672.11488681418945421299
    push.0.720194206461772757.2598466967529127931.6328033201182038376.162398518823601012.16349925022211791010.14667633014198352533.14255577508614373157.9742584346892621668.8913513274800101625.6767093374636725885
    push.0.1513239383983390597.3881939293556647424.8871378906242947630.14002583970809189601.4726157027650864397.7042570309940007294.16612191256137489295.11854706250503962102.10651682766097519826.4574141681497070886
    push.0.3155555010707711936.4460170742813213974.12918577011826601505.7923346381252862495.6449483830345108895.6241667637367853546.12297116774396814851.864671203568571996.5347544684824831922.4391376230659025515
    push.0.956465015299339602.5883162714270322933.2920244646098849978.13906706522588249096.13125360647228959092.7669078422662812117.5036765305938224580.15890289968357012385.9625125309337852164.4348687462467490068
    push.0.17152286243660947940.912744779674814011.6522005594585063420.3966505992581668075.12939902333833546030.14400726150484082872.10924383168589797394.9961340207455158438.16697448387125678335.6698820774710454489
    push.0.5862151430197264537.17220471129089505109.6207972933433518405.9937849971776449565.13537076925315072235.12751110108919398786.14678188468394292210.269414110069512860.9351042882261785230.13060565083683834331
    push.0.3769256222378880867.7356414205302264082.16629501451850225958.2367456662035602199.1912171082832675337.185445556247919115.3107732428678187526.13803196323570958493.4081671325235676305.10862498472188759189
    push.0.245609228228677923.8068984295394180411.6520160845328007437.6007675525184723980.11335105319805158590.8623077240085086090.2560121534594824754.17644628569611813848.2715643884202461046.3224322244548182674
    push.0.5720046272797842877.5171576953207992001.18081066491606933869.6578136266773667727.6906118703221500909.1813488847154193177.17109324815496773176.5047397038333095232.12931353516383035550.11183471991333628399
    push.0.1707657945570475336.2462504542687865671.15584782332692965331.14623736982660005973.16447714422605359879.15785437988516389191.3353891651911668862.17850062461160875620.8897566392917907594.605271667971140511
    push.0.12381862564422678176.17455748764766298451.13673461583836657926.16229733076988992397.10381812735376079608.4918771585843991544.4138244591837273041.14839099094719211703.16168158949912222802.12621899939574432967
    push.0.12137761829331324462.13404859705288299900.15832201988566214417.7879707010841901253.7960930220941839999.6110453944225230611.5830513073868570681.6133343128763034085.3179539342662685253.2506989035164745754
    push.0.8147544997300936011.15963203259842887483.7559660486907481814.11348834105433679959.14011134952947482980.13805232482355751617.13526145272176577322.11001693783609836178.9811141336368542017.3568056640253614205
    push.0.18040565740704123592.7602424976567882797.10602326541526150057.5213312158569539556.8947887650292553776.3663695970230020386.17993030455914906557.5297386352792076176.11470201025072093702.14092593036750126868
    push.0.3849991557031585302.12788713491536107978.4249724670949531803.2062613705372431125.8754291050532289046.6916873994600256445.15951292487850507413.8600255179739064593.7841222411267298420.9535747424656304654
    push.0.950890250829509552.16276355063716717068.17724592353458626341.17951424236104136460.9947817445422442543.6157177023721387080.6495289797906016847.1949894286487165001.11443863295322289431.6286095189921468769
    push.0.13149126005278873057.17987029861039750048.3126614120924136740.7692406626841930211.17794604877501013324.14052226613575903169.17083904563253436707.15971807082071035001.7672340365510116772.15296969761744966149
    push.0.6500858963555336839.13354162830651225597.15753458316654552716.3288604620802021095.5618700860161248815.9872021803979988120.4480282083826295351.5953675707286512180.16372148924993275755.14342126748963471415
    push.0.3450353957141005227.1053332175964743902.5403614890348002847.737686714400830555.9742253169219191825.2837294335041420393.9121170542602212883.50684457416083703.13830539047164452224.14913956449955758633
    push.0.11977259427584126707.1451602330274340880.3380343861829813850.12102225861214259412.10500110994145331582.1188991365539383560.9303055952232746793.15958865059222928943.13382308822353552476.8668566869783055556
    push.0.10968643604202633427.8771882850893868695.11841575220013508845.13455675228555678898.6181744131716155809.7623903683918488549.5640517345260356312.2582320435338781532.8769938796759843928.15933156761734087162
    push.0.7572545546475353162.14551938341291651639.12769806542622065700.16811455157347462241.11947872626217715900.16144236176968740691.4168444894364409539.3335456763488459374.12136565007212109774.15108353693171004855
    push.0.7777135139827937522.3401438605277181618.8047157674983970014.1443519105569010292.14427918017848256232.17148306232484291618.1623435145844298583.14227813269199308903.7803012959148747414.1421439115643722689
    push.0.12918816973155661297.5990120507917515599.10550310673220454081.13198972032874297748.1153722405389843385.16650895406160247045.15359526225116345618.13192473669852811586.18048709634770912759.6119475593200336599
    push.0.9547040717918487999.17604012252847490935.18122182430023661464.5932155492629156991.6334593679401285465.10787855633126916939.1914698980244566192.17467924426709176187.5008762998014598176.9260043735419662118
    push.0.10316725331900106704.18108346754297695821.2229760347008894679.8868385275319276858.9399990374083867693.6469673533405007563.5671458231179582112.8682074545206485138.2060731154217444053.5115211187686634548
    push.0.14451574030524655202.9292880133922011353.695265726924629139.1033965899619237503.6160329798503928767.2589321769440641625.16140103425940382256.5049809870341304660.14235201702929378134.14886730206956011116
    push.0.9793640284382595140.8663895577921260088.2548978194165003307.17426078571020221072.14639054205878357634.2448410071095648785.2165973894480315022.5248930565894896907.4356519642755055268.12883135586176881569

    repeat.2 # process first 8 limbs of scalar
        repeat.4 # process 4 consecutive 32 -bit limbs
            repeat.32 # process each 32 -bit limb
                push.0.0.0.0
                loc_loadw_be.0

                dup
                push.1
                u32and
                movdn.4

                u32shr.1

                loc_storew_be.0
                dropw

                if.true
                    # base already on stack top
                    # bring res from memory
                    loc_load.28

                    loc_load.24
                    push.0.0.0.0
                    loc_loadw_be.20

                    loc_load.16
                    push.0.0.0.0
                    loc_loadw_be.12

                    exec.add

                    # write back res
                    loc_storew_be.12
                    dropw
                    loc_store.16

                    loc_storew_be.20
                    dropw
                    loc_store.24

                    loc_store.28
                else
                    dropw
                    dropw
                    push.0
                    dropw
                end
            end

            push.0.0.0.0
            loc_loadw_be.0

            drop
            push.0
            movdn.3

            loc_storew_be.0
            dropw
        end

        push.0.0.0.0
        loc_loadw_be.4
        loc_storew_be.0
        dropw
    end

    repeat.2 # process last 2 limbs of scalar
        repeat.32 # process each of last two 32 -bit limbs
            push.0.0.0.0
            loc_loadw_be.8

            dup
            push.1
            u32and
            movdn.4

            u32shr.1

            loc_storew_be.8
            dropw

            if.true
                # base already on stack top
                # bring res from memory
                loc_load.28

                loc_load.24
                push.0.0.0.0
                loc_loadw_be.20

                loc_load.16
                push.0.0.0.0
                loc_loadw_be.12

                exec.add

                # write back res
                loc_storew_be.12
                dropw
                loc_store.16

                loc_storew_be.20
                dropw
                loc_store.24

                loc_store.28
            else
                dropw
                dropw
                push.0
                dropw
            end
        end

        push.0.0.0.0
        loc_loadw_be.8

        drop
        push.0
        movdn.3

        loc_storew_be.8
        dropw
    end

    # bring res back to stack
    loc_load.28

    loc_load.24
    push.0.0.0.0
    loc_loadw_be.20

    loc_load.16
    push.0.0.0.0
    loc_loadw_be.12
end