/* MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal * in the Software without restriction, including without limitation the rights * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell * copies of the Software, and to permit persons to whom the Software is * furnished to do so, subject to the following conditions: * * The above copyright notice and this permission notice shall be included in all * copies or substantial portions of the Software. * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE * SOFTWARE. */ #ifndef __internal_Hacl_Ed25519_PrecompTable_H #define __internal_Hacl_Ed25519_PrecompTable_H #if defined(__cplusplus) extern "C" { #endif #include #include "krml/internal/types.h" #include "krml/lowstar_endianness.h" #include "krml/internal/target.h" static const uint64_t Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w4[320U] = { 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1738742601995546ULL, 1146398526822698ULL, 2070867633025821ULL, 562264141797630ULL, 587772402128613ULL, 1801439850948184ULL, 1351079888211148ULL, 450359962737049ULL, 900719925474099ULL, 1801439850948198ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1841354044333475ULL, 16398895984059ULL, 755974180946558ULL, 900171276175154ULL, 1821297809914039ULL, 1661154287933054ULL, 284530020860578ULL, 1390261174866914ULL, 1524110943907984ULL, 1045603498418422ULL, 928651508580478ULL, 1383326941296346ULL, 961937908925785ULL, 80455759693706ULL, 904734540352947ULL, 1507481815385608ULL, 2223447444246085ULL, 1083941587175919ULL, 2059929906842505ULL, 1581435440146976ULL, 782730187692425ULL, 9928394897574ULL, 1539449519985236ULL, 1923587931078510ULL, 552919286076056ULL, 376925408065760ULL, 447320488831784ULL, 1362918338468019ULL, 1470031896696846ULL, 2189796996539902ULL, 1337552949959847ULL, 1762287177775726ULL, 237994495816815ULL, 1277840395970544ULL, 543972849007241ULL, 1224692671618814ULL, 162359533289271ULL, 282240927125249ULL, 586909166382289ULL, 17726488197838ULL, 377014554985659ULL, 1433835303052512ULL, 702061469493692ULL, 1142253108318154ULL, 318297794307551ULL, 954362646308543ULL, 517363881452320ULL, 1868013482130416ULL, 262562472373260ULL, 902232853249919ULL, 2107343057055746ULL, 462368348619024ULL, 1893758677092974ULL, 2177729767846389ULL, 2168532543559143ULL, 443867094639821ULL, 730169342581022ULL, 1564589016879755ULL, 51218195700649ULL, 76684578423745ULL, 560266272480743ULL, 922517457707697ULL, 2066645939860874ULL, 1318277348414638ULL, 1576726809084003ULL, 1817337608563665ULL, 1874240939237666ULL, 754733726333910ULL, 97085310406474ULL, 751148364309235ULL, 1622159695715187ULL, 1444098819684916ULL, 130920805558089ULL, 1260449179085308ULL, 1860021740768461ULL, 110052860348509ULL, 193830891643810ULL, 164148413933881ULL, 180017794795332ULL, 1523506525254651ULL, 465981629225956ULL, 559733514964572ULL, 1279624874416974ULL, 2026642326892306ULL, 1425156829982409ULL, 2160936383793147ULL, 1061870624975247ULL, 2023497043036941ULL, 117942212883190ULL, 490339622800774ULL, 1729931303146295ULL, 422305932971074ULL, 529103152793096ULL, 1211973233775992ULL, 721364955929681ULL, 1497674430438813ULL, 342545521275073ULL, 2102107575279372ULL, 2108462244669966ULL, 1382582406064082ULL, 2206396818383323ULL, 2109093268641147ULL, 10809845110983ULL, 1605176920880099ULL, 744640650753946ULL, 1712758897518129ULL, 373410811281809ULL, 648838265800209ULL, 813058095530999ULL, 513987632620169ULL, 465516160703329ULL, 2136322186126330ULL, 1979645899422932ULL, 1197131006470786ULL, 1467836664863979ULL, 1340751381374628ULL, 1810066212667962ULL, 1009933588225499ULL, 1106129188080873ULL, 1388980405213901ULL, 533719246598044ULL, 1169435803073277ULL, 198920999285821ULL, 487492330629854ULL, 1807093008537778ULL, 1540899012923865ULL, 2075080271659867ULL, 1527990806921523ULL, 1323728742908002ULL, 1568595959608205ULL, 1388032187497212ULL, 2026968840050568ULL, 1396591153295755ULL, 820416950170901ULL, 520060313205582ULL, 2016404325094901ULL, 1584709677868520ULL, 272161374469956ULL, 1567188603996816ULL, 1986160530078221ULL, 553930264324589ULL, 1058426729027503ULL, 8762762886675ULL, 2216098143382988ULL, 1835145266889223ULL, 1712936431558441ULL, 1017009937844974ULL, 585361667812740ULL, 2114711541628181ULL, 2238729632971439ULL, 121257546253072ULL, 847154149018345ULL, 211972965476684ULL, 287499084460129ULL, 2098247259180197ULL, 839070411583329ULL, 339551619574372ULL, 1432951287640743ULL, 526481249498942ULL, 931991661905195ULL, 1884279965674487ULL, 200486405604411ULL, 364173020594788ULL, 518034455936955ULL, 1085564703965501ULL, 16030410467927ULL, 604865933167613ULL, 1695298441093964ULL, 498856548116159ULL, 2193030062787034ULL, 1706339802964179ULL, 1721199073493888ULL, 820740951039755ULL, 1216053436896834ULL, 23954895815139ULL, 1662515208920491ULL, 1705443427511899ULL, 1957928899570365ULL, 1189636258255725ULL, 1795695471103809ULL, 1691191297654118ULL, 282402585374360ULL, 460405330264832ULL, 63765529445733ULL, 469763447404473ULL, 733607089694996ULL, 685410420186959ULL, 1096682630419738ULL, 1162548510542362ULL, 1020949526456676ULL, 1211660396870573ULL, 613126398222696ULL, 1117829165843251ULL, 742432540886650ULL, 1483755088010658ULL, 942392007134474ULL, 1447834130944107ULL, 489368274863410ULL, 23192985544898ULL, 648442406146160ULL, 785438843373876ULL, 249464684645238ULL, 170494608205618ULL, 335112827260550ULL, 1462050123162735ULL, 1084803668439016ULL, 853459233600325ULL, 215777728187495ULL, 1965759433526974ULL, 1349482894446537ULL, 694163317612871ULL, 860536766165036ULL, 1178788094084321ULL, 1652739626626996ULL, 2115723946388185ULL, 1577204379094664ULL, 1083882859023240ULL, 1768759143381635ULL, 1737180992507258ULL, 246054513922239ULL, 577253134087234ULL, 356340280578042ULL, 1638917769925142ULL, 223550348130103ULL, 470592666638765ULL, 22663573966996ULL, 596552461152400ULL, 364143537069499ULL, 3942119457699ULL, 107951982889287ULL, 1843471406713209ULL, 1625773041610986ULL, 1466141092501702ULL, 1043024095021271ULL, 310429964047508ULL, 98559121500372ULL, 152746933782868ULL, 259407205078261ULL, 828123093322585ULL, 1576847274280091ULL, 1170871375757302ULL, 1588856194642775ULL, 984767822341977ULL, 1141497997993760ULL, 809325345150796ULL, 1879837728202511ULL, 201340910657893ULL, 1079157558888483ULL, 1052373448588065ULL, 1732036202501778ULL, 2105292670328445ULL, 679751387312402ULL, 1679682144926229ULL, 1695823455818780ULL, 498852317075849ULL, 1786555067788433ULL, 1670727545779425ULL, 117945875433544ULL, 407939139781844ULL, 854632120023778ULL, 1413383148360437ULL, 286030901733673ULL, 1207361858071196ULL, 461340408181417ULL, 1096919590360164ULL, 1837594897475685ULL, 533755561544165ULL, 1638688042247712ULL, 1431653684793005ULL, 1036458538873559ULL, 390822120341779ULL, 1920929837111618ULL, 543426740024168ULL, 645751357799929ULL, 2245025632994463ULL, 1550778638076452ULL, 223738153459949ULL, 1337209385492033ULL, 1276967236456531ULL, 1463815821063071ULL, 2070620870191473ULL, 1199170709413753ULL, 273230877394166ULL, 1873264887608046ULL, 890877152910775ULL }; static const uint64_t Hacl_Ed25519_PrecompTable_precomp_g_pow2_64_table_w4[320U] = { 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 13559344787725ULL, 2051621493703448ULL, 1947659315640708ULL, 626856790370168ULL, 1592804284034836ULL, 1781728767459187ULL, 278818420518009ULL, 2038030359908351ULL, 910625973862690ULL, 471887343142239ULL, 1298543306606048ULL, 794147365642417ULL, 129968992326749ULL, 523140861678572ULL, 1166419653909231ULL, 2009637196928390ULL, 1288020222395193ULL, 1007046974985829ULL, 208981102651386ULL, 2074009315253380ULL, 1564056062071967ULL, 276822668750618ULL, 206621292512572ULL, 470304361809269ULL, 895215438398493ULL, 1527859053868686ULL, 1624967223409369ULL, 811821865979736ULL, 350450534838340ULL, 219143807921807ULL, 507994540371254ULL, 986513794574720ULL, 1142661369967121ULL, 621278293399257ULL, 556189161519781ULL, 351964007865066ULL, 2011573453777822ULL, 1367125527151537ULL, 1691316722438196ULL, 731328817345164ULL, 1284781192709232ULL, 478439299539269ULL, 204842178076429ULL, 2085125369913651ULL, 1980773492792985ULL, 1480264409524940ULL, 688389585376233ULL, 612962643526972ULL, 165595382536676ULL, 1850300069212263ULL, 1176357203491551ULL, 1880164984292321ULL, 10786153104736ULL, 1242293560510203ULL, 1358399951884084ULL, 1901358796610357ULL, 1385092558795806ULL, 1734893785311348ULL, 2046201851951191ULL, 1233811309557352ULL, 1531160168656129ULL, 1543287181303358ULL, 516121446374119ULL, 723422668089935ULL, 1228176774959679ULL, 1598014722726267ULL, 1630810326658412ULL, 1343833067463760ULL, 1024397964362099ULL, 1157142161346781ULL, 56422174971792ULL, 544901687297092ULL, 1291559028869009ULL, 1336918672345120ULL, 1390874603281353ULL, 1127199512010904ULL, 992644979940964ULL, 1035213479783573ULL, 36043651196100ULL, 1220961519321221ULL, 1348190007756977ULL, 579420200329088ULL, 1703819961008985ULL, 1993919213460047ULL, 2225080008232251ULL, 392785893702372ULL, 464312521482632ULL, 1224525362116057ULL, 810394248933036ULL, 932513521649107ULL, 592314953488703ULL, 586334603791548ULL, 1310888126096549ULL, 650842674074281ULL, 1596447001791059ULL, 2086767406328284ULL, 1866377645879940ULL, 1721604362642743ULL, 738502322566890ULL, 1851901097729689ULL, 1158347571686914ULL, 2023626733470827ULL, 329625404653699ULL, 563555875598551ULL, 516554588079177ULL, 1134688306104598ULL, 186301198420809ULL, 1339952213563300ULL, 643605614625891ULL, 1947505332718043ULL, 1722071694852824ULL, 601679570440694ULL, 1821275721236351ULL, 1808307842870389ULL, 1654165204015635ULL, 1457334100715245ULL, 217784948678349ULL, 1820622417674817ULL, 1946121178444661ULL, 597980757799332ULL, 1745271227710764ULL, 2010952890941980ULL, 339811849696648ULL, 1066120666993872ULL, 261276166508990ULL, 323098645774553ULL, 207454744271283ULL, 941448672977675ULL, 71890920544375ULL, 840849789313357ULL, 1223996070717926ULL, 196832550853408ULL, 115986818309231ULL, 1586171527267675ULL, 1666169080973450ULL, 1456454731176365ULL, 44467854369003ULL, 2149656190691480ULL, 283446383597589ULL, 2040542647729974ULL, 305705593840224ULL, 475315822269791ULL, 648133452550632ULL, 169218658835720ULL, 24960052338251ULL, 938907951346766ULL, 425970950490510ULL, 1037622011013183ULL, 1026882082708180ULL, 1635699409504916ULL, 1644776942870488ULL, 2151820331175914ULL, 824120674069819ULL, 835744976610113ULL, 1991271032313190ULL, 96507354724855ULL, 400645405133260ULL, 343728076650825ULL, 1151585441385566ULL, 1403339955333520ULL, 230186314139774ULL, 1736248861506714ULL, 1010804378904572ULL, 1394932289845636ULL, 1901351256960852ULL, 2187471430089807ULL, 1003853262342670ULL, 1327743396767461ULL, 1465160415991740ULL, 366625359144534ULL, 1534791405247604ULL, 1790905930250187ULL, 1255484115292738ULL, 2223291365520443ULL, 210967717407408ULL, 26722916813442ULL, 1919574361907910ULL, 468825088280256ULL, 2230011775946070ULL, 1628365642214479ULL, 568871869234932ULL, 1066987968780488ULL, 1692242903745558ULL, 1678903997328589ULL, 214262165888021ULL, 1929686748607204ULL, 1790138967989670ULL, 1790261616022076ULL, 1559824537553112ULL, 1230364591311358ULL, 147531939886346ULL, 1528207085815487ULL, 477957922927292ULL, 285670243881618ULL, 264430080123332ULL, 1163108160028611ULL, 373201522147371ULL, 34903775270979ULL, 1750870048600662ULL, 1319328308741084ULL, 1547548634278984ULL, 1691259592202927ULL, 2247758037259814ULL, 329611399953677ULL, 1385555496268877ULL, 2242438354031066ULL, 1329523854843632ULL, 399895373846055ULL, 678005703193452ULL, 1496357700997771ULL, 71909969781942ULL, 1515391418612349ULL, 470110837888178ULL, 1981307309417466ULL, 1259888737412276ULL, 669991710228712ULL, 1048546834514303ULL, 1678323291295512ULL, 2172033978088071ULL, 1529278455500556ULL, 901984601941894ULL, 780867622403807ULL, 550105677282793ULL, 975860231176136ULL, 525188281689178ULL, 49966114807992ULL, 1776449263836645ULL, 267851776380338ULL, 2225969494054620ULL, 2016794225789822ULL, 1186108678266608ULL, 1023083271408882ULL, 1119289418565906ULL, 1248185897348801ULL, 1846081539082697ULL, 23756429626075ULL, 1441999021105403ULL, 724497586552825ULL, 1287761623605379ULL, 685303359654224ULL, 2217156930690570ULL, 163769288918347ULL, 1098423278284094ULL, 1391470723006008ULL, 570700152353516ULL, 744804507262556ULL, 2200464788609495ULL, 624141899161992ULL, 2249570166275684ULL, 378706441983561ULL, 122486379999375ULL, 430741162798924ULL, 113847463452574ULL, 266250457840685ULL, 2120743625072743ULL, 222186221043927ULL, 1964290018305582ULL, 1435278008132477ULL, 1670867456663734ULL, 2009989552599079ULL, 1348024113448744ULL, 1158423886300455ULL, 1356467152691569ULL, 306943042363674ULL, 926879628664255ULL, 1349295689598324ULL, 725558330071205ULL, 536569987519948ULL, 116436990335366ULL, 1551888573800376ULL, 2044698345945451ULL, 104279940291311ULL, 251526570943220ULL, 754735828122925ULL, 33448073576361ULL, 994605876754543ULL, 546007584022006ULL, 2217332798409487ULL, 706477052561591ULL, 131174619428653ULL, 2148698284087243ULL, 239290486205186ULL, 2161325796952184ULL, 1713452845607994ULL, 1297861562938913ULL, 1779539876828514ULL, 1926559018603871ULL, 296485747893968ULL, 1859208206640686ULL, 538513979002718ULL, 103998826506137ULL, 2025375396538469ULL, 1370680785701206ULL, 1698557311253840ULL, 1411096399076595ULL, 2132580530813677ULL, 2071564345845035ULL, 498581428556735ULL, 1136010486691371ULL, 1927619356993146ULL }; static const uint64_t Hacl_Ed25519_PrecompTable_precomp_g_pow2_128_table_w4[320U] = { 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 557549315715710ULL, 196756086293855ULL, 846062225082495ULL, 1865068224838092ULL, 991112090754908ULL, 522916421512828ULL, 2098523346722375ULL, 1135633221747012ULL, 858420432114866ULL, 186358544306082ULL, 1044420411868480ULL, 2080052304349321ULL, 557301814716724ULL, 1305130257814057ULL, 2126012765451197ULL, 1441004402875101ULL, 353948968859203ULL, 470765987164835ULL, 1507675957683570ULL, 1086650358745097ULL, 1911913434398388ULL, 66086091117182ULL, 1137511952425971ULL, 36958263512141ULL, 2193310025325256ULL, 1085191426269045ULL, 1232148267909446ULL, 1449894406170117ULL, 1241416717139557ULL, 1940876999212868ULL, 829758415918121ULL, 309608450373449ULL, 2228398547683851ULL, 1580623271960188ULL, 1675601502456740ULL, 1360363115493548ULL, 1098397313096815ULL, 1809255384359797ULL, 1458261916834384ULL, 210682545649705ULL, 1606836641068115ULL, 1230478270405318ULL, 1843192771547802ULL, 1794596343564051ULL, 229060710252162ULL, 2169742775467181ULL, 701467067318072ULL, 696018499035555ULL, 521051885339807ULL, 158329567901874ULL, 740426481832143ULL, 1369811177301441ULL, 503351589084015ULL, 1781114827942261ULL, 1650493549693035ULL, 2174562418345156ULL, 456517194809244ULL, 2052761522121179ULL, 2233342271123682ULL, 1445872925177435ULL, 1131882576902813ULL, 220765848055241ULL, 1280259961403769ULL, 1581497080160712ULL, 1477441080108824ULL, 218428165202767ULL, 1970598141278907ULL, 643366736173069ULL, 2167909426804014ULL, 834993711408259ULL, 1922437166463212ULL, 1900036281472252ULL, 513794844386304ULL, 1297904164900114ULL, 1147626295373268ULL, 1910101606251299ULL, 182933838633381ULL, 806229530787362ULL, 155511666433200ULL, 290522463375462ULL, 534373523491751ULL, 1302938814480515ULL, 1664979184120445ULL, 304235649499423ULL, 339284524318609ULL, 1881717946973483ULL, 1670802286833842ULL, 2223637120675737ULL, 135818919485814ULL, 1144856572842792ULL, 2234981613434386ULL, 963917024969826ULL, 402275378284993ULL, 141532417412170ULL, 921537468739387ULL, 963905069722607ULL, 1405442890733358ULL, 1567763927164655ULL, 1664776329195930ULL, 2095924165508507ULL, 994243110271379ULL, 1243925610609353ULL, 1029845815569727ULL, 1001968867985629ULL, 170368934002484ULL, 1100906131583801ULL, 1825190326449569ULL, 1462285121182096ULL, 1545240767016377ULL, 797859025652273ULL, 1062758326657530ULL, 1125600735118266ULL, 739325756774527ULL, 1420144485966996ULL, 1915492743426702ULL, 752968196344993ULL, 882156396938351ULL, 1909097048763227ULL, 849058590685611ULL, 840754951388500ULL, 1832926948808323ULL, 2023317100075297ULL, 322382745442827ULL, 1569741341737601ULL, 1678986113194987ULL, 757598994581938ULL, 29678659580705ULL, 1239680935977986ULL, 1509239427168474ULL, 1055981929287006ULL, 1894085471158693ULL, 916486225488490ULL, 642168890366120ULL, 300453362620010ULL, 1858797242721481ULL, 2077989823177130ULL, 510228455273334ULL, 1473284798689270ULL, 5173934574301ULL, 765285232030050ULL, 1007154707631065ULL, 1862128712885972ULL, 168873464821340ULL, 1967853269759318ULL, 1489896018263031ULL, 592451806166369ULL, 1242298565603883ULL, 1838918921339058ULL, 697532763910695ULL, 294335466239059ULL, 135687058387449ULL, 2133734403874176ULL, 2121911143127699ULL, 20222476737364ULL, 1200824626476747ULL, 1397731736540791ULL, 702378430231418ULL, 59059527640068ULL, 460992547183981ULL, 1016125857842765ULL, 1273530839608957ULL, 96724128829301ULL, 1313433042425233ULL, 3543822857227ULL, 761975685357118ULL, 110417360745248ULL, 1079634164577663ULL, 2044574510020457ULL, 338709058603120ULL, 94541336042799ULL, 127963233585039ULL, 94427896272258ULL, 1143501979342182ULL, 1217958006212230ULL, 2153887831492134ULL, 1519219513255575ULL, 251793195454181ULL, 392517349345200ULL, 1507033011868881ULL, 2208494254670752ULL, 1364389582694359ULL, 2214069430728063ULL, 1272814257105752ULL, 741450148906352ULL, 1105776675555685ULL, 824447222014984ULL, 528745219306376ULL, 589427609121575ULL, 1501786838809155ULL, 379067373073147ULL, 184909476589356ULL, 1346887560616185ULL, 1932023742314082ULL, 1633302311869264ULL, 1685314821133069ULL, 1836610282047884ULL, 1595571594397150ULL, 615441688872198ULL, 1926435616702564ULL, 235632180396480ULL, 1051918343571810ULL, 2150570051687050ULL, 879198845408738ULL, 1443966275205464ULL, 481362545245088ULL, 512807443532642ULL, 641147578283480ULL, 1594276116945596ULL, 1844812743300602ULL, 2044559316019485ULL, 202620777969020ULL, 852992984136302ULL, 1500869642692910ULL, 1085216217052457ULL, 1736294372259758ULL, 2009666354486552ULL, 1262389020715248ULL, 1166527705256867ULL, 1409917450806036ULL, 1705819160057637ULL, 1116901782584378ULL, 1278460472285473ULL, 257879811360157ULL, 40314007176886ULL, 701309846749639ULL, 1380457676672777ULL, 631519782380272ULL, 1196339573466793ULL, 955537708940017ULL, 532725633381530ULL, 641190593731833ULL, 7214357153807ULL, 481922072107983ULL, 1634886189207352ULL, 1247659758261633ULL, 1655809614786430ULL, 43105797900223ULL, 76205809912607ULL, 1936575107455823ULL, 1107927314642236ULL, 2199986333469333ULL, 802974829322510ULL, 718173128143482ULL, 539385184235615ULL, 2075693785611221ULL, 953281147333690ULL, 1623571637172587ULL, 655274535022250ULL, 1568078078819021ULL, 101142125049712ULL, 1488441673350881ULL, 1457969561944515ULL, 1492622544287712ULL, 2041460689280803ULL, 1961848091392887ULL, 461003520846938ULL, 934728060399807ULL, 117723291519705ULL, 1027773762863526ULL, 56765304991567ULL, 2184028379550479ULL, 1768767711894030ULL, 1304432068983172ULL, 498080974452325ULL, 2134905654858163ULL, 1446137427202647ULL, 551613831549590ULL, 680288767054205ULL, 1278113339140386ULL, 378149431842614ULL, 80520494426960ULL, 2080985256348782ULL, 673432591799820ULL, 739189463724560ULL, 1847191452197509ULL, 527737312871602ULL, 477609358840073ULL, 1891633072677946ULL, 1841456828278466ULL, 2242502936489002ULL, 524791829362709ULL, 276648168514036ULL, 991706903257619ULL, 512580228297906ULL, 1216855104975946ULL, 67030930303149ULL, 769593945208213ULL, 2048873385103577ULL, 455635274123107ULL, 2077404927176696ULL, 1803539634652306ULL, 1837579953843417ULL, 1564240068662828ULL, 1964310918970435ULL, 832822906252492ULL, 1516044634195010ULL, 770571447506889ULL, 602215152486818ULL, 1760828333136947ULL, 730156776030376ULL }; static const uint64_t Hacl_Ed25519_PrecompTable_precomp_g_pow2_192_table_w4[320U] = { 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1129953239743101ULL, 1240339163956160ULL, 61002583352401ULL, 2017604552196030ULL, 1576867829229863ULL, 1508654942849389ULL, 270111619664077ULL, 1253097517254054ULL, 721798270973250ULL, 161923365415298ULL, 828530877526011ULL, 1494851059386763ULL, 662034171193976ULL, 1315349646974670ULL, 2199229517308806ULL, 497078277852673ULL, 1310507715989956ULL, 1881315714002105ULL, 2214039404983803ULL, 1331036420272667ULL, 296286697520787ULL, 1179367922639127ULL, 25348441419697ULL, 2200984961703188ULL, 150893128908291ULL, 1978614888570852ULL, 1539657347172046ULL, 553810196523619ULL, 246017573977646ULL, 1440448985385485ULL, 346049108099981ULL, 601166606218546ULL, 855822004151713ULL, 1957521326383188ULL, 1114240380430887ULL, 1349639675122048ULL, 957375954499040ULL, 111551795360136ULL, 618586733648988ULL, 490708840688866ULL, 1267002049697314ULL, 1130723224930028ULL, 215603029480828ULL, 1277138555414710ULL, 1556750324971322ULL, 1407903521793741ULL, 1836836546590749ULL, 576500297444199ULL, 2074707599091135ULL, 1826239864380012ULL, 1935365705983312ULL, 239501825683682ULL, 1594236669034980ULL, 1283078975055301ULL, 856745636255925ULL, 1342128647959981ULL, 945216428379689ULL, 938746202496410ULL, 105775123333919ULL, 1379852610117266ULL, 1770216827500275ULL, 1016017267535704ULL, 1902885522469532ULL, 994184703730489ULL, 2227487538793763ULL, 53155967096055ULL, 1264120808114350ULL, 1334928769376729ULL, 393911808079997ULL, 826229239481845ULL, 1827903006733192ULL, 1449283706008465ULL, 1258040415217849ULL, 1641484112868370ULL, 1140150841968176ULL, 391113338021313ULL, 162138667815833ULL, 742204396566060ULL, 110709233440557ULL, 90179377432917ULL, 530511949644489ULL, 911568635552279ULL, 135869304780166ULL, 617719999563692ULL, 1802525001631319ULL, 1836394639510490ULL, 1862739456475085ULL, 1378284444664288ULL, 1617882529391756ULL, 876124429891172ULL, 1147654641445091ULL, 1476943370400542ULL, 688601222759067ULL, 2120281968990205ULL, 1387113236912611ULL, 2125245820685788ULL, 1030674016350092ULL, 1594684598654247ULL, 1165939511879820ULL, 271499323244173ULL, 546587254515484ULL, 945603425742936ULL, 1242252568170226ULL, 561598728058142ULL, 604827091794712ULL, 19869753585186ULL, 565367744708915ULL, 536755754533603ULL, 1767258313589487ULL, 907952975936127ULL, 292851652613937ULL, 163573546237963ULL, 837601408384564ULL, 591996990118301ULL, 2126051747693057ULL, 182247548824566ULL, 908369044122868ULL, 1335442699947273ULL, 2234292296528612ULL, 689537529333034ULL, 2174778663790714ULL, 1011407643592667ULL, 1856130618715473ULL, 1557437221651741ULL, 2250285407006102ULL, 1412384213410827ULL, 1428042038612456ULL, 962709733973660ULL, 313995703125919ULL, 1844969155869325ULL, 787716782673657ULL, 622504542173478ULL, 930119043384654ULL, 2128870043952488ULL, 537781531479523ULL, 1556666269904940ULL, 417333635741346ULL, 1986743846438415ULL, 877620478041197ULL, 2205624582983829ULL, 595260668884488ULL, 2025159350373157ULL, 2091659716088235ULL, 1423634716596391ULL, 653686638634080ULL, 1972388399989956ULL, 795575741798014ULL, 889240107997846ULL, 1446156876910732ULL, 1028507012221776ULL, 1071697574586478ULL, 1689630411899691ULL, 604092816502174ULL, 1909917373896122ULL, 1602544877643837ULL, 1227177032923867ULL, 62684197535630ULL, 186146290753883ULL, 414449055316766ULL, 1560555880866750ULL, 157579947096755ULL, 230526795502384ULL, 1197673369665894ULL, 593779215869037ULL, 214638834474097ULL, 1796344443484478ULL, 493550548257317ULL, 1628442824033694ULL, 1410811655893495ULL, 1009361960995171ULL, 604736219740352ULL, 392445928555351ULL, 1254295770295706ULL, 1958074535046128ULL, 508699942241019ULL, 739405911261325ULL, 1678760393882409ULL, 517763708545996ULL, 640040257898722ULL, 384966810872913ULL, 407454748380128ULL, 152604679407451ULL, 185102854927662ULL, 1448175503649595ULL, 100328519208674ULL, 1153263667012830ULL, 1643926437586490ULL, 609632142834154ULL, 980984004749261ULL, 855290732258779ULL, 2186022163021506ULL, 1254052618626070ULL, 1850030517182611ULL, 162348933090207ULL, 1948712273679932ULL, 1331832516262191ULL, 1219400369175863ULL, 89689036937483ULL, 1554886057235815ULL, 1520047528432789ULL, 81263957652811ULL, 146612464257008ULL, 2207945627164163ULL, 919846660682546ULL, 1925694087906686ULL, 2102027292388012ULL, 887992003198635ULL, 1817924871537027ULL, 746660005584342ULL, 753757153275525ULL, 91394270908699ULL, 511837226544151ULL, 736341543649373ULL, 1256371121466367ULL, 1977778299551813ULL, 817915174462263ULL, 1602323381418035ULL, 190035164572930ULL, 603796401391181ULL, 2152666873671669ULL, 1813900316324112ULL, 1292622433358041ULL, 888439870199892ULL, 978918155071994ULL, 534184417909805ULL, 466460084317313ULL, 1275223140288685ULL, 786407043883517ULL, 1620520623925754ULL, 1753625021290269ULL, 751937175104525ULL, 905301961820613ULL, 697059847245437ULL, 584919033981144ULL, 1272165506533156ULL, 1532180021450866ULL, 1901407354005301ULL, 1421319720492586ULL, 2179081609765456ULL, 2193253156667632ULL, 1080248329608584ULL, 2158422436462066ULL, 759167597017850ULL, 545759071151285ULL, 641600428493698ULL, 943791424499848ULL, 469571542427864ULL, 951117845222467ULL, 1780538594373407ULL, 614611122040309ULL, 1354826131886963ULL, 221898131992340ULL, 1145699723916219ULL, 798735379961769ULL, 1843560518208287ULL, 1424523160161545ULL, 205549016574779ULL, 2239491587362749ULL, 1918363582399888ULL, 1292183072788455ULL, 1783513123192567ULL, 1584027954317205ULL, 1890421443925740ULL, 1718459319874929ULL, 1522091040748809ULL, 399467600667219ULL, 1870973059066576ULL, 287514433150348ULL, 1397845311152885ULL, 1880440629872863ULL, 709302939340341ULL, 1813571361109209ULL, 86598795876860ULL, 1146964554310612ULL, 1590956584862432ULL, 2097004628155559ULL, 656227622102390ULL, 1808500445541891ULL, 958336726523135ULL, 2007604569465975ULL, 313504950390997ULL, 1399686004953620ULL, 1759732788465234ULL, 1562539721055836ULL, 1575722765016293ULL, 793318366641259ULL, 443876859384887ULL, 547308921989704ULL, 636698687503328ULL, 2179175835287340ULL, 498333551718258ULL, 932248760026176ULL, 1612395686304653ULL, 2179774103745626ULL, 1359658123541018ULL, 171488501802442ULL, 1625034951791350ULL, 520196922773633ULL, 1873787546341877ULL, 303457823885368ULL }; static const uint64_t Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5[640U] = { 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1738742601995546ULL, 1146398526822698ULL, 2070867633025821ULL, 562264141797630ULL, 587772402128613ULL, 1801439850948184ULL, 1351079888211148ULL, 450359962737049ULL, 900719925474099ULL, 1801439850948198ULL, 1ULL, 0ULL, 0ULL, 0ULL, 0ULL, 1841354044333475ULL, 16398895984059ULL, 755974180946558ULL, 900171276175154ULL, 1821297809914039ULL, 1661154287933054ULL, 284530020860578ULL, 1390261174866914ULL, 1524110943907984ULL, 1045603498418422ULL, 928651508580478ULL, 1383326941296346ULL, 961937908925785ULL, 80455759693706ULL, 904734540352947ULL, 1507481815385608ULL, 2223447444246085ULL, 1083941587175919ULL, 2059929906842505ULL, 1581435440146976ULL, 782730187692425ULL, 9928394897574ULL, 1539449519985236ULL, 1923587931078510ULL, 552919286076056ULL, 376925408065760ULL, 447320488831784ULL, 1362918338468019ULL, 1470031896696846ULL, 2189796996539902ULL, 1337552949959847ULL, 1762287177775726ULL, 237994495816815ULL, 1277840395970544ULL, 543972849007241ULL, 1224692671618814ULL, 162359533289271ULL, 282240927125249ULL, 586909166382289ULL, 17726488197838ULL, 377014554985659ULL, 1433835303052512ULL, 702061469493692ULL, 1142253108318154ULL, 318297794307551ULL, 954362646308543ULL, 517363881452320ULL, 1868013482130416ULL, 262562472373260ULL, 902232853249919ULL, 2107343057055746ULL, 462368348619024ULL, 1893758677092974ULL, 2177729767846389ULL, 2168532543559143ULL, 443867094639821ULL, 730169342581022ULL, 1564589016879755ULL, 51218195700649ULL, 76684578423745ULL, 560266272480743ULL, 922517457707697ULL, 2066645939860874ULL, 1318277348414638ULL, 1576726809084003ULL, 1817337608563665ULL, 1874240939237666ULL, 754733726333910ULL, 97085310406474ULL, 751148364309235ULL, 1622159695715187ULL, 1444098819684916ULL, 130920805558089ULL, 1260449179085308ULL, 1860021740768461ULL, 110052860348509ULL, 193830891643810ULL, 164148413933881ULL, 180017794795332ULL, 1523506525254651ULL, 465981629225956ULL, 559733514964572ULL, 1279624874416974ULL, 2026642326892306ULL, 1425156829982409ULL, 2160936383793147ULL, 1061870624975247ULL, 2023497043036941ULL, 117942212883190ULL, 490339622800774ULL, 1729931303146295ULL, 422305932971074ULL, 529103152793096ULL, 1211973233775992ULL, 721364955929681ULL, 1497674430438813ULL, 342545521275073ULL, 2102107575279372ULL, 2108462244669966ULL, 1382582406064082ULL, 2206396818383323ULL, 2109093268641147ULL, 10809845110983ULL, 1605176920880099ULL, 744640650753946ULL, 1712758897518129ULL, 373410811281809ULL, 648838265800209ULL, 813058095530999ULL, 513987632620169ULL, 465516160703329ULL, 2136322186126330ULL, 1979645899422932ULL, 1197131006470786ULL, 1467836664863979ULL, 1340751381374628ULL, 1810066212667962ULL, 1009933588225499ULL, 1106129188080873ULL, 1388980405213901ULL, 533719246598044ULL, 1169435803073277ULL, 198920999285821ULL, 487492330629854ULL, 1807093008537778ULL, 1540899012923865ULL, 2075080271659867ULL, 1527990806921523ULL, 1323728742908002ULL, 1568595959608205ULL, 1388032187497212ULL, 2026968840050568ULL, 1396591153295755ULL, 820416950170901ULL, 520060313205582ULL, 2016404325094901ULL, 1584709677868520ULL, 272161374469956ULL, 1567188603996816ULL, 1986160530078221ULL, 553930264324589ULL, 1058426729027503ULL, 8762762886675ULL, 2216098143382988ULL, 1835145266889223ULL, 1712936431558441ULL, 1017009937844974ULL, 585361667812740ULL, 2114711541628181ULL, 2238729632971439ULL, 121257546253072ULL, 847154149018345ULL, 211972965476684ULL, 287499084460129ULL, 2098247259180197ULL, 839070411583329ULL, 339551619574372ULL, 1432951287640743ULL, 526481249498942ULL, 931991661905195ULL, 1884279965674487ULL, 200486405604411ULL, 364173020594788ULL, 518034455936955ULL, 1085564703965501ULL, 16030410467927ULL, 604865933167613ULL, 1695298441093964ULL, 498856548116159ULL, 2193030062787034ULL, 1706339802964179ULL, 1721199073493888ULL, 820740951039755ULL, 1216053436896834ULL, 23954895815139ULL, 1662515208920491ULL, 1705443427511899ULL, 1957928899570365ULL, 1189636258255725ULL, 1795695471103809ULL, 1691191297654118ULL, 282402585374360ULL, 460405330264832ULL, 63765529445733ULL, 469763447404473ULL, 733607089694996ULL, 685410420186959ULL, 1096682630419738ULL, 1162548510542362ULL, 1020949526456676ULL, 1211660396870573ULL, 613126398222696ULL, 1117829165843251ULL, 742432540886650ULL, 1483755088010658ULL, 942392007134474ULL, 1447834130944107ULL, 489368274863410ULL, 23192985544898ULL, 648442406146160ULL, 785438843373876ULL, 249464684645238ULL, 170494608205618ULL, 335112827260550ULL, 1462050123162735ULL, 1084803668439016ULL, 853459233600325ULL, 215777728187495ULL, 1965759433526974ULL, 1349482894446537ULL, 694163317612871ULL, 860536766165036ULL, 1178788094084321ULL, 1652739626626996ULL, 2115723946388185ULL, 1577204379094664ULL, 1083882859023240ULL, 1768759143381635ULL, 1737180992507258ULL, 246054513922239ULL, 577253134087234ULL, 356340280578042ULL, 1638917769925142ULL, 223550348130103ULL, 470592666638765ULL, 22663573966996ULL, 596552461152400ULL, 364143537069499ULL, 3942119457699ULL, 107951982889287ULL, 1843471406713209ULL, 1625773041610986ULL, 1466141092501702ULL, 1043024095021271ULL, 310429964047508ULL, 98559121500372ULL, 152746933782868ULL, 259407205078261ULL, 828123093322585ULL, 1576847274280091ULL, 1170871375757302ULL, 1588856194642775ULL, 984767822341977ULL, 1141497997993760ULL, 809325345150796ULL, 1879837728202511ULL, 201340910657893ULL, 1079157558888483ULL, 1052373448588065ULL, 1732036202501778ULL, 2105292670328445ULL, 679751387312402ULL, 1679682144926229ULL, 1695823455818780ULL, 498852317075849ULL, 1786555067788433ULL, 1670727545779425ULL, 117945875433544ULL, 407939139781844ULL, 854632120023778ULL, 1413383148360437ULL, 286030901733673ULL, 1207361858071196ULL, 461340408181417ULL, 1096919590360164ULL, 1837594897475685ULL, 533755561544165ULL, 1638688042247712ULL, 1431653684793005ULL, 1036458538873559ULL, 390822120341779ULL, 1920929837111618ULL, 543426740024168ULL, 645751357799929ULL, 2245025632994463ULL, 1550778638076452ULL, 223738153459949ULL, 1337209385492033ULL, 1276967236456531ULL, 1463815821063071ULL, 2070620870191473ULL, 1199170709413753ULL, 273230877394166ULL, 1873264887608046ULL, 890877152910775ULL, 983226445635730ULL, 44873798519521ULL, 697147127512130ULL, 961631038239304ULL, 709966160696826ULL, 1706677689540366ULL, 502782733796035ULL, 812545535346033ULL, 1693622521296452ULL, 1955813093002510ULL, 1259937612881362ULL, 1873032503803559ULL, 1140330566016428ULL, 1675726082440190ULL, 60029928909786ULL, 170335608866763ULL, 766444312315022ULL, 2025049511434113ULL, 2200845622430647ULL, 1201269851450408ULL, 590071752404907ULL, 1400995030286946ULL, 2152637413853822ULL, 2108495473841983ULL, 3855406710349ULL, 1726137673168580ULL, 51004317200100ULL, 1749082328586939ULL, 1704088976144558ULL, 1977318954775118ULL, 2062602253162400ULL, 948062503217479ULL, 361953965048030ULL, 1528264887238440ULL, 62582552172290ULL, 2241602163389280ULL, 156385388121765ULL, 2124100319761492ULL, 388928050571382ULL, 1556123596922727ULL, 979310669812384ULL, 113043855206104ULL, 2023223924825469ULL, 643651703263034ULL, 2234446903655540ULL, 1577241261424997ULL, 860253174523845ULL, 1691026473082448ULL, 1091672764933872ULL, 1957463109756365ULL, 530699502660193ULL, 349587141723569ULL, 674661681919563ULL, 1633727303856240ULL, 708909037922144ULL, 2160722508518119ULL, 1302188051602540ULL, 976114603845777ULL, 120004758721939ULL, 1681630708873780ULL, 622274095069244ULL, 1822346309016698ULL, 1100921177951904ULL, 2216952659181677ULL, 1844020550362490ULL, 1976451368365774ULL, 1321101422068822ULL, 1189859436282668ULL, 2008801879735257ULL, 2219413454333565ULL, 424288774231098ULL, 359793146977912ULL, 270293357948703ULL, 587226003677000ULL, 1482071926139945ULL, 1419630774650359ULL, 1104739070570175ULL, 1662129023224130ULL, 1609203612533411ULL, 1250932720691980ULL, 95215711818495ULL, 498746909028150ULL, 158151296991874ULL, 1201379988527734ULL, 561599945143989ULL, 2211577425617888ULL, 2166577612206324ULL, 1057590354233512ULL, 1968123280416769ULL, 1316586165401313ULL, 762728164447634ULL, 2045395244316047ULL, 1531796898725716ULL, 315385971670425ULL, 1109421039396756ULL, 2183635256408562ULL, 1896751252659461ULL, 840236037179080ULL, 796245792277211ULL, 508345890111193ULL, 1275386465287222ULL, 513560822858784ULL, 1784735733120313ULL, 1346467478899695ULL, 601125231208417ULL, 701076661112726ULL, 1841998436455089ULL, 1156768600940434ULL, 1967853462343221ULL, 2178318463061452ULL, 481885520752741ULL, 675262828640945ULL, 1033539418596582ULL, 1743329872635846ULL, 159322641251283ULL, 1573076470127113ULL, 954827619308195ULL, 778834750662635ULL, 619912782122617ULL, 515681498488209ULL, 1675866144246843ULL, 811716020969981ULL, 1125515272217398ULL, 1398917918287342ULL, 1301680949183175ULL, 726474739583734ULL, 587246193475200ULL, 1096581582611864ULL, 1469911826213486ULL, 1990099711206364ULL, 1256496099816508ULL, 2019924615195672ULL, 1251232456707555ULL, 2042971196009755ULL, 214061878479265ULL, 115385726395472ULL, 1677875239524132ULL, 756888883383540ULL, 1153862117756233ULL, 503391530851096ULL, 946070017477513ULL, 1878319040542579ULL, 1101349418586920ULL, 793245696431613ULL, 397920495357645ULL, 2174023872951112ULL, 1517867915189593ULL, 1829855041462995ULL, 1046709983503619ULL, 424081940711857ULL, 2112438073094647ULL, 1504338467349861ULL, 2244574127374532ULL, 2136937537441911ULL, 1741150838990304ULL, 25894628400571ULL, 512213526781178ULL, 1168384260796379ULL, 1424607682379833ULL, 938677789731564ULL, 872882241891896ULL, 1713199397007700ULL, 1410496326218359ULL, 854379752407031ULL, 465141611727634ULL, 315176937037857ULL, 1020115054571233ULL, 1856290111077229ULL, 2028366269898204ULL, 1432980880307543ULL, 469932710425448ULL, 581165267592247ULL, 496399148156603ULL, 2063435226705903ULL, 2116841086237705ULL, 498272567217048ULL, 1829438076967906ULL, 1573925801278491ULL, 460763576329867ULL, 1705264723728225ULL, 999514866082412ULL, 29635061779362ULL, 1884233592281020ULL, 1449755591461338ULL, 42579292783222ULL, 1869504355369200ULL, 495506004805251ULL, 264073104888427ULL, 2088880861028612ULL, 104646456386576ULL, 1258445191399967ULL, 1348736801545799ULL, 2068276361286613ULL, 884897216646374ULL, 922387476801376ULL, 1043886580402805ULL, 1240883498470831ULL, 1601554651937110ULL, 804382935289482ULL, 512379564477239ULL, 1466384519077032ULL, 1280698500238386ULL, 211303836685749ULL, 2081725624793803ULL, 545247644516879ULL, 215313359330384ULL, 286479751145614ULL, 2213650281751636ULL, 2164927945999874ULL, 2072162991540882ULL, 1443769115444779ULL, 1581473274363095ULL, 434633875922699ULL, 340456055781599ULL, 373043091080189ULL, 839476566531776ULL, 1856706858509978ULL, 931616224909153ULL, 1888181317414065ULL, 213654322650262ULL, 1161078103416244ULL, 1822042328851513ULL, 915817709028812ULL, 1828297056698188ULL, 1212017130909403ULL, 60258343247333ULL, 342085800008230ULL, 930240559508270ULL, 1549884999174952ULL, 809895264249462ULL, 184726257947682ULL, 1157065433504828ULL, 1209999630381477ULL, 999920399374391ULL, 1714770150788163ULL, 2026130985413228ULL, 506776632883140ULL, 1349042668246528ULL, 1937232292976967ULL, 942302637530730ULL, 160211904766226ULL, 1042724500438571ULL, 212454865139142ULL, 244104425172642ULL, 1376990622387496ULL, 76126752421227ULL, 1027540886376422ULL, 1912210655133026ULL, 13410411589575ULL, 1475856708587773ULL, 615563352691682ULL, 1446629324872644ULL, 1683670301784014ULL, 1049873327197127ULL, 1826401704084838ULL, 2032577048760775ULL, 1922203607878853ULL, 836708788764806ULL, 2193084654695012ULL, 1342923183256659ULL, 849356986294271ULL, 1228863973965618ULL, 94886161081867ULL, 1423288430204892ULL, 2016167528707016ULL, 1633187660972877ULL, 1550621242301752ULL, 340630244512994ULL, 2103577710806901ULL, 221625016538931ULL, 421544147350960ULL, 580428704555156ULL, 1479831381265617ULL, 518057926544698ULL, 955027348790630ULL, 1326749172561598ULL, 1118304625755967ULL, 1994005916095176ULL, 1799757332780663ULL, 751343129396941ULL, 1468672898746144ULL, 1451689964451386ULL, 755070293921171ULL, 904857405877052ULL, 1276087530766984ULL, 403986562858511ULL, 1530661255035337ULL, 1644972908910502ULL, 1370170080438957ULL, 139839536695744ULL, 909930462436512ULL, 1899999215356933ULL, 635992381064566ULL, 788740975837654ULL, 224241231493695ULL, 1267090030199302ULL, 998908061660139ULL, 1784537499699278ULL, 859195370018706ULL, 1953966091439379ULL, 2189271820076010ULL, 2039067059943978ULL, 1526694380855202ULL, 2040321513194941ULL, 329922071218689ULL, 1953032256401326ULL, 989631424403521ULL, 328825014934242ULL, 9407151397696ULL, 63551373671268ULL, 1624728632895792ULL, 1608324920739262ULL, 1178239350351945ULL, 1198077399579702ULL, 277620088676229ULL, 1775359437312528ULL, 1653558177737477ULL, 1652066043408850ULL, 1063359889686622ULL, 1975063804860653ULL }; #if defined(__cplusplus) } #endif #define __internal_Hacl_Ed25519_PrecompTable_H_DEFINED #endif