missing vstd specification for executable str equality

[wood-ghost]

There seems to be a missing specification connecting executable str equality with equality of Seq<char> .

The following example fails to verify:

equality with ==

use vstd::prelude::*;

verus! {

struct TextSource;

uninterp spec fn modeled_text(source: &TextSource) -> Seq<char>;

#[verifier::external_body]
fn get_text<'a>(source: &'a TextSource) -> (result: &'a str)
    ensures
        result@ == modeled_text(source),
{
    "hello world"
}

spec fn is_hello(source: &TextSource) -> bool {
    modeled_text(source) == "hello world"@
}

fn check(source: &TextSource) -> (result: bool)
    ensures
        result == is_hello(source),
{
    get_text(source) == "hello world"
}

}

The postcondition of check cannot be proved, even though get_text guarantees result@ == modeled_text(source) and the executable comparison is get_text(source) == "hello world"

Workaround

Currently it works by rewriting the original codes using a helper function

#[verifier::external_body]
fn str_equal(a: &str, b: &str) -> (result: bool)
    ensures
        result == (a@ == b@),
{
    a == b
}

and replace the check body with

str_equal(get_text(source), "hello world")

Complete working version:

use vstd::prelude::*;

verus! {

struct TextSource;

uninterp spec fn modeled_text(source: &TextSource) -> Seq<char>;

#[verifier::external_body]
fn get_text<'a>(source: &'a TextSource) -> (result: &'a str)
    ensures
        result@ == modeled_text(source),
{
    "hello world"
}

#[verifier::external_body]
fn str_equal(a: &str, b: &str) -> (result: bool)
    ensures
        result == (a@ == b@),
{
    a == b
}

spec fn is_hello(source: &TextSource) -> bool {
    modeled_text(source) == "hello world"@
}

fn check(source: &TextSource) -> (result: bool)
    ensures
        result == is_hello(source),
{
    str_equal(get_text(source), "hello world")
}

}

Expected behavior

The first version should verify without requiring a trusted helper.

The Playground share interface appears to preserve only one version at a time, so I included only the failing version as a Playground link and included the working workaround inline.

[wood-ghost]

This also fails:

fn test() {
    assert(
        ("a"@ + "b"@) =~= "ab"@
    );
}

[parno]

By default, Verus doesn't reveal the individual characters in string literals. If you want that level of detail, you need to call reveal_strlit. For example, your most recent example works if you add such calls. Your initial problem is most likely due to a missing definition of PartialEq/Eq for String.

[wood-ghost]

By default, Verus doesn't reveal the individual characters in string literals. If you want that level of detail, you need to call reveal_strlit. For example, your most recent example works if you add such calls. Your initial problem is most likely due to a missing definition of PartialEq/Eq for String.

Thank you for the reply! I added the definition of PartialEq/Eq for String and it solves my original problem.

[wood-ghost]

By default, Verus doesn't reveal the individual characters in string literals. If you want that level of detail, you need to call reveal_strlit. For example, your most recent example works if you add such calls. Your initial problem is most likely due to a missing definition of PartialEq/Eq for String.

I oversimplified my earlier question. My actual use case is more general, since I am currently verifying many string comparisons.

I would like to express a reusable property such as:

pub open spec fn str_cat_equal( str1: &str, str2: &str, string: &str ) -> bool { 
    str1@ + str2@ =~= string@ 
}

At concrete call sites, I can prove this by calling reveal_strlit on every involved literal. However, that requires hardcoding every string used by the program, which does not scale.

Conceptually, I was imagining the following chain:

&str -> Seq<char>                 supported via @
Seq<char> + Seq<char>            supported
Seq<char> -> corresponding &str   currently not supported?
&str compared with &str          supported

My current strategy is to use macro to generate all the reveal_strlit needed, which adds substantial annotation overhead.