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*/
 19
 20include "compconstant.circom";
 21include "pointbits.circom";
 22include "mimc.circom";
 23include "bitify.circom";
 24include "escalarmulany.circom";
 25include "escalarmulfix.circom";
 26
 27template EdDSAMiMCVerifier() {
 28    signal input enabled;
 29    signal input Ax;
 30    signal input Ay;
 31
 32    signal input S;
 33    signal input R8x;
 34    signal input R8y;
 35
 36    signal input M;
 37
 38    var i;
 39
 40// Ensure S<Subgroup Order
 41
 42    component snum2bits = Num2Bits(253);
 43    snum2bits.in <== S;
 44
 45    component  compConstant = CompConstant(2736030358979909402780800718157159386076813972158567259200215660948447373040);
 46
 47    for (i=0; i<253; i++) {
 48        snum2bits.out[i] ==> compConstant.in[i];
 49    }
 50    compConstant.in[253] <== 0;
 51    compConstant.out === 0;
 52
 53// Calculate the h = H(R,A, msg)
 54
 55    component hash = MultiMiMC7(5, 91);
 56    hash.in[0] <== R8x;
 57    hash.in[1] <== R8y;
 58    hash.in[2] <== Ax;
 59    hash.in[3] <== Ay;
 60    hash.in[4] <== M;
 61    hash.k <== 0;
 62
 63    component h2bits = Num2Bits_strict();
 64    h2bits.in <== hash.out;
 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.xout;
 75    dbl2.y <== dbl1.yout;
 76    component dbl3 = BabyDbl();
 77    dbl3.x <== dbl2.xout;
 78    dbl3.y <== dbl2.yout;
 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(254);
 86    for (i=0; i<254; i++) {
 87        mulAny.e[i] <== h2bits.out[i];
 88    }
 89    mulAny.p[0] <== dbl3.xout;
 90    mulAny.p[1] <== dbl3.yout;
 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        5299619240641551281634865583518297030282874472190772894086521144482721001553,
105        16950150798460657717958625567821834550301663161624707787222815936182638968203
106    ];
107    component mulFix = EscalarMulFix(253, BASE8);
108    for (i=0; i<253; i++) {
109        mulFix.e[i] <== snum2bits.out[i];
110    }
111
112// Do the comparation left == right if enabled;
113
114    component eqCheckX = ForceEqualIfEnabled();
115    eqCheckX.enabled <== enabled;
116    eqCheckX.in[0] <== mulFix.out[0];
117    eqCheckX.in[1] <== addRight.xout;
118
119    component eqCheckY = ForceEqualIfEnabled();
120    eqCheckY.enabled <== enabled;
121    eqCheckY.in[0] <== mulFix.out[1];
122    eqCheckY.in[1] <== addRight.yout;
123}