streebog.bend

bend-osdev-hashes@0.1.0.0 · 852 lines · 62 definitions

1# Streebog (GOST R 34.11-2012; RFC 6986, V. Dolmatov and A. Degtyarev,
2# "GOST R 34.11-2012: Hash Function", 2013): 256- and 512-bit digests of
3# 64-byte blocks. The compression function (section 8)
4#   g_N(h, m) = E(LPS(h xor N), m) xor h xor m,
5#   E(K, m) = X[K_13] LPS X[K_12] ... LPS X[K_1](m), K_1 = K,
6#   K_(i+1) = LPS(K_i xor C_i),
7# where N counts the bits hashed so far; the hash (section 9) feeds the
8# message 512 bits at a time, keeping N and the sum Sigma of the blocks
9# modulo 2^512, then pads the last (short, possibly empty) block with a 1
10# bit and zeros, and finishes with g_0(h, N) and g_0(h, Sigma). Streebog-256
11# starts from h = (00000001)^64 and keeps the most significant 256 bits.
12#
13# Byte order: RFC 6986 writes a 512-bit vector a_63 || ... || a_0; byte i of
14# a 64-byte string in memory is a_i (its examples print messages and digests
15# most significant byte first, the reverse of memory order). A 512-bit
16# vector here is an Hs.HsW16 of sixteen 32-bit words, least significant
17# first (word i holds bytes 4i .. 4i+3, little-endian), and a digest is the
18# bytes in memory order: a_0 first. The 512-bit sums use 32-bit words with
19# carries.
20#
21# LPS runs on eight tables of 64-bit entries (each T_j[b] = l(Pi(b) << 8j);
22# gen/streebog.py writes them from RFC 6986's Pi', tau and A, and checks
23# them against S, P and L applied one after the other). The tables are part
24# of the chaining value (built once by init), so a lookup is a walk down a
25# tree of depth 8.
26#
27# The hashes, as the crypto package's hash interface takes them:
28#   ~Hs.HsMdState<HsStbCv>, ~64n, ~32n, ~HsStreebog.init256(),
29#   ~HsStreebog.update, ~HsStreebog.final256, ~HsStreebog.digest256
30#   ~Hs.HsMdState<HsStbCv>, ~64n, ~64n, ~HsStreebog.init512(),
31#   ~HsStreebog.update, ~HsStreebog.final512, ~HsStreebog.digest512
32import Base
33import bend-osdev-bytes@0.1.0.0/bytes.bend as B
34import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
35
36# A table of 256 64-bit entries, as a tree on the index's bits (opaque)
37type HsStbTab is Data:
38  HsStbLeaf{v: Hs.HsW2}
39  HsStbNode{l: HsStbTab, r: HsStbTab}
40
41# The eight LPS tables (opaque)
42type HsStbTabs is Data:
43  HsStbTabs{t0: HsStbTab, t1: HsStbTab, t2: HsStbTab, t3: HsStbTab, t4: HsStbTab, t5: HsStbTab, t6: HsStbTab, t7: HsStbTab}
44
45# The chaining value (opaque): h, N, Sigma, and the tables
46type HsStbCv is Data:
47  HsStbCv{h: Hs.HsW16, n: Hs.HsW16, s: Hs.HsW16, t: HsStbTabs}
48
49def hs.stb.leaves(xs: List<&2, Hs.HsW2>) -> List<&2, HsStbTab>:
50  match xs:
51    case Nil{}:
52      Nil{}
53    case Con{h, t}:
54      Con{HsStbLeaf{h}, hs.stb.leaves(t)}
55
56def hs.stb.pairs(ts: List<&2, HsStbTab>) -> List<&2, HsStbTab>:
57  match ts:
58    case Con{a, Con{b, t}}:
59      Con{HsStbNode{a, b}, hs.stb.pairs(t)}
60    case _:
61      Nil{}
62
63def hs.stb.up(n: Nat, ts: List<&2, HsStbTab>) -> List<&2, HsStbTab>:
64  match n:
65    case 0n:
66      ts
67    case 1n+p:
68      hs.stb.up(p, hs.stb.pairs(ts))
69
70def hs.stb.root(ts: List<&2, HsStbTab>) -> HsStbTab:
71  match ts:
72    case Nil{}:
73      HsStbLeaf{Hs.HsW2{0, 0}}
74    case Con{h, t}:
75      h
76
77# the table of 256 entries (entry i is element i)
78def hs.stb.tab(xs: List<&2, Hs.HsW2>) -> HsStbTab:
79  hs.stb.root(hs.stb.up(8n, hs.stb.leaves(xs)))
80
81def hs.stb.pick(one: Bool, l: HsStbTab, r: HsStbTab) -> HsStbTab:
82  match one:
83    case True{}:
84      r
85    case False{}:
86      l
87
88def hs.stb.get.go(d: Nat, t: HsStbTab, +i: U32) -> Hs.HsW2:
89  match d:
90    case 0n:
91      match t:
92        case HsStbLeaf{v}:
93          v
94        case HsStbNode{l, r}:
95          Hs.HsW2{0, 0}
96    case 1n+(+p):
97      match t:
98        case HsStbLeaf{v}:
99          v
100        case HsStbNode{l, r}:
101          hs.stb.get.go(p, hs.stb.pick(U32.is_eq(U32.and(1, U32.shrn(i, p)), 1), l, r), i)
102
103# entry i (a byte) of a table
104def hs.stb.get(t: HsStbTab, +i: U32) -> Hs.HsW2:
105  hs.stb.get.go(8n, t, i)
106
107# the XOR of eight 64-bit values
108def hs.stb.x8(e0: Hs.HsW2, e1: Hs.HsW2, e2: Hs.HsW2, e3: Hs.HsW2, e4: Hs.HsW2, e5: Hs.HsW2, e6: Hs.HsW2, e7: Hs.HsW2) -> Hs.HsW2:
109  match e0 e1 e2 e3 e4 e5 e6 e7:
110    case Hs.HsW2{a0, b0} Hs.HsW2{a1, b1} Hs.HsW2{a2, b2} Hs.HsW2{a3, b3} Hs.HsW2{a4, b4} Hs.HsW2{a5, b5} Hs.HsW2{a6, b6} Hs.HsW2{a7, b7}:
111      Hs.HsW2{U32.xor(U32.xor(U32.xor(a0, a1), U32.xor(a2, a3)), U32.xor(U32.xor(a4, a5), U32.xor(a6, a7))), U32.xor(U32.xor(U32.xor(b0, b1), U32.xor(b2, b3)), U32.xor(U32.xor(b4, b5), U32.xor(b6, b7)))}
112
113# eight 64-bit chunks as a 512-bit vector, chunk 0 the least significant
114def hs.stb.join(o0: Hs.HsW2, o1: Hs.HsW2, o2: Hs.HsW2, o3: Hs.HsW2, o4: Hs.HsW2, o5: Hs.HsW2, o6: Hs.HsW2, o7: Hs.HsW2) -> Hs.HsW16:
115  match o0 o1 o2 o3 o4 o5 o6 o7:
116    case Hs.HsW2{a0, a1} Hs.HsW2{a2, a3} Hs.HsW2{a4, a5} Hs.HsW2{a6, a7} Hs.HsW2{a8, a9} Hs.HsW2{a10, a11} Hs.HsW2{a12, a13} Hs.HsW2{a14, a15}:
117      Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}
118
119# BEGIN GENERATED by gen/streebog.py: tables
120# T_0[b] = l(Pi(b) << 0): each entry's low and high 32 bits
121def hs.stb.t0.list() -> List<&2, Hs.HsW2>:
122  [Hs.HsW2{1551825126, 3491721563}, Hs.HsW2{2155316005, 385491977}, Hs.HsW2{2128628168, 2829332101}, Hs.HsW2{2709931611, 1791035023},
123    Hs.HsW2{2733191691, 1849785303}, Hs.HsW2{2755123883, 1717338471}, Hs.HsW2{2828408822, 1986422810}, Hs.HsW2{1879825653, 1268093283},
124    Hs.HsW2{2381537864, 4048283319}, Hs.HsW2{2590137599, 3313876328}, Hs.HsW2{2793243339, 2505562108}, Hs.HsW2{2943210342, 2314254697},
125    Hs.HsW2{1956604981, 2961390920}, Hs.HsW2{2985081980, 2711194659}, Hs.HsW2{2885855030, 2372977713}, Hs.HsW2{3500717726, 3604986927},
126    Hs.HsW2{1375345035, 934196197}, Hs.HsW2{1085656988, 192746122}, Hs.HsW2{3044543676, 1519329288}, Hs.HsW2{2229482469, 3991701538},
127    Hs.HsW2{3553084110, 3529490807}, Hs.HsW2{3054991596, 1578065232}, Hs.HsW2{3233959097, 495400579}, Hs.HsW2{3026002060, 2902723531},
128    Hs.HsW2{1535458422, 797548584}, Hs.HsW2{2031848792, 1462960118}, Hs.HsW2{2666982463, 1049825603}, Hs.HsW2{2681454607, 3373808256},
129    Hs.HsW2{638190062, 2209215477}, Hs.HsW2{4108906256, 2792954177}, Hs.HsW2{211930461, 272296317}, Hs.HsW2{502143818, 753485842},
130    Hs.HsW2{3690118995, 963871777}, Hs.HsW2{3473733044, 155034278}, Hs.HsW2{2629612639, 3449309144}, Hs.HsW2{2335017704, 4183170055},
131    Hs.HsW2{1769043839, 2624222554}, Hs.HsW2{1898901701, 3156130464}, Hs.HsW2{2885247910, 1927681346}, Hs.HsW2{580825390, 2025545694},
132    Hs.HsW2{265206029, 347771941}, Hs.HsW2{1661883010, 2219665047}, Hs.HsW2{1780351791, 2565474306}, Hs.HsW2{1143045980, 4033592993},
133    Hs.HsW2{483080058, 3680658385}, Hs.HsW2{730783875, 1679569227}, Hs.HsW2{2605150415, 839816875}, Hs.HsW2{2259250053, 518512313},
134    Hs.HsW2{2274117557, 3916232058}, Hs.HsW2{2286091960, 4258685279}, Hs.HsW2{1442962715, 3359138454}, Hs.HsW2{2455183714, 782891070},
135    Hs.HsW2{1124046844, 4168500241}, Hs.HsW2{137723293, 3945547094}, Hs.HsW2{2965999692, 1444063200}, Hs.HsW2{760219683, 1812057083},
136    Hs.HsW2{4194531885, 1162389159}, Hs.HsW2{948662004, 2881799871}, Hs.HsW2{4260937405, 3135141844}, Hs.HsW2{3947670586, 2040203208},
137    Hs.HsW2{95526128, 211650536}, Hs.HsW2{275446311, 3411577516}, Hs.HsW2{3253166217, 3926662464}, Hs.HsW2{511799066, 677983562},
138    Hs.HsW2{133940368, 4288074099}, Hs.HsW2{790253635, 2668272992}, Hs.HsW2{3759580663, 2520203206}, Hs.HsW2{3014059036, 1385355960},
139    Hs.HsW2{745874451, 2609569848}, Hs.HsW2{1935976613, 1326836795}, Hs.HsW2{1462038827, 1068714325}, Hs.HsW2{366700247, 3351579972},
140    Hs.HsW2{3816411559, 2461483678}, Hs.HsW2{437641178, 3548354913}, Hs.HsW2{1580507270, 588523456}, Hs.HsW2{2068960568, 2755242349},
141    Hs.HsW2{2012223589, 3020111888}, Hs.HsW2{2417850626, 3718426277}, Hs.HsW2{2305282696, 173886108}, Hs.HsW2{3748007827, 3261409290},
142    Hs.HsW2{550824270, 2343569733}, Hs.HsW2{2436388146, 707364198}, Hs.HsW2{3204917569, 1118319557}, Hs.HsW2{1647017650, 1942375764},
143    Hs.HsW2{1157911404, 132158818}, Hs.HsW2{3909547098, 2324713811}, Hs.HsW2{1799040799, 1868637121}, Hs.HsW2{3691609027, 3336918354},
144    Hs.HsW2{869361465, 1147731633}, Hs.HsW2{3342436393, 3792824304}, Hs.HsW2{4152859456, 2734253081}, Hs.HsW2{3282909417, 419908571},
145    Hs.HsW2{1196296972, 4109091833}, Hs.HsW2{1993684053, 1133013971}, Hs.HsW2{1520439366, 3624045547}, Hs.HsW2{4123902752, 1374827138},
146    Hs.HsW2{226812269, 3887186622}, Hs.HsW2{115271840, 136182448}, Hs.HsW2{1414235515, 993211405}, Hs.HsW2{1738203714, 2136722108},
147    Hs.HsW2{2315822808, 249378756}, Hs.HsW2{2847095750, 2179810265}, Hs.HsW2{3175969057, 2980275550}, Hs.HsW2{3891093863, 1772220085},
148    Hs.HsW2{3371643172, 4138431445}, Hs.HsW2{2244354005, 442999777}, Hs.HsW2{3560703582, 768151556}, Hs.HsW2{2411280936, 37793836},
149    Hs.HsW2{1824582543, 2432168626}, Hs.HsW2{290444823, 1020502383}, Hs.HsW2{4049171424, 2867109545}, Hs.HsW2{2362855032, 113298804},
150    Hs.HsW2{3575196270, 3661773767}, Hs.HsW2{380899975, 3276107804}, Hs.HsW2{3833730359, 1830917101}, Hs.HsW2{1100014508, 4243994953},
151    Hs.HsW2{569492862, 2084250246}, Hs.HsW2{76853440, 4212567083}, Hs.HsW2{927324153, 3212726938}, Hs.HsW2{775912563, 1753331363},
152    Hs.HsW2{3652773683, 3396915898}, Hs.HsW2{875209641, 3153997762}, Hs.HsW2{3429073380, 230547454}, Hs.HsW2{608197006, 1889969518},
153    Hs.HsW2{1274005073, 3838913156}, Hs.HsW2{1708177954, 2354093095}, Hs.HsW2{3263698137, 4002177048}, Hs.HsW2{1235590705, 400194591},
154    Hs.HsW2{685872339, 1620855827}, Hs.HsW2{854870793, 3018052978}, Hs.HsW2{2769483419, 2446830244}, Hs.HsW2{1138408396, 268267474},
155    Hs.HsW2{1008721460, 1355967124}, Hs.HsW2{1750358863, 1809931929}, Hs.HsW2{1873780703, 2490863594}, Hs.HsW2{1491748902, 722066800},
156    Hs.HsW2{1843775423, 1736235377}, Hs.HsW2{4289914589, 1238704463}, Hs.HsW2{1181427516, 56682554}, Hs.HsW2{1333491345, 533169839},
157    Hs.HsW2{2017370472, 2696533045}, Hs.HsW2{1594985654, 3567193091}, Hs.HsW2{3385990420, 18896918}, Hs.HsW2{2106539416, 2888061917},
158    Hs.HsW2{1064348260, 1414666188}, Hs.HsW2{2492058050, 649331342}, Hs.HsW2{3598081598, 3737274015}, Hs.HsW2{57635920, 75529560},
159    Hs.HsW2{2185091909, 3857805970}, Hs.HsW2{38426720, 4077606555}, Hs.HsW2{2807607035, 1658649663}, Hs.HsW2{1314806433, 3897339244},
160    Hs.HsW2{1433315659, 3434618830}, Hs.HsW2{2054486280, 1404207790}, Hs.HsW2{1276379841, 457702391}, Hs.HsW2{2552759455, 915336179},
161    Hs.HsW2{2905049862, 2063331314}, Hs.HsW2{4271360749, 3193834124}, Hs.HsW2{319131255, 3487102964}, Hs.HsW2{19213360, 4153093059},
162    Hs.HsW2{4242379405, 1297439767}, Hs.HsW2{2143643128, 1596917062}, Hs.HsW2{456193002, 620016290}, Hs.HsW2{3971442858, 2249053883},
163    Hs.HsW2{890212249, 1282737153}, Hs.HsW2{0, 0}, Hs.HsW2{1295068913, 3972845620}, Hs.HsW2{3189900657, 3038976006},
164    Hs.HsW2{2567776431, 3238379568}, Hs.HsW2{3797745047, 1698457949}, Hs.HsW2{3323765785, 362466355}, Hs.HsW2{1916896405, 3097413624},
165    Hs.HsW2{3073529052, 2844030611}, Hs.HsW2{985740948, 1489997860}, Hs.HsW2{4078119808, 1508886578}, Hs.HsW2{967721668, 1548742012},
166    Hs.HsW2{4023917818, 2190322659}, Hs.HsW2{2511136242, 3510577485}, Hs.HsW2{3894663274, 2098952848}, Hs.HsW2{4165542477, 3057905724},
167    Hs.HsW2{3634219779, 1039399289}, Hs.HsW2{657403358, 1948702774}, Hs.HsW2{530858794, 3756138121}, Hs.HsW2{2644088943, 974351387},
168    Hs.HsW2{3443961300, 4197905469}, Hs.HsW2{1356805563, 3223689254}, Hs.HsW2{2866565014, 2238529153}, Hs.HsW2{1404060139, 3299206526},
169    Hs.HsW2{1975140357, 1191712395}, Hs.HsW2{1004804772, 2940517351}, Hs.HsW2{700758243, 2534893520}, Hs.HsW2{3147012481, 3116277742},
170    Hs.HsW2{3515718318, 559192044}, Hs.HsW2{3710670835, 829324945}, Hs.HsW2{3671561059, 3472404450}, Hs.HsW2{304128583, 945019959},
171    Hs.HsW2{3728941987, 904790985}, Hs.HsW2{3294035065, 3868301992}, Hs.HsW2{1216393729, 3763427292}, Hs.HsW2{1693816338, 2077997028},
172    Hs.HsW2{2199451509, 310008145}, Hs.HsW2{1385524699, 858705597}, Hs.HsW2{599498014, 2402317341}, Hs.HsW2{2473725266, 3642938365},
173    Hs.HsW2{1631849186, 2001088524}, Hs.HsW2{3538087678, 634710708}, Hs.HsW2{4009570506, 1963360288}, Hs.HsW2{1254812257, 324665671},
174    Hs.HsW2{352209639, 810428039}, Hs.HsW2{2994980908, 2769940859}, Hs.HsW2{1506763798, 3699570355}, Hs.HsW2{2091520424, 1538226206},
175    Hs.HsW2{4213593629, 2999160164}, Hs.HsW2{395394743, 885939167}, Hs.HsW2{4034682832, 1567602026}, Hs.HsW2{176104957, 405214157},
176    Hs.HsW2{3871886679, 2653603190}, Hs.HsW2{3852941575, 2594879534}, Hs.HsW2{1045792340, 2748922895}, Hs.HsW2{2924019542, 2122027690},
177    Hs.HsW2{627406270, 2267909805}, Hs.HsW2{4184608381, 1103682559}, Hs.HsW2{2748063291, 2580172820}, Hs.HsW2{817763177, 1088979945},
178    Hs.HsW2{152064429, 480734869}, Hs.HsW2{3132536241, 1312142381}, Hs.HsW2{3401410884, 94381390}, Hs.HsW2{2169679637, 3782283210},
179    Hs.HsW2{3415754100, 4062908045}, Hs.HsW2{832257881, 3076761642}, Hs.HsW2{1854583791, 1677501481}, Hs.HsW2{2695064171, 2638884172},
180    Hs.HsW2{250320189, 3811688422}, Hs.HsW2{2529399202, 3586085909}, Hs.HsW2{2392593944, 4123761647}, Hs.HsW2{3160956177, 1177046685},
181    Hs.HsW2{408913850, 544526330}, Hs.HsW2{3103583697, 3175015094}, Hs.HsW2{4063627184, 2925847537}, Hs.HsW2{3458849156, 4273375589},
182    Hs.HsW2{4137858928, 1433554906}, Hs.HsW2{3612570126, 692677980}, Hs.HsW2{1027273220, 2807644503}, Hs.HsW2{3932782602, 2383424523},
183    Hs.HsW2{3312701513, 286962027}, Hs.HsW2{427469706, 3623871545}, Hs.HsW2{190450125, 4021041166}, Hs.HsW2{912325577, 1224046937},
184    Hs.HsW2{2548481426, 573865942}, Hs.HsW2{3778251207, 1639715845}, Hs.HsW2{3118055905, 1253427573}, Hs.HsW2{1616979666, 2160925647},
185    Hs.HsW2{3985786010, 1904672120}, Hs.HsW2{715902131, 2476153480}, Hs.HsW2{1723846258, 2295390591}, Hs.HsW2{1566299350, 664033944}]
186
187# T_1[b] = l(Pi(b) << 8): each entry's low and high 32 bits
188def hs.stb.t1.list() -> List<&2, Hs.HsW2>:
189  [Hs.HsW2{94900680, 3730128780}, Hs.HsW2{833942885, 419870102}, Hs.HsW2{2979418103, 1131311318}, Hs.HsW2{2334039429, 919815115},
190    Hs.HsW2{2240457562, 2218654412}, Hs.HsW2{2579482617, 4261189058}, Hs.HsW2{2715099042, 258165726}, Hs.HsW2{1995420621, 1833274171},
191    Hs.HsW2{4166598528, 2244212604}, Hs.HsW2{3195239602, 1016148319}, Hs.HsW2{1722606488, 558411827}, Hs.HsW2{1281843647, 418953254},
192    Hs.HsW2{2513042191, 3358638532}, Hs.HsW2{545693866, 2551870992}, Hs.HsW2{1123243872, 2853568801}, Hs.HsW2{209075446, 902583302},
193    Hs.HsW2{3427130157, 1116765542}, Hs.HsW2{2522543292, 2181289035}, Hs.HsW2{3282102376, 1030700271}, Hs.HsW2{3532832167, 3161718633},
194    Hs.HsW2{48368169, 2267213057}, Hs.HsW2{3442794167, 2407630312}, Hs.HsW2{2817393113, 2600821213}, Hs.HsW2{841480918, 1396023321},
195    Hs.HsW2{3894046677, 3385773172}, Hs.HsW2{1545875946, 1425376046}, Hs.HsW2{1565865072, 2581887904}, Hs.HsW2{2899453646, 4156483414},
196    Hs.HsW2{1461196541, 944637349}, Hs.HsW2{2759659114, 3510006866}, Hs.HsW2{946526299, 4070563356}, Hs.HsW2{1651898314, 839677745},
197    Hs.HsW2{3652098736, 3502799330}, Hs.HsW2{2433806173, 3681814214}, Hs.HsW2{2722500625, 1162894929}, Hs.HsW2{3832304419, 4228028530},
198    Hs.HsW2{4156296389, 4198282997}, Hs.HsW2{2271781235, 52369357}, Hs.HsW2{2940283261, 3180196569}, Hs.HsW2{3023986239, 2637909850},
199    Hs.HsW2{922676868, 1081173787}, Hs.HsW2{3554916413, 1902249959}, Hs.HsW2{4180163098, 1221726194}, Hs.HsW2{1971108990, 662085300},
200    Hs.HsW2{2482169204, 1549200327}, Hs.HsW2{2666912792, 2760591183}, Hs.HsW2{1341419020, 1389079977}, Hs.HsW2{763468230, 1623710360},
201    Hs.HsW2{3691416440, 245188206}, Hs.HsW2{3942147580, 1324097909}, Hs.HsW2{569877808, 1426820766}, Hs.HsW2{1698688043, 1803265468},
202    Hs.HsW2{1766445277, 1589113274}, Hs.HsW2{3679228057, 1474991331}, Hs.HsW2{3506549268, 4131449574}, Hs.HsW2{2193666235, 3712624705},
203    Hs.HsW2{1661268560, 4280127423}, Hs.HsW2{1006229480, 3098332051}, Hs.HsW2{2394328141, 3901127751}, Hs.HsW2{958127553, 1066280594},
204    Hs.HsW2{312564348, 3408909833}, Hs.HsW2{2878881071, 2932422107}, Hs.HsW2{1449726823, 4116708651}, Hs.HsW2{1826734357, 2162347574},
205    Hs.HsW2{3987897885, 396096504}, Hs.HsW2{2111018202, 33426864}, Hs.HsW2{3972234119, 3666479990}, Hs.HsW2{3751118027, 1152275425},
206    Hs.HsW2{1934074373, 3004216503}, Hs.HsW2{2021360914, 3752538684}, Hs.HsW2{3497047950, 995168872}, Hs.HsW2{3107546963, 1709630418},
207    Hs.HsW2{3797372248, 1751429745}, Hs.HsW2{2412218839, 630686921}, Hs.HsW2{4206572969, 48306813}, Hs.HsW2{2738296203, 2286003935},
208    Hs.HsW2{2606616016, 2061400259}, Hs.HsW2{2586626122, 3083829325}, Hs.HsW2{461338434, 548846979}, Hs.HsW2{982045298, 1975333661},
209    Hs.HsW2{1261271646, 1099917995}, Hs.HsW2{1806424820, 3650428091}, Hs.HsW2{3892272272, 3056700925}, Hs.HsW2{577022595, 523803409},
210    Hs.HsW2{2231086784, 1227620930}, Hs.HsW2{3322476960, 3812229987}, Hs.HsW2{145696932, 646484740}, Hs.HsW2{874308781, 3344140826},
211    Hs.HsW2{3995169198, 1571350135}, Hs.HsW2{1247576004, 2359202341}, Hs.HsW2{2867411125, 1675152725}, Hs.HsW2{2843358982, 703322330},
212    Hs.HsW2{2078837409, 2509776819}, Hs.HsW2{1792728942, 344253493}, Hs.HsW2{429751659, 2811515010}, Hs.HsW2{1442454740, 3211585700},
213    Hs.HsW2{3387804389, 2630173418}, Hs.HsW2{473263267, 2042720014}, Hs.HsW2{3739517265, 2311039855}, Hs.HsW2{818278655, 3558296856},
214    Hs.HsW2{367739293, 2455241860}, Hs.HsW2{1347554588, 1631180584}, Hs.HsW2{418150641, 1787144204}, Hs.HsW2{24184218, 3440507022},
215    Hs.HsW2{2091028800, 3438277950}, Hs.HsW2{588623641, 3525927839}, Hs.HsW2{4015027252, 2428051193}, Hs.HsW2{122297313, 1501024909},
216    Hs.HsW2{3843905209, 823353596}, Hs.HsW2{1511993233, 3230902573}, Hs.HsW2{3067892758, 437887579}, Hs.HsW2{165555518, 3952700298},
217    Hs.HsW2{517432970, 4276322831}, Hs.HsW2{3081589132, 3607648981}, Hs.HsW2{266679109, 2147434889}, Hs.HsW2{1742595586, 3965274301},
218    Hs.HsW2{3131730144, 802551389}, Hs.HsW2{3810937026, 2775927551}, Hs.HsW2{218577260, 4175277192}, Hs.HsW2{2354349668, 1873056070},
219    Hs.HsW2{649969361, 209476627}, Hs.HsW2{59969459, 1244861839}, Hs.HsW2{2676283778, 1771749313}, Hs.HsW2{2819306140, 3841597524},
220    Hs.HsW2{1132614394, 1728575919}, Hs.HsW2{3486962846, 144926953}, Hs.HsW2{1492985272, 1202799660}, Hs.HsW2{3163649691, 3149126750},
221    Hs.HsW2{2422336199, 375782984}, Hs.HsW2{530998032, 871529089}, Hs.HsW2{1748555079, 2477132084}, Hs.HsW2{2563687011, 820866380},
222    Hs.HsW2{3638533930, 500793708}, Hs.HsW2{104537723, 2489723395}, Hs.HsW2{3951648870, 2214451707}, Hs.HsW2{3868088586, 2065724787},
223    Hs.HsW2{345654279, 1598684170}, Hs.HsW2{1906681900, 875714998}, Hs.HsW2{2322569247, 4223843141}, Hs.HsW2{2695109176, 3262296912},
224    Hs.HsW2{2913149780, 984555480}, Hs.HsW2{188491543, 1824229003}, Hs.HsW2{2368046078, 2729798088}, Hs.HsW2{3204610344, 4051749329},
225    Hs.HsW2{3595282933, 2939631723}, Hs.HsW2{2030731400, 314231474}, Hs.HsW2{272846933, 1275935496}, Hs.HsW2{244594399, 3001989383},
226    Hs.HsW2{3467104516, 3316813927}, Hs.HsW2{4279444577, 3702793713}, Hs.HsW2{2536239398, 1326591173}, Hs.HsW2{1361250438, 2888314790},
227    Hs.HsW2{795055087, 3890558873}, Hs.HsW2{1387267893, 3860544041}, Hs.HsW2{2922392807, 1889274455}, Hs.HsW2{1096833235, 3760526510},
228    Hs.HsW2{3010741726, 3293355479}, Hs.HsW2{2149759634, 1516815680}, Hs.HsW2{2769030128, 472354012}, Hs.HsW2{4052161214, 1851432182},
229    Hs.HsW2{2133958387, 2262622385}, Hs.HsW2{1074879817, 758443040}, Hs.HsW2{2118163305, 1271732287}, Hs.HsW2{3567887324, 672519530},
230    Hs.HsW2{4061404429, 610896249}, Hs.HsW2{0, 0}, Hs.HsW2{1605844569, 516331169}, Hs.HsW2{376983086, 3630895371},
231    Hs.HsW2{2967947885, 2390722648}, Hs.HsW2{332423142, 104738439}, Hs.HsW2{3151719802, 3804499667}, Hs.HsW2{2315032492, 2985406154},
232    Hs.HsW2{1018416137, 3789232414}, Hs.HsW2{3303732105, 1679355490}, Hs.HsW2{1238331511, 3333261226}, Hs.HsW2{3397305686, 3606468453},
233    Hs.HsW2{3661468931, 2600168557}, Hs.HsW2{2290979382, 2095076932}, Hs.HsW2{932178718, 2371919765}, Hs.HsW2{2618807857, 598321742},
234    Hs.HsW2{3610946671, 1646706917}, Hs.HsW2{2795439171, 1444190547}, Hs.HsW2{2640761771, 4005057216}, Hs.HsW2{1405158063, 722125479},
235    Hs.HsW2{1845742396, 130032439}, Hs.HsW2{1036175763, 751493520}, Hs.HsW2{1590049731, 3554111023}, Hs.HsW2{861339468, 2653182103},
236    Hs.HsW2{1682893233, 2791988530}, Hs.HsW2{896393527, 172126868}, Hs.HsW2{1642526841, 2017419966}, Hs.HsW2{81335378, 323274498},
237    Hs.HsW2{4260441672, 1536608496}, Hs.HsW2{3315332627, 2835945196}, Hs.HsW2{673810446, 3197297940}, Hs.HsW2{1418402126, 1920798762},
238    Hs.HsW2{3406807244, 468168683}, Hs.HsW2{1153976603, 1047538466}, Hs.HsW2{1293313061, 3588833448}, Hs.HsW2{1045546528, 1727656991},
239    Hs.HsW2{1059111866, 2884111505}, Hs.HsW2{3268537842, 4034839649}, Hs.HsW2{1169771649, 4083274668}, Hs.HsW2{2495151765, 86063434},
240    Hs.HsW2{753966172, 2916491798}, Hs.HsW2{4083488919, 3916984823}, Hs.HsW2{733644733, 4104253595}, Hs.HsW2{2986688580, 157115737},
241    Hs.HsW2{1220441581, 196902692}, Hs.HsW2{772970101, 720686871}, Hs.HsW2{386485172, 360376709}, Hs.HsW2{1317366678, 2681885991},
242    Hs.HsW2{2458116334, 2437354313}, Hs.HsW2{1177174834, 3109209635}, Hs.HsW2{1197164200, 1950564013}, Hs.HsW2{610252024, 2338238738},
243    Hs.HsW2{4042659620, 2739627128}, Hs.HsW2{4267844091, 296082815}, Hs.HsW2{667728715, 3245188253}, Hs.HsW2{3185603329, 1990337744},
244    Hs.HsW2{1502355490, 2325789858}, Hs.HsW2{1838204047, 1307784888}, Hs.HsW2{1947056612, 3932644922}, Hs.HsW2{3769976689, 4014366576},
245    Hs.HsW2{717980199, 967837717}, Hs.HsW2{4116580076, 2099141620}, Hs.HsW2{2209461537, 274452687}, Hs.HsW2{3224627163, 2002528608},
246    Hs.HsW2{1916184479, 2114014265}, Hs.HsW2{288511439, 2166145926}, Hs.HsW2{437154520, 3987162381}, Hs.HsW2{2056884027, 1485430589},
247    Hs.HsW2{3346660410, 774634477}, Hs.HsW2{2249827561, 3457085251}, Hs.HsW2{4140632415, 925716091}, Hs.HsW2{3916130895, 81736954},
248    Hs.HsW2{1892986294, 4179861816}, Hs.HsW2{172827277, 2712305157}, Hs.HsW2{3091751625, 2834766684}, Hs.HsW2{1620573667, 3039730224},
249    Hs.HsW2{1533946379, 226644387}, Hs.HsW2{3787735787, 576169982}, Hs.HsW2{693669268, 1937972634}, Hs.HsW2{3365719935, 1372895844},
250    Hs.HsW2{3041876901, 1344976852}, Hs.HsW2{2169749256, 2541305294}, Hs.HsW2{3587745350, 3842256356}, Hs.HsW2{4236258258, 2525442174},
251    Hs.HsW2{2006890071, 2689889205}, Hs.HsW2{491022649, 3033569152}, Hs.HsW2{4224331827, 3488670451}, Hs.HsW2{3715600098, 3280781024},
252    Hs.HsW2{623817058, 1179601308}, Hs.HsW2{1869794982, 3402750905}, Hs.HsW2{3242385985, 3125662190}, Hs.HsW2{4096721782, 2953814906}]
253
254# T_2[b] = l(Pi(b) << 16): each entry's low and high 32 bits
255def hs.stb.t2.list() -> List<&2, Hs.HsW2>:
256  [Hs.HsW2{2842210885, 3437546810}, Hs.HsW2{3893067695, 144528516}, Hs.HsW2{3008660228, 1669482177}, Hs.HsW2{3258274962, 3539865288},
257    Hs.HsW2{4063710958, 2818301823}, Hs.HsW2{2452847126, 1307664396}, Hs.HsW2{1379603195, 2229601258}, Hs.HsW2{1403718730, 126925821},
258    Hs.HsW2{955706013, 428505103}, Hs.HsW2{1441548491, 716377231}, Hs.HsW2{2999229877, 3774349014}, Hs.HsW2{583719900, 3068982260},
259    Hs.HsW2{324591377, 1084004948}, Hs.HsW2{3755884515, 3553528406}, Hs.HsW2{315146656, 3286835779}, Hs.HsW2{2171315463, 225311320},
260    Hs.HsW2{2039818103, 3723747761}, Hs.HsW2{1955312089, 79702594}, Hs.HsW2{2670587064, 2495785983}, Hs.HsW2{2834869492, 1334932781},
261    Hs.HsW2{2976497531, 2020092911}, Hs.HsW2{2939156164, 3787946568}, Hs.HsW2{2625687158, 207453894}, Hs.HsW2{2413302119, 1287775378},
262    Hs.HsW2{3650714466, 4276960548}, Hs.HsW2{3282389539, 1368110815}, Hs.HsW2{354392976, 1841245478}, Hs.HsW2{99247695, 3049022027},
263    Hs.HsW2{1523573274, 3899304530}, Hs.HsW2{4216561854, 1208078032}, Hs.HsW2{3221776621, 3373556710}, Hs.HsW2{3440836163, 271034389},
264    Hs.HsW2{831653069, 4134562208}, Hs.HsW2{1821031655, 2957823127}, Hs.HsW2{904428595, 3233395708}, Hs.HsW2{1492311653, 4085303164},
265    Hs.HsW2{3729662290, 1354445377}, Hs.HsW2{1130295701, 3751015568}, Hs.HsW2{1647904903, 4058042973}, Hs.HsW2{440152385, 2942733307},
266    Hs.HsW2{4027216529, 3155276369}, Hs.HsW2{2118286663, 1940254420}, Hs.HsW2{3997973294, 633267190}, Hs.HsW2{880304770, 1137445867},
267    Hs.HsW2{3722642332, 3357861752}, Hs.HsW2{2318563112, 4185753305}, Hs.HsW2{1159312660, 4071637986}, Hs.HsW2{2282703703, 3801607159},
268    Hs.HsW2{2566567560, 982819994}, Hs.HsW2{1760609305, 2256869067}, Hs.HsW2{157609552, 4026143151}, Hs.HsW2{3575116669, 2762690240},
269    Hs.HsW2{1417434746, 2848371864}, Hs.HsW2{2163981238, 2383954511}, Hs.HsW2{3475751484, 198034747}, Hs.HsW2{3929424848, 326580650},
270    Hs.HsW2{464269296, 739455980}, Hs.HsW2{2816149029, 2370360304}, Hs.HsW2{1801316055, 505070578}, Hs.HsW2{380811614, 4112578591},
271    Hs.HsW2{1342582404, 2668588740}, Hs.HsW2{501967729, 19956894}, Hs.HsW2{2356491177, 3562942891}, Hs.HsW2{4246004799, 1696758178},
272    Hs.HsW2{1894893863, 839512094}, Hs.HsW2{3401688179, 3195119472}, Hs.HsW2{2789939348, 238906343}, Hs.HsW2{4280932416, 2127041676},
273    Hs.HsW2{4207132175, 3413407431}, Hs.HsW2{1672025654, 1922394698}, Hs.HsW2{428938127, 939089602}, Hs.HsW2{1307395573, 2654988890},
274    Hs.HsW2{2521367272, 2067315280}, Hs.HsW2{3186046820, 573462539}, Hs.HsW2{2308920806, 1642222560}, Hs.HsW2{3813846400, 4237109253},
275    Hs.HsW2{593151341, 899238883}, Hs.HsW2{4125103326, 162385946}, Hs.HsW2{2013608390, 1585863078}, Hs.HsW2{1902237590, 2977712137},
276    Hs.HsW2{986437346, 39851297}, Hs.HsW2{3843418369, 3517882231}, Hs.HsW2{1059172525, 3084679018}, Hs.HsW2{1857519768, 2879824313},
277    Hs.HsW2{613261149, 2614051974}, Hs.HsW2{910515965, 1478911685}, Hs.HsW2{4273587953, 4257066139}, Hs.HsW2{1097059818, 3296303550},
278    Hs.HsW2{388147183, 1985298440}, Hs.HsW2{3966830417, 1045728984}, Hs.HsW2{3411131074, 1023680359}, Hs.HsW2{2894255114, 2035855217},
279    Hs.HsW2{75135230, 919198300}, Hs.HsW2{867121330, 3986293902}, Hs.HsW2{3379332797, 653161033}, Hs.HsW2{3953548641, 2416083389},
280    Hs.HsW2{3506279730, 286731403}, Hs.HsW2{1610888440, 3926572915}, Hs.HsW2{697502195, 1123848053}, Hs.HsW2{1051831836, 883543933},
281    Hs.HsW2{1208427450, 730040337}, Hs.HsW2{1120857892, 1558596743}, Hs.HsW2{534140686, 450554288}, Hs.HsW2{3602567603, 1010080761},
282    Hs.HsW2{477853120, 2185575561}, Hs.HsW2{3087880491, 2542942784}, Hs.HsW2{3247994460, 1247927281}, Hs.HsW2{402722110, 3029133013},
283    Hs.HsW2{2387087318, 3484703877}, Hs.HsW2{220108462, 3644050419}, Hs.HsW2{2874510906, 3608059924}, Hs.HsW2{671291202, 3246995298},
284    Hs.HsW2{3513617283, 2455934108}, Hs.HsW2{2112839561, 3946462189}, Hs.HsW2{3870870479, 1227967054}, Hs.HsW2{1685998598, 3703792943},
285    Hs.HsW2{708717373, 3663944268}, Hs.HsW2{1089721179, 1191977385}, Hs.HsW2{1473344692, 827941281}, Hs.HsW2{3660863916, 1718806557},
286    Hs.HsW2{291890030, 1534523258}, Hs.HsW2{1741909704, 1146925078}, Hs.HsW2{1552459419, 3309903136}, Hs.HsW2{2050491833, 1164719240},
287    Hs.HsW2{3295809555, 4292721082}, Hs.HsW2{507922879, 2578403751}, Hs.HsW2{3161926101, 2707152924}, Hs.HsW2{3833984944, 1390094176},
288    Hs.HsW2{3123735892, 2356696942}, Hs.HsW2{131553840, 2924875621}, Hs.HsW2{2194048969, 2515677025}, Hs.HsW2{1149873061, 1908800501},
289    Hs.HsW2{3878212990, 3393516121}, Hs.HsW2{3468418189, 2293792044}, Hs.HsW2{3192526250, 3132198194}, Hs.HsW2{3919274270, 2347297939},
290    Hs.HsW2{2663248393, 397874152}, Hs.HsW2{1269432692, 3004980520}, Hs.HsW2{344950049, 4006253873}, Hs.HsW2{2223096648, 3100743699},
291    Hs.HsW2{3545282556, 2307455410}, Hs.HsW2{2573903929, 3118537869}, Hs.HsW2{210667551, 1514566628}, Hs.HsW2{2203490680, 377984886},
292    Hs.HsW2{3609906946, 3208717294}, Hs.HsW2{3037972357, 1319236019}, Hs.HsW2{3782185471, 3882304811}, Hs.HsW2{805444220, 1963315639},
293    Hs.HsW2{3371997196, 2778450526}, Hs.HsW2{553117603, 2902892250}, Hs.HsW2{2721144938, 955560379}, Hs.HsW2{2490646167, 1624430462},
294    Hs.HsW2{963048492, 2600452120}, Hs.HsW2{4087828575, 613312360}, Hs.HsW2{3028539700, 3453241764}, Hs.HsW2{1964748648, 2276823637},
295    Hs.HsW2{37567615, 468348206}, Hs.HsW2{1533017259, 1797198405}, Hs.HsW2{770273549, 1949652265}, Hs.HsW2{284556767, 3624095597},
296    Hs.HsW2{2074614536, 3323563167}, Hs.HsW2{2745269979, 3145796012}, Hs.HsW2{2903689915, 4197259110}, Hs.HsW2{1715695737, 3341355009},
297    Hs.HsW2{1999016727, 2623537019}, Hs.HsW2{0, 0}, Hs.HsW2{2759206123, 366413513}, Hs.HsW2{802442610, 1876899847},
298    Hs.HsW2{1710117559, 1605819704}, Hs.HsW2{2260533047, 2738615613}, Hs.HsW2{4236573326, 3864510901}, Hs.HsW2{1935469545, 2861966631},
299    Hs.HsW2{3218737947, 969159973}, Hs.HsW2{2267865478, 542002474}, Hs.HsW2{2342676889, 2047360718}, Hs.HsW2{3073309690, 1431018653},
300    Hs.HsW2{1447127557, 2989283766}, Hs.HsW2{2783328858, 2527248094}, Hs.HsW2{649110306, 2149919144}, Hs.HsW2{995870803, 2165681462},
301    Hs.HsW2{26222257, 2205530135}, Hs.HsW2{1245323205, 812246335}, Hs.HsW2{3990952416, 3173070543}, Hs.HsW2{622690796, 414907537},
302    Hs.HsW2{1283283780, 491409997}, Hs.HsW2{1767955112, 99659484}, Hs.HsW2{1926034776, 702782768}, Hs.HsW2{1499644116, 1895137131},
303    Hs.HsW2{61678286, 2560611641}, Hs.HsW2{2547588185, 4165796423}, Hs.HsW2{2865074315, 1417353219}, Hs.HsW2{2144494582, 4040185539},
304    Hs.HsW2{2443073752, 3580802357}, Hs.HsW2{1368797237, 477812435}, Hs.HsW2{560462098, 779298509}, Hs.HsW2{1025281234, 2889226820},
305    Hs.HsW2{1637100105, 1769932644}, Hs.HsW2{3698531629, 1263624047}, Hs.HsW2{4100983407, 2329438221}, Hs.HsW2{246658144, 1101799114},
306    Hs.HsW2{3624494547, 2107147571}, Hs.HsW2{1234648331, 2834706438}, Hs.HsW2{180997278, 2003158166}, Hs.HsW2{3319926434, 2091385261},
307    Hs.HsW2{1588959972, 3735253006}, Hs.HsW2{2711372452, 2691392642}, Hs.HsW2{1186240474, 1781503707}, Hs.HsW2{3565678028, 668923607},
308    Hs.HsW2{1561901098, 1178379575}, Hs.HsW2{4024182175, 2798345185}, Hs.HsW2{4184775873, 1407951870}, Hs.HsW2{2476958887, 3464812571},
309    Hs.HsW2{190435887, 4094721153}, Hs.HsW2{1830462038, 859403392}, Hs.HsW2{3147854821, 252571513}, Hs.HsW2{2685164565, 589225109},
310    Hs.HsW2{3327077484, 3828864148}, Hs.HsW2{4132255248, 2435974435}, Hs.HsW2{3353293533, 1732406403}, Hs.HsW2{842999299, 1861205145},
311    Hs.HsW2{1791883366, 2641329125}, Hs.HsW2{732837260, 1494671963}, Hs.HsW2{3804410673, 2146996242}, Hs.HsW2{656457107, 55611839},
312    Hs.HsW2{2416854633, 1444613410}, Hs.HsW2{1864867369, 684923310}, Hs.HsW2{1015845475, 792961619}, Hs.HsW2{4177429104, 3500022761},
313    Hs.HsW2{746155964, 4148227390}, Hs.HsW2{936722508, 3679706834}, Hs.HsW2{2931812469, 1655882335}, Hs.HsW2{3535841613, 184369573},
314    Hs.HsW2{3774844750, 1678966076}, Hs.HsW2{2514755622, 3819401065}, Hs.HsW2{150270177, 1821354424}, Hs.HsW2{253995729, 3269043933},
315    Hs.HsW2{2635124935, 2401814225}, Hs.HsW2{1339062666, 2245363572}, Hs.HsW2{2606208070, 2718658979}, Hs.HsW2{2088714552, 1750041594},
316    Hs.HsW2{3684976413, 3842461706}, Hs.HsW2{4053429280, 1063520838}, Hs.HsW2{4158466209, 306691380}, Hs.HsW2{105333889, 757315442},
317    Hs.HsW2{3431391474, 2471628802}, Hs.HsW2{2380606744, 1462471100}, Hs.HsW2{2969149898, 4213019640}, Hs.HsW2{1193576811, 3915001548},
318    Hs.HsW2{2232540665, 1000611844}, Hs.HsW2{3065963851, 3594396810}, Hs.HsW2{1596294229, 1574357017}, Hs.HsW2{1312843579, 111165283},
319    Hs.HsW2{1991675302, 522864492}, Hs.HsW2{2596768503, 561957300}, Hs.HsW2{776229827, 3970596880}, Hs.HsW2{3114094490, 350716503}]
320
321# T_3[b] = l(Pi(b) << 24): each entry's low and high 32 bits
322def hs.stb.t3.list() -> List<&2, Hs.HsW2>:
323  [Hs.HsW2{3363551749, 540187436}, Hs.HsW2{1699128625, 1331607288}, Hs.HsW2{4149327537, 3572778869}, Hs.HsW2{2232285835, 2187764859},
324    Hs.HsW2{1517070725, 3147328161}, Hs.HsW2{4188934041, 3380210440}, Hs.HsW2{2721537697, 765916231}, Hs.HsW2{3447555446, 510928733},
325    Hs.HsW2{2148255224, 3156219914}, Hs.HsW2{3000788414, 3030578945}, Hs.HsW2{2551934310, 3878065263}, Hs.HsW2{3206662476, 1223083091},
326    Hs.HsW2{252330389, 1120590227}, Hs.HsW2{2865548576, 4020534116}, Hs.HsW2{1614846530, 1897400969}, Hs.HsW2{4137963020, 2343776923},
327    Hs.HsW2{758569676, 3544987102}, Hs.HsW2{3156466838, 2838453116}, Hs.HsW2{1757088195, 3004859818}, Hs.HsW2{2805031378, 333465654},
328    Hs.HsW2{700783874, 2991455297}, Hs.HsW2{3084540621, 2330217328}, Hs.HsW2{3647306151, 3866226052}, Hs.HsW2{3597613106, 2763731991},
329    Hs.HsW2{3580702184, 1165142840}, Hs.HsW2{3930530140, 2981394273}, Hs.HsW2{1890296157, 3894151631}, Hs.HsW2{3464466604, 4290623602},
330    Hs.HsW2{4250781783, 2826445463}, Hs.HsW2{1783424164, 227831659}, Hs.HsW2{1536774456, 3839827791}, Hs.HsW2{3398195042, 2663150061},
331    Hs.HsW2{2955643097, 170663360}, Hs.HsW2{1570601873, 995114001}, Hs.HsW2{287228834, 3326310056}, Hs.HsW2{600400868, 3468794275},
332    Hs.HsW2{3313899255, 3698763902}, Hs.HsW2{1940501639, 164992736}, Hs.HsW2{2102791599, 341326493}, Hs.HsW2{1059720372, 4106673241},
333    Hs.HsW2{2230846006, 3709981077}, Hs.HsW2{1037951443, 1246246552}, Hs.HsW2{451364345, 3850921636}, Hs.HsW2{2119440501, 4119963058},
334    Hs.HsW2{1951950483, 2300428368}, Hs.HsW2{403744926, 1527155813}, Hs.HsW2{201872463, 2734900924}, Hs.HsW2{3330540333, 1035941713},
335    Hs.HsW2{2018521820, 706643692}, Hs.HsW2{4238881002, 4148123513}, Hs.HsW2{807423265, 3054241226}, Hs.HsW2{724758629, 214111872},
336    Hs.HsW2{3717643881, 2272273435}, Hs.HsW2{2582549979, 3093422465}, Hs.HsW2{337181905, 4161129177}, Hs.HsW2{3151105666, 703008204},
337    Hs.HsW2{1348523875, 3339980611}, Hs.HsW2{3903900731, 255499680}, Hs.HsW2{1299595406, 2723430231}, Hs.HsW2{3245723961, 3178717665},
338    Hs.HsW2{2091119890, 1260343155}, Hs.HsW2{801191851, 1841487647}, Hs.HsW2{1739671638, 4056964153}, Hs.HsW2{367854700, 2806169399},
339    Hs.HsW2{488019949, 1698705428}, Hs.HsW2{3664211069, 129528491}, Hs.HsW2{2281314284, 1021857466}, Hs.HsW2{3413749727, 3254453251},
340    Hs.HsW2{84295539, 1044823153}, Hs.HsW2{303879800, 663415175}, Hs.HsW2{2398387408, 2712515703}, Hs.HsW2{1398981305, 652054636},
341    Hs.HsW2{1486570722, 85360736}, Hs.HsW2{3617243279, 4227613177}, Hs.HsW2{2848905466, 242082891}, Hs.HsW2{2347910051, 2682980358},
342    Hs.HsW2{3496678043, 2067011401}, Hs.HsW2{1250398874, 580676071}, Hs.HsW2{1115423003, 3768510148}, Hs.HsW2{1918651450, 1452466958},
343    Hs.HsW2{1587506763, 3667501886}, Hs.HsW2{4099122027, 893245530}, Hs.HsW2{2430664423, 623123276}, Hs.HsW2{2198458402, 1575585573},
344    Hs.HsW2{3229624708, 3794801679}, Hs.HsW2{2696983494, 2468880006}, Hs.HsW2{2754835464, 4062828313}, Hs.HsW2{2906464052, 1869360596},
345    Hs.HsW2{2923367150, 2393223931}, Hs.HsW2{3295931978, 2201083280}, Hs.HsW2{3039672234, 879403441}, Hs.HsW2{100936361, 3750699870},
346    Hs.HsW2{2704624507, 3429854056}, Hs.HsW2{1858020202, 1821746932}, Hs.HsW2{1807293465, 1389566597}, Hs.HsW2{3566785877, 439738070},
347    Hs.HsW2{3847053513, 4085165810}, Hs.HsW2{2747442716, 1927381417}, Hs.HsW2{1368731614, 2555607725}, Hs.HsW2{4289340720, 385271894},
348    Hs.HsW2{2635944469, 3646957598}, Hs.HsW2{484667216, 973555194}, Hs.HsW2{4048919576, 192635947}, Hs.HsW2{2599190529, 1504214702},
349    Hs.HsW2{1082911868, 1578109957}, Hs.HsW2{434458659, 71432587}, Hs.HsW2{886278895, 3608005717}, Hs.HsW2{3787368199, 2457823085},
350    Hs.HsW2{3106268133, 2540300045}, Hs.HsW2{2434074202, 2053336738}, Hs.HsW2{384766390, 1183522840}, Hs.HsW2{1054864393, 2877401527},
351    Hs.HsW2{2315762462, 3232529896}, Hs.HsW2{2349044151, 522411702}, Hs.HsW2{1166922511, 1616294004}, Hs.HsW2{49802599, 3197037249},
352    Hs.HsW2{3763036090, 3443004035}, Hs.HsW2{3262629091, 1556020942}, Hs.HsW2{1816710669, 3525004341}, Hs.HsW2{1689476492, 270123798},
353    Hs.HsW2{3516852774, 611541671}, Hs.HsW2{3005848835, 3957687023}, Hs.HsW2{2197563551, 45019851}, Hs.HsW2{2632493736, 2250726896},
354    Hs.HsW2{4205582915, 682652711}, Hs.HsW2{2652850127, 950646577}, Hs.HsW2{3100646232, 3358495459}, Hs.HsW2{2602137788, 116329280},
355    Hs.HsW2{3346135952, 1660437183}, Hs.HsW2{283851551, 2567177030}, Hs.HsW2{1199193704, 3738720949}, Hs.HsW2{1665306520, 2429654438},
356    Hs.HsW2{717687000, 1401185134}, Hs.HsW2{2068981510, 3419871683}, Hs.HsW2{1715777771, 2929142231}, Hs.HsW2{168591078, 2089575906},
357    Hs.HsW2{133288468, 2160613040}, Hs.HsW2{750985841, 2349547568}, Hs.HsW2{534870666, 3687766741}, Hs.HsW2{953933472, 1947110121},
358    Hs.HsW2{1418924205, 2786445020}, Hs.HsW2{387639563, 432821750}, Hs.HsW2{4267695501, 1236385208}, Hs.HsW2{674293183, 3976890799},
359    Hs.HsW2{4121320406, 1786424756}, Hs.HsW2{2297452153, 2116196137}, Hs.HsW2{1432807440, 4182946610}, Hs.HsW2{3747697422, 973000410},
360    Hs.HsW2{83085262, 1627507103}, Hs.HsW2{1639277311, 778010471}, Hs.HsW2{651123863, 4035388882}, Hs.HsW2{2249191249, 1672428372},
361    Hs.HsW2{4014022191, 2415053584}, Hs.HsW2{891712082, 2286598587}, Hs.HsW2{3887762862, 1307591731}, Hs.HsW2{3546875713, 2600306790},
362    Hs.HsW2{3734285235, 1723448116}, Hs.HsW2{2450985856, 2611671437}, Hs.HsW2{4037043365, 1413222853}, Hs.HsW2{3201577457, 396472765},
363    Hs.HsW2{4087509375, 3052769002}, Hs.HsW2{1233487680, 3277190856}, Hs.HsW2{1766781310, 3965579332}, Hs.HsW2{3697493716, 3627504117},
364    Hs.HsW2{234728690, 4232328018}, Hs.HsW2{0, 0}, Hs.HsW2{1500429407, 1515320718}, Hs.HsW2{775212822, 847620849},
365    Hs.HsW2{1841116848, 2371631579}, Hs.HsW2{3863966995, 313995741}, Hs.HsW2{2057822139, 2492492845}, Hs.HsW2{2898847625, 808147002},
366    Hs.HsW2{151939900, 2638609101}, Hs.HsW2{2298851012, 560325319}, Hs.HsW2{2002416457, 1758748543}, Hs.HsW2{1449459146, 412822557},
367    Hs.HsW2{50468314, 3788087087}, Hs.HsW2{908355464, 1770202772}, Hs.HsW2{504660535, 2223615803}, Hs.HsW2{836089244, 3914035236},
368    Hs.HsW2{1867176919, 869454618}, Hs.HsW2{1133115814, 3218707242}, Hs.HsW2{2872653213, 2967670410}, Hs.HsW2{2949313107, 3521300245},
369    Hs.HsW2{1009260910, 353321846}, Hs.HsW2{2481122109, 3303900259}, Hs.HsW2{3280092254, 66685728}, Hs.HsW2{1283700787, 4245899961},
370    Hs.HsW2{2984144996, 1433102382}, Hs.HsW2{936484661, 918836090}, Hs.HsW2{2040908385, 1968829186}, Hs.HsW2{1385642500, 2040194434},
371    Hs.HsW2{1215332349, 2618458918}, Hs.HsW2{334048965, 2026740841}, Hs.HsW2{251640104, 495823997}, Hs.HsW2{1316246868, 1134403704},
372    Hs.HsW2{3431497163, 1093882547}, Hs.HsW2{454212932, 3134133066}, Hs.HsW2{634210637, 290372349}, Hs.HsW2{550204990, 789055116},
373    Hs.HsW2{3123181119, 1990228002}, Hs.HsW2{4065823170, 3937598212}, Hs.HsW2{2180922693, 3815206372}, Hs.HsW2{2514928020, 459450173},
374    Hs.HsW2{1550353196, 1679247871}, Hs.HsW2{2534485235, 2783727100}, Hs.HsW2{3184927787, 4134022802}, Hs.HsW2{1148726194, 1058129306},
375    Hs.HsW2{3988190024, 830218705}, Hs.HsW2{1974312494, 3596268990}, Hs.HsW2{3034074903, 1798165599}, Hs.HsW2{2531578958, 4205525010},
376    Hs.HsW2{4004832914, 3501571838}, Hs.HsW2{852992070, 142798603}, Hs.HsW2{2822447175, 1361744293}, Hs.HsW2{4166776612, 2520686310},
377    Hs.HsW2{607695344, 1309265683}, Hs.HsW2{4216972030, 2012676553}, Hs.HsW2{1265789479, 2111511561}, Hs.HsW2{32897213, 1598518766},
378    Hs.HsW2{574397273, 2441538637}, Hs.HsW2{2399241325, 4276797849}, Hs.HsW2{3837302900, 2889472796}, Hs.HsW2{1902008800, 3076226081},
379    Hs.HsW2{658154538, 2948616252}, Hs.HsW2{3963816949, 1849381951}, Hs.HsW2{557747843, 1884255074}, Hs.HsW2{3683816640, 1493108549},
380    Hs.HsW2{2682961778, 1743700703}, Hs.HsW2{3481954321, 2700791196}, Hs.HsW2{3633348890, 3107362922}, Hs.HsW2{1004129146, 2512852422},
381    Hs.HsW2{975975367, 3397410856}, Hs.HsW2{3913626758, 1350428750}, Hs.HsW2{1600820982, 2245973712}, Hs.HsW2{1333898729, 484103574},
382    Hs.HsW2{3056575088, 3584245406}, Hs.HsW2{2381736202, 1080306520}, Hs.HsW2{3381543608, 2138435266}, Hs.HsW2{3813231200, 754027948},
383    Hs.HsW2{200902235, 600510476}, Hs.HsW2{3954366945, 4008903311}, Hs.HsW2{2484287785, 1143329491}, Hs.HsW2{2141315272, 2866204764},
384    Hs.HsW2{2781252789, 2909709047}, Hs.HsW2{150705025, 3254947619}, Hs.HsW2{1183827669, 2174693211}, Hs.HsW2{3533504508, 3317366152},
385    Hs.HsW2{1469121911, 1205623283}, Hs.HsW2{959325725, 726269703}, Hs.HsW2{857889019, 1472568037}, Hs.HsW2{3804017373, 1941370946},
386    Hs.HsW2{1656190757, 3482771528}, Hs.HsW2{2797902191, 1286028760}, Hs.HsW2{1098781889, 22510059}, Hs.HsW2{1991216116, 932391569}]
387
388# T_4[b] = l(Pi(b) << 32): each entry's low and high 32 bits
389def hs.stb.t4.list() -> List<&2, Hs.HsW2>:
390  [Hs.HsW2{614330942, 420097179}, Hs.HsW2{576971241, 795015350}, Hs.HsW2{1083782741, 2055173447}, Hs.HsW2{3579202975, 856390564},
391    Hs.HsW2{1181164930, 1276617066}, Hs.HsW2{2097542584, 2989426923}, Hs.HsW2{197216460, 1398753268}, Hs.HsW2{3565695031, 988568871},
392    Hs.HsW2{625184662, 283970072}, Hs.HsW2{740506903, 1365311991}, Hs.HsW2{2681228974, 332165012}, Hs.HsW2{1095191549, 1939362756},
393    Hs.HsW2{222255899, 1698141145}, Hs.HsW2{2528181295, 1379951739}, Hs.HsW2{3530957792, 210012426}, Hs.HsW2{1882893987, 3608714034},
394    Hs.HsW2{599628865, 646307381}, Hs.HsW2{297795322, 2570157147}, Hs.HsW2{1325897475, 228305541}, Hs.HsW2{4225010373, 1891186248},
395    Hs.HsW2{3809199806, 2818851324}, Hs.HsW2{3694591774, 1921478731}, Hs.HsW2{870063891, 3058926829}, Hs.HsW2{1055081480, 3546552116},
396    Hs.HsW2{1847324943, 969750699}, Hs.HsW2{169817444, 1522033015}, Hs.HsW2{4120139323, 247123721}, Hs.HsW2{2221966640, 3494212280},
397    Hs.HsW2{3182669639, 1018074914}, Hs.HsW2{794606322, 1247112047}, Hs.HsW2{1992605044, 3782233887}, Hs.HsW2{1153884111, 1589964145},
398    Hs.HsW2{1282937062, 380616733}, Hs.HsW2{3593063034, 675221820}, Hs.HsW2{390196525, 2941888630}, Hs.HsW2{505503660, 4006978457},
399    Hs.HsW2{1241089236, 1005813416}, Hs.HsW2{2775376700, 3826507926}, Hs.HsW2{2565873873, 742628666}, Hs.HsW2{1678034027, 1668635100},
400    Hs.HsW2{3858093417, 2657916369}, Hs.HsW2{73394586, 616273974}, Hs.HsW2{3670600905, 1156555878}, Hs.HsW2{3356005846, 3337269925},
401    Hs.HsW2{891423940, 2151370944}, Hs.HsW2{3130245432, 52520332}, Hs.HsW2{1573383708, 2409544774}, Hs.HsW2{419508691, 3512357175},
402    Hs.HsW2{1759896280, 262532230}, Hs.HsW2{2366650289, 2445900119}, Hs.HsW2{1765515120, 105040389}, Hs.HsW2{2203118415, 4023025686},
403    Hs.HsW2{4083828204, 953293604}, Hs.HsW2{2943604312, 3198910945}, Hs.HsW2{3881053988, 2361383370}, Hs.HsW2{2180059394, 4246326285},
404    Hs.HsW2{3142433936, 180765455}, Hs.HsW2{1782847637, 494313629}, Hs.HsW2{4056661921, 704730943}, Hs.HsW2{2303712811, 3044204897},
405    Hs.HsW2{2824058919, 2166649679}, Hs.HsW2{1139192240, 1632313311}, Hs.HsW2{1111018520, 1756117340}, Hs.HsW2{3623335890, 567818175},
406    Hs.HsW2{1250296625, 549917744}, Hs.HsW2{1663347220, 1559931762}, Hs.HsW2{3037552750, 1959115342}, Hs.HsW2{1952794425, 4087546628},
407    Hs.HsW2{4027957769, 602304956}, Hs.HsW2{1203329066, 1173391337}, Hs.HsW2{417287291, 3636295604}, Hs.HsW2{3954510231, 3765398672},
408    Hs.HsW2{641468531, 198795392}, Hs.HsW2{239131902, 2114189633}, Hs.HsW2{3326626088, 3102297060}, Hs.HsW2{3905588850, 4217046536},
409    Hs.HsW2{2651730694, 439044375}, Hs.HsW2{1636126809, 1311369065}, Hs.HsW2{4243907770, 1328989414}, Hs.HsW2{2513402826, 1232342755},
410    Hs.HsW2{2261876605, 3264626339}, Hs.HsW2{274826066, 2429967064}, Hs.HsW2{44169805, 315837467}, Hs.HsW2{1975204497, 4198770055},
411    Hs.HsW2{3119269597, 404033300}, Hs.HsW2{1805280573, 345081374}, Hs.HsW2{2871803842, 2584746455}, Hs.HsW2{117314519, 912839725},
412    Hs.HsW2{1443276496, 3703700402}, Hs.HsW2{2035948578, 2526318813}, Hs.HsW2{3161314031, 894022049}, Hs.HsW2{2699917070, 3377421859},
413    Hs.HsW2{1530527179, 3119933547}, Hs.HsW2{4025147405, 3302290598}, Hs.HsW2{536814084, 3878847770}, Hs.HsW2{1589144057, 2494224094},
414    Hs.HsW2{119565951, 1066398382}, Hs.HsW2{996331578, 4265126273}, Hs.HsW2{2347639910, 2812390778}, Hs.HsW2{3723002550, 2069911240},
415    Hs.HsW2{1875217575, 808066600}, Hs.HsW2{2049285063, 2376137285}, Hs.HsW2{3765715291, 3006278500}, Hs.HsW2{4287325023, 1409461886},
416    Hs.HsW2{2628766027, 150471948}, Hs.HsW2{2318424526, 2923858937}, Hs.HsW2{2844640655, 2294502860}, Hs.HsW2{3348509824, 2970512743},
417    Hs.HsW2{3786030323, 3134655975}, Hs.HsW2{839017147, 3216286318}, Hs.HsW2{2265907925, 3413186592}, Hs.HsW2{1420254365, 3457333161},
418    Hs.HsW2{3630765700, 1446832253}, Hs.HsW2{2021941642, 2675160670}, Hs.HsW2{1824131906, 723416240}, Hs.HsW2{1616588273, 1204732394},
419    Hs.HsW2{4147489910, 476676882}, Hs.HsW2{3652676396, 1608240894}, Hs.HsW2{2410794492, 2199532876}, Hs.HsW2{314603807, 2181371587},
420    Hs.HsW2{2930617328, 3075254114}, Hs.HsW2{478193121, 4228312962}, Hs.HsW2{1159242343, 1461963762}, Hs.HsW2{1600525393, 2639130717},
421    Hs.HsW2{771571903, 1485186932}, Hs.HsW2{1060977056, 3666031031}, Hs.HsW2{3507069957, 397468562}, Hs.HsW2{3475569577, 4184162315},
422    Hs.HsW2{698525989, 2084421442}, Hs.HsW2{669152731, 37635587}, Hs.HsW2{216082099, 1825617242}, Hs.HsW2{2190382823, 3861751445},
423    Hs.HsW2{3019076537, 1118662243}, Hs.HsW2{941447135, 3842818841}, Hs.HsW2{1922782446, 3318470441}, Hs.HsW2{4247427346, 1188160101},
424    Hs.HsW2{2421092344, 1680388182}, Hs.HsW2{320734391, 2346856512}, Hs.HsW2{719138496, 1728697818}, Hs.HsW2{4098501523, 123595146},
425    Hs.HsW2{2080106095, 2219302086}, Hs.HsW2{3081542179, 1712780885}, Hs.HsW2{3981122112, 3590830269}, Hs.HsW2{3551026760, 90419081},
426    Hs.HsW2{549591972, 1035056301}, Hs.HsW2{3090299765, 301083031}, Hs.HsW2{1264090777, 689975987}, Hs.HsW2{2469488669, 2132597454},
427    Hs.HsW2{3233176319, 2390859721}, Hs.HsW2{3805657878, 2716034943}, Hs.HsW2{3996425637, 3442725413}, Hs.HsW2{2242836632, 3651294267},
428    Hs.HsW2{4195022701, 2036207819}, Hs.HsW2{2569952633, 631552953}, Hs.HsW2{1736131470, 2017538884}, Hs.HsW2{3472262657, 4035077768},
429    Hs.HsW2{2744316139, 3531289787}, Hs.HsW2{1660606396, 1428000241}, Hs.HsW2{3503806893, 509068561}, Hs.HsW2{1910821643, 3741302193},
430    Hs.HsW2{2150591658, 4110346894}, Hs.HsW2{830334302, 2759903478}, Hs.HsW2{2141458421, 2700887280}, Hs.HsW2{3284786458, 2511730001},
431    Hs.HsW2{1835300586, 586764851}, Hs.HsW2{0, 0}, Hs.HsW2{379555973, 2797506293}, Hs.HsW2{1933912390, 3425497514},
432    Hs.HsW2{3205649674, 780000057}, Hs.HsW2{1473829752, 3576094001}, Hs.HsW2{146722601, 1214983532}, Hs.HsW2{912100129, 2601466456},
433    Hs.HsW2{2916232213, 2893598202}, Hs.HsW2{2291245955, 3163932642}, Hs.HsW2{1708833219, 1787985759}, Hs.HsW2{463522718, 3280543020},
434    Hs.HsW2{1358476551, 3936956319}, Hs.HsW2{3386304638, 3473773606}, Hs.HsW2{444511798, 3396221871}, Hs.HsW2{1503135622, 2871338096},
435    Hs.HsW2{3746134267, 1773345491}, Hs.HsW2{3428285516, 3796970131}, Hs.HsW2{2786288857, 4280781326}, Hs.HsW2{1722105382, 1906709959},
436    Hs.HsW2{888959340, 2312926787}, Hs.HsW2{1381584714, 4168770436}, Hs.HsW2{3910464474, 4072415371}, Hs.HsW2{3244828503, 2271656266},
437    Hs.HsW2{2094762000, 3150458472}, Hs.HsW2{4185223304, 1651145299}, Hs.HsW2{1481013806, 2730623731}, Hs.HsW2{3675689313, 1292403429},
438    Hs.HsW2{31358376, 166143619}, Hs.HsW2{1998242012, 3902237084}, Hs.HsW2{1033683949, 3360718252}, Hs.HsW2{2704476838, 3232266400},
439    Hs.HsW2{3828066497, 2542515026}, Hs.HsW2{3932910655, 3918023187}, Hs.HsW2{3201050786, 664468922}, Hs.HsW2{1322904235, 75271174},
440    Hs.HsW2{2974976500, 1350443640}, Hs.HsW2{2962027612, 1503200507}, Hs.HsW2{367007584, 3179996269}, Hs.HsW2{4071897156, 825572775},
441    Hs.HsW2{3867824780, 2237202249}, Hs.HsW2{2465142197, 1996225613}, Hs.HsW2{555509260, 878088750}, Hs.HsW2{1545180084, 2256116421},
442    Hs.HsW2{2589055644, 1049678113}, Hs.HsW2{92378162, 761052853}, Hs.HsW2{2362329625, 2553176020}, Hs.HsW2{2722925891, 3684438584},
443    Hs.HsW2{3400101787, 3560570558}, Hs.HsW2{157332097, 1099697135}, Hs.HsW2{4142649822, 361670033}, Hs.HsW2{1302752590, 524871326},
444    Hs.HsW2{2389684308, 2331841487}, Hs.HsW2{492755017, 4125214977}, Hs.HsW2{1361496239, 3813542172}, Hs.HsW2{816027894, 2909269621},
445    Hs.HsW2{780322650, 1135758828}, Hs.HsW2{679269517, 1977260481}, Hs.HsW2{931395209, 2464685275}, Hs.HsW2{3308768973, 2749178236},
446    Hs.HsW2{3734439251, 1616133200}, Hs.HsW2{2868003434, 2482454356}, Hs.HsW2{2121953885, 2837144179}, Hs.HsW2{1401369314, 4053615879},
447    Hs.HsW2{262054230, 2011488194}, Hs.HsW2{3033734598, 2099420365}, Hs.HsW2{58689509, 456419992}, Hs.HsW2{2763169428, 3992241685},
448    Hs.HsW2{2484143714, 1083385952}, Hs.HsW2{1525121123, 2953924328}, Hs.HsW2{3060983691, 1878118614}, Hs.HsW2{2442170960, 1842321109},
449    Hs.HsW2{3969214440, 3756039742}, Hs.HsW2{1210579324, 840194091}, Hs.HsW2{339634888, 3027092206}, Hs.HsW2{2815236465, 4139822221},
450    Hs.HsW2{3448308196, 3954576400}, Hs.HsW2{985443730, 4158623490}, Hs.HsW2{3256328370, 2622673874}, Hs.HsW2{4171959584, 1804426448},
451    Hs.HsW2{2609882932, 930609058}, Hs.HsW2{2641474787, 18817935}, Hs.HsW2{1011007045, 3250019119}, Hs.HsW2{4266991351, 1575323901},
452    Hs.HsW2{721638248, 1861153625}, Hs.HsW2{3303650149, 2855929855}, Hs.HsW2{969091703, 3974882714}, Hs.HsW2{2540601735, 1537688312},
453    Hs.HsW2{2989297169, 1263159520}, Hs.HsW2{3413578291, 3722369085}, Hs.HsW2{2886488509, 2778721145}, Hs.HsW2{1434001717, 3354759466}]
454
455# T_5[b] = l(Pi(b) << 40): each entry's low and high 32 bits
456def hs.stb.t5.list() -> List<&2, Hs.HsW2>:
457  [Hs.HsW2{1755951242, 1835720774}, Hs.HsW2{199804739, 984870987}, Hs.HsW2{1421068552, 3843954283}, Hs.HsW2{901968185, 3197151723},
458    Hs.HsW2{938655425, 2999387750}, Hs.HsW2{865214508, 2859025761}, Hs.HsW2{995230187, 2586362735}, Hs.HsW2{2874370452, 3721288339},
459    Hs.HsW2{4130875431, 238293822}, Hs.HsW2{3964994699, 1386228641}, Hs.HsW2{3300041079, 2734198679}, Hs.HsW2{3391246757, 2252399891},
460    Hs.HsW2{1477670434, 3455177570}, Hs.HsW2{3739192795, 4268537608}, Hs.HsW2{3356630621, 2316782238}, Hs.HsW2{1803638286, 1738053123},
461    Hs.HsW2{2507759598, 1508705075}, Hs.HsW2{2339696047, 500660395}, Hs.HsW2{765432429, 3998433017}, Hs.HsW2{4171815157, 713849274},
462    Hs.HsW2{1773214198, 1808742798}, Hs.HsW2{800054677, 3791950196}, Hs.HsW2{2157718252, 660900064}, Hs.HsW2{3633274062, 3935656834},
463    Hs.HsW2{2581192900, 1896007226}, Hs.HsW2{2781059398, 4185272343}, Hs.HsW2{521476925, 1117758032}, Hs.HsW2{3926250910, 1180288811},
464    Hs.HsW2{3478808116, 2555084764}, Hs.HsW2{1409003873, 4148306729}, Hs.HsW2{146809287, 809600526}, Hs.HsW2{382571398, 1954282902},
465    Hs.HsW2{2452694919, 1269905009}, Hs.HsW2{2322351315, 460497251}, Hs.HsW2{3895827046, 1242458278}, Hs.HsW2{4065900234, 379211833},
466    Hs.HsW2{1323230628, 3112840948}, Hs.HsW2{1581492023, 3641196520}, Hs.HsW2{962743827, 2524933346}, Hs.HsW2{1008368002, 2289366573},
467    Hs.HsW2{183529023, 1008085379}, Hs.HsW2{1115576974, 2439375869}, Hs.HsW2{1290709596, 3051192697}, Hs.HsW2{2016735769, 233369946},
468    Hs.HsW2{3822935333, 1891473645}, Hs.HsW2{847939920, 2899090601}, Hs.HsW2{424004136, 1449545434}, Hs.HsW2{260594094, 572371788},
469    Hs.HsW2{4204304141, 651941431}, Hs.HsW2{4033411378, 449707956}, Hs.HsW2{1678315424, 1166353743}, Hs.HsW2{399850234, 1927160926},
470    Hs.HsW2{2085907700, 356954717}, Hs.HsW2{4219485809, 545132543}, Hs.HsW2{735003512, 4205498995}, Hs.HsW2{921311165, 3026378670},
471    Hs.HsW2{2887455229, 3482480593}, Hs.HsW2{3685202506, 3764858311}, Hs.HsW2{1567310259, 3556395437}, Hs.HsW2{2987828156, 2343048265},
472    Hs.HsW2{105959701, 351923338}, Hs.HsW2{3944578274, 1090264803}, Hs.HsW2{1972167759, 597880219}, Hs.HsW2{352181374, 2016170523},
473    Hs.HsW2{4050669646, 476587644}, Hs.HsW2{3251279590, 3170047320}, Hs.HsW2{1269223989, 2810295355}, Hs.HsW2{704580736, 4143807998},
474    Hs.HsW2{3287996702, 2963585749}, Hs.HsW2{2841847404, 3516527902}, Hs.HsW2{2434384131, 1094926388}, Hs.HsW2{3981290999, 1409675881},
475    Hs.HsW2{1234607565, 2882935734}, Hs.HsW2{3887973320, 1746131946}, Hs.HsW2{2676568529, 1710959280}, Hs.HsW2{1390614557, 4058512097},
476    Hs.HsW2{1512258010, 3248913647}, Hs.HsW2{3774200737, 2052058792}, Hs.HsW2{91764625, 504077007}, Hs.HsW2{1634809905, 1536081792},
477    Hs.HsW2{3409639641, 2162506971}, Hs.HsW2{367359234, 2122943443}, Hs.HsW2{557788487, 3334274032}, Hs.HsW2{3077477421, 2510524038},
478    Hs.HsW2{2367962298, 154047521}, Hs.HsW2{1161175783, 2201607871}, Hs.HsW2{3120456959, 2971395074}, Hs.HsW2{1665234889, 1473843213},
479    Hs.HsW2{571984835, 3427700149}, Hs.HsW2{1911323298, 990686876}, Hs.HsW2{1372323481, 4212493476}, Hs.HsW2{2192336148, 724772717},
480    Hs.HsW2{2047131105, 29318871}, Hs.HsW2{2939418489, 3311409556}, Hs.HsW2{1825123943, 1975821121}, Hs.HsW2{2800451522, 4085532242},
481    Hs.HsW2{4258328420, 881320821}, Hs.HsW2{73441005, 414073607}, Hs.HsW2{2468974331, 1293217721}, Hs.HsW2{2973648184, 2170184204},
482    Hs.HsW2{122189929, 308032834}, Hs.HsW2{3460484936, 2666440212}, Hs.HsW2{3592399900, 3459068166}, Hs.HsW2{3134620283, 3152646727},
483    Hs.HsW2{2065437853, 119179039}, Hs.HsW2{230168150, 776608961}, Hs.HsW2{2562804152, 2007441394}, Hs.HsW2{18393468, 111532488},
484    Hs.HsW2{1217279153, 2910044798}, Hs.HsW2{504214081, 1144683416}, Hs.HsW2{1437294708, 3820736419}, Hs.HsW2{53012100, 183662149},
485    Hs.HsW2{1842448155, 1935768201}, Hs.HsW2{4018004495, 1481792996}, Hs.HsW2{3102133635, 3082698186}, Hs.HsW2{2120491788, 420552144},
486    Hs.HsW2{1042953850, 2216909216}, Hs.HsW2{4081065910, 272599537}, Hs.HsW2{3512194165, 3698394180}, Hs.HsW2{886724677, 3090509859},
487    Hs.HsW2{1695655644, 1126235271}, Hs.HsW2{3546782605, 3492195273}, Hs.HsW2{2287733547, 388304622}, Hs.HsW2{947578735, 2430252330},
488    Hs.HsW2{1925487654, 838785241}, Hs.HsW2{1176421475, 2311825658}, Hs.HsW2{2008853431, 804602390}, Hs.HsW2{2246319485, 963580463},
489    Hs.HsW2{817546920, 2694525732}, Hs.HsW2{3607561568, 3364415694}, Hs.HsW2{3330469519, 2930712602}, Hs.HsW2{2302976599, 293656358},
490    Hs.HsW2{686269948, 4032341046}, Hs.HsW2{3150850823, 3175893903}, Hs.HsW2{1253997385, 2703519219}, Hs.HsW2{2615783228, 2102749623},
491    Hs.HsW2{3181312530, 2847254277}, Hs.HsW2{2857091304, 3681256283}, Hs.HsW2{2400482114, 91831212}, Hs.HsW2{2172945296, 566317352},
492    Hs.HsW2{1356027877, 4256191852}, Hs.HsW2{1788477298, 1631408075}, Hs.HsW2{2383206974, 64807524}, Hs.HsW2{1451460336, 3913923046},
493    Hs.HsW2{718793220, 4228844475}, Hs.HsW2{330671127, 1785751385}, Hs.HsW2{1877068003, 2134299908}, Hs.HsW2{36720632, 207073165},
494    Hs.HsW2{4240983576, 841104061}, Hs.HsW2{4146102619, 143772406}, Hs.HsW2{832729044, 2789141228}, Hs.HsW2{1955876147, 621229139},
495    Hs.HsW2{1715028056, 1238534850}, Hs.HsW2{2817775294, 4112621466}, Hs.HsW2{2209664104, 764870309}, Hs.HsW2{460686800, 1513218391},
496    Hs.HsW2{1023594750, 2396073957}, Hs.HsW2{1599802955, 3752715808}, Hs.HsW2{3912053530, 1286320494}, Hs.HsW2{4111519395, 80110971},
497    Hs.HsW2{2826669840, 3611045078}, Hs.HsW2{2711816107, 3789058832}, Hs.HsW2{313331051, 1825947281}, Hs.HsW2{1130820594, 2545955381},
498    Hs.HsW2{645354798, 3571502770}, Hs.HsW2{0, 0}, Hs.HsW2{1990460107, 693148638}, Hs.HsW2{3559908324, 3262815883},
499    Hs.HsW2{3999615859, 1593279532}, Hs.HsW2{3162919790, 2937093837}, Hs.HsW2{2231153665, 1070255079}, Hs.HsW2{1551100111, 3579809893},
500    Hs.HsW2{3669955382, 3871536143}, Hs.HsW2{747059985, 3908495153}, Hs.HsW2{2727076143, 3945399637}, Hs.HsW2{783774953, 3835775164},
501    Hs.HsW2{1096203274, 2610404792}, Hs.HsW2{3869600436, 1857421858}, Hs.HsW2{2955340868, 2281683908}, Hs.HsW2{1530630310, 3338904871},
502    Hs.HsW2{2416011391, 1206295036}, Hs.HsW2{977971351, 2626493095}, Hs.HsW2{3790410461, 2095724384}, Hs.HsW2{488985797, 1321733597},
503    Hs.HsW2{2102183304, 333671317}, Hs.HsW2{1617531213, 1563125320}, Hs.HsW2{3430056112, 2461600153}, Hs.HsW2{1650056885, 1367132613},
504    Hs.HsW2{2902702209, 3375871513}, Hs.HsW2{3650614706, 3962602058}, Hs.HsW2{3316254731, 2757580383}, Hs.HsW2{3531551473, 3598938625},
505    Hs.HsW2{2660341933, 1667167096}, Hs.HsW2{2521938282, 1394570614}, Hs.HsW2{1730275620, 1333220106}, Hs.HsW2{473824697, 1215157269},
506    Hs.HsW2{2489448082, 1598610171}, Hs.HsW2{1943811418, 928710929}, Hs.HsW2{1895093214, 1034516308}, Hs.HsW2{3004041920, 2366492033},
507    Hs.HsW2{165185723, 920936390}, Hs.HsW2{2538147862, 1438297278}, Hs.HsW2{3372922657, 2360513366}, Hs.HsW2{3804623961, 1981301029},
508    Hs.HsW2{3042892757, 2582913291}, Hs.HsW2{2627852117, 1862884597}, Hs.HsW2{3024515753, 2672949443}, Hs.HsW2{2278838917, 892911010},
509    Hs.HsW2{408773460, 1354995474}, Hs.HsW2{3706700323, 4063959173}, Hs.HsW2{1861837215, 2039680204}, Hs.HsW2{2744338515, 3985628317},
510    Hs.HsW2{1493950302, 3411282602}, Hs.HsW2{443362476, 1553217695}, Hs.HsW2{2696654551, 3883772632}, Hs.HsW2{211861290, 686802185},
511    Hs.HsW2{1338395864, 3207591740}, Hs.HsW2{1307968288, 3011008689}, Hs.HsW2{3754370215, 4173950656}, Hs.HsW2{1060282118, 2189852776},
512    Hs.HsW2{3446286796, 2484916305}, Hs.HsW2{2922077701, 3284516956}, Hs.HsW2{3269619810, 3053544221}, Hs.HsW2{539460667, 3222872632},
513    Hs.HsW2{244379858, 616065668}, Hs.HsW2{661650514, 3527743354}, Hs.HsW2{2352780742, 260787689}, Hs.HsW2{4277668320, 1047893296},
514    Hs.HsW2{2032950117, 189606034}, Hs.HsW2{3577170584, 3302967107}, Hs.HsW2{3215898090, 2783053960}, Hs.HsW2{3235004314, 3126250640},
515    Hs.HsW2{4292911260, 953175288}, Hs.HsW2{3834979660, 1658957231}, Hs.HsW2{4094191583, 40090803}, Hs.HsW2{588210879, 3404420221},
516    Hs.HsW2{278741651, 1619136796}, Hs.HsW2{3494870281, 3671383436}, Hs.HsW2{1469788044, 4025245742}, Hs.HsW2{2138868336, 531940376},
517    Hs.HsW2{2765828154, 4292078047}, Hs.HsW2{2599487040, 2079371391}, Hs.HsW2{3723979615, 4104044877}, Hs.HsW2{1191603487, 2406379826},
518    Hs.HsW2{2261580793, 865952874}, Hs.HsW2{3851258928, 1682207847}, Hs.HsW2{4189090185, 740925554}, Hs.HsW2{608639702, 3635896639},
519    Hs.HsW2{293989359, 1713883348}, Hs.HsW2{3199605910, 2739392832}, Hs.HsW2{627028906, 3725768951}, Hs.HsW2{1078859126, 2637317232},
520    Hs.HsW2{3061202257, 2466666318}, Hs.HsW2{3348776947, 2819291602}, Hs.HsW2{1143901083, 2241595255}, Hs.HsW2{2646179369, 1772913981}]
521
522# T_6[b] = l(Pi(b) << 48): each entry's low and high 32 bits
523def hs.stb.t6.list() -> List<&2, Hs.HsW2>:
524  [Hs.HsW2{770062206, 3275783676}, Hs.HsW2{2753916791, 1537119214}, Hs.HsW2{1355302368, 2914357213}, Hs.HsW2{2807819654, 1377435409},
525    Hs.HsW2{3641384425, 896229839}, Hs.HsW2{632021047, 4220469358}, Hs.HsW2{3237349270, 2052719153}, Hs.HsW2{3790930443, 2638008854},
526    Hs.HsW2{1799936243, 207966459}, Hs.HsW2{671030370, 4118087876}, Hs.HsW2{1909145725, 1255366650}, Hs.HsW2{375827053, 1653646042},
527    Hs.HsW2{1228234655, 3800362019}, Hs.HsW2{1031570668, 3015903173}, Hs.HsW2{1748392450, 98712580}, Hs.HsW2{1822343080, 420195405},
528    Hs.HsW2{3800793338, 2495332073}, Hs.HsW2{1386002869, 2739914615}, Hs.HsW2{2512181624, 3430627824}, Hs.HsW2{216347363, 606514651},
529    Hs.HsW2{315510727, 2121872019}, Hs.HsW2{3958122775, 2869536558}, Hs.HsW2{4139374274, 4174468249}, Hs.HsW2{3213658461, 441825466},
530    Hs.HsW2{4218854021, 3683310871}, Hs.HsW2{2253973531, 3045011254}, Hs.HsW2{2403287542, 2328704753}, Hs.HsW2{2769228243, 1558427579},
531    Hs.HsW2{3589156618, 290311188}, Hs.HsW2{3977261288, 3105521613}, Hs.HsW2{3848136609, 2178237023}, Hs.HsW2{1430970094, 3055631297},
532    Hs.HsW2{1599337970, 2148814585}, Hs.HsW2{1840562444, 511084568}, Hs.HsW2{3680494012, 999369061}, Hs.HsW2{2548573485, 3263263066},
533    Hs.HsW2{478118257, 1420154850}, Hs.HsW2{3418706478, 1259492188}, Hs.HsW2{3198613497, 489200879}, Hs.HsW2{2100195998, 1861612065},
534    Hs.HsW2{2601326542, 3869760641}, Hs.HsW2{92445454, 462730268}, Hs.HsW2{1647276318, 869747004}, Hs.HsW2{4200391713, 3707238722},
535    Hs.HsW2{2138738379, 1611643531}, Hs.HsW2{444831886, 1186336513}, Hs.HsW2{231689287, 593201550}, Hs.HsW2{1485148841, 2507846223},
536    Hs.HsW2{1924514444, 1129591557}, Hs.HsW2{3921204546, 2784227204}, Hs.HsW2{874196225, 2356223490}, Hs.HsW2{1784850007, 186152110},
537    Hs.HsW2{117185023, 303290595}, Hs.HsW2{1302182453, 4268588138}, Hs.HsW2{390911177, 1710065295}, Hs.HsW2{3861079376, 2287087264},
538    Hs.HsW2{1546483459, 2308121094}, Hs.HsW2{4277404043, 3223218443}, Hs.HsW2{2327698168, 2438562541}, Hs.HsW2{3963244108, 3194444696},
539    Hs.HsW2{2196770225, 2845228927}, Hs.HsW2{2586274154, 3789224148}, Hs.HsW2{3700000487, 788518355}, Hs.HsW2{723136129, 3511919903},
540    Hs.HsW2{3599805947, 415932651}, Hs.HsW2{2990785818, 957231412}, Hs.HsW2{3757507606, 662223148}, Hs.HsW2{1763452070, 43980881},
541    Hs.HsW2{3423810933, 1585229802}, Hs.HsW2{2678452836, 4199435464}, Hs.HsW2{506166564, 1516216136}, Hs.HsW2{416769243, 1212958635},
542    Hs.HsW2{2712138873, 1074407410}, Hs.HsW2{2212131605, 2934676266}, Hs.HsW2{2038863668, 1914462824}, Hs.HsW2{3526903889, 69415074},
543    Hs.HsW2{929411056, 2247521021}, Hs.HsW2{1040320029, 3125046074}, Hs.HsW2{3280504167, 1943891662}, Hs.HsW2{4153649254, 4289491148},
544    Hs.HsW2{693031636, 3752455605}, Hs.HsW2{338843192, 1818946160}, Hs.HsW2{2353120007, 2202688014}, Hs.HsW2{800246571, 3451532630},
545    Hs.HsW2{3496784900, 182024200}, Hs.HsW2{3092966918, 255542284}, Hs.HsW2{1209999675, 3858352246}, Hs.HsW2{2311280649, 2564746770},
546    Hs.HsW2{3443084241, 1493273535}, Hs.HsW2{539589433, 3759928434}, Hs.HsW2{2470494343, 3731415315}, Hs.HsW2{2296981165, 2678311495},
547    Hs.HsW2{2215384142, 3146082204}, Hs.HsW2{492175317, 1406727095}, Hs.HsW2{3511077536, 228875357}, Hs.HsW2{3340787917, 1865744007},
548    Hs.HsW2{3480074116, 1476117269}, Hs.HsW2{4238409182, 3471057313}, Hs.HsW2{1618709835, 1026359702}, Hs.HsW2{2906834586, 1680640553},
549    Hs.HsW2{3185079560, 347074576}, Hs.HsW2{3938867123, 2893316987}, Hs.HsW2{3626066765, 840320410}, Hs.HsW2{157788653, 1068636615},
550    Hs.HsW2{3139726583, 112994547}, Hs.HsW2{651518662, 4060621969}, Hs.HsW2{3294552636, 1723044472}, Hs.HsW2{1059616953, 3174649711},
551    Hs.HsW2{2660207808, 4248004765}, Hs.HsW2{2954312015, 938768798}, Hs.HsW2{1876966745, 277659826}, Hs.HsW2{1098418390, 3662401969},
552    Hs.HsW2{4000231961, 2963084082}, Hs.HsW2{1720161460, 792648053}, Hs.HsW2{2000116098, 1489012505}, Hs.HsW2{2024597904, 1969309245},
553    Hs.HsW2{58622705, 159870207}, Hs.HsW2{2831179156, 2142780981}, Hs.HsW2{1710822981, 649704842}, Hs.HsW2{2557711679, 4011896958},
554    Hs.HsW2{187913656, 826823021}, Hs.HsW2{464119338, 1103833940}, Hs.HsW2{333721955, 2030311110}, Hs.HsW2{2173603648, 2685522816},
555    Hs.HsW2{1632760815, 978331075}, Hs.HsW2{4179781328, 3580925373}, Hs.HsW2{2732160648, 1233996557}, Hs.HsW2{892425125, 2332834391},
556    Hs.HsW2{1691576545, 566530527}, Hs.HsW2{3876133876, 2402224885}, Hs.HsW2{261861394, 765575460}, Hs.HsW2{751585754, 3292354985},
557    Hs.HsW2{1446272031, 3215349566}, Hs.HsW2{911200596, 2190169768}, Hs.HsW2{3772742831, 2588014147}, Hs.HsW2{2233887466, 3170386889},
558    Hs.HsW2{3032472805, 723380695}, Hs.HsW2{3739056818, 537238905}, Hs.HsW2{2923185259, 1839982294}, Hs.HsW2{3381767803, 1172839414},
559    Hs.HsW2{2892544062, 1666297468}, Hs.HsW2{1404487441, 2754798370}, Hs.HsW2{2434022610, 3499272633}, Hs.HsW2{781759887, 3402043651},
560    Hs.HsW2{677686384, 3637823968}, Hs.HsW2{2529319817, 3321648399}, Hs.HsW2{2419999350, 3622800876}, Hs.HsW2{2119233647, 1735565022},
561    Hs.HsW2{4031106877, 3938618490}, Hs.HsW2{1415618634, 2975604628}, Hs.HsW2{1543180376, 2633883312}, Hs.HsW2{3819044446, 2479266492},
562    Hs.HsW2{1246485870, 3942875356}, Hs.HsW2{4161280116, 3524112872}, Hs.HsW2{3082903060, 580551976}, Hs.HsW2{1939848232, 1143543632},
563    Hs.HsW2{1107692071, 3553410382}, Hs.HsW2{4109183639, 4130020403}, Hs.HsW2{3833043205, 2259183114}, Hs.HsW2{707809317, 3593371978},
564    Hs.HsW2{2693630685, 1198982055}, Hs.HsW2{2063078853, 2073759383}, Hs.HsW2{2850693936, 2026183264}, Hs.HsW2{984277943, 2796419955},
565    Hs.HsW2{832157199, 2548410910}, Hs.HsW2{0, 0}, Hs.HsW2{2649820721, 4105438306}, Hs.HsW2{2792461090, 1432673092},
566    Hs.HsW2{1504701453, 2449970714}, Hs.HsW2{2341971036, 2518984376}, Hs.HsW2{169421596, 909473080}, Hs.HsW2{3046482497, 744541570},
567    Hs.HsW2{3252451634, 2099717732}, Hs.HsW2{2861867457, 1900181151}, Hs.HsW2{998284563, 2714820390}, Hs.HsW2{3569635758, 372303937},
568    Hs.HsW2{1157239768, 3252643245}, Hs.HsW2{3169979308, 332584005}, Hs.HsW2{2456469027, 3642082630}, Hs.HsW2{139319113, 953105810},
569    Hs.HsW2{553846173, 3882274855}, Hs.HsW2{4292771631, 3345173854}, Hs.HsW2{19562148, 125641813}, Hs.HsW2{4050629017, 3988760623},
570    Hs.HsW2{970219846, 2938804108}, Hs.HsW2{3367751903, 1117077411}, Hs.HsW2{2492901340, 3406175653}, Hs.HsW2{3068862640, 635937149},
571    Hs.HsW2{1661276090, 883584361}, Hs.HsW2{2158293476, 2808936405}, Hs.HsW2{1323514052, 4159312021}, Hs.HsW2{612474515, 4243743803},
572    Hs.HsW2{1185869709, 3475320071}, Hs.HsW2{2750613548, 1324379992}, Hs.HsW2{1969464791, 1446694835}, Hs.HsW2{3460811040, 1351018304},
573    Hs.HsW2{3718510659, 696447366}, Hs.HsW2{1585023830, 2271832748}, Hs.HsW2{520160128, 1562557213}, Hs.HsW2{3541186293, 56497399},
574    Hs.HsW2{3665141528, 1022102832}, Hs.HsW2{2631626901, 4090044471}, Hs.HsW2{1461592763, 3101389675}, Hs.HsW2{1079178866, 3711366628},
575    Hs.HsW2{1373780804, 2865277832}, Hs.HsW2{956178402, 2824319961}, Hs.HsW2{1858749437, 401728743}, Hs.HsW2{1264690122, 3967722633},
576    Hs.HsW2{854013182, 2657273569}, Hs.HsW2{1126986883, 3568408859}, Hs.HsW2{2937469647, 1792459395}, Hs.HsW2{78177706, 485068873},
577    Hs.HsW2{1981622054, 1606263628}, Hs.HsW2{1287111825, 4178597951}, Hs.HsW2{1171287420, 3332522488}, Hs.HsW2{436017791, 1328636926},
578    Hs.HsW2{592968136, 3919353997}, Hs.HsW2{1560742311, 2397963859}, Hs.HsW2{39124053, 251283626}, Hs.HsW2{1012333128, 3032359824},
579    Hs.HsW2{2881412965, 1983861450}, Hs.HsW2{578652012, 4007771352}, Hs.HsW2{4080750028, 3813007493}, Hs.HsW2{3010051006, 1047729505},
580    Hs.HsW2{1739450896, 675544352}, Hs.HsW2{246533814, 719119729}, Hs.HsW2{4014263485, 3084924775}, Hs.HsW2{2383757138, 2377126564},
581    Hs.HsW2{3312753816, 1640937005}, Hs.HsW2{2572807067, 3898446891}, Hs.HsW2{3404672138, 1282373385}, Hs.HsW2{2372648355, 2218229339},
582    Hs.HsW2{2973583339, 814308811}, Hs.HsW2{3265461187, 1956661915}, Hs.HsW2{353904796, 1796722213}, Hs.HsW2{4061213544, 3828925648},
583    Hs.HsW2{3619345247, 532120766}, Hs.HsW2{1523674876, 2608921317}, Hs.HsW2{296799542, 2013159020}, Hs.HsW2{1199870249, 3361212754},
584    Hs.HsW2{3111162018, 138829913}, Hs.HsW2{3121484371, 29428902}, Hs.HsW2{2080640058, 1770575476}, Hs.HsW2{3322551913, 1749670610},
585    Hs.HsW2{1950997363, 1363667942}, Hs.HsW2{4253713274, 3382248948}, Hs.HsW2{869091930, 2569003700}, Hs.HsW2{1338590816, 4036441280},
586    Hs.HsW2{3901926374, 2727267281}, Hs.HsW2{4123481139, 4048959590}, Hs.HsW2{1893809881, 1303280559}, Hs.HsW2{2077387617, 2095459010},
587    Hs.HsW2{278573970, 1887664697}, Hs.HsW2{817088683, 2425917003}, Hs.HsW2{2272433855, 2986478435}, Hs.HsW2{131491675, 359595190}]
588
589# T_7[b] = l(Pi(b) << 56): each entry's low and high 32 bits
590def hs.stb.t7.list() -> List<&2, Hs.HsW2>:
591  [Hs.HsW2{2546151888, 3862910414}, Hs.HsW2{22788630, 632620720}, Hs.HsW2{3870137256, 3362811433}, Hs.HsW2{1565663082, 1531171703},
592    Hs.HsW2{1882525806, 200949079}, Hs.HsW2{721096294, 2878733335}, Hs.HsW2{2658808438, 4132135831}, Hs.HsW2{1688055115, 4119545186},
593    Hs.HsW2{2920055793, 1224197083}, Hs.HsW2{1123403973, 4281438566}, Hs.HsW2{474612885, 3417327836}, Hs.HsW2{3747752329, 1723398204},
594    Hs.HsW2{149076400, 901853417}, Hs.HsW2{4038283169, 2088114785}, Hs.HsW2{4060423821, 906040860}, Hs.HsW2{572110806, 2656357630},
595    Hs.HsW2{949225527, 2340262053}, Hs.HsW2{2393070859, 2631140184}, Hs.HsW2{2630638426, 3158077418}, Hs.HsW2{1831120621, 3858723643},
596    Hs.HsW2{259963090, 3471647454}, Hs.HsW2{2980795486, 3968172490}, Hs.HsW2{2415453981, 3110143464}, Hs.HsW2{2266652333, 2359309569},
597    Hs.HsW2{3604687407, 1993133669}, Hs.HsW2{2813689943, 1485043074}, Hs.HsW2{780852286, 1065084141}, Hs.HsW2{895277513, 266845702},
598    Hs.HsW2{487702147, 3993325164}, Hs.HsW2{163120038, 276051545}, Hs.HsW2{3028368400, 1574870912}, Hs.HsW2{45508908, 1249315965},
599    Hs.HsW2{3615526969, 1400490197}, Hs.HsW2{371119113, 3020321864}, Hs.HsW2{406574797, 1600016422}, Hs.HsW2{4106395129, 3902276251},
600    Hs.HsW2{173330588, 2142649492}, Hs.HsW2{2135664828, 3306626953}, Hs.HsW2{3005037938, 2800913847}, Hs.HsW2{1903078008, 776944615},
601    Hs.HsW2{2582000404, 224883104}, Hs.HsW2{3827036804, 2181522004}, Hs.HsW2{657711000, 789566132}, Hs.HsW2{3806087664, 1553888979},
602    Hs.HsW2{425749723, 2062243478}, Hs.HsW2{2990966628, 2202503943}, Hs.HsW2{1495518514, 3484273549}, Hs.HsW2{1536533534, 2245707760},
603    Hs.HsW2{1078174185, 3041303835}, Hs.HsW2{3651506941, 3089231035}, Hs.HsW2{2039223240, 462293774}, Hs.HsW2{2584469550, 1655012205},
604    Hs.HsW2{3088209912, 4243699603}, Hs.HsW2{3640535275, 2643782155}, Hs.HsW2{3949283926, 1290420362}, Hs.HsW2{3901266284, 589843015},
605    Hs.HsW2{2341025093, 764353810}, Hs.HsW2{851499179, 4106988593}, Hs.HsW2{3398512314, 3179054777}, Hs.HsW2{1035886713, 975605487},
606    Hs.HsW2{2007568652, 4040568672}, Hs.HsW2{2917224651, 657836310}, Hs.HsW2{2486100714, 2315083523}, Hs.HsW2{802252328, 449765981},
607    Hs.HsW2{1092099071, 2431884203}, Hs.HsW2{3728315295, 1124990604}, Hs.HsW2{3358017430, 4144728772}, Hs.HsW2{3322037586, 475246250},
608    Hs.HsW2{4083063963, 330567852}, Hs.HsW2{1241162319, 2771561282}, Hs.HsW2{1650071103, 722620901}, Hs.HsW2{3662168519, 3622037110},
609    Hs.HsW2{3846195346, 2813486308}, Hs.HsW2{1135506131, 3666122710}, Hs.HsW2{2708618019, 2249908485}, Hs.HsW2{2432993956, 950419785},
610    Hs.HsW2{629520052, 1702420169}, Hs.HsW2{2897930973, 41996198}, Hs.HsW2{3262355210, 2294134352}, Hs.HsW2{3154085058, 2469641566},
611    Hs.HsW2{1205837963, 1315606316}, Hs.HsW2{3077369642, 840734029}, Hs.HsW2{1921218882, 1099772202}, Hs.HsW2{4291688307, 2996517055},
612    Hs.HsW2{4178201607, 1812081720}, Hs.HsW2{185559690, 1510160932}, Hs.HsW2{1021696623, 529762399}, Hs.HsW2{2526579654, 3280622462},
613    Hs.HsW2{3344564036, 971417626}, Hs.HsW2{3470851298, 697474627}, Hs.HsW2{618532002, 1087232121}, Hs.HsW2{2728388633, 3923307464},
614    Hs.HsW2{3485157108, 203921651}, Hs.HsW2{1045672771, 1441039394}, Hs.HsW2{3440193496, 1179686030}, Hs.HsW2{309266001, 552103090},
615    Hs.HsW2{2941729255, 1833092459}, Hs.HsW2{1523457544, 2691678528}, Hs.HsW2{1329404219, 2074853317}, Hs.HsW2{2288313983, 1112348639},
616    Hs.HsW2{4011104270, 3624163440}, Hs.HsW2{2242656129, 3335993724}, Hs.HsW2{1144157105, 564692449}, Hs.HsW2{2302631017, 1744310639},
617    Hs.HsW2{1460064246, 620097507}, Hs.HsW2{1995615002, 3580045776}, Hs.HsW2{1315349293, 1579071861}, Hs.HsW2{2562558210, 684881680},
618    Hs.HsW2{2113782160, 2405438452}, Hs.HsW2{3057079612, 396989437}, Hs.HsW2{2114982570, 3768719673}, Hs.HsW2{3050997254, 2020317488},
619    Hs.HsW2{1437640410, 1854071710}, Hs.HsW2{4147072707, 2270824534}, Hs.HsW2{2757251949, 927072079}, Hs.HsW2{2507495676, 2890422707},
620    Hs.HsW2{1544136060, 2130105799}, Hs.HsW2{1820267771, 3226105227}, Hs.HsW2{2871454655, 4188855697}, Hs.HsW2{3320813160, 1938924647},
621    Hs.HsW2{3778124490, 861699102}, Hs.HsW2{2252465339, 2836738993}, Hs.HsW2{997841677, 3837762152}, Hs.HsW2{731952240, 2384525991},
622    Hs.HsW2{2067430116, 1375274867}, Hs.HsW2{3201690764, 577282836}, Hs.HsW2{3108629998, 3645157667}, Hs.HsW2{1300983831, 836547512},
623    Hs.HsW2{2669774944, 3556664615}, Hs.HsW2{3700423347, 159052529}, Hs.HsW2{825035665, 2601101052}, Hs.HsW2{2747552271, 3429756280},
624    Hs.HsW2{1589627984, 880925114}, Hs.HsW2{293786987, 1328178815}, Hs.HsW2{1352322708, 3755605460}, Hs.HsW2{4223411499, 645210181},
625    Hs.HsW2{1714144359, 3220982047}, Hs.HsW2{4229964873, 3713610354}, Hs.HsW2{3563930371, 1018937880}, Hs.HsW2{390426143, 2444456696},
626    Hs.HsW2{3160638880, 1746906985}, Hs.HsW2{3131326164, 3062283246}, Hs.HsW2{1288751617, 342471944}, Hs.HsW2{3419051180, 2563342345},
627    Hs.HsW2{1943585620, 1681405850}, Hs.HsW2{3234201126, 3268065837}, Hs.HsW2{2027399646, 1044057534}, Hs.HsW2{761728772, 1354362400},
628    Hs.HsW2{938127589, 1167110779}, Hs.HsW2{917572339, 1613083851}, Hs.HsW2{127664482, 4213969463}, Hs.HsW2{210988008, 2704222227},
629    Hs.HsW2{1424694476, 1261954350}, Hs.HsW2{2329055059, 138025890}, Hs.HsW2{975331611, 3238698200}, Hs.HsW2{1950663222, 2668897709},
630    Hs.HsW2{3922928506, 110972151}, Hs.HsW2{3891667390, 3989137561}, Hs.HsW2{2156289999, 2005673782}, Hs.HsW2{467011063, 815553259},
631    Hs.HsW2{3511102285, 2380323922}, Hs.HsW2{4252737119, 4176229570}, Hs.HsW2{1484289828, 3927493949}, Hs.HsW2{2091285382, 2866091332},
632    Hs.HsW2{2643976524, 2575919450}, Hs.HsW2{0, 0}, Hs.HsW2{569664748, 4053190195}, Hs.HsW2{1767210165, 1896967105},
633    Hs.HsW2{1871890369, 2944958278}, Hs.HsW2{4271263077, 2536390159}, Hs.HsW2{3577149717, 420398248}, Hs.HsW2{1378658232, 2511270313},
634    Hs.HsW2{2860339625, 3692682017}, Hs.HsW2{74568280, 2498631930}, Hs.HsW2{1218517081, 2156375538}, Hs.HsW2{689364316, 3294099162},
635    Hs.HsW2{1371632770, 4201446244}, Hs.HsW2{3675519953, 4065779910}, Hs.HsW2{282685309, 1788829903}, Hs.HsW2{3174580150, 1303030233},
636    Hs.HsW2{4209483581, 62924533}, Hs.HsW2{113752948, 3734574215}, Hs.HsW2{872899551, 710064310}, Hs.HsW2{65917754, 1874987725},
637    Hs.HsW2{548396794, 3559112835}, Hs.HsW2{591531456, 3152136782}, Hs.HsW2{2831890565, 2523846492}, Hs.HsW2{237306564, 3948422254},
638    Hs.HsW2{322223175, 90008066}, Hs.HsW2{531093423, 2758951441}, Hs.HsW2{2230816151, 3814866892}, Hs.HsW2{519859641, 2177320097},
639    Hs.HsW2{969912865, 2932381205}, Hs.HsW2{2370735665, 4078307733}, Hs.HsW2{3428226510, 1675989566}, Hs.HsW2{2605734456, 1192263133},
640    Hs.HsW2{2687074613, 2746214325}, Hs.HsW2{3817337830, 2032889955}, Hs.HsW2{1448965600, 21031251}, Hs.HsW2{2768497019, 318044671},
641    Hs.HsW2{742176018, 1963780240}, Hs.HsW2{368248627, 3687087749}, Hs.HsW2{1790488463, 517169420}, Hs.HsW2{2178803161, 1379475846},
642    Hs.HsW2{3534420087, 3793933983}, Hs.HsW2{346602789, 4268849205}, Hs.HsW2{1243050357, 3404767631}, Hs.HsW2{1626111763, 1634033048},
643    Hs.HsW2{3248374832, 3883908253}, Hs.HsW2{3721674917, 751825985}, Hs.HsW2{3765051612, 384400046}, Hs.HsW2{3491533147, 2824198882},
644    Hs.HsW2{2422157490, 487802873}, Hs.HsW2{3975760692, 3083227837}, Hs.HsW2{1707480925, 3493741522}, Hs.HsW2{3998163480, 4256259776},
645    Hs.HsW2{2464766366, 1466190724}, Hs.HsW2{3213776538, 131966372}, Hs.HsW2{1745798819, 1420062065}, Hs.HsW2{3300142206, 1445241559},
646    Hs.HsW2{813085063, 3200032844}, Hs.HsW2{2800630337, 2100753202}, Hs.HsW2{1810044313, 996566972}, Hs.HsW2{3929993280, 1767851578},
647    Hs.HsW2{3274190108, 2903027936}, Hs.HsW2{86665294, 2975538762}, Hs.HsW2{1639433477, 1154505512}, Hs.HsW2{445497313, 355032155},
648    Hs.HsW2{2053226738, 1951138243}, Hs.HsW2{4058576311, 1505959121}, Hs.HsW2{1263324003, 4014319423}, Hs.HsW2{1183062685, 1809811868},
649    Hs.HsW2{2184197859, 1039870795}, Hs.HsW2{4134859989, 2733575910}, Hs.HsW2{2204863733, 407776763}, Hs.HsW2{1608808006, 288677642},
650    Hs.HsW2{1964996640, 3131122461}, Hs.HsW2{865821373, 3514739329}, Hs.HsW2{1400315310, 2954622745}, Hs.HsW2{231264766, 2224696995},
651    Hs.HsW2{1057491285, 1884390034}, Hs.HsW2{1661053993, 245847893}, Hs.HsW2{1164560807, 69043025}, Hs.HsW2{644375950, 180016132},
652    Hs.HsW2{4166120977, 1236740744}, Hs.HsW2{1858698711, 2319284726}, Hs.HsW2{4120455151, 3442279467}, Hs.HsW2{2968579656, 3375400826},
653    Hs.HsW2{3986878754, 2457031693}, Hs.HsW2{3555803745, 3348615215}, Hs.HsW2{676161354, 3789746282}, Hs.HsW2{3380411776, 3535703156},
654    Hs.HsW2{1735425649, 2588495791}, Hs.HsW2{2844820115, 3017527788}, Hs.HsW2{2477974408, 1926319412}, Hs.HsW2{2350199847, 3601010469}]
655
656def HsStreebog.tables() -> HsStbTabs:
657  HsStbTabs{hs.stb.tab(hs.stb.t0.list()), hs.stb.tab(hs.stb.t1.list()), hs.stb.tab(hs.stb.t2.list()), hs.stb.tab(hs.stb.t3.list()), hs.stb.tab(hs.stb.t4.list()), hs.stb.tab(hs.stb.t5.list()), hs.stb.tab(hs.stb.t6.list()), hs.stb.tab(hs.stb.t7.list())}
658# END GENERATED: tables
659
660# BEGIN GENERATED by gen/streebog.py: consts
661def hs.stb.c1() -> Hs.HsW16:
662  Hs.HsW16{4070982919, 3716179289, 3430173987, 91649078, 2757808917, 2722245128, 2456250625, 1266475153, 1971700988, 1900984461, 776327190, 795506243, 3227876383, 3955961729, 516610793, 2970115034}
663
664def hs.stb.c2() -> Hs.HsW16:
665  Hs.HsW16{565287863, 3866690672, 3620457814, 1440588315, 3674908618, 1555390914, 316053848, 2595559275, 380961073, 1641373199, 170077080, 4093569650, 259044823, 1340316998, 2845650714, 1872999818}
666
667def hs.stb.c3() -> Hs.HsW16:
668  Hs.HsW16{179964594, 2568918773, 2256198449, 3266769987, 1617091337, 3251190327, 2419433137, 3554807780, 2972285819, 4075451668, 1385963403, 116481631, 1782416437, 171572264, 734932935, 4118076588}
669
670def hs.stb.c4() -> Hs.HsW16:
671  Hs.HsW16{2229522734, 571260604, 2481469425, 877914785, 2471625662, 3635876659, 3976451701, 2849451138, 1751004479, 2641501357, 861682813, 1217299838, 1567745245, 4182303136, 3893716690, 4011843507}
672
673def hs.stb.c5() -> Hs.HsW16:
674  Hs.HsW16{2087517783, 1612142845, 2850710517, 2052498046, 589765142, 3758031031, 624620963, 3217889095, 2148532157, 899560919, 377884746, 2132089887, 1823023971, 2587836684, 2907129753, 1273654188}
675
676def hs.stb.c6() -> Hs.HsW16:
677  Hs.HsW16{1180990830, 4201136250, 915427125, 3211904370, 3267282614, 183639910, 479901620, 3489310391, 2599456454, 411015860, 1363321964, 761709817, 2049980864, 1873068859, 490394585, 2924457646}
678
679def hs.stb.c7() -> Hs.HsW16:
680  Hs.HsW16{974443667, 2290505293, 2721860339, 890717516, 675939588, 105343363, 763505719, 160607173, 427463625, 3544661555, 3871311817, 966706887, 3206809940, 1370261246, 4004169196, 4106685974}
681
682def hs.stb.c8() -> Hs.HsW16:
683  Hs.HsW16{3204638494, 2759790036, 1498523865, 917291573, 3517301807, 1775340843, 2459633296, 4102630347, 1306248346, 2310292539, 2620841502, 1320679537, 208552257, 65513986, 1301531047, 2602523458}
684
685def hs.stb.c9() -> Hs.HsW16:
686  Hs.HsW16{2200132315, 1918977105, 3407817312, 238607506, 2785516628, 2066451098, 3685928625, 2148156427, 3758950788, 1020876215, 629752356, 981285403, 3960889310, 2488048344, 372318875, 932141652}
687
688def hs.stb.c10() -> Hs.HsW16:
689  Hs.HsW16{2554698989, 1958004731, 356234947, 915995345, 997610228, 2048814128, 2942907211, 2682742530, 456352003, 536863114, 4287264987, 2302797596, 3001349107, 942335304, 2147839826, 2881412774}
690
691def hs.stb.c11() -> Hs.HsW16:
692  Hs.HsW16{2180197659, 1808442573, 3228555357, 3735181642, 2101833368, 4021996829, 3930634698, 2317185519, 344221305, 536969249, 3953854305, 3640290235, 1666907796, 805488333, 4022897147, 2077073104}
693
694def hs.stb.c12() -> Hs.HsW16:
695  Hs.HsW16{4045133600, 1220317770, 3652328345, 4210300885, 2296457298, 3877479594, 412208262, 1568731037, 807509915, 4162851540, 3168738679, 3450092594, 71938426, 3524493488, 4044763578, 932112231}
696# END GENERATED: consts
697
698# BEGIN GENERATED by gen/streebog.py: lps
699# LPS(x): chunk k of the result is the XOR over j of T_j[byte k of chunk j]
700def hs.stb.lps(+t: HsStbTabs, x: Hs.HsW16) -> Hs.HsW16:
701  match t x:
702    case HsStbTabs{+t0, +t1, +t2, +t3, +t4, +t5, +t6, +t7} Hs.HsW16{+x0, +x1, +x2, +x3, +x4, +x5, +x6, +x7, +x8, +x9, +x10, +x11, +x12, +x13, +x14, +x15}:
703      +o0 = hs.stb.x8(hs.stb.get(t0, U32.and(255, x0)), hs.stb.get(t1, U32.and(255, x2)), hs.stb.get(t2, U32.and(255, x4)), hs.stb.get(t3, U32.and(255, x6)), hs.stb.get(t4, U32.and(255, x8)), hs.stb.get(t5, U32.and(255, x10)), hs.stb.get(t6, U32.and(255, x12)), hs.stb.get(t7, U32.and(255, x14)))
704      +o1 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x0, 8n))), hs.stb.get(t1, U32.and(255, U32.shrn(x2, 8n))), hs.stb.get(t2, U32.and(255, U32.shrn(x4, 8n))), hs.stb.get(t3, U32.and(255, U32.shrn(x6, 8n))), hs.stb.get(t4, U32.and(255, U32.shrn(x8, 8n))), hs.stb.get(t5, U32.and(255, U32.shrn(x10, 8n))), hs.stb.get(t6, U32.and(255, U32.shrn(x12, 8n))), hs.stb.get(t7, U32.and(255, U32.shrn(x14, 8n))))
705      +o2 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x0, 16n))), hs.stb.get(t1, U32.and(255, U32.shrn(x2, 16n))), hs.stb.get(t2, U32.and(255, U32.shrn(x4, 16n))), hs.stb.get(t3, U32.and(255, U32.shrn(x6, 16n))), hs.stb.get(t4, U32.and(255, U32.shrn(x8, 16n))), hs.stb.get(t5, U32.and(255, U32.shrn(x10, 16n))), hs.stb.get(t6, U32.and(255, U32.shrn(x12, 16n))), hs.stb.get(t7, U32.and(255, U32.shrn(x14, 16n))))
706      +o3 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x0, 24n))), hs.stb.get(t1, U32.and(255, U32.shrn(x2, 24n))), hs.stb.get(t2, U32.and(255, U32.shrn(x4, 24n))), hs.stb.get(t3, U32.and(255, U32.shrn(x6, 24n))), hs.stb.get(t4, U32.and(255, U32.shrn(x8, 24n))), hs.stb.get(t5, U32.and(255, U32.shrn(x10, 24n))), hs.stb.get(t6, U32.and(255, U32.shrn(x12, 24n))), hs.stb.get(t7, U32.and(255, U32.shrn(x14, 24n))))
707      +o4 = hs.stb.x8(hs.stb.get(t0, U32.and(255, x1)), hs.stb.get(t1, U32.and(255, x3)), hs.stb.get(t2, U32.and(255, x5)), hs.stb.get(t3, U32.and(255, x7)), hs.stb.get(t4, U32.and(255, x9)), hs.stb.get(t5, U32.and(255, x11)), hs.stb.get(t6, U32.and(255, x13)), hs.stb.get(t7, U32.and(255, x15)))
708      +o5 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x1, 8n))), hs.stb.get(t1, U32.and(255, U32.shrn(x3, 8n))), hs.stb.get(t2, U32.and(255, U32.shrn(x5, 8n))), hs.stb.get(t3, U32.and(255, U32.shrn(x7, 8n))), hs.stb.get(t4, U32.and(255, U32.shrn(x9, 8n))), hs.stb.get(t5, U32.and(255, U32.shrn(x11, 8n))), hs.stb.get(t6, U32.and(255, U32.shrn(x13, 8n))), hs.stb.get(t7, U32.and(255, U32.shrn(x15, 8n))))
709      +o6 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x1, 16n))), hs.stb.get(t1, U32.and(255, U32.shrn(x3, 16n))), hs.stb.get(t2, U32.and(255, U32.shrn(x5, 16n))), hs.stb.get(t3, U32.and(255, U32.shrn(x7, 16n))), hs.stb.get(t4, U32.and(255, U32.shrn(x9, 16n))), hs.stb.get(t5, U32.and(255, U32.shrn(x11, 16n))), hs.stb.get(t6, U32.and(255, U32.shrn(x13, 16n))), hs.stb.get(t7, U32.and(255, U32.shrn(x15, 16n))))
710      +o7 = hs.stb.x8(hs.stb.get(t0, U32.and(255, U32.shrn(x1, 24n))), hs.stb.get(t1, U32.and(255, U32.shrn(x3, 24n))), hs.stb.get(t2, U32.and(255, U32.shrn(x5, 24n))), hs.stb.get(t3, U32.and(255, U32.shrn(x7, 24n))), hs.stb.get(t4, U32.and(255, U32.shrn(x9, 24n))), hs.stb.get(t5, U32.and(255, U32.shrn(x11, 24n))), hs.stb.get(t6, U32.and(255, U32.shrn(x13, 24n))), hs.stb.get(t7, U32.and(255, U32.shrn(x15, 24n))))
711      hs.stb.join(o0, o1, o2, o3, o4, o5, o6, o7)
712# END GENERATED: lps
713
714# 512-bit vectors: X[k] (XOR) and addition modulo 2^512
715
716def hs.stb.xor(a: Hs.HsW16, b: Hs.HsW16) -> Hs.HsW16:
717  match a b:
718    case Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15} Hs.HsW16{b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15}:
719      Hs.HsW16{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3), U32.xor(a4, b4), U32.xor(a5, b5), U32.xor(a6, b6), U32.xor(a7, b7), U32.xor(a8, b8), U32.xor(a9, b9), U32.xor(a10, b10), U32.xor(a11, b11), U32.xor(a12, b12), U32.xor(a13, b13), U32.xor(a14, b14), U32.xor(a15, b15)}
720
721def hs.stb.words(a: Hs.HsW16) -> List<&2, U32>:
722  match a:
723    case Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}:
724      [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]
725
726def hs.stb.of_words(xs: List<&2, U32>) -> Hs.HsW16:
727  match xs:
728    case [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]:
729      Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}
730    case _:
731      Hs.HsW16{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}
732
733def hs.stb.bit(b: Bool) -> U32:
734  match b:
735    case True{}:
736      1
737    case False{}:
738      0
739
740# the words of x + y + c (c a carry, 0 or 1), least significant first,
741# modulo 2^(32 n)
742def hs.stb.add.go(xs: List<&2, U32>, ys: List<&2, U32>, +c: U32) -> List<&2, U32>:
743  match xs ys:
744    case Con{+x, xt} Con{y, yt}:
745      +t = U32.add(x, y)
746      +s = U32.add(t, c)
747      Con{s, hs.stb.add.go(xt, yt, U32.or(hs.stb.bit(U32.is_lt(t, x)), hs.stb.bit(U32.is_lt(s, t))))}
748    case _ _:
749      Nil{}
750
751def hs.stb.add(a: Hs.HsW16, b: Hs.HsW16) -> Hs.HsW16:
752  hs.stb.of_words(hs.stb.add.go(hs.stb.words(a), hs.stb.words(b), 0))
753
754# the 512-bit vector of a number below 2^32
755def hs.stb.small(v: U32) -> Hs.HsW16:
756  Hs.HsW16{v, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}
757
758def hs.stb.zero() -> Hs.HsW16:
759  hs.stb.small(0)
760
761# The compression function
762
763def hs.stb.cs() -> List<&2, Hs.HsW16>:
764  [hs.stb.c1(), hs.stb.c2(), hs.stb.c3(), hs.stb.c4(), hs.stb.c5(), hs.stb.c6(), hs.stb.c7(), hs.stb.c8(), hs.stb.c9(), hs.stb.c10(), hs.stb.c11(), hs.stb.c12()]
765
766# E's rounds: x the data so far, k the round key; then the last key added
767def hs.stb.rounds(cs: List<&2, Hs.HsW16>, +t: HsStbTabs, +k: Hs.HsW16, x: Hs.HsW16) -> Hs.HsW16:
768  match cs:
769    case Nil{}:
770      hs.stb.xor(x, k)
771    case Con{c, rest}:
772      hs.stb.rounds(rest, t, hs.stb.lps(t, hs.stb.xor(k, c)), hs.stb.lps(t, hs.stb.xor(x, k)))
773
774# g_N(h, m)
775def hs.stb.g(+t: HsStbTabs, n: Hs.HsW16, +h: Hs.HsW16, +m: Hs.HsW16) -> Hs.HsW16:
776  hs.stb.xor(hs.stb.xor(hs.stb.rounds(hs.stb.cs(), t, hs.stb.lps(t, hs.stb.xor(h, n)), m), h), m)
777
778# One 64-byte block of stage 2: h = g_N(h, m), N += 512, Sigma += m
779def hs.stb.compress.of(cv: HsStbCv, +m: Hs.HsW16) -> HsStbCv:
780  match cv:
781    case HsStbCv{h, +n, s, +t}:
782      HsStbCv{hs.stb.g(t, n, h, m), hs.stb.add(n, hs.stb.small(512)), hs.stb.add(s, m), t}
783
784# (a block of another length gives zeros, as Hs.hs.block.le does: the engine
785# passes only whole blocks)
786def HsStreebog.compress(cv: HsStbCv, blk: List<&2, U32>) -> HsStbCv:
787  hs.stb.compress.of(cv, Hs.hs.block.le(blk))
788
789# Stage 3 on the chaining value: the last block m (its cnt bytes, then 1,
790# then zeros), N += 8 cnt, Sigma += m, then g_0(h, N) and g_0(h, Sigma)
791def hs.stb.finish.of(cv: HsStbCv, +m: Hs.HsW16, cnt: U32) -> Hs.HsW16:
792  match cv:
793    case HsStbCv{h, +n, s, +t}:
794      +h1 = hs.stb.g(t, n, h, m)
795      +h2 = hs.stb.g(t, hs.stb.zero(), h1, hs.stb.add(n, hs.stb.small(U32.shln(cnt, 3n))))
796      hs.stb.g(t, hs.stb.zero(), h2, hs.stb.add(s, m))
797
798def hs.stb.finish(+st: Hs.HsMdState<HsStbCv>) -> Hs.HsW16:
799  +cnt = Hs.HsMd.count(~HsStbCv, st)
800  hs.stb.finish.of(Hs.HsMd.cv(~HsStbCv, st), Hs.hs.block.le(B.append(Hs.HsMd.pending(~HsStbCv, st), Con{1, B.zeros(U32.to_nat(U32.sub(63, cnt)))})), cnt)
801
802# the digests' bytes: all 64 (Streebog-512), or the most significant 32,
803# bytes 32 to 63 (Streebog-256)
804def hs.stb.out512(x: Hs.HsW16) -> B.Octets:
805  match x:
806    case Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}:
807      B.Octets.of_list(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))))))))))
808
809def hs.stb.out256(x: Hs.HsW16) -> B.Octets:
810  match x:
811    case Hs.HsW16{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}:
812      B.Octets.of_list(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15)))))))))
813
814# The transformations on 512-bit vectors as 64-byte strings, byte i a_i (a
815# shorter string is a number's low bytes, zeros above; bytes past 64 are
816# ignored): LPS, and the compression function g_N(h, m) (RFC 6986,
817# sections 7 and 8)
818def hs.stb.v512(o: B.Octets) -> Hs.HsW16:
819  Hs.hs.block.le(B.take(64n, B.append(B.Octets.to_list(o), B.zeros(64n))))
820
821def HsStreebog.lps(x: B.Octets) -> B.Octets:
822  hs.stb.out512(hs.stb.lps(HsStreebog.tables(), hs.stb.v512(x)))
823
824def HsStreebog.g(n: B.Octets, h: B.Octets, m: B.Octets) -> B.Octets:
825  hs.stb.out512(hs.stb.g(HsStreebog.tables(), hs.stb.v512(n), hs.stb.v512(h), hs.stb.v512(m)))
826
827# The interface
828
829def HsStreebog.init512() -> Hs.HsMdState<HsStbCv>:
830  Hs.HsMd.start(~HsStbCv, HsStbCv{hs.stb.zero(), hs.stb.zero(), hs.stb.zero(), HsStreebog.tables()})
831
832def HsStreebog.init256() -> Hs.HsMdState<HsStbCv>:
833  Hs.HsMd.start(~HsStbCv, HsStbCv{Hs.HsW16{16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009, 16843009}, hs.stb.zero(), hs.stb.zero(), HsStreebog.tables()})
834
835# the state after more bytes (either digest size: init chooses)
836def HsStreebog.update(s: Hs.HsMdState<HsStbCv>, o: B.Octets) -> Hs.HsMdState<HsStbCv>:
837  Hs.HsMd.update(~HsStbCv, ~HsStreebog.compress, ~63, s, o)
838
839# the digests of the bytes so far (a state from init512 for final512, from
840# init256 for final256)
841def HsStreebog.final512(s: Hs.HsMdState<HsStbCv>) -> B.Octets:
842  hs.stb.out512(hs.stb.finish(s))
843
844def HsStreebog.final256(s: Hs.HsMdState<HsStbCv>) -> B.Octets:
845  hs.stb.out256(hs.stb.finish(s))
846
847# The digests in one call
848def HsStreebog.digest512(o: B.Octets) -> B.Octets:
849  HsStreebog.final512(HsStreebog.update(HsStreebog.init512(), o))
850
851def HsStreebog.digest256(o: B.Octets) -> B.Octets:
852  HsStreebog.final256(HsStreebog.update(HsStreebog.init256(), o))