Constants and arithmetic in bitvector assertions

[matthias-brun]

I recently worked on improving the hardware model for the verified page table and in the process used bitvector assertions a fair bit. Generally, I was impressed by how powerful the bitvector prover is but also annoyed at some of the restrictions Verus currently has in place for bitvector assertions.

A lot of my bitvector reasoning involves various constants, e.g.:

pub const L3_ENTRY_SIZE: usize = PAGE_SIZE;
pub const L2_ENTRY_SIZE: usize = 512 * L3_ENTRY_SIZE;
pub const L1_ENTRY_SIZE: usize = 512 * L2_ENTRY_SIZE;
pub const L0_ENTRY_SIZE: usize = 512 * L1_ENTRY_SIZE;

I needed to prove a number of equalities involving these constants, for example the one below (for particular values of l0_idx, l1_idx, l2_idx, l3_idx)

l0_idx * L0_ENTRY_SIZE + l1_idx * L1_ENTRY_SIZE + l2_idx * L2_ENTRY_SIZE + l3_idx * L3_ENTRY_SIZE
== (l0_idx as u64) << 39u64 | (l1_idx as u64) << 30u64 | (l2_idx as u64) << 21u64 | (l3_idx as u64) << 12u64

Verus currently doesn't support using constants in bitvector assertions and arithmetic operators have to be written as function calls, which means we have to use the following assertion

assert(add(add(add(
        mul(l0_idx_u64, mul(512u64, mul(512, mul(512, 4096)))),
        mul(l1_idx_u64, mul(512u64, mul(512, 4096)))),
        mul(l2_idx_u64, mul(512, 4096))),
        mul(l3_idx_u64, 4096))
       == l0_idx_u64 << 39u64 | l1_idx_u64 << 30u64 | l2_idx_u64 << 21u64 | l3_idx_u64 << 12u64) by (bit_vector)
    requires l0_idx_u64 < 512 && l1_idx_u64 < 512 && l2_idx_u64 < 512 && l3_idx_u64 < 512;
// Previous assert proves:
// l0_idx * L0_ENTRY_SIZE + l1_idx * L1_ENTRY_SIZE + l2_idx * L2_ENTRY_SIZE + l3_idx * L3_ENTRY_SIZE
// == (l0_idx as u64) << 39u64 | (l1_idx as u64) << 30u64 | (l2_idx as u64) << 21u64 | (l3_idx as u64) << 12u64

Assertions like this are cumbersome to write and make the overall workflow with bitvector more frustrating than it has to be.
I managed to somewhat work around this by first using a normal assert or assume to identify the necessary bitvector step and then "translating" it to a bitvector assertion and proving it. However, this still failed when I occasionally discovered that I had in fact written an untrue statement and needed to change it.

I don't know how hard or easy it is to support the use of constants and normal arithmetic operators in bitvector assertions but it would make working with them significantly more pleasant.

[chanheec]

Regarding add/mul/sub, we might consider automatically translating +/*/- into add/mul/sub in the syntax macro. I suspect it might be a small change.

When we change this, I think we need to change a part of the tutorial we have. For example, the type signature of + in ghost code. (We currently say that it returns an int, but in bit-vector assertion, it will return a finite integer once this change lands)

After the change, we get this example, which can be confusing if not explicitly mentioned in the tutorial:

proof fn test() {
    assert(0xffff_ffffu32 + 1u32 == 0u32) by (bit_vector); // succeeds
    assert(0xffff_ffffu32 + 1u32 == 0u32);                 // fails, since + returns 0x1_0000_0000int
    assert(add(0xffff_ffffu32, 1u32) == 0u32);             // succeeds
}

(maybe tweaking macro here: https://github.com/verus-lang/verus/blob/main/source/builtin_macros/src/syntax.rs#L1726)
(tutorial link: the type signature table is at the end of this page: https://verus-lang.github.io/verus/guide/integers.html)

[Chris-Hawblitzel]

I like the idea of inlining constants into assert-by-bit_vector.

On the other hand, I think automatically turning +/-/* into add/sub/mul would be confusing, because, as the hypothetical tutorial example above shows, you could have assert-by-bit-vector succeed and then the same subsequent assert fail:

proof fn test() {
    assert(0xffff_ffffu32 + 1u32 == 0u32) by(bit_vector); // succeeds
    assert(0xffff_ffffu32 + 1u32 == 0u32);                // fails, since + returns 0x1_0000_0000int
}

I think if assert(P) by(bit_vector) succceds, then the subsequent assert(P) should also succeed. (In fact, this is why assert-by-bit_vector uses add/sub/mul instead of +/-/*.) So I'd like to consider alternatives that don't violate this property. Here are some ideas:

1. Keep the design as-is, using add/sub/mul.
2. Add more convenient operator symbols for bit-vector add/sub/mul in spec code, like #+, #-, #* or something
3. Provide a separate explicit macro that converts all +/-/* into add/sub/mul, as in:

proof fn test() {
    // bv!(0xffff_ffffu32 + 1u32 == 0u32) is equivalent to add(0xffff_ffffu32, 1u32) == 0u32
    assert(bv!(0xffff_ffffu32 + 1u32 == 0u32)) by(bit_vector); // succeeds
    assert(bv!(0xffff_ffffu32 + 1u32 == 0u32));                // succeeds
    assert(0xffff_ffffu32 + 1u32 == 0u32);                     // fails, since + returns 0x1_0000_0000int
}

[utaal]

[Verus meeting]

Constants

@Chris-Hawblitzel: For constants, run the interpreter, if we get a constant out, we use the constant.
To ensure this does not make things "less verifiable" (because we lost some symbolic property) we can add the constant value as an additional assumption.
The interpreter would additional help by inlining function calls.

Bit-width for usizes

To support multiple possible usize sizes we will want to run the query multiple times, once per possible size (in the absence of --arch-word-bits).

add, mul, sub

These have different semantics than +, *, - in terms of overflow. @matthias-brun thinks that unifying the syntax is not desirable, given this.
There's most support for a bv! macro. Though @matthias-brun notes that it would not be entirely obvious what it does. @jaybosamiya maybe use a more descriptive name?

[jaybosamiya]

My suggestion was something like wrapping_ops! or similar as the name; @tjhance then suggested bounded_arith!, and then @jaylorch suggested wrapping_arith!