Skip to content

Demonstrates an easy mistake to make in circom, allowing usual statements to be proven, like `100 < 10`

Notifications You must be signed in to change notification settings

BlakeMScurr/comparator-overflow

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

8 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

comparator-overflow

What is the bug?

Comparator overflow is a common misuse of circomlib comparators. The LessThan component takes two n-bit inputs and checks returns 1 if the first is less than the second. I.e.,

component lt = Component(252); // 252 bits
lt.in[0] <== 5;
lt.in[1] <== 10;
lt.out === 1;

Or it returns 0 if the first number is larger:

component lt = Component(252); // 252 bits
lt.in[0] <== 11;
lt.in[1] <== 10;
lt.out === 0;

However, if the first number is almost as large p (the size of the prime field), LessThan can unexpectedly return true. This happens when lt.in[0] is close enough to p to "wrap around", for example, lt.in[0] === p - 1:

component lt = Component(252); // 252 bits
lt.in[0] <== 21888242871839275222246405745257275088548364400416034343698204186575808495616; // p - 1
lt.in[1] <== 10;
lt.out === 1;

In particular, this happens precisely when lt.in[0] > p - 2^n + lt.in[1], does not correspond to circom's standard definition of negative numbers, nor, likely, anything relevant to any common use case. Note that similar issues can happen when lt.in[1] is outside the range.

Demonstration

To test this yourself, make sure you install circom then run

npm i
./build.sh

If your machine is setup properly this will output Everything went okay, circom safe. This shows that according to the LessThan comparator, p-1 < 10. Uncomment different lines of main.circom to confirm LessThan works as decribed above, including verifying the flipping point.

Fix

The simplest solution is to use Num2Bits to verify that both inputs are in the appropriate range:

template someTemplate() {
    ...
    component aInRange = Num2Bits(252);
    aInRange.in <== a;
    component bInRange = Num2Bits(252);
    bInRange.in <== lower;
    component leq = LessEqThan(252);
    leq.in[0] <== a;
    leq.in[1] <== b;
    ...
}

Here Num2Bits decomposes its input into 252 bits, then reconstructs the number as a sum of the bits, and puts a hard constraint making sure the reconstruction is equal to the input. If there are any bits in a location higher than 252 this constraint will fail.

Why does this happen?

This is the code for LessThan:

template LessThan(n) {
    assert(n <= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in <== in[0]+ (1<<n) - in[1];

    out <== 1-n2b.out[n];
}

It's best to think of this as bitwise operation. First we get 2^n (written as 1<<n), which looks like 100000, then we add the first input, and subtract the second. If the nth bit has been flipped we know that second input is larger, so we should return true, i.e., 1, hence the bit flip on the last line.

Visually:

  nth-bit
  |
  v
  100
+ 011
- 001
_____
  110

The nth bit is still 1, so 011 is larger than 001

However, if we put an extra large number in the first input, we can wrap around and not flip the nth bit:

kth-bit  nth-bit
  |     |
  v     v
  000...100
+ 111...111
- 000...001
_____
  000...100

The nth bit is not flipped, so we think 100...000 < 000...001.
Note, the above sum assumes we're in a k-bit field, i.e., 111...111+000...001=0

About

Demonstrates an easy mistake to make in circom, allowing usual statements to be proven, like `100 < 10`

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages