File tree Expand file tree Collapse file tree 3 files changed +440
-81
lines changed
src/lean_spec/subspecs/poseidon2
tests/lean_spec/subspecs/poseidon2 Expand file tree Collapse file tree 3 files changed +440
-81
lines changed Original file line number Diff line number Diff line change 1+ """Round constants for the Poseidon2 permutation over the KoalaBear field."""
2+
3+ from typing import List
4+
5+ from ..koalabear .field import Fp
6+
7+ _RAW_CONSTANTS_16 : List [int ] = [
8+ 2128964168 ,
9+ 288780357 ,
10+ 316938561 ,
11+ 2126233899 ,
12+ 426817493 ,
13+ 1714118888 ,
14+ 1045008582 ,
15+ 1738510837 ,
16+ 889721787 ,
17+ 8866516 ,
18+ 681576474 ,
19+ 419059826 ,
20+ 1596305521 ,
21+ 1583176088 ,
22+ 1584387047 ,
23+ 1529751136 ,
24+ 1863858111 ,
25+ 1072044075 ,
26+ 517831365 ,
27+ 1464274176 ,
28+ 1138001621 ,
29+ 428001039 ,
30+ 245709561 ,
31+ 1641420379 ,
32+ 1365482496 ,
33+ 770454828 ,
34+ 693167409 ,
35+ 757905735 ,
36+ 136670447 ,
37+ 436275702 ,
38+ 525466355 ,
39+ 1559174242 ,
40+ 1030087950 ,
41+ 869864998 ,
42+ 322787870 ,
43+ 267688717 ,
44+ 948964561 ,
45+ 740478015 ,
46+ 679816114 ,
47+ 113662466 ,
48+ 2066544572 ,
49+ 1744924186 ,
50+ 367094720 ,
51+ 1380455578 ,
52+ 1842483872 ,
53+ 416711434 ,
54+ 1342291586 ,
55+ 1692058446 ,
56+ 1493348999 ,
57+ 1113949088 ,
58+ 210900530 ,
59+ 1071655077 ,
60+ 610242121 ,
61+ 1136339326 ,
62+ 2020858841 ,
63+ 1019840479 ,
64+ 678147278 ,
65+ 1678413261 ,
66+ 1361743414 ,
67+ 61132629 ,
68+ 1209546658 ,
69+ 64412292 ,
70+ 1936878279 ,
71+ 1980661727 ,
72+ 1423960925 ,
73+ 2101391318 ,
74+ 1915532054 ,
75+ 275400051 ,
76+ 1168624859 ,
77+ 1141248885 ,
78+ 356546469 ,
79+ 1165250474 ,
80+ 1320543726 ,
81+ 932505663 ,
82+ 1204226364 ,
83+ 1452576828 ,
84+ 1774936729 ,
85+ 926808140 ,
86+ 1184948056 ,
87+ 1186493834 ,
88+ 843181003 ,
89+ 185193011 ,
90+ 452207447 ,
91+ 510054082 ,
92+ 1139268644 ,
93+ 630873441 ,
94+ 669538875 ,
95+ 462500858 ,
96+ 876500520 ,
97+ 1214043330 ,
98+ 383937013 ,
99+ 375087302 ,
100+ 636912601 ,
101+ 307200505 ,
102+ 390279673 ,
103+ 1999916485 ,
104+ 1518476730 ,
105+ 1606686591 ,
106+ 1410677749 ,
107+ 1581191572 ,
108+ 1004269969 ,
109+ 143426723 ,
110+ 1747283099 ,
111+ 1016118214 ,
112+ 1749423722 ,
113+ 66331533 ,
114+ 1177761275 ,
115+ 1581069649 ,
116+ 1851371119 ,
117+ 852520128 ,
118+ 1499632627 ,
119+ 1820847538 ,
120+ 150757557 ,
121+ 884787840 ,
122+ 619710451 ,
123+ 1651711087 ,
124+ 505263814 ,
125+ 212076987 ,
126+ 1482432120 ,
127+ 1458130652 ,
128+ 382871348 ,
129+ 417404007 ,
130+ 2066495280 ,
131+ 1996518884 ,
132+ 902934924 ,
133+ 582892981 ,
134+ 1337064375 ,
135+ 1199354861 ,
136+ 2102596038 ,
137+ 1533193853 ,
138+ 1436311464 ,
139+ 2012303432 ,
140+ 839997195 ,
141+ 1225781098 ,
142+ 2011967775 ,
143+ 575084315 ,
144+ 1309329169 ,
145+ 786393545 ,
146+ 995788880 ,
147+ 1702925345 ,
148+ 1444525226 ,
149+ 908073383 ,
150+ 1811535085 ,
151+ 1531002367 ,
152+ 1635653662 ,
153+ 1585100155 ,
154+ 867006515 ,
155+ 879151050 ,
156+ ]
157+
158+ _RAW_CONSTANTS_24 : List [int ] = [
159+ 487143900 ,
160+ 1829048205 ,
161+ 1652578477 ,
162+ 646002781 ,
163+ 1044144830 ,
164+ 53279448 ,
165+ 1519499836 ,
166+ 22697702 ,
167+ 1768655004 ,
168+ 230479744 ,
169+ 1484895689 ,
170+ 705130286 ,
171+ 1429811285 ,
172+ 1695785093 ,
173+ 1417332623 ,
174+ 1115801016 ,
175+ 1048199020 ,
176+ 878062617 ,
177+ 738518649 ,
178+ 249004596 ,
179+ 1601837737 ,
180+ 24601614 ,
181+ 245692625 ,
182+ 364803730 ,
183+ 1857019234 ,
184+ 1906668230 ,
185+ 1916890890 ,
186+ 835590867 ,
187+ 557228239 ,
188+ 352829675 ,
189+ 515301498 ,
190+ 973918075 ,
191+ 954515249 ,
192+ 1142063750 ,
193+ 1795549558 ,
194+ 608869266 ,
195+ 1850421928 ,
196+ 2028872854 ,
197+ 1197543771 ,
198+ 1027240055 ,
199+ 1976813168 ,
200+ 963257461 ,
201+ 652017844 ,
202+ 2113212249 ,
203+ 213459679 ,
204+ 90747280 ,
205+ 1540619478 ,
206+ 324138382 ,
207+ 1377377119 ,
208+ 294744504 ,
209+ 512472871 ,
210+ 668081958 ,
211+ 907306515 ,
212+ 518526882 ,
213+ 1907091534 ,
214+ 1152942192 ,
215+ 1572881424 ,
216+ 720020214 ,
217+ 729527057 ,
218+ 1762035789 ,
219+ 86171731 ,
220+ 205890068 ,
221+ 453077400 ,
222+ 1201344594 ,
223+ 986483134 ,
224+ 125174298 ,
225+ 2050269685 ,
226+ 1895332113 ,
227+ 749706654 ,
228+ 40566555 ,
229+ 742540942 ,
230+ 1735551813 ,
231+ 162985276 ,
232+ 1943496073 ,
233+ 1469312688 ,
234+ 703013107 ,
235+ 1979485151 ,
236+ 1278193166 ,
237+ 548674995 ,
238+ 2118718736 ,
239+ 749596440 ,
240+ 1476142294 ,
241+ 1293606474 ,
242+ 918523452 ,
243+ 890353212 ,
244+ 1691895663 ,
245+ 1932240646 ,
246+ 1180911992 ,
247+ 86098300 ,
248+ 1592168978 ,
249+ 895077289 ,
250+ 724819849 ,
251+ 1697986774 ,
252+ 1608418116 ,
253+ 1083269213 ,
254+ 691256798 ,
255+ 328586442 ,
256+ 1572520009 ,
257+ 1375479591 ,
258+ 322991001 ,
259+ 967600467 ,
260+ 1172861548 ,
261+ 1973891356 ,
262+ 1503625929 ,
263+ 1881993531 ,
264+ 40601941 ,
265+ 1155570620 ,
266+ 571547775 ,
267+ 1361622243 ,
268+ 1495024047 ,
269+ 1733254248 ,
270+ 964808915 ,
271+ 763558040 ,
272+ 1887228519 ,
273+ 994888261 ,
274+ 718330940 ,
275+ 213359415 ,
276+ 603124968 ,
277+ 1038411577 ,
278+ 2099454809 ,
279+ 949846777 ,
280+ 630926956 ,
281+ 1168723439 ,
282+ 222917504 ,
283+ 1527025973 ,
284+ 1009157017 ,
285+ 2029957881 ,
286+ 805977836 ,
287+ 1347511739 ,
288+ 540019059 ,
289+ 589807745 ,
290+ 440771316 ,
291+ 1530063406 ,
292+ 761076336 ,
293+ 87974206 ,
294+ 1412686751 ,
295+ 1230318064 ,
296+ 514464425 ,
297+ 1469011754 ,
298+ 1770970737 ,
299+ 1510972858 ,
300+ 965357206 ,
301+ 209398053 ,
302+ 778802532 ,
303+ 40567006 ,
304+ 1984217577 ,
305+ 1545851069 ,
306+ 879801839 ,
307+ 1611910970 ,
308+ 1215591048 ,
309+ 330802499 ,
310+ 1051639108 ,
311+ 321036 ,
312+ 511927202 ,
313+ 591603098 ,
314+ 1775897642 ,
315+ 115598532 ,
316+ 278200718 ,
317+ 233743176 ,
318+ 525096211 ,
319+ 1335507608 ,
320+ 830017835 ,
321+ 1380629279 ,
322+ 560028578 ,
323+ 598425701 ,
324+ 302162385 ,
325+ 567434115 ,
326+ 1859222575 ,
327+ 958294793 ,
328+ 1582225556 ,
329+ 1781487858 ,
330+ 1570246000 ,
331+ 1067748446 ,
332+ 526608119 ,
333+ 1666453343 ,
334+ 1786918381 ,
335+ 348203640 ,
336+ 1860035017 ,
337+ 1489902626 ,
338+ 1904576699 ,
339+ 860033965 ,
340+ 1954077639 ,
341+ 1685771567 ,
342+ 971513929 ,
343+ 1877873770 ,
344+ 137113380 ,
345+ 520695829 ,
346+ 806829080 ,
347+ 1408699405 ,
348+ 1613277964 ,
349+ 793223662 ,
350+ 648443918 ,
351+ 893435011 ,
352+ 403879071 ,
353+ 1363789863 ,
354+ 1662900517 ,
355+ 2043370 ,
356+ 2109755796 ,
357+ 931751726 ,
358+ 2091644718 ,
359+ 606977583 ,
360+ 185050397 ,
361+ 946157136 ,
362+ 1350065230 ,
363+ 1625860064 ,
364+ 122045240 ,
365+ 880989921 ,
366+ 145137438 ,
367+ 1059782436 ,
368+ 1477755661 ,
369+ 335465138 ,
370+ 1640704282 ,
371+ 1757946479 ,
372+ 1551204074 ,
373+ 681266718 ,
374+ ]
375+
376+ # For width 16 (needs 8*16 + 20 = 148 constants).
377+ ROUND_CONSTANTS_16 : List [Fp ] = [Fp (value = v ) for v in _RAW_CONSTANTS_16 ]
378+
379+ # For width 24 (needs 8*24 + 23 = 215 constants).
380+ ROUND_CONSTANTS_24 : List [Fp ] = [Fp (value = v ) for v in _RAW_CONSTANTS_24 ]
You can’t perform that action at this time.
0 commit comments