VK summary (#1391)

This PR adds verification key 'summaries' to the snarky verifiers.

Basically we construct a (non-deterministic, non-total) function `summary : G1.t list * G2.t list * Fqk.Unitary.t list -> bool list` which is injective (if it doesn't throw). By `Fqk.Unitary.t` I mean Fqk elements which are unitary. `a + b beta : Fqk.t` is unitary if `(a + b beta)(a - b beta) = 1`.

The summary works element-wise as follows:
- G1 elements are mapped to their x coordinate and the parity of their y coordinate
- G2 elements are mapped to their x coordinate and the parity of the 'real part' of their y coordinate, assuming the real part is non-zero
- Fqk.t elements `a + b beta` are mapped to `a` and the parity of the 'real part' of `b`, assuming the real part is non-zero. `b` is determined up to sign by `a` by unitary-ness.

The point of this is for making hashing more efficient. `summary` shrinks the size of its input, so you can get away with hashing fewer bits.

Author: imeckler

src/lib/snarky_verifier/groth.ml

@@ -4,11 +4,19 @@ open Core
 module Make (Inputs : Inputs.S) = struct
   open Inputs
   open Impl
+  open Let_syntax
 
   module Verification_key = struct
     type ('g1, 'g2, 'fqk) t_ =
       {query_base: 'g1; query: 'g1 list; delta: 'g2; alpha_beta_inv: 'fqk}
 
+    include Summary.Make (Inputs)
+
+    let summary_input {query_base; query; delta; alpha_beta_inv} =
+      { Summary.Input.g1s= query_base :: query
+      ; g2s= [delta]
+      ; gts= [alpha_beta_inv] }
+
     type ('a, 'b, 'c) vk = ('a, 'b, 'c) t_
 
     module Precomputation = struct
@@ -40,7 +48,6 @@ module Make (Inputs : Inputs.S) = struct
 
   let verify (vk : (_, _, _) Verification_key.t_)
       (vk_precomp : Verification_key.Precomputation.t) inputs {Proof.a; b; c} =
-    let open Let_syntax in
     let%bind acc =
       let%bind (module Shifted) = G1.Shifted.create () in
       let%bind init = Shifted.(add zero vk.query_base) in

src/lib/snarky_verifier/groth_maller.ml

@@ -17,6 +17,21 @@ module Make (Inputs : Inputs.S) = struct
       ; h_gamma: 'g2
       ; g_alpha_h_beta: 'fqk }
 
+    include Summary.Make (Inputs)
+
+    let summary_input
+        { g_alpha
+        ; g_gamma
+        ; query_base
+        ; query
+        ; h
+        ; h_beta
+        ; h_gamma
+        ; g_alpha_h_beta } =
+      { Summary.Input.g1s= g_alpha :: g_gamma :: query_base :: query
+      ; g2s= [h; h_beta; h_gamma]
+      ; gts= [g_alpha_h_beta] }
+
     type ('a, 'b, 'c) vk = ('a, 'b, 'c) t_
 
     module Precomputation = struct

src/lib/snarky_verifier/inputs.ml

@@ -74,6 +74,14 @@ module type S = sig
     val one : t
   end
 
+  module Fqe : sig
+    type _ t_
+
+    val real_part : 'a t_ -> 'a
+
+    val parts : 'a t_ -> 'a list
+  end
+
   val group_miller_loop :
        (Sgn.t * G1_precomputation.t * G2_precomputation.t) list
     -> (Fqk.t, _) Checked.t

src/lib/snarky_verifier/summary.ml

@@ -0,0 +1,67 @@
+open Core_kernel
+
+module type Inputs_intf = sig
+  module Impl : Snarky.Snark_intf.S
+
+  module Fqe : sig
+    type _ t_
+
+    val real_part : 'a t_ -> 'a
+
+    val parts : 'a t_ -> 'a list
+  end
+end
+
+module Input = struct
+  type ('g1, 'g2, 'gt) t = {g1s: 'g1 list; g2s: 'g2 list; gts: 'gt list}
+end
+
+module Make (Inputs : Inputs_intf) = struct
+  open Inputs
+  open Impl
+  open Let_syntax
+
+  let summary {Input.g1s; g2s; gts} =
+    let%map elts =
+      List.map g1s ~f:(fun (x, _) -> x)
+      @ List.concat_map g2s ~f:(fun (x, _) -> Fqe.parts x)
+      @ List.concat_map gts ~f:(fun (a, _) -> Fqe.parts a)
+      |> Checked.List.map ~f:(fun x ->
+             Field.Checked.choose_preimage_var x ~length:Field.size_in_bits
+             >>| List.hd_exn )
+    and signs =
+      let parity x =
+        let%map bs = Field.Checked.unpack_full x in
+        List.hd_exn (bs :> Boolean.var list)
+      in
+      let real_part_parity a =
+        let x = Fqe.real_part a in
+        let%bind () = Field.Checked.Assert.non_zero x in
+        parity x
+      in
+      let%map g1s = Checked.List.map g1s ~f:(fun (_, y) -> parity y)
+      and g2s = Checked.List.map g2s ~f:(fun (_, y) -> real_part_parity y)
+      and gts = Checked.List.map gts ~f:(fun (_, b) -> real_part_parity b) in
+      g1s @ g2s @ gts
+    in
+    elts @ signs
+
+  let summary_unchecked {Input.g1s; g2s; gts} =
+    let parity x = Bigint.(test_bit (of_field x) 0) in
+    let elts =
+      List.map g1s ~f:(fun (x, _) -> x)
+      @ List.concat_map g2s ~f:(fun (x, _) -> Fqe.parts x)
+      @ List.concat_map gts ~f:(fun (a, _) -> Fqe.parts a)
+      |> List.map ~f:parity
+    and signs =
+      let real_part_parity a =
+        let x = Fqe.real_part a in
+        assert (not (Field.equal Field.zero x)) ;
+        parity x
+      in
+      List.map g1s ~f:(fun (_, y) -> parity y)
+      @ List.map g2s ~f:(fun (_, y) -> real_part_parity y)
+      @ List.map gts ~f:(fun (_, b) -> real_part_parity b)
+    in
+    elts @ signs
+end