vest_lib/asn1/
printablestring.rs

1//! ASN.1 PrintableString borrowed and owned values and contents format.
2use super::utf8string::{is_valid_utf8, utf8_from_bytes_unchecked};
3use crate::core::exec::input::{InputBuf, InputSlice};
4use crate::core::exec::output::*;
5use crate::core::exec::{
6    parser::{PResult, Parser},
7    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
8    ParseError,
9};
10use crate::{
11    combinators::{mapped::spec::FnSpecMapper, Mapped, Refined, Tail},
12    core::{proof::*, spec::*},
13};
14#[cfg(feature = "alloc")]
15use alloc::string::String;
16use vstd::prelude::*;
17use vstd::string::StringSliceAdditionalSpecFns;
18use OutputBuf;
19
20verus! {
21
22pub struct PrintableString<'a> {
23    inner: &'a str,
24}
25
26/// Owned PrintableString value used when the wire representation is assembled
27/// from multiple BER segments.
28#[cfg(feature = "alloc")]
29pub struct PrintableStringOwned {
30    inner: String,
31}
32
33#[verifier::ext_equal]
34pub struct PrintableStringSpec {
35    pub inner: Seq<char>,
36}
37
38impl<'a> DeepView for PrintableString<'a> {
39    type V = PrintableStringSpec;
40
41    closed spec fn deep_view(&self) -> Self::V {
42        PrintableStringSpec { inner: self.inner.deep_view() }
43    }
44}
45
46#[cfg(feature = "alloc")]
47impl DeepView for PrintableStringOwned {
48    type V = PrintableStringSpec;
49
50    closed spec fn deep_view(&self) -> Self::V {
51        PrintableStringSpec { inner: self.inner.deep_view() }
52    }
53}
54
55impl<'a> PrintableString<'a> {
56    #[verifier::type_invariant]
57    spec fn wf(&self) -> bool {
58        self.deep_view().wf()
59    }
60
61    pub fn new(inner: &'a str) -> (res: Self)
62        requires
63            is_valid_printable_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),
64        ensures
65            res.deep_view() == (PrintableStringSpec { inner: inner.deep_view() }),
66    {
67        PrintableString { inner }
68    }
69
70    pub fn inner(&self) -> (res: &'a str)
71        ensures
72            res.deep_view() == self.deep_view().inner,
73    {
74        self.inner
75    }
76}
77
78#[cfg(feature = "alloc")]
79impl PrintableStringOwned {
80    #[verifier::type_invariant]
81    spec fn wf(&self) -> bool {
82        self.deep_view().wf()
83    }
84
85    pub fn new(inner: String) -> (res: Self)
86        requires
87            is_valid_printable_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),
88        ensures
89            res.deep_view() == (PrintableStringSpec { inner: inner.deep_view() }),
90    {
91        Self { inner }
92    }
93
94    pub fn inner(&self) -> (res: &str)
95        ensures
96            res.deep_view() == self.deep_view().inner,
97    {
98        self.inner.as_str()
99    }
100}
101
102impl PrintableStringSpec {
103    pub open spec fn wf(&self) -> bool {
104        is_valid_printable_string_spec(vstd::utf8::encode_utf8(self.inner))
105    }
106}
107
108pub open spec fn is_printable_byte(b: u8) -> bool {
109    ||| (0x41 <= b <= 0x5a)  // A-Z
110    ||| (0x61 <= b <= 0x7a)  // a-z
111    ||| (0x30 <= b <= 0x39)  // 0-9
112    ||| b == 0x20  // space
113    ||| b == 0x27  // '
114    ||| b == 0x28  // (
115    ||| b == 0x29  // )
116    ||| b == 0x2b  // +
117    ||| b == 0x2c  // ,
118    ||| b == 0x2d  // -
119    ||| b == 0x2e  // .
120    ||| b == 0x2f  // /
121    ||| b == 0x3a  // :
122    ||| b == 0x3d  // =
123    ||| b == 0x3f  // ?
124
125}
126
127pub open spec fn is_valid_printable_string_spec(bytes: Seq<u8>) -> bool {
128    forall|i: int| 0 <= i < bytes.len() ==> is_printable_byte(#[trigger] bytes[i])
129}
130
131pub fn is_valid_printable_string(bytes: &[u8]) -> (res: bool)
132    ensures
133        res == is_valid_printable_string_spec(bytes.deep_view()),
134{
135    for b in iter: bytes.iter()
136        invariant
137            forall|k: int|
138                0 <= k < iter.index() ==> #[trigger] is_printable_byte(bytes.deep_view()[k]),
139    {
140        if !matches!(
141            b,
142            0x41..=0x5a | // A-Z
143            0x61..=0x7a | // a-z
144            0x30..=0x39 | // 0-9
145            0x20 |        // space
146            0x27 |        // '
147            0x28 |        // (
148            0x29 |        // )
149            0x2b |        // +
150            0x2c |        // ,
151            0x2d |        // -
152            0x2e |        // .
153            0x2f |        // /
154            0x3a |        // :
155            0x3d |        // =
156            0x3f          // ?
157        ) {
158            assert(!is_printable_byte(bytes.deep_view()[iter.index()]));
159            return false;
160        }
161    }
162    true
163}
164
165type PrintableStringFmt = Mapped<
166    Refined<Tail, PredFnSpec<Seq<u8>>>,
167    FnSpecMapper<Seq<u8>, PrintableStringSpec>,
168>;
169
170pub open spec fn printablestring_fmt() -> PrintableStringFmt {
171    Mapped {
172        inner: Refined(
173            Tail,
174            |bytes: Seq<u8>| is_valid_printable_string_spec(bytes) && vstd::utf8::valid_utf8(bytes),
175        ),
176        mapper: (
177            |bytes: Seq<u8>| PrintableStringSpec { inner: vstd::utf8::decode_utf8(bytes) },
178            |s: PrintableStringSpec| vstd::utf8::encode_utf8(s.inner),
179        ),
180    }
181}
182
183mod derived_specs {
184    use super::*;
185
186    impl SpecParser for super::super::PrintableStringFmt {
187        type PVal = PrintableStringSpec;
188
189        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
190            printablestring_fmt().spec_parse(ibuf)
191        }
192    }
193
194    impl Consistency for super::super::PrintableStringFmt {
195        type Val = PrintableStringSpec;
196
197        open spec fn consistent(&self, v: Self::Val) -> bool {
198            printablestring_fmt().consistent(v)
199        }
200    }
201
202    impl SpecSerializerDps for super::super::PrintableStringFmt {
203        type SValue = PrintableStringSpec;
204
205        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
206            printablestring_fmt().spec_serialize_dps(v, obuf)
207        }
208    }
209
210    impl SpecSerializer for super::super::PrintableStringFmt {
211        type SVal = PrintableStringSpec;
212
213        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
214            printablestring_fmt().spec_serialize(v)
215        }
216    }
217
218    impl SpecByteLen for super::super::PrintableStringFmt {
219        type T = PrintableStringSpec;
220
221        open spec fn byte_len(&self, v: Self::T) -> nat {
222            printablestring_fmt().byte_len(v)
223        }
224    }
225
226}
227
228mod derived_proofs {
229    use super::*;
230
231    impl SafeParser for super::super::PrintableStringFmt {
232        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
233            printablestring_fmt().lemma_parse_safe(ibuf);
234        }
235    }
236
237    impl Productive for super::super::PrintableStringFmt {
238        open spec fn productive_inv(&self) -> bool {
239            false
240        }
241
242        proof fn lemma_productive(&self, s: Seq<u8>) {
243        }
244    }
245
246    impl SoundParser for super::super::PrintableStringFmt {
247        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
248            broadcast use vstd::utf8::decode_utf8_encode_utf8;
249
250            printablestring_fmt().lemma_parse_sound_consumption(ibuf);
251        }
252
253        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
254            broadcast use vstd::utf8::decode_utf8_encode_utf8;
255
256            printablestring_fmt().lemma_parse_sound_value(ibuf);
257        }
258    }
259
260    impl GoodSerializer for super::super::PrintableStringFmt {
261        proof fn lemma_serialize_len(&self, v: Self::SVal) {
262            printablestring_fmt().lemma_serialize_len(v);
263        }
264    }
265
266    impl SPRoundTripDps for super::super::PrintableStringFmt {
267        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
268            broadcast use vstd::utf8::encode_utf8_decode_utf8;
269
270            printablestring_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
271        }
272    }
273
274    impl NonMalleable for super::super::PrintableStringFmt {
275        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
276            broadcast use vstd::utf8::decode_utf8_encode_utf8;
277
278            printablestring_fmt().lemma_parse_non_malleable(buf1, buf2);
279        }
280    }
281
282    impl EquivSerializers for super::super::PrintableStringFmt {
283        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
284            printablestring_fmt().lemma_serialize_equiv_on_empty(v);
285        }
286    }
287
288}
289
290impl<'i> Parser<&'i [u8]> for super::PrintableStringFmt {
291    type PT = PrintableString<'i>;
292
293    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
294        let (n, bytes) = Tail.parse(ibuf)?;
295        if !is_valid_printable_string(bytes) {
296            Err(ParseError::custom("Invalid PrintableString"))
297        } else if !is_valid_utf8(bytes) {
298            Err(ParseError::custom("Invalid UTF-8"))
299        } else {
300            let inner = utf8_from_bytes_unchecked(bytes);
301            Ok((n, PrintableString::new(inner)))
302        }
303    }
304}
305
306impl<Output: OutputBuf, 'i> Serializer<Output, PrintableString<'i>> for super::PrintableStringFmt {
307    fn serialize_into(&self, v: &PrintableString<'i>, obuf: &mut Output) {
308        proof {
309            use_type_invariant(v);
310        }
311        let bytes = v.inner.as_bytes();
312        Tail.serialize_into(&bytes, obuf);
313    }
314}
315
316impl<'i> Prepare<PrintableString<'i>> for super::PrintableStringFmt {
317    fn prepare(&self, v: &PrintableString<'i>) -> Result<usize, PreSerializeError> {
318        broadcast use vstd::utf8::encode_utf8_valid_utf8;
319
320        proof {
321            use_type_invariant(v);
322        }
323        let bytes = v.inner.as_bytes();
324        Tail.prepare(&bytes)
325    }
326}
327
328impl<'i> ByteLen<PrintableString<'i>> for super::PrintableStringFmt {
329    fn length(&self, v: &PrintableString<'i>) -> usize {
330        proof {
331            use_type_invariant(v);
332        }
333        let bytes = v.inner.as_bytes();
334        Tail.length(&bytes)
335    }
336}
337
338#[cfg(feature = "alloc")]
339impl<Output: OutputBuf> Serializer<Output, PrintableStringOwned> for super::PrintableStringFmt {
340    fn serialize_into(&self, v: &PrintableStringOwned, obuf: &mut Output) {
341        proof {
342            use_type_invariant(v);
343        }
344        let bytes = v.inner.as_str().as_bytes();
345        Tail.serialize_into(&bytes, obuf);
346    }
347}
348
349#[cfg(feature = "alloc")]
350impl Prepare<PrintableStringOwned> for super::PrintableStringFmt {
351    fn prepare(&self, v: &PrintableStringOwned) -> Result<usize, PreSerializeError> {
352        broadcast use vstd::utf8::encode_utf8_valid_utf8;
353
354        proof {
355            use_type_invariant(v);
356        }
357        let bytes = v.inner.as_str().as_bytes();
358        Tail.prepare(&bytes)
359    }
360}
361
362#[cfg(feature = "alloc")]
363impl ByteLen<PrintableStringOwned> for super::PrintableStringFmt {
364    fn length(&self, v: &PrintableStringOwned) -> usize {
365        proof {
366            use_type_invariant(v);
367        }
368        let bytes = v.inner.as_str().as_bytes();
369        Tail.length(&bytes)
370    }
371}
372
373} // verus!
vest_lib/asn1/printablestring.rs

vest_lib/asn1/
printablestring.rs
