usize in const typechecking may be inconsistent with Verus global

[tjhance]

The theory is that Verus is checking your code for both 32-bit and 64-bit architectures, no matter which machine you're running on.

However, assumptions about your platform can leak into Verus's assumptions:

proof fn test<const X: usize>()
    ensures 0 <= X <= usize::MAX,
{
}

proof fn ensure_is_64_bit()
    ensures usize::MAX == 0xffff_ffff_ffff_ffff,
{
    test::<0xffff_ffff_ffff>();
}

[utaal]

@tjhance we should coordinate a fix for this that also addresses the const-eval related issues (from 1.79).