vest_lib/combinators/star/
proof.rs

1//! Correctness, termination, and ambiguity proofs for repetition.
2use crate::combinators::length::AsLen;
3use crate::combinators::Pair;
4use crate::core::{proof::*, spec::*};
5use vstd::{calc, prelude::*};
6
7verus! {
8
9impl<A> super::Star<A> where A: SPRoundTripDps + NonTailFmt {
10    proof fn lemma_serialize_parse_roundtrip_rec(&self, vs: Seq<A::PVal>, obuf: Seq<u8>)
11        requires
12            self.0.serialize_dps_inv(),
13            self.0.unambiguous(),
14            parser_fails_on(self.0, obuf),
15            self.consistent(vs),
16        ensures
17            self.spec_parse(self.spec_serialize_dps(vs, obuf)) == Some(
18                ((self.spec_serialize_dps(vs, obuf).len() - obuf.len()) as int, vs),
19            ),
20        decreases vs.len(),
21    {
22        reveal(<super::Star::<_> as SpecParser>::spec_parse);
23        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
24        reveal(<super::Star::<_> as Consistency>::consistent);
25        if vs.len() == 0 {
26            assert(self.0.spec_parse(obuf) is None);
27        } else {
28            let v = vs[0];
29            let rest = vs.skip(1);
30            let rest_buf = self.spec_serialize_dps(rest, obuf);
31            let serialized = self.spec_serialize_dps(vs, obuf);
32            assert(serialized == self.0.spec_serialize_dps(v, rest_buf));
33
34            // induction
35            assert(self.consistent(rest));
36            self.lemma_serialize_parse_roundtrip_rec(rest, obuf);
37
38            // base
39            assert(self.0.consistent(v));
40            self.0.theorem_serialize_dps_parse_roundtrip(v, rest_buf);
41            self.0.lemma_serialize_dps_prepend(v, rest_buf);
42            self.0.lemma_serialize_dps_len(v, rest_buf);
43
44            let n0 = (serialized.len() - rest_buf.len()) as int;
45            assert(self.0.spec_parse(serialized) == Some((n0, v)));
46            assert(serialized.skip(n0) == rest_buf);
47
48            if 0 < n0 <= serialized.len() {
49                assert(self.spec_parse(rest_buf) == Some(self.parse_rec(rest_buf)));
50                let (n1, v1) = self.parse_rec(rest_buf);
51                assert(self.spec_parse(serialized) == Some((n0 + n1, seq![v] + v1)));
52            } else {
53                assert(n0 == 0);
54                assert(serialized == rest_buf);
55                assert(self.0.spec_parse(rest_buf) == Some((0int, v)));
56
57                // from the definition
58                assert(self.parse_rec(rest_buf) == (0int, Seq::<A::PVal>::empty()));
59                // from I.H.:
60                assert(self.parse_rec(rest_buf) == (rest_buf.len() - obuf.len(), rest));
61                self.lemma_serialize_dps_prepend(rest, obuf);
62
63                // therefore:
64                assert(rest_buf == obuf);
65                assert(rest == Seq::<A::PVal>::empty());
66
67                // contradiction
68                assert(self.0.spec_parse(obuf) is Some);
69                assert(self.0.spec_parse(obuf) is None);
70            }
71        }
72    }
73}
74
75impl<A: NonMalleable + SafeParser> super::Star<A> {
76    proof fn lemma_parse_non_malleable_rec(&self, buf1: Seq<u8>, buf2: Seq<u8>)
77        requires
78            self.nonmal_inv(),
79        ensures
80            ({
81                let (n1, v1) = self.parse_rec(buf1);
82                let (n2, v2) = self.parse_rec(buf2);
83                v1 == v2 ==> buf1.take(n1) == buf2.take(n2)
84            }),
85        decreases buf1.len(),
86    {
87        reveal(<super::Star::<_> as SpecParser>::spec_parse);
88        let (n1, v1) = self.parse_rec(buf1);
89        let (n2, v2) = self.parse_rec(buf2);
90        if v1 == v2 {
91            match (self.0.spec_parse(buf1), self.0.spec_parse(buf2)) {
92                (Some((m1, a1)), Some((m2, a2))) => {
93                    if 0 < m1 <= buf1.len() && 0 < m2 <= buf2.len() {
94                        let (n1_rest, rest1) = self.parse_rec(buf1.skip(m1));
95                        let (n2_rest, rest2) = self.parse_rec(buf2.skip(m2));
96
97                        assert(n1 == m1 + n1_rest);
98                        assert(n2 == m2 + n2_rest);
99                        assert(v1 == seq![a1] + rest1);
100                        assert(v2 == seq![a2] + rest2);
101
102                        assert(a1 == a2) by {
103                            assert(a1 == v1[0] && a2 == v2[0]);
104                        }
105                        assert(rest1 == rest2) by {
106                            assert(rest1 == v1.skip(1));
107                            assert(rest2 == v2.skip(1));
108                        }
109
110                        // base
111                        self.0.lemma_parse_non_malleable(buf1, buf2);
112                        assert(buf1.take(m1) == buf2.take(m2));
113
114                        // induction
115                        assert(self.safe_inv());
116                        self.lemma_parse_non_malleable_rec(buf1.skip(m1), buf2.skip(m2));
117                        assert(buf1.skip(m1).take(n1_rest) == buf2.skip(m2).take(n2_rest));
118
119                        // need to show buf1.take(n1) == buf2.take(n2)
120                        assert(self.safe_inv());
121                        self.lemma_parse_safe(buf1.skip(m1));
122                        self.lemma_parse_safe(buf2.skip(m2));
123                        assert(buf1.take(n1) == buf1.take(m1) + buf1.skip(m1).take(n1_rest));
124                        assert(buf2.take(n2) == buf2.take(m2) + buf2.skip(m2).take(n2_rest));
125                    }
126                },
127                _ => {},
128            }
129        }
130    }
131}
132
133impl<A: NonMalleable + SafeParser> NonMalleable for super::Star<A> {
134    open spec fn nonmal_inv(&self) -> bool {
135        &&& self.0.nonmal_inv()
136        &&& self.0.safe_inv()
137    }
138
139    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
140        reveal(<super::Star::<_> as SpecParser>::spec_parse);
141        assert(self.nonmal_inv());
142        assert(self.safe_inv());
143        self.lemma_parse_non_malleable_rec(buf1, buf2);
144    }
145}
146
147impl<A: SafeParser> Productive for super::Star<A> {
148    open spec fn productive_inv(&self) -> bool {
149        false
150    }
151
152    proof fn lemma_productive(&self, s: Seq<u8>) {
153    }
154}
155
156impl<A: NoLookAhead> super::Star<A> {
157    proof fn lemma_parse_rec_no_lookahead_conditional(&self, i1: Seq<u8>, i2: Seq<u8>)
158        requires
159            self.safe_inv(),
160            self.0.no_lookahead_inv(),
161            parser_fails_on(self.0, i2.skip(self.parse_rec(i1).0)),
162        ensures
163            ({
164                let r = self.parse_rec(i1);
165                0 <= r.0 <= i2.len() ==> i2.take(r.0) == i1.take(r.0) ==> self.parse_rec(i2) == r
166            }),
167        decreases i1.len(),
168    {
169        reveal(<super::Star::<_> as SpecParser>::spec_parse);
170        use crate::combinators::tuple::proof::lemma_take_skip;
171        broadcast use vstd::seq_lib::group_seq_properties;
172
173        let (n, vs) = self.parse_rec(i1);
174        match self.0.spec_parse(i1) {
175            Some((m, v)) if 0 < m <= i1.len() => {
176                let i1_rest = i1.skip(m);
177                let i2_rest = i2.skip(m);
178                let (n_rest, vs_rest) = self.parse_rec(i1_rest);
179                assert(self.safe_inv());
180                self.lemma_parse_safe(i1_rest);
181                if 0 <= n <= i2.len() {
182                    if i2.take(n) == i1.take(n) {
183                        assert(i2.take(m) == i1.take(m));
184                        assert(self.0.safe_inv());
185                        self.0.lemma_no_lookahead(i1, i2);
186                        assert(i2_rest.take(n_rest) == i1_rest.take(n_rest)) by {
187                            lemma_take_skip(i1, m, n_rest);
188                            lemma_take_skip(i2, m, n_rest);
189                        };
190                        assert(parser_fails_on(self.0, i2_rest.skip(n_rest))) by {
191                            broadcast use vstd::seq_lib::lemma_seq_skip_of_skip;
192
193                        };
194                        self.lemma_parse_rec_no_lookahead_conditional(i1_rest, i2_rest);
195                        assert(self.parse_rec(i2) == (m + n_rest, seq![v] + vs_rest));
196                    }
197                }
198            },
199            _ => {},
200        }
201    }
202}
203
204impl<A> super::Star<A> where A: EquivSerializersGeneral {
205    proof fn lemma_serialize_equiv_rec(&self, vs: Seq<A::SVal>, obuf: Seq<u8>)
206        requires
207            self.0.equiv_general_inv(),
208        ensures
209            self.rfold_serialize_dps(vs, obuf) == self.spec_serialize(vs) + obuf,
210        decreases vs.len(),
211    {
212        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
213        let f = |buf: Seq<u8>, elem: A::SVal| buf + self.0.spec_serialize(elem);
214
215        if vs.len() == 0 {
216        } else {
217            let v0 = vs[0];
218            let rest = vs.skip(1);
219
220            let rest_foldr = self.rfold_serialize_dps(rest, obuf);
221            let rest_foldl = rest.fold_left(Seq::empty(), f);
222
223            calc! {
224                (==)
225                self.rfold_serialize_dps(vs, obuf); {  // definition
226                }
227                self.0.spec_serialize_dps(v0, rest_foldr); {
228                    // base
229                    self.0.lemma_serialize_equiv(v0, rest_foldr);
230                }
231                self.0.spec_serialize(v0) + rest_foldr; {
232                    // induction
233                    self.lemma_serialize_equiv_rec(rest, obuf);
234                }
235                self.0.spec_serialize(v0) + (rest_foldl + obuf); {}
236                (self.0.spec_serialize(v0) + rest_foldl) + obuf;
237            }
238
239            // need to show: fold_left(vs, empty, f) == inner.spec_serialize(v0) + rest_foldl
240
241            calc! {
242                (==)
243                vs.fold_left(Seq::empty(), f); {
244                    vs.lemma_fold_left_alt(Seq::empty(), f);
245                }
246                vs.fold_left_alt(Seq::empty(), f); {}
247                rest.fold_left_alt(f(Seq::empty(), v0), f); {}
248                rest.fold_left_alt(self.0.spec_serialize(v0), f); {
249                    rest.lemma_fold_left_alt(self.0.spec_serialize(v0), f);
250                }
251                rest.fold_left(self.0.spec_serialize(v0), f); {
252                    assert forall|acc: Seq<u8>, x: Seq<u8>, y: A::SVal| #[trigger]
253                        f(acc + x, y) == acc + #[trigger] f(x, y) by {}
254                    lemma_fold_left_accumulate_seq(rest, self.0.spec_serialize(v0), f);
255                }
256                self.0.spec_serialize(v0) + rest_foldl;
257            }
258        }
259    }
260}
261
262pub(crate) proof fn lemma_fold_left_accumulate_seq<T, U>(
263    vs: Seq<T>,
264    init: Seq<U>,
265    f: spec_fn(Seq<U>, T) -> Seq<U>,
266)
267    requires
268        forall|acc: Seq<U>, x: Seq<U>, y: T| #[trigger] f(acc + x, y) == acc + #[trigger] f(x, y),
269    ensures
270        vs.fold_left(init, f) == init + vs.fold_left(Seq::<U>::empty(), f),
271    decreases vs.len(),
272{
273    if vs.len() == 0 {
274    } else {
275        let last = vs.last();
276        let prefix = vs.drop_last();
277        lemma_fold_left_accumulate_seq(prefix, init, f);
278    }
279}
280
281pub(crate) proof fn lemma_fold_left_accumulate_nat<T>(
282    vs: Seq<T>,
283    init: nat,
284    f: spec_fn(nat, T) -> nat,
285)
286    requires
287        forall|acc: nat, x: nat, y: T| #[trigger] f(acc + x, y) == acc + #[trigger] f(x, y),
288    ensures
289        vs.fold_left(init, f) == init + vs.fold_left(0, f),
290    decreases vs.len(),
291{
292    if vs.len() == 0 {
293    } else {
294        let last = vs.last();
295        let prefix = vs.drop_last();
296        lemma_fold_left_accumulate_nat(prefix, init, f);
297    }
298}
299
300impl<A> EquivSerializersGeneral for super::Star<A> where A: EquivSerializersGeneral {
301    open spec fn equiv_general_inv(&self) -> bool {
302        self.0.equiv_general_inv()
303    }
304
305    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
306        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
307        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
308        self.lemma_serialize_equiv_rec(v, obuf);
309    }
310}
311
312impl<A> EquivSerializers for super::Star<A> where A: EquivSerializersGeneral {
313    open spec fn equiv_inv(&self) -> bool {
314        self.0.equiv_general_inv()
315    }
316
317    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
318        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
319        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
320        self.lemma_serialize_equiv_rec(v, Seq::empty());
321    }
322}
323
324impl<C, N> super::RepeatN<C, N> where C: SPRoundTripDps + NonTailFmt, N: AsLen {
325    proof fn lemma_serialize_parse_roundtrip_rec(&self, vs: Seq<C::PVal>, count: nat, obuf: Seq<u8>)
326        requires
327            self.1.serialize_dps_inv(),
328            self.1.unambiguous(),
329            vs.len() == count,
330            (super::Star(self.1).consistent(vs)),
331        ensures
332            self.parse_n_rec(count, self.spec_serialize_dps(vs, obuf)) == Some(
333                ((self.spec_serialize_dps(vs, obuf).len() - obuf.len()) as int, vs),
334            ),
335        decreases count,
336    {
337        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
338        reveal(<super::Star::<_> as Consistency>::consistent);
339        if count == 0 {
340        } else {
341            let v0 = vs[0];
342            let rest = vs.skip(1);
343            let rest_buf = self.spec_serialize_dps(rest, obuf);
344            let serialized = self.spec_serialize_dps(vs, obuf);
345
346            self.lemma_serialize_parse_roundtrip_rec(rest, (count - 1) as nat, obuf);
347
348            self.1.theorem_serialize_dps_parse_roundtrip(v0, rest_buf);
349            self.1.lemma_serialize_dps_prepend(v0, rest_buf);
350            self.1.lemma_serialize_dps_len(v0, rest_buf);
351
352            let n0 = (serialized.len() - rest_buf.len()) as int;
353            assert(serialized.skip(n0) == rest_buf);
354        }
355    }
356}
357
358impl<C, N> SPRoundTripDps for super::RepeatN<C, N> where C: SPRoundTripDps + NonTailFmt, N: AsLen {
359    open spec fn unambiguous(&self) -> bool {
360        &&& self.1.serialize_dps_inv()
361        &&& self.1.unambiguous()
362    }
363
364    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
365        self.lemma_serialize_parse_roundtrip_rec(v, self.0.as_nat(), obuf);
366        self.lemma_serialize_dps_len(v, obuf);
367    }
368}
369
370impl<C: NonMalleable, N: AsLen> super::RepeatN<C, N> {
371    #[verusfmt::skip]
372    proof fn lemma_parse_non_malleable_rec(&self, count: nat, buf1: Seq<u8>, buf2: Seq<u8>)
373        requires
374            self.1.nonmal_inv(),
375            self.1.safe_inv(),
376        ensures
377            self.parse_n_rec(count, buf1) matches Some((n1, v1)) ==>
378            self.parse_n_rec(count, buf2) matches Some((n2, v2)) ==>
379            v1 == v2 ==> buf1.take(n1) == buf2.take(n2),
380        decreases count,
381    {
382        broadcast use vstd::seq_lib::group_seq_properties;
383
384        if count == 0 {
385        } else {
386            if let Some((n1, v1)) = self.parse_n_rec(count, buf1) {
387                if let Some((n2, v2)) = self.parse_n_rec(count, buf2) {
388                    if v1 == v2 {
389                        let (m1, a1) = self.1.spec_parse(buf1)->0;
390                        let (m2, a2) = self.1.spec_parse(buf2)->0;
391                        let (r1, rest1) = self.parse_n_rec((count - 1) as nat, buf1.skip(m1))->0;
392                        let (r2, rest2) = self.parse_n_rec((count - 1) as nat, buf2.skip(m2))->0;
393                        assert(v1 == seq![a1] + rest1);
394                        assert(v2 == seq![a2] + rest2);
395                        assert(a1 == a2) by {
396                            assert(a1 == v1[0]);
397                            assert(a2 == v2[0]);
398                        }
399                        assert(rest1 == rest2) by {
400                            assert(rest1 == v1.skip(1));
401                            assert(rest2 == v2.skip(1));
402                        }
403
404                        self.1.lemma_parse_safe(buf1);
405                        self.1.lemma_parse_safe(buf2);
406                        self.lemma_parse_n_len_bound((count - 1) as nat, buf1.skip(m1));
407                        self.lemma_parse_n_len_bound((count - 1) as nat, buf2.skip(m2));
408                        self.1.lemma_parse_non_malleable(buf1, buf2);
409                        assert(buf1.take(m1) == buf2.take(m2));
410
411                        self.lemma_parse_non_malleable_rec((count - 1) as nat, buf1.skip(m1), buf2.skip(m2));
412                        assert(buf1.skip(m1).take(r1) == buf2.skip(m2).take(r2));
413
414                        assert(n1 == m1 + r1);
415                        assert(n2 == m2 + r2);
416                        assert(buf1.take(n1) == buf1.take(m1) + buf1.skip(m1).take(r1));
417                        assert(buf2.take(n2) == buf2.take(m2) + buf2.skip(m2).take(r2));
418                    }
419                }
420            }
421        }
422    }
423}
424
425impl<C: NonMalleable + SafeParser, N: AsLen> NonMalleable for super::RepeatN<C, N> {
426    open spec fn nonmal_inv(&self) -> bool {
427        &&& self.1.nonmal_inv()
428        &&& self.1.safe_inv()
429    }
430
431    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
432        assert(self.nonmal_inv());
433        self.lemma_parse_non_malleable_rec(self.0.as_nat(), buf1, buf2);
434    }
435}
436
437impl<C: NoLookAhead, N: AsLen> super::RepeatN<C, N> {
438    proof fn lemma_no_lookahead_rec(&self, count: nat, i1: Seq<u8>, i2: Seq<u8>)
439        requires
440            self.1.safe_inv(),
441            self.1.no_lookahead_inv(),
442        ensures
443            self.parse_n_rec(count, i1) matches Some((n, v)) ==> 0 <= n <= i2.len() ==> i2.take(n)
444                == i1.take(n) ==> self.parse_n_rec(count, i2) == Some((n, v)),
445        decreases count,
446    {
447        use crate::combinators::tuple::proof::lemma_take_skip;
448        broadcast use vstd::seq_lib::group_seq_properties;
449
450        if count == 0 {
451        } else {
452            if let Some((n, v)) = self.parse_n_rec(count, i1) {
453                if 0 <= n <= i2.len() {
454                    if i2.take(n) == i1.take(n) {
455                        let (m, a) = self.1.spec_parse(i1)->0;
456                        let (r, rest) = self.parse_n_rec((count - 1) as nat, i1.skip(m))->0;
457                        assert(v == seq![a] + rest);
458                        assert(n == m + r);
459                        self.1.lemma_parse_safe(i1);
460                        self.lemma_parse_n_len_bound((count - 1) as nat, i1.skip(m));
461                        assert(0 <= m <= n);
462                        assert(i2.take(m) == i1.take(m));
463                        self.1.lemma_no_lookahead(i1, i2);
464                        assert(i2.skip(m).take(r) == i1.skip(m).take(r)) by {
465                            lemma_take_skip(i1, m, r);
466                            lemma_take_skip(i2, m, r);
467                        };
468                        self.lemma_no_lookahead_rec((count - 1) as nat, i1.skip(m), i2.skip(m));
469                    }
470                }
471            }
472        }
473    }
474}
475
476impl<C: NoLookAhead, N: AsLen> NoLookAhead for super::RepeatN<C, N> {
477    open spec fn no_lookahead_inv(&self) -> bool {
478        self.1.no_lookahead_inv()
479    }
480
481    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
482        self.lemma_no_lookahead_rec(self.0.as_nat(), i1, i2);
483    }
484}
485
486impl<A: SpecParser> super::Star<A> {
487    proof fn lemma_parse_rec_nonnegative(&self, ibuf: Seq<u8>)
488        ensures
489            0 <= self.parse_rec(ibuf).0,
490        decreases ibuf.len(),
491    {
492        if let Some((n, _v)) = self.0.spec_parse(ibuf) {
493            if 0 < n <= ibuf.len() {
494                self.lemma_parse_rec_nonnegative(ibuf.skip(n));
495            }
496        }
497    }
498}
499
500impl<C: Productive, N: AsLen> super::RepeatN<C, N> {
501    proof fn lemma_parse_n_positive(&self, count: nat, ibuf: Seq<u8>)
502        requires
503            self.1.productive_inv(),
504            self.1.safe_inv(),
505            count > 0,
506        ensures
507            self.parse_n_rec(count, ibuf) matches Some((n, _)) ==> n > 0,
508        decreases count,
509    {
510        if let Some((n0, _v0)) = self.1.spec_parse(ibuf) {
511            self.1.lemma_productive(ibuf);
512            if let Some((n1, _rest)) = self.parse_n_rec((count - 1) as nat, ibuf.skip(n0)) {
513                if count - 1 > 0 {
514                    self.lemma_parse_n_positive((count - 1) as nat, ibuf.skip(n0));
515                    assert(n1 > 0);
516                } else {
517                    assert(n1 == 0);
518                }
519                assert(n0 > 0);
520                assert(n0 + n1 > 0);
521            }
522        }
523    }
524}
525
526impl<C: Productive, N: AsLen> Productive for super::RepeatN<C, N> {
527    open spec fn productive_inv(&self) -> bool {
528        &&& self.0.as_nat() > 0
529        &&& self.1.productive_inv()
530    }
531
532    proof fn lemma_productive(&self, s: Seq<u8>) {
533        if let Some((n, _v)) = self.spec_parse(s) {
534            self.lemma_parse_n_positive(self.0.as_nat(), s);
535            assert(n > 0);
536        }
537    }
538}
539
540impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializersGeneral for super::RepeatN<C, N> {
541    open spec fn equiv_general_inv(&self) -> bool {
542        self.1.equiv_general_inv()
543    }
544
545    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
546        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
547        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
548        super::Star(self.1).lemma_serialize_equiv(v, obuf);
549    }
550}
551
552impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializers for super::RepeatN<C, N> {
553    open spec fn equiv_inv(&self) -> bool {
554        self.1.equiv_general_inv()
555    }
556
557    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
558        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
559        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
560        super::Star(self.1).lemma_serialize_equiv_on_empty(v);
561    }
562}
563
564impl<const N: usize, C> SPRoundTripDps for super::Array<N, C> where C: SPRoundTripDps + NonTailFmt {
565    open spec fn unambiguous(&self) -> bool {
566        super::RepeatN(N, self.0).unambiguous()
567    }
568
569    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
570        super::RepeatN(N, self.0).theorem_serialize_dps_parse_roundtrip(v, obuf);
571    }
572}
573
574impl<const N: usize, C: NonMalleable> NonMalleable for super::Array<N, C> {
575    open spec fn nonmal_inv(&self) -> bool {
576        super::RepeatN(N, self.0).nonmal_inv()
577    }
578
579    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
580        super::RepeatN(N, self.0).lemma_parse_non_malleable(buf1, buf2);
581    }
582}
583
584impl<const N: usize, C: NoLookAhead> NoLookAhead for super::Array<N, C> {
585    open spec fn no_lookahead_inv(&self) -> bool {
586        self.0.no_lookahead_inv()
587    }
588
589    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
590        super::RepeatN(N, self.0).lemma_no_lookahead(i1, i2);
591    }
592}
593
594impl<const N: usize, C: Productive> Productive for super::Array<N, C> {
595    open spec fn productive_inv(&self) -> bool {
596        super::RepeatN(N, self.0).productive_inv()
597    }
598
599    proof fn lemma_productive(&self, s: Seq<u8>) {
600        super::RepeatN(N, self.0).lemma_productive(s);
601    }
602}
603
604impl<const N: usize, C: EquivSerializersGeneral> EquivSerializersGeneral for super::Array<N, C> {
605    open spec fn equiv_general_inv(&self) -> bool {
606        self.0.equiv_general_inv()
607    }
608
609    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
610        super::RepeatN(N, self.0).lemma_serialize_equiv(v, obuf);
611    }
612}
613
614impl<const N: usize, C: EquivSerializersGeneral> EquivSerializers for super::Array<N, C> {
615    open spec fn equiv_inv(&self) -> bool {
616        self.0.equiv_general_inv()
617    }
618
619    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
620        super::RepeatN(N, self.0).lemma_serialize_equiv_on_empty(v);
621    }
622}
623
624impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for super::Repeat<A, B> {
625    open spec fn unambiguous(&self) -> bool {
626        &&& self.0.serialize_dps_inv()
627        &&& self.0.unambiguous()
628        &&& self.1.unambiguous()
629        &&& disjoint_domains(self.0, self.1)
630    }
631
632    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
633        assert(self.unambiguous());
634        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
635        let star = super::Star(self.0);
636        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
637        self.1.theorem_serialize_dps_parse_roundtrip(v.1, obuf);
638        assert(parser_fails_on(self.0, serialized1)) by {
639            reveal(disjoint_domains);
640            assert(self.1.spec_parse(serialized1) is Some);
641        }
642        let serialized0 = star.spec_serialize_dps(v.0, serialized1);
643        star.lemma_serialize_parse_roundtrip_rec(v.0, serialized1);
644        let n0 = serialized0.len() - serialized1.len();
645        star.lemma_serialize_dps_prepend(v.0, serialized1);
646        star.lemma_serialize_dps_len(v.0, serialized1);
647        assert(serialized0.skip(n0) == serialized1);
648    }
649}
650
651// impl<
652//     A: PSRoundTrip + GoodSerializerDps + EquivSerializersGeneral,
653//     B: PSRoundTrip,
654// > PSRoundTrip for super::Repeat<A, B> {
655// }
656impl<A: NonMalleable, B: NonMalleable> NonMalleable for super::Repeat<A, B> {
657    open spec fn nonmal_inv(&self) -> bool {
658        Pair(super::Star(self.0), self.1).nonmal_inv()
659    }
660
661    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
662        Pair(super::Star(self.0), self.1).lemma_parse_non_malleable(buf1, buf2);
663    }
664}
665
666impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for super::Repeat<A, B> {
667    open spec fn no_lookahead_inv(&self) -> bool {
668        &&& self.0.no_lookahead_inv()
669        &&& self.1.no_lookahead_inv()
670        &&& disjoint_domains(self.0, self.1)
671    }
672
673    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
674        reveal(disjoint_domains);
675        reveal(<super::Star::<_> as SpecParser>::spec_parse);
676        use crate::combinators::tuple::proof::lemma_take_skip;
677        broadcast use vstd::seq_lib::group_seq_properties;
678
679        let star = super::Star(self.0);
680        self.lemma_parse_safe(i1);
681        if let Some((n, v)) = self.spec_parse(i1) {
682            if 0 <= n <= i2.len() {
683                if i2.take(n) == i1.take(n) {
684                    if let Some((n0, v0)) = star.spec_parse(i1) {
685                        if let Some((n1, v1)) = self.1.spec_parse(i1.skip(n0)) {
686                            star.lemma_parse_safe(i1);
687                            self.1.lemma_parse_safe(i1.skip(n0));
688                            assert(i2.take(n0) == i1.take(n0));
689                            assert(i2.skip(n0).take(n1) == i1.skip(n0).take(n1)) by {
690                                lemma_take_skip(i1, n0, n1);
691                                lemma_take_skip(i2, n0, n1);
692                            };
693                            self.1.lemma_no_lookahead(i1.skip(n0), i2.skip(n0));
694                            assert(disjoint_domains(self.0, self.1));
695                            star.lemma_parse_rec_no_lookahead_conditional(i1, i2);
696                        }
697                    }
698                }
699            }
700        }
701    }
702}
703
704impl<A: SafeParser, B: Productive> Productive for super::Repeat<A, B> {
705    open spec fn productive_inv(&self) -> bool {
706        self.1.productive_inv()
707    }
708
709    proof fn lemma_productive(&self, s: Seq<u8>) {
710        reveal(<super::Star::<_> as SpecParser>::spec_parse);
711        let star = super::Star(self.0);
712        if let Some((n, _v)) = self.spec_parse(s) {
713            let (n0, _vs) = star.spec_parse(s)->0;
714            let (n1, _b) = self.1.spec_parse(s.skip(n0))->0;
715            star.lemma_parse_rec_nonnegative(s);
716            self.1.lemma_productive(s.skip(n0));
717            assert(n1 > 0);
718            assert(n == n0 + n1);
719            assert(n > 0);
720        }
721    }
722}
723
724impl<
725    A: EquivSerializersGeneral,
726    B: EquivSerializersGeneral,
727> EquivSerializersGeneral for super::Repeat<A, B> {
728    open spec fn equiv_general_inv(&self) -> bool {
729        &&& self.0.equiv_general_inv()
730        &&& self.1.equiv_general_inv()
731    }
732
733    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
734        Pair(super::Star(self.0), self.1).lemma_serialize_equiv(v, obuf);
735    }
736}
737
738impl<A: EquivSerializersGeneral, B: EquivSerializers> EquivSerializers for super::Repeat<A, B> {
739    open spec fn equiv_inv(&self) -> bool {
740        &&& self.0.equiv_general_inv()
741        &&& self.1.equiv_inv()
742    }
743
744    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
745        assert(self.equiv_inv());
746        Pair(super::Star(self.0), self.1).lemma_serialize_equiv_on_empty(v);
747    }
748}
749
750} // verus!
vest_lib/combinators/star/proof.rs

vest_lib/combinators/star/
proof.rs
