/** @file ***************************************************************************** * @author This file is part of libsnark, developed by SCIPR Lab * and contributors (see AUTHORS). * @copyright MIT license (see LICENSE file) *****************************************************************************/ #ifndef BASIC_GADGETS_TCC_ #define BASIC_GADGETS_TCC_ #include "common/profiling.hpp" #include "common/utils.hpp" namespace libsnark { template void generate_boolean_r1cs_constraint(protoboard &pb, const pb_linear_combination &lc, const std::string &annotation_prefix) /* forces lc to take value 0 or 1 by adding constraint lc * (1-lc) = 0 */ { pb.add_r1cs_constraint(r1cs_constraint(lc, 1-lc, 0), FMT(annotation_prefix, " boolean_r1cs_constraint")); } template void generate_r1cs_equals_const_constraint(protoboard &pb, const pb_linear_combination &lc, const FieldT& c, const std::string &annotation_prefix) { pb.add_r1cs_constraint(r1cs_constraint(1, lc, c), FMT(annotation_prefix, " constness_constraint")); } template void packing_gadget::generate_r1cs_constraints(const bool enforce_bitness) /* adds constraint result = \sum bits[i] * 2^i */ { this->pb.add_r1cs_constraint(r1cs_constraint(1, pb_packing_sum(bits), packed), FMT(this->annotation_prefix, " packing_constraint")); if (enforce_bitness) { for (size_t i = 0; i < bits.size(); ++i) { generate_boolean_r1cs_constraint(this->pb, bits[i], FMT(this->annotation_prefix, " bitness_%zu", i)); } } } template void packing_gadget::generate_r1cs_witness_from_packed() { packed.evaluate(this->pb); assert(this->pb.lc_val(packed).as_bigint().num_bits() <= bits.size()); bits.fill_with_bits_of_field_element(this->pb, this->pb.lc_val(packed)); } template void packing_gadget::generate_r1cs_witness_from_bits() { bits.evaluate(this->pb); this->pb.lc_val(packed) = bits.get_field_element_from_bits(this->pb); } template multipacking_gadget::multipacking_gadget(protoboard &pb, const pb_linear_combination_array &bits, const pb_linear_combination_array &packed_vars, const size_t chunk_size, const std::string &annotation_prefix) : gadget(pb, annotation_prefix), bits(bits), packed_vars(packed_vars), chunk_size(chunk_size), num_chunks(div_ceil(bits.size(), chunk_size)) // last_chunk_size(bits.size() - (num_chunks-1) * chunk_size) { assert(packed_vars.size() == num_chunks); for (size_t i = 0; i < num_chunks; ++i) { packers.emplace_back(packing_gadget(this->pb, pb_linear_combination_array(bits.begin() + i * chunk_size, bits.begin() + std::min((i+1) * chunk_size, bits.size())), packed_vars[i], FMT(this->annotation_prefix, " packers_%zu", i))); } } template void multipacking_gadget::generate_r1cs_constraints(const bool enforce_bitness) { for (size_t i = 0; i < num_chunks; ++i) { packers[i].generate_r1cs_constraints(enforce_bitness); } } template void multipacking_gadget::generate_r1cs_witness_from_packed() { for (size_t i = 0; i < num_chunks; ++i) { packers[i].generate_r1cs_witness_from_packed(); } } template void multipacking_gadget::generate_r1cs_witness_from_bits() { for (size_t i = 0; i < num_chunks; ++i) { packers[i].generate_r1cs_witness_from_bits(); } } template size_t multipacking_num_chunks(const size_t num_bits) { return div_ceil(num_bits, FieldT::capacity()); } template field_vector_copy_gadget::field_vector_copy_gadget(protoboard &pb, const pb_variable_array &source, const pb_variable_array &target, const pb_linear_combination &do_copy, const std::string &annotation_prefix) : gadget(pb, annotation_prefix), source(source), target(target), do_copy(do_copy) { assert(source.size() == target.size()); } template void field_vector_copy_gadget::generate_r1cs_constraints() { for (size_t i = 0; i < source.size(); ++i) { this->pb.add_r1cs_constraint(r1cs_constraint(do_copy, source[i] - target[i], 0), FMT(this->annotation_prefix, " copying_check_%zu", i)); } } template void field_vector_copy_gadget::generate_r1cs_witness() { do_copy.evaluate(this->pb); assert(this->pb.lc_val(do_copy) == FieldT::one() || this->pb.lc_val(do_copy) == FieldT::zero()); if (this->pb.lc_val(do_copy) != FieldT::zero()) { for (size_t i = 0; i < source.size(); ++i) { this->pb.val(target[i]) = this->pb.val(source[i]); } } } template bit_vector_copy_gadget::bit_vector_copy_gadget(protoboard &pb, const pb_variable_array &source_bits, const pb_variable_array &target_bits, const pb_linear_combination &do_copy, const size_t chunk_size, const std::string &annotation_prefix) : gadget(pb, annotation_prefix), source_bits(source_bits), target_bits(target_bits), do_copy(do_copy), chunk_size(chunk_size), num_chunks(div_ceil(source_bits.size(), chunk_size)) { assert(source_bits.size() == target_bits.size()); packed_source.allocate(pb, num_chunks, FMT(annotation_prefix, " packed_source")); pack_source.reset(new multipacking_gadget(pb, source_bits, packed_source, chunk_size, FMT(annotation_prefix, " pack_source"))); packed_target.allocate(pb, num_chunks, FMT(annotation_prefix, " packed_target")); pack_target.reset(new multipacking_gadget(pb, target_bits, packed_target, chunk_size, FMT(annotation_prefix, " pack_target"))); copier.reset(new field_vector_copy_gadget(pb, packed_source, packed_target, do_copy, FMT(annotation_prefix, " copier"))); } template void bit_vector_copy_gadget::generate_r1cs_constraints(const bool enforce_source_bitness, const bool enforce_target_bitness) { pack_source->generate_r1cs_constraints(enforce_source_bitness); pack_target->generate_r1cs_constraints(enforce_target_bitness); copier->generate_r1cs_constraints(); } template void bit_vector_copy_gadget::generate_r1cs_witness() { do_copy.evaluate(this->pb); assert(this->pb.lc_val(do_copy) == FieldT::zero() || this->pb.lc_val(do_copy) == FieldT::one()); if (this->pb.lc_val(do_copy) == FieldT::one()) { for (size_t i = 0; i < source_bits.size(); ++i) { this->pb.val(target_bits[i]) = this->pb.val(source_bits[i]); } } pack_source->generate_r1cs_witness_from_bits(); pack_target->generate_r1cs_witness_from_bits(); } template void dual_variable_gadget::generate_r1cs_constraints(const bool enforce_bitness) { consistency_check->generate_r1cs_constraints(enforce_bitness); } template void dual_variable_gadget::generate_r1cs_witness_from_packed() { consistency_check->generate_r1cs_witness_from_packed(); } template void dual_variable_gadget::generate_r1cs_witness_from_bits() { consistency_check->generate_r1cs_witness_from_bits(); } template void disjunction_gadget::generate_r1cs_constraints() { /* inv * sum = output */ linear_combination a1, b1, c1; a1.add_term(inv); for (size_t i = 0; i < inputs.size(); ++i) { b1.add_term(inputs[i]); } c1.add_term(output); this->pb.add_r1cs_constraint(r1cs_constraint(a1, b1, c1), FMT(this->annotation_prefix, " inv*sum=output")); /* (1-output) * sum = 0 */ linear_combination a2, b2, c2; a2.add_term(ONE); a2.add_term(output, -1); for (size_t i = 0; i < inputs.size(); ++i) { b2.add_term(inputs[i]); } c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint(a2, b2, c2), FMT(this->annotation_prefix, " (1-output)*sum=0")); } template void disjunction_gadget::generate_r1cs_witness() { FieldT sum = FieldT::zero(); for (size_t i = 0; i < inputs.size(); ++i) { sum += this->pb.val(inputs[i]); } if (sum.is_zero()) { this->pb.val(inv) = FieldT::zero(); this->pb.val(output) = FieldT::zero(); } else { this->pb.val(inv) = sum.inverse(); this->pb.val(output) = FieldT::one(); } } template void test_disjunction_gadget(const size_t n) { printf("testing disjunction_gadget on all %zu bit strings\n", n); protoboard pb; pb_variable_array inputs; inputs.allocate(pb, n, "inputs"); pb_variable output; output.allocate(pb, "output"); disjunction_gadget d(pb, inputs, output, "d"); d.generate_r1cs_constraints(); for (size_t w = 0; w < 1ul< void conjunction_gadget::generate_r1cs_constraints() { /* inv * (n-sum) = 1-output */ linear_combination a1, b1, c1; a1.add_term(inv); b1.add_term(ONE, inputs.size()); for (size_t i = 0; i < inputs.size(); ++i) { b1.add_term(inputs[i], -1); } c1.add_term(ONE); c1.add_term(output, -1); this->pb.add_r1cs_constraint(r1cs_constraint(a1, b1, c1), FMT(this->annotation_prefix, " inv*(n-sum)=(1-output)")); /* output * (n-sum) = 0 */ linear_combination a2, b2, c2; a2.add_term(output); b2.add_term(ONE, inputs.size()); for (size_t i = 0; i < inputs.size(); ++i) { b2.add_term(inputs[i], -1); } c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint(a2, b2, c2), FMT(this->annotation_prefix, " output*(n-sum)=0")); } template void conjunction_gadget::generate_r1cs_witness() { FieldT sum = FieldT(inputs.size()); for (size_t i = 0; i < inputs.size(); ++i) { sum -= this->pb.val(inputs[i]); } if (sum.is_zero()) { this->pb.val(inv) = FieldT::zero(); this->pb.val(output) = FieldT::one(); } else { this->pb.val(inv) = sum.inverse(); this->pb.val(output) = FieldT::zero(); } } template void test_conjunction_gadget(const size_t n) { printf("testing conjunction_gadget on all %zu bit strings\n", n); protoboard pb; pb_variable_array inputs; inputs.allocate(pb, n, "inputs"); pb_variable output; output.allocate(pb, "output"); conjunction_gadget c(pb, inputs, output, "c"); c.generate_r1cs_constraints(); for (size_t w = 0; w < 1ul< void comparison_gadget::generate_r1cs_constraints() { /* packed(alpha) = 2^n + B - A not_all_zeros = \bigvee_{i=0}^{n-1} alpha_i if B - A > 0, then 2^n + B - A > 2^n, so alpha_n = 1 and not_all_zeros = 1 if B - A = 0, then 2^n + B - A = 2^n, so alpha_n = 1 and not_all_zeros = 0 if B - A < 0, then 2^n + B - A \in {0, 1, \ldots, 2^n-1}, so alpha_n = 0 therefore alpha_n = less_or_eq and alpha_n * not_all_zeros = less */ /* not_all_zeros to be Boolean, alpha_i are Boolean by packing gadget */ generate_boolean_r1cs_constraint(this->pb, not_all_zeros, FMT(this->annotation_prefix, " not_all_zeros")); /* constraints for packed(alpha) = 2^n + B - A */ pack_alpha->generate_r1cs_constraints(true); this->pb.add_r1cs_constraint(r1cs_constraint(1, (FieldT(2)^n) + B - A, alpha_packed), FMT(this->annotation_prefix, " main_constraint")); /* compute result */ all_zeros_test->generate_r1cs_constraints(); this->pb.add_r1cs_constraint(r1cs_constraint(less_or_eq, not_all_zeros, less), FMT(this->annotation_prefix, " less")); } template void comparison_gadget::generate_r1cs_witness() { A.evaluate(this->pb); B.evaluate(this->pb); /* unpack 2^n + B - A into alpha_packed */ this->pb.val(alpha_packed) = (FieldT(2)^n) + this->pb.lc_val(B) - this->pb.lc_val(A); pack_alpha->generate_r1cs_witness_from_packed(); /* compute result */ all_zeros_test->generate_r1cs_witness(); this->pb.val(less) = this->pb.val(less_or_eq) * this->pb.val(not_all_zeros); } template void test_comparison_gadget(const size_t n) { printf("testing comparison_gadget on all %zu bit inputs\n", n); protoboard pb; pb_variable A, B, less, less_or_eq; A.allocate(pb, "A"); B.allocate(pb, "B"); less.allocate(pb, "less"); less_or_eq.allocate(pb, "less_or_eq"); comparison_gadget cmp(pb, n, A, B, less, less_or_eq, "cmp"); cmp.generate_r1cs_constraints(); for (size_t a = 0; a < 1ul< void inner_product_gadget::generate_r1cs_constraints() { /* S_i = \sum_{k=0}^{i+1} A[i] * B[i] S[0] = A[0] * B[0] S[i+1] - S[i] = A[i] * B[i] */ for (size_t i = 0; i < A.size(); ++i) { this->pb.add_r1cs_constraint( r1cs_constraint(A[i], B[i], (i == A.size()-1 ? result : S[i]) + (i == 0 ? 0 * ONE : -S[i-1])), FMT(this->annotation_prefix, " S_%zu", i)); } } template void inner_product_gadget::generate_r1cs_witness() { FieldT total = FieldT::zero(); for (size_t i = 0; i < A.size(); ++i) { A[i].evaluate(this->pb); B[i].evaluate(this->pb); total += this->pb.lc_val(A[i]) * this->pb.lc_val(B[i]); this->pb.val(i == A.size()-1 ? result : S[i]) = total; } } template void test_inner_product_gadget(const size_t n) { printf("testing inner_product_gadget on all %zu bit strings\n", n); protoboard pb; pb_variable_array A; A.allocate(pb, n, "A"); pb_variable_array B; B.allocate(pb, n, "B"); pb_variable result; result.allocate(pb, "result"); inner_product_gadget g(pb, A, B, result, "g"); g.generate_r1cs_constraints(); for (size_t i = 0; i < 1ul< void loose_multiplexing_gadget::generate_r1cs_constraints() { /* \alpha_i (index - i) = 0 */ for (size_t i = 0; i < arr.size(); ++i) { this->pb.add_r1cs_constraint( r1cs_constraint(alpha[i], index - i, 0), FMT(this->annotation_prefix, " alpha_%zu", i)); } /* 1 * (\sum \alpha_i) = success_flag */ linear_combination a, b, c; a.add_term(ONE); for (size_t i = 0; i < arr.size(); ++i) { b.add_term(alpha[i]); } c.add_term(success_flag); this->pb.add_r1cs_constraint(r1cs_constraint(a, b, c), FMT(this->annotation_prefix, " main_constraint")); /* now success_flag is constrained to either 0 (if index is out of range) or \alpha_i. constrain it and \alpha_i to zero */ generate_boolean_r1cs_constraint(this->pb, success_flag, FMT(this->annotation_prefix, " success_flag")); /* compute result */ compute_result->generate_r1cs_constraints(); } template void loose_multiplexing_gadget::generate_r1cs_witness() { /* assumes that idx can be fit in ulong; true for our purposes for now */ const bigint valint = this->pb.val(index).as_bigint(); unsigned long idx = valint.as_ulong(); const bigint arrsize(arr.size()); if (idx >= arr.size() || mpn_cmp(valint.data, arrsize.data, FieldT::num_limbs) >= 0) { for (size_t i = 0; i < arr.size(); ++i) { this->pb.val(alpha[i]) = FieldT::zero(); } this->pb.val(success_flag) = FieldT::zero(); } else { for (size_t i = 0; i < arr.size(); ++i) { this->pb.val(alpha[i]) = (i == idx ? FieldT::one() : FieldT::zero()); } this->pb.val(success_flag) = FieldT::one(); } compute_result->generate_r1cs_witness(); } template void test_loose_multiplexing_gadget(const size_t n) { printf("testing loose_multiplexing_gadget on 2**%zu pb_variable array inputs\n", n); protoboard pb; pb_variable_array arr; arr.allocate(pb, 1ul< index, result, success_flag; index.allocate(pb, "index"); result.allocate(pb, "result"); success_flag.allocate(pb, "success_flag"); loose_multiplexing_gadget g(pb, arr, index, result, success_flag, "g"); g.generate_r1cs_constraints(); for (size_t i = 0; i < 1ul< void create_linear_combination_constraints(protoboard &pb, const std::vector &base, const std::vector > &v, const VarT &target, const std::string &annotation_prefix) { for (size_t i = 0; i < base.size(); ++i) { linear_combination a, b, c; a.add_term(ONE); b.add_term(ONE, base[i]); for (auto &p : v) { b.add_term(p.first.all_vars[i], p.second); } c.add_term(target.all_vars[i]); pb.add_r1cs_constraint(r1cs_constraint(a, b, c), FMT(annotation_prefix, " linear_combination_%zu", i)); } } template void create_linear_combination_witness(protoboard &pb, const std::vector &base, const std::vector > &v, const VarT &target) { for (size_t i = 0; i < base.size(); ++i) { pb.val(target.all_vars[i]) = base[i]; for (auto &p : v) { pb.val(target.all_vars[i]) += p.second * pb.val(p.first.all_vars[i]); } } } } // libsnark #endif // BASIC_GADGETS_TCC_