Bitwise proofs

[George-Miao]

Hi! First of all thanks for the great project!

I'm new to the language and was trying to learn it by verifying one of my libraries, thin-cell. It's a reference counted smart pointer with RefCell-like internal mutability. The core logic is State, a usize wrapper with lowest bit as the borrow flag and the rest as the reference counts. But I wasn't able to verify the logic with verus and eventually reduces to the following example:

proof fn test_bitwise(input: u64) -> (output: u64)
    requires
        input & 1 == 0,
        input & !1 == 0,
    ensures
        output == 0,
{
    assert(input == 0) by (bit_vector);
    input
}

Which gives me:

error: bitvector assertion not satisfied
   --> src/verify.rs:78:5
    |
 78 |     assert(input == 0) by (bit_vector);
    |     ^^^^^^

What additional assert/lemma/etc do I need? Any help appreciated!

[parno]

Thanks for giving Verus a try! To answer your question, the bit-vector solver, by default, doesn't inherit the surrounding proof context, so in your example, it doesn't know anything about input except that it's a 64-bit unsigned number. This design helps keep the bit-vector solver faster and more deterministic. To provide any necessary context, you can include a requires clause on your assert. With that added, it verifies.

The bit-vector docs have more details.

[George-Miao]

Cool! This really helps. Thanks.

[tjhance]

I would also check out the guide page on bitvector which has more tips and tricks.