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
203
204
205
206
|
; -*- mode: Lisp; fill-column: 240 -*-
; Poseidon Library
;
; Copyright 2024 Provable Inc.
;
; Licensed under the Apache License, Version 2.0 (the "License");
; you may not use this file except in compliance with the License.
; You may obtain a copy of the License at
;
; http://www.apache.org/licenses/LICENSE-2.0
;
; Unless required by applicable law or agreed to in writing, software
; distributed under the License is distributed on an "AS IS" BASIS,
; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
; See the License for the specific language governing permissions and
; limitations under the License.
; 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-2-alpha-17
:parents (poseidon-instantiations)
:short "Instantiation of Poseidon with rate=2 and alpha=17."
:long
(xdoc::topstring
(xdoc::p
"This is an instantiation of Poseidon used internally by the
Aleo Instructions opcode "
(xdoc::ahref "https://developer.aleo.org/aleo/opcodes#hashpsd2" "hash.psd2")
".")
(xdoc::p
"Note, there are also some test cases for this instantiation
in the source file @('rate-2-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-2-ark* ; taken from .snap
'((1370773116404421539888881648821194629032979299946048429076387284005101684675 4673035637825817609038514733539555185313791666023633961663352080665830654830 3476986714632640194314485873881082667866912997891863048915892042674874286264)
(1082495278266482754833562621758308632581366365108718780801560341752506567697 4949432510532674124503328437030614426007112126335799011165573383397503068558 1330731268421256836250705136567442317504087954921291231955447229193812596308)
(2649505161225663922316999879032136225486779063673300240621719420078616600331 4969420587703679612645522006695883166296724515300508402438681500077273342102 205635712587803026777585519450868615715404988831679984758308345484658244699)
(6145772648854219628629735661952781083869402744236565775495743574991105198727 5694971131555029816374722311330556638260056256238039903705739439184187043937 5741725876337992913741719090196370235271299497940404104226910654118627348231)
(6469638413629030129780219709477213488269112947492045389237429028620220258446 3701595212702118832843766258638566924918883592466668319824165091176624488470 3788264172113320071929375505654410621672880197708720070568683533593741188367)
(7440115096888436553805393179190448787187286166192882400220572931865568317182 792346028642694686435936057983036575794551345818605100013220351237266490211 3512073197867644095949820682768614757198377867832806840119595329029395413419)
(3327088580126882425803902509250293076948968718390152099056814690231480975540 7158369207426751973498757672315193862013926247640641608613447343948389969907 6576114422707630183258306285876174832535448513519868242206479550748199028650)
(1750441329216804285131573838407988974537000108919914117251383215390240334007 6643642586767682146943021170325866479407987761019956931934065669737733844970 4106833857706706417652949425395842926674588555313556065852954705212767334548)
(5196247641080157421214976259470019902011109253162446920598369271583914387912 6360624992789526556614108772011303405529807087502693775123890278812066474754 8425833359837698797187325575646708254811496588866812335451071326764069753553)
(7571765444928048488636382364785227388831860339901373587410494373985769122100 1146560176939543249528183531911179059346379826648787355971780563762045417939 7065673187452873657602174269205792331276819829797382751854008973390840650347)
(2996886232144394882237600400269759049381836612341075168714674419715424495381 7668744387648470169368229696434415530109096020857128629089289952099341334341 936627698981026919732496023789041288394375500602254911470718843646602645053)
(6199749224785668013863210092063343076018531979597999604829468825162260274190 1653132234679858820482383205271489733007453315887823778464537322543673289375 7939359542319254103812635759696217625861967838748888560647186882218141754398)
(5250147394211818178524181700154433748053992647055590962793825894928645733326 235902753941634492088451291363018081809625358810315316265161104829935550542 6608963137139961850002639926351347514621255004982055637993898513250013620207)
(686840635267965663175276645211808051025823527505028096239338481540935993835 6836915689880452140045500520891176609600850753468429607484223074627863622754 4411311036661487117682008390277121256586135166845650218368031395328640568455)
(7765580651637884064091086941299831107821005732883926779656422881469118342677 332549754384827539552516583331436482626027168628972328124682073094327566178 8438579169602499403531276834153862236681805902767396281885988675130427183942)
(4371224392051444141538216717830171873522813314722974453159288159086172590441 4471819188266525256545603690402039960553559029943278641513107103995534212653 7934285249368611074358220926618133755594116808280441387064776330233673680433)
(3296929004083914338419828203502973195235748568216135964056267831058260996338 7828705062628438916991665037339807083733865061668384262916273779860279371794 6313358380505257639005175768394745400256528068580776946435054333930810425918)
(7673091158517942236320201239127705985446414040558434294512441355493079388101 3589839431787481799335476281766961640592432750884680804513596535388211513959 3497309798506406648010286927425548038594271991920637549888387014860982947288)
(3598928531842189258027744661377220155690961099878644839237443661252156892627 8323476545439527339398168929351847585459351691146904838200536423836775797722 2525233425021205371462807301191193452372106809085080242885832543937723343824)
(1670123541208150697178760793866430341950571765422973242642698972122650175931 2615994352824306042392204336460002628039562926557752567316988279659549764738 3845612285742795068547496524855308821681721826554794539870518271238257264872)
(8111729937113136682593516470591971173110681064547090000686075778488505769131 8396009887088699712099390488777898295472002649026341742255474271675851100167 7414449034416524223782013238252312102346828190465700203171291370882467344947)
(3778308769422683143427677977866154704853508570989688082271648398982585170107 2565370813801956884760401215151019368813258954878221563399238313359761598300 7277843344904687178893605017520459777796065293383180828267621160222576167983)
(6533305346353864830435743885484797433819452357103761181561861553139604158691 7023616807188225486961828699414844137821383541366139971758751915067616890468 6455936034448761051686329703810283225146169133435552271890713431685063292826)
(2781819771186595572605878483518345975589831093852202671865373784050027047498 7768920898267371999735782676903681841500678447293607126814923973294043875457 6463549363657422809088424260159871142005366302883731565233242485772646214776)
(4269033939844383336636476360431731618619965524039119758847937142713481376709 5618036788017776315188246458501777138795420885496187406031735668173200947333 1128431213282240763420656004648057492974288942591424362188971631793337713791)
(6900739195883338461228609955335408882714240356250551921341894223851444718631 3771335365721990684607605930021444592509300370948450043449389607062564762590 4101659620264578558029808267598816776989279597141521237379858078563415422176)
(7265965499850925058171553371274334440963706378337393611300731052328159723420 4766078774636290635629565607286497839044156826339894416138410680627572132174 6432220484581857509344049161489739648526811837695982886809250552529276108059)
(6361365189519422980433504384140223138978192212838226387265114914908491362931 7610377774980016354219333532677870219839779550900332138169496134065793623856 363180943030113865942993953461474483659264066502549823448101062593623940092)
(3562244767885763851343292605940116818317029725206904934994049890929589055395 7782549227482772885045540707357099585281118980712854335622177919009966444948 1275552603578693917501370061277948491143012995771911804618466157236333967239)
(5104148721380689096094143534135757186465840305075873333902995773940524349076 3827555903928560008785730325772720209567461775844698712063218244346202837926 6537952092752701292661689328736100739363623229800800023575262375504637794811)
(2625555787287768315537311869809801184270047957788564515280996906803464172085 2268046926631224821219360422346148209575446526490776085639666316914303207343 8301985790233975096406293902798523168400755923104779849614021896827941122062)
(6186410907907226666421909877388154922245464592386712702411681535145025981542 1570197114753247526703806268420919303949793186535455032181860083077073573260 6433616921731463425493337442585921501113569311931762833956390491384184622184)
(3730715929874541583946502538607860277000019933547155277889700636306045698678 4162712607911623590542516061947062496983700183068013598513127619182396118738 4885581468925689451043482261642022591161185334411569876922526171563347772487)
(679010986662603253067780482929422410547319947222192616893132766589997651700 7045332371454775389874918027434858274122123892961682451412342124928285105115 796483939088841221822094384379289433804847199444006131260701274900329521826)
(6930777873598706215302735286927888271122111082058406024378887982572264481712 3833261336312955683233981899122259611841384124139797023838966596495768744423 6081952172694136481884686958014712088378824178559544670607383857565862846284)
(3816381396460078181431529965953560061945407168453302734314638292833792891390 56734387980297685686110088096585973744605712015961903089771968507489169889 1528381975769046861077120384272922840572114805411576866912148437940560430592)
(4051427337822729290390706006634045761150954597129823553613464074823819976689 928801883926308717594921627141285880564599719525707838888160095066522021660 2575814441780474908465005749689528467553680700052052921662671958906858409792)
(4188482005041843983756841875722811236284873807578170011114849822278345286775 2055640774204777367415844703991682482137697203553277498227758201416424138567 4575553062307433825409075011087260276527850105624870927391350382554634786094)
(1854996916655462786356197865726500413712215270951193953965916926815164398288 4106990062567081635175461840146829007165341060131472749713325730182145598945 4440684113159162228103294475409844107272920293202271745070427054893404635089)))
; The MDS matrix is t by t, where t = capacity + rate
(defconst *poseidon-rate-2-mds* ; taken from .snap
'((6093452032963406658309134825240609333033222270199073508119142384975416392638 5968273173562867837210008744966745230923761158428968101807573098840850097286 1100466639266852149977689148055725793531897994956807001704693611715839541982)
(3160983601532844171864802850648492289862147997874094785600836495095965353712 2338351297827692414112631814274572996809824929139580588221558887342663769892 3177005087903404343485399282920555615020488967881372266904325860698809358885)
(2285176219817854683696635383059984246218458246545520061123961933072089703485 84377861777946561525373172505381054389617879929776365352216307785104476701 8280884008678095605415834125731826663585461281789631237939546251146561093166)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Make this a nullary function to make it easier to prevent expansion
; and easier to view in the debugger.
(define rate-2-alpha-17-parameters ()
:short "Poseidon parameters for Aleo circuit rate 2 implementation."
(make-param
:prime primes::*bls12-377-scalar-field-prime*
:rate 2
:capacity 1
:alpha 17
:full-rounds-half 4
:partial-rounds 31
:constants *poseidon-rate-2-ark*
:mds *poseidon-rate-2-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-2-domain-fe ()
:short "Domain separation field element for Aleo circuit rate 2 Poseidon hash."
(acl2::lendian=>nat 256 (acl2::chars=>nats (acl2::explode "Poseidon2"))))
; Regression test, and have the constant recorded.
(assert-equal
(rate-2-domain-fe)
930294893155900944208)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Interface functions.
; possible alternative: disable executable counterpart of (disable (:e param->prime))
(define hash2-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-hash2-many
:hints (("Goal" :use (:instance fe-listp-of-hash
(inputs (cons (rate-2-domain-fe)
(cons (len inputs)
inputs)))
(param (rate-2-alpha-17-parameters)))
:in-theory (disable fe-listp-of-hash))))
:short "Hash any reasonable number of inputs to any number of outputs using RATE=2"
:long
(xdoc::topstring
(xdoc::p
"The inputs and outputs are field elements.")
(xdoc::p
"This interface function prepends a domain-separation field element
and a field element whose value is the remaining number of inputs,
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-2-domain-fe)
(cons (len inputs)
inputs))))
(hash preimage-and-inputs (rate-2-alpha-17-parameters) count))
///
(more-returns
(outputs true-listp
:rule-classes :type-prescription
:hints (("Goal"
:use fe-listp-of-hash2-many
:in-theory (e/d (pfield::true-listp-when-fe-listp) (fe-listp-of-hash2-many))))))
(defret len-of-hash2-many
(equal (len outputs)
(nfix count)))
)
(define hash2 ((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-hash2
:hints (("Goal" :use (:instance len-of-hash2-many
(count 1))
:in-theory (disable len-of-hash2-many))))
:short "Hash any reasonable number of inputs to a single field output using RATE=2"
: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 (hash2-many inputs 1))
:guard-hints (("Goal" :in-theory (enable hash2-many))))
|
