123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185typeerror=[|`Invalid_format|`Invalid_length|`Invalid_range|`Not_on_curve|`At_infinity|`Low_order]leterror_to_string=function|`Invalid_format->"invalid format"|`Not_on_curve->"point is not on curve"|`At_infinity->"point is at infinity"|`Invalid_length->"invalid length"|`Invalid_range->"invalid range"|`Low_order->"low order"letpp_errorfmte=Format.fprintffmt"Cannot parse point: %s"(error_to_stringe)letrev_stringbuf=letlen=String.lengthbufinletres=Bytes.makelen'\000'infori=0tolen-1doBytes.setres(len-1-i)(String.getbufi)done;Bytes.unsafe_to_stringresexceptionMessage_too_longletstring_get_uint8bufidx=(* TODO: use String.get_uint8 when mirage-crypto-ec requires OCaml >= 4.13 *)Bytes.get_uint8(Bytes.unsafe_of_stringbuf)idxletbit_atbufi=letbyte_num=i/8inletbit_num=imod8inletbyte=string_get_uint8bufbyte_numinbyteland(1lslbit_num)<>0moduletypeDh=sigtypesecretvalsecret_of_cs:?compress:bool->Cstruct.t->(secret*Cstruct.t,error)resultvalgen_key:?compress:bool->?g:Mirage_crypto_rng.g->unit->secret*Cstruct.tvalkey_exchange:secret->Cstruct.t->(Cstruct.t,error)resultendmoduletypeDsa=sigtypeprivtypepubvalbyte_length:intvalpriv_of_cstruct:Cstruct.t->(priv,error)resultvalpriv_to_cstruct:priv->Cstruct.tvalpub_of_cstruct:Cstruct.t->(pub,error)resultvalpub_to_cstruct:?compress:bool->pub->Cstruct.tvalpub_of_priv:priv->pubvalgenerate:?g:Mirage_crypto_rng.g->unit->priv*pubvalsign:key:priv->?k:Cstruct.t->Cstruct.t->Cstruct.t*Cstruct.tvalverify:key:pub->Cstruct.t*Cstruct.t->Cstruct.t->boolmoduleK_gen(H:Mirage_crypto.Hash.S):sigvalgenerate:key:priv->Cstruct.t->Cstruct.tendmodulePrecompute:sigvalgenerator_tables:unit->stringarrayarrayarrayendendmoduletypeDh_dsa=sigmoduleDh:DhmoduleDsa:Dsaendtypefield_element=stringtypeout_field_element=bytesmoduletypeParameters=sigvala:field_elementvalb:field_elementvalg_x:field_elementvalg_y:field_elementvalp:field_elementvaln:field_elementvalpident:stringvalbyte_length:intvalfe_length:intvalfirst_byte_bits:intoptionendtypepoint={f_x:field_element;f_y:field_element;f_z:field_element}typeout_point={m_f_x:out_field_element;m_f_y:out_field_element;m_f_z:out_field_element}typescalar=ScalarofstringmoduletypeForeign=sigvalmul:out_field_element->field_element->field_element->unitvalsub:out_field_element->field_element->field_element->unitvaladd:out_field_element->field_element->field_element->unitvalto_montgomery:out_field_element->field_element->unitvalfrom_octets:out_field_element->string->unitvalset_one:out_field_element->unitvalnz:field_element->boolvalsqr:out_field_element->field_element->unitvalfrom_montgomery:out_field_element->field_element->unitvalto_octets:bytes->field_element->unitvalinv:out_field_element->field_element->unitvalselect_c:out_field_element->bool->field_element->field_element->unitvaldouble_c:out_point->point->unitvaladd_c:out_point->point->point->unitvalscalar_mult_base_c:out_point->string->unitendmoduletypeField_element=sigvalmul:field_element->field_element->field_elementvalsub:field_element->field_element->field_elementvaladd:field_element->field_element->field_elementvalfrom_montgomery:field_element->field_elementvalzero:field_elementvalone:field_elementvalnz:field_element->boolvalsqr:field_element->field_elementvalinv:field_element->field_elementvalselect:bool->then_:field_element->else_:field_element->field_elementvalfrom_be_octets:string->field_elementvalto_octets:field_element->stringvaldouble_point:point->pointvaladd_point:point->point->pointvalscalar_mult_base_point:scalar->pointendmoduleMake_field_element(P:Parameters)(F:Foreign):Field_element=structletb_utsb=Bytes.unsafe_to_stringbletcreate()=Bytes.makeP.fe_length'\000'letmulab=lettmp=create()inF.multmpab;b_utstmpletsubab=lettmp=create()inF.subtmpab;b_utstmpletaddab=lettmp=create()inF.addtmpab;b_utstmpletfrom_montgomerya=lettmp=create()inF.from_montgomerytmpa;b_utstmpletzero=b_uts(create())letone=letfe=create()inF.set_onefe;b_utsfeletnza=F.nzaletsqra=lettmp=create()inF.sqrtmpa;b_utstmpletinva=lettmp=create()inF.invtmpa;b_utstmpletselectbit~then_~else_=lettmp=create()inF.select_ctmpbitthen_else_;b_utstmpletfrom_be_octetsbuf=letbuf_rev=rev_stringbufinlettmp=create()inF.from_octetstmpbuf_rev;F.to_montgomerytmp(b_utstmp);b_utstmpletcreate_octets()=Bytes.makeP.byte_length'\000'letto_octetsfe=lettmp=create_octets()inF.to_octetstmpfe;b_utstmpletout_point()={m_f_x=create();m_f_y=create();m_f_z=create();}letout_p_to_pp={f_x=b_utsp.m_f_x;f_y=b_utsp.m_f_y;f_z=b_utsp.m_f_z;}letdouble_pointp=lettmp=out_point()inF.double_ctmpp;out_p_to_ptmpletadd_pointab=lettmp=out_point()inF.add_ctmpab;out_p_to_ptmpletscalar_mult_base_point(Scalard)=lettmp=out_point()inF.scalar_mult_base_ctmpd;out_p_to_ptmpendmoduletypePoint=sigvalat_infinity:unit->pointvalis_infinity:point->boolvaladd:point->point->pointvaldouble:point->pointvalof_octets:string->(point,error)resultvalto_octets:compress:bool->point->stringvalto_affine_raw:point->(field_element*field_element)optionvalx_of_finite_point:point->stringvalparams_g:pointvalselect:bool->then_:point->else_:point->pointvalscalar_mult_base:scalar->pointendmoduleMake_point(P:Parameters)(F:Foreign):Point=structmoduleFe=Make_field_element(P)(F)letat_infinity()=letf_x=Fe.oneinletf_y=Fe.oneinletf_z=Fe.zeroin{f_x;f_y;f_z}letis_infinity(p:point)=not(Fe.nzp.f_z)letis_solution_to_curve_equation=leta=Fe.from_be_octetsP.ainletb=Fe.from_be_octetsP.binfun~x~y->letx3=Fe.mulxxinletx3=Fe.mulx3xinletax=Fe.mulaxinlety2=Fe.mulyyinletsum=Fe.addx3axinletsum=Fe.addsumbinletsum=Fe.subsumy2innot(Fe.nzsum)letcheck_coordinatebuf=(* ensure buf < p: *)matchEqaf.compare_be_with_len~len:P.byte_lengthbufP.p>=0with|true->None|exceptionInvalid_argument_->None|false->Some(Fe.from_be_octetsbuf)(** Convert cstruct coordinates to a finite point ensuring:
- x < p
- y < p
- y^2 = ax^3 + ax + b
*)letvalidate_finite_point~x~y=match(check_coordinatex,check_coordinatey)with|Somef_x,Somef_y->ifis_solution_to_curve_equation~x:f_x~y:f_ythenletf_z=Fe.oneinOk{f_x;f_y;f_z}elseError`Not_on_curve|_->Error`Invalid_rangeletto_affine_rawp=ifis_infinitypthenNoneelseletz1=Fe.from_montgomeryp.f_zinletz2=Fe.invz1inletz1=Fe.sqrz2inletz1=Fe.from_montgomeryz1inletx=Fe.mulp.f_xz1inletz1=Fe.mulz1z2inlety=Fe.mulp.f_yz1inSome(x,y)letto_affinep=Option.map(fun(x,y)->Fe.to_octetsx,Fe.to_octetsy)(to_affine_rawp)letto_octets~compressp=letbuf=matchto_affinepwith|None->String.make1'\000'|Some(x,y)->letlen_x=String.lengthxandlen_y=String.lengthyinletres=Bytes.make(1+len_x+len_y)'\000'inBytes.setres0'\004';letrev_x=rev_stringxandrev_y=rev_stringyinBytes.blit_stringrev_x0res1len_x;Bytes.blit_stringrev_y0res(1+len_x)len_y;Bytes.unsafe_to_stringresinifcompressthenletout=Bytes.make(P.byte_length+1)'\000'inletident=2+(string_get_uint8buf((P.byte_length*2)-1))land1inBytes.blit_stringbuf1out1P.byte_length;Bytes.set_uint8out0ident;Bytes.unsafe_to_stringoutelsebufletdoublep=Fe.double_pointpletaddpq=Fe.add_pointpqletx_of_finite_pointp=matchto_affinepwithNone->assertfalse|Some(x,_)->rev_stringxletparams_g=matchvalidate_finite_point~x:P.g_x~y:P.g_ywith|Okp->p|Error_->assertfalseletselectbit~then_~else_={f_x=Fe.selectbit~then_:then_.f_x~else_:else_.f_x;f_y=Fe.selectbit~then_:then_.f_y~else_:else_.f_y;f_z=Fe.selectbit~then_:then_.f_z~else_:else_.f_z;}letpowxexp=letr0=refFe.oneinletr1=refxinfori=P.byte_length*8-1downto0doletbit=bit_atexpiinletmultiplied=Fe.mul!r0!r1inletr0_sqr=Fe.sqr!r0inletr1_sqr=Fe.sqr!r1inr0:=Fe.selectbit~then_:multiplied~else_:r0_sqr;r1:=Fe.selectbit~then_:r1_sqr~else_:multiplied;done;!r0letdecompress=(* When p = 4*k+3, as is the case of NIST-P256, there is an efficient square
root algorithm to recover the y, as follows:
Given the compact representation of Q as x,
y2 = x^3 + a*x + b
y' = y2^((p+1)/4)
y = min(y',p-y')
Q=(x,y) is the canonical representation of the point
*)letpident=P.pident(* (Params.p + 1) / 4*)inleta=Fe.from_be_octetsP.ainletb=Fe.from_be_octetsP.binletp=Fe.from_be_octetsP.pinfunpk->letx=Fe.from_be_octets(String.subpk1P.byte_length)inletx3=Fe.mulxxinletx3=Fe.mulx3xin(* x3 *)letax=Fe.mulaxin(* ax *)letsum=Fe.addx3axinletsum=Fe.addsumbin(* y^2 *)lety=powsumpidentin(* https://tools.ietf.org/id/draft-jivsov-ecc-compact-00.xml#sqrt point 4.3*)lety'=Fe.subpyinlety=Fe.from_montgomeryyinlety_struct=Fe.to_octetsyin(* number must not be in montgomery domain*)lety_struct=rev_stringy_structinlety'=Fe.from_montgomeryy'inlety_struct2=Fe.to_octetsy'in(* number must not be in montgomery domain*)lety_struct2=rev_stringy_struct2inletident=string_get_uint8pk0inletsignY=2+(string_get_uint8y_struct(P.byte_length-2))land1inletres=ifInt.equalsignYidenttheny_structelsey_struct2inletout=Bytes.make((P.byte_length*2)+1)'\000'inBytes.setout0'\004';Bytes.blit_stringpk1out1P.byte_length;Bytes.blit_stringres0out(P.byte_length+1)P.byte_length;Bytes.unsafe_to_stringoutletof_octetsbuf=letlen=P.byte_lengthinifString.lengthbuf=0thenError`Invalid_formatelseletof_octetsbuf=letx=String.subbuf1leninlety=String.subbuf(1+len)leninvalidate_finite_point~x~yinmatchstring_get_uint8buf0with|0x00whenString.lengthbuf=1->Ok(at_infinity())|0x02|0x03whenString.lengthP.pident>0->letdecompressed=decompressbufinof_octetsdecompressed|0x04whenString.lengthbuf=1+len+len->of_octetsbuf|0x00|0x04->Error`Invalid_length|_->Error`Invalid_formatletscalar_mult_base=Fe.scalar_mult_base_pointendmoduletypeScalar=sigvalnot_zero:string->boolvalis_in_range:string->boolvalof_octets:string->(scalar,error)resultvalto_octets:scalar->stringvalscalar_mult:scalar->point->pointvalscalar_mult_base:scalar->pointvalgenerator_tables:unit->field_elementarrayarrayarrayendmoduleMake_scalar(Param:Parameters)(P:Point):Scalar=structletnot_zero=letzero=String.makeParam.byte_length'\000'infunbuf->not(Eqaf.equalbufzero)letis_in_rangebuf=not_zerobuf&&Eqaf.compare_be_with_len~len:Param.byte_lengthParam.nbuf>0letof_octetsbuf=matchis_in_rangebufwith|exceptionInvalid_argument_->Error`Invalid_length|true->Ok(Scalar(rev_stringbuf))|false->Error`Invalid_rangeletto_octets(Scalarbuf)=rev_stringbuf(* Branchless Montgomery ladder method *)letscalar_mult(Scalars)p=letr0=ref(P.at_infinity())inletr1=refpinfori=Param.byte_length*8-1downto0doletbit=bit_atsiinletsum=P.add!r0!r1inletr0_double=P.double!r0inletr1_double=P.double!r1inr0:=P.selectbit~then_:sum~else_:r0_double;r1:=P.selectbit~then_:r1_double~else_:sumdone;!r0(* Specialization of [scalar_mult d p] when [p] is the generator *)letscalar_mult_base=P.scalar_mult_base(* Pre-compute multiples of the generator point
returns the tables along with the number of significant bytes *)letgenerator_tables()=letlen=Param.fe_length*2inletone_table_=Array.init15(fun_->P.at_infinity())inlettable=Array.initlenone_tableinletbase=refP.params_ginfori=0tolen-1dotable.(i).(0)<-!base;forj=1to14dotable.(i).(j)<-P.add!basetable.(i).(j-1)done;base:=P.double!base;base:=P.double!base;base:=P.double!base;base:=P.double!basedone;letconvert{f_x;f_y;f_z}=[|f_x;f_y;f_z|]inArray.map(Array.mapconvert)tableendmoduleMake_dh(Param:Parameters)(P:Point)(S:Scalar):Dh=structletpoint_of_octetsc=matchP.of_octetscwith|Okpwhennot(P.is_infinityp)->Okp|Ok_->Error`At_infinity|Error_ase->eletpoint_to_octets=P.to_octetstypesecret=scalarletshare?(compress=false)private_key=letpublic_key=S.scalar_mult_baseprivate_keyinpoint_to_octets~compresspublic_keyletsecret_of_octets?compresss=matchS.of_octetsswith|Okp->Ok(p,share?compressp)|Error_ase->eletsecret_of_cs?compresss=Result.map(fun(p,share)->p,Cstruct.of_stringshare)(secret_of_octets?compress(Cstruct.to_strings))letrecgenerate_private_key?g()=letcandidate=Mirage_crypto_rng.generate?gParam.byte_lengthinmatchS.of_octets(Cstruct.to_stringcandidate)with|Oksecret->secret|Error_->generate_private_key?g()letgen_key_octets?compress?g()=letprivate_key=generate_private_key?g()in(private_key,share?compressprivate_key)letgen_key?compress?g()=letprivate_key,share=gen_key_octets?compress?g()inprivate_key,Cstruct.of_stringshareletkey_exchange_octetssecretreceived=matchpoint_of_octetsreceivedwith|Error_aserr->err|Okshared->Ok(P.x_of_finite_point(S.scalar_multsecretshared))letkey_exchangesecretreceived=matchkey_exchange_octetssecret(Cstruct.to_stringreceived)with|Error_aserr->err|Okshared->Ok(Cstruct.of_stringshared)endmoduletypeForeign_n=sigvalmul:out_field_element->field_element->field_element->unitvaladd:out_field_element->field_element->field_element->unitvalinv:out_field_element->field_element->unitvalone:out_field_element->unitvalfrom_bytes:out_field_element->string->unitvalto_bytes:bytes->field_element->unitvalfrom_montgomery:out_field_element->field_element->unitvalto_montgomery:out_field_element->field_element->unitendmoduletypeFn=sigvalfrom_be_octets:string->field_elementvalto_be_octets:field_element->stringvalmul:field_element->field_element->field_elementvaladd:field_element->field_element->field_elementvalinv:field_element->field_elementvalone:field_elementvalfrom_montgomery:field_element->field_elementvalto_montgomery:field_element->field_elementendmoduleMake_Fn(P:Parameters)(F:Foreign_n):Fn=structletb_uts=Bytes.unsafe_to_stringletcreate()=Bytes.makeP.fe_length'\000'letcreate_octets()=Bytes.makeP.byte_length'\000'letfrom_be_octetsv=letv'=create()inF.from_bytesv'(rev_stringv);F.to_montgomeryv'(b_utsv');b_utsv'letto_be_octetsv=letbuf=create_octets()inF.to_bytesbufv;rev_string(b_utsbuf)letmulab=lettmp=create()inF.multmpab;b_utstmpletaddab=lettmp=create()inF.addtmpab;b_utstmpletinva=lettmp=create()inF.invtmpa;F.to_montgomerytmp(b_utstmp);b_utstmpletone=lettmp=create()inF.onetmp;b_utstmpletfrom_montgomerya=lettmp=create()inF.from_montgomerytmpa;b_utstmpletto_montgomerya=lettmp=create()inF.to_montgomerytmpa;b_utstmpendmoduleMake_dsa(Param:Parameters)(F:Fn)(P:Point)(S:Scalar)(H:Mirage_crypto.Hash.S)=structtypepriv=scalarletbyte_length=Param.byte_lengthletpriv_of_octets=S.of_octetsletpriv_to_octets=S.to_octetsletpriv_of_cstructcs=priv_of_octets(Cstruct.to_stringcs)letpriv_to_cstructp=Cstruct.of_string(priv_to_octetsp)letpaddedmsg=letl=String.lengthmsginletbl=Param.byte_lengthinletfirst_byte_ok()=matchParam.first_byte_bitswith|None->true|Somem->(string_get_uint8msg0)land(0xFFland(lnotm))=0inifl>bl||(l=bl&¬(first_byte_ok()))thenraiseMessage_too_longelseifl=blthenmsgelse(letres=Bytes.makebl'\000'inBytes.blit_stringmsg0res(bl-l)(String.lengthmsg);Bytes.unsafe_to_stringres)letpadded_csmsg=letl=Cstruct.lengthmsginletbl=Param.byte_lengthinletfirst_byte_ok()=matchParam.first_byte_bitswith|None->true|Somem->(Cstruct.get_uint8msg0)land(0xFFland(lnotm))=0inifl>bl||(l=bl&¬(first_byte_ok()))thenraiseMessage_too_longelseifl=blthenmsgelseCstruct.append(Cstruct.create(bl-l))msg(* RFC 6979: compute a deterministic k *)moduleK_gen(H:Mirage_crypto.Hash.S)=structletdrbg:'aMirage_crypto_rng.generator=letmoduleM=Mirage_crypto_rng.Hmac_drbg(H)in(moduleM)letg~keycs=letg=Mirage_crypto_rng.create~strict:truedrbginMirage_crypto_rng.reseed~g(Cstruct.append(Cstruct.of_string(S.to_octetskey))cs);gletg_octets~keymsg=letg=Mirage_crypto_rng.create~strict:truedrbginMirage_crypto_rng.reseed~g(Cstruct.of_string(String.concat""[S.to_octetskey;msg]));g(* take qbit length, and ensure it is suitable for ECDSA (> 0 & < n) *)letgeng=letrecgo()=letr=Mirage_crypto_rng.generate~gParam.byte_lengthinletr=Cstruct.to_stringrinifS.is_in_rangerthenrelsego()ingo()(* let generate_octets ~key buf = gen (g ~key (Cstruct.of_string (padded buf))) *)letgenerate~keybuf=Cstruct.of_string(gen(g~key(padded_csbuf)))endmoduleK_gen_default=K_gen(H)typepub=pointletpub_of_octets=P.of_octetsletpub_to_octets?(compress=false)pk=P.to_octets~compresspkletpub_of_cstructcs=pub_of_octets(Cstruct.to_stringcs)letpub_to_cstruct?compressp=Cstruct.of_string(pub_to_octets?compressp)letgenerate?g()=(* FIPS 186-4 B 4.2 *)letd=letrecone()=matchS.of_octets(Cstruct.to_string(Mirage_crypto_rng.generate?gParam.byte_length))with|Okx->x|Error_->one()inone()inletq=S.scalar_mult_basedin(d,q)letx_of_finite_point_mod_np=matchP.to_affine_rawpwith|None->None|Some(x,_)->letx=F.to_montgomeryxinletx=F.mulxF.oneinletx=F.from_montgomeryxinSome(F.to_be_octetsx)letsign_octets~key?kmsg=letmsg=paddedmsginlete=F.from_be_octetsmsginletg=K_gen_default.g_octets~keymsginletrecdo_signg=letagain()=matchkwith|None->do_signg|Some_->invalid_arg"k not suitable"inletk'=matchkwithNone->K_gen_default.geng|Somek->kinletksc=matchS.of_octetsk'with|Okksc->ksc|Error_->invalid_arg"k not in range"(* if no k is provided, this cannot happen since K_gen_*.gen already preserves the Scalar invariants *)inletpoint=S.scalar_mult_basekscinmatchx_of_finite_point_mod_npointwith|None->again()|Somer->letr_mon=F.from_be_octetsrinletkmon=F.from_be_octetsk'inletkinv=F.invkmoninletdmon=F.from_be_octets(S.to_octetskey)inletrd=F.mulr_mondmoninletcmon=F.adderdinletsmon=F.mulkinvcmoninlets=F.from_montgomerysmoninlets=F.to_be_octetssinifS.not_zeros&&S.not_zerorthenr,selseagain()indo_signgletsign~key?kmsg=letr,s=sign_octets~key?k:(Option.mapCstruct.to_stringk)(Cstruct.to_stringmsg)inCstruct.of_stringr,Cstruct.of_stringsletpub_of_privpriv=S.scalar_mult_baseprivletverify_octets~key(r,s)msg=tryletr=paddedrands=paddedsinifnot(S.is_in_ranger&&S.is_in_ranges)thenfalseelseletmsg=paddedmsginletz=F.from_be_octetsmsginlets_mon=F.from_be_octetssinlets_inv=F.invs_moninletu1=F.mulzs_invinletr_mon=F.from_be_octetsrinletu2=F.mulr_mons_invinletu1=F.from_montgomeryu1inletu2=F.from_montgomeryu2inmatchS.of_octets(F.to_be_octetsu1),S.of_octets(F.to_be_octetsu2)with|Oku1,Oku2->letpoint=P.add(S.scalar_mult_baseu1)(S.scalar_multu2key)inbeginmatchx_of_finite_point_mod_npointwith|None->false(* point is infinity *)|Somer'->String.equalrr'end|Error_,_|_,Error_->falsewith|Message_too_long->falseletverify~key(r,s)digest=verify_octets~key(Cstruct.to_stringr,Cstruct.to_strings)(Cstruct.to_stringdigest)modulePrecompute=structletgenerator_tables=S.generator_tablesendendmoduleP224:Dh_dsa=structmoduleParams=structleta="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE"letb="\xB4\x05\x0A\x85\x0C\x04\xB3\xAB\xF5\x41\x32\x56\x50\x44\xB0\xB7\xD7\xBF\xD8\xBA\x27\x0B\x39\x43\x23\x55\xFF\xB4"letg_x="\xB7\x0E\x0C\xBD\x6B\xB4\xBF\x7F\x32\x13\x90\xB9\x4A\x03\xC1\xD3\x56\xC2\x11\x22\x34\x32\x80\xD6\x11\x5C\x1D\x21"letg_y="\xBD\x37\x63\x88\xB5\xF7\x23\xFB\x4C\x22\xDF\xE6\xCD\x43\x75\xA0\x5A\x07\x47\x64\x44\xD5\x81\x99\x85\x00\x7E\x34"letp="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01"letn="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\x16\xA2\xE0\xB8\xF0\x3E\x13\xDD\x29\x45\x5C\x5C\x2A\x3D"letpident=""letbyte_length=28letfe_length=ifSys.word_size==64then32else28(* TODO: is this congruent with C code? *)letfirst_byte_bits=NoneendmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p224_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p224_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p224_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p224_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p224_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p224_set_one"[@@noalloc]externalnz:field_element->bool="mc_p224_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p224_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p224_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p224_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p224_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p224_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p224_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p224_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p224_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np224_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np224_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np224_inv"[@@noalloc]externalone:out_field_element->unit="mc_np224_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np224_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np224_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np224_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np224_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Mirage_crypto.Hash.SHA256)endmoduleP256:Dh_dsa=structmoduleParams=structleta="\xFF\xFF\xFF\xFF\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFC"letb="\x5A\xC6\x35\xD8\xAA\x3A\x93\xE7\xB3\xEB\xBD\x55\x76\x98\x86\xBC\x65\x1D\x06\xB0\xCC\x53\xB0\xF6\x3B\xCE\x3C\x3E\x27\xD2\x60\x4B"letg_x="\x6B\x17\xD1\xF2\xE1\x2C\x42\x47\xF8\xBC\xE6\xE5\x63\xA4\x40\xF2\x77\x03\x7D\x81\x2D\xEB\x33\xA0\xF4\xA1\x39\x45\xD8\x98\xC2\x96"letg_y="\x4F\xE3\x42\xE2\xFE\x1A\x7F\x9B\x8E\xE7\xEB\x4A\x7C\x0F\x9E\x16\x2B\xCE\x33\x57\x6B\x31\x5E\xCE\xCB\xB6\x40\x68\x37\xBF\x51\xF5"letp="\xFF\xFF\xFF\xFF\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF"letn="\xFF\xFF\xFF\xFF\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xBC\xE6\xFA\xAD\xA7\x17\x9E\x84\xF3\xB9\xCA\xC2\xFC\x63\x25\x51"letpident="\x3F\xFF\xFF\xFF\xC0\x00\x00\x00\x40\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x40\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"|>rev_string(* (Params.p + 1) / 4*)letbyte_length=32letfe_length=32letfirst_byte_bits=NoneendmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p256_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p256_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p256_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p256_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p256_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p256_set_one"[@@noalloc]externalnz:field_element->bool="mc_p256_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p256_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p256_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p256_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p256_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p256_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p256_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p256_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p256_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np256_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np256_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np256_inv"[@@noalloc]externalone:out_field_element->unit="mc_np256_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np256_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np256_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np256_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np256_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Mirage_crypto.Hash.SHA256)endmoduleP384:Dh_dsa=structmoduleParams=structleta="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFC"letb="\xB3\x31\x2F\xA7\xE2\x3E\xE7\xE4\x98\x8E\x05\x6B\xE3\xF8\x2D\x19\x18\x1D\x9C\x6E\xFE\x81\x41\x12\x03\x14\x08\x8F\x50\x13\x87\x5A\xC6\x56\x39\x8D\x8A\x2E\xD1\x9D\x2A\x85\xC8\xED\xD3\xEC\x2A\xEF"letg_x="\xAA\x87\xCA\x22\xBE\x8B\x05\x37\x8E\xB1\xC7\x1E\xF3\x20\xAD\x74\x6E\x1D\x3B\x62\x8B\xA7\x9B\x98\x59\xF7\x41\xE0\x82\x54\x2A\x38\x55\x02\xF2\x5D\xBF\x55\x29\x6C\x3A\x54\x5E\x38\x72\x76\x0A\xB7"letg_y="\x36\x17\xde\x4a\x96\x26\x2c\x6f\x5d\x9e\x98\xbf\x92\x92\xdc\x29\xf8\xf4\x1d\xbd\x28\x9a\x14\x7c\xe9\xda\x31\x13\xb5\xf0\xb8\xc0\x0a\x60\xb1\xce\x1d\x7e\x81\x9d\x7a\x43\x1d\x7c\x90\xea\x0e\x5f"letp="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF"letn="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xC7\x63\x4D\x81\xF4\x37\x2D\xDF\x58\x1A\x0D\xB2\x48\xB0\xA7\x7A\xEC\xEC\x19\x6A\xCC\xC5\x29\x73"letpident="\x3F\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xBF\xFF\xFF\xFF\xC0\x00\x00\x00\x00\x00\x00\x00\x40\x00\x00\x00"|>rev_string(* (Params.p + 1) / 4*)letbyte_length=48letfe_length=48letfirst_byte_bits=NoneendmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p384_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p384_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p384_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p384_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p384_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p384_set_one"[@@noalloc]externalnz:field_element->bool="mc_p384_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p384_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p384_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p384_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p384_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p384_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p384_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p384_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p384_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np384_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np384_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np384_inv"[@@noalloc]externalone:out_field_element->unit="mc_np384_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np384_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np384_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np384_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np384_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Mirage_crypto.Hash.SHA384)endmoduleP521:Dh_dsa=structmoduleParams=structleta="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFC"letb="\x00\x51\x95\x3E\xB9\x61\x8E\x1C\x9A\x1F\x92\x9A\x21\xA0\xB6\x85\x40\xEE\xA2\xDA\x72\x5B\x99\xB3\x15\xF3\xB8\xB4\x89\x91\x8E\xF1\x09\xE1\x56\x19\x39\x51\xEC\x7E\x93\x7B\x16\x52\xC0\xBD\x3B\xB1\xBF\x07\x35\x73\xDF\x88\x3D\x2C\x34\xF1\xEF\x45\x1F\xD4\x6B\x50\x3F\x00"letg_x="\x00\xC6\x85\x8E\x06\xB7\x04\x04\xE9\xCD\x9E\x3E\xCB\x66\x23\x95\xB4\x42\x9C\x64\x81\x39\x05\x3F\xB5\x21\xF8\x28\xAF\x60\x6B\x4D\x3D\xBA\xA1\x4B\x5E\x77\xEF\xE7\x59\x28\xFE\x1D\xC1\x27\xA2\xFF\xA8\xDE\x33\x48\xB3\xC1\x85\x6A\x42\x9B\xF9\x7E\x7E\x31\xC2\xE5\xBD\x66"letg_y="\x01\x18\x39\x29\x6a\x78\x9a\x3b\xc0\x04\x5c\x8a\x5f\xb4\x2c\x7d\x1b\xd9\x98\xf5\x44\x49\x57\x9b\x44\x68\x17\xaf\xbd\x17\x27\x3e\x66\x2c\x97\xee\x72\x99\x5e\xf4\x26\x40\xc5\x50\xb9\x01\x3f\xad\x07\x61\x35\x3c\x70\x86\xa2\x72\xc2\x40\x88\xbe\x94\x76\x9f\xd1\x66\x50"letp="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF"letn="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFA\x51\x86\x87\x83\xBF\x2F\x96\x6B\x7F\xCC\x01\x48\xF7\x09\xA5\xD0\x3B\xB5\xC9\xB8\x89\x9C\x47\xAE\xBB\x6F\xB7\x1E\x91\x38\x64\x09"letpident="\x01\x7f\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"|>rev_stringletbyte_length=66letfe_length=ifSys.word_size==64then72else68(* TODO: is this congruent with C code? *)letfirst_byte_bits=Some0x01endmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p521_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p521_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p521_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p521_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p521_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p521_set_one"[@@noalloc]externalnz:field_element->bool="mc_p521_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p521_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p521_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p521_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p521_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p521_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p521_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p521_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p521_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np521_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np521_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np521_inv"[@@noalloc]externalone:out_field_element->unit="mc_np521_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np521_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np521_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np521_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np521_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Mirage_crypto.Hash.SHA512)endmoduleX25519=struct(* RFC 7748 *)externalx25519_scalar_mult_generic:bytes->string->string->unit="mc_x25519_scalar_mult_generic"[@@noalloc]letkey_len=32letscalar_multin_base=letout=Bytes.makekey_len'\000'inx25519_scalar_mult_genericoutin_base;Bytes.unsafe_to_stringouttypesecret=stringletbasepoint=String.initkey_len(function0->'\009'|_->'\000')letpublicpriv=scalar_multprivbasepointletgen_key_octets?compress:_?g()=letsecret=Cstruct.to_string(Mirage_crypto_rng.generate?gkey_len)insecret,publicsecretletgen_key?compress?g()=letsecret,public=gen_key_octets~compress?g()insecret,Cstruct.of_stringpublicletsecret_of_octets?compress:_s=ifString.lengths=key_lenthenOk(s,publics)elseError`Invalid_lengthletsecret_of_cs?compresscs=Result.map(fun(secret,public)->secret,Cstruct.of_stringpublic)(secret_of_octets~compress(Cstruct.to_stringcs))letis_zero=letzero=String.makekey_len'\000'infunbuf->String.equalzerobufletkey_exchange_octetssecretpublic=ifString.lengthpublic=key_lenthenletres=scalar_multsecretpublicinifis_zeroresthenError`Low_orderelseOkreselseError`Invalid_lengthletkey_exchangesecretpublic=Result.mapCstruct.of_string(key_exchange_octetssecret(Cstruct.to_stringpublic))endmoduleEd25519=structexternalscalar_mult_base_to_bytes:bytes->string->unit="mc_25519_scalar_mult_base"[@@noalloc]externalreduce_l:bytes->unit="mc_25519_reduce_l"[@@noalloc]externalmuladd:bytes->string->string->string->unit="mc_25519_muladd"[@@noalloc]externaldouble_scalar_mult:bytes->string->string->string->bool="mc_25519_double_scalar_mult"[@@noalloc]externalpub_ok:string->bool="mc_25519_pub_ok"[@@noalloc]letkey_len=32letscalar_mult_base_to_bytesp=lettmp=Bytes.makekey_len'\000'inscalar_mult_base_to_bytestmpp;Bytes.unsafe_to_stringtmpletmuladdabc=lettmp=Bytes.makekey_len'\000'inmuladdtmpabc;Bytes.unsafe_to_stringtmpletdouble_scalar_multabc=lettmp=Bytes.makekey_len'\000'inlets=double_scalar_multtmpabcins,Bytes.unsafe_to_stringtmptypepub=stringtypepriv=string(* RFC 8032 *)letpublicsecret=(* section 5.1.5 *)(* step 1 *)leth=Mirage_crypto.Hash.SHA512.digest(Cstruct.of_stringsecret)in(* step 2 *)lets,rest=Cstruct.splithkey_leninlets,rest=Cstruct.to_bytess,Cstruct.to_stringrestinBytes.set_uint8s0((Bytes.get_uint8s0)land248);Bytes.set_uint8s31(((Bytes.get_uint8s31)land127)lor64);lets=Bytes.unsafe_to_stringsin(* step 3 and 4 *)letpublic=scalar_mult_base_to_bytessinpublic,(s,rest)letpub_of_privsecret=fst(publicsecret)letpriv_of_octetsbuf=ifString.lengthbuf=key_lenthenOkbufelseError`Invalid_lengthletpriv_of_cstructp=priv_of_octets(Cstruct.to_stringp)letpriv_to_octetspriv=privletpriv_to_cstructp=Cstruct.of_string(priv_to_octetsp)letpub_of_octetsbuf=ifString.lengthbuf=key_lenthenifpub_okbufthenOkbufelseError`Not_on_curveelseError`Invalid_lengthletpub_of_cstructp=pub_of_octets(Cstruct.to_stringp)letpub_to_octetspub=publetpub_to_cstructp=Cstruct.of_string(pub_to_octetsp)letgenerate?g()=letsecret=Mirage_crypto_rng.generate?gkey_leninletsecret=Cstruct.to_stringsecretinsecret,pub_of_privsecretletsign_octets~keymsg=(* section 5.1.6 *)letpub,(s,prefix)=publickeyinletr=Mirage_crypto.Hash.SHA512.digest(Cstruct.of_string(String.concat""[prefix;msg]))inletr=Cstruct.to_bytesrinreduce_lr;letr=Bytes.unsafe_to_stringrinletr_big=scalar_mult_base_to_bytesrinletk=Mirage_crypto.Hash.SHA512.digest(Cstruct.of_string(String.concat""[r_big;pub;msg]))inletk=Cstruct.to_byteskinreduce_lk;letk=Bytes.unsafe_to_stringkinlets_out=muladdksrinletres=Bytes.make(key_len+key_len)'\000'inBytes.blit_stringr_big0res0key_len;Bytes.blit_strings_out0reskey_lenkey_len;Bytes.unsafe_to_stringresletsign~keymsg=Cstruct.of_string(sign_octets~key(Cstruct.to_stringmsg))letverify_octets~keysignature~msg=(* section 5.1.7 *)ifString.lengthsignature=2*key_lenthenletr,s=String.subsignature0key_len,String.subsignaturekey_lenkey_leninlets_smaller_l=(* check s within 0 <= s < L *)lets'=Bytes.make(key_len*2)'\000'inBytes.blit_strings0s'0key_len;reduce_ls';lets'=Bytes.unsafe_to_strings'inlets''=String.concat""[s;String.makekey_len'\000']inString.equals''s'inifs_smaller_lthenbeginletk=letdata_to_hash=String.concat""[r;key;msg]inMirage_crypto.Hash.SHA512.digest(Cstruct.of_stringdata_to_hash)inletk=Cstruct.to_byteskinreduce_lk;letk=Bytes.unsafe_to_stringkinletsuccess,r'=double_scalar_multkkeysinsuccess&&String.equalrr'endelsefalseelsefalseletverify~keysignature~msg=verify_octets~key(Cstruct.to_stringsignature)~msg:(Cstruct.to_stringmsg)end