SE SNARK verifier gadget

libsnark/CMakeLists.txt

@@ -386,6 +386,18 @@ target_link_libraries(
   snark
 )
 
+add_executable(
+  gadgetlib1_r1cs_se_ppzksnark_verifier_gadget_test
+  EXCLUDE_FROM_ALL
+
+  gadgetlib1/gadgets/verifiers/tests/test_r1cs_se_ppzksnark_verifier_gadget.cpp
+)
+target_link_libraries(
+  gadgetlib1_r1cs_se_ppzksnark_verifier_gadget_test
+
+  snark
+)
+
 add_executable(
   gadgetlib2_adapters_test
   EXCLUDE_FROM_ALL

libsnark/gadgetlib1/gadgets/basic_gadgets.hpp

@@ -218,6 +218,26 @@ class conjunction_gadget : public gadget<FieldT> {
 template<typename FieldT>
 void test_conjunction_gadget(const size_t n);
 
+  template<typename FieldT>
+class field_vector_equals_gadget : public gadget<FieldT> {
+public:
+    const pb_linear_combination_array<FieldT> X;
+    const pb_linear_combination_array<FieldT> Y;
+    const pb_variable<FieldT> result;
+
+    pb_variable_array<FieldT> results; // boolean
+    pb_variable_array<FieldT> invs;
+
+    std::shared_ptr<conjunction_gadget<FieldT>> all_equal;
+
+    field_vector_equals_gadget(protoboard<FieldT> &pb,
+                               const pb_linear_combination_array<FieldT> &X,
+                               const pb_linear_combination_array<FieldT> &Y,
+                               const pb_variable<FieldT> &result,
+                               const std::string &annotation_prefix="");
+    void generate_r1cs_constraints();
+    void generate_r1cs_witness();
+  };
 template<typename FieldT>
 class comparison_gadget : public gadget<FieldT> {
 private:

libsnark/gadgetlib1/gadgets/basic_gadgets.tcc

@@ -110,7 +110,51 @@ size_t multipacking_num_chunks(const size_t num_bits)
 {
     return libff::div_ceil(num_bits, FieldT::capacity());
 }
+template<typename FieldT>
+field_vector_equals_gadget<FieldT>::field_vector_equals_gadget(
+    protoboard<FieldT> &pb,
+    const pb_linear_combination_array<FieldT> &X,
+    const pb_linear_combination_array<FieldT> &Y,
+    const pb_variable<FieldT> &result,
+    const std::string &annotation_prefix) :
+gadget<FieldT>(pb, annotation_prefix), X(X), Y(Y), result(result)
+{
+    assert(X.size() == Y.size());
+    invs.allocate(pb, X.size(), FMT(this->annotation_prefix, " invs"));
+    results.allocate(pb, X.size(), FMT(this->annotation_prefix, " results"));
+    all_equal.reset(new conjunction_gadget<FieldT>(pb, results, result, FMT(this->annotation_prefix, " all_equal")));
+}
+
+template<typename FieldT>
+void field_vector_equals_gadget<FieldT>::generate_r1cs_constraints()
+{
+    for (size_t i = 0; i < X.size(); ++i)
+    {
+        // If X[i] != Y[i], then results[i] = 0
+        this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(results[i], X[i] - Y[i], 0),
+                                     FMT(this->annotation_prefix, " vector_equals_check_1_%zu", i));
+        // If X[i] = Y[i], then this constraint forces
+        // 0 = 1 - results[i]
+        // so results[i] = 1.
+        this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(invs[i], X[i] - Y[i], 1 - results[i]),
+                                     FMT(this->annotation_prefix, " vector_equals_check_2_%zu", i));
+    }
+
+    all_equal->generate_r1cs_constraints();
+}
 
+template<typename FieldT>
+void field_vector_equals_gadget<FieldT>::generate_r1cs_witness()
+{
+    for (size_t i = 0; i < X.size(); ++i) {
+        FieldT x = this->pb.lc_val(X[i]);
+        FieldT y = this->pb.lc_val(Y[i]);
+        bool equal = x == y;
+        this->pb.val(results[i]) = equal ? FieldT::one() : FieldT::zero();
+        this->pb.val(invs[i]) = equal ? FieldT::zero() : (x - y).inverse();
+    }
+    all_equal->generate_r1cs_witness();
+}
 template<typename FieldT>
 field_vector_copy_gadget<FieldT>::field_vector_copy_gadget(protoboard<FieldT> &pb,
                                                            const pb_variable_array<FieldT> &source,

libsnark/gadgetlib1/gadgets/curves/weierstrass_g2_gadget.hpp

@@ -81,6 +81,43 @@ class G2_checker_gadget : public gadget<libff::Fr<ppT> > {
     void generate_r1cs_witness();
 };
 
+/**
+ * Gadget that creates constraints for G2 addition.
+ */
+template<typename ppT>
+class G2_add_gadget : public gadget<libff::Fr<ppT> > {
+public:
+    typedef libff::Fr<ppT> FieldT;
+    typedef libff::Fqe<other_curve<ppT> > FqeT;
+
+    std::shared_ptr<Fqe_variable<ppT>> lambda;
+    std::shared_ptr<Fqe_variable<ppT>> inv;
+
+    G2_variable<ppT> A;
+    G2_variable<ppT> B;
+    G2_variable<ppT> C;
+
+    std::shared_ptr<Fqe_variable<ppT> > B_x_sub_A_x;
+    std::shared_ptr<Fqe_variable<ppT> > B_y_sub_A_y;
+    std::shared_ptr<Fqe_variable<ppT> > C_x_add_A_x_add_B_x;
+    std::shared_ptr<Fqe_variable<ppT> > A_x_sub_C_x;
+    std::shared_ptr<Fqe_variable<ppT> > C_y_add_A_y;
+    std::shared_ptr<Fqe_variable<ppT> > Fqe_one;
+
+    std::shared_ptr<Fqe_mul_gadget<ppT> > calc_lambda;
+    std::shared_ptr<Fqe_mul_gadget<ppT> > calc_X;
+    std::shared_ptr<Fqe_mul_gadget<ppT> > calc_Y;
+    std::shared_ptr<Fqe_mul_gadget<ppT> > no_special_cases;
+
+    G2_add_gadget(protoboard<FieldT> &pb,
+                  const G2_variable<ppT> &A,
+                  const G2_variable<ppT> &B,
+                  const G2_variable<ppT> &C,
+                  const std::string &annotation_prefix);
+    void generate_r1cs_constraints();
+    void generate_r1cs_witness();
+};
+
 } // libsnark
 
 #include <libsnark/gadgetlib1/gadgets/curves/weierstrass_g2_gadget.tcc>

libsnark/gadgetlib1/gadgets/curves/weierstrass_g2_gadget.tcc

@@ -125,6 +125,102 @@ void test_G2_checker_gadget(const std::string &annotation)
     printf("number of constraints for G2 checker (Fr is %s)  = %zu\n", annotation.c_str(), pb.num_constraints());
 }
 
