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[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[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[0..n1] == buf2[0..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[m1..]);
95                        let (n2_rest, rest2) = self.parse_rec(buf2[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[1..]);
107                            assert(rest2 == v2[1..]);
108                        }
109
110                        // base
111                        self.0.lemma_parse_non_malleable(buf1, buf2);
112                        assert(buf1[0..m1] == buf2[0..m2]);
113
114                        // induction
115                        assert(self.safe_inv());
116                        self.lemma_parse_non_malleable_rec(buf1[m1..], buf2[m2..]);
117                        assert(buf1[m1..][0..n1_rest] == buf2[m2..][0..n2_rest]);
118
119                        // need to show buf1[0..n1] == buf2[0..n2]
120                        assert(self.safe_inv());
121                        self.lemma_parse_safe(buf1[m1..]);
122                        self.lemma_parse_safe(buf2[m2..]);
123                        assert(buf1[0..n1] == buf1[0..m1] + buf1[m1..][0..n1_rest]);
124                        assert(buf2[0..n2] == buf2[0..m2] + buf2[m2..][0..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[self.parse_rec(i1).0..]),
162        ensures
163            ({
164                let r = self.parse_rec(i1);
165                0 <= r.0 <= i2.len() ==> i2[0..r.0] == i1[0..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[m..];
177                let i2_rest = i2[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[0..n] == i1[0..n] {
183                        assert(i2[0..m] == i1[0..m]);
184                        assert(self.0.safe_inv());
185                        self.0.lemma_no_lookahead(i1, i2);
186                        assert(i2_rest[0..n_rest] == i1_rest[0..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[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[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        assert(self.equiv_inv() == self.0.equiv_general_inv());
321        self.lemma_serialize_equiv_rec(v, Seq::empty());
322    }
323}
324
325impl<C, N> super::RepeatN<C, N> where C: SPRoundTripDps + NonTailFmt, N: AsLen {
326    proof fn lemma_serialize_parse_roundtrip_rec(&self, vs: Seq<C::PVal>, count: nat, obuf: Seq<u8>)
327        requires
328            self.1.serialize_dps_inv(),
329            self.1.unambiguous(),
330            vs.len() == count,
331            (super::Star(self.1).consistent(vs)),
332        ensures
333            self.parse_n_rec(count, self.spec_serialize_dps(vs, obuf)) == Some(
334                ((self.spec_serialize_dps(vs, obuf).len() - obuf.len()) as int, vs),
335            ),
336        decreases count,
337    {
338        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
339        reveal(<super::Star::<_> as Consistency>::consistent);
340        if count == 0 {
341        } else {
342            let v0 = vs[0];
343            let rest = vs[1..];
344            let rest_buf = self.spec_serialize_dps(rest, obuf);
345            let serialized = self.spec_serialize_dps(vs, obuf);
346
347            self.lemma_serialize_parse_roundtrip_rec(rest, (count - 1) as nat, obuf);
348
349            self.1.theorem_serialize_dps_parse_roundtrip(v0, rest_buf);
350            self.1.lemma_serialize_dps_prepend(v0, rest_buf);
351            self.1.lemma_serialize_dps_len(v0, rest_buf);
352
353            let n0 = (serialized.len() - rest_buf.len()) as int;
354            assert(serialized[n0..] == rest_buf);
355        }
356    }
357}
358
359impl<C, N> SPRoundTripDps for super::RepeatN<C, N> where C: SPRoundTripDps + NonTailFmt, N: AsLen {
360    open spec fn unambiguous(&self) -> bool {
361        &&& self.1.serialize_dps_inv()
362        &&& self.1.unambiguous()
363    }
364
365    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
366        self.lemma_serialize_parse_roundtrip_rec(v, self.0.as_nat(), obuf);
367        self.lemma_serialize_dps_len(v, obuf);
368    }
369}
370
371impl<C: NonMalleable, N: AsLen> super::RepeatN<C, N> {
372    #[verusfmt::skip]
373    proof fn lemma_parse_non_malleable_rec(&self, count: nat, buf1: Seq<u8>, buf2: Seq<u8>)
374        requires
375            self.1.nonmal_inv(),
376            self.1.safe_inv(),
377        ensures
378            self.parse_n_rec(count, buf1) matches Some((n1, v1)) ==>
379            self.parse_n_rec(count, buf2) matches Some((n2, v2)) ==>
380            v1 == v2 ==> buf1[0..n1] == buf2[0..n2],
381        decreases count,
382    {
383        broadcast use vstd::seq_lib::group_seq_properties;
384
385        if count == 0 {
386        } else {
387            if let Some((n1, v1)) = self.parse_n_rec(count, buf1) {
388                if let Some((n2, v2)) = self.parse_n_rec(count, buf2) {
389                    if v1 == v2 {
390                        let (m1, a1) = self.1.spec_parse(buf1)->0;
391                        let (m2, a2) = self.1.spec_parse(buf2)->0;
392                        let (r1, rest1) = self.parse_n_rec((count - 1) as nat, buf1[m1..])->0;
393                        let (r2, rest2) = self.parse_n_rec((count - 1) as nat, buf2[m2..])->0;
394                        assert(v1 == seq![a1] + rest1);
395                        assert(v2 == seq![a2] + rest2);
396                        assert(a1 == a2) by {
397                            assert(a1 == v1[0]);
398                            assert(a2 == v2[0]);
399                        }
400                        assert(rest1 == rest2) by {
401                            assert(rest1 == v1[1..]);
402                            assert(rest2 == v2[1..]);
403                        }
404
405                        self.1.lemma_parse_safe(buf1);
406                        self.1.lemma_parse_safe(buf2);
407                        self.lemma_parse_n_len_bound((count - 1) as nat, buf1[m1..]);
408                        self.lemma_parse_n_len_bound((count - 1) as nat, buf2[m2..]);
409                        self.1.lemma_parse_non_malleable(buf1, buf2);
410                        assert(buf1[0..m1] == buf2[0..m2]);
411
412                        self.lemma_parse_non_malleable_rec((count - 1) as nat, buf1[m1..], buf2[m2..]);
413                        assert(buf1[m1..][0..r1] == buf2[m2..][0..r2]);
414
415                        assert(n1 == m1 + r1);
416                        assert(n2 == m2 + r2);
417                        assert(buf1[0..n1] == buf1[0..m1] + buf1[m1..][0..r1]);
418                        assert(buf2[0..n2] == buf2[0..m2] + buf2[m2..][0..r2]);
419                    }
420                }
421            }
422        }
423    }
424}
425
426impl<C: NonMalleable + SafeParser, N: AsLen> NonMalleable for super::RepeatN<C, N> {
427    open spec fn nonmal_inv(&self) -> bool {
428        &&& self.1.nonmal_inv()
429        &&& self.1.safe_inv()
430    }
431
432    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
433        assert(self.nonmal_inv());
434        self.lemma_parse_non_malleable_rec(self.0.as_nat(), buf1, buf2);
435    }
436}
437
438impl<C: NoLookAhead, N: AsLen> super::RepeatN<C, N> {
439    proof fn lemma_no_lookahead_rec(&self, count: nat, i1: Seq<u8>, i2: Seq<u8>)
440        requires
441            self.1.safe_inv(),
442            self.1.no_lookahead_inv(),
443        ensures
444            self.parse_n_rec(count, i1) matches Some((n, v)) ==> 0 <= n <= i2.len() ==> i2[0..n]
445                == i1[0..n] ==> self.parse_n_rec(count, i2) == Some((n, v)),
446        decreases count,
447    {
448        use crate::combinators::tuple::proof::lemma_take_skip;
449        broadcast use vstd::seq_lib::group_seq_properties;
450
451        if count == 0 {
452        } else {
453            if let Some((n, v)) = self.parse_n_rec(count, i1) {
454                if 0 <= n <= i2.len() {
455                    if i2[0..n] == i1[0..n] {
456                        let (m, a) = self.1.spec_parse(i1)->0;
457                        let (r, rest) = self.parse_n_rec((count - 1) as nat, i1[m..])->0;
458                        assert(v == seq![a] + rest);
459                        assert(n == m + r);
460                        self.1.lemma_parse_safe(i1);
461                        self.lemma_parse_n_len_bound((count - 1) as nat, i1[m..]);
462                        assert(0 <= m <= n);
463                        assert(i2[0..m] == i1[0..m]);
464                        self.1.lemma_no_lookahead(i1, i2);
465                        assert(i2[m..][0..r] == i1[m..][0..r]) by {
466                            lemma_take_skip(i1, m, r);
467                            lemma_take_skip(i2, m, r);
468                        };
469                        self.lemma_no_lookahead_rec((count - 1) as nat, i1[m..], i2[m..]);
470                    }
471                }
472            }
473        }
474    }
475}
476
477impl<C: NoLookAhead, N: AsLen> NoLookAhead for super::RepeatN<C, N> {
478    open spec fn no_lookahead_inv(&self) -> bool {
479        self.1.no_lookahead_inv()
480    }
481
482    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
483        self.lemma_no_lookahead_rec(self.0.as_nat(), i1, i2);
484    }
485}
486
487impl<A: SpecParser> super::Star<A> {
488    proof fn lemma_parse_rec_nonnegative(&self, ibuf: Seq<u8>)
489        ensures
490            0 <= self.parse_rec(ibuf).0,
491        decreases ibuf.len(),
492    {
493        if let Some((n, _v)) = self.0.spec_parse(ibuf) {
494            if 0 < n <= ibuf.len() {
495                self.lemma_parse_rec_nonnegative(ibuf[n..]);
496            }
497        }
498    }
499}
500
501impl<C: Productive, N: AsLen> super::RepeatN<C, N> {
502    proof fn lemma_parse_n_positive(&self, count: nat, ibuf: Seq<u8>)
503        requires
504            self.1.productive_inv(),
505            self.1.safe_inv(),
506            count > 0,
507        ensures
508            self.parse_n_rec(count, ibuf) matches Some((n, _)) ==> n > 0,
509        decreases count,
510    {
511        if let Some((n0, _v0)) = self.1.spec_parse(ibuf) {
512            self.1.lemma_productive(ibuf);
513            if let Some((n1, _rest)) = self.parse_n_rec((count - 1) as nat, ibuf[n0..]) {
514                if count - 1 > 0 {
515                    self.lemma_parse_n_positive((count - 1) as nat, ibuf[n0..]);
516                    assert(n1 > 0);
517                } else {
518                    assert(n1 == 0);
519                }
520                assert(n0 > 0);
521                assert(n0 + n1 > 0);
522            }
523        }
524    }
525}
526
527impl<C: Productive, N: AsLen> Productive for super::RepeatN<C, N> {
528    open spec fn productive_inv(&self) -> bool {
529        &&& self.0.as_nat() > 0
530        &&& self.1.productive_inv()
531    }
532
533    proof fn lemma_productive(&self, s: Seq<u8>) {
534        if let Some((n, _v)) = self.spec_parse(s) {
535            self.lemma_parse_n_positive(self.0.as_nat(), s);
536            assert(n > 0);
537        }
538    }
539}
540
541impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializersGeneral for super::RepeatN<C, N> {
542    open spec fn equiv_general_inv(&self) -> bool {
543        self.1.equiv_general_inv()
544    }
545
546    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
547        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
548        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
549        super::Star(self.1).lemma_serialize_equiv(v, obuf);
550    }
551}
552
553impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializers for super::RepeatN<C, N> {
554    open spec fn equiv_inv(&self) -> bool {
555        self.1.equiv_general_inv()
556    }
557
558    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
559        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
560        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
561        super::Star(self.1).lemma_serialize_equiv_on_empty(v);
562    }
563}
564
565impl<const N: usize, C> SPRoundTripDps for super::Array<N, C> where C: SPRoundTripDps + NonTailFmt {
566    open spec fn unambiguous(&self) -> bool {
567        super::RepeatN(N, self.0).unambiguous()
568    }
569
570    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
571        super::RepeatN(N, self.0).theorem_serialize_dps_parse_roundtrip(v, obuf);
572    }
573}
574
575impl<const N: usize, C: NonMalleable> NonMalleable for super::Array<N, C> {
576    open spec fn nonmal_inv(&self) -> bool {
577        super::RepeatN(N, self.0).nonmal_inv()
578    }
579
580    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
581        super::RepeatN(N, self.0).lemma_parse_non_malleable(buf1, buf2);
582    }
583}
584
585impl<const N: usize, C: NoLookAhead> NoLookAhead for super::Array<N, C> {
586    open spec fn no_lookahead_inv(&self) -> bool {
587        self.0.no_lookahead_inv()
588    }
589
590    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
591        super::RepeatN(N, self.0).lemma_no_lookahead(i1, i2);
592    }
593}
594
595impl<const N: usize, C: Productive> Productive for super::Array<N, C> {
596    open spec fn productive_inv(&self) -> bool {
597        super::RepeatN(N, self.0).productive_inv()
598    }
599
600    proof fn lemma_productive(&self, s: Seq<u8>) {
601        super::RepeatN(N, self.0).lemma_productive(s);
602    }
603}
604
605impl<const N: usize, C: EquivSerializersGeneral> EquivSerializersGeneral for super::Array<N, C> {
606    open spec fn equiv_general_inv(&self) -> bool {
607        self.0.equiv_general_inv()
608    }
609
610    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
611        super::RepeatN(N, self.0).lemma_serialize_equiv(v, obuf);
612    }
613}
614
615impl<const N: usize, C: EquivSerializersGeneral> EquivSerializers for super::Array<N, C> {
616    open spec fn equiv_inv(&self) -> bool {
617        self.0.equiv_general_inv()
618    }
619
620    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
621        super::RepeatN(N, self.0).lemma_serialize_equiv_on_empty(v);
622    }
623}
624
625impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for super::Repeat<A, B> {
626    open spec fn unambiguous(&self) -> bool {
627        &&& self.0.serialize_dps_inv()
628        &&& self.0.unambiguous()
629        &&& self.1.unambiguous()
630        &&& disjoint_domains(self.0, self.1)
631    }
632
633    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
634        assert(self.unambiguous());
635        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
636        let star = super::Star(self.0);
637        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
638        self.1.theorem_serialize_dps_parse_roundtrip(v.1, obuf);
639        assert(parser_fails_on(self.0, serialized1)) by {
640            reveal(disjoint_domains);
641            assert(self.1.spec_parse(serialized1) is Some);
642        }
643        let serialized0 = star.spec_serialize_dps(v.0, serialized1);
644        star.lemma_serialize_parse_roundtrip_rec(v.0, serialized1);
645        let n0 = serialized0.len() - serialized1.len();
646        star.lemma_serialize_dps_prepend(v.0, serialized1);
647        star.lemma_serialize_dps_len(v.0, serialized1);
648        assert(serialized0[n0..] == serialized1);
649    }
650}
651
652// impl<
653//     A: PSRoundTrip + GoodSerializerDps + EquivSerializersGeneral,
654//     B: PSRoundTrip,
655// > PSRoundTrip for super::Repeat<A, B> {
656// }
657impl<A: NonMalleable, B: NonMalleable> NonMalleable for super::Repeat<A, B> {
658    open spec fn nonmal_inv(&self) -> bool {
659        Pair(super::Star(self.0), self.1).nonmal_inv()
660    }
661
662    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
663        Pair(super::Star(self.0), self.1).lemma_parse_non_malleable(buf1, buf2);
664    }
665}
666
667impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for super::Repeat<A, B> {
668    open spec fn no_lookahead_inv(&self) -> bool {
669        &&& self.0.no_lookahead_inv()
670        &&& self.1.no_lookahead_inv()
671        &&& disjoint_domains(self.0, self.1)
672    }
673
674    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
675        reveal(disjoint_domains);
676        reveal(<super::Star::<_> as SpecParser>::spec_parse);
677        use crate::combinators::tuple::proof::lemma_take_skip;
678        broadcast use vstd::seq_lib::group_seq_properties;
679
680        let star = super::Star(self.0);
681        self.lemma_parse_safe(i1);
682        if let Some((n, v)) = self.spec_parse(i1) {
683            if 0 <= n <= i2.len() {
684                if i2[0..n] == i1[0..n] {
685                    if let Some((n0, v0)) = star.spec_parse(i1) {
686                        if let Some((n1, v1)) = self.1.spec_parse(i1[n0..]) {
687                            star.lemma_parse_safe(i1);
688                            self.1.lemma_parse_safe(i1[n0..]);
689                            assert(i2[0..n0] == i1[0..n0]);
690                            assert(i2[n0..][0..n1] == i1[n0..][0..n1]) by {
691                                lemma_take_skip(i1, n0, n1);
692                                lemma_take_skip(i2, n0, n1);
693                            };
694                            self.1.lemma_no_lookahead(i1[n0..], i2[n0..]);
695                            assert(disjoint_domains(self.0, self.1));
696                            star.lemma_parse_rec_no_lookahead_conditional(i1, i2);
697                        }
698                    }
699                }
700            }
701        }
702    }
703}
704
705impl<A: SafeParser, B: Productive> Productive for super::Repeat<A, B> {
706    open spec fn productive_inv(&self) -> bool {
707        self.1.productive_inv()
708    }
709
710    proof fn lemma_productive(&self, s: Seq<u8>) {
711        reveal(<super::Star::<_> as SpecParser>::spec_parse);
712        let star = super::Star(self.0);
713        if let Some((n, _v)) = self.spec_parse(s) {
714            let (n0, _vs) = star.spec_parse(s)->0;
715            let (n1, _b) = self.1.spec_parse(s[n0..])->0;
716            star.lemma_parse_rec_nonnegative(s);
717            self.1.lemma_productive(s[n0..]);
718            assert(n1 > 0);
719            assert(n == n0 + n1);
720            assert(n > 0);
721        }
722    }
723}
724
725impl<
726    A: EquivSerializersGeneral,
727    B: EquivSerializersGeneral,
728> EquivSerializersGeneral for super::Repeat<A, B> {
729    open spec fn equiv_general_inv(&self) -> bool {
730        &&& self.0.equiv_general_inv()
731        &&& self.1.equiv_general_inv()
732    }
733
734    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
735        Pair(super::Star(self.0), self.1).lemma_serialize_equiv(v, obuf);
736    }
737}
738
739impl<A: EquivSerializersGeneral, B: EquivSerializers> EquivSerializers for super::Repeat<A, B> {
740    open spec fn equiv_inv(&self) -> bool {
741        &&& self.0.equiv_general_inv()
742        &&& self.1.equiv_inv()
743    }
744
745    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
746        assert(self.equiv_inv());
747        Pair(super::Star(self.0), self.1).lemma_serialize_equiv_on_empty(v);
748    }
749}
750
751} // verus!
vest_lib/combinators/star/proof.rs

vest_lib/combinators/star/
proof.rs
