vest_lib/asn1/
universalstring.rs

1//! ASN.1 UniversalString contents.
2//!
3//! UniversalString represents ISO/IEC 10646 scalar values as four-octet,
4//! big-endian code points. Its semantic Rust value is an owned `String`
5//! because the wire representation is not UTF-8.
6use crate::core::exec::input::{InputBuf, InputSlice};
7use crate::core::exec::output::*;
8use crate::core::exec::{
9    parser::{PResult, Parser},
10    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
11    ParseError,
12};
13use crate::{
14    combinators::{
15        mapped::spec::FnSpecMapper,
16        uints::{exec::u32_to_be_bytes, spec::*},
17        Mapped, Refined, Tail,
18    },
19    core::{proof::*, spec::*},
20};
21#[cfg(feature = "alloc")]
22use alloc::string::String;
23use vstd::prelude::*;
24#[cfg(feature = "alloc")]
25use vstd::string::StrSliceExecFns;
26use OutputBuf;
27
28verus! {
29
30#[cfg(feature = "alloc")]
31pub type UniversalString = String;
32
33pub type UniversalStringSpec = Seq<char>;
34
35pub open spec fn universal_code_point(bytes: Seq<u8>, i: int) -> u32
36    recommends
37        0 <= 4 * i,
38        4 * i + 3 < bytes.len(),
39{
40    u32_be_from_bytes([bytes[4 * i], bytes[4 * i + 1], bytes[4 * i + 2], bytes[4 * i + 3]])
41}
42
43/// The well-formedness condition for UniversalString contents octets.
44pub open spec fn is_valid_universal_string(bytes: Seq<u8>) -> bool {
45    &&& bytes.len() % 4 == 0
46    &&& forall|i: int|
47        0 <= i < bytes.len() / 4 ==> vstd::utf8::is_scalar(
48            #[trigger] universal_code_point(bytes, i),
49        )
50}
51
52/// Decode four-octet big-endian ISO/IEC 10646 scalar values.
53pub open spec fn decode_universal_string(bytes: Seq<u8>) -> Seq<char> {
54    Seq::new(bytes.len() / 4, |i: int| universal_code_point(bytes, i) as char)
55}
56
57/// Encode Unicode scalar values as four-octet big-endian code points.
58pub open spec fn encode_universal_string(chars: Seq<char>) -> Seq<u8> {
59    Seq::new(chars.len() * 4, |i: int| u32_be_to_bytes(chars[i / 4] as u32)[i % 4])
60}
61
62proof fn lemma_scalar_char_cast(u: u32)
63    requires
64        vstd::utf8::is_scalar(u),
65    ensures
66        (u as char) as u32 == u,
67{
68}
69
70proof fn lemma_encoded_universal_code_point(chars: Seq<char>, i: int)
71    requires
72        0 <= i < chars.len(),
73    ensures
74        universal_code_point(encode_universal_string(chars), i) == chars[i] as u32,
75{
76    let c = chars[i];
77    let word = u32_be_to_bytes(c as u32);
78    lemma_u32_be_value_roundtrip(c as u32);
79    assert(encode_universal_string(chars)[4 * i] == word[0]);
80    assert(encode_universal_string(chars)[4 * i + 1] == word[1]);
81    assert(encode_universal_string(chars)[4 * i + 2] == word[2]);
82    assert(encode_universal_string(chars)[4 * i + 3] == word[3]);
83}
84
85proof fn lemma_decoded_universal_code_point(bytes: Seq<u8>, i: int)
86    requires
87        is_valid_universal_string(bytes),
88        0 <= i < bytes.len() / 4,
89    ensures
90        u32_be_to_bytes(decode_universal_string(bytes)[i] as u32) == [
91            bytes[4 * i],
92            bytes[4 * i + 1],
93            bytes[4 * i + 2],
94            bytes[4 * i + 3],
95        ],
96{
97    let word = [bytes[4 * i], bytes[4 * i + 1], bytes[4 * i + 2], bytes[4 * i + 3]];
98    let code = u32_be_from_bytes(word);
99    assert(code == universal_code_point(bytes, i));
100    assert(vstd::utf8::is_scalar(code));
101    lemma_scalar_char_cast(code);
102    lemma_u32_be_bytes_roundtrip(word);
103}
104
105pub proof fn lemma_encode_universal_string_valid(chars: Seq<char>)
106    ensures
107        is_valid_universal_string(encode_universal_string(chars)),
108{
109    let bytes = encode_universal_string(chars);
110    assert(bytes.len() % 4 == 0);
111    assert forall|i: int| 0 <= i < bytes.len() / 4 implies vstd::utf8::is_scalar(
112        #[trigger] universal_code_point(bytes, i),
113    ) by {
114        vstd::utf8::char_is_scalar(chars[i]);
115        lemma_encoded_universal_code_point(chars, i);
116    }
117}
118
119pub proof fn lemma_decode_encode_universal_string(chars: Seq<char>)
120    ensures
121        decode_universal_string(encode_universal_string(chars)) == chars,
122{
123    let bytes = encode_universal_string(chars);
124    assert(decode_universal_string(bytes).len() == chars.len());
125    assert forall|i: int| 0 <= i < chars.len() implies #[trigger] decode_universal_string(bytes)[i]
126        == chars[i] by {
127        lemma_encoded_universal_code_point(chars, i);
128        vstd::utf8::char_u32_cast(chars[i], universal_code_point(bytes, i));
129    }
130}
131
132pub proof fn lemma_encode_decode_universal_string(bytes: Seq<u8>)
133    requires
134        is_valid_universal_string(bytes),
135    ensures
136        encode_universal_string(decode_universal_string(bytes)) == bytes,
137{
138    let chars = decode_universal_string(bytes);
139    assert(encode_universal_string(chars).len() == bytes.len());
140    assert forall|i: int| 0 <= i < bytes.len() implies #[trigger] encode_universal_string(chars)[i]
141        == bytes[i] by {
142        lemma_decoded_universal_code_point(bytes, i / 4);
143    }
144}
145
146type UniversalStringInnerFmt = Mapped<
147    Refined<Tail, PredFnSpec<Seq<u8>>>,
148    FnSpecMapper<Seq<u8>, Seq<char>>,
149>;
150
151pub open spec fn universalstring_fmt() -> UniversalStringInnerFmt {
152    Mapped {
153        inner: Refined(Tail, |bytes: Seq<u8>| is_valid_universal_string(bytes)),
154        mapper: (
155            |bytes: Seq<u8>| decode_universal_string(bytes),
156            |chars: Seq<char>| encode_universal_string(chars),
157        ),
158    }
159}
160
161proof fn lemma_universalstring_fmt_sound_nonmal_inv()
162    ensures
163        universalstring_fmt().sound_inv(),
164        universalstring_fmt().nonmal_inv(),
165{
166    assert forall|bytes: Seq<u8>| #[trigger]
167        is_valid_universal_string(bytes) implies encode_universal_string(
168        decode_universal_string(bytes),
169    ) == bytes by {
170        lemma_encode_decode_universal_string(bytes);
171    }
172}
173
174mod derived_specs {
175    use super::*;
176
177    impl SpecParser for super::super::UniversalStringFmt {
178        type PVal = Seq<char>;
179
180        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
181            universalstring_fmt().spec_parse(ibuf)
182        }
183    }
184
185    impl Consistency for super::super::UniversalStringFmt {
186        type Val = Seq<char>;
187
188        open spec fn consistent(&self, value: Self::Val) -> bool {
189            universalstring_fmt().consistent(value)
190        }
191    }
192
193    impl SpecSerializerDps for super::super::UniversalStringFmt {
194        type SValue = Seq<char>;
195
196        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
197            universalstring_fmt().spec_serialize_dps(value, obuf)
198        }
199    }
200
201    impl SpecSerializer for super::super::UniversalStringFmt {
202        type SVal = Seq<char>;
203
204        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
205            universalstring_fmt().spec_serialize(value)
206        }
207    }
208
209    impl SpecByteLen for super::super::UniversalStringFmt {
210        type T = Seq<char>;
211
212        open spec fn byte_len(&self, value: Self::T) -> nat {
213            universalstring_fmt().byte_len(value)
214        }
215    }
216
217}
218
219pub(crate) proof fn lemma_universal_string_fmt_serialization(value: Seq<char>)
220    ensures
221        super::UniversalStringFmt.spec_serialize(value) == encode_universal_string(value),
222        super::UniversalStringFmt.byte_len(value) == value.len() * 4,
223{
224}
225
226mod derived_proofs {
227    use super::*;
228
229    impl SafeParser for super::super::UniversalStringFmt {
230        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
231            universalstring_fmt().lemma_parse_safe(ibuf);
232        }
233    }
234
235    impl Productive for super::super::UniversalStringFmt {
236        open spec fn productive_inv(&self) -> bool {
237            false
238        }
239
240        proof fn lemma_productive(&self, _input: Seq<u8>) {
241        }
242    }
243
244    impl SoundParser for super::super::UniversalStringFmt {
245        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
246            lemma_universalstring_fmt_sound_nonmal_inv();
247            universalstring_fmt().lemma_parse_sound_consumption(ibuf);
248        }
249
250        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
251            lemma_universalstring_fmt_sound_nonmal_inv();
252            universalstring_fmt().lemma_parse_sound_value(ibuf);
253        }
254    }
255
256    impl GoodSerializer for super::super::UniversalStringFmt {
257        proof fn lemma_serialize_len(&self, value: Self::SVal) {
258            universalstring_fmt().lemma_serialize_len(value);
259        }
260    }
261
262    impl SPRoundTripDps for super::super::UniversalStringFmt {
263        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
264            lemma_encode_universal_string_valid(value);
265            lemma_decode_encode_universal_string(value);
266            let bytes = encode_universal_string(value);
267            let inner = Refined(Tail, |bytes: Seq<u8>| is_valid_universal_string(bytes));
268            inner.theorem_serialize_dps_parse_roundtrip(bytes, obuf);
269        }
270    }
271
272    impl NonMalleable for super::super::UniversalStringFmt {
273        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
274            lemma_universalstring_fmt_sound_nonmal_inv();
275            universalstring_fmt().lemma_parse_non_malleable(buf1, buf2);
276        }
277    }
278
279    impl EquivSerializers for super::super::UniversalStringFmt {
280        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
281            universalstring_fmt().lemma_serialize_equiv_on_empty(value);
282        }
283    }
284
285}
286
287/// Check a UniversalString contents slice without allocation.
288#[verifier::external_body]
289pub fn check_valid_universal_string(bytes: &[u8]) -> (valid: bool)
290    ensures
291        valid == is_valid_universal_string(bytes.deep_view()),
292{
293    if bytes.len() % 4 != 0 {
294        return false;
295    }
296    bytes.chunks_exact(4).map(|word| u32::from_be_bytes([word[0], word[1], word[2], word[3]])).all(
297        |code| char::from_u32(code).is_some(),
298    )
299}
300
301#[cfg(feature = "alloc")]
302#[verifier::external_body]
303pub(crate) fn decode_universal_string_owned(bytes: &[u8]) -> (value: String)
304    requires
305        is_valid_universal_string(bytes.deep_view()),
306    ensures
307        value.deep_view() == decode_universal_string(bytes.deep_view()),
308{
309    bytes.chunks_exact(4).map(
310        |word|
311            unsafe {
312                char::from_u32_unchecked(u32::from_be_bytes([word[0], word[1], word[2], word[3]]))
313            },
314    ).collect()
315}
316
317#[cfg(feature = "alloc")]
318impl<'i> Parser<&'i [u8]> for super::UniversalStringFmt {
319    type PT = UniversalString;
320
321    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
322        let (n, bytes) = Tail.parse(ibuf)?;
323        if !check_valid_universal_string(bytes) {
324            Err(ParseError::custom("Invalid UniversalString"))
325        } else {
326            Ok((n, decode_universal_string_owned(bytes)))
327        }
328    }
329}
330
331#[cfg(feature = "alloc")]
332impl<Output: OutputBuf> Serializer<Output, UniversalString> for super::UniversalStringFmt {
333    #[verifier::loop_isolation(false)]
334    fn serialize_into(&self, value: &UniversalString, obuf: &mut Output) {
335        broadcast use crate::core::exec::output::outbuf_lemmas;
336
337        proof {
338            lemma_encode_universal_string_valid(value.deep_view());
339        }
340        let value = value.as_str();
341
342        let ghost initial = obuf@;
343        let len = value.unicode_len();
344        for i in 0..len
345            invariant
346                obuf@ == initial + encode_universal_string(value.deep_view().take(i as int)),
347                forall|n| old(obuf).fits(4 * i as nat + n) <==> obuf.fits(n),
348                old(obuf).same_destination(obuf),
349        {
350            proof {
351                old(obuf).lemma_fits_mono(4 * i as nat + 4, 4 * len as nat);
352            }
353            let c = value.get_char(i);
354            let word = u32_to_be_bytes(c as u32);
355            obuf.write_bytes(&word);
356        }
357    }
358}
359
360#[cfg(feature = "alloc")]
361impl Prepare<UniversalString> for super::UniversalStringFmt {
362    fn prepare(&self, value: &UniversalString) -> Result<usize, PreSerializeError> {
363        proof {
364            lemma_encode_universal_string_valid(value.deep_view());
365        }
366        value.as_str().unicode_len().checked_mul(4).ok_or(PreSerializeError::length_too_large())
367    }
368}
369
370#[cfg(feature = "alloc")]
371impl ByteLen<UniversalString> for super::UniversalStringFmt {
372    fn length(&self, value: &UniversalString) -> usize {
373        value.as_str().unicode_len() * 4
374    }
375}
376
377} // verus!
vest_lib/asn1/universalstring.rs

vest_lib/asn1/
universalstring.rs
