vstd/cell/
invcell.rs

1#![allow(unused_imports)]
2
3use super::super::invariant::*;
4use super::super::predicate::*;
5use super::super::prelude::*;
6use super::CellId;
7use super::pcell::*;
8
9use verus as verus_;
10verus_! {
11
12/** Verus's closest analogue of [`Cell`](std::cell::Cell).
13
14An `InvCell` always allows reading and writing, even through a shared reference.
15To reason about the value in an `InvCell`, the client must specify an "invariant predicate"
16to constrain the allowed values.
17
18### Examples
19
20On construction of an `InvCell`, we can specify an invariant for the object that goes inside.
21One way to do this is by providing a `spec_fn`, which implements the [`Predicate`] trait.
22
23```rust,ignore
24fn example1() {
25    // We can create a cell with an invariant: `v == 5 || v == 13`.
26    // Thus only 5 or 13 can be stored in the cell.
27    let cell = InvCell::<u64, spec_fn(u64) -> bool>::new(5, Ghost(|v| v == 5 || v == 13));
28
29    let ref1 = &cell;
30    let ref2 = &cell;
31
32    let x = ref1.get();
33    assert(x == 5 || x == 13);
34
35    ref1.set(13);
36
37    let y = ref2.get();
38    assert(y == 5 || y == 13);
39}
40```
41
42It's often easier to implement the [`Predicate`] trait yourself. This way you can
43have a configurable predicate without needing to work with higher-order functions.
44
45```rust,ignore
46pub struct FixedParity {
47    pub parity: int,
48}
49
50impl Predicate<u64> for FixedParity {
51    open spec fn predicate(&self, v: u64) -> bool {
52        v % 2 == self.parity
53    }
54}
55
56fn example2() {
57    // Create a cell that can only store even integers
58    let cell_even = InvCell::<u64, FixedParity>::new(20, Ghost(FixedParity { parity: 0 }));
59
60    // Create a cell that can only store odd integers
61    let cell_odd = InvCell::<u64, FixedParity>::new(23, Ghost(FixedParity { parity: 1 }));
62
63    let x = cell_even.get();
64    assert(x % 2 == 0);
65
66    let y = cell_odd.get();
67    assert(y % 2 == 1);
68}
69```
70*/
71#[verifier::accept_recursive_types(T)]
72pub struct InvCell<T, Pred> {
73    pcell: PCell<T>,
74    perm_inv: Tracked<LocalInvariant<(Pred, CellId), PointsTo<T>, InvCellPred>>,
75}
76
77struct InvCellPred { }
78
79impl<T, Pred: Predicate<T>> InvariantPredicate<(Pred, CellId), PointsTo<T>> for InvCellPred {
80    closed spec fn inv(k: (Pred, CellId), perm: PointsTo<T>) -> bool {
81        let (pred, pcell_id) = k;
82        {
83            &&& pred.predicate(*perm.value())
84            &&& pcell_id === perm.id()
85        }
86    }
87}
88
89impl<T, Pred> InvCell<T, Pred> {
90    #[verifier::type_invariant]
91    closed spec fn wf(&self) -> bool {
92        &&& self.perm_inv@.constant().1 === self.pcell.id()
93    }
94
95    pub closed spec fn predicate(&self) -> Pred {
96        self.perm_inv@.constant().0
97    }
98}
99
100impl<T, Pred: Predicate<T>> InvCell<T, Pred> {
101    pub open spec fn inv(&self, val: T) -> bool {
102        self.predicate().predicate(val)
103    }
104
105    pub fn new(val: T, Ghost(pred): Ghost<Pred>) -> (cell: Self)
106        requires
107            pred.predicate(val),
108        ensures
109            cell.predicate() == pred,
110    {
111        let (pcell, Tracked(perm)) = PCell::new(val);
112        let tracked perm_inv = LocalInvariant::new((pred, pcell.id()), perm, 0);
113        InvCell { pcell, perm_inv: Tracked(perm_inv) }
114    }
115
116    pub fn set(&self, val: T)
117        requires
118            self.inv(val),
119    {
120        let _ = self.replace(val);
121    }
122
123    pub fn replace(&self, val: T) -> (old_val: T)
124        requires
125            self.inv(val),
126        ensures
127            self.inv(old_val),
128    {
129        proof {
130            use_type_invariant(self);
131        }
132        let r;
133        open_local_invariant!(self.perm_inv.borrow() => perm => {
134            r = self.pcell.replace(Tracked(&mut perm), val);
135        });
136        r
137    }
138
139    pub fn get(&self) -> (val: T)
140        where T: Copy
141        ensures
142            self.inv(val),
143    {
144        proof {
145            use_type_invariant(self);
146        }
147        let r;
148        open_local_invariant!(self.perm_inv.borrow() => perm => {
149            r = *self.pcell.borrow(Tracked(&perm));
150        });
151        r
152    }
153
154    #[allow(non_shorthand_field_patterns)]
155    pub fn into_inner(self) -> (val: T)
156        ensures
157            self.inv(val),
158    {
159        proof {
160            use_type_invariant(&self);
161        }
162        let InvCell { pcell, perm_inv: Tracked(perm_inv) } = self;
163        let tracked perm = perm_inv.into_inner();
164        pcell.into_inner(Tracked(perm))
165    }
166}
167
168}
vstd/cell/invcell.rs

vstd/cell/
invcell.rs
