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

vest_lib/combinators/star/
spec.rs
