запутался в реализации Circom LessThan

Question

Я пытаюсь реализовать шаблон LessThan, который выводит 1, если y меньше, чем x, и 0, если x больше, чем y. Ниже приведен пример кода из библиотеки circom, и я пытаюсь понять, что происходит в этом коде ниже.

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

я не знаю, что происходит в:

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

это включает некоторую побитовую операцию.

Answer 1

Поскольку это не квадратичное выражение, мы должны немного переписать условие, чтобы иметь возможность выразить его как ограничение. Ключевая идея здесь состоит в том, чтобы увидеть, чтоin[0] < in[1]эквивалентноin[0] - in[1] < 0. Добавление2^nв обе стороны получаем .

Сейчас,2^n = (1 << n)где выражениеin[0] + (1 << n) - in[1]происходит от. Окончательное ограничение просто гарантирует, чтоout = 1если и только если битnиз2^n + in[0] - in[1]равен 0, что происходит ровно тогда, когда2^n + in[0] - in[1] < 2^n.