vest_lib/combinators/refined/
spec.rs

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

vest_lib/combinators/refined/
spec.rs
