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