1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4#[cfg(feature = "alloc")]
5use alloc::str::Chars;
6#[cfg(feature = "alloc")]
7use alloc::string::{self, String, ToString};
8
9#[cfg(feature = "alloc")]
10use super::pervasive::{ForLoopGhostIterator, ForLoopGhostIteratorNew};
11use super::prelude::*;
12use super::seq::Seq;
13use super::view::*;
14
15verus! {
16
17impl View for str {
18 type V = Seq<char>;
19
20 uninterp spec fn view(&self) -> Seq<char>;
21}
22
23impl DeepView for str {
24 type V = Seq<char>;
25
26 open spec fn deep_view(&self) -> Seq<char> {
27 self.view()
28 }
29}
30
31pub uninterp spec fn str_slice_is_ascii(s: &str) -> bool;
32
33#[verifier::when_used_as_spec(str_slice_is_ascii)]
34pub assume_specification[ str::is_ascii ](s: &str) -> (b: bool)
35 ensures
36 b == str_slice_is_ascii(s),
37;
38
39pub open spec fn new_strlit_spec(s: &str) -> &str {
40 s
41}
42
43#[cfg(feature = "alloc")]
44use crate::alloc::borrow::ToOwned;
45
46#[cfg(feature = "alloc")]
47pub assume_specification[ str::to_owned ](s: &str) -> (res: String)
48 ensures
49 s@ == res@,
50 s.is_ascii() == res.is_ascii(),
51;
52
53#[cfg(feature = "alloc")]
54pub uninterp spec fn to_string_from_display_ensures<T: core::fmt::Display + ?Sized>(
55 t: &T,
56 s: String,
57) -> bool;
58
59#[cfg(feature = "alloc")]
60pub broadcast proof fn to_string_from_display_ensures_for_str(t: &str, res: String)
61 ensures
62 #[trigger] to_string_from_display_ensures::<str>(t, res) <==> (t@ == res@ && t.is_ascii()
63 == res.is_ascii()),
64{
65 admit();
66}
67
68#[cfg(feature = "alloc")]
69pub assume_specification<T: core::fmt::Display + ?Sized>[ <T as ToString>::to_string ](
70 t: &T,
71) -> (res: String)
72 ensures
73 to_string_from_display_ensures::<T>(t, res),
74;
75
76#[verifier::external]
77pub trait StrSliceExecFns {
78 fn unicode_len(&self) -> usize;
79
80 fn get_char(&self, i: usize) -> char;
81
82 fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str;
83
84 fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str;
85
86 fn get_ascii(&self, i: usize) -> u8;
87
88 #[cfg(feature = "alloc")]
89 fn as_bytes_vec(&self) -> alloc::vec::Vec<u8>;
90}
91
92impl StrSliceExecFns for str {
93 #[verifier::external_body]
98 fn unicode_len(&self) -> (l: usize)
99 ensures
100 l as nat == self@.len(),
101 {
102 self.chars().count()
103 }
104
105 #[verifier::external_body]
107 fn get_char(&self, i: usize) -> (c: char)
108 requires
109 i < self@.len(),
110 ensures
111 self@.index(i as int) == c,
112 self.is_ascii() ==> forall|i: int| i < self@.len() ==> (self@.index(i) as nat) < 256,
113 {
114 self.chars().nth(i).unwrap()
115 }
116
117 #[verifier::external_body]
118 fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str)
119 requires
120 self.is_ascii(),
121 from < self@.len(),
122 to <= self@.len(),
123 ensures
124 ret@ == self@.subrange(from as int, to as int),
125 ret.is_ascii() == self.is_ascii(),
126 {
127 &self[from..to]
128 }
129
130 #[verifier::external_body]
131 fn substring_char<'a>(&'a self, from: usize, to: usize) -> (ret: &'a str)
132 requires
133 from < self@.len(),
134 to <= self@.len(),
135 ensures
136 ret@ == self@.subrange(from as int, to as int),
137 ret.is_ascii() == self.is_ascii(),
138 {
139 let mut char_pos = 0;
140 let mut byte_start = None;
141 let mut byte_end = None;
142 let mut byte_pos = 0;
143 let mut it = self.chars();
144 loop {
145 if char_pos == from {
146 byte_start = Some(byte_pos);
147 }
148 if char_pos == to {
149 byte_end = Some(byte_pos);
150 break ;
151 }
152 if let Some(c) = it.next() {
153 char_pos += 1;
154 byte_pos += c.len_utf8();
155 } else {
156 break ;
157 }
158 }
159 let byte_start = byte_start.unwrap();
160 let byte_end = byte_end.unwrap();
161 &self[byte_start..byte_end]
162 }
163
164 #[verifier::external_body]
165 fn get_ascii(&self, i: usize) -> (b: u8)
166 requires
167 self.is_ascii(),
168 ensures
169 self.view().index(i as int) as u8 == b,
170 {
171 self.as_bytes()[i]
172 }
173
174 #[cfg(feature = "alloc")]
178 #[verifier::external_body]
179 fn as_bytes_vec(&self) -> (ret: alloc::vec::Vec<u8>)
180 requires
181 self.is_ascii(),
182 ensures
183 ret.view() == Seq::new(self.view().len(), |i| self.view().index(i) as u8),
184 {
185 let mut v = alloc::vec::Vec::new();
186 for c in self.as_bytes().iter() {
187 v.push(*c);
188 }
189 v
190 }
191}
192
193pub broadcast axiom fn axiom_str_literal_is_ascii<'a>(s: &'a str)
194 ensures
195 #[trigger] s.is_ascii() == strslice_is_ascii(s),
196;
197
198pub broadcast axiom fn axiom_str_literal_len<'a>(s: &'a str)
199 ensures
200 #[trigger] s@.len() == strslice_len(s),
201;
202
203pub broadcast axiom fn axiom_str_literal_get_char<'a>(s: &'a str, i: int)
204 ensures
205 #[trigger] s@.index(i) == strslice_get_char(s, i),
206;
207
208#[cfg(not(feature = "alloc"))]
209pub broadcast group group_string_axioms {
210 axiom_str_literal_is_ascii,
211 axiom_str_literal_len,
212 axiom_str_literal_get_char,
213}
214
215#[cfg(feature = "alloc")]
216pub broadcast group group_string_axioms {
217 axiom_str_literal_is_ascii,
218 axiom_str_literal_len,
219 axiom_str_literal_get_char,
220 to_string_from_display_ensures_for_str,
221}
222
223#[cfg(feature = "alloc")]
224impl View for String {
225 type V = Seq<char>;
226
227 uninterp spec fn view(&self) -> Seq<char>;
228}
229
230#[cfg(feature = "alloc")]
231impl DeepView for String {
232 type V = Seq<char>;
233
234 open spec fn deep_view(&self) -> Seq<char> {
235 self.view()
236 }
237}
238
239#[cfg(feature = "alloc")]
240#[verifier::external_type_specification]
241#[verifier::external_body]
242pub struct ExString(String);
243
244#[cfg(feature = "alloc")]
245pub uninterp spec fn string_is_ascii(s: &String) -> bool;
246
247#[cfg(feature = "alloc")]
248#[verifier::when_used_as_spec(string_is_ascii)]
249pub assume_specification[ String::is_ascii ](s: &String) -> (b: bool)
250 ensures
251 b == string_is_ascii(s),
252;
253
254#[cfg(feature = "alloc")]
255pub assume_specification<'a>[ String::as_str ](s: &'a String) -> (res: &'a str)
256 ensures
257 res@ == s@,
258 s.is_ascii() == res.is_ascii(),
259;
260
261#[cfg(feature = "alloc")]
262pub assume_specification[ <String as Clone>::clone ](s: &String) -> (res: String)
263 ensures
264 res == s,
265;
266
267#[cfg(feature = "alloc")]
268pub assume_specification[ <String as PartialEq>::eq ](s: &String, other: &String) -> (res: bool)
269 ensures
270 res == (s@ == other@),
271;
272
273#[cfg(feature = "alloc")]
274#[verifier::external]
275pub trait StringExecFnsIsAscii: Sized {
276 fn is_ascii(&self) -> bool;
277}
278
279#[cfg(feature = "alloc")]
280#[verifier::external]
281impl StringExecFnsIsAscii for String {
282 #[inline(always)]
283 fn is_ascii(&self) -> bool {
284 self.as_str().is_ascii()
285 }
286}
287
288#[cfg(feature = "alloc")]
289#[verifier::external]
290pub trait StringExecFns: Sized {
291 fn from_str<'a>(s: &'a str) -> String;
292
293 fn append<'a, 'b>(&'a mut self, other: &'b str);
294
295 fn concat<'b>(self, other: &'b str) -> String;
296}
297
298#[cfg(feature = "alloc")]
299impl StringExecFns for String {
300 #[verifier::external_body]
301 fn from_str<'a>(s: &'a str) -> (ret: String)
302 ensures
303 s@ == ret@,
304 s.is_ascii() == ret.is_ascii(),
305 {
306 s.to_string()
307 }
308
309 #[verifier::external_body]
310 fn append<'a, 'b>(&'a mut self, other: &'b str)
311 ensures
312 self@ == old(self)@ + other@,
313 self.is_ascii() == old(self).is_ascii() && other.is_ascii(),
314 {
315 *self += other;
316 }
317
318 #[verifier::external_body]
319 fn concat<'b>(self, other: &'b str) -> (ret: String)
320 ensures
321 ret@ == self@ + other@,
322 ret.is_ascii() == self.is_ascii() && other.is_ascii(),
323 {
324 self + other
325 }
326}
327
328#[cfg(feature = "alloc")]
329pub assume_specification[ str::chars ](s: &str) -> (chars: Chars<'_>)
330 ensures
331 ({
332 let (index, c) = chars@;
333 &&& index == 0
334 &&& c == s@
335 }),
336;
337
338#[verifier::external_type_specification]
341#[verifier::external_body]
342#[cfg(feature = "alloc")]
343pub struct ExChars<'a>(Chars<'a>);
344
345#[cfg(feature = "alloc")]
346impl<'a> View for Chars<'a> {
347 type V = (int, Seq<char>);
348
349 uninterp spec fn view(&self) -> (int, Seq<char>);
350}
351
352#[cfg(feature = "alloc")]
353impl<'a> DeepView for Chars<'a> {
354 type V = <Self as View>::V;
355
356 open spec fn deep_view(&self) -> Self::V {
357 self@
358 }
359}
360
361#[cfg(feature = "alloc")]
362pub assume_specification<'a>[ Chars::<'a>::next ](chars: &mut Chars<'a>) -> (r: Option<char>)
363 ensures
364 ({
365 let (old_index, old_seq) = old(chars)@;
366 match r {
367 None => {
368 &&& chars@ == old(chars)@
369 &&& old_index >= old_seq.len()
370 },
371 Some(k) => {
372 let (new_index, new_seq) = chars@;
373 &&& 0 <= old_index < old_seq.len()
374 &&& new_seq == old_seq
375 &&& new_index == old_index + 1
376 &&& k == old_seq[old_index]
377 },
378 }
379 }),
380;
381
382#[cfg(feature = "alloc")]
383pub struct CharsGhostIterator<'a> {
384 pub pos: int,
385 pub chars: Seq<char>,
386 pub phantom: Option<&'a char>,
387}
388
389#[cfg(feature = "alloc")]
390impl<'a> ForLoopGhostIteratorNew for Chars<'a> {
391 type GhostIter = CharsGhostIterator<'a>;
392
393 open spec fn ghost_iter(&self) -> CharsGhostIterator<'a> {
394 CharsGhostIterator { pos: self@.0, chars: self@.1, phantom: None }
395 }
396}
397
398#[cfg(feature = "alloc")]
399impl<'a> ForLoopGhostIterator for CharsGhostIterator<'a> {
400 type ExecIter = Chars<'a>;
401
402 type Item = char;
403
404 type Decrease = int;
405
406 open spec fn exec_invariant(&self, exec_iter: &Chars<'a>) -> bool {
407 &&& self.pos == exec_iter@.0
408 &&& self.chars == exec_iter@.1
409 }
410
411 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
412 init matches Some(init) ==> {
413 &&& init.pos == 0
414 &&& init.chars == self.chars
415 &&& 0 <= self.pos <= self.chars.len()
416 }
417 }
418
419 open spec fn ghost_ensures(&self) -> bool {
420 self.pos == self.chars.len()
421 }
422
423 open spec fn ghost_decrease(&self) -> Option<int> {
424 Some(self.chars.len() - self.pos)
425 }
426
427 open spec fn ghost_peek_next(&self) -> Option<char> {
428 if 0 <= self.pos < self.chars.len() {
429 Some(self.chars[self.pos])
430 } else {
431 None
432 }
433 }
434
435 open spec fn ghost_advance(&self, _exec_iter: &Chars<'a>) -> CharsGhostIterator<'a> {
436 Self { pos: self.pos + 1, ..*self }
437 }
438}
439
440#[cfg(feature = "alloc")]
441impl<'a> View for CharsGhostIterator<'a> {
442 type V = Seq<char>;
443
444 open spec fn view(&self) -> Seq<char> {
445 self.chars.take(self.pos)
446 }
447}
448
449#[cfg(feature = "alloc")]
450impl<'a> DeepView for CharsGhostIterator<'a> {
451 type V = Seq<char>;
452
453 open spec fn deep_view(&self) -> Seq<char> {
454 self.view()
455 }
456}
457
458pub use super::view::View;
459
460}