pub open spec fn valid_utf8(bytes: Seq<u8>) -> bool
{ bytes.len() != 0 ==> valid_first_scalar(bytes) && valid_utf8(pop_first_scalar(bytes)) }
True when the given bytes form a valid UTF-8 encoding.