vstd_extra/
panic.rs

1//! Runtime panic helper whose type (`-> !`) lets Verus discharge
2//! post-conditions by branch elimination at the call site.
3use vstd::prelude::*;
4use vstd::vpanic;
5
6verus! {
7
8/// Represents the intention that the code will panic at some point in the future.
9/// Consumed by [`panic_diverge`] to ensure that the top-level API spec must always
10/// intentionally document potential panics.
11pub uninterp spec fn may_panic() -> bool;
12
13/// Unconditionally diverges. Must be provided with a [`may_panic()] token to ensure that
14/// the panic is expected.
15#[verifier::external_body]
16pub fn panic_diverge() -> !
17    requires
18        may_panic(),
19{
20    vpanic!("")
21}
22
23/// Extension trait providing a panicking `unwrap` that models Rust's
24/// real `Option::unwrap` semantics.
25///
26/// Verus' `Option::unwrap` carries a `requires self is Some`; Rust's
27/// `unwrap` instead panics on `None`. `unwrap_or_panic` *diverges* on
28/// `None` (via [`panic_diverge`]) — a sound model of the real panic —
29/// and discharges `is_present()` (i.e. `self is Some` for `Option`) at
30/// the call site by branch elimination, so callers need not prove the
31/// value is populated.
32pub trait UnwrapOrPanic: Sized {
33    type Inner;
34
35    spec fn is_present(&self) -> bool;
36
37    spec fn payload(&self) -> Self::Inner;
38
39    fn unwrap_or_panic(self) -> (r: Self::Inner)
40        requires
41            !self.is_present() ==> may_panic(),
42        ensures
43            self.is_present(),
44            r == self.payload(),
45    ;
46}
47
48impl<T> UnwrapOrPanic for Option<T> {
49    type Inner = T;
50
51    open spec fn is_present(&self) -> bool {
52        self is Some
53    }
54
55    open spec fn payload(&self) -> T {
56        self->0
57    }
58
59    fn unwrap_or_panic(self) -> (r: T) {
60        match self {
61            Some(v) => v,
62            None => panic_diverge(),
63        }
64    }
65}
66
67} // verus!
vstd_extra/panic.rs

vstd_extra/
panic.rs
