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

vstd/std_specs/
btree.rs
