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    signal input in[2];
 90    signal output out;
 91
 92    component n2b = Num2Bits(n*2+1);
 93
 94    n2b.in <== in[0]+ (1<<n) - in[1];
 95
 96    out <== 1-n2b.out[n];
 97}
 98
 99
100
101// N is the number of bits the input  have.
102// The MSF is the sign bit.
103template LessEqThan(n) {
104    signal input in[2];
105    signal output out;
106
107    component lt = LessThan(n);
108
109    lt.in[0] <== in[0];
110    lt.in[1] <== in[1]+1;
111    lt.out ==> out;
112}
113
114// N is the number of bits the input  have.
115// The MSF is the sign bit.
116template GreaterThan(n) {
117    signal input in[2];
118    signal output out;
119
120    component lt = LessThan(n);
121
122    lt.in[0] <== in[1];
123    lt.in[1] <== in[0];
124    lt.out ==> out;
125}
126
127// N is the number of bits the input  have.
128// The MSF is the sign bit.
129template GreaterEqThan(n) {
130    signal input in[2];
131    signal output out;
132
133    component lt = LessThan(n);
134
135    lt.in[0] <== in[1];
136    lt.in[1] <== in[0]+1;
137    lt.out ==> out;
138}
139