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

(**
  aPlonK is a {e PlonK}-based proving system.
  As such, it provides a way to create {e succinct cryptographic proofs}
  about a given predicate, which can be then verified with a low
  computational cost.

  In this system, a predicate is represented by an {e arithmetic circuit},
  i.e. a collection of arithmetic {e gates} operating over a {e prime field},
  connected through {e wires} holding {e scalars} from this field.
  For example, the following diagram illustrates a simple circuit checking that
  the addition of two scalars ([w1] and [w2]) is equal to [w0]. Here,
  the [add] gate can be seen as taking two inputs and producing an output,
  while the [eq] gate just takes two inputs and asserts they're equal.

{[
          (w0)│      w1│         w2│
              │        └───┐   ┌───┘
              │          ┌─┴───┴─┐
              │          │  add  │
              │          └───┬───┘
              └──────┐   ┌───┘w3
                   ┌─┴───┴─┐
                   │  eq   │
                   └───────┘
]}

  The wires of a circuit are called {e prover inputs}, since the prover needs
  an assignment of all wires to produce a proof.
  The predicate also declares a subset of the wires called {e verifier inputs}.
  In our example, wire [w0] is the only verifier input, which is
  indicated by the parenthesis.
  A proof for a given [w0] would prove the following statement:
    [∃ w1, w2, w3: w3 = w1 + w2 ∧ w0 = w3]
  This means that the verifier only needs a (typically small) subset of the
  inputs alongside the (succinct) proof to check the validity of the statement.

  A more interesting example would be to replace the [add] gate
  by a more complicated hash circuit. This would prove the knowledge of the
  pre-image of a hash.

  A simplified view of aPlonk's API consists of the following three functions:
{[
    val setup : circuit -> srs ->
      (prover_public_parameters, verifier_public_parameters)

    val prove : prover_public_parameters -> prover_inputs ->
      private_inputs -> proof

    val verify : verifier_public_parameters -> verifier_inputs ->
      proof -> bool
]}

  In addition to the prove and verify, the interface provides a function
  to setup the system. The setup function requires a {e Structured Reference String}.
  Two large SRSs were generated by the ZCash and Filecoin
  projects and are both used in aPlonK.
  Notice also that the circuit is used during setup only and, independently
  from its size, the resulting {e verifier_public_parameters} will be a
  succinct piece of data that will be posted on-chain to allow
  verification and they are bound to the specific circuit that generated
  them.
  The {e prover_public_parameters}'s size is linear in the size of the circuit.
  *)

open Kzg.Bls
open Kzg.Utils
open Identities
include Main_protocol_intf

