vest_lib/asn1/
teletexstring.rs

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

vest_lib/asn1/
teletexstring.rs
