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

open Bls
open Identities
module L = Plompiler.LibCircuit

module type S = sig
  val arith_label : string

  val qadv_label : string

  val com_label : string

  val gates_list : string list

  val nb_custom_gates : int

  val nb_input_com : int

  val get_eqs :
    string ->
    q:Scalar.t ->
    wires:Scalar.t array ->
    wires_g:Scalar.t array ->
    ?precomputed_advice:Scalar.t SMap.t ->
    unit ->
    Scalar.t list

  val get_ids : string -> string * int

  val get_cs :
    string ->
    q:L.scalar L.repr ->
    wires:L.scalar L.repr array ->
    wires_g:L.scalar L.repr array ->
    ?precomputed_advice:L.scalar L.repr SMap.t ->
    unit ->
    L.scalar L.repr list L.t

  val aggregate_prover_identities :
    ?circuit_prefix:(string -> string) ->
    input_coms_size:int ->
    proof_prefix:(string -> string) ->
    gates:'a SMap.t ->
    public_inputs:Scalar.t array ->
    domain:Domain.t ->
    unit ->
    prover_identities

  val aggregate_verifier_identities :
    ?circuit_prefix:(string -> string) ->
    input_com_sizes:int list ->
    proof_prefix:(string -> string) ->
    gates:'a SMap.t ->
    public_inputs:Scalar.t array ->
    generator:Scalar.t ->
    size_domain:int ->
    unit ->
    verifier_identities

  val aggregate_polynomials_degree : gates:'a SMap.t -> int

  val exists_gx_composition : gates:'a SMap.t -> bool

  val cs_pi :
    generator:Scalar.t ->
    n:Scalar.t ->
    x:L.scalar L.repr ->
    zs:L.scalar L.repr ->
    L.scalar L.repr list ->
    L.scalar L.repr L.t
end

