diff --git a/circom_circuits/Jubjub/escalarmulanyJubjub.circom b/circom_circuits/Jubjub/escalarmulanyJubjub.circom new file mode 100644 index 0000000..e8f6e26 --- /dev/null +++ b/circom_circuits/Jubjub/escalarmulanyJubjub.circom @@ -0,0 +1,197 @@ +/* + Copyright 2018 0KIMS association. + + This file is part of circom (Zero Knowledge Circuit Compiler). + + circom is a free software: you can redistribute it and/or modify it + under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + circom is distributed in the hope that it will be useful, but WITHOUT + ANY WARRANTY; without even the implied warranty of MERCHANTABILITY + or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public + License for more details. + + You should have received a copy of the GNU General Public License + along with circom. If not, see . +*/ +pragma circom 2.0.0; + +include "montgomeryJubjub.circom"; +include "jubjub.circom"; +include "../../circom_circuits/circomlib/circuits/comparators.circom"; + +template Multiplexor2() { + signal input sel; + signal input in[2][2]; + signal output out[2]; + + out[0] <== (in[1][0] - in[0][0])*sel + in[0][0]; + out[1] <== (in[1][1] - in[0][1])*sel + in[0][1]; +} + +template BitElementMulAny() { + signal input sel; + signal input dblIn[2]; + signal input addIn[2]; + signal output dblOut[2]; + signal output addOut[2]; + + component doubler = MontgomeryDouble(); + component adder = MontgomeryAdd(); + component selector = Multiplexor2(); + + + sel ==> selector.sel; + + dblIn[0] ==> doubler.in[0]; + dblIn[1] ==> doubler.in[1]; + doubler.out[0] ==> adder.in1[0]; + doubler.out[1] ==> adder.in1[1]; + addIn[0] ==> adder.in2[0]; + addIn[1] ==> adder.in2[1]; + addIn[0] ==> selector.in[0][0]; + addIn[1] ==> selector.in[0][1]; + adder.out[0] ==> selector.in[1][0]; + adder.out[1] ==> selector.in[1][1]; + + doubler.out[0] ==> dblOut[0]; + doubler.out[1] ==> dblOut[1]; + selector.out[0] ==> addOut[0]; + selector.out[1] ==> addOut[1]; +} + +// p is montgomery point +// n must be <= 248 +// returns out in twisted edwards +// Double is in montgomery to be linked; + +template SegmentMulAny(n) { + signal input e[n]; + signal input p[2]; + signal output out[2]; + signal output dbl[2]; + + component bits[n-1]; + + component e2m = Edwards2Montgomery(); + + p[0] ==> e2m.in[0]; + p[1] ==> e2m.in[1]; + + var i; + + bits[0] = BitElementMulAny(); + e2m.out[0] ==> bits[0].dblIn[0]; + e2m.out[1] ==> bits[0].dblIn[1]; + e2m.out[0] ==> bits[0].addIn[0]; + e2m.out[1] ==> bits[0].addIn[1]; + e[1] ==> bits[0].sel; + + for (i=1; i bits[i].dblIn[0]; + bits[i-1].dblOut[1] ==> bits[i].dblIn[1]; + bits[i-1].addOut[0] ==> bits[i].addIn[0]; + bits[i-1].addOut[1] ==> bits[i].addIn[1]; + e[i+1] ==> bits[i].sel; + } + + bits[n-2].dblOut[0] ==> dbl[0]; + bits[n-2].dblOut[1] ==> dbl[1]; + + component m2e = Montgomery2Edwards(); + + bits[n-2].addOut[0] ==> m2e.in[0]; + bits[n-2].addOut[1] ==> m2e.in[1]; + + component eadder = JubjubAdd(); + + m2e.out[0] ==> eadder.x1; + m2e.out[1] ==> eadder.y1; + -p[0] ==> eadder.x2; + p[1] ==> eadder.y2; + + component lastSel = Multiplexor2(); + + e[0] ==> lastSel.sel; + eadder.xout ==> lastSel.in[0][0]; + eadder.yout ==> lastSel.in[0][1]; + m2e.out[0] ==> lastSel.in[1][0]; + m2e.out[1] ==> lastSel.in[1][1]; + + lastSel.out[0] ==> out[0]; + lastSel.out[1] ==> out[1]; +} + +// This function assumes that p is in the subgroup and it is different to 0 + +template EscalarMulAny(n) { + signal input e[n]; // Input in binary format + signal input p[2]; // Point (Twisted format) + signal output out[2]; // Point (Twisted format) + + var nsegments = (n-1)\148 +1; + var nlastsegment = n - (nsegments-1)*148; + + component segments[nsegments]; + component doublers[nsegments-1]; + component m2e[nsegments-1]; + component adders[nsegments-1]; + component zeropoint = IsZero(); + zeropoint.in <== p[0]; + + var s; + var i; + var nseg; + + for (s=0; s segments[s].e[i]; + } + + if (s==0) { + // force G8 point if input point is zero + segments[s].p[0] <== p[0] + (0x11dafe5d23e1218086a365b99fbf3d3be72f6afd7d1f72623e6b071492d1122b - p[0])*zeropoint.out; + segments[s].p[1] <== p[1] + (0x1d523cf1ddab1a1793132e78c866c0c33e26ba5cc220fed7cc3f870e59d292aa - p[1])*zeropoint.out; + } else { + doublers[s-1] = MontgomeryDouble(); + m2e[s-1] = Montgomery2Edwards(); + adders[s-1] = JubjubAdd(); + + segments[s-1].dbl[0] ==> doublers[s-1].in[0]; + segments[s-1].dbl[1] ==> doublers[s-1].in[1]; + + doublers[s-1].out[0] ==> m2e[s-1].in[0]; + doublers[s-1].out[1] ==> m2e[s-1].in[1]; + + m2e[s-1].out[0] ==> segments[s].p[0]; + m2e[s-1].out[1] ==> segments[s].p[1]; + + if (s==1) { + segments[s-1].out[0] ==> adders[s-1].x1; + segments[s-1].out[1] ==> adders[s-1].y1; + } else { + adders[s-2].xout ==> adders[s-1].x1; + adders[s-2].yout ==> adders[s-1].y1; + } + segments[s].out[0] ==> adders[s-1].x2; + segments[s].out[1] ==> adders[s-1].y2; + } + } + + if (nsegments == 1) { + segments[0].out[0]*(1-zeropoint.out) ==> out[0]; + segments[0].out[1]+(1-segments[0].out[1])*zeropoint.out ==> out[1]; + } else { + adders[nsegments-2].xout*(1-zeropoint.out) ==> out[0]; + adders[nsegments-2].yout+(1-adders[nsegments-2].yout)*zeropoint.out ==> out[1]; + } +} diff --git a/circom_circuits/Jubjub/jubjub.circom b/circom_circuits/Jubjub/jubjub.circom new file mode 100644 index 0000000..c9c887f --- /dev/null +++ b/circom_circuits/Jubjub/jubjub.circom @@ -0,0 +1,63 @@ +/* + Copyright 2018 0KIMS association. + + This file is part of circom (Zero Knowledge Circuit Compiler). + + circom is a free software: you can redistribute it and/or modify it + under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + circom is distributed in the hope that it will be useful, but WITHOUT + ANY WARRANTY; without even the implied warranty of MERCHANTABILITY + or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public + License for more details. + + You should have received a copy of the GNU General Public License + along with circom. If not, see . +*/ +pragma circom 2.1.9; + +template JubjubAdd() { + signal input x1; + signal input y1; + signal input x2; + signal input y2; + signal output xout; + signal output yout; + + signal beta; + signal gamma; + signal delta; + signal tau; + + var a = 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000; + var d = 0x2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1; + + beta <== x1*y2; + gamma <== y1*x2; + delta <== (-a*x1+y1)*(x2 + y2); + tau <== beta * gamma; + + xout <-- (beta + gamma) / (1+ d*tau); + (1+ d*tau) * xout === (beta + gamma); + + yout <-- (delta + a*beta - gamma) / (1-d*tau); + (1-d*tau)*yout === (delta + a*beta - gamma); +} + +template JubjubDbl() { + signal input x; + signal input y; + signal output xout; + signal output yout; + + component adder = JubjubAdd(); + adder.x1 <== x; + adder.y1 <== y; + adder.x2 <== x; + adder.y2 <== y; + + adder.xout ==> xout; + adder.yout ==> yout; +} \ No newline at end of file diff --git a/circom_circuits/Jubjub/montgomeryJubjub.circom b/circom_circuits/Jubjub/montgomeryJubjub.circom new file mode 100644 index 0000000..60965f6 --- /dev/null +++ b/circom_circuits/Jubjub/montgomeryJubjub.circom @@ -0,0 +1,142 @@ +/* + Copyright 2018 0KIMS association. + + This file is part of circom (Zero Knowledge Circuit Compiler). + + circom is a free software: you can redistribute it and/or modify it + under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + circom is distributed in the hope that it will be useful, but WITHOUT + ANY WARRANTY; without even the implied warranty of MERCHANTABILITY + or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public + License for more details. + + You should have received a copy of the GNU General Public License + along with circom. If not, see . +*/ + +/* + Source: https://en.wikipedia.org/wiki/Montgomery_curve + + 1 + y 1 + y + [u, v] = [ ------- , ---------- ] + 1 - y (1 - y)x + + */ + pragma circom 2.0.0; + +template Edwards2Montgomery() { + signal input in[2]; + signal output out[2]; + + out[0] <-- (1 + in[1]) / (1 - in[1]); + out[1] <-- out[0] / in[0]; + + + out[0] * (1-in[1]) === (1 + in[1]); + out[1] * in[0] === out[0]; +} + +/* + + u u - 1 + [x, y] = [ ---, ------- ] + v u + 1 + + */ +template Montgomery2Edwards() { + signal input in[2]; + signal output out[2]; + + out[0] <-- in[0] / in[1]; + out[1] <-- (in[0] - 1) / (in[0] + 1); + + out[0] * in[1] === in[0]; + out[1] * (in[0] + 1) === in[0] - 1; +} + + +/* + x2 - x1 + lamda = --------- + y2 - y1 + + x3 + A + x1 + x2 + x3 = B * lamda^2 - A - x1 -x2 => lamda^2 = ------------------ + B + + y3 = (2*x1 + x2 + A)*lamda - B*lamda^3 - y1 => + + + => y3 = lamda * ( 2*x1 + x2 + A - x3 - A - x1 - x2) - y1 => + + => y3 = lamda * ( x1 - x3 ) - y1 + +---------- + + y2 - y1 + lamda = --------- + x2 - x1 + + x3 = B * lamda^2 - A - x1 -x2 + + y3 = lamda * ( x1 - x3 ) - y1 + + */ + +template MontgomeryAdd() { + signal input in1[2]; + signal input in2[2]; + signal output out[2]; + + var a = 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000; + var d = 0x2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1; + + var A = (2 * (a + d)) / (a - d); + var B = 4 / (a - d); + + signal lamda; + + lamda <-- (in2[1] - in1[1]) / (in2[0] - in1[0]); + lamda * (in2[0] - in1[0]) === (in2[1] - in1[1]); + + out[0] <== B*lamda*lamda - A - in1[0] -in2[0]; + out[1] <== lamda * (in1[0] - out[0]) - in1[1]; +} + +/* + + x1_2 = x1*x1 + + 3*x1_2 + 2*A*x1 + 1 + lamda = --------------------- + 2*B*y1 + + x3 = B * lamda^2 - A - x1 -x1 + + y3 = lamda * ( x1 - x3 ) - y1 + + */ +template MontgomeryDouble() { + signal input in[2]; + signal output out[2]; + + var a = 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000000; + var d = 0x2a9318e74bfa2b48f5fd9207e6bd7fd4292d7f6d37579d2601065fd6d6343eb1; + + var A = (2 * (a + d)) / (a - d); + var B = 4 / (a - d); + + signal lamda; + signal x1_2; + + x1_2 <== in[0] * in[0]; + + lamda <-- (3*x1_2 + 2*A*in[0] + 1 ) / (2*B*in[1]); + lamda * (2*B*in[1]) === (3*x1_2 + 2*A*in[0] + 1 ); + + out[0] <== B*lamda*lamda - A - 2*in[0]; + out[1] <== lamda * (in[0] - out[0]) - in[1]; +} diff --git a/proof_of_validator/circom/validator_Caulk.circom b/proof_of_validator/circom/validator_Caulk.circom new file mode 100644 index 0000000..6ef6aef --- /dev/null +++ b/proof_of_validator/circom/validator_Caulk.circom @@ -0,0 +1,209 @@ +//test +pragma circom 2.1.9; + +include "../../circom_circuits/hash/anemoi/anemoi_2_to_1_Jubjub.circom"; +include "../../circom_circuits/hash/anemoi/anemoi_4_to_1_Jubjub.circom"; +include "../../circom_circuits/hash/anemoi/anemoi_16_to_1_Jubjub.circom"; +include "../../circom_circuits/circomlib/circuits/bitify.circom"; +include "../../circom_circuits/circomlib/circuits/comparators.circom"; +include "../../circom_circuits/Jubjub/escalarmulanyJubjub.circom"; +include "../../circom_circuits/Jubjub/jubjub.circom"; + +template BLSLessThan(n) { + assert(n <= 253); + signal input in[2]; + signal output out; + + component n2b = Num2Bits(n+1); + + n2b.in <== in[0]+ (1< n2b.in; + + for (var i=0; i<255; i++) { + n2b.out[i] ==> out[i]; + if(i != 0){ + n2b.out[i] ==> check_range.in[i-1]; + } + } + + check_range.out * (n2b.out[0]) === 0; //must be zero exept if the first bit is 0 => then in is on 254 bits and p-1 on 255 +} + +template check_bits(n){ + signal input bits[n]; + for(var i=0; i