vstd/std_specs/
smart_ptrs.rs

1use super::super::prelude::*;
2
3use alloc::boxed::Box;
4use alloc::rc::Rc;
5use alloc::sync::Arc;
6use alloc::vec::Vec;
7use core::alloc::Allocator;
8
9verus! {
10
11// TODO
12pub assume_specification<T, A: Allocator>[ <[T]>::into_vec ](b: Box<[T], A>) -> (v: Vec<T, A>)
13    ensures
14        v@ == b@,
15;
16
17pub assume_specification<T>[ Box::<T>::new ](t: T) -> (v: Box<T>)
18    ensures
19        v == t,
20;
21
22pub assume_specification<T: core::default::Default>[ <Box<
23    T,
24> as core::default::Default>::default ]() -> (res: Box<T>)
25    ensures
26        T::default.ensures((), *res),
27;
28
29pub assume_specification<T>[ Rc::<T>::new ](t: T) -> (v: Rc<T>)
30    ensures
31        v == t,
32;
33
34pub assume_specification<T: core::default::Default>[ <Rc<
35    T,
36> as core::default::Default>::default ]() -> (res: Rc<T>)
37    ensures
38        T::default.ensures((), *res),
39;
40
41pub assume_specification<T>[ Arc::<T>::new ](t: T) -> (v: Arc<T>)
42    ensures
43        v == t,
44;
45
46pub assume_specification<T: core::default::Default>[ <Arc<
47    T,
48> as core::default::Default>::default ]() -> (res: Arc<T>)
49    ensures
50        T::default.ensures((), *res),
51;
52
53pub assume_specification<T: Clone, A: Allocator + Clone>[ <Box<T, A> as Clone>::clone ](
54    b: &Box<T, A>,
55) -> (res: Box<T, A>)
56    ensures
57        cloned::<T>(**b, *res),
58;
59
60pub assume_specification<T, A: Allocator>[ Rc::<T, A>::try_unwrap ](v: Rc<T, A>) -> (result: Result<
61    T,
62    Rc<T, A>,
63>)
64    ensures
65        match result {
66            Ok(t) => t == v,
67            Err(e) => e == v,
68        },
69;
70
71pub assume_specification<T, A: Allocator>[ Rc::<T, A>::into_inner ](v: Rc<T, A>) -> (result: Option<
72    T,
73>)
74    ensures
75        result matches Some(t) ==> t == v,
76;
77
78} // verus!
vstd/std_specs/smart_ptrs.rs

vstd/std_specs/
smart_ptrs.rs
