`eval_global` fails on `usize` and `isize` expressions.

[ayhon]

When defining a usize constant in Rust initialized by a constant expression, eval_global fails to prove that the computation doesn't fail.

MWE:

const W: usize = 0 + 0;
// const W: isize = 0 + 0; // Also works

I believe this is because prove_eval_global is unable to reason about the bounds of Std.Usize and Std.Isize.

As a workaround, I've added native_decide to prove_eval_global, which is able to inspect the System.Platform.numBits constants and therefore close the goal. However, this approach relies on trusting the compilation toolchain.

[sonmarcho]

Also, using native_decide reveals the value of System.Platform.numBits (which is linked to the architecture on which you actually do the proofs). It means that someone can prove that System.Platform.numBits = 32 while someone else proves that System.Platform.numBits = 64 on a different machine, which is a bit annoying... Following the discussion on the Zulip, I have a solution for this, which is simply not to use BitVec.ofNat in the definition of Scalar.ofNat.