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>[ Rc::<T>::new ](t: T) -> (v: Rc<T>)
23    ensures
24        v == t,
25;
26
27pub assume_specification<T>[ Arc::<T>::new ](t: T) -> (v: Arc<T>)
28    ensures
29        v == t,
30;
31
32pub assume_specification<T: Clone, A: Allocator + Clone>[ <Box<T, A> as Clone>::clone ](
33    b: &Box<T, A>,
34) -> (res: Box<T, A>)
35    ensures
36        cloned::<T>(**b, *res),
37;
38
39pub assume_specification<T, A: Allocator>[ Rc::<T, A>::try_unwrap ](v: Rc<T, A>) -> (result: Result<
40    T,
41    Rc<T, A>,
42>)
43    ensures
44        match result {
45            Ok(t) => t == v,
46            Err(e) => e == v,
47        },
48;
49
50pub assume_specification<T, A: Allocator>[ Rc::<T, A>::into_inner ](v: Rc<T, A>) -> (result: Option<
51    T,
52>)
53    ensures
54        result matches Some(t) ==> t == v,
55;
56
57} // verus!
vstd/std_specs/smart_ptrs.rs

vstd/std_specs/
smart_ptrs.rs
