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 "bitify.circom";
 21include "binsum.circom";
 22
 23template IsZero() {
 24    signal input in;
 25    signal output out;
 26
 27    signal inv;
 28
 29    inv <-- in!=0 ? 1/in : 0;
 30
 31    out <== -in*inv +1;
 32    in*out === 0;
 33}
 34
 35
 36template IsEqual() {
 37    signal input in[2];
 38    signal output out;
 39
 40    component isz = IsZero();
 41
 42    in[1] - in[0] ==> isz.in;
 43
 44    isz.out ==> out;
 45}
 46
 47template ForceEqualIfEnabled() {
 48    signal input enabled;
 49    signal input in[2];
 50
 51    component isz = IsZero();
 52
 53    in[1] - in[0] ==> isz.in;
 54
 55    (1 - isz.out)*enabled === 0;
 56}
 57
 58/*
 59// N is the number of bits the input  have.
 60// The MSF is the sign bit.
 61template LessThan(n) {
 62    signal input in[2];
 63    signal output out;
 64
 65    component num2Bits0;
 66    component num2Bits1;
 67
 68    component adder;
 69
 70    adder = BinSum(n, 2);
 71
 72    num2Bits0 = Num2Bits(n);
 73    num2Bits1 = Num2BitsNeg(n);
 74
 75    in[0] ==> num2Bits0.in;
 76    in[1] ==> num2Bits1.in;
 77
 78    var i;
 79    for (i=0;i<n;i++) {
 80        num2Bits0.out[i] ==> adder.in[0][i];
 81        num2Bits1.out[i] ==> adder.in[1][i];
 82    }
 83
 84    adder.out[n-1] ==> out;
 85}
 86*/
 87
 88template LessThan(n) {
 89    assert(n <= 252);
 90    signal input in[2];
 91    signal output out;
 92
 93    component n2b = Num2Bits(n+1);
 94
 95    n2b.in <== in[0]+ (1<<n) - in[1];
 96
 97    out <== 1-n2b.out[n];
 98}
 99
100
101
102// N is the number of bits the input  have.
103// The MSF is the sign bit.
104template LessEqThan(n) {
105    signal input in[2];
106    signal output out;
107
108    component lt = LessThan(n);
109
110    lt.in[0] <== in[0];
111    lt.in[1] <== in[1]+1;
112    lt.out ==> out;
113}
114
115// N is the number of bits the input  have.
116// The MSF is the sign bit.
117template GreaterThan(n) {
118    signal input in[2];
119    signal output out;
120
121    component lt = LessThan(n);
122
123    lt.in[0] <== in[1];
124    lt.in[1] <== in[0];
125    lt.out ==> out;
126}
127
128// N is the number of bits the input  have.
129// The MSF is the sign bit.
130template GreaterEqThan(n) {
131    signal input in[2];
132    signal output out;
133
134    component lt = LessThan(n);
135
136    lt.in[0] <== in[1];
137    lt.in[1] <== in[0]+1;
138    lt.out ==> out;
139}
140