Circomlib2 buses

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

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 <https://www.gnu.org/licenses/>.
 */
-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;
 }

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 <https://www.gnu.org/licenses/>.
 */
-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;
 }

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 <https://www.gnu.org/licenses/>.
+*/
+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<n; i++) {
+        out.bits[i] <-- (in >> 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<n; i++) {
+        lc1 += in.bits[i] * e2;
+        e2 = e2 + e2;
+    }
+    out.maxbit = n;
+    lc1 ==> 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<n; i++) {
+        out[i] <-- (neg >> 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;
+    }
+
+}