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