Source file main_protocol.ml

(*****************************************************************************)
(*                                                                           *)
(* 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.                                                 *)
(*                                                                           *)
(*****************************************************************************)

module SMap = Plonk.SMap

module Make_impl
    (Super_PP : Polynomial_protocol.S with type PC.Scalar.t = Plompiler.S.t) =
struct
  include Plonk.Main_protocol.Make_impl (Super_PP)
  module PP = Super_PP

  type prover_aux = {
    answers : scalar SMap.t SMap.t list;
    batch : scalar SMap.t list;
    alpha : scalar;
    beta : scalar;
    gamma : scalar;
    delta : scalar;
    x : scalar;
    r : scalar;
    cm_answers : scalar;
    cm_pi : scalar;
  }

  type verifier_aux = {
    alpha : scalar;
    beta : scalar;
    gamma : scalar;
    delta : scalar;
    x : scalar;
    r : scalar;
  }

  let prove_list (pp : prover_public_parameters) ~inputs =
    assert (SMap.cardinal pp.circuits_map = 1);
    assert (SMap.cardinal inputs = 1);
    (* Rename inputs as circuit *)
    let inputs =
      SMap.map (fun _ -> snd @@ SMap.choose inputs) pp.circuits_map
    in
    (* TODO: can we commit only to the hidden pi?*)
    let cm_pi =
      SMap.bindings inputs
      |> List.map (fun (_, i_l) ->
             List.map (fun i -> i.public) i_l |> Array.concat)
      |> Array.concat |> Super_PP.poseidon
    in
    (* add the PI in the transcript *)
    let transcript =
      Plonk.Utils.expand_transcript Scalar.t cm_pi pp.transcript
    in
    let ( (pp_proof, Super_PP.{ answers; batch; alpha; x; r; cm_answers }),
          (perm_and_plook, wires_cm, beta, gamma, delta) ) =
      Prover.prove_circuits ~pp_prove:Super_PP.prove_super_aggregation
        ((pp.common_pp, pp.circuits_map), transcript)
        ~inputs_map:inputs
    in
    ( { perm_and_plook; wires_cm; pp_proof },
      { answers; batch; alpha; beta; gamma; delta; x; r; cm_answers; cm_pi } )

  let verify_list pp ~nb_proofs (proof, s_list, cm_answers, cm_pi) =
    assert (SMap.cardinal pp.circuits_map = 1);
    (* add the PI in the transcript *)
    let transcript =
      Plonk.Utils.expand_transcript Scalar.t cm_pi pp.transcript
    in
    let public_inputs =
      SMap.singleton
        (fst @@ SMap.choose pp.circuits_map)
        (List.init nb_proofs (fun _ -> [||]))
    in
    let transcript, _, beta, gamma, delta, commitments, eval_points =
      Verifier.verify_parameters
        ((pp.common_pp, pp.circuits_map), transcript)
        ~public_inputs proof
    in
    let (kzg_verif, Super_PP.{ alpha; x; r }), _transcript =
      Super_PP.verify_super_aggregation pp.common_pp.pp_public_parameters
        transcript ~n:pp.common_pp.n ~generator:pp.common_pp.generator
        ~commitments ~eval_points ~s_list ~cm_answers proof.pp_proof
    in
    (kzg_verif, { alpha; beta; gamma; delta; x; r })

  let get_gen_n_t (prover_public_params : prover_public_parameters) =
    ( Domain.get prover_public_params.common_pp.domain 1,
      prover_public_params.common_pp.n,
      prover_public_params.common_pp.nb_of_t_chunks )
end

module type S = sig
  module PP : Polynomial_protocol.S
  include Plonk.Main_protocol.S with type Scalar.t = PP.PC.Scalar.t
  module Gates : Plonk.Custom_gates.Aggregator_sig with module PP := PP
  module Perm : Plonk.Permutation_gate.S with module PP := PP

  val get_gen_n_t : prover_public_parameters -> scalar * int * int

  type prover_aux = {
    answers : scalar SMap.t SMap.t list;
    batch : scalar SMap.t list;
    alpha : scalar;
    beta : scalar;
    gamma : scalar;
    delta : scalar;
    x : scalar;
    r : scalar;
    cm_answers : scalar;
    cm_pi : scalar;
  }

  type verifier_aux = {
    alpha : scalar;
    beta : scalar;
    gamma : scalar;
    delta : scalar;
    x : scalar;
    r : scalar;
  }

  val prove_list :
    prover_public_parameters -> inputs:prover_inputs -> proof * prover_aux

  val verify_list :
    verifier_public_parameters ->
    nb_proofs:int ->
    proof * scalar SMap.t list * scalar * scalar ->
    bool * verifier_aux
end

module Make : functor
  (PP : Polynomial_protocol.S with type PC.Scalar.t = Plompiler.S.t)
  ->
  S
    with module PP = PP
     and type circuit_verifier_input = PP.PC.Scalar.t array list =
  Make_impl

include Make (Polynomial_protocol)