vstd/std_specs/
btree.rs

1//! This code adds specifications for the standard-library types
2//! `alloc::collections::BTreeMap` and `alloc::collections::BTreeSet`.
3//!
4//! The specification is only meaningful when the `Key` obeys our [`Ord`] model,
5//! as specified by [`super::super::laws_cmp::obeys_cmp_spec`].
6//!
7//! By default, the Verus standard library brings useful axioms
8//! about the behavior of `BTreeMap` and `BTreeSet` into the ambient
9//! reasoning context by broadcasting the group
10//! `vstd::std_specs::btree::group_btree_axioms`.
11use super::super::laws_cmp::obeys_cmp;
12use super::super::prelude::*;
13use super::cmp::OrdSpec;
14use super::iter::IteratorSpec;
15
16use alloc::alloc::Allocator;
17use alloc::boxed::Box;
18use alloc::collections::btree_map;
19use alloc::collections::btree_map::{Keys, Values};
20use alloc::collections::btree_set;
21use alloc::collections::{BTreeMap, BTreeSet};
22use core::borrow::Borrow;
23use core::marker::PhantomData;
24use core::option::Option;
25
26verus! {
27
28/// Whether the `Key` type obeys the cmp spec, required for [`BTreeMap`]
29///
30/// This is a workaround to the fact that [`BTreeMap`] "late binds" the trait bounds when needed.
31/// For instance, [`BTreeMap::iter`] does not require `Key: Ord`, even though it yields ordered
32/// items. Rather, it relies on the fact that [`BTreeMap::insert`] does require `Key: Ord`, meaning
33/// no instance of a [`BTreeMap`] will ever have keys that cannot be comparable.
34///
35/// See also [`axiom_key_obeys_cmp_spec_meaning`].
36pub uninterp spec fn key_obeys_cmp_spec<Key: ?Sized>() -> bool;
37
38/// For types that are ordered, [`key_obeys_cmp_spec`] is equivalent to [`obeys_cmp`].
39pub broadcast axiom fn axiom_key_obeys_cmp_spec_meaning<K: Ord>()
40    ensures
41        #[trigger] key_obeys_cmp_spec::<K>() <==> obeys_cmp::<K>(),
42;
43
44/// Whether a sequence is ordered in increasing order.
45/// This only has meaning if `K: Ord` and [`obeys_cmp::<K>`].
46///
47/// See [`axiom_increasing_seq_meaning`] for an interpretation of this predicate.
48pub uninterp spec fn increasing_seq<K>(s: Seq<K>) -> bool;
49
50/// An interpretation for the [`increasing_seq`] predicate.
51pub broadcast axiom fn axiom_increasing_seq_meaning<K: Ord>(s: Seq<K>)
52    requires
53        obeys_cmp::<K>(),
54    ensures
55        #[trigger] increasing_seq(s) <==> forall|i, j|
56            0 <= i < j < s.len() ==> s[i].cmp_spec(&s[j]) is Less,
57;
58
59/// Specifications for the behavior of
60/// [`alloc::collections::btree_map::Keys`](https://doc.rust-lang.org/alloc/collections/btree_map/struct.Keys.html).
61#[verifier::external_type_specification]
62#[verifier::external_body]
63#[verifier::accept_recursive_types(Key)]
64#[verifier::accept_recursive_types(Value)]
65pub struct ExKeys<'a, Key, Value>(Keys<'a, Key, Value>);
66
67// To allow reasoning about the "contents" of the Keys iterator, without using
68// a prophecy, we need a function that gives us the underlying sequence of the original keys.
69pub uninterp spec fn into_iter_keys<'a, Key, Value>(i: Keys<'a, Key, Value>) -> Seq<Key>;
70
71impl<'a, K, V> super::iter::IteratorSpecImpl for Keys<'a, K, V> {
72    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
73        true
74    }
75
76    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
77
78    uninterp spec fn will_return_none(&self) -> bool;
79
80    uninterp spec fn decrease(&self) -> Option<nat>;
81
82    open spec fn peek(&self, index: int) -> Option<Self::Item> {
83        if 0 <= index < into_iter_keys(*self).len() {
84            Some(&into_iter_keys(*self)[index])
85        } else {
86            None
87        }
88    }
89}
90
91/// Specifications for the behavior of
92/// [`alloc::collections::btree_map::Values`](https://doc.rust-lang.org/alloc/collections/btree_map/struct.Values.html).
93#[verifier::external_type_specification]
94#[verifier::external_body]
95#[verifier::accept_recursive_types(Key)]
96#[verifier::accept_recursive_types(Value)]
97pub struct ExValues<'a, Key, Value>(Values<'a, Key, Value>);
98
99// To allow reasoning about the "contents" of the Values iterator, without using
100// a prophecy, we need a function that gives us the underlying sequence of the original values.
101pub uninterp spec fn into_iter_values<'a, Key, Value>(i: Values<'a, Key, Value>) -> Seq<Value>;
102
103impl<'a, K, V> super::iter::IteratorSpecImpl for Values<'a, K, V> {
104    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
105        true
106    }
107
108    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
109
110    uninterp spec fn will_return_none(&self) -> bool;
111
112    uninterp spec fn decrease(&self) -> Option<nat>;
113
114    open spec fn peek(&self, index: int) -> Option<Self::Item> {
115        if 0 <= index < into_iter_values(*self).len() {
116            Some(&into_iter_values(*self)[index])
117        } else {
118            None
119        }
120    }
121}
122
123// The `iter` method of a `BTreeMap` returns an iterator of type `btree_map::Iter`,
124// so we specify that type here.
125#[verifier::external_type_specification]
126#[verifier::external_body]
127#[verifier::accept_recursive_types(K)]
128#[verifier::accept_recursive_types(V)]
129pub struct ExMapIter<'a, K, V>(btree_map::Iter<'a, K, V>);
130
131// To allow reasoning about the "contents" of the Iter iterator, without using
132// a prophecy, we need a function that gives us the underlying sequence of the original map.
133pub uninterp spec fn into_iter<'a, Key, Value>(i: btree_map::Iter<'a, Key, Value>) -> Seq<
134    (Key, Value),
135>;
136
137impl<'a, K, V> super::iter::IteratorSpecImpl for btree_map::Iter<'a, K, V> {
138    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
139        true
140    }
141
142    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
143
144    uninterp spec fn will_return_none(&self) -> bool;
145
146    uninterp spec fn decrease(&self) -> Option<nat>;
147
148    open spec fn peek(&self, index: int) -> Option<Self::Item> {
149        if 0 <= index < into_iter(*self).len() {
150            let (k, v) = into_iter(*self)[index];
151            Some((&k, &v))
152        } else {
153            None
154        }
155    }
156}
157
158pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::iter ](
159    m: &'a BTreeMap<Key, Value, A>,
160) -> (iter: btree_map::Iter<'a, Key, Value>)
161    ensures
162        key_obeys_cmp_spec::<Key>() ==> {
163            &&& IteratorSpec::remaining(&iter).len() == m@.dom().len()
164            &&& forall|i: int|
165                #![trigger m@.contains_key(*IteratorSpec::remaining(&iter)[i].0)]
166                #![trigger m@[*IteratorSpec::remaining(&iter)[i].0]]
167                0 <= i < IteratorSpec::remaining(&iter).len() ==> m@.contains_key(
168                    *IteratorSpec::remaining(&iter)[i].0,
169                ) && m@[*IteratorSpec::remaining(&iter)[i].0] == *IteratorSpec::remaining(
170                    &iter,
171                )[i].1
172            &&& forall|k: Key| #[trigger]
173                m@.contains_key(k) ==> IteratorSpec::remaining(&iter).contains((&k, &m@[k]))
174            &&& IteratorSpec::remaining(&iter).unref().to_set() == m@.kv_pairs()
175            &&& iter.remaining().no_duplicates()
176            &&& into_iter(iter) == IteratorSpec::remaining(&iter).unref()
177            &&& IteratorSpec::decrease(&iter) is Some
178            &&& increasing_seq(iter.remaining().map_values(|kv: (&Key, &Value)| *kv.0))
179        },
180;
181
182/// Specifications for the behavior of [`alloc::collections::BTreeMap`](https://doc.rust-lang.org/alloc/collections/struct.BTreeMap.html).
183///
184/// We model a `BTreeMap` as having a view of type `Map<Key, Value>`, which reflects the current state of the map.
185///
186/// These specifications are only meaningful if `key_obeys_cmp_spec::<Key>()` holds.
187/// See [`key_obeys_cmp_spec`] for information on use with primitive types and other types.
188///
189/// Axioms about the behavior of BTreeMap are present in the broadcast group `vstd::std_specs::btree::group_btree_axioms`.
190#[verifier::external_type_specification]
191#[verifier::external_body]
192#[verifier::accept_recursive_types(Key)]
193#[verifier::accept_recursive_types(Value)]
194#[verifier::reject_recursive_types(A)]
195pub struct ExBTreeMap<Key, Value, A: Allocator + Clone>(BTreeMap<Key, Value, A>);
196
197pub trait BTreeMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
198    spec fn spec_index(&self, k: Key) -> Value
199        recommends
200            self@.contains_key(k),
201    ;
202}
203
204impl<Key, Value, A: Allocator + Clone> BTreeMapAdditionalSpecFns<Key, Value> for BTreeMap<
205    Key,
206    Value,
207    A,
208> {
209    #[verifier::inline]
210    open spec fn spec_index(&self, k: Key) -> Value {
211        self@.index(k)
212    }
213}
214
215impl<Key, Value, A: Allocator + Clone> View for BTreeMap<Key, Value, A> {
216    type V = Map<Key, Value>;
217
218    uninterp spec fn view(&self) -> Map<Key, Value>;
219}
220
221impl<Key: DeepView, Value: DeepView, A: Allocator + Clone> DeepView for BTreeMap<Key, Value, A> {
222    type V = Map<Key::V, Value::V>;
223
224    open spec fn deep_view(&self) -> Map<Key::V, Value::V> {
225        btree_map_deep_view_impl(*self)
226    }
227}
228
229/// The actual definition of `BTreeMap::deep_view`.
230///
231/// This is a separate function since it introduces a lot of quantifiers and revealing an opaque trait
232/// method is not supported. In most cases, it's easier to use one of the lemmas below instead
233/// of revealing this function directly.
234#[verifier::opaque]
235pub open spec fn btree_map_deep_view_impl<Key: DeepView, Value: DeepView, A: Allocator + Clone>(
236    m: BTreeMap<Key, Value, A>,
237) -> Map<Key::V, Value::V> {
238    Map::new(
239        m@.dom().map(|k: Key| k.deep_view()),
240        |dk: Key::V|
241            {
242                let k = choose|k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
243                m@[k].deep_view()
244            },
245    )
246}
247
248pub broadcast proof fn lemma_btree_map_deepview_dom<K: DeepView, V: DeepView>(m: BTreeMap<K, V>)
249    ensures
250        #[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),
251{
252    reveal(btree_map_deep_view_impl);
253    broadcast use group_btree_axioms;
254    broadcast use crate::vstd::group_vstd_default;
255
256    assert(m.deep_view().dom() =~= m@.dom().map(|k: K| k.deep_view()));
257}
258
259pub broadcast proof fn lemma_btree_map_deepview_properties<K: DeepView, V: DeepView>(
260    m: BTreeMap<K, V>,
261)
262    requires
263        crate::relations::injective(|k: K| k.deep_view()),
264    ensures
265        #![trigger m.deep_view()]
266        // all elements in m.view() are present in m.deep_view()
267        forall|k: K| #[trigger]
268            m@.contains_key(k) ==> m.deep_view().contains_key(k.deep_view())
269                && m.deep_view()[k.deep_view()] == m@[k].deep_view(),
270        // all elements in m.deep_view() are present in m.view()
271        forall|dk: <K as DeepView>::V| #[trigger]
272            m.deep_view().contains_key(dk) ==> exists|k: K|
273                k.deep_view() == dk && #[trigger] m@.contains_key(k),
274{
275    reveal(btree_map_deep_view_impl);
276    broadcast use group_btree_axioms;
277    broadcast use crate::vstd::group_vstd_default;
278
279    assert(m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()));
280    assert forall|k: K| #[trigger] m@.contains_key(k) implies m.deep_view().contains_key(
281        k.deep_view(),
282    ) && m.deep_view()[k.deep_view()] == m@[k].deep_view() by {
283        assert forall|k1: K, k2: K| #[trigger]
284            k1.deep_view() == #[trigger] k2.deep_view() implies k1 == k2 by {
285            let ghost k_deepview = |k: K| k.deep_view();
286            assert(crate::relations::injective(k_deepview));
287            assert(k_deepview(k1) == k_deepview(k2));
288        }
289    }
290}
291
292pub broadcast proof fn lemma_btree_map_deepview_values<K: DeepView, V: DeepView>(m: BTreeMap<K, V>)
293    requires
294        crate::relations::injective(|k: K| k.deep_view()),
295    ensures
296        #[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),
297{
298    reveal(btree_map_deep_view_impl);
299    broadcast use group_btree_axioms;
300    broadcast use lemma_btree_map_deepview_properties;
301    broadcast use crate::vstd::group_vstd_default;
302
303    let lhs = m.deep_view().values();
304    let rhs = m@.values().map(|v: V| v.deep_view());
305    assert forall|v: V::V| #[trigger] lhs.contains(v) implies rhs.contains(v) by {
306        let dk = choose|dk: K::V| #[trigger]
307            m.deep_view().contains_key(dk) && m.deep_view()[dk] == v;
308        let k = choose|k: K| #[trigger] m@.contains_key(k) && k.deep_view() == dk;
309        let ov = choose|ov: V| #[trigger] m@.contains_key(k) && m@[k] == ov && ov.deep_view() == v;
310        assert(v == ov.deep_view());
311        assert(m@.values().contains(ov));
312    }
313}
314
315/// Borrowing a key works the same way on deep_view as on view,
316/// if deep_view is injective; see `axiom_contains_deref_key`.
317pub broadcast axiom fn axiom_btree_map_deepview_borrow<
318    K: DeepView + Borrow<Q>,
319    V: DeepView,
320    Q: View<V = <K as DeepView>::V> + Eq + ?Sized,
321>(m: BTreeMap<K, V>, k: &Q)
322    requires
323        key_obeys_cmp_spec::<K>(),
324        crate::relations::injective(|k: K| k.deep_view()),
325    ensures
326        #[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),
327;
328
329pub uninterp spec fn spec_btree_map_len<Key, Value, A: Allocator + Clone>(
330    m: &BTreeMap<Key, Value, A>,
331) -> usize;
332
333pub broadcast axiom fn axiom_spec_btree_map_len<Key, Value, A: Allocator + Clone>(
334    m: &BTreeMap<Key, Value, A>,
335)
336    ensures
337        key_obeys_cmp_spec::<Key>() ==> #[trigger] spec_btree_map_len(m) == m@.len(),
338;
339
340#[verifier::when_used_as_spec(spec_btree_map_len)]
341pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::len ](
342    m: &BTreeMap<Key, Value, A>,
343) -> (len: usize)
344    ensures
345        len == spec_btree_map_len(m),
346;
347
348pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::is_empty ](
349    m: &BTreeMap<Key, Value, A>,
350) -> (res: bool)
351    ensures
352        res == m@.is_empty(),
353;
354
355pub assume_specification<K: Clone, V: Clone, A: Allocator + Clone>[ <BTreeMap::<
356    K,
357    V,
358    A,
359> as Clone>::clone ](this: &BTreeMap<K, V, A>) -> (other: BTreeMap<K, V, A>)
360    ensures
361        other@ == this@,
362;
363
364pub assume_specification<Key, Value>[ BTreeMap::<Key, Value>::new ]() -> (m: BTreeMap<Key, Value>)
365    ensures
366        m@ == Map::<Key, Value>::empty(),
367;
368
369pub assume_specification<K, V>[ <BTreeMap<K, V> as core::default::Default>::default ]() -> (m:
370    BTreeMap<K, V>)
371    ensures
372        m@ == Map::<K, V>::empty(),
373;
374
375pub assume_specification<Key: Ord, Value, A: Allocator + Clone>[ BTreeMap::<
376    Key,
377    Value,
378    A,
379>::insert ](m: &mut BTreeMap<Key, Value, A>, k: Key, v: Value) -> (result: Option<Value>)
380    ensures
381        obeys_cmp::<Key>() ==> {
382            &&& final(m)@ == old(m)@.insert(k, v)
383            &&& match result {
384                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
385                None => !old(m)@.contains_key(k),
386            }
387        },
388;
389
390// The specification for `contains_key` has a parameter `key: &Q`
391// where you'd expect to find `key: &Key`. This allows for the case
392// that `Key` can be borrowed as something other than `&Key`. For
393// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
394// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
395// respectively.
396// To deal with this, we have a specification function that opaquely
397// specifies what it means for a map to contain a borrowed key of type
398// `&Q`. And the postcondition of `contains_key` just says that its
399// result matches the output of that specification function. But this
400// isn't very helpful by itself, since there's no body to that
401// specification function. So we have special-case axioms that say
402// what this means in two important circumstances: (1) `Key = Q` and
403// (2) `Key = Box<Q>`.
404pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
405    m: Map<Key, Value>,
406    k: &Q,
407) -> bool;
408
409pub broadcast axiom fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
410    ensures
411        #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
412;
413
414pub broadcast axiom fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
415    ensures
416        #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
417            Box::new(*k),
418        ),
419;
420
421pub assume_specification<
422    Key: Borrow<Q> + Ord,
423    Value,
424    A: Allocator + Clone,
425    Q: Ord + ?Sized,
426>[ BTreeMap::<Key, Value, A>::contains_key::<Q> ](m: &BTreeMap<Key, Value, A>, k: &Q) -> (result:
427    bool)
428    ensures
429        obeys_cmp::<Key>() ==> result == contains_borrowed_key(m@, k),
430;
431
432// The specification for `get` has a parameter `key: &Q` where you'd
433// expect to find `key: &Key`. This allows for the case that `Key` can
434// be borrowed as something other than `&Key`. For instance,
435// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
436// as `&str`, so in those cases `Q` would be `u32` and `str`
437// respectively.
438// To deal with this, we have a specification function that opaquely
439// specifies what it means for a map to map a borrowed key of type
440// `&Q` to a certain value. And the postcondition of `get` says that
441// its result matches the output of that specification function. (It
442// also says that its result corresponds to the output of
443// `contains_borrowed_key`, discussed above.) But this isn't very
444// helpful by itself, since there's no body to that specification
445// function. So we have special-case axioms that say what this means
446// in two important circumstances: (1) `Key = Q` and (2) `Key =
447// Box<Q>`.
448pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
449    m: Map<Key, Value>,
450    k: &Q,
451    v: Value,
452) -> bool;
453
454pub broadcast axiom fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
455    ensures
456        #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
457            && m[*k] == v,
458;
459
460pub broadcast axiom fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
461    ensures
462        #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
463            let k = Box::new(*q);
464            &&& m.contains_key(k)
465            &&& m[k] == v
466        },
467;
468
469pub assume_specification<
470    'a,
471    Key: Borrow<Q> + Ord,
472    Value,
473    A: Allocator + Clone,
474    Q: Ord + ?Sized,
475>[ BTreeMap::<Key, Value, A>::get::<Q> ](m: &'a BTreeMap<Key, Value, A>, k: &Q) -> (result: Option<
476    &'a Value,
477>)
478    ensures
479        obeys_cmp::<Key>() ==> match result {
480            Some(v) => maps_borrowed_key_to_value(m@, k, *v),
481            None => !contains_borrowed_key(m@, k),
482        },
483;
484
485// The specification for `remove` has a parameter `key: &Q` where
486// you'd expect to find `key: &Key`. This allows for the case that
487// `Key` can be borrowed as something other than `&Key`. For instance,
488// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
489// as `&str`, so in those cases `Q` would be `u32` and `str`
490// respectively. To deal with this, we have a specification function
491// that opaquely specifies what it means for two maps to be related by
492// a remove of a certain `&Q`. And the postcondition of `remove` says
493// that `old(self)@` and `self@` satisfy that relationship. (It also
494// says that its result corresponds to the output of
495// `contains_borrowed_key` and `maps_borrowed_key_to_value`, discussed
496// above.) But this isn't very helpful by itself, since there's no
497// body to that specification function. So we have special-case axioms
498// that say what this means in two important circumstances: (1) `Key =
499// Q` and (2) `Key = Box<Q>`.
500pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
501    old_m: Map<Key, Value>,
502    new_m: Map<Key, Value>,
503    k: &Q,
504) -> bool;
505
506pub broadcast axiom fn axiom_deref_key_removed<Q, Value>(
507    old_m: Map<Q, Value>,
508    new_m: Map<Q, Value>,
509    k: &Q,
510)
511    ensures
512        #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
513            *k,
514        ),
515;
516
517pub broadcast axiom fn axiom_box_key_removed<Q, Value>(
518    old_m: Map<Box<Q>, Value>,
519    new_m: Map<Box<Q>, Value>,
520    q: &Q,
521)
522    ensures
523        #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
524            == old_m.remove(Box::new(*q)),
525;
526
527pub assume_specification<
528    Key: Borrow<Q> + Ord,
529    Value,
530    A: Allocator + Clone,
531    Q: Ord + ?Sized,
532>[ BTreeMap::<Key, Value, A>::remove::<Q> ](m: &mut BTreeMap<Key, Value, A>, k: &Q) -> (result:
533    Option<Value>)
534    ensures
535        obeys_cmp::<Key>() ==> {
536            &&& borrowed_key_removed(old(m)@, final(m)@, k)
537            &&& match result {
538                Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
539                None => !contains_borrowed_key(old(m)@, k),
540            }
541        },
542;
543
544pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::clear ](
545    m: &mut BTreeMap<Key, Value, A>,
546)
547    ensures
548        final(m)@ == Map::<Key, Value>::empty(),
549;
550
551pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::keys ](
552    m: &'a BTreeMap<Key, Value, A>,
553) -> (keys: Keys<'a, Key, Value>)
554    ensures
555        key_obeys_cmp_spec::<Key>() ==> {
556            &&& IteratorSpec::remaining(&keys).unref().to_set() == m@.dom()
557            &&& IteratorSpec::remaining(&keys).no_duplicates()
558            &&& IteratorSpec::remaining(&keys).len() == m@.dom().len()
559            &&& increasing_seq(IteratorSpec::remaining(&keys))
560            &&& into_iter_keys(keys) == IteratorSpec::remaining(&keys).unref()
561            &&& IteratorSpec::decrease(&keys) is Some
562        },
563;
564
565pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::values ](
566    m: &'a BTreeMap<Key, Value, A>,
567) -> (values: Values<'a, Key, Value>)
568    ensures
569        key_obeys_cmp_spec::<Key>() ==> {
570            &&& IteratorSpec::remaining(&values).unref().to_set() == m@.values()
571            &&& IteratorSpec::remaining(&values).len() == m@.dom().len()
572            &&& into_iter_values(values) == IteratorSpec::remaining(&values).unref()
573            &&& IteratorSpec::decrease(&values) is Some
574            &&& exists|key_seq: Seq<Key>|
575                {
576                    &&& increasing_seq(key_seq)
577                    &&& key_seq.to_set() == m@.dom()
578                    &&& key_seq.no_duplicates()
579                    &&& IteratorSpec::remaining(&values) == key_seq.map(|i: int, k| &m@[k])
580                }
581        },
582;
583
584pub broadcast axiom fn axiom_btree_map_decreases<Key, Value, A: Allocator + Clone>(
585    m: BTreeMap<Key, Value, A>,
586)
587    ensures
588        #[trigger] (decreases_to!(m => m@)),
589;
590
591// The `iter` method of a `BTreeSet` returns an iterator of type `btree_set::Iter`,
592// so we specify that type here.
593#[verifier::external_type_specification]
594#[verifier::external_body]
595#[verifier::accept_recursive_types(K)]
596pub struct ExSetIter<'a, K: 'a>(btree_set::Iter<'a, K>);
597
598// To allow reasoning about the "contents" of the BtreeSet iterator, without using
599// a prophecy, we need a function that gives us the underlying sequence of the original keys.
600pub uninterp spec fn into_iter_btree_keys<'a, Key>(i: btree_set::Iter::<'a, Key>) -> Seq<Key>;
601
602impl<'a, T> super::iter::IteratorSpecImpl for btree_set::Iter::<'a, T> {
603    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
604        true
605    }
606
607    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
608
609    uninterp spec fn will_return_none(&self) -> bool;
610
611    uninterp spec fn decrease(&self) -> Option<nat>;
612
613    open spec fn peek(&self, index: int) -> Option<Self::Item> {
614        if 0 <= index < into_iter_btree_keys(*self).len() {
615            Some(&into_iter_btree_keys(*self)[index])
616        } else {
617            None
618        }
619    }
620}
621
622/// Specifications for the behavior of [`alloc::collections::BTreeSet`](https://doc.rust-lang.org/alloc/collections/struct.BTreeSet.html).
623///
624/// We model a `BTreeSet` as having a view of type `Set<Key>`, which reflects the current state of the set.
625///
626/// These specifications are only meaningful if `obeys_cmp::<Key>()` hold.
627/// See [`obeys_cmp`] for information on use with primitive types and custom types.
628///
629/// Axioms about the behavior of BTreeSet are present in the broadcast group `vstd::std_specs::btree::group_btree_axioms`.
630#[verifier::external_type_specification]
631#[verifier::external_body]
632#[verifier::accept_recursive_types(Key)]
633#[verifier::reject_recursive_types(A)]
634pub struct ExBTreeSet<Key, A: Allocator + Clone>(BTreeSet<Key, A>);
635
636impl<Key, A: Allocator + Clone> View for BTreeSet<Key, A> {
637    type V = Set<Key>;
638
639    uninterp spec fn view(&self) -> Set<Key>;
640}
641
642impl<Key: DeepView, A: Allocator + Clone> DeepView for BTreeSet<Key, A> {
643    type V = Set<Key::V>;
644
645    open spec fn deep_view(&self) -> Set<Key::V> {
646        self@.map(|x: Key| x.deep_view())
647    }
648}
649
650pub uninterp spec fn spec_btree_set_len<Key, A: Allocator + Clone>(m: &BTreeSet<Key, A>) -> usize;
651
652pub broadcast axiom fn axiom_spec_btree_set_len<Key, A: Allocator + Clone>(m: &BTreeSet<Key, A>)
653    ensures
654        key_obeys_cmp_spec::<Key>() ==> #[trigger] spec_btree_set_len(m) == m@.len(),
655;
656
657#[verifier::when_used_as_spec(spec_btree_set_len)]
658pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::len ](
659    m: &BTreeSet<Key, A>,
660) -> (len: usize)
661    ensures
662        len == spec_btree_set_len(m),
663;
664
665pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::is_empty ](
666    m: &BTreeSet<Key, A>,
667) -> (res: bool)
668    ensures
669        res == m@.is_empty(),
670;
671
672pub assume_specification<K: Clone, A: Allocator + Clone>[ <BTreeSet::<K, A> as Clone>::clone ](
673    this: &BTreeSet<K, A>,
674) -> (other: BTreeSet<K, A>)
675    ensures
676        other@ == this@,
677;
678
679pub assume_specification<Key>[ BTreeSet::<Key>::new ]() -> (m: BTreeSet<Key>)
680    ensures
681        m@ == Set::<Key>::empty(),
682;
683
684pub assume_specification<T>[ <BTreeSet<T> as core::default::Default>::default ]() -> (m: BTreeSet<
685    T,
686>)
687    ensures
688        m@ == Set::<T>::empty(),
689;
690
691pub assume_specification<Key: Ord, A: Allocator + Clone>[ BTreeSet::<Key, A>::insert ](
692    m: &mut BTreeSet<Key, A>,
693    k: Key,
694) -> (result: bool)
695    ensures
696        obeys_cmp::<Key>() ==> {
697            &&& final(m)@ == old(m)@.insert(k)
698            &&& result == !old(m)@.contains(k)
699        },
700;
701
702// The specification for `contains` has a parameter `key: &Q`
703// where you'd expect to find `key: &Key`. This allows for the case
704// that `Key` can be borrowed as something other than `&Key`. For
705// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
706// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
707// respectively.
708// To deal with this, we have a specification function that opaquely
709// specifies what it means for a set to contain a borrowed key of type
710// `&Q`. And the postcondition of `contains` just says that its
711// result matches the output of that specification function. But this
712// isn't very helpful by itself, since there's no body to that
713// specification function. So we have special-case axioms that say
714// what this means in two important circumstances: (1) `Key = Q` and
715// (2) `Key = Box<Q>`.
716pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
717
718pub broadcast axiom fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
719    ensures
720        #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
721;
722
723pub broadcast axiom fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
724    ensures
725        #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
726;
727
728pub assume_specification<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>[ BTreeSet::<
729    Key,
730    A,
731>::contains ](m: &BTreeSet<Key, A>, k: &Q) -> (result: bool)
732    ensures
733        obeys_cmp::<Key>() ==> result == set_contains_borrowed_key(m@, k),
734    no_unwind
735;
736
737// The specification for `get` has a parameter `key: &Q` where you'd
738// expect to find `key: &Key`. This allows for the case that `Key` can
739// be borrowed as something other than `&Key`. For instance,
740// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
741// as `&str`, so in those cases `Q` would be `u32` and `str`
742// respectively.
743// To deal with this, we have a specification function that opaquely
744// specifies what it means for a returned reference to point to an
745// element of a BTreeSet. And the postcondition of `get` says that
746// its result matches the output of that specification function. (It
747// also says that its result corresponds to the output of
748// `contains_borrowed_key`, discussed above.) But this isn't very
749// helpful by itself, since there's no body to that specification
750// function. So we have special-case axioms that say what this means
751// in two important circumstances: (1) `Key = Q` and (2) `Key =
752// Box<Q>`.
753pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
754
755pub broadcast axiom fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
756    ensures
757        #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
758;
759
760pub broadcast axiom fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
761    ensures
762        #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
763            *q,
764        ) == v),
765;
766
767pub assume_specification<
768    'a,
769    Key: Borrow<Q> + Ord,
770    A: Allocator + Clone,
771    Q: Ord + ?Sized,
772>[ BTreeSet::<Key, A>::get::<Q> ](m: &'a BTreeSet<Key, A>, k: &Q) -> (result: Option<&'a Key>)
773    ensures
774        obeys_cmp::<Key>() ==> match result {
775            Some(v) => sets_borrowed_key_to_key(m@, k, v),
776            None => !set_contains_borrowed_key(m@, k),
777        },
778;
779
780// The specification for `remove` has a parameter `key: &Q` where
781// you'd expect to find `key: &Key`. This allows for the case that
782// `Key` can be borrowed as something other than `&Key`. For instance,
783// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
784// as `&str`, so in those cases `Q` would be `u32` and `str`
785// respectively. To deal with this, we have a specification function
786// that opaquely specifies what it means for two sets to be related by
787// a remove of a certain `&Q`. And the postcondition of `remove` says
788// that `old(self)@` and `self@` satisfy that relationship. (It also
789// says that its result corresponds to the output of
790// `set_contains_borrowed_key`, discussed above.) But this isn't very
791// helpful by itself, since there's no body to that specification
792// function. So we have special-case axioms that say what this means
793// in two important circumstances: (1) `Key = Q` and (2) `Key = Box<Q>`.
794pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
795    old_m: Set<Key>,
796    new_m: Set<Key>,
797    k: &Q,
798) -> bool;
799
800pub broadcast axiom fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
801    ensures
802        #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
803            *k,
804        ),
805;
806
807pub broadcast axiom fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
808    ensures
809        #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
810            == old_m.remove(Box::new(*q)),
811;
812
813pub assume_specification<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>[ BTreeSet::<
814    Key,
815    A,
816>::remove::<Q> ](m: &mut BTreeSet<Key, A>, k: &Q) -> (result: bool)
817    ensures
818        obeys_cmp::<Key>() ==> {
819            &&& sets_differ_by_borrowed_key(old(m)@, final(m)@, k)
820            &&& result == set_contains_borrowed_key(old(m)@, k)
821        },
822;
823
824pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::clear ](
825    m: &mut BTreeSet<Key, A>,
826) where A: Clone
827    ensures
828        final(m)@ == Set::<Key>::empty(),
829;
830
831pub assume_specification<'a, Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::iter ](
832    m: &'a BTreeSet<Key, A>,
833) -> (r: btree_set::Iter<'a, Key>)
834    ensures
835        key_obeys_cmp_spec::<Key>() ==> {
836            &&& IteratorSpec::remaining(&r).unref().to_set() == m@
837            &&& IteratorSpec::remaining(&r).no_duplicates()
838            &&& IteratorSpec::remaining(&r).len() == m@.len()
839            &&& increasing_seq(IteratorSpec::remaining(&r))
840            &&& into_iter_btree_keys(r) == IteratorSpec::remaining(&r).unref()
841            &&& IteratorSpec::decrease(&r) is Some
842        },
843;
844
845pub broadcast axiom fn axiom_btree_set_decreases<Key, A: Allocator + Clone>(m: BTreeSet<Key, A>)
846    ensures
847        #[trigger] (decreases_to!(m => m@)),
848;
849
850pub broadcast group group_btree_axioms {
851    axiom_key_obeys_cmp_spec_meaning,
852    axiom_increasing_seq_meaning,
853    axiom_box_key_removed,
854    axiom_contains_deref_key,
855    axiom_contains_box,
856    axiom_deref_key_removed,
857    axiom_maps_deref_key_to_value,
858    axiom_maps_box_key_to_value,
859    axiom_btree_map_deepview_borrow,
860    axiom_spec_btree_map_len,
861    axiom_set_box_key_removed,
862    axiom_set_contains_deref_key,
863    axiom_set_contains_box,
864    axiom_set_deref_key_removed,
865    axiom_set_deref_key_to_value,
866    axiom_set_box_key_to_value,
867    axiom_spec_btree_set_len,
868    axiom_btree_map_decreases,
869    axiom_btree_set_decreases,
870}
871
872} // verus!
vstd/std_specs/btree.rs

vstd/std_specs/
btree.rs
