pub open spec fn encode_universal_string(chars: Seq<char>) -> Seq<u8>
{ Seq::new(chars.len() * 4, |i: int| u32_be_to_bytes(chars[i / 4] as u32)[i % 4]) }
Encode Unicode scalar values as four-octet big-endian code points.