1
  2include "../node_modules/circom/circuits/bitify.circom";
  3include "../node_modules/circom/circuits/comparators.circom";
  4include "escalarmulany.circom";
  5include "babyjub.circom";
  6
  7
  8templete EdDSAVerfier(n) {
  9    signal input msg[n];
 10
 11    signal input A[256];
 12    signal input R8[256];
 13    signal input S[256];
 14
 15    signal Ax;
 16    signal Ay;
 17
 18    signal R8x;
 19    signal R8y;
 20
 21    var i;
 22
 23// Ensure S<Subgroup Order
 24
 25    component  compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040);
 26
 27    for (var i=0; i<254; i++) {
 28        S[i] ==> compConstant.in[i];
 29    }
 30    compConstant.out === 0;
 31    S[255] === 0;
 32    S[256] === 0;
 33
 34// Convert A to Field elements (And verify A)
 35
 36    component bits2pointA = Bits2Point_Strict();
 37
 38    for (i=0; i<256; i++) {
 39        bits2pointA.in[i] <== A[i];
 40    }
 41    Ax <== bits2pointA.out[0];
 42    Ay <== bits2pointA.out[1];
 43
 44// Convert R8 to Field elements (And verify R8)
 45
 46    component bits2pointR8 = Bits2Point_Strict();
 47
 48    for (i=0; i<256; i++) {
 49        bits2pointR8.in[i] <== R8[i];
 50    }
 51    R8x <== bits2pointR8.out[0];
 52    R8y <== bits2pointR8.out[1];
 53
 54// Calculate the h = H(R,A, msg)
 55
 56    component hash = Pedersen(512+n);
 57
 58    for (i=0; i<256; i++) {
 59        hash.in[i] <== R[i];
 60        hash.in[256+i] <== A[i];
 61    }
 62    for (i=0; i<n; i++) {
 63        hash.in[512+i] <== msg[i];
 64    }
 65
 66// Calculate second part of the right side:  right2 = h*8*A
 67
 68    // Multiply by 8 by adding it 3 times.  This also ensure that the result is in
 69    // the subgroup.
 70    component dbl1 = BabyDbl();
 71    dbl1.x <== Ax;
 72    dbl1.y <== Ay;
 73    component dbl2 = BabyDbl();
 74    dbl2.x <== dbl1.outx;
 75    dbl2.y <== dbl1.outy;
 76    component dbl3 = BabyDbl();
 77    dbl3.x <== dbl2.outx;
 78    dbl3.y <== dbl2.outy;
 79
 80    // We check that A is not zero.
 81    component isZero = IsZero();
 82    isZero.in <== dbl3.x;
 83    isZero.out === 0;
 84
 85    component mulAny = EscalarMulAny(256);
 86    for (i=0; i<256; i++) {
 87        mulAny.e[i] <== hash.out[i];
 88    }
 89    mulAny.p[0] <== dbl3.outx;
 90    mulAny.p[1] <== dbl3.outy;
 91
 92
 93// Compute the right side: right =  R8 + right2
 94
 95    component addRight = BabyAdd();
 96    addRight.x1 <== R8x;
 97    addRight.y1 <== R8y;
 98    addRight.x2 <== mulAny.out[0];
 99    addRight.y2 <== mulAny.out[1];
100
101// Calculate left side of equation left = S*B8
102
103    var BASE8 = [
104        17777552123799933955779906779655732241715742912184938656739573121738514868268,
105        2626589144620713026669568689430873010625803728049924121243784502389097019475
106    ];
107    component mulFix = EscalarMulFix(256, BASE8);
108    for (i=0; i<256; i++) {
109        mulFix.e[i] <== S[i];
110    }
111
112// Do the comparation left == right
113
114    mulFix.out[0] === addRight.xout;
115    mulFix.out[1] === addRight.yout;
116}