123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686(*****************************************************************************)(* *)(* MIT License *)(* Copyright (c) 2022 Nomadic Labs <contact@nomadic-labs.com> *)(* *)(* Permission is hereby granted, free of charge, to any person obtaining a *)(* copy of this software and associated documentation files (the "Software"),*)(* to deal in the Software without restriction, including without limitation *)(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)(* and/or sell copies of the Software, and to permit persons to whom the *)(* Software is furnished to do so, subject to the following conditions: *)(* *)(* The above copyright notice and this permission notice shall be included *)(* in all copies or substantial portions of the Software. *)(* *)(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)(* DEALINGS IN THE SOFTWARE. *)(* *)(*****************************************************************************)moduleU=UtilsopenPlompilermoduleHashPV=Anemoi128moduleMerklePV=Gadget.Merkle(HashPV)moduleSchnorrPV=Plompiler.Schnorr(HashPV)moduleCurve=Mec.Curve.Jubjub.AffineEdwardsopenConstantsmoduleBounded=Bounded.Make(Bound)moduleP=structmoduleSchnorr=SchnorrPV.PmoduleMerkle=MerklePV.PmoduleBounded=Bounded.Ptype'aticket={id:S.t;amount:'aBounded.t}typetezos_pkh=bytestypetezos_zkru=bytestypeaccount={pk:Schnorr.pk;tez_balance:balanceBounded.t;cnt:counterBounded.t;tickets_root:S.t;}typeleaf={pos:positionBounded.t;ticket:balanceticket}moduleIMap=Map.Make(Int)typestate={(* account index*)accounts:(account*leafarray*Merkle.tree)IMap.t;accounts_tree:Merkle.tree;(* First leaf of an empty account *)next_position:int;}typeproof={path:Merkle.path;root:S.t}typeaccount_tree_el={before:account;after:account;proof:proof}typeleaf_tree_el={before:leaf;after:leaf;path:Merkle.path}typetree_el={account:account_tree_el;leaf:leaf_tree_el}typeheader={op_code:op_codeBounded.t;price:balanceticket;l1_dst:tezos_pkh;rollup_id:tezos_zkru;}typeunsigned_transfer_payload={cnt:counterBounded.t;src:positionBounded.t;dst:positionBounded.t;amount:amountticket;fee:feeBounded.t;}typetransfer_payload={msg:unsigned_transfer_payload;signature:Schnorr.signature;}typeunsigned_transfer={header:header;payload:unsigned_transfer_payload;}typetransfer={header:header;payload:transfer_payload}typetransfer_storage={src:tree_el;dst:tree_el;valid:bool}typeunsigned_create_payload={pk:Schnorr.pk;fee:feeBounded.t}typecreate_payload={msg:unsigned_create_payload;signature:Schnorr.signature;}typeunsigned_create={header:header;payload:unsigned_create_payload}typecreate={header:header;payload:create_payload}typecreate_storage={dst:tree_el;next_empty:tree_el;valid:bool}typecredit_payload={cnt:counterBounded.t;dst:positionBounded.t;amount:amountticket;}typecredit={header:header;payload:credit_payload}typecredit_storage={dst:tree_el;valid:bool}typeunsigned_debit_payload={cnt:counterBounded.t;src:positionBounded.t;amount:amountticket;}typedebit_payload={msg:unsigned_debit_payload;signature:Schnorr.signature;}typeunsigned_debit={header:header;payload:unsigned_debit_payload}typedebit={header:header;payload:debit_payload}typedebit_storage={src:tree_el;valid:bool}typeunsigned_tx=|Transferofunsigned_transfer|Createofunsigned_create|Creditofcredit|Debitofunsigned_debittypetx=|Transferoftransfer|Createofcreate|Creditofcredit|Debitofdebittypetx_storage=|Transferoftransfer_storage|Createofcreate_storage|Creditofcredit_storage|Debitofdebit_storagemoduleDummy=structletcnt=Bounded.make~bound:Bound.max_counterZ.zeroletfee=Bounded.make~bound:Bound.max_feeZ.zeroletpos=Bounded.make~bound:Bound.max_nb_leavesZ.zeroletamount=Bounded.make~bound:Bound.max_amountZ.zeroletbalance=Bounded.make~bound:Bound.max_balanceZ.zeroletticket_amount={id=S.zero;amount}letticket_balance={id=S.zero;amount=balance}letop_code=Bounded.make~bound:Bound.max_op_codeZ.zeroletroot=Bls12_381.Fr.random()letsk=Curve.Scalar.random()letpk=Schnorr.neuterizesklettezos_pkh=Bytes.init21(funi->char_of_inti)lettezos_zkru=Bytes.init20(fun_i->char_of_int0)letsignature=letrand=Curve.Scalar.random()inSchnorr.signskS.zerorandletleaf:leaf={pos;ticket=ticket_balance}letaccount:account={pk;tez_balance=balance;cnt;tickets_root=root}letproofdepth:proof={path=List.initdepth(fun_->(Bls12_381.Fr.random(),true));root}letaccount_tree_el:account_tree_el={before=account;after=account;proof=proofConstants.accounts_depth;}letleaf_tree_el:leaf_tree_el={before=leaf;after=leaf;path=(proofConstants.tickets_depth).path}lettree_el:tree_el={account=account_tree_el;leaf=leaf_tree_el}letheader={op_code;price=ticket_balance;l1_dst=tezos_pkh;rollup_id=tezos_zkru;}letunsigned_transfer_payload={cnt;src=pos;dst=pos;amount=ticket_amount;fee}lettransfer_payload:transfer_payload={msg=unsigned_transfer_payload;signature}lettransfer:transfer={header;payload=transfer_payload}lettransfer_storage:transfer_storage={src=tree_el;dst=tree_el;valid=true}letunsigned_create_payload={pk;fee}letcreate_payload:create_payload={msg=unsigned_create_payload;signature}letcreate:create={header;payload=create_payload}letcreate_storage:create_storage={dst=tree_el;next_empty=tree_el;valid=true}letcredit_payload={cnt;dst=pos;amount=ticket_amount}letcredit:credit={header;payload=credit_payload}letcredit_storage:credit_storage={dst=tree_el;valid=true}letunsgined_debit_payload={cnt;src=pos;amount=ticket_amount}letdebit_payload:debit_payload={msg=unsgined_debit_payload;signature}letdebit:debit={header;payload=debit_payload}letdebit_storage:debit_storage={src=tree_el;valid=true}endendmoduleV(L:LIB)=structopenLmoduleSchnorr=SchnorrPV.V(L)moduleMerkle=MerklePV.V(L)moduleBounded_u=Bounded.V(L)typecurve_t_u=(scalar*scalar)reprtypecurve_base_t_u=scalarreprtypecurve_scalar_t_u=scalarreprtype'aticket_u={id:scalarrepr;amount:'aBounded_u.t}typetezos_pkh_u=scalarreprtypetezos_zkru_u=scalarreprtypeaccount_u={pk:Schnorr.pkrepr;tez_balance:balanceBounded_u.t;cnt:counterBounded_u.t;tickets_root:scalarrepr;}typeleaf_u={pos:positionBounded_u.t;ticket:balanceticket_u}typeproof_u={path:Merkle.path;root:scalarrepr}typeaccount_tree_el_u={before:account_u;after:account_u;proof:proof_u;}typeleaf_tree_el_u={before:leaf_u;after:leaf_u;path:Merkle.path}typetree_el_u={account:account_tree_el_u;leaf:leaf_tree_el_u}typeheader_u={op_code:op_codeBounded_u.t;price:balanceticket_u;l1_dst:tezos_pkh_u;rollup_id:tezos_zkru_u;}typeunsigned_transfer_payload_u={cnt:counterBounded_u.t;src:positionBounded_u.t;dst:positionBounded_u.t;amount:amountticket_u;fee:feeBounded_u.t;}typetransfer_payload_u={msg:unsigned_transfer_payload_u;signature:Schnorr.signature;}typetransfer_u={header:header_u;payload:transfer_payload_u}typetransfer_storage_u={src:tree_el_u;dst:tree_el_u;valid:boolrepr;}typeunsigned_create_payload_u={pk:Schnorr.pkrepr;fee:feeBounded_u.t}typecreate_payload_u={msg:unsigned_create_payload_u;signature:Schnorr.signature;}typecreate_u={header:header_u;payload:create_payload_u}typecreate_storage_u={dst:tree_el_u;next_empty:tree_el_u;valid:boolrepr;}typecredit_payload_u={cnt:counterBounded_u.t;dst:positionBounded_u.t;amount:amountticket_u;}typecredit_u={header:header_u;payload:credit_payload_u}typecredit_storage_u={dst:tree_el_u;valid:boolrepr}typeunsigned_debit_payload_u={cnt:counterBounded_u.t;src:positionBounded_u.t;amount:amountticket_u;}typedebit_payload_u={msg:unsigned_debit_payload_u;signature:Schnorr.signature;}typedebit_u={header:header_u;payload:debit_payload_u}typedebit_storage_u={src:tree_el_u;valid:boolrepr}endmoduleEncodings(L:LIB)=structmoduleBounded_e=Bounded.Encoding(L)openPopenLopenV(L)openL.EncodingsmoduleAnemoi=Anemoi128.VmodulePlompiler_Curve=JubjubEdwards(L)modulePlompiler_Hash=Anemoi(L)openUlets_of_intx=S.of_z(Z.of_intx)letcurve_base_t_encoding:(Curve.Base.t,curve_base_t_u,_)encoding=conv(funr->r)(funr->r)curve_base_to_scurve_base_of_sscalar_encodingletcurve_scalar_t_encoding:(Curve.Scalar.t,curve_scalar_t_u,_)encoding=conv(funr->r)(funr->r)curve_scalar_to_scurve_scalar_of_sscalar_encodingletcurve_t_encoding:(Curve.t,curve_t_u,_)encoding=with_implicit_bool_checkPlompiler_Curve.is_on_curve@@conv(funr->of_pairr)(fun(u,v)->pairuv)(func->(curve_base_to_s@@Curve.get_u_coordinatec,curve_base_to_s@@Curve.get_v_coordinatec))(fun(u,v)->Curve.from_coordinates_exn~u:(curve_base_of_su)~v:(curve_base_of_sv))(obj2_encodingscalar_encodingscalar_encoding)letbalance_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_balanceletamount_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_amountletfee_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_feeletpos_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_nb_leavesletcnt_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_counterletop_code_encoding~safety=Bounded_e.encoding~safetyConstants.Bound.max_op_codelettezos_pkh_encoding:(tezos_pkh,tezos_pkh_u,_)encoding=conv(funpkhu->pkhu)(funw->w)U.scalar_of_bytesU.scalar_to_bytesscalar_encodinglettezos_zkru_encoding:(tezos_zkru,tezos_zkru_u,_)encoding=conv(funzkru->zkru)(funw->w)U.scalar_of_bytesU.scalar_to_bytesscalar_encodingletticket_encoding~safety(bound:'aBound.t):('aticket,'aticket_u,_)encoding=conv(fun{id;amount}->(id,amount))(fun(id,amount)->{id;amount})(fun({id;amount}:'aticket)->(id,amount))(fun(id,amount)->{id;amount})(obj2_encodingscalar_encoding(Bounded_e.encoding~safetybound))letticket_balance_encoding~safety=ticket_encoding~safetyConstants.Bound.max_balanceletticket_amount_encoding~safety=ticket_encoding~safetyConstants.Bound.max_amountletaccount_encoding:(account,account_u,_)encoding=conv(fun{pk;tez_balance;cnt;tickets_root}->(pk,(tez_balance,(cnt,tickets_root))))(fun(pk,(tez_balance,(cnt,tickets_root)))->{pk;tez_balance;cnt;tickets_root})(fun(acc:account)->(acc.pk,(acc.tez_balance,(acc.cnt,acc.tickets_root))))(fun(pk,(tez_balance,(cnt,tickets_root)))->{pk;tez_balance;cnt;tickets_root})(obj4_encodingSchnorr.pk_encoding(balance_encoding~safety:NoCheck)(cnt_encoding~safety:NoCheck)scalar_encoding)letleaf_encoding:(leaf,leaf_u,_)encoding=conv(fun{pos;ticket}->(pos,ticket))(fun(pos,ticket)->{pos;ticket})(fun({pos;ticket}:leaf)->(pos,ticket))(fun(pos,ticket)->{pos;ticket})(obj2_encoding(pos_encoding~safety:NoCheck)(ticket_balance_encoding~safety:NoCheck))letproof_encoding:(proof,proof_u,_)encoding=conv(fun{path;root}->(path,root))(fun(path,root)->{path;root})(fun({path;root}:proof)->(path,root))(fun(path,root)->{path;root})(obj2_encodingMerkle.path_encodingscalar_encoding)letaccount_tree_el_encoding:(account_tree_el,account_tree_el_u,_)encoding=conv(fun{before;after;proof}->(before,(after,proof)))(fun(before,(after,proof))->{before;after;proof})(fun({before;after;proof}:account_tree_el)->(before,(after,proof)))(fun(before,(after,proof))->{before;after;proof})(obj3_encodingaccount_encodingaccount_encodingproof_encoding)letleaf_tree_el_encoding:(leaf_tree_el,leaf_tree_el_u,_)encoding=conv(fun{before;after;path}->(before,(after,path)))(fun(before,(after,path))->{before;after;path})(fun({before;after;path}:leaf_tree_el)->(before,(after,path)))(fun(before,(after,path))->{before;after;path})(obj3_encodingleaf_encodingleaf_encodingMerkle.path_encoding)lettree_el_encoding:(tree_el,tree_el_u,_)encoding=conv(fun{account;leaf}->(account,leaf))(fun(account,leaf)->{account;leaf})(fun({account;leaf}:tree_el)->(account,leaf))(fun(account,leaf)->{account;leaf})(obj2_encodingaccount_tree_el_encodingleaf_tree_el_encoding)letheader_encoding~safety:(header,header_u,_)encoding=conv(fun{op_code;price;l1_dst;rollup_id}->(op_code,(price,(l1_dst,rollup_id))))(fun(op_code,(price,(l1_dst,rollup_id)))->{op_code;price;l1_dst;rollup_id})(fun({op_code;price;l1_dst;rollup_id}:header)->(op_code,(price,(l1_dst,rollup_id))))(fun(op_code,(price,(l1_dst,rollup_id)))->{op_code;price;l1_dst;rollup_id})(obj4_encoding(op_code_encoding~safety)(ticket_balance_encoding~safety)tezos_pkh_encodingtezos_zkru_encoding)letunsigned_transfer_payload_encoding~safety:(unsigned_transfer_payload,unsigned_transfer_payload_u,_)encoding=conv(fun(tx:unsigned_transfer_payload_u)->(tx.cnt,(tx.src,(tx.dst,(tx.amount,tx.fee)))))(fun(cnt,(src,(dst,(amount,fee))))->{cnt;src;dst;amount;fee})(fun(tx:unsigned_transfer_payload)->(tx.cnt,(tx.src,(tx.dst,(tx.amount,tx.fee)))))(fun(cnt,(src,(dst,(amount,fee))))->{cnt;src;dst;amount;fee})(obj5_encoding(cnt_encoding~safety)(pos_encoding~safety)(pos_encoding~safety)(ticket_amount_encoding~safety)(fee_encoding~safety))lettransfer_payload_encoding~safety:(transfer_payload,transfer_payload_u,_)encoding=conv(fun({msg;signature}:transfer_payload_u)->(msg,signature))(fun(msg,signature)->{msg;signature})(fun({msg;signature}:transfer_payload)->(msg,signature))(fun(msg,signature)->{msg;signature})(obj2_encoding(unsigned_transfer_payload_encoding~safety)Schnorr.signature_encoding)lettransfer_encoding~safety:(transfer,transfer_u,_)encoding=conv(fun(tx:transfer_u)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(fun(tx:transfer)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(obj2_encoding(header_encoding~safety)(transfer_payload_encoding~safety))lettransfer_storage_encoding:(transfer_storage,transfer_storage_u,_)encoding=conv(fun(tx:transfer_storage_u)->(tx.src,(tx.dst,tx.valid)))(fun(src,(dst,valid))->{src;dst;valid})(fun(tx:transfer_storage)->(tx.src,(tx.dst,tx.valid)))(fun(src,(dst,valid))->{src;dst;valid})(obj3_encodingtree_el_encodingtree_el_encodingbool_encoding)letunsigned_create_payload_encoding~safety:(unsigned_create_payload,unsigned_create_payload_u,_)encoding=conv(fun(tx:unsigned_create_payload_u)->(tx.pk,tx.fee))(fun(pk,fee)->{pk;fee})(fun(tx:unsigned_create_payload)->(tx.pk,tx.fee))(fun(pk,fee)->{pk;fee})(obj2_encodingSchnorr.pk_encoding(fee_encoding~safety))letcreate_payload_encoding~safety:(create_payload,create_payload_u,_)encoding=conv(fun({msg;signature}:create_payload_u)->(msg,signature))(fun(msg,signature)->{msg;signature})(fun({msg;signature}:create_payload)->(msg,signature))(fun(msg,signature)->{msg;signature})(obj2_encoding(unsigned_create_payload_encoding~safety)Schnorr.signature_encoding)letcreate_encoding~safety:(create,create_u,_)encoding=conv(fun(tx:create_u)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(fun(tx:create)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(obj2_encoding(header_encoding~safety)(create_payload_encoding~safety))letcreate_storage_encoding:(create_storage,create_storage_u,_)encoding=conv(fun(tx:create_storage_u)->(tx.dst,(tx.next_empty,tx.valid)))(fun(dst,(next_empty,valid))->{dst;next_empty;valid})(fun(tx:create_storage)->(tx.dst,(tx.next_empty,tx.valid)))(fun(dst,(next_empty,valid))->{dst;next_empty;valid})(obj3_encodingtree_el_encodingtree_el_encodingbool_encoding)letcredit_payload_encoding~safety:(credit_payload,credit_payload_u,_)encoding=conv(fun(tx:credit_payload_u)->(tx.cnt,(tx.dst,tx.amount)))(fun(cnt,(dst,amount))->{cnt;dst;amount})(fun(tx:credit_payload)->(tx.cnt,(tx.dst,tx.amount)))(fun(cnt,(dst,amount))->{cnt;dst;amount})(obj3_encoding(cnt_encoding~safety)(pos_encoding~safety)(ticket_amount_encoding~safety))letcredit_encoding~safety:(credit,credit_u,_)encoding=conv(fun(tx:credit_u)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(fun(tx:credit)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(obj2_encoding(header_encoding~safety)(credit_payload_encoding~safety))letcredit_storage_encoding:(credit_storage,credit_storage_u,_)encoding=conv(fun(tx:credit_storage_u)->(tx.dst,tx.valid))(fun(dst,valid)->{dst;valid})(fun(tx:credit_storage)->(tx.dst,tx.valid))(fun(dst,valid)->{dst;valid})(obj2_encodingtree_el_encodingbool_encoding)letunsigned_debit_payload_encoding~safety:(unsigned_debit_payload,unsigned_debit_payload_u,_)encoding=conv(fun(tx:unsigned_debit_payload_u)->(tx.cnt,(tx.src,tx.amount)))(fun(cnt,(src,amount))->{cnt;src;amount})(fun(tx:unsigned_debit_payload)->(tx.cnt,(tx.src,tx.amount)))(fun(cnt,(src,amount))->{cnt;src;amount})(obj3_encoding(cnt_encoding~safety)(pos_encoding~safety)(ticket_amount_encoding~safety))letdebit_payload_encoding~safety:(debit_payload,debit_payload_u,_)encoding=conv(fun({msg;signature}:debit_payload_u)->(msg,signature))(fun(msg,signature)->{msg;signature})(fun({msg;signature}:debit_payload)->(msg,signature))(fun(msg,signature)->{msg;signature})(obj2_encoding(unsigned_debit_payload_encoding~safety)Schnorr.signature_encoding)letdebit_encoding~safety:(debit,debit_u,_)encoding=conv(fun(tx:debit_u)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(fun(tx:debit)->(tx.header,tx.payload))(fun(header,payload)->{header;payload})(obj2_encoding(header_encoding~safety)(debit_payload_encoding~safety))letdebit_storage_encoding:(debit_storage,debit_storage_u,_)encoding=conv(fun(tx:debit_storage_u)->(tx.src,tx.valid))(fun(src,valid)->{src;valid})(fun(tx:debit_storage)->(tx.src,tx.valid))(fun(src,valid)->{src;valid})(obj2_encodingtree_el_encodingbool_encoding)end