i8::MIN / -1 panics but verifies

[ambiso]

The following function verifies with the condition that y != 0, but I believe it should not, since it can panic.

// Read more about `requires` here: https://hacspec.org/book/tutorial/panic-freedom.html
#[hax_lib::requires(y != 0)]
fn d(x: i8, y: i8) -> i8 {
    x / y
}

Open this code snippet in the playground

When calling this function with i8::MIN and -1 it overflows:

fn d(x: i8, y: i8) -> i8 {
    x / y
}

fn main() {
    println!("{}", d(i8::MIN, -1));
}

$ cargo run
   Compiling hax_repro v0.1.0 (/home/projects/dump/hax_repro)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.12s
     Running `target/debug/hax_repro`
thread 'main' panicked at src/main.rs:2:5:
attempt to divide with overflow
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

(See also https://blog.regehr.org/archives/887 and https://mastodon.social/@regehr/113564124872096630 )

[ambiso]

More direct repro:

#[allow(unconditional_panic)]

// Read more about `requires` here: https://hacspec.org/book/tutorial/panic-freedom.html
#[hax_lib::requires(true)]
fn d() -> i8 {
    (-128i8) / (-1i8)
}

Playground

[ambiso]

I assume this condition would need to be updated?

hax/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

Line 241 in 1c5e17c

let div (#t:inttype) (a:int_t t) (b:int_t t{v b <> 0}) =

It seems odd that the instantiation of the int succeeds when the resulting integer is out of bounds

hax/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

Line 243 in 1c5e17c

mk_int #t (v a / v b)

Is this assume at fault?

hax/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

Line 242 in 1c5e17c

assume(unsigned t \/ range (v a / v b) t); // see issue #423

[karthikbhargavan]

Correct: this function has an assume whereas it should have a pre-condition. We have been working on a new version of the library model which does not have these assumes, but we should fix this.

…

On Mon, Dec 2, 2024 at 2:28 PM ambiso ***@***.***> wrote: I assume this condition would need to be updated? https://github.com/hacspec/hax/blob/1c5e17c9ceee5adede0f4ea7f68bb3d8337f33a0/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti#L241 — Reply to this email directly, view it on GitHub <#1155 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFUVS3MZJVJQOCES5B7CKL2DROA5AVCNFSM6AAAAABS3MJ352VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMJRGU2DMOJZHE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>