module Make_impl (PP : Polynomial_protocol.S) = struct
  module RangeCheck = Range_check_gate.Range_check_gate (PP)
  module Perm = Permutation_gate.Permutation_gate (PP)
  module Plook = Plookup_gate.Plookup_gate (PP)
  module Gates = Custom_gates
  module Commitment = PP.PC.Commitment
  module Input_commitment = Input_commitment.Make (PP.PC.Commitment)
  module PP = PP

  exception Entry_not_in_table = Plook.Entry_not_in_table

  exception Rest_not_null = Poly.Rest_not_null

  type scalar = Scalar.t [@@deriving repr]

  type circuit_map = (Circuit.t * int) SMap.t

  type proof = {
    perm_and_plook : Commitment.t;
    wires_cm : Commitment.t;
    pp_proof : PP.proof;
  }
  [@@deriving repr]

  type circuit_prover_input = {
    witness : scalar array;
    input_commitments : Input_commitment.t list;
  }
  [@@deriving repr]

  type prover_inputs = circuit_prover_input list SMap.t [@@deriving repr]

  type public_inputs = scalar array list [@@deriving repr]

  type circuit_verifier_input = {
    nb_proofs : int;
    public : public_inputs;
    commitments : Input_commitment.public list list;
  }
  [@@deriving repr]

  type verifier_inputs = circuit_verifier_input SMap.t [@@deriving repr]

  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 check_circuits circuits_map inputs =
    check_circuit_name inputs ;
    SMap.(
      iter (fun k _ ->
          if not (mem k circuits_map) then
            failwith
              (Printf.sprintf
                 "check_circuits : circuit %s not found in public parameters."
                 k)))
      inputs

  (* Returns the wire names as a string list *)
  let wire_names nb_wires = List.init nb_wires Plompiler.Csir.wire_name

  (* Convert the wire arrays into maps, keyed as in [wire_names] *)
  let name_wires wires_array =
    SMap.map
      (List.map (fun array ->
           let n = Array.length array in
           List.combine (wire_names n) (Array.to_list array) |> SMap.of_list))
      wires_array

  type gate_randomness = {beta : scalar; gamma : scalar; delta : scalar}

  let build_gates_randomness transcript =
    let betas_gammas, transcript = Fr_generation.random_fr_list transcript 3 in
    ( {
        beta = List.hd betas_gammas;
        gamma = List.nth betas_gammas 1;
        delta = List.nth betas_gammas 2;
      },
      transcript )

  module Prover = struct
    (* - n : upper-bound on the number of constraints in a circuit
       - domain : n powers of an n-th root of unity
       - pp_public_parameters : polynomial protocol prover parameters
       - g_map : preprocessed polynomials for each circuit, prefixed with the
                 circuit name ; note that this is circuit specific, but we need
                 them together in order to commit to the whole g_map once.
       - g_prover_aux : auxiliary information returned when commiting to g_map.
                        Note that the rest of the commitment is not needed by
                        the prover.
       - evaluations : FFT evaluations of commonly used polynomials for all
                       circuits, e.g. L1, Si1, Si2, Si3, X (Lnp1 for plookup).
                       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. These evaluations
                       does not contain g_map’s.
       - zk : true if we want to hide witness polynomial by adding multiple of
              (X^n - 1). This increases polynomials degree & may increase the
              the size of the evaluations domain & FFTs.
       - nb_of_t_chunks : number of T polynomials returned by PP
       - eval_points : used for the PC query ; note that the input commitments
                       are not here, their eval_points have to be added at
                       proof/verification time
    *)
    type common_prover_pp = {
      n : int;
      domain : Domain.t;
      pp_public_parameters : PP.prover_public_parameters;
      g_map : Poly.t SMap.t;
      g_prover_aux : Commitment.prover_aux;
      evaluations : Evaluations.t SMap.t;
      zk : bool;
      nb_of_t_chunks : int;
      eval_points : eval_point list list;
    }
    [@@deriving repr]

    (* - circuit_size : number of constraints in the circuit
       - input_com_sizes : the size of each input_commitment
       - public_input_size : the size of the public inputs
       - 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,
                 except qpub, that should be [||] if there are public inputs.
       - tables : [tables] is a list of scalar arrays, one per wire, so the list
                 length is Plompiler.Csir.nb_wires_arch.
                 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 : an array where each of the components corresponds to a wire in
                 the architecture and contains 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.
       - permutation: indices corresponding to a permutation that preserves
                 [wires]. Its length is [n * Plompiler.Csir.nb_wires_arch] 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),
                 that are contained in common_pp.g_map.
       - alpha : scalar used by plookup.
       - ultra : flag to specify whether plookup is being used.
    *)
    type circuit_prover_pp = {
      circuit_size : int;
      input_com_sizes : int list;
      public_input_size : int;
      gates : Scalar.t array SMap.t;
      tables : Scalar.t array list;
      wires : int array array;
      permutation : int array;
      rc_permutations : int array SMap.t;
      evaluations : Evaluations.t SMap.t;
      alpha : Scalar.t option;
      ultra : bool;
      range_checks : (int * int) list SMap.t;
    }
    [@@deriving repr]

    type public_parameters = {
      common_pp : common_prover_pp;
      circuits_map : circuit_prover_pp SMap.t;
      transcript : Kzg.Utils.Transcript.t;
    }
    [@@deriving repr]

    (* [build_all_wire_keys nb_proofs nb_wires] returns a list of prefixed wires name *)
    let build_all_wires_keys pp nb_proofs_map nb_wires =
      let names = wire_names nb_wires in
      List.concat_map (fun (circuit_name, n) ->
          let wires_keys =
            List.concat_map
              (SMap.Aggregation.build_all_names circuit_name n)
              names
          in
          let c = SMap.find circuit_name pp.circuits_map in
          let rc_keys =
            SMap.mapi
              (fun wire _ ->
                let n = SMap.find circuit_name nb_proofs_map in
                List.concat_map
                  (SMap.Aggregation.build_all_names circuit_name n)
                  (RangeCheck.z_names wire))
              c.range_checks
            |> SMap.values |> List.concat
          in
          wires_keys @ rc_keys)
      @@ SMap.bindings nb_proofs_map

    (* TODO #5551
       Handle Plookup
    *)
    (* For the distributed_prover *)
    let build_all_keys_z pp =
      List.concat_map
        (fun (c_name, c) ->
          let perm =
            List.map (SMap.Aggregation.add_prefix c_name) Perm.shared_z_names
          in
          if SMap.is_empty c.range_checks then perm
          else
            perm
            @ (SMap.mapi
                 (fun wire _ ->
                   List.map
                     (SMap.Aggregation.add_prefix c_name)
                     (RangeCheck.shared_z_names wire))
                 c.range_checks
              |> SMap.values |> List.concat))
        (SMap.bindings pp.circuits_map)

    let enforce_wire_values wire_indices wire_values =
      try
        Array.map
          (fun l ->
            let w_array = Array.map (fun index -> wire_values.(index)) l in
            Evaluations.of_array (Array.length w_array - 1, w_array))
          wire_indices
      with Invalid_argument _ ->
        failwith
          "Compute_wire_polynomial : x's length does not match with circuit. \
           Either your witness is too short, or some indexes are greater than \
           the witness size."

    let blind ~pp f_map =
      let nb_extra_blinds =
        List.fold_left
          (fun acc e -> max acc (List.length e))
          0
          pp.common_pp.eval_points
      in
      let blind_list_map l =
        List.map
          (fun unblinded ->
            if pp.common_pp.zk then
              let blinded =
                SMap.map
                  (Poly.blind ~nb_blinds:(1 + nb_extra_blinds) pp.common_pp.n)
                  unblinded
                |> SMap.to_pair
              in
              (fst blinded, Some (snd blinded))
            else (unblinded, None))
          l
        |> List.split
      in
      SMap.map blind_list_map f_map |> SMap.to_pair

    let update_wires_with_rc_1 ?shifts_map pp
        (all_f_wires, f_wires, f_blinds, wires_list_map) =
      let rc_z_evals, rc_map =
        SMap.mapi
          (fun name w_list ->
            let circuit_pp = SMap.find name pp.circuits_map in
            if SMap.is_empty circuit_pp.range_checks then ([], [])
            else
              List.map
                (fun values ->
                  RangeCheck.f_map_contribution_1
                    ~range_checks:circuit_pp.range_checks
                    ~domain:pp.common_pp.domain
                    ~values)
                w_list
              |> List.split)
          wires_list_map
        |> SMap.filter (fun _ x -> x <> ([], []))
        |> SMap.to_pair
      in
      let rc_map, rc_blinds = blind ~pp rc_map in
      let all_rc_z = SMap.Aggregation.gather_maps ?shifts_map rc_map in

      let wires_list_map =
        SMap.Aggregation.add_map_list_map wires_list_map rc_z_evals
      in
      let f_wires = SMap.Aggregation.add_map_list_map f_wires rc_map in
      let all_f_wires = SMap.union_disjoint all_f_wires all_rc_z in
      let f_blinds =
        SMap.mapi
          (fun k l1 ->
            match SMap.find_opt k rc_blinds with
            | Some l2 ->
                List.map2
                  (fun a -> function
                    | Some b -> Some (SMap.union_disjoint (Option.get a) b)
                    | None -> None)
                  l1
                  l2
            | None -> l1)
          f_blinds
      in
      (all_f_wires, f_wires, f_blinds, wires_list_map)

    (* returns informations about wires, including commitment, blinds &
       different useful representations of wires *)
    let commit_to_wires ?all_keys ?shifts_map pp
        (inputs_map : circuit_prover_input list SMap.t) =
      (* wires values map list map *)
      let wires_list_map =
        SMap.mapi
          (fun name input ->
            let circuit_pp = SMap.find name pp.circuits_map in
            List.map
              (fun w -> enforce_wire_values circuit_pp.wires w.witness)
              input)
          inputs_map
        |> name_wires
      in
      (* wire-polynomials array list map & there blinds *)
      let f_wires, f_blinds =
        let f_wires =
          SMap.map
            (List.map
               (SMap.map (Evaluations.interpolation_fft pp.common_pp.domain)))
            wires_list_map
        in
        blind ~pp f_wires
      in
      (* all wire-polynomials gathered in a map *)
      let all_f_wires = SMap.Aggregation.gather_maps ?shifts_map f_wires in

      let all_f_wires, f_wires, f_blinds, wires_list_map =
        update_wires_with_rc_1
          ?shifts_map
          pp
          (all_f_wires, f_wires, f_blinds, wires_list_map)
      in

      let cm_wires, cm_aux_wires =
        Commitment.commit
          ?all_keys
          (PP.PC.Public_parameters.get_commit_parameters
             pp.common_pp.pp_public_parameters)
          all_f_wires
      in
      (wires_list_map, f_wires, f_blinds, all_f_wires, cm_wires, cm_aux_wires)

    (* For each circuits, compute the shared Z polynomial *)
    let build_f_map_perm pp {beta; gamma; _} batched_wires =
      SMap.mapi
        (fun name values ->
          let circuit_pp = SMap.find name pp.circuits_map in
          (* Removing everything that is not wires *)
          let values =
            let wires_names =
              wire_names Plompiler.Csir.nb_wires_arch
              |> List.map String.capitalize_ascii
            in
            SMap.filter (fun k _ -> List.mem k wires_names) values
          in
          let zs =
            Perm.f_map_contribution
              ~permutation:circuit_pp.permutation
              ~values
              ~beta
              ~gamma
              ~domain:pp.common_pp.domain
              ()
          in
          if pp.common_pp.zk then
            SMap.map
              (fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
              zs
          else zs)
        batched_wires
      |> SMap.Aggregation.smap_of_smap_smap

    (* For each circuit, computes Plookup-specific polynomials *)
    let build_f_map_plook ?shifts_map pp rd wires_list_map =
      SMap.mapi
        (fun name w_list ->
          let circuit_pp = SMap.find name pp.circuits_map in
          if not circuit_pp.ultra then []
          else
            List.map
              (fun wires ->
                let plook_map =
                  Plook.f_map_contribution
                    ~wires
                    ~gates:circuit_pp.gates
                    ~tables:circuit_pp.tables
                    ~alpha:circuit_pp.alpha
                    ~beta:rd.beta
                    ~gamma:rd.gamma
                    ~domain:pp.common_pp.domain
                in
                if pp.common_pp.zk then
                  SMap.map
                    (fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
                    plook_map
                else plook_map)
              w_list)
        wires_list_map
      |> SMap.Aggregation.gather_maps ?shifts_map

    let build_f_map_rc_2 pp rd batched_values =
      SMap.mapi
        (fun name values ->
          let circuit_pp = SMap.find name pp.circuits_map in
          if SMap.is_empty circuit_pp.range_checks then SMap.empty
          else
            let zs =
              RangeCheck.f_map_contribution_2
                ~permutations:circuit_pp.rc_permutations
                ~beta:rd.beta
                ~gamma:rd.gamma
                ~domain:pp.common_pp.domain
                ~values
            in
            if pp.common_pp.zk then
              SMap.map
                (* 3 blinds because the polynomial is evaluated at x and gx *)
                  (fun f -> fst (Poly.blind ~nb_blinds:3 pp.common_pp.n f))
                zs
            else zs)
        batched_values
      |> SMap.Aggregation.smap_of_smap_smap

    let format_input_com (inputs_map : circuit_prover_input list SMap.t) =
      SMap.mapi
        (fun name l ->
          let n = List.length l in
          List.mapi
            (fun i w ->
              (* For each proof, transforms the list of inputs commitments into
                 a map of the form {com_label0 -> ic0 ; com_label1 -> ic1 ; …} *)
              (List.mapi (fun j ic ->
                   let name =
                     SMap.Aggregation.add_prefix
                       ~n
                       ~i
                       name
                       (Gates.com_label ^ string_of_int j)
                   in
                   ( Input_commitment.(SMap.singleton name ic.prover_aux.poly),
                     ic.prover_aux.pc_prover_aux )))
                w.input_commitments)
            l
          |> List.concat)
        inputs_map
      |> SMap.values |> List.concat

    let build_evaluations pp f_map =
      (* rebuild g_maps’ evaluations *)
      let evaluations =
        SMap.fold
          (fun _ pp evals -> SMap.union_disjoint pp.evaluations evals)
          pp.circuits_map
          pp.common_pp.evaluations
      in
      Evaluations.compute_evaluations_update_map ~evaluations f_map

    let build_perm_rc2_identities pp rd =
      SMap.mapi
        (fun circuit_name circuit_pp ->
          (* Using the batched wires *)
          let wires_names =
            List.map
              String.capitalize_ascii
              (wire_names @@ Array.length circuit_pp.wires)
          in
          let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
          let perm_id =
            Perm.prover_identities
              ~circuit_prefix
              ~wires_names
              ~beta:rd.beta
              ~gamma:rd.gamma
              ~n:pp.common_pp.n
              ()
          in
          let range_checks = circuit_pp.range_checks in
          if SMap.is_empty range_checks then perm_id
          else
            let rc2_ids =
              RangeCheck.prover_identities_2
                ~range_checks
                ~circuit_prefix
                ~beta:rd.beta
                ~gamma:rd.gamma
                ~domain_size:pp.common_pp.n
                ()
            in
            merge_prover_identities [perm_id; rc2_ids])
        pp.circuits_map
      |> SMap.values |> merge_prover_identities

    let build_gates_plook_rc1_identities ?shifts_map pp rd inputs_map =
      let identities_map =
        SMap.mapi
          (fun circuit_name inputs_list ->
            let circuit_pp = SMap.find circuit_name pp.circuits_map in
            let wires_names = wire_names @@ Array.length circuit_pp.wires in
            (* Identities that must be computed for each proof *)
            let shift, nb_proofs =
              match shifts_map with
              | None -> (0, List.length inputs_list)
              | Some shifts_map -> SMap.find circuit_name shifts_map
            in
            let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
            let proof_prefix i =
              SMap.Aggregation.add_prefix
                ~n:nb_proofs
                ~i:(i + shift)
                circuit_name
            in
            let gates_identities =
              List.mapi
                (fun i inputs ->
                  let input_coms_size =
                    List.fold_left ( + ) 0 circuit_pp.input_com_sizes
                  in
                  let public_inputs =
                    Array.sub
                      inputs.witness
                      input_coms_size
                      circuit_pp.public_input_size
                  in
                  Gates.aggregate_prover_identities
                    ~circuit_prefix
                    ~input_coms_size
                    ~proof_prefix:(proof_prefix i)
                    ~gates:circuit_pp.gates
                    ~public_inputs
                    ~domain:pp.common_pp.domain
                    ())
                inputs_list
            in
            (* for plookup and rc, we do a mapi on the input_list & ignore the
               input (instead of doing a List.init nb_proofs) because for the
               distributed prover, the number of inputs given will differ from
               nb_proofs *)
            let plookup_identities =
              if not circuit_pp.ultra then []
              else
                List.mapi
                  (fun i _ ->
                    Plook.prover_identities
                      ~circuit_prefix
                      ~proof_prefix:(proof_prefix i)
                      ~wires_names
                      ~alpha:circuit_pp.alpha
                      ~beta:rd.beta
                      ~gamma:rd.gamma
                      ~n:pp.common_pp.n
                      ())
                  inputs_list
            in
            let rc1_identities =
              let range_checks = circuit_pp.range_checks in
              if SMap.is_empty range_checks then []
              else
                List.mapi
                  (fun i _ ->
                    RangeCheck.prover_identities_1
                      ~range_checks
                      ~circuit_prefix
                      ~proof_prefix:(proof_prefix i)
                      ~domain_size:pp.common_pp.n
                      ())
                  inputs_list
            in
            merge_prover_identities
              (rc1_identities @ plookup_identities @ gates_identities))
          inputs_map
      in
      merge_prover_identities (SMap.values identities_map)

    let prove_parameters ~pp_prove pp ~inputs_map =
      let wires_list_map, f_wires, f_blinds, all_f_wires, cm_wires, cm_aux_wires
          =
        commit_to_wires pp inputs_map
      in
      (* compute beta & gamma (common for all proofs) *)
      let transcript = Transcript.expand Commitment.t cm_wires pp.transcript in
      let rd, transcript = build_gates_randomness transcript in

      let batched_wires =
        Perm.Shared_argument.build_batched_wires_values
          ~delta:rd.delta
          ~wires:wires_list_map
          ()
      in

      (* The new batched_wires is used for the RC shared perm argument *)
      let f_map_contributions =
        let f_map_perm = build_f_map_perm pp rd batched_wires in
        let f_map_plook = build_f_map_plook pp rd wires_list_map in
        let f_map_rc2 = build_f_map_rc_2 pp rd batched_wires in
        SMap.union_disjoint_list [f_map_perm; f_map_plook; f_map_rc2]
      in

      let input_com_secrets = format_input_com inputs_map in

      let identities =
        let gates_plook_rc1_ids =
          build_gates_plook_rc1_identities pp rd inputs_map
        in
        let perm_rc2_ids = build_perm_rc2_identities pp rd in
        merge_prover_identities [perm_rc2_ids; gates_plook_rc1_ids]
      in

      let eval_points =
        pp.common_pp.eval_points @ List.map (Fun.const [X]) input_com_secrets
      in

      (* Here we introduced the use_batched_wires because f_wires does not contain rc stuff, which will be missing if batched wires polys are deduced from f_wires *)
      let batched_wires_polys =
        Perm.Shared_argument.build_batched_witness_polys
          ~use_batched_wires:
            (SMap.exists
               (fun _ c -> not (SMap.is_empty c.range_checks))
               pp.circuits_map)
          ~zero_knowledge:pp.common_pp.zk
          ~domain:pp.common_pp.domain
          ~delta:rd.delta
          ~batched_wires
          ~f:(f_wires, f_blinds)
          ()
      in

      let evaluations =
        build_evaluations
          pp
          (SMap.union_disjoint_list
             (all_f_wires :: f_map_contributions :: batched_wires_polys
             :: List.map fst input_com_secrets))
      in

      let cm_perm_plook_rc, perm_plook_rc_prv_aux =
        PP.PC.commit pp.common_pp.pp_public_parameters f_map_contributions
      in
      let transcript =
        Transcript.expand Commitment.t cm_perm_plook_rc transcript
      in

      let secrets =
        [
          (pp.common_pp.g_map, pp.common_pp.g_prover_aux);
          (f_map_contributions, perm_plook_rc_prv_aux);
          (all_f_wires, cm_aux_wires);
        ]
        @ input_com_secrets
      in

      let generator = Domain.get pp.common_pp.domain 1 in
      let pp_proof, _transcript =
        pp_prove
          pp.common_pp.pp_public_parameters
          transcript
          ~n:pp.common_pp.n
          ~generator
          ~secrets
          ~eval_points
          ~evaluations
          ~identities
          ~nb_of_t_chunks:pp.common_pp.nb_of_t_chunks
      in

      (pp_proof, (cm_perm_plook_rc, cm_wires, rd))
  end

  module Verifier = struct
    (* - n : upper-bound on the number of constraints in a circuit
       - generator : primitive n-th root of unity
       - pp_public_parameters : polynomial protocol verifier parameters
       - cm_g : commitment to the preprocessed polynomials
       - eval_points : used for the PC query ; note that the input commitments
                       are not here, their eval_points have to be added at
                       proof/verification time
    *)
    type common_verifier_pp = {
      n : int;
      generator : Scalar.t;
      pp_public_parameters : PP.verifier_public_parameters;
      cm_g : Commitment.t;
      eval_points : eval_point list list;
    }
    [@@deriving repr]

    (* - gates : map of selector names ; they are binded to unit because we
                 just need their name for the verification
       - alpha : scalar used by plookup.
       - ultra : flag to specify whether plookup is being used.
       - input_com_sizes : the size of each input_commitment
    *)
    type circuit_verifier_pp = {
      gates : unit SMap.t;
      alpha : Scalar.t option;
      ultra : bool;
      input_com_sizes : int list;
      range_checks : bool SMap.t;
    }
    [@@deriving repr]

    let circuit_verifier_pp_of_circuit_prover_pp
        (prover_pp : Prover.circuit_prover_pp) =
      {
        gates = SMap.map (Fun.const ()) prover_pp.gates;
        alpha = prover_pp.alpha;
        ultra = prover_pp.ultra;
        input_com_sizes = prover_pp.input_com_sizes;
        range_checks = SMap.map (fun l -> l <> []) prover_pp.range_checks;
      }

    let build_identities circuits_map (n, generator) rd inputs_map =
      let identities_map =
        SMap.mapi
          (fun circuit_name {nb_proofs; public = pi_list; _} ->
            assert (List.compare_length_with pi_list nb_proofs = 0) ;
            let circuit_pp = SMap.find circuit_name circuits_map in
            let circuit_prefix = SMap.Aggregation.add_prefix circuit_name in
            let proof_prefix i =
              SMap.Aggregation.add_prefix ~n:nb_proofs ~i circuit_name
            in
            let wires_names = wire_names Plompiler.Csir.nb_wires_arch in
            let perm_identities =
              Perm.verifier_identities
                ~circuit_prefix
                ~wires_names
                ~nb_proofs
                ~generator
                ~n
                ~beta:rd.beta
                ~gamma:rd.gamma
                ~delta:rd.delta
                ()
            in
            let gates_identities =
              List.mapi
                (fun i public_inputs ->
                  Gates.aggregate_verifier_identities
                    ~circuit_prefix
                    ~input_com_sizes:circuit_pp.input_com_sizes
                    ~gates:circuit_pp.gates
                    ~public_inputs
                    ~generator
                    ~size_domain:n
                    ()
                    ~proof_prefix:(proof_prefix i))
                pi_list
            in
            let plookup_identities =
              if not circuit_pp.ultra then []
              else
                List.init nb_proofs (fun i ->
                    Plook.verifier_identities
                      ~circuit_prefix
                      ~wires_names
                      ~generator
                      ~n
                      ~alpha:circuit_pp.alpha
                      ~beta:rd.beta
                      ~gamma:rd.gamma
                      ~proof_prefix:(proof_prefix i)
                      ())
            in
            let range_checks = circuit_pp.range_checks in
            if SMap.is_empty range_checks then
              merge_verifier_identities
                (perm_identities :: (plookup_identities @ gates_identities))
            else
              let rc1_identities =
                List.init nb_proofs (fun i ->
                    RangeCheck.verifier_identities_1
                      ~range_checks
                      ~circuit_prefix
                      ~proof_prefix:(proof_prefix i)
                      ())
              in
              let rc2_identities =
                RangeCheck.verifier_identities_2
                  ~range_checks
                  ~circuit_prefix
                  ~nb_proofs
                  ~beta:rd.beta
                  ~gamma:rd.gamma
                  ~delta:rd.delta
                  ~domain_size:n
                  ~generator
                  ()
              in
              merge_verifier_identities
                (perm_identities :: rc2_identities
                :: (rc1_identities @ plookup_identities @ gates_identities)))
          inputs_map
      in
      merge_verifier_identities (SMap.values identities_map)

    let format_input_com (inputs_map : verifier_inputs) =
      SMap.mapi
        (fun name {commitments = l; _} ->
          let n = List.length l in
          List.mapi
            (fun i ic ->
              let rename j s =
                SMap.Aggregation.add_prefix ~n ~i name s ^ string_of_int j
              in
              List.mapi (fun j -> Commitment.rename (rename j)) ic)
            l
          |> List.concat)
        inputs_map
      |> SMap.values |> List.concat

    (* Assumes the same circuit, i.e. the public parameters are fixed *)
    let verify_parameters ((common_pp, circuits_map), transcript) inputs_map
        proof =
      (* The transcript is the same as the provers's transcript since the proof
         is already aggregated *)
      let transcript =
        Transcript.expand Commitment.t proof.wires_cm transcript
      in
      (* Get the same randomness for all proofs *)
      (* Step 1a : compute beta & gamma *)
      let rd, transcript = build_gates_randomness transcript in
      (* Step 3 : compute verifier’s identities *)
      let identities =
        build_identities
          circuits_map
          (common_pp.n, common_pp.generator)
          rd
          inputs_map
      in
      let input_commitments = format_input_com inputs_map in
      let commitments =
        [common_pp.cm_g; proof.perm_and_plook; proof.wires_cm]
        @ input_commitments
      in
      let eval_points =
        common_pp.eval_points @ List.map (Fun.const [X]) input_commitments
      in
      let transcript =
        Transcript.expand Commitment.t proof.perm_and_plook transcript
      in
      (transcript, identities, rd, commitments, eval_points)
  end

  type prover_public_parameters = Prover.public_parameters = {
    common_pp : Prover.common_prover_pp;
    circuits_map : Prover.circuit_prover_pp SMap.t;
    transcript : Transcript.t;
  }
  [@@deriving repr]

  type verifier_public_parameters = {
    common_pp : Verifier.common_verifier_pp;
    circuits_map : Verifier.circuit_verifier_pp SMap.t;
    transcript : Transcript.t;
  }
  [@@deriving repr]

  module Preprocess = struct
    let eval_points (circuits_map : Prover.circuit_prover_pp SMap.t) =
      let open Prover in
      let used_ultra = SMap.exists (fun _ c -> c.ultra) circuits_map in
      (* We need gX evaluation for wires if there is a next gate, or if there is a range check gate (RC.Z needs to be evaluated at X & gX and is committed with wires) *)
      let gx_wires =
        SMap.exists
          (fun _ c ->
            Gates.exists_gx_composition ~gates:c.gates
            || c.range_checks <> SMap.empty)
          circuits_map
      in
      let g_points = if used_ultra then [X; GX] else [X] in
      let f_points = if gx_wires then [X; GX] else [X] in
      [g_points; [X; GX]; f_points]

    let degree_evaluations ~nb_wires ~gates ~ultra =
      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
      max min_deg (Gates.aggregate_polynomials_degree ~gates)

    let domain_evaluations ~zero_knowledge ~n len_evals =
      let zk_factor = if zero_knowledge then if n <= 2 then 4 else 2 else 1 in
      let len_evals = zk_factor * len_evals * n in
      Domain.build_power_of_two 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
       - l, the number of public inputs + the number of elements committed in input_commitments
       Outputs:
       - interpolated_gates: selector polynomials, prepended with 0/1s for the public inputs,
       interpolated on the domain
       - extended_gates: gates with "q_pub" selector if there is public_inputs
       - extended_wires: circuits wires prepended with wires corresponding to the public inputs
       - extended_tables: formatted tables
       - adapted_range_checks: range check with indexes shifted regarding public_inputs
    *)
    let preprocessing n domain (c : Circuit.t) =
      let l = List.fold_left ( + ) c.public_input_size c.input_com_sizes in
      let ql_name = Plompiler.Csir.linear_selector_name 0 in
      (* 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_name c.gates) then
          SMap.add
            ql_name
            (Array.init c.circuit_size (fun _ -> Scalar.zero))
            c.gates
        else c.gates
      in
      (* other preprocessed things in article are computed in prove of permutations *)
      let extended_gates =
        (* Adding 0s/1s for public inputs & input_commitments *)
        SMap.mapi
          (fun label gate ->
            let length_poly = Array.length gate in
            Array.init n (fun i ->
                if i < l && label = ql_name then Scalar.one
                else if l <= i && i < l + length_poly then gate.(i - l)
                else Scalar.zero))
          gates
      in
      let extended_gates, _, _ =
        List.fold_left
          (fun (acc, i, k) size ->
            let acc =
              SMap.add
                ("qcom" ^ string_of_int i)
                (Array.init n (fun j ->
                     if j >= k && j < k + size then Scalar.(negate one)
                     else Scalar.zero))
                acc
            in
            (acc, i + 1, k + size))
          (extended_gates, 0, 0)
          c.input_com_sizes
      in
      let interpolated_gates =
        SMap.map (Evaluations.interpolation_fft2 domain) extended_gates
      in
      let extended_gates =
        if c.public_input_size = 0 then extended_gates
        else SMap.add_unique "qpub" [||] extended_gates
      in
      let extended_wires =
        let li_array = Array.init l (fun i -> i) in
        (* Adding public inputs and resizing *)
        Array.map (fun w -> pad_array (Array.append li_array w) n) c.wires
      in
      let adapted_range_checks =
        SMap.map (List.map (fun (i, n) -> (l + i, n))) c.range_checks
      in
      let extended_tables =
        if not c.ultra then []
        else
          Plook.format_tables
            ~tables:c.tables
            ~nb_columns:Plompiler.Csir.nb_wires_arch
            ~length_not_padded:c.table_size
            ~length_padded:n
      in
      ( interpolated_gates,
        extended_gates,
        extended_wires,
        extended_tables,
        adapted_range_checks )

    let preprocess_map domain domain_evals n circuits_map =
      (* Preprocessing wires, gates and tables *)
      SMap.fold
        (fun circuit_name (circuit, _) (prv, vrf, all_g_maps) ->
          (* Generating alpha for Plookup *)
          let alpha =
            if Circuit.(circuit.ultra) then Some (Scalar.random ()) else None
          in
          let gates_poly, gates, wires, tables, range_checks =
            preprocessing n domain circuit
          in
          (* Generating permutation *)
          let permutation = Perm.build_permutation wires in

          let rc_permutations =
            RangeCheck.build_permutations ~range_checks ~size_domain:n
          in
          let g_map_perm =
            Perm.preprocessing
              ~domain
              ~nb_wires:Plompiler.Csir.nb_wires_arch
              ~permutation
              ()
          in
          let g_map_plook =
            if circuit.ultra then Plook.preprocessing ~domain ~tables ~alpha ()
            else SMap.empty
          in
          let g_map_range_check =
            RangeCheck.preprocessing
              ~permutations:rc_permutations
              ~range_checks:circuit.range_checks
              ~domain
          in
          let circuit_g_map =
            SMap.union_disjoint_list
              [g_map_plook; g_map_perm; gates_poly; g_map_range_check]
            |> SMap.Aggregation.prefix_map circuit_name
          in
          let evaluations =
            Evaluations.compute_evaluations ~domain:domain_evals circuit_g_map
          in
          let prover_pp =
            Prover.
              {
                circuit_size = circuit.circuit_size;
                input_com_sizes = circuit.input_com_sizes;
                public_input_size = circuit.public_input_size;
                gates;
                tables;
                wires;
                evaluations;
                permutation;
                rc_permutations;
                alpha;
                ultra = circuit.ultra;
                range_checks;
              }
          in
          let verifier_pp =
            let gates = SMap.map (fun _ -> ()) gates in
            Verifier.
              {
                gates;
                alpha;
                ultra = circuit.ultra;
                input_com_sizes = circuit.input_com_sizes;
                range_checks = SMap.map (fun rc -> rc <> []) range_checks;
              }
          in
          ( SMap.add_unique circuit_name prover_pp prv,
            SMap.add_unique circuit_name verifier_pp vrf,
            SMap.union_disjoint all_g_maps circuit_g_map ))
        circuits_map
        SMap.(empty, empty, empty)

    let compute_sizes circuit_name
        ( Circuit.
            {
              public_input_size;
              input_com_sizes;
              circuit_size;
              table_size;
              nb_lookups;
              ultra;
              gates;
              range_checks;
              _;
            },
          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).
         For range-checks, we want to ensure that the domain size is greater than the "size" of the "biggest" range-checks
      *)
      let nb_max_constraints =
        let base_size =
          circuit_size
          + List.fold_left ( + ) public_input_size input_com_sizes
          + if ultra then 1 else 0
        in
        let size_with_rc, biggest_rc_wire =
          SMap.fold
            (fun wire r (acc, rc_wire) ->
              let sum_bounds =
                (List.fold_left (fun sum (_, bound) -> sum + bound)) 0 r
              in
              if sum_bounds > acc then (sum_bounds, wire) else (acc, rc_wire))
            range_checks
            (base_size, "")
        in
        (* if the circuit size has been increased because of the range checks we raise a warning *)
        let _print_warning =
          match biggest_rc_wire with
          | "" -> ()
          | w ->
              Printf.printf
                "\n\
                 WARNING: Circuit %s's size has been increased to %d (initial \
                 size was %d) because of the range-checks on the %s wire."
                circuit_name
                size_with_rc
                base_size
                w
        in
        size_with_rc
      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_max_constraints nb_rec_look in
      let log = Z.(log2up (of_int max_nb)) in
      let n = Int.shift_left 1 log 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 + Plompiler.Csir.nb_wires_arch + SMap.cardinal gates + ultra_polys
        in
        let nb_extra_polys = if ultra then 5 else 1 in
        let online =
          max Plompiler.Csir.nb_wires_arch 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, pack_size)

    let get_sizes ~zero_knowledge circuits_map =
      let log, n, total_pack, some_ultra =
        SMap.fold
          (fun k (c, nb_proofs) (acc_log, acc_n, acc_pack_size, acc_ultra) ->
            let log, n, pack_size = compute_sizes k (c, nb_proofs) in
            ( max acc_log log,
              max acc_n n,
              acc_pack_size + pack_size,
              acc_ultra || c.ultra ))
          circuits_map
          (0, 0, 0, false)
      in
      let degree_evals =
        SMap.fold
          (fun _ ((c : Circuit.t), _) acc_deg_eval ->
            let deg_eval =
              degree_evaluations
                ~nb_wires:Plompiler.Csir.nb_wires_arch
                ~gates:c.gates
                ~ultra:c.ultra
            in
            max acc_deg_eval deg_eval)
          circuits_map
          0
      in
      let domain_evals = domain_evaluations ~zero_knowledge ~n degree_evals in
      let domain = Domain.build_power_of_two log in
      let total_pack = 1 lsl Z.(log2up (of_int total_pack)) in
      (* Each t chunk should be of degree [n].
         We remove 1 because t is divided by (X^n - 1) *)
      let nb_of_t_chunks =
        degree_evals + (if zero_knowledge then 1 else 0) - 1
      in
      (domain, n, total_pack, domain_evals, some_ultra, nb_of_t_chunks)

    let setup_circuits ~zero_knowledge circuits_map ~srs =
      let domain, n, pack_size, domain_evals, some_ultra, nb_of_t_chunks =
        get_sizes ~zero_knowledge circuits_map
      in
      let evaluations =
        (* Add X evaluations, which is the domain needed for other evaluations *)
        let evaluations =
          SMap.singleton "X" (Evaluations.of_domain domain_evals)
        in
        (* Add L₁, Sid₁, Sid₂, Sid₃, Sid₄, Sid₅ *)
        let evaluations =
          Perm.common_preprocessing
            ~nb_wires:Plompiler.Csir.nb_wires_arch
            ~domain
            ~evaluations
        in

        (* if ultra add L_n_plus_1 *)
        if some_ultra then Plook.common_preprocessing ~n ~domain ~evaluations
        else evaluations
      in
      let pp_prv, pp_vrf, g_map =
        preprocess_map domain domain_evals n circuits_map
      in
      (* Generating public parameters *)
      let pp_prover, pp_verifier, transcript =
        PP.setup ~setup_params:pack_size ~srs
      in
      let cm_g, g_prover_aux = PP.PC.commit pp_prover g_map in
      let eval_points = eval_points pp_prv in
      let common_prv =
        Prover.
          {
            n;
            domain;
            pp_public_parameters = pp_prover;
            evaluations;
            g_map;
            g_prover_aux;
            zk = zero_knowledge;
            nb_of_t_chunks;
            eval_points;
          }
      in
      let common_vrf =
        Verifier.
          {
            n;
            generator = Domain.get domain 1;
            pp_public_parameters = pp_verifier;
            cm_g;
            eval_points;
          }
      in
      ( ({common_pp = common_prv; circuits_map = pp_prv; transcript}
          : prover_public_parameters),
        {common_pp = common_vrf; circuits_map = pp_vrf; transcript} )
  end

  let to_verifier_inputs (pp : prover_public_parameters) =
    let extract name (secrets : circuit_prover_input list) :
        circuit_verifier_input =
      let c = SMap.find name pp.circuits_map in
      let ic_size = List.fold_left ( + ) 0 c.input_com_sizes in
      let public =
        List.map
          (fun s -> Array.sub s.witness ic_size c.public_input_size)
          secrets
      in
      let nb_proofs = List.length public in
      let commitments =
        if List.exists (fun c -> c.input_commitments <> []) secrets then
          List.map
            (fun s ->
              List.map
                (fun (c : Input_commitment.t) -> c.public)
                s.input_commitments)
            secrets
        else []
      in
      {nb_proofs; public; commitments}
    in
    SMap.mapi extract

  let input_commit ?size ?shift (pp : prover_public_parameters) secret =
    Input_commitment.commit
      ?size
      ?shift
      (PP.PC.Public_parameters.get_commit_parameters
         pp.common_pp.pp_public_parameters)
      pp.common_pp.n
      secret

  let update_prover_public_parameters repr x (pp : prover_public_parameters) =
    {pp with transcript = Transcript.expand repr x pp.transcript}

  let update_verifier_public_parameters repr x (pp : verifier_public_parameters)
      =
    {pp with transcript = Transcript.expand repr x pp.transcript}

  (* [filter_pp_circuits pp inputs_map] returns [pp]
     without the circuits that don’t appear in [inputs_map]’s keys
  *)
  let filter_prv_pp_circuits (pp : prover_public_parameters) inputs_map =
    check_circuits pp.circuits_map inputs_map ;
    {pp with circuits_map = SMap.sub_map inputs_map pp.circuits_map}

  let filter_vrf_pp_circuits pp inputs_map =
    check_circuits pp.circuits_map inputs_map ;
    {pp with circuits_map = SMap.sub_map inputs_map pp.circuits_map}

  let setup ~zero_knowledge circuits_map ~srs =
    check_circuit_name circuits_map ;
    Preprocess.setup_circuits ~zero_knowledge circuits_map ~srs

  (* inputs is a map between circuit names to list of public inputs *)
  let prove (pp : prover_public_parameters) ~inputs =
    check_circuit_name pp.circuits_map ;
    (* add the verifier inputs to the transcript *)
    let pp =
      {
        pp with
        transcript =
          Transcript.expand
            verifier_inputs_t
            (to_verifier_inputs pp inputs)
            pp.transcript;
      }
    in
    let pp_proof, (perm_and_plook, wires_cm, _) =
      Prover.prove_parameters
        ~pp_prove:PP.prove
        (filter_prv_pp_circuits pp inputs)
        ~inputs_map:inputs
    in
    {perm_and_plook; wires_cm; pp_proof}

  let verify pp ~inputs proof =
    check_circuit_name pp.circuits_map ;
    let circuits_map = SMap.sub_map inputs pp.circuits_map in
    (* add the verifier inputs to the transcript *)
    let transcript =
      let inputs =
        SMap.map
          (fun i ->
            if List.exists (fun c -> c <> []) i.commitments then i
            else {i with commitments = []})
          inputs
      in
      Transcript.expand verifier_inputs_t inputs pp.transcript
    in
    let transcript, identities, _, commitments, eval_points =
      Verifier.verify_parameters
        ((pp.common_pp, circuits_map), transcript)
        inputs
        proof
    in
    PP.verify
      pp.common_pp.pp_public_parameters
      transcript
      ~n:pp.common_pp.n
      ~generator:pp.common_pp.generator
      ~commitments
      ~identities
      ~eval_points
      proof.pp_proof
    |> fst

  let scalar_encoding =
    Data_encoding.(
      conv
        Scalar.to_bytes
        Scalar.of_bytes_exn
        (Fixed.bytes Scalar.size_in_bytes))

  let data_encoding_of_repr repr =
    Data_encoding.conv
      (Plompiler.Utils.to_bytes repr)
      (Plompiler.Utils.of_bytes repr)
      Data_encoding.bytes

  let proof_encoding = data_encoding_of_repr proof_t

  let verifier_public_parameters_encoding =
    data_encoding_of_repr verifier_public_parameters_t

  module Internal_for_tests = struct
    let mutate_vi verifier_inputs =
      (* TODO we could do a more randomized search *)
      let key, {nb_proofs; public; commitments} = SMap.choose verifier_inputs in
      match public with
      | head :: tail ->
          if head = [||] then None (* empty public inputs *)
          else
            let new_head = Array.copy head in
            new_head.(0) <- Scalar.(add one new_head.(0)) ;
            let public = new_head :: tail in
            let inputs = {nb_proofs; public; commitments} in
            Some (SMap.add key inputs verifier_inputs)
      | [] -> failwith "mutate_vi : all circuits should have verifier inputs."
  end
end

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

include Make (Polynomial_protocol)