Add slice ASCII and iterator specifications

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 37c58501-5f9f-4a00-b559-69d47c22f399

Author: Ubuntu

source/vstd/std_specs/slice.rs

@@ -7,7 +7,11 @@ use super::range::{slice_range_end, slice_range_start, slice_range_valid};
 use core::ops::{
     Index, IndexMut, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,
 };
-use core::slice::{Iter, SliceIndex};
+use core::slice::{
+    ChunksExact, ChunksExactMut, EscapeAscii, Iter, IterMut, RChunksExact, RChunksExactMut,
+    SliceIndex, Windows,
+};
+use core::str::Utf8Chunks;
 
 use verus as verus_;
 
@@ -408,6 +412,314 @@ pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy
         ),
 ;
 
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExIterMut<'a, T: 'a>(IterMut<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExChunksExact<'a, T: 'a>(ChunksExact<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExChunksExactMut<'a, T: 'a>(ChunksExactMut<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExRChunksExact<'a, T: 'a>(RChunksExact<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExRChunksExactMut<'a, T: 'a>(RChunksExactMut<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExWindows<'a, T: 'a>(Windows<'a, T>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExUtf8Chunks<'a>(Utf8Chunks<'a>);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExEscapeAscii<'a>(EscapeAscii<'a>);
+
+pub ghost struct SliceIteratorView<T> {
+    pub source: Seq<T>,
+    pub remaining: Seq<T>,
+    pub yielded_prefix: Seq<T>,
+    pub remainder: Seq<T>,
+    pub chunk_size: int,
+    pub reverse: bool,
+}
+
+pub uninterp spec fn slice_iterator_view<I, T>(iter: I) -> SliceIteratorView<T>;
+
+pub open spec fn slice_iterator_well_formed<T>(view: SliceIteratorView<T>) -> bool {
+    0 <= view.chunk_size && view.remainder.len() <= view.source.len()
+}
+
+pub broadcast axiom fn axiom_slice_iterator_view_well_formed<I, T>(iter: I)
+    ensures
+        slice_iterator_well_formed(#[trigger] slice_iterator_view::<I, T>(iter)),
+;
+
+pub open spec fn utf8_chunk_partition<I>(iter: I, source: Seq<u8>) -> bool {
+    let view = slice_iterator_view::<I, u8>(iter);
+    slice_iterator_well_formed(view)
+        && view.source == source
+        && view.remaining == source
+        && view.yielded_prefix == Seq::empty()
+        && view.remainder == Seq::empty()
+        && view.chunk_size == 0
+        && !view.reverse
+}
+
+pub open spec fn ascii_is_uppercase(byte: u8) -> bool {
+    0x41 <= (byte as int) && (byte as int) <= 0x5a
+}
+
+pub open spec fn ascii_is_lowercase(byte: u8) -> bool {
+    0x61 <= (byte as int) && (byte as int) <= 0x7a
+}
+
+pub open spec fn ascii_lower_byte(byte: u8) -> u8 {
+    if ascii_is_uppercase(byte) {
+        ((byte as int) + 0x20) as u8
+    } else {
+        byte
+    }
+}
+
+pub open spec fn ascii_upper_byte(byte: u8) -> u8 {
+    if ascii_is_lowercase(byte) {
+        ((byte as int) - 0x20) as u8
+    } else {
+        byte
+    }
+}
+
+pub open spec fn ascii_is_whitespace(byte: u8) -> bool {
+    byte == 0x09u8
+        || byte == 0x0au8
+        || byte == 0x0cu8
+        || byte == 0x0du8
+        || byte == 0x20u8
+}
+
+pub open spec fn ascii_lower_seq(seq: Seq<u8>) -> Seq<u8> {
+    Seq::new(seq.len(), |i: int| ascii_lower_byte(seq[i]))
+}
+
+pub open spec fn ascii_upper_seq(seq: Seq<u8>) -> Seq<u8> {
+    Seq::new(seq.len(), |i: int| ascii_upper_byte(seq[i]))
+}
+
+pub open spec fn ascii_eq_ignore_case(left: Seq<u8>, right: Seq<u8>) -> bool {
+    left.len() == right.len()
+        && forall|i: int| 0 <= i < left.len()
+            ==> ascii_lower_byte(left[i]) == ascii_lower_byte(right[i])
+}
+
+pub open spec fn ascii_trim_start_boundary(seq: Seq<u8>, i: int) -> bool {
+    0 <= i <= seq.len()
+        && (forall|j: int| 0 <= j < i ==> #[trigger] ascii_is_whitespace(seq[j]))
+        && (i < seq.len() ==> !ascii_is_whitespace(seq[i]))
+}
+
+pub open spec fn ascii_trim_end_boundary(seq: Seq<u8>, i: int) -> bool {
+    0 <= i <= seq.len()
+        && (forall|j: int| i <= j < seq.len() ==> #[trigger] ascii_is_whitespace(seq[j]))
+        && (0 < i ==> !ascii_is_whitespace(seq[i - 1]))
+}
+
+pub open spec fn ascii_trim_start_index(seq: Seq<u8>) -> int {
+    choose|i: int| #[trigger] ascii_trim_start_boundary(seq, i)
+}
+
+pub open spec fn ascii_trim_end_index(seq: Seq<u8>) -> int {
+    choose|i: int| #[trigger] ascii_trim_end_boundary(seq, i)
+}
+
+pub open spec fn ascii_trim_start_result(seq: Seq<u8>, ret: &[u8]) -> bool {
+    0 <= ascii_trim_start_index(seq) <= seq.len()
+        && ret@ == seq.subrange(ascii_trim_start_index(seq), seq.len() as int)
+        && (forall|i: int| 0 <= i < ascii_trim_start_index(seq)
+            ==> ascii_is_whitespace(seq[i]))
+        && (ascii_trim_start_index(seq) < seq.len()
+            ==> !ascii_is_whitespace(seq[ascii_trim_start_index(seq)]))
+}
+
+pub open spec fn ascii_trim_end_result(seq: Seq<u8>, ret: &[u8]) -> bool {
+    0 <= ascii_trim_end_index(seq) <= seq.len()
+        && ret@ == seq.subrange(0, ascii_trim_end_index(seq))
+        && (forall|i: int| ascii_trim_end_index(seq) <= i < seq.len()
+            ==> ascii_is_whitespace(seq[i]))
+        && (0 < ascii_trim_end_index(seq)
+            ==> !ascii_is_whitespace(seq[ascii_trim_end_index(seq) - 1]))
+}
+
+pub open spec fn ascii_trim_source_body_result(seq: Seq<u8>, ret: &[u8]) -> bool {
+    let start = ascii_trim_start_index(seq);
+    let after_start = seq.subrange(start, seq.len() as int);
+    let end = ascii_trim_end_index(after_start);
+    0 <= start <= seq.len()
+        && 0 <= end <= after_start.len()
+        && ret@ == seq.subrange(start, start + end)
+        && (forall|i: int| 0 <= i < start ==> ascii_is_whitespace(seq[i]))
+        && (forall|i: int| start + end <= i < seq.len() ==> ascii_is_whitespace(seq[i]))
+}
+
+pub open spec fn ascii_lower_hex_digit(nibble: int) -> u8
+    recommends
+        0 <= nibble < 16,
+{
+    if nibble < 10 {
+        (0x30 + nibble) as u8
+    } else {
+        (0x61 + (nibble - 10)) as u8
+    }
+}
+
+pub open spec fn ascii_escape_byte(byte: u8) -> Seq<u8> {
+    if byte == 0x09u8 {
+        seq![0x5cu8, 0x74u8]
+    } else if byte == 0x0du8 {
+        seq![0x5cu8, 0x72u8]
+    } else if byte == 0x0au8 {
+        seq![0x5cu8, 0x6eu8]
+    } else if byte == 0x27u8 {
+        seq![0x5cu8, 0x27u8]
+    } else if byte == 0x22u8 {
+        seq![0x5cu8, 0x22u8]
+    } else if byte == 0x5cu8 {
+        seq![0x5cu8, 0x5cu8]
+    } else if 0x20 <= (byte as int) && (byte as int) <= 0x7e {
+        seq![byte]
+    } else {
+        seq![
+            0x5cu8,
+            0x78u8,
+            ascii_lower_hex_digit((byte as int) / 16),
+            ascii_lower_hex_digit((byte as int) % 16),
+        ]
+    }
+}
+
+pub open spec fn ascii_escape_seq(seq: Seq<u8>) -> Seq<u8> {
+    seq.flat_map(|byte: u8| ascii_escape_byte(byte))
+}
+
+pub assume_specification<'a, T>[ <[T]>::iter_mut ](
+    slice: &'a mut [T],
+) -> (iter: IterMut<'a, T>)
+    ensures
+        slice_iterator_view::<IterMut<'a, T>, T>(iter).source == old(slice)@,
+        slice_iterator_view::<IterMut<'a, T>, T>(iter).remaining == old(slice)@,
+        final(slice)@ == old(slice)@,
+;
+
+pub assume_specification<'a, T>[ <[T]>::windows ](
+    slice: &'a [T],
+    size: usize,
+) -> (iter: Windows<'a, T>)
+    requires
+        size != 0,
+    ensures
+        slice_iterator_view::<Windows<'a, T>, T>(iter).source == slice@,
+        slice_iterator_view::<Windows<'a, T>, T>(iter).remaining == slice@,
+        slice_iterator_view::<Windows<'a, T>, T>(iter).yielded_prefix == Seq::empty(),
+        slice_iterator_view::<Windows<'a, T>, T>(iter).remainder == Seq::empty(),
+        slice_iterator_view::<Windows<'a, T>, T>(iter).chunk_size == size as int,
+        !slice_iterator_view::<Windows<'a, T>, T>(iter).reverse,
+;
+
+pub assume_specification<'a, T>[ ChunksExact::<'a, T>::remainder ](
+    iter: &ChunksExact<'a, T>,
+) -> (ret: &'a [T])
+    ensures
+        ret@ == slice_iterator_view::<&ChunksExact<'a, T>, T>(iter).remainder,
+        ret@.len() < slice_iterator_view::<&ChunksExact<'a, T>, T>(iter).chunk_size,
+;
+
+pub assume_specification<'a, T>[ ChunksExactMut::<'a, T>::into_remainder ](
+    iter: ChunksExactMut<'a, T>,
+) -> (ret: &'a mut [T])
+    ensures
+        ret@ == slice_iterator_view::<ChunksExactMut<'a, T>, T>(iter).remainder,
+        ret@.len() < slice_iterator_view::<ChunksExactMut<'a, T>, T>(iter).chunk_size,
+;
+
+pub assume_specification<'a, T>[ RChunksExact::<'a, T>::remainder ](
+    iter: &RChunksExact<'a, T>,
+) -> (ret: &'a [T])
+    ensures
+        ret@ == slice_iterator_view::<&RChunksExact<'a, T>, T>(iter).remainder,
+        ret@.len() < slice_iterator_view::<&RChunksExact<'a, T>, T>(iter).chunk_size,
+;
+
+pub assume_specification<'a, T>[ RChunksExactMut::<'a, T>::into_remainder ](
+    iter: RChunksExactMut<'a, T>,
+) -> (ret: &'a mut [T])
+    ensures
+        ret@ == slice_iterator_view::<RChunksExactMut<'a, T>, T>(iter).remainder,
+        ret@.len() < slice_iterator_view::<RChunksExactMut<'a, T>, T>(iter).chunk_size,
+;
+
+pub assume_specification<'a>[ <[u8]>::utf8_chunks ](
+    slice: &'a [u8],
+) -> (iter: Utf8Chunks<'a>)
+    ensures
+        utf8_chunk_partition::<Utf8Chunks<'a>>(iter, slice@),
+;
+
+pub assume_specification[ <[u8]>::eq_ignore_ascii_case ](
+    slice: &[u8],
+    other: &[u8],
+) -> (ret: bool)
+    ensures
+        ret <==> ascii_eq_ignore_case(slice@, other@),
+;
+
+pub assume_specification<'a>[ <[u8]>::escape_ascii ](
+    slice: &'a [u8],
+) -> (iter: EscapeAscii<'a>)
+    ensures
+        slice_iterator_view::<EscapeAscii<'a>, u8>(iter).source == slice@,
+        slice_iterator_view::<EscapeAscii<'a>, u8>(iter).remaining == ascii_escape_seq(slice@),
+;
+
+pub assume_specification[ <[u8]>::make_ascii_lowercase ](slice: &mut [u8])
+    ensures
+        final(slice)@ == ascii_lower_seq(old(slice)@),
+;
+
+pub assume_specification[ <[u8]>::make_ascii_uppercase ](slice: &mut [u8])
+    ensures
+        final(slice)@ == ascii_upper_seq(old(slice)@),
+;
+
+pub assume_specification[ <[u8]>::trim_ascii ](slice: &[u8]) -> (ret: &[u8])
+    ensures
+        ascii_trim_source_body_result(slice@, ret),
+;
+
+pub assume_specification[ <[u8]>::trim_ascii_end ](slice: &[u8]) -> (ret: &[u8])
+    ensures
+        ascii_trim_end_result(slice@, ret),
+;
+
+pub assume_specification[ <[u8]>::trim_ascii_start ](slice: &[u8]) -> (ret: &[u8])
+    ensures
+        ascii_trim_start_result(slice@, ret),
+;
+
 pub broadcast group group_slice_axioms {
     axiom_slice_get_range,
     axiom_slice_get_range_to,