vest_lib/combinators/refined/
exec.rs

1//! Executable predicates and refined-format implementations.
2use crate::combinators::{Fixed, Preceded, Terminated};
3use crate::core::exec::bytes_eq;
4use crate::core::exec::input::InputBuf;
5use crate::core::exec::output::*;
6use crate::core::{
7    exec::{
8        fns::Pred,
9        input::InputSlice,
10        parser::{PResult, Parser},
11        serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
12        ParseError,
13    },
14    spec::{Consistency, SafeParser, SoundParser, SpecByteLen, SpecParser, SpecPred},
15};
16use vstd::prelude::*;
17use OutputBuf;
18
19verus! {
20
21impl<I, A, PredFn> Parser<I> for super::Refined<A, PredFn> where
22    I: View<V = Seq<u8>>,
23    A: Parser<I>,
24    PredFn: Pred<A::PT>,
25 {
26    type PT = A::PT;
27
28    open spec fn exec_inv(&self) -> bool {
29        self.0.exec_inv()
30    }
31
32    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
33        let (n, v) = self.0.parse(ibuf)?;
34        if self.1.test(&v) {
35            Ok((n, v))
36        } else {
37            Err(ParseError::predicate_failed())
38        }
39    }
40}
41
42impl<Output: OutputBuf, A, PredFn, T> Serializer<Output, T> for super::Refined<A, PredFn> where
43    T: DeepView,
44    A: Serializer<Output, T>,
45    PredFn: SpecPred<T::V>,
46 {
47    #[verifier::prophetic]
48    open spec fn exec_inv(&self) -> bool {
49        self.0.exec_inv()
50    }
51
52    fn serialize_into(&self, v: &T, obuf: &mut Output) {
53        self.0.serialize_into(v, obuf);
54    }
55}
56
57impl<A, PredFn, T> ByteLen<T> for super::Refined<A, PredFn> where
58    T: DeepView,
59    A: ByteLen<T>,
60    PredFn: Pred<T>,
61 {
62    open spec fn exec_inv(&self) -> bool {
63        self.0.exec_inv()
64    }
65
66    fn length(&self, v: &T) -> (len: usize) {
67        self.0.length(v)
68    }
69}
70
71impl<A, PredFn, T> Prepare<T> for super::Refined<A, PredFn> where
72    T: DeepView,
73    A: Prepare<T>,
74    PredFn: Pred<T>,
75 {
76    open spec fn exec_inv(&self) -> bool {
77        self.0.exec_inv()
78    }
79
80    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
81        if self.1.test(v) {
82            self.0.prepare(v)
83        } else {
84            Err(PreSerializeError::not_compliant(ComplianceErrorKind::PredicateFailed))
85        }
86    }
87}
88
89impl<I, Inner, T> Parser<I> for super::Const<Inner, T> where
90    I: InputBuf,
91    Inner: Parser<I, PT = T, PVal = T>,
92    T: DeepView<V = T> + PartialEq + Structural,
93 {
94    type PT = Inner::PVal;
95
96    open spec fn exec_inv(&self) -> bool {
97        &&& self.0.exec_inv()
98        &&& forall|v: Inner::PVal| v.deep_view() == v
99    }
100
101    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
102        let (n, v) = self.0.parse(ibuf)?;
103        if v == self.1 {
104            Ok((n, v))
105        } else {
106            Err(ParseError::invalid_tag())
107        }
108    }
109}
110
111impl<Output: OutputBuf, Inner, T> Serializer<Output, T> for super::Const<Inner, T> where
112    T: DeepView<V = T>,
113    Inner: Serializer<Output, T>,
114 {
115    #[verifier::prophetic]
116    open spec fn exec_inv(&self) -> bool {
117        self.0.exec_inv()
118    }
119
120    fn serialize_into(&self, v: &T, obuf: &mut Output) {
121        self.0.serialize_into(v, obuf);
122    }
123}
124
125impl<Inner, V, T> ByteLen<T> for super::Const<Inner, V> where
126    T: DeepView<V = V>,
127    Inner: SpecByteLen<T = V> + ByteLen<T>,
128 {
129    open spec fn exec_inv(&self) -> bool {
130        self.0.exec_inv()
131    }
132
133    fn length(&self, v: &T) -> (len: usize) {
134        self.0.length(v)
135    }
136}
137
138impl<Inner, T> Prepare<T> for super::Const<Inner, T> where
139    T: DeepView<V = T> + PartialEq + Structural,
140    Inner: Prepare<T>,
141 {
142    open spec fn exec_inv(&self) -> bool {
143        &&& self.0.exec_inv()
144        &&& forall|v: T| v.deep_view() == v
145    }
146
147    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
148        if v == &self.1 {
149            self.0.prepare(v)
150        } else {
151            Err(PreSerializeError::not_compliant(ComplianceErrorKind::InvalidTag))
152        }
153    }
154}
155
156impl<const N: usize> ByteLen<[u8; N]> for super::Const<Fixed<N>, [u8; N]> {
157    open spec fn exec_inv(&self) -> bool {
158        true
159    }
160
161    fn length(&self, _v: &[u8; N]) -> (len: usize) {
162        N
163    }
164}
165
166impl<const N: usize> Prepare<[u8; N]> for super::Const<Fixed<N>, [u8; N]> {
167    fn prepare(&self, v: &[u8; N]) -> (checked: Result<usize, PreSerializeError>) {
168        let v_slice = v.as_slice();
169        let tag_slice = self.1.as_slice();
170        let eq = bytes_eq(v_slice, tag_slice);
171        proof {
172            assert(v_slice.deep_view() == v.deep_view());
173            assert(tag_slice.deep_view() == self.1@);
174            assert(eq == (v.deep_view() == self.1@));
175        }
176        if eq {
177            Ok(N)
178        } else {
179            Err(PreSerializeError::not_compliant(ComplianceErrorKind::InvalidTag))
180        }
181    }
182}
183
184// pub assume_specification<const N: usize>[ <[u8; N] as PartialEq<&[u8]>>::eq ](
185//     x: &[u8; N],
186//     y: &&[u8],
187// ) -> (is_eq: bool)
188//     ensures
189//         is_eq == (x@ == y@),
190// ;
191// pub assume_specification<'a, T, U, const N: usize>[ <[T; N] as core::cmp::PartialEq<&[U]>>::eq ](
192//     a: &[T; N],
193//     b: &&[U],
194// ) -> (r: bool) where T: core::cmp::PartialEq<U>
195// // , T: DeepView, U: DeepView<V = T::V>,
196//     // ensures
197//     //     // r == (a@ == b@),
198//     //     r == (a.deep_view() == b.deep_view()),
199// ;
200impl<const N: usize> Parser<&[u8]> for super::Const<Fixed<N>, [u8; N]> {
201    type PT = [u8; N];
202
203    fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT> {
204        let (n, v) = self.0.parse(ibuf)?;
205        let tag = self.1.as_slice();
206        proof {
207            self.0.lemma_parse_sound_consumption(ibuf@);
208            assert(v.len() == N);
209            assert(tag.len() == N);
210            v.deep_view_eq_view();
211            tag.deep_view_eq_view();
212        }
213        if bytes_eq(tag, v) {
214            Ok((n, self.1))
215        } else {
216            Err(ParseError::invalid_tag())
217        }
218    }
219}
220
221impl<I, Tg, TagVal, Of> Parser<I> for super::PrefixTagged<Tg, TagVal, Of> where
222    I: InputBuf,
223    Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser,
224    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
225    Of: Parser<I> + SafeParser,
226 {
227    type PT = Of::PT;
228
229    open spec fn exec_inv(&self) -> bool {
230        Preceded::<_, _, _, false> {
231            a: super::Const(&self.0, self.1),
232            b: &self.2,
233            a_val: self.1,
234        }.exec_inv()
235    }
236
237    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
238        let fmt = Preceded::<_, _, _, false> {
239            a: super::Const(&self.0, self.1),
240            b: &self.2,
241            a_val: self.1,
242        };
243        fmt.parse(ibuf)
244    }
245}
246
247impl<Output: OutputBuf, Tg, TagVal, Of, T> Serializer<Output, T> for super::PrefixTagged<
248    Tg,
249    TagVal,
250    Of,
251> where
252    Tg: SpecByteLen<T = TagVal> + Serializer<Output, TagVal>,
253    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
254    T: DeepView,
255    Of: Serializer<Output, T>,
256 {
257    #[verifier::prophetic]
258    open spec fn exec_inv(&self) -> bool {
259        &&& self.0.exec_inv()
260        &&& self.2.exec_inv()
261        &&& forall|v: Tg::T| v.deep_view() == v
262    }
263
264    fn serialize_into(&self, v: &T, obuf: &mut Output) {
265        let fmt = Preceded::<_, _, _, false> {
266            a: super::Const(&self.0, self.1),
267            b: &self.2,
268            a_val: self.1,
269        };
270        fmt.serialize_into(v, obuf);
271    }
272}
273
274impl<Tg, TagVal, Of, T> ByteLen<T> for super::PrefixTagged<Tg, TagVal, Of> where
275    Tg: SpecByteLen<T = TagVal> + ByteLen<TagVal>,
276    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
277    T: DeepView,
278    Of: ByteLen<T>,
279 {
280    open spec fn exec_inv(&self) -> bool {
281        &&& self.0.exec_inv()
282        &&& self.2.exec_inv()
283        &&& forall|v: TagVal| v.deep_view() == v
284    }
285
286    fn length(&self, v: &T) -> (len: usize) {
287        let fmt = Preceded::<_, _, _, false> {
288            a: super::Const(&self.0, self.1),
289            b: &self.2,
290            a_val: self.1,
291        };
292        fmt.length(v)
293    }
294}
295
296impl<Tg, TagVal, Of, T> Prepare<T> for super::PrefixTagged<Tg, TagVal, Of> where
297    Tg: SpecByteLen<T = TagVal> + Prepare<TagVal>,
298    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
299    T: DeepView,
300    Of: Prepare<T>,
301 {
302    open spec fn exec_inv(&self) -> bool {
303        &&& self.0.exec_inv()
304        &&& self.2.exec_inv()
305        &&& forall|v: TagVal| v.deep_view() == v
306    }
307
308    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
309        let fmt = Preceded::<_, _, _, false> {
310            a: super::Const(&self.0, self.1),
311            b: &self.2,
312            a_val: self.1,
313        };
314        fmt.prepare(v)
315    }
316}
317
318impl<I, Of, Tg, TagVal> Parser<I> for super::SuffixTagged<Of, Tg, TagVal> where
319    I: InputBuf,
320    Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser,
321    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
322    Of: Parser<I> + SafeParser,
323 {
324    type PT = Of::PT;
325
326    open spec fn exec_inv(&self) -> bool {
327        Terminated::<_, _, _, false> {
328            a: &self.0,
329            b: super::Const(&self.1, self.2),
330            b_val: self.2,
331        }.exec_inv()
332    }
333
334    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
335        let fmt = Terminated::<_, _, _, false> {
336            a: &self.0,
337            b: super::Const(&self.1, self.2),
338            b_val: self.2,
339        };
340        fmt.parse(ibuf)
341    }
342}
343
344impl<Output: OutputBuf, Of, Tg, TagVal, T> Serializer<Output, T> for super::SuffixTagged<
345    Of,
346    Tg,
347    TagVal,
348> where
349    Tg: SpecByteLen<T = TagVal> + Serializer<Output, TagVal>,
350    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
351    T: DeepView,
352    Of: Serializer<Output, T>,
353 {
354    #[verifier::prophetic]
355    open spec fn exec_inv(&self) -> bool {
356        &&& self.0.exec_inv()
357        &&& self.1.exec_inv()
358        &&& forall|v: TagVal| v.deep_view() == v
359    }
360
361    fn serialize_into(&self, v: &T, obuf: &mut Output) {
362        let fmt = Terminated::<_, _, _, false> {
363            a: &self.0,
364            b: super::Const(&self.1, self.2),
365            b_val: self.2,
366        };
367        fmt.serialize_into(v, obuf);
368    }
369}
370
371impl<Of, TagVal, Tg, T> ByteLen<T> for super::SuffixTagged<Of, Tg, TagVal> where
372    Tg: SpecByteLen<T = TagVal> + ByteLen<TagVal>,
373    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
374    T: DeepView,
375    Of: ByteLen<T>,
376 {
377    open spec fn exec_inv(&self) -> bool {
378        &&& self.0.exec_inv()
379        &&& self.1.exec_inv()
380        &&& forall|v: TagVal| v.deep_view() == v
381    }
382
383    fn length(&self, v: &T) -> (len: usize) {
384        let fmt = Terminated::<_, _, _, false> {
385            a: &self.0,
386            b: super::Const(&self.1, self.2),
387            b_val: self.2,
388        };
389        fmt.length(v)
390    }
391}
392
393impl<Of, TagVal, Tg, T> Prepare<T> for super::SuffixTagged<Of, Tg, TagVal> where
394    Tg: SpecByteLen<T = TagVal> + Prepare<TagVal>,
395    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
396    T: DeepView,
397    Of: Prepare<T>,
398 {
399    open spec fn exec_inv(&self) -> bool {
400        &&& self.0.exec_inv()
401        &&& self.1.exec_inv()
402        &&& forall|v: TagVal| v.deep_view() == v
403    }
404
405    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
406        let fmt = Terminated::<_, _, _, false> {
407            a: &self.0,
408            b: super::Const(&self.1, self.2),
409            b_val: self.2,
410        };
411        fmt.prepare(v)
412    }
413}
414
415} // verus!
vest_lib/combinators/refined/exec.rs

vest_lib/combinators/refined/
exec.rs
