vstd_extra/external/
deref.rs

1#![deprecated(
2    note = "If you can, do not use this module as it adds assumptions about the core of Rust's deref semantics."
3)]
4
5use alloc::boxed::Box;
6use core::hint::spin_loop;
7use core::mem::ManuallyDrop;
8use core::ops::Deref;
9use vstd::prelude::*;
10// Assumptions about external functions
11
12verus! {
13
14/// This is a workaround to add an uninterpreted specification of Deref trait, as Deref is included in Verus but does not have spec functions.
15/// It is currently not used, and we do not recommend using it, as it adds assumptions about the core of Rust's deref semantics, which may cause soundness issues if not used carefully.
16/// It may change if Verus adds native support for spec functions in the Deref trait.
17pub trait DerefSpec: Deref {
18    spec fn deref_spec(&self) -> &<Self as Deref>::Target;
19
20    proof fn deref_spec_eq(&self)
21        ensures
22            forall|output|
23                call_ensures(Self::deref, (self,), output) ==> self.deref_spec() == output,
24    ;
25}
26
27impl<T: Deref> DerefSpec for T {
28    uninterp spec fn deref_spec(&self) -> &<Self as Deref>::Target;
29
30    axiom fn deref_spec_eq(&self);
31}
32
33// Special Cases
34pub broadcast axiom fn ref_deref_spec<T>(r: &T)
35    ensures
36        #[trigger] *(r.deref_spec()) == *r,
37;
38
39pub broadcast axiom fn box_deref_spec<T>(b: Box<T>)
40    ensures
41        #[trigger] *(b.deref_spec()) == *b,
42;
43
44pub broadcast axiom fn rc_deref_spec<T>(r: alloc::rc::Rc<T>)
45    ensures
46        #[trigger] *(r.deref_spec()) == *r,
47;
48
49pub broadcast axiom fn arc_deref_spec<T>(a: alloc::sync::Arc<T>)
50    ensures
51        #[trigger] *(a.deref_spec()) == *a,
52;
53
54pub broadcast group group_deref_spec {
55    ref_deref_spec,
56    box_deref_spec,
57    rc_deref_spec,
58    arc_deref_spec,
59}
60
61} // verus!
vstd_extra/external/deref.rs

vstd_extra/external/
deref.rs
