diff --git a/CHANGES.txt b/CHANGES.txt new file mode 100644 index 00000000..127ae7ea --- /dev/null +++ b/CHANGES.txt @@ -0,0 +1,21 @@ +Changes: + +- Added file tags-managing.circom with templates for managing tags binary, maxbit, maxvalue... + +- Removed files mimc.circom, mimcsponge.circom, eddsamimc.circom, eddsamimcsponge.circom, multiplexer.circom + +- Added info of the prime field required by the templates + +- Added specification describing the expected behavior of the templates + +- Updated required circom version to 2.1.5 + +- Changed comparators GreaterEqThan and LessEqThan to satisfy tags + +- Change name of the template EdDSAVerifier to EdDSAPedersenVerifier in file eddsapedersen.circom (previously eddsa.circom) + +- Fixed include in poseidon_old.circom => using old constants now + +- Moved template Compconstant(ct) and Sign (from files compconstant.circom and sign.circom) to comparators.circom + +- Added tags minvlue and maxvalue to babypkb diff --git a/circuits/aliascheck.circom b/circuits/aliascheck.circom index 1c5a5f87..11a09de8 100644 --- a/circuits/aliascheck.circom +++ b/circuits/aliascheck.circom @@ -16,18 +16,33 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "compconstant.circom"; +include "comparators.circom"; +include "buses.circom"; +include "bitify.circom"; + +// The templates and functions of this file only work for any prime field + + +/* +*** AliasCheck(): template that receives an input in representing a value in binary using maxbits() bits and checks that the value belongs to the prime field (that is, if in represents the value x in binary, then the template checks that x <= p-1) + - Inputs: in[maxbits()] -> array of maxbits() bits + requires tag binary + - Outputs: None + + Example: in case we are working in the prime field with p = 11, then AliasCheck()([1, 0, 0, 1]) is satisfiable as 9 < 11, but AliasCheck()([1, 0, 1, 1]) is not as 13 >= 11. In the second case the executable program (C or WASM) reaches a false assert, and the generated R1CS is not satisfiable + +*/ template AliasCheck() { - signal input in[254]; + input signal {binary} in[maxbits()]; - component compConstant = CompConstant(-1); + component compConstant = CompConstant(maxbits(), -1); - for (var i=0; i<254; i++) in[i] ==> compConstant.in[i]; + compConstant.in <== in; compConstant.out === 0; } diff --git a/circuits/babyjub.circom b/circuits/babyjub.circom index 36810fee..1c899f47 100644 --- a/circuits/babyjub.circom +++ b/circuits/babyjub.circom @@ -16,18 +16,60 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; include "bitify.circom"; -include "escalarmulfix.circom"; +include "montgomery.circom"; +include "escalarmul/escalarmulfix.circom"; + +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. + +/* + The Baby-Jubjub Montgomery elliptic curve defined over the finite field bn128 is given by the equation + + B*v^2 = u^3 + A*u^2 + u, A = 168698, B = 1 + + This curve is birationally equivalent to the twisted Edwards elliptic curve + + a*x^2 + y^2 = 1 + d*x^2*y^2, a = 168700 = (A+2)/B, d = 168696 = (A-2)/B + + u u-1 1+y 1+y + via the map (u,v) -> (x,y) = [ --- , ----- ] with inverse (x,y) -> (u,v) = [ ----- , --------- ] + v u+1 1-y (1-y)*x + + Since a is not a square in bn128, the twisted Edwards curve is a quadratic twist of the Edwards curve + + x'^2 + y'^2 = 1 + d'*x'^2*y'^2 + + via the map (x,y) -> (x',y') = [ sqrt(a)*x , y ] + + where d' = 9706598848417545097372247223557719406784115219466060233080913168975159366771. + We will be working with the twisted Edwards form of the Baby-Jubjub curve because the algorithms for adding, doubling + and multiplying points by a scalar are faster this way. +*/ + +/* + spec tag babyedwards: 168700*(p.x)^2 + (p.y)^2 = 1 + 168696*(p.x)^2*(p.y)^2 + spec tag babymontgomery: (p.y)^2 = (p.x)^3 + 168698*(p.x)^2 + p.x +*/ + +/* +*** BabyAdd(): template that receives two points of the Baby-Jubjub curve in twisted Edwards form and returns the addition of the points. + - Inputs: p1 = (x1, y1) -> bus representing a point of the curve in twisted Edwards form + p2 = (x2, y2) -> bus representing a point of the curve in twisted Edwards form + - Outputs: pout = (xout, yout) -> bus representing a point of the curve in twisted Edwards form, pout = p1 + p2 + + Twisted Edwards Addition Law: + x1*y2 + y1*x2 y1*y2 - a * x1*x2 + [xout, yout] = [x1, y1] + [x2, y2] = [ --------------------- , --------------------- ] + 1 + d * x1*x2*y1*y2 1 - d * x1*x2*y1*y2 + +*/ template BabyAdd() { - signal input x1; - signal input y1; - signal input x2; - signal input y2; - signal output xout; - signal output yout; + input Point {babyedwards} pin1,pin2; + output Point {babyedwards} pout; signal beta; signal gamma; @@ -37,57 +79,92 @@ template BabyAdd() { var a = 168700; var d = 168696; - beta <== x1*y2; - gamma <== y1*x2; - delta <== (-a*x1+y1)*(x2 + y2); + beta <== pin1.x*pin2.y; + gamma <== pin1.y*pin2.x; + delta <== (-a*pin1.x + pin1.y)*(pin2.x + pin2.y); tau <== beta * gamma; - xout <-- (beta + gamma) / (1+ d*tau); - (1+ d*tau) * xout === (beta + gamma); + pout.x <-- (beta + gamma) / (1 + d*tau); + (1 + d*tau) * pout.x === (beta + gamma); - yout <-- (delta + a*beta - gamma) / (1-d*tau); - (1-d*tau)*yout === (delta + a*beta - gamma); + pout.y <-- (delta + a*beta - gamma) / (1 - d*tau); + (1 - d*tau)*pout.y === (delta + a*beta - gamma); } + + +/* +*** BabyDouble(): template that receives a point pin of the Baby-Jubjub curve in twisted Edwards form and returns the point 2 * pin. + - Inputs: pin = (x1, y1) -> bus representing a point of the curve in twisted Edwards form + - Outputs: pout = (x2, y2) -> bus representing a point of the curve in twisted Edwards form, 2 * pin = pout + + Twisted Edwards Doubling Law: 2 * [x, y] = [x, y] + [x, y] + +*/ + template BabyDbl() { - signal input x; - signal input y; - signal output xout; - signal output yout; + input Point {babyedwards} pin; + output Point {babyedwards} pout; component adder = BabyAdd(); - adder.x1 <== x; - adder.y1 <== y; - adder.x2 <== x; - adder.y2 <== y; - adder.xout ==> xout; - adder.yout ==> yout; + adder.pin1 <== pin; + adder.pin2 <== pin; + adder.pout ==> pout; } +/* +*** BabyCheck(): template that receives an input point pin and checks if it belongs to the Baby-Jubjub curve in twisted Edwards form. + - Inputs: pin = (x1, y1) -> bus representing the point that we want to check + - Outputs: pout = (x2, y2) -> two field values representing the same point as the input but with the babyedwards tag + attached to point out it is a point of the Baby-Jubjub curve in twisted Edwards form + + The set of solutions of BabyCheck()(p) are the points of the Baby-Jubjub curve in twisted Edwards form. + They must fulfil the equation a*x^2 + y^2 = 1 + d*x^2*y^2, a = 168700, d = 168696. + +*/ + + template BabyCheck() { - signal input x; - signal input y; + input Point pin; + output Point {babyedwards} pout; + // Point p2; signal x2; signal y2; var a = 168700; var d = 168696; - x2 <== x*x; - y2 <== y*y; - + x2 <== pin.x*pin.x; //x2 = pin.x^2 + y2 <== pin.y*pin.y; //y2 = pin.y^2 + a*x2 + y2 === 1 + d*x2*y2; + + pout <== pin; } -// Extracts the public key from private key + +/* +*** BabyPbk(): template that receives an input in representing a value in the prime subgroup with order + r = 2736030358979909402780800718157159386076813972158567259200215660948447373041, + and returns the point of the Baby-Jubjub curve in twisted Edwards form in * P, with P being the point + P = (5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203) + +This template is used to extract the public key from the private key. + - Inputs: in -> field value in [1,r-1] + - Outputs: A = (x, y) -> two field values representing a point of the curve in Edwards form, in * P = A + +*/ + template BabyPbk() { - signal input in; - signal output Ax; - signal output Ay; + input signal {minvalue, maxvalue} in; + output Point {babyedwards} A; + + var r = 2736030358979909402780800718157159386076813972158567259200215660948447373041; + assert(in.minvalue > 0 && in.maxvalue < r); var BASE8[2] = [ 5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203 @@ -98,10 +175,6 @@ template BabyPbk() { component mulFix = EscalarMulFix(253, BASE8); - var i; - for (i=0; i<253; i++) { - mulFix.e[i] <== pvkBits.out[i]; - } - Ax <== mulFix.out[0]; - Ay <== mulFix.out[1]; + mulFix.e <== pvkBits.out; + A <== mulFix.pout; } diff --git a/circuits/binnum.circom b/circuits/binnum.circom new file mode 100644 index 00000000..1ca4dd84 --- /dev/null +++ b/circuits/binnum.circom @@ -0,0 +1,122 @@ +/* + 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.5; + +include "aliascheck.circom"; +include "buses.circom"; +include "bitify.circom"; + +/* +*** Num2Bin(n): template that transforms an input into its binary representation using n bits + - Inputs: in -> field value + - Output: out -> BinaryNumber(n) bus with the n bits of the binary representation + It has the bus tag "unique" which indicates that the number represented is below the prime + + Example: Num2Bin(3)(7) = {bits: [1, 1, 1]} + Note: in case the input in cannot be represented using n bits then the generated system of constraints does not have any solution for that input. + For instance, Num2Bin(3)(10) -> no solution + +*/ + +template Num2Bin(n) { + signal input in; + BinaryNumber(n) output {unique} out; + var lc1=0; + + var e2=1; + for (var i = 0; i> i) & 1; + out.bits[i] * (out.bits[i] -1 ) === 0; + lc1 += out.bits[i] * e2; + e2 = e2+e2; + } + lc1 === in; + + if (n == maxbits()) { + component aliasCheck = AliasCheck(); + aliasCheck.in <== out.bits; + } +} + + +/* + +*** Bin2Num(n): template that transforms an input bus representing a value x in binary into the decimal representation of x + - Inputs: in -> BinaryNumber(n) bus with the binary representation of out using n bits + requires tag "unique" + - Output: out -> value represented by the input + satisfies tag maxbit with out.maxbit = n + + Example: Bits2Num(3)([1, 0, 1]) = 5 + +*/ + + +template Bin2Num(n) { + BinaryNumber(n) input {unique} in; + signal output {maxbit} out; + var lc1=0; + + var e2 = 1; + for (var i = 0; i out; +} + + +/* +*** Num2BinNeg(n): template that given an input x returns the binary representation of 2 ** n - x using n bits, in case in == 0 then it returns 0 + - Inputs: in -> field value + - Output: out -> BinaryNumber(n) bus with the binary representation of 2 ** n - in using n bits if in != 0, + and all 0's otherwise. + It has the bus tag "unique" which indicates that the number represented is below the prime + + Example: Num2BitsNeg(3)(2) = [0, 1, 1], Num2Bits(3)(8) = [0, 0, 0] + +*/ + +template Num2BinNeg(n) { + signal input in; + BinaryNumber(n) output {unique} out; + var lc1=0; + + component isZero; + + isZero = IsZero(); + + var neg = n == 0 ? 0 : 2**n - in; + + for (var i = 0; i> i) & 1; + out[i] * (out[i] -1 ) === 0; + lc1 += out[i] * 2**i; + } + in ==> isZero.in; + lc1 + isZero.out * 2**n === 2**n - in; + + + if (n == maxbits()) { + component aliasCheck = AliasCheck(); + aliasCheck.in <== out.bits; + } + +} diff --git a/circuits/binsub.circom b/circuits/binsub.circom index a20fbf81..4082aea9 100644 --- a/circuits/binsub.circom +++ b/circuits/binsub.circom @@ -17,32 +17,44 @@ along with circom. If not, see . */ -/* -This component creates a binary substraction. - +pragma circom 2.1.5; -Main Constraint: - (in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1)) + - + 2^n - - (in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1)) - === - out[0] * 2^0 + out[1] * 2^1 + + out[n-1] *2^(n-1) + aux +// The templates and functions in this file are general and work for any prime field - out[0] * (out[0] - 1) === 0 - out[1] * (out[0] - 1) === 0 - . - . - . - out[n-1] * (out[n-1] - 1) === 0 - aux * (aux-1) == 0 +/* +*** BinSub(n): template that receives two inputs of n bits representing values in[0] and in[1] in binary and returns n bits representing the result of in[0] - in[1] + - Inputs: in[2][n] -> two arrays representing the values in[0] and in[1] using n bits + requires tag binary + - Output: out[n] -> result of in[0] - in[1] expressed using n bits + satisfies tag binary + + Example: BinSub(3)([[1, 0, 1], [1, 1, 1]]) = [0, 1, 1] + + + Main Constraint: + (in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1)) + + + 2^n + - (in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1)) + === + out[0] * 2^0 + out[1] * 2^1 + + out[n-1] *2^(n-1) + aux * 2^n + + + out[0] * (out[0] - 1) === 0 + out[1] * (out[0] - 1) === 0 + . + . + . + out[n-1] * (out[n-1] - 1) === 0 + aux * (aux-1) == 0 + */ -pragma circom 2.0.0; + template BinSub(n) { - signal input in[2][n]; - signal output out[n]; + input signal {binary} in[2][n]; + output signal {binary} out[n]; signal aux; diff --git a/circuits/binsum.circom b/circuits/binsum.circom index 28c7fcce..667ce700 100644 --- a/circuits/binsum.circom +++ b/circuits/binsum.circom @@ -17,55 +17,45 @@ along with circom. If not, see . */ -/* - -Binary Sum -========== - -This component creates a binary sum componet of ops operands and n bits each operand. - -e is Number of carries: Depends on the number of operands in the input. - -Main Constraint: - in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1) + - + in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1) + - + .. - + in[ops-1][0] * 2^0 + in[ops-1][1] * 2^1 + ..... + in[ops-1][n-1] * 2^(n-1) + - === - out[0] * 2^0 + out[1] * 2^1 + + out[n+e-1] *2(n+e-1) + pragma circom 2.1.5; -To waranty binary outputs: - - out[0] * (out[0] - 1) === 0 - out[1] * (out[0] - 1) === 0 - . - . - . - out[n+e-1] * (out[n+e-1] - 1) == 0 - - */ +// The templates and functions in this file are general and work for any prime field /* - This function calculates the number of extra bits in the output to do the full sum. - */ - pragma circom 2.0.0; - -function nbits(a) { - var n = 1; - var r = 0; - while (n-1 ops arrays representing the values in[0], ... , in[ops - 1] using n bits + satisfies tag binary + - Output: out[n + nbits(ops - 1)] -> result of in[0] + ... + in[ops - 1] expressed using n + nbits(ops) bits + satisfies tag binary + + Example: BinSum(3, 3)([[1, 0, 1], [1, 1, 1], [0, 0, 1]]) = [0, 0, 0, 0, 1] + + + Main Constraint: + in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1) + + + in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1) + + + .. + + in[ops-1][0] * 2^0 + in[ops-1][1] * 2^1 + ..... + in[ops-1][n-1] * 2^(n-1) + + === + out[0] * 2^0 + out[1] * 2^1 + + out[n+e-1] *2(n+e-1) + + To waranty output binarys: + + out[0] * (out[0] - 1) === 0 + out[1] * (out[0] - 1) === 0 + . + . + . + out[n+e-1] * (out[n+e-1] - 1) == 0 + +*/ template BinSum(n, ops) { var nout = nbits((2**n -1)*ops); - signal input in[ops][n]; - signal output out[nout]; + input signal {binary} in[ops][n]; + output signal {binary} out[nout]; var lin = 0; var lout = 0; diff --git a/circuits/bitify.circom b/circuits/bitify.circom index bfdd4e82..5226fd91 100644 --- a/circuits/bitify.circom +++ b/circuits/bitify.circom @@ -16,15 +16,81 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; include "comparators.circom"; include "aliascheck.circom"; +include "buses.circom"; +// The templates and functions of this file only work for any prime field + +/* +*** maxbits(): function that returns the number of bits that we use to represent the prime generating the field + - Inputs: None + - Outputs: number of bits that we use to represent the field + + + Example: if we consider the prime p = 11, then maxbits() = 4 +*/ + +function maxbits(){ + var n = 1; + var r = 1; + while(2 * n > n){ + n = n * 2; + r = r + 1; + } + return r + 1; +} + + +/* +*** nbits(x): function that returns the number of bits that we need to represent the value x + - Inputs: x -> field value + - Output: number of bits needed to represent x + + Example: nbits(7) = 3, nbits(10) = 4 + +*/ + +function nbits(a) { + if (a == 0){ + return 1; + } else if (a < 0){ // in case a > p \ 2 -> we need maxbits() + return(maxbits()); + } else{ + var n = 1; + var r = 0; + + while (n-1= 0) { + r++; + n *= 2; + log(n); + } + if (n-1 < 0){ + return maxbits(); + } + return r; + } +} + + +/* +*** Num2Bits(n): template that transforms an input into its binary representation using n bits + - Inputs: in -> field value + - Output: out[n] -> binary representation of in using n bits + satisfies tag binary + + Example: Num2Bits(3)(7) = [1, 1, 1] + Note: in case the input in cannot be represented using n bits then the generated system of constraints does not have any solution for that input. + For instance, Num2Bits(3)(10) -> no solution + +*/ + template Num2Bits(n) { - signal input in; - signal output out[n]; + input signal in; + output signal {binary} out[n]; var lc1=0; var e2=1; @@ -34,27 +100,52 @@ template Num2Bits(n) { lc1 += out[i] * e2; e2 = e2+e2; } - + lc1 === in; } +/* + +*** Num2Bits_strict(): template that transforms an input into its binary representation using 254 bits + - Inputs: in -> field value + - Output: out[n] -> binary representation of in using 254 bits + satisfies tag binary + + Example: Assuming p = 11, then Num2Bits_strict()(13) = [0, 1, 0, 0] + +*/ + template Num2Bits_strict() { - signal input in; - signal output out[254]; + + var max_nbits = maxbits(); + + input signal in; + output signal {binary} out[max_nbits]; component aliasCheck = AliasCheck(); - component n2b = Num2Bits(254); + component n2b = Num2Bits(max_nbits); in ==> n2b.in; - for (var i=0; i<254; i++) { - n2b.out[i] ==> out[i]; - n2b.out[i] ==> aliasCheck.in[i]; - } + n2b.out ==> out; + n2b.out ==> aliasCheck.in; } +/* + +*** Bits2Num(n): template that transforms an input of n bits representing a value x in binary into the decimal representation of x + - Inputs: in[n] -> binary representation of out using n bits + requires tag binary + - Output: out -> value represented by the input + satisfies tag maxbit with out.maxbit = n + + Example: Bits2Num(3)([1, 0, 1]) = 5 + +*/ + + template Bits2Num(n) { - signal input in[n]; - signal output out; + input signal {binary} in[n]; + output signal {maxbit} out; var lc1=0; var e2 = 1; @@ -62,28 +153,54 @@ template Bits2Num(n) { lc1 += in[i] * e2; e2 = e2 + e2; } - + out.maxbit = n; lc1 ==> out; } + +/* + +*** Bits2Num_strict(): template that transforms an input of 254 bits representing a value x in binary into the decimal representation of x + - Inputs: in[n] -> binary representation of out using maxbits() + 1 bits + requires tag binary + - Output: out -> value represented by the input + satisfies tag maxbit with out.maxbit = 254 + + Example: Assuming p = 11, then Bits2Num_strict()([1, 1, 0, 1]) = 2 (13 mod 11 = 2) + +*/ + template Bits2Num_strict() { - signal input in[254]; - signal output out; - component aliasCheck = AliasCheck(); - component b2n = Bits2Num(254); + var max_nbits = maxbits(); - for (var i=0; i<254; i++) { - in[i] ==> b2n.in[i]; - in[i] ==> aliasCheck.in[i]; - } + input signal {binary} in[max_nbits]; + output signal {maxbit} out; + component aliasCheck = AliasCheck(); // Maybe remove? + component b2n = Bits2Num(max_nbits); + + in ==> b2n.in; + in ==> aliasCheck.in; + + out.maxbit = max_nbits; b2n.out ==> out; } + +/* +*** Num2BitsNeg(n): template that given an input x returns the binary representation of 2 ** n - x using n bits, in case in == 0 then it returns 0 + - Inputs: in -> field value + - Output: out[n] -> if in != 0 then binary representation of 2 ** n - in using n bits, else 0 + satisfies tag binary + + Example: Num2BitsNeg(3)(2) = [0, 1, 1], Num2Bits(3)(8) = [0, 0, 0] + +*/ + template Num2BitsNeg(n) { - signal input in; - signal output out[n]; + input signal in; + output signal {binary} out[n]; var lc1=0; component isZero; diff --git a/circuits/bits.circom b/circuits/bits.circom new file mode 100644 index 00000000..68edee69 --- /dev/null +++ b/circuits/bits.circom @@ -0,0 +1,18 @@ +/* +*** nbits(x): function that returns the number of bits that we need to represent the value x + - Inputs: x -> field value + - Output: number of bits needed to represent x + + Example: nbits(7) = 3, nbits(10) = 4 + +*/ + +function nbits(a) { + var n = 1; + var r = 0; + while (n-1. */ -pragma circom 2.0.0; +pragma circom 2.1.5; include "bitify.circom"; include "binsum.circom"; +include "gates.circom"; +include "buses.circom"; + +// The templates and functions of this file only work for any prime field + + +/* +*** IsZero(): template that receives an input in representing a field value and returns 1 if the input value is zero, 0 otherwise. + - Inputs: in -> field value + - Outputs: out -> in == 0 + satisfies tag binary + + Example: IsZero()(5) = 0, IsZero()(0) = 0 + +*/ template IsZero() { - signal input in; - signal output out; + input signal in; + output signal {binary} out; signal inv; @@ -34,9 +49,20 @@ template IsZero() { } + +/* +*** IsEqual(): template that receives two inputs in[0] and in[1] representing field values and returns 1 if in[0] == in[1], 0 otherwise. + - Inputs: in[2] -> array of 2 field values + - Outputs: out -> in[0] == in[1] + satisfies tag binary + + Example: IsEqual()([5, 2]) = 0, IsZero()([2, 2]) = 0 + +*/ + template IsEqual() { - signal input in[2]; - signal output out; + input signal in[2]; + output signal {binary} out; component isz = IsZero(); @@ -45,9 +71,21 @@ template IsEqual() { isz.out ==> out; } + +/* +*** ForceEqualIfEnabled(): template that receives two inputs in[0] and in[1] representing field values and checks that in[0] == in[1] in case enabled == 1 + - Inputs: in[2] -> array of 2 field values + enabled -> binary value + requires tag binary + - Outputs: None + + Example: ForceEqualIfEnabled()([5, 2], 1) is not satisfiable as in[0] != in[1] and enabled = 1 + +*/ + template ForceEqualIfEnabled() { - signal input enabled; - signal input in[2]; + input signal {binary} enabled; + input signal in[2]; component isz = IsZero(); @@ -56,40 +94,26 @@ template ForceEqualIfEnabled() { (1 - isz.out)*enabled === 0; } -/* -// N is the number of bits the input have. -// The MSF is the sign bit. -template LessThan(n) { - signal input in[2]; - signal output out; - - component num2Bits0; - component num2Bits1; - - component adder; - - adder = BinSum(n, 2); - - num2Bits0 = Num2Bits(n); - num2Bits1 = Num2BitsNeg(n); - in[0] ==> num2Bits0.in; - in[1] ==> num2Bits1.in; - var i; - for (i=0;i adder.in[0][i]; - num2Bits1.out[i] ==> adder.in[1][i]; - } +/* - adder.out[n-1] ==> out; -} +*** LessThan(n): template that receives two inputs in[0] and in[1] representing field values and returns 1 if in[0] < in[1], 0 otherwise. + - Inputs: in[2] -> array of 2 field values + requires tag maxbit with in.maxbit <= n + - Outputs: out -> in[0] < in[1] + satisfies tag binary + + Example: LessThan()([5, 2]) = 0, LessThan()([1, 2]) = 1 + */ template LessThan(n) { - assert(n <= 252); - signal input in[2]; - signal output out; + assert(n <= maxbits()-2); + input signal {maxbit} in[2]; + output signal {binary} out; + + assert(in.maxbit <= n); component n2b = Num2Bits(n+1); @@ -99,25 +123,51 @@ template LessThan(n) { } +/* -// N is the number of bits the input have. -// The MSF is the sign bit. -template LessEqThan(n) { - signal input in[2]; - signal output out; +*** LessEqThan(n): template that receives two inputs in[0] and in[1] representing field values and returns 1 if in[0] <= in[1], 0 otherwise. + - Inputs: in[2] -> array of 2 field values + requires tag maxbit with in.maxbit <= n + - Outputs: out -> in[0] <= in[1] + satisfies tag binary + + Example: LessEqThan()([5, 2]) = 0, LessEqThan()([2, 2]) = 1 + +*/ - component lt = LessThan(n); +template LessEqThan(n){ + input signal {maxbit} in[2]; + output signal {binary} out; + assert(in.maxbit <= n); + + component gt = GreaterThan(n); + gt.in <== in; + + component nt = NOT(); + nt.in <== gt.out; + nt.out ==> out; - lt.in[0] <== in[0]; - lt.in[1] <== in[1]+1; - lt.out ==> out; } -// N is the number of bits the input have. -// The MSF is the sign bit. + +/* + +*** GreaterThan(n): template that receives two inputs in[0] and in[1] representing field values and returns 1 if in[0] > in[1], 0 otherwise. + - Inputs: in[2] -> array of 2 field values + requires tag maxbit with in.maxbit <= n + - Outputs: out -> in[0] > in[1] + satisfies tag binary + + Example: GreaterThan()([5, 2]) = 1, GreaterThan()([2, 2]) = 0 + +*/ + + template GreaterThan(n) { - signal input in[2]; - signal output out; + input signal {maxbit} in[2]; + output signal {binary} out; + + assert(in.maxbit <= n); component lt = LessThan(n); @@ -126,16 +176,92 @@ template GreaterThan(n) { lt.out ==> out; } -// N is the number of bits the input have. -// The MSF is the sign bit. + + +/* + +*** GreaterEqThan(n): template that receives two inputs in[0] and in[1] representing field values and returns 1 if in[0] >= in[1], 0 otherwise. + - Inputs: in[2] -> array of 2 field values + requires tag maxbit with in.maxbit <= n + - Outputs: out -> in[0] >= in[1] + satisfies tag binary + + Example: GreterEqThan()([5, 2]) = 1, GreaterEqThan()([2, 2]) = 1 + +*/ + template GreaterEqThan(n) { - signal input in[2]; - signal output out; + input signal {maxbit} in[2]; + output signal {binary} out; + + assert(in.maxbit <= n); + + component gt = LessThan(n); + gt.in <== in; + + component nt = NOT(); + nt.in <== gt.out; + nt.out ==> out; +} - component lt = LessThan(n); - lt.in[0] <== in[1]; - lt.in[1] <== in[0]+1; - lt.out ==> out; +/* +*** Sign(): template that receives an input in representing a value in binary using maxbits() bits and checks if the value is positive or negative. We consider a number positive in case in <= p \ 2 and negative otherwise + - Inputs: in[maxbits()] -> array of maxbits() bits + requires tag binary + - Outputs: sign -> 0 in case in <= prime \ 2, 1 otherwise + satisfies tag binary + + +*/ + +template Sign() { + input signal {binary} in[maxbits()]; + output signal {binary} sign; + + component comp = CompConstant(maxbits(), - 1 \ 2); + + var i; + + comp.in <== in; + + sign <== comp.out; } + + +/* +*** CompConstant(n,ct): template that receives an input in representing a value in binary using n bits and checks if its value is greater than the constant value ct given as a parameter. De constant must be representable with n bits. + + - Inputs: in[maxbits()] -> array of maxbits() bits + requires tag binary + - Outputs: out -> binary value, out = in > ct + satisfies tag binary + + Example: CompConstant(10)([0, ..., 0]) = 0, CompConstant(10)([1, ..., 1]) = 1 + +*/ + +template CompConstant(n,ct) { + log(nbits(ct)); + assert(nbits(ct) <= n); + input signal {binary} in[n]; + output signal {binary} out; + + signal {binary} res[n]; + if (ct & 1 == 0) { + res[0] <== in[0]; + } else { + res[0] <== 0; + } + for (var i=1; i < n; i++) { + // re[i-1] says if in[0..i-1] > ct[0..i-1] (upto bit i-1) + if ((ct >> i) & 1 == 0) { + res[i] <== OR()(res[i-1],in[i]); + } else { + res[i] <== AND()(res[i-1],in[i]); + } + } + out <== res[n-1]; +} + diff --git a/circuits/compconstant.circom b/circuits/compconstant.circom deleted file mode 100644 index 1bca83a5..00000000 --- a/circuits/compconstant.circom +++ /dev/null @@ -1,74 +0,0 @@ -/* - 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 "bitify.circom"; - -// Returns 1 if in (in binary) > ct - -template CompConstant(ct) { - signal input in[254]; - signal output out; - - signal parts[127]; - signal sout; - - var clsb; - var cmsb; - var slsb; - var smsb; - - var sum=0; - - var b = (1 << 128) -1; - var a = 1; - var e = 1; - var i; - - for (i=0;i<127; i++) { - clsb = (ct >> (i*2)) & 1; - cmsb = (ct >> (i*2+1)) & 1; - slsb = in[i*2]; - smsb = in[i*2+1]; - - if ((cmsb==0)&&(clsb==0)) { - parts[i] <== -b*smsb*slsb + b*smsb + b*slsb; - } else if ((cmsb==0)&&(clsb==1)) { - parts[i] <== a*smsb*slsb - a*slsb + b*smsb - a*smsb + a; - } else if ((cmsb==1)&&(clsb==0)) { - parts[i] <== b*smsb*slsb - a*smsb + a; - } else { - parts[i] <== -a*smsb*slsb + a; - } - - sum = sum + parts[i]; - - b = b -e; - a = a +e; - e = e*2; - } - - sout <== sum; - - component num2bits = Num2Bits(135); - - num2bits.in <== sout; - - out <== num2bits.out[127]; -} diff --git a/circuits/eddsa.circom b/circuits/eddsa.circom deleted file mode 100644 index 04b5f87c..00000000 --- a/circuits/eddsa.circom +++ /dev/null @@ -1,139 +0,0 @@ -/* - 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 "compconstant.circom"; -include "pointbits.circom"; -include "pedersen.circom"; -include "escalarmulany.circom"; -include "escalarmulfix.circom"; - -template EdDSAVerifier(n) { - signal input msg[n]; - - signal input A[256]; - signal input R8[256]; - signal input S[256]; - - signal Ax; - signal Ay; - - signal R8x; - signal R8y; - - var i; - -// Ensure S compConstant.in[i]; - } - compConstant.out === 0; - S[254] === 0; - S[255] === 0; - -// Convert A to Field elements (And verify A) - - component bits2pointA = Bits2Point_Strict(); - - for (i=0; i<256; i++) { - bits2pointA.in[i] <== A[i]; - } - Ax <== bits2pointA.out[0]; - Ay <== bits2pointA.out[1]; - -// Convert R8 to Field elements (And verify R8) - - component bits2pointR8 = Bits2Point_Strict(); - - for (i=0; i<256; i++) { - bits2pointR8.in[i] <== R8[i]; - } - R8x <== bits2pointR8.out[0]; - R8y <== bits2pointR8.out[1]; - -// Calculate the h = H(R,A, msg) - - component hash = Pedersen(512+n); - - for (i=0; i<256; i++) { - hash.in[i] <== R8[i]; - hash.in[256+i] <== A[i]; - } - for (i=0; i. -*/ -pragma circom 2.0.0; - -include "compconstant.circom"; -include "pointbits.circom"; -include "mimc.circom"; -include "bitify.circom"; -include "escalarmulany.circom"; -include "escalarmulfix.circom"; - -template EdDSAMiMCVerifier() { - signal input enabled; - signal input Ax; - signal input Ay; - - signal input S; - signal input R8x; - signal input R8y; - - signal input M; - - var i; - -// Ensure S compConstant.in[i]; - } - compConstant.in[253] <== 0; - compConstant.out === 0; - -// Calculate the h = H(R,A, msg) - - component hash = MultiMiMC7(5, 91); - hash.in[0] <== R8x; - hash.in[1] <== R8y; - hash.in[2] <== Ax; - hash.in[3] <== Ay; - hash.in[4] <== M; - hash.k <== 0; - - component h2bits = Num2Bits_strict(); - h2bits.in <== hash.out; - -// Calculate second part of the right side: right2 = h*8*A - - // Multiply by 8 by adding it 3 times. This also ensure that the result is in - // the subgroup. - component dbl1 = BabyDbl(); - dbl1.x <== Ax; - dbl1.y <== Ay; - component dbl2 = BabyDbl(); - dbl2.x <== dbl1.xout; - dbl2.y <== dbl1.yout; - component dbl3 = BabyDbl(); - dbl3.x <== dbl2.xout; - dbl3.y <== dbl2.yout; - - // We check that A is not zero. - component isZero = IsZero(); - isZero.in <== dbl3.x; - isZero.out === 0; - - component mulAny = EscalarMulAny(254); - for (i=0; i<254; i++) { - mulAny.e[i] <== h2bits.out[i]; - } - mulAny.p[0] <== dbl3.xout; - mulAny.p[1] <== dbl3.yout; - - -// Compute the right side: right = R8 + right2 - - component addRight = BabyAdd(); - addRight.x1 <== R8x; - addRight.y1 <== R8y; - addRight.x2 <== mulAny.out[0]; - addRight.y2 <== mulAny.out[1]; - -// Calculate left side of equation left = S*B8 - - var BASE8[2] = [ - 5299619240641551281634865583518297030282874472190772894086521144482721001553, - 16950150798460657717958625567821834550301663161624707787222815936182638968203 - ]; - component mulFix = EscalarMulFix(253, BASE8); - for (i=0; i<253; i++) { - mulFix.e[i] <== snum2bits.out[i]; - } - -// Do the comparation left == right if enabled; - - component eqCheckX = ForceEqualIfEnabled(); - eqCheckX.enabled <== enabled; - eqCheckX.in[0] <== mulFix.out[0]; - eqCheckX.in[1] <== addRight.xout; - - component eqCheckY = ForceEqualIfEnabled(); - eqCheckY.enabled <== enabled; - eqCheckY.in[0] <== mulFix.out[1]; - eqCheckY.in[1] <== addRight.yout; -} diff --git a/circuits/eddsamimcsponge.circom b/circuits/eddsamimcsponge.circom deleted file mode 100644 index 3267c455..00000000 --- a/circuits/eddsamimcsponge.circom +++ /dev/null @@ -1,124 +0,0 @@ -/* - 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 "compconstant.circom"; -include "pointbits.circom"; -include "mimcsponge.circom"; -include "bitify.circom"; -include "escalarmulany.circom"; -include "escalarmulfix.circom"; - -template EdDSAMiMCSpongeVerifier() { - signal input enabled; - signal input Ax; - signal input Ay; - - signal input S; - signal input R8x; - signal input R8y; - - signal input M; - - var i; - -// Ensure S compConstant.in[i]; - } - compConstant.in[253] <== 0; - compConstant.out === 0; - -// Calculate the h = H(R,A, msg) - - component hash = MiMCSponge(5, 220, 1); - hash.ins[0] <== R8x; - hash.ins[1] <== R8y; - hash.ins[2] <== Ax; - hash.ins[3] <== Ay; - hash.ins[4] <== M; - hash.k <== 0; - - component h2bits = Num2Bits_strict(); - h2bits.in <== hash.outs[0]; - -// Calculate second part of the right side: right2 = h*8*A - - // Multiply by 8 by adding it 3 times. This also ensure that the result is in - // the subgroup. - component dbl1 = BabyDbl(); - dbl1.x <== Ax; - dbl1.y <== Ay; - component dbl2 = BabyDbl(); - dbl2.x <== dbl1.xout; - dbl2.y <== dbl1.yout; - component dbl3 = BabyDbl(); - dbl3.x <== dbl2.xout; - dbl3.y <== dbl2.yout; - - // We check that A is not zero. - component isZero = IsZero(); - isZero.in <== dbl3.x; - isZero.out === 0; - - component mulAny = EscalarMulAny(254); - for (i=0; i<254; i++) { - mulAny.e[i] <== h2bits.out[i]; - } - mulAny.p[0] <== dbl3.xout; - mulAny.p[1] <== dbl3.yout; - - -// Compute the right side: right = R8 + right2 - - component addRight = BabyAdd(); - addRight.x1 <== R8x; - addRight.y1 <== R8y; - addRight.x2 <== mulAny.out[0]; - addRight.y2 <== mulAny.out[1]; - -// Calculate left side of equation left = S*B8 - - var BASE8[2] = [ - 5299619240641551281634865583518297030282874472190772894086521144482721001553, - 16950150798460657717958625567821834550301663161624707787222815936182638968203 - ]; - component mulFix = EscalarMulFix(253, BASE8); - for (i=0; i<253; i++) { - mulFix.e[i] <== snum2bits.out[i]; - } - -// Do the comparation left == right if enabled; - - component eqCheckX = ForceEqualIfEnabled(); - eqCheckX.enabled <== enabled; - eqCheckX.in[0] <== mulFix.out[0]; - eqCheckX.in[1] <== addRight.xout; - - component eqCheckY = ForceEqualIfEnabled(); - eqCheckY.enabled <== enabled; - eqCheckY.in[0] <== mulFix.out[1]; - eqCheckY.in[1] <== addRight.yout; -} diff --git a/circuits/eddsapedersen.circom b/circuits/eddsapedersen.circom new file mode 100644 index 00000000..f7f3fe04 --- /dev/null +++ b/circuits/eddsapedersen.circom @@ -0,0 +1,140 @@ +/* + 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.5; + +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) + +include "comparators.circom"; +include "pointbits.circom"; +include "pedersen.circom"; +include "escalarmul/escalarmulany.circom"; +include "escalarmul/escalarmulfix.circom"; + +/* + +*** EdDSAPedersenVerifier(n): template that implements the EdDSA verification protocol based on Pedersen hash for a message of size n. The circuit receives the message that we want to verify and the public and private keys (that are points of a curve in Edwards representation encoded using 256 bits) and checks if the message is correct. + - Inputs: msg[n] -> msg encoded in bits + requires tag binary + A[256] -> encoding of a point of a curve in Edwards representation using 256 bits + requires tag binary + R8[256] -> encoding of a point of a curve in Edwards representation using 256 bits + requires tag binary + S[256] -> value of the subgroup generated by the prime 2736030358979909402780800718157159386076813972158567259200215660948447373041 + requires tag binary + - Outputs: None +*/ + + +template EdDSAPedersenVerifier(n) { + input signal {binary} msg[n]; + + input BinaryPoint(254) A; + input BinaryPoint(254) R8; + input BinaryPoint(254) S; + + Point pA; + Point pR8; + + + var i; + +// Ensure S compConstant.in; + compConstant.out === 0; + S.signX === 0; + +// Convert A to Field elements (And verify A) + pA <== Bits2Point_Strict()(A); + + +// Convert R8 to Field elements (And verify R8) + pR8 <== Bits2Point_Strict()(R8); + +// Calculate the h = H(R,A, msg) + + component hash = Pedersen(510+n); + + for (i=0; i<254; i++) { + hash.in[i] <== R8.binY[i]; + } + hash.in[254] <== R8.signX; + + for (i=0; i<254; i++) { + hash.in[255 + i] <== A.binY[i]; + } + hash.in[509] <== A.signX; + + for (i=0; i. +*/ + +pragma circom 2.1.5; + +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) + +include "comparators.circom"; +include "pointbits.circom"; +include "pedersen.circom"; +include "escalarmul/escalarmulany.circom"; +include "escalarmul/escalarmulfix.circom"; + +/* + +*** EdDSAPedersenVerifier(n): template that implements the EdDSA verification protocol based on Pedersen hash for a message of size n. The circuit receives the message that we want to verify and the public and private keys (that are points of a curve in Edwards representation encoded using 256 bits) and checks if the message is correct. + - Inputs: msg[n] -> msg encoded in bits + requires tag binary + A[256] -> encoding of a point of a curve in Edwards representation using 256 bits + requires tag binary + R8[256] -> encoding of a point of a curve in Edwards representation using 256 bits + requires tag binary + S[256] -> value of the subgroup generated by the prime 2736030358979909402780800718157159386076813972158567259200215660948447373041 + requires tag binary + - Outputs: None +*/ + + +template EdDSAPedersenVerifier(n) { + input signal {binary} msg[n]; + + input BinaryPoint(254) A; + input BinaryPoint(254) R8; + input BinaryPoint(254) S; + + Point pA; + Point pR8; + + signal {binary} aux_0 <== 0; + + var i; + +// Ensure S compConstant.in; + compConstant.out === 0; + S.signX === 0; + +// Convert A to Field elements (And verify A) + pA <== Bits2Point_Strict()(A); + + +// Convert R8 to Field elements (And verify R8) + pR8 <== Bits2Point_Strict()(R8); + +// Calculate the h = H(R,A, msg) + + component hash = Pedersen(512+n); + + for (i=0; i<254; i++) { + hash.in[i] <== R8.binY[i]; + } + hash.in[254] <== aux_0; + hash.in[255] <== R8.signX; + + for (i=0; i<254; i++) { + hash.in[256 + i] <== A.binY[i]; + } + hash.in[256 + 254] <== aux_0; + hash.in[256 + 255] <== A.signX; + + for (i=0; i. */ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "compconstant.circom"; +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) + +include "comparators.circom"; include "poseidon.circom"; include "bitify.circom"; -include "escalarmulany.circom"; -include "escalarmulfix.circom"; +include "escalarmul/escalarmulany.circom"; +include "escalarmul/escalarmulfix.circom"; +include "buses.circom"; + +/* + +*** EdDSAPoseidonVerifier(): template that implements the EdDSA verification protocol based on poseidon hash. The circuit receives the message that we want to verify and the public and private keys (that are points of a curve in Edwards representation) and checks if the message is correct. + - Inputs: msg -> field value + enabled -> bit indicating if the verification is enabled or not + requires tag binary + Ax -> x coodinate of the curve point A that is in Edwards representation + Ay -> y coodinate of the curve point A that is in Edwards representation + S -> value of the subgroup generated by the prime 2736030358979909402780800718157159386076813972158567259200215660948447373041 + R8x -> x coodinate of the curve point R8 that is in Edwards representation + R8y -> y coodinate of the curve point R8 that is in Edwards representation + - Outputs: None +*/ + template EdDSAPoseidonVerifier() { - signal input enabled; - signal input Ax; - signal input Ay; + input signal {binary} enabled; + input Point {babyedwards} A; - signal input S; - signal input R8x; - signal input R8y; + input signal S; + input Point {babyedwards} R8; - signal input M; + input signal M; var i; @@ -42,22 +58,24 @@ template EdDSAPoseidonVerifier() { component snum2bits = Num2Bits(253); snum2bits.in <== S; - component compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040); + component compConstant = CompConstant(maxbits(), 2736030358979909402780800718157159386076813972158567259200215660948447373040); for (i=0; i<253; i++) { snum2bits.out[i] ==> compConstant.in[i]; } - compConstant.in[253] <== 0; + + signal {binary} aux_0 <== 0; + compConstant.in[253] <== aux_0; compConstant.out*enabled === 0; // Calculate the h = H(R,A, msg) component hash = Poseidon(5); - hash.inputs[0] <== R8x; - hash.inputs[1] <== R8y; - hash.inputs[2] <== Ax; - hash.inputs[3] <== Ay; + hash.inputs[0] <== R8.x; + hash.inputs[1] <== R8.y; + hash.inputs[2] <== A.x; + hash.inputs[3] <== A.y; hash.inputs[4] <== M; component h2bits = Num2Bits_strict(); @@ -68,35 +86,27 @@ template EdDSAPoseidonVerifier() { // Multiply by 8 by adding it 3 times. This also ensure that the result is in // the subgroup. component dbl1 = BabyDbl(); - dbl1.x <== Ax; - dbl1.y <== Ay; + dbl1.pin <== A; component dbl2 = BabyDbl(); - dbl2.x <== dbl1.xout; - dbl2.y <== dbl1.yout; + dbl2.pin <== dbl1.pout; component dbl3 = BabyDbl(); - dbl3.x <== dbl2.xout; - dbl3.y <== dbl2.yout; + dbl3.pin <== dbl2.pout; // We check that A is not zero. component isZero = IsZero(); - isZero.in <== dbl3.x; + isZero.in <== dbl3.pin.x; isZero.out*enabled === 0; component mulAny = EscalarMulAny(254); - for (i=0; i<254; i++) { - mulAny.e[i] <== h2bits.out[i]; - } - mulAny.p[0] <== dbl3.xout; - mulAny.p[1] <== dbl3.yout; + mulAny.e <== h2bits.out; + mulAny.pin <== dbl3.pout; // Compute the right side: right = R8 + right2 component addRight = BabyAdd(); - addRight.x1 <== R8x; - addRight.y1 <== R8y; - addRight.x2 <== mulAny.out[0]; - addRight.y2 <== mulAny.out[1]; + addRight.pin1 <== R8; + addRight.pin2 <== mulAny.pout; // Calculate left side of equation left = S*B8 @@ -105,19 +115,17 @@ template EdDSAPoseidonVerifier() { 16950150798460657717958625567821834550301663161624707787222815936182638968203 ]; component mulFix = EscalarMulFix(253, BASE8); - for (i=0; i<253; i++) { - mulFix.e[i] <== snum2bits.out[i]; - } + mulFix.e <== snum2bits.out; // Do the comparation left == right if enabled; component eqCheckX = ForceEqualIfEnabled(); eqCheckX.enabled <== enabled; - eqCheckX.in[0] <== mulFix.out[0]; - eqCheckX.in[1] <== addRight.xout; + eqCheckX.in[0] <== mulFix.pout.x; + eqCheckX.in[1] <== addRight.pout.x; component eqCheckY = ForceEqualIfEnabled(); eqCheckY.enabled <== enabled; - eqCheckY.in[0] <== mulFix.out[1]; - eqCheckY.in[1] <== addRight.yout; + eqCheckY.in[0] <== mulFix.pout.y; + eqCheckY.in[1] <== addRight.pout.y; } diff --git a/circuits/escalarmul.circom b/circuits/escalarmul/escalarmul.circom similarity index 77% rename from circuits/escalarmul.circom rename to circuits/escalarmul/escalarmul.circom index 809d9957..b0807c37 100644 --- a/circuits/escalarmul.circom +++ b/circuits/escalarmul/escalarmul.circom @@ -16,9 +16,27 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ + +pragma circom 2.1.5; + +include "../mux4.circom"; +include "escalarmulw4table.circom"; +include "../babyjub.circom"; +include "../buses.circom"; -/* +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. + + +/* +*** EscalarMulWindow(base, k): template that receives two inputs in[2] and a sel[4] representing a value of the prime field and a binary value respectively, and returns the point out according to the scheme below. This circuit is used in order to multiply a curve of the BabyJub curve by a escalar (val * base with base in the curve). The parameter k indicates the number of window in the protocol + - Inputs: in[2] -> field values + sel[4] -> binary values + requires tag binary + - Outputs: out[2] -> field values + + Scheme: ┏━━━━━━━━━━━┓ ┃ ┃ ┃ ┃ @@ -60,17 +78,12 @@ */ -pragma circom 2.0.0; - -include "mux4.circom"; -include "escalarmulw4table.circom"; -include "babyjub.circom"; template EscalarMulWindow(base, k) { - signal input in[2]; - signal input sel[4]; - signal output out[2]; + input Point {babyedwards} pin; + input signal {binary} sel[4]; + output Point {babyedwards} pout; var table[16][2]; component mux; @@ -82,27 +95,34 @@ template EscalarMulWindow(base, k) { mux = MultiMux4(2); adder = BabyAdd(); - for (i=0; i<4; i++) { - sel[i] ==> mux.s[i]; - } + sel ==> mux.s; for (i=0; i<16; i++) { mux.c[0][i] <== table[i][0]; mux.c[1][i] <== table[i][1]; } - in[0] ==> adder.x1; - in[1] ==> adder.y1; + pin ==> adder.pin1; + Point {babyedwards} aux; + aux.x <== mux.out[0]; + aux.y <== mux.out[1]; + aux ==> adder.pin2; + + adder.pout ==> pout; +} + - mux.out[0] ==> adder.x2; - mux.out[1] ==> adder.y2; - adder.xout ==> out[0]; - adder.yout ==> out[1]; -} /* +*** EscalarMul(n, base): template that receives two inputs inp[2] and in[n] representing a point of BabyJub curve in its Edwards representation and the binary representation of a field value k respectively, and returns the value out according to the scheme below. This circuit is used in order to multiply a point of the BabyJub curve by a escalar (k * inp with inp in the curve). The input in is the binary representation of the value k and in is the point of the curve. + - Inputs: in[n] -> binary representation of k + requires tag binary + inp[2] -> input curve point to be multiplied + - Outputs: out[2] -> output curve point k * inp + + Scheme: ┏━━━━━━━━━┓ ┏━━━━━━━━━┓ ┏━━━━━━━━━━━━━━━━━━━┓ ┃ ┃ ┃ ┃ ┃ ┃ @@ -126,14 +146,15 @@ template EscalarMulWindow(base, k) { */ template EscalarMul(n, base) { - signal input in[n]; - signal input inp[2]; // Point input to be added - signal output out[2]; + input signal {binary} in[n]; + input Point {babyedwards} pin; // Point input to be added + output Point {babyedwards} pout; var nBlocks = ((n-1)>>2)+1; var i; var j; + signal {binary} aux_0 <== 0; component windows[nBlocks]; // Construct the windows @@ -145,7 +166,7 @@ template EscalarMul(n, base) { for (i=0; i= n) { - windows[i].sel[j] <== 0; + windows[i].sel[j] <== aux_0; } else { windows[i].sel[j] <== in[i*4+j]; } @@ -153,14 +174,11 @@ template EscalarMul(n, base) { } // Start with generator - windows[0].in[0] <== inp[0]; - windows[0].in[1] <== inp[1]; + windows[0].pin <== pin; for(i=0; i windows[i+1].in[0]; - windows[i].out[1] ==> windows[i+1].in[1]; + windows[i].pout ==> windows[i+1].pin; } - windows[nBlocks-1].out[0] ==> out[0]; - windows[nBlocks-1].out[1] ==> out[1]; + windows[nBlocks-1].pout ==> pout; } diff --git a/circuits/escalarmul/escalarmulany.circom b/circuits/escalarmul/escalarmulany.circom new file mode 100644 index 00000000..0fee72c6 --- /dev/null +++ b/circuits/escalarmul/escalarmulany.circom @@ -0,0 +1,243 @@ +/* + 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.5; + +include "../montgomery.circom"; +include "../babyjub.circom"; +include "../comparators.circom"; +include "../buses.circom"; + +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. + + +/* + +*** Multiplexor2(): template that implements a multiplexer 2-to-1 between two inputs of 2 elements + - If s == 0 then out = in[0] + - If s == 1 then out = in[1] + + - Inputs: sel -> binary value, selector + requires tag binary + in[2][2] -> two arrays of 2 elements that correspond to the inputs of the mux: in[0] => first input, in[1] => second input + - Output: out[2] -> array of 2 elements, it takes the value in[0] if sel == 0, in[1] if sel == 1 + + */ + +template MultiplexorEdwards2() { + input signal {binary} sel; + input Point {babyedwards} pin[2]; + output Point {babyedwards} pout; + + pout.x <== (pin[1].x - pin[0].x)*sel + pin[0].x; + pout.y <== (pin[1].y - pin[0].y)*sel + pin[0].y; +} + +template MultiplexorMontgomery2() { + input signal {binary} sel; + input Point {babymontgomery} pin[2]; + output Point {babymontgomery} pout; + + pout.x <== (pin[1].x - pin[0].x)*sel + pin[0].x; + pout.y <== (pin[1].y - pin[0].y)*sel + pin[0].y; +} + + +/* + +*** BitElementMulAny(): template that receives three inputs: sel representing a bit, and two points of the elliptic curve in Montgomery form dblIn and addIn, and returns the points in Montgomery form dblOut and addOut according to the scheme below. This circuit is used in order to multiply a point of the BabyJub curve by a escalar (k * p with p in the curve). + - Inputs: sel -> binary value + requires tag binary + dblIn[2] -> input curve point in Montgomery representation + addIn[2] -> input curve point in Montgomery representation + - Outputs: dblOut[2] -> output curve point in Montgomery representation + addOut[2] -> output curve point in Montgomery representation + + +*** dblOut = 2 * dblIn; +*** addOut = + -- If sel == 0: addIn; + -- If sel == 1: 2 * dblIn + addIn; + +*/ + +template BitElementMulAny() { + input signal {binary} sel; + input Point {babymontgomery} dblIn; + input Point {babymontgomery} addIn; + output Point {babymontgomery} dblOut; + output Point {babymontgomery} addOut; + + component doubler = MontgomeryDouble(); + component adder = MontgomeryAdd(); + component selector = MultiplexorMontgomery2(); + + + sel ==> selector.sel; + + dblIn ==> doubler.pin; + doubler.pout ==> adder.pin1; + addIn ==> adder.pin2; + addIn ==> selector.pin[0]; + adder.pout ==> selector.pin[1]; + + + doubler.pout ==> dblOut; + selector.pout ==> addOut; + +} + +/* + +*** SegmentMulAny(n): template that receives two inputs p[2] and e[n] representing a point of BabyJub curve in its Edwards representation and the binary representation of a field value k respectively, and returns the value out according to the scheme below. This circuit is used in order to multiply a point of the BabyJub curve by a escalar (k * p with p in the curve). + - Inputs: e[n] -> binary representation of k + requires tag binary + p[2] -> input curve point in Edwards representation + - Outputs: out[2] -> output curve point in Edwards representation + +TODO: ADD SCHEME + +*/ + +template SegmentMulAny(n) { + input signal {binary} e[n]; + input Point {babyedwards} pin; + output Point {babyedwards} pout; + output Point {babymontgomery} dbl; + + component bits[n-1]; + + component e2m = Edwards2Montgomery(); + + pin ==> e2m.pin; + + var i; + + bits[0] = BitElementMulAny(); + e2m.pout ==> bits[0].dblIn; + e2m.pout ==> bits[0].addIn; + e[1] ==> bits[0].sel; + + for (i=1; i bits[i].dblIn; + bits[i-1].addOut ==> bits[i].addIn; + e[i+1] ==> bits[i].sel; + } + + bits[n-2].dblOut ==> dbl; + + component m2e = Montgomery2Edwards(); + + bits[n-2].addOut ==> m2e.pin; + + component eadder = BabyAdd(); + + m2e.pout ==> eadder.pin1; + Point {babyedwards} inv_pin; + inv_pin.x <== -pin.x; + inv_pin.y <== pin.y; + inv_pin ==> eadder.pin2; + + component lastSel = MultiplexorEdwards2(); + + e[0] ==> lastSel.sel; + eadder.pout ==> lastSel.pin[0]; + m2e.pout ==> lastSel.pin[1]; + + lastSel.pout ==> pout; +} + +/* + +*** EscalarMulAny(n): template that receives two inputs p[2] and e[n] representing a point of BabyJub curve in its Edwards representation and the binary representation of a field value k respectively, and returns the value out according to the scheme below. This circuit is used in order to multiply a point of the BabyJub curve by a escalar (k * p with p in the curve). The input e is the binary representation of the value k and p is the point of the curve. + - Inputs: e[n] -> binary representation of k + requires tag binary + p[2] -> input curve point to be multiplied in Edwards representation + - Outputs: out[2] -> output curve point k * p in Edwards representation + + Note: This function assumes that p is in the subgroup and it is different to 0 + +TODO: ADD SCHEME + +*/ + +template EscalarMulAny(n) { + input signal {binary} e[n]; // Input in binary format + input Point {babyedwards} pin; // Point (Twisted format) + output Point {babyedwards} pout; // 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 <== pin.x; + + var s; + var i; + var nseg; + + Point {babyedwards} aux; + + for (s=0; s segments[s].e[i]; + } + + if (s==0) { + // force G8 point if input point is zero + aux.x <== pin.x + (5299619240641551281634865583518297030282874472190772894086521144482721001553 - pin.x)*zeropoint.out; + aux.y <== pin.y + (16950150798460657717958625567821834550301663161624707787222815936182638968203 - pin.y)*zeropoint.out; + segments[s].pin <== aux; + } else { + doublers[s-1] = MontgomeryDouble(); + m2e[s-1] = Montgomery2Edwards(); + adders[s-1] = BabyAdd(); + + segments[s-1].dbl ==> doublers[s-1].pin; + doublers[s-1].pout ==> m2e[s-1].pin; + m2e[s-1].pout ==> segments[s].pin; + + if (s==1) { + segments[s-1].pout ==> adders[s-1].pin1; + } else { + adders[s-2].pout ==> adders[s-1].pin1; + } + segments[s].pout ==> adders[s-1].pin2; + } + } + + if (nsegments == 1) { + segments[0].pout.x*(1-zeropoint.out) ==> pout.x; + segments[0].pout.y+(1-segments[0].pout.y)*zeropoint.out ==> pout.y; + } else { + adders[nsegments-2].pout.x*(1-zeropoint.out) ==> pout.x; + adders[nsegments-2].pout.y+(1-adders[nsegments-2].pout.y)*zeropoint.out ==> pout.y; + } +} diff --git a/circuits/escalarmul/escalarmulfix.circom b/circuits/escalarmul/escalarmulfix.circom new file mode 100644 index 00000000..ebe6e6c1 --- /dev/null +++ b/circuits/escalarmul/escalarmulfix.circom @@ -0,0 +1,290 @@ +/* + 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.5; + +include "../mux3.circom"; +include "../montgomery.circom"; +include "../babyjub.circom"; +include "../buses.circom"; + + +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. + +/* + + The scalar is s = a0 + a1*2^3 + a2*2^6 + ...... + a81*2^243 + First We calculate Q = B + 2^3*B + 2^6*B + ......... + 2^246*B + + Then we calculate S1 = 2*2^246*B + (1 + a0)*B + (2^3 + a1)*B + .....+ (2^243 + a81)*B + + And Finaly we compute the result: RES = SQ - Q + + As you can see the input of the adders cannot be equal nor zero, except for the last + substraction that it's done in montgomery. + + A good way to see it is that the accumulator input of the adder >= 2^247*B and the other input + is the output of the windows that it's going to be <= 2^246*B + */ + + +/* + +*** WindowMulFix(): template that given a point in Montgomery representation base and a binary input in, calculates: + out = base + base*in[0] + 2*base*in[1] + 4*base*in[2] + out8 = 8*base + + This circuit is used in order to multiply a fixed point of the BabyJub curve by a escalar (k * p with p a fixed point of the curve). + - Inputs: in[3] -> binary value + requires tag binary + base[2] -> input curve point in Montgomery representation + - Outputs: out[2] -> output curve point in Montgomery representation + out8[2] -> output curve point in Montgomery representation + + */ + +template WindowMulFix() { + input signal {binary} in[3]; + input Point {babymontgomery} base; + output Point {babymontgomery} pout; + output Point {babymontgomery} pout8; // Returns 8*Base (To be linked) + + component mux = MultiMux3(2); + + mux.s[0] <== in[0]; + mux.s[1] <== in[1]; + mux.s[2] <== in[2]; + + component dbl2 = MontgomeryDouble(); + component adr3 = MontgomeryAdd(); + component adr4 = MontgomeryAdd(); + component adr5 = MontgomeryAdd(); + component adr6 = MontgomeryAdd(); + component adr7 = MontgomeryAdd(); + component adr8 = MontgomeryAdd(); + +// in[0] -> 1*BASE + + mux.c[0][0] <== base.x; + mux.c[1][0] <== base.y; + +// in[1] -> 2*BASE + dbl2.pin <== base; + mux.c[0][1] <== dbl2.pout.x; + mux.c[1][1] <== dbl2.pout.y; + +// in[2] -> 3*BASE + adr3.pin1 <== base; + adr3.pin2 <== dbl2.pout; + mux.c[0][2] <== adr3.pout.x; + mux.c[1][2] <== adr3.pout.y; + +// in[3] -> 4*BASE + adr4.pin1 <== base; + adr4.pin2 <== adr3.pout; + mux.c[0][3] <== adr4.pout.x; + mux.c[1][3] <== adr4.pout.y; + +// in[4] -> 5*BASE + adr5.pin1 <== base; + adr5.pin2 <== adr4.pout; + mux.c[0][4] <== adr5.pout.x; + mux.c[1][4] <== adr5.pout.y; + +// in[5] -> 6*BASE + adr6.pin1 <== base; + adr6.pin2 <== adr5.pout; + mux.c[0][5] <== adr6.pout.x; + mux.c[1][5] <== adr6.pout.y; + +// in[6] -> 7*BASE + adr7.pin1 <== base; + adr7.pin2 <== adr6.pout; + mux.c[0][6] <== adr7.pout.x; + mux.c[1][6] <== adr7.pout.y; + +// in[7] -> 8*BASE + adr8.pin1 <== base; + adr8.pin2 <== adr7.pout; + mux.c[0][7] <== adr8.pout.x; + mux.c[1][7] <== adr8.pout.y; + + pout8 <== adr8.pout; + + pout.x <== mux.out[0]; + pout.y <== mux.out[1]; +} + + +/* + +*** SegmentMulFix(nWindows): template used to perform a segment of the multiplications needed to perform a multiplication of a scalar times a fix base (k * BASE). + - Inputs: e[3 * nWindows] -> binary representation of the scalar + requires tag binary + base[2] -> input curve point in Edwards representation + - Outputs: out[2] -> output curve point in Edwards representation + dbl[2] -> output curve point in Montgomery representation (to be linked to the next segment) + + */ + +template SegmentMulFix(nWindows) { + input signal {binary} e[nWindows*3]; + input Point {babyedwards} base; + output Point {babyedwards} pout; + output Point {babymontgomery} dbl; + + var i; + var j; + + // Convert the base to montgomery + + component e2m = Edwards2Montgomery(); + e2m.pin <== base; + + component windows[nWindows]; + component adders[nWindows]; + component cadders[nWindows]; + + // In the last step we add an extra doubler so that numbers do not match. + component dblLast = MontgomeryDouble(); + + for (i=0; i pout; + + windows[nWindows-1].pout8 ==> dbl; +} + + +/* + +*** EscalarMulFix(n, BASE): template that does a multiplication of a scalar times a fixed point BASE. It receives a point in Edwards representation BASE and a binary input e representing a value k using n bits, and calculates the point k * p. + - Inputs: e[n] -> binary representation of the scalar k + requires tag binary + - Outputs: out[2] -> output curve point in Edwards representation out = k * BASE + + */ + + +template EscalarMulFix(n, BASE) { + input signal {binary} e[n]; // Input in binary format + output Point {babyedwards} pout; // Point (Twisted format) + + var nsegments = (n-1)\246 +1; // 249 probably would work. But I'm not sure and for security I keep 246 + var nlastsegment = n - (nsegments-1)*249; + + component segments[nsegments]; + + component m2e[nsegments-1]; + component adders[nsegments-1]; + + Point {babyedwards} aux_base; + aux_base.x <== BASE[0]; + aux_base.y <== BASE[1]; + + var s; + var i; + var nseg; + var nWindows; + + signal {binary} aux_0 <== 0; + + for (s=0; s m2e[s-1].pin; + + m2e[s-1].pout ==> segments[s].base; + + if (s==1) { + segments[s-1].pout ==> adders[s-1].pin1; + } else { + adders[s-2].pout ==> adders[s-1].pin1; + } + segments[s].pout ==> adders[s-1].pin2; + } + } + + if (nsegments == 1) { + segments[0].pout ==> pout; + } else { + adders[nsegments-2].pout ==> pout; + } +} diff --git a/circuits/escalarmulw4table.circom b/circuits/escalarmul/escalarmulw4table.circom similarity index 86% rename from circuits/escalarmulw4table.circom rename to circuits/escalarmul/escalarmulw4table.circom index 25c095af..497b1929 100644 --- a/circuits/escalarmulw4table.circom +++ b/circuits/escalarmul/escalarmulw4table.circom @@ -16,7 +16,11 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; + +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. + function pointAdd(x1,y1,x2,y2) { var a = 168700; diff --git a/circuits/escalarmulany.circom b/circuits/escalarmulany.circom deleted file mode 100644 index f07fe7d5..00000000 --- a/circuits/escalarmulany.circom +++ /dev/null @@ -1,197 +0,0 @@ -/* - 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 "montgomery.circom"; -include "babyjub.circom"; -include "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 = BabyAdd(); - - 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] + (5299619240641551281634865583518297030282874472190772894086521144482721001553 - p[0])*zeropoint.out; - segments[s].p[1] <== p[1] + (16950150798460657717958625567821834550301663161624707787222815936182638968203 - p[1])*zeropoint.out; - } else { - doublers[s-1] = MontgomeryDouble(); - m2e[s-1] = Montgomery2Edwards(); - adders[s-1] = BabyAdd(); - - 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/circuits/escalarmulfix.circom b/circuits/escalarmulfix.circom deleted file mode 100644 index 4669d36f..00000000 --- a/circuits/escalarmulfix.circom +++ /dev/null @@ -1,299 +0,0 @@ -/* - 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 "mux3.circom"; -include "montgomery.circom"; -include "babyjub.circom"; - -/* - Window of 3 elements, it calculates - out = base + base*in[0] + 2*base*in[1] + 4*base*in[2] - out4 = 4*base - - The result should be compensated. - */ - -/* - - The scalar is s = a0 + a1*2^3 + a2*2^6 + ...... + a81*2^243 - First We calculate Q = B + 2^3*B + 2^6*B + ......... + 2^246*B - - Then we calculate S1 = 2*2^246*B + (1 + a0)*B + (2^3 + a1)*B + .....+ (2^243 + a81)*B - - And Finaly we compute the result: RES = SQ - Q - - As you can see the input of the adders cannot be equal nor zero, except for the last - substraction that it's done in montgomery. - - A good way to see it is that the accumulator input of the adder >= 2^247*B and the other input - is the output of the windows that it's going to be <= 2^246*B - */ -template WindowMulFix() { - signal input in[3]; - signal input base[2]; - signal output out[2]; - signal output out8[2]; // Returns 8*Base (To be linked) - - component mux = MultiMux3(2); - - mux.s[0] <== in[0]; - mux.s[1] <== in[1]; - mux.s[2] <== in[2]; - - component dbl2 = MontgomeryDouble(); - component adr3 = MontgomeryAdd(); - component adr4 = MontgomeryAdd(); - component adr5 = MontgomeryAdd(); - component adr6 = MontgomeryAdd(); - component adr7 = MontgomeryAdd(); - component adr8 = MontgomeryAdd(); - -// in[0] -> 1*BASE - - mux.c[0][0] <== base[0]; - mux.c[1][0] <== base[1]; - -// in[1] -> 2*BASE - dbl2.in[0] <== base[0]; - dbl2.in[1] <== base[1]; - mux.c[0][1] <== dbl2.out[0]; - mux.c[1][1] <== dbl2.out[1]; - -// in[2] -> 3*BASE - adr3.in1[0] <== base[0]; - adr3.in1[1] <== base[1]; - adr3.in2[0] <== dbl2.out[0]; - adr3.in2[1] <== dbl2.out[1]; - mux.c[0][2] <== adr3.out[0]; - mux.c[1][2] <== adr3.out[1]; - -// in[3] -> 4*BASE - adr4.in1[0] <== base[0]; - adr4.in1[1] <== base[1]; - adr4.in2[0] <== adr3.out[0]; - adr4.in2[1] <== adr3.out[1]; - mux.c[0][3] <== adr4.out[0]; - mux.c[1][3] <== adr4.out[1]; - -// in[4] -> 5*BASE - adr5.in1[0] <== base[0]; - adr5.in1[1] <== base[1]; - adr5.in2[0] <== adr4.out[0]; - adr5.in2[1] <== adr4.out[1]; - mux.c[0][4] <== adr5.out[0]; - mux.c[1][4] <== adr5.out[1]; - -// in[5] -> 6*BASE - adr6.in1[0] <== base[0]; - adr6.in1[1] <== base[1]; - adr6.in2[0] <== adr5.out[0]; - adr6.in2[1] <== adr5.out[1]; - mux.c[0][5] <== adr6.out[0]; - mux.c[1][5] <== adr6.out[1]; - -// in[6] -> 7*BASE - adr7.in1[0] <== base[0]; - adr7.in1[1] <== base[1]; - adr7.in2[0] <== adr6.out[0]; - adr7.in2[1] <== adr6.out[1]; - mux.c[0][6] <== adr7.out[0]; - mux.c[1][6] <== adr7.out[1]; - -// in[7] -> 8*BASE - adr8.in1[0] <== base[0]; - adr8.in1[1] <== base[1]; - adr8.in2[0] <== adr7.out[0]; - adr8.in2[1] <== adr7.out[1]; - mux.c[0][7] <== adr8.out[0]; - mux.c[1][7] <== adr8.out[1]; - - out8[0] <== adr8.out[0]; - out8[1] <== adr8.out[1]; - - out[0] <== mux.out[0]; - out[1] <== mux.out[1]; -} - - -/* - This component does a multiplication of a escalar times a fix base - Signals: - e: The scalar in bits - base: the base point in edwards format - out: The result - dbl: Point in Edwards to be linked to the next segment. - */ - -template SegmentMulFix(nWindows) { - signal input e[nWindows*3]; - signal input base[2]; - signal output out[2]; - signal output dbl[2]; - - var i; - var j; - - // Convert the base to montgomery - - component e2m = Edwards2Montgomery(); - e2m.in[0] <== base[0]; - e2m.in[1] <== base[1]; - - component windows[nWindows]; - component adders[nWindows]; - component cadders[nWindows]; - - // In the last step we add an extra doubler so that numbers do not match. - component dblLast = MontgomeryDouble(); - - for (i=0; i out[0]; - cAdd.yout ==> out[1]; - - windows[nWindows-1].out8[0] ==> dbl[0]; - windows[nWindows-1].out8[1] ==> dbl[1]; -} - - -/* -This component multiplies a escalar times a fixed point BASE (twisted edwards format) - Signals - e: The escalar in binary format - out: The output point in twisted edwards - */ -template EscalarMulFix(n, BASE) { - signal input e[n]; // Input in binary format - signal output out[2]; // Point (Twisted format) - - var nsegments = (n-1)\246 +1; // 249 probably would work. But I'm not sure and for security I keep 246 - var nlastsegment = n - (nsegments-1)*249; - - component segments[nsegments]; - - component m2e[nsegments-1]; - component adders[nsegments-1]; - - var s; - var i; - var nseg; - var nWindows; - - for (s=0; s m2e[s-1].in[0]; - segments[s-1].dbl[1] ==> m2e[s-1].in[1]; - - m2e[s-1].out[0] ==> segments[s].base[0]; - m2e[s-1].out[1] ==> segments[s].base[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] ==> out[0]; - segments[0].out[1] ==> out[1]; - } else { - adders[nsegments-2].xout ==> out[0]; - adders[nsegments-2].yout ==> out[1]; - } -} diff --git a/circuits/gates.circom b/circuits/gates.circom index 374353e9..1bd79b11 100644 --- a/circuits/gates.circom +++ b/circuits/gates.circom @@ -16,58 +16,144 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; + +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + +/* +*** XOR(): template that given two inputs a and b representing booleans (0 or 1) returns the value of a XOR b + - Inputs: a -> binary value + requires tag binary + b -> binary value + requires tag binary + - Output: out -> binary value, result of a XOR b + satisfies tag binary + + Example: XOR()(1, 1) = 0 +*/ template XOR() { - signal input a; - signal input b; - signal output out; + input signal {binary} a; + input signal {binary} b; + output signal {binary} out; out <== a + b - 2*a*b; } +/* +*** AND(): template that given two inputs a and b representing booleans (0 or 1) returns the value of a AND b + - Inputs: a -> binary value + requires tag binary + b -> binary value + requires tag binary + - Output: out -> binary value, result of a AND b + satisfies tag binary + + Example: AND()(1, 1) = 1 +*/ + template AND() { - signal input a; - signal input b; - signal output out; + input signal {binary} a; + input signal {binary} b; + output signal {binary} out; out <== a*b; } + +/* +*** OR(): template that given two inputs a and b representing booleans (0 or 1) returns the value of a OR b + - Inputs: a -> binary value + requires tag binary + b -> binary value + requires tag binary + - Output: out -> binary value, result of a OR b + satisfies tag binary + + Example: OR()(1, 0) = 1 +*/ + template OR() { - signal input a; - signal input b; - signal output out; + input signal {binary} a; + input signal {binary} b; + output signal {binary} out; out <== a + b - a*b; } + +/* +*** NOT(): template that given an input in representing a boolean (0 or 1) returns the value of NOT in + - Inputs: in -> binary value + requires tag binary + - Output: out -> binary value, result of NOT in + satisfies tag binary + + Example: NOT()(1) = 0 +*/ + template NOT() { - signal input in; - signal output out; + input signal {binary} in; + output signal {binary} out; out <== 1 + in - 2*in; } +/* +*** NAND(): template that given two inputs a and b representing booleans (0 or 1) returns the value of a NAND b + - Inputs: a -> binary value + requires tag binary + b -> binary value + requires tag binary + - Output: out -> binary value, result of a NAND b + satisfies tag binary + + Example: NAND()(1, 1) = 0 +*/ + template NAND() { - signal input a; - signal input b; - signal output out; + input signal {binary} a; + input signal {binary} b; + output signal {binary} out; out <== 1 - a*b; } + +/* +*** NOR(): template that given two inputs a and b representing booleans (0 or 1) returns the value of a NOR b + - Inputs: a -> binary value + requires tag binary + b -> binary value + requires tag binary + - Output: out -> binary value, result of a NOR b + satisfies tag binary + + Example: NOR()(1, 0) = 0 +*/ + template NOR() { - signal input a; - signal input b; - signal output out; + input signal {binary} a; + input signal {binary} b; + output signal {binary} out; out <== a*b + 1 - a - b; } +/* +*** MultiAND(n): template that given as input an array of n signals representing booleans (0 or 1) in[0], ... , in[n-1] and returns the value of and[0] AND and[1] ... AND and[n-1] + - Inputs: in[n] -> binary values + requires tag binary + - Output: out[n] -> binary value, result of in[0] AND ... AND in[n-1] + satisfies tag binary + + Example: MultiAND(4)([1, 1, 0, 1]) = 0 +*/ + template MultiAND(n) { - signal input in[n]; - signal output out; + input signal {binary} in[n]; + output signal {binary} out; component and1; component and2; component ands[2]; diff --git a/circuits/mimc.circom b/circuits/mimc.circom deleted file mode 100644 index 64be5611..00000000 --- a/circuits/mimc.circom +++ /dev/null @@ -1,156 +0,0 @@ -/* - 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; - -template MiMC7(nrounds) { - signal input x_in; - signal input k; - signal output out; - - var c[91] = [ - 0, - 20888961410941983456478427210666206549300505294776164667214940546594746570981, - 15265126113435022738560151911929040668591755459209400716467504685752745317193, - 8334177627492981984476504167502758309043212251641796197711684499645635709656, - 1374324219480165500871639364801692115397519265181803854177629327624133579404, - 11442588683664344394633565859260176446561886575962616332903193988751292992472, - 2558901189096558760448896669327086721003508630712968559048179091037845349145, - 11189978595292752354820141775598510151189959177917284797737745690127318076389, - 3262966573163560839685415914157855077211340576201936620532175028036746741754, - 17029914891543225301403832095880481731551830725367286980611178737703889171730, - 4614037031668406927330683909387957156531244689520944789503628527855167665518, - 19647356996769918391113967168615123299113119185942498194367262335168397100658, - 5040699236106090655289931820723926657076483236860546282406111821875672148900, - 2632385916954580941368956176626336146806721642583847728103570779270161510514, - 17691411851977575435597871505860208507285462834710151833948561098560743654671, - 11482807709115676646560379017491661435505951727793345550942389701970904563183, - 8360838254132998143349158726141014535383109403565779450210746881879715734773, - 12663821244032248511491386323242575231591777785787269938928497649288048289525, - 3067001377342968891237590775929219083706800062321980129409398033259904188058, - 8536471869378957766675292398190944925664113548202769136103887479787957959589, - 19825444354178182240559170937204690272111734703605805530888940813160705385792, - 16703465144013840124940690347975638755097486902749048533167980887413919317592, - 13061236261277650370863439564453267964462486225679643020432589226741411380501, - 10864774797625152707517901967943775867717907803542223029967000416969007792571, - 10035653564014594269791753415727486340557376923045841607746250017541686319774, - 3446968588058668564420958894889124905706353937375068998436129414772610003289, - 4653317306466493184743870159523234588955994456998076243468148492375236846006, - 8486711143589723036499933521576871883500223198263343024003617825616410932026, - 250710584458582618659378487568129931785810765264752039738223488321597070280, - 2104159799604932521291371026105311735948154964200596636974609406977292675173, - 16313562605837709339799839901240652934758303521543693857533755376563489378839, - 6032365105133504724925793806318578936233045029919447519826248813478479197288, - 14025118133847866722315446277964222215118620050302054655768867040006542798474, - 7400123822125662712777833064081316757896757785777291653271747396958201309118, - 1744432620323851751204287974553233986555641872755053103823939564833813704825, - 8316378125659383262515151597439205374263247719876250938893842106722210729522, - 6739722627047123650704294650168547689199576889424317598327664349670094847386, - 21211457866117465531949733809706514799713333930924902519246949506964470524162, - 13718112532745211817410303291774369209520657938741992779396229864894885156527, - 5264534817993325015357427094323255342713527811596856940387954546330728068658, - 18884137497114307927425084003812022333609937761793387700010402412840002189451, - 5148596049900083984813839872929010525572543381981952060869301611018636120248, - 19799686398774806587970184652860783461860993790013219899147141137827718662674, - 19240878651604412704364448729659032944342952609050243268894572835672205984837, - 10546185249390392695582524554167530669949955276893453512788278945742408153192, - 5507959600969845538113649209272736011390582494851145043668969080335346810411, - 18177751737739153338153217698774510185696788019377850245260475034576050820091, - 19603444733183990109492724100282114612026332366576932662794133334264283907557, - 10548274686824425401349248282213580046351514091431715597441736281987273193140, - 1823201861560942974198127384034483127920205835821334101215923769688644479957, - 11867589662193422187545516240823411225342068709600734253659804646934346124945, - 18718569356736340558616379408444812528964066420519677106145092918482774343613, - 10530777752259630125564678480897857853807637120039176813174150229243735996839, - 20486583726592018813337145844457018474256372770211860618687961310422228379031, - 12690713110714036569415168795200156516217175005650145422920562694422306200486, - 17386427286863519095301372413760745749282643730629659997153085139065756667205, - 2216432659854733047132347621569505613620980842043977268828076165669557467682, - 6309765381643925252238633914530877025934201680691496500372265330505506717193, - 20806323192073945401862788605803131761175139076694468214027227878952047793390, - 4037040458505567977365391535756875199663510397600316887746139396052445718861, - 19948974083684238245321361840704327952464170097132407924861169241740046562673, - 845322671528508199439318170916419179535949348988022948153107378280175750024, - 16222384601744433420585982239113457177459602187868460608565289920306145389382, - 10232118865851112229330353999139005145127746617219324244541194256766741433339, - 6699067738555349409504843460654299019000594109597429103342076743347235369120, - 6220784880752427143725783746407285094967584864656399181815603544365010379208, - 6129250029437675212264306655559561251995722990149771051304736001195288083309, - 10773245783118750721454994239248013870822765715268323522295722350908043393604, - 4490242021765793917495398271905043433053432245571325177153467194570741607167, - 19596995117319480189066041930051006586888908165330319666010398892494684778526, - 837850695495734270707668553360118467905109360511302468085569220634750561083, - 11803922811376367215191737026157445294481406304781326649717082177394185903907, - 10201298324909697255105265958780781450978049256931478989759448189112393506592, - 13564695482314888817576351063608519127702411536552857463682060761575100923924, - 9262808208636973454201420823766139682381973240743541030659775288508921362724, - 173271062536305557219323722062711383294158572562695717740068656098441040230, - 18120430890549410286417591505529104700901943324772175772035648111937818237369, - 20484495168135072493552514219686101965206843697794133766912991150184337935627, - 19155651295705203459475805213866664350848604323501251939850063308319753686505, - 11971299749478202793661982361798418342615500543489781306376058267926437157297, - 18285310723116790056148596536349375622245669010373674803854111592441823052978, - 7069216248902547653615508023941692395371990416048967468982099270925308100727, - 6465151453746412132599596984628739550147379072443683076388208843341824127379, - 16143532858389170960690347742477978826830511669766530042104134302796355145785, - 19362583304414853660976404410208489566967618125972377176980367224623492419647, - 1702213613534733786921602839210290505213503664731919006932367875629005980493, - 10781825404476535814285389902565833897646945212027592373510689209734812292327, - 4212716923652881254737947578600828255798948993302968210248673545442808456151, - 7594017890037021425366623750593200398174488805473151513558919864633711506220, - 18979889247746272055963929241596362599320706910852082477600815822482192194401, - 13602139229813231349386885113156901793661719180900395818909719758150455500533 - ]; - - var t; - signal t2[nrounds]; - signal t4[nrounds]; - signal t6[nrounds]; - signal t7[nrounds-1]; - - for (var i=0; i nRounds should be 220 -template MiMCSponge(nInputs, nRounds, nOutputs) { - signal input ins[nInputs]; - signal input k; - signal output outs[nOutputs]; - - var i; - - // S = R||C - component S[nInputs + nOutputs - 1]; - - for (i = 0; i < nInputs; i++) { - S[i] = MiMCFeistel(nRounds); - S[i].k <== k; - if (i == 0) { - S[i].xL_in <== ins[0]; - S[i].xR_in <== 0; - } else { - S[i].xL_in <== S[i-1].xL_out + ins[i]; - S[i].xR_in <== S[i-1].xR_out; - } - } - - outs[0] <== S[nInputs - 1].xL_out; - - for (i = 0; i < nOutputs - 1; i++) { - S[nInputs + i] = MiMCFeistel(nRounds); - S[nInputs + i].k <== k; - S[nInputs + i].xL_in <== S[nInputs + i - 1].xL_out; - S[nInputs + i].xR_in <== S[nInputs + i - 1].xR_out; - outs[i + 1] <== S[nInputs + i].xL_out; - } -} - -template MiMCFeistel(nrounds) { - signal input xL_in; - signal input xR_in; - signal input k; - signal output xL_out; - signal output xR_out; - - // doesn't contain the first and last round constants, which are always zero - var c_partial[218] = [ - 7120861356467848435263064379192047478074060781135320967663101236819528304084, - 5024705281721889198577876690145313457398658950011302225525409148828000436681, - 17980351014018068290387269214713820287804403312720763401943303895585469787384, - 19886576439381707240399940949310933992335779767309383709787331470398675714258, - 1213715278223786725806155661738676903520350859678319590331207960381534602599, - 18162138253399958831050545255414688239130588254891200470934232514682584734511, - 7667462281466170157858259197976388676420847047604921256361474169980037581876, - 7207551498477838452286210989212982851118089401128156132319807392460388436957, - 9864183311657946807255900203841777810810224615118629957816193727554621093838, - 4798196928559910300796064665904583125427459076060519468052008159779219347957, - 17387238494588145257484818061490088963673275521250153686214197573695921400950, - 10005334761930299057035055370088813230849810566234116771751925093634136574742, - 11897542014760736209670863723231849628230383119798486487899539017466261308762, - 16771780563523793011283273687253985566177232886900511371656074413362142152543, - 749264854018824809464168489785113337925400687349357088413132714480582918506, - 3683645737503705042628598550438395339383572464204988015434959428676652575331, - 7556750851783822914673316211129907782679509728346361368978891584375551186255, - 20391289379084797414557439284689954098721219201171527383291525676334308303023, - 18146517657445423462330854383025300323335289319277199154920964274562014376193, - 8080173465267536232534446836148661251987053305394647905212781979099916615292, - 10796443006899450245502071131975731672911747129805343722228413358507805531141, - 5404287610364961067658660283245291234008692303120470305032076412056764726509, - 4623894483395123520243967718315330178025957095502546813929290333264120223168, - 16845753148201777192406958674202574751725237939980634861948953189320362207797, - 4622170486584704769521001011395820886029808520586507873417553166762370293671, - 16688277490485052681847773549197928630624828392248424077804829676011512392564, - 11878652861183667748838188993669912629573713271883125458838494308957689090959, - 2436445725746972287496138382764643208791713986676129260589667864467010129482, - 1888098689545151571063267806606510032698677328923740058080630641742325067877, - 148924106504065664829055598316821983869409581623245780505601526786791681102, - 18875020877782404439294079398043479420415331640996249745272087358069018086569, - 15189693413320228845990326214136820307649565437237093707846682797649429515840, - 19669450123472657781282985229369348220906547335081730205028099210442632534079, - 5521922218264623411380547905210139511350706092570900075727555783240701821773, - 4144769320246558352780591737261172907511489963810975650573703217887429086546, - 10097732913112662248360143041019433907849917041759137293018029019134392559350, - 1720059427972723034107765345743336447947522473310069975142483982753181038321, - 6302388219880227251325608388535181451187131054211388356563634768253301290116, - 6745410632962119604799318394592010194450845483518862700079921360015766217097, - 10858157235265583624235850660462324469799552996870780238992046963007491306222, - 20241898894740093733047052816576694435372877719072347814065227797906130857593, - 10165780782761211520836029617746977303303335603838343292431760011576528327409, - 2832093654883670345969792724123161241696170611611744759675180839473215203706, - 153011722355526826233082383360057587249818749719433916258246100068258954737, - 20196970640587451358539129330170636295243141659030208529338914906436009086943, - 3180973917010545328313139835982464870638521890385603025657430208141494469656, - 17198004293191777441573635123110935015228014028618868252989374962722329283022, - 7642160509228669138628515458941659189680509753651629476399516332224325757132, - 19346204940546791021518535594447257347218878114049998691060016493806845179755, - 11501810868606870391127866188394535330696206817602260610801897042898616817272, - 3113973447392053821824427670386252797811804954746053461397972968381571297505, - 6545064306297957002139416752334741502722251869537551068239642131448768236585, - 5203908808704813498389265425172875593837960384349653691918590736979872578408, - 2246692432011290582160062129070762007374502637007107318105405626910313810224, - 11760570435432189127645691249600821064883781677693087773459065574359292849137, - 5543749482491340532547407723464609328207990784853381797689466144924198391839, - 8837549193990558762776520822018694066937602576881497343584903902880277769302, - 12855514863299373699594410385788943772765811961581749194183533625311486462501, - 5363660674689121676875069134269386492382220935599781121306637800261912519729, - 13162342403579303950549728848130828093497701266240457479693991108217307949435, - 916941639326869583414469202910306428966657806899788970948781207501251816730, - 15618589556584434434009868216186115416835494805174158488636000580759692174228, - 8959562060028569701043973060670353733575345393653685776974948916988033453971, - 16390754464333401712265575949874369157699293840516802426621216808905079127650, - 168282396747788514908709091757591226095443902501365500003618183905496160435, - 8327443473179334761744301768309008451162322941906921742120510244986704677004, - 17213012626801210615058753489149961717422101711567228037597150941152495100640, - 10394369641533736715250242399198097296122982486516256408681925424076248952280, - 17784386835392322654196171115293700800825771210400152504776806618892170162248, - 16533189939837087893364000390641148516479148564190420358849587959161226782982, - 18725396114211370207078434315900726338547621160475533496863298091023511945076, - 7132325028834551397904855671244375895110341505383911719294705267624034122405, - 148317947440800089795933930720822493695520852448386394775371401743494965187, - 19001050671757720352890779127693793630251266879994702723636759889378387053056, - 18824274411769830274877839365728651108434404855803844568234862945613766611460, - 12771414330193951156383998390424063470766226667986423961689712557338777174205, - 11332046574800279729678603488745295198038913503395629790213378101166488244657, - 9607550223176946388146938069307456967842408600269548190739947540821716354749, - 8756385288462344550200229174435953103162307705310807828651304665320046782583, - 176061952957067086877570020242717222844908281373122372938833890096257042779, - 12200212977482648306758992405065921724409841940671166017620928947866825250857, - 10868453624107875516866146499877130701929063632959660262366632833504750028858, - 2016095394399807253596787752134573207202567875457560571095586743878953450738, - 21815578223768330433802113452339488275704145896544481092014911825656390567514, - 4923772847693564777744725640710197015181591950368494148029046443433103381621, - 1813584943682214789802230765734821149202472893379265320098816901270224589984, - 10810123816265612772922113403831964815724109728287572256602010709288980656498, - 1153669123397255702524721206511185557982017410156956216465120456256288427021, - 5007518659266430200134478928344522649876467369278722765097865662497773767152, - 2511432546938591792036639990606464315121646668029252285288323664350666551637, - 32883284540320451295484135704808083452381176816565850047310272290579727564, - 10484856914279112612610993418405543310546746652738541161791501150994088679557, - 2026733759645519472558796412979210009170379159866522399881566309631434814953, - 14731806221235869882801331463708736361296174006732553130708107037190460654379, - 14740327483193277147065845135561988641238516852487657117813536909482068950652, - 18787428285295558781869865751953016580493190547148386433580291216673009884554, - 3804047064713122820157099453648459188816376755739202017447862327783289895072, - 16709604795697901641948603019242067672006293290826991671766611326262532802914, - 11061717085931490100602849654034280576915102867237101935487893025907907250695, - 2821730726367472966906149684046356272806484545281639696873240305052362149654, - 17467794879902895769410571945152708684493991588672014763135370927880883292655, - 1571520786233540988201616650622796363168031165456869481368085474420849243232, - 10041051776251223165849354194892664881051125330236567356945669006147134614302, - 3981753758468103976812813304477670033098707002886030847251581853700311567551, - 4365864398105436789177703571412645548020537580493599380018290523813331678900, - 2391801327305361293476178683853802679507598622000359948432171562543560193350, - 214219368547551689972421167733597094823289857206402800635962137077096090722, - 18192064100315141084242006659317257023098826945893371479835220462302399655674, - 15487549757142039139328911515400805508248576685795694919457041092150651939253, - 10142447197759703415402259672441315777933858467700579946665223821199077641122, - 11246573086260753259993971254725613211193686683988426513880826148090811891866, - 6574066859860991369704567902211886840188702386542112593710271426704432301235, - 11311085442652291634822798307831431035776248927202286895207125867542470350078, - 20977948360215259915441258687649465618185769343138135384346964466965010873779, - 792781492853909872425531014397300057232399608769451037135936617996830018501, - 5027602491523497423798779154966735896562099398367163998686335127580757861872, - 14595204575654316237672764823862241845410365278802914304953002937313300553572, - 13973538843621261113924259058427434053808430378163734641175100160836376897004, - 16395063164993626722686882727042150241125309409717445381854913964674649318585, - 8465768840047024550750516678171433288207841931251654898809033371655109266663, - 21345603324471810861925019445720576814602636473739003852898308205213912255830, - 21171984405852590343970239018692870799717057961108910523876770029017785940991, - 10761027113757988230637066281488532903174559953630210849190212601991063767647, - 6678298831065390834922566306988418588227382406175769592902974103663687992230, - 4993662582188632374202316265508850988596880036291765531885657575099537176757, - 18364168158495573675698600238443218434246806358811328083953887470513967121206, - 3506345610354615013737144848471391553141006285964325596214723571988011984829, - 248732676202643792226973868626360612151424823368345645514532870586234380100, - 10090204501612803176317709245679152331057882187411777688746797044706063410969, - 21297149835078365363970699581821844234354988617890041296044775371855432973500, - 16729368143229828574342820060716366330476985824952922184463387490091156065099, - 4467191506765339364971058668792642195242197133011672559453028147641428433293, - 8677548159358013363291014307402600830078662555833653517843708051504582990832, - 1022951765127126818581466247360193856197472064872288389992480993218645055345, - 1888195070251580606973417065636430294417895423429240431595054184472931224452, - 4221265384902749246920810956363310125115516771964522748896154428740238579824, - 2825393571154632139467378429077438870179957021959813965940638905853993971879, - 19171031072692942278056619599721228021635671304612437350119663236604712493093, - 10780807212297131186617505517708903709488273075252405602261683478333331220733, - 18230936781133176044598070768084230333433368654744509969087239465125979720995, - 16901065971871379877929280081392692752968612240624985552337779093292740763381, - 146494141603558321291767829522948454429758543710648402457451799015963102253, - 2492729278659146790410698334997955258248120870028541691998279257260289595548, - 2204224910006646535594933495262085193210692406133533679934843341237521233504, - 16062117410185840274616925297332331018523844434907012275592638570193234893570, - 5894928453677122829055071981254202951712129328678534592916926069506935491729, - 4947482739415078212217504789923078546034438919537985740403824517728200332286, - 16143265650645676880461646123844627780378251900510645261875867423498913438066, - 397690828254561723549349897112473766901585444153303054845160673059519614409, - 11272653598912269895509621181205395118899451234151664604248382803490621227687, - 15566927854306879444693061574322104423426072650522411176731130806720753591030, - 14222898219492484180162096141564251903058269177856173968147960855133048449557, - 16690275395485630428127725067513114066329712673106153451801968992299636791385, - 3667030990325966886479548860429670833692690972701471494757671819017808678584, - 21280039024501430842616328642522421302481259067470872421086939673482530783142, - 15895485136902450169492923978042129726601461603404514670348703312850236146328, - 7733050956302327984762132317027414325566202380840692458138724610131603812560, - 438123800976401478772659663183448617575635636575786782566035096946820525816, - 814913922521637742587885320797606426167962526342166512693085292151314976633, - 12368712287081330853637674140264759478736012797026621876924395982504369598764, - 2494806857395134874309386694756263421445039103814920780777601708371037591569, - 16101132301514338989512946061786320637179843435886825102406248183507106312877, - 6252650284989960032925831409804233477770646333900692286731621844532438095656, - 9277135875276787021836189566799935097400042171346561246305113339462708861695, - 10493603554686607050979497281838644324893776154179810893893660722522945589063, - 8673089750662709235894359384294076697329948991010184356091130382437645649279, - 9558393272910366944245875920138649617479779893610128634419086981339060613250, - 19012287860122586147374214541764572282814469237161122489573881644994964647218, - 9783723818270121678386992630754842961728702994964214799008457449989291229500, - 15550788416669474113213749561488122552422887538676036667630838378023479382689, - 15016165746156232864069722572047169071786333815661109750860165034341572904221, - 6506225705710197163670556961299945987488979904603689017479840649664564978574, - 10796631184889302076168355684722130903785890709107732067446714470783437829037, - 19871836214837460419845806980869387567383718044439891735114283113359312279540, - 20871081766843466343749609089986071784031203517506781251203251608363835140622, - 5100105771517691442278432864090229416166996183792075307747582375962855820797, - 8777887112076272395250620301071581171386440850451972412060638225741125310886, - 5300440870136391278944213332144327695659161151625757537632832724102670898756, - 1205448543652932944633962232545707633928124666868453915721030884663332604536, - 5542499997310181530432302492142574333860449305424174466698068685590909336771, - 11028094245762332275225364962905938096659249161369092798505554939952525894293, - 19187314764836593118404597958543112407224947638377479622725713735224279297009, - 17047263688548829001253658727764731047114098556534482052135734487985276987385, - 19914849528178967155534624144358541535306360577227460456855821557421213606310, - 2929658084700714257515872921366736697080475676508114973627124569375444665664, - 15092262360719700162343163278648422751610766427236295023221516498310468956361, - 21578580340755653236050830649990190843552802306886938815497471545814130084980, - 1258781501221760320019859066036073675029057285507345332959539295621677296991, - 3819598418157732134449049289585680301176983019643974929528867686268702720163, - 8653175945487997845203439345797943132543211416447757110963967501177317426221, - 6614652990340435611114076169697104582524566019034036680161902142028967568142, - 19212515502973904821995111796203064175854996071497099383090983975618035391558, - 18664315914479294273286016871365663486061896605232511201418576829062292269769, - 11498264615058604317482574216318586415670903094838791165247179252175768794889, - 10814026414212439999107945133852431304483604215416531759535467355316227331774, - 17566185590731088197064706533119299946752127014428399631467913813769853431107, - 14016139747289624978792446847000951708158212463304817001882956166752906714332, - 8242601581342441750402731523736202888792436665415852106196418942315563860366, - 9244680976345080074252591214216060854998619670381671198295645618515047080988, - 12216779172735125538689875667307129262237123728082657485828359100719208190116, - 10702811721859145441471328511968332847175733707711670171718794132331147396634, - 6479667912792222539919362076122453947926362746906450079329453150607427372979, - 15117544653571553820496948522381772148324367479772362833334593000535648316185, - 6842203153996907264167856337497139692895299874139131328642472698663046726780, - 12732823292801537626009139514048596316076834307941224506504666470961250728055, - 6936272626871035740815028148058841877090860312517423346335878088297448888663, - 17297554111853491139852678417579991271009602631577069694853813331124433680030, - 16641596134749940573104316021365063031319260205559553673368334842484345864859, - 7400481189785154329569470986896455371037813715804007747228648863919991399081, - 2273205422216987330510475127669563545720586464429614439716564154166712854048, - 15162538063742142685306302282127534305212832649282186184583465569986719234456, - 5628039096440332922248578319648483863204530861778160259559031331287721255522, - 16085392195894691829567913404182676871326863890140775376809129785155092531260, - 14227467863135365427954093998621993651369686288941275436795622973781503444257, - 18224457394066545825553407391290108485121649197258948320896164404518684305122, - 274945154732293792784580363548970818611304339008964723447672490026510689427, - 11050822248291117548220126630860474473945266276626263036056336623671308219529, - 2119542016932434047340813757208803962484943912710204325088879681995922344971 - ]; - - var t; - signal t2[nrounds]; - signal t4[nrounds]; - signal xL[nrounds-1]; - signal xR[nrounds-1]; - - var c; - for (var i=0; i. */ + + pragma circom 2.1.5; + +include "buses.circom"; + +// The templates and functions of this file only work for finite field F_p = bn128, +// with the prime number p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. /* Source: https://en.wikipedia.org/wiki/Montgomery_curve - 1 + y 1 + y - [u, v] = [ ------- , ---------- ] - 1 - y (1 - y)x +*/ - */ - pragma circom 2.0.0; +/* + The Baby-Jubjub Montgomery elliptic curve defined over the finite field bn128 is given by the equation -template Edwards2Montgomery() { - signal input in[2]; - signal output out[2]; + B*v^2 = u^3 + A*u^2 + u, A = 168698, B = 1 - out[0] <-- (1 + in[1]) / (1 - in[1]); - out[1] <-- out[0] / in[0]; + This curve is birationally equivalent to the twisted Edwards elliptic curve + a*x^2 + y^2 = 1 + d*x^2*y^2, a = 168700 = (A+2)/B, d = 168696 = (A-2)/B - out[0] * (1-in[1]) === (1 + in[1]); - out[1] * in[0] === out[0]; -} + u u-1 1+y 1+y + via the map (u,v) -> (x,y) = [ --- , ----- ] with inverse (x,y) -> (u,v) = [ ----- , --------- ] + v u+1 1-y (1-y)*x + + Since a is not a square in bn128, the twisted Edwards curve is a quadratic twist of the Edwards curve + + x'^2 + y'^2 = 1 + d'*x'^2*y'^2 + + via the map (x,y) -> (x',y') = [ sqrt(a)*x , y ] + + where d' = 9706598848417545097372247223557719406784115219466060233080913168975159366771. + Here circuits are provided to transform a point of the Baby-Jubjub curve in twisted Edwards to its Montgomery form and vice versa. + Circuits to add and double points of the Baby-Jubjub Montgomery curve are provided as well. +*/ /* + spec tag babyedwards: 168700*(p.x)^2 + (p.y)^2 = 1 + 168696*(p.x)^2*(p.y)^2 + spec tag babymontgomery: (p.y)^2 = (p.x)^3 + 168698*(p.x)^2 + p.x +*/ - u u - 1 - [x, y] = [ ---, ------- ] - v u + 1 +/* +*** Edwards2Montgomery(): template that receives a point of the Baby-Jubjub curve in twisted Edwards form + and returns the equivalent point in Montgomery form. + - Inputs: pin -> bus representing a point of the Baby-Jubjub curve in twisted Edwards form + - Outputs: pout -> bus representing a point of the Baby-Jubjub curve in Montgomery form + + Map from twisted Edwards elliptic curve to its birationally equivalent Montgomery curve: + + 1 + y 1 + y + (x, y) -> (u, v) = [ ------- , ----------- ] + 1 - y (1 - y)*x + +*/ - */ -template Montgomery2Edwards() { - signal input in[2]; - signal output out[2]; +template Edwards2Montgomery() { + input Point {babyedwards} pin; + output Point {babymontgomery} pout; - out[0] <-- in[0] / in[1]; - out[1] <-- (in[0] - 1) / (in[0] + 1); + pout.x <-- (1 + pin.y) / (1 - pin.y); + pout.y <-- pout.x / pin.x; - out[0] * in[1] === in[0]; - out[1] * (in[0] + 1) === in[0] - 1; + pout.x * (1 - pin.y) === (1 + pin.y); + pout.y * pin.x === pout.x; } - /* - x2 - x1 - lamda = --------- - y2 - y1 +*** Montgomery2Edwards(): template that receives an input pin representing a point of the Baby-Jubjub curve in Montgomery form + and returns the equivalent point in twisted Edwards form. + - Inputs: pin -> bus representing a point of the Baby-Jubjub curve in Montgomery form + - Outputs: pout -> bus representing a point of the curve Baby-Jubjub in twisted Edwards form + + Map from Montgomery elliptic curve to its birationally equivalent twisted Edwards curve: + + u u - 1 + (u, v) -> (x, y) = [ ---, ------- ] + v u + 1 - x3 + A + x1 + x2 - x3 = B * lamda^2 - A - x1 -x2 => lamda^2 = ------------------ - B + */ - y3 = (2*x1 + x2 + A)*lamda - B*lamda^3 - y1 => +template Montgomery2Edwards() { + input Point {babymontgomery} pin; + output Point {babyedwards} pout; + pout.x <-- pin.x / pin.y; + pout.y <-- (pin.x - 1) / (pin.x + 1); - => y3 = lamda * ( 2*x1 + x2 + A - x3 - A - x1 - x2) - y1 => + pout.x * pin.y === pin.x; + pout.y * (pin.x + 1) === pin.x - 1; +} - => y3 = lamda * ( x1 - x3 ) - y1 ----------- +/* +*** MontgomeryAdd(): template that receives two inputs pin1, pin2 representing points of the Baby-Jubjub curve in Montgomery form + and returns the addition of the points. + - Inputs: pin1 -> bus representing a point of the Baby-Jubjub curve in Montgomery form + pin2 -> bus representing a point of the Baby-Jubjub curve in Montgomery form + - Outputs: pout -> bus representing the point pin1 + pin2 of the Baby-Jubjub curve in Montgomery form + + Montgomery Addition Law: + + y2 - y1 y2 - y1 y2 - y1 + [x3, y3] = [x1, y1] + [x2, y2] = [ B*( --------- )^2 - A - x1 - x2, ( --------- )*(A + 2*x1 + x2) - B*( --------- )^3 - y1 ] + x2 - x1 x2 - x1 x2 - x1 y2 - y1 lamda = --------- x2 - x1 - x3 = B * lamda^2 - A - x1 -x2 + x3 = B*lamda^2 - A - x1 -x2 - y3 = lamda * ( x1 - x3 ) - y1 - - */ + y3 = lamda*( x1 - x3 ) - y1 +*/ template MontgomeryAdd() { - signal input in1[2]; - signal input in2[2]; - signal output out[2]; - - var a = 168700; - var d = 168696; + input Point {babymontgomery} pin1, pin2; + output Point {babymontgomery} pout; - var A = (2 * (a + d)) / (a - d); - var B = 4 / (a - d); + var A = 168698; + var B = 1; signal lamda; - lamda <-- (in2[1] - in1[1]) / (in2[0] - in1[0]); - lamda * (in2[0] - in1[0]) === (in2[1] - in1[1]); + lamda <-- (pin2.y - pin1.y) / (pin2.x - pin1.x); + lamda * (pin2.x - pin1.x) === pin2.y - pin1.y; - out[0] <== B*lamda*lamda - A - in1[0] -in2[0]; - out[1] <== lamda * (in1[0] - out[0]) - in1[1]; + pout.x <== B*lamda*lamda - A - pin1.x - pin2.x; + pout.y <== lamda * (pin1.x - pout.x) - pin1.y; } /* +*** MontgomeryDouble(): template that receives an input pin representing a point of the Baby-Jubjub curve in Montgomery form + and returns the point 2 * pin. + - Inputs: pin -> bus representing a point of the Baby-Jubjub curve in Montgomery form + - Outputs: pout -> bus representing the point 2*pin of the Baby-Jubjub curve in Montgomery form + + + Montgomery Doubling Law: + + 3*x1^2 + 2*A*x1 + 1 3*x1^2 + 2*A*x1 + 1 3*x1^2 + 2*A*x1 + 1 + [x2, y2] = 2*[x1, y1] = [ B*( --------------------- )^2 - A - x1 - x2, ( --------------------- )*(A + 2*x1 + x2) - B*( --------------------- )^3 - y1 ] + 2*B*y1 2*B*y1 2*B*y1 x1_2 = x1*x1 @@ -114,29 +166,44 @@ template MontgomeryAdd() { lamda = --------------------- 2*B*y1 - x3 = B * lamda^2 - A - x1 -x1 + x2 = B*lamda^2 - A - x1 -x1 - y3 = lamda * ( x1 - x3 ) - y1 + y2 = lamda*( x1 - x2 ) - y1 */ + template MontgomeryDouble() { - signal input in[2]; - signal output out[2]; + input Point {babymontgomery} pin; + output Point {babymontgomery} pout; - var a = 168700; - var d = 168696; - - var A = (2 * (a + d)) / (a - d); - var B = 4 / (a - d); + var A = 168698; + var B = 1; signal lamda; signal x1_2; - x1_2 <== in[0] * in[0]; + x1_2 <== pin.x * pin.x; + + lamda <-- (3*x1_2 + 2*A*pin.x + 1) / (2*B*pin.y); + lamda * (2*B*pin.y) === (3*x1_2 + 2*A*pin.x + 1); + + pout.x <== B*lamda*lamda - A - 2*pin.x; + pout.y <== lamda * (pin.x - pout.x) - pin.y; +} + + - 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 ); +template MontgomeryBabyCheck(){ + input Point pin; + output Point {babymontgomery} pout; + + var A = 168698; + + signal x_2 <== pin.x * pin.x; + signal y_2 <== pin.y * pin.y; + + y_2 === x_2 * pin.x + A * x_2 + pin.x; + + pin ==> pout; - out[0] <== B*lamda*lamda - A - 2*in[0]; - out[1] <== lamda * (in[0] - out[0]) - in[1]; } diff --git a/circuits/multiplexer.circom b/circuits/multiplexer.circom deleted file mode 100644 index 848e31e4..00000000 --- a/circuits/multiplexer.circom +++ /dev/null @@ -1,115 +0,0 @@ -/* - 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 . -*/ - -/* - 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 . -*/ - -// --> Assignation without constraint -// <-- Assignation without constraint -// === Constraint -// <== Assignation with constraint -// ==> Assignation with constraint -// All variables are members of the field F[p] -// https://github.com/zcash-hackworks/sapling-crypto -// https://github.com/ebfull/bellman - -/* -function log2(a) { - if (a==0) { - return 0; - } - let n = 1; - let r = 1; - while (n success; - success * (success -1) === 0; -} - - -template Multiplexer(wIn, nIn) { - signal input inp[nIn][wIn]; - signal input sel; - signal output out[wIn]; - component dec = Decoder(nIn); - component ep[wIn]; - - for (var k=0; k dec.inp; - for (var j=0; j ep[j].in1[k]; - dec.out[k] ==> ep[j].in2[k]; - } - ep[j].out ==> out[j]; - } - dec.success === 1; -} diff --git a/circuits/mux1.circom b/circuits/mux1.circom index 444cb849..4cf2b42a 100644 --- a/circuits/mux1.circom +++ b/circuits/mux1.circom @@ -16,12 +16,30 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; + +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + +/* + +*** MultiMux1(n): template that implements a multiplexer 2-to-1 between two inputs of n elements + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + + - Inputs: s -> binary value, selector + requires tag binary + c[n][2] -> two arrays of n elements that correspond to the inputs of the mux: c[i][0] => first input, c[i][1] => second input + - Output: out[n] -> array of n elements, it takes the value c[i][0] if s == 0, c[i][1] if s == 1 + + Example: MultiMux1(3)([[1, 2], [3, 1], [4, 6]], 1) = [2, 1, 6] + + */ template MultiMux1(n) { - signal input c[n][2]; // Constants - signal input s; // Selector - signal output out[n]; + input signal c[n][2]; // Constants + input signal {binary} s; // Selector + output signal out[n]; for (var i=0; i binary value, selector + requires tag binary + c[2] -> two elements that correspond to the inputs of the mux: c[0] => first input, c[1] => second input + - Output: out -> field element, it takes the value c[0] if s == 0, c[1] if s == 1 + + Example: Mux1()([1, 5], 0) = 1 + + */ + template Mux1() { var i; - signal input c[2]; // Constants - signal input s; // Selector - signal output out; + input signal c[2]; // Constants + input signal {binary} s; // Selector + output signal out; component mux = MultiMux1(1); diff --git a/circuits/mux2.circom b/circuits/mux2.circom index 557539bf..162d11f2 100644 --- a/circuits/mux2.circom +++ b/circuits/mux2.circom @@ -16,12 +16,33 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + + +/* + +*** MultiMux2(n): template that implements a multiplexer 4-to-1 between four inputs of n elements + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + - If s == 2 then out = c[2] + - If s == 3 then out = c[3] + + - Inputs: s[2] -> binary values, selector + requires tag binary + c[n][4] -> four arrays of n elements that correspond to the inputs of the mux: c[i][0] => first input, c[i][1] => second input, ... + - Output: out[n] -> array of n elements, it takes the value c[i][0] if s == [0, 0], c[i][1] if s == [1, 0], c[i][2] if s == [0, 1], c[i][3] if s == [1, 1] + + Example: MultiMux2(3)([[1, 2, 4, 1], [3, 1, 3, 1], [4, 6, 6, 2]], [0, 1]) = [4, 3, 6] + + */ + template MultiMux2(n) { - signal input c[n][4]; // Constants - signal input s[2]; // Selector - signal output out[n]; + input signal c[n][4]; // Constants + input signal {binary} s[2]; // Selector + output signal out[n]; signal a10[n]; signal a1[n]; @@ -43,11 +64,30 @@ template MultiMux2(n) { } } + + +/* + +*** Mux2(): template that implements a multiplexer 4-to-1 + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + - If s == 2 then out = c[2] + - If s == 3 then out = c[3] + + - Inputs: s[2] -> binary values, selector + requires tag binary + c[4] -> four elements that correspond to the inputs of the mux: c[0] => first input, c[1] => second input, ... + - Output: out -> field element, it takes the value c[0] if s == [0, 0], c[1] if s == [1, 0], c[2] if s == [0, 1], c[3] if s == [1, 1] + + Example: Mux2()([1, 5, 4, 2], [1, 1]) = 2 + + */ + template Mux2() { var i; - signal input c[4]; // Constants - signal input s[2]; // Selector - signal output out; + input signal c[4]; // Constants + input signal {binary} s[2]; // Selector + output signal out; component mux = MultiMux2(1); diff --git a/circuits/mux3.circom b/circuits/mux3.circom index 4be5f7c6..16828b36 100644 --- a/circuits/mux3.circom +++ b/circuits/mux3.circom @@ -16,12 +16,37 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; + + +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + +/* + +*** MultiMux3(n): template that implements a multiplexer 8-to-1 between eight inputs of n elements + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + . + . + . + + - If s == 6 then out = c[6] + - If s == 7 then out = c[7] + + - Inputs: s[3] -> binary values, selector + requires tag binary + c[n][8] -> eight arrays of n elements that correspond to the inputs of the mux: c[i][0] => first input, c[i][1] => second input, ... + - Output: out[n] -> array of n elements, it takes the value c[i][0] if s == [0, 0, 0], c[i][1] if s == [1, 0, 0], ... , c[i][7] if s == [1, 1, 1] + + Example: MultiMux3(2)([[1, 2, 4, 1, 1, 6, 7, 3], [3, 1, 3, 1, 4, 6, 6, 2]], [1, 0 , 1]) = [6, 6] + + */ template MultiMux3(n) { - signal input c[n][8]; // Constants - signal input s[3]; // Selector - signal output out[n]; + input signal c[n][8]; // Constants + input signal {binary} s[3]; // Selector + output signal out[n]; signal a210[n]; signal a21[n]; @@ -55,11 +80,33 @@ template MultiMux3(n) { } } + +/* + +*** Mux3(): template that implements a multiplexer 8-to-1 + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + . + . + . + + - If s == 6 then out = c[6] + - If s == 7 then out = c[7] + + - Inputs: s[3] -> binary values, selector + requires tag binary + c[8] -> eight elements that correspond to the inputs of the mux: c[0] => first input, c[1] => second input, ... + - Output: out -> field element, it takes the value c[0] if s == [0, 0, 0], c[1] if s == [1, 0, 0], . . ., c[7] if s == [1, 1, 1] + + Example: Mux3()([1, 5, 4, 2, 6, 3, 1, 5], [0, 1, 1]] = 1 + + */ + template Mux3() { var i; - signal input c[8]; // Constants - signal input s[3]; // Selector - signal output out; + input signal c[8]; // Constants + input signal {binary} s[3]; // Selector + output signal out; component mux = MultiMux3(1); diff --git a/circuits/mux4.circom b/circuits/mux4.circom index 01e98bc8..9169eb51 100644 --- a/circuits/mux4.circom +++ b/circuits/mux4.circom @@ -16,12 +16,37 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; + +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + + +/* + +*** MultiMux4(n): template that implements a multiplexer 16-to-1 between 16 inputs of n elements + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + . + . + . + + - If s == 14 then out = c[14] + - If s == 15 then out = c[15] + + - Inputs: s[4] -> binary values, selector + requires tag binary + c[n][16] -> 16 arrays of n elements that correspond to the inputs of the mux: c[i][0] => first input, c[i][1] => second input, ... + - Output: out[n] -> array of n elements, it takes the value c[i][0] if s == [0, 0, 0, 0], c[i][1] if s == [1, 0, 0, 0], ... , c[i][15] if s == [1, 1, 1, 1] + + Example: MultiMux4(2)([[1, 2, 4, 1, 1, 6, 7, 3, 1, 2, 4, 1, 1, 6, 7, 3], [3, 1, 3, 1, 4, 6, 6, 2, 1, 2, 4, 1, 1, 6, 7, 3]], [1, 0, 1, 0]) = [6, 6] + + */ template MultiMux4(n) { - signal input c[n][16]; // Constants - signal input s[4]; // Selector - signal output out[n]; + input signal c[n][16]; // Constants + input signal {binary} s[4]; // Selector + output signal out[n]; signal a3210[n]; signal a321[n]; @@ -76,34 +101,38 @@ template MultiMux4(n) { out[i] <== ( a3210[i] + a321[i] + a320[i] + a310[i] + a32[i] + a31[i] + a30[i] + a3[i] ) * s[3] + ( a210[i] + a21[i] + a20[i] + a10[i] + a2[i] + a1[i] + a0[i] + a[i] ); -/* - out[i] <== ( s210 * ( c[i][15]-c[i][14]-c[i][13]+c[i][12] - c[i][11]+c[i][10]+c[i][ 9]-c[i][ 8] - -c[i][ 7]+c[i][ 6]+c[i][ 5]-c[i][ 4] + c[i][ 3]-c[i][ 2]-c[i][ 1]+c[i][ 0] ) + - s21 * ( c[i][14]-c[i][12]-c[i][10]+c[i][ 8] - c[i][ 6]+c[i][ 4]+c[i][ 2]-c[i][ 0] ) + - s20 * ( c[i][13]-c[i][12]-c[i][ 9]+c[i][ 8] - c[i][ 5]+c[i][ 4]+c[i][ 1]-c[i][ 0] ) + - s10 * ( c[i][11]-c[i][10]-c[i][ 9]+c[i][ 8] - c[i][ 3]+c[i][ 2]+c[i][ 1]-c[i][ 0] ) + - s[2] * ( c[i][12]-c[i][ 8]-c[i][ 4]+c[i][ 0] ) + - s[1] * ( c[i][10]-c[i][ 8]-c[i][ 2]+c[i][ 0] ) + - s[0] * ( c[i][ 9]-c[i][ 8]-c[i][ 1]+c[i][ 0] ) + - ( c[i][ 8]-c[i][ 0] ) ) * s[3] + - ( s210 * ( c[i][ 7]-c[i][ 6]-c[i][ 5]+c[i][ 4] - c[i][ 3]+c[i][ 2]+c[i][ 1]-c[i][ 0] ) + - s21 * ( c[i][ 6]-c[i][ 4]-c[i][ 2]+c[i][ 0] ) + - s20 * ( c[i][ 5]-c[i][ 4]-c[i][ 1]+c[i][ 0] ) + - s10 * ( c[i][ 3]-c[i][ 2]-c[i][ 1]+c[i][ 0] ) + - s[2] * ( c[i][ 4]-c[i][ 0] ) + - s[1] * ( c[i][ 2]-c[i][ 0] ) + - s[0] * ( c[i][ 1]-c[i][ 0] ) + - ( c[i][ 0] )); -*/ } } + + +/* + +*** Mux4(): template that implements a multiplexer 16-to-1 + - If s == 0 then out = c[0] + - If s == 1 then out = c[1] + . + . + . + + - If s == 14 then out = c[14] + - If s == 15 then out = c[15] + + - Inputs: s[4] -> binary values, selector + requires tag binary + c[16] -> 16 elements that correspond to the inputs of the mux: c[0] => first input, c[1] => second input, ... + - Output: out -> field element, it takes the value c[0] if s == [0, 0, 0, 0], c[1] if s == [1, 0, 0, 0], . . ., c[15] if s == [1, 1, 1, 1] + + Example: Mux3()([1, 5, 4, 2, 6, 3, 1, 5, 1, 5, 4, 2, 6, 3, 1, 5], [0, 0, 1, 1]) = 6 + + */ + template Mux4() { var i; - signal input c[16]; // Constants - signal input s[4]; // Selector - signal output out; + input signal c[16]; // Constants + input signal {binary} s[4]; // Selector + output signal out; component mux = MultiMux4(1); diff --git a/circuits/pedersen.circom b/circuits/pedersen.circom index a29f4863..318f889f 100644 --- a/circuits/pedersen.circom +++ b/circuits/pedersen.circom @@ -16,17 +16,37 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; + +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) include "montgomery.circom"; include "mux3.circom"; include "babyjub.circom"; +include "buses.circom"; + + +/* + +*** Window4(): template that given a point in Montgomery representation base and a binary input in, calculates: + out = base + base*in[0] + 2*base*in[1] + 4*base*in[2] in case in[3] == 0, in case in[3] == 1 then it negates out[1] --> out = base * (in[0..2] + 1) if in[3] == 0, out = - base * (in[0..2] + 1) if in[3] == 1 + + out8 = 8*base + + This circuit is used in order to perform the Pedersen protocol on an input in. + - Inputs: in[4] -> binary value + requires tag binary + base[2] -> input curve point in Montgomery representation + - Outputs: out[2] -> output curve point in Montgomery representation + out8[2] -> output curve point in Montgomery representation + + */ template Window4() { - signal input in[4]; - signal input base[2]; - signal output out[2]; - signal output out8[2]; // Returns 8*Base (To be linked) + input signal {binary} in[4]; + input Point {babymontgomery} base; + output Point {babymontgomery} pout; + output Point {babymontgomery} pout8; // Returns 8*Base (To be linked) component mux = MultiMux3(2); @@ -44,75 +64,71 @@ template Window4() { // in[0] -> 1*BASE - mux.c[0][0] <== base[0]; - mux.c[1][0] <== base[1]; + mux.c[0][0] <== base.x; + mux.c[1][0] <== base.y; // in[1] -> 2*BASE - dbl2.in[0] <== base[0]; - dbl2.in[1] <== base[1]; - mux.c[0][1] <== dbl2.out[0]; - mux.c[1][1] <== dbl2.out[1]; + dbl2.pin <== base; + mux.c[0][1] <== dbl2.pout.x; + mux.c[1][1] <== dbl2.pout.y; // in[2] -> 3*BASE - adr3.in1[0] <== base[0]; - adr3.in1[1] <== base[1]; - adr3.in2[0] <== dbl2.out[0]; - adr3.in2[1] <== dbl2.out[1]; - mux.c[0][2] <== adr3.out[0]; - mux.c[1][2] <== adr3.out[1]; + adr3.pin1 <== base; + adr3.pin2 <== dbl2.pout; + mux.c[0][2] <== adr3.pout.x; + mux.c[1][2] <== adr3.pout.y; // in[3] -> 4*BASE - adr4.in1[0] <== base[0]; - adr4.in1[1] <== base[1]; - adr4.in2[0] <== adr3.out[0]; - adr4.in2[1] <== adr3.out[1]; - mux.c[0][3] <== adr4.out[0]; - mux.c[1][3] <== adr4.out[1]; + adr4.pin1 <== base; + adr4.pin2 <== adr3.pout; + mux.c[0][3] <== adr4.pout.x; + mux.c[1][3] <== adr4.pout.y; // in[4] -> 5*BASE - adr5.in1[0] <== base[0]; - adr5.in1[1] <== base[1]; - adr5.in2[0] <== adr4.out[0]; - adr5.in2[1] <== adr4.out[1]; - mux.c[0][4] <== adr5.out[0]; - mux.c[1][4] <== adr5.out[1]; + adr5.pin1 <== base; + adr5.pin2 <== adr4.pout; + mux.c[0][4] <== adr5.pout.x; + mux.c[1][4] <== adr5.pout.y; // in[5] -> 6*BASE - adr6.in1[0] <== base[0]; - adr6.in1[1] <== base[1]; - adr6.in2[0] <== adr5.out[0]; - adr6.in2[1] <== adr5.out[1]; - mux.c[0][5] <== adr6.out[0]; - mux.c[1][5] <== adr6.out[1]; + adr6.pin1 <== base; + adr6.pin2 <== adr5.pout; + mux.c[0][5] <== adr6.pout.x; + mux.c[1][5] <== adr6.pout.y; // in[6] -> 7*BASE - adr7.in1[0] <== base[0]; - adr7.in1[1] <== base[1]; - adr7.in2[0] <== adr6.out[0]; - adr7.in2[1] <== adr6.out[1]; - mux.c[0][6] <== adr7.out[0]; - mux.c[1][6] <== adr7.out[1]; + adr7.pin1 <== base; + adr7.pin2 <== adr6.pout; + mux.c[0][6] <== adr7.pout.x; + mux.c[1][6] <== adr7.pout.y; // in[7] -> 8*BASE - adr8.in1[0] <== base[0]; - adr8.in1[1] <== base[1]; - adr8.in2[0] <== adr7.out[0]; - adr8.in2[1] <== adr7.out[1]; - mux.c[0][7] <== adr8.out[0]; - mux.c[1][7] <== adr8.out[1]; - - out8[0] <== adr8.out[0]; - out8[1] <== adr8.out[1]; - - out[0] <== mux.out[0]; - out[1] <== - mux.out[1]*2*in[3] + mux.out[1]; // Negate y if in[3] is one + adr8.pin1 <== base; + adr8.pin2 <== adr7.pout; + mux.c[0][7] <== adr8.pout.x; + mux.c[1][7] <== adr8.pout.y; + + pout8 <== adr8.pout; + + pout.x <== mux.out[0]; + pout.y <== - mux.out[1]*2*in[3] + mux.out[1]; // Negate y if in[3] is one } +/* + +*** Segment(nWindows):template used to perform a segment of the multiplications needed to perform a the Pedersen protocol. + - Inputs: in[4 * nWindows] -> binary representation of the scalar + requires tag binary + base[2] -> input curve point in Edwards representation + - Outputs: out[2] -> output curve point in Edwards representation + + */ + template Segment(nWindows) { - signal input in[nWindows*4]; - signal input base[2]; - signal output out[2]; + input signal {binary} in[nWindows*4]; + input Point {babyedwards} base; + output Point {babyedwards} pout; var i; var j; @@ -120,8 +136,7 @@ template Segment(nWindows) { // Convert the base to montgomery component e2m = Edwards2Montgomery(); - e2m.in[0] <== base[0]; - e2m.in[1] <== base[1]; + e2m.pin <== base; component windows[nWindows]; component doublers1[nWindows-1]; @@ -133,49 +148,49 @@ template Segment(nWindows) { windows[i].in[j] <== in[4*i+j]; } if (i==0) { - windows[i].base[0] <== e2m.out[0]; - windows[i].base[1] <== e2m.out[1]; + windows[i].base <== e2m.pout; } else { doublers1[i-1] = MontgomeryDouble(); doublers2[i-1] = MontgomeryDouble(); - doublers1[i-1].in[0] <== windows[i-1].out8[0]; - doublers1[i-1].in[1] <== windows[i-1].out8[1]; - doublers2[i-1].in[0] <== doublers1[i-1].out[0]; - doublers2[i-1].in[1] <== doublers1[i-1].out[1]; + doublers1[i-1].pin <== windows[i-1].pout8; + doublers2[i-1].pin <== doublers1[i-1].pout; - windows[i].base[0] <== doublers2[i-1].out[0]; - windows[i].base[1] <== doublers2[i-1].out[1]; + windows[i].base <== doublers2[i-1].pout; adders[i-1] = MontgomeryAdd(); if (i==1) { - adders[i-1].in1[0] <== windows[0].out[0]; - adders[i-1].in1[1] <== windows[0].out[1]; + adders[i-1].pin1 <== windows[0].pout; } else { - adders[i-1].in1[0] <== adders[i-2].out[0]; - adders[i-1].in1[1] <== adders[i-2].out[1]; + adders[i-1].pin1 <== adders[i-2].pout; } - adders[i-1].in2[0] <== windows[i].out[0]; - adders[i-1].in2[1] <== windows[i].out[1]; + adders[i-1].pin2 <== windows[i].pout; } } component m2e = Montgomery2Edwards(); if (nWindows > 1) { - m2e.in[0] <== adders[nWindows-2].out[0]; - m2e.in[1] <== adders[nWindows-2].out[1]; + m2e.pin <== adders[nWindows-2].pout; } else { - m2e.in[0] <== windows[0].out[0]; - m2e.in[1] <== windows[0].out[1]; + m2e.pin <== windows[0].pout; } - out[0] <== m2e.out[0]; - out[1] <== m2e.out[1]; + pout <== m2e.pout; } + +/* + +*** Pedersen(n): template that performs the Pedersen protocol on the input in, that is the binary representation of the field using n bits. It calculates the output point of the Pedersen protocol in Edwards representation + - Inputs: in[n] -> binary representation of the scalar + requires tag binary + - Outputs: out[2] -> output curve point in Edwards representation + + */ + template Pedersen(n) { - signal input in[n]; - signal output out[2]; + input signal {binary} in[n]; + output Point {babyedwards} pout; var BASE[10][2] = [ [10457101036533406547632367118273992217979173478358440826365724437999023779287,19824078218392094440610104313265183977899662750282163392862422243483260492317], @@ -199,18 +214,22 @@ template Pedersen(n) { var j; var nBits; var nWindows; + Point {babyedwards} aux[nSegments]; + + signal {binary} aux_0 <== 0; for (i=0; i1) { - packPoint.in[0] <== adders[nSegments-2].xout; - packPoint.in[1] <== adders[nSegments-2].yout; - } else { - packPoint.in[0] <== segments[0].out[0]; - packPoint.in[1] <== segments[0].out[1]; - } - - out[0] <== packPoint.out[0]; - out[1] <== packPoint.out[1]; -*/ if (nSegments>1) { - out[0] <== adders[nSegments-2].xout; - out[1] <== adders[nSegments-2].yout; + pout <== adders[nSegments-2].pout; } else { - out[0] <== segments[0].out[0]; - out[1] <== segments[0].out[1]; + pout <== segments[0].pout; } } diff --git a/circuits/pedersen_old.circom b/circuits/pedersen_old.circom index c338e44f..6be981d6 100644 --- a/circuits/pedersen_old.circom +++ b/circuits/pedersen_old.circom @@ -16,13 +16,25 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "escalarmul.circom"; +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) + +include "escalarmul/escalarmul.circom"; +include "buses.circom"; + +/* + +*** Pedersen(n): template that performs the Pedersen protocol on the input in, that is the binary representation of a value x using n bits. It calculates the output point of the protocol out in Edwards representation + - Inputs: in[n] -> binary representation of the scalar + requires tag binary + - Outputs: out[2] -> output curve point in Edwards representation + + */ template Pedersen(n) { - signal input in[n]; - signal output out[2]; + input signal {binary} in[n]; + output Point {babyedwards} pout; var nexps = ((n-1) \ 250) + 1; var nlastbits = n - (nexps-1)*250; @@ -46,6 +58,9 @@ template Pedersen(n) { var i; var j; var nexpbits; + Point {babyedwards} paux; // Auxiliar point [0, 1] + paux.x <== 0; + paux.y <== 1; for (i=0; i out[0]; - escalarMuls[nexps-1].out[1] ==> out[1]; + escalarMuls[nexps-1].pout ==> pout; } diff --git a/circuits/pointbits.circom b/circuits/pointbits.circom index fa6007db..7b0260d2 100644 --- a/circuits/pointbits.circom +++ b/circuits/pointbits.circom @@ -16,13 +16,22 @@ You should have received a copy of the GNU General Public License along with circom. If not, see . */ -pragma circom 2.0.0; +pragma circom 2.1.5; + +// The templates and functions of this file only work for prime field bn128 (21888242871839275222246405745257275088548364400416034343698204186575808495617) include "bitify.circom"; include "aliascheck.circom"; -include "compconstant.circom"; +include "comparators.circom"; include "babyjub.circom"; +include "buses.circom"; + +/* +*** sqrt(n): function that returns the square of the value n. + That is, it returns a value r s.t. r * r = n mod p + + */ function sqrt(n) { @@ -69,96 +78,93 @@ function sqrt(n) { return r; } +/* + +*** Bits2Point_Strict(): template that receives the encoding of a point of a curve using 256 bits and returns its Edwards representation + - Inputs: in[256] -> encoding of the point using 256 bits + requires tag binary + - Outputs: out[2] -> curve point using Edwards representation + + Encoding: + in[0..253] -> binary representation of out[1] + in[254] -> 0 + in[255] -> if out[0] is positive then 0, else 1 +*/ -template Bits2Point() { - signal input in[256]; - signal output out[2]; -} template Bits2Point_Strict() { - signal input in[256]; - signal output out[2]; + BinaryPoint(254) input in; + output Point {babyedwards} pout; var i; // Check aliasing component aliasCheckY = AliasCheck(); - for (i=0; i<254; i++) { - aliasCheckY.in[i] <== in[i]; - } - in[254] === 0; + aliasCheckY.in <== in.binY; component b2nY = Bits2Num(254); - for (i=0; i<254; i++) { - b2nY.in[i] <== in[i]; - } + b2nY.in <== in.binY; - out[1] <== b2nY.out; + pout.y <== b2nY.out; var a = 168700; var d = 168696; - var y2 = out[1] * out[1]; + var y2 = pout.y * pout.y; var x = sqrt( (1-y2)/(a - d*y2) ); - if (in[255] == 1) x = -x; + if (in.signX == 1) x = -x; - out[0] <-- x; + pout.x <-- x; component babyCheck = BabyCheck(); - babyCheck.x <== out[0]; - babyCheck.y <== out[1]; + babyCheck.pin <== pout; component n2bX = Num2Bits(254); - n2bX.in <== out[0]; + n2bX.in <== pout.x; component aliasCheckX = AliasCheck(); - for (i=0; i<254; i++) { - aliasCheckX.in[i] <== n2bX.out[i]; - } + aliasCheckX.in <== n2bX.out; - component signCalc = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808); - for (i=0; i<254; i++) { - signCalc.in[i] <== n2bX.out[i]; - } + component signCalc = CompConstant(maxbits(), 10944121435919637611123202872628637544274182200208017171849102093287904247808); + signCalc.in <== n2bX.out; - signCalc.out === in[255]; + signCalc.out === in.signX; } -template Point2Bits() { - signal input in[2]; - signal output out[256]; - +/* -} +*** Point2Bits_Strict(): template that receives a point as an input and returns its encoding using 256 bits + - Inputs: in[2] -> curve point using Edwards representation + - Outputs: out[256] -> encoding of the point using 256 bits + satisfies tag binary + + Encoding: + out[0..253] -> binary representation of in[1] + out[254] -> 0 + out[255] -> if in[0] is positive then 0, else 1 +*/ template Point2Bits_Strict() { - signal input in[2]; - signal output out[256]; + input Point pin; + BinaryPoint(254) output out; var i; component n2bX = Num2Bits(254); - n2bX.in <== in[0]; + n2bX.in <== pin.x; component n2bY = Num2Bits(254); - n2bY.in <== in[1]; + n2bY.in <== pin.y; component aliasCheckX = AliasCheck(); component aliasCheckY = AliasCheck(); - for (i=0; i<254; i++) { - aliasCheckX.in[i] <== n2bX.out[i]; - aliasCheckY.in[i] <== n2bY.out[i]; - } + aliasCheckX.in <== n2bX.out; + aliasCheckY.in <== n2bY.out; - component signCalc = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808); - for (i=0; i<254; i++) { - signCalc.in[i] <== n2bX.out[i]; - } + component signCalc = CompConstant(maxbits(), 10944121435919637611123202872628637544274182200208017171849102093287904247808); + signCalc.in <== n2bX.out; - for (i=0; i<254; i++) { - out[i] <== n2bY.out[i]; - } - out[254] <== 0; - out[255] <== signCalc.out; + out.binY <== n2bY.out; + out.signX <== signCalc.out; } diff --git a/circuits/poseidon.circom b/circuits/poseidon.circom index 1c45ab95..3e86ea28 100644 --- a/circuits/poseidon.circom +++ b/circuits/poseidon.circom @@ -1,10 +1,23 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; + + +// The templates and functions in this file are general and work for any prime field include "./poseidon_constants.circom"; +/* + +*** Sigma(): template that receives an input in an returns the value in ** 5: + - Inputs: in -> field value + - Outputs: out -> field value + + Example: Sigma()(2) = 32 + */ + + template Sigma() { - signal input in; - signal output out; + input signal in; + output signal out; signal in2; signal in4; @@ -15,18 +28,43 @@ template Sigma() { out <== in4*in; } + +/* + +*** Ark(t, C, r): template that receives an input array of signals in of length t, and returns the array out of length t such that for each position of the array out[i] = in[i] + C[i+r] with C and r parameters of the template (r is the shifting to be used and C the values to be added) + - Inputs: in[t] -> field value + - Outputs: out[t] -> field value + + Ark(2, [1, 2, 3, 4], 2)([5, 5]) = [8, 9] + + Obs: C is expected to be an array of length at least t + r + +*/ + template Ark(t, C, r) { - signal input in[t]; - signal output out[t]; + input signal in[t]; + output signal out[t]; for (var i=0; i field value + - Outputs: out[t] -> field value + + Mix(2, [[1, 2], [3, 4]])([1, 0]) = [1, 3] + + Obs: M is expected to be a matrix of dimensions at least t * t + +*/ + template Mix(t, M) { - signal input in[t]; - signal output out[t]; + input signal in[t]; + output signal out[t]; var lc; for (var i=0; i field value + - Outputs: out -> field value + + MixLast(2, [[1, 2], [3, 4]], 1)([1, 0]) = 3 + + Obs: M is expected to be a matrix of dimensions at leadt t * t, s is a value between 0..t-1 + +*/ + template MixLast(t, M, s) { - signal input in[t]; - signal output out; + input signal in[t]; + output signal out; var lc = 0; for (var j=0; j field value + - Outputs: out -> field value +*/ + + template MixS(t, S, r) { - signal input in[t]; - signal output out[t]; + input signal in[t]; + output signal out[t]; var lc = 0; @@ -64,10 +126,20 @@ template MixS(t, S, r) { } } + + +/* + +*** PoseidonEx(nInputs, nOuts): template that implements the Poseidon hash protocol for nInputs and nOuts. The circuit receives the inputs to be hashed, the initial state and returns the hashed values + - Inputs: inputs[nInputs] -> field value + initialState -> field value + - Outputs: out[nOuts] -> field value +*/ + template PoseidonEx(nInputs, nOuts) { - signal input inputs[nInputs]; - signal input initialState; - signal output out[nOuts]; + input signal inputs[nInputs]; + input signal initialState; + output signal out[nOuts]; // Using recommended parameters from whitepaper https://eprint.iacr.org/2019/458.pdf (table 2, table 8) // Generated by https://extgit.iaik.tugraz.at/krypto/hadeshash/-/blob/master/code/calc_round_numbers.py @@ -195,9 +267,18 @@ template PoseidonEx(nInputs, nOuts) { } + + +/* + +*** Poseidon(nInputs): template that implements the Poseidon hash protocol for nInputs. The circuit receives the inputs to be hashed and returns the hashed values. It takes the value 0 as initial state. + - Inputs: inputs[nInputs] -> field value + - Outputs: out -> field value +*/ + template Poseidon(nInputs) { - signal input inputs[nInputs]; - signal output out; + input signal inputs[nInputs]; + output signal out; component pEx = PoseidonEx(nInputs, 1); pEx.initialState <== 0; diff --git a/circuits/poseidon_old.circom b/circuits/poseidon_old.circom index b8e2316b..39d9d2ed 100644 --- a/circuits/poseidon_old.circom +++ b/circuits/poseidon_old.circom @@ -1,10 +1,23 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "./poseidon_constants.circom"; + +// The templates and functions in this file are general and work for any prime field + +include "./poseidon_constants_old.circom"; + + +/* + +*** Sigma(): template that receives an input in an returns the value in ** 5: + - Inputs: in -> field value + - Outputs: out -> field value + + Example: Sigma()(2) = 32 + */ template Sigma() { - signal input in; - signal output out; + input signal in; + output signal out; signal in2; signal in4; @@ -15,18 +28,42 @@ template Sigma() { out <== in4*in; } +/* + +*** Ark(t, C, r): template that receives an input array of signals in of length t, and returns the array out of length t such that for each position of the array out[i] = in[i] + C[i+r] with C and r parameters of the template (r is the shifting to be used and C the values to be added) + - Inputs: in[t] -> field value + - Outputs: out[t] -> field value + + Ark(2, [1, 2, 3, 4], 2)([5, 5]) = [8, 9] + + Obs: C is expected to be an array of length at least t + r + +*/ + template Ark(t, C, r) { - signal input in[t]; - signal output out[t]; + input signal in[t]; + output signal out[t]; for (var i=0; i field value + - Outputs: out[t] -> field value + + Mix(2, [[1, 2], [3, 4]])([1, 0]) = [1, 3] + + Obs: M is expected to be a matrix of dimensions at least t * t + +*/ + template Mix(t, M) { - signal input in[t]; - signal output out[t]; + input signal in[t]; + output signal out[t]; var lc; for (var i=0; i field value + - Outputs: out -> field value +*/ + + template Poseidon(nInputs) { - signal input inputs[nInputs]; - signal output out; + input signal inputs[nInputs]; + output signal out; // Using recommended parameters from whitepaper https://eprint.iacr.org/2019/458.pdf (table 2, table 8) // Generated by https://extgit.iaik.tugraz.at/krypto/hadeshash/-/blob/master/code/calc_round_numbers.py diff --git a/circuits/sha256/ch.circom b/circuits/sha256/ch.circom index e95f6acc..ef1155c3 100644 --- a/circuits/sha256/ch.circom +++ b/circuits/sha256/ch.circom @@ -36,10 +36,10 @@ out = a*(b-c) + c pragma circom 2.0.0; template Ch_t(n) { - signal input a[n]; - signal input b[n]; - signal input c[n]; - signal output out[n]; + input signal {binary} a[n]; + input signal {binary} b[n]; + input signal {binary} c[n]; + output signal {binary} out[n]; for (var k=0; k= n) { diff --git a/circuits/sha256/sigma.circom b/circuits/sha256/sigma.circom index bcb0b805..8095e3e1 100644 --- a/circuits/sha256/sigma.circom +++ b/circuits/sha256/sigma.circom @@ -23,8 +23,8 @@ include "rotate.circom"; include "shift.circom"; template SmallSigma(ra, rb, rc) { - signal input in[32]; - signal output out[32]; + input signal {binary} in[32]; + output signal {binary} out[32]; var k; component rota = RotR(32, ra); @@ -50,8 +50,8 @@ template SmallSigma(ra, rb, rc) { } template BigSigma(ra, rb, rc) { - signal input in[32]; - signal output out[32]; + input signal {binary} in[32]; + output signal {binary} out[32]; var k; component rota = RotR(32, ra); diff --git a/circuits/sha256/sigmaplus.circom b/circuits/sha256/sigmaplus.circom index 35e3300a..2d504a3d 100644 --- a/circuits/sha256/sigmaplus.circom +++ b/circuits/sha256/sigmaplus.circom @@ -22,11 +22,11 @@ include "../binsum.circom"; include "sigma.circom"; template SigmaPlus() { - signal input in2[32]; - signal input in7[32]; - signal input in15[32]; - signal input in16[32]; - signal output out[32]; + input signal {binary} in2[32]; + input signal {binary} in7[32]; + input signal {binary} in15[32]; + input signal {binary} in16[32]; + output signal {binary} out[32]; var k; component sigma1 = SmallSigma(17,19,10); diff --git a/circuits/sha256/t1.circom b/circuits/sha256/t1.circom index e606772f..c8707b79 100644 --- a/circuits/sha256/t1.circom +++ b/circuits/sha256/t1.circom @@ -23,13 +23,13 @@ include "sigma.circom"; include "ch.circom"; template T1() { - signal input h[32]; - signal input e[32]; - signal input f[32]; - signal input g[32]; - signal input k[32]; - signal input w[32]; - signal output out[32]; + input signal {binary} h[32]; + input signal {binary} e[32]; + input signal {binary} f[32]; + input signal {binary} g[32]; + input signal {binary} k[32]; + input signal {binary} w[32]; + output signal {binary} out[32]; var ki; diff --git a/circuits/sha256/t2.circom b/circuits/sha256/t2.circom index 5a83d594..331341ab 100644 --- a/circuits/sha256/t2.circom +++ b/circuits/sha256/t2.circom @@ -23,10 +23,10 @@ include "sigma.circom"; include "maj.circom"; template T2() { - signal input a[32]; - signal input b[32]; - signal input c[32]; - signal output out[32]; + input signal {binary} a[32]; + input signal {binary} b[32]; + input signal {binary} c[32]; + output signal {binary} out[32]; var k; component bigsigma0 = BigSigma(2, 13, 22); diff --git a/circuits/sha256/xor3.circom b/circuits/sha256/xor3.circom index 9c21e4e2..33c7aeb9 100644 --- a/circuits/sha256/xor3.circom +++ b/circuits/sha256/xor3.circom @@ -32,11 +32,11 @@ out = a*( 1 - 2*b -2*c + 4*mid ) + b + c - 2 * mid pragma circom 2.0.0; template Xor3(n) { - signal input a[n]; - signal input b[n]; - signal input c[n]; - signal output out[n]; - signal mid[n]; + input signal {binary} a[n]; + input signal {binary} b[n]; + input signal {binary} c[n]; + output signal {binary} out[n]; + signal {binary} mid[n]; for (var k=0; k. */ -pragma circom 2.0.0; -include "compconstant.circom"; +/* -template Sign() { - signal input in[254]; - signal output sign; +Defines a bus that represents a state of the state machine (sm) used to perform the smt hashing. +See smtverifiersm.circom to see more details of the behavior of this machine - component comp = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808); +*/ + pragma circom 2.1.9; - var i; - for (i=0; i<254; i++) { - comp.in[i] <== in[i]; - } +bus SMTVerifierState() { + signal top; + signal i0; + signal iold; + signal inew; + signal na; +} - sign <== comp.out; + +bus SMTProcessorState() { + signal top; + signal old0; + signal bot; + signal new1; + signal na; + signal upd; } + diff --git a/circuits/smt/smthash_mimc.circom b/circuits/smt/smthash_mimc.circom index 272e5270..bb23e461 100644 --- a/circuits/smt/smthash_mimc.circom +++ b/circuits/smt/smthash_mimc.circom @@ -26,9 +26,9 @@ include "../mimc.circom"; */ template SMTHash1() { - signal input key; - signal input value; - signal output out; + input signal key; + input signal value; + output signal out; component h = MultiMiMC7(2, 91); // Constant h.in[0] <== key; @@ -45,9 +45,9 @@ template SMTHash1() { */ template SMTHash2() { - signal input L; - signal input R; - signal output out; + input signal L; + input signal R; + output signal out; component h = MultiMiMC7(2, 91); // Constant h.in[0] <== L; diff --git a/circuits/smt/smthash_poseidon.circom b/circuits/smt/smthash_poseidon.circom index aa6b8b3a..60e2433d 100644 --- a/circuits/smt/smthash_poseidon.circom +++ b/circuits/smt/smthash_poseidon.circom @@ -26,9 +26,9 @@ include "../poseidon.circom"; */ template SMTHash1() { - signal input key; - signal input value; - signal output out; + input signal key; + input signal value; + output signal out; component h = Poseidon(3); // Constant h.inputs[0] <== key; @@ -45,9 +45,9 @@ template SMTHash1() { */ template SMTHash2() { - signal input L; - signal input R; - signal output out; + input signal L; + input signal R; + output signal out; component h = Poseidon(2); // Constant h.inputs[0] <== L; diff --git a/circuits/smt/smtlevins.circom b/circuits/smt/smtlevins.circom index a03ae50a..13718c61 100644 --- a/circuits/smt/smtlevins.circom +++ b/circuits/smt/smtlevins.circom @@ -75,9 +75,9 @@ a parent with a sibling != 0. pragma circom 2.0.0; template SMTLevIns(nLevels) { - signal input enabled; - signal input siblings[nLevels]; - signal output levIns[nLevels]; + input signal {binary} enabled; + input signal siblings[nLevels]; + output signal {binary} levIns[nLevels]; signal done[nLevels-1]; // Indicates if the insLevel has aready been detected. var i; diff --git a/circuits/smt/smtprocessor.circom b/circuits/smt/smtprocessor.circom index b75f17c7..b79d4607 100644 --- a/circuits/smt/smtprocessor.circom +++ b/circuits/smt/smtprocessor.circom @@ -129,6 +129,7 @@ fnc[0] fnc[1] ***************************************************************************************************/ pragma circom 2.0.0; +include "smtbuses.circom"; include "../gates.circom"; include "../bitify.circom"; include "../comparators.circom"; @@ -139,17 +140,17 @@ include "smtprocessorsm.circom"; include "smthash_poseidon.circom"; template SMTProcessor(nLevels) { - signal input oldRoot; - signal output newRoot; - signal input siblings[nLevels]; - signal input oldKey; - signal input oldValue; - signal input isOld0; - signal input newKey; - signal input newValue; - signal input fnc[2]; - - signal enabled; + input signal oldRoot; + output signal newRoot; + input signal siblings[nLevels]; + input signal oldKey; + input signal oldValue; + input signal {binary} isOld0; + input signal newKey; + input signal newValue; + input signal {binary} fnc[2]; + + signal {binary} enabled; var i; @@ -184,19 +185,14 @@ template SMTProcessor(nLevels) { for (i=0; i VERIFY INCLUSION 1 -> VERIFY NOT INCLUSION */ - pragma circom 2.0.0; - + pragma circom 2.1.9; +include "smtbuses.circom"; include "../gates.circom"; include "../bitify.circom"; include "../comparators.circom"; @@ -39,15 +39,15 @@ include "smtverifiersm.circom"; include "smthash_poseidon.circom"; template SMTVerifier(nLevels) { - signal input enabled; - signal input root; - signal input siblings[nLevels]; - signal input oldKey; - signal input oldValue; - signal input isOld0; - signal input key; - signal input value; - signal input fnc; + input signal {binary} enabled; + input signal root; + input signal siblings[nLevels]; + input signal oldKey; + input signal oldValue; + input signal {binary} isOld0; + input signal key; + input signal value; + input signal {binary} fnc; var i; @@ -73,33 +73,25 @@ template SMTVerifier(nLevels) { for (i=0; i. */ +pragma circom 2.1.5; + +// The templates and functions in this file are general and work for any prime field + + /* - Assume sel is binary. - If sel == 0 then outL = L and outR=R - If sel == 1 then outL = R and outR=L +*** Switcher(): template that receives three inputs: L, R and sel with sel being a binary value, and switchs the value of L and R in case sel == 1, that it returns the values outL and outR such that: + - If sel == 0 then outL = L and outR=R + - If sel == 1 then outL = R and outR=L + + - Inputs: sel -> binary value + requires tag binary + L -> field element + R -> field element + - Output: outL -> field element, if sel == 0 then L, else R + outR -> field element, if sel == 0 then R, else L + + Example: Switcher()(1, 4, 7) = (7, 4) */ - -pragma circom 2.0.0; template Switcher() { - signal input sel; - signal input L; - signal input R; - signal output outL; - signal output outR; + input signal {binary} sel; + input signal L; + input signal R; + output signal outL; + output signal outR; signal aux; diff --git a/circuits/tags-managing.circom b/circuits/tags-managing.circom new file mode 100644 index 00000000..6828f242 --- /dev/null +++ b/circuits/tags-managing.circom @@ -0,0 +1,210 @@ +/* + 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.5; + +include "comparators.circom"; +include "bitify.circom"; + + +// The templates and functions in this file are general and work for any prime field + + + +/* +*** BinaryCheck(n): template that adds the constraints needed to ensure that a signal in is binary and adds the tag binary to the input + - Inputs: in -> field value + - Output: out -> same value as in, but including binary tag + satisfies tag binary + + Example: BinaryCheck()(1) = 1 + Note: in case the input in is not binary then the generated system of constraints does not have any solution for that input. + For instance, BinaryCheck()(10) -> no solution + +*/ + +template BinaryCheck () { + input signal in; + output signal {binary} out; + + in * (in - 1) === 0; + out <== in; +} + +/* +*** BinaryCheckArray(n): template that adds the constraints needed to ensure that all signal of an array of n elements are binary and adds the tag binary to the input + - Inputs: in[n] -> array of n field elements + - Output: out[n] -> same value as in, but including binary tag + satisfies tag binary + + Example: BinaryCheckArray(2)([0,1]) = [0,1] + Note: in case the input contains a non binary element then the generated system of constraints does not have any solution for that input. + For instance, BinaryCheckArray(2)([0,10]) -> no solution + +*/ + +template BinaryCheckArray(n) { + input signal in[n]; + output signal {binary} out[n]; + + for (var i = 0; i < n; i++) { + out[i] <== BinaryCheck()(in[i]); + } +} + + +/* +*** MaxbitCheck(n): template that adds the constraints needed to ensure that a signal can be expressed using n bits(that is, that is value is in [0, 2**n)) and adds the tag maxbit = n to the input + - Inputs: in -> field value + - Output: out -> same value as in, but including maxbit tag with out.maxbit = n + satisfies tag out.maxbit = n + + Example: MaxbitCheck(5)(14) = 14 + Note: in case the input in does not satisfy the specification of maxbit then the generated system of constraints does not have any solution for that input. + For instance, MaxbitCheck(3)(100) -> no solution + +*/ + +template MaxbitCheck(n) { + input signal in; + output signal {maxbit} out; + + _ <== Num2Bits(n)(in); + + out.maxbit = n; + out <== in; +} + +/* +*** MaxbitCheckArray(n): template that adds the constraints needed to ensure that the signals an array of length m can be expressed using n bits(that is, that is value is in [0, 2**n)) and adds the tag maxbit = n to the input + - Inputs: in[m] -> array of m field values + - Output: out[m] -> same values as in, but including maxbit tag with out.maxbit = n + satisfies tag out.maxbit = n + + Example: MaxbitCheckArray(5, 2)([3,14]) = [3, 14] with tag maxbit = 5 + Note: in case the a signal of the input in does not satisfy the specification of maxbit then the generated system of constraints does not have any solution for that input. + For instance, MaxbitCheckArray(3, 2)([3, 100]) -> no solution + +*/ + + +template MaxbitCheckArray(n,m) { + input signal in[m]; + output signal {maxbit} out[m]; + + out.maxbit = n; + + for (var i = 0; i < m; i++) { + out[i] <== MaxbitCheck(n)(in[i]); + } + +} + + +/* +*** MaxValueCheck(ct): template that receives an input, checks its value is smaller than or equal to the constant value ct given as a parameter, and returns the same input but with the tag maxvalue with value ct + - Inputs: in -> field number + - Outputs: out -> field number + satisfies tag maxvalue with value ct + + Example: MaxValueCheck(15)(14) = 14 and can be satisfied + Note: in case the input in does not satisfy the specification of max then the generated system of constraints does not have any solution for that input. + For instance, MaxValueCheck(3)(100) -> no solution +*/ + +template MaxValueCheck(ct){ + input signal in; + output signal {maxvalue} out; + + signal res <== CompConstant(nbits(ct), ct)(Num2Bits(nbits(ct))(in)); + res === 0; + out.maxvalue = ct; + out <== in; +} + +/* +*** MinValueCheck(ct): template that receives an input, checks its value is greater than or equal to the constant value ct given as a parameter, and returns the same input but with the tag minvalue with value ct + - Inputs: in -> field number + - Outputs: out -> field number + satisfies tag minvalue with value ct +*/ + +template MinValueCheck(ct){ + input signal in; + output signal {minvalue} out; + + signal res <== CompConstant(maxbits(), ct-1)(Num2Bits(maxbits())(in)); + res === 1; + out.minvalue = ct; + out <== in; +} + +/* +*** MinMaxValueCheck(ct): template that receives an input, checks its value is greater than or equal to the constant value ct1 given as a first parameter and smaller than or equal to the constant value ct2 given as a second parameter, and returns the same input but with the tag minvalue with value ct1 and the tag maxvalue with value ct2 + - Inputs: in -> field number + - Outputs: out -> field number + satisfies tag minvalue with value ct1 + satisfies tag maxvalue with value ct2 +*/ + +template MinMaxValueCheck(ct1,ct2){ + input signal in; + output signal {minvalue,maxvalue} out; + + var n = nbits(ct2); + + signal inb[n] <== Num2Bits(n)(in); + signal res1 <== CompConstant(n, ct1-1)(inb); + res1 === 1; + out.minvalue = ct1; + signal res2 <== CompConstant(n, ct2)(inb); + res2 === 0; + out.maxvalue = ct2; + out <== in; +} + +/* +*** MaxAbsValueTagCheck(n): template that adds the constraints needed to ensure that the absolute value of a signal is smaller or equal than a given value n and adds the tag max_abs = n to the input + - Inputs: in -> field value + - Output: out -> same value as in, but including max_abs tag with out.max_abs = n + satisfies tag out.max_abs = n + + Example: MaxValueTagCheck(15)(-14) = 14 and can be satisfied + Note: in case the input in does not satisfy the specification of max_abs then the generated system of constraints does not have any solution for that input. + For instance, MaxAbsValueTagCheck(33)(-100) -> no solution + +*/ + +template MaxAbsValueTagCheck(n){ + input signal in; + output signal {max_abs} out; + + var needed_bits = nbits(2 * n); + + signal {maxbit} aux[2]; + aux.maxbit = needed_bits; + aux[0] <== MaxbitCheck(needed_bits)(in + n); // to ensure that 0 <= aux[0] < 2**nbits(2 * n) + aux[1] <== 2 * n; + + signal out1 <== LessEqThan(n)(aux); // checks that 0 <= in + n <= 2 * n <==> -n <= in <= n + out1 === 1; + + out.max_abs = n; + out <== in; +} + diff --git a/test/circuits/aliascheck_test.circom b/test/circuits/aliascheck_test.circom index 942b77c8..937435eb 100644 --- a/test/circuits/aliascheck_test.circom +++ b/test/circuits/aliascheck_test.circom @@ -1,4 +1,15 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/aliascheck.circom"; +include "../../circuits/tags-managing.circom"; -component main = AliasCheck(); + +template Main(){ + input signal in[254]; + + component ac = AliasCheck(); + ac.in <== BinaryCheckArray(254)(in); + + +} + +component main = Main(); diff --git a/test/circuits/babyadd_tester.circom b/test/circuits/babyadd_tester.circom index 18c9d8c6..78933a44 100644 --- a/test/circuits/babyadd_tester.circom +++ b/test/circuits/babyadd_tester.circom @@ -1,4 +1,14 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/babyjub.circom"; -component main = BabyAdd(); +template Main(){ + input Point a; + input Point b; + //output Point out <== BabyAdd()(BabyCheck()(a), BabyCheck()(b)); + Point {babyedwards} a_aux <== a; + Point {babyedwards} b_aux <== b; + output Point out <== BabyAdd()(a_aux, b_aux); +} + + +component main = Main(); diff --git a/test/circuits/babycheck_test.circom b/test/circuits/babycheck_test.circom index bdcdc699..7fc34ea5 100644 --- a/test/circuits/babycheck_test.circom +++ b/test/circuits/babycheck_test.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/babyjub.circom"; component main = BabyCheck(); diff --git a/test/circuits/babypbk_test.circom b/test/circuits/babypbk_test.circom index 5e1f8a54..bdc35dd7 100644 --- a/test/circuits/babypbk_test.circom +++ b/test/circuits/babypbk_test.circom @@ -1,4 +1,14 @@ pragma circom 2.0.0; include "../../circuits/babyjub.circom"; +include "../../circuits/tags-managing.circom"; -component main = BabyPbk(); +template BabyPbk_aux() { + input signal in; + output Point {babyedwards} pout; + + var r = 2736030358979909402780800718157159386076813972158567259200215660948447373041; + signal in_aux <== MinMaxValueCheck(1,r-1)(in); + pout <== BabyPbk()(in_aux); +} + +component main = BabyPbk_aux(); diff --git a/test/circuits/binsub_test.circom b/test/circuits/binsub_test.circom index 33cd1a48..d8170793 100644 --- a/test/circuits/binsub_test.circom +++ b/test/circuits/binsub_test.circom @@ -1,12 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/bitify.circom"; include "../../circuits/binsub.circom"; +include "../../circuits/buses.circom"; template A() { - signal input a; //private - signal input b; - signal output out; + input signal a; //private + input signal b; + output signal out; var i; @@ -18,14 +19,10 @@ template A() { n2ba.in <== a; n2bb.in <== b; - for (i=0; i<16; i++) { - sub.in[0][i] <== n2ba.out[i]; - sub.in[1][i] <== n2bb.out[i]; - } - - for (i=0; i<16; i++) { - b2n.in[i] <== sub.out[i]; - } + sub.in[0] <== n2ba.out; + sub.in[1] <== n2bb.out; + + b2n.in <== sub.out; out <== b2n.out; } diff --git a/test/circuits/sum_test.circom b/test/circuits/binsum_test.circom similarity index 53% rename from test/circuits/sum_test.circom rename to test/circuits/binsum_test.circom index b0be22f3..6b269dfe 100644 --- a/test/circuits/sum_test.circom +++ b/test/circuits/binsum_test.circom @@ -4,28 +4,24 @@ include "../../circuits/bitify.circom"; include "../../circuits/binsum.circom"; template A() { - signal input a; //private - signal input b; - signal output out; + input signal a; //private + input signal b; + output signal out; var i; component n2ba = Num2Bits(32); component n2bb = Num2Bits(32); component sum = BinSum(32,2); - component b2n = Bits2Num(32); + component b2n = Bits2Num(33); n2ba.in <== a; n2bb.in <== b; - for (i=0; i<32; i++) { - sum.in[0][i] <== n2ba.out[i]; - sum.in[1][i] <== n2bb.out[i]; - } + sum.in[0] <== n2ba.out; + sum.in[1] <== n2bb.out; - for (i=0; i<32; i++) { - b2n.in[i] <== sum.out[i]; - } + b2n.in <== sum.out; out <== b2n.out; } diff --git a/test/circuits/bitify_test.circom b/test/circuits/bitify_test.circom new file mode 100644 index 00000000..ab70af52 --- /dev/null +++ b/test/circuits/bitify_test.circom @@ -0,0 +1,13 @@ +pragma circom 2.1.5; +include "../../circuits/bitify.circom"; + +template Main(n) { + signal input in; + + signal {binary} aux[n] <== Num2Bits(n)(in); + signal {maxbit} aux2 <== Bits2Num(n)(aux); + assert(aux2.maxbit == n); + in === aux2; +} + +component main = Main(30); diff --git a/test/circuits/constants_test.circom b/test/circuits/constants_test.circom index 1acb271d..2b4b0122 100644 --- a/test/circuits/constants_test.circom +++ b/test/circuits/constants_test.circom @@ -3,7 +3,7 @@ pragma circom 2.0.0; include "../../circuits/sha256/constants.circom"; template A() { - signal input in; + input signal in; component h0; h0 = K(8); diff --git a/test/circuits/eddsa_test.circom b/test/circuits/eddsa_test.circom deleted file mode 100644 index b04ef9b3..00000000 --- a/test/circuits/eddsa_test.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/eddsa.circom"; - -component main = EdDSAVerifier(80); diff --git a/test/circuits/eddsamimc_test.circom b/test/circuits/eddsamimc_test.circom deleted file mode 100644 index ca1a9791..00000000 --- a/test/circuits/eddsamimc_test.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/eddsamimc.circom"; - -component main = EdDSAMiMCVerifier(); diff --git a/test/circuits/eddsapedersen_old_test.circom b/test/circuits/eddsapedersen_old_test.circom new file mode 100644 index 00000000..42d2bede --- /dev/null +++ b/test/circuits/eddsapedersen_old_test.circom @@ -0,0 +1,46 @@ +pragma circom 2.1.5; + +include "../../circuits/eddsapedersen_old.circom"; +include "../../circuits/tags-managing.circom"; + +template A(n){ + signal input msg[n]; + + input signal A[256]; + input signal R8[256]; + input signal S[256]; + + BinaryPoint(254) A_aux; + BinaryPoint(254) R8_aux; + BinaryPoint(254) S_aux; + + signal {binary} msg_aux[n] <== BinaryCheckArray(n)(msg); + component check_a = BinaryCheckArray(256); + check_a.in <== A; + for (var i = 0; i < 254; i++){ + check_a.out[i] ==> A_aux.binY[i]; + } + check_a.out[254] === 0; + check_a.out[255] ==> A_aux.signX; + component check_R8 = BinaryCheckArray(256); + check_R8.in <== R8; + for (var i = 0; i < 254; i++){ + check_R8.out[i] ==> R8_aux.binY[i]; + } + check_R8.out[254] === 0; + check_R8.out[255] ==> R8_aux.signX; + component check_S = BinaryCheckArray(256); + check_S.in <== S; + for (var i = 0; i < 254; i++){ + check_S.out[i] ==> S_aux.binY[i]; + } + check_S.out[254] === 0; + check_S.out[255] ==> S_aux.signX; + + + EdDSAPedersenVerifier(n)(msg_aux, A_aux, R8_aux, S_aux); + +} + +component main = A(80); + diff --git a/test/circuits/eddsapedersen_test.circom b/test/circuits/eddsapedersen_test.circom new file mode 100644 index 00000000..d3d23bb3 --- /dev/null +++ b/test/circuits/eddsapedersen_test.circom @@ -0,0 +1,43 @@ +pragma circom 2.1.5; + +include "../../circuits/eddsapedersen.circom"; +include "../../circuits/tags-managing.circom"; + +template A(n){ + signal input msg[n]; + + input signal A[255]; + input signal R8[255]; + input signal S[255]; + + BinaryPoint(254) A_aux; + BinaryPoint(254) R8_aux; + BinaryPoint(254) S_aux; + + signal {binary} msg_aux[n] <== BinaryCheckArray(n)(msg); + component check_a = BinaryCheckArray(255); + check_a.in <== A; + for (var i = 0; i < 254; i++){ + check_a.out[i] ==> A_aux.binY[i]; + } + check_a.out[254] ==> A_aux.signX; + component check_R8 = BinaryCheckArray(255); + check_R8.in <== R8; + for (var i = 0; i < 254; i++){ + check_R8.out[i] ==> R8_aux.binY[i]; + } + check_R8.out[254] ==> R8_aux.signX; + component check_S = BinaryCheckArray(255); + check_S.in <== S; + for (var i = 0; i < 254; i++){ + check_S.out[i] ==> S_aux.binY[i]; + } + check_S.out[254] ==> S_aux.signX; + + + EdDSAPedersenVerifier(n)(msg_aux, A_aux, R8_aux, S_aux); + +} + +component main = A(80); + diff --git a/test/circuits/eddsaposeidon_test.circom b/test/circuits/eddsaposeidon_test.circom index 22ee5997..165428d0 100644 --- a/test/circuits/eddsaposeidon_test.circom +++ b/test/circuits/eddsaposeidon_test.circom @@ -1,5 +1,25 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/eddsaposeidon.circom"; +include "../../circuits/tags-managing.circom"; +include "../../circuits/babyjub.circom"; -component main = EdDSAPoseidonVerifier(); +template A(){ + input signal enabled; + input Point A; // point in Edwards representation + + input signal S; + input Point R8; // point in Edwards representation + + input signal M; // mesage + + signal enabled_aux <== BinaryCheck()(enabled); + Point A_aux <== BabyCheck()(A); + Point R8_aux <== BabyCheck()(R8); + + EdDSAPoseidonVerifier()(enabled_aux, A_aux, S, R8_aux, M); + + +} + +component main = A(); diff --git a/test/circuits/edwards2montgomery.circom b/test/circuits/edwards2montgomery.circom index 7fce4d73..305ca509 100644 --- a/test/circuits/edwards2montgomery.circom +++ b/test/circuits/edwards2montgomery.circom @@ -1,5 +1,16 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/montgomery.circom"; +include "../../circuits/babyjub.circom"; + +template Main(){ + input Point a; + output Point out; + Point {babyedwards} a_aux <== a; + //out <== Edwards2Montgomery()(BabyCheck()(a)); + out <== Edwards2Montgomery()(a_aux); +} + + +component main = Main(); -component main = Edwards2Montgomery(); diff --git a/test/circuits/escalarmul_min_test.circom b/test/circuits/escalarmul_min_test.circom index 50ce99e4..68c93b19 100644 --- a/test/circuits/escalarmul_min_test.circom +++ b/test/circuits/escalarmul_min_test.circom @@ -1,27 +1,26 @@ -pragma circom 2.0.0; - -include "../../circuits/escalarmul.circom"; +pragma circom 2.1.5; +include "../../circuits/escalarmul/escalarmul.circom"; +include "../../circuits/tags-managing.circom"; template Main() { - signal input in[256]; - signal output out[2]; - + input signal in[256]; + output Point {babyedwards} pout; + + signal {binary} aux_in[256] <== BinaryCheckArray(256)(in); var i; var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203]; component escalarMul = EscalarMul(256, base); - - escalarMul.inp[0] <== 0; - escalarMul.inp[1] <== 1; - - for (i=0; i<256; i++) { - in[i] ==> escalarMul.in[i]; - } - - escalarMul.out[0] ==> out[0]; - escalarMul.out[1] ==> out[1]; + Point {babyedwards} paux; + paux.x <== 0; + paux.y <== 1; + + paux ==> escalarMul.pin; + aux_in ==> escalarMul.in; + + escalarMul.pout ==> pout; } component main = Main(); diff --git a/test/circuits/escalarmul_test.circom b/test/circuits/escalarmul_test.circom index 1988633e..84e485fc 100644 --- a/test/circuits/escalarmul_test.circom +++ b/test/circuits/escalarmul_test.circom @@ -1,12 +1,12 @@ pragma circom 2.0.0; -include "../../circuits/escalarmul.circom"; +include "../../circuits/escalarmul/escalarmul.circom"; include "../../circuits/bitify.circom"; template Main() { - signal input in; - signal output out[2]; + input signal in; + output Point {babyedwards} pout; var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203]; @@ -15,19 +15,19 @@ template Main() { component n2b = Num2Bits(253); component escalarMul = EscalarMul(253, base); - escalarMul.inp[0] <== 0; - escalarMul.inp[1] <== 1; + Point {babyedwards} aux; // Auxiliar point [0,1] + aux.x <== 0; + aux.y <== 1; + escalarMul.pin <== aux; var i; in ==> n2b.in; - for (i=0; i<253; i++) { - n2b.out[i] ==> escalarMul.in[i]; - } + n2b.out ==> escalarMul.in; - escalarMul.out[0] ==> out[0]; - escalarMul.out[1] ==> out[1]; + + escalarMul.pout ==> pout; } component main = Main(); diff --git a/test/circuits/escalarmul_test_min.circom b/test/circuits/escalarmul_test_min.circom deleted file mode 100644 index 422e0a81..00000000 --- a/test/circuits/escalarmul_test_min.circom +++ /dev/null @@ -1,28 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/escalarmul.circom"; - - -template Main() { - signal input in[256]; - signal output out[2]; - - var i; - - var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, - 16950150798460657717958625567821834550301663161624707787222815936182638968203]; - - component escalarMul = EscalarMul(256, base); - - escalarMul.inp[0] <== 0; - escalarMul.inp[1] <== 1; - - for (i=0; i<256; i++) { - in[i] ==> escalarMul.in[i]; - } - - escalarMul.out[0] ==> out[0]; - escalarMul.out[1] ==> out[1]; -} - -component main = Main(); diff --git a/test/circuits/escalarmulany_test.circom b/test/circuits/escalarmulany_test.circom index 5e79bbec..4cf4333d 100644 --- a/test/circuits/escalarmulany_test.circom +++ b/test/circuits/escalarmulany_test.circom @@ -1,29 +1,25 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "../../circuits/escalarmulany.circom"; +include "../../circuits/escalarmul/escalarmulany.circom"; include "../../circuits/bitify.circom"; template Main() { - signal input e; - signal input p[2]; - signal output out[2]; + input signal e; + input Point p; + output Point {babyedwards} pout; + + Point checked_p <== BabyCheck()(p); component n2b = Num2Bits(253); component escalarMulAny = EscalarMulAny(253); - escalarMulAny.p[0] <== p[0]; - escalarMulAny.p[1] <== p[1]; - - var i; + escalarMulAny.pin <== checked_p; e ==> n2b.in; + n2b.out ==> escalarMulAny.e; - for (i=0; i<253; i++) { - n2b.out[i] ==> escalarMulAny.e[i]; - } + escalarMulAny.pout ==> pout; - escalarMulAny.out[0] ==> out[0]; - escalarMulAny.out[1] ==> out[1]; } component main = Main(); diff --git a/test/circuits/escalarmulfix_test.circom b/test/circuits/escalarmulfix_test.circom index 54cd7bab..25f2f16c 100644 --- a/test/circuits/escalarmulfix_test.circom +++ b/test/circuits/escalarmulfix_test.circom @@ -1,12 +1,12 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "../../circuits/escalarmulfix.circom"; +include "../../circuits/escalarmul/escalarmulfix.circom"; include "../../circuits/bitify.circom"; template Main() { - signal input e; - signal output out[2]; + input signal e; + output Point {babyedwards} pout; var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203]; @@ -19,12 +19,9 @@ template Main() { e ==> n2b.in; - for (i=0; i<253; i++) { - n2b.out[i] ==> escalarMul.e[i]; - } + n2b.out ==> escalarMul.e; - escalarMul.out[0] ==> out[0]; - escalarMul.out[1] ==> out[1]; + escalarMul.pout ==> pout; } component main = Main(); diff --git a/test/circuits/escalarmulw4table.circom b/test/circuits/escalarmulw4table.circom deleted file mode 100644 index 74b43348..00000000 --- a/test/circuits/escalarmulw4table.circom +++ /dev/null @@ -1,20 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/escalarmulw4table.circom"; - - - - -template Main() { - signal output out[16][2]; - var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, - 16950150798460657717958625567821834550301663161624707787222815936182638968203]; - - var escalarMul[16][2] = EscalarMulW4Table(base, 0); - for (var i=0; i<16; i++) { - out[i][0] <== escalarMul[i][0]; - out[i][1] <== escalarMul[i][1]; - } -} - -component main = Main(); diff --git a/test/circuits/escalarmulw4table_test.circom b/test/circuits/escalarmulw4table_test.circom index ed2ac41e..48c0f89b 100644 --- a/test/circuits/escalarmulw4table_test.circom +++ b/test/circuits/escalarmulw4table_test.circom @@ -1,11 +1,11 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "../../circuits/escalarmulw4table.circom"; +include "../../circuits/escalarmul/escalarmulw4table.circom"; template Main() { - signal input in; - signal output out[16][2]; + input signal in; + output signal out[16][2]; var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203]; diff --git a/test/circuits/escalarmulw4table_test3.circom b/test/circuits/escalarmulw4table_test3.circom index 14c0ee89..4fcf78ad 100644 --- a/test/circuits/escalarmulw4table_test3.circom +++ b/test/circuits/escalarmulw4table_test3.circom @@ -1,11 +1,11 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "../../circuits/escalarmulw4table.circom"; +include "../../circuits/escalarmul/escalarmulw4table.circom"; template Main() { - signal input in; - signal output out[16][2]; + input signal in; + output signal out[16][2]; var base[2] = [5299619240641551281634865583518297030282874472190772894086521144482721001553, 16950150798460657717958625567821834550301663161624707787222815936182638968203]; diff --git a/test/circuits/greatereqthan.circom b/test/circuits/greatereqthan.circom index 8e53f940..284bc011 100644 --- a/test/circuits/greatereqthan.circom +++ b/test/circuits/greatereqthan.circom @@ -1,5 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; +include "../../circuits/tags-managing.circom"; -component main = GreaterEqThan(32); + +template A(n){ + input signal in[2]; + output signal out <== GreaterEqThan(n)(MaxbitCheckArray(n, 2)(in)); + +} + +component main = A(30); diff --git a/test/circuits/greaterthan.circom b/test/circuits/greaterthan.circom index d2142379..887a1c93 100644 --- a/test/circuits/greaterthan.circom +++ b/test/circuits/greaterthan.circom @@ -1,5 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; +include "../../circuits/tags-managing.circom"; -component main = GreaterThan(32); + +template A(n){ + input signal in[2]; + output signal out <== GreaterThan(n)(MaxbitCheckArray(n, 2)(in)); + +} + +component main = A(30); diff --git a/test/circuits/isequal.circom b/test/circuits/isequal.circom index eb4fcc4d..1d69e03d 100644 --- a/test/circuits/isequal.circom +++ b/test/circuits/isequal.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; diff --git a/test/circuits/iszero.circom b/test/circuits/iszero.circom index 0ce848a4..c9ece1ad 100644 --- a/test/circuits/iszero.circom +++ b/test/circuits/iszero.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; diff --git a/test/circuits/lesseqthan.circom b/test/circuits/lesseqthan.circom index 9b9a89b4..98112254 100644 --- a/test/circuits/lesseqthan.circom +++ b/test/circuits/lesseqthan.circom @@ -1,5 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; +include "../../circuits/tags-managing.circom"; -component main = LessEqThan(32); + +template A(n){ + input signal in[2]; + output signal out <== LessEqThan(n)(MaxbitCheckArray(n, 2)(in)); + +} + +component main = A(30); diff --git a/test/circuits/lessthan.circom b/test/circuits/lessthan.circom index 78660b76..61664549 100644 --- a/test/circuits/lessthan.circom +++ b/test/circuits/lessthan.circom @@ -1,5 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/comparators.circom"; +include "../../circuits/tags-managing.circom"; -component main = LessThan(32); + +template A(n){ + input signal in[2]; + output signal out <== LessThan(n)(MaxbitCheckArray(n, 2)(in)); + +} + +component main = A(30); diff --git a/test/circuits/mimc_sponge_hash_test.circom b/test/circuits/mimc_sponge_hash_test.circom deleted file mode 100644 index 68a8ab59..00000000 --- a/test/circuits/mimc_sponge_hash_test.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/mimcsponge.circom"; - -component main = MiMCSponge(2, 220, 3); diff --git a/test/circuits/mimc_sponge_test.circom b/test/circuits/mimc_sponge_test.circom deleted file mode 100644 index 367c6159..00000000 --- a/test/circuits/mimc_sponge_test.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/mimcsponge.circom"; - -component main = MiMCFeistel(220); diff --git a/test/circuits/mimc_test.circom b/test/circuits/mimc_test.circom deleted file mode 100644 index 2325e65e..00000000 --- a/test/circuits/mimc_test.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "../../circuits/mimc.circom"; - -component main = MiMC7(91); diff --git a/test/circuits/montgomery2edwards.circom b/test/circuits/montgomery2edwards.circom index af344a4c..a1894537 100644 --- a/test/circuits/montgomery2edwards.circom +++ b/test/circuits/montgomery2edwards.circom @@ -1,5 +1,14 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/montgomery.circom"; -component main = Montgomery2Edwards(); +template Main(){ + input Point a; + output Point out; + out <== Montgomery2Edwards()(MontgomeryBabyCheck()(a)); + +} + + +component main = Main(); + diff --git a/test/circuits/montgomeryadd.circom b/test/circuits/montgomeryadd.circom index 8d0e73b3..afb7610c 100644 --- a/test/circuits/montgomeryadd.circom +++ b/test/circuits/montgomeryadd.circom @@ -1,5 +1,13 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/montgomery.circom"; -component main = MontgomeryAdd(); +template Main(){ + input Point a; + input Point b; + output Point out; + out <== MontgomeryAdd()(MontgomeryBabyCheck()(a), MontgomeryBabyCheck()(b)); +} + + +component main = Main(); diff --git a/test/circuits/montgomerydouble.circom b/test/circuits/montgomerydouble.circom index 51909dbd..9d235042 100644 --- a/test/circuits/montgomerydouble.circom +++ b/test/circuits/montgomerydouble.circom @@ -1,5 +1,12 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/montgomery.circom"; -component main = MontgomeryDouble(); +template Main(){ + input Point a; + output Point out; + out <== MontgomeryDouble()(MontgomeryBabyCheck()(a)); +} + + +component main = Main(); diff --git a/test/circuits/mux1_1.circom b/test/circuits/mux1_1.circom index ff13ae22..83cd5175 100644 --- a/test/circuits/mux1_1.circom +++ b/test/circuits/mux1_1.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/mux1.circom"; include "../../circuits/bitify.circom"; @@ -6,16 +6,15 @@ include "../../circuits/bitify.circom"; template Constants() { var i; - signal output out[2]; + output signal out[2]; out[0] <== 37; out[1] <== 47; } template Main() { - var i; - signal input selector;//private - signal output out; + input signal selector;//private + output signal out; component mux = Mux1(); component n2b = Num2Bits(1); @@ -23,9 +22,7 @@ template Main() { selector ==> n2b.in; n2b.out[0] ==> mux.s; - for (i=0; i<2; i++) { - cst.out[i] ==> mux.c[i]; - } + cst.out ==> mux.c; mux.out ==> out; } diff --git a/test/circuits/mux2_1.circom b/test/circuits/mux2_1.circom index 419fe625..60db22f5 100644 --- a/test/circuits/mux2_1.circom +++ b/test/circuits/mux2_1.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/mux2.circom"; include "../../circuits/bitify.circom"; @@ -6,7 +6,7 @@ include "../../circuits/bitify.circom"; template Constants() { var i; - signal output out[4]; + output signal out[4]; out[0] <== 37; out[1] <== 47; @@ -15,21 +15,16 @@ template Constants() { } template Main() { - var i; - signal input selector;//private - signal output out; + input signal selector;//private + output signal out; component mux = Mux2(); component n2b = Num2Bits(2); component cst = Constants(); selector ==> n2b.in; - for (i=0; i<2; i++) { - n2b.out[i] ==> mux.s[i]; - } - for (i=0; i<4; i++) { - cst.out[i] ==> mux.c[i]; - } + n2b.out ==> mux.s; + cst.out ==> mux.c; mux.out ==> out; } diff --git a/test/circuits/mux3_1.circom b/test/circuits/mux3_1.circom index 8723c8ba..bfe2d25b 100644 --- a/test/circuits/mux3_1.circom +++ b/test/circuits/mux3_1.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/mux3.circom"; include "../../circuits/bitify.circom"; @@ -6,7 +6,7 @@ include "../../circuits/bitify.circom"; template Constants() { var i; - signal output out[8]; + output signal out[8]; out[0] <== 37; out[1] <== 47; @@ -19,21 +19,16 @@ template Constants() { } template Main() { - var i; - signal input selector;//private - signal output out; + input signal selector;//private + output signal out; component mux = Mux3(); component n2b = Num2Bits(3); component cst = Constants(); selector ==> n2b.in; - for (i=0; i<3; i++) { - n2b.out[i] ==> mux.s[i]; - } - for (i=0; i<8; i++) { - cst.out[i] ==> mux.c[i]; - } + n2b.out ==> mux.s; + cst.out ==> mux.c; mux.out ==> out; } diff --git a/test/circuits/mux4_1.circom b/test/circuits/mux4_1.circom index c9b10dda..702f7377 100644 --- a/test/circuits/mux4_1.circom +++ b/test/circuits/mux4_1.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/mux4.circom"; include "../../circuits/bitify.circom"; @@ -6,7 +6,7 @@ include "../../circuits/bitify.circom"; template Constants() { var i; - signal output out[16]; + output signal out[16]; out[0] <== 123; out[1] <== 456; @@ -34,21 +34,16 @@ template Constants() { } template Main() { - var i; - signal input selector;//private - signal output out; + input signal selector;//private + output signal out; component mux = Mux4(); component n2b = Num2Bits(4); component cst = Constants(); selector ==> n2b.in; - for (i=0; i<4; i++) { - n2b.out[i] ==> mux.s[i]; - } - for (i=0; i<16; i++) { - cst.out[i] ==> mux.c[i]; - } + n2b.out ==> mux.s; + cst.out ==> mux.c; mux.out ==> out; } diff --git a/test/circuits/pedersen2_test.circom b/test/circuits/pedersen2_test.circom index c407d53d..fc2180db 100644 --- a/test/circuits/pedersen2_test.circom +++ b/test/circuits/pedersen2_test.circom @@ -1,12 +1,12 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/pedersen.circom"; include "../../circuits/bitify.circom"; template Main() { - signal input in; - signal output out[2]; + input signal in; + output Point {babyedwards} pout; component pedersen = Pedersen(256); @@ -20,13 +20,12 @@ template Main() { for (i=0; i<253; i++) { pedersen.in[i] <== n2b.out[i]; } - + signal {binary} aux_0 <== 0; for (i=253; i<256; i++) { - pedersen.in[i] <== 0; + pedersen.in[i] <== aux_0; } - pedersen.out[0] ==> out[0]; - pedersen.out[1] ==> out[1]; + pedersen.pout ==> pout; } component main = Main(); diff --git a/test/circuits/pedersen_test.circom b/test/circuits/pedersen_test.circom index eba561cb..5bdaf79a 100644 --- a/test/circuits/pedersen_test.circom +++ b/test/circuits/pedersen_test.circom @@ -1,12 +1,12 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/pedersen_old.circom"; include "../../circuits/bitify.circom"; template Main() { - signal input in[2]; - signal output out[2]; + input signal in[2]; + output Point {babyedwards} pout; component pedersen = Pedersen(250*2); @@ -24,8 +24,7 @@ template Main() { n2b[1].out[i] ==> pedersen.in[250+i]; } - pedersen.out[0] ==> out[0]; - pedersen.out[1] ==> out[1]; + pedersen.pout ==> pout; } component main = Main(); diff --git a/test/circuits/pointbits_loopback.circom b/test/circuits/pointbits_loopback.circom index cbba8fcb..02647514 100644 --- a/test/circuits/pointbits_loopback.circom +++ b/test/circuits/pointbits_loopback.circom @@ -1,25 +1,22 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/pointbits.circom"; template Main() { - signal input in[2]; + input signal in[2]; var i; component p2b = Point2Bits_Strict(); component b2p = Bits2Point_Strict(); - p2b.in[0] <== in[0]; - p2b.in[1] <== in[1]; + p2b.pin.x <== in[0]; + p2b.pin.y <== in[1]; - for (i=0; i<256; i++) { - b2p.in[i] <== p2b.out[i]; - } + b2p.in <== p2b.out; - b2p.out[0] === in[0]; - b2p.out[1] === in[1]; + b2p.pout === p2b.pin; } component main = Main(); diff --git a/test/circuits/poseidon3_test.circom b/test/circuits/poseidon3_test.circom index 1b06c187..5a5bca9c 100644 --- a/test/circuits/poseidon3_test.circom +++ b/test/circuits/poseidon3_test.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/poseidon.circom"; diff --git a/test/circuits/poseidon6_test.circom b/test/circuits/poseidon6_test.circom index 83cd1cfb..483e92c0 100644 --- a/test/circuits/poseidon6_test.circom +++ b/test/circuits/poseidon6_test.circom @@ -1,4 +1,4 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/poseidon.circom"; diff --git a/test/circuits/sha256_2_test.circom b/test/circuits/sha256_2_test.circom index 13a445da..24fcc107 100644 --- a/test/circuits/sha256_2_test.circom +++ b/test/circuits/sha256_2_test.circom @@ -1,11 +1,11 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/sha256/sha256_2.circom"; template Main() { - signal input a; //private - signal input b; //private - signal output out; + input signal a; //private + input signal b; //private + output signal out; component sha256_2 = Sha256_2(); diff --git a/test/circuits/sha256_test448.circom b/test/circuits/sha256_test448.circom index 7a9843cd..4180d3c1 100644 --- a/test/circuits/sha256_test448.circom +++ b/test/circuits/sha256_test448.circom @@ -1,5 +1,17 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/sha256/sha256.circom"; +include "../../circuits/tags-managing.circom"; -component main = Sha256(448); + +template Main() { + input signal a[448]; //private + output signal out[256]; + + component sha256_2 = Sha256(448); + + sha256_2.in <== BinaryCheckArray(448)(a); + out <== sha256_2.out; +} + +component main = Main(); diff --git a/test/circuits/sha256_test512.circom b/test/circuits/sha256_test512.circom index 06db0d39..d49e3b31 100644 --- a/test/circuits/sha256_test512.circom +++ b/test/circuits/sha256_test512.circom @@ -1,5 +1,17 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/sha256/sha256.circom"; +include "../../circuits/tags-managing.circom"; -component main = Sha256(512); + +template Main() { + input signal a[512]; //private + output signal out[256]; + + component sha256_2 = Sha256(512); + + sha256_2.in <== BinaryCheckArray(512)(a); + out <== sha256_2.out; +} + +component main = Main(); diff --git a/test/circuits/sign_test.circom b/test/circuits/sign_test.circom index 2dae52c3..12efab0a 100644 --- a/test/circuits/sign_test.circom +++ b/test/circuits/sign_test.circom @@ -1,5 +1,14 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; -include "../../circuits/sign.circom"; +include "../../circuits/comparators.circom"; +include "../../circuits/tags-managing.circom"; -component main = Sign(); +template A(){ + input signal in[254]; + component sign = Sign(); + sign.in <== BinaryCheckArray(254)(in); + output signal {binary} out <== sign.sign; + +} + +component main = A(); diff --git a/test/circuits/smtprocessor10_test.circom b/test/circuits/smtprocessor10_test.circom index 3030054e..8960bc2c 100644 --- a/test/circuits/smtprocessor10_test.circom +++ b/test/circuits/smtprocessor10_test.circom @@ -1,5 +1,24 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/smt/smtprocessor.circom"; +include "../../circuits/tags-managing.circom"; -component main = SMTProcessor(10); + +template Main() { + input signal oldRoot; + input signal siblings[10]; + input signal oldKey; + input signal oldValue; + input signal isOld0; + input signal newKey; + input signal newValue; + input signal fnc[2]; + + output signal newRoot; + + newRoot <== SMTProcessor(10)(oldRoot, siblings, oldKey, oldValue, BinaryCheck()(isOld0), newKey, newValue, BinaryCheckArray(2)(fnc)); + + +} + +component main = Main(); diff --git a/test/circuits/smtverifier10_test.circom b/test/circuits/smtverifier10_test.circom index 5b6d47a7..52d90fad 100644 --- a/test/circuits/smtverifier10_test.circom +++ b/test/circuits/smtverifier10_test.circom @@ -1,5 +1,21 @@ -pragma circom 2.0.0; +pragma circom 2.1.5; include "../../circuits/smt/smtverifier.circom"; +include "../../circuits/tags-managing.circom"; -component main = SMTVerifier(10); +template SMTVerifier_main(nLevels) { + input signal enabled; + input signal root; + input signal siblings[nLevels]; + input signal oldKey; + input signal oldValue; + input signal isOld0; + input signal key; + input signal value; + input signal fnc; + + SMTVerifier(nLevels)(BinaryCheck()(enabled), root, siblings, oldKey, oldValue, + BinaryCheck()(isOld0), key, value, + BinaryCheck()(fnc)); +} +component main = SMTVerifier_main(10); diff --git a/test/circuits/tags_specifications.circom b/test/circuits/tags_specifications.circom new file mode 100644 index 00000000..47769a54 --- /dev/null +++ b/test/circuits/tags_specifications.circom @@ -0,0 +1,21 @@ +pragma circom 2.1.0; +spec_tags {binary} in{ + 0 <= in <= 1 +} + +spec_tags {maxbit} in{ + 0 <= in <= 2**in.maxbit-1 +} + +spec_tags {max} in{ + 0 <= in <= in.max +} + +spec_tags {max_abs} in{ + -in.max_abs <= in <= in.max_abs +} + + +spec_tags {maxbit_abs} in{ + - 2**in.maxbit_abs <= in <= 2 ** in.maxbit_abs +}