circomlib/circuits/binsub.circom
circuits/binsub.circomRaw
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
20/*
21This component creates a binary substraction.
22
23
24Main Constraint:
25 (in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1)) +
26 + 2^n
27 - (in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1))
28 ===
29 out[0] * 2^0 + out[1] * 2^1 + + out[n-1] *2^(n-1) + aux
30
31
32 out[0] * (out[0] - 1) === 0
33 out[1] * (out[0] - 1) === 0
34 .
35 .
36 .
37 out[n-1] * (out[n-1] - 1) === 0
38 aux * (aux-1) == 0
39
40*/
41
42template BinSub(n) {
43 signal input in[2][n];
44 signal output out[n];
45
46 signal aux;
47
48 var lin = 2**n;
49 var lout = 0;
50
51 var i;
52
53 for (i=0; i<n; i++) {
54 lin = lin + in[0][i]*(2**i);
55 lin = lin - in[1][i]*(2**i);
56 }
57
58 for (i=0; i<n; i++) {
59 out[i] <-- (lin >> i) & 1;
60
61 // Ensure out is binary
62 out[i] * (out[i] - 1) === 0;
63
64 lout = lout + out[i]*(2**i);
65 }
66
67 aux <-- (lin >> n) & 1;
68 aux*(aux-1) === 0;
69 lout = lout + aux*(2**n);
70
71 // Ensure the sum;
72 lin === lout;
73}