Usize is only able to handle the number of 32 bits

[zpzigi754]

The below code would generate an error saying that integer literal out of range.

use vstd::prelude::*;

verus! {

pub const NUMBER: u64 = 0x1_0000_0000; // this is supported
pub const NUMBER2: usize = 0x1_0000_0000; // this is not supported

fn main() {
}

} // verus!

Given the error message, usize in verus seems to be interpreted as 32bits integer. For 64bits environment like x64, I think that usize should be interpreted as 64bits integer.

[utaal]

You can set the size of usize using the global size directive.

Here are a couple of examples. We'll be adding documentation for this soon.

        global size_of usize == 4;

        fn test1() {  // ARCH-WORD-BITS-32
            assert(arch_word_bits() == 32);
        }
        fn test2() {
            assert(arch_word_bits() == 32) by(compute);
        }

        fn test_constants() {
            assert(isize::MIN == -0x80000000);
            assert(usize::MAX == 0xffffffff);
            assert(isize::MAX == 0x7fffffff);
            assert(usize::BITS == 32);
            assert(isize::BITS == 32);
        }

        fn fail1() {
            assert(arch_word_bits() == 64); // FAILS
        }

        global size_of usize == 8;

        fn test1() {  // ARCH-WORD-BITS-64
            assert(arch_word_bits() == 64);
        }
        fn test2() {
            assert(arch_word_bits() == 64) by(compute);
        }

        fn test_constants() {
            assert(isize::MIN == -0x8000000000000000);
            assert(usize::MAX == 0xffffffffffffffff);
            assert(isize::MAX == 0x7fffffffffffffff);
            assert(usize::BITS == 64);
            assert(isize::BITS == 64);
        }

        fn fail1() {
            assert(arch_word_bits() == 32); // FAILS
        }

[zpzigi754]

Thank you very much, @utaal. Setting the size of usize with the global size directive would be really helpful.