vest_lib/asn1/
bmpstring.rs

1//! ASN.1 BMPString values and UCS-2 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::{
11        mapped::spec::FnSpecMapper,
12        uints::{
13            exec::{u16_from_be_bytes, u16_to_be_bytes},
14            spec::*,
15        },
16        Mapped, Refined, Tail,
17    },
18    core::{proof::*, spec::*},
19};
20#[cfg(feature = "alloc")]
21use alloc::string::String;
22use vstd::prelude::*;
23#[cfg(verus_only)]
24use vstd::std_specs::iter::IteratorSpec;
25use vstd::string::StrSliceExecFns;
26use OutputBuf;
27
28verus! {
29
30/// Semantic BMPString value. Parsing necessarily owns the result because
31/// BMPString wire octets are not UTF-8 and constructed BER values may span
32/// discontiguous input segments.
33#[cfg(feature = "alloc")]
34pub struct BmpString {
35    inner: String,
36}
37
38#[verifier::ext_equal]
39pub struct BmpStringSpec {
40    pub inner: Seq<char>,
41}
42
43#[cfg(feature = "alloc")]
44impl DeepView for BmpString {
45    type V = BmpStringSpec;
46
47    closed spec fn deep_view(&self) -> Self::V {
48        BmpStringSpec { inner: self.inner.deep_view() }
49    }
50}
51
52pub open spec fn is_bmp_char(c: char) -> bool {
53    (c as u32) <= 0xffff
54}
55
56pub open spec fn is_valid_bmp_chars(chars: Seq<char>) -> bool {
57    forall|i: int| 0 <= i < chars.len() ==> is_bmp_char(#[trigger] chars[i])
58}
59
60impl BmpStringSpec {
61    pub open spec fn wf(&self) -> bool {
62        is_valid_bmp_chars(self.inner)
63    }
64}
65
66#[cfg(feature = "alloc")]
67impl BmpString {
68    #[verifier::type_invariant]
69    spec fn wf(&self) -> bool {
70        self.deep_view().wf()
71    }
72
73    pub fn new(inner: String) -> (res: Self)
74        requires
75            is_valid_bmp_chars(inner.deep_view()),
76        ensures
77            res.deep_view() == (BmpStringSpec { inner: inner.deep_view() }),
78    {
79        Self { inner }
80    }
81
82    pub fn inner(&self) -> (res: &str)
83        ensures
84            res.deep_view() == self.deep_view().inner,
85    {
86        self.inner.as_str()
87    }
88}
89
90pub open spec fn bmp_code_unit(bytes: Seq<u8>, i: int) -> u32
91    recommends
92        0 <= 2 * i,
93        2 * i + 1 < bytes.len(),
94{
95    u16_be_from_bytes([bytes[2 * i], bytes[2 * i + 1]]) as u32
96}
97
98/// The well-formedness condition for the BMP/UCS-2 contents octets.
99pub open spec fn is_valid_bmp_string(bytes: Seq<u8>) -> bool {
100    &&& bytes.len() % 2 == 0
101    &&& forall|i: int|
102        0 <= i < bytes.len() / 2 ==> vstd::utf8::is_scalar(#[trigger] bmp_code_unit(bytes, i))
103}
104
105/// Decode two-octet big-endian BMP/UCS-2 code units.
106pub open spec fn decode_bmp_string(bytes: Seq<u8>) -> Seq<char> {
107    Seq::new(bytes.len() / 2, |i: int| bmp_code_unit(bytes, i) as char)
108}
109
110/// Encode Unicode BMP scalars as two-octet big-endian BMP/UCS-2 code units.
111pub open spec fn encode_bmp_string(chars: Seq<char>) -> Seq<u8> {
112    Seq::new(chars.len() * 2, |i: int| u16_be_to_bytes(chars[i / 2] as u16)[i % 2])
113}
114
115proof fn lemma_scalar_char_cast(u: u32)
116    requires
117        vstd::utf8::is_scalar(u),
118    ensures
119        (u as char) as u32 == u,
120{
121}
122
123proof fn lemma_bmp_char_u16_cast(c: char)
124    requires
125        is_bmp_char(c),
126    ensures
127        (c as u16) as u32 == c as u32,
128{
129}
130
131proof fn lemma_encoded_bmp_code_unit(chars: Seq<char>, i: int)
132    requires
133        is_valid_bmp_chars(chars),
134        0 <= i < chars.len(),
135    ensures
136        bmp_code_unit(encode_bmp_string(chars), i) == chars[i] as u32,
137{
138    let c = chars[i];
139    let pair = u16_be_to_bytes(c as u16);
140    lemma_bmp_char_u16_cast(c);
141    lemma_u16_be_value_roundtrip(c as u16);
142    assert(encode_bmp_string(chars)[2 * i] == pair[0]);
143    assert(encode_bmp_string(chars)[2 * i + 1] == pair[1]);
144}
145
146proof fn lemma_decoded_bmp_code_unit(bytes: Seq<u8>, i: int)
147    requires
148        is_valid_bmp_string(bytes),
149        0 <= i < bytes.len() / 2,
150    ensures
151        is_bmp_char(decode_bmp_string(bytes)[i]),
152        u16_be_to_bytes(decode_bmp_string(bytes)[i] as u16) == [bytes[2 * i], bytes[2 * i + 1]],
153{
154    let unit = bmp_code_unit(bytes, i);
155    let pair = [bytes[2 * i], bytes[2 * i + 1]];
156    let code = u16_be_from_bytes(pair);
157    assert(vstd::utf8::is_scalar(unit));
158    lemma_scalar_char_cast(unit);
159    lemma_u16_be_bytes_roundtrip(pair);
160    lemma_bmp_char_u16_cast(unit as char);
161}
162
163pub proof fn lemma_encode_bmp_string_valid(chars: Seq<char>)
164    requires
165        is_valid_bmp_chars(chars),
166    ensures
167        is_valid_bmp_string(encode_bmp_string(chars)),
168{
169    let bytes = encode_bmp_string(chars);
170    assert(bytes.len() % 2 == 0);
171    assert forall|i: int| 0 <= i < bytes.len() / 2 implies vstd::utf8::is_scalar(
172        #[trigger] bmp_code_unit(bytes, i),
173    ) by {
174        let c = chars[i];
175        vstd::utf8::char_is_scalar(c);
176        lemma_encoded_bmp_code_unit(chars, i);
177    }
178}
179
180pub proof fn lemma_decode_encode_bmp_string(chars: Seq<char>)
181    requires
182        is_valid_bmp_chars(chars),
183    ensures
184        decode_bmp_string(encode_bmp_string(chars)) == chars,
185{
186    let bytes = encode_bmp_string(chars);
187    assert(decode_bmp_string(bytes).len() == chars.len());
188    assert forall|i: int| 0 <= i < chars.len() implies #[trigger] decode_bmp_string(bytes)[i]
189        == chars[i] by {
190        lemma_encoded_bmp_code_unit(chars, i);
191        vstd::utf8::char_u32_cast(chars[i], bmp_code_unit(bytes, i));
192    }
193}
194
195pub proof fn lemma_encode_decode_bmp_string(bytes: Seq<u8>)
196    requires
197        is_valid_bmp_string(bytes),
198    ensures
199        encode_bmp_string(decode_bmp_string(bytes)) == bytes,
200{
201    let chars = decode_bmp_string(bytes);
202    assert(encode_bmp_string(chars).len() == bytes.len());
203    assert forall|i: int| 0 <= i < bytes.len() implies #[trigger] encode_bmp_string(chars)[i]
204        == bytes[i] by {
205        let unit_index = i / 2;
206        lemma_decoded_bmp_code_unit(bytes, unit_index);
207    }
208}
209
210pub proof fn lemma_decoded_bmp_string_valid(bytes: Seq<u8>)
211    requires
212        is_valid_bmp_string(bytes),
213    ensures
214        is_valid_bmp_chars(decode_bmp_string(bytes)),
215{
216    assert forall|i: int| 0 <= i < decode_bmp_string(bytes).len() implies is_bmp_char(
217        #[trigger] decode_bmp_string(bytes)[i],
218    ) by {
219        lemma_decoded_bmp_code_unit(bytes, i);
220    }
221}
222
223type BmpStringInnerFmt = Mapped<
224    Refined<Tail, PredFnSpec<Seq<u8>>>,
225    FnSpecMapper<Seq<u8>, BmpStringSpec>,
226>;
227
228pub open spec fn bmpstring_fmt() -> BmpStringInnerFmt {
229    Mapped {
230        inner: Refined(Tail, |bytes: Seq<u8>| is_valid_bmp_string(bytes)),
231        mapper: (
232            |bytes: Seq<u8>| BmpStringSpec { inner: decode_bmp_string(bytes) },
233            |s: BmpStringSpec| encode_bmp_string(s.inner),
234        ),
235    }
236}
237
238proof fn lemma_bmpstring_fmt_sound_nonmal_inv()
239    ensures
240        bmpstring_fmt().sound_inv(),
241        bmpstring_fmt().nonmal_inv(),
242{
243    assert forall|bytes: Seq<u8>| #[trigger] is_valid_bmp_string(bytes) implies encode_bmp_string(
244        decode_bmp_string(bytes),
245    ) == bytes by {
246        lemma_encode_decode_bmp_string(bytes);
247    }
248}
249
250mod derived_specs {
251    use super::*;
252
253    impl SpecParser for super::super::BmpStringFmt {
254        type PVal = BmpStringSpec;
255
256        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
257            bmpstring_fmt().spec_parse(ibuf)
258        }
259    }
260
261    impl Consistency for super::super::BmpStringFmt {
262        type Val = BmpStringSpec;
263
264        open spec fn consistent(&self, v: Self::Val) -> bool {
265            bmpstring_fmt().consistent(v) && v.wf()
266        }
267    }
268
269    impl SpecSerializerDps for super::super::BmpStringFmt {
270        type SValue = BmpStringSpec;
271
272        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
273            bmpstring_fmt().spec_serialize_dps(v, obuf)
274        }
275    }
276
277    impl SpecSerializer for super::super::BmpStringFmt {
278        type SVal = BmpStringSpec;
279
280        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
281            bmpstring_fmt().spec_serialize(v)
282        }
283    }
284
285    impl SpecByteLen for super::super::BmpStringFmt {
286        type T = BmpStringSpec;
287
288        open spec fn byte_len(&self, v: Self::T) -> nat {
289            bmpstring_fmt().byte_len(v)
290        }
291    }
292
293}
294
295pub(crate) proof fn lemma_bmp_string_fmt_serialization(value: BmpStringSpec)
296    ensures
297        super::BmpStringFmt.spec_serialize(value) == encode_bmp_string(value.inner),
298        super::BmpStringFmt.byte_len(value) == value.inner.len() * 2,
299{
300}
301
302mod derived_proofs {
303    use super::*;
304
305    impl SafeParser for super::super::BmpStringFmt {
306        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
307            bmpstring_fmt().lemma_parse_safe(ibuf);
308        }
309    }
310
311    impl Productive for super::super::BmpStringFmt {
312        open spec fn productive_inv(&self) -> bool {
313            false
314        }
315
316        proof fn lemma_productive(&self, _s: Seq<u8>) {
317        }
318    }
319
320    impl SoundParser for super::super::BmpStringFmt {
321        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
322            lemma_bmpstring_fmt_sound_nonmal_inv();
323            bmpstring_fmt().lemma_parse_sound_consumption(ibuf);
324        }
325
326        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
327            lemma_bmpstring_fmt_sound_nonmal_inv();
328            bmpstring_fmt().lemma_parse_sound_value(ibuf);
329        }
330    }
331
332    impl GoodSerializer for super::super::BmpStringFmt {
333        proof fn lemma_serialize_len(&self, v: Self::SVal) {
334            bmpstring_fmt().lemma_serialize_len(v);
335        }
336    }
337
338    impl SPRoundTripDps for super::super::BmpStringFmt {
339        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
340            lemma_encode_bmp_string_valid(v.inner);
341            lemma_decode_encode_bmp_string(v.inner);
342            let bytes = encode_bmp_string(v.inner);
343            let inner = Refined(Tail, |bytes: Seq<u8>| is_valid_bmp_string(bytes));
344            inner.theorem_serialize_dps_parse_roundtrip(bytes, obuf);
345        }
346    }
347
348    impl NonMalleable for super::super::BmpStringFmt {
349        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
350            lemma_bmpstring_fmt_sound_nonmal_inv();
351            bmpstring_fmt().lemma_parse_non_malleable(buf1, buf2);
352        }
353    }
354
355    impl EquivSerializers for super::super::BmpStringFmt {
356        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
357            bmpstring_fmt().lemma_serialize_equiv_on_empty(v);
358        }
359    }
360
361}
362
363/// Check that a byte slice is a valid BMPString without allocation.
364pub fn check_valid_bmp_string(bytes: &[u8]) -> (res: bool)
365    ensures
366        res == is_valid_bmp_string(bytes.deep_view()),
367{
368    if bytes.len() % 2 != 0 {
369        return false;
370    }
371    let mut iter = 0..bytes.len() / 2;
372    let ghost indices = iter.remaining();
373    let valid = iter.all(
374        |i: usize| -> (valid: bool)
375            requires
376                i < bytes@.len() / 2,
377            ensures
378                valid == vstd::utf8::is_scalar(bmp_code_unit(bytes@, i as int)),
379            {
380                let unit = u16_from_be_bytes([bytes[2 * i], bytes[2 * i + 1]]) as u32;
381                super::utf8string::is_unicode_scalar(unit)
382            },
383    );
384    assert(bytes@ == bytes.deep_view());
385    // The range's elements are exactly the code-unit indices, for either `all` outcome.
386    assert forall|i: int| 0 <= i < indices.len() implies vstd::utf8::is_scalar(
387        bmp_code_unit(bytes@, indices[i] as int),
388    ) == vstd::utf8::is_scalar(#[trigger] bmp_code_unit(bytes@, i)) by {}
389
390    valid
391}
392
393/// Decode a byte slice into a String, assuming it contains a valid BMPString.
394/// TODO: Verify this function while keeping it efficient and idiomatic.
395#[cfg(feature = "alloc")]
396#[verifier::external_body]
397fn decode_bmp_string_owned(bytes: &[u8]) -> (res: String)
398    requires
399        is_valid_bmp_string(bytes.deep_view()),
400    ensures
401        res.deep_view() == decode_bmp_string(bytes.deep_view()),
402{
403    // SAFETY: `is_valid_bmp_string` guarantees that all code units are valid BMP scalars, which are valid Unicode code points, so `char::from_u32_unchecked` is safe to use here.
404    bytes.chunks_exact(2).map(
405        |pair| unsafe { char::from_u32_unchecked(u16::from_be_bytes([pair[0], pair[1]]) as u32) },
406    ).collect()
407}
408
409#[cfg(feature = "alloc")]
410impl<'i> Parser<&'i [u8]> for super::BmpStringFmt {
411    type PT = BmpString;
412
413    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
414        let (n, bytes) = Tail.parse(ibuf)?;
415        if !check_valid_bmp_string(bytes) {
416            Err(ParseError::custom("Invalid BMPString"))
417        } else {
418            let inner = decode_bmp_string_owned(bytes);
419            Ok((n, BmpString::new(inner)))
420        }
421    }
422}
423
424#[cfg(feature = "alloc")]
425impl<Output: OutputBuf> Serializer<Output, BmpString> for super::BmpStringFmt {
426    #[verifier::loop_isolation(false)]
427    fn serialize_into(&self, v: &BmpString, obuf: &mut Output) {
428        broadcast use crate::core::exec::output::outbuf_lemmas;
429
430        proof {
431            use_type_invariant(v);
432            lemma_encode_bmp_string_valid(v.deep_view().inner);
433        }
434        let value = v.inner.as_str();
435
436        let ghost initial = obuf@;
437        let ghost len = value.deep_view().len();
438        for c in iter: value.chars()
439            invariant
440                obuf@ == initial + encode_bmp_string(value.deep_view()[0..iter.index()]),
441                forall|n| old(obuf).fits(2 * iter.index() as nat + n) <==> obuf.fits(n),
442                old(obuf).same_destination(obuf),
443        {
444            proof {
445                old(obuf).lemma_fits_mono(2 * iter.index() as nat + 2, 2 * len as nat);
446            }
447            let pair = u16_to_be_bytes(c as u16);
448            obuf.write_bytes(&pair);
449        }
450    }
451}
452
453#[cfg(feature = "alloc")]
454impl Prepare<BmpString> for super::BmpStringFmt {
455    fn prepare(&self, v: &BmpString) -> Result<usize, PreSerializeError> {
456        proof {
457            use_type_invariant(v);
458            lemma_encode_bmp_string_valid(v.deep_view().inner);
459        }
460        v.inner.as_str().unicode_len().checked_mul(2).ok_or(PreSerializeError::length_too_large())
461    }
462}
463
464#[cfg(feature = "alloc")]
465impl ByteLen<BmpString> for super::BmpStringFmt {
466    fn length(&self, v: &BmpString) -> usize {
467        proof {
468            use_type_invariant(v);
469        }
470        v.inner.as_str().unicode_len() * 2
471    }
472}
473
474} // verus!
vest_lib/asn1/bmpstring.rs

vest_lib/asn1/
bmpstring.rs
