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

vest_lib/combinators/permute/
exec.rs
