Strings #

Verus supports reasoning about Rust String and &str:

{{#include ../../../../examples/guide/strings.rs:initial}}

By default a string literal is treated as opaque,

fn opaque_by_default() {
    let x = "hello world";
    assert(x@.len() == 11); // FAILS
}

this code results in a failed assertion:

error: assertion failed
  --> ../examples/guide/strings.rs:21:12
   |
21 |     assert(x@.len() == 11); // FAILS
   |            ^^^^^^^^^^^^^^ assertion failed

which can be fixed by using reveal_strlit (like in the example at the top).

However, comparing for equality does not require revealing literals:

{{#include ../../../../examples/guide/strings.rs:literal_eq}}

A string literal is a &str and its view is a Seq<char>,

{{#include ../../../../examples/guide/strings.rs:literal_view}}

whose value is unknown until the literal is revealed.

One can of course specify information about the view in, e.g., a function precondition (or some other predicate);

fn subrange<'a>(s: &str)
    requires
        s@ =~= "Hello"@,
{
    assert(s@.subrange(0, 1) == "H"@);
}

however, we need to reveal both literals to obtain information about their views in this case:

{{#include ../../../../examples/guide/strings.rs:pre_substring}}

Operating on strings currently requires the operations defined in vstd::string documented here.

An important predicate for &str and String is is_ascii, which enables efficient slicing, for example:

{{#include ../../../../examples/guide/strings.rs:substring_ascii}}