vstd/std_specs/
range.rs

1use super::super::laws_cmp::obeys_cmp;
2use super::super::prelude::*;
3use super::super::view::View;
4use super::cmp::{PartialOrdIs, PartialOrdSpec};
5use super::iter::{IteratorSpec, StepSpec, StepSpecImpl};
6use core::ops::{
7    Bound, Range, RangeBounds, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,
8};
9
10verus! {
11
12#[verifier::external_type_specification]
13#[verifier::reject_recursive_types_in_ground_variants(Idx)]
14pub struct ExRange<Idx>(Range<Idx>);
15
16#[verifier::external_type_specification]
17#[verifier::external_body]
18#[verifier::reject_recursive_types_in_ground_variants(Idx)]
19pub struct ExRangeInclusive<Idx>(RangeInclusive<Idx>);
20
21pub struct RangeInclusiveView<Idx> {
22    pub start: Idx,
23    pub end: Idx,
24    /// Whether iteration has marked the range as finished.
25    pub exhausted: bool,
26}
27
28pub open spec fn spec_range_inclusive_is_empty<Idx>(r: &RangeInclusive<Idx>) -> bool {
29    r@.exhausted || spec_range_inclusive_out_of_order(r)
30}
31
32/// Uninterpreted because `RangeBounds` methods have no
33/// `PartialOrd` bound. Defined by [`axiom_range_inclusive_out_of_order`].
34pub uninterp spec fn spec_range_inclusive_out_of_order<Idx>(r: &RangeInclusive<Idx>) -> bool;
35
36pub broadcast axiom fn axiom_range_inclusive_out_of_order<Idx: PartialOrd<Idx>>(
37    r: &RangeInclusive<Idx>,
38)
39    ensures
40        Idx::obeys_partial_cmp_spec() ==> (#[trigger] spec_range_inclusive_out_of_order(r)
41            <==> !r@.start.is_le(&r@.end)),
42;
43
44// Results std leaves unspecified for empty ranges.
45pub uninterp spec fn spec_range_inclusive_unspecified_contains<Idx, U: ?Sized>(
46    r: &RangeInclusive<Idx>,
47    item: &U,
48) -> bool;
49
50pub uninterp spec fn spec_range_inclusive_unspecified_bounds<T>(r: &RangeInclusive<T>) -> (
51    Bound<&T>,
52    Bound<&T>,
53);
54
55pub uninterp spec fn spec_range_inclusive_unspecified_ref_bounds<'a, T>(
56    r: &RangeInclusive<&'a T>,
57) -> (Bound<&'a T>, Bound<&'a T>);
58
59pub trait ContainsSpec<Idx, U> where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx> {
60    spec fn obeys_contains() -> bool;
61
62    spec fn contains_spec(&self, i: &U) -> bool;
63}
64
65impl<Idx, U> ContainsSpec<Idx, U> for RangeInclusive<Idx> where
66    Idx: PartialOrd<U>,
67    U: ?Sized + PartialOrd<Idx>,
68 {
69    open spec fn obeys_contains() -> bool {
70        (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec())
71    }
72
73    open spec fn contains_spec(&self, i: &U) -> bool {
74        if spec_range_inclusive_is_empty(self) {
75            spec_range_inclusive_unspecified_contains(self, i)
76        } else {
77            self@.start.is_le(&i) && i.is_le(&self@.end)
78        }
79    }
80}
81
82/// An empty range contains nothing when `Idx` is totally ordered.
83pub broadcast axiom fn axiom_range_inclusive_empty_contains<Idx: Ord>(
84    r: &RangeInclusive<Idx>,
85    item: &Idx,
86)
87    requires
88        obeys_cmp::<Idx>(),
89        spec_range_inclusive_is_empty(r),
90    ensures
91        !#[trigger] r.contains_spec(item),
92;
93
94impl<Idx, U> ContainsSpec<Idx, U> for Range<Idx> where
95    Idx: PartialOrd<U>,
96    U: ?Sized + PartialOrd<Idx>,
97 {
98    open spec fn obeys_contains() -> bool {
99        (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec())
100    }
101
102    open spec fn contains_spec(&self, i: &U) -> bool {
103        self.start.is_le(&i) && i.is_lt(&self.end)
104    }
105}
106
107impl<Idx> View for RangeInclusive<Idx> {
108    type V = RangeInclusiveView<Idx>;
109
110    uninterp spec fn view(&self) -> Self::V;
111}
112
113pub uninterp spec fn spec_range_next<A>(a: Range<A>) -> (Range<A>, Option<A>);
114
115/// Whether `A`'s executable stepping, comparison, and cloning obey the model
116/// used by range iterators. The axioms below establish this for primitive
117/// integers only; implementing `StepSpecImpl` alone does not establish it.
118pub uninterp spec fn obeys_range_step_spec<A>() -> bool;
119
120/// Range::contains method is valid and safe to use only when cmp operations are implemented to satisfy
121/// obeys_partial_cmp_spec. Specifically, the comparison must be deterministic, and `lt` (less than)
122/// and `le` (less than or equal to) must define total orders.
123/// If using Range::contains with types that do not satisfy obeys_partial_cmp_spec, no spec is provided.
124pub assume_specification<Idx: PartialOrd<Idx>, U>[ Range::<Idx>::contains ](
125    r: &Range<Idx>,
126    i: &U,
127) -> (ret: bool) where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>
128    ensures
129        <Range::<Idx> as ContainsSpec<Idx, U>>::obeys_contains() ==> ret == r.contains_spec(i),
130;
131
132pub assume_specification<Idx: PartialOrd<Idx>, U>[ RangeInclusive::<Idx>::contains ](
133    r: &RangeInclusive<Idx>,
134    i: &U,
135) -> (ret: bool) where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>
136    ensures
137        <RangeInclusive::<Idx> as ContainsSpec<Idx, U>>::obeys_contains() ==> ret
138            == r.contains_spec(i),
139;
140
141pub assume_specification<Idx: PartialOrd<Idx>>[ RangeInclusive::<Idx>::is_empty ](
142    r: &RangeInclusive<Idx>,
143) -> (res: bool) where Idx: PartialOrd<Idx>
144    ensures
145        <Idx as PartialOrdSpec<Idx>>::obeys_partial_cmp_spec() ==> res
146            == spec_range_inclusive_is_empty(r),
147;
148
149pub assume_specification<Idx>[ RangeInclusive::<Idx>::new ](start: Idx, end: Idx) -> (ret:
150    core::ops::RangeInclusive<Idx>)
151    ensures
152        ret@ == (RangeInclusiveView { start, end, exhausted: false }),
153;
154
155impl<A: core::iter::Step> super::iter::IteratorSpecImpl for Range<A> {
156    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
157        obeys_range_step_spec::<A>()
158    }
159
160    open spec fn remaining(&self) -> Seq<Self::Item> {
161        let steps = self.start.spec_steps_between_int(self.end);
162        let len = if steps > 0 {
163            steps
164        } else {
165            0
166        };
167        Seq::new(len as nat, |i: int| self.start.spec_forward_checked_int(i).unwrap())
168    }
169
170    #[verifier::prophetic]
171    open spec fn produces(&self) -> Seq<bool> {
172        Seq::new(IteratorSpec::remaining(self).len(), |i: int| true)
173    }
174
175    open spec fn decrease(&self) -> Option<nat> {
176        Some(self.start.spec_steps_between_int(self.end) as nat)
177    }
178
179    open spec fn peek(&self, index: int) -> Option<Self::Item> {
180        //Some(self.start.spec_forward_checked_int(index).unwrap())
181        if 0 <= index <= self.start.spec_steps_between_int(self.end) {
182            Some(self.start.spec_forward_checked_int(index).unwrap())
183        } else {
184            None
185        }
186    }
187}
188
189/// Number of elements left in an inclusive range: zero once it is exhausted or if `start > end`.
190pub open spec fn spec_range_inclusive_len<A: core::iter::Step>(r: &RangeInclusive<A>) -> nat {
191    let steps = r@.start.spec_steps_between_int(r@.end);
192    if steps >= 0 && !r@.exhausted {
193        (steps + 1) as nat
194    } else {
195        0
196    }
197}
198
199impl<A: core::iter::Step> super::iter::IteratorSpecImpl for RangeInclusive<A> {
200    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
201        obeys_range_step_spec::<A>()
202    }
203
204    open spec fn remaining(&self) -> Seq<Self::Item> {
205        Seq::new(
206            spec_range_inclusive_len(self),
207            |i: int| self@.start.spec_forward_checked_int(i).unwrap(),
208        )
209    }
210
211    #[verifier::prophetic]
212    open spec fn produces(&self) -> Seq<bool> {
213        Seq::new(IteratorSpec::remaining(self).len(), |i: int| true)
214    }
215
216    open spec fn decrease(&self) -> Option<nat> {
217        Some(spec_range_inclusive_len(self))
218    }
219
220    open spec fn peek(&self, index: int) -> Option<Self::Item> {
221        if 0 <= index <= spec_range_inclusive_len(self) {
222            Some(self@.start.spec_forward_checked_int(index).unwrap())
223        } else {
224            None
225        }
226    }
227}
228
229pub assume_specification<A: core::iter::Step>[ <Range<A> as Iterator>::next ](
230    range: &mut Range<A>,
231) -> (r: Option<A>)
232    ensures
233        obeys_range_step_spec::<A>() ==> (*final(range), r) == spec_range_next(*old(range)),
234;
235
236#[verifier::external_type_specification]
237pub struct ExBound<T>(Bound<T>);
238
239#[verifier::external_type_specification]
240pub struct ExRangeFull(RangeFull);
241
242#[verifier::external_type_specification]
243#[verifier::reject_recursive_types(Idx)]
244pub struct ExRangeFrom<Idx>(RangeFrom<Idx>);
245
246#[verifier::external_type_specification]
247#[verifier::reject_recursive_types(Idx)]
248pub struct ExRangeTo<Idx>(RangeTo<Idx>);
249
250#[verifier::external_type_specification]
251#[verifier::reject_recursive_types(Idx)]
252pub struct ExRangeToInclusive<Idx>(RangeToInclusive<Idx>);
253
254pub open spec fn bound_as_ref<T>(b: &Bound<T>) -> Bound<&T> {
255    match b {
256        Bound::Included(start) => Bound::Included(start),
257        Bound::Excluded(start) => Bound::Excluded(start),
258        Bound::Unbounded => Bound::Unbounded,
259    }
260}
261
262// Per-type specifications for `RangeBounds::start_bound`/`end_bound`. Each spec
263// agrees with the corresponding `RangeBoundsSpecImpl`, and so with the
264// `ExRangeBounds` ensures below.
265pub assume_specification<'s, T>[ <Range<T> as RangeBounds<T>>::start_bound ](
266    range: &'s Range<T>,
267) -> (result: Bound<&'s T>)
268    ensures
269        result == Bound::Included(&range.start),
270;
271
272pub assume_specification<'s, T>[ <Range<T> as RangeBounds<T>>::end_bound ](
273    range: &'s Range<T>,
274) -> (result: Bound<&'s T>)
275    ensures
276        result == Bound::Excluded(&range.end),
277;
278
279pub assume_specification<'s, T: ?Sized>[ <RangeFull as RangeBounds<T>>::start_bound ](
280    range: &'s RangeFull,
281) -> (result: Bound<&'s T>)
282    ensures
283        result == Bound::Unbounded,
284;
285
286pub assume_specification<'s, T: ?Sized>[ <RangeFull as RangeBounds<T>>::end_bound ](
287    range: &'s RangeFull,
288) -> (result: Bound<&'s T>)
289    ensures
290        result == Bound::Unbounded,
291;
292
293pub assume_specification<'s, T>[ <RangeFrom<T> as RangeBounds<T>>::start_bound ](
294    range: &'s RangeFrom<T>,
295) -> (result: Bound<&'s T>)
296    ensures
297        result == Bound::Included(&range.start),
298;
299
300pub assume_specification<'s, T>[ <RangeFrom<T> as RangeBounds<T>>::end_bound ](
301    range: &'s RangeFrom<T>,
302) -> (result: Bound<&'s T>)
303    ensures
304        result == Bound::Unbounded,
305;
306
307pub assume_specification<'s, T>[ <RangeTo<T> as RangeBounds<T>>::start_bound ](
308    range: &'s RangeTo<T>,
309) -> (result: Bound<&'s T>)
310    ensures
311        result == Bound::Unbounded,
312;
313
314pub assume_specification<'s, T>[ <RangeTo<T> as RangeBounds<T>>::end_bound ](
315    range: &'s RangeTo<T>,
316) -> (result: Bound<&'s T>)
317    ensures
318        result == Bound::Excluded(&range.end),
319;
320
321// Shared by `start_bound()`/`end_bound()` and their `RangeBoundsSpec` models.
322pub open spec fn spec_range_inclusive_start_bound<T>(r: &RangeInclusive<T>) -> Bound<&T> {
323    if spec_range_inclusive_is_empty(r) {
324        spec_range_inclusive_unspecified_bounds(r).0
325    } else {
326        Bound::Included(&r@.start)
327    }
328}
329
330pub open spec fn spec_range_inclusive_end_bound<T>(r: &RangeInclusive<T>) -> Bound<&T> {
331    if spec_range_inclusive_is_empty(r) {
332        spec_range_inclusive_unspecified_bounds(r).1
333    } else {
334        Bound::Included(&r@.end)
335    }
336}
337
338pub assume_specification<'s, T>[ <RangeInclusive<T> as RangeBounds<T>>::start_bound ](
339    range: &'s RangeInclusive<T>,
340) -> (result: Bound<&'s T>)
341    ensures
342        result == spec_range_inclusive_start_bound(range),
343;
344
345pub assume_specification<'s, T>[ <RangeInclusive<T> as RangeBounds<T>>::end_bound ](
346    range: &'s RangeInclusive<T>,
347) -> (result: Bound<&'s T>)
348    ensures
349        result == spec_range_inclusive_end_bound(range),
350;
351
352pub assume_specification<'s, T>[ <RangeToInclusive<T> as RangeBounds<T>>::start_bound ](
353    range: &'s RangeToInclusive<T>,
354) -> (result: Bound<&'s T>)
355    ensures
356        result == Bound::Unbounded,
357;
358
359pub assume_specification<'s, T>[ <RangeToInclusive<T> as RangeBounds<T>>::end_bound ](
360    range: &'s RangeToInclusive<T>,
361) -> (result: Bound<&'s T>)
362    ensures
363        result == Bound::Included(&range.end),
364;
365
366pub assume_specification<'s, T>[ <(Bound<T>, Bound<T>) as RangeBounds<T>>::start_bound ](
367    range: &'s (Bound<T>, Bound<T>),
368) -> (result: Bound<&'s T>)
369    ensures
370        result == bound_as_ref(&range.0),
371;
372
373pub assume_specification<'s, T>[ <(Bound<T>, Bound<T>) as RangeBounds<T>>::end_bound ](
374    range: &'s (Bound<T>, Bound<T>),
375) -> (result: Bound<&'s T>)
376    ensures
377        result == bound_as_ref(&range.1),
378;
379
380/// Specification for [`core::ops::RangeBounds`], exposing spec-mode models
381/// [`spec_start_bound`](RangeBoundsSpec::spec_start_bound) and
382/// [`spec_end_bound`](RangeBoundsSpec::spec_end_bound) of the trait's
383/// `start_bound`/`end_bound` methods. This mirrors std's normalization of an
384/// arbitrary range into a pair of bounds and is the model used by
385/// `<[T]>::copy_within` (see `vstd::std_specs::slice`). Implementations must
386/// return these spec bounds from `start_bound`/`end_bound`, since std's
387/// `copy_within` calls those methods.
388#[verifier::external_trait_specification]
389#[verifier::external_trait_extension(RangeBoundsSpec via RangeBoundsSpecImpl)]
390pub trait ExRangeBounds<T: ?Sized> {
391    type ExternalTraitSpecificationFor: RangeBounds<T>;
392
393    spec fn spec_start_bound(&self) -> Bound<&T>;
394
395    spec fn spec_end_bound(&self) -> Bound<&T>;
396
397    fn start_bound(&self) -> (r: Bound<&T>)
398        ensures
399            r == self.spec_start_bound(),
400    ;
401
402    fn end_bound(&self) -> (r: Bound<&T>)
403        ensures
404            r == self.spec_end_bound(),
405    ;
406}
407
408impl<T> RangeBoundsSpecImpl<T> for Range<T> {
409    open spec fn spec_start_bound(&self) -> Bound<&T> {
410        Bound::Included(&self.start)
411    }
412
413    open spec fn spec_end_bound(&self) -> Bound<&T> {
414        Bound::Excluded(&self.end)
415    }
416}
417
418impl<T: ?Sized> RangeBoundsSpecImpl<T> for RangeFull {
419    open spec fn spec_start_bound(&self) -> Bound<&T> {
420        Bound::Unbounded
421    }
422
423    open spec fn spec_end_bound(&self) -> Bound<&T> {
424        Bound::Unbounded
425    }
426}
427
428impl<T> RangeBoundsSpecImpl<T> for RangeFrom<T> {
429    open spec fn spec_start_bound(&self) -> Bound<&T> {
430        Bound::Included(&self.start)
431    }
432
433    open spec fn spec_end_bound(&self) -> Bound<&T> {
434        Bound::Unbounded
435    }
436}
437
438impl<T> RangeBoundsSpecImpl<T> for RangeTo<T> {
439    open spec fn spec_start_bound(&self) -> Bound<&T> {
440        Bound::Unbounded
441    }
442
443    open spec fn spec_end_bound(&self) -> Bound<&T> {
444        Bound::Excluded(&self.end)
445    }
446}
447
448impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<T> {
449    open spec fn spec_start_bound(&self) -> Bound<&T> {
450        spec_range_inclusive_start_bound(self)
451    }
452
453    open spec fn spec_end_bound(&self) -> Bound<&T> {
454        spec_range_inclusive_end_bound(self)
455    }
456}
457
458impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<T> {
459    open spec fn spec_start_bound(&self) -> Bound<&T> {
460        Bound::Unbounded
461    }
462
463    open spec fn spec_end_bound(&self) -> Bound<&T> {
464        Bound::Included(&self.end)
465    }
466}
467
468impl<T> RangeBoundsSpecImpl<T> for (Bound<T>, Bound<T>) {
469    open spec fn spec_start_bound(&self) -> Bound<&T> {
470        bound_as_ref(&self.0)
471    }
472
473    open spec fn spec_end_bound(&self) -> Bound<&T> {
474        bound_as_ref(&self.1)
475    }
476}
477
478impl<'a, T: ?Sized + 'a> RangeBoundsSpecImpl<T> for (Bound<&'a T>, Bound<&'a T>) {
479    open spec fn spec_start_bound(&self) -> Bound<&T> {
480        self.0
481    }
482
483    open spec fn spec_end_bound(&self) -> Bound<&T> {
484        self.1
485    }
486}
487
488impl<T> RangeBoundsSpecImpl<T> for RangeFrom<&T> {
489    open spec fn spec_start_bound(&self) -> Bound<&T> {
490        Bound::Included(self.start)
491    }
492
493    open spec fn spec_end_bound(&self) -> Bound<&T> {
494        Bound::Unbounded
495    }
496}
497
498impl<T> RangeBoundsSpecImpl<T> for RangeTo<&T> {
499    open spec fn spec_start_bound(&self) -> Bound<&T> {
500        Bound::Unbounded
501    }
502
503    open spec fn spec_end_bound(&self) -> Bound<&T> {
504        Bound::Excluded(self.end)
505    }
506}
507
508impl<T> RangeBoundsSpecImpl<T> for Range<&T> {
509    open spec fn spec_start_bound(&self) -> Bound<&T> {
510        Bound::Included(self.start)
511    }
512
513    open spec fn spec_end_bound(&self) -> Bound<&T> {
514        Bound::Excluded(self.end)
515    }
516}
517
518impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<&T> {
519    open spec fn spec_start_bound(&self) -> Bound<&T> {
520        if spec_range_inclusive_is_empty(self) {
521            spec_range_inclusive_unspecified_ref_bounds(self).0
522        } else {
523            Bound::Included(self@.start)
524        }
525    }
526
527    open spec fn spec_end_bound(&self) -> Bound<&T> {
528        if spec_range_inclusive_is_empty(self) {
529            spec_range_inclusive_unspecified_ref_bounds(self).1
530        } else {
531            Bound::Included(self@.end)
532        }
533    }
534}
535
536impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<&T> {
537    open spec fn spec_start_bound(&self) -> Bound<&T> {
538        Bound::Unbounded
539    }
540
541    open spec fn spec_end_bound(&self) -> Bound<&T> {
542        Bound::Included(self.end)
543    }
544}
545
546/// Normalized (inclusive) start index of `range`, matching std's
547/// `core::slice::range`: an inclusive bound `i` stays `i`, an exclusive bound
548/// `i` becomes `i + 1`, and an unbounded start is `0`.
549pub open spec fn slice_range_start<R: RangeBoundsSpec<usize>>(range: &R) -> int {
550    match range.spec_start_bound() {
551        Bound::Included(i) => *i as int,
552        Bound::Excluded(i) => (*i as int) + 1,
553        Bound::Unbounded => 0,
554    }
555}
556
557/// Normalized (exclusive) end index of a range over a sequence of length `len`,
558/// matching std's `core::slice::range`: an inclusive bound `i` becomes `i + 1`,
559/// an exclusive bound `i` stays `i`, and an unbounded end is `len`.
560pub open spec fn slice_range_end<R: RangeBoundsSpec<usize>>(range: &R, len: nat) -> int {
561    match range.spec_end_bound() {
562        Bound::Included(i) => (*i as int) + 1,
563        Bound::Excluded(i) => *i as int,
564        Bound::Unbounded => len as int,
565    }
566}
567
568/// Whether a range normalizes to `start <= end <= len`, i.e. the condition
569/// under which std's `core::slice::range` does not panic.
570pub open spec fn slice_range_valid<R: RangeBoundsSpec<usize>>(range: &R, len: nat) -> bool {
571    slice_range_start(range) <= slice_range_end(range, len) <= len
572}
573
574} // verus!
575macro_rules! step_specs {
576    ($t: ty, $axiom: ident, $step_axiom: ident) => {
577        verus! {
578        impl StepSpecImpl for $t {
579            open spec fn spec_is_lt(self, other: Self) -> bool {
580                self < other
581            }
582            open spec fn spec_steps_between(self, end: Self) -> Option<usize> {
583                let n = end - self;
584                if usize::MIN <= n <= usize::MAX {
585                    Some(n as usize)
586                } else {
587                    None
588                }
589            }
590            open spec fn spec_steps_between_int(self, end: Self) -> int {
591                end - self
592            }
593            open spec fn spec_forward_checked(self, count: usize) -> Option<Self> {
594                StepSpec::spec_forward_checked_int(self, count as int)
595            }
596            open spec fn spec_forward_checked_int(self, count: int) -> Option<Self> {
597                if self + count <= $t::MAX {
598                    Some((self + count) as $t)
599                } else {
600                    None
601                }
602            }
603            open spec fn spec_backward_checked(self, count: usize) -> Option<Self> {
604                StepSpec::spec_backward_checked_int(self, count as int)
605            }
606            open spec fn spec_backward_checked_int(self, count: int) -> Option<Self> {
607                if self - count >= $t::MIN {
608                    Some((self - count) as $t)
609                } else {
610                    None
611                }
612            }
613        }
614        pub broadcast proof fn $step_axiom()
615            ensures
616                #[trigger] obeys_range_step_spec::<$t>(),
617        {
618            admit();
619        }
620
621        // TODO: we might be able to make this generic over A: StepSpec
622        // once we settle on a way to connect std traits like Step with spec traits like StepSpec.
623        pub broadcast proof fn $axiom(range: Range<$t>)
624            ensures
625                StepSpec::spec_is_lt(range.start, range.end) ==>
626                    // TODO (not important): use new "matches ==>" syntax here
627                    (if let Some(n) = StepSpec::spec_forward_checked(range.start, 1) {
628                        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
629                    } else {
630                        true
631                    }),
632                !StepSpec::spec_is_lt(range.start, range.end) ==>
633                    #[trigger] spec_range_next(range) == (range, None::<$t>),
634        {
635            admit();
636        }
637        } // verus!
638    };
639}
640
641step_specs!(u8, axiom_spec_range_next_u8, axiom_u8_obeys_range_step_spec);
642step_specs!(u16, axiom_spec_range_next_u16, axiom_u16_obeys_range_step_spec);
643step_specs!(u32, axiom_spec_range_next_u32, axiom_u32_obeys_range_step_spec);
644step_specs!(u64, axiom_spec_range_next_u64, axiom_u64_obeys_range_step_spec);
645step_specs!(u128, axiom_spec_range_next_u128, axiom_u128_obeys_range_step_spec);
646step_specs!(usize, axiom_spec_range_next_usize, axiom_usize_obeys_range_step_spec);
647step_specs!(i8, axiom_spec_range_next_i8, axiom_i8_obeys_range_step_spec);
648step_specs!(i16, axiom_spec_range_next_i16, axiom_i16_obeys_range_step_spec);
649step_specs!(i32, axiom_spec_range_next_i32, axiom_i32_obeys_range_step_spec);
650step_specs!(i64, axiom_spec_range_next_i64, axiom_i64_obeys_range_step_spec);
651step_specs!(i128, axiom_spec_range_next_i128, axiom_i128_obeys_range_step_spec);
652step_specs!(isize, axiom_spec_range_next_isize, axiom_isize_obeys_range_step_spec);
653
654verus! {
655
656pub broadcast group group_range_axioms {
657    axiom_range_inclusive_out_of_order,
658    axiom_range_inclusive_empty_contains,
659    axiom_u8_obeys_range_step_spec,
660    axiom_u16_obeys_range_step_spec,
661    axiom_u32_obeys_range_step_spec,
662    axiom_u64_obeys_range_step_spec,
663    axiom_u128_obeys_range_step_spec,
664    axiom_usize_obeys_range_step_spec,
665    axiom_i8_obeys_range_step_spec,
666    axiom_i16_obeys_range_step_spec,
667    axiom_i32_obeys_range_step_spec,
668    axiom_i64_obeys_range_step_spec,
669    axiom_i128_obeys_range_step_spec,
670    axiom_isize_obeys_range_step_spec,
671    axiom_spec_range_next_u8,
672    axiom_spec_range_next_u16,
673    axiom_spec_range_next_u32,
674    axiom_spec_range_next_u64,
675    axiom_spec_range_next_u128,
676    axiom_spec_range_next_usize,
677    axiom_spec_range_next_i8,
678    axiom_spec_range_next_i16,
679    axiom_spec_range_next_i32,
680    axiom_spec_range_next_i64,
681    axiom_spec_range_next_i128,
682    axiom_spec_range_next_isize,
683}
684
685} // verus!
vstd/std_specs/range.rs

vstd/std_specs/
range.rs
