Revision control
Copy as Markdown
Other Tools
//! This file is auto-generated by HACL*.
#![allow(non_snake_case)]
#![allow(non_upper_case_globals)]
#![allow(non_camel_case_types)]
#![allow(unused_assignments)]
#![allow(unreachable_patterns)]
pub(crate) const precomp_basepoint_table_w4: [u64; 192] = [
0u64,
0u64,
0u64,
0u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
0u64,
0u64,
0u64,
0u64,
8784043285714375740u64,
8483257759279461889u64,
8789745728267363600u64,
1770019616739251654u64,
15992936863339206154u64,
10037038012062884956u64,
15197544864945402661u64,
9615747158586711429u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
10634854829044225757u64,
351552716085025155u64,
10645315080955407736u64,
3609262091244858135u64,
15760741698986874125u64,
14936374388219697827u64,
15751360096993017895u64,
18012233706239762398u64,
1993877568177495041u64,
10345888787846536528u64,
7746511691117935375u64,
14517043990409914413u64,
14122549297570634151u64,
16934610359517083771u64,
5724511325497097418u64,
8983432969107448705u64,
2687429970334080245u64,
16525396802810050288u64,
7602596488871585854u64,
4813919589149203084u64,
7680395813780804519u64,
6687709583048023590u64,
18086445169104142027u64,
9637814708330203929u64,
14785108459960679090u64,
3838023279095023581u64,
3555615526157830307u64,
5177066488380472871u64,
18218186719108038403u64,
16281556341699656105u64,
1524227924561461191u64,
4148060517641909597u64,
2858290374115363433u64,
8942772026334130620u64,
3034451298319885113u64,
8447866036736640940u64,
11204933433076256578u64,
18333595740249588297u64,
8259597024804538246u64,
9539734295777539786u64,
9797290423046626413u64,
5777303437849646537u64,
8739356909899132020u64,
14815960973766782158u64,
15286581798204509801u64,
17597362577777019682u64,
13259283710820519742u64,
10501322996899164670u64,
1221138904338319642u64,
14586685489551951885u64,
895326705426031212u64,
14398171728560617847u64,
9592550823745097391u64,
17240998489162206026u64,
8085479283308189196u64,
14844657737893882826u64,
15923425394150618234u64,
2997808084773249525u64,
494323555453660587u64,
1215695327517794764u64,
9476207381098391690u64,
7480789678419122995u64,
15212230329321082489u64,
436189395349576388u64,
17377474396456660834u64,
15237013929655017939u64,
11444428846883781676u64,
5112749694521428575u64,
950829367509872073u64,
17665036182057559519u64,
17205133339690002313u64,
16233765170251334549u64,
10122775683257972591u64,
3352514236455632420u64,
9143148522359954691u64,
601191684005658860u64,
13398772186646349998u64,
15512696600132928431u64,
9128416073728948653u64,
11233051033546138578u64,
6769345682610122833u64,
10823233224575054288u64,
9997725227559980175u64,
6733425642852897415u64,
16302206918151466066u64,
1669330822143265921u64,
2661645605036546002u64,
17182558479745802165u64,
1165082692376932040u64,
9470595929011488359u64,
6142147329285324932u64,
4829075085998111287u64,
10231370681107338930u64,
9591876895322495239u64,
10316468561384076618u64,
11592503647238064235u64,
13395813606055179632u64,
511127033980815508u64,
12434976573147649880u64,
3425094795384359127u64,
6816971736303023445u64,
15444670609021139344u64,
9464349818322082360u64,
16178216413042376883u64,
9595540370774317348u64,
7229365182662875710u64,
4601177649460012843u64,
5455046447382487090u64,
10854066421606187521u64,
15913416821879788071u64,
2297365362023460173u64,
2603252216454941350u64,
6768791943870490934u64,
15705936687122754810u64,
9537096567546600694u64,
17580538144855035062u64,
4496542856965746638u64,
8444341625922124942u64,
12191263903636183168u64,
17427332907535974165u64,
14307569739254103736u64,
13900598742063266169u64,
7176996424355977650u64,
5709008170379717479u64,
14471312052264549092u64,
1464519909491759867u64,
3328154641049602121u64,
13020349337171136774u64,
2772166279972051938u64,
10854476939425975292u64,
1967189930534630940u64,
2802919076529341959u64,
14792226094833519208u64,
14675640928566522177u64,
14838974364643800837u64,
17631460696099549980u64,
17434186275364935469u64,
2665648200587705473u64,
13202122464492564051u64,
7576287350918073341u64,
2272206013910186424u64,
14558761641743937843u64,
5675729149929979729u64,
9043135187561613166u64,
11750149293830589225u64,
740555197954307911u64,
9871738005087190699u64,
17178667634283502053u64,
18046255991533013265u64,
4458222096988430430u64,
8452427758526311627u64,
13825286929656615266u64,
13956286357198391218u64,
15875692916799995079u64,
10634895319157013920u64,
13230116118036304207u64,
8795317393614625606u64,
7001710806858862020u64,
7949746088586183478u64,
14677556044923602317u64,
11184023437485843904u64,
11215864722023085094u64,
6444464081471519014u64,
1706241174022415217u64,
8243975633057550613u64,
15502902453836085864u64,
3799182188594003953u64,
3538840175098724094u64,
];
pub(crate) const precomp_g_pow2_64_table_w4: [u64; 192] = [
0u64,
0u64,
0u64,
0u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
0u64,
0u64,
0u64,
0u64,
1499621593102562565u64,
16692369783039433128u64,
15337520135922861848u64,
5455737214495366228u64,
17827017231032529600u64,
12413621606240782649u64,
2290483008028286132u64,
15752017553340844820u64,
4846430910634234874u64,
10861682798464583253u64,
15404737222404363049u64,
363586619281562022u64,
9866710912401645115u64,
1162548847543228595u64,
7649967190445130486u64,
5212340432230915749u64,
7572620550182916491u64,
14876145112448665096u64,
2063227348838176167u64,
3519435548295415847u64,
8390400282019023103u64,
17666843593163037841u64,
9450204148816496323u64,
8483374507652916768u64,
6254661047265818424u64,
16382127809582285023u64,
125359443771153172u64,
1374336701588437897u64,
11362596098420127726u64,
2101654420738681387u64,
12772780342444840510u64,
12546934328908550060u64,
8331880412333790397u64,
11687262051473819904u64,
8926848496503457587u64,
9603974142010467857u64,
13199952163826973175u64,
2189856264898797734u64,
11356074861870267226u64,
2027714896422561895u64,
5261606367808050149u64,
153855954337762312u64,
6375919692894573986u64,
12364041207536146533u64,
1891896010455057160u64,
1568123795087313171u64,
18138710056556660101u64,
6004886947510047736u64,
4811859325589542932u64,
3618763430148954981u64,
11434521746258554122u64,
10086341535864049427u64,
8073421629570399570u64,
12680586148814729338u64,
9619958020761569612u64,
15827203580658384478u64,
12832694810937550406u64,
14977975484447400910u64,
5478002389061063653u64,
14731136312639060880u64,
4317867687275472033u64,
6642650962855259884u64,
2514254944289495285u64,
14231405641534478436u64,
4045448346091518946u64,
8985477013445972471u64,
8869039454457032149u64,
4356978486208692970u64,
10805288613335538577u64,
12832353127812502042u64,
4576590051676547490u64,
6728053735138655107u64,
17814206719173206184u64,
79790138573994940u64,
17920293215101822267u64,
13422026625585728864u64,
5018058010492547271u64,
110232326023384102u64,
10834264070056942976u64,
15222249086119088588u64,
15119439519142044997u64,
11655511970063167313u64,
1614477029450566107u64,
3619322817271059794u64,
9352862040415412867u64,
14017522553242747074u64,
13138513643674040327u64,
3610195242889455765u64,
8371069193996567291u64,
12670227996544662654u64,
1205961025092146303u64,
13106709934003962112u64,
4350113471327723407u64,
15060941403739680459u64,
13639127647823205030u64,
10790943339357725715u64,
498760574280648264u64,
17922071907832082887u64,
15122670976670152145u64,
6275027991110214322u64,
7250912847491816402u64,
15206617260142982380u64,
3385668313694152877u64,
17522479771766801905u64,
2965919117476170655u64,
1553238516603269404u64,
5820770015631050991u64,
4999445222232605348u64,
9245650860833717444u64,
1508811811724230728u64,
5190684913765614385u64,
15692927070934536166u64,
12981978499190500902u64,
5143491963193394698u64,
7705698092144084129u64,
581120653055084783u64,
13886552864486459714u64,
6290301270652587255u64,
8663431529954393128u64,
17033405846475472443u64,
5206780355442651635u64,
12580364474736467688u64,
17934601912005283310u64,
15119491731028933652u64,
17848231399859044858u64,
4427673319524919329u64,
2673607337074368008u64,
14034876464294699949u64,
10938948975420813697u64,
15202340615298669183u64,
5496603454069431071u64,
2486526142064906845u64,
4507882119510526802u64,
13888151172411390059u64,
15049027856908071726u64,
9667231543181973158u64,
6406671575277563202u64,
3395801050331215139u64,
9813607433539108308u64,
2681417728820980381u64,
18407064643927113994u64,
7707177692113485527u64,
14218149384635317074u64,
3658668346206375919u64,
15404713991002362166u64,
10152074687696195207u64,
10926946599582128139u64,
16907298600007085320u64,
16544287219664720279u64,
11007075933432813205u64,
8652245965145713599u64,
7857626748965990384u64,
5602306604520095870u64,
2525139243938658618u64,
14405696176872077447u64,
18432270482137885332u64,
9913880809120071177u64,
16896141737831216972u64,
7484791498211214829u64,
15635259968266497469u64,
8495118537612215624u64,
4915477980562575356u64,
16453519279754924350u64,
14462108244565406969u64,
14837837755237096687u64,
14130171078892575346u64,
15423793222528491497u64,
5460399262075036084u64,
16085440580308415349u64,
26873200736954488u64,
5603655807457499550u64,
3342202915871129617u64,
1604413932150236626u64,
9684226585089458974u64,
1213229904006618539u64,
6782978662408837236u64,
11197029877749307372u64,
14085968786551657744u64,
17352273610494009342u64,
7876582961192434984u64,
];
pub(crate) const precomp_g_pow2_128_table_w4: [u64; 192] = [
0u64,
0u64,
0u64,
0u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
0u64,
0u64,
0u64,
0u64,
14619254753077084366u64,
13913835116514008593u64,
15060744674088488145u64,
17668414598203068685u64,
10761169236902342334u64,
15467027479157446221u64,
14989185522423469618u64,
14354539272510107003u64,
14298211796392133693u64,
13270323784253711450u64,
13380964971965046957u64,
8686204248456909699u64,
17434630286744937066u64,
1355903775279084720u64,
7554695053550308662u64,
11354971222741863570u64,
564601613420749879u64,
8466325837259054896u64,
10752965181772434263u64,
11405876547368426319u64,
13791894568738930940u64,
8230587134406354675u64,
12415514098722758608u64,
18414183046995786744u64,
15508000368227372870u64,
5781062464627999307u64,
15339429052219195590u64,
16038703753810741903u64,
9587718938298980714u64,
4822658817952386407u64,
1376351024833260660u64,
1120174910554766702u64,
1730170933262569274u64,
5187428548444533500u64,
16242053503368957131u64,
3036811119519868279u64,
1760267587958926638u64,
170244572981065185u64,
8063080791967388171u64,
4824892826607692737u64,
16286391083472040552u64,
11945158615253358747u64,
14096887760410224200u64,
1613720831904557039u64,
14316966673761197523u64,
17411006201485445341u64,
8112301506943158801u64,
2069889233927989984u64,
10082848378277483927u64,
3609691194454404430u64,
6110437205371933689u64,
9769135977342231601u64,
11977962151783386478u64,
18088718692559983573u64,
11741637975753055u64,
11110390325701582190u64,
1341402251566067019u64,
3028229550849726478u64,
10438984083997451310u64,
12730851885100145709u64,
11524169532089894189u64,
4523375903229602674u64,
2028602258037385622u64,
17082839063089388410u64,
6103921364634113167u64,
17066180888225306102u64,
11395680486707876195u64,
10952892272443345484u64,
8792831960605859401u64,
14194485427742325139u64,
15146020821144305250u64,
1654766014957123343u64,
7955526243090948551u64,
3989277566080493308u64,
12229385116397931231u64,
13430548930727025562u64,
3434892688179800602u64,
8431998794645622027u64,
12132530981596299272u64,
2289461608863966999u64,
18345870950201487179u64,
13517947207801901576u64,
5213113244172561159u64,
17632986594098340879u64,
4405251818133148856u64,
11783009269435447793u64,
9332138983770046035u64,
12863411548922539505u64,
3717030292816178224u64,
10026078446427137374u64,
11167295326594317220u64,
12425328773141588668u64,
5760335125172049352u64,
9016843701117277863u64,
5657892835694680172u64,
11025130589305387464u64,
1368484957977406173u64,
17361351345281258834u64,
1907113641956152700u64,
16439233413531427752u64,
5893322296986588932u64,
14000206906171746627u64,
14979266987545792900u64,
6926291766898221120u64,
7162023296083360752u64,
14762747553625382529u64,
12610831658612406849u64,
10462926899548715515u64,
4794017723140405312u64,
5234438200490163319u64,
8019519110339576320u64,
7194604241290530100u64,
12626770134810813246u64,
10793074474236419890u64,
11323224347913978783u64,
16831128015895380245u64,
18323094195124693378u64,
2361097165281567692u64,
15755578675014279498u64,
14289876470325854580u64,
12856787656093616839u64,
3578928531243900594u64,
3847532758790503699u64,
8377953190224748743u64,
3314546646092744596u64,
800810188859334358u64,
4626344124229343596u64,
6620381605850876621u64,
11422073570955989527u64,
12676813626484814469u64,
16725029886764122240u64,
16648497372773830008u64,
9135702594931291048u64,
16080949688826680333u64,
11528096561346602947u64,
2632498067099740984u64,
11583842699108800714u64,
8378404864573610526u64,
1076560261627788534u64,
13836015994325032828u64,
11234295937817067909u64,
5893659808396722708u64,
11277421142886984364u64,
8968549037166726491u64,
14841374331394032822u64,
9967344773947889341u64,
8799244393578496085u64,
5094686877301601410u64,
8780316747074726862u64,
9119697306829835718u64,
15381243327921855368u64,
2686250164449435196u64,
16466917280442198358u64,
13791704489163125216u64,
16955859337117924272u64,
17112836394923783642u64,
4639176427338618063u64,
16770029310141094964u64,
11049953922966416185u64,
12012669590884098968u64,
4859326885929417214u64,
896380084392586061u64,
7153028362977034008u64,
10540021163316263301u64,
9318277998512936585u64,
18344496977694796523u64,
11374737400567645494u64,
17158800051138212954u64,
18343197867863253153u64,
18204799297967861226u64,
15798973531606348828u64,
9870158263408310459u64,
17578869832774612627u64,
8395748875822696932u64,
15310679007370670872u64,
11205576736030808860u64,
10123429210002838967u64,
5910544144088393959u64,
14016615653353687369u64,
11191676704772957822u64,
];
pub(crate) const precomp_g_pow2_192_table_w4: [u64; 192] = [
0u64,
0u64,
0u64,
0u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
0u64,
0u64,
0u64,
0u64,
7870395003430845958u64,
18001862936410067720u64,
8006461232116967215u64,
5921313779532424762u64,
10702113371959864307u64,
8070517410642379879u64,
7139806720777708306u64,
8253938546650739833u64,
17490482834545705718u64,
1065249776797037500u64,
5018258455937968775u64,
14100621120178668337u64,
8392845221328116213u64,
14630296398338540788u64,
4268947906723414372u64,
9231207002243517909u64,
14261219637616504262u64,
7786881626982345356u64,
11412720751765882139u64,
14119585051365330009u64,
15281626286521302128u64,
6350171933454266732u64,
16559468304937127866u64,
13200760478271693417u64,
6733381546280350776u64,
3801404890075189193u64,
2741036364686993903u64,
3218612940540174008u64,
10894914335165419505u64,
11862941430149998362u64,
4223151729402839584u64,
2913215088487087887u64,
14562168920104952953u64,
2170089393468287453u64,
10520900655016579352u64,
7040362608949989273u64,
8376510559381705307u64,
9142237200448131532u64,
5696859948123854080u64,
925422306716081180u64,
11155545953469186421u64,
1888208646862572812u64,
11151095998248845721u64,
15793503271680275267u64,
7729877044494854851u64,
6235134673193032913u64,
7364280682182401564u64,
5479679373325519985u64,
17966037684582301763u64,
14140891609330279185u64,
5814744449740463867u64,
5652588426712591652u64,
774745682988690912u64,
13228255573220500373u64,
11949122068786859397u64,
8021166392900770376u64,
7994323710948720063u64,
9924618472877849977u64,
17618517523141194266u64,
2750424097794401714u64,
15481749570715253207u64,
14646964509921760497u64,
1037442848094301355u64,
6295995947389299132u64,
16915049722317579514u64,
10493877400992990313u64,
18391008753060553521u64,
483942209623707598u64,
2017775662838016613u64,
5933251998459363553u64,
11789135019970707407u64,
5484123723153268336u64,
13246954648848484954u64,
4774374393926023505u64,
14863995618704457336u64,
13220153167104973625u64,
5988445485312390826u64,
17580359464028944682u64,
7297100131969874771u64,
379931507867989375u64,
10927113096513421444u64,
17688881974428340857u64,
4259872578781463333u64,
8573076295966784472u64,
16389829450727275032u64,
1667243868963568259u64,
17730726848925960919u64,
11408899874569778008u64,
3576527582023272268u64,
16492920640224231656u64,
7906130545972460130u64,
13878604278207681266u64,
41446695125652041u64,
8891615271337333503u64,
2594537723613594470u64,
7699579176995770924u64,
147458463055730655u64,
12120406862739088406u64,
12044892493010567063u64,
8554076749615475136u64,
1005097692260929999u64,
2687202654471188715u64,
9457588752176879209u64,
17472884880062444019u64,
9792097892056020166u64,
2525246678512797150u64,
15958903035313115662u64,
11336038170342247032u64,
11560342382835141123u64,
6212009033479929024u64,
8214308203775021229u64,
8475469210070503698u64,
13287024123485719563u64,
12956951963817520723u64,
10693035819908470465u64,
11375478788224786725u64,
16934625208487120398u64,
10094585729115874495u64,
2763884524395905776u64,
13535890148969964883u64,
13514657411765064358u64,
9903074440788027562u64,
17324720726421199990u64,
2273931039117368789u64,
3442641041506157854u64,
1119853641236409612u64,
12037070344296077989u64,
581736433335671746u64,
6019150647054369174u64,
14864096138068789375u64,
6652995210998318662u64,
12773883697029175304u64,
12751275631451845119u64,
11449095003038250478u64,
1025805267334366480u64,
2764432500300815015u64,
18274564429002844381u64,
10445634195592600351u64,
11814099592837202735u64,
5006796893679120289u64,
6908397253997261914u64,
13266696965302879279u64,
7768715053015037430u64,
3569923738654785686u64,
5844853453464857549u64,
1837340805629559110u64,
1034657624388283114u64,
711244516069456460u64,
12519286026957934814u64,
2613464944620837619u64,
10003023321338286213u64,
7291332092642881376u64,
9832199564117004897u64,
3280736694860799890u64,
6416452202849179874u64,
7326961381798642069u64,
8435688798040635029u64,
16630141263910982958u64,
17222635514422533318u64,
9482787389178881499u64,
836561194658263905u64,
3405319043337616649u64,
2786146577568026518u64,
7625483685691626321u64,
6728084875304656716u64,
1140997959232544268u64,
12847384827606303792u64,
1719121337754572070u64,
12863589482936438532u64,
3880712899640530862u64,
2748456882813671564u64,
4775988900044623019u64,
8937847374382191162u64,
3767367347172252295u64,
13468672401049388646u64,
14359032216842397576u64,
2002555958685443975u64,
16488678606651526810u64,
11826135409597474760u64,
15296495673182508601u64,
];
pub(crate) const precomp_basepoint_table_w5: [u64; 384] = [
0u64,
0u64,
0u64,
0u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
0u64,
0u64,
0u64,
0u64,
8784043285714375740u64,
8483257759279461889u64,
8789745728267363600u64,
1770019616739251654u64,
15992936863339206154u64,
10037038012062884956u64,
15197544864945402661u64,
9615747158586711429u64,
1u64,
18446744069414584320u64,
18446744073709551615u64,
4294967294u64,
10634854829044225757u64,
351552716085025155u64,
10645315080955407736u64,
3609262091244858135u64,
15760741698986874125u64,
14936374388219697827u64,
15751360096993017895u64,
18012233706239762398u64,
1993877568177495041u64,
10345888787846536528u64,
7746511691117935375u64,
14517043990409914413u64,
14122549297570634151u64,
16934610359517083771u64,
5724511325497097418u64,
8983432969107448705u64,
2687429970334080245u64,
16525396802810050288u64,
7602596488871585854u64,
4813919589149203084u64,
7680395813780804519u64,
6687709583048023590u64,
18086445169104142027u64,
9637814708330203929u64,
14785108459960679090u64,
3838023279095023581u64,
3555615526157830307u64,
5177066488380472871u64,
18218186719108038403u64,
16281556341699656105u64,
1524227924561461191u64,
4148060517641909597u64,
2858290374115363433u64,
8942772026334130620u64,
3034451298319885113u64,
8447866036736640940u64,
11204933433076256578u64,
18333595740249588297u64,
8259597024804538246u64,
9539734295777539786u64,
9797290423046626413u64,
5777303437849646537u64,
8739356909899132020u64,
14815960973766782158u64,
15286581798204509801u64,
17597362577777019682u64,
13259283710820519742u64,
10501322996899164670u64,
1221138904338319642u64,
14586685489551951885u64,
895326705426031212u64,
14398171728560617847u64,
9592550823745097391u64,
17240998489162206026u64,
8085479283308189196u64,
14844657737893882826u64,
15923425394150618234u64,
2997808084773249525u64,
494323555453660587u64,
1215695327517794764u64,
9476207381098391690u64,
7480789678419122995u64,
15212230329321082489u64,
436189395349576388u64,
17377474396456660834u64,
15237013929655017939u64,
11444428846883781676u64,
5112749694521428575u64,
950829367509872073u64,
17665036182057559519u64,
17205133339690002313u64,
16233765170251334549u64,
10122775683257972591u64,
3352514236455632420u64,
9143148522359954691u64,
601191684005658860u64,
13398772186646349998u64,
15512696600132928431u64,
9128416073728948653u64,
11233051033546138578u64,
6769345682610122833u64,
10823233224575054288u64,
9997725227559980175u64,
6733425642852897415u64,
16302206918151466066u64,
1669330822143265921u64,
2661645605036546002u64,
17182558479745802165u64,
1165082692376932040u64,
9470595929011488359u64,
6142147329285324932u64,
4829075085998111287u64,
10231370681107338930u64,
9591876895322495239u64,
10316468561384076618u64,
11592503647238064235u64,
13395813606055179632u64,
511127033980815508u64,
12434976573147649880u64,
3425094795384359127u64,
6816971736303023445u64,
15444670609021139344u64,
9464349818322082360u64,
16178216413042376883u64,
9595540370774317348u64,
7229365182662875710u64,
4601177649460012843u64,
5455046447382487090u64,
10854066421606187521u64,
15913416821879788071u64,
2297365362023460173u64,
2603252216454941350u64,
6768791943870490934u64,
15705936687122754810u64,
9537096567546600694u64,
17580538144855035062u64,
4496542856965746638u64,
8444341625922124942u64,
12191263903636183168u64,
17427332907535974165u64,
14307569739254103736u64,
13900598742063266169u64,
7176996424355977650u64,
5709008170379717479u64,
14471312052264549092u64,
1464519909491759867u64,
3328154641049602121u64,
13020349337171136774u64,
2772166279972051938u64,
10854476939425975292u64,
1967189930534630940u64,
2802919076529341959u64,
14792226094833519208u64,
14675640928566522177u64,
14838974364643800837u64,
17631460696099549980u64,
17434186275364935469u64,
2665648200587705473u64,
13202122464492564051u64,
7576287350918073341u64,
2272206013910186424u64,
14558761641743937843u64,
5675729149929979729u64,
9043135187561613166u64,
11750149293830589225u64,
740555197954307911u64,
9871738005087190699u64,
17178667634283502053u64,
18046255991533013265u64,
4458222096988430430u64,
8452427758526311627u64,
13825286929656615266u64,
13956286357198391218u64,
15875692916799995079u64,
10634895319157013920u64,
13230116118036304207u64,
8795317393614625606u64,
7001710806858862020u64,
7949746088586183478u64,
14677556044923602317u64,
11184023437485843904u64,
11215864722023085094u64,
6444464081471519014u64,
1706241174022415217u64,
8243975633057550613u64,
15502902453836085864u64,
3799182188594003953u64,
3538840175098724094u64,
13240193491554624643u64,
12365034249541329920u64,
2924326828590977357u64,
5687195797140589099u64,
16880427227292834531u64,
9691471435758991112u64,
16642385273732487288u64,
12173806747523009914u64,
13142722756877876849u64,
8370377548305121979u64,
17988526053752025426u64,
4818750752684100334u64,
5669241919350361655u64,
4964810303238518540u64,
16709712747671533191u64,
4461414404267448242u64,
3971798785139504238u64,
6276818948740422136u64,
1426735892164275762u64,
7943622674892418919u64,
9864274225563929680u64,
57815533745003233u64,
10893588105168960233u64,
15739162732907069535u64,
3923866849462073470u64,
12279826158399226875u64,
1533015761334846582u64,
15860156818568437510u64,
8252625373831297988u64,
9666953804812706358u64,
8767785238646914634u64,
14382179044941403551u64,
10401039907264254245u64,
8584860003763157350u64,
3120462679504470266u64,
8670255778748340069u64,
5313789577940369984u64,
16977072364454789224u64,
12199578693972188324u64,
18211098771672599237u64,
12868831556008795030u64,
5310155061431048194u64,
18114153238435112606u64,
14482365809278304512u64,
12520721662723001511u64,
405943624021143002u64,
8146944101507657423u64,
181739317780393495u64,
81743892273670099u64,
14759561962550473930u64,
4592623849546992939u64,
6916440441743449719u64,
1304610503530809833u64,
5464930909232486441u64,
15414883617496224671u64,
8129283345256790u64,
18294252198413739489u64,
17394115281884857288u64,
7808348415224731235u64,
13195566655747230608u64,
8568194219353949094u64,
15329813048672122440u64,
9604275495885785744u64,
1577712551205219835u64,
15964209008022052790u64,
15087297920782098160u64,
3946031512438511898u64,
10050061168984440631u64,
11382452014533138316u64,
6313670788911952792u64,
12015989229696164014u64,
5946702628076168852u64,
5219995658774362841u64,
12230141881068377972u64,
12361195202673441956u64,
4732862275653856711u64,
17221430380805252370u64,
15397525953897375810u64,
16557437297239563045u64,
10101683801868971351u64,
1402611372245592868u64,
1931806383735563658u64,
10991705207471512479u64,
861333583207471392u64,
15207766844626322355u64,
9224628129811432393u64,
3497069567089055613u64,
11956632757898590316u64,
8733729372586312960u64,
18091521051714930927u64,
77582787724373283u64,
9922437373519669237u64,
3079321456325704615u64,
12171198408512478457u64,
17179130884012147596u64,
6839115479620367181u64,
4421032569964105406u64,
10353331468657256053u64,
17400988720335968824u64,
17138855889417480540u64,
4507980080381370611u64,
10703175719793781886u64,
12598516658725890426u64,
8353463412173898932u64,
17703029389228422404u64,
9313111267107226233u64,
5441322942995154196u64,
8952817660034465484u64,
17571113341183703118u64,
7375087953801067019u64,
13381466302076453648u64,
3218165271423914596u64,
16956372157249382685u64,
509080090049418841u64,
13374233893294084913u64,
2988537624204297086u64,
4979195832939384620u64,
3803931594068976394u64,
10731535883829627646u64,
12954845047607194278u64,
10494298062560667399u64,
4967351022190213065u64,
13391917938145756456u64,
951370484866918160u64,
13531334179067685307u64,
12868421357919390599u64,
15918857042998130258u64,
17769743831936974016u64,
7137921979260368809u64,
12461369180685892062u64,
827476514081935199u64,
15107282134224767230u64,
10084765752802805748u64,
3303739059392464407u64,
17859532612136591428u64,
10949414770405040164u64,
12838613589371008785u64,
5554397169231540728u64,
18375114572169624408u64,
15649286703242390139u64,
2957281557463706877u64,
14000350446219393213u64,
14355199721749620351u64,
2730856240099299695u64,
17528131000714705752u64,
2537498525883536360u64,
6121058967084509393u64,
16897667060435514221u64,
12367869599571112440u64,
3388831797050807508u64,
16791449724090982798u64,
2673426123453294928u64,
11369313542384405846u64,
15641960333586432634u64,
15080962589658958379u64,
7747943772340226569u64,
8075023376199159152u64,
8485093027378306528u64,
13503706844122243648u64,
8401961362938086226u64,
8125426002124226402u64,
9005399361407785203u64,
6847968030066906634u64,
11934937736309295197u64,
5116750888594772351u64,
2817039227179245227u64,
17724206901239332980u64,
4985702708254058578u64,
5786345435756642871u64,
17772527414940936938u64,
1201320251272957006u64,
15787430120324348129u64,
6305488781359965661u64,
12423900845502858433u64,
17485949424202277720u64,
2062237315546855852u64,
10353639467860902375u64,
2315398490451287299u64,
15394572894814882621u64,
232866113801165640u64,
7413443736109338926u64,
902719806551551191u64,
16568853118619045174u64,
14202214862428279177u64,
11719595395278861192u64,
5890053236389907647u64,
9996196494965833627u64,
12967056942364782577u64,
9034128755157395787u64,
17898204904710512655u64,
8229373445062993977u64,
13580036169519833644u64,
];