vest_lib/asn1/
utf8string.rs

1//! ASN.1 UTF8String borrowed and owned values and contents format.
2use crate::core::exec::input::{InputBuf, InputSlice};
3use crate::core::exec::output::*;
4use crate::core::exec::{
5    parser::{PResult, Parser},
6    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
7    ParseError,
8};
9use crate::{
10    combinators::{mapped::spec::FnSpecMapper, Mapped, Refined, Tail},
11    core::{proof::*, spec::*},
12};
13#[cfg(feature = "alloc")]
14use alloc::{string::String, vec::Vec};
15use vstd::prelude::*;
16use vstd::string::StringSliceAdditionalSpecFns;
17use OutputBuf;
18
19verus! {
20
21pub type Utf8String<'a> = &'a str;
22
23/// Owned UTF8String value used by formats, such as constructed BER strings, whose
24/// contents cannot borrow one contiguous range of the input.
25#[cfg(feature = "alloc")]
26pub type Utf8StringOwned = String;
27
28/// Tests a Unicode scalar value without converting it to a `char`.
29#[verifier::allow_in_spec]
30pub(crate) fn is_unicode_scalar(value: u32) -> bool
31    returns
32        vstd::utf8::is_scalar(value),
33{
34    value <= 0x10ffff && !(0xd800 <= value && value <= 0xdfff)
35}
36
37#[verifier::external_body]
38pub fn is_valid_utf8(bytes: &[u8]) -> (res: bool)
39    ensures
40        res == vstd::utf8::valid_utf8(bytes.deep_view()),
41{
42    str::from_utf8(bytes).is_ok()
43}
44
45pub fn utf8_from_bytes_unchecked<'a>(bytes: &'a [u8]) -> (res: &'a str)
46    requires
47        vstd::utf8::valid_utf8(bytes.deep_view()),
48    ensures
49        res.spec_bytes() == bytes.deep_view(),
50        res.deep_view() == vstd::utf8::decode_utf8(bytes.deep_view()),
51{
52    broadcast use vstd::utf8::decode_utf8_encode_utf8;
53    broadcast use vstd::utf8::encode_utf8_decode_utf8;
54
55    assert(bytes@ == bytes.deep_view());
56    // SAFETY: Verus ensures that the bytes are valid UTF-8 :p
57    unsafe { str::from_utf8_unchecked(bytes) }
58}
59
60/// Specification for converting an owned UTF-8 byte buffer into a `String` without copying or
61/// reallocating it.
62#[cfg(feature = "alloc")]
63pub assume_specification[ String::from_utf8_unchecked ](bytes: Vec<u8>) -> (res: String)
64    requires
65        vstd::utf8::valid_utf8(bytes.deep_view()),
66    ensures
67        res.deep_view() == vstd::utf8::decode_utf8(bytes.deep_view()),
68;
69
70type Utf8StringFmt = Mapped<Refined<Tail, PredFnSpec<Seq<u8>>>, FnSpecMapper<Seq<u8>, Seq<char>>>;
71
72pub open spec fn utf8string_fmt() -> Utf8StringFmt {
73    Mapped {
74        inner: Refined(Tail, |bytes: Seq<u8>| vstd::utf8::valid_utf8(bytes)),
75        mapper: (
76            |bytes: Seq<u8>| vstd::utf8::decode_utf8(bytes),
77            |chars: Seq<char>| vstd::utf8::encode_utf8(chars),
78        ),
79    }
80}
81
82mod derived_specs {
83    use super::*;
84
85    impl SpecParser for super::super::Utf8StringFmt {
86        type PVal = Seq<char>;
87
88        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
89            utf8string_fmt().spec_parse(ibuf)
90        }
91    }
92
93    impl Consistency for super::super::Utf8StringFmt {
94        type Val = Seq<char>;
95
96        open spec fn consistent(&self, v: Self::Val) -> bool {
97            utf8string_fmt().consistent(v)
98        }
99    }
100
101    impl SpecSerializerDps for super::super::Utf8StringFmt {
102        type SValue = Seq<char>;
103
104        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
105            utf8string_fmt().spec_serialize_dps(v, obuf)
106        }
107    }
108
109    impl SpecSerializer for super::super::Utf8StringFmt {
110        type SVal = Seq<char>;
111
112        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
113            utf8string_fmt().spec_serialize(v)
114        }
115    }
116
117    impl SpecByteLen for super::super::Utf8StringFmt {
118        type T = Seq<char>;
119
120        open spec fn byte_len(&self, v: Self::T) -> nat {
121            utf8string_fmt().byte_len(v)
122        }
123    }
124
125}
126
127mod derived_proofs {
128    use super::*;
129
130    impl SafeParser for super::super::Utf8StringFmt {
131        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
132            utf8string_fmt().lemma_parse_safe(ibuf);
133        }
134    }
135
136    impl Productive for super::super::Utf8StringFmt {
137        open spec fn productive_inv(&self) -> bool {
138            false
139        }
140
141        proof fn lemma_productive(&self, s: Seq<u8>) {
142        }
143    }
144
145    impl SoundParser for super::super::Utf8StringFmt {
146        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
147            broadcast use vstd::utf8::decode_utf8_encode_utf8;
148
149            utf8string_fmt().lemma_parse_sound_consumption(ibuf);
150        }
151
152        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
153            broadcast use vstd::utf8::decode_utf8_encode_utf8;
154
155            utf8string_fmt().lemma_parse_sound_value(ibuf);
156        }
157    }
158
159    impl GoodSerializer for super::super::Utf8StringFmt {
160        proof fn lemma_serialize_len(&self, v: Self::SVal) {
161            utf8string_fmt().lemma_serialize_len(v);
162        }
163    }
164
165    impl SPRoundTripDps for super::super::Utf8StringFmt {
166        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
167            broadcast use vstd::utf8::encode_utf8_decode_utf8;
168
169            utf8string_fmt().theorem_serialize_dps_parse_roundtrip(v, obuf);
170        }
171    }
172
173    impl NonMalleable for super::super::Utf8StringFmt {
174        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
175            broadcast use vstd::utf8::decode_utf8_encode_utf8;
176
177            utf8string_fmt().lemma_parse_non_malleable(buf1, buf2);
178        }
179    }
180
181    impl EquivSerializers for super::super::Utf8StringFmt {
182        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
183            utf8string_fmt().lemma_serialize_equiv_on_empty(v);
184        }
185    }
186
187}
188
189impl<'i> Parser<&'i [u8]> for super::Utf8StringFmt {
190    type PT = &'i str;
191
192    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
193        let (n, bytes) = Tail.parse(ibuf)?;
194        if is_valid_utf8(bytes) {
195            let inner = utf8_from_bytes_unchecked(bytes);
196            Ok((n, inner))
197        } else {
198            Err(ParseError::custom("Invalid UTF-8"))
199        }
200    }
201}
202
203impl<Output: OutputBuf, 'i> Serializer<Output, &'i str> for super::Utf8StringFmt {
204    fn serialize_into(&self, v: &&'i str, obuf: &mut Output) {
205        let bytes = v.as_bytes();
206        Tail.serialize_into(&bytes, obuf);
207    }
208}
209
210impl<'i> Prepare<&'i str> for super::Utf8StringFmt {
211    fn prepare(&self, v: &&'i str) -> Result<usize, PreSerializeError> {
212        broadcast use vstd::utf8::encode_utf8_valid_utf8;
213
214        let bytes = v.as_bytes();
215        Tail.prepare(&bytes)
216    }
217}
218
219impl<'i> ByteLen<&'i str> for super::Utf8StringFmt {
220    fn length(&self, v: &&'i str) -> usize {
221        let bytes = v.as_bytes();
222        Tail.length(&bytes)
223    }
224}
225
226#[cfg(feature = "alloc")]
227impl<Output: OutputBuf> Serializer<Output, Utf8StringOwned> for super::Utf8StringFmt {
228    fn serialize_into(&self, v: &Utf8StringOwned, obuf: &mut Output) {
229        let bytes = v.as_str().as_bytes();
230        Tail.serialize_into(&bytes, obuf);
231    }
232}
233
234#[cfg(feature = "alloc")]
235impl Prepare<Utf8StringOwned> for super::Utf8StringFmt {
236    fn prepare(&self, v: &Utf8StringOwned) -> Result<usize, PreSerializeError> {
237        broadcast use vstd::utf8::encode_utf8_valid_utf8;
238
239        let bytes = v.as_str().as_bytes();
240        Tail.prepare(&bytes)
241    }
242}
243
244#[cfg(feature = "alloc")]
245impl ByteLen<Utf8StringOwned> for super::Utf8StringFmt {
246    fn length(&self, v: &Utf8StringOwned) -> usize {
247        let bytes = v.as_str().as_bytes();
248        Tail.length(&bytes)
249    }
250}
251
252} // verus!
vest_lib/asn1/utf8string.rs

vest_lib/asn1/
utf8string.rs
