Function bmpstring_fmt 

pub open spec fn bmpstring_fmt() -> Mapped<Refined<Tail, PredFnSpec<Seq<u8>>>, FnSpecMapper<Seq<u8>, BmpStringSpec>>

{
    Mapped {
        inner: Refined(Tail, |bytes: Seq<u8>| is_valid_bmp_string(bytes)),
        mapper: (
            |bytes: Seq<u8>| BmpStringSpec {
                inner: decode_bmp_string(bytes),
            },
            |s: BmpStringSpec| encode_bmp_string(s.inner),
        ),
    }
}