vest/regular/
bytes_n.rs

1use crate::properties::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7/// Combinator for parsing and serializing a fixed number of bytes (statically known).
8pub struct BytesN<const N: usize>;
9
10impl<const N: usize> View for BytesN<N> {
11    type V = BytesN<N>;
12
13    open spec fn view(&self) -> Self::V {
14        *self
15    }
16}
17
18impl<const N: usize> SpecCombinator for BytesN<N> {
19    type SpecResult = Seq<u8>;
20
21    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
22        if N <= s.len() {
23            Ok((N, s.subrange(0, N as int)))
24        } else {
25            Err(())
26        }
27    }
28
29    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
30        if v.len() == N {
31            Ok(v)
32        } else {
33            Err(())
34        }
35    }
36
37    proof fn spec_parse_wf(&self, s: Seq<u8>) {
38    }
39}
40
41impl<const N: usize> SecureSpecCombinator for BytesN<N> {
42    open spec fn is_prefix_secure() -> bool {
43        true
44    }
45
46    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
47        assert(s1.add(s2).len() == s1.len() + s2.len());
48        if let Ok((n, v)) = self.spec_parse(s1) {
49            assert(s1.add(s2).subrange(0, n as int) == s1.subrange(0, n as int))
50        } else {
51        }
52    }
53
54    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
55        if let Ok(buf) = self.spec_serialize(v) {
56            assert(v.subrange(0, v.len() as int) == v);
57        }
58    }
59
60    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
61    }
62}
63
64impl<const N: usize> Combinator for BytesN<N> {
65    type Result<'a> = &'a [u8];
66
67    type Owned = Vec<u8>;
68
69    open spec fn spec_length(&self) -> Option<usize> {
70        Some(N)
71    }
72
73    fn length(&self) -> Option<usize> {
74        Some(N)
75    }
76
77    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
78        if N <= s.len() {
79            let s_ = slice_subrange(s, 0, N);
80            Ok((N, s_))
81        } else {
82            Err(ParseError::UnexpectedEndOfInput)
83        }
84    }
85
86    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
87        usize,
88        SerializeError,
89    >) {
90        if v.len() <= data.len() && v.len() == N && pos < data.len() - v.len() {
91            set_range(data, pos, v);
92            assert(data@.subrange(pos as int, pos + N as int) == self@.spec_serialize(v@).unwrap());
93            Ok(N)
94        } else {
95            Err(SerializeError::InsufficientBuffer)
96        }
97    }
98}
99
100} // verus!
vest/regular/bytes_n.rs

vest/regular/
bytes_n.rs
