vstd_extra/external/
str.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specifications for the UTF-8 string APIs missing from `vstd`.
3//!
4//! `vstd` models UTF-8 validity itself (`vstd::utf8::valid_utf8`) and specifies
5//! `str::from_utf8_unchecked`, but it does not specify `core::str::from_utf8`.
6use vstd::{prelude::*, string::StringSliceAdditionalSpecFns, utf8::valid_utf8};
7
8verus! {
9
10/// The error payload of [`core::str::from_utf8`]. It is never inspected by
11/// OSTD, so it carries no specification of its own beyond being usable in
12/// Verus specs.
13#[verifier::external_type_specification]
14#[verifier::external_body]
15pub struct ExUtf8Error(core::str::Utf8Error);
16
17/// Validates UTF-8 and returns a `&str` borrowing the input bytes on success.
18/// See [`std::str::from_utf8`](https://doc.rust-lang.org/std/str/fn.from_utf8.html).
19///
20/// The result is `Ok` exactly when the input models a valid UTF-8 string
21/// ([`vstd::utf8::valid_utf8`]); on `Ok`, the decoded string borrows exactly
22/// the input bytes.
23pub assume_specification[ core::str::from_utf8 ](v: &[u8]) -> (res: Result<
24    &str,
25    core::str::Utf8Error,
26>)
27    ensures
28        res matches Ok(s) ==> {
29            &&& valid_utf8(v@)
30            &&& s.spec_bytes() =~= v@
31        },
32        res matches Err(_) ==> !valid_utf8(v@),
33;
34
35} // verus!
vstd_extra/external/str.rs

vstd_extra/external/
str.rs
