123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739 |
- #include "libsnark/gadgetlib1/gadgets/basic_gadgets.hpp"
- using namespace libsnark;
- // Double a public EC point (inx,iny) to yield (outx,outy). The input
- // point must not be the point at infinity.
- template<typename FieldT>
- 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 public EC points (inx, iny) and (addx, addy) to yield (outx, outy).
- // inx and addx must not be equal.
- template<typename FieldT>
- 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 EC point (inx,iny) to yield (outx,outy). The input point
- // must not be the point at infinity.
- template<typename FieldT>
- class ec_double_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> lambda, inxsq;
- public:
- const pb_variable<FieldT> outx, outy, inx, iny;
- ec_double_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable<FieldT> &inx,
- const pb_variable<FieldT> &iny) :
- gadget<FieldT>(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<FieldT>(inx, inx, inxsq));
- // 2 * iny * lambda = 3 * inxsq - 3 (a = -3 on our curve)
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(2 * iny, lambda, 3 * inxsq - 3));
- // outx = lambda^2 - 2 * inx
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, lambda, outx + 2 * inx));
- // outy = lambda * (inx - outx) - iny
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, inx - outx, outy + iny));
- }
- void generate_r1cs_witness()
- {
- this->pb.val(inxsq) = this->pb.val(inx) * this->pb.val(inx);
- this->pb.val(lambda) = (this->pb.val(inxsq) * 3 - 3) * (this->pb.val(iny) * 2).inverse();
- this->pb.val(outx) = this->pb.val(lambda).squared() - this->pb.val(inx) * 2;
- this->pb.val(outy) = this->pb.val(lambda) * (this->pb.val(inx) - this->pb.val(outx)) - this->pb.val(iny);
- }
- };
- // Add the EC point (addx,addy) to the EC point (inx,iny) to yield
- // (outx,outy). The input point must not be the point at infinity.
- template<typename FieldT>
- class ec_add_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> lambda;
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_linear_combination<FieldT> inx, iny, addx, addy;
- ec_add_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_linear_combination<FieldT> &inx,
- const pb_linear_combination<FieldT> &iny,
- const pb_linear_combination<FieldT> &addx,
- const pb_linear_combination<FieldT> &addy) :
- gadget<FieldT>(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<FieldT>(addx - inx, lambda, addy - iny));
- // outx = lambda^2 - (addx + inx)
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, lambda, outx + addx + inx));
- // outy = lambda * (inx - outx) - iny
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 public EC point P to the EC point (inx,iny) to yield
- // (outx,outy). The input point must not be the point at infinity.
- template<typename FieldT>
- class ec_public_add_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> lambda;
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_linear_combination<FieldT> inx, iny;
- const FieldT Px, Py;
- ec_public_add_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_linear_combination<FieldT> &inx,
- const pb_linear_combination<FieldT> &iny,
- const FieldT &Px, const FieldT &Py) :
- gadget<FieldT>(pb, "ec_public_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<FieldT>(Px - inx, lambda, Py - iny));
- // outx = lambda^2 - (Px + inx)
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, lambda, outx + Px + inx));
- // outy = lambda * (inx - outx) - iny
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 nothing or the public EC point P to the EC point (inx,iny) to
- // yield (outx,outy). The input point must not be the point at
- // infinity. The input bit do_add controls whether the addition is
- // done.
- template<typename FieldT>
- class ec_conditional_add_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> sumx, sumy;
- std::vector<ec_public_add_gadget<FieldT> > adder;
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_linear_combination<FieldT> inx, iny;
- const pb_variable<FieldT> do_add;
- const FieldT Px, Py;
- ec_conditional_add_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_linear_combination<FieldT> &inx,
- const pb_linear_combination<FieldT> &iny,
- const pb_variable<FieldT> &do_add,
- const FieldT &Px, const FieldT &Py) :
- gadget<FieldT>(pb, "ec_conditional_add_gadget"),
- outx(outx), outy(outy), inx(inx), iny(iny), do_add(do_add),
- Px(Px), Py(Py)
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- sumx.allocate(this->pb, "sumx");
- sumy.allocate(this->pb, "sumy");
- adder.emplace_back(this->pb, sumx, sumy, inx, iny, Px, Py);
- }
- void generate_r1cs_constraints()
- {
- // Strategy: we always do the addition, but if do_add = 0, we throw
- // it away later.
- adder[0].generate_r1cs_constraints();
- // Now we want to conditionally move the sum. We want that
- // outx = do_add ? sumx : inx
- // outy = do_add ? sumy : iny
- // so we compute
- // outx = inx + (sumx - inx) * do_add
- // outy = iny + (sumy - iny) * do_add
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(sumx - inx, do_add, outx - inx));
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(sumy - iny, do_add, outy - iny));
- }
- void generate_r1cs_witness()
- {
- adder[0].generate_r1cs_witness();
- bool move = this->pb.val(do_add) != FieldT(0);
- this->pb.val(outx) = move ? this->pb.val(sumx) : this->pb.lc_val(inx);
- this->pb.val(outy) = move ? this->pb.val(sumy) : this->pb.lc_val(iny);
- }
- };
- // Add nothing, or one of the public EC points P1, P2, or P3 to the EC
- // point (inx,iny) to yield (outx,outy). The input point must not be
- // the point at infinity. The two input bits add1 and add2 control what
- // is added. Typically, P3 will equal P1+P2, in which case this gadget
- // does two conditional adds simultaneously in just 6 constraints.
- template<typename FieldT>
- class ec_add_P123_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> lambda, sumx, sumy, move;
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_linear_combination<FieldT> inx, iny;
- const pb_variable<FieldT> add1, add2;
- const FieldT P1x, P1y, P2x, P2y, P3x, P3y;
- ec_add_P123_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_linear_combination<FieldT> &inx,
- const pb_linear_combination<FieldT> &iny,
- const pb_variable<FieldT> &add1,
- const pb_variable<FieldT> &add2,
- const FieldT &P1x, const FieldT &P1y,
- const FieldT &P2x, const FieldT &P2y,
- const FieldT &P3x, const FieldT &P3y) :
- gadget<FieldT>(pb, "ec_add_P123_gadget"),
- outx(outx), outy(outy), inx(inx), iny(iny), add1(add1), add2(add2),
- P1x(P1x), P1y(P1y), P2x(P2x), P2y(P2y), P3x(P3x), P3y(P3y)
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- lambda.allocate(this->pb, "lambda");
- sumx.allocate(this->pb, "sumx");
- sumy.allocate(this->pb, "sumy");
- move.allocate(this->pb, "move");
- }
- void generate_r1cs_constraints()
- {
- // Strategy: if add1 = add2 = 0, we compute some nonsense but throw
- // it away later. Otherwise, the coordinates of the point to add
- // are a _linear_ function of add1 and add2 (since P1, P2, and P3
- // are public constants)
- // In particular, the point to add is ( (P3x - P2x) * add1 + (P3x -
- // P1x) * add2 + (P1x + P2x - P3x), (P3y - P2y) * add1 + (P3y - P1y) *
- // add2 + (P1y + P2y - P3y))
- // (addx - inx) * lambda = addy - iny
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>((P3x - P2x) * add1 + (P3x - P1x) * add2 + (P1x + P2x - P3x) - inx, lambda, (P3y - P2y) * add1 + (P3y - P1y) * add2 + (P1y + P2y - P3y) - iny));
- // sumx = lambda^2 - (addx + inx)
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, lambda, sumx + (P3x - P2x) * add1 + (P3x - P1x) * add2 + (P1x + P2x - P3x) + inx));
- // sumy = lambda * (inx - sumx) - iny
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, inx - sumx, sumy + iny));
- // Now we want to conditionally move the sum. We want that
- // outx = (add1 || add2) ? sumx : inx
- // outy = (add1 || add2) ? sumy : iny
- // so we compute move = add1 || add2, and then
- // outx = inx + (sumx - inx) * move
- // outy = iny + (sumy - iny) * move
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(1 - add1, 1 - add2, 1 - move));
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(sumx - inx, move, outx - inx));
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(sumy - iny, move, outy - iny));
- }
- void generate_r1cs_witness()
- {
- FieldT addxval = (P3x - P2x) * this->pb.val(add1) + (P3x - P1x) * this->pb.val(add2) + (P1x + P2x - P3x);
- FieldT addyval = (P3y - P2y) * this->pb.val(add1) + (P3y - P1y) * this->pb.val(add2) + (P1y + P2y - P3y);
- this->pb.val(lambda) = (addyval - this->pb.lc_val(iny)) * (addxval - this->pb.lc_val(inx)).inverse();
- this->pb.val(sumx) = this->pb.val(lambda).squared() - (addxval + this->pb.lc_val(inx));
- this->pb.val(sumy) = this->pb.val(lambda) * (this->pb.lc_val(inx) - this->pb.val(sumx)) - this->pb.lc_val(iny);
- bool a1 = this->pb.val(add1) != FieldT(0);
- bool a2 = this->pb.val(add2) != FieldT(0);
- this->pb.val(move) = a1 || a2;
- this->pb.val(outx) = (a1 || a2) ? this->pb.val(sumx) : this->pb.lc_val(inx);
- this->pb.val(outy) = (a1 || a2) ? this->pb.val(sumy) : this->pb.lc_val(iny);
- }
- };
- // Compute a*P as (outx, outy) for a given public point P, given a
- // as a bit vector. The _caller_ is responsible for proving that the
- // elements of avec are bits.
- template<typename FieldT>
- class ec_scalarmul_vec_gadget : public gadget<FieldT> {
- private:
- FieldT Cx, Cy, CPx, CPy;
- pb_variable_array<FieldT> accumx, accumy;
- std::vector<ec_add_P123_gadget<FieldT> > conddoubleadders;
- std::vector<ec_conditional_add_gadget<FieldT> > condsingleadders;
- std::vector<ec_public_add_gadget<FieldT> > singleadders;
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_variable_array<FieldT> avec;
- const FieldT Px, Py;
- // Strategy: We compute (in public) (powers of 2) times P, and then
- // conditionally add them into an accumulator. Because our adder cannot
- // handle the point at infinity O, we start the accumulator with a value
- // of C, whose discrete log with respect to P should be unknown, so that
- // we won't encounter O along the way. (Also, a should not be 0 or
- // the group order.) We actually start the accumulator with either
- // C or C+P depending on avec[0], so we get the first conditional add
- // "for free". Then we use the ec_add_P123_gadget to do the conditional
- // adds two at a time (at a cost of 6 constraints per pair, as opposed to
- // 5 for a single conditional add). If the length of avec is even, then
- // there will be one left over, and we do a single conditional add for
- // that one. Finally, we add the public point -C.
- ec_scalarmul_vec_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable_array<FieldT> &avec,
- const FieldT &Px, const FieldT &Py) :
- gadget<FieldT>(pb, "ec_pedersen_vec_gadget"),
- // Precomputed coordinates of C
- Cx(2),
- Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"),
- outx(outx), outy(outy), avec(avec), Px(Px), Py(Py)
- {
- size_t numbits = avec.size();
- accumx.allocate(this->pb, numbits/2+1, "accumx");
- accumy.allocate(this->pb, numbits/2+1, "accumy");
- ec_add_points(CPx, CPy, Cx, Cy, Px, Py);
- FieldT twoiPx, twoiPy, twoi1Px, twoi1Py, twoi3Px, twoi3Py;
- size_t i = 1;
- ec_double_point(twoiPx, twoiPy, Px, Py);
- while(i < numbits) {
- // Invariants: i is odd, and twoiP = 2^i * P
- // Compute twoi1P = 2^{i+1} * P = 2 * twoiP and
- // twoi3P = 2^i * 3 * P = 3 * twoiP
- ec_double_point(twoi1Px, twoi1Py, twoiPx, twoiPy);
- ec_add_points(twoi3Px, twoi3Py, twoi1Px, twoi1Py, twoiPx, twoiPy);
- if (i == numbits-1) {
- // There's only one bit of avec left; use a single conditional
- // add.
- condsingleadders.emplace_back(this->pb,
- accumx[(i+1)/2], accumy[(i+1)/2],
- accumx[(i-1)/2], accumy[(i-1)/2],
- avec[i],
- twoiPx, twoiPy);
- } else {
- conddoubleadders.emplace_back(this->pb,
- accumx[(i+1)/2], accumy[(i+1)/2],
- accumx[(i-1)/2], accumy[(i-1)/2],
- avec[i], avec[i+1],
- twoiPx, twoiPy, twoi1Px, twoi1Py, twoi3Px, twoi3Py);
- }
- ec_double_point(twoiPx, twoiPy, twoi1Px, twoi1Py);
- i += 2;
- }
- // If numbits is even, the output so far is in accum[(numbits)/2].
- // If numbits is odd, it is in accum[(numbits-1)/2]. So in either
- // case, it is in accum[numbits/2].
- singleadders.emplace_back(this->pb,
- outx, outy, accumx[numbits/2], accumy[numbits/2],
- Cx, -Cy);
- }
- void generate_r1cs_constraints()
- {
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(Cx + (CPx-Cx) * avec[0], 1, accumx[0]));
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(Cy + (CPy-Cy) * avec[0], 1, accumy[0]));
- for (auto&& gadget : conddoubleadders) {
- gadget.generate_r1cs_constraints();
- }
- for (auto&& gadget : condsingleadders) {
- gadget.generate_r1cs_constraints();
- }
- for (auto&& gadget : singleadders) {
- gadget.generate_r1cs_constraints();
- }
- }
- void generate_r1cs_witness()
- {
- this->pb.val(accumx[0]) = Cx + (CPx-Cx) * this->pb.val(avec[0]);
- this->pb.val(accumy[0]) = Cy + (CPy-Cy) * this->pb.val(avec[0]);
- for (auto&& gadget : conddoubleadders) {
- gadget.generate_r1cs_witness();
- }
- for (auto&& gadget : condsingleadders) {
- gadget.generate_r1cs_witness();
- }
- for (auto&& gadget : singleadders) {
- gadget.generate_r1cs_witness();
- }
- }
- };
- // Compute a*P as (outx, outy) for a given public point P, given a
- // as a field element.
- template<typename FieldT>
- class ec_scalarmul_gadget : public gadget<FieldT> {
- private:
- pb_variable_array<FieldT> avec;
- std::vector<packing_gadget<FieldT> > packers;
- std::vector<ec_scalarmul_vec_gadget<FieldT> > vecgadget;
- public:
- const pb_variable<FieldT> outx, outy, a;
- const FieldT Px, Py;
- ec_scalarmul_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable<FieldT> &a,
- const FieldT &Px, const FieldT &Py) :
- gadget<FieldT>(pb, "ec_scalarmul_gadget"),
- outx(outx), outy(outy), a(a), Px(Px), Py(Py)
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- size_t numbits = FieldT::num_bits;
- avec.allocate(this->pb, numbits, "avec");
- packers.emplace_back(this->pb, avec, a);
- vecgadget.emplace_back(this->pb, outx, outy, avec, 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();
- }
- };
- // Compute a*G + b*H as (outx, outy), given a and b as bit vectors.
- // a and b must be of the same size. The _caller_ is responsible for
- // proving that the elements of avec and bvec are bits.
- template<typename FieldT>
- class ec_pedersen_vec_gadget : public gadget<FieldT> {
- private:
- pb_variable_array<FieldT> accumx, accumy, daccumx, daccumy;
- pb_variable<FieldT> lambda;
- std::vector<ec_double_gadget<FieldT> > doublers;
- std::vector<ec_add_P123_gadget<FieldT> > adders;
- const FieldT Cx, Cy, CGx, CGy, CHx, CHy, CGHx, CGHy;
- FieldT m2nCx, m2nCy;
- // Compute m2nC = -2^n * C. We can precomute the answers for values
- // of n we expect to get.
- void compute_m2nC(FieldT &m2nCx, FieldT &m2nCy, size_t n)
- {
- if (n == 253) {
- // Precomputed coordinates of -2^253*C
- m2nCx = FieldT("2630025903576807331238993847875694711243784786568881628418508626984487096258");
- m2nCy = FieldT("17628834417659968531880949658739649785248429713924280788649629869316127047701");
- } else {
- // Invariant: m2iC = -2^i * C
- FieldT m2iCx = Cx;
- FieldT m2iCy = -Cy;
- size_t i = 0;
- while (i < n) {
- FieldT m2iCxo, m2iCyo;
- ec_double_point(m2iCxo, m2iCyo, m2iCx, m2iCy);
- m2iCx = m2iCxo;
- m2iCy = m2iCyo;
- ++i;
- }
- m2nCx = m2iCx;
- m2nCy = m2iCy;
- }
- }
- public:
- const pb_variable<FieldT> outx, outy;
- const pb_variable_array<FieldT> avec, bvec;
- ec_pedersen_vec_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable_array<FieldT> &avec,
- const pb_variable_array<FieldT> &bvec) :
- gadget<FieldT>(pb, "ec_pedersen_vec_gadget"),
- // Precomputed coordinates of C, C+G, C+H, and C+G+H
- Cx(2),
- Cy("4950745124018817972378217179409499695353526031437053848725554590521829916331"),
- CGx("4998993376791159436553350546778310121346937620672073819457843493128326049156"),
- CGy("11119675827304465476900978353730540420130346377889406728458325551400357147144"),
- CHx("19614539896004018833724771305328960655474424364705508053472946746883341111010"),
- CHy("9853241351900213537247225242092949438866383394579783148395572971112906592855"),
- CGHx("10755582242294898568680134375159803731902153202607833320871336755950640390928"),
- CGHy("3110667473759844579409644567672992116704859238881299917617768683686288881761"),
- outx(outx), outy(outy), avec(avec), bvec(bvec)
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- size_t numbits = avec.size();
- accumx.allocate(this->pb, numbits, "accumx");
- accumy.allocate(this->pb, numbits, "accumy");
- daccumx.allocate(this->pb, numbits-1, "daccumx");
- daccumy.allocate(this->pb, numbits-1, "daccumy");
- lambda.allocate(this->pb, "lambda");
- for (size_t i = 0; i < numbits-1; ++i) {
- doublers.emplace_back(this->pb, daccumx[i], daccumy[i],
- accumx[i], accumy[i]);
- adders.emplace_back(this->pb, accumx[i+1], accumy[i+1],
- daccumx[i], daccumy[i], avec[numbits-2-i], bvec[numbits-2-i],
- // The coordinates of G, H, and G+H
- FieldT(0), FieldT("11977228949870389393715360594190192321220966033310912010610740966317727761886"),
- FieldT(1), FieldT("21803877843449984883423225223478944275188924769286999517937427649571474907279"),
- FieldT("2864090850787705444524344020850508438903451433901276387624248428140647539638"),
- FieldT("3350168998338968221269367365107720885864670493693161027931048546881356285970"));
- }
- compute_m2nC(m2nCx, m2nCy, numbits-1);
- }
- void generate_r1cs_constraints()
- {
- // Strategy: We do a basic double-and-add, using the variant of a
- // single double and an add of one of (O, G, H, G+H) at each step.
- // *However*, there's a twist. Our doubling and adding routines
- // don't handle the point at infinity O as the point to add to or to
- // double. (Adding O as one of the four options above is fine.)
- // Normally, the double-and-add algorithm starts with an accumulator
- // of O, and that won't work for us. So instead, we start the
- // accumulator at a different base point C, whose discrete log
- // with respect to the (G,H) basis is unknown. Then we'll end up
- // with an extra 2^n * C in the accumulator (where n is the number
- // of doublings we do), so at the end, we'll add the (constant!)
- // point -2^n * C to get the final result. That the discrete log of
- // C is unknown means we won't encounter O along the way, either (if
- // we did, we could compute the DL of C in the (G,H) basis).
- // For the first bit, we just precompute C, C+G, C+H, C+G+H (the
- // values are above) and use the top bit of a and b to choose which
- // one to start with.
- // accumx[0] = Cx + (CGx - Cx) * avec[numbits-1] + (CHx - Cx) *
- // bvec[numbits-1] + (CGHx - CGx - CHx + Cx) *
- // avec[numbits-1]*bvec[numbits-1] (and similarly for y)
- // We could possibly optimize this later by computing the a*b
- // product once, but then we'd have to pass a large linear
- // combination to a gadget, which it probably doesn't like? It
- // would save just one constraint, so probably not so important?
- size_t numbits = avec.size();
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>((CGHx - CGx - CHx + Cx) * avec[numbits-1], bvec[numbits-1], accumx[0] - (Cx + (CGx - Cx) * avec[numbits-1] + (CHx - Cx) * bvec[numbits-1])));
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>((CGHy - CGy - CHy + Cy) * avec[numbits-1], bvec[numbits-1], accumy[0] - (Cy + (CGy - Cy) * avec[numbits-1] + (CHy - Cy) * bvec[numbits-1])));
- // After that, for each remaining bit of a and b, we use the
- // ec_double_gadget and the ec_add_GH_gadget to accumulate
- // the answer.
- for (size_t i = 0; i < numbits-1; ++i) {
- doublers[i].generate_r1cs_constraints();
- adders[i].generate_r1cs_constraints();
- }
- // Finally, we add the constant point -2^n * C to the result, where
- // n = numbits-1
- // (m2nCx - accumx[numbits-1]) * lambda = m2nCy - accumy[numbits-1]
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(m2nCx - accumx[numbits-1], lambda, m2nCy - accumy[numbits-1]));
- // outx = lambda^2 - (m2nCx + accumx[numbits-1])
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, lambda, outx + m2nCx + accumx[numbits-1]));
- // outy = lambda * (accumx[numbits-1] - outx) - accumy[numbits-1]
- this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lambda, accumx[numbits-1] - outx, outy + accumy[numbits-1]));
- }
- void generate_r1cs_witness()
- {
- size_t numbits = avec.size();
- this->pb.val(accumx[0]) = Cx + (CGx - Cx) * this->pb.val(avec[numbits-1]) + (CHx - Cx) * this->pb.val(bvec[numbits-1]) + (CGHx - CGx - CHx + Cx) * this->pb.val(avec[numbits-1])*this->pb.val(bvec[numbits-1]);
- this->pb.val(accumy[0]) = Cy + (CGy - Cy) * this->pb.val(avec[numbits-1]) + (CHy - Cy) * this->pb.val(bvec[numbits-1]) + (CGHy - CGy - CHy + Cy) * this->pb.val(avec[numbits-1])*this->pb.val(bvec[numbits-1]);
- for (size_t i = 0; i < numbits-1; ++i) {
- doublers[i].generate_r1cs_witness();
- adders[i].generate_r1cs_witness();
- }
- this->pb.val(lambda) = (m2nCy - this->pb.val(accumy[numbits-1])) *
- (m2nCx - this->pb.val(accumx[numbits-1])).inverse();
- this->pb.val(outx) = this->pb.val(lambda).squared() -
- (m2nCx + this->pb.val(accumx[numbits-1]));
- this->pb.val(outy) = this->pb.val(lambda) *
- (this->pb.val(accumx[numbits-1]) - this->pb.val(outx))
- - this->pb.val(accumy[numbits-1]);
-
- }
- };
- // Compute a*G + b*H as (outx, outy), given a and b as field elements.
- template<typename FieldT>
- class ec_old_pedersen_gadget : public gadget<FieldT> {
- private:
- pb_variable_array<FieldT> avec, bvec;
- std::vector<packing_gadget<FieldT> > packers;
- std::vector<ec_pedersen_vec_gadget<FieldT> > vecgadget;
- public:
- const pb_variable<FieldT> outx, outy, a, b;
- ec_old_pedersen_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable<FieldT> &a,
- const pb_variable<FieldT> &b) :
- gadget<FieldT>(pb, "ec_old_pedersen_gadget"),
- outx(outx), outy(outy), a(a), b(b)
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- size_t numbits = FieldT::num_bits;
- avec.allocate(this->pb, numbits, "avec");
- bvec.allocate(this->pb, numbits, "bvec");
- packers.emplace_back(this->pb, avec, a);
- packers.emplace_back(this->pb, bvec, b);
- vecgadget.emplace_back(this->pb, outx, outy, avec, bvec);
- }
- void generate_r1cs_constraints()
- {
- packers[0].generate_r1cs_constraints(true);
- packers[1].generate_r1cs_constraints(true);
- vecgadget[0].generate_r1cs_constraints();
- }
- void generate_r1cs_witness()
- {
- packers[0].generate_r1cs_witness_from_packed();
- packers[1].generate_r1cs_witness_from_packed();
- vecgadget[0].generate_r1cs_witness();
- }
- };
- // Compute a*G + b*H as (outx, outy), given a and b as field elements.
- template<typename FieldT>
- class ec_pedersen_gadget : public gadget<FieldT> {
- private:
- pb_variable<FieldT> aoutx, aouty, boutx, bouty;
- std::vector<ec_scalarmul_gadget<FieldT> > mulgadgets;
- std::vector<ec_add_gadget<FieldT> > addgadget;
- const FieldT Gx, Gy, Hx, Hy;
- public:
- const pb_variable<FieldT> outx, outy, a, b;
- ec_pedersen_gadget(protoboard<FieldT> &pb,
- const pb_variable<FieldT> &outx,
- const pb_variable<FieldT> &outy,
- const pb_variable<FieldT> &a,
- const pb_variable<FieldT> &b) :
- gadget<FieldT>(pb, "ec_pedersen_gadget"),
- outx(outx), outy(outy), a(a), b(b),
- // Precomputed coordinates of G and H
- Gx(0),
- Gy("11977228949870389393715360594190192321220966033310912010610740966317727761886"),
- Hx(1),
- Hy("21803877843449984883423225223478944275188924769286999517937427649571474907279")
- {
- // Allocate variables to protoboard
- // The strings (like "x") are only for debugging purposes
-
- aoutx.allocate(this->pb, "aoutx");
- aouty.allocate(this->pb, "aouty");
- boutx.allocate(this->pb, "boutx");
- bouty.allocate(this->pb, "bouty");
- mulgadgets.emplace_back(this->pb, aoutx, aouty, a, Gx, Gy);
- mulgadgets.emplace_back(this->pb, boutx, bouty, b, Hx, Hy);
- addgadget.emplace_back(this->pb, outx, outy, aoutx, aouty, boutx, bouty);
- }
- void generate_r1cs_constraints()
- {
- 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();
- }
- };
|