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

vest_lib/asn1/
bmpstring.rs
