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