vstd 0.0.0-2026-04-20-1748

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

use crate::contrib::exec_spec::*;
use crate::prelude::*;
use std::collections::{HashMap, HashSet};

verus! {

/// Impls for shared traits
impl<'a, T: Sized + DeepView> ToRef<&'a Option<T>> for &'a Option<T> {
    #[inline(always)]
    fn get_ref(self) -> &'a Option<T> {
        self
    }
}

impl<'a, T: DeepView + DeepViewClone> ToOwned<Option<T>> for &'a Option<T> {
    #[inline(always)]
    fn get_owned(self) -> Option<T> {
        self.deep_clone()
    }
}

impl<T: DeepViewClone> DeepViewClone for Option<T> {
    #[inline(always)]
    fn deep_clone(&self) -> Self {
        match self {
            Some(t) => Some(t.deep_clone()),
            None => None,
        }
    }
}

impl<'a, T: DeepView> ExecSpecEq<'a> for &'a Option<T> where &'a T: ExecSpecEq<'a, Other = &'a T> {
    type Other = &'a Option<T>;

    #[inline(always)]
    fn exec_eq(this: Self, other: Self::Other) -> bool {
        match (this, other) {
            (Some(t1), Some(t2)) => <&'a T>::exec_eq(t1, t2),
            (None, None) => true,
            _ => false,
        }
    }
}

/// Traits for Option methods
/// Spec for executable version of [`Option::unwrap`].
pub trait ExecSpecOptionUnwrap<'a>: Sized + DeepView {
    type Elem: DeepView + DeepViewClone;

    spec fn is_some_spec(&self) -> bool;

    fn exec_unwrap(self) -> Self::Elem
        requires
            self.is_some_spec(),
    ;
}

/// Impls for Option methods
impl<'a, T> ExecSpecOptionUnwrap<'a> for &'a Option<T> where T: DeepView + DeepViewClone {
    type Elem = T;

    open spec fn is_some_spec(&self) -> bool {
        self.is_some()
    }

    #[inline(always)]
    fn exec_unwrap(self) -> (res: Self::Elem)
        ensures
            res.deep_view() == self.deep_view()->0,
    {
        self.deep_clone().unwrap()
    }
}

} // verus!