/ circuits / binsum.circom
binsum.circom
  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  /*
 21  
 22  Binary Sum
 23  ==========
 24  
 25  This component creates a binary sum componet of ops operands and n bits each operand.
 26  
 27  e is Number of carries: Depends on the number of operands in the input.
 28  
 29  Main Constraint:
 30     in[0][0]     * 2^0  +  in[0][1]     * 2^1  + ..... + in[0][n-1]    * 2^(n-1)  +
 31   + in[1][0]     * 2^0  +  in[1][1]     * 2^1  + ..... + in[1][n-1]    * 2^(n-1)  +
 32   + ..
 33   + in[ops-1][0] * 2^0  +  in[ops-1][1] * 2^1  + ..... + in[ops-1][n-1] * 2^(n-1)  +
 34   ===
 35     out[0] * 2^0  + out[1] * 2^1 +   + out[n+e-1] *2(n+e-1)
 36  
 37  To waranty binary outputs:
 38  
 39      out[0]     * (out[0] - 1) === 0
 40      out[1]     * (out[0] - 1) === 0
 41      .
 42      .
 43      .
 44      out[n+e-1] * (out[n+e-1] - 1) == 0
 45  
 46   */
 47  
 48  
 49  /*
 50      This function calculates the number of extra bits in the output to do the full sum.
 51   */
 52   pragma circom 2.0.0;
 53  
 54  function nbits(a) {
 55      var n = 1;
 56      var r = 0;
 57      while (n-1<a) {
 58          r++;
 59          n *= 2;
 60      }
 61      return r;
 62  }
 63  
 64  
 65  template BinSum(n, ops) {
 66      var nout = nbits((2**n -1)*ops);
 67      signal input in[ops][n];
 68      signal output out[nout];
 69  
 70      var lin = 0;
 71      var lout = 0;
 72  
 73      var k;
 74      var j;
 75  
 76      var e2;
 77  
 78      e2 = 1;
 79      for (k=0; k<n; k++) {
 80          for (j=0; j<ops; j++) {
 81              lin += in[j][k] * e2;
 82          }
 83          e2 = e2 + e2;
 84      }
 85  
 86      e2 = 1;
 87      for (k=0; k<nout; k++) {
 88          out[k] <-- (lin >> k) & 1;
 89  
 90          // Ensure out is binary
 91          out[k] * (out[k] - 1) === 0;
 92  
 93          lout += out[k] * e2;
 94  
 95          e2 = e2+e2;
 96      }
 97  
 98      // Ensure the sum;
 99  
100      lin === lout;
101  }