vstd/std_specs/
btree.rs

1//! This code adds specifications for the standard-library types
2//! `std::collections::BTreeMap` and `std::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_spec;
12use super::super::prelude::*;
13use super::cmp::OrdSpec;
14
15use alloc::alloc::Allocator;
16use core::borrow::Borrow;
17use core::marker::PhantomData;
18use core::option::Option;
19use std::collections::btree_map;
20use std::collections::btree_map::{Keys, Values};
21use std::collections::btree_set;
22use std::collections::{BTreeMap, BTreeSet};
23
24verus! {
25
26/// Whether the `Key` type obeys the cmp spec, required for [`BTreeMap`]
27///
28/// This is a workaround to the fact that [`BTreeMap`] "late binds" the trait bounds when needed.
29/// For instance, [`BTreeMap::iter`] does not require `Key: Ord`, even though it yields ordered
30/// items. Rather, it relies on the fact that [`BTreeMap::insert`] does require `Key: Ord`, meaning
31/// no instance of a [`BTreeMap`] will ever have keys that cannot be comparable.
32///
33/// See also [`axiom_key_obeys_cmp_spec_meaning`].
34pub uninterp spec fn key_obeys_cmp_spec<Key: ?Sized>() -> bool;
35
36/// For types that are ordered, [`key_obeys_cmp_spec`] is equivalent to [`obeys_cmp_spec`].
37pub broadcast axiom fn axiom_key_obeys_cmp_spec_meaning<K: Ord>()
38    ensures
39        #[trigger] key_obeys_cmp_spec::<K>() <==> obeys_cmp_spec::<K>(),
40;
41
42/// Whether a sequence is ordered in increasing order.
43/// This only has meaning if `K: Ord` and [`obeys_cmp_spec::<K>`].
44///
45/// See [`axiom_increasing_seq_meaning`] for an interpretation of this predicate.
46pub uninterp spec fn increasing_seq<K>(s: Seq<K>) -> bool;
47
48/// An interpretation for the [`increasing_seq`] predicate.
49pub broadcast axiom fn axiom_increasing_seq_meaning<K: Ord>(s: Seq<K>)
50    requires
51        obeys_cmp_spec::<K>(),
52    ensures
53        #[trigger] increasing_seq(s) <==> forall|i, j|
54            0 <= i < j < s.len() ==> s[i].cmp_spec(&s[j]) is Less,
55;
56
57/// Specifications for the behavior of
58/// [`std::collections::btree_map::Keys`](https://doc.rust-lang.org/std/collections/btree_map/struct.Keys.html).
59#[verifier::external_type_specification]
60#[verifier::external_body]
61#[verifier::accept_recursive_types(Key)]
62#[verifier::accept_recursive_types(Value)]
63pub struct ExKeys<'a, Key, Value>(Keys<'a, Key, Value>);
64
65impl<'a, Key, Value> View for Keys<'a, Key, Value> {
66    type V = (int, Seq<Key>);
67
68    uninterp spec fn view(self: &Keys<'a, Key, Value>) -> (int, Seq<Key>);
69}
70
71pub assume_specification<'a, Key, Value>[ Keys::<'a, Key, Value>::next ](
72    keys: &mut Keys<'a, Key, Value>,
73) -> (r: Option<&'a Key>)
74    ensures
75        ({
76            let (old_index, old_seq) = old(keys)@;
77            match r {
78                None => {
79                    &&& keys@ == old(keys)@
80                    &&& old_index >= old_seq.len()
81                },
82                Some(k) => {
83                    let (new_index, new_seq) = keys@;
84                    &&& 0 <= old_index < old_seq.len()
85                    &&& new_seq == old_seq
86                    &&& new_index == old_index + 1
87                    &&& k == old_seq[old_index]
88                },
89            }
90        }),
91;
92
93pub struct KeysGhostIterator<'a, Key, Value> {
94    pub pos: int,
95    pub keys: Seq<Key>,
96    pub phantom: Option<&'a Value>,
97}
98
99impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Keys<'a, Key, Value> {
100    type GhostIter = KeysGhostIterator<'a, Key, Value>;
101
102    open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value> {
103        KeysGhostIterator { pos: self@.0, keys: self@.1, phantom: None }
104    }
105}
106
107impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for KeysGhostIterator<
108    'a,
109    Key,
110    Value,
111> {
112    type ExecIter = Keys<'a, Key, Value>;
113
114    type Item = Key;
115
116    type Decrease = int;
117
118    open spec fn exec_invariant(&self, exec_iter: &Keys<'a, Key, Value>) -> bool {
119        &&& self.pos == exec_iter@.0
120        &&& self.keys == exec_iter@.1
121    }
122
123    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
124        init matches Some(init) ==> {
125            &&& init.pos == 0
126            &&& init.keys == self.keys
127            &&& 0 <= self.pos <= self.keys.len()
128        }
129    }
130
131    open spec fn ghost_ensures(&self) -> bool {
132        self.pos == self.keys.len()
133    }
134
135    open spec fn ghost_decrease(&self) -> Option<int> {
136        Some(self.keys.len() - self.pos)
137    }
138
139    open spec fn ghost_peek_next(&self) -> Option<Key> {
140        if 0 <= self.pos < self.keys.len() {
141            Some(self.keys[self.pos])
142        } else {
143            None
144        }
145    }
146
147    open spec fn ghost_advance(&self, _exec_iter: &Keys<'a, Key, Value>) -> KeysGhostIterator<
148        'a,
149        Key,
150        Value,
151    > {
152        Self { pos: self.pos + 1, ..*self }
153    }
154}
155
156impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value> {
157    type V = Seq<Key>;
158
159    open spec fn view(&self) -> Seq<Key> {
160        self.keys.take(self.pos)
161    }
162}
163
164/// Specifications for the behavior of
165/// [`std::collections::btree_map::Values`](https://doc.rust-lang.org/std/collections/btree_map/struct.Values.html).
166#[verifier::external_type_specification]
167#[verifier::external_body]
168#[verifier::accept_recursive_types(Key)]
169#[verifier::accept_recursive_types(Value)]
170pub struct ExValues<'a, Key, Value>(Values<'a, Key, Value>);
171
172impl<'a, Key, Value> View for Values<'a, Key, Value> {
173    type V = (int, Seq<Value>);
174
175    uninterp spec fn view(self: &Values<'a, Key, Value>) -> (int, Seq<Value>);
176}
177
178pub assume_specification<'a, Key, Value>[ Values::<'a, Key, Value>::next ](
179    values: &mut Values<'a, Key, Value>,
180) -> (r: Option<&'a Value>)
181    ensures
182        ({
183            let (old_index, old_seq) = old(values)@;
184            match r {
185                None => {
186                    &&& values@ == old(values)@
187                    &&& old_index >= old_seq.len()
188                },
189                Some(v) => {
190                    let (new_index, new_seq) = values@;
191                    &&& 0 <= old_index < old_seq.len()
192                    &&& new_seq == old_seq
193                    &&& new_index == old_index + 1
194                    &&& v == old_seq[old_index]
195                },
196            }
197        }),
198;
199
200pub struct ValuesGhostIterator<'a, Key, Value> {
201    pub pos: int,
202    pub values: Seq<Value>,
203    pub phantom: Option<&'a Key>,
204}
205
206impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Values<'a, Key, Value> {
207    type GhostIter = ValuesGhostIterator<'a, Key, Value>;
208
209    open spec fn ghost_iter(&self) -> ValuesGhostIterator<'a, Key, Value> {
210        ValuesGhostIterator { pos: self@.0, values: self@.1, phantom: None }
211    }
212}
213
214impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for ValuesGhostIterator<
215    'a,
216    Key,
217    Value,
218> {
219    type ExecIter = Values<'a, Key, Value>;
220
221    type Item = Value;
222
223    type Decrease = int;
224
225    open spec fn exec_invariant(&self, exec_iter: &Values<'a, Key, Value>) -> bool {
226        &&& self.pos == exec_iter@.0
227        &&& self.values == exec_iter@.1
228    }
229
230    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
231        init matches Some(init) ==> {
232            &&& init.pos == 0
233            &&& init.values == self.values
234            &&& 0 <= self.pos <= self.values.len()
235        }
236    }
237
238    open spec fn ghost_ensures(&self) -> bool {
239        self.pos == self.values.len()
240    }
241
242    open spec fn ghost_decrease(&self) -> Option<int> {
243        Some(self.values.len() - self.pos)
244    }
245
246    open spec fn ghost_peek_next(&self) -> Option<Value> {
247        if 0 <= self.pos < self.values.len() {
248            Some(self.values[self.pos])
249        } else {
250            None
251        }
252    }
253
254    open spec fn ghost_advance(&self, _exec_iter: &Values<'a, Key, Value>) -> ValuesGhostIterator<
255        'a,
256        Key,
257        Value,
258    > {
259        Self { pos: self.pos + 1, ..*self }
260    }
261}
262
263impl<'a, Key, Value> View for ValuesGhostIterator<'a, Key, Value> {
264    type V = Seq<Value>;
265
266    open spec fn view(&self) -> Seq<Value> {
267        self.values.take(self.pos)
268    }
269}
270
271// The `iter` method of a `BTreeMap` returns an iterator of type `btree_map::Iter`,
272// so we specify that type here.
273#[verifier::external_type_specification]
274#[verifier::external_body]
275#[verifier::accept_recursive_types(K)]
276#[verifier::accept_recursive_types(V)]
277pub struct ExMapIter<'a, K, V>(btree_map::Iter<'a, K, V>);
278
279pub trait MapIterAdditionalSpecFns<'a, Key, Value> {
280    spec fn view(self: &Self) -> (int, Seq<(Key, Value)>);
281}
282
283impl<'a, K: 'a, V: 'a> View for btree_map::Iter<'a, K, V> {
284    type V = (int, Seq<(K, V)>);
285
286    uninterp spec fn view(self: &btree_map::Iter<'a, K, V>) -> (int, Seq<(K, V)>);
287}
288
289pub assume_specification<'a, K: 'a, V: 'a>[ btree_map::Iter::<'a, K, V>::next ](
290    iter: &mut btree_map::Iter<'a, K, V>,
291) -> (r: Option<(&'a K, &'a V)>)
292    ensures
293        ({
294            let (old_index, old_seq) = old(iter)@;
295            match r {
296                None => {
297                    &&& iter@ == old(iter)@
298                    &&& old_index >= old_seq.len()
299                },
300                Some((k, v)) => {
301                    let (new_index, new_seq) = iter@;
302                    let (old_k, old_v) = old_seq[old_index];
303                    &&& 0 <= old_index < old_seq.len()
304                    &&& new_seq == old_seq
305                    &&& new_index == old_index + 1
306                    &&& k == old_k
307                    &&& v == old_v
308                    &&& old_seq.to_set().contains((*k, *v))
309                },
310            }
311        }),
312;
313
314pub struct MapIterGhostIterator<'a, Key: 'a, Value: 'a> {
315    pub pos: int,
316    pub kv_pairs: Seq<(Key, Value)>,
317    pub _marker: PhantomData<&'a Key>,
318}
319
320impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIteratorNew for btree_map::Iter<
321    'a,
322    Key,
323    Value,
324> {
325    type GhostIter = MapIterGhostIterator<'a, Key, Value>;
326
327    open spec fn ghost_iter(&self) -> MapIterGhostIterator<'a, Key, Value> {
328        MapIterGhostIterator { pos: self@.0, kv_pairs: self@.1, _marker: PhantomData }
329    }
330}
331
332impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for MapIterGhostIterator<
333    'a,
334    Key,
335    Value,
336> {
337    type ExecIter = btree_map::Iter<'a, Key, Value>;
338
339    type Item = (Key, Value);
340
341    type Decrease = int;
342
343    open spec fn exec_invariant(&self, exec_iter: &btree_map::Iter<'a, Key, Value>) -> bool {
344        &&& self.pos == exec_iter@.0
345        &&& self.kv_pairs == exec_iter@.1
346    }
347
348    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
349        init matches Some(init) ==> {
350            &&& init.pos == 0
351            &&& init.kv_pairs == self.kv_pairs
352            &&& 0 <= self.pos <= self.kv_pairs.len()
353        }
354    }
355
356    open spec fn ghost_ensures(&self) -> bool {
357        self.pos == self.kv_pairs.len()
358    }
359
360    open spec fn ghost_decrease(&self) -> Option<int> {
361        Some(self.kv_pairs.len() - self.pos)
362    }
363
364    open spec fn ghost_peek_next(&self) -> Option<(Key, Value)> {
365        if 0 <= self.pos < self.kv_pairs.len() {
366            Some(self.kv_pairs[self.pos])
367        } else {
368            None
369        }
370    }
371
372    open spec fn ghost_advance(
373        &self,
374        _exec_iter: &btree_map::Iter<'a, Key, Value>,
375    ) -> MapIterGhostIterator<'a, Key, Value> {
376        Self { pos: self.pos + 1, ..*self }
377    }
378}
379
380impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value> {
381    type V = Seq<(Key, Value)>;
382
383    open spec fn view(&self) -> Seq<(Key, Value)> {
384        self.kv_pairs.take(self.pos)
385    }
386}
387
388// To allow reasoning about the ghost iterator when the executable
389// function `iter()` is invoked in a `for` loop header (e.g., in
390// `for x in it: v.iter() { ... }`), we need to specify the behavior of
391// the iterator in spec mode. To do that, we add
392// `#[verifier::when_used_as_spec(spec_iter)]` to the specification for
393// the executable `iter` method and define that spec function here.
394pub uninterp spec fn spec_btree_map_iter<'a, Key, Value, A: Allocator + Clone>(
395    m: &'a BTreeMap<Key, Value, A>,
396) -> (r: btree_map::Iter<'a, Key, Value>);
397
398pub broadcast axiom fn axiom_spec_btree_map_iter<'a, Key, Value, A: Allocator + Clone>(
399    m: &'a BTreeMap<Key, Value, A>,
400)
401    ensures
402        ({
403            let (pos, v) = #[trigger] spec_btree_map_iter(m)@;
404            &&& pos == 0int
405            &&& forall|i: int| 0 <= i < v.len() ==> #[trigger] m@[v[i].0] == v[i].1
406            &&& increasing_seq(v.map(|idx: int, kv: (Key, Value)| kv.0))
407        }),
408;
409
410#[verifier::when_used_as_spec(spec_btree_map_iter)]
411pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::iter ](
412    m: &'a BTreeMap<Key, Value, A>,
413) -> (iter: btree_map::Iter<'a, Key, Value>)
414    ensures
415        key_obeys_cmp_spec::<Key>() ==> {
416            let (index, s) = iter@;
417            &&& index == 0
418            &&& s.to_set() == m@.kv_pairs()
419            &&& s.no_duplicates()
420            &&& increasing_seq(s.map(|idx: int, kv: (Key, Value)| kv.0))
421        },
422;
423
424/// Specifications for the behavior of [`std::collections::BTreeMap`](https://doc.rust-lang.org/std/collections/struct.BTreeMap.html).
425///
426/// We model a `BTreeMap` as having a view of type `Map<Key, Value>`, which reflects the current state of the map.
427///
428/// These specifications are only meaningful if `key_obeys_cmp_spec::<Key>()` holds.
429/// See [`key_obeys_cmp_spec`] for information on use with primitive types and other types.
430///
431/// Axioms about the behavior of BTreeMap are present in the broadcast group `vstd::std_specs::btree::group_btree_axioms`.
432#[verifier::external_type_specification]
433#[verifier::external_body]
434#[verifier::accept_recursive_types(Key)]
435#[verifier::accept_recursive_types(Value)]
436#[verifier::reject_recursive_types(A)]
437pub struct ExBTreeMap<Key, Value, A: Allocator + Clone>(BTreeMap<Key, Value, A>);
438
439pub trait BTreeMapAdditionalSpecFns<Key, Value>: View<V = Map<Key, Value>> {
440    spec fn spec_index(&self, k: Key) -> Value
441        recommends
442            self@.contains_key(k),
443    ;
444}
445
446impl<Key, Value, A: Allocator + Clone> BTreeMapAdditionalSpecFns<Key, Value> for BTreeMap<
447    Key,
448    Value,
449    A,
450> {
451    #[verifier::inline]
452    open spec fn spec_index(&self, k: Key) -> Value {
453        self@.index(k)
454    }
455}
456
457impl<Key, Value, A: Allocator + Clone> View for BTreeMap<Key, Value, A> {
458    type V = Map<Key, Value>;
459
460    uninterp spec fn view(&self) -> Map<Key, Value>;
461}
462
463impl<Key: DeepView, Value: DeepView, A: Allocator + Clone> DeepView for BTreeMap<Key, Value, A> {
464    type V = Map<Key::V, Value::V>;
465
466    open spec fn deep_view(&self) -> Map<Key::V, Value::V> {
467        btree_map_deep_view_impl(*self)
468    }
469}
470
471/// The actual definition of `BTreeMap::deep_view`.
472///
473/// This is a separate function since it introduces a lot of quantifiers and revealing an opaque trait
474/// method is not supported. In most cases, it's easier to use one of the lemmas below instead
475/// of revealing this function directly.
476#[verifier::opaque]
477pub open spec fn btree_map_deep_view_impl<Key: DeepView, Value: DeepView, A: Allocator + Clone>(
478    m: BTreeMap<Key, Value, A>,
479) -> Map<Key::V, Value::V> {
480    Map::new(
481        |k: Key::V|
482            exists|orig_k: Key| #[trigger] m@.contains_key(orig_k) && k == orig_k.deep_view(),
483        |dk: Key::V|
484            {
485                let k = choose|k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
486                m@[k].deep_view()
487            },
488    )
489}
490
491pub broadcast proof fn lemma_btree_map_deepview_dom<K: DeepView, V: DeepView>(m: BTreeMap<K, V>)
492    ensures
493        #[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),
494{
495    reveal(btree_map_deep_view_impl);
496    broadcast use group_btree_axioms;
497    broadcast use crate::vstd::group_vstd_default;
498
499    assert(m.deep_view().dom() =~= m@.dom().map(|k: K| k.deep_view()));
500}
501
502pub broadcast proof fn lemma_btree_map_deepview_properties<K: DeepView, V: DeepView>(
503    m: BTreeMap<K, V>,
504)
505    requires
506        crate::relations::injective(|k: K| k.deep_view()),
507    ensures
508        #![trigger m.deep_view()]
509        // all elements in m.view() are present in m.deep_view()
510        forall|k: K| #[trigger]
511            m@.contains_key(k) ==> m.deep_view().contains_key(k.deep_view())
512                && m.deep_view()[k.deep_view()] == m@[k].deep_view(),
513        // all elements in m.deep_view() are present in m.view()
514        forall|dk: <K as DeepView>::V| #[trigger]
515            m.deep_view().contains_key(dk) ==> exists|k: K|
516                k.deep_view() == dk && #[trigger] m@.contains_key(k),
517{
518    reveal(btree_map_deep_view_impl);
519    broadcast use group_btree_axioms;
520    broadcast use crate::vstd::group_vstd_default;
521
522    assert(m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()));
523    assert forall|k: K| #[trigger] m@.contains_key(k) implies m.deep_view().contains_key(
524        k.deep_view(),
525    ) && m.deep_view()[k.deep_view()] == m@[k].deep_view() by {
526        assert forall|k1: K, k2: K| #[trigger]
527            k1.deep_view() == #[trigger] k2.deep_view() implies k1 == k2 by {
528            let ghost k_deepview = |k: K| k.deep_view();
529            assert(crate::relations::injective(k_deepview));
530            assert(k_deepview(k1) == k_deepview(k2));
531        }
532    }
533}
534
535pub broadcast proof fn lemma_btree_map_deepview_values<K: DeepView, V: DeepView>(m: BTreeMap<K, V>)
536    requires
537        crate::relations::injective(|k: K| k.deep_view()),
538    ensures
539        #[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),
540{
541    reveal(btree_map_deep_view_impl);
542    broadcast use group_btree_axioms;
543    broadcast use lemma_btree_map_deepview_properties;
544    broadcast use crate::vstd::group_vstd_default;
545
546    let lhs = m.deep_view().values();
547    let rhs = m@.values().map(|v: V| v.deep_view());
548    assert forall|v: V::V| #[trigger] lhs.contains(v) implies rhs.contains(v) by {
549        let dk = choose|dk: K::V| #[trigger]
550            m.deep_view().contains_key(dk) && m.deep_view()[dk] == v;
551        let k = choose|k: K| #[trigger] m@.contains_key(k) && k.deep_view() == dk;
552        let ov = choose|ov: V| #[trigger] m@.contains_key(k) && m@[k] == ov && ov.deep_view() == v;
553        assert(v == ov.deep_view());
554        assert(m@.values().contains(ov));
555    }
556}
557
558/// Borrowing a key works the same way on deep_view as on view,
559/// if deep_view is injective; see `axiom_contains_deref_key`.
560pub broadcast axiom fn axiom_btree_map_deepview_borrow<
561    K: DeepView + Borrow<Q>,
562    V: DeepView,
563    Q: View<V = <K as DeepView>::V> + Eq + ?Sized,
564>(m: BTreeMap<K, V>, k: &Q)
565    requires
566        key_obeys_cmp_spec::<K>(),
567        crate::relations::injective(|k: K| k.deep_view()),
568    ensures
569        #[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),
570;
571
572/// A `Map` constructed from a `BTreeMap` is always finite.
573pub broadcast axiom fn axiom_btree_map_view_finite_dom<K, V>(m: BTreeMap<K, V>)
574    ensures
575        #[trigger] m@.dom().finite(),
576;
577
578pub uninterp spec fn spec_btree_map_len<Key, Value, A: Allocator + Clone>(
579    m: &BTreeMap<Key, Value, A>,
580) -> usize;
581
582pub broadcast axiom fn axiom_spec_btree_map_len<Key, Value, A: Allocator + Clone>(
583    m: &BTreeMap<Key, Value, A>,
584)
585    ensures
586        key_obeys_cmp_spec::<Key>() ==> #[trigger] spec_btree_map_len(m) == m@.len(),
587;
588
589#[verifier::when_used_as_spec(spec_btree_map_len)]
590pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::len ](
591    m: &BTreeMap<Key, Value, A>,
592) -> (len: usize)
593    ensures
594        len == spec_btree_map_len(m),
595;
596
597pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::is_empty ](
598    m: &BTreeMap<Key, Value, A>,
599) -> (res: bool)
600    ensures
601        res == m@.is_empty(),
602;
603
604pub assume_specification<K: Clone, V: Clone, A: Allocator + Clone>[ <BTreeMap::<
605    K,
606    V,
607    A,
608> as Clone>::clone ](this: &BTreeMap<K, V, A>) -> (other: BTreeMap<K, V, A>)
609    ensures
610        other@ == this@,
611;
612
613pub assume_specification<Key, Value>[ BTreeMap::<Key, Value>::new ]() -> (m: BTreeMap<Key, Value>)
614    ensures
615        m@ == Map::<Key, Value>::empty(),
616;
617
618pub assume_specification<K, V>[ <BTreeMap<K, V> as core::default::Default>::default ]() -> (m:
619    BTreeMap<K, V>)
620    ensures
621        m@ == Map::<K, V>::empty(),
622;
623
624pub assume_specification<Key: Ord, Value, A: Allocator + Clone>[ BTreeMap::<
625    Key,
626    Value,
627    A,
628>::insert ](m: &mut BTreeMap<Key, Value, A>, k: Key, v: Value) -> (result: Option<Value>)
629    ensures
630        obeys_cmp_spec::<Key>() ==> {
631            &&& m@ == old(m)@.insert(k, v)
632            &&& match result {
633                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
634                None => !old(m)@.contains_key(k),
635            }
636        },
637;
638
639// The specification for `contains_key` has a parameter `key: &Q`
640// where you'd expect to find `key: &Key`. This allows for the case
641// that `Key` can be borrowed as something other than `&Key`. For
642// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
643// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
644// respectively.
645// To deal with this, we have a specification function that opaquely
646// specifies what it means for a map to contain a borrowed key of type
647// `&Q`. And the postcondition of `contains_key` just says that its
648// result matches the output of that specification function. But this
649// isn't very helpful by itself, since there's no body to that
650// specification function. So we have special-case axioms that say
651// what this means in two important circumstances: (1) `Key = Q` and
652// (2) `Key = Box<Q>`.
653pub uninterp spec fn contains_borrowed_key<Key, Value, Q: ?Sized>(
654    m: Map<Key, Value>,
655    k: &Q,
656) -> bool;
657
658pub broadcast axiom fn axiom_contains_deref_key<Q, Value>(m: Map<Q, Value>, k: &Q)
659    ensures
660        #[trigger] contains_borrowed_key::<Q, Value, Q>(m, k) <==> m.contains_key(*k),
661;
662
663pub broadcast axiom fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
664    ensures
665        #[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k) <==> m.contains_key(
666            Box::new(*k),
667        ),
668;
669
670pub assume_specification<
671    Key: Borrow<Q> + Ord,
672    Value,
673    A: Allocator + Clone,
674    Q: Ord + ?Sized,
675>[ BTreeMap::<Key, Value, A>::contains_key::<Q> ](m: &BTreeMap<Key, Value, A>, k: &Q) -> (result:
676    bool)
677    ensures
678        obeys_cmp_spec::<Key>() ==> result == contains_borrowed_key(m@, k),
679;
680
681// The specification for `get` has a parameter `key: &Q` where you'd
682// expect to find `key: &Key`. This allows for the case that `Key` can
683// be borrowed as something other than `&Key`. For instance,
684// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
685// as `&str`, so in those cases `Q` would be `u32` and `str`
686// respectively.
687// To deal with this, we have a specification function that opaquely
688// specifies what it means for a map to map a borrowed key of type
689// `&Q` to a certain value. And the postcondition of `get` says that
690// its result matches the output of that specification function. (It
691// also says that its result corresponds to the output of
692// `contains_borrowed_key`, discussed above.) But this isn't very
693// helpful by itself, since there's no body to that specification
694// function. So we have special-case axioms that say what this means
695// in two important circumstances: (1) `Key = Q` and (2) `Key =
696// Box<Q>`.
697pub uninterp spec fn maps_borrowed_key_to_value<Key, Value, Q: ?Sized>(
698    m: Map<Key, Value>,
699    k: &Q,
700    v: Value,
701) -> bool;
702
703pub broadcast axiom fn axiom_maps_deref_key_to_value<Q, Value>(m: Map<Q, Value>, k: &Q, v: Value)
704    ensures
705        #[trigger] maps_borrowed_key_to_value::<Q, Value, Q>(m, k, v) <==> m.contains_key(*k)
706            && m[*k] == v,
707;
708
709pub broadcast axiom fn axiom_maps_box_key_to_value<Q, Value>(m: Map<Box<Q>, Value>, q: &Q, v: Value)
710    ensures
711        #[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v) <==> {
712            let k = Box::new(*q);
713            &&& m.contains_key(k)
714            &&& m[k] == v
715        },
716;
717
718pub assume_specification<
719    'a,
720    Key: Borrow<Q> + Ord,
721    Value,
722    A: Allocator + Clone,
723    Q: Ord + ?Sized,
724>[ BTreeMap::<Key, Value, A>::get::<Q> ](m: &'a BTreeMap<Key, Value, A>, k: &Q) -> (result: Option<
725    &'a Value,
726>)
727    ensures
728        obeys_cmp_spec::<Key>() ==> match result {
729            Some(v) => maps_borrowed_key_to_value(m@, k, *v),
730            None => !contains_borrowed_key(m@, k),
731        },
732;
733
734// The specification for `remove` has a parameter `key: &Q` where
735// you'd expect to find `key: &Key`. This allows for the case that
736// `Key` can be borrowed as something other than `&Key`. For instance,
737// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
738// as `&str`, so in those cases `Q` would be `u32` and `str`
739// respectively. To deal with this, we have a specification function
740// that opaquely specifies what it means for two maps to be related by
741// a remove of a certain `&Q`. And the postcondition of `remove` says
742// that `old(self)@` and `self@` satisfy that relationship. (It also
743// says that its result corresponds to the output of
744// `contains_borrowed_key` and `maps_borrowed_key_to_value`, discussed
745// above.) But this isn't very helpful by itself, since there's no
746// body to that specification function. So we have special-case axioms
747// that say what this means in two important circumstances: (1) `Key =
748// Q` and (2) `Key = Box<Q>`.
749pub uninterp spec fn borrowed_key_removed<Key, Value, Q: ?Sized>(
750    old_m: Map<Key, Value>,
751    new_m: Map<Key, Value>,
752    k: &Q,
753) -> bool;
754
755pub broadcast axiom fn axiom_deref_key_removed<Q, Value>(
756    old_m: Map<Q, Value>,
757    new_m: Map<Q, Value>,
758    k: &Q,
759)
760    ensures
761        #[trigger] borrowed_key_removed::<Q, Value, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
762            *k,
763        ),
764;
765
766pub broadcast axiom fn axiom_box_key_removed<Q, Value>(
767    old_m: Map<Box<Q>, Value>,
768    new_m: Map<Box<Q>, Value>,
769    q: &Q,
770)
771    ensures
772        #[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q) <==> new_m
773            == old_m.remove(Box::new(*q)),
774;
775
776pub assume_specification<
777    Key: Borrow<Q> + Ord,
778    Value,
779    A: Allocator + Clone,
780    Q: Ord + ?Sized,
781>[ BTreeMap::<Key, Value, A>::remove::<Q> ](m: &mut BTreeMap<Key, Value, A>, k: &Q) -> (result:
782    Option<Value>)
783    ensures
784        obeys_cmp_spec::<Key>() ==> {
785            &&& borrowed_key_removed(old(m)@, m@, k)
786            &&& match result {
787                Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
788                None => !contains_borrowed_key(old(m)@, k),
789            }
790        },
791;
792
793pub assume_specification<Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::clear ](
794    m: &mut BTreeMap<Key, Value, A>,
795)
796    ensures
797        m@ == Map::<Key, Value>::empty(),
798;
799
800pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::keys ](
801    m: &'a BTreeMap<Key, Value, A>,
802) -> (keys: Keys<'a, Key, Value>)
803    ensures
804        key_obeys_cmp_spec::<Key>() ==> {
805            let (index, s) = keys@;
806            &&& index == 0
807            &&& s.to_set() == m@.dom()
808            &&& s.no_duplicates()
809            &&& increasing_seq(s)
810        },
811;
812
813pub assume_specification<'a, Key, Value, A: Allocator + Clone>[ BTreeMap::<Key, Value, A>::values ](
814    m: &'a BTreeMap<Key, Value, A>,
815) -> (values: Values<'a, Key, Value>)
816    ensures
817        key_obeys_cmp_spec::<Key>() ==> {
818            let (index, s) = values@;
819            &&& index == 0
820            &&& s.to_set() == m@.values()
821            &&& exists|key_seq: Seq<Key>|
822                {
823                    &&& increasing_seq(key_seq)
824                    &&& key_seq.to_set() == m@.dom()
825                    &&& key_seq.no_duplicates()
826                    &&& s == key_seq.map(|i: int, k| m@[k])
827                }
828        },
829;
830
831pub broadcast axiom fn axiom_btree_map_decreases<Key, Value, A: Allocator + Clone>(
832    m: BTreeMap<Key, Value, A>,
833)
834    ensures
835        #[trigger] (decreases_to!(m => m@)),
836;
837
838// The `iter` method of a `BTreeSet` returns an iterator of type `btree_set::Iter`,
839// so we specify that type here.
840#[verifier::external_type_specification]
841#[verifier::external_body]
842#[verifier::accept_recursive_types(K)]
843pub struct ExSetIter<'a, K: 'a>(btree_set::Iter<'a, K>);
844
845impl<'a, Key> View for btree_set::Iter<'a, Key> {
846    type V = (int, Seq<Key>);
847
848    uninterp spec fn view(self: &btree_set::Iter<'a, Key>) -> (int, Seq<Key>);
849}
850
851pub assume_specification<'a, Key>[ btree_set::Iter::<'a, Key>::next ](
852    elements: &mut btree_set::Iter<'a, Key>,
853) -> (r: Option<&'a Key>)
854    ensures
855        ({
856            let (old_index, old_seq) = old(elements)@;
857            match r {
858                None => {
859                    &&& elements@ == old(elements)@
860                    &&& old_index >= old_seq.len()
861                },
862                Some(element) => {
863                    let (new_index, new_seq) = elements@;
864                    &&& 0 <= old_index < old_seq.len()
865                    &&& new_seq == old_seq
866                    &&& new_index == old_index + 1
867                    &&& element == old_seq[old_index]
868                },
869            }
870        }),
871;
872
873pub struct SetIterGhostIterator<'a, Key> {
874    pub pos: int,
875    pub elements: Seq<Key>,
876    pub phantom: Option<&'a Key>,
877}
878
879impl<'a, Key> super::super::pervasive::ForLoopGhostIteratorNew for btree_set::Iter<'a, Key> {
880    type GhostIter = SetIterGhostIterator<'a, Key>;
881
882    open spec fn ghost_iter(&self) -> SetIterGhostIterator<'a, Key> {
883        SetIterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
884    }
885}
886
887impl<'a, Key> super::super::pervasive::ForLoopGhostIterator for SetIterGhostIterator<'a, Key> {
888    type ExecIter = btree_set::Iter<'a, Key>;
889
890    type Item = Key;
891
892    type Decrease = int;
893
894    open spec fn exec_invariant(&self, exec_iter: &btree_set::Iter<'a, Key>) -> bool {
895        &&& self.pos == exec_iter@.0
896        &&& self.elements == exec_iter@.1
897    }
898
899    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
900        init matches Some(init) ==> {
901            &&& init.pos == 0
902            &&& init.elements == self.elements
903            &&& 0 <= self.pos <= self.elements.len()
904        }
905    }
906
907    open spec fn ghost_ensures(&self) -> bool {
908        self.pos == self.elements.len()
909    }
910
911    open spec fn ghost_decrease(&self) -> Option<int> {
912        Some(self.elements.len() - self.pos)
913    }
914
915    open spec fn ghost_peek_next(&self) -> Option<Key> {
916        if 0 <= self.pos < self.elements.len() {
917            Some(self.elements[self.pos])
918        } else {
919            None
920        }
921    }
922
923    open spec fn ghost_advance(
924        &self,
925        _exec_iter: &btree_set::Iter<'a, Key>,
926    ) -> SetIterGhostIterator<'a, Key> {
927        Self { pos: self.pos + 1, ..*self }
928    }
929}
930
931impl<'a, Key> View for SetIterGhostIterator<'a, Key> {
932    type V = Seq<Key>;
933
934    open spec fn view(&self) -> Seq<Key> {
935        self.elements.take(self.pos)
936    }
937}
938
939/// Specifications for the behavior of [`std::collections::BTreeSet`](https://doc.rust-lang.org/std/collections/struct.BTreeSet.html).
940///
941/// We model a `BTreeSet` as having a view of type `Set<Key>`, which reflects the current state of the set.
942///
943/// These specifications are only meaningful if `obeys_cmp_spec::<Key>()` hold.
944/// See [`obeys_cmp_spec`] for information on use with primitive types and custom types.
945///
946/// Axioms about the behavior of BTreeSet are present in the broadcast group `vstd::std_specs::btree::group_btree_axioms`.
947#[verifier::external_type_specification]
948#[verifier::external_body]
949#[verifier::accept_recursive_types(Key)]
950#[verifier::reject_recursive_types(A)]
951pub struct ExBTreeSet<Key, A: Allocator + Clone>(BTreeSet<Key, A>);
952
953impl<Key, A: Allocator + Clone> View for BTreeSet<Key, A> {
954    type V = Set<Key>;
955
956    uninterp spec fn view(&self) -> Set<Key>;
957}
958
959impl<Key: DeepView, A: Allocator + Clone> DeepView for BTreeSet<Key, A> {
960    type V = Set<Key::V>;
961
962    open spec fn deep_view(&self) -> Set<Key::V> {
963        self@.map(|x: Key| x.deep_view())
964    }
965}
966
967pub uninterp spec fn spec_btree_set_len<Key, A: Allocator + Clone>(m: &BTreeSet<Key, A>) -> usize;
968
969pub broadcast axiom fn axiom_spec_btree_set_len<Key, A: Allocator + Clone>(m: &BTreeSet<Key, A>)
970    ensures
971        key_obeys_cmp_spec::<Key>() ==> #[trigger] spec_btree_set_len(m) == m@.len(),
972;
973
974#[verifier::when_used_as_spec(spec_btree_set_len)]
975pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::len ](
976    m: &BTreeSet<Key, A>,
977) -> (len: usize)
978    ensures
979        len == spec_btree_set_len(m),
980;
981
982pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::is_empty ](
983    m: &BTreeSet<Key, A>,
984) -> (res: bool)
985    ensures
986        res == m@.is_empty(),
987;
988
989pub assume_specification<K: Clone, A: Allocator + Clone>[ <BTreeSet::<K, A> as Clone>::clone ](
990    this: &BTreeSet<K, A>,
991) -> (other: BTreeSet<K, A>)
992    ensures
993        other@ == this@,
994;
995
996pub assume_specification<Key>[ BTreeSet::<Key>::new ]() -> (m: BTreeSet<Key>)
997    ensures
998        m@ == Set::<Key>::empty(),
999;
1000
1001pub assume_specification<T>[ <BTreeSet<T> as core::default::Default>::default ]() -> (m: BTreeSet<
1002    T,
1003>)
1004    ensures
1005        m@ == Set::<T>::empty(),
1006;
1007
1008pub assume_specification<Key: Ord, A: Allocator + Clone>[ BTreeSet::<Key, A>::insert ](
1009    m: &mut BTreeSet<Key, A>,
1010    k: Key,
1011) -> (result: bool)
1012    ensures
1013        obeys_cmp_spec::<Key>() ==> {
1014            &&& m@ == old(m)@.insert(k)
1015            &&& result == !old(m)@.contains(k)
1016        },
1017;
1018
1019// The specification for `contains` has a parameter `key: &Q`
1020// where you'd expect to find `key: &Key`. This allows for the case
1021// that `Key` can be borrowed as something other than `&Key`. For
1022// instance, `Box<u32>` can be borrowed as `&u32` and `String` can be
1023// borrowed as `&str`, so in those cases `Q` would be `u32` and `str`
1024// respectively.
1025// To deal with this, we have a specification function that opaquely
1026// specifies what it means for a set to contain a borrowed key of type
1027// `&Q`. And the postcondition of `contains` just says that its
1028// result matches the output of that specification function. But this
1029// isn't very helpful by itself, since there's no body to that
1030// specification function. So we have special-case axioms that say
1031// what this means in two important circumstances: (1) `Key = Q` and
1032// (2) `Key = Box<Q>`.
1033pub uninterp spec fn set_contains_borrowed_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q) -> bool;
1034
1035pub broadcast axiom fn axiom_set_contains_deref_key<Q>(m: Set<Q>, k: &Q)
1036    ensures
1037        #[trigger] set_contains_borrowed_key::<Q, Q>(m, k) <==> m.contains(*k),
1038;
1039
1040pub broadcast axiom fn axiom_set_contains_box<Q>(m: Set<Box<Q>>, k: &Q)
1041    ensures
1042        #[trigger] set_contains_borrowed_key::<Box<Q>, Q>(m, k) <==> m.contains(Box::new(*k)),
1043;
1044
1045pub assume_specification<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>[ BTreeSet::<
1046    Key,
1047    A,
1048>::contains ](m: &BTreeSet<Key, A>, k: &Q) -> (result: bool)
1049    ensures
1050        obeys_cmp_spec::<Key>() ==> result == set_contains_borrowed_key(m@, k),
1051;
1052
1053// The specification for `get` has a parameter `key: &Q` where you'd
1054// expect to find `key: &Key`. This allows for the case that `Key` can
1055// be borrowed as something other than `&Key`. For instance,
1056// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1057// as `&str`, so in those cases `Q` would be `u32` and `str`
1058// respectively.
1059// To deal with this, we have a specification function that opaquely
1060// specifies what it means for a returned reference to point to an
1061// element of a BTreeSet. And the postcondition of `get` says that
1062// its result matches the output of that specification function. (It
1063// also says that its result corresponds to the output of
1064// `contains_borrowed_key`, discussed above.) But this isn't very
1065// helpful by itself, since there's no body to that specification
1066// function. So we have special-case axioms that say what this means
1067// in two important circumstances: (1) `Key = Q` and (2) `Key =
1068// Box<Q>`.
1069pub uninterp spec fn sets_borrowed_key_to_key<Key, Q: ?Sized>(m: Set<Key>, k: &Q, v: &Key) -> bool;
1070
1071pub broadcast axiom fn axiom_set_deref_key_to_value<Q>(m: Set<Q>, k: &Q, v: &Q)
1072    ensures
1073        #[trigger] sets_borrowed_key_to_key::<Q, Q>(m, k, v) <==> m.contains(*k) && k == v,
1074;
1075
1076pub broadcast axiom fn axiom_set_box_key_to_value<Q>(m: Set<Box<Q>>, q: &Q, v: &Box<Q>)
1077    ensures
1078        #[trigger] sets_borrowed_key_to_key::<Box<Q>, Q>(m, q, v) <==> (m.contains(*v) && Box::new(
1079            *q,
1080        ) == v),
1081;
1082
1083pub assume_specification<
1084    'a,
1085    Key: Borrow<Q> + Ord,
1086    A: Allocator + Clone,
1087    Q: Ord + ?Sized,
1088>[ BTreeSet::<Key, A>::get::<Q> ](m: &'a BTreeSet<Key, A>, k: &Q) -> (result: Option<&'a Key>)
1089    ensures
1090        obeys_cmp_spec::<Key>() ==> match result {
1091            Some(v) => sets_borrowed_key_to_key(m@, k, v),
1092            None => !set_contains_borrowed_key(m@, k),
1093        },
1094;
1095
1096// The specification for `remove` has a parameter `key: &Q` where
1097// you'd expect to find `key: &Key`. This allows for the case that
1098// `Key` can be borrowed as something other than `&Key`. For instance,
1099// `Box<u32>` can be borrowed as `&u32` and `String` can be borrowed
1100// as `&str`, so in those cases `Q` would be `u32` and `str`
1101// respectively. To deal with this, we have a specification function
1102// that opaquely specifies what it means for two sets to be related by
1103// a remove of a certain `&Q`. And the postcondition of `remove` says
1104// that `old(self)@` and `self@` satisfy that relationship. (It also
1105// says that its result corresponds to the output of
1106// `set_contains_borrowed_key`, discussed above.) But this isn't very
1107// helpful by itself, since there's no body to that specification
1108// function. So we have special-case axioms that say what this means
1109// in two important circumstances: (1) `Key = Q` and (2) `Key = Box<Q>`.
1110pub uninterp spec fn sets_differ_by_borrowed_key<Key, Q: ?Sized>(
1111    old_m: Set<Key>,
1112    new_m: Set<Key>,
1113    k: &Q,
1114) -> bool;
1115
1116pub broadcast axiom fn axiom_set_deref_key_removed<Q>(old_m: Set<Q>, new_m: Set<Q>, k: &Q)
1117    ensures
1118        #[trigger] sets_differ_by_borrowed_key::<Q, Q>(old_m, new_m, k) <==> new_m == old_m.remove(
1119            *k,
1120        ),
1121;
1122
1123pub broadcast axiom fn axiom_set_box_key_removed<Q>(old_m: Set<Box<Q>>, new_m: Set<Box<Q>>, q: &Q)
1124    ensures
1125        #[trigger] sets_differ_by_borrowed_key::<Box<Q>, Q>(old_m, new_m, q) <==> new_m
1126            == old_m.remove(Box::new(*q)),
1127;
1128
1129pub assume_specification<Key: Borrow<Q> + Ord, A: Allocator + Clone, Q: Ord + ?Sized>[ BTreeSet::<
1130    Key,
1131    A,
1132>::remove::<Q> ](m: &mut BTreeSet<Key, A>, k: &Q) -> (result: bool)
1133    ensures
1134        obeys_cmp_spec::<Key>() ==> {
1135            &&& sets_differ_by_borrowed_key(old(m)@, m@, k)
1136            &&& result == set_contains_borrowed_key(old(m)@, k)
1137        },
1138;
1139
1140pub assume_specification<Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::clear ](
1141    m: &mut BTreeSet<Key, A>,
1142) where A: Clone
1143    ensures
1144        m@ == Set::<Key>::empty(),
1145;
1146
1147pub assume_specification<'a, Key, A: Allocator + Clone>[ BTreeSet::<Key, A>::iter ](
1148    m: &'a BTreeSet<Key, A>,
1149) -> (r: btree_set::Iter<'a, Key>)
1150    ensures
1151        key_obeys_cmp_spec::<Key>() ==> {
1152            let (index, s) = r@;
1153            &&& index == 0
1154            &&& s.to_set() == m@
1155            &&& s.no_duplicates()
1156            &&& increasing_seq(s)
1157        },
1158;
1159
1160pub broadcast axiom fn axiom_btree_set_decreases<Key, A: Allocator + Clone>(m: BTreeSet<Key, A>)
1161    ensures
1162        #[trigger] (decreases_to!(m => m@)),
1163;
1164
1165pub broadcast group group_btree_axioms {
1166    axiom_key_obeys_cmp_spec_meaning,
1167    axiom_increasing_seq_meaning,
1168    axiom_box_key_removed,
1169    axiom_contains_deref_key,
1170    axiom_contains_box,
1171    axiom_deref_key_removed,
1172    axiom_maps_deref_key_to_value,
1173    axiom_maps_box_key_to_value,
1174    axiom_btree_map_deepview_borrow,
1175    axiom_btree_map_view_finite_dom,
1176    axiom_spec_btree_map_len,
1177    axiom_set_box_key_removed,
1178    axiom_set_contains_deref_key,
1179    axiom_set_contains_box,
1180    axiom_set_deref_key_removed,
1181    axiom_set_deref_key_to_value,
1182    axiom_set_box_key_to_value,
1183    axiom_spec_btree_set_len,
1184    axiom_spec_btree_map_iter,
1185    axiom_btree_map_decreases,
1186    axiom_btree_set_decreases,
1187}
1188
1189} // verus!
vstd/std_specs/btree.rs

vstd/std_specs/
btree.rs
