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

vest_lib/asn1/
universalstring.rs
