Function is_valid_universal_string 

pub open spec fn is_valid_universal_string(bytes: Seq<u8>) -> bool

{
    &&& bytes.len() % 4 == 0
    &&& forall |i: int| {
        0 <= i < bytes.len() / 4
            ==> vstd::utf8::is_scalar(#[trigger] universal_code_point(bytes, i))
    }

}

The well-formedness condition for UniversalString contents octets.