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    open spec fn exec_inv(&self) -> bool {
267        &&& self.1.exec_inv()
268        &&& self.1.safe_inv()
269        &&& self.1.productive_inv()
270    }
271
272    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
273        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
274        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
275
276        let _ = ibuf.len();
277        let (tag_len, _tag) = Const(TagFmt, self.0).parse(ibuf)?;
278        let after_tag = ibuf.skip(tag_len);
279        let (length_len, length) = BerLengthFmt.parse(&after_tag)?;
280        let content = after_tag.skip(length_len);
281
282        let (content_len, values) = match length {
283            BerLength::Definite(len) => {
284                let exact = ExactLen(len, RepeatTillEnd(self.1));
285                exact.parse(&content)?
286            },
287            BerLength::Indefinite => {
288                let repeated = Repeat(self.1, EOC);
289                proof {
290                    crate::core::exec::bridge_lemmas::lemma_pair_parser_exec_inv::<&'i [u8], _, _>(
291                        &EOC,
292                    );
293                    crate::core::exec::bridge_lemmas::lemma_repeat_parser_exec_inv::<
294                        &'i [u8],
295                        _,
296                        _,
297                    >(&repeated);
298                }
299                parse_discard_eoc(&repeated, &content)?
300            },
301        };
302        let total = tag_len + length_len + content_len;
303        assert(self.spec_parse(ibuf@) == Some((total as int, values.deep_view())));
304        Ok((total, values))
305    }
306}
307
308impl<Output: OutputBuf, C, T> Serializer<Output, &[T]> for BerSequenceOfFmt<C> where
309    C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,
310    T: DeepView,
311 {
312    #[verifier::prophetic]
313    open spec fn exec_inv(&self) -> bool {
314        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
315        &&& <C as ByteLen<T>>::exec_inv(&self.1)
316    }
317
318    fn serialize_into(&self, value: &&[T], obuf: &mut Output) {
319        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
320        normalized.serialize_into(value, obuf);
321    }
322}
323
324impl<C, T> Prepare<&[T]> for BerSequenceOfFmt<C> where
325    C: SpecCombinator + Prepare<T> + Copy,
326    T: DeepView,
327 {
328    open spec fn exec_inv(&self) -> bool {
329        <C as Prepare<T>>::exec_inv(&self.1)
330    }
331
332    fn prepare(&self, value: &&[T]) -> Result<usize, PreSerializeError> {
333        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
334        normalized.prepare(value)
335    }
336}
337
338impl<C, T> ByteLen<&[T]> for BerSequenceOfFmt<C> where
339    C: SpecCombinator + ByteLen<T> + Copy,
340    T: DeepView,
341 {
342    open spec fn exec_inv(&self) -> bool {
343        <C as ByteLen<T>>::exec_inv(&self.1)
344    }
345
346    fn length(&self, value: &&[T]) -> usize {
347        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
348        normalized.length(value)
349    }
350}
351
352#[cfg(feature = "alloc")]
353impl<Output: OutputBuf, C, T> Serializer<Output, Vec<T>> for BerSequenceOfFmt<C> where
354    C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,
355    T: DeepView,
356 {
357    #[verifier::prophetic]
358    open spec fn exec_inv(&self) -> bool {
359        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
360        &&& <C as ByteLen<T>>::exec_inv(&self.1)
361    }
362
363    fn serialize_into(&self, value: &Vec<T>, obuf: &mut Output) {
364        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
365        normalized.serialize_into(value, obuf);
366    }
367}
368
369#[cfg(feature = "alloc")]
370impl<C, T> Prepare<Vec<T>> for BerSequenceOfFmt<C> where
371    C: SpecCombinator + Prepare<T> + Copy,
372    T: DeepView,
373 {
374    open spec fn exec_inv(&self) -> bool {
375        <C as Prepare<T>>::exec_inv(&self.1)
376    }
377
378    fn prepare(&self, value: &Vec<T>) -> Result<usize, PreSerializeError> {
379        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
380        normalized.prepare(value)
381    }
382}
383
384#[cfg(feature = "alloc")]
385impl<C, T> ByteLen<Vec<T>> for BerSequenceOfFmt<C> where
386    C: SpecCombinator + ByteLen<T> + Copy,
387    T: DeepView,
388 {
389    open spec fn exec_inv(&self) -> bool {
390        <C as ByteLen<T>>::exec_inv(&self.1)
391    }
392
393    fn length(&self, value: &Vec<T>) -> usize {
394        let normalized = ASN1Fmt::<_, BER>(self.0, RepeatTillEnd(self.1));
395        normalized.length(value)
396    }
397}
398
399} // verus!
vest_lib/asn1/ber/sequence_of.rs

vest_lib/asn1/ber/
sequence_of.rs
