[Bug][prover] Bitvector not working in context of aborts_if with clause

[wrwg]

Drop the following into the prover functional test dir:

module 0x42::test {
    use std::error;

    spec module {
        pragma verify = true;
    }

    fun assert_no_spec(x: u64) {
        assert!(x > 815);
    }

    fun assert_with_spec(x: u64) {
        assert!(x > 815);
    }
    spec assert_with_spec  {
        aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
    }
}

Boogie error:

Move prover returns: [internal] boogie exited with compilation errors:
aborts_if_compiler_codes.bpl(3672,47): Error: invalid type for argument 0 in application of $Or'Bv64': int (expected: bv64)
aborts_if_compiler_codes.bpl(3672,70): Error: invalid type for argument 1 in application of $Or'Bv64': int (expected: bv64)
aborts_if_compiler_codes.bpl(3675,4): Error: mismatched types in assignment command (cannot assign bv64 to int)
3 type checking errors detected in aborts_if_compiler_codes.bpl

[rahxephon89]

Automatic type inference and conversion between bv and int type is not complete but we can express this property in an awkward way by using the builtin function bv2int and int2bv:

    spec assert_with_spec  {
        aborts_if x > 815 with bv2int(int2bv(std::error::internal(0) as u64) | int2bv((0xCA26CBD9BE << 24) as u64));
    }

[wrwg]

Could there be a better error message which hints to use the conversion functions explicitly, then the errors on boogie level?

[rahxephon89]

Could there be a better error message which hints to use the conversion functions explicitly, then the errors on boogie level?

Yes, it is possible but the fix would not be trivial because in some cases constants/variables/temporaries in an expression are automatically converted into a bv type so we need to know when and where we need to insert the conversion and then give hints to users. Will come back to this issue later.

[wrwg]

Then I would still wonder whether in this case the automatic conversion just did not happen because the expression is part of an aborts-if. This is a rather obvious case where it should have triggered.