verdict_parser/common/
repeat.rs

1use super::*;
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
11#[derive(Debug)]
12pub struct Repeat<C>(pub C);
13
14impl<C: View> View for Repeat<C>
15{
16    type V = Repeat<<C as View>::V>;
17
18    open spec fn view(&self) -> Self::V {
19        Repeat(self.0@)
20    }
21}
22
23impl<C: SpecCombinator + SecureSpecCombinator> SpecCombinator for Repeat<C> {
24    type SpecResult = Seq<C::SpecResult>;
25
26    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>
27        decreases s.len()
28    {
29        if !C::is_prefix_secure() {
30            Err(())
31        } else if s.len() == 0 {
32            Ok((0, seq![]))
33        } else {
34            match self.0.spec_parse(s) {
35                Ok((n, v)) =>
36                    if 0 < n <= s.len() {
37                        match self.spec_parse(s.skip(n as int)) {
38                            Ok((_, vs)) => Ok((s.len() as usize, seq![v] + vs)),
39                            Err(..) => Err(()),
40                        }
41                    } else {
42                        Err(())
43                    }
44                Err(..) => Err(()),
45            }
46        }
47    }
48
49    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
50
51    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>
52        decreases v.len()
53    {
54        if !C::is_prefix_secure() {
55            Err(())
56        } else if v.len() == 0 {
57            Ok(seq![])
58        } else {
59            match self.0.spec_serialize(v[0]) {
60                Ok(s) =>
61                    if s.len() != 0 {
62                        match self.spec_serialize(v.drop_first()) {
63                            Ok(rest) =>
64                                if s.len() + rest.len() <= usize::MAX {
65                                    Ok(s + rest)
66                                } else {
67                                    Err(())
68                                }
69                            Err(..) => Err(()),
70                        }
71                    } else {
72                        Err(())
73                    }
74                Err(..) => Err(()),
75            }
76        }
77    }
78}
79
80impl<C: SecureSpecCombinator> SecureSpecCombinator for Repeat<C> {
81    /// Prepending bytes to the buffer may result in more items parsed
82    /// so Repeat is not prefix secure
83    open spec fn is_prefix_secure() -> bool {
84        false
85    }
86
87    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult)
88        decreases v.len()
89    {
90        if v.len() == 0 {
91            assert(self.spec_serialize(v) matches Ok(b) ==> self.spec_parse(b).unwrap() =~= (0, v));
92        } else {
93            if self.spec_serialize(v).is_ok() {
94                let s = self.0.spec_serialize(v[0]).unwrap();
95                let rest = self.spec_serialize(v.drop_first()).unwrap();
96
97                self.theorem_serialize_parse_roundtrip(v.drop_first());
98                self.0.theorem_serialize_parse_roundtrip(v[0]);
99
100                // Some technical assumptions (e.g. C should not parse a different
101                // value when the buffer is extended with more bytes)
102                if C::is_prefix_secure() && s.len() + rest.len() <= usize::MAX {
103                    self.0.lemma_prefix_secure(s, rest);
104                    let (n, _) = self.0.spec_parse(s + rest).unwrap();
105                    self.0.spec_parse_wf(s + rest);
106
107                    assert((s + rest).skip(n as int) =~= rest);
108                    assert(seq![v[0]] + v.drop_first() == v);
109                }
110            }
111        }
112    }
113
114    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
115        decreases buf.len()
116    {
117        if buf.len() == 0 {
118            let empty: Seq<u8> = seq![];
119            assert(buf.subrange(0, 0) =~= empty);
120        } else {
121            if let Ok((n, v)) = self.spec_parse(buf) {
122                let (n1, v1) = self.0.spec_parse(buf).unwrap();
123                let (n2, v2) = self.spec_parse(buf.skip(n1 as int)).unwrap();
124
125                self.theorem_parse_serialize_roundtrip(buf.skip(n1 as int));
126                self.0.theorem_parse_serialize_roundtrip(buf);
127
128                if C::is_prefix_secure() {
129                    assert(v2 == v.drop_first());
130                    assert(buf.subrange(0, n1 as int) + buf.skip(n1 as int).subrange(0, n2 as int) == buf.subrange(0, n as int));
131                }
132            }
133        }
134    }
135
136    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
137}
138
139impl<C: Combinator> Repeat<C> where
140    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
141{
142    pub open spec fn deep_view<'a>(v: &'a [C::Result<'a>]) -> Seq<<C::Owned as View>::V> {
143        Seq::new(v.len() as nat, |i: int| v@[i]@)
144    }
145
146    /// Helper function for parse()
147    /// TODO: Recursion is not ideal, but hopefully tail call opt will kick in
148    #[inline(always)]
149    fn parse_helper<'a>(&self, s: &'a [u8], res: &mut VecDeep<C::Result<'a>>) -> (r: Result<(), ParseError>)
150        requires
151            self.0.parse_requires(),
152            <C as View>::V::is_prefix_secure(),
153
154        ensures
155            r is Ok ==> {
156                &&& self@.spec_parse(s@) is Ok
157                &&& self@.spec_parse(s@) matches Ok((n, v)) ==>
158                    res@ =~= old(res)@ + v
159            },
160            r is Err ==> self@.spec_parse(s@) is Err
161
162        decreases s.len(),
163    {
164        if s.len() == 0 {
165            return Ok(());
166        }
167
168        let (n, v) = self.0.parse(s)?;
169
170        if n > 0 {
171            res.push(v);
172            self.parse_helper(slice_subrange(s, n, s.len()), res)
173        } else {
174            Err(ParseError::RepeatEmptyElement)
175        }
176    }
177
178    #[inline(always)]
179    fn serialize_helper(&self, v: &mut VecDeep<C::Result<'_>>, data: &mut Vec<u8>, pos: usize, len: usize)
180        -> (res: Result<usize, SerializeError>)
181        requires
182            self.0.serialize_requires(),
183            <C as View>::V::is_prefix_secure(),
184
185        ensures
186            data@.len() == old(data)@.len(),
187            res matches Ok(n) ==> {
188                &&& self@.spec_serialize(old(v)@) is Ok
189                &&& self@.spec_serialize(old(v)@) matches Ok(s) ==>
190                    n == (len + s.len()) && data@ =~= seq_splice(old(data)@, (pos + len) as usize, s)
191            },
192
193        decreases old(v)@.len()
194    {
195        if pos > usize::MAX - len || pos + len >= data.len() {
196            return Err(SerializeError::InsufficientBuffer);
197        }
198
199        if v.0.len() == 0 {
200            assert(data@ =~= seq_splice(old(data)@, pos, seq![]));
201            return Ok(len);
202        }
203
204        let n1 = self.0.serialize(v.0.remove(0), data, pos + len)?;
205
206        assert(v@ =~= old(v)@.drop_first());
207
208        if n1 > 0 {
209            if let Some(next_len) = len.checked_add(n1) {
210                self.serialize_helper(v, data, pos, next_len)
211            } else {
212                Err(SerializeError::SizeOverflow)
213            }
214        } else {
215            Err(SerializeError::RepeatEmptyElement)
216        }
217    }
218}
219
220/// TODO: this is somewhat arbitrary and based on the
221/// max number of arcs in an OID
222const REPEAT_DEFAULT_CAP: usize = 10;
223
224impl<C: Combinator> Combinator for Repeat<C> where
225    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
226{
227    type Result<'a> = VecDeep<C::Result<'a>>;
228    type Owned = VecDeep<C::Owned>;
229
230    closed spec fn spec_length(&self) -> Option<usize> {
231        None
232    }
233
234    fn length(&self) -> Option<usize> {
235        None
236    }
237
238    open spec fn parse_requires(&self) -> bool {
239        &&& <C as View>::V::is_prefix_secure()
240        &&& self.0.parse_requires()
241    }
242
243    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
244        let mut res = VecDeep::with_capacity(REPEAT_DEFAULT_CAP);
245        self.parse_helper(s, &mut res)?;
246        Ok((s.len(), res))
247    }
248
249    open spec fn serialize_requires(&self) -> bool {
250        &&& <C as View>::V::is_prefix_secure()
251        &&& self.0.serialize_requires()
252    }
253
254    fn serialize(&self, mut v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
255        let n = self.serialize_helper(&mut v, data, pos, 0)?;
256        assert(v@.skip(0) == v@);
257        Ok(n)
258    }
259}
260
261}
verdict_parser/common/repeat.rs

verdict_parser/common/
repeat.rs
