Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000#![feature(rustc_attrs)]#![allow(unused_imports)]
#[cfg(all(feature = "alloc", not(verus_verify_core)))]use alloc::str::Chars;#[cfg(all(feature = "alloc", not(verus_verify_core)))]use alloc::string::{self, String, ToString};#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]use core::ops::{Bound, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive};#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]use core::slice::SliceIndex;
use super::prelude::*;use super::seq::Seq;use super::slice::*;#[cfg(all(verus_keep_ghost, feature = "alloc", not(verus_verify_core)))]use super::std_specs::fmt::DisplaySpec;#[cfg(verus_keep_ghost)]#[cfg(all(feature = "alloc", not(verus_verify_core)))]use super::std_specs::iter::IteratorSpec;#[cfg(verus_keep_ghost)]use super::std_specs::range::{ ExRange, RangeBoundsSpec, slice_range_end, slice_range_start, slice_range_valid, spec_range_inclusive_slice_bounds,};use super::utf8::*;use super::view::*;
#[cfg(verus_keep_ghost)]#[cfg(not(verus_verify_core))]use super::std_specs::cmp::PartialEqSpecImpl;
verus! {
broadcast use {super::seq::group_seq_lemmas, super::slice::group_slice_axioms};
#[cfg(not(verus_verify_core))]impl View for str { type V = Seq<char>;
uninterp spec fn view(&self) -> Seq<char>;}
#[cfg(not(verus_verify_core))]impl DeepView for str { type V = Seq<char>;
open spec fn deep_view(&self) -> Seq<char> { self.view() }}
#[cfg(verus_keep_ghost)]#[cfg(not(verus_verify_core))]impl PartialEqSpecImpl for str { open spec fn obeys_eq_spec() -> bool { true }
open spec fn eq_spec(&self, other: &str) -> bool { self@ == other@ }}
#[cfg(not(verus_verify_core))]pub trait StringSliceAdditionalSpecFns { spec fn spec_bytes(&self) -> Seq<u8>;}
#[cfg(not(verus_verify_core))]impl StringSliceAdditionalSpecFns for str { open spec fn spec_bytes(&self) -> Seq<u8> { encode_utf8(self@) }}
#[cfg(not(verus_verify_core))]pub open spec fn is_ascii(s: &str) -> bool { is_ascii_chars(s@)}
#[cfg(not(verus_verify_core))]pub broadcast proof fn is_ascii_spec_bytes(s: &str) ensures #[trigger] is_ascii(s) ==> #[trigger] s.spec_bytes() =~= Seq::new( s@.len(), |i| s@.index(i) as u8, ),{ if (is_ascii(s)) { is_ascii_chars_encode_utf8(s@); }}
#[cfg(not(verus_verify_core))]pub broadcast proof fn is_ascii_concat(s1: &str, s2: &str, s3: &str) requires s1@ =~= s2@ + s3@, ensures #![trigger s2@ + s3@, is_ascii(s1), is_ascii(s2), is_ascii(s3)] is_ascii(s1) <==> is_ascii(s2) && is_ascii(s3),{ broadcast use is_ascii_chars_concat;
if (is_ascii(s1)) { is_ascii_chars_concat(s1@, s2@, s3@); }}
#[cfg(not(verus_verify_core))]#[verifier::when_used_as_spec(is_ascii)]pub assume_specification[ str::is_ascii ](s: &str) -> (b: bool) ensures b == is_ascii(s),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]use crate::alloc::borrow::ToOwned;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ str::to_owned ](s: &str) -> (res: String) ensures s@ == res@,;
#[cfg(not(verus_verify_core))]pub assume_specification[ str::as_bytes ](s: &str) -> (b: &[u8]) ensures b@ == s.spec_bytes(), opens_invariants none no_unwind;
#[cfg(not(verus_verify_core))]#[verifier::allow_in_spec]pub assume_specification[ str::len ](s: &str) -> usize returns s.spec_bytes().len() as usize, opens_invariants none no_unwind;
#[cfg(not(verus_verify_core))]#[verifier::allow_in_spec]pub assume_specification[ str::is_empty ](s: &str) -> bool returns s@.len() == 0, opens_invariants none no_unwind;
#[cfg(not(verus_verify_core))]#[verifier::allow_in_spec]pub assume_specification[ str::is_char_boundary ](s: &str, index: usize) -> bool returns is_char_boundary(s.spec_bytes(), index as int),;
#[cfg(not(verus_verify_core))]pub assume_specification[ str::split_at ](s: &str, mid: usize) -> (res: (&str, &str)) requires is_char_boundary(s.spec_bytes(), mid as int), ensures res.0.spec_bytes() =~= s.spec_bytes()[..mid], res.1.spec_bytes() =~= s.spec_bytes()[mid..],;
#[cfg(not(verus_verify_core))]pub assume_specification[ str::from_utf8_unchecked ](v: &[u8]) -> (res: &str) requires valid_utf8(v@), ensures res.spec_bytes() =~= v@,;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub uninterp spec fn to_string_from_display_ensures<T: core::fmt::Display + ?Sized>( t: &T, s: String,) -> bool;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub broadcast proof fn to_string_from_display_ensures_for_str(t: &str, res: String) ensures #[trigger] to_string_from_display_ensures::<str>(t, res) <==> (t@ == res@),{ admit();}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification<T: core::fmt::Display + ?Sized>[ <T as ToString>::to_string ]( t: &T,) -> (res: String) requires forall|f: &core::fmt::Formatter<'_>| t.fmt_req(f), ensures to_string_from_display_ensures::<T>(t, res),;
#[cfg(not(verus_verify_core))]#[verifier::external]pub trait StrSliceExecFns { fn unicode_len(&self) -> usize;
fn get_char(&self, i: usize) -> char;
fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str;
fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str;
fn get_ascii(&self, i: usize) -> u8;
#[cfg(feature = "alloc")] fn as_bytes_vec(&self) -> alloc::vec::Vec<u8>;}
#[cfg(not(verus_verify_core))]impl StrSliceExecFns for str { /// The len() function in rust returns the byte length. /// It is more useful to talk about the length of characters and therefore this function was added. /// Please note that this function counts the unicode variation selectors as characters. /// Warning: O(n) #[verifier::external_body] fn unicode_len(&self) -> (l: usize) ensures l as nat == self@.len(), { self.chars().count() }
/// Warning: O(n) not O(1) due to unicode decoding needed #[verifier::external_body] fn get_char(&self, i: usize) -> (c: char) requires i < self@.len(), ensures self@.index(i as int) == c, { self.chars().nth(i).unwrap() }
#[verifier::external_body] fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str) requires self.is_ascii(), from <= to <= self@.len(), ensures ret@ == self@[from..to], ret.is_ascii(), { // Range::index panics if from > to or from > self@.len() &self[from..to] }
#[verifier::external_body] fn substring_char<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str) requires from <= to <= self@.len(), ensures ret@ == self@[from..to], { let mut char_pos = 0; let mut byte_start = None; let mut byte_end = None; let mut byte_pos = 0; let mut it = self.chars(); loop { if char_pos == from { byte_start = Some(byte_pos); } if char_pos == to { byte_end = Some(byte_pos); break; } if let Some(c) = it.next() { char_pos += 1; byte_pos += c.len_utf8(); } else { break; } } let byte_start = byte_start.unwrap(); let byte_end = byte_end.unwrap(); // Range::index panics if from > to or from > self@.len() &self[byte_start..byte_end] }
fn get_ascii(&self, i: usize) -> (b: u8) requires self.is_ascii(), i < self@.len(), ensures self@.index(i as int) as u8 == b, { broadcast use is_ascii_spec_bytes; // panics if i is not a valid index
self.as_bytes()[i] }
#[cfg(feature = "alloc")] fn as_bytes_vec(&self) -> (ret: alloc::vec::Vec<u8>) ensures ret@ == self.spec_bytes(), { slice_to_vec(self.as_bytes()) }}
#[cfg(not(verus_verify_core))]pub uninterp spec fn strlit_view_id(s: Seq<char>) -> int;
/// Distinct string literals have provably distinct views.#[cfg(not(verus_verify_core))]pub broadcast axiom fn axiom_new_strlit_view_id(id: int) ensures strlit_view_id(#[trigger] strslice_new_strlit(id).view()) == id,;
#[cfg(not(verus_verify_core))]pub broadcast axiom fn axiom_str_literal_len<'a>(s: &'a str) ensures #[trigger] s@.len() == strslice_len(s),;
#[cfg(not(verus_verify_core))]pub broadcast axiom fn axiom_str_literal_get_char<'a>(s: &'a str, i: int) ensures #[trigger] s@.index(i) == strslice_get_char(s, i),;
#[cfg(all(not(feature = "alloc"), not(verus_verify_core)))]pub broadcast group group_string_axioms { axiom_new_strlit_view_id, axiom_str_literal_len, axiom_str_literal_get_char, is_ascii_spec_bytes, is_ascii_concat,}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub broadcast group group_string_axioms { axiom_new_strlit_view_id, axiom_str_literal_len, axiom_str_literal_get_char, to_string_from_display_ensures_for_str, is_ascii_spec_bytes, is_ascii_concat,}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]impl View for String { type V = Seq<char>;
uninterp spec fn view(&self) -> Seq<char>;}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]impl DeepView for String { type V = Seq<char>;
open spec fn deep_view(&self) -> Seq<char> { self.view() }}
#[cfg(verus_keep_ghost)]#[cfg(all(feature = "alloc", not(verus_verify_core)))]impl PartialEqSpecImpl for String { open spec fn obeys_eq_spec() -> bool { true }
open spec fn eq_spec(&self, other: &String) -> bool { self@ == other@ }}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]#[verifier::external_type_specification]#[verifier::external_body]pub struct ExString(String);
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub open spec fn string_is_ascii(s: &String) -> bool { is_ascii_chars(s@)}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification<'a>[ String::as_str ](s: &'a String) -> (res: &'a str) ensures res@ == s@, opens_invariants none no_unwind;
// same as above#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification<'a>[ <String as core::ops::Deref>::deref ](s: &'a String) -> (res: &'a str) ensures res@ == s@,;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ <String as Clone>::clone ](s: &String) -> (res: String) ensures res == s,;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ <String as PartialEq>::eq ](s: &String, other: &String) -> (res: bool) ensures res == (s@ == other@),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::new ]() -> (res: String) ensures res@ == Seq::<char>::empty(),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::push ](s: &mut String, c: char) ensures final(s)@ == old(s)@.push(c),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::pop ](s: &mut String) -> (res: Option<char>) ensures old(s)@.len() == 0 ==> res is None && final(s)@ == old(s)@, old(s)@.len() > 0 ==> res == Some(old(s)@.last()) && final(s)@ == old(s)@.drop_last(),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::push_str ](s: &mut String, other: &str) ensures final(s)@ == old(s)@ + other@,;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::is_empty ](s: &String) -> (res: bool) ensures res == (s@.len() == 0), opens_invariants none no_unwind;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ String::clear ](s: &mut String) ensures final(s)@ == Seq::<char>::empty(),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub assume_specification[ <String as core::default::Default>::default ]() -> (r: String) ensures r@ == Seq::<char>::empty(),;
#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub trait StringExecFnsIsAscii: Sized { fn is_ascii(&self) -> bool;}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]impl StringExecFnsIsAscii for String { #[inline(always)] #[verifier::when_used_as_spec(string_is_ascii)] fn is_ascii(&self) -> (ret: bool) ensures ret == string_is_ascii(self), { self.as_str().is_ascii() }}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]#[verifier::external]pub trait StringExecFns: Sized { fn from_str<'a>(s: &'a str) -> String;
fn append<'a, 'b>(&'a mut self, other: &'b str);
fn concat<'b>(self, other: &'b str) -> String;}
#[cfg(all(feature = "alloc", not(verus_verify_core)))]impl StringExecFns for String { #[verifier::external_body] fn from_str<'a>(s: &'a str) -> (ret: String) ensures s@ == ret@, { s.to_string() }
#[verifier::external_body] fn append<'a, 'b>(&'a mut self, other: &'b str) ensures final(self)@ == old(self)@ + other@, { *self += other; }
#[verifier::external_body] fn concat<'b>(self, other: &'b str) -> (ret: String) ensures ret@ == self@ + other@, { self + other }}
// The `chars` method of a `str` returns an iterator of type `Chars`,// so we specify that type here.#[verifier::external_type_specification]#[verifier::external_body]#[cfg(all(feature = "alloc", not(verus_verify_core)))]pub struct ExChars<'a>(Chars<'a>);
// To allow reasoning about the "contents" of the string iterator, without using// a prophecy, we need a function that gives us the underlying sequence of the original string.#[cfg(feature = "alloc")]pub uninterp spec fn into_iter_elts<'a>(i: Chars<'a>) -> Seq<char>;
#[cfg(feature = "alloc")]pub assume_specification[ str::chars ](s: &str) -> (iter: Chars<'_>) ensures IteratorSpec::remaining(&iter) == s@, IteratorSpec::decrease(&iter) is Some,;
#[cfg(verus_keep_ghost)]#[cfg(feature = "alloc")]impl<'a> super::std_specs::iter::IteratorSpecImpl for Chars<'a> { open spec fn obeys_prophetic_iter_laws(&self) -> bool { true }
uninterp spec fn remaining(&self) -> Seq<Self::Item>;
#[verifier::prophetic] open spec fn produces(&self) -> Seq<bool> { Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) }
uninterp spec fn decrease(&self) -> Option<nat>;
open spec fn peek(&self, index: int) -> Option<Self::Item> { if 0 <= index < into_iter_elts(*self).len() { Some(into_iter_elts(*self)[index]) } else { None } }}
// There are various types you can use to index into a `str` to get a// slice, i.e., to implement `SliceIndex<str>`. Here we indicate, for// any such type (e.g., `Range<usize>`), whether an index of that// type is valid when applied to a given `&str`.#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]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()))}
// There are various types you can use to index into a `str` to get a// slice, i.e., to implement `SliceIndex<str>`. Here we indicate, for// any such type (e.g., `Range<usize>`), the semantics of immutably// indexing a string.#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub open spec fn str_slice_index_postcondition<R: RangeBoundsSpec<usize>>( range: &R, s: Seq<u8>, r: Seq<u8>,) -> bool { r == s[slice_range_start(range)..slice_range_end(range, s.len())]}
// There are various types you can use to index into a `str` to get a// slice, i.e., to implement `SliceIndex<str>`. Here we indicate, for// any such type (e.g., `Range<usize>`), the semantics of mutably// indexing a string.#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub open spec fn str_slice_index_mut_postcondition<R: RangeBoundsSpec<usize>>( range: &R, old_s: Seq<u8>, final_s: Seq<u8>, r: Seq<u8>, final_r: Seq<u8>,) -> bool { let start = slice_range_start(range); let end = slice_range_end(range, old_s.len()); &&& r == old_s[start..end] &&& final_s.len() == old_s.len() &&& final_s[..start] == old_s[..start] &&& final_s[start..end] == final_r &&& final_s[end..old_s.len()] == old_s[end..]}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for (Bound<usize>, Bound<usize>) { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <(Bound<usize>, Bound<usize>) as SliceIndex<str>>::get ]( i: (Bound<usize>, Bound<usize>), s: &str,) -> (r: Option<&str>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <(Bound<usize>, Bound<usize>) as SliceIndex<str>>::index ]( i: (Bound<usize>, Bound<usize>), s: &str,) -> (r: &str);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <(Bound<usize>, Bound<usize>) as SliceIndex<str>>::get_mut ]( i: (Bound<usize>, Bound<usize>), s: &mut str,) -> (r: Option<&mut str>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <(Bound<usize>, Bound<usize>) as SliceIndex<str>>::index_mut ]( i: (Bound<usize>, Bound<usize>), s: &mut str,) -> (r: &mut str);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for Range<usize> { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <Range<usize> as SliceIndex<str>>::get ](i: Range<usize>, s: &str) -> (r: Option<&<Range<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <Range<usize> as SliceIndex<str>>::index ]( i: Range<usize>, s: &str,) -> (r: &<Range<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <Range<usize> as SliceIndex<str>>::get_mut ]( i: Range<usize>, s: &mut str,) -> (r: Option<&mut <Range<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <Range<usize> as SliceIndex<str>>::index_mut ]( i: Range<usize>, s: &mut str,) -> (r: &mut <Range<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for RangeFrom<usize> { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFrom<usize> as SliceIndex<str>>::get ]( i: RangeFrom<usize>, s: &str,) -> (r: Option<&<RangeFrom<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFrom<usize> as SliceIndex<str>>::index ]( i: RangeFrom<usize>, s: &str,) -> (r: &<RangeFrom<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFrom<usize> as SliceIndex<str>>::get_mut ]( i: RangeFrom<usize>, s: &mut str,) -> (r: Option<&mut <RangeFrom<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFrom<usize> as SliceIndex<str>>::index_mut ]( i: RangeFrom<usize>, s: &mut str,) -> (r: &mut <RangeFrom<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for RangeFull { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFull as SliceIndex<str>>::get ](i: RangeFull, s: &str) -> (r: Option<&<RangeFull as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFull as SliceIndex<str>>::index ](i: RangeFull, s: &str) -> (r: &<RangeFull as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFull as SliceIndex<str>>::get_mut ]( i: RangeFull, s: &mut str,) -> (r: Option<&mut <RangeFull as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeFull as SliceIndex<str>>::index_mut ]( i: RangeFull, s: &mut str,) -> (r: &mut <RangeFull as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for RangeInclusive<usize> { open spec fn in_bounds(&self, s: &str) -> bool { str_slice_in_bounds(&spec_range_inclusive_slice_bounds(self), s) }
open spec fn index_postcondition(&self, s: &str, r: &str) -> bool { str_slice_index_postcondition( &spec_range_inclusive_slice_bounds(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( &spec_range_inclusive_slice_bounds(self), old_slice.spec_bytes(), final_slice.spec_bytes(), immediate_output.spec_bytes(), final_output.spec_bytes(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeInclusive<usize> as SliceIndex<str>>::get ]( i: RangeInclusive<usize>, s: &str,) -> (r: Option<&<RangeInclusive<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeInclusive<usize> as SliceIndex<str>>::index ]( i: RangeInclusive<usize>, s: &str,) -> (r: &<RangeInclusive<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeInclusive<usize> as SliceIndex<str>>::get_mut ]( i: RangeInclusive<usize>, s: &mut str,) -> (r: Option<&mut <RangeInclusive<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeInclusive<usize> as SliceIndex<str>>::index_mut ]( i: RangeInclusive<usize>, s: &mut str,) -> (r: &mut <RangeInclusive<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for RangeTo<usize> { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeTo<usize> as SliceIndex<str>>::get ]( i: RangeTo<usize>, s: &str,) -> (r: Option<&<RangeTo<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeTo<usize> as SliceIndex<str>>::index ]( i: RangeTo<usize>, s: &str,) -> (r: &<RangeTo<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeTo<usize> as SliceIndex<str>>::get_mut ]( i: RangeTo<usize>, s: &mut str,) -> (r: Option<&mut <RangeTo<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeTo<usize> as SliceIndex<str>>::index_mut ]( i: RangeTo<usize>, s: &mut str,) -> (r: &mut <RangeTo<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl super::slice::SliceIndexSpecImpl<str> for RangeToInclusive<usize> { 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(), ) }}
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeToInclusive<usize> as SliceIndex<str>>::get ]( i: RangeToInclusive<usize>, s: &str,) -> (r: Option<&<RangeToInclusive<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeToInclusive<usize> as SliceIndex<str>>::index ]( i: RangeToInclusive<usize>, s: &str,) -> (r: &<RangeToInclusive<usize> as SliceIndex<str>>::Output);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeToInclusive<usize> as SliceIndex<str>>::get_mut ]( i: RangeToInclusive<usize>, s: &mut str,) -> (r: Option<&mut <RangeToInclusive<usize> as SliceIndex<str>>::Output>);
#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]pub assume_specification[ <RangeToInclusive<usize> as SliceIndex<str>>::index_mut ]( i: RangeToInclusive<usize>, s: &mut str,) -> (r: &mut <RangeToInclusive<usize> as SliceIndex<str>>::Output);
// `<str as ops::Index<I>>::index(&self, index: I)` just invokes// `index.index(self)`. So we likewise delegate determining the meaning// of the string-index operation to that of the index type.#[cfg(all(verus_keep_ghost, not(verus_verify_core)))]impl<I: SliceIndexSpec<str>> super::std_specs::core::IndexSpecImpl<I> for str { open spec fn index_req(&self, index: &I) -> bool { index.in_bounds(self) }}
pub use super::view::View;
} // verus!