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
91pub assume_specification<Idx>[ RangeInclusive::<Idx>::new ](start: Idx, end: Idx) -> (ret:
92    core::ops::RangeInclusive<Idx>)
93    ensures
94        ret@ == (RangeInclusiveView { start, end, exhausted: false }),
95;
96
97impl<A: core::iter::Step> super::iter::IteratorSpecImpl for Range<A> {
98    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
99        true
100    }
101
102    open spec fn remaining(&self) -> Seq<Self::Item> {
103        let steps = self.start.spec_steps_between_int(self.end);
104        let len = if steps > 0 {
105            steps
106        } else {
107            0
108        };
109        Seq::new(len as nat, |i: int| self.start.spec_forward_checked_int(i).unwrap())
110    }
111
112    uninterp spec fn will_return_none(&self) -> bool;
113
114    open spec fn decrease(&self) -> Option<nat> {
115        Some(self.start.spec_steps_between_int(self.end) as nat)
116    }
117
118    open spec fn peek(&self, index: int) -> Option<Self::Item> {
119        //Some(self.start.spec_forward_checked_int(index).unwrap())
120        if 0 <= index <= self.start.spec_steps_between_int(self.end) {
121            Some(self.start.spec_forward_checked_int(index).unwrap())
122        } else {
123            None
124        }
125    }
126}
127
128impl<A: core::iter::Step> super::iter::IteratorSpecImpl for RangeInclusive<A> {
129    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
130        true
131    }
132
133    open spec fn remaining(&self) -> Seq<Self::Item> {
134        Seq::new(
135            (self@.start.spec_steps_between_int(self@.end) + 1) as nat,
136            |i: int| self@.start.spec_forward_checked_int(i).unwrap(),
137        )
138    }
139
140    uninterp spec fn will_return_none(&self) -> bool;
141
142    open spec fn decrease(&self) -> Option<nat> {
143        Some((self@.start.spec_steps_between_int(self@.end) + 1) as nat)
144    }
145
146    open spec fn peek(&self, index: int) -> Option<Self::Item> {
147        if 0 <= index <= self@.start.spec_steps_between_int(self@.end) + 1 {
148            Some(self@.start.spec_forward_checked_int(index).unwrap())
149        } else {
150            None
151        }
152    }
153}
154
155pub assume_specification<A: core::iter::Step>[ <Range<A> as Iterator>::next ](
156    range: &mut Range<A>,
157) -> (r: Option<A>)
158    ensures
159        (*final(range), r) == spec_range_next(*old(range)),
160;
161
162/// Spec model of [`core::ops::Bound`], used by [`RangeBoundsSpec`] to describe
163/// the start and end bounds of a range. See [`spec_bound`] for the connection
164/// to `Bound` values.
165pub enum SpecBound<T> {
166    Included(T),
167    Excluded(T),
168    Unbounded,
169}
170
171/// Spec model of a [`core::ops::Bound`] value as a [`SpecBound`].
172pub open spec fn spec_bound<T>(bound: Bound<T>) -> SpecBound<T> {
173    match bound {
174        Bound::Included(value) => SpecBound::Included(value),
175        Bound::Excluded(value) => SpecBound::Excluded(value),
176        Bound::Unbounded => SpecBound::Unbounded,
177    }
178}
179
180/// Spec model of a borrowed [`core::ops::Bound`] value as a [`SpecBound`].
181pub open spec fn spec_bound_ref<'a, T>(bound: &'a Bound<T>) -> SpecBound<&'a T> {
182    match bound {
183        Bound::Included(value) => SpecBound::Included(value),
184        Bound::Excluded(value) => SpecBound::Excluded(value),
185        Bound::Unbounded => SpecBound::Unbounded,
186    }
187}
188
189#[verifier::external_type_specification]
190pub struct ExBound<T>(Bound<T>);
191
192#[verifier::external_type_specification]
193pub struct ExRangeFull(RangeFull);
194
195#[verifier::external_type_specification]
196#[verifier::reject_recursive_types(Idx)]
197pub struct ExRangeFrom<Idx>(RangeFrom<Idx>);
198
199#[verifier::external_type_specification]
200#[verifier::reject_recursive_types(Idx)]
201pub struct ExRangeTo<Idx>(RangeTo<Idx>);
202
203#[verifier::external_type_specification]
204#[verifier::reject_recursive_types(Idx)]
205pub struct ExRangeToInclusive<Idx>(RangeToInclusive<Idx>);
206
207// Per-type specifications for `RangeBounds::start_bound`/`end_bound`, so these
208// methods can also be called directly in exec code (not just via the spec-mode
209// models above). Each spec agrees with the corresponding `RangeBoundsSpecImpl`.
210pub assume_specification<'s, T>[ <Range<T> as RangeBounds<T>>::start_bound ](
211    range: &'s Range<T>,
212) -> (result: Bound<&'s T>)
213    ensures
214        spec_bound(result) == SpecBound::Included(&range.start),
215;
216
217pub assume_specification<'s, T>[ <Range<T> as RangeBounds<T>>::end_bound ](
218    range: &'s Range<T>,
219) -> (result: Bound<&'s T>)
220    ensures
221        spec_bound(result) == SpecBound::Excluded(&range.end),
222;
223
224pub assume_specification<'s, T: ?Sized>[ <RangeFull as RangeBounds<T>>::start_bound ](
225    range: &'s RangeFull,
226) -> (result: Bound<&'s T>)
227    ensures
228        spec_bound(result) == SpecBound::Unbounded,
229;
230
231pub assume_specification<'s, T: ?Sized>[ <RangeFull as RangeBounds<T>>::end_bound ](
232    range: &'s RangeFull,
233) -> (result: Bound<&'s T>)
234    ensures
235        spec_bound(result) == SpecBound::Unbounded,
236;
237
238pub assume_specification<'s, T>[ <RangeFrom<T> as RangeBounds<T>>::start_bound ](
239    range: &'s RangeFrom<T>,
240) -> (result: Bound<&'s T>)
241    ensures
242        spec_bound(result) == SpecBound::Included(&range.start),
243;
244
245pub assume_specification<'s, T>[ <RangeFrom<T> as RangeBounds<T>>::end_bound ](
246    range: &'s RangeFrom<T>,
247) -> (result: Bound<&'s T>)
248    ensures
249        spec_bound(result) == SpecBound::Unbounded,
250;
251
252pub assume_specification<'s, T>[ <RangeTo<T> as RangeBounds<T>>::start_bound ](
253    range: &'s RangeTo<T>,
254) -> (result: Bound<&'s T>)
255    ensures
256        spec_bound(result) == SpecBound::Unbounded,
257;
258
259pub assume_specification<'s, T>[ <RangeTo<T> as RangeBounds<T>>::end_bound ](
260    range: &'s RangeTo<T>,
261) -> (result: Bound<&'s T>)
262    ensures
263        spec_bound(result) == SpecBound::Excluded(&range.end),
264;
265
266pub assume_specification<'s, T>[ <RangeInclusive<T> as RangeBounds<T>>::start_bound ](
267    range: &'s RangeInclusive<T>,
268) -> (result: Bound<&'s T>)
269    ensures
270        spec_bound(result) == SpecBound::Included(&range@.start),
271;
272
273pub assume_specification<'s, T>[ <RangeInclusive<T> as RangeBounds<T>>::end_bound ](
274    range: &'s RangeInclusive<T>,
275) -> (result: Bound<&'s T>)
276    ensures
277        spec_bound(result) == SpecBound::Included(&range@.end),
278;
279
280pub assume_specification<'s, T>[ <RangeToInclusive<T> as RangeBounds<T>>::start_bound ](
281    range: &'s RangeToInclusive<T>,
282) -> (result: Bound<&'s T>)
283    ensures
284        spec_bound(result) == SpecBound::Unbounded,
285;
286
287pub assume_specification<'s, T>[ <RangeToInclusive<T> as RangeBounds<T>>::end_bound ](
288    range: &'s RangeToInclusive<T>,
289) -> (result: Bound<&'s T>)
290    ensures
291        spec_bound(result) == SpecBound::Included(&range.end),
292;
293
294pub assume_specification<'s, T>[ <(Bound<T>, Bound<T>) as RangeBounds<T>>::start_bound ](
295    range: &'s (Bound<T>, Bound<T>),
296) -> (result: Bound<&'s T>)
297    ensures
298        spec_bound(result) == spec_bound_ref(&range.0),
299;
300
301pub assume_specification<'s, T>[ <(Bound<T>, Bound<T>) as RangeBounds<T>>::end_bound ](
302    range: &'s (Bound<T>, Bound<T>),
303) -> (result: Bound<&'s T>)
304    ensures
305        spec_bound(result) == spec_bound_ref(&range.1),
306;
307
308/// Specification for [`core::ops::RangeBounds`], exposing spec-mode models
309/// [`spec_start_bound`](RangeBoundsSpec::spec_start_bound) and
310/// [`spec_end_bound`](RangeBoundsSpec::spec_end_bound) of the trait's
311/// `start_bound`/`end_bound` methods. This mirrors std's normalization of an
312/// arbitrary range into a pair of bounds and is the model used by
313/// `<[T]>::copy_within` (see `vstd::std_specs::slice`).
314#[verifier::external_trait_specification]
315#[verifier::external_trait_extension(RangeBoundsSpec via RangeBoundsSpecImpl)]
316pub trait ExRangeBounds<T: ?Sized> {
317    type ExternalTraitSpecificationFor: RangeBounds<T>;
318
319    spec fn spec_start_bound(&self) -> SpecBound<&T>;
320
321    spec fn spec_end_bound(&self) -> SpecBound<&T>;
322
323    fn start_bound(&self) -> Bound<&T>;
324
325    fn end_bound(&self) -> Bound<&T>;
326}
327
328impl<T> RangeBoundsSpecImpl<T> for Range<T> {
329    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
330        SpecBound::Included(&self.start)
331    }
332
333    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
334        SpecBound::Excluded(&self.end)
335    }
336}
337
338impl<T: ?Sized> RangeBoundsSpecImpl<T> for RangeFull {
339    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
340        SpecBound::Unbounded
341    }
342
343    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
344        SpecBound::Unbounded
345    }
346}
347
348impl<T> RangeBoundsSpecImpl<T> for RangeFrom<T> {
349    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
350        SpecBound::Included(&self.start)
351    }
352
353    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
354        SpecBound::Unbounded
355    }
356}
357
358impl<T> RangeBoundsSpecImpl<T> for RangeTo<T> {
359    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
360        SpecBound::Unbounded
361    }
362
363    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
364        SpecBound::Excluded(&self.end)
365    }
366}
367
368impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<T> {
369    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
370        SpecBound::Included(&self@.start)
371    }
372
373    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
374        SpecBound::Included(&self@.end)
375    }
376}
377
378impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<T> {
379    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
380        SpecBound::Unbounded
381    }
382
383    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
384        SpecBound::Included(&self.end)
385    }
386}
387
388impl<T> RangeBoundsSpecImpl<T> for (Bound<T>, Bound<T>) {
389    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
390        spec_bound_ref(&self.0)
391    }
392
393    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
394        spec_bound_ref(&self.1)
395    }
396}
397
398impl<'a, T: ?Sized + 'a> RangeBoundsSpecImpl<T> for (Bound<&'a T>, Bound<&'a T>) {
399    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
400        match self.0 {
401            Bound::Included(start) => SpecBound::Included(start),
402            Bound::Excluded(start) => SpecBound::Excluded(start),
403            Bound::Unbounded => SpecBound::Unbounded,
404        }
405    }
406
407    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
408        match self.1 {
409            Bound::Included(end) => SpecBound::Included(end),
410            Bound::Excluded(end) => SpecBound::Excluded(end),
411            Bound::Unbounded => SpecBound::Unbounded,
412        }
413    }
414}
415
416impl<T> RangeBoundsSpecImpl<T> for RangeFrom<&T> {
417    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
418        SpecBound::Included(self.start)
419    }
420
421    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
422        SpecBound::Unbounded
423    }
424}
425
426impl<T> RangeBoundsSpecImpl<T> for RangeTo<&T> {
427    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
428        SpecBound::Unbounded
429    }
430
431    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
432        SpecBound::Excluded(self.end)
433    }
434}
435
436impl<T> RangeBoundsSpecImpl<T> for Range<&T> {
437    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
438        SpecBound::Included(self.start)
439    }
440
441    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
442        SpecBound::Excluded(self.end)
443    }
444}
445
446impl<T> RangeBoundsSpecImpl<T> for RangeInclusive<&T> {
447    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
448        SpecBound::Included(self@.start)
449    }
450
451    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
452        SpecBound::Included(self@.end)
453    }
454}
455
456impl<T> RangeBoundsSpecImpl<T> for RangeToInclusive<&T> {
457    open spec fn spec_start_bound(&self) -> SpecBound<&T> {
458        SpecBound::Unbounded
459    }
460
461    open spec fn spec_end_bound(&self) -> SpecBound<&T> {
462        SpecBound::Included(self.end)
463    }
464}
465
466/// Normalized (inclusive) start index of `range`, matching std's
467/// `core::slice::range`: an inclusive bound `i` stays `i`, an exclusive bound
468/// `i` becomes `i + 1`, and an unbounded start is `0`.
469pub open spec fn slice_range_start<R: RangeBoundsSpec<usize>>(range: &R) -> int {
470    match range.spec_start_bound() {
471        SpecBound::Included(i) => *i as int,
472        SpecBound::Excluded(i) => (*i as int) + 1,
473        SpecBound::Unbounded => 0,
474    }
475}
476
477/// Normalized (exclusive) end index of a range over a sequence of length `len`,
478/// matching std's `core::slice::range`: an inclusive bound `i` becomes `i + 1`,
479/// an exclusive bound `i` stays `i`, and an unbounded end is `len`.
480pub open spec fn slice_range_end<R: RangeBoundsSpec<usize>>(range: &R, len: nat) -> int {
481    match range.spec_end_bound() {
482        SpecBound::Included(i) => (*i as int) + 1,
483        SpecBound::Excluded(i) => *i as int,
484        SpecBound::Unbounded => len as int,
485    }
486}
487
488/// Whether a range normalizes to `start <= end <= len`, i.e. the condition
489/// under which std's `core::slice::range` does not panic.
490pub open spec fn slice_range_valid<R: RangeBoundsSpec<usize>>(range: &R, len: nat) -> bool {
491    slice_range_start(range) <= slice_range_end(range, len) <= len
492}
493
494} // verus!
495macro_rules! step_specs {
496    ($t: ty, $axiom: ident) => {
497        verus! {
498        impl StepSpecImpl for $t {
499            open spec fn spec_is_lt(self, other: Self) -> bool {
500                self < other
501            }
502            open spec fn spec_steps_between(self, end: Self) -> Option<usize> {
503                let n = end - self;
504                if usize::MIN <= n <= usize::MAX {
505                    Some(n as usize)
506                } else {
507                    None
508                }
509            }
510            open spec fn spec_steps_between_int(self, end: Self) -> int {
511                end - self
512            }
513            open spec fn spec_forward_checked(self, count: usize) -> Option<Self> {
514                StepSpec::spec_forward_checked_int(self, count as int)
515            }
516            open spec fn spec_forward_checked_int(self, count: int) -> Option<Self> {
517                if self + count <= $t::MAX {
518                    Some((self + count) as $t)
519                } else {
520                    None
521                }
522            }
523            open spec fn spec_backward_checked(self, count: usize) -> Option<Self> {
524                StepSpec::spec_backward_checked_int(self, count as int)
525            }
526            open spec fn spec_backward_checked_int(self, count: int) -> Option<Self> {
527                if self - count >= $t::MIN {
528                    Some((self - count) as $t)
529                } else {
530                    None
531                }
532            }
533        }
534        // TODO: we might be able to make this generic over A: StepSpec
535        // once we settle on a way to connect std traits like Step with spec traits like StepSpec.
536        pub broadcast proof fn $axiom(range: Range<$t>)
537            ensures
538                StepSpec::spec_is_lt(range.start, range.end) ==>
539                    // TODO (not important): use new "matches ==>" syntax here
540                    (if let Some(n) = StepSpec::spec_forward_checked(range.start, 1) {
541                        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
542                    } else {
543                        true
544                    }),
545                !StepSpec::spec_is_lt(range.start, range.end) ==>
546                    #[trigger] spec_range_next(range) == (range, None::<$t>),
547        {
548            admit();
549        }
550        } // verus!
551    };
552}
553
554step_specs!(u8, axiom_spec_range_next_u8);
555step_specs!(u16, axiom_spec_range_next_u16);
556step_specs!(u32, axiom_spec_range_next_u32);
557step_specs!(u64, axiom_spec_range_next_u64);
558step_specs!(u128, axiom_spec_range_next_u128);
559step_specs!(usize, axiom_spec_range_next_usize);
560step_specs!(i8, axiom_spec_range_next_i8);
561step_specs!(i16, axiom_spec_range_next_i16);
562step_specs!(i32, axiom_spec_range_next_i32);
563step_specs!(i64, axiom_spec_range_next_i64);
564step_specs!(i128, axiom_spec_range_next_i128);
565step_specs!(isize, axiom_spec_range_next_isize);
566
567verus! {
568
569pub broadcast group group_range_axioms {
570    axiom_spec_range_next_u8,
571    axiom_spec_range_next_u16,
572    axiom_spec_range_next_u32,
573    axiom_spec_range_next_u64,
574    axiom_spec_range_next_u128,
575    axiom_spec_range_next_usize,
576    axiom_spec_range_next_i8,
577    axiom_spec_range_next_i16,
578    axiom_spec_range_next_i32,
579    axiom_spec_range_next_i64,
580    axiom_spec_range_next_i128,
581    axiom_spec_range_next_isize,
582}
583
584} // verus!
vstd/std_specs/range.rs

vstd/std_specs/
range.rs
