vest_lib/asn1/ber/
sequence_of.rs

1//! BER SEQUENCE OF / SET OF element list combinators.
2use crate::asn1::{ASN1Fmt, BerLength, BerLengthFmt, Class, Tag, TagFmt, BER};
3use crate::combinators::{
4    bytes::ExactLen, mapped::spec::FnSpecMapper, tail::RepeatTillEnd, Bind, Const, Mapped,
5    PrefixTagged, Repeat, Sum,
6};
7use crate::core::exec::input::InputBuf;
8use crate::core::exec::parser::*;
9use crate::core::exec::{
10    ByteLen, OutputBuf, PResult, ParseError, ParseErrorKind, Parser, PreSerializeError, Prepare,
11    Serializer,
12};
13use crate::core::{proof::*, spec::*};
14#[cfg(feature = "alloc")]
15use alloc::vec::Vec;
16use vstd::prelude::*;
17
18use super::any::{parse_discard_eoc, EocFmt, EocValue, EOC};
19use Sum::Inl as L;
20use Sum::Inr as R;
21
22verus! {
23
24type BerSequenceOfWireType<T> = (BerLength, Sum<Seq<T>, (Seq<T>, EocValue)>);
25
26type BerSequenceOfInnerFmt<C> = Mapped<
27    PrefixTagged<
28        TagFmt,
29        Tag,
30        Bind<
31            BerLengthFmt,
32            spec_fn(BerLength) -> Sum<ExactLen<RepeatTillEnd<C>, usize>, Repeat<C, EocFmt>>,
33        >,
34    >,
35    FnSpecMapper<BerSequenceOfWireType<<C as SpecByteLen>::T>, Seq<<C as SpecByteLen>::T>>,
36>;
37
38/// BER `SEQUENCE OF` accepting definite and indefinite outer length forms.
39///
40/// The indefinite branch is non-recursive at this layer: [`Repeat`] parses complete ASN.1
41/// elements until [`EOC`]. Nested indefinite values are handled by the element codec itself.
42/// Serialization is normalized to the definite form.
43pub open spec fn ber_sequence_of_fmt<C: SpecCombinator>(
44    tag: Tag,
45    content: C,
46) -> BerSequenceOfInnerFmt<C> {
47    #[verusfmt::skip]
48    Mapped {
49        inner: PrefixTagged(TagFmt, tag, Bind(BerLengthFmt, |len: BerLength|
50                match len {
51                    BerLength::Definite(len) => L(ExactLen(len, RepeatTillEnd(content))),
52                    BerLength::Indefinite => R(Repeat(content, EOC)),
53                },
54            ),
55        ),
56        mapper: (
57            |parsed: BerSequenceOfWireType<C::T>|
58                match parsed.1 {
59                    L(values) => values,
60                    R((values, _eoc)) => values,
61                },
62            |values: Seq<C::T>|
63                {
64                    let len = RepeatTillEnd(content).byte_len(values) as usize;
65                    (BerLength::Definite(len), L(values))
66                },
67        ),
68    }
69}
70
71/// The definite-length BER encoding selected by [`BerSequenceOfFmt`]'s serializer.
72pub open spec fn ber_sequence_of_normalized_fmt<C>(tag: Tag, content: C) -> ASN1Fmt<
73    RepeatTillEnd<C>,
74    BER,
75> {
76    ASN1Fmt(tag, RepeatTillEnd(content))
77}
78
79/// BER `SEQUENCE OF` codec with a configurable outer tag.
80///
81/// Parsing accepts either a definite-length contents or an indefinite-length sequence
82/// terminated by [`EOC`]. Each element must be a productive, complete ASN.1 TLV; in particular,
83/// its parser must not accept [`EOC`] as an element. Serialization always emits definite-length BER.
84#[derive(Copy)]
85pub struct BerSequenceOfFmt<C>(pub Tag, pub C);
86
87impl<C: Clone> Clone for BerSequenceOfFmt<C> {
88    fn clone(&self) -> (cloned: Self)
89        ensures
90            cloned.0 == self.0,
91            call_ensures(C::clone, (&self.1,), cloned.1),
92    {
93        BerSequenceOfFmt(self.0, self.1.clone())
94    }
95}
96
97impl<C: Copy> BerSequenceOfFmt<C> {
98    /// Ordinary universal `SEQUENCE OF`.
99    #[verifier::allow_in_spec]
100    pub const fn universal(content: C) -> Self
101        returns
102            Self(TagFmt::SEQUENCE, content),
103    {
104        Self(TagFmt::SEQUENCE, content)
105    }
106
107    /// An IMPLICIT-tagged `SEQUENCE OF`.
108    #[verifier::allow_in_spec]
109    pub const fn implicit(class: Class, number: u64, content: C) -> Self
110        returns
111            Self(
112                Tag {
113                    class,
114                    constructed: true,
115                    number: crate::asn1::tag::tag_num_from_uint(number),
116                },
117                content,
118            ),
119    {
120        Self(
121            Tag { class, constructed: true, number: crate::asn1::tag::tag_num_from_uint(number) },
122            content,
123        )
124    }
125}
126
127mod derived_specs {
128    use super::*;
129
130    impl<C: SpecCombinator> SpecParser for BerSequenceOfFmt<C> {
131        type PVal = Seq<C::T>;
132
133        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
134            ber_sequence_of_fmt(self.0, self.1).spec_parse(ibuf)
135        }
136    }
137
138    impl<C: SpecCombinator> Consistency for BerSequenceOfFmt<C> {
139        type Val = Seq<C::T>;
140
141        open spec fn consistent(&self, value: Self::Val) -> bool {
142            ber_sequence_of_fmt(self.0, self.1).consistent(value)
143        }
144    }
145
146    impl<C: SpecCombinator> SpecSerializerDps for BerSequenceOfFmt<C> {
147        type SValue = Seq<C::T>;
148
149        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
150            ber_sequence_of_fmt(self.0, self.1).spec_serialize_dps(value, obuf)
151        }
152    }
153
154    impl<C: SpecCombinator> SpecSerializer for BerSequenceOfFmt<C> {
155        type SVal = Seq<C::T>;
156
157        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
158            ber_sequence_of_fmt(self.0, self.1).spec_serialize(value)
159        }
160    }
161
162    impl<C: SpecCombinator> SpecByteLen for BerSequenceOfFmt<C> {
163        type T = Seq<C::T>;
164
165        open spec fn byte_len(&self, value: Self::T) -> nat {
166            ber_sequence_of_fmt(self.0, self.1).byte_len(value)
167        }
168    }
169
170}
171
172mod derived_proofs {
173    use super::*;
174
175    impl<C: SpecCombinator + SafeParser> SafeParser for BerSequenceOfFmt<C> {
176        open spec fn safe_inv(&self) -> bool {
177            self.1.safe_inv()
178        }
179
180        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
181            ber_sequence_of_fmt(self.0, self.1).lemma_parse_safe(ibuf);
182        }
183    }
184
185    impl<C: SpecCombinator + SafeParser> Productive for BerSequenceOfFmt<C> {
186        open spec fn productive_inv(&self) -> bool {
187            self.1.safe_inv()
188        }
189
190        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
191            ber_sequence_of_fmt(self.0, self.1).lemma_productive(ibuf);
192        }
193    }
194
195    impl<C: SpecCombinator + GoodSerializer> GoodSerializer for BerSequenceOfFmt<C> {
196        open spec fn serialize_inv(&self) -> bool {
197            self.1.serialize_inv()
198        }
199
200        proof fn lemma_serialize_len(&self, value: Self::SVal) {
201            ber_sequence_of_fmt(self.0, self.1).lemma_serialize_len(value);
202        }
203    }
204
205    impl<
206        C: SpecCombinator + GoodSerializer + EquivSerializersGeneral,
207    > NonTailFmt for BerSequenceOfFmt<C> {
208        open spec fn serialize_dps_inv(&self) -> bool {
209            &&& self.1.serialize_inv()
210            &&& self.1.equiv_general_inv()
211        }
212
213        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
214            ber_sequence_of_normalized_fmt(self.0, self.1).lemma_serialize_dps_prepend(value, obuf);
215        }
216
217        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
218            ber_sequence_of_normalized_fmt(self.0, self.1).lemma_serialize_dps_len(value, obuf);
219        }
220    }
221
222    impl<C: SpecCombinator + EquivSerializersGeneral> EquivSerializersGeneral for BerSequenceOfFmt<
223        C,
224    > {
225        open spec fn equiv_general_inv(&self) -> bool {
226            self.1.equiv_general_inv()
227        }
228
229        proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
230            ber_sequence_of_normalized_fmt(self.0, self.1).lemma_serialize_equiv(value, obuf);
231        }
232    }
233
234    impl<C: SpecCombinator + EquivSerializersGeneral> EquivSerializers for BerSequenceOfFmt<C> {
235        open spec fn equiv_inv(&self) -> bool {
236            self.1.equiv_general_inv()
237        }
238
239        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
240            self.lemma_serialize_equiv(value, Seq::empty());
241        }
242    }
243
244    impl<C> SPRoundTripDps for BerSequenceOfFmt<C> where
245        C:
246            SpecCombinator + Productive + GoodSerializer + NonTailFmt + SPRoundTripDps + EquivSerializersGeneral,
247     {
248        open spec fn unambiguous(&self) -> bool {
249            &&& RepeatTillEnd(self.1).sp_roundtrip_inv()
250            &&& disjoint_domains(self.1, EOC)
251        }
252
253        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
254            ber_sequence_of_fmt(self.0, self.1).theorem_serialize_dps_parse_roundtrip(value, obuf);
255        }
256    }
257
258}
259
260#[cfg(feature = "alloc")]
261impl<'i, C> Parser<&'i [u8]> for BerSequenceOfFmt<C> where
262    C: SpecCombinator + Parser<&'i [u8]> + Productive + Copy,
263 {
264    type PT = Vec<C::PT>;
265
266    fn min_byte_len(&self) -> usize {
267        // An empty value has an identifier and a length octet.
268        2
269    }
270
271    open spec fn exec_inv(&self) -> bool {
272        &&& self.1.exec_inv()
273        &&& self.1.safe_inv()
274        &&& self.1.productive_inv()
275    }
276
277    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
278        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
279        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
280
281        let _ = ibuf.len();
282        let (tag_len, _tag) = Const(TagFmt, self.0).parse(ibuf)?;
283        let after_tag = ibuf.skip(tag_len);
284        let (length_len, length) = BerLengthFmt.parse(&after_tag)?;
285        let content = after_tag.skip(length_len);
286
287        let (content_len, values) = match length {
288            BerLength::Definite(len) => {
289                let exact = ExactLen(len, RepeatTillEnd(self.1));
290                exact.parse(&content)?
291            },
292            BerLength::Indefinite => {
293                let repeated = Repeat(self.1, EOC);
294                proof {
295                    crate::core::exec::bridge_lemmas::lemma_pair_parser_exec_inv::<&'i [u8], _, _>(
296                        &EOC,
297                    );
298                    crate::core::exec::bridge_lemmas::lemma_repeat_parser_exec_inv::<
299                        &'i [u8],
300                        _,
301                        _,
302                    >(&repeated);
303                }
304                parse_discard_eoc(&repeated, &content)?
305            },
306        };
307        let total = tag_len + length_len + content_len;
308        assert(self.spec_parse(ibuf@) == Some((total as int, values.deep_view())));
309        Ok((total, values))
310    }
311}
312
313impl<Output: OutputBuf, C, T> Serializer<Output, &[T]> for BerSequenceOfFmt<C> where
314    C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,
315    T: DeepView,
316 {
317    #[verifier::prophetic]
318    open spec fn exec_inv(&self) -> bool {
319        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
320        &&& <C as ByteLen<T>>::exec_inv(&self.1)
321    }
322
323    fn serialize_into(&self, value: &&[T], obuf: &mut Output) {
324        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
325        normalized.serialize_into(value, obuf);
326    }
327}
328
329impl<C, T> Prepare<&[T]> for BerSequenceOfFmt<C> where
330    C: SpecCombinator + Prepare<T> + Copy,
331    T: DeepView,
332 {
333    open spec fn exec_inv(&self) -> bool {
334        <C as Prepare<T>>::exec_inv(&self.1)
335    }
336
337    fn prepare(&self, value: &&[T]) -> Result<usize, PreSerializeError> {
338        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
339        normalized.prepare(value)
340    }
341}
342
343impl<C, T> ByteLen<&[T]> for BerSequenceOfFmt<C> where
344    C: SpecCombinator + ByteLen<T> + Copy,
345    T: DeepView,
346 {
347    open spec fn exec_inv(&self) -> bool {
348        <C as ByteLen<T>>::exec_inv(&self.1)
349    }
350
351    fn length(&self, value: &&[T]) -> usize {
352        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
353        normalized.length(value)
354    }
355}
356
357#[cfg(feature = "alloc")]
358impl<Output: OutputBuf, C, T> Serializer<Output, Vec<T>> for BerSequenceOfFmt<C> where
359    C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,
360    T: DeepView,
361 {
362    #[verifier::prophetic]
363    open spec fn exec_inv(&self) -> bool {
364        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
365        &&& <C as ByteLen<T>>::exec_inv(&self.1)
366    }
367
368    fn serialize_into(&self, value: &Vec<T>, obuf: &mut Output) {
369        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
370        normalized.serialize_into(value, obuf);
371    }
372}
373
374#[cfg(feature = "alloc")]
375impl<C, T> Prepare<Vec<T>> for BerSequenceOfFmt<C> where
376    C: SpecCombinator + Prepare<T> + Copy,
377    T: DeepView,
378 {
379    open spec fn exec_inv(&self) -> bool {
380        <C as Prepare<T>>::exec_inv(&self.1)
381    }
382
383    fn prepare(&self, value: &Vec<T>) -> Result<usize, PreSerializeError> {
384        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
385        normalized.prepare(value)
386    }
387}
388
389#[cfg(feature = "alloc")]
390impl<C, T> ByteLen<Vec<T>> for BerSequenceOfFmt<C> where
391    C: SpecCombinator + ByteLen<T> + Copy,
392    T: DeepView,
393 {
394    open spec fn exec_inv(&self) -> bool {
395        <C as ByteLen<T>>::exec_inv(&self.1)
396    }
397
398    fn length(&self, value: &Vec<T>) -> usize {
399        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
400        normalized.length(value)
401    }
402}
403
404} // verus!
vest_lib/asn1/ber/sequence_of.rs

vest_lib/asn1/ber/
sequence_of.rs
