vstd_extra/external/
btree.rs

1//! Additional specifications for mutable [`BTreeMap`] operations not covered by vstd.
2use alloc::{
3    alloc::Allocator,
4    collections::{BTreeMap, btree_map::CursorMut},
5};
6use core::{borrow::Borrow, cmp::Ordering, ops::Bound};
7use vstd::{
8    assert_maps_equal,
9    laws_cmp::obeys_cmp,
10    prelude::*,
11    std_specs::{
12        btree::{
13            borrowed_key_removed, contains_borrowed_key, increasing_seq, maps_borrowed_key_to_value,
14        },
15        cmp::OrdSpec,
16    },
17};
18
19verus! {
20
21/// Verus declaration for Rust's mutable B-tree cursor type.
22#[verifier::external_type_specification]
23#[verifier::external_body]
24#[verifier::reject_recursive_types(K)]
25#[verifier::reject_recursive_types(V)]
26#[verifier::reject_recursive_types(A)]
27pub struct ExCursorMut<'a, K: 'a, V: 'a, A>(CursorMut<'a, K, V, A>);
28
29/// The abstract state of a mutable B-tree cursor.
30///
31/// A cursor points at the gap immediately before `keys[position]`. Therefore `peek_next`
32/// accesses `keys[position]`, while `peek_prev` accesses `keys[position - 1]`.
33pub ghost struct CursorMutModel<Key, Value> {
34    /// All keys in the underlying map, in strictly increasing order.
35    pub keys: Seq<Key>,
36    /// The index of the element immediately after the cursor.
37    pub position: int,
38    /// The current contents of the complete map borrowed by the cursor.
39    pub map: Map<Key, Value>,
40}
41
42impl<Key, Value> CursorMutModel<Key, Value> {
43    /// Whether this model consistently represents an ordered map and a gap in that map.
44    pub open spec fn wf(self) -> bool {
45        &&& 0 <= self.position <= self.keys.len()
46        &&& self.keys.no_duplicates()
47        &&& self.keys.to_set() == self.map.dom()
48        &&& increasing_seq(self.keys)
49    }
50}
51
52/// Additional abstract and prophetic state for mutable B-tree cursors.
53pub trait CursorMutAdditionalSpecFns<Key, Value>: Sized {
54    spec fn view(&self) -> CursorMutModel<Key, Value>;
55
56    /// The contents of the borrowed map when this cursor's borrow is resolved.
57    #[verifier::prophetic]
58    spec fn final_map(self) -> Map<Key, Value>;
59}
60
61impl<'a, Key, Value, A> CursorMutAdditionalSpecFns<Key, Value> for CursorMut<'a, Key, Value, A> {
62    uninterp spec fn view(&self) -> CursorMutModel<Key, Value>;
63
64    #[verifier::prophetic]
65    uninterp spec fn final_map(self) -> Map<Key, Value>;
66}
67
68/// Whether a borrowed key type's ordering agrees with the ordering of stored keys.
69///
70/// This is the semantic requirement imposed on `Key: Borrow<Q>` by the standard library's
71/// borrowed-key `BTreeMap` operations.
72pub uninterp spec fn borrowed_key_ordering_matches<Key: Borrow<Q> + Ord, Q: Ord + ?Sized>() -> bool;
73
74/// The ordering of a stored key relative to a borrowed lookup key.
75pub uninterp spec fn borrowed_key_cmp<Key, Q: ?Sized>(stored_key: Key, key: &Q) -> Ordering;
76
77/// A key type has the same ordering as itself.
78pub broadcast axiom fn axiom_deref_key_ordering_matches<Key: Ord>()
79    ensures
80        #[trigger] borrowed_key_ordering_matches::<Key, Key>(),
81;
82
83/// Comparing a stored key against a borrowed key of the same type agrees with `Ord`'s model.
84pub broadcast axiom fn axiom_deref_key_cmp<Key: Ord>(stored_key: Key, key: &Key)
85    ensures
86        #[trigger] borrowed_key_cmp::<Key, Key>(stored_key, key) == stored_key.cmp_spec(key),
87;
88
89/// Whether a key occurs before the gap returned by `lower_bound_mut`.
90pub open spec fn before_lower_bound<Key, Q: ?Sized>(key: Key, bound: Bound<&Q>) -> bool {
91    match bound {
92        Bound::Included(bound_key) => borrowed_key_cmp(key, bound_key) is Less,
93        Bound::Excluded(bound_key) => !(borrowed_key_cmp(key, bound_key) is Greater),
94        Bound::Unbounded => false,
95    }
96}
97
98/// Whether a key occurs before the gap returned by `upper_bound_mut`.
99pub open spec fn before_upper_bound<Key, Q: ?Sized>(key: Key, bound: Bound<&Q>) -> bool {
100    match bound {
101        Bound::Included(bound_key) => !(borrowed_key_cmp(key, bound_key) is Greater),
102        Bound::Excluded(bound_key) => borrowed_key_cmp(key, bound_key) is Less,
103        Bound::Unbounded => true,
104    }
105}
106
107/// Whether a cursor is at the gap selected by `lower_bound_mut`.
108pub open spec fn positioned_at_lower_bound<Key, Value, Q: ?Sized>(
109    model: CursorMutModel<Key, Value>,
110    bound: Bound<&Q>,
111) -> bool {
112    &&& forall|i: int|
113        #![trigger before_lower_bound(model.keys[i], bound)]
114        0 <= i < model.position ==> before_lower_bound(model.keys[i], bound)
115    &&& forall|i: int|
116        #![trigger before_lower_bound(model.keys[i], bound)]
117        model.position <= i < model.keys.len() ==> !before_lower_bound(model.keys[i], bound)
118}
119
120/// Whether a cursor is at the gap selected by `upper_bound_mut`.
121pub open spec fn positioned_at_upper_bound<Key, Value, Q: ?Sized>(
122    model: CursorMutModel<Key, Value>,
123    bound: Bound<&Q>,
124) -> bool {
125    &&& forall|i: int|
126        #![trigger before_upper_bound(model.keys[i], bound)]
127        0 <= i < model.position ==> before_upper_bound(model.keys[i], bound)
128    &&& forall|i: int|
129        #![trigger before_upper_bound(model.keys[i], bound)]
130        model.position <= i < model.keys.len() ==> !before_upper_bound(model.keys[i], bound)
131}
132
133/// Once the cursor has been dropped, its prophesied map is its current map.
134pub broadcast axiom fn axiom_has_resolved_cursor<Key, Value, A>(cursor: CursorMut<Key, Value, A>)
135    ensures
136        #[trigger] has_resolved(cursor) ==> cursor.final_map() == cursor@.map,
137;
138
139/// Relates a map before and after mutating the value selected by a borrowed key.
140pub open spec fn borrowed_key_mutated<Key, Value, Q: ?Sized>(
141    old_map: Map<Key, Value>,
142    new_map: Map<Key, Value>,
143    key: &Q,
144    old_value: Value,
145    new_value: Value,
146) -> bool {
147    &&& maps_borrowed_key_to_value(old_map, key, old_value)
148    &&& maps_borrowed_key_to_value(new_map, key, new_value)
149    &&& exists|remainder: Map<Key, Value>|
150        {
151            &&& borrowed_key_removed(old_map, remainder, key)
152            &&& borrowed_key_removed(new_map, remainder, key)
153        }
154}
155
156/// Simplifies [`borrowed_key_mutated`] when the borrowed key has the map's key type.
157pub broadcast proof fn lemma_borrowed_key_mutated_deref<Key, Value>(
158    old_map: Map<Key, Value>,
159    new_map: Map<Key, Value>,
160    key: &Key,
161    old_value: Value,
162    new_value: Value,
163)
164    ensures
165        #[trigger] borrowed_key_mutated(old_map, new_map, key, old_value, new_value) <==> {
166            &&& old_map.contains_key(*key)
167            &&& old_map[*key] == old_value
168            &&& new_map == old_map.insert(*key, new_value)
169        },
170{
171    broadcast use vstd::std_specs::btree::group_btree_axioms;
172
173    if borrowed_key_mutated(old_map, new_map, key, old_value, new_value) {
174        let remainder = choose|remainder: Map<Key, Value>|
175            {
176                &&& borrowed_key_removed(old_map, remainder, key)
177                &&& borrowed_key_removed(new_map, remainder, key)
178            };
179        assert(remainder == new_map.remove(*key));
180        assert_maps_equal!(new_map, old_map.insert(*key, new_value), candidate => {
181            if candidate != *key {
182                assert(old_map.remove(*key)[candidate] == old_map[candidate]);
183            }
184        });
185    } else if old_map.contains_key(*key) && old_map[*key] == old_value && new_map == old_map.insert(
186        *key,
187        new_value,
188    ) {
189        let remainder = old_map.remove(*key);
190        assert_maps_equal!(new_map.remove(*key), remainder, candidate => {});
191        assert(borrowed_key_removed(new_map, remainder, key));
192    }
193}
194
195/// Additional axioms for mutable B-tree operations.
196pub broadcast group group_btree_extra_axioms {
197    axiom_deref_key_ordering_matches,
198    axiom_deref_key_cmp,
199    axiom_has_resolved_cursor,
200    lemma_borrowed_key_mutated_deref,
201}
202
203/// Specification for [`BTreeMap::get_mut`].
204pub assume_specification<
205    'a,
206    Key: Borrow<Q> + Ord,
207    Value,
208    A: Allocator + Clone,
209    Q: Ord + ?Sized,
210>[ BTreeMap::<Key, Value, A>::get_mut::<Q> ](
211    map: &'a mut BTreeMap<Key, Value, A>,
212    key: &Q,
213) -> (result: Option<&'a mut Value>)
214    requires
215        borrowed_key_ordering_matches::<Key, Q>(),
216    ensures
217        obeys_cmp::<Key>() ==> match result {
218            Some(value) => borrowed_key_mutated(old(map)@, final(map)@, key, *value, *final(value)),
219            None => !contains_borrowed_key(old(map)@, key) && final(map)@ == old(map)@,
220        },
221;
222
223/// Specification for [`BTreeMap::lower_bound_mut`].
224pub assume_specification<
225    'a,
226    Key: Borrow<Q> + Ord,
227    Value,
228    A: Allocator + Clone,
229    Q: Ord + ?Sized,
230>[ BTreeMap::<Key, Value, A>::lower_bound_mut::<Q> ](
231    map: &'a mut BTreeMap<Key, Value, A>,
232    bound: Bound<&Q>,
233) -> (cursor: CursorMut<'a, Key, Value, A>)
234    requires
235        borrowed_key_ordering_matches::<Key, Q>(),
236    ensures
237        obeys_cmp::<Key>() ==> {
238            &&& cursor@.wf()
239            &&& cursor@.map == old(map)@
240            &&& final(map)@ == cursor.final_map()
241            &&& positioned_at_lower_bound(cursor@, bound)
242        },
243;
244
245/// Specification for [`BTreeMap::upper_bound_mut`]. See [`BTreeMap::lower_bound_mut`].
246pub assume_specification<
247    'a,
248    Key: Borrow<Q> + Ord,
249    Value,
250    A: Allocator + Clone,
251    Q: Ord + ?Sized,
252>[ BTreeMap::<Key, Value, A>::upper_bound_mut::<Q> ](
253    map: &'a mut BTreeMap<Key, Value, A>,
254    bound: Bound<&Q>,
255) -> (cursor: CursorMut<'a, Key, Value, A>)
256    requires
257        borrowed_key_ordering_matches::<Key, Q>(),
258    ensures
259        obeys_cmp::<Key>() ==> {
260            &&& cursor@.wf()
261            &&& cursor@.map == old(map)@
262            &&& final(map)@ == cursor.final_map()
263            &&& positioned_at_upper_bound(cursor@, bound)
264        },
265;
266
267/// Specification for [`CursorMut::peek_prev`].
268pub assume_specification<'a, 'b, Key, Value, A>[ CursorMut::<'a, Key, Value, A>::peek_prev ](
269    cursor: &'b mut CursorMut<'a, Key, Value, A>,
270) -> (result: Option<(&'b Key, &'b mut Value)>)
271    requires
272        old(cursor)@.wf(),
273    ensures
274        final(cursor).final_map() == old(cursor).final_map(),
275        final(cursor)@.wf(),
276        match result {
277            Some((key, value)) => {
278                let old_model = old(cursor)@;
279                let new_model = final(cursor)@;
280                &&& old_model.position > 0
281                &&& *key == old_model.keys[old_model.position - 1]
282                &&& *value == old_model.map[*key]
283                &&& new_model.keys == old_model.keys
284                &&& new_model.position == old_model.position
285                &&& new_model.map == old_model.map.insert(*key, *final(value))
286            },
287            None => {
288                &&& old(cursor)@.position == 0
289                &&& final(cursor)@ == old(cursor)@
290            },
291        },
292;
293
294/// Specification for [`CursorMut::peek_next`].
295pub assume_specification<'a, 'b, Key, Value, A>[ CursorMut::<'a, Key, Value, A>::peek_next ](
296    cursor: &'b mut CursorMut<'a, Key, Value, A>,
297) -> (result: Option<(&'b Key, &'b mut Value)>)
298    requires
299        old(cursor)@.wf(),
300    ensures
301        final(cursor).final_map() == old(cursor).final_map(),
302        final(cursor)@.wf(),
303        match result {
304            Some((key, value)) => {
305                let old_model = old(cursor)@;
306                let new_model = final(cursor)@;
307                &&& old_model.position < old_model.keys.len()
308                &&& *key == old_model.keys[old_model.position]
309                &&& *value == old_model.map[*key]
310                &&& new_model.keys == old_model.keys
311                &&& new_model.position == old_model.position
312                &&& new_model.map == old_model.map.insert(*key, *final(value))
313            },
314            None => {
315                &&& old(cursor)@.position == old(cursor)@.keys.len()
316                &&& final(cursor)@ == old(cursor)@
317            },
318        },
319;
320
321} // verus!
vstd_extra/external/btree.rs

vstd_extra/external/
btree.rs
