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

vstd/std_specs/
btree.rs
