/ circuit / binary_compare.circom
binary_compare.circom
 1  
 2  pragma circom 2.2.0;
 3  
 4  //------------------------------------------------------------------------------
 5  
 6  //
 7  // given two numbers in `n`-bit binary decomposition
 8  // (least significant bit first), we compute
 9  //
10  //             /  -1   if   A <  B
11  //   out  :=  {    0   if   A == B
12  //             \  +1   if   A >  B
13  //
14  // NOTE: we don't check that the digits are indeed binary;
15  //       that's the responsibility of the caller!
16  //
17  // This version uses `(3*n-1)` nonlinear constraints.
18  // Question: can we do better? (note that this has to work with n >= 254 digits too!)
19  //
20  
21  template BinaryCompare(n) {
22    signal input  A[n];
23    signal input  B[n];
24    signal output out;
25  
26    signal eq[n];
27    signal aux[n];
28  
29    signal jump[n+1];
30    jump[n] <== 1;
31  
32    var sum = 0;
33    for(var k=n-1; k>=0; k--) {
34      var y = A[k] - B[k];
35      eq[k]   <== 1 - y*y;                      // (A[k] == B[k]) ? 1 : 0
36      jump[k] <== eq[k] * jump[k+1];            // this jumps from 1 to 0 at the highest inequal digit
37      aux[k]  <== (jump[k+1] - jump[k]) * y;    // where we store whether A was greater or less
38      sum += aux[k];
39    }
40  
41    out <== sum;
42  }
43  
44  //------------------------------------------------------------------------------
45  
46  //
47  // given two numbers in `n`-bit binary decomposition (little-endian), we compute
48  //
49  //   out  :=  (A <= B) ? 1 : 0
50  //
51  // NOTE: we don't check that the digits are indeed binary;
52  //       that's the responsibility of the caller!
53  //
54  
55  template BinaryLessOrEqual(n) {
56    signal input  A[n];
57    signal input  B[n];
58    signal output out;
59  
60    var phalf = 1/2;       // +1/2 as field element
61    var mhalf = -phalf;    // -1/2 as field element
62  
63    component cmp = BinaryCompare(n);
64    cmp.A <== A;
65    cmp.B <== B;
66  
67    var x = cmp.out;
68    out <== mhalf * (x-1) * (x+2);
69  }
70  
71  //------------------------------------------------------------------------------
72  
73  //
74  // given two numbers in `n`-bit binary decomposition (little-endian), we compute
75  //
76  //   out  :=  (A >= B) ? 1 : 0
77  //
78  // NOTE: we don't check that the digits are indeed binary;
79  //       that's the responsibility of the caller!
80  //
81  
82  template BinaryGreaterOrEqual(n) {
83    signal input  A[n];
84    signal input  B[n];
85    signal output out;
86  
87    var phalf = 1/2;       // +1/2 as field element
88    var mhalf = -phalf;    // -1/2 as field element
89  
90    component cmp = BinaryCompare(n);
91    cmp.A <== A;
92    cmp.B <== B;
93  
94    var x = cmp.out;
95    out <== mhalf * (x+1) * (x-2);
96  }
97  
98  //------------------------------------------------------------------------------