vest/regular/
bytes.rs

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

vest/regular/
bytes.rs
