vest_lib/combinators/choice/
proof.rs

1//! Correctness, disjointness, and malleability proofs for alternatives.
2use super::spec::*;
3use crate::combinators::Sum;
4use crate::core::{proof::*, spec::*};
5use vstd::prelude::*;
6
7verus! {
8
9impl<A: SPRoundTripDps, B: SPRoundTripDps> SPRoundTripDps for super::Choice<A, B> {
10    open spec fn unambiguous(&self) -> bool {
11        &&& self.0.unambiguous()
12        &&& self.1.unambiguous()
13        &&& disjoint_domains(self.0, self.1)
14    }
15
16    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
17        reveal(disjoint_domains);
18        match v {
19            Sum::Inl(va) => {
20                self.0.theorem_serialize_dps_parse_roundtrip(va, obuf);
21            },
22            Sum::Inr(vb) => {
23                self.1.theorem_serialize_dps_parse_roundtrip(vb, obuf);
24            },
25        }
26    }
27}
28
29// impl<A: PSRoundTrip, B: PSRoundTrip> PSRoundTrip for super::Choice<A, B> {
30//     proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
31//         self.0.theorem_parse_serialize_roundtrip(ibuf);
32//         self.1.theorem_parse_serialize_roundtrip(ibuf);
33//     }
34// }
35impl<A: NonMalleable, B: NonMalleable> NonMalleable for super::Choice<A, B> {
36    open spec fn nonmal_inv(&self) -> bool {
37        &&& self.0.nonmal_inv()
38        &&& self.1.nonmal_inv()
39    }
40
41    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
42        self.0.lemma_parse_non_malleable(buf1, buf2);
43        self.1.lemma_parse_non_malleable(buf1, buf2);
44    }
45}
46
47impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for super::Choice<A, B> {
48    open spec fn no_lookahead_inv(&self) -> bool {
49        &&& self.0.no_lookahead_inv()
50        &&& self.1.no_lookahead_inv()
51        &&& disjoint_domains(self.0, self.1)
52    }
53
54    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
55        reveal(disjoint_domains);
56        self.0.lemma_no_lookahead(i1, i2);
57        self.1.lemma_no_lookahead(i1, i2);
58        assert(disjoint_domains(self.0, self.1));
59    }
60}
61
62impl<A: Productive, B: Productive> Productive for super::Choice<A, B> {
63    open spec fn productive_inv(&self) -> bool {
64        &&& self.0.productive_inv()
65        &&& self.1.productive_inv()
66    }
67
68    proof fn lemma_productive(&self, s: Seq<u8>) {
69        self.0.lemma_productive(s);
70        self.1.lemma_productive(s);
71    }
72}
73
74impl<A, B> EquivSerializersGeneral for super::Choice<A, B> where
75    A: EquivSerializersGeneral,
76    B: EquivSerializersGeneral,
77 {
78    open spec fn equiv_general_inv(&self) -> bool {
79        &&& self.0.equiv_general_inv()
80        &&& self.1.equiv_general_inv()
81    }
82
83    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
84        match v {
85            Sum::Inl(va) => {
86                self.0.lemma_serialize_equiv(va, obuf);
87            },
88            Sum::Inr(vb) => {
89                self.1.lemma_serialize_equiv(vb, obuf);
90            },
91        }
92    }
93}
94
95impl<A, B> EquivSerializers for super::Choice<A, B> where A: EquivSerializers, B: EquivSerializers {
96    open spec fn equiv_inv(&self) -> bool {
97        &&& self.0.equiv_inv()
98        &&& self.1.equiv_inv()
99    }
100
101    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
102        match v {
103            Sum::Inl(va) => {
104                self.0.lemma_serialize_equiv_on_empty(va);
105            },
106            Sum::Inr(vb) => {
107                self.1.lemma_serialize_equiv_on_empty(vb);
108            },
109        }
110    }
111}
112
113impl<
114    const NONDETERMINISTIC: bool,
115    A: SPRoundTripDps,
116    B: SPRoundTripDps<T = A::T>,
117> SPRoundTripDps for super::Alt<A, B, NONDETERMINISTIC> {
118    open spec fn unambiguous(&self) -> bool {
119        &&& self.0.unambiguous()
120        &&& self.1.unambiguous()
121        &&& disjoint_domains(self.0, self.1)
122    }
123
124    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
125        reveal(disjoint_domains);
126        if self.choose_left(v) {
127            self.0.theorem_serialize_dps_parse_roundtrip(v, obuf);
128        } else {
129            self.1.theorem_serialize_dps_parse_roundtrip(v, obuf);
130        }
131    }
132}
133
134// NonMalleable only holds for [`Alt`] when the two parsers produce disjoint sets of values.
135// This ensures that if two byte sequences parse to the same value, they must have used the same underlying parser.
136impl<const NONDETERMINISTIC: bool, A, B> NonMalleable for super::Alt<A, B, NONDETERMINISTIC> where
137    A: SoundParser + NonMalleable,
138    B: SoundParser<T = A::T> + NonMalleable,
139 {
140    open spec fn nonmal_inv(&self) -> bool {
141        &&& self.0.sound_inv()
142        &&& self.1.sound_inv()
143        &&& self.0.nonmal_inv()
144        &&& self.1.nonmal_inv()
145        &&& disjoint_values(self.0, self.1)
146    }
147
148    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
149        if let Some((n1, v1)) = self.spec_parse(buf1) {
150            if let Some((n2, v2)) = self.spec_parse(buf2) {
151                if v1 == v2 {
152                    let a_parses_buf1 = self.0.spec_parse(buf1) is Some;
153                    let a_parses_buf2 = self.0.spec_parse(buf2) is Some;
154                    if a_parses_buf1 && a_parses_buf2 {
155                        // Both use parser A
156                        self.0.lemma_parse_non_malleable(buf1, buf2);
157                    } else if !a_parses_buf1 && !a_parses_buf2 {
158                        // Both use parser B
159                        self.1.lemma_parse_non_malleable(buf1, buf2);
160                    } else {
161                        // buf1 uses A; buf2 uses B
162                        if a_parses_buf1 && !a_parses_buf2 {
163                            self.0.lemma_parse_sound_value(buf1);
164                            self.1.lemma_parse_sound_value(buf2);
165                            assert(self.0.consistent(v1));
166                            assert(self.1.consistent(v2));
167                            assert(disjoint_values(self.0, self.1));
168                        } else {
169                            // buf1 uses B; buf2 uses A
170                            self.1.lemma_parse_sound_value(buf1);
171                            self.0.lemma_parse_sound_value(buf2);
172                            assert(self.1.consistent(v1));
173                            assert(self.0.consistent(v2));
174                            assert(disjoint_values(self.0, self.1));
175                        }
176                    }
177                }
178            }
179        }
180    }
181}
182
183impl<const NONDETERMINISTIC: bool, A, B> NoLookAhead for super::Alt<A, B, NONDETERMINISTIC> where
184    A: NoLookAhead,
185    B: NoLookAhead<PVal = A::PVal>,
186 {
187    open spec fn no_lookahead_inv(&self) -> bool {
188        &&& self.0.no_lookahead_inv()
189        &&& self.1.no_lookahead_inv()
190        &&& disjoint_domains(self.0, self.1)
191    }
192
193    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
194        reveal(disjoint_domains);
195        assert(self.no_lookahead_inv());
196        self.0.lemma_no_lookahead(i1, i2);
197        self.1.lemma_no_lookahead(i1, i2);
198        assert(disjoint_domains(self.0, self.1));
199    }
200}
201
202impl<const NONDETERMINISTIC: bool, A, B> Productive for super::Alt<A, B, NONDETERMINISTIC> where
203    A: Productive,
204    B: Productive<PVal = A::PVal>,
205 {
206    open spec fn productive_inv(&self) -> bool {
207        &&& self.0.productive_inv()
208        &&& self.1.productive_inv()
209    }
210
211    proof fn lemma_productive(&self, s: Seq<u8>) {
212        self.0.lemma_productive(s);
213        self.1.lemma_productive(s);
214    }
215}
216
217impl<const NONDETERMINISTIC: bool, A, B> EquivSerializersGeneral for super::Alt<
218    A,
219    B,
220    NONDETERMINISTIC,
221> where
222    A: EquivSerializersGeneral + Consistency<Val = A::SVal>,
223    B: EquivSerializersGeneral<SVal = A::SVal> + Consistency<Val = B::SVal>,
224 {
225    open spec fn equiv_general_inv(&self) -> bool {
226        &&& self.0.equiv_general_inv()
227        &&& self.1.equiv_general_inv()
228    }
229
230    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
231        if self.choose_left(v) {
232            self.0.lemma_serialize_equiv(v, obuf);
233        } else {
234            self.1.lemma_serialize_equiv(v, obuf);
235        }
236    }
237}
238
239impl<const NONDETERMINISTIC: bool, A, B> EquivSerializers for super::Alt<
240    A,
241    B,
242    NONDETERMINISTIC,
243> where
244    A: EquivSerializers + Consistency<Val = A::SVal>,
245    B: EquivSerializers<SVal = A::SVal> + Consistency<Val = B::SVal>,
246 {
247    open spec fn equiv_inv(&self) -> bool {
248        &&& self.0.equiv_inv()
249        &&& self.1.equiv_inv()
250    }
251
252    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
253        if self.choose_left(v) {
254            self.0.lemma_serialize_equiv_on_empty(v);
255        } else {
256            self.1.lemma_serialize_equiv_on_empty(v);
257        }
258    }
259}
260
261impl<T, C, const N: usize> SPRoundTripDps for super::Dispatch<T, C, N> where C: SPRoundTripDps {
262    open spec fn unambiguous(&self) -> bool {
263        self.active_branch().unambiguous()
264    }
265
266    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
267        self.active_branch().theorem_serialize_dps_parse_roundtrip(v, obuf);
268    }
269}
270
271impl<T, C: NonMalleable, const N: usize> NonMalleable for super::Dispatch<T, C, N> {
272    open spec fn nonmal_inv(&self) -> bool {
273        self.active_branch().nonmal_inv()
274    }
275
276    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
277        if let Some((_n1, _v1)) = self.spec_parse(buf1) {
278            if let Some((_n2, _v2)) = self.spec_parse(buf2) {
279                self.active_branch().lemma_parse_non_malleable(buf1, buf2);
280            }
281        }
282    }
283}
284
285impl<T, C: NoLookAhead, const N: usize> NoLookAhead for super::Dispatch<T, C, N> {
286    open spec fn no_lookahead_inv(&self) -> bool {
287        self.active_branch().no_lookahead_inv()
288    }
289
290    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
291        if let Some((n, v)) = self.spec_parse(i1) {
292            if 0 <= n <= i2.len() {
293                if i2.take(n) == i1.take(n) {
294                    self.active_branch().lemma_no_lookahead(i1, i2);
295                }
296            }
297        }
298    }
299}
300
301impl<T, C: Productive, const N: usize> Productive for super::Dispatch<T, C, N> {
302    open spec fn productive_inv(&self) -> bool {
303        self.active_branch().productive_inv()
304    }
305
306    proof fn lemma_productive(&self, s: Seq<u8>) {
307        self.active_branch().lemma_productive(s);
308    }
309}
310
311impl<T, C, const N: usize> EquivSerializersGeneral for super::Dispatch<T, C, N> where
312    C: EquivSerializersGeneral,
313 {
314    open spec fn equiv_general_inv(&self) -> bool {
315        self.active_branch().equiv_general_inv()
316    }
317
318    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
319        self.active_branch().lemma_serialize_equiv(v, obuf);
320    }
321}
322
323impl<T, C: EquivSerializers, const N: usize> EquivSerializers for super::Dispatch<T, C, N> {
324    open spec fn equiv_inv(&self) -> bool {
325        self.active_branch().equiv_inv()
326    }
327
328    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
329        self.active_branch().lemma_serialize_equiv_on_empty(v);
330    }
331}
332
333impl<A: SPRoundTripDps, B: SPRoundTripDps> SPRoundTripDps for Sum<A, B> {
334    open spec fn unambiguous(&self) -> bool {
335        match self {
336            Sum::Inl(a) => a.unambiguous(),
337            Sum::Inr(b) => b.unambiguous(),
338        }
339    }
340
341    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
342        match (self, v) {
343            (Sum::Inl(a), Sum::Inl(va)) => a.theorem_serialize_dps_parse_roundtrip(va, obuf),
344            (Sum::Inr(b), Sum::Inr(vb)) => b.theorem_serialize_dps_parse_roundtrip(vb, obuf),
345            _ => (),
346        }
347    }
348}
349
350impl<A: NonMalleable, B: NonMalleable> NonMalleable for Sum<A, B> {
351    open spec fn nonmal_inv(&self) -> bool {
352        match self {
353            Sum::Inl(a) => a.nonmal_inv(),
354            Sum::Inr(b) => b.nonmal_inv(),
355        }
356    }
357
358    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
359        match self {
360            Sum::Inl(a) => a.lemma_parse_non_malleable(buf1, buf2),
361            Sum::Inr(b) => b.lemma_parse_non_malleable(buf1, buf2),
362        }
363    }
364}
365
366impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for Sum<A, B> {
367    open spec fn no_lookahead_inv(&self) -> bool {
368        match self {
369            Sum::Inl(a) => a.no_lookahead_inv(),
370            Sum::Inr(b) => b.no_lookahead_inv(),
371        }
372    }
373
374    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
375        match self {
376            Sum::Inl(a) => a.lemma_no_lookahead(i1, i2),
377            Sum::Inr(b) => b.lemma_no_lookahead(i1, i2),
378        }
379    }
380}
381
382impl<A: Productive, B: Productive> Productive for Sum<A, B> {
383    open spec fn productive_inv(&self) -> bool {
384        match self {
385            Sum::Inl(a) => a.productive_inv(),
386            Sum::Inr(b) => b.productive_inv(),
387        }
388    }
389
390    proof fn lemma_productive(&self, s: Seq<u8>) {
391        match self {
392            Sum::Inl(a) => a.lemma_productive(s),
393            Sum::Inr(b) => b.lemma_productive(s),
394        }
395    }
396}
397
398impl<A, B> EquivSerializersGeneral for Sum<A, B> where
399    A: EquivSerializersGeneral,
400    B: EquivSerializersGeneral,
401 {
402    open spec fn equiv_general_inv(&self) -> bool {
403        match self {
404            Sum::Inl(a) => a.equiv_general_inv(),
405            Sum::Inr(b) => b.equiv_general_inv(),
406        }
407    }
408
409    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
410        match (self, v) {
411            (Sum::Inl(a), Sum::Inl(va)) => a.lemma_serialize_equiv(va, obuf),
412            (Sum::Inr(b), Sum::Inr(vb)) => b.lemma_serialize_equiv(vb, obuf),
413            _ => (),
414        }
415    }
416}
417
418impl<A, B> EquivSerializers for Sum<A, B> where A: EquivSerializers, B: EquivSerializers {
419    open spec fn equiv_inv(&self) -> bool {
420        match self {
421            Sum::Inl(a) => a.equiv_inv(),
422            Sum::Inr(b) => b.equiv_inv(),
423        }
424    }
425
426    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
427        match (self, v) {
428            (Sum::Inl(a), Sum::Inl(va)) => a.lemma_serialize_equiv_on_empty(va),
429            (Sum::Inr(b), Sum::Inr(vb)) => b.lemma_serialize_equiv_on_empty(vb),
430            _ => (),
431        }
432    }
433}
434
435} // verus!
vest_lib/combinators/choice/proof.rs

vest_lib/combinators/choice/
proof.rs
