Trait SliceIndexSpecImpl 

pub trait SliceIndexSpecImpl<T>: SliceIndex<T>
where
    T: ?Sized,
{
    // Required methods
    exec fn in_bounds(&self, slice: &T) -> bool;
    exec fn index_postcondition(&self, slice: &T, r: &Self::Output) -> bool;
    exec fn index_mut_postcondition(
        &self,
        old_slice: &T,
        final_slice: &T,
        immediate_output: &Self::Output,
        final_output: &Self::Output,
    ) -> bool;
}

Required Methods

exec fn in_bounds(&self, slice: &T) -> bool

exec fn index_postcondition(&self, slice: &T, r: &Self::Output) -> bool

exec fn index_mut_postcondition( &self, old_slice: &T, final_slice: &T, immediate_output: &Self::Output, final_output: &Self::Output, ) -> bool

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl SliceIndexSpecImpl<str> for (Bound<usize>, Bound<usize>)

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl SliceIndexSpecImpl<str> for Range<usize>

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl SliceIndexSpecImpl<str> for RangeFrom<usize>

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl SliceIndexSpecImpl<str> for RangeFull

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl SliceIndexSpecImpl<str> for RangeInclusive<usize>

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        spec_range_inclusive_unspecified_str_in_bounds(self, s)
    } else {
        str_slice_in_bounds(self, s)
    }
}

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        r.spec_bytes().len() == 0
    } else {
        str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes())
    }
}

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        &&& immediate_output.spec_bytes().len() == 0
        &&& final_slice.spec_bytes() == old_slice.spec_bytes()

    } else {
        str_slice_index_mut_postcondition(
            self,
            old_slice.spec_bytes(),
            final_slice.spec_bytes(),
            immediate_output.spec_bytes(),
            final_output.spec_bytes(),
        )
    }
}

impl SliceIndexSpecImpl<str> for RangeTo<usize>

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl SliceIndexSpecImpl<str> for RangeToInclusive<usize>

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn in_bounds(&self, s: &str) -> bool

{ str_slice_in_bounds(self, s) }

open spec fn index_postcondition(&self, s: &str, r: &str) -> bool

{ str_slice_index_postcondition(self, s.spec_bytes(), r.spec_bytes()) }

open spec fn index_mut_postcondition( &self, old_slice: &str, final_slice: &str, immediate_output: &str, final_output: &str, ) -> bool

{
    str_slice_index_mut_postcondition(
        self,
        old_slice.spec_bytes(),
        final_slice.spec_bytes(),
        immediate_output.spec_bytes(),
        final_output.spec_bytes(),
    )
}

impl<T> SliceIndexSpecImpl<[T]> for Range<usize>

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ generic_slice_in_bounds(self, slice@) }

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{ generic_slice_index_postcondition(self, slice@, r@) }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    generic_slice_index_mut_postcondition(
        self,
        old_slice@,
        final_slice@,
        immediate_output@,
        final_output@,
    )
}

impl<T> SliceIndexSpecImpl<[T]> for RangeFrom<usize>

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ generic_slice_in_bounds(self, slice@) }

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{ generic_slice_index_postcondition(self, slice@, r@) }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    generic_slice_index_mut_postcondition(
        self,
        old_slice@,
        final_slice@,
        immediate_output@,
        final_output@,
    )
}

impl<T> SliceIndexSpecImpl<[T]> for RangeFull

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ generic_slice_in_bounds(self, slice@) }

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{ generic_slice_index_postcondition(self, slice@, r@) }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    generic_slice_index_mut_postcondition(
        self,
        old_slice@,
        final_slice@,
        immediate_output@,
        final_output@,
    )
}

impl<T> SliceIndexSpecImpl<[T]> for RangeInclusive<usize>

open spec fn in_bounds(&self, slice: &[T]) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        spec_range_inclusive_unspecified_slice_in_bounds(self, slice)
    } else {
        generic_slice_in_bounds(self, slice@)
    }
}

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        r@.len() == 0
    } else {
        generic_slice_index_postcondition(self, slice@, r@)
    }
}

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    if spec_range_inclusive_is_empty(self) {
        &&& immediate_output@.len() == 0
        &&& final_slice@ == old_slice@

    } else {
        generic_slice_index_mut_postcondition(
            self,
            old_slice@,
            final_slice@,
            immediate_output@,
            final_output@,
        )
    }
}

impl<T> SliceIndexSpecImpl<[T]> for RangeTo<usize>

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ generic_slice_in_bounds(self, slice@) }

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{ generic_slice_index_postcondition(self, slice@, r@) }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    generic_slice_index_mut_postcondition(
        self,
        old_slice@,
        final_slice@,
        immediate_output@,
        final_output@,
    )
}

impl<T> SliceIndexSpecImpl<[T]> for RangeToInclusive<usize>

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ generic_slice_in_bounds(self, slice@) }

open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool

{ generic_slice_index_postcondition(self, slice@, r@) }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T], ) -> bool

{
    generic_slice_index_mut_postcondition(
        self,
        old_slice@,
        final_slice@,
        immediate_output@,
        final_output@,
    )
}

impl<T> SliceIndexSpecImpl<[T]> for usize

open spec fn in_bounds(&self, slice: &[T]) -> bool

{ *self < slice@.len() }

open spec fn index_postcondition(&self, slice: &[T], r: &T) -> bool

{ r == slice@[self as int] }

open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &T, final_output: &T, ) -> bool

{
    &&& *immediate_output == old_slice@[*self as int]
    &&& final_slice@ == old_slice@.update(*self as int, *final_output)

}

Implementors