vest_lib/asn1/ber/
sequence.rs

1//! BER SEQUENCE combinators.
2use crate::asn1::{ASN1Fmt, BerLength, BerLengthFmt, Class, Tag, TagFmt, BER};
3use crate::combinators::{
4    bytes::ExactLen, mapped::spec::FnSpecMapper, Bind, Const, Mapped, Pair, PrefixTagged, Sum,
5};
6use crate::core::exec::input::InputBuf;
7use crate::core::exec::parser::*;
8use crate::core::exec::{
9    ByteLen, OutputBuf, PResult, Parser, PreSerializeError, Prepare, Serializer,
10};
11use crate::core::{proof::*, spec::*};
12use vstd::prelude::*;
13
14use super::any::{parse_discard_eoc, EocFmt, EocValue, EOC};
15use Sum::Inl as L;
16use Sum::Inr as R;
17
18verus! {
19
20type BerSequenceWireType<T> = (BerLength, Sum<T, (T, EocValue)>);
21
22type BerSequenceFmt__<C> = Mapped<
23    PrefixTagged<
24        TagFmt,
25        Tag,
26        Bind<BerLengthFmt, spec_fn(BerLength) -> Sum<ExactLen<C, usize>, Pair<C, EocFmt>>>,
27    >,
28    FnSpecMapper<BerSequenceWireType<<C as SpecByteLen>::T>, <C as SpecByteLen>::T>,
29>;
30
31/// BER `SEQUENCE` accepting definite and indefinite outer length forms.
32///
33/// `content` ends in [`super::BerEndFmt`]. [`ExactLen`] makes that marker observe the end of a
34/// bounded definite body; under indefinite framing it recognizes EOC without consuming it, after
35/// which [`Pair`] consumes EOC. Serialization is normalized to definite-length BER.
36pub open spec fn ber_sequence_fmt<C: SpecCombinator>(tag: Tag, content: C) -> BerSequenceFmt__<C> {
37    #[verusfmt::skip]
38    Mapped {
39        inner: PrefixTagged(TagFmt, tag, Bind(BerLengthFmt, |len: BerLength|
40                match len {
41                    BerLength::Definite(len) => L(ExactLen(len, content)),
42                    BerLength::Indefinite => R(Pair(content, EOC)),
43                },
44            ),
45        ),
46        mapper: (
47            |parsed: BerSequenceWireType<C::T>|
48                match parsed.1 {
49                    L(value) => value,
50                    R((value, _eoc)) => value,
51                },
52            |value: C::T| {
53                let len = content.byte_len(value) as usize;
54                (BerLength::Definite(len), L(value))
55            },
56        ),
57    }
58}
59
60/// The definite-length BER encoding selected by [`BerSequenceFmt`]'s serializer.
61pub open spec fn ber_sequence_normalized_fmt<C>(tag: Tag, content: C) -> ASN1Fmt<C, BER> {
62    ASN1Fmt(tag, content)
63}
64
65/// BER `SEQUENCE` codec with a configurable outer tag.
66///
67/// Parsing accepts definite and indefinite framing for one schema body. Serialization always
68/// emits the normalized definite-length form.
69#[derive(Copy)]
70pub struct BerSequenceFmt<C>(pub Tag, pub C);
71
72impl<C: Clone> Clone for BerSequenceFmt<C> {
73    fn clone(&self) -> (cloned: Self)
74        ensures
75            cloned.0 == self.0,
76            call_ensures(C::clone, (&self.1,), cloned.1),
77    {
78        BerSequenceFmt(self.0, self.1.clone())
79    }
80}
81
82impl<C: Copy> BerSequenceFmt<C> {
83    /// Ordinary universal `SEQUENCE`.
84    #[verifier::allow_in_spec]
85    pub const fn universal(content: C) -> Self
86        returns
87            Self(TagFmt::SEQUENCE, content),
88    {
89        Self(TagFmt::SEQUENCE, content)
90    }
91
92    /// An IMPLICIT-tagged `SEQUENCE`.
93    #[verifier::allow_in_spec]
94    pub const fn implicit(class: Class, number: u64, content: C) -> Self
95        returns
96            Self(
97                Tag {
98                    class,
99                    constructed: true,
100                    number: crate::asn1::tag::tag_num_from_uint(number),
101                },
102                content,
103            ),
104    {
105        Self(
106            Tag { class, constructed: true, number: crate::asn1::tag::tag_num_from_uint(number) },
107            content,
108        )
109    }
110}
111
112mod derived_specs {
113    use super::*;
114
115    impl<C: SpecCombinator> SpecParser for BerSequenceFmt<C> {
116        type PVal = C::T;
117
118        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
119            ber_sequence_fmt(self.0, self.1).spec_parse(ibuf)
120        }
121    }
122
123    impl<C: SpecCombinator> Consistency for BerSequenceFmt<C> {
124        type Val = C::T;
125
126        open spec fn consistent(&self, value: Self::Val) -> bool {
127            ber_sequence_fmt(self.0, self.1).consistent(value)
128        }
129    }
130
131    impl<C: SpecCombinator> SpecSerializerDps for BerSequenceFmt<C> {
132        type SValue = C::T;
133
134        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
135            ber_sequence_fmt(self.0, self.1).spec_serialize_dps(value, obuf)
136        }
137    }
138
139    impl<C: SpecCombinator> SpecSerializer for BerSequenceFmt<C> {
140        type SVal = C::T;
141
142        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
143            ber_sequence_fmt(self.0, self.1).spec_serialize(value)
144        }
145    }
146
147    impl<C: SpecCombinator> SpecByteLen for BerSequenceFmt<C> {
148        type T = C::T;
149
150        open spec fn byte_len(&self, value: Self::T) -> nat {
151            ber_sequence_fmt(self.0, self.1).byte_len(value)
152        }
153    }
154
155}
156
157mod derived_proofs {
158    use super::*;
159
160    impl<C: SpecCombinator + SafeParser> SafeParser for BerSequenceFmt<C> {
161        open spec fn safe_inv(&self) -> bool {
162            self.1.safe_inv()
163        }
164
165        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
166            ber_sequence_fmt(self.0, self.1).lemma_parse_safe(ibuf);
167        }
168    }
169
170    impl<C: SpecCombinator + SafeParser + Productive> Productive for BerSequenceFmt<C> {
171        open spec fn productive_inv(&self) -> bool {
172            self.1.safe_inv()
173        }
174
175        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
176            ber_sequence_fmt(self.0, self.1).lemma_productive(ibuf);
177        }
178    }
179
180    impl<C: SpecCombinator + GoodSerializer> GoodSerializer for BerSequenceFmt<C> {
181        open spec fn serialize_inv(&self) -> bool {
182            self.1.serialize_inv()
183        }
184
185        proof fn lemma_serialize_len(&self, value: Self::SVal) {
186            ber_sequence_normalized_fmt(self.0, self.1).lemma_serialize_len(value);
187        }
188    }
189
190    impl<C: SpecCombinator + GoodSerializer + EquivSerializers> NonTailFmt for BerSequenceFmt<C> {
191        open spec fn serialize_dps_inv(&self) -> bool {
192            &&& self.1.serialize_inv()
193            &&& self.1.equiv_inv()
194        }
195
196        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
197            ber_sequence_normalized_fmt(self.0, self.1).lemma_serialize_dps_prepend(value, obuf);
198        }
199
200        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
201            ber_sequence_normalized_fmt(self.0, self.1).lemma_serialize_dps_len(value, obuf);
202        }
203    }
204
205    impl<C: SpecCombinator + EquivSerializers> EquivSerializersGeneral for BerSequenceFmt<C> {
206        open spec fn equiv_general_inv(&self) -> bool {
207            self.1.equiv_inv()
208        }
209
210        proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
211            ber_sequence_normalized_fmt(self.0, self.1).lemma_serialize_equiv(value, obuf);
212        }
213    }
214
215    impl<C: SpecCombinator + EquivSerializers> EquivSerializers for BerSequenceFmt<C> {
216        open spec fn equiv_inv(&self) -> bool {
217            self.1.equiv_inv()
218        }
219
220        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
221            self.lemma_serialize_equiv(value, Seq::empty());
222        }
223    }
224
225    impl<C> SPRoundTripDps for BerSequenceFmt<C> where
226        C: SpecCombinator + GoodSerializer + EquivSerializers + SPRoundTripDps,
227     {
228        open spec fn unambiguous(&self) -> bool {
229            ber_sequence_normalized_fmt(self.0, self.1).unambiguous()
230        }
231
232        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
233            let normalized = ber_sequence_normalized_fmt(self.0, self.1);
234            normalized.theorem_serialize_dps_parse_roundtrip(value, obuf);
235            let len = self.1.byte_len(value) as usize;
236            let exact = ExactLen(len, self.1);
237            exact.theorem_serialize_dps_parse_roundtrip(value, obuf);
238            let content_suffix = exact.spec_serialize_dps(value, obuf);
239            BerLengthFmt.theorem_serialize_dps_parse_roundtrip(
240                BerLength::Definite(len),
241                content_suffix,
242            );
243            let length_suffix = BerLengthFmt.spec_serialize_dps(
244                BerLength::Definite(len),
245                content_suffix,
246            );
247            BerLengthFmt.lemma_serialize_dps_prepend(BerLength::Definite(len), content_suffix);
248            BerLengthFmt.lemma_serialize_dps_len(BerLength::Definite(len), content_suffix);
249            let length_len = BerLengthFmt.byte_len(BerLength::Definite(len)) as int;
250            TagFmt.theorem_serialize_dps_parse_roundtrip(self.0, length_suffix);
251            TagFmt.lemma_serialize_dps_prepend(self.0, length_suffix);
252            TagFmt.lemma_serialize_dps_len(self.0, length_suffix);
253
254        }
255    }
256
257}
258
259impl<'i, C> Parser<&'i [u8]> for BerSequenceFmt<C> where
260    C: SpecCombinator + Parser<&'i [u8]> + SafeParser + Copy,
261 {
262    type PT = C::PT;
263
264    open spec fn exec_inv(&self) -> bool {
265        &&& self.1.exec_inv()
266        &&& self.1.safe_inv()
267    }
268
269    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
270        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
271        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
272
273        let _ = ibuf.len();
274        let (tag_len, _tag) = Const(TagFmt, self.0).parse(ibuf)?;
275        let after_tag = ibuf.skip(tag_len);
276        let (length_len, length) = BerLengthFmt.parse(&after_tag)?;
277        let content = after_tag.skip(length_len);
278
279        let (content_len, value) = match length {
280            BerLength::Definite(len) => ExactLen(len, self.1).parse(&content)?,
281            BerLength::Indefinite => {
282                let framed = Pair(self.1, EOC);
283                proof {
284                    crate::core::exec::bridge_lemmas::lemma_pair_parser_exec_inv::<&'i [u8], _, _>(
285                        &EOC,
286                    );
287                    crate::core::exec::bridge_lemmas::lemma_pair_parser_exec_inv::<&'i [u8], _, _>(
288                        &framed,
289                    );
290                }
291                parse_discard_eoc(&framed, &content)?
292            },
293        };
294        let total = tag_len + length_len + content_len;
295        assert(self.spec_parse(ibuf@) == Some((total as int, value.deep_view())));
296        Ok((total, value))
297    }
298}
299
300impl<Output: OutputBuf, C, T> Serializer<Output, T> for BerSequenceFmt<C> where
301    T: DeepView + ?Sized,
302    C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,
303 {
304    #[verifier::prophetic]
305    open spec fn exec_inv(&self) -> bool {
306        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
307        &&& <C as ByteLen<T>>::exec_inv(&self.1)
308    }
309
310    fn serialize_into(&self, value: &T, obuf: &mut Output) {
311        let normalized = ASN1Fmt::<_, BER>(self.0, self.1);
312        normalized.serialize_into(value, obuf);
313    }
314}
315
316impl<C, T> Prepare<T> for BerSequenceFmt<C> where
317    T: DeepView + ?Sized,
318    C: SpecCombinator + Prepare<T> + Copy,
319 {
320    open spec fn exec_inv(&self) -> bool {
321        <C as Prepare<T>>::exec_inv(&self.1)
322    }
323
324    fn prepare(&self, value: &T) -> Result<usize, PreSerializeError> {
325        let normalized = ASN1Fmt::<_, BER>(self.0, self.1);
326        normalized.prepare(value)
327    }
328}
329
330impl<C, T> ByteLen<T> for BerSequenceFmt<C> where
331    T: DeepView + ?Sized,
332    C: SpecCombinator + ByteLen<T> + Copy,
333 {
334    open spec fn exec_inv(&self) -> bool {
335        <C as ByteLen<T>>::exec_inv(&self.1)
336    }
337
338    fn length(&self, value: &T) -> usize {
339        let normalized = ASN1Fmt::<_, BER>(self.0, self.1);
340        normalized.length(value)
341    }
342}
343
344} // verus!
vest_lib/asn1/ber/sequence.rs

vest_lib/asn1/ber/
sequence.rs
