vest_lib/combinators/tail/
exec.rs

1//! Executable implementations for end-of-input and remaining-input formats.
2use crate::combinators::{Eof, Opt, Optional, Pair, Repeat, Star};
3use crate::core::exec::output::*;
4use crate::core::exec::{
5    input::InputBuf,
6    parser::{PResult, Parser},
7    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
8    ParseError,
9};
10use crate::core::proof::Productive;
11use crate::core::spec::SafeParser;
12use crate::core::spec::{Consistency, SpecByteLen};
13#[cfg(feature = "alloc")]
14use alloc::vec::Vec;
15use vstd::prelude::*;
16use OutputBuf;
17
18verus! {
19
20impl<I: InputBuf> Parser<I> for super::Tail {
21    type PT = I;
22
23    fn min_byte_len(&self) -> usize {
24        // The remaining input may be empty.
25        0
26    }
27
28    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
29        let len = ibuf.len();
30        let tail = ibuf.take(len);
31        proof {
32            assert(tail.deep_view() == ibuf@);
33        }
34        Ok((len, tail))
35    }
36}
37
38impl<Output: OutputBuf> Serializer<Output, [u8]> for super::Tail {
39    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
40        obuf.write_bytes(v);
41    }
42}
43
44impl<'i, Output: OutputBuf> Serializer<Output, &'i [u8]> for super::Tail {
45    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
46        obuf.write_bytes(*v);
47    }
48}
49
50impl ByteLen<[u8]> for super::Tail {
51    open spec fn exec_inv(&self) -> bool {
52        true
53    }
54
55    fn length(&self, v: &[u8]) -> (len: usize) {
56        v.len()
57    }
58}
59
60impl<'i> ByteLen<&'i [u8]> for super::Tail {
61    open spec fn exec_inv(&self) -> bool {
62        true
63    }
64
65    fn length(&self, v: &&'i [u8]) -> (len: usize) {
66        v.len()
67    }
68}
69
70impl Prepare<[u8]> for super::Tail {
71    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
72        Ok(v.len())
73    }
74}
75
76impl<'i> Prepare<&'i [u8]> for super::Tail {
77    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
78        Ok(v.len())
79    }
80}
81
82impl<I: InputBuf> Parser<I> for super::Eof {
83    type PT = ();
84
85    fn min_byte_len(&self) -> usize {
86        0
87    }
88
89    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
90        let len = ibuf.len();
91        if len == 0 {
92            Ok((0, ()))
93        } else {
94            Err(ParseError::expecting_eof())
95        }
96    }
97}
98
99impl<Output: OutputBuf> Serializer<Output, ()> for super::Eof {
100    fn serialize_into(&self, _v: &(), _obuf: &mut Output) {
101        broadcast use crate::core::exec::output::outbuf_lemmas;
102
103    }
104}
105
106impl ByteLen<()> for super::Eof {
107    fn length(&self, _v: &()) -> (len: usize) {
108        0
109    }
110}
111
112impl Prepare<()> for super::Eof {
113    fn prepare(&self, _v: &()) -> (checked: Result<usize, PreSerializeError>) {
114        Ok(0)
115    }
116}
117
118impl<A, B, AVal, BVal> ByteLen<(AVal, BVal)> for super::PairRev<A, B> where
119    AVal: DeepView,
120    BVal: DeepView,
121    A: ByteLen<AVal>,
122    B: ByteLen<BVal>,
123 {
124    open spec fn exec_inv(&self) -> bool {
125        &&& self.0.exec_inv()
126        &&& self.1.exec_inv()
127    }
128
129    fn length(&self, v: &(AVal, BVal)) -> (len: usize) {
130        let la = self.1.length(&v.0);
131        let lb = self.0.length(&v.1);
132        proof {
133            assert((la + lb) as nat == la as nat + lb as nat);
134        }
135        la + lb
136    }
137}
138
139impl<A, B, AVal, BVal> Prepare<(AVal, BVal)> for super::PairRev<A, B> where
140    AVal: DeepView,
141    BVal: DeepView,
142    A: Prepare<AVal>,
143    B: Prepare<BVal>,
144 {
145    open spec fn exec_inv(&self) -> bool {
146        &&& self.0.exec_inv()
147        &&& self.1.exec_inv()
148    }
149
150    fn prepare(&self, v: &(AVal, BVal)) -> Result<usize, PreSerializeError> {
151        let la = self.1.prepare(&v.0)?;
152        let lb = self.0.prepare(&v.1)?;
153        if let Some(total) = la.checked_add(lb) {
154            Ok(total)
155        } else {
156            Err(PreSerializeError::length_too_large())
157        }
158    }
159}
160
161#[cfg(feature = "alloc")]
162impl<I, A> Parser<I> for super::RepeatTillEnd<A> where
163    I: InputBuf,
164    A: Parser<I> + SafeParser + Productive + Copy,
165 {
166    type PT = Vec<A::PT>;
167
168    fn min_byte_len(&self) -> usize {
169        // A repetition may be empty.
170        0
171    }
172
173    open spec fn exec_inv(&self) -> bool {
174        &&& self.0.exec_inv()
175        &&& self.0.safe_inv()
176        &&& self.0.productive_inv()
177    }
178
179    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
180        let (n, (r, _)) = Repeat(self.0, super::Eof).parse(ibuf)?;
181        Ok((n, r))
182    }
183}
184
185impl<I, A> Parser<I> for super::OptionalEnd<A> where I: InputBuf, A: Parser<I> + SafeParser {
186    type PT = Option<A::PT>;
187
188    fn min_byte_len(&self) -> usize {
189        // The inner format may be absent.
190        0
191    }
192
193    open spec fn exec_inv(&self) -> bool {
194        &&& self.0.exec_inv()
195        &&& self.0.safe_inv()
196    }
197
198    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
199        let (n, (r, _)) = Optional(&self.0, super::Eof).parse(ibuf)?;
200        Ok((n, r))
201    }
202}
203
204impl<Output: OutputBuf, A, T> Serializer<Output, &[T]> for super::RepeatTillEnd<A> where
205    A: Serializer<Output, T> + Copy,
206    T: DeepView,
207 {
208    #[verifier::prophetic]
209    open spec fn exec_inv(&self) -> bool {
210        self.0.exec_inv()
211    }
212
213    fn serialize_into(&self, v: &&[T], obuf: &mut Output) {
214        Star(self.0).serialize_into(v, obuf);
215    }
216}
217
218impl<A, T> ByteLen<&[T]> for super::RepeatTillEnd<A> where A: ByteLen<T> + Copy, T: DeepView {
219    open spec fn exec_inv(&self) -> bool {
220        self.0.exec_inv()
221    }
222
223    fn length(&self, v: &&[T]) -> (len: usize) {
224        Star(self.0).length(v)
225    }
226}
227
228impl<A, T> Prepare<&[T]> for super::RepeatTillEnd<A> where A: Prepare<T> + Copy, T: DeepView {
229    open spec fn exec_inv(&self) -> bool {
230        self.0.exec_inv()
231    }
232
233    fn prepare(&self, v: &&[T]) -> Result<usize, PreSerializeError> {
234        Star(self.0).prepare(v)
235    }
236}
237
238#[cfg(feature = "alloc")]
239impl<Output: OutputBuf, A, T> Serializer<Output, Vec<T>> for super::RepeatTillEnd<A> where
240    A: Serializer<Output, T> + Copy,
241    T: DeepView,
242 {
243    #[verifier::prophetic]
244    open spec fn exec_inv(&self) -> bool {
245        self.0.exec_inv()
246    }
247
248    fn serialize_into(&self, v: &Vec<T>, obuf: &mut Output) {
249        let values = v.as_slice();
250        proof {
251            assert(values.deep_view() == v.deep_view());
252        }
253        Star(self.0).serialize_into(&values, obuf);
254    }
255}
256
257#[cfg(feature = "alloc")]
258impl<A, T> ByteLen<Vec<T>> for super::RepeatTillEnd<A> where A: ByteLen<T> + Copy, T: DeepView {
259    open spec fn exec_inv(&self) -> bool {
260        self.0.exec_inv()
261    }
262
263    fn length(&self, v: &Vec<T>) -> (len: usize) {
264        let values = v.as_slice();
265        proof {
266            assert(values.deep_view() == v.deep_view());
267        }
268        Star(self.0).length(&values)
269    }
270}
271
272#[cfg(feature = "alloc")]
273impl<A, T> Prepare<Vec<T>> for super::RepeatTillEnd<A> where A: Prepare<T> + Copy, T: DeepView {
274    open spec fn exec_inv(&self) -> bool {
275        self.0.exec_inv()
276    }
277
278    fn prepare(&self, v: &Vec<T>) -> Result<usize, PreSerializeError> {
279        let values = v.as_slice();
280        proof {
281            assert(values.deep_view() == v.deep_view());
282        }
283        Star(self.0).prepare(&values)
284    }
285}
286
287impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for super::OptionalEnd<A> where
288    A: Serializer<Output, T>,
289    T: DeepView,
290 {
291    #[verifier::prophetic]
292    open spec fn exec_inv(&self) -> bool {
293        self.0.exec_inv()
294    }
295
296    fn serialize_into(&self, v: &Option<T>, obuf: &mut Output) {
297        Opt(&self.0).serialize_into(v, obuf);
298    }
299}
300
301impl<A, AST> ByteLen<Option<AST>> for super::OptionalEnd<A> where A: ByteLen<AST>, AST: DeepView {
302    open spec fn exec_inv(&self) -> bool {
303        self.0.exec_inv()
304    }
305
306    fn length(&self, v: &Option<AST>) -> (len: usize) {
307        Opt(&self.0).length(v)
308    }
309}
310
311impl<A, AST> Prepare<Option<AST>> for super::OptionalEnd<A> where A: Prepare<AST>, AST: DeepView {
312    open spec fn exec_inv(&self) -> bool {
313        self.0.exec_inv()
314    }
315
316    fn prepare(&self, v: &Option<AST>) -> Result<usize, PreSerializeError> {
317        Opt(&self.0).prepare(v)
318    }
319}
320
321} // verus!
vest_lib/combinators/tail/exec.rs

vest_lib/combinators/tail/
exec.rs
