vest_lib/combinators/cond/
spec.rs

1//! Specification for boolean-gated formats.
2use crate::core::{proof::*, spec::*};
3use vstd::prelude::*;
4
5verus! {
6
7impl<Inner: SpecParser> SpecParser for super::Cond<Inner> {
8    type PVal = Inner::PVal;
9
10    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
11        if self.0 {
12            self.1.spec_parse(ibuf)
13        } else {
14            None
15        }
16    }
17}
18
19impl<Inner: Consistency> Consistency for super::Cond<Inner> {
20    type Val = Inner::Val;
21
22    open spec fn consistent(&self, v: Self::Val) -> bool {
23        self.0 && self.1.consistent(v)
24    }
25}
26
27impl<Inner: SafeParser> SafeParser for super::Cond<Inner> {
28    open spec fn safe_inv(&self) -> bool {
29        self.1.safe_inv()
30    }
31
32    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
33        if self.0 {
34            self.1.lemma_parse_safe(ibuf);
35        }
36    }
37}
38
39impl<Inner: SoundParser> SoundParser for super::Cond<Inner> {
40    open spec fn sound_inv(&self) -> bool {
41        self.1.sound_inv()
42    }
43
44    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
45        if self.0 {
46            self.1.lemma_parse_sound_consumption(ibuf);
47        }
48    }
49
50    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
51        if self.0 {
52            self.1.lemma_parse_sound_value(ibuf);
53            if let Some((_, v)) = self.1.spec_parse(ibuf) {
54                assert(self.consistent(v));
55            }
56        }
57    }
58}
59
60impl<Inner: SpecSerializerDps> SpecSerializerDps for super::Cond<Inner> {
61    type SValue = Inner::SValue;
62
63    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
64        self.1.spec_serialize_dps(v, obuf)
65    }
66}
67
68impl<Inner: SpecSerializer> SpecSerializer for super::Cond<Inner> {
69    type SVal = Inner::SVal;
70
71    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
72        self.1.spec_serialize(v)
73    }
74}
75
76impl<Inner: NonTailFmt> NonTailFmt for super::Cond<Inner> {
77    open spec fn serialize_dps_inv(&self) -> bool {
78        self.1.serialize_dps_inv()
79    }
80
81    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
82        self.1.lemma_serialize_dps_prepend(v, obuf);
83    }
84
85    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
86        self.1.lemma_serialize_dps_len(v, obuf);
87    }
88}
89
90impl<Inner: GoodSerializer> GoodSerializer for super::Cond<Inner> {
91    open spec fn serialize_inv(&self) -> bool {
92        self.1.serialize_inv()
93    }
94
95    proof fn lemma_serialize_len(&self, v: Self::SVal) {
96        self.1.lemma_serialize_len(v);
97    }
98}
99
100impl<Inner: SpecByteLen> SpecByteLen for super::Cond<Inner> {
101    type T = Inner::T;
102
103    open spec fn byte_len(&self, v: Self::T) -> nat {
104        self.1.byte_len(v)
105    }
106}
107
108impl<Inner: MinMaxByteLen> MinMaxByteLen for super::Cond<Inner> {
109    open spec fn min(&self) -> nat {
110        self.1.min()
111    }
112
113    open spec fn max(&self) -> nat {
114        self.1.max()
115    }
116
117    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
118        self.1.lemma_min_max_byte_len(v);
119    }
120}
121
122impl<Inner: StaticByteLen> StaticByteLen for super::Cond<Inner> {
123    open spec fn static_byte_len() -> nat {
124        Inner::static_byte_len()
125    }
126
127    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
128        self.1.lemma_static_len_matches_byte_len(v);
129    }
130}
131
132impl<Inner: ValueByteLen> ValueByteLen for super::Cond<Inner> {
133    open spec fn value_byte_len(v: Self::T) -> nat {
134        Inner::value_byte_len(v)
135    }
136
137    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
138        self.1.lemma_value_len_matches_byte_len(v);
139    }
140}
141
142} // verus!
vest_lib/combinators/cond/spec.rs

vest_lib/combinators/cond/
spec.rs
