Quelle  p256_precomptable.rs

//! 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,
];