[Bug] Prover cannot deal with abort codes using upper 5 bytes

[wrwg]

Drop in the following into functional prover tests:

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

    spec module {
        pragma verify = true;
    }

    fun assert_with_spec(x: u64) {
        assert!(x > 815);
    }
    spec assert_with_spec  {
        aborts_if x > 815 with 0xCA26CBD9BE0B0000; //std::error::internal(0) + 0xCA26CBD9BE000000;
    }
}

The prover says contradicting things:

Move prover returns: exiting with verification errors
error: function does not abort under this condition
   ┌─ tests/sources/functional/aborts_if_compiler_codes.move:18:9
   │
18 │         aborts_if x > 815 with 0xCA26CBD9BE0B0000; //std::error::internal(0) + 0xCA26CBD9BE000000;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/aborts_if_compiler_codes.move:14: assert_with_spec
   =         x = <redacted>
   =     at tests/sources/functional/aborts_if_compiler_codes.move:15: assert_with_spec
   =     at tests/sources/functional/aborts_if_compiler_codes.move:16: assert_with_spec
   =     at tests/sources/functional/aborts_if_compiler_codes.move:18: assert_with_spec (spec)

error: abort not covered by any of the `aborts_if` clauses
   ┌─ tests/sources/functional/aborts_if_compiler_codes.move:17:5
   │
15 │           assert!(x > 815);
   │           ------ abort happened here with code 0xCA26CBD9BE0B0000
16 │       }
17 │ ╭     spec assert_with_spec  {
18 │ │         aborts_if x > 815 with 0xCA26CBD9BE0B0000; //std::error::internal(0) + 0xCA26CBD9BE000000;
19 │ │     }
   │ ╰─────^
   │
   =     at tests/sources/functional/aborts_if_compiler_codes.move:14: assert_with_spec
   =         x = <redacted>
   =     at tests/sources/functional/aborts_if_compiler_codes.move:15: assert_with_spec
   =         ABORTED

This probably happens because the code passed to with has the higher bytes truncated. However, if that is the case, we need to also truncate the actual code, otherwise we can never reach it.

[rahxephon89]

@wrwg, the aborts_if condition should be aborts_if x <= 815 with 0xCA26CBD9BE0B0000;, which can be proved.

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

    spec module {
        pragma verify = true;
    }

    fun assert_with_spec(x: u64) {
        assert!(x > 815);
    }
    spec assert_with_spec  {
        aborts_if x <= 815 with 0xCA26CBD9BE0B0000; //std::error::internal(0) + 0xCA26CBD9BE000000;
    }
}