vstd_extra/external/
slice.rs

1use core::ops::Range;
2use vstd::prelude::*;
3
4verus! {
5
6#[verifier::when_used_as_spec(as_ptr_spec)]
7pub assume_specification<T>[ <[T]>::as_ptr ](s: &[T]) -> (r: *const T)
8    ensures
9        r == as_ptr_spec(s),
10;
11
12pub uninterp spec fn as_ptr_spec<T>(s: &[T]) -> *const T;
13
14pub uninterp spec fn as_mut_ptr_spec<T>(s: &mut [T]) -> *mut T;
15
16pub assume_specification<T>[ <[T]>::as_mut_ptr ](s: &mut [T]) -> (r: *mut T)
17    ensures
18        r == as_mut_ptr_spec(s),
19;
20
21/// AXIOM: A slice's one-past-the-end byte address fits in `usize`.
22///
23/// Rust guarantees that any valid slice's memory range lies within the
24/// addressable address space, so `as_ptr(s) as usize + s.len() * size_of::<T>()`
25/// never overflows. We package this as a `usize`-level fact for `T = u8` (the
26/// common case for byte-slice plumbing); other element types can use it after
27/// multiplying by `size_of::<T>()`.
28pub broadcast axiom fn axiom_slice_addr_no_overflow(s: &[u8])
29    ensures
30        #[trigger] (as_ptr_spec(s) as usize) + s.len() <= usize::MAX,
31;
32
33/// Spec for `core::slice::from_raw_parts`. We promise only that the resulting
34/// slice has the requested length; soundness for the memory aliased lives in
35/// the `unsafe` contract upheld by the caller.
36pub assume_specification<'a, T>[ core::slice::from_raw_parts::<'a, T> ](
37    data: *const T,
38    len: usize,
39) -> (ret: &'a [T])
40    ensures
41        ret.len() == len,
42;
43
44/// Spec for `core::slice::from_raw_parts_mut`. As above.
45pub assume_specification<'a, T>[ core::slice::from_raw_parts_mut::<'a, T> ](
46    data: *mut T,
47    len: usize,
48) -> (ret: &'a mut [T])
49    ensures
50        ret.len() == len,
51;
52
53} // verus!
vstd_extra/external/slice.rs

vstd_extra/external/
slice.rs
