fix: handle panics for bit_vector

[Marsman1996]

Fix reachable panic for bit_vector.

I modify the panic code in source/vir/src/bitvector_to_air.rs.
However, codex suggests that it shall be handled in the early stage, and it adds check code in source/vir/src/ast_to_sst.rs.

PoCs:

use vstd::prelude::*;

verus! {
proof fn test() {
    use verus_builtin::*;
    assert(f32_to_bits(1.0f32) == 0u32) by(bit_vector);
}
}

fn main() {}

and

use vstd::prelude::*;

verus! {
proof fn test() {
    use verus_builtin::*;
    assert(strslice_len::<u64>(7u64) == 0int) by(bit_vector);
}
}

fn main() {}

Logs

thread '<unnamed>' (45030) panicked at vir/src/bitvector_to_air.rs:447:37:
internal error: unexpected float to bits coercion
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (45030) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

and

thread '<unnamed>' (12041) panicked at vir/src/bitvector_to_air.rs:456:32:
internal error: matching for bit vector ops on this match should be impossible
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (12041) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[Marsman1996]

PoC

use vstd::prelude::*;

verus! {

proof fn test() {
    assert(
        infer_spec_for_loop_iter(1u8, 2u8, false)
            === infer_spec_for_loop_iter(1u8, 2u8, false)
    ) by(bit_vector);
}

}

fn main() {}

and

use vstd::prelude::*;

verus! {

proof fn test() {
    assert(1.0real.floor() == 1int) by(bit_vector);
}

}

fn main() {}

Log

thread '<unnamed>' (31) panicked at vir/src/bitvector_to_air.rs:460:17:
internal error: unexpected Option type (from InferSpecForLoopIter)
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=822a7685c61df92ba9a02fc9aebf1ebe#)

thread '<unnamed>' (31) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

and

thread '<unnamed>' (2539554) panicked at vir/src/bitvector_to_air.rs:446:35:
internal error: unexpected real to int coercion
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (2539554) panicked at rust_verify/src/verifier.rs:2228:29:
worker thread panicked

[sunmy2019]

Could we refine the error message here?

'Unsupported' might be interpreted by users as a permanent restriction.

Phrasing it as 'not yet supported' would be more encouraging and accurately reflect the status.

[Marsman1996]

Could we refine the error message here?

'Unsupported' might be interpreted by users as a permanent restriction.

Phrasing it as 'not yet supported' would be more encouraging and accurately reflect the status.

Update the error message.

[tjhance]

i'm not sure about the logic for putting the checks in ast_to_sst. bitvector_to_air is the source of truth for what's supported. There are already a large number of checks there, anyway, and it doesn't make sense to split them up without a good reason (like if the check was easier to do elsewhere, but that doesn't seem to be the case here). It is true that earlier is better, usually, but not if it decreases maintainability, and anyway, there's not much difference between bitvector_to_air and ast_to_sst. A better (i.e., earlier) would be well_formed.rs, or possibly modes.rs, but even then, it seems unnecessary to me.

[Marsman1996]

i'm not sure about the logic for putting the checks in ast_to_sst. bitvector_to_air is the source of truth for what's supported. There are already a large number of checks there, anyway, and it doesn't make sense to split them up without a good reason (like if the check was easier to do elsewhere, but that doesn't seem to be the case here). It is true that earlier is better, usually, but not if it decreases maintainability, and anyway, there's not much difference between bitvector_to_air and ast_to_sst. A better (i.e., earlier) would be well_formed.rs, or possibly modes.rs, but even then, it seems unnecessary to me.

Removed the checks in source/vir/src/ast_to_sst.rs.

[Marsman1996]

I have another question: Does this PR need to add test?
Since the panic error and fix are straightforward.