vest/regular/
repeat.rs

1use crate::properties::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7/// A combinator to repeatedly parse/serialize the inner combinator C
8/// until the end of the buffer.
9///
10/// If the inner combinator fails before the end of the buffer, Repeat fails
11pub struct Repeat<C>(pub C);
12
13/// Wrappers around Vec so that their View's can be implemented as DeepView
14#[derive(Debug)]
15pub struct RepeatResult<'a, C: Combinator>(pub Vec<C::Result<'a>>) where
16    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
17;
18
19/// Owned version of RepeatResult
20#[derive(Debug)]
21pub struct RepeatResultOwned<C: Combinator>(pub Vec<C::Owned>) where
22    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
23;
24
25impl<C: View> View for Repeat<C> {
26    type V = Repeat<<C as View>::V>;
27
28    open spec fn view(&self) -> Self::V {
29        Repeat(self.0@)
30    }
31}
32
33impl<C: Combinator> View for RepeatResultOwned<C> where
34    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
35 {
36    type V = Seq<<C::Owned as View>::V>;
37
38    open spec fn view(&self) -> Self::V {
39        Seq::new(self.0.len() as nat, |i: int| self.0@[i]@)
40    }
41}
42
43impl<'a, C: Combinator> View for RepeatResult<'a, C> where
44    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
45 {
46    type V = Seq<<C::Owned as View>::V>;
47
48    open spec fn view(&self) -> Self::V {
49        Seq::new(self.0.len() as nat, |i: int| self.0@[i]@)
50    }
51}
52
53impl<C: SpecCombinator + SecureSpecCombinator> SpecCombinator for Repeat<C> {
54    type SpecResult = Seq<C::SpecResult>;
55
56    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>
57        decreases s.len(),
58    {
59        if !C::is_prefix_secure() {
60            Err(())
61        } else if s.len() == 0 {
62            Ok((0, seq![]))
63        } else {
64            match self.0.spec_parse(s) {
65                Ok((n, v)) => if 0 < n <= s.len() {
66                    match self.spec_parse(s.skip(n as int)) {
67                        Ok((_, vs)) => Ok((s.len() as usize, seq![v] + vs)),
68                        Err(..) => Err(()),
69                    }
70                } else {
71                    Err(())
72                },
73                Err(..) => Err(()),
74            }
75        }
76    }
77
78    proof fn spec_parse_wf(&self, s: Seq<u8>) {
79    }
80
81    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>
82        decreases v.len(),
83    {
84        if !C::is_prefix_secure() {
85            Err(())
86        } else if v.len() == 0 {
87            Ok(seq![])
88        } else {
89            match self.0.spec_serialize(v[0]) {
90                Ok(s) => if s.len() != 0 {
91                    match self.spec_serialize(v.drop_first()) {
92                        Ok(rest) => if s.len() + rest.len() <= usize::MAX {
93                            Ok(s + rest)
94                        } else {
95                            Err(())
96                        },
97                        Err(..) => Err(()),
98                    }
99                } else {
100                    Err(())
101                },
102                Err(..) => Err(()),
103            }
104        }
105    }
106}
107
108impl<C: SecureSpecCombinator> SecureSpecCombinator for Repeat<C> {
109    /// Prepending bytes to the buffer may result in more items parsed
110    /// so Repeat is not prefix secure
111    open spec fn is_prefix_secure() -> bool {
112        false
113    }
114
115    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult)
116        decreases v.len(),
117    {
118        if v.len() == 0 {
119            assert(self.spec_serialize(v) matches Ok(b) ==> self.spec_parse(b).unwrap() =~= (0, v));
120        } else {
121            if self.spec_serialize(v).is_ok() {
122                let s = self.0.spec_serialize(v[0]).unwrap();
123                let rest = self.spec_serialize(v.drop_first()).unwrap();
124
125                self.theorem_serialize_parse_roundtrip(v.drop_first());
126                self.0.theorem_serialize_parse_roundtrip(v[0]);
127
128                // Some technical assumptions (e.g. C should not parse a different
129                // value when the buffer is extended with more bytes)
130                if C::is_prefix_secure() && s.len() + rest.len() <= usize::MAX {
131                    self.0.lemma_prefix_secure(s, rest);
132                    let (n, _) = self.0.spec_parse(s + rest).unwrap();
133                    self.0.spec_parse_wf(s + rest);
134
135                    assert((s + rest).skip(n as int) =~= rest);
136                    assert(seq![v[0]] + v.drop_first() == v);
137                }
138            }
139        }
140    }
141
142    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
143        decreases buf.len(),
144    {
145        if buf.len() == 0 {
146            let empty: Seq<u8> = seq![];
147            assert(buf.subrange(0, 0) =~= empty);
148        } else {
149            if let Ok((n, v)) = self.spec_parse(buf) {
150                let (n1, v1) = self.0.spec_parse(buf).unwrap();
151                let (n2, v2) = self.spec_parse(buf.skip(n1 as int)).unwrap();
152
153                self.theorem_parse_serialize_roundtrip(buf.skip(n1 as int));
154                self.0.theorem_parse_serialize_roundtrip(buf);
155
156                if C::is_prefix_secure() {
157                    assert(v2 == v.drop_first());
158                    assert(buf.subrange(0, n1 as int) + buf.skip(n1 as int).subrange(0, n2 as int)
159                        == buf.subrange(0, n as int));
160                }
161            }
162        }
163    }
164
165    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
166    }
167}
168
169impl<C: Combinator> Repeat<C> where
170    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
171 {
172    /// Get the deep view of RepeatResult
173    pub open spec fn deep_view<'a>(v: &'a [C::Result<'a>]) -> Seq<<C::Owned as View>::V> {
174        Seq::new(v.len() as nat, |i: int| v@[i]@)
175    }
176
177    /// Helper function for parse()
178    #[inline(always)]
179    fn parse_helper<'a>(&self, s: &'a [u8]) -> (r: Result<Vec<C::Result<'a>>, ParseError>)
180        requires
181            self.0.parse_requires(),
182            C::V::is_prefix_secure(),
183        ensures
184            r matches Ok(res) ==> {
185                &&& self@.spec_parse(s@) matches Ok((_, v))
186                &&& RepeatResult::<C>(res)@ =~= v
187            },
188            r is Err ==> self@.spec_parse(s@) is Err,
189    {
190        let mut res = Vec::new();
191        let mut offset: usize = 0;
192
193        assert(s@.subrange(0, s@.len() as int) == s@);
194
195        while offset < s.len()
196            invariant
197                0 <= offset <= s@.len(),
198                self.parse_requires(),
199                self@.spec_parse(s@.subrange(offset as int, s@.len() as int)) matches Ok((_, rest)) ==> {
200                    &&& self@.spec_parse(s@) matches Ok((_, v))
201                    &&& RepeatResult::<C>(res)@ + rest =~= v
202                },
203                offset < s@.len() ==>
204                    (self@.spec_parse(s@.subrange(offset as int, s@.len() as int)) is Err ==> self@.spec_parse(s@) is Err),
205            decreases s.len() - offset
206        {
207            let (n, v) = self.0.parse(slice_subrange(s, offset, s.len()))?;
208            if n == 0 {
209                return Err(ParseError::RepeatEmptyElement);
210            }
211
212            let ghost prev_offset = offset;
213
214            res.push(v);
215            offset += n;
216
217            assert(s@.subrange(prev_offset as int, s@.len() as int).skip(n as int)
218                =~= s@.subrange(offset as int, s@.len() as int))
219        }
220
221        let ghost empty: Seq<u8> = seq![];
222        assert(s@.subrange(s@.len() as int, s@.len() as int) == empty);
223
224        Ok(res)
225    }
226
227    fn serialize_helper(
228        &self,
229        v: &mut RepeatResult<'_, C>,
230        data: &mut Vec<u8>,
231        pos: usize,
232        len: usize,
233    ) -> (res: Result<usize, SerializeError>)
234        requires
235            self.0.serialize_requires(),
236            C::V::is_prefix_secure(),
237        ensures
238            data@.len() == old(data)@.len(),
239            res matches Ok(n) ==> {
240                &&& self@.spec_serialize(old(v)@) is Ok
241                &&& self@.spec_serialize(old(v)@) matches Ok(s) ==> n == (len + s.len()) && data@
242                    =~= seq_splice(old(data)@, (pos + len) as usize, s)
243            },
244        decreases old(v)@.len()
245    {
246        if pos > usize::MAX - len || pos + len >= data.len() {
247            return Err(SerializeError::InsufficientBuffer);
248        }
249        if v.0.len() == 0 {
250            assert(data@ =~= seq_splice(old(data)@, pos, seq![]));
251            return Ok(len);
252        }
253        let n1 = self.0.serialize(v.0.remove(0), data, pos + len)?;
254
255        assert(v@ =~= old(v)@.drop_first());
256
257        if n1 > 0 {
258            let ghost data2 = data@;
259
260            if let Some(next_len) = len.checked_add(n1) {
261                self.serialize_helper(v, data, pos, next_len)
262            } else {
263                Err(SerializeError::SizeOverflow)
264            }
265        } else {
266            Err(SerializeError::RepeatEmptyElement)
267        }
268    }
269}
270
271impl<C: Combinator> Combinator for Repeat<C> where
272    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
273 {
274    type Result<'a> = RepeatResult<'a, C>;
275
276    type Owned = RepeatResultOwned<C>;
277
278    open spec fn spec_length(&self) -> Option<usize> {
279        None
280    }
281
282    fn length(&self) -> Option<usize> {
283        None
284    }
285
286    open spec fn parse_requires(&self) -> bool {
287        &&& <C as View>::V::is_prefix_secure()
288        &&& self.0.parse_requires()
289    }
290
291    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
292        Ok((s.len(), RepeatResult(self.parse_helper(s)?)))
293    }
294
295    open spec fn serialize_requires(&self) -> bool {
296        &&& <C as View>::V::is_prefix_secure()
297        &&& self.0.serialize_requires()
298    }
299
300    fn serialize(&self, mut v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
301        usize,
302        SerializeError,
303    >) {
304        let n = self.serialize_helper(&mut v, data, pos, 0)?;
305        assert(v@.skip(0) == v@);
306        Ok(n)
307    }
308}
309
310} // verus!
vest/regular/repeat.rs

vest/regular/
repeat.rs
