open Poseidon_utils

module Stubs = struct
  type ctxt

  external allocate_ctxt :
    state_size:int ->
    nb_full_rounds:int ->
    nb_partial_rounds:int ->
    batch_size:int ->
    ark:Bls12_381.Fr.t array ->
    mds:Bls12_381.Fr.t array array ->
    ctxt
    = "caml_bls12_381_hash_poseidon_allocate_ctxt_stubs_bytecode" "caml_bls12_381_hash_poseidon_allocate_ctxt_stubs"

  external get_state : Bls12_381.Fr.t array -> ctxt -> unit
    = "caml_bls12_381_hash_poseidon_get_state_stubs"

  external set_state : ctxt -> Bls12_381.Fr.t array -> unit
    = "caml_bls12_381_hash_poseidon_set_state_stubs"

  external get_state_size : ctxt -> int
    = "caml_bls12_381_hash_poseidon_get_state_size_stubs"

  external apply_permutation : ctxt -> unit
    = "caml_bls12_381_hash_poseidon_apply_permutation_stubs"
end

module Parameters = struct
  type t = {
    state_size : int;
    nb_of_partial_rounds : int;
    nb_of_full_rounds : int;
    batch_size : int;
    round_constants : Bls12_381.Fr.t array;
    linear_layer : Bls12_381.Fr.t array array;
  }

  (* Generated with the command below from ocaml-ec commit
     cd13dd0e984a4eeadd82e0ac4ce792c275bd3b18 [dune exec ./generate_ark.exe 8 56 3
     52435875175126190479447740508185965837690552500527637822603658699938581184513
     NomadicLabs] *)

  let state_size_3_ark =
    [|
      "51466596801245350172389236854912648222719187746298709105513845567941180611585";
      "21750751762978437653936573013155607200736969558902465208523342419237410586198";
      "12486517768781903523286807847370218034689963995541894791925792444351839473647";
      "20445718088460789875962943176961386089719184042145123661083866290956184640219";
      "27873160203424299876666416455237485949282512273439804047040763657322096149056";
      "41356063063918478660008355287283031045994439439052675999621074603564345282569";
      "39339901461669097862513996312696398098463519178491001542393778258774347097156";
      "9204042589329629203508256352213922752007565761246017599071231880772962888313";
      "44872792620396140616818721079703154415798612187578057809815607666928058754777";
      "15937726977018206908966109373834056579034465379649731865901151172854062328666";
      "23605712034497375740219228439343452998072299839093594319857450624289690266228";
      "6402638958817972947806346954920050102512724107777426591914400080844084499349";
      "3185239264644999224390913018332891687143438328474986546082170376396564918303";
      "8810128481422180179093610800905689707749830921384041843188605671660723745224";
      "23856254368860098877925830552890800356559853619873956523749705505858453741419";
      "24587049159258135725439557767222187037564112044982562605667614163816312730472";
      "22837536766890438293232796017074642678223630893636795777506185541273623237047";
      "9192015516308615812149895996678356120602200776491327365416854885711899134185";
      "4002652916865493677251257166117182479501804845054999793592382685603350748223";
      "33066348252219459468552045146523238597048287748451612668563453612283148717787";
      "22032405802641325275844419284045173476338377422793990841002770933934147271753";
      "40810499016480900907962993830032852958946905562531549979714594924288595159449";
      "11360048753112901991330610389408512769078774607723790648797196048769123341818";
      "31073120699274505130875191050788584204810084807427992815212547386082177411939";
      "38905424489726634595807315824887707754301482341060164517868666848234609856296";
      "16437589687938886598993201288686198745024640875414943299079721648754955896524";
      "9246415141807177921760679831767807305667023086044867913825908258624135672402";
      "43267134335847210508826260454424281515957785150826503791438907274325277067689";
      "47405994765042204778087426457971662098880376129631959037220571890293893837627";
      "51109501544539159334717344833663305202169784719089645141283241708762847921831";
      "28367352686904931835510258483164340654232741901091990185726515423922311395266";
      "49750106362878302307560487257360445042628424171940583005315598767946030678175";
      "45959469784902653889236043731939532829295000363517367441618551318205534438835";
      "27018375398598043392768159138944903620978890067620474698695220978535490993662";
      "37680060127197925845671480407334293104013784691230898581176604640776871595820";
      "10072365749347322273683640976003223868449058525371389769456254873788829510856";
      "5776958426313577264021166002700070711779258526703552908022966622941040975486";
      "2052552766687385987890760301444512953288614090851121718631539540584797743813";
      "29589973335212398499653074528975769763663217998670026908669929887809390254086";
      "47176517056998440790693968750261830775359488909857950144871025285282622331205";
      "4044841108655017183998683299702141262167457310115051178539772996106040315055";
      "23145769961882962007007503964681965122021931165884937363089732236563915279899";
      "7603705117156652453963281055927587143772971225944827219299824918233735396544";
      "678587461188445034628596985861476825212606316443632929982806452029635142763";
      "43358198653600383869329744766691886425670686115842008451706594321104589073353";
      "29783989749004381558893964246285207519677877370947641650381151227672399441258";
      "46788814117768703246098518443423934593855222525287642802070140820481989754464";
      "47667240567568953271881931068585333300960463653436442752666537199724542862209";
      "36185825409915459203448245743109969343193138020188742950229819419575178293681";
      "10268626031678681962519788038923114866365639923373751230918298280203944789089";
      "22423180878570467317830579782624040309181433514468470079452795926252301501451";
      "27854213599947523969400957712485981554578482677686500615005910306191690675548";
      "32552238758912415934584820719305968737837410579067602670579118065160652867044";
      "27524020150199858721583983985008046355789957344374031640804833804334599991125";
      "11598691035533751109698164453612171297192910953856758972631340412485692367245";
      "19240281692025919244580609351663678384250073443852130798436970816624877123792";
      "19081743524319516787728673230184684387616956386482784328031473187929184929813";
      "13482824733237717061443533817612030042881142888904695925365483772570662398419";
      "24557586779364722370887646696339785224219486745231704250023468368642112077961";
      "49132695885737549819731989839786719093658647324506783818463101428078920152339";
      "47598003338017334595631291432676651103981450315484662200923020856309789617505";
      "29657580775158274893108525946918168971159316368647847989798236676167226124425";
      "2089871173039090298283861039787654594553968107879556266696645874401027551594";
      "17062674176584193145991964541286296980632589397952567044305875706903816798918";
      "39759050960205479940159986279409353005846424612008117451162722701140967479478";
      "22533616828186323521649895181466155821530425549183373709986149684843468562921";
      "11710329771453525931280127059748492796905639784050357470339844149929022650252";
      "28382230089609321965313624834250197889691846195285335974753263997326737343307";
      "17483468269617424580234048407267881623433885539437967900597355348779845904370";
      "15393678108977111939937458813237466536883800502542016725609655847312425800060";
      "35335672469945182745009570081451366206953223954844817103347451918365408472583";
      "18485543557533557196522038987860777539645907448847172084578647917456309932838";
      "35453109551100805378496992884404555281031142908343718145992408005796255932067";
      "26162388899534531304185889785161995414351042512495564813598387581820788701274";
      "30513272868498004256565910019709317337704607470343755267516092336967857454429";
      "7482438077715696595671300257575441576458965352889636767368860652528296466835";
      "4420972756750713378268292139245553512010082345332818480344347760992140415579";
      "45443072118542869094106210430408632401658283491040846320908484790994846489479";
      "4587498519897850005501095589592009810295823998176500983502979737014704428427";
      "20140268669484747984769809200637802968551617462409085249909344252279198873265";
      "29246773006012167464394782413277073922652993569428539217341804135677142314734";
      "2090453766635748262896094182234431405487694916721156619151573559829565285658";
      "28154797511075990999067437210883725325588221412791352016549710458849851400443";
      "7437576051454980648324143413673447321627481635285743115910231258907952681902";
      "47849325109234284589063376275405356989691773872687047237532536232042052359483";
      "12480987611376364480590099596287568108053904335043512585655935306753098846056";
      "35282772152784155873872416038091486728018085424598473101796189937824691931982";
      "44644309599357388823648910637703362148932670809274055496007925095230623381923";
      "40669859985254288073391010054507859022800795198091698303895855303568474914724";
      "49443653278257139506363224578511517450965492260748531903735461532886298470324";
      "28151927370999705099548977210331844092002690574491843105417307465011218883372";
      "1645107825636563552234056692699842524648459238860722695243162269478817742307";
      "20451009040028965353495911802150535366781462589345362185312598771266505204706";
      "27819682514111647266735378995664843430901566567232355462928465778589146617300";
      "9554102125843498587844759244118187314040788045621020914785690475852459244712";
      "19166777550065260996957117606165528594010042113228133002376856047908024628860";
      "26933579719124735456146556120749918059938219375765953757687070745926421730690";
      "43664899352313137143462906778788854871017052765412139294077435721003011363428";
      "36173458814979531375880943417934798141032455281648386700864729797402421147643";
      "11182517313384645430276258135181995604973901045769946685233925860600679925400";
      "18957585496621103259998572202861039692818169581041076732942953590132787413185";
      "990272065387976234207571590743065697998566272630425704533408985373371347703";
      "4566865954002478217870742631824891308061027453183663472158387320791808636718";
      "13275080024861611833879690760787568594881779009163813547717517171800075477326";
      "18280289328587924651942995072338785526297904605272226018248763384856128538194";
      "37393719051038483957290231134622753224758957341736360150179478705995454183736";
      "35471769041551236267108986169916522221022951796087962631717489467967242728989";
      "18313615850921029128115249415256953514199920171298188893865360820700589880640";
      "8649505551495013773478550513798423370916587725243242103915932173300802613836";
      "29426595573001164623970767658482684730540336753851606403197168017465308935012";
      "15800050789941506886367343947552537811144738254935176866599264324633404561668";
      "2388599729796011963372654009792156200311446590133223685676648683498130023426";
      "39710359146943858258478963255479846071237665235335480449874571631729609456656";
      "12539354052138844839668649494440055311612800274194314682724519322900896888667";
      "34775703808689652205221353219074769424059692664878491357308664495453361798542";
      "16602078529355937689782643082006360605957411241022465529030420514355243740084";
      "20279850236027730246187137397861434992518721949131469477063849268012331913542";
      "20700406847766119075096991790226756382972208779794861885683190244345925948772";
      "10767548586122669600841175107605340206307369812479898137983203022752955229420";
      "33780485917217277294437000521052335973598541648381872358473220524753392579944";
      "26053477836690449767759260916263153231466698419416254714069016291032716493795";
      "51075719579296898046678332991810264442802867440545970415662411469944202971572";
      "44425065795172674272025431261784423304992373196100933574446818463450861237636";
      "21673427825228648696679367470878911746787913779734335379612724957949663438503";
      "39500036723407342733895180253912956707996173847799994738506003893694134507820";
      "18814390742264124557923083818518430926773544077233525827507879093955534745943";
      "33285136419882565391925060802949863649369447257963104257237128389534667335431";
      "7242824697084765204242498009056108554791055701454269759053340822841847843590";
      "31173248312673499793759274086904799638353536404479301039538892557122201869326";
      "31186133094427811821728441124091409602329280228993044467507339271468902426067";
      "25737910716320624211587760844165755540380223663083209047341376780006952817951";
      "41007486903540773766178646801963663835738017272207371664092100665995867447476";
      "33733614421653704619906981612465553433605639878071728634533669588152171336923";
      "44508002187727655261274038726582531821774653664912931880913651223618478524203";
      "29308206009053294442851242412693308913204908282227130202504576346803290538114";
      "37195044959073314994498067496758410674853446343706809704471573374824766240756";
      "27750290920151880266415654177442693344449343287594569254432923001134909857161";
      "15765188586172333129026261765507777427830002956246082548695725135386026089531";
      "1723567911352974656239983052419150859691079784042460780666277969900550546629";
      "32624380698163043349452348170080919066187676495607088889037247382764371823304";
      "42332347907545864823851740450059178607636354773434217763190376183475294814740";
      "32851187296571784166842016235453193261263026420621113443940941911613891853263";
      "46515450218610398244495734725817662625773300495752440637456039809680716524335";
      "48802434618714806701215020572358407402163910104929505500552346872970874445024";
      "15041030433764412988626541831537854311766371887970954109236962491586466599144";
      "24914207471851043784197436527940466212674042052967065649457499415892446136159";
      "9071888319763577380151443506898914744736366395870413605185856133895174517345";
      "14324407136483074978482942921602872905704673210914714962854893980450386451889";
      "29042406409942557018444189727617456411092110677398829954434968404039936168367";
      "45298132425441112218235385216467264374863717020516284112024948473015955374084";
      "5848266257013307529285399749765616739303579930676051972945621978827280728485";
      "50258542824814649118248459254788489871100732773736051031417014804244168803608";
      "2211331518382464997157173039326358398024782525487574099479995890254668498248";
      "25495625009683093041292487489064498029388757676050435379647316032736436019034";
      "1673456300079357795623609138015785582077169647352697470259283949067483430156";
      "732875001458000671533092091268384759392197266180901126140125986324726970217";
      "15937486314053418275659636264513684188072392679031027560851186610858143116536";
      "37523979262473761872442642124630377368104280370382009467506872860620420272028";
      "1463301537361190248611634113301833004506917120571380701549297040601288661632";
      "15388046866006485479772795262309796656931214897645470303116977773763549826647";
      "24820458677922696742762859449292673635627885851532245057181102097543570979209";
      "42204379350085294410776773079715228191662735656426212256162333812793552403993";
      "1195814176795714164840835333744966813414161441324551406851397366147530373686";
      "16761973517502055324144398018035682278752429331149035356778515867109688520079";
      "5794935406580257517632452299232288835369749493148532249516641371649010994761";
      "28489054235450115341655557856812811692903805568161190542887091508558194202484";
      "46027667092982098207528356294714952530753544394086856091550981466630371723227";
      "36549545461270844973100848885411892468389487357334958172813302441582453767995";
      "27730798985447029088568033769773024804917434212093202895074054132301610442265";
      "30053494660111523933577748614419372203999341521131288200082766152193752930915";
      "42669519840379176591693261573919152190190830699417113996773900230897690941207";
      "40491463463369636128381274334600090418795787105664137021554873372325496120497";
      "37855317198077808209359933009653152621140711928666934200968394018548493650684";
      "30289339203582770465154470558134566153982220926251521920946038335272057457401";
      "27778690140622310321003540914723670899734999136798303644913768708258653156597";
      "3973394156719142858738591330892034076809261304074876595400530436577715032673";
      "34101414891901169069858357639409485174940075127343413252072373211617833012486";
      "24763874711353584430968413634679742313122411936945926412259875031351381484206";
      "36482519855965638025925823411871352935082631497149119671124638993468289313858";
      "33663960240182462215313666658229034428117630528389633368925326911863733915779";
      "24156616496917756781377614606496469046971000527652456728186486373912788616012";
      "17862377433968409862537980143869608526991820954912158743675488121333401401128";
      "9883166492675772730546061809268489723031153354700278026721716994418744028520";
      "651720966810612228203754272949951577724164458606405611640617175537862475287";
      "45029571820041579599811835408905235857907197206303946042784264756752149312055";
      "15218138019507525985285504884751281493313515412230279354014712290617793064643";
      "7889502179901137713876340968057633612399550484642109442993286207350478652780";
      "51114781021375925510384757787309929484526957562759351412663650152039538436129";
      "49153605396638540179308253872425727518164881509781489770081628829948751933325";
      "39446436805473057234521273352946756590838723177719005850741347955181052035907";
      "32522116151199401996556140465344290516461661003004520182401454275644784968841";
      "35709586671485611381280332540710898003892567989895109778435218770617343891091";
    |]
    |> Array.map Bls12_381.Fr.of_string

  (* Generated with the command below from ocaml-ec commit
     cd13dd0e984a4eeadd82e0ac4ce792c275bd3b18 [sage generate_mds.sage 3
     NomadicLabs
     52435875175126190479447740508185965837690552500527637822603658699938581184513] *)
  let state_size_3_mds =
    [|
      [|
        "48527463322097587091854420767453816291840635874249958396342138881138912067190";
        "11996084473350366483175782359948025962778681837397784970341328014763133439499";
        "5762620760470856886668821516275719951899130793312002468640314451189655462163";
      |];
      [|
        "43372445583202124108992832749257195116898314930070456682841601188523728879167";
        "22957843818027924237635625446720638788994914691706001027915412076310000455035";
        "45912682675908730967574769352367944608550602185952960151299062991058447525440";
      |];
      [|
        "31497265986585083362120862432803344331731948296021705208949638957481968624918";
        "51685553404028716702307457799190688643603961331524463449216360083627404197200";
        "46564571507606908377998846740442910952080430324196357605862207064906809134438";
      |];
    |]
    |> Array.map (Array.map Bls12_381.Fr.of_string)

  let security_128_state_size_3 =
    {
      state_size = 3;
      nb_of_full_rounds = 8;
      nb_of_partial_rounds = 56;
      batch_size = 3;
      round_constants = state_size_3_ark;
      linear_layer = state_size_3_mds;
    }

  let state_size_256_5_ark =
    (* Come from https://github.com/dusk-network/Hades252/tree/7a7a255f6cc48f892de5cf8935b5264eb8893852/assets *)
    [|
      "49485629590707188350627438543790601843164666730832802354167700559078990180805";
      "5252492454239988725999362667606361246537049278449296815482681202241423199030";
      "14618464101860214640501669418913406667488798576646720991952572594257377039502";
      "49620695691812425396881667059975042814057870860951834243048751692229624331677";
      "52370272705607335752267236318243264940083827067691749458235447563501832651257";
      "14710933242610523976995706443397757945742163741677668728466445608487118981880";
      "40295605676867759583334785789872476122167378326657237878145663333439589007156";
      "17275250730668933226474210235642934004873625116556680337206784052264566986455";
      "45633796471806275582583687299302600425559632837704148321307522586100540673964";
      "33681130375233352141656505268473716952957296224087839911967969212184713588195";
      "712629851673255722293534395801485044243728655856788348424319702704859382351";
      "43317142284252827604873495043870647060512975769565878032083607834275571303426";
      "49340354054830215768241644525595586576960916648952093483202539768057155695733";
      "51072133689923992485577335797823140838583096495379330871465525854048879509188";
      "46949696588385743239566882413656461741807666921366097544593880485391490027378";
      "20573821191096550126141597782760949856255209170402036553268647563825526870436";
      "27160407187556206874731839906107055583040719055315009650316032986707542736994";
      "50189849422262643653706645096664834529407274784147778804216234124791624405728";
      "36711845592560022607016872007330968632549815256229219571331231734465570541772";
      "35499690369690524959345453870997264497352033723668303049826986491601092626610";
      "16316511810555998552036883529281049006950270019860246764897773268401228568605";
      "24273505785788709750944619357321960159456240163658175721572690190239573216897";
      "38957445901173225235458499674711464149245486205504890531219786468849422975246";
      "11823467170230054064490275077272871963881914272709655957174399232209364647447";
      "49592360594196231864432308576338740596601726416914181276008583207908643556097";
      "3309012748654570967607135422003010755248166478871582757366403846071939043322";
      "28008997260349091544245311173997512340365040670749744770222988406313503293844";
      "7882946347332999275161185525751330966422116178677196163170258809540423320804";
      "29731010687109400386993771800155774620735785970162866907509352726525420687486";
      "23931998959081617445949503259792788311676984957946834382760056406764899364397";
      "20391484046421688653112911850234570788797563186823093327188237858525889539247";
      "22656719734855634367860470343411809786356929276974263964151006136177227714579";
      "42018013924524453942303746320960679879055521221983992010530880401352394546138";
      "34997396324562296578241314578708220449054628732531003841806342137992978809863";
      "42567292638455246337550117708556510507190278048736836413208545981863780856831";
      "19529288884212474725617121011420109083719176084042307000138428649194091920639";
      "8327938075667211716886168580211869181679628310891241396086663868161241632320";
      "50546778806178535468498887210218810106123307251791580882247524421100294295341";
      "30574977411404820333239918514944667200338902645085529348563130262864324926217";
      "9892903275194545714737750789991423957405171153621887382923972196579113423179";
      "4920577323034891968079586456848977110594227055454553465331672976737322470181";
      "10785473652133501829555600968223966606682909992869608850754498368109405959958";
      "44259656456536904544779434380762383481009668840670964276817234604369847527532";
      "16013602167551971824719708405514957436426476815028708803379542465790908188145";
      "13198374304416209263916195294139003986416471192907786718634040648208496216781";
      "21804530702651053682928092693590400484720275112701610945338033348613546128300";
      "41258400074102294032881307279891022609951591773444936556013171377165772120999";
      "37500410649974720689109041933579952412448029290473291361854784961766576368877";
      "34335673011929272194773705817147158647851634047942272296257858433783818390462";
      "13886304004325070507319308017925418279796532347344964674118255936953984359681";
      "36212245366398184116212011743173706647869616792063869197638400841024375748712";
      "25759006975740081144269794348054803069434307735185793664670622388493509618893";
      "27454141834179019142193646102488261892878322855049554559653828601521710959492";
      "46231413498972598224538743321743754536555738713900369992799611667660505830198";
      "12831308687888044138550325104853798541540822575395885697883589148652582777980";
      "35086901484248977088412788551567969916605411503392381636519644581735135246639";
      "6475115432881146883349186955429401720007995218321780836251063967786164777830";
      "8814580017771885006531117758255250813668411043820855097899546270767102414310";
      "7807296524174932448970457695754749231363157877776562676221113586348272093145";
      "42150072600290314522584934838938619527057217927054115870685066610015126576749";
      "12014531038737162581705520180807422015561278346762069046014491217217393623145";
      "19933331143038021192464408343147972121326092927465949610356498707738693905912";
      "48162370217774420152062014238018799880581373414572553684036906215372618932347";
      "40819852050845908476800605687008690729086125750975079926804162995170273045987";
      "22226594575860551577968163846926724696603097833150589784765199214152339318359";
      "19545194169971732111027157974516008318207647066892354069067261444231038348510";
      "6049836141434740667284236008114543106249641546035952601692539242914716493120";
      "6791353070942758297826333323115522110180828045205749596445149910757953314373";
      "29909049992012855058485881696486638410170793566701289014595505025597038675406";
      "37049050048958384299197228584051152045340884544932681109205219968133691211039";
      "8271317962040216706363322101654508431702987030110073352137002798152913000015";
      "1670774897775895329767148809679299585171850878621026134776642441972236794266";
      "17422031471600536376610034591163807877753208015405398182227178552347096580633";
      "18756624022690204397552680734127650080255894251074233287591407798661854030530";
      "30668115702052736591929919340014079888097509113980964494205188093038881676393";
      "22070300308208791796677976010650187233479496718840088914015812675958670301234";
      "8719223857171626532277312086417428648729460205529882841381547602107666862130";
      "37958249804564731124361955041894134137282950000798272227069902229038293082676";
      "37189467966805221844845186538807960819299637527099935959247421905494814306365";
      "21466607532037915848310355716841895751321958036985554994122512635502114704749";
      "14179699035342293451307513028958516816541083634684431605407839181393476104825";
      "29154847955666596586127425042717506047631050595585497722311215198569277732248";
      "33188642560979777145374528795549704783805148120231153611600332204665631092317";
      "42564521923637471405699083052532506872185646145525237703447984248100308540906";
      "9688958844450335307002049478744008486071252176234867674338843547336023975670";
      "42848254690746470199841780456337093355003554479162355775109612541732121188865";
      "26571650306498172537015187191960172565543217489415394043243003022941239501277";
      "13259263851666023894687861132930820553832823620306352930622248435429243173163";
      "14935311346095148671867793890923330605843422232075508196436807220447844613370";
      "4344538561671100537571115284147321749241294067305664704606142724262115973132";
      "3661287306275145440306213618539663151346918182078062211644897084121048254313";
      "20823698858703001283317436317010639863721597996546476932310242177301854267509";
      "29589286785528202709772071088244026953664280695981877455063175736821781541694";
      "14714810814119711606060345652389090896596349569507164391329166387481498170325";
      "14212678415151015135383112231592717825106807730018994977285657694049579298318";
      "27294817345129277597625121693563352246269025230758913013178562651622515976209";
      "16308958452953063563921495978976808898979645896736092486449459545961496250858";
      "23801416487202359083498068782586588131855222018242538192997207782091276206860";
      "21788204341490442112154345605131469142633618445779895292676418878377458001839";
      "42939889385890003399975992564558390206777324067014435789391978812483943473084";
      "18744379815502146842706137175625169737619118740225857671323003521379145620839";
      "22969419294986037114832463860692313839911009856023995119192316414140491424064";
      "5158048168028926443440685040647048915854092072898670428607816727103222084992";
      "45436514015774807133067927806141304958513041619855877603424280662728885659666";
      "4148575853437187976059844949320814090464120728486411120676443836675361156433";
      "39274458258755370051287444400457797244045933354561090576339386851101477414906";
      "24226038446737669899105084780102219021070008789681262557528873238824761650295";
      "45554128757216009101367584501852978682053416379828133489710853000149481226345";
      "15468212483347652283360923936198282812982215187267560543021929817615478344667";
      "49120785890340968057046175708683790395194430243216223332975263066275757413807";
      "22165820818885004643510856850784071522542800536416499851315809803527220567485";
      "24255417733013943695455694074510916498983472445769012245738544215443095625555";
      "3578717881416756340877516666877448995809041970558865616428083782655188854064";
      "23826341091172689336238927086223180009822950998486138608038032100061694451939";
      "27712967780178175030774348740828282622058332263075474167028713006452109351081";
      "10692520630891410810882731879436263881937079315958040076096859309741666181887";
      "4139611615212690436843419488530338015260675471298926305839949926237319638064";
      "23893117338530655111858176000813570070168939016669641291797989062978619668263";
      "29493430044283825498112780304231954297919106956762292987523773747600907821123";
      "31224696921534136211793606269507101328026664939270273541391154325809905983477";
      "1161990788645954276916059640768435755816955781531340749166719053457102674329";
      "40032672466651019681467480685414198090289911817277735486101335738870038918838";
      "4663929628087510457582572341889343283250798458980128777564503205493248261588";
      "14576003601768386193074498529707218258345393840871241657474970275429765574440";
      "41907905377583342345509053513634246064531351674075011102250846877938645814680";
      "13820230842080821315141850957892243677733920498405615643268916522170002600281";
      "19848873264729615502674527376791162181860225160995619982736986062940458512804";
      "39528445680729025348431669264547519897612726406686606338168880578253680155174";
      "3118432592224748465457531048962416120738464253058324843908920356643714609755";
      "20291688884043804174664313901962915383913038845115296389312218366129420572704";
      "42557007757415638497613471685612090789101153750789304616028486221591259415030";
      "46792197373741062915032927311079971699067950253133746671662212783669451417489";
      "4446326402184357086836436163159453880944166545117770668456616153083342179625";
      "28708468885765405820890561098801183951304364975777439218943183437220558999123";
      "36301422605515541288198992288053820065278318287890213939282985302088469667626";
      "16513700588570500247891971462860214234891585098734807087134948638523417237942";
      "51303521335085563665906206982117421593801796082688254691383972540879029269486";
      "38349748912024833254388160686883390837675515065069293547130880253459258191513";
      "5863602768144479058589215618670066402672112266393989291900873801213554123005";
      "24816851569224726654303407018916136914696378461182187828394888509457202905452";
      "35668217636187023661106024284393036487257457620610684950679976695467857461614";
      "18049157617317886186455739291622755056587311439504905678793914609021791583485";
      "24311184582337406630675921345578587870745539726250911563471149827579208380375";
      "47049171163587328805804625147855798309518236528924756379359079671413806548741";
      "49217441966653616354960566046394237511933307451264416176581197097030607882249";
      "9741440763223308622766088611912800832840447253106863229069648354711337865316";
      "6711970275005184765958920828167320253630591665126522378985833259053410800609";
      "9977417151377590543160871053129520943830884975635063831123262229069994513327";
      "3082837542990263750321290997953667039889961622919749500136642256407112034669";
      "44429448918101910406096079124013269684487142109369137229916801140750864418243";
      "10204944711013435201457808979370927831932282339697033510029454082329887203672";
      "27567961079029968585701667459244395330846299598586490098261597725737547209132";
      "17092282981739153700626134625162471407726486372216667820609932370888878727413";
      "31485584271040282956654226763326588049877825728467428926223647874479701786506";
      "12955442244748326703021715942574723118787276791607410352602368690534050770417";
      "36233598404262020873794741863731429804608939874302234761885447289322137408181";
      "17365032709923238164430981278878270324454980279560841069445448454199643029113";
      "1599308425815788479548362313813963333016792520742870977461515191009005920540";
      "43669871288596037415496023789232130242903264831017218631867709702917757490026";
      "49117721877014812477333148166335201583815489936606800780714317383158496433108";
      "50780218530638944533890976760629911189324354866670913408371520875375844233903";
      "7689428494847004464240529995304510607351514709716679690600711591096978491670";
      "47955977594669526260247931440322469685056949069904259470080759325035295286461";
      "8365512332847242169003328823195689637827840697541204265356337650289585838123";
      "3840401128719370383692078279691168408796656116885154086592491099204611073383";
      "43069581936608602226405255629351890119646172590162211959289288774795830286246";
      "43974189709355209820476462362097537404927792511028786194043940929898183793414";
      "26332351117299179629573047197679883935341765313312089900660919650133476414458";
      "50351703458402831605416039704608408974892592655299422309480445654414527175979";
      "33468607565896128905680223110626886234307943229683243021379890835118051012325";
      "6614565191349098977235002226407314032868555511403717887772191274612517181410";
      "38103056918801597643212870363828947832437506655680421481428698964117403542602";
      "32908423128582779977704279934611177327699184469671505430337832556835115384573";
      "51834951159973764105688866487621285182469090830458796598668031091107941720686";
      "20906443585217694636590360222926761090515273711034774487436003326403616929638";
      "11543128149317521186944038480148089876167062819998754661365448516694779551074";
      "13337387009791879577397425157695857206822652677921492812658909620421271792366";
      "26158663219738110112661733659009555223590055652836643266081611952515633330808";
      "16620288606563676461349358549564125077202861312536356779066223457462338103688";
      "9370353560216700598486832215289311328374345394195634955453105798486005404415";
      "33633718565315235577394971195804503457415899433434050508477479187227057261067";
      "22882449296374811923033442799913069323577656681081909852574042775892111287921";
      "2940185604989639101256714689859475930684457088567484617894462057139075862941";
      "34483194121915222880375114276064125544128032137924712006849489977876279836276";
      "45372384774901078103486078987247871000423060133375498791638103398927924400835";
      "52387604781514376107006295066270649568927674910028459430830457444029012327788";
      "6167869651297502278429690950623450349205119487045648580978208453778184411341";
      "27462497275790959876141507254409980360566911339456621474224385082554805533038";
      "49147087543811949479056383453491986538702256593160239527509029396813090030404";
      "49587001406488557808406328288652991476747338395266693648839878008858484697835";
      "6313958677173548204879553757285379819254567579081576303778677143280554291690";
      "5591468493874061488706454796222404166033712948542307967483439147905003945470";
      "2437221293824201160919193686511276517772539907794390113067425954677677410182";
      "30357986563693269312610963334150804237408332248581737751589214609304706424480";
      "16637601486751396636529759375224983522742599069263721097214299703128247198523";
      "27879534340144216562112405598077066811919674403148810235445326156746715979842";
      "30788313762153313626674963316612595454484683342245093445515009044754566899486";
      "15725387840690796443588540099094119524389569177620500091843845820844320431289";
      "34132295312326003636265296299999208396694730499866986050666477793086157249908";
      "15362934941085533070255910138373084570641154047840765685532551420580152655609";
      "2755137135618857778067513724833509904536351561976592574187101898503219001617";
      "46622911741851631588024639842856120275465416427660592975008281197121795628830";
      "6964635240711037051215022604794208273817621384886657093402502491567294160845";
      "25783574129877826155110663698218382830525380279909999762879880818546978011140";
      "23465315121256052707655414720713957672069185881022798701424890012062179540328";
      "14395053091536499765531983402867839134341617705786295303106179101403117403050";
      "11316253621114442899553787480078181551163062516697851587687844977545722300558";
      "50064661939091922013762459183760659158315803719176946262123119222324910530256";
      "8783665334345037843914454257570704820761444130918358310108843988258662584186";
      "27618475988876729519248024362417979774716550450998439569984942958903150185062";
      "43015769169394210865366119150018957649114200451714812555830871262755495468016";
      "49732426066558397245060256272342911170810452758926457010543502425937044377044";
      "2952797980452813888623715400169643543685112681184348275283000981057872198778";
      "50872740372354623466916457669382604074806324513038750478426891403283893655073";
      "392818184515825854281773563914353854398754713238832910269587407972143774476";
      "50779005954836595097541637958107285799215893016482426373886980746829520936350";
      "25176357246579974791673072598303068538657314197431647903881566730654004596817";
      "20248152184837592885327768689673131083342577141215627095954882454724068067303";
      "30064303728202536588603791400844418739073552658034934314710159102990759896158";
      "21384606984835160613401783081720653002397794837776744119212545320680659814207";
      "22759565228734648282413300371375307271924944352100268152538666537290900864554";
      "39429333593022349595681621998820719879621843929926124877175561019165223081129";
      "12070092883346592852789463918508042095108508741001381953375286128032289075905";
      "33289517265391819899507145162086978987916991654940411189206013329200864859674";
      "7221597429770981330375263241511499043705983470816845272720562845158859285226";
      "16638272235182748474572289194344411365650205299005022442793882687465898549539";
      "36006214239196604148614442091188440583481038594995316939593040856887035358617";
      "25792600705977450864245882132395859611441619832808864344772519627069798329604";
      "4080552845447537437568804141996338888821838801402604114257764603164350512676";
      "11798208445675100720061102611516112959643834415640440909769995293901688418811";
      "19858693043126873191571109475227847243177160525403793202276277722982907002636";
      "51792167109522919038849306964270342579703542020877440269381030774505714185697";
      "11631710203663443472344988456889389622339025983399538662094459108486378805525";
      "2182473716255059033897861691447270412333028850406831066185078223238986325112";
      "761168299106618959837253184610027302352675981172895412789219362344349418506";
      "36857059855189113781134096792662950699742275482770772595919903687711739320818";
      "18213396754699008102047102089506462494549290414412359468656221893099620902008";
      "12599997312887962866854539884234476951913054226022526078890032319964768070561";
      "31295812056319316979171165714902562241023210946259070539368704588259135657855";
      "36028478227374554353553197903612149760893367375462390976595843472968694902073";
      "19755792677313410149868952739127262822852161041591595345565317109808360990362";
      "7604195354962581173699215459157831606985245892932148667568863588427368471328";
      "37402797671729867091958880703368044330554219817351439709435695854279377052968";
      "15021754554199031983119820117039379649754158617595693761803226478334678245252";
      "47490255684408806072434251664743508051420570808132025501451725974827121258687";
      "17058297088100779754668670576690752359201713072728307725116578742664258035812";
      "33177512279709821535209584501483624708734718786595445144375381063910225855217";
      "22722275695407528091691304246968383686239176745361072723538077075588718852746";
      "22523893181902428650174996691790130832371188536502447987063143120257450653772";
      "23308895356450165080771503655705485959702912748685275383709016805561195393730";
      "31027920485628166856312777655247597928527620141623480299311482321440235423250";
      "45061629190945989233993296798591248101958034421473451931174248051572365665596";
      "12635346734022971744529531315542317156695950592572588825637598149329121435602";
      "20943947811812318510797609944365001415379144029156369080552566308035645494236";
      "25272795848989661284291121337868232983504512905079898072787482710703777539907";
      "30267260031722018334657676019133705236740734579176664833600084021013496843546";
      "31517311768361733509846398942976030662400143969686723910638374750883139079149";
      "23179568872539103374642859400181289258494250830556186918556740813443091863672";
      "43764857307902449625975867969146072336127131357517214347103058354083616467535";
      "50986536293458449273154397197499183679036967678265692625380537258000063532144";
      "17739561056178158081098295809388500809247889131390006315905372775593328303174";
      "29288755790242817717621638923197240104295093218759888966129245521028472275230";
      "34134838804483412147238682009351758572433373367047849860439248437388218182820";
      "5678031864698043849290292270505282805363676850706953191264384683006133884965";
      "26520160397861331597785508913058535821999870140894147231231876363158277734288";
      "29240730915918164705120039064238164059586741149554989326639275573958724232530";
      "8343909311567226700622893556200749476532608824719086807691291972160111871498";
      "35422495044092101446713476071226458201086591087201551382952729636451893974060";
      "28788191175818003347220573268922959045830070401915571862444782695818400239985";
      "4964783835867249774083299211014420218490608209476492267659355881364453511847";
      "10216614694145379678113358015463688529998198929758355282726851046519070445194";
      "27803494825843439402691751649293753560989707643490491294838415993813244078970";
      "30748627242627915480476055895904136928510253392793276393732599431460830214019";
      "7751739221008798527034371607783061382972620557894156823243899329549833690423";
      "33136351771438729026535955096064818190694747127577887810498359791738478202735";
      "15487861031051273320246153480621276816764645205006338931216717383286810036662";
      "49842641210693624237669424014970933360600934128562418971602444161937944689815";
      "38080738277407466133634923380952979679353443729179754588489421357109266527740";
      "49835778803230991359657573667412732792328267908571176221265893225909110634684";
      "48979716276201786775168967369617265563190564537859459940775310207730069238772";
      "48115968293689106220270565101906186091927515718072586052159138752415504690487";
      "44974490348051781688152167728748294073951164996734932874793980137333724713822";
      "32723711714533643804223002624655983381445583052702071992248370814287912622753";
      "35770018441385880747665875909685263825335619219990900501758283083700215049177";
      "24462225877284730742182932602961025133445826599619125054636967365951416719552";
      "23783458847678429109975790282720688654564666590790639711956826681143293787773";
      "22347164999197115677368036880715580840867296071947684897983662897368903035923";
      "44436078084173495334203313236158995421334213775491689085750945085639709823274";
      "25531354606207591001503734717276709131788523985002917593279732600020946775257";
      "25684785975858758309831379800021705800796165309307017255796818608524248856681";
      "15689846944752800355408013445547581183295267110737304356038985876510433629593";
      "2954755130869062203053930362449428183522050551079825685966392986029023636700";
      "27701477658173432393740883974255870340912747006748435341251832401519511471276";
      "49144605237971303130051477474500252441736011779691510816968732821261269570968";
      "41339385840143300905581133617960524027180235012107468786212952859173390468514";
      "39648185702412479261241716678418509894559280563465255646156879733379530382617";
      "2941231259680949143593699011623744100174752512729757643099482873601163245575";
      "42912407210638823710182011018928480520340098630346497369618624020054117846676";
      "48149959907456562949390018405936990163864807774773031806196322989123705667163";
      "22688265260172456453339993837459152038039626634400711129266583542220009592074";
      "12000693219442732741816223290743392039668089531561600727937394342995414579134";
      "11903596729989502145549179132986907891593077014729378748826473464861625192683";
      "2687111115125246444031317339291347908971840740015813305558838776418739833086";
      "23449522976975553535812413915796651435793968713230742677655098865139106223667";
      "9127447737910095400860412314688824392136048676974256371522014899566329800277";
      "18470081002802756098187392375443129770425055057517598292932337151147562979415";
      "44570736387423385650881595596783530585778739624944938740374839306088992916739";
      "41506121518765476611532159577026640847942725069679660287546611181740321613803";
      "17879365806603642296154180079678225700598122219887762781358998608195664544974";
      "5797039731182029290044110349162251456412636832186827899836873551225117057673";
      "16295660997252122627187664110946939903408094437070458659338126254215674463605";
      "34524081549397177387160463682322947783604339299199714872938486944639466740633";
      "46792070054974847313209541773010710216925758583669099409416452772447490195997";
      "26758138270863118025378847876443541196713233312489031593470542282276213542370";
      "25932795773661200059482623714428701540382804071390881515116858419823633841821";
      "13321689192715674395770738630438750136066468135694575335309580617698058033117";
      "9707380803157554078082855616156559824492425930465667797574921265494807066314";
      "7456158743057656267196226193273529706797096313758394320439183942428804984716";
      "45355642533698338070691932069661520741557819242118354206922415757362929214681";
      "11678259483364614216163185940141297609599778858679439537001487250711661685168";
      "3518832067902435230725709346836794333454945124555395496274090845504580131455";
      "32945555853640395249820450907965284295734348780933164440399544563294403789630";
      "39144256186074248653430012132977997931891740120897263028206417805470480396128";
      "513475060263080708913788928053965257750752082706905923893128454713255069681";
      "3683049475437575758554728873338252672236374719853531546923396056498941488282";
      "40512995296870597270088595777901813960760477076488920843379483396300135285919";
      "27566780071222822332525446641593709138022329153495927653774019832657393592701";
      "14553386429473594909470688556596424443792788721346677010176123183887024496060";
      "27859920549341120221544363269894592509610202544403757207234685024595167318501";
      "43630799630596017253244467929174687910181739803861346262759350693495295759987";
      "10566905550291524816328331044922050443675986854353663452037665157735899469921";
      "41883294330455662982758134167170988606274464177099964393473215947428373454548";
      "49807615802944289048873232050825447587887207808798093013193396431089336030610";
      "10322165791099655621755425357073963493688332466706230721287522258992803490137";
      "30646173733388488363150064701278686720564910831836411411651976803737973266145";
      "9402643818207936923863049876511905578631103389374441210902427576559340397042";
      "26796903570709220124665459153306887688701095587820014535393806663646332690802";
      "46485326810825309550921448694342993906840425779587939587426865276020325464945";
      "24356907333535237405651241236585413997915979417848569943590616378149521017774";
      "23511169606994309941348827806149481805650274994320980240977267213388100293357";
      "15731023427833496072707128064453862171578629248859961123054184724775612220021";
      "15476157034920561920585064222922712755398556043478554933175489223519135633295";
      "2588249154193062661573385899432005495347251302263070328643388740869671399217";
      "6009738957936176982507178002696621297792591037813275212151400246297074354799";
      "19233332597631491707508807992208382330520636330001528420218682645685589256221";
      "52257447718383093991766497150127369332489778818971489581567733290721167946805";
      "49137177389699894517809095595548850494591743777874595835879738514452528623678";
      "46568408911734306168397184498986706003337923310668800879260860154439924802578";
      "47934768334329838261157101167633276452145498250520979978623243405647174036268";
      "50548985142375412913344898480017599364756597551569943313108030702053373292351";
      "47313547501137846688862600708885501470839439049482542252265318066588835595877";
      "44379141510324834123427106121179013384083052933887649345549024509665387337907";
      "12745350498713174792397397689765109018413448791457948167478567090039244524261";
      "26500864710621301469407121438090857294270092269498670394353899106577395878729";
      "11347414485694636965135491107674675767460314869225865451044094742585314486685";
      "30546797282015374456420465905729920533639220341847643819193401157056239855445";
      "9764420137258539782443919930298504966223551788317773035826893207520127548815";
      "22299459460462072891198481974919074362126418543881491087838369912934426392572";
      "16855285284125844489209514080904609067369163236122279642071700082910563677928";
      "28470684714066956536547171205246920705847552363405765916824456152219308886458";
      "4732461843529436130239807886795100206469260396399272943452254374852516911378";
      "34562136348353570109700872901928872554702381799420513020116701553340267771150";
      "32365558558736606695100598286177066733690579155204608260555923597643725911454";
      "39093274064908662087943844021095101112203783571135735803933668222858746865243";
      "43197629030144295844773883705380449163834899349448680049499938815732794818313";
      "28135261046436067943449704769784602664670169528558709941327602925531279330283";
      "1506102606338525938978917833686468888009362316628110197189912144850886803765";
      "42336701278628501135217154714167575672783514963702875925876272615990289229528";
      "25024620564425776027644674844378116603084237932862382763192286329954441925762";
      "17870721740021152115020062852028651603316820821405634598215292938053122266052";
      "8726154223262675362011088994808023052872330129832279854214301067840970209836";
      "14874402962592699078349928625650239666631999908036706122344921639840279200415";
      "39756319747099752854658342549564553329846048617905492959798860958027344323191";
      "16691128005183566214615852202071092535806876544863611664073120718156966518635";
      "3656641624593787470623179851898501381429958149290052751094306413295906197198";
      "23058535769798180750363501250801625076459404778101435404523789853891253539536";
      "33558816550895409218380886501604904940103012687961987303678839499951905999903";
      "3535320991257296205944099868175259133046387724680729551263894422361251248758";
      "7317061444673855310460676987104314467363507031733135923911471906709732796227";
      "11500894792409448904640700230690380435021471256333652274764744790985040833762";
      "29946587402762992979637543680372942972051576109298571343103906148223476379391";
      "4083115199018558811067305667801506297182902358286795914571961100973484984414";
      "21780845559336370060316195032869693907916051322860704165373540781960864925849";
      "50108406296877211542712950356627343571290344962477533388788483384843943241826";
      "3604194748440975970709176256380189264567204604496059337216505471586505569550";
      "25367520387024971306924473288179691904393907838798350326959612955828936977623";
      "20832698602125152248033711132843527797288526400731772664791124082045251454142";
      "42631062868366746704081529205540353901856777480389910573915817519106326556653";
      "34498285379235908749982034362054765010463122336180289849202738319552611997489";
      "42569303254780782209383769555863500331363619065952722987173481354130829961783";
      "2968398972388390861514824927379622551058313567208592925335792817590639277711";
      "26932822849411517822460887083515713714294971165226156231324226720523884126957";
      "12289852530007884112177675781197310398488340001613130934099944458324157517609";
      "32571394385633728540470223537905763247514888927223219047927568504736330049592";
      "49323371198951330358894217978741100439230061670861277900398849522199063498403";
      "20916227317093555798135256109920923636673315915840710498394615832626002268064";
      "50437846180582211045193594549699682565194393344569259404783034512017335183667";
      "12720868063213131315535911341883761360678170824615477340625750278643114107287";
      "37197243361742872107474934672270277255457140880848614348969979603547286846838";
      "49972563335848604083615943319581538413921258859517393388640982639930301010342";
      "24578514759429435534489548439103508142292694204518742527201734880498761607088";
      "13544000375663478018521907983648192775225634805964564209488796232080592901057";
      "30244906257123439752743184026932532959005248829599515228075497819748836533053";
      "17158480056121611203761622020240364912867157439578870271481544859959963992982";
      "43213708539956730045950791581115215808814156477860100393372067402068523043784";
      "48148048525328038354477853614732455140796148613572766084643376345096272862233";
      "23955550900926153176119256387738001205670821929278609825909043128410785370923";
      "32084112248131778873683184950328740630941915092866433791792196623349700717247";
      "25228735758855933155378400293367847597725487322422339171350380923514466214585";
      "38708924229373547897104118288852039016237551318118836657141457341427167364654";
      "25573420543845971899026547821922148843484281700825584055000279017238479818969";
      "24727047789721276146751871546128337281102901395874275592320129585145360286605";
      "16376363547325397340914349214206199307694252744603372010394026437013197100776";
      "20208836376333578926014682699975542524501761930394685283441636991924627929267";
      "35206301732048412276841356453505638516993236521927454740085319844070799435331";
      "41261166618096608240361379074330395434896879239200007895635788430952244472582";
      "41432219394078727593377645450491483074448807484512488014556070054882946094209";
      "20834236252121597410527416638607520798042160344062107596356735831487842114761";
      "23532139063413819501017120637575271821539320929878848328154727861013760586039";
      "3946253966634265225936238815600554190068564160724890879995534127285456411579";
      "22846690625697257310904779889019761152674142140749605466121380947233821897617";
      "22087213788241393345997830798811611648992098114012713841486529785834041554496";
      "43158723807235728204358654052498829642083060365187988897913589551158805148577";
      "15465863697980742098871467263990006125886103501516872842535870075250801222781";
      "5680194980291197839690960478626830816555317427024014693910787627450289237742";
      "9094058180026172545686171028787053405103676091999366345519984327286409630688";
      "2332670368762680570021571783692863301454064644206808151563000113996159738789";
      "41147800869911993983577010981800974642409890520338080941707731579519543968663";
      "13279894307388819655466420434801883531790954002783939588058497750423667181893";
      "4870460897717989146446912775477927413376391253591063401746677243573570104602";
      "21434150992290282229101961254012913715487714753851223580286820712178569140123";
      "5884699423472479901902447150142507004213890029567299438503194948937225087869";
      "10751322070759878166895822040094727160998828737858183859125132419531492304288";
      "38992650885322951602413869202579221872340599306440561607592984827348058953230";
      "29170379394369260301915803080156002423232616339189492529725305493825816836491";
      "28207328749747479105410685727161242130439891647417887391083580573114642433586";
      "30853455820741483128256761592665063199571831731867607712950643840486915981512";
      "19674757655311695412098014331868801137574968530161273910500977119681828944720";
      "39760311849140484104401541894168574438723197691222319633908463502228900435385";
      "32907700014271836452044581308399924687442165571312547230568158377188973441089";
      "21419616329214777079035587170514020306037526204702975777693989034339440177318";
      "26618360897653828866229525715043321785206978439662756876063444705770873337597";
      "36839328402947719672481705066838749753765029179922670705966460218560367824702";
      "33819865214094561436972297577491830411674255022072017707118420428518277463984";
      "52239226873754505993400788229529834860768913846928108083029668222253331104089";
      "33663514509883297348657719612646437260376060472686074175777529465535219635914";
      "41003879710590127522478830906318116993393243242504050949617603963042321060476";
      "7812617450066867719201142889276223443655576184992693957516680471935511930279";
      "51121304503531803641767527835120763884818550079574319802192969900240584243331";
      "1274612101252555263549693940665575968018149479789118602662813998362863815476";
      "28111554183672061495966203485846707355259261091518108181556420685499275202196";
      "42136394643178945109983278623800719553667430014244921031314292928454177600075";
      "29400787731444232592537985972506449856480774156983480052734223261628825541468";
      "51495741815899207992089872049098533532158347593725999004967104881825150810836";
      "39333115389438061754746792518056897857082090561687954807372914815130461016655";
      "14294336768755739754763672664822083245398240681090554840744022889714341896060";
      "47674122242123052198728676357951860449892667730335860967923060333702419341834";
      "35684666049106444634028920061342458983421529108234610860428488342278162340897";
      "9217271467341686730075876652325145965408071349745719665965491968116132171401";
      "49102996771041826251600275636051473450230724151940234292281582608241970286503";
      "34854604674557982238222418551502188390821202909341038834798601283398583979700";
      "44103714803951799081408903773636811469217830709674983501189338090554583969027";
      "35216265618185969272100001311669741239205828963710925045672291350518816047261";
      "38403524999556193056272637467205416979772986748102914574085083812998622738913";
      "27146144115803706054383284709975278288993223860198708633471683084389321626754";
      "13717875182956004040277399923680066755828211406717894371621241252873305128902";
      "43893363745908782939920493548985641014151424637808957048781989937501374580035";
      "11726253545109081409164353376819469125399426277505280541880391837677360874072";
      "38928083350744149770676864428063336223211502898736165860838144487338522811447";
      "14125823190822219756837975179681223974137829967998184374453263586157382305654";
      "38513876015199093611082189496524624266110546915344263711135739803957351751310";
      "47685229118417094929745561957819690007671043576786068405288351527235450947053";
      "6959539796323704070461146242134806197237474129123359577767978063953427949977";
      "47545452988897685363050245883092979778729706327058096488694175926251841756750";
      "50819854690063046353662942259579520840136358471545216283227859112171763003225";
      "15309201933918541480912493953275686961353315663926344924717901793290472429632";
      "25814701665737234866376372053628534273087781843875343981916301130840793116256";
      "1916844826075222519090392623030931550354624290318063661929274409207762237329";
      "1046514656280512977708818059092759387987165875435181225389723691639677269582";
      "48632931314601925346131427356122727760212316227166299632747707086089052363684";
      "6605181920334239323337807639920607887166441510148481166461711505022421245712";
      "24648729211610178594528829323421440848291736568213484173668007946234312273906";
      "46859494710268538864658299697721145997690895979735714480735923808224531095520";
      "41175929282429829777281847415308245248403968515148043916452754293744702303400";
      "4936300094396586135539485728167289346454991472436633497057899786781957023646";
      "26497056294320821551797856452767310941293845697666592809944450466405074510159";
      "30179755929855617808122588385117490529340524783380573627382420814158046220265";
      "51404155368749455548900426038075050336878399275390882961314989220012144625413";
      "14816852270047203104312028732909159967998906770274196690632931234420725527426";
      "9617752168355609648284058626664682170830718885414476704978109198619947225853";
      "7427964446763934879077123333856010036056226354148572747809815822346855367365";
      "29674872948739147286091273509870908664455349901359630308300510194622261921733";
      "43495676299055671139434544393413803052382814125675363612358978059313789429586";
      "13094408335698611712427781744265395983524687621162836316320830449519959763188";
      "38569497775632608093794125886753456740306226239072882532108501824492224325593";
      "40308698798346304095630271480781739014165493986458798701620020450887376406428";
      "21695323206500389583562384680685981414856167910480068112985112222651637002862";
      "28462792058602339889033620039075559101583339912637364038250676107653835038248";
      "46541024611362968529348952496518032317778604675804472582130971946588321773057";
      "51356043325501315362210916662661650495252901592454120098836536302110199287188";
      "50506579084327411763038002678064865811256717858083039734318534808177330899455";
      "43768274514650675477817361475016698140148452675749491793321899996800017542942";
      "4365130454011506171008828920058285825290911024175299642700028827967669304334";
      "41317071247365873784712926167181757675491093869449596462352859768807347211544";
      "2666773836237810619617948712753874439458872566874729089643359958440020536859";
      "11268787534831056816083083174895755956352873998182091668492218789389708906242";
      "40695329903519172458025898268523734890965958519055359802905784576698941321234";
      "41627365240233602645027028937623461357745612228956394512781214869371540472342";
      "4164478539096095999131892571705567059771712234999653371776917360777549612104";
      "51248727099288674225044422898397396359619826428997072695850613136023953439945";
      "48153799345590764241473716564225186646412111682334808658902588825212784855559";
      "4038288326645960636183384957834655531514058972517268839850385229326514434196";
      "9349746370858115821223769976893823674367044998087780251985518797575566269054";
      "26635144643229156230109683885266832396020379662024410046384058858172974749048";
      "43223596713057491838453489984430963701106626227127004266936175851674881127669";
      "34365304033357616463976462028585280284797223483341370850659338406635297935595";
      "2134516731680789816358678416060804041161035786347309768102559295564927033298";
      "45222140147028755238863517248876975843048731238253735396150896367564901004686";
      "498606925255879431664844628549393158879953298471933183455573478512612767210";
      "31655578397479065559694701010163356160453434259437394629612488741366238826723";
      "44556920347721604505312194713898769297829148630669474738183867182834534512253";
      "41066252220898939528372277962872199592413634363843816853371068676896371450235";
      "17898654860211486557422421879369818443339885864697693239455405713385693412604";
      "32513783099500141673439294633034010193535529791111957913458937240956644750422";
      "39905409111076411206565494347110894882613346677151423254819846790782130025281";
      "34988407687074005102516587752744593627068947572334289485494224614781612900746";
      "49737579529532507611760379505316974983940800332946027442906862839608822441536";
      "40162178377217761341550347366456178201094415946625032846674573547145969502567";
      "19353664035666185668244147626872757644951716514199713218834744622396379021728";
      "47102456478332690688659328489760691845709562508921577866325372829999411432449";
      "12207115819013703533090639097195525814981520405803331543503208389206865838351";
      "49994145749153772801588770229283450802831018859577109122749028671638201340175";
      "11750496117230153414206471040577887902252831603305505401836225613139968743361";
      "39247158472854700135101098114122648755375036565112534510407184246554146458821";
      "34888420087558994696576075863747777609045400754497672888032242287719438881063";
      "36746602810649853608305671227827297524785410557002588877308144918466075161379";
      "35110190469581159095125917772271263108711630576551389559652466237914252519706";
      "17666646113580405089387681323991445813223732839702375394019098767167481113374";
      "49832915191890911296130390700527381380353409264287349518316829690779511940285";
      "24443498466703215427536198609292882343492137081224136946780263563592401049860";
      "9354050407159006695831135953483212990074661420262042032504530886059244184549";
      "43333009983788285821400695240087914486289602002713044560524409547002696507943";
      "18752273838312523782927643189706439976957320321860728910806488085573896888517";
      "17277900024182511146710507398920674498144288099203282562831710644330579267863";
      "37307678413917534108508235735432663978301009388979394911932194936937228116983";
      "28849789673530572936431250397502939284314408030083300337114716226795362105688";
      "50912816147821018549769876876636191732251692688907664846983470977761901142017";
      "30131058343978916976539560634538314390572592064574889352048802922118040591878";
      "3706738172138818078705220133282568519342502151909947908081476774050163705447";
      "45699814681518246744400453094285582701849408763005827286692443508836010669243";
      "18846003060227712054607266173221112847285282616057372060555371817788046689458";
      "22066640520973054711560800705115163615789502002092761843459719025242646197522";
      "23829247396636262290884964425831569678858143545005515755792807616917823372004";
      "48198239185624674941704629705912623499339853704797750011743362965545369705797";
      "14437343003724224631871818628799571960312140411440628694004790267232875166985";
      "9205739813512268504763814673014453677276549572272076135414717042201476484408";
      "39791411423593512268799994379557077985176861512059575297944927863183698039381";
      "35926621231744856494112841579711773281980064124370668225976659404439672270700";
      "44486629680241930770190601741590174294937444204078046665996776098470715578917";
      "12162293378945031764624085071759188374782023105344514611109545726564556675201";
      "36307225704631546442623734392611975648010152587096752396997755313409683740066";
      "41250750058001775370365399976123622596191578857360075239352807587783963966911";
      "27326083632152278734711454453088575834660104218399840842350769848804017390818";
      "21738472712881664490908162471080764510324227185426320378156680732466086006946";
      "48253221985307003164932400584047916688911336639213284074501437919167577474120";
      "31747278632217258576675538435288102373171173881876663185343643389289388474560";
      "5761801194886985126517131550892405530757591539197426021056539623860947947777";
      "25080051431129686333412677366349247249765542691781361133023295276989895785662";
      "44725507017222585824480973320142248615864064267075237276314928012346637335685";
      "2270142730849677751753329523089749032641108434062308390614061733510185159182";
      "29151537587921846263406040946950786214733637455178025270138954283829217507166";
      "51701993706600967882137291998419813154460359807514636008564722369823738880081";
      "27396983310969582762655735423233600814011645446508465877860524193464148646437";
      "47027464785635786821973369345787882857794216687685310972827981582102274085589";
      "8537697526465704802497642132002864572208835642458535053052653228499861354076";
      "33216310879070852920780500139920461536347985311343304758357092362169634432945";
      "39742197294627214520191321293386324944093718559889580220315772412754596333618";
      "33896963789316206258615821504316306436964228772759528417727957697783861669643";
      "25010660153820592469701812125053548417837781371102734874578902256052345209508";
      "36367261405021942429836445456841404357897358255476611125054531559819745708605";
      "52426140434579970656719582674709112782140126494023197627160774284296958026640";
      "17974065625542652257057290211548736634195575643976320857820652175876530118764";
      "37053031019194686166066970377043979546613341770302232565495885535831842113241";
      "13811446176969112541505871240921570152518757388141946244776461129201049000050";
      "15092093442185484653246077567190483143911375332335503262901381196989675075655";
      "30290712242976568484406185485374545475757630659561739950369976270424078249156";
      "42300599090797035681205333143172106725230562804023721865246977451648659325451";
      "23034899362471909543298700478448553281114092027702550350324373720046757230720";
      "48731736718724459302206059867835027581192820404271125436441919516120222347777";
      "38210977651743308949567656032696478385819661205063514163655683061120398680442";
      "31066571830413162458652431971739961248158700618823531207554971312281336740306";
      "38604214043841500037487247628107100072934980241996056096027128810264297729133";
      "42466391101465852203816440495696613849995732468216567393767726715283921987679";
      "7918626562942975338180644093933988817993856782142079793192213031203713419564";
      "49684155517934574637878829138073579948423899014921699823733824485886261361800";
      "1451275366564565438656353212713435069619539370740288657639758022186872783344";
      "4060684572698408855577084852784974870722088774822168823176048676904575595914";
      "2266042413117404820068618979432448191143223638313669085447265538970047743222";
      "30905627074463551844852560969973865864965309523440254426402110555428247986128";
      "44158908912184255345458082216141321324031565774822466208284543424748103990868";
      "46781765007298128451676105938324040827134620337685516847682075321984346802681";
      "14555474190305191329651931092157102989148485771814319545054338444403258212594";
      "16881117240817753666225190901719116414117517568051590769838881684777210471563";
      "2091384128545629176488696135490230680171339008214937873929334100299232999763";
      "42961581958424980887960069029855144961942029721580484171693959065822644239271";
      "37293380196472166233044745617934489446223933790110588175152241706018245409475";
      "50472789792567303044557428917354654330233740880518444155725173737527015380692";
      "26254591932763759021184569941619883521949754828362687682030335425079808014229";
      "17113230459817249275857268126349806861319046074842290127707156305676386386894";
      "24231753369429127358009700702110183480199277263167907099485750041582214965155";
      "32263789144438090923613388538761009896632203008432412115908330894004664953052";
      "12618230980377962991318338064162350506512133151309212471355044610992713035428";
      "44287411811548063431416128186222883697784161373833563087100707769861270222355";
      "12243970408204409993839495395374510961024300896394362315078558518998085218595";
      "44173339028947996046249077532478888110286784422982124321103998220058630129185";
      "4598274292520003424438601799771684670337297603988895001679632082627567473920";
      "32220511643743595369808381786406376653262724588548158227055695474753444711477";
      "35927311526370278156701529193976259428647110571727767928074012487713280141168";
      "33414541138436871747848548210767170259303594301338319380897399124147207142256";
      "10985815035297592042713783076262430811622978337187158511590030541267680813140";
      "47191419930669230163741552576498932288846324126311314824353674932127709343958";
      "22784828163631611768238083672698851077894334504107657128357294425726824989181";
      "49949907206009595584434917818119046546975686520915136028196584050967515480584";
      "26410109194133218506580932937648982507548919566531870050806115243653049366263";
      "49713902702044838319213158273679308025133803584815262572193546155507722324872";
      "23535559504337049461830629174751216364093038300260308135874588247062574403616";
      "2238775094716444052477495313057898840054408997234199224243609623847342839111";
      "24251437981344168177052800972995593868567104302081741438918736451368941030394";
      "27982993433491253628745454998904820434128996322734239523565021212024510217448";
      "50295838517535590686256014994179135654184756295823594187599260917362939655408";
      "20057613369317870978599836560225006632816653691101308330458367154191918881132";
      "39394614248557203761718739642839828701390805742892989071457854079306409260621";
      "47798093889297880302781161190820961988270610469163421109136182280644356165044";
      "44393568357054115404229042885561023580153267137301539458060374049988839557996";
      "33693283919970625185262931602508844386692612080074318597070832534138700238378";
      "39815716493396968613970558873707844074909540436043586091356171795994263694381";
      "46853573174002303039170539308214250609519855889637324611927935851194802547886";
      "40815147595190732687521587437353012947450179162389073327247952677750833108813";
      "26339521409702735393744068131812259633542864885333572967691724944624282632629";
      "29354121099706613567496209577487729580389509912153101367352651455990974641897";
      "13956682594977060215824578428178631751673652949659210522408548576867791213468";
      "21710651844333023404269198169431081997914625130038397009887765719584062563582";
      "34776931503807259527470945396912938849688359577250098809620069934536239444952";
      "30888022057753192523461569966379378071529579974487499148314453535224010075827";
      "50706911026467569615838130915836644196872403584282694942070640728917921207853";
      "46864858442437162961458912480193558760809343578316469752769914636209220922273";
      "13257506406075894433104506959381001454814282265917832054419709339905914092656";
      "748651022964498225720140702853094466861887182520450179370194887763003477434";
      "9928055927827498106046655953164657438589198384956991765511981535095278477147";
      "17282353886786306350464074480326051762770764361308450866796096466478345879680";
      "1031912496796069267128921308084345914023374178989340573752894044339622888592";
      "25926134979442574649058093555286719859705643564478648509775995356905528815887";
      "15964568489522278652756557360367403556214280414131594187699659173938365588488";
      "38050091280410708232976422594473351403153808832581737053257668228216639900422";
      "12030737699352751292766799393553393267232605717122753898023894800120436351283";
      "28481686315014470274923914799086898836504959567797773710778502159442143532873";
      "34854855773809028752393995264841215192998714650018251274814328745684277843700";
      "23177024339262302793601070921104366455941060951873187433549022636746564985947";
      "32706651237059443616796121926868583069846707958453355769010508784973815882902";
      "46999132467290246174738142479599222392723632370675458675293558263299577721042";
      "51658189751923308132217973966348349720258327530023246552822556444736712390623";
      "6849360125712696557397143449526597653234220520772426233279930720210309738320";
      "37750806736224959930132995620486959583722999721579507748526178865808200136556";
      "20596145017860309309979234965966368019102563566006691095290434157503935075151";
      "41254341165403645465348838011157544897177244154415343520886560798681195976471";
      "39958936321623717554709758924074568269853737880198337327309503417601943446557";
      "19195223398318500029787325435183109593313197618937185661501802900443846527922";
      "10629204629388999052909123660165259102503430047516526387386913093894818621559";
      "22392494050571001911742800275551946666157619565710102369399744439030672915709";
      "45789181983557040436379972210390979168574359994520320974901389101449898971667";
      "31993107635680932518045016097850934312675277860051930648249938294616399737203";
      "41394691516688662849678605584944839500777787870042035604148788674531052718761";
      "4260057227269055804184487378356538538091829237564811490140159259203053493365";
      "22755914276797984949384994213736139778684895539493230631683465009788203482529";
      "40041235704216186530314362855470728008875244931687384625262157538702289816794";
      "6239837510956467015853754603670020841591725704614056805052967999814231026644";
      "29458802836337316653464358527714116167816937061907636047906242601994052671860";
      "10495803222616830164930921154664460461646398358336997556169589368662143070925";
      "22898549214190047583215260016577644830295617833670028301698818524286997579532";
      "24393132143758164018011524734233512995814989110864264594937375305003558662082";
      "35599669100699975483818766527498585288817388816371602239888485323895149359158";
      "38006814568801552692257172170653057840209105926496657875471253681231978835474";
      "37543934971882261953367219974994268988229276972094897853703891601912512732069";
      "15638582370101925565491212811912002274875207706665814348068235624071156999370";
      "31580840665375344887237728746628275665874622958061630557939670052080082572146";
      "12367368728174853025325572761705668347969447581862767534739917589252910852407";
      "6431300041535226336752933722639922185807048849346218384550177388163783622203";
      "25253158156291597068997002534648267078756725939239005896820619368973386400618";
      "32407272173038095334116664653948892086910040424886147129262625126739839822771";
      "13280522211524717536348472783270194511863920959394096229476951226643221055230";
      "16772104472116956787783912564859125725251207740620474891039818280005602295238";
      "9380491773071000549418384879702223304167388163133689178789924347338789859850";
      "6740138750908982892458436295989575152579732709412893038486800886922449522370";
      "48314810935891480393270246846320465418304988645667044400639849377044382785493";
      "49525268202538850726708934355964079225214093569356591960731024652251573337974";
      "10491451908415598562758512398208310743863775903122876297029651957513361141458";
      "19406081409800592976259677521739333450025655891055151006357086244687039619147";
      "13796012858975195466491814297891072959260328291852781745607018638427554265885";
      "6485115628027826708347895792986221021092093804047270852634430130894243301376";
      "7032119811712255634773442378987402663863092963351749353790436863005730387277";
      "49570765767525444909530922468492577696342166915419424004169639950326136617057";
      "1285129643807481578340292178367830355589280266621317949423705788259432932006";
      "3441634142357505544306799203411944242234343920049337423233909232710820734846";
      "46025794658354018692379411175175073186560341494151624685587728046975000562010";
      "12106158677633440534700667787331666286230014762373964286877200484724425265456";
      "23852090676446145451864225599736384585160730887606821819365287956188313561217";
      "4645666973599908624611019322719702479503064932117311025810250241310882715612";
      "27973788552235695206305543261730414876912259984347644517174031345462270738555";
      "43025700336074147238459595423479529842575492457031762291142760348199150113491";
      "11114947607987207788072907159327922005689782074310097245997186074333396056216";
      "49687044256007315302113254820386474091495296180003075377414100433265777233121";
      "10121176151471384524101283711923697637725868232114641816445390512389391879025";
      "51330986445125278830864400207324675203699148153035087480401908084977553474061";
      "47310595279963533769585290517718071207229353045922336729470385238771992063949";
      "45470655810089077363013869164914020509319391456872208545345084082605634862224";
      "40929877503242649981348819772838274267223608227057310481110253536393018059255";
      "17372055570115191467281872597379815744802692968021921450248895690511846645695";
      "47678362609779802562177762420543329986622289631981586798104589503720694371775";
      "26411767877298533345027866329803788909747237313956364077530765489692282596278";
      "24229533690702187779130733022119521753205414714542053126286077188979825374531";
      "18497840321762427856624303545987123524462980182393573916022980133186401139409";
      "926339800459865307621110262317592729066835255833528961455819197753330330312";
      "26987605273411980269258666993213102373601884668454325175338172997856347972333";
      "18391274780315164583236795984691281435086666456604388825240216970397471681364";
      "12097832322841410456967729421116714442525972726222297222010623646121128815790";
      "49675177072983404142217920899359528991366227410655512062504000260893530407911";
      "15707135722931316515055649351245978339654864807851241599499601638769193005324";
      "13383342070542016733720366624023776259361772045149591256080689729754658059980";
      "50987374166360059560703430211826736262378937327825787684985599281463601570367";
      "37692333855557499699736644309219454870696030700215486572270708025082781551549";
      "48478650594548719294793600227459643485482841832424895683273572346673969340753";
      "34197000768287613413510926912918063900967585863143579777915396555872696168197";
      "42341791561950739851197883113950655969381083158985137996020454938455824791661";
      "50432013007639406618408631759754993701106347480289482412566889289659098747090";
      "33561349681426358960433818341708626828528089088226844117603110599540730269202";
      "50705077822458966913066394832821751993904360422435901531249988211620289538605";
      "45812150193659057136265559669604043591894801656607121583303377953470442982671";
      "44899405678979175008096051077001310599468936311348170044304489130853662237683";
      "7059127019337779356629411915385107326268136949565987358909106161315155646816";
      "34328690381291138075517043550284055917545629141111757511239996475405290993321";
      "26939654315244001880568035987806732594072719629182278790540271608004202736265";
      "30814725983945874115800588983627465902316483105630339244815320449875682709724";
      "8398481858488384468602034607148505717684965642826928411240604873022038757210";
      "32368995614504469151394179394757902584570432859893345667551706377300971640771";
      "41155627378215384456908425831665893311330630453454498015644998744726313357371";
      "2153340160120049982298930685564703679245036425190525326118018096283043155652";
      "30352448634031048114241985941470924393535967542582997762031027911599426568195";
      "15261716957885212013251887338156359768948744882202708080437574444095163828003";
      "38989413931358185435843776850185009130324946962753359173722889885807098911567";
      "1704331953122835388982301028858718889034690658545952309945645484614333632807";
      "27403750471903172003031534481941256144265878552723731083968505201259043778402";
      "17562955366799954474182871335569462132288297189443997453618631664362553626261";
      "19086162457604934210305997669117786907689549640695600906760353084525692086019";
      "909236720157425570791649582895043242306821976668909162225950852357093705234";
      "2587678208364293762041139325677564169740285152881638284308667606120057681746";
      "35455340013646018884370176867194236432498101681197729616134222175532845188407";
      "10597974015947868971053495476281648442554475914904865903565006092661125167077";
      "3237760185979457517707698614567204490221992393739789914647016856511321085131";
      "36946097031106423588593893994546210486025823406712493196127193878277998127793";
      "1562072353855994226121886801808336494359509412675230144523806046877228821245";
      "19010448428150791333165899594482872847843192038124839342939985299225110393618";
      "21579288013136572427312994291446922214090964937547933878834394360351661124147";
      "27476725675454012862496969681583556164753553840148186542141037944739225011404";
      "12721482754555216902365268649699780762391451537917039204354173116225938906231";
      "17726161376964586155439029895353641881124547308134311074590598308682629739586";
      "21277449426226092595780141778474905944490289128777491654503164263224221094647";
      "8027270477264632862462234106666097274072824365485884960263030432202348123210";
      "41704607970414222533592973837383672465179394179105424582475027116253727832320";
      "24911397878677534717817496400765259525912587429394942164360589864420581372895";
      "28487683264297785882293411974724574939733908335995066450236207591718649511876";
      "9410945672219127372505114826532796375498170564414051544192375021034240158151";
      "41501277216118808186585885765499182580814856188527129455247808366786573543421";
      "10786842188586265560953543650077602380076591787820349469333358966937440803493";
      "27009619599448135465453464435058428424786314448509662877166278927396974389912";
      "24408090401747031528777292030856366914050775066115322946199273876732066533603";
      "27717428010589203122459895369508850795775086801529508808907903171549714517552";
      "43961339117528688303727933814338246842560025117902212123957164184934798616272";
      "23539099267901977681530985543753979115801969780392578671053292012737090359960";
      "29129130787064690115403858309463936784595038310196943453528132510780666740275";
      "11544217335881527838309935861738104229903387666758470620902798348360616219319";
      "33462911116491023898914175915108269500003786821526355903193319352945031002857";
      "42971396791389197300566908724428992708740412328465643262012289069601063353167";
      "11114100576866102546082991452575837001302257906574345014759165856210897893390";
      "10869503142950375121273168986955759969708630281326506993743041491528703068926";
      "10056285389986129969950435124477608942343465496465667661560622683088232566646";
      "34352912333098020699609122066221942402647202729511926372551684177727356125767";
      "48815653149287031584900334425973245208502245603175731919813468058312231051539";
      "27279886970331272055453009825591093815823325722521311734285899406328214417219";
      "30743518328862506788849929078973418258912120322041236148115187319465176865909";
      "23836593777410321994736212695067663874445976812493472680359497431194677069707";
      "14271245249714372701863366640280358937336173352148459212765723706902523416666";
      "44751389477552162369260519320913279071846090137697398153616721749914975209463";
      "50049310530591903842202745108285775951310636397993830164309261859077944727008";
      "31203592346501430398694586706221740358145194595166035656399113862917383342162";
      "37447642270457825605341454299863838011561200065009939824839354876147406554050";
      "10574164763913009315349684560659607328049286937437594137678635676492164664990";
      "38325320802240945919839117157786458966683186777304529608044491498455717130551";
      "40805013056129827384501225380368635414535634360289381317746546936202290112538";
      "48333388268805149543196989643320441803480506998791523089965182033002284368947";
      "5782032582803275485235374665654094879290446054520008831705805183845211898185";
      "39802516355118908351021607643423040697458583372235828229304343199015399090975";
      "30492929460132725992608458300060364368351457395826268799884859998700261205304";
      "1420460004901060161999428487693270028427827250557258348019289211566581365454";
      "44193635056304562477505124994430538128890073548458826363763791536481254794966";
      "50720689419341593983069569011764146978553260482771698590157644701830829402947";
      "8073796990034033964469665366473997793181957677797087439421280810770488925256";
      "11918471565012754466601744707948105395283969402172028499903545447868170529713";
      "20077023346487118481621638270056399928015669807959870935567399723256898313150";
      "17213961046117186209464109755931248173988132541497089384021158920901269721090";
      "40806924151578521440897441275485084726249888295413627153644179743836373627459";
      "48180670522504204627184158154001766027012194162495506518370446939968021666069";
      "42003056523512230201797933267792902549574504149012715622767056620086275745478";
      "45101413241990392158966509799943874633896537344671548489389563011092925383814";
      "50587462404507583069240045742171989746743467775065297737509970837012535861612";
      "47815286514663372521264717191280262614050727424357000042525142008994950651639";
      "17400463065364361454879212497416099212109445911086039739080338012549330324535";
      "18161390929522210528368217943618859674698687969813941340329551243423634163215";
      "14441574882494975584903294130579023104909680031021053889713767896122879098657";
      "21912867184623729582081200571230217079961934918095841057644441114392793081978";
      "45361556540636295590917957481529238741505687644950500354869312727558668766825";
      "49539592650928368969231099603636984862255298622407911855462789343614490745974";
      "33869060934120743008239749284289212363453006243904282220127716668152965210748";
      "25076370715589585424326332620725315977885925199077963714556765297037513234989";
      "8002444064393390123216308842243771494245898705227632990107898963043446382143";
      "1356017732914259689267113844885694824971954414004791084036465384478863651474";
      "18698831976592497490869840317995921745505006029532075513759064786215310313034";
      "48836462159247124316625665463190819813831892402600021151195654650125270340651";
      "44079217861342722911981257144373371771560838079739791623631524927582118528474";
      "7917860632115468421843323257057624091855319060906343969030682698738062187742";
      "15328920775298393985301712443835521222368870056830753657709551066102881234707";
      "40585149282725386186676237190866920474926692908526104716015727560418525066965";
      "22476618951264551734672333363230193505101669500810396582135708891630628995331";
      "22976271519589645590337728787979950618802152541630285510037871742827357400405";
      "26490418622799095788111021654113322288820745026736077183862125058416171724885";
      "38668434553373591212556681994380448212723195862087041826021901890569924770065";
      "15734290460192933229142204966761293110558662629712541767317274191859409979185";
      "50708043312916419002750805838232616804578377791118982931279441695110104859619";
      "25661993114668520552639676665126758448336667422881593126449325707247794604888";
      "27300404692554829310057036397197575379085146250686335589922839236734268293026";
      "16616950908374247513630471498870667771958507881588444010494951003904728142357";
      "780331858290974370698544345229396895975774808594696606255314479320722478183";
      "15356252408972709076003921799298413990129664042289284426790671672668901277378";
      "22195679839447440563352896996056925121555070971714547978827589453261615780585";
      "50055031037344446643661166893394701232488862253278315780297281928041839024491";
      "39853343710092418340651301215898149540667450843137399936276811087705281337915";
      "41234320088350200826168830307183441504603558317128457459369045773720261208509";
      "41026304730141400072631269150112787967137999190332230376064990660056537630883";
      "46270298741623878847116335581496501056187952274321389849457282429215904661001";
      "24229852243440737653059813128440054999089637857670449169075813133344895934250";
      "8424306277967302875586430461180994699747156058101091594395383080190147483624";
      "49672959835707465722916473003774662744770586652374151972176418791640619586394";
      "50953606432923765425047764715621990710996981237692942916850916691445210588986";
      "44233571495113761415664137120393901177879884654356773130439945796774579578083";
      "11574634161412767461102549430739220546934205978274834090884125505175189074069";
      "8645184998607708462451095150206729904754427459024724873922986748255464652029";
      "37128418642109534373362468648382548670038346064741412903988995594256056481978";
      "33355443735171069266537113956815564199390017657125748952951909212993930853609";
      "18346976095151853612362092673379644124598042905694460090917547301686808797968";
      "32646375704171180130330224041820560945074015817182291941815877259349052407072";
      "43225167886161343156931475989059671126108470737009680929793198947446394575937";
      "8816437937287404337360397847635602367292009763466086832728768883240427981891";
      "38366899091948084905344245020593946957409036781563456341174116328327175180679";
      "800298045483712205484307334575942288725541659796453174814416446066185314381";
      "14508830287813168002435636185480014871079716479693496544419639273961439244196";
      "19123558056196698077756824716735733526899307503111963110801154666985150036515";
      "16303389189674597252380274616649999385814924811197807163354356674102789306574";
      "7453668915100625394664770229394717267390236182731660405097681417166662567678";
      "38798071571359045878565848619638213488585154176099273867945877100609620185282";
      "36631959497302172344707808434460251250381882633514089681745071353294520523286";
      "3295651438846461067006904471387575625423106106098387875100629738076787368486";
      "7639968555171428539513522652621621046079902482011709740085444603640503656201";
      "29579395581332007484259733934571852879364872891046795155379474874395906573519";
      "26653656757216667921153411281655535324426792606630320014981412395252223538329";
      "33945142010095644499737879503783227769340995607126548035094938552106092827502";
      "35659738763390756446419442911986047138385980543377566364330341100094367895238";
      "5380796247086464908504473508326895383205443609034527483380059328805596144573";
      "45555109220928268984543580497682265831199280528890734732631782982445734750732";
      "20535285005178766298291665162439441374276729776225027287990176172368474655430";
      "42276900911794446922826515302740555211179964292337862181106694848183792840849";
      "52163438563491625237964145588646657521828399654529930322643039527692977471445";
      "12381085634185465518625170120342681595340115886064341209590250417404145330796";
      "41332854461896499143467401552257229221502912725720917689641824107995364172760";
      "48130816341111135562667996573877686235140742636682402903593978927062615809300";
      "40708352896435303925197058053634288518207618858900910754332784721266337267119";
      "20414673166470607272747811391805104245858774907937409341200492727939746607797";
      "25627294268923401583055123311122337854601831198810692741217863178401731813982";
      "9471796077791050250358831370212483753463358283515022318409978072807223150958";
      "18314066421198133015325418115287580268791041525896152562360347711250600527843";
      "24017014751842644177743018360725989342257842302110775272063931146838823820708";
      "21581200003538126245980521668237719802680919088433705982480735447972766043363";
      "50184800347056048262055270151626286042367002765576087001102590179487127900402";
      "30495886812798520386657837931015291018488945515192090129642139250370928693580";
      "22576369160305502855935040778001809663355224383879666287087499574629468037932";
      "8892650559142637497217516060667987141940174680954367407928503085925759784531";
      "26585722842364766084323735392097803839711029569348840728693523172589688253154";
      "29233945065322679878626700781011757896403829828629855948960912667621036626304";
      "46495499699253457275171950570731129922763854056949062569251813711011602552765";
      "20175726311806847923316241767174947396593584808993154634747567993383544235788";
      "4439738901982759407797641994447539352385040803130129830312569441261131407125";
      "16457982232415810076025629044220925770877965806117341776311181746417552277025";
      "19907475632940820992995770155453308899317289306448422338160567626015082798255";
      "35223042914091176169939921699730780563001221818541154418947974752159293542388";
      "43001533944345692738449547388403626716967932955110192080457393496732555299619";
      "34125500451758985735535246859157148109918522814391361071782479828094264751521";
      "672210927468386341214054725731176563716514412831001669942787056703691451010";
      "11955392088705171556964578398079500139155403309741307240924960466165999666255";
      "15001212103447594119920182143104283078666143755444714277900928289186853558391";
      "12494141652757315459070169705561134159399433995127302554127714989589492762158";
      "12539864421219420825268500409099786634396457699752281899702857644933872397743";
      "43101784081867314199511257387329290804750329977663948322198895874188929154741";
      "27446223298884346343269149146243911653385549792135607763714158002175305061634";
      "1221810201232089129932400022193871837808173942749956359312713538906718836479";
      "27532908760517365244003806543506083069460105424541918130562804937168539380933";
      "15648693309686663323928562339596607937964297674438414931587554610267850089762";
      "51990644901841817393110558619667069965078896715337659449054804464607693143160";
      "33794620192818979295379085241975052389791263016087838781391920545764975674473";
      "101607244559760430212506597577050204264047733826203142005234996733194535803";
      "40666396311706682608077428065814708907526669028006167240560016976036610792591";
      "12093027072881844562446294223504358738044964433607132404028203137662407596800";
      "47855031407689076102071980457490179464098686349841578053656622219683394194927";
      "22887362617646323246137538576383771868750784401107098034751943222440904306549";
      "14772206578599333281746941359370160645118537874167329823865244020069915126081";
      "3526757700545255914615010391053602312122669226422265428284197630347896730651";
      "33007891082396853981232434558524697472333004416828682481099968575992162687374";
      "31988013417414141593906072198372172527694109442594239825489920432494911766933";
      "11191961053993644897418397896972876540611743197344140729636835194462710841804";
      "21880105207814770273563304401112493784911759454461136323535459121487533758411";
      "41486397989964301339068924325783394852002678141033490060445600519554945226014";
      "16498626461620337833657560298722288376309400783422382991374550718050901966642";
      "24943377286264067314569680564276927094588309007929081549392361988305161867433";
      "37986591875971070389212991388767178111861904302329418052260086662061715255565";
      "32017690217798460109067983234755326443554479110662411364776709358644611216536";
      "11268114558872136972649888237328080074799940976672472351727712756343878033991";
      "8553866868885110753717367996095488037219349823019339928639756785019374917125";
      "32329156174505548357975583161085823726178367498919221564757310317285457845069";
      "27211717469524004207872746964920608620364761642576492559180465819096139390446";
      "17951459528837145129192967424193834007781706018124597879528401736511208623124";
      "5641081412497253735686285180366403504609424502347938813022628844058433088254";
      "44149401842640426661188167090997457203149609985845860407845476505741286527400";
      "1131272348428881671180311242049529569730380344899908988923912651593170365621";
      "29408853361809783058473821719041796914748403385269196060920996759386405450822";
      "46397512824547164970111952967961313462600614947138288894235958387784135997027";
      "47516645729584090306484976699637881381716439437813917167035708795500295063993";
      "33055093158354315225697732538526252497152864807143121380155645175831367997411";
      "2483278713512874912077821925021730472549918913537260777217235941375925483743";
      "48815704230612764031863984553515469905544143230929551627072471933945117691529";
      "4328792740667001536219824544300358343992356873304526946361038441974068375040";
      "8936186593485597641227715388671424329734834396891419524831642301555170823192";
      "17951920387101669293331644306482124096994648510679825947980062912137916768437";
      "19375514622607648705471192919423809092605947096218527444759114794843323604399";
      "29610094038370566321951750688045410763551744002173884016718675203262367949199";
      "26412332356216088802741437584182840836365448342900386978712282658982011423028";
      "6857200692997830027964569096279902529051039382386370537664642602910884711585";
      "23793860449672430773141781094420115804950727589006926766592001526772413630888";
      "48757257789712605511132590475466929307721670979642060291457808809543669563707";
      "41645960082452856575583766422864660930176349173234319988174582522281045680944";
      "33000251418643291466811739862781501771791890505914908533407925955048210111449";
      "15394914111369858819577264515844393687512099293048804309053356275657357176587";
      "8206746691969770388090261805798801614135957851585811798250200766530283892894";
      "8853211220347505554369001872046201218026106125304684911336722654414177119527";
    |]
    |> Array.map Bls12_381.Fr.of_string

  (* Come from https://github.com/dusk-network/Hades252/tree/7a7a255f6cc48f892de5cf8935b5264eb8893852/assets *)
  let state_size_256_5_mds =
    [|
      [|
        "2184067777412762892935100798463195235577775932917057678850053321607193454182";
        "36777306597928096063744411004176639921441848277782639947444150234631715334827";
        "46505084276831565334480278148775967314861742095393016475696031258238207768284";
        "14474011154664524427946373126085988481658748083205070504932198000989141204992";
        "41996829456994127535645520838846415226858083018697639239163986389734003951389";
      |];
      [|
        "36777306597928096063744411004176639921441848277782639947444150234631715334827";
        "46505084276831565334480278148775967314861742095393016475696031258238207768284";
        "14474011154664524427946373126085988481658748083205070504932198000989141204992";
        "41996829456994127535645520838846415226858083018697639239163986389734003951389";
        "1092033888706381446467550399231597617788887966458528839425026660803596727091";
      |];
      [|
        "46505084276831565334480278148775967314861742095393016475696031258238207768284";
        "14474011154664524427946373126085988481658748083205070504932198000989141204992";
        "41996829456994127535645520838846415226858083018697639239163986389734003951389";
        "1092033888706381446467550399231597617788887966458528839425026660803596727091";
        "20060349053415325125678769638641803593513735424245076334969536491617299273542";
      |];
      [|
        "14474011154664524427946373126085988481658748083205070504932198000989141204992";
        "41996829456994127535645520838846415226858083018697639239163986389734003951389";
        "1092033888706381446467550399231597617788887966458528839425026660803596727091";
        "20060349053415325125678769638641803593513735424245076334969536491617299273542";
        "44606590886527143271596075756181302879566200389155138885023904467285148259670";
      |];
      [|
        "41996829456994127535645520838846415226858083018697639239163986389734003951389";
        "1092033888706381446467550399231597617788887966458528839425026660803596727091";
        "20060349053415325125678769638641803593513735424245076334969536491617299273542";
        "44606590886527143271596075756181302879566200389155138885023904467285148259670";
        "37141785804861502213823474505076128362854142474564156061360245762114092148579";
      |];
    |]
    |> Array.map (Array.map Bls12_381.Fr.of_string)

  let security_256_state_size_5 =
    {
      state_size = 5;
      nb_of_full_rounds = 8;
      nb_of_partial_rounds = 59;
      batch_size = 1;
      round_constants = state_size_256_5_ark;
      linear_layer = state_size_256_5_mds;
    }
end

type parameters = Parameters.t

type ctxt = Stubs.ctxt

let allocate_ctxt parameters =
  let open Parameters in
  let modified_ark =
    let ( arc_full_round_start_with_first_partial,
          arc_intermediate_state,
          arc_unbatched,
          arc_full_round_end ) =
      compute_updated_constants
        parameters.nb_of_partial_rounds
        parameters.nb_of_full_rounds
        parameters.state_size
        parameters.batch_size
        parameters.round_constants
        parameters.linear_layer
    in
    Array.concat
      [
        arc_full_round_start_with_first_partial;
        arc_intermediate_state;
        arc_unbatched;
        arc_full_round_end;
        (* Adding dummy constants, zeroes, for the last round as we apply the
           round key at the end of a full round. *)
        Array.init parameters.state_size (fun _ -> Bls12_381.Fr.(copy zero));
      ]
  in
  let mds_nb_rows = Array.length parameters.linear_layer in
  let mds_nb_cols = Array.length parameters.linear_layer.(0) in
  if mds_nb_cols <> mds_nb_rows then
    failwith "The parameter MDS must be a square matrix" ;
  let ctxt =
    Stubs.allocate_ctxt
      ~state_size:parameters.state_size
      ~nb_full_rounds:parameters.nb_of_full_rounds
      ~nb_partial_rounds:parameters.nb_of_partial_rounds
      ~batch_size:parameters.batch_size
      ~ark:modified_ark
      ~mds:parameters.linear_layer
  in
  ctxt

let get_state_size ctxt = Stubs.get_state_size ctxt

let set_state ctxt state =
  let exp_state_size = Stubs.get_state_size ctxt in
  let state_size = Array.length state in
  if state_size <> exp_state_size then
    failwith
      (Printf.sprintf
         "The given array contains %d elements but the expected state size is \
          %d"
         state_size
         exp_state_size) ;
  Stubs.set_state ctxt state

let get_state ctxt =
  let state_size = Stubs.get_state_size ctxt in
  let state = Array.init state_size (fun _ -> Bls12_381.Fr.(copy zero)) in
  Stubs.get_state state ctxt ;
  state

let apply_permutation ctxt = Stubs.apply_permutation ctxt