pub open spec fn encode_bmp_string(chars: Seq<char>) -> Seq<u8>
{ Seq::new(chars.len() * 2, |i: int| u16_be_to_bytes(chars[i / 2] as u16)[i % 2]) }
Encode Unicode BMP scalars as two-octet big-endian BMP/UCS-2 code units.