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

(** A polynomial protocol allows a prover to convince a verifier of the fact
    that certain algebraic identites between polynomials (polynomials that have
    been previously committed) hold when evaluated over a set of points.
    (In our implementation such set of points must be a subgroup of roots of
    unity.)

    For example, let K be a field and let H be a subset of K.
    Let f1(X), f2(X) and f3(X) be univariate polynomials over K and let
    C1, C2 and C3 be polynomial commitments to f1, f2 and f3, respectively.
    A polynomial protocol allows a prover to argue knowledge of:
    {[
      PoK{ (f1, f2, f3) : Ci = Com(fi) ∀ i  /\  f1(x) * f2(x) = f3(x) ∀ x ∈ H }
    ]}
    This can be accomplished by evaluating polynomial commitments at a single
    point ξ (uniformly sampled from K). For that, note that the above
    polynomial identity holds for every x ∈ H iff polynomial (f1 * f2 - f3) is
    divisible by Zh, the minimal (monic) polynomial that vanishes over set H.
    Thus, the prover can commit to polynomial T := (f1 * f2 - f3) / Zh and
    evaluate polynomial commitments C1, C2, C3, T at ξ (chosen after T). Let
    c1, c2, c3, t be such evaluations.
    The verifier can then check that  t * Zh(ξ) = c1 * c2 - c3.

    A general polynomial protocol should allow for multiple identities involving
    addition, multiplication and composition of polynomials.

    See {{: https://eprint.iacr.org/2019/953.pdf }2019/953 Section 4.1} for
    more details. *)

(** Functor building an implementation of a polynomial protocol given a
    polynomial commitment scheme [PC]. *)
module Make_impl (PC : Polynomial_commitment.S) = struct
  module PC = PC
  module Domain = PC.Polynomial.Domain
  module Poly = PC.Polynomial.Polynomial
  module Evaluations = Evaluations_map.Make (PC.Polynomial.Evaluations)
  module Fr_generation = PC.Fr_generation

  type prover_public_parameters = PC.Public_parameters.prover [@@deriving repr]

  type verifier_public_parameters = PC.Public_parameters.verifier
  [@@deriving repr]

  type prover_identities = Evaluations.t SMap.t -> Evaluations.t SMap.t

  type verifier_identities =
    PC.Scalar.t -> PC.Scalar.t SMap.t SMap.t -> PC.Scalar.t SMap.t

  type non_committed =
    PC.Scalar.t -> PC.Scalar.t SMap.t SMap.t -> PC.Scalar.t SMap.t

  type transcript = Bytes.t [@@deriving repr]

  type proof = {
    cm_t : PC.Commitment.t;
    pc_proof : PC.proof;
    pc_answers : PC.answer list;
  }
  [@@deriving repr]

  type eval_point = X | GX | Custom of string * (PC.Scalar.t -> PC.Scalar.t)

  let string_of_eval_point = function
    | X -> "x"
    | GX -> "gx"
    | Custom (s, _) -> s

  let convert_eval_points ~generator ~x l =
    let eval = function
      | X -> x
      | GX -> PC.Scalar.mul generator x
      | Custom (_, f) -> f x
    in
    SMap.of_list @@ List.map (fun p -> (string_of_eval_point p, eval p)) l

  let get_answer answers x n =
    SMap.find (string_of_eval_point x) answers |> SMap.find n

  let merge_prover_identities identities_list : prover_identities =
   fun evaluations ->
    List.fold_left
      (fun acc_map ids -> SMap.union_disjoint acc_map (ids evaluations))
      SMap.empty identities_list

  let merge_verifier_identities identities_list : verifier_identities =
   fun x answers ->
    List.fold_left
      (fun acc_map ids -> SMap.union_disjoint acc_map (ids x answers))
      SMap.empty identities_list

  let split_t n t nb_of_t_chunks =
    List.mapi
      (fun i t_i -> ("T_" ^ string_of_int i, t_i))
      (Poly.split ~nb_chunks:nb_of_t_chunks n t)
    |> SMap.of_list

  let compute_t ~n ~alpha ~nb_of_t_chunks evaluated_identities =
    let nb_ids = SMap.cardinal evaluated_identities in
    let evaluations = List.map snd @@ SMap.bindings evaluated_identities in
    let alphas = Fr_generation.powers nb_ids alpha |> Array.to_list in
    let s_eval = Evaluations.linear_c ~evaluations ~linear_coeffs:alphas () in
    let s_deg = Evaluations.degree s_eval in
    let domain = Domain.build_power_of_two (Z.log2up (Z.of_int (s_deg + 1))) in
    let s = Evaluations.interpolation_fft domain s_eval in
    let t, rem = Poly.division_xn s n PC.Scalar.(negate one) in
    if Poly.is_zero rem then (
      let splits = split_t n t nb_of_t_chunks in
      assert (SMap.for_all (fun _k v -> Poly.degree v < n) splits);
      splits)
    else raise @@ Poly.Rest_not_null "T is not divisible by Zh"

  let verify_t n x alpha evaluated_identities cm_t answers =
    let values = List.map snd @@ SMap.bindings evaluated_identities in
    let s = Fr_generation.batch alpha values in
    let t_val =
      let x_evals = SMap.find (string_of_eval_point X) answers in
      let nb_t = PC.Commitment.cardinal cm_t in
      List.init nb_t (fun i -> SMap.find ("T_" ^ string_of_int i) x_evals)
      |> Fr_generation.batch (PC.Scalar.pow x (Z.of_int n))
    in
    let zh = PC.Scalar.(sub (pow x (Z.of_int n)) one) in
    PC.Scalar.(eq s (t_val * zh))

  let setup ~setup_params ~srs = PC.Public_parameters.setup setup_params srs

  let prove_aux ~pc_function pc_public_parameters transcript n generator secrets
      eval_points evaluations identities nb_of_t_chunks =
    let alpha, transcript = Fr_generation.random_fr transcript in
    let evaluated_ids = identities evaluations in
    let t = compute_t ~n ~alpha ~nb_of_t_chunks evaluated_ids in
    let cm_t, t_prover_aux = PC.Commitment.commit pc_public_parameters t in
    let transcript = Utils.expand_transcript PC.Commitment.t cm_t transcript in
    let x, transcript = Fr_generation.random_fr transcript in
    let prover_aux_list = t_prover_aux :: List.map snd secrets in
    let polys_list = t :: List.map fst secrets in
    let eval_points = [ X ] :: eval_points in
    let query_list = List.map (convert_eval_points ~generator ~x) eval_points in
    let answer_list = List.map2 PC.evaluate polys_list query_list in
    let pc_ret =
      pc_function pc_public_parameters transcript polys_list prover_aux_list
        query_list answer_list
    in
    (pc_ret, (alpha, x, answer_list, cm_t))

  let prove pc_public_parameters transcript ~n ~generator ~secrets ~eval_points
      ~evaluations ~identities ~nb_of_t_chunks =
    let (pc_proof, transcript), (_, _, answer_list, cm_t) =
      prove_aux ~pc_function:PC.prove pc_public_parameters transcript n
        generator secrets eval_points evaluations identities nb_of_t_chunks
    in
    ({ cm_t; pc_proof; pc_answers = answer_list }, transcript)

  type pp_commit_to_t_r = Evaluations.t SMap.t [@@deriving repr]

  let verify_aux transcript generator commitments eval_points proof =
    let alpha, transcript = Fr_generation.random_fr transcript in
    let transcript =
      Utils.expand_transcript PC.Commitment.t proof.cm_t transcript
    in
    let x, transcript = Fr_generation.random_fr transcript in
    let cm_list = proof.cm_t :: commitments in
    let eval_points = [ X ] :: eval_points in
    let query_list = List.map (convert_eval_points ~generator ~x) eval_points in
    (alpha, x, transcript, cm_list, query_list)

  let verify pc_public_parameters transcript ~n ~generator ~commitments
      ~eval_points ?(non_committed = fun _ _ -> SMap.empty) ~identities proof =
    let alpha, x, transcript, cmts, query_list =
      verify_aux transcript generator commitments eval_points proof
    in
    let pc_verif, transcript =
      PC.verify pc_public_parameters transcript cmts query_list proof.pc_answers
        proof.pc_proof
    in
    let answers =
      let f _key m1 m2 = Some (SMap.union_disjoint m1 m2) in
      let answers = List.fold_left (SMap.union f) SMap.empty proof.pc_answers in
      let nc_answers =
        non_committed x answers |> SMap.singleton (string_of_eval_point X)
      in
      SMap.union f answers nc_answers
    in
    let evaluated_ids = identities x answers in
    let t_verif = verify_t n x alpha evaluated_ids proof.cm_t answers in
    (pc_verif && t_verif, transcript)
end

(**  Output signature of the functor [Polynomial_protocol.Make]. *)
module type S = sig
  module PC : Polynomial_commitment.S
  (** Underlying polynomial commitment scheme on which the polynomial protocol
      is based. Input of the functor [Polynomial_protocol.Make]. *)

  (** Module to operate with polynomials in FFT evaluations form. *)
  module Evaluations :
    Evaluations_map.Evaluations_sig
      with type scalar := PC.Scalar.t
       and type domain = PC.Polynomial.Domain.t
       and type polynomial = PC.Polynomial.Polynomial.t
       and type t = PC.Polynomial.Evaluations.t

  type prover_public_parameters = PC.Public_parameters.prover [@@deriving repr]
  (** The type of prover public parameters. *)

  type verifier_public_parameters = PC.Public_parameters.verifier
  [@@deriving repr]
  (** The type of verifier public parameters. *)

  type prover_identities = Evaluations.t SMap.t -> Evaluations.t SMap.t
  (** The type for prover identities: functions from a (string) map of
      polynomials in FFT evaluations form to a (string) map of evaluated
      identities (also polynomials in FFT evaluations form). *)

  type verifier_identities =
    PC.Scalar.t -> PC.Scalar.t SMap.t SMap.t -> PC.Scalar.t SMap.t
  (** The type for verifier identities: functions which map an evaluation point
      ξ an a [PC.answer] into a (string) map of evaluated identities. *)

  type non_committed =
    PC.Scalar.t -> PC.Scalar.t SMap.t SMap.t -> PC.Scalar.t SMap.t
  (** A type to involve in the identities computations corresponding to
    (public) polynomials that have not been committed by the prover.
    It maps an evaluation point ξ and a [PC.answer] into a (string) map
    of evaluated (non-committed) polynomials. *)

  type transcript = PC.transcript [@@deriving repr]
  (** The type for transcripts, used for applying the Fiat-Shamir heuristic *)

  type proof = {
    cm_t : PC.Commitment.t;
    pc_proof : PC.proof;
    pc_answers : PC.answer list;
  }
  [@@deriving repr]
  (** The type for proofs, containing a commitment to the polynomial T that
    asserts the satisfiability of the identities over the subset of interest,
    as well as a [PC] proof and a list of [PC] answers. *)

  (** The type for evaluation points. Either [X], [GX], or a custom point,
      which must be specified by an evaluation point name paired with a
      function that computes it from ξ. For example:
        - [X] could be implemented as [Custom ("x", Fun.id)]
        - [GX] could be implemented as
          [Custom ("gx", fun x -> Scalar.mul generator x)]. *)
  type eval_point = X | GX | Custom of string * (PC.Scalar.t -> PC.Scalar.t)

  val convert_eval_points :
    generator:PC.Scalar.t ->
    x:PC.Scalar.t ->
    eval_point list ->
    PC.Scalar.t SMap.t
  (** [convert_eval_points gen x points] maps the polynomial protocol
     [points : eval_point list] into scalars, by evaluating the underlying
     "composition" polynomial at [x].
     The generator [gen] is used in case the [eval_point] equals [GX], in
     which case the resulting scalar is [x * gen]. *)

  val get_answer : PC.answer -> eval_point -> string -> PC.Scalar.t
  (** [get_answer answers p name] extracts the evaluation of polynomial [name]
      at point [p] from the given [answers]. *)

  val merge_prover_identities : prover_identities list -> prover_identities
  (** A function to merge a list of prover identities into one. *)

  val merge_verifier_identities :
    verifier_identities list -> verifier_identities
  (** A function to merge a list of verifier identities into one. *)

  val compute_t :
    n:int ->
    alpha:PC.Scalar.t ->
    nb_of_t_chunks:int ->
    Evaluations.t SMap.t ->
    Evaluations.polynomial SMap.t
  (** [compute_t ~n ~alpha evaluations] returns a polynomial T splitted in chunks,
     where [T(X) = (sum_i alpha^i evaluations[i]) / (X^n - 1)] and the returned
     chunks [{ 'T_0' -> T0; 'T_1' -> T1; 'T_2' -> T2 }] are such that
     [T = T0 + X^n T1 + X^{2n} T2]. *)

  val setup :
    setup_params:PC.Public_parameters.setup_params ->
    srs:Bls12_381_polynomial.Srs.t * Bls12_381_polynomial.Srs.t ->
    prover_public_parameters * verifier_public_parameters
  (** The polynomial commitment setup function, requires a labeled
      argument of setup parameters for the underlying [PC] and a labeled
      argument containing the path location of a set of SRS files. *)

  val prove :
    prover_public_parameters ->
    transcript ->
    n:int ->
    generator:PC.Scalar.t ->
    secrets:(PC.Polynomial.Polynomial.t SMap.t * PC.Commitment.prover_aux) list ->
    eval_points:eval_point list list ->
    evaluations:Evaluations.t SMap.t ->
    identities:prover_identities ->
    nb_of_t_chunks:int ->
    proof * transcript
  (** The prover function. Takes as input the [prover_public_parameters],
    an initial [transcript] (possibly including a context if this [prove] is
    used as a building block of a bigger protocol), the size [n] of subgroup H,
    the canonical [generator] of subgroup H, a list of [secrets] including
    polynomials that have supposedly been committed (and a verifier received
    such commitments) as well as prover auxiliary information generated
    during the committing process, a list of evaluation point lists specifying
    the evaluation points where each secret needs to be evaluated at,
    a map of the above-mentioned polynomials this time in FFT [evaluations] form,
    for efficient polynomial multiplication, and some [prover_identities] that
    are supposedly satisfied by the secret polynomials.
    Outputs a proof and an updated transcript. *)

  val verify :
    verifier_public_parameters ->
    transcript ->
    n:int ->
    generator:PC.Scalar.t ->
    commitments:PC.Commitment.t list ->
    eval_points:eval_point list list ->
    ?non_committed:non_committed ->
    identities:verifier_identities ->
    proof ->
    bool * transcript
  (** The verifier function. Takes as input the [verifier_public_parameters],
    an initial [transcript] (that should coincide with the initial transcript
    used by [prove]), the size [n] of subgroup H, the canonical [generator] of
    subgroup H, a list of [commitments] to the secret polynomials by the prover,
    a list of evaluation points as in [prove], some [verifier_identities], and
    a [proof].
    Outputs a [bool] value representing acceptance or rejection. *)
end

module Make : functor (PC : Polynomial_commitment.S) -> S with module PC = PC =
  Make_impl

include Make (Polynomial_commitment)