vest_lib/combinators/permute/
mod.rs

1//! Combinators for parsing permutations of sub-parsers.
2//!
3//! Each `Permute*` combinator accepts any ordering of its components while its serializer always
4//! emits the declared order. That makes them deliberately *malleable*: distinct byte strings map to
5//! the same value, so [`NonMalleable`](crate::core::proof::NonMalleable) and
6//! [`PSRoundTrip`](crate::core::proof::PSRoundTrip) are not available. Soundness is, because
7//! reordering preserves the total length.
8//!
9//! Only widths 2 to 5 are provided. The construction enumerates orderings, so the number of parse
10//! paths grows as `N!` (`Permute4` has 24, `Permute5` has 120).
11/// Executable parser and serializer implementations for this combinator.
12pub mod exec;
13/// Proofs of the security and correctness properties for this combinator.
14pub mod proof;
15/// Specification trait implementations for this combinator.
16pub mod spec;
17
18use vstd::prelude::*;
19
20use crate::combinators::choice::Alt;
21use crate::combinators::Mapped;
22
23verus! {
24
25pub open spec fn swap2<A, B>(i: (B, A)) -> (A, B) {
26    (i.1, i.0)
27}
28
29pub open spec fn swap3_1<A, B, C>(i: (B, (A, C))) -> (A, (B, C)) {
30    (i.1.0, (i.0, i.1.1))
31}
32
33pub open spec fn swap3_2<A, B, C>(i: (C, (A, B))) -> (A, (B, C)) {
34    (i.1.0, (i.1.1, i.0))
35}
36
37pub open spec fn swap4_1<A, B, C, D>(i: (B, (A, (C, D)))) -> (A, (B, (C, D))) {
38    (i.1.0, (i.0, i.1.1))
39}
40
41pub open spec fn swap4_2<A, B, C, D>(i: (C, (A, (B, D)))) -> (A, (B, (C, D))) {
42    (i.1.0, (i.1.1.0, (i.0, i.1.1.1)))
43}
44
45pub open spec fn swap4_3<A, B, C, D>(i: (D, (A, (B, C)))) -> (A, (B, (C, D))) {
46    (i.1.0, (i.1.1.0, (i.1.1.1, i.0)))
47}
48
49pub open spec fn swap5_1<A, B, C, D, E>(i: (B, (A, (C, (D, E))))) -> (A, (B, (C, (D, E)))) {
50    (i.1.0, (i.0, i.1.1))
51}
52
53pub open spec fn swap5_2<A, B, C, D, E>(i: (C, (A, (B, (D, E))))) -> (A, (B, (C, (D, E)))) {
54    (i.1.0, (i.1.1.0, (i.0, i.1.1.1)))
55}
56
57pub open spec fn swap5_3<A, B, C, D, E>(i: (D, (A, (B, (C, E))))) -> (A, (B, (C, (D, E)))) {
58    (i.1.0, (i.1.1.0, (i.1.1.1.0, (i.0, i.1.1.1.1))))
59}
60
61pub open spec fn swap5_4<A, B, C, D, E>(i: (E, (A, (B, (C, D))))) -> (A, (B, (C, (D, E)))) {
62    (i.1.0, (i.1.1.0, (i.1.1.1.0, (i.1.1.1.1, i.0))))
63}
64
65/// `Permute2<P1, P2>` parses either `(P1, P2)` or `(P2, P1)` and produces `(P1::PVal, P2::PVal)`
66///
67/// `Permute2 ::= Alt((P1, P2), Mapped((P2, P1), swap))`
68#[derive(Copy)]
69pub struct Permute2<P1, P2>(pub P1, pub P2);
70
71impl<P1: Clone, P2: Clone> Clone for Permute2<P1, P2> {
72    fn clone(&self) -> (cloned: Self)
73        ensures
74            call_ensures(P1::clone, (&self.0,), cloned.0),
75            call_ensures(P2::clone, (&self.1,), cloned.1),
76    {
77        Permute2(self.0.clone(), self.1.clone())
78    }
79}
80
81/// `Permute3<A, B, C>` parses any permutation of A, B, C and produces `(A::PVal, (B::PVal, C::PVal))`
82///
83/// ```text
84/// Permute3(A, B, C) ::= Alt(
85///     (A, Permute2(B, C)),
86///     Alt(
87///         Mapped((B, Permute2(A, C)), swap2),
88///         Mapped((C, Permute2(A, B)), swap3),
89///     )
90/// )
91/// ```
92#[derive(Copy)]
93pub struct Permute3<A, B, C>(pub A, pub B, pub C);
94
95impl<A: Clone, B: Clone, C: Clone> Clone for Permute3<A, B, C> {
96    fn clone(&self) -> (cloned: Self)
97        ensures
98            call_ensures(A::clone, (&self.0,), cloned.0),
99            call_ensures(B::clone, (&self.1,), cloned.1),
100            call_ensures(C::clone, (&self.2,), cloned.2),
101    {
102        Permute3(self.0.clone(), self.1.clone(), self.2.clone())
103    }
104}
105
106/// `Permute4<A, B, C, D>` parses any permutation and produces `(A::PVal, (B::PVal, (C::PVal, D::PVal)))`
107///
108/// ```text
109/// Permute4(A, B, C, D) ::= Alt(
110///     (A, Permute3(B, C, D)),
111///     Alt(
112///         Mapped((B, Permute3(A, C, D)), swap4_1),
113///         Alt(
114///             Mapped((C, Permute3(A, B, D)), swap4_2),
115///             Mapped((D, Permute3(A, B, C)), swap4_3),
116///         )
117///     )
118/// )
119/// ```
120#[derive(Copy)]
121pub struct Permute4<A, B, C, D>(pub A, pub B, pub C, pub D);
122
123impl<A: Clone, B: Clone, C: Clone, D: Clone> Clone for Permute4<A, B, C, D> {
124    fn clone(&self) -> (cloned: Self)
125        ensures
126            call_ensures(A::clone, (&self.0,), cloned.0),
127            call_ensures(B::clone, (&self.1,), cloned.1),
128            call_ensures(C::clone, (&self.2,), cloned.2),
129            call_ensures(D::clone, (&self.3,), cloned.3),
130    {
131        Permute4(self.0.clone(), self.1.clone(), self.2.clone(), self.3.clone())
132    }
133}
134
135/// `Permute5<A, B, C, D, E>` parses any permutation and produces `(A::PVal, (B::PVal, (C::PVal, (D::PVal, E::PVal))))`
136///
137/// ```text
138/// Permute5(A, B, C, D, E) ::= Alt(
139///     (A, Permute4(B, C, D, E)),
140///     Alt(
141///         Mapped((B, Permute4(A, C, D, E)), swap5_1),
142///         Alt(
143///             Mapped((C, Permute4(A, B, D, E)), swap5_2),
144///             Alt(
145///                 Mapped((D, Permute4(A, B, C, E)), swap5_3),
146///                 Mapped((E, Permute4(A, B, C, D)), swap5_4),
147///             )
148///         )
149///     )
150/// )
151/// ```
152#[derive(Copy)]
153pub struct Permute5<A, B, C, D, E>(pub A, pub B, pub C, pub D, pub E);
154
155impl<A: Clone, B: Clone, C: Clone, D: Clone, E: Clone> Clone for Permute5<A, B, C, D, E> {
156    fn clone(&self) -> (cloned: Self)
157        ensures
158            call_ensures(A::clone, (&self.0,), cloned.0),
159            call_ensures(B::clone, (&self.1,), cloned.1),
160            call_ensures(C::clone, (&self.2,), cloned.2),
161            call_ensures(D::clone, (&self.3,), cloned.3),
162            call_ensures(E::clone, (&self.4,), cloned.4),
163    {
164        Permute5(self.0.clone(), self.1.clone(), self.2.clone(), self.3.clone(), self.4.clone())
165    }
166}
167
168} // verus!
169#[cfg(test)]
170mod tests {
171    use super::{Permute2, Permute3, Permute4, Permute5};
172    use crate::combinators::{Const, U8};
173    use crate::core::exec::{ByteLen, Parser, Prepare, SerializerExt};
174
175    /// A one-byte format that only accepts `b`, so orderings are distinguishable.
176    fn tag(b: u8) -> Const<U8, u8> {
177        Const(U8, b)
178    }
179
180    /// Serializes `$v` with `$fmt`, checking that `prepare` and `length` agree.
181    macro_rules! serialized {
182        ($fmt:expr, $v:expr) => {{
183            let len = $fmt.prepare(&$v).unwrap();
184            assert_eq!($fmt.length(&$v), len, "length and prepare disagree");
185            let mut out = vec![0u8; len];
186            $fmt.serialize(&$v, out.as_mut_slice());
187            out
188        }};
189    }
190
191    #[test]
192    fn permute2_accepts_both_orders_and_serializes_the_declared_one() {
193        let fmt = Permute2(tag(0xAA), tag(0xBB));
194        let value = (0xAAu8, 0xBBu8);
195
196        // Declared order and the swap both parse to the same value: the malleability witness.
197        assert_eq!(fmt.parse(&&[0xAA, 0xBB][..]), Ok((2, value)));
198        assert_eq!(fmt.parse(&&[0xBB, 0xAA][..]), Ok((2, value)));
199
200        // Serialization always emits the declared order.
201        assert_eq!(serialized!(fmt, value), vec![0xAA, 0xBB]);
202    }
203
204    #[test]
205    fn permute2_rejects_wrong_and_truncated_input() {
206        let fmt = Permute2(tag(0xAA), tag(0xBB));
207        assert!(fmt.parse(&&[0xAA, 0xAA][..]).is_err());
208        assert!(fmt.parse(&&[0xAA][..]).is_err());
209        assert!(fmt.parse(&&[][..]).is_err());
210    }
211
212    #[test]
213    fn permute3_accepts_all_six_orders() {
214        let fmt = Permute3(tag(0xA1), tag(0xB2), tag(0xC3));
215        let value = (0xA1u8, (0xB2u8, 0xC3u8));
216
217        for order in [
218            [0xA1, 0xB2, 0xC3],
219            [0xA1, 0xC3, 0xB2],
220            [0xB2, 0xA1, 0xC3],
221            [0xB2, 0xC3, 0xA1],
222            [0xC3, 0xA1, 0xB2],
223            [0xC3, 0xB2, 0xA1],
224        ] {
225            assert_eq!(fmt.parse(&&order[..]), Ok((3, value)), "order {order:02x?}");
226        }
227
228        assert_eq!(serialized!(fmt, value), vec![0xA1, 0xB2, 0xC3]);
229        assert!(fmt.parse(&&[0xA1, 0xB2, 0xB2][..]).is_err());
230        assert!(fmt.parse(&&[0xA1, 0xB2][..]).is_err());
231    }
232
233    #[test]
234    fn permute4_accepts_every_order() {
235        let fmt = Permute4(tag(0xA1), tag(0xB2), tag(0xC3), tag(0xD4));
236        let value = (0xA1u8, (0xB2u8, (0xC3u8, 0xD4u8)));
237
238        // All 24 permutations, generated so the test covers each branch of each nesting level.
239        let bytes = [0xA1u8, 0xB2, 0xC3, 0xD4];
240        let mut count = 0;
241        for i in 0..4 {
242            for j in 0..4 {
243                for k in 0..4 {
244                    for l in 0..4 {
245                        if i == j || i == k || i == l || j == k || j == l || k == l {
246                            continue;
247                        }
248                        let order = [bytes[i], bytes[j], bytes[k], bytes[l]];
249                        assert_eq!(fmt.parse(&&order[..]), Ok((4, value)), "order {order:02x?}");
250                        count += 1;
251                    }
252                }
253            }
254        }
255        assert_eq!(count, 24);
256
257        assert_eq!(serialized!(fmt, value), vec![0xA1, 0xB2, 0xC3, 0xD4]);
258        assert!(fmt.parse(&&[0xA1, 0xB2, 0xC3][..]).is_err());
259        assert!(fmt.parse(&&[0xA1, 0xB2, 0xC3, 0xC3][..]).is_err());
260    }
261
262    #[test]
263    fn permute5_accepts_every_order() {
264        let fmt = Permute5(tag(0xA1), tag(0xB2), tag(0xC3), tag(0xD4), tag(0xE5));
265        let value = (0xA1u8, (0xB2u8, (0xC3u8, (0xD4u8, 0xE5u8))));
266
267        // All 120 permutations
268        let bytes = [0xA1u8, 0xB2, 0xC3, 0xD4, 0xE5];
269        let mut count = 0;
270        for i in 0..5 {
271            for j in 0..5 {
272                for k in 0..5 {
273                    for l in 0..5 {
274                        for m in 0..5 {
275                            if i == j || i == k || i == l || i == m
276                                || j == k || j == l || j == m
277                                || k == l || k == m
278                                || l == m
279                            {
280                                continue;
281                            }
282                            let order = [bytes[i], bytes[j], bytes[k], bytes[l], bytes[m]];
283                            assert_eq!(fmt.parse(&&order[..]), Ok((5, value)), "order {order:02x?}");
284                            count += 1;
285                        }
286                    }
287                }
288            }
289        }
290        assert_eq!(count, 120);
291
292        assert_eq!(serialized!(fmt, value), vec![0xA1, 0xB2, 0xC3, 0xD4, 0xE5]);
293        assert!(fmt.parse(&&[0xA1, 0xB2, 0xC3, 0xD4][..]).is_err());
294        assert!(fmt.parse(&&[0xA1, 0xB2, 0xC3, 0xD4, 0xD4][..]).is_err());
295    }
296
297    #[test]
298    fn parsing_consumes_only_the_permutation_and_leaves_trailing_bytes() {
299        let fmt = Permute2(tag(0xAA), tag(0xBB));
300        let (consumed, value) = fmt.parse(&&[0xBB, 0xAA, 0x99][..]).unwrap();
301        assert_eq!(consumed, 2);
302        assert_eq!(value, (0xAAu8, 0xBBu8));
303    }
304}
vest_lib/combinators/permute/mod.rs

vest_lib/combinators/permute/
mod.rs
