Function ber_char_string_fmt 

pub open spec fn ber_char_string_fmt<C: SpecCombinator, const LIMIT: usize>(
    tag: Tag,
    content: C,
) -> Mapped<Refined<BerOctetStringFmt<LIMIT>, PredFnSpec<Seq<u8>>>, FnSpecMapper<Seq<u8>, <C as SpecByteLen>::T>>

{
    Mapped {
        inner: Refined(
            BerOctetStringFmt::<LIMIT>(tag),
            |bytes: Seq<u8>| content.spec_parse(bytes) is Some,
        ),
        mapper: (
            |bytes: Seq<u8>| (content.spec_parse(bytes)->0).1,
            |value: C::T| content.spec_serialize(value),
        ),
    }
}

reject invalid flattened contents, then map the validated octets to the string value.