vest_lib/combinators/permute/
spec.rs

1//! Specifications for formats accepting multiple component orders.
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// ============== Permute2 ==============
11// Permute2 ::= Alt((P1, P2), Mapped((P2, P1), swap))
12impl<P1, P2> SpecParser for super::Permute2<P1, P2> where P1: SpecParser, P2: SpecParser {
13    type PVal = (P1::PVal, P2::PVal);
14
15    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
16        let inner = Alt::<_, _, false>(
17            Pair(self.0, self.1),
18            Mapped { inner: Pair(self.1, self.0), mapper: |i| super::swap2(i) },
19        );
20        inner.spec_parse(ibuf)
21    }
22}
23
24impl<P1, P2> Consistency for super::Permute2<P1, P2> where P1: Consistency, P2: Consistency {
25    type Val = (P1::Val, P2::Val);
26
27    open spec fn consistent(&self, v: Self::Val) -> bool {
28        Pair(self.0, self.1).consistent(v)
29    }
30}
31
32impl<P1, P2> SpecSerializerDps for super::Permute2<P1, P2> where
33    P1: SpecSerializerDps,
34    P2: SpecSerializerDps,
35 {
36    type SValue = (P1::SValue, P2::SValue);
37
38    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
39        Pair(self.0, self.1).spec_serialize_dps(v, obuf)
40    }
41}
42
43impl<P1, P2> SpecSerializer for super::Permute2<P1, P2> where
44    P1: SpecSerializer,
45    P2: SpecSerializer,
46 {
47    type SVal = (P1::SVal, P2::SVal);
48
49    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
50        Pair(self.0, self.1).spec_serialize(v)
51    }
52}
53
54impl<P1, P2> NonTailFmt for super::Permute2<P1, P2> where P1: NonTailFmt, P2: NonTailFmt {
55    open spec fn serialize_dps_inv(&self) -> bool {
56        &&& self.0.serialize_dps_inv()
57        &&& self.1.serialize_dps_inv()
58    }
59
60    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
61        Pair(self.0, self.1).lemma_serialize_dps_prepend(v, obuf);
62    }
63
64    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
65        Pair(self.0, self.1).lemma_serialize_dps_len(v, obuf);
66    }
67}
68
69impl<P1, P2> GoodSerializer for super::Permute2<P1, P2> where
70    P1: GoodSerializer,
71    P2: GoodSerializer,
72 {
73    open spec fn serialize_inv(&self) -> bool {
74        &&& self.0.serialize_inv()
75        &&& self.1.serialize_inv()
76    }
77
78    proof fn lemma_serialize_len(&self, v: Self::SVal) {
79        Pair(self.0, self.1).lemma_serialize_len(v);
80    }
81}
82
83impl<P1: SpecByteLen, P2: SpecByteLen> SpecByteLen for super::Permute2<P1, P2> {
84    type T = (P1::T, P2::T);
85
86    open spec fn byte_len(&self, v: Self::T) -> nat {
87        Pair(self.0, self.1).byte_len(v)
88    }
89}
90
91impl<P1: MinMaxByteLen, P2: MinMaxByteLen> MinMaxByteLen for super::Permute2<P1, P2> {
92    open spec fn min(&self) -> nat {
93        Pair(self.0, self.1).min()
94    }
95
96    open spec fn max(&self) -> nat {
97        Pair(self.0, self.1).max()
98    }
99
100    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
101        Pair(self.0, self.1).lemma_min_max_byte_len(v);
102    }
103}
104
105impl<P1: ValueByteLen, P2: ValueByteLen> ValueByteLen for super::Permute2<P1, P2> {
106    open spec fn value_byte_len(v: Self::T) -> nat {
107        <crate::combinators::Pair<P1, P2> as ValueByteLen>::value_byte_len(v)
108    }
109
110    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
111        crate::combinators::Pair(self.0, self.1).lemma_value_len_matches_byte_len(v);
112    }
113}
114
115impl<P1: StaticByteLen, P2: StaticByteLen> StaticByteLen for super::Permute2<P1, P2> {
116    open spec fn static_byte_len() -> nat {
117        P1::static_byte_len() + P2::static_byte_len()
118    }
119
120    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
121        self.0.lemma_static_len_matches_byte_len(v.0);
122        self.1.lemma_static_len_matches_byte_len(v.1);
123    }
124}
125
126// ============== Permute3 ==============
127// Permute3(A, B, C) ::= Alt(
128//     (A, Permute2(B, C)),
129//     Alt(
130//         Mapped((B, Permute2(A, C)), swap3_1),
131//         Mapped((C, Permute2(A, B)), swap3_2),
132//     )
133// )
134impl<A, B, C> SpecParser for super::Permute3<A, B, C> where
135    A: SpecParser,
136    B: SpecParser,
137    C: SpecParser,
138 {
139    type PVal = (A::PVal, (B::PVal, C::PVal));
140
141    // Opaque for the same reason as `Permute4::spec_parse`: it keeps each `Permute*` proof
142    // obligation proportional to that level's branch count instead of the factorial expansion.
143    #[verifier::opaque]
144    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
145        let inner = Alt::<_, _, false>(
146            Pair(self.0, super::Permute2(self.1, self.2)),
147            Alt::<_, _, false>(
148                Mapped {
149                    inner: Pair(self.1, super::Permute2(self.0, self.2)),
150                    mapper: |i| super::swap3_1(i),
151                },
152                Mapped {
153                    inner: Pair(self.2, super::Permute2(self.0, self.1)),
154                    mapper: |i| super::swap3_2(i),
155                },
156            ),
157        );
158        inner.spec_parse(ibuf)
159    }
160}
161
162impl<A, B, C> Consistency for super::Permute3<A, B, C> where
163    A: Consistency,
164    B: Consistency,
165    C: Consistency,
166 {
167    type Val = (A::Val, (B::Val, C::Val));
168
169    open spec fn consistent(&self, v: Self::Val) -> bool {
170        Pair(self.0, Pair(self.1, self.2)).consistent(v)
171    }
172}
173
174impl<A, B, C> SpecSerializerDps for super::Permute3<A, B, C> where
175    A: SpecSerializerDps,
176    B: SpecSerializerDps,
177    C: SpecSerializerDps,
178 {
179    type SValue = (A::SValue, (B::SValue, C::SValue));
180
181    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
182        Pair(self.0, super::Permute2(self.1, self.2)).spec_serialize_dps(v, obuf)
183    }
184}
185
186impl<A, B, C> SpecSerializer for super::Permute3<A, B, C> where
187    A: SpecSerializer,
188    B: SpecSerializer,
189    C: SpecSerializer,
190 {
191    type SVal = (A::SVal, (B::SVal, C::SVal));
192
193    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
194        Pair(self.0, super::Permute2(self.1, self.2)).spec_serialize(v)
195    }
196}
197
198impl<A, B, C> NonTailFmt for super::Permute3<A, B, C> where
199    A: NonTailFmt,
200    B: NonTailFmt,
201    C: NonTailFmt,
202 {
203    open spec fn serialize_dps_inv(&self) -> bool {
204        &&& self.0.serialize_dps_inv()
205        &&& self.1.serialize_dps_inv()
206        &&& self.2.serialize_dps_inv()
207    }
208
209    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
210        Pair(self.0, super::Permute2(self.1, self.2)).lemma_serialize_dps_prepend(v, obuf);
211    }
212
213    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
214        Pair(self.0, super::Permute2(self.1, self.2)).lemma_serialize_dps_len(v, obuf);
215    }
216}
217
218impl<A, B, C> GoodSerializer for super::Permute3<A, B, C> where
219    A: GoodSerializer,
220    B: GoodSerializer,
221    C: GoodSerializer,
222 {
223    open spec fn serialize_inv(&self) -> bool {
224        &&& self.0.serialize_inv()
225        &&& self.1.serialize_inv()
226        &&& self.2.serialize_inv()
227    }
228
229    proof fn lemma_serialize_len(&self, v: Self::SVal) {
230        Pair(self.0, super::Permute2(self.1, self.2)).lemma_serialize_len(v);
231    }
232}
233
234impl<A: SpecByteLen, B: SpecByteLen, C: SpecByteLen> SpecByteLen for super::Permute3<A, B, C> {
235    type T = (A::T, (B::T, C::T));
236
237    open spec fn byte_len(&self, v: Self::T) -> nat {
238        Pair(self.0, super::Permute2(self.1, self.2)).byte_len(v)
239    }
240}
241
242impl<A: MinMaxByteLen, B: MinMaxByteLen, C: MinMaxByteLen> MinMaxByteLen for super::Permute3<
243    A,
244    B,
245    C,
246> {
247    open spec fn min(&self) -> nat {
248        Pair(self.0, super::Permute2(self.1, self.2)).min()
249    }
250
251    open spec fn max(&self) -> nat {
252        Pair(self.0, super::Permute2(self.1, self.2)).max()
253    }
254
255    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
256        Pair(self.0, super::Permute2(self.1, self.2)).lemma_min_max_byte_len(v);
257    }
258}
259
260impl<A: ValueByteLen, B: ValueByteLen, C: ValueByteLen> ValueByteLen for super::Permute3<A, B, C> {
261    open spec fn value_byte_len(v: Self::T) -> nat {
262        <crate::combinators::Pair<A, super::Permute2<B, C>> as ValueByteLen>::value_byte_len(v)
263    }
264
265    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
266        crate::combinators::Pair(
267            self.0,
268            super::Permute2(self.1, self.2),
269        ).lemma_value_len_matches_byte_len(v);
270    }
271}
272
273impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen> StaticByteLen for super::Permute3<
274    A,
275    B,
276    C,
277> {
278    open spec fn static_byte_len() -> nat {
279        A::static_byte_len() + <super::Permute2<B, C> as StaticByteLen>::static_byte_len()
280    }
281
282    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
283        self.0.lemma_static_len_matches_byte_len(v.0);
284        self.1.lemma_static_len_matches_byte_len(v.1.0);
285        self.2.lemma_static_len_matches_byte_len(v.1.1);
286    }
287}
288
289// ============== Permute4 ==============
290// Permute4(A, B, C, D) ::= Alt(
291//     (A, Permute3(B, C, D)),
292//     Alt(
293//         Mapped((B, Permute3(A, C, D)), swap4_1),
294//         Alt(
295//             Mapped((C, Permute3(A, B, D)), swap4_2),
296//             Mapped((D, Permute3(A, B, C)), swap4_3),
297//         )
298//     )
299// )
300impl<A, B, C, D> SpecParser for super::Permute4<A, B, C, D> where
301    A: SpecParser,
302    B: SpecParser,
303    C: SpecParser,
304    D: SpecParser,
305 {
306    type PVal = (A::PVal, (B::PVal, (C::PVal, D::PVal)));
307
308    // Opaque so that `Permute5`'s obligations stop unfolding here. Without this the `Permute5`
309    // proofs expand the whole 5*4*3*2 = 120-path `Alt` tree into a single query.
310    #[verifier::opaque]
311    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
312        let inner = Alt::<_, _, false>(
313            Pair(self.0, super::Permute3(self.1, self.2, self.3)),
314            Alt::<_, _, false>(
315                Mapped {
316                    inner: Pair(self.1, super::Permute3(self.0, self.2, self.3)),
317                    mapper: |i| super::swap4_1(i),
318                },
319                Alt::<_, _, false>(
320                    Mapped {
321                        inner: Pair(self.2, super::Permute3(self.0, self.1, self.3)),
322                        mapper: |i| super::swap4_2(i),
323                    },
324                    Mapped {
325                        inner: Pair(self.3, super::Permute3(self.0, self.1, self.2)),
326                        mapper: |i| super::swap4_3(i),
327                    },
328                ),
329            ),
330        );
331        inner.spec_parse(ibuf)
332    }
333}
334
335impl<A, B, C, D> Consistency for super::Permute4<A, B, C, D> where
336    A: Consistency,
337    B: Consistency,
338    C: Consistency,
339    D: Consistency,
340 {
341    type Val = (A::Val, (B::Val, (C::Val, D::Val)));
342
343    open spec fn consistent(&self, v: Self::Val) -> bool {
344        self.0.consistent(v.0) && self.1.consistent(v.1.0) && self.2.consistent(v.1.1.0)
345            && self.3.consistent(v.1.1.1)
346    }
347}
348
349impl<A, B, C, D> SpecSerializerDps for super::Permute4<A, B, C, D> where
350    A: SpecSerializerDps,
351    B: SpecSerializerDps,
352    C: SpecSerializerDps,
353    D: SpecSerializerDps,
354 {
355    type SValue = (A::SValue, (B::SValue, (C::SValue, D::SValue)));
356
357    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
358        Pair(self.0, super::Permute3(self.1, self.2, self.3)).spec_serialize_dps(v, obuf)
359    }
360}
361
362impl<A, B, C, D> SpecSerializer for super::Permute4<A, B, C, D> where
363    A: SpecSerializer,
364    B: SpecSerializer,
365    C: SpecSerializer,
366    D: SpecSerializer,
367 {
368    type SVal = (A::SVal, (B::SVal, (C::SVal, D::SVal)));
369
370    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
371        Pair(self.0, super::Permute3(self.1, self.2, self.3)).spec_serialize(v)
372    }
373}
374
375impl<A, B, C, D> NonTailFmt for super::Permute4<A, B, C, D> where
376    A: NonTailFmt,
377    B: NonTailFmt,
378    C: NonTailFmt,
379    D: NonTailFmt,
380 {
381    open spec fn serialize_dps_inv(&self) -> bool {
382        &&& self.0.serialize_dps_inv()
383        &&& self.1.serialize_dps_inv()
384        &&& self.2.serialize_dps_inv()
385        &&& self.3.serialize_dps_inv()
386    }
387
388    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
389        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_serialize_dps_prepend(v, obuf);
390    }
391
392    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
393        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_serialize_dps_len(v, obuf);
394    }
395}
396
397impl<A, B, C, D> GoodSerializer for super::Permute4<A, B, C, D> where
398    A: GoodSerializer,
399    B: GoodSerializer,
400    C: GoodSerializer,
401    D: GoodSerializer,
402 {
403    open spec fn serialize_inv(&self) -> bool {
404        &&& self.0.serialize_inv()
405        &&& self.1.serialize_inv()
406        &&& self.2.serialize_inv()
407        &&& self.3.serialize_inv()
408    }
409
410    proof fn lemma_serialize_len(&self, v: Self::SVal) {
411        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_serialize_len(v);
412    }
413}
414
415impl<
416    A: SpecByteLen,
417    B: SpecByteLen,
418    C: SpecByteLen,
419    D: SpecByteLen,
420> SpecByteLen for super::Permute4<A, B, C, D> {
421    type T = (A::T, (B::T, (C::T, D::T)));
422
423    open spec fn byte_len(&self, v: Self::T) -> nat {
424        Pair(self.0, super::Permute3(self.1, self.2, self.3)).byte_len(v)
425    }
426}
427
428impl<
429    A: MinMaxByteLen,
430    B: MinMaxByteLen,
431    C: MinMaxByteLen,
432    D: MinMaxByteLen,
433> MinMaxByteLen for super::Permute4<A, B, C, D> {
434    open spec fn min(&self) -> nat {
435        Pair(self.0, super::Permute3(self.1, self.2, self.3)).min()
436    }
437
438    open spec fn max(&self) -> nat {
439        Pair(self.0, super::Permute3(self.1, self.2, self.3)).max()
440    }
441
442    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
443        Pair(self.0, super::Permute3(self.1, self.2, self.3)).lemma_min_max_byte_len(v);
444    }
445}
446
447impl<
448    A: ValueByteLen,
449    B: ValueByteLen,
450    C: ValueByteLen,
451    D: ValueByteLen,
452> ValueByteLen for super::Permute4<A, B, C, D> {
453    open spec fn value_byte_len(v: Self::T) -> nat {
454        <crate::combinators::Pair<A, super::Permute3<B, C, D>> as ValueByteLen>::value_byte_len(v)
455    }
456
457    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
458        crate::combinators::Pair(
459            self.0,
460            super::Permute3(self.1, self.2, self.3),
461        ).lemma_value_len_matches_byte_len(v);
462    }
463}
464
465impl<
466    A: StaticByteLen,
467    B: StaticByteLen,
468    C: StaticByteLen,
469    D: StaticByteLen,
470> StaticByteLen for super::Permute4<A, B, C, D> {
471    open spec fn static_byte_len() -> nat {
472        A::static_byte_len() + <super::Permute3<B, C, D> as StaticByteLen>::static_byte_len()
473    }
474
475    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
476        self.0.lemma_static_len_matches_byte_len(v.0);
477        self.1.lemma_static_len_matches_byte_len(v.1.0);
478        self.2.lemma_static_len_matches_byte_len(v.1.1.0);
479        self.3.lemma_static_len_matches_byte_len(v.1.1.1);
480    }
481}
482
483// ============== Permute5 ==============
484// Permute5(A, B, C, D, E) ::= Alt(
485//     (A, Permute4(B, C, D, E)),
486//     Alt(
487//         Mapped((B, Permute4(A, C, D, E)), swap5_1),
488//         Alt(
489//             Mapped((C, Permute4(A, B, D, E)), swap5_2),
490//             Alt(
491//                 Mapped((D, Permute4(A, B, C, E)), swap5_3),
492//                 Mapped((E, Permute4(A, B, C, D)), swap5_4),
493//             )
494//         )
495//     )
496// )
497impl<A, B, C, D, E> SpecParser for super::Permute5<A, B, C, D, E> where
498    A: SpecParser,
499    B: SpecParser,
500    C: SpecParser,
501    D: SpecParser,
502    E: SpecParser,
503{
504    type PVal = (A::PVal, (B::PVal, (C::PVal, (D::PVal, E::PVal))));
505
506    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
507        let inner = Alt::<_, _, false>(
508            Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)),
509            Alt::<_, _, false>(
510                Mapped {
511                    inner: Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4)),
512                    mapper: |i| super::swap5_1(i),
513                },
514                Alt::<_, _, false>(
515                    Mapped {
516                        inner: Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4)),
517                        mapper: |i| super::swap5_2(i),
518                    },
519                    Alt::<_, _, false>(
520                        Mapped {
521                            inner: Pair(self.3, super::Permute4(self.0, self.1, self.2, self.4)),
522                            mapper: |i| super::swap5_3(i),
523                        },
524                        Mapped {
525                            inner: Pair(self.4, super::Permute4(self.0, self.1, self.2, self.3)),
526                            mapper: |i| super::swap5_4(i),
527                        },
528                    ),
529                ),
530            ),
531        );
532        inner.spec_parse(ibuf)
533    }
534}
535
536impl<A, B, C, D, E> Consistency for super::Permute5<A, B, C, D, E> where
537    A: Consistency,
538    B: Consistency,
539    C: Consistency,
540    D: Consistency,
541    E: Consistency,
542{
543    type Val = (A::Val, (B::Val, (C::Val, (D::Val, E::Val))));
544
545    open spec fn consistent(&self, v: Self::Val) -> bool {
546        self.0.consistent(v.0) && self.1.consistent(v.1.0) && self.2.consistent(v.1.1.0)
547            && self.3.consistent(v.1.1.1.0) && self.4.consistent(v.1.1.1.1)
548    }
549}
550
551impl<A, B, C, D, E> SpecSerializerDps for super::Permute5<A, B, C, D, E> where
552    A: SpecSerializerDps,
553    B: SpecSerializerDps,
554    C: SpecSerializerDps,
555    D: SpecSerializerDps,
556    E: SpecSerializerDps,
557{
558    type SValue = (A::SValue, (B::SValue, (C::SValue, (D::SValue, E::SValue))));
559
560    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
561        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).spec_serialize_dps(v, obuf)
562    }
563}
564
565impl<A, B, C, D, E> SpecSerializer for super::Permute5<A, B, C, D, E> where
566    A: SpecSerializer,
567    B: SpecSerializer,
568    C: SpecSerializer,
569    D: SpecSerializer,
570    E: SpecSerializer,
571{
572    type SVal = (A::SVal, (B::SVal, (C::SVal, (D::SVal, E::SVal))));
573
574    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
575        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).spec_serialize(v)
576    }
577}
578
579impl<A, B, C, D, E> NonTailFmt for super::Permute5<A, B, C, D, E> where
580    A: NonTailFmt,
581    B: NonTailFmt,
582    C: NonTailFmt,
583    D: NonTailFmt,
584    E: NonTailFmt,
585{
586    open spec fn serialize_dps_inv(&self) -> bool {
587        &&& self.0.serialize_dps_inv()
588        &&& self.1.serialize_dps_inv()
589        &&& self.2.serialize_dps_inv()
590        &&& self.3.serialize_dps_inv()
591        &&& self.4.serialize_dps_inv()
592    }
593
594    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
595        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_serialize_dps_prepend(
596            v,
597            obuf,
598        );
599    }
600
601    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
602        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_serialize_dps_len(
603            v,
604            obuf,
605        );
606    }
607}
608
609impl<A, B, C, D, E> GoodSerializer for super::Permute5<A, B, C, D, E> where
610    A: GoodSerializer,
611    B: GoodSerializer,
612    C: GoodSerializer,
613    D: GoodSerializer,
614    E: GoodSerializer,
615{
616    open spec fn serialize_inv(&self) -> bool {
617        &&& self.0.serialize_inv()
618        &&& self.1.serialize_inv()
619        &&& self.2.serialize_inv()
620        &&& self.3.serialize_inv()
621        &&& self.4.serialize_inv()
622    }
623
624    proof fn lemma_serialize_len(&self, v: Self::SVal) {
625        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_serialize_len(v);
626    }
627}
628
629impl<
630    A: SpecByteLen,
631    B: SpecByteLen,
632    C: SpecByteLen,
633    D: SpecByteLen,
634    E: SpecByteLen,
635> SpecByteLen for super::Permute5<A, B, C, D, E> {
636    type T = (A::T, (B::T, (C::T, (D::T, E::T))));
637
638    open spec fn byte_len(&self, v: Self::T) -> nat {
639        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).byte_len(v)
640    }
641}
642
643impl<
644    A: MinMaxByteLen,
645    B: MinMaxByteLen,
646    C: MinMaxByteLen,
647    D: MinMaxByteLen,
648    E: MinMaxByteLen,
649> MinMaxByteLen for super::Permute5<A, B, C, D, E> {
650    open spec fn min(&self) -> nat {
651        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).min()
652    }
653
654    open spec fn max(&self) -> nat {
655        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).max()
656    }
657
658    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
659        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).lemma_min_max_byte_len(v);
660    }
661}
662
663impl<
664    A: ValueByteLen,
665    B: ValueByteLen,
666    C: ValueByteLen,
667    D: ValueByteLen,
668    E: ValueByteLen,
669> ValueByteLen for super::Permute5<A, B, C, D, E> {
670    open spec fn value_byte_len(v: Self::T) -> nat {
671        <crate::combinators::Pair<A, super::Permute4<B, C, D, E>> as ValueByteLen>::value_byte_len(
672            v,
673        )
674    }
675
676    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
677        crate::combinators::Pair(
678            self.0,
679            super::Permute4(self.1, self.2, self.3, self.4),
680        ).lemma_value_len_matches_byte_len(v);
681    }
682}
683
684impl<
685    A: StaticByteLen,
686    B: StaticByteLen,
687    C: StaticByteLen,
688    D: StaticByteLen,
689    E: StaticByteLen,
690> StaticByteLen for super::Permute5<A, B, C, D, E> {
691    open spec fn static_byte_len() -> nat {
692        A::static_byte_len() + <super::Permute4<B, C, D, E> as StaticByteLen>::static_byte_len()
693    }
694
695    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
696        self.0.lemma_static_len_matches_byte_len(v.0);
697        self.1.lemma_static_len_matches_byte_len(v.1.0);
698        self.2.lemma_static_len_matches_byte_len(v.1.1.0);
699        self.3.lemma_static_len_matches_byte_len(v.1.1.1.0);
700        self.4.lemma_static_len_matches_byte_len(v.1.1.1.1);
701    }
702}
703
704// ============== reference bridging ==============
705// The executable `parse` methods build their sub-parsers from borrows (`Permute3(&a, &b, &c)`)
706// while the specs above are written over owned components (`Permute3(a, b, c)`). Those are
707// distinct types, so with `spec_parse` opaque the two denotations are no longer related by
708// unfolding. Each lemma below re-establishes the link for exactly one level, treating the level
709// underneath it as an atom, which keeps every query linear in that level's branch count rather
710// than re-expanding the whole factorial tree at each use site.
711//
712// The equality has to hold at *every* input, not just the caller's: `Pair` runs its second
713// component on a suffix (`ibuf.skip(n)`), so a pointwise fact about the caller's `ibuf` alone
714// would never apply to the nested occurrences.
715
716/// `Permute3` denotes the same parser whether its components are owned or borrowed.
717pub proof fn lemma_permute3_spec_parse_ref<A: SpecParser, B: SpecParser, C: SpecParser>(
718    a: A,
719    b: B,
720    c: C,
721)
722    ensures
723        forall|ibuf: Seq<u8>|
724            #[trigger] super::Permute3(&a, &b, &c).spec_parse(ibuf) == super::Permute3(
725                a,
726                b,
727                c,
728            ).spec_parse(ibuf),
729{
730    reveal(<super::Permute3<_, _, _> as SpecParser>::spec_parse);
731}
732
733/// `Permute4` denotes the same parser whether its components are owned or borrowed.
734pub proof fn lemma_permute4_spec_parse_ref<
735    A: SpecParser,
736    B: SpecParser,
737    C: SpecParser,
738    D: SpecParser,
739>(a: A, b: B, c: C, d: D)
740    ensures
741        forall|ibuf: Seq<u8>|
742            #[trigger] super::Permute4(&a, &b, &c, &d).spec_parse(ibuf) == super::Permute4(
743                a,
744                b,
745                c,
746                d,
747            ).spec_parse(ibuf),
748{
749    reveal(<super::Permute4<_, _, _, _> as SpecParser>::spec_parse);
750    lemma_permute3_spec_parse_ref(b, c, d);
751    lemma_permute3_spec_parse_ref(a, c, d);
752    lemma_permute3_spec_parse_ref(a, b, d);
753    lemma_permute3_spec_parse_ref(a, b, c);
754}
755
756} // verus!
vest_lib/combinators/permute/spec.rs

vest_lib/combinators/permute/
spec.rs
