pxfm 0.1.28

/*
 * // Copyright (c) Radzivon Bartoshyk 7/2025. All rights reserved.
 * //
 * // Redistribution and use in source and binary forms, with or without modification,
 * // are permitted provided that the following conditions are met:
 * //
 * // 1.  Redistributions of source code must retain the above copyright notice, this
 * // list of conditions and the following disclaimer.
 * //
 * // 2.  Redistributions in binary form must reproduce the above copyright notice,
 * // this list of conditions and the following disclaimer in the documentation
 * // and/or other materials provided with the distribution.
 * //
 * // 3.  Neither the name of the copyright holder nor the names of its
 * // contributors may be used to endorse or promote products derived from
 * // this software without specific prior written permission.
 * //
 * // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * // DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * // FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * // DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * // SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * // CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * // OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * // OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

// Digits of 2^(16*i) / pi, generated by Sollya with:
// > procedure ulp(x, n) { return 2^(floor(log2(abs(x))) - n); };
// > for i from 0 to 63 do {
//     if i < 3 then { pi_inv = 0.25 + 2^(16*(i - 3)) / pi; }
//     else { pi_inv = 2^(16*(i-3)) / pi; };
//     pn = nearestint(pi_inv);
//     pi_frac = pi_inv - pn;
//     a = round(pi_frac, 51, RN);
//     b = round(pi_frac - a, 51, RN);
//     c = round(pi_frac - a - b, 51, RN);
//     d = round(pi_frac - a - b - c, D, RN);
//     print("{", 2^7 * a, ",", 2^7 * b, ",", 2^7 * c, ",", 2^7 * d, "},");
// };
//
// Notice that for [0..2] the leading bit of 2^(16*(i - 3)) / pi is very small,
// so we add 0.25 so that the conditions for the algorithms are still satisfied,
// and one of those conditions guarantees that ulp(0.25 * x_reduced) >= 2, and
// will safely be discarded.
pub(crate) static ONE_TWENTY_EIGHT_OVER_PI: [(u64, u64, u64, u64); 128] = [
    (
        0x4040000000000014,
        0x3ce7cc1b727220a9,
        0x3983f84eafa3ea6a,
        0xb6211f924eb53362,
    ),
    (
        0x4040000000145f30,
        0x3ceb727220a94fe1,
        0x397d5f47d4d37703,
        0x361b6295993c4390,
    ),
    (
        0x404000145f306dca,
        0xbcdbbead603d8a83,
        0x395f534ddc0db629,
        0x35f664f10e4107f9,
    ),
    (
        0x40445f306dc9c883,
        0xbce6b01ec5417056,
        0xb986447e493ad4ce,
        0x362e21c820ff28b2,
    ),
    (
        0xc03f246c6efab581,
        0x3ca3abe8fa9a6ee0,
        0x394b6c52b3278872,
        0x35b07f9458eaf7af,
    ),
    (
        0x403391054a7f09d6,
        0xbca70565911f924f,
        0x3942b32788720840,
        0xb5dae9c5421443aa,
    ),
    (
        0x401529fc2757d1f5,
        0x3caa6ee06db14acd,
        0xb948778df7c035d4,
        0x35ed5ef5de2b0db9,
    ),
    (
        0xbfeec54170565912,
        0x3c4b6c52b3278872,
        0x38b07f9458eaf7af,
        0xb52d4f246dc8e2df,
    ),
    (
        0xc04505c1596447e5,
        0x3ceb14acc9e21c82,
        0x395fe5163abdebbc,
        0x35f586dc91b8e909,
    ),
    (
        0xc00596447e493ad5,
        0x3c993c439041fe51,
        0x3938eaf7aef1586e,
        0xb5cb7238b7b645a4,
    ),
    (
        0x404bb81b6c52b328,
        0xbcede37df00d74e3,
        0x3987bd778ac36e49,
        0xb611c5bdb22d1ffa,
    ),
    (
        0x404b6c52b3278872,
        0x3cb07f9458eaf7af,
        0xb92d4f246dc8e2df,
        0x35b374b801924bbb,
    ),
    (
        0x4042b32788720840,
        0xbcdae9c5421443aa,
        0x395b7246e3a424dd,
        0x35e700324977504f,
    ),
    (
        0xc048778df7c035d4,
        0x3ced5ef5de2b0db9,
        0x3971b8e909374b80,
        0x35f924bba8274648,
    ),
    (
        0xc03bef806ba71508,
        0xbcd443a9e48db91c,
        0xb976f6c8b47fe6db,
        0xb61115f62e6de302,
    ),
    (
        0xbfdae9c5421443aa,
        0x3c5b7246e3a424dd,
        0x38e700324977504f,
        0xb58cdbc603c429c7,
    ),
    (
        0xc0438a84288753c9,
        0xbccb7238b7b645a4,
        0x38f924bba8274648,
        0x359cfe1deb1cb12a,
    ),
    (
        0xc020a21d4f246dc9,
        0x3cad2126e9700325,
        0xb94a22bec5cdbc60,
        0xb5de214e34ed658c,
    ),
    (
        0xc02d4f246dc8e2df,
        0x3cb374b801924bbb,
        0xb95f62e6de301e21,
        0xb5f38d3b5963045e,
    ),
    (
        0xc03236e4716f6c8b,
        0xbcd1ff9b6d115f63,
        0x395921cfe1deb1cb,
        0x35d29a73ee88235f,
    ),
    (
        0x403b8e909374b802,
        0xbcdb6d115f62e6de,
        0xb9680f10a71a76b3,
        0x35fcfba208d7d4bb,
    ),
    (
        0x40309374b801924c,
        0xbcd15f62e6de301e,
        0xb960a71a76b2c609,
        0x3601046bea5d7689,
    ),
    (
        0xc0268ffcdb688afb,
        0xbca736f180f10a72,
        0x39462534e7dd1047,
        0xb5e0568a25dbd8b3,
    ),
    (
        0x3ff924bba8274648,
        0x3c9cfe1deb1cb12a,
        0xb9363045df7282b4,
        0xb5d44bb7b16638fe,
    ),
    (
        0xc04a22bec5cdbc60,
        0xbcde214e34ed658c,
        0xb95177dca0ad144c,
        0x35f213a671c09ad1,
    ),
    (
        0x4003a32439fc3bd6,
        0x3c9cb129a73ee882,
        0x392afa975da24275,
        0xb5b8e3f652e82070,
    ),
    (
        0xc03b78c0788538d4,
        0x3cd29a73ee88235f,
        0x3974baed1213a672,
        0xb60fb29741037d8d,
    ),
    (
        0x404fc3bd63962535,
        0xbcc822efb9415a29,
        0x396a24274ce38136,
        0xb60741037d8cdc54,
    ),
    (
        0xc014e34ed658c117,
        0xbcbf7282b4512edf,
        0x394d338e04d68bf0,
        0xb5dbec66e29c67cb,
    ),
    (
        0x40462534e7dd1047,
        0xbce0568a25dbd8b3,
        0xb96c7eca5d040df6,
        0xb5f9b8a719f2b318,
    ),
    (
        0xc0363045df7282b4,
        0xbcd44bb7b16638fe,
        0x397ad17df904e647,
        0x361639835339f49d,
    ),
    (
        0x404d1046bea5d769,
        0xbcebd8b31c7eca5d,
        0xb94037d8cdc538d0,
        0x35ea99cfa4e422fc,
    ),
    (
        0x402afa975da24275,
        0xbcb8e3f652e82070,
        0x3953991d63983534,
        0xb5f82d8dee81d108,
    ),
    (
        0xc04a28976f62cc72,
        0x3ca35a2fbf209cc9,
        0xb924e33e566305b2,
        0x35c08bf177bf2507,
    ),
    (
        0xc0476f62cc71fb29,
        0xbced040df633714e,
        0xb979f2b3182d8def,
        0x361f8bbdf9283b20,
    ),
    (
        0x404d338e04d68bf0,
        0xbcdbec66e29c67cb,
        0x3969cfa4e422fc5e,
        0xb5e036be27003b40,
    ),
    (
        0x403c09ad17df904e,
        0x3cd91d639835339f,
        0x397272117e2ef7e5,
        0xb617c4e007680022,
    ),
    (
        0x40468befc827323b,
        0xbcdc67cacc60b638,
        0x39717e2ef7e4a0ec,
        0x361ff897ffde0598,
    ),
    (
        0xc04037d8cdc538d0,
        0x3cea99cfa4e422fc,
        0x39877bf250763ff1,
        0x3617ffde05980fef,
    ),
    (
        0xc048cdc538cf9599,
        0x3cdf49c845f8bbe0,
        0xb97b5f13801da001,
        0x361e05980fef2f12,
    ),
    (
        0xc024e33e566305b2,
        0x3cc08bf177bf2507,
        0x3968ffc4bffef02d,
        0xb5ffc04343b9d298,
    ),
    (
        0xc03f2b3182d8dee8,
        0xbcbd1081b5f13802,
        0x3942fffbc0b301fe,
        0xb5ca1dce94beb25c,
    ),
    (
        0xc048c16c6f740e88,
        0xbce036be27003b40,
        0xb920fd33f8086877,
        0xb5bd297d64b824b2,
    ),
    (
        0x4043908bf177bf25,
        0x3cad8ffc4bffef03,
        0xb939fc04343b9d29,
        0xb5df592e092c9813,
    ),
    (
        0x4037e2ef7e4a0ec8,
        0xbc7da00087e99fc0,
        0xb910d0ee74a5f593,
        0x359f6d367ecf27cb,
    ),
    (
        0xc03081b5f13801da,
        0xbc20fd33f8086877,
        0xb8bd297d64b824b2,
        0xb558130d834f648b,
    ),
    (
        0xc04af89c00ed0004,
        0xbcdfa67f010d0ee7,
        0xb97297d64b824b26,
        0xb5d30d834f648b0c,
    ),
    (
        0xc04c00ed00043f4d,
        0x3c8fde5e2316b415,
        0xb912e092c98130d8,
        0xb5aa7b24585ce04d,
    ),
    (
        0x4042fffbc0b301fe,
        0xbcca1dce94beb25c,
        0xb9425930261b069f,
        0x35db74f463f669e6,
    ),
    (
        0xc020fd33f8086877,
        0xbcbd297d64b824b2,
        0xb958130d834f648b,
        0xb5c738132c3402ba,
    ),
    (
        0xc039fc04343b9d29,
        0xbcdf592e092c9813,
        0xb94b069ec9161738,
        0xb5c32c3402ba515b,
    ),
    (
        0xc010d0ee74a5f593,
        0x3c9f6d367ecf27cb,
        0x39036e9e8c7ecd3d,
        0xb5a00ae9456c229c,
    ),
    (
        0xc04dce94beb25c12,
        0xbce64c0986c1a7b2,
        0xb98161738132c340,
        0xb615d28ad8453814,
    ),
    (
        0xc044beb25c125930,
        0xbcd30d834f648b0c,
        0x3978fd9a797fa8b6,
        0xb605b08a7028341d,
    ),
    (
        0x403b47db4d9fb3ca,
        0xbcaa7b24585ce04d,
        0x3943cbfd45aea4f7,
        0x35e63f5f2f8bd9e8,
    ),
    (
        0xc0425930261b069f,
        0x3cdb74f463f669e6,
        0xb915d28ad8453814,
        0xb59a0e84c2f8c608,
    ),
    (
        0x403fb3c9f2c26dd4,
        0xbcc738132c3402ba,
        0xb96456c229c0a0d0,
        0xb60d0985f18c10eb,
    ),
    (
        0xc04b069ec9161738,
        0xbcc32c3402ba515b,
        0xb9314e050683a131,
        0x35d0739f78a5292f,
    ),
    (
        0xc04ec9161738132c,
        0xbcda015d28ad8454,
        0x397faf97c5ecf41d,
        0xb5f821d6b5b45650,
    ),
    (
        0xc0461738132c3403,
        0x3ce16ba93dd63f5f,
        0x3977c5ecf41ce7de,
        0x3604a525d4d7f6bf,
    ),
    (
        0x402fb34f2ff516bb,
        0xbccb08a7028341d1,
        0x3969e839cfbc5295,
        0xb60a2b2809409dc1,
    ),
    (
        0x4043cbfd45aea4f7,
        0x3ce63f5f2f8bd9e8,
        0x397ce7de294a4baa,
        0xb61404a04ee072a3,
    ),
    (
        0xc015d28ad8453814,
        0xbc9a0e84c2f8c608,
        0xb93d6b5b45650128,
        0xb5b3b81ca8bdea7f,
    ),
    (
        0xc0415b08a7028342,
        0x3cd7b3d0739f78a5,
        0x396497535fdafd89,
        0xb5bca8bdea7f33ee,
    ),
    (
        0x0000000000000000,
        0x0000000000000000,
        0x3c5f938a73db97fb,
        0x3f992155f7a3667c,
    ),
    (
        0xbc2912bd0d569a90,
        0x3fa91f65f10dd814,
        0x3c7ccbeeeae8129a,
        0x3fb2d52092ce19f4,
    ),
    (
        0xbc3e2718d26ed688,
        0x3fb917a6bc29b42c,
        0xbc7cbb1f71aca352,
        0x3fbf564e56a97310,
    ),
    (
        0xbc8dd9ffeaecbdc4,
        0x3fc2c8106e8e613c,
        0xbc8ab3802218894f,
        0x3fc5e214448b3fc8,
    ),
    (
        0xbc849b466e7fe360,
        0x3fc8f8b83c69a60c,
        0xbc8035e2873ca432,
        0x3fcc0b826a7e4f64,
    ),
    (
        0xbc850b7bbc4768b1,
        0x3fcf19f97b215f1c,
        0xbc83ed9efaa42ab3,
        0x3fd111d262b1f678,
    ),
    (
        0x3c9a8b5c974ee7b5,
        0x3fd294062ed59f04,
        0x3c94325f12be8946,
        0x3fd4135c94176600,
    ),
    (
        0x3c8fc2047e54e614,
        0x3fd58f9a75ab1fdc,
        0xbc9512c678219317,
        0x3fd7088530fa45a0,
    ),
    (
        0xbc92e59dba7ab4c2,
        0x3fd87de2a6aea964,
        0xbc9d24afdade848b,
        0x3fd9ef7943a8ed8c,
    ),
    (
        0x3c65b362cb974183,
        0x3fdb5d1009e15cc0,
        0xbc9e97af1a63c807,
        0x3fdcc66e9931c460,
    ),
    (
        0xbc8c3e4edc5872f8,
        0x3fde2b5d3806f63c,
        0x3c9fb44f80f92225,
        0x3fdf8ba4dbf89ab8,
    ),
    (
        0x3ca9697faf2e2fe5,
        0x3fe073879922ffec,
        0xbca7bc8eda6af93c,
        0x3fe11eb3541b4b24,
    ),
    (
        0x3c8b25dd267f6600,
        0x3fe1c73b39ae68c8,
        0xbca5769d0fbcddc3,
        0x3fe26d054cdd12e0,
    ),
    (
        0x3c9c20673b2116b2,
        0x3fe30ff7fce17034,
        0x3ca3c7c4bc72a92c,
        0x3fe3affa292050b8,
    ),
    (
        0xbcae7f895d302395,
        0x3fe44cf325091dd8,
        0x3ca13c293edceb32,
        0x3fe4e6cabbe3e5e8,
    ),
    (
        0xbc875720992bfbb2,
        0x3fe57d69348ceca0,
        0xbca24a366a5fe547,
        0x3fe610b7551d2ce0,
    ),
    (
        0x3c921165f626cdd5,
        0x3fe6a09e667f3bcc,
        0xbcabcac43c389ba9,
        0x3fe72d0837efff98,
    ),
    (
        0xbca21ea6f59be15b,
        0x3fe7b5df226aafb0,
        0x3cad217be0e2b971,
        0x3fe83b0e0bff976c,
    ),
    (
        0x3c969d0f6897664a,
        0x3fe8bc806b151740,
        0xbc9615f32b6f907a,
        0x3fe93a22499263fc,
    ),
    (
        0x3c96788ebcc76dc6,
        0x3fe9b3e047f38740,
        0x3caddae89fd441d1,
        0x3fea29a7a0462780,
    ),
    (
        0xbc9f98273c5d2495,
        0x3fea9b66290ea1a4,
        0xbc8926da300ffcce,
        0x3feb090a58150200,
    ),
    (
        0x3ca90e58336c64a8,
        0x3feb728345196e3c,
        0x3ca9f6963354e3fe,
        0x3febd7c0ac6f9528,
    ),
    (
        0x3c9a47d3a2a0dcbe,
        0x3fec38b2f180bdb0,
        0x3c9ed0489e16b9a0,
        0x3fec954b213411f4,
    ),
    (
        0xbca0f3db5dad5ac5,
        0x3feced7af43cc774,
        0x3caac42b5a8b6943,
        0x3fed4134d14dc938,
    ),
    (
        0xbcad75033dfb9ca8,
        0x3fed906bcf328d48,
        0x3c883c37c6107db3,
        0x3feddb13b6ccc23c,
    ),
    (
        0x3c97f59c49f6cd6d,
        0x3fee212104f686e4,
        0x3caee94a90d7b88b,
        0x3fee6288ec48e110,
    ),
    (
        0xbcaa27d3874701f9,
        0x3fee9f4156c62ddc,
        0xbc985f4e1b8298d0,
        0x3feed740e7684964,
    ),
    (
        0xbc9ab4e148e52d9e,
        0x3fef0a7efb9230d8,
        0x3c98a11412b82346,
        0x3fef38f3ac64e588,
    ),
    (
        0x3c7562172a361fd3,
        0x3fef6297cff75cb0,
        0x3ca3564acef1ff97,
        0x3fef8764fa714ba8,
    ),
    (
        0xbca5e82a3284d5c8,
        0x3fefa7557f08a518,
        0xbc9709bccb89a989,
        0x3fefc26470e19fd4,
    ),
    (
        0x3ca9e082721dfb8e,
        0x3fefd88da3d12524,
        0xbcaeade132f3981d,
        0x3fefe9cdad01883c,
    ),
    (
        0x3cae3a843d1db55f,
        0x3feff621e3796d7c,
        0x3c9765595d548d9a,
        0x3feffd886084cd0c,
    ),
    (
        0x0000000000000000,
        0x3ff0000000000000,
        0x3c9765595d548d9a,
        0x3feffd886084cd0c,
    ),
    (
        0x3cae3a843d1db55f,
        0x3feff621e3796d7c,
        0xbcaeade132f3981d,
        0x3fefe9cdad01883c,
    ),
    (
        0x3ca9e082721dfb8e,
        0x3fefd88da3d12524,
        0xbc9709bccb89a989,
        0x3fefc26470e19fd4,
    ),
    (
        0xbca5e82a3284d5c8,
        0x3fefa7557f08a518,
        0x3ca3564acef1ff97,
        0x3fef8764fa714ba8,
    ),
    (
        0x3c7562172a361fd3,
        0x3fef6297cff75cb0,
        0x3c98a11412b82346,
        0x3fef38f3ac64e588,
    ),
    (
        0xbc9ab4e148e52d9e,
        0x3fef0a7efb9230d8,
        0xbc985f4e1b8298d0,
        0x3feed740e7684964,
    ),
    (
        0xbcaa27d3874701f9,
        0x3fee9f4156c62ddc,
        0x3caee94a90d7b88b,
        0x3fee6288ec48e110,
    ),
    (
        0x3c97f59c49f6cd6d,
        0x3fee212104f686e4,
        0x3c883c37c6107db3,
        0x3feddb13b6ccc23c,
    ),
    (
        0xbcad75033dfb9ca8,
        0x3fed906bcf328d48,
        0x3caac42b5a8b6943,
        0x3fed4134d14dc938,
    ),
    (
        0xbca0f3db5dad5ac5,
        0x3feced7af43cc774,
        0x3c9ed0489e16b9a0,
        0x3fec954b213411f4,
    ),
    (
        0x3c9a47d3a2a0dcbe,
        0x3fec38b2f180bdb0,
        0x3ca9f6963354e3fe,
        0x3febd7c0ac6f9528,
    ),
    (
        0x3ca90e58336c64a8,
        0x3feb728345196e3c,
        0xbc8926da300ffcce,
        0x3feb090a58150200,
    ),
    (
        0xbc9f98273c5d2495,
        0x3fea9b66290ea1a4,
        0x3caddae89fd441d1,
        0x3fea29a7a0462780,
    ),
    (
        0x3c96788ebcc76dc6,
        0x3fe9b3e047f38740,
        0xbc9615f32b6f907a,
        0x3fe93a22499263fc,
    ),
    (
        0x3c969d0f6897664a,
        0x3fe8bc806b151740,
        0x3cad217be0e2b971,
        0x3fe83b0e0bff976c,
    ),
    (
        0xbca21ea6f59be15b,
        0x3fe7b5df226aafb0,
        0xbcabcac43c389ba9,
        0x3fe72d0837efff98,
    ),
    (
        0x3c921165f626cdd5,
        0x3fe6a09e667f3bcc,
        0xbca24a366a5fe547,
        0x3fe610b7551d2ce0,
    ),
    (
        0xbc875720992bfbb2,
        0x3fe57d69348ceca0,
        0x3ca13c293edceb32,
        0x3fe4e6cabbe3e5e8,
    ),
    (
        0xbcae7f895d302395,
        0x3fe44cf325091dd8,
        0x3ca3c7c4bc72a92c,
        0x3fe3affa292050b8,
    ),
    (
        0x3c9c20673b2116b2,
        0x3fe30ff7fce17034,
        0xbca5769d0fbcddc3,
        0x3fe26d054cdd12e0,
    ),
    (
        0x3c8b25dd267f6600,
        0x3fe1c73b39ae68c8,
        0xbca7bc8eda6af93c,
        0x3fe11eb3541b4b24,
    ),
    (
        0x3ca9697faf2e2fe5,
        0x3fe073879922ffec,
        0x3c9fb44f80f92225,
        0x3fdf8ba4dbf89ab8,
    ),
    (
        0xbc8c3e4edc5872f8,
        0x3fde2b5d3806f63c,
        0xbc9e97af1a63c807,
        0x3fdcc66e9931c460,
    ),
    (
        0x3c65b362cb974183,
        0x3fdb5d1009e15cc0,
        0xbc9d24afdade848b,
        0x3fd9ef7943a8ed8c,
    ),
    (
        0xbc92e59dba7ab4c2,
        0x3fd87de2a6aea964,
        0xbc9512c678219317,
        0x3fd7088530fa45a0,
    ),
    (
        0x3c8fc2047e54e614,
        0x3fd58f9a75ab1fdc,
        0x3c94325f12be8946,
        0x3fd4135c94176600,
    ),
    (
        0x3c9a8b5c974ee7b5,
        0x3fd294062ed59f04,
        0xbc83ed9efaa42ab3,
        0x3fd111d262b1f678,
    ),
    (
        0xbc850b7bbc4768b1,
        0x3fcf19f97b215f1c,
        0xbc8035e2873ca432,
        0x3fcc0b826a7e4f64,
    ),
    (
        0xbc849b466e7fe360,
        0x3fc8f8b83c69a60c,
        0xbc8ab3802218894f,
        0x3fc5e214448b3fc8,
    ),
    (
        0xbc8dd9ffeaecbdc4,
        0x3fc2c8106e8e613c,
        0xbc7cbb1f71aca352,
        0x3fbf564e56a97310,
    ),
    (
        0xbc3e2718d26ed688,
        0x3fb917a6bc29b42c,
        0x3c7ccbeeeae8129a,
        0x3fb2d52092ce19f4,
    ),
    (
        0xbc2912bd0d569a90,
        0x3fa91f65f10dd814,
        0x3c5f938a73db97fb,
        0x3f992155f7a3667c,
    ),
];