Skip to content

mukeshtiwari/Formally_Verified_Verifiable_Group_Generator

Repository files navigation

Coq Installation Instruction

See the file Coq_Installation.md.

Formally Verified Verifiable Group Generation

Repo for verifiable generation of group generators.

Run 'make' in _CoqProject directory to compute generators and 'make clean' to clean everything. 'make' will produce output shown below:

coq_makefile -f _CoqProject -o CoqMakefile
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f CoqMakefile 
COQDEP VFILES
COQC src/Sha256.v
Finished transaction in 0.047 secs (0.047u,0.s) (successful)
Finished transaction in 0.027 secs (0.027u,0.s) (successful)
Finished transaction in 0.057 secs (0.057u,0.s) (successful)
Finished transaction in 0.06 secs (0.06u,0.s) (successful)
COQC src/Bytestring.v
COQC src/Functions.v
COQC src/Fermat.v
COQC src/Domainpar.v
COQC src/Generator_1.v
Finished transaction in 51.48 secs (51.393u,0.088s) (successful)
     = genr.Valid
         138454106708200479055735335430888877165820506315681808529812588774891294266745965935843260905810124292112533861018873505541666292973867778507479111324012276358327291576815142910454131034197568218833096994765060449736987726137450505727390912803873697812682423871774182713509275008471752297521355610521695631738
     : genr.Tag
Finished transaction in 0.083 secs (0.083u,0.s) (successful)
     = true
     : bool
Finished transaction in 63.875 secs (63.792u,0.084s) (successful)
COQC src/Generator_2.v
Finished transaction in 51.361 secs (51.249u,0.078s) (successful)
     = genr.Valid
         102469831306215617781528906572847226693904307485739300130034645449135192789390308052087414564151228873441394591233561760912933102036228956601258949517417972024163761928741329990676466410461313046468961302321734855374139857073309659521504765942247678350704168525388693094421920249884964626193856064170107448094
     : genr.Tag
Finished transaction in 0.083 secs (0.083u,0.s) (successful)
     = true
     : bool
Finished transaction in 64.447 secs (63.943u,0.447s) (successful)
COQC src/Generator_3.v
Finished transaction in 51.082 secs (50.757u,0.313s) (successful)
     = genr.Valid
         88263658766223357461869144483248908802431230135321993360469791817434515043095308104988988885613316192808653647560362493809139862324204760674673830428720363991237057673925805011298607088991781235425078687556099730304327702471847840027357950827996311819356543334664389981253439309485633438223355769536120472886
     : genr.Tag
Finished transaction in 0.082 secs (0.082u,0.s) (successful)
     = true
     : bool
Finished transaction in 63.961 secs (63.544u,0.377s) (successful)
COQC src/Generator_4.v
Finished transaction in 416.781 secs (415.863u,0.883s) (successful)
     = genr.Valid
         16779584886618334955777146143805151742756109597848073032897659526710040302176218585670602669216587991633935024592787306349889100902129684576531517671064338120830768458737964024941626899266181419534731022507702381832220695652481201002313417792528591777912496057497664476810455186127730777145720725703338677122474655371704794416925100215075257492292453624627321349273605377338405654300066568869264460444035900045343943151207471750966197679881151399230919361519925420099999305148035925485570132525240424489924786140236333173248767301480930310664404386723788396232966052596334360090754073589039580595341483241910869439850
     : genr.Tag
Finished transaction in 0.323 secs (0.322u,0.001s) (successful)
     = true
     : bool
Finished transaction in 488.913 secs (488.178u,0.684s) (successful)
COQC src/Generator_5.v
Finished transaction in 413.334 secs (412.819u,0.517s) (successful)
     = genr.Valid
         7397663020529711748206327096495171056013349351297608836944581506776048299910727642018586975845411776739383886069050283668821048481626107184005913661785643385036737596310220141611324379597898168338084415315514945719018373740779993806917733907530535236684877616590789694426081749803454970748757282080960157265510732047192013417745603316937655021638539157108532588624321791236022232330371996545235390513598460611657625080679893233973467700124099006756332896043933323158170849561410748839052823646886645648103667336693441857536896810350359149834341507095181106437695481549438875894694601062306932502363245043364720122144
     : genr.Tag
Finished transaction in 0.322 secs (0.321u,0.001s) (successful)
     = true
     : bool
Finished transaction in 485.221 secs (484.627u,0.572s) (successful)
COQC src/Generator_6.v
Finished transaction in 417.792 secs (417.312u,0.484s) (successful)
     = genr.Valid
         17000091980252583428757806982638937856245893569533792216699813468191566634688128634050776893335947220947031435842901649795772466193775260976330643619179865466997471285306413279441538541328081656290102268160274755294414079471402076954782591372589274675093571750842213809016165031347652847970867397746301688224983069772073832490178172576260017477008355450432674058720853288885702484954444657071164813330071988886337091404537365227283011682049166650944586632286313933806893049897200661578473701190683228555851424768513111930423324951216677475160773117624980727524747216080485677785692737362530025677011447036821713540195
     : genr.Tag
Finished transaction in 0.32 secs (0.319u,0.s) (successful)
     = true
     : bool
Finished transaction in 495.599 secs (492.449u,2.686s) (successful)
COQC src/Generator_7.v
Finished transaction in 405.835 secs (405.245u,0.573s) (successful)
     = genr.Valid
         19505007897628087214258470741983733303993129606909771160933535007624517213905478669883399507508368338521633288116655756851871582957570975665522208849109692771478416189849647516623601185277096525404613089202268761028314488416628441521995648895965894383947550057509046815947139230214991308459417898812040648095362629463239815796837419841946171750790842682733367933794859041951588095792472952772187723597083481033010341517250868974535354067787123216189678903435534409554938991048675677096549033814900474097699209573422225276935134621669497733391117821219447658975257788692574807159800602790330174406663975472198869382895
     : genr.Tag
