Add support for disabling overflow checks

[WeetHet]

It's basically impossible to write code that uses any arithmetics and not run into needing to insert tons of invariants and guards to ensure it does not overflow. In reality, my code works with reasonable numbers, so it can't overflow, and I care more about other qualities of it. So a switch to disable overflow checks would be nice to have

[utaal]

Thank you @WeetHet for the input. I've moved this to a discussion, as that's what we use for feature requests.

We'd need to be careful in adding a feature like the one you're describing, to not run into potential unsoundness, but I take your point of wanting to verify other properties.

I realize this is probably not possible at the moment, as the relevant functions are lacking verus specifications, but would you be open to using the checked (or panicking) versions of the arithmetic operations? Or would you really want just to disable overflow checks?

[utaal]

One challenge you're encountering with your approach is that by default verus requires you to import all relevant facts into the loop context, including n <= 10, as a new invariant; you can override this behavior using #[verifier::loop_isolation(false)] on the loop.

[WeetHet]

Thanks, I'm not that experienced yet to write something like this, so I've gone the other way and written it this way:

#[verifier::external_body]
fn add_one(n: i32) -> (result: i32)
    ensures result == n + 1,
{
    n + 1
}

#[verifier::external_body]
fn square(n: i32) -> (result: i32)
    ensures n * n == result,
{
    n * n
}

fn integer_square_root(n: i32) -> (result: i32)
    requires n >= 1,
    ensures
        0 <= result * result,
        result * result <= n,
        n < (result + 1) * (result + 1),
{
    let mut result = 0;
    while square(add_one(result)) <= n
        invariant
            0 <= result,
            0 <= result * result <= n,
    {
        result = add_one(result);
    }
    result
}

Which is a way to disable overflow checks, I guess, so this discussion is resolved, I guess

[utaal]

This is very risky, as those two external_body functions are unsound, and I think you can prove false from them, technically invalidating your whole verification effort.
I would leave the discussion open, to consider options to reduce the overflow checking burden.

[utaal]

Here's how to trivially prove false from add_one, and why it's dangerous:

#[verifier::external_body]
fn add_one(n: i32) -> (result: i32)
    ensures result == n + 1,
{
    n + 1
}

fn get_false()
    ensures false {
    let n1 = i32::MAX;
    let n2 = add_one(n1);
    assert(n2 > n1);
    assert(false);
}

fn main() {
    let a = 2 + 3;
    get_false();
    assert(a == 6);
}

[WeetHet]

Yeah, sure, that's true, I've reopened the discussion