vstd/resource/
ghost_var.rs

1#[cfg(verus_keep_ghost)]
2use super::super::modes::tracked_swap;
3use super::super::prelude::*;
4use super::Loc;
5use super::frac::FracGhost;
6
7verus! {
8
9/// See [`GhostVarAuth<T>`] for more information.
10pub tracked struct GhostVar<T> {
11    frac: FracGhost<T>,
12}
13
14impl<T> GhostVar<T> {
15    #[verifier::type_invariant]
16    spec fn inv(self) -> bool {
17        self.frac.frac() == (1 as real) / (2 as real)
18    }
19
20    pub closed spec fn id(self) -> Loc {
21        self.frac.id()
22    }
23
24    pub closed spec fn view(self) -> T {
25        self.frac.view()
26    }
27}
28
29/// `GhostVarAuth<T>` is one half of a pair of tokens—the other being [`GhostVar<T>`].
30/// These tokens each track a value, and they can only be allocated or updated together.
31/// Thus, the pair of tokens always agree on the value, but they can be owned separately.
32///
33/// One possible application is to have a library which
34/// keeps `GhostVarAuth<T>` and maintains an invariant relating the implementation's
35/// abstract state to the value of `GhostVarAuth<T>`.  Both `GhostVarAuth<T>`
36/// and [`GhostVar<T>`] are needed together to update the value, but either one alone
37/// allows reasoning about the current state.
38///
39/// These tokens can be implemented using fractional permissions, e.g., [`FracGhost`].
40///
41/// ### Example
42///
43/// ```
44/// fn example() {
45///     let tracked (mut gauth, mut gvar) = GhostVarAuth::<u64>::new(1);
46///     assert(gauth@ == 1);
47///     assert(gvar@ == 1);
48///     proof {
49///         gauth.update(&mut gvar, 2);
50///     }
51///     assert(gauth@ == 2);
52///     assert(gvar@ == 2);
53/// }
54/// ```
55pub tracked struct GhostVarAuth<T> {
56    frac: FracGhost<T>,
57}
58
59impl<T> GhostVarAuth<T> {
60    #[verifier::type_invariant]
61    spec fn inv(self) -> bool {
62        self.frac.frac() == (1 as real) / (2 as real)
63    }
64
65    pub closed spec fn id(self) -> Loc {
66        self.frac.id()
67    }
68
69    pub closed spec fn view(self) -> T {
70        self.frac.view()
71    }
72
73    /// Allocate a new pair of tokens, each initialized to the given value.
74    pub proof fn new(v: T) -> (tracked result: (GhostVarAuth<T>, GhostVar<T>))
75        ensures
76            result.0.id() == result.1.id(),
77            result.0@ == v,
78            result.1@ == v,
79    {
80        let tracked mut f = FracGhost::<T>::new(v);
81        let tracked v = GhostVar::<T> { frac: f.split() };
82        let tracked a = GhostVarAuth::<T> { frac: f };
83        (a, v)
84    }
85
86    /// Ensure that both tokens agree on the value.
87    pub proof fn agree(tracked &self, tracked v: &GhostVar<T>)
88        requires
89            self.id() == v.id(),
90        ensures
91            self@ == v@,
92    {
93        self.frac.agree(&v.frac)
94    }
95
96    /// Update the value on each token.
97    pub proof fn update(tracked &mut self, tracked v: &mut GhostVar<T>, new_val: T)
98        requires
99            old(self).id() == old(v).id(),
100        ensures
101            self.id() == old(self).id(),
102            v.id() == old(v).id(),
103            old(self)@ == old(v)@,
104            self@ == new_val,
105            v@ == new_val,
106    {
107        let tracked (mut ms, mut mv) = Self::new(new_val);
108        tracked_swap(self, &mut ms);
109        tracked_swap(v, &mut mv);
110        use_type_invariant(&ms);
111        use_type_invariant(&mv);
112        let tracked mut msfrac = ms.frac;
113        msfrac.combine(mv.frac);
114        msfrac.update(new_val);
115        let tracked mut nv = GhostVar::<T> { frac: msfrac.split() };
116        let tracked mut ns = Self { frac: msfrac };
117        tracked_swap(self, &mut ns);
118        tracked_swap(v, &mut nv);
119    }
120}
121
122} // verus!
vstd/resource/ghost_var.rs

vstd/resource/
ghost_var.rs