+template<typename ppT>
+G2_add_gadget<ppT>::G2_add_gadget(protoboard<FieldT> &pb,
+                                  const G2_variable<ppT> &A,
+                                  const G2_variable<ppT> &B,
+                                  const G2_variable<ppT> &C,
+                                  const std::string &annotation_prefix) :
+    gadget<FieldT>(pb, annotation_prefix),
+    A(A),
+    B(B),
+    C(C)
+{
+    /*
+      lambda = (B.y - A.y)/(B.x - A.x)
+      C.x = lambda^2 - A.x - B.x
+      C.y = lambda(A.x - C.x) - A.y
+
+      Special cases:
+
+      doubling: if B.y = A.y and B.x = A.x then lambda is unbound and
+      C = (lambda^2, lambda^3)
+
+      addition of negative point: if B.y = -A.y and B.x = A.x then no
+      lambda can satisfy the first equation unless B.y - A.y = 0. But
+      then this reduces to doubling.
+
+      So we need to check that A.x - B.x != 0, which can be done by
+      enforcing I * (B.x - A.x) = 1
+    */
+
+    lambda.reset(
+      new Fqe_variable<ppT>(pb, FMT(annotation_prefix, " lambda")));
+    inv.reset(
+      new Fqe_variable<ppT>(pb, FMT(annotation_prefix, " lambda")));
+    B_x_sub_A_x.reset(
+      new Fqe_variable<ppT>(*(B.X) - *(A.X)));
+    B_y_sub_A_y.reset(
+      new Fqe_variable<ppT>(*(B.Y) - *(A.Y)));
+    C_x_add_A_x_add_B_x.reset(
+      new Fqe_variable<ppT>(*(C.X) + *(A.X) + *(B.X)));
+    A_x_sub_C_x.reset(
+      new Fqe_variable<ppT>(*(A.X) - *(C.X)));
+    C_y_add_A_y.reset(
+      new Fqe_variable<ppT>(*(C.Y) + *(A.Y)));
+    Fqe_one.reset(
+      new Fqe_variable<ppT>(pb, FqeT::one(), FMT(annotation_prefix, "Fqe_one")));
+
+    calc_lambda.reset(new Fqe_mul_gadget<ppT>(pb,
+          *lambda, *B_x_sub_A_x, *B_y_sub_A_y,
+          FMT(annotation_prefix, " calc_lambda")));
+    calc_X.reset(new Fqe_mul_gadget<ppT>(pb,
+          *lambda, *lambda, *C_x_add_A_x_add_B_x,
+          FMT(annotation_prefix, " calc_X")));
+    calc_Y.reset(new Fqe_mul_gadget<ppT>(pb,
+          *lambda, *A_x_sub_C_x, *C_y_add_A_y,
+          FMT(annotation_prefix, " calc_Y")));
+    no_special_cases.reset(new Fqe_mul_gadget<ppT>(pb,
+          *inv, *B_x_sub_A_x, *Fqe_one,
+          FMT(annotation_prefix, " no_special_cases")));
+}
+
+template<typename ppT>
+void G2_add_gadget<ppT>::generate_r1cs_constraints()
+{
+    calc_lambda->generate_r1cs_constraints();
+    calc_X->generate_r1cs_constraints();
+    calc_Y->generate_r1cs_constraints();
+    no_special_cases->generate_r1cs_constraints();
+}
+
+template<typename ppT>
+void G2_add_gadget<ppT>::generate_r1cs_witness()
+{
+    inv->generate_r1cs_witness(
+      ( B.X->get_element() - A.X->get_element() ).inverse());
+    lambda->generate_r1cs_witness(
+      (B.Y->get_element() - A.Y->get_element())
+      * inv->get_element() );
+
+    C.X->generate_r1cs_witness(
+      lambda->get_element().squared() - A.X->get_element() - B.X->get_element());
+    C.Y->generate_r1cs_witness(
+      lambda->get_element() * ( A.X->get_element() - C.X->get_element()) - A.Y->get_element());
+
+    B_x_sub_A_x->evaluate();
+    B_y_sub_A_y->evaluate();
+    C_x_add_A_x_add_B_x->evaluate();
+    A_x_sub_C_x->evaluate();
+    C_y_add_A_y->evaluate();
+    Fqe_one->evaluate();
+
+    calc_lambda->generate_r1cs_witness_internal();
+    calc_X->generate_r1cs_witness_internal();
+    calc_Y->generate_r1cs_witness_internal();
+    no_special_cases->generate_r1cs_witness_internal();
+}
+
 } // libsnark
 
 #endif // WEIERSTRASS_G2_GADGET_TCC_

