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

vest_lib/asn1/
ia5string.rs
