mithril-common 0.7.14

/// If there is a need to update this data, we can run the `verify_kes_key_cache_content` test in
/// `test::builder::fixture_builder.rs` which generates the code of this function.
pub fn cached_kes_key(kes_key_seed: &[u8]) -> Option<([u8; 612], [u8; 32])> {
    let (kes_bytes, kes_verification_key) = match kes_key_seed {
        [
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                128, 187, 141, 128, 160, 231, 239, 110, 82, 252, 249, 34, 220, 14, 143, 165, 242,
                90, 4, 236, 214, 96, 227, 50, 71, 244, 188, 40, 141, 216, 137, 210, 206, 165, 21,
                189, 4, 148, 200, 150, 184, 216, 7, 97, 48, 185, 125, 24, 59, 246, 162, 241, 133,
                123, 210, 127, 22, 136, 236, 156, 255, 227, 65, 230, 167, 220, 108, 71, 68, 38, 29,
                177, 148, 78, 242, 26, 66, 29, 118, 13, 203, 222, 83, 4, 3, 80, 150, 45, 238, 178,
                82, 152, 207, 54, 128, 158, 100, 214, 191, 130, 126, 80, 215, 9, 177, 40, 83, 223,
                154, 116, 16, 89, 0, 185, 180, 127, 190, 162, 190, 81, 111, 80, 137, 49, 49, 65, 9,
                149, 218, 132, 101, 230, 222, 131, 28, 186, 236, 85, 139, 144, 207, 0, 169, 229,
                111, 154, 175, 219, 155, 161, 105, 118, 221, 211, 205, 141, 175, 215, 241, 179, 92,
                96, 106, 82, 88, 58, 93, 156, 194, 30, 148, 255, 143, 74, 33, 242, 22, 74, 234, 10,
                236, 188, 221, 100, 43, 234, 253, 188, 105, 76, 163, 82, 240, 214, 189, 217, 49,
                36, 51, 133, 156, 55, 208, 173, 238, 2, 158, 79, 162, 173, 164, 157, 55, 118, 189,
                23, 31, 103, 153, 23, 41, 49, 80, 10, 178, 81, 52, 31, 215, 188, 64, 7, 98, 103,
                180, 75, 31, 6, 204, 146, 174, 33, 36, 156, 233, 196, 3, 68, 114, 226, 17, 9, 30,
                52, 234, 86, 11, 201, 206, 198, 244, 223, 131, 101, 79, 41, 215, 53, 121, 187, 193,
                71, 50, 105, 235, 89, 100, 80, 106, 43, 90, 173, 66, 24, 53, 76, 147, 190, 159,
                104, 91, 95, 230, 197, 204, 45, 46, 18, 238, 244, 116, 74, 202, 160, 71, 147, 236,
                181, 208, 129, 239, 132, 64, 30, 242, 196, 206, 237, 234, 213, 93, 35, 127, 238,
                129, 90, 58, 134, 38, 5, 8, 236, 78, 253, 213, 190, 39, 20, 131, 141, 93, 41, 211,
                45, 35, 88, 213, 37, 241, 68, 32, 81, 25, 248, 225, 211, 73, 242, 227, 34, 175,
                171, 42, 196, 152, 10, 107, 158, 162, 66, 229, 239, 224, 148, 197, 90, 11, 174,
                108, 228, 221, 10, 9, 158, 96, 231, 69, 86, 251, 145, 105, 34, 255, 50, 230, 129,
                248, 132, 228, 123, 24, 233, 185, 204, 144, 44, 11, 71, 9, 73, 127, 149, 142, 99,
                24, 7, 199, 255, 128, 84, 137, 24, 186, 142, 79, 83, 227, 233, 12, 245, 7, 136, 48,
                192, 186, 163, 62, 51, 28, 105, 62, 109, 27, 21, 191, 140, 158, 202, 85, 231, 208,
                66, 120, 135, 163, 22, 10, 173, 97, 154, 53, 156, 156, 30, 247, 103, 171, 207, 17,
                243, 168, 196, 132, 210, 39, 128, 98, 114, 117, 49, 242, 215, 97, 129, 119, 90,
                210, 168, 125, 124, 40, 235, 62, 149, 47, 205, 119, 81, 239, 88, 74, 234, 185, 122,
                232, 87, 207, 35, 98, 164, 46, 87, 15, 215, 229, 255, 142, 152, 79, 220, 219, 176,
                87, 167, 140, 199, 154, 105, 227, 110, 134, 224, 70, 136, 28, 196, 49, 99, 97, 24,
                48, 167, 156, 4, 240, 242, 104, 125, 146, 246, 134, 129, 61, 146, 201, 205, 30, 41,
                125, 29, 193, 122, 54, 244, 102, 147, 200, 231, 102, 113, 190, 132, 89, 55, 26,
                131, 251, 94, 153, 224, 168, 137, 190, 18, 132, 119, 222, 14, 51, 34, 160, 215,
                182, 254, 235, 247, 201, 18, 151, 35, 215, 40, 102, 56, 151, 25, 229, 122, 0, 0, 0,
                0,
            ],
            [
                230, 80, 215, 83, 21, 9, 187, 108, 255, 215, 153, 140, 40, 198, 142, 78, 200, 250,
                98, 26, 9, 82, 32, 110, 161, 30, 176, 63, 205, 125, 203, 41,
            ],
        ),
        [
            1,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                210, 93, 249, 195, 14, 165, 182, 98, 135, 235, 9, 62, 35, 186, 42, 18, 30, 110, 58,
                10, 118, 221, 21, 226, 247, 117, 252, 206, 2, 209, 41, 212, 36, 91, 172, 163, 39,
                33, 169, 243, 119, 30, 61, 249, 211, 182, 147, 125, 128, 82, 237, 1, 150, 52, 93,
                205, 51, 13, 222, 123, 176, 30, 183, 177, 26, 246, 109, 161, 160, 99, 129, 84, 223,
                59, 144, 76, 31, 153, 177, 114, 227, 190, 15, 107, 251, 66, 12, 209, 130, 152, 223,
                216, 2, 216, 99, 193, 187, 70, 56, 31, 8, 225, 222, 7, 225, 44, 229, 119, 2, 111,
                47, 70, 243, 250, 227, 139, 144, 122, 136, 1, 122, 148, 90, 14, 4, 162, 238, 255,
                132, 153, 107, 152, 59, 29, 54, 227, 110, 187, 175, 133, 48, 88, 154, 133, 88, 140,
                123, 250, 62, 129, 52, 147, 154, 53, 200, 193, 134, 18, 219, 107, 44, 38, 111, 27,
                122, 142, 111, 236, 34, 101, 21, 197, 119, 33, 110, 50, 115, 215, 162, 252, 217,
                108, 99, 115, 107, 15, 173, 246, 214, 239, 47, 56, 127, 12, 175, 157, 26, 42, 23,
                39, 175, 167, 248, 225, 91, 243, 176, 99, 12, 58, 28, 80, 154, 139, 159, 138, 254,
                147, 28, 234, 128, 80, 79, 87, 181, 84, 53, 246, 130, 176, 139, 221, 15, 181, 70,
                53, 138, 250, 6, 5, 199, 87, 205, 200, 83, 198, 190, 33, 90, 0, 163, 220, 19, 126,
                204, 208, 247, 194, 163, 188, 253, 28, 53, 69, 176, 38, 238, 32, 92, 119, 113, 71,
                24, 101, 208, 181, 196, 52, 182, 117, 243, 150, 136, 44, 99, 211, 36, 52, 29, 31,
                137, 205, 112, 252, 140, 233, 85, 128, 96, 15, 108, 27, 25, 73, 83, 184, 11, 28,
                86, 186, 29, 161, 91, 210, 176, 109, 153, 127, 217, 99, 16, 247, 210, 177, 206,
                252, 67, 207, 174, 128, 206, 218, 245, 45, 228, 9, 65, 135, 32, 52, 148, 26, 157,
                250, 31, 249, 95, 237, 80, 16, 207, 56, 147, 161, 220, 177, 121, 11, 211, 247, 224,
                90, 254, 190, 52, 161, 87, 63, 116, 48, 78, 0, 162, 115, 227, 156, 137, 53, 49,
                141, 196, 195, 196, 48, 156, 191, 147, 80, 16, 127, 113, 90, 186, 58, 215, 234,
                143, 213, 113, 177, 35, 46, 194, 28, 125, 80, 150, 39, 63, 54, 177, 137, 19, 71,
                52, 186, 79, 98, 22, 10, 164, 18, 188, 205, 236, 160, 251, 138, 239, 22, 220, 86,
                243, 62, 29, 177, 132, 22, 182, 199, 118, 178, 217, 228, 254, 221, 8, 230, 28, 209,
                169, 114, 81, 232, 132, 230, 173, 4, 53, 64, 118, 188, 49, 38, 112, 198, 52, 142,
                120, 248, 128, 80, 239, 55, 126, 226, 42, 69, 89, 24, 14, 49, 55, 103, 196, 161,
                31, 202, 119, 53, 133, 181, 37, 172, 192, 71, 57, 211, 101, 101, 220, 74, 198, 37,
                202, 48, 5, 83, 197, 239, 249, 58, 189, 3, 168, 225, 143, 44, 4, 38, 159, 36, 255,
                2, 12, 240, 222, 239, 25, 206, 25, 170, 58, 72, 181, 23, 0, 229, 5, 31, 119, 70,
                162, 47, 146, 237, 26, 224, 81, 41, 134, 252, 126, 29, 65, 182, 37, 24, 99, 35, 32,
                103, 249, 76, 198, 150, 69, 128, 4, 181, 183, 2, 101, 33, 209, 16, 158, 243, 185,
                241, 138, 237, 172, 106, 245, 249, 193, 251, 125, 35, 253, 221, 25, 65, 194, 148,
                135, 196, 228, 130, 112, 94, 194, 189, 249, 180, 173, 60, 0, 0, 0, 0,
            ],
            [
                220, 182, 153, 148, 26, 157, 158, 196, 1, 198, 147, 188, 177, 228, 236, 244, 160,
                40, 71, 39, 160, 100, 249, 10, 11, 185, 159, 166, 199, 118, 182, 139,
            ],
        ),
        [
            2,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                76, 77, 214, 152, 97, 253, 163, 35, 174, 150, 149, 11, 47, 60, 44, 69, 10, 101,
                166, 175, 20, 2, 3, 95, 214, 246, 83, 162, 246, 189, 177, 232, 252, 14, 69, 60, 11,
                249, 78, 244, 127, 233, 91, 197, 23, 10, 106, 137, 195, 89, 169, 172, 186, 135,
                225, 7, 149, 197, 25, 195, 200, 168, 47, 202, 164, 125, 238, 199, 38, 183, 38, 14,
                58, 50, 88, 5, 17, 6, 164, 131, 58, 46, 168, 131, 27, 216, 167, 122, 143, 33, 170,
                155, 225, 83, 189, 217, 32, 68, 144, 21, 177, 237, 121, 148, 11, 194, 3, 92, 96,
                50, 225, 112, 160, 254, 118, 120, 67, 188, 41, 232, 220, 49, 100, 218, 67, 206,
                173, 69, 42, 53, 63, 162, 92, 119, 253, 247, 117, 160, 104, 255, 31, 153, 159, 255,
                52, 84, 178, 232, 80, 214, 157, 114, 70, 226, 47, 51, 184, 185, 31, 74, 141, 201,
                140, 183, 199, 49, 152, 108, 120, 158, 87, 219, 108, 81, 65, 168, 237, 207, 248,
                119, 102, 55, 185, 50, 101, 0, 47, 151, 127, 250, 86, 55, 60, 13, 137, 41, 92, 223,
                0, 97, 205, 142, 74, 59, 167, 213, 254, 140, 241, 115, 80, 152, 248, 216, 87, 92,
                97, 5, 31, 8, 178, 238, 22, 112, 203, 55, 13, 15, 112, 104, 113, 124, 165, 198, 78,
                189, 88, 154, 120, 82, 86, 164, 139, 178, 98, 28, 57, 150, 249, 7, 219, 121, 58,
                115, 104, 175, 41, 85, 20, 242, 214, 33, 39, 130, 93, 92, 0, 184, 198, 54, 135,
                214, 60, 39, 216, 160, 130, 88, 63, 27, 186, 209, 149, 68, 159, 19, 72, 167, 235,
                84, 208, 176, 209, 56, 208, 250, 27, 123, 254, 54, 118, 114, 173, 43, 26, 203, 26,
                80, 159, 45, 72, 29, 190, 195, 28, 52, 179, 187, 79, 93, 213, 195, 235, 221, 33,
                233, 125, 171, 170, 183, 253, 53, 202, 175, 6, 80, 119, 8, 190, 25, 48, 224, 105,
                108, 91, 97, 38, 80, 140, 114, 163, 70, 93, 128, 193, 203, 163, 149, 119, 63, 190,
                62, 7, 204, 75, 165, 124, 44, 154, 163, 244, 112, 88, 196, 152, 213, 18, 239, 108,
                74, 146, 93, 220, 33, 68, 62, 158, 65, 122, 9, 247, 199, 229, 119, 68, 244, 220,
                39, 190, 50, 28, 110, 244, 137, 134, 171, 228, 15, 143, 11, 45, 84, 197, 109, 17,
                154, 211, 177, 187, 38, 9, 66, 86, 207, 251, 208, 241, 41, 186, 10, 87, 33, 237,
                16, 150, 243, 127, 104, 17, 238, 76, 253, 5, 124, 123, 53, 51, 55, 101, 52, 106,
                239, 170, 87, 170, 225, 209, 113, 68, 65, 103, 228, 202, 89, 29, 123, 210, 95, 176,
                197, 74, 246, 163, 64, 238, 113, 228, 91, 2, 225, 227, 71, 208, 151, 55, 113, 58,
                231, 161, 170, 87, 247, 66, 109, 114, 249, 96, 106, 190, 132, 173, 34, 132, 58,
                132, 17, 162, 253, 32, 131, 138, 138, 227, 223, 34, 103, 30, 187, 121, 172, 230,
                39, 197, 220, 184, 82, 95, 199, 178, 53, 58, 174, 136, 58, 188, 213, 29, 55, 8,
                242, 164, 49, 177, 155, 217, 13, 144, 140, 156, 32, 18, 133, 149, 220, 67, 81, 206,
                72, 169, 217, 188, 239, 146, 239, 202, 85, 13, 103, 186, 221, 195, 59, 49, 153,
                176, 177, 116, 69, 43, 252, 142, 83, 119, 105, 102, 207, 33, 48, 229, 183, 126,
                126, 126, 180, 202, 57, 57, 211, 156, 40, 145, 76, 72, 247, 26, 38, 109, 178, 0, 0,
                0, 0,
            ],
            [
                221, 44, 88, 255, 31, 20, 114, 241, 109, 225, 1, 83, 142, 238, 60, 111, 228, 32,
                95, 25, 232, 148, 236, 63, 219, 153, 75, 178, 229, 197, 169, 124,
            ],
        ),
        [
            3,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                25, 238, 160, 109, 164, 222, 38, 150, 154, 217, 116, 63, 8, 54, 9, 78, 67, 96, 44,
                179, 128, 251, 217, 132, 234, 44, 157, 10, 96, 85, 79, 52, 153, 72, 116, 12, 196,
                70, 79, 141, 162, 193, 5, 59, 220, 225, 69, 24, 125, 7, 132, 226, 131, 141, 225,
                134, 179, 31, 77, 13, 125, 197, 43, 57, 175, 179, 11, 90, 218, 196, 22, 220, 56,
                73, 160, 75, 183, 57, 72, 170, 56, 210, 37, 1, 197, 132, 44, 114, 70, 151, 28, 188,
                180, 38, 90, 59, 132, 229, 115, 104, 63, 100, 84, 100, 19, 17, 236, 121, 234, 229,
                201, 164, 194, 219, 114, 255, 159, 231, 130, 216, 134, 206, 86, 4, 153, 117, 248,
                59, 115, 67, 224, 247, 138, 237, 195, 61, 130, 87, 113, 0, 65, 97, 219, 88, 15,
                228, 246, 106, 53, 6, 201, 92, 148, 15, 159, 249, 184, 169, 99, 67, 101, 44, 159,
                8, 154, 143, 162, 37, 196, 193, 72, 183, 23, 127, 244, 53, 240, 243, 228, 53, 76,
                45, 136, 137, 212, 9, 170, 116, 114, 85, 170, 106, 198, 139, 225, 62, 226, 228,
                133, 139, 250, 118, 118, 131, 50, 222, 159, 82, 164, 185, 202, 206, 228, 101, 47,
                72, 102, 136, 170, 170, 120, 57, 9, 122, 248, 124, 216, 139, 138, 223, 2, 225, 227,
                149, 165, 22, 138, 170, 99, 84, 198, 3, 212, 17, 78, 232, 13, 228, 223, 106, 161,
                218, 164, 248, 143, 233, 185, 22, 48, 215, 194, 151, 17, 192, 10, 86, 54, 195, 237,
                141, 139, 159, 30, 8, 125, 172, 237, 83, 252, 42, 42, 240, 62, 219, 225, 27, 121,
                75, 43, 240, 181, 186, 95, 81, 79, 252, 133, 105, 52, 195, 201, 175, 64, 107, 175,
                224, 223, 115, 212, 93, 93, 78, 147, 67, 240, 243, 130, 7, 216, 253, 128, 197, 28,
                25, 151, 5, 252, 128, 41, 124, 252, 98, 201, 6, 223, 66, 5, 114, 230, 180, 21, 185,
                147, 178, 195, 195, 109, 212, 77, 33, 214, 35, 88, 87, 93, 82, 141, 214, 243, 227,
                167, 101, 133, 45, 92, 228, 246, 0, 96, 59, 36, 27, 128, 165, 201, 56, 58, 198, 33,
                110, 24, 226, 141, 235, 175, 129, 133, 57, 216, 249, 165, 172, 154, 234, 190, 152,
                231, 121, 173, 220, 91, 242, 59, 58, 229, 159, 106, 97, 55, 145, 251, 128, 128,
                241, 142, 42, 77, 227, 156, 28, 51, 176, 39, 19, 123, 103, 33, 34, 168, 244, 37,
                158, 228, 118, 20, 106, 140, 155, 169, 144, 227, 219, 214, 144, 56, 100, 43, 85,
                134, 173, 237, 232, 166, 188, 206, 254, 187, 195, 233, 163, 231, 88, 205, 43, 223,
                196, 9, 56, 167, 106, 105, 231, 216, 102, 88, 217, 191, 152, 68, 154, 168, 19, 64,
                127, 185, 39, 155, 147, 125, 70, 107, 164, 144, 51, 120, 34, 18, 234, 239, 252, 49,
                25, 87, 155, 200, 28, 94, 230, 179, 209, 71, 167, 202, 76, 129, 83, 9, 104, 148,
                204, 248, 13, 245, 100, 48, 106, 252, 119, 112, 206, 94, 58, 250, 96, 58, 217, 126,
                169, 39, 5, 201, 211, 107, 254, 1, 253, 4, 226, 100, 96, 25, 35, 46, 132, 79, 252,
                57, 93, 25, 14, 2, 210, 160, 142, 70, 63, 100, 58, 28, 237, 221, 24, 191, 72, 8,
                113, 20, 190, 27, 35, 47, 254, 54, 12, 23, 85, 135, 105, 12, 127, 237, 132, 224,
                22, 169, 216, 89, 76, 199, 171, 82, 32, 237, 61, 138, 164, 149, 90, 0, 0, 0, 0,
            ],
            [
                187, 249, 4, 79, 86, 107, 53, 190, 106, 137, 217, 26, 173, 41, 155, 230, 240, 88,
                156, 248, 43, 46, 162, 131, 174, 252, 171, 241, 89, 244, 83, 49,
            ],
        ),
        [
            4,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                228, 185, 33, 133, 42, 222, 133, 221, 109, 99, 95, 16, 205, 50, 210, 113, 151, 229,
                239, 164, 160, 235, 185, 61, 51, 118, 11, 67, 65, 157, 79, 207, 126, 117, 95, 68,
                165, 114, 191, 138, 107, 49, 172, 68, 85, 11, 4, 242, 191, 15, 233, 169, 148, 244,
                173, 73, 139, 19, 175, 15, 47, 132, 86, 83, 239, 158, 166, 13, 198, 75, 187, 165,
                138, 133, 24, 57, 197, 171, 161, 76, 109, 149, 209, 109, 178, 182, 78, 91, 197, 41,
                119, 224, 65, 116, 158, 88, 224, 183, 232, 177, 110, 120, 227, 98, 173, 147, 65,
                240, 227, 228, 70, 11, 194, 102, 133, 60, 53, 165, 116, 187, 150, 111, 77, 66, 156,
                125, 4, 38, 125, 254, 121, 81, 241, 16, 71, 172, 31, 252, 143, 75, 20, 210, 97,
                154, 198, 112, 162, 26, 172, 191, 34, 224, 58, 205, 132, 222, 7, 12, 231, 107, 138,
                216, 38, 193, 215, 23, 198, 212, 8, 232, 151, 222, 42, 183, 216, 94, 13, 109, 120,
                43, 250, 11, 81, 98, 245, 200, 167, 231, 253, 117, 73, 190, 16, 105, 52, 33, 156,
                193, 78, 21, 2, 251, 45, 127, 76, 212, 159, 153, 206, 221, 10, 96, 39, 86, 103, 60,
                110, 114, 19, 132, 33, 175, 243, 225, 206, 57, 129, 40, 152, 142, 47, 61, 152, 224,
                9, 4, 222, 154, 226, 168, 17, 105, 154, 80, 44, 119, 220, 40, 236, 100, 162, 120,
                160, 76, 177, 226, 188, 213, 169, 143, 89, 186, 254, 186, 89, 22, 196, 181, 36, 22,
                176, 89, 148, 101, 205, 33, 95, 66, 5, 173, 144, 242, 145, 246, 99, 225, 35, 31,
                117, 18, 114, 108, 86, 165, 180, 171, 6, 119, 246, 205, 192, 178, 16, 149, 77, 248,
                145, 187, 169, 147, 75, 64, 254, 109, 66, 216, 191, 189, 34, 56, 63, 225, 126, 40,
                10, 249, 168, 108, 180, 228, 230, 26, 226, 56, 18, 141, 51, 202, 200, 25, 209, 87,
                37, 39, 122, 254, 224, 223, 20, 211, 135, 67, 57, 101, 0, 240, 235, 92, 246, 132,
                35, 107, 94, 155, 208, 211, 128, 246, 99, 124, 174, 143, 164, 148, 137, 229, 225,
                115, 165, 250, 136, 75, 156, 102, 98, 200, 170, 180, 105, 190, 95, 232, 15, 142,
                228, 53, 44, 67, 63, 184, 123, 37, 69, 125, 47, 111, 45, 29, 157, 32, 118, 56, 193,
                40, 124, 160, 79, 47, 202, 136, 233, 180, 94, 242, 90, 186, 183, 84, 135, 80, 43,
                172, 161, 54, 127, 81, 246, 31, 170, 47, 69, 45, 113, 234, 158, 83, 79, 26, 196,
                202, 20, 88, 5, 112, 43, 64, 151, 23, 88, 85, 205, 56, 238, 32, 62, 19, 8, 203,
                254, 10, 4, 134, 20, 54, 218, 10, 101, 23, 119, 168, 97, 118, 104, 20, 222, 26, 80,
                237, 129, 254, 151, 12, 25, 220, 123, 15, 191, 109, 166, 117, 183, 107, 147, 87,
                230, 215, 235, 112, 115, 47, 174, 196, 143, 91, 191, 179, 166, 134, 246, 118, 13,
                200, 225, 174, 203, 120, 58, 64, 145, 40, 247, 37, 56, 183, 249, 149, 53, 213, 179,
                55, 241, 221, 47, 65, 251, 51, 40, 83, 199, 62, 216, 86, 185, 240, 33, 124, 140,
                101, 210, 254, 167, 29, 88, 243, 153, 143, 135, 31, 225, 18, 232, 18, 53, 29, 227,
                13, 115, 125, 122, 171, 209, 75, 205, 23, 82, 180, 20, 39, 220, 11, 9, 193, 113,
                146, 119, 5, 38, 2, 102, 50, 224, 199, 195, 93, 117, 40, 125, 246, 0, 0, 0, 0,
            ],
            [
                228, 233, 42, 103, 141, 57, 76, 25, 145, 41, 160, 159, 45, 46, 210, 29, 56, 66,
                225, 90, 143, 193, 113, 93, 52, 179, 200, 240, 102, 83, 173, 184,
            ],
        ),
        [
            5,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                209, 107, 167, 55, 10, 147, 210, 134, 52, 184, 0, 89, 80, 242, 88, 183, 228, 254,
                176, 180, 236, 167, 121, 176, 1, 50, 94, 247, 32, 106, 165, 65, 171, 71, 210, 164,
                121, 209, 201, 202, 123, 6, 143, 170, 29, 182, 191, 98, 245, 37, 103, 99, 131, 141,
                201, 54, 218, 119, 192, 103, 234, 192, 180, 193, 135, 169, 218, 240, 228, 104, 100,
                226, 140, 89, 248, 7, 250, 235, 228, 100, 107, 8, 82, 252, 247, 186, 104, 234, 237,
                50, 40, 22, 31, 182, 139, 84, 9, 43, 151, 12, 90, 248, 124, 17, 239, 103, 205, 119,
                172, 151, 149, 216, 230, 189, 124, 104, 168, 30, 18, 57, 190, 47, 104, 40, 121, 26,
                126, 205, 134, 145, 191, 228, 100, 45, 108, 21, 195, 161, 157, 59, 140, 146, 101,
                16, 210, 214, 14, 156, 177, 132, 123, 112, 224, 228, 57, 130, 123, 99, 122, 200,
                230, 54, 2, 204, 85, 44, 73, 149, 150, 53, 15, 40, 26, 243, 227, 225, 82, 38, 151,
                223, 142, 151, 247, 233, 112, 1, 208, 131, 127, 94, 35, 116, 161, 189, 68, 124,
                234, 109, 208, 31, 177, 198, 19, 186, 156, 112, 206, 107, 183, 23, 107, 60, 161,
                167, 65, 112, 252, 46, 224, 179, 60, 54, 55, 215, 30, 158, 222, 65, 106, 194, 221,
                66, 221, 131, 240, 193, 70, 174, 26, 51, 16, 9, 101, 134, 121, 28, 64, 6, 70, 208,
                247, 75, 180, 178, 168, 167, 124, 5, 49, 48, 41, 196, 250, 50, 115, 108, 16, 8, 34,
                155, 65, 75, 121, 140, 191, 29, 152, 205, 187, 76, 113, 11, 181, 64, 217, 52, 17,
                39, 181, 35, 54, 105, 166, 248, 37, 132, 141, 29, 4, 196, 62, 164, 186, 135, 222,
                14, 63, 209, 3, 39, 171, 23, 159, 181, 77, 4, 124, 183, 20, 221, 120, 107, 218,
                218, 112, 136, 219, 1, 147, 191, 60, 196, 20, 232, 65, 195, 21, 189, 249, 104, 22,
                107, 104, 106, 49, 156, 132, 175, 151, 22, 166, 250, 117, 141, 198, 218, 170, 138,
                143, 246, 37, 182, 123, 232, 27, 47, 58, 36, 1, 217, 137, 30, 93, 223, 225, 16, 94,
                133, 60, 150, 132, 118, 86, 37, 155, 206, 139, 69, 191, 68, 55, 80, 90, 56, 49, 75,
                77, 90, 112, 249, 8, 164, 122, 85, 120, 87, 252, 126, 178, 21, 214, 222, 191, 147,
                79, 133, 192, 2, 131, 140, 164, 121, 218, 203, 255, 183, 248, 154, 183, 232, 217,
                11, 208, 90, 125, 100, 87, 155, 86, 39, 91, 12, 191, 137, 170, 23, 30, 90, 142,
                129, 6, 250, 31, 211, 77, 6, 36, 248, 247, 226, 1, 161, 59, 142, 205, 59, 191, 245,
                155, 219, 192, 180, 249, 61, 44, 155, 213, 188, 126, 164, 165, 162, 227, 74, 104,
                42, 49, 231, 144, 42, 129, 142, 143, 68, 3, 114, 89, 84, 1, 191, 203, 56, 32, 36,
                61, 84, 104, 192, 95, 145, 118, 8, 162, 105, 1, 64, 115, 234, 194, 92, 175, 15, 86,
                142, 154, 239, 39, 21, 45, 109, 110, 223, 106, 235, 66, 145, 225, 136, 139, 213,
                188, 127, 11, 213, 18, 97, 111, 189, 227, 223, 170, 66, 0, 103, 51, 85, 136, 61,
                29, 47, 238, 246, 72, 118, 80, 181, 175, 104, 210, 247, 4, 79, 59, 250, 25, 127,
                81, 89, 226, 71, 52, 25, 88, 65, 83, 248, 95, 113, 10, 148, 58, 36, 42, 247, 168,
                252, 18, 107, 110, 249, 143, 163, 184, 149, 135, 117, 147, 22, 0, 0, 0, 0,
            ],
            [
                82, 168, 182, 80, 236, 4, 194, 123, 240, 190, 4, 252, 216, 206, 73, 217, 54, 113,
                3, 123, 189, 152, 59, 20, 156, 171, 23, 48, 17, 133, 142, 94,
            ],
        ),
        [
            6,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                18, 99, 90, 253, 190, 227, 177, 127, 57, 101, 196, 15, 247, 136, 94, 213, 101, 62,
                239, 159, 103, 190, 84, 235, 107, 118, 68, 143, 91, 160, 91, 64, 217, 129, 23, 5,
                230, 199, 30, 170, 166, 11, 254, 212, 107, 238, 25, 113, 223, 36, 76, 135, 134, 21,
                13, 44, 89, 219, 157, 5, 132, 117, 42, 162, 151, 28, 187, 89, 244, 38, 40, 71, 104,
                139, 98, 34, 82, 160, 221, 0, 110, 30, 40, 137, 125, 68, 7, 214, 132, 160, 195, 1,
                122, 110, 116, 244, 189, 17, 233, 142, 122, 149, 0, 239, 216, 61, 104, 174, 194,
                236, 9, 50, 173, 186, 175, 139, 69, 66, 132, 20, 78, 181, 197, 233, 30, 61, 174,
                238, 46, 26, 18, 73, 228, 94, 186, 109, 110, 218, 195, 220, 249, 165, 127, 93, 77,
                220, 228, 64, 72, 234, 210, 99, 111, 169, 135, 221, 22, 85, 62, 247, 203, 122, 59,
                237, 158, 69, 34, 85, 211, 130, 179, 71, 65, 194, 48, 12, 83, 0, 36, 21, 189, 142,
                33, 220, 233, 82, 128, 76, 92, 101, 132, 122, 112, 234, 62, 214, 81, 114, 205, 245,
                127, 59, 148, 158, 27, 52, 106, 170, 240, 117, 136, 243, 114, 78, 213, 116, 141,
                57, 216, 78, 60, 70, 151, 207, 229, 82, 125, 28, 137, 120, 175, 118, 194, 169, 7,
                114, 10, 175, 174, 219, 168, 151, 135, 108, 69, 69, 220, 30, 39, 52, 90, 123, 207,
                232, 185, 182, 161, 30, 86, 122, 5, 35, 149, 210, 119, 85, 122, 23, 141, 145, 78,
                137, 174, 105, 51, 24, 173, 236, 70, 221, 14, 135, 80, 119, 144, 60, 28, 166, 52,
                243, 144, 159, 192, 218, 107, 159, 68, 56, 103, 31, 130, 82, 31, 103, 29, 133, 122,
                21, 20, 3, 87, 183, 251, 192, 97, 49, 208, 100, 230, 170, 235, 245, 213, 89, 68,
                221, 113, 240, 191, 250, 98, 26, 252, 34, 175, 161, 171, 113, 97, 141, 56, 176,
                234, 74, 165, 173, 154, 106, 16, 232, 169, 92, 195, 47, 181, 16, 132, 140, 102,
                220, 226, 139, 101, 119, 237, 97, 9, 206, 10, 195, 178, 87, 26, 102, 9, 29, 227,
                63, 74, 240, 246, 33, 111, 42, 0, 78, 61, 226, 65, 32, 27, 61, 219, 168, 33, 134,
                64, 33, 64, 152, 203, 164, 115, 126, 178, 0, 21, 137, 109, 103, 89, 230, 18, 46,
                157, 94, 195, 14, 77, 86, 233, 86, 35, 245, 168, 111, 160, 203, 156, 201, 13, 9,
                95, 135, 56, 77, 103, 161, 76, 186, 227, 7, 147, 131, 57, 229, 87, 251, 165, 195,
                24, 113, 223, 63, 240, 27, 96, 89, 150, 122, 223, 160, 133, 25, 128, 245, 111, 206,
                53, 231, 0, 145, 167, 143, 232, 34, 29, 216, 21, 192, 30, 169, 73, 146, 138, 214,
                55, 111, 42, 87, 238, 45, 61, 228, 32, 41, 43, 128, 120, 1, 135, 177, 204, 134,
                174, 95, 147, 42, 128, 61, 228, 219, 254, 158, 20, 29, 168, 246, 58, 43, 62, 227,
                60, 157, 90, 196, 163, 249, 34, 157, 40, 35, 188, 4, 9, 9, 113, 114, 204, 226, 221,
                165, 66, 70, 229, 126, 42, 93, 38, 9, 122, 73, 248, 62, 172, 255, 123, 23, 137,
                123, 116, 44, 188, 206, 44, 116, 189, 188, 13, 214, 179, 163, 44, 31, 141, 46, 234,
                22, 87, 46, 121, 118, 34, 80, 24, 6, 114, 20, 166, 29, 79, 110, 137, 248, 136, 97,
                25, 19, 84, 58, 212, 189, 62, 28, 142, 171, 112, 233, 0, 0, 0, 0,
            ],
            [
                142, 207, 162, 102, 170, 11, 206, 116, 39, 103, 20, 69, 126, 75, 198, 106, 53, 119,
                13, 100, 221, 100, 218, 124, 113, 218, 144, 194, 180, 197, 20, 60,
            ],
        ),
        [
            7,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                128, 119, 139, 98, 88, 169, 77, 1, 195, 80, 102, 60, 183, 246, 219, 214, 249, 46,
                75, 243, 48, 32, 3, 67, 8, 70, 103, 140, 110, 55, 121, 97, 114, 16, 152, 85, 225,
                72, 58, 87, 0, 155, 119, 136, 77, 225, 106, 99, 27, 88, 114, 237, 148, 220, 124,
                80, 228, 250, 133, 6, 86, 182, 244, 137, 84, 245, 224, 239, 7, 2, 180, 3, 163, 117,
                161, 102, 90, 233, 242, 70, 101, 159, 210, 86, 4, 200, 67, 70, 67, 51, 218, 195,
                37, 49, 130, 219, 71, 166, 58, 188, 210, 12, 252, 245, 75, 127, 83, 145, 215, 213,
                137, 29, 165, 38, 172, 180, 115, 60, 75, 233, 113, 117, 219, 176, 36, 164, 239, 20,
                52, 170, 62, 84, 6, 26, 155, 44, 36, 124, 150, 172, 185, 69, 9, 72, 102, 160, 18,
                14, 239, 169, 147, 228, 35, 180, 197, 52, 254, 211, 148, 189, 63, 159, 39, 234,
                131, 109, 253, 27, 183, 156, 140, 119, 113, 55, 60, 22, 97, 169, 13, 244, 43, 212,
                130, 65, 51, 43, 80, 30, 19, 59, 18, 221, 125, 110, 46, 200, 17, 68, 15, 48, 105,
                89, 131, 108, 73, 115, 254, 171, 212, 59, 4, 70, 79, 171, 147, 8, 188, 189, 216,
                145, 60, 181, 249, 226, 87, 93, 187, 57, 118, 252, 170, 237, 47, 80, 150, 63, 244,
                9, 148, 12, 32, 249, 13, 53, 104, 95, 183, 195, 33, 215, 125, 122, 118, 50, 84, 58,
                60, 205, 93, 212, 78, 197, 190, 88, 104, 193, 160, 205, 119, 33, 139, 141, 163,
                248, 199, 145, 98, 85, 154, 226, 46, 241, 10, 107, 56, 181, 210, 155, 216, 154, 19,
                105, 238, 194, 234, 70, 213, 18, 96, 137, 82, 177, 173, 3, 175, 3, 57, 111, 243,
                10, 53, 49, 28, 140, 51, 122, 16, 104, 161, 188, 62, 204, 89, 149, 99, 254, 12, 2,
                211, 149, 223, 204, 235, 22, 99, 83, 121, 24, 169, 65, 214, 165, 217, 100, 165, 26,
                119, 239, 128, 24, 184, 250, 59, 17, 238, 35, 39, 41, 229, 147, 113, 11, 166, 205,
                245, 2, 222, 147, 151, 242, 237, 252, 0, 151, 131, 245, 152, 116, 39, 70, 210, 125,
                82, 139, 81, 234, 122, 41, 246, 131, 74, 74, 37, 195, 192, 75, 84, 29, 213, 35, 25,
                57, 141, 166, 153, 254, 116, 28, 224, 136, 133, 28, 249, 164, 64, 20, 216, 142,
                152, 19, 228, 228, 56, 146, 2, 76, 222, 27, 192, 223, 223, 66, 232, 168, 142, 4,
                17, 119, 39, 14, 62, 25, 251, 200, 210, 131, 206, 50, 178, 135, 109, 54, 175, 210,
                50, 202, 137, 247, 255, 76, 32, 31, 33, 109, 96, 224, 70, 196, 227, 109, 45, 30,
                227, 65, 170, 83, 179, 131, 39, 177, 71, 85, 3, 101, 160, 110, 69, 253, 71, 146,
                165, 203, 93, 209, 159, 9, 252, 146, 79, 157, 73, 67, 101, 46, 172, 47, 220, 140,
                139, 51, 221, 232, 131, 143, 77, 0, 235, 152, 118, 104, 245, 8, 89, 67, 140, 219,
                7, 32, 25, 240, 141, 133, 193, 183, 4, 70, 19, 211, 234, 11, 189, 35, 99, 208, 243,
                127, 13, 240, 129, 230, 111, 41, 143, 28, 96, 132, 151, 98, 141, 172, 11, 63, 218,
                88, 119, 164, 117, 60, 91, 10, 129, 37, 139, 130, 131, 1, 187, 127, 23, 141, 192,
                99, 239, 196, 196, 103, 129, 61, 78, 134, 209, 35, 97, 76, 95, 242, 156, 31, 165,
                234, 60, 28, 124, 242, 165, 50, 208, 167, 0, 0, 0, 0,
            ],
            [
                152, 88, 235, 194, 80, 172, 172, 33, 230, 44, 141, 167, 215, 240, 95, 248, 194,
                136, 250, 239, 163, 86, 51, 45, 147, 68, 47, 247, 55, 82, 111, 176,
            ],
        ),
        [
            8,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                182, 109, 140, 211, 64, 96, 122, 219, 197, 151, 29, 193, 30, 68, 92, 212, 87, 28,
                53, 102, 129, 178, 95, 32, 31, 254, 180, 15, 98, 23, 26, 127, 152, 174, 204, 217,
                28, 54, 138, 211, 97, 35, 110, 214, 151, 138, 215, 116, 214, 16, 201, 98, 197, 166,
                10, 106, 12, 74, 16, 171, 131, 184, 127, 179, 62, 248, 99, 147, 189, 111, 247, 107,
                232, 89, 46, 195, 141, 238, 114, 55, 206, 223, 158, 154, 97, 69, 135, 244, 99, 93,
                223, 91, 144, 96, 78, 33, 109, 55, 216, 247, 109, 183, 82, 3, 102, 131, 159, 77,
                250, 108, 53, 214, 239, 227, 138, 204, 145, 28, 255, 45, 241, 155, 0, 147, 129,
                129, 155, 29, 25, 247, 13, 103, 89, 95, 95, 117, 230, 0, 217, 38, 184, 122, 247,
                87, 95, 183, 197, 213, 250, 234, 153, 237, 92, 201, 176, 150, 108, 252, 253, 74,
                230, 66, 82, 90, 56, 105, 100, 150, 73, 164, 20, 186, 118, 79, 93, 234, 98, 50, 4,
                160, 155, 234, 211, 140, 227, 86, 97, 65, 96, 235, 10, 174, 149, 239, 17, 154, 209,
                243, 39, 105, 218, 86, 229, 191, 9, 76, 185, 14, 11, 96, 89, 227, 254, 242, 71,
                155, 196, 161, 89, 39, 154, 229, 234, 88, 48, 9, 189, 199, 83, 135, 126, 164, 247,
                176, 253, 132, 234, 33, 93, 9, 68, 153, 93, 56, 216, 87, 182, 194, 182, 48, 67,
                146, 137, 23, 209, 86, 5, 156, 8, 30, 108, 139, 171, 150, 41, 165, 204, 148, 251,
                249, 201, 248, 100, 33, 129, 124, 82, 171, 125, 169, 45, 3, 156, 93, 255, 99, 60,
                232, 32, 47, 133, 65, 163, 227, 25, 165, 131, 141, 48, 23, 103, 114, 250, 126, 222,
                71, 244, 59, 201, 93, 170, 91, 47, 15, 11, 139, 94, 108, 162, 234, 186, 141, 140,
                33, 165, 228, 124, 15, 25, 65, 99, 162, 33, 118, 129, 116, 252, 203, 62, 226, 115,
                208, 255, 63, 35, 162, 226, 169, 39, 172, 170, 167, 110, 150, 216, 178, 234, 98,
                230, 124, 160, 83, 116, 25, 82, 79, 84, 224, 11, 244, 158, 86, 250, 158, 83, 124,
                211, 18, 209, 205, 220, 11, 1, 226, 92, 243, 70, 119, 162, 132, 154, 160, 16, 106,
                100, 59, 163, 232, 7, 166, 164, 62, 17, 214, 108, 178, 190, 109, 6, 17, 128, 76,
                37, 88, 219, 253, 1, 13, 79, 18, 181, 218, 171, 54, 205, 112, 14, 101, 99, 85, 99,
                121, 110, 185, 132, 130, 111, 128, 222, 200, 134, 213, 163, 146, 135, 196, 136,
                214, 189, 252, 61, 102, 108, 213, 97, 144, 205, 70, 244, 186, 191, 119, 219, 19,
                30, 95, 198, 71, 248, 9, 119, 145, 220, 240, 44, 150, 223, 15, 43, 169, 199, 106,
                201, 51, 198, 252, 158, 38, 47, 95, 79, 20, 221, 215, 96, 131, 191, 109, 18, 119,
                197, 114, 124, 132, 23, 128, 241, 98, 249, 88, 167, 187, 88, 56, 162, 16, 174, 124,
                218, 3, 175, 252, 126, 50, 55, 192, 244, 42, 6, 161, 249, 150, 41, 210, 209, 210,
                157, 234, 219, 255, 142, 164, 26, 181, 16, 90, 233, 6, 242, 27, 215, 123, 153, 109,
                150, 209, 179, 142, 246, 136, 128, 151, 159, 3, 154, 25, 197, 11, 8, 176, 138, 83,
                27, 33, 225, 95, 39, 113, 116, 180, 22, 134, 150, 85, 82, 33, 218, 9, 27, 33, 55,
                35, 197, 11, 202, 176, 32, 57, 16, 79, 55, 175, 107, 16, 40, 38, 196, 207, 0, 0, 0,
                0,
            ],
            [
                123, 153, 8, 242, 239, 71, 28, 37, 104, 48, 48, 126, 183, 158, 163, 245, 101, 161,
                14, 163, 245, 185, 219, 11, 103, 118, 58, 145, 162, 56, 41, 94,
            ],
        ),
        [
            9,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
            0,
        ] => (
            [
                63, 95, 47, 36, 206, 31, 213, 108, 221, 175, 130, 240, 101, 114, 25, 135, 38, 151,
                158, 255, 133, 47, 96, 169, 204, 61, 167, 196, 154, 233, 159, 87, 158, 8, 19, 145,
                177, 60, 26, 4, 9, 90, 211, 121, 17, 145, 71, 111, 183, 193, 240, 157, 175, 28, 33,
                100, 232, 31, 4, 152, 139, 172, 98, 90, 36, 255, 194, 163, 81, 134, 50, 136, 140,
                110, 106, 163, 212, 166, 63, 94, 53, 127, 158, 12, 11, 138, 234, 106, 90, 89, 224,
                13, 7, 86, 55, 113, 140, 155, 64, 235, 53, 39, 128, 68, 171, 111, 254, 33, 233, 67,
                83, 234, 101, 16, 173, 68, 20, 77, 38, 48, 169, 136, 248, 171, 147, 102, 134, 150,
                64, 27, 23, 137, 193, 16, 120, 18, 236, 253, 250, 91, 113, 194, 48, 26, 231, 233,
                112, 186, 237, 66, 249, 52, 100, 117, 54, 189, 185, 24, 222, 249, 114, 129, 188,
                73, 23, 186, 25, 185, 231, 134, 216, 220, 220, 162, 147, 131, 31, 196, 79, 81, 155,
                147, 174, 207, 163, 31, 244, 85, 71, 88, 193, 11, 61, 194, 232, 63, 74, 21, 243,
                216, 70, 159, 59, 11, 99, 25, 60, 127, 75, 203, 165, 56, 127, 155, 221, 154, 96,
                209, 23, 64, 49, 207, 111, 154, 194, 184, 85, 48, 24, 169, 68, 61, 239, 41, 195,
                100, 139, 184, 175, 181, 109, 61, 124, 214, 82, 4, 99, 171, 180, 101, 78, 131, 84,
                74, 164, 225, 0, 14, 115, 131, 233, 124, 69, 61, 54, 25, 50, 251, 15, 184, 187,
                141, 222, 201, 97, 167, 113, 47, 94, 117, 164, 207, 155, 101, 247, 46, 24, 60, 199,
                144, 196, 209, 253, 159, 1, 192, 159, 97, 32, 8, 147, 157, 216, 54, 123, 35, 74,
                244, 26, 138, 27, 153, 5, 89, 112, 243, 169, 21, 68, 99, 44, 179, 205, 161, 90,
                220, 12, 141, 37, 234, 63, 159, 247, 62, 225, 183, 212, 207, 199, 176, 90, 8, 187,
                162, 124, 118, 100, 132, 60, 34, 220, 226, 214, 95, 134, 59, 13, 182, 175, 213, 82,
                25, 95, 251, 109, 249, 188, 69, 137, 131, 202, 171, 23, 214, 26, 173, 144, 170,
                222, 204, 14, 109, 141, 19, 216, 165, 244, 212, 129, 243, 70, 219, 221, 82, 44, 7,
                82, 197, 185, 19, 18, 68, 168, 228, 93, 67, 89, 184, 156, 88, 18, 35, 238, 243, 44,
                124, 224, 104, 9, 226, 184, 36, 27, 246, 152, 34, 109, 17, 236, 33, 64, 51, 196,
                247, 88, 32, 119, 241, 75, 110, 133, 126, 118, 77, 10, 87, 179, 214, 97, 160, 87,
                144, 82, 170, 30, 43, 155, 167, 35, 98, 250, 69, 187, 236, 227, 230, 98, 0, 1, 252,
                121, 245, 69, 52, 222, 191, 81, 227, 62, 94, 55, 209, 128, 116, 150, 60, 88, 173,
                5, 15, 223, 47, 156, 220, 127, 121, 48, 184, 189, 192, 28, 250, 168, 141, 197, 234,
                152, 186, 243, 83, 116, 22, 49, 85, 174, 172, 200, 91, 82, 77, 64, 159, 212, 52,
                176, 244, 163, 3, 71, 26, 208, 7, 203, 116, 175, 70, 241, 93, 21, 186, 169, 164,
                146, 54, 81, 52, 172, 22, 240, 34, 69, 46, 81, 72, 101, 224, 174, 156, 201, 235,
                225, 86, 1, 108, 140, 16, 74, 98, 155, 127, 30, 251, 200, 245, 237, 39, 120, 2,
                187, 34, 66, 143, 201, 193, 231, 229, 145, 21, 28, 10, 252, 195, 10, 49, 182, 141,
                29, 78, 105, 35, 153, 223, 75, 104, 204, 182, 125, 113, 0, 0, 0, 0,
            ],
            [
                110, 122, 177, 245, 90, 69, 146, 26, 145, 133, 25, 58, 88, 167, 119, 56, 97, 116,
                176, 133, 208, 27, 58, 66, 60, 200, 2, 230, 0, 168, 108, 14,
            ],
        ),
        _ => return None,
    };
    Some((kes_bytes, kes_verification_key))
}