libsnark/gadgetlib1/gadgets/fields/fp2_gadgets.hpp

@@ -55,6 +55,7 @@ class Fp2_variable : public gadget<typename Fp2T::my_Fp> {
     Fp2_variable<Fp2T> operator*(const FieldT &coeff) const;
     Fp2_variable<Fp2T> operator+(const Fp2_variable<Fp2T> &other) const;
     Fp2_variable<Fp2T> operator+(const Fp2T &other) const;
+    Fp2_variable<Fp2T> operator-(const Fp2_variable<Fp2T> &other) const;
     Fp2_variable<Fp2T> mul_by_X() const;
     void evaluate() const;
     bool is_constant() const;
@@ -83,6 +84,7 @@ class Fp2_mul_gadget : public gadget<typename Fp2T::my_Fp> {
                    const Fp2_variable<Fp2T> &result,
                    const std::string &annotation_prefix);
     void generate_r1cs_constraints();
+    void generate_r1cs_witness_internal();
     void generate_r1cs_witness();
 };
 

libsnark/gadgetlib1/gadgets/fields/fp2_gadgets.tcc

@@ -116,6 +116,15 @@ Fp2_variable<Fp2T> Fp2_variable<Fp2T>::operator+(const Fp2_variable<Fp2T> &other
     return Fp2_variable<Fp2T>(this->pb, new_c0, new_c1, FMT(this->annotation_prefix, " operator+"));
 }
 