Finished transaction in 0.321 secs (0.32u,0.s) (successful)
     = true
     : bool
Finished transaction in 487.974 secs (487.221u,0.744s) (successful)
COQC src/Generator_8.v
Finished transaction in 410.604 secs (410.136u,0.47s) (successful)
     = genr.Valid
         30827113638062155707616269302531551119452708162605460531443522853399265094233230090236106474498610375088818881076937033907305380556951808525873535920749157105046303837536400957943237319508356497271947437278408440860865578536217653463247439380042444965023833640988275702519504511399551304181130117912437679538658396981265574932497402871300874163564126307709025599418598053644899380489152058952873644130199699802630122529043373387575803101121529968419553822680328682440160187107789650220640886602154339302225594385286571930972897568894793232717531235783992916417706832642343335576285265690498010286215611726811463907643
     : genr.Tag
Finished transaction in 0.321 secs (0.32u,0.001s) (successful)
     = true
     : bool
Finished transaction in 492.23 secs (491.645u,0.572s) (successful)
COQC src/Generator_9.v
Finished transaction in 405.737 secs (405.263u,0.476s) (successful)
     = genr.Valid
         16686255796188270469452539079851735482599464970095728845376833175044739122871243427199534360628114649000541180209352807279464906205869949161498141911328904969470630729113553098750547922591310704595028004997153534924113212998484168331949285437631969721323791545627286096124025385227828302583519400718140112333266887611575180549759041245944334854043622278279872761414635392575968374689231799056303753969701579382272273478745221727429281144967043356266411949754822424536441553774980090741788351724931604116702476051827592394461684697135364574264113516123841060846295360996479772006006264947007196630074887221145679917094
     : genr.Tag
Finished transaction in 0.32 secs (0.319u,0.s) (successful)
     = true
     : bool
Finished transaction in 488.461 secs (487.889u,0.573s) (successful)
COQC src/Generator_10.v
Finished transaction in 1405.595 secs (1403.775u,1.768s) (successful)
     = genr.Valid
         4287387900415874329539416709976769266459844797692946850755415061049853969319540434254000367372908561163305788123715331746181952931541577688878686605993064449816575775307400434277728575572844256140961810807167967475008910118050149173691595814863249029683210571233391135692095930504883097353773675029750447458648565889607516441739549398590419378630385561755690018707618481919584673291517946074890885633559908927469486214697952958610772113903851819749942559038101483475130120011622816821220963461713750348003626557633182785359819145157202281708787559969804326599766245155181476364432107381838847593953877465069492847591267620616534670348397979155312950958449441222674271271613478097938270718517831996227760019288273525360891505079303702445984462284560738211594759025717202810336102260198678784414582391155551558673657742352410700356853958784720389419009118656191948454137538595843290747283916485507903283505003679857626459847957
     : genr.Tag
Finished transaction in 0.741 secs (0.74u,0.s) (successful)
     = true
     : bool
Finished transaction in 1589.213 secs (1587.26u,1.901s) (successful)
COQC src/Generator_11.v
Finished transaction in 1404.323 secs (1402.608u,1.702s) (successful)
     = genr.Valid
         2815857067680651424347728195758246993191714291494761217484085964025213854469287867033561128449900900542462959417353120442070851755032021214983970103765146890716305532795232886202363258275657863077915583611655753362163656499220264084336345455815303397349442140403382571439497917600111644650834845541746126249643813462066176659367193455120967628954142480075772577080948417949213511906413145103570460433944152933121864621552213123281686253383669446690860954251216167486044861167685492759490205462427228551444743543073926251592860014822346807308315112641756207739293679496794973286349904658615276240292724715580842054385093926991100921590637938925586397890638618258362890968509121690608946555141641898453203613149349214698377732472649750557446967482753177687967393915835032845286305409022430101066346395788534519697210466132849239485539531264233037800600251881786274602063793159587693118604019689435792492692309345753911927683445
     : genr.Tag
Finished transaction in 0.739 secs (0.738u,0.s) (successful)
     = true
     : bool
Finished transaction in 1584.587 secs (1582.653u,1.892s) (successful)
COQC src/Generator_12.v
Finished transaction in 1417.487 secs (1415.836u,1.591s) (successful)
     = genr.Valid
         5142269046611298751053334471712018380952381659994149061069643310780863411117756830385169625171306902268731945265611175832982085711414921325430792621067001642054430322541316695452318115167970016625546426097672467620839422473921709026039725510992923909031023192174059668984872166791847785098121010517945765446961570007177822942898941331888153276962092525360573272974634978013864168046512739478574948414329466141821447534309755925230066981468451347043551719324995849899067726237010049836515585927730058820192474169847466483361570985526862054236113750881396542483192524341448209408531022129289703356623973794545446814225059247328981961060656844942121203760003864474654437004736370165730970677136513883966628087789535547496889264530799006158784007444380513118730444715144564668024953057128445187848415738918976578866440346949147032367775690198477927956647715787727147792313887321249651999990491718645651559760096877183540600160369
     : genr.Tag
Finished transaction in 0.736 secs (0.735u,0.s) (successful)
     = true
     : bool
Finished transaction in 1601.835 secs (1600.034u,1.772s) (successful)

About

Repo for computing group generators in publicly verifiable manner.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages