Function ber_any_rec_body 

pub open spec fn ber_any_rec_body(
    rec: ParamRecSpecs<(), Captured<AnySpec>>,
) -> Capture<Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<Tail, usize>, Sum<Repeat<BundledSpecs<Captured<AnySpec>>, EocFmt>, Void>>>>, Void>>>, FnSpecMapper<(Tag, Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, (Tag, u8)), Never>>), Never>), AnySpec>>>

{
    #[verusfmt::skip]
    Capture(Mapped {
        inner: Bind(
            TagFmt,
            |tag: Tag| {
                if tag == TagFmt::EOC {
                    R(Void("EOC is not an open-type value"))
                } else {
                    L(
                        Bind(
                            BerLengthFmt,
                            |length: BerLength| match length {
                                BerLength::Definite(len) => L(ExactLen(len, Tail)),
                                BerLength::Indefinite if tag.constructed => {
                                    R(L(Repeat(rec(()), EOC)))
                                }
                                BerLength::Indefinite => {
                                    R(R(Void("Primitive values cannot use indefinite length")))
                                }
                            },
                        ),
                    )
                }
            },
        ),
        mapper: (
            |parsed: BerAnyWireType| {
                match parsed.1 {
                    L((_length, L(content))) => AnySpec { tag: parsed.0, content },
                    L((_length, R(L((children, _eoc))))) => {
                        AnySpec {
                            tag: parsed.0,
                            content: captured_any_contents(children),
                        }
                    }
                    L((_length, R(R(_)))) => arbitrary(),
                    R(_) => arbitrary(),
                }
            },
            |value: AnySpec| (
                value.tag,
                L((BerLength::Definite(value.content.len() as usize), L(value.content))),
            ),
        ),
    })
}

One recursive unfolding of a BER open type.

Definite values retain their opaque contents. Indefinite values are legal only for constructed tags and retain the exact encodings of their child TLVs, excluding the terminating EOC. EOC itself is never accepted as an ANY value.