Function check_valid_bmp_string 

pub exec fn check_valid_bmp_string(bytes: &[u8]) -> res : bool

ensures

res == is_valid_bmp_string(bytes.deep_view()),

Check that a byte slice is a valid BMPString without allocation. TODO: Verify this function while keeping it efficient and idiomatic.