vest_lib/asn1/ber/
char_string.rs

1//! BER restricted character string combinators.
2use crate::asn1::{
3    primitive_tag, ASN1Fmt, BmpStringFmt, Class, Ia5StringFmt, NumericStringFmt,
4    PrintableStringFmt, Tag, TagFmt, TeletexStringFmt, UniversalStringFmt, Utf8StringFmt, BER,
5};
6#[cfg(feature = "alloc")]
7use crate::asn1::{
8    BmpString, Ia5StringOwned, NumericStringOwned, PrintableStringOwned, TeletexStringOwned,
9    UniversalString, Utf8StringOwned,
10};
11use crate::combinators::{mapped::spec::FnSpecMapper, Mapped, Refined};
12use crate::core::exec::parser::*;
13use crate::core::exec::{
14    ByteLen, OutputBuf, PResult, ParseError, Parser, PreSerializeError, Prepare, Serializer,
15};
16use crate::core::{proof::*, spec::*};
17#[cfg(feature = "alloc")]
18use alloc::string::String;
19#[cfg(feature = "alloc")]
20use alloc::vec::Vec;
21use vstd::prelude::*;
22
23use super::octet_string::BerOctetStringFmt;
24
25verus! {
26
27type BerRestrictedStringFmt__<C, const LIMIT: usize> = Mapped<
28    Refined<BerOctetStringFmt<LIMIT>, PredFnSpec<Seq<u8>>>,
29    FnSpecMapper<Seq<u8>, <C as SpecByteLen>::T>,
30>;
31
32/// reject invalid flattened contents, then map the validated octets to the string value.
33pub open spec fn ber_char_string_fmt<C: SpecCombinator, const LIMIT: usize>(
34    tag: Tag,
35    content: C,
36) -> BerRestrictedStringFmt__<C, LIMIT> {
37    Mapped {
38        inner: Refined(
39            BerOctetStringFmt::<LIMIT>(tag),
40            |bytes: Seq<u8>| content.spec_parse(bytes) is Some,
41        ),
42        mapper: (
43            |bytes: Seq<u8>| (content.spec_parse(bytes)->0).1,
44            |value: C::T| content.spec_serialize(value),
45        ),
46    }
47}
48
49/// BER restricted character string represented as an IMPLICITly tagged BER OCTET STRING.
50///
51/// Parsing accepts primitive, definite constructed, indefinite constructed, and nested forms.
52/// Only the outermost tag is configurable; recursive components retain the universal OCTET STRING
53/// tag. Serialization is normalized to primitive definite form.
54#[verifier::allow(autoderive_clone_without_spec)]
55#[derive(Clone, Copy)]
56pub struct BerCharStringFmt<C, const LIMIT: usize>(pub Tag, pub C);
57
58mod derived_specs {
59    use super::*;
60
61    impl<C: SpecCombinator, const LIMIT: usize> SpecParser for BerCharStringFmt<C, LIMIT> {
62        type PVal = C::T;
63
64        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
65            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).spec_parse(ibuf)
66        }
67    }
68
69    impl<C: SpecCombinator, const LIMIT: usize> Consistency for BerCharStringFmt<C, LIMIT> {
70        type Val = C::T;
71
72        open spec fn consistent(&self, value: Self::Val) -> bool {
73            &&& self.1.consistent(value)
74            &&& ber_char_string_fmt::<C, LIMIT>(self.0, self.1).consistent(value)
75        }
76    }
77
78    impl<C: SpecCombinator, const LIMIT: usize> SpecSerializerDps for BerCharStringFmt<C, LIMIT> {
79        type SValue = C::T;
80
81        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
82            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).spec_serialize_dps(value, obuf)
83        }
84    }
85
86    impl<C: SpecCombinator, const LIMIT: usize> SpecSerializer for BerCharStringFmt<C, LIMIT> {
87        type SVal = C::T;
88
89        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
90            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).spec_serialize(value)
91        }
92    }
93
94    impl<C: SpecCombinator, const LIMIT: usize> SpecByteLen for BerCharStringFmt<C, LIMIT> {
95        type T = C::T;
96
97        open spec fn byte_len(&self, value: Self::T) -> nat {
98            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).byte_len(value)
99        }
100    }
101
102}
103
104mod derived_proofs {
105    use super::*;
106
107    impl<C: SpecCombinator, const LIMIT: usize> SafeParser for BerCharStringFmt<C, LIMIT> {
108        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
109            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_parse_safe(ibuf);
110        }
111    }
112
113    impl<C: SpecCombinator, const LIMIT: usize> Productive for BerCharStringFmt<C, LIMIT> {
114        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
115            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_productive(ibuf);
116        }
117    }
118
119    impl<C: SpecCombinator, const LIMIT: usize> GoodSerializer for BerCharStringFmt<C, LIMIT> {
120        proof fn lemma_serialize_len(&self, value: Self::SVal) {
121            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_serialize_len(value);
122        }
123    }
124
125    impl<C: SpecCombinator, const LIMIT: usize> NonTailFmt for BerCharStringFmt<C, LIMIT> {
126        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
127            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_serialize_dps_prepend(
128                value,
129                obuf,
130            );
131        }
132
133        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
134            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_serialize_dps_len(value, obuf);
135        }
136    }
137
138    impl<C: SpecCombinator, const LIMIT: usize> EquivSerializersGeneral for BerCharStringFmt<
139        C,
140        LIMIT,
141    > {
142        proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
143            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_serialize_equiv(value, obuf);
144        }
145    }
146
147    impl<C: SpecCombinator, const LIMIT: usize> EquivSerializers for BerCharStringFmt<C, LIMIT> {
148        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
149            ber_char_string_fmt::<C, LIMIT>(self.0, self.1).lemma_serialize_equiv_on_empty(value);
150        }
151    }
152
153    impl<C: SpecCombinator + SPRoundTrip, const LIMIT: usize> SPRoundTripDps for BerCharStringFmt<
154        C,
155        LIMIT,
156    > {
157        open spec fn unambiguous(&self) -> bool {
158            self.1.sp_roundtrip_inv()
159        }
160
161        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
162            let bytes = self.1.spec_serialize(value);
163            self.1.theorem_serialize_parse_roundtrip(value);
164            BerOctetStringFmt::<LIMIT>(self.0).theorem_serialize_dps_parse_roundtrip(bytes, obuf);
165        }
166    }
167
168}
169
170impl<C: Copy, const LIMIT: usize> BerCharStringFmt<C, LIMIT> {
171    #[verifier::allow_in_spec]
172    pub const fn with_implicit_tag(content: C, class: Class, number: u64) -> Self
173        returns
174            Self(
175                Tag {
176                    class,
177                    constructed: false,
178                    number: crate::asn1::tag::tag_num_from_uint(number),
179                },
180                content,
181            ),
182    {
183        Self(
184            Tag { class, constructed: false, number: crate::asn1::tag::tag_num_from_uint(number) },
185            content,
186        )
187    }
188}
189
190pub type BerUtf8StringFmt<const LIMIT: usize> = BerCharStringFmt<Utf8StringFmt, LIMIT>;
191
192pub type BerPrintableStringFmt<const LIMIT: usize> = BerCharStringFmt<PrintableStringFmt, LIMIT>;
193
194pub type BerIa5StringFmt<const LIMIT: usize> = BerCharStringFmt<Ia5StringFmt, LIMIT>;
195
196pub type BerTeletexStringFmt<const LIMIT: usize> = BerCharStringFmt<TeletexStringFmt, LIMIT>;
197
198pub type BerBmpStringFmt<const LIMIT: usize> = BerCharStringFmt<BmpStringFmt, LIMIT>;
199
200pub type BerNumericStringFmt<const LIMIT: usize> = BerCharStringFmt<NumericStringFmt, LIMIT>;
201
202pub type BerUniversalStringFmt<const LIMIT: usize> = BerCharStringFmt<UniversalStringFmt, LIMIT>;
203
204impl<const LIMIT: usize> BerUtf8StringFmt<LIMIT> {
205    #[verifier::allow_in_spec]
206    pub const fn universal() -> Self
207        returns
208            Self(TagFmt::UTF8_STRING, Utf8StringFmt),
209    {
210        Self(TagFmt::UTF8_STRING, Utf8StringFmt)
211    }
212
213    #[verifier::allow_in_spec]
214    pub const fn implicit(class: Class, number: u64) -> Self
215        returns
216            Self::with_implicit_tag(Utf8StringFmt, class, number),
217    {
218        Self::with_implicit_tag(Utf8StringFmt, class, number)
219    }
220}
221
222impl<const LIMIT: usize> BerPrintableStringFmt<LIMIT> {
223    #[verifier::allow_in_spec]
224    pub const fn universal() -> Self
225        returns
226            Self(TagFmt::PRINTABLE_STRING, PrintableStringFmt),
227    {
228        Self(TagFmt::PRINTABLE_STRING, PrintableStringFmt)
229    }
230
231    #[verifier::allow_in_spec]
232    pub const fn implicit(class: Class, number: u64) -> Self
233        returns
234            Self::with_implicit_tag(PrintableStringFmt, class, number),
235    {
236        Self::with_implicit_tag(PrintableStringFmt, class, number)
237    }
238}
239
240impl<const LIMIT: usize> BerIa5StringFmt<LIMIT> {
241    #[verifier::allow_in_spec]
242    pub const fn universal() -> Self
243        returns
244            Self(TagFmt::IA5_STRING, Ia5StringFmt),
245    {
246        Self(TagFmt::IA5_STRING, Ia5StringFmt)
247    }
248
249    #[verifier::allow_in_spec]
250    pub const fn implicit(class: Class, number: u64) -> Self
251        returns
252            Self::with_implicit_tag(Ia5StringFmt, class, number),
253    {
254        Self::with_implicit_tag(Ia5StringFmt, class, number)
255    }
256}
257
258impl<const LIMIT: usize> BerTeletexStringFmt<LIMIT> {
259    #[verifier::allow_in_spec]
260    pub const fn universal() -> Self
261        returns
262            Self(TagFmt::TELETEX_STRING, TeletexStringFmt),
263    {
264        Self(TagFmt::TELETEX_STRING, TeletexStringFmt)
265    }
266
267    #[verifier::allow_in_spec]
268    pub const fn implicit(class: Class, number: u64) -> Self
269        returns
270            Self::with_implicit_tag(TeletexStringFmt, class, number),
271    {
272        Self::with_implicit_tag(TeletexStringFmt, class, number)
273    }
274}
275
276impl<const LIMIT: usize> BerBmpStringFmt<LIMIT> {
277    #[verifier::allow_in_spec]
278    pub const fn universal() -> Self
279        returns
280            Self(TagFmt::BMP_STRING, BmpStringFmt),
281    {
282        Self(TagFmt::BMP_STRING, BmpStringFmt)
283    }
284
285    #[verifier::allow_in_spec]
286    pub const fn implicit(class: Class, number: u64) -> Self
287        returns
288            Self::with_implicit_tag(BmpStringFmt, class, number),
289    {
290        Self::with_implicit_tag(BmpStringFmt, class, number)
291    }
292}
293
294impl<const LIMIT: usize> BerNumericStringFmt<LIMIT> {
295    #[verifier::allow_in_spec]
296    pub const fn universal() -> Self
297        returns
298            Self(TagFmt::NUMERIC_STRING, NumericStringFmt),
299    {
300        Self(TagFmt::NUMERIC_STRING, NumericStringFmt)
301    }
302}
303
304impl<const LIMIT: usize> BerUniversalStringFmt<LIMIT> {
305    #[verifier::allow_in_spec]
306    pub const fn universal() -> Self
307        returns
308            Self(TagFmt::UNIVERSAL_STRING, UniversalStringFmt),
309    {
310        Self(TagFmt::UNIVERSAL_STRING, UniversalStringFmt)
311    }
312}
313
314/// Executable bridge from owned BER contents octets to owned values.
315#[cfg(feature = "alloc")]
316pub trait BerDecoderOwned: SpecCombinator {
317    type Owned: DeepView<V = Self::T>;
318
319    fn decode_owned(&self, bytes: Vec<u8>) -> (r: Result<Self::Owned, ParseError>)
320        ensures
321            ({
322                let expected = match self.spec_parse(bytes.deep_view()) {
323                    Some((_, value)) => Some(value),
324                    None => None,
325                };
326                &&& r is Ok <==> expected is Some
327                &&& r is Err <==> expected is None
328                &&& r matches Ok(value) ==> expected == Some(value.deep_view())
329            }),
330    ;
331}
332
333#[cfg(feature = "alloc")]
334impl BerDecoderOwned for Utf8StringFmt {
335    type Owned = Utf8StringOwned;
336
337    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
338        let input = bytes.as_slice();
339        if crate::asn1::utf8string::is_valid_utf8(input) {
340            // SAFETY: the branch condition establishes that `bytes` is valid UTF-8.
341            let inner = unsafe { String::from_utf8_unchecked(bytes) };
342            Ok(inner)
343        } else {
344            Err(ParseError::custom("Invalid UTF-8"))
345        }
346    }
347}
348
349#[cfg(feature = "alloc")]
350impl BerDecoderOwned for PrintableStringFmt {
351    type Owned = PrintableStringOwned;
352
353    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
354        broadcast use vstd::utf8::decode_utf8_encode_utf8;
355
356        let input = bytes.as_slice();
357        if !crate::asn1::printablestring::is_valid_printable_string(input) {
358            Err(ParseError::custom("Invalid PrintableString"))
359        } else if !crate::asn1::utf8string::is_valid_utf8(input) {
360            Err(ParseError::custom("Invalid UTF-8"))
361        } else {
362            // SAFETY: the preceding check establishes that `bytes` is valid UTF-8.
363            let inner = unsafe { String::from_utf8_unchecked(bytes) };
364            Ok(PrintableStringOwned::new(inner))
365        }
366    }
367}
368
369#[cfg(feature = "alloc")]
370impl BerDecoderOwned for NumericStringFmt {
371    type Owned = NumericStringOwned;
372
373    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
374        let value = <PrintableStringFmt as BerDecoderOwned>::decode_owned(
375            &PrintableStringFmt,
376            bytes,
377        )?;
378        if crate::core::exec::fns::Pred::test(
379            &crate::asn1::numericstring::NumericStringChars,
380            &value,
381        ) {
382            Ok(value)
383        } else {
384            Err(ParseError::custom("Invalid NumericString"))
385        }
386    }
387}
388
389#[cfg(feature = "alloc")]
390impl BerDecoderOwned for UniversalStringFmt {
391    type Owned = UniversalString;
392
393    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
394        if crate::asn1::universalstring::check_valid_universal_string(bytes.as_slice()) {
395            Ok(crate::asn1::universalstring::decode_universal_string_owned(bytes.as_slice()))
396        } else {
397            Err(ParseError::custom("Invalid UniversalString"))
398        }
399    }
400}
401
402#[cfg(feature = "alloc")]
403impl BerDecoderOwned for Ia5StringFmt {
404    type Owned = Ia5StringOwned;
405
406    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
407        broadcast use vstd::utf8::decode_utf8_encode_utf8;
408
409        let input = bytes.as_slice();
410        if !crate::asn1::ia5string::is_valid_ia5_string(input) {
411            Err(ParseError::custom("Invalid IA5String"))
412        } else if !crate::asn1::utf8string::is_valid_utf8(input) {
413            Err(ParseError::custom("Invalid UTF-8"))
414        } else {
415            // SAFETY: the preceding check establishes that `bytes` is valid UTF-8.
416            let inner = unsafe { String::from_utf8_unchecked(bytes) };
417            Ok(Ia5StringOwned::new(inner))
418        }
419    }
420}
421
422#[cfg(feature = "alloc")]
423impl BerDecoderOwned for TeletexStringFmt {
424    type Owned = TeletexStringOwned;
425
426    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
427        broadcast use vstd::utf8::decode_utf8_encode_utf8;
428
429        let input = bytes.as_slice();
430        if !crate::asn1::teletexstring::is_valid_teletex_string(input) {
431            Err(ParseError::custom("Invalid TeletexString"))
432        } else if !crate::asn1::utf8string::is_valid_utf8(input) {
433            Err(ParseError::custom("Invalid UTF-8"))
434        } else {
435            // SAFETY: the preceding check establishes that `bytes` is valid UTF-8.
436            let inner = unsafe { String::from_utf8_unchecked(bytes) };
437            Ok(TeletexStringOwned::new(inner))
438        }
439    }
440}
441
442#[cfg(feature = "alloc")]
443impl BerDecoderOwned for BmpStringFmt {
444    type Owned = BmpString;
445
446    fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError> {
447        assert(bytes@ == bytes.deep_view());
448        let (_, parsed) = BmpStringFmt.parse(&bytes.as_slice())?;
449        Ok(parsed)
450    }
451}
452
453#[cfg(feature = "alloc")]
454impl<'i, C, const LIMIT: usize> Parser<&'i [u8]> for BerCharStringFmt<C, LIMIT> where
455    C: BerDecoderOwned,
456 {
457    type PT = C::Owned;
458
459    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
460        let (n, bytes) = BerOctetStringFmt::<LIMIT>(self.0).parse(ibuf)?;
461        let value = self.1.decode_owned(bytes)?;
462        Ok((n, value))
463    }
464}
465
466impl<Output, C, T, const LIMIT: usize> Serializer<Output, T> for BerCharStringFmt<C, LIMIT> where
467    Output: OutputBuf,
468    T: DeepView + ?Sized,
469    C: SpecCombinator + Copy + GoodSerializer + Serializer<Output, T> + ByteLen<T>,
470 {
471    #[verifier::prophetic]
472    open spec fn exec_inv(&self) -> bool {
473        &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
474        &&& <C as ByteLen<T>>::exec_inv(&self.1)
475        &&& self.1.serialize_inv()
476    }
477
478    fn serialize_into(&self, value: &T, obuf: &mut Output) {
479        proof {
480            self.1.lemma_serialize_len(value.deep_view());
481        }
482        let normalized = ASN1Fmt::<C, BER>(primitive_tag(self.0), self.1);
483        normalized.serialize_into(value, obuf);
484    }
485}
486
487impl<C, T, const LIMIT: usize> Prepare<T> for BerCharStringFmt<C, LIMIT> where
488    T: DeepView + ?Sized,
489    C: SpecCombinator + Copy + GoodSerializer + SPRoundTrip + Prepare<T>,
490 {
491    open spec fn exec_inv(&self) -> bool {
492        &&& <C as Prepare<T>>::exec_inv(&self.1)
493        &&& self.1.serialize_inv()
494        &&& self.1.sp_roundtrip_inv()
495    }
496
497    fn prepare(&self, value: &T) -> Result<usize, PreSerializeError> {
498        let normalized = ASN1Fmt::<C, BER>(primitive_tag(self.0), self.1);
499        let result = normalized.prepare(value);
500        proof {
501            if let Ok(_len) = result {
502                self.1.lemma_serialize_len(value.deep_view());
503                self.1.theorem_serialize_parse_roundtrip(value.deep_view());
504            }
505        }
506        result
507    }
508}
509
510impl<C, T, const LIMIT: usize> ByteLen<T> for BerCharStringFmt<C, LIMIT> where
511    T: DeepView + ?Sized,
512    C: SpecCombinator + Copy + GoodSerializer + ByteLen<T>,
513 {
514    open spec fn exec_inv(&self) -> bool {
515        <C as ByteLen<T>>::exec_inv(&self.1) && self.1.serialize_inv()
516    }
517
518    fn length(&self, value: &T) -> usize {
519        proof {
520            self.1.lemma_serialize_len(value.deep_view());
521        }
522        let normalized = ASN1Fmt::<C, BER>(primitive_tag(self.0), self.1);
523        normalized.length(value)
524    }
525}
526
527} // verus!
vest_lib/asn1/ber/char_string.rs

vest_lib/asn1/ber/
char_string.rs
