Function is_valid_bmp_string 

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

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

}

The well-formedness condition for the BMP/UCS-2 contents octets.