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 "mimc.circom";
 24include "bitify.circom";
 25include "escalarmulany.circom";
 26include "escalarmulfix.circom";
 27
 28template EdDSAMiMCVerifier() {
 29    signal input enabled;
 30    signal input Ax;
 31    signal input Ay;
 32
 33    signal input S;
 34    signal input R8x;
 35    signal input R8y;
 36
 37    signal input M;
 38
 39    var i;
 40
 41// Ensure S<Subgroup Order
 42
 43    component snum2bits = Num2Bits(253);
 44    snum2bits.in <== S;
 45
 46    component  compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040);
 47
 48    for (i=0; i<253; i++) {
 49        snum2bits.out[i] ==> compConstant.in[i];
 50    }
 51    compConstant.in[253] <== 0;
 52    compConstant.out === 0;
 53
 54// Calculate the h = H(R,A, msg)
 55
 56    component hash = MultiMiMC7(5, 91);
 57    hash.in[0] <== R8x;
 58    hash.in[1] <== R8y;
 59    hash.in[2] <== Ax;
 60    hash.in[3] <== Ay;
 61    hash.in[4] <== M;
 62    hash.k <== 0;
 63
 64    component h2bits = Num2Bits_strict();
 65    h2bits.in <== hash.out;
 66
 67// Calculate second part of the right side:  right2 = h*8*A
 68
 69    // Multiply by 8 by adding it 3 times.  This also ensure that the result is in
 70    // the subgroup.
 71    component dbl1 = BabyDbl();
 72    dbl1.x <== Ax;
 73    dbl1.y <== Ay;
 74    component dbl2 = BabyDbl();
 75    dbl2.x <== dbl1.xout;
 76    dbl2.y <== dbl1.yout;
 77    component dbl3 = BabyDbl();
 78    dbl3.x <== dbl2.xout;
 79    dbl3.y <== dbl2.yout;
 80
 81    // We check that A is not zero.
 82    component isZero = IsZero();
 83    isZero.in <== dbl3.x;
 84    isZero.out === 0;
 85
 86    component mulAny = EscalarMulAny(254);
 87    for (i=0; i<254; i++) {
 88        mulAny.e[i] <== h2bits.out[i];
 89    }
 90    mulAny.p[0] <== dbl3.xout;
 91    mulAny.p[1] <== dbl3.yout;
 92
 93
 94// Compute the right side: right =  R8 + right2
 95
 96    component addRight = BabyAdd();
 97    addRight.x1 <== R8x;
 98    addRight.y1 <== R8y;
 99    addRight.x2 <== mulAny.out[0];
100    addRight.y2 <== mulAny.out[1];
101
102// Calculate left side of equation left = S*B8
103
104    var BASE8[2] = [
105        5299619240641551281634865583518297030282874472190772894086521144482721001553,
106        16950150798460657717958625567821834550301663161624707787222815936182638968203
107    ];
108    component mulFix = EscalarMulFix(253, BASE8);
109    for (i=0; i<253; i++) {
110        mulFix.e[i] <== snum2bits.out[i];
111    }
112
113// Do the comparation left == right if enabled;
114
115    component eqCheckX = ForceEqualIfEnabled();
116    eqCheckX.enabled <== enabled;
117    eqCheckX.in[0] <== mulFix.out[0];
118    eqCheckX.in[1] <== addRight.xout;
119
120    component eqCheckY = ForceEqualIfEnabled();
121    eqCheckY.enabled <== enabled;
122    eqCheckY.in[0] <== mulFix.out[1];
123    eqCheckY.in[1] <== addRight.yout;
124}