incorrect spec for String::len?

[arnaudgolfouse]

impl ShallowModel for String {
    type ShallowModelTy = Seq<char>;
}

#[ensures(result@ == self@.len())]
fn len(&self) -> usize;

The length of the string is in bytes, so this spec is not correct I think? Same for str::split_at. Although I guess there is no way no observe this at the moment...

[xldenis]

Hmm yea I guess we should relax that to >=?

[arnaudgolfouse]

This would work, but shouldn't we actually give the correct length? With a logical function utf8_len(char) -> usize
I guess this would make str::len hard on provers, but if we use >= it would be a bit useless.

[xldenis]

Depends on what we need it for really.

[jhjourdan]

Do we want to formalized Unicode? No.
So the only alternative we have is not supporting len at all, which is definitely an option.