fix: handle several reachable panics

[Marsman1996]

This PR handles #2175, #2184 and more
Fix #2174

My pipeline depends on Verus returning errors in JSON format.
When Verus panics, no JSON message is produced, which breaks the pipeline.
This PR changes the behavior to return a structured error message instead of panicking.

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

[Marsman1996]

check_expr_handle_mut_arg

https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=82beda3c9809ccf0d59539c8b381193b

PoC

use vstd::prelude::*;
verus!{
proof fn p(){
    let _f = |x:int| -> int { return x; };
}
fn main(){}
}

Log

thread 'rustc' (42) panicked at vir/src/modes.rs:2891:30:
internal error: missing return type
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

binopkind_to_binaryop_inner

https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=faaee97e93ac1ef62099c7780d2124ec

PoC

use vstd::prelude::*;
verus! {
fn f() {
    let x = true & false;
    let z = true ^ false;
    let y = true | false;
}
fn main(){}
}

Log

thread 'rustc' (42) panicked at rust_verify/src/rust_to_vir_expr.rs:3046:21:
bitwise AND for bools (i.e., the not-short-circuited version) not supported
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[tjhance]

the bitwise operator change looks fine; the other 2 are internal errors (the expected invariants on verus's internal state are being violated) so they need further investigation. I'd appreciate it if (in addition to this PR) you could:

• leave #2175 open
• file an additional issue with the closure "missing return type" example

thanks!

[Marsman1996]

• file an additional issue with the closure "missing return type" example

See #2184

[Marsman1996]

The new commit fixes #2174

error: The verifier does not yet support the following Rust feature: this type of bound
 --> ./test/impl.rs:3:15
  |
3 | pub fn f() -> impl Copy { 1u8 }
  |               ^^^^^^^^^

error: aborting due to 1 previous error

just like

verus/source/rust_verify/src/rust_to_vir_base.rs

Line 2328 in ac50b8f

"Verus does not yet support this type of bound",

and

verus/source/rust_verify/src/rust_to_vir_base.rs

Line 1791 in ac50b8f

return err_span(*span, "Verus does not yet support this type of bound");