123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314(*****************************************************************************)(* *)(* 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. *)(* *)(*****************************************************************************)openPlonkopenBlsopenUtilsmoduletypeS=sigincludePolynomial_commitment.S(** Auxiliary information needed by the prover for the meta-verification in
aPlonK *)typeprover_aux={r:Scalar.t;s_list:Scalar.tSMap.tlist}valprove_super_aggregation:Public_parameters.prover->transcript->Poly.tSMap.tlist->Commitment.prover_auxlist->querylist->Scalar.tSMap.tSMap.tlist->(proof*prover_aux)*transcriptvalverify_super_aggregation:Public_parameters.verifier->transcript->Commitment.tlist->querylist->Scalar.tSMap.tlist->proof->bool*Scalar.t*transcriptendmoduleMake_impl(PC:Polynomial_commitment.SwithtypeCommitment.t=Bls.G1.tSMap.t)=structtypesecret=PC.secrettypequery=PC.query[@@derivingrepr]typeanswer=PC.answer[@@derivingrepr]typetranscript=PC.transcriptmodulePublic_parameters=structtypeprover={pp_pc_prover:PC.Public_parameters.prover;pp_pack_prover:Pack.prover_public_parameters;}[@@derivingrepr]typeverifier={pp_pc_verifier:PC.Public_parameters.verifier;pp_pack_verifier:Pack.verifier_public_parameters;}[@@derivingrepr]typesetup_params=intletsetupsetup_paramssrs=letpp_pc_prover,pp_pc_verifier=PC.Public_parameters.setupsetup_paramssrsinletpp_pack_prover,pp_pack_verifier=Pack.setupsetup_params(sndsrs)inletpp_prover={pp_pc_prover;pp_pack_prover}inletpp_verifier={pp_pc_verifier;pp_pack_verifier}in(pp_prover,pp_verifier)letto_bytesd({pp_pc_prover;pp_pack_prover}:prover)=Utils.Hash.hash_bytes[PC.Public_parameters.to_bytesdpp_pc_prover;Pack.public_parameters_to_bytespp_pack_prover;]endmoduleCommitment=structtypeprover_public_parameters=Public_parameters.provertypesecret=Poly.tSMap.ttypet=Pack.commitment[@@derivingrepr](* [PC.Commitment.t] is required to be [Bls12_381.G1.t SMap.t],
containing all the commitments that were packed *)typeprover_aux=PC.Commitment.t*PC.Commitment.prover_aux[@@derivingrepr]letcommit?all_keys(pp:Public_parameters.prover)f_map=(* Relevant_positions is the list of the indexes of f_map’s elements in the all_keys list. *)letrelevant_positions=matchall_keyswith|None->List.init(SMap.cardinalf_map)Fun.id|Some[]->List.init(SMap.cardinalf_map)Fun.id|Someks->(* Note that in order to get relevant_positions relatively to the map,
the keys need to be sorted as they are be in the commitment smap *)letsorted_ks=List.sortString.compareksinList.mapi(funix->(i,x))sorted_ks|>List.filter_map(fun(i,x)->Option.map(Fun.consti)(SMap.find_optxf_map))inletprover_aux=PC.Commitment.commitpp.pp_pc_proverf_mapinletcm_list=SMap.values(fstprover_aux)inletpack_cmt=Pack.partial_commit~relevant_positionspp.pp_pack_prover(Array.of_listcm_list)in(pack_cmt,prover_aux)letcardinal=Pack.commitment_cardinalletrename_fcmt=cmtletcommit_singlepp=PC.Commitment.commit_singlePublic_parameters.(pp.pp_pc_prover)letempty=Pack.empty_commitmentletempty_prover_aux=(PC.Commitment.empty,PC.Commitment.empty_prover_aux)letrecombine=function|[]->empty|h::t->List.fold_leftPack.combinehtletrecombine_prover_auxl=letcm=PC.Commitment.recombine(List.mapfstl)inletp_a=PC.Commitment.recombine_prover_aux(List.mapsndl)in(cm,p_a)letof_listpp~namel=letpc_cm=PC.Commitment.(of_listPublic_parameters.(pp.pp_pc_prover)~namel)in(Pack.commitPublic_parameters.(pp.pp_pack_prover)(Array.of_listl),pc_cm)letto_map_=failwith"Not implemented & should not be used in verifier"endtypeproof={pc_proof:PC.proof;packed_values:Pack.packedlist;pack_proof:Pack.proof;}[@@derivingrepr]typeprover_aux={r:Scalar.t;s_list:Scalar.tSMap.tlist}letbatch_polysrmap=letpolys=SMap.valuesmapinPoly.linear_with_powerspolysrletbatch_answersr=SMap.map(funm->Fr_generation.batchr@@SMap.valuesm)letevaluate=PC.evaluate(* compute P := cmt₀ + r cmt₁ + r² cmt₂ + ... for every group of commitments
in the list [prover_aux_list], and common randomness r (freshly sampled);
such P values are returned as [packed_values], together with a proof
[packed_proof] of their correctness;
also, on input a list of evaluations [answer_list], at the requested points
in [query_list], produce a proof of their validity: such proof is a PC
proof (for every group) on the aggregatted commitment P with respect to the
corresponding aggregated evaluations (we thus batch [answer_list] with [r]
similarly) *)letprove_pack(pp:Public_parameters.prover)transcriptf_map_list(prover_aux_list:Commitment.prover_auxlist)query_listanswer_list=letr,transcript=Fr_generation.random_frtranscriptinletf_list=List.map(batch_polysr)f_map_listinlets_list=List.map(batch_answersr)answer_listin(* [cmts_list] is a list of G1.t SMap.t, containing the PC commitments to
every polynomial (note that PC.Commitment.t = Bls12_381.G1.t SMap.t) *)letcmts_list=List.map(fun(cmts,_prover_aux)->SMap.valuescmts|>Array.of_list)prover_aux_listin(* [packed_values] has type [G1.t list] and it is the result of batching
each map in [cmt_list] with powers of [r].
[pack_proof] asserts that [packed_values] was correctly computed. *)let(packed_values,pack_proof),transcript=Pack.provepp.pp_pack_provertranscriptrcmts_listin(* prepare [f_list] and [s_list], the batched version of [f_map_list]
polys and [answer_list] (using randomness [r]) by selecting a dummy
name for them [string_of_int i] in order to call the underlying PC *)letf_map_list=List.mapi(funil->SMap.singleton(string_of_inti)l)f_listinlets_map_list=List.mapi(funim->SMap.map(funs->SMap.singleton(string_of_inti)s)m)s_listinletprover_aux_list=List.mapsndprover_aux_listin(* call the underlying PC prover on the batched polynomials/evaluations
the verifier will verify such proof using [packed_values] as the
commitments *)letpc_proof,transcript=PC.provepp.pp_pc_provertranscriptf_map_listprover_aux_listquery_lists_map_listinletproof={pc_proof;packed_values;pack_proof}inlettranscript=Transcript.expandproof_tprooftranscriptin((proof,{r;s_list}),transcript)letprove(pp:Public_parameters.prover)transcriptf_map_list(prover_aux_list:Commitment.prover_auxlist)query_listanswer_list=lettranscript=Transcript.list_expandquery_tquery_listtranscriptinlettranscript=Transcript.list_expandanswer_tanswer_listtranscriptinlet(proof,_),transcript=prove_packpptranscriptf_map_listprover_aux_listquery_listanswer_listin(proof,transcript)letprove_super_aggregation(pp:Public_parameters.prover)transcriptf_map_list(prover_aux_list:Commitment.prover_auxlist)query_listanswer_list=lettranscript=Transcript.list_expandquery_tquery_listtranscriptinprove_packpptranscriptf_map_listprover_aux_listquery_listanswer_listletverify_pack(pp:Public_parameters.verifier)rtranscriptcmt_listquery_lists_listproof=(* verify that the [packed_values] are correct, they will be used as
the commitments for the PC proof of (batched) evaluations *)letpack_ok,transcript=Pack.verifypp.pp_pack_verifiertranscriptcmt_listr(proof.packed_values,proof.pack_proof)in(* batch the evaluations using [r] and prepare the query to the PC verifier
by selecting the default dummy names [string_of_int i] names *)lets_map_list=List.mapi(funim->SMap.map(funs->SMap.singleton(string_of_inti)s)m)s_listinletcmt_map_list=List.mapi(funil->SMap.singleton(string_of_inti)l)proof.packed_valuesin(* verify that the batched evaluations are correct *)letpc_ok,transcript=PC.verifypp.pp_pc_verifiertranscriptcmt_map_listquery_lists_map_listproof.pc_proofin(pack_ok&&pc_ok,Transcript.expandproof_tprooftranscript)letverify(pp:Public_parameters.verifier)transcriptcmt_listquery_lists_map_listproof=lettranscript=Transcript.list_expandquery_tquery_listtranscriptinlettranscript=Transcript.list_expandanswer_ts_map_listtranscriptinletr,transcript=Fr_generation.random_frtranscriptinlets_list=List.map(batch_answersr)s_map_listinverify_packpprtranscriptcmt_listquery_lists_listproofletverify_super_aggregation(pp:Public_parameters.verifier)transcriptcmt_listquery_lists_listproof=lettranscript=Transcript.list_expandquery_tquery_listtranscriptinletr,transcript=Fr_generation.random_frtranscriptinletok,transcript=verify_packpprtranscriptcmt_listquery_lists_listproofin(ok,r,transcript)endmoduleMake:functor(PC:Polynomial_commitment.SwithtypeCommitment.t=Bls.G1.tSMap.t)->S=Make_implincludeMake(Polynomial_commitment.Kzg_impl)