vest_lib/combinators/star/
spec.rs

1//! Specifications for zero-or-more repetition.
2use crate::combinators::length::AsLen;
3use crate::combinators::Pair;
4use crate::core::{proof::*, spec::*};
5use vstd::calc;
6use vstd::prelude::*;
7
8verus! {
9
10proof fn lemma_static_seq_byte_len<A: StaticByteLen>(inner: A, vs: Seq<A::T>)
11    requires
12        forall|i: int| 0 <= i < vs.len() ==> #[trigger] inner.consistent(vs[i]),
13    ensures
14        (super::Star(inner)).byte_len(vs) == vs.len() * A::static_byte_len(),
15    decreases vs.len(),
16{
17    let star = super::Star(inner);
18    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
19    if vs.len() == 0 {
20    } else {
21        let v0 = vs[0];
22        let rest = vs.skip(1);
23        let k = A::static_byte_len();
24        assert(vs == seq![v0] + rest);
25        star.lemma_byte_len_cons(v0, rest);
26        inner.lemma_static_len_matches_byte_len(v0);
27        lemma_static_seq_byte_len(inner, rest);
28        assert(k + rest.len() * k == (rest.len() + 1) * k) by (nonlinear_arith);
29    }
30}
31
32proof fn lemma_value_seq_byte_len<A: ValueByteLen>(inner: A, vs: Seq<A::T>)
33    requires
34        forall|i: int| 0 <= i < vs.len() ==> #[trigger] inner.consistent(vs[i]),
35    ensures
36        (super::Star(inner)).byte_len(vs) == vs.fold_left(
37            0,
38            |acc: nat, elem| acc + A::value_byte_len(elem),
39        ),
40    decreases vs.len(),
41{
42    use crate::combinators::star::proof::lemma_fold_left_accumulate_nat;
43
44    let star = super::Star(inner);
45    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
46    if vs.len() == 0 {
47    } else {
48        let v0 = vs[0];
49        let rest = vs.skip(1);
50        let g = |acc: nat, elem: A::T| acc + A::value_byte_len(elem);
51
52        assert(vs == seq![v0] + rest);
53        star.lemma_byte_len_cons(v0, rest);
54        lemma_value_seq_byte_len(inner, rest);
55        inner.lemma_value_len_matches_byte_len(v0);
56        assert(star.byte_len(rest) == rest.fold_left(0, g));
57        lemma_fold_left_accumulate_nat(rest, A::value_byte_len(v0), g);
58        rest.lemma_fold_left_alt(A::value_byte_len(v0), g);
59        (seq![v0] + rest).lemma_fold_left_alt(0, g);
60        calc! {
61            (==)
62            star.byte_len(vs); {}
63            inner.byte_len(v0) + star.byte_len(rest); {}
64            A::value_byte_len(v0) + rest.fold_left(0, g); {}
65            rest.fold_left(A::value_byte_len(v0), g); {}
66            rest.fold_left_alt(A::value_byte_len(v0), g); {}
67            (seq![v0] + rest).fold_left_alt(0, g); {}
68            (seq![v0] + rest).fold_left(0, g); {}
69            vs.fold_left(0, g);
70        }
71    }
72}
73
74proof fn lemma_seq_min_max_byte_len<A: MinMaxByteLen>(inner: A, vs: Seq<A::T>)
75    requires
76        forall|i: int| 0 <= i < vs.len() ==> #[trigger] inner.consistent(vs[i]),
77    ensures
78        vs.len() * inner.min() <= (super::Star(inner)).byte_len(vs) <= vs.len() * inner.max(),
79    decreases vs.len(),
80{
81    let star = super::Star(inner);
82    reveal(<super::Star::<_> as SpecByteLen>::byte_len);
83    if vs.len() == 0 {
84    } else {
85        let v0 = vs[0];
86        let rest = vs.skip(1);
87        assert(vs == seq![v0] + rest);
88        inner.lemma_min_max_byte_len(v0);
89        lemma_seq_min_max_byte_len(inner, rest);
90        star.lemma_byte_len_cons(v0, rest);
91        assert((rest.len() + 1) * inner.min() == rest.len() * inner.min() + inner.min())
92            by (nonlinear_arith);
93        assert((rest.len() + 1) * inner.max() == rest.len() * inner.max() + inner.max())
94            by (nonlinear_arith);
95    }
96}
97
98impl<A: SpecParser> super::Star<A> {
99    /// Recursive helper function for parsing.
100    /// Since `Star` always succeeds, this function is total.
101    pub open spec fn parse_rec(&self, ibuf: Seq<u8>) -> (int, Seq<A::PVal>)
102        decreases ibuf.len(),
103    {
104        match self.0.spec_parse(ibuf) {
105            Some((n, v)) if 0 < n <= ibuf.len() => {
106                let (n_rest, vs) = self.parse_rec(ibuf.skip(n));
107                (n + n_rest, seq![v] + vs)
108            },
109            _ => (0, Seq::empty()),
110        }
111    }
112}
113
114impl<A: SpecByteLen> super::Star<A> {
115    pub proof fn lemma_byte_len_cons(&self, v: A::T, vs: Seq<A::T>)
116        ensures
117            self.byte_len(seq![v] + vs) == self.0.byte_len(v) + self.byte_len(vs),
118    {
119        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
120        use crate::combinators::star::proof::lemma_fold_left_accumulate_nat;
121
122        let f = |acc: nat, elem: A::T| acc + self.0.byte_len(elem);
123        (seq![v] + vs).lemma_fold_left_alt(0, f);
124        vs.lemma_fold_left_alt(self.0.byte_len(v), f);
125        lemma_fold_left_accumulate_nat(vs, self.0.byte_len(v), f);
126        assert((seq![v] + vs).skip(1) == vs);
127    }
128}
129
130impl<A: SpecSerializer + Copy> super::Star<A> {
131    /// Serializing a nonempty sequence is the serialization of its first value followed by the
132    /// serialization of the remaining values.
133    pub proof fn lemma_spec_serialize_cons(&self, first: A::SVal, rest: Seq<A::SVal>)
134        ensures
135            self.spec_serialize(seq![first] + rest) == self.0.spec_serialize(first)
136                + self.spec_serialize(rest),
137    {
138        use crate::combinators::star::proof::lemma_fold_left_accumulate_seq;
139        reveal(<super::Star<_> as SpecSerializer>::spec_serialize);
140
141        let f = |acc: Seq<u8>, elem: A::SVal| acc + self.0.spec_serialize(elem);
142        let values = seq![first] + rest;
143        assert(values.len() > 0);
144        assert(values[0] == first);
145        assert(values.skip(1) =~= rest);
146        assert forall|acc: Seq<u8>, x: Seq<u8>, y: A::SVal| #[trigger]
147            f(acc + x, y) == acc + #[trigger] f(x, y) by {}
148        values.lemma_fold_left_alt(Seq::empty(), f);
149        rest.lemma_fold_left_alt(self.0.spec_serialize(first), f);
150        lemma_fold_left_accumulate_seq(rest, self.0.spec_serialize(first), f);
151    }
152
153    /// Decomposes the serialization suffix beginning at `i`.
154    pub proof fn lemma_spec_serialize_suffix_step(&self, vs: Seq<A::SVal>, i: int)
155        requires
156            0 <= i < vs.len(),
157        ensures
158            self.spec_serialize(vs.skip(i)) == self.0.spec_serialize(vs[i]) + self.spec_serialize(
159                vs.skip(i + 1),
160            ),
161    {
162        assert(vs.skip(i) =~= seq![vs[i]] + vs.skip(i + 1));
163        self.lemma_spec_serialize_cons(vs[i], vs.skip(i + 1));
164    }
165}
166
167impl<A: SafeParser> super::Star<A> {
168    proof fn lemma_parse_rec_length(&self, ibuf: Seq<u8>)
169        requires
170            self.0.safe_inv(),
171        ensures
172            0 <= self.parse_rec(ibuf).0 <= ibuf.len(),
173        decreases ibuf.len(),
174    {
175        self.0.lemma_parse_safe(ibuf);
176        if let Some((n, v)) = self.0.spec_parse(ibuf) {
177            if 0 < n <= ibuf.len() {
178                self.lemma_parse_rec_length(ibuf.skip(n));
179            }
180        }
181    }
182}
183
184impl<A: SoundParser> super::Star<A> {
185    proof fn lemma_parse_rec_consistent(&self, ibuf: Seq<u8>)
186        requires
187            self.0.sound_inv(),
188        ensures
189            self.consistent(self.parse_rec(ibuf).1),
190        decreases ibuf.len(),
191    {
192        reveal(<super::Star::<_> as Consistency>::consistent);
193        self.0.lemma_parse_sound_value(ibuf);
194        if let Some((n, v)) = self.0.spec_parse(ibuf) {
195            if 0 < n <= ibuf.len() {
196                self.lemma_parse_rec_consistent(ibuf.skip(n));
197            }
198        }
199    }
200
201    proof fn lemma_parse_rec_byte_len(&self, ibuf: Seq<u8>)
202        requires
203            self.0.sound_inv(),
204        ensures
205            self.parse_rec(ibuf).0 == self.byte_len(self.parse_rec(ibuf).1),
206        decreases ibuf.len(),
207    {
208        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
209        self.0.lemma_parse_sound_consumption(ibuf);
210        if let Some((n, v)) = self.0.spec_parse(ibuf) {
211            if 0 < n <= ibuf.len() {
212                let (n_rest, vs) = self.parse_rec(ibuf.skip(n));
213                self.lemma_parse_rec_byte_len(ibuf.skip(n));
214                self.lemma_byte_len_cons(v, vs);
215            }
216        }
217    }
218}
219
220impl<A: SpecParser> SpecParser for super::Star<A> {
221    type PVal = Seq<A::PVal>;
222
223    #[verifier::opaque]
224    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
225        let (n, vs) = self.parse_rec(ibuf);
226        Some((n, vs))
227    }
228}
229
230impl<A> Consistency for super::Star<A> where A: Consistency {
231    type Val = Seq<A::Val>;
232
233    #[verifier::opaque]
234    open spec fn consistent(&self, vs: Self::Val) -> bool {
235        forall|i: int| 0 <= i < vs.len() ==> self.0.consistent(#[trigger] vs[i])
236    }
237}
238
239impl<A> SafeParser for super::Star<A> where A: SafeParser {
240    open spec fn safe_inv(&self) -> bool {
241        self.0.safe_inv()
242    }
243
244    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
245        reveal(<super::Star::<_> as SpecParser>::spec_parse);
246        self.lemma_parse_rec_length(ibuf);
247    }
248}
249
250impl<A> SoundParser for super::Star<A> where A: SoundParser {
251    open spec fn sound_inv(&self) -> bool {
252        self.0.sound_inv()
253    }
254
255    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
256        reveal(<super::Star::<_> as SpecParser>::spec_parse);
257        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
258        self.lemma_parse_rec_byte_len(ibuf);
259    }
260
261    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
262        reveal(<super::Star::<_> as SpecParser>::spec_parse);
263        reveal(<super::Star::<_> as Consistency>::consistent);
264        self.lemma_parse_rec_consistent(ibuf);
265    }
266}
267
268impl<A: SpecSerializerDps> super::Star<A> {
269    pub open spec fn rfold_serialize_dps(&self, vs: Seq<A::SValue>, obuf: Seq<u8>) -> Seq<u8>
270        decreases vs.len(),
271    {
272        vs.fold_right_alt(|elem, buf| self.0.spec_serialize_dps(elem, buf), obuf)
273    }
274}
275
276impl<A: NonTailFmt> super::Star<A> {
277    proof fn lemma_rfold_serialize_buf(&self, vs: Seq<A::SValue>, obuf: Seq<u8>)
278        requires
279            self.serialize_dps_inv(),
280        ensures
281            exists|new_buf: Seq<u8>| self.rfold_serialize_dps(vs, obuf) == new_buf + obuf,
282        decreases vs.len(),
283    {
284        if vs.len() == 0 {
285            assert(self.rfold_serialize_dps(vs, obuf) == Seq::empty() + obuf);
286        } else {
287            let rest = vs.skip(1);
288            let rest_buf = self.rfold_serialize_dps(rest, obuf);
289
290            // induction
291            self.lemma_rfold_serialize_buf(rest, obuf);
292            let rest_witness = choose|wit: Seq<u8>|
293                self.rfold_serialize_dps(rest, obuf) == wit + obuf;
294
295            // base
296            self.0.lemma_serialize_dps_prepend(vs[0], rest_buf);
297            let fst_witness = choose|wit: Seq<u8>|
298                self.0.spec_serialize_dps(vs[0], rest_buf) == wit + rest_buf;
299
300            assert(self.rfold_serialize_dps(vs, obuf) == (fst_witness + rest_witness) + obuf);
301        }
302    }
303}
304
305impl<A> SpecSerializerDps for super::Star<A> where A: SpecSerializerDps {
306    type SValue = Seq<A::SValue>;
307
308    #[verifier::opaque]
309    open spec fn spec_serialize_dps(&self, vs: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
310        self.rfold_serialize_dps(vs, obuf)
311    }
312}
313
314pub open spec fn spec_serialize_seq<A: SpecSerializer>(inner: &A, vs: Seq<A::SVal>) -> Seq<u8> {
315    vs.fold_left(Seq::empty(), |buf: Seq<u8>, elem| buf + inner.spec_serialize(elem))
316}
317
318impl<A> SpecSerializer for super::Star<A> where A: SpecSerializer {
319    type SVal = Seq<A::SVal>;
320
321    #[verifier::opaque]
322    open spec fn spec_serialize(&self, vs: Self::SVal) -> Seq<u8> {
323        spec_serialize_seq(&self.0, vs)
324    }
325}
326
327impl<A> NonTailFmt for super::Star<A> where A: NonTailFmt {
328    open spec fn serialize_dps_inv(&self) -> bool {
329        self.0.serialize_dps_inv()
330    }
331
332    proof fn lemma_serialize_dps_prepend(&self, vs: Self::SValue, obuf: Seq<u8>) {
333        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
334        self.lemma_rfold_serialize_buf(vs, obuf);
335    }
336
337    proof fn lemma_serialize_dps_len(&self, vs: Self::SValue, obuf: Seq<u8>)
338        decreases vs.len(),
339    {
340        reveal(<super::Star::<_> as SpecSerializerDps>::spec_serialize_dps);
341        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
342        use crate::combinators::star::proof::lemma_fold_left_accumulate_nat;
343        assert(self.serialize_dps_inv());
344
345        if vs.len() == 0 {
346        } else {
347            let v0 = vs[0];
348            let rest = vs.skip(1);
349            let rest_buf = self.rfold_serialize_dps(rest, obuf);
350            // base
351            self.0.lemma_serialize_dps_len(v0, rest_buf);
352            // induction
353            self.lemma_serialize_dps_len(rest, obuf);
354            // fold_left lemmas
355            let f = |acc: nat, elem: A::SValue| acc + self.0.byte_len(elem);
356            vs.lemma_fold_left_alt(0, f);
357            rest.lemma_fold_left_alt(self.0.byte_len(v0), f);
358            lemma_fold_left_accumulate_nat(rest, self.0.byte_len(v0), f);
359        }
360    }
361}
362
363impl<A: GoodSerializer> GoodSerializer for super::Star<A> {
364    open spec fn serialize_inv(&self) -> bool {
365        self.0.serialize_inv()
366    }
367
368    proof fn lemma_serialize_len(&self, v: Self::SVal)
369        decreases v.len(),
370    {
371        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
372        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
373        if v.len() == 0 {
374        } else {
375            let v_last = v.last();
376            self.0.lemma_serialize_len(v_last);
377            self.lemma_serialize_len(v.drop_last());
378        }
379    }
380}
381
382impl<A: SpecByteLen> SpecByteLen for super::Star<A> {
383    type T = Seq<A::T>;
384
385    #[verifier::opaque]
386    open spec fn byte_len(&self, v: Self::T) -> nat {
387        v.fold_left(0, |acc: nat, elem| acc + self.0.byte_len(elem))
388    }
389}
390
391impl<A: ValueByteLen> ValueByteLen for super::Star<A> {
392    open spec fn value_byte_len(v: Self::T) -> nat {
393        v.fold_left(0, |acc: nat, elem| acc + A::value_byte_len(elem))
394    }
395
396    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
397        reveal(<super::Star::<_> as Consistency>::consistent);
398        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
399        lemma_value_seq_byte_len(self.0, v);
400    }
401}
402
403impl<C: SpecParser, N: AsLen> super::RepeatN<C, N> {
404    pub open spec fn parse_n_rec(&self, count: nat, ibuf: Seq<u8>) -> Option<(int, Seq<C::PVal>)>
405        decreases count,
406    {
407        if count == 0 {
408            Some((0, Seq::empty()))
409        } else {
410            match self.1.spec_parse(ibuf) {
411                Some((n0, v0)) => match self.parse_n_rec((count - 1) as nat, ibuf.skip(n0)) {
412                    Some((n1, vs1)) => Some((n0 + n1, seq![v0] + vs1)),
413                    None => None,
414                },
415                None => None,
416            }
417        }
418    }
419
420    proof fn lemma_parse_n_rec_count(&self, count: nat, ibuf: Seq<u8>)
421        ensures
422            self.parse_n_rec(count, ibuf) matches Some((_, vs)) ==> vs.len() == count,
423        decreases count,
424    {
425        if count == 0 {
426        } else {
427            if let Some((n0, v0)) = self.1.spec_parse(ibuf) {
428                self.lemma_parse_n_rec_count((count - 1) as nat, ibuf.skip(n0));
429            }
430        }
431    }
432
433    pub proof fn lemma_parse_exactly_n_times(&self, ibuf: Seq<u8>)
434        ensures
435            self.spec_parse(ibuf) matches Some((_, vs)) ==> vs.len() == self.0.as_nat(),
436    {
437        self.lemma_parse_n_rec_count(self.0.as_nat(), ibuf);
438    }
439}
440
441impl<C: SpecParser, N: AsLen> SpecParser for super::RepeatN<C, N> {
442    type PVal = Seq<C::PVal>;
443
444    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
445        self.parse_n_rec(self.0.as_nat(), ibuf)
446    }
447}
448
449impl<C: Consistency, N: AsLen> Consistency for super::RepeatN<C, N> {
450    type Val = Seq<C::Val>;
451
452    open spec fn consistent(&self, vs: Self::Val) -> bool {
453        &&& vs.len() == self.0.as_nat()
454        &&& super::Star(self.1).consistent(vs)
455    }
456}
457
458impl<C: SafeParser, N: AsLen> super::RepeatN<C, N> {
459    pub(crate) proof fn lemma_parse_n_len_bound(&self, count: nat, ibuf: Seq<u8>)
460        requires
461            self.1.safe_inv(),
462        ensures
463            self.parse_n_rec(count, ibuf) matches Some((n, _)) ==> 0 <= n <= ibuf.len(),
464        decreases count,
465    {
466        if count == 0 {
467        } else {
468            self.1.lemma_parse_safe(ibuf);
469            if let Some((n0, _v0)) = self.1.spec_parse(ibuf) {
470                self.lemma_parse_n_len_bound((count - 1) as nat, ibuf.skip(n0));
471            }
472        }
473    }
474}
475
476impl<C: SoundParser, N: AsLen> super::RepeatN<C, N> {
477    proof fn lemma_parse_n_byte_len(&self, count: nat, ibuf: Seq<u8>)
478        requires
479            self.1.sound_inv(),
480        ensures
481            self.parse_n_rec(count, ibuf) matches Some((n, vs)) ==> n == (super::Star(
482                self.1,
483            )).byte_len(vs),
484        decreases count,
485    {
486        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
487        if count == 0 {
488        } else {
489            self.1.lemma_parse_sound_consumption(ibuf);
490            if let Some((n0, v0)) = self.1.spec_parse(ibuf) {
491                self.lemma_parse_n_byte_len((count - 1) as nat, ibuf.skip(n0));
492                if let Some((n1, vs1)) = self.parse_n_rec((count - 1) as nat, ibuf.skip(n0)) {
493                    let star = super::Star(self.1);
494                    star.lemma_byte_len_cons(v0, vs1);
495                }
496            }
497        }
498    }
499
500    proof fn lemma_parse_n_consistent(&self, count: nat, ibuf: Seq<u8>)
501        requires
502            self.1.sound_inv(),
503        ensures
504            self.parse_n_rec(count, ibuf) matches Some((_, vs)) ==> {
505                &&& vs.len() == count
506                &&& super::Star(self.1).consistent(vs)
507            },
508        decreases count,
509    {
510        reveal(<super::Star::<_> as Consistency>::consistent);
511        if count == 0 {
512        } else {
513            self.1.lemma_parse_sound_value(ibuf);
514            if let Some((n0, v0)) = self.1.spec_parse(ibuf) {
515                self.lemma_parse_n_consistent((count - 1) as nat, ibuf.skip(n0));
516            }
517        }
518    }
519}
520
521impl<C: SafeParser, N: AsLen> SafeParser for super::RepeatN<C, N> {
522    open spec fn safe_inv(&self) -> bool {
523        self.1.safe_inv()
524    }
525
526    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
527        self.lemma_parse_n_len_bound(self.0.as_nat(), ibuf);
528    }
529}
530
531impl<C: SoundParser, N: AsLen> SoundParser for super::RepeatN<C, N> {
532    open spec fn sound_inv(&self) -> bool {
533        self.1.sound_inv()
534    }
535
536    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
537        self.lemma_parse_n_byte_len(self.0.as_nat(), ibuf);
538    }
539
540    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
541        self.lemma_parse_n_consistent(self.0.as_nat(), ibuf);
542    }
543}
544
545impl<C: SpecSerializerDps, N: AsLen> SpecSerializerDps for super::RepeatN<C, N> {
546    type SValue = Seq<C::SValue>;
547
548    open spec fn spec_serialize_dps(&self, vs: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
549        super::Star(self.1).spec_serialize_dps(vs, obuf)
550    }
551}
552
553impl<C: SpecSerializer, N: AsLen> SpecSerializer for super::RepeatN<C, N> {
554    type SVal = Seq<C::SVal>;
555
556    open spec fn spec_serialize(&self, vs: Self::SVal) -> Seq<u8> {
557        spec_serialize_seq(&self.1, vs)
558    }
559}
560
561impl<C: NonTailFmt, N: AsLen> NonTailFmt for super::RepeatN<C, N> {
562    open spec fn serialize_dps_inv(&self) -> bool {
563        self.1.serialize_dps_inv()
564    }
565
566    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
567        super::Star(self.1).lemma_serialize_dps_prepend(v, obuf);
568    }
569
570    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
571        assert(self.serialize_dps_inv());
572        super::Star(self.1).lemma_serialize_dps_len(v, obuf);
573    }
574}
575
576impl<C: GoodSerializer, N: AsLen> GoodSerializer for super::RepeatN<C, N> {
577    open spec fn serialize_inv(&self) -> bool {
578        self.1.serialize_inv()
579    }
580
581    proof fn lemma_serialize_len(&self, v: Self::SVal) {
582        reveal(<super::Star::<_> as SpecSerializer>::spec_serialize);
583        super::Star(self.1).lemma_serialize_len(v);
584    }
585}
586
587impl<C: SpecByteLen, N: AsLen> SpecByteLen for super::RepeatN<C, N> {
588    type T = Seq<C::T>;
589
590    open spec fn byte_len(&self, vs: Self::T) -> nat {
591        super::Star(self.1).byte_len(vs)
592    }
593}
594
595impl<C: MinMaxByteLen, N: AsLen> MinMaxByteLen for super::RepeatN<C, N> {
596    open spec fn min(&self) -> nat {
597        self.0.as_nat() * self.1.min()
598    }
599
600    open spec fn max(&self) -> nat {
601        self.0.as_nat() * self.1.max()
602    }
603
604    proof fn lemma_min_max_byte_len(&self, vs: Self::T) {
605        reveal(<super::Star::<_> as Consistency>::consistent);
606        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
607        lemma_seq_min_max_byte_len(self.1, vs);
608        assert(vs.len() == self.0.as_nat());
609    }
610}
611
612impl<C: ValueByteLen, N: AsLen> ValueByteLen for super::RepeatN<C, N> {
613    open spec fn value_byte_len(vs: Self::T) -> nat {
614        <super::Star<C> as ValueByteLen>::value_byte_len(vs)
615    }
616
617    proof fn lemma_value_len_matches_byte_len(&self, vs: Self::T) {
618        reveal(<super::Star::<_> as Consistency>::consistent);
619        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
620        lemma_value_seq_byte_len(self.1, vs);
621    }
622}
623
624impl<const N: usize, C: SpecParser> SpecParser for super::Array<N, C> {
625    type PVal = Seq<C::PVal>;
626
627    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
628        super::RepeatN(N, self.0).spec_parse(ibuf)
629    }
630}
631
632impl<const N: usize, C: Consistency> Consistency for super::Array<N, C> {
633    type Val = Seq<C::Val>;
634
635    open spec fn consistent(&self, v: Self::Val) -> bool {
636        super::RepeatN(N, self.0).consistent(v)
637    }
638}
639
640impl<const N: usize, C: SafeParser> SafeParser for super::Array<N, C> {
641    open spec fn safe_inv(&self) -> bool {
642        super::RepeatN(N, self.0).safe_inv()
643    }
644
645    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
646        super::RepeatN(N, self.0).lemma_parse_safe(ibuf);
647    }
648}
649
650impl<const N: usize, C: SoundParser> SoundParser for super::Array<N, C> {
651    open spec fn sound_inv(&self) -> bool {
652        super::RepeatN(N, self.0).sound_inv()
653    }
654
655    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
656        super::RepeatN(N, self.0).lemma_parse_sound_consumption(ibuf);
657    }
658
659    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
660        super::RepeatN(N, self.0).lemma_parse_sound_value(ibuf);
661    }
662}
663
664impl<const N: usize, C: SpecSerializerDps> SpecSerializerDps for super::Array<N, C> {
665    type SValue = Seq<C::SValue>;
666
667    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
668        super::RepeatN(N, self.0).spec_serialize_dps(v, obuf)
669    }
670}
671
672impl<const N: usize, C: SpecSerializer> SpecSerializer for super::Array<N, C> {
673    type SVal = Seq<C::SVal>;
674
675    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
676        super::RepeatN(N, self.0).spec_serialize(v)
677    }
678}
679
680impl<const N: usize, C: NonTailFmt> NonTailFmt for super::Array<N, C> {
681    open spec fn serialize_dps_inv(&self) -> bool {
682        super::RepeatN(N, self.0).serialize_dps_inv()
683    }
684
685    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
686        super::RepeatN(N, self.0).lemma_serialize_dps_prepend(v, obuf);
687    }
688
689    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
690        super::RepeatN(N, self.0).lemma_serialize_dps_len(v, obuf);
691    }
692}
693
694impl<const N: usize, C: GoodSerializer> GoodSerializer for super::Array<N, C> {
695    open spec fn serialize_inv(&self) -> bool {
696        super::RepeatN(N, self.0).serialize_inv()
697    }
698
699    proof fn lemma_serialize_len(&self, v: Self::SVal) {
700        super::RepeatN(N, self.0).lemma_serialize_len(v);
701    }
702}
703
704impl<const N: usize, C: SpecByteLen> SpecByteLen for super::Array<N, C> {
705    type T = Seq<C::T>;
706
707    open spec fn byte_len(&self, v: Self::T) -> nat {
708        super::RepeatN(N, self.0).byte_len(v)
709    }
710}
711
712impl<const N: usize, C: MinMaxByteLen> MinMaxByteLen for super::Array<N, C> {
713    open spec fn min(&self) -> nat {
714        super::RepeatN(N, self.0).min()
715    }
716
717    open spec fn max(&self) -> nat {
718        super::RepeatN(N, self.0).max()
719    }
720
721    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
722        super::RepeatN(N, self.0).lemma_min_max_byte_len(v);
723    }
724}
725
726impl<const N: usize, C: StaticByteLen> StaticByteLen for super::Array<N, C> {
727    open spec fn static_byte_len() -> nat {
728        N as nat * C::static_byte_len()
729    }
730
731    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
732        let star = super::Star(self.0);
733        reveal(<super::Star::<_> as Consistency>::consistent);
734        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
735        lemma_static_seq_byte_len(star.0, v);
736        assert(self.byte_len(v) == star.byte_len(v));
737        assert(v.len() == N as nat);
738        assert(self.byte_len(v) == v.len() * C::static_byte_len());
739    }
740}
741
742impl<const N: usize, C: ValueByteLen> ValueByteLen for super::Array<N, C> {
743    open spec fn value_byte_len(v: Self::T) -> nat {
744        <super::Star<C> as ValueByteLen>::value_byte_len(v)
745    }
746
747    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
748        reveal(<super::Star::<_> as Consistency>::consistent);
749        reveal(<super::Star::<_> as SpecByteLen>::byte_len);
750        lemma_value_seq_byte_len(self.0, v);
751        assert(self.byte_len(v) == (super::Star(self.0)).byte_len(v));
752    }
753}
754
755impl<A: SpecParser, B: SpecParser> SpecParser for super::Repeat<A, B> {
756    type PVal = (Seq<A::PVal>, B::PVal);
757
758    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
759        Pair(super::Star(self.0), self.1).spec_parse(ibuf)
760    }
761}
762
763impl<A, B> Consistency for super::Repeat<A, B> where A: Consistency, B: Consistency {
764    type Val = (Seq<A::Val>, B::Val);
765
766    open spec fn consistent(&self, v: Self::Val) -> bool {
767        Pair(super::Star(self.0), self.1).consistent(v)
768    }
769}
770
771impl<A, B> SafeParser for super::Repeat<A, B> where A: SafeParser, B: SafeParser {
772    open spec fn safe_inv(&self) -> bool {
773        &&& self.0.safe_inv()
774        &&& self.1.safe_inv()
775    }
776
777    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
778        Pair(super::Star(self.0), self.1).lemma_parse_safe(ibuf)
779    }
780}
781
782impl<A, B> SoundParser for super::Repeat<A, B> where A: SoundParser, B: SoundParser {
783    open spec fn sound_inv(&self) -> bool {
784        &&& self.0.sound_inv()
785        &&& self.1.sound_inv()
786    }
787
788    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
789        Pair(super::Star(self.0), self.1).lemma_parse_sound_consumption(ibuf)
790    }
791
792    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
793        Pair(super::Star(self.0), self.1).lemma_parse_sound_value(ibuf)
794    }
795}
796
797impl<A: SpecSerializerDps, B: SpecSerializerDps> SpecSerializerDps for super::Repeat<A, B> {
798    type SValue = (Seq<A::SValue>, B::SValue);
799
800    open spec fn spec_serialize_dps(&self, vs: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
801        Pair(super::Star(self.0), self.1).spec_serialize_dps(vs, obuf)
802    }
803}
804
805impl<A: SpecSerializer, B: SpecSerializer> SpecSerializer for super::Repeat<A, B> {
806    type SVal = (Seq<A::SVal>, B::SVal);
807
808    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
809        Pair(super::Star(self.0), self.1).spec_serialize(v)
810    }
811}
812
813impl<A: NonTailFmt, B: NonTailFmt> NonTailFmt for super::Repeat<A, B> {
814    open spec fn serialize_dps_inv(&self) -> bool {
815        &&& self.0.serialize_dps_inv()
816        &&& self.1.serialize_dps_inv()
817    }
818
819    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
820        Pair(super::Star(self.0), self.1).lemma_serialize_dps_prepend(v, obuf)
821    }
822
823    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
824        Pair(super::Star(self.0), self.1).lemma_serialize_dps_len(v, obuf);
825    }
826}
827
828impl<A: GoodSerializer, B: GoodSerializer> GoodSerializer for super::Repeat<A, B> {
829    open spec fn serialize_inv(&self) -> bool {
830        &&& self.0.serialize_inv()
831        &&& self.1.serialize_inv()
832    }
833
834    proof fn lemma_serialize_len(&self, v: Self::SVal) {
835        assert(self.serialize_inv());
836        Pair(super::Star(self.0), self.1).lemma_serialize_len(v);
837    }
838}
839
840impl<A: SpecByteLen, B: SpecByteLen> SpecByteLen for super::Repeat<A, B> {
841    type T = (Seq<A::T>, B::T);
842
843    open spec fn byte_len(&self, v: Self::T) -> nat {
844        Pair(super::Star(self.0), self.1).byte_len(v)
845    }
846}
847
848impl<A: ValueByteLen, B: ValueByteLen> ValueByteLen for super::Repeat<A, B> {
849    open spec fn value_byte_len(v: Self::T) -> nat {
850        <Pair<super::Star<A>, B> as ValueByteLen>::value_byte_len(v)
851    }
852
853    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
854        Pair(super::Star(self.0), self.1).lemma_value_len_matches_byte_len(v);
855    }
856}
857
858} // verus!
vest_lib/combinators/star/spec.rs

vest_lib/combinators/star/
spec.rs
