1pub 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}