vest_lib/asn1/ber/
any.rs

1//! BER ANY open type and capture wrappers.
2#[cfg(feature = "alloc")]
3use crate::asn1::AnyOwned;
4use crate::asn1::{AnyFmt, AnySpec, BerLength, BerLengthFmt, Tag, TagFmt, BER};
5use crate::combinators::{
6    bytes::ExactLen,
7    mapped::spec::FnSpecMapper,
8    recursive::{
9        BundledSpecs, EquivSerializersGeneralRecBody, GoodSerializerRecBody, ParamRecSpecs,
10        ParserRecBody, ProductiveRecBody, SafeParserRecBody, SpecRecBody,
11    },
12    Bind, Const, FixWith, Mapped, Pair, Repeat, Sum, Tail, Void, U8,
13};
14use crate::core::exec::fns::*;
15use crate::core::exec::parser::*;
16use crate::core::exec::{
17    input::InputBuf, ByteLen, OutputBuf, PResult, ParseError, PreSerializeError, Prepare,
18    Serializer,
19};
20use crate::core::{proof::*, spec::*};
21use crate::Never;
22#[cfg(feature = "alloc")]
23use alloc::vec::Vec;
24use vstd::prelude::*;
25#[cfg(feature = "alloc")]
26use vstd::slice::slice_to_vec;
27
28use Sum::Inl as L;
29use Sum::Inr as R;
30
31verus! {
32
33/// Exact BER end-of-contents marker: the universal primitive EOC tag followed by a zero length
34/// octet (`00 00`).
35pub type EocFmt = Pair<Const<TagFmt, Tag>, Const<U8, u8>>;
36
37/// Parsed value of [`EocFmt`]. BER framing discards this value after recognizing the marker.
38pub(super) type EocValue = (Tag, u8);
39
40/// Exact BER end-of-contents marker (`00 00`).
41pub const EOC: EocFmt = Pair(Const(TagFmt, TagFmt::EOC), Const(U8, 0u8));
42
43pub(super) open spec fn discard_eoc_result<T>(result: Option<(int, (T, EocValue))>) -> Option<
44    (int, T),
45> {
46    match result {
47        Some((n, (value, _eoc))) => Some((n, value)),
48        None => None,
49    }
50}
51
52pub(super) fn parse_discard_eoc<I, P, T>(parser: &P, input: &I) -> (result: PResult<T>) where
53    I: InputBuf,
54    T: DeepView,
55    P: Parser<I, PT = (T, EocValue), PVal = (T::V, EocValue)>,
56
57    requires
58        parser.exec_inv(),
59    ensures
60        parse_matches_spec(result, discard_eoc_result(parser.spec_parse(input@))),
61{
62    let (n, (value, _eoc)) = parser.parse(input)?;
63    Ok((n, value))
64}
65
66/// Zero-width boundary marker for the contents of a schema-defined BER constructed value.
67///
68/// It succeeds at the end of a definite-length input or immediately before EOC. In the latter
69/// case it deliberately leaves EOC unconsumed for the enclosing indefinite-length framing
70/// combinator. Serialization emits no bytes.
71#[derive(Clone, Copy)]
72pub struct BerEndFmt;
73
74/// BER constructed-content boundary.
75pub const BER_END: BerEndFmt = BerEndFmt;
76
77pub open spec fn at_ber_end(input: Seq<u8>) -> bool {
78    input.len() == 0 || EOC.spec_parse(input) is Some
79}
80
81impl SpecParser for BerEndFmt {
82    type PVal = ();
83
84    open spec fn spec_parse(&self, input: Seq<u8>) -> Option<(int, Self::PVal)> {
85        if at_ber_end(input) {
86            Some((0, ()))
87        } else {
88            None
89        }
90    }
91}
92
93impl Consistency for BerEndFmt {
94    type Val = ();
95
96    open spec fn consistent(&self, _value: Self::Val) -> bool {
97        true
98    }
99}
100
101impl AdmitsUniqueVal for BerEndFmt {
102    proof fn lemma_unique_consistent_val(&self, _left: Self::Val, _right: Self::Val) {
103    }
104}
105
106impl SpecSerializerDps for BerEndFmt {
107    type SValue = ();
108
109    open spec fn spec_serialize_dps(&self, _value: Self::SValue, _obuf: Seq<u8>) -> Seq<u8> {
110        Seq::empty()
111    }
112}
113
114impl SpecSerializer for BerEndFmt {
115    type SVal = ();
116
117    open spec fn spec_serialize(&self, _value: Self::SVal) -> Seq<u8> {
118        Seq::empty()
119    }
120}
121
122impl SpecByteLen for BerEndFmt {
123    type T = ();
124
125    open spec fn byte_len(&self, _value: Self::T) -> nat {
126        0
127    }
128}
129
130impl SafeParser for BerEndFmt {
131    proof fn lemma_parse_safe(&self, _input: Seq<u8>) {
132    }
133}
134
135impl Productive for BerEndFmt {
136    open spec fn productive_inv(&self) -> bool {
137        false
138    }
139
140    proof fn lemma_productive(&self, _input: Seq<u8>) {
141    }
142}
143
144impl GoodSerializer for BerEndFmt {
145    proof fn lemma_serialize_len(&self, _value: Self::SVal) {
146    }
147}
148
149impl EquivSerializers for BerEndFmt {
150    proof fn lemma_serialize_equiv_on_empty(&self, _value: Self::SVal) {
151    }
152}
153
154impl SPRoundTripDps for BerEndFmt {
155    proof fn theorem_serialize_dps_parse_roundtrip(&self, _value: Self::T, _obuf: Seq<u8>) {
156    }
157}
158
159impl<'i> Parser<&'i [u8]> for BerEndFmt {
160    type PT = ();
161
162    fn parse(&self, input: &&'i [u8]) -> PResult<Self::PT> {
163        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
164
165        proof {
166            crate::core::exec::bridge_lemmas::lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&EOC);
167        }
168        if input.len() == 0 {
169            Ok((0, ()))
170        } else {
171            match EOC.parse(input) {
172                Ok(_) => Ok((0, ())),
173                Err(_) => Err(ParseError::custom("expected end of BER constructed contents")),
174            }
175        }
176    }
177}
178
179impl<Output: OutputBuf> Serializer<Output, ()> for BerEndFmt {
180    fn serialize_into(&self, _value: &(), _obuf: &mut Output) {
181        broadcast use crate::core::exec::output::outbuf_lemmas;
182
183    }
184}
185
186impl Prepare<()> for BerEndFmt {
187    fn prepare(&self, _value: &()) -> Result<usize, PreSerializeError> {
188        Ok(0)
189    }
190}
191
192impl ByteLen<()> for BerEndFmt {
193    fn length(&self, _value: &()) -> usize {
194        0
195    }
196}
197
198/// A parsed value together with the exact octets consumed for it.
199///
200/// Recursive BER ANY needs this small internal layer because the contents of an
201/// indefinite-length parent are the original child TLVs, including any legal
202/// non-canonical BER tag or length encodings.
203#[verifier::ext_equal]
204#[doc(hidden)]
205pub struct Captured<T> {
206    pub value: T,
207    pub encoded: Seq<u8>,
208}
209
210/// Specification-only wrapper retaining the exact input prefix consumed by `C`.
211#[doc(hidden)]
212pub struct Capture<C>(pub C);
213
214impl<C: SpecParser> SpecParser for Capture<C> {
215    type PVal = Captured<C::PVal>;
216
217    open spec fn spec_parse(&self, input: Seq<u8>) -> Option<(int, Self::PVal)> {
218        match self.0.spec_parse(input) {
219            Some((n, value)) => Some((n, Captured { value, encoded: input.take(n) })),
220            None => None,
221        }
222    }
223}
224
225impl<C: SpecCombinator> Consistency for Capture<C> {
226    type Val = Captured<C::T>;
227
228    open spec fn consistent(&self, value: Self::Val) -> bool {
229        self.0.consistent(value.value)
230    }
231}
232
233impl<C: SpecCombinator> SpecSerializerDps for Capture<C> {
234    type SValue = Captured<C::T>;
235
236    open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
237        value.encoded + obuf
238    }
239}
240
241impl<C: SpecCombinator> SpecSerializer for Capture<C> {
242    type SVal = Captured<C::T>;
243
244    open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
245        value.encoded
246    }
247}
248
249impl<C: SpecCombinator> SpecByteLen for Capture<C> {
250    type T = Captured<C::T>;
251
252    open spec fn byte_len(&self, value: Self::T) -> nat {
253        value.encoded.len()
254    }
255}
256
257impl<C: SpecCombinator + SafeParser> SafeParser for Capture<C> {
258    open spec fn safe_inv(&self) -> bool {
259        self.0.safe_inv()
260    }
261
262    proof fn lemma_parse_safe(&self, input: Seq<u8>) {
263        self.0.lemma_parse_safe(input);
264    }
265}
266
267impl<C: SpecCombinator + Productive> Productive for Capture<C> {
268    open spec fn productive_inv(&self) -> bool {
269        self.0.productive_inv()
270    }
271
272    proof fn lemma_productive(&self, input: Seq<u8>) {
273        self.0.lemma_productive(input);
274    }
275}
276
277type BerAnyWireType = (
278    Tag,
279    Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, EocValue), Never>>), Never>,
280);
281
282type BerAnyRawBodyFmt<Rec> = Bind<
283    TagFmt,
284    spec_fn(Tag) -> Sum<
285        Bind<
286            BerLengthFmt,
287            spec_fn(BerLength) -> Sum<ExactLen<Tail, usize>, Sum<Repeat<Rec, EocFmt>, Void>>,
288        >,
289        Void,
290    >,
291>;
292
293type BerAnyMappedBodyFmt<Rec> = Mapped<
294    BerAnyRawBodyFmt<Rec>,
295    FnSpecMapper<BerAnyWireType, AnySpec>,
296>;
297
298type BerAnyBodyFmt<Rec> = Capture<BerAnyMappedBodyFmt<Rec>>;
299
300pub open spec fn captured_any_contents(children: Seq<Captured<AnySpec>>) -> Seq<u8> {
301    children.map(|_i: int, child: Captured<AnySpec>| child.encoded).flatten()
302}
303
304/// One recursive unfolding of a BER open type.
305///
306/// Definite values retain their opaque contents. Indefinite values are legal only for
307/// constructed tags and retain the exact encodings of their child TLVs, excluding the
308/// terminating EOC. EOC itself is never accepted as an ANY value.
309pub open spec fn ber_any_rec_body(rec: ParamRecSpecs<(), Captured<AnySpec>>) -> BerAnyBodyFmt<
310    BundledSpecs<Captured<AnySpec>>,
311> {
312    #[verusfmt::skip]
313    Capture(Mapped {
314        inner: Bind(TagFmt, |tag: Tag|
315            if tag == TagFmt::EOC {
316                R(Void("EOC is not an open-type value"))
317            } else {
318                L(Bind(BerLengthFmt, |length: BerLength|
319                    match length {
320                        BerLength::Definite(len) =>
321                            L(ExactLen(len, Tail)),
322                        BerLength::Indefinite if tag.constructed =>
323                            R(L(Repeat(rec(()), EOC))),
324                        BerLength::Indefinite =>
325                            R(R(Void("Primitive values cannot use indefinite length"))),
326                    },
327                ))
328            },
329        ),
330        mapper: (
331            |parsed: BerAnyWireType| {
332                match parsed.1 {
333                    L((_length, L(content))) =>
334                        AnySpec { tag: parsed.0, content },
335                    L((_length, R(L((children, _eoc))))) =>
336                        AnySpec {
337                            tag: parsed.0,
338                            content: captured_any_contents(children),
339                        },
340                    L((_length, R(R(_)))) => arbitrary(),
341                    R(_) => arbitrary(),
342                }
343            },
344            |value: AnySpec| (
345                value.tag,
346                L((
347                    BerLength::Definite(value.content.len() as usize),
348                    L(value.content),
349                )),
350            ),
351        ),
352    })
353}
354
355pub struct BerAnyRecBody;
356
357impl SpecRecBody for BerAnyRecBody {
358    type Param = ();
359
360    type T = Captured<AnySpec>;
361
362    type Body = BerAnyBodyFmt<BundledSpecs<Captured<AnySpec>>>;
363
364    open spec fn spec_body(
365        &self,
366        _param: (),
367        rec: ParamRecSpecs<(), Captured<AnySpec>>,
368    ) -> Self::Body {
369        ber_any_rec_body(rec)
370    }
371}
372
373mod recursive_proofs {
374    use super::*;
375
376    impl SafeParserRecBody for BerAnyRecBody {
377        proof fn lemma_body_safe_inv_preservation(
378            &self,
379            _param: (),
380            rec: ParamRecSpecs<(), Captured<AnySpec>>,
381        ) {
382        }
383    }
384
385    impl ProductiveRecBody for BerAnyRecBody {
386        proof fn lemma_body_productive_inv_preservation(
387            &self,
388            _param: (),
389            rec: ParamRecSpecs<(), Captured<AnySpec>>,
390        ) {
391        }
392    }
393
394}
395
396/// BER ANY/open type with bounded nesting for indefinite-length constructed values.
397///
398/// Parsing accepts definite values and recursively framed indefinite constructed values.
399/// Serialization is normalized to a definite-length encoding.
400#[derive(Clone, Copy)]
401pub struct BerAnyFmt<const LIMIT: usize>;
402
403pub open spec fn ber_any_parse<const LIMIT: usize>(input: Seq<u8>) -> Option<(int, AnySpec)> {
404    match AnyFmt::<BER>.spec_parse(input) {
405        Some(parsed) => Some(parsed),
406        None => match FixWith::<LIMIT, _, _>(BerAnyRecBody, ()).spec_parse(input) {
407            Some((n, captured)) => Some((n, captured.value)),
408            None => None,
409        },
410    }
411}
412
413mod derived_specs {
414    use super::*;
415
416    impl<const LIMIT: usize> SpecParser for BerAnyFmt<LIMIT> {
417        type PVal = AnySpec;
418
419        open spec fn spec_parse(&self, input: Seq<u8>) -> Option<(int, Self::PVal)> {
420            ber_any_parse::<LIMIT>(input)
421        }
422    }
423
424    impl<const LIMIT: usize> Consistency for BerAnyFmt<LIMIT> {
425        type Val = AnySpec;
426
427        open spec fn consistent(&self, value: Self::Val) -> bool {
428            AnyFmt::<BER>.consistent(value)
429        }
430    }
431
432    impl<const LIMIT: usize> SpecSerializerDps for BerAnyFmt<LIMIT> {
433        type SValue = AnySpec;
434
435        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
436            AnyFmt::<BER>.spec_serialize_dps(value, obuf)
437        }
438    }
439
440    impl<const LIMIT: usize> SpecSerializer for BerAnyFmt<LIMIT> {
441        type SVal = AnySpec;
442
443        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
444            AnyFmt::<BER>.spec_serialize(value)
445        }
446    }
447
448    impl<const LIMIT: usize> SpecByteLen for BerAnyFmt<LIMIT> {
449        type T = AnySpec;
450
451        open spec fn byte_len(&self, value: Self::T) -> nat {
452            AnyFmt::<BER>.byte_len(value)
453        }
454    }
455
456}
457
458mod derived_proofs {
459    use super::*;
460
461    impl<const LIMIT: usize> SafeParser for BerAnyFmt<LIMIT> {
462        proof fn lemma_parse_safe(&self, input: Seq<u8>) {
463            AnyFmt::<BER>.lemma_parse_safe(input);
464            FixWith::<LIMIT, _, _>(BerAnyRecBody, ()).lemma_parse_safe(input);
465        }
466    }
467
468    impl<const LIMIT: usize> Productive for BerAnyFmt<LIMIT> {
469        proof fn lemma_productive(&self, input: Seq<u8>) {
470            AnyFmt::<BER>.lemma_productive(input);
471            FixWith::<LIMIT, _, _>(BerAnyRecBody, ()).lemma_productive(input);
472        }
473    }
474
475    impl<const LIMIT: usize> GoodSerializer for BerAnyFmt<LIMIT> {
476        proof fn lemma_serialize_len(&self, value: AnySpec) {
477            AnyFmt::<BER>.lemma_serialize_len(value);
478        }
479    }
480
481    impl<const LIMIT: usize> NonTailFmt for BerAnyFmt<LIMIT> {
482        proof fn lemma_serialize_dps_prepend(&self, value: AnySpec, obuf: Seq<u8>) {
483            AnyFmt::<BER>.lemma_serialize_dps_prepend(value, obuf);
484        }
485
486        proof fn lemma_serialize_dps_len(&self, value: AnySpec, obuf: Seq<u8>) {
487            AnyFmt::<BER>.lemma_serialize_dps_len(value, obuf);
488        }
489    }
490
491    impl<const LIMIT: usize> EquivSerializersGeneral for BerAnyFmt<LIMIT> {
492        proof fn lemma_serialize_equiv(&self, value: AnySpec, obuf: Seq<u8>) {
493            AnyFmt::<BER>.lemma_serialize_equiv(value, obuf);
494        }
495    }
496
497    impl<const LIMIT: usize> EquivSerializers for BerAnyFmt<LIMIT> {
498        proof fn lemma_serialize_equiv_on_empty(&self, value: AnySpec) {
499            self.lemma_serialize_equiv(value, Seq::empty());
500        }
501    }
502
503    impl<const LIMIT: usize> SPRoundTripDps for BerAnyFmt<LIMIT> {
504        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: AnySpec, obuf: Seq<u8>) {
505            AnyFmt::<BER>.theorem_serialize_dps_parse_roundtrip(value, obuf);
506        }
507    }
508
509}
510
511#[cfg(feature = "alloc")]
512impl<Output: OutputBuf, const LIMIT: usize> Serializer<Output, AnyOwned> for BerAnyFmt<LIMIT> {
513    fn serialize_into(&self, value: &AnyOwned, obuf: &mut Output) {
514        AnyFmt::<BER>.serialize_into(value, obuf)
515    }
516}
517
518#[cfg(feature = "alloc")]
519impl<const LIMIT: usize> Prepare<AnyOwned> for BerAnyFmt<LIMIT> {
520    fn prepare(&self, value: &AnyOwned) -> Result<usize, PreSerializeError> {
521        AnyFmt::<BER>.prepare(value)
522    }
523}
524
525#[cfg(feature = "alloc")]
526impl<const LIMIT: usize> ByteLen<AnyOwned> for BerAnyFmt<LIMIT> {
527    fn length(&self, value: &AnyOwned) -> usize {
528        AnyFmt::<BER>.length(value)
529    }
530}
531
532#[cfg(feature = "alloc")]
533#[doc(hidden)]
534pub struct CapturedAnyOwned {
535    pub value: AnyOwned,
536    pub encoded: Vec<u8>,
537}
538
539#[cfg(feature = "alloc")]
540impl DeepView for CapturedAnyOwned {
541    type V = Captured<AnySpec>;
542
543    closed spec fn deep_view(&self) -> Self::V {
544        Captured { value: self.value.deep_view(), encoded: self.encoded.deep_view() }
545    }
546}
547
548#[cfg(feature = "alloc")]
549fn flatten_captured_any_contents(children: Vec<CapturedAnyOwned>) -> (content: Vec<u8>)
550    ensures
551        content.deep_view() == captured_any_contents(children.deep_view()),
552{
553    broadcast use vstd::seq_lib::group_seq_properties;
554
555    let ghost child_views = children.deep_view();
556    let ghost encoded_views = child_views.map(|_i: int, child: Captured<AnySpec>| child.encoded);
557    let mut content = Vec::new();
558    for i in 0..children.len()
559        invariant
560            children.deep_view() == child_views,
561            encoded_views == child_views.map(|_i: int, child: Captured<AnySpec>| child.encoded),
562            content.deep_view() == encoded_views.take(i as int).flatten(),
563    {
564        let encoded = children[i].encoded.as_slice();
565        proof {
566            let prefix = encoded_views.take(i as int);
567            prefix.lemma_flatten_push(encoded.deep_view());
568            assert(encoded_views[i as int] == encoded.deep_view());
569            assert(encoded_views.take(i as int + 1) == prefix.push(encoded.deep_view()));
570        }
571        content.extend_from_slice(encoded);
572    }
573    content
574}
575
576#[cfg(feature = "alloc")]
577spec fn flattened_captured_any_result(
578    result: Option<(int, (Seq<Captured<AnySpec>>, EocValue))>,
579) -> Option<(int, Seq<u8>)> {
580    match result {
581        Some((n, (children, _eoc))) => Some((n, captured_any_contents(children))),
582        None => None,
583    }
584}
585
586#[cfg(feature = "alloc")]
587fn parse_captured_any_children<I, P>(parser: &P, input: &I) -> (result: PResult<Vec<u8>>) where
588    I: InputBuf,
589    P: Parser<I, PT = (Vec<CapturedAnyOwned>, EocValue), PVal = (Seq<Captured<AnySpec>>, EocValue)>,
590
591    requires
592        parser.exec_inv(),
593    ensures
594        parse_matches_spec(result, flattened_captured_any_result(parser.spec_parse(input@))),
595{
596    let (n, (children, _eoc)) = parser.parse(input)?;
597    let content = flatten_captured_any_contents(children);
598    Ok((n, content))
599}
600
601#[cfg(feature = "alloc")]
602impl<'i> ParserRecBody<&'i [u8]> for BerAnyRecBody {
603    type EP = ();
604
605    type O = CapturedAnyOwned;
606
607    fn parse_body<Exec>(
608        &self,
609        _param: &(),
610        Ghost(spec_rec): Ghost<ParamRecSpecs<(), Captured<AnySpec>>>,
611        exec_rec: Exec,
612        ibuf: &&'i [u8],
613    ) -> PResult<CapturedAnyOwned> where Exec: Fn(&(), &&'i [u8]) -> PResult<CapturedAnyOwned> {
614        use crate::combinators::congruence::*;
615        use crate::core::exec::bridge_lemmas::*;
616
617        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
618        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
619        broadcast use lemma_parser_congruent_reflexive;
620
621        let _ = ibuf.len();
622        let (tag_len, tag) = TagFmt.parse(ibuf)?;
623        if tag == TagFmt::EOC {
624            return Err(ParseError::invalid_tag());
625        }
626        let after_tag = ibuf.skip(tag_len);
627        let (length_len, length) = BerLengthFmt.parse(&after_tag)?;
628        let contents = after_tag.skip(length_len);
629
630        let (content_len, value) = match length {
631            BerLength::Definite(len) => {
632                let (content_len, content) = ExactLen(len, Tail).parse(&contents)?;
633                let content = slice_to_vec(content);
634                let value = AnyOwned::new(tag, content);
635                (content_len, value)
636            },
637            BerLength::Indefinite => {
638                if !tag.constructed {
639                    return Err(ParseError::custom("Primitive values cannot use indefinite length"));
640                }
641                let ghost child_spec = spec_rec(());
642                let child_exec = |input: &&'i [u8]| -> (r: PResult<CapturedAnyOwned>)
643                    ensures
644                        parse_matches_spec(r, child_spec.2(input@)),
645                    { exec_rec(&(), input) };
646                let child: &FnParser<
647                    &'i [u8],
648                    CapturedAnyOwned,
649                    BundledSpecs<Captured<AnySpec>>,
650                    _,
651                > = &FnParser::new(child_exec, Ghost(child_spec));
652                proof {
653                    lemma_ref_parser_exec_inv::<&'i [u8], _>(child);
654                    lemma_ref_safe_productive_inv(child);
655                    lemma_ref_fn_parser_congruence(child);
656                }
657                let repeated = Repeat(child, EOC);
658                proof {
659                    lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&EOC);
660                    lemma_repeat_parser_exec_inv::<&'i [u8], _, _>(&repeated);
661                    lemma_repeat_parser_congruence(child, child_spec, EOC, EOC);
662                    reveal(parser_congruent);
663                }
664                let (content_len, content) = parse_captured_any_children(&repeated, &contents)?;
665                let value = AnyOwned::new(tag, content);
666                (content_len, value)
667            },
668        };
669
670        let total = tag_len + length_len + content_len;
671        let encoded = slice_to_vec(ibuf.take(total));
672        Ok((total, CapturedAnyOwned { value, encoded }))
673    }
674}
675
676#[cfg(feature = "alloc")]
677impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerAnyFmt<LIMIT> {
678    type PT = AnyOwned;
679
680    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
681        match AnyFmt::<BER>.parse(ibuf) {
682            Ok((n, value)) => {
683                let tag = value.tag();
684                let content = slice_to_vec(value.content());
685                Ok((n, AnyOwned::new(tag, content)))
686            },
687            Err(_) => {
688                let (n, captured) = FixWith::<LIMIT, _, _>(BerAnyRecBody, ()).parse(ibuf)?;
689                Ok((n, captured.value))
690            },
691        }
692    }
693}
694
695} // verus!
vest_lib/asn1/ber/any.rs

vest_lib/asn1/ber/
any.rs
