1/*
  2    Copyright 2018 0KIMS association.
  3
  4    This file is part of circom (Zero Knowledge Circuit Compiler).
  5
  6    circom is a free software: you can redistribute it and/or modify it
  7    under the terms of the GNU General Public License as published by
  8    the Free Software Foundation, either version 3 of the License, or
  9    (at your option) any later version.
 10
 11    circom is distributed in the hope that it will be useful, but WITHOUT
 12    ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
 13    or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
 14    License for more details.
 15
 16    You should have received a copy of the GNU General Public License
 17    along with circom. If not, see <https://www.gnu.org/licenses/>.
 18*/
 19pragma circom 2.0.0;
 20
 21include "compconstant.circom";
 22include "pointbits.circom";
 23include "pedersen.circom";
 24include "escalarmulany.circom";
 25include "escalarmulfix.circom";
 26
 27template EdDSAVerifier(n) {
 28    signal input msg[n];
 29
 30    signal input A[256];
 31    signal input R8[256];
 32    signal input S[256];
 33
 34    signal Ax;
 35    signal Ay;
 36
 37    signal R8x;
 38    signal R8y;
 39
 40    var i;
 41
 42// Ensure S<Subgroup Order
 43
 44    component  compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040);
 45
 46    for (i=0; i<254; i++) {
 47        S[i] ==> compConstant.in[i];
 48    }
 49    compConstant.out === 0;
 50    S[254] === 0;
 51    S[255] === 0;
 52
 53// Convert A to Field elements (And verify A)
 54
 55    component bits2pointA = Bits2Point_Strict();
 56
 57    for (i=0; i<256; i++) {
 58        bits2pointA.in[i] <== A[i];
 59    }
 60    Ax <== bits2pointA.out[0];
 61    Ay <== bits2pointA.out[1];
 62
 63// Convert R8 to Field elements (And verify R8)
 64
 65    component bits2pointR8 = Bits2Point_Strict();
 66
 67    for (i=0; i<256; i++) {
 68        bits2pointR8.in[i] <== R8[i];
 69    }
 70    R8x <== bits2pointR8.out[0];
 71    R8y <== bits2pointR8.out[1];
 72
 73// Calculate the h = H(R,A, msg)
 74
 75    component hash = Pedersen(512+n);
 76
 77    for (i=0; i<256; i++) {
 78        hash.in[i] <== R8[i];
 79        hash.in[256+i] <== A[i];
 80    }
 81    for (i=0; i<n; i++) {
 82        hash.in[512+i] <== msg[i];
 83    }
 84
 85    component point2bitsH = Point2Bits_Strict();
 86    point2bitsH.in[0] <== hash.out[0];
 87    point2bitsH.in[1] <== hash.out[1];
 88
 89// Calculate second part of the right side:  right2 = h*8*A
 90
 91    // Multiply by 8 by adding it 3 times.  This also ensure that the result is in
 92    // the subgroup.
 93    component dbl1 = BabyDbl();
 94    dbl1.x <== Ax;
 95    dbl1.y <== Ay;
 96    component dbl2 = BabyDbl();
 97    dbl2.x <== dbl1.xout;
 98    dbl2.y <== dbl1.yout;
 99    component dbl3 = BabyDbl();
100    dbl3.x <== dbl2.xout;
101    dbl3.y <== dbl2.yout;
102
103    // We check that A is not zero.
104    component isZero = IsZero();
105    isZero.in <== dbl3.x;
106    isZero.out === 0;
107
108    component mulAny = EscalarMulAny(256);
109    for (i=0; i<256; i++) {
110        mulAny.e[i] <== point2bitsH.out[i];
111    }
112    mulAny.p[0] <== dbl3.xout;
113    mulAny.p[1] <== dbl3.yout;
114
115
116// Compute the right side: right =  R8 + right2
117
118    component addRight = BabyAdd();
119    addRight.x1 <== R8x;
120    addRight.y1 <== R8y;
121    addRight.x2 <== mulAny.out[0];
122    addRight.y2 <== mulAny.out[1];
123
124// Calculate left side of equation left = S*B8
125
126    var BASE8[2] = [
127        5299619240641551281634865583518297030282874472190772894086521144482721001553,
128        16950150798460657717958625567821834550301663161624707787222815936182638968203
129    ];
130    component mulFix = EscalarMulFix(256, BASE8);
131    for (i=0; i<256; i++) {
132        mulFix.e[i] <== S[i];
133    }
134
135// Do the comparation left == right
136
137    mulFix.out[0] === addRight.xout;
138    mulFix.out[1] === addRight.yout;
139}