mithril_common/test_utils/
precomputed_kes_key.rs

1/// If there is a need to update this data, we can run the `verify_kes_key_cache_content` test in `fixture_builder.rs`
2/// which generates the code of this function.
3pub fn cached_kes_key(kes_key_seed: &[u8]) -> Option<([u8; 612], [u8; 32])> {
4    let (kes_bytes, kes_verification_key) = match kes_key_seed {
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, 0] => {
6            (
7                [
8                    128, 187, 141, 128, 160, 231, 239, 110, 82, 252, 249, 34, 220, 14, 143, 165,
9                    242, 90, 4, 236, 214, 96, 227, 50, 71, 244, 188, 40, 141, 216, 137, 210, 206,
10                    165, 21, 189, 4, 148, 200, 150, 184, 216, 7, 97, 48, 185, 125, 24, 59, 246,
11                    162, 241, 133, 123, 210, 127, 22, 136, 236, 156, 255, 227, 65, 230, 167, 220,
12                    108, 71, 68, 38, 29, 177, 148, 78, 242, 26, 66, 29, 118, 13, 203, 222, 83, 4,
13                    3, 80, 150, 45, 238, 178, 82, 152, 207, 54, 128, 158, 100, 214, 191, 130, 126,
14                    80, 215, 9, 177, 40, 83, 223, 154, 116, 16, 89, 0, 185, 180, 127, 190, 162,
15                    190, 81, 111, 80, 137, 49, 49, 65, 9, 149, 218, 132, 101, 230, 222, 131, 28,
16                    186, 236, 85, 139, 144, 207, 0, 169, 229, 111, 154, 175, 219, 155, 161, 105,
17                    118, 221, 211, 205, 141, 175, 215, 241, 179, 92, 96, 106, 82, 88, 58, 93, 156,
18                    194, 30, 148, 255, 143, 74, 33, 242, 22, 74, 234, 10, 236, 188, 221, 100, 43,
19                    234, 253, 188, 105, 76, 163, 82, 240, 214, 189, 217, 49, 36, 51, 133, 156, 55,
20                    208, 173, 238, 2, 158, 79, 162, 173, 164, 157, 55, 118, 189, 23, 31, 103, 153,
21                    23, 41, 49, 80, 10, 178, 81, 52, 31, 215, 188, 64, 7, 98, 103, 180, 75, 31, 6,
22                    204, 146, 174, 33, 36, 156, 233, 196, 3, 68, 114, 226, 17, 9, 30, 52, 234, 86,
23                    11, 201, 206, 198, 244, 223, 131, 101, 79, 41, 215, 53, 121, 187, 193, 71, 50,
24                    105, 235, 89, 100, 80, 106, 43, 90, 173, 66, 24, 53, 76, 147, 190, 159, 104,
25                    91, 95, 230, 197, 204, 45, 46, 18, 238, 244, 116, 74, 202, 160, 71, 147, 236,
26                    181, 208, 129, 239, 132, 64, 30, 242, 196, 206, 237, 234, 213, 93, 35, 127,
27                    238, 129, 90, 58, 134, 38, 5, 8, 236, 78, 253, 213, 190, 39, 20, 131, 141, 93,
28                    41, 211, 45, 35, 88, 213, 37, 241, 68, 32, 81, 25, 248, 225, 211, 73, 242, 227,
29                    34, 175, 171, 42, 196, 152, 10, 107, 158, 162, 66, 229, 239, 224, 148, 197, 90,
30                    11, 174, 108, 228, 221, 10, 9, 158, 96, 231, 69, 86, 251, 145, 105, 34, 255,
31                    50, 230, 129, 248, 132, 228, 123, 24, 233, 185, 204, 144, 44, 11, 71, 9, 73,
32                    127, 149, 142, 99, 24, 7, 199, 255, 128, 84, 137, 24, 186, 142, 79, 83, 227,
33                    233, 12, 245, 7, 136, 48, 192, 186, 163, 62, 51, 28, 105, 62, 109, 27, 21, 191,
34                    140, 158, 202, 85, 231, 208, 66, 120, 135, 163, 22, 10, 173, 97, 154, 53, 156,
35                    156, 30, 247, 103, 171, 207, 17, 243, 168, 196, 132, 210, 39, 128, 98, 114,
36                    117, 49, 242, 215, 97, 129, 119, 90, 210, 168, 125, 124, 40, 235, 62, 149, 47,
37                    205, 119, 81, 239, 88, 74, 234, 185, 122, 232, 87, 207, 35, 98, 164, 46, 87,
38                    15, 215, 229, 255, 142, 152, 79, 220, 219, 176, 87, 167, 140, 199, 154, 105,
39                    227, 110, 134, 224, 70, 136, 28, 196, 49, 99, 97, 24, 48, 167, 156, 4, 240,
40                    242, 104, 125, 146, 246, 134, 129, 61, 146, 201, 205, 30, 41, 125, 29, 193,
41                    122, 54, 244, 102, 147, 200, 231, 102, 113, 190, 132, 89, 55, 26, 131, 251, 94,
42                    153, 224, 168, 137, 190, 18, 132, 119, 222, 14, 51, 34, 160, 215, 182, 254,
43                    235, 247, 201, 18, 151, 35, 215, 40, 102, 56, 151, 25, 229, 122, 0, 0, 0, 0,
44                ],
45                [
46                    230, 80, 215, 83, 21, 9, 187, 108, 255, 215, 153, 140, 40, 198, 142, 78, 200,
47                    250, 98, 26, 9, 82, 32, 110, 161, 30, 176, 63, 205, 125, 203, 41,
48                ],
49            )
50        }
51        [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] => {
52            (
53                [
54                    210, 93, 249, 195, 14, 165, 182, 98, 135, 235, 9, 62, 35, 186, 42, 18, 30, 110,
55                    58, 10, 118, 221, 21, 226, 247, 117, 252, 206, 2, 209, 41, 212, 36, 91, 172,
56                    163, 39, 33, 169, 243, 119, 30, 61, 249, 211, 182, 147, 125, 128, 82, 237, 1,
57                    150, 52, 93, 205, 51, 13, 222, 123, 176, 30, 183, 177, 26, 246, 109, 161, 160,
58                    99, 129, 84, 223, 59, 144, 76, 31, 153, 177, 114, 227, 190, 15, 107, 251, 66,
59                    12, 209, 130, 152, 223, 216, 2, 216, 99, 193, 187, 70, 56, 31, 8, 225, 222, 7,
60                    225, 44, 229, 119, 2, 111, 47, 70, 243, 250, 227, 139, 144, 122, 136, 1, 122,
61                    148, 90, 14, 4, 162, 238, 255, 132, 153, 107, 152, 59, 29, 54, 227, 110, 187,
62                    175, 133, 48, 88, 154, 133, 88, 140, 123, 250, 62, 129, 52, 147, 154, 53, 200,
63                    193, 134, 18, 219, 107, 44, 38, 111, 27, 122, 142, 111, 236, 34, 101, 21, 197,
64                    119, 33, 110, 50, 115, 215, 162, 252, 217, 108, 99, 115, 107, 15, 173, 246,
65                    214, 239, 47, 56, 127, 12, 175, 157, 26, 42, 23, 39, 175, 167, 248, 225, 91,
66                    243, 176, 99, 12, 58, 28, 80, 154, 139, 159, 138, 254, 147, 28, 234, 128, 80,
67                    79, 87, 181, 84, 53, 246, 130, 176, 139, 221, 15, 181, 70, 53, 138, 250, 6, 5,
68                    199, 87, 205, 200, 83, 198, 190, 33, 90, 0, 163, 220, 19, 126, 204, 208, 247,
69                    194, 163, 188, 253, 28, 53, 69, 176, 38, 238, 32, 92, 119, 113, 71, 24, 101,
70                    208, 181, 196, 52, 182, 117, 243, 150, 136, 44, 99, 211, 36, 52, 29, 31, 137,
71                    205, 112, 252, 140, 233, 85, 128, 96, 15, 108, 27, 25, 73, 83, 184, 11, 28, 86,
72                    186, 29, 161, 91, 210, 176, 109, 153, 127, 217, 99, 16, 247, 210, 177, 206,
73                    252, 67, 207, 174, 128, 206, 218, 245, 45, 228, 9, 65, 135, 32, 52, 148, 26,
74                    157, 250, 31, 249, 95, 237, 80, 16, 207, 56, 147, 161, 220, 177, 121, 11, 211,
75                    247, 224, 90, 254, 190, 52, 161, 87, 63, 116, 48, 78, 0, 162, 115, 227, 156,
76                    137, 53, 49, 141, 196, 195, 196, 48, 156, 191, 147, 80, 16, 127, 113, 90, 186,
77                    58, 215, 234, 143, 213, 113, 177, 35, 46, 194, 28, 125, 80, 150, 39, 63, 54,
78                    177, 137, 19, 71, 52, 186, 79, 98, 22, 10, 164, 18, 188, 205, 236, 160, 251,
79                    138, 239, 22, 220, 86, 243, 62, 29, 177, 132, 22, 182, 199, 118, 178, 217, 228,
80                    254, 221, 8, 230, 28, 209, 169, 114, 81, 232, 132, 230, 173, 4, 53, 64, 118,
81                    188, 49, 38, 112, 198, 52, 142, 120, 248, 128, 80, 239, 55, 126, 226, 42, 69,
82                    89, 24, 14, 49, 55, 103, 196, 161, 31, 202, 119, 53, 133, 181, 37, 172, 192,
83                    71, 57, 211, 101, 101, 220, 74, 198, 37, 202, 48, 5, 83, 197, 239, 249, 58,
84                    189, 3, 168, 225, 143, 44, 4, 38, 159, 36, 255, 2, 12, 240, 222, 239, 25, 206,
85                    25, 170, 58, 72, 181, 23, 0, 229, 5, 31, 119, 70, 162, 47, 146, 237, 26, 224,
86                    81, 41, 134, 252, 126, 29, 65, 182, 37, 24, 99, 35, 32, 103, 249, 76, 198, 150,
87                    69, 128, 4, 181, 183, 2, 101, 33, 209, 16, 158, 243, 185, 241, 138, 237, 172,
88                    106, 245, 249, 193, 251, 125, 35, 253, 221, 25, 65, 194, 148, 135, 196, 228,
89                    130, 112, 94, 194, 189, 249, 180, 173, 60, 0, 0, 0, 0,
90                ],
91                [
92                    220, 182, 153, 148, 26, 157, 158, 196, 1, 198, 147, 188, 177, 228, 236, 244,
93                    160, 40, 71, 39, 160, 100, 249, 10, 11, 185, 159, 166, 199, 118, 182, 139,
94                ],
95            )
96        }
97        [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] => {
98            (
99                [
100                    76, 77, 214, 152, 97, 253, 163, 35, 174, 150, 149, 11, 47, 60, 44, 69, 10, 101,
101                    166, 175, 20, 2, 3, 95, 214, 246, 83, 162, 246, 189, 177, 232, 252, 14, 69, 60,
102                    11, 249, 78, 244, 127, 233, 91, 197, 23, 10, 106, 137, 195, 89, 169, 172, 186,
103                    135, 225, 7, 149, 197, 25, 195, 200, 168, 47, 202, 164, 125, 238, 199, 38, 183,
104                    38, 14, 58, 50, 88, 5, 17, 6, 164, 131, 58, 46, 168, 131, 27, 216, 167, 122,
105                    143, 33, 170, 155, 225, 83, 189, 217, 32, 68, 144, 21, 177, 237, 121, 148, 11,
106                    194, 3, 92, 96, 50, 225, 112, 160, 254, 118, 120, 67, 188, 41, 232, 220, 49,
107                    100, 218, 67, 206, 173, 69, 42, 53, 63, 162, 92, 119, 253, 247, 117, 160, 104,
108                    255, 31, 153, 159, 255, 52, 84, 178, 232, 80, 214, 157, 114, 70, 226, 47, 51,
109                    184, 185, 31, 74, 141, 201, 140, 183, 199, 49, 152, 108, 120, 158, 87, 219,
110                    108, 81, 65, 168, 237, 207, 248, 119, 102, 55, 185, 50, 101, 0, 47, 151, 127,
111                    250, 86, 55, 60, 13, 137, 41, 92, 223, 0, 97, 205, 142, 74, 59, 167, 213, 254,
112                    140, 241, 115, 80, 152, 248, 216, 87, 92, 97, 5, 31, 8, 178, 238, 22, 112, 203,
113                    55, 13, 15, 112, 104, 113, 124, 165, 198, 78, 189, 88, 154, 120, 82, 86, 164,
114                    139, 178, 98, 28, 57, 150, 249, 7, 219, 121, 58, 115, 104, 175, 41, 85, 20,
115                    242, 214, 33, 39, 130, 93, 92, 0, 184, 198, 54, 135, 214, 60, 39, 216, 160,
116                    130, 88, 63, 27, 186, 209, 149, 68, 159, 19, 72, 167, 235, 84, 208, 176, 209,
117                    56, 208, 250, 27, 123, 254, 54, 118, 114, 173, 43, 26, 203, 26, 80, 159, 45,
118                    72, 29, 190, 195, 28, 52, 179, 187, 79, 93, 213, 195, 235, 221, 33, 233, 125,
119                    171, 170, 183, 253, 53, 202, 175, 6, 80, 119, 8, 190, 25, 48, 224, 105, 108,
120                    91, 97, 38, 80, 140, 114, 163, 70, 93, 128, 193, 203, 163, 149, 119, 63, 190,
121                    62, 7, 204, 75, 165, 124, 44, 154, 163, 244, 112, 88, 196, 152, 213, 18, 239,
122                    108, 74, 146, 93, 220, 33, 68, 62, 158, 65, 122, 9, 247, 199, 229, 119, 68,
123                    244, 220, 39, 190, 50, 28, 110, 244, 137, 134, 171, 228, 15, 143, 11, 45, 84,
124                    197, 109, 17, 154, 211, 177, 187, 38, 9, 66, 86, 207, 251, 208, 241, 41, 186,
125                    10, 87, 33, 237, 16, 150, 243, 127, 104, 17, 238, 76, 253, 5, 124, 123, 53, 51,
126                    55, 101, 52, 106, 239, 170, 87, 170, 225, 209, 113, 68, 65, 103, 228, 202, 89,
127                    29, 123, 210, 95, 176, 197, 74, 246, 163, 64, 238, 113, 228, 91, 2, 225, 227,
128                    71, 208, 151, 55, 113, 58, 231, 161, 170, 87, 247, 66, 109, 114, 249, 96, 106,
129                    190, 132, 173, 34, 132, 58, 132, 17, 162, 253, 32, 131, 138, 138, 227, 223, 34,
130                    103, 30, 187, 121, 172, 230, 39, 197, 220, 184, 82, 95, 199, 178, 53, 58, 174,
131                    136, 58, 188, 213, 29, 55, 8, 242, 164, 49, 177, 155, 217, 13, 144, 140, 156,
132                    32, 18, 133, 149, 220, 67, 81, 206, 72, 169, 217, 188, 239, 146, 239, 202, 85,
133                    13, 103, 186, 221, 195, 59, 49, 153, 176, 177, 116, 69, 43, 252, 142, 83, 119,
134                    105, 102, 207, 33, 48, 229, 183, 126, 126, 126, 180, 202, 57, 57, 211, 156, 40,
135                    145, 76, 72, 247, 26, 38, 109, 178, 0, 0, 0, 0,
136                ],
137                [
138                    221, 44, 88, 255, 31, 20, 114, 241, 109, 225, 1, 83, 142, 238, 60, 111, 228,
139                    32, 95, 25, 232, 148, 236, 63, 219, 153, 75, 178, 229, 197, 169, 124,
140                ],
141            )
142        }
143        [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] => {
144            (
145                [
146                    25, 238, 160, 109, 164, 222, 38, 150, 154, 217, 116, 63, 8, 54, 9, 78, 67, 96,
147                    44, 179, 128, 251, 217, 132, 234, 44, 157, 10, 96, 85, 79, 52, 153, 72, 116,
148                    12, 196, 70, 79, 141, 162, 193, 5, 59, 220, 225, 69, 24, 125, 7, 132, 226, 131,
149                    141, 225, 134, 179, 31, 77, 13, 125, 197, 43, 57, 175, 179, 11, 90, 218, 196,
150                    22, 220, 56, 73, 160, 75, 183, 57, 72, 170, 56, 210, 37, 1, 197, 132, 44, 114,
151                    70, 151, 28, 188, 180, 38, 90, 59, 132, 229, 115, 104, 63, 100, 84, 100, 19,
152                    17, 236, 121, 234, 229, 201, 164, 194, 219, 114, 255, 159, 231, 130, 216, 134,
153                    206, 86, 4, 153, 117, 248, 59, 115, 67, 224, 247, 138, 237, 195, 61, 130, 87,
154                    113, 0, 65, 97, 219, 88, 15, 228, 246, 106, 53, 6, 201, 92, 148, 15, 159, 249,
155                    184, 169, 99, 67, 101, 44, 159, 8, 154, 143, 162, 37, 196, 193, 72, 183, 23,
156                    127, 244, 53, 240, 243, 228, 53, 76, 45, 136, 137, 212, 9, 170, 116, 114, 85,
157                    170, 106, 198, 139, 225, 62, 226, 228, 133, 139, 250, 118, 118, 131, 50, 222,
158                    159, 82, 164, 185, 202, 206, 228, 101, 47, 72, 102, 136, 170, 170, 120, 57, 9,
159                    122, 248, 124, 216, 139, 138, 223, 2, 225, 227, 149, 165, 22, 138, 170, 99, 84,
160                    198, 3, 212, 17, 78, 232, 13, 228, 223, 106, 161, 218, 164, 248, 143, 233, 185,
161                    22, 48, 215, 194, 151, 17, 192, 10, 86, 54, 195, 237, 141, 139, 159, 30, 8,
162                    125, 172, 237, 83, 252, 42, 42, 240, 62, 219, 225, 27, 121, 75, 43, 240, 181,
163                    186, 95, 81, 79, 252, 133, 105, 52, 195, 201, 175, 64, 107, 175, 224, 223, 115,
164                    212, 93, 93, 78, 147, 67, 240, 243, 130, 7, 216, 253, 128, 197, 28, 25, 151, 5,
165                    252, 128, 41, 124, 252, 98, 201, 6, 223, 66, 5, 114, 230, 180, 21, 185, 147,
166                    178, 195, 195, 109, 212, 77, 33, 214, 35, 88, 87, 93, 82, 141, 214, 243, 227,
167                    167, 101, 133, 45, 92, 228, 246, 0, 96, 59, 36, 27, 128, 165, 201, 56, 58, 198,
168                    33, 110, 24, 226, 141, 235, 175, 129, 133, 57, 216, 249, 165, 172, 154, 234,
169                    190, 152, 231, 121, 173, 220, 91, 242, 59, 58, 229, 159, 106, 97, 55, 145, 251,
170                    128, 128, 241, 142, 42, 77, 227, 156, 28, 51, 176, 39, 19, 123, 103, 33, 34,
171                    168, 244, 37, 158, 228, 118, 20, 106, 140, 155, 169, 144, 227, 219, 214, 144,
172                    56, 100, 43, 85, 134, 173, 237, 232, 166, 188, 206, 254, 187, 195, 233, 163,
173                    231, 88, 205, 43, 223, 196, 9, 56, 167, 106, 105, 231, 216, 102, 88, 217, 191,
174                    152, 68, 154, 168, 19, 64, 127, 185, 39, 155, 147, 125, 70, 107, 164, 144, 51,
175                    120, 34, 18, 234, 239, 252, 49, 25, 87, 155, 200, 28, 94, 230, 179, 209, 71,
176                    167, 202, 76, 129, 83, 9, 104, 148, 204, 248, 13, 245, 100, 48, 106, 252, 119,
177                    112, 206, 94, 58, 250, 96, 58, 217, 126, 169, 39, 5, 201, 211, 107, 254, 1,
178                    253, 4, 226, 100, 96, 25, 35, 46, 132, 79, 252, 57, 93, 25, 14, 2, 210, 160,
179                    142, 70, 63, 100, 58, 28, 237, 221, 24, 191, 72, 8, 113, 20, 190, 27, 35, 47,
180                    254, 54, 12, 23, 85, 135, 105, 12, 127, 237, 132, 224, 22, 169, 216, 89, 76,
181                    199, 171, 82, 32, 237, 61, 138, 164, 149, 90, 0, 0, 0, 0,
182                ],
183                [
184                    187, 249, 4, 79, 86, 107, 53, 190, 106, 137, 217, 26, 173, 41, 155, 230, 240,
185                    88, 156, 248, 43, 46, 162, 131, 174, 252, 171, 241, 89, 244, 83, 49,
186                ],
187            )
188        }
189        [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] => {
190            (
191                [
192                    228, 185, 33, 133, 42, 222, 133, 221, 109, 99, 95, 16, 205, 50, 210, 113, 151,
193                    229, 239, 164, 160, 235, 185, 61, 51, 118, 11, 67, 65, 157, 79, 207, 126, 117,
194                    95, 68, 165, 114, 191, 138, 107, 49, 172, 68, 85, 11, 4, 242, 191, 15, 233,
195                    169, 148, 244, 173, 73, 139, 19, 175, 15, 47, 132, 86, 83, 239, 158, 166, 13,
196                    198, 75, 187, 165, 138, 133, 24, 57, 197, 171, 161, 76, 109, 149, 209, 109,
197                    178, 182, 78, 91, 197, 41, 119, 224, 65, 116, 158, 88, 224, 183, 232, 177, 110,
198                    120, 227, 98, 173, 147, 65, 240, 227, 228, 70, 11, 194, 102, 133, 60, 53, 165,
199                    116, 187, 150, 111, 77, 66, 156, 125, 4, 38, 125, 254, 121, 81, 241, 16, 71,
200                    172, 31, 252, 143, 75, 20, 210, 97, 154, 198, 112, 162, 26, 172, 191, 34, 224,
201                    58, 205, 132, 222, 7, 12, 231, 107, 138, 216, 38, 193, 215, 23, 198, 212, 8,
202                    232, 151, 222, 42, 183, 216, 94, 13, 109, 120, 43, 250, 11, 81, 98, 245, 200,
203                    167, 231, 253, 117, 73, 190, 16, 105, 52, 33, 156, 193, 78, 21, 2, 251, 45,
204                    127, 76, 212, 159, 153, 206, 221, 10, 96, 39, 86, 103, 60, 110, 114, 19, 132,
205                    33, 175, 243, 225, 206, 57, 129, 40, 152, 142, 47, 61, 152, 224, 9, 4, 222,
206                    154, 226, 168, 17, 105, 154, 80, 44, 119, 220, 40, 236, 100, 162, 120, 160, 76,
207                    177, 226, 188, 213, 169, 143, 89, 186, 254, 186, 89, 22, 196, 181, 36, 22, 176,
208                    89, 148, 101, 205, 33, 95, 66, 5, 173, 144, 242, 145, 246, 99, 225, 35, 31,
209                    117, 18, 114, 108, 86, 165, 180, 171, 6, 119, 246, 205, 192, 178, 16, 149, 77,
210                    248, 145, 187, 169, 147, 75, 64, 254, 109, 66, 216, 191, 189, 34, 56, 63, 225,
211                    126, 40, 10, 249, 168, 108, 180, 228, 230, 26, 226, 56, 18, 141, 51, 202, 200,
212                    25, 209, 87, 37, 39, 122, 254, 224, 223, 20, 211, 135, 67, 57, 101, 0, 240,
213                    235, 92, 246, 132, 35, 107, 94, 155, 208, 211, 128, 246, 99, 124, 174, 143,
214                    164, 148, 137, 229, 225, 115, 165, 250, 136, 75, 156, 102, 98, 200, 170, 180,
215                    105, 190, 95, 232, 15, 142, 228, 53, 44, 67, 63, 184, 123, 37, 69, 125, 47,
216                    111, 45, 29, 157, 32, 118, 56, 193, 40, 124, 160, 79, 47, 202, 136, 233, 180,
217                    94, 242, 90, 186, 183, 84, 135, 80, 43, 172, 161, 54, 127, 81, 246, 31, 170,
218                    47, 69, 45, 113, 234, 158, 83, 79, 26, 196, 202, 20, 88, 5, 112, 43, 64, 151,
219                    23, 88, 85, 205, 56, 238, 32, 62, 19, 8, 203, 254, 10, 4, 134, 20, 54, 218, 10,
220                    101, 23, 119, 168, 97, 118, 104, 20, 222, 26, 80, 237, 129, 254, 151, 12, 25,
221                    220, 123, 15, 191, 109, 166, 117, 183, 107, 147, 87, 230, 215, 235, 112, 115,
222                    47, 174, 196, 143, 91, 191, 179, 166, 134, 246, 118, 13, 200, 225, 174, 203,
223                    120, 58, 64, 145, 40, 247, 37, 56, 183, 249, 149, 53, 213, 179, 55, 241, 221,
224                    47, 65, 251, 51, 40, 83, 199, 62, 216, 86, 185, 240, 33, 124, 140, 101, 210,
225                    254, 167, 29, 88, 243, 153, 143, 135, 31, 225, 18, 232, 18, 53, 29, 227, 13,
226                    115, 125, 122, 171, 209, 75, 205, 23, 82, 180, 20, 39, 220, 11, 9, 193, 113,
227                    146, 119, 5, 38, 2, 102, 50, 224, 199, 195, 93, 117, 40, 125, 246, 0, 0, 0, 0,
228                ],
229                [
230                    228, 233, 42, 103, 141, 57, 76, 25, 145, 41, 160, 159, 45, 46, 210, 29, 56, 66,
231                    225, 90, 143, 193, 113, 93, 52, 179, 200, 240, 102, 83, 173, 184,
232                ],
233            )
234        }
235        [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] => {
236            (
237                [
238                    209, 107, 167, 55, 10, 147, 210, 134, 52, 184, 0, 89, 80, 242, 88, 183, 228,
239                    254, 176, 180, 236, 167, 121, 176, 1, 50, 94, 247, 32, 106, 165, 65, 171, 71,
240                    210, 164, 121, 209, 201, 202, 123, 6, 143, 170, 29, 182, 191, 98, 245, 37, 103,
241                    99, 131, 141, 201, 54, 218, 119, 192, 103, 234, 192, 180, 193, 135, 169, 218,
242                    240, 228, 104, 100, 226, 140, 89, 248, 7, 250, 235, 228, 100, 107, 8, 82, 252,
243                    247, 186, 104, 234, 237, 50, 40, 22, 31, 182, 139, 84, 9, 43, 151, 12, 90, 248,
244                    124, 17, 239, 103, 205, 119, 172, 151, 149, 216, 230, 189, 124, 104, 168, 30,
245                    18, 57, 190, 47, 104, 40, 121, 26, 126, 205, 134, 145, 191, 228, 100, 45, 108,
246                    21, 195, 161, 157, 59, 140, 146, 101, 16, 210, 214, 14, 156, 177, 132, 123,
247                    112, 224, 228, 57, 130, 123, 99, 122, 200, 230, 54, 2, 204, 85, 44, 73, 149,
248                    150, 53, 15, 40, 26, 243, 227, 225, 82, 38, 151, 223, 142, 151, 247, 233, 112,
249                    1, 208, 131, 127, 94, 35, 116, 161, 189, 68, 124, 234, 109, 208, 31, 177, 198,
250                    19, 186, 156, 112, 206, 107, 183, 23, 107, 60, 161, 167, 65, 112, 252, 46, 224,
251                    179, 60, 54, 55, 215, 30, 158, 222, 65, 106, 194, 221, 66, 221, 131, 240, 193,
252                    70, 174, 26, 51, 16, 9, 101, 134, 121, 28, 64, 6, 70, 208, 247, 75, 180, 178,
253                    168, 167, 124, 5, 49, 48, 41, 196, 250, 50, 115, 108, 16, 8, 34, 155, 65, 75,
254                    121, 140, 191, 29, 152, 205, 187, 76, 113, 11, 181, 64, 217, 52, 17, 39, 181,
255                    35, 54, 105, 166, 248, 37, 132, 141, 29, 4, 196, 62, 164, 186, 135, 222, 14,
256                    63, 209, 3, 39, 171, 23, 159, 181, 77, 4, 124, 183, 20, 221, 120, 107, 218,
257                    218, 112, 136, 219, 1, 147, 191, 60, 196, 20, 232, 65, 195, 21, 189, 249, 104,
258                    22, 107, 104, 106, 49, 156, 132, 175, 151, 22, 166, 250, 117, 141, 198, 218,
259                    170, 138, 143, 246, 37, 182, 123, 232, 27, 47, 58, 36, 1, 217, 137, 30, 93,
260                    223, 225, 16, 94, 133, 60, 150, 132, 118, 86, 37, 155, 206, 139, 69, 191, 68,
261                    55, 80, 90, 56, 49, 75, 77, 90, 112, 249, 8, 164, 122, 85, 120, 87, 252, 126,
262                    178, 21, 214, 222, 191, 147, 79, 133, 192, 2, 131, 140, 164, 121, 218, 203,
263                    255, 183, 248, 154, 183, 232, 217, 11, 208, 90, 125, 100, 87, 155, 86, 39, 91,
264                    12, 191, 137, 170, 23, 30, 90, 142, 129, 6, 250, 31, 211, 77, 6, 36, 248, 247,
265                    226, 1, 161, 59, 142, 205, 59, 191, 245, 155, 219, 192, 180, 249, 61, 44, 155,
266                    213, 188, 126, 164, 165, 162, 227, 74, 104, 42, 49, 231, 144, 42, 129, 142,
267                    143, 68, 3, 114, 89, 84, 1, 191, 203, 56, 32, 36, 61, 84, 104, 192, 95, 145,
268                    118, 8, 162, 105, 1, 64, 115, 234, 194, 92, 175, 15, 86, 142, 154, 239, 39, 21,
269                    45, 109, 110, 223, 106, 235, 66, 145, 225, 136, 139, 213, 188, 127, 11, 213,
270                    18, 97, 111, 189, 227, 223, 170, 66, 0, 103, 51, 85, 136, 61, 29, 47, 238, 246,
271                    72, 118, 80, 181, 175, 104, 210, 247, 4, 79, 59, 250, 25, 127, 81, 89, 226, 71,
272                    52, 25, 88, 65, 83, 248, 95, 113, 10, 148, 58, 36, 42, 247, 168, 252, 18, 107,
273                    110, 249, 143, 163, 184, 149, 135, 117, 147, 22, 0, 0, 0, 0,
274                ],
275                [
276                    82, 168, 182, 80, 236, 4, 194, 123, 240, 190, 4, 252, 216, 206, 73, 217, 54,
277                    113, 3, 123, 189, 152, 59, 20, 156, 171, 23, 48, 17, 133, 142, 94,
278                ],
279            )
280        }
281        [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] => {
282            (
283                [
284                    18, 99, 90, 253, 190, 227, 177, 127, 57, 101, 196, 15, 247, 136, 94, 213, 101,
285                    62, 239, 159, 103, 190, 84, 235, 107, 118, 68, 143, 91, 160, 91, 64, 217, 129,
286                    23, 5, 230, 199, 30, 170, 166, 11, 254, 212, 107, 238, 25, 113, 223, 36, 76,
287                    135, 134, 21, 13, 44, 89, 219, 157, 5, 132, 117, 42, 162, 151, 28, 187, 89,
288                    244, 38, 40, 71, 104, 139, 98, 34, 82, 160, 221, 0, 110, 30, 40, 137, 125, 68,
289                    7, 214, 132, 160, 195, 1, 122, 110, 116, 244, 189, 17, 233, 142, 122, 149, 0,
290                    239, 216, 61, 104, 174, 194, 236, 9, 50, 173, 186, 175, 139, 69, 66, 132, 20,
291                    78, 181, 197, 233, 30, 61, 174, 238, 46, 26, 18, 73, 228, 94, 186, 109, 110,
292                    218, 195, 220, 249, 165, 127, 93, 77, 220, 228, 64, 72, 234, 210, 99, 111, 169,
293                    135, 221, 22, 85, 62, 247, 203, 122, 59, 237, 158, 69, 34, 85, 211, 130, 179,
294                    71, 65, 194, 48, 12, 83, 0, 36, 21, 189, 142, 33, 220, 233, 82, 128, 76, 92,
295                    101, 132, 122, 112, 234, 62, 214, 81, 114, 205, 245, 127, 59, 148, 158, 27, 52,
296                    106, 170, 240, 117, 136, 243, 114, 78, 213, 116, 141, 57, 216, 78, 60, 70, 151,
297                    207, 229, 82, 125, 28, 137, 120, 175, 118, 194, 169, 7, 114, 10, 175, 174, 219,
298                    168, 151, 135, 108, 69, 69, 220, 30, 39, 52, 90, 123, 207, 232, 185, 182, 161,
299                    30, 86, 122, 5, 35, 149, 210, 119, 85, 122, 23, 141, 145, 78, 137, 174, 105,
300                    51, 24, 173, 236, 70, 221, 14, 135, 80, 119, 144, 60, 28, 166, 52, 243, 144,
301                    159, 192, 218, 107, 159, 68, 56, 103, 31, 130, 82, 31, 103, 29, 133, 122, 21,
302                    20, 3, 87, 183, 251, 192, 97, 49, 208, 100, 230, 170, 235, 245, 213, 89, 68,
303                    221, 113, 240, 191, 250, 98, 26, 252, 34, 175, 161, 171, 113, 97, 141, 56, 176,
304                    234, 74, 165, 173, 154, 106, 16, 232, 169, 92, 195, 47, 181, 16, 132, 140, 102,
305                    220, 226, 139, 101, 119, 237, 97, 9, 206, 10, 195, 178, 87, 26, 102, 9, 29,
306                    227, 63, 74, 240, 246, 33, 111, 42, 0, 78, 61, 226, 65, 32, 27, 61, 219, 168,
307                    33, 134, 64, 33, 64, 152, 203, 164, 115, 126, 178, 0, 21, 137, 109, 103, 89,
308                    230, 18, 46, 157, 94, 195, 14, 77, 86, 233, 86, 35, 245, 168, 111, 160, 203,
309                    156, 201, 13, 9, 95, 135, 56, 77, 103, 161, 76, 186, 227, 7, 147, 131, 57, 229,
310                    87, 251, 165, 195, 24, 113, 223, 63, 240, 27, 96, 89, 150, 122, 223, 160, 133,
311                    25, 128, 245, 111, 206, 53, 231, 0, 145, 167, 143, 232, 34, 29, 216, 21, 192,
312                    30, 169, 73, 146, 138, 214, 55, 111, 42, 87, 238, 45, 61, 228, 32, 41, 43, 128,
313                    120, 1, 135, 177, 204, 134, 174, 95, 147, 42, 128, 61, 228, 219, 254, 158, 20,
314                    29, 168, 246, 58, 43, 62, 227, 60, 157, 90, 196, 163, 249, 34, 157, 40, 35,
315                    188, 4, 9, 9, 113, 114, 204, 226, 221, 165, 66, 70, 229, 126, 42, 93, 38, 9,
316                    122, 73, 248, 62, 172, 255, 123, 23, 137, 123, 116, 44, 188, 206, 44, 116, 189,
317                    188, 13, 214, 179, 163, 44, 31, 141, 46, 234, 22, 87, 46, 121, 118, 34, 80, 24,
318                    6, 114, 20, 166, 29, 79, 110, 137, 248, 136, 97, 25, 19, 84, 58, 212, 189, 62,
319                    28, 142, 171, 112, 233, 0, 0, 0, 0,
320                ],
321                [
322                    142, 207, 162, 102, 170, 11, 206, 116, 39, 103, 20, 69, 126, 75, 198, 106, 53,
323                    119, 13, 100, 221, 100, 218, 124, 113, 218, 144, 194, 180, 197, 20, 60,
324                ],
325            )
326        }
327        [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] => {
328            (
329                [
330                    128, 119, 139, 98, 88, 169, 77, 1, 195, 80, 102, 60, 183, 246, 219, 214, 249,
331                    46, 75, 243, 48, 32, 3, 67, 8, 70, 103, 140, 110, 55, 121, 97, 114, 16, 152,
332                    85, 225, 72, 58, 87, 0, 155, 119, 136, 77, 225, 106, 99, 27, 88, 114, 237, 148,
333                    220, 124, 80, 228, 250, 133, 6, 86, 182, 244, 137, 84, 245, 224, 239, 7, 2,
334                    180, 3, 163, 117, 161, 102, 90, 233, 242, 70, 101, 159, 210, 86, 4, 200, 67,
335                    70, 67, 51, 218, 195, 37, 49, 130, 219, 71, 166, 58, 188, 210, 12, 252, 245,
336                    75, 127, 83, 145, 215, 213, 137, 29, 165, 38, 172, 180, 115, 60, 75, 233, 113,
337                    117, 219, 176, 36, 164, 239, 20, 52, 170, 62, 84, 6, 26, 155, 44, 36, 124, 150,
338                    172, 185, 69, 9, 72, 102, 160, 18, 14, 239, 169, 147, 228, 35, 180, 197, 52,
339                    254, 211, 148, 189, 63, 159, 39, 234, 131, 109, 253, 27, 183, 156, 140, 119,
340                    113, 55, 60, 22, 97, 169, 13, 244, 43, 212, 130, 65, 51, 43, 80, 30, 19, 59,
341                    18, 221, 125, 110, 46, 200, 17, 68, 15, 48, 105, 89, 131, 108, 73, 115, 254,
342                    171, 212, 59, 4, 70, 79, 171, 147, 8, 188, 189, 216, 145, 60, 181, 249, 226,
343                    87, 93, 187, 57, 118, 252, 170, 237, 47, 80, 150, 63, 244, 9, 148, 12, 32, 249,
344                    13, 53, 104, 95, 183, 195, 33, 215, 125, 122, 118, 50, 84, 58, 60, 205, 93,
345                    212, 78, 197, 190, 88, 104, 193, 160, 205, 119, 33, 139, 141, 163, 248, 199,
346                    145, 98, 85, 154, 226, 46, 241, 10, 107, 56, 181, 210, 155, 216, 154, 19, 105,
347                    238, 194, 234, 70, 213, 18, 96, 137, 82, 177, 173, 3, 175, 3, 57, 111, 243, 10,
348                    53, 49, 28, 140, 51, 122, 16, 104, 161, 188, 62, 204, 89, 149, 99, 254, 12, 2,
349                    211, 149, 223, 204, 235, 22, 99, 83, 121, 24, 169, 65, 214, 165, 217, 100, 165,
350                    26, 119, 239, 128, 24, 184, 250, 59, 17, 238, 35, 39, 41, 229, 147, 113, 11,
351                    166, 205, 245, 2, 222, 147, 151, 242, 237, 252, 0, 151, 131, 245, 152, 116, 39,
352                    70, 210, 125, 82, 139, 81, 234, 122, 41, 246, 131, 74, 74, 37, 195, 192, 75,
353                    84, 29, 213, 35, 25, 57, 141, 166, 153, 254, 116, 28, 224, 136, 133, 28, 249,
354                    164, 64, 20, 216, 142, 152, 19, 228, 228, 56, 146, 2, 76, 222, 27, 192, 223,
355                    223, 66, 232, 168, 142, 4, 17, 119, 39, 14, 62, 25, 251, 200, 210, 131, 206,
356                    50, 178, 135, 109, 54, 175, 210, 50, 202, 137, 247, 255, 76, 32, 31, 33, 109,
357                    96, 224, 70, 196, 227, 109, 45, 30, 227, 65, 170, 83, 179, 131, 39, 177, 71,
358                    85, 3, 101, 160, 110, 69, 253, 71, 146, 165, 203, 93, 209, 159, 9, 252, 146,
359                    79, 157, 73, 67, 101, 46, 172, 47, 220, 140, 139, 51, 221, 232, 131, 143, 77,
360                    0, 235, 152, 118, 104, 245, 8, 89, 67, 140, 219, 7, 32, 25, 240, 141, 133, 193,
361                    183, 4, 70, 19, 211, 234, 11, 189, 35, 99, 208, 243, 127, 13, 240, 129, 230,
362                    111, 41, 143, 28, 96, 132, 151, 98, 141, 172, 11, 63, 218, 88, 119, 164, 117,
363                    60, 91, 10, 129, 37, 139, 130, 131, 1, 187, 127, 23, 141, 192, 99, 239, 196,
364                    196, 103, 129, 61, 78, 134, 209, 35, 97, 76, 95, 242, 156, 31, 165, 234, 60,
365                    28, 124, 242, 165, 50, 208, 167, 0, 0, 0, 0,
366                ],
367                [
368                    152, 88, 235, 194, 80, 172, 172, 33, 230, 44, 141, 167, 215, 240, 95, 248, 194,
369                    136, 250, 239, 163, 86, 51, 45, 147, 68, 47, 247, 55, 82, 111, 176,
370                ],
371            )
372        }
373        [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] => {
374            (
375                [
376                    182, 109, 140, 211, 64, 96, 122, 219, 197, 151, 29, 193, 30, 68, 92, 212, 87,
377                    28, 53, 102, 129, 178, 95, 32, 31, 254, 180, 15, 98, 23, 26, 127, 152, 174,
378                    204, 217, 28, 54, 138, 211, 97, 35, 110, 214, 151, 138, 215, 116, 214, 16, 201,
379                    98, 197, 166, 10, 106, 12, 74, 16, 171, 131, 184, 127, 179, 62, 248, 99, 147,
380                    189, 111, 247, 107, 232, 89, 46, 195, 141, 238, 114, 55, 206, 223, 158, 154,
381                    97, 69, 135, 244, 99, 93, 223, 91, 144, 96, 78, 33, 109, 55, 216, 247, 109,
382                    183, 82, 3, 102, 131, 159, 77, 250, 108, 53, 214, 239, 227, 138, 204, 145, 28,
383                    255, 45, 241, 155, 0, 147, 129, 129, 155, 29, 25, 247, 13, 103, 89, 95, 95,
384                    117, 230, 0, 217, 38, 184, 122, 247, 87, 95, 183, 197, 213, 250, 234, 153, 237,
385                    92, 201, 176, 150, 108, 252, 253, 74, 230, 66, 82, 90, 56, 105, 100, 150, 73,
386                    164, 20, 186, 118, 79, 93, 234, 98, 50, 4, 160, 155, 234, 211, 140, 227, 86,
387                    97, 65, 96, 235, 10, 174, 149, 239, 17, 154, 209, 243, 39, 105, 218, 86, 229,
388                    191, 9, 76, 185, 14, 11, 96, 89, 227, 254, 242, 71, 155, 196, 161, 89, 39, 154,
389                    229, 234, 88, 48, 9, 189, 199, 83, 135, 126, 164, 247, 176, 253, 132, 234, 33,
390                    93, 9, 68, 153, 93, 56, 216, 87, 182, 194, 182, 48, 67, 146, 137, 23, 209, 86,
391                    5, 156, 8, 30, 108, 139, 171, 150, 41, 165, 204, 148, 251, 249, 201, 248, 100,
392                    33, 129, 124, 82, 171, 125, 169, 45, 3, 156, 93, 255, 99, 60, 232, 32, 47, 133,
393                    65, 163, 227, 25, 165, 131, 141, 48, 23, 103, 114, 250, 126, 222, 71, 244, 59,
394                    201, 93, 170, 91, 47, 15, 11, 139, 94, 108, 162, 234, 186, 141, 140, 33, 165,
395                    228, 124, 15, 25, 65, 99, 162, 33, 118, 129, 116, 252, 203, 62, 226, 115, 208,
396                    255, 63, 35, 162, 226, 169, 39, 172, 170, 167, 110, 150, 216, 178, 234, 98,
397                    230, 124, 160, 83, 116, 25, 82, 79, 84, 224, 11, 244, 158, 86, 250, 158, 83,
398                    124, 211, 18, 209, 205, 220, 11, 1, 226, 92, 243, 70, 119, 162, 132, 154, 160,
399                    16, 106, 100, 59, 163, 232, 7, 166, 164, 62, 17, 214, 108, 178, 190, 109, 6,
400                    17, 128, 76, 37, 88, 219, 253, 1, 13, 79, 18, 181, 218, 171, 54, 205, 112, 14,
401                    101, 99, 85, 99, 121, 110, 185, 132, 130, 111, 128, 222, 200, 134, 213, 163,
402                    146, 135, 196, 136, 214, 189, 252, 61, 102, 108, 213, 97, 144, 205, 70, 244,
403                    186, 191, 119, 219, 19, 30, 95, 198, 71, 248, 9, 119, 145, 220, 240, 44, 150,
404                    223, 15, 43, 169, 199, 106, 201, 51, 198, 252, 158, 38, 47, 95, 79, 20, 221,
405                    215, 96, 131, 191, 109, 18, 119, 197, 114, 124, 132, 23, 128, 241, 98, 249, 88,
406                    167, 187, 88, 56, 162, 16, 174, 124, 218, 3, 175, 252, 126, 50, 55, 192, 244,
407                    42, 6, 161, 249, 150, 41, 210, 209, 210, 157, 234, 219, 255, 142, 164, 26, 181,
408                    16, 90, 233, 6, 242, 27, 215, 123, 153, 109, 150, 209, 179, 142, 246, 136, 128,
409                    151, 159, 3, 154, 25, 197, 11, 8, 176, 138, 83, 27, 33, 225, 95, 39, 113, 116,
410                    180, 22, 134, 150, 85, 82, 33, 218, 9, 27, 33, 55, 35, 197, 11, 202, 176, 32,
411                    57, 16, 79, 55, 175, 107, 16, 40, 38, 196, 207, 0, 0, 0, 0,
412                ],
413                [
414                    123, 153, 8, 242, 239, 71, 28, 37, 104, 48, 48, 126, 183, 158, 163, 245, 101,
415                    161, 14, 163, 245, 185, 219, 11, 103, 118, 58, 145, 162, 56, 41, 94,
416                ],
417            )
418        }
419        [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] => {
420            (
421                [
422                    63, 95, 47, 36, 206, 31, 213, 108, 221, 175, 130, 240, 101, 114, 25, 135, 38,
423                    151, 158, 255, 133, 47, 96, 169, 204, 61, 167, 196, 154, 233, 159, 87, 158, 8,
424                    19, 145, 177, 60, 26, 4, 9, 90, 211, 121, 17, 145, 71, 111, 183, 193, 240, 157,
425                    175, 28, 33, 100, 232, 31, 4, 152, 139, 172, 98, 90, 36, 255, 194, 163, 81,
426                    134, 50, 136, 140, 110, 106, 163, 212, 166, 63, 94, 53, 127, 158, 12, 11, 138,
427                    234, 106, 90, 89, 224, 13, 7, 86, 55, 113, 140, 155, 64, 235, 53, 39, 128, 68,
428                    171, 111, 254, 33, 233, 67, 83, 234, 101, 16, 173, 68, 20, 77, 38, 48, 169,
429                    136, 248, 171, 147, 102, 134, 150, 64, 27, 23, 137, 193, 16, 120, 18, 236, 253,
430                    250, 91, 113, 194, 48, 26, 231, 233, 112, 186, 237, 66, 249, 52, 100, 117, 54,
431                    189, 185, 24, 222, 249, 114, 129, 188, 73, 23, 186, 25, 185, 231, 134, 216,
432                    220, 220, 162, 147, 131, 31, 196, 79, 81, 155, 147, 174, 207, 163, 31, 244, 85,
433                    71, 88, 193, 11, 61, 194, 232, 63, 74, 21, 243, 216, 70, 159, 59, 11, 99, 25,
434                    60, 127, 75, 203, 165, 56, 127, 155, 221, 154, 96, 209, 23, 64, 49, 207, 111,
435                    154, 194, 184, 85, 48, 24, 169, 68, 61, 239, 41, 195, 100, 139, 184, 175, 181,
436                    109, 61, 124, 214, 82, 4, 99, 171, 180, 101, 78, 131, 84, 74, 164, 225, 0, 14,
437                    115, 131, 233, 124, 69, 61, 54, 25, 50, 251, 15, 184, 187, 141, 222, 201, 97,
438                    167, 113, 47, 94, 117, 164, 207, 155, 101, 247, 46, 24, 60, 199, 144, 196, 209,
439                    253, 159, 1, 192, 159, 97, 32, 8, 147, 157, 216, 54, 123, 35, 74, 244, 26, 138,
440                    27, 153, 5, 89, 112, 243, 169, 21, 68, 99, 44, 179, 205, 161, 90, 220, 12, 141,
441                    37, 234, 63, 159, 247, 62, 225, 183, 212, 207, 199, 176, 90, 8, 187, 162, 124,
442                    118, 100, 132, 60, 34, 220, 226, 214, 95, 134, 59, 13, 182, 175, 213, 82, 25,
443                    95, 251, 109, 249, 188, 69, 137, 131, 202, 171, 23, 214, 26, 173, 144, 170,
444                    222, 204, 14, 109, 141, 19, 216, 165, 244, 212, 129, 243, 70, 219, 221, 82, 44,
445                    7, 82, 197, 185, 19, 18, 68, 168, 228, 93, 67, 89, 184, 156, 88, 18, 35, 238,
446                    243, 44, 124, 224, 104, 9, 226, 184, 36, 27, 246, 152, 34, 109, 17, 236, 33,
447                    64, 51, 196, 247, 88, 32, 119, 241, 75, 110, 133, 126, 118, 77, 10, 87, 179,
448                    214, 97, 160, 87, 144, 82, 170, 30, 43, 155, 167, 35, 98, 250, 69, 187, 236,
449                    227, 230, 98, 0, 1, 252, 121, 245, 69, 52, 222, 191, 81, 227, 62, 94, 55, 209,
450                    128, 116, 150, 60, 88, 173, 5, 15, 223, 47, 156, 220, 127, 121, 48, 184, 189,
451                    192, 28, 250, 168, 141, 197, 234, 152, 186, 243, 83, 116, 22, 49, 85, 174, 172,
452                    200, 91, 82, 77, 64, 159, 212, 52, 176, 244, 163, 3, 71, 26, 208, 7, 203, 116,
453                    175, 70, 241, 93, 21, 186, 169, 164, 146, 54, 81, 52, 172, 22, 240, 34, 69, 46,
454                    81, 72, 101, 224, 174, 156, 201, 235, 225, 86, 1, 108, 140, 16, 74, 98, 155,
455                    127, 30, 251, 200, 245, 237, 39, 120, 2, 187, 34, 66, 143, 201, 193, 231, 229,
456                    145, 21, 28, 10, 252, 195, 10, 49, 182, 141, 29, 78, 105, 35, 153, 223, 75,
457                    104, 204, 182, 125, 113, 0, 0, 0, 0,
458                ],
459                [
460                    110, 122, 177, 245, 90, 69, 146, 26, 145, 133, 25, 58, 88, 167, 119, 56, 97,
461                    116, 176, 133, 208, 27, 58, 66, 60, 200, 2, 230, 0, 168, 108, 14,
462                ],
463            )
464        }
465        _ => return None,
466    };
467    Some((kes_bytes, kes_verification_key))
468}