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

vstd/std_specs/
range.rs
