bitvector encoding overhaul

[tjhance]

• Support signed integers
• Support unwrapped arithmetic (e.g., add two bv8 values to get a bv9)
• Support comparisons for ints of different types as in ordinary spec code
• Support queries that are dependent on the arch-size (we generate two queries, one for 32 bit, one for 64 bit)
• In AIR prelude, make operations independent of bitwidth

Here are some things that now work which didn't previously:

proof fn test10(a: u8, b: u8) {
    // We can write conditions about overflow in bit_vector assertion
    assert((a & b) == 0 ==> (a | b) == (a + b) && (a + b) < 256) by(bit_vector);
}

proof fn test11(x: u32, y: u32) {
    // XOR operation is independent of bitwidth so we don't need bit_vector solver to do this:
    assert((x as u64) ^ (y as u64) == (x ^ y) as u64);
}

proof fn test_usize(x: usize, y: usize, z: usize) {
    assert(((x & y) & z) == (x & (y & z))) by(bit_vector);
}

proof fn test_signed(x: i8, y: i8, z: i8, u: u8) {
    assert(!(x & y) == (!x | !y)) by(bit_vector);
    assert((!z) == (!(z as i32))) by(bit_vector);
    assert((z & (128u8 as i8)) != 0 <==> z < 0) by(bit_vector);

    // Compare signed vs unsigned
    assert(u > -1) by(bit_vector);
    assert(u > 128 ==> u > x) by(bit_vector);
}

todo

• [x] Needs tests
• [x] Resolve division-by-0 inconsistency

[parno]

Can we add a warning about +, -, * to help people with this?

At one point, we had talked about adding a bits! macro that would automatically replace operators like + with add. It would be nice to have the warning point at the macro, if it existed.

[tjhance]

It occurs to me that since !x is just -x - 1, it might be reasonable to have the AIR prelude know this automatically.

[tjhance]

@Chris-Hawblitzel I believe I've addressed all your comments