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))
}