vest_lib/combinators/choice/
spec.rs

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

vest_lib/combinators/choice/
spec.rs
