From 5b28926d3c641491b15c96b1fee91e13a5ee540d Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Sun, 3 Mar 2024 23:35:01 +0000 Subject: [PATCH] Updated to latest extractor --- lean-circuit/LeanCircuit.lean | 314 +++++++------- lean-circuit/LeanCircuit/Common.lean | 11 + lean-circuit/LeanCircuit/Poseidon.lean | 74 ++++ .../LeanCircuit/Poseidon/Constants.lean | 46 --- .../LeanCircuit/Poseidon/Correctness.lean | 391 ------------------ lean-circuit/LeanCircuit/Poseidon/Spec.lean | 42 -- .../LeanCircuit/SemanticEquivalence.lean | 173 ++++---- lean-circuit/Main.lean | 44 +- lean-circuit/lake-manifest.json | 8 +- lean-circuit/lakefile.lean | 7 +- 10 files changed, 358 insertions(+), 752 deletions(-) create mode 100644 lean-circuit/LeanCircuit/Common.lean create mode 100644 lean-circuit/LeanCircuit/Poseidon.lean delete mode 100644 lean-circuit/LeanCircuit/Poseidon/Constants.lean delete mode 100644 lean-circuit/LeanCircuit/Poseidon/Correctness.lean delete mode 100644 lean-circuit/LeanCircuit/Poseidon/Spec.lean diff --git a/lean-circuit/LeanCircuit.lean b/lean-circuit/LeanCircuit.lean index e0d99e4..81723a3 100644 --- a/lean-circuit/LeanCircuit.lean +++ b/lean-circuit/LeanCircuit.lean @@ -1,6 +1,8 @@ import ProvenZk.Gates import ProvenZk.Ext.Vector +set_option linter.unusedVariables false + namespace Semaphore def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 @@ -14,23 +16,23 @@ def sbox (Inp: F) (k: F -> Prop): Prop := k gate_2 def mds_3 (Inp: Vector F 3) (k: Vector F 3 -> Prop): Prop := - ∃gate_0, gate_0 = Gates.mul Inp[0] 7511745149465107256748700652201246547602992235352608707588321460060273774987 ∧ - ∃gate_1, gate_1 = Gates.add 0 gate_0 ∧ - ∃gate_2, gate_2 = Gates.mul Inp[1] 10370080108974718697676803824769673834027675643658433702224577712625900127200 ∧ + ∃gate_0, gate_0 = Gates.mul Inp[0] (7511745149465107256748700652201246547602992235352608707588321460060273774987:F) ∧ + ∃gate_1, gate_1 = Gates.add (0:F) gate_0 ∧ + ∃gate_2, gate_2 = Gates.mul Inp[1] (10370080108974718697676803824769673834027675643658433702224577712625900127200:F) ∧ ∃gate_3, gate_3 = Gates.add gate_1 gate_2 ∧ - ∃gate_4, gate_4 = Gates.mul Inp[2] 19705173408229649878903981084052839426532978878058043055305024233888854471533 ∧ + ∃gate_4, gate_4 = Gates.mul Inp[2] (19705173408229649878903981084052839426532978878058043055305024233888854471533:F) ∧ ∃gate_5, gate_5 = Gates.add gate_3 gate_4 ∧ - ∃gate_6, gate_6 = Gates.mul Inp[0] 18732019378264290557468133440468564866454307626475683536618613112504878618481 ∧ - ∃gate_7, gate_7 = Gates.add 0 gate_6 ∧ - ∃gate_8, gate_8 = Gates.mul Inp[1] 20870176810702568768751421378473869562658540583882454726129544628203806653987 ∧ + ∃gate_6, gate_6 = Gates.mul Inp[0] (18732019378264290557468133440468564866454307626475683536618613112504878618481:F) ∧ + ∃gate_7, gate_7 = Gates.add (0:F) gate_6 ∧ + ∃gate_8, gate_8 = Gates.mul Inp[1] (20870176810702568768751421378473869562658540583882454726129544628203806653987:F) ∧ ∃gate_9, gate_9 = Gates.add gate_7 gate_8 ∧ - ∃gate_10, gate_10 = Gates.mul Inp[2] 7266061498423634438633389053804536045105766754026813321943009179476902321146 ∧ + ∃gate_10, gate_10 = Gates.mul Inp[2] (7266061498423634438633389053804536045105766754026813321943009179476902321146:F) ∧ ∃gate_11, gate_11 = Gates.add gate_9 gate_10 ∧ - ∃gate_12, gate_12 = Gates.mul Inp[0] 9131299761947733513298312097611845208338517739621853568979632113419485819303 ∧ - ∃gate_13, gate_13 = Gates.add 0 gate_12 ∧ - ∃gate_14, gate_14 = Gates.mul Inp[1] 10595341252162738537912664445405114076324478519622938027420701542910180337937 ∧ + ∃gate_12, gate_12 = Gates.mul Inp[0] (9131299761947733513298312097611845208338517739621853568979632113419485819303:F) ∧ + ∃gate_13, gate_13 = Gates.add (0:F) gate_12 ∧ + ∃gate_14, gate_14 = Gates.mul Inp[1] (10595341252162738537912664445405114076324478519622938027420701542910180337937:F) ∧ ∃gate_15, gate_15 = Gates.add gate_13 gate_14 ∧ - ∃gate_16, gate_16 = Gates.mul Inp[2] 11597556804922396090267472882856054602429588299176362916247939723151043581408 ∧ + ∃gate_16, gate_16 = Gates.mul Inp[2] (11597556804922396090267472882856054602429588299176362916247939723151043581408:F) ∧ ∃gate_17, gate_17 = Gates.add gate_15 gate_16 ∧ k vec![gate_5, gate_11, gate_17] @@ -42,7 +44,7 @@ def fullRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop) sbox gate_1 fun gate_4 => sbox gate_2 fun gate_5 => mds_3 vec![gate_3, gate_4, gate_5] fun gate_6 => - k vec![gate_6[0], gate_6[1], gate_6[2]] + k gate_6 def halfRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop): Prop := ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧ @@ -50,88 +52,88 @@ def halfRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop) ∃gate_2, gate_2 = Gates.add Inp[2] Consts[2] ∧ sbox gate_0 fun gate_3 => mds_3 vec![gate_3, gate_1, gate_2] fun gate_4 => - k vec![gate_4[0], gate_4[1], gate_4[2]] + k gate_4 def poseidon_3 (Inputs: Vector F 3) (k: Vector F 3 -> Prop): Prop := - fullRound_3_3 vec![Inputs[0], Inputs[1], Inputs[2]] vec![6745197990210204598374042828761989596302876299545964402857411729872131034734, 426281677759936592021316809065178817848084678679510574715894138690250139748, 4014188762916583598888942667424965430287497824629657219807941460227372577781] fun gate_0 => - fullRound_3_3 vec![gate_0[0], gate_0[1], gate_0[2]] vec![21328925083209914769191926116470334003273872494252651254811226518870906634704, 19525217621804205041825319248827370085205895195618474548469181956339322154226, 1402547928439424661186498190603111095981986484908825517071607587179649375482] fun gate_1 => - fullRound_3_3 vec![gate_1[0], gate_1[1], gate_1[2]] vec![18320863691943690091503704046057443633081959680694199244583676572077409194605, 17709820605501892134371743295301255810542620360751268064484461849423726103416, 15970119011175710804034336110979394557344217932580634635707518729185096681010] fun gate_2 => - fullRound_3_3 vec![gate_2[0], gate_2[1], gate_2[2]] vec![9818625905832534778628436765635714771300533913823445439412501514317783880744, 6235167673500273618358172865171408902079591030551453531218774338170981503478, 12575685815457815780909564540589853169226710664203625668068862277336357031324] fun gate_3 => - halfRound_3_3 vec![gate_3[0], gate_3[1], gate_3[2]] vec![7381963244739421891665696965695211188125933529845348367882277882370864309593, 14214782117460029685087903971105962785460806586237411939435376993762368956406, 13382692957873425730537487257409819532582973556007555550953772737680185788165] fun gate_4 => - halfRound_3_3 vec![gate_4[0], gate_4[1], gate_4[2]] vec![2203881792421502412097043743980777162333765109810562102330023625047867378813, 2916799379096386059941979057020673941967403377243798575982519638429287573544, 4341714036313630002881786446132415875360643644216758539961571543427269293497] fun gate_5 => - halfRound_3_3 vec![gate_5[0], gate_5[1], gate_5[2]] vec![2340590164268886572738332390117165591168622939528604352383836760095320678310, 5222233506067684445011741833180208249846813936652202885155168684515636170204, 7963328565263035669460582454204125526132426321764384712313576357234706922961] fun gate_6 => - halfRound_3_3 vec![gate_6[0], gate_6[1], gate_6[2]] vec![1394121618978136816716817287892553782094854454366447781505650417569234586889, 20251767894547536128245030306810919879363877532719496013176573522769484883301, 141695147295366035069589946372747683366709960920818122842195372849143476473] fun gate_7 => - halfRound_3_3 vec![gate_7[0], gate_7[1], gate_7[2]] vec![15919677773886738212551540894030218900525794162097204800782557234189587084981, 2616624285043480955310772600732442182691089413248613225596630696960447611520, 4740655602437503003625476760295930165628853341577914460831224100471301981787] fun gate_8 => - halfRound_3_3 vec![gate_8[0], gate_8[1], gate_8[2]] vec![19201590924623513311141753466125212569043677014481753075022686585593991810752, 12116486795864712158501385780203500958268173542001460756053597574143933465696, 8481222075475748672358154589993007112877289817336436741649507712124418867136] fun gate_9 => - halfRound_3_3 vec![gate_9[0], gate_9[1], gate_9[2]] vec![5181207870440376967537721398591028675236553829547043817076573656878024336014, 1576305643467537308202593927724028147293702201461402534316403041563704263752, 2555752030748925341265856133642532487884589978209403118872788051695546807407] fun gate_10 => - halfRound_3_3 vec![gate_10[0], gate_10[1], gate_10[2]] vec![18840924862590752659304250828416640310422888056457367520753407434927494649454, 14593453114436356872569019099482380600010961031449147888385564231161572479535, 20826991704411880672028799007667199259549645488279985687894219600551387252871] fun gate_11 => - halfRound_3_3 vec![gate_11[0], gate_11[1], gate_11[2]] vec![9159011389589751902277217485643457078922343616356921337993871236707687166408, 5605846325255071220412087261490782205304876403716989785167758520729893194481, 1148784255964739709393622058074925404369763692117037208398835319441214134867] fun gate_12 => - halfRound_3_3 vec![gate_12[0], gate_12[1], gate_12[2]] vec![20945896491956417459309978192328611958993484165135279604807006821513499894540, 229312996389666104692157009189660162223783309871515463857687414818018508814, 21184391300727296923488439338697060571987191396173649012875080956309403646776] fun gate_13 => - halfRound_3_3 vec![gate_13[0], gate_13[1], gate_13[2]] vec![21853424399738097885762888601689700621597911601971608617330124755808946442758, 12776298811140222029408960445729157525018582422120161448937390282915768616621, 7556638921712565671493830639474905252516049452878366640087648712509680826732] fun gate_14 => - halfRound_3_3 vec![gate_14[0], gate_14[1], gate_14[2]] vec![19042212131548710076857572964084011858520620377048961573689299061399932349935, 12871359356889933725034558434803294882039795794349132643274844130484166679697, 3313271555224009399457959221795880655466141771467177849716499564904543504032] fun gate_15 => - halfRound_3_3 vec![gate_15[0], gate_15[1], gate_15[2]] vec![15080780006046305940429266707255063673138269243146576829483541808378091931472, 21300668809180077730195066774916591829321297484129506780637389508430384679582, 20480395468049323836126447690964858840772494303543046543729776750771407319822] fun gate_16 => - halfRound_3_3 vec![gate_16[0], gate_16[1], gate_16[2]] vec![10034492246236387932307199011778078115444704411143703430822959320969550003883, 19584962776865783763416938001503258436032522042569001300175637333222729790225, 20155726818439649091211122042505326538030503429443841583127932647435472711802] fun gate_17 => - halfRound_3_3 vec![gate_17[0], gate_17[1], gate_17[2]] vec![13313554736139368941495919643765094930693458639277286513236143495391474916777, 14606609055603079181113315307204024259649959674048912770003912154260692161833, 5563317320536360357019805881367133322562055054443943486481491020841431450882] fun gate_18 => - halfRound_3_3 vec![gate_18[0], gate_18[1], gate_18[2]] vec![10535419877021741166931390532371024954143141727751832596925779759801808223060, 12025323200952647772051708095132262602424463606315130667435888188024371598063, 2906495834492762782415522961458044920178260121151056598901462871824771097354] fun gate_19 => - halfRound_3_3 vec![gate_19[0], gate_19[1], gate_19[2]] vec![19131970618309428864375891649512521128588657129006772405220584460225143887876, 8896386073442729425831367074375892129571226824899294414632856215758860965449, 7748212315898910829925509969895667732958278025359537472413515465768989125274] fun gate_20 => - halfRound_3_3 vec![gate_20[0], gate_20[1], gate_20[2]] vec![422974903473869924285294686399247660575841594104291551918957116218939002865, 6398251826151191010634405259351528880538837895394722626439957170031528482771, 18978082967849498068717608127246258727629855559346799025101476822814831852169] fun gate_21 => - halfRound_3_3 vec![gate_21[0], gate_21[1], gate_21[2]] vec![19150742296744826773994641927898928595714611370355487304294875666791554590142, 12896891575271590393203506752066427004153880610948642373943666975402674068209, 9546270356416926575977159110423162512143435321217584886616658624852959369669] fun gate_22 => - halfRound_3_3 vec![gate_22[0], gate_22[1], gate_22[2]] vec![2159256158967802519099187112783460402410585039950369442740637803310736339200, 8911064487437952102278704807713767893452045491852457406400757953039127292263, 745203718271072817124702263707270113474103371777640557877379939715613501668] fun gate_23 => - halfRound_3_3 vec![gate_23[0], gate_23[1], gate_23[2]] vec![19313999467876585876087962875809436559985619524211587308123441305315685710594, 13254105126478921521101199309550428567648131468564858698707378705299481802310, 1842081783060652110083740461228060164332599013503094142244413855982571335453] fun gate_24 => - halfRound_3_3 vec![gate_24[0], gate_24[1], gate_24[2]] vec![9630707582521938235113899367442877106957117302212260601089037887382200262598, 5066637850921463603001689152130702510691309665971848984551789224031532240292, 4222575506342961001052323857466868245596202202118237252286417317084494678062] fun gate_25 => - halfRound_3_3 vec![gate_25[0], gate_25[1], gate_25[2]] vec![2919565560395273474653456663643621058897649501626354982855207508310069954086, 6828792324689892364977311977277548750189770865063718432946006481461319858171, 2245543836264212411244499299744964607957732316191654500700776604707526766099] fun gate_26 => - halfRound_3_3 vec![gate_26[0], gate_26[1], gate_26[2]] vec![19602444885919216544870739287153239096493385668743835386720501338355679311704, 8239538512351936341605373169291864076963368674911219628966947078336484944367, 15053013456316196458870481299866861595818749671771356646798978105863499965417] fun gate_27 => - halfRound_3_3 vec![gate_27[0], gate_27[1], gate_27[2]] vec![7173615418515925804810790963571435428017065786053377450925733428353831789901, 8239211677777829016346247446855147819062679124993100113886842075069166957042, 15330855478780269194281285878526984092296288422420009233557393252489043181621] fun gate_28 => - halfRound_3_3 vec![gate_28[0], gate_28[1], gate_28[2]] vec![10014883178425964324400942419088813432808659204697623248101862794157084619079, 14014440630268834826103915635277409547403899966106389064645466381170788813506, 3580284508947993352601712737893796312152276667249521401778537893620670305946] fun gate_29 => - halfRound_3_3 vec![gate_29[0], gate_29[1], gate_29[2]] vec![2559754020964039399020874042785294258009596917335212876725104742182177996988, 14898657953331064524657146359621913343900897440154577299309964768812788279359, 2094037260225570753385567402013028115218264157081728958845544426054943497065] fun gate_30 => - halfRound_3_3 vec![gate_30[0], gate_30[1], gate_30[2]] vec![18051086536715129874440142649831636862614413764019212222493256578581754875930, 21680659279808524976004872421382255670910633119979692059689680820959727969489, 13950668739013333802529221454188102772764935019081479852094403697438884885176] fun gate_31 => - halfRound_3_3 vec![gate_31[0], gate_31[1], gate_31[2]] vec![9703845704528288130475698300068368924202959408694460208903346143576482802458, 12064310080154762977097567536495874701200266107682637369509532768346427148165, 16970760937630487134309762150133050221647250855182482010338640862111040175223] fun gate_32 => - halfRound_3_3 vec![gate_32[0], gate_32[1], gate_32[2]] vec![9790997389841527686594908620011261506072956332346095631818178387333642218087, 16314772317774781682315680698375079500119933343877658265473913556101283387175, 82044870826814863425230825851780076663078706675282523830353041968943811739] fun gate_33 => - halfRound_3_3 vec![gate_33[0], gate_33[1], gate_33[2]] vec![21696416499108261787701615667919260888528264686979598953977501999747075085778, 327771579314982889069767086599893095509690747425186236545716715062234528958, 4606746338794869835346679399457321301521448510419912225455957310754258695442] fun gate_34 => - halfRound_3_3 vec![gate_34[0], gate_34[1], gate_34[2]] vec![64499140292086295251085369317820027058256893294990556166497635237544139149, 10455028514626281809317431738697215395754892241565963900707779591201786416553, 10421411526406559029881814534127830959833724368842872558146891658647152404488] fun gate_35 => - halfRound_3_3 vec![gate_35[0], gate_35[1], gate_35[2]] vec![18848084335930758908929996602136129516563864917028006334090900573158639401697, 13844582069112758573505569452838731733665881813247931940917033313637916625267, 13488838454403536473492810836925746129625931018303120152441617863324950564617] fun gate_36 => - halfRound_3_3 vec![gate_36[0], gate_36[1], gate_36[2]] vec![15742141787658576773362201234656079648895020623294182888893044264221895077688, 6756884846734501741323584200608866954194124526254904154220230538416015199997, 7860026400080412708388991924996537435137213401947704476935669541906823414404] fun gate_37 => - halfRound_3_3 vec![gate_37[0], gate_37[1], gate_37[2]] vec![7871040688194276447149361970364037034145427598711982334898258974993423182255, 20758972836260983284101736686981180669442461217558708348216227791678564394086, 21723241881201839361054939276225528403036494340235482225557493179929400043949] fun gate_38 => - halfRound_3_3 vec![gate_38[0], gate_38[1], gate_38[2]] vec![19428469330241922173653014973246050805326196062205770999171646238586440011910, 7969200143746252148180468265998213908636952110398450526104077406933642389443, 10950417916542216146808986264475443189195561844878185034086477052349738113024] fun gate_39 => - halfRound_3_3 vec![gate_39[0], gate_39[1], gate_39[2]] vec![18149233917533571579549129116652755182249709970669448788972210488823719849654, 3729796741814967444466779622727009306670204996071028061336690366291718751463, 5172504399789702452458550583224415301790558941194337190035441508103183388987] fun gate_40 => - halfRound_3_3 vec![gate_40[0], gate_40[1], gate_40[2]] vec![6686473297578275808822003704722284278892335730899287687997898239052863590235, 19426913098142877404613120616123695099909113097119499573837343516470853338513, 5120337081764243150760446206763109494847464512045895114970710519826059751800] fun gate_41 => - halfRound_3_3 vec![gate_41[0], gate_41[1], gate_41[2]] vec![5055737465570446530938379301905385631528718027725177854815404507095601126720, 14235578612970484492268974539959119923625505766550088220840324058885914976980, 653592517890187950103239281291172267359747551606210609563961204572842639923] fun gate_42 => - halfRound_3_3 vec![gate_42[0], gate_42[1], gate_42[2]] vec![5507360526092411682502736946959369987101940689834541471605074817375175870579, 7864202866011437199771472205361912625244234597659755013419363091895334445453, 21294659996736305811805196472076519801392453844037698272479731199885739891648] fun gate_43 => - halfRound_3_3 vec![gate_43[0], gate_43[1], gate_43[2]] vec![13767183507040326119772335839274719411331242166231012705169069242737428254651, 810181532076738148308457416289197585577119693706380535394811298325092337781, 14232321930654703053193240133923161848171310212544136614525040874814292190478] fun gate_44 => - halfRound_3_3 vec![gate_44[0], gate_44[1], gate_44[2]] vec![16796904728299128263054838299534612533844352058851230375569421467352578781209, 16256310366973209550759123431979563367001604350120872788217761535379268327259, 19791658638819031543640174069980007021961272701723090073894685478509001321817] fun gate_45 => - halfRound_3_3 vec![gate_45[0], gate_45[1], gate_45[2]] vec![7046232469803978873754056165670086532908888046886780200907660308846356865119, 16001732848952745747636754668380555263330934909183814105655567108556497219752, 9737276123084413897604802930591512772593843242069849260396983774140735981896] fun gate_46 => - halfRound_3_3 vec![gate_46[0], gate_46[1], gate_46[2]] vec![11410895086919039954381533622971292904413121053792570364694836768885182251535, 19098362474249267294548762387533474746422711206129028436248281690105483603471, 11013788190750472643548844759298623898218957233582881400726340624764440203586] fun gate_47 => - halfRound_3_3 vec![gate_47[0], gate_47[1], gate_47[2]] vec![2206958256327295151076063922661677909471794458896944583339625762978736821035, 7171889270225471948987523104033632910444398328090760036609063776968837717795, 2510237900514902891152324520472140114359583819338640775472608119384714834368] fun gate_48 => - halfRound_3_3 vec![gate_48[0], gate_48[1], gate_48[2]] vec![8825275525296082671615660088137472022727508654813239986303576303490504107418, 1481125575303576470988538039195271612778457110700618040436600537924912146613, 16268684562967416784133317570130804847322980788316762518215429249893668424280] fun gate_49 => - halfRound_3_3 vec![gate_49[0], gate_49[1], gate_49[2]] vec![4681491452239189664806745521067158092729838954919425311759965958272644506354, 3131438137839074317765338377823608627360421824842227925080193892542578675835, 7930402370812046914611776451748034256998580373012248216998696754202474945793] fun gate_50 => - halfRound_3_3 vec![gate_50[0], gate_50[1], gate_50[2]] vec![8973151117361309058790078507956716669068786070949641445408234962176963060145, 10223139291409280771165469989652431067575076252562753663259473331031932716923, 2232089286698717316374057160056566551249777684520809735680538268209217819725] fun gate_51 => - halfRound_3_3 vec![gate_51[0], gate_51[1], gate_51[2]] vec![16930089744400890347392540468934821520000065594669279286854302439710657571308, 21739597952486540111798430281275997558482064077591840966152905690279247146674, 7508315029150148468008716674010060103310093296969466203204862163743615534994] fun gate_52 => - halfRound_3_3 vec![gate_52[0], gate_52[1], gate_52[2]] vec![11418894863682894988747041469969889669847284797234703818032750410328384432224, 10895338268862022698088163806301557188640023613155321294365781481663489837917, 18644184384117747990653304688839904082421784959872380449968500304556054962449] fun gate_53 => - halfRound_3_3 vec![gate_53[0], gate_53[1], gate_53[2]] vec![7414443845282852488299349772251184564170443662081877445177167932875038836497, 5391299369598751507276083947272874512197023231529277107201098701900193273851, 10329906873896253554985208009869159014028187242848161393978194008068001342262] fun gate_54 => - halfRound_3_3 vec![gate_54[0], gate_54[1], gate_54[2]] vec![4711719500416619550464783480084256452493890461073147512131129596065578741786, 11943219201565014805519989716407790139241726526989183705078747065985453201504, 4298705349772984837150885571712355513879480272326239023123910904259614053334] fun gate_55 => - halfRound_3_3 vec![gate_55[0], gate_55[1], gate_55[2]] vec![9999044003322463509208400801275356671266978396985433172455084837770460579627, 4908416131442887573991189028182614782884545304889259793974797565686968097291, 11963412684806827200577486696316210731159599844307091475104710684559519773777] fun gate_56 => - halfRound_3_3 vec![gate_56[0], gate_56[1], gate_56[2]] vec![20129916000261129180023520480843084814481184380399868943565043864970719708502, 12884788430473747619080473633364244616344003003135883061507342348586143092592, 20286808211545908191036106582330883564479538831989852602050135926112143921015] fun gate_57 => - halfRound_3_3 vec![gate_57[0], gate_57[1], gate_57[2]] vec![16282045180030846845043407450751207026423331632332114205316676731302016331498, 4332932669439410887701725251009073017227450696965904037736403407953448682093, 11105712698773407689561953778861118250080830258196150686012791790342360778288] fun gate_58 => - halfRound_3_3 vec![gate_58[0], gate_58[1], gate_58[2]] vec![21853934471586954540926699232107176721894655187276984175226220218852955976831, 9807888223112768841912392164376763820266226276821186661925633831143729724792, 13411808896854134882869416756427789378942943805153730705795307450368858622668] fun gate_59 => - halfRound_3_3 vec![gate_59[0], gate_59[1], gate_59[2]] vec![17906847067500673080192335286161014930416613104209700445088168479205894040011, 14554387648466176616800733804942239711702169161888492380425023505790070369632, 4264116751358967409634966292436919795665643055548061693088119780787376143967] fun gate_60 => - fullRound_3_3 vec![gate_60[0], gate_60[1], gate_60[2]] vec![2401104597023440271473786738539405349187326308074330930748109868990675625380, 12251645483867233248963286274239998200789646392205783056343767189806123148785, 15331181254680049984374210433775713530849624954688899814297733641575188164316] fun gate_61 => - fullRound_3_3 vec![gate_61[0], gate_61[1], gate_61[2]] vec![13108834590369183125338853868477110922788848506677889928217413952560148766472, 6843160824078397950058285123048455551935389277899379615286104657075620692224, 10151103286206275742153883485231683504642432930275602063393479013696349676320] fun gate_62 => - fullRound_3_3 vec![gate_62[0], gate_62[1], gate_62[2]] vec![7074320081443088514060123546121507442501369977071685257650287261047855962224, 11413928794424774638606755585641504971720734248726394295158115188173278890938, 7312756097842145322667451519888915975561412209738441762091369106604423801080] fun gate_63 => - fullRound_3_3 vec![gate_63[0], gate_63[1], gate_63[2]] vec![7181677521425162567568557182629489303281861794357882492140051324529826589361, 15123155547166304758320442783720138372005699143801247333941013553002921430306, 13409242754315411433193860530743374419854094495153957441316635981078068351329] fun gate_64 => - k vec![gate_64[0], gate_64[1], gate_64[2]] + fullRound_3_3 Inputs vec![(6745197990210204598374042828761989596302876299545964402857411729872131034734:F), (426281677759936592021316809065178817848084678679510574715894138690250139748:F), (4014188762916583598888942667424965430287497824629657219807941460227372577781:F)] fun gate_0 => + fullRound_3_3 gate_0 vec![(21328925083209914769191926116470334003273872494252651254811226518870906634704:F), (19525217621804205041825319248827370085205895195618474548469181956339322154226:F), (1402547928439424661186498190603111095981986484908825517071607587179649375482:F)] fun gate_1 => + fullRound_3_3 gate_1 vec![(18320863691943690091503704046057443633081959680694199244583676572077409194605:F), (17709820605501892134371743295301255810542620360751268064484461849423726103416:F), (15970119011175710804034336110979394557344217932580634635707518729185096681010:F)] fun gate_2 => + fullRound_3_3 gate_2 vec![(9818625905832534778628436765635714771300533913823445439412501514317783880744:F), (6235167673500273618358172865171408902079591030551453531218774338170981503478:F), (12575685815457815780909564540589853169226710664203625668068862277336357031324:F)] fun gate_3 => + halfRound_3_3 gate_3 vec![(7381963244739421891665696965695211188125933529845348367882277882370864309593:F), (14214782117460029685087903971105962785460806586237411939435376993762368956406:F), (13382692957873425730537487257409819532582973556007555550953772737680185788165:F)] fun gate_4 => + halfRound_3_3 gate_4 vec![(2203881792421502412097043743980777162333765109810562102330023625047867378813:F), (2916799379096386059941979057020673941967403377243798575982519638429287573544:F), (4341714036313630002881786446132415875360643644216758539961571543427269293497:F)] fun gate_5 => + halfRound_3_3 gate_5 vec![(2340590164268886572738332390117165591168622939528604352383836760095320678310:F), (5222233506067684445011741833180208249846813936652202885155168684515636170204:F), (7963328565263035669460582454204125526132426321764384712313576357234706922961:F)] fun gate_6 => + halfRound_3_3 gate_6 vec![(1394121618978136816716817287892553782094854454366447781505650417569234586889:F), (20251767894547536128245030306810919879363877532719496013176573522769484883301:F), (141695147295366035069589946372747683366709960920818122842195372849143476473:F)] fun gate_7 => + halfRound_3_3 gate_7 vec![(15919677773886738212551540894030218900525794162097204800782557234189587084981:F), (2616624285043480955310772600732442182691089413248613225596630696960447611520:F), (4740655602437503003625476760295930165628853341577914460831224100471301981787:F)] fun gate_8 => + halfRound_3_3 gate_8 vec![(19201590924623513311141753466125212569043677014481753075022686585593991810752:F), (12116486795864712158501385780203500958268173542001460756053597574143933465696:F), (8481222075475748672358154589993007112877289817336436741649507712124418867136:F)] fun gate_9 => + halfRound_3_3 gate_9 vec![(5181207870440376967537721398591028675236553829547043817076573656878024336014:F), (1576305643467537308202593927724028147293702201461402534316403041563704263752:F), (2555752030748925341265856133642532487884589978209403118872788051695546807407:F)] fun gate_10 => + halfRound_3_3 gate_10 vec![(18840924862590752659304250828416640310422888056457367520753407434927494649454:F), (14593453114436356872569019099482380600010961031449147888385564231161572479535:F), (20826991704411880672028799007667199259549645488279985687894219600551387252871:F)] fun gate_11 => + halfRound_3_3 gate_11 vec![(9159011389589751902277217485643457078922343616356921337993871236707687166408:F), (5605846325255071220412087261490782205304876403716989785167758520729893194481:F), (1148784255964739709393622058074925404369763692117037208398835319441214134867:F)] fun gate_12 => + halfRound_3_3 gate_12 vec![(20945896491956417459309978192328611958993484165135279604807006821513499894540:F), (229312996389666104692157009189660162223783309871515463857687414818018508814:F), (21184391300727296923488439338697060571987191396173649012875080956309403646776:F)] fun gate_13 => + halfRound_3_3 gate_13 vec![(21853424399738097885762888601689700621597911601971608617330124755808946442758:F), (12776298811140222029408960445729157525018582422120161448937390282915768616621:F), (7556638921712565671493830639474905252516049452878366640087648712509680826732:F)] fun gate_14 => + halfRound_3_3 gate_14 vec![(19042212131548710076857572964084011858520620377048961573689299061399932349935:F), (12871359356889933725034558434803294882039795794349132643274844130484166679697:F), (3313271555224009399457959221795880655466141771467177849716499564904543504032:F)] fun gate_15 => + halfRound_3_3 gate_15 vec![(15080780006046305940429266707255063673138269243146576829483541808378091931472:F), (21300668809180077730195066774916591829321297484129506780637389508430384679582:F), (20480395468049323836126447690964858840772494303543046543729776750771407319822:F)] fun gate_16 => + halfRound_3_3 gate_16 vec![(10034492246236387932307199011778078115444704411143703430822959320969550003883:F), (19584962776865783763416938001503258436032522042569001300175637333222729790225:F), (20155726818439649091211122042505326538030503429443841583127932647435472711802:F)] fun gate_17 => + halfRound_3_3 gate_17 vec![(13313554736139368941495919643765094930693458639277286513236143495391474916777:F), (14606609055603079181113315307204024259649959674048912770003912154260692161833:F), (5563317320536360357019805881367133322562055054443943486481491020841431450882:F)] fun gate_18 => + halfRound_3_3 gate_18 vec![(10535419877021741166931390532371024954143141727751832596925779759801808223060:F), (12025323200952647772051708095132262602424463606315130667435888188024371598063:F), (2906495834492762782415522961458044920178260121151056598901462871824771097354:F)] fun gate_19 => + halfRound_3_3 gate_19 vec![(19131970618309428864375891649512521128588657129006772405220584460225143887876:F), (8896386073442729425831367074375892129571226824899294414632856215758860965449:F), (7748212315898910829925509969895667732958278025359537472413515465768989125274:F)] fun gate_20 => + halfRound_3_3 gate_20 vec![(422974903473869924285294686399247660575841594104291551918957116218939002865:F), (6398251826151191010634405259351528880538837895394722626439957170031528482771:F), (18978082967849498068717608127246258727629855559346799025101476822814831852169:F)] fun gate_21 => + halfRound_3_3 gate_21 vec![(19150742296744826773994641927898928595714611370355487304294875666791554590142:F), (12896891575271590393203506752066427004153880610948642373943666975402674068209:F), (9546270356416926575977159110423162512143435321217584886616658624852959369669:F)] fun gate_22 => + halfRound_3_3 gate_22 vec![(2159256158967802519099187112783460402410585039950369442740637803310736339200:F), (8911064487437952102278704807713767893452045491852457406400757953039127292263:F), (745203718271072817124702263707270113474103371777640557877379939715613501668:F)] fun gate_23 => + halfRound_3_3 gate_23 vec![(19313999467876585876087962875809436559985619524211587308123441305315685710594:F), (13254105126478921521101199309550428567648131468564858698707378705299481802310:F), (1842081783060652110083740461228060164332599013503094142244413855982571335453:F)] fun gate_24 => + halfRound_3_3 gate_24 vec![(9630707582521938235113899367442877106957117302212260601089037887382200262598:F), (5066637850921463603001689152130702510691309665971848984551789224031532240292:F), (4222575506342961001052323857466868245596202202118237252286417317084494678062:F)] fun gate_25 => + halfRound_3_3 gate_25 vec![(2919565560395273474653456663643621058897649501626354982855207508310069954086:F), (6828792324689892364977311977277548750189770865063718432946006481461319858171:F), (2245543836264212411244499299744964607957732316191654500700776604707526766099:F)] fun gate_26 => + halfRound_3_3 gate_26 vec![(19602444885919216544870739287153239096493385668743835386720501338355679311704:F), (8239538512351936341605373169291864076963368674911219628966947078336484944367:F), (15053013456316196458870481299866861595818749671771356646798978105863499965417:F)] fun gate_27 => + halfRound_3_3 gate_27 vec![(7173615418515925804810790963571435428017065786053377450925733428353831789901:F), (8239211677777829016346247446855147819062679124993100113886842075069166957042:F), (15330855478780269194281285878526984092296288422420009233557393252489043181621:F)] fun gate_28 => + halfRound_3_3 gate_28 vec![(10014883178425964324400942419088813432808659204697623248101862794157084619079:F), (14014440630268834826103915635277409547403899966106389064645466381170788813506:F), (3580284508947993352601712737893796312152276667249521401778537893620670305946:F)] fun gate_29 => + halfRound_3_3 gate_29 vec![(2559754020964039399020874042785294258009596917335212876725104742182177996988:F), (14898657953331064524657146359621913343900897440154577299309964768812788279359:F), (2094037260225570753385567402013028115218264157081728958845544426054943497065:F)] fun gate_30 => + halfRound_3_3 gate_30 vec![(18051086536715129874440142649831636862614413764019212222493256578581754875930:F), (21680659279808524976004872421382255670910633119979692059689680820959727969489:F), (13950668739013333802529221454188102772764935019081479852094403697438884885176:F)] fun gate_31 => + halfRound_3_3 gate_31 vec![(9703845704528288130475698300068368924202959408694460208903346143576482802458:F), (12064310080154762977097567536495874701200266107682637369509532768346427148165:F), (16970760937630487134309762150133050221647250855182482010338640862111040175223:F)] fun gate_32 => + halfRound_3_3 gate_32 vec![(9790997389841527686594908620011261506072956332346095631818178387333642218087:F), (16314772317774781682315680698375079500119933343877658265473913556101283387175:F), (82044870826814863425230825851780076663078706675282523830353041968943811739:F)] fun gate_33 => + halfRound_3_3 gate_33 vec![(21696416499108261787701615667919260888528264686979598953977501999747075085778:F), (327771579314982889069767086599893095509690747425186236545716715062234528958:F), (4606746338794869835346679399457321301521448510419912225455957310754258695442:F)] fun gate_34 => + halfRound_3_3 gate_34 vec![(64499140292086295251085369317820027058256893294990556166497635237544139149:F), (10455028514626281809317431738697215395754892241565963900707779591201786416553:F), (10421411526406559029881814534127830959833724368842872558146891658647152404488:F)] fun gate_35 => + halfRound_3_3 gate_35 vec![(18848084335930758908929996602136129516563864917028006334090900573158639401697:F), (13844582069112758573505569452838731733665881813247931940917033313637916625267:F), (13488838454403536473492810836925746129625931018303120152441617863324950564617:F)] fun gate_36 => + halfRound_3_3 gate_36 vec![(15742141787658576773362201234656079648895020623294182888893044264221895077688:F), (6756884846734501741323584200608866954194124526254904154220230538416015199997:F), (7860026400080412708388991924996537435137213401947704476935669541906823414404:F)] fun gate_37 => + halfRound_3_3 gate_37 vec![(7871040688194276447149361970364037034145427598711982334898258974993423182255:F), (20758972836260983284101736686981180669442461217558708348216227791678564394086:F), (21723241881201839361054939276225528403036494340235482225557493179929400043949:F)] fun gate_38 => + halfRound_3_3 gate_38 vec![(19428469330241922173653014973246050805326196062205770999171646238586440011910:F), (7969200143746252148180468265998213908636952110398450526104077406933642389443:F), (10950417916542216146808986264475443189195561844878185034086477052349738113024:F)] fun gate_39 => + halfRound_3_3 gate_39 vec![(18149233917533571579549129116652755182249709970669448788972210488823719849654:F), (3729796741814967444466779622727009306670204996071028061336690366291718751463:F), (5172504399789702452458550583224415301790558941194337190035441508103183388987:F)] fun gate_40 => + halfRound_3_3 gate_40 vec![(6686473297578275808822003704722284278892335730899287687997898239052863590235:F), (19426913098142877404613120616123695099909113097119499573837343516470853338513:F), (5120337081764243150760446206763109494847464512045895114970710519826059751800:F)] fun gate_41 => + halfRound_3_3 gate_41 vec![(5055737465570446530938379301905385631528718027725177854815404507095601126720:F), (14235578612970484492268974539959119923625505766550088220840324058885914976980:F), (653592517890187950103239281291172267359747551606210609563961204572842639923:F)] fun gate_42 => + halfRound_3_3 gate_42 vec![(5507360526092411682502736946959369987101940689834541471605074817375175870579:F), (7864202866011437199771472205361912625244234597659755013419363091895334445453:F), (21294659996736305811805196472076519801392453844037698272479731199885739891648:F)] fun gate_43 => + halfRound_3_3 gate_43 vec![(13767183507040326119772335839274719411331242166231012705169069242737428254651:F), (810181532076738148308457416289197585577119693706380535394811298325092337781:F), (14232321930654703053193240133923161848171310212544136614525040874814292190478:F)] fun gate_44 => + halfRound_3_3 gate_44 vec![(16796904728299128263054838299534612533844352058851230375569421467352578781209:F), (16256310366973209550759123431979563367001604350120872788217761535379268327259:F), (19791658638819031543640174069980007021961272701723090073894685478509001321817:F)] fun gate_45 => + halfRound_3_3 gate_45 vec![(7046232469803978873754056165670086532908888046886780200907660308846356865119:F), (16001732848952745747636754668380555263330934909183814105655567108556497219752:F), (9737276123084413897604802930591512772593843242069849260396983774140735981896:F)] fun gate_46 => + halfRound_3_3 gate_46 vec![(11410895086919039954381533622971292904413121053792570364694836768885182251535:F), (19098362474249267294548762387533474746422711206129028436248281690105483603471:F), (11013788190750472643548844759298623898218957233582881400726340624764440203586:F)] fun gate_47 => + halfRound_3_3 gate_47 vec![(2206958256327295151076063922661677909471794458896944583339625762978736821035:F), (7171889270225471948987523104033632910444398328090760036609063776968837717795:F), (2510237900514902891152324520472140114359583819338640775472608119384714834368:F)] fun gate_48 => + halfRound_3_3 gate_48 vec![(8825275525296082671615660088137472022727508654813239986303576303490504107418:F), (1481125575303576470988538039195271612778457110700618040436600537924912146613:F), (16268684562967416784133317570130804847322980788316762518215429249893668424280:F)] fun gate_49 => + halfRound_3_3 gate_49 vec![(4681491452239189664806745521067158092729838954919425311759965958272644506354:F), (3131438137839074317765338377823608627360421824842227925080193892542578675835:F), (7930402370812046914611776451748034256998580373012248216998696754202474945793:F)] fun gate_50 => + halfRound_3_3 gate_50 vec![(8973151117361309058790078507956716669068786070949641445408234962176963060145:F), (10223139291409280771165469989652431067575076252562753663259473331031932716923:F), (2232089286698717316374057160056566551249777684520809735680538268209217819725:F)] fun gate_51 => + halfRound_3_3 gate_51 vec![(16930089744400890347392540468934821520000065594669279286854302439710657571308:F), (21739597952486540111798430281275997558482064077591840966152905690279247146674:F), (7508315029150148468008716674010060103310093296969466203204862163743615534994:F)] fun gate_52 => + halfRound_3_3 gate_52 vec![(11418894863682894988747041469969889669847284797234703818032750410328384432224:F), (10895338268862022698088163806301557188640023613155321294365781481663489837917:F), (18644184384117747990653304688839904082421784959872380449968500304556054962449:F)] fun gate_53 => + halfRound_3_3 gate_53 vec![(7414443845282852488299349772251184564170443662081877445177167932875038836497:F), (5391299369598751507276083947272874512197023231529277107201098701900193273851:F), (10329906873896253554985208009869159014028187242848161393978194008068001342262:F)] fun gate_54 => + halfRound_3_3 gate_54 vec![(4711719500416619550464783480084256452493890461073147512131129596065578741786:F), (11943219201565014805519989716407790139241726526989183705078747065985453201504:F), (4298705349772984837150885571712355513879480272326239023123910904259614053334:F)] fun gate_55 => + halfRound_3_3 gate_55 vec![(9999044003322463509208400801275356671266978396985433172455084837770460579627:F), (4908416131442887573991189028182614782884545304889259793974797565686968097291:F), (11963412684806827200577486696316210731159599844307091475104710684559519773777:F)] fun gate_56 => + halfRound_3_3 gate_56 vec![(20129916000261129180023520480843084814481184380399868943565043864970719708502:F), (12884788430473747619080473633364244616344003003135883061507342348586143092592:F), (20286808211545908191036106582330883564479538831989852602050135926112143921015:F)] fun gate_57 => + halfRound_3_3 gate_57 vec![(16282045180030846845043407450751207026423331632332114205316676731302016331498:F), (4332932669439410887701725251009073017227450696965904037736403407953448682093:F), (11105712698773407689561953778861118250080830258196150686012791790342360778288:F)] fun gate_58 => + halfRound_3_3 gate_58 vec![(21853934471586954540926699232107176721894655187276984175226220218852955976831:F), (9807888223112768841912392164376763820266226276821186661925633831143729724792:F), (13411808896854134882869416756427789378942943805153730705795307450368858622668:F)] fun gate_59 => + halfRound_3_3 gate_59 vec![(17906847067500673080192335286161014930416613104209700445088168479205894040011:F), (14554387648466176616800733804942239711702169161888492380425023505790070369632:F), (4264116751358967409634966292436919795665643055548061693088119780787376143967:F)] fun gate_60 => + fullRound_3_3 gate_60 vec![(2401104597023440271473786738539405349187326308074330930748109868990675625380:F), (12251645483867233248963286274239998200789646392205783056343767189806123148785:F), (15331181254680049984374210433775713530849624954688899814297733641575188164316:F)] fun gate_61 => + fullRound_3_3 gate_61 vec![(13108834590369183125338853868477110922788848506677889928217413952560148766472:F), (6843160824078397950058285123048455551935389277899379615286104657075620692224:F), (10151103286206275742153883485231683504642432930275602063393479013696349676320:F)] fun gate_62 => + fullRound_3_3 gate_62 vec![(7074320081443088514060123546121507442501369977071685257650287261047855962224:F), (11413928794424774638606755585641504971720734248726394295158115188173278890938:F), (7312756097842145322667451519888915975561412209738441762091369106604423801080:F)] fun gate_63 => + fullRound_3_3 gate_63 vec![(7181677521425162567568557182629489303281861794357882492140051324529826589361:F), (15123155547166304758320442783720138372005699143801247333941013553002921430306:F), (13409242754315411433193860530743374419854094495153957441316635981078068351329:F)] fun gate_64 => + k gate_64 def Poseidon2 (In1: F) (In2: F) (k: F -> Prop): Prop := - poseidon_3 vec![0, In1, In2] fun gate_0 => + poseidon_3 vec![(0:F), In1, In2] fun gate_0 => k gate_0[0] def mds_2 (Inp: Vector F 2) (k: Vector F 2 -> Prop): Prop := - ∃gate_0, gate_0 = Gates.mul Inp[0] 2910766817845651019878574839501801340070030115151021261302834310722729507541 ∧ - ∃gate_1, gate_1 = Gates.add 0 gate_0 ∧ - ∃gate_2, gate_2 = Gates.mul Inp[1] 19727366863391167538122140361473584127147630672623100827934084310230022599144 ∧ + ∃gate_0, gate_0 = Gates.mul Inp[0] (2910766817845651019878574839501801340070030115151021261302834310722729507541:F) ∧ + ∃gate_1, gate_1 = Gates.add (0:F) gate_0 ∧ + ∃gate_2, gate_2 = Gates.mul Inp[1] (19727366863391167538122140361473584127147630672623100827934084310230022599144:F) ∧ ∃gate_3, gate_3 = Gates.add gate_1 gate_2 ∧ - ∃gate_4, gate_4 = Gates.mul Inp[0] 5776684794125549462448597414050232243778680302179439492664047328281728356345 ∧ - ∃gate_5, gate_5 = Gates.add 0 gate_4 ∧ - ∃gate_6, gate_6 = Gates.mul Inp[1] 8348174920934122550483593999453880006756108121341067172388445916328941978568 ∧ + ∃gate_4, gate_4 = Gates.mul Inp[0] (5776684794125549462448597414050232243778680302179439492664047328281728356345:F) ∧ + ∃gate_5, gate_5 = Gates.add (0:F) gate_4 ∧ + ∃gate_6, gate_6 = Gates.mul Inp[1] (8348174920934122550483593999453880006756108121341067172388445916328941978568:F) ∧ ∃gate_7, gate_7 = Gates.add gate_5 gate_6 ∧ k vec![gate_3, gate_7] @@ -141,84 +143,84 @@ def fullRound_2_2 (Inp: Vector F 2) (Consts: Vector F 2) (k: Vector F 2 -> Prop) sbox gate_0 fun gate_2 => sbox gate_1 fun gate_3 => mds_2 vec![gate_2, gate_3] fun gate_4 => - k vec![gate_4[0], gate_4[1]] + k gate_4 def halfRound_2_2 (Inp: Vector F 2) (Consts: Vector F 2) (k: Vector F 2 -> Prop): Prop := ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧ ∃gate_1, gate_1 = Gates.add Inp[1] Consts[1] ∧ sbox gate_0 fun gate_2 => mds_2 vec![gate_2, gate_1] fun gate_3 => - k vec![gate_3[0], gate_3[1]] + k gate_3 def poseidon_2 (Inputs: Vector F 2) (k: Vector F 2 -> Prop): Prop := - fullRound_2_2 vec![Inputs[0], Inputs[1]] vec![4417881134626180770308697923359573201005643519861877412381846989312604493735, 5433650512959517612316327474713065966758808864213826738576266661723522780033] fun gate_0 => - fullRound_2_2 vec![gate_0[0], gate_0[1]] vec![13641176377184356099764086973022553863760045607496549923679278773208775739952, 17949713444224994136330421782109149544629237834775211751417461773584374506783] fun gate_1 => - fullRound_2_2 vec![gate_1[0], gate_1[1]] vec![13765628375339178273710281891027109699578766420463125835325926111705201856003, 19179513468172002314585757290678967643352171735526887944518845346318719730387] fun gate_2 => - fullRound_2_2 vec![gate_2[0], gate_2[1]] vec![5157412437176756884543472904098424903141745259452875378101256928559722612176, 535160875740282236955320458485730000677124519901643397458212725410971557409] fun gate_3 => - halfRound_2_2 vec![gate_3[0], gate_3[1]] vec![1050793453380762984940163090920066886770841063557081906093018330633089036729, 10665495010329663932664894101216428400933984666065399374198502106997623173873] fun gate_4 => - halfRound_2_2 vec![gate_4[0], gate_4[1]] vec![19965634623406616956648724894636666805991993496469370618546874926025059150737, 13007250030070838431593222885902415182312449212965120303174723305710127422213] fun gate_5 => - halfRound_2_2 vec![gate_5[0], gate_5[1]] vec![16877538715074991604507979123743768693428157847423939051086744213162455276374, 18211747749504876135588847560312685184956239426147543810126553367063157141465] fun gate_6 => - halfRound_2_2 vec![gate_6[0], gate_6[1]] vec![18151553319826126919739798892854572062191241985315767086020821632812331245635, 19957033149976712666746140949846950406660099037474791840946955175819555930825] fun gate_7 => - halfRound_2_2 vec![gate_7[0], gate_7[1]] vec![3469514863538261843186854830917934449567467100548474599735384052339577040841, 989698510043911779243192466312362856042600749099921773896924315611668507708] fun gate_8 => - halfRound_2_2 vec![gate_8[0], gate_8[1]] vec![12568377015646290945235387813564567111330046038050864455358059568128000172201, 20856104135605479600325529349246932565148587186338606236677138505306779314172] fun gate_9 => - halfRound_2_2 vec![gate_9[0], gate_9[1]] vec![8206918720503535523121349917159924938835810381723474192155637697065780938424, 1309058477013932989380617265069188723120054926187607548493110334522527703566] fun gate_10 => - halfRound_2_2 vec![gate_10[0], gate_10[1]] vec![14076116939332667074621703729512195584105250395163383769419390236426287710606, 10153498892749751942204288991871286290442690932856658983589258153608012428674] fun gate_11 => - halfRound_2_2 vec![gate_11[0], gate_11[1]] vec![18202499207234128286137597834010475797175973146805180988367589376893530181575, 12739388830157083522877690211447248168864006284243907142044329113461613743052] fun gate_12 => - halfRound_2_2 vec![gate_12[0], gate_12[1]] vec![15123358710467780770838026754240340042441262572309759635224051333176022613949, 19925004701844594370904593774447343836015483888496504201331110250494635362184] fun gate_13 => - halfRound_2_2 vec![gate_13[0], gate_13[1]] vec![10352416606816998476681131583320899030072315953910679608943150613208329645891, 10567371822366244361703342347428230537114808440249611395507235283708966113221] fun gate_14 => - halfRound_2_2 vec![gate_14[0], gate_14[1]] vec![5635498582763880627392290206431559361272660937399944184533035305989295959602, 11866432933224219174041051738704352719163271639958083608224676028593315904909] fun gate_15 => - halfRound_2_2 vec![gate_15[0], gate_15[1]] vec![5795020705294401441272215064554385591292330721703923167136157291459784140431, 9482202378699252817564375087302794636287866584767523335624368774856230692758] fun gate_16 => - halfRound_2_2 vec![gate_16[0], gate_16[1]] vec![4245237636894546151746468406560945873445548423466753843402086544922216329298, 12000500941313982757584712677991730019124834399479314697467598397927435905133] fun gate_17 => - halfRound_2_2 vec![gate_17[0], gate_17[1]] vec![7596790274058425558167520209857956363736666939016807569082239187494363541787, 2484867918246116343205467273440098378820186751202461278013576281097918148877] fun gate_18 => - halfRound_2_2 vec![gate_18[0], gate_18[1]] vec![18312645949449997391810445935615409295369169383463185688973803378104013950190, 15320686572748723004980855263301182130424010735782762814513954166519592552733] fun gate_19 => - halfRound_2_2 vec![gate_19[0], gate_19[1]] vec![12618438900597948888520621062416758747872180395546164387827245287017031303859, 17438141672027706116733201008397064011774368832458707512367404736905021019585] fun gate_20 => - halfRound_2_2 vec![gate_20[0], gate_20[1]] vec![6374197807230665998865688675365359100400438034755781666913068586172586548950, 2189398913433273865510950346186699930188746169476472274335177556702504595264] fun gate_21 => - halfRound_2_2 vec![gate_21[0], gate_21[1]] vec![6268495580028970231803791523870131137294646402347399003576649137450213034606, 17896250365994900261202920044129628104272791547990619503076839618914047059275] fun gate_22 => - halfRound_2_2 vec![gate_22[0], gate_22[1]] vec![13692156312448722528008862371944543449350293305158722920787736248435893008873, 15234446864368744483209945022439268713300180233589581910497691316744177619376] fun gate_23 => - halfRound_2_2 vec![gate_23[0], gate_23[1]] vec![1572426502623310766593681563281600503979671244997798691029595521622402217227, 80103447810215150918585162168214870083573048458555897999822831203653996617] fun gate_24 => - halfRound_2_2 vec![gate_24[0], gate_24[1]] vec![8228820324013669567851850635126713973797711779951230446503353812192849106342, 5375851433746509614045812476958526065449377558695752132494533666370449415873] fun gate_25 => - halfRound_2_2 vec![gate_25[0], gate_25[1]] vec![12115998939203497346386774317892338270561208357481805380546938146796257365018, 9764067909645821279940531410531154041386008396840887338272986634350423466622] fun gate_26 => - halfRound_2_2 vec![gate_26[0], gate_26[1]] vec![8538708244538850542384936174629541085495830544298260335345008245230827876882, 7140127896620013355910287215441004676619168261422440177712039790284719613114] fun gate_27 => - halfRound_2_2 vec![gate_27[0], gate_27[1]] vec![14297402962228458726038826185823085337698917275385741292940049024977027409762, 6667115556431351074165934212337261254608231545257434281887966406956835140819] fun gate_28 => - halfRound_2_2 vec![gate_28[0], gate_28[1]] vec![20226761165244293291042617464655196752671169026542832236139342122602741090001, 12038289506489256655759141386763477208196694421666339040483042079632134429119] fun gate_29 => - halfRound_2_2 vec![gate_29[0], gate_29[1]] vec![19027757334170818571203982241812412991528769934917288000224335655934473717551, 16272152964456553579565580463468069884359929612321610357528838696790370074720] fun gate_30 => - halfRound_2_2 vec![gate_30[0], gate_30[1]] vec![2500392889689246014710135696485946334448570271481948765283016105301740284071, 8595254970528530312401637448610398388203855633951264114100575485022581946023] fun gate_31 => - halfRound_2_2 vec![gate_31[0], gate_31[1]] vec![11635945688914011450976408058407206367914559009113158286982919675551688078198, 614739068603482619581328040478536306925147663946742687395148680260956671871] fun gate_32 => - halfRound_2_2 vec![gate_32[0], gate_32[1]] vec![18692271780377861570175282183255720350972693125537599213951106550953176268753, 4987059230784976306647166378298632695585915319042844495357753339378260807164] fun gate_33 => - halfRound_2_2 vec![gate_33[0], gate_33[1]] vec![21851403978498723616722415377430107676258664746210815234490134600998983955497, 9830635451186415300891533983087800047564037813328875992115573428596207326204] fun gate_34 => - halfRound_2_2 vec![gate_34[0], gate_34[1]] vec![4842706106434537116860242620706030229206345167233200482994958847436425185478, 6422235064906823218421386871122109085799298052314922856340127798647926126490] fun gate_35 => - halfRound_2_2 vec![gate_35[0], gate_35[1]] vec![4564364104986856861943331689105797031330091877115997069096365671501473357846, 1944043894089780613038197112872830569538541856657037469098448708685350671343] fun gate_36 => - halfRound_2_2 vec![gate_36[0], gate_36[1]] vec![21179865974855950600518216085229498748425990426231530451599322283119880194955, 14296697761894107574369608843560006996183955751502547883167824879840894933162] fun gate_37 => - halfRound_2_2 vec![gate_37[0], gate_37[1]] vec![12274619649702218570450581712439138337725246879938860735460378251639845671898, 16371396450276899401411886674029075408418848209575273031725505038938314070356] fun gate_38 => - halfRound_2_2 vec![gate_38[0], gate_38[1]] vec![3702561221750983937578095019779188631407216522704543451228773892695044653565, 19721616877735564664624984774636557499099875603996426215495516594530838681980] fun gate_39 => - halfRound_2_2 vec![gate_39[0], gate_39[1]] vec![6383350109027696789969911008057747025018308755462287526819231672217685282429, 20860583956177367265984596617324237471765572961978977333122281041544719622905] fun gate_40 => - halfRound_2_2 vec![gate_40[0], gate_40[1]] vec![5766390934595026947545001478457407504285452477687752470140790011329357286275, 4043175758319898049344746138515323336207420888499903387536875603879441092484] fun gate_41 => - halfRound_2_2 vec![gate_41[0], gate_41[1]] vec![15579382179133608217098622223834161692266188678101563820988612253342538956534, 1864640783252634743892105383926602930909039567065240010338908865509831749824] fun gate_42 => - halfRound_2_2 vec![gate_42[0], gate_42[1]] vec![15943719865023133586707144161652035291705809358178262514871056013754142625673, 2326415993032390211558498780803238091925402878871059708106213703504162832999] fun gate_43 => - halfRound_2_2 vec![gate_43[0], gate_43[1]] vec![19995326402773833553207196590622808505547443523750970375738981396588337910289, 5143583711361588952673350526320181330406047695593201009385718506918735286622] fun gate_44 => - halfRound_2_2 vec![gate_44[0], gate_44[1]] vec![15436006486881920976813738625999473183944244531070780793506388892313517319583, 16660446760173633166698660166238066533278664023818938868110282615200613695857] fun gate_45 => - halfRound_2_2 vec![gate_45[0], gate_45[1]] vec![4966065365695755376133119391352131079892396024584848298231004326013366253934, 20683781957411705574951987677641476019618457561419278856689645563561076926702] fun gate_46 => - halfRound_2_2 vec![gate_46[0], gate_46[1]] vec![17280836839165902792086432296371645107551519324565649849400948918605456875699, 17045635513701208892073056357048619435743564064921155892004135325530808465371] fun gate_47 => - halfRound_2_2 vec![gate_47[0], gate_47[1]] vec![17055032967194400710390142791334572297458033582458169295920670679093585707295, 15727174639569115300068198908071514334002742825679221638729902577962862163505] fun gate_48 => - halfRound_2_2 vec![gate_48[0], gate_48[1]] vec![1001755657610446661315902885492677747789366510875120894840818704741370398633, 18638547332826171619311285502376343504539399518545103511265465604926625041234] fun gate_49 => - halfRound_2_2 vec![gate_49[0], gate_49[1]] vec![6751954224763196429755298529194402870632445298969935050224267844020826420799, 3526747115904224771452549517614107688674036840088422555827581348280834879405] fun gate_50 => - halfRound_2_2 vec![gate_50[0], gate_50[1]] vec![15705897908180497062880001271426561999724005008972544196300715293701537574122, 574386695213920937259007343820417029802510752426579750428758189312416867750] fun gate_51 => - halfRound_2_2 vec![gate_51[0], gate_51[1]] vec![15973040855000600860816974646787367136127946402908768408978806375685439868553, 20934130413948796333037139460875996342810005558806621330680156931816867321122] fun gate_52 => - halfRound_2_2 vec![gate_52[0], gate_52[1]] vec![6918585327145564636398173845411579411526758237572034236476079610890705810764, 14158163500813182062258176233162498241310167509137716527054939926126453647182] fun gate_53 => - halfRound_2_2 vec![gate_53[0], gate_53[1]] vec![4164602626597695668474100217150111342272610479949122406544277384862187287433, 12146526846507496913615390662823936206892812880963914267275606265272996025304] fun gate_54 => - halfRound_2_2 vec![gate_54[0], gate_54[1]] vec![10153527926900017763244212043512822363696541810586522108597162891799345289938, 13564663485965299104296214940873270349072051793008946663855767889066202733588] fun gate_55 => - halfRound_2_2 vec![gate_55[0], gate_55[1]] vec![5612449256997576125867742696783020582952387615430650198777254717398552960096, 12151885480032032868507892738683067544172874895736290365318623681886999930120] fun gate_56 => - halfRound_2_2 vec![gate_56[0], gate_56[1]] vec![380452237704664384810613424095477896605414037288009963200982915188629772177, 9067557551252570188533509616805287919563636482030947363841198066124642069518] fun gate_57 => - halfRound_2_2 vec![gate_57[0], gate_57[1]] vec![21280306817619711661335268484199763923870315733198162896599997188206277056900, 5567165819557297006750252582140767993422097822227408837378089569369734876257] fun gate_58 => - halfRound_2_2 vec![gate_58[0], gate_58[1]] vec![10411936321072105429908396649383171465939606386380071222095155850987201580137, 21338390051413922944780864872652000187403217966653363270851298678606449622266] fun gate_59 => - fullRound_2_2 vec![gate_59[0], gate_59[1]] vec![12156296560457833712186127325312904760045212412680904475497938949653569234473, 4271647814574748734312113971565139132510281260328947438246615707172526380757] fun gate_60 => - fullRound_2_2 vec![gate_60[0], gate_60[1]] vec![9061738206062369647211128232833114177054715885442782773131292534862178874950, 10134551893627587797380445583959894183158393780166496661696555422178052339133] fun gate_61 => - fullRound_2_2 vec![gate_61[0], gate_61[1]] vec![8932270237664043612366044102088319242789325050842783721780970129656616386103, 3339412934966886386194449782756711637636784424032779155216609410591712750636] fun gate_62 => - fullRound_2_2 vec![gate_62[0], gate_62[1]] vec![9704903972004596791086522314847373103670545861209569267884026709445485704400, 17467570179597572575614276429760169990940929887711661192333523245667228809456] fun gate_63 => - k vec![gate_63[0], gate_63[1]] + fullRound_2_2 Inputs vec![(4417881134626180770308697923359573201005643519861877412381846989312604493735:F), (5433650512959517612316327474713065966758808864213826738576266661723522780033:F)] fun gate_0 => + fullRound_2_2 gate_0 vec![(13641176377184356099764086973022553863760045607496549923679278773208775739952:F), (17949713444224994136330421782109149544629237834775211751417461773584374506783:F)] fun gate_1 => + fullRound_2_2 gate_1 vec![(13765628375339178273710281891027109699578766420463125835325926111705201856003:F), (19179513468172002314585757290678967643352171735526887944518845346318719730387:F)] fun gate_2 => + fullRound_2_2 gate_2 vec![(5157412437176756884543472904098424903141745259452875378101256928559722612176:F), (535160875740282236955320458485730000677124519901643397458212725410971557409:F)] fun gate_3 => + halfRound_2_2 gate_3 vec![(1050793453380762984940163090920066886770841063557081906093018330633089036729:F), (10665495010329663932664894101216428400933984666065399374198502106997623173873:F)] fun gate_4 => + halfRound_2_2 gate_4 vec![(19965634623406616956648724894636666805991993496469370618546874926025059150737:F), (13007250030070838431593222885902415182312449212965120303174723305710127422213:F)] fun gate_5 => + halfRound_2_2 gate_5 vec![(16877538715074991604507979123743768693428157847423939051086744213162455276374:F), (18211747749504876135588847560312685184956239426147543810126553367063157141465:F)] fun gate_6 => + halfRound_2_2 gate_6 vec![(18151553319826126919739798892854572062191241985315767086020821632812331245635:F), (19957033149976712666746140949846950406660099037474791840946955175819555930825:F)] fun gate_7 => + halfRound_2_2 gate_7 vec![(3469514863538261843186854830917934449567467100548474599735384052339577040841:F), (989698510043911779243192466312362856042600749099921773896924315611668507708:F)] fun gate_8 => + halfRound_2_2 gate_8 vec![(12568377015646290945235387813564567111330046038050864455358059568128000172201:F), (20856104135605479600325529349246932565148587186338606236677138505306779314172:F)] fun gate_9 => + halfRound_2_2 gate_9 vec![(8206918720503535523121349917159924938835810381723474192155637697065780938424:F), (1309058477013932989380617265069188723120054926187607548493110334522527703566:F)] fun gate_10 => + halfRound_2_2 gate_10 vec![(14076116939332667074621703729512195584105250395163383769419390236426287710606:F), (10153498892749751942204288991871286290442690932856658983589258153608012428674:F)] fun gate_11 => + halfRound_2_2 gate_11 vec![(18202499207234128286137597834010475797175973146805180988367589376893530181575:F), (12739388830157083522877690211447248168864006284243907142044329113461613743052:F)] fun gate_12 => + halfRound_2_2 gate_12 vec![(15123358710467780770838026754240340042441262572309759635224051333176022613949:F), (19925004701844594370904593774447343836015483888496504201331110250494635362184:F)] fun gate_13 => + halfRound_2_2 gate_13 vec![(10352416606816998476681131583320899030072315953910679608943150613208329645891:F), (10567371822366244361703342347428230537114808440249611395507235283708966113221:F)] fun gate_14 => + halfRound_2_2 gate_14 vec![(5635498582763880627392290206431559361272660937399944184533035305989295959602:F), (11866432933224219174041051738704352719163271639958083608224676028593315904909:F)] fun gate_15 => + halfRound_2_2 gate_15 vec![(5795020705294401441272215064554385591292330721703923167136157291459784140431:F), (9482202378699252817564375087302794636287866584767523335624368774856230692758:F)] fun gate_16 => + halfRound_2_2 gate_16 vec![(4245237636894546151746468406560945873445548423466753843402086544922216329298:F), (12000500941313982757584712677991730019124834399479314697467598397927435905133:F)] fun gate_17 => + halfRound_2_2 gate_17 vec![(7596790274058425558167520209857956363736666939016807569082239187494363541787:F), (2484867918246116343205467273440098378820186751202461278013576281097918148877:F)] fun gate_18 => + halfRound_2_2 gate_18 vec![(18312645949449997391810445935615409295369169383463185688973803378104013950190:F), (15320686572748723004980855263301182130424010735782762814513954166519592552733:F)] fun gate_19 => + halfRound_2_2 gate_19 vec![(12618438900597948888520621062416758747872180395546164387827245287017031303859:F), (17438141672027706116733201008397064011774368832458707512367404736905021019585:F)] fun gate_20 => + halfRound_2_2 gate_20 vec![(6374197807230665998865688675365359100400438034755781666913068586172586548950:F), (2189398913433273865510950346186699930188746169476472274335177556702504595264:F)] fun gate_21 => + halfRound_2_2 gate_21 vec![(6268495580028970231803791523870131137294646402347399003576649137450213034606:F), (17896250365994900261202920044129628104272791547990619503076839618914047059275:F)] fun gate_22 => + halfRound_2_2 gate_22 vec![(13692156312448722528008862371944543449350293305158722920787736248435893008873:F), (15234446864368744483209945022439268713300180233589581910497691316744177619376:F)] fun gate_23 => + halfRound_2_2 gate_23 vec![(1572426502623310766593681563281600503979671244997798691029595521622402217227:F), (80103447810215150918585162168214870083573048458555897999822831203653996617:F)] fun gate_24 => + halfRound_2_2 gate_24 vec![(8228820324013669567851850635126713973797711779951230446503353812192849106342:F), (5375851433746509614045812476958526065449377558695752132494533666370449415873:F)] fun gate_25 => + halfRound_2_2 gate_25 vec![(12115998939203497346386774317892338270561208357481805380546938146796257365018:F), (9764067909645821279940531410531154041386008396840887338272986634350423466622:F)] fun gate_26 => + halfRound_2_2 gate_26 vec![(8538708244538850542384936174629541085495830544298260335345008245230827876882:F), (7140127896620013355910287215441004676619168261422440177712039790284719613114:F)] fun gate_27 => + halfRound_2_2 gate_27 vec![(14297402962228458726038826185823085337698917275385741292940049024977027409762:F), (6667115556431351074165934212337261254608231545257434281887966406956835140819:F)] fun gate_28 => + halfRound_2_2 gate_28 vec![(20226761165244293291042617464655196752671169026542832236139342122602741090001:F), (12038289506489256655759141386763477208196694421666339040483042079632134429119:F)] fun gate_29 => + halfRound_2_2 gate_29 vec![(19027757334170818571203982241812412991528769934917288000224335655934473717551:F), (16272152964456553579565580463468069884359929612321610357528838696790370074720:F)] fun gate_30 => + halfRound_2_2 gate_30 vec![(2500392889689246014710135696485946334448570271481948765283016105301740284071:F), (8595254970528530312401637448610398388203855633951264114100575485022581946023:F)] fun gate_31 => + halfRound_2_2 gate_31 vec![(11635945688914011450976408058407206367914559009113158286982919675551688078198:F), (614739068603482619581328040478536306925147663946742687395148680260956671871:F)] fun gate_32 => + halfRound_2_2 gate_32 vec![(18692271780377861570175282183255720350972693125537599213951106550953176268753:F), (4987059230784976306647166378298632695585915319042844495357753339378260807164:F)] fun gate_33 => + halfRound_2_2 gate_33 vec![(21851403978498723616722415377430107676258664746210815234490134600998983955497:F), (9830635451186415300891533983087800047564037813328875992115573428596207326204:F)] fun gate_34 => + halfRound_2_2 gate_34 vec![(4842706106434537116860242620706030229206345167233200482994958847436425185478:F), (6422235064906823218421386871122109085799298052314922856340127798647926126490:F)] fun gate_35 => + halfRound_2_2 gate_35 vec![(4564364104986856861943331689105797031330091877115997069096365671501473357846:F), (1944043894089780613038197112872830569538541856657037469098448708685350671343:F)] fun gate_36 => + halfRound_2_2 gate_36 vec![(21179865974855950600518216085229498748425990426231530451599322283119880194955:F), (14296697761894107574369608843560006996183955751502547883167824879840894933162:F)] fun gate_37 => + halfRound_2_2 gate_37 vec![(12274619649702218570450581712439138337725246879938860735460378251639845671898:F), (16371396450276899401411886674029075408418848209575273031725505038938314070356:F)] fun gate_38 => + halfRound_2_2 gate_38 vec![(3702561221750983937578095019779188631407216522704543451228773892695044653565:F), (19721616877735564664624984774636557499099875603996426215495516594530838681980:F)] fun gate_39 => + halfRound_2_2 gate_39 vec![(6383350109027696789969911008057747025018308755462287526819231672217685282429:F), (20860583956177367265984596617324237471765572961978977333122281041544719622905:F)] fun gate_40 => + halfRound_2_2 gate_40 vec![(5766390934595026947545001478457407504285452477687752470140790011329357286275:F), (4043175758319898049344746138515323336207420888499903387536875603879441092484:F)] fun gate_41 => + halfRound_2_2 gate_41 vec![(15579382179133608217098622223834161692266188678101563820988612253342538956534:F), (1864640783252634743892105383926602930909039567065240010338908865509831749824:F)] fun gate_42 => + halfRound_2_2 gate_42 vec![(15943719865023133586707144161652035291705809358178262514871056013754142625673:F), (2326415993032390211558498780803238091925402878871059708106213703504162832999:F)] fun gate_43 => + halfRound_2_2 gate_43 vec![(19995326402773833553207196590622808505547443523750970375738981396588337910289:F), (5143583711361588952673350526320181330406047695593201009385718506918735286622:F)] fun gate_44 => + halfRound_2_2 gate_44 vec![(15436006486881920976813738625999473183944244531070780793506388892313517319583:F), (16660446760173633166698660166238066533278664023818938868110282615200613695857:F)] fun gate_45 => + halfRound_2_2 gate_45 vec![(4966065365695755376133119391352131079892396024584848298231004326013366253934:F), (20683781957411705574951987677641476019618457561419278856689645563561076926702:F)] fun gate_46 => + halfRound_2_2 gate_46 vec![(17280836839165902792086432296371645107551519324565649849400948918605456875699:F), (17045635513701208892073056357048619435743564064921155892004135325530808465371:F)] fun gate_47 => + halfRound_2_2 gate_47 vec![(17055032967194400710390142791334572297458033582458169295920670679093585707295:F), (15727174639569115300068198908071514334002742825679221638729902577962862163505:F)] fun gate_48 => + halfRound_2_2 gate_48 vec![(1001755657610446661315902885492677747789366510875120894840818704741370398633:F), (18638547332826171619311285502376343504539399518545103511265465604926625041234:F)] fun gate_49 => + halfRound_2_2 gate_49 vec![(6751954224763196429755298529194402870632445298969935050224267844020826420799:F), (3526747115904224771452549517614107688674036840088422555827581348280834879405:F)] fun gate_50 => + halfRound_2_2 gate_50 vec![(15705897908180497062880001271426561999724005008972544196300715293701537574122:F), (574386695213920937259007343820417029802510752426579750428758189312416867750:F)] fun gate_51 => + halfRound_2_2 gate_51 vec![(15973040855000600860816974646787367136127946402908768408978806375685439868553:F), (20934130413948796333037139460875996342810005558806621330680156931816867321122:F)] fun gate_52 => + halfRound_2_2 gate_52 vec![(6918585327145564636398173845411579411526758237572034236476079610890705810764:F), (14158163500813182062258176233162498241310167509137716527054939926126453647182:F)] fun gate_53 => + halfRound_2_2 gate_53 vec![(4164602626597695668474100217150111342272610479949122406544277384862187287433:F), (12146526846507496913615390662823936206892812880963914267275606265272996025304:F)] fun gate_54 => + halfRound_2_2 gate_54 vec![(10153527926900017763244212043512822363696541810586522108597162891799345289938:F), (13564663485965299104296214940873270349072051793008946663855767889066202733588:F)] fun gate_55 => + halfRound_2_2 gate_55 vec![(5612449256997576125867742696783020582952387615430650198777254717398552960096:F), (12151885480032032868507892738683067544172874895736290365318623681886999930120:F)] fun gate_56 => + halfRound_2_2 gate_56 vec![(380452237704664384810613424095477896605414037288009963200982915188629772177:F), (9067557551252570188533509616805287919563636482030947363841198066124642069518:F)] fun gate_57 => + halfRound_2_2 gate_57 vec![(21280306817619711661335268484199763923870315733198162896599997188206277056900:F), (5567165819557297006750252582140767993422097822227408837378089569369734876257:F)] fun gate_58 => + halfRound_2_2 gate_58 vec![(10411936321072105429908396649383171465939606386380071222095155850987201580137:F), (21338390051413922944780864872652000187403217966653363270851298678606449622266:F)] fun gate_59 => + fullRound_2_2 gate_59 vec![(12156296560457833712186127325312904760045212412680904475497938949653569234473:F), (4271647814574748734312113971565139132510281260328947438246615707172526380757:F)] fun gate_60 => + fullRound_2_2 gate_60 vec![(9061738206062369647211128232833114177054715885442782773131292534862178874950:F), (10134551893627587797380445583959894183158393780166496661696555422178052339133:F)] fun gate_61 => + fullRound_2_2 gate_61 vec![(8932270237664043612366044102088319242789325050842783721780970129656616386103:F), (3339412934966886386194449782756711637636784424032779155216609410591712750636:F)] fun gate_62 => + fullRound_2_2 gate_62 vec![(9704903972004596791086522314847373103670545861209569267884026709445485704400:F), (17467570179597572575614276429760169990940929887711661192333523245667228809456:F)] fun gate_63 => + k gate_63 def Poseidon1 (In: F) (k: F -> Prop): Prop := - poseidon_2 vec![0, In] fun gate_0 => + poseidon_2 vec![(0:F), In] fun gate_0 => k gate_0[0] def MerkleTreeRecoverRound (Direction: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop := @@ -256,7 +258,7 @@ def circuit (IdentityNullifier: F) (IdentityTrapdoor: F) (TreePathIndices: Vecto Poseidon1 gate_0 fun gate_1 => Poseidon2 ExternalNullifier IdentityNullifier fun gate_2 => Gates.eq gate_2 NullifierHash ∧ - MerkleTreeInclusionProof_20_20 gate_1 vec![TreePathIndices[0], TreePathIndices[1], TreePathIndices[2], TreePathIndices[3], TreePathIndices[4], TreePathIndices[5], TreePathIndices[6], TreePathIndices[7], TreePathIndices[8], TreePathIndices[9], TreePathIndices[10], TreePathIndices[11], TreePathIndices[12], TreePathIndices[13], TreePathIndices[14], TreePathIndices[15], TreePathIndices[16], TreePathIndices[17], TreePathIndices[18], TreePathIndices[19]] vec![TreeSiblings[0], TreeSiblings[1], TreeSiblings[2], TreeSiblings[3], TreeSiblings[4], TreeSiblings[5], TreeSiblings[6], TreeSiblings[7], TreeSiblings[8], TreeSiblings[9], TreeSiblings[10], TreeSiblings[11], TreeSiblings[12], TreeSiblings[13], TreeSiblings[14], TreeSiblings[15], TreeSiblings[16], TreeSiblings[17], TreeSiblings[18], TreeSiblings[19]] fun gate_4 => + MerkleTreeInclusionProof_20_20 gate_1 TreePathIndices TreeSiblings fun gate_4 => Gates.eq gate_4 MTRoot ∧ ∃_ignored_, _ignored_ = Gates.mul SignalHash SignalHash ∧ True diff --git a/lean-circuit/LeanCircuit/Common.lean b/lean-circuit/LeanCircuit/Common.lean new file mode 100644 index 0000000..d2a521f --- /dev/null +++ b/lean-circuit/LeanCircuit/Common.lean @@ -0,0 +1,11 @@ +import LeanCircuit +import ProvenZk.Binary +import ProvenZk.Hash +import ProvenZk.Merkle +import ProvenZk.Ext.Vector + +def Bn256_Fr : Nat := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 +axiom bn256_Fr_prime : Nat.Prime Bn256_Fr +instance : Fact (Nat.Prime Semaphore.Order) := Fact.mk (by apply bn256_Fr_prime) + +abbrev D := 20 diff --git a/lean-circuit/LeanCircuit/Poseidon.lean b/lean-circuit/LeanCircuit/Poseidon.lean new file mode 100644 index 0000000..35c9736 --- /dev/null +++ b/lean-circuit/LeanCircuit/Poseidon.lean @@ -0,0 +1,74 @@ +import LeanCircuit +import LeanCircuit.Common +import Mathlib +import ProvenZk + +open Semaphore (F Order) + +instance : Fact (Nat.Prime Semaphore.Order) := Fact.mk (by apply bn256_Fr_prime) + +def sbox_uniqueAssignment (Inp : F): UniqueAssignment (Semaphore.sbox Inp) id := UniqueAssignment.mk _ $ by + simp [Semaphore.sbox]; tauto + +/- + Poseidon Hash with 2 arguments +-/ + +def mds_3_uniqueAssignment (S : Vector F 3): UniqueAssignment (Semaphore.mds_3 S) id := UniqueAssignment.mk _ $ by + simp [Semaphore.mds_3]; tauto + +def fullRound_3_3_uniqueAssignment (S C : Vector F 3): UniqueAssignment (Semaphore.fullRound_3_3 S C) id := UniqueAssignment.mk _ $ by + simp [Semaphore.fullRound_3_3, (sbox_uniqueAssignment _).equiv, (mds_3_uniqueAssignment _).equiv]; tauto + +def halfRound_3_3_uniqueAssignment (S C : Vector F 3): UniqueAssignment (Semaphore.halfRound_3_3 S C) id := UniqueAssignment.mk _ $ by + simp [Semaphore.halfRound_3_3, (sbox_uniqueAssignment _).equiv, (mds_3_uniqueAssignment _).equiv]; tauto + +def poseidon_3_uniqueAssignment (inp : Vector F 3): UniqueAssignment (Semaphore.poseidon_3 inp) id := by + unfold Semaphore.poseidon_3 + repeat ( + apply UniqueAssignment.compose + . (first | apply fullRound_3_3_uniqueAssignment | apply halfRound_3_3_uniqueAssignment) + intro _ + ) + apply UniqueAssignment.constant + +theorem poseidon_3_testVector : (poseidon_3_uniqueAssignment (vec![0,1,2])).val = vec![0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a, 0x0fca49b798923ab0239de1c9e7a4a9a2210312b6a2f616d18b5a87f9b628ae29, 0x0e7ae82e40091e63cbd4f16a6d16310b3729d4b6e138fcf54110e2867045a30c] := + by native_decide + +def poseidon₂ : Hash F 2 := fun a => (poseidon_3_uniqueAssignment vec![0, a.get 0, a.get 1]).val.get 0 + +lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : Semaphore.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by + unfold Semaphore.Poseidon2 poseidon₂ + apply Iff.of_eq + rw [(poseidon_3_uniqueAssignment _).equiv] + congr + +/- + Poseidon Hash with 1 argument +-/ + +def mds_2_uniqueAssignment (S : Vector F 2): UniqueAssignment (Semaphore.mds_2 S) id := UniqueAssignment.mk _ $ by + simp [Semaphore.mds_2]; tauto + +def fullRound_2_2_uniqueAssignment (S C : Vector F 2): UniqueAssignment (Semaphore.fullRound_2_2 S C) id := UniqueAssignment.mk _ $ by + simp [Semaphore.fullRound_2_2, (sbox_uniqueAssignment _).equiv, (mds_2_uniqueAssignment _).equiv]; tauto + +def halfRound_2_2_uniqueAssignment (S C : Vector F 2): UniqueAssignment (Semaphore.halfRound_2_2 S C) id := UniqueAssignment.mk _ $ by + simp [Semaphore.halfRound_2_2, (sbox_uniqueAssignment _).equiv, (mds_2_uniqueAssignment _).equiv]; tauto + +def poseidon_2_uniqueAssignment (inp : Vector F 2): UniqueAssignment (Semaphore.poseidon_2 inp) id := by + unfold Semaphore.poseidon_2 + repeat ( + apply UniqueAssignment.compose + . (first | apply fullRound_2_2_uniqueAssignment | apply halfRound_2_2_uniqueAssignment) + intro _ + ) + apply UniqueAssignment.constant + +def poseidon₁ : Hash F 1 := fun a => (poseidon_2_uniqueAssignment vec![0, a.get 0]).val.get 0 + +lemma Poseidon1_uncps (a : F) (k : F -> Prop) : Semaphore.Poseidon1 a k ↔ k (poseidon₁ vec![a]) := by + unfold Semaphore.Poseidon1 poseidon₁ + apply Iff.of_eq + rw [(poseidon_2_uniqueAssignment _).equiv] + congr diff --git a/lean-circuit/LeanCircuit/Poseidon/Constants.lean b/lean-circuit/LeanCircuit/Poseidon/Constants.lean deleted file mode 100644 index 2c3c179..0000000 --- a/lean-circuit/LeanCircuit/Poseidon/Constants.lean +++ /dev/null @@ -1,46 +0,0 @@ -import Mathlib - -structure Constants where - prime : Nat - t : Nat - t_ne_zero : t ≠ 0 - R_F : Nat - R_P : Nat - round_constants : List (ZMod prime) - MDS_matrix : Matrix (Fin t) (Fin t) (ZMod prime) - -namespace Constants - -abbrev F (cfg : Constants) : Type := ZMod cfg.prime - -instance {cfg : Constants} : NeZero cfg.t := ⟨cfg.t_ne_zero⟩ - -def bn254_prime : Nat := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 - -def x5_254_2_constants : List (ZMod bn254_prime) := [0x09c46e9ec68e9bd4fe1faaba294cba38a71aa177534cdd1b6c7dc0dbd0abd7a7, 0x0c0356530896eec42a97ed937f3135cfc5142b3ae405b8343c1d83ffa604cb81, 0x1e28a1d935698ad1142e51182bb54cf4a00ea5aabd6268bd317ea977cc154a30, 0x27af2d831a9d2748080965db30e298e40e5757c3e008db964cf9e2b12b91251f, 0x1e6f11ce60fc8f513a6a3cfe16ae175a41291462f214cd0879aaf43545b74e03, 0x2a67384d3bbd5e438541819cb681f0be04462ed14c3613d8f719206268d142d3, 0x0b66fdf356093a611609f8e12fbfecf0b985e381f025188936408f5d5c9f45d0, 0x012ee3ec1e78d470830c61093c2ade370b26c83cc5cebeeddaa6852dbdb09e21, 0x0252ba5f6760bfbdfd88f67f8175e3fd6cd1c431b099b6bb2d108e7b445bb1b9, 0x179474cceca5ff676c6bec3cef54296354391a8935ff71d6ef5aeaad7ca932f1, 0x2c24261379a51bfa9228ff4a503fd4ed9c1f974a264969b37e1a2589bbed2b91, 0x1cc1d7b62692e63eac2f288bd0695b43c2f63f5001fc0fc553e66c0551801b05, 0x255059301aada98bb2ed55f852979e9600784dbf17fbacd05d9eff5fd9c91b56, 0x28437be3ac1cb2e479e1f5c0eccd32b3aea24234970a8193b11c29ce7e59efd9, 0x28216a442f2e1f711ca4fa6b53766eb118548da8fb4f78d4338762c37f5f2043, 0x2c1f47cd17fa5adf1f39f4e7056dd03feee1efce03094581131f2377323482c9, 0x07abad02b7a5ebc48632bcc9356ceb7dd9dafca276638a63646b8566a621afc9, 0x0230264601ffdf29275b33ffaab51dfe9429f90880a69cd137da0c4d15f96c3c, 0x1bc973054e51d905a0f168656497ca40a864414557ee289e717e5d66899aa0a9, 0x2e1c22f964435008206c3157e86341edd249aff5c2d8421f2a6b22288f0a67fc, 0x1224f38df67c5378121c1d5f461bbc509e8ea1598e46c9f7a70452bc2bba86b8, 0x02e4e69d8ba59e519280b4bd9ed0068fd7bfe8cd9dfeda1969d2989186cde20e, 0x1f1eccc34aaba0137f5df81fc04ff3ee4f19ee364e653f076d47e9735d98018e, 0x1672ad3d709a353974266c3039a9a7311424448032cd1819eacb8a4d4284f582, 0x283e3fdc2c6e420c56f44af5192b4ae9cda6961f284d24991d2ed602df8c8fc7, 0x1c2a3d120c550ecfd0db0957170fa013683751f8fdff59d6614fbd69ff394bcc, 0x216f84877aac6172f7897a7323456efe143a9a43773ea6f296cb6b8177653fbd, 0x2c0d272becf2a75764ba7e8e3e28d12bceaa47ea61ca59a411a1f51552f94788, 0x16e34299865c0e28484ee7a74c454e9f170a5480abe0508fcb4a6c3d89546f43, 0x175ceba599e96f5b375a232a6fb9cc71772047765802290f48cd939755488fc5, 0x0c7594440dc48c16fead9e1758b028066aa410bfbc354f54d8c5ffbb44a1ee32, 0x1a3c29bc39f21bb5c466db7d7eb6fd8f760e20013ccf912c92479882d919fd8d, 0x0ccfdd906f3426e5c0986ea049b253400855d349074f5a6695c8eeabcd22e68f, 0x14f6bc81d9f186f62bdb475ce6c9411866a7a8a3fd065b3ce0e699b67dd9e796, 0x0962b82789fb3d129702ca70b2f6c5aacc099810c9c495c888edeb7386b97052, 0x1a880af7074d18b3bf20c79de25127bc13284ab01ef02575afef0c8f6a31a86d, 0x10cba18419a6a332cd5e77f0211c154b20af2924fc20ff3f4c3012bb7ae9311b, 0x057e62a9a8f89b3ebdc76ba63a9eaca8fa27b7319cae3406756a2849f302f10d, 0x287c971de91dc0abd44adf5384b4988cb961303bbf65cff5afa0413b44280cee, 0x21df3388af1687bbb3bca9da0cca908f1e562bc46d4aba4e6f7f7960e306891d, 0x1be5c887d25bce703e25cc974d0934cd789df8f70b498fd83eff8b560e1682b3, 0x268da36f76e568fb68117175cea2cd0dd2cb5d42fda5acea48d59c2706a0d5c1, 0x0e17ab091f6eae50c609beaf5510ececc5d8bb74135ebd05bd06460cc26a5ed6, 0x04d727e728ffa0a67aee535ab074a43091ef62d8cf83d270040f5caa1f62af40, 0x0ddbd7bf9c29341581b549762bc022ed33702ac10f1bfd862b15417d7e39ca6e, 0x2790eb3351621752768162e82989c6c234f5b0d1d3af9b588a29c49c8789654b, 0x1e457c601a63b73e4471950193d8a570395f3d9ab8b2fd0984b764206142f9e9, 0x21ae64301dca9625638d6ab2bbe7135ffa90ecd0c43ff91fc4c686fc46e091b0, 0x0379f63c8ce3468d4da293166f494928854be9e3432e09555858534eed8d350b, 0x002d56420359d0266a744a080809e054ca0e4921a46686ac8c9f58a324c35049, 0x123158e5965b5d9b1d68b3cd32e10bbeda8d62459e21f4090fc2c5af963515a6, 0x0be29fc40847a941661d14bbf6cbe0420fbb2b6f52836d4e60c80eb49cad9ec1, 0x1ac96991dec2bb0557716142015a453c36db9d859cad5f9a233802f24fdf4c1a, 0x1596443f763dbcc25f4964fc61d23b3e5e12c9fa97f18a9251ca3355bcb0627e, 0x12e0bcd3654bdfa76b2861d4ec3aeae0f1857d9f17e715aed6d049eae3ba3212, 0x0fc92b4f1bbea82b9ea73d4af9af2a50ceabac7f37154b1904e6c76c7cf964ba, 0x1f9c0b1610446442d6f2e592a8013f40b14f7c7722236f4f9c7e965233872762, 0x0ebd74244ae72675f8cde06157a782f4050d914da38b4c058d159f643dbbf4d3, 0x2cb7f0ed39e16e9f69a9fafd4ab951c03b0671e97346ee397a839839dccfc6d1, 0x1a9d6e2ecff022cc5605443ee41bab20ce761d0514ce526690c72bca7352d9bf, 0x2a115439607f335a5ea83c3bc44a9331d0c13326a9a7ba3087da182d648ec72f, 0x23f9b6529b5d040d15b8fa7aee3e3410e738b56305cd44f29535c115c5a4c060, 0x05872c16db0f72a2249ac6ba484bb9c3a3ce97c16d58b68b260eb939f0e6e8a7, 0x1300bdee08bb7824ca20fb80118075f40219b6151d55b5c52b624a7cdeddf6a7, 0x19b9b63d2f108e17e63817863a8f6c288d7ad29916d98cb1072e4e7b7d52b376, 0x015bee1357e3c015b5bda237668522f613d1c88726b5ec4224a20128481b4f7f, 0x2953736e94bb6b9f1b9707a4f1615e4efe1e1ce4bab218cbea92c785b128ffd1, 0x0b069353ba091618862f806180c0385f851b98d372b45f544ce7266ed6608dfc, 0x304f74d461ccc13115e4e0bcfb93817e55aeb7eb9306b64e4f588ac97d81f429, 0x15bbf146ce9bca09e8a33f5e77dfe4f5aad2a164a4617a4cb8ee5415cde913fc, 0x0ab4dfe0c2742cde44901031487964ed9b8f4b850405c10ca9ff23859572c8c6, 0x0e32db320a044e3197f45f7649a19675ef5eedfea546dea9251de39f9639779a, 0x0a1756aa1f378ca4b27635a78b6888e66797733a82774896a3078efa516da016, 0x044c4a33b10f693447fd17177f952ef895e61d328f85efa94254d6a2a25d93ef, 0x2ed3611b725b8a70be655b537f66f700fe0879d79a496891d37b07b5466c4b8b, 0x1f9ba4e8bab7ce42c8ecc3d722aa2e0eadfdeb9cfdd347b5d8339ea7120858aa, 0x1b233043052e8c288f7ee907a84e518aa38e82ac4502066db74056f865c5d3da, 0x2431e1cc164bb8d074031ab72bd55b4c902053bfc0f14db0ca2f97b020875954, 0x082f934c91f5aac330cd6953a0a7db45a13e322097583319a791f273965801fd, 0x2b9a0a223e7538b0a34be074315542a3c77245e2ae7cbe999ad6bb930c48997c, 0x0e1cd91edd2cfa2cceb85483b887a9be8164163e75a8a00eb0b589cc70214e7d, 0x2e1eac0f2bfdfd63c951f61477e3698999774f19854d00f588d324601cebe2f9, 0x0cbfa95f37fb74060c76158e769d6d157345784d8efdb33c23d748115b500b83, 0x08f05b3be923ed44d65ad49d8a61e9a676d991e3a77513d9980c232dfa4a4f84, 0x22719e2a070bcd0852bf8e21984d0443e7284925dc0758a325a2dd510c047ef6, 0x041f596a9ee1cb2bc060f7fcc3a1ab4c7bdbf036119982c0f41f62b2f26830c0, 0x233fd35de1be520a87628eb06f6b1d4c021be1c2d0dc464a19fcdd0986b10f89, 0x0524b46d1aa87a5e4325e0a423ebc810d31e078aa1b4707eefcb453c61c9c267, 0x2c34f424c81e5716ce47fcac894b85824227bb954b0f3199cc4486237c515211, 0x0b5f2a4b63387819207effc2b5541fb72dd2025b5457cc97f33010327de4915e, 0x22207856082ccc54c5b72fe439d2cfd6c17435d2f57af6ceaefac41fe05c659f, 0x24d57a8bf5da63fe4e24159b7f8950b5cdfb210194caf79f27854048ce2c8171, 0x0afab181fdd5e0583b371d75bd693f98374ad7097bb01a8573919bb23b79396e, 0x2dba9b108f208772998a52efac7cbd5676c0057194c16c0bf16290d62b1128ee, 0x26349b66edb8b16f56f881c788f53f83cbb83de0bd592b255aff13e6bce420b3, 0x25af7ce0e5e10357685e95f92339753ad81a56d28ecc193b235288a3e6f137db, 0x25b4ce7bd2294390c094d6a55edd68b970eed7aae88b2bff1f7c0187fe35011f, 0x22c543f10f6c89ec387e53f1908a88e5de9cef28ebdf30b18cb9d54c1e02b631, 0x0236f93e7789c4724fc7908a9f191e1e425e906a919d7a34df668e74882f87a9, 0x29350b401166ca010e7d27e37d05da99652bdae114eb01659cb497af980c4b52, 0x0eed787d65820d3f6bd31bbab547f75a65edb75d844ebb89ee1260916652363f, 0x07cc1170f13b46f2036a753f520b3291fdcd0e99bd94297d1906f656f4de6fad, 0x22b939233b1d7205f49bcf613a3d30b1908786d7f9f5d10c2059435689e8acea, 0x01451762a0aab81c8aad1dc8bc33e870740f083a5aa85438add650ace60ae5a6, 0x23506bb5d8727d4461fabf1025d46d1fe32eaa61dec7da57e704fec0892fce89, 0x2e484c44e838aea0bac06ae3f71bdd092a3709531e1efea97f8bd68907355522, 0x0f4bc7d07ebafd64379e78c50bd2e42baf4a594545cedc2545418da26835b54c, 0x1f4d3c8f6583e9e5fa76637862faaee851582388725df460e620996d50d8e74e, 0x093514e0c70711f82660d07be0e4a988fae02abc7b681d9153eb9bcb48fe7389, 0x1adab0c8e2b3bad346699a2b5f3bc03643ee83ece47228f24a58e0a347e153d8, 0x1672b1726057d99dd14709ebb474641a378c1b94b8072bac1a22dbef9e80dad2, 0x1dfd53d4576af2e38f44f53fdcab468cc5d8e2fae0acc4ee30d47b239b479c14, 0x0c6888a10b75b0f3a70a36263a37e17fe6d77d640f6fc3debc7f207753205c60, 0x1addb933a65be77092b34a7e77d12fe8611a61e00ee6848b85091ecca9d1e508, 0x00d7540dcd268a845c10ae18d1de933cf638ff5425f0afff7935628e299d1791, 0x140c0e42687e9ead01b2827a5664ca9c26fedde4acd99db1d316939d20b82c0e, 0x2f0c3a115d4317d191ba89b8d13d1806c20a0f9b24f8c5edc091e2ae56565984, 0x0c4ee778ff7c14553006ed220cf9c81008a0cff670b22b82d8c538a1dc958c61, 0x1704f2766d46f82c3693f00440ccc3609424ed26c0acc66227c3d7485de74c69, 0x2f2d19cc3ea5d78ea7a02c1b51d244abf0769c9f8544e40239b66fe9009c3cfa, 0x1ae03853b75fcaba5053f112e2a8e8dcdd7ee6cb9cfed9c7d6c766a806fc6629, 0x0971aabf795241df51d131d0fa61aa5f3556921b2d6f014e4e41a86ddaf056d5, 0x1408c316e6014e1a91d4cf6b6e0de73eda624f8380df1c875f5c29f7bfe2f646, 0x1667f3fe2edbe850248abe42b543093b6c89f1f773ef285341691f39822ef5bd, 0x13bf7c5d0d2c4376a48b0a03557cdf915b81718409e5c133424c69576500fe37, 0x07620a6dfb0b6cec3016adf3d3533c24024b95347856b79719bc0ba743a62c2c, 0x1574c7ef0c43545f36a8ca08bdbdd8b075d2959e2f322b731675de3e1982b4d0, 0x269e4b5b7a2eb21afd567970a717ceec5bd4184571c254fdc06e03a7ff8378f0] -def x5_254_2_MDS_matrix : Matrix (Fin 2) (Fin 2) (ZMod bn254_prime) := ![![0x066f6f85d6f68a85ec10345351a23a3aaf07f38af8c952a7bceca70bd2af7ad5, 0x2b9d4b4110c9ae997782e1509b1d0fdb20a7c02bbd8bea7305462b9f8125b1e8],![0x0cc57cdbb08507d62bf67a4493cc262fb6c09d557013fff1f573f431221f8ff9, 0x1274e649a32ed355a31a6ed69724e1adade857e86eb5c3a121bcd147943203c8]] - -def x5_254_3_constants : List (ZMod bn254_prime) := [0x0ee9a592ba9a9518d05986d656f40c2114c4993c11bb29938d21d47304cd8e6e, 0x00f1445235f2148c5986587169fc1bcd887b08d4d00868df5696fff40956e864, 0x08dff3487e8ac99e1f29a058d0fa80b930c728730b7ab36ce879f3890ecf73f5, 0x2f27be690fdaee46c3ce28f7532b13c856c35342c84bda6e20966310fadc01d0, 0x2b2ae1acf68b7b8d2416bebf3d4f6234b763fe04b8043ee48b8327bebca16cf2, 0x0319d062072bef7ecca5eac06f97d4d55952c175ab6b03eae64b44c7dbf11cfa, 0x28813dcaebaeaa828a376df87af4a63bc8b7bf27ad49c6298ef7b387bf28526d, 0x2727673b2ccbc903f181bf38e1c1d40d2033865200c352bc150928adddf9cb78, 0x234ec45ca27727c2e74abd2b2a1494cd6efbd43e340587d6b8fb9e31e65cc632, 0x15b52534031ae18f7f862cb2cf7cf760ab10a8150a337b1ccd99ff6e8797d428, 0x0dc8fad6d9e4b35f5ed9a3d186b79ce38e0e8a8d1b58b132d701d4eecf68d1f6, 0x1bcd95ffc211fbca600f705fad3fb567ea4eb378f62e1fec97805518a47e4d9c, 0x10520b0ab721cadfe9eff81b016fc34dc76da36c2578937817cb978d069de559, 0x1f6d48149b8e7f7d9b257d8ed5fbbaf42932498075fed0ace88a9eb81f5627f6, 0x1d9655f652309014d29e00ef35a2089bfff8dc1c816f0dc9ca34bdb5460c8705, 0x04df5a56ff95bcafb051f7b1cd43a99ba731ff67e47032058fe3d4185697cc7d, 0x0672d995f8fff640151b3d290cedaf148690a10a8c8424a7f6ec282b6e4be828, 0x099952b414884454b21200d7ffafdd5f0c9a9dcc06f2708e9fc1d8209b5c75b9, 0x052cba2255dfd00c7c483143ba8d469448e43586a9b4cd9183fd0e843a6b9fa6, 0x0b8badee690adb8eb0bd74712b7999af82de55707251ad7716077cb93c464ddc, 0x119b1590f13307af5a1ee651020c07c749c15d60683a8050b963d0a8e4b2bdd1, 0x03150b7cd6d5d17b2529d36be0f67b832c4acfc884ef4ee5ce15be0bfb4a8d09, 0x2cc6182c5e14546e3cf1951f173912355374efb83d80898abe69cb317c9ea565, 0x005032551e6378c450cfe129a404b3764218cadedac14e2b92d2cd73111bf0f9, 0x233237e3289baa34bb147e972ebcb9516469c399fcc069fb88f9da2cc28276b5, 0x05c8f4f4ebd4a6e3c980d31674bfbe6323037f21b34ae5a4e80c2d4c24d60280, 0x0a7b1db13042d396ba05d818a319f25252bcf35ef3aeed91ee1f09b2590fc65b, 0x2a73b71f9b210cf5b14296572c9d32dbf156e2b086ff47dc5df542365a404ec0, 0x1ac9b0417abcc9a1935107e9ffc91dc3ec18f2c4dbe7f22976a760bb5c50c460, 0x12c0339ae08374823fabb076707ef479269f3e4d6cb104349015ee046dc93fc0, 0x0b7475b102a165ad7f5b18db4e1e704f52900aa3253baac68246682e56e9a28e, 0x037c2849e191ca3edb1c5e49f6e8b8917c843e379366f2ea32ab3aa88d7f8448, 0x05a6811f8556f014e92674661e217e9bd5206c5c93a07dc145fdb176a716346f, 0x29a795e7d98028946e947b75d54e9f044076e87a7b2883b47b675ef5f38bd66e, 0x20439a0c84b322eb45a3857afc18f5826e8c7382c8a1585c507be199981fd22f, 0x2e0ba8d94d9ecf4a94ec2050c7371ff1bb50f27799a84b6d4a2a6f2a0982c887, 0x143fd115ce08fb27ca38eb7cce822b4517822cd2109048d2e6d0ddcca17d71c8, 0x0c64cbecb1c734b857968dbbdcf813cdf8611659323dbcbfc84323623be9caf1, 0x028a305847c683f646fca925c163ff5ae74f348d62c2b670f1426cef9403da53, 0x2e4ef510ff0b6fda5fa940ab4c4380f26a6bcb64d89427b824d6755b5db9e30c, 0x0081c95bc43384e663d79270c956ce3b8925b4f6d033b078b96384f50579400e, 0x2ed5f0c91cbd9749187e2fade687e05ee2491b349c039a0bba8a9f4023a0bb38, 0x30509991f88da3504bbf374ed5aae2f03448a22c76234c8c990f01f33a735206, 0x1c3f20fd55409a53221b7c4d49a356b9f0a1119fb2067b41a7529094424ec6ad, 0x10b4e7f3ab5df003049514459b6e18eec46bb2213e8e131e170887b47ddcb96c, 0x2a1982979c3ff7f43ddd543d891c2abddd80f804c077d775039aa3502e43adef, 0x1c74ee64f15e1db6feddbead56d6d55dba431ebc396c9af95cad0f1315bd5c91, 0x07533ec850ba7f98eab9303cace01b4b9e4f2e8b82708cfa9c2fe45a0ae146a0, 0x21576b438e500449a151e4eeaf17b154285c68f42d42c1808a11abf3764c0750, 0x2f17c0559b8fe79608ad5ca193d62f10bce8384c815f0906743d6930836d4a9e, 0x2d477e3862d07708a79e8aae946170bc9775a4201318474ae665b0b1b7e2730e, 0x162f5243967064c390e095577984f291afba2266c38f5abcd89be0f5b2747eab, 0x2b4cb233ede9ba48264ecd2c8ae50d1ad7a8596a87f29f8a7777a70092393311, 0x2c8fbcb2dd8573dc1dbaf8f4622854776db2eece6d85c4cf4254e7c35e03b07a, 0x1d6f347725e4816af2ff453f0cd56b199e1b61e9f601e9ade5e88db870949da9, 0x204b0c397f4ebe71ebc2d8b3df5b913df9e6ac02b68d31324cd49af5c4565529, 0x0c4cb9dc3c4fd8174f1149b3c63c3c2f9ecb827cd7dc25534ff8fb75bc79c502, 0x174ad61a1448c899a25416474f4930301e5c49475279e0639a616ddc45bc7b54, 0x1a96177bcf4d8d89f759df4ec2f3cde2eaaa28c177cc0fa13a9816d49a38d2ef, 0x066d04b24331d71cd0ef8054bc60c4ff05202c126a233c1a8242ace360b8a30a, 0x2a4c4fc6ec0b0cf52195782871c6dd3b381cc65f72e02ad527037a62aa1bd804, 0x13ab2d136ccf37d447e9f2e14a7cedc95e727f8446f6d9d7e55afc01219fd649, 0x1121552fca26061619d24d843dc82769c1b04fcec26f55194c2e3e869acc6a9a, 0x00ef653322b13d6c889bc81715c37d77a6cd267d595c4a8909a5546c7c97cff1, 0x0e25483e45a665208b261d8ba74051e6400c776d652595d9845aca35d8a397d3, 0x29f536dcb9dd7682245264659e15d88e395ac3d4dde92d8c46448db979eeba89, 0x2a56ef9f2c53febadfda33575dbdbd885a124e2780bbea170e456baace0fa5be, 0x1c8361c78eb5cf5decfb7a2d17b5c409f2ae2999a46762e8ee416240a8cb9af1, 0x151aff5f38b20a0fc0473089aaf0206b83e8e68a764507bfd3d0ab4be74319c5, 0x04c6187e41ed881dc1b239c88f7f9d43a9f52fc8c8b6cdd1e76e47615b51f100, 0x13b37bd80f4d27fb10d84331f6fb6d534b81c61ed15776449e801b7ddc9c2967, 0x01a5c536273c2d9df578bfbd32c17b7a2ce3664c2a52032c9321ceb1c4e8a8e4, 0x2ab3561834ca73835ad05f5d7acb950b4a9a2c666b9726da832239065b7c3b02, 0x1d4d8ec291e720db200fe6d686c0d613acaf6af4e95d3bf69f7ed516a597b646, 0x041294d2cc484d228f5784fe7919fd2bb925351240a04b711514c9c80b65af1d, 0x154ac98e01708c611c4fa715991f004898f57939d126e392042971dd90e81fc6, 0x0b339d8acca7d4f83eedd84093aef51050b3684c88f8b0b04524563bc6ea4da4, 0x0955e49e6610c94254a4f84cfbab344598f0e71eaff4a7dd81ed95b50839c82e, 0x06746a6156eba54426b9e22206f15abca9a6f41e6f535c6f3525401ea0654626, 0x0f18f5a0ecd1423c496f3820c549c27838e5790e2bd0a196ac917c7ff32077fb, 0x04f6eeca1751f7308ac59eff5beb261e4bb563583ede7bc92a738223d6f76e13, 0x2b56973364c4c4f5c1a3ec4da3cdce038811eb116fb3e45bc1768d26fc0b3758, 0x123769dd49d5b054dcd76b89804b1bcb8e1392b385716a5d83feb65d437f29ef, 0x2147b424fc48c80a88ee52b91169aacea989f6446471150994257b2fb01c63e9, 0x0fdc1f58548b85701a6c5505ea332a29647e6f34ad4243c2ea54ad897cebe54d, 0x12373a8251fea004df68abcf0f7786d4bceff28c5dbbe0c3944f685cc0a0b1f2, 0x21e4f4ea5f35f85bad7ea52ff742c9e8a642756b6af44203dd8a1f35c1a90035, 0x16243916d69d2ca3dfb4722224d4c462b57366492f45e90d8a81934f1bc3b147, 0x1efbe46dd7a578b4f66f9adbc88b4378abc21566e1a0453ca13a4159cac04ac2, 0x07ea5e8537cf5dd08886020e23a7f387d468d5525be66f853b672cc96a88969a, 0x05a8c4f9968b8aa3b7b478a30f9a5b63650f19a75e7ce11ca9fe16c0b76c00bc, 0x20f057712cc21654fbfe59bd345e8dac3f7818c701b9c7882d9d57b72a32e83f, 0x04a12ededa9dfd689672f8c67fee31636dcd8e88d01d49019bd90b33eb33db69, 0x27e88d8c15f37dcee44f1e5425a51decbd136ce5091a6767e49ec9544ccd101a, 0x2feed17b84285ed9b8a5c8c5e95a41f66e096619a7703223176c41ee433de4d1, 0x1ed7cc76edf45c7c404241420f729cf394e5942911312a0d6972b8bd53aff2b8, 0x15742e99b9bfa323157ff8c586f5660eac6783476144cdcadf2874be45466b1a, 0x1aac285387f65e82c895fc6887ddf40577107454c6ec0317284f033f27d0c785, 0x25851c3c845d4790f9ddadbdb6057357832e2e7a49775f71ec75a96554d67c77, 0x15a5821565cc2ec2ce78457db197edf353b7ebba2c5523370ddccc3d9f146a67, 0x2411d57a4813b9980efa7e31a1db5966dcf64f36044277502f15485f28c71727, 0x002e6f8d6520cd4713e335b8c0b6d2e647e9a98e12f4cd2558828b5ef6cb4c9b, 0x2ff7bc8f4380cde997da00b616b0fcd1af8f0e91e2fe1ed7398834609e0315d2, 0x00b9831b948525595ee02724471bcd182e9521f6b7bb68f1e93be4febb0d3cbe, 0x0a2f53768b8ebf6a86913b0e57c04e011ca408648a4743a87d77adbf0c9c3512, 0x00248156142fd0373a479f91ff239e960f599ff7e94be69b7f2a290305e1198d, 0x171d5620b87bfb1328cf8c02ab3f0c9a397196aa6a542c2350eb512a2b2bcda9, 0x170a4f55536f7dc970087c7c10d6fad760c952172dd54dd99d1045e4ec34a808, 0x29aba33f799fe66c2ef3134aea04336ecc37e38c1cd211ba482eca17e2dbfae1, 0x1e9bc179a4fdd758fdd1bb1945088d47e70d114a03f6a0e8b5ba650369e64973, 0x1dd269799b660fad58f7f4892dfb0b5afeaad869a9c4b44f9c9e1c43bdaf8f09, 0x22cdbc8b70117ad1401181d02e15459e7ccd426fe869c7c95d1dd2cb0f24af38, 0x0ef042e454771c533a9f57a55c503fcefd3150f52ed94a7cd5ba93b9c7dacefd, 0x11609e06ad6c8fe2f287f3036037e8851318e8b08a0359a03b304ffca62e8284, 0x1166d9e554616dba9e753eea427c17b7fecd58c076dfe42708b08f5b783aa9af, 0x2de52989431a859593413026354413db177fbf4cd2ac0b56f855a888357ee466, 0x3006eb4ffc7a85819a6da492f3a8ac1df51aee5b17b8e89d74bf01cf5f71e9ad, 0x2af41fbb61ba8a80fdcf6fff9e3f6f422993fe8f0a4639f962344c8225145086, 0x119e684de476155fe5a6b41a8ebc85db8718ab27889e85e781b214bace4827c3, 0x1835b786e2e8925e188bea59ae363537b51248c23828f047cff784b97b3fd800, 0x28201a34c594dfa34d794996c6433a20d152bac2a7905c926c40e285ab32eeb6, 0x083efd7a27d1751094e80fefaf78b000864c82eb571187724a761f88c22cc4e7, 0x0b6f88a3577199526158e61ceea27be811c16df7774dd8519e079564f61fd13b, 0x0ec868e6d15e51d9644f66e1d6471a94589511ca00d29e1014390e6ee4254f5b, 0x2af33e3f866771271ac0c9b3ed2e1142ecd3e74b939cd40d00d937ab84c98591, 0x0b520211f904b5e7d09b5d961c6ace7734568c547dd6858b364ce5e47951f178, 0x0b2d722d0919a1aad8db58f10062a92ea0c56ac4270e822cca228620188a1d40, 0x1f790d4d7f8cf094d980ceb37c2453e957b54a9991ca38bbe0061d1ed6e562d4, 0x0171eb95dfbf7d1eaea97cd385f780150885c16235a2a6a8da92ceb01e504233, 0x0c2d0e3b5fd57549329bf6885da66b9b790b40defd2c8650762305381b168873, 0x1162fb28689c27154e5a8228b4e72b377cbcafa589e283c35d3803054407a18d, 0x2f1459b65dee441b64ad386a91e8310f282c5a92a89e19921623ef8249711bc0, 0x1e6ff3216b688c3d996d74367d5cd4c1bc489d46754eb712c243f70d1b53cfbb, 0x01ca8be73832b8d0681487d27d157802d741a6f36cdc2a0576881f9326478875, 0x1f7735706ffe9fc586f976d5bdf223dc680286080b10cea00b9b5de315f9650e, 0x2522b60f4ea3307640a0c2dce041fba921ac10a3d5f096ef4745ca838285f019, 0x23f0bee001b1029d5255075ddc957f833418cad4f52b6c3f8ce16c235572575b, 0x2bc1ae8b8ddbb81fcaac2d44555ed5685d142633e9df905f66d9401093082d59, 0x0f9406b8296564a37304507b8dba3ed162371273a07b1fc98011fcd6ad72205f, 0x2360a8eb0cc7defa67b72998de90714e17e75b174a52ee4acb126c8cd995f0a8, 0x15871a5cddead976804c803cbaef255eb4815a5e96df8b006dcbbc2767f88948, 0x193a56766998ee9e0a8652dd2f3b1da0362f4f54f72379544f957ccdeefb420f, 0x2a394a43934f86982f9be56ff4fab1703b2e63c8ad334834e4309805e777ae0f, 0x1859954cfeb8695f3e8b635dcb345192892cd11223443ba7b4166e8876c0d142, 0x04e1181763050e58013444dbcb99f1902b11bc25d90bbdca408d3819f4fed32b, 0x0fdb253dee83869d40c335ea64de8c5bb10eb82db08b5e8b1f5e5552bfd05f23, 0x058cbe8a9a5027bdaa4efb623adead6275f08686f1c08984a9d7c5bae9b4f1c0, 0x1382edce9971e186497eadb1aeb1f52b23b4b83bef023ab0d15228b4cceca59a, 0x03464990f045c6ee0819ca51fd11b0be7f61b8eb99f14b77e1e6634601d9e8b5, 0x23f7bfc8720dc296fff33b41f98ff83c6fcab4605db2eb5aaa5bc137aeb70a58, 0x0a59a158e3eec2117e6e94e7f0e9decf18c3ffd5e1531a9219636158bbaf62f2, 0x06ec54c80381c052b58bf23b312ffd3ce2c4eba065420af8f4c23ed0075fd07b, 0x118872dc832e0eb5476b56648e867ec8b09340f7a7bcb1b4962f0ff9ed1f9d01, 0x13d69fa127d834165ad5c7cba7ad59ed52e0b0f0e42d7fea95e1906b520921b1, 0x169a177f63ea681270b1c6877a73d21bde143942fb71dc55fd8a49f19f10c77b, 0x04ef51591c6ead97ef42f287adce40d93abeb032b922f66ffb7e9a5a7450544d, 0x256e175a1dc079390ecd7ca703fb2e3b19ec61805d4f03ced5f45ee6dd0f69ec, 0x30102d28636abd5fe5f2af412ff6004f75cc360d3205dd2da002813d3e2ceeb2, 0x10998e42dfcd3bbf1c0714bc73eb1bf40443a3fa99bef4a31fd31be182fcc792, 0x193edd8e9fcf3d7625fa7d24b598a1d89f3362eaf4d582efecad76f879e36860, 0x18168afd34f2d915d0368ce80b7b3347d1c7a561ce611425f2664d7aa51f0b5d, 0x29383c01ebd3b6ab0c017656ebe658b6a328ec77bc33626e29e2e95b33ea6111, 0x10646d2f2603de39a1f4ae5e7771a64a702db6e86fb76ab600bf573f9010c711, 0x0beb5e07d1b27145f575f1395a55bf132f90c25b40da7b3864d0242dcb1117fb, 0x16d685252078c133dc0d3ecad62b5c8830f95bb2e54b59abdffbf018d96fa336, 0x0a6abd1d833938f33c74154e0404b4b40a555bbbec21ddfafd672dd62047f01a, 0x1a679f5d36eb7b5c8ea12a4c2dedc8feb12dffeec450317270a6f19b34cf1860, 0x0980fb233bd456c23974d50e0ebfde4726a423eada4e8f6ffbc7592e3f1b93d6, 0x161b42232e61b84cbf1810af93a38fc0cece3d5628c9282003ebacb5c312c72b, 0x0ada10a90c7f0520950f7d47a60d5e6a493f09787f1564e5d09203db47de1a0b, 0x1a730d372310ba82320345a29ac4238ed3f07a8a2b4e121bb50ddb9af407f451, 0x2c8120f268ef054f817064c369dda7ea908377feaba5c4dffbda10ef58e8c556, 0x1c7c8824f758753fa57c00789c684217b930e95313bcb73e6e7b8649a4968f70, 0x2cd9ed31f5f8691c8e39e4077a74faa0f400ad8b491eb3f7b47b27fa3fd1cf77, 0x23ff4f9d46813457cf60d92f57618399a5e022ac321ca550854ae23918a22eea, 0x09945a5d147a4f66ceece6405dddd9d0af5a2c5103529407dff1ea58f180426d, 0x188d9c528025d4c2b67660c6b771b90f7c7da6eaa29d3f268a6dd223ec6fc630, 0x3050e37996596b7f81f68311431d8734dba7d926d3633595e0c0d8ddf4f0f47f, 0x15af1169396830a91600ca8102c35c426ceae5461e3f95d89d829518d30afd78, 0x1da6d09885432ea9a06d9f37f873d985dae933e351466b2904284da3320d8acc, 0x2796ea90d269af29f5f8acf33921124e4e4fad3dbe658945e546ee411ddaa9cb, 0x202d7dd1da0f6b4b0325c8b3307742f01e15612ec8e9304a7cb0319e01d32d60, 0x096d6790d05bb759156a952ba263d672a2d7f9c788f4c831a29dace4c0f8be5f, 0x054efa1f65b0fce283808965275d877b438da23ce5b13e1963798cb1447d25a4, 0x1b162f83d917e93edb3308c29802deb9d8aa690113b2e14864ccf6e18e4165f1, 0x21e5241e12564dd6fd9f1cdd2a0de39eedfefc1466cc568ec5ceb745a0506edc, 0x1cfb5662e8cf5ac9226a80ee17b36abecb73ab5f87e161927b4349e10e4bdf08, 0x0f21177e302a771bbae6d8d1ecb373b62c99af346220ac0129c53f666eb24100, 0x1671522374606992affb0dd7f71b12bec4236aede6290546bcef7e1f515c2320, 0x0fa3ec5b9488259c2eb4cf24501bfad9be2ec9e42c5cc8ccd419d2a692cad870, 0x193c0e04e0bd298357cb266c1506080ed36edce85c648cc085e8c57b1ab54bba, 0x102adf8ef74735a27e9128306dcbc3c99f6f7291cd406578ce14ea2adaba68f8, 0x0fe0af7858e49859e2a54d6f1ad945b1316aa24bfbdd23ae40a6d0cb70c3eab1, 0x216f6717bbc7dedb08536a2220843f4e2da5f1daa9ebdefde8a5ea7344798d22, 0x1da55cc900f0d21f4a3e694391918a1b3c23b2ac773c6b3ef88e2e4228325161] -def x5_254_3_MDS_matrix : Matrix (Fin 3) (Fin 3) (ZMod bn254_prime) := ![![0x109b7f411ba0e4c9b2b70caf5c36a7b194be7c11ad24378bfedb68592ba8118b, 0x16ed41e13bb9c0c66ae119424fddbcbc9314dc9fdbdeea55d6c64543dc4903e0, 0x2b90bba00fca0589f617e7dcbfe82e0df706ab640ceb247b791a93b74e36736d], ![0x2969f27eed31a480b9c36c764379dbca2cc8fdd1415c3dded62940bcde0bd771, 0x2e2419f9ec02ec394c9871c832963dc1b89d743c8c7b964029b2311687b1fe23, 0x101071f0032379b697315876690f053d148d4e109f5fb065c8aacc55a0f89bfa], ![0x143021ec686a3f330d5f9e654638065ce6cd79e28c5b3753326244ee65a1b1a7, 0x176cc029695ad02582a70eff08a6fd99d057e12e58e7d7b6b16cdfabc8ee2911, 0x19a3fc0a56702bf417ba7fee3802593fa644470307043f7773279cd71d25d5e0]] - -def x5_254_3 : Constants := { - prime := bn254_prime, - t := 3, - t_ne_zero := by decide, - R_F := 8, - R_P := 57, - round_constants := x5_254_3_constants, - MDS_matrix := x5_254_3_MDS_matrix -} - -def x5_254_2 : Constants := { - prime := bn254_prime - t := 2, - t_ne_zero := by decide, - R_F := 8, - R_P := 56, - round_constants := x5_254_2_constants, - MDS_matrix := x5_254_2_MDS_matrix -} - -end Constants \ No newline at end of file diff --git a/lean-circuit/LeanCircuit/Poseidon/Correctness.lean b/lean-circuit/LeanCircuit/Poseidon/Correctness.lean deleted file mode 100644 index 7261764..0000000 --- a/lean-circuit/LeanCircuit/Poseidon/Correctness.lean +++ /dev/null @@ -1,391 +0,0 @@ -import LeanCircuit -import LeanCircuit.Poseidon.Constants -import LeanCircuit.Poseidon.Spec -import Mathlib -import ProvenZk - -open Matrix -open Semaphore (F Order) - -variable [Fact (Nat.Prime Order)] - -private lemma iff_to_eq {α} {a b: α} {k : α -> Prop }: a = b -> (k a ↔ k b) := by intro eq; rw [eq] - -def mds_matmul (cfg : Constants) (S : Vector cfg.F cfg.t) : Vector cfg.F cfg.t := (cfg.MDS_matrix ⬝ S.to_column).to_vector - -def full_round (cfg : Constants) (S C: Vector cfg.F cfg.t) : Vector cfg.F cfg.t := - mds_matmul cfg (S.mapIdx fun i s => (s + C.get i) ^ 5) - -def partial_round (cfg : Constants) (S C: Vector cfg.F cfg.t) : Vector cfg.F cfg.t := - let with_const := S.mapIdx fun i s => s + C.get i - mds_matmul cfg (with_const.set 0 (with_const.get 0 ^ 5)) - -def full_rounds (cfg : Constants) (state_words : Vector cfg.F cfg.t) (round_constants_counter rounds : ℕ) : Vector cfg.F cfg.t := Id.run do - let mut round_constants_counter := round_constants_counter - let mut state_words := state_words - - for _ in [0:rounds] do - let consts := Vector.ofFn (fun i => cfg.round_constants[round_constants_counter + i]!) - state_words := full_round cfg state_words consts - round_constants_counter := round_constants_counter + cfg.t - state_words - -def partial_rounds (cfg : Constants) (state_words : Vector cfg.F cfg.t) (round_constants_counter rounds : ℕ) : Vector cfg.F cfg.t := Id.run do - let mut round_constants_counter := round_constants_counter - let mut state_words := state_words - - for _ in [0:rounds] do - let consts := Vector.ofFn (fun i => cfg.round_constants[round_constants_counter + i]!) - state_words := partial_round cfg state_words consts - round_constants_counter := round_constants_counter + cfg.t - state_words - -def full_rounds_cps - (cfg : Constants) - (full_round : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop) - (state: Vector cfg.F cfg.t) - (init_const: Nat) - (round_count: Nat) - (k : Vector cfg.F cfg.t -> Prop): Prop := match round_count with -| Nat.zero => k state -| Nat.succ round_count => - full_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' => - full_rounds_cps cfg full_round state' (init_const + cfg.t) round_count k - -def half_rounds_cps - (cfg : Constants) - (half_round : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop) - (state: Vector cfg.F cfg.t) - (init_const: Nat) - (round_count: Nat) - (k : Vector cfg.F cfg.t -> Prop): Prop := match round_count with -| Nat.zero => k state -| Nat.succ round_count => - half_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' => - half_rounds_cps cfg half_round state' (init_const + cfg.t) round_count k - -lemma sbox_uncps (A : F) (k : F -> Prop): Semaphore.sbox A k = k (A ^ 5) := by - unfold Semaphore.sbox - simp [Gates.mul] - apply iff_to_eq - repeat (rw [pow_succ]) - rw [pow_zero, mul_one, mul_assoc] - -lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop): - Semaphore.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by - simp [Semaphore.mds_3, Gates.add, Gates.mul] - apply iff_to_eq - simp [mds_matmul, Constants.x5_254_3, Constants.x5_254_3_MDS_matrix] - simp [Vector.to_column, Matrix.to_vector, Vector.ofFn] - repeat ( - apply congrArg₂ - { - simp [getElem, Matrix.of, Matrix.mul, Matrix.dotProduct] - simp [Finset.sum, Finset.univ, Fintype.elems] - rw [←add_assoc] - conv => lhs; simp [mul_comm] - } - ) - rfl - -lemma mds_2_uncps (S : Vector F 2) (k : Vector F 2 -> Prop): - Semaphore.mds_2 S k = k (mds_matmul Constants.x5_254_2 S) := by - simp [Semaphore.mds_2, Gates.add, Gates.mul] - apply iff_to_eq - simp [mds_matmul, Constants.x5_254_2, Constants.x5_254_2_MDS_matrix] - simp [Vector.to_column, Matrix.to_vector, Vector.ofFn] - repeat ( - apply congrArg₂ - { - simp [getElem, Matrix.of, Matrix.mul, Matrix.dotProduct] - simp [Finset.sum, Finset.univ, Fintype.elems] - conv => lhs; simp [mul_comm] - } - ) - rfl - -lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop): - Semaphore.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by - unfold Semaphore.fullRound_3_3 - unfold Gates.add - simp [Gates.add, sbox_uncps, mds_3_uncps, full_round] - apply iff_to_eq - have : ∀ {α} {v : Vector α 3}, vec![v[0], v[1], v[2]] = v := by - intro α v - conv => rhs; rw [←Vector.ofFn_get v] - rw [this] - congr - conv => rhs ; rw [←Vector.ofFn_get S] - -lemma full_round_2_uncps (S C: Vector F 2) (k : Vector F 2 -> Prop): - Semaphore.fullRound_2_2 S C k = k (full_round Constants.x5_254_2 S C) := by - unfold Semaphore.fullRound_2_2 - unfold Gates.add - simp [Gates.add, sbox_uncps, mds_2_uncps, full_round] - apply iff_to_eq - have : ∀ {α} {v : Vector α 2}, vec![v[0], v[1]] = v := by - intro α v - conv => rhs; rw [←Vector.ofFn_get v] - rw [this] - congr - conv => rhs ; rw [←Vector.ofFn_get S] - -lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop): - Semaphore.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by - unfold Semaphore.halfRound_3_3 - unfold Gates.add - simp [Gates.add, sbox_uncps, mds_3_uncps, partial_round] - apply iff_to_eq - have : ∀ {α} {v : Vector α 3}, vec![v[0], v[1], v[2]] = v := by - intro α v - conv => rhs; rw [←Vector.ofFn_get v] - rw [this] - congr - conv => rhs ; rw [←Vector.ofFn_get S] - -lemma half_round_2_uncps (S C: Vector F 2) (k : Vector F 2 -> Prop): - Semaphore.halfRound_2_2 S C k = k (partial_round Constants.x5_254_2 S C) := by - unfold Semaphore.halfRound_2_2 - unfold Gates.add - simp [Gates.add, sbox_uncps, mds_2_uncps, partial_round] - apply iff_to_eq - have : ∀ {α} {v : Vector α 2}, vec![v[0], v[1]] = v := by - intro α v - conv => rhs; rw [←Vector.ofFn_get v] - rw [this] - congr - conv => rhs ; rw [←Vector.ofFn_get S] - -lemma partial_rounds_uncps - {cfg : Constants} - {S : Vector cfg.F cfg.t} - {start count : Nat} - {k : Vector cfg.F cfg.t -> Prop} - {half_round_cps : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop} - {half_round_uncps : ∀ S C k, half_round_cps S C k = k (partial_round cfg S C)} - : - half_rounds_cps cfg half_round_cps S start count k = k (partial_rounds cfg S start count) := by - induction count generalizing start S with - | zero => - simp [half_rounds_cps, partial_rounds, forIn, Std.Range.forIn, Std.Range.forIn.loop, Id.run] - | succ count ih => - unfold half_rounds_cps - rw [half_round_uncps, ih] - unfold partial_rounds - simp [Id.run, forIn] - apply iff_to_eq - simp [Std.Range.counter_elide_fst] - rw [←zero_add (Nat.succ count), Std.Range.forIn_startSucc] - have : Nat.succ 0 = 0 + 1 := by rfl - rw [this] - have : 0 + Nat.succ count = count + 1 := by simp_arith - rw [this] - rw [←Std.Range.forIn_ixShift] - apply congrArg₂ - { simp } - funext i r - congr - funext i' - have : start + cfg.t + i * cfg.t + ↑i' = start + (i + 1) * cfg.t + ↑i' := by linarith - rw [this] - -lemma partial_rounds_2_uncps - {S : Vector F 2} - {start count : Nat} - {k : Vector F 2 -> Prop}: - half_rounds_cps Constants.x5_254_2 Semaphore.halfRound_2_2 S start count k = k (partial_rounds Constants.x5_254_2 S start count) := by - apply partial_rounds_uncps - apply half_round_2_uncps - -lemma partial_rounds_3_uncps - {S : Vector F 3} - {start count : Nat} - {k : Vector F 3 -> Prop}: - half_rounds_cps Constants.x5_254_3 Semaphore.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by - apply partial_rounds_uncps - apply half_round_3_uncps - -lemma full_rounds_uncps - {cfg : Constants} - {S : Vector cfg.F cfg.t} - {start count : Nat} - {k : Vector cfg.F cfg.t -> Prop} - {full_round_cps : Vector cfg.F cfg.t -> Vector cfg.F cfg.t -> (Vector cfg.F cfg.t -> Prop) -> Prop} - {full_round_uncps : ∀ S C k, full_round_cps S C k = k (full_round cfg S C)} - : - full_rounds_cps cfg full_round_cps S start count k = k (full_rounds cfg S start count) := by - induction count generalizing start S with - | zero => - simp [full_rounds_cps, full_rounds, forIn, Std.Range.forIn, Std.Range.forIn.loop, Id.run] - | succ count ih => - unfold full_rounds_cps - rw [full_round_uncps, ih] - unfold full_rounds - simp [Id.run, forIn] - apply iff_to_eq - simp [Std.Range.counter_elide_fst] - rw [←zero_add (Nat.succ count), Std.Range.forIn_startSucc] - have : Nat.succ 0 = 0 + 1 := by rfl - rw [this] - have : 0 + Nat.succ count = count + 1 := by simp_arith - rw [this] - rw [←Std.Range.forIn_ixShift] - apply congrArg₂ - { simp } - funext i r - congr - funext i' - have : start + cfg.t + i * cfg.t + ↑i' = start + (i + 1) * cfg.t + ↑i' := by linarith - rw [this] - -lemma full_rounds_2_uncps - {S : Vector F 2} - {start count : Nat} - {k : Vector F 2 -> Prop}: - full_rounds_cps Constants.x5_254_2 Semaphore.fullRound_2_2 S start count k = k (full_rounds Constants.x5_254_2 S start count) := by - apply full_rounds_uncps - apply full_round_2_uncps - -lemma full_rounds_3_uncps - {S : Vector F 3} - {start count : Nat} - {k : Vector F 3 -> Prop}: - full_rounds_cps Constants.x5_254_3 Semaphore.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by - apply full_rounds_uncps - apply full_round_3_uncps - -def looped_poseidon_2 (inp : Vector F 2) (k: Vector F 2 -> Prop): Prop := - full_rounds_cps Constants.x5_254_2 Semaphore.fullRound_2_2 inp 0 4 fun state => - half_rounds_cps Constants.x5_254_2 Semaphore.halfRound_2_2 state 8 56 fun state' => - full_rounds_cps Constants.x5_254_2 Semaphore.fullRound_2_2 state' 120 4 k - -lemma fold_vec_2 {v : Vector F 2}: vec![v[0], v[1]] = v := by - conv => rhs; rw [←Vector.ofFn_get v] - -def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop := - full_rounds_cps Constants.x5_254_3 Semaphore.fullRound_3_3 inp 0 4 fun state => - half_rounds_cps Constants.x5_254_3 Semaphore.halfRound_3_3 state 12 57 fun state' => - full_rounds_cps Constants.x5_254_3 Semaphore.fullRound_3_3 state' 183 4 k - -lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by - conv => rhs; rw [←Vector.ofFn_get v] - -set_option maxRecDepth 2048 - -theorem looped_poseidon_2_go (inp : Vector F 2) (k : Vector F 2 -> Prop): - Semaphore.poseidon_2 inp k = looped_poseidon_2 inp k := by - unfold looped_poseidon_2 - unfold Semaphore.poseidon_2 - simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_2, Vector.ofFn] - rfl - -theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop): - Semaphore.poseidon_3 inp k = looped_poseidon_3 inp k := by - unfold looped_poseidon_3 - unfold Semaphore.poseidon_3 - simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_3, Vector.ofFn] - rfl - -set_option maxRecDepth 512 - -def perm_folded (cfg : Constants) (input_words : Vector cfg.F cfg.t): Vector cfg.F cfg.t := Id.run do - let R_f := cfg.R_F / 2 - let mut round_constants_counter := 0 - let mut state_words := input_words - - state_words := full_rounds cfg state_words round_constants_counter R_f - round_constants_counter := R_f * cfg.t - - state_words := partial_rounds cfg state_words round_constants_counter cfg.R_P - round_constants_counter := R_f * cfg.t + cfg.R_P * cfg.t - - state_words := full_rounds cfg state_words round_constants_counter R_f - - state_words - -theorem perm_folded_go (cfg : Constants) (input_words : Vector cfg.F cfg.t): - Poseidon.perm cfg input_words = perm_folded cfg input_words := by - unfold Poseidon.perm - unfold perm_folded - unfold full_rounds - unfold partial_rounds - simp [Id.run, forIn] - simp [Std.Range.counter_elide_fst] - cases cfg; rename_i prime t t_ne_zero R_F R_P round_constants MDS_matrix - cases t - { contradiction } - rename_i t' - simp at * - apply congrArg₂ - { - apply congrArg₂ - { - apply congrArg - funext i r - unfold full_round - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - apply congrArg - rw [Vector.setLoop_def (f := fun _ r => r ^ 5)] - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[i * Nat.succ t' + i']!)] - simp [Vector.setLoop_mapIdx, Vector.mapIdx_compose] - rw [Vector.mapIdx_mod] - } - { - funext i r - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[R_F / 2 * Nat.succ t' + i * Nat.succ t' + i']!)] - rw [Vector.setLoop_mapIdx] - apply congrArg - unfold partial_round - simp - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - rw [Vector.mapIdx_mod] - } - } - { - funext i r - apply congrArg - unfold full_round - unfold mds_matmul - simp - apply congrArg - apply congrArg - apply congrArg - rw [Vector.setLoop_def (f := fun _ r => r ^ 5)] - rw [Vector.setLoop_def (f := fun i' r => r + round_constants[R_F / 2 * Nat.succ t' + R_P * Nat.succ t' + i * Nat.succ t' + i']!)] - simp [Vector.setLoop_mapIdx, Vector.mapIdx_compose] - rw [Vector.mapIdx_mod] - } - -theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop): - Semaphore.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by - simp [ - looped_poseidon_3_go, - looped_poseidon_3, - full_rounds_uncps, - partial_rounds_3_uncps, - full_rounds_3_uncps, - perm_folded_go, - perm_folded - ] - rfl - -theorem poseidon_2_correct (inp : Vector F 2) (k : Vector F 2 -> Prop): - Semaphore.poseidon_2 inp k = k (Poseidon.perm Constants.x5_254_2 inp) := by - simp [ - looped_poseidon_2_go, - looped_poseidon_2, - full_rounds_uncps, - partial_rounds_2_uncps, - full_rounds_2_uncps, - perm_folded_go, - perm_folded - ] - rfl \ No newline at end of file diff --git a/lean-circuit/LeanCircuit/Poseidon/Spec.lean b/lean-circuit/LeanCircuit/Poseidon/Spec.lean deleted file mode 100644 index 784e646..0000000 --- a/lean-circuit/LeanCircuit/Poseidon/Spec.lean +++ /dev/null @@ -1,42 +0,0 @@ -import Mathlib -import ProvenZk -import LeanCircuit.Poseidon.Constants - -open Matrix - -namespace Poseidon - -def perm (cfg : Constants) (input_words : Vector cfg.F cfg.t): Vector cfg.F cfg.t := Id.run do - let R_f := cfg.R_F / 2 - let mut round_constants_counter := 0 - let mut state_words := input_words - for _ in [0:R_f] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - for _ in [0:cfg.R_P] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - state_words := state_words.set 0 (state_words.get 0 ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - for _ in [0:R_f] do - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i + cfg.round_constants[round_constants_counter]!) - round_constants_counter := round_constants_counter + 1 - for i in [0:cfg.t] do - state_words := state_words.set i (state_words.get i ^ 5) - state_words := (cfg.MDS_matrix ⬝ state_words.to_column).to_vector - - state_words - -theorem test_vector_correct_x5_254_3: - perm Constants.x5_254_3 vec![0,1,2] = vec![0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a, 0x0fca49b798923ab0239de1c9e7a4a9a2210312b6a2f616d18b5a87f9b628ae29, 0x0e7ae82e40091e63cbd4f16a6d16310b3729d4b6e138fcf54110e2867045a30c] := - by eq_refl - -end Poseidon \ No newline at end of file diff --git a/lean-circuit/LeanCircuit/SemanticEquivalence.lean b/lean-circuit/LeanCircuit/SemanticEquivalence.lean index e14755d..8a15d37 100644 --- a/lean-circuit/LeanCircuit/SemanticEquivalence.lean +++ b/lean-circuit/LeanCircuit/SemanticEquivalence.lean @@ -3,72 +3,75 @@ import ProvenZk.Hash import ProvenZk.Merkle import LeanCircuit -import LeanCircuit.Poseidon.Spec -import LeanCircuit.Poseidon.Correctness +import LeanCircuit.Poseidon +-- import LeanCircuit.Poseidon.Spec +-- import LeanCircuit.Poseidon.Correctness open Semaphore (F Order) variable [Fact (Nat.Prime Order)] -abbrev D := 20 +-- abbrev D := 20 -def embed_dir : Dir -> F - | x => Dir.toZMod x +-- def embed_dir : Dir -> F +-- | x => Dir.toZMod x -def embed_dir_vector {depth} (ix: Vector Dir depth) : Vector F depth := - Vector.map embed_dir ix +-- def embed_dir_vector {depth} (ix: Vector Dir depth) : Vector F depth := +-- Vector.map embed_dir ix -lemma dir_embed_recover {d : Dir} : Dir.nat_to_dir (embed_dir d).val = d := by - cases d <;> rfl +-- lemma dir_embed_recover {d : Dir} : Dir.nat_to_dir (embed_dir d).val = d := by +-- cases d <;> rfl -@[simp] -lemma dir_embed_recover_vector {depth} (ix: Vector Dir depth) : - Dir.create_dir_vec (embed_dir_vector ix) = ix := by - simp [Dir.create_dir_vec, embed_dir_vector, dir_embed_recover] - apply Vector.eq - simp +-- @[simp] +-- lemma dir_embed_recover_vector {depth} (ix: Vector Dir depth) : +-- Dir.create_dir_vec (embed_dir_vector ix) = ix := by +-- simp [Dir.create_dir_vec, embed_dir_vector, dir_embed_recover] +-- apply Vector.eq +-- simp -@[simp] -lemma embed_dir_vector_reverse {depth} (ix : Vector Dir depth) : - embed_dir_vector ix.reverse = (embed_dir_vector ix).reverse := by - simp [embed_dir_vector] - apply Vector.eq - simp [Vector.toList_reverse, List.map_reverse] +-- @[simp] +-- lemma embed_dir_vector_reverse {depth} (ix : Vector Dir depth) : +-- embed_dir_vector ix.reverse = (embed_dir_vector ix).reverse := by +-- simp [embed_dir_vector] +-- apply Vector.eq +-- simp [Vector.toList_reverse, List.map_reverse] -lemma embed_dir_vector_is_binary {depth} (ix : Vector Dir depth) : - is_vector_binary (embed_dir_vector ix) := by - simp [is_vector_binary, embed_dir_vector] - induction ix using Vector.inductionOn with - | h_nil => simp [is_vector_binary] - | @h_cons n d ds ih => - simp [is_vector_binary_cons] - apply And.intro - { simp [embed_dir, is_bit]; cases d <;> simp } - { assumption } +-- lemma embed_dir_vector_is_binary {depth} (ix : Vector Dir depth) : +-- is_vector_binary (embed_dir_vector ix) := by +-- simp [is_vector_binary, embed_dir_vector] +-- induction ix using Vector.inductionOn with +-- | h_nil => simp [is_vector_binary] +-- | @h_cons n d ds ih => +-- simp [is_vector_binary_cons] +-- apply And.intro +-- { simp [embed_dir, is_bit]; cases d <;> simp } +-- { assumption } -def poseidon₁ : Hash F 1 := fun a => (Poseidon.perm Constants.x5_254_2 vec![0, a.get 0]).get 0 +-- def poseidon₁ : Hash F 1 := fun a => (Poseidon.perm Constants.x5_254_2 vec![0, a.get 0]).get 0 -lemma Poseidon1_uncps (a : F) (k : F -> Prop) : Semaphore.Poseidon1 a k ↔ k (poseidon₁ vec![a]) := by - simp [Semaphore.Poseidon1, poseidon₁, poseidon_2_correct, getElem] +-- lemma Poseidon1_uncps (a : F) (k : F -> Prop) : Semaphore.Poseidon1 a k ↔ k (poseidon₁ vec![a]) := by +-- simp [Semaphore.Poseidon1, poseidon₁, poseidon_2_correct, getElem] -def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0 +-- def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0 -lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : Semaphore.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by - simp [Semaphore.Poseidon2, poseidon₂, poseidon_3_correct, getElem] - rfl +-- lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : Semaphore.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by +-- simp [Semaphore.Poseidon2, poseidon₂, poseidon_3_correct, getElem] +-- rfl + +def hashLevel (d : Bool) (h s : F): F := match d with + | false => poseidon₂ (vec![h, s]) + | true => poseidon₂ (vec![s, h]) + +lemma MerkleTreeRecoverRound_uncps {dir: Bool} {hash sibling : F} {k : F -> Prop}: + Semaphore.MerkleTreeRecoverRound dir.toZMod hash sibling k ↔ + k (hashLevel dir hash sibling) := by + cases dir <;> + simp [Semaphore.MerkleTreeRecoverRound, Gates.is_bool, hashLevel, Poseidon2_uncps, Poseidon2_uncps] -lemma MerkleTreeRecoverRound_uncps {dir hash sibling : F} {k : F -> Prop}: - Semaphore.MerkleTreeRecoverRound dir hash sibling k ↔ - is_bit dir ∧ k (match Dir.nat_to_dir dir.val with - | Dir.left => poseidon₂ vec![hash, sibling] - | Dir.right => poseidon₂ vec![sibling, hash]) := by - simp [Semaphore.MerkleTreeRecoverRound, Gates.is_bool] - intro hb - rw [Poseidon2_uncps, Poseidon2_uncps] - cases hb <;> { - simp [*, Gates.select, Gates.is_bool, Dir.nat_to_dir] - try rfl - } +lemma MerkleTreeRecoverRound_bool {dir: F} {hash sibling : F} {k : F -> Prop}: + Semaphore.MerkleTreeRecoverRound dir hash sibling k → is_bit dir := by + simp [Semaphore.MerkleTreeRecoverRound] + intros; assumption def merkle_tree_recover_rounds (Leaf : F) (PathIndices Siblings : Vector F n) (k : F -> Prop) : Prop := match n with @@ -78,19 +81,19 @@ def merkle_tree_recover_rounds (Leaf : F) (PathIndices Siblings : Vector F n) (k lemma merkle_tree_recover_rounds_uncps {Leaf : F} - {PathIndices Siblings : Vector F n} + {PathIndices : Vector Bool n} + {Siblings : Vector F n} {k : F -> Prop}: - merkle_tree_recover_rounds Leaf PathIndices Siblings k ↔ - is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings Leaf) := by + merkle_tree_recover_rounds Leaf (Vector.map Bool.toZMod PathIndices) Siblings k ↔ + k (MerkleTree.recover poseidon₂ PathIndices.reverse Siblings.reverse Leaf) := by induction PathIndices, Siblings using Vector.inductionOn₂ generalizing Leaf with | nil => simp [is_vector_binary] rfl | @cons n ix sib ixes sibs ih => - simp [MerkleTree.recover_tail_reverse_equals_recover, MerkleTree.recover_tail, merkle_tree_recover_rounds] + simp [merkle_tree_recover_rounds] simp [MerkleTreeRecoverRound_uncps, is_vector_binary_cons, and_assoc, ih] - intros - rfl + cases ix <;> simp [MerkleTree.recover_snoc, hashLevel] lemma MerkleTreeInclusionProof_looped (Leaf: F) (PathIndices: Vector F D) (Siblings: Vector F D) (k: F -> Prop): Semaphore.MerkleTreeInclusionProof_20_20 Leaf PathIndices Siblings k = @@ -101,9 +104,13 @@ lemma MerkleTreeInclusionProof_looped (Leaf: F) (PathIndices: Vector F D) (Sibli rw [←Vector.ofFn_get (v := Siblings)] rfl -lemma MerkleTreeInclusionProof_20_20_uncps {Leaf : F} {PathIndices Siblings : Vector F D} {k : F -> Prop}: - Semaphore.MerkleTreeInclusionProof_20_20 Leaf PathIndices Siblings k ↔ - is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings Leaf) := by +lemma MerkleTreeInclusionProof_20_20_uncps + {Leaf : F} + {PathIndices : Vector Bool D} + {Siblings : Vector F D} + {k : F -> Prop} : + Semaphore.MerkleTreeInclusionProof_20_20 Leaf (Vector.map Bool.toZMod PathIndices) Siblings k ↔ + k (MerkleTree.recover poseidon₂ PathIndices.reverse Siblings.reverse Leaf) := by simp [MerkleTreeInclusionProof_looped, merkle_tree_recover_rounds_uncps] abbrev secret (IdentityNullifier: F) (IdentityTrapdoor: F) : F := @@ -115,13 +122,12 @@ abbrev identity_commitment (IdentityNullifier: F) (IdentityTrapdoor: F) : F := abbrev nullifier_hash (ExternalNullifier: F) (IdentityNullifier: F) : F := poseidon₂ vec![ExternalNullifier, IdentityNullifier] -def circuit_sem (IdentityNullifier IdentityTrapdoor ExternalNullifier NullifierHash Root: F) (Path Proof: Vector F D): Prop := +def circuit_sem (IdentityNullifier IdentityTrapdoor ExternalNullifier NullifierHash Root: F) (Path: Vector Bool D) (Proof: Vector F D): Prop := NullifierHash = nullifier_hash ExternalNullifier IdentityNullifier ∧ - is_vector_binary Path ∧ - MerkleTree.recover poseidon₂ (Dir.create_dir_vec Path).reverse Proof.reverse (identity_commitment IdentityNullifier IdentityTrapdoor) = Root + MerkleTree.recover poseidon₂ Path.reverse Proof.reverse (identity_commitment IdentityNullifier IdentityTrapdoor) = Root -theorem circuit_semantics {IdentityNullifier IdentityTrapdoor SignalHash ExternalNullifier NullifierHash Root: F} {Path Proof: Vector F D}: - Semaphore.circuit IdentityNullifier IdentityTrapdoor Path Proof SignalHash ExternalNullifier NullifierHash Root ↔ +theorem circuit_semantics_bool {IdentityNullifier IdentityTrapdoor SignalHash ExternalNullifier NullifierHash Root: F} {Path: Vector Bool D} {Proof: Vector F D}: + Semaphore.circuit IdentityNullifier IdentityTrapdoor (Vector.map Bool.toZMod Path) Proof SignalHash ExternalNullifier NullifierHash Root ↔ circuit_sem IdentityNullifier IdentityTrapdoor ExternalNullifier NullifierHash Root Path Proof := by simp [ circuit_sem, @@ -130,32 +136,17 @@ theorem circuit_semantics {IdentityNullifier IdentityTrapdoor SignalHash Externa Poseidon1_uncps, MerkleTreeInclusionProof_20_20_uncps, Gates.eq, - nullifier_hash, - Dir.create_dir_vec, - ←MerkleTree.recover_tail_reverse_equals_recover + nullifier_hash ] + intro apply Iff.intro - case mp => - intros - casesm* (_ ∧ _) - rw [←Vector.ofFn_get (v := Path)] - rw [←Vector.ofFn_get (v := Proof)] - subst_vars - apply And.intro - {rfl} - apply And.intro - {assumption} - {rfl} - case mpr => - intro h - cases h; rename_i h₁ h₂ - cases h₂; rename_i h₂ h₃ - rw [←Vector.ofFn_get (v := Path)] at h₂ - rw [←Vector.ofFn_get (v := Path)] at h₃ - rw [←Vector.ofFn_get (v := Proof)] at h₃ - subst_vars - apply And.intro - {rfl} - apply And.intro - assumption - {rfl} \ No newline at end of file + repeat ( + intro h; simp [h] + ) + +theorem circuit_semantics {IdentityNullifier IdentityTrapdoor SignalHash ExternalNullifier NullifierHash Root: F} {Path Proof: Vector F D}: + (is_vector_binary Path ∧ ∃x : Vector Bool D, Path = x.map Bool.toZMod) → + (Semaphore.circuit IdentityNullifier IdentityTrapdoor (Vector.map Bool.toZMod x) Proof SignalHash ExternalNullifier NullifierHash Root ↔ + circuit_sem IdentityNullifier IdentityTrapdoor ExternalNullifier NullifierHash Root x Proof) := by + intro + apply circuit_semantics_bool diff --git a/lean-circuit/Main.lean b/lean-circuit/Main.lean index f13ba2c..d3f1cbb 100644 --- a/lean-circuit/Main.lean +++ b/lean-circuit/Main.lean @@ -10,52 +10,58 @@ open Semaphore (F Order) variable [Fact (Nat.Prime Order)] theorem always_possible_to_signal + [Fact (CollisionResistant poseidon₂)] (IdentityNullifier IdentityTrapdoor SignalHash ExtNullifier : F) (Tree : MerkleTree F poseidon₂ 20) - (Path : Vector Dir 20) - (commitment_in_tree : Tree.item_at Path = identity_commitment IdentityNullifier IdentityTrapdoor) + (Path : Vector Bool 20) + (commitment_in_tree : Tree.itemAt Path = identity_commitment IdentityNullifier IdentityTrapdoor) : Semaphore.circuit IdentityNullifier IdentityTrapdoor - (embed_dir_vector Path.reverse) + (Vector.map Bool.toZMod Path.reverse) (Tree.proof Path).reverse SignalHash ExtNullifier (nullifier_hash ExtNullifier IdentityNullifier) Tree.root := by - rw [circuit_semantics, ←MerkleTree.recover_proof_is_root, commitment_in_tree] - simp [circuit_sem] - apply embed_dir_vector_is_binary + simp [circuit_semantics_bool, circuit_sem] + rw [←commitment_in_tree] theorem signaller_is_in_tree + [Fact (CollisionResistant poseidon₂)] (IdentityNullifier IdentityTrapdoor SignalHash ExtNullifier NullifierHash : F) (Tree : MerkleTree F poseidon₂ 20) (Path Proof: Vector F 20) - [Fact (perfect_hash poseidon₂)] : - Semaphore.circuit IdentityNullifier IdentityTrapdoor Path Proof SignalHash ExtNullifier NullifierHash Tree.root → - Tree.item_at (Dir.create_dir_vec Path.reverse) = identity_commitment IdentityNullifier IdentityTrapdoor := by - simp [circuit_semantics, circuit_sem] - intros - apply MerkleTree.proof_ceritfies_item - assumption + (is_vector_binary Path ∧ ∃x : Vector Bool D, Path = x.map Bool.toZMod) → + Semaphore.circuit IdentityNullifier IdentityTrapdoor (Vector.map Bool.toZMod x) Proof SignalHash ExtNullifier NullifierHash Tree.root → + Tree.itemAt (Vector.reverse x) = identity_commitment IdentityNullifier IdentityTrapdoor := by + intro hbin + simp [circuit_semantics_bool] + intros h + simp [circuit_sem] at h + casesm* (_ ∧ _) + rename_i h + simp [h] theorem no_double_signal_with_same_commitment + [Fact (CollisionResistant poseidon₁)] + [Fact (CollisionResistant poseidon₂)] (IdentityNullifier₁ IdentityNullifier₂ IdentityTrapdoor₁ IdentityTrapdoor₂ SignalHash₁ SignalHash₂ ExtNullifier₁ ExtNullifier₂ NullifierHash₁ NullifierHash₂ Root₁ Root₂ : F) (Path₁ Proof₁ Path₂ Proof₂: Vector F 20) - [Fact (perfect_hash poseidon₁)] - [Fact (perfect_hash poseidon₂)] : - Semaphore.circuit IdentityNullifier₁ IdentityTrapdoor₁ Path₁ Proof₁ SignalHash₁ ExtNullifier₁ NullifierHash₁ Root₁ → - Semaphore.circuit IdentityNullifier₂ IdentityTrapdoor₂ Path₂ Proof₂ SignalHash₂ ExtNullifier₂ NullifierHash₂ Root₂ → + (is_vector_binary Path₁ ∧ ∃x₁ : Vector Bool D, Path₁ = x₁.map Bool.toZMod) → + (is_vector_binary Path₂ ∧ ∃x₂ : Vector Bool D, Path₂ = x₂.map Bool.toZMod) → + Semaphore.circuit IdentityNullifier₁ IdentityTrapdoor₁ (Vector.map Bool.toZMod x₁) Proof₁ SignalHash₁ ExtNullifier₁ NullifierHash₁ Root₁ → + Semaphore.circuit IdentityNullifier₂ IdentityTrapdoor₂ (Vector.map Bool.toZMod x₂) Proof₂ SignalHash₂ ExtNullifier₂ NullifierHash₂ Root₂ → ExtNullifier₁ = ExtNullifier₂ → identity_commitment IdentityNullifier₁ IdentityTrapdoor₁ = identity_commitment IdentityNullifier₂ IdentityTrapdoor₂ → NullifierHash₁ = NullifierHash₂ := by - simp [circuit_semantics, circuit_sem, secret, Vector.eq_cons_iff] + simp [circuit_semantics_bool, circuit_sem, secret, Vector.eq_cons_iff] intros subst_vars rfl -def main : IO Unit := pure () \ No newline at end of file +def main : IO Unit := pure () diff --git a/lean-circuit/lake-manifest.json b/lean-circuit/lake-manifest.json index 144219f..e2c9d69 100644 --- a/lean-circuit/lake-manifest.json +++ b/lean-circuit/lake-manifest.json @@ -16,15 +16,15 @@ {"git": {"url": "https://github.com/reilabs/proven-zk.git", "subDir?": null, - "rev": "08431b93eeef80f6acbf3d6a6401c02d849f6864", + "rev": "ae9327ec14d84b20f1c17f336ed7698e5b0fbae1", "name": "ProvenZK", - "inputRev?": "v1.0.0"}}, + "inputRev?": "v1.3.0"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "ea67efc21e4e1496f0a1d954cd0c0a952523133a", + "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9", "name": "mathlib", - "inputRev?": "ea67efc21e4e1496f0a1d954cd0c0a952523133a"}}, + "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lean-circuit/lakefile.lean b/lean-circuit/lakefile.lean index a468f67..a6073fd 100644 --- a/lean-circuit/lakefile.lean +++ b/lean-circuit/lakefile.lean @@ -6,17 +6,18 @@ package «lean-circuit» { } require mathlib from git - "https://github.com/leanprover-community/mathlib4.git"@"ea67efc21e4e1496f0a1d954cd0c0a952523133a" + "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9" require ProvenZK from git - "https://github.com/reilabs/proven-zk.git"@"v1.0.0" + "https://github.com/reilabs/proven-zk.git"@"v1.3.0" lean_lib LeanCircuit { + moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"] -- add library configuration options here } @[default_target] lean_exe «lean-circuit» { - moreLeanArgs := #["--tstack=1000000"] + moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"] root := `Main }