pxfm/
sincos_reduce_tables.rs

1/*
2 * // Copyright (c) Radzivon Bartoshyk 7/2025. All rights reserved.
3 * //
4 * // Redistribution and use in source and binary forms, with or without modification,
5 * // are permitted provided that the following conditions are met:
6 * //
7 * // 1.  Redistributions of source code must retain the above copyright notice, this
8 * // list of conditions and the following disclaimer.
9 * //
10 * // 2.  Redistributions in binary form must reproduce the above copyright notice,
11 * // this list of conditions and the following disclaimer in the documentation
12 * // and/or other materials provided with the distribution.
13 * //
14 * // 3.  Neither the name of the copyright holder nor the names of its
15 * // contributors may be used to endorse or promote products derived from
16 * // this software without specific prior written permission.
17 * //
18 * // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
19 * // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
20 * // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
21 * // DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
22 * // FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
23 * // DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
24 * // SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
25 * // CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
26 * // OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
27 * // OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28 */
29
30// Digits of 2^(16*i) / pi, generated by Sollya with:
31// > procedure ulp(x, n) { return 2^(floor(log2(abs(x))) - n); };
32// > for i from 0 to 63 do {
33//     if i < 3 then { pi_inv = 0.25 + 2^(16*(i - 3)) / pi; }
34//     else { pi_inv = 2^(16*(i-3)) / pi; };
35//     pn = nearestint(pi_inv);
36//     pi_frac = pi_inv - pn;
37//     a = round(pi_frac, 51, RN);
38//     b = round(pi_frac - a, 51, RN);
39//     c = round(pi_frac - a - b, 51, RN);
40//     d = round(pi_frac - a - b - c, D, RN);
41//     print("{", 2^7 * a, ",", 2^7 * b, ",", 2^7 * c, ",", 2^7 * d, "},");
42// };
43//
44// Notice that for [0..2] the leading bit of 2^(16*(i - 3)) / pi is very small,
45// so we add 0.25 so that the conditions for the algorithms are still satisfied,
46// and one of those conditions guarantees that ulp(0.25 * x_reduced) >= 2, and
47// will safely be discarded.
48pub(crate) static ONE_TWENTY_EIGHT_OVER_PI: [(u64, u64, u64, u64); 128] = [
49    (
50        0x4040000000000014,
51        0x3ce7cc1b727220a9,
52        0x3983f84eafa3ea6a,
53        0xb6211f924eb53362,
54    ),
55    (
56        0x4040000000145f30,
57        0x3ceb727220a94fe1,
58        0x397d5f47d4d37703,
59        0x361b6295993c4390,
60    ),
61    (
62        0x404000145f306dca,
63        0xbcdbbead603d8a83,
64        0x395f534ddc0db629,
65        0x35f664f10e4107f9,
66    ),
67    (
68        0x40445f306dc9c883,
69        0xbce6b01ec5417056,
70        0xb986447e493ad4ce,
71        0x362e21c820ff28b2,
72    ),
73    (
74        0xc03f246c6efab581,
75        0x3ca3abe8fa9a6ee0,
76        0x394b6c52b3278872,
77        0x35b07f9458eaf7af,
78    ),
79    (
80        0x403391054a7f09d6,
81        0xbca70565911f924f,
82        0x3942b32788720840,
83        0xb5dae9c5421443aa,
84    ),
85    (
86        0x401529fc2757d1f5,
87        0x3caa6ee06db14acd,
88        0xb948778df7c035d4,
89        0x35ed5ef5de2b0db9,
90    ),
91    (
92        0xbfeec54170565912,
93        0x3c4b6c52b3278872,
94        0x38b07f9458eaf7af,
95        0xb52d4f246dc8e2df,
96    ),
97    (
98        0xc04505c1596447e5,
99        0x3ceb14acc9e21c82,
100        0x395fe5163abdebbc,
101        0x35f586dc91b8e909,
102    ),
103    (
104        0xc00596447e493ad5,
105        0x3c993c439041fe51,
106        0x3938eaf7aef1586e,
107        0xb5cb7238b7b645a4,
108    ),
109    (
110        0x404bb81b6c52b328,
111        0xbcede37df00d74e3,
112        0x3987bd778ac36e49,
113        0xb611c5bdb22d1ffa,
114    ),
115    (
116        0x404b6c52b3278872,
117        0x3cb07f9458eaf7af,
118        0xb92d4f246dc8e2df,
119        0x35b374b801924bbb,
120    ),
121    (
122        0x4042b32788720840,
123        0xbcdae9c5421443aa,
124        0x395b7246e3a424dd,
125        0x35e700324977504f,
126    ),
127    (
128        0xc048778df7c035d4,
129        0x3ced5ef5de2b0db9,
130        0x3971b8e909374b80,
131        0x35f924bba8274648,
132    ),
133    (
134        0xc03bef806ba71508,
135        0xbcd443a9e48db91c,
136        0xb976f6c8b47fe6db,
137        0xb61115f62e6de302,
138    ),
139    (
140        0xbfdae9c5421443aa,
141        0x3c5b7246e3a424dd,
142        0x38e700324977504f,
143        0xb58cdbc603c429c7,
144    ),
145    (
146        0xc0438a84288753c9,
147        0xbccb7238b7b645a4,
148        0x38f924bba8274648,
149        0x359cfe1deb1cb12a,
150    ),
151    (
152        0xc020a21d4f246dc9,
153        0x3cad2126e9700325,
154        0xb94a22bec5cdbc60,
155        0xb5de214e34ed658c,
156    ),
157    (
158        0xc02d4f246dc8e2df,
159        0x3cb374b801924bbb,
160        0xb95f62e6de301e21,
161        0xb5f38d3b5963045e,
162    ),
163    (
164        0xc03236e4716f6c8b,
165        0xbcd1ff9b6d115f63,
166        0x395921cfe1deb1cb,
167        0x35d29a73ee88235f,
168    ),
169    (
170        0x403b8e909374b802,
171        0xbcdb6d115f62e6de,
172        0xb9680f10a71a76b3,
173        0x35fcfba208d7d4bb,
174    ),
175    (
176        0x40309374b801924c,
177        0xbcd15f62e6de301e,
178        0xb960a71a76b2c609,
179        0x3601046bea5d7689,
180    ),
181    (
182        0xc0268ffcdb688afb,
183        0xbca736f180f10a72,
184        0x39462534e7dd1047,
185        0xb5e0568a25dbd8b3,
186    ),
187    (
188        0x3ff924bba8274648,
189        0x3c9cfe1deb1cb12a,
190        0xb9363045df7282b4,
191        0xb5d44bb7b16638fe,
192    ),
193    (
194        0xc04a22bec5cdbc60,
195        0xbcde214e34ed658c,
196        0xb95177dca0ad144c,
197        0x35f213a671c09ad1,
198    ),
199    (
200        0x4003a32439fc3bd6,
201        0x3c9cb129a73ee882,
202        0x392afa975da24275,
203        0xb5b8e3f652e82070,
204    ),
205    (
206        0xc03b78c0788538d4,
207        0x3cd29a73ee88235f,
208        0x3974baed1213a672,
209        0xb60fb29741037d8d,
210    ),
211    (
212        0x404fc3bd63962535,
213        0xbcc822efb9415a29,
214        0x396a24274ce38136,
215        0xb60741037d8cdc54,
216    ),
217    (
218        0xc014e34ed658c117,
219        0xbcbf7282b4512edf,
220        0x394d338e04d68bf0,
221        0xb5dbec66e29c67cb,
222    ),
223    (
224        0x40462534e7dd1047,
225        0xbce0568a25dbd8b3,
226        0xb96c7eca5d040df6,
227        0xb5f9b8a719f2b318,
228    ),
229    (
230        0xc0363045df7282b4,
231        0xbcd44bb7b16638fe,
232        0x397ad17df904e647,
233        0x361639835339f49d,
234    ),
235    (
236        0x404d1046bea5d769,
237        0xbcebd8b31c7eca5d,
238        0xb94037d8cdc538d0,
239        0x35ea99cfa4e422fc,
240    ),
241    (
242        0x402afa975da24275,
243        0xbcb8e3f652e82070,
244        0x3953991d63983534,
245        0xb5f82d8dee81d108,
246    ),
247    (
248        0xc04a28976f62cc72,
249        0x3ca35a2fbf209cc9,
250        0xb924e33e566305b2,
251        0x35c08bf177bf2507,
252    ),
253    (
254        0xc0476f62cc71fb29,
255        0xbced040df633714e,
256        0xb979f2b3182d8def,
257        0x361f8bbdf9283b20,
258    ),
259    (
260        0x404d338e04d68bf0,
261        0xbcdbec66e29c67cb,
262        0x3969cfa4e422fc5e,
263        0xb5e036be27003b40,
264    ),
265    (
266        0x403c09ad17df904e,
267        0x3cd91d639835339f,
268        0x397272117e2ef7e5,
269        0xb617c4e007680022,
270    ),
271    (
272        0x40468befc827323b,
273        0xbcdc67cacc60b638,
274        0x39717e2ef7e4a0ec,
275        0x361ff897ffde0598,
276    ),
277    (
278        0xc04037d8cdc538d0,
279        0x3cea99cfa4e422fc,
280        0x39877bf250763ff1,
281        0x3617ffde05980fef,
282    ),
283    (
284        0xc048cdc538cf9599,
285        0x3cdf49c845f8bbe0,
286        0xb97b5f13801da001,
287        0x361e05980fef2f12,
288    ),
289    (
290        0xc024e33e566305b2,
291        0x3cc08bf177bf2507,
292        0x3968ffc4bffef02d,
293        0xb5ffc04343b9d298,
294    ),
295    (
296        0xc03f2b3182d8dee8,
297        0xbcbd1081b5f13802,
298        0x3942fffbc0b301fe,
299        0xb5ca1dce94beb25c,
300    ),
301    (
302        0xc048c16c6f740e88,
303        0xbce036be27003b40,
304        0xb920fd33f8086877,
305        0xb5bd297d64b824b2,
306    ),
307    (
308        0x4043908bf177bf25,
309        0x3cad8ffc4bffef03,
310        0xb939fc04343b9d29,
311        0xb5df592e092c9813,
312    ),
313    (
314        0x4037e2ef7e4a0ec8,
315        0xbc7da00087e99fc0,
316        0xb910d0ee74a5f593,
317        0x359f6d367ecf27cb,
318    ),
319    (
320        0xc03081b5f13801da,
321        0xbc20fd33f8086877,
322        0xb8bd297d64b824b2,
323        0xb558130d834f648b,
324    ),
325    (
326        0xc04af89c00ed0004,
327        0xbcdfa67f010d0ee7,
328        0xb97297d64b824b26,
329        0xb5d30d834f648b0c,
330    ),
331    (
332        0xc04c00ed00043f4d,
333        0x3c8fde5e2316b415,
334        0xb912e092c98130d8,
335        0xb5aa7b24585ce04d,
336    ),
337    (
338        0x4042fffbc0b301fe,
339        0xbcca1dce94beb25c,
340        0xb9425930261b069f,
341        0x35db74f463f669e6,
342    ),
343    (
344        0xc020fd33f8086877,
345        0xbcbd297d64b824b2,
346        0xb958130d834f648b,
347        0xb5c738132c3402ba,
348    ),
349    (
350        0xc039fc04343b9d29,
351        0xbcdf592e092c9813,
352        0xb94b069ec9161738,
353        0xb5c32c3402ba515b,
354    ),
355    (
356        0xc010d0ee74a5f593,
357        0x3c9f6d367ecf27cb,
358        0x39036e9e8c7ecd3d,
359        0xb5a00ae9456c229c,
360    ),
361    (
362        0xc04dce94beb25c12,
363        0xbce64c0986c1a7b2,
364        0xb98161738132c340,
365        0xb615d28ad8453814,
366    ),
367    (
368        0xc044beb25c125930,
369        0xbcd30d834f648b0c,
370        0x3978fd9a797fa8b6,
371        0xb605b08a7028341d,
372    ),
373    (
374        0x403b47db4d9fb3ca,
375        0xbcaa7b24585ce04d,
376        0x3943cbfd45aea4f7,
377        0x35e63f5f2f8bd9e8,
378    ),
379    (
380        0xc0425930261b069f,
381        0x3cdb74f463f669e6,
382        0xb915d28ad8453814,
383        0xb59a0e84c2f8c608,
384    ),
385    (
386        0x403fb3c9f2c26dd4,
387        0xbcc738132c3402ba,
388        0xb96456c229c0a0d0,
389        0xb60d0985f18c10eb,
390    ),
391    (
392        0xc04b069ec9161738,
393        0xbcc32c3402ba515b,
394        0xb9314e050683a131,
395        0x35d0739f78a5292f,
396    ),
397    (
398        0xc04ec9161738132c,
399        0xbcda015d28ad8454,
400        0x397faf97c5ecf41d,
401        0xb5f821d6b5b45650,
402    ),
403    (
404        0xc0461738132c3403,
405        0x3ce16ba93dd63f5f,
406        0x3977c5ecf41ce7de,
407        0x3604a525d4d7f6bf,
408    ),
409    (
410        0x402fb34f2ff516bb,
411        0xbccb08a7028341d1,
412        0x3969e839cfbc5295,
413        0xb60a2b2809409dc1,
414    ),
415    (
416        0x4043cbfd45aea4f7,
417        0x3ce63f5f2f8bd9e8,
418        0x397ce7de294a4baa,
419        0xb61404a04ee072a3,
420    ),
421    (
422        0xc015d28ad8453814,
423        0xbc9a0e84c2f8c608,
424        0xb93d6b5b45650128,
425        0xb5b3b81ca8bdea7f,
426    ),
427    (
428        0xc0415b08a7028342,
429        0x3cd7b3d0739f78a5,
430        0x396497535fdafd89,
431        0xb5bca8bdea7f33ee,
432    ),
433    (
434        0x0000000000000000,
435        0x0000000000000000,
436        0x3c5f938a73db97fb,
437        0x3f992155f7a3667c,
438    ),
439    (
440        0xbc2912bd0d569a90,
441        0x3fa91f65f10dd814,
442        0x3c7ccbeeeae8129a,
443        0x3fb2d52092ce19f4,
444    ),
445    (
446        0xbc3e2718d26ed688,
447        0x3fb917a6bc29b42c,
448        0xbc7cbb1f71aca352,
449        0x3fbf564e56a97310,
450    ),
451    (
452        0xbc8dd9ffeaecbdc4,
453        0x3fc2c8106e8e613c,
454        0xbc8ab3802218894f,
455        0x3fc5e214448b3fc8,
456    ),
457    (
458        0xbc849b466e7fe360,
459        0x3fc8f8b83c69a60c,
460        0xbc8035e2873ca432,
461        0x3fcc0b826a7e4f64,
462    ),
463    (
464        0xbc850b7bbc4768b1,
465        0x3fcf19f97b215f1c,
466        0xbc83ed9efaa42ab3,
467        0x3fd111d262b1f678,
468    ),
469    (
470        0x3c9a8b5c974ee7b5,
471        0x3fd294062ed59f04,
472        0x3c94325f12be8946,
473        0x3fd4135c94176600,
474    ),
475    (
476        0x3c8fc2047e54e614,
477        0x3fd58f9a75ab1fdc,
478        0xbc9512c678219317,
479        0x3fd7088530fa45a0,
480    ),
481    (
482        0xbc92e59dba7ab4c2,
483        0x3fd87de2a6aea964,
484        0xbc9d24afdade848b,
485        0x3fd9ef7943a8ed8c,
486    ),
487    (
488        0x3c65b362cb974183,
489        0x3fdb5d1009e15cc0,
490        0xbc9e97af1a63c807,
491        0x3fdcc66e9931c460,
492    ),
493    (
494        0xbc8c3e4edc5872f8,
495        0x3fde2b5d3806f63c,
496        0x3c9fb44f80f92225,
497        0x3fdf8ba4dbf89ab8,
498    ),
499    (
500        0x3ca9697faf2e2fe5,
501        0x3fe073879922ffec,
502        0xbca7bc8eda6af93c,
503        0x3fe11eb3541b4b24,
504    ),
505    (
506        0x3c8b25dd267f6600,
507        0x3fe1c73b39ae68c8,
508        0xbca5769d0fbcddc3,
509        0x3fe26d054cdd12e0,
510    ),
511    (
512        0x3c9c20673b2116b2,
513        0x3fe30ff7fce17034,
514        0x3ca3c7c4bc72a92c,
515        0x3fe3affa292050b8,
516    ),
517    (
518        0xbcae7f895d302395,
519        0x3fe44cf325091dd8,
520        0x3ca13c293edceb32,
521        0x3fe4e6cabbe3e5e8,
522    ),
523    (
524        0xbc875720992bfbb2,
525        0x3fe57d69348ceca0,
526        0xbca24a366a5fe547,
527        0x3fe610b7551d2ce0,
528    ),
529    (
530        0x3c921165f626cdd5,
531        0x3fe6a09e667f3bcc,
532        0xbcabcac43c389ba9,
533        0x3fe72d0837efff98,
534    ),
535    (
536        0xbca21ea6f59be15b,
537        0x3fe7b5df226aafb0,
538        0x3cad217be0e2b971,
539        0x3fe83b0e0bff976c,
540    ),
541    (
542        0x3c969d0f6897664a,
543        0x3fe8bc806b151740,
544        0xbc9615f32b6f907a,
545        0x3fe93a22499263fc,
546    ),
547    (
548        0x3c96788ebcc76dc6,
549        0x3fe9b3e047f38740,
550        0x3caddae89fd441d1,
551        0x3fea29a7a0462780,
552    ),
553    (
554        0xbc9f98273c5d2495,
555        0x3fea9b66290ea1a4,
556        0xbc8926da300ffcce,
557        0x3feb090a58150200,
558    ),
559    (
560        0x3ca90e58336c64a8,
561        0x3feb728345196e3c,
562        0x3ca9f6963354e3fe,
563        0x3febd7c0ac6f9528,
564    ),
565    (
566        0x3c9a47d3a2a0dcbe,
567        0x3fec38b2f180bdb0,
568        0x3c9ed0489e16b9a0,
569        0x3fec954b213411f4,
570    ),
571    (
572        0xbca0f3db5dad5ac5,
573        0x3feced7af43cc774,
574        0x3caac42b5a8b6943,
575        0x3fed4134d14dc938,
576    ),
577    (
578        0xbcad75033dfb9ca8,
579        0x3fed906bcf328d48,
580        0x3c883c37c6107db3,
581        0x3feddb13b6ccc23c,
582    ),
583    (
584        0x3c97f59c49f6cd6d,
585        0x3fee212104f686e4,
586        0x3caee94a90d7b88b,
587        0x3fee6288ec48e110,
588    ),
589    (
590        0xbcaa27d3874701f9,
591        0x3fee9f4156c62ddc,
592        0xbc985f4e1b8298d0,
593        0x3feed740e7684964,
594    ),
595    (
596        0xbc9ab4e148e52d9e,
597        0x3fef0a7efb9230d8,
598        0x3c98a11412b82346,
599        0x3fef38f3ac64e588,
600    ),
601    (
602        0x3c7562172a361fd3,
603        0x3fef6297cff75cb0,
604        0x3ca3564acef1ff97,
605        0x3fef8764fa714ba8,
606    ),
607    (
608        0xbca5e82a3284d5c8,
609        0x3fefa7557f08a518,
610        0xbc9709bccb89a989,
611        0x3fefc26470e19fd4,
612    ),
613    (
614        0x3ca9e082721dfb8e,
615        0x3fefd88da3d12524,
616        0xbcaeade132f3981d,
617        0x3fefe9cdad01883c,
618    ),
619    (
620        0x3cae3a843d1db55f,
621        0x3feff621e3796d7c,
622        0x3c9765595d548d9a,
623        0x3feffd886084cd0c,
624    ),
625    (
626        0x0000000000000000,
627        0x3ff0000000000000,
628        0x3c9765595d548d9a,
629        0x3feffd886084cd0c,
630    ),
631    (
632        0x3cae3a843d1db55f,
633        0x3feff621e3796d7c,
634        0xbcaeade132f3981d,
635        0x3fefe9cdad01883c,
636    ),
637    (
638        0x3ca9e082721dfb8e,
639        0x3fefd88da3d12524,
640        0xbc9709bccb89a989,
641        0x3fefc26470e19fd4,
642    ),
643    (
644        0xbca5e82a3284d5c8,
645        0x3fefa7557f08a518,
646        0x3ca3564acef1ff97,
647        0x3fef8764fa714ba8,
648    ),
649    (
650        0x3c7562172a361fd3,
651        0x3fef6297cff75cb0,
652        0x3c98a11412b82346,
653        0x3fef38f3ac64e588,
654    ),
655    (
656        0xbc9ab4e148e52d9e,
657        0x3fef0a7efb9230d8,
658        0xbc985f4e1b8298d0,
659        0x3feed740e7684964,
660    ),
661    (
662        0xbcaa27d3874701f9,
663        0x3fee9f4156c62ddc,
664        0x3caee94a90d7b88b,
665        0x3fee6288ec48e110,
666    ),
667    (
668        0x3c97f59c49f6cd6d,
669        0x3fee212104f686e4,
670        0x3c883c37c6107db3,
671        0x3feddb13b6ccc23c,
672    ),
673    (
674        0xbcad75033dfb9ca8,
675        0x3fed906bcf328d48,
676        0x3caac42b5a8b6943,
677        0x3fed4134d14dc938,
678    ),
679    (
680        0xbca0f3db5dad5ac5,
681        0x3feced7af43cc774,
682        0x3c9ed0489e16b9a0,
683        0x3fec954b213411f4,
684    ),
685    (
686        0x3c9a47d3a2a0dcbe,
687        0x3fec38b2f180bdb0,
688        0x3ca9f6963354e3fe,
689        0x3febd7c0ac6f9528,
690    ),
691    (
692        0x3ca90e58336c64a8,
693        0x3feb728345196e3c,
694        0xbc8926da300ffcce,
695        0x3feb090a58150200,
696    ),
697    (
698        0xbc9f98273c5d2495,
699        0x3fea9b66290ea1a4,
700        0x3caddae89fd441d1,
701        0x3fea29a7a0462780,
702    ),
703    (
704        0x3c96788ebcc76dc6,
705        0x3fe9b3e047f38740,
706        0xbc9615f32b6f907a,
707        0x3fe93a22499263fc,
708    ),
709    (
710        0x3c969d0f6897664a,
711        0x3fe8bc806b151740,
712        0x3cad217be0e2b971,
713        0x3fe83b0e0bff976c,
714    ),
715    (
716        0xbca21ea6f59be15b,
717        0x3fe7b5df226aafb0,
718        0xbcabcac43c389ba9,
719        0x3fe72d0837efff98,
720    ),
721    (
722        0x3c921165f626cdd5,
723        0x3fe6a09e667f3bcc,
724        0xbca24a366a5fe547,
725        0x3fe610b7551d2ce0,
726    ),
727    (
728        0xbc875720992bfbb2,
729        0x3fe57d69348ceca0,
730        0x3ca13c293edceb32,
731        0x3fe4e6cabbe3e5e8,
732    ),
733    (
734        0xbcae7f895d302395,
735        0x3fe44cf325091dd8,
736        0x3ca3c7c4bc72a92c,
737        0x3fe3affa292050b8,
738    ),
739    (
740        0x3c9c20673b2116b2,
741        0x3fe30ff7fce17034,
742        0xbca5769d0fbcddc3,
743        0x3fe26d054cdd12e0,
744    ),
745    (
746        0x3c8b25dd267f6600,
747        0x3fe1c73b39ae68c8,
748        0xbca7bc8eda6af93c,
749        0x3fe11eb3541b4b24,
750    ),
751    (
752        0x3ca9697faf2e2fe5,
753        0x3fe073879922ffec,
754        0x3c9fb44f80f92225,
755        0x3fdf8ba4dbf89ab8,
756    ),
757    (
758        0xbc8c3e4edc5872f8,
759        0x3fde2b5d3806f63c,
760        0xbc9e97af1a63c807,
761        0x3fdcc66e9931c460,
762    ),
763    (
764        0x3c65b362cb974183,
765        0x3fdb5d1009e15cc0,
766        0xbc9d24afdade848b,
767        0x3fd9ef7943a8ed8c,
768    ),
769    (
770        0xbc92e59dba7ab4c2,
771        0x3fd87de2a6aea964,
772        0xbc9512c678219317,
773        0x3fd7088530fa45a0,
774    ),
775    (
776        0x3c8fc2047e54e614,
777        0x3fd58f9a75ab1fdc,
778        0x3c94325f12be8946,
779        0x3fd4135c94176600,
780    ),
781    (
782        0x3c9a8b5c974ee7b5,
783        0x3fd294062ed59f04,
784        0xbc83ed9efaa42ab3,
785        0x3fd111d262b1f678,
786    ),
787    (
788        0xbc850b7bbc4768b1,
789        0x3fcf19f97b215f1c,
790        0xbc8035e2873ca432,
791        0x3fcc0b826a7e4f64,
792    ),
793    (
794        0xbc849b466e7fe360,
795        0x3fc8f8b83c69a60c,
796        0xbc8ab3802218894f,
797        0x3fc5e214448b3fc8,
798    ),
799    (
800        0xbc8dd9ffeaecbdc4,
801        0x3fc2c8106e8e613c,
802        0xbc7cbb1f71aca352,
803        0x3fbf564e56a97310,
804    ),
805    (
806        0xbc3e2718d26ed688,
807        0x3fb917a6bc29b42c,
808        0x3c7ccbeeeae8129a,
809        0x3fb2d52092ce19f4,
810    ),
811    (
812        0xbc2912bd0d569a90,
813        0x3fa91f65f10dd814,
814        0x3c5f938a73db97fb,
815        0x3f992155f7a3667c,
816    ),
817];