vest_lib/asn1/ber/
bit_string.rs

1//! BER BIT STRING combinators with constructed/indefinite segment trees.
2use crate::asn1::{
3    constructed_tag, primitive_tag, ASN1Fmt, BerLength, BerLengthFmt, BitStringFmt, BitStringSpec,
4    Class, LengthFmt, Tag, TagFmt, BER,
5};
6#[cfg(feature = "alloc")]
7use crate::asn1::{BitString, BitStringOwned};
8use crate::combinators::{
9    bytes::ExactLen,
10    mapped::spec::FnSpecMapper,
11    recursive::{
12        BundledSpecs, ParamRecSpecs, ParserRecBody, ProductiveRecBody, SafeParserRecBody,
13        SpecRecBody,
14    },
15    tail::RepeatTillEnd,
16    Bind, FixWith, Mapped, Refined, Repeat, Sum, Void,
17};
18use crate::core::exec::fns::*;
19use crate::core::exec::parser::*;
20use crate::core::exec::{
21    input::InputBuf, ByteLen, OutputBuf, PResult, ParseError, Parser, PreSerializeError, Prepare,
22    Serializer,
23};
24use crate::core::{proof::*, spec::*};
25use crate::Never;
26#[cfg(feature = "alloc")]
27use alloc::vec::Vec;
28use vstd::prelude::*;
29#[cfg(feature = "alloc")]
30use vstd::slice::slice_to_vec;
31
32use super::any::{EocFmt, EocValue, EOC};
33use Sum::Inl as L;
34use Sum::Inr as R;
35
36verus! {
37
38type BerBitStringWireType = (
39    Tag,
40    Sum<
41        (usize, BitStringSpec),
42        Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, EocValue)>), Never>,
43    >,
44);
45
46type BerBitStringRawBodyFmt<Rec> = Bind<
47    TagFmt,
48    spec_fn(Tag) -> Sum<
49        Bind<LengthFmt<BER>, spec_fn(usize) -> ExactLen<BitStringFmt<BER>, usize>>,
50        Sum<
51            Bind<
52                BerLengthFmt,
53                spec_fn(BerLength) -> Sum<ExactLen<RepeatTillEnd<Rec>, usize>, Repeat<Rec, EocFmt>>,
54            >,
55            Void,
56        >,
57    >,
58>;
59
60type BerBitStringBodyFmt<Rec> = Mapped<
61    Refined<BerBitStringRawBodyFmt<Rec>, PredFnSpec<BerBitStringWireType>>,
62    FnSpecMapper<BerBitStringWireType, BitStringSpec>,
63>;
64
65/// Constructed BIT STRING segments are concatenable only when every segment except the last has
66/// zero unused bits (X.690 §8.6.4.2).
67pub open spec fn ber_bit_string_segments_wf(segments: Seq<BitStringSpec>) -> bool {
68    forall|i: int| 0 <= i < segments.len() - 1 ==> #[trigger] segments[i].unused == 0
69}
70
71pub open spec fn flatten_ber_bit_string_segments(segments: Seq<BitStringSpec>) -> BitStringSpec {
72    let bits = segments.map(|_i: int, segment: BitStringSpec| segment.bits).flatten();
73    BitStringSpec {
74        unused: if bits.len() == 0 || segments.len() == 0 {
75            0
76        } else {
77            segments.last().unused
78        },
79        bits,
80    }
81}
82
83pub open spec fn ber_bit_string_wire_wf(parsed: BerBitStringWireType) -> bool {
84    match parsed.1 {
85        L(_) => true,
86        R(L((_length, inner))) => match inner {
87            L(segments) => ber_bit_string_segments_wf(segments),
88            R((segments, _eoc)) => ber_bit_string_segments_wf(segments),
89        },
90        R(R(_)) => true,
91    }
92}
93
94/// One recursive unfolding of a BER BIT STRING.
95///
96/// IMPLICIT tagging replaces only the outer tag. Nested fragments retain universal BIT STRING
97/// tag 3, as required by X.690 §8.6.4.1.
98pub open spec fn ber_bit_string_rec_body(
99    tag: Tag,
100    rec: ParamRecSpecs<Tag, BitStringSpec>,
101) -> BerBitStringBodyFmt<BundledSpecs<BitStringSpec>> {
102    #[verusfmt::skip]
103    Mapped {
104        inner: Refined(
105            Bind(TagFmt, |parsed_tag: Tag|
106                match parsed_tag {
107                    t if t == primitive_tag(tag) =>
108                        L(Bind(LengthFmt::<BER>, |len: usize|
109                            ExactLen(len, BitStringFmt::<BER>))),
110                    t if t == constructed_tag(tag) =>
111                        R(L(Bind(BerLengthFmt, |len: BerLength|
112                            match len {
113                                BerLength::Definite(len) =>
114                                    L(ExactLen(len, RepeatTillEnd(rec(TagFmt::BIT_STRING)))),
115                                BerLength::Indefinite =>
116                                    R(Repeat(rec(TagFmt::BIT_STRING), EOC)),
117                            }))),
118                    _ => R(R(Void("Tag must match the configured BER BIT STRING identity"))),
119                },
120            ),
121            |parsed: BerBitStringWireType| ber_bit_string_wire_wf(parsed),
122        ),
123        mapper: (
124            |parsed: BerBitStringWireType|
125                match parsed.1 {
126                    L((_len, value)) => value,
127                    R(L((_len, inner))) => match inner {
128                        L(segments) => flatten_ber_bit_string_segments(segments),
129                        R((segments, _eoc)) => flatten_ber_bit_string_segments(segments),
130                    },
131                    R(R(_)) => arbitrary(), // unreachable
132                },
133            |value: BitStringSpec| (
134                primitive_tag(tag),
135                L((BitStringFmt::<BER>.byte_len(value) as usize, value)),
136            ),
137        ),
138    }
139}
140
141pub struct BerBitStringRecBody;
142
143impl SpecRecBody for BerBitStringRecBody {
144    type Param = Tag;
145
146    type T = BitStringSpec;
147
148    type Body = BerBitStringBodyFmt<BundledSpecs<BitStringSpec>>;
149
150    open spec fn spec_body(
151        &self,
152        tag: Self::Param,
153        rec: ParamRecSpecs<Self::Param, Self::T>,
154    ) -> Self::Body {
155        ber_bit_string_rec_body(tag, rec)
156    }
157}
158
159mod recursive_proofs {
160    use super::*;
161
162    impl SafeParserRecBody for BerBitStringRecBody {
163        proof fn lemma_body_safe_inv_preservation(
164            &self,
165            _tag: Tag,
166            _rec: ParamRecSpecs<Tag, BitStringSpec>,
167        ) {
168        }
169    }
170
171    impl ProductiveRecBody for BerBitStringRecBody {
172        proof fn lemma_body_productive_inv_preservation(
173            &self,
174            _tag: Tag,
175            _rec: ParamRecSpecs<Tag, BitStringSpec>,
176        ) {
177        }
178    }
179
180}
181
182/// The primitive, definite-length BER encoding selected by the BIT STRING serializer.
183pub open spec fn ber_bit_string_normalized_fmt(tag: Tag) -> ASN1Fmt<BitStringFmt<BER>, BER> {
184    ASN1Fmt(primitive_tag(tag), BitStringFmt::<BER>)
185}
186
187/// BER BIT STRING with bounded constructed nesting and a configurable outer tag identity.
188///
189/// Parsing accepts primitive and constructed definite/indefinite forms. Serialization always
190/// emits a primitive definite-length BER encoding.
191#[derive(Clone, Copy)]
192pub struct BerBitStringFmt<const LIMIT: usize>(pub Tag);
193
194impl<const LIMIT: usize> BerBitStringFmt<LIMIT> {
195    #[verifier::allow_in_spec]
196    pub const fn universal() -> Self
197        returns
198            Self(TagFmt::BIT_STRING),
199    {
200        Self(TagFmt::BIT_STRING)
201    }
202
203    #[verifier::allow_in_spec]
204    pub const fn implicit(class: Class, number: u64) -> Self
205        returns
206            Self(
207                Tag {
208                    class,
209                    constructed: false,
210                    number: crate::asn1::tag::tag_num_from_uint(number),
211                },
212            ),
213    {
214        Self(Tag { class, constructed: false, number: crate::asn1::tag::tag_num_from_uint(number) })
215    }
216}
217
218mod derived_specs {
219    use super::*;
220
221    impl<const LIMIT: usize> SpecParser for BerBitStringFmt<LIMIT> {
222        type PVal = BitStringSpec;
223
224        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
225            FixWith::<LIMIT, _, _>(BerBitStringRecBody, self.0).spec_parse(ibuf)
226        }
227    }
228
229    impl<const LIMIT: usize> Consistency for BerBitStringFmt<LIMIT> {
230        type Val = BitStringSpec;
231
232        open spec fn consistent(&self, value: Self::Val) -> bool {
233            ber_bit_string_normalized_fmt(self.0).consistent(value)
234        }
235    }
236
237    impl<const LIMIT: usize> SpecSerializerDps for BerBitStringFmt<LIMIT> {
238        type SValue = BitStringSpec;
239
240        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
241            ber_bit_string_normalized_fmt(self.0).spec_serialize_dps(value, obuf)
242        }
243    }
244
245    impl<const LIMIT: usize> SpecSerializer for BerBitStringFmt<LIMIT> {
246        type SVal = BitStringSpec;
247
248        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
249            ber_bit_string_normalized_fmt(self.0).spec_serialize(value)
250        }
251    }
252
253    impl<const LIMIT: usize> SpecByteLen for BerBitStringFmt<LIMIT> {
254        type T = BitStringSpec;
255
256        open spec fn byte_len(&self, value: Self::T) -> nat {
257            ber_bit_string_normalized_fmt(self.0).byte_len(value)
258        }
259    }
260
261}
262
263mod derived_proofs {
264    use super::*;
265
266    impl<const LIMIT: usize> SafeParser for BerBitStringFmt<LIMIT> {
267        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
268            FixWith::<LIMIT, _, _>(BerBitStringRecBody, self.0).lemma_parse_safe(ibuf);
269        }
270    }
271
272    impl<const LIMIT: usize> Productive for BerBitStringFmt<LIMIT> {
273        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
274            FixWith::<LIMIT, _, _>(BerBitStringRecBody, self.0).lemma_productive(ibuf);
275        }
276    }
277
278    impl<const LIMIT: usize> GoodSerializer for BerBitStringFmt<LIMIT> {
279        proof fn lemma_serialize_len(&self, value: BitStringSpec) {
280            ber_bit_string_normalized_fmt(self.0).lemma_serialize_len(value);
281        }
282    }
283
284    impl<const LIMIT: usize> NonTailFmt for BerBitStringFmt<LIMIT> {
285        proof fn lemma_serialize_dps_prepend(&self, value: BitStringSpec, obuf: Seq<u8>) {
286            ber_bit_string_normalized_fmt(self.0).lemma_serialize_dps_prepend(value, obuf);
287        }
288
289        proof fn lemma_serialize_dps_len(&self, value: BitStringSpec, obuf: Seq<u8>) {
290            ber_bit_string_normalized_fmt(self.0).lemma_serialize_dps_len(value, obuf);
291        }
292    }
293
294    impl<const LIMIT: usize> EquivSerializersGeneral for BerBitStringFmt<LIMIT> {
295        proof fn lemma_serialize_equiv(&self, value: BitStringSpec, obuf: Seq<u8>) {
296            ber_bit_string_normalized_fmt(self.0).lemma_serialize_equiv(value, obuf);
297        }
298    }
299
300    impl<const LIMIT: usize> EquivSerializers for BerBitStringFmt<LIMIT> {
301        proof fn lemma_serialize_equiv_on_empty(&self, value: BitStringSpec) {
302            self.lemma_serialize_equiv(value, Seq::empty());
303        }
304    }
305
306    impl<const LIMIT: usize> SPRoundTripDps for BerBitStringFmt<LIMIT> {
307        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: BitStringSpec, obuf: Seq<u8>) {
308            ber_bit_string_normalized_fmt(self.0).theorem_serialize_dps_parse_roundtrip(
309                value,
310                obuf,
311            );
312        }
313    }
314
315}
316
317impl<Output, T, const LIMIT: usize> Serializer<Output, T> for BerBitStringFmt<LIMIT> where
318    Output: OutputBuf,
319    T: DeepView<V = BitStringSpec> + ?Sized,
320    ASN1Fmt<BitStringFmt<BER>, BER>: Serializer<Output, T>,
321 {
322    #[verifier::prophetic]
323    open spec fn exec_inv(&self) -> bool {
324        <ASN1Fmt<BitStringFmt<BER>, BER> as Serializer<Output, T>>::exec_inv(
325            &ber_bit_string_normalized_fmt(self.0),
326        )
327    }
328
329    fn serialize_into(&self, value: &T, obuf: &mut Output) {
330        let normalized = ASN1Fmt::<BitStringFmt<BER>, BER>(
331            primitive_tag(self.0),
332            BitStringFmt::<BER>,
333        );
334        normalized.serialize_into(value, obuf);
335    }
336}
337
338impl<T, const LIMIT: usize> Prepare<T> for BerBitStringFmt<LIMIT> where
339    T: DeepView<V = BitStringSpec> + ?Sized,
340    ASN1Fmt<BitStringFmt<BER>, BER>: Prepare<T>,
341 {
342    open spec fn exec_inv(&self) -> bool {
343        <ASN1Fmt<BitStringFmt<BER>, BER> as Prepare<T>>::exec_inv(
344            &ber_bit_string_normalized_fmt(self.0),
345        )
346    }
347
348    fn prepare(&self, value: &T) -> Result<usize, PreSerializeError> {
349        let normalized = ASN1Fmt::<BitStringFmt<BER>, BER>(
350            primitive_tag(self.0),
351            BitStringFmt::<BER>,
352        );
353        normalized.prepare(value)
354    }
355}
356
357impl<T, const LIMIT: usize> ByteLen<T> for BerBitStringFmt<LIMIT> where
358    T: DeepView<V = BitStringSpec> + ?Sized,
359    ASN1Fmt<BitStringFmt<BER>, BER>: ByteLen<T>,
360 {
361    open spec fn exec_inv(&self) -> bool {
362        <ASN1Fmt<BitStringFmt<BER>, BER> as ByteLen<T>>::exec_inv(
363            &ber_bit_string_normalized_fmt(self.0),
364        )
365    }
366
367    fn length(&self, value: &T) -> usize {
368        let normalized = ASN1Fmt::<BitStringFmt<BER>, BER>(
369            primitive_tag(self.0),
370            BitStringFmt::<BER>,
371        );
372        normalized.length(value)
373    }
374}
375
376#[cfg(feature = "alloc")]
377fn bit_string_to_owned(value: BitString<'_, BER>) -> (owned: BitStringOwned)
378    ensures
379        owned.deep_view() == value.deep_view(),
380{
381    let unused = value.unused();
382    let bits = slice_to_vec(value.bits());
383    BitStringOwned::new(unused, bits)
384}
385
386#[cfg(feature = "alloc")]
387fn ber_bit_string_segments_wf_exec(segments: &Vec<BitStringOwned>) -> (valid: bool)
388    ensures
389        valid == ber_bit_string_segments_wf(segments.deep_view()),
390{
391    let ghost views = segments.deep_view();
392    let mut i = 0usize;
393    while i < segments.len()
394        invariant
395            segments.deep_view() == views,
396            i <= segments.len(),
397            forall|j: int| 0 <= j < i && j < views.len() - 1 ==> #[trigger] views[j].unused == 0,
398        decreases segments.len() - i,
399    {
400        if i + 1 < segments.len() {
401            let unused = segments[i].unused();
402            if unused != 0 {
403                assert(0 <= i as int);
404                assert((i as int) < views.len() - 1);
405                assert(views[i as int].unused != 0);
406                return false;
407            }
408        }
409        i += 1;
410    }
411    true
412}
413
414#[cfg(feature = "alloc")]
415fn flatten_bit_string_segments(segments: Vec<BitStringOwned>) -> (flat: BitStringOwned)
416    requires
417        ber_bit_string_segments_wf(segments.deep_view()),
418    ensures
419        flat.deep_view() == flatten_ber_bit_string_segments(segments.deep_view()),
420{
421    broadcast use vstd::seq_lib::group_seq_properties;
422
423    let ghost segment_views = segments.deep_view();
424    let ghost bit_views = segment_views.map(|_i: int, segment: BitStringSpec| segment.bits);
425    let mut bits = Vec::new();
426    for i in 0..segments.len()
427        invariant
428            segments.deep_view() == segment_views,
429            bit_views == segment_views.map(|_i: int, segment: BitStringSpec| segment.bits),
430            bits@ == bit_views.take(i as int).flatten(),
431    {
432        let segment_bits = segments[i].bits();
433        proof {
434            let prefix = bit_views.take(i as int);
435            prefix.lemma_flatten_push(segment_bits@);
436            assert(bit_views[i as int] == segment_bits@);
437            assert(bit_views.take(i as int + 1) == prefix.push(segment_bits@));
438        }
439        bits.extend_from_slice(segment_bits);
440    }
441
442    let unused = if bits.len() == 0 || segments.len() == 0 {
443        0
444    } else {
445        let last = &segments[segments.len() - 1];
446        last.unused()
447    };
448    BitStringOwned::new(unused, bits)
449}
450
451spec fn flattened_bit_string_result(result: Option<(int, Seq<BitStringSpec>)>) -> Option<
452    (int, BitStringSpec),
453> {
454    match result {
455        Some((n, segments)) if ber_bit_string_segments_wf(segments) => {
456            Some((n, flatten_ber_bit_string_segments(segments)))
457        },
458        _ => None,
459    }
460}
461
462spec fn flattened_bit_string_eoc_result(
463    result: Option<(int, (Seq<BitStringSpec>, EocValue))>,
464) -> Option<(int, BitStringSpec)> {
465    match result {
466        Some((n, (segments, _eoc))) if ber_bit_string_segments_wf(segments) => {
467            Some((n, flatten_ber_bit_string_segments(segments)))
468        },
469        _ => None,
470    }
471}
472
473#[inline(always)]
474#[cfg(feature = "alloc")]
475fn parse_bit_string_segments<I, P>(parser: &P, ibuf: &I) -> (result: PResult<BitStringOwned>) where
476    I: InputBuf,
477    P: Parser<I, PT = Vec<BitStringOwned>, PVal = Seq<BitStringSpec>>,
478
479    requires
480        parser.exec_inv(),
481    ensures
482        parse_matches_spec(result, flattened_bit_string_result(parser.spec_parse(ibuf@))),
483{
484    let (n, segments) = parser.parse(ibuf)?;
485    if !ber_bit_string_segments_wf_exec(&segments) {
486        return Err(
487            ParseError::custom(
488                "Only the final constructed BIT STRING segment may have unused bits",
489            ),
490        );
491    }
492    let flat = flatten_bit_string_segments(segments);
493    Ok((n, flat))
494}
495
496#[inline(always)]
497#[cfg(feature = "alloc")]
498fn parse_bit_string_segments_eoc<I, P>(parser: &P, ibuf: &I) -> (result: PResult<
499    BitStringOwned,
500>) where
501    I: InputBuf,
502    P: Parser<I, PT = (Vec<BitStringOwned>, EocValue), PVal = (Seq<BitStringSpec>, EocValue)>,
503
504    requires
505        parser.exec_inv(),
506    ensures
507        parse_matches_spec(result, flattened_bit_string_eoc_result(parser.spec_parse(ibuf@))),
508{
509    let (n, (segments, _eoc)) = parser.parse(ibuf)?;
510    if !ber_bit_string_segments_wf_exec(&segments) {
511        return Err(
512            ParseError::custom(
513                "Only the final constructed BIT STRING segment may have unused bits",
514            ),
515        );
516    }
517    let flat = flatten_bit_string_segments(segments);
518    Ok((n, flat))
519}
520
521#[cfg(feature = "alloc")]
522impl<'i> ParserRecBody<&'i [u8]> for BerBitStringRecBody {
523    type EP = Tag;
524
525    type O = BitStringOwned;
526
527    fn parse_body<Exec>(
528        &self,
529        expected: &Tag,
530        Ghost(spec_rec): Ghost<ParamRecSpecs<Tag, BitStringSpec>>,
531        exec_rec: Exec,
532        ibuf: &&'i [u8],
533    ) -> PResult<BitStringOwned> where Exec: Fn(&Tag, &&'i [u8]) -> PResult<BitStringOwned> {
534        use crate::combinators::congruence::*;
535        use crate::core::exec::bridge_lemmas::*;
536
537        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
538        broadcast use crate::asn1::tag::lemma_const_tag_fmt_exec_inv;
539        broadcast use lemma_parser_congruent_reflexive;
540
541        let _ = ibuf.len();
542        let (tag_len, actual_tag) = TagFmt.parse(ibuf)?;
543        let rest = ibuf.skip(tag_len);
544
545        if actual_tag == primitive_tag(*expected) {
546            let (length_len, content_len) = LengthFmt::<BER>.parse(&rest)?;
547            let content_bytes = rest.skip(length_len);
548            let (content_len, value) = ExactLen(content_len, BitStringFmt::<BER>).parse(
549                &content_bytes,
550            )?;
551            let value = bit_string_to_owned(value);
552            Ok((tag_len + length_len + content_len, value))
553        } else if actual_tag == constructed_tag(*expected) {
554            let (length_len, content_len) = BerLengthFmt.parse(&rest)?;
555            let content_bytes = rest.skip(length_len);
556            let ghost child_spec = spec_rec(TagFmt::BIT_STRING);
557            let child_exec = |input: &&'i [u8]| -> (r: PResult<BitStringOwned>)
558                ensures
559                    parse_matches_spec(r, child_spec.2(input@)),
560                { exec_rec(&TagFmt::BIT_STRING, input) };
561            let child: &FnParser<&'i [u8], BitStringOwned, BundledSpecs<BitStringSpec>, _> =
562                &FnParser::new(child_exec, Ghost(child_spec));
563            proof {
564                lemma_ref_parser_exec_inv::<&'i [u8], _>(child);
565                lemma_ref_safe_productive_inv(child);
566                lemma_ref_fn_parser_congruence(child);
567            }
568
569            let (content_len, value) = match content_len {
570                BerLength::Definite(content_len) => {
571                    let ghost repeated_spec = RepeatTillEnd(child_spec);
572                    let repeated = RepeatTillEnd(child);
573                    let exact = ExactLen(content_len, repeated);
574                    proof {
575                        lemma_repeat_till_end_parser_exec_inv::<&'i [u8], _>(&repeated);
576                        lemma_exact_len_parser_exec_inv::<&'i [u8], _, _>(&exact);
577                        lemma_repeat_till_end_parser_congruence(child, child_spec);
578                        lemma_exact_len_parser_congruence(content_len, repeated, repeated_spec);
579                        reveal(parser_congruent);
580                    }
581                    parse_bit_string_segments(&exact, &content_bytes)?
582                },
583                BerLength::Indefinite => {
584                    let repeated = Repeat(child, EOC);
585                    proof {
586                        lemma_pair_parser_exec_inv::<&'i [u8], _, _>(&EOC);
587                        lemma_repeat_parser_exec_inv::<&'i [u8], _, _>(&repeated);
588                        lemma_repeat_parser_congruence(child, child_spec, EOC, EOC);
589                        reveal(parser_congruent);
590                    }
591                    parse_bit_string_segments_eoc(&repeated, &content_bytes)?
592                },
593            };
594            Ok((tag_len + length_len + content_len, value))
595        } else {
596            Err(ParseError::custom("Tag must match the configured BER BIT STRING identity"))
597        }
598    }
599}
600
601#[cfg(feature = "alloc")]
602impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerBitStringFmt<LIMIT> {
603    type PT = BitStringOwned;
604
605    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
606        FixWith::<LIMIT, _, _>(BerBitStringRecBody, self.0).parse(ibuf)
607    }
608}
609
610} // verus!
vest_lib/asn1/ber/bit_string.rs

vest_lib/asn1/ber/
bit_string.rs
