vest_lib/combinators/permute/
proof.rs

1//! Correctness and malleability proofs for permutation formats.
2use crate::combinators::choice::Alt;
3use crate::combinators::tuple::Pair;
4use crate::combinators::Mapped;
5use crate::core::{proof::*, spec::*};
6use vstd::prelude::*;
7
8verus! {
9
10// ============================================================================
11// Permute2
12// ============================================================================
13impl<P1: SafeParser, P2: SafeParser> SafeParser for super::Permute2<P1, P2> {
14    open spec fn safe_inv(&self) -> bool {
15        &&& self.0.safe_inv()
16        &&& self.1.safe_inv()
17    }
18
19    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
20        Alt::<_, _, false>(
21            Pair(self.0, self.1),
22            Mapped { inner: Pair(self.1, self.0), mapper: |i| super::swap2(i) },
23        ).lemma_parse_safe(ibuf);
24    }
25}
26
27impl<P1: Productive, P2: Productive> Productive for super::Permute2<P1, P2> {
28    open spec fn productive_inv(&self) -> bool {
29        &&& self.0.productive_inv()
30        &&& self.1.productive_inv()
31    }
32
33    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
34        Alt::<_, _, false>(
35            Pair(self.0, self.1),
36            Mapped { inner: Pair(self.1, self.0), mapper: |i| super::swap2(i) },
37        ).lemma_productive(ibuf);
38    }
39}
40
41// `NoLookAhead` is deliberately not implemented.
42
43impl<P1: SoundParser, P2: SoundParser> SoundParser for super::Permute2<P1, P2> {
44    open spec fn sound_inv(&self) -> bool {
45        &&& self.0.sound_inv()
46        &&& self.1.sound_inv()
47    }
48
49    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
50        let canonical = Pair(self.0, self.1);
51        let swapped = Pair(self.1, self.0);
52        canonical.lemma_parse_sound_consumption(ibuf);
53        swapped.lemma_parse_sound_consumption(ibuf);
54        // Either the declared order matched, in which case the length claim is `Pair`'s, or the
55        // swapped order matched and the two length sums agree by commutativity of `nat` addition.
56        if canonical.spec_parse(ibuf) is None {
57            if let Some((_n, iv)) = swapped.spec_parse(ibuf) {
58                assert(self.byte_len(super::swap2(iv)) == swapped.byte_len(iv));
59            }
60        }
61    }
62
63    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
64        let canonical = Pair(self.0, self.1);
65        let swapped = Pair(self.1, self.0);
66        canonical.lemma_parse_sound_value(ibuf);
67        swapped.lemma_parse_sound_value(ibuf);
68        // Both branches establish the same conjunction of component consistencies, just reordered.
69        if canonical.spec_parse(ibuf) is None {
70            if let Some((_n, iv)) = swapped.spec_parse(ibuf) {
71                assert(self.consistent(super::swap2(iv)));
72            }
73        }
74    }
75}
76
77impl<P1, P2> SPRoundTripDps for super::Permute2<P1, P2> where
78    P1: SPRoundTripDps + NonTailFmt,
79    P2: SPRoundTripDps,
80 {
81    open spec fn unambiguous(&self) -> bool {
82        &&& self.0.unambiguous()
83        &&& self.1.unambiguous()
84        &&& self.0.serialize_dps_inv()
85    }
86
87    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
88        let canonical = Pair(self.0, self.1);
89        canonical.theorem_serialize_dps_parse_roundtrip(v, obuf);
90    }
91}
92
93impl<P1, P2> EquivSerializersGeneral for super::Permute2<P1, P2> where
94    P1: EquivSerializersGeneral,
95    P2: EquivSerializersGeneral,
96 {
97    open spec fn equiv_general_inv(&self) -> bool {
98        &&& self.0.equiv_general_inv()
99        &&& self.1.equiv_general_inv()
100    }
101
102    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
103        Pair(self.0, self.1).lemma_serialize_equiv(v, obuf);
104    }
105}
106
107impl<P1, P2> EquivSerializers for super::Permute2<P1, P2> where
108    P1: EquivSerializersGeneral,
109    P2: EquivSerializers,
110 {
111    open spec fn equiv_inv(&self) -> bool {
112        &&& self.0.equiv_general_inv()
113        &&& self.1.equiv_inv()
114    }
115
116    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
117        Pair(self.0, self.1).lemma_serialize_equiv_on_empty(v);
118    }
119}
120
121// ============================================================================
122// Permute3
123// ============================================================================
124impl<A: SafeParser, B: SafeParser, C: SafeParser> SafeParser for super::Permute3<A, B, C> {
125    open spec fn safe_inv(&self) -> bool {
126        &&& self.0.safe_inv()
127        &&& self.1.safe_inv()
128        &&& self.2.safe_inv()
129    }
130
131    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
132        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
133        Alt::<_, _, false>(
134            Pair(self.0, super::Permute2(self.1, self.2)),
135            Alt::<_, _, false>(
136                Mapped {
137                    inner: Pair(self.1, super::Permute2(self.0, self.2)),
138                    mapper: |i| super::swap3_1(i),
139                },
140                Mapped {
141                    inner: Pair(self.2, super::Permute2(self.0, self.1)),
142                    mapper: |i| super::swap3_2(i),
143                },
144            ),
145        ).lemma_parse_safe(ibuf);
146    }
147}
148
149impl<A: Productive, B: Productive, C: Productive> Productive for super::Permute3<A, B, C> {
150    open spec fn productive_inv(&self) -> bool {
151        &&& self.0.productive_inv()
152        &&& self.1.productive_inv()
153        &&& self.2.productive_inv()
154    }
155
156    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
157        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
158        Alt::<_, _, false>(
159            Pair(self.0, super::Permute2(self.1, self.2)),
160            Alt::<_, _, false>(
161                Mapped {
162                    inner: Pair(self.1, super::Permute2(self.0, self.2)),
163                    mapper: |i| super::swap3_1(i),
164                },
165                Mapped {
166                    inner: Pair(self.2, super::Permute2(self.0, self.1)),
167                    mapper: |i| super::swap3_2(i),
168                },
169            ),
170        ).lemma_productive(ibuf);
171    }
172}
173
174impl<A: SoundParser, B: SoundParser, C: SoundParser> SoundParser for super::Permute3<A, B, C> {
175    open spec fn sound_inv(&self) -> bool {
176        &&& self.0.sound_inv()
177        &&& self.1.sound_inv()
178        &&& self.2.sound_inv()
179    }
180
181    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
182        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
183        let b0 = Pair(self.0, super::Permute2(self.1, self.2));
184        let b1 = Pair(self.1, super::Permute2(self.0, self.2));
185        let b2 = Pair(self.2, super::Permute2(self.0, self.1));
186        b0.lemma_parse_sound_consumption(ibuf);
187        b1.lemma_parse_sound_consumption(ibuf);
188        b2.lemma_parse_sound_consumption(ibuf);
189        if b0.spec_parse(ibuf) is None {
190            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
191                assert(self.byte_len(super::swap3_1(iv)) == b1.byte_len(iv));
192            }
193            if b1.spec_parse(ibuf) is None {
194                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
195                    assert(self.byte_len(super::swap3_2(iv)) == b2.byte_len(iv));
196                }
197            }
198        }
199    }
200
201    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
202        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
203        let b0 = Pair(self.0, super::Permute2(self.1, self.2));
204        let b1 = Pair(self.1, super::Permute2(self.0, self.2));
205        let b2 = Pair(self.2, super::Permute2(self.0, self.1));
206        b0.lemma_parse_sound_value(ibuf);
207        b1.lemma_parse_sound_value(ibuf);
208        b2.lemma_parse_sound_value(ibuf);
209        if b0.spec_parse(ibuf) is None {
210            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
211                assert(self.consistent(super::swap3_1(iv)));
212            }
213            if b1.spec_parse(ibuf) is None {
214                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
215                    assert(self.consistent(super::swap3_2(iv)));
216                }
217            }
218        }
219    }
220}
221
222impl<A, B, C> SPRoundTripDps for super::Permute3<A, B, C> where
223    A: SPRoundTripDps + NonTailFmt,
224    B: SPRoundTripDps + NonTailFmt,
225    C: SPRoundTripDps,
226 {
227    open spec fn unambiguous(&self) -> bool {
228        &&& self.0.unambiguous()
229        &&& self.1.unambiguous()
230        &&& self.2.unambiguous()
231        &&& self.0.serialize_dps_inv()
232        &&& self.1.serialize_dps_inv()
233    }
234
235    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
236        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
237        Pair(self.0, super::Permute2(self.1, self.2)).theorem_serialize_dps_parse_roundtrip(
238            v,
239            obuf,
240        );
241    }
242}
243
244impl<A, B, C> EquivSerializersGeneral for super::Permute3<A, B, C> where
245    A: EquivSerializersGeneral,
246    B: EquivSerializersGeneral,
247    C: EquivSerializersGeneral,
248 {
249    open spec fn equiv_general_inv(&self) -> bool {
250        &&& self.0.equiv_general_inv()
251        &&& self.1.equiv_general_inv()
252        &&& self.2.equiv_general_inv()
253    }
254
255    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
256        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
257        Pair(self.0, super::Permute2(self.1, self.2)).lemma_serialize_equiv(v, obuf);
258    }
259}
260
261impl<A, B, C> EquivSerializers for super::Permute3<A, B, C> where
262    A: EquivSerializersGeneral,
263    B: EquivSerializersGeneral,
264    C: EquivSerializers,
265 {
266    open spec fn equiv_inv(&self) -> bool {
267        &&& self.0.equiv_general_inv()
268        &&& self.1.equiv_general_inv()
269        &&& self.2.equiv_inv()
270    }
271
272    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
273        reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
274        Pair(self.0, super::Permute2(self.1, self.2)).lemma_serialize_equiv_on_empty(v);
275    }
276}
277
278// ============================================================================
279// Permute4
280// ============================================================================
281impl<A: SafeParser, B: SafeParser, C: SafeParser, D: SafeParser> SafeParser for super::Permute4<
282    A,
283    B,
284    C,
285    D,
286> {
287    open spec fn safe_inv(&self) -> bool {
288        &&& self.0.safe_inv()
289        &&& self.1.safe_inv()
290        &&& self.2.safe_inv()
291        &&& self.3.safe_inv()
292    }
293
294    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
295        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
296        Alt::<_, _, false>(
297            Pair(self.0, super::Permute3(self.1, self.2, self.3)),
298            Alt::<_, _, false>(
299                Mapped {
300                    inner: Pair(self.1, super::Permute3(self.0, self.2, self.3)),
301                    mapper: |i| super::swap4_1(i),
302                },
303                Alt::<_, _, false>(
304                    Mapped {
305                        inner: Pair(self.2, super::Permute3(self.0, self.1, self.3)),
306                        mapper: |i| super::swap4_2(i),
307                    },
308                    Mapped {
309                        inner: Pair(self.3, super::Permute3(self.0, self.1, self.2)),
310                        mapper: |i| super::swap4_3(i),
311                    },
312                ),
313            ),
314        ).lemma_parse_safe(ibuf);
315    }
316}
317
318impl<A: Productive, B: Productive, C: Productive, D: Productive> Productive for super::Permute4<
319    A,
320    B,
321    C,
322    D,
323> {
324    open spec fn productive_inv(&self) -> bool {
325        &&& self.0.productive_inv()
326        &&& self.1.productive_inv()
327        &&& self.2.productive_inv()
328        &&& self.3.productive_inv()
329    }
330
331    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
332        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
333        Alt::<_, _, false>(
334            Pair(self.0, super::Permute3(self.1, self.2, self.3)),
335            Alt::<_, _, false>(
336                Mapped {
337                    inner: Pair(self.1, super::Permute3(self.0, self.2, self.3)),
338                    mapper: |i| super::swap4_1(i),
339                },
340                Alt::<_, _, false>(
341                    Mapped {
342                        inner: Pair(self.2, super::Permute3(self.0, self.1, self.3)),
343                        mapper: |i| super::swap4_2(i),
344                    },
345                    Mapped {
346                        inner: Pair(self.3, super::Permute3(self.0, self.1, self.2)),
347                        mapper: |i| super::swap4_3(i),
348                    },
349                ),
350            ),
351        ).lemma_productive(ibuf);
352    }
353}
354
355impl<
356    A: SoundParser,
357    B: SoundParser,
358    C: SoundParser,
359    D: SoundParser,
360> SoundParser for super::Permute4<A, B, C, D> {
361    open spec fn sound_inv(&self) -> bool {
362        &&& self.0.sound_inv()
363        &&& self.1.sound_inv()
364        &&& self.2.sound_inv()
365        &&& self.3.sound_inv()
366    }
367
368    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
369        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
370        let b0 = Pair(self.0, super::Permute3(self.1, self.2, self.3));
371        let b1 = Pair(self.1, super::Permute3(self.0, self.2, self.3));
372        let b2 = Pair(self.2, super::Permute3(self.0, self.1, self.3));
373        let b3 = Pair(self.3, super::Permute3(self.0, self.1, self.2));
374        b0.lemma_parse_sound_consumption(ibuf);
375        b1.lemma_parse_sound_consumption(ibuf);
376        b2.lemma_parse_sound_consumption(ibuf);
377        b3.lemma_parse_sound_consumption(ibuf);
378        if b0.spec_parse(ibuf) is None {
379            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
380                assert(self.byte_len(super::swap4_1(iv)) == b1.byte_len(iv));
381            }
382            if b1.spec_parse(ibuf) is None {
383                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
384                    assert(self.byte_len(super::swap4_2(iv)) == b2.byte_len(iv));
385                }
386                if b2.spec_parse(ibuf) is None {
387                    if let Some((_n, iv)) = b3.spec_parse(ibuf) {
388                        assert(self.byte_len(super::swap4_3(iv)) == b3.byte_len(iv));
389                    }
390                }
391            }
392        }
393    }
394
395    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
396        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
397        let b0 = Pair(self.0, super::Permute3(self.1, self.2, self.3));
398        let b1 = Pair(self.1, super::Permute3(self.0, self.2, self.3));
399        let b2 = Pair(self.2, super::Permute3(self.0, self.1, self.3));
400        let b3 = Pair(self.3, super::Permute3(self.0, self.1, self.2));
401        b0.lemma_parse_sound_value(ibuf);
402        b1.lemma_parse_sound_value(ibuf);
403        b2.lemma_parse_sound_value(ibuf);
404        b3.lemma_parse_sound_value(ibuf);
405        if b0.spec_parse(ibuf) is None {
406            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
407                assert(self.consistent(super::swap4_1(iv)));
408            }
409            if b1.spec_parse(ibuf) is None {
410                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
411                    assert(self.consistent(super::swap4_2(iv)));
412                }
413                if b2.spec_parse(ibuf) is None {
414                    if let Some((_n, iv)) = b3.spec_parse(ibuf) {
415                        assert(self.consistent(super::swap4_3(iv)));
416                    }
417                }
418            }
419        }
420    }
421}
422
423impl<A, B, C, D> SPRoundTripDps for super::Permute4<A, B, C, D> where
424    A: SPRoundTripDps + NonTailFmt,
425    B: SPRoundTripDps + NonTailFmt,
426    C: SPRoundTripDps + NonTailFmt,
427    D: SPRoundTripDps,
428 {
429    open spec fn unambiguous(&self) -> bool {
430        &&& self.0.unambiguous()
431        &&& self.1.unambiguous()
432        &&& self.2.unambiguous()
433        &&& self.3.unambiguous()
434        &&& self.0.serialize_dps_inv()
435        &&& self.1.serialize_dps_inv()
436        &&& self.2.serialize_dps_inv()
437    }
438
439    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
440        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
441        Pair(self.0, super::Permute3(self.1, self.2, self.3)).theorem_serialize_dps_parse_roundtrip(
442            v,
443            obuf,
444        );
445    }
446}
447
448impl<A, B, C, D> EquivSerializersGeneral for super::Permute4<A, B, C, D> where
449    A: EquivSerializersGeneral,
450    B: EquivSerializersGeneral,
451    C: EquivSerializersGeneral,
452    D: EquivSerializersGeneral,
453 {
454    open spec fn equiv_general_inv(&self) -> bool {
455        &&& self.0.equiv_general_inv()
456        &&& self.1.equiv_general_inv()
457        &&& self.2.equiv_general_inv()
458        &&& self.3.equiv_general_inv()
459    }
460
461    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
462        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
463        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_serialize_equiv(v, obuf);
464    }
465}
466
467impl<A, B, C, D> EquivSerializers for super::Permute4<A, B, C, D> where
468    A: EquivSerializersGeneral,
469    B: EquivSerializersGeneral,
470    C: EquivSerializersGeneral,
471    D: EquivSerializers,
472 {
473    open spec fn equiv_inv(&self) -> bool {
474        &&& self.0.equiv_general_inv()
475        &&& self.1.equiv_general_inv()
476        &&& self.2.equiv_general_inv()
477        &&& self.3.equiv_inv()
478    }
479
480    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
481        reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
482        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_serialize_equiv_on_empty(v);
483    }
484}
485
486// ============================================================================
487// Permute5
488// ============================================================================
489impl<A: SafeParser, B: SafeParser, C: SafeParser, D: SafeParser, E: SafeParser> SafeParser for super::Permute5<
490    A,
491    B,
492    C,
493    D,
494    E,
495> {
496    open spec fn safe_inv(&self) -> bool {
497        &&& self.0.safe_inv()
498        &&& self.1.safe_inv()
499        &&& self.2.safe_inv()
500        &&& self.3.safe_inv()
501        &&& self.4.safe_inv()
502    }
503
504    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
505        Alt::<_, _, false>(
506            Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)),
507            Alt::<_, _, false>(
508                Mapped {
509                    inner: Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4)),
510                    mapper: |i| super::swap5_1(i),
511                },
512                Alt::<_, _, false>(
513                    Mapped {
514                        inner: Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4)),
515                        mapper: |i| super::swap5_2(i),
516                    },
517                    Alt::<_, _, false>(
518                        Mapped {
519                            inner: Pair(self.3, super::Permute4(self.0, self.1, self.2, self.4)),
520                            mapper: |i| super::swap5_3(i),
521                        },
522                        Mapped {
523                            inner: Pair(self.4, super::Permute4(self.0, self.1, self.2, self.3)),
524                            mapper: |i| super::swap5_4(i),
525                        },
526                    ),
527                ),
528            ),
529        ).lemma_parse_safe(ibuf);
530    }
531}
532
533impl<A: Productive, B: Productive, C: Productive, D: Productive, E: Productive> Productive for super::Permute5<
534    A,
535    B,
536    C,
537    D,
538    E,
539> {
540    open spec fn productive_inv(&self) -> bool {
541        &&& self.0.productive_inv()
542        &&& self.1.productive_inv()
543        &&& self.2.productive_inv()
544        &&& self.3.productive_inv()
545        &&& self.4.productive_inv()
546    }
547
548    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
549        Alt::<_, _, false>(
550            Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)),
551            Alt::<_, _, false>(
552                Mapped {
553                    inner: Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4)),
554                    mapper: |i| super::swap5_1(i),
555                },
556                Alt::<_, _, false>(
557                    Mapped {
558                        inner: Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4)),
559                        mapper: |i| super::swap5_2(i),
560                    },
561                    Alt::<_, _, false>(
562                        Mapped {
563                            inner: Pair(self.3, super::Permute4(self.0, self.1, self.2, self.4)),
564                            mapper: |i| super::swap5_3(i),
565                        },
566                        Mapped {
567                            inner: Pair(self.4, super::Permute4(self.0, self.1, self.2, self.3)),
568                            mapper: |i| super::swap5_4(i),
569                        },
570                    ),
571                ),
572            ),
573        ).lemma_productive(ibuf);
574    }
575}
576
577impl<
578    A: SoundParser,
579    B: SoundParser,
580    C: SoundParser,
581    D: SoundParser,
582    E: SoundParser,
583> SoundParser for super::Permute5<A, B, C, D, E> {
584    open spec fn sound_inv(&self) -> bool {
585        &&& self.0.sound_inv()
586        &&& self.1.sound_inv()
587        &&& self.2.sound_inv()
588        &&& self.3.sound_inv()
589        &&& self.4.sound_inv()
590    }
591
592    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
593        let b0 = Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4));
594        let b1 = Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4));
595        let b2 = Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4));
596        let b3 = Pair(self.3, super::Permute4(self.0, self.1, self.2, self.4));
597        let b4 = Pair(self.4, super::Permute4(self.0, self.1, self.2, self.3));
598        b0.lemma_parse_sound_consumption(ibuf);
599        b1.lemma_parse_sound_consumption(ibuf);
600        b2.lemma_parse_sound_consumption(ibuf);
601        b3.lemma_parse_sound_consumption(ibuf);
602        b4.lemma_parse_sound_consumption(ibuf);
603        if b0.spec_parse(ibuf) is None {
604            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
605                assert(self.byte_len(super::swap5_1(iv)) == b1.byte_len(iv));
606            }
607            if b1.spec_parse(ibuf) is None {
608                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
609                    assert(self.byte_len(super::swap5_2(iv)) == b2.byte_len(iv));
610                }
611                if b2.spec_parse(ibuf) is None {
612                    if let Some((_n, iv)) = b3.spec_parse(ibuf) {
613                        assert(self.byte_len(super::swap5_3(iv)) == b3.byte_len(iv));
614                    }
615                    if b3.spec_parse(ibuf) is None {
616                        if let Some((_n, iv)) = b4.spec_parse(ibuf) {
617                            assert(self.byte_len(super::swap5_4(iv)) == b4.byte_len(iv));
618                        }
619                    }
620                }
621            }
622        }
623    }
624
625    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
626        let b0 = Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4));
627        let b1 = Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4));
628        let b2 = Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4));
629        let b3 = Pair(self.3, super::Permute4(self.0, self.1, self.2, self.4));
630        let b4 = Pair(self.4, super::Permute4(self.0, self.1, self.2, self.3));
631        b0.lemma_parse_sound_value(ibuf);
632        b1.lemma_parse_sound_value(ibuf);
633        b2.lemma_parse_sound_value(ibuf);
634        b3.lemma_parse_sound_value(ibuf);
635        b4.lemma_parse_sound_value(ibuf);
636        if b0.spec_parse(ibuf) is None {
637            if let Some((_n, iv)) = b1.spec_parse(ibuf) {
638                assert(self.consistent(super::swap5_1(iv)));
639            }
640            if b1.spec_parse(ibuf) is None {
641                if let Some((_n, iv)) = b2.spec_parse(ibuf) {
642                    assert(self.consistent(super::swap5_2(iv)));
643                }
644                if b2.spec_parse(ibuf) is None {
645                    if let Some((_n, iv)) = b3.spec_parse(ibuf) {
646                        assert(self.consistent(super::swap5_3(iv)));
647                    }
648                    if b3.spec_parse(ibuf) is None {
649                        if let Some((_n, iv)) = b4.spec_parse(ibuf) {
650                            assert(self.consistent(super::swap5_4(iv)));
651                        }
652                    }
653                }
654            }
655        }
656    }
657}
658
659impl<A, B, C, D, E> SPRoundTripDps for super::Permute5<A, B, C, D, E> where
660    A: SPRoundTripDps + NonTailFmt,
661    B: SPRoundTripDps + NonTailFmt,
662    C: SPRoundTripDps + NonTailFmt,
663    D: SPRoundTripDps + NonTailFmt,
664    E: SPRoundTripDps,
665{
666    open spec fn unambiguous(&self) -> bool {
667        &&& self.0.unambiguous()
668        &&& self.1.unambiguous()
669        &&& self.2.unambiguous()
670        &&& self.3.unambiguous()
671        &&& self.4.unambiguous()
672        &&& self.0.serialize_dps_inv()
673        &&& self.1.serialize_dps_inv()
674        &&& self.2.serialize_dps_inv()
675        &&& self.3.serialize_dps_inv()
676    }
677
678    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
679        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).theorem_serialize_dps_parse_roundtrip(
680            v,
681            obuf,
682        );
683    }
684}
685
686impl<A, B, C, D, E> EquivSerializersGeneral for super::Permute5<A, B, C, D, E> where
687    A: EquivSerializersGeneral,
688    B: EquivSerializersGeneral,
689    C: EquivSerializersGeneral,
690    D: EquivSerializersGeneral,
691    E: EquivSerializersGeneral,
692{
693    open spec fn equiv_general_inv(&self) -> bool {
694        &&& self.0.equiv_general_inv()
695        &&& self.1.equiv_general_inv()
696        &&& self.2.equiv_general_inv()
697        &&& self.3.equiv_general_inv()
698        &&& self.4.equiv_general_inv()
699    }
700
701    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
702        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_serialize_equiv(v, obuf);
703    }
704}
705
706impl<A, B, C, D, E> EquivSerializers for super::Permute5<A, B, C, D, E> where
707    A: EquivSerializersGeneral,
708    B: EquivSerializersGeneral,
709    C: EquivSerializersGeneral,
710    D: EquivSerializersGeneral,
711    E: EquivSerializers,
712{
713    open spec fn equiv_inv(&self) -> bool {
714        &&& self.0.equiv_general_inv()
715        &&& self.1.equiv_general_inv()
716        &&& self.2.equiv_general_inv()
717        &&& self.3.equiv_general_inv()
718        &&& self.4.equiv_inv()
719    }
720
721    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
722        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_serialize_equiv_on_empty(v);
723    }
724}
725
726} // verus!
vest_lib/combinators/permute/proof.rs

vest_lib/combinators/permute/
proof.rs
