Function str_slice_in_bounds 

pub open spec fn str_slice_in_bounds<R: RangeBoundsSpec<usize>>(
    range: &R,
    s: &str,
) -> bool

{
    &&& slice_range_valid(range, s.spec_bytes().len())
    &&& is_char_boundary(s.spec_bytes(), slice_range_start(range))
    &&& is_char_boundary(s.spec_bytes(), slice_range_end(range, s.spec_bytes().len()))

}