+template<typename Fp2T>
+Fp2_variable<Fp2T> Fp2_variable<Fp2T>::operator-(const Fp2_variable<Fp2T> &other) const
+{
+    pb_linear_combination<FieldT> new_c0, new_c1;
+    new_c0.assign(this->pb, this->c0 - other.c0);
+    new_c1.assign(this->pb, this->c1 - other.c1);
+    return Fp2_variable<Fp2T>(this->pb, new_c0, new_c1, FMT(this->annotation_prefix, " operator-"));
+}
+
 template<typename Fp2T>
 Fp2_variable<Fp2T> Fp2_variable<Fp2T>::operator+(const Fp2T &other) const
 {
@@ -198,11 +207,17 @@ void Fp2_mul_gadget<Fp2T>::generate_r1cs_constraints()
                                  FMT(this->annotation_prefix, " result.c1"));
 }
 
+template<typename Fp2T>
+void Fp2_mul_gadget<Fp2T>::generate_r1cs_witness_internal()
+{
+    this->pb.val(v1) = this->pb.lc_val(A.c1) * this->pb.lc_val(B.c1);
+}
+
 template<typename Fp2T>
 void Fp2_mul_gadget<Fp2T>::generate_r1cs_witness()
 {
     const FieldT aA = this->pb.lc_val(A.c0) * this->pb.lc_val(B.c0);
-    this->pb.val(v1) = this->pb.lc_val(A.c1) * this->pb.lc_val(B.c1);
+    this->generate_r1cs_witness_internal();
     this->pb.lc_val(result.c0) = aA + Fp2T::non_residue * this->pb.val(v1);
     this->pb.lc_val(result.c1) = (this->pb.lc_val(A.c0) + this->pb.lc_val(A.c1)) * (this->pb.lc_val(B.c0) + this->pb.lc_val(B.c1)) - aA - this->pb.lc_val(v1);
 }

libsnark/gadgetlib1/gadgets/fields/fp3_gadgets.hpp

