Function is_bmp_char 

pub open spec fn is_bmp_char(c: char) -> bool

{ (c as u32) <= 0xffff }