Function ber_octet_string_rec_body 

pub open spec fn ber_octet_string_rec_body(
    tag: Tag,
    rec: ParamRecSpecs<Tag, Seq<u8>>,
) -> Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<LengthFmt<BER>, FnSpec<(usize,), ExactLen<OctetStringFmt, usize>>>, Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<RepeatTillEnd<BundledSpecs<Seq<u8>>>, usize>, Repeat<BundledSpecs<Seq<u8>>, EocFmt>>>>, Void>>>>, FnSpecMapper<(Tag, Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, (Tag, u8))>), Never>>), Seq<u8>>>

{
    #[verusfmt::skip]
    Mapped {
        inner: Bind(
            TagFmt,
            |parsed_tag: Tag| match parsed_tag {
                t if t == primitive_tag(tag) => {
                    L(Bind(LengthFmt::<BER>, |len: usize| ExactLen(len, OctetStringFmt)))
                }
                t if t == constructed_tag(tag) => {
                    R(
                        L(
                            Bind(
                                BerLengthFmt,
                                |len: BerLength| match len {
                                    BerLength::Definite(len) => {
                                        L(ExactLen(len, RepeatTillEnd(rec(TagFmt::OCTET_STRING))))
                                    }
                                    BerLength::Indefinite => {
                                        R(Repeat(rec(TagFmt::OCTET_STRING), EOC))
                                    }
                                },
                            ),
                        ),
                    )
                }
                _ => {
                    R(R(Void("Tag must match the configured BER OCTET STRING identity")))
                }
            },
        ),
        mapper: (
            |parsed: BerOctetStringWireType| match parsed.1 {
                L((_len, bytes)) => bytes,
                R(L((_len, inner))) => {
                    match inner {
                        L(segments) => segments.flatten(),
                        R((segments, _eoc)) => segments.flatten(),
                    }
                }
                R(R(_)) => arbitrary(),
            },
            |bytes: Seq<u8>| (primitive_tag(tag), L((bytes.len() as usize, bytes))),
        ),
    }
}

One full TLV unfolding of a BER OCTET STRING.

X.690 §8.23.3 specifies a restricted character string as [UNIVERSAL x] IMPLICIT OCTET STRING. Thus tag applies only to the outermost TLV; constructed fragments recursively use universal OCTET STRING tag 4, as required by X.690 §8.7.3.2.