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