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

vest_lib/asn1/
utf8string.rs
