vest_lib/asn1/ber/
octet_string.rs

1//! BER OCTET STRING combinators with constructed/indefinite segment trees.
2use crate::asn1::{
3    constructed_tag, primitive_tag, ASN1Fmt, BerLength, BerLengthFmt, Class, LengthFmt,
4    OctetStringFmt, Tag, TagFmt, BER,
5};
6use crate::combinators::{
7    bytes::ExactLen,
8    mapped::spec::FnSpecMapper,
9    recursive::{
10        BundledSpecs, ParamRecSpecs, ParserRecBody, ProductiveRecBody, SafeParserRecBody,
11        SpecRecBody,
12    },
13    tail::RepeatTillEnd,
14    Bind, FixWith, Mapped, Repeat, Sum, Void,
15};
16use crate::core::exec::fns::*;
17use crate::core::exec::parser::*;
18use crate::core::exec::{
19    input::InputBuf, ByteLen, OutputBuf, PResult, ParseError, Parser, PreSerializeError, Prepare,
20    Serializer,
21};
22use crate::core::{proof::*, spec::*};
23use crate::Never;
24#[cfg(feature = "alloc")]
25use alloc::vec::Vec;
26use vstd::prelude::*;
27#[cfg(feature = "alloc")]
28use vstd::slice::slice_to_vec;
29
30use super::any::{EocFmt, EocValue, EOC};
31use Sum::Inl as L;
32use Sum::Inr as R;
33
34verus! {
35
36type BerOctetStringWireType = (
37    Tag,
38    Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, EocValue)>), Never>>,
39);
40
41type BerOctetStringBodyFmt<Rec> = Mapped<
42    Bind<
43        TagFmt,
44        spec_fn(Tag) -> Sum<
45            Bind<LengthFmt<BER>, spec_fn(usize) -> ExactLen<OctetStringFmt, usize>>,
46            Sum<
47                Bind<
48                    BerLengthFmt,
49                    spec_fn(BerLength) -> Sum<
50                        ExactLen<RepeatTillEnd<Rec>, usize>,
51                        Repeat<Rec, EocFmt>,
52                    >,
53                >,
54                Void,
55            >,
56        >,
57    >,
58    FnSpecMapper<BerOctetStringWireType, Seq<u8>>,
59>;
60
61/// One full TLV unfolding of a BER OCTET STRING.
62///
63/// X.690 §8.23.3 specifies a restricted character string as
64/// `[UNIVERSAL x] IMPLICIT OCTET STRING`. Thus `tag` applies only to the outermost TLV; constructed
65/// fragments recursively use universal OCTET STRING tag 4, as required by X.690 §8.7.3.2.
66pub open spec fn ber_octet_string_rec_body(
67    tag: Tag,
68    rec: ParamRecSpecs<Tag, Seq<u8>>,
69) -> BerOctetStringBodyFmt<BundledSpecs<Seq<u8>>> {
70    #[verusfmt::skip]
71    Mapped {
72        inner: Bind(TagFmt, |parsed_tag: Tag|
73            match parsed_tag {
74                t if t == primitive_tag(tag) =>
75                    L(Bind(LengthFmt::<BER>, |len: usize| ExactLen(len, OctetStringFmt))),
76                t if t == constructed_tag(tag) =>
77                    R(L(Bind(BerLengthFmt, |len: BerLength|
78                        match len {
79                            BerLength::Definite(len) =>
80                                L(ExactLen(len, RepeatTillEnd(rec(TagFmt::OCTET_STRING)))),
81                            BerLength::Indefinite =>
82                                R(Repeat(rec(TagFmt::OCTET_STRING), EOC)),
83                        }))),
84                _ => R(R(Void("Tag must match the configured BER OCTET STRING identity"))),
85            },
86        ),
87        mapper: (
88            |parsed: BerOctetStringWireType|
89                match parsed.1 {
90                    L((_len, bytes)) => bytes,
91                    R(L((_len, inner))) => match inner {
92                        L(segments) => segments.flatten(),
93                        R((segments, _eoc)) => segments.flatten(),
94                    },
95                    R(R(_)) => arbitrary(), // unreachable
96                },
97            |bytes: Seq<u8>| (primitive_tag(tag), L((bytes.len() as usize, bytes))),
98        ),
99    }
100}
101
102pub struct BerOctetStringRecBody;
103
104impl SpecRecBody for BerOctetStringRecBody {
105    type Param = Tag;
106
107    type T = Seq<u8>;
108
109    type Body = BerOctetStringBodyFmt<BundledSpecs<Seq<u8>>>;
110
111    open spec fn spec_body(
112        &self,
113        tag: Self::Param,
114        rec: ParamRecSpecs<Self::Param, Self::T>,
115    ) -> Self::Body {
116        ber_octet_string_rec_body(tag, rec)
117    }
118}
119
120mod recursive_proofs {
121    use super::*;
122
123    impl SafeParserRecBody for BerOctetStringRecBody {
124        proof fn lemma_body_safe_inv_preservation(
125            &self,
126            tag: Tag,
127            rec: ParamRecSpecs<Tag, Seq<u8>>,
128        ) {
129        }
130    }
131
132    impl ProductiveRecBody for BerOctetStringRecBody {
133        proof fn lemma_body_productive_inv_preservation(
134            &self,
135            tag: Tag,
136            rec: ParamRecSpecs<Tag, Seq<u8>>,
137        ) {
138        }
139    }
140
141}
142
143/// The primitive, definite-length encoding selected by the reverse mapper.
144pub open spec fn ber_octet_string_normalized_fmt(tag: Tag) -> ASN1Fmt<OctetStringFmt, BER> {
145    ASN1Fmt(primitive_tag(tag), OctetStringFmt)
146}
147
148/// BER OCTET STRING with bounded recursive nesting and a configurable outer tag identity.
149///
150/// Use [`Self::universal`] for an ordinary OCTET STRING or [`Self::implicit`] for an
151/// IMPLICIT-tagged value. The stored tag's constructed bit is normalized away: parsing accepts
152/// either primitive or constructed form and serialization always emits primitive definite form.
153#[derive(Clone, Copy)]
154pub struct BerOctetStringFmt<const LIMIT: usize>(pub Tag);
155
156impl<const LIMIT: usize> BerOctetStringFmt<LIMIT> {
157    /// Ordinary universal OCTET STRING.
158    #[verifier::allow_in_spec]
159    pub const fn universal() -> Self
160        returns
161            Self(TagFmt::OCTET_STRING),
162    {
163        Self(TagFmt::OCTET_STRING)
164    }
165
166    /// An IMPLICIT-tagged OCTET STRING. Only the outermost tag identity is replaced.
167    #[verifier::allow_in_spec]
168    pub const fn implicit(class: Class, number: u64) -> Self
169        returns
170            Self(
171                Tag {
172                    class,
173                    constructed: false,
174                    number: crate::asn1::tag::tag_num_from_uint(number),
175                },
176            ),
177    {
178        Self(Tag { class, constructed: false, number: crate::asn1::tag::tag_num_from_uint(number) })
179    }
180}
181
182mod derived_specs {
183    use super::*;
184
185    impl<const LIMIT: usize> SpecParser for BerOctetStringFmt<LIMIT> {
186        type PVal = Seq<u8>;
187
188        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
189            FixWith::<LIMIT, _, _>(BerOctetStringRecBody, self.0).spec_parse(ibuf)
190        }
191    }
192
193    impl<const LIMIT: usize> Consistency for BerOctetStringFmt<LIMIT> {
194        type Val = Seq<u8>;
195
196        open spec fn consistent(&self, value: Self::Val) -> bool {
197            ber_octet_string_normalized_fmt(self.0).consistent(value)
198        }
199    }
200
201    impl<const LIMIT: usize> SpecSerializerDps for BerOctetStringFmt<LIMIT> {
202        type SValue = Seq<u8>;
203
204        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
205            ber_octet_string_normalized_fmt(self.0).spec_serialize_dps(value, obuf)
206        }
207    }
208
209    impl<const LIMIT: usize> SpecSerializer for BerOctetStringFmt<LIMIT> {
210        type SVal = Seq<u8>;
211
212        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
213            ber_octet_string_normalized_fmt(self.0).spec_serialize(value)
214        }
215    }
216
217    impl<const LIMIT: usize> SpecByteLen for BerOctetStringFmt<LIMIT> {
218        type T = Seq<u8>;
219
220        open spec fn byte_len(&self, value: Self::T) -> nat {
221            ber_octet_string_normalized_fmt(self.0).byte_len(value)
222        }
223    }
224
225}
226
227mod derived_proofs {
228    use super::*;
229
230    impl<const LIMIT: usize> SafeParser for BerOctetStringFmt<LIMIT> {
231        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
232            FixWith::<LIMIT, _, _>(BerOctetStringRecBody, self.0).lemma_parse_safe(ibuf);
233        }
234    }
235
236    impl<const LIMIT: usize> Productive for BerOctetStringFmt<LIMIT> {
237        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
238            FixWith::<LIMIT, _, _>(BerOctetStringRecBody, self.0).lemma_productive(ibuf);
239        }
240    }
241
242    impl<const LIMIT: usize> GoodSerializer for BerOctetStringFmt<LIMIT> {
243        proof fn lemma_serialize_len(&self, value: Seq<u8>) {
244            ber_octet_string_normalized_fmt(self.0).lemma_serialize_len(value);
245        }
246    }
247
248    impl<const LIMIT: usize> NonTailFmt for BerOctetStringFmt<LIMIT> {
249        proof fn lemma_serialize_dps_prepend(&self, value: Seq<u8>, obuf: Seq<u8>) {
250            let normalized = ber_octet_string_normalized_fmt(self.0);
251            normalized.lemma_serialize_dps_prepend(value, obuf);
252        }
253
254        proof fn lemma_serialize_dps_len(&self, value: Seq<u8>, obuf: Seq<u8>) {
255            let normalized = ber_octet_string_normalized_fmt(self.0);
256            normalized.lemma_serialize_dps_len(value, obuf);
257        }
258    }
259
260    impl<const LIMIT: usize> EquivSerializersGeneral for BerOctetStringFmt<LIMIT> {
261        proof fn lemma_serialize_equiv(&self, value: Seq<u8>, obuf: Seq<u8>) {
262            let normalized = ber_octet_string_normalized_fmt(self.0);
263            normalized.lemma_serialize_equiv(value, obuf);
264        }
265    }
266
267    impl<const LIMIT: usize> EquivSerializers for BerOctetStringFmt<LIMIT> {
268        proof fn lemma_serialize_equiv_on_empty(&self, value: Seq<u8>) {
269            self.lemma_serialize_equiv(value, Seq::empty());
270        }
271    }
272
273    impl<const LIMIT: usize> SPRoundTripDps for BerOctetStringFmt<LIMIT> {
274        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Seq<u8>, obuf: Seq<u8>) {
275            let normalized = ber_octet_string_normalized_fmt(self.0);
276            normalized.theorem_serialize_dps_parse_roundtrip(value, obuf);
277        }
278    }
279
280}
281
282impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, [u8]> for BerOctetStringFmt<LIMIT> {
283    fn serialize_into(&self, value: &[u8], obuf: &mut Output) {
284        let tag = Tag { class: self.0.class, constructed: false, number: self.0.number };
285        let normalized = ASN1Fmt::<OctetStringFmt, BER>(tag, OctetStringFmt);
286        normalized.serialize_into(value, obuf);
287    }
288}
289
290impl<const LIMIT: usize> Prepare<[u8]> for BerOctetStringFmt<LIMIT> {
291    fn prepare(&self, value: &[u8]) -> Result<usize, PreSerializeError> {
292        let tag = Tag { class: self.0.class, constructed: false, number: self.0.number };
293        let normalized = ASN1Fmt::<OctetStringFmt, BER>(tag, OctetStringFmt);
294        normalized.prepare(value)
295    }
296}
297
298impl<const LIMIT: usize> ByteLen<[u8]> for BerOctetStringFmt<LIMIT> {
299    fn length(&self, value: &[u8]) -> usize {
300        let tag = Tag { class: self.0.class, constructed: false, number: self.0.number };
301        let normalized = ASN1Fmt::<OctetStringFmt, BER>(tag, OctetStringFmt);
302        normalized.length(value)
303    }
304}
305
306#[cfg(feature = "alloc")]
307impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, Vec<u8>> for BerOctetStringFmt<
308    LIMIT,
309> {
310    fn serialize_into(&self, value: &Vec<u8>, obuf: &mut Output) {
311        self.serialize_into(value.as_slice(), obuf)
312    }
313}
314
315#[cfg(feature = "alloc")]
316impl<const LIMIT: usize> Prepare<Vec<u8>> for BerOctetStringFmt<LIMIT> {
317    fn prepare(&self, value: &Vec<u8>) -> Result<usize, PreSerializeError> {
318        self.prepare(value.as_slice())
319    }
320}
321
322#[cfg(feature = "alloc")]
323impl<const LIMIT: usize> ByteLen<Vec<u8>> for BerOctetStringFmt<LIMIT> {
324    fn length(&self, value: &Vec<u8>) -> usize {
325        self.length(value.as_slice())
326    }
327}
328
329#[cfg(feature = "alloc")]
330fn flatten_octet_segments(segments: Vec<Vec<u8>>) -> (flat: Vec<u8>)
331    ensures
332        flat@ == segments.deep_view().flatten(),
333{
334    broadcast use vstd::seq_lib::group_seq_properties;
335
336    let mut flat = Vec::new();
337    let ghost segment_views = segments.deep_view();
338    for i in 0..segments.len()
339        invariant
340            segments.deep_view() == segment_views,
341            flat@ == segment_views.take(i as int).flatten(),
342    {
343        let segment = &segments[i];
344        proof {
345            let prefix = segment_views.take(i as int);
346            prefix.lemma_flatten_push(segment@);
347            assert(segment_views[i as int] == segment@);
348            assert(segment_views.take(i as int + 1) == prefix.push(segment@));
349        }
350        flat.extend_from_slice(&segment);
351    }
352    flat
353}
354
355spec fn flattened_result(r: Option<(int, Seq<Seq<u8>>)>) -> Option<(int, Seq<u8>)> {
356    match r {
357        Some((n, segments)) => Some((n, segments.flatten())),
358        None => None,
359    }
360}
361
362spec fn flattened_result_eoc(r: Option<(int, (Seq<Seq<u8>>, EocValue))>) -> Option<(int, Seq<u8>)> {
363    match r {
364        Some((n, (segments, _eoc))) => Some((n, segments.flatten())),
365        None => None,
366    }
367}
368
369#[inline(always)]
370#[cfg(feature = "alloc")]
371fn parse_segments_flatten<I, P>(parser: &P, ibuf: &I) -> (r: PResult<Vec<u8>>) where
372    I: InputBuf,
373    P: Parser<I, PT = Vec<Vec<u8>>, PVal = Seq<Seq<u8>>>,
374
375    requires
376        parser.exec_inv(),
377    ensures
378        parse_matches_spec(r, flattened_result(parser.spec_parse(ibuf@))),
379{
380    let (n, segments) = parser.parse(ibuf)?;
381    let flat = flatten_octet_segments(segments);
382    assert(flat.deep_view() == flat@);
383    Ok((n, flat))
384}
385
386#[inline(always)]
387#[cfg(feature = "alloc")]
388fn parse_segments_eoc_flatten<I, P>(parser: &P, ibuf: &I) -> (r: PResult<Vec<u8>>) where
389    I: InputBuf,
390    P: Parser<I, PT = (Vec<Vec<u8>>, EocValue), PVal = (Seq<Seq<u8>>, EocValue)>,
391
392    requires
393        parser.exec_inv(),
394    ensures
395        parse_matches_spec(r, flattened_result_eoc(parser.spec_parse(ibuf@))),
396{
397    let (n, (segments, _eoc)) = parser.parse(ibuf)?;
398    let flat = flatten_octet_segments(segments);
399    assert(flat.deep_view() == flat@);
400    Ok((n, flat))
401}
402
403#[cfg(feature = "alloc")]
404impl<'i> ParserRecBody<&'i [u8]> for BerOctetStringRecBody {
405    type EP = Tag;
406
407    type O = Vec<u8>;
408
409    fn parse_body<Exec>(
410        &self,
411        expected: &Tag,
412        Ghost(spec_rec): Ghost<ParamRecSpecs<Tag, Seq<u8>>>,
413        exec_rec: Exec,
414        ibuf: &&'i [u8],
415    ) -> PResult<Vec<u8>> where Exec: Fn(&Tag, &&'i [u8]) -> PResult<Vec<u8>> {
416        use crate::core::exec::bridge_lemmas::*;
417        use crate::combinators::congruence::*;
418
419        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
420        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
421        broadcast use lemma_parser_congruent_reflexive;
422
423        let _ = ibuf.len();
424        let (tag_len, actual_tag) = TagFmt.parse(ibuf)?;
425        let rest = ibuf.skip(tag_len);
426
427        if actual_tag == primitive_tag(*expected) {
428            let (length_len, content_len) = LengthFmt::<BER>.parse(&rest)?;
429            let content_bytes = rest.skip(length_len);
430            let (content_len, v) = ExactLen(content_len, OctetStringFmt).parse(&content_bytes)?;
431            let v = slice_to_vec(v);
432            assert(v.deep_view() == v@);
433            let total = tag_len + length_len + content_len;
434            Ok((total, v))
435        } else if actual_tag == constructed_tag(*expected) {
436            let (length_len, content_len) = BerLengthFmt.parse(&rest)?;
437            let content_bytes = rest.skip(length_len);
438            let ghost child_spec = spec_rec(TagFmt::OCTET_STRING);
439            let child_exec = |input: &&'i [u8]| -> (r: PResult<Vec<u8>>)
440                ensures
441                    parse_matches_spec(r, child_spec.2(input@)),
442                { exec_rec(&TagFmt::OCTET_STRING, input) };
443            // The explicit spec type is required by ordinary rustc: the value of a
444            // `Ghost<_>` is erased, so it cannot by itself drive type inference outside Verus.
445            let child: &FnParser<&'i [u8], Vec<u8>, BundledSpecs<Seq<u8>>, _> = &FnParser::new(
446                child_exec,
447                Ghost(child_spec),
448            );
449            proof {
450                lemma_ref_parser_exec_inv::<&'i [u8], _>(child);
451                lemma_ref_safe_productive_inv(child);
452                lemma_ref_fn_parser_congruence(child);
453            }
454
455            let (content_len, v) = match content_len {
456                BerLength::Definite(content_len) => {
457                    let ghost repeated_spec = RepeatTillEnd(child_spec);
458                    let repeated = RepeatTillEnd(child);
459                    let exact = ExactLen(content_len, repeated);
460                    proof {
461                        lemma_repeat_till_end_parser_exec_inv::<&'i [u8], _>(&repeated);
462                        lemma_exact_len_parser_exec_inv::<&'i [u8], _, _>(&exact);
463                        lemma_repeat_till_end_parser_congruence(child, child_spec);
464                        lemma_exact_len_parser_congruence(content_len, repeated, repeated_spec);
465                        reveal(parser_congruent);
466                    }
467                    parse_segments_flatten(&exact, &content_bytes)?
468                },
469                BerLength::Indefinite => {
470                    let repeated = Repeat(child, EOC);
471                    proof {
472                        lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&EOC);
473                        lemma_repeat_parser_exec_inv::<&'i [u8], _, _>(&repeated);
474                        lemma_repeat_parser_congruence(child, child_spec, EOC, EOC);
475                        reveal(parser_congruent);
476                    }
477                    parse_segments_eoc_flatten(&repeated, &content_bytes)?
478                },
479            };
480            let total = tag_len + length_len + content_len;
481            Ok((total, v))
482        } else {
483            Err(ParseError::custom("Tag must match the configured BER OCTET STRING identity"))
484        }
485    }
486}
487
488#[cfg(feature = "alloc")]
489impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerOctetStringFmt<LIMIT> {
490    type PT = Vec<u8>;
491
492    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
493        FixWith::<LIMIT, _, _>(BerOctetStringRecBody, self.0).parse(ibuf)
494    }
495}
496
497} // verus!
vest_lib/asn1/ber/octet_string.rs

vest_lib/asn1/ber/
octet_string.rs
