verdict_parser/common/
base64.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Base64 combinator (RFC 4648)
7#[derive(Debug, View)]
8pub struct Base64;
9
10impl Base64 {
11    /// Some() => valid 6 bits
12    /// None => padding byte
13    closed spec fn spec_char_to_bits(b: u8) -> Result<Option<u8>, ()> {
14        let c = b as char;
15        if c >= 'A' && c <= 'Z' {
16            Ok(Some((b - 'A' as u8) as u8))
17        } else if c >= 'a' && c <= 'z' {
18            Ok(Some((b - 'a' as u8 + 26) as u8))
19        } else if c >= '0' && c <= '9' {
20            Ok(Some((b - '0' as u8 + 52) as u8))
21        } else if c == '+' {
22            Ok(Some(62))
23        } else if c == '/' {
24            Ok(Some(63))
25        } else if c == '=' {
26            Ok(None)
27        } else {
28            Err(())
29        }
30    }
31
32    closed spec fn spec_bits_to_char(b: u8) -> u8 {
33        if b < 26 {
34            (b + 'A' as u8) as u8
35        } else if b < 52 {
36            (b - 26 + 'a' as u8) as u8
37        } else if b < 62 {
38            (b - 52 + '0' as u8) as u8
39        } else if b == 62 {
40            '+' as u8
41        } else {
42            '/' as u8
43        }
44    }
45
46    /// Convert a quadruple of 6-bit bytes to a 3-byte sequence
47    closed spec fn spec_decode_6_bit_bytes(b1: u8, b2: u8, b3: u8, b4: u8) -> (u8, u8, u8) {
48        let v1 = (b1 << 2) | (b2 >> 4);
49        let v2 = (b2 << 4) | (b3 >> 2);
50        let v3 = (b3 << 6) | b4;
51        (v1, v2, v3)
52    }
53
54    /// Convert a byte sequence [v1, v2, v3] to a quadruple of 6-bit bytes
55    closed spec fn spec_encode_6_bit_bytes(v1: u8, v2: u8, v3: u8) -> (u8, u8, u8, u8) {
56        let b1 = v1 >> 2;
57        let b2 = ((v1 & 0b11) << 4) | (v2 >> 4);
58        let b3 = ((v2 & 0b1111) << 2) | (v3 >> 6);
59        let b4 = v3 & 0b111111;
60        (b1, b2, b3, b4)
61    }
62
63    closed spec fn spec_parse_helper(s: Seq<u8>) -> Result<(usize, Seq<u8>), ()>
64        decreases s.len()
65    {
66        if s.len() == 0 {
67            Ok((0, seq![]))
68        } else if s.len() < 4 {
69            Err(())
70        } else {
71            let b1 = Self::spec_char_to_bits(s[0]);
72            let b2 = Self::spec_char_to_bits(s[1]);
73            let b3 = Self::spec_char_to_bits(s[2]);
74            let b4 = Self::spec_char_to_bits(s[3]);
75
76            match (b1, b2, b3, b4, Self::spec_parse_helper(s.skip(4))) {
77                (Ok(Some(b1)), Ok(Some(b2)), Ok(Some(b3)), Ok(Some(b4)), Ok((len, rest))) => {
78                    let (v1, v2, v3) = Self::spec_decode_6_bit_bytes(b1, b2, b3, b4);
79                    Ok((s.len() as usize, seq![ v1, v2, v3 ] + rest))
80                }
81
82                // Final 4-byte block with 1 padding `=`
83                (Ok(Some(b1)), Ok(Some(b2)), Ok(Some(b3)), Ok(None), _) => {
84                    let (v1, v2, v3) = Self::spec_decode_6_bit_bytes(b1, b2, b3, 0);
85                    if s.len() == 4 && v3 == 0 {
86                        Ok((4 as usize, seq![ v1, v2 ]))
87                    } else {
88                        Err(())
89                    }
90                }
91
92                // Final 4-byte block with 2 padding `=`s
93                (Ok(Some(b1)), Ok(Some(b2)), Ok(None), Ok(None), _) => {
94                    let (v1, v2, v3) = Self::spec_decode_6_bit_bytes(b1, b2, 0, 0);
95                    if s.len() == 4 && v2 == v3 == 0 {
96                        Ok((4 as usize, seq![ v1 ]))
97                    } else {
98                        Err(())
99                    }
100                }
101
102                _ => Err(()),
103            }
104        }
105    }
106
107    closed spec fn spec_serialize_helper(v: Seq<u8>) -> Result<Seq<u8>, ()>
108        decreases v.len()
109    {
110        if v.len() == 0 {
111            Ok(seq![])
112        } else {
113            let v1 = v[0];
114            let v2 = if v.len() > 1 { v[1] } else { 0 };
115            let v3 = if v.len() > 2 { v[2] } else { 0 };
116
117            let (b1, b2, b3, b4) = Self::spec_encode_6_bit_bytes(v1, v2, v3);
118
119            let b1 = Self::spec_bits_to_char(b1);
120            let b2 = Self::spec_bits_to_char(b2);
121            let b3 = if v.len() > 1 { Self::spec_bits_to_char(b3) } else { '=' as u8 };
122            let b4 = if v.len() > 2 { Self::spec_bits_to_char(b4) } else { '=' as u8 };
123
124            if v.len() <= 3 {
125                Ok(seq![ b1, b2, b3, b4 ])
126            } else {
127                match Self::spec_serialize_helper(v.skip(3)) {
128                    Ok(rest) => Ok(seq![ b1, b2, b3, b4 ] + rest),
129                    Err(()) => Err(())
130                }
131            }
132        }
133    }
134}
135
136impl SpecCombinator for Base64 {
137    type SpecResult = Seq<u8>;
138
139    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
140        Self::spec_parse_helper(s)
141    }
142
143    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
144        match Self::spec_serialize_helper(v) {
145            Ok(s) =>
146                if s.len() <= usize::MAX {
147                    Ok(s)
148                } else {
149                    Err(())
150                }
151
152            Err(()) => Err(())
153        }
154    }
155
156    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
157}
158
159/// Some lemmas
160impl Base64 {
161    broadcast proof fn encode_spec_decode_6_bit_bytes(v1: u8, v2: u8, v3: u8)
162        ensures ({
163            let (b1, b2, b3, b4) = #[trigger] Self::spec_encode_6_bit_bytes(v1, v2, v3);
164            (v1, v2, v3) == Self::spec_decode_6_bit_bytes(b1, b2, b3, b4)
165        })
166    {
167        // Essentially everything unfolded
168        assert(
169            v1 == ((v1 >> 2) << 2) | ((((v1 & 0b11) << 4) | (v2 >> 4)) >> 4) &&
170            v2 == ((((v1 & 0b11) << 4) | (v2 >> 4)) << 4) | ((((v2 & 0b1111) << 2) | (v3 >> 6)) >> 2) &&
171            v3 == ((((v2 & 0b1111) << 2) | (v3 >> 6)) << 6) | (v3 & 0b111111)
172        ) by (bit_vector);
173    }
174
175    broadcast proof fn spec_encode_6_bit_bytes_range(v1: u8, v2: u8, v3: u8)
176        ensures ({
177            let (b1, b2, b3, b4) = #[trigger] Self::spec_encode_6_bit_bytes(v1, v2, v3);
178            b1 <= 0b111111 &&
179            b2 <= 0b111111 &&
180            b3 <= 0b111111 &&
181            b4 <= 0b111111 &&
182            (v3 == 0 ==> b4 == 0) &&
183            (v2 == v3 == 0 ==> b3 == b4 == 0)
184        })
185    {
186        assert(
187            (v1 >> 2) <= 0b111111 &&
188            ((v1 & 0b11) << 4) | (v2 >> 4) <= 0b111111 &&
189            ((v2 & 0b1111) << 2) | (v3 >> 6) <= 0b111111 &&
190            (v3 & 0b111111) <= 0b111111 &&
191            (v3 == 0 ==> (v3 & 0b111111) == 0) &&
192            (v2 == v3 == 0 ==> ((v2 & 0b1111) << 2) | (v3 >> 6) == (v3 & 0b111111) == 0)
193        ) by (bit_vector);
194    }
195
196    broadcast proof fn decode_spec_encode_6_bit_bytes(b1: u8, b2: u8, b3: u8, b4: u8)
197        requires b1 <= 0b111111 && b2 <= 0b111111 && b3 <= 0b111111 && b4 <= 0b111111
198        ensures ({
199            let (v1, v2, v3) = #[trigger] Self::spec_decode_6_bit_bytes(b1, b2, b3, b4);
200            (b1, b2, b3, b4) == Self::spec_encode_6_bit_bytes(v1, v2, v3)
201        })
202    {
203        assert(
204            b1 <= 0b111111 && b2 <= 0b111111 && b3 <= 0b111111 && b4 <= 0b111111 ==>
205            b1 == (((b1 << 2) | (b2 >> 4)) >> 2) &&
206            b2 == ((((b1 << 2) | (b2 >> 4)) & 0b11) << 4) | (((b2 << 4) | (b3 >> 2)) >> 4) &&
207            b3 == ((((b2 << 4) | (b3 >> 2)) & 0b1111) << 2) | (((b3 << 6) | b4) >> 6) &&
208            b4 == ((b3 << 6) | b4) & 0b111111
209        ) by (bit_vector);
210    }
211}
212
213impl SecureSpecCombinator for Base64 {
214    open spec fn is_prefix_secure() -> bool {
215        false
216    }
217
218    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult)
219        decreases v.len()
220    {
221        let empty: Seq<u8> = seq![];
222
223        if v.len() == 0 {
224            assert(self.spec_serialize(v).unwrap() == empty);
225            assert(self.spec_parse(empty).unwrap() == (0usize, v));
226        } else {
227            if let Ok(s) = self.spec_serialize(v) {
228                broadcast use
229                    Base64::encode_spec_decode_6_bit_bytes,
230                    Base64::spec_encode_6_bit_bytes_range,
231                    Base64::decode_spec_encode_6_bit_bytes;
232
233                if v.len() < 3 {
234                    assert(s.skip(4) == empty);
235                } else {
236                    self.theorem_serialize_parse_roundtrip(v.skip(3));
237                    let s_rest = self.spec_serialize(v.skip(3)).unwrap();
238                    assert(s.skip(4) =~= s_rest);
239                    assert(s =~= seq![ s[0], s[1], s[2], s[3] ] + s.skip(4));
240                }
241
242                assert(self.spec_parse(s).unwrap().1 =~= v);
243            }
244        }
245    }
246
247    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>)
248        decreases s.len()
249    {
250        let empty: Seq<u8> = seq![];
251
252        if s.len() == 0 {
253            assert(self.spec_parse(s).unwrap().1 == empty);
254            assert(self.spec_serialize(empty).unwrap() == s);
255            assert(empty.subrange(0, 0) == empty);
256        } else {
257            if let Ok((len, v)) = self.spec_parse(s) {
258                broadcast use
259                    Base64::encode_spec_decode_6_bit_bytes,
260                    Base64::spec_encode_6_bit_bytes_range,
261                    Base64::decode_spec_encode_6_bit_bytes;
262
263                if s.len() >= 4 {
264                    self.theorem_parse_serialize_roundtrip(s.skip(4));
265
266                    let (len_rest, v_rest) = self.spec_parse(s.skip(4)).unwrap();
267                    let s_rest = self.spec_serialize(v_rest).unwrap();
268                    assert(s.skip(4) =~= s_rest);
269
270                    if v.len() >= 3 {
271                        assert(v_rest =~= v.skip(3));
272                    } else if v.len() == 1 || v.len() == 2 {
273                        assert(s.len() == 4);
274                    }
275
276                    let s2 = self.spec_serialize(v).unwrap();
277                    assert(s2 =~= s);
278                    assert(s2.subrange(0, s2.len() as int) =~= s);
279                }
280            }
281        }
282    }
283
284    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
285}
286
287/// Exec versions of some of the spec functions above
288impl Base64 {
289    #[inline(always)]
290    fn char_to_bits(b: u8) -> (res: Result<Option<u8>, ()>)
291        ensures res == Self::spec_char_to_bits(b)
292    {
293        let c = b as char;
294        if c >= 'A' && c <= 'Z' {
295            Ok(Some((b - 'A' as u8) as u8))
296        } else if c >= 'a' && c <= 'z' {
297            Ok(Some((b - 'a' as u8 + 26) as u8))
298        } else if c >= '0' && c <= '9' {
299            Ok(Some((b - '0' as u8 + 52) as u8))
300        } else if c == '+' {
301            Ok(Some(62))
302        } else if c == '/' {
303            Ok(Some(63))
304        } else if c == '=' {
305            Ok(None)
306        } else {
307            Err(())
308        }
309    }
310
311    #[inline(always)]
312    fn bits_to_char(b: u8) -> (res: u8)
313        ensures res == Self::spec_bits_to_char(b)
314    {
315        if b < 26 {
316            (b + 'A' as u8) as u8
317        } else if b < 52 {
318            (b - 26 + 'a' as u8) as u8
319        } else if b < 62 {
320            (b - 52 + '0' as u8) as u8
321        } else if b == 62 {
322            '+' as u8
323        } else {
324            '/' as u8
325        }
326    }
327
328    /// Exec version of spec_decode_6_bit_bytes
329    #[inline(always)]
330    fn decode_6_bit_bytes(b1: u8, b2: u8, b3: u8, b4: u8) -> (res: (u8, u8, u8))
331        ensures res == Self::spec_decode_6_bit_bytes(b1, b2, b3, b4)
332    {
333        let v1 = (b1 << 2) | (b2 >> 4);
334        let v2 = (b2 << 4) | (b3 >> 2);
335        let v3 = (b3 << 6) | b4;
336        (v1, v2, v3)
337    }
338
339    /// Exec version of spec_encode_6_bit_bytes
340    #[inline(always)]
341    fn encode_6_bit_bytes(v1: u8, v2: u8, v3: u8) -> (res: (u8, u8, u8, u8))
342        ensures res == Self::spec_encode_6_bit_bytes(v1, v2, v3)
343    {
344        let b1 = v1 >> 2;
345        let b2 = ((v1 & 0b11) << 4) | (v2 >> 4);
346        let b3 = ((v2 & 0b1111) << 2) | (v3 >> 6);
347        let b4 = v3 & 0b111111;
348        (b1, b2, b3, b4)
349    }
350}
351
352impl Combinator for Base64 {
353    type Result<'a> = Vec<u8>;
354    type Owned = Vec<u8>;
355
356    closed spec fn spec_length(&self) -> Option<usize> {
357        None
358    }
359
360    fn length(&self) -> Option<usize> {
361        None
362    }
363
364    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
365        let mut out = Vec::with_capacity(s.len() / 4 * 3);
366        let mut i = 0;
367        let len = s.len();
368
369        assert(s@.skip(0) == s@);
370
371        while i < len
372            invariant
373                0 <= i <= len,
374                len == s@.len(),
375
376                Self::spec_parse_helper(s@.skip(i as int)) matches Ok((_, rest)) ==> {
377                    &&& Self::spec_parse_helper(s@) matches Ok((_, final_out))
378                    &&& final_out =~= out@ + rest
379                },
380
381                Self::spec_parse_helper(s@.skip(i as int)) is Err ==>
382                    Self::spec_parse_helper(s@) is Err,
383            decreases len - i
384        {
385            assert(len - i == s@.skip(i as int).len());
386
387            if len - i < 4 {
388                return Err(ParseError::Other("invalid base64".to_string()));
389            }
390
391            let b1 = Self::char_to_bits(s[i]);
392            let b2 = Self::char_to_bits(s[i + 1]);
393            let b3 = Self::char_to_bits(s[i + 2]);
394            let b4 = Self::char_to_bits(s[i + 3]);
395
396            match (b1, b2, b3, b4) {
397                // No padding, continue parsing
398                (Ok(Some(b1)), Ok(Some(b2)), Ok(Some(b3)), Ok(Some(b4))) => {
399                    let (v1, v2, v3) = Self::decode_6_bit_bytes(b1, b2, b3, b4);
400                    out.push(v1);
401                    out.push(v2);
402                    out.push(v3);
403                    assert(s@.skip(i as int).skip(4) =~= s@.skip(i + 4));
404                }
405
406                // Padding of 1/2 bytes, stop parsing
407                (Ok(Some(b1)), Ok(Some(b2)), Ok(Some(b3)), Ok(None)) => {
408                    let (v1, v2, v3) = Self::decode_6_bit_bytes(b1, b2, b3, 0);
409                    if len - i == 4 && v3 == 0 {
410                        out.push(v1);
411                        out.push(v2);
412                    } else {
413                        return Err(ParseError::Other("invalid base64 padding".to_string()));
414                    }
415                }
416
417                (Ok(Some(b1)), Ok(Some(b2)), Ok(None), Ok(None)) => {
418                    let (v1, v2, v3) = Self::decode_6_bit_bytes(b1, b2, 0, 0);
419                    if len - i == 4 && v2 == 0 && v3 == 0 {
420                        out.push(v1);
421                    } else {
422                        return Err(ParseError::Other("invalid base64 padding".to_string()));
423                    }
424                }
425
426                _ => return Err(ParseError::Other("invalid base64".to_string())),
427            }
428
429            i += 4;
430        }
431
432        Ok((s.len(), out))
433    }
434
435    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
436        let mut i = 0;
437        let mut written = 0;
438        let len = v.len();
439
440        if pos >= data.len() {
441            return Err(SerializeError::InsufficientBuffer);
442        }
443
444        assert(v@.skip(0) == v@);
445
446        while i < len
447            invariant
448                0 <= i <= len,
449                len == v@.len(),
450
451                data@.len() == old(data)@.len(),
452                data@ =~= seq_splice(old(data)@, pos, data@.subrange(pos as int, pos + written)),
453
454                Self::spec_serialize_helper(v@.skip(i as int)) matches Ok(rest) ==> {
455                    &&& Self::spec_serialize_helper(v@) matches Ok(final_out)
456                    &&& final_out =~= data@.subrange(pos as int, pos + written) + rest
457                    &&& final_out.len() == written + rest.len()
458                },
459
460                // Self::spec_serialize_helper(v@.skip(i as int)) is Err ==>
461                //     Self::spec_serialize_helper(v@) is Err,
462            decreases len - i
463        {
464            let v1 = v[i];
465            let v2 = if len - i > 1 { v[i + 1] } else { 0 };
466            let v3 = if len - i > 2 { v[i + 2] } else { 0 };
467
468            let (b1, b2, b3, b4) = Self::encode_6_bit_bytes(v1, v2, v3);
469
470            let b1 = Self::bits_to_char(b1);
471            let b2 = Self::bits_to_char(b2);
472            let b3 = if len - i > 1 { Self::bits_to_char(b3) } else { '=' as u8 };
473            let b4 = if len - i > 2 { Self::bits_to_char(b4) } else { '=' as u8 };
474
475            if pos < data.len() && data.len() - pos >= written && data.len() - pos - written >= 4 {
476                data.set(pos + written, b1);
477                data.set(pos + written + 1, b2);
478                data.set(pos + written + 2, b3);
479                data.set(pos + written + 3, b4);
480            } else {
481                return Err(SerializeError::InsufficientBuffer);
482            }
483
484            if len - i < 3 {
485                let ghost empty: Seq<u8> = seq![];
486                assert(v@.skip(len as int) =~= empty);
487                i = len;
488            } else {
489                assert(v@.skip(i + 3) =~= v@.skip(i as int).skip(3));
490                i += 3;
491            }
492
493            written += 4;
494        }
495
496        assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
497
498        Ok(written)
499    }
500}
501
502}
503
504#[cfg(test)]
505mod test {
506    use super::*;
507
508    fn assert_parses_to(s: &[u8], expected: &[u8]) {
509        let (len, out) = Base64.parse(s).unwrap();
510        assert_eq!(len, s.len());
511        assert_eq!(out, expected);
512    }
513
514    #[test]
515    fn basic() {
516        assert_parses_to(b"aGVsbG8=", b"hello");
517        assert_parses_to(b"aGVsbA==", b"hell");
518        assert_parses_to(b"aGVs", b"hel");
519
520        assert!(Base64.parse(b"aGVsbG8").is_err());
521        assert!(Base64.parse(b"aGVsbA=").is_err());
522    }
523}
verdict_parser/common/base64.rs

verdict_parser/common/
base64.rs
