creusot_contracts/std/
range.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use std::range::{Range, RangeFrom, RangeInclusive, legacy};
4
5extern_spec! {
6    impl<T> From<Range<T>> for legacy::Range<T> {
7        #[erasure]
8        #[ensures(result == legacy::Range { start: value.start, end: value.end })]
9        fn from(value: Range<T>) -> Self {
10            legacy::Range { start: value.start, end: value.end }
11        }
12    }
13
14    impl<T> From<legacy::Range<T>> for Range<T> {
15        #[erasure]
16        #[ensures(result == Range { start: value.start, end: value.end })]
17        fn from(value: legacy::Range<T>) -> Self {
18            Range { start: value.start, end: value.end }
19        }
20    }
21
22    impl<T> From<RangeFrom<T>> for legacy::RangeFrom<T> {
23        #[erasure]
24        #[ensures(result == legacy::RangeFrom { start: value.start })]
25        fn from(value: RangeFrom<T>) -> Self {
26            legacy::RangeFrom { start: value.start }
27        }
28    }
29
30    impl<T> From<legacy::RangeFrom<T>> for RangeFrom<T> {
31        #[erasure]
32        #[ensures(result == RangeFrom { start: value.start })]
33        fn from(value: legacy::RangeFrom<T>) -> Self {
34            RangeFrom { start: value.start }
35        }
36    }
37
38    impl<T> From<RangeInclusive<T>> for legacy::RangeInclusive<T> {
39        #[erasure]
40        #[ensures(result.start_log() == value.start)]
41        #[ensures(result.end_log() == value.last)]
42        #[ensures(value.start.deep_model() <= value.last.deep_model() ==> !result.is_empty_log())]
43        fn from(value: RangeInclusive<T>) -> Self where T: DeepModel<DeepModelTy: OrdLogic> {
44            legacy::RangeInclusive::new(value.start, value.last)
45        }
46    }
47
48    // Note: the other impl `From<legacy::RangeInclusive<T>> for range::RangeInclusive<T>` is partial...
49}
creusot_contracts/std/range.rs

creusot_contracts/std/
range.rs
