Strings

Verus supports reasoning about Rust String and &str:

fn get_char() {
    let x = "hello world";
    proof {
        reveal_strlit("hello world");
    }
    assert(x@.len() == 11);
    let val = x.get_char(0);
    assert('h' === val);
}

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:

fn literal_eq() {
    let x = "hello world";
    let y = "hello world";
    assert(x@ == y@);
}

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

fn str_view() {
    let x = "hello world";
    let ghost y: Seq<char> = x@;
}

whose value is unkown 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:

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

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

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

fn test() {
    let a = String::from_str(("ABC"));
    proof {
        reveal_strlit("ABC");
    }
    assert(a.is_ascii());
    let b = a.as_str().substring_ascii(2, 3);
    proof {
        reveal_strlit("C");
    }
    assert(b@ =~= ("C")@);
}