module Aggregator = struct
  open Gates_common

  let arith_label = arith

  let com_label = com_label

  let qadv_label = qadv_label

  (* Maximum number of input commitments that can be used in a proof *)
  let nb_input_com = 3

  let gates_map =
    let open Arithmetic_gates in
    let open Boolean_gates in
    let open Hash_gates in
    let open Ecc_gates in
    let open Mod_arith_gates in
    let linear_monomials =
      let open Plompiler.Csir in
      List.init nb_wires_arch (fun i -> (linear_selector_name i, i))
    in
    SMap.of_list
      ([
         (Public.q_label, (module Public : Base_sig));
         (Constant.q_label, (module Constant));
         (Multiplication.q_label, (module Multiplication));
         (X5A.q_label, (module X5A));
         (X5C.q_label, (module X5C));
         (X2B.q_label, (module X2B));
         (AddWeierstrass.q_label, (module AddWeierstrass));
         (AddEdwards.q_label, (module AddEdwards));
         (ConditionalAddEdwards.q_label, (module ConditionalAddEdwards));
         (BoolCheck.q_label, (module BoolCheck));
         (CondSwap.q_label, (module CondSwap));
         (AnemoiDouble.q_label, (module AnemoiDouble));
         (AddMod25519.q_label, (module AddMod25519));
         (MulMod25519.q_label, (module MulMod25519));
         (AddMod64.q_label, (module AddMod64));
         (MulMod64.q_label, (module MulMod64));
       ]
      @ List.map (fun (q, i) -> (q, linear_monomial i q)) linear_monomials
      @ List.map
          (fun (q, i) ->
            let q = Plompiler.Csir.add_next_wire_suffix q in
            (q, linear_monomial ~is_next:true i q))
          linear_monomials
      @ List.init nb_input_com (fun i ->
            ( "qcom" ^ string_of_int i,
              (module InputCom (struct
                let idx = i
              end) : Base_sig) )))

  let gates_list = SMap.keys gates_map

  let nb_custom_gates = SMap.cardinal gates_map

  (* Removes non-custom-gates from gates (for example q_plookup) *)
  let filter_gates gates = SMap.(filter (fun q _ -> mem q gates_map) gates)

  let find_gate q =
    match SMap.find_opt q gates_map with
    | Some gate -> gate
    | None ->
        failwith
          (Printf.sprintf "\nCustom_gates.find_gate : unknown selector %s." q)

  let get_prover_identities q =
    let module M = (val find_gate q : Base_sig) in
    M.prover_identities

  let get_coms q =
    let module M = (val find_gate q : Base_sig) in
    M.index_com

  let get_nb_advs q =
    let module M = (val find_gate q : Base_sig) in
    M.nb_advs

  let get_nb_buffers q =
    let module M = (val find_gate q : Base_sig) in
    M.nb_buffers

  let get_verifier_identities q =
    let module M = (val find_gate q : Base_sig) in
    M.verifier_identities

  let get_polynomials_degree q =
    let module M = (val find_gate q : Base_sig) in
    M.polynomials_degree

  let get_eqs q =
    let module M = (val find_gate q : Base_sig) in
    M.equations

  let get_ids q =
    let module M = (val find_gate q : Base_sig) in
    M.identity

  let get_cs q =
    let module M = (val find_gate q : Base_sig) in
    M.cs

  let get_gx_composition q =
    let module M = (val find_gate q : Base_sig) in
    M.gx_composition

  let exists_gx_composition ~gates =
    SMap.exists (fun q _ -> get_gx_composition q) (filter_gates gates)

  let wires_map prefix get =
    List.init Plompiler.Csir.nb_wires_arch (fun i ->
        let w = prefix @@ wire_name i in
        (w, get w))
    |> SMap.of_list

  let filter_evaluations ~evaluations ~prefix ~circuit_prefix gates =
    let get_eval = Evaluations.find_evaluation evaluations in
    let base = SMap.singleton "X" (get_eval "X") in
    (* Add wires *)
    let wires = SMap.union_disjoint base (wires_map prefix get_eval) in
    List.fold_left
      (fun acc gate ->
        (* Adding commitments *)
        let acc =
          match get_coms gate with
          | None -> acc
          | Some idx ->
              let com_i = prefix com_label ^ string_of_int idx in
              SMap.add com_i (get_eval com_i) acc
        in
        (* Adding advice *)
        let acc =
          List.init (get_nb_advs gate) (fun i ->
              circuit_prefix qadv_label ^ string_of_int i)
          |> List.fold_left
               (fun acc2 adv_i -> SMap.add adv_i (get_eval adv_i) acc2)
               acc
        in
        (* Adding selector *)
        let gate = circuit_prefix gate in
        if gate = circuit_prefix "qpub" then acc
        else SMap.add gate (get_eval gate) acc)
      wires
      gates

  let filter_answers ~answers ~prefix ~circuit_prefix gates =
    let x, gx = (string_of_eval_point X, string_of_eval_point GX) in
    let get_x, get_gx = (get_answer answers X, get_answer answers GX) in
    let add_mapmap k' k v mm =
      SMap.(update k' (fun m -> Option.bind m (fun m -> Some (add k v m)))) mm
    in
    let add_x = add_mapmap x in
    (* Wires map *)
    let wires =
      let base = SMap.singleton x (wires_map prefix get_x) in
      let wires_g =
        if exists_gx_composition ~gates then wires_map prefix get_gx
        else SMap.empty
      in
      SMap.add_unique gx wires_g base
    in
    SMap.fold
      (fun gate _ acc ->
        (* Adding input_commitments *)
        let acc =
          match get_coms gate with
          | None -> acc
          | Some idx ->
              let com_i = prefix com_label ^ string_of_int idx in
              add_x com_i (get_x com_i) acc
        in
        (* Adding advice *)
        let acc =
          List.init (get_nb_advs gate) (fun i ->
              circuit_prefix qadv_label ^ string_of_int i)
          |> List.fold_left
               (fun acc2 adv_i -> add_x adv_i (get_x adv_i) acc2)
               acc
        in
        (* Adding selector *)
        let gate = circuit_prefix gate in
        if gate = circuit_prefix "qpub" then acc
        else add_x gate (get_x gate) acc)
      gates
      wires

  let aggregate_prover_identities ?(circuit_prefix = Fun.id) ~input_coms_size
      ~proof_prefix:prefix ~gates ~public_inputs ~domain () : prover_identities
      =
   fun evaluations ->
    let size_eval = Evaluations.size_evaluations evaluations in
    (* Sort and filter gates according to nb of tmp buffers *)
    let gates =
      List.sort
        (fun gate1 gate2 ->
          Int.compare (get_nb_buffers gate1) (get_nb_buffers gate2))
        (filter_gates gates |> SMap.keys)
    in
    (* Creating tmp buffers for prover identities *)
    let nb_min_buffers =
      match gates with
      | [] -> 0
      | hd_gates :: _ -> max 1 (get_nb_buffers hd_gates)
    in
    tmp_buffers :=
      Array.init nb_min_buffers (fun _ -> Evaluations.create size_eval) ;
    (* Filter evaluations *)
    let evaluations =
      filter_evaluations ~evaluations ~prefix ~circuit_prefix gates
    in
    (* Except for the arithmetic gates,
       all gates correspond to distinct identities. *)
    let init_ids =
      let arith_acc_evaluation = Evaluations.create size_eval in
      SMap.singleton (prefix @@ arith ^ ".0") arith_acc_evaluation
    in
    let union key e1 e2 =
      assert (key = prefix @@ arith ^ ".0") ;
      Some (Evaluations.add ~res:e1 e1 e2)
    in
    let public = {public_inputs; input_coms_size} in
    List.fold_left
      (fun accumulated_ids gate ->
        SMap.union
          union
          accumulated_ids
          (get_prover_identities
             gate
             ~prefix_common:circuit_prefix
             ~prefix
             ~public
             ~domain
             evaluations))
      init_ids
      gates

  let aggregate_verifier_identities ?(circuit_prefix = Fun.id) ~input_com_sizes
      ~proof_prefix:prefix ~gates ~public_inputs ~generator ~size_domain () :
      verifier_identities =
   fun x answers ->
    let gates = filter_gates gates in
    let answers = filter_answers ~answers ~prefix ~circuit_prefix gates in
    let arith_id = SMap.singleton (prefix @@ arith ^ ".0") Scalar.zero in
    let union key s1 s2 =
      assert (key = prefix @@ arith ^ ".0") ;
      Some (Scalar.add s1 s2)
    in
    let public =
      {public_inputs; input_coms_size = List.fold_left ( + ) 0 input_com_sizes}
    in
    SMap.fold
      (fun gate _ accumulated_ids ->
        let gate_ids =
          get_verifier_identities
            gate
            ~prefix_common:circuit_prefix
            ~prefix
            ~public
            ~generator
            ~size_domain
        in
        SMap.union union accumulated_ids (gate_ids x answers))
      gates
      arith_id

  let aggregate_polynomials_degree ~gates =
    SMap.fold
      (fun gate _ degree ->
        let map = get_polynomials_degree gate in
        SMap.fold (fun _ d acc -> max d acc) map degree)
      (filter_gates gates)
      0

  (* - (x^n -1)/n·(w0/(x -1) + w1/(x/g - 1) + … + wn/(x/g^n - 1)) *)
  let cs_pi ~generator ~n ~x ~zs pi_list =
    let open L in
    let open Num in
    let mone = Scalar.(negate one) in
    let n_inv = Scalar.(inverse_exn (negate n)) in
    let g_inv = Scalar.inverse_exn generator in
    match pi_list with
    | [] -> Num.zero
    | hd :: tl_pi ->
        (* negate because we want -PI(x) *)
        let* left_term = mul_by_constant n_inv zs in
        let* init_value =
          let* x_minus_one = add_constant mone x in
          div hd x_minus_one
        in
        let* sum, _g_inv_k =
          foldM
            (fun (res, g_inv_k) w_k ->
              let* x_g_inv_k_minus_one = add_constant ~ql:g_inv_k mone x in
              let* to_add = div w_k x_g_inv_k_minus_one in
              let* res = add res to_add in
              ret (res, Scalar.mul g_inv_k g_inv))
            (init_value, g_inv)
            tl_pi
        in
        mul left_term sum
end

include (Aggregator : S)