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