confused about Circom LessThan implementation

Question

I am trying to implement a LessThan template which outputs 1 if y is less than x and 0 is x is more than y. Below is the sample code from the circom library and I am trying to understand whats going on this code below.

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];
}

i dont whats going on in:

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

it involves some bitwise operation.

Answer 1

Since in[0] < in[1] is not a quadratic expression we have to rewrite the condition a bit to be able to express it as a constraint. The key idea here is to see that in[0] < in[1] is equivalent to in[0] - in[1] < 0. Adding 2^n to both sides we get 2^n + in[0] - in[1] < 2^n.

Now, 2^n = (1 << n) which is where the expression in[0] + (1 << n) - in[1] comes from. The final constraint simply ensures that out = 1 if and only if bit n of 2^n + in[0] - in[1] is 0, which happens exactly when 2^n + in[0] - in[1] < 2^n.