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

vest_lib/combinators/refined/
exec.rs
