1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
; -*- mode: Lisp; fill-column: 800 -*-
;
; Poseidon Library
;
; Copyright (C) 2024 Provable Inc.
;
; Authors: Alessandro Coglio (www.alessandrocoglio.info)
; Eric McCarthy (bendyarm on GitHub)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "POSEIDON")
(include-book "std/util/defval" :dir :system)
(include-book "kestrel/crypto/primes/bls12-377-prime" :dir :system)
(include-book "kestrel/utilities/strings/chars-codes" :dir :system)
(include-book "kestrel/utilities/digits-any-base/core" :dir :system)
(include-book "std/testing/assert-equal" :dir :system)
(include-book "main-definition")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ poseidon-rate-8-alpha-17
:parents (poseidon-instantiations)
:short "Instantiation of Poseidon with rate=8 and alpha=17."
:long
(xdoc::topstring
(xdoc::p
"This is the instantiation of Poseidon used internally by the
Aleo Instructions opcode "
(xdoc::ahref "https://developer.aleo.org/aleo/opcodes#hashpsd8" "hash.psd8")
".")
(xdoc::p
"Note, there are also some test cases for this instantiation
in the source file @('rate-8-alpha-17-tests.lisp')."))
:order-subtopics t
:default-parent t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; ark and mds matrices
; The ark matrix is #rounds rows, and t columns, where t = capacity + rate
(defconst *poseidon-rate-8-ark* ; taken from .snap
'((2806882019829952968543507592167502510188638053153774646465991640201889135551 7953247105561388613818796096585208374004041246553546421719675967186343612382 4209630100732310389470443719424678536445717817273388361307748937071916709762 2708657174353833177212161576417280079553606818497994462596920203325861488310 4914396193506640167561224216962140561302166360273879670360806295220567110846 295536384786706610813678639821769285888063882754058400585797169722730125203 7088161376195220545533298741851547842807908166700362538713989579699264509415 7532306175271927417091028238680678701320476535087824123390162112507462582920 1092348435238443378898980541087234894920999099851557323366945089973512075343)
(3387629280791160092745008617588796234120044636970795035833925422658657783884 6674303095240814412578024266313127907993265306795829285460480287269792488675 1171650099816562181663632811078645200323537422456123528833482703403343152177 6316447175412946600693561008623895654026892074059898051590587530503644921200 7404279336936038326557304138949407027440753805114996183705359328557575743398 7473790327527614629501497014077722791924475975982381415974524824697680354613 3672516199728669441433178675323852007453570382866812801329942248123137445478 7466476789295703004629427211536531887573219157834920653344192781739291131711 442431306194059143168495939289186121984155052360593764268495867628420272498)
(5567599045735327995732646653901770353675475602746634424155313248955796258861 7335724870860570727801345242182788096355483799486304264316134274522567012128 7959479429762265277864101047956303146795056511096709490257212384212236759140 2351258670587535228626660155390948638048894393464691022524802965999741673166 5235144232636468068308533276413903304582042208947218837467221083617314880204 1396911594804421619173173686144637658535607163292407925438997760512449247183 1411056441945545374240518413818008239910554233660820733484645124348796236730 1567690350302901882125860181011547763700945576304922471800350000710668041750 1601880862338588726059288722613531312969132685666192241750324840223532602882)
(5165452707727564003180969734649206880455904914873255216341963623364929898161 7431571243575718115166762666196431530393933188561556175224256619605671595052 8079770193659650620328033112588093897467243558010039805821639673749408389747 3732440051431269764990832963502001516496580250573468717987620964628761453508 4649994065677719818920260959937489690553054685169302708177452768977716522791 4170570437959433388087397253436245255853260240315455576763010400519635320096 5865530011699075906538860793649253983457515422987186694246022376257668589506 5857443034326126002914265813911290221568879913658079538263909313776438357983 7024623393151384926835944563471377438744311618211952734013568110723590939894)
(2549630801725007111193085378566793263468045835202701569276435785551532838138 2852303469671807667827657334480471925071240569608343090794747814603768546089 7249514523527674003111255523451463088975192102303778923274960356909660571357 4876209892158769081684874297148742215072010734782912956120844896195422484444 3996763149209794409569332270031298463561848480188391492948110738796990330859 5730262624493460234496984440095693188832536868361399644452809836644982114041 6376690763934998384710664623459727894610107372908429532469509285600382873170 6020210382802681129523958003511145807626319500885851292994990907904686009104 7525153136416607352592797999129915644512454151012224692685432347894411246586)
(5678885841624621095309707659605724926230071098672893521397658548439197311456 7831328658365028022033585708856558927438248765028704799197781820129606371394 492853156850581222331275109890096244508205313341056484333810095391535425985 2259503057324710572171537701248883352989417764625796294039706363680347416133 309657006833738433284646454949157576837640362834519907898814819009083868435 1680097847258528343352813319023261787930865758348218317804319183815115680426 8067459034252215888421854121509902831998744918599789211022212971028818066765 4372608603258705318507898179499426511082243971035079352245956082770072583347 4323880404878552197879603712776168079449327387979268638137862847834988729148)
(4989394347821742491949427145311980784321120941197410650098124541232000957319 2957154840523669611672993056544836016496948516661166759965975819186395790763 2504590134372870911436388735119115053121739478718019308636507248974717042368 6688473037709447857061858232972019178695941731808864718072159711173980630573 1842673539521848778024218630641912523846849278382441314221999654086766332628 168871589483082631197729534498313361581437845920735239212489937949616939096 1843314976306351376644485207293318238763012504363297816606588292768575054009 765812530281252435376360450028295792020877588658588839870620306147745881842 296065337135187843804077951527086706443308192751787939549475310584926486962)
(7439381682295122753565615301984039189684930281440290415617891805062653003889 4703662262479375272100466584332505889540233001772194952438636721020237312495 4621143766803298196692203507095532899061507464943403103295917995831120818968 2847207461025403823411936598178926718166380743151434582993013592938295734478 1611481409914711599767415203383742086045723516817669452618155689828527569463 1616591834607766360008264896763668263846698424155417463973070977152705712264 7496517885685442871873812682724770316871501436295402729706382423578737665034 774483519180888607455639911805771859732610316604312223031400696177695083473 8330614967631827792468258132090241213549975159633487997982795933006291397923)
(5472656179974287348643363132841548471539499328442810427967544367248087810252 2398910916026360365277326085012500010107318242993136147386953016274511816280 1814412591583817841305607617042895643219683064829182935065231821389827113382 1464256028914027786416226557378964719634836467752275330377633316803740134370 8148636618068765709102116218756106260676899132268843336149926824936651662645 2521205146106507896047966384494892960557444834158455399914728324580564142916 7576116187505626391623204648538571540376019652624834995384597370869358153738 231395589435939085986062872181123359818950983012241797573330027185504769236 7470793471750064918258306610309438044287822207945599768191292446553196328400)
(5029448085521616730694022369615178801079432243112073673181688518848690455046 8110082787691669361014456082063840862356048236088281343786354091596792674467 6437609978071442646264959388817531972455108706883016793991596362163035912774 5142977314064707121832440774285160209108825873985850176934619500199872596536 709048258744075021678175845901757800353176389975121896862158626971375405363 4031369321180990250054470013056064796619144993018304380668558979716387130813 7928138591508461350386188591638414684389522408960956818348559920734518778864 7857780012975387384560903348995909322519179012486201302433807896848873584084 6272156473580080416633847903535483243556290995475992475729074232017978992223)
(5157159974857819246570691121767273880061056767957933768099654515440255728041 8238047369415980951281334615340522510216806785581449495984040929632056040009 8357114215566597122111598126255647436395467043931002215981037940500429286001 7142898483988272410837510244085346143849539125729761852432604318818084265501 3525959191012203669737681485816627234294396785661188185634731196134206236900 428240821685308740519035572379270081329328776525906451409213863467230451007 1528226405266566805110134155963462558730385795035338049851625843013821837835 7652104307142633109480693208909197063408920055894146495261571096948429997232 1580807451602196467578728370303839407828636801072435089858497382105920919786)
(6550428316194672901989178267858858483908417419086273025561677000177360472598 7586055394079964130643874335757118875770911785757838297736312639360688960347 4747345542262298909507835852711510580083275117549493413983455755823170268860 3687384045064366355592755039891573113159432783611878629251695538410367094372 4334973840787287791539368735976710441488088858549545777693255305980900909422 1745241694218515021606710753741966370796282524073640227998447905109620178560 3431415561002294889273896346130292958853673101651159924762598194534335708011 4381568256287187638267465579619279098838602522409132427263575917299359003306 4424104188952377440606444541603106561283630486067416987192891019752199197184)
(2813021338148458513119319127815349837889938042576849917359253549422699693367 4768943950243362681446546195715941967863530216030744118705124508699935210859 8110401837226551961892248876156696544993413075117241143159317427737178620101 3762671667931500314147722160412629297027598570697085016795810681932662050848 2061804365904956423406853290898130936067929866732038708470619479075013080220 7521789161998123441095930388209994268793543466226644593000978827630168485005 3430018233958435552052408459170138903455047735840160758149013820961951169205 8052415037159878636365514935965941957313756798293316105908076532486760050715 4627027953057930048121729304349652424562011283704807436819052904965268958570)
(770171363074421770829607798441781763172332722373744180080847243526869252662 6778719413072186177700911796415751157751314188156415204328682850664193158323 3375660644806620551889704718311371249317777160849095252263544091221704474266 709759458315001689168359977176955936742669004456845295329003460912410373017 6187441934164439629836192031074922054082373648374828765583991388278470903063 1778859476708790205018462773823902421948933143229315149305010783162624661004 2448270227367799998766162073001504171261784143615105757594222998179217217463 3275689726433429811730625760246953298383812788940543010269099322665835684852 7841385419347757113793115370434487216768899746956205070275327898335297746552)
(3606519329602938016732752484020614833548856191081254339551305374778425045802 2879545695284183593950460750810637109140484186908245693068119655793554960834 1210571880547626065260343858532771197560800856322692702641310698281777388126 2261966181494540680736826672436420895102650752068632008606005321212668235113 5248963701267482825208485707705488209547860260912863465306239868567197132169 5342858989132583027309433460093582417723479100466485624048444391820166766092 7206707710352128208288732684772477428765322415296346775538901730816758593131 445288426397843092610983719643944271172718920237269877430473689287977667333 3931546005711348854514054434835333119985904385710579751699736360571763653642)
(5271383300107496776760771186644441106428729991459318791653230446547060161986 8051019910515747815873254889957498177815833466442172041448449338383896712630 826881434797287086702663642293273226235590511645075907186863165007534050377 480122060545311631644487698206350502762022350048301851311780204396693509430 1278442136534081986546563484110956980175426496350230924813790699374895251305 1194542117111929412898022110894421415971077687231391268424002154427957848737 2650626373644981932638790372395237133409811480802732614832201758150513351018 5623713656348387345777412039277110772813748202199586554300973561519183298107 2579041246910802030799554533563785281293680496416417918841026523570059304913)
(5655909122311143361668781127812119519986742524756048831698514027254257540113 4742759954783579474235520252360749171845865470290070342295273246512266855541 3638556303542752880372394213626352819437650634433258492774452971291107010995 7881140097639393330939655530654111268548352472835177103718956658132542644980 2360808279804851288346031767293829514962967455312010162957026170384661989869 3802991761628254651545902467001043965645585055237158274540402804002757213944 5395010738122229882589216793365079671456375241827210495029558833379299238047 471717569761844823416416313450901394773001595978235468400330553266457484796 4460811273534881541662865950232784275533033578361501586052604935973564619080)
(2610288555018277633180172902139781359760235989700305731804073746134582185294 721591341392217891024496194032938204955795335927028259176073492045422891727 2381180450651604237352753566492886011044519738492617697045416563917797818304 6275184939630690569930906949544388202809801399466164617759547806697078215002 8390853032030607485946864586665424615128808033911245013310579440822044422358 3385901706493368197234022980650238237093039485572216711858839884381756185387 6995417945558107572428345732810446730289330539373950798656466507436487419061 5739343533210286582354034905854942314259982701232865604927585417771429742442 3904469872041978345885586368216068429176375879007622807529381091209824642050)
(5102222966072920551609924538200406918998018143838604125324748318213346853014 949489051465015451325677142284020190671758961943632685567778157000539473305 6200545606419924032531974329163485441492280253587863353404731811169756900253 7953679656832464856346556258482722305771588161719809776342553707271126072008 3226202957185493353101759987534176861404815016078751927325567998440199661182 1620819951139395323849994764979600145027801787539748284141082009692581815914 5385507420884791193870569908085843852478781433461248795982073911433312708757 7209297489800574928319691556310906692340497800128963998741401560106786133968 6619367309220335627493636191084338868200998687670091678427950881518665180264)
(7525853737908237665102674926963483800285253846852169575560676089761761121490 4212504589091815688818771776355400646994189580837280732696331540631852844778 1616052256154873768023987658667481357731630771100001820856790700135536325244 1131909866193573445311174013529981507792580945342873668659563536919203856160 1605767156330163403827892239243575028984975963929530645352707452755841165462 5957041046809106073068143031570607736273084287851434060842392321541411575700 8068064349826635813131192691447590927096450524693969622851506004461313091193 5463404409658137119599397164565883549515650225973251874257319814061286379997 2155513604081155073955817245147696051309669097287192039368640058452518729833)
(1806993092599017301739195041009720456494185253323749431447919947755156653606 2966136564275088132129265926336191500769817447110466811586691840100573937505 5353768688653107159808098146807299867291789761352989070242322107511657871222 7367069942120638899481564960778363976822642884531094319217806546678542113619 4646033157940660087126289769777439743862622711363834136522792380229139990656 7761008990666868552353073571115725369151446628932714034737089759285964741651 2278398711809268673299739331391890616300741848782371438016241733081867047471 3780119117330691758382822757067768360459211483702834603646050667724603976328 3829933610683116264094004297905816907375393070487439866707346781523469118685)
(7997662110075666351735834253896731006244312355853925342601026515398149285498 7834897191126606972613148601547963682788121066696477610022704840399147873042 6230009053380706996083336774134600806526720835880568402150974032000652199683 1691785708800132050344242908720482093286446117640890212729547486696967424917 1892149389331799506307032028851715034129340007729413502483946630844742495533 4244974645303642862347167829109628360403825986452156179164270532198768375029 4782354099081300307989877709664980128779027716082640049745075123364690322338 2209461582192115305195912952785101207487255627730127690302944860541076254030 1895279508478463322644000508169648299354474815336200944494967142432608092812)
(7354615869483716942175226414047116555871109065654067315061955029682435366134 8358063842230731126882236192914337920554534541213012117317418026310644402078 7838403614911155306083348159735285598737240468526657697218515261132141141557 5162855920399677263966174677245875024227211837961211061783731181724065887589 1271246412151738423599582070850121071517574712573543045244142329333047368064 1098291478573034602410613017528600162317717195488733112587729414880698928304 5332269051178598703550075657382380242300659967049783538654233080490809831904 1186131394032636619315318556663597567227554945738308526069106153158954159884 1131107898235394355159213862157333186288370429691709767635876747231002220048)
(4387061745163365134536271965373484892675546312128913337144778511848562786889 5399083735548955046190784377266581429176248846091154234801512047145603328600 2960894959200690718298617750349786055393653727306691796575977613756300001021 6742363415214513068800467904313672523207662372749779406529883697809601496174 3815027474864184322396882596270924220938186888651179409441359374892709435976 7006060680099224141899890561771010239213061908245686053723044372284356814328 1310262856628841899343513222803215215523460731577893282637535938176546128053 7935359883050090551188290462454499669489917997885995502215905180579241975896 5106492513648030277740766527610273235449076891265712277767605804394132546754)
(1286962689132382481840160673683507087451273787390753038686488240564254163972 4067208694314006978301813862348447861881719717942211819928057688739199749023 7124202881858440784870218531335769487177165724326312402042950453366582210374 3196480308603501455795703509854787569826167393656277666819805045212038823488 4873031862625284082840072575828038018789879527145757091904713085731528752257 4832441588020304784792928888085852660503602523533402063633745078244016319234 6421663079811856766731178801145288329097232161373754890069959178561045383500 537567683308944401050300174065516915526088779560845869235644056769319201823 6126455090506407861504412382238323028117568893640400033369568166903658871766)
(1792844118859848481163741158099730698249056923918380212685013252460933887169 5524106373662745692910027274039905499899984239025991265557087286339142510750 5777963625430462472717953906178865414026627551056679524913629318499800374652 2382190640174471414450081476745588918536996007437139218143761591932747333172 603604343048436100769589838038283547884975584649620923186447634595029048091 2069418633159152451088062189316735418318474864188602015926680493029867081674 5782658519422946191046352412159358240417245687978214359105012742010457569318 884588679401944255630005556077555544003428561842230755406363054406385178584 7759578938461111255704167479297599301307391423336657382256603344950200499565)
(3561708701305664669471604456603433952256533843853768157207749537514467942143 5690688803199998718404848826111380845802184403108817934168567426027808129597 3192112822753566399058225882371183464336941100901165311721779089518820485058 7192388083107503618563437178263224087151181156409483679687309962361551781501 6586001119836557779379417677800634983506127812221385233244367614353573293892 8433275641930685781821863273694263058085899212908820106438860162210556370208 7528611556364408078050375569198442226468826837011841140719680247799343744596 703620727484730721319141661431718104855801711166546799810617942987706497601 3616179015167614734396082224023734885052796289996553997091908627020451537877)
(6346727447205815701429655239869400221627454100896859881691879920741827383373 3738870365633581641567308704087610739287023903185812774243416352339043245746 4451376008416706275501240270548752290992051130613783918997446422811643700210 3328024219280030630582709813307356650176243676483698101846769363460351898417 7061819691810074581052858152804033340764510248400374572725534934605188080386 7395022706511889150800777287371861054600016507936101554569053224861450068820 5602339239011901533202928685782621149364516872778528456004679141419974620557 5369647328773690419580912362063259439140194100686031954437533741494464662063 7631336087907304934744127932288338664785987460720415805279254172397806770233)
(4547479486383380855319173619252013135577790568999733870704615113212162268300 6473218807239136309175819216951724989744022766122750144545838268487887719981 7017062290747675541831968517858842069857011721927946862703172556553658786655 2731370543857178803854561015488810444909067858670046898068955920412991484289 4104547605003949350470218523301214397731096140399950611439920541560788218759 1694747307067104122251013246306626884397162528089055696122361538692506563122 5006882484238937622282121066041408243802640620280004873124026070148354205958 8340788306727521860726728749752428522904038115530226156646843731200661796252 5222870324795647085758910188580635110264193244470872419679479006596008782304)
(546281900264852237539326543731583331658097643948679448044425257747924618822 4021558503226872685188599075959902967617354437068425944688263206069474659093 5977582077639120540882440179250284066775369559199134213179244171439309213555 7306279940526391587145985447894635896071088605086786083552882537558647848489 5510262282448022589518040514260963704606988624295294733840653421507392592112 5647332449464210157942253722769540402975131549364666744323387303543984797468 6409877864924456316359746390054474162860049114311986407388801537967554768317 1577932864534398684375811055884003673001139481464973188344764578530958881741 4703546144584173136613925374871993996623578663549827144935191229421335193122)
(731257450853078772289304107141193658301337077264276892400775813873147831378 313473907817493437902129211675385980374286519987678467133825202912959344892 769323851648612813029007038511165103363954325252326796675427554752962149839 6916971205384173074819535074281770255072926285989184840716482425743693208472 7569885514147759510492885072812768170042210853897933910331754479603836983067 1036253428167149501139973374176457618018129686665695451777250553901630683622 455366088092074409013722375856547252623404410524141871909070549089225702096 5628349397220944882076016530754648903578678665336137189455770851852324046479 3658542062402586628640579863909521347018064129992690479801341535046831754040)
(2338695634823929973807951664624640672699522710731260221164335735321356670404 8217936689912538478584409386057193159390029541400090346004000317610679053037 3255935411569630617698159777401109206861941274428203431356009451357044246468 8315991139031493348154402582053754194902384171689441788098015161424831253981 3721646286550539399960618100488745278822154738881729340651132896540916331898 5454899882236771200954729068041406519981564005138640869286877403368512200170 2851432367819618255765312527287910908676659054622557646473531058473484247843 8163870640406259559570079651891238291728715603030023163943948014670021301738 3903668299195440918219935426497100144730881812193735928992362762032571315243)
(4881895242495631475141058841299921123154211005797430042204053128742585833595 6177119647731036949184323464636374397798234393335371833531291813339405405362 4152173055009358551679246768416155189040765756046269402178578759327014130199 1690326830835402837087828435679036622079875109679624559919382512425796868805 836542722616753708205183052069421656849387295824858211040318222641310997964 5154372515366959096578493728737615951237354245164447089064654656654737269150 8211882276256250874195482980748775323112853964641154691545239902071055927517 4671076582313928280095721693833018423546929324706277032981112163122827391196 3911661568533242658734525394301291112898047963907993737905119525906547536227)
(1841458974196368371037172372569887608737786129279657997555334661446579082076 4610928573269023127031937981753420855106772041737039342917476259229801964783 5713968680123462147881491951533889440965890790241528430565516968598088153441 1312858373446646191554011683584724586479993811462450726476757284705060700019 6575019323694990273255733783803236612268855822623657420275811046677738392241 2247922781961658976178550551599457427327796980714321335979865915891927756559 1386276356218750889858752840354898226046285370019852411888434351593414304816 3913370657880242438092240277693349791191479978563620927076943664630586214195 5973145785034801836729248659912758160892875591579071799255755873133486026796)
(341512804667925057083092830303365698432250494403043639435560218293195837562 160895951580389706659907027483151875213333010019551276998320919296228647317 8334099740396373026754940038411748941117628023990297711605274995172393663866 6508516067551208838086421306235504440162527555399726948591414865066786644888 5260580011132523115913756761919139190330166964648541423363604516046903841683 5364551699340921126666868355866939894481659185100479400603118274281861821633 3674066413309338422416216473958582675169915385409011506980101661947061762850 6089678617608113083923592896806550278443104377373709501664309910090765415546 6726106378605858332527139412082732860344829813597195980987777258184388930397)
(2996623582643535968094092734748634267437456916702490683520023531675940735251 1066299182733912299977577599302716102002738653010828827086884529157392046228 1977519953625589014039847898215240724041194773120013187722954068145627219929 1618348632868002512910764605250139381231860094469042556990470848701700964713 1157459381876765943377450451674060447297483544491073402235960067133285590974 5298236609772405279593752222902041704789667250912138819252061446709116778660 6974011484123198318137673875976573470980696656331842268727413000800460504043 3537330457015472572035437842225265462344123811786458942680852640549163387370 4641912165003191972375287669923666268884784048345023237765199657149838164586)
(3609270259990306509398906329626938258600521378091862454121014717258070025318 2241061724039470158487229089505123379386376040366677537043719491567584322339 4450395467941419565906844040025562669400620759737863109185235386261110553073 3763549180544198711495347718218896634621699987767108409942867882747700142403 1834649076610684411560795826346579299134200286711220272747136514724202486145 3330794675297759513930533281299019673013197332462213086257974185952740704073 5929621997900969559642343088519370677943323262633114245367700983937202243619 8211311402459203356251863974142333868284569297703150729090604853345946857386 3940918639550186633137910755014539941607503792857029778093574261965117018602)
(1200191697757979418325161979569707209062505050490558308163874179392788193480 3912308888616251672812272013988802988420414245857866136212784631403027079860 4100923705771018951561873336835055979905965765839649442185404560120892958216 5701101373789959818781445339314572139971317958997296225671698446757742149719 5785597627944719799683455467917641287692417422465938462034769734951914291948 7114563815762200851408085187508391374176957207477684923891429124014152652019 3449981208711757723253092077239727571315820659357981502515684674545336808636 1494785435086439930074023714558690402569866060612974338095965942335481916666 5559087334151237083403116950881822335957965948680035909778235211195474233838)
(6591044377942830746091296841086781137650941715236925502916636959397483722471 214818498460401597228033958287537426429167258531438668351703993840760770582 4497884203527978976088488455523871581608892729212445595385399904032800522087 4010331535874074900042223641934450423780782982190514529696596753456937384201 6067637133445382691713836557146174628934072680692724940823629181144890569742 5966421531117752671625849775894572561179958822813329961720805067254995723444 3931621787437169432081350272895729413874740194038049241027071656893555590399 356632626599222161610283546928228710267634046857241188698902611247395943760 2222695123731804671898759958264892525212796616676613023322738578439345523267))
)
; The MDS matrix is t by t, where t = capacity + rate
(defconst *poseidon-rate-8-mds*
'((3195939821470342407043866187037485190412960074203265869296316033794290707270 8192999172287681978279937705484780209698661207375769758856214590447668659103 1665163833558793134901638856359158517426266045166622406883753300854106512133 2449323359783449939971620411100757168597711619642133905105139552556745653655 7997054509376614612478892971990071898042005712049464815984455966308522818321 4555043748994907879169314788407046522094670487469991975952733061011231124083 4220020953881675228052350163693177709395032941921773866940137655004312512639 6140894171802652360785515137586631217522889399255586808033915037001216040977 4989259181903499544646700172492807664060080972756633790331935903190270228190)
(697803788815986345601601330313660859365440719263778333868781527433783449571 2026091974998222616602188362308290303501972667130640949077975270335809845403 6206075751069269905707439983001875051435534429020421682405039061392585300498 1464939134024816013774540031869332285004750070390455669023649553483899815656 2907833318518803687716961895380693105486571105787061697370242877001462607970 5238651046585462724284164251954632695845998694171105229707534426063480175524 3079751201386093353296964674446576551306341900148526772765947048995787750297 2405587386664055630654065632134520200107765790464370415562343982536672490320 5575903494865596878754842108705737910435780159785678405009281428896603682231)
(4469798835198444546916330968558933081228153970715554991291913917927696066613 59204161935304065637509255108163146974273455256599445484154695693620027176 5245859476292151600200677265533610166667683825767642751148496038891598375998 3501408804777215283662219469185625031813093089503048081399116904156452158334 5831201328300360628584696062941324134945275477439080917904254648229685394378 5722074739256548820385451845894511284247422903956941157718514060268665186038 4181413630337445736836198637188012116342519506215705555946434207635903063812 4492144215532121199695805763885568108083759766617272940108988062267687160291 1612560838516989776222036361361222739637371694875979327361105314605332391424)
(7953749166116749549253003928004776389374576588475899384013586151659143849837 6153802489206433377917059113433805010158264256347055705224264345316908843047 5281028029734566778880272955609248756519350618367255820126580204010134272241 7792058682161837330899571443207157817751964966813420786697452336810793603850 3380992253160248496953383536986648681236129094471266537502054404528803123260 3504945083968383797099482535773353341406224917148034262696844007866755493591 6064734000320673669749334564078943159381042080255237567943800636821059667781 6782524386335950509890523431068361631725821487351818796274643940120498217850 2153218424016457404078212740710051128293155340021557696253674035873657438750)
(3620059470289043734062892638376864996895707384584571820250032189417117153277 6736331289337345444729361387338422809027692253158668415458282440630693464286 1389573522841108453411129248618540478518866237272209443598793955549294244111 7536696420957075865417847234666768134686303107809129224258456330638643096561 8365161861294129182650896837616835474341532431309409544964309813542919968363 8434084005082771644611578048781921012598011131920352439214229400041306214083 2750548395764276413363080018634112240079324332969486569935092884455713799323 4959211069908119180134850630775227057955779261703865929401337722528476837939 7659833953527652231877260925978903674910813449699072095570803967720443533704)
(5684032818099481924921681530595548171547404450297014204085234823635471362374 1135135675423514061561049973549610147196984437585230361509130320992410661325 1029187681938329826566872456170907037433789329950914477900148354354863240195 3491715990597707058568313905402749540968468421211864924809605262623735853167 7168317248801406623927664171891530550391378208378623841519775703352290315043 1649471994030090271983785929570950685731765308909911065344726697619294501571 618655241035555529248944974385435189465158747382644065785058014859525805607 3866945461701990101780215922488478938212491220967378583866841030872392013910 1592193401508732840254871014256822755399425325702415181941293031461205814179)
(1460566483811622418591307178233279213660057810890076468304893120634307292382 1818006159963986740920722136413611067532051156094491674761667226298511368274 4014423002025547732947550660316233069630275033177273370486634024050074305602 538084293539756081602182792400459423151507360940409586854372868101057925102 8385521515659289735680837803725809430374844246800899804313226422909249791288 6679563729266586409002899773541147235942478365814888891022023265423509541687 3458040072957251647421946562064169784509317301597776520132997940473510601097 1867771395381271834522491259485584999456788663588326557789367887846988040923 1713899847379613547377427421720483917103884729237419458190016956334867685225)
(1402661654834849948208414955493379802426114184069202735017655681808067189975 3801852864665033841774715284518384682376829752661853198612247855579120198106 8354898322875240371401674517397790035008442020361740574117886421279083828480 4810388512520169167962815122521832339992376865086300759308552937986944510606 1806278863067630397941269234951941896370617486625414347832536440203404317871 4017177598231920767921734423139954103557056461408532722673217828464276314809 4502122148343933124673154378613890139567720582268024644020209068919416902214 4561829712907233792471674922406483420574947340289420058610189883205900987113 6148338654730560071040421189313196324157983353250055388836104661881521574716)
(8159682927754000992321184499997107098749343396015601482130535740628509397238 5875458165131202198687456465132303861996162717895733590135903107762343629586 369689081101970051654464068728946984508029041063982163515876043614865310223 8090746012031721314085811588103730937574817095108146541180098921277401730689 6507604872493162886464118469227907850209464370879492905037848895266033072042 1871499703193787598722336027158458679846087700726158474066616161770353775755 2845267823865273840574612844588974809740242353743053403429113456533348630811 7159850948497071111825071237736057149842575696322662301463787483519703327031 7907342083471017768552185139305524785354620391900552744466864799424145439241))
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Make this a nullary function to make it easier to prevent expansion
; and easier to view in the debugger.
(define rate-8-alpha-17-parameters ()
:short "Poseidon parameters for Aleo circuit rate 8 implementation."
(make-param
:prime primes::*bls12-377-scalar-field-prime*
:rate 8
:capacity 1
:alpha 17
:full-rounds-half 4
:partial-rounds 31
:constants *poseidon-rate-8-ark*
:mds *poseidon-rate-8-mds*
:rate-then-capacity-p nil
:ascending-p t
:partial-first-p t))
; Make this a nullary function so the meaning is more obvious in the debugger.
(define rate-8-domain-fe ()
:short "Domain separation field element for Aleo circuit rate 8 Poseidon hash."
(acl2::lendian=>nat 256 (acl2::chars=>nats (acl2::explode "Poseidon8"))))
; Regression test, and have the constant recorded.
(assert-equal
(rate-8-domain-fe)
1040975357598158253904)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Interface functions.
(define hash8-many ((inputs (fe-listp inputs primes::*bls12-377-scalar-field-prime*))
(count natp))
:guard (fep (len inputs) primes::*bls12-377-scalar-field-prime*)
:returns (outputs (fe-listp outputs
primes::*bls12-377-scalar-field-prime*)
:name fe-listp-of-hash8-many
:hints (("Goal" :use (:instance fe-listp-of-hash
;; this :use hint must match the preimage calc below
(inputs (cons (rate-8-domain-fe)
(cons (len inputs)
(append (repeat 6 0)
inputs))))
(param (rate-8-alpha-17-parameters)))
:in-theory (disable fe-listp-of-hash))))
:short "Hash any reasonable number of inputs to any number of outputs using RATE=8"
:long
(xdoc::topstring
(xdoc::p
"The inputs and outputs are field elements.")
(xdoc::p
"This interface function prepends RATE elements to the input to construct the
preimage: [ DOMAIN || LENGTH(INPUT) || [0; RATE-2] || INPUT ],
and then calls the main hash function.")
(xdoc::p
"The number of inputs must be less than the field size so that the length
field is expressable."))
(let ((preimage-and-inputs
(cons (rate-8-domain-fe)
(cons (len inputs)
(append (repeat 6 0) ; 6 zeros to pad to RATE=8
inputs)))))
(hash preimage-and-inputs (rate-8-alpha-17-parameters) count))
///
(more-returns
(outputs true-listp
:rule-classes :type-prescription
:hints (("Goal"
:use fe-listp-of-hash8-many
:in-theory (e/d (pfield::true-listp-when-fe-listp) (fe-listp-of-hash8-many))))))
(defret len-of-hash8-many
(equal (len outputs)
(nfix count)))
)
(define hash8 ((inputs (fe-listp inputs primes::*bls12-377-scalar-field-prime*)))
:guard (fep (len inputs) primes::*bls12-377-scalar-field-prime*)
:returns (output (fep output primes::*bls12-377-scalar-field-prime*)
:name fep-of-hash8
:hints (("Goal" :use (:instance len-of-hash8-many
(count 1))
:in-theory (disable len-of-hash8-many))))
:short "Hash any reasonable number of inputs to a single field output using RATE=8"
:long
(xdoc::topstring
(xdoc::p
"The inputs and output are field elements.")
(xdoc::p
"This interface function prepends a domain-separation field element
and a remaining input-length field element,
and then calls the main hash function with an output count of 1.")
(xdoc::p
"The number of inputs must be less than the field size."))
(first (hash8-many inputs 1))
:guard-hints (("Goal" :in-theory (enable hash8-many))))
|
