#include "libsnark_headers.hpp" using namespace libsnark; // There are two types of values: // _constants_ are values known at circuit generation time; they // are global constants known to everyone // _variables_ are values that change in each use of the circuit; // they have two subtypes: // // _public variables_ are values known to both the prover // and verifier but change in each use of the circuit // _private variables_ are values known only to the prover // and change in each use of the circuit // Double a constant EC point (inx,iny) to yield (outx,outy). The input // point must not be the point at infinity. template static void ec_double_point(FieldT &outx, FieldT &outy, const FieldT &inx, const FieldT &iny) { FieldT xsq = inx.squared(); FieldT lambda = (xsq * 3 - 3) * (iny * 2).inverse(); outx = lambda.squared() - inx * 2; outy = lambda * (inx - outx) - iny; } // Add constant EC points (inx, iny) and (addx, addy) to yield (outx, outy). // inx and addx must not be equal. template static void ec_add_points(FieldT &outx, FieldT &outy, const FieldT &inx, const FieldT &iny, const FieldT &addx, const FieldT &addy) { FieldT lambda = (addy - iny) * (addx - inx).inverse(); outx = lambda.squared() - (addx + inx); outy = lambda * (inx - outx) - iny; } // Double the variable EC point (inx,iny) to yield (outx,outy). The // input point must not be the point at infinity. template class ec_double_gadget : public gadget { private: pb_variable lambda, inxsq; public: const pb_variable outx, outy, inx, iny; ec_double_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny) : gadget(pb, "ec_double_gadget"), outx(outx), outy(outy), inx(inx), iny(iny) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes lambda.allocate(this->pb, "lambda"); inxsq.allocate(this->pb, "inxsq"); } void generate_r1cs_constraints() { // inxsq = inx * inx this->pb.add_r1cs_constraint(r1cs_constraint(inx, inx, inxsq)); // 2 * iny * lambda = 3 * inxsq - 3 (a = -3 on our curve) this->pb.add_r1cs_constraint(r1cs_constraint(2 * iny, lambda, 3 * inxsq - 3)); // outx = lambda^2 - 2 * inx this->pb.add_r1cs_constraint(r1cs_constraint(lambda, lambda, outx + 2 * inx)); // outy = lambda * (inx - outx) - iny this->pb.add_r1cs_constraint(r1cs_constraint(lambda, inx - outx, outy + iny)); } void generate_r1cs_witness() { this->pb.val(inxsq) = this->pb.lc_val(inx) * this->pb.lc_val(inx); this->pb.val(lambda) = (this->pb.val(inxsq) * 3 - 3) * (this->pb.lc_val(iny) * 2).inverse(); this->pb.val(outx) = this->pb.val(lambda).squared() - this->pb.lc_val(inx) * 2; this->pb.val(outy) = this->pb.val(lambda) * (this->pb.lc_val(inx) - this->pb.val(outx)) - this->pb.lc_val(iny); } }; // Add the variable EC point (addx,addy) to the variable EC point // (inx,iny) to yield (outx,outy). The input point must not be the // point at infinity. template class ec_add_gadget : public gadget { private: pb_variable lambda; public: const pb_variable outx, outy; const pb_linear_combination inx, iny, addx, addy; ec_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const pb_linear_combination &addx, const pb_linear_combination &addy) : gadget(pb, "ec_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), addx(addx), addy(addy) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes lambda.allocate(this->pb, "lambda"); } void generate_r1cs_constraints() { // (addx - inx) * lambda = addy - iny this->pb.add_r1cs_constraint(r1cs_constraint(addx - inx, lambda, addy - iny)); // outx = lambda^2 - (addx + inx) this->pb.add_r1cs_constraint(r1cs_constraint(lambda, lambda, outx + addx + inx)); // outy = lambda * (inx - outx) - iny this->pb.add_r1cs_constraint(r1cs_constraint(lambda, inx - outx, outy + iny)); } void generate_r1cs_witness() { this->pb.val(lambda) = (this->pb.lc_val(addy) - this->pb.lc_val(iny)) * (this->pb.lc_val(addx) - this->pb.lc_val(inx)).inverse(); this->pb.val(outx) = this->pb.val(lambda).squared() - (this->pb.lc_val(addx) + this->pb.lc_val(inx)); this->pb.val(outy) = this->pb.val(lambda) * (this->pb.lc_val(inx) - this->pb.val(outx)) - this->pb.lc_val(iny); } }; // Add the variable EC point P to the constant EC point (inx,iny) to // yield (outx,outy). The input point must not be the point at // infinity. template class ec_constant_add_gadget : public gadget { private: pb_variable lambda; public: const pb_variable outx, outy; const pb_linear_combination inx, iny; const FieldT Px, Py; ec_constant_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const FieldT &Px, const FieldT &Py) : gadget(pb, "ec_constant_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), Px(Px), Py(Py) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes lambda.allocate(this->pb, "lambda"); } void generate_r1cs_constraints() { // (Px - inx) * lambda = Py - iny this->pb.add_r1cs_constraint(r1cs_constraint(Px - inx, lambda, Py - iny)); // outx = lambda^2 - (Px + inx) this->pb.add_r1cs_constraint(r1cs_constraint(lambda, lambda, outx + Px + inx)); // outy = lambda * (inx - outx) - iny this->pb.add_r1cs_constraint(r1cs_constraint(lambda, inx - outx, outy + iny)); } void generate_r1cs_witness() { this->pb.val(lambda) = (Py - this->pb.lc_val(iny)) * (Px - this->pb.lc_val(inx)).inverse(); this->pb.val(outx) = this->pb.val(lambda).squared() - (Px + this->pb.lc_val(inx)); this->pb.val(outy) = this->pb.val(lambda) * (this->pb.lc_val(inx) - this->pb.val(outx)) - this->pb.lc_val(iny); } }; // Add the constant EC point P0 or the constant EC point P1 to the // variable EC point (inx,iny) to yield (outx,outy). The input point // must not be the point at infinity. The input bit choice controls // which addition is done. template class ec_2_constant_add_gadget : public gadget { private: pb_linear_combination addx, addy; std::vector > adder; public: const pb_variable outx, outy; const pb_linear_combination inx, iny; const pb_variable choice; const FieldT P0x, P0y, P1x, P1y; ec_2_constant_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const pb_variable &choice, const FieldT &P0x, const FieldT &P0y, const FieldT &P1x, const FieldT &P1y) : gadget(pb, "ec_2_constant_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), choice(choice), P0x(P0x), P0y(P0y), P1x(P1x), P1y(P1y) { // Allocate variables to protoboard addx.assign(pb, choice * (P1x-P0x) + P0x); addy.assign(pb, choice * (P1y-P0y) + P0y); adder.emplace_back(this->pb, outx, outy, inx, iny, addx, addy); } void generate_r1cs_constraints() { adder[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { addx.evaluate(this->pb); addy.evaluate(this->pb); adder[0].generate_r1cs_witness(); } }; // Add the constant EC point P0 or the variable EC point P1 to the // variable EC point (inx,iny) to yield (outx,outy). The input point // must not be the point at infinity. The input bit choice controls // which addition is done. template class ec_2_1constant_add_gadget : public gadget { private: pb_variable addx, addy; std::vector > adder; public: const pb_variable outx, outy; const pb_linear_combination inx, iny; const pb_variable choice; const FieldT P0x, P0y; const pb_variable P1x, P1y; ec_2_1constant_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const pb_variable &choice, const FieldT &P0x, const FieldT &P0y, const pb_variable &P1x, const pb_variable &P1y) : gadget(pb, "ec_2_1constant_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), choice(choice), P0x(P0x), P0y(P0y), P1x(P1x), P1y(P1y) { // Allocate variables to protoboard addx.allocate(this->pb, "addx"); addy.allocate(this->pb, "addy"); adder.emplace_back(this->pb, outx, outy, inx, iny, addx, addy); } void generate_r1cs_constraints() { // Set (addx,addy) = choice ? (P0x, P0y) : (P1x, P1y) this->pb.add_r1cs_constraint(r1cs_constraint(P1x - P0x, choice, addx - P0x)); this->pb.add_r1cs_constraint(r1cs_constraint(P1y - P0y, choice, addy - P0y)); adder[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { bool choiceb = this->pb.val(choice) != FieldT(0); this->pb.val(addx) = choiceb ? this->pb.val(P1x) : P0x; this->pb.val(addy) = choiceb ? this->pb.val(P1y) : P0y; adder[0].generate_r1cs_witness(); } }; // Add the variable EC point P0 or the variable EC point P1 to the // variable EC point (inx,iny) to yield (outx,outy). The input point // must not be the point at infinity. The input bit choice controls // which addition is done. template class ec_2_add_gadget : public gadget { private: pb_variable addx, addy; std::vector > adder; public: const pb_variable outx, outy; const pb_linear_combination inx, iny; const pb_variable choice; const pb_variable P0x, P0y, P1x, P1y; ec_2_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const pb_variable &choice, const pb_variable &P0x, const pb_variable &P0y, const pb_variable &P1x, const pb_variable &P1y) : gadget(pb, "ec_2_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), choice(choice), P0x(P0x), P0y(P0y), P1x(P1x), P1y(P1y) { // Allocate variables to protoboard addx.allocate(this->pb, "addx"); addy.allocate(this->pb, "addy"); adder.emplace_back(this->pb, outx, outy, inx, iny, addx, addy); } void generate_r1cs_constraints() { // Set (addx,addy) = choice ? (P0x, P0y) : (P1x, P1y) this->pb.add_r1cs_constraint(r1cs_constraint(P1x - P0x, choice, addx - P0x)); this->pb.add_r1cs_constraint(r1cs_constraint(P1y - P0y, choice, addy - P0y)); adder[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { bool choiceb = this->pb.val(choice) != FieldT(0); this->pb.val(addx) = choiceb ? this->pb.val(P1x) : this->pb.val(P0x); this->pb.val(addy) = choiceb ? this->pb.val(P1y) : this->pb.val(P0y); adder[0].generate_r1cs_witness(); } }; // Add one of the four constant EC points to the variable EC point // (inx,iny) to yield (outx,outy). The input point must not be the // point at infinity. The input bits choice0 and choice1 control which // addition is done (P{2*choice1+choice0} is added). template class ec_4_constant_add_gadget : public gadget { private: pb_variable both; pb_linear_combination addx, addy; std::vector > adder; public: const pb_variable outx, outy; const pb_linear_combination inx, iny; const pb_variable choice0, choice1; const FieldT P0x, P0y, P1x, P1y, P2x, P2y, P3x, P3y; ec_4_constant_add_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_linear_combination &inx, const pb_linear_combination &iny, const pb_variable &choice0, const pb_variable &choice1, const FieldT &P0x, const FieldT &P0y, const FieldT &P1x, const FieldT &P1y, const FieldT &P2x, const FieldT &P2y, const FieldT &P3x, const FieldT &P3y) : gadget(pb, "ec_4_constant_add_gadget"), outx(outx), outy(outy), inx(inx), iny(iny), choice0(choice0), choice1(choice1), P0x(P0x), P0y(P0y), P1x(P1x), P1y(P1y), P2x(P2x), P2y(P2y), P3x(P3x), P3y(P3y) { // Allocate variables to protoboard both.allocate(this->pb, "both"); addx.assign(this->pb, both * (P3x - P2x - P1x + P0x) + choice1 * (P2x - P0x) + choice0 * (P1x - P0x) + P0x); addy.assign(this->pb, both * (P3y - P2y - P1y + P0y) + choice1 * (P2y - P0y) + choice0 * (P1y - P0y) + P0y); adder.emplace_back(this->pb, outx, outy, inx, iny, addx, addy); } void generate_r1cs_constraints() { this->pb.add_r1cs_constraint(r1cs_constraint(choice0, choice1, both)); adder[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { bool c0 = this->pb.val(choice0) != FieldT(0); bool c1 = this->pb.val(choice1) != FieldT(0); this->pb.val(both) = c0 && c1; addx.evaluate(this->pb); addy.evaluate(this->pb); adder[0].generate_r1cs_witness(); } }; // Compute A + s*P as (outx, outy) for an accumulator A, a given // constant point P, and s given as a bit vector. The _caller_ is // responsible for proving that the elements of svec are bits. The // (constant) accumulator excess (AXS) will be updated; when all the // computations are complete, AXS should be subtracted from the // accumulator A. template class ec_constant_scalarmul_vec_accum_gadget : public gadget { private: FieldT Cx, Cy; pb_variable_array accumx, accumy; std::vector > fouradders; std::vector > twoadders; public: const pb_variable outx, outy; const pb_variable Ax, Ay; const pb_variable_array svec; const FieldT Px, Py; // Strategy: We compute (as compile-time constants) (powers of 2) // times P. Based on each bit of s, we add one of the constant points // C or (2^i * P) + C to the accumulator, and regardless of s, add C // to the excess. ec_constant_scalarmul_vec_accum_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &Ax, const pb_variable &Ay, const pb_variable_array &svec, const FieldT &Px, const FieldT &Py, FieldT &AXSx, FieldT &AXSy) : gadget(pb, "ec_constant_scalarmul_vec_accum_gadget"), // Precomputed coordinates of C Cx(2), Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"), outx(outx), outy(outy), Ax(Ax), Ay(Ay), svec(svec), Px(Px), Py(Py) { size_t numbits = svec.size(); // See loop comments below: if numbits is odd, we need (numbits-1)/2 // slots. If numbits is even, we need (numbits-2)/2 slots. So // with integer truncated division, (numbits-1)/2 will be correct // in both cases. (Well, if numbits is 0 for some reason, we also want // to get 0.) size_t accumslots = 0; if (numbits > 0) { accumslots = (numbits-1)/2; } accumx.allocate(this->pb, accumslots, "accumx"); accumy.allocate(this->pb, accumslots, "accumy"); FieldT twoiPx = Px, twoiPy = Py; size_t i = 0, accnext = 0; while(i < numbits) { // Invariant: twoiP = 2^i * P // Invariant: i is even and accnext = i/2 if (i == numbits-1) { FieldT twoiPCx, twoiPCy; ec_add_points(twoiPCx, twoiPCy, twoiPx, twoiPy, Cx, Cy); twoadders.emplace_back(this->pb, outx, outy, (i == 0 ? Ax : accumx[accnext-1]), (i == 0 ? Ay : accumy[accnext-1]), svec[i], Cx, Cy, twoiPCx, twoiPCy); // This makes i odd, but also exits the loop with // i = numbits and accnext = (numbits-1)/2 i += 1; } else { // Do two bits at a time // We need to compute 2^i * a * P + C for a = 1,2,3 FieldT twoi2Px, twoi2Py; FieldT twoi1PCx, twoi1PCy, twoi2PCx, twoi2PCy, twoi3PCx, twoi3PCy; ec_add_points(twoi1PCx, twoi1PCy, twoiPx, twoiPy, Cx, Cy); ec_double_point(twoi2Px, twoi2Py, twoiPx, twoiPy); ec_add_points(twoi2PCx, twoi2PCy, twoi2Px, twoi2Py, Cx, Cy); ec_add_points(twoi3PCx, twoi3PCy, twoi2Px, twoi2Py, twoi1PCx, twoi1PCy); fouradders.emplace_back(this->pb, (i == numbits-2 ? outx : accumx[accnext]), (i == numbits-2 ? outy : accumy[accnext]), (i == 0 ? Ax : accumx[accnext-1]), (i == 0 ? Ay : accumy[accnext-1]), svec[i], svec[i+1], Cx, Cy, twoi1PCx, twoi1PCy, twoi2PCx, twoi2PCy, twoi3PCx, twoi3PCy); // If i == numbits-2, we write directly to out and not accum above, and // exit the loop with i even and i == numbits and accnext = (numbits-2)/2 if (i < numbits - 2) { accnext += 1; } i += 2; ec_double_point(twoiPx, twoiPy, twoi2Px, twoi2Py); } FieldT newAXSx, newAXSy; ec_add_points(newAXSx, newAXSy, AXSx, AXSy, Cx, Cy); AXSx = newAXSx; AXSy = newAXSy; } } void generate_r1cs_constraints() { for (auto&& gadget : fouradders) { gadget.generate_r1cs_constraints(); } for (auto&& gadget : twoadders) { gadget.generate_r1cs_constraints(); } } void generate_r1cs_witness() { for (auto&& gadget : fouradders) { gadget.generate_r1cs_witness(); } for (auto&& gadget : twoadders) { gadget.generate_r1cs_witness(); } } }; // Compute A + s*P as (outx, outy) for an accumulator A, a given // constant point P, and s given as a field element. The (constant) // accumulator excess (AXS) will be updated; when all the computations // are complete, AXS should be subtracted from the accumulator A. template class ec_constant_scalarmul_accum_gadget : public gadget { private: pb_variable_array svec; std::vector > packers; std::vector > vecgadget; public: const pb_variable outx, outy; const pb_variable Ax, Ay; const pb_variable s; const FieldT Px, Py; ec_constant_scalarmul_accum_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &Ax, const pb_variable &Ay, const pb_variable &s, const FieldT &Px, const FieldT &Py, FieldT &AXSx, FieldT &AXSy) : gadget(pb, "ec_constant_scalarmul_accum_gadget"), outx(outx), outy(outy), Ax(Ax), Ay(Ay), s(s), Px(Px), Py(Py) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes size_t numbits = FieldT::num_bits; svec.allocate(this->pb, numbits, "svec"); packers.emplace_back(this->pb, svec, s); vecgadget.emplace_back(this->pb, outx, outy, Ax, Ay, svec, Px, Py, AXSx, AXSy); } void generate_r1cs_constraints() { packers[0].generate_r1cs_constraints(true); vecgadget[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { packers[0].generate_r1cs_witness_from_packed(); vecgadget[0].generate_r1cs_witness(); } }; // Compute s*P as (outx, outy) for a given constant point P, and s given // as a bit vector. The _caller_ is responsible for proving that the // elements of svec are bits. template class ec_constant_scalarmul_vec_gadget : public gadget { private: FieldT Cx, Cy, Ax, Ay, AXSx, AXSy; pb_variable accinx, acciny, accoutx, accouty; std::vector > scalarmuls; std::vector > adders; public: const pb_variable outx, outy; const pb_variable_array svec; const FieldT Px, Py; ec_constant_scalarmul_vec_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable_array &svec, const FieldT &Px, const FieldT &Py) : gadget(pb, "ec_constant_scalarmul_vec_gadget"), // Precomputed coordinates of C and A Cx(2), Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"), Ax("7536839002660211356286040193441766649532044555061394833845553337792579131020"), Ay("11391058648720923807988142436733355540810929560298907319389650598553246451302"), outx(outx), outy(outy), svec(svec), Px(Px), Py(Py) { AXSx = Ax; AXSy = Ay; accinx.allocate(this->pb, "accinx"); acciny.allocate(this->pb, "acciny"); accoutx.allocate(this->pb, "accoutx"); accouty.allocate(this->pb, "accouty"); scalarmuls.emplace_back(pb, accoutx, accouty, accinx, acciny, svec, Px, Py, AXSx, AXSy); adders.emplace_back(pb, outx, outy, accoutx, accouty, AXSx, -AXSy); } void generate_r1cs_constraints() { this->pb.add_r1cs_constraint(r1cs_constraint(accinx, 1, Ax)); this->pb.add_r1cs_constraint(r1cs_constraint(acciny, 1, Ay)); scalarmuls[0].generate_r1cs_constraints(); adders[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { this->pb.val(accinx) = Ax; this->pb.val(acciny) = Ay; scalarmuls[0].generate_r1cs_witness(); adders[0].generate_r1cs_witness(); } }; // Compute s*P as (outx, outy) for a given constant point P, and s given // as a field element. template class ec_constant_scalarmul_gadget : public gadget { private: pb_variable_array svec; std::vector > packers; std::vector > vecgadget; public: const pb_variable outx, outy; const pb_variable s; const FieldT Px, Py; ec_constant_scalarmul_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &s, const FieldT &Px, const FieldT &Py) : gadget(pb, "ec_constant_scalarmul_gadget"), outx(outx), outy(outy), s(s), Px(Px), Py(Py) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes size_t numbits = FieldT::num_bits; svec.allocate(this->pb, numbits, "svec"); packers.emplace_back(this->pb, svec, s); vecgadget.emplace_back(this->pb, outx, outy, svec, Px, Py); } void generate_r1cs_constraints() { packers[0].generate_r1cs_constraints(true); vecgadget[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { packers[0].generate_r1cs_witness_from_packed(); vecgadget[0].generate_r1cs_witness(); } }; template class ec_scalarmul_gadget; // Compute A + s*P as (outx, outy) for an accumulator A, a precomputed // addition table Ptable for a variable point P, and s given as a bit // vector. The _caller_ is responsible for proving that the elements of // svec are bits. The (constant) accumulator excess (AXS) will be // updated; when all the computations are complete, AXS should be // subtracted from the accumulator A. The addition table is a variable // array of length 2*numbits (where numbits is the length of svec) such // that Ptable[2*i] and Ptable[2*i+1] are the (x,y) coordinates of // 2^i * P + C. Set Ptable_set_constraints to true (exactly once // in the event the same Ptable is reused in the same circuit) if // the Ptable is part of the private input. Set Ptable_fill_values // to true exactly once per Ptable (again, in case it it reused in the // same circuit). template class ec_scalarmul_vec_accum_gadget : public gadget { private: FieldT Cx, Cy; pb_variable_array accumx, accumy; pb_variable_array twoiPx, twoiPy; std::vector > cadders; std::vector > adders; std::vector > twoadders; public: const pb_variable outx, outy; const pb_variable Ax, Ay; const pb_variable_array svec; const pb_variable Px, Py; const pb_variable_array Ptable; bool Ptable_set_constraints, Ptable_fill_values; ec_scalarmul_vec_accum_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &Ax, const pb_variable &Ay, const pb_variable_array &svec, const pb_variable &Px, const pb_variable &Py, const pb_variable_array &Ptable, bool Ptable_set_constraints, bool Ptable_fill_values, FieldT &AXSx, FieldT &AXSy) : gadget(pb, "ec_scalarmul_vec_accum_gadget"), // Precomputed coordinates of C Cx(2), Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"), outx(outx), outy(outy), Ax(Ax), Ay(Ay), svec(svec), Px(Px), Py(Py), Ptable(Ptable), Ptable_set_constraints(Ptable_set_constraints), Ptable_fill_values(Ptable_fill_values) { size_t numbits = svec.size(); assert(Ptable.size() == 2*numbits); if (Ptable_set_constraints) { // Create the adders to fill the Ptable with the correct values. // Ptable[2*i] and Ptable[2*i+1] are the (x,y) coordinates of // 2^i * P + C. if (numbits > 0) { // Add P and C to get Ptable[0,1] = P+C cadders.emplace_back(this->pb, Ptable[0], Ptable[1], Px, Py, Cx, Cy); } if (numbits > 1) { // Add P and P+C to get Ptable[2,3] = 2*P+C adders.emplace_back(this->pb, Ptable[2], Ptable[3], Px, Py, Ptable[0], Ptable[1]); } if (numbits > 2) { twoiPx.allocate(this->pb, numbits-2, "twoiPx"); twoiPy.allocate(this->pb, numbits-2, "twoiPy"); } for (size_t i = 2; i < numbits; ++i) { // Invariant: twoiP[i] = 2^{i+1} * P // Compute 2^{i-1}*P = (2^{i-1}*P + C) - C cadders.emplace_back(this->pb, twoiPx[i-2], twoiPy[i-2], Ptable[2*(i-1)], Ptable[2*(i-1)+1], Cx, -Cy); // Compute 2^{i}*P + C = (2^{i-1}*P + C) + (2^{i-1}*P) adders.emplace_back(this->pb, Ptable[2*i], Ptable[2*i+1], Ptable[2*i-2], Ptable[2*i-1], twoiPx[i-2], twoiPy[i-2]); } } accumx.allocate(this->pb, numbits-1, "accumx"); accumy.allocate(this->pb, numbits-1, "accumy"); for (size_t i = 0; i < numbits; ++i) { twoadders.emplace_back(this->pb, (i == numbits-1 ? outx : accumx[i]), (i == numbits-1 ? outy : accumy[i]), (i == 0 ? Ax : accumx[i-1]), (i == 0 ? Ay : accumy[i-1]), svec[i], Cx, Cy, Ptable[2*i], Ptable[2*i+1]); FieldT newAXSx, newAXSy; ec_add_points(newAXSx, newAXSy, AXSx, AXSy, Cx, Cy); AXSx = newAXSx; AXSy = newAXSy; } } void generate_r1cs_constraints() { if (Ptable_set_constraints) { for (auto&& gadget : cadders) { gadget.generate_r1cs_constraints(); } for (auto&& gadget : adders) { gadget.generate_r1cs_constraints(); } } for (auto&& gadget : twoadders) { gadget.generate_r1cs_constraints(); } } void generate_r1cs_witness() { if (Ptable_set_constraints) { // We also have to satisfy the constraints we set size_t numbits = Ptable.size() / 2; if (numbits > 0) { cadders[0].generate_r1cs_witness(); } if (numbits > 1) { adders[0].generate_r1cs_witness(); } for (size_t i = 2; i < numbits; ++i) { cadders[i-1].generate_r1cs_witness(); adders[i-1].generate_r1cs_witness(); } } else if (Ptable_fill_values) { // We can just compute the Ptable values manually ec_scalarmul_gadget::compute_Ptable(this->pb, Ptable, Px, Py); } for (auto&& gadget : twoadders) { gadget.generate_r1cs_witness(); } } }; // Compute A + s*P as (outx, outy) for an accumulator A, a precomputed // addition table Ptable for a variable point P, and s given as a field // element. The _caller_ is responsible for proving that the elements // of svec are bits. The (constant) accumulator excess (AXS) will be // updated; when all the computations are complete, AXS should be // subtracted from the accumulator A. The addition table is a variable // array of length 2*numbits (where numbits is the length of the FieldT // size) such that Ptable[2*i] and Ptable[2*i+1] are the (x,y) // coordinates of 2^i * P + C. Set Ptable_set_constraints to true // (exactly once in the event the same Ptable is reused in the same // circuit) if the Ptable is part of the private input. Set // Ptable_fill_values to true exactly once per Ptable (again, in case it // it reused in the same circuit). template class ec_scalarmul_accum_gadget : public gadget { private: pb_variable_array svec; std::vector > packers; std::vector > vecgadget; public: const pb_variable outx, outy; const pb_variable Ax, Ay; const pb_variable s; const pb_variable Px, Py; const pb_variable_array Ptable; bool Ptable_set_constraints, Ptable_fill_values; ec_scalarmul_accum_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &Ax, const pb_variable &Ay, const pb_variable &s, const pb_variable &Px, const pb_variable &Py, const pb_variable_array &Ptable, bool Ptable_set_constraints, bool Ptable_fill_values, FieldT &AXSx, FieldT &AXSy) : gadget(pb, "ec_scalarmul_accum_gadget"), outx(outx), outy(outy), Ax(Ax), Ay(Ay), s(s), Px(Px), Py(Py), Ptable(Ptable), Ptable_set_constraints(Ptable_set_constraints), Ptable_fill_values(Ptable_fill_values) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes size_t numbits = FieldT::num_bits; svec.allocate(this->pb, numbits, "svec"); packers.emplace_back(this->pb, svec, s); vecgadget.emplace_back(this->pb, outx, outy, Ax, Ay, svec, Px, Py, Ptable, Ptable_set_constraints, Ptable_fill_values, AXSx, AXSy); } void generate_r1cs_constraints() { packers[0].generate_r1cs_constraints(true); vecgadget[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { packers[0].generate_r1cs_witness_from_packed(); vecgadget[0].generate_r1cs_witness(); } }; // Compute s*P as (outx, outy) for a precomputed addition table Ptable // for a variable point P, and s given as a bit vector. The _caller_ is // responsible for proving that the elements of svec are bits. // The addition table is a variable array of length 2*numbits (where // numbits is the length of svec) such that Ptable[2*i] and // Ptable[2*i+1] are the (x,y) coordinates of 2^i * P + C. Set // Ptable_set_constraints to true (exactly once in the event the same // Ptable is reused in the same circuit) if the Ptable is part of the // private input. Set Ptable_fill_values to true exactly once per // Ptable (again, in case it it reused in the same circuit). template class ec_scalarmul_vec_gadget : public gadget { private: FieldT Cx, Cy, Ax, Ay, AXSx, AXSy; pb_variable accinx, acciny, accoutx, accouty; std::vector > scalarmuls; std::vector > adders; public: const pb_variable outx, outy; const pb_variable_array svec; const pb_variable Px, Py; const pb_variable_array Ptable; bool Ptable_set_constraints, Ptable_fill_values; ec_scalarmul_vec_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable_array &svec, const pb_variable &Px, const pb_variable &Py, const pb_variable_array &Ptable, bool Ptable_set_constraints, bool Ptable_fill_values) : gadget(pb, "ec_scalarmul_vec_gadget"), // Precomputed coordinates of C and A Cx(2), Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"), Ax("7536839002660211356286040193441766649532044555061394833845553337792579131020"), Ay("11391058648720923807988142436733355540810929560298907319389650598553246451302"), outx(outx), outy(outy), svec(svec), Px(Px), Py(Py), Ptable(Ptable), Ptable_set_constraints(Ptable_set_constraints), Ptable_fill_values(Ptable_fill_values) { AXSx = Ax; AXSy = Ay; accinx.allocate(this->pb, "accinx"); acciny.allocate(this->pb, "acciny"); accoutx.allocate(this->pb, "accoutx"); accouty.allocate(this->pb, "accouty"); scalarmuls.emplace_back(pb, accoutx, accouty, accinx, acciny, svec, Px, Py, Ptable, Ptable_set_constraints, Ptable_fill_values, AXSx, AXSy); adders.emplace_back(pb, outx, outy, accoutx, accouty, AXSx, -AXSy); } void generate_r1cs_constraints() { this->pb.add_r1cs_constraint(r1cs_constraint(accinx, 1, Ax)); this->pb.add_r1cs_constraint(r1cs_constraint(acciny, 1, Ay)); scalarmuls[0].generate_r1cs_constraints(); adders[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { this->pb.val(accinx) = Ax; this->pb.val(acciny) = Ay; scalarmuls[0].generate_r1cs_witness(); adders[0].generate_r1cs_witness(); } }; // Compute s*P as (outx, outy) for a precomputed addition table Ptable // for a variable point P, and s given as a field element. The addition // table is a variable array of length 2*numbits (where numbits is the // length of the FieldT size) such that Ptable[2*i] and Ptable[2*i+1] // are the (x,y) coordinates of 2^i * P + C. Set Ptable_set_constraints // to true (exactly once in the event the same Ptable is reused in the // same circuit) if the Ptable is part of the private input. Set // Ptable_fill_values to true exactly once per Ptable (again, in case it // it reused in the same circuit). template class ec_scalarmul_gadget : public gadget { private: pb_variable_array svec; std::vector > packers; std::vector > vecgadget; public: const pb_variable outx, outy; const pb_variable s; const pb_variable Px, Py; const pb_variable_array Ptable; bool Ptable_set_constraints, Ptable_fill_values; ec_scalarmul_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &s, const pb_variable &Px, const pb_variable &Py, const pb_variable_array &Ptable, bool Ptable_set_constraints, bool Ptable_fill_values) : gadget(pb, "ec_scalarmul_gadget"), outx(outx), outy(outy), s(s), Px(Px), Py(Py), Ptable(Ptable), Ptable_set_constraints(Ptable_set_constraints), Ptable_fill_values(Ptable_fill_values) { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes size_t numbits = FieldT::num_bits; svec.allocate(this->pb, numbits, "svec"); packers.emplace_back(this->pb, svec, s); vecgadget.emplace_back(this->pb, outx, outy, svec, Px, Py, Ptable, Ptable_set_constraints, Ptable_fill_values); } void generate_r1cs_constraints() { packers[0].generate_r1cs_constraints(true); vecgadget[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { packers[0].generate_r1cs_witness_from_packed(); vecgadget[0].generate_r1cs_witness(); } // Compute the addition table. The addition table is a variable array // of length 2*numbits such that Ptable[2*i] and Ptable[2*i+1] are the // (x,y) coordinates of 2^i * P + C. static void compute_Ptable(protoboard &pb, const pb_variable_array &Ptable, const pb_variable &Px, const pb_variable &Py) { const FieldT Cx(2); const FieldT Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"); assert(Ptable.size() % 2 == 0); size_t numbits = Ptable.size() / 2; FieldT twoiPx = pb.val(Px); FieldT twoiPy = pb.val(Py); for (size_t i = 0; i < numbits; ++i) { // Invariant: (twoiPx, twoiPy) = 2^i * P // Compute 2^i * P + C FieldT twoiPCx, twoiPCy; ec_add_points(twoiPCx, twoiPCy, twoiPx, twoiPy, Cx, Cy); pb.val(Ptable[2*i]) = twoiPCx; pb.val(Ptable[2*i+1]) = twoiPCy; // Compute 2^{i+1} * P FieldT twoi1Px, twoi1Py; ec_double_point(twoi1Px, twoi1Py, twoiPx, twoiPy); twoiPx = twoi1Px; twoiPy = twoi1Py; } } }; // Compute a*G + b*H as (outx, outy), given a and b as field elements. template class ec_pedersen_gadget : public gadget { private: pb_variable accinx, acciny, accmidx, accmidy, accoutx, accouty; std::vector > mulgadgets; std::vector > addgadget; const FieldT Gx, Gy, Hx, Hy, Ax, Ay; public: const pb_variable outx, outy, a, b; ec_pedersen_gadget(protoboard &pb, const pb_variable &outx, const pb_variable &outy, const pb_variable &a, const pb_variable &b) : gadget(pb, "ec_pedersen_gadget"), outx(outx), outy(outy), a(a), b(b), // Precomputed coordinates of G, H, and A Gx(0), Gy("11977228949870389393715360594190192321220966033310912010610740966317727761886"), Hx(1), Hy("21803877843449984883423225223478944275188924769286999517937427649571474907279"), Ax("7536839002660211356286040193441766649532044555061394833845553337792579131020"), Ay("11391058648720923807988142436733355540810929560298907319389650598553246451302") { // Allocate variables to protoboard // The strings (like "x") are only for debugging purposes accinx.allocate(this->pb, "accinx"); acciny.allocate(this->pb, "acciny"); accmidx.allocate(this->pb, "accmidx"); accmidy.allocate(this->pb, "accmidy"); accoutx.allocate(this->pb, "accoutx"); accouty.allocate(this->pb, "accouty"); // Initialize the accumulator FieldT AXSx = Ax; FieldT AXSy = Ay; this->pb.add_r1cs_constraint(r1cs_constraint(accinx, 1, Ax)); this->pb.add_r1cs_constraint(r1cs_constraint(acciny, 1, Ay)); // Initialize the gadgets mulgadgets.emplace_back(this->pb, accmidx, accmidy, accinx, acciny, a, Gx, Gy, AXSx, AXSy); mulgadgets.emplace_back(this->pb, accoutx, accouty, accmidx, accmidy, b, Hx, Hy, AXSx, AXSy); // Subtract the accumulator excess to get the result addgadget.emplace_back(this->pb, outx, outy, accoutx, accouty, AXSx, -AXSy); } void generate_r1cs_constraints() { this->pb.val(accinx) = Ax; this->pb.val(acciny) = Ay; mulgadgets[0].generate_r1cs_constraints(); mulgadgets[1].generate_r1cs_constraints(); addgadget[0].generate_r1cs_constraints(); } void generate_r1cs_witness() { mulgadgets[0].generate_r1cs_witness(); mulgadgets[1].generate_r1cs_witness(); addgadget[0].generate_r1cs_witness(); } };