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
108/// Tests membership in PrintableString's ASCII repertoire.
109#[verifier::allow_in_spec]
110pub fn is_printable_byte(b: u8) -> bool
111    returns
112        matches!(b, b'A'..=b'Z' | b'a'..=b'z' | b'0'..=b'9'
113            | b' ' | b'\'' | b'(' | b')' | b'+' | b',' | b'-' | b'.' | b'/'
114            | b':' | b'=' | b'?'),
115{
116    matches!(b, b'A'..=b'Z' | b'a'..=b'z' | b'0'..=b'9'
117        | b' ' | b'\'' | b'(' | b')' | b'+' | b',' | b'-' | b'.' | b'/'
118        | b':' | b'=' | b'?')
119}
120
121pub open spec fn is_valid_printable_string_spec(bytes: Seq<u8>) -> bool {
122    forall|i: int| 0 <= i < bytes.len() ==> is_printable_byte(#[trigger] bytes[i])
123}
124
125/// Checks PrintableString contents without allocation.
126#[verifier::allow_in_spec]
127pub fn is_valid_printable_string(bytes: &[u8]) -> (res: bool)
128    returns
129        is_valid_printable_string_spec(bytes.deep_view()),
130{
131    assert(bytes@ == bytes.deep_view());
132    bytes.iter().all(
133        |&b: &u8| -> (valid: bool)
134            ensures
135                valid == is_printable_byte(b),
136            { is_printable_byte(b) },
137    )
138}
139
140type PrintableStringFmt = Mapped<
141    Refined<Tail, PredFnSpec<Seq<u8>>>,
142    FnSpecMapper<Seq<u8>, PrintableStringSpec>,
143>;
144
145pub open spec fn printablestring_fmt() -> PrintableStringFmt {
146    Mapped {
147        inner: Refined(
148            Tail,
149            |bytes: Seq<u8>| is_valid_printable_string_spec(bytes) && vstd::utf8::valid_utf8(bytes),
150        ),
151        mapper: (
152            |bytes: Seq<u8>| PrintableStringSpec { inner: vstd::utf8::decode_utf8(bytes) },
153            |s: PrintableStringSpec| vstd::utf8::encode_utf8(s.inner),
154        ),
155    }
156}
157
158mod derived_specs {
159    use super::*;
160
161    impl SpecParser for super::super::PrintableStringFmt {
162        type PVal = PrintableStringSpec;
163
164        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
165            printablestring_fmt().spec_parse(ibuf)
166        }
167    }
168
169    impl Consistency for super::super::PrintableStringFmt {
170        type Val = PrintableStringSpec;
171
172        open spec fn consistent(&self, v: Self::Val) -> bool {
173            printablestring_fmt().consistent(v)
174        }
175    }
176
177    impl SpecSerializerDps for super::super::PrintableStringFmt {
178        type SValue = PrintableStringSpec;
179
180        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
181            printablestring_fmt().spec_serialize_dps(v, obuf)
182        }
183    }
184
185    impl SpecSerializer for super::super::PrintableStringFmt {
186        type SVal = PrintableStringSpec;
187
188        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
189            printablestring_fmt().spec_serialize(v)
190        }
191    }
192
193    impl SpecByteLen for super::super::PrintableStringFmt {
194        type T = PrintableStringSpec;
195
196        open spec fn byte_len(&self, v: Self::T) -> nat {
197            printablestring_fmt().byte_len(v)
198        }
199    }
200
201}
202
203mod derived_proofs {
204    use super::*;
205
206    impl SafeParser for super::super::PrintableStringFmt {
207        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
208            printablestring_fmt().lemma_parse_safe(ibuf);
209        }
210    }
211
212    impl Productive for super::super::PrintableStringFmt {
213        open spec fn productive_inv(&self) -> bool {
214            false
215        }
216
217        proof fn lemma_productive(&self, s: Seq<u8>) {
218        }
219    }
220
221    impl SoundParser for super::super::PrintableStringFmt {
222        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
223            broadcast use vstd::utf8::decode_utf8_encode_utf8;
224
225            printablestring_fmt().lemma_parse_sound_consumption(ibuf);
226        }
227
228        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
229            broadcast use vstd::utf8::decode_utf8_encode_utf8;
230
231            printablestring_fmt().lemma_parse_sound_value(ibuf);
232        }
233    }
234
235    impl GoodSerializer for super::super::PrintableStringFmt {
236        proof fn lemma_serialize_len(&self, v: Self::SVal) {
237            printablestring_fmt().lemma_serialize_len(v);
238        }
239    }
240
241    impl SPRoundTripDps for super::super::PrintableStringFmt {
242        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
243            broadcast use vstd::utf8::encode_utf8_decode_utf8;
244
245            printablestring_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
246        }
247    }
248
249    impl NonMalleable for super::super::PrintableStringFmt {
250        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
251            broadcast use vstd::utf8::decode_utf8_encode_utf8;
252
253            printablestring_fmt().lemma_parse_non_malleable(buf1, buf2);
254        }
255    }
256
257    impl EquivSerializers for super::super::PrintableStringFmt {
258        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
259            printablestring_fmt().lemma_serialize_equiv_on_empty(v);
260        }
261    }
262
263}
264
265impl<'i> Parser<&'i [u8]> for super::PrintableStringFmt {
266    type PT = PrintableString<'i>;
267
268    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
269        let (n, bytes) = Tail.parse(ibuf)?;
270        if !is_valid_printable_string(bytes) {
271            Err(ParseError::custom("Invalid PrintableString"))
272        } else if !is_valid_utf8(bytes) {
273            Err(ParseError::custom("Invalid UTF-8"))
274        } else {
275            let inner = utf8_from_bytes_unchecked(bytes);
276            Ok((n, PrintableString::new(inner)))
277        }
278    }
279}
280
281impl<Output: OutputBuf, 'i> Serializer<Output, PrintableString<'i>> for super::PrintableStringFmt {
282    fn serialize_into(&self, v: &PrintableString<'i>, obuf: &mut Output) {
283        proof {
284            use_type_invariant(v);
285        }
286        let bytes = v.inner.as_bytes();
287        Tail.serialize_into(&bytes, obuf);
288    }
289}
290
291impl<'i> Prepare<PrintableString<'i>> for super::PrintableStringFmt {
292    fn prepare(&self, v: &PrintableString<'i>) -> Result<usize, PreSerializeError> {
293        broadcast use vstd::utf8::encode_utf8_valid_utf8;
294
295        proof {
296            use_type_invariant(v);
297        }
298        let bytes = v.inner.as_bytes();
299        Tail.prepare(&bytes)
300    }
301}
302
303impl<'i> ByteLen<PrintableString<'i>> for super::PrintableStringFmt {
304    fn length(&self, v: &PrintableString<'i>) -> usize {
305        proof {
306            use_type_invariant(v);
307        }
308        let bytes = v.inner.as_bytes();
309        Tail.length(&bytes)
310    }
311}
312
313#[cfg(feature = "alloc")]
314impl<Output: OutputBuf> Serializer<Output, PrintableStringOwned> for super::PrintableStringFmt {
315    fn serialize_into(&self, v: &PrintableStringOwned, obuf: &mut Output) {
316        proof {
317            use_type_invariant(v);
318        }
319        let bytes = v.inner.as_str().as_bytes();
320        Tail.serialize_into(&bytes, obuf);
321    }
322}
323
324#[cfg(feature = "alloc")]
325impl Prepare<PrintableStringOwned> for super::PrintableStringFmt {
326    fn prepare(&self, v: &PrintableStringOwned) -> Result<usize, PreSerializeError> {
327        broadcast use vstd::utf8::encode_utf8_valid_utf8;
328
329        proof {
330            use_type_invariant(v);
331        }
332        let bytes = v.inner.as_str().as_bytes();
333        Tail.prepare(&bytes)
334    }
335}
336
337#[cfg(feature = "alloc")]
338impl ByteLen<PrintableStringOwned> for super::PrintableStringFmt {
339    fn length(&self, v: &PrintableStringOwned) -> usize {
340        proof {
341            use_type_invariant(v);
342        }
343        let bytes = v.inner.as_str().as_bytes();
344        Tail.length(&bytes)
345    }
346}
347
348} // verus!
vest_lib/asn1/printablestring.rs

vest_lib/asn1/
printablestring.rs
