vest_lib/combinators/permute/
exec.rs

1//! Executable implementations for permutation formats.
2use crate::combinators::tuple::Pair;
3use crate::core::exec::output::OutputBuf;
4use crate::core::exec::parser::{PResult, Parser};
5use crate::core::exec::serializer::{ByteLen, PreSerializeError, Prepare, Serializer};
6use vstd::prelude::*;
7
8verus! {
9
10impl<I, P1, P2> Parser<I> for super::Permute2<P1, P2> where
11    I: crate::core::exec::input::InputBuf,
12    P1: Parser<I> + crate::core::spec::SafeParser,
13    P2: Parser<I> + crate::core::spec::SafeParser,
14 {
15    type PT = (P1::PT, P2::PT);
16
17    fn min_byte_len(&self) -> usize {
18        self.0.min_byte_len()
19            .saturating_add(self.1.min_byte_len())
20    }
21
22    open spec fn exec_inv(&self) -> bool {
23        &&& self.0.exec_inv()
24        &&& self.0.safe_inv()
25        &&& self.1.exec_inv()
26        &&& self.1.safe_inv()
27    }
28
29    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
30        // Mirrors the left-biased `Alt` in the spec: try the declared order, then the swap.
31        match Pair(&self.0, &self.1).parse(ibuf) {
32            Ok((n, v)) => Ok((n, v)),
33            Err(_) => match Pair(&self.1, &self.0).parse(ibuf) {
34                Ok((n, (v2, v1))) => Ok((n, (v1, v2))),
35                Err(e) => Err(e),
36            },
37        }
38    }
39}
40
41impl<Output: OutputBuf, P1, P2, T1, T2> Serializer<Output, (T1, T2)> for super::Permute2<
42    P1,
43    P2,
44> where T1: DeepView, T2: DeepView, P1: Serializer<Output, T1>, P2: Serializer<Output, T2> {
45    #[verifier::prophetic]
46    open spec fn exec_inv(&self) -> bool {
47        &&& self.0.exec_inv()
48        &&& self.1.exec_inv()
49    }
50
51    fn serialize_into(&self, v: &(T1, T2), obuf: &mut Output) {
52        // Serialization always emits the declared order.
53        Pair(&self.0, &self.1).serialize_into(v, obuf)
54    }
55}
56
57impl<P1, P2, T1, T2> ByteLen<(T1, T2)> for super::Permute2<P1, P2> where
58    T1: DeepView,
59    T2: DeepView,
60    P1: ByteLen<T1>,
61    P2: ByteLen<T2>,
62 {
63    open spec fn exec_inv(&self) -> bool {
64        &&& self.0.exec_inv()
65        &&& self.1.exec_inv()
66    }
67
68    fn length(&self, v: &(T1, T2)) -> (len: usize) {
69        Pair(&self.0, &self.1).length(v)
70    }
71}
72
73impl<P1, P2, T1, T2> Prepare<(T1, T2)> for super::Permute2<P1, P2> where
74    T1: DeepView,
75    T2: DeepView,
76    P1: Prepare<T1>,
77    P2: Prepare<T2>,
78 {
79    open spec fn exec_inv(&self) -> bool {
80        &&& self.0.exec_inv()
81        &&& self.1.exec_inv()
82    }
83
84    fn prepare(&self, v: &(T1, T2)) -> (checked: Result<usize, PreSerializeError>) {
85        Pair(&self.0, &self.1).prepare(v)
86    }
87}
88
89impl<I, A, B, C> Parser<I> for super::Permute3<A, B, C> where
90    I: crate::core::exec::input::InputBuf,
91    A: Parser<I> + crate::core::spec::SafeParser,
92    B: Parser<I> + crate::core::spec::SafeParser,
93    C: Parser<I> + crate::core::spec::SafeParser,
94 {
95    type PT = (A::PT, (B::PT, C::PT));
96
97    fn min_byte_len(&self) -> usize {
98        self.0.min_byte_len()
99            .saturating_add(self.1.min_byte_len())
100            .saturating_add(self.2.min_byte_len())
101    }
102
103    open spec fn exec_inv(&self) -> bool {
104        &&& self.0.exec_inv()
105        &&& self.0.safe_inv()
106        &&& self.1.exec_inv()
107        &&& self.1.safe_inv()
108        &&& self.2.exec_inv()
109        &&& self.2.safe_inv()
110    }
111
112    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
113        reveal(<super::Permute3<_, _, _> as crate::core::spec::SpecParser>::spec_parse);
114        match Pair(&self.0, super::Permute2(&self.1, &self.2)).parse(ibuf) {
115            Ok((n, v)) => Ok((n, v)),
116            Err(_) => match Pair(&self.1, super::Permute2(&self.0, &self.2)).parse(ibuf) {
117                Ok((n, (vb, (va, vc)))) => Ok((n, (va, (vb, vc)))),
118                Err(_) => match Pair(&self.2, super::Permute2(&self.0, &self.1)).parse(ibuf) {
119                    Ok((n, (vc, (va, vb)))) => Ok((n, (va, (vb, vc)))),
120                    Err(e) => Err(e),
121                },
122            },
123        }
124    }
125}
126
127impl<Output: OutputBuf, A, B, C, TA, TB, TC> Serializer<Output, (TA, (TB, TC))> for super::Permute3<
128    A,
129    B,
130    C,
131> where
132    TA: DeepView,
133    TB: DeepView,
134    TC: DeepView,
135    A: Serializer<Output, TA>,
136    B: Serializer<Output, TB>,
137    C: Serializer<Output, TC>,
138 {
139    #[verifier::prophetic]
140    open spec fn exec_inv(&self) -> bool {
141        &&& self.0.exec_inv()
142        &&& self.1.exec_inv()
143        &&& self.2.exec_inv()
144    }
145
146    fn serialize_into(&self, v: &(TA, (TB, TC)), obuf: &mut Output) {
147        Pair(&self.0, super::Permute2(&self.1, &self.2)).serialize_into(v, obuf)
148    }
149}
150
151impl<A, B, C, TA, TB, TC> ByteLen<(TA, (TB, TC))> for super::Permute3<A, B, C> where
152    TA: DeepView,
153    TB: DeepView,
154    TC: DeepView,
155    A: ByteLen<TA>,
156    B: ByteLen<TB>,
157    C: ByteLen<TC>,
158 {
159    open spec fn exec_inv(&self) -> bool {
160        &&& self.0.exec_inv()
161        &&& self.1.exec_inv()
162        &&& self.2.exec_inv()
163    }
164
165    fn length(&self, v: &(TA, (TB, TC))) -> (len: usize) {
166        Pair(&self.0, super::Permute2(&self.1, &self.2)).length(v)
167    }
168}
169
170impl<I, A, B, C, D> Parser<I> for super::Permute4<A, B, C, D> where
171    I: crate::core::exec::input::InputBuf,
172    A: Parser<I> + crate::core::spec::SafeParser,
173    B: Parser<I> + crate::core::spec::SafeParser,
174    C: Parser<I> + crate::core::spec::SafeParser,
175    D: Parser<I> + crate::core::spec::SafeParser,
176 {
177    type PT = (A::PT, (B::PT, (C::PT, D::PT)));
178
179    fn min_byte_len(&self) -> usize {
180        self.0.min_byte_len()
181            .saturating_add(self.1.min_byte_len())
182            .saturating_add(self.2.min_byte_len())
183            .saturating_add(self.3.min_byte_len())
184    }
185
186    open spec fn exec_inv(&self) -> bool {
187        &&& self.0.exec_inv()
188        &&& self.0.safe_inv()
189        &&& self.1.exec_inv()
190        &&& self.1.safe_inv()
191        &&& self.2.exec_inv()
192        &&& self.2.safe_inv()
193        &&& self.3.exec_inv()
194        &&& self.3.safe_inv()
195    }
196
197    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
198        reveal(<super::Permute4<_, _, _, _> as crate::core::spec::SpecParser>::spec_parse);
199        proof {
200            super::spec::lemma_permute3_spec_parse_ref(self.1, self.2, self.3);
201            super::spec::lemma_permute3_spec_parse_ref(self.0, self.2, self.3);
202            super::spec::lemma_permute3_spec_parse_ref(self.0, self.1, self.3);
203            super::spec::lemma_permute3_spec_parse_ref(self.0, self.1, self.2);
204        }
205        match Pair(&self.0, super::Permute3(&self.1, &self.2, &self.3)).parse(ibuf) {
206            Ok((n, v)) => Ok((n, v)),
207            Err(_) => match Pair(&self.1, super::Permute3(&self.0, &self.2, &self.3)).parse(ibuf) {
208                Ok((n, (vb, (va, (vc, vd))))) => Ok((n, (va, (vb, (vc, vd))))),
209                Err(_) => match Pair(&self.2, super::Permute3(&self.0, &self.1, &self.3)).parse(
210                    ibuf,
211                ) {
212                    Ok((n, (vc, (va, (vb, vd))))) => Ok((n, (va, (vb, (vc, vd))))),
213                    Err(_) => match Pair(&self.3, super::Permute3(&self.0, &self.1, &self.2)).parse(
214                        ibuf,
215                    ) {
216                        Ok((n, (vd, (va, (vb, vc))))) => Ok((n, (va, (vb, (vc, vd))))),
217                        Err(e) => Err(e),
218                    },
219                },
220            },
221        }
222    }
223}
224
225impl<Output: OutputBuf, A, B, C, D, TA, TB, TC, TD> Serializer<
226    Output,
227    (TA, (TB, (TC, TD))),
228> for super::Permute4<A, B, C, D> where
229    TA: DeepView,
230    TB: DeepView,
231    TC: DeepView,
232    TD: DeepView,
233    A: Serializer<Output, TA>,
234    B: Serializer<Output, TB>,
235    C: Serializer<Output, TC>,
236    D: Serializer<Output, TD>,
237 {
238    #[verifier::prophetic]
239    open spec fn exec_inv(&self) -> bool {
240        &&& self.0.exec_inv()
241        &&& self.1.exec_inv()
242        &&& self.2.exec_inv()
243        &&& self.3.exec_inv()
244    }
245
246    fn serialize_into(&self, v: &(TA, (TB, (TC, TD))), obuf: &mut Output) {
247        Pair(&self.0, super::Permute3(&self.1, &self.2, &self.3)).serialize_into(v, obuf)
248    }
249}
250
251impl<A, B, C, D, TA, TB, TC, TD> ByteLen<(TA, (TB, (TC, TD)))> for super::Permute4<
252    A,
253    B,
254    C,
255    D,
256> where
257    TA: DeepView,
258    TB: DeepView,
259    TC: DeepView,
260    TD: DeepView,
261    A: ByteLen<TA>,
262    B: ByteLen<TB>,
263    C: ByteLen<TC>,
264    D: ByteLen<TD>,
265 {
266    open spec fn exec_inv(&self) -> bool {
267        &&& self.0.exec_inv()
268        &&& self.1.exec_inv()
269        &&& self.2.exec_inv()
270        &&& self.3.exec_inv()
271    }
272
273    fn length(&self, v: &(TA, (TB, (TC, TD)))) -> (len: usize) {
274        Pair(&self.0, super::Permute3(&self.1, &self.2, &self.3)).length(v)
275    }
276}
277
278impl<A, B, C, TA, TB, TC> Prepare<(TA, (TB, TC))> for super::Permute3<A, B, C> where
279    TA: DeepView,
280    TB: DeepView,
281    TC: DeepView,
282    A: Prepare<TA>,
283    B: Prepare<TB>,
284    C: Prepare<TC>,
285 {
286    open spec fn exec_inv(&self) -> bool {
287        &&& self.0.exec_inv()
288        &&& self.1.exec_inv()
289        &&& self.2.exec_inv()
290    }
291
292    fn prepare(&self, v: &(TA, (TB, TC))) -> (checked: Result<usize, PreSerializeError>) {
293        Pair(&self.0, super::Permute2(&self.1, &self.2)).prepare(v)
294    }
295}
296
297impl<A, B, C, D, TA, TB, TC, TD> Prepare<(TA, (TB, (TC, TD)))> for super::Permute4<
298    A,
299    B,
300    C,
301    D,
302> where
303    TA: DeepView,
304    TB: DeepView,
305    TC: DeepView,
306    TD: DeepView,
307    A: Prepare<TA>,
308    B: Prepare<TB>,
309    C: Prepare<TC>,
310    D: Prepare<TD>,
311 {
312    open spec fn exec_inv(&self) -> bool {
313        &&& self.0.exec_inv()
314        &&& self.1.exec_inv()
315        &&& self.2.exec_inv()
316        &&& self.3.exec_inv()
317    }
318
319    fn prepare(&self, v: &(TA, (TB, (TC, TD)))) -> (checked: Result<usize, PreSerializeError>) {
320        Pair(&self.0, super::Permute3(&self.1, &self.2, &self.3)).prepare(v)
321    }
322}
323
324impl<I, A, B, C, D, E> Parser<I> for super::Permute5<A, B, C, D, E> where
325    I: crate::core::exec::input::InputBuf,
326    A: Parser<I> + crate::core::spec::SafeParser,
327    B: Parser<I> + crate::core::spec::SafeParser,
328    C: Parser<I> + crate::core::spec::SafeParser,
329    D: Parser<I> + crate::core::spec::SafeParser,
330    E: Parser<I> + crate::core::spec::SafeParser,
331{
332    type PT = (A::PT, (B::PT, (C::PT, (D::PT, E::PT))));
333
334    fn min_byte_len(&self) -> usize {
335        self.0.min_byte_len()
336            .saturating_add(self.1.min_byte_len())
337            .saturating_add(self.2.min_byte_len())
338            .saturating_add(self.3.min_byte_len())
339            .saturating_add(self.4.min_byte_len())
340    }
341
342    open spec fn exec_inv(&self) -> bool {
343        &&& self.0.exec_inv()
344        &&& self.0.safe_inv()
345        &&& self.1.exec_inv()
346        &&& self.1.safe_inv()
347        &&& self.2.exec_inv()
348        &&& self.2.safe_inv()
349        &&& self.3.exec_inv()
350        &&& self.3.safe_inv()
351        &&& self.4.exec_inv()
352        &&& self.4.safe_inv()
353    }
354
355    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
356        proof {
357            super::spec::lemma_permute4_spec_parse_ref(self.1, self.2, self.3, self.4);
358            super::spec::lemma_permute4_spec_parse_ref(self.0, self.2, self.3, self.4);
359            super::spec::lemma_permute4_spec_parse_ref(self.0, self.1, self.3, self.4);
360            super::spec::lemma_permute4_spec_parse_ref(self.0, self.1, self.2, self.4);
361            super::spec::lemma_permute4_spec_parse_ref(self.0, self.1, self.2, self.3);
362        }
363        match Pair(&self.0, super::Permute4(&self.1, &self.2, &self.3, &self.4)).parse(ibuf) {
364            Ok((n, v)) => Ok((n, v)),
365            Err(_) => match Pair(&self.1, super::Permute4(&self.0, &self.2, &self.3, &self.4)).parse(ibuf) {
366                Ok((n, (vb, (va, (vc, (vd, ve)))))) => Ok((n, (va, (vb, (vc, (vd, ve)))))),
367                Err(_) => match Pair(&self.2, super::Permute4(&self.0, &self.1, &self.3, &self.4)).parse(
368                    ibuf,
369                ) {
370                    Ok((n, (vc, (va, (vb, (vd, ve)))))) => Ok((n, (va, (vb, (vc, (vd, ve)))))),
371                    Err(_) => match Pair(&self.3, super::Permute4(&self.0, &self.1, &self.2, &self.4)).parse(
372                        ibuf,
373                    ) {
374                        Ok((n, (vd, (va, (vb, (vc, ve)))))) => Ok((n, (va, (vb, (vc, (vd, ve)))))),
375                        Err(_) => match Pair(&self.4, super::Permute4(&self.0, &self.1, &self.2, &self.3)).parse(
376                            ibuf,
377                        ) {
378                            Ok((n, (ve, (va, (vb, (vc, vd)))))) => Ok((n, (va, (vb, (vc, (vd, ve)))))),
379                            Err(e) => Err(e),
380                        },
381                    },
382                },
383            },
384        }
385    }
386}
387
388impl<Output: OutputBuf, A, B, C, D, E, TA, TB, TC, TD, TE> Serializer<
389    Output,
390    (TA, (TB, (TC, (TD, TE)))),
391> for super::Permute5<A, B, C, D, E> where
392    TA: DeepView,
393    TB: DeepView,
394    TC: DeepView,
395    TD: DeepView,
396    TE: DeepView,
397    A: Serializer<Output, TA>,
398    B: Serializer<Output, TB>,
399    C: Serializer<Output, TC>,
400    D: Serializer<Output, TD>,
401    E: Serializer<Output, TE>,
402{
403    #[verifier::prophetic]
404    open spec fn exec_inv(&self) -> bool {
405        &&& self.0.exec_inv()
406        &&& self.1.exec_inv()
407        &&& self.2.exec_inv()
408        &&& self.3.exec_inv()
409        &&& self.4.exec_inv()
410    }
411
412    fn serialize_into(&self, v: &(TA, (TB, (TC, (TD, TE)))), obuf: &mut Output) {
413        Pair(&self.0, super::Permute4(&self.1, &self.2, &self.3, &self.4)).serialize_into(v, obuf)
414    }
415}
416
417impl<A, B, C, D, E, TA, TB, TC, TD, TE> ByteLen<(TA, (TB, (TC, (TD, TE))))> for super::Permute5<
418    A,
419    B,
420    C,
421    D,
422    E,
423> where
424    TA: DeepView,
425    TB: DeepView,
426    TC: DeepView,
427    TD: DeepView,
428    TE: DeepView,
429    A: ByteLen<TA>,
430    B: ByteLen<TB>,
431    C: ByteLen<TC>,
432    D: ByteLen<TD>,
433    E: ByteLen<TE>,
434{
435    open spec fn exec_inv(&self) -> bool {
436        &&& self.0.exec_inv()
437        &&& self.1.exec_inv()
438        &&& self.2.exec_inv()
439        &&& self.3.exec_inv()
440        &&& self.4.exec_inv()
441    }
442
443    fn length(&self, v: &(TA, (TB, (TC, (TD, TE))))) -> (len: usize) {
444        Pair(&self.0, super::Permute4(&self.1, &self.2, &self.3, &self.4)).length(v)
445    }
446}
447
448impl<A, B, C, D, E, TA, TB, TC, TD, TE> Prepare<(TA, (TB, (TC, (TD, TE))))> for super::Permute5<
449    A,
450    B,
451    C,
452    D,
453    E,
454> where
455    TA: DeepView,
456    TB: DeepView,
457    TC: DeepView,
458    TD: DeepView,
459    TE: DeepView,
460    A: Prepare<TA>,
461    B: Prepare<TB>,
462    C: Prepare<TC>,
463    D: Prepare<TD>,
464    E: Prepare<TE>,
465{
466    open spec fn exec_inv(&self) -> bool {
467        &&& self.0.exec_inv()
468        &&& self.1.exec_inv()
469        &&& self.2.exec_inv()
470        &&& self.3.exec_inv()
471        &&& self.4.exec_inv()
472    }
473
474    fn prepare(&self, v: &(TA, (TB, (TC, (TD, TE))))) -> (checked: Result<usize, PreSerializeError>) {
475        Pair(&self.0, super::Permute4(&self.1, &self.2, &self.3, &self.4)).prepare(v)
476    }
477}
478
479} // verus!
vest_lib/combinators/permute/exec.rs

vest_lib/combinators/permute/
exec.rs
