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

vest_lib/combinators/tail/
exec.rs
