How to generate constraint on right shift bitwise operator in Circom

Question

How to generate constraint on right shift bitwise operator in the circom circuit language?

I'm trying to do the following:

pragma circom 2.0.0;

template MAIN() {

    signal input v;
    signal output type;

    type <== v >> 5;
}

component main = MAIN();

I'm getting the following error:

error[T3001]: Non quadratic constraints are not allowed!
   ┌─ "/Users/ilia/compiling/main-circom/main.circom":68:5
   │
68 │     type <== v >> 5;
   │     ^^^^^^^^^^^^^^^ found here
   │
   = call trace:
     ->MAIN

I think this has to do with the fact that v >> 5 expression can not be re-expressed as a quadratic expression by the circom compiler.

I struggle to rewrite the expression to be quadratic. It might involve writing assignment and constraint as two separate operations, but I'm not sure what a proper validating constraint would be for a right shift.

In terms of test cases, I expect type to be $5$ when v is $168$ for example.

Answer 1

Solution using the LessThan comparator from circomlib:

//... import comparators from circomlib ...

template MAIN() {

    signal input v;
    signal output type;
    signal check_v;
    component lessThan = LessThan(8);

    type <-- v >> 5;
    check_v <== type*32;
    // use circomlib LessThan to check that (v - check_v) < 32
    lessThan.in[0] <== v - check_v;
    lessThan.in[1] <== 32;    
    lessThan.out === 1;
}

component main = MAIN();
```

Answer 2

EDIT: This doesn't sufficiently verify the shift operation. See @meshcollider's answer instead.

Ok, i'm not fully sure if this is right, but this is what I came up with.

pragma circom 2.0.0;

template MAIN() {

    signal input v;
    signal output type;

    // assign `type` signal
    // shift 0bXXXYYYYY to 0b00000XXX
    // v is a trusted signal
    type <-- v >> 5;

    // prepare constraint checking for `type`
    signal three_upper_bits;
    // 0b11100000 = 0xE0
    // v is trusted signal
    three_upper_bits <-- v & 0xE0; // 3 upper bits of v (0bXXX00000). v can only be 8 bits.

    // should_only_be_lower_bits is 0b000YYYYY
    // we get it by 0bXXXYYYYY - 0bXXX00000 to get 0b000YYYYY
    var should_only_be_lower_bits = v - three_upper_bits;
    // we're checking that should_only_be_lower_bits can only be LESS THAN 32 (0b00011111)
    // that verifies that three_upper_bits are pristine and were not messed with.
    // if someone were to mess with three_upper_bits, should_only_be_lower_bits would contain higher bits
    // and be more than 32 (0b00011111).
    // by doing that, we cryptographically assert that should_only_be_lower_bits is in the form of 0b000YYYYY
    signal upper_bit_1;
    signal upper_bit_2;
    signal upper_bit_3;
    upper_bit_1 <-- should_only_be_lower_bits & 0x80; // 0b10000000. This signal can be 0bX0000000
    upper_bit_2 <-- should_only_be_lower_bits & 0x40; // 0b01000000. This signal can be 0b0X000000
    upper_bit_3 <-- should_only_be_lower_bits & 0x20; // 0b00100000. This signal can be 0b00X00000
    upper_bit_1 === 0; // Assert that 0bX0000000 is 0b00000000
    upper_bit_2 === 0; // Assert that 0b0X000000 is 0b00000000
    upper_bit_3 === 0; // Assert that 0b00X00000 is 0b00000000

    // generate constraint for type signal
    // 2^5 = 32
    type * 32 === three_upper_bits;
}

component main = MAIN();

The comments go through my thinking, but essentially I verify the signal assignments with substraction/multiplication constraints.

Answer 3

circomlib/circuits/sha256/shift.circom has a ShR component which performs right shift.

    var InputBits = 8;
    var ResultBits = 3;

    // convert v to bits
    component n2b = Num2Bits(InputBits);
    n2b.in <== v;

    // shift
    component shr = ShR(InputBits, 5); // v >> 5
    for (var i = 0; i < InputBits; i++) {
        shr.in[i] <== n2b.out[i];
    }

    // convert back to number
    component b2n = Bits2Num(ResultBits);
    for (var i = 0; i < ResultBits; i++) {
        b2n.in[i] <== shr.out[i];
    }
    type <== b2n.out;

Answer 4

Following is a solution for the error.

//Code Begins

pragma circom 2.0.0;

template MAIN() {

signal input v;
signal output type;
signal rs;

rs <-- v >> 5;
type <== rs;

}

component main = MAIN();

//End of code

Regards