@@ -57,6 +57,7 @@ class Fp3_variable : public gadget<typename Fp3T::my_Fp> {
     Fp3_variable<Fp3T> operator*(const FieldT &coeff) const;
     Fp3_variable<Fp3T> operator+(const Fp3_variable<Fp3T> &other) const;
     Fp3_variable<Fp3T> operator+(const Fp3T &other) const;
+    Fp3_variable<Fp3T> operator-(const Fp3_variable<Fp3T> &other) const;
     Fp3_variable<Fp3T> mul_by_X() const;
     void evaluate() const;
     bool is_constant() const;
@@ -86,6 +87,7 @@ class Fp3_mul_gadget : public gadget<typename Fp3T::my_Fp> {
                    const Fp3_variable<Fp3T> &result,
                    const std::string &annotation_prefix);
     void generate_r1cs_constraints();
+    void generate_r1cs_witness_internal();
     void generate_r1cs_witness();
 };
 

libsnark/gadgetlib1/gadgets/fields/fp3_gadgets.tcc

@@ -132,6 +132,16 @@ Fp3_variable<Fp3T> Fp3_variable<Fp3T>::operator+(const Fp3_variable<Fp3T> &other
     return Fp3_variable<Fp3T>(this->pb, new_c0, new_c1, new_c2, FMT(this->annotation_prefix, " operator+"));
 }
 
+template<typename Fp3T>
+Fp3_variable<Fp3T> Fp3_variable<Fp3T>::operator-(const Fp3_variable<Fp3T> &other) const
+{
+    pb_linear_combination<FieldT> new_c0, new_c1, new_c2;
+    new_c0.assign(this->pb, this->c0 - other.c0);
+    new_c1.assign(this->pb, this->c1 - other.c1);
+    new_c2.assign(this->pb, this->c2 - other.c2);
+    return Fp3_variable<Fp3T>(this->pb, new_c0, new_c1, new_c2, FMT(this->annotation_prefix, " operator-"));
+}
+
 template<typename Fp3T>
 Fp3_variable<Fp3T> Fp3_variable<Fp3T>::operator+(const Fp3T &other) const
 {
@@ -248,10 +258,16 @@ void Fp3_mul_gadget<Fp3T>::generate_r1cs_constraints()
 }
 
 template<typename Fp3T>
-void Fp3_mul_gadget<Fp3T>::generate_r1cs_witness()
+void Fp3_mul_gadget<Fp3T>::generate_r1cs_witness_internal()
 {
     this->pb.val(v0) = this->pb.lc_val(A.c0) * this->pb.lc_val(B.c0);
     this->pb.val(v4) = this->pb.lc_val(A.c2) * this->pb.lc_val(B.c2);
+}
+
+template<typename Fp3T>
+void Fp3_mul_gadget<Fp3T>::generate_r1cs_witness()
+{
+    this->generate_r1cs_witness_internal();
 
     const Fp3T Aval = A.get_element();
     const Fp3T Bval = B.get_element();

libsnark/gadgetlib1/gadgets/fields/fp4_gadgets.hpp

@@ -32,15 +32,25 @@ class Fp4_variable : public gadget<typename Fp4T::my_Fp> {
     Fp2_variable<Fp2T> c0;
     Fp2_variable<Fp2T> c1;
 
+  pb_linear_combination_array<FieldT> all_vars;
+
+
     Fp4_variable(protoboard<FieldT> &pb, const std::string &annotation_prefix);
     Fp4_variable(protoboard<FieldT> &pb, const Fp4T &el, const std::string &annotation_prefix);
     Fp4_variable(protoboard<FieldT> &pb, const Fp2_variable<Fp2T> &c0, const Fp2_variable<Fp2T> &c1, const std::string &annotation_prefix);
+
+  void generate_r1cs_equals_constraints(const Fp4_variable<Fp4T> &other);
+  void generate_r1cs_equals_unitary_inverse_constraints(const Fp4_variable<Fp4T> &other);
     void generate_r1cs_equals_const_constraints(const Fp4T &el);
     void generate_r1cs_witness(const Fp4T &el);
     Fp4T get_element();
 
     Fp4_variable<Fp4T> Frobenius_map(const size_t power) const;
     void evaluate() const;
+
+  static size_t __attribute__((noinline)) size_in_bits();
+  static size_t num_variables();
+
 };
 
 /**