Unintuitive precondition for absence of overflow

[jschneider-bensch]

The below precondition leads to a type error in F*, since a + b is translated to (a +! b <: usize) in the precondition, which could also overflow.
Interestingly the alternative formulation using subtraction does not lead to an error, so is -! saturating? Is there a way to write this as a sum without using F* directly?

#[hax_lib::requires(a + b <= usize::MAX)]
//#[hax_lib::requires(a <= usize::MAX - b)]  // This works
fn f(a: usize, b: usize) {
    let c = a + b;
}

Open this code snippet in the playground

[W95Psp]

Sorry for the late repply -- I think we spoke about it in chat though.

But, for reference, here, you are indeed hitting the fact that preconditions should be panic-free, just like any other piece of code.
The issue is that you are doing arithmetic with machine integers, which are bounded.

So, the escape hatch here is hax_lib::int, which provides unbounded mathematical integers.
You can use it in the following way:

use hax_lib::int::*;

#[hax_lib::requires(a.to_int() + b.to_int() <= usize::MAX.to_int())]
fn f(a: usize, b: usize) {
    let c = a + b;
}

Open this code snippet in the playground

[jschneider-bensch]

Indeed, that's how I solved it. Thanks for coming back and documenting this here!