vest_lib/regular/
bytes.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4use super::modifier::AndThen;
5
6verus! {
7
8/// Combinator for parsing and serializing a fixed number of bytes (dynamically known).
9pub struct Variable(pub usize);
10
11impl View for Variable {
12    type V = Variable;
13
14    open spec fn view(&self) -> Self::V {
15        *self
16    }
17}
18
19impl Variable {
20    /// Spec version of [`Self::and_then`]
21    pub open spec fn spec_and_then<Next: SpecCombinator>(self, next: Next) -> AndThen<
22        Variable,
23        Next,
24    > {
25        AndThen(self, next)
26    }
27
28    /// Chains this combinator with another combinator.
29    pub fn and_then<'x, I, O, Next: Combinator<'x, I, O>>(self, next: Next) -> (o: AndThen<
30        Variable,
31        Next,
32    >) where
33        I: VestPublicInput,
34        O: VestPublicOutput<I>,
35        Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,
36
37        ensures
38            o@ == self@.spec_and_then(next@),
39    {
40        AndThen(self, next)
41    }
42}
43
44impl SpecCombinator for Variable {
45    type Type = Seq<u8>;
46
47    open spec fn wf(&self, v: Self::Type) -> bool {
48        v.len() == self.0
49    }
50
51    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
52        if self.0 <= s.len() {
53            Some((self.0 as int, s.take(self.0 as int)))
54        } else {
55            None
56        }
57    }
58
59    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
60        v
61    }
62}
63
64impl SecureSpecCombinator for Variable {
65    open spec fn is_prefix_secure() -> bool {
66        true
67    }
68
69    open spec fn is_productive(&self) -> bool {
70        self.0 > 0
71    }
72
73    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
74        assert(s1.add(s2).len() == s1.len() + s2.len());
75        if let Some((n, v)) = self.spec_parse(s1) {
76            assert(s1.add(s2).subrange(0, n as int) == s1.subrange(0, n as int))
77        } else {
78        }
79    }
80
81    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
82        assert(v.take(v.len() as int) == v);
83    }
84
85    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
86    }
87
88    proof fn lemma_parse_length(&self, s: Seq<u8>) {
89    }
90
91    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
92    }
93}
94
95impl<'x, I, O> Combinator<'x, I, O> for Variable where I: VestInput + 'x, O: VestOutput<I> {
96    type Type = I;
97
98    type SType = &'x I;
99
100    fn length(&self, v: Self::SType) -> usize {
101        self.0
102    }
103
104    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
105        if self.0 <= s.len() {
106            let s_ = s.subrange(0, self.0);
107            Ok((self.0, s_))
108        } else {
109            Err(ParseError::UnexpectedEndOfInput)
110        }
111    }
112
113    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
114        usize,
115        SerializeError,
116    >) {
117        if v.len() <= data.len() && pos <= data.len() - v.len() {
118            data.set_range(pos, &v);
119            assert(data@.subrange(pos as int, pos + self.0 as int) == self@.spec_serialize(v@));
120            Ok(self.0)
121        } else {
122            Err(SerializeError::InsufficientBuffer)
123        }
124    }
125}
126
127/// Combinator for parsing and serializing a fixed number of bytes (statically known).
128pub struct Fixed<const N: usize>;
129
130impl<const N: usize> View for Fixed<N> {
131    type V = Fixed<N>;
132
133    open spec fn view(&self) -> Self::V {
134        *self
135    }
136}
137
138impl<const N: usize> SpecCombinator for Fixed<N> {
139    type Type = Seq<u8>;
140
141    open spec fn wf(&self, v: Self::Type) -> bool {
142        v.len() == N
143    }
144
145    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
146        if N <= s.len() {
147            Some((N as int, s.take(N as int)))
148        } else {
149            None
150        }
151    }
152
153    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
154        v
155    }
156}
157
158impl<const N: usize> SecureSpecCombinator for Fixed<N> {
159    open spec fn is_prefix_secure() -> bool {
160        true
161    }
162
163    open spec fn is_productive(&self) -> bool {
164        N > 0
165    }
166
167    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
168        assert(s1.add(s2).len() == s1.len() + s2.len());
169        if let Some((n, v)) = self.spec_parse(s1) {
170            assert(s1.add(s2).subrange(0, n as int) == s1.subrange(0, n as int))
171        } else {
172        }
173    }
174
175    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
176        assert(v.take(v.len() as int) == v);
177    }
178
179    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
180    }
181
182    proof fn lemma_parse_length(&self, s: Seq<u8>) {
183    }
184
185    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
186    }
187}
188
189impl<'x, const N: usize, I, O> Combinator<'x, I, O> for Fixed<N> where
190    I: VestInput + 'x,
191    O: VestOutput<I>,
192 {
193    type Type = I;
194
195    type SType = &'x I;
196
197    fn length(&self, v: Self::SType) -> usize {
198        N
199    }
200
201    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
202        if N <= s.len() {
203            let s_ = s.subrange(0, N);
204            Ok((N, s_))
205        } else {
206            Err(ParseError::UnexpectedEndOfInput)
207        }
208    }
209
210    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
211        usize,
212        SerializeError,
213    >) {
214        if v.len() <= data.len() && pos <= data.len() - v.len() {
215            data.set_range(pos, &v);
216            assert(data@.subrange(pos as int, pos + N as int) == self@.spec_serialize(v@));
217            Ok(N)
218        } else {
219            Err(SerializeError::InsufficientBuffer)
220        }
221    }
222}
223
224/// Combinator that returns the rest of the input bytes from the current position.
225pub struct Tail;
226
227impl View for Tail {
228    type V = Tail;
229
230    open spec fn view(&self) -> Self::V {
231        Tail
232    }
233}
234
235impl SpecCombinator for Tail {
236    type Type = Seq<u8>;
237
238    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
239        Some((s.len() as int, s))
240    }
241
242    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
243        v
244    }
245}
246
247impl SecureSpecCombinator for Tail {
248    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
249    }
250
251    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
252        assert(buf.subrange(0, buf.len() as int) == buf);
253    }
254
255    open spec fn is_prefix_secure() -> bool {
256        false
257    }
258
259    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
260    }
261
262    proof fn lemma_parse_length(&self, s: Seq<u8>) {
263    }
264
265    open spec fn is_productive(&self) -> bool {
266        false
267    }
268
269    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
270    }
271}
272
273impl<'x, I: VestInput + 'x, O: VestOutput<I>> Combinator<'x, I, O> for Tail {
274    type Type = I;
275
276    type SType = &'x I;
277
278    fn length(&self, v: Self::SType) -> usize {
279        v.len()
280    }
281
282    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
283        Ok(((s.len()), s))
284    }
285
286    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
287        usize,
288        SerializeError,
289    >) {
290        if v.len() <= data.len() - pos {
291            data.set_range(pos, &v);
292            assert(data@.subrange(pos as int, pos + v@.len() as int) == self@.spec_serialize(v@));
293            Ok(v.len())
294        } else {
295            Err(SerializeError::InsufficientBuffer)
296        }
297    }
298}
299
300} // verus!
vest_lib/regular/bytes.rs

vest_lib/regular/
bytes.rs
