vstd/std_specs/
range.rs

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

vstd/std_specs/
range.rs
