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