vest/regular/
preceded.rs

1use crate::properties::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7/// Combinator that sequentially applies two combinators and returns the result of the second one.
8pub struct Preceded<Fst, Snd>(pub Fst, pub Snd);
9
10impl<Fst, Snd> View for Preceded<
11    Fst,
12    Snd,
13> where
14    Fst: for<'a> Combinator<Result<'a> = (), Owned = ()>,
15    Snd: Combinator,
16    Fst::V: SecureSpecCombinator<SpecResult = ()>,
17    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
18 {
19    type V = Preceded<Fst::V, Snd::V>;
20
21    open spec fn view(&self) -> Self::V {
22        Preceded(self.0@, self.1@)
23    }
24}
25
26impl<Fst: SecureSpecCombinator<SpecResult = ()>, Snd: SpecCombinator> SpecCombinator for Preceded<
27    Fst,
28    Snd,
29> {
30    type SpecResult = Snd::SpecResult;
31
32    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
33        if Fst::is_prefix_secure() {
34            if let Ok((n, ())) = self.0.spec_parse(s) {
35                if let Ok((m, v)) = self.1.spec_parse(s.subrange(n as int, s.len() as int)) {
36                    Ok(((n + m) as usize, v))
37                } else {
38                    Err(())
39                }
40            } else {
41                Err(())
42            }
43        } else {
44            Err(())
45        }
46    }
47
48    proof fn spec_parse_wf(&self, s: Seq<u8>) {
49        if let Ok((n, ())) = self.0.spec_parse(s) {
50            if let Ok((m, v)) = self.1.spec_parse(s.subrange(n as int, s.len() as int)) {
51                self.0.spec_parse_wf(s);
52                self.1.spec_parse_wf(s.subrange(n as int, s.len() as int));
53            }
54        }
55    }
56
57    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
58        if Fst::is_prefix_secure() {
59            if let Ok(buf1) = self.0.spec_serialize(()) {
60                if let Ok(buf2) = self.1.spec_serialize(v) {
61                    if buf1.len() + buf2.len() <= usize::MAX {
62                        Ok(buf1.add(buf2))
63                    } else {
64                        Err(())
65                    }
66                } else {
67                    Err(())
68                }
69            } else {
70                Err(())
71            }
72        } else {
73            Err(())
74        }
75    }
76}
77
78impl<
79    Fst: SecureSpecCombinator<SpecResult = ()>,
80    Snd: SecureSpecCombinator,
81> SecureSpecCombinator for Preceded<Fst, Snd> {
82    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
83        if let Ok((buf)) = self.spec_serialize(v) {
84            let buf0 = self.0.spec_serialize(()).unwrap();
85            let buf1 = self.1.spec_serialize(v).unwrap();
86            self.0.theorem_serialize_parse_roundtrip(());
87            self.0.lemma_prefix_secure(buf0, buf1);
88            self.1.theorem_serialize_parse_roundtrip(v);
89            assert(buf0.add(buf1).subrange(buf0.len() as int, buf.len() as int) == buf1);
90        }
91    }
92
93    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
94        if let Ok((nm, v)) = self.spec_parse(buf) {
95            let (n, _) = self.0.spec_parse(buf).unwrap();
96            self.0.spec_parse_wf(buf);
97            let buf0 = buf.subrange(0, n as int);
98            let buf1 = buf.subrange(n as int, buf.len() as int);
99            assert(buf == buf0.add(buf1));
100            self.0.lemma_prefix_secure(buf0, buf1);
101            self.0.theorem_parse_serialize_roundtrip(buf);
102            let (m, v_) = self.1.spec_parse(buf1).unwrap();
103            self.1.theorem_parse_serialize_roundtrip(buf1);
104            self.1.spec_parse_wf(buf1);
105            let buf2 = self.spec_serialize(v).unwrap();
106            assert(buf2 == buf.subrange(0, nm as int));
107        } else {
108        }
109    }
110
111    open spec fn is_prefix_secure() -> bool {
112        Fst::is_prefix_secure() && Snd::is_prefix_secure()
113    }
114
115    proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
116        if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
117            if let Ok((nm, v)) = self.spec_parse(buf) {
118                let (n, _) = self.0.spec_parse(buf).unwrap();
119                self.0.spec_parse_wf(buf);
120                let buf0 = buf.subrange(0, n as int);
121                let buf1 = buf.subrange(n as int, buf.len() as int);
122                self.0.lemma_prefix_secure(buf0, buf1);
123                self.0.lemma_prefix_secure(buf0, buf1.add(s2));
124                self.0.lemma_prefix_secure(buf, s2);
125                let (m, v_) = self.1.spec_parse(buf1).unwrap();
126                assert(buf.add(s2).subrange(0, n as int) == buf0);
127                assert(buf.add(s2).subrange(n as int, buf.add(s2).len() as int) == buf1.add(s2));
128                self.1.lemma_prefix_secure(buf1, s2);
129            } else {
130            }
131        } else {
132        }
133    }
134}
135
136impl<Fst, Snd> Combinator for Preceded<
137    Fst,
138    Snd,
139> where
140    Fst: for<'a> Combinator<Result<'a> = (), Owned = ()>,
141    Snd: Combinator,
142    Fst::V: SecureSpecCombinator<SpecResult = ()>,
143    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
144 {
145    type Result<'a> = Snd::Result<'a>;
146
147    type Owned = Snd::Owned;
148
149    open spec fn spec_length(&self) -> Option<usize> {
150        if let Some(n) = self.0.spec_length() {
151            if let Some(m) = self.1.spec_length() {
152                if n <= usize::MAX - m {
153                    Some((n + m) as usize)
154                } else {
155                    None
156                }
157            } else {
158                None
159            }
160        } else {
161            None
162        }
163    }
164
165    fn length(&self) -> Option<usize> {
166        if let Some(n) = self.0.length() {
167            if let Some(m) = self.1.length() {
168                if n <= usize::MAX - m {
169                    Some(n + m)
170                } else {
171                    None
172                }
173            } else {
174                None
175            }
176        } else {
177            None
178        }
179    }
180
181    open spec fn parse_requires(&self) -> bool {
182        self.0.parse_requires() && self.1.parse_requires() && Fst::V::is_prefix_secure()
183    }
184
185    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
186        let (n, ()): (usize, ()) = self.0.parse(s)?;
187        let s_ = slice_subrange(s, n, s.len());
188        let (m, v) = self.1.parse(s_)?;
189        if n <= usize::MAX - m {
190            Ok(((n + m), v))
191        } else {
192            Err(ParseError::SizeOverflow)
193        }
194    }
195
196    open spec fn serialize_requires(&self) -> bool {
197        self.0.serialize_requires() && self.1.serialize_requires() && Fst::V::is_prefix_secure()
198    }
199
200    fn serialize<'b>(&self, v: Self::Result<'_>, data: &'b mut Vec<u8>, pos: usize) -> (res: Result<
201        usize,
202        SerializeError,
203    >) {
204        let n = self.0.serialize((), data, pos)?;
205        if n <= usize::MAX - pos && n + pos <= data.len() {
206            let m = self.1.serialize(v, data, pos + n)?;
207            if m <= usize::MAX - n {
208                assert(data@.subrange(pos as int, pos + n + m as int) == self@.spec_serialize(
209                    v@,
210                ).unwrap());
211                assert(data@ == seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
212                Ok(n + m)
213            } else {
214                Err(SerializeError::SizeOverflow)
215            }
216        } else {
217            Err(SerializeError::InsufficientBuffer)
218        }
219    }
220}
221
222} // verus!
vest/regular/preceded.rs

vest/regular/
preceded.rs
