vest_lib/asn1/
ia5string.rs

1//! ASN.1 IA5String 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 Ia5String<'a> {
23    inner: &'a str,
24}
25
26/// Owned IA5String value used when the wire representation is assembled from
27/// multiple BER segments.
28#[cfg(feature = "alloc")]
29pub struct Ia5StringOwned {
30    inner: String,
31}
32
33#[verifier::ext_equal]
34pub struct Ia5StringSpec {
35    pub inner: Seq<char>,
36}
37
38impl<'a> DeepView for Ia5String<'a> {
39    type V = Ia5StringSpec;
40
41    closed spec fn deep_view(&self) -> Self::V {
42        Ia5StringSpec { inner: self.inner.deep_view() }
43    }
44}
45
46#[cfg(feature = "alloc")]
47impl DeepView for Ia5StringOwned {
48    type V = Ia5StringSpec;
49
50    closed spec fn deep_view(&self) -> Self::V {
51        Ia5StringSpec { inner: self.inner.deep_view() }
52    }
53}
54
55impl<'a> Ia5String<'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_ia5_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),
64        ensures
65            res.deep_view() == (Ia5StringSpec { inner: inner.deep_view() }),
66    {
67        Ia5String { 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 Ia5StringOwned {
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_ia5_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),
88        ensures
89            res.deep_view() == (Ia5StringSpec { 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 Ia5StringSpec {
103    pub open spec fn wf(&self) -> bool {
104        is_valid_ia5_string_spec(vstd::utf8::encode_utf8(self.inner))
105    }
106}
107
108pub open spec fn is_valid_ia5_string_spec(bytes: Seq<u8>) -> bool {
109    forall|i: int| 0 <= i < bytes.len() ==> #[trigger] bytes[i] <= 127
110}
111
112pub fn is_valid_ia5_string(bytes: &[u8]) -> (res: bool)
113    ensures
114        res == is_valid_ia5_string_spec(bytes.deep_view()),
115{
116    for b in iter: bytes.iter()
117        invariant
118            forall|k: int| 0 <= k < iter.index() ==> #[trigger] bytes.deep_view()[k] <= 127,
119    {
120        if *b > 127 {
121            assert(bytes.deep_view()[iter.index()] > 127);
122            return false;
123        }
124    }
125    true
126}
127
128type Ia5StringFmt = Mapped<
129    Refined<Tail, PredFnSpec<Seq<u8>>>,
130    FnSpecMapper<Seq<u8>, Ia5StringSpec>,
131>;
132
133pub open spec fn ia5string_fmt() -> Ia5StringFmt {
134    Mapped {
135        inner: Refined(
136            Tail,
137            |bytes: Seq<u8>| is_valid_ia5_string_spec(bytes) && vstd::utf8::valid_utf8(bytes),
138        ),
139        mapper: (
140            |bytes: Seq<u8>| Ia5StringSpec { inner: vstd::utf8::decode_utf8(bytes) },
141            |s: Ia5StringSpec| vstd::utf8::encode_utf8(s.inner),
142        ),
143    }
144}
145
146mod derived_specs {
147    use super::*;
148
149    impl SpecParser for super::super::Ia5StringFmt {
150        type PVal = Ia5StringSpec;
151
152        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
153            ia5string_fmt().spec_parse(ibuf)
154        }
155    }
156
157    impl Consistency for super::super::Ia5StringFmt {
158        type Val = Ia5StringSpec;
159
160        open spec fn consistent(&self, v: Self::Val) -> bool {
161            ia5string_fmt().consistent(v)
162        }
163    }
164
165    impl SpecSerializerDps for super::super::Ia5StringFmt {
166        type SValue = Ia5StringSpec;
167
168        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
169            ia5string_fmt().spec_serialize_dps(v, obuf)
170        }
171    }
172
173    impl SpecSerializer for super::super::Ia5StringFmt {
174        type SVal = Ia5StringSpec;
175
176        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
177            ia5string_fmt().spec_serialize(v)
178        }
179    }
180
181    impl SpecByteLen for super::super::Ia5StringFmt {
182        type T = Ia5StringSpec;
183
184        open spec fn byte_len(&self, v: Self::T) -> nat {
185            ia5string_fmt().byte_len(v)
186        }
187    }
188
189}
190
191mod derived_proofs {
192    use super::*;
193
194    impl SafeParser for super::super::Ia5StringFmt {
195        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
196            ia5string_fmt().lemma_parse_safe(ibuf);
197        }
198    }
199
200    impl Productive for super::super::Ia5StringFmt {
201        open spec fn productive_inv(&self) -> bool {
202            false
203        }
204
205        proof fn lemma_productive(&self, s: Seq<u8>) {
206        }
207    }
208
209    impl SoundParser for super::super::Ia5StringFmt {
210        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
211            broadcast use vstd::utf8::decode_utf8_encode_utf8;
212
213            ia5string_fmt().lemma_parse_sound_consumption(ibuf);
214        }
215
216        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
217            broadcast use vstd::utf8::decode_utf8_encode_utf8;
218
219            ia5string_fmt().lemma_parse_sound_value(ibuf);
220        }
221    }
222
223    impl GoodSerializer for super::super::Ia5StringFmt {
224        proof fn lemma_serialize_len(&self, v: Self::SVal) {
225            ia5string_fmt().lemma_serialize_len(v);
226        }
227    }
228
229    impl SPRoundTripDps for super::super::Ia5StringFmt {
230        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
231            broadcast use vstd::utf8::encode_utf8_decode_utf8;
232
233            ia5string_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
234        }
235    }
236
237    impl NonMalleable for super::super::Ia5StringFmt {
238        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
239            broadcast use vstd::utf8::decode_utf8_encode_utf8;
240
241            ia5string_fmt().lemma_parse_non_malleable(buf1, buf2);
242        }
243    }
244
245    impl EquivSerializers for super::super::Ia5StringFmt {
246        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
247            ia5string_fmt().lemma_serialize_equiv_on_empty(v);
248        }
249    }
250
251}
252
253impl<'i> Parser<&'i [u8]> for super::Ia5StringFmt {
254    type PT = Ia5String<'i>;
255
256    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
257        let (n, bytes) = Tail.parse(ibuf)?;
258        if !is_valid_ia5_string(bytes) {
259            Err(ParseError::custom("Invalid Ia5String"))
260        } else if !is_valid_utf8(bytes) {
261            Err(ParseError::custom("Invalid UTF-8"))
262        } else {
263            let inner = utf8_from_bytes_unchecked(bytes);
264            Ok((n, Ia5String::new(inner)))
265        }
266    }
267}
268
269impl<Output: OutputBuf, 'i> Serializer<Output, Ia5String<'i>> for super::Ia5StringFmt {
270    fn serialize_into(&self, v: &Ia5String<'i>, obuf: &mut Output) {
271        proof {
272            use_type_invariant(v);
273        }
274        let bytes = v.inner.as_bytes();
275        Tail.serialize_into(&bytes, obuf);
276    }
277}
278
279impl<'i> Prepare<Ia5String<'i>> for super::Ia5StringFmt {
280    fn prepare(&self, v: &Ia5String<'i>) -> Result<usize, PreSerializeError> {
281        broadcast use vstd::utf8::encode_utf8_valid_utf8;
282
283        proof {
284            use_type_invariant(v);
285        }
286        let bytes = v.inner.as_bytes();
287        Tail.prepare(&bytes)
288    }
289}
290
291impl<'i> ByteLen<Ia5String<'i>> for super::Ia5StringFmt {
292    fn length(&self, v: &Ia5String<'i>) -> usize {
293        proof {
294            use_type_invariant(v);
295        }
296        let bytes = v.inner.as_bytes();
297        Tail.length(&bytes)
298    }
299}
300
301#[cfg(feature = "alloc")]
302impl<Output: OutputBuf> Serializer<Output, Ia5StringOwned> for super::Ia5StringFmt {
303    fn serialize_into(&self, v: &Ia5StringOwned, obuf: &mut Output) {
304        proof {
305            use_type_invariant(v);
306        }
307        let bytes = v.inner.as_str().as_bytes();
308        Tail.serialize_into(&bytes, obuf);
309    }
310}
311
312#[cfg(feature = "alloc")]
313impl Prepare<Ia5StringOwned> for super::Ia5StringFmt {
314    fn prepare(&self, v: &Ia5StringOwned) -> Result<usize, PreSerializeError> {
315        broadcast use vstd::utf8::encode_utf8_valid_utf8;
316
317        proof {
318            use_type_invariant(v);
319        }
320        let bytes = v.inner.as_str().as_bytes();
321        Tail.prepare(&bytes)
322    }
323}
324
325#[cfg(feature = "alloc")]
326impl ByteLen<Ia5StringOwned> for super::Ia5StringFmt {
327    fn length(&self, v: &Ia5StringOwned) -> usize {
328        proof {
329            use_type_invariant(v);
330        }
331        let bytes = v.inner.as_str().as_bytes();
332        Tail.length(&bytes)
333    }
334}
335
336} // verus!
vest_lib/asn1/ia5string.rs

vest_lib/asn1/
ia5string.rs
