from "field" import FIELD_SIZE_IN_BITS;

// we can compare numbers whose difference fits in (pbits - 2) bits
// It should not work for the maxvalue = 2^(pbits - 2) - 1 augmented by one
// /!\ should be called with a = 0

def main(field a) {
    u32 pbits = FIELD_SIZE_IN_BITS;
    // we added a = 0 to prevent the condition to be evaluated at compile time
    field maxvalue = a + (2**(pbits - 2) - 1);
    bool c = a < maxvalue + 1;
    return;
}
