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 Make (PP : Polynomial_protocol.Polynomial_protocol_sig) = struct
  module Scalar = PP.PC.Scalar
  module Domain = PP.PC.Polynomial.Domain
  module Poly = PP.PC.Polynomial.Polynomial
  module Evaluations = PP.Evaluations

  module Perm : Permutation_gate.Permutation_gate_sig with module PP = PP =
    Permutation_gate.Permutation_gate (PP)

  module Plook : Plookup_gate.Plookup_gate_sig with module PP = PP =
    Plookup_gate.Plookup_gate (PP)

  module Gates = Custom_gate.Custom_gate_impl (PP)
  module Commitment = PP.PC.Commitment
  module Fr_generation = Fr_generation.Make (Scalar)
  module SMap = SMap

  exception Entry_not_in_table = Plook.Entry_not_in_table
  exception Rest_not_null = Poly.Rest_not_null
  exception Wrong_transcript = PP.Wrong_transcript

  type scalar = Scalar.t

  type proof = {
    perm_and_plook : PP.PC.Commitment.t;
    wires_cm : PP.PC.Commitment.t;
    proof : PP.proof;
  }

  let proof_encoding : proof Data_encoding.t =
    Data_encoding.(
      conv
        (fun { perm_and_plook; wires_cm; proof } ->
          (perm_and_plook, wires_cm, proof))
        (fun (perm_and_plook, wires_cm, proof) ->
          { perm_and_plook; wires_cm; proof })
        (obj3
           (req "perm_and_plook" PP.PC.Commitment.encoding)
           (req "wires_cm" PP.PC.Commitment.encoding)
           (req "proof" PP.proof_encoding)))

  type transcript = PP.transcript

  let scalar_encoding = Encodings.fr_encoding
  let transcript_encoding : transcript Data_encoding.t = PP.transcript_encoding

  type prover_inputs = { public : scalar array; witness : scalar array }

  let sep = SMap.Aggregation.sep

  module IntSet = Set.Make (Int)

  (* key = int, intended to be bound to int set *)
  module IntMap = Map.Make (Int)

  module Partition = struct
    type t = IntSet.t IntMap.t

    (* receives [wire_indices], a map from wire names (e.g. "a", "b", "c") to
       [int list], flattens its data into a concatenated list of indices [idxs]
       and outputs a map keyed by indices, pointing to the set of (integer)
       positions where the index appears in [idxs] *)
    let build_partition wire_indices =
      (* [add_IntMap i e map] adds [e] to the set bound to [i] in [map],
         if [i] is not bound, it binds [i] to the singleton set {e} *)
      let add_IntMap i e map =
        let set = Option.value (IntMap.find_opt i map) ~default:IntSet.empty in
        IntMap.add i (IntSet.add e set) map
      in
      let idxs = List.map snd (SMap.bindings wire_indices) in
      let map, _i =
        List.fold_left
          (fun (int_map, i) wire_indices_i ->
            let new_map, j =
              Array.fold_left
                (fun (map, j) h ->
                  let new_map = add_IntMap h (i + j) map in
                  (new_map, j + 1))
                (int_map, 0) wire_indices_i
            in
            (new_map, i + j))
          (IntMap.empty, 0) idxs
      in
      map

    (* returns a permutation in the form of [int array] which splits in cycles
       that involve the indices of each group in the given [partition], e.g.
       on input partition := { 0 -> { 0; 3; 4 } ; 1 -> { 1; 2 } }
       outputs permutation [| 3 2 1 4 0 |] *)
    let partition_to_permutation partition =
      let kn =
        IntMap.fold (fun _ set sum -> sum + IntSet.cardinal set) partition 0
      in
      (* array initialisation *)
      let permutation = Array.make kn (-1) in
      let set_cycle_in_permutation _idx cycle =
        match IntSet.cardinal cycle with
        | 0 -> failwith "cycles_to_permutation_map_set : empty cycle"
        | 1 ->
            (* σ(e) = e *)
            let e = IntSet.choose cycle in
            permutation.(e) <- e
        | n ->
            let first = IntSet.min_elt cycle in
            let aux e (i, prec) =
              if i = 0 then (i + 1, e)
              else if i < n - 1 then (
                permutation.(prec) <- e;
                (i + 1, e))
              else (
                permutation.(prec) <- e;
                permutation.(e) <- first;
                (i + 1, e))
            in
            ignore @@ IntSet.fold aux cycle (0, -1)
      in
      IntMap.iter set_cycle_in_permutation partition;
      (* If cycles is a legit partition of [kn], no -1 should be left *)
      if Array.mem (-1) permutation then
        failwith "cycles is not a 'partition' of kn"
      else permutation
  end

  let module_list =
    [
      (module Gates.Constant_gate : Gates.Gate_base_sig);
      (module Gates.Public_gate);
      (module Gates.AddLeft_gate);
      (module Gates.AddRight_gate);
      (module Gates.AddOutput_gate);
      (module Gates.AddNextLeft_gate);
      (module Gates.AddNextRight_gate);
      (module Gates.AddNextOutput_gate);
      (module Gates.Multiplication_gate);
      (module Gates.X5_gate);
      (module Gates.AddWeierstrass_gate);
      (module Gates.AddEdwards_gate);
    ]

  let select_modules gate_names =
    let to_q_label m =
      let module M = (val m : Gates.Gate_base_sig) in
      M.q_label
    in
    List.filter (fun m -> SMap.mem (to_q_label m) gate_names) module_list

  let get_wires_names nb_wires =
    let alphabet = "abcdefghijklmnopqrstuvwxyz" in
    Array.init nb_wires (fun i -> Char.escaped alphabet.[i])

  let hash_public_inputs transcript public_inputs =
    let open Utils.Hash in
    let st = init () in
    update st transcript;
    SMap.iter
      (fun key (elt : scalar array list) ->
        update st (Bytes.of_string key);
        List.iter (Array.iter (fun s -> update st (Scalar.to_bytes s))) elt)
      public_inputs;
    finish st

  module Prover = struct
    (* - n      : upper-bound on the number of constraints in a circuit
       - domain : (n powers of an n-th root of unity, n)
       - pp_public_parameters : polynomial protocol prover parameters
       - evaluations : FFT evaluations of commonly used
                       polynomials for all circuits, e.g. L1, Si1, Si2, Si3, X.
                       Each evaluation is on a domain that may be bigger than
                       [domain] the size is [4n] for most polynomials and [8n]
                       for some of them. For that, there must exist a [8n]-th
                       root of unity in the scalar field.
       - common_keys : name of the polynomials in evaluations, some are also
                       selector polynomials, is that intentional? *)
    type prover_common_pp = {
      n : int;
      (* domain is n powers of omega *)
      domain : Domain.t;
      pp_public_parameters : PP.prover_public_parameters;
      (* evalautions is a map of about 5 polynomials:  L1, Si1, Si2, Si3, X *)
      evaluations : Evaluations.t SMap.t;
      common_keys : string list;
    }

    (* - circuit_size : number of constraints in the circuit
       - nb_wires : wire architecture (number of wires per gate, typically 3)
       - gates : map from selector names to an array of selector coefficients
                 (one selector coefficient per constraint).
                 The length of such array is the domain size (also n). If there
                 are fewer constraints than n, the array is padded with 0's.
                 An exception is qpub! It seems to always have an array of
                 length 0!
       - tables : [tables] is a list of scalar arrays, one per wire, so the list
                 length is nb_wires, typically 3.
                 Each array is the concatenation of one of the columns of all
                 Plookup tables. (One column per wire, tables which use fewer
                 columns are completed with dummy ones).
                 Each scalar array is a concatenation of tables
       - wires : map from wire names to an array of indices (one index per
                 constraint representing the variable that such wire takes at
                 that constraint).
                 Again, the length of such array is the domain size (i.e. n).
                 If there are fewer constraints than n, the array is padded with
                 the last array element.
                 Is this important? A few times I saw a padding with a 0!
       - permutation: indices corresponding to a permutation that preserves
                 [wires]. Its length is [n * nb_wires], typically [3n] and
                 should be maximal in the sense that it splits in as many cycles
                 as there are variables in the circuit.
       - evaluations : similar as the common_pp evaluations, but for the
                 circuit-specific polynomials (selectors, Ss_i, plookup polys).
       - alpha : scalar used by plookup.
       - ultra : flag to specify whether plookup is being used. *)
    type prover_circuit_pp = {
      circuit_size : int;
      nb_wires : int;
      (* One gate per selector 14 * n *)
      gates : Scalar.t array SMap.t;
      tables : Scalar.t array list;
      (* 3n integers *)
      wires : int array SMap.t;
      (* 3n integers : permutation [3n] -> [3n] *)
      permutation : int array;
      (* A map of about 14 entries
         (polynomials ql, qr, qo, qc, qm, qlg, qrg, qog,
          qx5, qecc, ... Ss1, Ss2, Ss3 )
         14 * 8n scalars *)
      evaluations : Evaluations.t SMap.t;
      alpha : Scalar.t;
      ultra : bool;
    }

    let enforce_wire_values wire_indices wire_values =
      SMap.map
        (fun l -> Array.map (fun index -> wire_values.(index)) l)
        wire_indices

    let compute_wire_polynomials ~zero_knowledge ~module_list n domain wires =
      let unblinded_res =
        try SMap.map (fun w -> Evaluations.interpolation_fft2 domain w) wires
        with Invalid_argument _ ->
          failwith
            "Compute_wire_polynomial : x's length does not match with circuit. \
             Either your witness is too short, or some indexes in a, b or c \
             are greater than the witness size."
      in
      if zero_knowledge then
        let nb_blinds_map =
          Gates.Gate_aggregator.aggregate_blinds ~module_list
        in
        let polys_and_blinds =
          SMap.mapi
            (fun name f ->
              (* 1 more blind is added for the commitment evaluation *)
              let nb_blinds =
                1 + Option.value ~default:0 (SMap.find_opt name nb_blinds_map)
              in
              Poly.blind ~nb_blinds n f)
            unblinded_res
        in
        (SMap.map fst polys_and_blinds, Some (SMap.map snd polys_and_blinds))
      else (unblinded_res, None)

    type wires_info = {
      wires : scalar array SMap.t;
      f_wires_map : Evaluations.polynomial SMap.t;
      f_blinds_map : Evaluations.polynomial SMap.t option;
      wires_values : scalar array;
      wires_indices : int array SMap.t;
    }

    let build_wires_map ?(zero_knowledge = true) common_pp circuits_map
        circuit_name inputs =
      let pp : prover_circuit_pp = SMap.find circuit_name circuits_map in
      let module_list = select_modules pp.gates in
      (* compute the list of wires related values *)
      List.map
        (fun input ->
          let wires_values = input.witness in
          let wires_indices = pp.wires in
          let wires = enforce_wire_values wires_indices wires_values in
          let f_wires_map, f_blinds_map =
            compute_wire_polynomials ~zero_knowledge ~module_list common_pp.n
              common_pp.domain wires
          in
          ( f_wires_map,
            { wires; f_wires_map; f_blinds_map; wires_values; wires_indices } ))
        inputs
      |> List.split

    let build_all_f_wires_map ~zero_knowledge common_pp circuits_map inputs_map
        =
      let wires =
        SMap.mapi
          (build_wires_map ~zero_knowledge common_pp circuits_map)
          inputs_map
      in
      (SMap.map fst wires, SMap.map snd wires)

    (* The shared permutation argument consists of leveraging the fact that
       all proofs of the same circuit type share the same permutation
       for ensuring the copy-satisfiability.
       This allows us to run a single permutation argument on a linear
       combination of the wire polynomials of all same-circuit proofs.
       Namely, let a_i(X), b_i(X), c_i(X) be the wire polynomials of the
       i-th proof. Let delta be some scalar sampled after (and based on)
       a commitment to all a_i, b_i, c_i and consider batched polynomials:
       A(X) := \sum_i delta^{i-1} a_i(X)
       B(X) := \sum_i delta^{i-1} b_i(X)
       C(X) := \sum_i delta^{i-1} c_i(X)
       We will perform a single permutation argument for A, B and C. *)
    let build_aggregated_wires_map ~zero_knowledge delta common_pp circuits_map
        wires_map circuit_name batched_witness =
      let pp : prover_circuit_pp = SMap.find circuit_name circuits_map in
      (* FIXME: remove this naive conversion from C to OCaml *)
      let ocaml_batched_witness = Evaluations.to_array batched_witness in
      let wires = enforce_wire_values pp.wires ocaml_batched_witness in
      let batched_polys =
        fst
        @@ compute_wire_polynomials ~zero_knowledge:false ~module_list:[]
             common_pp.n common_pp.domain wires
      in
      if not zero_knowledge then batched_polys
      else
        (* delta is only used to batched the blinds, the polys are computed
           from a witness batched with delta already *)
        let wires = SMap.find circuit_name wires_map in
        let batched_blinds =
          let blinds = List.map (fun w -> Option.get w.f_blinds_map) wires in
          SMap.map_list_to_list_map blinds |> SMap.map (Poly.batch delta)
        in
        let zh =
          Poly.of_coefficients
            [ (Scalar.one, common_pp.n); (Scalar.negate Scalar.one, 0) ]
        in
        SMap.mapi
          (fun name f ->
            let b = SMap.find name batched_blinds in
            Poly.(f + (b * zh)))
          batched_polys

    (* compute the batched polynomials A, B, C for the shared-permutation
       argument; polynomial A (analogously B and C) can be computed by
       batching polynomials a_i with powers of delta; or alternatively, by
       applying an IFFT interpolation on the batched witness; we expect
       the latter to be more efficient if the number of batched proofs
       is over the threshold of [log2(n)] proofs, where [n] is the domain
       size: this is because polynomial batching would require about
       [n * nb_proofs] scalar operations (per polynomial) whereas the IFFT
       would need [n * log2(n)]; such theoretical threshold has also been
       empirically sustained with benchmarks *)
    let build_all_aggregated_wires_map ~zero_knowledge delta common_pp
        circuits_map f_wires_map_list_map wires_map batched_witness_map =
      SMap.mapi
        (fun circuit_name map_list ->
          let logn = Z.log2 @@ Z.of_int common_pp.n in
          if List.compare_length_with map_list logn > 0 then
            (* we apply an IFFT on the batched witness *)
            let batched_witness = SMap.find circuit_name batched_witness_map in
            build_aggregated_wires_map ~zero_knowledge delta common_pp
              circuits_map wires_map circuit_name batched_witness
          else
            (* we batched the a_i polynomials (analogously for b_i and c_i) *)
            SMap.map (Poly.batch delta) @@ SMap.map_list_to_list_map map_list)
        f_wires_map_list_map

    let add_prefix_to_query ~prefix (query : PP.prover_query) =
      let precomputed_polys =
        SMap.bindings query.precomputed_polys
        |> List.map (fun (key, x) -> (prefix ^ key, x))
        |> SMap.of_list
      in
      { query with precomputed_polys }

    let build_query (common_pp : prover_common_pp) beta_plonk gamma_plonk
        beta_plookup gamma_plookup generator circuits_map inputs_map
        f_perm_map_map circuit_name f_map_list =
      let pp = SMap.find circuit_name circuits_map in
      let inputs = SMap.find circuit_name inputs_map in
      let f_perm_map = SMap.find circuit_name f_perm_map_map in
      let domain_evals = Evaluations.get_domain common_pp.evaluations in
      let g_evals = SMap.union_disjoint common_pp.evaluations pp.evaluations in
      let extra_prefix = if circuit_name = "" then "" else circuit_name ^ sep in
      let query_list =
        List.map2
          (fun f_map inputs ->
            let evaluations =
              PP.Evaluations.compute_evaluations ~domain:domain_evals f_map
              |> SMap.union_disjoint g_evals
            in
            let plookup_query =
              if pp.ultra then
                Plook.prover_query ~prefix:extra_prefix
                  ~wires_name:(get_wires_names pp.nb_wires)
                  ~generator ~alpha:pp.alpha ~beta:beta_plookup
                  ~gamma:gamma_plookup ~f_map ~ultra:pp.ultra ~evaluations
                  ~n:common_pp.n ()
              else PP.empty_prover_query
            in
            let gates_queries =
              Gates.Gate_aggregator.aggregate_prover_queries
                ~prefix:extra_prefix ~module_list:(select_modules pp.gates)
                ~public_inputs:inputs.public ~domain:common_pp.domain
                ~evaluations ()
            in
            let queries = [ plookup_query; gates_queries ] in
            PP.merge_prover_queries queries)
          f_map_list inputs
      in
      let perm_query =
        let evaluations =
          PP.Evaluations.compute_evaluations ~domain:domain_evals f_perm_map
          |> SMap.union_disjoint g_evals
        in
        Perm.prover_query ~prefix:extra_prefix
          ~wires_name:
            (get_wires_names pp.nb_wires |> Array.map String.capitalize_ascii)
          ~generator ~beta:beta_plonk ~gamma:gamma_plonk ~evaluations
          ~n:common_pp.n ()
      in
      (* get the pre-computed polynomials to avoid renaming them
         as we want to open them once only *)
      let v_map = PP.((List.hd query_list : PP.prover_query).v_map) in
      let common_keys =
        PP.update_common_keys_with_v_map common_pp.common_keys ~v_map
      in
      let nb_proofs = List.length inputs in
      let len_prefix = SMap.Aggregation.compute_len_prefix ~nb_proofs in
      (* merge all queries without renaming pre computed-polynomials *)
      let aggregated_query =
        PP.merge_equal_set_of_keys_prover_queries ~extra_prefix ~len_prefix
          ~common_keys query_list
      in
      let perm_query = add_prefix_to_query ~prefix:extra_prefix perm_query in
      PP.merge_prover_queries [ perm_query; aggregated_query ]

    let build_all_queries (common_pp : prover_common_pp) beta_plonk gamma_plonk
        beta_plookup gamma_plookup circuits_map inputs_map f_perm_map_map
        f_map_list_map =
      let generator = Domain.get common_pp.domain 1 in
      let map =
        SMap.mapi
          (build_query common_pp beta_plonk gamma_plonk beta_plookup
             gamma_plookup generator circuits_map inputs_map f_perm_map_map)
          f_map_list_map
      in
      PP.merge_prover_queries (List.map snd (SMap.bindings map))

    let build_f_map_evaluation_perm ~zero_knowledge (cpp : prover_common_pp)
        delta beta_plonk gamma_plonk circuits_map circuit_name wires =
      let pp = SMap.find circuit_name circuits_map in
      let batched_witness =
        let deltas =
          Fr_generation.powers (List.length wires) delta |> Array.to_list
        in
        (* FIXME: remove this naive conversion from OCaml to C, i.e.,
           load inputs in the correct format *)
        let wire_values_c_list =
          List.map
            (fun wires_info ->
              let degree = Array.length wires_info.wires_values - 1 in
              Evaluations.make_evaluation (degree, wires_info.wires_values))
            wires
        in
        Evaluations.linear_c ~evaluations:wire_values_c_list
          ~linear_coeffs:deltas ()
      in
      (* Note that [wire_indices] are supposed to be the same across all
         blinds at this level, since they are about the same circuit *)
      let zs =
        let indices = (List.hd wires).wires_indices in
        Perm.f_map_contribution ~permutation:pp.permutation
          ~values:batched_witness ~indices ~beta:beta_plonk ~gamma:gamma_plonk
          ~domain:cpp.domain
      in
      let zs =
        if zero_knowledge then
          SMap.map (fun f -> Poly.blind ~nb_blinds:3 cpp.n f |> fst) zs
        else zs
      in
      (zs, batched_witness)

    let build_all_f_map_evaluation_perm ~zero_knowledge pp delta beta_plonk
        gamma_plonk circuits_map wires_map =
      SMap.mapi
        (build_f_map_evaluation_perm ~zero_knowledge pp delta beta_plonk
           gamma_plonk circuits_map)
        wires_map

    let build_f_map_evaluation_plook ~zero_knowledge (cpp : prover_common_pp)
        beta_plookup gamma_plookup circuits_map circuit_name wires =
      let pp = SMap.find circuit_name circuits_map in
      List.map
        (fun wires_info ->
          let plook_map =
            if pp.ultra then
              Plook.f_map_contribution ~wires:wires_info.wires ~gates:pp.gates
                ~tables:pp.tables ~alpha:pp.alpha ~beta:beta_plookup
                ~gamma:gamma_plookup ~domain:cpp.domain ~size_domain:cpp.n
                ~circuit_size:pp.circuit_size
            else SMap.empty
          in
          if zero_knowledge then
            SMap.map (fun f -> Poly.blind ~nb_blinds:3 cpp.n f |> fst) plook_map
          else plook_map)
        wires

    let build_all_f_map_evaluation_plook ~zero_knowledge pp beta_plookup
        gamma_plookup circuits_map wires_map =
      SMap.mapi
        (build_f_map_evaluation_plook ~zero_knowledge pp beta_plookup
           gamma_plookup circuits_map)
        wires_map

    (* flattens a map_list_map into a single map by prefixing keys with circuit
       names and proof indices; for example, on input:
       { 'circuit_foo' -> [ {'a' -> fa0; 'b' -> fb0; 'c' -> fc0};
                            {'a' -> fa1; 'b' -> fb1; 'c' -> fc1} ];
         'circuit_bar' -> [ {'a' -> ga0; 'b' -> gb0; 'c' -> gc0} ]; }
       outputs
       { '0~circuit_foo~a' -> fa0;
         '0~circuit_foo~b' -> fb0
         '0~circuit_foo~c' -> fc0
         '1~circuit_foo~a' -> fa1
         '1~circuit_foo~b' -> fb1
         '1~circuit_foo~c' -> fc1
         '0~circuit_bar~a' -> ga0
         '0~circuit_bar~b' -> gb0
         '0~circuit_bar~c' -> gc0
       } *)
    let gather_maps map_list_map =
      SMap.bindings map_list_map
      |> List.map (fun (circuit_name, map_list) ->
             let nb_proofs = List.length map_list in
             let len_prefix = SMap.Aggregation.compute_len_prefix ~nb_proofs in
             let extra_prefix =
               if circuit_name = "" then ""
               else circuit_name ^ SMap.Aggregation.sep
             in
             SMap.Aggregation.merge_equal_set_of_keys ~extra_prefix ~len_prefix
               map_list)
      |> SMap.union_disjoint_list

    (* similar to [gather_maps] but for permutation maps, in this the index
       prefix is not added, since there is only one map per circuit type *)
    let gather_maps_perm map_map =
      SMap.bindings map_map
      |> List.map (fun (circuit_name, map) ->
             let prefix =
               if circuit_name = "" then ""
               else circuit_name ^ SMap.Aggregation.sep
             in
             SMap.Aggregation.prefix_map ~prefix map)
      |> SMap.union_disjoint_list

    let prove_circuits_with_pool ?(zero_knowledge = true)
        ((common_pp, circuits_map), transcript) ~inputs_map =
      (* add the PI in the transcript*)
      let transcript =
        hash_public_inputs transcript
        @@ SMap.map (List.map (fun sa -> sa.public)) inputs_map
      in
      (* building wire-polynomials *)
      (* the variable name [f_wires_map_list_map] makes explicit its structure,
         the outer map is keyed by a circuit_name, we then have a list (of maps)
         where each element corresponds to a different proof on the same circuit
         type, the inner map keys correspond to polynomial names 'a', 'b', 'c' *)
      let f_wires_map_list_map, wires_map =
        build_all_f_wires_map ~zero_knowledge common_pp circuits_map inputs_map
      in
      let f_wires_map = gather_maps f_wires_map_list_map in
      (* commit to the wire-polynomials *)
      let srs = common_pp.pp_public_parameters.pc_public_parameters in
      let commitment_wires, wires_prover_aux =
        PP.PC.Commitment.commit srs f_wires_map
      in
      (* compute beta & gamma (common for all proofs) *)
      let transcript =
        PP.PC.Commitment.expand_transcript transcript commitment_wires
      in
      (* TODO : unify randomness generation and nomenclature *)
      let betas_gammas, transcript =
        Fr_generation.random_fr_list transcript 5
      in
      let beta_plonk = List.hd betas_gammas in
      let gamma_plonk = List.nth betas_gammas 1 in
      let beta_plookup = List.nth betas_gammas 2 in
      let gamma_plookup = List.nth betas_gammas 3 in
      let delta = List.nth betas_gammas 4 in

      (* computed permutation polynomials, shared across the same circuit *)
      (* the variable name [f_perm_map_map] makes explicit its structure, the
         outer map is keyed by a circuit_name, note that (contrary to
         f_wires_map_list_map, we do not have a list here, since the permutation
         argument is shared across all proofs of the same circuit type, we
         directly have a map of polynomial names, in this case just with one
         single key, 'Z', but we keep the map structure for consistency with
         the rest of the code *)
      let f_perm_and_witness_map_map =
        build_all_f_map_evaluation_perm ~zero_knowledge common_pp delta
          beta_plonk gamma_plonk circuits_map wires_map
      in
      let f_perm_map_map = SMap.map fst f_perm_and_witness_map_map in
      let batched_witness_map = SMap.map snd f_perm_and_witness_map_map in
      let f_perm_map = gather_maps_perm f_perm_map_map in

      (* compute plookup polynomials *)
      let f_plook_map_list_map =
        build_all_f_map_evaluation_plook ~zero_knowledge common_pp beta_plookup
          gamma_plookup circuits_map wires_map
      in
      let f_plook_map = gather_maps f_plook_map_list_map in

      let f_perm_and_plook_map = SMap.union_disjoint f_perm_map f_plook_map in

      (* commit to the permutation (and plookup) polynomials *)
      let cmt_perm_and_plook, perm_and_plook_prover_aux =
        PP.PC.Commitment.commit srs f_perm_and_plook_map
      in
      let transcript =
        PP.PC.Commitment.expand_transcript transcript cmt_perm_and_plook
      in
      (* compute the list of prover queries for all proofs & all circuits *)
      let batched_f_wires_map_map =
        build_all_aggregated_wires_map ~zero_knowledge delta common_pp
          circuits_map f_wires_map_list_map wires_map batched_witness_map
      in
      let updated_f_perm_map_map =
        SMap.mapi
          (fun circuit_name map ->
            SMap.fold
              (fun key f acc -> SMap.add (String.capitalize_ascii key) f acc)
              (SMap.find circuit_name batched_f_wires_map_map)
              map)
          f_perm_map_map
      in
      let query =
        let f_map_list_map =
          SMap.union
            (fun _ l1 l2 ->
              Some (List.map2 (fun m1 m2 -> SMap.union_disjoint m1 m2) l1 l2))
            f_wires_map_list_map f_plook_map_list_map
        in
        build_all_queries common_pp beta_plonk gamma_plonk beta_plookup
          gamma_plookup circuits_map inputs_map updated_f_perm_map_map
          f_map_list_map
      in
      let proof, transcript =
        PP.prove common_pp.pp_public_parameters transcript
          ( [ f_wires_map; f_perm_and_plook_map ],
            [ wires_prover_aux; perm_and_plook_prover_aux ] )
          query
      in
      ( {
          perm_and_plook = cmt_perm_and_plook;
          wires_cm = commitment_wires;
          proof;
        },
        transcript )
  end

  module Verifier = struct
    type verifier_common_pp = {
      n : int;
      generator : Scalar.t;
      pp_public_parameters : PP.verifier_public_parameters;
      query : PP.verifier_query;
      common_keys : string list;
    }

    let verifier_common_pp_encoding : verifier_common_pp Data_encoding.t =
      let open Encodings in
      let open Data_encoding in
      conv
        (fun { n; generator; pp_public_parameters; query; common_keys } ->
          (n, generator, pp_public_parameters, query, common_keys))
        (fun (n, generator, pp_public_parameters, query, common_keys) ->
          { n; generator; pp_public_parameters; query; common_keys })
        (obj5 (req "n" int31)
           (req "generator" fr_encoding)
           (req "pp_public_parameters" PP.verifier_public_parameters_encoding)
           (req "query" PP.verifier_query_encoding)
           (req "common_keys" (list string)))

    type verifier_circuit_pp = {
      gates : unit SMap.t;
      nb_wires : int;
      alpha : Scalar.t;
      ultra : bool;
    }

    let verifier_circuit_pp_encoding : verifier_circuit_pp Data_encoding.t =
      let open Encodings in
      let open Data_encoding in
      conv
        (fun { gates; nb_wires; alpha; ultra } ->
          (gates, nb_wires, alpha, ultra))
        (fun (gates, nb_wires, alpha, ultra) ->
          { gates; nb_wires; alpha; ultra })
        (obj4
           (req "gates" (SMap.encoding unit))
           (req "nb_wires" int31) (req "alpha" fr_encoding) (req "ultra" bool))

    let build_query pp beta_plonk gamma_plonk beta_plookup gamma_plookup
        circuits_map =
      let query_list, gates_query, common_keys =
        SMap.fold
          (fun name (c, inputs, nb_proofs)
               (query_list, gates_query, common_keys) ->
            let prefix = if name = "" then "" else name ^ sep in
            let perm_query =
              Perm.verifier_query ~compute_sid:false ~prefix
                ~wires_name:
                  (get_wires_names c.nb_wires
                  |> Array.map String.capitalize_ascii)
                ~generator:pp.generator ~beta:beta_plonk ~gamma:gamma_plonk
                ~nb_wires:c.nb_wires ()
            in
            let plookup_query =
              if c.ultra then
                Plook.verifier_query ~prefix ~generator:pp.generator
                  ~wires_name:(get_wires_names c.nb_wires)
                  ~alpha:c.alpha ~beta:beta_plookup ~gamma:gamma_plookup
                  ~ultra:c.ultra ()
              else PP.empty_verifier_query
            in
            let common_query =
              PP.merge_verifier_queries [ perm_query; plookup_query ]
            in
            let len_prefix = SMap.Aggregation.compute_len_prefix ~nb_proofs in
            (* We now add the PI polynomial*)
            let gates_query, _ =
              List.fold_left
                (fun (query, i) public_inputs ->
                  let si = SMap.Aggregation.(int_to_string ~len_prefix i) in
                  let prefix = si ^ prefix in
                  ( Gates.Gate_aggregator.add_public_inputs ~prefix
                      ~public_inputs ~generator:pp.generator ~size_domain:pp.n
                      query,
                    i + 1 ))
                (gates_query, 0) inputs
            in
            (* Contains the names of polynomials that have the same value
               for each proof, especially preprocessed polynomials,
                but also later T polynomials, and possibly their evaluations
                in gX if needed by v_maps *)
            (* Merge all queries without renaming pre computed polynomials
               as we want to open them once only. *)
            let new_common_keys =
              let common_perm =
                Perm.z :: Perm.zg
                :: (get_wires_names c.nb_wires |> Array.to_list)
                |> List.map String.capitalize_ascii
              in
              (common_perm |> List.map (fun x -> prefix ^ x))
              @ PP.update_common_keys_with_v_map common_keys
                  ~v_map:common_query.v_map
              |> List.sort_uniq String.compare
            in
            (common_query :: query_list, gates_query, new_common_keys))
          circuits_map
          ([], pp.query, pp.common_keys)
      in
      ( PP.merge_verifier_queries ~common_keys (gates_query :: query_list),
        common_keys )

    (* Assumes the same circuit, i.e. the public parameters are fixed *)
    let verify_circuits ((common_pp, circuits_map), transcript) ~public_inputs
        proof =
      let circuits_map =
        try
          SMap.mapi
            (fun i pi -> (SMap.find i circuits_map, pi, List.length pi))
            public_inputs
        with _ ->
          failwith
            "Main : public inputs maps keys must be included in circuits_map's."
      in
      (* add the PI in the transcript*)
      let transcript = hash_public_inputs transcript public_inputs in
      (* The transcript is the same as the provers's transcript since the proof
         is already aggregated *)
      let transcript =
        PP.PC.Commitment.expand_transcript transcript proof.wires_cm
      in
      (* Get the same randomness for all proofs *)
      (* Step 1a : compute beta & gamma *)
      let betas_gammas, transcript =
        Fr_generation.random_fr_list transcript 5
      in
      let beta_plonk = List.hd betas_gammas in
      let gamma_plonk = List.nth betas_gammas 1 in
      let beta_plookup = List.nth betas_gammas 2 in
      let gamma_plookup = List.nth betas_gammas 3 in
      let delta = List.nth betas_gammas 4 in
      (* Step 3 : compute verifier’s identities *)
      (* common_keys is the list of the names of polynomials that have the same value for each proof, especially preprocessed polynomials, but also later T polynomials, and possibly their evaluations in gX if needed by v_maps *)
      let query, common_keys =
        build_query common_pp beta_plonk gamma_plonk beta_plookup gamma_plookup
          circuits_map
      in
      (* Build multi-variate polynomials for evaluating the batched A, B, C *)
      let not_committed_online =
        SMap.fold
          (fun circuit_name (c, _, nb_proofs) acc ->
            let extra_prefix =
              if circuit_name = "" then "" else circuit_name ^ sep
            in
            let len_prefix = SMap.Aggregation.compute_len_prefix ~nb_proofs in
            Array.fold_left
              (fun acc wire_name ->
                let key = extra_prefix ^ String.capitalize_ascii wire_name in
                let p =
                  Perm.create_batched_wire_poly ~extra_prefix ~len_prefix
                    ~wire_name delta nb_proofs
                in
                SMap.add key p acc)
              acc
              (get_wires_names c.nb_wires))
          circuits_map SMap.empty
      in
      let transcript =
        PP.PC.Commitment.expand_transcript transcript proof.perm_and_plook
      in
      PP.verify
        ~proof_type:
          (PP.Aggregated
             {
               nb_proofs = SMap.map (fun (_, _, n) -> n) circuits_map;
               common_keys;
             })
        common_pp.pp_public_parameters transcript
        [ proof.wires_cm; proof.perm_and_plook ]
        ~not_committed_online proof.proof query
  end

  type prover_public_parameters = {
    common_pp : Prover.prover_common_pp;
    circuits_map : Prover.prover_circuit_pp SMap.t;
  }

  type verifier_public_parameters = {
    common_pp : Verifier.verifier_common_pp;
    circuits_map : Verifier.verifier_circuit_pp SMap.t;
  }

  let verifier_public_parameters_encoding :
      verifier_public_parameters Data_encoding.t =
    Data_encoding.(
      conv
        (fun { common_pp; circuits_map } -> (common_pp, circuits_map))
        (fun (common_pp, circuits_map) -> { common_pp; circuits_map })
        (obj2
           (req "common_pp" Verifier.verifier_common_pp_encoding)
           (req "circuits_map"
              (SMap.encoding Verifier.verifier_circuit_pp_encoding))))

  module Preprocess = struct
    let degree_evaluations ~nb_wires ~zero_knowledge ~gates ~n ~ultra =
      let module_list = select_modules gates in
      let degree_evaluation =
        Gates.Gate_aggregator.aggregate_polynomials_degree ~module_list
      in
      let zk_factor = if zero_knowledge then if n <= 2 then 4 else 2 else 1 in
      let min_deg =
        (* minimum size needed for permutation gate ; if we are in the gate case, nb_wires = 0 => min_perm = 1 which is the minimum degree anyway *)
        let min_perm = Perm.polynomials_degree ~nb_wires in
        if ultra then max (Plook.polynomials_degree ()) min_perm else min_perm
      in
      let max_degree =
        SMap.fold (fun _ d acc -> max d acc) degree_evaluation min_deg
      in
      let len_evals = zk_factor * max_degree * n in
      len_evals

    let domain_evaluations ~nb_wires ~zero_knowledge ~gates ~n ~ultra =
      let len_evals =
        degree_evaluations ~nb_wires ~zero_knowledge ~gates ~n ~ultra
      in
      Domain.build ~log:Z.(log2up (of_int len_evals))

    (* Function preprocessing the circuit wires and selector polynomials;
          Inputs:
          - n: the number of constraints in the circuits + the number of public inputs
       -   domain: the interpolation domain for polynomials of size n
       - s elector_polys: the selector polynomials,
       e.g. [ql, qr, qo, qm, qc] for an arithmetic circuit.
       We assume ql is the first polynomial in the list.
       - wire_indices: the list corresponding to the wires indices,
       e.g. [a, b, c] for an arithmetic circuit
       - l, the number of public inputs
       Outputs:
       - interpolated_polys: selector polynomials, prepended with 0/1s for the public inputs,
       interpolated on the domain
       - extended_wires: circuits wires prepended with wires corresponding to the public inputs
    *)
    let preprocessing ?(prefix = "") domain gates wires tables n l circuit_size
        table_size nb_wires ~ultra =
      (* Updating selectors for public inputs. *)
      let gates =
        (* Define ql if undefined as it is the gate taking the public input in. *)
        if l > 0 && (not @@ SMap.mem "ql" gates) then
          SMap.add "ql" (Array.init circuit_size (fun _ -> Scalar.zero)) gates
        else gates
      in
      (* other preprocessed things in article are computed in prove of permutations *)
      let extended_gates =
        (* Adding 0s/1s for public inputs *)
        SMap.mapi
          (fun label poly ->
            let length_poly = Array.length poly in
            Array.init n (fun i ->
                if i < l && label = "ql" then Scalar.one
                else if l <= i && i < l + length_poly then poly.(i - l)
                else Scalar.zero))
          gates
      in
      (* renommage des portes *)
      let extended_gates = SMap.Aggregation.prefix_map ~prefix extended_gates in
      let interpolated_gates =
        SMap.map (Evaluations.interpolation_fft2 domain) extended_gates
      in
      let extended_gates =
        if l = 0 then extended_gates
        else SMap.add (prefix ^ "qpub") [||] extended_gates
      in
      let extended_wires =
        let li_array = Array.init l (fun i -> i) in
        (* Adding public inputs and resizing *)
        SMap.map (fun w -> Utils.pad (Array.append li_array w) n) wires
      in
      let extended_tables =
        if not ultra then []
        else
          Plook.format_tables ~tables ~nb_columns:nb_wires
            ~length_not_padded:table_size ~length_padded:n
      in
      (interpolated_gates, extended_gates, extended_wires, extended_tables)

    let preprocess_map domain domain_evals n circuits_map =
      (* Preprocessing wires, gates and tables *)
      SMap.fold
        (fun name ((c : Circuit.t), _) (prv, vrf, all_g_maps, gates_query) ->
          (* Generating alpha for Plookup *)
          let alpha = Scalar.random () in
          let gates_poly, gates, wires, tables =
            preprocessing domain c.gates c.wires c.tables n c.public_input_size
              c.circuit_size c.table_size c.nb_wires ~ultra:c.ultra
          in
          (* Generating permutation *)
          let permutation =
            let partition = Partition.build_partition wires in
            Partition.partition_to_permutation partition
          in
          (* Computing g_map *)
          let g_map_perm =
            Perm.preprocessing ~domain ~nb_wires:c.nb_wires ~permutation ()
          in
          let g_map_plook =
            if c.ultra then Plook.preprocessing ~domain ~tables ~alpha ()
            else SMap.empty
          in
          let circuit_g_map =
            SMap.union_disjoint_list [ g_map_plook; g_map_perm; gates_poly ]
          in
          let evaluations =
            Evaluations.compute_evaluations ~domain:domain_evals circuit_g_map
          in
          let prefix = if name = "" then "" else name ^ sep in
          let prover_pp =
            Prover.
              {
                circuit_size = c.circuit_size;
                nb_wires = c.nb_wires;
                gates;
                tables;
                wires;
                evaluations;
                permutation;
                alpha;
                ultra = c.ultra;
              }
          in

          let generator = Domain.get domain 1 in
          let c_gates_query =
            (* Compute gate_query without PI’s not_committed *)
            Gates.Gate_aggregator.aggregate_verifier_queries ~prefix
              ~module_list:(select_modules gates) ~generator ~size_domain:n ()
          in
          let verifier_pp =
            let gates = SMap.map (fun _ -> ()) gates in
            Verifier.{ gates; nb_wires = c.nb_wires; alpha; ultra = c.ultra }
          in
          let g_map =
            SMap.(
              union_disjoint all_g_maps
                (Aggregation.prefix_map ~prefix circuit_g_map))
          in
          ( SMap.(union_disjoint prv (singleton name prover_pp)),
            SMap.(union_disjoint vrf (singleton name verifier_pp)),
            g_map,
            PP.merge_verifier_queries [ c_gates_query; gates_query ] ))
        circuits_map
        SMap.(empty, empty, empty, PP.empty_verifier_query)

    let compute_sizes ~zero_knowledge
        Circuit.
          {
            public_input_size;
            circuit_size;
            nb_wires;
            table_size;
            nb_lookups;
            ultra;
            gates;
            _;
          } nb_proofs =
      (* Computing domain *)
      (* For TurboPlonk, we want a domain of size a power of two
         higher than or equal to the number of constraints plus public inputs.
         As for UltraPlonk, a domain of size stricly higher than the number of constraints
         (to be sure we pad the last lookup). *)
      let nb_cs_pi =
        circuit_size + public_input_size + if ultra then 1 else 0
      in
      (* For UltraPlonk, we want a domain of size a power of two
         higher than the number of records and strictly higher than the number of lookups *)
      let nb_rec_look = if ultra then max (nb_lookups + 1) table_size else 0 in
      let max_nb = max nb_cs_pi nb_rec_look in
      let log = Z.(log2up (of_int max_nb)) in
      let n = Int.shift_left 1 log in
      (* Computing SRS size *)
      let srs_size =
        let srs_size_plonk = Perm.srs_size ~zero_knowledge ~n in
        if ultra then
          let srs_size_plookup = Plook.srs_size ~length_table:n in
          max srs_size_plonk srs_size_plookup + 1
        else srs_size_plonk
      in
      let pack_size =
        (* L1, Ssi, selectors, ultra stuff *)
        let nb_g_map_polys =
          let ultra_polys = if ultra then 2 else 0 in
          1 + nb_wires + SMap.cardinal gates + ultra_polys
        in
        let nb_extra_polys = if ultra then 5 else 1 in
        let online = max nb_wires nb_extra_polys * nb_proofs in
        (* 5 stands for the max number of T polynomials, if we split T *)
        let offline = max nb_g_map_polys 5 in
        (* Multiply by 2 to have more than needed, just in case *)
        2 * max online offline
      in
      (log, n, srs_size, pack_size)

    let get_sizes ~zero_knowledge circuits_map =
      let log, n, max_d, total_pack, some_ultra =
        SMap.fold
          (fun _ (c, nb_proofs)
               (acc_log, acc_n, acc_srs_size, acc_pack_size, acc_ultra) ->
            let log, n, srs_size, pack_size =
              compute_sizes ~zero_knowledge c nb_proofs
            in
            ( max acc_log log,
              max acc_n n,
              max acc_srs_size srs_size,
              acc_pack_size + pack_size,
              acc_ultra || c.ultra ))
          circuits_map (0, 0, 0, 0, false)
      in
      let len_evals =
        SMap.fold
          (fun _ ((c : Circuit.t), _) acc_deg_eval ->
            let deg_eval =
              degree_evaluations ~nb_wires:c.nb_wires ~zero_knowledge
                ~gates:c.gates ~n ~ultra:c.ultra
            in
            max acc_deg_eval deg_eval)
          circuits_map 0
      in
      let domain_evals = Domain.build ~log:Z.(log2up (of_int len_evals)) in
      let domain = Domain.build ~log in
      let total_pack = 1 lsl Z.(log2up (of_int total_pack)) in
      (domain, n, max_d, total_pack, domain_evals, some_ultra)

    let setup_circuits_with_pool ?(zero_knowledge = true) circuits_map ~srsfiles
        =
      let domain, n, srs_size, pack_size, domain_evals, some_ultra =
        get_sizes ~zero_knowledge circuits_map
      in
      let g_map_common, evaluations, sid_verifier_query =
        let g_map_perm, evaluations_perm, sid_verifier_query =
          Perm.common_preprocessing ~compute_l1:(not some_ultra) ~domain
            ~nb_wires:3 (* Fixme what should we keep this nb_wires as it is ? *)
            ~domain_evals
        in
        let g_map_plook =
          if some_ultra then Plook.common_preprocessing ~n ~domain
          else SMap.empty
        in
        let g_map = SMap.union_disjoint g_map_perm g_map_plook in
        (* Add X evaluations, which is the domain needed for other evaluations *)
        let evaluations =
          SMap.add "X" (Evaluations.of_domain domain_evals) evaluations_perm
        in
        ( g_map,
          Evaluations.compute_evaluations_update_map ~evaluations g_map,
          sid_verifier_query )
      in
      let pp_prv, pp_vrf, g_map, gates_query =
        preprocess_map domain domain_evals n circuits_map
      in
      let query =
        PP.merge_verifier_queries [ sid_verifier_query; gates_query ]
      in
      let g_map = SMap.union_disjoint g_map g_map_common in
      (* Generating public parameters *)
      let pp_prover, pp_verifier =
        PP.setup ~setup_params:(srs_size, pack_size) g_map ~subgroup_size:n
          srsfiles
      in
      (* Generating transcript *)
      let transcript =
        let pc_public_parameters = pp_prover.pc_public_parameters in
        let tmp = PP.PC.Public_parameters.to_bytes pc_public_parameters in
        PP.PC.Commitment.expand_transcript tmp pp_verifier.cm_g_map
      in
      let common_keys =
        let common_keys = List.map fst (SMap.bindings g_map) in
        if some_ultra then common_keys @ [ "Si1"; "Si2"; "Si3"; "x_minus_1" ]
        else common_keys @ [ "Si1"; "Si2"; "Si3" ]
      in
      let common_prv =
        Prover.
          {
            n;
            domain;
            pp_public_parameters = pp_prover;
            evaluations;
            common_keys;
          }
      in
      let common_vrf =
        Verifier.
          {
            n;
            generator = Domain.get domain 1;
            pp_public_parameters = pp_verifier;
            query;
            common_keys;
          }
      in
      ( ( ({ common_pp = common_prv; circuits_map = pp_prv }
            : prover_public_parameters),
          { common_pp = common_vrf; circuits_map = pp_vrf } ),
        transcript )
  end

  let check_circuit_name map =
    SMap.iter
      (fun name _ ->
        if name = "" then ()
        else if Char.compare name.[0] '9' <= 0 then
          failwith
            (Printf.sprintf "check_circuit_name : circuit name (= '%s')" name
            ^ " must not begin with '\\', '#', '$', '%', '&', ''', '(', ')', \
               '*', '+', ',', '-', '.', '/' or a digit.")
        else if String.contains name SMap.Aggregation.sep.[0] then
          failwith
            (Printf.sprintf
               "check_circuit_name : circuit name (= '%s') mustn't contain '%s'"
               name SMap.Aggregation.sep))
      map

  let setup_multi_circuits ?(zero_knowledge = true)
      ?(num_additional_domains = 0) circuits_map ~srsfiles =
    check_circuit_name circuits_map;
    Multicore.with_pool ~num_additional_domains (fun () ->
        Preprocess.setup_circuits_with_pool ~zero_knowledge circuits_map
          ~srsfiles)

  (* inputs is a map between circuit names to list of public inputs *)
  let prove_multi_circuits ?(zero_knowledge = true)
      ?(num_additional_domains = 0)
      ((pp : prover_public_parameters), transcript) ~inputs =
    check_circuit_name pp.circuits_map;
    Multicore.with_pool ~num_additional_domains (fun () ->
        Prover.prove_circuits_with_pool ~zero_knowledge
          ((pp.common_pp, pp.circuits_map), transcript)
          ~inputs_map:inputs)

  let verify_multi_circuits (pp, transcript) ~public_inputs proof =
    check_circuit_name pp.circuits_map;
    Multicore.with_pool ~num_additional_domains:0 (fun () ->
        Verifier.verify_circuits
          ((pp.common_pp, pp.circuits_map), transcript)
          ~public_inputs proof)

  let setup ?(zero_knowledge = true) ?(num_additional_domains = 0) circuit
      ~srsfiles ~nb_proofs =
    let circuits_map = SMap.singleton "" (circuit, nb_proofs) in
    Multicore.with_pool ~num_additional_domains (fun () ->
        Preprocess.setup_circuits_with_pool ~zero_knowledge circuits_map
          ~srsfiles)

  (* Prover function:
      proves a statement for some inputs

     computes the wires polynomials
     and calls Polynomial Protocol on the identities of the gates needed,
     the Permutation (copy-satisfaction) & optionally Plookup
      Inputs:
      - transcript: transcript initialized with SRS
      - public_parameters: (output of setup for the statement)
        - domain: the interpolation domain for polynomials of size n
        - n: the number of constraints in the circuits + the number of public inputs
        - wires: the int list representation for each wire’s indices
        - gates: the scalar list representation for each gate
        - tables: the representation of tables
        - pp_public_parameters: public parameters of Polynomial_protocol
        - permutation: the int array representation for the permutation defined by the circuit
        - alpha: the random scalar for plookup
        - ultra: true if Plookup gate must be called
        - circuit_size: the number of constraints in the circuit
        - nb_wires: the number of wires
        - evaluations: the (degree, fft evaluation) of preprocessed polynomials
      - private_inputs: the values of the wires
      - public_inputs: the firsts values of private_inputs that are public
      Outputs:
      - a unique zk-snark
  *)
  (* TODO : add antireplay arg *)
  let prove ?(zero_knowledge = true) ?(num_additional_domains = 0) pp ~inputs =
    let inputs_map = SMap.singleton "" [ inputs ] in
    prove_multi_circuits ~zero_knowledge ~num_additional_domains pp
      ~inputs:inputs_map

  let verify pp ~public_inputs proof =
    let public_inputs = SMap.singleton "" [ public_inputs ] in
    verify_multi_circuits pp ~public_inputs proof
end

module type Main_protocol_sig = sig
  exception Entry_not_in_table of string
  exception Rest_not_null of string
  exception Wrong_transcript of string

  module SMap : SMap.StringMap_sig

  type scalar = Bls12_381.Fr.t

  val scalar_encoding : scalar Data_encoding.t

  type transcript
  type prover_public_parameters
  type verifier_public_parameters

  val verifier_public_parameters_encoding :
    verifier_public_parameters Data_encoding.t

  type proof

  val proof_encoding : proof Data_encoding.t

  type prover_inputs = { public : scalar array; witness : scalar array }

  val transcript_encoding : transcript Data_encoding.t

  (* Computes the public parameters needed for prove & verify from a circuit
     Inputs:
     - zero_knowledge: true if wires polynomials have to be blinded
     - circuit: output from Circuit.make
     - srsfile: the name of SRS file in the srs folder from where the SRS will be imported
     Outputs:
     - public_parameters & transcript
  *)
  val setup :
    ?zero_knowledge:bool ->
    ?num_additional_domains:int ->
    Circuit.t ->
    srsfiles:(string * string) * (string * string) ->
    nb_proofs:int ->
    (prover_public_parameters * verifier_public_parameters) * transcript

  (* Prover function: computes the wires polynomials and calls Polynomial Protocol on the identities of the gates needed, the Permutation (copy-satisfaction) & optionally Plookup
     Inputs:
     - zero_knowledge: true if wires polynomials have to be blinded
     - transcript: transcript initialized with SRS
     - public_parameters: output of setup
     - private_inputs: the values of the wires
     - public_inputs: the firsts values of private_inputs that are public
     Outputs:
     - zk-snark
  *)
  val prove :
    ?zero_knowledge:bool ->
    ?num_additional_domains:int ->
    prover_public_parameters * transcript ->
    inputs:prover_inputs ->
    proof * transcript

  (* Verifier function: checks proof
     Inputs:
     - transcript: transcript initialized with SRS
     - public_parameters: output of setup
     - public_inputs (scalar array): the firsts values of private_inputs that are public
     - proof: output of prove
     Outputs:
     - bool
  *)
  val verify :
    verifier_public_parameters * transcript ->
    public_inputs:scalar array ->
    proof ->
    bool * transcript

  (* Computes the public parameters needed for prove & verify for several circuit
     Inputs:
     - zero_knowledge: true if wires polynomials have to be blinded
     - circuit: a StringMap of (outputs from Circuit.make, upper bound of the number of proofs to aggregate for this circuit) binded with the circuit’s name
     - srsfile: the name of SRS file in the srs folder from where the SRS will be imported
     Outputs:
     - public_parameters & transcript
  *)
  val setup_multi_circuits :
    ?zero_knowledge:bool ->
    ?num_additional_domains:int ->
    (Circuit.t * int) SMap.t ->
    srsfiles:(string * string) * (string * string) ->
    (prover_public_parameters * verifier_public_parameters) * transcript

  (* Prover function: for several circuits & several inputs, computes the wires polynomials and calls Polynomial Protocol on the identities of the gates needed, the Permutation (copy-satisfaction) & optionally Plookup
     Inputs:
     - zero_knowledge: true if wires polynomials have to be blinded
     - transcript: transcript initialized with SRS
     - public_parameters: output of setup
     - private_inputs: the map of the list of values of the wires binded with the circuit name
     - public_inputs: the map of the list of the firsts values of private_inputs that are public,  binded with the circuit name
     Outputs:
     - zk-snark
  *)
  val prove_multi_circuits :
    ?zero_knowledge:bool ->
    ?num_additional_domains:int ->
    prover_public_parameters * transcript ->
    inputs:prover_inputs list SMap.t ->
    proof * transcript

  (* Verifier function: checks a bunch of proofs for several circuits
     Inputs:
     - transcript: transcript initialized with SRS
     - public_parameters: output of setup_multi_circuits for the circuits being checked
     - public_inputs: StringMap where the lists of public inputs are binded with the circuit to which they correspond
     - proof: the unique proof that correspond to all inputs
     Outputs:
     - bool
  *)
  val verify_multi_circuits :
    verifier_public_parameters * transcript ->
    public_inputs:scalar array list SMap.t ->
    proof ->
    bool * transcript
end

include (Make (Polynomial_protocol) : Main_protocol_sig)