Reachable unwrap panic in opaque_def_to_vir #2174
Description
PoC
use vstd::prelude::*;
verus! {
pub fn f() -> impl Copy { 1u8 }
fn main() {}
}Panic Log
verus/source/rust_verify/src/rust_to_vir_base.rs
Lines 2264 to 2280 in ac50b8f
warning: verus was compiled in debug mode, which will result in worse performance
thread 'rustc' (1362312) panicked at rust_verify/src/rust_to_vir_base.rs:2280:26:
called `Option::unwrap()` on a `None` value
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: core::panicking::panic
3: core::option::unwrap_failed
4: <core::option::Option<alloc::sync::Arc<vir::ast::GenericBoundX>>>::unwrap
at /home/root/.rustup/toolchains/1.93.0-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:1016:21
5: rust_verify::rust_to_vir_base::opaque_def_to_vir
at ./source/rust_verify/src/rust_to_vir_base.rs:2280:26
6: rust_verify::rust_to_vir_base::check_fn_opaque_ty
at ./source/rust_verify/src/rust_to_vir_base.rs:2217:5
7: rust_verify::rust_to_vir::check_item
at ./source/rust_verify/src/rust_to_vir.rs:184:21
8: rust_verify::rust_to_vir::crate_to_vir
at ./source/rust_verify/src/rust_to_vir.rs:482:25
9: <rust_verify::verifier::Verifier>::construct_vir_crate::<rust_verify::verifier::Reporter>
at ./source/rust_verify/src/verifier.rs:2695:13
10: <rust_verify::verifier::VerifierCallbacksEraseMacro as rustc_driver_impl::Callbacks>::after_expansion
at ./source/rust_verify/src/verifier.rs:3093:64
11: <rustc_interface::passes::create_and_enter_global_ctxt<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>::{closure#2} as core::ops::function::FnOnce<(&rustc_session::session::Session, rustc_middle::ty::context::CurrentGcx, alloc::sync::Arc<rustc_data_structures::jobserver::Proxy>, &std::sync::once_lock::OnceLock<rustc_middle::ty::context::GlobalCtxt>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_middle::arena::Arena>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_hir::Arena>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2})>>::call_once::{shim:vtable#0}
12: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
Env
Verus Version: 2026.02.11 c780c07